%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : LCL050-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n011.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:45 PM UTC 2026
% Result : Unsatisfiable 57.15s 57.44s
% Output : CNFRefutation 57.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 32
% Number of leaves : 5
% Syntax : Number of clauses : 49 ( 36 unt; 0 nHn; 9 RR)
% Number of literals : 63 ( 0 equ; 15 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 : 5 ( 5 usr; 3 con; 0-2 aty)
% Number of variables : 129 ( 39 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(prove_cn_21,negated_conjecture,
~ is_a_theorem(implies(implies(a,implies(b,c)),implies(b,implies(a,c)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_cn_21) ).
cnf(condensed_detachment,axiom,
( ~ is_a_theorem(implies(X6,X5))
| ~ is_a_theorem(X6)
| is_a_theorem(X5) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',condensed_detachment) ).
cnf(cn_1,axiom,
is_a_theorem(implies(implies(X12,X10),implies(implies(X10,X11),implies(X12,X11)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cn_1) ).
cnf(c5,plain,
( ~ is_a_theorem(implies(X26,X28))
| is_a_theorem(implies(implies(X28,X27),implies(X26,X27))) ),
inference(resolution,[status(thm)],[cn_1,condensed_detachment]) ).
cnf(c15,plain,
is_a_theorem(implies(implies(implies(implies(X112,X111),implies(X110,X111)),X113),implies(implies(X110,X112),X113))),
inference(resolution,[status(thm)],[c5,cn_1]) ).
cnf(c116,plain,
( ~ is_a_theorem(implies(implies(implies(X1461,X1460),implies(X1459,X1460)),X1458))
| is_a_theorem(implies(implies(X1459,X1461),X1458)) ),
inference(resolution,[status(thm)],[c15,condensed_detachment]) ).
cnf(cn_3,axiom,
is_a_theorem(implies(X4,implies(not(X4),X3))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cn_3) ).
cnf(c14,plain,
is_a_theorem(implies(implies(implies(not(X31),X29),X30),implies(X31,X30))),
inference(resolution,[status(thm)],[c5,cn_3]) ).
cnf(c19,plain,
is_a_theorem(implies(implies(implies(X150,X148),X149),implies(implies(implies(not(X150),X147),X148),X149))),
inference(resolution,[status(thm)],[c14,c5]) ).
cnf(c164,plain,
( ~ is_a_theorem(implies(implies(X2329,X2327),X2328))
| is_a_theorem(implies(implies(implies(not(X2329),X2326),X2327),X2328)) ),
inference(resolution,[status(thm)],[c19,condensed_detachment]) ).
cnf(cn_2,axiom,
is_a_theorem(implies(implies(not(X2),X2),X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cn_2) ).
cnf(c1,plain,
( ~ is_a_theorem(implies(not(X9),X9))
| is_a_theorem(X9) ),
inference(resolution,[status(thm)],[condensed_detachment,cn_2]) ).
cnf(c18,plain,
( ~ is_a_theorem(implies(implies(not(X36),X34),X35))
| is_a_theorem(implies(X36,X35)) ),
inference(resolution,[status(thm)],[c14,condensed_detachment]) ).
cnf(c0,plain,
( ~ is_a_theorem(X8)
| is_a_theorem(implies(not(X8),X7)) ),
inference(resolution,[status(thm)],[condensed_detachment,cn_3]) ).
cnf(c26,plain,
is_a_theorem(implies(X41,X41)),
inference(resolution,[status(thm)],[c18,cn_2]) ).
cnf(c32,plain,
is_a_theorem(implies(not(implies(X45,X45)),X46)),
inference(resolution,[status(thm)],[c26,c0]) ).
cnf(c37,plain,
is_a_theorem(implies(implies(X116,X115),implies(not(implies(X114,X114)),X115))),
inference(resolution,[status(thm)],[c32,c5]) ).
cnf(c120,plain,
is_a_theorem(implies(X117,implies(not(implies(X119,X119)),X118))),
inference(resolution,[status(thm)],[c37,c18]) ).
cnf(c129,plain,
is_a_theorem(implies(implies(implies(not(implies(X218,X218)),X215),X217),implies(X216,X217))),
inference(resolution,[status(thm)],[c120,c5]) ).
cnf(c254,plain,
( ~ is_a_theorem(implies(implies(not(implies(X221,X221)),X219),X222))
| is_a_theorem(implies(X220,X222)) ),
inference(resolution,[status(thm)],[c129,condensed_detachment]) ).
cnf(c261,plain,
is_a_theorem(implies(X224,implies(X223,X223))),
inference(resolution,[status(thm)],[c254,cn_2]) ).
cnf(c276,plain,
is_a_theorem(implies(implies(implies(X272,X272),X271),implies(X270,X271))),
inference(resolution,[status(thm)],[c261,c5]) ).
cnf(c16,plain,
is_a_theorem(implies(implies(X32,X33),implies(implies(not(X32),X32),X33))),
inference(resolution,[status(thm)],[c5,cn_2]) ).
cnf(c308,plain,
( ~ is_a_theorem(implies(implies(X275,X275),X273))
| is_a_theorem(implies(X274,X273)) ),
inference(resolution,[status(thm)],[c276,condensed_detachment]) ).
cnf(c319,plain,
is_a_theorem(implies(X316,implies(implies(not(X315),X315),X315))),
inference(resolution,[status(thm)],[c308,c16]) ).
cnf(c383,plain,
is_a_theorem(implies(implies(implies(implies(not(X906),X906),X906),X905),implies(X904,X905))),
inference(resolution,[status(thm)],[c319,c5]) ).
cnf(c1193,plain,
is_a_theorem(implies(implies(X2115,implies(not(X2116),X2116)),implies(X2117,implies(X2115,X2116)))),
inference(resolution,[status(thm)],[c116,c383]) ).
cnf(c2110,plain,
( ~ is_a_theorem(implies(X2396,implies(not(X2395),X2395)))
| is_a_theorem(implies(X2397,implies(X2396,X2395))) ),
inference(resolution,[status(thm)],[c1193,condensed_detachment]) ).
cnf(c2583,plain,
is_a_theorem(implies(X2435,implies(implies(implies(X2434,X2434),X2433),X2433))),
inference(resolution,[status(thm)],[c2110,c276]) ).
cnf(c2680,plain,
is_a_theorem(implies(implies(implies(X2440,X2440),X2441),X2441)),
inference(resolution,[status(thm)],[c2583,c1]) ).
cnf(c2708,plain,
is_a_theorem(implies(implies(implies(not(implies(X2667,X2667)),X2666),X2665),X2665)),
inference(resolution,[status(thm)],[c2680,c164]) ).
cnf(c2955,plain,
( ~ is_a_theorem(implies(implies(not(implies(X2754,X2754)),X2753),X2752))
| is_a_theorem(X2752) ),
inference(resolution,[status(thm)],[c2708,condensed_detachment]) ).
cnf(c2121,plain,
is_a_theorem(implies(implies(not(X4587),X4588),implies(X4586,implies(implies(X4588,X4587),X4587)))),
inference(resolution,[status(thm)],[c1193,c116]) ).
cnf(c23,plain,
is_a_theorem(implies(X151,implies(implies(not(not(X151)),not(X151)),X152))),
inference(resolution,[status(thm)],[c18,c16]) ).
cnf(c172,plain,
is_a_theorem(implies(implies(implies(implies(not(not(X2460)),not(X2460)),X2461),X2462),implies(X2460,X2462))),
inference(resolution,[status(thm)],[c23,c5]) ).
cnf(c5530,plain,
is_a_theorem(implies(X4600,implies(X4602,implies(implies(X4601,X4600),X4600)))),
inference(resolution,[status(thm)],[c2121,c18]) ).
cnf(c5575,plain,
is_a_theorem(implies(X4619,implies(X4618,implies(implies(X4617,X4618),X4618)))),
inference(resolution,[status(thm)],[c5530,c2110]) ).
cnf(c5849,plain,
is_a_theorem(implies(X4621,implies(implies(X4620,X4621),X4621))),
inference(resolution,[status(thm)],[c5575,c2955]) ).
cnf(c5884,plain,
is_a_theorem(implies(implies(implies(implies(X4845,X4844),X4844),X4846),implies(X4844,X4846))),
inference(resolution,[status(thm)],[c5849,c5]) ).
cnf(c6793,plain,
( ~ is_a_theorem(implies(implies(implies(X4975,X4974),X4974),X4976))
| is_a_theorem(implies(X4974,X4976)) ),
inference(resolution,[status(thm)],[c5884,condensed_detachment]) ).
cnf(c6951,plain,
is_a_theorem(implies(X4985,implies(X4984,X4985))),
inference(resolution,[status(thm)],[c6793,c172]) ).
cnf(c7118,plain,
is_a_theorem(implies(implies(implies(X5346,X5344),X5345),implies(X5344,X5345))),
inference(resolution,[status(thm)],[c6951,c5]) ).
cnf(c7960,plain,
( ~ is_a_theorem(implies(implies(X5459,X5461),X5460))
| is_a_theorem(implies(X5461,X5460)) ),
inference(resolution,[status(thm)],[c7118,condensed_detachment]) ).
cnf(c8248,plain,
is_a_theorem(implies(X5775,implies(X5777,implies(implies(X5775,X5776),X5776)))),
inference(resolution,[status(thm)],[c7960,c2121]) ).
cnf(c9185,plain,
is_a_theorem(implies(X5870,implies(X5868,implies(implies(X5868,X5869),X5869)))),
inference(resolution,[status(thm)],[c8248,c2110]) ).
cnf(c9889,plain,
is_a_theorem(implies(X5873,implies(implies(X5873,X5874),X5874))),
inference(resolution,[status(thm)],[c9185,c2955]) ).
cnf(c9933,plain,
is_a_theorem(implies(implies(implies(implies(X12834,X12835),X12835),X12836),implies(X12834,X12836))),
inference(resolution,[status(thm)],[c9889,c5]) ).
cnf(c28186,plain,
is_a_theorem(implies(implies(X16291,implies(X16290,X16292)),implies(X16290,implies(X16291,X16292)))),
inference(resolution,[status(thm)],[c9933,c116]) ).
cnf(c36950,plain,
$false,
inference(resolution,[status(thm)],[c28186,prove_cn_21]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : LCL050-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.06 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.17/0.43 % Computer : n011.cluster.edu
% 0.17/0.43 % Model : x86_64 x86_64
% 0.17/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.43 % Memory : 8046.5625MB
% 0.17/0.43 % OS : Linux 6.8.0-71-generic
% 0.17/0.43 % CPULimit : 300
% 0.17/0.43 % WCLimit : 300
% 0.17/0.43 % DateTime : Sat Sep 5 21:42:14 UTC 2026
% 0.17/0.44 % CPUTime :
% 0.26/0.52 /export/starexec/sandbox2/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.26/0.52 (re.compile("\."), Token.FullStop),
% 0.26/0.52 /export/starexec/sandbox2/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.26/0.52 (re.compile("\("), Token.OpenPar),
% 0.26/0.52 /export/starexec/sandbox2/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.26/0.52 (re.compile("\)"), Token.ClosePar),
% 0.26/0.52 /export/starexec/sandbox2/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.26/0.52 (re.compile("\["), Token.OpenSquare),
% 0.26/0.52 /export/starexec/sandbox2/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.26/0.52 (re.compile("\]"), Token.CloseSquare),
% 0.26/0.52 /export/starexec/sandbox2/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.26/0.52 (re.compile("~\|"), Token.Nor),
% 0.26/0.52 /export/starexec/sandbox2/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.26/0.53 (re.compile("\|"), Token.Or),
% 0.26/0.53 /export/starexec/sandbox2/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.26/0.53 (re.compile("\?"), Token.Existential),
% 0.26/0.53 /export/starexec/sandbox2/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.26/0.53 (re.compile("\s+"), Token.WhiteSpace),
% 0.26/0.53 /export/starexec/sandbox2/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.26/0.53 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.35/0.63 /export/starexec/sandbox2/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.35/0.63 """
% 0.35/0.63 /export/starexec/sandbox2/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.35/0.63 """
% 0.46/0.78 /export/starexec/sandbox2/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.46/0.78 """
% 57.15/57.44 % Version: 1.5
% 57.15/57.44 % SZS status Unsatisfiable
% 57.15/57.44 % SZS output start CNFRefutation
% See solution above
% 57.15/57.44
% 57.15/57.44 % Initial clauses : 5
% 57.15/57.44 % Processed clauses : 854
% 57.15/57.44 % Factors computed : 0
% 57.15/57.44 % Resolvents computed: 36975
% 57.15/57.44 % Tautologies deleted: 1
% 57.15/57.44 % Forward subsumed : 4157
% 57.15/57.44 % Backward subsumed : 62
% 57.15/57.44 % -------- CPU Time ---------
% 57.15/57.44 % User time : 56.885 s
% 57.15/57.44 % System time : 0.119 s
% 57.15/57.44 % Total time : 57.004 s
%------------------------------------------------------------------------------