From 6da830ce7e095866ba36c1918a2e6db2139ef663 Mon Sep 17 00:00:00 2001
From: Michael Rawson <michael@rawsons.uk>
Date: Sat, 10 Oct 2026 15:33:33 +0100
Subject: [PATCH] improve Vampire's Prolog compliance: space after negation,
 parenthesise disjunctions where necessary

---
 Kernel/Formula.cpp        | 7 +++----
 Kernel/InferenceStore.cpp | 4 ++--
 Kernel/Term.cpp           | 7 ++++++-
 Shell/TPTPPrinter.cpp     | 5 +++--
 checks/sanity             | 4 ++--
 5 files changed, 16 insertions(+), 11 deletions(-)

diff --git a/Kernel/Formula.cpp b/Kernel/Formula.cpp
index c4a3b730c..f93d77db3 100644
--- a/Kernel/Formula.cpp
+++ b/Kernel/Formula.cpp
@@ -174,12 +174,11 @@ std::string Formula::toString (bool topLevel) const
 
     case NOT:
       {
-        res += toString(c);
+        // always separate with a space: "~$true", "~~p" or "~?[X] : p(X)" do not tokenise as intended,
+        // and "~(p & q)" is read by Prolog as functional notation, where the argument may not be an operator of high priority
+        res += toString(c) + " ";
 
         const Formula* arg = f->uarg();
-        Connective subc = arg->connective();
-        if(subc == FORALL || subc == EXISTS || subc == NOT || subc == LITERAL)
-          res += " ";
         stack.push({arg->parenthesesRequired(c),NOCONN,arg});
 
         continue;
diff --git a/Kernel/InferenceStore.cpp b/Kernel/InferenceStore.cpp
index ed89c116b..8998a24e5 100644
--- a/Kernel/InferenceStore.cpp
+++ b/Kernel/InferenceStore.cpp
@@ -741,7 +741,7 @@ std::string getSkolemizeMap(unsigned unitNumber, It symIt){
   }
 
   void printSATStep(SATClause *cl) override {
-    out << "cnf(s" << cl->number << ", plain, ";
+    out << "cnf(s" << cl->number << ", plain, (";
     if(cl->isEmpty())
       out << "$false";
     else {
@@ -754,7 +754,7 @@ std::string getSkolemizeMap(unsigned unitNumber, It symIt){
       }
     }
 
-    out << ", inference(";
+    out << "), inference(";
     auto inference = cl->inference();
     switch(inference->getType()) {
     case SAT::SATInference::PROP_INF: {
diff --git a/Kernel/Term.cpp b/Kernel/Term.cpp
index d1d589223..c46862d14 100644
--- a/Kernel/Term.cpp
+++ b/Kernel/Term.cpp
@@ -917,7 +917,12 @@ std::string Literal::toString(bool reverseEquality) const
     }
   }
 
-  s += predicateName();
+  const std::string& name = predicateName();
+  // "~$less(X,Y)" is not valid Prolog: "~$" would be read as a single token
+  if (polarity() == 0 && name[0] == '$') {
+    s += ' ';
+  }
+  s += name;
 
   //cerr << "predicate: "<< predicateName()<<endl;
   if (_arity > 0) {
diff --git a/Shell/TPTPPrinter.cpp b/Shell/TPTPPrinter.cpp
index 0d5bde1b0..ac09d70b8 100644
--- a/Shell/TPTPPrinter.cpp
+++ b/Shell/TPTPPrinter.cpp
@@ -71,7 +71,7 @@ void TPTPPrinter::printWithRole(std::string name, std::string role, Unit* u, boo
   std::string body = getBodyStr(u, includeSplitLevels);
 
   ensureHeadersPrinted(u);
-  tgt() << "tff(" << name << ", " << role << ", " << body << ")." << endl;
+  tgt() << "tff(" << name << ", " << role << ", (" << body << "))." << endl;
 }
 
 /**
@@ -328,7 +328,7 @@ std::string TPTPPrinter::toString(const Formula* formula)
 {
   static std::string names [] =
     { "", " & ", " | ", " => ", " <=> ", " <~> ",
-      "~", "!", "?", "$term", "$false", "$true", "", ""};
+      "~ ", "!", "?", "$term", "$false", "$true", "", ""};
   ASS_EQ(sizeof(names)/sizeof(std::string), NOCONN+1);
 
   std::string res;
@@ -542,6 +542,7 @@ std::string TPTPPrinter::toString (const Unit* unit, bool typedClauses)
       main = universalPrefix(unit) + "( " + main + " )";
     } else {
       prefix = "cnf";
+      main = "( " + main + " )";
     }
   }
   else {
diff --git a/checks/sanity b/checks/sanity
index 6bc2075c3..75834f92e 100755
--- a/checks/sanity
+++ b/checks/sanity
@@ -340,10 +340,10 @@ check_output_contains '(f @ (^[X0 : a] : (X0)) @ (^[X1 : b] : (X1)))' --mode out
 check_output_contains '(^[X0 : a] : ((g @ X0))) @ y' --mode output parse/thf-lambda-in-app-chain.p
 check_output_contains '(ev @ (^[X0 : a] : ((? [X1 : b] : (r @ X0 @ X1)))) @ q)' --mode output parse/thf-lambda-in-app-chain.p
 check_output_contains '(((((^[X0 : b] : (y)) @ w)) = y))' --mode output parse/thf-lambda-in-app-chain.p
-check_output_contains '(fl @ (^[X0 : a] : ((~(r @ X0 @ w)))) @ q)' --mode output parse/thf-lambda-in-app-chain.p
+check_output_contains '(fl @ (^[X0 : a] : ((~ (r @ X0 @ w)))) @ q)' --mode output parse/thf-lambda-in-app-chain.p
 check_rejected 'sort mismatch in the application x @ y' --input_syntax tptp --mode output parse/thf-ill-typed-app.p
 check_rejected 'sort mismatch in the application r | q @ x' --input_syntax tptp --mode output parse/thf-app-to-formula.p
-check_output_contains '(~((p = q)))' --mode output parse/thf-not-eq.p
+check_output_contains '(~ ((p = q)))' --mode output parse/thf-not-eq.p
 check_output_contains_once "'~' applied to an unparenthesized (in)equality" --mode output parse/thf-non-conformity-warnings.p
 check_output_contains_once 'an unparenthesized application as a connective argument' --mode output parse/thf-non-conformity-warnings.p
 check_output_contains_once 'as an unparenthesized equality argument' --mode output parse/thf-non-conformity-warnings.p