--definitional-cnf=24  --split-clauses=4 --split-reuse-defs --simul-paramod  --destructive-er-aggressive --destructive-er --prefer-initial-clauses -tAuto -Ginvfreqconstmin -F1 --delete-bad-limit=150000000 -WSelectComplexG  -H'(10*RelevanceLevelWeight2(PreferWatchlist,2,0,1,0,50,-1,-1,1,2.5,9999.9,9999.9),2*SymbolTypeweight(SimulateSOS,7,20,5,400,3,0.8,5),34*ConjectureRelativeTermWeight(SimulateSOS,0,3,0.1,18,200,50,50,1,2,2,2.5),4*OrientLMaxWeight(ConstPrio,3,2,1,9999.9,9999.9))'