%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : LCL039-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n005.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:44 PM UTC 2026
% Result : Unsatisfiable 40.76s 41.07s
% Output : CNFRefutation 40.76s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 8
% Syntax : Number of clauses : 42 ( 29 unt; 0 nHn; 14 RR)
% Number of literals : 56 ( 0 equ; 15 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; 1 con; 0-2 aty)
% Number of variables : 80 ( 14 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(prove_this,negated_conjecture,
~ is_a_theorem(implies(necessary(a),not(necessary(not(a))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this) ).
cnf(condensed_detachment,axiom,
( ~ is_a_theorem(implies(X9,X10))
| ~ is_a_theorem(X9)
| is_a_theorem(X10) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',condensed_detachment) ).
cnf(necessitation2,axiom,
is_a_theorem(implies(necessary(X2),X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',necessitation2) ).
cnf(cn_18,axiom,
is_a_theorem(implies(X4,implies(X5,X4))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cn_18) ).
cnf(c5,plain,
( ~ is_a_theorem(X14)
| is_a_theorem(implies(X13,X14)) ),
inference(resolution,[status(thm)],[condensed_detachment,cn_18]) ).
cnf(c8,plain,
is_a_theorem(implies(X17,implies(necessary(X18),X18))),
inference(resolution,[status(thm)],[c5,necessitation2]) ).
cnf(cn_35,axiom,
is_a_theorem(implies(implies(X20,implies(X21,X19)),implies(implies(X20,X21),implies(X20,X19)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cn_35) ).
cnf(c15,plain,
( ~ is_a_theorem(implies(X71,implies(X70,X72)))
| is_a_theorem(implies(implies(X71,X70),implies(X71,X72))) ),
inference(resolution,[status(thm)],[cn_35,condensed_detachment]) ).
cnf(c55,plain,
is_a_theorem(implies(implies(X145,necessary(X146)),implies(X145,X146))),
inference(resolution,[status(thm)],[c15,c8]) ).
cnf(c133,plain,
( ~ is_a_theorem(implies(X170,necessary(X171)))
| is_a_theorem(implies(X170,X171)) ),
inference(resolution,[status(thm)],[c55,condensed_detachment]) ).
cnf(necessitation1,axiom,
is_a_theorem(implies(necessary(implies(X44,X45)),implies(necessary(X44),necessary(X45)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',necessitation1) ).
cnf(c36,plain,
( ~ is_a_theorem(necessary(implies(X214,X215)))
| is_a_theorem(implies(necessary(X214),necessary(X215))) ),
inference(resolution,[status(thm)],[necessitation1,condensed_detachment]) ).
cnf(axiom_of_necessitation,axiom,
( ~ is_a_theorem(X3)
| is_a_theorem(necessary(X3)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_of_necessitation) ).
cnf(cn_49,axiom,
is_a_theorem(implies(implies(not(X32),not(X33)),implies(X33,X32))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cn_49) ).
cnf(c24,plain,
( ~ is_a_theorem(implies(not(X111),not(X112)))
| is_a_theorem(implies(X112,X111)) ),
inference(resolution,[status(thm)],[cn_49,condensed_detachment]) ).
cnf(c0,plain,
is_a_theorem(necessary(implies(necessary(X6),X6))),
inference(resolution,[status(thm)],[axiom_of_necessitation,necessitation2]) ).
cnf(c9,plain,
is_a_theorem(implies(X38,necessary(implies(necessary(X39),X39)))),
inference(resolution,[status(thm)],[c5,c0]) ).
cnf(c57,plain,
is_a_theorem(implies(implies(X74,X73),implies(X74,X74))),
inference(resolution,[status(thm)],[c15,cn_18]) ).
cnf(c62,plain,
( ~ is_a_theorem(implies(X75,X76))
| is_a_theorem(implies(X75,X75)) ),
inference(resolution,[status(thm)],[c57,condensed_detachment]) ).
cnf(c67,plain,
is_a_theorem(implies(X77,X77)),
inference(resolution,[status(thm)],[c62,c9]) ).
cnf(c81,plain,
is_a_theorem(implies(X94,implies(X95,X95))),
inference(resolution,[status(thm)],[c67,c5]) ).
cnf(c58,plain,
is_a_theorem(implies(implies(implies(X413,implies(X412,X414)),implies(X413,X412)),implies(implies(X413,implies(X412,X414)),implies(X413,X414)))),
inference(resolution,[status(thm)],[c15,cn_35]) ).
cnf(c396,plain,
( ~ is_a_theorem(implies(implies(X2246,implies(X2244,X2245)),implies(X2246,X2244)))
| is_a_theorem(implies(implies(X2246,implies(X2244,X2245)),implies(X2246,X2245))) ),
inference(resolution,[status(thm)],[c58,condensed_detachment]) ).
cnf(c2575,plain,
is_a_theorem(implies(implies(X2247,implies(X2247,X2248)),implies(X2247,X2248))),
inference(resolution,[status(thm)],[c396,c81]) ).
cnf(c2596,plain,
( ~ is_a_theorem(implies(X2250,implies(X2250,X2251)))
| is_a_theorem(implies(X2250,X2251)) ),
inference(resolution,[status(thm)],[c2575,condensed_detachment]) ).
cnf(c26,plain,
is_a_theorem(implies(X135,implies(implies(not(X134),not(X136)),implies(X136,X134)))),
inference(resolution,[status(thm)],[cn_49,c5]) ).
cnf(c127,plain,
is_a_theorem(implies(implies(X791,implies(not(X792),not(X793))),implies(X791,implies(X793,X792)))),
inference(resolution,[status(thm)],[c26,c15]) ).
cnf(c11,plain,
is_a_theorem(implies(X26,implies(X27,implies(X28,X27)))),
inference(resolution,[status(thm)],[c5,cn_18]) ).
cnf(c79,plain,
is_a_theorem(implies(implies(implies(X526,X525),X526),implies(implies(X526,X525),X525))),
inference(resolution,[status(thm)],[c67,c15]) ).
cnf(c506,plain,
( ~ is_a_theorem(implies(implies(X2739,X2738),X2739))
| is_a_theorem(implies(implies(X2739,X2738),X2738)) ),
inference(resolution,[status(thm)],[c79,condensed_detachment]) ).
cnf(c3204,plain,
is_a_theorem(implies(implies(implies(X3440,implies(X3441,X3440)),X3439),X3439)),
inference(resolution,[status(thm)],[c506,c11]) ).
cnf(c4313,plain,
( ~ is_a_theorem(implies(implies(X3676,implies(X3675,X3676)),X3674))
| is_a_theorem(X3674) ),
inference(resolution,[status(thm)],[c3204,condensed_detachment]) ).
cnf(c4548,plain,
is_a_theorem(implies(not(X3701),implies(X3701,X3702))),
inference(resolution,[status(thm)],[c4313,c127]) ).
cnf(c946,plain,
( ~ is_a_theorem(implies(X8048,implies(not(X8047),not(X8046))))
| is_a_theorem(implies(X8048,implies(X8046,X8047))) ),
inference(resolution,[status(thm)],[c127,condensed_detachment]) ).
cnf(c10238,plain,
is_a_theorem(implies(not(not(X8059)),implies(X8058,X8059))),
inference(resolution,[status(thm)],[c946,c4548]) ).
cnf(c10295,plain,
is_a_theorem(implies(not(not(X8064)),X8064)),
inference(resolution,[status(thm)],[c10238,c2596]) ).
cnf(c10319,plain,
is_a_theorem(implies(not(not(necessary(X8090))),X8090)),
inference(resolution,[status(thm)],[c10295,c133]) ).
cnf(c10937,plain,
is_a_theorem(implies(X8121,not(necessary(not(X8121))))),
inference(resolution,[status(thm)],[c10319,c24]) ).
cnf(c11041,plain,
is_a_theorem(necessary(implies(X8676,not(necessary(not(X8676)))))),
inference(resolution,[status(thm)],[c10937,axiom_of_necessitation]) ).
cnf(c14518,plain,
is_a_theorem(implies(necessary(X12435),necessary(not(necessary(not(X12435)))))),
inference(resolution,[status(thm)],[c11041,c36]) ).
cnf(c27957,plain,
is_a_theorem(implies(necessary(X12442),not(necessary(not(X12442))))),
inference(resolution,[status(thm)],[c14518,c133]) ).
cnf(c28000,plain,
$false,
inference(resolution,[status(thm)],[c27957,prove_this]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL039-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.03 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.09/0.35 % Computer : n005.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Sat Sep 5 00:13:06 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.11/0.41 /export/starexec/sandbox/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.11/0.41 (re.compile("\."), Token.FullStop),
% 0.11/0.41 /export/starexec/sandbox/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.11/0.41 (re.compile("\("), Token.OpenPar),
% 0.11/0.41 /export/starexec/sandbox/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.11/0.41 (re.compile("\)"), Token.ClosePar),
% 0.11/0.41 /export/starexec/sandbox/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.11/0.41 (re.compile("\["), Token.OpenSquare),
% 0.11/0.41 /export/starexec/sandbox/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.11/0.41 (re.compile("\]"), Token.CloseSquare),
% 0.11/0.41 /export/starexec/sandbox/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.11/0.42 (re.compile("~\|"), Token.Nor),
% 0.11/0.42 /export/starexec/sandbox/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.11/0.42 (re.compile("\|"), Token.Or),
% 0.11/0.42 /export/starexec/sandbox/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.11/0.42 (re.compile("\?"), Token.Existential),
% 0.11/0.42 /export/starexec/sandbox/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.11/0.42 (re.compile("\s+"), Token.WhiteSpace),
% 0.11/0.42 /export/starexec/sandbox/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.11/0.42 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.20/0.48 /export/starexec/sandbox/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.20/0.48 """
% 0.20/0.49 /export/starexec/sandbox/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.20/0.49 """
% 0.31/0.58 /export/starexec/sandbox/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.31/0.58 """
% 40.76/41.07 % Version: 1.5
% 40.76/41.07 % SZS status Unsatisfiable
% 40.76/41.07 % SZS output start CNFRefutation
% See solution above
% 40.76/41.07
% 40.76/41.07 % Initial clauses : 8
% 40.76/41.07 % Processed clauses : 1024
% 40.76/41.07 % Factors computed : 0
% 40.76/41.07 % Resolvents computed: 28019
% 40.76/41.07 % Tautologies deleted: 1
% 40.76/41.07 % Forward subsumed : 4112
% 40.76/41.07 % Backward subsumed : 3
% 40.76/41.07 % -------- CPU Time ---------
% 40.76/41.07 % User time : 40.622 s
% 40.76/41.07 % System time : 0.089 s
% 40.76/41.07 % Total time : 40.711 s
%------------------------------------------------------------------------------