-tKBO6 --order-weight-generation=invfreqrank --order-precedence-generation=invfreq --no-eq-unfolding --definitional-cnf=6 --presat-simplify --literal-selection-strategy=SelectMaxLComplexAvoidAppVar --simul-paramod --forward-context-sr --forward-demod-level=1 --destructive-er-aggressive --strong-destructive-er --satcheck-proc-interval=5000 --satcheck=ConjMinMinFreq --delete-bad-limit=2000000000 --sos-uses-input-types --neg-ext=all --pos-ext=all --ext-sup-max-depth=0 -H'(1*ConjectureRelativeSymbolWeight(SimulateSOS,0.5,100,100,100,100,1.5,1.5,1),4*ConjectureRelativeSymbolWeight(PreferFO,0.1,100,100,100,100,1.5,1.5,1.5),1*FIFOWeight(PreferProcessed),1*ConjectureRelativeSymbolWeight(PreferHOSteps,0.5,100,100,100,100,1.5,1.5,1),4*Refinedweight(SimulateSOS,3,2,2,1.5,2))'
