%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : LCL083-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n008.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:49 PM UTC 2026
% Result : Unsatisfiable 48.47s 48.77s
% Output : CNFRefutation 48.47s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 3
% Syntax : Number of clauses : 54 ( 35 unt; 0 nHn; 5 RR)
% Number of literals : 74 ( 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 : 209 ( 112 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(prove_ic_3,negated_conjecture,
~ is_a_theorem(implies(implies(implies(a,b),a),a)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_ic_3) ).
cnf(condensed_detachment,axiom,
( ~ is_a_theorem(implies(X3,X2))
| ~ is_a_theorem(X3)
| is_a_theorem(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',condensed_detachment) ).
cnf(ic_JLukasiewicz,axiom,
is_a_theorem(implies(implies(implies(X5,X4),X6),implies(implies(X6,X5),implies(X7,X5)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ic_JLukasiewicz) ).
cnf(c0,plain,
( ~ is_a_theorem(implies(implies(X8,X9),X11))
| is_a_theorem(implies(implies(X11,X8),implies(X10,X8))) ),
inference(resolution,[status(thm)],[ic_JLukasiewicz,condensed_detachment]) ).
cnf(c1,plain,
is_a_theorem(implies(implies(implies(implies(X15,X16),implies(X12,X16)),implies(X16,X13)),implies(X14,implies(X16,X13)))),
inference(resolution,[status(thm)],[c0,ic_JLukasiewicz]) ).
cnf(c2,plain,
is_a_theorem(implies(implies(implies(X20,implies(X21,X18)),implies(implies(X17,X21),implies(X22,X21))),implies(X19,implies(implies(X17,X21),implies(X22,X21))))),
inference(resolution,[status(thm)],[c1,c0]) ).
cnf(c4,plain,
is_a_theorem(implies(implies(implies(X43,implies(implies(X39,X41),implies(X42,X41))),implies(X38,implies(X41,X44))),implies(X40,implies(X38,implies(X41,X44))))),
inference(resolution,[status(thm)],[c2,c0]) ).
cnf(c18,plain,
( ~ is_a_theorem(implies(implies(X128,implies(implies(X126,X123),implies(X124,X123))),implies(X125,implies(X123,X127))))
| is_a_theorem(implies(X122,implies(X125,implies(X123,X127)))) ),
inference(resolution,[status(thm)],[c4,condensed_detachment]) ).
cnf(c3,plain,
( ~ is_a_theorem(implies(implies(implies(X23,X26),implies(X27,X26)),implies(X26,X24)))
| is_a_theorem(implies(X25,implies(X26,X24))) ),
inference(resolution,[status(thm)],[c1,condensed_detachment]) ).
cnf(c17,plain,
is_a_theorem(implies(implies(implies(X105,implies(X109,implies(X106,X111))),implies(X112,implies(implies(X110,X106),implies(X107,X106)))),implies(X108,implies(X112,implies(implies(X110,X106),implies(X107,X106)))))),
inference(resolution,[status(thm)],[c4,c0]) ).
cnf(c5,plain,
( ~ is_a_theorem(implies(implies(X57,implies(X59,X62)),implies(implies(X58,X59),implies(X60,X59))))
| is_a_theorem(implies(X61,implies(implies(X58,X59),implies(X60,X59)))) ),
inference(resolution,[status(thm)],[c2,condensed_detachment]) ).
cnf(c28,plain,
is_a_theorem(implies(X63,implies(implies(X65,X64),implies(X64,X64)))),
inference(resolution,[status(thm)],[c5,c1]) ).
cnf(c37,plain,
( ~ is_a_theorem(X76)
| is_a_theorem(implies(implies(X75,X77),implies(X77,X77))) ),
inference(resolution,[status(thm)],[c28,condensed_detachment]) ).
cnf(c38,plain,
is_a_theorem(implies(implies(X81,X82),implies(X82,X82))),
inference(resolution,[status(thm)],[c37,c1]) ).
cnf(c52,plain,
is_a_theorem(implies(implies(implies(X130,X130),X131),implies(X129,X131))),
inference(resolution,[status(thm)],[c38,c0]) ).
cnf(c88,plain,
is_a_theorem(implies(X136,implies(X135,implies(X134,X135)))),
inference(resolution,[status(thm)],[c52,c3]) ).
cnf(c97,plain,
( ~ is_a_theorem(X140)
| is_a_theorem(implies(X141,implies(X142,X141))) ),
inference(resolution,[status(thm)],[c88,condensed_detachment]) ).
cnf(c99,plain,
is_a_theorem(implies(X149,implies(X148,X149))),
inference(resolution,[status(thm)],[c97,c17]) ).
cnf(c117,plain,
is_a_theorem(implies(X489,implies(X488,implies(implies(X487,X488),implies(X490,X488))))),
inference(resolution,[status(thm)],[c99,c3]) ).
cnf(c252,plain,
( ~ is_a_theorem(X686)
| is_a_theorem(implies(X687,implies(implies(X685,X687),implies(X688,X687)))) ),
inference(resolution,[status(thm)],[c117,condensed_detachment]) ).
cnf(c329,plain,
is_a_theorem(implies(X694,implies(implies(X695,X694),implies(X693,X694)))),
inference(resolution,[status(thm)],[c252,c1]) ).
cnf(c356,plain,
is_a_theorem(implies(X1866,implies(implies(X1863,implies(X1862,implies(implies(X1864,X1865),implies(X1867,X1865)))),implies(X1865,implies(X1862,implies(implies(X1864,X1865),implies(X1867,X1865))))))),
inference(resolution,[status(thm)],[c329,c18]) ).
cnf(c119,plain,
( ~ is_a_theorem(X183)
| is_a_theorem(implies(X184,X183)) ),
inference(resolution,[status(thm)],[c99,condensed_detachment]) ).
cnf(c131,plain,
is_a_theorem(implies(X1230,implies(implies(implies(X1231,X1228),X1229),implies(implies(X1229,X1231),implies(X1227,X1231))))),
inference(resolution,[status(thm)],[c119,ic_JLukasiewicz]) ).
cnf(c83,plain,
is_a_theorem(implies(X803,implies(implies(implies(implies(X801,X800),implies(X804,X800)),X802),implies(X800,X802)))),
inference(resolution,[status(thm)],[c18,ic_JLukasiewicz]) ).
cnf(c427,plain,
( ~ is_a_theorem(X2825)
| is_a_theorem(implies(implies(implies(implies(X2822,X2823),implies(X2824,X2823)),X2826),implies(X2823,X2826))) ),
inference(resolution,[status(thm)],[c83,condensed_detachment]) ).
cnf(c1173,plain,
is_a_theorem(implies(implies(implies(implies(X2829,X2830),implies(X2827,X2830)),X2828),implies(X2830,X2828))),
inference(resolution,[status(thm)],[c427,c131]) ).
cnf(c1246,plain,
( ~ is_a_theorem(implies(implies(implies(X3235,X3236),implies(X3237,X3236)),X3234))
| is_a_theorem(implies(X3236,X3234)) ),
inference(resolution,[status(thm)],[c1173,condensed_detachment]) ).
cnf(c1364,plain,
is_a_theorem(implies(X3427,implies(X3426,implies(implies(X3425,X3427),implies(X3424,X3427))))),
inference(resolution,[status(thm)],[c1246,c99]) ).
cnf(c1541,plain,
( ~ is_a_theorem(X3549)
| is_a_theorem(implies(X3551,implies(implies(X3550,X3549),implies(X3548,X3549)))) ),
inference(resolution,[status(thm)],[c1364,condensed_detachment]) ).
cnf(c1594,plain,
is_a_theorem(implies(X20511,implies(implies(X20510,implies(X20512,implies(implies(X20509,implies(X20506,implies(implies(X20508,X20505),implies(X20513,X20505)))),implies(X20505,implies(X20506,implies(implies(X20508,X20505),implies(X20513,X20505))))))),implies(X20507,implies(X20512,implies(implies(X20509,implies(X20506,implies(implies(X20508,X20505),implies(X20513,X20505)))),implies(X20505,implies(X20506,implies(implies(X20508,X20505),implies(X20513,X20505)))))))))),
inference(resolution,[status(thm)],[c1541,c356]) ).
cnf(c32,plain,
is_a_theorem(implies(X296,implies(implies(implies(X297,X298),X297),implies(X299,X297)))),
inference(resolution,[status(thm)],[c5,ic_JLukasiewicz]) ).
cnf(c193,plain,
is_a_theorem(implies(implies(implies(implies(implies(X1330,X1331),X1330),implies(X1329,X1330)),X1328),implies(X1327,X1328))),
inference(resolution,[status(thm)],[c32,c0]) ).
cnf(c625,plain,
( ~ is_a_theorem(implies(implies(implies(implies(X4795,X4794),X4795),implies(X4793,X4795)),X4792))
| is_a_theorem(implies(X4791,X4792)) ),
inference(resolution,[status(thm)],[c193,condensed_detachment]) ).
cnf(c6,plain,
is_a_theorem(implies(X30,implies(implies(X28,X29),implies(X29,implies(X28,X29))))),
inference(resolution,[status(thm)],[c3,c1]) ).
cnf(c9,plain,
( ~ is_a_theorem(X32)
| is_a_theorem(implies(implies(X33,X31),implies(X31,implies(X33,X31)))) ),
inference(resolution,[status(thm)],[c6,condensed_detachment]) ).
cnf(c11,plain,
is_a_theorem(implies(implies(X34,X35),implies(X35,implies(X34,X35)))),
inference(resolution,[status(thm)],[c9,c6]) ).
cnf(c15,plain,
is_a_theorem(implies(implies(implies(X55,implies(X56,X55)),X56),implies(X54,X56))),
inference(resolution,[status(thm)],[c11,c0]) ).
cnf(c54,plain,
( ~ is_a_theorem(implies(X104,X103))
| is_a_theorem(implies(X103,X103)) ),
inference(resolution,[status(thm)],[c38,condensed_detachment]) ).
cnf(c61,plain,
is_a_theorem(implies(implies(X114,X113),implies(X114,X113))),
inference(resolution,[status(thm)],[c54,c15]) ).
cnf(c79,plain,
is_a_theorem(implies(implies(implies(X207,X206),X207),implies(X205,X207))),
inference(resolution,[status(thm)],[c61,c0]) ).
cnf(c136,plain,
is_a_theorem(implies(implies(implies(X1200,X1201),implies(X1201,X1202)),implies(X1203,implies(X1201,X1202)))),
inference(resolution,[status(thm)],[c79,c0]) ).
cnf(c546,plain,
is_a_theorem(implies(implies(implies(X4653,implies(X4655,X4651)),implies(X4654,X4655)),implies(X4652,implies(X4654,X4655)))),
inference(resolution,[status(thm)],[c136,c0]) ).
cnf(c2235,plain,
( ~ is_a_theorem(implies(implies(X10027,implies(X10030,X10029)),implies(X10026,X10030)))
| is_a_theorem(implies(X10028,implies(X10026,X10030))) ),
inference(resolution,[status(thm)],[c546,condensed_detachment]) ).
cnf(c5474,plain,
is_a_theorem(implies(X10118,implies(implies(implies(implies(X10117,X10116),X10115),X10116),implies(X10117,X10116)))),
inference(resolution,[status(thm)],[c2235,ic_JLukasiewicz]) ).
cnf(c5553,plain,
( ~ is_a_theorem(X10286)
| is_a_theorem(implies(implies(implies(implies(X10284,X10287),X10285),X10287),implies(X10284,X10287))) ),
inference(resolution,[status(thm)],[c5474,condensed_detachment]) ).
cnf(c5558,plain,
is_a_theorem(implies(implies(implies(implies(X10296,X10295),X10294),X10295),implies(X10296,X10295))),
inference(resolution,[status(thm)],[c5553,c1]) ).
cnf(c5701,plain,
is_a_theorem(implies(implies(implies(X39260,X39261),implies(implies(X39260,X39261),X39262)),implies(X39263,implies(implies(X39260,X39261),X39262)))),
inference(resolution,[status(thm)],[c5558,c0]) ).
cnf(c25287,plain,
is_a_theorem(implies(X39288,implies(X39285,implies(implies(implies(X39287,X39286),X39287),X39287)))),
inference(resolution,[status(thm)],[c5701,c625]) ).
cnf(c25420,plain,
( ~ is_a_theorem(X39567)
| is_a_theorem(implies(X39569,implies(implies(implies(X39568,X39566),X39568),X39568))) ),
inference(resolution,[status(thm)],[c25287,condensed_detachment]) ).
cnf(c25803,plain,
is_a_theorem(implies(X39571,implies(implies(implies(X39570,X39572),X39570),X39570))),
inference(resolution,[status(thm)],[c25420,c1594]) ).
cnf(c26252,plain,
( ~ is_a_theorem(X41710)
| is_a_theorem(implies(implies(implies(X41709,X41711),X41709),X41709)) ),
inference(resolution,[status(thm)],[c25803,condensed_detachment]) ).
cnf(c27550,plain,
is_a_theorem(implies(implies(implies(X41713,X41712),X41713),X41713)),
inference(resolution,[status(thm)],[c26252,c1594]) ).
cnf(c27969,plain,
$false,
inference(resolution,[status(thm)],[c27550,prove_ic_3]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL083-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.09/0.35 % Computer : n008.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Sat Sep 5 04:00:53 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.14/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.14/0.41 (re.compile("\."), Token.FullStop),
% 0.14/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.14/0.41 (re.compile("\("), Token.OpenPar),
% 0.14/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.14/0.41 (re.compile("\)"), Token.ClosePar),
% 0.14/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.14/0.41 (re.compile("\["), Token.OpenSquare),
% 0.14/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.14/0.41 (re.compile("\]"), Token.CloseSquare),
% 0.14/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.14/0.41 (re.compile("~\|"), Token.Nor),
% 0.14/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.14/0.41 (re.compile("\|"), Token.Or),
% 0.14/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.14/0.42 (re.compile("\?"), Token.Existential),
% 0.14/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.14/0.42 (re.compile("\s+"), Token.WhiteSpace),
% 0.14/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.14/0.42 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.23/0.48 /export/starexec/sandbox2/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.23/0.48 """
% 0.23/0.49 /export/starexec/sandbox2/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.23/0.49 """
% 0.33/0.58 /export/starexec/sandbox2/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.33/0.58 """
% 48.47/48.77 % Version: 1.5
% 48.47/48.77 % SZS status Unsatisfiable
% 48.47/48.77 % SZS output start CNFRefutation
% See solution above
% 48.47/48.77
% 48.47/48.77 % Initial clauses : 3
% 48.47/48.77 % Processed clauses : 691
% 48.47/48.77 % Factors computed : 0
% 48.47/48.77 % Resolvents computed: 27991
% 48.47/48.77 % Tautologies deleted: 2
% 48.47/48.77 % Forward subsumed : 7363
% 48.47/48.77 % Backward subsumed : 230
% 48.47/48.77 % -------- CPU Time ---------
% 48.47/48.77 % User time : 48.289 s
% 48.47/48.77 % System time : 0.121 s
% 48.47/48.77 % Total time : 48.410 s
%------------------------------------------------------------------------------