%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : LCL092-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n006.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:50 PM UTC 2026
% Result : Unsatisfiable 30.06s 30.31s
% Output : CNFRefutation 30.06s
% Verified :
% SZS Type : Refutation
% Derivation depth : 35
% Number of leaves : 3
% Syntax : Number of clauses : 65 ( 41 unt; 0 nHn; 3 RR)
% Number of literals : 90 ( 0 equ; 26 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 2 ( 1 usr; 1 prp; 0-1 aty)
% Number of functors : 3 ( 3 usr; 2 con; 0-2 aty)
% Number of variables : 307 ( 192 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(prove_ic_3,negated_conjecture,
~ is_a_theorem(implies(implies(implies(a,b),a),a)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_ic_3) ).
cnf(condensed_detachment,axiom,
( ~ is_a_theorem(implies(X2,X3))
| ~ is_a_theorem(X2)
| is_a_theorem(X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',condensed_detachment) ).
cnf(ic_JLukasiewicz_5,axiom,
is_a_theorem(implies(implies(implies(X7,X4),implies(X8,X6)),implies(implies(X6,X7),implies(X5,implies(X8,X7))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ic_JLukasiewicz_5) ).
cnf(c0,plain,
( ~ is_a_theorem(implies(implies(X11,X12),implies(X10,X13)))
| is_a_theorem(implies(implies(X13,X11),implies(X9,implies(X10,X11)))) ),
inference(resolution,[status(thm)],[ic_JLukasiewicz_5,condensed_detachment]) ).
cnf(c1,plain,
is_a_theorem(implies(implies(implies(X15,implies(X16,X17)),implies(X17,X18)),implies(X14,implies(implies(X19,X17),implies(X17,X18))))),
inference(resolution,[status(thm)],[c0,ic_JLukasiewicz_5]) ).
cnf(c2,plain,
( ~ is_a_theorem(implies(implies(X23,implies(X21,X25)),implies(X25,X22)))
| is_a_theorem(implies(X20,implies(implies(X24,X25),implies(X25,X22)))) ),
inference(resolution,[status(thm)],[c1,condensed_detachment]) ).
cnf(c4,plain,
is_a_theorem(implies(X28,implies(implies(X26,X27),implies(X27,implies(implies(X29,X30),implies(X30,X27)))))),
inference(resolution,[status(thm)],[c2,c1]) ).
cnf(c6,plain,
( ~ is_a_theorem(X33)
| is_a_theorem(implies(implies(X34,X31),implies(X31,implies(implies(X35,X32),implies(X32,X31))))) ),
inference(resolution,[status(thm)],[c4,condensed_detachment]) ).
cnf(c8,plain,
is_a_theorem(implies(implies(X38,X36),implies(X36,implies(implies(X37,X39),implies(X39,X36))))),
inference(resolution,[status(thm)],[c6,c1]) ).
cnf(c12,plain,
is_a_theorem(implies(implies(implies(implies(X60,X62),implies(X62,X63)),X61),implies(X59,implies(X63,X61)))),
inference(resolution,[status(thm)],[c8,c0]) ).
cnf(c23,plain,
is_a_theorem(implies(X67,implies(implies(X64,X68),implies(X68,implies(X66,implies(X65,X68)))))),
inference(resolution,[status(thm)],[c12,c2]) ).
cnf(c25,plain,
( ~ is_a_theorem(X69)
| is_a_theorem(implies(implies(X73,X72),implies(X72,implies(X71,implies(X70,X72))))) ),
inference(resolution,[status(thm)],[c23,condensed_detachment]) ).
cnf(c29,plain,
is_a_theorem(implies(implies(X77,X75),implies(X75,implies(X76,implies(X74,X75))))),
inference(resolution,[status(thm)],[c25,c23]) ).
cnf(c36,plain,
is_a_theorem(implies(implies(implies(X118,implies(X115,X117)),X116),implies(X114,implies(X117,X116)))),
inference(resolution,[status(thm)],[c29,c0]) ).
cnf(c54,plain,
( ~ is_a_theorem(implies(implies(X120,implies(X122,X121)),X123))
| is_a_theorem(implies(X119,implies(X121,X123))) ),
inference(resolution,[status(thm)],[c36,condensed_detachment]) ).
cnf(c65,plain,
is_a_theorem(implies(X214,implies(X215,implies(implies(X215,X211),implies(X212,implies(X213,X211)))))),
inference(resolution,[status(thm)],[c54,ic_JLukasiewicz_5]) ).
cnf(c104,plain,
( ~ is_a_theorem(X237)
| is_a_theorem(implies(X235,implies(implies(X235,X236),implies(X238,implies(X234,X236))))) ),
inference(resolution,[status(thm)],[c65,condensed_detachment]) ).
cnf(c124,plain,
is_a_theorem(implies(X242,implies(implies(X242,X240),implies(X239,implies(X241,X240))))),
inference(resolution,[status(thm)],[c104,c23]) ).
cnf(c138,plain,
( ~ is_a_theorem(X316)
| is_a_theorem(implies(implies(X316,X315),implies(X314,implies(X313,X315)))) ),
inference(resolution,[status(thm)],[c124,condensed_detachment]) ).
cnf(c5,plain,
is_a_theorem(implies(X82,implies(implies(X78,implies(X81,X79)),implies(implies(X81,X79),implies(X79,implies(implies(X83,X80),implies(X80,X79))))))),
inference(resolution,[status(thm)],[c4,c2]) ).
cnf(c39,plain,
is_a_theorem(implies(implies(implies(implies(X602,X599),implies(X599,implies(implies(X603,X601),implies(X601,X599)))),X604),implies(X600,implies(implies(X605,implies(X602,X599)),X604)))),
inference(resolution,[status(thm)],[c5,c0]) ).
cnf(c338,plain,
is_a_theorem(implies(implies(implies(implies(implies(implies(X5724,X5722),implies(X5722,implies(implies(X5725,X5731),implies(X5731,X5722)))),X5729),implies(X5727,implies(implies(X5726,implies(X5724,X5722)),X5729))),X5723),implies(X5728,implies(X5730,X5723)))),
inference(resolution,[status(thm)],[c39,c138]) ).
cnf(c139,plain,
is_a_theorem(implies(implies(implies(X2027,implies(X2026,X2024)),X2025),implies(X2023,implies(implies(implies(X2025,X2028),X2024),X2025)))),
inference(resolution,[status(thm)],[c124,c0]) ).
cnf(c3,plain,
is_a_theorem(implies(implies(implies(implies(X53,X54),implies(X54,X50)),implies(X51,implies(X49,X54))),implies(X48,implies(X52,implies(X51,implies(X49,X54)))))),
inference(resolution,[status(thm)],[c1,c0]) ).
cnf(c35,plain,
( ~ is_a_theorem(implies(X110,X112))
| is_a_theorem(implies(X112,implies(X113,implies(X111,X112)))) ),
inference(resolution,[status(thm)],[c29,condensed_detachment]) ).
cnf(c50,plain,
is_a_theorem(implies(implies(X344,implies(X343,X342)),implies(X340,implies(X341,implies(X344,implies(X343,X342)))))),
inference(resolution,[status(thm)],[c35,c12]) ).
cnf(c179,plain,
( ~ is_a_theorem(implies(X598,implies(X594,X597)))
| is_a_theorem(implies(X595,implies(X596,implies(X598,implies(X594,X597))))) ),
inference(resolution,[status(thm)],[c50,condensed_detachment]) ).
cnf(c316,plain,
is_a_theorem(implies(X5358,implies(X5357,implies(implies(implies(implies(X5360,X5362),implies(X5362,X5361)),implies(X5356,implies(X5364,X5362))),implies(X5359,implies(X5363,implies(X5356,implies(X5364,X5362)))))))),
inference(resolution,[status(thm)],[c179,c3]) ).
cnf(c60,plain,
is_a_theorem(implies(X128,implies(X126,implies(X124,implies(X127,implies(X125,X126)))))),
inference(resolution,[status(thm)],[c54,c36]) ).
cnf(c66,plain,
( ~ is_a_theorem(X130)
| is_a_theorem(implies(X131,implies(X132,implies(X133,implies(X129,X131))))) ),
inference(resolution,[status(thm)],[c60,condensed_detachment]) ).
cnf(c71,plain,
is_a_theorem(implies(X143,implies(X141,implies(X144,implies(X142,X143))))),
inference(resolution,[status(thm)],[c66,c23]) ).
cnf(c84,plain,
is_a_theorem(implies(implies(implies(X537,implies(X535,implies(X533,X536))),X533),implies(X532,implies(X534,X533)))),
inference(resolution,[status(thm)],[c71,c0]) ).
cnf(c276,plain,
is_a_theorem(implies(implies(implies(X4790,X4794),implies(X4791,implies(X4792,implies(X4794,X4789)))),implies(X4788,implies(X4793,implies(X4791,implies(X4792,implies(X4794,X4789))))))),
inference(resolution,[status(thm)],[c84,c0]) ).
cnf(c14,plain,
is_a_theorem(implies(implies(implies(X166,implies(X161,implies(X168,X165))),implies(implies(X163,X165),implies(X165,X164))),implies(X162,implies(X167,implies(implies(X163,X165),implies(X165,X164)))))),
inference(resolution,[status(thm)],[c3,c0]) ).
cnf(c88,plain,
( ~ is_a_theorem(implies(implies(X1291,implies(X1296,implies(X1293,X1298))),implies(implies(X1292,X1298),implies(X1298,X1294))))
| is_a_theorem(implies(X1297,implies(X1295,implies(implies(X1292,X1298),implies(X1298,X1294))))) ),
inference(resolution,[status(thm)],[c14,condensed_detachment]) ).
cnf(c620,plain,
is_a_theorem(implies(X1455,implies(X1456,implies(implies(implies(X1452,X1453),X1453),implies(X1453,implies(X1454,X1453)))))),
inference(resolution,[status(thm)],[c88,ic_JLukasiewicz_5]) ).
cnf(c682,plain,
( ~ is_a_theorem(X1478)
| is_a_theorem(implies(X1480,implies(implies(implies(X1477,X1481),X1481),implies(X1481,implies(X1479,X1481))))) ),
inference(resolution,[status(thm)],[c620,condensed_detachment]) ).
cnf(c710,plain,
is_a_theorem(implies(X1482,implies(implies(implies(X1484,X1483),X1483),implies(X1483,implies(X1485,X1483))))),
inference(resolution,[status(thm)],[c682,c23]) ).
cnf(c750,plain,
( ~ is_a_theorem(X1682)
| is_a_theorem(implies(implies(implies(X1680,X1679),X1679),implies(X1679,implies(X1681,X1679)))) ),
inference(resolution,[status(thm)],[c710,condensed_detachment]) ).
cnf(c880,plain,
is_a_theorem(implies(implies(implies(X1685,X1684),X1684),implies(X1684,implies(X1683,X1684)))),
inference(resolution,[status(thm)],[c750,c23]) ).
cnf(c921,plain,
is_a_theorem(implies(implies(implies(X1956,X1957),implies(X1955,X1957)),implies(X1958,implies(X1957,implies(X1955,X1957))))),
inference(resolution,[status(thm)],[c880,c0]) ).
cnf(c22,plain,
is_a_theorem(implies(implies(implies(X368,X372),implies(implies(X369,X370),implies(X370,X368))),implies(X367,implies(X371,implies(implies(X369,X370),implies(X370,X368)))))),
inference(resolution,[status(thm)],[c12,c0]) ).
cnf(c217,plain,
( ~ is_a_theorem(implies(implies(X3876,X3875),implies(implies(X3877,X3880),implies(X3880,X3876))))
| is_a_theorem(implies(X3879,implies(X3878,implies(implies(X3877,X3880),implies(X3880,X3876))))) ),
inference(resolution,[status(thm)],[c22,condensed_detachment]) ).
cnf(c2151,plain,
is_a_theorem(implies(X3888,implies(X3885,implies(implies(X3889,X3886),implies(X3886,implies(X3887,X3886)))))),
inference(resolution,[status(thm)],[c217,c921]) ).
cnf(c2199,plain,
( ~ is_a_theorem(X5057)
| is_a_theorem(implies(X5059,implies(implies(X5056,X5058),implies(X5058,implies(X5055,X5058))))) ),
inference(resolution,[status(thm)],[c2151,condensed_detachment]) ).
cnf(c3728,plain,
is_a_theorem(implies(X5062,implies(implies(X5061,X5060),implies(X5060,implies(X5063,X5060))))),
inference(resolution,[status(thm)],[c2199,c276]) ).
cnf(c3854,plain,
( ~ is_a_theorem(X5715)
| is_a_theorem(implies(implies(X5714,X5712),implies(X5712,implies(X5713,X5712)))) ),
inference(resolution,[status(thm)],[c3728,condensed_detachment]) ).
cnf(c4320,plain,
is_a_theorem(implies(implies(X5716,X5717),implies(X5717,implies(X5718,X5717)))),
inference(resolution,[status(thm)],[c3854,c316]) ).
cnf(c55,plain,
is_a_theorem(implies(implies(implies(X1079,X1082),implies(X1078,implies(X1080,X1079))),implies(X1077,implies(X1081,implies(X1078,implies(X1080,X1079)))))),
inference(resolution,[status(thm)],[c36,c0]) ).
cnf(c525,plain,
( ~ is_a_theorem(implies(implies(X8102,X8105),implies(X8104,implies(X8103,X8102))))
| is_a_theorem(implies(X8107,implies(X8106,implies(X8104,implies(X8103,X8102))))) ),
inference(resolution,[status(thm)],[c55,condensed_detachment]) ).
cnf(c7057,plain,
is_a_theorem(implies(X8109,implies(X8108,implies(X8111,implies(X8110,X8111))))),
inference(resolution,[status(thm)],[c525,c4320]) ).
cnf(c7106,plain,
( ~ is_a_theorem(X8115)
| is_a_theorem(implies(X8114,implies(X8112,implies(X8113,X8112)))) ),
inference(resolution,[status(thm)],[c7057,condensed_detachment]) ).
cnf(c7112,plain,
is_a_theorem(implies(X8118,implies(X8117,implies(X8116,X8117)))),
inference(resolution,[status(thm)],[c7106,c338]) ).
cnf(c7299,plain,
( ~ is_a_theorem(X8917)
| is_a_theorem(implies(X8915,implies(X8916,X8915))) ),
inference(resolution,[status(thm)],[c7112,condensed_detachment]) ).
cnf(c7611,plain,
is_a_theorem(implies(X8918,implies(X8919,X8918))),
inference(resolution,[status(thm)],[c7299,c338]) ).
cnf(c7790,plain,
is_a_theorem(implies(implies(implies(X12839,X12841),X12839),implies(X12842,implies(X12840,X12839)))),
inference(resolution,[status(thm)],[c7611,c0]) ).
cnf(c10260,plain,
( ~ is_a_theorem(implies(implies(X13362,X13363),X13362))
| is_a_theorem(implies(X13364,implies(X13365,X13362))) ),
inference(resolution,[status(thm)],[c7790,condensed_detachment]) ).
cnf(c10552,plain,
is_a_theorem(implies(X16216,implies(X16217,implies(X16220,implies(implies(implies(X16219,X16218),X16219),X16219))))),
inference(resolution,[status(thm)],[c10260,c139]) ).
cnf(c11770,plain,
( ~ is_a_theorem(X20935)
| is_a_theorem(implies(X20933,implies(X20936,implies(implies(implies(X20934,X20932),X20934),X20934)))) ),
inference(resolution,[status(thm)],[c10552,condensed_detachment]) ).
cnf(c15588,plain,
is_a_theorem(implies(X20938,implies(X20939,implies(implies(implies(X20937,X20940),X20937),X20937)))),
inference(resolution,[status(thm)],[c11770,c338]) ).
cnf(c15940,plain,
( ~ is_a_theorem(X22911)
| is_a_theorem(implies(X22910,implies(implies(implies(X22908,X22909),X22908),X22908))) ),
inference(resolution,[status(thm)],[c15588,condensed_detachment]) ).
cnf(c17167,plain,
is_a_theorem(implies(X22914,implies(implies(implies(X22913,X22912),X22913),X22913))),
inference(resolution,[status(thm)],[c15940,c338]) ).
cnf(c17534,plain,
( ~ is_a_theorem(X24587)
| is_a_theorem(implies(implies(implies(X24585,X24586),X24585),X24585)) ),
inference(resolution,[status(thm)],[c17167,condensed_detachment]) ).
cnf(c18288,plain,
is_a_theorem(implies(implies(implies(X24588,X24589),X24588),X24588)),
inference(resolution,[status(thm)],[c17534,c338]) ).
cnf(c18646,plain,
$false,
inference(resolution,[status(thm)],[c18288,prove_ic_3]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL092-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.08/0.35 % Computer : n006.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 22:25:01 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.13/0.41 /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.23/0.49 /export/starexec/sandbox/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.23/0.49 """
% 0.23/0.49 /export/starexec/sandbox/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.23/0.49 """
% 0.32/0.58 /export/starexec/sandbox/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.32/0.58 """
% 30.06/30.31 % Version: 1.5
% 30.06/30.31 % SZS status Unsatisfiable
% 30.06/30.31 % SZS output start CNFRefutation
% See solution above
% 30.06/30.31
% 30.06/30.31 % Initial clauses : 3
% 30.06/30.31 % Processed clauses : 511
% 30.06/30.31 % Factors computed : 0
% 30.06/30.31 % Resolvents computed: 18664
% 30.06/30.31 % Tautologies deleted: 1
% 30.06/30.31 % Forward subsumed : 5010
% 30.06/30.31 % Backward subsumed : 125
% 30.06/30.31 % -------- CPU Time ---------
% 30.06/30.31 % User time : 29.898 s
% 30.06/30.31 % System time : 0.051 s
% 30.06/30.31 % Total time : 29.948 s
%------------------------------------------------------------------------------