%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : LCL524+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n013.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 : Thu Sep 24 01:07:55 PM UTC 2026
% Result : Theorem 0.12s 0.62s
% Output : CNFRefutation 0.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 147
% Syntax : Number of formulae : 538 ( 74 unt; 91 def)
% Number of atoms : 1474 ( 43 equ)
% Maximal formula atoms : 16 ( 2 avg)
% Number of connectives : 1621 ( 685 ~; 732 |; 73 &)
% ( 123 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 4 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 126 ( 124 usr; 124 prp; 0-2 aty)
% Number of functors : 59 ( 59 usr; 52 con; 0-2 aty)
% Number of variables : 444 ( 390 !; 54 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,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') ).
fof(f2,axiom,
( substitution_of_equivalents
<=> ! [X,Y] :
( is_a_theorem(equiv(X,Y))
=> X = Y ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,axiom,
( modus_tollens
<=> ! [X,Y] : is_a_theorem(implies(implies(not(Y),not(X)),implies(X,Y))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,axiom,
( implies_1
<=> ! [X,Y] : is_a_theorem(implies(X,implies(Y,X))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,axiom,
( implies_2
<=> ! [X,Y] : is_a_theorem(implies(implies(X,implies(X,Y)),implies(X,Y))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,axiom,
( implies_3
<=> ! [X,Y,Z] : is_a_theorem(implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,axiom,
( and_1
<=> ! [X,Y] : is_a_theorem(implies(and(X,Y),X)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f8,axiom,
( and_2
<=> ! [X,Y] : is_a_theorem(implies(and(X,Y),Y)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9,axiom,
( and_3
<=> ! [X,Y] : is_a_theorem(implies(X,implies(Y,and(X,Y)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10,axiom,
( or_1
<=> ! [X,Y] : is_a_theorem(implies(X,or(X,Y))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f11,axiom,
( or_2
<=> ! [X,Y] : is_a_theorem(implies(Y,or(X,Y))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f12,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') ).
fof(f13,axiom,
( equivalence_1
<=> ! [X,Y] : is_a_theorem(implies(equiv(X,Y),implies(X,Y))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f14,axiom,
( equivalence_2
<=> ! [X,Y] : is_a_theorem(implies(equiv(X,Y),implies(Y,X))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f15,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') ).
fof(f16,axiom,
( kn1
<=> ! [P] : is_a_theorem(implies(P,and(P,P))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f17,axiom,
( kn2
<=> ! [P,Q] : is_a_theorem(implies(and(P,Q),P)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f19,axiom,
( cn1
<=> ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(implies(Q,R),implies(P,R)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f20,axiom,
( cn2
<=> ! [P,Q] : is_a_theorem(implies(P,implies(not(P),Q))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f21,axiom,
( cn3
<=> ! [P] : is_a_theorem(implies(implies(not(P),P),P)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f22,axiom,
( r1
<=> ! [P] : is_a_theorem(implies(or(P,P),P)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f23,axiom,
( r2
<=> ! [P,Q] : is_a_theorem(implies(Q,or(P,Q))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f27,axiom,
( op_or
=> ! [X,Y] : or(X,Y) = not(and(not(X),not(Y))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f29,axiom,
( op_implies_and
=> ! [X,Y] : implies(X,Y) = not(and(X,not(Y))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f31,axiom,
( op_equiv
=> ! [X,Y] : equiv(X,Y) = and(implies(X,Y),implies(Y,X)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f32,axiom,
op_or,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f33,axiom,
op_implies_and,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f34,axiom,
op_equiv,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f35,axiom,
modus_ponens,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f36,axiom,
modus_tollens,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f37,axiom,
implies_1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f38,axiom,
implies_2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f39,axiom,
implies_3,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f40,axiom,
and_1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f41,axiom,
and_2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f42,axiom,
and_3,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f43,axiom,
or_1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f44,axiom,
or_2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f45,axiom,
or_3,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f46,axiom,
equivalence_1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f47,axiom,
equivalence_2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f48,axiom,
equivalence_3,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f49,axiom,
substitution_of_equivalents,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f50,axiom,
( necessitation
<=> ! [X] :
( is_a_theorem(X)
=> is_a_theorem(necessarily(X)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f52,axiom,
( adjunction
<=> ! [X,Y] :
( ( is_a_theorem(Y)
& is_a_theorem(X) )
=> is_a_theorem(and(X,Y)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f54,axiom,
( axiom_K
<=> ! [X,Y] : is_a_theorem(implies(necessarily(implies(X,Y)),implies(necessarily(X),necessarily(Y)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f55,axiom,
( axiom_M
<=> ! [X] : is_a_theorem(implies(necessarily(X),X)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f57,axiom,
( axiom_B
<=> ! [X] : is_a_theorem(implies(X,necessarily(possibly(X)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f58,axiom,
( axiom_5
<=> ! [X] : is_a_theorem(implies(possibly(X),necessarily(possibly(X)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f73,axiom,
( op_possibly
=> ! [X] : possibly(X) = not(necessarily(not(X))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f77,axiom,
op_possibly,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f78,axiom,
necessitation,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f79,axiom,
axiom_K,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f80,axiom,
axiom_M,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f81,axiom,
axiom_5,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f82,conjecture,
axiom_B,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f83,negated_conjecture,
~ axiom_B,
inference(negated_conjecture,[status(cth)],[f82]) ).
fof(f84,plain,
( modus_ponens
<=> ! [X,Y] :
( is_a_theorem(Y)
| ~ is_a_theorem(implies(X,Y))
| ~ is_a_theorem(X) ) ),
inference(pre_NNF_transformation,[status(thm)],[f1]) ).
fof(f85,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)],[f84]) ).
fof(f86,plain,
( ( ? [Y] :
( ~ is_a_theorem(Y)
& ? [X] :
( is_a_theorem(implies(X,Y))
& is_a_theorem(X) ) )
| modus_ponens )
& ( ! [Y] :
( is_a_theorem(Y)
| ! [X] :
( ~ is_a_theorem(implies(X,Y))
| ~ is_a_theorem(X) ) )
| ~ modus_ponens ) ),
inference(miniscoping,[status(thm)],[f85]) ).
fof(f87,plain,
( ( ( ~ is_a_theorem(sK0_skl)
& is_a_theorem(implies(sK1_skl,sK0_skl))
& is_a_theorem(sK1_skl) )
| modus_ponens )
& ( ! [Y] :
( is_a_theorem(Y)
| ! [X] :
( ~ is_a_theorem(implies(X,Y))
| ~ is_a_theorem(X) ) )
| ~ modus_ponens ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(Y,sK0_skl),skolemize(X,sK1_skl)],[f86]) ).
fof(f88,plain,
! [X0,X1] :
( is_a_theorem(X1)
| ~ is_a_theorem(implies(X0,X1))
| ~ is_a_theorem(X0)
| ~ modus_ponens ),
inference(cnf_transformation,[status(thm)],[f87]) ).
fof(f92,plain,
( substitution_of_equivalents
<=> ! [X,Y] :
( X = Y
| ~ is_a_theorem(equiv(X,Y)) ) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f93,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)],[f92]) ).
fof(f94,plain,
( ( ( sK2_skl != sK3_skl
& is_a_theorem(equiv(sK2_skl,sK3_skl)) )
| substitution_of_equivalents )
& ( ! [X,Y] :
( X = Y
| ~ is_a_theorem(equiv(X,Y)) )
| ~ substitution_of_equivalents ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl,sK3_skl]),skolemize(X,sK2_skl),skolemize(Y,sK3_skl)],[f93]) ).
fof(f95,plain,
! [X0,X1] :
( X0 = X1
| ~ is_a_theorem(equiv(X0,X1))
| ~ substitution_of_equivalents ),
inference(cnf_transformation,[status(thm)],[f94]) ).
fof(f98,plain,
( ( ? [X,Y] : ~ is_a_theorem(implies(implies(not(Y),not(X)),implies(X,Y)))
| modus_tollens )
& ( ! [X,Y] : is_a_theorem(implies(implies(not(Y),not(X)),implies(X,Y)))
| ~ modus_tollens ) ),
inference(NNF_transformation,[status(thm)],[f3]) ).
fof(f99,plain,
( ( ~ is_a_theorem(implies(implies(not(sK5_skl),not(sK4_skl)),implies(sK4_skl,sK5_skl)))
| modus_tollens )
& ( ! [X,Y] : is_a_theorem(implies(implies(not(Y),not(X)),implies(X,Y)))
| ~ modus_tollens ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl,sK5_skl]),skolemize(X,sK4_skl),skolemize(Y,sK5_skl)],[f98]) ).
fof(f100,plain,
! [X0,X1] :
( is_a_theorem(implies(implies(not(X0),not(X1)),implies(X1,X0)))
| ~ modus_tollens ),
inference(cnf_transformation,[status(thm)],[f99]) ).
fof(f102,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)],[f4]) ).
fof(f103,plain,
( ( ~ is_a_theorem(implies(sK6_skl,implies(sK7_skl,sK6_skl)))
| implies_1 )
& ( ! [X,Y] : is_a_theorem(implies(X,implies(Y,X)))
| ~ implies_1 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6_skl,sK7_skl]),skolemize(X,sK6_skl),skolemize(Y,sK7_skl)],[f102]) ).
fof(f104,plain,
! [X0,X1] :
( is_a_theorem(implies(X0,implies(X1,X0)))
| ~ implies_1 ),
inference(cnf_transformation,[status(thm)],[f103]) ).
fof(f106,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)],[f5]) ).
fof(f107,plain,
( ( ~ is_a_theorem(implies(implies(sK8_skl,implies(sK8_skl,sK9_skl)),implies(sK8_skl,sK9_skl)))
| implies_2 )
& ( ! [X,Y] : is_a_theorem(implies(implies(X,implies(X,Y)),implies(X,Y)))
| ~ implies_2 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl,sK9_skl]),skolemize(X,sK8_skl),skolemize(Y,sK9_skl)],[f106]) ).
fof(f108,plain,
! [X0,X1] :
( is_a_theorem(implies(implies(X0,implies(X0,X1)),implies(X0,X1)))
| ~ implies_2 ),
inference(cnf_transformation,[status(thm)],[f107]) ).
fof(f110,plain,
( ( ? [X,Y,Z] : ~ is_a_theorem(implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z))))
| implies_3 )
& ( ! [X,Y,Z] : is_a_theorem(implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z))))
| ~ implies_3 ) ),
inference(NNF_transformation,[status(thm)],[f6]) ).
fof(f111,plain,
( ( ~ is_a_theorem(implies(implies(sK10_skl,sK11_skl),implies(implies(sK11_skl,sK12_skl),implies(sK10_skl,sK12_skl))))
| implies_3 )
& ( ! [X,Y,Z] : is_a_theorem(implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z))))
| ~ implies_3 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl,sK11_skl,sK12_skl]),skolemize(X,sK10_skl),skolemize(Y,sK11_skl),skolemize(Z,sK12_skl)],[f110]) ).
fof(f112,plain,
! [X0,X1,X2] :
( is_a_theorem(implies(implies(X0,X1),implies(implies(X1,X2),implies(X0,X2))))
| ~ implies_3 ),
inference(cnf_transformation,[status(thm)],[f111]) ).
fof(f114,plain,
( ( ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),X))
| and_1 )
& ( ! [X,Y] : is_a_theorem(implies(and(X,Y),X))
| ~ and_1 ) ),
inference(NNF_transformation,[status(thm)],[f7]) ).
fof(f115,plain,
( ( ~ is_a_theorem(implies(and(sK13_skl,sK14_skl),sK13_skl))
| and_1 )
& ( ! [X,Y] : is_a_theorem(implies(and(X,Y),X))
| ~ and_1 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13_skl,sK14_skl]),skolemize(X,sK13_skl),skolemize(Y,sK14_skl)],[f114]) ).
fof(f116,plain,
! [X0,X1] :
( is_a_theorem(implies(and(X0,X1),X0))
| ~ and_1 ),
inference(cnf_transformation,[status(thm)],[f115]) ).
fof(f118,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)],[f8]) ).
fof(f119,plain,
( ( ~ is_a_theorem(implies(and(sK15_skl,sK16_skl),sK16_skl))
| and_2 )
& ( ! [X,Y] : is_a_theorem(implies(and(X,Y),Y))
| ~ and_2 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15_skl,sK16_skl]),skolemize(X,sK15_skl),skolemize(Y,sK16_skl)],[f118]) ).
fof(f120,plain,
! [X0,X1] :
( is_a_theorem(implies(and(X0,X1),X1))
| ~ and_2 ),
inference(cnf_transformation,[status(thm)],[f119]) ).
fof(f122,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)],[f9]) ).
fof(f123,plain,
( ( ~ is_a_theorem(implies(sK17_skl,implies(sK18_skl,and(sK17_skl,sK18_skl))))
| and_3 )
& ( ! [X,Y] : is_a_theorem(implies(X,implies(Y,and(X,Y))))
| ~ and_3 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK17_skl,sK18_skl]),skolemize(X,sK17_skl),skolemize(Y,sK18_skl)],[f122]) ).
fof(f124,plain,
! [X0,X1] :
( is_a_theorem(implies(X0,implies(X1,and(X0,X1))))
| ~ and_3 ),
inference(cnf_transformation,[status(thm)],[f123]) ).
fof(f126,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)],[f10]) ).
fof(f127,plain,
( ( ~ is_a_theorem(implies(sK19_skl,or(sK19_skl,sK20_skl)))
| or_1 )
& ( ! [X,Y] : is_a_theorem(implies(X,or(X,Y)))
| ~ or_1 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK19_skl,sK20_skl]),skolemize(X,sK19_skl),skolemize(Y,sK20_skl)],[f126]) ).
fof(f128,plain,
! [X0,X1] :
( is_a_theorem(implies(X0,or(X0,X1)))
| ~ or_1 ),
inference(cnf_transformation,[status(thm)],[f127]) ).
fof(f130,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)],[f11]) ).
fof(f131,plain,
( ( ~ is_a_theorem(implies(sK22_skl,or(sK21_skl,sK22_skl)))
| or_2 )
& ( ! [X,Y] : is_a_theorem(implies(Y,or(X,Y)))
| ~ or_2 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK21_skl,sK22_skl]),skolemize(X,sK21_skl),skolemize(Y,sK22_skl)],[f130]) ).
fof(f132,plain,
! [X0,X1] :
( is_a_theorem(implies(X0,or(X1,X0)))
| ~ or_2 ),
inference(cnf_transformation,[status(thm)],[f131]) ).
fof(f134,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)],[f12]) ).
fof(f135,plain,
( ( ~ is_a_theorem(implies(implies(sK23_skl,sK25_skl),implies(implies(sK24_skl,sK25_skl),implies(or(sK23_skl,sK24_skl),sK25_skl))))
| or_3 )
& ( ! [X,Y,Z] : is_a_theorem(implies(implies(X,Z),implies(implies(Y,Z),implies(or(X,Y),Z))))
| ~ or_3 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK23_skl,sK24_skl,sK25_skl]),skolemize(X,sK23_skl),skolemize(Y,sK24_skl),skolemize(Z,sK25_skl)],[f134]) ).
fof(f136,plain,
! [X0,X1,X2] :
( is_a_theorem(implies(implies(X0,X1),implies(implies(X2,X1),implies(or(X0,X2),X1))))
| ~ or_3 ),
inference(cnf_transformation,[status(thm)],[f135]) ).
fof(f138,plain,
( ( ? [X,Y] : ~ is_a_theorem(implies(equiv(X,Y),implies(X,Y)))
| equivalence_1 )
& ( ! [X,Y] : is_a_theorem(implies(equiv(X,Y),implies(X,Y)))
| ~ equivalence_1 ) ),
inference(NNF_transformation,[status(thm)],[f13]) ).
fof(f139,plain,
( ( ~ is_a_theorem(implies(equiv(sK26_skl,sK27_skl),implies(sK26_skl,sK27_skl)))
| equivalence_1 )
& ( ! [X,Y] : is_a_theorem(implies(equiv(X,Y),implies(X,Y)))
| ~ equivalence_1 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK26_skl,sK27_skl]),skolemize(X,sK26_skl),skolemize(Y,sK27_skl)],[f138]) ).
fof(f140,plain,
! [X0,X1] :
( is_a_theorem(implies(equiv(X0,X1),implies(X0,X1)))
| ~ equivalence_1 ),
inference(cnf_transformation,[status(thm)],[f139]) ).
fof(f142,plain,
( ( ? [X,Y] : ~ is_a_theorem(implies(equiv(X,Y),implies(Y,X)))
| equivalence_2 )
& ( ! [X,Y] : is_a_theorem(implies(equiv(X,Y),implies(Y,X)))
| ~ equivalence_2 ) ),
inference(NNF_transformation,[status(thm)],[f14]) ).
fof(f143,plain,
( ( ~ is_a_theorem(implies(equiv(sK28_skl,sK29_skl),implies(sK29_skl,sK28_skl)))
| equivalence_2 )
& ( ! [X,Y] : is_a_theorem(implies(equiv(X,Y),implies(Y,X)))
| ~ equivalence_2 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK28_skl,sK29_skl]),skolemize(X,sK28_skl),skolemize(Y,sK29_skl)],[f142]) ).
fof(f144,plain,
! [X0,X1] :
( is_a_theorem(implies(equiv(X0,X1),implies(X1,X0)))
| ~ equivalence_2 ),
inference(cnf_transformation,[status(thm)],[f143]) ).
fof(f146,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)],[f15]) ).
fof(f147,plain,
( ( ~ is_a_theorem(implies(implies(sK30_skl,sK31_skl),implies(implies(sK31_skl,sK30_skl),equiv(sK30_skl,sK31_skl))))
| equivalence_3 )
& ( ! [X,Y] : is_a_theorem(implies(implies(X,Y),implies(implies(Y,X),equiv(X,Y))))
| ~ equivalence_3 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK30_skl,sK31_skl]),skolemize(X,sK30_skl),skolemize(Y,sK31_skl)],[f146]) ).
fof(f148,plain,
! [X0,X1] :
( is_a_theorem(implies(implies(X0,X1),implies(implies(X1,X0),equiv(X0,X1))))
| ~ equivalence_3 ),
inference(cnf_transformation,[status(thm)],[f147]) ).
fof(f150,plain,
( ( ? [P] : ~ is_a_theorem(implies(P,and(P,P)))
| kn1 )
& ( ! [P] : is_a_theorem(implies(P,and(P,P)))
| ~ kn1 ) ),
inference(NNF_transformation,[status(thm)],[f16]) ).
fof(f151,plain,
( ( ~ is_a_theorem(implies(sK32_skl,and(sK32_skl,sK32_skl)))
| kn1 )
& ( ! [P] : is_a_theorem(implies(P,and(P,P)))
| ~ kn1 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK32_skl]),skolemize(P,sK32_skl)],[f150]) ).
fof(f153,plain,
( ~ is_a_theorem(implies(sK32_skl,and(sK32_skl,sK32_skl)))
| kn1 ),
inference(cnf_transformation,[status(thm)],[f151]) ).
fof(f154,plain,
( ( ? [P,Q] : ~ is_a_theorem(implies(and(P,Q),P))
| kn2 )
& ( ! [P,Q] : is_a_theorem(implies(and(P,Q),P))
| ~ kn2 ) ),
inference(NNF_transformation,[status(thm)],[f17]) ).
fof(f155,plain,
( ( ~ is_a_theorem(implies(and(sK33_skl,sK34_skl),sK33_skl))
| kn2 )
& ( ! [P,Q] : is_a_theorem(implies(and(P,Q),P))
| ~ kn2 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK33_skl,sK34_skl]),skolemize(P,sK33_skl),skolemize(Q,sK34_skl)],[f154]) ).
fof(f157,plain,
( ~ is_a_theorem(implies(and(sK33_skl,sK34_skl),sK33_skl))
| kn2 ),
inference(cnf_transformation,[status(thm)],[f155]) ).
fof(f162,plain,
( ( ? [P,Q,R] : ~ is_a_theorem(implies(implies(P,Q),implies(implies(Q,R),implies(P,R))))
| cn1 )
& ( ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(implies(Q,R),implies(P,R))))
| ~ cn1 ) ),
inference(NNF_transformation,[status(thm)],[f19]) ).
fof(f163,plain,
( ( ~ is_a_theorem(implies(implies(sK38_skl,sK39_skl),implies(implies(sK39_skl,sK40_skl),implies(sK38_skl,sK40_skl))))
| cn1 )
& ( ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(implies(Q,R),implies(P,R))))
| ~ cn1 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK38_skl,sK39_skl,sK40_skl]),skolemize(P,sK38_skl),skolemize(Q,sK39_skl),skolemize(R,sK40_skl)],[f162]) ).
fof(f165,plain,
( ~ is_a_theorem(implies(implies(sK38_skl,sK39_skl),implies(implies(sK39_skl,sK40_skl),implies(sK38_skl,sK40_skl))))
| cn1 ),
inference(cnf_transformation,[status(thm)],[f163]) ).
fof(f166,plain,
( ( ? [P,Q] : ~ is_a_theorem(implies(P,implies(not(P),Q)))
| cn2 )
& ( ! [P,Q] : is_a_theorem(implies(P,implies(not(P),Q)))
| ~ cn2 ) ),
inference(NNF_transformation,[status(thm)],[f20]) ).
fof(f167,plain,
( ( ~ is_a_theorem(implies(sK41_skl,implies(not(sK41_skl),sK42_skl)))
| cn2 )
& ( ! [P,Q] : is_a_theorem(implies(P,implies(not(P),Q)))
| ~ cn2 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK41_skl,sK42_skl]),skolemize(P,sK41_skl),skolemize(Q,sK42_skl)],[f166]) ).
fof(f168,plain,
! [X0,X1] :
( is_a_theorem(implies(X0,implies(not(X0),X1)))
| ~ cn2 ),
inference(cnf_transformation,[status(thm)],[f167]) ).
fof(f169,plain,
( ~ is_a_theorem(implies(sK41_skl,implies(not(sK41_skl),sK42_skl)))
| cn2 ),
inference(cnf_transformation,[status(thm)],[f167]) ).
fof(f170,plain,
( ( ? [P] : ~ is_a_theorem(implies(implies(not(P),P),P))
| cn3 )
& ( ! [P] : is_a_theorem(implies(implies(not(P),P),P))
| ~ cn3 ) ),
inference(NNF_transformation,[status(thm)],[f21]) ).
fof(f171,plain,
( ( ~ is_a_theorem(implies(implies(not(sK43_skl),sK43_skl),sK43_skl))
| cn3 )
& ( ! [P] : is_a_theorem(implies(implies(not(P),P),P))
| ~ cn3 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK43_skl]),skolemize(P,sK43_skl)],[f170]) ).
fof(f172,plain,
! [X0] :
( is_a_theorem(implies(implies(not(X0),X0),X0))
| ~ cn3 ),
inference(cnf_transformation,[status(thm)],[f171]) ).
fof(f173,plain,
( ~ is_a_theorem(implies(implies(not(sK43_skl),sK43_skl),sK43_skl))
| cn3 ),
inference(cnf_transformation,[status(thm)],[f171]) ).
fof(f174,plain,
( ( ? [P] : ~ is_a_theorem(implies(or(P,P),P))
| r1 )
& ( ! [P] : is_a_theorem(implies(or(P,P),P))
| ~ r1 ) ),
inference(NNF_transformation,[status(thm)],[f22]) ).
fof(f175,plain,
( ( ~ is_a_theorem(implies(or(sK44_skl,sK44_skl),sK44_skl))
| r1 )
& ( ! [P] : is_a_theorem(implies(or(P,P),P))
| ~ r1 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK44_skl]),skolemize(P,sK44_skl)],[f174]) ).
fof(f176,plain,
! [X0] :
( is_a_theorem(implies(or(X0,X0),X0))
| ~ r1 ),
inference(cnf_transformation,[status(thm)],[f175]) ).
fof(f177,plain,
( ~ is_a_theorem(implies(or(sK44_skl,sK44_skl),sK44_skl))
| r1 ),
inference(cnf_transformation,[status(thm)],[f175]) ).
fof(f178,plain,
( ( ? [P,Q] : ~ is_a_theorem(implies(Q,or(P,Q)))
| r2 )
& ( ! [P,Q] : is_a_theorem(implies(Q,or(P,Q)))
| ~ r2 ) ),
inference(NNF_transformation,[status(thm)],[f23]) ).
fof(f179,plain,
( ( ~ is_a_theorem(implies(sK46_skl,or(sK45_skl,sK46_skl)))
| r2 )
& ( ! [P,Q] : is_a_theorem(implies(Q,or(P,Q)))
| ~ r2 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK45_skl,sK46_skl]),skolemize(P,sK45_skl),skolemize(Q,sK46_skl)],[f178]) ).
fof(f181,plain,
( ~ is_a_theorem(implies(sK46_skl,or(sK45_skl,sK46_skl)))
| r2 ),
inference(cnf_transformation,[status(thm)],[f179]) ).
fof(f194,plain,
( ! [X,Y] : or(X,Y) = not(and(not(X),not(Y)))
| ~ op_or ),
inference(pre_NNF_transformation,[status(thm)],[f27]) ).
fof(f195,plain,
! [X0,X1] :
( or(X0,X1) = not(and(not(X0),not(X1)))
| ~ op_or ),
inference(cnf_transformation,[status(thm)],[f194]) ).
fof(f198,plain,
( ! [X,Y] : implies(X,Y) = not(and(X,not(Y)))
| ~ op_implies_and ),
inference(pre_NNF_transformation,[status(thm)],[f29]) ).
fof(f199,plain,
! [X0,X1] :
( implies(X0,X1) = not(and(X0,not(X1)))
| ~ op_implies_and ),
inference(cnf_transformation,[status(thm)],[f198]) ).
fof(f202,plain,
( ! [X,Y] : equiv(X,Y) = and(implies(X,Y),implies(Y,X))
| ~ op_equiv ),
inference(pre_NNF_transformation,[status(thm)],[f31]) ).
fof(f203,plain,
! [X0,X1] :
( equiv(X0,X1) = and(implies(X0,X1),implies(X1,X0))
| ~ op_equiv ),
inference(cnf_transformation,[status(thm)],[f202]) ).
fof(f204,plain,
op_or,
inference(cnf_transformation,[status(thm)],[f32]) ).
fof(f205,plain,
op_implies_and,
inference(cnf_transformation,[status(thm)],[f33]) ).
fof(f206,plain,
op_equiv,
inference(cnf_transformation,[status(thm)],[f34]) ).
fof(f207,plain,
modus_ponens,
inference(cnf_transformation,[status(thm)],[f35]) ).
fof(f208,plain,
modus_tollens,
inference(cnf_transformation,[status(thm)],[f36]) ).
fof(f209,plain,
implies_1,
inference(cnf_transformation,[status(thm)],[f37]) ).
fof(f210,plain,
implies_2,
inference(cnf_transformation,[status(thm)],[f38]) ).
fof(f211,plain,
implies_3,
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f212,plain,
and_1,
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f213,plain,
and_2,
inference(cnf_transformation,[status(thm)],[f41]) ).
fof(f214,plain,
and_3,
inference(cnf_transformation,[status(thm)],[f42]) ).
fof(f215,plain,
or_1,
inference(cnf_transformation,[status(thm)],[f43]) ).
fof(f216,plain,
or_2,
inference(cnf_transformation,[status(thm)],[f44]) ).
fof(f217,plain,
or_3,
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f218,plain,
equivalence_1,
inference(cnf_transformation,[status(thm)],[f46]) ).
fof(f219,plain,
equivalence_2,
inference(cnf_transformation,[status(thm)],[f47]) ).
fof(f220,plain,
equivalence_3,
inference(cnf_transformation,[status(thm)],[f48]) ).
fof(f221,plain,
substitution_of_equivalents,
inference(cnf_transformation,[status(thm)],[f49]) ).
fof(f222,plain,
( necessitation
<=> ! [X] :
( is_a_theorem(necessarily(X))
| ~ is_a_theorem(X) ) ),
inference(pre_NNF_transformation,[status(thm)],[f50]) ).
fof(f223,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)],[f222]) ).
fof(f224,plain,
( ( ( ~ is_a_theorem(necessarily(sK55_skl))
& is_a_theorem(sK55_skl) )
| necessitation )
& ( ! [X] :
( is_a_theorem(necessarily(X))
| ~ is_a_theorem(X) )
| ~ necessitation ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK55_skl]),skolemize(X,sK55_skl)],[f223]) ).
fof(f225,plain,
! [X0] :
( is_a_theorem(necessarily(X0))
| ~ is_a_theorem(X0)
| ~ necessitation ),
inference(cnf_transformation,[status(thm)],[f224]) ).
fof(f236,plain,
( adjunction
<=> ! [X,Y] :
( is_a_theorem(and(X,Y))
| ~ is_a_theorem(Y)
| ~ is_a_theorem(X) ) ),
inference(pre_NNF_transformation,[status(thm)],[f52]) ).
fof(f237,plain,
( ( ? [X,Y] :
( ~ is_a_theorem(and(X,Y))
& is_a_theorem(Y)
& is_a_theorem(X) )
| adjunction )
& ( ! [X,Y] :
( is_a_theorem(and(X,Y))
| ~ is_a_theorem(Y)
| ~ is_a_theorem(X) )
| ~ adjunction ) ),
inference(NNF_transformation,[status(thm)],[f236]) ).
fof(f238,plain,
( ( ( ~ is_a_theorem(and(sK58_skl,sK59_skl))
& is_a_theorem(sK59_skl)
& is_a_theorem(sK58_skl) )
| adjunction )
& ( ! [X,Y] :
( is_a_theorem(and(X,Y))
| ~ is_a_theorem(Y)
| ~ is_a_theorem(X) )
| ~ adjunction ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK58_skl,sK59_skl]),skolemize(X,sK58_skl),skolemize(Y,sK59_skl)],[f237]) ).
fof(f239,plain,
! [X0,X1] :
( is_a_theorem(and(X0,X1))
| ~ is_a_theorem(X1)
| ~ is_a_theorem(X0)
| ~ adjunction ),
inference(cnf_transformation,[status(thm)],[f238]) ).
fof(f240,plain,
( is_a_theorem(sK58_skl)
| adjunction ),
inference(cnf_transformation,[status(thm)],[f238]) ).
fof(f241,plain,
( is_a_theorem(sK59_skl)
| adjunction ),
inference(cnf_transformation,[status(thm)],[f238]) ).
fof(f242,plain,
( ~ is_a_theorem(and(sK58_skl,sK59_skl))
| adjunction ),
inference(cnf_transformation,[status(thm)],[f238]) ).
fof(f249,plain,
( ( ? [X,Y] : ~ is_a_theorem(implies(necessarily(implies(X,Y)),implies(necessarily(X),necessarily(Y))))
| axiom_K )
& ( ! [X,Y] : is_a_theorem(implies(necessarily(implies(X,Y)),implies(necessarily(X),necessarily(Y))))
| ~ axiom_K ) ),
inference(NNF_transformation,[status(thm)],[f54]) ).
fof(f250,plain,
( ( ~ is_a_theorem(implies(necessarily(implies(sK62_skl,sK63_skl)),implies(necessarily(sK62_skl),necessarily(sK63_skl))))
| axiom_K )
& ( ! [X,Y] : is_a_theorem(implies(necessarily(implies(X,Y)),implies(necessarily(X),necessarily(Y))))
| ~ axiom_K ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK62_skl,sK63_skl]),skolemize(X,sK62_skl),skolemize(Y,sK63_skl)],[f249]) ).
fof(f251,plain,
! [X0,X1] :
( is_a_theorem(implies(necessarily(implies(X0,X1)),implies(necessarily(X0),necessarily(X1))))
| ~ axiom_K ),
inference(cnf_transformation,[status(thm)],[f250]) ).
fof(f253,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)],[f55]) ).
fof(f254,plain,
( ( ~ is_a_theorem(implies(necessarily(sK64_skl),sK64_skl))
| axiom_M )
& ( ! [X] : is_a_theorem(implies(necessarily(X),X))
| ~ axiom_M ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK64_skl]),skolemize(X,sK64_skl)],[f253]) ).
fof(f255,plain,
! [X0] :
( is_a_theorem(implies(necessarily(X0),X0))
| ~ axiom_M ),
inference(cnf_transformation,[status(thm)],[f254]) ).
fof(f261,plain,
( ( ? [X] : ~ is_a_theorem(implies(X,necessarily(possibly(X))))
| axiom_B )
& ( ! [X] : is_a_theorem(implies(X,necessarily(possibly(X))))
| ~ axiom_B ) ),
inference(NNF_transformation,[status(thm)],[f57]) ).
fof(f262,plain,
( ( ~ is_a_theorem(implies(sK66_skl,necessarily(possibly(sK66_skl))))
| axiom_B )
& ( ! [X] : is_a_theorem(implies(X,necessarily(possibly(X))))
| ~ axiom_B ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK66_skl]),skolemize(X,sK66_skl)],[f261]) ).
fof(f264,plain,
( ~ is_a_theorem(implies(sK66_skl,necessarily(possibly(sK66_skl))))
| axiom_B ),
inference(cnf_transformation,[status(thm)],[f262]) ).
fof(f265,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)],[f58]) ).
fof(f266,plain,
( ( ~ is_a_theorem(implies(possibly(sK67_skl),necessarily(possibly(sK67_skl))))
| axiom_5 )
& ( ! [X] : is_a_theorem(implies(possibly(X),necessarily(possibly(X))))
| ~ axiom_5 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK67_skl]),skolemize(X,sK67_skl)],[f265]) ).
fof(f267,plain,
! [X0] :
( is_a_theorem(implies(possibly(X0),necessarily(possibly(X0))))
| ~ axiom_5 ),
inference(cnf_transformation,[status(thm)],[f266]) ).
fof(f325,plain,
( ! [X] : possibly(X) = not(necessarily(not(X)))
| ~ op_possibly ),
inference(pre_NNF_transformation,[status(thm)],[f73]) ).
fof(f326,plain,
! [X0] :
( possibly(X0) = not(necessarily(not(X0)))
| ~ op_possibly ),
inference(cnf_transformation,[status(thm)],[f325]) ).
fof(f333,plain,
op_possibly,
inference(cnf_transformation,[status(thm)],[f77]) ).
fof(f334,plain,
necessitation,
inference(cnf_transformation,[status(thm)],[f78]) ).
fof(f335,plain,
axiom_K,
inference(cnf_transformation,[status(thm)],[f79]) ).
fof(f336,plain,
axiom_M,
inference(cnf_transformation,[status(thm)],[f80]) ).
fof(f337,plain,
axiom_5,
inference(cnf_transformation,[status(thm)],[f81]) ).
fof(f338,plain,
~ axiom_B,
inference(cnf_transformation,[status(thm)],[f83]) ).
fof(f339,definition,
( sQ0_spl
<=> modus_ponens ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f341,plain,
( sQ0_spl
| ~ modus_ponens ),
inference(component_clause,[status(thm)],[f339]) ).
fof(f342,definition,
! [X0,X1] :
( sQ1_spl
<=> ( is_a_theorem(X1)
| ~ is_a_theorem(implies(X0,X1))
| ~ is_a_theorem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f343,plain,
! [X0,X1] :
( ~ sQ1_spl
| is_a_theorem(X1)
| ~ is_a_theorem(implies(X0,X1))
| ~ is_a_theorem(X0) ),
inference(component_clause,[status(thm)],[f342]) ).
fof(f345,plain,
( sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f88,f339,f342]) ).
fof(f358,definition,
( sQ5_spl
<=> substitution_of_equivalents ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f360,plain,
( sQ5_spl
| ~ substitution_of_equivalents ),
inference(component_clause,[status(thm)],[f358]) ).
fof(f361,definition,
! [X0,X1] :
( sQ6_spl
<=> ( X0 = X1
| ~ is_a_theorem(equiv(X0,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f362,plain,
! [X0,X1] :
( ~ sQ6_spl
| X0 = X1
| ~ is_a_theorem(equiv(X0,X1)) ),
inference(component_clause,[status(thm)],[f361]) ).
fof(f364,plain,
( sQ6_spl
| ~ sQ5_spl ),
inference(split_clause,[status(thm)],[f95,f358,f361]) ).
fof(f373,definition,
( sQ9_spl
<=> modus_tollens ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f375,plain,
( sQ9_spl
| ~ modus_tollens ),
inference(component_clause,[status(thm)],[f373]) ).
fof(f376,definition,
! [X0,X1] :
( sQ10_spl
<=> is_a_theorem(implies(implies(not(X0),not(X1)),implies(X1,X0))) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f377,plain,
! [X0,X1] :
( ~ sQ10_spl
| is_a_theorem(implies(implies(not(X0),not(X1)),implies(X1,X0))) ),
inference(component_clause,[status(thm)],[f376]) ).
fof(f379,plain,
( sQ10_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f100,f373,f376]) ).
fof(f380,definition,
( sQ11_spl
<=> is_a_theorem(implies(implies(not(sK5_skl),not(sK4_skl)),implies(sK4_skl,sK5_skl))) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f382,plain,
( sQ11_spl
| ~ is_a_theorem(implies(implies(not(sK5_skl),not(sK4_skl)),implies(sK4_skl,sK5_skl))) ),
inference(component_clause,[status(thm)],[f380]) ).
fof(f384,definition,
( sQ12_spl
<=> implies_1 ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f386,plain,
( sQ12_spl
| ~ implies_1 ),
inference(component_clause,[status(thm)],[f384]) ).
fof(f387,definition,
! [X0,X1] :
( sQ13_spl
<=> is_a_theorem(implies(X0,implies(X1,X0))) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f388,plain,
! [X0,X1] :
( ~ sQ13_spl
| is_a_theorem(implies(X0,implies(X1,X0))) ),
inference(component_clause,[status(thm)],[f387]) ).
fof(f390,plain,
( sQ13_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f104,f384,f387]) ).
fof(f391,definition,
( sQ14_spl
<=> is_a_theorem(implies(sK6_skl,implies(sK7_skl,sK6_skl))) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f393,plain,
( sQ14_spl
| ~ is_a_theorem(implies(sK6_skl,implies(sK7_skl,sK6_skl))) ),
inference(component_clause,[status(thm)],[f391]) ).
fof(f395,definition,
( sQ15_spl
<=> implies_2 ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f397,plain,
( sQ15_spl
| ~ implies_2 ),
inference(component_clause,[status(thm)],[f395]) ).
fof(f398,definition,
! [X0,X1] :
( sQ16_spl
<=> is_a_theorem(implies(implies(X0,implies(X0,X1)),implies(X0,X1))) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f399,plain,
! [X0,X1] :
( ~ sQ16_spl
| is_a_theorem(implies(implies(X0,implies(X0,X1)),implies(X0,X1))) ),
inference(component_clause,[status(thm)],[f398]) ).
fof(f401,plain,
( sQ16_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f108,f395,f398]) ).
fof(f402,definition,
( sQ17_spl
<=> is_a_theorem(implies(implies(sK8_skl,implies(sK8_skl,sK9_skl)),implies(sK8_skl,sK9_skl))) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f404,plain,
( sQ17_spl
| ~ is_a_theorem(implies(implies(sK8_skl,implies(sK8_skl,sK9_skl)),implies(sK8_skl,sK9_skl))) ),
inference(component_clause,[status(thm)],[f402]) ).
fof(f406,definition,
( sQ18_spl
<=> implies_3 ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f408,plain,
( sQ18_spl
| ~ implies_3 ),
inference(component_clause,[status(thm)],[f406]) ).
fof(f409,definition,
! [X0,X1,X2] :
( sQ19_spl
<=> is_a_theorem(implies(implies(X0,X1),implies(implies(X1,X2),implies(X0,X2)))) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f410,plain,
! [X0,X1,X2] :
( ~ sQ19_spl
| is_a_theorem(implies(implies(X0,X1),implies(implies(X1,X2),implies(X0,X2)))) ),
inference(component_clause,[status(thm)],[f409]) ).
fof(f412,plain,
( sQ19_spl
| ~ sQ18_spl ),
inference(split_clause,[status(thm)],[f112,f406,f409]) ).
fof(f413,definition,
( sQ20_spl
<=> is_a_theorem(implies(implies(sK10_skl,sK11_skl),implies(implies(sK11_skl,sK12_skl),implies(sK10_skl,sK12_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f415,plain,
( sQ20_spl
| ~ is_a_theorem(implies(implies(sK10_skl,sK11_skl),implies(implies(sK11_skl,sK12_skl),implies(sK10_skl,sK12_skl)))) ),
inference(component_clause,[status(thm)],[f413]) ).
fof(f417,definition,
( sQ21_spl
<=> and_1 ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f419,plain,
( sQ21_spl
| ~ and_1 ),
inference(component_clause,[status(thm)],[f417]) ).
fof(f420,definition,
! [X0,X1] :
( sQ22_spl
<=> is_a_theorem(implies(and(X0,X1),X0)) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f421,plain,
! [X0,X1] :
( ~ sQ22_spl
| is_a_theorem(implies(and(X0,X1),X0)) ),
inference(component_clause,[status(thm)],[f420]) ).
fof(f423,plain,
( sQ22_spl
| ~ sQ21_spl ),
inference(split_clause,[status(thm)],[f116,f417,f420]) ).
fof(f424,definition,
( sQ23_spl
<=> is_a_theorem(implies(and(sK13_skl,sK14_skl),sK13_skl)) ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f426,plain,
( sQ23_spl
| ~ is_a_theorem(implies(and(sK13_skl,sK14_skl),sK13_skl)) ),
inference(component_clause,[status(thm)],[f424]) ).
fof(f428,definition,
( sQ24_spl
<=> and_2 ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f430,plain,
( sQ24_spl
| ~ and_2 ),
inference(component_clause,[status(thm)],[f428]) ).
fof(f431,definition,
! [X0,X1] :
( sQ25_spl
<=> is_a_theorem(implies(and(X0,X1),X1)) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f432,plain,
! [X0,X1] :
( ~ sQ25_spl
| is_a_theorem(implies(and(X0,X1),X1)) ),
inference(component_clause,[status(thm)],[f431]) ).
fof(f434,plain,
( sQ25_spl
| ~ sQ24_spl ),
inference(split_clause,[status(thm)],[f120,f428,f431]) ).
fof(f435,definition,
( sQ26_spl
<=> is_a_theorem(implies(and(sK15_skl,sK16_skl),sK16_skl)) ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f437,plain,
( sQ26_spl
| ~ is_a_theorem(implies(and(sK15_skl,sK16_skl),sK16_skl)) ),
inference(component_clause,[status(thm)],[f435]) ).
fof(f439,definition,
( sQ27_spl
<=> and_3 ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f441,plain,
( sQ27_spl
| ~ and_3 ),
inference(component_clause,[status(thm)],[f439]) ).
fof(f442,definition,
! [X0,X1] :
( sQ28_spl
<=> is_a_theorem(implies(X0,implies(X1,and(X0,X1)))) ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f443,plain,
! [X0,X1] :
( ~ sQ28_spl
| is_a_theorem(implies(X0,implies(X1,and(X0,X1)))) ),
inference(component_clause,[status(thm)],[f442]) ).
fof(f445,plain,
( sQ28_spl
| ~ sQ27_spl ),
inference(split_clause,[status(thm)],[f124,f439,f442]) ).
fof(f446,definition,
( sQ29_spl
<=> is_a_theorem(implies(sK17_skl,implies(sK18_skl,and(sK17_skl,sK18_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f448,plain,
( sQ29_spl
| ~ is_a_theorem(implies(sK17_skl,implies(sK18_skl,and(sK17_skl,sK18_skl)))) ),
inference(component_clause,[status(thm)],[f446]) ).
fof(f450,definition,
( sQ30_spl
<=> or_1 ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f452,plain,
( sQ30_spl
| ~ or_1 ),
inference(component_clause,[status(thm)],[f450]) ).
fof(f453,definition,
! [X0,X1] :
( sQ31_spl
<=> is_a_theorem(implies(X0,or(X0,X1))) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f454,plain,
! [X0,X1] :
( ~ sQ31_spl
| is_a_theorem(implies(X0,or(X0,X1))) ),
inference(component_clause,[status(thm)],[f453]) ).
fof(f456,plain,
( sQ31_spl
| ~ sQ30_spl ),
inference(split_clause,[status(thm)],[f128,f450,f453]) ).
fof(f457,definition,
( sQ32_spl
<=> is_a_theorem(implies(sK19_skl,or(sK19_skl,sK20_skl))) ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f459,plain,
( sQ32_spl
| ~ is_a_theorem(implies(sK19_skl,or(sK19_skl,sK20_skl))) ),
inference(component_clause,[status(thm)],[f457]) ).
fof(f461,definition,
( sQ33_spl
<=> or_2 ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f463,plain,
( sQ33_spl
| ~ or_2 ),
inference(component_clause,[status(thm)],[f461]) ).
fof(f464,definition,
! [X0,X1] :
( sQ34_spl
<=> is_a_theorem(implies(X0,or(X1,X0))) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f465,plain,
! [X0,X1] :
( ~ sQ34_spl
| is_a_theorem(implies(X0,or(X1,X0))) ),
inference(component_clause,[status(thm)],[f464]) ).
fof(f467,plain,
( sQ34_spl
| ~ sQ33_spl ),
inference(split_clause,[status(thm)],[f132,f461,f464]) ).
fof(f468,definition,
( sQ35_spl
<=> is_a_theorem(implies(sK22_skl,or(sK21_skl,sK22_skl))) ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f470,plain,
( sQ35_spl
| ~ is_a_theorem(implies(sK22_skl,or(sK21_skl,sK22_skl))) ),
inference(component_clause,[status(thm)],[f468]) ).
fof(f472,definition,
( sQ36_spl
<=> or_3 ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f474,plain,
( sQ36_spl
| ~ or_3 ),
inference(component_clause,[status(thm)],[f472]) ).
fof(f475,definition,
! [X0,X1,X2] :
( sQ37_spl
<=> is_a_theorem(implies(implies(X0,X1),implies(implies(X2,X1),implies(or(X0,X2),X1)))) ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f476,plain,
! [X0,X1,X2] :
( ~ sQ37_spl
| is_a_theorem(implies(implies(X0,X1),implies(implies(X2,X1),implies(or(X0,X2),X1)))) ),
inference(component_clause,[status(thm)],[f475]) ).
fof(f478,plain,
( sQ37_spl
| ~ sQ36_spl ),
inference(split_clause,[status(thm)],[f136,f472,f475]) ).
fof(f479,definition,
( sQ38_spl
<=> is_a_theorem(implies(implies(sK23_skl,sK25_skl),implies(implies(sK24_skl,sK25_skl),implies(or(sK23_skl,sK24_skl),sK25_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f481,plain,
( sQ38_spl
| ~ is_a_theorem(implies(implies(sK23_skl,sK25_skl),implies(implies(sK24_skl,sK25_skl),implies(or(sK23_skl,sK24_skl),sK25_skl)))) ),
inference(component_clause,[status(thm)],[f479]) ).
fof(f483,definition,
( sQ39_spl
<=> equivalence_1 ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f485,plain,
( sQ39_spl
| ~ equivalence_1 ),
inference(component_clause,[status(thm)],[f483]) ).
fof(f486,definition,
! [X0,X1] :
( sQ40_spl
<=> is_a_theorem(implies(equiv(X0,X1),implies(X0,X1))) ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f487,plain,
! [X0,X1] :
( ~ sQ40_spl
| is_a_theorem(implies(equiv(X0,X1),implies(X0,X1))) ),
inference(component_clause,[status(thm)],[f486]) ).
fof(f489,plain,
( sQ40_spl
| ~ sQ39_spl ),
inference(split_clause,[status(thm)],[f140,f483,f486]) ).
fof(f490,definition,
( sQ41_spl
<=> is_a_theorem(implies(equiv(sK26_skl,sK27_skl),implies(sK26_skl,sK27_skl))) ),
introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition]) ).
fof(f492,plain,
( sQ41_spl
| ~ is_a_theorem(implies(equiv(sK26_skl,sK27_skl),implies(sK26_skl,sK27_skl))) ),
inference(component_clause,[status(thm)],[f490]) ).
fof(f494,definition,
( sQ42_spl
<=> equivalence_2 ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f496,plain,
( sQ42_spl
| ~ equivalence_2 ),
inference(component_clause,[status(thm)],[f494]) ).
fof(f497,definition,
! [X0,X1] :
( sQ43_spl
<=> is_a_theorem(implies(equiv(X0,X1),implies(X1,X0))) ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f498,plain,
! [X0,X1] :
( ~ sQ43_spl
| is_a_theorem(implies(equiv(X0,X1),implies(X1,X0))) ),
inference(component_clause,[status(thm)],[f497]) ).
fof(f500,plain,
( sQ43_spl
| ~ sQ42_spl ),
inference(split_clause,[status(thm)],[f144,f494,f497]) ).
fof(f501,definition,
( sQ44_spl
<=> is_a_theorem(implies(equiv(sK28_skl,sK29_skl),implies(sK29_skl,sK28_skl))) ),
introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition]) ).
fof(f503,plain,
( sQ44_spl
| ~ is_a_theorem(implies(equiv(sK28_skl,sK29_skl),implies(sK29_skl,sK28_skl))) ),
inference(component_clause,[status(thm)],[f501]) ).
fof(f505,definition,
( sQ45_spl
<=> equivalence_3 ),
introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition]) ).
fof(f507,plain,
( sQ45_spl
| ~ equivalence_3 ),
inference(component_clause,[status(thm)],[f505]) ).
fof(f508,definition,
! [X0,X1] :
( sQ46_spl
<=> is_a_theorem(implies(implies(X0,X1),implies(implies(X1,X0),equiv(X0,X1)))) ),
introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition]) ).
fof(f509,plain,
! [X0,X1] :
( ~ sQ46_spl
| is_a_theorem(implies(implies(X0,X1),implies(implies(X1,X0),equiv(X0,X1)))) ),
inference(component_clause,[status(thm)],[f508]) ).
fof(f511,plain,
( sQ46_spl
| ~ sQ45_spl ),
inference(split_clause,[status(thm)],[f148,f505,f508]) ).
fof(f512,definition,
( sQ47_spl
<=> is_a_theorem(implies(implies(sK30_skl,sK31_skl),implies(implies(sK31_skl,sK30_skl),equiv(sK30_skl,sK31_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition]) ).
fof(f514,plain,
( sQ47_spl
| ~ is_a_theorem(implies(implies(sK30_skl,sK31_skl),implies(implies(sK31_skl,sK30_skl),equiv(sK30_skl,sK31_skl)))) ),
inference(component_clause,[status(thm)],[f512]) ).
fof(f516,definition,
( sQ48_spl
<=> kn1 ),
introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition]) ).
fof(f519,definition,
! [X0] :
( sQ49_spl
<=> is_a_theorem(implies(X0,and(X0,X0))) ),
introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition]) ).
fof(f520,plain,
! [X0] :
( ~ sQ49_spl
| is_a_theorem(implies(X0,and(X0,X0))) ),
inference(component_clause,[status(thm)],[f519]) ).
fof(f523,definition,
( sQ50_spl
<=> is_a_theorem(implies(sK32_skl,and(sK32_skl,sK32_skl))) ),
introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition]) ).
fof(f525,plain,
( sQ50_spl
| ~ is_a_theorem(implies(sK32_skl,and(sK32_skl,sK32_skl))) ),
inference(component_clause,[status(thm)],[f523]) ).
fof(f526,plain,
( ~ sQ50_spl
| sQ48_spl ),
inference(split_clause,[status(thm)],[f153,f516,f523]) ).
fof(f527,definition,
( sQ51_spl
<=> kn2 ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f531,definition,
( sQ52_spl
<=> is_a_theorem(implies(and(sK33_skl,sK34_skl),sK33_skl)) ),
introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition]) ).
fof(f533,plain,
( sQ52_spl
| ~ is_a_theorem(implies(and(sK33_skl,sK34_skl),sK33_skl)) ),
inference(component_clause,[status(thm)],[f531]) ).
fof(f534,plain,
( ~ sQ52_spl
| sQ51_spl ),
inference(split_clause,[status(thm)],[f157,f527,f531]) ).
fof(f546,definition,
( sQ56_spl
<=> cn1 ),
introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition]) ).
fof(f550,definition,
( sQ57_spl
<=> is_a_theorem(implies(implies(sK38_skl,sK39_skl),implies(implies(sK39_skl,sK40_skl),implies(sK38_skl,sK40_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition]) ).
fof(f552,plain,
( sQ57_spl
| ~ is_a_theorem(implies(implies(sK38_skl,sK39_skl),implies(implies(sK39_skl,sK40_skl),implies(sK38_skl,sK40_skl)))) ),
inference(component_clause,[status(thm)],[f550]) ).
fof(f553,plain,
( ~ sQ57_spl
| sQ56_spl ),
inference(split_clause,[status(thm)],[f165,f546,f550]) ).
fof(f554,definition,
( sQ58_spl
<=> cn2 ),
introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition]) ).
fof(f557,definition,
! [X0,X1] :
( sQ59_spl
<=> is_a_theorem(implies(X0,implies(not(X0),X1))) ),
introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition]) ).
fof(f560,plain,
( sQ59_spl
| ~ sQ58_spl ),
inference(split_clause,[status(thm)],[f168,f554,f557]) ).
fof(f561,definition,
( sQ60_spl
<=> is_a_theorem(implies(sK41_skl,implies(not(sK41_skl),sK42_skl))) ),
introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition]) ).
fof(f563,plain,
( sQ60_spl
| ~ is_a_theorem(implies(sK41_skl,implies(not(sK41_skl),sK42_skl))) ),
inference(component_clause,[status(thm)],[f561]) ).
fof(f564,plain,
( ~ sQ60_spl
| sQ58_spl ),
inference(split_clause,[status(thm)],[f169,f554,f561]) ).
fof(f565,definition,
( sQ61_spl
<=> cn3 ),
introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition]) ).
fof(f568,definition,
! [X0] :
( sQ62_spl
<=> is_a_theorem(implies(implies(not(X0),X0),X0)) ),
introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition]) ).
fof(f571,plain,
( sQ62_spl
| ~ sQ61_spl ),
inference(split_clause,[status(thm)],[f172,f565,f568]) ).
fof(f572,definition,
( sQ63_spl
<=> is_a_theorem(implies(implies(not(sK43_skl),sK43_skl),sK43_skl)) ),
introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition]) ).
fof(f574,plain,
( sQ63_spl
| ~ is_a_theorem(implies(implies(not(sK43_skl),sK43_skl),sK43_skl)) ),
inference(component_clause,[status(thm)],[f572]) ).
fof(f575,plain,
( ~ sQ63_spl
| sQ61_spl ),
inference(split_clause,[status(thm)],[f173,f565,f572]) ).
fof(f576,definition,
( sQ64_spl
<=> r1 ),
introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition]) ).
fof(f579,definition,
! [X0] :
( sQ65_spl
<=> is_a_theorem(implies(or(X0,X0),X0)) ),
introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition]) ).
fof(f580,plain,
! [X0] :
( ~ sQ65_spl
| is_a_theorem(implies(or(X0,X0),X0)) ),
inference(component_clause,[status(thm)],[f579]) ).
fof(f582,plain,
( sQ65_spl
| ~ sQ64_spl ),
inference(split_clause,[status(thm)],[f176,f576,f579]) ).
fof(f583,definition,
( sQ66_spl
<=> is_a_theorem(implies(or(sK44_skl,sK44_skl),sK44_skl)) ),
introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition]) ).
fof(f585,plain,
( sQ66_spl
| ~ is_a_theorem(implies(or(sK44_skl,sK44_skl),sK44_skl)) ),
inference(component_clause,[status(thm)],[f583]) ).
fof(f586,plain,
( ~ sQ66_spl
| sQ64_spl ),
inference(split_clause,[status(thm)],[f177,f576,f583]) ).
fof(f587,definition,
( sQ67_spl
<=> r2 ),
introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition]) ).
fof(f591,definition,
( sQ68_spl
<=> is_a_theorem(implies(sK46_skl,or(sK45_skl,sK46_skl))) ),
introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition]) ).
fof(f593,plain,
( sQ68_spl
| ~ is_a_theorem(implies(sK46_skl,or(sK45_skl,sK46_skl))) ),
inference(component_clause,[status(thm)],[f591]) ).
fof(f594,plain,
( ~ sQ68_spl
| sQ67_spl ),
inference(split_clause,[status(thm)],[f181,f587,f591]) ).
fof(f628,definition,
( sQ78_spl
<=> op_or ),
introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition]) ).
fof(f630,plain,
( sQ78_spl
| ~ op_or ),
inference(component_clause,[status(thm)],[f628]) ).
fof(f631,definition,
! [X0,X1] :
( sQ79_spl
<=> or(X0,X1) = not(and(not(X0),not(X1))) ),
introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition]) ).
fof(f632,plain,
! [X0,X1] :
( ~ sQ79_spl
| or(X0,X1) = not(and(not(X0),not(X1))) ),
inference(component_clause,[status(thm)],[f631]) ).
fof(f634,plain,
( sQ79_spl
| ~ sQ78_spl ),
inference(split_clause,[status(thm)],[f195,f628,f631]) ).
fof(f642,definition,
( sQ82_spl
<=> op_implies_and ),
introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition]) ).
fof(f644,plain,
( sQ82_spl
| ~ op_implies_and ),
inference(component_clause,[status(thm)],[f642]) ).
fof(f645,definition,
! [X0,X1] :
( sQ83_spl
<=> implies(X0,X1) = not(and(X0,not(X1))) ),
introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition]) ).
fof(f646,plain,
! [X0,X1] :
( ~ sQ83_spl
| implies(X0,X1) = not(and(X0,not(X1))) ),
inference(component_clause,[status(thm)],[f645]) ).
fof(f648,plain,
( sQ83_spl
| ~ sQ82_spl ),
inference(split_clause,[status(thm)],[f199,f642,f645]) ).
fof(f652,definition,
! [X0,X1] :
( sQ85_spl
<=> implies(X0,X1) = or(not(X0),X1) ),
introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition]) ).
fof(f653,plain,
! [X0,X1] :
( ~ sQ85_spl
| implies(X0,X1) = or(not(X0),X1) ),
inference(component_clause,[status(thm)],[f652]) ).
fof(f656,definition,
( sQ86_spl
<=> op_equiv ),
introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition]) ).
fof(f658,plain,
( sQ86_spl
| ~ op_equiv ),
inference(component_clause,[status(thm)],[f656]) ).
fof(f659,definition,
! [X0,X1] :
( sQ87_spl
<=> equiv(X0,X1) = and(implies(X0,X1),implies(X1,X0)) ),
introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition]) ).
fof(f660,plain,
! [X0,X1] :
( ~ sQ87_spl
| equiv(X0,X1) = and(implies(X0,X1),implies(X1,X0)) ),
inference(component_clause,[status(thm)],[f659]) ).
fof(f662,plain,
( sQ87_spl
| ~ sQ86_spl ),
inference(split_clause,[status(thm)],[f203,f656,f659]) ).
fof(f663,definition,
( sQ88_spl
<=> necessitation ),
introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition]) ).
fof(f665,plain,
( sQ88_spl
| ~ necessitation ),
inference(component_clause,[status(thm)],[f663]) ).
fof(f666,definition,
! [X0] :
( sQ89_spl
<=> ( is_a_theorem(necessarily(X0))
| ~ is_a_theorem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition]) ).
fof(f669,plain,
( sQ89_spl
| ~ sQ88_spl ),
inference(split_clause,[status(thm)],[f225,f663,f666]) ).
fof(f697,definition,
( sQ97_spl
<=> adjunction ),
introduced(definition,[new_symbols(definition,[sQ97_spl])],[split_symbol_definition]) ).
fof(f700,definition,
! [X0,X1] :
( sQ98_spl
<=> ( is_a_theorem(and(X0,X1))
| ~ is_a_theorem(X1)
| ~ is_a_theorem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ98_spl])],[split_symbol_definition]) ).
fof(f701,plain,
! [X0,X1] :
( ~ sQ98_spl
| is_a_theorem(and(X0,X1))
| ~ is_a_theorem(X1)
| ~ is_a_theorem(X0) ),
inference(component_clause,[status(thm)],[f700]) ).
fof(f703,plain,
( sQ98_spl
| ~ sQ97_spl ),
inference(split_clause,[status(thm)],[f239,f697,f700]) ).
fof(f704,definition,
( sQ99_spl
<=> is_a_theorem(sK58_skl) ),
introduced(definition,[new_symbols(definition,[sQ99_spl])],[split_symbol_definition]) ).
fof(f707,plain,
( sQ99_spl
| sQ97_spl ),
inference(split_clause,[status(thm)],[f240,f697,f704]) ).
fof(f708,definition,
( sQ100_spl
<=> is_a_theorem(sK59_skl) ),
introduced(definition,[new_symbols(definition,[sQ100_spl])],[split_symbol_definition]) ).
fof(f711,plain,
( sQ100_spl
| sQ97_spl ),
inference(split_clause,[status(thm)],[f241,f697,f708]) ).
fof(f712,definition,
( sQ101_spl
<=> is_a_theorem(and(sK58_skl,sK59_skl)) ),
introduced(definition,[new_symbols(definition,[sQ101_spl])],[split_symbol_definition]) ).
fof(f714,plain,
( sQ101_spl
| ~ is_a_theorem(and(sK58_skl,sK59_skl)) ),
inference(component_clause,[status(thm)],[f712]) ).
fof(f715,plain,
( ~ sQ101_spl
| sQ97_spl ),
inference(split_clause,[status(thm)],[f242,f697,f712]) ).
fof(f731,definition,
( sQ106_spl
<=> axiom_K ),
introduced(definition,[new_symbols(definition,[sQ106_spl])],[split_symbol_definition]) ).
fof(f733,plain,
( sQ106_spl
| ~ axiom_K ),
inference(component_clause,[status(thm)],[f731]) ).
fof(f734,definition,
! [X0,X1] :
( sQ107_spl
<=> is_a_theorem(implies(necessarily(implies(X0,X1)),implies(necessarily(X0),necessarily(X1)))) ),
introduced(definition,[new_symbols(definition,[sQ107_spl])],[split_symbol_definition]) ).
fof(f735,plain,
! [X0,X1] :
( ~ sQ107_spl
| is_a_theorem(implies(necessarily(implies(X0,X1)),implies(necessarily(X0),necessarily(X1)))) ),
inference(component_clause,[status(thm)],[f734]) ).
fof(f737,plain,
( sQ107_spl
| ~ sQ106_spl ),
inference(split_clause,[status(thm)],[f251,f731,f734]) ).
fof(f738,definition,
( sQ108_spl
<=> is_a_theorem(implies(necessarily(implies(sK62_skl,sK63_skl)),implies(necessarily(sK62_skl),necessarily(sK63_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ108_spl])],[split_symbol_definition]) ).
fof(f740,plain,
( sQ108_spl
| ~ is_a_theorem(implies(necessarily(implies(sK62_skl,sK63_skl)),implies(necessarily(sK62_skl),necessarily(sK63_skl)))) ),
inference(component_clause,[status(thm)],[f738]) ).
fof(f742,definition,
( sQ109_spl
<=> axiom_M ),
introduced(definition,[new_symbols(definition,[sQ109_spl])],[split_symbol_definition]) ).
fof(f744,plain,
( sQ109_spl
| ~ axiom_M ),
inference(component_clause,[status(thm)],[f742]) ).
fof(f745,definition,
! [X0] :
( sQ110_spl
<=> is_a_theorem(implies(necessarily(X0),X0)) ),
introduced(definition,[new_symbols(definition,[sQ110_spl])],[split_symbol_definition]) ).
fof(f746,plain,
! [X0] :
( ~ sQ110_spl
| is_a_theorem(implies(necessarily(X0),X0)) ),
inference(component_clause,[status(thm)],[f745]) ).
fof(f748,plain,
( sQ110_spl
| ~ sQ109_spl ),
inference(split_clause,[status(thm)],[f255,f742,f745]) ).
fof(f749,definition,
( sQ111_spl
<=> is_a_theorem(implies(necessarily(sK64_skl),sK64_skl)) ),
introduced(definition,[new_symbols(definition,[sQ111_spl])],[split_symbol_definition]) ).
fof(f751,plain,
( sQ111_spl
| ~ is_a_theorem(implies(necessarily(sK64_skl),sK64_skl)) ),
inference(component_clause,[status(thm)],[f749]) ).
fof(f764,definition,
( sQ115_spl
<=> axiom_B ),
introduced(definition,[new_symbols(definition,[sQ115_spl])],[split_symbol_definition]) ).
fof(f765,plain,
( ~ sQ115_spl
| axiom_B ),
inference(component_clause,[status(thm)],[f764]) ).
fof(f767,definition,
! [X0] :
( sQ116_spl
<=> is_a_theorem(implies(X0,necessarily(possibly(X0)))) ),
introduced(definition,[new_symbols(definition,[sQ116_spl])],[split_symbol_definition]) ).
fof(f768,plain,
! [X0] :
( ~ sQ116_spl
| is_a_theorem(implies(X0,necessarily(possibly(X0)))) ),
inference(component_clause,[status(thm)],[f767]) ).
fof(f771,definition,
( sQ117_spl
<=> is_a_theorem(implies(sK66_skl,necessarily(possibly(sK66_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ117_spl])],[split_symbol_definition]) ).
fof(f773,plain,
( sQ117_spl
| ~ is_a_theorem(implies(sK66_skl,necessarily(possibly(sK66_skl)))) ),
inference(component_clause,[status(thm)],[f771]) ).
fof(f774,plain,
( ~ sQ117_spl
| sQ115_spl ),
inference(split_clause,[status(thm)],[f264,f764,f771]) ).
fof(f775,definition,
( sQ118_spl
<=> axiom_5 ),
introduced(definition,[new_symbols(definition,[sQ118_spl])],[split_symbol_definition]) ).
fof(f777,plain,
( sQ118_spl
| ~ axiom_5 ),
inference(component_clause,[status(thm)],[f775]) ).
fof(f778,definition,
! [X0] :
( sQ119_spl
<=> is_a_theorem(implies(possibly(X0),necessarily(possibly(X0)))) ),
introduced(definition,[new_symbols(definition,[sQ119_spl])],[split_symbol_definition]) ).
fof(f779,plain,
! [X0] :
( ~ sQ119_spl
| is_a_theorem(implies(possibly(X0),necessarily(possibly(X0)))) ),
inference(component_clause,[status(thm)],[f778]) ).
fof(f781,plain,
( sQ119_spl
| ~ sQ118_spl ),
inference(split_clause,[status(thm)],[f267,f775,f778]) ).
fof(f782,definition,
( sQ120_spl
<=> is_a_theorem(implies(possibly(sK67_skl),necessarily(possibly(sK67_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ120_spl])],[split_symbol_definition]) ).
fof(f784,plain,
( sQ120_spl
| ~ is_a_theorem(implies(possibly(sK67_skl),necessarily(possibly(sK67_skl)))) ),
inference(component_clause,[status(thm)],[f782]) ).
fof(f940,definition,
( sQ163_spl
<=> op_possibly ),
introduced(definition,[new_symbols(definition,[sQ163_spl])],[split_symbol_definition]) ).
fof(f942,plain,
( sQ163_spl
| ~ op_possibly ),
inference(component_clause,[status(thm)],[f940]) ).
fof(f943,definition,
! [X0] :
( sQ164_spl
<=> possibly(X0) = not(necessarily(not(X0))) ),
introduced(definition,[new_symbols(definition,[sQ164_spl])],[split_symbol_definition]) ).
fof(f944,plain,
! [X0] :
( ~ sQ164_spl
| possibly(X0) = not(necessarily(not(X0))) ),
inference(component_clause,[status(thm)],[f943]) ).
fof(f946,plain,
( sQ164_spl
| ~ sQ163_spl ),
inference(split_clause,[status(thm)],[f326,f940,f943]) ).
fof(f968,plain,
( sQ163_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f942,f333]) ).
fof(f969,plain,
sQ163_spl,
inference(contradiction_clause,[status(thm)],[f968]) ).
fof(f970,plain,
( sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f341,f207]) ).
fof(f971,plain,
sQ0_spl,
inference(contradiction_clause,[status(thm)],[f970]) ).
fof(f972,plain,
( sQ88_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f665,f334]) ).
fof(f973,plain,
sQ88_spl,
inference(contradiction_clause,[status(thm)],[f972]) ).
fof(f974,plain,
( sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f360,f221]) ).
fof(f975,plain,
sQ5_spl,
inference(contradiction_clause,[status(thm)],[f974]) ).
fof(f976,plain,
( sQ86_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f658,f206]) ).
fof(f977,plain,
sQ86_spl,
inference(contradiction_clause,[status(thm)],[f976]) ).
fof(f978,plain,
( sQ82_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f644,f205]) ).
fof(f979,plain,
sQ82_spl,
inference(contradiction_clause,[status(thm)],[f978]) ).
fof(f980,plain,
( sQ78_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f630,f204]) ).
fof(f981,plain,
sQ78_spl,
inference(contradiction_clause,[status(thm)],[f980]) ).
fof(f986,plain,
( sQ111_spl
| ~ sQ110_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f751,f746]) ).
fof(f987,plain,
( sQ111_spl
| ~ sQ110_spl ),
inference(contradiction_clause,[status(thm)],[f986]) ).
fof(f988,plain,
( sQ109_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f744,f336]) ).
fof(f989,plain,
sQ109_spl,
inference(contradiction_clause,[status(thm)],[f988]) ).
fof(f1003,plain,
( sQ117_spl
| ~ sQ116_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f773,f768]) ).
fof(f1004,plain,
( sQ117_spl
| ~ sQ116_spl ),
inference(contradiction_clause,[status(thm)],[f1003]) ).
fof(f1005,plain,
( sQ68_spl
| ~ sQ34_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f593,f465]) ).
fof(f1006,plain,
( sQ68_spl
| ~ sQ34_spl ),
inference(contradiction_clause,[status(thm)],[f1005]) ).
fof(f1007,plain,
( sQ33_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f463,f216]) ).
fof(f1008,plain,
sQ33_spl,
inference(contradiction_clause,[status(thm)],[f1007]) ).
fof(f1011,plain,
( sQ52_spl
| ~ sQ22_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f533,f421]) ).
fof(f1012,plain,
( sQ52_spl
| ~ sQ22_spl ),
inference(contradiction_clause,[status(thm)],[f1011]) ).
fof(f1013,plain,
( sQ21_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f419,f212]) ).
fof(f1014,plain,
sQ21_spl,
inference(contradiction_clause,[status(thm)],[f1013]) ).
fof(f1015,plain,
( sQ50_spl
| ~ sQ49_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f525,f520]) ).
fof(f1016,plain,
( sQ50_spl
| ~ sQ49_spl ),
inference(contradiction_clause,[status(thm)],[f1015]) ).
fof(f1019,plain,
( sQ32_spl
| ~ sQ31_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f459,f454]) ).
fof(f1020,plain,
( sQ32_spl
| ~ sQ31_spl ),
inference(contradiction_clause,[status(thm)],[f1019]) ).
fof(f1021,plain,
( sQ30_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f452,f215]) ).
fof(f1022,plain,
sQ30_spl,
inference(contradiction_clause,[status(thm)],[f1021]) ).
fof(f1023,plain,
( sQ26_spl
| ~ sQ25_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f437,f432]) ).
fof(f1024,plain,
( sQ26_spl
| ~ sQ25_spl ),
inference(contradiction_clause,[status(thm)],[f1023]) ).
fof(f1025,plain,
( sQ24_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f430,f213]) ).
fof(f1026,plain,
sQ24_spl,
inference(contradiction_clause,[status(thm)],[f1025]) ).
fof(f1027,plain,
( sQ14_spl
| ~ sQ13_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f393,f388]) ).
fof(f1028,plain,
( sQ14_spl
| ~ sQ13_spl ),
inference(contradiction_clause,[status(thm)],[f1027]) ).
fof(f1029,plain,
( sQ12_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f386,f209]) ).
fof(f1030,plain,
sQ12_spl,
inference(contradiction_clause,[status(thm)],[f1029]) ).
fof(f1042,plain,
! [X0,X1] :
( ~ sQ28_spl
| ~ sQ1_spl
| is_a_theorem(implies(X1,and(X0,X1)))
| ~ is_a_theorem(X0) ),
inference(resolution,[status(thm)],[f343,f443]) ).
fof(f1043,plain,
! [X0,X1] :
( ~ sQ13_spl
| ~ sQ1_spl
| is_a_theorem(implies(X1,X0))
| ~ is_a_theorem(X0) ),
inference(resolution,[status(thm)],[f343,f388]) ).
fof(f1047,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ sQ13_spl
| is_a_theorem(X0)
| ~ is_a_theorem(X1)
| ~ is_a_theorem(X0) ),
inference(resolution,[status(thm)],[f1043,f343]) ).
fof(f1048,definition,
! [X0] :
( sQ171_spl
<=> ( is_a_theorem(X0)
| ~ is_a_theorem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ171_spl])],[split_symbol_definition]) ).
fof(f1051,definition,
! [X1] :
( sQ172_spl
<=> ~ is_a_theorem(X1) ),
introduced(definition,[new_symbols(definition,[sQ172_spl])],[split_symbol_definition]) ).
fof(f1052,plain,
! [X0] :
( ~ sQ172_spl
| ~ is_a_theorem(X0) ),
inference(component_clause,[status(thm)],[f1051]) ).
fof(f1054,plain,
( ~ sQ1_spl
| ~ sQ13_spl
| sQ172_spl
| sQ171_spl ),
inference(split_clause,[status(thm)],[f1047,f1048,f1051,f387,f342]) ).
fof(f1115,plain,
! [X0,X1] :
( ~ sQ28_spl
| ~ sQ1_spl
| ~ is_a_theorem(X1)
| is_a_theorem(and(X1,X0))
| ~ is_a_theorem(X0) ),
inference(resolution,[status(thm)],[f343,f1042]) ).
fof(f1123,plain,
( sQ120_spl
| ~ sQ119_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f784,f779]) ).
fof(f1125,plain,
( sQ120_spl
| ~ sQ119_spl ),
inference(contradiction_clause,[status(thm)],[f1123]) ).
fof(f1126,plain,
( sQ118_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f777,f337]) ).
fof(f1127,plain,
sQ118_spl,
inference(contradiction_clause,[status(thm)],[f1126]) ).
fof(f1136,plain,
( sQ108_spl
| ~ sQ107_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f740,f735]) ).
fof(f1138,plain,
( sQ108_spl
| ~ sQ107_spl ),
inference(contradiction_clause,[status(thm)],[f1136]) ).
fof(f1139,plain,
( sQ106_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f733,f335]) ).
fof(f1140,plain,
sQ106_spl,
inference(contradiction_clause,[status(thm)],[f1139]) ).
fof(f1148,plain,
( sQ101_spl
| ~ sQ28_spl
| ~ sQ1_spl
| ~ is_a_theorem(sK58_skl)
| ~ is_a_theorem(sK59_skl) ),
inference(resolution,[status(thm)],[f1115,f714]) ).
fof(f1155,plain,
( sQ101_spl
| ~ sQ28_spl
| ~ sQ1_spl
| ~ sQ99_spl
| ~ sQ100_spl ),
inference(split_clause,[status(thm)],[f1148,f708,f704,f342,f442,f712]) ).
fof(f1158,plain,
( sQ27_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f441,f214]) ).
fof(f1159,plain,
sQ27_spl,
inference(contradiction_clause,[status(thm)],[f1158]) ).
fof(f1160,plain,
( sQ23_spl
| ~ sQ22_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f426,f421]) ).
fof(f1161,plain,
( sQ23_spl
| ~ sQ22_spl ),
inference(contradiction_clause,[status(thm)],[f1160]) ).
fof(f1162,plain,
( sQ35_spl
| ~ sQ34_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f470,f465]) ).
fof(f1163,plain,
( sQ35_spl
| ~ sQ34_spl ),
inference(contradiction_clause,[status(thm)],[f1162]) ).
fof(f1165,plain,
( ~ sQ43_spl
| ~ sQ172_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f498,f1052]) ).
fof(f1248,plain,
( sQ47_spl
| ~ sQ46_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f514,f509]) ).
fof(f1249,plain,
( sQ47_spl
| ~ sQ46_spl ),
inference(contradiction_clause,[status(thm)],[f1248]) ).
fof(f1250,plain,
( sQ45_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f507,f220]) ).
fof(f1251,plain,
sQ45_spl,
inference(contradiction_clause,[status(thm)],[f1250]) ).
fof(f1291,plain,
( sQ38_spl
| ~ sQ37_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f481,f476]) ).
fof(f1294,plain,
( sQ38_spl
| ~ sQ37_spl ),
inference(contradiction_clause,[status(thm)],[f1291]) ).
fof(f1295,plain,
( sQ36_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f474,f217]) ).
fof(f1296,plain,
sQ36_spl,
inference(contradiction_clause,[status(thm)],[f1295]) ).
fof(f1297,plain,
( sQ29_spl
| ~ sQ28_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f448,f443]) ).
fof(f1298,plain,
( sQ29_spl
| ~ sQ28_spl ),
inference(contradiction_clause,[status(thm)],[f1297]) ).
fof(f1309,plain,
( sQ44_spl
| ~ sQ43_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f503,f498]) ).
fof(f1311,plain,
( sQ44_spl
| ~ sQ43_spl ),
inference(contradiction_clause,[status(thm)],[f1309]) ).
fof(f1312,plain,
( sQ42_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f496,f219]) ).
fof(f1313,plain,
sQ42_spl,
inference(contradiction_clause,[status(thm)],[f1312]) ).
fof(f1314,plain,
( sQ41_spl
| ~ sQ40_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f492,f487]) ).
fof(f1316,plain,
( sQ41_spl
| ~ sQ40_spl ),
inference(contradiction_clause,[status(thm)],[f1314]) ).
fof(f1317,plain,
( sQ39_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f485,f218]) ).
fof(f1318,plain,
sQ39_spl,
inference(contradiction_clause,[status(thm)],[f1317]) ).
fof(f1325,plain,
( sQ17_spl
| ~ sQ16_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f404,f399]) ).
fof(f1326,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ sQ16_spl
| is_a_theorem(implies(X0,X1))
| ~ is_a_theorem(implies(X0,implies(X0,X1))) ),
inference(resolution,[status(thm)],[f399,f343]) ).
fof(f1327,plain,
( sQ17_spl
| ~ sQ16_spl ),
inference(contradiction_clause,[status(thm)],[f1325]) ).
fof(f1328,plain,
( sQ15_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f397,f210]) ).
fof(f1329,plain,
sQ15_spl,
inference(contradiction_clause,[status(thm)],[f1328]) ).
fof(f1344,plain,
! [X0,X1] :
( ~ sQ87_spl
| ~ sQ98_spl
| is_a_theorem(equiv(X0,X1))
| ~ is_a_theorem(implies(X1,X0))
| ~ is_a_theorem(implies(X0,X1)) ),
inference(paramodulation,[status(thm)],[f660,f701]) ).
fof(f1349,plain,
( sQ11_spl
| ~ sQ79_spl
| ~ sQ83_spl
| ~ is_a_theorem(implies(or(sK5_skl,not(sK4_skl)),implies(sK4_skl,sK5_skl))) ),
inference(backward_demodulation,[status(thm)],[f1353,f382]) ).
fof(f1351,plain,
( sQ60_spl
| ~ sQ79_spl
| ~ sQ83_spl
| ~ is_a_theorem(implies(sK41_skl,or(sK41_skl,sK42_skl))) ),
inference(backward_demodulation,[status(thm)],[f1353,f563]) ).
fof(f1353,plain,
! [X0,X1] :
( ~ sQ79_spl
| ~ sQ83_spl
| or(X0,X1) = implies(not(X0),X1) ),
inference(forward_demodulation,[status(thm)],[f646,f632]) ).
fof(f1371,plain,
( sQ60_spl
| ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ31_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1351,f454]) ).
fof(f1372,plain,
( sQ60_spl
| ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ31_spl ),
inference(contradiction_clause,[status(thm)],[f1371]) ).
fof(f1381,plain,
! [X0,X1] :
( ~ sQ10_spl
| ~ sQ79_spl
| ~ sQ83_spl
| is_a_theorem(implies(or(X0,not(X1)),implies(X1,X0))) ),
inference(forward_demodulation,[status(thm)],[f1353,f377]) ).
fof(f1387,plain,
! [X0,X1] :
( ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ10_spl
| is_a_theorem(implies(or(X0,not(not(X1))),or(X1,X0))) ),
inference(paramodulation,[status(thm)],[f1353,f1381]) ).
fof(f1563,plain,
( sQ63_spl
| ~ sQ79_spl
| ~ sQ83_spl
| ~ is_a_theorem(implies(or(sK43_skl,sK43_skl),sK43_skl)) ),
inference(forward_demodulation,[status(thm)],[f1353,f574]) ).
fof(f1585,plain,
( sQ20_spl
| ~ sQ19_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f415,f410]) ).
fof(f1586,plain,
( sQ57_spl
| ~ sQ19_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f552,f410]) ).
fof(f1591,plain,
( sQ20_spl
| ~ sQ19_spl ),
inference(contradiction_clause,[status(thm)],[f1585]) ).
fof(f1592,plain,
( sQ18_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f408,f211]) ).
fof(f1593,plain,
sQ18_spl,
inference(contradiction_clause,[status(thm)],[f1592]) ).
fof(f1594,plain,
( sQ57_spl
| ~ sQ19_spl ),
inference(contradiction_clause,[status(thm)],[f1586]) ).
fof(f1771,plain,
( sQ9_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f375,f208]) ).
fof(f1772,plain,
sQ9_spl,
inference(contradiction_clause,[status(thm)],[f1771]) ).
fof(f1994,plain,
! [X0,X1] :
( ~ sQ37_spl
| ~ sQ1_spl
| ~ sQ16_spl
| is_a_theorem(implies(implies(X0,X1),implies(or(X0,X0),X1))) ),
inference(resolution,[status(thm)],[f1326,f476]) ).
fof(f1996,plain,
! [X0] :
( ~ sQ28_spl
| ~ sQ1_spl
| ~ sQ16_spl
| is_a_theorem(implies(X0,and(X0,X0))) ),
inference(resolution,[status(thm)],[f1326,f443]) ).
fof(f1997,plain,
! [X0] :
( ~ sQ13_spl
| ~ sQ1_spl
| ~ sQ16_spl
| is_a_theorem(implies(X0,X0)) ),
inference(resolution,[status(thm)],[f1326,f388]) ).
fof(f2002,plain,
( ~ sQ28_spl
| ~ sQ1_spl
| ~ sQ16_spl
| sQ49_spl ),
inference(split_clause,[status(thm)],[f1996,f519,f398,f342,f442]) ).
fof(f2114,plain,
( sQ11_spl
| ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ10_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1349,f1381]) ).
fof(f2115,plain,
( sQ11_spl
| ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ10_spl ),
inference(contradiction_clause,[status(thm)],[f2114]) ).
fof(f3256,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ sQ37_spl
| ~ sQ16_spl
| is_a_theorem(implies(or(X0,X0),X1))
| ~ is_a_theorem(implies(X0,X1)) ),
inference(resolution,[status(thm)],[f1994,f343]) ).
fof(f3288,plain,
( sQ66_spl
| ~ sQ1_spl
| ~ sQ37_spl
| ~ sQ16_spl
| ~ is_a_theorem(implies(sK44_skl,sK44_skl)) ),
inference(resolution,[status(thm)],[f3256,f585]) ).
fof(f3289,plain,
( sQ63_spl
| ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ1_spl
| ~ sQ37_spl
| ~ sQ16_spl
| ~ is_a_theorem(implies(sK43_skl,sK43_skl)) ),
inference(resolution,[status(thm)],[f3256,f1563]) ).
fof(f3294,plain,
( sQ66_spl
| ~ sQ1_spl
| ~ sQ37_spl
| ~ sQ16_spl
| ~ sQ13_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3288,f1997]) ).
fof(f3295,plain,
( sQ66_spl
| ~ sQ1_spl
| ~ sQ37_spl
| ~ sQ16_spl
| ~ sQ13_spl ),
inference(contradiction_clause,[status(thm)],[f3294]) ).
fof(f3296,plain,
( sQ63_spl
| ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ1_spl
| ~ sQ37_spl
| ~ sQ16_spl
| ~ sQ13_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3289,f1997]) ).
fof(f3297,plain,
( sQ63_spl
| ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ1_spl
| ~ sQ37_spl
| ~ sQ16_spl
| ~ sQ13_spl ),
inference(contradiction_clause,[status(thm)],[f3296]) ).
fof(f3310,plain,
! [X0] :
( ~ sQ119_spl
| ~ sQ87_spl
| ~ sQ98_spl
| is_a_theorem(equiv(necessarily(possibly(X0)),possibly(X0)))
| ~ is_a_theorem(implies(necessarily(possibly(X0)),possibly(X0))) ),
inference(resolution,[status(thm)],[f1344,f779]) ).
fof(f3318,plain,
! [X0] :
( ~ sQ65_spl
| ~ sQ87_spl
| ~ sQ98_spl
| is_a_theorem(equiv(X0,or(X0,X0)))
| ~ is_a_theorem(implies(X0,or(X0,X0))) ),
inference(resolution,[status(thm)],[f1344,f580]) ).
fof(f3338,plain,
! [X0] :
( ~ sQ49_spl
| ~ sQ87_spl
| ~ sQ98_spl
| is_a_theorem(equiv(and(X0,X0),X0))
| ~ is_a_theorem(implies(and(X0,X0),X0)) ),
inference(resolution,[status(thm)],[f1344,f520]) ).
fof(f3343,plain,
! [X0] :
( ~ sQ119_spl
| ~ sQ87_spl
| ~ sQ98_spl
| ~ sQ110_spl
| is_a_theorem(equiv(necessarily(possibly(X0)),possibly(X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[f3310,f746]) ).
fof(f3345,plain,
! [X0] :
( ~ sQ65_spl
| ~ sQ87_spl
| ~ sQ98_spl
| ~ sQ34_spl
| is_a_theorem(equiv(X0,or(X0,X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[f3318,f465]) ).
fof(f3349,plain,
! [X0] :
( ~ sQ49_spl
| ~ sQ87_spl
| ~ sQ98_spl
| ~ sQ22_spl
| is_a_theorem(equiv(and(X0,X0),X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f3338,f421]) ).
fof(f3414,plain,
! [X0] :
( ~ sQ6_spl
| ~ sQ65_spl
| ~ sQ87_spl
| ~ sQ98_spl
| ~ sQ34_spl
| X0 = or(X0,X0) ),
inference(resolution,[status(thm)],[f3345,f362]) ).
fof(f3455,plain,
! [X0] :
( ~ sQ6_spl
| ~ sQ49_spl
| ~ sQ87_spl
| ~ sQ98_spl
| ~ sQ22_spl
| and(X0,X0) = X0 ),
inference(resolution,[status(thm)],[f3349,f362]) ).
fof(f3470,plain,
! [X0] :
( ~ sQ6_spl
| ~ sQ49_spl
| ~ sQ87_spl
| ~ sQ98_spl
| ~ sQ22_spl
| ~ sQ83_spl
| implies(not(X0),X0) = not(not(X0)) ),
inference(paramodulation,[status(thm)],[f3455,f646]) ).
fof(f3488,plain,
! [X0] :
( ~ sQ6_spl
| ~ sQ49_spl
| ~ sQ87_spl
| ~ sQ98_spl
| ~ sQ22_spl
| ~ sQ83_spl
| ~ sQ79_spl
| or(X0,X0) = not(not(X0)) ),
inference(forward_demodulation,[status(thm)],[f1353,f3470]) ).
fof(f3489,plain,
! [X0] :
( ~ sQ6_spl
| ~ sQ49_spl
| ~ sQ87_spl
| ~ sQ98_spl
| ~ sQ22_spl
| ~ sQ83_spl
| ~ sQ79_spl
| ~ sQ65_spl
| ~ sQ34_spl
| X0 = not(not(X0)) ),
inference(forward_demodulation,[status(thm)],[f3414,f3488]) ).
fof(f3519,plain,
! [X0,X1] :
( ~ sQ6_spl
| ~ sQ49_spl
| ~ sQ87_spl
| ~ sQ98_spl
| ~ sQ22_spl
| ~ sQ83_spl
| ~ sQ79_spl
| ~ sQ65_spl
| ~ sQ34_spl
| or(not(X0),X1) = implies(X0,X1) ),
inference(paramodulation,[status(thm)],[f3489,f1353]) ).
fof(f3520,plain,
! [X0] :
( ~ sQ6_spl
| ~ sQ49_spl
| ~ sQ87_spl
| ~ sQ98_spl
| ~ sQ22_spl
| ~ sQ83_spl
| ~ sQ79_spl
| ~ sQ65_spl
| ~ sQ34_spl
| ~ sQ164_spl
| possibly(not(X0)) = not(necessarily(X0)) ),
inference(paramodulation,[status(thm)],[f3489,f944]) ).
fof(f3527,plain,
( ~ sQ6_spl
| ~ sQ49_spl
| ~ sQ87_spl
| ~ sQ98_spl
| ~ sQ22_spl
| ~ sQ83_spl
| ~ sQ79_spl
| ~ sQ65_spl
| ~ sQ34_spl
| sQ85_spl ),
inference(split_clause,[status(thm)],[f3519,f652,f464,f579,f631,f645,f420,f700,f659,f519,f361]) ).
fof(f3529,plain,
( ~ sQ43_spl
| ~ sQ172_spl ),
inference(contradiction_clause,[status(thm)],[f1165]) ).
fof(f4094,plain,
! [X0] :
( ~ sQ6_spl
| ~ sQ119_spl
| ~ sQ87_spl
| ~ sQ98_spl
| ~ sQ110_spl
| necessarily(possibly(X0)) = possibly(X0) ),
inference(resolution,[status(thm)],[f3343,f362]) ).
fof(f4096,plain,
( sQ117_spl
| ~ sQ6_spl
| ~ sQ119_spl
| ~ sQ87_spl
| ~ sQ98_spl
| ~ sQ110_spl
| ~ is_a_theorem(implies(sK66_skl,possibly(sK66_skl))) ),
inference(backward_demodulation,[status(thm)],[f4094,f773]) ).
fof(f4248,plain,
! [X0,X1] :
( ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ10_spl
| ~ sQ6_spl
| ~ sQ49_spl
| ~ sQ87_spl
| ~ sQ98_spl
| ~ sQ22_spl
| ~ sQ65_spl
| ~ sQ34_spl
| is_a_theorem(implies(or(X0,X1),or(X1,X0))) ),
inference(forward_demodulation,[status(thm)],[f3489,f1387]) ).
fof(f4249,plain,
! [X0,X1] :
( ~ sQ87_spl
| ~ sQ98_spl
| ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ10_spl
| ~ sQ6_spl
| ~ sQ49_spl
| ~ sQ22_spl
| ~ sQ65_spl
| ~ sQ34_spl
| is_a_theorem(equiv(or(X0,X1),or(X1,X0)))
| ~ is_a_theorem(implies(or(X0,X1),or(X1,X0))) ),
inference(resolution,[status(thm)],[f4248,f1344]) ).
fof(f4261,plain,
! [X0,X1] :
( ~ sQ87_spl
| ~ sQ98_spl
| ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ10_spl
| ~ sQ6_spl
| ~ sQ49_spl
| ~ sQ22_spl
| ~ sQ65_spl
| ~ sQ34_spl
| is_a_theorem(equiv(or(X0,X1),or(X1,X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[f4249,f4248]) ).
fof(f4996,plain,
! [X0,X1] :
( ~ sQ6_spl
| ~ sQ87_spl
| ~ sQ98_spl
| ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ10_spl
| ~ sQ49_spl
| ~ sQ22_spl
| ~ sQ65_spl
| ~ sQ34_spl
| or(X0,X1) = or(X1,X0) ),
inference(resolution,[status(thm)],[f4261,f362]) ).
fof(f5012,plain,
! [X0,X1] :
( ~ sQ85_spl
| ~ sQ6_spl
| ~ sQ87_spl
| ~ sQ98_spl
| ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ10_spl
| ~ sQ49_spl
| ~ sQ22_spl
| ~ sQ65_spl
| ~ sQ34_spl
| implies(X0,X1) = or(X1,not(X0)) ),
inference(paramodulation,[status(thm)],[f653,f4996]) ).
fof(f5152,plain,
! [X0,X1] :
( ~ sQ85_spl
| ~ sQ6_spl
| ~ sQ87_spl
| ~ sQ98_spl
| ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ10_spl
| ~ sQ49_spl
| ~ sQ22_spl
| ~ sQ65_spl
| ~ sQ34_spl
| implies(X0,not(X1)) = implies(X1,not(X0)) ),
inference(paramodulation,[status(thm)],[f653,f5012]) ).
fof(f5413,plain,
! [X0] :
( ~ sQ85_spl
| ~ sQ6_spl
| ~ sQ87_spl
| ~ sQ98_spl
| ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ10_spl
| ~ sQ49_spl
| ~ sQ22_spl
| ~ sQ65_spl
| ~ sQ34_spl
| ~ sQ110_spl
| is_a_theorem(implies(X0,not(necessarily(not(X0))))) ),
inference(paramodulation,[status(thm)],[f5152,f746]) ).
fof(f5524,plain,
! [X0] :
( ~ sQ85_spl
| ~ sQ6_spl
| ~ sQ87_spl
| ~ sQ98_spl
| ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ10_spl
| ~ sQ49_spl
| ~ sQ22_spl
| ~ sQ65_spl
| ~ sQ34_spl
| ~ sQ110_spl
| ~ sQ164_spl
| is_a_theorem(implies(X0,possibly(not(not(X0))))) ),
inference(forward_demodulation,[status(thm)],[f3520,f5413]) ).
fof(f5525,plain,
! [X0] :
( ~ sQ85_spl
| ~ sQ6_spl
| ~ sQ87_spl
| ~ sQ98_spl
| ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ10_spl
| ~ sQ49_spl
| ~ sQ22_spl
| ~ sQ65_spl
| ~ sQ34_spl
| ~ sQ110_spl
| ~ sQ164_spl
| is_a_theorem(implies(X0,possibly(X0))) ),
inference(forward_demodulation,[status(thm)],[f3489,f5524]) ).
fof(f5574,plain,
( sQ117_spl
| ~ sQ6_spl
| ~ sQ119_spl
| ~ sQ87_spl
| ~ sQ98_spl
| ~ sQ110_spl
| ~ sQ85_spl
| ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ10_spl
| ~ sQ49_spl
| ~ sQ22_spl
| ~ sQ65_spl
| ~ sQ34_spl
| ~ sQ164_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f4096,f5525]) ).
fof(f5582,plain,
( sQ117_spl
| ~ sQ6_spl
| ~ sQ119_spl
| ~ sQ87_spl
| ~ sQ98_spl
| ~ sQ110_spl
| ~ sQ85_spl
| ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ10_spl
| ~ sQ49_spl
| ~ sQ22_spl
| ~ sQ65_spl
| ~ sQ34_spl
| ~ sQ164_spl ),
inference(contradiction_clause,[status(thm)],[f5574]) ).
fof(f5585,plain,
( ~ sQ115_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f765,f338]) ).
fof(f5586,plain,
~ sQ115_spl,
inference(contradiction_clause,[status(thm)],[f5585]) ).
fof(f5587,plain,
$false,
inference(sat_refutation,[status(thm)],[f345,f364,f379,f390,f401,f412,f423,f434,f445,f456,f467,f478,f489,f500,f511,f526,f534,f553,f560,f564,f571,f575,f582,f586,f594,f634,f648,f662,f669,f703,f707,f711,f715,f737,f748,f774,f781,f946,f969,f971,f973,f975,f977,f979,f981,f987,f989,f1004,f1006,f1008,f1012,f1014,f1016,f1020,f1022,f1024,f1026,f1028,f1030,f1054,f1125,f1127,f1138,f1140,f1155,f1159,f1161,f1163,f1249,f1251,f1294,f1296,f1298,f1311,f1313,f1316,f1318,f1327,f1329,f1372,f1591,f1593,f1594,f1772,f2002,f2115,f3295,f3297,f3527,f3529,f5582,f5586]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL524+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/0.38 % Computer : n013.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Mon Sep 21 00:36:51 UTC 2026
% 0.12/0.38 % CPUTime :
% 0.12/0.39 % Drodi V4.1.1
% 0.12/0.62 % Refutation found
% 0.12/0.62 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.12/0.62 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.95/0.66 % Elapsed time: 0.264681 seconds
% 0.95/0.66 % CPU time: 1.773665 seconds
% 0.95/0.66 % Total memory used: 118.508 MB
% 0.95/0.66 % Net memory used: 116.121 MB
%------------------------------------------------------------------------------