--delete-bad-limit=150000000 --split-aggressive --split-reuse-defs --forward-context-sr --definitional-cnf --prefer-initial-clauses --forward-demod-level=1 --destructive-er --destructive-er-aggressive --simul-paramod -tLPO4 -Ginvfreq -WSelectComplexG --sine='GSinE(CountFormulas,hypos,5.0,,3,500,1.0)' -H'(1*PNRefinedweight(PreferUnitGroundGoals,200,400,1,50,2,0.2,0.5),2*RelevanceLevelWeight2(DeferSOS,1,1,2,0,50,-1,100,5,4,4,1.5),8*ConjectureRelativeTermWeight(ConstPrio,0,3,0.1,100,300,200,10,1,0.8,1.5,0.2),21*RelevanceLevelWeight2(PreferUnitGroundGoals,2,2,2,2,9999,5,200,9999,2,4,4))'
