%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : LCL053-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n009.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 27.55s 27.85s
% Output : CNFRefutation 27.55s
% Verified :
% SZS Type : Refutation
% Derivation depth : 31
% Number of leaves : 5
% Syntax : Number of clauses : 51 ( 36 unt; 0 nHn; 11 RR)
% Number of literals : 67 ( 0 equ; 17 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; 2 con; 0-2 aty)
% Number of variables : 126 ( 32 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(prove_cn_30,negated_conjecture,
~ is_a_theorem(implies(implies(a,implies(a,b)),implies(a,b))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_cn_30) ).
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,X11),implies(implies(X11,X12),implies(X10,X12)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cn_1) ).
cnf(c4,plain,
( ~ is_a_theorem(implies(X27,X26))
| is_a_theorem(implies(implies(X26,X28),implies(X27,X28))) ),
inference(resolution,[status(thm)],[cn_1,condensed_detachment]) ).
cnf(c16,plain,
is_a_theorem(implies(implies(implies(implies(X111,X113),implies(X112,X113)),X110),implies(implies(X112,X111),X110))),
inference(resolution,[status(thm)],[c4,cn_1]) ).
cnf(c116,plain,
( ~ is_a_theorem(implies(implies(implies(X1456,X1457),implies(X1458,X1457)),X1455))
| is_a_theorem(implies(implies(X1458,X1456),X1455)) ),
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(c0,plain,
( ~ is_a_theorem(implies(not(X7),X7))
| is_a_theorem(X7) ),
inference(resolution,[status(thm)],[condensed_detachment,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),X31),X32),implies(X33,X32))),
inference(resolution,[status(thm)],[c4,cn_3]) ).
cnf(c21,plain,
( ~ is_a_theorem(implies(implies(not(X50),X51),X49))
| is_a_theorem(implies(X50,X49)) ),
inference(resolution,[status(thm)],[c15,condensed_detachment]) ).
cnf(c1,plain,
( ~ is_a_theorem(X9)
| is_a_theorem(implies(not(X9),X8)) ),
inference(resolution,[status(thm)],[condensed_detachment,cn_3]) ).
cnf(c43,plain,
is_a_theorem(implies(X55,X55)),
inference(resolution,[status(thm)],[c21,cn_2]) ).
cnf(c53,plain,
is_a_theorem(implies(not(implies(X59,X59)),X60)),
inference(resolution,[status(thm)],[c43,c1]) ).
cnf(c62,plain,
is_a_theorem(implies(implies(X116,X114),implies(not(implies(X115,X115)),X114))),
inference(resolution,[status(thm)],[c53,c4]) ).
cnf(c120,plain,
is_a_theorem(implies(X118,implies(not(implies(X117,X117)),X119))),
inference(resolution,[status(thm)],[c62,c21]) ).
cnf(c130,plain,
is_a_theorem(implies(implies(implies(not(implies(X216,X216)),X217),X219),implies(X218,X219))),
inference(resolution,[status(thm)],[c120,c4]) ).
cnf(c252,plain,
( ~ is_a_theorem(implies(implies(not(implies(X222,X222)),X223),X221))
| is_a_theorem(implies(X220,X221)) ),
inference(resolution,[status(thm)],[c130,condensed_detachment]) ).
cnf(c14,plain,
is_a_theorem(implies(implies(X29,X30),implies(implies(not(X29),X29),X30))),
inference(resolution,[status(thm)],[c4,cn_2]) ).
cnf(c18,plain,
( ~ is_a_theorem(implies(X35,X34))
| is_a_theorem(implies(implies(not(X35),X35),X34)) ),
inference(resolution,[status(thm)],[c14,condensed_detachment]) ).
cnf(c25,plain,
is_a_theorem(implies(implies(not(implies(X236,X235)),implies(X236,X235)),implies(implies(not(X236),X236),X235))),
inference(resolution,[status(thm)],[c18,c14]) ).
cnf(c297,plain,
is_a_theorem(implies(X264,implies(implies(not(X263),X263),X263))),
inference(resolution,[status(thm)],[c25,c252]) ).
cnf(c331,plain,
is_a_theorem(implies(implies(implies(implies(not(X905),X905),X905),X903),implies(X904,X903))),
inference(resolution,[status(thm)],[c297,c4]) ).
cnf(c1203,plain,
is_a_theorem(implies(implies(X2130,implies(not(X2132),X2132)),implies(X2131,implies(X2130,X2132)))),
inference(resolution,[status(thm)],[c116,c331]) ).
cnf(c2135,plain,
( ~ is_a_theorem(implies(X2472,implies(not(X2471),X2471)))
| is_a_theorem(implies(X2473,implies(X2472,X2471))) ),
inference(resolution,[status(thm)],[c1203,condensed_detachment]) ).
cnf(c2138,plain,
is_a_theorem(implies(implies(not(X5038),X5039),implies(X5040,implies(implies(X5039,X5038),X5038)))),
inference(resolution,[status(thm)],[c1203,c116]) ).
cnf(c42,plain,
is_a_theorem(implies(X152,implies(implies(not(not(X152)),not(X152)),X151))),
inference(resolution,[status(thm)],[c21,c14]) ).
cnf(c171,plain,
is_a_theorem(implies(implies(implies(implies(not(not(X2439)),not(X2439)),X2440),X2438),implies(X2439,X2438))),
inference(resolution,[status(thm)],[c42,c4]) ).
cnf(c29,plain,
is_a_theorem(implies(implies(not(implies(X278,X277)),implies(X278,X277)),implies(implies(X277,X279),implies(X278,X279)))),
inference(resolution,[status(thm)],[c18,cn_1]) ).
cnf(c348,plain,
( ~ is_a_theorem(implies(not(implies(X4497,X4498)),implies(X4497,X4498)))
| is_a_theorem(implies(implies(X4498,X4496),implies(X4497,X4496))) ),
inference(resolution,[status(thm)],[c29,condensed_detachment]) ).
cnf(c6931,plain,
is_a_theorem(implies(X5056,implies(X5055,implies(implies(X5057,X5056),X5056)))),
inference(resolution,[status(thm)],[c2138,c21]) ).
cnf(c6970,plain,
is_a_theorem(implies(X5060,implies(X5059,implies(implies(X5058,X5059),X5059)))),
inference(resolution,[status(thm)],[c6931,c2135]) ).
cnf(c7022,plain,
is_a_theorem(implies(implies(implies(implies(X5283,X5285),X5285),X5284),implies(X5285,X5284))),
inference(resolution,[status(thm)],[c6970,c348]) ).
cnf(c8007,plain,
( ~ is_a_theorem(implies(implies(implies(X5413,X5414),X5414),X5415))
| is_a_theorem(implies(X5414,X5415)) ),
inference(resolution,[status(thm)],[c7022,condensed_detachment]) ).
cnf(c8114,plain,
is_a_theorem(implies(X5420,implies(X5419,X5420))),
inference(resolution,[status(thm)],[c8007,c171]) ).
cnf(c8272,plain,
is_a_theorem(implies(implies(implies(X5788,X5789),X5787),implies(X5789,X5787))),
inference(resolution,[status(thm)],[c8114,c4]) ).
cnf(c9274,plain,
( ~ is_a_theorem(implies(implies(X5923,X5924),X5925))
| is_a_theorem(implies(X5924,X5925)) ),
inference(resolution,[status(thm)],[c8272,condensed_detachment]) ).
cnf(c9854,plain,
is_a_theorem(implies(X6220,implies(X6222,implies(implies(X6220,X6221),X6221)))),
inference(resolution,[status(thm)],[c9274,c2138]) ).
cnf(c10887,plain,
is_a_theorem(implies(X6337,implies(X6336,implies(implies(X6336,X6335),X6335)))),
inference(resolution,[status(thm)],[c9854,c2135]) ).
cnf(c11420,plain,
is_a_theorem(implies(X6339,implies(implies(X6339,X6338),X6338))),
inference(resolution,[status(thm)],[c10887,c0]) ).
cnf(c11466,plain,
( ~ is_a_theorem(X6356)
| is_a_theorem(implies(implies(X6356,X6355),X6355)) ),
inference(resolution,[status(thm)],[c11420,condensed_detachment]) ).
cnf(c11631,plain,
is_a_theorem(implies(implies(implies(implies(not(X7977),X7977),X7977),X7976),X7976)),
inference(resolution,[status(thm)],[c11466,cn_2]) ).
cnf(c15941,plain,
is_a_theorem(implies(implies(X9136,implies(not(X9135),X9135)),implies(X9136,X9135))),
inference(resolution,[status(thm)],[c11631,c116]) ).
cnf(c20719,plain,
is_a_theorem(implies(implies(not(X10036),X10037),implies(implies(X10037,X10036),X10036))),
inference(resolution,[status(thm)],[c15941,c116]) ).
cnf(c23453,plain,
( ~ is_a_theorem(implies(not(X10731),X10732))
| is_a_theorem(implies(implies(X10732,X10731),X10731)) ),
inference(resolution,[status(thm)],[c20719,condensed_detachment]) ).
cnf(c11449,plain,
is_a_theorem(implies(implies(implies(implies(X13150,X13149),X13149),X13148),implies(X13150,X13148))),
inference(resolution,[status(thm)],[c10887,c348]) ).
cnf(c30212,plain,
( ~ is_a_theorem(implies(implies(implies(X16641,X16640),X16640),X16639))
| is_a_theorem(implies(X16641,X16639)) ),
inference(resolution,[status(thm)],[c11449,condensed_detachment]) ).
cnf(c40073,plain,
is_a_theorem(implies(not(X16675),implies(X16675,X16676))),
inference(resolution,[status(thm)],[c30212,c15]) ).
cnf(c40600,plain,
is_a_theorem(implies(implies(implies(X16762,X16761),X16762),X16762)),
inference(resolution,[status(thm)],[c40073,c23453]) ).
cnf(c41057,plain,
is_a_theorem(implies(implies(X17800,implies(X17800,X17799)),implies(X17800,X17799))),
inference(resolution,[status(thm)],[c40600,c116]) ).
cnf(c50285,plain,
$false,
inference(resolution,[status(thm)],[c41057,prove_cn_30]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL053-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.03 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.08/0.35 % Computer : n009.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Sat Sep 5 01:59:51 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.13/0.38 /export/starexec/sandbox/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.13/0.38 (re.compile("\."), Token.FullStop),
% 0.13/0.38 /export/starexec/sandbox/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.13/0.38 (re.compile("\("), Token.OpenPar),
% 0.13/0.38 /export/starexec/sandbox/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.13/0.38 (re.compile("\)"), Token.ClosePar),
% 0.13/0.38 /export/starexec/sandbox/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.13/0.38 (re.compile("\["), Token.OpenSquare),
% 0.13/0.38 /export/starexec/sandbox/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.13/0.38 (re.compile("\]"), Token.CloseSquare),
% 0.13/0.38 /export/starexec/sandbox/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.13/0.38 (re.compile("~\|"), Token.Nor),
% 0.13/0.38 /export/starexec/sandbox/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.13/0.38 (re.compile("\|"), Token.Or),
% 0.13/0.38 /export/starexec/sandbox/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.13/0.39 (re.compile("\?"), Token.Existential),
% 0.13/0.39 /export/starexec/sandbox/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.13/0.39 (re.compile("\s+"), Token.WhiteSpace),
% 0.13/0.39 /export/starexec/sandbox/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.13/0.39 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.13/0.42 /export/starexec/sandbox/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.13/0.42 """
% 0.13/0.42 /export/starexec/sandbox/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.13/0.42 """
% 0.13/0.46 /export/starexec/sandbox/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.13/0.46 """
% 27.55/27.85 % Version: 1.5
% 27.55/27.85 % SZS status Unsatisfiable
% 27.55/27.85 % SZS output start CNFRefutation
% See solution above
% 27.55/27.85
% 27.55/27.85 % Initial clauses : 5
% 27.55/27.85 % Processed clauses : 984
% 27.55/27.85 % Factors computed : 0
% 27.55/27.85 % Resolvents computed: 50321
% 27.55/27.85 % Tautologies deleted: 1
% 27.55/27.85 % Forward subsumed : 4572
% 27.55/27.85 % Backward subsumed : 157
% 27.55/27.86 % -------- CPU Time ---------
% 27.55/27.86 % User time : 27.416 s
% 27.55/27.86 % System time : 0.072 s
% 27.55/27.86 % Total time : 27.488 s
%------------------------------------------------------------------------------