+ let vars_of_clause (id,nlit,plit,_,pr) =
+ let vars_of_lit acc lit =
+ match lit with
+ | (Terms.Predicate t,_) -> Terms.vars_of_term ~start_acc:acc t
+ | (Terms.Equation (l,r,ty,o),_) ->
+ Terms.vars_of_term ~start_acc:(Terms.vars_of_term ~start_acc:acc l) r
+ in
+ List.fold_left vars_of_lit [] (nlit@plit)
+;;
+