%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : LCL052-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n002.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Sep 7 12:57:45 PM UTC 2026
% Result : Unsatisfiable 26.35s 26.67s
% Output : CNFRefutation 26.35s
% Verified :
% SZS Type : Refutation
% Derivation depth : 33
% Number of leaves : 5
% Syntax : Number of clauses : 60 ( 41 unt; 0 nHn; 12 RR)
% Number of literals : 80 ( 0 equ; 21 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 2 ( 1 usr; 1 prp; 0-1 aty)
% Number of functors : 4 ( 4 usr; 2 con; 0-2 aty)
% Number of variables : 159 ( 51 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(prove_cn_24,negated_conjecture,
~ is_a_theorem(implies(implies(implies(a,b),a),a)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_cn_24) ).
cnf(condensed_detachment,axiom,
( ~ is_a_theorem(implies(X6,X5))
| ~ is_a_theorem(X6)
| is_a_theorem(X5) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',condensed_detachment) ).
cnf(cn_1,axiom,
is_a_theorem(implies(implies(X12,X11),implies(implies(X11,X10),implies(X12,X10)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cn_1) ).
cnf(c5,plain,
( ~ is_a_theorem(implies(X31,X30))
| is_a_theorem(implies(implies(X30,X32),implies(X31,X32))) ),
inference(resolution,[status(thm)],[cn_1,condensed_detachment]) ).
cnf(c20,plain,
is_a_theorem(implies(implies(implies(implies(X165,X168),implies(X166,X168)),X167),implies(implies(X166,X165),X167))),
inference(resolution,[status(thm)],[c5,cn_1]) ).
cnf(c207,plain,
( ~ is_a_theorem(implies(implies(implies(X2862,X2864),implies(X2863,X2864)),X2861))
| is_a_theorem(implies(implies(X2863,X2862),X2861)) ),
inference(resolution,[status(thm)],[c20,condensed_detachment]) ).
cnf(cn_2,axiom,
is_a_theorem(implies(implies(not(X2),X2),X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cn_2) ).
cnf(c1,plain,
( ~ is_a_theorem(implies(not(X9),X9))
| is_a_theorem(X9) ),
inference(resolution,[status(thm)],[condensed_detachment,cn_2]) ).
cnf(cn_3,axiom,
is_a_theorem(implies(X4,implies(not(X4),X3))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cn_3) ).
cnf(c19,plain,
is_a_theorem(implies(implies(implies(not(X35),X37),X36),implies(X35,X36))),
inference(resolution,[status(thm)],[c5,cn_3]) ).
cnf(c25,plain,
is_a_theorem(implies(implies(implies(X241,X242),X239),implies(implies(implies(not(X241),X240),X242),X239))),
inference(resolution,[status(thm)],[c19,c5]) ).
cnf(c17,plain,
is_a_theorem(implies(implies(X33,X34),implies(implies(not(X33),X33),X34))),
inference(resolution,[status(thm)],[c5,cn_2]) ).
cnf(c26,plain,
( ~ is_a_theorem(implies(implies(not(X62),X63),X61))
| is_a_theorem(implies(X62,X61)) ),
inference(resolution,[status(thm)],[c19,condensed_detachment]) ).
cnf(c0,plain,
( ~ is_a_theorem(X7)
| is_a_theorem(implies(not(X7),X8)) ),
inference(resolution,[status(thm)],[condensed_detachment,cn_3]) ).
cnf(c55,plain,
is_a_theorem(implies(X64,X64)),
inference(resolution,[status(thm)],[c26,cn_2]) ).
cnf(c60,plain,
is_a_theorem(implies(not(implies(X72,X72)),X73)),
inference(resolution,[status(thm)],[c55,c0]) ).
cnf(c67,plain,
is_a_theorem(implies(implies(X119,X120),implies(not(implies(X118,X118)),X120))),
inference(resolution,[status(thm)],[c60,c5]) ).
cnf(c120,plain,
is_a_theorem(implies(X121,implies(not(implies(X122,X122)),X123))),
inference(resolution,[status(thm)],[c67,c26]) ).
cnf(c125,plain,
is_a_theorem(implies(implies(implies(not(implies(X213,X213)),X216),X214),implies(X215,X214))),
inference(resolution,[status(thm)],[c120,c5]) ).
cnf(c249,plain,
( ~ is_a_theorem(implies(implies(not(implies(X219,X219)),X217),X220))
| is_a_theorem(implies(X218,X220)) ),
inference(resolution,[status(thm)],[c125,condensed_detachment]) ).
cnf(c258,plain,
is_a_theorem(implies(X221,implies(X222,X222))),
inference(resolution,[status(thm)],[c249,cn_2]) ).
cnf(c267,plain,
is_a_theorem(implies(implies(implies(X267,X267),X268),implies(X269,X268))),
inference(resolution,[status(thm)],[c258,c5]) ).
cnf(c310,plain,
( ~ is_a_theorem(implies(implies(X270,X270),X271))
| is_a_theorem(implies(X272,X271)) ),
inference(resolution,[status(thm)],[c267,condensed_detachment]) ).
cnf(c326,plain,
is_a_theorem(implies(X314,implies(implies(not(X313),X313),X313))),
inference(resolution,[status(thm)],[c310,c17]) ).
cnf(c381,plain,
is_a_theorem(implies(implies(implies(implies(not(X941),X941),X941),X939),implies(X940,X939))),
inference(resolution,[status(thm)],[c326,c5]) ).
cnf(c814,plain,
( ~ is_a_theorem(implies(implies(implies(not(X1154),X1154),X1154),X1153))
| is_a_theorem(implies(X1152,X1153)) ),
inference(resolution,[status(thm)],[c381,condensed_detachment]) ).
cnf(c940,plain,
is_a_theorem(implies(X1234,implies(implies(implies(not(not(X1235)),X1236),X1235),X1235))),
inference(resolution,[status(thm)],[c814,c25]) ).
cnf(c990,plain,
is_a_theorem(implies(implies(implies(not(not(X1243)),X1242),X1243),X1243)),
inference(resolution,[status(thm)],[c940,c1]) ).
cnf(c1009,plain,
( ~ is_a_theorem(implies(implies(not(not(X1247)),X1246),X1247))
| is_a_theorem(X1247) ),
inference(resolution,[status(thm)],[c990,condensed_detachment]) ).
cnf(c2978,plain,
is_a_theorem(implies(implies(X4508,implies(not(X4507),X4507)),implies(X4506,implies(X4508,X4507)))),
inference(resolution,[status(thm)],[c207,c381]) ).
cnf(c6204,plain,
( ~ is_a_theorem(implies(X6010,implies(not(X6011),X6011)))
| is_a_theorem(implies(X6009,implies(X6010,X6011))) ),
inference(resolution,[status(thm)],[c2978,condensed_detachment]) ).
cnf(c6209,plain,
is_a_theorem(implies(implies(not(X7367),X7368),implies(X7369,implies(implies(X7368,X7367),X7367)))),
inference(resolution,[status(thm)],[c2978,c207]) ).
cnf(c325,plain,
is_a_theorem(implies(X283,implies(X282,implies(X284,X284)))),
inference(resolution,[status(thm)],[c310,c267]) ).
cnf(c348,plain,
is_a_theorem(implies(implies(implies(X428,implies(X430,X430)),X427),implies(X429,X427))),
inference(resolution,[status(thm)],[c325,c5]) ).
cnf(c460,plain,
( ~ is_a_theorem(implies(implies(X469,implies(X470,X470)),X471))
| is_a_theorem(implies(X468,X471)) ),
inference(resolution,[status(thm)],[c348,condensed_detachment]) ).
cnf(c498,plain,
is_a_theorem(implies(X543,implies(not(implies(X542,implies(X541,X541))),X544))),
inference(resolution,[status(thm)],[c460,cn_3]) ).
cnf(c548,plain,
is_a_theorem(implies(implies(implies(not(implies(X6908,implies(X6906,X6906))),X6904),X6907),implies(X6905,X6907))),
inference(resolution,[status(thm)],[c498,c5]) ).
cnf(c23,plain,
( ~ is_a_theorem(implies(X46,X45))
| is_a_theorem(implies(implies(not(X46),X46),X45)) ),
inference(resolution,[status(thm)],[c17,condensed_detachment]) ).
cnf(c39,plain,
is_a_theorem(implies(implies(not(implies(X432,X431)),implies(X432,X431)),implies(implies(X431,X433),implies(X432,X433)))),
inference(resolution,[status(thm)],[c23,cn_1]) ).
cnf(c468,plain,
( ~ is_a_theorem(implies(not(implies(X6225,X6227)),implies(X6225,X6227)))
| is_a_theorem(implies(implies(X6227,X6226),implies(X6225,X6226))) ),
inference(resolution,[status(thm)],[c39,condensed_detachment]) ).
cnf(c11376,plain,
is_a_theorem(implies(X7380,implies(X7382,implies(implies(X7381,X7380),X7380)))),
inference(resolution,[status(thm)],[c6209,c26]) ).
cnf(c11435,plain,
is_a_theorem(implies(X7398,implies(X7397,implies(implies(X7396,X7397),X7397)))),
inference(resolution,[status(thm)],[c11376,c6204]) ).
cnf(c11847,plain,
is_a_theorem(implies(implies(implies(implies(X7594,X7595),X7595),X7593),implies(X7595,X7593))),
inference(resolution,[status(thm)],[c11435,c468]) ).
cnf(c12740,plain,
( ~ is_a_theorem(implies(implies(implies(X7782,X7783),X7783),X7784))
| is_a_theorem(implies(X7783,X7784)) ),
inference(resolution,[status(thm)],[c11847,condensed_detachment]) ).
cnf(c13022,plain,
is_a_theorem(implies(X7793,implies(X7792,X7793))),
inference(resolution,[status(thm)],[c12740,c548]) ).
cnf(c13203,plain,
is_a_theorem(implies(implies(implies(X8257,X8256),X8255),implies(X8256,X8255))),
inference(resolution,[status(thm)],[c13022,c5]) ).
cnf(c15272,plain,
( ~ is_a_theorem(implies(implies(X8460,X8461),X8459))
| is_a_theorem(implies(X8461,X8459)) ),
inference(resolution,[status(thm)],[c13203,condensed_detachment]) ).
cnf(c15579,plain,
is_a_theorem(implies(X8779,implies(X8778,implies(implies(X8779,X8777),X8777)))),
inference(resolution,[status(thm)],[c15272,c6209]) ).
cnf(c16152,plain,
is_a_theorem(implies(X8840,implies(X8838,implies(implies(X8838,X8839),X8839)))),
inference(resolution,[status(thm)],[c15579,c6204]) ).
cnf(c17074,plain,
is_a_theorem(implies(X8842,implies(implies(X8842,X8841),X8841))),
inference(resolution,[status(thm)],[c16152,c1009]) ).
cnf(c17117,plain,
( ~ is_a_theorem(X8860)
| is_a_theorem(implies(implies(X8860,X8859),X8859)) ),
inference(resolution,[status(thm)],[c17074,condensed_detachment]) ).
cnf(c17215,plain,
is_a_theorem(implies(implies(implies(implies(not(X10366),X10366),X10366),X10367),X10367)),
inference(resolution,[status(thm)],[c17117,cn_2]) ).
cnf(c22336,plain,
is_a_theorem(implies(implies(X11577,implies(not(X11576),X11576)),implies(X11577,X11576))),
inference(resolution,[status(thm)],[c17215,c207]) ).
cnf(c26023,plain,
is_a_theorem(implies(implies(not(X12608),X12609),implies(implies(X12609,X12608),X12608))),
inference(resolution,[status(thm)],[c22336,c207]) ).
cnf(c28245,plain,
( ~ is_a_theorem(implies(not(X13275),X13274))
| is_a_theorem(implies(implies(X13274,X13275),X13275)) ),
inference(resolution,[status(thm)],[c26023,condensed_detachment]) ).
cnf(c17069,plain,
is_a_theorem(implies(implies(implies(implies(X16170,X16168),X16168),X16169),implies(X16170,X16169))),
inference(resolution,[status(thm)],[c16152,c468]) ).
cnf(c37001,plain,
( ~ is_a_theorem(implies(implies(implies(X19532,X19531),X19531),X19533))
| is_a_theorem(implies(X19532,X19533)) ),
inference(resolution,[status(thm)],[c17069,condensed_detachment]) ).
cnf(c46678,plain,
is_a_theorem(implies(not(X19574),implies(X19574,X19575))),
inference(resolution,[status(thm)],[c37001,c19]) ).
cnf(c47027,plain,
is_a_theorem(implies(implies(implies(X19662,X19661),X19662),X19662)),
inference(resolution,[status(thm)],[c46678,c28245]) ).
cnf(c47289,plain,
$false,
inference(resolution,[status(thm)],[c47027,prove_cn_24]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL052-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.09/0.35 % Computer : n002.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Sat Sep 5 07:52:50 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.12/0.38 /export/starexec/sandbox2/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.12/0.38 (re.compile("\."), Token.FullStop),
% 0.12/0.38 /export/starexec/sandbox2/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.12/0.38 (re.compile("\("), Token.OpenPar),
% 0.12/0.38 /export/starexec/sandbox2/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.12/0.38 (re.compile("\)"), Token.ClosePar),
% 0.12/0.38 /export/starexec/sandbox2/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.12/0.38 (re.compile("\["), Token.OpenSquare),
% 0.12/0.38 /export/starexec/sandbox2/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.12/0.38 (re.compile("\]"), Token.CloseSquare),
% 0.12/0.38 /export/starexec/sandbox2/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.12/0.38 (re.compile("~\|"), Token.Nor),
% 0.12/0.38 /export/starexec/sandbox2/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.12/0.38 (re.compile("\|"), Token.Or),
% 0.12/0.38 /export/starexec/sandbox2/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.12/0.38 (re.compile("\?"), Token.Existential),
% 0.12/0.38 /export/starexec/sandbox2/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.12/0.38 (re.compile("\s+"), Token.WhiteSpace),
% 0.12/0.38 /export/starexec/sandbox2/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.12/0.38 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.12/0.42 /export/starexec/sandbox2/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.12/0.42 """
% 0.12/0.42 /export/starexec/sandbox2/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.12/0.42 """
% 0.12/0.46 /export/starexec/sandbox2/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.12/0.46 """
% 26.35/26.67 % Version: 1.5
% 26.35/26.67 % SZS status Unsatisfiable
% 26.35/26.67 % SZS output start CNFRefutation
% See solution above
% 26.35/26.67
% 26.35/26.67 % Initial clauses : 5
% 26.35/26.67 % Processed clauses : 1024
% 26.35/26.67 % Factors computed : 0
% 26.35/26.67 % Resolvents computed: 47354
% 26.35/26.67 % Tautologies deleted: 1
% 26.35/26.67 % Forward subsumed : 4885
% 26.35/26.67 % Backward subsumed : 66
% 26.35/26.67 % -------- CPU Time ---------
% 26.35/26.67 % User time : 26.253 s
% 26.35/26.67 % System time : 0.063 s
% 26.35/26.67 % Total time : 26.316 s
%------------------------------------------------------------------------------