--definitional-cnf=24    --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -tKBO6 -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred  -H'(1*ConjectureSymbolWeight(ConstPrio,9999,5,10,50,50,4,3,0.5),1*ConjectureTermPrefixWeight(PreferNonGoals,1,3,100,9999.9,0,9999.9,3,5),1*FIFOWeight(PreferProcessed),3*ConjectureRelativeSymbolWeight(ConstPrio,0.7,100,100,100,100,2,1.5,1.5),5*Clauseweight(PreferUnitGroundGoals,7,9999,5))'