--definitional-cnf=24 --split-aggressive --split-clauses=4  --simul-paramod  --destructive-er-aggressive --destructive-er --prefer-initial-clauses -tKBO -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectComplexG  -H'(1*ConjectureGeneralSymbolWeight(DeferSOS,3,18,5,4,-1,4,0,2.5,1,0.5),1*RelevanceLevelWeight(ConstPrio,0,2,2,1,2,10,200,1,4,0.3,1),13*ConjectureRelativeTermWeight(SimulateSOS,0,0,0.1,20,9999,50,50,1,4,2,4),2*RelevanceLevelWeight(PreferWatchlist,0,1,2,1,7,20,9999,200,5,3,1),3*RelevanceLevelWeight2(PreferProcessed,1,2,2,1,4,20,2,20,0.5,9999.9,9999.9),3*RelevanceLevelWeight2(PreferUnitGroundGoals,1,0,0,2,100,2,-2,-2,1.5,4,3))'