let pp_unit_clause ~formatter:f c =
let (id, l, vars, proof) = c in
- Format.fprintf f "Id : %d, " id ;
+ Format.fprintf f "Id : %3d, " id ;
match l with
| Terms.Predicate t ->
pp_foterm f t
| Terms.Equation (lhs, rhs, ty, comp) ->
- Format.fprintf f "{";
+ Format.fprintf f "@[<hv>{";
pp_foterm f ty;
- Format.fprintf f "}: ";
+ Format.fprintf f "}:@;@[<hv>";
pp_foterm f lhs;
- Format.fprintf f " %s " (string_of_comparison comp);
+ Format.fprintf f "@;%s@;" (string_of_comparison comp);
pp_foterm f rhs;
- Format.fprintf f " [%s] by %s"
+ Format.fprintf f "@]@;[%s] by %s@]"
(String.concat ", " (List.map string_of_int vars))
(match proof with
| Terms.Exact _ -> "axiom"