--definitional-cnf=24  --split-clauses=4  --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -tKBO6 -Ginvfreqconstmin -F1 --delete-bad-limit=150000000000 -WSelectComplexG  -H'(1*ConjectureRelativeSymbolWeight(PreferNonGoals,3,9999,4,3,5,4,4,2.5),1*RelevanceLevelWeight2(ConstPrio,1,0,2,2,7,-1,2,0,0.2,9999.9,9999.9),2*ConjectureRelativeTermWeight(PreferGoals,0,3,0.1,100,9999,200,1,1,3,2,2.5),2*SymbolTypeweight(PreferNonGoals,20,7,-1,4,3,2,1.5))'
