- | Terms.Equation (l,r,_,Terms.Lt) ->
- let _r's = all_positions r (superposition_right table) in
+ | Terms.Equation (l,r,ty,Terms.Lt) ->
+ let res = all_positions r (superposition_right table vl) in
+ let _new_clauses =
+ List.map
+ (fun (r,subst,vl,id2,pos,dir) ->
+ let proof =
+ Terms.Step(Terms.SuperpositionRight,id,id2, dir, pos, subst)
+ in
+ let r = Subst.apply_subst subst r in
+ let l = Subst.apply_subst subst l in
+ let ty = Subst.apply_subst subst ty in
+ (0, Terms.Equation (l,r,ty,Terms.Incomparable), vl, proof))
+ res
+ in
+ (* fresh ID and metas and compute orientataion of new_clauses *)