%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : LCL069-1 : TPTP v9.3.1. Bugfixed v1.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n003.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:47 PM UTC 2026
% Result : Unsatisfiable 36.66s 37.02s
% Output : CNFRefutation 36.66s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 5
% Syntax : Number of clauses : 37 ( 25 unt; 0 nHn; 10 RR)
% Number of literals : 50 ( 0 equ; 14 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 : 101 ( 27 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(prove_cn_3,negated_conjecture,
~ is_a_theorem(implies(a,implies(not(a),b))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_cn_3) ).
cnf(condensed_detachment,axiom,
( ~ is_a_theorem(implies(X3,X2))
| ~ is_a_theorem(X3)
| is_a_theorem(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',condensed_detachment) ).
cnf(cn_19,axiom,
is_a_theorem(implies(implies(implies(X5,X4),X6),implies(X4,X6))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cn_19) ).
cnf(c0,plain,
( ~ is_a_theorem(implies(implies(X8,X9),X7))
| is_a_theorem(implies(X9,X7)) ),
inference(resolution,[status(thm)],[cn_19,condensed_detachment]) ).
cnf(c1,plain,
is_a_theorem(implies(X10,implies(X11,X10))),
inference(resolution,[status(thm)],[c0,cn_19]) ).
cnf(cn_37,axiom,
is_a_theorem(implies(implies(implies(X13,X12),X14),implies(not(X13),X14))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cn_37) ).
cnf(c4,plain,
( ~ is_a_theorem(implies(implies(X51,X49),X50))
| is_a_theorem(implies(not(X51),X50)) ),
inference(resolution,[status(thm)],[cn_37,condensed_detachment]) ).
cnf(c38,plain,
is_a_theorem(implies(not(X57),implies(X56,implies(X57,X55)))),
inference(resolution,[status(thm)],[c4,c1]) ).
cnf(cn_59,axiom,
is_a_theorem(implies(implies(not(X29),X30),implies(implies(X28,X30),implies(implies(X29,X28),X30)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cn_59) ).
cnf(c21,plain,
( ~ is_a_theorem(implies(not(X251),X249))
| is_a_theorem(implies(implies(X250,X249),implies(implies(X251,X250),X249))) ),
inference(resolution,[status(thm)],[cn_59,condensed_detachment]) ).
cnf(c42,plain,
is_a_theorem(implies(not(implies(X59,X60)),implies(X60,X58))),
inference(resolution,[status(thm)],[c4,cn_19]) ).
cnf(c184,plain,
is_a_theorem(implies(implies(X824,implies(X821,X823)),implies(implies(implies(X822,X821),X824),implies(X821,X823)))),
inference(resolution,[status(thm)],[c21,c42]) ).
cnf(c453,plain,
( ~ is_a_theorem(implies(X1013,implies(X1011,X1014)))
| is_a_theorem(implies(implies(implies(X1012,X1011),X1013),implies(X1011,X1014))) ),
inference(resolution,[status(thm)],[c184,condensed_detachment]) ).
cnf(c559,plain,
is_a_theorem(implies(implies(implies(X1093,X1095),not(X1094)),implies(X1095,implies(X1094,X1096)))),
inference(resolution,[status(thm)],[c453,c38]) ).
cnf(c558,plain,
is_a_theorem(implies(implies(implies(X1186,X1188),implies(implies(X1187,X1188),X1185)),implies(X1188,X1185))),
inference(resolution,[status(thm)],[c453,cn_19]) ).
cnf(c740,plain,
( ~ is_a_theorem(implies(implies(X1386,X1385),implies(implies(X1387,X1385),X1384)))
| is_a_theorem(implies(X1385,X1384)) ),
inference(resolution,[status(thm)],[c558,condensed_detachment]) ).
cnf(c890,plain,
is_a_theorem(implies(not(X1430),implies(X1430,X1431))),
inference(resolution,[status(thm)],[c740,c559]) ).
cnf(c982,plain,
is_a_theorem(implies(implies(X2957,implies(X2956,X2955)),implies(implies(X2956,X2957),implies(X2956,X2955)))),
inference(resolution,[status(thm)],[c890,c21]) ).
cnf(c1960,plain,
( ~ is_a_theorem(implies(X3247,implies(X3245,X3246)))
| is_a_theorem(implies(implies(X3245,X3247),implies(X3245,X3246))) ),
inference(resolution,[status(thm)],[c982,condensed_detachment]) ).
cnf(c2076,plain,
is_a_theorem(implies(implies(X3498,not(X3497)),implies(X3498,implies(X3497,X3499)))),
inference(resolution,[status(thm)],[c1960,c38]) ).
cnf(c2614,plain,
( ~ is_a_theorem(implies(X3629,not(X3630)))
| is_a_theorem(implies(X3629,implies(X3630,X3628))) ),
inference(resolution,[status(thm)],[c2076,condensed_detachment]) ).
cnf(c923,plain,
is_a_theorem(implies(X1388,X1388)),
inference(resolution,[status(thm)],[c740,cn_19]) ).
cnf(c2075,plain,
is_a_theorem(implies(implies(X3263,implies(X3263,X3262)),implies(X3263,X3262))),
inference(resolution,[status(thm)],[c1960,c923]) ).
cnf(c3,plain,
is_a_theorem(implies(X21,implies(X19,implies(X20,X21)))),
inference(resolution,[status(thm)],[c1,c0]) ).
cnf(c2171,plain,
is_a_theorem(implies(implies(X3285,X3283),implies(X3285,implies(X3284,X3283)))),
inference(resolution,[status(thm)],[c1960,c3]) ).
cnf(c2229,plain,
( ~ is_a_theorem(implies(X3391,X3389))
| is_a_theorem(implies(X3391,implies(X3390,X3389))) ),
inference(resolution,[status(thm)],[c2171,condensed_detachment]) ).
cnf(c2547,plain,
is_a_theorem(implies(implies(X3906,implies(X3906,X3905)),implies(X3907,implies(X3906,X3905)))),
inference(resolution,[status(thm)],[c2229,c2075]) ).
cnf(c2879,plain,
is_a_theorem(implies(implies(X9793,implies(X9792,implies(X9792,X9794))),implies(X9793,implies(X9792,X9794)))),
inference(resolution,[status(thm)],[c2547,c1960]) ).
cnf(c7985,plain,
( ~ is_a_theorem(implies(X18301,implies(X18300,implies(X18300,X18302))))
| is_a_theorem(implies(X18301,implies(X18300,X18302))) ),
inference(resolution,[status(thm)],[c2879,condensed_detachment]) ).
cnf(c167,plain,
is_a_theorem(implies(implies(X1997,implies(X1995,implies(X1996,not(X1994)))),implies(implies(X1994,X1997),implies(X1995,implies(X1996,not(X1994)))))),
inference(resolution,[status(thm)],[c21,c3]) ).
cnf(c1299,plain,
( ~ is_a_theorem(implies(X23304,implies(X23302,implies(X23303,not(X23301)))))
| is_a_theorem(implies(implies(X23301,X23304),implies(X23302,implies(X23303,not(X23301))))) ),
inference(resolution,[status(thm)],[c167,condensed_detachment]) ).
cnf(c19943,plain,
is_a_theorem(implies(implies(X23508,not(X23509)),implies(X23510,implies(X23509,not(X23508))))),
inference(resolution,[status(thm)],[c1299,c38]) ).
cnf(c20221,plain,
is_a_theorem(implies(implies(X23527,not(X23528)),implies(X23528,not(X23527)))),
inference(resolution,[status(thm)],[c19943,c7985]) ).
cnf(c20288,plain,
( ~ is_a_theorem(implies(X23558,not(X23557)))
| is_a_theorem(implies(X23557,not(X23558))) ),
inference(resolution,[status(thm)],[c20221,condensed_detachment]) ).
cnf(c20401,plain,
is_a_theorem(implies(X23559,not(not(X23559)))),
inference(resolution,[status(thm)],[c20288,c923]) ).
cnf(c20439,plain,
is_a_theorem(implies(X23570,implies(not(X23570),X23569))),
inference(resolution,[status(thm)],[c20401,c2614]) ).
cnf(c21016,plain,
$false,
inference(resolution,[status(thm)],[c20439,prove_cn_3]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL069-1 : TPTP v9.3.1. Bugfixed v1.2.0.
% 0.00/0.03 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.09/0.34 % Computer : n003.cluster.edu
% 0.09/0.34 % Model : x86_64 x86_64
% 0.09/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.34 % Memory : 8046.5625MB
% 0.09/0.34 % OS : Linux 6.8.0-71-generic
% 0.09/0.34 % CPULimit : 300
% 0.09/0.34 % WCLimit : 300
% 0.09/0.34 % DateTime : Sat Sep 5 03:56:05 UTC 2026
% 0.09/0.34 % CPUTime :
% 0.12/0.40 /export/starexec/sandbox/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.12/0.40 (re.compile("\."), Token.FullStop),
% 0.12/0.40 /export/starexec/sandbox/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.12/0.40 (re.compile("\("), Token.OpenPar),
% 0.12/0.40 /export/starexec/sandbox/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.12/0.40 (re.compile("\)"), Token.ClosePar),
% 0.12/0.40 /export/starexec/sandbox/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.12/0.40 (re.compile("\["), Token.OpenSquare),
% 0.12/0.40 /export/starexec/sandbox/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.12/0.40 (re.compile("\]"), Token.CloseSquare),
% 0.12/0.40 /export/starexec/sandbox/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.12/0.40 (re.compile("~\|"), Token.Nor),
% 0.12/0.40 /export/starexec/sandbox/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.12/0.40 (re.compile("\|"), Token.Or),
% 0.12/0.40 /export/starexec/sandbox/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.12/0.40 (re.compile("\?"), Token.Existential),
% 0.12/0.40 /export/starexec/sandbox/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.12/0.40 (re.compile("\s+"), Token.WhiteSpace),
% 0.12/0.40 /export/starexec/sandbox/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.12/0.40 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.23/0.47 /export/starexec/sandbox/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.23/0.47 """
% 0.23/0.47 /export/starexec/sandbox/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.23/0.47 """
% 0.33/0.56 /export/starexec/sandbox/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.33/0.56 """
% 36.66/37.02 % Version: 1.5
% 36.66/37.02 % SZS status Unsatisfiable
% 36.66/37.02 % SZS output start CNFRefutation
% See solution above
% 36.66/37.02
% 36.66/37.02 % Initial clauses : 5
% 36.66/37.02 % Processed clauses : 607
% 36.66/37.02 % Factors computed : 0
% 36.66/37.02 % Resolvents computed: 21027
% 36.66/37.02 % Tautologies deleted: 1
% 36.66/37.02 % Forward subsumed : 4795
% 36.66/37.02 % Backward subsumed : 0
% 36.66/37.02 % -------- CPU Time ---------
% 36.66/37.02 % User time : 36.598 s
% 36.66/37.02 % System time : 0.078 s
% 36.66/37.02 % Total time : 36.676 s
%------------------------------------------------------------------------------