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

        (* have to treat '=' special *)
        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"