Support for TPTP's TFF0 (with arithmetic)

This commit reverses an "SZS ontology compliance hack" that was done for CASC-24 this year, and adds a TPTP pretty-printer which is capable of outputting results in the TPTP way (rather than the SMT way). This commit includes minor changes to the Expr package to add obvious missing functionality, and to fix the way expressions with builtin operators are made. These changes are truly a _fix_, the implementation had not been properly aligned with the design vision for some corner cases.
author: Morgan Deters <mdeters@cs.nyu.edu> 2013-06-24 19:58:37 -0400
committer: Morgan Deters <mdeters@cs.nyu.edu> 2013-07-11 17:15:59 -0400
commit: e80b93ca958bdbeb28959029868f6193b39a3f19 (patch)
tree: 92218adf47348cb8011a41599e158b371f5659de
parent: b76afedab3a23525da478ba4a8687c882793ea81 (diff)
79 files changed, 3577 insertions, 364 deletions
diff --git a/NEWS b/NEWS
index bd54ae81a..bd7347a75 100644
--- a/NEWS
+++ b/NEWS
@@ -4,7 +4,10 @@ Changes since 1.2
 =================
 
 * SMT-LIB support for abs, to_real, to_int, is_int
+* Expr::substitute() now capable of substituting operators (e.g.,
+  function symbols under an APPLY_UF)
 * Support in linear logics for /, div, and mod by constants.
+* Support for TPTP's TFF and TFA formats.
 * We no longer permit model or proof generation if there's been an
   intervening push/pop.
 * Increased compliance to SMT-LIBv2, numerous bugs and usability issues
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 524bc2095..3a2feb624 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -304,8 +304,8 @@ Expr ExprManager::mkExpr(Kind kind, Expr child1, const std::vector<Expr>& otherC
 
 Expr ExprManager::mkExpr(Expr opExpr) {
   const unsigned n = 0;
-  Kind kind = kind::operatorKindToKind(opExpr.getKind());
-  CheckArgument(kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
+  Kind kind = NodeManager::operatorToKind(opExpr.getNode());
+  CheckArgument(opExpr.getKind() == kind::BUILTIN || kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
                 "This Expr constructor is for parameterized kinds only");
   CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
                 "Exprs with kind %s must have at least %u children and "
@@ -323,8 +323,8 @@ Expr ExprManager::mkExpr(Expr opExpr) {
 
 Expr ExprManager::mkExpr(Expr opExpr, Expr child1) {
   const unsigned n = 1;
-  Kind kind = kind::operatorKindToKind(opExpr.getKind());
-  CheckArgument(kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
+  Kind kind = NodeManager::operatorToKind(opExpr.getNode());
+  CheckArgument(opExpr.getKind() == kind::BUILTIN || kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
                 "This Expr constructor is for parameterized kinds only");
   CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
                 "Exprs with kind %s must have at least %u children and "
@@ -342,8 +342,8 @@ Expr ExprManager::mkExpr(Expr opExpr, Expr child1) {
 
 Expr ExprManager::mkExpr(Expr opExpr, Expr child1, Expr child2) {
   const unsigned n = 2;
-  Kind kind = kind::operatorKindToKind(opExpr.getKind());
-  CheckArgument(kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
+  Kind kind = NodeManager::operatorToKind(opExpr.getNode());
+  CheckArgument(opExpr.getKind() == kind::BUILTIN || kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
                 "This Expr constructor is for parameterized kinds only");
   CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
                 "Exprs with kind %s must have at least %u children and "
@@ -363,8 +363,8 @@ Expr ExprManager::mkExpr(Expr opExpr, Expr child1, Expr child2) {
 
 Expr ExprManager::mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3) {
   const unsigned n = 3;
-  Kind kind = kind::operatorKindToKind(opExpr.getKind());
-  CheckArgument(kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
+  Kind kind = NodeManager::operatorToKind(opExpr.getNode());
+  CheckArgument(opExpr.getKind() == kind::BUILTIN || kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
                 "This Expr constructor is for parameterized kinds only");
   CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
                 "Exprs with kind %s must have at least %u children and "
@@ -386,8 +386,8 @@ Expr ExprManager::mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3) {
 Expr ExprManager::mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3,
                          Expr child4) {
   const unsigned n = 4;
-  Kind kind = kind::operatorKindToKind(opExpr.getKind());
-  CheckArgument(kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
+  Kind kind = NodeManager::operatorToKind(opExpr.getNode());
+  CheckArgument(opExpr.getKind() == kind::BUILTIN || kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
                 "This Expr constructor is for parameterized kinds only");
   CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
                 "Exprs with kind %s must have at least %u children and "
@@ -410,8 +410,8 @@ Expr ExprManager::mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3,
 Expr ExprManager::mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3,
                          Expr child4, Expr child5) {
   const unsigned n = 5;
-  Kind kind = kind::operatorKindToKind(opExpr.getKind());
-  CheckArgument(kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
+  Kind kind = NodeManager::operatorToKind(opExpr.getNode());
+  CheckArgument(opExpr.getKind() == kind::BUILTIN || kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
                 "This Expr constructor is for parameterized kinds only");
   CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
                 "Exprs with kind %s must have at least %u children and "
@@ -434,8 +434,8 @@ Expr ExprManager::mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3,
 
 Expr ExprManager::mkExpr(Expr opExpr, const std::vector<Expr>& children) {
   const unsigned n = children.size();
-  Kind kind = kind::operatorKindToKind(opExpr.getKind());
-  CheckArgument(kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
+  Kind kind = NodeManager::operatorToKind(opExpr.getNode());
+  CheckArgument(opExpr.getKind() == kind::BUILTIN || kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
                 "This Expr constructor is for parameterized kinds only");
   CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
                 "Exprs with kind %s must have at least %u children and "
diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h
index 22d7baac3..8486e8ec3 100644
--- a/src/expr/metakind_template.h
+++ b/src/expr/metakind_template.h
@@ -126,18 +126,6 @@ ${metakind_kinds}
   return metaKinds[k + 1];
 }/* metaKindOf(k) */
 
-/**
- * Map a kind of the operator to the kind of the enclosing expression. For
- * example, since the kind of functions is just VARIABLE, it should map
- * VARIABLE to APPLY_UF.
- */
-static inline Kind operatorKindToKind(Kind k) {
-  switch (k) {
-${metakind_operatorKinds}
-  default:
-    return kind::UNDEFINED_KIND;  /* LAST_KIND */
-  };
-}
 }/* CVC4::kind namespace */
 
 namespace expr {
@@ -324,9 +312,29 @@ ${metakind_ubchildren}
 }
 
 }/* CVC4::kind::metakind namespace */
+
+/**
+ * Map a kind of the operator to the kind of the enclosing expression. For
+ * example, since the kind of functions is just VARIABLE, it should map
+ * VARIABLE to APPLY_UF.
+ */
+static inline Kind operatorToKind(::CVC4::expr::NodeValue* nv) {
+  if(nv->getKind() == kind::BUILTIN) {
+    return nv->getConst<Kind>();
+  } else if(nv->getKind() == kind::LAMBDA) {
+    return kind::APPLY_UF;
+  }
+
+  switch(Kind k CVC4_UNUSED = nv->getKind()) {
+${metakind_operatorKinds}
+  default:
+    return kind::UNDEFINED_KIND;  /* LAST_KIND */
+  };
+}
+
 }/* CVC4::kind namespace */
 
-#line 330 "${template}"
+#line 338 "${template}"
 
 namespace theory {
 
diff --git a/src/expr/node.h b/src/expr/node.h
index d9e88d8af..99e1e7ee7 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -1337,7 +1337,11 @@ NodeTemplate<ref_count>::substitute(TNode node, TNode replacement,
   NodeBuilder<> nb(getKind());
   if(getMetaKind() == kind::metakind::PARAMETERIZED) {
     // push the operator
-    nb << getOperator();
+    if(getOperator() == node) {
+      nb << replacement;
+    } else {
+      nb << getOperator().substitute(node, replacement, cache);
+    }
   }
   for(const_iterator i = begin(),
         iend = end();
diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h
index 1f098b4e8..64080c275 100644
--- a/src/expr/node_builder.h
+++ b/src/expr/node_builder.h
@@ -660,6 +660,9 @@ public:
     Assert(!isUsed(), "NodeBuilder is one-shot only; "
            "attempt to access it after conversion");
     Assert(!n.isNull(), "Cannot use NULL Node as a child of a Node");
+    if(n.getKind() == kind::BUILTIN) {
+      return *this << NodeManager::operatorToKind(n);
+    }
     allocateNvIfNecessaryForAppend();
     expr::NodeValue* nv = n.d_nv;
     nv->inc();
@@ -980,7 +983,7 @@ expr::NodeValue* NodeBuilder<nchild_thresh>::constructNV() {
 #if 0
   // if the kind is PARAMETERIZED, check that the operator is correctly-kinded
   Assert(kind::metaKindOf(getKind()) != kind::metakind::PARAMETERIZED ||
-         kind::operatorKindToKind(getOperator().getKind()) == getKind(),
+         NodeManager::operatorToKind(getOperator()) == getKind(),
          "Attempted to construct a parameterized kind `%s' with "
          "incorrectly-kinded operator `%s'",
          kind::kindToString(getKind()).c_str(),
@@ -1165,7 +1168,7 @@ expr::NodeValue* NodeBuilder<nchild_thresh>::constructNV() const {
 #if 0
   // if the kind is PARAMETERIZED, check that the operator is correctly-kinded
   Assert(kind::metaKindOf(getKind()) != kind::metakind::PARAMETERIZED ||
-         kind::operatorKindToKind(getOperator().getKind()) == getKind(),
+         NodeManager::operatorToKind(getOperator()) == getKind(),
          "Attempted to construct a parameterized kind `%s' with "
          "incorrectly-kinded operator `%s'",
          kind::kindToString(getKind()).c_str(),
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 0c62d31c5..913b8befb 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -353,6 +353,9 @@ public:
     d_listeners.erase(elt);
   }
 
+  /** Get a Kind from an operator expression */
+  static inline Kind operatorToKind(TNode n);
+
   // general expression-builders
 
   /** Create a node with one child. */
@@ -1280,6 +1283,10 @@ inline TypeNode NodeManager::mkSortConstructor(const std::string& name,
   return type;
 }
 
+inline Kind NodeManager::operatorToKind(TNode n) {
+  return kind::operatorToKind(n.d_nv);
+}
+
 inline Node NodeManager::mkNode(Kind kind, TNode child1) {
   NodeBuilder<1> nb(this, kind);
   nb << child1;
@@ -1367,80 +1374,114 @@ inline Node* NodeManager::mkNodePtr(Kind kind,
 
 // for operators
 inline Node NodeManager::mkNode(TNode opNode) {
-  NodeBuilder<1> nb(this, kind::operatorKindToKind(opNode.getKind()));
-  nb << opNode;
+  NodeBuilder<1> nb(this, operatorToKind(opNode));
+  if(opNode.getKind() != kind::BUILTIN) {
+    nb << opNode;
+  }
   return nb.constructNode();
 }
 
 inline Node* NodeManager::mkNodePtr(TNode opNode) {
-  NodeBuilder<1> nb(this, kind::operatorKindToKind(opNode.getKind()));
-  nb << opNode;
+  NodeBuilder<1> nb(this, operatorToKind(opNode));
+  if(opNode.getKind() != kind::BUILTIN) {
+    nb << opNode;
+  }
   return nb.constructNodePtr();
 }
 
 inline Node NodeManager::mkNode(TNode opNode, TNode child1) {
-  NodeBuilder<2> nb(this, kind::operatorKindToKind(opNode.getKind()));
-  nb << opNode << child1;
+  NodeBuilder<2> nb(this, operatorToKind(opNode));
+  if(opNode.getKind() != kind::BUILTIN) {
+    nb << opNode;
+  }
+  nb << child1;
   return nb.constructNode();
 }
 
 inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1) {
-  NodeBuilder<2> nb(this, kind::operatorKindToKind(opNode.getKind()));
-  nb << opNode << child1;
+  NodeBuilder<2> nb(this, operatorToKind(opNode));
+  if(opNode.getKind() != kind::BUILTIN) {
+    nb << opNode;
+  }
+  nb << child1;
   return nb.constructNodePtr();
 }
 
 inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2) {
-  NodeBuilder<3> nb(this, kind::operatorKindToKind(opNode.getKind()));
-  nb << opNode << child1 << child2;
+  NodeBuilder<3> nb(this, operatorToKind(opNode));
+  if(opNode.getKind() != kind::BUILTIN) {
+    nb << opNode;
+  }
+  nb << child1 << child2;
   return nb.constructNode();
 }
 
 inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1, TNode child2) {
-  NodeBuilder<3> nb(this, kind::operatorKindToKind(opNode.getKind()));
-  nb << opNode << child1 << child2;
+  NodeBuilder<3> nb(this, operatorToKind(opNode));
+  if(opNode.getKind() != kind::BUILTIN) {
+    nb << opNode;
+  }
+  nb << child1 << child2;
   return nb.constructNodePtr();
 }
 
 inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2,
                                 TNode child3) {
-  NodeBuilder<4> nb(this, kind::operatorKindToKind(opNode.getKind()));
-  nb << opNode << child1 << child2 << child3;
+  NodeBuilder<4> nb(this, operatorToKind(opNode));
+  if(opNode.getKind() != kind::BUILTIN) {
+    nb << opNode;
+  }
+  nb << child1 << child2 << child3;
   return nb.constructNode();
 }
 
 inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1, TNode child2,
                                 TNode child3) {
-  NodeBuilder<4> nb(this, kind::operatorKindToKind(opNode.getKind()));
-  nb << opNode << child1 << child2 << child3;
+  NodeBuilder<4> nb(this, operatorToKind(opNode));
+  if(opNode.getKind() != kind::BUILTIN) {
+    nb << opNode;
+  }
+  nb << child1 << child2 << child3;
   return nb.constructNodePtr();
 }
 
 inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2,
                                 TNode child3, TNode child4) {
-  NodeBuilder<5> nb(this, kind::operatorKindToKind(opNode.getKind()));
-  nb << opNode << child1 << child2 << child3 << child4;
+  NodeBuilder<5> nb(this, operatorToKind(opNode));
+  if(opNode.getKind() != kind::BUILTIN) {
+    nb << opNode;
+  }
+  nb << child1 << child2 << child3 << child4;
   return nb.constructNode();
 }
 
 inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1, TNode child2,
                                 TNode child3, TNode child4) {
-  NodeBuilder<5> nb(this, kind::operatorKindToKind(opNode.getKind()));
-  nb << opNode << child1 << child2 << child3 << child4;
+  NodeBuilder<5> nb(this, operatorToKind(opNode));
+  if(opNode.getKind() != kind::BUILTIN) {
+    nb << opNode;
+  }
+  nb << child1 << child2 << child3 << child4;
   return nb.constructNodePtr();
 }
 
 inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2,
                                 TNode child3, TNode child4, TNode child5) {
-  NodeBuilder<6> nb(this, kind::operatorKindToKind(opNode.getKind()));
-  nb << opNode << child1 << child2 << child3 << child4 << child5;
+  NodeBuilder<6> nb(this, operatorToKind(opNode));
+  if(opNode.getKind() != kind::BUILTIN) {
+    nb << opNode;
+  }
+  nb << child1 << child2 << child3 << child4 << child5;
   return nb.constructNode();
 }
 
 inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1, TNode child2,
                                     TNode child3, TNode child4, TNode child5) {
-  NodeBuilder<6> nb(this, kind::operatorKindToKind(opNode.getKind()));
-  nb << opNode << child1 << child2 << child3 << child4 << child5;
+  NodeBuilder<6> nb(this, operatorToKind(opNode));
+  if(opNode.getKind() != kind::BUILTIN) {
+    nb << opNode;
+  }
+  nb << child1 << child2 << child3 << child4 << child5;
   return nb.constructNodePtr();
 }
 
@@ -1449,8 +1490,10 @@ template <bool ref_count>
 inline Node NodeManager::mkNode(TNode opNode,
                                 const std::vector<NodeTemplate<ref_count> >&
                                 children) {
-  NodeBuilder<> nb(this, kind::operatorKindToKind(opNode.getKind()));
-  nb << opNode;
+  NodeBuilder<> nb(this, operatorToKind(opNode));
+  if(opNode.getKind() != kind::BUILTIN) {
+    nb << opNode;
+  }
   nb.append(children);
   return nb.constructNode();
 }
@@ -1459,8 +1502,10 @@ template <bool ref_count>
 inline Node* NodeManager::mkNodePtr(TNode opNode,
                                     const std::vector<NodeTemplate<ref_count> >&
                                     children) {
-  NodeBuilder<> nb(this, kind::operatorKindToKind(opNode.getKind()));
-  nb << opNode;
+  NodeBuilder<> nb(this, operatorToKind(opNode));
+  if(opNode.getKind() != kind::BUILTIN) {
+    nb << opNode;
+  }
   nb.append(children);
   return nb.constructNodePtr();
 }
diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index 71c25bd50..f3cf992ba 100644
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -317,6 +317,10 @@ bool Type::isSubrange() const {
   return d_typeNode->isSubrange();
 }
 
+size_t FunctionType::getArity() const {
+  return d_typeNode->getNumChildren() - 1;
+}
+
 vector<Type> FunctionType::getArgTypes() const {
   NodeManagerScope nms(d_nodeManager);
   vector<Type> args;
diff --git a/src/expr/type.h b/src/expr/type.h
index 5e4e86264..3c772d461 100644
--- a/src/expr/type.h
+++ b/src/expr/type.h
@@ -415,6 +415,9 @@ public:
   /** Construct from the base type */
   FunctionType(const Type& type = Type()) throw(IllegalArgumentException);
 
+  /** Get the arity of the function type */
+  size_t getArity() const;
+
   /** Get the argument types */
   std::vector<Type> getArgTypes() const;
 
diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index 556e51216..9ee896107 100644
--- a/src/main/command_executor.cpp
+++ b/src/main/command_executor.cpp
@@ -24,11 +24,12 @@
 namespace CVC4 {
 namespace main {
 
-CommandExecutor::CommandExecutor(ExprManager &exprMgr, Options &options):
+CommandExecutor::CommandExecutor(ExprManager &exprMgr, Options &options) :
   d_exprMgr(exprMgr),
   d_smtEngine(SmtEngine(&exprMgr)),
   d_options(options),
-  d_stats("driver") {
+  d_stats("driver"),
+  d_result() {
 }
 
 bool CommandExecutor::doCommand(Command* cmd)
@@ -58,7 +59,7 @@ bool CommandExecutor::doCommand(Command* cmd)
   }
 }
 
-bool CommandExecutor::doCommandSingleton(Command *cmd)
+bool CommandExecutor::doCommandSingleton(Command* cmd)
 {
   bool status = true;
   if(d_options[options::verbosity] >= -1) {
@@ -66,25 +67,27 @@ bool CommandExecutor::doCommandSingleton(Command *cmd)
   } else {
     status = smtEngineInvoke(&d_smtEngine, cmd, NULL);
   }
-  //dump the model if option is set
-  if(status && d_options[options::produceModels] && d_options[options::dumpModels]) {
-    CheckSatCommand *cs = dynamic_cast<CheckSatCommand*>(cmd);
-    if(cs != NULL) {
-      if(cs->getResult().asSatisfiabilityResult().isSat() == Result::SAT ||
-         (cs->getResult().isUnknown() && cs->getResult().whyUnknown() == Result::INCOMPLETE) ){
-        Command * gm = new GetModelCommand;
-        status = doCommandSingleton(gm);
-      }
-    }
+  Result res;
+  CheckSatCommand* cs = dynamic_cast<CheckSatCommand*>(cmd);
+  if(cs != NULL) {
+    d_result = res = cs->getResult();
+  }
+  QueryCommand* q = dynamic_cast<QueryCommand*>(cmd);
+  if(q != NULL) {
+    d_result = res = q->getResult();
+  }
+  // dump the model if option is set
+  if( status &&
+      d_options[options::produceModels] &&
+      d_options[options::dumpModels] &&
+      ( res.asSatisfiabilityResult() == Result::SAT ||
+        (res.isUnknown() && res.whyUnknown() == Result::INCOMPLETE) ) ) {
+    Command* gm = new GetModelCommand();
+    status = doCommandSingleton(gm);
   }
   return status;
 }
 
-std::string CommandExecutor::getSmtEngineStatus()
-{
-  return d_smtEngine.getInfo("status").getValue();
-}
-
 bool smtEngineInvoke(SmtEngine* smt, Command* cmd, std::ostream *out)
 {
   if(out == NULL) {
diff --git a/src/main/command_executor.h b/src/main/command_executor.h
index f1b8d8f2f..cbc71b075 100644
--- a/src/main/command_executor.h
+++ b/src/main/command_executor.h
@@ -34,6 +34,7 @@ protected:
   SmtEngine d_smtEngine;
   Options& d_options;
   StatisticsRegistry d_stats;
+  Result d_result;
 
 public:
   CommandExecutor(ExprManager &exprMgr, Options &options);
@@ -47,7 +48,7 @@ public:
    */
   bool doCommand(CVC4::Command* cmd);
 
-  virtual std::string getSmtEngineStatus();
+  Result getResult() const { return d_result; }
 
   StatisticsRegistry& getStatisticsRegistry() {
     return d_stats;
diff --git a/src/main/command_executor_portfolio.cpp b/src/main/command_executor_portfolio.cpp
index 63f689d48..2dfd5e6bd 100644
--- a/src/main/command_executor_portfolio.cpp
+++ b/src/main/command_executor_portfolio.cpp
@@ -184,7 +184,7 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd)
   // command
 
   if(dynamic_cast<CheckSatCommand*>(cmd) != NULL ||
-    dynamic_cast<QueryCommand*>(cmd) != NULL) {
+     dynamic_cast<QueryCommand*>(cmd) != NULL) {
     mode = 1;
   } else if(dynamic_cast<GetValueCommand*>(cmd) != NULL ||
             dynamic_cast<GetAssignmentCommand*>(cmd) != NULL ||
@@ -298,6 +298,16 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd)
 
     d_lastWinner = portfolioReturn.first;
 
+    CheckSatCommand* cs = dynamic_cast<CheckSatCommand*>(cmd);
+    if(cs != NULL) {
+      d_result = cs->getResult();
+    }
+    QueryCommand* q = dynamic_cast<QueryCommand*>(cmd);
+    if(q != NULL) {
+      d_result = q->getResult();
+    }
+    dynamic_cast<QueryCommand*>(cmd) != NULL) {
+
     if(d_ostringstreams.size() != 0) {
       assert(d_numThreads == d_options[options::threads]);
       assert(portfolioReturn.first >= 0);
@@ -340,11 +350,6 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd)
 
 }/* CommandExecutorPortfolio::doCommandSingleton() */
 
-std::string CommandExecutorPortfolio::getSmtEngineStatus()
-{
-  return d_smts[d_lastWinner]->getInfo("status").getValue();
-}
-
 void CommandExecutorPortfolio::flushStatistics(std::ostream& out) const {
   assert(d_numThreads == d_exprMgrs.size() && d_exprMgrs.size() == d_smts.size());
   for(size_t i = 0; i < d_numThreads; ++i) {
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index f57d4f2d7..20a989106 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -297,13 +297,13 @@ int runCvc4(int argc, char* argv[], Options& opts) {
       opts.set(options::replayStream, NULL);
     }
 
-    string result = "unknown";
+    Result result;
     if(status) {
-      result = pExecutor->getSmtEngineStatus();
+      result = pExecutor->getResult();
 
-      if(result == "sat") {
+      if(result.asSatisfiabilityResult() == Result::SAT) {
         returnValue = 10;
-      } else if(result == "unsat") {
+      } else if(result.asSatisfiabilityResult() == Result::UNSAT) {
         returnValue = 20;
       } else {
         returnValue = 0;
diff --git a/src/parser/options b/src/parser/options
index e16f963f4..f277b231d 100644
--- a/src/parser/options
+++ b/src/parser/options
@@ -14,9 +14,6 @@ option memoryMap --mmap bool
 option semanticChecks /--no-checking bool :default DO_SEMANTIC_CHECKS_BY_DEFAULT :link /--no-type-checking
  disable ALL semantic checks, including type checks
 
-option szsCompliant --szs-compliant bool :default false
- temporary support for szs ontolotogy, print if conjecture is found
-
 # this is just to support security in the online version
 # (--no-include-file disables filesystem access in TPTP and SMT2 parsers)
 undocumented-option canIncludeFile /--no-include-file bool :default true
diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp
index 684a495b6..cb8c0d4f6 100644
--- a/src/parser/parser_builder.cpp
+++ b/src/parser/parser_builder.cpp
@@ -90,11 +90,7 @@ Parser* ParserBuilder::build()
     parser = new Smt2(d_exprManager, input, d_strictMode, d_parseOnly);
     break;
   case language::input::LANG_TPTP:
-  {
-    Tptp * tparser = new Tptp(d_exprManager, input, d_strictMode, d_parseOnly);
-    tparser->d_szsCompliant = d_szsCompliant;
-    parser = tparser;
-  }
+    parser = new Tptp(d_exprManager, input, d_strictMode, d_parseOnly);
     break;
   default:
     parser = new Parser(d_exprManager, input, d_strictMode, d_parseOnly);
@@ -152,7 +148,6 @@ ParserBuilder& ParserBuilder::withParseOnly(bool flag) {
 }
 
 ParserBuilder& ParserBuilder::withOptions(const Options& options) {
-  d_szsCompliant = options[options::szsCompliant];
   return
     withInputLanguage(options[options::inputLanguage])
       .withMmap(options[options::memoryMap])
diff --git a/src/parser/parser_builder.h b/src/parser/parser_builder.h
index 9779bf37b..b6e15b2ff 100644
--- a/src/parser/parser_builder.h
+++ b/src/parser/parser_builder.h
@@ -80,9 +80,6 @@ class CVC4_PUBLIC ParserBuilder {
   /** Are we parsing only? */
   bool d_parseOnly;
 
-  /** hack for szs compliance */
-  bool d_szsCompliant;
-
   /** Initialize this parser builder */
   void init(ExprManager* exprManager, const std::string& filename);
 
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 16b5bc4ea..c048feea7 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -786,7 +786,7 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
                    kind == CVC4::kind::LEQ || kind == CVC4::kind::GEQ ) &&
                  args.size() > 2 ) {
         /* "chainable", but CVC4 internally only supports 2 args */
-        expr = MK_EXPR(CVC4::kind::CHAIN, MK_CONST(kind), args);
+        expr = MK_EXPR(MK_CONST(Chain(kind)), args);
       } else if( PARSER_STATE->strictModeEnabled() && kind == CVC4::kind::ABS &&
                  args.size() == 1 && !args[0].getType().isInteger() ) {
         /* first, check that ABS is even defined in this logic */
diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g
index 9e814b358..beeca818e 100644
--- a/src/parser/tptp/Tptp.g
+++ b/src/parser/tptp/Tptp.g
@@ -27,7 +27,7 @@ options {
   // Only lookahead of <= k requested (disable for LL* parsing)
   // Note that CVC4's BoundedTokenBuffer requires a fixed k !
   // If you change this k, change it also in tptp_input.cpp !
-  k = 1;
+  k = 2;
 }/* options */
 
 @header {
@@ -102,6 +102,8 @@ using namespace CVC4::parser;
 #include "util/output.h"
 #include "util/rational.h"
 #include <vector>
+#include <iterator>
+#include <algorithm>
 
 using namespace CVC4;
 using namespace CVC4::parser;
@@ -114,12 +116,12 @@ using namespace CVC4::parser;
 #define EXPR_MANAGER PARSER_STATE->getExprManager()
 #undef MK_EXPR
 #define MK_EXPR EXPR_MANAGER->mkExpr
+#undef MK_EXPR_ASSOCIATIVE
+#define MK_EXPR_ASSOCIATIVE EXPR_MANAGER->mkAssociative
 #undef MK_CONST
 #define MK_CONST EXPR_MANAGER->mkConst
 #define UNSUPPORTED PARSER_STATE->unimplementedFeature
 
-
-
 }/* parser::postinclude */
 
 /**
@@ -139,46 +141,81 @@ parseCommand returns [CVC4::Command* cmd = NULL]
 @declarations {
   Expr expr;
   Tptp::FormulaRole fr;
-  std::string name;
-  std::string incl_args;
+  std::string name, inclSymbol;
 }
 //  : LPAREN_TOK c = command RPAREN_TOK { $cmd = c; }
   : CNF_TOK LPAREN_TOK nameN[name] COMMA_TOK formulaRole[fr] COMMA_TOK
-  { PARSER_STATE->cnf=true; PARSER_STATE->pushScope(); }
+  { PARSER_STATE->cnf = true; PARSER_STATE->fof = false; PARSER_STATE->pushScope(); }
     cnfFormula[expr]
   { PARSER_STATE->popScope();
     std::vector<Expr> bvl = PARSER_STATE->getFreeVar();
-    if(!bvl.empty()){
+    if(!bvl.empty()) {
       expr = MK_EXPR(kind::FORALL,MK_EXPR(kind::BOUND_VAR_LIST,bvl),expr);
     };
   }
     (COMMA_TOK anything*)? RPAREN_TOK DOT_TOK
     {
-      cmd = PARSER_STATE->makeCommand(fr,expr);
+      cmd = PARSER_STATE->makeCommand(fr, expr, /* cnf == */ true);
     }
   | FOF_TOK LPAREN_TOK nameN[name] COMMA_TOK formulaRole[fr] COMMA_TOK
-    { PARSER_STATE->cnf=false; }
+    { PARSER_STATE->cnf = false; PARSER_STATE->fof = true; }
     fofFormula[expr] (COMMA_TOK anything*)? RPAREN_TOK DOT_TOK
     {
-      cmd = PARSER_STATE->makeCommand(fr,expr);
+      cmd = PARSER_STATE->makeCommand(fr, expr, /* cnf == */ false);
     }
+  | TFF_TOK LPAREN_TOK nameN[name] COMMA_TOK
+    ( TYPE_TOK COMMA_TOK tffTypedAtom[cmd]
+    | formulaRole[fr] COMMA_TOK
+      { PARSER_STATE->cnf = false; PARSER_STATE->fof = false; }
+      tffFormula[expr] (COMMA_TOK anything*)?
+      {
+        cmd = PARSER_STATE->makeCommand(fr, expr, /* cnf == */ false);
+      }
+    ) RPAREN_TOK DOT_TOK
   | INCLUDE_TOK LPAREN_TOK unquotedFileName[name]
-    ( COMMA_TOK LBRACK_TOK nameN[incl_args] ( COMMA_TOK nameN[incl_args] )* RBRACK_TOK )?
+    ( COMMA_TOK LBRACK_TOK nameN[inclSymbol]
+      ( COMMA_TOK nameN[inclSymbol] )* RBRACK_TOK )?
     RPAREN_TOK DOT_TOK
-    {
-      PARSER_STATE->includeFile(name);
-      // The command of the included file will be produce at the new parseCommand call
+    { /* TODO - implement symbol filtering for file inclusion.
+       * the following removes duplicates and "all", just need to pass it
+       * through to includeFile() and implement it there.
+      std::sort(inclArgs.begin(), inclArgs.end());
+      std::vector<std::string>::iterator it =
+        std::unique(inclArgs.begin(), inclArgs.end());
+      inclArgs.resize(std::distance(inclArgs.begin(), it));
+      it = std::lower_bound(inclArgs.begin(), inclArgs.end(), std::string("all"));
+      if(it != inclArgs.end() && *it == "all") {
+        inclArgs.erase(it);
+      }
+      */
+      PARSER_STATE->includeFile(name /* , inclArgs */ );
+      // The command of the included file will be produced at the new parseCommand call
       cmd = new EmptyCommand("include::" + name);
     }
   | EOF
     {
-      PARSER_STATE->preemptCommand(new CheckSatCommand(MK_CONST(bool(true))));
+      std::string filename = PARSER_STATE->getInput()->getInputStreamName();
+      size_t i = filename.find_last_of('/');
+      if(i != std::string::npos) {
+        filename = filename.substr(i + 1);
+      }
+      if(filename.substr(filename.length() - 2) == ".p") {
+        filename = filename.substr(0, filename.length() - 2);
+      }
+      CommandSequence* seq = new CommandSequence();
+      seq->addCommand(new SetInfoCommand("name", filename));
+      if(PARSER_STATE->hasConjecture()) {
+        seq->addCommand(new QueryCommand(MK_CONST(bool(false))));
+      } else {
+        seq->addCommand(new CheckSatCommand());
+      }
+      PARSER_STATE->preemptCommand(seq);
       cmd = NULL;
     }
   ;
 
 /* Parse a formula Role */
-formulaRole[CVC4::parser::Tptp::FormulaRole & role]
+formulaRole[CVC4::parser::Tptp::FormulaRole& role]
   : LOWER_WORD
     {
       std::string r = AntlrInput::tokenText($LOWER_WORD);
@@ -204,33 +241,30 @@ formulaRole[CVC4::parser::Tptp::FormulaRole & role]
 /* CNF */
 
 /* It can parse a little more than the cnf grammar: false and true can appear.
-   Normally only false can appear and only at top level
-*/
+ * Normally only false can appear and only at top level. */
 
 cnfFormula[CVC4::Expr& expr]
-  :
-  LPAREN_TOK disjunction[expr] RPAREN_TOK
-| disjunction[expr]
+  : LPAREN_TOK cnfDisjunction[expr] RPAREN_TOK
+  | cnfDisjunction[expr]
 //| FALSE_TOK { expr = MK_CONST(bool(false)); }
 ;
 
-disjunction[CVC4::Expr& expr]
+cnfDisjunction[CVC4::Expr& expr]
 @declarations {
   std::vector<Expr> args;
 }
-  :
-    literal[expr] {args.push_back(expr); } ( OR_TOK literal[expr] {args.push_back(expr); } )*
-    {
-      if(args.size() > 1){
-        expr = MK_EXPR(kind::OR,args);
+  : cnfLiteral[expr] { args.push_back(expr); }
+    ( OR_TOK cnfLiteral[expr] { args.push_back(expr); } )*
+    { if(args.size() > 1) {
+        expr = MK_EXPR_ASSOCIATIVE(kind::OR, args);
       } // else its already in the expr
     }
 ;
 
-literal[CVC4::Expr& expr]
+cnfLiteral[CVC4::Expr& expr]
   : atomicFormula[expr]
-  | NOT_TOK atomicFormula[expr] { expr = MK_EXPR(kind::NOT,expr); }
-//  | folInfixUnary[expr]
+  | NOT_TOK atomicFormula[expr] { expr = MK_EXPR(kind::NOT, expr); }
+//| folInfixUnary[expr]
   ;
 
 atomicFormula[CVC4::Expr& expr]
@@ -241,28 +275,32 @@ atomicFormula[CVC4::Expr& expr]
   bool equal;
 }
   : atomicWord[name] (LPAREN_TOK arguments[args] RPAREN_TOK)?
-    ( ( equalOp[equal] //equality/disequality between terms
-       {
-         PARSER_STATE->makeApplication(expr,name,args,true);
-       }
-       term[expr2]
-       {
-         expr = MK_EXPR(kind::EQUAL, expr, expr2);
-         if(!equal) expr = MK_EXPR(kind::NOT,expr);
-       }
-      )
-    | //predicate
-      {
-        PARSER_STATE->makeApplication(expr,name,args,false);
+    ( equalOp[equal] term[expr2]
+      { // equality/disequality between terms
+        PARSER_STATE->makeApplication(expr, name, args, true);
+        expr = MK_EXPR(kind::EQUAL, expr, expr2);
+        if(!equal) expr = MK_EXPR(kind::NOT, expr);
       }
-  )
-  | simpleTerm[expr] equalOp[equal] term[expr2]
-    {
+    | { // predicate
+        PARSER_STATE->makeApplication(expr, name, args, false);
+      }
+    )
+  | definedFun[expr] LPAREN_TOK arguments[args] RPAREN_TOK
+    equalOp[equal] term[expr2]
+    { expr = EXPR_MANAGER->mkExpr(expr, args);
+      expr = MK_EXPR(kind::EQUAL, expr, expr2);
+      if(!equal) expr = MK_EXPR(kind::NOT, expr);
+    }
+  | (simpleTerm[expr] | letTerm[expr] | conditionalTerm[expr])
+    equalOp[equal] term[expr2]
+    { // equality/disequality between terms
       expr = MK_EXPR(kind::EQUAL, expr, expr2);
-      if(!equal) expr = MK_EXPR(kind::NOT,expr);
+      if(!equal) expr = MK_EXPR(kind::NOT, expr);
     }
+  | definedPred[expr] LPAREN_TOK arguments[args] RPAREN_TOK
+    { expr = EXPR_MANAGER->mkExpr(expr, args); }
   | definedProp[expr]
-;
+  ;
 //%----Using <plain_term> removes a reduce/reduce ambiguity in lex/yacc.
 //%----Note: "defined" means a word starting with one $ and "system" means $$.
 
@@ -270,35 +308,170 @@ definedProp[CVC4::Expr& expr]
   : TRUE_TOK { expr = MK_CONST(bool(true)); }
   | FALSE_TOK  { expr = MK_CONST(bool(false)); }
   ;
+
+definedPred[CVC4::Expr& expr]
+  : '$less' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::LT); }
+  | '$lesseq' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::LEQ); }
+  | '$greater' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::GT); }
+  | '$greatereq' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::GEQ); }
+  | '$is_rat' // all "real" are actually "rat" in CVC4
+    { Expr n = EXPR_MANAGER->mkBoundVar("N", EXPR_MANAGER->realType());
+      n = MK_EXPR(CVC4::kind::BOUND_VAR_LIST, n);
+      expr = MK_EXPR(CVC4::kind::LAMBDA, n, MK_CONST(bool(true)));
+    }
+  | '$is_int' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::IS_INTEGER); }
+  | '$distinct' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::DISTINCT); }
+  ;
+
+definedFun[CVC4::Expr& expr]
+@declarations {
+  bool remainder = false;
+}
+  : '$uminus' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::UMINUS); }
+  | '$sum' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::PLUS); }
+  | '$difference' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::MINUS); }
+  | '$product' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::MULT); }
+  | '$quotient' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::DIVISION_TOTAL); }
+  | ( '$quotient_e' { remainder = false; }
+    | '$remainder_e' { remainder = true; }
+    )
+    { Expr n = EXPR_MANAGER->mkBoundVar("N", EXPR_MANAGER->realType());
+      Expr d = EXPR_MANAGER->mkBoundVar("D", EXPR_MANAGER->realType());
+      Expr formals = MK_EXPR(CVC4::kind::BOUND_VAR_LIST, n, d);
+      expr = MK_EXPR(CVC4::kind::DIVISION_TOTAL, n, d);
+      expr = MK_EXPR(CVC4::kind::ITE, MK_EXPR(CVC4::kind::GEQ, d, MK_CONST(Rational(0))),
+                                      MK_EXPR(CVC4::kind::TO_INTEGER, expr),
+                                      MK_EXPR(CVC4::kind::UMINUS, MK_EXPR(CVC4::kind::TO_INTEGER, MK_EXPR(CVC4::kind::UMINUS, expr))));
+      if(remainder) {
+        expr = MK_EXPR(CVC4::kind::MINUS, n, MK_EXPR(CVC4::kind::MULT, expr, d));
+      }
+      expr = MK_EXPR(CVC4::kind::LAMBDA, formals, expr);
+    }
+  | ( '$quotient_t' { remainder = false; }
+    | '$remainder_t' { remainder = true; }
+    )
+    { Expr n = EXPR_MANAGER->mkBoundVar("N", EXPR_MANAGER->realType());
+      Expr d = EXPR_MANAGER->mkBoundVar("D", EXPR_MANAGER->realType());
+      Expr formals = MK_EXPR(CVC4::kind::BOUND_VAR_LIST, n, d);
+      expr = MK_EXPR(CVC4::kind::DIVISION_TOTAL, n, d);
+      expr = MK_EXPR(CVC4::kind::ITE, MK_EXPR(CVC4::kind::GEQ, expr, MK_CONST(Rational(0))),
+                                      MK_EXPR(CVC4::kind::TO_INTEGER, expr),
+                                      MK_EXPR(CVC4::kind::UMINUS, MK_EXPR(CVC4::kind::TO_INTEGER, MK_EXPR(CVC4::kind::UMINUS, expr))));
+      if(remainder) {
+        expr = MK_EXPR(CVC4::kind::MINUS, n, MK_EXPR(CVC4::kind::MULT, expr, d));
+      }
+      expr = MK_EXPR(CVC4::kind::LAMBDA, formals, expr);
+    }
+  | ( '$quotient_f' { remainder = false; }
+    | '$remainder_f' { remainder = true; }
+    )
+    { Expr n = EXPR_MANAGER->mkBoundVar("N", EXPR_MANAGER->realType());
+      Expr d = EXPR_MANAGER->mkBoundVar("D", EXPR_MANAGER->realType());
+      Expr formals = MK_EXPR(CVC4::kind::BOUND_VAR_LIST, n, d);
+      expr = MK_EXPR(CVC4::kind::DIVISION_TOTAL, n, d);
+      expr = MK_EXPR(CVC4::kind::TO_INTEGER, expr);
+      if(remainder) {
+        expr = MK_EXPR(CVC4::kind::MINUS, n, MK_EXPR(CVC4::kind::MULT, expr, d));
+      }
+      expr = MK_EXPR(CVC4::kind::LAMBDA, formals, expr);
+    }
+  | '$floor' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::TO_INTEGER); }
+  | '$ceiling'
+    { Expr n = EXPR_MANAGER->mkBoundVar("N", EXPR_MANAGER->realType());
+      Expr formals = MK_EXPR(CVC4::kind::BOUND_VAR_LIST, n);
+      expr = MK_EXPR(CVC4::kind::UMINUS, MK_EXPR(CVC4::kind::TO_INTEGER, MK_EXPR(CVC4::kind::UMINUS, n)));
+      expr = MK_EXPR(CVC4::kind::LAMBDA, formals, expr);
+    }
+  | '$truncate'
+    { Expr n = EXPR_MANAGER->mkBoundVar("N", EXPR_MANAGER->realType());
+      Expr formals = MK_EXPR(CVC4::kind::BOUND_VAR_LIST, n);
+      expr = MK_EXPR(CVC4::kind::ITE, MK_EXPR(CVC4::kind::GEQ, n, MK_CONST(Rational(0))),
+                                      MK_EXPR(CVC4::kind::TO_INTEGER, n),
+                                      MK_EXPR(CVC4::kind::UMINUS, MK_EXPR(CVC4::kind::TO_INTEGER, MK_EXPR(CVC4::kind::UMINUS, n))));
+      expr = MK_EXPR(CVC4::kind::LAMBDA, formals, expr);
+    }
+  | '$round'
+    { Expr n = EXPR_MANAGER->mkBoundVar("N", EXPR_MANAGER->realType());
+      Expr formals = MK_EXPR(CVC4::kind::BOUND_VAR_LIST, n);
+      Expr decPart = MK_EXPR(CVC4::kind::MINUS, n, MK_EXPR(CVC4::kind::TO_INTEGER, n));
+      expr = MK_EXPR(CVC4::kind::ITE, MK_EXPR(CVC4::kind::LT, decPart, MK_CONST(Rational(1, 2))),
+                                      // if decPart < 0.5, round down
+                                      MK_EXPR(CVC4::kind::TO_INTEGER, n),
+             MK_EXPR(CVC4::kind::ITE, MK_EXPR(CVC4::kind::GT, decPart, MK_CONST(Rational(1, 2))),
+                                      // if decPart > 0.5, round up
+                                      MK_EXPR(CVC4::kind::TO_INTEGER, MK_EXPR(CVC4::kind::PLUS, n, MK_CONST(Rational(1)))),
+                                      // if decPart == 0.5, round to nearest even integer:
+                                      // result is: to_int(n/2 + .5) * 2
+                                      MK_EXPR(CVC4::kind::MULT, MK_EXPR(CVC4::kind::TO_INTEGER, MK_EXPR(CVC4::kind::PLUS, MK_EXPR(CVC4::kind::DIVISION_TOTAL, n, MK_CONST(Rational(2))), MK_CONST(Rational(1, 2)))), MK_CONST(Rational(2)))));
+      expr = MK_EXPR(CVC4::kind::LAMBDA, formals, expr);
+    }
+  | '$to_int' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::TO_INTEGER); }
+  | '$to_rat' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::TO_REAL); }
+  | '$to_real' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::TO_REAL); }
+  ;
+
 //%----Pure CNF should not use $true or $false in problems, and use $false only
 //%----at the roots of a refutation.
 
-equalOp[bool & equal]
- :  EQUAL_TOK    {equal = true;}
-  | DISEQUAL_TOK {equal = false;}
+equalOp[bool& equal]
+  : EQUAL_TOK    { equal = true; }
+  | DISEQUAL_TOK { equal = false; }
   ;
 
 term[CVC4::Expr& expr]
- : functionTerm[expr]
+  : functionTerm[expr]
+  | conditionalTerm[expr]
   | simpleTerm[expr]
-//  | conditionalTerm
-//  | let_term
+  | letTerm[expr]
+  ;
+
+letTerm[CVC4::Expr& expr]
+@declarations {
+  CVC4::Expr lhs, rhs;
+}
+  : '$let_ft' LPAREN_TOK { PARSER_STATE->pushScope(); }
+    tffLetFormulaDefn[lhs, rhs] COMMA_TOK
+    term[expr]
+    { PARSER_STATE->popScope();
+      expr = expr.substitute(lhs, rhs);
+    }
+    RPAREN_TOK
+  | '$let_tt' LPAREN_TOK { PARSER_STATE->pushScope(); }
+    tffLetTermDefn[lhs, rhs] COMMA_TOK
+    term[expr]
+    { PARSER_STATE->popScope();
+      expr = expr.substitute(lhs, rhs);
+    }
+    RPAREN_TOK
   ;
 
 /* Not an application */
 simpleTerm[CVC4::Expr& expr]
   : variable[expr]
   | NUMBER { expr = PARSER_STATE->d_tmp_expr; }
-  | DISTINCT_OBJECT { expr = PARSER_STATE->convertStrToUnsorted(
-        AntlrInput::tokenText($DISTINCT_OBJECT)); }
-;
+  | DISTINCT_OBJECT { expr = PARSER_STATE->convertStrToUnsorted(AntlrInput::tokenText($DISTINCT_OBJECT)); }
+  ;
 
 functionTerm[CVC4::Expr& expr]
-  : plainTerm[expr] // | <defined_term> | <system_term>
+@declarations {
+  std::vector<CVC4::Expr> args;
+}
+  : plainTerm[expr]
+  | definedFun[expr] LPAREN_TOK arguments[args] RPAREN_TOK
+    { expr = EXPR_MANAGER->mkExpr(expr, args); }
+// | <system_term>
+  ;
+
+conditionalTerm[CVC4::Expr& expr]
+@declarations {
+  CVC4::Expr expr2, expr3;
+}
+  : '$ite_t' LPAREN_TOK tffLogicFormula[expr] COMMA_TOK term[expr2] COMMA_TOK term[expr3] RPAREN_TOK
+    { expr = EXPR_MANAGER->mkExpr(CVC4::kind::ITE, expr, expr2, expr3); }
   ;
 
 plainTerm[CVC4::Expr& expr]
-@declarations{
+@declarations {
   std::string name;
   std::vector<Expr> args;
 }
@@ -308,19 +481,19 @@ plainTerm[CVC4::Expr& expr]
     }
   ;
 
-arguments[std::vector<CVC4::Expr> & args]
-@declarations{
+arguments[std::vector<CVC4::Expr>& args]
+@declarations {
   Expr expr;
 }
   :
   term[expr] { args.push_back(expr); } ( COMMA_TOK term[expr] { args.push_back(expr); } )*
   ;
 
-variable[CVC4::Expr & expr]
+variable[CVC4::Expr& expr]
   : UPPER_WORD
     {
       std::string name = AntlrInput::tokenText($UPPER_WORD);
-      if(!PARSER_STATE->cnf || PARSER_STATE->isDeclared(name)){
+      if(!PARSER_STATE->cnf || PARSER_STATE->isDeclared(name)) {
         expr = PARSER_STATE->getVariable(name);
       } else {
         expr = PARSER_STATE->mkBoundVar(name, PARSER_STATE->d_unsorted);
@@ -331,18 +504,18 @@ variable[CVC4::Expr & expr]
 
 /*******/
 /* FOF */
-fofFormula[CVC4::Expr & expr] : fofLogicFormula[expr] ;
+fofFormula[CVC4::Expr& expr] : fofLogicFormula[expr] ;
 
-fofLogicFormula[CVC4::Expr & expr]
-@declarations{
+fofLogicFormula[CVC4::Expr& expr]
+@declarations {
   tptp::NonAssoc na;
   std::vector< Expr > args;
   Expr expr2;
 }
   : fofUnitaryFormula[expr]
-    ( //Non Assoc <=> <~> ~& ~|
+    ( // Non-associative: <=> <~> ~& ~|
       ( fofBinaryNonAssoc[na] fofUnitaryFormula[expr2]
-        { switch(na){
+        { switch(na) {
            case tptp::NA_IFF:
              expr = MK_EXPR(kind::IFF,expr,expr2);
              break;
@@ -364,21 +537,21 @@ fofLogicFormula[CVC4::Expr & expr]
           }
         }
       )
-    | //And &
+    | // N-ary and &
       ( { args.push_back(expr); }
         ( AND_TOK fofUnitaryFormula[expr] { args.push_back(expr); } )+
-        { expr = MK_EXPR(kind::AND,args); }
+        { expr = MK_EXPR_ASSOCIATIVE(kind::AND, args); }
       )
-    | //Or |
+    | // N-ary or |
       ( { args.push_back(expr); }
         ( OR_TOK fofUnitaryFormula[expr] { args.push_back(expr); } )+
-        { expr = MK_EXPR(kind::OR,args); }
+        { expr = MK_EXPR_ASSOCIATIVE(kind::OR, args); }
       )
-   )?
+    )?
   ;
 
-fofUnitaryFormula[CVC4::Expr & expr]
-@declarations{
+fofUnitaryFormula[CVC4::Expr& expr]
+@declarations {
   Kind kind;
   std::vector< Expr > bv;
 }
@@ -389,20 +562,20 @@ fofUnitaryFormula[CVC4::Expr & expr]
     folQuantifier[kind] LBRACK_TOK {PARSER_STATE->pushScope();}
     ( bindvariable[expr] { bv.push_back(expr); }
       ( COMMA_TOK bindvariable[expr] { bv.push_back(expr); } )* ) RBRACK_TOK
-  COLON_TOK fofUnitaryFormula[expr]
-  { PARSER_STATE->popScope();
-    expr = MK_EXPR(kind, MK_EXPR(kind::BOUND_VAR_LIST, bv), expr);
-  } ;
+    COLON_TOK fofUnitaryFormula[expr]
+    { PARSER_STATE->popScope();
+      expr = MK_EXPR(kind, MK_EXPR(kind::BOUND_VAR_LIST, bv), expr);
+    }
+  ;
 
-bindvariable[CVC4::Expr & expr]
+bindvariable[CVC4::Expr& expr]
   : UPPER_WORD
-    {
-      std::string name = AntlrInput::tokenText($UPPER_WORD);
+    { std::string name = AntlrInput::tokenText($UPPER_WORD);
       expr = PARSER_STATE->mkBoundVar(name, PARSER_STATE->d_unsorted);
     }
-    ;
+  ;
 
-fofBinaryNonAssoc[CVC4::parser::tptp::NonAssoc & na]
+fofBinaryNonAssoc[CVC4::parser::tptp::NonAssoc& na]
   : IFF_TOK      { na = tptp::NA_IFF; }
   | REVIFF_TOK   { na = tptp::NA_REVIFF; }
   | REVOR_TOK    { na = tptp::NA_REVOR; }
@@ -411,11 +584,229 @@ fofBinaryNonAssoc[CVC4::parser::tptp::NonAssoc & na]
   | REVIMPLIES_TOK { na = tptp::NA_REVIMPLIES; }
   ;
 
-folQuantifier[CVC4::Kind & kind]
+folQuantifier[CVC4::Kind& kind]
   : BANG_TOK { kind = kind::FORALL; }
   | MARK_TOK { kind = kind::EXISTS; }
   ;
 
+/*******/
+/* TFF */
+tffFormula[CVC4::Expr& expr] : tffLogicFormula[expr];
+
+tffTypedAtom[CVC4::Command*& cmd]
+@declarations {
+  CVC4::Expr expr;
+  CVC4::Type type;
+  std::string name;
+}
+  : LPAREN_TOK tffTypedAtom[cmd] RPAREN_TOK
+  | nameN[name] COLON_TOK
+    ( '$tType'
+      { if(PARSER_STATE->isDeclared(name, SYM_SORT)) {
+          // duplicate declaration is fine, they're compatible
+          cmd = new EmptyCommand("compatible redeclaration of sort " + name);
+        } else if(PARSER_STATE->isDeclared(name, SYM_VARIABLE)) {
+          // error: cannot be both sort and constant
+          PARSER_STATE->parseError("Symbol `" + name + "' previously declared as a constant; cannot also be a sort");
+        } else {
+          // as yet, it's undeclared
+          Type type = PARSER_STATE->mkSort(name);
+          cmd = new DeclareTypeCommand(name, 0, type);
+        }
+      }
+    | parseType[type]
+      { if(PARSER_STATE->isDeclared(name, SYM_SORT)) {
+          // error: cannot be both sort and constant
+          PARSER_STATE->parseError("Symbol `" + name + "' previously declared as a sort");
+          cmd = new EmptyCommand("compatible redeclaration of sort " + name);
+        } else if(PARSER_STATE->isDeclared(name, SYM_VARIABLE)) {
+          if(type == PARSER_STATE->getVariable(name).getType()) {
+            // duplicate declaration is fine, they're compatible
+            cmd = new EmptyCommand("compatible redeclaration of constant " + name);
+          } else {
+            // error: sorts incompatible
+            PARSER_STATE->parseError("Symbol `" + name + "' declared previously with a different sort");
+          }
+        } else {
+          // as yet, it's undeclared
+          CVC4::Expr expr;
+          if(type.isFunction()) {
+            expr = PARSER_STATE->mkTffFunction(name, type);
+          } else {
+            expr = PARSER_STATE->mkTffVar(name, type);
+          }
+          cmd = new DeclareFunctionCommand(name, expr, type);
+        }
+      }
+    )
+  ;
+
+tffLogicFormula[CVC4::Expr& expr]
+@declarations {
+  tptp::NonAssoc na;
+  std::vector< Expr > args;
+  Expr expr2;
+}
+  : tffUnitaryFormula[expr]
+    ( // Non Assoc <=> <~> ~& ~|
+      ( fofBinaryNonAssoc[na] tffUnitaryFormula[expr2]
+        { switch(na) {
+           case tptp::NA_IFF:
+             expr = MK_EXPR(kind::IFF,expr,expr2);
+             break;
+           case tptp::NA_REVIFF:
+             expr = MK_EXPR(kind::XOR,expr,expr2);
+             break;
+           case tptp::NA_IMPLIES:
+             expr = MK_EXPR(kind::IMPLIES,expr,expr2);
+             break;
+           case tptp::NA_REVIMPLIES:
+             expr = MK_EXPR(kind::IMPLIES,expr2,expr);
+             break;
+           case tptp::NA_REVOR:
+             expr = MK_EXPR(kind::NOT,MK_EXPR(kind::OR,expr,expr2));
+             break;
+           case tptp::NA_REVAND:
+             expr = MK_EXPR(kind::NOT,MK_EXPR(kind::AND,expr,expr2));
+             break;
+          }
+        }
+      )
+    | // And &
+      ( { args.push_back(expr); }
+        ( AND_TOK tffUnitaryFormula[expr] { args.push_back(expr); } )+
+        { expr = MK_EXPR(kind::AND,args); }
+      )
+    | // Or |
+      ( { args.push_back(expr); }
+        ( OR_TOK tffUnitaryFormula[expr] { args.push_back(expr); } )+
+        { expr = MK_EXPR(kind::OR,args); }
+      )
+    )?
+  ;
+
+tffUnitaryFormula[CVC4::Expr& expr]
+@declarations {
+  Kind kind;
+  std::vector< Expr > bv;
+  Expr lhs, rhs;
+}
+  : atomicFormula[expr]
+  | LPAREN_TOK tffLogicFormula[expr] RPAREN_TOK
+  | NOT_TOK tffUnitaryFormula[expr] { expr = MK_EXPR(kind::NOT,expr); }
+  | // Quantified
+    folQuantifier[kind] LBRACK_TOK {PARSER_STATE->pushScope();}
+    ( tffbindvariable[expr] { bv.push_back(expr); }
+      ( COMMA_TOK tffbindvariable[expr] { bv.push_back(expr); } )* ) RBRACK_TOK
+    COLON_TOK tffUnitaryFormula[expr]
+    { PARSER_STATE->popScope();
+      expr = MK_EXPR(kind, MK_EXPR(kind::BOUND_VAR_LIST, bv), expr);
+    }
+  | '$ite_f' LPAREN_TOK tffLogicFormula[expr] COMMA_TOK tffLogicFormula[lhs] COMMA_TOK tffLogicFormula[rhs] RPAREN_TOK
+    { expr = EXPR_MANAGER->mkExpr(CVC4::kind::ITE, expr, lhs, rhs); }
+  | '$let_tf' LPAREN_TOK { PARSER_STATE->pushScope(); }
+    tffLetTermDefn[lhs, rhs] COMMA_TOK
+    tffFormula[expr]
+    { PARSER_STATE->popScope();
+      expr = expr.substitute(lhs, rhs);
+    }
+    RPAREN_TOK
+  | '$let_ff' LPAREN_TOK { PARSER_STATE->pushScope(); }
+    tffLetFormulaDefn[lhs, rhs] COMMA_TOK
+    tffFormula[expr]
+    { PARSER_STATE->popScope();
+      expr = expr.substitute(lhs, rhs);
+    }
+    RPAREN_TOK
+  ;
+
+tffLetTermDefn[CVC4::Expr& lhs, CVC4::Expr& rhs]
+@declarations {
+  std::vector<CVC4::Expr> bvlist;
+}
+  : (BANG_TOK LBRACK_TOK tffVariableList[bvlist] RBRACK_TOK COLON_TOK)*
+    tffLetTermBinding[bvlist, lhs, rhs]
+  ;
+
+tffLetTermBinding[std::vector<CVC4::Expr>& bvlist, CVC4::Expr& lhs, CVC4::Expr& rhs]
+  : term[lhs] EQUAL_TOK term[rhs]
+    { PARSER_STATE->checkLetBinding(bvlist, lhs, rhs, false);
+      rhs = MK_EXPR(CVC4::kind::LAMBDA, MK_EXPR(CVC4::kind::BOUND_VAR_LIST, lhs.getChildren()), rhs);
+      lhs = lhs.getOperator();
+    }
+  | LPAREN_TOK tffLetTermBinding[bvlist, lhs, rhs] RPAREN_TOK
+  ;
+
+tffLetFormulaDefn[CVC4::Expr& lhs, CVC4::Expr& rhs]
+@declarations {
+  std::vector<CVC4::Expr> bvlist;
+}
+  : (BANG_TOK LBRACK_TOK tffVariableList[bvlist] RBRACK_TOK COLON_TOK)*
+    tffLetFormulaBinding[bvlist, lhs, rhs]
+  ;
+
+tffLetFormulaBinding[std::vector<CVC4::Expr>& bvlist, CVC4::Expr& lhs, CVC4::Expr& rhs]
+  : atomicFormula[lhs] IFF_TOK tffUnitaryFormula[rhs]
+    { PARSER_STATE->checkLetBinding(bvlist, lhs, rhs, true);
+      rhs = MK_EXPR(CVC4::kind::LAMBDA, MK_EXPR(CVC4::kind::BOUND_VAR_LIST, lhs.getChildren()), rhs);
+      lhs = lhs.getOperator();
+    }
+  | LPAREN_TOK tffLetFormulaBinding[bvlist, lhs, rhs] RPAREN_TOK
+  ;
+
+tffbindvariable[CVC4::Expr& expr]
+@declarations {
+  CVC4::Type type = PARSER_STATE->d_unsorted;
+}
+  : UPPER_WORD
+    ( COLON_TOK parseType[type] )?
+    { std::string name = AntlrInput::tokenText($UPPER_WORD);
+      expr = PARSER_STATE->mkBoundVar(name, type);
+    }
+  ;
+
+// bvlist is accumulative; it can already contain elements
+// on the way in, which are left undisturbed
+tffVariableList[std::vector<CVC4::Expr>& bvlist]
+@declarations {
+  CVC4::Expr e;
+}
+  : tffbindvariable[e] { bvlist.push_back(e); }
+    ( COMMA_TOK tffbindvariable[e] { bvlist.push_back(e); } )*
+  ;
+
+parseType[CVC4::Type& type]
+@declarations {
+  std::vector<CVC4::Type> v;
+}
+  : simpleType[type]
+  | ( simpleType[type] { v.push_back(type); }
+    | LPAREN_TOK simpleType[type] { v.push_back(type); }
+      ( TIMES_TOK simpleType[type] { v.push_back(type); } )+
+      RPAREN_TOK
+    )
+    GREATER_TOK simpleType[type]
+    { v.push_back(type);
+      type = EXPR_MANAGER->mkFunctionType(v);
+    }
+  ;
+
+// non-function types
+simpleType[CVC4::Type& type]
+  : DEFINED_SYMBOL
+    { std::string s = AntlrInput::tokenText($DEFINED_SYMBOL);
+      if(s == "\$i") type = PARSER_STATE->d_unsorted;
+      else if(s == "\$o") type = EXPR_MANAGER->booleanType();
+      else if(s == "\$int") type = EXPR_MANAGER->integerType();
+      else if(s == "\$rat") type = EXPR_MANAGER->realType();
+      else if(s == "\$real") type = EXPR_MANAGER->realType();
+      else if(s == "\$tType") PARSER_STATE->parseError("Type of types `\$tType' cannot be used here");
+      else PARSER_STATE->parseError("unknown defined type `" + s + "'");
+    }
+  | LOWER_WORD
+    { type = PARSER_STATE->getSort(AntlrInput::tokenText($LOWER_WORD)); }
+  ;
+
 /***********************************************/
 /* Anything well parenthesis */
 
@@ -447,6 +838,7 @@ anything
   | FOF_TOK
   | THF_TOK
   | TFF_TOK
+  | TYPE_TOK
   | INCLUDE_TOK
   | DISTINCT_OBJECT
   | UPPER_WORD
@@ -467,6 +859,8 @@ LBRACK_TOK : '[';
 RBRACK_TOK : ']';
 COLON_TOK  : ':';
 
+GREATER_TOK  : '>';
+
 //operator
 OR_TOK       : '|';
 NOT_TOK      : '~';
@@ -494,6 +888,7 @@ CNF_TOK     : 'cnf';
 FOF_TOK     : 'fof';
 THF_TOK     : 'thf';
 TFF_TOK     : 'tff';
+TYPE_TOK    : 'type';
 INCLUDE_TOK : 'include';
 
 //Other defined symbols, must be defined after all the other
@@ -533,30 +928,30 @@ UPPER_WORD : UPPER_ALPHA ALPHA_NUMERIC*;
 LOWER_WORD : LOWER_ALPHA ALPHA_NUMERIC*;
 
 /* filename */
-unquotedFileName[std::string & name] /* Beware fileName identifier is used by the backend ... */
+unquotedFileName[std::string& name] /* Beware fileName identifier is used by the backend ... */
  : (s=LOWER_WORD_SINGLE_QUOTED | s=SINGLE_QUOTED)
     { name = AntlrInput::tokenText($s);
       name = name.substr(1, name.size() - 2 );
     };
 
 /* axiom name */
-nameN[std::string & name]
+nameN[std::string& name]
  : atomicWord[name]
  | NUMBER { name = AntlrInput::tokenText($NUMBER); }
  ;
 
 /* atomic word everything (fof, cnf, thf, tff, include must not be keyword at this position ) */
-atomicWord[std::string & name]
+atomicWord[std::string& name]
  : FOF_TOK     { name = "fof"; }
  | CNF_TOK     { name = "cnf"; }
  | THF_TOK     { name = "thf"; }
  | TFF_TOK     { name = "tff"; }
+ | TYPE_TOK    { name = "type"; }
  | INCLUDE_TOK { name = "include"; }
  | LOWER_WORD  { name = AntlrInput::tokenText($LOWER_WORD); }
- | LOWER_WORD_SINGLE_QUOTED //the lower word single quoted are considered without quote
-    {
-      /* strip off the quotes */
-      name = AntlrInput::tokenTextSubstr($LOWER_WORD_SINGLE_QUOTED,1,
+ | LOWER_WORD_SINGLE_QUOTED // the lower word single quoted are considered without quote
+    { /* strip off the quotes */
+      name = AntlrInput::tokenTextSubstr($LOWER_WORD_SINGLE_QUOTED, 1 ,
                                          ($LOWER_WORD_SINGLE_QUOTED->stop - $LOWER_WORD_SINGLE_QUOTED->start) - 1);
     }
  | SINGLE_QUOTED {name = AntlrInput::tokenText($SINGLE_QUOTED); }; //for the others the quote remains
@@ -565,35 +960,34 @@ atomicWord[std::string & name]
 /* Rational */
 
 fragment DOT              : '.';
-fragment EXPONENT         : 'E'|'e';
+fragment EXPONENT         : 'E' | 'e';
 fragment SLASH            : '/';
 
 fragment DECIMAL : NUMERIC+;
 
-/* Currently we put all in the rationnal type */
-fragment SIGN[bool & pos] : PLUS_TOK | MINUS_TOK { pos = false; } ;
-
+/* Currently we put all in the rational type */
+fragment SIGN[bool& pos]
+  : PLUS_TOK { pos = true; }
+  | MINUS_TOK { pos = false; }
+  ;
 
 NUMBER
-@declarations{
+@declarations {
   bool pos = true;
   bool posE = true;
 }
-  :
-  ( SIGN[pos]? num=DECIMAL
-    {
-      Integer i (AntlrInput::tokenText($num));
-      Rational r = ( pos ? i : -i );
-      PARSER_STATE->d_tmp_expr = MK_CONST(r);
-    }
-  | SIGN[pos]? num=DECIMAL DOT den=DECIMAL (EXPONENT SIGN[posE]? e=DECIMAL)?
-    {
-        std::string snum = AntlrInput::tokenText($num);
+  : ( SIGN[pos]? num=DECIMAL
+      { Integer i(AntlrInput::tokenText($num));
+        Rational r = pos ? i : -i;
+        PARSER_STATE->d_tmp_expr = MK_CONST(r);
+      }
+    | SIGN[pos]? num=DECIMAL DOT den=DECIMAL (EXPONENT SIGN[posE]? e=DECIMAL)?
+      { std::string snum = AntlrInput::tokenText($num);
         std::string sden = AntlrInput::tokenText($den);
         /* compute the numerator */
-        Integer inum( snum + sden );
+        Integer inum(snum + sden);
         // The sign
-        inum = pos ? inum : - inum;
+        inum = pos ? inum : -inum;
         // The exponent
         size_t exp = ($e == NULL ? 0 : AntlrInput::tokenToUnsigned($e));
         // Decimal part
@@ -601,26 +995,25 @@ NUMBER
         /* multiply it by 10 raised to the exponent reduced by the
          * number of decimal place in den (dec) */
         Rational r;
-        if( !posE ) r = Rational(inum, Integer(10).pow(exp + dec));
-        else if( exp == dec ) r = Rational(inum);
-        else if( exp > dec ) r = Rational(inum * Integer(10).pow(exp - dec));
+        if(!posE) r = Rational(inum, Integer(10).pow(exp + dec));
+        else if(exp == dec) r = Rational(inum);
+        else if(exp > dec) r = Rational(inum * Integer(10).pow(exp - dec));
         else r = Rational(inum, Integer(10).pow(dec - exp));
-        PARSER_STATE->d_tmp_expr = MK_CONST( r );
+        PARSER_STATE->d_tmp_expr = MK_CONST(r);
+      }
+    | SIGN[pos]? num=DECIMAL SLASH den=DECIMAL
+      { Integer inum(AntlrInput::tokenText($num));
+        Integer iden(AntlrInput::tokenText($den));
+        PARSER_STATE->d_tmp_expr = MK_CONST(Rational(pos ? inum : -inum, iden));
+      }
+    )
+    { if(PARSER_STATE->cnf || PARSER_STATE->fof) {
+        // We're in an unsorted context, so put a conversion around it
+        PARSER_STATE->d_tmp_expr = PARSER_STATE->convertRatToUnsorted( PARSER_STATE->d_tmp_expr );
       }
-  | SIGN[pos]? num=DECIMAL SLASH den=DECIMAL
-    {
-      Integer inum(AntlrInput::tokenText($num));
-      Integer iden(AntlrInput::tokenText($den));
-      PARSER_STATE->d_tmp_expr = MK_CONST(
-        Rational(pos ? inum : -inum, iden));
-    }
-  ) {
-      //Put a convertion around it
-      PARSER_STATE->d_tmp_expr = PARSER_STATE->convertRatToUnsorted( PARSER_STATE->d_tmp_expr );
     }
   ;
 
-
 /**
  * Matches the comments and ignores them
  */
@@ -629,5 +1022,3 @@ COMMENT
   | '/*'  ( options {greedy=false;} : . )*  '*/' { SKIP(); } //comment block
   ;
 
-
-
diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp
index 93c2168b1..3e6aa82b7 100644
--- a/src/parser/tptp/tptp.cpp
+++ b/src/parser/tptp/tptp.cpp
@@ -33,26 +33,26 @@ Tptp::Tptp(ExprManager* exprManager, Input* input, bool strictMode, bool parseOn
   /* Try to find TPTP dir */
   // From tptp4x FileUtilities
   //----Try the TPTP directory, and TPTP variations
-    char* home = getenv("TPTP");
-    if (home == NULL) {
-        home = getenv("TPTP_HOME");
+  char* home = getenv("TPTP");
+  if(home == NULL) {
+     home = getenv("TPTP_HOME");
 // //----If no TPTP_HOME, try the tptp user (aaargh)
-//         if (home == NULL && (PasswdEntry = getpwnam("tptp")) != NULL) {
-//             home = PasswdEntry->pw_dir;
+//         if(home == NULL && (PasswdEntry = getpwnam("tptp")) != NULL) {
+//            home = PasswdEntry->pw_dir;
 //         }
 //----Now look in the TPTP directory from there
-        if (home != NULL) {
-          d_tptpDir = home;
-          d_tptpDir.append("/TPTP/");
-        }
-    } else {
+    if(home != NULL) {
       d_tptpDir = home;
-      //add trailing "/"
-      if( d_tptpDir[d_tptpDir.size() - 1] != '/'){
-        d_tptpDir.append("/");
-      }
+      d_tptpDir.append("/TPTP/");
     }
-    d_hasConjecture = false;
+  } else {
+    d_tptpDir = home;
+    //add trailing "/"
+    if(d_tptpDir[d_tptpDir.size() - 1] != '/') {
+      d_tptpDir.append("/");
+    }
+  }
+  d_hasConjecture = false;
 }
 
 void Tptp::addTheory(Theory theory) {
@@ -92,7 +92,7 @@ void Tptp::addTheory(Theory theory) {
 /* The include are managed in the lexer but called in the parser */
 // Inspired by http://www.antlr3.org/api/C/interop.html
 
-bool newInputStream(std::string fileName, pANTLR3_LEXER lexer){
+bool newInputStream(std::string fileName, pANTLR3_LEXER lexer) {
   Debug("parser") << "Including " << fileName << std::endl;
   // Create a new input stream and take advantage of built in stream stacking
   // in C target runtime.
@@ -103,7 +103,7 @@ bool newInputStream(std::string fileName, pANTLR3_LEXER lexer){
 #else /* CVC4_ANTLR3_OLD_INPUT_STREAM */
   in = antlr3FileStreamNew((pANTLR3_UINT8) fileName.c_str(), ANTLR3_ENC_8BIT);
 #endif /* CVC4_ANTLR3_OLD_INPUT_STREAM */
-  if( in == NULL ) {
+  if(in == NULL) {
     Debug("parser") << "Can't open " << fileName << std::endl;
     return false;
   }
@@ -126,8 +126,15 @@ bool newInputStream(std::string fileName, pANTLR3_LEXER lexer){
   return true;
 }
 
+/* overridden popCharStream for the lexer - necessary if we had symbol
+ * filtering in file inclusion.
+void Tptp::myPopCharStream(pANTLR3_LEXER lexer) {
+  ((Tptp*)lexer->super)->d_oldPopCharStream(lexer);
+  ((Tptp*)lexer->super)->popScope();
+}
+*/
 
-void Tptp::includeFile(std::string fileName){
+void Tptp::includeFile(std::string fileName) {
   // security for online version
   if(!canIncludeFile()) {
     parseError("include-file feature was disabled for this run.");
@@ -136,36 +143,78 @@ void Tptp::includeFile(std::string fileName){
   // Get the lexer
   AntlrInput * ai = static_cast<AntlrInput *>(getInput());
   pANTLR3_LEXER lexer = ai->getAntlr3Lexer();
+
+  // set up popCharStream - would be necessary for handling symbol
+  // filtering in inclusions
+  /*
+  if(d_oldPopCharStream == NULL) {
+    d_oldPopCharStream = lexer->popCharStream;
+    lexer->popCharStream = myPopCharStream;
+  }
+  */
+
+  // push the inclusion scope; will be popped by our special popCharStream
+  // would be necessary for handling symbol filtering in inclusions
+  //pushScope();
+
   // get the name of the current stream "Does it work inside an include?"
   const std::string inputName = ai->getInputStreamName();
 
   // Test in the directory of the actual parsed file
   std::string currentDirFileName;
-  if( inputName != "<stdin>"){
+  if(inputName != "<stdin>") {
     // TODO: Use dirname ot Boost::filesystem?
     size_t pos = inputName.rfind('/');
-    if( pos != std::string::npos){
+    if(pos != std::string::npos) {
       currentDirFileName = std::string(inputName, 0, pos + 1);
     }
     currentDirFileName.append(fileName);
-    if( newInputStream(currentDirFileName,lexer) ){
+    if(newInputStream(currentDirFileName,lexer)) {
       return;
     }
   } else {
     currentDirFileName = "<unknown current directory for stdin>";
   }
 
-  if( d_tptpDir.empty() ){
+  if(d_tptpDir.empty()) {
     parseError("Couldn't open included file: " + fileName
                + " at " + currentDirFileName + " and the TPTP directory is not specified (environment variable TPTP)");
   };
 
   std::string tptpDirFileName = d_tptpDir + fileName;
-  if( !newInputStream(tptpDirFileName,lexer) ){
+  if(! newInputStream(tptpDirFileName,lexer)) {
     parseError("Couldn't open included file: " + fileName
                + " at " + currentDirFileName + " or " + tptpDirFileName);
   }
 }
 
+void Tptp::checkLetBinding(std::vector<Expr>& bvlist, Expr lhs, Expr rhs, bool formula) {
+  if(lhs.getKind() != CVC4::kind::APPLY_UF) {
+    parseError("malformed let: LHS must be a flat function application");
+  }
+  std::vector<CVC4::Expr> v = lhs.getChildren();
+  if(formula && !lhs.getType().isBoolean()) {
+    parseError("malformed let: LHS must be formula");
+  }
+  for(size_t i = 0; i < v.size(); ++i) {
+    if(v[i].hasOperator()) {
+      parseError("malformed let: LHS must be flat, illegal child: " + v[i].toString());
+    }
+  }
+  std::sort(v.begin(), v.end());
+  std::sort(bvlist.begin(), bvlist.end());
+  // ensure all let-bound variables appear on the LHS, and appear only once
+  for(size_t i = 0; i < bvlist.size(); ++i) {
+    std::vector<CVC4::Expr>::const_iterator found = std::lower_bound(v.begin(), v.end(), bvlist[i]);
+    if(found == v.end() || *found != bvlist[i]) {
+      parseError("malformed let: LHS must make use of all quantified variables, missing `" + bvlist[i].toString() + "'");
+    }
+    std::vector<CVC4::Expr>::const_iterator found2 = found + 1;
+    if(found2 != v.end() && *found2 == *found) {
+      parseError("malformed let: LHS cannot use same bound variable twice: " + (*found).toString());
+    }
+  }
+}
+
 }/* CVC4::parser namespace */
 }/* CVC4 namespace */
diff --git a/src/parser/tptp/tptp.h b/src/parser/tptp/tptp.h
index cea246282..79092e98f 100644
--- a/src/parser/tptp/tptp.h
+++ b/src/parser/tptp/tptp.h
@@ -25,6 +25,7 @@
 #include <ext/hash_set>
 #include <cassert>
 #include "parser/options.h"
+#include "parser/antlr_input.h"
 
 namespace CVC4 {
 
@@ -46,51 +47,57 @@ class Tptp : public Parser {
   std::hash_set<Expr, ExprHashFunction> d_r_converted;
   std::hash_map<std::string, Expr, StringHashFunction> d_distinct_objects;
 
-  //TPTP directory where to find includes
+  // TPTP directory where to find includes;
   // empty if none could be determined
   std::string d_tptpDir;
 
-  //hack to make output SZS ontology-compliant
+  // hack to make output SZS ontology-compliant
   bool d_hasConjecture;
-  // hack for szs compliance
-  bool d_szsCompliant;
+
+  static void myPopCharStream(pANTLR3_LEXER lexer);
+  void (*d_oldPopCharStream)(pANTLR3_LEXER);
 
 public:
-  bool cnf; //in a cnf formula
 
-  void addFreeVar(Expr var){assert(cnf); d_freeVar.push_back(var); };
-  std::vector< Expr > getFreeVar(){
+  bool cnf; // in a cnf formula
+  bool fof; // in an fof formula
+
+  void addFreeVar(Expr var) {
+    assert(cnf);
+    d_freeVar.push_back(var);
+  }
+  std::vector< Expr > getFreeVar() {
     assert(cnf);
     std::vector< Expr > r;
     r.swap(d_freeVar);
     return r;
   }
 
-  inline Expr convertRatToUnsorted(Expr expr){
+  inline Expr convertRatToUnsorted(Expr expr) {
     ExprManager * em = getExprManager();
 
     // Create the conversion function If they doesn't exists
-    if(d_rtu_op.isNull()){
+    if(d_rtu_op.isNull()) {
       Type t;
-      //Conversion from rational to unsorted
+      // Conversion from rational to unsorted
       t = em->mkFunctionType(em->realType(), d_unsorted);
       d_rtu_op = em->mkVar("$$rtu",t);
       preemptCommand(new DeclareFunctionCommand("$$rtu", d_rtu_op, t));
-      //Conversion from unsorted to rational
+      // Conversion from unsorted to rational
       t = em->mkFunctionType(d_unsorted, em->realType());
       d_utr_op = em->mkVar("$$utr",t);
-      preemptCommand(new DeclareFunctionCommand("$$utur", d_utr_op, t));
+      preemptCommand(new DeclareFunctionCommand("$$utr", d_utr_op, t));
     }
     // Add the inverse in order to show that over the elements that
     // appear in the problem there is a bijection between unsorted and
     // rational
     Expr ret = em->mkExpr(kind::APPLY_UF,d_rtu_op,expr);
-    if ( d_r_converted.find(expr) == d_r_converted.end() ){
+    if(d_r_converted.find(expr) == d_r_converted.end()) {
       d_r_converted.insert(expr);
-      Expr eq = em->mkExpr(kind::EQUAL,expr,
-                           em->mkExpr(kind::APPLY_UF,d_utr_op,ret));
+      Expr eq = em->mkExpr(kind::EQUAL, expr,
+                           em->mkExpr(kind::APPLY_UF, d_utr_op, ret));
       preemptCommand(new AssertCommand(eq));
-    };
+    }
     return ret;
   }
 
@@ -104,12 +111,13 @@ public:
 
 public:
 
-  //TPTP (CNF and FOF) is unsorted so we define this common type
+  // CNF and FOF are unsorted so we define this common type.
+  // This is also the Type of $i in TFF.
   Type d_unsorted;
 
   enum Theory {
     THEORY_CORE,
-  };
+  };/* enum Theory */
 
   enum FormulaRole {
     FR_AXIOM,
@@ -126,8 +134,9 @@ public:
     FR_FI_FUNCTORS,
     FR_FI_PREDICATES,
     FR_TYPE,
-  };
+  };/* enum FormulaRole */
 
+  bool hasConjecture() const { return d_hasConjecture; }
 
 protected:
   Tptp(ExprManager* exprManager, Input* input, bool strictMode = false, bool parseOnly = false);
@@ -140,10 +149,30 @@ public:
    */
   void addTheory(Theory theory);
 
-  inline void makeApplication(Expr & expr, std::string & name,
-                              std::vector<Expr> & args, bool term);
+  inline void makeApplication(Expr& expr, std::string& name,
+                              std::vector<Expr>& args, bool term);
+
+  inline Command* makeCommand(FormulaRole fr, Expr& expr, bool cnf);
+
+  inline Expr mkTffVar(std::string& name, const Type& type) {
+    std::string orig = name;
+    std::stringstream ss;
+    ss << name << "_0";
+    name = ss.str();
+    Expr var = mkVar(name, type);
+    defineFunction(orig, var);
+    return var;
+  }
 
-  inline Command* makeCommand(FormulaRole fr, Expr & expr);
+  inline Expr mkTffFunction(std::string& name, const FunctionType& type) {
+    std::string orig = name;
+    std::stringstream ss;
+    ss << name << "_" << type.getArity();
+    name = ss.str();
+    Expr fun = mkFunction(name, type);
+    defineFunction(orig, fun);
+    return fun;
+  }
 
   /** Ugly hack because I don't know how to return an expression from a
       token */
@@ -153,48 +182,57 @@ public:
       is reused */
   void includeFile(std::string fileName);
 
+  /** Check a TPTP let binding for well-formedness. */
+  void checkLetBinding(std::vector<Expr>& bvlist, Expr lhs, Expr rhs, bool formula);
+
 private:
 
   void addArithmeticOperators();
 };/* class Tptp */
 
-inline void Tptp::makeApplication(Expr & expr, std::string & name,
-                           std::vector<Expr> & args, bool term){
+inline void Tptp::makeApplication(Expr& expr, std::string& name,
+                                  std::vector<Expr>& args, bool term) {
   // We distinguish the symbols according to their arities
   std::stringstream ss;
   ss << name << "_" << args.size();
   name = ss.str();
-  if(args.empty()){ // Its a constant
-    if(isDeclared(name)){ //already appeared
+  if(args.empty()) { // Its a constant
+    if(isDeclared(name)) { // already appeared
       expr = getVariable(name);
     } else {
       Type t = term ? d_unsorted : getExprManager()->booleanType();
-      expr = mkVar(name,t,true); //levelZero
+      expr = mkVar(name, t, true); // levelZero
       preemptCommand(new DeclareFunctionCommand(name, expr, t));
     }
   } else { // Its an application
-    if(isDeclared(name)){ //already appeared
+    if(isDeclared(name)) { // already appeared
       expr = getVariable(name);
     } else {
       std::vector<Type> sorts(args.size(), d_unsorted);
       Type t = term ? d_unsorted : getExprManager()->booleanType();
       t = getExprManager()->mkFunctionType(sorts, t);
-      expr = mkVar(name,t,true); //levelZero
+      expr = mkVar(name, t, true); // levelZero
       preemptCommand(new DeclareFunctionCommand(name, expr, t));
     }
+    // args might be rationals, in which case we need to create
+    // distinct constants of the "unsorted" sort to represent them
+    for(size_t i = 0; i < args.size(); ++i) {
+      if(args[i].getType().isReal() && FunctionType(expr.getType()).getArgTypes()[i] == d_unsorted) {
+        args[i] = convertRatToUnsorted(args[i]);
+      }
+    }
     expr = getExprManager()->mkExpr(kind::APPLY_UF, expr, args);
   }
-};
+}
 
-inline Command* Tptp::makeCommand(FormulaRole fr, Expr & expr){
-  //hack for SZS ontology compliance
-  if(d_szsCompliant && (fr==FR_NEGATED_CONJECTURE || fr==FR_CONJECTURE)){
-    if( !d_hasConjecture ){
-      d_hasConjecture = true;
-      std::cout << "conjecture-";
-    }
+inline Command* Tptp::makeCommand(FormulaRole fr, Expr& expr, bool cnf) {
+  // For SZS ontology compliance.
+  // if we're in cnf() though, conjectures don't result in "Theorem" or
+  // "CounterSatisfiable".
+  if(!cnf && (fr == FR_NEGATED_CONJECTURE || fr == FR_CONJECTURE)) {
+    d_hasConjecture = true;
   }
-  switch(fr){
+  switch(fr) {
   case FR_AXIOM:
   case FR_HYPOTHESIS:
   case FR_DEFINITION:
diff --git a/src/parser/tptp/tptp_input.cpp b/src/parser/tptp/tptp_input.cpp
index 34a620187..bfaeb07c9 100644
--- a/src/parser/tptp/tptp_input.cpp
+++ b/src/parser/tptp/tptp_input.cpp
@@ -28,9 +28,9 @@
 namespace CVC4 {
 namespace parser {
 
-/* Use lookahead=1 */
+/* Use lookahead=2 */
 TptpInput::TptpInput(AntlrInputStream& inputStream) :
-  AntlrInput(inputStream, 1) {
+  AntlrInput(inputStream, 2) {
   pANTLR3_INPUT_STREAM input = inputStream.getAntlr3InputStream();
   assert( input != NULL );
 
diff --git a/src/printer/Makefile.am b/src/printer/Makefile.am
index fd48b8352..cd938088e 100644
--- a/src/printer/Makefile.am
+++ b/src/printer/Makefile.am
@@ -19,7 +19,9 @@ libprinter_la_SOURCES = \
 	smt2/smt2_printer.h \
 	smt2/smt2_printer.cpp \
 	cvc/cvc_printer.h \
-	cvc/cvc_printer.cpp
+	cvc/cvc_printer.cpp \
+	tptp/tptp_printer.h \
+	tptp/tptp_printer.cpp
 
 EXTRA_DIST = \
 	options_handlers.h
diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp
index 344cbfe8c..f9d7c2a38 100644
--- a/src/printer/printer.cpp
+++ b/src/printer/printer.cpp
@@ -20,6 +20,7 @@
 
 #include "printer/smt1/smt1_printer.h"
 #include "printer/smt2/smt2_printer.h"
+#include "printer/tptp/tptp_printer.h"
 #include "printer/cvc/cvc_printer.h"
 #include "printer/ast/ast_printer.h"
 
@@ -41,8 +42,8 @@ Printer* Printer::makePrinter(OutputLanguage lang) throw() {
   case LANG_SMTLIB_V2:
     return new printer::smt2::Smt2Printer();
 
-  case LANG_TPTP: //TODO the printer
-    return new printer::smt2::Smt2Printer();
+  case LANG_TPTP:
+    return new printer::tptp::TptpPrinter();
 
   case LANG_CVC4:
     return new printer::cvc::CvcPrinter();
diff --git a/src/printer/printer.h b/src/printer/printer.h
index 5198a6ef1..d3a9201ee 100644
--- a/src/printer/printer.h
+++ b/src/printer/printer.h
@@ -45,6 +45,11 @@ protected:
   /** write model response to command */
   virtual void toStream(std::ostream& out, const Model& m, const Command* c) const throw() = 0;
 
+  /** write model response to command using another language printer */
+  void toStreamUsing(OutputLanguage lang, std::ostream& out, const Model& m, const Command* c) const throw() {
+    getPrinter(lang)->toStream(out, m, c);
+  }
+
 public:
   /** Get the Printer for a given OutputLanguage */
   static Printer* getPrinter(OutputLanguage lang) throw() {
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 1ab364f0c..76856532f 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -696,7 +696,7 @@ void Smt2Printer::toStream(std::ostream& out, const Model& m, const Command* c)
 }
 
 void Smt2Printer::toStream(std::ostream& out, const Result& r) const throw() {
-  if (r.getType() == Result::TYPE_SAT && r.isSat() == Result::SAT_UNKNOWN) {
+  if(r.getType() == Result::TYPE_SAT && r.isSat() == Result::SAT_UNKNOWN) {
     out << "unknown";
   } else {
     Printer::toStream(out, r);
diff --git a/src/printer/tptp/tptp_printer.cpp b/src/printer/tptp/tptp_printer.cpp
new file mode 100644
index 000000000..ec2a8758b
--- /dev/null
+++ b/src/printer/tptp/tptp_printer.cpp
@@ -0,0 +1,83 @@
+/*********************                                                        */
+/*! \file tptp_printer.cpp
+ ** \verbatim
+ ** Original author: Morgan Deters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief The pretty-printer interface for the TPTP output language
+ **
+ ** The pretty-printer interface for the TPTP output language.
+ **/
+
+#include "printer/tptp/tptp_printer.h"
+#include "expr/expr.h" // for ExprSetDepth etc..
+#include "util/language.h" // for LANG_AST
+#include "expr/node_manager.h" // for VarNameAttr
+#include "expr/command.h"
+
+#include <iostream>
+#include <vector>
+#include <string>
+#include <typeinfo>
+
+using namespace std;
+
+namespace CVC4 {
+namespace printer {
+namespace tptp {
+
+void TptpPrinter::toStream(std::ostream& out, TNode n,
+                           int toDepth, bool types, size_t dag) const throw() {
+  n.toStream(out, toDepth, types, dag, language::output::LANG_SMTLIB_V2);
+}/* TptpPrinter::toStream() */
+
+void TptpPrinter::toStream(std::ostream& out, const Command* c,
+                           int toDepth, bool types, size_t dag) const throw() {
+  c->toStream(out, toDepth, types, dag, language::output::LANG_SMTLIB_V2);
+}/* TptpPrinter::toStream() */
+
+void TptpPrinter::toStream(std::ostream& out, const CommandStatus* s) const throw() {
+  s->toStream(out, language::output::LANG_SMTLIB_V2);
+}/* TptpPrinter::toStream() */
+
+void TptpPrinter::toStream(std::ostream& out, const SExpr& sexpr) const throw() {
+  Printer::getPrinter(language::output::LANG_SMTLIB_V2)->toStream(out, sexpr);
+}/* TptpPrinter::toStream() */
+
+void TptpPrinter::toStream(std::ostream& out, const Model& m) const throw() {
+  out << "% SZS output start FiniteModel for " << m.getInputName() << endl;
+  for(size_t i = 0; i < m.getNumCommands(); ++i) {
+    this->Printer::toStreamUsing(language::output::LANG_SMTLIB_V2, out, m, m.getCommand(i));
+  }
+  out << "% SZS output end FiniteModel for " << m.getInputName() << endl;
+}
+
+void TptpPrinter::toStream(std::ostream& out, const Model& m, const Command* c) const throw() {
+  // shouldn't be called; only the non-Command* version above should be
+  Unreachable();
+}
+
+void TptpPrinter::toStream(std::ostream& out, const Result& r) const throw() {
+  out << "% SZS status ";
+  if(r.isSat() == Result::SAT) {
+    out << "Satisfiable";
+  } else if(r.isSat() == Result::UNSAT) {
+    out << "Unsatisfiable";
+  } else if(r.isValid() == Result::VALID) {
+    out << "Theorem";
+  } else if(r.isValid() == Result::INVALID) {
+    out << "CounterSatisfiable";
+  } else {
+    out << "GaveUp";
+  }
+  out << " for " << r.getInputName();
+}
+
+}/* CVC4::printer::tptp namespace */
+}/* CVC4::printer namespace */
+}/* CVC4 namespace */
diff --git a/src/printer/tptp/tptp_printer.h b/src/printer/tptp/tptp_printer.h
new file mode 100644
index 000000000..a0f3de62b
--- /dev/null
+++ b/src/printer/tptp/tptp_printer.h
@@ -0,0 +1,46 @@
+/*********************                                                        */
+/*! \file tptp_printer.h
+ ** \verbatim
+ ** Original author: Morgan Deters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief The pretty-printer interface for the TPTP output language
+ **
+ ** The pretty-printer interface for the TPTP output language.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__PRINTER__TPTP_PRINTER_H
+#define __CVC4__PRINTER__TPTP_PRINTER_H
+
+#include <iostream>
+
+#include "printer/printer.h"
+
+namespace CVC4 {
+namespace printer {
+namespace tptp {
+
+class TptpPrinter : public CVC4::Printer {
+  void toStream(std::ostream& out, const Model& m, const Command* c) const throw();
+public:
+  using CVC4::Printer::toStream;
+  void toStream(std::ostream& out, TNode n, int toDepth, bool types, size_t dag) const throw();
+  void toStream(std::ostream& out, const Command* c, int toDepth, bool types, size_t dag) const throw();
+  void toStream(std::ostream& out, const CommandStatus* s) const throw();
+  void toStream(std::ostream& out, const SExpr& sexpr) const throw();
+  void toStream(std::ostream& out, const Model& m) const throw();
+  void toStream(std::ostream& out, const Result& r) const throw();
+};/* class TptpPrinter */
+
+}/* CVC4::printer::tptp namespace */
+}/* CVC4::printer namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__PRINTER__TPTP_PRINTER_H */
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 4ee00161f..b72f52092 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1108,13 +1108,15 @@ void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value)
   }
 
   // Check for standard info keys (SMT-LIB v1, SMT-LIB v2, ...)
-  if(key == "name" ||
-     key == "source" ||
+  if(key == "source" ||
      key == "category" ||
      key == "difficulty" ||
      key == "notes") {
     // ignore these
     return;
+  } else if(key == "name") {
+    d_filename = value.getValue();
+    return;
   } else if(key == "smt-lib-version") {
     if( (value.isInteger() && value.getIntegerValue() == Integer(2)) ||
         (value.isRational() && value.getRationalValue() == Rational(2)) ||
@@ -1133,7 +1135,7 @@ void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value)
       throw OptionException("argument to (set-info :status ..) must be "
                             "`sat' or `unsat' or `unknown'");
     }
-    d_status = Result(s);
+    d_status = Result(s, d_filename);
     return;
   }
   throw UnrecognizedOptionException();
@@ -2568,7 +2570,7 @@ Result SmtEngine::check() {
   if(d_timeBudgetCumulative != 0) {
     millis = getTimeRemaining();
     if(millis == 0) {
-      return Result(Result::VALIDITY_UNKNOWN, Result::TIMEOUT);
+      return Result(Result::VALIDITY_UNKNOWN, Result::TIMEOUT, d_filename);
     }
   }
   if(d_timeBudgetPerCall != 0 && (millis == 0 || d_timeBudgetPerCall < millis)) {
@@ -2579,7 +2581,7 @@ Result SmtEngine::check() {
   if(d_resourceBudgetCumulative != 0) {
     resource = getResourceRemaining();
     if(resource == 0) {
-      return Result(Result::VALIDITY_UNKNOWN, Result::RESOURCEOUT);
+      return Result(Result::VALIDITY_UNKNOWN, Result::RESOURCEOUT, d_filename);
     }
   }
   if(d_resourceBudgetPerCall != 0 && (resource == 0 || d_resourceBudgetPerCall < resource)) {
@@ -2600,13 +2602,13 @@ Result SmtEngine::check() {
   Trace("limit") << "SmtEngine::check(): cumulative millis " << d_cumulativeTimeUsed
                  << ", conflicts " << d_cumulativeResourceUsed << endl;
 
-  return result;
+  return Result(result, d_filename);
 }
 
 Result SmtEngine::quickCheck() {
   Assert(d_fullyInited);
   Trace("smt") << "SMT quickCheck()" << endl;
-  return Result(Result::VALIDITY_UNKNOWN, Result::REQUIRES_FULL_CHECK);
+  return Result(Result::VALIDITY_UNKNOWN, Result::REQUIRES_FULL_CHECK, d_filename);
 }
 
 
@@ -3427,7 +3429,9 @@ Model* SmtEngine::getModel() throw(ModalException) {
       "Cannot get model when produce-models options is off.";
     throw ModalException(msg);
   }
-  return d_theoryEngine->getModel();
+  TheoryModel* m = d_theoryEngine->getModel();
+  m->d_inputName = d_filename;
+  return m;
 }
 
 void SmtEngine::checkModel(bool hardFailure) {
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index a45fe3383..552f5cd67 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -234,6 +234,11 @@ class CVC4_PUBLIC SmtEngine {
   Result d_status;
 
   /**
+   * The name of the input (if any).
+   */
+  std::string d_filename;
+
+  /**
    * A private utility class to SmtEngine.
    */
   smt::SmtEnginePrivate* d_private;
diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds
index fca79aff0..6a6fb2e31 100644
--- a/src/theory/builtin/kinds
+++ b/src/theory/builtin/kinds
@@ -300,7 +300,12 @@ operator SEXPR 0: "a symbolic expression"
 
 operator LAMBDA 2 "lambda"
 
-parameterized CHAIN BUILTIN 2: "chain operator"
+parameterized CHAIN CHAIN_OP 2: "chained operator"
+constant CHAIN_OP \
+    ::CVC4::Chain \
+    ::CVC4::ChainHashFunction \
+    "util/chain.h" \
+    "the chained operator"
 
 constant TYPE_CONSTANT \
     ::CVC4::TypeConstant \
@@ -344,6 +349,7 @@ typerule DISTINCT ::CVC4::theory::builtin::DistinctTypeRule
 typerule SEXPR ::CVC4::theory::builtin::SExprTypeRule
 typerule LAMBDA ::CVC4::theory::builtin::LambdaTypeRule
 typerule CHAIN ::CVC4::theory::builtin::ChainTypeRule
+typerule CHAIN_OP ::CVC4::theory::builtin::ChainedOperatorTypeRule
 
 constant SUBTYPE_TYPE \
     ::CVC4::Predicate \
diff --git a/src/theory/builtin/theory_builtin_rewriter.cpp b/src/theory/builtin/theory_builtin_rewriter.cpp
index 4d62ce511..392e146ba 100644
--- a/src/theory/builtin/theory_builtin_rewriter.cpp
+++ b/src/theory/builtin/theory_builtin_rewriter.cpp
@@ -16,6 +16,7 @@
  **/
 
 #include "theory/builtin/theory_builtin_rewriter.h"
+#include "util/chain.h"
 
 using namespace std;
 
@@ -53,7 +54,7 @@ Node TheoryBuiltinRewriter::blastChain(TNode in) {
 
   Assert(in.getKind() == kind::CHAIN);
 
-  Kind chainedOp = in.getOperator().getConst<Kind>();
+  Kind chainedOp = in.getOperator().getConst<Chain>().getOperator();
 
   if(in.getNumChildren() == 2) {
     // if this is the case exactly 1 pair will be generated so the
diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h
index 2a4e07528..a04f9f88a 100644
--- a/src/theory/builtin/theory_builtin_type_rules.h
+++ b/src/theory/builtin/theory_builtin_type_rules.h
@@ -220,6 +220,14 @@ public:
   }
 };/* class ChainTypeRule */
 
+class ChainedOperatorTypeRule {
+public:
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) {
+    Assert(n.getKind() == kind::CHAIN_OP);
+    return nodeManager->getType(nodeManager->operatorOf(n.getConst<Chain>().getOperator()), check);
+  }
+};/* class ChainedOperatorTypeRule */
+
 class SortProperties {
 public:
   inline static bool isWellFounded(TypeNode type) {
diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index 51eb5cb1a..23318b95d 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -77,6 +77,7 @@ libutil_la_SOURCES = \
 	ite_removal.h \
 	ite_removal.cpp \
 	node_visitor.h \
+	chain.h \
 	index.h \
 	uninterpreted_constant.h \
 	uninterpreted_constant.cpp \
@@ -139,7 +140,8 @@ EXTRA_DIST = \
 	rational.i \
 	hash.i \
 	predicate.i \
-	uninterpreted_constant.i
+	uninterpreted_constant.i \
+	chain.i
 
 DISTCLEANFILES = \
 	integer.h.tmp \
diff --git a/src/util/boolean_simplification.h b/src/util/boolean_simplification.h
index e5c4ead6c..be39f69c1 100644
--- a/src/util/boolean_simplification.h
+++ b/src/util/boolean_simplification.h
@@ -22,6 +22,7 @@
 #include <vector>
 #include <algorithm>
 
+#include "expr/expr_manager_scope.h"
 #include "expr/node.h"
 #include "util/cvc4_assert.h"
 
@@ -202,6 +203,7 @@ public:
    * @param e the Expr to negate (cannot be the null Expr)
    */
   static Expr negate(Expr e) throw(AssertionException) {
+    ExprManagerScope ems(e);
     return negate(Node::fromExpr(e)).toExpr();
   }
 
diff --git a/src/util/chain.h b/src/util/chain.h
new file mode 100644
index 000000000..2e9cf7bf6
--- /dev/null
+++ b/src/util/chain.h
@@ -0,0 +1,50 @@
+/*********************                                                        */
+/*! \file chain.h
+ ** \verbatim
+ ** Original author: Morgan Deters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__CHAIN_H
+#define __CVC4__CHAIN_H
+
+#include "expr/kind.h"
+#include <iostream>
+
+namespace CVC4 {
+
+/** A class to represent a chained, built-in operator. */
+class Chain {
+  Kind d_kind;
+public:
+  explicit Chain(Kind k) : d_kind(k) { }
+  bool operator==(const Chain& ch) const { return d_kind == ch.d_kind; }
+  bool operator!=(const Chain& ch) const { return d_kind != ch.d_kind; }
+  Kind getOperator() const { return d_kind; }
+};/* class Chain */
+
+inline std::ostream& operator<<(std::ostream& out, const Chain& ch) {
+  return out << ch.getOperator();
+}
+
+struct ChainHashFunction {
+  size_t operator()(const Chain& ch) const {
+    return kind::KindHashFunction()(ch.getOperator());
+  }
+};/* struct ChainHashFunction */
+
+}/* CVC4 namespace */
+
+#endif  /* __CVC4__CHAIN_H */
diff --git a/src/util/chain.i b/src/util/chain.i
new file mode 100644
index 000000000..1c97a527f
--- /dev/null
+++ b/src/util/chain.i
@@ -0,0 +1,12 @@
+%{
+#include "util/chain.h"
+%}
+
+%rename(equals) CVC4::Chain::operator==(const Chain&) const;
+%ignore CVC4::Chain::operator!=(const Chain&) const;
+
+%ignore CVC4::operator<<(std::ostream&, const Chain&);
+
+%rename(apply) CVC4::ChainHashFunction::operator()(const CVC4::Chain&) const;
+
+%include "util/chain.h"
diff --git a/src/util/result.cpp b/src/util/result.cpp
index e0e34f07d..909a7d8c6 100644
--- a/src/util/result.cpp
+++ b/src/util/result.cpp
@@ -27,11 +27,12 @@ using namespace std;
 
 namespace CVC4 {
 
-Result::Result(const std::string& instr) :
+Result::Result(const std::string& instr, std::string inputName) :
   d_sat(SAT_UNKNOWN),
   d_validity(VALIDITY_UNKNOWN),
   d_which(TYPE_NONE),
-  d_unknownExplanation(UNKNOWN_REASON) {
+  d_unknownExplanation(UNKNOWN_REASON),
+  d_inputName(inputName) {
   string s = instr;
   transform(s.begin(), s.end(), s.begin(), ::tolower);
   if(s == "sat" || s == "satisfiable") {
@@ -115,13 +116,13 @@ Result Result::asSatisfiabilityResult() const throw() {
     switch(d_validity) {
 
     case INVALID:
-      return Result(SAT);
+      return Result(SAT, d_inputName);
 
     case VALID:
-      return Result(UNSAT);
+      return Result(UNSAT, d_inputName);
 
     case VALIDITY_UNKNOWN:
-      return Result(SAT_UNKNOWN, d_unknownExplanation);
+      return Result(SAT_UNKNOWN, d_unknownExplanation, d_inputName);
 
     default:
       Unhandled(d_validity);
@@ -129,7 +130,7 @@ Result Result::asSatisfiabilityResult() const throw() {
   }
 
   // TYPE_NONE
-  return Result(SAT_UNKNOWN, NO_STATUS);
+  return Result(SAT_UNKNOWN, NO_STATUS, d_inputName);
 }
 
 Result Result::asValidityResult() const throw() {
@@ -141,13 +142,13 @@ Result Result::asValidityResult() const throw() {
     switch(d_sat) {
 
     case SAT:
-      return Result(INVALID);
+      return Result(INVALID, d_inputName);
 
     case UNSAT:
-      return Result(VALID);
+      return Result(VALID, d_inputName);
 
     case SAT_UNKNOWN:
-      return Result(VALIDITY_UNKNOWN, d_unknownExplanation);
+      return Result(VALIDITY_UNKNOWN, d_unknownExplanation, d_inputName);
 
     default:
       Unhandled(d_sat);
@@ -155,7 +156,7 @@ Result Result::asValidityResult() const throw() {
   }
 
   // TYPE_NONE
-  return Result(VALIDITY_UNKNOWN, NO_STATUS);
+  return Result(VALIDITY_UNKNOWN, NO_STATUS, d_inputName);
 }
 
 string Result::toString() const {
diff --git a/src/util/result.h b/src/util/result.h
index cb1bd50fa..54ec3a38c 100644
--- a/src/util/result.h
+++ b/src/util/result.h
@@ -71,47 +71,58 @@ private:
   enum Validity d_validity;
   enum Type d_which;
   enum UnknownExplanation d_unknownExplanation;
+  std::string d_inputName;
 
 public:
-  Result() :
+  Result(std::string inputName = "") :
     d_sat(SAT_UNKNOWN),
     d_validity(VALIDITY_UNKNOWN),
     d_which(TYPE_NONE),
-    d_unknownExplanation(UNKNOWN_REASON) {
+    d_unknownExplanation(UNKNOWN_REASON),
+    d_inputName(inputName) {
   }
-  Result(enum Sat s) :
+  Result(enum Sat s, std::string inputName = "") :
     d_sat(s),
     d_validity(VALIDITY_UNKNOWN),
     d_which(TYPE_SAT),
-    d_unknownExplanation(UNKNOWN_REASON) {
+    d_unknownExplanation(UNKNOWN_REASON),
+    d_inputName(inputName) {
     CheckArgument(s != SAT_UNKNOWN,
                   "Must provide a reason for satisfiability being unknown");
   }
-  Result(enum Validity v) :
+  Result(enum Validity v, std::string inputName = "") :
     d_sat(SAT_UNKNOWN),
     d_validity(v),
     d_which(TYPE_VALIDITY),
-    d_unknownExplanation(UNKNOWN_REASON) {
+    d_unknownExplanation(UNKNOWN_REASON),
+    d_inputName(inputName) {
     CheckArgument(v != VALIDITY_UNKNOWN,
                   "Must provide a reason for validity being unknown");
   }
-  Result(enum Sat s, enum UnknownExplanation unknownExplanation) :
+  Result(enum Sat s, enum UnknownExplanation unknownExplanation, std::string inputName = "") :
     d_sat(s),
     d_validity(VALIDITY_UNKNOWN),
     d_which(TYPE_SAT),
-    d_unknownExplanation(unknownExplanation) {
+    d_unknownExplanation(unknownExplanation),
+    d_inputName(inputName) {
     CheckArgument(s == SAT_UNKNOWN,
                   "improper use of unknown-result constructor");
   }
-  Result(enum Validity v, enum UnknownExplanation unknownExplanation) :
+  Result(enum Validity v, enum UnknownExplanation unknownExplanation, std::string inputName = "") :
     d_sat(SAT_UNKNOWN),
     d_validity(v),
     d_which(TYPE_VALIDITY),
-    d_unknownExplanation(unknownExplanation) {
+    d_unknownExplanation(unknownExplanation),
+    d_inputName(inputName) {
     CheckArgument(v == VALIDITY_UNKNOWN,
                   "improper use of unknown-result constructor");
   }
-  Result(const std::string& s);
+  Result(const std::string& s, std::string inputName = "");
+
+  Result(const Result& r, std::string inputName) {
+    *this = r;
+    d_inputName = inputName;
+  }
 
   enum Sat isSat() const {
     return d_which == TYPE_SAT ? d_sat : SAT_UNKNOWN;
@@ -142,6 +153,8 @@ public:
 
   std::string toString() const;
 
+  std::string getInputName() const { return d_inputName; }
+
 };/* class Result */
 
 inline bool Result::operator!=(const Result& r) const throw() {
diff --git a/src/util/util_model.h b/src/util/util_model.h
index 365e7124d..e5bd1f955 100644
--- a/src/util/util_model.h
+++ b/src/util/util_model.h
@@ -33,6 +33,10 @@ std::ostream& operator<<(std::ostream&, const Model&);
 
 class Model {
   friend std::ostream& operator<<(std::ostream&, const Model&);
+  friend class SmtEngine;
+
+  /** the input name (file name, etc.) this model is associated to */
+  std::string d_inputName;
 
 protected:
   /** The SmtEngine we're associated with */
@@ -52,6 +56,8 @@ public:
   SmtEngine* getSmtEngine() { return &d_smt; }
   /** get the smt engine (as a pointer-to-const) that this model is hooked up to */
   const SmtEngine* getSmtEngine() const { return &d_smt; }
+  /** get the input name (file name, etc.) this model is associated to */
+  std::string getInputName() const { return d_inputName; }
 
 public:
   /** get value for expression */
diff --git a/test/Makefile.am b/test/Makefile.am
index 0fdc69e03..1ac00eb82 100644
--- a/test/Makefile.am
+++ b/test/Makefile.am
@@ -51,6 +51,7 @@ subdirs_to_check = \
 	regress/regress0/push-pop/boolean \
 	regress/regress0/precedence \
 	regress/regress0/preprocess \
+	regress/regress0/tptp \
 	regress/regress0/unconstrained \
 	regress/regress0/decision \
 	regress/regress0/fmf \
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index e380f2fc2..b1c15c73a 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -1,5 +1,5 @@
-SUBDIRS = . arith precedence uf uflra uflia bv arrays aufbv auflia datatypes quantifiers rewriterules lemmas push-pop preprocess unconstrained decision fmf
-DIST_SUBDIRS = . arith precedence uf uflra uflia bv arrays aufbv auflia datatypes quantifiers rewriterules lemmas push-pop preprocess unconstrained decision fmf
+SUBDIRS = . arith precedence uf uflra uflia bv arrays aufbv auflia datatypes quantifiers rewriterules lemmas push-pop preprocess tptp unconstrained decision fmf
+DIST_SUBDIRS = . arith precedence uf uflra uflia bv arrays aufbv auflia datatypes quantifiers rewriterules lemmas push-pop preprocess tptp unconstrained decision fmf
 
 BINARY = cvc4
 LOG_COMPILER = @srcdir@/../run_regression
@@ -101,17 +101,7 @@ CVC_TESTS = \
 	print_lambda.cvc
 
 # Regression tests for TPTP inputs
-TPTP_TESTS = \
-	tptp_parser.p \
-	tptp_parser2.p \
-	tptp_parser3.p \
-	tptp_parser4.p \
-	tptp_parser5.p \
-	tptp_parser6.p \
-	tptp_parser7.p \
-	tptp_parser8.p \
-	tptp_parser9.p \
-	tptp_parser10.p
+TPTP_TESTS =
 
 # Regression tests derived from bug reports
 BUG_TESTS = \
diff --git a/test/regress/regress0/tptp/ARI086=1.p b/test/regress/regress0/tptp/ARI086=1.p
new file mode 100644
index 000000000..f6d2fcb28
--- /dev/null
+++ b/test/regress/regress0/tptp/ARI086=1.p
@@ -0,0 +1,32 @@
+%------------------------------------------------------------------------------
+% File     : ARI086=1 : TPTP v5.5.0. Released v5.0.0.
+% Domain   : Arithmetic
+% Problem  : Integer: Sum 2 and 2 is 5
+% Version  : Especial.
+% English  :
+
+% Refs     :
+% Source   : [TPTP]
+% Names    :
+
+% Status   : CounterSatisfiable
+% Rating   : 0.00 v5.2.0, 1.00 v5.0.0
+% Syntax   : Number of formulae    :    1 (   1 unit;   0 type)
+%            Number of atoms       :    1 (   1 equality)
+%            Maximal formula depth :    1 (   1 average)
+%            Number of connectives :    0 (   0   ~;   0   |;   0   &)
+%                                         (   0 <=>;   0  =>;   0  <=;   0 <~>)
+%                                         (   0  ~|;   0  ~&)
+%            Number of type conns  :    0 (   0   >;   0   *;   0   +;   0  <<)
+%            Number of predicates  :    1 (   0 propositional; 2-2 arity)
+%            Number of functors    :    3 (   2 constant; 0-2 arity)
+%            Number of variables   :    0 (   0 sgn;   0   !;   0   ?)
+%            Maximal term depth    :    2 (   2 average)
+%            Arithmetic symbols    :    3 (   0 pred;    1 func;    2 numbers)
+% SPC      : TFF_CSA_EQU_ARI
+
+% Comments :
+%------------------------------------------------------------------------------
+tff(anti_sum_2_2_5,conjecture,
+    ( $sum(2,2) = 5 )).
+%------------------------------------------------------------------------------
diff --git a/test/regress/regress0/tptp/Axioms/BOO004-0.ax b/test/regress/regress0/tptp/Axioms/BOO004-0.ax
new file mode 100644
index 000000000..e02b4c2f8
--- /dev/null
+++ b/test/regress/regress0/tptp/Axioms/BOO004-0.ax
@@ -0,0 +1,48 @@
+%--------------------------------------------------------------------------
+% File     : BOO004-0 : TPTP v5.5.0. Released v1.0.0.
+% Domain   : Boolean Algebra
+% Axioms   : Boolean algebra (equality) axioms
+% Version  : [Ver94] (equality) axioms.
+% English  :
+
+% Refs     : [Ver94] Veroff (1994), Problem Set
+% Source   : [Ver94]
+% Names    :
+
+% Status   : Satisfiable
+% Syntax   : Number of clauses    :    8 (   0 non-Horn;   8 unit;   0 RR)
+%            Number of atoms      :    8 (   8 equality)
+%            Maximal clause size  :    1 (   1 average)
+%            Number of predicates :    1 (   0 propositional; 2-2 arity)
+%            Number of functors   :    5 (   2 constant; 0-2 arity)
+%            Number of variables  :   14 (   0 singleton)
+%            Maximal term depth   :    3 (   2 average)
+% SPC      : 
+
+% Comments :
+%--------------------------------------------------------------------------
+cnf(commutativity_of_add,axiom,
+    ( add(X,Y) = add(Y,X) )).
+
+cnf(commutativity_of_multiply,axiom,
+    ( multiply(X,Y) = multiply(Y,X) )).
+
+cnf(distributivity1,axiom,
+    ( add(X,multiply(Y,Z)) = multiply(add(X,Y),add(X,Z)) )).
+
+cnf(distributivity2,axiom,
+    ( multiply(X,add(Y,Z)) = add(multiply(X,Y),multiply(X,Z)) )).
+
+cnf(additive_id1,axiom,
+    ( add(X,additive_identity) = X )).
+
+cnf(multiplicative_id1,axiom,
+    ( multiply(X,multiplicative_identity) = X )).
+
+cnf(additive_inverse1,axiom,
+    ( add(X,inverse(X)) = multiplicative_identity )).
+
+cnf(multiplicative_inverse1,axiom,
+    ( multiply(X,inverse(X)) = additive_identity )).
+
+%--------------------------------------------------------------------------
diff --git a/test/regress/regress0/tptp/Axioms/SYN000+0.ax b/test/regress/regress0/tptp/Axioms/SYN000+0.ax
new file mode 100644
index 000000000..24ef682b7
--- /dev/null
+++ b/test/regress/regress0/tptp/Axioms/SYN000+0.ax
@@ -0,0 +1,37 @@
+%------------------------------------------------------------------------------
+% File     : SYN000+0 : TPTP v5.5.0. Released v3.6.0.
+% Domain   : Syntactic
+% Axioms   : A simple include file for FOF
+% Version  : Biased.
+% English  :
+
+% Refs     :
+% Source   : [TPTP]
+% Names    :
+
+% Status   : Satisfiable
+% Syntax   : Number of formulae    :    3 (   3 unit)
+%            Number of atoms       :    3 (   0 equality)
+%            Maximal formula depth :    1 (   1 average)
+%            Number of connectives :    0 (   0 ~  ;   0  |;   0  &)
+%                                         (   0 <=>;   0 =>;   0 <=)
+%                                         (   0 <~>;   0 ~|;   0 ~&)
+%            Number of predicates  :    3 (   3 propositional; 0-0 arity)
+%            Number of functors    :    0 (   0 constant; --- arity)
+%            Number of variables   :    0 (   0 singleton;   0 !;   0 ?)
+%            Maximal term depth    :    0 (   0 average)
+% SPC      : 
+
+% Comments :
+%------------------------------------------------------------------------------
+%----Some axioms to include
+fof(ia1,axiom,
+    ia1).
+
+fof(ia2,axiom,
+    ia2).
+
+fof(ia3,axiom,
+    ia3).
+
+%------------------------------------------------------------------------------
diff --git a/test/regress/regress0/tptp/Axioms/SYN000-0.ax b/test/regress/regress0/tptp/Axioms/SYN000-0.ax
new file mode 100644
index 000000000..d67e61aee
--- /dev/null
+++ b/test/regress/regress0/tptp/Axioms/SYN000-0.ax
@@ -0,0 +1,34 @@
+%------------------------------------------------------------------------------
+% File     : SYN000-0 : TPTP v5.5.0. Released v3.6.0.
+% Domain   : Syntactic
+% Axioms   : A simple include file for CNF
+% Version  : Biased.
+% English  :
+
+% Refs     :
+% Source   : [TPTP]
+% Names    :
+
+% Status   : Satisfiable
+% Syntax   : Number of clauses     :    3 (   0 non-Horn;   3 unit;   3 RR)
+%            Number of atoms       :    3 (   0 equality)
+%            Maximal clause size   :    1 (   1 average)
+%            Number of predicates  :    3 (   3 propositional; 0-0 arity)
+%            Number of functors    :    0 (   0 constant; --- arity)
+%            Number of variables   :    0 (   0 singleton)
+%            Maximal term depth    :    0 (   0 average)
+% SPC      : 
+
+% Comments :
+%------------------------------------------------------------------------------
+%----Some axioms to include
+cnf(ia1,axiom,
+    ia1).
+
+cnf(ia2,axiom,
+    ia2).
+
+cnf(ia3,axiom,
+    ia3).
+
+%------------------------------------------------------------------------------
diff --git a/test/regress/regress0/tptp/Axioms/SYN000_0.ax b/test/regress/regress0/tptp/Axioms/SYN000_0.ax
new file mode 100644
index 000000000..acb557ef4
--- /dev/null
+++ b/test/regress/regress0/tptp/Axioms/SYN000_0.ax
@@ -0,0 +1,47 @@
+%------------------------------------------------------------------------------
+% File     : SYN000_0 : TPTP v5.5.0. Released v5.0.0.
+% Domain   : Syntactic
+% Axioms   : A simple include file for TFF
+% Version  : Biased.
+% English  :
+
+% Refs     :
+% Source   : [TPTP]
+% Names    :
+
+% Status   : Satisfiable
+% Syntax   : Number of formulae    :    6 (   6 unit;   3 type)
+%            Number of atoms       :    6 (   0 equality)
+%            Maximal formula depth :    2 (   2 average)
+%            Number of connectives :    0 (   0   ~;   0   |;   0   &)
+%                                         (   0 <=>;   0  =>;   0  <=;   0 <~>)
+%                                         (   0  ~|;   0  ~&)
+%            Number of type conns  :    0 (   0   >;   0   *;   0   +;   0  <<)
+%            Number of predicates  :    4 (   4 propositional; 0-0 arity)
+%            Number of functors    :    0 (   0 constant; --- arity)
+%            Number of variables   :    0 (   0 sgn;   0   !;   0   ?)
+%            Maximal term depth    :    0 (   0 average)
+% SPC      : 
+
+% Comments :
+%------------------------------------------------------------------------------
+%----Some axioms to include
+tff(ia1_type,type,(
+    ia1: $o )).
+
+tff(ia2_type,type,(
+    ia2: $o )).
+
+tff(ia3_type,type,(
+    ia3: $o )).
+
+tff(ia1,axiom,(
+    ia1 )).
+
+tff(ia2,axiom,(
+    ia2 )).
+
+tff(ia3,axiom,(
+    ia3 )).
+
+%------------------------------------------------------------------------------
diff --git a/test/regress/regress0/tptp/BOO003-4.p b/test/regress/regress0/tptp/BOO003-4.p
new file mode 100644
index 000000000..0ea15fefc
--- /dev/null
+++ b/test/regress/regress0/tptp/BOO003-4.p
@@ -0,0 +1,31 @@
+%--------------------------------------------------------------------------
+% File     : BOO003-4 : TPTP v5.5.0. Released v1.1.0.
+% Domain   : Boolean Algebra
+% Problem  : Multiplication is idempotent (X * X = X)
+% Version  : [Ver94] (equality) axioms.
+% English  :
+
+% Refs     : [Ver94] Veroff (1994), Problem Set
+% Source   : [Ver94]
+% Names    : TA [Ver94]
+
+% Status   : Unsatisfiable
+% Rating   : 0.10 v5.5.0, 0.05 v5.4.0, 0.00 v2.1.0, 0.13 v2.0.0
+% Syntax   : Number of clauses     :    9 (   0 non-Horn;   9 unit;   1 RR)
+%            Number of atoms       :    9 (   9 equality)
+%            Maximal clause size   :    1 (   1 average)
+%            Number of predicates  :    1 (   0 propositional; 2-2 arity)
+%            Number of functors    :    6 (   3 constant; 0-2 arity)
+%            Number of variables   :   14 (   0 singleton)
+%            Maximal term depth    :    3 (   2 average)
+% SPC      : CNF_UNS_RFO_PEQ_UEQ
+
+% Comments :
+%--------------------------------------------------------------------------
+%----Include boolean algebra axioms for equality formulation
+include('Axioms/BOO004-0.ax').
+%--------------------------------------------------------------------------
+cnf(prove_a_times_a_is_a,negated_conjecture,
+    (  multiply(a,a) != a )).
+
+%--------------------------------------------------------------------------
diff --git a/test/regress/regress0/tptp/BOO027-1.p b/test/regress/regress0/tptp/BOO027-1.p
new file mode 100644
index 000000000..a3cd4224c
--- /dev/null
+++ b/test/regress/regress0/tptp/BOO027-1.p
@@ -0,0 +1,48 @@
+%--------------------------------------------------------------------------
+% File     : BOO027-1 : TPTP v5.5.0. Released v2.2.0.
+% Domain   : Boolean Algebra
+% Problem  : Independence of self-dual 2-basis.
+% Version  : [MP96] (eqiality) axioms : Especial.
+% English  : Show that half of the self-dual 2-basis in DUAL-BA-3 is not
+%            a basis for Boolean Algebra.
+
+% Refs     : [McC98] McCune (1998), Email to G. Sutcliffe
+%          : [MP96]  McCune & Padmanabhan (1996), Automated Deduction in Eq
+% Source   : [McC98]
+% Names    : DUAL-BA-4 [MP96]
+
+% Status   : Satisfiable
+% Rating   : 0.00 v5.5.0, 0.20 v5.4.0, 0.25 v5.3.0, 0.33 v5.2.0, 0.00 v3.2.0, 0.33 v3.1.0, 0.00 v2.2.1
+% Syntax   : Number of clauses     :    6 (   0 non-Horn;   6 unit;   1 RR)
+%            Number of atoms       :    6 (   6 equality)
+%            Maximal clause size   :    1 (   1 average)
+%            Number of predicates  :    1 (   0 propositional; 2-2 arity)
+%            Number of functors    :    5 (   2 constant; 0-2 arity)
+%            Number of variables   :   10 (   0 singleton)
+%            Maximal term depth    :    5 (   3 average)
+% SPC      : CNF_SAT_RFO_PEQ_UEQ
+
+% Comments : There is a 2-element model.
+%--------------------------------------------------------------------------
+%----Two properties of Boolean algebra:
+cnf(multiply_add_property,axiom,
+    ( multiply(X,add(Y,Z)) = add(multiply(Y,X),multiply(Z,X)) )).
+
+cnf(additive_inverse,axiom,
+    ( add(X,inverse(X)) = one )).
+
+%----Pixley properties:
+cnf(pixley1,axiom,
+    ( add(multiply(X,inverse(X)),add(multiply(X,Y),multiply(inverse(X),Y))) = Y )).
+
+cnf(pixley2,axiom,
+    ( add(multiply(X,inverse(Y)),add(multiply(X,Y),multiply(inverse(Y),Y))) = X )).
+
+cnf(pixley3,axiom,
+    ( add(multiply(X,inverse(Y)),add(multiply(X,X),multiply(inverse(Y),X))) = X )).
+
+%----Denial of a property of Boolean Algebra:
+cnf(prove_idempotence,negated_conjecture,
+    (  add(a,a) != a )).
+
+%--------------------------------------------------------------------------
diff --git a/test/regress/regress0/tptp/DAT001=1.p b/test/regress/regress0/tptp/DAT001=1.p
new file mode 100644
index 000000000..922a6cfc3
--- /dev/null
+++ b/test/regress/regress0/tptp/DAT001=1.p
@@ -0,0 +1,57 @@
+%------------------------------------------------------------------------------
+% File     : DAT001=1 : TPTP v5.5.0. Released v5.0.0.
+% Domain   : Data Structures
+% Problem  : Recursive list sort
+% Version  : Especial.
+% English  : 
+
+% Refs     : 
+% Source   : [TPTP]
+% Names    :
+
+% Status   : Theorem
+% Rating   : 0.12 v5.5.0, 0.25 v5.4.0, 0.38 v5.3.0, 0.29 v5.2.0, 0.20 v5.1.0, 0.25 v5.0.0
+% Syntax   : Number of formulae    :    8 (   5 unit;   4 type)
+%            Number of atoms       :   13 (   0 equality)
+%            Maximal formula depth :    6 (   3 average)
+%            Number of connectives :    2 (   0   ~;   0   |;   1   &)
+%                                         (   0 <=>;   1  =>;   0  <=;   0 <~>)
+%                                         (   0  ~|;   0  ~&)
+%            Number of type conns  :    3 (   2   >;   1   *;   0   +;   0  <<)
+%            Number of predicates  :    9 (   7 propositional; 0-2 arity)
+%            Number of functors    :    7 (   6 constant; 0-2 arity)
+%            Number of variables   :    4 (   0 sgn;   4   !;   0   ?)
+%            Maximal term depth    :    6 (   2 average)
+%            Arithmetic symbols    :    7 (   2 pred;    0 func;    5 numbers)
+% SPC      : TFF_THM_NEQ_ARI
+
+% Comments :
+%------------------------------------------------------------------------------
+tff(list_type,type,(
+    list: $tType )).
+
+tff(nil_type,type,(
+    nil: list )).
+
+tff(mycons_type,type,(
+    mycons: ( $int * list ) > list )).
+
+tff(sorted_type,type,(
+    sorted: list > $o )).
+
+tff(empty_is_sorted,axiom,(
+    sorted(nil) )).
+
+tff(single_is_sorted,axiom,(
+    ! [X: $int] : sorted(mycons(X,nil)) )).
+
+tff(recursive_sort,axiom,(
+    ! [X: $int,Y: $int,R: list] :
+      ( ( $less(X,Y)
+        & sorted(mycons(Y,R)) )
+     => sorted(mycons(X,mycons(Y,R))) ) )).
+
+tff(check_list,conjecture,(
+    sorted(mycons(1,mycons(2,mycons(4,mycons(7,mycons(100,nil)))))) )).
+
+%------------------------------------------------------------------------------
diff --git a/test/regress/regress0/tptp/KRS018+1.p b/test/regress/regress0/tptp/KRS018+1.p
new file mode 100644
index 000000000..91039877b
--- /dev/null
+++ b/test/regress/regress0/tptp/KRS018+1.p
@@ -0,0 +1,55 @@
+%------------------------------------------------------------------------------
+% File     : KRS018+1 : TPTP v5.5.0. Released v3.1.0.
+% Domain   : Knowledge Representation (Semantic Web)
+% Problem  : Nothing can be defined using OWL Lite restrictions
+% Version  : Especial.
+% English  :
+
+% Refs     : [Bec03] Bechhofer (2003), Email to G. Sutcliffe
+%          : [TR+04] Tsarkov et al. (2004), Using Vampire to Reason with OW
+% Source   : [Bec03]
+% Names    : consistent_I5.2-Manifest001 [Bec03]
+
+% Status   : Satisfiable
+% Rating   : 0.00 v4.1.0, 0.25 v4.0.1, 0.00 v3.1.0
+% Syntax   : Number of formulae    :    4 (   0 unit)
+%            Number of atoms       :    8 (   0 equality)
+%            Maximal formula depth :    5 (   4 average)
+%            Number of connectives :    7 (   3 ~  ;   0  |;   1  &)
+%                                         (   1 <=>;   2 =>;   0 <=)
+%                                         (   0 <~>;   0 ~|;   0 ~&)
+%            Number of predicates  :    6 (   0 propositional; 1-2 arity)
+%            Number of functors    :    0 (   0 constant; --- arity)
+%            Number of variables   :    6 (   0 singleton;   4 !;   2 ?)
+%            Maximal term depth    :    1 (   1 average)
+% SPC      : FOF_SAT_RFO_NEQ
+
+% Comments : Sean Bechhofer says there are some errors in the encoding of
+%            datatypes, so this problem may not be perfect. At least it's
+%            still representative of the type of reasoning required for OWL.
+%------------------------------------------------------------------------------
+%----Thing and Nothing
+fof(axiom_0,axiom,
+    ( ! [X] :
+        ( cowlThing(X)
+        & ~ cowlNothing(X) ) )).
+
+%----String and Integer disjoint
+fof(axiom_1,axiom,
+    ( ! [X] :
+        ( xsd_string(X)
+      <=> ~ xsd_integer(X) ) )).
+
+%----Super cNothing
+fof(axiom_2,axiom,
+    ( ! [X] :
+        ( cNothing(X)
+       => ~ ( ? [Y] : rp(X,Y) ) ) )).
+
+%----Super cNothing
+fof(axiom_3,axiom,
+    ( ! [X] :
+        ( cNothing(X)
+       => ? [Y0] : rp(X,Y0) ) )).
+
+%------------------------------------------------------------------------------
diff --git a/test/regress/regress0/tptp/KRS063+1.p b/test/regress/regress0/tptp/KRS063+1.p
new file mode 100644
index 000000000..737741dee
--- /dev/null
+++ b/test/regress/regress0/tptp/KRS063+1.p
@@ -0,0 +1,181 @@
+%------------------------------------------------------------------------------
+% File     : KRS063+1 : TPTP v5.5.0. Released v3.1.0.
+% Domain   : Knowledge Representation (Semantic Web)
+% Problem  : An example combining owl:oneOf and owl:inverseOf
+% Version  : Especial.
+% English  :
+
+% Refs     : [Bec03] Bechhofer (2003), Email to G. Sutcliffe
+%          : [TR+04] Tsarkov et al. (2004), Using Vampire to Reason with OW
+% Source   : [Bec03]
+% Names    : inconsistent_I4.5-Manifest002 [Bec03]
+
+% Status   : Unsatisfiable
+% Rating   : 0.00 v3.1.0
+% Syntax   : Number of formulae    :   27 (   9 unit)
+%            Number of atoms       :   63 (  18 equality)
+%            Maximal formula depth :    8 (   4 average)
+%            Number of connectives :   39 (   3 ~  ;   5  |;  14  &)
+%                                         (   4 <=>;  13 =>;   0 <=)
+%                                         (   0 <~>;   0 ~|;   0 ~&)
+%            Number of predicates  :   11 (   0 propositional; 1-2 arity)
+%            Number of functors    :    7 (   7 constant; 0-0 arity)
+%            Number of variables   :   37 (   0 singleton;  36 !;   1 ?)
+%            Maximal term depth    :    1 (   1 average)
+% SPC      : FOF_UNS_RFO_SEQ
+
+% Comments : Sean Bechhofer says there are some errors in the encoding of
+%            datatypes, so this problem may not be perfect. At least it's
+%            still representative of the type of reasoning required for OWL.
+%------------------------------------------------------------------------------
+fof(cEUCountry_substitution_1,axiom,
+    ( ! [A,B] :
+        ( ( A = B
+          & cEUCountry(A) )
+       => cEUCountry(B) ) )).
+
+fof(cEuroMP_substitution_1,axiom,
+    ( ! [A,B] :
+        ( ( A = B
+          & cEuroMP(A) )
+       => cEuroMP(B) ) )).
+
+fof(cEuropeanCountry_substitution_1,axiom,
+    ( ! [A,B] :
+        ( ( A = B
+          & cEuropeanCountry(A) )
+       => cEuropeanCountry(B) ) )).
+
+fof(cPerson_substitution_1,axiom,
+    ( ! [A,B] :
+        ( ( A = B
+          & cPerson(A) )
+       => cPerson(B) ) )).
+
+fof(cowlNothing_substitution_1,axiom,
+    ( ! [A,B] :
+        ( ( A = B
+          & cowlNothing(A) )
+       => cowlNothing(B) ) )).
+
+fof(cowlThing_substitution_1,axiom,
+    ( ! [A,B] :
+        ( ( A = B
+          & cowlThing(A) )
+       => cowlThing(B) ) )).
+
+fof(rhasEuroMP_substitution_1,axiom,
+    ( ! [A,B,C] :
+        ( ( A = B
+          & rhasEuroMP(A,C) )
+       => rhasEuroMP(B,C) ) )).
+
+fof(rhasEuroMP_substitution_2,axiom,
+    ( ! [A,B,C] :
+        ( ( A = B
+          & rhasEuroMP(C,A) )
+       => rhasEuroMP(C,B) ) )).
+
+fof(risEuroMPFrom_substitution_1,axiom,
+    ( ! [A,B,C] :
+        ( ( A = B
+          & risEuroMPFrom(A,C) )
+       => risEuroMPFrom(B,C) ) )).
+
+fof(risEuroMPFrom_substitution_2,axiom,
+    ( ! [A,B,C] :
+        ( ( A = B
+          & risEuroMPFrom(C,A) )
+       => risEuroMPFrom(C,B) ) )).
+
+fof(xsd_integer_substitution_1,axiom,
+    ( ! [A,B] :
+        ( ( A = B
+          & xsd_integer(A) )
+       => xsd_integer(B) ) )).
+
+fof(xsd_string_substitution_1,axiom,
+    ( ! [A,B] :
+        ( ( A = B
+          & xsd_string(A) )
+       => xsd_string(B) ) )).
+
+%----Thing and Nothing
+fof(axiom_0,axiom,
+    ( ! [X] :
+        ( cowlThing(X)
+        & ~ cowlNothing(X) ) )).
+
+%----String and Integer disjoint
+fof(axiom_1,axiom,
+    ( ! [X] :
+        ( xsd_string(X)
+      <=> ~ xsd_integer(X) ) )).
+
+%----Enumeration cEUCountry
+fof(axiom_2,axiom,
+    ( ! [X] :
+        ( cEUCountry(X)
+      <=> ( X = iPT
+          | X = iBE
+          | X = iNL
+          | X = iES
+          | X = iFR
+          | X = iUK ) ) )).
+
+%----Equality cEuroMP
+fof(axiom_3,axiom,
+    ( ! [X] :
+        ( cEuroMP(X)
+      <=> ? [Y] :
+            ( risEuroMPFrom(X,Y)
+            & cowlThing(Y) ) ) )).
+
+%----Domain: rhasEuroMP
+fof(axiom_4,axiom,
+    ( ! [X,Y] :
+        ( rhasEuroMP(X,Y)
+       => cEUCountry(X) ) )).
+
+%----Inverse: risEuroMPFrom
+fof(axiom_5,axiom,
+    ( ! [X,Y] :
+        ( risEuroMPFrom(X,Y)
+      <=> rhasEuroMP(Y,X) ) )).
+
+%----iBE
+fof(axiom_6,axiom,
+    ( cEuropeanCountry(iBE) )).
+
+%----iES
+fof(axiom_7,axiom,
+    ( cEuropeanCountry(iES) )).
+
+%----iFR
+fof(axiom_8,axiom,
+    ( cEuropeanCountry(iFR) )).
+
+%----iKinnock
+fof(axiom_9,axiom,
+    ( cPerson(iKinnock) )).
+
+%----iKinnock
+fof(axiom_10,axiom,
+    ( ~ cEuroMP(iKinnock) )).
+
+%----iNL
+fof(axiom_11,axiom,
+    ( cEuropeanCountry(iNL) )).
+
+%----iPT
+fof(axiom_12,axiom,
+    ( cEuropeanCountry(iPT) )).
+
+%----iUK
+fof(axiom_13,axiom,
+    ( cEuropeanCountry(iUK) )).
+
+fof(axiom_14,axiom,
+    ( rhasEuroMP(iUK,iKinnock) )).
+
+%------------------------------------------------------------------------------
diff --git a/test/regress/regress0/tptp/MGT019+2.p b/test/regress/regress0/tptp/MGT019+2.p
new file mode 100644
index 000000000..fb2cd7f62
--- /dev/null
+++ b/test/regress/regress0/tptp/MGT019+2.p
@@ -0,0 +1,84 @@
+%--------------------------------------------------------------------------
+% File     : MGT019+2 : TPTP v5.5.0. Released v2.0.0.
+% Domain   : Management (Organisation Theory)
+% Problem  : Growth rate of EPs exceeds that of FMs in stable environments
+% Version  : [PM93] axioms.
+% English  : The growth rate of efficent producers exceeds the growth rate
+%            of first movers past a certain time in stable environments.
+
+% Refs     : [PM93]  Peli & Masuch (1993), The Logic of Propogation Strateg
+%          : [PM94]  Peli & Masuch (1994), The Logic of Propogation Strateg
+%          : [PB+94] Peli et al. (1994), A Logical Approach to Formalizing
+% Source   : [PM93]
+% Names    : LEMMA 1 [PM93]
+%          : L1 [PB+94]
+
+% Status   : CounterSatisfiable
+% Rating   : 0.00 v4.1.0, 0.20 v4.0.1, 0.00 v3.5.0, 0.33 v3.4.0, 0.00 v2.1.0
+% Syntax   : Number of formulae    :    5 (   0 unit)
+%            Number of atoms       :   21 (   1 equality)
+%            Maximal formula depth :    8 (   6 average)
+%            Number of connectives :   17 (   1 ~  ;   1  |;   8  &)
+%                                         (   0 <=>;   7 =>;   0 <=)
+%                                         (   0 <~>;   0 ~|;   0 ~&)
+%            Number of predicates  :    7 (   0 propositional; 1-4 arity)
+%            Number of functors    :    5 (   2 constant; 0-2 arity)
+%            Number of variables   :   11 (   0 singleton;   9 !;   2 ?)
+%            Maximal term depth    :    2 (   1 average)
+% SPC      : FOF_CSA_RFO_SEQ
+
+% Comments : There is no MGT019+1 as Kamps did not send it to me.
+%--------------------------------------------------------------------------
+%----Subsitution axioms
+%----Problem axioms
+%----L2. The disbanding rate of first movers exceeds the disbanding
+%----rate of efficient producers.
+fof(l2,axiom,
+    ( ~ ( ! [E,T] :
+            ( ( environment(E)
+              & subpopulations(first_movers,efficient_producers,E,T) )
+           => greater(disbanding_rate(first_movers,T),disbanding_rate(efficient_producers,T)) ) ) )).
+
+%----If EP have lower disbanding rate and not lower founding rate than
+%----FM, then EP have higher growth rate.
+fof(mp_EP_lower_disbanding_rate,axiom,
+    ( ! [T] :
+        ( ( greater(disbanding_rate(first_movers,T),disbanding_rate(efficient_producers,T))
+          & greater_or_equal(founding_rate(efficient_producers,T),founding_rate(first_movers,T)) )
+       => greater(growth_rate(efficient_producers,T),growth_rate(first_movers,T)) ) )).
+
+%----MP. on "greater or equal to"
+fof(mp_greater_or_equal,axiom,
+    ( ! [X,Y] :
+        ( greater_or_equal(X,Y)
+       => ( greater(X,Y)
+          | X = Y ) ) )).
+
+%----A8.  The founding rate of first movers does not exceed the founding
+%----rate of efficient producers past a certain point in a stable
+%----environment.
+fof(a8,hypothesis,
+    ( ! [E] :
+        ( ( environment(E)
+          & stable(E) )
+       => ? [To] :
+            ( in_environment(E,To)
+            & ! [T] :
+                ( ( subpopulations(first_movers,efficient_producers,E,T)
+                  & greater_or_equal(T,To) )
+               => greater_or_equal(founding_rate(efficient_producers,T),founding_rate(first_movers,T)) ) ) ) )).
+
+%----GOAL: L1. The growth rate of efficient producers exceeds the growth
+%----rate of first movers past a certain time in stable environments.
+fof(prove_l1,conjecture,
+    ( ! [E] :
+        ( ( environment(E)
+          & stable(E) )
+       => ? [To] :
+            ( in_environment(E,To)
+            & ! [T] :
+                ( ( subpopulations(first_movers,efficient_producers,E,T)
+                  & greater_or_equal(T,To) )
+               => greater(growth_rate(efficient_producers,T),growth_rate(first_movers,T)) ) ) ) )).
+
+%--------------------------------------------------------------------------
diff --git a/test/regress/regress0/tptp/MGT031-1.p b/test/regress/regress0/tptp/MGT031-1.p
new file mode 100644
index 000000000..f5cd1937e
--- /dev/null
+++ b/test/regress/regress0/tptp/MGT031-1.p
@@ -0,0 +1,95 @@
+%--------------------------------------------------------------------------
+% File     : MGT031-1 : TPTP v5.5.0. Released v2.4.0.
+% Domain   : Management (Organisation Theory)
+% Problem  : First movers appear first in an environment
+% Version  : [PB+94] axioms : Reduced & Augmented > Complete.
+% English  :
+
+% Refs     : [PM93]  Peli & Masuch (1993), The Logic of Propogation Strateg
+%          : [PM94]  Peli & Masuch (1994), The Logic of Propogation Strateg
+%          : [Kam95] Kamps (1995), Email to G. Sutcliffe
+% Source   : [TPTP]
+% Names    :
+
+% Status   : Satisfiable
+% Rating   : 0.00 v2.5.0, 0.17 v2.4.0
+% Syntax   : Number of clauses     :   15 (   2 non-Horn;   3 unit;  15 RR)
+%            Number of atoms       :   38 (   5 equality)
+%            Maximal clause size   :    5 (   3 average)
+%            Number of predicates  :    6 (   0 propositional; 1-3 arity)
+%            Number of functors    :   10 (   6 constant; 0-2 arity)
+%            Number of variables   :   23 (   0 singleton)
+%            Maximal term depth    :    3 (   1 average)
+% SPC      : CNF_SAT_RFO_EQU_NUE
+
+% Comments : Created with tptp2X -f tptp -t clausify:otter MGT031+1.p
+%--------------------------------------------------------------------------
+cnf(mp_positive_number_when_appear_20,axiom,
+    ( ~ environment(A)
+    | greater(number_of_organizations(e,appear(an_organisation,A)),zero) )).
+
+cnf(mp_number_mean_non_empty_21,axiom,
+    ( ~ environment(A)
+    | ~ greater(number_of_organizations(A,B),zero)
+    | subpopulation(sk1(B,A),A,B) )).
+
+cnf(mp_number_mean_non_empty_22,axiom,
+    ( ~ environment(A)
+    | ~ greater(number_of_organizations(A,B),zero)
+    | greater(cardinality_at_time(sk1(B,A),B),zero) )).
+
+cnf(mp_no_EP_before_appearance_23,axiom,
+    ( ~ environment(A)
+    | ~ in_environment(A,B)
+    | ~ greater(appear(efficient_producers,A),B)
+    | ~ greater(cardinality_at_time(efficient_producers,B),zero) )).
+
+cnf(mp_no_FM_before_appearance_24,axiom,
+    ( ~ environment(A)
+    | ~ in_environment(A,B)
+    | ~ greater(appear(first_movers,A),B)
+    | ~ greater(cardinality_at_time(first_movers,B),zero) )).
+
+cnf(mp_FM_not_precede_first_25,axiom,
+    ( ~ environment(A)
+    | greater_or_equal(appear(first_movers,A),appear(an_organisation,A)) )).
+
+cnf(mp_greater_transitivity_26,axiom,
+    ( ~ greater(A,B)
+    | ~ greater(B,C)
+    | greater(A,C) )).
+
+cnf(mp_greater_or_equal_27,axiom,
+    ( ~ greater_or_equal(A,B)
+    | greater(A,B)
+    | A = B )).
+
+cnf(mp_greater_or_equal_28,axiom,
+    ( ~ greater(A,B)
+    | greater_or_equal(A,B) )).
+
+cnf(mp_greater_or_equal_29,axiom,
+    ( A != B
+    | greater_or_equal(A,B) )).
+
+cnf(a9_30,hypothesis,
+    ( ~ environment(A)
+    | ~ subpopulation(B,A,C)
+    | ~ greater(cardinality_at_time(B,C),zero)
+    | B = efficient_producers
+    | B = first_movers )).
+
+cnf(a13_31,hypothesis,
+    ( ~ environment(A)
+    | greater(appear(efficient_producers,e),appear(first_movers,A)) )).
+
+cnf(prove_l13_32,negated_conjecture,
+    ( environment(sk2) )).
+
+cnf(prove_l13_33,negated_conjecture,
+    ( in_environment(sk2,appear(an_organisation,sk2)) )).
+
+cnf(prove_l13_34,negated_conjecture,
+    (  appear(an_organisation,sk2) != appear(first_movers,sk2) )).
+
+%--------------------------------------------------------------------------
diff --git a/test/regress/regress0/tptp/MGT041-2.p b/test/regress/regress0/tptp/MGT041-2.p
new file mode 100644
index 000000000..a10a2f42d
--- /dev/null
+++ b/test/regress/regress0/tptp/MGT041-2.p
@@ -0,0 +1,61 @@
+%--------------------------------------------------------------------------
+% File     : MGT041-2 : TPTP v5.5.0. Released v2.4.0.
+% Domain   : Management (Organisation Theory)
+% Problem  : There are non-FM and non-EP organisations
+% Version  : [PM93] axioms.
+% English  : There are non-first mover and non-efficient producers
+%            organisations.
+
+% Refs     : [PM93]  Peli & Masuch (1993), The Logic of Propogation Strateg
+%          : [PM94]  Peli & Masuch (1994), The Logic of Propogation Strateg
+%          : [Kam95] Kamps (1995), Email to G. Sutcliffe
+% Source   : [TPTP]
+% Names    :
+
+% Status   : Unsatisfiable
+% Rating   : 0.00 v2.4.0
+% Syntax   : Number of clauses     :    8 (   1 non-Horn;   4 unit;   8 RR)
+%            Number of atoms       :   17 (   0 equality)
+%            Maximal clause size   :    4 (   2 average)
+%            Number of predicates  :    6 (   0 propositional; 1-3 arity)
+%            Number of functors    :    4 (   4 constant; 0-0 arity)
+%            Number of variables   :    8 (   1 singleton)
+%            Maximal term depth    :    1 (   1 average)
+% SPC      : CNF_UNS_EPR
+
+% Comments : Created with tptp2X -f tptp -t clausify:otter MGT041+2.p
+%--------------------------------------------------------------------------
+cnf(mp_not_high_and_low_1,axiom,
+    ( ~ number_of_routines(A,B,low)
+    | ~ number_of_routines(A,B,high) )).
+
+cnf(a14_2,hypothesis,
+    ( ~ organisation_at_time(A,B)
+    | ~ efficient_producer(A)
+    | ~ founding_time(A,B)
+    | has_elaborated_routines(A,B) )).
+
+cnf(a15_3,hypothesis,
+    ( ~ organisation_at_time(A,B)
+    | ~ first_mover(A)
+    | ~ founding_time(A,B)
+    | number_of_routines(A,B,low) )).
+
+cnf(a16_4,hypothesis,
+    ( organisation_at_time(sk1,sk2) )).
+
+cnf(a16_5,hypothesis,
+    ( founding_time(sk1,sk2) )).
+
+cnf(a16_6,hypothesis,
+    ( number_of_routines(sk1,sk2,high) )).
+
+cnf(a16_7,hypothesis,
+    ( ~ has_elaborated_routines(sk1,sk2) )).
+
+cnf(prove_t10_8,negated_conjecture,
+    ( ~ organisation_at_time(A,B)
+    | first_mover(A)
+    | efficient_producer(A) )).
+
+%--------------------------------------------------------------------------
diff --git a/test/regress/regress0/tptp/Makefile b/test/regress/regress0/tptp/Makefile
new file mode 100644
index 000000000..8c3909592
--- /dev/null
+++ b/test/regress/regress0/tptp/Makefile
@@ -0,0 +1,8 @@
+topdir = ../../../..
+srcdir = test/regress/regress0/tptp
+
+include $(topdir)/Makefile.subdir
+
+# synonyms for "check"
+.PHONY: test
+test: check
diff --git a/test/regress/regress0/tptp/Makefile.am b/test/regress/regress0/tptp/Makefile.am
new file mode 100644
index 000000000..130a9dc7c
--- /dev/null
+++ b/test/regress/regress0/tptp/Makefile.am
@@ -0,0 +1,79 @@
+BINARY = cvc4
+LOG_COMPILER = @srcdir@/../../run_regression
+AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT)
+
+if AUTOMAKE_1_11
+# old-style (pre-automake 1.12) test harness
+TESTS_ENVIRONMENT = \
+	$(TESTS_ENVIRONMENT) $(LOG_COMPILER) \
+	$(AM_LOG_FLAGS) $(LOG_FLAGS)
+endif
+
+# escape the `=' in file names
+equals = =
+
+# These are run for all build profiles.
+# If a test shouldn't be run in e.g. competition mode,
+# put it below in "TESTS +="
+TESTS =	\
+	tptp_parser.p \
+	tptp_parser2.p \
+	tptp_parser3.p \
+	tptp_parser4.p \
+	tptp_parser5.p \
+	tptp_parser6.p \
+	tptp_parser7.p \
+	tptp_parser8.p \
+	tptp_parser9.p \
+	tptp_parser10.p \
+	tff0.p \
+	tff0-arith.p \
+	ARI086$(equals)1.p \
+	BOO003-4.p \
+	DAT001$(equals)1.p \
+	KRS018+1.p \
+	KRS063+1.p \
+	MGT019+2.p \
+	MGT041-2.p \
+	PUZ131_1.p \
+	SYN000+1.p \
+	SYN000+2.p \
+	SYN000-1.p \
+	SYN000-2.p \
+	SYN000$(equals)2.p \
+	SYN000_1.p \
+	SYN000_2.p \
+	SYN075-1.p
+
+# axiom files required for the above tests
+TEST_DEPS_DIST = \
+	Axioms/BOO004-0.ax \
+	Axioms/SYN000_0.ax \
+	Axioms/SYN000-0.ax \
+	Axioms/SYN000+0.ax
+
+# these take too long at present
+EXTRA_DIST = $(TESTS) \
+	$(TEST_DEPS_DIST) \
+	BOO027-1.p \
+	MGT031-1.p \
+	NLP114-1.p \
+	SYN075+1.p
+
+#if CVC4_BUILD_PROFILE_COMPETITION
+#else
+#TESTS += \
+#	error.cvc
+#endif
+#
+# and make sure to distribute it
+#EXTRA_DIST += \
+#	error.cvc
+
+# synonyms for "check"
+.PHONY: regress regress0 test
+regress regress0 test: check
+
+# do nothing in this subdir
+.PHONY: regress1 regress2 regress3
+regress1 regress2 regress3:
diff --git a/test/regress/regress0/tptp/NLP114-1.p b/test/regress/regress0/tptp/NLP114-1.p
new file mode 100644
index 000000000..cf5bd272a
--- /dev/null
+++ b/test/regress/regress0/tptp/NLP114-1.p
@@ -0,0 +1,202 @@
+%--------------------------------------------------------------------------
+% File     : NLP114-1 : TPTP v5.5.0. Released v2.4.0.
+% Domain   : Natural Language Processing
+% Problem  : An old dirty white Chevy, problem 1
+% Version  : [Bos00b] axioms.
+% English  : Eliminating logically equivalent interpretations in the statement
+%            "An old dirty white chevy barrels down a lonely street in
+%            hollywood."
+
+% Refs     : [Bos00a] Bos (2000), DORIS: Discourse Oriented Representation a
+%            [Bos00b] Bos (2000), Applied Theorem Proving - Natural Language
+% Source   : [TPTP]
+% Names    :
+
+% Status   : Satisfiable
+% Rating   : 0.00 v2.4.0
+% Syntax   : Number of clauses     :   36 (  16 non-Horn;   2 unit;  36 RR)
+%            Number of atoms       :  102 (   0 equality)
+%            Maximal clause size   :   18 (   3 average)
+%            Number of predicates  :   18 (   1 propositional; 0-3 arity)
+%            Number of functors    :   11 (  11 constant; 0-0 arity)
+%            Number of variables   :   11 (   0 singleton)
+%            Maximal term depth    :    1 (   1 average)
+% SPC      : CNF_SAT_EPR
+
+% Comments : Created from NLP114+1.p using FLOTTER
+%--------------------------------------------------------------------------
+cnf(clause1,negated_conjecture,
+    ( actual_world(skc17) )).
+
+cnf(clause2,negated_conjecture,
+    ( actual_world(skc11) )).
+
+cnf(clause3,negated_conjecture,
+    ( ssSkC0
+    | city(skc17,skc20) )).
+
+cnf(clause4,negated_conjecture,
+    ( ssSkC0
+    | street(skc17,skc20) )).
+
+cnf(clause5,negated_conjecture,
+    ( ssSkC0
+    | lonely(skc17,skc20) )).
+
+cnf(clause6,negated_conjecture,
+    ( ssSkC0
+    | placename(skc17,skc21) )).
+
+cnf(clause7,negated_conjecture,
+    ( ssSkC0
+    | hollywood_placename(skc17,skc21) )).
+
+cnf(clause8,negated_conjecture,
+    ( ssSkC0
+    | event(skc17,skc18) )).
+
+cnf(clause9,negated_conjecture,
+    ( ssSkC0
+    | present(skc17,skc18) )).
+
+cnf(clause10,negated_conjecture,
+    ( ssSkC0
+    | barrel(skc17,skc18) )).
+
+cnf(clause11,negated_conjecture,
+    ( ssSkC0
+    | old(skc17,skc19) )).
+
+cnf(clause12,negated_conjecture,
+    ( ssSkC0
+    | dirty(skc17,skc19) )).
+
+cnf(clause13,negated_conjecture,
+    ( ssSkC0
+    | white(skc17,skc19) )).
+
+cnf(clause14,negated_conjecture,
+    ( ssSkC0
+    | chevy(skc17,skc19) )).
+
+cnf(clause15,negated_conjecture,
+    ( ~ ssSkC0
+    | lonely(skc11,skc16) )).
+
+cnf(clause16,negated_conjecture,
+    ( ~ ssSkC0
+    | street(skc11,skc16) )).
+
+cnf(clause17,negated_conjecture,
+    ( ~ ssSkC0
+    | barrel(skc11,skc12) )).
+
+cnf(clause18,negated_conjecture,
+    ( ~ ssSkC0
+    | present(skc11,skc12) )).
+
+cnf(clause19,negated_conjecture,
+    ( ~ ssSkC0
+    | event(skc11,skc12) )).
+
+cnf(clause20,negated_conjecture,
+    ( ~ ssSkC0
+    | hollywood_placename(skc11,skc14) )).
+
+cnf(clause21,negated_conjecture,
+    ( ~ ssSkC0
+    | placename(skc11,skc14) )).
+
+cnf(clause22,negated_conjecture,
+    ( ~ ssSkC0
+    | city(skc11,skc15) )).
+
+cnf(clause23,negated_conjecture,
+    ( ~ ssSkC0
+    | chevy(skc11,skc13) )).
+
+cnf(clause24,negated_conjecture,
+    ( ~ ssSkC0
+    | white(skc11,skc13) )).
+
+cnf(clause25,negated_conjecture,
+    ( ~ ssSkC0
+    | dirty(skc11,skc13) )).
+
+cnf(clause26,negated_conjecture,
+    ( ~ ssSkC0
+    | old(skc11,skc13) )).
+
+cnf(clause27,negated_conjecture,
+    ( ssSkC0
+    | down(skc17,skc18,skc20) )).
+
+cnf(clause28,negated_conjecture,
+    ( ssSkC0
+    | in(skc17,skc18,skc20) )).
+
+cnf(clause29,negated_conjecture,
+    ( ssSkC0
+    | of(skc17,skc21,skc20) )).
+
+cnf(clause30,negated_conjecture,
+    ( ssSkC0
+    | agent(skc17,skc18,skc19) )).
+
+cnf(clause31,negated_conjecture,
+    ( ~ ssSkC0
+    | down(skc11,skc12,skc16) )).
+
+cnf(clause32,negated_conjecture,
+    ( ~ ssSkC0
+    | in(skc11,skc12,skc15) )).
+
+cnf(clause33,negated_conjecture,
+    ( ~ ssSkC0
+    | of(skc11,skc14,skc15) )).
+
+cnf(clause34,negated_conjecture,
+    ( ~ ssSkC0
+    | agent(skc11,skc12,skc13) )).
+
+cnf(clause35,negated_conjecture,
+    ( ~ down(U,V,W)
+    | ~ lonely(U,W)
+    | ~ street(U,W)
+    | ~ barrel(U,V)
+    | ~ present(U,V)
+    | ~ event(U,V)
+    | ~ hollywood_placename(U,X)
+    | ~ placename(U,X)
+    | ~ in(U,V,Y)
+    | ~ city(U,Y)
+    | ~ of(U,X,Y)
+    | ~ chevy(U,Z)
+    | ~ white(U,Z)
+    | ~ dirty(U,Z)
+    | ~ old(U,Z)
+    | ~ agent(U,V,Z)
+    | ~ actual_world(U)
+    | ssSkC0 )).
+
+cnf(clause36,negated_conjecture,
+    ( ~ city(U,V)
+    | ~ street(U,V)
+    | ~ lonely(U,V)
+    | ~ down(U,W,V)
+    | ~ in(U,W,V)
+    | ~ placename(U,X)
+    | ~ hollywood_placename(U,X)
+    | ~ of(U,X,V)
+    | ~ event(U,W)
+    | ~ present(U,W)
+    | ~ barrel(U,W)
+    | ~ agent(U,W,Y)
+    | ~ old(U,Y)
+    | ~ dirty(U,Y)
+    | ~ white(U,Y)
+    | ~ chevy(U,Y)
+    | ~ actual_world(U)
+    | ~ ssSkC0 )).
+
+%--------------------------------------------------------------------------
diff --git a/test/regress/regress0/tptp/PUZ131_1.p b/test/regress/regress0/tptp/PUZ131_1.p
new file mode 100644
index 000000000..b9e1c648b
--- /dev/null
+++ b/test/regress/regress0/tptp/PUZ131_1.p
@@ -0,0 +1,100 @@
+%------------------------------------------------------------------------------
+% File     : PUZ131_1 : TPTP v5.5.0. Released v5.0.0.
+% Domain   : Puzzles
+% Problem  : Victor teaches Michael
+% Version  : Especial.
+% English  : Every student is enrolled in at least one course. Every professor
+%            teaches at least one course. Every course has at least one student
+%            enrolled. Every course has at least one professor teaching. The
+%            coordinator of a course teaches the course. If a student is
+%            enroled in a course then the student is taught by every professor
+%            who teaches the course. Michael is enrolled in CSC410. Victor is
+%            the coordinator of CSC410. Therefore, Michael is taught by Victor.
+
+% Refs     :
+% Source   : [TPTP]
+% Names    :
+
+% Status   : Theorem
+% Rating   : 0.00 v5.0.0
+% Syntax   : Number of formulae    :   19 (  14 unit;  10 type)
+%            Number of atoms       :   28 (   1 equality)
+%            Maximal formula depth :    6 (   3 average)
+%            Number of connectives :    2 (   0   ~;   0   |;   0   &)
+%                                         (   0 <=>;   2  =>;   0  <=;   0 <~>)
+%                                         (   0  ~|;   0  ~&)
+%            Number of type conns  :    7 (   4   >;   3   *;   0   +;   0  <<)
+%            Number of predicates  :   16 (  12 propositional; 0-2 arity)
+%            Number of functors    :    4 (   3 constant; 0-1 arity)
+%            Number of variables   :   12 (   0 sgn;   8   !;   4   ?)
+%            Maximal term depth    :    2 (   1 average)
+% SPC      : TFF_THM_EQU_NAR
+
+% Comments :
+%------------------------------------------------------------------------------
+tff(student_type,type,(
+    student: $tType )).
+
+tff(professor_type,type,(
+    professor: $tType )).
+
+tff(course_type,type,(
+    course: $tType )).
+
+tff(michael_type,type,(
+    michael: student )).
+
+tff(victor_type,type,(
+    victor: professor )).
+
+tff(csc410_type,type,(
+    csc410: course )).
+
+tff(enrolled_type,type,(
+    enrolled: ( student * course ) > $o )).
+
+tff(teaches_type,type,(
+    teaches: ( professor * course ) > $o )).
+
+tff(taught_by_type,type,(
+    taughtby: ( student * professor ) > $o )).
+
+tff(coordinator_of_type,type,(
+    coordinatorof: course > professor )).
+
+tff(student_enrolled_axiom,axiom,(
+    ! [X: student] :
+    ? [Y: course] : enrolled(X,Y) )).
+
+tff(professor_teaches,axiom,(
+    ! [X: professor] :
+    ? [Y: course] : teaches(X,Y) )).
+
+tff(course_enrolled,axiom,(
+    ! [X: course] :
+    ? [Y: student] : enrolled(Y,X) )).
+
+tff(course_teaches,axiom,(
+    ! [X: course] :
+    ? [Y: professor] : teaches(Y,X) )).
+
+tff(coordinator_teaches,axiom,(
+    ! [X: course] : teaches(coordinatorof(X),X) )).
+
+tff(student_enrolled_taught,axiom,(
+    ! [X: student,Y: course] :
+      ( enrolled(X,Y)
+     => ! [Z: professor] :
+          ( teaches(Z,Y)
+         => taughtby(X,Z) ) ) )).
+
+tff(michael_enrolled_csc410_axiom,axiom,(
+    enrolled(michael,csc410) )).
+
+tff(victor_coordinator_csc410_axiom,axiom,(
+    coordinatorof(csc410) = victor )).
+
+tff(teaching_conjecture,conjecture,(
+    taughtby(michael,victor) )).
+
+%------------------------------------------------------------------------------
diff --git a/test/regress/regress0/tptp/SYN000+1.p b/test/regress/regress0/tptp/SYN000+1.p
new file mode 100644
index 000000000..682c11b69
--- /dev/null
+++ b/test/regress/regress0/tptp/SYN000+1.p
@@ -0,0 +1,99 @@
+%------------------------------------------------------------------------------
+% File     : SYN000+1 : TPTP v5.5.0. Released v4.0.0.
+% Domain   : Syntactic
+% Problem  : Basic TPTP FOF syntax
+% Version  : Biased.
+% English  : Basic TPTP FOF syntax that you can't survive without parsing.
+
+% Refs     :
+% Source   : [TPTP]
+% Names    :
+
+% Status   : Theorem
+% Rating   : 0.43 v5.5.0, 0.48 v5.4.0, 0.46 v5.3.0, 0.52 v5.2.0, 0.40 v5.1.0, 0.43 v5.0.0, 0.54 v4.1.0, 0.57 v4.0.1, 0.78 v4.0.0
+% Syntax   : Number of formulae    :   12 (   5 unit)
+%            Number of atoms       :   31 (   3 equality)
+%            Maximal formula depth :    7 (   4 average)
+%            Number of connectives :   28 (   9   ~;  10   |;   3   &)
+%                                         (   1 <=>;   3  =>;   1  <=)
+%                                         (   1 <~>;   0  ~|;   0  ~&)
+%            Number of predicates  :   16 (  10 propositional; 0-3 arity)
+%            Number of functors    :    8 (   5 constant; 0-3 arity)
+%            Number of variables   :   13 (   0 sgn;   5   !;   8   ?)
+%            Maximal term depth    :    4 (   2 average)
+% SPC      : FOF_THM_RFO_SEQ
+
+% Comments :
+%------------------------------------------------------------------------------
+%----Propositional
+fof(propositional,axiom,
+    ( ( p0
+      & ~ q0 )
+   => ( r0
+      | ~ s0 ) )).
+
+%----First-order
+fof(first_order,axiom,(
+    ! [X] :
+      ( ( p(X)
+        | ~ q(X,a) )
+     => ? [Y,Z] :
+          ( r(X,f(Y),g(X,f(Y),Z))
+          & ~ s(f(f(f(b)))) ) ) )).
+
+%----Equality
+fof(equality,axiom,(
+    ? [Y] :
+    ! [X,Z] :
+      ( f(Y) = g(X,f(Y),Z)
+      | f(f(f(b))) != a
+      | X = f(Y) ) )).
+
+%----True and false
+fof(true_false,axiom,
+    ( $true
+    | $false )).
+
+%----Quoted symbols
+fof(single_quoted,axiom,
+    ( 'A proposition'
+    | 'A predicate'(a)
+    | p('A constant')
+    | p('A function'(a))
+    | p('A \'quoted \\ escape\'') )).
+
+%----Connectives - seen |, &, =>, ~ already
+fof(useful_connectives,axiom,(
+    ! [X] :
+      ( ( p(X)
+       <= ~ q(X,a) )
+    <=> ? [Y,Z] :
+          ( r(X,f(Y),g(X,f(Y),Z))
+        <~> ~ s(f(f(f(b)))) ) ) )).
+
+%----Annotated formula names
+fof(123,axiom,(
+    ! [X] :
+      ( ( p(X)
+        | ~ q(X,a) )
+     => ? [Y,Z] :
+          ( r(X,f(Y),g(X,f(Y),Z))
+          & ~ s(f(f(f(b)))) ) ) )).
+
+%----Roles
+fof(role_hypothesis,hypothesis,(
+    p(h) )).
+
+fof(role_conjecture,conjecture,(
+    ? [X] : p(X) )).
+
+%----Include directive
+include('Axioms/SYN000+0.ax').
+
+%----Comments
+/* This
+   is a block
+   comment.
+*/
+
+%------------------------------------------------------------------------------
diff --git a/test/regress/regress0/tptp/SYN000+2.p b/test/regress/regress0/tptp/SYN000+2.p
new file mode 100644
index 000000000..8c6f2f9f9
--- /dev/null
+++ b/test/regress/regress0/tptp/SYN000+2.p
@@ -0,0 +1,127 @@
+%------------------------------------------------------------------------------
+% File     : SYN000+2 : TPTP v5.5.0. Bugfixed v4.1.1.
+% Domain   : Syntactic
+% Problem  : Advanced TPTP FOF syntax
+% Version  : Biased.
+% English  : Advanced TPTP FOF syntax that you will encounter some time.
+
+% Refs     :
+% Source   : [TPTP]
+% Names    :
+
+% Status   : Satisfiable
+% Rating   : 0.50 v5.5.0, 0.67 v5.2.0, 1.00 v5.0.0
+% Syntax   : Number of formulae    :   20 (  16 unit)
+%            Number of atoms       :   31 (   2 equality)
+%            Maximal formula depth :    7 (   2 average)
+%            Number of connectives :   13 (   2   ~;   9   |;   0   &)
+%                                         (   0 <=>;   0  =>;   0  <=;   0 <~>)
+%                                         (   1  ~|;   1  ~&)
+%            Number of predicates  :    8 (   3 propositional; 0-3 arity)
+%            Number of functors    :   22 (  20 constant; 0-3 arity)
+%            Number of variables   :    8 (   0 sgn;   8   !;   0   ?)
+%            Maximal term depth    :    2 (   1 average)
+%            Arithmetic symbols    :   12 (   0 pred;    0 func;   12 numbers)
+% SPC      : FOF_SAT_RFO_SEQ
+
+% Comments :
+% Bugfixes : v4.0.1 - Added more numbers, particularly rationals.
+%          : v4.1.1 - Removed rationals with negative denominators.
+%------------------------------------------------------------------------------
+%----Quoted symbols
+fof(distinct_object,axiom,(
+    "An Apple" != "A \"Microsoft \\ escape\"" )).
+
+%----Numbers
+fof(integers,axiom,
+    ( p(12)
+    | p(-12) )).
+
+fof(rationals,axiom,
+    ( p(123/456)
+    | p(-123/456)
+    | p(+123/456) )).
+
+fof(reals,axiom,
+    ( p(123.456 )
+    | p(-123.456 )
+    | p(123.456E789 )
+    | p(123.456e789 )
+    | p(-123.456E789 )
+    | p(123.456E-789 )
+    | p(-123.456E-789 ) )).
+
+%----Connectives - seen |, &, =>, ~ already
+fof(never_used_connectives,axiom,(
+    ! [X] :
+      ( ( p(X)
+       ~| ~ q(X,a) )
+     ~& p(X) ) )).
+
+%----Roles
+fof(role_definition,definition,(
+    ! [X] : f(d) = f(X) )).
+
+fof(role_assumption,assumption,(
+    p(a) )).
+
+fof(role_lemma,lemma,(
+    p(l) )).
+
+fof(role_theorem,theorem,(
+    p(t) )).
+
+fof(role_unknown,unknown,(
+    p(u) )).
+
+%----Selective include directive
+include('Axioms/SYN000+0.ax',[ia1,ia3]).
+
+%----Source
+fof(source_unknown,axiom,(
+    ! [X] : p(X) ),
+    unknown).
+
+fof(source,axiom,(
+    ! [X] : p(X) ),
+    file('SYN000-1.p')).
+
+fof(source_name,axiom,(
+    ! [X] : p(X) ),
+    file('SYN000-1.p',source_unknown)).
+
+fof(source_copy,axiom,(
+    ! [X] : p(X) ),
+    source_unknown).
+
+fof(source_introduced_assumption,axiom,(
+    ! [X] : p(X) ),
+    introduced(assumption,[from,the,world])).
+
+fof(source_inference,plain,(
+    p(a) ),
+    inference(magic,
+        [status(thm),assumptions([source_introduced_assumption])],
+        [theory(equality),source_unknown])).
+
+fof(source_inference_with_bind,plain,(
+    p(a) ),
+    inference(magic,
+        [status(thm)],
+        [theory(equality),source_unknown:[bind(X,$fot(a))]])).
+
+%----Useful info
+fof(useful_info,axiom,(
+    ! [X] : p(X) ),
+    unknown,
+    [simple,
+     prolog(like,Data,[nested,12.2]),
+     AVariable,
+     12.2,
+     "A distinct object",
+     $fof(p(X) | ~ q(X,a) | r(X,f(Y),g(X,f(Y),Z)) | ~ s(f(f(f(b))))),
+     data(name):[colon,list,2],
+     [simple,prolog(like,Data,[nested,12.2]),AVariable,12.2]
+    ]).
+
+%------------------------------------------------------------------------------
diff --git a/test/regress/regress0/tptp/SYN000-1.p b/test/regress/regress0/tptp/SYN000-1.p
new file mode 100644
index 000000000..b6a68ec95
--- /dev/null
+++ b/test/regress/regress0/tptp/SYN000-1.p
@@ -0,0 +1,83 @@
+%------------------------------------------------------------------------------
+% File     : SYN000-1 : TPTP v5.5.0. Released v4.0.0.
+% Domain   : Syntactic
+% Problem  : Basic TPTP CNF syntax
+% Version  : Biased.
+% English  : Basic TPTP CNF syntax that you can't survive without parsing.
+
+% Refs     :
+% Source   : [TPTP]
+% Names    :
+
+% Status   : Unsatisfiable
+% Rating   : 0.50 v5.4.0, 0.55 v5.3.0, 0.56 v5.2.0, 0.62 v5.1.0, 0.65 v5.0.0, 0.64 v4.1.0, 0.62 v4.0.1, 0.64 v4.0.0
+% Syntax   : Number of clauses     :   11 (   6 non-Horn;   5 unit;   7 RR)
+%            Number of atoms       :   27 (   3 equality)
+%            Maximal clause size   :    5 (   2 average)
+%            Number of predicates  :   16 (  10 propositional; 0-3 arity)
+%            Number of functors    :    8 (   5 constant; 0-3 arity)
+%            Number of variables   :   11 (   5 singleton)
+%            Maximal term depth    :    4 (   2 average)
+% SPC      : CNF_UNS_RFO_SEQ_NHN
+
+% Comments :
+%------------------------------------------------------------------------------
+%----Propositional
+cnf(propositional,axiom,
+    ( p0
+    | ~ q0
+    | r0
+    | ~ s0 )).
+
+%----First-order
+cnf(first_order,axiom,
+    ( p(X)
+    | ~ q(X,a)
+    | r(X,f(Y),g(X,f(Y),Z))
+    | ~ s(f(f(f(b)))) )).
+
+%----Equality
+cnf(equality,axiom,
+    ( f(Y) = g(X,f(Y),Z)
+    | f(f(f(b))) != a
+    | X = f(Y) )).
+
+%----True and false
+cnf(true_false,axiom,
+    ( $true
+    | $false )).
+
+%----Quoted symbols
+cnf(single_quoted,axiom,
+    ( 'A proposition'
+    | 'A predicate'(Y)
+    | p('A constant')
+    | p('A function'(a))
+    | p('A \'quoted \\ escape\'') )).
+
+%----Connectives - seen them all already
+
+%----Annotated formula names
+cnf(123,axiom,
+    ( p(X)
+    | ~ q(X,a)
+    | r(X,f(Y),g(X,f(Y),Z))
+    | ~ s(f(f(f(b)))) )).
+
+%----Roles - seen axiom already
+cnf(role_hypothesis,hypothesis,
+    p(h)).
+
+cnf(role_negated_conjecture,negated_conjecture,
+    ~ p(X)).
+
+%----Include directive
+include('Axioms/SYN000-0.ax').
+
+%----Comments
+/* This
+   is a block
+   comment.
+*/
+
+%------------------------------------------------------------------------------
diff --git a/test/regress/regress0/tptp/SYN000-2.p b/test/regress/regress0/tptp/SYN000-2.p
new file mode 100644
index 000000000..0c6c0b59f
--- /dev/null
+++ b/test/regress/regress0/tptp/SYN000-2.p
@@ -0,0 +1,117 @@
+%------------------------------------------------------------------------------
+% File     : SYN000-2 : TPTP v5.5.0. Bugfixed v4.1.1.
+% Domain   : Syntactic
+% Problem  : Advanced TPTP CNF syntax
+% Version  : Biased.
+% English  : Advanced TPTP CNF syntax that you will encounter some time.
+
+% Refs     :
+% Source   : [TPTP]
+% Names    :
+
+% Status   : Satisfiable
+% Rating   : 1.00 v5.4.0, 0.90 v5.3.0, 0.89 v5.2.0, 0.90 v5.0.0
+% Syntax   : Number of clauses     :   19 (   3 non-Horn;  16 unit;  12 RR)
+%            Number of atoms       :   28 (   2 equality)
+%            Maximal clause size   :    7 (   1 average)
+%            Number of predicates  :    8 (   3 propositional; 0-3 arity)
+%            Number of functors    :   22 (  20 constant; 0-3 arity)
+%            Number of variables   :    7 (   7 singleton)
+%            Maximal term depth    :    2 (   1 average)
+%            Arithmetic symbols    :   12 (   0 pred;    0 func;   12 numbers)
+% SPC      : CNF_SAT_RFO_EQU_NUE
+
+% Comments :
+% Bugfixes : v4.0.1 - Added more numbers, particularly rationals.
+%          : v4.1.1 - Removed rationals with negative denominators.
+%------------------------------------------------------------------------------
+%----Quoted symbols
+cnf(distinct_object,axiom,
+    ( "An Apple" != "A \"Microsoft \\ escape\"" )).
+
+%----Numbers
+cnf(integers,axiom,
+    ( p(12)
+    | p(-12) )).
+
+cnf(rationals,axiom,
+    ( p(123/456)
+    | p(-123/456)
+    | p(+123/456) )).
+
+cnf(reals,axiom,
+    ( p(123.456 )
+    | p(-123.456 )
+    | p(123.456E789 )
+    | p(123.456e789 )
+    | p(-123.456E789 )
+    | p(123.456E-789 )
+    | p(-123.456E-789 ) )).
+
+%----Roles - seen axiom already
+cnf(role_definition,definition,
+    f(d) = f(X) ).
+
+cnf(role_assumption,assumption,
+    p(a) ).
+
+cnf(role_lemma,lemma,
+    p(l) ).
+
+cnf(role_theorem,theorem,
+    p(t) ).
+
+cnf(role_unknown,unknown,
+    p(u) ).
+
+%----Selective include directive
+include('Axioms/SYN000-0.ax',[ia1,ia3]).
+
+%----Source
+cnf(source_unknown,axiom,
+    p(X),
+    unknown).
+
+cnf(source,axiom,
+    p(X),
+    file('SYN000-1.p')).
+
+cnf(source_name,axiom,
+    p(X),
+    file('SYN000-1.p',source_unknown)).
+
+cnf(source_copy,axiom,
+    p(X),
+    source_unknown).
+
+cnf(source_introduced_assumption,axiom,
+    p(X),
+    introduced(assumption,[from,the,world])).
+
+cnf(source_inference,plain,
+    p(a),
+    inference(magic,
+        [status(thm),assumptions([source_introduced_assumption])],
+        [theory(equality),source_unknown])  ).
+
+cnf(source_inference_with_bind,plain,
+    p(a),
+    inference(magic,
+        [status(thm)],
+        [theory(equality),source_unknown:[bind(X,$fot(a))]])  ).
+
+%----Useful info
+cnf(useful_info,axiom,
+    p(X),
+    unknown,
+    [simple,
+     prolog(like,Data,[nested,12.2]),
+     AVariable,
+     12.2,
+     "A distinct object",
+     $cnf(p(X) | ~q(X,a) | r(X,f(Y),g(X,f(Y),Z)) | ~ s(f(f(f(b))))),
+     data(name):[colon,list,2],
+     [simple,prolog(like,Data,[nested,12.2]),AVariable,12.2]
+    ]).
+
+%------------------------------------------------------------------------------
diff --git a/test/regress/regress0/tptp/SYN000=2.p b/test/regress/regress0/tptp/SYN000=2.p
new file mode 100644
index 000000000..802613f4b
--- /dev/null
+++ b/test/regress/regress0/tptp/SYN000=2.p
@@ -0,0 +1,309 @@
+%------------------------------------------------------------------------------
+% File     : SYN000=2 : TPTP v5.5.0. Bugfixed v5.5.1.
+% Domain   : Syntactic
+% Problem  : TF0 syntax with arithmetic
+% Version  : Biased.
+% English  : 
+
+% Refs     :
+% Source   : [TPTP]
+% Names    :
+
+% Status   : Theorem
+% Rating   : ? v5.5.1
+% Syntax   : Number of formulae    :   83 (  73 unit;   6 type)
+%            Number of atoms       :  100 (   4 equality)
+%            Maximal formula depth :    7 (   1 average)
+%            Number of connectives :   14 (   0   ~;  10   |;   1   &)
+%                                         (   0 <=>;   3  =>;   0  <=;   0 <~>)
+%                                         (   0  ~|;   0  ~&)
+%            Number of type conns  :    3 (   3   >;   0   *;   0   +;   0  <<)
+%            Number of predicates  :   20 (  10 propositional; 0-2 arity)
+%            Number of functors    :   41 (  24 constant; 0-2 arity)
+%            Number of variables   :   14 (   1 sgn;   3   !;  11   ?)
+%            Maximal term depth    :    3 (   1 average)
+%            Arithmetic symbols    :   37 (   9 pred;    7 func;   21 numbers)
+% SPC      : TF0_THM_EQU_ARI
+
+% Comments : 
+% Bugfixes : v5.5.1 - Removed $evaleq.
+%------------------------------------------------------------------------------
+%----Types for what follows
+tff(p_int_type,type,(
+    p_int: $int > $o )).
+
+tff(p_rat_type,type,(
+    p_rat: $rat > $o )).
+
+tff(p_real_type,type,(
+    p_real: $real > $o )).
+
+tff(a_int,type,(
+    a_int: $int )).
+
+tff(a_rat,type,(
+    a_rat: $rat )).
+
+tff(a_real,type,(
+    a_real: $real )).
+
+%----Numbers
+tff(integers,axiom,
+    ( p_int(123)
+    | p_int(-123) )).
+
+tff(rationals,axiom,
+    ( p_rat(123/456)
+    | p_rat(-123/456)
+    | p_rat(123/456) )).
+
+tff(reals,axiom,
+    ( p_real(123.456)
+    | p_real(-123.456)
+    | p_real(123.456E78)
+    | p_real(123.456e78)
+    | p_real(-123.456E78)
+    | p_real(123.456E-78)
+    | p_real(-123.456E-78) )).
+
+%----Variables
+tff(variables_int,axiom,(
+    ! [X: $int] :
+    ? [Y: $int] :
+      ( p_int(X)
+     => p_int(Y) ) )).
+
+tff(variables_rat,axiom,(
+    ! [X: $rat] :
+    ? [Y: $rat] :
+      ( p_rat(X)
+     => p_rat(Y) ) )).
+
+tff(variables_real,axiom,(
+    ! [X: $real] :
+    ? [Y: $real] :
+      ( p_real(X)
+     => p_real(Y) ) )).
+
+%----Arithmetic relations
+tff(less_int,axiom,(
+    $less(a_int,3) )).
+
+tff(less_rat,axiom,(
+    $less(a_rat,3/9) )).
+
+tff(less_real,axiom,(
+    $less(a_real,3.3) )).
+
+tff(lesseq_int,axiom,(
+    $lesseq(a_int,3) )).
+
+tff(lesseq_rat,axiom,(
+    $lesseq(a_rat,3/9) )).
+
+tff(lesseq_real,axiom,(
+    $lesseq(a_real,3.3) )).
+
+tff(greater_int,axiom,(
+    $greater(a_int,-3) )).
+
+tff(greater_rat,axiom,(
+    $greater(a_rat,-3/9) )).
+
+tff(greater_real,axiom,(
+    $greater(a_real,-3.3) )).
+
+tff(greatereq_int,axiom,(
+    $greatereq(a_int,-3) )).
+
+tff(greatereq_rat,axiom,(
+    $greatereq(a_rat,-3/9) )).
+
+tff(greatereq_real,axiom,(
+    $greatereq(a_real,-3.3) )).
+
+tff(equal_int,axiom,(
+    a_int = 0 )).
+
+tff(equal_rat,axiom,(
+    a_rat = 0/1 )).
+
+tff(equal_real,axiom,(
+    a_real = 0.0 )).
+
+%----Arithmetic functions
+tff(uminus_int,axiom,(
+    p_int($uminus(3)) )).
+
+tff(uminus_rat,axiom,(
+    p_rat($uminus(3/9)) )).
+
+tff(uminus_real,axiom,(
+    p_real($uminus(3.3)) )).
+
+tff(sum_int,axiom,(
+    p_int($sum(3,3)) )).
+
+tff(sum_rat,axiom,(
+    p_rat($sum(3/9,3/9)) )).
+
+tff(sum_real,axiom,(
+    p_real($sum(3.3,3.3)) )).
+
+tff(difference_int,axiom,(
+    p_int($difference(3,3)) )).
+
+tff(difference_rat,axiom,(
+    p_rat($difference(3/9,3/9)) )).
+
+tff(difference_real,axiom,(
+    p_real($difference(3.3,3.3)) )).
+
+tff(product_int,axiom,(
+    p_int($product(3,3)) )).
+
+tff(product_rat,axiom,(
+    p_rat($product(3/9,3/9)) )).
+
+tff(product_real,axiom,(
+    p_real($product(3.3,3.3)) )).
+
+tff(quotient_rat,axiom,(
+    p_rat($quotient(3/9,3/9)) )).
+
+tff(quotient_real,axiom,(
+    p_real($quotient(3.3,3.3)) )).
+
+tff(quotient_e_int,axiom,(
+    p_int($quotient_e(3,3)) )).
+
+tff(quotient_e_rat,axiom,(
+    p_rat($quotient_e(3/9,3/9)) )).
+
+tff(quotient_e_real,axiom,(
+    p_real($quotient_e(3.3,3.3)) )).
+
+tff(quotient_t_int,axiom,(
+    p_int($quotient_t(3,3)) )).
+
+tff(quotient_t_rat,axiom,(
+    p_rat($quotient_t(3/9,3/9)) )).
+
+tff(quotient_t_real,axiom,(
+    p_real($quotient_t(3.3,3.3)) )).
+
+tff(quotient_f_int,axiom,(
+    p_int($quotient_f(3,3)) )).
+
+tff(quotient_f_rat,axiom,(
+    p_rat($quotient_f(3/9,3/9)) )).
+
+tff(quotient_f_real,axiom,(
+    p_real($quotient_f(3.3,3.3)) )).
+
+tff(remainder_e_int,axiom,(
+    p_int($remainder_e(3,3)) )).
+
+tff(remainder_e_rat,axiom,(
+    p_rat($remainder_e(3/9,3/9)) )).
+
+tff(remainder_e_real,axiom,(
+    p_real($remainder_e(3.3,3.3)) )).
+
+tff(remainder_t_int,axiom,(
+    p_int($remainder_t(3,3)) )).
+
+tff(remainder_t_rat,axiom,(
+    p_rat($remainder_t(3/9,3/9)) )).
+
+tff(remainder_t_real,axiom,(
+    p_real($remainder_t(3.3,3.3)) )).
+
+tff(remainder_f_int,axiom,(
+    p_int($remainder_f(3,3)) )).
+
+tff(remainder_f_rat,axiom,(
+    p_rat($remainder_f(3/9,3/9)) )).
+
+tff(remainder_f_real,axiom,(
+    p_real($remainder_f(3.3,3.3)) )).
+
+tff(floor_int,axiom,(
+    p_int($floor(3)) )).
+
+tff(floor_rat,axiom,(
+    p_rat($floor(3/9)) )).
+
+tff(floor_int,axiom,(
+    p_real($floor(3.3)) )).
+
+tff(ceiling_int,axiom,(
+    p_int($ceiling(3)) )).
+
+tff(ceiling_rat,axiom,(
+    p_rat($ceiling(3/9)) )).
+
+tff(ceiling_int,axiom,(
+    p_real($ceiling(3.3)) )).
+
+tff(truncate_int,axiom,(
+    p_int($truncate(3)) )).
+
+tff(truncate_rat,axiom,(
+    p_rat($truncate(3/9)) )).
+
+tff(truncate_int,axiom,(
+    p_real($truncate(3.3)) )).
+
+%----Recognizing numbers
+tff(is_int_int,axiom,(
+    ? [X: $int] : $is_int(X) )).
+
+tff(is_int_rat,axiom,(
+    ? [X: $rat] : $is_int(X) )).
+
+tff(is_int_real,axiom,(
+    ? [X: $real] : $is_int(X) )).
+
+tff(is_rat_rat,axiom,(
+    ? [X: $rat] : $is_rat(X) )).
+
+tff(is_rat_real,axiom,(
+    ? [X: $real] : $is_rat(X) )).
+
+%----Coercion
+tff(to_int_int,axiom,(
+    p_int($to_int(3)) )).
+
+tff(to_int_rat,axiom,(
+    p_int($to_int(3/9)) )).
+
+tff(to_int_real,axiom,(
+    p_int($to_int(3.3)) )).
+
+tff(to_rat_int,axiom,(
+    p_rat($to_rat(3)) )).
+
+tff(to_rat_rat,axiom,(
+    p_rat($to_rat(3/9)) )).
+
+tff(to_rat_real,axiom,(
+    p_rat($to_rat(3.3)) )).
+
+tff(to_real_int,axiom,(
+    p_real($to_real(3)) )).
+
+tff(to_real_rat,axiom,(
+    p_real($to_real(3/9)) )).
+
+tff(to_real_real,axiom,(
+    p_real($to_real(3.3)) )).
+
+%----A conjecture to prove
+tff(mixed,conjecture,(
+    ? [X: $int,Y: $rat,Z: $real] :
+      ( Y = $to_rat($sum(X,2))
+      & ( $less($to_int(Y),3)
+        | $greater($to_real(Y),3.3) ) ) )).
+
+%------------------------------------------------------------------------------
diff --git a/test/regress/regress0/tptp/SYN000_1.p b/test/regress/regress0/tptp/SYN000_1.p
new file mode 100644
index 000000000..ed683c070
--- /dev/null
+++ b/test/regress/regress0/tptp/SYN000_1.p
@@ -0,0 +1,170 @@
+%------------------------------------------------------------------------------
+% File     : SYN000_1 : TPTP v5.5.0. Released v5.0.0.
+% Domain   : Syntactic
+% Problem  : Basic TPTP TFF syntax without arithmetic
+% Version  : Biased.
+% English  : Basic TPTP TFF syntax that you can't survive without parsing.
+
+% Refs     :
+% Source   : [TPTP]
+% Names    :
+
+% Status   : Theorem
+% Rating   : 0.40 v5.5.0, 0.25 v5.4.0, 0.33 v5.2.0, 0.67 v5.0.0
+% Syntax   : Number of formulae    :   38 (  21 unit;  25 type)
+%            Number of atoms       :   74 (   3 equality)
+%            Maximal formula depth :    7 (   3 average)
+%            Number of connectives :   28 (   9   ~;  10   |;   3   &)
+%                                         (   1 <=>;   3  =>;   1  <=;   1 <~>)
+%                                         (   0  ~|;   0  ~&)
+%            Number of type conns  :   17 (  10   >;   7   *;   0   +;   0  <<)
+%            Number of predicates  :   37 (  30 propositional; 0-3 arity)
+%            Number of functors    :   10 (   6 constant; 0-3 arity)
+%            Number of variables   :   14 (   1 sgn;   6   !;   8   ?)
+%            Maximal term depth    :    4 (   2 average)
+% SPC      : TFF_THM_EQU_NAR
+
+% Comments :
+%------------------------------------------------------------------------------
+%----Propositional
+tff(p0_type,type,(
+    p0: $o )).
+
+tff(q0_type,type,(
+    q0: $o )).
+
+tff(r0_type,type,(
+    r0: $o )).
+
+tff(s0_type,type,(
+    s0: $o )).
+
+tff(propositional,axiom,
+    ( ( p0
+      & ~ q0 )
+   => ( r0
+      | ~ s0 ) )).
+
+%----First-order
+tff(a_type,type,(
+    a: $i )).
+
+tff(b_type,type,(
+    b: $i )).
+
+tff(h_type,type,(
+    h: $i )).
+
+tff(f_type,type,(
+    f: $i > $i )).
+
+tff(g_type,type,(
+    g: ( $i * $i * $i ) > $i )).
+
+tff(p_type,type,(
+    p: $i > $o )).
+
+tff(q_type,type,(
+    q: ( $i * $i ) > $o )).
+
+tff(r_type,type,(
+    r: ( $i * $i * $i ) > $o )).
+
+tff(s_type,type,(
+    s: $i > $o )).
+
+tff(first_order,axiom,(
+    ! [X: $i] :
+      ( ( p(X)
+        | ~ q(X,a) )
+     => ? [Y: $i,Z: $i] :
+          ( r(X,f(Y),g(X,f(Y),Z))
+          & ~ s(f(f(f(b)))) ) ) )).
+
+%----Equality
+tff(equality,axiom,(
+    ? [Y: $i] :
+    ! [X: $i,Z: $i] :
+      ( f(Y) = g(X,f(Y),Z)
+      | f(f(f(b))) != a
+      | X = f(Y) ) )).
+
+%----True and false
+tff(true_false,axiom,
+    ( $true
+    | $false )).
+
+tff(quoted_proposition_type,type,(
+    'A proposition': $o )).
+
+tff(quoted_predicate_type,type,(
+    'A predicate': $i > $o )).
+
+tff(quoted_constant_type,type,(
+    'A constant': $i )).
+
+tff(quoted_function_type,type,(
+    'A function': $i > $i )).
+
+tff(quoted_escape_type,type,(
+    'A \'quoted \\ escape\'': $i )).
+
+%----Quoted symbols
+tff(single_quoted,axiom,
+    ( 'A proposition'
+    | 'A predicate'(a)
+    | p('A constant')
+    | p('A function'(a))
+    | p('A \'quoted \\ escape\'') )).
+
+%----Connectives - seen |, &, =>, ~ already
+tff(useful_connectives,axiom,(
+    ! [X: $i] :
+      ( ( p(X)
+       <= ~ q(X,a) )
+    <=> ? [Y: $i,Z: $i] :
+          ( r(X,f(Y),g(X,f(Y),Z))
+        <~> ~ s(f(f(f(b)))) ) ) )).
+
+%----New types
+tff(new_type,type,(
+    new: $tType )).
+
+tff(newc_type,type,(
+    newc: new )).
+
+tff(newf_type,type,(
+    newf: ( new * $i ) > new )).
+
+tff(newp_type,type,(
+    newp: ( new * $i ) > $o )).
+
+tff(new_axiom,axiom,(
+    ! [X: new] : newp(newf(newc,a),a) )).
+
+%----Annotated formula names
+tff(123,axiom,(
+    ! [X: $i] :
+      ( ( p(X)
+        | ~ q(X,a) )
+     => ? [Y: $i,Z: $i] :
+          ( r(X,f(Y),g(X,f(Y),Z))
+          & ~ s(f(f(f(b)))) ) ) )).
+
+%----Roles
+tff(role_hypothesis,hypothesis,(
+    p(h) )).
+
+tff(role_conjecture,conjecture,(
+    ? [X: $i] : p(X) )).
+
+%----Include directive
+include('Axioms/SYN000_0.ax').
+
+%----Comments
+/* This
+   is a block
+   comment.
+*/
+
+%------------------------------------------------------------------------------
diff --git a/test/regress/regress0/tptp/SYN000_2.p b/test/regress/regress0/tptp/SYN000_2.p
new file mode 100644
index 000000000..ece5fa6b1
--- /dev/null
+++ b/test/regress/regress0/tptp/SYN000_2.p
@@ -0,0 +1,135 @@
+%------------------------------------------------------------------------------
+% File     : SYN000_2 : TPTP v5.5.0. Bugfixed v5.5.1.
+% Domain   : Syntactic
+% Problem  : Advanced TPTP TF0 syntax without arithmetic
+% Version  : Biased.
+% English  : Advanced TPTP TF0 syntax that you will encounter some time.
+
+% Refs     :
+% Source   : [TPTP]
+% Names    :
+
+% Status   : Satisfiable
+% Rating   : ? v5.5.1
+% Syntax   : Number of formulae    :   26 (  18 unit;   7 type)
+%            Number of atoms       :   42 (   2 equality)
+%            Maximal formula depth :    5 (   2 average)
+%            Number of connectives :    6 (   2   ~;   0   |;   1   &)
+%                                         (   1 <=>;   0  =>;   0  <=;   0 <~>)
+%                                         (   1  ~|;   1  ~&)
+%            Number of type conns  :    9 (   5   >;   4   *;   0   +;   0  <<)
+%            Number of predicates  :   14 (  11 propositional; 0-2 arity)
+%            Number of functors    :    6 (   4 constant; 0-2 arity)
+%            Number of variables   :   18 (   0 sgn;  13   !;   1   ?)
+%            Maximal term depth    :    2 (   1 average)
+% SPC      : TF0_SAT_EQU_NAR
+
+% Comments : 
+% Bugfixes : v5.5.1 - Fixed let_binders.
+%------------------------------------------------------------------------------
+%----Quoted symbols
+tff(distinct_object,axiom,(
+    "An Apple" != "A \"Microsoft \\ escape\"" )).
+
+%----Types for stuff below
+tff(a_type,type,(
+    a: $i )).
+
+tff(b_type,type,(
+    b: $i )).
+
+tff(f_type,type,(
+    f: $i > $i )).
+
+tff(g_type,type,(
+    g: ( $i * $i ) > $i )).
+
+tff(h_type,type,(
+    h: ( $i * $i * $i ) > $i )).
+
+tff(p_type,type,(
+    p: $i > $o )).
+
+tff(q_type,type,(
+    q: ( $i * $i ) > $o )).
+
+%----Conditional constructs
+tff(conditionals,axiom,(
+    ! [Z: $i] :
+      $ite_f(
+        ? [X: $i] : p(X)
+      , ! [X: $i] : q(X,X)
+      , q(Z,$ite_t(! [X: $i] : p(X), f(a), f(Z))) ) )).
+
+%----Let binders
+tff(let_binders,axiom,(
+    ! [X: $i] :
+      $let_ff(
+        ! [Y1: $i,Y2: $i] :
+          ( q(Y1,Y2)
+        <=> p(Y1) )
+      , ( q($let_tt(! [Z1: $i] : f(Z1) = g(Z1,b), f(a)),X)
+        & p($let_ft(! [Y3: $i] : ! [Y4: $i] : ( q(Y3,Y4) <=> $ite_f(Y3 = Y4, q(a,a), q(Y3,Y4) ) ), $ite_t(q(b,b), f(a), f(X)))) ) ) )).
+
+%----Rare connectives
+tff(never_used_connectives,axiom,(
+    ! [X: $i] :
+      ( ( p(X)
+       ~| ~ q(X,a) )
+     ~& p(X) ) )).
+
+%----Roles
+tff(role_definition,definition,(
+    ! [X: $i] : f(a) = f(X) )).
+
+tff(role_assumption,assumption,(
+    p(a) )).
+
+tff(role_lemma,lemma,(
+    p(a) )).
+
+tff(role_theorem,theorem,(
+    p(a) )).
+
+tff(role_unknown,unknown,(
+    p(a) )).
+
+%----Selective include directive
+include('Axioms/SYN000_0.ax',[ia1,ia3]).
+
+%----Source
+tff(source_unknown,axiom,(
+    ! [X: $i] : p(X) ),
+    unknown).
+
+tff(source,axiom,(
+    ! [X: $i] : p(X) ),
+    file('SYN000-1.p')).
+
+tff(source_name,axiom,(
+    ! [X: $i] : p(X) ),
+    file('SYN000-1.p',source_unknown)).
+
+tff(source_copy,axiom,(
+    ! [X: $i] : p(X) ),
+    source_unknown).
+
+tff(source_introduced_assumption,axiom,(
+    ! [X: $i] : p(X) ),
+    introduced(assumption,[from,the,world])).
+
+tff(source_inference,plain,(
+    p(a) ),
+    inference(magic,[status(thm),assumptions([source_introduced_assumption])],[theory(equality),source_unknown])).
+
+tff(source_inference_with_bind,plain,(
+    p(a) ),
+    inference(magic,[status(thm)],[theory(equality),source_unknown:[bind(X,$fot(a))]])).
+
+%----Useful info
+tff(useful_info,axiom,(
+    ! [X: $i] : p(X) ),
+    unknown,
+    [simple,prolog(like,Data,[nested,12.2]),AVariable,12.2,"A distinct object",$tff(p(X) | ~ q(X,a)),data(name):[colon,list,2],[simple,prolog(like,Data,[nested,12.2]),AVariable,12.2]]).
+
+%------------------------------------------------------------------------------
diff --git a/test/regress/regress0/tptp/SYN075+1.p b/test/regress/regress0/tptp/SYN075+1.p
new file mode 100644
index 000000000..7ef40217c
--- /dev/null
+++ b/test/regress/regress0/tptp/SYN075+1.p
@@ -0,0 +1,46 @@
+%--------------------------------------------------------------------------
+% File     : SYN075+1 : TPTP v5.5.0. Released v2.0.0.
+% Domain   : Syntactic
+% Problem  : Pelletier Problem 52
+% Version  : Especial.
+% English  :
+
+% Refs     : [Pel86] Pelletier (1986), Seventy-five Problems for Testing Au
+%          : [Hah94] Haehnle (1994), Email to G. Sutcliffe
+% Source   : [Hah94]
+% Names    : Pelletier 52 [Pel86]
+
+% Status   : Theorem
+% Rating   : 0.22 v5.5.0, 0.15 v5.4.0, 0.18 v5.3.0, 0.26 v5.2.0, 0.05 v5.0.0, 0.21 v4.1.0, 0.17 v4.0.1, 0.22 v4.0.0, 0.21 v3.7.0, 0.00 v3.3.0, 0.11 v3.2.0, 0.33 v3.1.0, 0.17 v2.7.0, 0.00 v2.5.0, 0.33 v2.4.0, 0.33 v2.2.1, 0.00 v2.1.0
+% Syntax   : Number of formulae    :    2 (   0 unit)
+%            Number of atoms       :    6 (   4 equality)
+%            Maximal formula depth :    7 (   7 average)
+%            Number of connectives :    4 (   0 ~  ;   0  |;   1  &)
+%                                         (   3 <=>;   0 =>;   0 <=)
+%                                         (   0 <~>;   0 ~|;   0 ~&)
+%            Number of predicates  :    2 (   0 propositional; 2-2 arity)
+%            Number of functors    :    0 (   0 constant; --- arity)
+%            Number of variables   :    8 (   0 singleton;   4 !;   4 ?)
+%            Maximal term depth    :    1 (   1 average)
+% SPC      : FOF_THM_RFO_SEQ
+
+% Comments :
+%--------------------------------------------------------------------------
+%----Problem axioms
+fof(pel52_1,axiom,
+    ( ? [Z,W] :
+      ! [X,Y] :
+        ( big_f(X,Y)
+      <=> ( X = Z
+          & Y = W ) ) )).
+
+fof(pel52,conjecture,
+    ( ? [W] :
+      ! [Y] :
+        ( ? [Z] :
+          ! [X] :
+            ( big_f(X,Y)
+          <=> X = Z )
+      <=> Y = W ) )).
+
+%--------------------------------------------------------------------------
diff --git a/test/regress/regress0/tptp/SYN075-1.p b/test/regress/regress0/tptp/SYN075-1.p
new file mode 100644
index 000000000..40b49fa36
--- /dev/null
+++ b/test/regress/regress0/tptp/SYN075-1.p
@@ -0,0 +1,76 @@
+%--------------------------------------------------------------------------
+% File     : SYN075-1 : TPTP v5.5.0. Released v1.0.0.
+% Domain   : Syntactic
+% Problem  : Pelletier Problem 52
+% Version  : Especial.
+% English  :
+
+% Refs     : [Pel86] Pelletier (1986), Seventy-five Problems for Testing Au
+% Source   : [Pel86]
+% Names    : Pelletier 52 [Pel86]
+
+% Status   : Unsatisfiable
+% Rating   : 0.00 v5.5.0, 0.20 v5.3.0, 0.22 v5.2.0, 0.12 v5.1.0, 0.06 v5.0.0, 0.07 v4.1.0, 0.08 v4.0.1, 0.18 v4.0.0, 0.09 v3.7.0, 0.00 v3.3.0, 0.14 v3.2.0, 0.08 v3.1.0, 0.09 v2.7.0, 0.08 v2.6.0, 0.00 v2.5.0, 0.08 v2.4.0, 0.11 v2.2.1, 0.11 v2.2.0, 0.22 v2.1.0, 0.33 v2.0.0
+% Syntax   : Number of clauses     :   10 (   4 non-Horn;   0 unit;   8 RR)
+%            Number of atoms       :   31 (  17 equality)
+%            Maximal clause size   :    4 (   3 average)
+%            Number of predicates  :    2 (   0 propositional; 2-2 arity)
+%            Number of functors    :    5 (   2 constant; 0-2 arity)
+%            Number of variables   :   23 (   2 singleton)
+%            Maximal term depth    :    2 (   1 average)
+% SPC      : CNF_UNS_RFO_SEQ_NHN
+
+% Comments :
+%--------------------------------------------------------------------------
+cnf(clause_1,axiom,
+    ( ~ big_f(X,Y)
+    | X = a )).
+
+cnf(clause_2,axiom,
+    ( ~ big_f(X,Y)
+    | Y = b )).
+
+cnf(clause_3,axiom,
+    ( X != a
+    | Y != b
+    | big_f(X,Y) )).
+
+cnf(clause_4,negated_conjecture,
+    ( ~ big_f(Y,f(X))
+    | Y != g(X)
+    | f(X) = X )).
+
+cnf(clause_5,negated_conjecture,
+    ( ~ big_f(Y,f(X))
+    | Y = g(X)
+    | big_f(h(X,Z),f(X))
+    | ~ big_f(h(X,Z),f(X)) )).
+
+cnf(clause_6,negated_conjecture,
+    ( Y != g(X)
+    | big_f(Y,f(X))
+    | f(X) = X )).
+
+cnf(clause_7,negated_conjecture,
+    ( Y != g(X)
+    | big_f(Y,f(X))
+    | big_f(h(X,Z),f(X))
+    | h(X,Z) = Z )).
+
+cnf(clause_8,negated_conjecture,
+    ( Y != g(X)
+    | big_f(Y,f(X))
+    | h(X,Z) != Z
+    | ~ big_f(h(X,Z),f(X)) )).
+
+cnf(clause_9,negated_conjecture,
+    ( f(X) != X
+    | big_f(h(X,Z),f(X))
+    | h(X,Z) = Z )).
+
+cnf(clause_10,negated_conjecture,
+    ( f(X) != X
+    | h(X,Z) != Z
+    | ~ big_f(h(X,Z),f(X)) )).
+
+%--------------------------------------------------------------------------
diff --git a/test/regress/regress0/tptp/tff0-arith.p b/test/regress/regress0/tptp/tff0-arith.p
new file mode 100644
index 000000000..c0e9af25a
--- /dev/null
+++ b/test/regress/regress0/tptp/tff0-arith.p
@@ -0,0 +1,27 @@
+% example from the TFF0 paper
+% see https://sites.google.com/site/polymorphictptptff/relevant-links/tff-tfa
+%
+% Status : Theorem
+%
+tff(list_type,type, ( list: $tType )).
+tff(nil_type,type, ( nil: list )).
+tff(mycons_type,type,( mycons: ( $int * list ) > list )).
+tff(sorted_type,type,( fib_sorted: list > $o )).
+
+tff(empty_fib_sorted,axiom,(
+    fib_sorted(nil) )).
+tff(single_is_fib_sorted,axiom,(
+    ! [X: $int] : fib_sorted(mycons(X,nil)) )).
+tff(double_is_fib_sorted_if_ordered,axiom,(
+    ! [X: $int,Y: $int] :
+      ( $less(X,Y)
+     => fib_sorted(mycons(X,mycons(Y,nil))) ) )).
+tff(recursive_fib_sort,axiom,(
+    ! [X: $int,Y: $int,Z: $int,R: list] :
+      ( ( $less(X,Y)
+        & $greatereq(Z,$sum(X,Y))
+        & fib_sorted(mycons(Y,mycons(Z,R))) )
+     => fib_sorted(mycons(X,mycons(Y,mycons(Z,R)))) ) )).
+
+tff(check_list,conjecture,(
+    fib_sorted(mycons(1,mycons(2,mycons(4,nil)))) )).
diff --git a/test/regress/regress0/tptp/tff0.p b/test/regress/regress0/tptp/tff0.p
new file mode 100644
index 000000000..0402687bc
--- /dev/null
+++ b/test/regress/regress0/tptp/tff0.p
@@ -0,0 +1,37 @@
+% example from the TFF0 paper
+% see https://sites.google.com/site/polymorphictptptff/relevant-links/tff-tfa
+%
+% Status : Theorem
+%
+tff(student_type,type, ( student: $tType )).
+tff(professor_type,type,( professor: $tType )).
+tff(course_type,type, ( course: $tType )).
+tff(michael_type,type, ( michael: student )).
+tff(victor_type,type, ( victor: professor )).
+tff(csc410_type,type, ( csc410: course )).
+tff(enrolled_type,type, ( enrolled: ( student * course ) > $o )).
+tff(teaches_type,type, ( teaches: ( professor * course ) > $o )).
+tff(taught_by_type,type,( taughtby: ( student * professor ) > $o )).
+tff(coordinator_of_type,type,( coordinatorof: course > professor )).
+
+tff(student_enrolled_axiom,axiom,(
+    ! [X: student] : ? [Y: course] : enrolled(X,Y) )).
+tff(professor_teaches,axiom,(
+    ! [X: professor] : ? [Y: course] : teaches(X,Y) )).
+tff(course_enrolled,axiom,(
+    ! [X: course] : ? [Y: student] : enrolled(Y,X) )).
+tff(course_teaches,axiom,(
+    ! [X: course] : ? [Y: professor] : teaches(Y,X) )).
+tff(coordinator_teaches,axiom,(
+    ! [X: course] : teaches(coordinatorof(X),X) )).
+tff(student_enrolled_taught,axiom,(
+    ! [X: student,Y: course] :
+      ( enrolled(X,Y)
+     => ! [Z: professor] : ( teaches(Z,Y) => taughtby(X,Z) ) ) )).
+tff(michael_enrolled_csc410_axiom,axiom,(
+    enrolled(michael,csc410) )).
+tff(victor_coordinator_csc410_axiom,axiom,(
+    coordinatorof(csc410) = victor )).
+
+tff(teaching_conjecture,conjecture,(
+    taughtby(michael,victor) )).
diff --git a/test/regress/regress0/tptp_parser.p b/test/regress/regress0/tptp/tptp_parser.p
index 0be0adbbf..9c10d5bd3 100644
--- a/test/regress/regress0/tptp_parser.p
+++ b/test/regress/regress0/tptp/tptp_parser.p
@@ -1,5 +1,4 @@
-% EXPECT: unsat
-% EXIT: 20
+% Status: Unsatisfiable
 
 %--------------------------------------------------------------------------
 
diff --git a/test/regress/regress0/tptp_parser10.p b/test/regress/regress0/tptp/tptp_parser10.p
index 90db619e7..d6a257121 100644
--- a/test/regress/regress0/tptp_parser10.p
+++ b/test/regress/regress0/tptp/tptp_parser10.p
@@ -1,5 +1,4 @@
-% EXPECT: unsat
-% EXIT: 20
+% Status: Theorem
 
 %--------------------------------------------------------------------------
 
diff --git a/test/regress/regress0/tptp_parser2.p b/test/regress/regress0/tptp/tptp_parser2.p
index 83a5f7b83..e165b6b2f 100644
--- a/test/regress/regress0/tptp_parser2.p
+++ b/test/regress/regress0/tptp/tptp_parser2.p
@@ -1,5 +1,4 @@
-% EXPECT: unsat
-% EXIT: 20
+% Status: Unsatisfiable
 
 %--------------------------------------------------------------------------
 
diff --git a/test/regress/regress0/tptp_parser3.p b/test/regress/regress0/tptp/tptp_parser3.p
index 3677e6ffe..2840892bc 100644
--- a/test/regress/regress0/tptp_parser3.p
+++ b/test/regress/regress0/tptp/tptp_parser3.p
@@ -1,5 +1,4 @@
-% EXPECT: unsat
-% EXIT: 20
+% Status: Unsatisfiable
 
 %--------------------------------------------------------------------------
 
diff --git a/test/regress/regress0/tptp_parser4.p b/test/regress/regress0/tptp/tptp_parser4.p
index 6c5bd29da..448db77d2 100644
--- a/test/regress/regress0/tptp_parser4.p
+++ b/test/regress/regress0/tptp/tptp_parser4.p
@@ -1,5 +1,4 @@
-% EXPECT: unsat
-% EXIT: 20
+% Status: Unsatisfiable
 
 %--------------------------------------------------------------------------
 
diff --git a/test/regress/regress0/tptp_parser5.p b/test/regress/regress0/tptp/tptp_parser5.p
index 23ddf3e60..c90d1cdad 100644
--- a/test/regress/regress0/tptp_parser5.p
+++ b/test/regress/regress0/tptp/tptp_parser5.p
@@ -1,5 +1,4 @@
-% EXPECT: unknown
-% EXIT: 0
+% Status: Satisfiable
 
 %--------------------------------------------------------------------------
 
diff --git a/test/regress/regress0/tptp_parser6.p b/test/regress/regress0/tptp/tptp_parser6.p
index 799bc4c6d..6283eb29a 100644
--- a/test/regress/regress0/tptp_parser6.p
+++ b/test/regress/regress0/tptp/tptp_parser6.p
@@ -1,5 +1,4 @@
-% EXPECT: unknown
-% EXIT: 0
+% Status: Satisfiable
 
 %--------------------------------------------------------------------------
 
diff --git a/test/regress/regress0/tptp_parser7.p b/test/regress/regress0/tptp/tptp_parser7.p
index f87c3484c..73c2b3834 100644
--- a/test/regress/regress0/tptp_parser7.p
+++ b/test/regress/regress0/tptp/tptp_parser7.p
@@ -1,5 +1,4 @@
-% EXPECT: unknown
-% EXIT: 0
+% Status: Satisfiable
 
 %--------------------------------------------------------------------------
 
diff --git a/test/regress/regress0/tptp_parser8.p b/test/regress/regress0/tptp/tptp_parser8.p
index 4bb2694ea..da281151b 100644
--- a/test/regress/regress0/tptp_parser8.p
+++ b/test/regress/regress0/tptp/tptp_parser8.p
@@ -1,5 +1,4 @@
-% EXPECT: unknown
-% EXIT: 0
+% Status: Satisfiable
 
 %--------------------------------------------------------------------------
 include('tptp_parser7.p').
diff --git a/test/regress/regress0/tptp_parser9.p b/test/regress/regress0/tptp/tptp_parser9.p
index bcbb88598..9bed19702 100644
--- a/test/regress/regress0/tptp_parser9.p
+++ b/test/regress/regress0/tptp/tptp_parser9.p
@@ -1,5 +1,4 @@
-% EXPECT: unknown
-% EXIT: 0
+% Status: CounterSatisfiable
 
 %--------------------------------------------------------------------------
 
diff --git a/test/regress/run_regression b/test/regress/run_regression
index 084df6ac9..b740e8486 100755
--- a/test/regress/run_regression
+++ b/test/regress/run_regression
@@ -164,21 +164,35 @@ elif expr "$benchmark" : '.*\.cvc$' &>/dev/null; then
   fi
   command_line=`grep '^% COMMAND-LINE: ' "$benchmark" | sed 's,^% COMMAND-LINE: ,,'`
 elif expr "$benchmark" : '.*\.p$' &>/dev/null; then
-  proof_command=PROOFS-NOT-SUPPORTED-IN-SMTLIB-V1;
+  proof_command=PROOFS-NOT-SUPPORTED-IN-TPTP;
   lang=tptp
+  command_line=--finite-model-find
   expected_proof=`grep '^% PROOF' "$benchmark" &>/dev/null && echo yes`
   expected_output=$(grep '^% EXPECT: ' "$benchmark")
   expected_error=`grep '^% EXPECT-ERROR: ' "$benchmark" | sed 's,^% EXPECT-ERROR: ,,'`
   if [ -z "$expected_output" -a -z "$expected_error" ]; then
-    error "cannot determine expected output of \`$benchmark': " \
-          "please use \`% EXPECT:' and/or \`% EXPECT-ERROR:' gestures"
+    if grep -q '^% Status *: ' "$benchmark"; then
+      expected_output="$(grep '^% *Status *: ' "$benchmark" | head -1 | awk '{print$NF}')"
+      case "$expected_output" in
+        Theorem|Unsatisfiable) expected_exit_status=20 ;;
+        CounterSatisfiable|Satisfiable) expected_exit_status=10 ;;
+        GaveUp) expected_exit_status=0 ;;
+      esac
+      expected_output="% SZS status $expected_output for $(basename "$benchmark" | sed 's,\.p$,,')"
+    else
+      error "cannot determine expected output of \`$benchmark': " \
+            "please use \`% EXPECT:' and/or \`% EXPECT-ERROR:' gestures"
+    fi
+  else
+    expected_output=$(echo "$expected_output" | perl -pe 's,^% EXPECT: ,,;s,\r,,')
+    expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark" | perl -pe 's,^% EXIT: ,,;s,\r,,'`
   fi
-  expected_output=$(echo "$expected_output" | perl -pe 's,^% EXPECT: ,,;s,\r,,')
-  expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark" | perl -pe 's,^% EXIT: ,,;s,\r,,'`
   if [ -z "$expected_exit_status" ]; then
     error "cannot determine expected exit status of \`$benchmark': please use \`% EXIT:' gesture"
   fi
-  command_line=`grep '^% COMMAND-LINE: ' "$benchmark" | sed 's,^% COMMAND-LINE: ,,'`
+  if grep -q '^% COMMAND-LINE: ' "$benchmark"; then
+    command_line=`grep '^% COMMAND-LINE: ' "$benchmark" | sed 's,^% COMMAND-LINE: ,,'`
+  fi
 else
   error "benchmark \`$benchmark' must be *.cvc or *.smt or *.smt2 or *.p"
 fi
author	Morgan Deters <mdeters@cs.nyu.edu>	2013-06-24 19:58:37 -0400
committer	Morgan Deters <mdeters@cs.nyu.edu>	2013-07-11 17:15:59 -0400
commit	e80b93ca958bdbeb28959029868f6193b39a3f19 (patch)
tree	92218adf47348cb8011a41599e158b371f5659de
parent	b76afedab3a23525da478ba4a8687c882793ea81 (diff)