--definitional-cnf=24 --destructive-er-aggressive --destructive-er --prefer-initial-clauses -F1 --delete-bad-limit=150000000 --forward-context-sr -winvfreqrank -c1 -Ginvfreq -WSelectMaxLComplexAvoidPosPred --simul-paramod -tLPO4 -H'(6*ConjectureRelativeSymbolWeight(ConstPrio,0.1,100,100,100,100,1.5,1.5,1.5),1*Clauseweight(ByCreationDate,2,1,0.8),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(ConstPrio),2*FIFOWeight(PreferProcessed),2*Refinedweight(PreferGroundGoals,2,1,2,1.0,1))' 