%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : LCL090-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n009.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 8.45s 8.80s
% Output : CNFRefutation 8.45s
% Verified :
% SZS Type : Refutation
% Derivation depth : 39
% Number of leaves : 3
% Syntax : Number of clauses : 61 ( 38 unt; 0 nHn; 3 RR)
% Number of literals : 85 ( 0 equ; 25 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 : 2 ( 2 usr; 1 con; 0-2 aty)
% Number of variables : 273 ( 173 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(prove_ic_1,negated_conjecture,
~ is_a_theorem(implies(a,a)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_ic_1) ).
cnf(condensed_detachment,axiom,
( ~ is_a_theorem(implies(X2,X3))
| ~ is_a_theorem(X2)
| is_a_theorem(X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',condensed_detachment) ).
cnf(ic_JLukasiewicz_5,axiom,
is_a_theorem(implies(implies(implies(X8,X7),implies(X4,X5)),implies(implies(X5,X8),implies(X6,implies(X4,X8))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ic_JLukasiewicz_5) ).
cnf(c0,plain,
( ~ is_a_theorem(implies(implies(X11,X13),implies(X12,X9)))
| is_a_theorem(implies(implies(X9,X11),implies(X10,implies(X12,X11)))) ),
inference(resolution,[status(thm)],[ic_JLukasiewicz_5,condensed_detachment]) ).
cnf(c1,plain,
is_a_theorem(implies(implies(implies(X16,implies(X18,X17)),implies(X17,X19)),implies(X14,implies(implies(X15,X17),implies(X17,X19))))),
inference(resolution,[status(thm)],[c0,ic_JLukasiewicz_5]) ).
cnf(c3,plain,
( ~ is_a_theorem(implies(implies(X27,implies(X28,X30)),implies(X30,X31)))
| is_a_theorem(implies(X32,implies(implies(X29,X30),implies(X30,X31)))) ),
inference(resolution,[status(thm)],[c1,condensed_detachment]) ).
cnf(c7,plain,
is_a_theorem(implies(X36,implies(implies(X33,X37),implies(X37,implies(implies(X34,X35),implies(X35,X37)))))),
inference(resolution,[status(thm)],[c3,c1]) ).
cnf(c8,plain,
is_a_theorem(implies(X139,implies(implies(X138,implies(X140,X141)),implies(implies(X140,X141),implies(X141,implies(implies(X137,X136),implies(X136,X141))))))),
inference(resolution,[status(thm)],[c7,c3]) ).
cnf(c2,plain,
is_a_theorem(implies(implies(implies(implies(X23,X24),implies(X24,X26)),implies(X21,implies(X22,X24))),implies(X20,implies(X25,implies(X21,implies(X22,X24)))))),
inference(resolution,[status(thm)],[c1,c0]) ).
cnf(c10,plain,
( ~ is_a_theorem(X42)
| is_a_theorem(implies(implies(X40,X41),implies(X41,implies(implies(X39,X38),implies(X38,X41))))) ),
inference(resolution,[status(thm)],[c7,condensed_detachment]) ).
cnf(c11,plain,
is_a_theorem(implies(implies(X43,X46),implies(X46,implies(implies(X44,X45),implies(X45,X46))))),
inference(resolution,[status(thm)],[c10,c2]) ).
cnf(c15,plain,
is_a_theorem(implies(implies(implies(implies(X72,X75),implies(X75,X73)),X74),implies(X71,implies(X73,X74)))),
inference(resolution,[status(thm)],[c11,c0]) ).
cnf(c28,plain,
is_a_theorem(implies(X78,implies(implies(X76,X80),implies(X80,implies(X77,implies(X79,X80)))))),
inference(resolution,[status(thm)],[c15,c3]) ).
cnf(c31,plain,
( ~ is_a_theorem(X92)
| is_a_theorem(implies(implies(X90,X91),implies(X91,implies(X88,implies(X89,X91))))) ),
inference(resolution,[status(thm)],[c28,condensed_detachment]) ).
cnf(c35,plain,
is_a_theorem(implies(implies(X94,X95),implies(X95,implies(X96,implies(X93,X95))))),
inference(resolution,[status(thm)],[c31,c1]) ).
cnf(c42,plain,
is_a_theorem(implies(implies(implies(X132,implies(X133,X134)),X135),implies(X131,implies(X134,X135)))),
inference(resolution,[status(thm)],[c35,c0]) ).
cnf(c53,plain,
( ~ is_a_theorem(implies(implies(X145,implies(X146,X143)),X144))
| is_a_theorem(implies(X142,implies(X143,X144))) ),
inference(resolution,[status(thm)],[c42,condensed_detachment]) ).
cnf(c67,plain,
is_a_theorem(implies(X230,implies(X231,implies(implies(X231,X233),implies(X232,implies(X234,X233)))))),
inference(resolution,[status(thm)],[c53,ic_JLukasiewicz_5]) ).
cnf(c126,plain,
( ~ is_a_theorem(X257)
| is_a_theorem(implies(X254,implies(implies(X254,X256),implies(X255,implies(X253,X256))))) ),
inference(resolution,[status(thm)],[c67,condensed_detachment]) ).
cnf(c137,plain,
is_a_theorem(implies(X267,implies(implies(X267,X265),implies(X266,implies(X264,X265))))),
inference(resolution,[status(thm)],[c126,c8]) ).
cnf(c155,plain,
( ~ is_a_theorem(X334)
| is_a_theorem(implies(implies(X334,X335),implies(X332,implies(X333,X335)))) ),
inference(resolution,[status(thm)],[c137,condensed_detachment]) ).
cnf(c63,plain,
is_a_theorem(implies(X147,implies(X149,implies(X148,implies(X151,implies(X150,X149)))))),
inference(resolution,[status(thm)],[c53,c42]) ).
cnf(c71,plain,
is_a_theorem(implies(implies(implies(X523,implies(X519,implies(X520,X521))),X522),implies(X518,implies(X521,X522)))),
inference(resolution,[status(thm)],[c63,c0]) ).
cnf(c281,plain,
is_a_theorem(implies(implies(implies(implies(implies(X5191,implies(X5194,implies(X5188,X5193))),X5189),implies(X5192,implies(X5193,X5189))),X5190),implies(X5187,implies(X5186,X5190)))),
inference(resolution,[status(thm)],[c71,c155]) ).
cnf(c52,plain,
is_a_theorem(implies(implies(implies(X889,X890),implies(X892,implies(X893,X889))),implies(X888,implies(X891,implies(X892,implies(X893,X889)))))),
inference(resolution,[status(thm)],[c42,c0]) ).
cnf(c457,plain,
( ~ is_a_theorem(implies(implies(X7521,X7517),implies(X7520,implies(X7519,X7521))))
| is_a_theorem(implies(X7518,implies(X7516,implies(X7520,implies(X7519,X7521))))) ),
inference(resolution,[status(thm)],[c52,condensed_detachment]) ).
cnf(c175,plain,
is_a_theorem(implies(implies(implies(implies(X3035,X3030),implies(X3030,implies(X3031,implies(X3032,X3030)))),X3034),implies(X3033,implies(X3029,X3034)))),
inference(resolution,[status(thm)],[c155,c35]) ).
cnf(c4,plain,
is_a_theorem(implies(implies(implies(X58,implies(X57,implies(X53,X51))),implies(implies(X54,X51),implies(X51,X56))),implies(X52,implies(X55,implies(implies(X54,X51),implies(X51,X56)))))),
inference(resolution,[status(thm)],[c2,c0]) ).
cnf(c18,plain,
( ~ is_a_theorem(implies(implies(X226,implies(X222,implies(X227,X224))),implies(implies(X229,X224),implies(X224,X228))))
| is_a_theorem(implies(X225,implies(X223,implies(implies(X229,X224),implies(X224,X228))))) ),
inference(resolution,[status(thm)],[c4,condensed_detachment]) ).
cnf(c117,plain,
is_a_theorem(implies(X621,implies(X620,implies(implies(implies(X622,X618),X618),implies(X618,implies(X619,X618)))))),
inference(resolution,[status(thm)],[c18,ic_JLukasiewicz_5]) ).
cnf(c326,plain,
( ~ is_a_theorem(X1051)
| is_a_theorem(implies(X1047,implies(implies(implies(X1050,X1049),X1049),implies(X1049,implies(X1048,X1049))))) ),
inference(resolution,[status(thm)],[c117,condensed_detachment]) ).
cnf(c529,plain,
is_a_theorem(implies(X1052,implies(implies(implies(X1055,X1053),X1053),implies(X1053,implies(X1054,X1053))))),
inference(resolution,[status(thm)],[c326,c35]) ).
cnf(c562,plain,
( ~ is_a_theorem(X1214)
| is_a_theorem(implies(implies(implies(X1211,X1212),X1212),implies(X1212,implies(X1213,X1212)))) ),
inference(resolution,[status(thm)],[c529,condensed_detachment]) ).
cnf(c573,plain,
is_a_theorem(implies(implies(implies(X1215,X1216),X1216),implies(X1216,implies(X1217,X1216)))),
inference(resolution,[status(thm)],[c562,c35]) ).
cnf(c609,plain,
is_a_theorem(implies(implies(implies(X1635,X1636),implies(X1633,X1636)),implies(X1634,implies(X1636,implies(X1633,X1636))))),
inference(resolution,[status(thm)],[c573,c0]) ).
cnf(c26,plain,
is_a_theorem(implies(implies(implies(X470,X466),implies(implies(X468,X467),implies(X467,X470))),implies(X465,implies(X469,implies(implies(X468,X467),implies(X467,X470)))))),
inference(resolution,[status(thm)],[c15,c0]) ).
cnf(c251,plain,
( ~ is_a_theorem(implies(implies(X4516,X4518),implies(implies(X4517,X4515),implies(X4515,X4516))))
| is_a_theorem(implies(X4513,implies(X4514,implies(implies(X4517,X4515),implies(X4515,X4516))))) ),
inference(resolution,[status(thm)],[c26,condensed_detachment]) ).
cnf(c2361,plain,
is_a_theorem(implies(X4523,implies(X4522,implies(implies(X4521,X4519),implies(X4519,implies(X4520,X4519)))))),
inference(resolution,[status(thm)],[c251,c609]) ).
cnf(c2403,plain,
( ~ is_a_theorem(X4530)
| is_a_theorem(implies(X4529,implies(implies(X4532,X4528),implies(X4528,implies(X4531,X4528))))) ),
inference(resolution,[status(thm)],[c2361,condensed_detachment]) ).
cnf(c2422,plain,
is_a_theorem(implies(X4535,implies(implies(X4534,X4533),implies(X4533,implies(X4536,X4533))))),
inference(resolution,[status(thm)],[c2403,c175]) ).
cnf(c2515,plain,
( ~ is_a_theorem(X5054)
| is_a_theorem(implies(implies(X5052,X5053),implies(X5053,implies(X5055,X5053)))) ),
inference(resolution,[status(thm)],[c2422,condensed_detachment]) ).
cnf(c2816,plain,
is_a_theorem(implies(implies(X5058,X5057),implies(X5057,implies(X5056,X5057)))),
inference(resolution,[status(thm)],[c2515,c175]) ).
cnf(c2918,plain,
( ~ is_a_theorem(implies(X5532,X5533))
| is_a_theorem(implies(X5533,implies(X5534,X5533))) ),
inference(resolution,[status(thm)],[c2816,condensed_detachment]) ).
cnf(c3229,plain,
is_a_theorem(implies(implies(X6631,implies(X6629,X6630)),implies(X6628,implies(X6631,implies(X6629,X6630))))),
inference(resolution,[status(thm)],[c2918,c281]) ).
cnf(c4304,plain,
is_a_theorem(implies(implies(implies(X7234,implies(X7232,X7235)),X7234),implies(X7231,implies(X7233,X7234)))),
inference(resolution,[status(thm)],[c3229,c0]) ).
cnf(c4689,plain,
( ~ is_a_theorem(implies(implies(X7414,implies(X7415,X7412)),X7414))
| is_a_theorem(implies(X7413,implies(X7416,X7414))) ),
inference(resolution,[status(thm)],[c4304,condensed_detachment]) ).
cnf(c4947,plain,
is_a_theorem(implies(X7417,implies(X7419,implies(X7420,implies(X7421,implies(X7418,X7421)))))),
inference(resolution,[status(thm)],[c4689,c71]) ).
cnf(c5033,plain,
( ~ is_a_theorem(X7430)
| is_a_theorem(implies(X7428,implies(X7429,implies(X7427,implies(X7431,X7427))))) ),
inference(resolution,[status(thm)],[c4947,condensed_detachment]) ).
cnf(c5053,plain,
is_a_theorem(implies(X7443,implies(X7441,implies(X7444,implies(X7442,X7444))))),
inference(resolution,[status(thm)],[c5033,c281]) ).
cnf(c5231,plain,
( ~ is_a_theorem(X8282)
| is_a_theorem(implies(X8281,implies(X8279,implies(X8280,X8279)))) ),
inference(resolution,[status(thm)],[c5053,condensed_detachment]) ).
cnf(c5763,plain,
is_a_theorem(implies(X8284,implies(X8283,implies(X8285,X8283)))),
inference(resolution,[status(thm)],[c5231,c281]) ).
cnf(c5921,plain,
( ~ is_a_theorem(X9075)
| is_a_theorem(implies(X9074,implies(X9073,X9074))) ),
inference(resolution,[status(thm)],[c5763,condensed_detachment]) ).
cnf(c6484,plain,
is_a_theorem(implies(X9076,implies(X9077,X9076))),
inference(resolution,[status(thm)],[c5921,c281]) ).
cnf(c6672,plain,
is_a_theorem(implies(X9812,implies(X9811,implies(X9810,implies(X9813,X9813))))),
inference(resolution,[status(thm)],[c6484,c457]) ).
cnf(c7181,plain,
( ~ is_a_theorem(X9847)
| is_a_theorem(implies(X9845,implies(X9848,implies(X9846,X9846)))) ),
inference(resolution,[status(thm)],[c6672,condensed_detachment]) ).
cnf(c7226,plain,
is_a_theorem(implies(X9849,implies(X9851,implies(X9850,X9850)))),
inference(resolution,[status(thm)],[c7181,c281]) ).
cnf(c7419,plain,
( ~ is_a_theorem(X10741)
| is_a_theorem(implies(X10739,implies(X10740,X10740))) ),
inference(resolution,[status(thm)],[c7226,condensed_detachment]) ).
cnf(c7792,plain,
is_a_theorem(implies(X10742,implies(X10743,X10743))),
inference(resolution,[status(thm)],[c7419,c281]) ).
cnf(c7993,plain,
( ~ is_a_theorem(X11523)
| is_a_theorem(implies(X11522,X11522)) ),
inference(resolution,[status(thm)],[c7792,condensed_detachment]) ).
cnf(c8336,plain,
is_a_theorem(implies(X11524,X11524)),
inference(resolution,[status(thm)],[c7993,c281]) ).
cnf(c8551,plain,
$false,
inference(resolution,[status(thm)],[c8336,prove_ic_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL090-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.03 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.08/0.35 % Computer : n009.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 23:17:06 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.12/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.12/0.41 (re.compile("\."), Token.FullStop),
% 0.12/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.12/0.41 (re.compile("\("), Token.OpenPar),
% 0.12/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.12/0.41 (re.compile("\)"), Token.ClosePar),
% 0.12/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.12/0.41 (re.compile("\["), Token.OpenSquare),
% 0.12/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.12/0.41 (re.compile("\]"), Token.CloseSquare),
% 0.12/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.12/0.41 (re.compile("~\|"), Token.Nor),
% 0.12/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.12/0.41 (re.compile("\|"), Token.Or),
% 0.12/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.12/0.41 (re.compile("\?"), Token.Existential),
% 0.12/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.12/0.41 (re.compile("\s+"), Token.WhiteSpace),
% 0.12/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.12/0.41 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.21/0.48 /export/starexec/sandbox2/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.21/0.48 """
% 0.21/0.48 /export/starexec/sandbox2/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.21/0.48 """
% 0.31/0.57 /export/starexec/sandbox2/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.31/0.57 """
% 8.45/8.80 % Version: 1.5
% 8.45/8.80 % SZS status Unsatisfiable
% 8.45/8.80 % SZS output start CNFRefutation
% See solution above
% 8.45/8.80
% 8.45/8.80 % Initial clauses : 3
% 8.45/8.80 % Processed clauses : 314
% 8.45/8.80 % Factors computed : 0
% 8.45/8.80 % Resolvents computed: 8570
% 8.45/8.80 % Tautologies deleted: 0
% 8.45/8.80 % Forward subsumed : 2150
% 8.45/8.80 % Backward subsumed : 76
% 8.45/8.80 % -------- CPU Time ---------
% 8.45/8.80 % User time : 8.397 s
% 8.45/8.80 % System time : 0.048 s
% 8.45/8.80 % Total time : 8.445 s
%------------------------------------------------------------------------------