%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : LCL405-1 : TPTP v9.3.1. Released v2.3.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n003.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:26 PM UTC 2026
% Result : Unsatisfiable 106.15s 106.40s
% Output : CNFRefutation 106.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 38
% Number of leaves : 5
% Syntax : Number of clauses : 80 ( 55 unt; 0 nHn; 17 RR)
% Number of literals : 106 ( 0 equ; 27 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 : 211 ( 61 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(prove_cn_71,negated_conjecture,
~ is_a_theorem(not(implies(implies(x,x),not(implies(y,y))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_cn_71) ).
cnf(condensed_detachment,axiom,
( ~ is_a_theorem(implies(X5,X6))
| ~ is_a_theorem(X5)
| is_a_theorem(X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',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(c1,plain,
( ~ is_a_theorem(implies(not(X9),X9))
| is_a_theorem(X9) ),
inference(resolution,[status(thm)],[condensed_detachment,cn_2]) ).
cnf(cn_1,axiom,
is_a_theorem(implies(implies(X10,X12),implies(implies(X12,X11),implies(X10,X11)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cn_1) ).
cnf(c5,plain,
( ~ is_a_theorem(implies(X28,X27))
| is_a_theorem(implies(implies(X27,X26),implies(X28,X26))) ),
inference(resolution,[status(thm)],[cn_1,condensed_detachment]) ).
cnf(cn_3,axiom,
is_a_theorem(implies(X3,implies(not(X3),X4))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cn_3) ).
cnf(c16,plain,
is_a_theorem(implies(implies(implies(not(X33),X31),X32),implies(X33,X32))),
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(c0,plain,
( ~ is_a_theorem(X8)
| is_a_theorem(implies(not(X8),X7)) ),
inference(resolution,[status(thm)],[condensed_detachment,cn_3]) ).
cnf(c44,plain,
is_a_theorem(implies(X56,X56)),
inference(resolution,[status(thm)],[c21,cn_2]) ).
cnf(c57,plain,
is_a_theorem(implies(not(implies(X67,X67)),X66)),
inference(resolution,[status(thm)],[c44,c0]) ).
cnf(c65,plain,
is_a_theorem(implies(implies(X114,X115),implies(not(implies(X116,X116)),X115))),
inference(resolution,[status(thm)],[c57,c5]) ).
cnf(c122,plain,
is_a_theorem(implies(X118,implies(not(implies(X119,X119)),X117))),
inference(resolution,[status(thm)],[c65,c21]) ).
cnf(c126,plain,
is_a_theorem(implies(implies(implies(not(implies(X217,X217)),X219),X218),implies(X216,X218))),
inference(resolution,[status(thm)],[c122,c5]) ).
cnf(c253,plain,
( ~ is_a_theorem(implies(implies(not(implies(X221,X221)),X223),X220))
| is_a_theorem(implies(X222,X220)) ),
inference(resolution,[status(thm)],[c126,condensed_detachment]) ).
cnf(c13,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)],[c13,condensed_detachment]) ).
cnf(c28,plain,
is_a_theorem(implies(implies(not(implies(X282,X281)),implies(X282,X281)),implies(implies(not(X282),X282),X281))),
inference(resolution,[status(thm)],[c18,c13]) ).
cnf(c341,plain,
is_a_theorem(implies(X284,implies(implies(not(X283),X283),X283))),
inference(resolution,[status(thm)],[c28,c253]) ).
cnf(c345,plain,
is_a_theorem(implies(implies(implies(implies(not(X1357),X1357),X1357),X1358),implies(X1356,X1358))),
inference(resolution,[status(thm)],[c341,c5]) ).
cnf(c1409,plain,
( ~ is_a_theorem(implies(implies(implies(not(X1829),X1829),X1829),X1830))
| is_a_theorem(implies(X1831,X1830)) ),
inference(resolution,[status(thm)],[c345,condensed_detachment]) ).
cnf(c258,plain,
is_a_theorem(implies(X228,implies(X227,X227))),
inference(resolution,[status(thm)],[c253,cn_2]) ).
cnf(c281,plain,
is_a_theorem(implies(implies(implies(X300,X300),X301),implies(X299,X301))),
inference(resolution,[status(thm)],[c258,c5]) ).
cnf(c364,plain,
is_a_theorem(implies(implies(implies(X5187,X5190),X5189),implies(implies(implies(X5188,X5188),X5190),X5189))),
inference(resolution,[status(thm)],[c281,c5]) ).
cnf(c8439,plain,
is_a_theorem(implies(X5192,implies(implies(implies(X5193,X5193),X5191),X5191))),
inference(resolution,[status(thm)],[c364,c1409]) ).
cnf(c8459,plain,
is_a_theorem(implies(implies(implies(X5195,X5195),X5194),X5194)),
inference(resolution,[status(thm)],[c8439,c1]) ).
cnf(c8515,plain,
( ~ is_a_theorem(implies(implies(X5222,X5222),X5221))
| is_a_theorem(X5221) ),
inference(resolution,[status(thm)],[c8459,condensed_detachment]) ).
cnf(c12,plain,
is_a_theorem(implies(implies(implies(implies(X77,X75),implies(X78,X75)),X76),implies(implies(X78,X77),X76))),
inference(resolution,[status(thm)],[c5,cn_1]) ).
cnf(c72,plain,
( ~ is_a_theorem(implies(implies(implies(X712,X711),implies(X714,X711)),X713))
| is_a_theorem(implies(implies(X714,X712),X713)) ),
inference(resolution,[status(thm)],[c12,condensed_detachment]) ).
cnf(c695,plain,
is_a_theorem(implies(implies(X783,not(X785)),implies(X785,implies(X783,X784)))),
inference(resolution,[status(thm)],[c72,c16]) ).
cnf(c906,plain,
( ~ is_a_theorem(implies(X864,not(X863)))
| is_a_theorem(implies(X863,implies(X864,X865))) ),
inference(resolution,[status(thm)],[c695,condensed_detachment]) ).
cnf(c8505,plain,
is_a_theorem(implies(X5580,implies(implies(implies(X5581,X5581),not(X5580)),X5579))),
inference(resolution,[status(thm)],[c8459,c906]) ).
cnf(c9086,plain,
is_a_theorem(implies(implies(implies(X6014,X6014),not(implies(X6015,X6015))),X6016)),
inference(resolution,[status(thm)],[c8505,c8515]) ).
cnf(c20,plain,
is_a_theorem(implies(implies(implies(X160,X162),X163),implies(implies(implies(not(X160),X161),X162),X163))),
inference(resolution,[status(thm)],[c16,c5]) ).
cnf(c210,plain,
( ~ is_a_theorem(implies(implies(X3114,X3113),X3112))
| is_a_theorem(implies(implies(implies(not(X3114),X3111),X3113),X3112)) ),
inference(resolution,[status(thm)],[c20,condensed_detachment]) ).
cnf(c1408,plain,
is_a_theorem(implies(implies(X1755,implies(not(X1756),X1756)),implies(X1757,implies(X1755,X1756)))),
inference(resolution,[status(thm)],[c345,c72]) ).
cnf(c1823,plain,
is_a_theorem(implies(implies(not(X10842),X10844),implies(X10843,implies(implies(X10844,X10842),X10842)))),
inference(resolution,[status(thm)],[c1408,c72]) ).
cnf(c692,plain,
is_a_theorem(implies(implies(X718,X720),implies(X719,implies(X718,X720)))),
inference(resolution,[status(thm)],[c72,c281]) ).
cnf(c710,plain,
is_a_theorem(implies(X725,implies(X726,implies(not(X725),X724)))),
inference(resolution,[status(thm)],[c692,c21]) ).
cnf(c721,plain,
is_a_theorem(implies(implies(implies(X1466,implies(not(X1467),X1468)),X1465),implies(X1467,X1465))),
inference(resolution,[status(thm)],[c710,c5]) ).
cnf(c1531,plain,
( ~ is_a_theorem(implies(implies(X2307,implies(not(X2308),X2309)),X2310))
| is_a_theorem(implies(X2308,X2310)) ),
inference(resolution,[status(thm)],[c721,condensed_detachment]) ).
cnf(c2460,plain,
is_a_theorem(implies(X2324,implies(X2325,implies(X2326,X2324)))),
inference(resolution,[status(thm)],[c1531,c1408]) ).
cnf(c2516,plain,
is_a_theorem(implies(implies(implies(X2660,implies(X2661,X2662)),X2659),implies(X2662,X2659))),
inference(resolution,[status(thm)],[c2460,c5]) ).
cnf(c3198,plain,
is_a_theorem(implies(X2666,implies(X2668,implies(X2667,X2668)))),
inference(resolution,[status(thm)],[c2516,c1409]) ).
cnf(c3213,plain,
is_a_theorem(implies(X2670,implies(X2669,X2670))),
inference(resolution,[status(thm)],[c3198,c1]) ).
cnf(c17,plain,
is_a_theorem(implies(implies(implies(implies(not(X129),X129),X128),X130),implies(implies(X129,X128),X130))),
inference(resolution,[status(thm)],[c13,c5]) ).
cnf(c135,plain,
( ~ is_a_theorem(implies(implies(implies(not(X1763),X1763),X1761),X1762))
| is_a_theorem(implies(implies(X1763,X1761),X1762)) ),
inference(resolution,[status(thm)],[c17,condensed_detachment]) ).
cnf(c3200,plain,
is_a_theorem(implies(implies(implies(X2835,X2834),X2833),implies(X2834,X2833))),
inference(resolution,[status(thm)],[c2516,c135]) ).
cnf(c3634,plain,
( ~ is_a_theorem(implies(implies(X2934,X2933),X2932))
| is_a_theorem(implies(X2933,X2932)) ),
inference(resolution,[status(thm)],[c3200,condensed_detachment]) ).
cnf(c21518,plain,
is_a_theorem(implies(X10858,implies(X10860,implies(implies(X10858,X10859),X10859)))),
inference(resolution,[status(thm)],[c1823,c3634]) ).
cnf(c21633,plain,
( ~ is_a_theorem(X10878)
| is_a_theorem(implies(X10877,implies(implies(X10878,X10879),X10879))) ),
inference(resolution,[status(thm)],[c21518,condensed_detachment]) ).
cnf(c21941,plain,
is_a_theorem(implies(X10988,implies(implies(implies(X10985,implies(X10987,X10985)),X10986),X10986))),
inference(resolution,[status(thm)],[c21633,c3213]) ).
cnf(c22488,plain,
is_a_theorem(implies(implies(implies(X10991,implies(X10993,X10991)),X10992),X10992)),
inference(resolution,[status(thm)],[c21941,c8515]) ).
cnf(c22567,plain,
( ~ is_a_theorem(implies(implies(X11090,implies(X11091,X11090)),X11092))
| is_a_theorem(X11092) ),
inference(resolution,[status(thm)],[c22488,condensed_detachment]) ).
cnf(c22926,plain,
is_a_theorem(implies(X11470,implies(implies(implies(X11471,not(X11469)),X11469),X11469))),
inference(resolution,[status(thm)],[c22567,c1823]) ).
cnf(c24205,plain,
is_a_theorem(implies(implies(implies(X11472,not(X11473)),X11473),X11473)),
inference(resolution,[status(thm)],[c22926,c8515]) ).
cnf(c24258,plain,
is_a_theorem(implies(implies(implies(not(implies(X14015,not(X14016))),X14017),X14016),X14016)),
inference(resolution,[status(thm)],[c24205,c210]) ).
cnf(c31251,plain,
( ~ is_a_theorem(implies(implies(not(implies(X14400,not(X14401))),X14399),X14401))
| is_a_theorem(X14401) ),
inference(resolution,[status(thm)],[c24258,condensed_detachment]) ).
cnf(c1824,plain,
( ~ is_a_theorem(implies(X14735,implies(not(X14734),X14734)))
| is_a_theorem(implies(X14736,implies(X14735,X14734))) ),
inference(resolution,[status(thm)],[c1408,condensed_detachment]) ).
cnf(c32451,plain,
is_a_theorem(implies(X14795,implies(X14796,implies(implies(X14796,X14797),X14797)))),
inference(resolution,[status(thm)],[c1824,c21518]) ).
cnf(c32764,plain,
is_a_theorem(implies(X14805,implies(implies(X14805,X14804),X14804))),
inference(resolution,[status(thm)],[c32451,c31251]) ).
cnf(c32871,plain,
( ~ is_a_theorem(X14832)
| is_a_theorem(implies(implies(X14832,X14833),X14833)) ),
inference(resolution,[status(thm)],[c32764,condensed_detachment]) ).
cnf(c32951,plain,
is_a_theorem(implies(implies(implies(implies(not(X15179),X15179),X15179),X15180),X15180)),
inference(resolution,[status(thm)],[c32871,cn_2]) ).
cnf(c34711,plain,
is_a_theorem(implies(implies(X15328,implies(not(X15329),X15329)),implies(X15328,X15329))),
inference(resolution,[status(thm)],[c32951,c72]) ).
cnf(c35855,plain,
is_a_theorem(implies(implies(not(X15941),X15942),implies(implies(X15942,X15941),X15941))),
inference(resolution,[status(thm)],[c34711,c72]) ).
cnf(c37032,plain,
( ~ is_a_theorem(implies(not(X16959),X16960))
| is_a_theorem(implies(implies(X16960,X16959),X16959)) ),
inference(resolution,[status(thm)],[c35855,condensed_detachment]) ).
cnf(c35871,plain,
( ~ is_a_theorem(implies(X15986,implies(not(X15985),X15985)))
| is_a_theorem(implies(X15986,X15985)) ),
inference(resolution,[status(thm)],[c34711,condensed_detachment]) ).
cnf(c33391,plain,
is_a_theorem(implies(implies(implies(X15218,implies(not(X15218),X15216)),X15217),X15217)),
inference(resolution,[status(thm)],[c32871,cn_3]) ).
cnf(c34780,plain,
( ~ is_a_theorem(implies(implies(X15675,implies(not(X15675),X15673)),X15674))
| is_a_theorem(X15674) ),
inference(resolution,[status(thm)],[c33391,condensed_detachment]) ).
cnf(c24,plain,
is_a_theorem(implies(implies(not(implies(X226,X225)),implies(X226,X225)),implies(implies(X225,X224),implies(X226,X224)))),
inference(resolution,[status(thm)],[c18,cn_1]) ).
cnf(c273,plain,
( ~ is_a_theorem(implies(not(implies(X4088,X4089)),implies(X4088,X4089)))
| is_a_theorem(implies(implies(X4089,X4090),implies(X4088,X4090))) ),
inference(resolution,[status(thm)],[c24,condensed_detachment]) ).
cnf(c32766,plain,
is_a_theorem(implies(implies(implies(implies(X19071,X19072),X19072),X19070),implies(X19071,X19070))),
inference(resolution,[status(thm)],[c32451,c273]) ).
cnf(c48834,plain,
is_a_theorem(implies(implies(X20558,implies(X20560,X20559)),implies(X20560,implies(X20558,X20559)))),
inference(resolution,[status(thm)],[c32766,c72]) ).
cnf(c50288,plain,
is_a_theorem(implies(not(X20565),implies(X20565,X20566))),
inference(resolution,[status(thm)],[c48834,c34780]) ).
cnf(c50341,plain,
is_a_theorem(implies(not(not(X20567)),X20567)),
inference(resolution,[status(thm)],[c50288,c35871]) ).
cnf(c50393,plain,
is_a_theorem(implies(implies(X20796,not(X20796)),not(X20796))),
inference(resolution,[status(thm)],[c50341,c37032]) ).
cnf(c51790,plain,
( ~ is_a_theorem(implies(X20926,not(X20926)))
| is_a_theorem(not(X20926)) ),
inference(resolution,[status(thm)],[c50393,condensed_detachment]) ).
cnf(c53349,plain,
is_a_theorem(not(implies(implies(X24406,X24406),not(implies(X24407,X24407))))),
inference(resolution,[status(thm)],[c51790,c9086]) ).
cnf(c72215,plain,
$false,
inference(resolution,[status(thm)],[c53349,prove_cn_71]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL405-1 : TPTP v9.3.1. Released v2.3.0.
% 0.00/0.04 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.10/0.36 % Computer : n003.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sat Sep 5 03:02:50 UTC 2026
% 0.13/0.36 % CPUTime :
% 0.13/0.42 /export/starexec/sandbox/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.13/0.42 (re.compile("\."), Token.FullStop),
% 0.13/0.42 /export/starexec/sandbox/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.13/0.42 (re.compile("\("), Token.OpenPar),
% 0.13/0.42 /export/starexec/sandbox/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.13/0.42 (re.compile("\)"), Token.ClosePar),
% 0.13/0.42 /export/starexec/sandbox/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.13/0.42 (re.compile("\["), Token.OpenSquare),
% 0.13/0.42 /export/starexec/sandbox/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.13/0.42 (re.compile("\]"), Token.CloseSquare),
% 0.13/0.42 /export/starexec/sandbox/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.13/0.42 (re.compile("~\|"), Token.Nor),
% 0.13/0.42 /export/starexec/sandbox/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.13/0.42 (re.compile("\|"), Token.Or),
% 0.13/0.42 /export/starexec/sandbox/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.13/0.42 (re.compile("\?"), Token.Existential),
% 0.13/0.42 /export/starexec/sandbox/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.13/0.42 (re.compile("\s+"), Token.WhiteSpace),
% 0.13/0.42 /export/starexec/sandbox/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.13/0.42 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.22/0.49 /export/starexec/sandbox/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.22/0.49 """
% 0.22/0.49 /export/starexec/sandbox/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.22/0.49 """
% 0.31/0.58 /export/starexec/sandbox/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.31/0.58 """
% 106.15/106.40 % Version: 1.5
% 106.15/106.40 % SZS status Unsatisfiable
% 106.15/106.40 % SZS output start CNFRefutation
% See solution above
% 106.15/106.40
% 106.15/106.40 % Initial clauses : 5
% 106.15/106.40 % Processed clauses : 1181
% 106.15/106.40 % Factors computed : 0
% 106.15/106.40 % Resolvents computed: 72243
% 106.15/106.40 % Tautologies deleted: 1
% 106.15/106.40 % Forward subsumed : 6298
% 106.15/106.40 % Backward subsumed : 116
% 106.15/106.40 % -------- CPU Time ---------
% 106.15/106.40 % User time : 105.835 s
% 106.15/106.40 % System time : 0.201 s
% 106.15/106.40 % Total time : 106.036 s
%------------------------------------------------------------------------------