--definitional-cnf=24    --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -tKBO6 -Ginvfreqconstmin -F1 --delete-bad-limit=150000000 -WSelectComplexG  -H'(1*ConjectureRelativeSymbolWeight(PreferGroundGoals,4,20,1,18,200,0.3,1,9999.9),1*OrientLMaxWeight(PreferProcessed,2,2,0.7,1,2),34*ConjectureRelativeTermWeight(PreferWatchlist,0,1,0.1,100,200,100,100,1,5,1.5,1.5),34*RelevanceLevelWeight2(ConstPrio,2,2,2,2,9999,0,2,9999,3,5,2.5),8*RelevanceLevelWeight2(PreferGroundGoals,2,2,2,0,9999,18,0,100,0.8,4,4))'