--definitional-cnf=24 --split-aggressive    --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -tLPO4 -Ginvfreqconstmin -F1 --delete-bad-limit=150000000 -WSelectNewComplexAHP  -H'(1*ConjectureRelativeSymbolWeight(PreferWatchlist,0.1,200,100,0,20,9999.9,0.2,2.5),1*StaggeredWeight(DeferSOS,2),10*ConjectureRelativeSymbolWeight(ConstPrio,0.1,100,100,100,100,1.5,1.5,1.5))'