--delete-bad-limit=150000000 --split-aggressive --split-reuse-defs --forward-context-sr --definitional-cnf --prefer-initial-clauses --forward-demod-level=1 --destructive-er --destructive-er-aggressive --oriented-simul-paramod -tKBO6 -Garity -warity -WSelectComplexG --sine='GSinE(CountFormulas,hypos,1.1,,2,100,1.0)' -H'(1*ConjectureSymbolWeight(PreferUnitGroundGoals,5,9999,4,-1,18,0.1,4,1),10*StaggeredWeight(PreferNonGoals,1),13*ConjectureTermPrefixWeight(PreferGroundGoals,0,3,0,10,1,1,1.5,1.5))'
