--definitional-cnf=24 --destructive-er-aggressive --destructive-er --prefer-initial-clauses -F1 --delete-bad-limit=150000000 --forward-context-sr -Garity -WSelectMaxLComplexAvoidPosPred --simul-paramod --split-clauses=4 --split-reuse-defs -tLPO4 -H'(8*ConjectureRelativeSymbolWeight(ConstPrio,0.1,100,100,100,100,1.5,1.5,1.5),3*ConjectureRelativeSymbolWeight(SimulateSOS,0.5,100,100,100,100,1.5,1.5,1),1*Clauseweight(ByCreationDate,2,1,0.8),1*Clauseweight(ConstPrio,3,1,1),1*FIFOWeight(PreferProcessed),8*Refinedweight(PreferGroundGoals,2,1,2,1.0,1),1*Refinedweight(SimulateSOS,1,1,2,1.5,2))'  