diff --git a/examples/tptp/tptp5.cpp b/examples/tptp/tptp5.cpp
index d0e174914..00d03a8b0 100644
--- a/examples/tptp/tptp5.cpp
+++ b/examples/tptp/tptp5.cpp
@@ -1630,10 +1630,8 @@ public:
                 unsigned parent_id = Z3_get_ast_id(ctx, p.arg(0));
                 std::set<unsigned> const& hyps = m_proof_hypotheses.find(parent_id)->second;
                 print_hypotheses(out, hyps);
-                out << ").\n";
+                out << "))).\n";
                 break;                
-                display_inference(out, "lemma", "thm", p);
-                break;           
             }     
             case Z3_OP_PR_UNIT_RESOLUTION:                                 
                 display_inference(out, "unit_resolution", "thm", p);