%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : LCL537+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n011.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 : Fri Sep 25 02:02:15 PM UTC 2026
% Result : Theorem 71.12s 9.64s
% Output : Proof 71.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 32
% Number of leaves : 33
% Syntax : Number of formulae : 213 ( 149 unt; 0 def)
% Number of atoms : 347 ( 116 equ)
% Maximal formula atoms : 8 ( 1 avg)
% Number of connectives : 223 ( 89 ~; 83 |; 33 &)
% ( 13 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 2 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 19 ( 17 usr; 17 prp; 0-2 aty)
% Number of functors : 33 ( 33 usr; 25 con; 0-4 aty)
% Number of variables : 235 ( 11 sgn 84 !; 23 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f82,conjecture,
axiom_5,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',km5_axiom_5) ).
fof(f82_neg,negated_conjecture,
~ axiom_5,
inference(negated_conjecture,[status(cth)],[f82]) ).
fof(f82_nnf,plain,
~ axiom_5,
inference(nnf_transformation,[status(thm)],[f82_neg]) ).
fof(f82_sk,plain,
~ axiom_5,
inference(skolemisation,[status(esa)],[f82_nnf]) ).
cnf(c140,plain,
~ axiom_5,
inference(cnf_transformation,[status(esa)],[f82_sk]) ).
cnf(t0,plain,
false = axiom_5,
inference(equality_encoding,[status(esa)],[c140]) ).
cnf(t319,plain,
axiom_5 = false,
inference(orient,[status(thm)],[t0]) ).
fof(f57,axiom,
( axiom_5
<=> ! [X] : is_a_theorem(implies(possibly(X),necessarily(possibly(X)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_5) ).
fof(f57_nnf,plain,
( ( ? [X] : ~ is_a_theorem(implies(possibly(X),necessarily(possibly(X))))
| axiom_5 )
& ( ! [X] : is_a_theorem(implies(possibly(X),necessarily(possibly(X))))
| ~ axiom_5 ) ),
inference(nnf_transformation,[status(thm)],[f57]) ).
fof(f57_sk,plain,
! [X] :
( ( ~ is_a_theorem(implies(possibly(sk67),necessarily(possibly(sk67))))
| axiom_5 )
& ( is_a_theorem(implies(possibly(X),necessarily(possibly(X))))
| ~ axiom_5 ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk67])],[f57_nnf]) ).
cnf(c101,plain,
( ~ is_a_theorem(implies(possibly(sk67),necessarily(possibly(sk67))))
| axiom_5 ),
inference(cnf_transformation,[status(esa)],[f57_sk]) ).
cnf(t193,plain,
ifeq(is_a_theorem(implies(possibly(sk67),necessarily(possibly(sk67)))),true,axiom_5,true) = true,
inference(equality_encoding,[status(esa)],[c101]) ).
cnf(t1622,plain,
ifeq(is_a_theorem(implies(possibly(sk67),necessarily(possibly(sk67)))),true,false,true) = true,
inference(step,[status(thm)],[t193,t319]) ).
cnf(t418,plain,
ifeq(is_a_theorem(implies(possibly(sk67),necessarily(possibly(sk67)))),true,false,true) = true,
inference(orient,[status(thm)],[t1622]) ).
fof(f56,axiom,
( axiom_B
<=> ! [X] : is_a_theorem(implies(X,necessarily(possibly(X)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_B) ).
fof(f56_nnf,plain,
( ( ? [X] : ~ is_a_theorem(implies(X,necessarily(possibly(X))))
| axiom_B )
& ( ! [X] : is_a_theorem(implies(X,necessarily(possibly(X))))
| ~ axiom_B ) ),
inference(nnf_transformation,[status(thm)],[f56]) ).
fof(f56_sk,plain,
! [X] :
( ( ~ is_a_theorem(implies(sk66,necessarily(possibly(sk66))))
| axiom_B )
& ( is_a_theorem(implies(X,necessarily(possibly(X))))
| ~ axiom_B ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk66])],[f56_nnf]) ).
cnf(c98,plain,
( is_a_theorem(implies(X0,necessarily(possibly(X0))))
| ~ axiom_B ),
inference(cnf_transformation,[status(esa)],[f56_sk]) ).
cnf(t153,plain,
ifeq(axiom_B,true,is_a_theorem(implies(X1,necessarily(possibly(X1)))),true) = true,
inference(equality_encoding,[status(esa)],[c98]) ).
cnf(t715,plain,
ifeq(axiom_B,true,is_a_theorem(implies(X1,necessarily(possibly(X1)))),true) = true,
inference(orient,[status(thm)],[t153]) ).
fof(f81,axiom,
axiom_B,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',km4b_axiom_B) ).
fof(f81_nnf,plain,
axiom_B,
inference(nnf_transformation,[status(thm)],[f81]) ).
cnf(c139,plain,
axiom_B,
inference(cnf_transformation,[status(esa)],[f81_nnf]) ).
cnf(t5,plain,
true = axiom_B,
inference(equality_encoding,[status(esa)],[c139]) ).
cnf(t863,plain,
axiom_B = true,
inference(orient,[status(thm)],[t5]) ).
cnf(t1652,plain,
ifeq(true,true,is_a_theorem(implies(X1,necessarily(possibly(X1)))),true) = true,
inference(step,[status(thm)],[t715,t863]) ).
cnf(t46,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t256,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t46]) ).
cnf(t1653,plain,
is_a_theorem(implies(X1,necessarily(possibly(X1)))) = true,
inference(step,[status(thm)],[t1652,t256]) ).
cnf(t864,plain,
is_a_theorem(implies(X1,necessarily(possibly(X1)))) = true,
inference(rw,[status(thm)],[t1653]) ).
cnf(t1171,plain,
is_a_theorem(implies(X1,necessarily(possibly(X1)))) = true,
inference(orient,[status(thm)],[t864]) ).
fof(f28,axiom,
( op_implies_and
=> ! [X,Y] : implies(X,Y) = not(and(X,not(Y))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',op_implies_and) ).
fof(f28_nnf,plain,
( ! [X,Y] : implies(X,Y) = not(and(X,not(Y)))
| ~ op_implies_and ),
inference(nnf_transformation,[status(thm)],[f28]) ).
fof(f28_sk,plain,
! [X,Y] :
( implies(X,Y) = not(and(X,not(Y)))
| ~ op_implies_and ),
inference(skolemisation,[status(esa)],[f28_nnf]) ).
cnf(c57,plain,
( implies(X0,X1) = not(and(X0,not(X1)))
| ~ op_implies_and ),
inference(cnf_transformation,[status(esa)],[f28_sk]) ).
cnf(hi57,axiom,
ifeq(op_implies_and,true,implies(X0,X1),not(and(X0,not(X1)))) = not(and(X0,not(X1))),
inference(equality_encoding,[status(esa)],[c57]) ).
fof(f32,axiom,
op_implies_and,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hilbert_op_implies_and) ).
fof(f32_nnf,plain,
op_implies_and,
inference(nnf_transformation,[status(thm)],[f32]) ).
cnf(c61,plain,
op_implies_and,
inference(cnf_transformation,[status(esa)],[f32_nnf]) ).
cnf(hi61,axiom,
op_implies_and = true,
inference(equality_encoding,[status(esa)],[c61]) ).
cnf(t109,plain,
not(and(X1,not(X2))) = implies(X1,X2),
inference(hyper_resolution,[status(thm)],[hi57,hi61]) ).
cnf(t265,plain,
not(and(X1,not(X2))) = implies(X1,X2),
inference(orient,[status(thm)],[t109]) ).
fof(f14,axiom,
( equivalence_3
<=> ! [X,Y] : is_a_theorem(implies(implies(X,Y),implies(implies(Y,X),equiv(X,Y)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',equivalence_3) ).
fof(f14_nnf,plain,
( ( ? [X,Y] : ~ is_a_theorem(implies(implies(X,Y),implies(implies(Y,X),equiv(X,Y))))
| equivalence_3 )
& ( ! [X,Y] : is_a_theorem(implies(implies(X,Y),implies(implies(Y,X),equiv(X,Y))))
| ~ equivalence_3 ) ),
inference(nnf_transformation,[status(thm)],[f14]) ).
fof(f14_sk,plain,
! [X,Y] :
( ( ~ is_a_theorem(implies(implies(sk30,sk31),implies(implies(sk31,sk30),equiv(sk30,sk31))))
| equivalence_3 )
& ( is_a_theorem(implies(implies(X,Y),implies(implies(Y,X),equiv(X,Y))))
| ~ equivalence_3 ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk30,sk31])],[f14_nnf]) ).
cnf(c31,plain,
( is_a_theorem(implies(implies(X0,X1),implies(implies(X1,X0),equiv(X0,X1))))
| ~ equivalence_3 ),
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
cnf(hi31,axiom,
ifeq(equivalence_3,true,is_a_theorem(implies(implies(X0,X1),implies(implies(X1,X0),equiv(X0,X1)))),true) = true,
inference(equality_encoding,[status(esa)],[c31]) ).
fof(f47,axiom,
equivalence_3,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hilbert_equivalence_3) ).
fof(f47_nnf,plain,
equivalence_3,
inference(nnf_transformation,[status(thm)],[f47]) ).
cnf(c76,plain,
equivalence_3,
inference(cnf_transformation,[status(esa)],[f47_nnf]) ).
cnf(hi76,axiom,
equivalence_3 = true,
inference(equality_encoding,[status(esa)],[c76]) ).
cnf(h15,plain,
is_a_theorem(implies(implies(V0,V1),implies(implies(V1,V0),equiv(V0,V1)))) = true,
inference(hyper_resolution,[status(thm)],[hi31,hi76]) ).
fof(f7,axiom,
( and_2
<=> ! [X,Y] : is_a_theorem(implies(and(X,Y),Y)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',and_2) ).
fof(f7_nnf,plain,
( ( ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),Y))
| and_2 )
& ( ! [X,Y] : is_a_theorem(implies(and(X,Y),Y))
| ~ and_2 ) ),
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
! [X,Y] :
( ( ~ is_a_theorem(implies(and(sk15,sk16),sk16))
| and_2 )
& ( is_a_theorem(implies(and(X,Y),Y))
| ~ and_2 ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk15,sk16])],[f7_nnf]) ).
cnf(c17,plain,
( is_a_theorem(implies(and(X0,X1),X1))
| ~ and_2 ),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(hi17,axiom,
ifeq(and_2,true,is_a_theorem(implies(and(X0,X1),X1)),true) = true,
inference(equality_encoding,[status(esa)],[c17]) ).
fof(f40,axiom,
and_2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hilbert_and_2) ).
fof(f40_nnf,plain,
and_2,
inference(nnf_transformation,[status(thm)],[f40]) ).
cnf(c69,plain,
and_2,
inference(cnf_transformation,[status(esa)],[f40_nnf]) ).
cnf(hi69,axiom,
and_2 = true,
inference(equality_encoding,[status(esa)],[c69]) ).
cnf(h8,plain,
is_a_theorem(implies(and(V0,V1),V1)) = true,
inference(hyper_resolution,[status(thm)],[hi17,hi69]) ).
fof(f0,axiom,
( modus_ponens
<=> ! [X,Y] :
( ( is_a_theorem(implies(X,Y))
& is_a_theorem(X) )
=> is_a_theorem(Y) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',modus_ponens) ).
fof(f0_nnf,plain,
( ( ? [X,Y] :
( ~ is_a_theorem(Y)
& is_a_theorem(implies(X,Y))
& is_a_theorem(X) )
| modus_ponens )
& ( ! [X,Y] :
( is_a_theorem(Y)
| ~ is_a_theorem(implies(X,Y))
| ~ is_a_theorem(X) )
| ~ modus_ponens ) ),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [X,Y] :
( ( ( ~ is_a_theorem(sk1)
& is_a_theorem(implies(sk0,sk1))
& is_a_theorem(sk0) )
| modus_ponens )
& ( is_a_theorem(Y)
| ~ is_a_theorem(implies(X,Y))
| ~ is_a_theorem(X)
| ~ modus_ponens ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0,sk1])],[f0_nnf]) ).
cnf(c0,plain,
( is_a_theorem(X1)
| ~ is_a_theorem(implies(X0,X1))
| ~ is_a_theorem(X0)
| ~ modus_ponens ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(hi0,axiom,
ifeq(modus_ponens,true,ifeq(is_a_theorem(X0),true,ifeq(is_a_theorem(implies(X0,X1)),true,is_a_theorem(X1),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c0]) ).
fof(f34,axiom,
modus_ponens,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hilbert_modus_ponens) ).
fof(f34_nnf,plain,
modus_ponens,
inference(nnf_transformation,[status(thm)],[f34]) ).
cnf(c63,plain,
modus_ponens,
inference(cnf_transformation,[status(esa)],[f34_nnf]) ).
cnf(hi63,axiom,
modus_ponens = true,
inference(equality_encoding,[status(esa)],[c63]) ).
cnf(h128,plain,
is_a_theorem(implies(implies(V0,and(V1,V0)),equiv(and(V1,V0),V0))) = true,
inference(hyper_resolution,[status(thm)],[hi0,hi63,h8,h15]) ).
fof(f4,axiom,
( implies_2
<=> ! [X,Y] : is_a_theorem(implies(implies(X,implies(X,Y)),implies(X,Y))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',implies_2) ).
fof(f4_nnf,plain,
( ( ? [X,Y] : ~ is_a_theorem(implies(implies(X,implies(X,Y)),implies(X,Y)))
| implies_2 )
& ( ! [X,Y] : is_a_theorem(implies(implies(X,implies(X,Y)),implies(X,Y)))
| ~ implies_2 ) ),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [X,Y] :
( ( ~ is_a_theorem(implies(implies(sk8,implies(sk8,sk9)),implies(sk8,sk9)))
| implies_2 )
& ( is_a_theorem(implies(implies(X,implies(X,Y)),implies(X,Y)))
| ~ implies_2 ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk8,sk9])],[f4_nnf]) ).
cnf(c11,plain,
( is_a_theorem(implies(implies(X0,implies(X0,X1)),implies(X0,X1)))
| ~ implies_2 ),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(hi11,axiom,
ifeq(implies_2,true,is_a_theorem(implies(implies(X0,implies(X0,X1)),implies(X0,X1))),true) = true,
inference(equality_encoding,[status(esa)],[c11]) ).
fof(f37,axiom,
implies_2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hilbert_implies_2) ).
fof(f37_nnf,plain,
implies_2,
inference(nnf_transformation,[status(thm)],[f37]) ).
cnf(c66,plain,
implies_2,
inference(cnf_transformation,[status(esa)],[f37_nnf]) ).
cnf(hi66,axiom,
implies_2 = true,
inference(equality_encoding,[status(esa)],[c66]) ).
cnf(h5,plain,
is_a_theorem(implies(implies(V0,implies(V0,V1)),implies(V0,V1))) = true,
inference(hyper_resolution,[status(thm)],[hi11,hi66]) ).
fof(f8,axiom,
( and_3
<=> ! [X,Y] : is_a_theorem(implies(X,implies(Y,and(X,Y)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',and_3) ).
fof(f8_nnf,plain,
( ( ? [X,Y] : ~ is_a_theorem(implies(X,implies(Y,and(X,Y))))
| and_3 )
& ( ! [X,Y] : is_a_theorem(implies(X,implies(Y,and(X,Y))))
| ~ and_3 ) ),
inference(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,plain,
! [X,Y] :
( ( ~ is_a_theorem(implies(sk17,implies(sk18,and(sk17,sk18))))
| and_3 )
& ( is_a_theorem(implies(X,implies(Y,and(X,Y))))
| ~ and_3 ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk17,sk18])],[f8_nnf]) ).
cnf(c19,plain,
( is_a_theorem(implies(X0,implies(X1,and(X0,X1))))
| ~ and_3 ),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(hi19,axiom,
ifeq(and_3,true,is_a_theorem(implies(X0,implies(X1,and(X0,X1)))),true) = true,
inference(equality_encoding,[status(esa)],[c19]) ).
fof(f41,axiom,
and_3,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hilbert_and_3) ).
fof(f41_nnf,plain,
and_3,
inference(nnf_transformation,[status(thm)],[f41]) ).
cnf(c70,plain,
and_3,
inference(cnf_transformation,[status(esa)],[f41_nnf]) ).
cnf(hi70,axiom,
and_3 = true,
inference(equality_encoding,[status(esa)],[c70]) ).
cnf(h9,plain,
is_a_theorem(implies(V0,implies(V1,and(V0,V1)))) = true,
inference(hyper_resolution,[status(thm)],[hi19,hi70]) ).
cnf(h56,plain,
is_a_theorem(implies(V0,and(V0,V0))) = true,
inference(hyper_resolution,[status(thm)],[hi0,hi63,h9,h5]) ).
cnf(h5046,plain,
is_a_theorem(equiv(and(V0,V0),V0)) = true,
inference(hyper_resolution,[status(thm)],[hi0,hi63,h56,h128]) ).
fof(f1,axiom,
( substitution_of_equivalents
<=> ! [X,Y] :
( is_a_theorem(equiv(X,Y))
=> X = Y ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',substitution_of_equivalents) ).
fof(f1_nnf,plain,
( ( ? [X,Y] :
( X != Y
& is_a_theorem(equiv(X,Y)) )
| substitution_of_equivalents )
& ( ! [X,Y] :
( X = Y
| ~ is_a_theorem(equiv(X,Y)) )
| ~ substitution_of_equivalents ) ),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [X,Y] :
( ( ( sk2 != sk3
& is_a_theorem(equiv(sk2,sk3)) )
| substitution_of_equivalents )
& ( X = Y
| ~ is_a_theorem(equiv(X,Y))
| ~ substitution_of_equivalents ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk2,sk3])],[f1_nnf]) ).
cnf(c4,plain,
( X0 = X1
| ~ is_a_theorem(equiv(X0,X1))
| ~ substitution_of_equivalents ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(hi4,axiom,
ifeq(substitution_of_equivalents,true,ifeq(is_a_theorem(equiv(X0,X1)),true,X0,X1),X1) = X1,
inference(equality_encoding,[status(esa)],[c4]) ).
fof(f48,axiom,
substitution_of_equivalents,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',use_substitution_of_equivalents) ).
fof(f48_nnf,plain,
substitution_of_equivalents,
inference(nnf_transformation,[status(thm)],[f48]) ).
cnf(c77,plain,
substitution_of_equivalents,
inference(cnf_transformation,[status(esa)],[f48_nnf]) ).
cnf(hi77,axiom,
substitution_of_equivalents = true,
inference(equality_encoding,[status(esa)],[c77]) ).
cnf(t30,plain,
and(X1,X1) = X1,
inference(hyper_resolution,[status(thm)],[hi4,hi77,h5046]) ).
cnf(t262,plain,
and(X1,X1) = X1,
inference(orient,[status(thm)],[t30]) ).
cnf(t266,plain,
implies(not(X1),X1) = not(not(X1)),
inference(cp,[status(thm)],[t265,t262]) ).
fof(f26,axiom,
( op_or
=> ! [X,Y] : or(X,Y) = not(and(not(X),not(Y))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',op_or) ).
fof(f26_nnf,plain,
( ! [X,Y] : or(X,Y) = not(and(not(X),not(Y)))
| ~ op_or ),
inference(nnf_transformation,[status(thm)],[f26]) ).
fof(f26_sk,plain,
! [X,Y] :
( or(X,Y) = not(and(not(X),not(Y)))
| ~ op_or ),
inference(skolemisation,[status(esa)],[f26_nnf]) ).
cnf(c55,plain,
( or(X0,X1) = not(and(not(X0),not(X1)))
| ~ op_or ),
inference(cnf_transformation,[status(esa)],[f26_sk]) ).
cnf(hi55,axiom,
ifeq(op_or,true,or(X0,X1),not(and(not(X0),not(X1)))) = not(and(not(X0),not(X1))),
inference(equality_encoding,[status(esa)],[c55]) ).
fof(f31,axiom,
op_or,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hilbert_op_or) ).
fof(f31_nnf,plain,
op_or,
inference(nnf_transformation,[status(thm)],[f31]) ).
cnf(c60,plain,
op_or,
inference(cnf_transformation,[status(esa)],[f31_nnf]) ).
cnf(hi60,axiom,
op_or = true,
inference(equality_encoding,[status(esa)],[c60]) ).
cnf(t145,plain,
not(and(not(X1),not(X2))) = or(X1,X2),
inference(hyper_resolution,[status(thm)],[hi55,hi60]) ).
cnf(t1593,plain,
implies(not(X1),X2) = or(X1,X2),
inference(step,[status(thm)],[t145,t265]) ).
cnf(t292,plain,
implies(not(X1),X2) = or(X1,X2),
inference(orient,[status(thm)],[t1593]) ).
cnf(t1697,plain,
or(X1,X1) = not(not(X1)),
inference(step,[status(thm)],[t266,t292]) ).
fof(f10,axiom,
( or_2
<=> ! [X,Y] : is_a_theorem(implies(Y,or(X,Y))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',or_2) ).
fof(f10_nnf,plain,
( ( ? [X,Y] : ~ is_a_theorem(implies(Y,or(X,Y)))
| or_2 )
& ( ! [X,Y] : is_a_theorem(implies(Y,or(X,Y)))
| ~ or_2 ) ),
inference(nnf_transformation,[status(thm)],[f10]) ).
fof(f10_sk,plain,
! [Y,X] :
( ( ~ is_a_theorem(implies(sk22,or(sk21,sk22)))
| or_2 )
& ( is_a_theorem(implies(Y,or(X,Y)))
| ~ or_2 ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk21,sk22])],[f10_nnf]) ).
cnf(c23,plain,
( is_a_theorem(implies(X1,or(X0,X1)))
| ~ or_2 ),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(hi23,axiom,
ifeq(or_2,true,is_a_theorem(implies(X0,or(X1,X0))),true) = true,
inference(equality_encoding,[status(esa)],[c23]) ).
fof(f43,axiom,
or_2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hilbert_or_2) ).
fof(f43_nnf,plain,
or_2,
inference(nnf_transformation,[status(thm)],[f43]) ).
cnf(c72,plain,
or_2,
inference(cnf_transformation,[status(esa)],[f43_nnf]) ).
cnf(hi72,axiom,
or_2 = true,
inference(equality_encoding,[status(esa)],[c72]) ).
cnf(h11,plain,
is_a_theorem(implies(V0,or(V1,V0))) = true,
inference(hyper_resolution,[status(thm)],[hi23,hi72]) ).
cnf(h125,plain,
is_a_theorem(implies(implies(or(V0,V1),V1),equiv(V1,or(V0,V1)))) = true,
inference(hyper_resolution,[status(thm)],[hi0,hi63,h11,h15]) ).
fof(f11,axiom,
( or_3
<=> ! [X,Y,Z] : is_a_theorem(implies(implies(X,Z),implies(implies(Y,Z),implies(or(X,Y),Z)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',or_3) ).
fof(f11_nnf,plain,
( ( ? [X,Y,Z] : ~ is_a_theorem(implies(implies(X,Z),implies(implies(Y,Z),implies(or(X,Y),Z))))
| or_3 )
& ( ! [X,Y,Z] : is_a_theorem(implies(implies(X,Z),implies(implies(Y,Z),implies(or(X,Y),Z))))
| ~ or_3 ) ),
inference(nnf_transformation,[status(thm)],[f11]) ).
fof(f11_sk,plain,
! [X,Z,Y] :
( ( ~ is_a_theorem(implies(implies(sk23,sk25),implies(implies(sk24,sk25),implies(or(sk23,sk24),sk25))))
| or_3 )
& ( is_a_theorem(implies(implies(X,Z),implies(implies(Y,Z),implies(or(X,Y),Z))))
| ~ or_3 ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk23,sk24,sk25])],[f11_nnf]) ).
cnf(c25,plain,
( is_a_theorem(implies(implies(X0,X2),implies(implies(X1,X2),implies(or(X0,X1),X2))))
| ~ or_3 ),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(hi25,axiom,
ifeq(or_3,true,is_a_theorem(implies(implies(X0,X1),implies(implies(X2,X1),implies(or(X0,X2),X1)))),true) = true,
inference(equality_encoding,[status(esa)],[c25]) ).
fof(f44,axiom,
or_3,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hilbert_or_3) ).
fof(f44_nnf,plain,
or_3,
inference(nnf_transformation,[status(thm)],[f44]) ).
cnf(c73,plain,
or_3,
inference(cnf_transformation,[status(esa)],[f44_nnf]) ).
cnf(hi73,axiom,
or_3 = true,
inference(equality_encoding,[status(esa)],[c73]) ).
cnf(h12,plain,
is_a_theorem(implies(implies(V0,V1),implies(implies(V2,V1),implies(or(V0,V2),V1)))) = true,
inference(hyper_resolution,[status(thm)],[hi25,hi73]) ).
cnf(h103,plain,
is_a_theorem(implies(implies(V0,V1),implies(or(V0,V0),V1))) = true,
inference(hyper_resolution,[status(thm)],[hi0,hi63,h12,h5]) ).
fof(f3,axiom,
( implies_1
<=> ! [X,Y] : is_a_theorem(implies(X,implies(Y,X))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',implies_1) ).
fof(f3_nnf,plain,
( ( ? [X,Y] : ~ is_a_theorem(implies(X,implies(Y,X)))
| implies_1 )
& ( ! [X,Y] : is_a_theorem(implies(X,implies(Y,X)))
| ~ implies_1 ) ),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [X,Y] :
( ( ~ is_a_theorem(implies(sk6,implies(sk7,sk6)))
| implies_1 )
& ( is_a_theorem(implies(X,implies(Y,X)))
| ~ implies_1 ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk6,sk7])],[f3_nnf]) ).
cnf(c9,plain,
( is_a_theorem(implies(X0,implies(X1,X0)))
| ~ implies_1 ),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(hi9,axiom,
ifeq(implies_1,true,is_a_theorem(implies(X0,implies(X1,X0))),true) = true,
inference(equality_encoding,[status(esa)],[c9]) ).
fof(f36,axiom,
implies_1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hilbert_implies_1) ).
fof(f36_nnf,plain,
implies_1,
inference(nnf_transformation,[status(thm)],[f36]) ).
cnf(c65,plain,
implies_1,
inference(cnf_transformation,[status(esa)],[f36_nnf]) ).
cnf(hi65,axiom,
implies_1 = true,
inference(equality_encoding,[status(esa)],[c65]) ).
cnf(h4,plain,
is_a_theorem(implies(V0,implies(V1,V0))) = true,
inference(hyper_resolution,[status(thm)],[hi9,hi65]) ).
cnf(h28,plain,
is_a_theorem(implies(V0,V0)) = true,
inference(hyper_resolution,[status(thm)],[hi0,hi63,h4,h5]) ).
cnf(h3445,plain,
is_a_theorem(implies(or(V0,V0),V0)) = true,
inference(hyper_resolution,[status(thm)],[hi0,hi63,h28,h103]) ).
cnf(h4861,plain,
is_a_theorem(equiv(V0,or(V0,V0))) = true,
inference(hyper_resolution,[status(thm)],[hi0,hi63,h3445,h125]) ).
cnf(t31,plain,
or(X1,X1) = X1,
inference(hyper_resolution,[status(thm)],[hi4,hi77,h4861]) ).
cnf(t259,plain,
or(X1,X1) = X1,
inference(orient,[status(thm)],[t31]) ).
cnf(t1698,plain,
X1 = not(not(X1)),
inference(step,[status(thm)],[t1697,t259]) ).
cnf(t913,plain,
not(not(X1)) = X1,
inference(orient,[status(thm)],[t1698]) ).
fof(f54,axiom,
( axiom_M
<=> ! [X] : is_a_theorem(implies(necessarily(X),X)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_M) ).
fof(f54_nnf,plain,
( ( ? [X] : ~ is_a_theorem(implies(necessarily(X),X))
| axiom_M )
& ( ! [X] : is_a_theorem(implies(necessarily(X),X))
| ~ axiom_M ) ),
inference(nnf_transformation,[status(thm)],[f54]) ).
fof(f54_sk,plain,
! [X] :
( ( ~ is_a_theorem(implies(necessarily(sk64),sk64))
| axiom_M )
& ( is_a_theorem(implies(necessarily(X),X))
| ~ axiom_M ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk64])],[f54_nnf]) ).
cnf(c94,plain,
( is_a_theorem(implies(necessarily(X0),X0))
| ~ axiom_M ),
inference(cnf_transformation,[status(esa)],[f54_sk]) ).
cnf(hi94,axiom,
ifeq(axiom_M,true,is_a_theorem(implies(necessarily(X0),X0)),true) = true,
inference(equality_encoding,[status(esa)],[c94]) ).
fof(f79,axiom,
axiom_M,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',km4b_axiom_M) ).
fof(f79_nnf,plain,
axiom_M,
inference(nnf_transformation,[status(thm)],[f79]) ).
cnf(c137,plain,
axiom_M,
inference(cnf_transformation,[status(esa)],[f79_nnf]) ).
cnf(hi137,axiom,
axiom_M = true,
inference(equality_encoding,[status(esa)],[c137]) ).
cnf(h18,plain,
is_a_theorem(implies(necessarily(V0),V0)) = true,
inference(hyper_resolution,[status(thm)],[hi94,hi137]) ).
cnf(h120,plain,
is_a_theorem(implies(implies(V0,necessarily(V0)),equiv(necessarily(V0),V0))) = true,
inference(hyper_resolution,[status(thm)],[hi0,hi63,h18,h15]) ).
fof(f55,axiom,
( axiom_4
<=> ! [X] : is_a_theorem(implies(necessarily(X),necessarily(necessarily(X)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_4) ).
fof(f55_nnf,plain,
( ( ? [X] : ~ is_a_theorem(implies(necessarily(X),necessarily(necessarily(X))))
| axiom_4 )
& ( ! [X] : is_a_theorem(implies(necessarily(X),necessarily(necessarily(X))))
| ~ axiom_4 ) ),
inference(nnf_transformation,[status(thm)],[f55]) ).
fof(f55_sk,plain,
! [X] :
( ( ~ is_a_theorem(implies(necessarily(sk65),necessarily(necessarily(sk65))))
| axiom_4 )
& ( is_a_theorem(implies(necessarily(X),necessarily(necessarily(X))))
| ~ axiom_4 ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk65])],[f55_nnf]) ).
cnf(c96,plain,
( is_a_theorem(implies(necessarily(X0),necessarily(necessarily(X0))))
| ~ axiom_4 ),
inference(cnf_transformation,[status(esa)],[f55_sk]) ).
cnf(hi96,axiom,
ifeq(axiom_4,true,is_a_theorem(implies(necessarily(X0),necessarily(necessarily(X0)))),true) = true,
inference(equality_encoding,[status(esa)],[c96]) ).
fof(f80,axiom,
axiom_4,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',km4b_axiom_4) ).
fof(f80_nnf,plain,
axiom_4,
inference(nnf_transformation,[status(thm)],[f80]) ).
cnf(c138,plain,
axiom_4,
inference(cnf_transformation,[status(esa)],[f80_nnf]) ).
cnf(hi138,axiom,
axiom_4 = true,
inference(equality_encoding,[status(esa)],[c138]) ).
cnf(h19,plain,
is_a_theorem(implies(necessarily(V0),necessarily(necessarily(V0)))) = true,
inference(hyper_resolution,[status(thm)],[hi96,hi138]) ).
cnf(h4614,plain,
is_a_theorem(equiv(necessarily(necessarily(V0)),necessarily(V0))) = true,
inference(hyper_resolution,[status(thm)],[hi0,hi63,h19,h120]) ).
cnf(t38,plain,
necessarily(necessarily(X1)) = necessarily(X1),
inference(hyper_resolution,[status(thm)],[hi4,hi77,h4614]) ).
cnf(t307,plain,
necessarily(necessarily(X1)) = necessarily(X1),
inference(orient,[status(thm)],[t38]) ).
fof(f72,axiom,
( op_possibly
=> ! [X] : possibly(X) = not(necessarily(not(X))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',op_possibly) ).
fof(f72_nnf,plain,
( ! [X] : possibly(X) = not(necessarily(not(X)))
| ~ op_possibly ),
inference(nnf_transformation,[status(thm)],[f72]) ).
fof(f72_sk,plain,
! [X] :
( possibly(X) = not(necessarily(not(X)))
| ~ op_possibly ),
inference(skolemisation,[status(esa)],[f72_nnf]) ).
cnf(c130,plain,
( possibly(X0) = not(necessarily(not(X0)))
| ~ op_possibly ),
inference(cnf_transformation,[status(esa)],[f72_sk]) ).
cnf(hi130,axiom,
ifeq(op_possibly,true,possibly(X0),not(necessarily(not(X0)))) = not(necessarily(not(X0))),
inference(equality_encoding,[status(esa)],[c130]) ).
fof(f76,axiom,
op_possibly,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',km4b_op_possibly) ).
fof(f76_nnf,plain,
op_possibly,
inference(nnf_transformation,[status(thm)],[f76]) ).
cnf(c134,plain,
op_possibly,
inference(cnf_transformation,[status(esa)],[f76_nnf]) ).
cnf(hi134,axiom,
op_possibly = true,
inference(equality_encoding,[status(esa)],[c134]) ).
cnf(t55,plain,
not(necessarily(not(X1))) = possibly(X1),
inference(hyper_resolution,[status(thm)],[hi130,hi134]) ).
cnf(t309,plain,
not(necessarily(not(X1))) = possibly(X1),
inference(orient,[status(thm)],[t55]) ).
cnf(t915,plain,
necessarily(not(X1)) = not(possibly(X1)),
inference(cp,[status(thm)],[t913,t309]) ).
cnf(t923,plain,
necessarily(not(X1)) = not(possibly(X1)),
inference(orient,[status(thm)],[t915]) ).
cnf(t927,plain,
necessarily(not(X1)) = necessarily(not(possibly(X1))),
inference(cp,[status(thm)],[t307,t923]) ).
cnf(t1705,plain,
not(possibly(X1)) = necessarily(not(possibly(X1))),
inference(step,[status(thm)],[t927,t923]) ).
cnf(t1706,plain,
not(possibly(X1)) = not(possibly(possibly(X1))),
inference(step,[status(thm)],[t1705,t923]) ).
cnf(t996,plain,
not(possibly(possibly(X1))) = not(possibly(X1)),
inference(orient,[status(thm)],[t1706]) ).
cnf(t999,plain,
possibly(possibly(X1)) = not(not(possibly(X1))),
inference(cp,[status(thm)],[t913,t996]) ).
cnf(t1707,plain,
possibly(possibly(X1)) = possibly(X1),
inference(step,[status(thm)],[t999,t913]) ).
cnf(t1005,plain,
possibly(possibly(X1)) = possibly(X1),
inference(orient,[status(thm)],[t1707]) ).
cnf(t1174,plain,
true = is_a_theorem(implies(possibly(X1),necessarily(possibly(X1)))),
inference(cp,[status(thm)],[t1171,t1005]) ).
cnf(t1575,plain,
is_a_theorem(implies(possibly(X1),necessarily(possibly(X1)))) = true,
inference(orient,[status(thm)],[t1174]) ).
cnf(t1735,plain,
ifeq(true,true,false,true) = true,
inference(step,[status(thm)],[t418,t1575]) ).
cnf(t1736,plain,
false = true,
inference(step,[status(thm)],[t1735,t256]) ).
cnf(t1583,plain,
false = true,
inference(rw,[status(thm)],[t1736]) ).
cnf(t1584,plain,
false = true,
inference(orient,[status(thm)],[t1583]) ).
cnf(t1737,plain,
axiom_5 = true,
inference(step,[status(thm)],[t319,t1584]) ).
cnf(t1585,plain,
axiom_5 = true,
inference(orient,[status(thm)],[t1737]) ).
cnf(goal_0,negated_conjecture,
true != axiom_5,
inference(equality_encoding,[status(esa)],[c140]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t1585]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL537+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/0.35 % Computer : n011.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 : Wed Sep 23 23:41:12 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 71.12/9.64 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 71.12/9.64 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------