%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : LCL089-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:50 PM UTC 2026
% Result : Unsatisfiable 7.47s 7.78s
% Output : CNFRefutation 7.47s
% Verified :
% SZS Type : Refutation
% Derivation depth : 32
% Number of leaves : 3
% Syntax : Number of clauses : 57 ( 36 unt; 0 nHn; 7 RR)
% Number of literals : 79 ( 0 equ; 23 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; 3 con; 0-2 aty)
% Number of variables : 193 ( 93 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(prove_ic_4,negated_conjecture,
~ is_a_theorem(implies(implies(a,b),implies(implies(b,c),implies(a,c)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_ic_4) ).
cnf(ic_JLukasiewicz_4,axiom,
is_a_theorem(implies(implies(implies(X7,X4),implies(X5,X6)),implies(X8,implies(implies(X6,X7),implies(X5,X7))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ic_JLukasiewicz_4) ).
cnf(condensed_detachment,axiom,
( ~ is_a_theorem(implies(X3,X2))
| ~ is_a_theorem(X3)
| is_a_theorem(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',condensed_detachment) ).
cnf(c0,plain,
( ~ is_a_theorem(implies(implies(X10,X11),implies(X13,X12)))
| is_a_theorem(implies(X9,implies(implies(X12,X10),implies(X13,X10)))) ),
inference(resolution,[status(thm)],[ic_JLukasiewicz_4,condensed_detachment]) ).
cnf(c1,plain,
is_a_theorem(implies(X19,implies(implies(implies(implies(X17,X15),implies(X18,X15)),implies(X15,X16)),implies(X14,implies(X15,X16))))),
inference(resolution,[status(thm)],[c0,ic_JLukasiewicz_4]) ).
cnf(c3,plain,
is_a_theorem(implies(X54,implies(implies(implies(X52,implies(X51,X53)),X49),implies(implies(implies(implies(X48,X51),implies(X50,X51)),implies(X51,X53)),X49)))),
inference(resolution,[status(thm)],[c1,c0]) ).
cnf(c2,plain,
( ~ is_a_theorem(X25)
| is_a_theorem(implies(implies(implies(implies(X20,X22),implies(X21,X22)),implies(X22,X24)),implies(X23,implies(X22,X24)))) ),
inference(resolution,[status(thm)],[c1,condensed_detachment]) ).
cnf(c4,plain,
is_a_theorem(implies(implies(implies(implies(X27,X29),implies(X26,X29)),implies(X29,X30)),implies(X28,implies(X29,X30)))),
inference(resolution,[status(thm)],[c2,c1]) ).
cnf(c6,plain,
( ~ is_a_theorem(implies(implies(implies(X39,X36),implies(X37,X36)),implies(X36,X38)))
| is_a_theorem(implies(X40,implies(X36,X38))) ),
inference(resolution,[status(thm)],[c4,condensed_detachment]) ).
cnf(c8,plain,
is_a_theorem(implies(X41,implies(implies(X43,X42),implies(X42,implies(X43,X42))))),
inference(resolution,[status(thm)],[c6,c4]) ).
cnf(c13,plain,
( ~ is_a_theorem(X60)
| is_a_theorem(implies(implies(X58,X59),implies(X59,implies(X58,X59)))) ),
inference(resolution,[status(thm)],[c8,condensed_detachment]) ).
cnf(c20,plain,
is_a_theorem(implies(implies(X62,X61),implies(X61,implies(X62,X61)))),
inference(resolution,[status(thm)],[c13,c3]) ).
cnf(c26,plain,
is_a_theorem(implies(X131,implies(implies(implies(X132,X133),X132),implies(X133,X132)))),
inference(resolution,[status(thm)],[c20,c0]) ).
cnf(c73,plain,
( ~ is_a_theorem(X139)
| is_a_theorem(implies(implies(implies(X138,X137),X138),implies(X137,X138))) ),
inference(resolution,[status(thm)],[c26,condensed_detachment]) ).
cnf(c74,plain,
is_a_theorem(implies(implies(implies(X141,X140),X141),implies(X140,X141))),
inference(resolution,[status(thm)],[c73,c3]) ).
cnf(c86,plain,
is_a_theorem(implies(X142,implies(X143,implies(X144,X143)))),
inference(resolution,[status(thm)],[c74,c6]) ).
cnf(c94,plain,
is_a_theorem(implies(X272,implies(implies(implies(X273,X275),X274),implies(X275,X274)))),
inference(resolution,[status(thm)],[c86,c0]) ).
cnf(c191,plain,
( ~ is_a_theorem(X330)
| is_a_theorem(implies(implies(implies(X331,X329),X328),implies(X329,X328))) ),
inference(resolution,[status(thm)],[c94,condensed_detachment]) ).
cnf(c226,plain,
is_a_theorem(implies(implies(implies(X333,X334),X332),implies(X334,X332))),
inference(resolution,[status(thm)],[c191,c3]) ).
cnf(c250,plain,
( ~ is_a_theorem(implies(implies(X411,X413),X412))
| is_a_theorem(implies(X413,X412)) ),
inference(resolution,[status(thm)],[c226,condensed_detachment]) ).
cnf(c256,plain,
is_a_theorem(implies(implies(X1659,X1662),implies(X1661,implies(implies(X1662,X1660),implies(X1659,X1660))))),
inference(resolution,[status(thm)],[c250,ic_JLukasiewicz_4]) ).
cnf(c189,plain,
is_a_theorem(implies(X2580,implies(implies(implies(X2579,X2577),X2578),implies(implies(implies(X2576,X2579),X2577),X2578)))),
inference(resolution,[status(thm)],[c94,c0]) ).
cnf(c10,plain,
is_a_theorem(implies(X46,implies(X47,implies(implies(X47,X45),implies(X44,X45))))),
inference(resolution,[status(thm)],[c6,ic_JLukasiewicz_4]) ).
cnf(c16,plain,
( ~ is_a_theorem(X94)
| is_a_theorem(implies(X91,implies(implies(X91,X92),implies(X93,X92)))) ),
inference(resolution,[status(thm)],[c10,condensed_detachment]) ).
cnf(c39,plain,
is_a_theorem(implies(X95,implies(implies(X95,X96),implies(X97,X96)))),
inference(resolution,[status(thm)],[c16,c3]) ).
cnf(c49,plain,
( ~ is_a_theorem(X125)
| is_a_theorem(implies(implies(X125,X124),implies(X123,X124))) ),
inference(resolution,[status(thm)],[c39,condensed_detachment]) ).
cnf(c58,plain,
is_a_theorem(implies(implies(implies(X631,implies(implies(implies(implies(X632,X635),implies(X634,X635)),implies(X635,X637)),implies(X636,implies(X635,X637)))),X633),implies(X638,X633))),
inference(resolution,[status(thm)],[c49,c1]) ).
cnf(c95,plain,
( ~ is_a_theorem(X157)
| is_a_theorem(implies(X155,implies(X156,X155))) ),
inference(resolution,[status(thm)],[c86,condensed_detachment]) ).
cnf(c96,plain,
is_a_theorem(implies(X158,implies(X159,X158))),
inference(resolution,[status(thm)],[c95,c3]) ).
cnf(c110,plain,
is_a_theorem(implies(X289,implies(implies(implies(X290,X292),X290),implies(X291,X290)))),
inference(resolution,[status(thm)],[c96,c0]) ).
cnf(c215,plain,
( ~ is_a_theorem(X536)
| is_a_theorem(implies(implies(implies(X537,X535),X537),implies(X534,X537))) ),
inference(resolution,[status(thm)],[c110,condensed_detachment]) ).
cnf(c382,plain,
is_a_theorem(implies(implies(implies(X540,X538),X540),implies(X539,X540))),
inference(resolution,[status(thm)],[c215,c3]) ).
cnf(c412,plain,
( ~ is_a_theorem(implies(implies(X666,X667),X666))
| is_a_theorem(implies(X665,X666)) ),
inference(resolution,[status(thm)],[c382,condensed_detachment]) ).
cnf(c482,plain,
is_a_theorem(implies(X669,implies(X668,X668))),
inference(resolution,[status(thm)],[c412,c382]) ).
cnf(c515,plain,
( ~ is_a_theorem(X681)
| is_a_theorem(implies(X680,X680)) ),
inference(resolution,[status(thm)],[c482,condensed_detachment]) ).
cnf(c519,plain,
is_a_theorem(implies(X682,X682)),
inference(resolution,[status(thm)],[c515,c58]) ).
cnf(c552,plain,
is_a_theorem(implies(implies(implies(X841,X841),X842),implies(X840,X842))),
inference(resolution,[status(thm)],[c519,c49]) ).
cnf(c409,plain,
is_a_theorem(implies(X1823,implies(implies(X1824,implies(X1824,X1825)),implies(X1826,implies(X1824,X1825))))),
inference(resolution,[status(thm)],[c382,c0]) ).
cnf(c1673,plain,
( ~ is_a_theorem(X4880)
| is_a_theorem(implies(implies(X4881,implies(X4881,X4879)),implies(X4878,implies(X4881,X4879)))) ),
inference(resolution,[status(thm)],[c409,condensed_detachment]) ).
cnf(c3589,plain,
is_a_theorem(implies(implies(X4882,implies(X4882,X4883)),implies(X4884,implies(X4882,X4883)))),
inference(resolution,[status(thm)],[c1673,c189]) ).
cnf(c3720,plain,
( ~ is_a_theorem(implies(X5575,implies(X5575,X5577)))
| is_a_theorem(implies(X5576,implies(X5575,X5577))) ),
inference(resolution,[status(thm)],[c3589,condensed_detachment]) ).
cnf(c4376,plain,
is_a_theorem(implies(X5631,implies(implies(implies(X5630,X5630),X5632),X5632))),
inference(resolution,[status(thm)],[c3720,c552]) ).
cnf(c4620,plain,
( ~ is_a_theorem(X5669)
| is_a_theorem(implies(implies(implies(X5668,X5668),X5670),X5670)) ),
inference(resolution,[status(thm)],[c4376,condensed_detachment]) ).
cnf(c4669,plain,
is_a_theorem(implies(implies(implies(X5676,X5676),X5675),X5675)),
inference(resolution,[status(thm)],[c4620,c189]) ).
cnf(c4817,plain,
( ~ is_a_theorem(implies(implies(X6206,X6206),X6205))
| is_a_theorem(X6205) ),
inference(resolution,[status(thm)],[c4669,condensed_detachment]) ).
cnf(c263,plain,
is_a_theorem(implies(X426,implies(X425,implies(X424,X426)))),
inference(resolution,[status(thm)],[c250,c96]) ).
cnf(c275,plain,
is_a_theorem(implies(X1728,implies(implies(implies(X1724,implies(X1727,X1726)),X1727),implies(X1725,X1727)))),
inference(resolution,[status(thm)],[c263,c0]) ).
cnf(c1491,plain,
( ~ is_a_theorem(X3171)
| is_a_theorem(implies(implies(implies(X3170,implies(X3168,X3169)),X3168),implies(X3167,X3168))) ),
inference(resolution,[status(thm)],[c275,condensed_detachment]) ).
cnf(c2339,plain,
is_a_theorem(implies(implies(implies(X3175,implies(X3173,X3172)),X3173),implies(X3174,X3173))),
inference(resolution,[status(thm)],[c1491,c189]) ).
cnf(c4343,plain,
is_a_theorem(implies(X6941,implies(implies(implies(X6940,implies(X6943,X6942)),X6943),X6943))),
inference(resolution,[status(thm)],[c3720,c2339]) ).
cnf(c6190,plain,
is_a_theorem(implies(implies(implies(X6962,implies(X6960,X6961)),X6960),X6960)),
inference(resolution,[status(thm)],[c4343,c4817]) ).
cnf(c6365,plain,
( ~ is_a_theorem(implies(implies(X7008,implies(X7007,X7009)),X7007))
| is_a_theorem(X7007) ),
inference(resolution,[status(thm)],[c6190,condensed_detachment]) ).
cnf(c4344,plain,
is_a_theorem(implies(X7086,implies(implies(X7085,implies(X7085,X7087)),implies(X7085,X7087)))),
inference(resolution,[status(thm)],[c3720,c3589]) ).
cnf(c6533,plain,
is_a_theorem(implies(implies(X7089,implies(X7089,X7088)),implies(X7089,X7088))),
inference(resolution,[status(thm)],[c4344,c6365]) ).
cnf(c6565,plain,
( ~ is_a_theorem(implies(X7143,implies(X7143,X7144)))
| is_a_theorem(implies(X7143,X7144)) ),
inference(resolution,[status(thm)],[c6533,condensed_detachment]) ).
cnf(c6676,plain,
is_a_theorem(implies(implies(X9136,X9138),implies(implies(X9138,X9137),implies(X9136,X9137)))),
inference(resolution,[status(thm)],[c6565,c256]) ).
cnf(c9960,plain,
$false,
inference(resolution,[status(thm)],[c6676,prove_ic_4]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL089-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 : n004.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 : Sat Sep 5 16:47:14 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.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.33/0.58 /export/starexec/sandbox/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.33/0.58 """
% 7.47/7.78 % Version: 1.5
% 7.47/7.78 % SZS status Unsatisfiable
% 7.47/7.78 % SZS output start CNFRefutation
% See solution above
% 7.47/7.78
% 7.47/7.78 % Initial clauses : 3
% 7.47/7.78 % Processed clauses : 287
% 7.47/7.78 % Factors computed : 0
% 7.47/7.78 % Resolvents computed: 9983
% 7.47/7.78 % Tautologies deleted: 1
% 7.47/7.78 % Forward subsumed : 2068
% 7.47/7.78 % Backward subsumed : 32
% 7.47/7.78 % -------- CPU Time ---------
% 7.47/7.78 % User time : 7.383 s
% 7.47/7.78 % System time : 0.042 s
% 7.47/7.78 % Total time : 7.425 s
%------------------------------------------------------------------------------