tuned Sledgehammer's TPTP generation

Some provers, such as E 3.1 and 3.2, fail to parse != without parentheses.

--- a/src/HOL/Tools/ATP/atp_problem.ML	Mon Feb 10 10:52:55 2025 +0100
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Wed Feb 12 08:47:44 2025 +0100
@@ -569,12 +569,10 @@
     |> parens
   | tptp_string_of_formula format
         (AConn (ANot, [AAtom (ATerm (("=" (* tptp_equal *), []), ts))])) =
-    space_implode (" " ^ tptp_not_equal ^ " ") (map (tptp_string_of_term format) ts)
-    |> is_format_higher_order format ? parens
+    parens (space_implode (" " ^ tptp_not_equal ^ " ") (map (tptp_string_of_term format) ts))
   | tptp_string_of_formula format
         (AConn (ANot, [AAtom (ATerm (("equal" (* tptp_old_equal *), []), ts))])) =
-    space_implode (" " ^ tptp_not_equal ^ " ") (map (tptp_string_of_term format) ts)
-    |> is_format_higher_order format ? parens
+    parens (space_implode (" " ^ tptp_not_equal ^ " ") (map (tptp_string_of_term format) ts))
   | tptp_string_of_formula format (AConn (c, [phi])) =
     tptp_string_of_connective c ^ " " ^ (tptp_string_of_formula format phi |> parens)
     |> parens