--definitional-cnf=24 --destructive-er-aggressive --destructive-er --prefer-initial-clauses -F1 --delete-bad-limit=150000000  --sine='GSinE(CountFormulas,hypos,5.0,,6,80,1.0)' -Ginvfreqconstmin -WSelectComplexG --simul-paramod --split-reuse-defs -tKBO6 -H'(8*ConjectureRelativeSymbolWeight(ConstPrio,0.1,100,100,100,100,1.5,1.5,1.5),4*ConjectureRelativeSymbolWeight(SimulateSOS,0.5,100,100,100,100,1.5,1.5,1),2*FIFOWeight(PreferProcessed),10*Refinedweight(SimulateSOS,1,1,2,1.5,2))' 
