--definitional-cnf=24  --split-clauses=7  --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -tAuto -Ginvfreqconstmin -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred --sine='GSinE(CountFormulas,hypos,1.1,,02,500,1.0)' -H'(2*ConjectureGeneralSymbolWeight(PreferWatchlist,3,200,5,4,-2,4,18,3,1,2.5),2*ConjectureTermPrefixWeight(PreferNonGoals,1,2,5,9999.9,0,0.1,2.5,9999.9),4*FIFOWeight(PreferProcessed),4*RelevanceLevelWeight2(PreferUnitGroundGoals,0,0,1,0,4,4,5,-2,9999.9,9999.9,0.5),5*Clauseweight(PreferWatchlist,1,18,4),8*StaggeredWeight(PreferGroundGoals,1))'
