--definitional-cnf=24   --split-reuse-defs --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -tLPO4 -Garity -F1 --delete-bad-limit=150000000 -WSelectComplexG --sine='GSinE(CountFormulas,,5.0,,,60,1.0)' -H'(13*RelevanceLevelWeight2(ConstPrio,2,1,0,0,100,7,10,100,0.3,4,3),2*FIFOWeight(PreferProcessed),3*ConjectureGeneralSymbolWeight(PreferNonGoals,50,100,3,300,4,10,100,0.3,2,4),8*RelevanceLevelWeight2(SimulateSOS,2,2,0,0,2,1,20,3,1.5,3,4))'
