%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : LCL034-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n003.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:43 PM UTC 2026
% Result : Unsatisfiable 8.89s 9.13s
% Output : CNFRefutation 8.89s
% Verified :
% SZS Type : Refutation
% Derivation depth : 33
% Number of leaves : 3
% Syntax : Number of clauses : 51 ( 34 unt; 0 nHn; 7 RR)
% Number of literals : 69 ( 0 equ; 19 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 7 ( 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 : 162 ( 86 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(prove_c0_3,negated_conjecture,
~ is_a_theorem(implies(implies(implies(a,b),a),a)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_c0_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(c0_CAMeredith,axiom,
is_a_theorem(implies(implies(implies(implies(implies(X5,X7),implies(X8,falsehood)),X4),X6),implies(implies(X6,X5),implies(X8,X5)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c0_CAMeredith) ).
cnf(c0,plain,
( ~ is_a_theorem(implies(implies(implies(implies(X10,X11),implies(X13,falsehood)),X12),X9))
| is_a_theorem(implies(implies(X9,X10),implies(X13,X10))) ),
inference(resolution,[status(thm)],[c0_CAMeredith,condensed_detachment]) ).
cnf(c1,plain,
is_a_theorem(implies(implies(implies(implies(X14,X15),implies(X18,X15)),implies(X15,X16)),implies(X17,implies(X15,X16)))),
inference(resolution,[status(thm)],[c0,c0_CAMeredith]) ).
cnf(c2,plain,
( ~ is_a_theorem(implies(implies(implies(X23,X21),implies(X19,X21)),implies(X21,X22)))
| is_a_theorem(implies(X20,implies(X21,X22))) ),
inference(resolution,[status(thm)],[c1,condensed_detachment]) ).
cnf(c4,plain,
is_a_theorem(implies(X25,implies(implies(X24,X26),implies(X26,implies(X24,X26))))),
inference(resolution,[status(thm)],[c2,c1]) ).
cnf(c5,plain,
( ~ is_a_theorem(X28)
| is_a_theorem(implies(implies(X27,X29),implies(X29,implies(X27,X29)))) ),
inference(resolution,[status(thm)],[c4,condensed_detachment]) ).
cnf(c8,plain,
is_a_theorem(implies(implies(X30,X31),implies(X31,implies(X30,X31)))),
inference(resolution,[status(thm)],[c5,c1]) ).
cnf(c12,plain,
is_a_theorem(implies(implies(implies(X73,implies(implies(implies(X74,X71),implies(X72,falsehood)),X73)),X74),implies(X72,X74))),
inference(resolution,[status(thm)],[c8,c0]) ).
cnf(c3,plain,
is_a_theorem(implies(implies(implies(X37,implies(falsehood,X36)),X39),implies(X38,X39))),
inference(resolution,[status(thm)],[c1,c0]) ).
cnf(c13,plain,
( ~ is_a_theorem(implies(implies(X85,implies(falsehood,X87)),X86))
| is_a_theorem(implies(X84,X86)) ),
inference(resolution,[status(thm)],[c3,condensed_detachment]) ).
cnf(c57,plain,
is_a_theorem(implies(X92,implies(X91,implies(falsehood,X93)))),
inference(resolution,[status(thm)],[c13,c12]) ).
cnf(c63,plain,
( ~ is_a_theorem(X108)
| is_a_theorem(implies(X107,implies(falsehood,X106))) ),
inference(resolution,[status(thm)],[c57,condensed_detachment]) ).
cnf(c75,plain,
is_a_theorem(implies(X110,implies(falsehood,X109))),
inference(resolution,[status(thm)],[c63,c8]) ).
cnf(c87,plain,
( ~ is_a_theorem(X139)
| is_a_theorem(implies(falsehood,X138)) ),
inference(resolution,[status(thm)],[c75,condensed_detachment]) ).
cnf(c98,plain,
is_a_theorem(implies(falsehood,X140)),
inference(resolution,[status(thm)],[c87,c8]) ).
cnf(c14,plain,
is_a_theorem(implies(implies(implies(X42,X43),X44),implies(falsehood,X44))),
inference(resolution,[status(thm)],[c3,c0]) ).
cnf(c22,plain,
is_a_theorem(implies(implies(implies(falsehood,X173),X174),implies(X172,X174))),
inference(resolution,[status(thm)],[c14,c0]) ).
cnf(c127,plain,
is_a_theorem(implies(X176,implies(X178,implies(X177,X178)))),
inference(resolution,[status(thm)],[c22,c2]) ).
cnf(c128,plain,
( ~ is_a_theorem(X180)
| is_a_theorem(implies(X179,implies(X181,X179))) ),
inference(resolution,[status(thm)],[c127,condensed_detachment]) ).
cnf(c133,plain,
is_a_theorem(implies(X183,implies(X182,X183))),
inference(resolution,[status(thm)],[c128,c98]) ).
cnf(c149,plain,
is_a_theorem(implies(implies(implies(X1054,implies(implies(implies(X1055,X1056),implies(X1057,falsehood)),X1053)),X1055),implies(X1057,X1055))),
inference(resolution,[status(thm)],[c133,c0]) ).
cnf(c414,plain,
is_a_theorem(implies(implies(implies(X1985,X1983),X1982),implies(implies(implies(X1983,X1984),implies(X1985,falsehood)),X1982))),
inference(resolution,[status(thm)],[c149,c0]) ).
cnf(c703,plain,
( ~ is_a_theorem(implies(implies(X3407,X3408),X3409))
| is_a_theorem(implies(implies(implies(X3408,X3406),implies(X3407,falsehood)),X3409)) ),
inference(resolution,[status(thm)],[c414,condensed_detachment]) ).
cnf(c1200,plain,
is_a_theorem(implies(implies(implies(X3425,X3428),implies(X3427,falsehood)),implies(X3426,implies(X3427,X3425)))),
inference(resolution,[status(thm)],[c703,c133]) ).
cnf(c1239,plain,
( ~ is_a_theorem(implies(implies(X3573,X3575),implies(X3574,falsehood)))
| is_a_theorem(implies(X3576,implies(X3574,X3573))) ),
inference(resolution,[status(thm)],[c1200,condensed_detachment]) ).
cnf(c147,plain,
( ~ is_a_theorem(X219)
| is_a_theorem(implies(X218,X219)) ),
inference(resolution,[status(thm)],[c133,condensed_detachment]) ).
cnf(c155,plain,
is_a_theorem(implies(X1106,implies(implies(implies(implies(X1108,X1105),implies(X1103,X1105)),implies(X1105,X1107)),implies(X1104,implies(X1105,X1107))))),
inference(resolution,[status(thm)],[c147,c1]) ).
cnf(c423,plain,
is_a_theorem(implies(implies(implies(implies(implies(implies(X3127,X3132),implies(X3128,X3132)),implies(X3132,X3130)),implies(X3129,implies(X3132,X3130))),X3131),implies(X3133,X3131))),
inference(resolution,[status(thm)],[c155,c0]) ).
cnf(c1337,plain,
is_a_theorem(implies(X3665,implies(implies(implies(X3666,X3663),implies(X3664,falsehood)),implies(X3664,X3666)))),
inference(resolution,[status(thm)],[c1239,c414]) ).
cnf(c1378,plain,
( ~ is_a_theorem(X3674)
| is_a_theorem(implies(implies(implies(X3673,X3675),implies(X3672,falsehood)),implies(X3672,X3673))) ),
inference(resolution,[status(thm)],[c1337,condensed_detachment]) ).
cnf(c1395,plain,
is_a_theorem(implies(implies(implies(X3678,X3676),implies(X3677,falsehood)),implies(X3677,X3678))),
inference(resolution,[status(thm)],[c1378,c423]) ).
cnf(c1473,plain,
is_a_theorem(implies(implies(implies(X3697,implies(X3698,X3695)),X3698),implies(X3696,X3698))),
inference(resolution,[status(thm)],[c1395,c0]) ).
cnf(c1502,plain,
is_a_theorem(implies(implies(implies(X3706,X3707),X3708),implies(X3707,X3708))),
inference(resolution,[status(thm)],[c1473,c0]) ).
cnf(c1503,plain,
( ~ is_a_theorem(implies(implies(X3728,X3730),X3729))
| is_a_theorem(implies(X3730,X3729)) ),
inference(resolution,[status(thm)],[c1502,condensed_detachment]) ).
cnf(c1544,plain,
is_a_theorem(implies(implies(X3826,falsehood),implies(X3826,X3825))),
inference(resolution,[status(thm)],[c1503,c1395]) ).
cnf(c1737,plain,
is_a_theorem(implies(X3827,implies(X3828,X3828))),
inference(resolution,[status(thm)],[c1544,c1239]) ).
cnf(c1516,plain,
is_a_theorem(implies(implies(implies(implies(X6708,falsehood),X6707),X6709),implies(X6708,X6709))),
inference(resolution,[status(thm)],[c1502,c0]) ).
cnf(c4051,plain,
is_a_theorem(implies(implies(implies(X6810,X6809),X6810),implies(X6808,X6810))),
inference(resolution,[status(thm)],[c1516,c0]) ).
cnf(c1466,plain,
( ~ is_a_theorem(implies(implies(X6597,X6596),implies(X6598,falsehood)))
| is_a_theorem(implies(X6598,X6597)) ),
inference(resolution,[status(thm)],[c1395,condensed_detachment]) ).
cnf(c4045,plain,
is_a_theorem(implies(X6727,implies(implies(X6727,falsehood),X6728))),
inference(resolution,[status(thm)],[c1516,c1466]) ).
cnf(c4030,plain,
( ~ is_a_theorem(implies(implies(implies(X8501,falsehood),X8502),X8500))
| is_a_theorem(implies(X8501,X8500)) ),
inference(resolution,[status(thm)],[c1516,condensed_detachment]) ).
cnf(c5998,plain,
is_a_theorem(implies(X11485,implies(implies(implies(implies(X11485,falsehood),X11486),falsehood),X11487))),
inference(resolution,[status(thm)],[c4030,c4045]) ).
cnf(c8767,plain,
is_a_theorem(implies(implies(implies(implies(implies(X11996,X11994),falsehood),X11995),falsehood),X11996)),
inference(resolution,[status(thm)],[c5998,c1466]) ).
cnf(c9200,plain,
is_a_theorem(implies(implies(X12010,implies(X12010,X12012)),implies(X12011,implies(X12010,X12012)))),
inference(resolution,[status(thm)],[c8767,c0]) ).
cnf(c9249,plain,
( ~ is_a_theorem(implies(X12058,implies(X12058,X12057)))
| is_a_theorem(implies(X12056,implies(X12058,X12057))) ),
inference(resolution,[status(thm)],[c9200,condensed_detachment]) ).
cnf(c9288,plain,
is_a_theorem(implies(X12096,implies(implies(implies(X12095,X12097),X12095),X12095))),
inference(resolution,[status(thm)],[c9249,c4051]) ).
cnf(c9521,plain,
( ~ is_a_theorem(X12179)
| is_a_theorem(implies(implies(implies(X12180,X12178),X12180),X12180)) ),
inference(resolution,[status(thm)],[c9288,condensed_detachment]) ).
cnf(c9641,plain,
is_a_theorem(implies(implies(implies(X12182,X12181),X12182),X12182)),
inference(resolution,[status(thm)],[c9521,c1737]) ).
cnf(c9878,plain,
$false,
inference(resolution,[status(thm)],[c9641,prove_c0_3]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL034-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.09/0.36 % Computer : n003.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.12/0.36 % CPULimit : 300
% 0.12/0.36 % WCLimit : 300
% 0.12/0.36 % DateTime : Sat Sep 5 06:05:50 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.22/0.49 /export/starexec/sandbox/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.22/0.49 """
% 0.22/0.49 /export/starexec/sandbox/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.22/0.49 """
% 0.32/0.59 /export/starexec/sandbox/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.32/0.59 """
% 8.89/9.13 % Version: 1.5
% 8.89/9.13 % SZS status Unsatisfiable
% 8.89/9.13 % SZS output start CNFRefutation
% See solution above
% 8.89/9.13
% 8.89/9.13 % Initial clauses : 3
% 8.89/9.13 % Processed clauses : 363
% 8.89/9.13 % Factors computed : 0
% 8.89/9.13 % Resolvents computed: 9902
% 8.89/9.13 % Tautologies deleted: 1
% 8.89/9.13 % Forward subsumed : 2580
% 8.89/9.13 % Backward subsumed : 72
% 8.89/9.13 % -------- CPU Time ---------
% 8.89/9.13 % User time : 8.719 s
% 8.89/9.13 % System time : 0.048 s
% 8.89/9.13 % Total time : 8.767 s
%------------------------------------------------------------------------------