-tKBO6 --order-weight-generation=precrank10 --order-precedence-generation=invfreq --strong-rw-inst --order-constant-weight=1 --no-eq-unfolding --presat-simplify --literal-selection-strategy=SelectMaxLComplexAvoidAppVar --simul-paramod --forward-context-sr --forward-demod-level=1 --condense --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 --local-rw=true -H'(2*ConjectureRelativeSymbolWeight(PreferGround,0.5,100,100,100,100,1.5,1.5,1),6*ConjectureRelativeSymbolWeight(ByDerivationDepth,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),2*Refinedweight(PreferGoals,3,2,2,1.5,2))'
