%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : LCL094-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n010.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 24.05s 24.37s
% Output : CNFRefutation 24.05s
% Verified :
% SZS Type : Refutation
% Derivation depth : 31
% Number of leaves : 3
% Syntax : Number of clauses : 56 ( 37 unt; 0 nHn; 6 RR)
% Number of literals : 76 ( 0 equ; 21 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 10 ( 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 : 214 ( 95 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(prove_ic_5,negated_conjecture,
~ is_a_theorem(implies(a,implies(implies(a,b),b))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_ic_5) ).
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_4,axiom,
is_a_theorem(implies(implies(implies(X4,X8),implies(X5,X6)),implies(X7,implies(implies(X6,X4),implies(X5,X4))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ic_JLukasiewicz_4) ).
cnf(c0,plain,
( ~ is_a_theorem(implies(implies(X11,X9),implies(X13,X10)))
| is_a_theorem(implies(X12,implies(implies(X10,X11),implies(X13,X11)))) ),
inference(resolution,[status(thm)],[ic_JLukasiewicz_4,condensed_detachment]) ).
cnf(c1,plain,
is_a_theorem(implies(X17,implies(implies(implies(implies(X15,X16),implies(X19,X16)),implies(X16,X14)),implies(X18,implies(X16,X14))))),
inference(resolution,[status(thm)],[c0,ic_JLukasiewicz_4]) ).
cnf(c2,plain,
is_a_theorem(implies(X21,implies(implies(implies(X22,implies(X24,X26)),X23),implies(implies(implies(implies(X20,X24),implies(X25,X24)),implies(X24,X26)),X23)))),
inference(resolution,[status(thm)],[c1,c0]) ).
cnf(c3,plain,
( ~ is_a_theorem(X30)
| is_a_theorem(implies(implies(implies(implies(X27,X29),implies(X31,X29)),implies(X29,X32)),implies(X28,implies(X29,X32)))) ),
inference(resolution,[status(thm)],[c1,condensed_detachment]) ).
cnf(c6,plain,
is_a_theorem(implies(implies(implies(implies(X37,X36),implies(X35,X36)),implies(X36,X34)),implies(X33,implies(X36,X34)))),
inference(resolution,[status(thm)],[c3,ic_JLukasiewicz_4]) ).
cnf(c10,plain,
( ~ is_a_theorem(implies(implies(implies(X49,X51),implies(X50,X51)),implies(X51,X48)))
| is_a_theorem(implies(X52,implies(X51,X48))) ),
inference(resolution,[status(thm)],[c6,condensed_detachment]) ).
cnf(c14,plain,
is_a_theorem(implies(X65,implies(implies(X67,X66),implies(X66,implies(X67,X66))))),
inference(resolution,[status(thm)],[c10,c6]) ).
cnf(c22,plain,
( ~ is_a_theorem(X116)
| is_a_theorem(implies(implies(X117,X118),implies(X118,implies(X117,X118)))) ),
inference(resolution,[status(thm)],[c14,condensed_detachment]) ).
cnf(c54,plain,
is_a_theorem(implies(implies(X119,X120),implies(X120,implies(X119,X120)))),
inference(resolution,[status(thm)],[c22,c6]) ).
cnf(c64,plain,
is_a_theorem(implies(X153,implies(implies(implies(X154,X152),X154),implies(X152,X154)))),
inference(resolution,[status(thm)],[c54,c0]) ).
cnf(c78,plain,
( ~ is_a_theorem(X166)
| is_a_theorem(implies(implies(implies(X167,X168),X167),implies(X168,X167))) ),
inference(resolution,[status(thm)],[c64,condensed_detachment]) ).
cnf(c83,plain,
is_a_theorem(implies(implies(implies(X169,X170),X169),implies(X170,X169))),
inference(resolution,[status(thm)],[c78,c6]) ).
cnf(c94,plain,
is_a_theorem(implies(X171,implies(X173,implies(X172,X173)))),
inference(resolution,[status(thm)],[c83,c10]) ).
cnf(c101,plain,
( ~ is_a_theorem(X185)
| is_a_theorem(implies(X187,implies(X186,X187))) ),
inference(resolution,[status(thm)],[c94,condensed_detachment]) ).
cnf(c117,plain,
is_a_theorem(implies(X189,implies(X188,X189))),
inference(resolution,[status(thm)],[c101,c94]) ).
cnf(c131,plain,
is_a_theorem(implies(X302,implies(implies(implies(X303,X301),X303),implies(X300,X303)))),
inference(resolution,[status(thm)],[c117,c0]) ).
cnf(c218,plain,
( ~ is_a_theorem(X547)
| is_a_theorem(implies(implies(implies(X550,X549),X550),implies(X548,X550))) ),
inference(resolution,[status(thm)],[c131,condensed_detachment]) ).
cnf(c397,plain,
is_a_theorem(implies(implies(implies(X553,X551),X553),implies(X552,X553))),
inference(resolution,[status(thm)],[c218,c2]) ).
cnf(c11,plain,
is_a_theorem(implies(X61,implies(X62,implies(implies(X62,X63),implies(X64,X63))))),
inference(resolution,[status(thm)],[c10,ic_JLukasiewicz_4]) ).
cnf(c19,plain,
( ~ is_a_theorem(X72)
| is_a_theorem(implies(X75,implies(implies(X75,X73),implies(X74,X73)))) ),
inference(resolution,[status(thm)],[c11,condensed_detachment]) ).
cnf(c24,plain,
is_a_theorem(implies(X78,implies(implies(X78,X77),implies(X76,X77)))),
inference(resolution,[status(thm)],[c19,c6]) ).
cnf(c31,plain,
( ~ is_a_theorem(X110)
| is_a_theorem(implies(implies(X110,X111),implies(X112,X111))) ),
inference(resolution,[status(thm)],[c24,condensed_detachment]) ).
cnf(c9,plain,
is_a_theorem(implies(X104,implies(implies(implies(X106,X101),implies(implies(X102,X106),implies(X105,X106))),implies(X103,implies(implies(X102,X106),implies(X105,X106)))))),
inference(resolution,[status(thm)],[c6,c0]) ).
cnf(c43,plain,
is_a_theorem(implies(X479,implies(implies(implies(X481,implies(implies(X482,X478),implies(X477,X478))),X480),implies(implies(implies(X478,X483),implies(implies(X482,X478),implies(X477,X478))),X480)))),
inference(resolution,[status(thm)],[c9,c0]) ).
cnf(c342,plain,
is_a_theorem(implies(implies(implies(X4737,implies(implies(implies(X4738,implies(implies(X4743,X4741),implies(X4742,X4741))),X4739),implies(implies(implies(X4741,X4745),implies(implies(X4743,X4741),implies(X4742,X4741))),X4739))),X4744),implies(X4740,X4744))),
inference(resolution,[status(thm)],[c43,c31]) ).
cnf(c428,plain,
is_a_theorem(implies(X1866,implies(implies(X1867,implies(X1867,X1865)),implies(X1864,implies(X1867,X1865))))),
inference(resolution,[status(thm)],[c397,c0]) ).
cnf(c1468,plain,
( ~ is_a_theorem(X4902)
| is_a_theorem(implies(implies(X4904,implies(X4904,X4905)),implies(X4903,implies(X4904,X4905)))) ),
inference(resolution,[status(thm)],[c428,condensed_detachment]) ).
cnf(c3486,plain,
is_a_theorem(implies(implies(X4912,implies(X4912,X4913)),implies(X4914,implies(X4912,X4913)))),
inference(resolution,[status(thm)],[c1468,c342]) ).
cnf(c3616,plain,
( ~ is_a_theorem(implies(X5492,implies(X5492,X5490)))
| is_a_theorem(implies(X5491,implies(X5492,X5490))) ),
inference(resolution,[status(thm)],[c3486,condensed_detachment]) ).
cnf(c4151,plain,
is_a_theorem(implies(X5536,implies(implies(implies(X5534,X5535),X5534),X5534))),
inference(resolution,[status(thm)],[c3616,c397]) ).
cnf(c52,plain,
is_a_theorem(implies(implies(implies(X685,implies(implies(implies(X683,X689),implies(implies(X688,X683),implies(X682,X683))),implies(X687,implies(implies(X688,X683),implies(X682,X683))))),X686),implies(X684,X686))),
inference(resolution,[status(thm)],[c31,c9]) ).
cnf(c426,plain,
( ~ is_a_theorem(implies(implies(X700,X699),X700))
| is_a_theorem(implies(X698,X700)) ),
inference(resolution,[status(thm)],[c397,condensed_detachment]) ).
cnf(c505,plain,
is_a_theorem(implies(X701,implies(X702,X702))),
inference(resolution,[status(thm)],[c426,c397]) ).
cnf(c535,plain,
( ~ is_a_theorem(X712)
| is_a_theorem(implies(X713,X713)) ),
inference(resolution,[status(thm)],[c505,condensed_detachment]) ).
cnf(c553,plain,
is_a_theorem(implies(X714,X714)),
inference(resolution,[status(thm)],[c535,c52]) ).
cnf(c595,plain,
is_a_theorem(implies(implies(implies(X867,X867),X866),implies(X865,X866))),
inference(resolution,[status(thm)],[c553,c31]) ).
cnf(c4106,plain,
is_a_theorem(implies(X5515,implies(implies(implies(X5514,X5514),X5516),X5516))),
inference(resolution,[status(thm)],[c3616,c595]) ).
cnf(c4225,plain,
( ~ is_a_theorem(X5588)
| is_a_theorem(implies(implies(implies(X5589,X5589),X5590),X5590)) ),
inference(resolution,[status(thm)],[c4106,condensed_detachment]) ).
cnf(c4282,plain,
is_a_theorem(implies(implies(implies(X5601,X5601),X5600),X5600)),
inference(resolution,[status(thm)],[c4225,c342]) ).
cnf(c4572,plain,
( ~ is_a_theorem(implies(implies(X6130,X6130),X6131))
| is_a_theorem(X6131) ),
inference(resolution,[status(thm)],[c4282,condensed_detachment]) ).
cnf(c5389,plain,
is_a_theorem(implies(implies(implies(X6237,X6238),X6237),X6237)),
inference(resolution,[status(thm)],[c4572,c4151]) ).
cnf(c5620,plain,
( ~ is_a_theorem(implies(implies(X6298,X6299),X6298))
| is_a_theorem(X6298) ),
inference(resolution,[status(thm)],[c5389,condensed_detachment]) ).
cnf(c4141,plain,
is_a_theorem(implies(X7697,implies(implies(X7698,implies(X7698,X7696)),implies(X7698,X7696)))),
inference(resolution,[status(thm)],[c3616,c3486]) ).
cnf(c7737,plain,
is_a_theorem(implies(implies(X7707,implies(X7707,X7706)),implies(X7707,X7706))),
inference(resolution,[status(thm)],[c4141,c5620]) ).
cnf(c4,plain,
is_a_theorem(implies(X55,implies(implies(implies(implies(implies(implies(X60,X54),implies(X53,X54)),implies(X54,X57)),X59),X58),implies(implies(implies(X56,implies(X54,X57)),X59),X58)))),
inference(resolution,[status(thm)],[c2,c0]) ).
cnf(c17,plain,
is_a_theorem(implies(X199,implies(implies(implies(implies(implies(X203,implies(X198,X197)),X204),X196),X202),implies(implies(implies(implies(implies(implies(X200,X198),implies(X201,X198)),implies(X198,X197)),X204),X196),X202)))),
inference(resolution,[status(thm)],[c4,c0]) ).
cnf(c137,plain,
is_a_theorem(implies(X1586,implies(implies(implies(implies(implies(implies(implies(implies(X1589,X1582),implies(X1590,X1582)),implies(X1582,X1584)),X1585),X1588),X1583),X1587),implies(implies(implies(implies(implies(X1581,implies(X1582,X1584)),X1585),X1588),X1583),X1587)))),
inference(resolution,[status(thm)],[c17,c0]) ).
cnf(c20,plain,
is_a_theorem(implies(X216,implies(implies(implies(implies(X215,X219),implies(X217,X219)),X218),implies(X215,X218)))),
inference(resolution,[status(thm)],[c11,c0]) ).
cnf(c142,plain,
( ~ is_a_theorem(X1732)
| is_a_theorem(implies(implies(implies(implies(X1734,X1731),implies(X1730,X1731)),X1733),implies(X1734,X1733))) ),
inference(resolution,[status(thm)],[c20,condensed_detachment]) ).
cnf(c1181,plain,
is_a_theorem(implies(implies(implies(implies(X2604,X2602),implies(X2605,X2602)),X2603),implies(X2604,X2603))),
inference(resolution,[status(thm)],[c142,c137]) ).
cnf(c2016,plain,
( ~ is_a_theorem(implies(implies(implies(X17964,X17965),implies(X17963,X17965)),X17966))
| is_a_theorem(implies(X17964,X17966)) ),
inference(resolution,[status(thm)],[c1181,condensed_detachment]) ).
cnf(c22093,plain,
is_a_theorem(implies(X18017,implies(implies(X18017,X18016),X18016))),
inference(resolution,[status(thm)],[c2016,c7737]) ).
cnf(c22435,plain,
$false,
inference(resolution,[status(thm)],[c22093,prove_ic_5]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL094-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.08/0.36 % Computer : n010.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Fri Sep 4 16:20:53 UTC 2026
% 0.12/0.36 % CPUTime :
% 0.12/0.42 /export/starexec/sandbox/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.12/0.42 (re.compile("\."), Token.FullStop),
% 0.12/0.42 /export/starexec/sandbox/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.12/0.42 (re.compile("\("), Token.OpenPar),
% 0.12/0.42 /export/starexec/sandbox/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.12/0.42 (re.compile("\)"), Token.ClosePar),
% 0.12/0.42 /export/starexec/sandbox/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.12/0.42 (re.compile("\["), Token.OpenSquare),
% 0.12/0.42 /export/starexec/sandbox/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.12/0.42 (re.compile("\]"), Token.CloseSquare),
% 0.12/0.42 /export/starexec/sandbox/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.12/0.42 (re.compile("~\|"), Token.Nor),
% 0.12/0.42 /export/starexec/sandbox/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.12/0.42 (re.compile("\|"), Token.Or),
% 0.12/0.42 /export/starexec/sandbox/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.12/0.42 (re.compile("\?"), Token.Existential),
% 0.12/0.42 /export/starexec/sandbox/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.12/0.42 (re.compile("\s+"), Token.WhiteSpace),
% 0.12/0.42 /export/starexec/sandbox/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.12/0.42 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.21/0.49 /export/starexec/sandbox/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.21/0.49 """
% 0.21/0.49 /export/starexec/sandbox/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.21/0.49 """
% 0.32/0.58 /export/starexec/sandbox/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.32/0.58 """
% 24.05/24.37 % Version: 1.5
% 24.05/24.37 % SZS status Unsatisfiable
% 24.05/24.37 % SZS output start CNFRefutation
% See solution above
% 24.05/24.37
% 24.05/24.37 % Initial clauses : 3
% 24.05/24.37 % Processed clauses : 463
% 24.05/24.37 % Factors computed : 0
% 24.05/24.37 % Resolvents computed: 22456
% 24.05/24.37 % Tautologies deleted: 1
% 24.05/24.37 % Forward subsumed : 3983
% 24.05/24.37 % Backward subsumed : 40
% 24.05/24.37 % -------- CPU Time ---------
% 24.05/24.37 % User time : 23.925 s
% 24.05/24.37 % System time : 0.085 s
% 24.05/24.37 % Total time : 24.010 s
%------------------------------------------------------------------------------