--definitional-cnf=24   --split-reuse-defs --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -tKBO -Garity -F1 --delete-bad-limit=150000000 -WSelectComplexG  -H'(1*ConjectureRelativeTermWeight(PreferGroundGoals,0,1,0.1,100,9999,100,0,1,9999.9,1.5,0.7),1*FIFOWeight(PreferProcessed),1*RelevanceLevelWeight2(PreferWatchlist,1,1,0,1,100,-2,-2,1,1.5,4,1),4*RelevanceLevelWeight2(PreferUnitGroundGoals,1,1,0,0,10,-2,1,7,2.5,4,4),5*ConjectureRelativeTermWeight(PreferGroundGoals,1,0,0.1,100,400,100,18,1,9999.9,2,0.7))'