%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : LCL535+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 : n016.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 84.87s 11.17s
% Output : Proof 84.87s
% Verified :
% SZS Type : Refutation
% Derivation depth : 42
% Number of leaves : 39
% Syntax : Number of formulae : 302 ( 226 unt; 0 def)
% Number of atoms : 458 ( 192 equ)
% Maximal formula atoms : 8 ( 1 avg)
% Number of connectives : 259 ( 103 ~; 97 |; 37 &)
% ( 14 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 2 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 22 ( 20 usr; 20 prp; 0-2 aty)
% Number of functors : 36 ( 36 usr; 27 con; 0-4 aty)
% Number of variables : 362 ( 16 sgn 102 !; 25 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f87,conjecture,
axiom_m9,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',s1_0_m6s3m9b_axiom_m9) ).
fof(f87_neg,negated_conjecture,
~ axiom_m9,
inference(negated_conjecture,[status(cth)],[f87]) ).
fof(f87_nnf,plain,
~ axiom_m9,
inference(nnf_transformation,[status(thm)],[f87_neg]) ).
fof(f87_sk,plain,
~ axiom_m9,
inference(skolemisation,[status(esa)],[f87_nnf]) ).
cnf(c145,plain,
~ axiom_m9,
inference(cnf_transformation,[status(esa)],[f87_sk]) ).
cnf(t0,plain,
false = axiom_m9,
inference(equality_encoding,[status(esa)],[c145]) ).
cnf(t847,plain,
axiom_m9 = false,
inference(orient,[status(thm)],[t0]) ).
fof(f70,axiom,
( axiom_m9
<=> ! [X] : is_a_theorem(strict_implies(possibly(possibly(X)),possibly(X))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_m9) ).
fof(f70_nnf,plain,
( ( ? [X] : ~ is_a_theorem(strict_implies(possibly(possibly(X)),possibly(X)))
| axiom_m9 )
& ( ! [X] : is_a_theorem(strict_implies(possibly(possibly(X)),possibly(X)))
| ~ axiom_m9 ) ),
inference(nnf_transformation,[status(thm)],[f70]) ).
fof(f70_sk,plain,
! [X] :
( ( ~ is_a_theorem(strict_implies(possibly(possibly(sk92)),possibly(sk92)))
| axiom_m9 )
& ( is_a_theorem(strict_implies(possibly(possibly(X)),possibly(X)))
| ~ axiom_m9 ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk92])],[f70_nnf]) ).
cnf(c127,plain,
( ~ is_a_theorem(strict_implies(possibly(possibly(sk92)),possibly(sk92)))
| axiom_m9 ),
inference(cnf_transformation,[status(esa)],[f70_sk]) ).
cnf(t197,plain,
ifeq(is_a_theorem(strict_implies(possibly(possibly(sk92)),possibly(sk92))),true,axiom_m9,true) = true,
inference(equality_encoding,[status(esa)],[c127]) ).
cnf(t346,plain,
ifeq(is_a_theorem(strict_implies(possibly(possibly(sk92)),possibly(sk92))),true,axiom_m9,true) = true,
inference(orient,[status(thm)],[t197]) ).
cnf(t78280,plain,
ifeq(is_a_theorem(strict_implies(possibly(possibly(sk92)),possibly(sk92))),true,false,true) = true,
inference(step,[status(thm)],[t346,t847]) ).
cnf(t849,plain,
ifeq(is_a_theorem(strict_implies(possibly(possibly(sk92)),possibly(sk92))),true,false,true) = true,
inference(rw,[status(thm)],[t78280]) ).
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(t101,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)],[t101]) ).
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(h129,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(h57,plain,
is_a_theorem(implies(V0,and(V0,V0))) = true,
inference(hyper_resolution,[status(thm)],[hi0,hi63,h9,h5]) ).
cnf(h5081,plain,
is_a_theorem(equiv(and(V0,V0),V0)) = true,
inference(hyper_resolution,[status(thm)],[hi0,hi63,h57,h129]) ).
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(t36,plain,
and(X1,X1) = X1,
inference(hyper_resolution,[status(thm)],[hi4,hi77,h5081]) ).
cnf(t262,plain,
and(X1,X1) = X1,
inference(orient,[status(thm)],[t36]) ).
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(t144,plain,
not(and(not(X1),not(X2))) = or(X1,X2),
inference(hyper_resolution,[status(thm)],[hi55,hi60]) ).
cnf(t78234,plain,
implies(not(X1),X2) = or(X1,X2),
inference(step,[status(thm)],[t144,t265]) ).
cnf(t708,plain,
implies(not(X1),X2) = or(X1,X2),
inference(orient,[status(thm)],[t78234]) ).
cnf(t78329,plain,
or(X1,X1) = not(not(X1)),
inference(step,[status(thm)],[t266,t708]) ).
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(h126,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(h104,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(h29,plain,
is_a_theorem(implies(V0,V0)) = true,
inference(hyper_resolution,[status(thm)],[hi0,hi63,h4,h5]) ).
cnf(h3329,plain,
is_a_theorem(implies(or(V0,V0),V0)) = true,
inference(hyper_resolution,[status(thm)],[hi0,hi63,h29,h104]) ).
cnf(h4896,plain,
is_a_theorem(equiv(V0,or(V0,V0))) = true,
inference(hyper_resolution,[status(thm)],[hi0,hi63,h3329,h126]) ).
cnf(t37,plain,
or(X1,X1) = X1,
inference(hyper_resolution,[status(thm)],[hi4,hi77,h4896]) ).
cnf(t259,plain,
or(X1,X1) = X1,
inference(orient,[status(thm)],[t37]) ).
cnf(t78330,plain,
X1 = not(not(X1)),
inference(step,[status(thm)],[t78329,t259]) ).
cnf(t927,plain,
not(not(X1)) = X1,
inference(orient,[status(thm)],[t78330]) ).
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',km5_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(t58,plain,
not(necessarily(not(X1))) = possibly(X1),
inference(hyper_resolution,[status(thm)],[hi130,hi134]) ).
cnf(t837,plain,
not(necessarily(not(X1))) = possibly(X1),
inference(orient,[status(thm)],[t58]) ).
cnf(t929,plain,
necessarily(not(X1)) = not(possibly(X1)),
inference(cp,[status(thm)],[t927,t837]) ).
cnf(t937,plain,
necessarily(not(X1)) = not(possibly(X1)),
inference(orient,[status(thm)],[t929]) ).
cnf(t938,plain,
not(possibly(not(X1))) = necessarily(X1),
inference(cp,[status(thm)],[t937,t927]) ).
cnf(t950,plain,
not(possibly(not(X1))) = necessarily(X1),
inference(orient,[status(thm)],[t938]) ).
cnf(t956,plain,
necessarily(possibly(not(X1))) = not(possibly(necessarily(X1))),
inference(cp,[status(thm)],[t950,t950]) ).
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',km5_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(h121,plain,
is_a_theorem(implies(implies(V0,necessarily(V0)),equiv(necessarily(V0),V0))) = true,
inference(hyper_resolution,[status(thm)],[hi0,hi63,h18,h15]) ).
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(c100,plain,
( is_a_theorem(implies(possibly(X0),necessarily(possibly(X0))))
| ~ axiom_5 ),
inference(cnf_transformation,[status(esa)],[f57_sk]) ).
cnf(hi100,axiom,
ifeq(axiom_5,true,is_a_theorem(implies(possibly(X0),necessarily(possibly(X0)))),true) = true,
inference(equality_encoding,[status(esa)],[c100]) ).
fof(f80,axiom,
axiom_5,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',km5_axiom_5) ).
fof(f80_nnf,plain,
axiom_5,
inference(nnf_transformation,[status(thm)],[f80]) ).
cnf(c138,plain,
axiom_5,
inference(cnf_transformation,[status(esa)],[f80_nnf]) ).
cnf(hi138,axiom,
axiom_5 = true,
inference(equality_encoding,[status(esa)],[c138]) ).
cnf(h19,plain,
is_a_theorem(implies(possibly(V0),necessarily(possibly(V0)))) = true,
inference(hyper_resolution,[status(thm)],[hi100,hi138]) ).
cnf(h4622,plain,
is_a_theorem(equiv(necessarily(possibly(V0)),possibly(V0))) = true,
inference(hyper_resolution,[status(thm)],[hi0,hi63,h19,h121]) ).
cnf(t44,plain,
necessarily(possibly(X1)) = possibly(X1),
inference(hyper_resolution,[status(thm)],[hi4,hi77,h4622]) ).
cnf(t824,plain,
necessarily(possibly(X1)) = possibly(X1),
inference(orient,[status(thm)],[t44]) ).
cnf(t78337,plain,
possibly(not(X1)) = not(possibly(necessarily(X1))),
inference(step,[status(thm)],[t956,t824]) ).
cnf(t1010,plain,
not(possibly(necessarily(X1))) = possibly(not(X1)),
inference(orient,[status(thm)],[t78337]) ).
cnf(t1016,plain,
possibly(necessarily(X1)) = not(possibly(not(X1))),
inference(cp,[status(thm)],[t927,t1010]) ).
cnf(t78338,plain,
possibly(necessarily(X1)) = necessarily(X1),
inference(step,[status(thm)],[t1016,t950]) ).
cnf(t1022,plain,
possibly(necessarily(X1)) = necessarily(X1),
inference(orient,[status(thm)],[t78338]) ).
cnf(t1025,plain,
necessarily(possibly(X1)) = possibly(possibly(X1)),
inference(cp,[status(thm)],[t1022,t824]) ).
cnf(t78339,plain,
possibly(X1) = possibly(possibly(X1)),
inference(step,[status(thm)],[t1025,t824]) ).
cnf(t1034,plain,
possibly(possibly(X1)) = possibly(X1),
inference(orient,[status(thm)],[t78339]) ).
cnf(t78904,plain,
ifeq(is_a_theorem(strict_implies(possibly(sk92),possibly(sk92))),true,false,true) = true,
inference(step,[status(thm)],[t849,t1034]) ).
cnf(t212,plain,
ifeq(substitution_of_equivalents,true,ifeq(is_a_theorem(equiv(X1,X2)),true,X1,X2),X2) = X2,
inference(equality_encoding,[status(esa)],[c4]) ).
cnf(t257,plain,
ifeq(substitution_of_equivalents,true,ifeq(is_a_theorem(equiv(X1,X2)),true,X1,X2),X2) = X2,
inference(orient,[status(thm)],[t212]) ).
cnf(t35,plain,
true = substitution_of_equivalents,
inference(equality_encoding,[status(esa)],[c77]) ).
cnf(t907,plain,
substitution_of_equivalents = true,
inference(orient,[status(thm)],[t35]) ).
cnf(t78321,plain,
ifeq(true,true,ifeq(is_a_theorem(equiv(X1,X2)),true,X1,X2),X2) = X2,
inference(step,[status(thm)],[t257,t907]) ).
cnf(t52,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t256,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t52]) ).
cnf(t78322,plain,
ifeq(is_a_theorem(equiv(X1,X2)),true,X1,X2) = X2,
inference(step,[status(thm)],[t78321,t256]) ).
cnf(t909,plain,
ifeq(is_a_theorem(equiv(X1,X2)),true,X1,X2) = X2,
inference(rw,[status(thm)],[t78322]) ).
cnf(t3579,plain,
ifeq(is_a_theorem(equiv(X1,X2)),true,X1,X2) = X2,
inference(orient,[status(thm)],[t909]) ).
cnf(h148,plain,
is_a_theorem(implies(V0,implies(V1,V1))) = true,
inference(hyper_resolution,[status(thm)],[hi0,hi63,h29,h4]) ).
cnf(h428,plain,
is_a_theorem(implies(implies(implies(V0,V0),V1),equiv(V1,implies(V0,V0)))) = true,
inference(hyper_resolution,[status(thm)],[hi0,hi63,h148,h15]) ).
cnf(h140,plain,
is_a_theorem(implies(implies(V0,V0),equiv(V0,V0))) = true,
inference(hyper_resolution,[status(thm)],[hi0,hi63,h15,h5]) ).
cnf(h6006,plain,
is_a_theorem(equiv(V0,V0)) = true,
inference(hyper_resolution,[status(thm)],[hi0,hi63,h29,h140]) ).
cnf(h6482,plain,
is_a_theorem(implies(V0,equiv(V1,V1))) = true,
inference(hyper_resolution,[status(thm)],[hi0,hi63,h6006,h4]) ).
cnf(t112,plain,
is_a_theorem(equiv(equiv(X1,X1),implies(X2,X2))) = true,
inference(hyper_resolution,[status(thm)],[hi0,hi63,h6482,h428]) ).
cnf(t303,plain,
is_a_theorem(equiv(equiv(X1,X1),implies(X2,X2))) = true,
inference(orient,[status(thm)],[t112]) ).
fof(f30,axiom,
( op_equiv
=> ! [X,Y] : equiv(X,Y) = and(implies(X,Y),implies(Y,X)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',op_equiv) ).
fof(f30_nnf,plain,
( ! [X,Y] : equiv(X,Y) = and(implies(X,Y),implies(Y,X))
| ~ op_equiv ),
inference(nnf_transformation,[status(thm)],[f30]) ).
fof(f30_sk,plain,
! [X,Y] :
( equiv(X,Y) = and(implies(X,Y),implies(Y,X))
| ~ op_equiv ),
inference(skolemisation,[status(esa)],[f30_nnf]) ).
cnf(c59,plain,
( equiv(X0,X1) = and(implies(X0,X1),implies(X1,X0))
| ~ op_equiv ),
inference(cnf_transformation,[status(esa)],[f30_sk]) ).
cnf(hi59,axiom,
ifeq(op_equiv,true,equiv(X0,X1),and(implies(X0,X1),implies(X1,X0))) = and(implies(X0,X1),implies(X1,X0)),
inference(equality_encoding,[status(esa)],[c59]) ).
fof(f33,axiom,
op_equiv,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hilbert_op_equiv) ).
fof(f33_nnf,plain,
op_equiv,
inference(nnf_transformation,[status(thm)],[f33]) ).
cnf(c62,plain,
op_equiv,
inference(cnf_transformation,[status(esa)],[f33_nnf]) ).
cnf(hi62,axiom,
op_equiv = true,
inference(equality_encoding,[status(esa)],[c62]) ).
cnf(t145,plain,
and(implies(X1,X2),implies(X2,X1)) = equiv(X1,X2),
inference(hyper_resolution,[status(thm)],[hi59,hi62]) ).
cnf(t768,plain,
and(implies(X1,X2),implies(X2,X1)) = equiv(X1,X2),
inference(orient,[status(thm)],[t145]) ).
cnf(t769,plain,
equiv(X1,X1) = implies(X1,X1),
inference(cp,[status(thm)],[t768,t262]) ).
cnf(t912,plain,
equiv(X1,X1) = implies(X1,X1),
inference(orient,[status(thm)],[t769]) ).
cnf(t78323,plain,
is_a_theorem(equiv(implies(X1,X1),implies(X2,X2))) = true,
inference(step,[status(thm)],[t303,t912]) ).
cnf(t913,plain,
is_a_theorem(equiv(implies(X1,X1),implies(X2,X2))) = true,
inference(rw,[status(thm)],[t78323]) ).
cnf(h146,plain,
is_a_theorem(implies(V0,and(implies(V1,V1),V0))) = true,
inference(hyper_resolution,[status(thm)],[hi0,hi63,h29,h9]) ).
cnf(t109,plain,
is_a_theorem(equiv(and(implies(X1,X1),X2),X2)) = true,
inference(hyper_resolution,[status(thm)],[hi0,hi63,h146,h129]) ).
cnf(t299,plain,
is_a_theorem(equiv(and(implies(X1,X1),X2),X2)) = true,
inference(orient,[status(thm)],[t109]) ).
cnf(t3580,plain,
X1 = ifeq(true,true,and(implies(X2,X2),X1),X1),
inference(cp,[status(thm)],[t3579,t299]) ).
cnf(t78444,plain,
X1 = and(implies(X2,X2),X1),
inference(step,[status(thm)],[t3580,t256]) ).
cnf(t3581,plain,
and(implies(X1,X1),X2) = X2,
inference(orient,[status(thm)],[t78444]) ).
cnf(t928,plain,
and(X1,not(X2)) = not(implies(X1,X2)),
inference(cp,[status(thm)],[t927,t265]) ).
cnf(t1131,plain,
not(implies(X1,X2)) = and(X1,not(X2)),
inference(orient,[status(thm)],[t928]) ).
cnf(t930,plain,
or(not(X1),X2) = implies(X1,X2),
inference(cp,[status(thm)],[t708,t927]) ).
cnf(t973,plain,
or(not(X1),X2) = implies(X1,X2),
inference(orient,[status(thm)],[t930]) ).
fof(f9,axiom,
( or_1
<=> ! [X,Y] : is_a_theorem(implies(X,or(X,Y))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',or_1) ).
fof(f9_nnf,plain,
( ( ? [X,Y] : ~ is_a_theorem(implies(X,or(X,Y)))
| or_1 )
& ( ! [X,Y] : is_a_theorem(implies(X,or(X,Y)))
| ~ or_1 ) ),
inference(nnf_transformation,[status(thm)],[f9]) ).
fof(f9_sk,plain,
! [X,Y] :
( ( ~ is_a_theorem(implies(sk19,or(sk19,sk20)))
| or_1 )
& ( is_a_theorem(implies(X,or(X,Y)))
| ~ or_1 ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk19,sk20])],[f9_nnf]) ).
cnf(c21,plain,
( is_a_theorem(implies(X0,or(X0,X1)))
| ~ or_1 ),
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
cnf(hi21,axiom,
ifeq(or_1,true,is_a_theorem(implies(X0,or(X0,X1))),true) = true,
inference(equality_encoding,[status(esa)],[c21]) ).
fof(f42,axiom,
or_1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hilbert_or_1) ).
fof(f42_nnf,plain,
or_1,
inference(nnf_transformation,[status(thm)],[f42]) ).
cnf(c71,plain,
or_1,
inference(cnf_transformation,[status(esa)],[f42_nnf]) ).
cnf(hi71,axiom,
or_1 = true,
inference(equality_encoding,[status(esa)],[c71]) ).
cnf(h10,plain,
is_a_theorem(implies(V0,or(V0,V1))) = true,
inference(hyper_resolution,[status(thm)],[hi21,hi71]) ).
cnf(h127,plain,
is_a_theorem(implies(implies(or(V0,V1),V0),equiv(V0,or(V0,V1)))) = true,
inference(hyper_resolution,[status(thm)],[hi0,hi63,h10,h15]) ).
cnf(h143,plain,
is_a_theorem(implies(implies(V0,V1),implies(or(V1,V0),V1))) = true,
inference(hyper_resolution,[status(thm)],[hi0,hi63,h29,h12]) ).
cnf(h6188,plain,
is_a_theorem(implies(or(V0,necessarily(V0)),V0)) = true,
inference(hyper_resolution,[status(thm)],[hi0,hi63,h18,h143]) ).
cnf(h14457,plain,
is_a_theorem(equiv(V0,or(V0,necessarily(V0)))) = true,
inference(hyper_resolution,[status(thm)],[hi0,hi63,h6188,h127]) ).
cnf(t45,plain,
or(X1,necessarily(X1)) = X1,
inference(hyper_resolution,[status(thm)],[hi4,hi77,h14457]) ).
cnf(t260,plain,
or(X1,necessarily(X1)) = X1,
inference(orient,[status(thm)],[t45]) ).
cnf(t975,plain,
implies(X1,necessarily(not(X1))) = not(X1),
inference(cp,[status(thm)],[t973,t260]) ).
cnf(t78364,plain,
implies(X1,not(possibly(X1))) = not(X1),
inference(step,[status(thm)],[t975,t937]) ).
cnf(t1189,plain,
implies(X1,not(possibly(X1))) = not(X1),
inference(orient,[status(thm)],[t78364]) ).
cnf(t1190,plain,
and(X1,not(not(possibly(X1)))) = not(not(X1)),
inference(cp,[status(thm)],[t1131,t1189]) ).
cnf(t78365,plain,
and(X1,possibly(X1)) = not(not(X1)),
inference(step,[status(thm)],[t1190,t927]) ).
cnf(t78366,plain,
and(X1,possibly(X1)) = X1,
inference(step,[status(thm)],[t78365,t927]) ).
cnf(t1198,plain,
and(X1,possibly(X1)) = X1,
inference(orient,[status(thm)],[t78366]) ).
cnf(t3582,plain,
possibly(implies(X1,X1)) = implies(X1,X1),
inference(cp,[status(thm)],[t3581,t1198]) ).
cnf(t3605,plain,
possibly(implies(X1,X1)) = implies(X1,X1),
inference(orient,[status(thm)],[t3582]) ).
cnf(t3615,plain,
possibly(implies(X1,X1)) = necessarily(implies(X1,X1)),
inference(cp,[status(thm)],[t824,t3605]) ).
cnf(t78454,plain,
implies(X1,X1) = necessarily(implies(X1,X1)),
inference(step,[status(thm)],[t3615,t3605]) ).
fof(f74,axiom,
( op_strict_implies
=> ! [X,Y] : strict_implies(X,Y) = necessarily(implies(X,Y)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',op_strict_implies) ).
fof(f74_nnf,plain,
( ! [X,Y] : strict_implies(X,Y) = necessarily(implies(X,Y))
| ~ op_strict_implies ),
inference(nnf_transformation,[status(thm)],[f74]) ).
fof(f74_sk,plain,
! [X,Y] :
( strict_implies(X,Y) = necessarily(implies(X,Y))
| ~ op_strict_implies ),
inference(skolemisation,[status(esa)],[f74_nnf]) ).
cnf(c132,plain,
( strict_implies(X0,X1) = necessarily(implies(X0,X1))
| ~ op_strict_implies ),
inference(cnf_transformation,[status(esa)],[f74_sk]) ).
cnf(hi132,axiom,
ifeq(op_strict_implies,true,strict_implies(X0,X1),necessarily(implies(X0,X1))) = necessarily(implies(X0,X1)),
inference(equality_encoding,[status(esa)],[c132]) ).
fof(f84,axiom,
op_strict_implies,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',s1_0_op_strict_implies) ).
fof(f84_nnf,plain,
op_strict_implies,
inference(nnf_transformation,[status(thm)],[f84]) ).
cnf(c142,plain,
op_strict_implies,
inference(cnf_transformation,[status(esa)],[f84_nnf]) ).
cnf(hi142,axiom,
op_strict_implies = true,
inference(equality_encoding,[status(esa)],[c142]) ).
cnf(t74,plain,
necessarily(implies(X1,X2)) = strict_implies(X1,X2),
inference(hyper_resolution,[status(thm)],[hi132,hi142]) ).
cnf(t805,plain,
necessarily(implies(X1,X2)) = strict_implies(X1,X2),
inference(orient,[status(thm)],[t74]) ).
cnf(t78455,plain,
implies(X1,X1) = strict_implies(X1,X1),
inference(step,[status(thm)],[t78454,t805]) ).
cnf(t3627,plain,
implies(X1,X1) = strict_implies(X1,X1),
inference(orient,[status(thm)],[t78455]) ).
cnf(t78485,plain,
is_a_theorem(equiv(strict_implies(X1,X1),implies(X2,X2))) = true,
inference(step,[status(thm)],[t913,t3627]) ).
cnf(t78486,plain,
is_a_theorem(equiv(strict_implies(X1,X1),strict_implies(X2,X2))) = true,
inference(step,[status(thm)],[t78485,t3627]) ).
cnf(t4166,plain,
is_a_theorem(equiv(strict_implies(X1,X1),strict_implies(X2,X2))) = true,
inference(orient,[status(thm)],[t78486]) ).
cnf(t4171,plain,
strict_implies(X1,X1) = ifeq(true,true,strict_implies(X2,X2),strict_implies(X1,X1)),
inference(cp,[status(thm)],[t3579,t4166]) ).
cnf(t78487,plain,
strict_implies(X1,X1) = strict_implies(X2,X2),
inference(step,[status(thm)],[t4171,t256]) ).
cnf(t4177,plain,
strict_implies(X1,X1) = strict_implies(X2,X2),
inference(orient,[status(thm)],[t78487]) ).
cnf(t78905,plain,
ifeq(is_a_theorem(strict_implies(true,true)),true,false,true) = true,
inference(step,[status(thm)],[t78904,t4177]) ).
fof(f49,axiom,
( necessitation
<=> ! [X] :
( is_a_theorem(X)
=> is_a_theorem(necessarily(X)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',necessitation) ).
fof(f49_nnf,plain,
( ( ? [X] :
( ~ is_a_theorem(necessarily(X))
& is_a_theorem(X) )
| necessitation )
& ( ! [X] :
( is_a_theorem(necessarily(X))
| ~ is_a_theorem(X) )
| ~ necessitation ) ),
inference(nnf_transformation,[status(thm)],[f49]) ).
fof(f49_sk,plain,
! [X] :
( ( ( ~ is_a_theorem(necessarily(sk55))
& is_a_theorem(sk55) )
| necessitation )
& ( is_a_theorem(necessarily(X))
| ~ is_a_theorem(X)
| ~ necessitation ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk55])],[f49_nnf]) ).
cnf(c78,plain,
( is_a_theorem(necessarily(X0))
| ~ is_a_theorem(X0)
| ~ necessitation ),
inference(cnf_transformation,[status(esa)],[f49_sk]) ).
cnf(hi78,axiom,
ifeq(necessitation,true,ifeq(is_a_theorem(X0),true,is_a_theorem(necessarily(X0)),true),true) = true,
inference(equality_encoding,[status(esa)],[c78]) ).
fof(f77,axiom,
necessitation,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',km5_necessitation) ).
fof(f77_nnf,plain,
necessitation,
inference(nnf_transformation,[status(thm)],[f77]) ).
cnf(c135,plain,
necessitation,
inference(cnf_transformation,[status(esa)],[f77_nnf]) ).
cnf(hi135,axiom,
necessitation = true,
inference(equality_encoding,[status(esa)],[c135]) ).
cnf(t57,plain,
is_a_theorem(necessarily(implies(X1,X1))) = true,
inference(hyper_resolution,[status(thm)],[hi78,hi135,h29]) ).
cnf(t297,plain,
is_a_theorem(necessarily(implies(X1,X1))) = true,
inference(orient,[status(thm)],[t57]) ).
cnf(t78259,plain,
is_a_theorem(strict_implies(X1,X1)) = true,
inference(step,[status(thm)],[t297,t805]) ).
cnf(t819,plain,
is_a_theorem(strict_implies(X1,X1)) = true,
inference(rw,[status(thm)],[t78259]) ).
cnf(t917,plain,
is_a_theorem(strict_implies(X1,X1)) = true,
inference(orient,[status(thm)],[t819]) ).
cnf(t78906,plain,
ifeq(true,true,false,true) = true,
inference(step,[status(thm)],[t78905,t917]) ).
cnf(t78907,plain,
false = true,
inference(step,[status(thm)],[t78906,t256]) ).
cnf(t78197,plain,
false = true,
inference(orient,[status(thm)],[t78907]) ).
cnf(t78908,plain,
axiom_m9 = true,
inference(step,[status(thm)],[t847,t78197]) ).
cnf(t78198,plain,
axiom_m9 = true,
inference(orient,[status(thm)],[t78908]) ).
cnf(goal_0,negated_conjecture,
true != axiom_m9,
inference(equality_encoding,[status(esa)],[c145]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t78198]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL535+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.10/0.36 % Computer : n016.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Wed Sep 23 23:45:29 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 84.87/11.17 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 84.87/11.17 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------