%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : LCL256-1 : TPTP v9.3.1. Released v1.1.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n006.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:11 PM UTC 2026
% Result : Unsatisfiable 46.96s 47.24s
% Output : CNFRefutation 46.96s
% Verified :
% SZS Type : Refutation
% Derivation depth : 35
% Number of leaves : 5
% Syntax : Number of clauses : 65 ( 48 unt; 0 nHn; 11 RR)
% Number of literals : 83 ( 0 equ; 19 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 : 3 ( 3 usr; 1 con; 0-2 aty)
% Number of variables : 170 ( 50 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(prove_not_not_implies,negated_conjecture,
~ is_a_theorem(not(not(implies(p,p)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_not_not_implies) ).
cnf(condensed_detachment,axiom,
( ~ is_a_theorem(implies(X6,X5))
| ~ is_a_theorem(X6)
| is_a_theorem(X5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',condensed_detachment) ).
cnf(cn_1,axiom,
is_a_theorem(implies(implies(X11,X10),implies(implies(X10,X12),implies(X11,X12)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cn_1) ).
cnf(c5,plain,
( ~ is_a_theorem(implies(X30,X32))
| is_a_theorem(implies(implies(X32,X31),implies(X30,X31))) ),
inference(resolution,[status(thm)],[cn_1,condensed_detachment]) ).
cnf(c16,plain,
is_a_theorem(implies(implies(implies(implies(X133,X132),implies(X131,X132)),X130),implies(implies(X131,X133),X130))),
inference(resolution,[status(thm)],[c5,cn_1]) ).
cnf(c133,plain,
( ~ is_a_theorem(implies(implies(implies(X1645,X1647),implies(X1644,X1647)),X1646))
| is_a_theorem(implies(implies(X1644,X1645),X1646)) ),
inference(resolution,[status(thm)],[c16,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(c20,plain,
is_a_theorem(implies(implies(X36,X37),implies(implies(not(X36),X36),X37))),
inference(resolution,[status(thm)],[c5,cn_2]) ).
cnf(cn_3,axiom,
is_a_theorem(implies(X4,implies(not(X4),X3))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cn_3) ).
cnf(c17,plain,
is_a_theorem(implies(implies(implies(not(X34),X33),X35),implies(X34,X35))),
inference(resolution,[status(thm)],[c5,cn_3]) ).
cnf(c23,plain,
( ~ is_a_theorem(implies(implies(not(X45),X46),X47))
| is_a_theorem(implies(X45,X47)) ),
inference(resolution,[status(thm)],[c17,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(c34,plain,
is_a_theorem(implies(X48,X48)),
inference(resolution,[status(thm)],[c23,cn_2]) ).
cnf(c35,plain,
is_a_theorem(implies(not(implies(X50,X50)),X51)),
inference(resolution,[status(thm)],[c34,c0]) ).
cnf(c41,plain,
is_a_theorem(implies(implies(X120,X121),implies(not(implies(X119,X119)),X121))),
inference(resolution,[status(thm)],[c35,c5]) ).
cnf(c119,plain,
is_a_theorem(implies(X122,implies(not(implies(X123,X123)),X124))),
inference(resolution,[status(thm)],[c41,c23]) ).
cnf(c124,plain,
is_a_theorem(implies(implies(implies(not(implies(X219,X219)),X217),X216),implies(X218,X216))),
inference(resolution,[status(thm)],[c119,c5]) ).
cnf(c249,plain,
( ~ is_a_theorem(implies(implies(not(implies(X222,X222)),X220),X221))
| is_a_theorem(implies(X223,X221)) ),
inference(resolution,[status(thm)],[c124,condensed_detachment]) ).
cnf(c258,plain,
is_a_theorem(implies(X225,implies(X224,X224))),
inference(resolution,[status(thm)],[c249,cn_2]) ).
cnf(c269,plain,
is_a_theorem(implies(implies(implies(X268,X268),X270),implies(X269,X270))),
inference(resolution,[status(thm)],[c258,c5]) ).
cnf(c311,plain,
( ~ is_a_theorem(implies(implies(X272,X272),X271))
| is_a_theorem(implies(X273,X271)) ),
inference(resolution,[status(thm)],[c269,condensed_detachment]) ).
cnf(c319,plain,
is_a_theorem(implies(X305,implies(implies(not(X304),X304),X304))),
inference(resolution,[status(thm)],[c311,c20]) ).
cnf(c356,plain,
is_a_theorem(implies(implies(implies(implies(not(X841),X841),X841),X843),implies(X842,X843))),
inference(resolution,[status(thm)],[c319,c5]) ).
cnf(c717,plain,
( ~ is_a_theorem(implies(implies(implies(not(X1034),X1034),X1034),X1035))
| is_a_theorem(implies(X1036,X1035)) ),
inference(resolution,[status(thm)],[c356,condensed_detachment]) ).
cnf(c308,plain,
is_a_theorem(implies(implies(implies(X1579,X1577),X1580),implies(implies(implies(X1578,X1578),X1577),X1580))),
inference(resolution,[status(thm)],[c269,c5]) ).
cnf(c1196,plain,
is_a_theorem(implies(X1582,implies(implies(implies(X1581,X1581),X1583),X1583))),
inference(resolution,[status(thm)],[c308,c717]) ).
cnf(c1198,plain,
is_a_theorem(implies(implies(implies(X1584,X1584),X1585),X1585)),
inference(resolution,[status(thm)],[c1196,c1]) ).
cnf(c22,plain,
is_a_theorem(implies(implies(implies(X210,X212),X209),implies(implies(implies(not(X210),X211),X212),X209))),
inference(resolution,[status(thm)],[c17,c5]) ).
cnf(c242,plain,
( ~ is_a_theorem(implies(implies(X3508,X3507),X3509))
| is_a_theorem(implies(implies(implies(not(X3508),X3506),X3507),X3509)) ),
inference(resolution,[status(thm)],[c22,condensed_detachment]) ).
cnf(c4146,plain,
is_a_theorem(implies(implies(implies(not(implies(X3514,X3514)),X3513),X3512),X3512)),
inference(resolution,[status(thm)],[c242,c1198]) ).
cnf(c4183,plain,
is_a_theorem(implies(implies(X3546,not(implies(X3547,X3547))),implies(X3546,X3545))),
inference(resolution,[status(thm)],[c4146,c133]) ).
cnf(c1329,plain,
is_a_theorem(implies(implies(X3063,implies(not(X3062),X3062)),implies(X3064,implies(X3063,X3062)))),
inference(resolution,[status(thm)],[c133,c356]) ).
cnf(c3472,plain,
( ~ is_a_theorem(implies(X4292,implies(not(X4294),X4294)))
| is_a_theorem(implies(X4293,implies(X4292,X4294))) ),
inference(resolution,[status(thm)],[c1329,condensed_detachment]) ).
cnf(c3457,plain,
is_a_theorem(implies(implies(not(X4175),X4174),implies(X4176,implies(implies(X4174,X4175),X4175)))),
inference(resolution,[status(thm)],[c1329,c133]) ).
cnf(c320,plain,
is_a_theorem(implies(X283,implies(X285,implies(X284,X284)))),
inference(resolution,[status(thm)],[c311,c269]) ).
cnf(c344,plain,
is_a_theorem(implies(implies(implies(X418,implies(X419,X419)),X421),implies(X420,X421))),
inference(resolution,[status(thm)],[c320,c5]) ).
cnf(c5486,plain,
is_a_theorem(implies(X4521,implies(implies(implies(X4522,implies(X4524,X4524)),X4523),X4523))),
inference(resolution,[status(thm)],[c3472,c344]) ).
cnf(c6279,plain,
is_a_theorem(implies(implies(implies(X4533,implies(X4534,X4534)),X4532),X4532)),
inference(resolution,[status(thm)],[c5486,c1]) ).
cnf(c6326,plain,
( ~ is_a_theorem(implies(implies(X4577,implies(X4579,X4579)),X4578))
| is_a_theorem(X4578) ),
inference(resolution,[status(thm)],[c6279,condensed_detachment]) ).
cnf(c5146,plain,
is_a_theorem(implies(X4187,implies(X4188,implies(implies(X4189,X4187),X4187)))),
inference(resolution,[status(thm)],[c3457,c23]) ).
cnf(c5606,plain,
is_a_theorem(implies(X4339,implies(X4340,implies(implies(X4338,X4340),X4340)))),
inference(resolution,[status(thm)],[c3472,c5146]) ).
cnf(c5686,plain,
is_a_theorem(implies(X4347,implies(implies(X4346,X4347),X4347))),
inference(resolution,[status(thm)],[c5606,c1]) ).
cnf(c5739,plain,
is_a_theorem(implies(implies(implies(implies(X4988,X4989),X4989),X4990),implies(X4989,X4990))),
inference(resolution,[status(thm)],[c5686,c5]) ).
cnf(c6880,plain,
is_a_theorem(implies(implies(X5129,implies(X5128,X5127)),implies(X5127,implies(X5129,X5127)))),
inference(resolution,[status(thm)],[c5739,c133]) ).
cnf(c7009,plain,
is_a_theorem(implies(X5130,implies(X5131,X5130))),
inference(resolution,[status(thm)],[c6880,c6326]) ).
cnf(c7019,plain,
is_a_theorem(implies(implies(implies(X5385,X5386),X5387),implies(X5386,X5387))),
inference(resolution,[status(thm)],[c7009,c5]) ).
cnf(c7683,plain,
( ~ is_a_theorem(implies(implies(X5493,X5495),X5494))
| is_a_theorem(implies(X5495,X5494)) ),
inference(resolution,[status(thm)],[c7019,condensed_detachment]) ).
cnf(c7873,plain,
is_a_theorem(implies(X5793,implies(X5795,implies(implies(X5793,X5794),X5794)))),
inference(resolution,[status(thm)],[c7683,c3457]) ).
cnf(c9336,plain,
is_a_theorem(implies(X5923,implies(X5924,implies(implies(X5924,X5925),X5925)))),
inference(resolution,[status(thm)],[c7873,c3472]) ).
cnf(c9891,plain,
is_a_theorem(implies(X5927,implies(implies(X5927,X5926),X5926))),
inference(resolution,[status(thm)],[c9336,c1]) ).
cnf(c9941,plain,
( ~ is_a_theorem(X5953)
| is_a_theorem(implies(implies(X5953,X5952),X5952)) ),
inference(resolution,[status(thm)],[c9891,condensed_detachment]) ).
cnf(c10155,plain,
is_a_theorem(implies(implies(implies(implies(not(X7427),X7427),X7427),X7426),X7426)),
inference(resolution,[status(thm)],[c9941,cn_2]) ).
cnf(c13590,plain,
is_a_theorem(implies(implies(X8409,implies(not(X8408),X8408)),implies(X8409,X8408))),
inference(resolution,[status(thm)],[c10155,c133]) ).
cnf(c16378,plain,
( ~ is_a_theorem(implies(X8994,implies(not(X8993),X8993)))
| is_a_theorem(implies(X8994,X8993)) ),
inference(resolution,[status(thm)],[c13590,condensed_detachment]) ).
cnf(c17938,plain,
is_a_theorem(implies(implies(not(X9198),not(implies(X9197,X9197))),X9198)),
inference(resolution,[status(thm)],[c16378,c4183]) ).
cnf(c18455,plain,
( ~ is_a_theorem(implies(not(X9391),not(implies(X9390,X9390))))
| is_a_theorem(X9391) ),
inference(resolution,[status(thm)],[c17938,condensed_detachment]) ).
cnf(c10038,plain,
is_a_theorem(implies(implies(implies(X7398,implies(not(X7398),X7397)),X7396),X7396)),
inference(resolution,[status(thm)],[c9941,cn_3]) ).
cnf(c13532,plain,
( ~ is_a_theorem(implies(implies(X8215,implies(not(X8215),X8214)),X8213))
| is_a_theorem(X8213) ),
inference(resolution,[status(thm)],[c10038,condensed_detachment]) ).
cnf(c9932,plain,
is_a_theorem(implies(implies(implies(implies(X13204,X13203),X13203),X13205),implies(X13204,X13205))),
inference(resolution,[status(thm)],[c9891,c5]) ).
cnf(c29084,plain,
is_a_theorem(implies(implies(X17091,implies(X17092,X17090)),implies(X17092,implies(X17091,X17090)))),
inference(resolution,[status(thm)],[c9932,c133]) ).
cnf(c39693,plain,
is_a_theorem(implies(not(X17101),implies(X17101,X17100))),
inference(resolution,[status(thm)],[c29084,c13532]) ).
cnf(c39780,plain,
is_a_theorem(implies(not(not(X17102)),X17102)),
inference(resolution,[status(thm)],[c39693,c16378]) ).
cnf(c39824,plain,
is_a_theorem(not(not(implies(X17104,X17104)))),
inference(resolution,[status(thm)],[c39780,c18455]) ).
cnf(c39860,plain,
$false,
inference(resolution,[status(thm)],[c39824,prove_not_not_implies]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL256-1 : TPTP v9.3.1. Released v1.1.0.
% 0.00/0.04 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.08/0.36 % Computer : n006.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 23:26:16 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.14/0.42 /export/starexec/sandbox/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.14/0.42 (re.compile("\."), Token.FullStop),
% 0.14/0.42 /export/starexec/sandbox/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.14/0.42 (re.compile("\("), Token.OpenPar),
% 0.14/0.42 /export/starexec/sandbox/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.14/0.42 (re.compile("\)"), Token.ClosePar),
% 0.14/0.42 /export/starexec/sandbox/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.14/0.42 (re.compile("\["), Token.OpenSquare),
% 0.14/0.42 /export/starexec/sandbox/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.14/0.42 (re.compile("\]"), Token.CloseSquare),
% 0.14/0.42 /export/starexec/sandbox/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.14/0.42 (re.compile("~\|"), Token.Nor),
% 0.14/0.42 /export/starexec/sandbox/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.14/0.42 (re.compile("\|"), Token.Or),
% 0.14/0.42 /export/starexec/sandbox/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.14/0.42 (re.compile("\?"), Token.Existential),
% 0.14/0.42 /export/starexec/sandbox/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.14/0.42 (re.compile("\s+"), Token.WhiteSpace),
% 0.14/0.42 /export/starexec/sandbox/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.14/0.42 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.24/0.49 /export/starexec/sandbox/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.24/0.49 """
% 0.24/0.49 /export/starexec/sandbox/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.24/0.49 """
% 0.34/0.59 /export/starexec/sandbox/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.34/0.59 """
% 46.96/47.24 % Version: 1.5
% 46.96/47.24 % SZS status Unsatisfiable
% 46.96/47.24 % SZS output start CNFRefutation
% See solution above
% 46.96/47.24
% 46.96/47.24 % Initial clauses : 5
% 46.96/47.24 % Processed clauses : 895
% 46.96/47.24 % Factors computed : 0
% 46.96/47.24 % Resolvents computed: 39868
% 46.96/47.24 % Tautologies deleted: 1
% 46.96/47.24 % Forward subsumed : 4340
% 46.96/47.24 % Backward subsumed : 64
% 46.96/47.24 % -------- CPU Time ---------
% 46.96/47.24 % User time : 46.738 s
% 46.96/47.24 % System time : 0.133 s
% 46.96/47.24 % Total time : 46.871 s
%------------------------------------------------------------------------------