sp-var-dec-heur sp-learned-clause-sort-heur sp-orig-clause-sort-heur sp-res-order-heur sp-clause-del-heur sp-phase-dec-heur sp-resolution sp-variable-decay sp-clause-decay sp-restart-inc sp-learned-size-factor sp-learned-clauses-inc sp-clause-activity-inc sp-var-activity-inc sp-rand-phase-dec-freq sp-rand-var-dec-freq sp-rand-var-dec-scaling sp-rand-phase-scaling sp-max-res-lit-inc sp-first-restart sp-res-cutoff-cls sp-res-cutoff-lits sp-max-res-runs sp-update-dec-queue sp-use-pure-literal-rule sp-clause-inversion
0 0 0 0 2 5 1 1.4 1.4 1.5 0.4 1.3 1.0 1.0 0.001 0.001 1.0 1.0 1 100 8 400 4 1 1 NA