--definitional-cnf=24 --split-aggressive --split-clauses=4 --split-reuse-defs --oriented-simul-paramod  --destructive-er-aggressive --destructive-er --prefer-initial-clauses -tLPO4 -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectComplexG --sine='GSinE(CountFormulas,hypos,1.1,,02,500,1.0)' -H'(2*StaggeredWeight(PreferNonGoals,1),3*ConjectureGeneralSymbolWeight(DeferSOS,18,9999,9999,-1,0,20,200,0.2,0.2,2),34*ConjectureGeneralSymbolWeight(PreferGroundGoals,7,200,9999,5,0,-2,4,0.3,2,2.5),4*StaggeredWeight(PreferUnitGroundGoals,1.5))'
