%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : LCL526+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 : n018.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 5.73s 1.21s
% Output : CNFRefutation 5.73s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 21
% Syntax : Number of formulae : 88 ( 39 unt; 0 def)
% Number of atoms : 185 ( 25 equ)
% Maximal formula atoms : 10 ( 2 avg)
% Number of connectives : 153 ( 56 ~; 65 |; 17 &)
% ( 8 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 14 ( 12 usr; 12 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 4 con; 0-2 aty)
% Number of variables : 93 ( 6 sgn 33 !; 4 ?)
% 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(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(op_equiv,axiom,
( op_equiv
=> ! [X,Y] : equiv(X,Y) = and(implies(X,Y),implies(Y,X)) ),
file('theBenchmark.p',op_equiv) ).
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(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_substitution_strict_equiv,conjecture,
substitution_strict_equiv,
file('theBenchmark.p',s1_0_substitution_strict_equiv) ).
fof(s1_0_substitution_strict_equiv_neg,negated_conjecture,
~ substitution_strict_equiv,
inference(assume_negation,[status(cth)],[s1_0_substitution_strict_equiv]) ).
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_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_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_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_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(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]) ).
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(sK0,sK1))
& is_a_theorem(sK1)
& is_a_theorem(sK0) )
| 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,[sK0,sK1]),skolemize(X,sK0),skolemize(Y,sK1)],[nnf_34]) ).
fof(sk_adjunction,plain,
( ( ~ is_a_theorem(and(sK0,sK1))
| adjunction )
& ( is_a_theorem(sK1)
| adjunction )
& ( is_a_theorem(sK0)
| 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(sK0)
| adjunction ),
inference(split_conjunct,[status(thm)],[sk_adjunction]) ).
cnf(c_150,plain,
( is_a_theorem(sK1)
| adjunction ),
inference(split_conjunct,[status(thm)],[sk_adjunction]) ).
cnf(c_151,plain,
( ~ is_a_theorem(and(sK0,sK1))
| 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,
( ( ( sK3 != sK2
& is_a_theorem(strict_equiv(sK2,sK3)) )
| substitution_strict_equiv )
& ( ! [X0,X1] :
( X1 = X0
| ~ is_a_theorem(strict_equiv(X0,X1)) )
| ~ substitution_strict_equiv ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2,sK3]),skolemize(X,sK2),skolemize(Y,sK3)],[nnf_35]) ).
fof(sk_substitution_strict_equiv,plain,
( ( sK3 != sK2
| substitution_strict_equiv )
& ( is_a_theorem(strict_equiv(sK2,sK3))
| 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_153,plain,
( is_a_theorem(strict_equiv(sK2,sK3))
| substitution_strict_equiv ),
inference(split_conjunct,[status(thm)],[sk_substitution_strict_equiv]) ).
cnf(c_154,plain,
( sK3 != sK2
| 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]) ).
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_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,
~ substitution_strict_equiv,
inference(clausify,[status(thm)],[s1_0_substitution_strict_equiv_neg]) ).
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_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_226,plain,
( B = A
| ~ is_a_theorem(equiv(A,B)) ),
inference(resolve,[status(thm)],[c_140,c_64]) ).
cnf(c_231,plain,
is_a_theorem(implies(necessarily(A),A)),
inference(resolve,[status(thm)],[c_203,c_157]) ).
cnf(c_233,plain,
necessarily(implies(A,B)) = strict_implies(A,B),
inference(resolve,[status(thm)],[c_206,c_198]) ).
cnf(c_234,plain,
strict_equiv(A,B) = and(strict_implies(A,B),strict_implies(B,A)),
inference(resolve,[status(thm)],[c_207,c_199]) ).
cnf(c_235,negated_conjecture,
sK3 != sK2,
inference(resolve,[status(thm)],[c_208,c_154]) ).
cnf(c_236,negated_conjecture,
is_a_theorem(strict_equiv(sK2,sK3)),
inference(resolve,[status(thm)],[c_208,c_153]) ).
cnf(c_267,plain,
( is_a_theorem(A)
| ~ is_a_theorem(and(A,B)) ),
inference(resolve,[status(thm)],[c_217,c_212]) ).
cnf(c_270,plain,
( is_a_theorem(B)
| ~ is_a_theorem(and(A,B)) ),
inference(resolve,[status(thm)],[c_218,c_212]) ).
cnf(c_273,plain,
( is_a_theorem(implies(B,and(A,B)))
| ~ is_a_theorem(A) ),
inference(resolve,[status(thm)],[c_219,c_212]) ).
cnf(c_294,plain,
( B = A
| ~ is_a_theorem(and(implies(A,B),implies(B,A))) ),
inference(paramod,[status(thm)],[c_211,c_226]) ).
cnf(c_342,plain,
( is_a_theorem(A)
| ~ is_a_theorem(necessarily(A)) ),
inference(resolve,[status(thm)],[c_231,c_212]) ).
cnf(c_360,plain,
is_a_theorem(and(strict_implies(sK2,sK3),strict_implies(sK3,sK2))),
inference(paramod,[status(thm)],[c_234,c_236]) ).
cnf(c_423,plain,
( is_a_theorem(implies(A,B))
| ~ is_a_theorem(strict_implies(A,B)) ),
inference(paramod,[status(thm)],[c_233,c_342]) ).
cnf(c_1584,plain,
( adjunction
| is_a_theorem(implies(A,and(sK0,A))) ),
inference(resolve,[status(thm)],[c_273,c_149]) ).
cnf(c_2596,plain,
( is_a_theorem(and(sK0,A))
| ~ is_a_theorem(A)
| adjunction ),
inference(resolve,[status(thm)],[c_1584,c_212]) ).
cnf(c_8350,plain,
( adjunction
| is_a_theorem(and(sK0,sK1))
| adjunction ),
inference(resolve,[status(thm)],[c_2596,c_150]) ).
cnf(c_2852,plain,
( is_a_theorem(and(sK0,sK1))
| adjunction ),
inference(copy,[status(thm)],[c_8350]) ).
cnf(c_8351,plain,
( adjunction
| adjunction ),
inference(resolve,[status(thm)],[c_2852,c_151]) ).
cnf(c_2861,plain,
adjunction,
inference(copy,[status(thm)],[c_8351]) ).
cnf(c_3729,plain,
( is_a_theorem(and(A,B))
| ~ is_a_theorem(B)
| ~ is_a_theorem(A) ),
inference(resolve,[status(thm)],[c_2861,c_148]) ).
cnf(c_3834,plain,
is_a_theorem(strict_implies(sK3,sK2)),
inference(resolve,[status(thm)],[c_360,c_270]) ).
cnf(c_3835,plain,
is_a_theorem(strict_implies(sK2,sK3)),
inference(resolve,[status(thm)],[c_360,c_267]) ).
cnf(c_3840,plain,
is_a_theorem(implies(sK3,sK2)),
inference(resolve,[status(thm)],[c_3834,c_423]) ).
cnf(c_3850,plain,
is_a_theorem(implies(sK2,sK3)),
inference(resolve,[status(thm)],[c_3835,c_423]) ).
cnf(c_3856,plain,
( is_a_theorem(and(A,implies(sK3,sK2)))
| ~ is_a_theorem(A) ),
inference(resolve,[status(thm)],[c_3840,c_3729]) ).
cnf(c_5214,plain,
is_a_theorem(and(implies(sK2,sK3),implies(sK3,sK2))),
inference(resolve,[status(thm)],[c_3856,c_3850]) ).
cnf(c_8352,plain,
sK3 = sK2,
inference(resolve,[status(thm)],[c_5214,c_294]) ).
cnf(c_8349,plain,
$false,
inference(resolve,[status(thm)],[c_235,c_8352]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL526+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.37 % Computer : n018.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Fri Sep 25 22:44:06 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.37 % Process 3027757 was started by sandbox2 on n018,
% 0.09/0.37 % Fri Sep 25 22:44:06 2026
% 0.09/0.37 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.09/0.39
% 0.09/0.39 % From the command line: assign(max_seconds, 300).
% 5.73/1.21
% 5.73/1.21 % SZS status Theorem for theBenchmark
% 5.73/1.21
% 5.73/1.21 % Proof 1 at 0.61 (+ 0.17) seconds.
% 5.73/1.21 % Length of proof is 69.
% 5.73/1.21 % Level of proof is 11.
% 5.73/1.21 % Maximum clause weight is 31.000.
% 5.73/1.21 % Given clauses 438.
% 5.73/1.21
% 5.73/1.21 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------