match ty with
| Terms.Node [ Terms.Leaf eq ; ty; l; r ] when B.eq B.eqP eq ->
let o = Order.compare_terms l r in
- (vars,(Terms.Equation (l, r, ty, o),false)::literals)
- | _ -> (vars,(Terms.Predicate ty,false)::literals)
+ (vars,(Terms.Equation (l, r, ty, o),true)::literals)
+ | _ -> (vars,(Terms.Predicate ty,true)::literals)
in
let varlist = Terms.vars_of_term proofterm in
let (varlist,nlit) = List.fold_left foterm_to_lit (varlist,[]) nlit in