%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : LCL400-1 : TPTP v9.3.1. Released v2.3.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n013.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:25 PM UTC 2026
% Result : Unsatisfiable 65.14s 65.49s
% Output : CNFRefutation 65.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 43
% Number of leaves : 5
% Syntax : Number of clauses : 69 ( 49 unt; 0 nHn; 14 RR)
% Number of literals : 90 ( 0 equ; 22 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 : 172 ( 53 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(prove_cn_66,negated_conjecture,
~ is_a_theorem(implies(not(implies(x,y)),x)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_cn_66) ).
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_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(c4,plain,
( ~ is_a_theorem(implies(X21,X23))
| is_a_theorem(implies(implies(X23,X22),implies(X21,X22))) ),
inference(resolution,[status(thm)],[cn_1,condensed_detachment]) ).
cnf(c16,plain,
is_a_theorem(implies(implies(implies(implies(X113,X111),implies(X110,X111)),X112),implies(implies(X110,X113),X112))),
inference(resolution,[status(thm)],[c4,cn_1]) ).
cnf(c115,plain,
( ~ is_a_theorem(implies(implies(implies(X1434,X1435),implies(X1437,X1435)),X1436))
| is_a_theorem(implies(implies(X1437,X1434),X1436)) ),
inference(resolution,[status(thm)],[c16,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_3,axiom,
is_a_theorem(implies(X3,implies(not(X3),X4))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cn_3) ).
cnf(c12,plain,
is_a_theorem(implies(implies(implies(not(X30),X29),X31),implies(X30,X31))),
inference(resolution,[status(thm)],[c4,cn_3]) ).
cnf(c17,plain,
is_a_theorem(implies(implies(implies(X130,X131),X128),implies(implies(implies(not(X130),X129),X131),X128))),
inference(resolution,[status(thm)],[c12,c4]) ).
cnf(c15,plain,
is_a_theorem(implies(implies(X32,X33),implies(implies(not(X32),X32),X33))),
inference(resolution,[status(thm)],[c4,cn_2]) ).
cnf(c18,plain,
( ~ is_a_theorem(implies(implies(not(X35),X34),X36))
| is_a_theorem(implies(X35,X36)) ),
inference(resolution,[status(thm)],[c12,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(c24,plain,
is_a_theorem(implies(X41,X41)),
inference(resolution,[status(thm)],[c18,cn_2]) ).
cnf(c33,plain,
is_a_theorem(implies(not(implies(X44,X44)),X43)),
inference(resolution,[status(thm)],[c24,c0]) ).
cnf(c35,plain,
is_a_theorem(implies(implies(X115,X116),implies(not(implies(X114,X114)),X116))),
inference(resolution,[status(thm)],[c33,c4]) ).
cnf(c123,plain,
is_a_theorem(implies(X117,implies(not(implies(X119,X119)),X118))),
inference(resolution,[status(thm)],[c35,c18]) ).
cnf(c125,plain,
is_a_theorem(implies(implies(implies(not(implies(X215,X215)),X217),X218),implies(X216,X218))),
inference(resolution,[status(thm)],[c123,c4]) ).
cnf(c252,plain,
( ~ is_a_theorem(implies(implies(not(implies(X220,X220)),X221),X222))
| is_a_theorem(implies(X219,X222)) ),
inference(resolution,[status(thm)],[c125,condensed_detachment]) ).
cnf(c260,plain,
is_a_theorem(implies(X224,implies(X223,X223))),
inference(resolution,[status(thm)],[c252,cn_2]) ).
cnf(c270,plain,
is_a_theorem(implies(implies(implies(X271,X271),X272),implies(X270,X272))),
inference(resolution,[status(thm)],[c260,c4]) ).
cnf(c308,plain,
( ~ is_a_theorem(implies(implies(X274,X274),X275))
| is_a_theorem(implies(X273,X275)) ),
inference(resolution,[status(thm)],[c270,condensed_detachment]) ).
cnf(c329,plain,
is_a_theorem(implies(X315,implies(implies(not(X316),X316),X316))),
inference(resolution,[status(thm)],[c308,c15]) ).
cnf(c379,plain,
is_a_theorem(implies(implies(implies(implies(not(X899),X899),X899),X900),implies(X898,X900))),
inference(resolution,[status(thm)],[c329,c4]) ).
cnf(c768,plain,
( ~ is_a_theorem(implies(implies(implies(not(X1168),X1168),X1168),X1169))
| is_a_theorem(implies(X1167,X1169)) ),
inference(resolution,[status(thm)],[c379,condensed_detachment]) ).
cnf(c996,plain,
is_a_theorem(implies(X1260,implies(implies(implies(not(not(X1261)),X1259),X1261),X1261))),
inference(resolution,[status(thm)],[c768,c17]) ).
cnf(c1027,plain,
is_a_theorem(implies(implies(implies(not(not(X1263)),X1262),X1263),X1263)),
inference(resolution,[status(thm)],[c996,c1]) ).
cnf(c1028,plain,
( ~ is_a_theorem(implies(implies(not(not(X1266)),X1267),X1266))
| is_a_theorem(X1266) ),
inference(resolution,[status(thm)],[c1027,condensed_detachment]) ).
cnf(c318,plain,
is_a_theorem(implies(X285,implies(X284,implies(X286,X286)))),
inference(resolution,[status(thm)],[c308,c270]) ).
cnf(c338,plain,
is_a_theorem(implies(implies(implies(X422,implies(X425,X425)),X423),implies(X424,X423))),
inference(resolution,[status(thm)],[c318,c4]) ).
cnf(c1202,plain,
is_a_theorem(implies(implies(X2127,implies(not(X2126),X2126)),implies(X2125,implies(X2127,X2126)))),
inference(resolution,[status(thm)],[c115,c379]) ).
cnf(c2234,plain,
( ~ is_a_theorem(implies(X2453,implies(not(X2455),X2455)))
| is_a_theorem(implies(X2454,implies(X2453,X2455))) ),
inference(resolution,[status(thm)],[c1202,condensed_detachment]) ).
cnf(c2875,plain,
is_a_theorem(implies(X3147,implies(implies(implies(X3146,implies(X3148,X3148)),X3149),X3149))),
inference(resolution,[status(thm)],[c2234,c338]) ).
cnf(c4006,plain,
is_a_theorem(implies(implies(implies(X3155,implies(X3153,X3153)),X3154),X3154)),
inference(resolution,[status(thm)],[c2875,c1028]) ).
cnf(c4044,plain,
( ~ is_a_theorem(implies(implies(X3188,implies(X3190,X3190)),X3189))
| is_a_theorem(X3189) ),
inference(resolution,[status(thm)],[c4006,condensed_detachment]) ).
cnf(c2241,plain,
is_a_theorem(implies(implies(not(X4683),X4684),implies(X4682,implies(implies(X4684,X4683),X4683)))),
inference(resolution,[status(thm)],[c1202,c115]) ).
cnf(c5941,plain,
is_a_theorem(implies(X4699,implies(X4701,implies(implies(X4700,X4699),X4699)))),
inference(resolution,[status(thm)],[c2241,c18]) ).
cnf(c5997,plain,
is_a_theorem(implies(X4713,implies(X4714,implies(implies(X4715,X4714),X4714)))),
inference(resolution,[status(thm)],[c5941,c2234]) ).
cnf(c6244,plain,
is_a_theorem(implies(X4716,implies(implies(X4717,X4716),X4716))),
inference(resolution,[status(thm)],[c5997,c4044]) ).
cnf(c6278,plain,
is_a_theorem(implies(implies(implies(implies(X5029,X5030),X5030),X5031),implies(X5030,X5031))),
inference(resolution,[status(thm)],[c6244,c4]) ).
cnf(c7171,plain,
( ~ is_a_theorem(implies(implies(implies(X5186,X5185),X5185),X5184))
| is_a_theorem(implies(X5185,X5184)) ),
inference(resolution,[status(thm)],[c6278,condensed_detachment]) ).
cnf(c7549,plain,
is_a_theorem(implies(X5195,implies(X5196,X5195))),
inference(resolution,[status(thm)],[c7171,c12]) ).
cnf(c7710,plain,
is_a_theorem(implies(implies(implies(X5583,X5582),X5584),implies(X5582,X5584))),
inference(resolution,[status(thm)],[c7549,c4]) ).
cnf(c8911,plain,
( ~ is_a_theorem(implies(implies(X5745,X5744),X5743))
| is_a_theorem(implies(X5744,X5743)) ),
inference(resolution,[status(thm)],[c7710,condensed_detachment]) ).
cnf(c9099,plain,
is_a_theorem(implies(X6060,implies(X6058,implies(implies(X6060,X6059),X6059)))),
inference(resolution,[status(thm)],[c8911,c2241]) ).
cnf(c9942,plain,
is_a_theorem(implies(X6160,implies(X6161,implies(implies(X6161,X6162),X6162)))),
inference(resolution,[status(thm)],[c9099,c2234]) ).
cnf(c10451,plain,
is_a_theorem(implies(X6166,implies(implies(X6166,X6165),X6165))),
inference(resolution,[status(thm)],[c9942,c4044]) ).
cnf(c10482,plain,
( ~ is_a_theorem(X6182)
| is_a_theorem(implies(implies(X6182,X6183),X6183)) ),
inference(resolution,[status(thm)],[c10451,condensed_detachment]) ).
cnf(c10817,plain,
is_a_theorem(implies(implies(implies(implies(not(X7595),X7595),X7595),X7594),X7594)),
inference(resolution,[status(thm)],[c10482,cn_2]) ).
cnf(c14130,plain,
is_a_theorem(implies(implies(X8736,implies(not(X8737),X8737)),implies(X8736,X8737))),
inference(resolution,[status(thm)],[c10817,c115]) ).
cnf(c17328,plain,
( ~ is_a_theorem(implies(X9115,implies(not(X9114),X9114)))
| is_a_theorem(implies(X9115,X9114)) ),
inference(resolution,[status(thm)],[c14130,condensed_detachment]) ).
cnf(c1160,plain,
is_a_theorem(implies(implies(X1504,not(X1505)),implies(X1505,implies(X1504,X1503)))),
inference(resolution,[status(thm)],[c115,c12]) ).
cnf(c1471,plain,
( ~ is_a_theorem(implies(X1582,not(X1581)))
| is_a_theorem(implies(X1581,implies(X1582,X1580))) ),
inference(resolution,[status(thm)],[c1160,condensed_detachment]) ).
cnf(c10493,plain,
is_a_theorem(implies(implies(implies(implies(X13057,X13058),X13058),X13059),implies(X13057,X13059))),
inference(resolution,[status(thm)],[c10451,c4]) ).
cnf(c29750,plain,
( ~ is_a_theorem(implies(implies(implies(X16602,X16601),X16601),X16603))
| is_a_theorem(implies(X16602,X16603)) ),
inference(resolution,[status(thm)],[c10493,condensed_detachment]) ).
cnf(c40691,plain,
is_a_theorem(implies(not(X16631),implies(X16631,X16630))),
inference(resolution,[status(thm)],[c29750,c12]) ).
cnf(c17335,plain,
is_a_theorem(implies(implies(not(X9471),X9472),implies(implies(X9472,X9471),X9471))),
inference(resolution,[status(thm)],[c14130,c115]) ).
cnf(c19301,plain,
( ~ is_a_theorem(implies(not(X10125),X10124))
| is_a_theorem(implies(implies(X10124,X10125),X10125)) ),
inference(resolution,[status(thm)],[c17335,condensed_detachment]) ).
cnf(c40874,plain,
is_a_theorem(implies(not(not(X16620)),X16620)),
inference(resolution,[status(thm)],[c29750,c1027]) ).
cnf(c41018,plain,
is_a_theorem(implies(implies(X16866,not(X16866)),not(X16866))),
inference(resolution,[status(thm)],[c40874,c19301]) ).
cnf(c42832,plain,
is_a_theorem(implies(X16876,not(not(X16876)))),
inference(resolution,[status(thm)],[c41018,c18]) ).
cnf(c42965,plain,
is_a_theorem(implies(implies(implies(X19822,not(not(X19822))),X19823),X19823)),
inference(resolution,[status(thm)],[c42832,c10482]) ).
cnf(c59827,plain,
is_a_theorem(implies(implies(X22711,X22712),implies(X22711,not(not(X22712))))),
inference(resolution,[status(thm)],[c42965,c115]) ).
cnf(c71573,plain,
( ~ is_a_theorem(implies(X23832,X23831))
| is_a_theorem(implies(X23832,not(not(X23831)))) ),
inference(resolution,[status(thm)],[c59827,condensed_detachment]) ).
cnf(c78957,plain,
is_a_theorem(implies(not(X23857),not(not(implies(X23857,X23856))))),
inference(resolution,[status(thm)],[c71573,c40691]) ).
cnf(c79200,plain,
is_a_theorem(implies(not(implies(X24122,X24121)),implies(not(X24122),X24120))),
inference(resolution,[status(thm)],[c78957,c1471]) ).
cnf(c81757,plain,
is_a_theorem(implies(not(implies(X24123,X24124)),X24123)),
inference(resolution,[status(thm)],[c79200,c17328]) ).
cnf(c81838,plain,
$false,
inference(resolution,[status(thm)],[c81757,prove_cn_66]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL400-1 : TPTP v9.3.1. Released v2.3.0.
% 0.00/0.03 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.08/0.35 % Computer : n013.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Fri Sep 4 18:17:50 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.13/0.38 /export/starexec/sandbox/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.13/0.38 (re.compile("\."), Token.FullStop),
% 0.13/0.38 /export/starexec/sandbox/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.13/0.38 (re.compile("\("), Token.OpenPar),
% 0.13/0.38 /export/starexec/sandbox/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.13/0.38 (re.compile("\)"), Token.ClosePar),
% 0.13/0.38 /export/starexec/sandbox/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.13/0.38 (re.compile("\["), Token.OpenSquare),
% 0.13/0.38 /export/starexec/sandbox/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.13/0.38 (re.compile("\]"), Token.CloseSquare),
% 0.13/0.38 /export/starexec/sandbox/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.13/0.38 (re.compile("~\|"), Token.Nor),
% 0.13/0.38 /export/starexec/sandbox/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.13/0.38 (re.compile("\|"), Token.Or),
% 0.13/0.38 /export/starexec/sandbox/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.13/0.38 (re.compile("\?"), Token.Existential),
% 0.13/0.38 /export/starexec/sandbox/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.13/0.38 (re.compile("\s+"), Token.WhiteSpace),
% 0.13/0.38 /export/starexec/sandbox/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.13/0.38 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.13/0.41 /export/starexec/sandbox/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.13/0.41 """
% 0.13/0.41 /export/starexec/sandbox/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.13/0.41 """
% 0.13/0.45 /export/starexec/sandbox/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.13/0.45 """
% 65.14/65.49 % Version: 1.5
% 65.14/65.49 % SZS status Unsatisfiable
% 65.14/65.49 % SZS output start CNFRefutation
% See solution above
% 65.14/65.49
% 65.14/65.49 % Initial clauses : 5
% 65.14/65.49 % Processed clauses : 1272
% 65.14/65.49 % Factors computed : 0
% 65.14/65.49 % Resolvents computed: 81856
% 65.14/65.49 % Tautologies deleted: 1
% 65.14/65.49 % Forward subsumed : 6565
% 65.14/65.49 % Backward subsumed : 193
% 65.14/65.49 % -------- CPU Time ---------
% 65.14/65.49 % User time : 65.007 s
% 65.14/65.49 % System time : 0.112 s
% 65.14/65.49 % Total time : 65.119 s
%------------------------------------------------------------------------------