%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : LCL026-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n028.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:42 PM UTC 2026
% Result : Unsatisfiable 209.28s 209.85s
% Output : CNFRefutation 209.28s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 5
% Syntax : Number of clauses : 45 ( 33 unt; 0 nHn; 14 RR)
% Number of literals : 58 ( 0 equ; 14 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 6 ( 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 : 101 ( 32 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(c0_2,axiom,
is_a_theorem(implies(X3,implies(X2,X3))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c0_2) ).
cnf(condensed_detachment,axiom,
( ~ is_a_theorem(implies(X5,X4))
| ~ is_a_theorem(X5)
| is_a_theorem(X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',condensed_detachment) ).
cnf(c0,plain,
( ~ is_a_theorem(X6)
| is_a_theorem(implies(X7,X6)) ),
inference(resolution,[status(thm)],[condensed_detachment,c0_2]) ).
cnf(c0_6,axiom,
is_a_theorem(implies(implies(X20,implies(X18,X19)),implies(implies(X20,X18),implies(X20,X19)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c0_6) ).
cnf(c11,plain,
( ~ is_a_theorem(implies(X55,implies(X53,X54)))
| is_a_theorem(implies(implies(X55,X53),implies(X55,X54))) ),
inference(resolution,[status(thm)],[c0_6,condensed_detachment]) ).
cnf(c0_5,axiom,
is_a_theorem(implies(implies(implies(X14,falsehood),falsehood),X14)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c0_5) ).
cnf(c5,plain,
is_a_theorem(implies(X33,implies(implies(implies(X34,falsehood),falsehood),X34))),
inference(resolution,[status(thm)],[c0_5,c0]) ).
cnf(c29,plain,
is_a_theorem(implies(implies(X197,implies(implies(X196,falsehood),falsehood)),implies(X197,X196))),
inference(resolution,[status(thm)],[c11,c5]) ).
cnf(c1,plain,
is_a_theorem(implies(X8,implies(X10,implies(X9,X10)))),
inference(resolution,[status(thm)],[c0,c0_2]) ).
cnf(c4,plain,
( ~ is_a_theorem(implies(implies(X15,falsehood),falsehood))
| is_a_theorem(X15) ),
inference(resolution,[status(thm)],[c0_5,condensed_detachment]) ).
cnf(c6,plain,
is_a_theorem(implies(falsehood,falsehood)),
inference(resolution,[status(thm)],[c4,c0_5]) ).
cnf(c8,plain,
is_a_theorem(implies(X16,implies(falsehood,falsehood))),
inference(resolution,[status(thm)],[c6,c0]) ).
cnf(c10,plain,
is_a_theorem(implies(X21,implies(X22,implies(falsehood,falsehood)))),
inference(resolution,[status(thm)],[c8,c0]) ).
cnf(c24,plain,
is_a_theorem(implies(implies(X56,X57),implies(X56,X56))),
inference(resolution,[status(thm)],[c11,c0_2]) ).
cnf(c33,plain,
( ~ is_a_theorem(implies(X59,X58))
| is_a_theorem(implies(X59,X59)) ),
inference(resolution,[status(thm)],[c24,condensed_detachment]) ).
cnf(c36,plain,
is_a_theorem(implies(X60,X60)),
inference(resolution,[status(thm)],[c33,c10]) ).
cnf(c49,plain,
is_a_theorem(implies(implies(implies(X198,X199),X198),implies(implies(X198,X199),X199))),
inference(resolution,[status(thm)],[c36,c11]) ).
cnf(c160,plain,
( ~ is_a_theorem(implies(implies(X288,X289),X288))
| is_a_theorem(implies(implies(X288,X289),X289)) ),
inference(resolution,[status(thm)],[c49,condensed_detachment]) ).
cnf(c224,plain,
is_a_theorem(implies(implies(implies(X357,implies(X358,X357)),X359),X359)),
inference(resolution,[status(thm)],[c160,c1]) ).
cnf(c292,plain,
( ~ is_a_theorem(implies(implies(X471,implies(X472,X471)),X470))
| is_a_theorem(X470) ),
inference(resolution,[status(thm)],[c224,condensed_detachment]) ).
cnf(c401,plain,
is_a_theorem(implies(falsehood,X474)),
inference(resolution,[status(thm)],[c292,c29]) ).
cnf(c412,plain,
is_a_theorem(implies(X491,implies(falsehood,X492))),
inference(resolution,[status(thm)],[c401,c0]) ).
cnf(c430,plain,
is_a_theorem(implies(implies(X569,falsehood),implies(X569,X568))),
inference(resolution,[status(thm)],[c412,c11]) ).
cnf(c470,plain,
is_a_theorem(implies(X1143,implies(implies(X1145,falsehood),implies(X1145,X1144)))),
inference(resolution,[status(thm)],[c430,c0]) ).
cnf(c28,plain,
is_a_theorem(implies(implies(implies(X185,implies(X183,X184)),implies(X185,X183)),implies(implies(X185,implies(X183,X184)),implies(X185,X184)))),
inference(resolution,[status(thm)],[c11,c0_6]) ).
cnf(c141,plain,
( ~ is_a_theorem(implies(implies(X1155,implies(X1156,X1154)),implies(X1155,X1156)))
| is_a_theorem(implies(implies(X1155,implies(X1156,X1154)),implies(X1155,X1154))) ),
inference(resolution,[status(thm)],[c28,condensed_detachment]) ).
cnf(c918,plain,
is_a_theorem(implies(implies(implies(X9934,falsehood),implies(implies(X9934,X9932),X9933)),implies(implies(X9934,falsehood),X9933))),
inference(resolution,[status(thm)],[c141,c470]) ).
cnf(c154,plain,
( ~ is_a_theorem(implies(X1322,implies(implies(X1323,falsehood),falsehood)))
| is_a_theorem(implies(X1322,X1323)) ),
inference(resolution,[status(thm)],[c29,condensed_detachment]) ).
cnf(c1163,plain,
is_a_theorem(implies(implies(implies(X1337,falsehood),X1337),X1337)),
inference(resolution,[status(thm)],[c154,c49]) ).
cnf(c1199,plain,
is_a_theorem(implies(X1639,implies(implies(implies(X1640,falsehood),X1640),X1640))),
inference(resolution,[status(thm)],[c1163,c0]) ).
cnf(c1499,plain,
is_a_theorem(implies(implies(X12219,implies(implies(X12218,falsehood),X12218)),implies(X12219,X12218))),
inference(resolution,[status(thm)],[c1199,c11]) ).
cnf(c17431,plain,
( ~ is_a_theorem(implies(X19554,implies(implies(X19555,falsehood),X19555)))
| is_a_theorem(implies(X19554,X19555)) ),
inference(resolution,[status(thm)],[c1499,condensed_detachment]) ).
cnf(c30974,plain,
is_a_theorem(implies(implies(implies(X27095,falsehood),implies(implies(X27095,X27094),X27095)),X27095)),
inference(resolution,[status(thm)],[c17431,c918]) ).
cnf(c3,plain,
is_a_theorem(implies(X25,implies(X26,implies(X27,implies(X28,X27))))),
inference(resolution,[status(thm)],[c1,c0]) ).
cnf(c219,plain,
is_a_theorem(implies(implies(implies(X2058,implies(X2057,implies(X2059,X2057))),X2060),X2060)),
inference(resolution,[status(thm)],[c160,c3]) ).
cnf(c2235,plain,
( ~ is_a_theorem(implies(implies(X3186,implies(X3185,implies(X3184,X3185))),X3183))
| is_a_theorem(X3183) ),
inference(resolution,[status(thm)],[c219,condensed_detachment]) ).
cnf(c12,plain,
is_a_theorem(implies(X63,implies(implies(X65,implies(X66,X64)),implies(implies(X65,X66),implies(X65,X64))))),
inference(resolution,[status(thm)],[c0_6,c0]) ).
cnf(c52,plain,
is_a_theorem(implies(implies(X304,implies(X306,implies(X305,X303))),implies(X304,implies(implies(X306,X305),implies(X306,X303))))),
inference(resolution,[status(thm)],[c12,c11]) ).
cnf(c385,plain,
is_a_theorem(implies(implies(X2641,X2640),implies(implies(X2642,X2641),implies(X2642,X2640)))),
inference(resolution,[status(thm)],[c292,c52]) ).
cnf(c3089,plain,
is_a_theorem(implies(implies(implies(X42231,X42230),implies(X42232,X42231)),implies(implies(X42231,X42230),implies(X42232,X42230)))),
inference(resolution,[status(thm)],[c385,c11]) ).
cnf(c90323,plain,
is_a_theorem(implies(implies(implies(X42249,X42248),X42250),implies(X42248,X42250))),
inference(resolution,[status(thm)],[c3089,c2235]) ).
cnf(c90565,plain,
( ~ is_a_theorem(implies(implies(X42457,X42458),X42459))
| is_a_theorem(implies(X42458,X42459)) ),
inference(resolution,[status(thm)],[c90323,condensed_detachment]) ).
cnf(c91708,plain,
is_a_theorem(implies(implies(implies(X43109,X43110),X43109),X43109)),
inference(resolution,[status(thm)],[c90565,c30974]) ).
cnf(c95165,plain,
$false,
inference(resolution,[status(thm)],[c91708,prove_c0_3]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL026-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.03 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.09/0.34 % Computer : n028.cluster.edu
% 0.09/0.34 % Model : x86_64 x86_64
% 0.09/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.34 % Memory : 8046.5625MB
% 0.09/0.34 % OS : Linux 6.8.0-71-generic
% 0.09/0.34 % CPULimit : 300
% 0.09/0.34 % WCLimit : 300
% 0.09/0.34 % DateTime : Sat Sep 5 12:35:14 UTC 2026
% 0.09/0.34 % CPUTime :
% 0.11/0.40 /export/starexec/sandbox/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.11/0.40 (re.compile("\."), Token.FullStop),
% 0.11/0.40 /export/starexec/sandbox/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.11/0.40 (re.compile("\("), Token.OpenPar),
% 0.11/0.40 /export/starexec/sandbox/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.11/0.40 (re.compile("\)"), Token.ClosePar),
% 0.11/0.40 /export/starexec/sandbox/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.11/0.40 (re.compile("\["), Token.OpenSquare),
% 0.11/0.40 /export/starexec/sandbox/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.11/0.40 (re.compile("\]"), Token.CloseSquare),
% 0.11/0.40 /export/starexec/sandbox/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.11/0.40 (re.compile("~\|"), Token.Nor),
% 0.11/0.40 /export/starexec/sandbox/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.11/0.40 (re.compile("\|"), Token.Or),
% 0.11/0.40 /export/starexec/sandbox/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.11/0.40 (re.compile("\?"), Token.Existential),
% 0.11/0.40 /export/starexec/sandbox/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.11/0.40 (re.compile("\s+"), Token.WhiteSpace),
% 0.11/0.40 /export/starexec/sandbox/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.11/0.40 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.21/0.47 /export/starexec/sandbox/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.21/0.47 """
% 0.21/0.48 /export/starexec/sandbox/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.21/0.48 """
% 0.31/0.57 /export/starexec/sandbox/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.31/0.57 """
% 209.28/209.85 % Version: 1.5
% 209.28/209.85 % SZS status Unsatisfiable
% 209.28/209.85 % SZS output start CNFRefutation
% See solution above
% 209.28/209.86
% 209.28/209.86 % Initial clauses : 5
% 209.28/209.86 % Processed clauses : 1186
% 209.28/209.86 % Factors computed : 0
% 209.28/209.86 % Resolvents computed: 95191
% 209.28/209.86 % Tautologies deleted: 2
% 209.28/209.86 % Forward subsumed : 11971
% 209.28/209.86 % Backward subsumed : 21
% 209.28/209.86 % -------- CPU Time ---------
% 209.28/209.86 % User time : 208.961 s
% 209.28/209.86 % System time : 0.275 s
% 209.28/209.86 % Total time : 209.236 s
%------------------------------------------------------------------------------