--definitional-cnf=24 --destructive-er-aggressive --destructive-er --prefer-initial-clauses -F1 --delete-bad-limit=150000000  --sine='GSinE(CountFormulas,,2.0,,04,40,1.0)' --forward-context-sr -Garity -WSelectMaxLComplexAvoidPosPred --simul-paramod --split-clauses=4 -tLPO4 -H'(2*ConjectureSymbolWeight(ConstPrio,10,10,5,5,5,1.5,1.5,1.5),1*Clauseweight(ByCreationDate,2,1,0.8),1*Clauseweight(ConstPrio,3,1,1),2*FIFOWeight(PreferProcessed),10*Refinedweight(PreferGroundGoals,2,1,2,1.0,1),1*Refinedweight(SimulateSOS,1,1,2,1.5,2))'  
