--definitional-cnf=24 --split-aggressive --split-clauses=4   --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -tLPO4 -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=1500000000 -WSelectMaxLComplexAvoidPosPred  -H'(13*ConjectureRelativeSymbolWeight(PreferNonGoals,0.1,100,50,20,5,0.1,1.5,1.5),3*ConjectureTermPrefixWeight(DeferSOS,1,3,0.1,9999.9,0,0.1,3,9999.9),4*RelevanceLevelWeight2(PreferUnitGroundGoals,1,2,2,2,4,-1,3,18,2,9999.9,9999.9),5*StaggeredWeight(DeferSOS,1.5),8*ConjectureGeneralSymbolWeight(PreferGroundGoals,5,300,300,4,-2,4,50,2,0.2,2.5),8*RelevanceLevelWeight2(PreferProcessed,1,2,2,0,4,-1,2,18,9999.9,9999.9,9999.9))'