%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : LCL057-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n002.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:46 PM UTC 2026
% Result : Unsatisfiable 51.04s 51.36s
% Output : CNFRefutation 51.04s
% Verified :
% SZS Type : Refutation
% Derivation depth : 38
% Number of leaves : 5
% Syntax : Number of clauses : 71 ( 50 unt; 0 nHn; 14 RR)
% Number of literals : 93 ( 0 equ; 23 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 : 3 ( 3 usr; 1 con; 0-2 aty)
% Number of variables : 182 ( 54 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(prove_cn_40,negated_conjecture,
~ is_a_theorem(implies(a,not(not(a)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_cn_40) ).
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_3,axiom,
is_a_theorem(implies(X4,implies(not(X4),X3))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cn_3) ).
cnf(cn_1,axiom,
is_a_theorem(implies(implies(X11,X10),implies(implies(X10,X12),implies(X11,X12)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cn_1) ).
cnf(c5,plain,
( ~ is_a_theorem(implies(X32,X31))
| is_a_theorem(implies(implies(X31,X30),implies(X32,X30))) ),
inference(resolution,[status(thm)],[cn_1,condensed_detachment]) ).
cnf(c19,plain,
is_a_theorem(implies(implies(implies(not(X36),X37),X35),implies(X36,X35))),
inference(resolution,[status(thm)],[c5,cn_3]) ).
cnf(c24,plain,
( ~ is_a_theorem(implies(implies(not(X63),X61),X62))
| is_a_theorem(implies(X63,X62)) ),
inference(resolution,[status(thm)],[c19,condensed_detachment]) ).
cnf(c16,plain,
is_a_theorem(implies(implies(implies(implies(X113,X112),implies(X114,X112)),X115),implies(implies(X114,X113),X115))),
inference(resolution,[status(thm)],[c5,cn_1]) ).
cnf(c103,plain,
( ~ is_a_theorem(implies(implies(implies(X1246,X1247),implies(X1248,X1247)),X1245))
| is_a_theorem(implies(implies(X1248,X1246),X1245)) ),
inference(resolution,[status(thm)],[c16,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(c0,plain,
( ~ is_a_theorem(implies(not(X7),X7))
| is_a_theorem(X7) ),
inference(resolution,[status(thm)],[condensed_detachment,cn_2]) ).
cnf(c26,plain,
is_a_theorem(implies(implies(implies(X241,X240),X242),implies(implies(implies(not(X241),X239),X240),X242))),
inference(resolution,[status(thm)],[c19,c5]) ).
cnf(c15,plain,
is_a_theorem(implies(implies(X33,X34),implies(implies(not(X33),X33),X34))),
inference(resolution,[status(thm)],[c5,cn_2]) ).
cnf(c1,plain,
( ~ is_a_theorem(X8)
| is_a_theorem(implies(not(X8),X9)) ),
inference(resolution,[status(thm)],[condensed_detachment,cn_3]) ).
cnf(c54,plain,
is_a_theorem(implies(X64,X64)),
inference(resolution,[status(thm)],[c24,cn_2]) ).
cnf(c60,plain,
is_a_theorem(implies(not(implies(X73,X73)),X74)),
inference(resolution,[status(thm)],[c54,c1]) ).
cnf(c74,plain,
is_a_theorem(implies(implies(X119,X121),implies(not(implies(X120,X120)),X121))),
inference(resolution,[status(thm)],[c60,c5]) ).
cnf(c117,plain,
is_a_theorem(implies(X122,implies(not(implies(X124,X124)),X123))),
inference(resolution,[status(thm)],[c74,c24]) ).
cnf(c126,plain,
is_a_theorem(implies(implies(implies(not(implies(X216,X216)),X215),X214),implies(X213,X214))),
inference(resolution,[status(thm)],[c117,c5]) ).
cnf(c243,plain,
( ~ is_a_theorem(implies(implies(not(implies(X217,X217)),X220),X219))
| is_a_theorem(implies(X218,X219)) ),
inference(resolution,[status(thm)],[c126,condensed_detachment]) ).
cnf(c252,plain,
is_a_theorem(implies(X221,implies(X222,X222))),
inference(resolution,[status(thm)],[c243,cn_2]) ).
cnf(c271,plain,
is_a_theorem(implies(implies(implies(X267,X267),X266),implies(X265,X266))),
inference(resolution,[status(thm)],[c252,c5]) ).
cnf(c302,plain,
( ~ is_a_theorem(implies(implies(X269,X269),X270))
| is_a_theorem(implies(X268,X270)) ),
inference(resolution,[status(thm)],[c271,condensed_detachment]) ).
cnf(c312,plain,
is_a_theorem(implies(X304,implies(implies(not(X303),X303),X303))),
inference(resolution,[status(thm)],[c302,c15]) ).
cnf(c357,plain,
is_a_theorem(implies(implies(implies(implies(not(X837),X837),X837),X838),implies(X836,X838))),
inference(resolution,[status(thm)],[c312,c5]) ).
cnf(c746,plain,
( ~ is_a_theorem(implies(implies(implies(not(X1056),X1056),X1056),X1057))
| is_a_theorem(implies(X1055,X1057)) ),
inference(resolution,[status(thm)],[c357,condensed_detachment]) ).
cnf(c875,plain,
is_a_theorem(implies(X1140,implies(implies(implies(not(not(X1139)),X1141),X1139),X1139))),
inference(resolution,[status(thm)],[c746,c26]) ).
cnf(c949,plain,
is_a_theorem(implies(implies(implies(not(not(X1143)),X1142),X1143),X1143)),
inference(resolution,[status(thm)],[c875,c0]) ).
cnf(c960,plain,
( ~ is_a_theorem(implies(implies(not(not(X1152)),X1151),X1152))
| is_a_theorem(X1152) ),
inference(resolution,[status(thm)],[c949,condensed_detachment]) ).
cnf(c318,plain,
is_a_theorem(implies(X280,implies(X279,implies(X281,X281)))),
inference(resolution,[status(thm)],[c302,c271]) ).
cnf(c335,plain,
is_a_theorem(implies(implies(implies(X425,implies(X424,X424)),X426),implies(X423,X426))),
inference(resolution,[status(thm)],[c318,c5]) ).
cnf(c463,plain,
( ~ is_a_theorem(implies(implies(X472,implies(X474,X474)),X471))
| is_a_theorem(implies(X473,X471)) ),
inference(resolution,[status(thm)],[c335,condensed_detachment]) ).
cnf(c1005,plain,
is_a_theorem(implies(implies(X1975,implies(not(X1974),X1974)),implies(X1973,implies(X1975,X1974)))),
inference(resolution,[status(thm)],[c103,c357]) ).
cnf(c1982,plain,
is_a_theorem(implies(implies(not(X2285),X2286),implies(X2284,implies(implies(X2286,X2285),X2285)))),
inference(resolution,[status(thm)],[c1005,c103]) ).
cnf(c2320,plain,
is_a_theorem(implies(X2301,implies(X2304,implies(implies(implies(X2303,X2303),X2302),X2302)))),
inference(resolution,[status(thm)],[c1982,c463]) ).
cnf(c2505,plain,
is_a_theorem(implies(X2307,implies(implies(implies(X2305,X2305),X2306),X2306))),
inference(resolution,[status(thm)],[c2320,c960]) ).
cnf(c2526,plain,
is_a_theorem(implies(implies(implies(X2311,X2311),X2312),X2312)),
inference(resolution,[status(thm)],[c2505,c960]) ).
cnf(c2566,plain,
( ~ is_a_theorem(implies(implies(X2326,X2326),X2325))
| is_a_theorem(X2325) ),
inference(resolution,[status(thm)],[c2526,condensed_detachment]) ).
cnf(c1983,plain,
( ~ is_a_theorem(implies(X3343,implies(not(X3345),X3345)))
| is_a_theorem(implies(X3344,implies(X3343,X3345))) ),
inference(resolution,[status(thm)],[c1005,condensed_detachment]) ).
cnf(c4049,plain,
is_a_theorem(implies(X3582,implies(implies(implies(X3583,implies(X3585,X3585)),X3584),X3584))),
inference(resolution,[status(thm)],[c1983,c335]) ).
cnf(c4745,plain,
is_a_theorem(implies(implies(implies(X3598,implies(X3597,X3597)),X3596),X3596)),
inference(resolution,[status(thm)],[c4049,c2566]) ).
cnf(c4816,plain,
( ~ is_a_theorem(implies(implies(X3636,implies(X3634,X3634)),X3635))
| is_a_theorem(X3635) ),
inference(resolution,[status(thm)],[c4745,condensed_detachment]) ).
cnf(c2324,plain,
is_a_theorem(implies(X2292,implies(X2294,implies(implies(X2293,X2292),X2292)))),
inference(resolution,[status(thm)],[c1982,c24]) ).
cnf(c3959,plain,
is_a_theorem(implies(X3374,implies(X3376,implies(implies(X3375,X3376),X3376)))),
inference(resolution,[status(thm)],[c1983,c2324]) ).
cnf(c4108,plain,
is_a_theorem(implies(X3378,implies(implies(X3377,X3378),X3378))),
inference(resolution,[status(thm)],[c3959,c2566]) ).
cnf(c4136,plain,
is_a_theorem(implies(implies(implies(implies(X4339,X4338),X4338),X4340),implies(X4338,X4340))),
inference(resolution,[status(thm)],[c4108,c5]) ).
cnf(c6010,plain,
is_a_theorem(implies(implies(X4548,implies(X4550,X4549)),implies(X4549,implies(X4548,X4549)))),
inference(resolution,[status(thm)],[c4136,c103]) ).
cnf(c6212,plain,
is_a_theorem(implies(X4552,implies(X4551,X4552))),
inference(resolution,[status(thm)],[c6010,c4816]) ).
cnf(c6219,plain,
is_a_theorem(implies(implies(implies(X4877,X4876),X4878),implies(X4876,X4878))),
inference(resolution,[status(thm)],[c6212,c5]) ).
cnf(c7087,plain,
( ~ is_a_theorem(implies(implies(X4995,X4996),X4997))
| is_a_theorem(implies(X4996,X4997)) ),
inference(resolution,[status(thm)],[c6219,condensed_detachment]) ).
cnf(c7463,plain,
is_a_theorem(implies(X5360,implies(X5359,implies(implies(X5360,X5358),X5358)))),
inference(resolution,[status(thm)],[c7087,c1982]) ).
cnf(c8748,plain,
is_a_theorem(implies(X5464,implies(X5465,implies(implies(X5465,X5466),X5466)))),
inference(resolution,[status(thm)],[c7463,c1983]) ).
cnf(c9187,plain,
is_a_theorem(implies(X5468,implies(implies(X5468,X5467),X5467))),
inference(resolution,[status(thm)],[c8748,c2566]) ).
cnf(c9244,plain,
( ~ is_a_theorem(X5493)
| is_a_theorem(implies(implies(X5493,X5494),X5494)) ),
inference(resolution,[status(thm)],[c9187,condensed_detachment]) ).
cnf(c9444,plain,
is_a_theorem(implies(implies(implies(implies(not(X7154),X7154),X7154),X7153),X7153)),
inference(resolution,[status(thm)],[c9244,cn_2]) ).
cnf(c13953,plain,
is_a_theorem(implies(implies(X8135,implies(not(X8136),X8136)),implies(X8135,X8136))),
inference(resolution,[status(thm)],[c9444,c103]) ).
cnf(c17022,plain,
is_a_theorem(implies(implies(not(X8662),X8663),implies(implies(X8663,X8662),X8662))),
inference(resolution,[status(thm)],[c13953,c103]) ).
cnf(c18301,plain,
( ~ is_a_theorem(implies(not(X9322),X9323))
| is_a_theorem(implies(implies(X9323,X9322),X9322)) ),
inference(resolution,[status(thm)],[c17022,condensed_detachment]) ).
cnf(c17024,plain,
( ~ is_a_theorem(implies(X8697,implies(not(X8696),X8696)))
| is_a_theorem(implies(X8697,X8696)) ),
inference(resolution,[status(thm)],[c13953,condensed_detachment]) ).
cnf(c9396,plain,
is_a_theorem(implies(implies(implies(X7128,implies(not(X7128),X7129)),X7127),X7127)),
inference(resolution,[status(thm)],[c9244,cn_3]) ).
cnf(c13893,plain,
( ~ is_a_theorem(implies(implies(X7945,implies(not(X7945),X7947)),X7946))
| is_a_theorem(X7946) ),
inference(resolution,[status(thm)],[c9396,condensed_detachment]) ).
cnf(c21,plain,
( ~ is_a_theorem(implies(X44,X43))
| is_a_theorem(implies(implies(not(X44),X44),X43)) ),
inference(resolution,[status(thm)],[c15,condensed_detachment]) ).
cnf(c32,plain,
is_a_theorem(implies(implies(not(implies(X321,X320)),implies(X321,X320)),implies(implies(X320,X319),implies(X321,X319)))),
inference(resolution,[status(thm)],[c21,cn_1]) ).
cnf(c391,plain,
( ~ is_a_theorem(implies(not(implies(X4896,X4894)),implies(X4896,X4894)))
| is_a_theorem(implies(implies(X4894,X4895),implies(X4896,X4895))) ),
inference(resolution,[status(thm)],[c32,condensed_detachment]) ).
cnf(c9214,plain,
is_a_theorem(implies(implies(implies(implies(X12248,X12249),X12249),X12250),implies(X12248,X12250))),
inference(resolution,[status(thm)],[c8748,c391]) ).
cnf(c26914,plain,
is_a_theorem(implies(implies(X15448,implies(X15449,X15450)),implies(X15449,implies(X15448,X15450)))),
inference(resolution,[status(thm)],[c9214,c103]) ).
cnf(c37343,plain,
is_a_theorem(implies(not(X15456),implies(X15456,X15455))),
inference(resolution,[status(thm)],[c26914,c13893]) ).
cnf(c37402,plain,
is_a_theorem(implies(not(not(X15464)),X15464)),
inference(resolution,[status(thm)],[c37343,c17024]) ).
cnf(c37517,plain,
is_a_theorem(implies(implies(X15668,not(X15668)),not(X15668))),
inference(resolution,[status(thm)],[c37402,c18301]) ).
cnf(c38382,plain,
is_a_theorem(implies(X15670,not(not(X15670)))),
inference(resolution,[status(thm)],[c37517,c24]) ).
cnf(c38419,plain,
$false,
inference(resolution,[status(thm)],[c38382,prove_cn_40]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL057-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.08/0.35 % Computer : n002.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 20:20:36 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.11/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.11/0.41 (re.compile("\."), Token.FullStop),
% 0.11/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.11/0.41 (re.compile("\("), Token.OpenPar),
% 0.11/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.11/0.41 (re.compile("\)"), Token.ClosePar),
% 0.11/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.11/0.41 (re.compile("\["), Token.OpenSquare),
% 0.11/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.11/0.41 (re.compile("\]"), Token.CloseSquare),
% 0.11/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.11/0.41 (re.compile("~\|"), Token.Nor),
% 0.11/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.11/0.41 (re.compile("\|"), Token.Or),
% 0.11/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.11/0.41 (re.compile("\?"), Token.Existential),
% 0.11/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.11/0.41 (re.compile("\s+"), Token.WhiteSpace),
% 0.11/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.11/0.41 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.20/0.48 /export/starexec/sandbox2/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.20/0.48 """
% 0.20/0.48 /export/starexec/sandbox2/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.20/0.48 """
% 0.30/0.57 /export/starexec/sandbox2/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.30/0.57 """
% 51.04/51.36 % Version: 1.5
% 51.04/51.36 % SZS status Unsatisfiable
% 51.04/51.36 % SZS output start CNFRefutation
% See solution above
% 51.04/51.36
% 51.04/51.36 % Initial clauses : 5
% 51.04/51.36 % Processed clauses : 863
% 51.04/51.36 % Factors computed : 0
% 51.04/51.36 % Resolvents computed: 38468
% 51.04/51.36 % Tautologies deleted: 1
% 51.04/51.36 % Forward subsumed : 3988
% 51.04/51.36 % Backward subsumed : 134
% 51.04/51.36 % -------- CPU Time ---------
% 51.04/51.36 % User time : 50.879 s
% 51.04/51.36 % System time : 0.125 s
% 51.04/51.36 % Total time : 51.004 s
%------------------------------------------------------------------------------