--definitional-cnf=24 --split-aggressive --split-clauses=4 --split-reuse-defs --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -tKBO -Ginvfreqconstmin -F1 --delete-bad-limit=150000000 -WSelectComplexG  -H'(1*RelevanceLevelWeight2(ByNegLitDist,1,2,2,1,4,-1,2,1,2,9999.9,9999.9),1*RelevanceLevelWeight2(SimulateSOS,0,2,1,0,50,4,9999,400,4,5,4),1*SymbolTypeweight(SimulateSOS,3,1,-1,1,2,2,9999.9),2*ConjectureRelativeTermWeight(PreferUnitGroundGoals,0,1,0.3,10,100,50,50,1,5,2,2))'