%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : LCL401-1 : TPTP v9.3.1. Released v2.3.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n020.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:58:25 PM UTC 2026
% Result : Unsatisfiable 247.44s 247.77s
% Output : CNFRefutation 247.44s
% Verified :
% SZS Type : Refutation
% Derivation depth : 37
% Number of leaves : 5
% Syntax : Number of clauses : 72 ( 52 unt; 0 nHn; 13 RR)
% Number of literals : 93 ( 0 equ; 22 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; 2 con; 0-2 aty)
% Number of variables : 190 ( 58 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(prove_cn_67,negated_conjecture,
~ is_a_theorem(implies(not(implies(x,y)),not(y))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_cn_67) ).
cnf(condensed_detachment,axiom,
( ~ is_a_theorem(implies(X5,X6))
| ~ is_a_theorem(X5)
| is_a_theorem(X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',condensed_detachment) ).
cnf(cn_1,axiom,
is_a_theorem(implies(implies(X10,X12),implies(implies(X12,X11),implies(X10,X11)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cn_1) ).
cnf(c5,plain,
( ~ is_a_theorem(implies(X31,X30))
| is_a_theorem(implies(implies(X30,X32),implies(X31,X32))) ),
inference(resolution,[status(thm)],[cn_1,condensed_detachment]) ).
cnf(c20,plain,
is_a_theorem(implies(implies(implies(implies(X167,X168),implies(X169,X168)),X170),implies(implies(X169,X167),X170))),
inference(resolution,[status(thm)],[c5,cn_1]) ).
cnf(c205,plain,
( ~ is_a_theorem(implies(implies(implies(X2839,X2841),implies(X2840,X2841)),X2842))
| is_a_theorem(implies(implies(X2840,X2839),X2842)) ),
inference(resolution,[status(thm)],[c20,condensed_detachment]) ).
cnf(cn_2,axiom,
is_a_theorem(implies(implies(not(X2),X2),X2)),
file('/export/starexec/sandbox/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(c16,plain,
is_a_theorem(implies(implies(X37,X36),implies(implies(not(X37),X37),X36))),
inference(resolution,[status(thm)],[c5,cn_2]) ).
cnf(cn_3,axiom,
is_a_theorem(implies(X3,implies(not(X3),X4))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cn_3) ).
cnf(c15,plain,
is_a_theorem(implies(implies(implies(not(X33),X34),X35),implies(X33,X35))),
inference(resolution,[status(thm)],[c5,cn_3]) ).
cnf(c23,plain,
( ~ is_a_theorem(implies(implies(not(X47),X46),X45))
| is_a_theorem(implies(X47,X45)) ),
inference(resolution,[status(thm)],[c15,condensed_detachment]) ).
cnf(c0,plain,
( ~ is_a_theorem(X7)
| is_a_theorem(implies(not(X7),X8)) ),
inference(resolution,[status(thm)],[condensed_detachment,cn_3]) ).
cnf(c32,plain,
is_a_theorem(implies(X48,X48)),
inference(resolution,[status(thm)],[c23,cn_2]) ).
cnf(c37,plain,
is_a_theorem(implies(not(implies(X55,X55)),X56)),
inference(resolution,[status(thm)],[c32,c0]) ).
cnf(c43,plain,
is_a_theorem(implies(implies(X121,X120),implies(not(implies(X119,X119)),X120))),
inference(resolution,[status(thm)],[c37,c5]) ).
cnf(c117,plain,
is_a_theorem(implies(X123,implies(not(implies(X122,X122)),X124))),
inference(resolution,[status(thm)],[c43,c23]) ).
cnf(c122,plain,
is_a_theorem(implies(implies(implies(not(implies(X217,X217)),X216),X218),implies(X219,X218))),
inference(resolution,[status(thm)],[c117,c5]) ).
cnf(c247,plain,
( ~ is_a_theorem(implies(implies(not(implies(X222,X222)),X223),X220))
| is_a_theorem(implies(X221,X220)) ),
inference(resolution,[status(thm)],[c122,condensed_detachment]) ).
cnf(c257,plain,
is_a_theorem(implies(X225,implies(X224,X224))),
inference(resolution,[status(thm)],[c247,cn_2]) ).
cnf(c265,plain,
is_a_theorem(implies(implies(implies(X269,X269),X270),implies(X268,X270))),
inference(resolution,[status(thm)],[c257,c5]) ).
cnf(c314,plain,
( ~ is_a_theorem(implies(implies(X273,X273),X271))
| is_a_theorem(implies(X272,X271)) ),
inference(resolution,[status(thm)],[c265,condensed_detachment]) ).
cnf(c322,plain,
is_a_theorem(implies(X305,implies(implies(not(X304),X304),X304))),
inference(resolution,[status(thm)],[c314,c16]) ).
cnf(c359,plain,
is_a_theorem(implies(implies(implies(implies(not(X843),X843),X843),X842),implies(X841,X842))),
inference(resolution,[status(thm)],[c322,c5]) ).
cnf(c712,plain,
( ~ is_a_theorem(implies(implies(implies(not(X1007),X1007),X1007),X1009))
| is_a_theorem(implies(X1008,X1009)) ),
inference(resolution,[status(thm)],[c359,condensed_detachment]) ).
cnf(c311,plain,
is_a_theorem(implies(implies(implies(X1573,X1575),X1574),implies(implies(implies(X1576,X1576),X1575),X1574))),
inference(resolution,[status(thm)],[c265,c5]) ).
cnf(c1191,plain,
is_a_theorem(implies(X1578,implies(implies(implies(X1577,X1577),X1579),X1579))),
inference(resolution,[status(thm)],[c311,c712]) ).
cnf(c1205,plain,
is_a_theorem(implies(implies(implies(X1581,X1581),X1580),X1580)),
inference(resolution,[status(thm)],[c1191,c1]) ).
cnf(c21,plain,
is_a_theorem(implies(implies(implies(X190,X187),X189),implies(implies(implies(not(X190),X188),X187),X189))),
inference(resolution,[status(thm)],[c15,c5]) ).
cnf(c231,plain,
( ~ is_a_theorem(implies(implies(X3229,X3227),X3230))
| is_a_theorem(implies(implies(implies(not(X3229),X3228),X3227),X3230)) ),
inference(resolution,[status(thm)],[c21,condensed_detachment]) ).
cnf(c3830,plain,
is_a_theorem(implies(implies(implies(not(implies(X3241,X3241)),X3242),X3240),X3240)),
inference(resolution,[status(thm)],[c231,c1205]) ).
cnf(c3851,plain,
( ~ is_a_theorem(implies(implies(not(implies(X3289,X3289)),X3290),X3291))
| is_a_theorem(X3291) ),
inference(resolution,[status(thm)],[c3830,condensed_detachment]) ).
cnf(c2891,plain,
is_a_theorem(implies(implies(X4081,implies(not(X4079),X4079)),implies(X4080,implies(X4081,X4079)))),
inference(resolution,[status(thm)],[c205,c359]) ).
cnf(c5220,plain,
( ~ is_a_theorem(implies(X5135,implies(not(X5134),X5134)))
| is_a_theorem(implies(X5133,implies(X5135,X5134))) ),
inference(resolution,[status(thm)],[c2891,condensed_detachment]) ).
cnf(c5204,plain,
is_a_theorem(implies(implies(not(X5019),X5021),implies(X5020,implies(implies(X5021,X5019),X5019)))),
inference(resolution,[status(thm)],[c2891,c205]) ).
cnf(c325,plain,
is_a_theorem(implies(X284,implies(X283,implies(X285,X285)))),
inference(resolution,[status(thm)],[c314,c265]) ).
cnf(c347,plain,
is_a_theorem(implies(implies(implies(X421,implies(X418,X418)),X420),implies(X419,X420))),
inference(resolution,[status(thm)],[c325,c5]) ).
cnf(c7202,plain,
is_a_theorem(implies(X5495,implies(implies(implies(X5497,implies(X5498,X5498)),X5496),X5496))),
inference(resolution,[status(thm)],[c5220,c347]) ).
cnf(c8154,plain,
is_a_theorem(implies(implies(implies(X5501,implies(X5502,X5502)),X5503),X5503)),
inference(resolution,[status(thm)],[c7202,c3851]) ).
cnf(c8213,plain,
( ~ is_a_theorem(implies(implies(X5547,implies(X5549,X5549)),X5548))
| is_a_theorem(X5548) ),
inference(resolution,[status(thm)],[c8154,condensed_detachment]) ).
cnf(c6630,plain,
is_a_theorem(implies(X5030,implies(X5031,implies(implies(X5032,X5030),X5030)))),
inference(resolution,[status(thm)],[c5204,c23]) ).
cnf(c7128,plain,
is_a_theorem(implies(X5175,implies(X5176,implies(implies(X5177,X5176),X5176)))),
inference(resolution,[status(thm)],[c5220,c6630]) ).
cnf(c7225,plain,
is_a_theorem(implies(X5179,implies(implies(X5178,X5179),X5179))),
inference(resolution,[status(thm)],[c7128,c3851]) ).
cnf(c7262,plain,
is_a_theorem(implies(implies(implies(implies(X5988,X5986),X5986),X5987),implies(X5986,X5987))),
inference(resolution,[status(thm)],[c7225,c5]) ).
cnf(c8948,plain,
is_a_theorem(implies(implies(X6227,implies(X6228,X6226)),implies(X6226,implies(X6227,X6226)))),
inference(resolution,[status(thm)],[c7262,c205]) ).
cnf(c9194,plain,
is_a_theorem(implies(X6230,implies(X6229,X6230))),
inference(resolution,[status(thm)],[c8948,c8213]) ).
cnf(c9226,plain,
is_a_theorem(implies(implies(implies(X6490,X6488),X6489),implies(X6488,X6489))),
inference(resolution,[status(thm)],[c9194,c5]) ).
cnf(c9934,plain,
( ~ is_a_theorem(implies(implies(X6612,X6611),X6610))
| is_a_theorem(implies(X6611,X6610)) ),
inference(resolution,[status(thm)],[c9226,condensed_detachment]) ).
cnf(c10073,plain,
is_a_theorem(implies(X6910,implies(X6911,implies(implies(X6910,X6912),X6912)))),
inference(resolution,[status(thm)],[c9934,c5204]) ).
cnf(c11257,plain,
is_a_theorem(implies(X7044,implies(X7045,implies(implies(X7045,X7046),X7046)))),
inference(resolution,[status(thm)],[c10073,c5220]) ).
cnf(c11805,plain,
is_a_theorem(implies(X7048,implies(implies(X7048,X7047),X7047))),
inference(resolution,[status(thm)],[c11257,c3851]) ).
cnf(c11839,plain,
( ~ is_a_theorem(X7067)
| is_a_theorem(implies(implies(X7067,X7066),X7066)) ),
inference(resolution,[status(thm)],[c11805,condensed_detachment]) ).
cnf(c12043,plain,
is_a_theorem(implies(implies(implies(implies(not(X8450),X8450),X8450),X8449),X8449)),
inference(resolution,[status(thm)],[c11839,cn_2]) ).
cnf(c15681,plain,
is_a_theorem(implies(implies(X9457,implies(not(X9456),X9456)),implies(X9457,X9456))),
inference(resolution,[status(thm)],[c12043,c205]) ).
cnf(c18965,plain,
is_a_theorem(implies(implies(not(X10054),X10055),implies(implies(X10055,X10054),X10054))),
inference(resolution,[status(thm)],[c15681,c205]) ).
cnf(c20807,plain,
( ~ is_a_theorem(implies(not(X10785),X10784))
| is_a_theorem(implies(implies(X10784,X10785),X10785)) ),
inference(resolution,[status(thm)],[c18965,condensed_detachment]) ).
cnf(c12149,plain,
is_a_theorem(implies(implies(implies(X7228,implies(X7230,X7228)),X7229),X7229)),
inference(resolution,[status(thm)],[c11839,c9194]) ).
cnf(c13035,plain,
is_a_theorem(implies(implies(X7283,X7285),implies(X7283,implies(X7284,X7285)))),
inference(resolution,[status(thm)],[c12149,c205]) ).
cnf(c13474,plain,
( ~ is_a_theorem(implies(X7446,X7444))
| is_a_theorem(implies(X7446,implies(X7445,X7444))) ),
inference(resolution,[status(thm)],[c13035,condensed_detachment]) ).
cnf(c18970,plain,
( ~ is_a_theorem(implies(X10085,implies(not(X10084),X10084)))
| is_a_theorem(implies(X10085,X10084)) ),
inference(resolution,[status(thm)],[c15681,condensed_detachment]) ).
cnf(c11873,plain,
is_a_theorem(implies(implies(implies(X8417,implies(not(X8417),X8418)),X8416),X8416)),
inference(resolution,[status(thm)],[c11839,cn_3]) ).
cnf(c15619,plain,
( ~ is_a_theorem(implies(implies(X9263,implies(not(X9263),X9261)),X9262))
| is_a_theorem(X9262) ),
inference(resolution,[status(thm)],[c11873,condensed_detachment]) ).
cnf(c11843,plain,
is_a_theorem(implies(implies(implies(implies(X14325,X14326),X14326),X14327),implies(X14325,X14327))),
inference(resolution,[status(thm)],[c11805,c5]) ).
cnf(c32898,plain,
is_a_theorem(implies(implies(X17817,implies(X17815,X17816)),implies(X17815,implies(X17817,X17816)))),
inference(resolution,[status(thm)],[c11843,c205]) ).
cnf(c41509,plain,
is_a_theorem(implies(not(X17829),implies(X17829,X17830))),
inference(resolution,[status(thm)],[c32898,c15619]) ).
cnf(c41588,plain,
is_a_theorem(implies(not(not(X17831)),X17831)),
inference(resolution,[status(thm)],[c41509,c18970]) ).
cnf(c41643,plain,
is_a_theorem(implies(not(not(X18083)),implies(X18084,X18083))),
inference(resolution,[status(thm)],[c41588,c13474]) ).
cnf(c43817,plain,
is_a_theorem(implies(implies(implies(X22407,X22408),not(X22408)),not(X22408))),
inference(resolution,[status(thm)],[c41643,c20807]) ).
cnf(c41600,plain,
is_a_theorem(implies(implies(implies(X27672,X27671),X27673),implies(not(X27672),X27673))),
inference(resolution,[status(thm)],[c41509,c5]) ).
cnf(c90928,plain,
( ~ is_a_theorem(implies(implies(X31661,X31663),X31662))
| is_a_theorem(implies(not(X31661),X31662)) ),
inference(resolution,[status(thm)],[c41600,condensed_detachment]) ).
cnf(c106865,plain,
is_a_theorem(implies(not(implies(X32332,X32331)),not(X32331))),
inference(resolution,[status(thm)],[c90928,c43817]) ).
cnf(c109457,plain,
$false,
inference(resolution,[status(thm)],[c106865,prove_cn_67]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL401-1 : TPTP v9.3.1. Released v2.3.0.
% 0.00/0.03 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.08/0.36 % Computer : n020.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Sat Sep 5 11:56:42 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.42 /export/starexec/sandbox/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.08/0.42 (re.compile("\."), Token.FullStop),
% 0.08/0.42 /export/starexec/sandbox/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.08/0.42 (re.compile("\("), Token.OpenPar),
% 0.08/0.42 /export/starexec/sandbox/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.08/0.42 (re.compile("\)"), Token.ClosePar),
% 0.08/0.42 /export/starexec/sandbox/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.08/0.42 (re.compile("\["), Token.OpenSquare),
% 0.08/0.42 /export/starexec/sandbox/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.08/0.42 (re.compile("\]"), Token.CloseSquare),
% 0.08/0.42 /export/starexec/sandbox/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.08/0.42 (re.compile("~\|"), Token.Nor),
% 0.08/0.42 /export/starexec/sandbox/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.08/0.42 (re.compile("\|"), Token.Or),
% 0.08/0.42 /export/starexec/sandbox/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.08/0.42 (re.compile("\?"), Token.Existential),
% 0.08/0.42 /export/starexec/sandbox/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.08/0.42 (re.compile("\s+"), Token.WhiteSpace),
% 0.08/0.42 /export/starexec/sandbox/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.08/0.42 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.23/0.49 /export/starexec/sandbox/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.23/0.49 """
% 0.23/0.49 /export/starexec/sandbox/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.23/0.49 """
% 0.33/0.58 /export/starexec/sandbox/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.33/0.58 """
% 247.44/247.77 % Version: 1.5
% 247.44/247.77 % SZS status Unsatisfiable
% 247.44/247.77 % SZS output start CNFRefutation
% See solution above
% 247.44/247.77
% 247.44/247.77 % Initial clauses : 5
% 247.44/247.77 % Processed clauses : 1709
% 247.44/247.77 % Factors computed : 0
% 247.44/247.77 % Resolvents computed: 109509
% 247.44/247.77 % Tautologies deleted: 1
% 247.44/247.77 % Forward subsumed : 9045
% 247.44/247.77 % Backward subsumed : 124
% 247.44/247.77 % -------- CPU Time ---------
% 247.44/247.77 % User time : 247.089 s
% 247.44/247.77 % System time : 0.300 s
% 247.44/247.77 % Total time : 247.389 s
%------------------------------------------------------------------------------