1 files changed, 6 insertions, 24 deletions
diff --git a/src/printer/tptp/tptp_printer.cpp b/src/printer/tptp/tptp_printer.cpp
index 3c46a5849..923a7b3aa 100644
--- a/src/printer/tptp/tptp_printer.cpp
+++ b/src/printer/tptp/tptp_printer.cpp
@@ -13,17 +13,17 @@
  **
  ** 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>
+#include <vector>
+
+#include "expr/expr.h" // for ExprSetDepth etc..
+#include "expr/node_manager.h" // for VarNameAttr
+#include "options/language.h" // for LANG_AST
+#include "smt_util/command.h"
 
 using namespace std;
 
@@ -45,9 +45,6 @@ void TptpPrinter::toStream(std::ostream& out, const CommandStatus* s) const thro
   s->toStream(out, language::output::LANG_SMTLIB_V2_5);
 }/* TptpPrinter::toStream() */
 
-void TptpPrinter::toStream(std::ostream& out, const SExpr& sexpr) const throw() {
-  Printer::getPrinter(language::output::LANG_SMTLIB_V2_5)->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;
@@ -62,21 +59,6 @@ void TptpPrinter::toStream(std::ostream& out, const Model& m, const Command* c)
   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 */