--definitional-cnf=24 --split-aggressive --split-clauses=4  --oriented-simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -tLPO4 -Garity -F1 --delete-bad-limit=150000000 -WSelectComplexG  -H'(13*ConjectureRelativeSymbolWeight(PreferProcessed,3,5,-1,20,-2,1.5,9999.9,0.8),13*FIFOWeight(PreferUnitGroundGoals),5*RelevanceLevelWeight2(SimulateSOS,1,2,0,1,300,2,0,400,1,3,9999.9),8*ConjectureTermPrefixWeight(PreferProcessed,0,3,0,9999.9,1,2.5,1,0.2))'