%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : LCL396-1 : TPTP v9.3.1. Released v2.3.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n004.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:58:24 PM UTC 2026
% Result : Unsatisfiable 68.66s 68.99s
% Output : CNFRefutation 68.66s
% Verified :
% SZS Type : Refutation
% Derivation depth : 32
% Number of leaves : 5
% Syntax : Number of clauses : 55 ( 38 unt; 0 nHn; 12 RR)
% Number of literals : 73 ( 0 equ; 19 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 : 134 ( 34 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(prove_cn_62,negated_conjecture,
~ is_a_theorem(implies(implies(not(not(x)),y),implies(x,y))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_cn_62) ).
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(X26,X28))
| is_a_theorem(implies(implies(X28,X27),implies(X26,X27))) ),
inference(resolution,[status(thm)],[cn_1,condensed_detachment]) ).
cnf(cn_3,axiom,
is_a_theorem(implies(X4,implies(not(X4),X3))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cn_3) ).
cnf(c16,plain,
is_a_theorem(implies(implies(implies(not(X31),X32),X33),implies(X31,X33))),
inference(resolution,[status(thm)],[c5,cn_3]) ).
cnf(c21,plain,
( ~ is_a_theorem(implies(implies(not(X49),X50),X51))
| is_a_theorem(implies(X49,X51)) ),
inference(resolution,[status(thm)],[c16,condensed_detachment]) ).
cnf(c15,plain,
is_a_theorem(implies(implies(implies(implies(X111,X110),implies(X112,X110)),X113),implies(implies(X112,X111),X113))),
inference(resolution,[status(thm)],[c5,cn_1]) ).
cnf(c117,plain,
( ~ is_a_theorem(implies(implies(implies(X1487,X1486),implies(X1484,X1486)),X1485))
| is_a_theorem(implies(implies(X1484,X1487),X1485)) ),
inference(resolution,[status(thm)],[c15,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(c22,plain,
is_a_theorem(implies(implies(implies(X182,X184),X183),implies(implies(implies(not(X182),X181),X184),X183))),
inference(resolution,[status(thm)],[c16,c5]) ).
cnf(c0,plain,
( ~ is_a_theorem(X7)
| is_a_theorem(implies(not(X7),X8)) ),
inference(resolution,[status(thm)],[condensed_detachment,cn_3]) ).
cnf(c42,plain,
is_a_theorem(implies(X56,X56)),
inference(resolution,[status(thm)],[c21,cn_2]) ).
cnf(c53,plain,
is_a_theorem(implies(not(implies(X60,X60)),X61)),
inference(resolution,[status(thm)],[c42,c0]) ).
cnf(c63,plain,
is_a_theorem(implies(implies(X115,X116),implies(not(implies(X114,X114)),X116))),
inference(resolution,[status(thm)],[c53,c5]) ).
cnf(c124,plain,
is_a_theorem(implies(X119,implies(not(implies(X117,X117)),X118))),
inference(resolution,[status(thm)],[c63,c21]) ).
cnf(c131,plain,
is_a_theorem(implies(implies(implies(not(implies(X216,X216)),X218),X219),implies(X217,X219))),
inference(resolution,[status(thm)],[c124,c5]) ).
cnf(c255,plain,
( ~ is_a_theorem(implies(implies(not(implies(X223,X223)),X220),X221))
| is_a_theorem(implies(X222,X221)) ),
inference(resolution,[status(thm)],[c131,condensed_detachment]) ).
cnf(c12,plain,
is_a_theorem(implies(implies(X29,X30),implies(implies(not(X29),X29),X30))),
inference(resolution,[status(thm)],[c5,cn_2]) ).
cnf(c18,plain,
( ~ is_a_theorem(implies(X35,X34))
| is_a_theorem(implies(implies(not(X35),X35),X34)) ),
inference(resolution,[status(thm)],[c12,condensed_detachment]) ).
cnf(c26,plain,
is_a_theorem(implies(implies(not(implies(X250,X249)),implies(X250,X249)),implies(implies(not(X250),X250),X249))),
inference(resolution,[status(thm)],[c18,c12]) ).
cnf(c299,plain,
is_a_theorem(implies(X266,implies(implies(not(X265),X265),X265))),
inference(resolution,[status(thm)],[c26,c255]) ).
cnf(c343,plain,
is_a_theorem(implies(implies(implies(implies(not(X909),X909),X909),X908),implies(X907,X908))),
inference(resolution,[status(thm)],[c299,c5]) ).
cnf(c771,plain,
( ~ is_a_theorem(implies(implies(implies(not(X1103),X1103),X1103),X1104))
| is_a_theorem(implies(X1102,X1104)) ),
inference(resolution,[status(thm)],[c343,condensed_detachment]) ).
cnf(c929,plain,
is_a_theorem(implies(X1177,implies(implies(implies(not(not(X1178)),X1176),X1178),X1178))),
inference(resolution,[status(thm)],[c771,c22]) ).
cnf(c1011,plain,
is_a_theorem(implies(implies(implies(not(not(X1179)),X1180),X1179),X1179)),
inference(resolution,[status(thm)],[c929,c1]) ).
cnf(c1020,plain,
( ~ is_a_theorem(implies(implies(not(not(X1187)),X1186),X1187))
| is_a_theorem(X1187) ),
inference(resolution,[status(thm)],[c1011,condensed_detachment]) ).
cnf(c1193,plain,
is_a_theorem(implies(implies(X2088,implies(not(X2090),X2090)),implies(X2089,implies(X2088,X2090)))),
inference(resolution,[status(thm)],[c117,c343]) ).
cnf(c2105,plain,
( ~ is_a_theorem(implies(X2408,implies(not(X2406),X2406)))
| is_a_theorem(implies(X2407,implies(X2408,X2406))) ),
inference(resolution,[status(thm)],[c1193,condensed_detachment]) ).
cnf(c2114,plain,
is_a_theorem(implies(implies(not(X4972),X4974),implies(X4973,implies(implies(X4974,X4972),X4972)))),
inference(resolution,[status(thm)],[c1193,c117]) ).
cnf(c28,plain,
is_a_theorem(implies(implies(not(implies(X277,X279)),implies(X277,X279)),implies(implies(X279,X278),implies(X277,X278)))),
inference(resolution,[status(thm)],[c18,cn_1]) ).
cnf(c351,plain,
( ~ is_a_theorem(implies(not(implies(X4531,X4530)),implies(X4531,X4530)))
| is_a_theorem(implies(implies(X4530,X4529),implies(X4531,X4529))) ),
inference(resolution,[status(thm)],[c28,condensed_detachment]) ).
cnf(c6498,plain,
is_a_theorem(implies(X4985,implies(X4984,implies(implies(X4983,X4985),X4985)))),
inference(resolution,[status(thm)],[c2114,c21]) ).
cnf(c6510,plain,
is_a_theorem(implies(X4991,implies(X4992,implies(implies(X4993,X4992),X4992)))),
inference(resolution,[status(thm)],[c6498,c2105]) ).
cnf(c6558,plain,
is_a_theorem(implies(implies(implies(implies(X5251,X5250),X5250),X5252),implies(X5250,X5252))),
inference(resolution,[status(thm)],[c6510,c351]) ).
cnf(c7601,plain,
( ~ is_a_theorem(implies(implies(implies(X5388,X5386),X5386),X5387))
| is_a_theorem(implies(X5386,X5387)) ),
inference(resolution,[status(thm)],[c6558,condensed_detachment]) ).
cnf(c7669,plain,
is_a_theorem(implies(X5399,implies(X5398,X5399))),
inference(resolution,[status(thm)],[c7601,c343]) ).
cnf(c7802,plain,
is_a_theorem(implies(implies(implies(X5754,X5755),X5756),implies(X5755,X5756))),
inference(resolution,[status(thm)],[c7669,c5]) ).
cnf(c8771,plain,
( ~ is_a_theorem(implies(implies(X5889,X5890),X5888))
| is_a_theorem(implies(X5890,X5888)) ),
inference(resolution,[status(thm)],[c7802,condensed_detachment]) ).
cnf(c9168,plain,
is_a_theorem(implies(X6180,implies(X6181,implies(implies(X6180,X6182),X6182)))),
inference(resolution,[status(thm)],[c8771,c2114]) ).
cnf(c10339,plain,
is_a_theorem(implies(X6335,implies(X6336,implies(implies(X6336,X6337),X6337)))),
inference(resolution,[status(thm)],[c9168,c2105]) ).
cnf(c10897,plain,
is_a_theorem(implies(X6346,implies(implies(X6346,X6345),X6345))),
inference(resolution,[status(thm)],[c10339,c1020]) ).
cnf(c10958,plain,
( ~ is_a_theorem(X6363)
| is_a_theorem(implies(implies(X6363,X6362),X6362)) ),
inference(resolution,[status(thm)],[c10897,condensed_detachment]) ).
cnf(c11097,plain,
is_a_theorem(implies(implies(implies(implies(not(X7919),X7919),X7919),X7920),X7920)),
inference(resolution,[status(thm)],[c10958,cn_2]) ).
cnf(c15209,plain,
is_a_theorem(implies(implies(X8864,implies(not(X8865),X8865)),implies(X8864,X8865))),
inference(resolution,[status(thm)],[c11097,c117]) ).
cnf(c18724,plain,
is_a_theorem(implies(implies(not(X9905),X9906),implies(implies(X9906,X9905),X9905))),
inference(resolution,[status(thm)],[c15209,c117]) ).
cnf(c22077,plain,
( ~ is_a_theorem(implies(not(X10664),X10663))
| is_a_theorem(implies(implies(X10663,X10664),X10664)) ),
inference(resolution,[status(thm)],[c18724,condensed_detachment]) ).
cnf(c10892,plain,
is_a_theorem(implies(implies(implies(implies(X13003,X13002),X13002),X13001),implies(X13003,X13001))),
inference(resolution,[status(thm)],[c10339,c351]) ).
cnf(c28944,plain,
( ~ is_a_theorem(implies(implies(implies(X16488,X16489),X16489),X16487))
| is_a_theorem(implies(X16488,X16487)) ),
inference(resolution,[status(thm)],[c10892,condensed_detachment]) ).
cnf(c37919,plain,
is_a_theorem(implies(not(not(X16514)),X16514)),
inference(resolution,[status(thm)],[c28944,c1011]) ).
cnf(c38258,plain,
is_a_theorem(implies(implies(X16753,not(X16753)),not(X16753))),
inference(resolution,[status(thm)],[c37919,c22077]) ).
cnf(c40011,plain,
is_a_theorem(implies(X16755,not(not(X16755)))),
inference(resolution,[status(thm)],[c38258,c21]) ).
cnf(c40049,plain,
is_a_theorem(implies(implies(not(not(X19374)),X19375),implies(X19374,X19375))),
inference(resolution,[status(thm)],[c40011,c5]) ).
cnf(c57287,plain,
$false,
inference(resolution,[status(thm)],[c40049,prove_cn_62]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL396-1 : TPTP v9.3.1. Released v2.3.0.
% 0.00/0.04 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.11/0.36 % Computer : n004.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Sat Sep 5 06:46:14 UTC 2026
% 0.11/0.36 % CPUTime :
% 0.14/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.14/0.42 (re.compile("\."), Token.FullStop),
% 0.14/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.14/0.42 (re.compile("\("), Token.OpenPar),
% 0.14/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.14/0.42 (re.compile("\)"), Token.ClosePar),
% 0.14/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.14/0.42 (re.compile("\["), Token.OpenSquare),
% 0.14/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.14/0.42 (re.compile("\]"), Token.CloseSquare),
% 0.14/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.14/0.42 (re.compile("~\|"), Token.Nor),
% 0.14/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.14/0.42 (re.compile("\|"), Token.Or),
% 0.14/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.14/0.42 (re.compile("\?"), Token.Existential),
% 0.14/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.14/0.43 (re.compile("\s+"), Token.WhiteSpace),
% 0.14/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.14/0.43 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.14/0.49 /export/starexec/sandbox2/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.14/0.49 """
% 0.26/0.50 /export/starexec/sandbox2/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.26/0.50 """
% 0.34/0.59 /export/starexec/sandbox2/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.34/0.59 """
% 68.66/68.99 % Version: 1.5
% 68.66/68.99 % SZS status Unsatisfiable
% 68.66/68.99 % SZS output start CNFRefutation
% See solution above
% 68.66/68.99
% 68.66/68.99 % Initial clauses : 5
% 68.66/68.99 % Processed clauses : 1060
% 68.66/68.99 % Factors computed : 0
% 68.66/68.99 % Resolvents computed: 57331
% 68.66/68.99 % Tautologies deleted: 1
% 68.66/68.99 % Forward subsumed : 5107
% 68.66/68.99 % Backward subsumed : 159
% 68.66/68.99 % -------- CPU Time ---------
% 68.66/68.99 % User time : 68.448 s
% 68.66/68.99 % System time : 0.175 s
% 68.66/68.99 % Total time : 68.623 s
%------------------------------------------------------------------------------