--definitional-cnf=24 --split-aggressive  --split-reuse-defs --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -tKBO6 -Garity -F1 --delete-bad-limit=1500000000 -WSelectComplexG --sine=GSinE(CountFormulas,hypos,6.0,,,60,1.0) -H'(1*ConjectureSymbolWeight(SimulateSOS,20,7,7,9999,1,2.5,9999.9,0.3),2*ConjectureRelativeTermWeight(PreferProcessed,0,2,0.3,10,9999,400,5,1,4,3,3),5*ConjectureRelativeTermWeight(PreferProcessed,0,1,0.1,100,400,100,7,1,9999.9,3,0.1),8*ConjectureTermPrefixWeight(PreferNonGoals,0,2,0.1,9999.9,1,9999.9,3,5))'