--definitional-cnf=24    --simul-paramod  --destructive-er-aggressive --destructive-er --prefer-initial-clauses -tAuto -Ginvfreqconstmin -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred --sine='GSinE(CountFormulas,hypos,6.0,,02,80,1.0)' -H'(5*ConjectureRelativeSymbolWeight(PreferUnitGroundGoals,0.2,400,50,200,300,9999.9,2.5,3),5*Refinedweight(PreferGoals,2,18,4,2,9999.9),8*RelevanceLevelWeight2(DeferSOS,0,0,2,0,100,1,1,0,9999.9,1.5,4))'
