-tKBO6 --order-weight-generation=precrank10 --order-precedence-generation=invfreq --strong-rw-inst --order-constant-weight=1 --no-eq-unfolding --definitional-cnf=4 --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 --lift-lambdas=false --local-rw=true --fool-unroll=false -H'(@@@freq:1@@@*EnigmaticLgb(@@@prio:ConstPrio@@@,"solverpy_db/models/@@@sel:default@@@",@@@weights:1@@@,@@@thrsel:0.5@@@))'