--definitional-cnf=24 --split-aggressive --split-clauses=4 --split-reuse-defs --oriented-simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -tLPO4 -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred --sine='GSinE(CountFormulas,hypos,1.5,,,100,1.0)' -H'(1*Clauseweight(PreferGoals,20,9999,3),1*ConjectureTermPrefixWeight(ConstPrio,1,3,5,9999.9,2,5,5,5),1*FIFOWeight(PreferProcessed),2*ConjectureLevDistanceWeight(PreferNonGoals,1,0,20,300,4,0,2.5,0.8,3),4*ConjectureGeneralSymbolWeight(ConstPrio,4,10,200,3,-2,1,50,0.7,4,2))'
