%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : LCL548+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 : n019.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:16 PM UTC 2026
% Result : Theorem 17.04s 13.16s
% Output : Proof 17.04s
% Verified :
% SZS Type : Refutation
% Derivation depth : 31
% Number of leaves : 37
% Syntax : Number of formulae : 260 ( 188 unt; 0 def)
% Number of atoms : 408 ( 157 equ)
% Maximal formula atoms : 8 ( 1 avg)
% Number of connectives : 246 ( 98 ~; 92 |; 35 &)
% ( 13 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 2 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 21 ( 19 usr; 19 prp; 0-2 aty)
% Number of functors : 34 ( 34 usr; 25 con; 0-4 aty)
% Number of variables : 305 ( 13 sgn 96 !; 23 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f88,conjecture,
axiom_m9,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s1_0_m6s3m9b_axiom_m9) ).
fof(f88_neg,negated_conjecture,
~ axiom_m9,
inference(negated_conjecture,[status(cth)],[f88]) ).
fof(f88_nnf,plain,
~ axiom_m9,
inference(nnf_transformation,[status(thm)],[f88_neg]) ).
fof(f88_sk,plain,
~ axiom_m9,
inference(skolemisation,[status(esa)],[f88_nnf]) ).
cnf(c146,plain,
~ axiom_m9,
inference(cnf_transformation,[status(esa)],[f88_sk]) ).
cnf(t0,plain,
false = axiom_m9,
inference(equality_encoding,[status(esa)],[c146]) ).
cnf(t867,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/sandbox2/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(t345,plain,
ifeq(is_a_theorem(strict_implies(possibly(possibly(sk92)),possibly(sk92))),true,axiom_m9,true) = true,
inference(orient,[status(thm)],[t197]) ).
cnf(t112640,plain,
ifeq(is_a_theorem(strict_implies(possibly(possibly(sk92)),possibly(sk92))),true,false,true) = true,
inference(step,[status(thm)],[t345,t867]) ).
cnf(t869,plain,
ifeq(is_a_theorem(strict_implies(possibly(possibly(sk92)),possibly(sk92))),true,false,true) = true,
inference(rw,[status(thm)],[t112640]) ).
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(t113,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)],[t113]) ).
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]) ).
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(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/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(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(h138,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(h62,plain,
is_a_theorem(implies(V0,and(V0,V0))) = true,
inference(hyper_resolution,[status(thm)],[hi0,hi63,h9,h5]) ).
cnf(h5529,plain,
is_a_theorem(equiv(and(V0,V0),V0)) = true,
inference(hyper_resolution,[status(thm)],[hi0,hi63,h62,h138]) ).
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(t36,plain,
and(X1,X1) = X1,
inference(hyper_resolution,[status(thm)],[hi4,hi77,h5529]) ).
cnf(t259,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,t259]) ).
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(t149,plain,
not(and(not(X1),not(X2))) = or(X1,X2),
inference(hyper_resolution,[status(thm)],[hi55,hi60]) ).
cnf(t112603,plain,
implies(not(X1),X2) = or(X1,X2),
inference(step,[status(thm)],[t149,t265]) ).
cnf(t766,plain,
implies(not(X1),X2) = or(X1,X2),
inference(orient,[status(thm)],[t112603]) ).
cnf(t112702,plain,
or(X1,X1) = not(not(X1)),
inference(step,[status(thm)],[t266,t766]) ).
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(h135,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]) ).
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(h30,plain,
is_a_theorem(implies(V0,V0)) = true,
inference(hyper_resolution,[status(thm)],[hi0,hi63,h4,h5]) ).
cnf(h96,plain,
is_a_theorem(implies(implies(V0,V1),implies(or(V1,V0),V1))) = true,
inference(hyper_resolution,[status(thm)],[hi0,hi63,h30,h12]) ).
cnf(h2538,plain,
is_a_theorem(implies(or(V0,V0),V0)) = true,
inference(hyper_resolution,[status(thm)],[hi0,hi63,h30,h96]) ).
cnf(h5339,plain,
is_a_theorem(equiv(V0,or(V0,V0))) = true,
inference(hyper_resolution,[status(thm)],[hi0,hi63,h2538,h135]) ).
cnf(t37,plain,
or(X1,X1) = X1,
inference(hyper_resolution,[status(thm)],[hi4,hi77,h5339]) ).
cnf(t260,plain,
or(X1,X1) = X1,
inference(orient,[status(thm)],[t37]) ).
cnf(t112703,plain,
X1 = not(not(X1)),
inference(step,[status(thm)],[t112702,t260]) ).
cnf(t959,plain,
not(not(X1)) = X1,
inference(orient,[status(thm)],[t112703]) ).
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',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(h130,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/sandbox2/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/sandbox2/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(h5071,plain,
is_a_theorem(equiv(necessarily(necessarily(V0)),necessarily(V0))) = true,
inference(hyper_resolution,[status(thm)],[hi0,hi63,h19,h130]) ).
cnf(t44,plain,
necessarily(necessarily(X1)) = necessarily(X1),
inference(hyper_resolution,[status(thm)],[hi4,hi77,h5071]) ).
cnf(t834,plain,
necessarily(necessarily(X1)) = necessarily(X1),
inference(orient,[status(thm)],[t44]) ).
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',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(t61,plain,
not(necessarily(not(X1))) = possibly(X1),
inference(hyper_resolution,[status(thm)],[hi130,hi134]) ).
cnf(t857,plain,
not(necessarily(not(X1))) = possibly(X1),
inference(orient,[status(thm)],[t61]) ).
cnf(t961,plain,
necessarily(not(X1)) = not(possibly(X1)),
inference(cp,[status(thm)],[t959,t857]) ).
cnf(t969,plain,
necessarily(not(X1)) = not(possibly(X1)),
inference(orient,[status(thm)],[t961]) ).
cnf(t973,plain,
necessarily(not(X1)) = necessarily(not(possibly(X1))),
inference(cp,[status(thm)],[t834,t969]) ).
cnf(t112711,plain,
not(possibly(X1)) = necessarily(not(possibly(X1))),
inference(step,[status(thm)],[t973,t969]) ).
cnf(t112712,plain,
not(possibly(X1)) = not(possibly(possibly(X1))),
inference(step,[status(thm)],[t112711,t969]) ).
cnf(t1035,plain,
not(possibly(possibly(X1))) = not(possibly(X1)),
inference(orient,[status(thm)],[t112712]) ).
cnf(t1038,plain,
possibly(possibly(X1)) = not(not(possibly(X1))),
inference(cp,[status(thm)],[t959,t1035]) ).
cnf(t112713,plain,
possibly(possibly(X1)) = possibly(X1),
inference(step,[status(thm)],[t1038,t959]) ).
cnf(t1044,plain,
possibly(possibly(X1)) = possibly(X1),
inference(orient,[status(thm)],[t112713]) ).
cnf(t113318,plain,
ifeq(is_a_theorem(strict_implies(possibly(sk92),possibly(sk92))),true,false,true) = true,
inference(step,[status(thm)],[t869,t1044]) ).
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(f85,axiom,
op_strict_implies,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s1_0_op_strict_implies) ).
fof(f85_nnf,plain,
op_strict_implies,
inference(nnf_transformation,[status(thm)],[f85]) ).
cnf(c143,plain,
op_strict_implies,
inference(cnf_transformation,[status(esa)],[f85_nnf]) ).
cnf(hi143,axiom,
op_strict_implies = true,
inference(equality_encoding,[status(esa)],[c143]) ).
cnf(t79,plain,
necessarily(implies(X1,X2)) = strict_implies(X1,X2),
inference(hyper_resolution,[status(thm)],[hi132,hi143]) ).
cnf(t843,plain,
necessarily(implies(X1,X2)) = strict_implies(X1,X2),
inference(orient,[status(thm)],[t79]) ).
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(t939,plain,
substitution_of_equivalents = true,
inference(orient,[status(thm)],[t35]) ).
cnf(t112693,plain,
ifeq(true,true,ifeq(is_a_theorem(equiv(X1,X2)),true,X1,X2),X2) = X2,
inference(step,[status(thm)],[t257,t939]) ).
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(t112694,plain,
ifeq(is_a_theorem(equiv(X1,X2)),true,X1,X2) = X2,
inference(step,[status(thm)],[t112693,t256]) ).
cnf(t941,plain,
ifeq(is_a_theorem(equiv(X1,X2)),true,X1,X2) = X2,
inference(rw,[status(thm)],[t112694]) ).
cnf(t3925,plain,
ifeq(is_a_theorem(equiv(X1,X2)),true,X1,X2) = X2,
inference(orient,[status(thm)],[t941]) ).
cnf(h33,plain,
is_a_theorem(implies(V0,implies(V1,V1))) = true,
inference(hyper_resolution,[status(thm)],[hi0,hi63,h30,h4]) ).
cnf(h231,plain,
is_a_theorem(implies(implies(implies(V0,V0),V1),equiv(V1,implies(V0,V0)))) = true,
inference(hyper_resolution,[status(thm)],[hi0,hi63,h33,h15]) ).
cnf(h129,plain,
is_a_theorem(implies(implies(V0,V0),equiv(V0,V0))) = true,
inference(hyper_resolution,[status(thm)],[hi0,hi63,h30,h15]) ).
cnf(h5028,plain,
is_a_theorem(equiv(V0,V0)) = true,
inference(hyper_resolution,[status(thm)],[hi0,hi63,h30,h129]) ).
cnf(h5129,plain,
is_a_theorem(implies(V0,equiv(V1,V1))) = true,
inference(hyper_resolution,[status(thm)],[hi0,hi63,h5028,h4]) ).
cnf(t123,plain,
is_a_theorem(equiv(equiv(X1,X1),implies(X2,X2))) = true,
inference(hyper_resolution,[status(thm)],[hi0,hi63,h5129,h231]) ).
cnf(t296,plain,
is_a_theorem(equiv(equiv(X1,X1),implies(X2,X2))) = true,
inference(orient,[status(thm)],[t123]) ).
fof(f30,axiom,
( op_equiv
=> ! [X,Y] : equiv(X,Y) = and(implies(X,Y),implies(Y,X)) ),
file('/export/starexec/sandbox2/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/sandbox2/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(t150,plain,
and(implies(X1,X2),implies(X2,X1)) = equiv(X1,X2),
inference(hyper_resolution,[status(thm)],[hi59,hi62]) ).
cnf(t727,plain,
and(implies(X1,X2),implies(X2,X1)) = equiv(X1,X2),
inference(orient,[status(thm)],[t150]) ).
cnf(t728,plain,
equiv(X1,X1) = implies(X1,X1),
inference(cp,[status(thm)],[t727,t259]) ).
cnf(t943,plain,
equiv(X1,X1) = implies(X1,X1),
inference(orient,[status(thm)],[t728]) ).
cnf(t112695,plain,
is_a_theorem(equiv(implies(X1,X1),implies(X2,X2))) = true,
inference(step,[status(thm)],[t296,t943]) ).
cnf(t944,plain,
is_a_theorem(equiv(implies(X1,X1),implies(X2,X2))) = true,
inference(rw,[status(thm)],[t112695]) ).
cnf(t4349,plain,
is_a_theorem(equiv(implies(X1,X1),implies(X2,X2))) = true,
inference(orient,[status(thm)],[t944]) ).
cnf(t4362,plain,
implies(X1,X1) = ifeq(true,true,implies(X2,X2),implies(X1,X1)),
inference(cp,[status(thm)],[t3925,t4349]) ).
cnf(t112833,plain,
implies(X1,X1) = implies(X2,X2),
inference(step,[status(thm)],[t4362,t256]) ).
cnf(t4369,plain,
implies(X1,X1) = implies(X2,X2),
inference(orient,[status(thm)],[t112833]) ).
cnf(t4381,plain,
strict_implies(X1,X1) = necessarily(implies(X2,X2)),
inference(cp,[status(thm)],[t843,t4369]) ).
cnf(t112834,plain,
strict_implies(X1,X1) = strict_implies(X2,X2),
inference(step,[status(thm)],[t4381,t843]) ).
cnf(t4387,plain,
strict_implies(X1,X1) = strict_implies(X2,X2),
inference(orient,[status(thm)],[t112834]) ).
cnf(t113319,plain,
ifeq(is_a_theorem(strict_implies(true,true)),true,false,true) = true,
inference(step,[status(thm)],[t113318,t4387]) ).
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(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/sandbox2/benchmark/theBenchmark.p',km4b_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(t58,plain,
is_a_theorem(necessarily(implies(X1,X1))) = true,
inference(hyper_resolution,[status(thm)],[hi78,hi135,h30]) ).
cnf(t292,plain,
is_a_theorem(necessarily(implies(X1,X1))) = true,
inference(orient,[status(thm)],[t58]) ).
cnf(t112628,plain,
is_a_theorem(strict_implies(X1,X1)) = true,
inference(step,[status(thm)],[t292,t843]) ).
cnf(t852,plain,
is_a_theorem(strict_implies(X1,X1)) = true,
inference(rw,[status(thm)],[t112628]) ).
cnf(t949,plain,
is_a_theorem(strict_implies(X1,X1)) = true,
inference(orient,[status(thm)],[t852]) ).
cnf(t113320,plain,
ifeq(true,true,false,true) = true,
inference(step,[status(thm)],[t113319,t949]) ).
cnf(t113321,plain,
false = true,
inference(step,[status(thm)],[t113320,t256]) ).
cnf(t112570,plain,
false = true,
inference(orient,[status(thm)],[t113321]) ).
cnf(t113322,plain,
axiom_m9 = true,
inference(step,[status(thm)],[t867,t112570]) ).
cnf(t112571,plain,
axiom_m9 = true,
inference(orient,[status(thm)],[t113322]) ).
cnf(goal_0,negated_conjecture,
true != axiom_m9,
inference(equality_encoding,[status(esa)],[c146]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t112571]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL548+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.09/0.35 % Computer : n019.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:43:05 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.09/0.35 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 17.04/13.16 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 17.04/13.16 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------