%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : LCL539+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:08 AM UTC 2026
% Result : Theorem 5.36s 1.16s
% Output : CNFRefutation 5.36s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 21
% Syntax : Number of formulae : 90 ( 42 unt; 0 def)
% Number of atoms : 187 ( 24 equ)
% Maximal formula atoms : 10 ( 2 avg)
% Number of connectives : 152 ( 55 ~; 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 : 95 ( 4 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]) ).
fof(hilbert_op_equiv,axiom,
op_equiv,
file('theBenchmark.p',hilbert_op_equiv) ).
cnf(c_124,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_125,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_130,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_131,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_132,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_139,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_147,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_148,plain,
( is_a_theorem(sK0)
| adjunction ),
inference(split_conjunct,[status(thm)],[sk_adjunction]) ).
cnf(c_149,plain,
( is_a_theorem(sK1)
| adjunction ),
inference(split_conjunct,[status(thm)],[sk_adjunction]) ).
cnf(c_150,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_152,plain,
( is_a_theorem(strict_equiv(sK2,sK3))
| substitution_strict_equiv ),
inference(split_conjunct,[status(thm)],[sk_substitution_strict_equiv]) ).
cnf(c_153,plain,
( sK3 != sK2
| substitution_strict_equiv ),
inference(split_conjunct,[status(thm)],[sk_substitution_strict_equiv]) ).
cnf(c_156,plain,
( is_a_theorem(implies(necessarily(A),A))
| ~ axiom_M ),
inference(clausify,[status(thm)],[axiom_M]) ).
cnf(c_196,plain,
( strict_implies(A,B) = necessarily(implies(A,B))
| ~ op_strict_implies ),
inference(clausify,[status(thm)],[op_strict_implies]) ).
cnf(c_197,plain,
( necessarily(implies(A,B)) = strict_implies(A,B)
| ~ op_strict_implies ),
inference(copy,[status(thm)],[c_196]) ).
cnf(c_198,plain,
( strict_equiv(A,B) = and(strict_implies(A,B),strict_implies(B,A))
| ~ op_strict_equiv ),
inference(clausify,[status(thm)],[op_strict_equiv]) ).
cnf(c_199,plain,
( and(strict_implies(A,B),strict_implies(B,A)) = strict_equiv(A,B)
| ~ op_strict_equiv ),
inference(copy,[status(thm)],[c_198]) ).
fof(km4b_axiom_M,axiom,
axiom_M,
file('theBenchmark.p',km4b_axiom_M) ).
cnf(c_203,plain,
axiom_M,
inference(clausify,[status(thm)],[km4b_axiom_M]) ).
fof(s1_0_op_strict_implies,axiom,
op_strict_implies,
file('theBenchmark.p',s1_0_op_strict_implies) ).
cnf(c_207,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_208,plain,
op_strict_equiv,
inference(clausify,[status(thm)],[s1_0_op_strict_equiv]) ).
cnf(c_209,negated_conjecture,
~ substitution_strict_equiv,
inference(clausify,[status(thm)],[s1_0_substitution_strict_equiv_neg]) ).
cnf(c_212,plain,
and(implies(A,B),implies(B,A)) = equiv(A,B),
inference(resolve,[status(thm)],[c_124,c_121]) ).
cnf(c_213,plain,
( is_a_theorem(B)
| ~ is_a_theorem(implies(A,B))
| ~ is_a_theorem(A) ),
inference(resolve,[status(thm)],[c_125,c_60]) ).
cnf(c_218,plain,
is_a_theorem(implies(and(A,B),A)),
inference(resolve,[status(thm)],[c_130,c_75]) ).
cnf(c_219,plain,
is_a_theorem(implies(and(A,B),B)),
inference(resolve,[status(thm)],[c_131,c_77]) ).
cnf(c_220,plain,
is_a_theorem(implies(A,implies(B,and(A,B)))),
inference(resolve,[status(thm)],[c_132,c_79]) ).
cnf(c_227,plain,
( B = A
| ~ is_a_theorem(equiv(A,B)) ),
inference(resolve,[status(thm)],[c_139,c_64]) ).
cnf(c_232,plain,
is_a_theorem(implies(necessarily(A),A)),
inference(resolve,[status(thm)],[c_203,c_156]) ).
cnf(c_235,plain,
necessarily(implies(A,B)) = strict_implies(A,B),
inference(resolve,[status(thm)],[c_207,c_197]) ).
cnf(c_236,plain,
and(strict_implies(A,B),strict_implies(B,A)) = strict_equiv(A,B),
inference(resolve,[status(thm)],[c_208,c_199]) ).
cnf(c_237,negated_conjecture,
sK3 != sK2,
inference(resolve,[status(thm)],[c_209,c_153]) ).
cnf(c_238,negated_conjecture,
is_a_theorem(strict_equiv(sK2,sK3)),
inference(resolve,[status(thm)],[c_209,c_152]) ).
cnf(c_259,plain,
( adjunction
| is_a_theorem(A)
| ~ is_a_theorem(implies(sK1,A)) ),
inference(resolve,[status(thm)],[c_213,c_149]) ).
cnf(c_260,plain,
( adjunction
| is_a_theorem(A)
| ~ is_a_theorem(implies(sK0,A)) ),
inference(resolve,[status(thm)],[c_213,c_148]) ).
cnf(c_378,plain,
is_a_theorem(implies(strict_implies(A,B),implies(A,B))),
inference(paramod,[status(thm)],[c_235,c_232]) ).
cnf(c_380,plain,
is_a_theorem(implies(strict_equiv(A,B),strict_implies(A,B))),
inference(paramod,[status(thm)],[c_236,c_218]) ).
cnf(c_381,plain,
is_a_theorem(implies(strict_equiv(A,B),strict_implies(B,A))),
inference(paramod,[status(thm)],[c_236,c_219]) ).
cnf(c_688,plain,
( adjunction
| is_a_theorem(implies(A,and(sK0,A))) ),
inference(resolve,[status(thm)],[c_260,c_220]) ).
cnf(c_8546,plain,
( adjunction
| is_a_theorem(and(sK0,sK1))
| adjunction ),
inference(resolve,[status(thm)],[c_688,c_259]) ).
cnf(c_2908,plain,
( is_a_theorem(and(sK0,sK1))
| adjunction ),
inference(copy,[status(thm)],[c_8546]) ).
cnf(c_8547,plain,
( adjunction
| adjunction ),
inference(resolve,[status(thm)],[c_2908,c_150]) ).
cnf(c_2921,plain,
adjunction,
inference(copy,[status(thm)],[c_8547]) ).
cnf(c_4074,plain,
( is_a_theorem(and(A,B))
| ~ is_a_theorem(B)
| ~ is_a_theorem(A) ),
inference(resolve,[status(thm)],[c_2921,c_147]) ).
cnf(c_4371,plain,
( is_a_theorem(strict_implies(A,B))
| ~ is_a_theorem(strict_equiv(A,B)) ),
inference(resolve,[status(thm)],[c_380,c_213]) ).
cnf(c_4373,plain,
is_a_theorem(strict_implies(sK2,sK3)),
inference(resolve,[status(thm)],[c_4371,c_238]) ).
cnf(c_4385,plain,
( is_a_theorem(A)
| ~ is_a_theorem(implies(strict_implies(sK2,sK3),A)) ),
inference(resolve,[status(thm)],[c_4373,c_213]) ).
cnf(c_4443,plain,
( is_a_theorem(strict_implies(B,A))
| ~ is_a_theorem(strict_equiv(A,B)) ),
inference(resolve,[status(thm)],[c_381,c_213]) ).
cnf(c_4445,plain,
is_a_theorem(strict_implies(sK3,sK2)),
inference(resolve,[status(thm)],[c_4443,c_238]) ).
cnf(c_4457,plain,
( is_a_theorem(A)
| ~ is_a_theorem(implies(strict_implies(sK3,sK2),A)) ),
inference(resolve,[status(thm)],[c_4445,c_213]) ).
cnf(c_7821,plain,
is_a_theorem(implies(sK3,sK2)),
inference(resolve,[status(thm)],[c_378,c_4457]) ).
cnf(c_7824,plain,
is_a_theorem(implies(sK2,sK3)),
inference(resolve,[status(thm)],[c_378,c_4385]) ).
cnf(c_7858,plain,
( is_a_theorem(and(A,implies(sK3,sK2)))
| ~ is_a_theorem(A) ),
inference(resolve,[status(thm)],[c_7821,c_4074]) ).
cnf(c_8548,plain,
is_a_theorem(and(implies(sK2,sK3),implies(sK3,sK2))),
inference(resolve,[status(thm)],[c_7858,c_7824]) ).
cnf(c_8372,plain,
is_a_theorem(equiv(sK2,sK3)),
inference(paramod,[status(thm)],[c_212,c_8548]) ).
cnf(c_8549,plain,
sK3 = sK2,
inference(resolve,[status(thm)],[c_8372,c_227]) ).
cnf(c_8545,plain,
$false,
inference(resolve,[status(thm)],[c_237,c_8549]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL539+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.10/0.34 % Computer : n018.cluster.edu
% 0.10/0.34 % Model : x86_64 x86_64
% 0.10/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.34 % Memory : 8046.5625MB
% 0.10/0.34 % OS : Linux 6.8.0-71-generic
% 0.10/0.34 % CPULimit : 300
% 0.10/0.34 % WCLimit : 300
% 0.10/0.34 % DateTime : Fri Sep 25 22:44:50 UTC 2026
% 0.10/0.34 % CPUTime :
% 0.10/0.34 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/0.34 % Process 3029526 was started by sandbox2 on n018,
% 0.10/0.34 % Fri Sep 25 22:44:50 2026
% 0.10/0.34 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.10/0.36
% 0.10/0.36 % From the command line: assign(max_seconds, 300).
% 5.36/1.16
% 5.36/1.16 % SZS status Theorem for theBenchmark
% 5.36/1.16
% 5.36/1.16 % Proof 1 at 0.59 (+ 0.14) seconds.
% 5.36/1.16 % Length of proof is 70.
% 5.36/1.16 % Level of proof is 11.
% 5.36/1.16 % Maximum clause weight is 31.000.
% 5.36/1.16 % Given clauses 490.
% 5.36/1.16
% 5.36/1.16 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------