%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : LCL004-1 : TPTP v9.3.1. Released v1.0.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:57:40 PM UTC 2026
% Result : Unsatisfiable 40.09s 40.48s
% Output : CNFRefutation 40.09s
% Verified :
% SZS Type : Refutation
% Derivation depth : 51
% Number of leaves : 3
% Syntax : Number of clauses : 67 ( 48 unt; 0 nHn; 4 RR)
% Number of literals : 87 ( 0 equ; 21 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 8 ( 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 : 278 ( 153 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(an_3,negated_conjecture,
~ is_a_theorem(or(not(a),or(b,a))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',an_3) ).
cnf(condensed_detachment,axiom,
( ~ is_a_theorem(or(not(X2),X3))
| ~ is_a_theorem(X2)
| is_a_theorem(X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',condensed_detachment) ).
cnf(an_CAMeredith,axiom,
is_a_theorem(or(not(or(not(or(not(X8),X4)),or(X5,or(X7,X6)))),or(not(or(not(X7),X8)),or(X5,or(X6,X8))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',an_CAMeredith) ).
cnf(c0,plain,
( ~ is_a_theorem(or(not(or(not(X13),X9)),or(X10,or(X11,X12))))
| is_a_theorem(or(not(or(not(X11),X13)),or(X10,or(X12,X13)))) ),
inference(resolution,[status(thm)],[an_CAMeredith,condensed_detachment]) ).
cnf(c1,plain,
is_a_theorem(or(not(or(not(X15),or(not(X18),X14))),or(not(or(not(X16),X18)),or(or(X17,X18),or(not(X18),X14))))),
inference(resolution,[status(thm)],[c0,an_CAMeredith]) ).
cnf(c2,plain,
is_a_theorem(or(not(or(not(or(X22,X19)),X20)),or(not(or(not(X23),X19)),or(or(not(X19),X21),X20)))),
inference(resolution,[status(thm)],[c1,c0]) ).
cnf(c4,plain,
is_a_theorem(or(not(or(not(or(not(X38),X37)),or(X36,X38))),or(not(or(not(X35),X38)),or(X34,or(X36,X38))))),
inference(resolution,[status(thm)],[c2,c0]) ).
cnf(c5,plain,
( ~ is_a_theorem(or(not(or(X25,X28)),X26))
| is_a_theorem(or(not(or(not(X24),X28)),or(or(not(X28),X27),X26))) ),
inference(resolution,[status(thm)],[c2,condensed_detachment]) ).
cnf(c14,plain,
( ~ is_a_theorem(or(not(or(not(X43),X40)),or(X41,X43)))
| is_a_theorem(or(not(or(not(X39),X43)),or(X42,or(X41,X43)))) ),
inference(resolution,[status(thm)],[c4,condensed_detachment]) ).
cnf(c16,plain,
is_a_theorem(or(not(or(not(X116),or(not(X117),or(X115,X117)))),or(X113,or(not(or(not(X114),X117)),or(not(X117),or(X115,X117)))))),
inference(resolution,[status(thm)],[c14,c4]) ).
cnf(c73,plain,
is_a_theorem(or(not(or(not(not(or(not(X119),X120))),X118)),or(X121,or(or(not(X120),or(X122,X120)),X118)))),
inference(resolution,[status(thm)],[c16,c0]) ).
cnf(c83,plain,
is_a_theorem(or(not(or(not(X151),X147)),or(or(not(X147),X146),or(X150,or(or(not(X148),or(X149,X148)),X147))))),
inference(resolution,[status(thm)],[c73,c5]) ).
cnf(c116,plain,
( ~ is_a_theorem(or(not(X155),X152))
| is_a_theorem(or(or(not(X152),X156),or(X153,or(or(not(X154),or(X157,X154)),X152)))) ),
inference(resolution,[status(thm)],[c83,condensed_detachment]) ).
cnf(c131,plain,
is_a_theorem(or(or(not(or(not(or(not(X3084),X3090)),or(X3089,or(X3087,X3090)))),X3083),or(X3086,or(or(not(X3088),or(X3085,X3088)),or(not(or(not(X3084),X3090)),or(X3089,or(X3087,X3090))))))),
inference(resolution,[status(thm)],[c116,c4]) ).
cnf(c3,plain,
( ~ is_a_theorem(or(not(X31),or(not(X29),X30)))
| is_a_theorem(or(not(or(not(X33),X29)),or(or(X32,X29),or(not(X29),X30)))) ),
inference(resolution,[status(thm)],[c1,condensed_detachment]) ).
cnf(c9,plain,
is_a_theorem(or(not(or(not(X123),or(not(X124),X128))),or(or(X125,or(not(X124),X128)),or(not(or(not(X124),X128)),or(or(not(X128),X127),X126))))),
inference(resolution,[status(thm)],[c3,c2]) ).
cnf(c90,plain,
is_a_theorem(or(not(or(not(X2143),or(not(or(not(X2141),X2144)),or(or(not(X2144),X2138),X2140)))),or(X2139,or(or(X2142,or(not(X2141),X2144)),or(not(or(not(X2141),X2144)),or(or(not(X2144),X2138),X2140)))))),
inference(resolution,[status(thm)],[c9,c14]) ).
cnf(c74,plain,
( ~ is_a_theorem(or(not(X1235),or(not(X1238),or(X1239,X1238))))
| is_a_theorem(or(X1236,or(not(or(not(X1237),X1238)),or(not(X1238),or(X1239,X1238))))) ),
inference(resolution,[status(thm)],[c16,condensed_detachment]) ).
cnf(c115,plain,
is_a_theorem(or(not(or(not(X177),X178)),or(or(not(X176),X180),or(or(or(not(X179),or(X181,X179)),X176),X178)))),
inference(resolution,[status(thm)],[c83,c0]) ).
cnf(c155,plain,
is_a_theorem(or(not(or(not(or(or(not(X189),or(X192,X189)),X193)),X191)),or(or(not(X193),X190),or(X188,X191)))),
inference(resolution,[status(thm)],[c115,c0]) ).
cnf(c185,plain,
is_a_theorem(or(not(or(not(X205),X201)),or(or(not(X201),X200),or(or(not(X202),X203),or(X204,X201))))),
inference(resolution,[status(thm)],[c155,c5]) ).
cnf(c203,plain,
is_a_theorem(or(not(or(not(or(not(X217),X212)),X215)),or(or(not(X214),X213),or(or(X216,X214),X215)))),
inference(resolution,[status(thm)],[c185,c0]) ).
cnf(c234,plain,
( ~ is_a_theorem(or(not(or(not(X220),X219)),X222))
| is_a_theorem(or(or(not(X221),X218),or(or(X223,X221),X222))) ),
inference(resolution,[status(thm)],[c203,condensed_detachment]) ).
cnf(c17,plain,
is_a_theorem(or(not(or(not(X316),or(or(not(X318),X317),X318))),or(X315,or(not(or(not(X314),X318)),or(or(not(X318),X317),X318))))),
inference(resolution,[status(thm)],[c14,c2]) ).
cnf(c280,plain,
is_a_theorem(or(or(not(X841),X842),or(or(X846,X841),or(X840,or(not(or(not(X843),X844)),or(or(not(X844),X845),X844)))))),
inference(resolution,[status(thm)],[c17,c234]) ).
cnf(c273,plain,
is_a_theorem(or(not(or(not(not(or(not(X321),X322))),X319)),or(X320,or(or(or(not(X322),X323),X322),X319)))),
inference(resolution,[status(thm)],[c17,c0]) ).
cnf(c1077,plain,
is_a_theorem(or(X1241,or(not(or(not(X1242),X1243)),or(not(X1243),or(or(or(not(X1240),X1244),X1240),X1243))))),
inference(resolution,[status(thm)],[c74,c273]) ).
cnf(c1091,plain,
( ~ is_a_theorem(X1258)
| is_a_theorem(or(not(or(not(X1257),X1259)),or(not(X1259),or(or(or(not(X1261),X1260),X1261),X1259)))) ),
inference(resolution,[status(thm)],[c1077,condensed_detachment]) ).
cnf(c1178,plain,
is_a_theorem(or(not(or(not(X1265),X1264)),or(not(X1264),or(or(or(not(X1262),X1263),X1262),X1264)))),
inference(resolution,[status(thm)],[c1091,c280]) ).
cnf(c1274,plain,
is_a_theorem(or(not(or(not(or(or(not(X1768),X1767),X1768)),X1765)),or(not(X1766),or(X1766,X1765)))),
inference(resolution,[status(thm)],[c1178,c0]) ).
cnf(c1360,plain,
is_a_theorem(or(X1773,or(not(or(not(X1774),X1775)),or(not(X1775),or(X1775,X1775))))),
inference(resolution,[status(thm)],[c1274,c74]) ).
cnf(c1367,plain,
( ~ is_a_theorem(X1787)
| is_a_theorem(or(not(or(not(X1785),X1786)),or(not(X1786),or(X1786,X1786)))) ),
inference(resolution,[status(thm)],[c1360,condensed_detachment]) ).
cnf(c1400,plain,
is_a_theorem(or(not(or(not(X1789),X1788)),or(not(X1788),or(X1788,X1788)))),
inference(resolution,[status(thm)],[c1367,c280]) ).
cnf(c1512,plain,
is_a_theorem(or(not(or(not(X2147),X2148)),or(not(X2147),or(X2147,X2148)))),
inference(resolution,[status(thm)],[c1400,c0]) ).
cnf(c1775,plain,
is_a_theorem(or(not(or(not(X2151),X2151)),or(not(X2151),or(X2152,X2151)))),
inference(resolution,[status(thm)],[c1512,c0]) ).
cnf(c1875,plain,
is_a_theorem(or(X2193,or(not(or(not(X2194),X2196)),or(not(X2196),or(X2195,X2196))))),
inference(resolution,[status(thm)],[c1775,c74]) ).
cnf(c1886,plain,
( ~ is_a_theorem(X2200)
| is_a_theorem(or(not(or(not(X2198),X2197)),or(not(X2197),or(X2199,X2197)))) ),
inference(resolution,[status(thm)],[c1875,condensed_detachment]) ).
cnf(c1922,plain,
is_a_theorem(or(not(or(not(X2201),X2203)),or(not(X2203),or(X2202,X2203)))),
inference(resolution,[status(thm)],[c1886,c90]) ).
cnf(c2049,plain,
is_a_theorem(or(not(or(not(X2747),X2745)),or(not(X2746),or(X2746,X2745)))),
inference(resolution,[status(thm)],[c1922,c0]) ).
cnf(c2231,plain,
is_a_theorem(or(not(or(not(X2774),X2772)),or(not(X2774),or(X2773,X2772)))),
inference(resolution,[status(thm)],[c2049,c0]) ).
cnf(c2651,plain,
( ~ is_a_theorem(or(not(X2785),X2784))
| is_a_theorem(or(not(X2785),or(X2786,X2784))) ),
inference(resolution,[status(thm)],[c2231,condensed_detachment]) ).
cnf(c2057,plain,
is_a_theorem(or(not(or(not(X12540),or(X12539,X12541))),or(X12538,or(not(X12541),or(X12539,X12541))))),
inference(resolution,[status(thm)],[c1922,c14]) ).
cnf(c16819,plain,
( ~ is_a_theorem(or(not(X12556),or(X12559,X12558)))
| is_a_theorem(or(X12557,or(not(X12558),or(X12559,X12558)))) ),
inference(resolution,[status(thm)],[c2057,condensed_detachment]) ).
cnf(c2707,plain,
is_a_theorem(or(not(or(not(X2973),X2971)),or(X2974,or(not(X2972),or(X2972,X2971))))),
inference(resolution,[status(thm)],[c2651,c2049]) ).
cnf(c4687,plain,
is_a_theorem(or(not(or(not(not(X3110)),X3109)),or(X3112,or(or(X3110,X3111),X3109)))),
inference(resolution,[status(thm)],[c2707,c0]) ).
cnf(c5753,plain,
is_a_theorem(or(not(or(not(or(X8709,X8708)),not(X8709))),or(X8710,or(X8707,not(X8709))))),
inference(resolution,[status(thm)],[c4687,c0]) ).
cnf(c16947,plain,
is_a_theorem(or(X14826,or(not(or(X14825,not(X14827))),or(X14824,or(X14825,not(X14827)))))),
inference(resolution,[status(thm)],[c16819,c5753]) ).
cnf(c20386,plain,
( ~ is_a_theorem(X14868)
| is_a_theorem(or(not(or(X14867,not(X14866))),or(X14865,or(X14867,not(X14866))))) ),
inference(resolution,[status(thm)],[c16947,condensed_detachment]) ).
cnf(c20458,plain,
is_a_theorem(or(not(or(X14869,not(X14870))),or(X14871,or(X14869,not(X14870))))),
inference(resolution,[status(thm)],[c20386,c131]) ).
cnf(c20800,plain,
is_a_theorem(or(not(or(not(not(X16262)),X16262)),or(X16264,or(not(X16263),X16262)))),
inference(resolution,[status(thm)],[c20458,c0]) ).
cnf(c21524,plain,
is_a_theorem(or(X16349,or(not(or(not(X16348),X16350)),or(X16347,or(not(X16348),X16350))))),
inference(resolution,[status(thm)],[c20800,c16819]) ).
cnf(c22864,plain,
( ~ is_a_theorem(X16364)
| is_a_theorem(or(not(or(not(X16362),X16363)),or(X16361,or(not(X16362),X16363)))) ),
inference(resolution,[status(thm)],[c21524,condensed_detachment]) ).
cnf(c22937,plain,
is_a_theorem(or(not(or(not(X16374),X16373)),or(X16375,or(not(X16374),X16373)))),
inference(resolution,[status(thm)],[c22864,c131]) ).
cnf(c23295,plain,
is_a_theorem(or(not(or(not(not(X17791)),X17791)),or(X17793,or(X17792,X17791)))),
inference(resolution,[status(thm)],[c22937,c0]) ).
cnf(c23994,plain,
is_a_theorem(or(X17820,or(not(or(X17819,X17821)),or(X17818,or(X17819,X17821))))),
inference(resolution,[status(thm)],[c23295,c16819]) ).
cnf(c24488,plain,
( ~ is_a_theorem(X17860)
| is_a_theorem(or(not(or(X17859,X17858)),or(X17857,or(X17859,X17858)))) ),
inference(resolution,[status(thm)],[c23994,condensed_detachment]) ).
cnf(c24934,plain,
is_a_theorem(or(not(or(X17869,X17871)),or(X17870,or(X17869,X17871)))),
inference(resolution,[status(thm)],[c24488,c131]) ).
cnf(c25259,plain,
is_a_theorem(or(not(or(X19387,X19389)),or(X19388,or(X19386,or(X19387,X19389))))),
inference(resolution,[status(thm)],[c24934,c2651]) ).
cnf(c25953,plain,
is_a_theorem(or(not(or(not(X24419),X24416)),or(X24418,or(or(not(X24416),X24417),X24416)))),
inference(resolution,[status(thm)],[c25259,c0]) ).
cnf(c28806,plain,
is_a_theorem(or(not(or(not(or(not(X24449),X24450)),X24452)),or(X24451,or(X24449,X24452)))),
inference(resolution,[status(thm)],[c25953,c0]) ).
cnf(c28961,plain,
( ~ is_a_theorem(or(not(or(not(X24476),X24478)),X24475))
| is_a_theorem(or(X24477,or(X24476,X24475))) ),
inference(resolution,[status(thm)],[c28806,condensed_detachment]) ).
cnf(c29037,plain,
is_a_theorem(or(X24479,or(X24481,or(not(X24482),or(X24480,X24482))))),
inference(resolution,[status(thm)],[c28961,c1922]) ).
cnf(c29150,plain,
( ~ is_a_theorem(X24514)
| is_a_theorem(or(X24511,or(not(X24512),or(X24513,X24512)))) ),
inference(resolution,[status(thm)],[c29037,condensed_detachment]) ).
cnf(c29500,plain,
is_a_theorem(or(X24517,or(not(X24516),or(X24515,X24516)))),
inference(resolution,[status(thm)],[c29150,c131]) ).
cnf(c29849,plain,
( ~ is_a_theorem(X26200)
| is_a_theorem(or(not(X26199),or(X26198,X26199))) ),
inference(resolution,[status(thm)],[c29500,condensed_detachment]) ).
cnf(c30525,plain,
is_a_theorem(or(not(X26202),or(X26201,X26202))),
inference(resolution,[status(thm)],[c29849,c131]) ).
cnf(c30896,plain,
$false,
inference(resolution,[status(thm)],[c30525,an_3]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL004-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.11/0.43 % Computer : n004.cluster.edu
% 0.11/0.43 % Model : x86_64 x86_64
% 0.11/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.43 % Memory : 8046.5625MB
% 0.11/0.43 % OS : Linux 6.8.0-71-generic
% 0.11/0.43 % CPULimit : 300
% 0.11/0.43 % WCLimit : 300
% 0.11/0.43 % DateTime : Fri Sep 4 17:55:44 UTC 2026
% 0.11/0.43 % CPUTime :
% 0.14/0.49 /export/starexec/sandbox/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.14/0.49 (re.compile("\."), Token.FullStop),
% 0.14/0.49 /export/starexec/sandbox/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.14/0.49 (re.compile("\("), Token.OpenPar),
% 0.14/0.49 /export/starexec/sandbox/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.14/0.49 (re.compile("\)"), Token.ClosePar),
% 0.14/0.49 /export/starexec/sandbox/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.14/0.49 (re.compile("\["), Token.OpenSquare),
% 0.14/0.49 /export/starexec/sandbox/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.14/0.49 (re.compile("\]"), Token.CloseSquare),
% 0.14/0.49 /export/starexec/sandbox/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.14/0.49 (re.compile("~\|"), Token.Nor),
% 0.14/0.49 /export/starexec/sandbox/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.14/0.49 (re.compile("\|"), Token.Or),
% 0.14/0.49 /export/starexec/sandbox/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.14/0.49 (re.compile("\?"), Token.Existential),
% 0.14/0.49 /export/starexec/sandbox/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.14/0.49 (re.compile("\s+"), Token.WhiteSpace),
% 0.14/0.49 /export/starexec/sandbox/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.14/0.49 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.25/0.56 /export/starexec/sandbox/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.25/0.56 """
% 0.25/0.56 /export/starexec/sandbox/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.25/0.56 """
% 0.33/0.65 /export/starexec/sandbox/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.33/0.65 """
% 40.09/40.48 % Version: 1.5
% 40.09/40.48 % SZS status Unsatisfiable
% 40.09/40.48 % SZS output start CNFRefutation
% See solution above
% 40.09/40.48
% 40.09/40.48 % Initial clauses : 3
% 40.09/40.48 % Processed clauses : 754
% 40.09/40.48 % Factors computed : 0
% 40.09/40.48 % Resolvents computed: 30951
% 40.09/40.48 % Tautologies deleted: 0
% 40.09/40.48 % Forward subsumed : 4620
% 40.09/40.48 % Backward subsumed : 317
% 40.09/40.48 % -------- CPU Time ---------
% 40.09/40.48 % User time : 39.928 s
% 40.09/40.48 % System time : 0.113 s
% 40.09/40.48 % Total time : 40.041 s
%------------------------------------------------------------------------------