--definitional-cnf=24    --oriented-simul-paramod  --destructive-er-aggressive --destructive-er --prefer-initial-clauses -tAuto -Garity -F1 --delete-bad-limit=150000000 -WSelectComplexG  -H'(1*FIFOWeight(PreferProcessed),1*RelevanceLevelWeight2(PreferProcessed,2,1,0,1,18,-2,0,20,0.8,9999.9,9999.9),1*SymbolTypeweight(SimulateSOS,4,-1,-1,1,2,4,4),13*ConjectureRelativeTermWeight(PreferNonGoals,1,0,0.1,100,300,100,10,1,4,2,0.8))'