%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : LCL380-1 : TPTP v9.3.1. Released v2.3.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:58:22 PM UTC 2026
% Result : Unsatisfiable 62.65s 62.92s
% Output : CNFRefutation 62.65s
% Verified :
% SZS Type : Refutation
% Derivation depth : 38
% Number of leaves : 5
% Syntax : Number of clauses : 67 ( 48 unt; 0 nHn; 12 RR)
% Number of literals : 87 ( 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 : 178 ( 57 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(prove_cn_41,negated_conjecture,
~ is_a_theorem(implies(implies(x,y),implies(not(not(x)),y))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_cn_41) ).
cnf(condensed_detachment,axiom,
( ~ is_a_theorem(implies(X6,X5))
| ~ is_a_theorem(X6)
| is_a_theorem(X5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',condensed_detachment) ).
cnf(cn_1,axiom,
is_a_theorem(implies(implies(X12,X10),implies(implies(X10,X11),implies(X12,X11)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cn_1) ).
cnf(c4,plain,
( ~ is_a_theorem(implies(X27,X26))
| is_a_theorem(implies(implies(X26,X28),implies(X27,X28))) ),
inference(resolution,[status(thm)],[cn_1,condensed_detachment]) ).
cnf(c14,plain,
is_a_theorem(implies(implies(implies(implies(X111,X113),implies(X112,X113)),X110),implies(implies(X112,X111),X110))),
inference(resolution,[status(thm)],[c4,cn_1]) ).
cnf(c114,plain,
( ~ is_a_theorem(implies(implies(implies(X1411,X1410),implies(X1412,X1410)),X1409))
| is_a_theorem(implies(implies(X1412,X1411),X1409)) ),
inference(resolution,[status(thm)],[c14,condensed_detachment]) ).
cnf(cn_2,axiom,
is_a_theorem(implies(implies(not(X2),X2),X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cn_2) ).
cnf(cn_3,axiom,
is_a_theorem(implies(X4,implies(not(X4),X3))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cn_3) ).
cnf(c15,plain,
is_a_theorem(implies(implies(implies(not(X30),X31),X29),implies(X30,X29))),
inference(resolution,[status(thm)],[c4,cn_3]) ).
cnf(c18,plain,
is_a_theorem(implies(implies(implies(X131,X128),X129),implies(implies(implies(not(X131),X130),X128),X129))),
inference(resolution,[status(thm)],[c15,c4]) ).
cnf(c133,plain,
( ~ is_a_theorem(implies(implies(X1630,X1629),X1628))
| is_a_theorem(implies(implies(implies(not(X1630),X1627),X1629),X1628)) ),
inference(resolution,[status(thm)],[c18,condensed_detachment]) ).
cnf(c1,plain,
( ~ is_a_theorem(implies(not(X9),X9))
| is_a_theorem(X9) ),
inference(resolution,[status(thm)],[condensed_detachment,cn_2]) ).
cnf(c16,plain,
is_a_theorem(implies(implies(X33,X32),implies(implies(not(X33),X33),X32))),
inference(resolution,[status(thm)],[c4,cn_2]) ).
cnf(c17,plain,
( ~ is_a_theorem(implies(implies(not(X36),X35),X34))
| is_a_theorem(implies(X36,X34)) ),
inference(resolution,[status(thm)],[c15,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(c26,plain,
is_a_theorem(implies(X41,X41)),
inference(resolution,[status(thm)],[c17,cn_2]) ).
cnf(c33,plain,
is_a_theorem(implies(not(implies(X43,X43)),X44)),
inference(resolution,[status(thm)],[c26,c0]) ).
cnf(c36,plain,
is_a_theorem(implies(implies(X116,X114),implies(not(implies(X115,X115)),X114))),
inference(resolution,[status(thm)],[c33,c4]) ).
cnf(c123,plain,
is_a_theorem(implies(X118,implies(not(implies(X117,X117)),X119))),
inference(resolution,[status(thm)],[c36,c17]) ).
cnf(c127,plain,
is_a_theorem(implies(implies(implies(not(implies(X215,X215)),X216),X214),implies(X217,X214))),
inference(resolution,[status(thm)],[c123,c4]) ).
cnf(c242,plain,
( ~ is_a_theorem(implies(implies(not(implies(X220,X220)),X221),X219))
| is_a_theorem(implies(X218,X219)) ),
inference(resolution,[status(thm)],[c127,condensed_detachment]) ).
cnf(c251,plain,
is_a_theorem(implies(X223,implies(X222,X222))),
inference(resolution,[status(thm)],[c242,cn_2]) ).
cnf(c263,plain,
is_a_theorem(implies(implies(implies(X270,X270),X269),implies(X271,X269))),
inference(resolution,[status(thm)],[c251,c4]) ).
cnf(c302,plain,
( ~ is_a_theorem(implies(implies(X272,X272),X274))
| is_a_theorem(implies(X273,X274)) ),
inference(resolution,[status(thm)],[c263,condensed_detachment]) ).
cnf(c306,plain,
is_a_theorem(implies(X307,implies(implies(not(X306),X306),X306))),
inference(resolution,[status(thm)],[c302,c16]) ).
cnf(c361,plain,
is_a_theorem(implies(implies(implies(implies(not(X839),X839),X839),X838),implies(X840,X838))),
inference(resolution,[status(thm)],[c306,c4]) ).
cnf(c723,plain,
( ~ is_a_theorem(implies(implies(implies(not(X1046),X1046),X1046),X1047))
| is_a_theorem(implies(X1045,X1047)) ),
inference(resolution,[status(thm)],[c361,condensed_detachment]) ).
cnf(c892,plain,
is_a_theorem(implies(X1140,implies(implies(implies(not(not(X1139)),X1141),X1139),X1139))),
inference(resolution,[status(thm)],[c723,c18]) ).
cnf(c949,plain,
is_a_theorem(implies(implies(implies(not(not(X1143)),X1142),X1143),X1143)),
inference(resolution,[status(thm)],[c892,c1]) ).
cnf(c955,plain,
( ~ is_a_theorem(implies(implies(not(not(X1151)),X1150),X1151))
| is_a_theorem(X1151) ),
inference(resolution,[status(thm)],[c949,condensed_detachment]) ).
cnf(c319,plain,
is_a_theorem(implies(X286,implies(X285,implies(X284,X284)))),
inference(resolution,[status(thm)],[c302,c263]) ).
cnf(c340,plain,
is_a_theorem(implies(implies(implies(X423,implies(X422,X422)),X421),implies(X424,X421))),
inference(resolution,[status(thm)],[c319,c4]) ).
cnf(c449,plain,
( ~ is_a_theorem(implies(implies(X461,implies(X463,X463)),X460))
| is_a_theorem(implies(X462,X460)) ),
inference(resolution,[status(thm)],[c340,condensed_detachment]) ).
cnf(c1164,plain,
is_a_theorem(implies(implies(X2085,implies(not(X2086),X2086)),implies(X2087,implies(X2085,X2086)))),
inference(resolution,[status(thm)],[c114,c361]) ).
cnf(c2222,plain,
is_a_theorem(implies(implies(not(X2454),X2453),implies(X2452,implies(implies(X2453,X2454),X2454)))),
inference(resolution,[status(thm)],[c1164,c114]) ).
cnf(c2775,plain,
is_a_theorem(implies(X2474,implies(X2471,implies(implies(implies(X2473,X2473),X2472),X2472)))),
inference(resolution,[status(thm)],[c2222,c449]) ).
cnf(c2972,plain,
is_a_theorem(implies(X2477,implies(implies(implies(X2476,X2476),X2475),X2475))),
inference(resolution,[status(thm)],[c2775,c955]) ).
cnf(c2995,plain,
is_a_theorem(implies(implies(implies(X2485,X2485),X2484),X2484)),
inference(resolution,[status(thm)],[c2972,c955]) ).
cnf(c3032,plain,
is_a_theorem(implies(implies(implies(not(implies(X2696,X2696)),X2697),X2698),X2698)),
inference(resolution,[status(thm)],[c2995,c133]) ).
cnf(c3298,plain,
( ~ is_a_theorem(implies(implies(not(implies(X2796,X2796)),X2795),X2797))
| is_a_theorem(X2797) ),
inference(resolution,[status(thm)],[c3032,condensed_detachment]) ).
cnf(c2225,plain,
( ~ is_a_theorem(implies(X3958,implies(not(X3956),X3956)))
| is_a_theorem(implies(X3957,implies(X3958,X3956))) ),
inference(resolution,[status(thm)],[c1164,condensed_detachment]) ).
cnf(c5338,plain,
is_a_theorem(implies(X4183,implies(implies(implies(X4182,implies(X4184,X4184)),X4181),X4181))),
inference(resolution,[status(thm)],[c2225,c340]) ).
cnf(c6055,plain,
is_a_theorem(implies(implies(implies(X4187,implies(X4188,X4188)),X4189),X4189)),
inference(resolution,[status(thm)],[c5338,c3298]) ).
cnf(c6091,plain,
( ~ is_a_theorem(implies(implies(X4242,implies(X4240,X4240)),X4241))
| is_a_theorem(X4241) ),
inference(resolution,[status(thm)],[c6055,condensed_detachment]) ).
cnf(c2767,plain,
is_a_theorem(implies(X2455,implies(X2457,implies(implies(X2456,X2455),X2455)))),
inference(resolution,[status(thm)],[c2222,c17]) ).
cnf(c5441,plain,
is_a_theorem(implies(X4002,implies(X4003,implies(implies(X4001,X4003),X4003)))),
inference(resolution,[status(thm)],[c2225,c2767]) ).
cnf(c5482,plain,
is_a_theorem(implies(X4011,implies(implies(X4010,X4011),X4011))),
inference(resolution,[status(thm)],[c5441,c3298]) ).
cnf(c5518,plain,
is_a_theorem(implies(implies(implies(implies(X4631,X4633),X4633),X4632),implies(X4633,X4632))),
inference(resolution,[status(thm)],[c5482,c4]) ).
cnf(c6623,plain,
is_a_theorem(implies(implies(X4796,implies(X4798,X4797)),implies(X4797,implies(X4796,X4797)))),
inference(resolution,[status(thm)],[c5518,c114]) ).
cnf(c6782,plain,
is_a_theorem(implies(X4799,implies(X4800,X4799))),
inference(resolution,[status(thm)],[c6623,c6091]) ).
cnf(c6813,plain,
is_a_theorem(implies(implies(implies(X5074,X5075),X5073),implies(X5075,X5073))),
inference(resolution,[status(thm)],[c6782,c4]) ).
cnf(c7595,plain,
( ~ is_a_theorem(implies(implies(X5196,X5195),X5197))
| is_a_theorem(implies(X5195,X5197)) ),
inference(resolution,[status(thm)],[c6813,condensed_detachment]) ).
cnf(c8099,plain,
is_a_theorem(implies(X5475,implies(X5476,implies(implies(X5475,X5474),X5474)))),
inference(resolution,[status(thm)],[c7595,c2222]) ).
cnf(c9177,plain,
is_a_theorem(implies(X5605,implies(X5604,implies(implies(X5604,X5603),X5603)))),
inference(resolution,[status(thm)],[c8099,c2225]) ).
cnf(c9917,plain,
is_a_theorem(implies(X5613,implies(implies(X5613,X5614),X5614))),
inference(resolution,[status(thm)],[c9177,c3298]) ).
cnf(c9963,plain,
( ~ is_a_theorem(X5629)
| is_a_theorem(implies(implies(X5629,X5628),X5628)) ),
inference(resolution,[status(thm)],[c9917,condensed_detachment]) ).
cnf(c9984,plain,
is_a_theorem(implies(implies(implies(implies(not(X7036),X7036),X7036),X7035),X7035)),
inference(resolution,[status(thm)],[c9963,cn_2]) ).
cnf(c13234,plain,
is_a_theorem(implies(implies(X7809,implies(not(X7810),X7810)),implies(X7809,X7810))),
inference(resolution,[status(thm)],[c9984,c114]) ).
cnf(c15647,plain,
( ~ is_a_theorem(implies(X8487,implies(not(X8486),X8486)))
| is_a_theorem(implies(X8487,X8486)) ),
inference(resolution,[status(thm)],[c13234,condensed_detachment]) ).
cnf(c10078,plain,
is_a_theorem(implies(implies(implies(X7055,implies(not(X7055),X7056)),X7054),X7054)),
inference(resolution,[status(thm)],[c9963,cn_3]) ).
cnf(c13315,plain,
( ~ is_a_theorem(implies(implies(X8067,implies(not(X8067),X8069)),X8068))
| is_a_theorem(X8068) ),
inference(resolution,[status(thm)],[c10078,condensed_detachment]) ).
cnf(c9964,plain,
is_a_theorem(implies(implies(implies(implies(X12549,X12548),X12548),X12547),implies(X12549,X12547))),
inference(resolution,[status(thm)],[c9917,c4]) ).
cnf(c28303,plain,
is_a_theorem(implies(implies(X16010,implies(X16011,X16012)),implies(X16011,implies(X16010,X16012)))),
inference(resolution,[status(thm)],[c9964,c114]) ).
cnf(c38451,plain,
is_a_theorem(implies(not(X16018),implies(X16018,X16017))),
inference(resolution,[status(thm)],[c28303,c13315]) ).
cnf(c38503,plain,
is_a_theorem(implies(not(not(X16019)),X16019)),
inference(resolution,[status(thm)],[c38451,c15647]) ).
cnf(c38532,plain,
is_a_theorem(implies(implies(X18347,X18346),implies(not(not(X18347)),X18346))),
inference(resolution,[status(thm)],[c38503,c4]) ).
cnf(c54889,plain,
$false,
inference(resolution,[status(thm)],[c38532,prove_cn_41]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL380-1 : TPTP v9.3.1. Released v2.3.0.
% 0.00/0.04 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.37 % Computer : n002.cluster.edu
% 0.12/0.37 % Model : x86_64 x86_64
% 0.12/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.37 % Memory : 8046.5625MB
% 0.12/0.37 % OS : Linux 6.8.0-71-generic
% 0.12/0.37 % CPULimit : 300
% 0.12/0.37 % WCLimit : 300
% 0.12/0.37 % DateTime : Sat Sep 5 10:02:05 UTC 2026
% 0.12/0.37 % CPUTime :
% 0.12/0.43 /export/starexec/sandbox/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.12/0.43 (re.compile("\."), Token.FullStop),
% 0.12/0.43 /export/starexec/sandbox/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.12/0.43 (re.compile("\("), Token.OpenPar),
% 0.12/0.43 /export/starexec/sandbox/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.12/0.43 (re.compile("\)"), Token.ClosePar),
% 0.12/0.43 /export/starexec/sandbox/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.12/0.43 (re.compile("\["), Token.OpenSquare),
% 0.12/0.43 /export/starexec/sandbox/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.12/0.43 (re.compile("\]"), Token.CloseSquare),
% 0.12/0.43 /export/starexec/sandbox/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.12/0.43 (re.compile("~\|"), Token.Nor),
% 0.12/0.43 /export/starexec/sandbox/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.12/0.43 (re.compile("\|"), Token.Or),
% 0.12/0.43 /export/starexec/sandbox/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.12/0.43 (re.compile("\?"), Token.Existential),
% 0.12/0.43 /export/starexec/sandbox/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.12/0.43 (re.compile("\s+"), Token.WhiteSpace),
% 0.12/0.43 /export/starexec/sandbox/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.12/0.43 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.22/0.50 /export/starexec/sandbox/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.22/0.50 """
% 0.22/0.50 /export/starexec/sandbox/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.22/0.50 """
% 0.33/0.59 /export/starexec/sandbox/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.33/0.59 """
% 62.65/62.92 % Version: 1.5
% 62.65/62.92 % SZS status Unsatisfiable
% 62.65/62.92 % SZS output start CNFRefutation
% See solution above
% 62.65/62.92
% 62.65/62.92 % Initial clauses : 5
% 62.65/62.92 % Processed clauses : 1017
% 62.65/62.92 % Factors computed : 0
% 62.65/62.92 % Resolvents computed: 54914
% 62.65/62.92 % Tautologies deleted: 1
% 62.65/62.92 % Forward subsumed : 4779
% 62.65/62.92 % Backward subsumed : 160
% 62.65/62.92 % -------- CPU Time ---------
% 62.65/62.92 % User time : 62.370 s
% 62.65/62.92 % System time : 0.161 s
% 62.65/62.92 % Total time : 62.531 s
%------------------------------------------------------------------------------