%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : LCL528+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 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 : Sun Sep 27 07:59:06 AM UTC 2026
% Result : Theorem 182.42s 24.60s
% Output : CNFRefutation 0.20s
% Verified :
% SZS Type : Refutation
% Derivation depth : 39
% Number of leaves : 37
% Syntax : Number of formulae : 204 ( 96 unt; 0 def)
% Number of atoms : 403 ( 55 equ)
% Maximal formula atoms : 10 ( 1 avg)
% Number of connectives : 311 ( 112 ~; 143 |; 30 &)
% ( 15 <=>; 11 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 2 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 23 ( 21 usr; 21 prp; 0-2 aty)
% Number of functors : 16 ( 16 usr; 8 con; 0-2 aty)
% Number of variables : 265 ( 18 sgn 62 !; 8 ?)
% Comments :
%------------------------------------------------------------------------------
fof(modus_ponens,axiom,
( modus_ponens
<=> ! [X,Y] :
( ( is_a_theorem(implies(X,Y))
& is_a_theorem(X) )
=> is_a_theorem(Y) ) ),
file('theBenchmark.p',modus_ponens) ).
fof(substitution_of_equivalents,axiom,
( substitution_of_equivalents
<=> ! [X,Y] :
( is_a_theorem(equiv(X,Y))
=> X = Y ) ),
file('theBenchmark.p',substitution_of_equivalents) ).
fof(modus_tollens,axiom,
( modus_tollens
<=> ! [X,Y] : is_a_theorem(implies(implies(not(Y),not(X)),implies(X,Y))) ),
file('theBenchmark.p',modus_tollens) ).
fof(implies_2,axiom,
( implies_2
<=> ! [X,Y] : is_a_theorem(implies(implies(X,implies(X,Y)),implies(X,Y))) ),
file('theBenchmark.p',implies_2) ).
fof(and_1,axiom,
( and_1
<=> ! [X,Y] : is_a_theorem(implies(and(X,Y),X)) ),
file('theBenchmark.p',and_1) ).
fof(and_2,axiom,
( and_2
<=> ! [X,Y] : is_a_theorem(implies(and(X,Y),Y)) ),
file('theBenchmark.p',and_2) ).
fof(and_3,axiom,
( and_3
<=> ! [X,Y] : is_a_theorem(implies(X,implies(Y,and(X,Y)))) ),
file('theBenchmark.p',and_3) ).
fof(or_1,axiom,
( or_1
<=> ! [X,Y] : is_a_theorem(implies(X,or(X,Y))) ),
file('theBenchmark.p',or_1) ).
fof(or_2,axiom,
( or_2
<=> ! [X,Y] : is_a_theorem(implies(Y,or(X,Y))) ),
file('theBenchmark.p',or_2) ).
fof(op_or,axiom,
( op_or
=> ! [X,Y] : or(X,Y) = not(and(not(X),not(Y))) ),
file('theBenchmark.p',op_or) ).
fof(op_implies_and,axiom,
( op_implies_and
=> ! [X,Y] : implies(X,Y) = not(and(X,not(Y))) ),
file('theBenchmark.p',op_implies_and) ).
fof(op_equiv,axiom,
( op_equiv
=> ! [X,Y] : equiv(X,Y) = and(implies(X,Y),implies(Y,X)) ),
file('theBenchmark.p',op_equiv) ).
fof(necessitation,axiom,
( necessitation
<=> ! [X] :
( is_a_theorem(X)
=> is_a_theorem(necessarily(X)) ) ),
file('theBenchmark.p',necessitation) ).
fof(modus_ponens_strict_implies,axiom,
( modus_ponens_strict_implies
<=> ! [X,Y] :
( ( is_a_theorem(strict_implies(X,Y))
& is_a_theorem(X) )
=> is_a_theorem(Y) ) ),
file('theBenchmark.p',modus_ponens_strict_implies) ).
fof(adjunction,axiom,
( adjunction
<=> ! [X,Y] :
( ( is_a_theorem(Y)
& is_a_theorem(X) )
=> is_a_theorem(and(X,Y)) ) ),
file('theBenchmark.p',adjunction) ).
fof(substitution_strict_equiv,axiom,
( substitution_strict_equiv
<=> ! [X,Y] :
( is_a_theorem(strict_equiv(X,Y))
=> X = Y ) ),
file('theBenchmark.p',substitution_strict_equiv) ).
fof(axiom_M,axiom,
( axiom_M
<=> ! [X] : is_a_theorem(implies(necessarily(X),X)) ),
file('theBenchmark.p',axiom_M) ).
fof(axiom_m1,axiom,
( axiom_m1
<=> ! [X,Y] : is_a_theorem(strict_implies(and(X,Y),and(Y,X))) ),
file('theBenchmark.p',axiom_m1) ).
fof(op_strict_implies,axiom,
( op_strict_implies
=> ! [X,Y] : strict_implies(X,Y) = necessarily(implies(X,Y)) ),
file('theBenchmark.p',op_strict_implies) ).
fof(op_strict_equiv,axiom,
( op_strict_equiv
=> ! [X,Y] : strict_equiv(X,Y) = and(strict_implies(X,Y),strict_implies(Y,X)) ),
file('theBenchmark.p',op_strict_equiv) ).
fof(s1_0_axiom_m1,conjecture,
axiom_m1,
file('theBenchmark.p',s1_0_axiom_m1) ).
fof(s1_0_axiom_m1_neg,negated_conjecture,
~ axiom_m1,
inference(assume_negation,[status(cth)],[s1_0_axiom_m1]) ).
cnf(c_60,plain,
( is_a_theorem(B)
| ~ is_a_theorem(implies(A,B))
| ~ is_a_theorem(A)
| ~ modus_ponens ),
inference(clausify,[status(thm)],[modus_ponens]) ).
cnf(c_64,plain,
( B = A
| ~ is_a_theorem(equiv(A,B))
| ~ substitution_of_equivalents ),
inference(clausify,[status(thm)],[substitution_of_equivalents]) ).
cnf(c_67,plain,
( is_a_theorem(implies(implies(not(A),not(B)),implies(B,A)))
| ~ modus_tollens ),
inference(clausify,[status(thm)],[modus_tollens]) ).
cnf(c_71,plain,
( is_a_theorem(implies(implies(A,implies(A,B)),implies(A,B)))
| ~ implies_2 ),
inference(clausify,[status(thm)],[implies_2]) ).
cnf(c_75,plain,
( is_a_theorem(implies(and(A,B),A))
| ~ and_1 ),
inference(clausify,[status(thm)],[and_1]) ).
cnf(c_77,plain,
( is_a_theorem(implies(and(A,B),B))
| ~ and_2 ),
inference(clausify,[status(thm)],[and_2]) ).
cnf(c_79,plain,
( is_a_theorem(implies(A,implies(B,and(A,B))))
| ~ and_3 ),
inference(clausify,[status(thm)],[and_3]) ).
cnf(c_81,plain,
( is_a_theorem(implies(A,or(A,B)))
| ~ or_1 ),
inference(clausify,[status(thm)],[or_1]) ).
cnf(c_83,plain,
( is_a_theorem(implies(A,or(B,A)))
| ~ or_2 ),
inference(clausify,[status(thm)],[or_2]) ).
cnf(c_115,plain,
( or(A,B) = not(and(not(A),not(B)))
| ~ op_or ),
inference(clausify,[status(thm)],[op_or]) ).
cnf(c_116,plain,
( not(and(not(A),not(B))) = or(A,B)
| ~ op_or ),
inference(copy,[status(thm)],[c_115]) ).
cnf(c_119,plain,
( not(and(A,not(B))) = implies(A,B)
| ~ op_implies_and ),
inference(clausify,[status(thm)],[op_implies_and]) ).
cnf(c_121,plain,
( and(implies(A,B),implies(B,A)) = equiv(A,B)
| ~ op_equiv ),
inference(clausify,[status(thm)],[op_equiv]) ).
cnf(c_122,plain,
( equiv(A,B) = and(implies(A,B),implies(B,A))
| ~ op_equiv ),
inference(copy,[status(thm)],[c_121]) ).
fof(hilbert_op_or,axiom,
op_or,
file('theBenchmark.p',hilbert_op_or) ).
cnf(c_123,plain,
op_or,
inference(clausify,[status(thm)],[hilbert_op_or]) ).
fof(hilbert_op_implies_and,axiom,
op_implies_and,
file('theBenchmark.p',hilbert_op_implies_and) ).
cnf(c_124,plain,
op_implies_and,
inference(clausify,[status(thm)],[hilbert_op_implies_and]) ).
fof(hilbert_op_equiv,axiom,
op_equiv,
file('theBenchmark.p',hilbert_op_equiv) ).
cnf(c_125,plain,
op_equiv,
inference(clausify,[status(thm)],[hilbert_op_equiv]) ).
fof(hilbert_modus_ponens,axiom,
modus_ponens,
file('theBenchmark.p',hilbert_modus_ponens) ).
cnf(c_126,plain,
modus_ponens,
inference(clausify,[status(thm)],[hilbert_modus_ponens]) ).
fof(hilbert_modus_tollens,axiom,
modus_tollens,
file('theBenchmark.p',hilbert_modus_tollens) ).
cnf(c_127,plain,
modus_tollens,
inference(clausify,[status(thm)],[hilbert_modus_tollens]) ).
fof(hilbert_implies_2,axiom,
implies_2,
file('theBenchmark.p',hilbert_implies_2) ).
cnf(c_129,plain,
implies_2,
inference(clausify,[status(thm)],[hilbert_implies_2]) ).
fof(hilbert_and_1,axiom,
and_1,
file('theBenchmark.p',hilbert_and_1) ).
cnf(c_131,plain,
and_1,
inference(clausify,[status(thm)],[hilbert_and_1]) ).
fof(hilbert_and_2,axiom,
and_2,
file('theBenchmark.p',hilbert_and_2) ).
cnf(c_132,plain,
and_2,
inference(clausify,[status(thm)],[hilbert_and_2]) ).
fof(hilbert_and_3,axiom,
and_3,
file('theBenchmark.p',hilbert_and_3) ).
cnf(c_133,plain,
and_3,
inference(clausify,[status(thm)],[hilbert_and_3]) ).
fof(hilbert_or_1,axiom,
or_1,
file('theBenchmark.p',hilbert_or_1) ).
cnf(c_134,plain,
or_1,
inference(clausify,[status(thm)],[hilbert_or_1]) ).
fof(hilbert_or_2,axiom,
or_2,
file('theBenchmark.p',hilbert_or_2) ).
cnf(c_135,plain,
or_2,
inference(clausify,[status(thm)],[hilbert_or_2]) ).
fof(use_substitution_of_equivalents,axiom,
substitution_of_equivalents,
file('theBenchmark.p',use_substitution_of_equivalents) ).
cnf(c_140,plain,
substitution_of_equivalents,
inference(clausify,[status(thm)],[use_substitution_of_equivalents]) ).
cnf(c_141,plain,
( is_a_theorem(necessarily(A))
| ~ is_a_theorem(A)
| ~ necessitation ),
inference(clausify,[status(thm)],[necessitation]) ).
fof(nnf_33,plain,
( ( ? [X,Y] :
( ~ is_a_theorem(Y)
& is_a_theorem(strict_implies(X,Y))
& is_a_theorem(X) )
| modus_ponens_strict_implies )
& ( ! [X0,X1] :
( is_a_theorem(X1)
| ~ is_a_theorem(strict_implies(X0,X1))
| ~ is_a_theorem(X0) )
| ~ modus_ponens_strict_implies ) ),
inference(fof_nnf,[status(thm)],[modus_ponens_strict_implies]) ).
fof(sk_modus_ponens_strict_implies_sk,plain,
( ( ( ~ is_a_theorem(sK1)
& is_a_theorem(strict_implies(sK0,sK1))
& is_a_theorem(sK0) )
| modus_ponens_strict_implies )
& ( ! [X0,X1] :
( is_a_theorem(X1)
| ~ is_a_theorem(strict_implies(X0,X1))
| ~ is_a_theorem(X0) )
| ~ modus_ponens_strict_implies ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1]),skolemize(X,sK0),skolemize(Y,sK1)],[nnf_33]) ).
fof(sk_modus_ponens_strict_implies,plain,
( ( ~ is_a_theorem(sK1)
| modus_ponens_strict_implies )
& ( is_a_theorem(strict_implies(sK0,sK1))
| modus_ponens_strict_implies )
& ( is_a_theorem(sK0)
| modus_ponens_strict_implies )
& ! [VAR_0,VAR_1] :
( is_a_theorem(VAR_1)
| ~ is_a_theorem(strict_implies(VAR_0,VAR_1))
| ~ is_a_theorem(VAR_0)
| ~ modus_ponens_strict_implies ) ),
inference(cnf_transformation,[status(thm)],[sk_modus_ponens_strict_implies_sk]) ).
cnf(c_144,plain,
( is_a_theorem(B)
| ~ is_a_theorem(strict_implies(A,B))
| ~ is_a_theorem(A)
| ~ modus_ponens_strict_implies ),
inference(split_conjunct,[status(thm)],[sk_modus_ponens_strict_implies]) ).
cnf(c_145,plain,
( is_a_theorem(sK0)
| modus_ponens_strict_implies ),
inference(split_conjunct,[status(thm)],[sk_modus_ponens_strict_implies]) ).
cnf(c_146,plain,
( is_a_theorem(strict_implies(sK0,sK1))
| modus_ponens_strict_implies ),
inference(split_conjunct,[status(thm)],[sk_modus_ponens_strict_implies]) ).
cnf(c_147,plain,
( ~ is_a_theorem(sK1)
| modus_ponens_strict_implies ),
inference(split_conjunct,[status(thm)],[sk_modus_ponens_strict_implies]) ).
fof(nnf_34,plain,
( ( ? [X,Y] :
( ~ is_a_theorem(and(X,Y))
& is_a_theorem(Y)
& is_a_theorem(X) )
| adjunction )
& ( ! [X0,X1] :
( is_a_theorem(and(X0,X1))
| ~ is_a_theorem(X1)
| ~ is_a_theorem(X0) )
| ~ adjunction ) ),
inference(fof_nnf,[status(thm)],[adjunction]) ).
fof(sk_adjunction_sk,plain,
( ( ( ~ is_a_theorem(and(sK2,sK3))
& is_a_theorem(sK3)
& is_a_theorem(sK2) )
| adjunction )
& ( ! [X0,X1] :
( is_a_theorem(and(X0,X1))
| ~ is_a_theorem(X1)
| ~ is_a_theorem(X0) )
| ~ adjunction ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2,sK3]),skolemize(X,sK2),skolemize(Y,sK3)],[nnf_34]) ).
fof(sk_adjunction,plain,
( ( ~ is_a_theorem(and(sK2,sK3))
| adjunction )
& ( is_a_theorem(sK3)
| adjunction )
& ( is_a_theorem(sK2)
| adjunction )
& ! [VAR_0,VAR_1] :
( is_a_theorem(and(VAR_0,VAR_1))
| ~ is_a_theorem(VAR_1)
| ~ is_a_theorem(VAR_0)
| ~ adjunction ) ),
inference(cnf_transformation,[status(thm)],[sk_adjunction_sk]) ).
cnf(c_148,plain,
( is_a_theorem(and(A,B))
| ~ is_a_theorem(B)
| ~ is_a_theorem(A)
| ~ adjunction ),
inference(split_conjunct,[status(thm)],[sk_adjunction]) ).
cnf(c_149,plain,
( is_a_theorem(sK2)
| adjunction ),
inference(split_conjunct,[status(thm)],[sk_adjunction]) ).
cnf(c_150,plain,
( is_a_theorem(sK3)
| adjunction ),
inference(split_conjunct,[status(thm)],[sk_adjunction]) ).
cnf(c_151,plain,
( ~ is_a_theorem(and(sK2,sK3))
| adjunction ),
inference(split_conjunct,[status(thm)],[sk_adjunction]) ).
fof(nnf_35,plain,
( ( ? [X,Y] :
( Y != X
& is_a_theorem(strict_equiv(X,Y)) )
| substitution_strict_equiv )
& ( ! [X0,X1] :
( X1 = X0
| ~ is_a_theorem(strict_equiv(X0,X1)) )
| ~ substitution_strict_equiv ) ),
inference(fof_nnf,[status(thm)],[substitution_strict_equiv]) ).
fof(sk_substitution_strict_equiv_sk,plain,
( ( ( sK5 != sK4
& is_a_theorem(strict_equiv(sK4,sK5)) )
| substitution_strict_equiv )
& ( ! [X0,X1] :
( X1 = X0
| ~ is_a_theorem(strict_equiv(X0,X1)) )
| ~ substitution_strict_equiv ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4,sK5]),skolemize(X,sK4),skolemize(Y,sK5)],[nnf_35]) ).
fof(sk_substitution_strict_equiv,plain,
( ( sK5 != sK4
| substitution_strict_equiv )
& ( is_a_theorem(strict_equiv(sK4,sK5))
| substitution_strict_equiv )
& ! [VAR_0,VAR_1] :
( VAR_1 = VAR_0
| ~ is_a_theorem(strict_equiv(VAR_0,VAR_1))
| ~ substitution_strict_equiv ) ),
inference(cnf_transformation,[status(thm)],[sk_substitution_strict_equiv_sk]) ).
cnf(c_152,plain,
( B = A
| ~ is_a_theorem(strict_equiv(A,B))
| ~ substitution_strict_equiv ),
inference(split_conjunct,[status(thm)],[sk_substitution_strict_equiv]) ).
cnf(c_153,plain,
( is_a_theorem(strict_equiv(sK4,sK5))
| substitution_strict_equiv ),
inference(split_conjunct,[status(thm)],[sk_substitution_strict_equiv]) ).
cnf(c_154,plain,
( sK5 != sK4
| substitution_strict_equiv ),
inference(split_conjunct,[status(thm)],[sk_substitution_strict_equiv]) ).
cnf(c_157,plain,
( is_a_theorem(implies(necessarily(A),A))
| ~ axiom_M ),
inference(clausify,[status(thm)],[axiom_M]) ).
fof(nnf_45,plain,
( ( ? [X,Y] : ~ is_a_theorem(strict_implies(and(X,Y),and(Y,X)))
| axiom_m1 )
& ( ! [X0,X1] : is_a_theorem(strict_implies(and(X0,X1),and(X1,X0)))
| ~ axiom_m1 ) ),
inference(fof_nnf,[status(thm)],[axiom_m1]) ).
fof(sk_axiom_m1_sk,plain,
( ( ~ is_a_theorem(strict_implies(and(sK6,sK7),and(sK7,sK6)))
| axiom_m1 )
& ( ! [X0,X1] : is_a_theorem(strict_implies(and(X0,X1),and(X1,X0)))
| ~ axiom_m1 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6,sK7]),skolemize(X,sK6),skolemize(Y,sK7)],[nnf_45]) ).
fof(sk_axiom_m1,plain,
( ( ~ is_a_theorem(strict_implies(and(sK6,sK7),and(sK7,sK6)))
| axiom_m1 )
& ! [VAR_0,VAR_1] :
( is_a_theorem(strict_implies(and(VAR_0,VAR_1),and(VAR_1,VAR_0)))
| ~ axiom_m1 ) ),
inference(cnf_transformation,[status(thm)],[sk_axiom_m1_sk]) ).
cnf(c_174,plain,
( ~ is_a_theorem(strict_implies(and(sK6,sK7),and(sK7,sK6)))
| axiom_m1 ),
inference(split_conjunct,[status(thm)],[sk_axiom_m1]) ).
cnf(c_197,plain,
( strict_implies(A,B) = necessarily(implies(A,B))
| ~ op_strict_implies ),
inference(clausify,[status(thm)],[op_strict_implies]) ).
cnf(c_198,plain,
( necessarily(implies(A,B)) = strict_implies(A,B)
| ~ op_strict_implies ),
inference(copy,[status(thm)],[c_197]) ).
cnf(c_199,plain,
( strict_equiv(A,B) = and(strict_implies(A,B),strict_implies(B,A))
| ~ op_strict_equiv ),
inference(clausify,[status(thm)],[op_strict_equiv]) ).
fof(km5_necessitation,axiom,
necessitation,
file('theBenchmark.p',km5_necessitation) ).
cnf(c_201,plain,
necessitation,
inference(clausify,[status(thm)],[km5_necessitation]) ).
fof(km5_axiom_M,axiom,
axiom_M,
file('theBenchmark.p',km5_axiom_M) ).
cnf(c_203,plain,
axiom_M,
inference(clausify,[status(thm)],[km5_axiom_M]) ).
fof(s1_0_op_strict_implies,axiom,
op_strict_implies,
file('theBenchmark.p',s1_0_op_strict_implies) ).
cnf(c_206,plain,
op_strict_implies,
inference(clausify,[status(thm)],[s1_0_op_strict_implies]) ).
fof(s1_0_op_strict_equiv,axiom,
op_strict_equiv,
file('theBenchmark.p',s1_0_op_strict_equiv) ).
cnf(c_207,plain,
op_strict_equiv,
inference(clausify,[status(thm)],[s1_0_op_strict_equiv]) ).
cnf(c_208,negated_conjecture,
~ axiom_m1,
inference(clausify,[status(thm)],[s1_0_axiom_m1_neg]) ).
cnf(c_209,plain,
not(and(not(A),not(B))) = or(A,B),
inference(resolve,[status(thm)],[c_123,c_116]) ).
cnf(c_210,plain,
not(and(A,not(B))) = implies(A,B),
inference(resolve,[status(thm)],[c_124,c_119]) ).
cnf(c_211,plain,
equiv(A,B) = and(implies(A,B),implies(B,A)),
inference(resolve,[status(thm)],[c_125,c_122]) ).
cnf(c_212,plain,
( is_a_theorem(B)
| ~ is_a_theorem(implies(A,B))
| ~ is_a_theorem(A) ),
inference(resolve,[status(thm)],[c_126,c_60]) ).
cnf(c_213,plain,
is_a_theorem(implies(implies(not(A),not(B)),implies(B,A))),
inference(resolve,[status(thm)],[c_127,c_67]) ).
cnf(c_215,plain,
is_a_theorem(implies(implies(A,implies(A,B)),implies(A,B))),
inference(resolve,[status(thm)],[c_129,c_71]) ).
cnf(c_217,plain,
is_a_theorem(implies(and(A,B),A)),
inference(resolve,[status(thm)],[c_131,c_75]) ).
cnf(c_218,plain,
is_a_theorem(implies(and(A,B),B)),
inference(resolve,[status(thm)],[c_132,c_77]) ).
cnf(c_219,plain,
is_a_theorem(implies(A,implies(B,and(A,B)))),
inference(resolve,[status(thm)],[c_133,c_79]) ).
cnf(c_220,plain,
is_a_theorem(implies(A,or(A,B))),
inference(resolve,[status(thm)],[c_134,c_81]) ).
cnf(c_221,plain,
is_a_theorem(implies(A,or(B,A))),
inference(resolve,[status(thm)],[c_135,c_83]) ).
cnf(c_28186,plain,
( B = A
| ~ is_a_theorem(and(implies(A,B),implies(B,A)))
| ~ substitution_of_equivalents ),
inference(paramod,[status(thm)],[c_211,c_64]) ).
cnf(c_223,plain,
( B = A
| ~ is_a_theorem(and(implies(A,B),implies(B,A))) ),
inference(resolve,[status(thm)],[c_140,c_28186]) ).
cnf(c_226,plain,
( is_a_theorem(necessarily(A))
| ~ is_a_theorem(A) ),
inference(resolve,[status(thm)],[c_201,c_141]) ).
cnf(c_228,plain,
is_a_theorem(implies(necessarily(A),A)),
inference(resolve,[status(thm)],[c_203,c_157]) ).
cnf(c_230,plain,
necessarily(implies(A,B)) = strict_implies(A,B),
inference(resolve,[status(thm)],[c_206,c_198]) ).
cnf(c_231,plain,
strict_equiv(A,B) = and(strict_implies(A,B),strict_implies(B,A)),
inference(resolve,[status(thm)],[c_207,c_199]) ).
cnf(c_232,negated_conjecture,
~ is_a_theorem(strict_implies(and(sK6,sK7),and(sK7,sK6))),
inference(resolve,[status(thm)],[c_208,c_174]) ).
cnf(c_28187,plain,
implies(not(A),B) = or(A,B),
inference(paramod,[status(thm)],[c_210,c_209]) ).
cnf(c_233,plain,
or(A,B) = implies(not(A),B),
inference(copy,[status(thm)],[c_28187]) ).
cnf(c_240,plain,
( is_a_theorem(and(strict_implies(sK4,sK5),strict_implies(sK5,sK4)))
| substitution_strict_equiv ),
inference(paramod,[status(thm)],[c_231,c_153]) ).
cnf(c_241,plain,
( B = A
| ~ is_a_theorem(and(strict_implies(A,B),strict_implies(B,A)))
| ~ substitution_strict_equiv ),
inference(paramod,[status(thm)],[c_231,c_152]) ).
cnf(c_247,plain,
( is_a_theorem(implies(B,A))
| ~ is_a_theorem(implies(not(A),not(B))) ),
inference(resolve,[status(thm)],[c_213,c_212]) ).
cnf(c_255,plain,
( is_a_theorem(implies(A,B))
| ~ is_a_theorem(implies(A,implies(A,B))) ),
inference(resolve,[status(thm)],[c_215,c_212]) ).
cnf(c_261,plain,
( is_a_theorem(A)
| ~ is_a_theorem(and(A,B)) ),
inference(resolve,[status(thm)],[c_217,c_212]) ).
cnf(c_264,plain,
( is_a_theorem(B)
| ~ is_a_theorem(and(A,B)) ),
inference(resolve,[status(thm)],[c_218,c_212]) ).
cnf(c_267,plain,
( is_a_theorem(implies(B,and(A,B)))
| ~ is_a_theorem(A) ),
inference(resolve,[status(thm)],[c_219,c_212]) ).
cnf(c_271,plain,
( is_a_theorem(and(A,implies(B,or(B,C))))
| ~ is_a_theorem(A)
| ~ adjunction ),
inference(resolve,[status(thm)],[c_220,c_148]) ).
cnf(c_28188,plain,
is_a_theorem(necessarily(implies(and(A,B),A))),
inference(resolve,[status(thm)],[c_226,c_217]) ).
cnf(c_301,plain,
is_a_theorem(strict_implies(and(A,B),A)),
inference(paramod,[status(thm)],[c_230,c_28188]) ).
cnf(c_28189,plain,
is_a_theorem(necessarily(implies(implies(not(A),not(B)),implies(B,A)))),
inference(resolve,[status(thm)],[c_226,c_213]) ).
cnf(c_305,plain,
is_a_theorem(strict_implies(implies(not(A),not(B)),implies(B,A))),
inference(paramod,[status(thm)],[c_230,c_28189]) ).
cnf(c_313,plain,
( is_a_theorem(A)
| ~ is_a_theorem(necessarily(A)) ),
inference(resolve,[status(thm)],[c_228,c_212]) ).
cnf(c_377,plain,
( is_a_theorem(implies(A,B))
| ~ is_a_theorem(strict_implies(A,B)) ),
inference(paramod,[status(thm)],[c_230,c_313]) ).
cnf(c_429,plain,
( substitution_strict_equiv
| is_a_theorem(strict_implies(sK4,sK5)) ),
inference(resolve,[status(thm)],[c_261,c_240]) ).
cnf(c_436,plain,
( substitution_strict_equiv
| is_a_theorem(strict_implies(sK5,sK4)) ),
inference(resolve,[status(thm)],[c_264,c_240]) ).
cnf(c_596,plain,
( substitution_strict_equiv
| is_a_theorem(implies(sK5,sK4)) ),
inference(resolve,[status(thm)],[c_377,c_436]) ).
cnf(c_597,plain,
( substitution_strict_equiv
| is_a_theorem(implies(sK4,sK5)) ),
inference(resolve,[status(thm)],[c_377,c_429]) ).
cnf(c_598,plain,
( modus_ponens_strict_implies
| is_a_theorem(implies(sK0,sK1)) ),
inference(resolve,[status(thm)],[c_377,c_146]) ).
cnf(c_616,plain,
( is_a_theorem(and(implies(sK4,sK5),A))
| ~ is_a_theorem(A)
| ~ adjunction
| substitution_strict_equiv ),
inference(resolve,[status(thm)],[c_597,c_148]) ).
cnf(c_623,plain,
( is_a_theorem(sK1)
| ~ is_a_theorem(sK0)
| modus_ponens_strict_implies ),
inference(resolve,[status(thm)],[c_598,c_212]) ).
cnf(c_28190,plain,
( modus_ponens_strict_implies
| is_a_theorem(sK1)
| modus_ponens_strict_implies ),
inference(resolve,[status(thm)],[c_623,c_145]) ).
cnf(c_626,plain,
( is_a_theorem(sK1)
| modus_ponens_strict_implies ),
inference(copy,[status(thm)],[c_28190]) ).
cnf(c_28191,plain,
( modus_ponens_strict_implies
| modus_ponens_strict_implies ),
inference(resolve,[status(thm)],[c_626,c_147]) ).
cnf(c_636,plain,
modus_ponens_strict_implies,
inference(copy,[status(thm)],[c_28191]) ).
cnf(c_637,plain,
( is_a_theorem(B)
| ~ is_a_theorem(strict_implies(A,B))
| ~ is_a_theorem(A) ),
inference(resolve,[status(thm)],[c_636,c_144]) ).
cnf(c_676,plain,
( is_a_theorem(and(strict_implies(and(B,C),B),A))
| ~ is_a_theorem(A)
| ~ adjunction ),
inference(resolve,[status(thm)],[c_301,c_148]) ).
cnf(c_1019,plain,
( adjunction
| is_a_theorem(implies(A,and(sK2,A))) ),
inference(resolve,[status(thm)],[c_267,c_149]) ).
cnf(c_1154,plain,
( is_a_theorem(and(sK2,A))
| ~ is_a_theorem(A)
| adjunction ),
inference(resolve,[status(thm)],[c_1019,c_212]) ).
cnf(c_28192,plain,
( adjunction
| is_a_theorem(and(sK2,sK3))
| adjunction ),
inference(resolve,[status(thm)],[c_1154,c_150]) ).
cnf(c_1246,plain,
( is_a_theorem(and(sK2,sK3))
| adjunction ),
inference(copy,[status(thm)],[c_28192]) ).
cnf(c_28193,plain,
( adjunction
| adjunction ),
inference(resolve,[status(thm)],[c_1246,c_151]) ).
cnf(c_1255,plain,
adjunction,
inference(copy,[status(thm)],[c_28193]) ).
cnf(c_1295,plain,
( is_a_theorem(and(strict_implies(and(B,C),B),A))
| ~ is_a_theorem(A) ),
inference(resolve,[status(thm)],[c_1255,c_676]) ).
cnf(c_1310,plain,
( is_a_theorem(and(implies(sK4,sK5),A))
| ~ is_a_theorem(A)
| substitution_strict_equiv ),
inference(resolve,[status(thm)],[c_1255,c_616]) ).
cnf(c_1349,plain,
( is_a_theorem(and(A,implies(B,or(B,C))))
| ~ is_a_theorem(A) ),
inference(resolve,[status(thm)],[c_1255,c_271]) ).
cnf(c_28194,plain,
( substitution_strict_equiv
| is_a_theorem(and(implies(sK4,sK5),implies(sK5,sK4)))
| substitution_strict_equiv ),
inference(resolve,[status(thm)],[c_1310,c_596]) ).
cnf(c_1382,plain,
( is_a_theorem(and(implies(sK4,sK5),implies(sK5,sK4)))
| substitution_strict_equiv ),
inference(copy,[status(thm)],[c_28194]) ).
cnf(c_1725,plain,
( sK5 = sK4
| substitution_strict_equiv ),
inference(resolve,[status(thm)],[c_1382,c_223]) ).
cnf(c_28195,plain,
( substitution_strict_equiv
| substitution_strict_equiv ),
inference(resolve,[status(thm)],[c_1725,c_154]) ).
cnf(c_1726,plain,
substitution_strict_equiv,
inference(copy,[status(thm)],[c_28195]) ).
cnf(c_1729,plain,
( B = A
| ~ is_a_theorem(and(strict_implies(A,B),strict_implies(B,A))) ),
inference(resolve,[status(thm)],[c_1726,c_241]) ).
cnf(c_2804,plain,
is_a_theorem(implies(A,and(A,A))),
inference(resolve,[status(thm)],[c_255,c_219]) ).
cnf(c_28196,plain,
is_a_theorem(necessarily(implies(A,and(A,A)))),
inference(resolve,[status(thm)],[c_2804,c_226]) ).
cnf(c_2882,plain,
is_a_theorem(strict_implies(A,and(A,A))),
inference(paramod,[status(thm)],[c_230,c_28196]) ).
cnf(c_5325,plain,
is_a_theorem(strict_implies(implies(not(A),not(not(B))),or(B,A))),
inference(paramod,[status(thm)],[c_233,c_305]) ).
cnf(c_5728,plain,
is_a_theorem(and(strict_implies(and(A,B),A),strict_implies(C,and(C,C)))),
inference(resolve,[status(thm)],[c_1295,c_2882]) ).
cnf(c_28197,plain,
A = and(A,A),
inference(resolve,[status(thm)],[c_5728,c_1729]) ).
cnf(c_16443,plain,
and(A,A) = A,
inference(copy,[status(thm)],[c_28197]) ).
cnf(c_16447,plain,
not(not(A)) = implies(not(A),A),
inference(paramod,[status(thm)],[c_16443,c_210]) ).
cnf(c_16451,plain,
is_a_theorem(strict_implies(implies(not(A),implies(not(B),B)),or(B,A))),
inference(paramod,[status(thm)],[c_16447,c_5325]) ).
cnf(c_28198,plain,
not(implies(A,B)) = implies(not(and(A,not(B))),and(A,not(B))),
inference(paramod,[status(thm)],[c_210,c_16447]) ).
cnf(c_16463,plain,
not(implies(A,B)) = implies(implies(A,B),and(A,not(B))),
inference(paramod,[status(thm)],[c_210,c_28198]) ).
cnf(c_16466,plain,
or(not(A),B) = implies(implies(not(A),A),B),
inference(paramod,[status(thm)],[c_16447,c_233]) ).
cnf(c_28199,plain,
not(not(A)) = or(A,A),
inference(paramod,[status(thm)],[c_233,c_16447]) ).
cnf(c_16467,plain,
implies(not(A),A) = or(A,A),
inference(paramod,[status(thm)],[c_16447,c_28199]) ).
cnf(c_28200,plain,
( is_a_theorem(implies(not(B),A))
| ~ is_a_theorem(implies(not(A),implies(not(B),B))) ),
inference(paramod,[status(thm)],[c_16447,c_247]) ).
cnf(c_16469,plain,
( is_a_theorem(implies(not(B),A))
| ~ is_a_theorem(implies(not(A),or(B,B))) ),
inference(paramod,[status(thm)],[c_16467,c_28200]) ).
cnf(c_16744,plain,
or(not(A),B) = implies(or(A,A),B),
inference(paramod,[status(thm)],[c_16467,c_16466]) ).
cnf(c_16748,plain,
is_a_theorem(strict_implies(implies(not(A),or(B,B)),or(B,A))),
inference(paramod,[status(thm)],[c_16467,c_16451]) ).
cnf(c_16751,plain,
not(not(A)) = or(A,A),
inference(paramod,[status(thm)],[c_16467,c_16447]) ).
cnf(c_28201,plain,
is_a_theorem(implies(not(not(A)),A)),
inference(resolve,[status(thm)],[c_16469,c_221]) ).
cnf(c_16904,plain,
is_a_theorem(implies(or(A,A),A)),
inference(paramod,[status(thm)],[c_16751,c_28201]) ).
cnf(c_16939,plain,
is_a_theorem(and(implies(or(A,A),A),implies(B,or(B,C)))),
inference(resolve,[status(thm)],[c_16904,c_1349]) ).
cnf(c_17044,plain,
not(and(A,or(B,B))) = implies(A,not(B)),
inference(paramod,[status(thm)],[c_16751,c_210]) ).
cnf(c_18565,plain,
( is_a_theorem(or(B,A))
| ~ is_a_theorem(implies(not(A),or(B,B))) ),
inference(resolve,[status(thm)],[c_16748,c_637]) ).
cnf(c_18578,plain,
( is_a_theorem(or(B,not(A)))
| ~ is_a_theorem(implies(or(A,A),or(B,B))) ),
inference(paramod,[status(thm)],[c_16751,c_18565]) ).
cnf(c_28202,plain,
A = or(A,A),
inference(resolve,[status(thm)],[c_16939,c_223]) ).
cnf(c_21349,plain,
or(A,A) = A,
inference(copy,[status(thm)],[c_28202]) ).
cnf(c_28203,plain,
( is_a_theorem(or(B,not(A)))
| ~ is_a_theorem(implies(A,or(B,B))) ),
inference(paramod,[status(thm)],[c_21349,c_18578]) ).
cnf(c_21903,plain,
( is_a_theorem(or(B,not(A)))
| ~ is_a_theorem(implies(A,B)) ),
inference(paramod,[status(thm)],[c_21349,c_28203]) ).
cnf(c_22114,plain,
not(and(A,B)) = implies(A,not(B)),
inference(paramod,[status(thm)],[c_21349,c_17044]) ).
cnf(c_22230,plain,
not(not(A)) = A,
inference(paramod,[status(thm)],[c_21349,c_16751]) ).
cnf(c_22237,plain,
or(not(A),B) = implies(A,B),
inference(paramod,[status(thm)],[c_21349,c_16744]) ).
cnf(c_22299,plain,
implies(not(A),A) = A,
inference(paramod,[status(thm)],[c_21349,c_16467]) ).
cnf(c_28204,plain,
is_a_theorem(or(implies(A,B),not(implies(not(B),not(A))))),
inference(resolve,[status(thm)],[c_21903,c_213]) ).
cnf(c_28205,plain,
is_a_theorem(or(implies(A,B),implies(implies(not(B),not(A)),and(not(B),not(not(A)))))),
inference(paramod,[status(thm)],[c_16463,c_28204]) ).
cnf(c_23181,plain,
is_a_theorem(or(implies(A,B),implies(implies(not(B),not(A)),and(not(B),A)))),
inference(paramod,[status(thm)],[c_22230,c_28205]) ).
cnf(c_23247,plain,
implies(implies(A,not(B)),and(A,B)) = and(A,B),
inference(paramod,[status(thm)],[c_22114,c_22299]) ).
cnf(c_23250,plain,
or(implies(A,not(B)),C) = implies(and(A,B),C),
inference(paramod,[status(thm)],[c_22114,c_22237]) ).
cnf(c_23253,plain,
is_a_theorem(or(implies(A,B),and(not(B),A))),
inference(paramod,[status(thm)],[c_23247,c_23181]) ).
cnf(c_28206,plain,
is_a_theorem(or(implies(A,not(B)),and(B,A))),
inference(paramod,[status(thm)],[c_22230,c_23253]) ).
cnf(c_28141,plain,
is_a_theorem(implies(and(A,B),and(B,A))),
inference(paramod,[status(thm)],[c_23250,c_28206]) ).
cnf(c_28207,plain,
is_a_theorem(necessarily(implies(and(A,B),and(B,A)))),
inference(resolve,[status(thm)],[c_28141,c_226]) ).
cnf(c_28184,plain,
is_a_theorem(strict_implies(and(A,B),and(B,A))),
inference(paramod,[status(thm)],[c_230,c_28207]) ).
cnf(c_28185,plain,
$false,
inference(resolve,[status(thm)],[c_28184,c_232]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : LCL528+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% 0.00/0.06 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.41 % Computer : n009.cluster.edu
% 0.17/0.41 % Model : x86_64 x86_64
% 0.17/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.41 % Memory : 8046.5625MB
% 0.17/0.41 % OS : Linux 6.8.0-71-generic
% 0.17/0.42 % CPULimit : 300
% 0.17/0.42 % WCLimit : 300
% 0.17/0.42 % DateTime : Fri Sep 25 22:42:14 UTC 2026
% 0.17/0.42 % CPUTime :
% 0.17/0.42 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.17/0.42 % Process 2759065 was started by sandbox2 on n009,
% 0.17/0.42 % Fri Sep 25 22:42:14 2026
% 0.17/0.42 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.17/0.45
% 0.17/0.45 % From the command line: assign(max_seconds, 300).
% 182.42/24.60
% 182.42/24.60 % given #500 (T,wt=30): 2986 is_a_theorem(and(strict_implies(A,implies(B,B)),implies(C,C))). [resolve(2811,a,2826,a)].
% 182.42/24.60
% 182.42/24.60 % given #1000 (T,wt=32): 7825 is_a_theorem(and(implies(and(A,B),A),implies(and(C,D),D))). [resolve(1353,a,217,a)].
% 182.42/24.60
% 182.42/24.60 % SZS status Theorem for theBenchmark
% 182.42/24.60
% 182.42/24.60 % Proof 1 at 5.57 (+ 2.31) seconds.
% 182.42/24.60 % Length of proof is 153.
% 182.42/24.60 % Level of proof is 25.
% 182.42/24.60 % Maximum clause weight is 46.000.
% 182.42/24.60 % Given clauses 1191.
% 182.42/24.60
% 182.42/24.60 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------