--definitional-cnf=24   --split-reuse-defs --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -tLPO4 -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred  -H'(1*ConjectureTermPrefixWeight(DeferSOS,1,3,0.1,9999.9,0,0.8,0.5,9999.9),1*PNRefinedweight(SimulateSOS,5,9999,9999,0,0.1,0.1,4),4*ConjectureGeneralSymbolWeight(PreferProcessed,10,9999,400,4,20,-2,50,0.2,0.3,2.5),4*StaggeredWeight(DeferSOS,1.5))'