--definitional-cnf=24    --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -tAuto -Ginvfreqconstmin -F1 --delete-bad-limit=150000000 -WSelectComplexG  -H'(1*ConjectureRelativeSymbolWeight(PreferWatchlist,2,10,2,50,200,2.5,2,9999.9),1*RelevanceLevelWeight2(PreferProcessed,1,2,1,2,400,-1,2,18,1.5,9999.9,5),1*RelevanceLevelWeight2(SimulateSOS,1,1,2,1,5,-1,-2,9999,9999.9,9999.9,9999.9),10*ConjectureRelativeTermWeight(PreferWatchlist,0,1,0.1,20,50,50,50,1,9999.9,4,2.5))'