%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : LCL533+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/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:14 PM UTC 2026
% Result : Theorem 87.06s 11.59s
% Output : Proof 87.06s
% Verified :
% SZS Type : Refutation
% Derivation depth : 35
% Number of leaves : 35
% Syntax : Number of formulae : 242 ( 174 unt; 0 def)
% Number of atoms : 386 ( 142 equ)
% Maximal formula atoms : 8 ( 1 avg)
% Number of connectives : 239 ( 95 ~; 89 |; 35 &)
% ( 13 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 2 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 20 ( 18 usr; 18 prp; 0-2 aty)
% Number of functors : 35 ( 35 usr; 26 con; 0-4 aty)
% Number of variables : 284 ( 20 sgn 93 !; 24 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f87,conjecture,
axiom_m6,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s1_0_m6s3m9b_axiom_m6) ).
fof(f87_neg,negated_conjecture,
~ axiom_m6,
inference(negated_conjecture,[status(cth)],[f87]) ).
fof(f87_nnf,plain,
~ axiom_m6,
inference(nnf_transformation,[status(thm)],[f87_neg]) ).
fof(f87_sk,plain,
~ axiom_m6,
inference(skolemisation,[status(esa)],[f87_nnf]) ).
cnf(c145,plain,
~ axiom_m6,
inference(cnf_transformation,[status(esa)],[f87_sk]) ).
cnf(t0,plain,
false = axiom_m6,
inference(equality_encoding,[status(esa)],[c145]) ).
cnf(t841,plain,
axiom_m6 = false,
inference(orient,[status(thm)],[t0]) ).
fof(f67,axiom,
( axiom_m6
<=> ! [X] : is_a_theorem(strict_implies(X,possibly(X))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_m6) ).
fof(f67_nnf,plain,
( ( ? [X] : ~ is_a_theorem(strict_implies(X,possibly(X)))
| axiom_m6 )
& ( ! [X] : is_a_theorem(strict_implies(X,possibly(X)))
| ~ axiom_m6 ) ),
inference(nnf_transformation,[status(thm)],[f67]) ).
fof(f67_sk,plain,
! [X] :
( ( ~ is_a_theorem(strict_implies(sk87,possibly(sk87)))
| axiom_m6 )
& ( is_a_theorem(strict_implies(X,possibly(X)))
| ~ axiom_m6 ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk87])],[f67_nnf]) ).
cnf(c121,plain,
( ~ is_a_theorem(strict_implies(sk87,possibly(sk87)))
| axiom_m6 ),
inference(cnf_transformation,[status(esa)],[f67_sk]) ).
cnf(t147,plain,
ifeq(is_a_theorem(strict_implies(sk87,possibly(sk87))),true,axiom_m6,true) = true,
inference(equality_encoding,[status(esa)],[c121]) ).
cnf(t349,plain,
ifeq(is_a_theorem(strict_implies(sk87,possibly(sk87))),true,axiom_m6,true) = true,
inference(orient,[status(thm)],[t147]) ).
cnf(t7130,plain,
ifeq(is_a_theorem(strict_implies(sk87,possibly(sk87))),true,false,true) = true,
inference(step,[status(thm)],[t349,t841]) ).
cnf(t843,plain,
ifeq(is_a_theorem(strict_implies(sk87,possibly(sk87))),true,false,true) = true,
inference(rw,[status(thm)],[t7130]) ).
fof(f49,axiom,
( necessitation
<=> ! [X] :
( is_a_theorem(X)
=> is_a_theorem(necessarily(X)) ) ),
file('/export/starexec/sandbox2/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(t208,plain,
ifeq(necessitation,true,ifeq(is_a_theorem(X1),true,is_a_theorem(necessarily(X1)),true),true) = true,
inference(equality_encoding,[status(esa)],[c78]) ).
cnf(t430,plain,
ifeq(necessitation,true,ifeq(is_a_theorem(X1),true,is_a_theorem(necessarily(X1)),true),true) = true,
inference(orient,[status(thm)],[t208]) ).
fof(f77,axiom,
necessitation,
file('/export/starexec/sandbox2/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(t18,plain,
true = necessitation,
inference(equality_encoding,[status(esa)],[c135]) ).
cnf(t847,plain,
necessitation = true,
inference(orient,[status(thm)],[t18]) ).
cnf(t7135,plain,
ifeq(true,true,ifeq(is_a_theorem(X1),true,is_a_theorem(necessarily(X1)),true),true) = true,
inference(step,[status(thm)],[t430,t847]) ).
cnf(t51,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t256,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t51]) ).
cnf(t7136,plain,
ifeq(is_a_theorem(X1),true,is_a_theorem(necessarily(X1)),true) = true,
inference(step,[status(thm)],[t7135,t256]) ).
cnf(t849,plain,
ifeq(is_a_theorem(X1),true,is_a_theorem(necessarily(X1)),true) = true,
inference(rw,[status(thm)],[t7136]) ).
cnf(t3184,plain,
ifeq(is_a_theorem(X1),true,is_a_theorem(necessarily(X1)),true) = true,
inference(orient,[status(thm)],[t849]) ).
fof(f7,axiom,
( and_2
<=> ! [X,Y] : is_a_theorem(implies(and(X,Y),Y)) ),
file('/export/starexec/sandbox2/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(t150,plain,
ifeq(and_2,true,is_a_theorem(implies(and(X1,X2),X2)),true) = true,
inference(equality_encoding,[status(esa)],[c17]) ).
cnf(t594,plain,
ifeq(and_2,true,is_a_theorem(implies(and(X1,X2),X2)),true) = true,
inference(orient,[status(thm)],[t150]) ).
fof(f40,axiom,
and_2,
file('/export/starexec/sandbox2/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(t2,plain,
true = and_2,
inference(equality_encoding,[status(esa)],[c69]) ).
cnf(t857,plain,
and_2 = true,
inference(orient,[status(thm)],[t2]) ).
cnf(t7140,plain,
ifeq(true,true,is_a_theorem(implies(and(X1,X2),X2)),true) = true,
inference(step,[status(thm)],[t594,t857]) ).
cnf(t7141,plain,
is_a_theorem(implies(and(X1,X2),X2)) = true,
inference(step,[status(thm)],[t7140,t256]) ).
cnf(t858,plain,
is_a_theorem(implies(and(X1,X2),X2)) = true,
inference(rw,[status(thm)],[t7141]) ).
cnf(t1293,plain,
is_a_theorem(implies(and(X1,X2),X2)) = true,
inference(orient,[status(thm)],[t858]) ).
fof(f28,axiom,
( op_implies_and
=> ! [X,Y] : implies(X,Y) = not(and(X,not(Y))) ),
file('/export/starexec/sandbox2/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/sandbox2/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(t99,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)],[t99]) ).
fof(f14,axiom,
( equivalence_3
<=> ! [X,Y] : is_a_theorem(implies(implies(X,Y),implies(implies(Y,X),equiv(X,Y)))) ),
file('/export/starexec/sandbox2/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/sandbox2/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]) ).
cnf(hi17,axiom,
ifeq(and_2,true,is_a_theorem(implies(and(X0,X1),X1)),true) = true,
inference(equality_encoding,[status(esa)],[c17]) ).
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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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(t35,plain,
and(X1,X1) = X1,
inference(hyper_resolution,[status(thm)],[hi4,hi77,h5081]) ).
cnf(t262,plain,
and(X1,X1) = X1,
inference(orient,[status(thm)],[t35]) ).
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/sandbox2/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/sandbox2/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(t141,plain,
not(and(not(X1),not(X2))) = or(X1,X2),
inference(hyper_resolution,[status(thm)],[hi55,hi60]) ).
cnf(t7084,plain,
implies(not(X1),X2) = or(X1,X2),
inference(step,[status(thm)],[t141,t265]) ).
cnf(t704,plain,
implies(not(X1),X2) = or(X1,X2),
inference(orient,[status(thm)],[t7084]) ).
cnf(t7174,plain,
or(X1,X1) = not(not(X1)),
inference(step,[status(thm)],[t266,t704]) ).
fof(f10,axiom,
( or_2
<=> ! [X,Y] : is_a_theorem(implies(Y,or(X,Y))) ),
file('/export/starexec/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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(t36,plain,
or(X1,X1) = X1,
inference(hyper_resolution,[status(thm)],[hi4,hi77,h4896]) ).
cnf(t259,plain,
or(X1,X1) = X1,
inference(orient,[status(thm)],[t36]) ).
cnf(t7175,plain,
X1 = not(not(X1)),
inference(step,[status(thm)],[t7174,t259]) ).
cnf(t916,plain,
not(not(X1)) = X1,
inference(orient,[status(thm)],[t7175]) ).
cnf(t917,plain,
and(X1,not(X2)) = not(implies(X1,X2)),
inference(cp,[status(thm)],[t916,t265]) ).
cnf(t1119,plain,
not(implies(X1,X2)) = and(X1,not(X2)),
inference(orient,[status(thm)],[t917]) ).
cnf(t919,plain,
or(not(X1),X2) = implies(X1,X2),
inference(cp,[status(thm)],[t704,t916]) ).
cnf(t961,plain,
or(not(X1),X2) = implies(X1,X2),
inference(orient,[status(thm)],[t919]) ).
fof(f9,axiom,
( or_1
<=> ! [X,Y] : is_a_theorem(implies(X,or(X,Y))) ),
file('/export/starexec/sandbox2/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/sandbox2/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]) ).
fof(f54,axiom,
( axiom_M
<=> ! [X] : is_a_theorem(implies(necessarily(X),X)) ),
file('/export/starexec/sandbox2/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/sandbox2/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(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(t44,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)],[t44]) ).
cnf(t963,plain,
implies(X1,necessarily(not(X1))) = not(X1),
inference(cp,[status(thm)],[t961,t260]) ).
fof(f72,axiom,
( op_possibly
=> ! [X] : possibly(X) = not(necessarily(not(X))) ),
file('/export/starexec/sandbox2/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/sandbox2/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(t57,plain,
not(necessarily(not(X1))) = possibly(X1),
inference(hyper_resolution,[status(thm)],[hi130,hi134]) ).
cnf(t831,plain,
not(necessarily(not(X1))) = possibly(X1),
inference(orient,[status(thm)],[t57]) ).
cnf(t918,plain,
necessarily(not(X1)) = not(possibly(X1)),
inference(cp,[status(thm)],[t916,t831]) ).
cnf(t926,plain,
necessarily(not(X1)) = not(possibly(X1)),
inference(orient,[status(thm)],[t918]) ).
cnf(t7213,plain,
implies(X1,not(possibly(X1))) = not(X1),
inference(step,[status(thm)],[t963,t926]) ).
cnf(t1177,plain,
implies(X1,not(possibly(X1))) = not(X1),
inference(orient,[status(thm)],[t7213]) ).
cnf(t1178,plain,
and(X1,not(not(possibly(X1)))) = not(not(X1)),
inference(cp,[status(thm)],[t1119,t1177]) ).
cnf(t7214,plain,
and(X1,possibly(X1)) = not(not(X1)),
inference(step,[status(thm)],[t1178,t916]) ).
cnf(t7215,plain,
and(X1,possibly(X1)) = X1,
inference(step,[status(thm)],[t7214,t916]) ).
cnf(t1187,plain,
and(X1,possibly(X1)) = X1,
inference(orient,[status(thm)],[t7215]) ).
cnf(t1294,plain,
true = is_a_theorem(implies(X1,possibly(X1))),
inference(cp,[status(thm)],[t1293,t1187]) ).
cnf(t1302,plain,
is_a_theorem(implies(X1,possibly(X1))) = true,
inference(orient,[status(thm)],[t1294]) ).
cnf(t3196,plain,
true = ifeq(true,true,is_a_theorem(necessarily(implies(X1,possibly(X1)))),true),
inference(cp,[status(thm)],[t3184,t1302]) ).
cnf(t7262,plain,
true = is_a_theorem(necessarily(implies(X1,possibly(X1)))),
inference(step,[status(thm)],[t3196,t256]) ).
fof(f74,axiom,
( op_strict_implies
=> ! [X,Y] : strict_implies(X,Y) = necessarily(implies(X,Y)) ),
file('/export/starexec/sandbox2/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/sandbox2/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(t73,plain,
necessarily(implies(X1,X2)) = strict_implies(X1,X2),
inference(hyper_resolution,[status(thm)],[hi132,hi142]) ).
cnf(t800,plain,
necessarily(implies(X1,X2)) = strict_implies(X1,X2),
inference(orient,[status(thm)],[t73]) ).
cnf(t7263,plain,
true = is_a_theorem(strict_implies(X1,possibly(X1))),
inference(step,[status(thm)],[t7262,t800]) ).
cnf(t3230,plain,
is_a_theorem(strict_implies(X1,possibly(X1))) = true,
inference(orient,[status(thm)],[t7263]) ).
cnf(t7430,plain,
ifeq(true,true,false,true) = true,
inference(step,[status(thm)],[t843,t3230]) ).
cnf(t7431,plain,
false = true,
inference(step,[status(thm)],[t7430,t256]) ).
cnf(t7043,plain,
false = true,
inference(orient,[status(thm)],[t7431]) ).
cnf(t7432,plain,
axiom_m6 = true,
inference(step,[status(thm)],[t841,t7043]) ).
cnf(t7044,plain,
axiom_m6 = true,
inference(orient,[status(thm)],[t7432]) ).
cnf(goal_0,negated_conjecture,
true != axiom_m6,
inference(equality_encoding,[status(esa)],[c145]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t7044]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : LCL533+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% 0.00/0.06 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.14/0.43 % Computer : n016.cluster.edu
% 0.14/0.43 % Model : x86_64 x86_64
% 0.14/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.43 % Memory : 8046.5625MB
% 0.14/0.43 % OS : Linux 6.8.0-71-generic
% 0.14/0.43 % CPULimit : 300
% 0.14/0.43 % WCLimit : 300
% 0.14/0.43 % DateTime : Wed Sep 23 23:45:29 UTC 2026
% 0.14/0.43 % CPUTime :
% 0.14/0.43 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 87.06/11.59 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 87.06/11.59 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------