--destructive-er --destructive-er --destructive-er-aggressive --forward-demod-level=1 --literal-selection-strategy=SelectMaxLComplexAvoidPosPred --order-constant-weight=1 --order-precedence-generation=invfreq --order-weight-generation=invfreqrank --presat-simplify --simul-paramod --strong-destructive-er --term-ordering=KBO6 -H'(1*ConjectureRelativeSymbolWeight(SimulateSOS,0.5,100,100,100,100,1.5,1.5,1),4*ConjectureRelativeSymbolWeight(ConstPrio,0.1,100,100,100,100,1.5,1.5,1.5),1*FIFOWeight(PreferProcessed),1*ConjectureRelativeSymbolWeight(PreferNonGoals,0.5,100,100,100,100,1.5,1.5,1),4*Refinedweight(SimulateSOS,3,2,2,1.5,2))'