let wl, ml = weight_of_term l in
let wr, mr = weight_of_term r in
weight_of_polynomial (wl+wr) (ml@mr)
;;
let compute_clause_weight (_,nl,pl,_,_) =
let wl, ml = weight_of_term l in
let wr, mr = weight_of_term r in
weight_of_polynomial (wl+wr) (ml@mr)
;;
let compute_clause_weight (_,nl,pl,_,_) =