let eq_foterm = eq_foterm B.eq;;
let compute_unit_clause_weight = compute_unit_clause_weight;;
let compute_goal_weight = compute_goal_weight;;
let eq_foterm = eq_foterm B.eq;;
let compute_unit_clause_weight = compute_unit_clause_weight;;
let compute_goal_weight = compute_goal_weight;;