--definitional-cnf=24 --destructive-er-aggressive --destructive-er --prefer-initial-clauses -F1 --delete-bad-limit=150000000  --sine='GSinE(CountFormulas,hypos,5.0,,,100,1.0)' --forward-context-sr -Ginvfreqconstmin -WSelectMaxLComplexAvoidPosPred --simul-paramod --split-clauses=4 --split-reuse-defs -tKBO6 -H'(6*ConjectureRelativeSymbolWeight(ConstPrio,0.1,100,100,100,100,1.5,1.5,1.5),1*ConjectureRelativeSymbolWeight(PreferNonGoals,0.5,100,100,100,100,1.5,1.5,1),2*ConjectureSymbolWeight(ConstPrio,10,10,5,5,5,1.5,1.5,1.5),1*Clauseweight(ByCreationDate,2,1,0.8),1*FIFOWeight(ConstPrio),1*FIFOWeight(PreferProcessed),1*Refinedweight(PreferGroundGoals,2,1,2,1.0,1))' 
