+ let build_new_clause bag maxvar filter t subst vl id id2 pos dir =
+ let maxvar, vl, relocsubst = Utils.relocate maxvar vl in
+ let subst = Subst.concat relocsubst subst in
+ let proof = Terms.Step(Terms.SuperpositionRight,id,id2,dir,pos,subst) in
+ let t = Subst.apply_subst subst t in
+ if filter t then
+ let literal =
+ match t with
+ | Terms.Node [ Terms.Leaf eq ; ty; l; r ] when B.eq B.eqP eq ->
+ let o = Order.compare_terms l r in
+ Terms.Equation (l, r, ty, o)
+ | t -> Terms.Predicate t
+ in
+ let bag, uc =
+ Utils.add_to_bag bag (0, literal, vl, proof)
+ in
+ Some (bag, maxvar, uc)
+ else
+ None
+ ;;
+
+ let fold_build_new_clause bag maxvar id filter res =
+ let maxvar, bag, new_clauses =
+ List.fold_left
+ (fun (maxvar, bag, acc) (t,subst,vl,id2,pos,dir) ->
+ match build_new_clause bag maxvar filter t subst vl id id2 pos dir
+ with Some (bag, maxvar, uc) -> maxvar, bag, uc::acc
+ | None -> maxvar, bag, acc)
+ (maxvar, bag, []) res
+ in
+ bag, maxvar, new_clauses
+ ;;
+
+ let superposition_right_with_table bag maxvar (id,selected,vl,_) table =