--definitional-cnf=24  --split-clauses=4 --split-reuse-defs --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -tLPO4 -Garity -F1 --delete-bad-limit=150000000 -WSelectComplexG --sine='GSinE(CountFormulas,,6.0,,04,40,1.0)' -H'(1*ConjectureSymbolWeight(SimulateSOS,9999,10,10,50,3,2.5,0.3,1.5),10*ConjectureRelativeTermWeight(SimulateSOS,0,1,0.1,100,400,400,-1,1,2,1.5,1.5),21*StaggeredWeight(PreferNonGoals,2),34*RelevanceLevelWeight2(PreferProcessed,2,2,2,1,4,-2,4,18,4,9999.9,9999.9),5*ConjectureSymbolWeight(SimulateSOS,400,400,1,10,18,0.1,2,2))'
