let tptp_clause_to_tptp_string (label: string) (clause: clause) : string =
let clause =
List.map
(fun literal ->
let sign =
if literal.sign then
" "
else
"~ "
in
let term =
tptp_replace_internal_symbols (tptp_replace_domain_elements (tptp_replace_vars literal.atom))
in
let term_repr =
match term with
| Func func when Symbol.equal Symbol.equality func.symbol ->
term_to_string ~pretty:false func.subterms.(0)
^ " = "
^ term_to_string ~pretty:false func.subterms.(1)
| _ ->
term_to_string ~pretty:false term
in
sign ^ term_repr ^ "\n"
)
clause;
in
"cnf(" ^ label ^ ",axiom,(\n"
^ " " ^ String.concat " | " clause
^ ")).\n"