%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : LCL504+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n020.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:52 PM UTC 2026
% Result : Theorem 143.58s 18.59s
% Output : CNFRefutation 36.76s
% Verified :
% SZS Type : Refutation
% Derivation depth : 44
% Number of leaves : 45
% Syntax : Number of formulae : 270 ( 29 unt; 26 def)
% Number of atoms : 1289 ( 33 equ)
% Maximal formula atoms : 13 ( 4 avg)
% Number of connectives : 1969 ( 950 ~; 955 |; 24 &)
% ( 35 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 7 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 39 ( 37 usr; 37 prp; 0-2 aty)
% Number of functors : 19 ( 19 usr; 14 con; 0-2 aty)
% Number of variables : 415 ( 399 !; 16 ?)
% 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/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,axiom,
( substitution_of_equivalents
<=> ! [X,Y] :
( is_a_theorem(equiv(X,Y))
=> X = Y ) ),
file('/export/starexec/sandbox2/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/sandbox2/benchmark/theBenchmark.p') ).
fof(f16,axiom,
( kn1
<=> ! [P] : is_a_theorem(implies(P,and(P,P))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f17,axiom,
( kn2
<=> ! [P,Q] : is_a_theorem(implies(and(P,Q),P)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f18,axiom,
( kn3
<=> ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f24,axiom,
( r3
<=> ! [P,Q] : is_a_theorem(implies(or(P,Q),or(Q,P))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f27,axiom,
( op_or
=> ! [X,Y] : or(X,Y) = not(and(not(X),not(Y))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f29,axiom,
( op_implies_and
=> ! [X,Y] : implies(X,Y) = not(and(X,not(Y))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f31,axiom,
( op_equiv
=> ! [X,Y] : equiv(X,Y) = and(implies(X,Y),implies(Y,X)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f32,axiom,
op_or,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f33,axiom,
op_implies_and,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f34,axiom,
op_equiv,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f35,axiom,
modus_ponens,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f36,axiom,
kn1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f37,axiom,
kn2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f38,axiom,
kn3,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f39,axiom,
substitution_of_equivalents,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f43,conjecture,
implies_2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f44,negated_conjecture,
~ implies_2,
inference(negated_conjecture,[status(cth)],[f43]) ).
fof(f45,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(f46,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)],[f45]) ).
fof(f47,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)],[f46]) ).
fof(f48,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)],[f47]) ).
fof(f49,plain,
! [X0,X1] :
( is_a_theorem(X1)
| ~ is_a_theorem(implies(X0,X1))
| ~ is_a_theorem(X0)
| ~ modus_ponens ),
inference(cnf_transformation,[status(thm)],[f48]) ).
fof(f53,plain,
( substitution_of_equivalents
<=> ! [X,Y] :
( X = Y
| ~ is_a_theorem(equiv(X,Y)) ) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f54,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)],[f53]) ).
fof(f55,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)],[f54]) ).
fof(f56,plain,
! [X0,X1] :
( X0 = X1
| ~ is_a_theorem(equiv(X0,X1))
| ~ substitution_of_equivalents ),
inference(cnf_transformation,[status(thm)],[f55]) ).
fof(f67,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(f68,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)],[f67]) ).
fof(f70,plain,
( ~ is_a_theorem(implies(implies(sK8_skl,implies(sK8_skl,sK9_skl)),implies(sK8_skl,sK9_skl)))
| implies_2 ),
inference(cnf_transformation,[status(thm)],[f68]) ).
fof(f111,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(f112,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)],[f111]) ).
fof(f113,plain,
! [X0] :
( is_a_theorem(implies(X0,and(X0,X0)))
| ~ kn1 ),
inference(cnf_transformation,[status(thm)],[f112]) ).
fof(f115,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(f116,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)],[f115]) ).
fof(f117,plain,
! [X0,X1] :
( is_a_theorem(implies(and(X0,X1),X0))
| ~ kn2 ),
inference(cnf_transformation,[status(thm)],[f116]) ).
fof(f119,plain,
( ( ? [P,Q,R] : ~ is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P)))))
| kn3 )
& ( ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P)))))
| ~ kn3 ) ),
inference(NNF_transformation,[status(thm)],[f18]) ).
fof(f120,plain,
( ( ~ is_a_theorem(implies(implies(sK35_skl,sK36_skl),implies(not(and(sK36_skl,sK37_skl)),not(and(sK37_skl,sK35_skl)))))
| kn3 )
& ( ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P)))))
| ~ kn3 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK35_skl,sK36_skl,sK37_skl]),skolemize(P,sK35_skl),skolemize(Q,sK36_skl),skolemize(R,sK37_skl)],[f119]) ).
fof(f121,plain,
! [X0,X1,X2] :
( is_a_theorem(implies(implies(X0,X1),implies(not(and(X1,X2)),not(and(X2,X0)))))
| ~ kn3 ),
inference(cnf_transformation,[status(thm)],[f120]) ).
fof(f143,plain,
( ( ? [P,Q] : ~ is_a_theorem(implies(or(P,Q),or(Q,P)))
| r3 )
& ( ! [P,Q] : is_a_theorem(implies(or(P,Q),or(Q,P)))
| ~ r3 ) ),
inference(NNF_transformation,[status(thm)],[f24]) ).
fof(f144,plain,
( ( ~ is_a_theorem(implies(or(sK47_skl,sK48_skl),or(sK48_skl,sK47_skl)))
| r3 )
& ( ! [P,Q] : is_a_theorem(implies(or(P,Q),or(Q,P)))
| ~ r3 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK47_skl,sK48_skl]),skolemize(P,sK47_skl),skolemize(Q,sK48_skl)],[f143]) ).
fof(f145,plain,
! [X0,X1] :
( is_a_theorem(implies(or(X0,X1),or(X1,X0)))
| ~ r3 ),
inference(cnf_transformation,[status(thm)],[f144]) ).
fof(f146,plain,
( ~ is_a_theorem(implies(or(sK47_skl,sK48_skl),or(sK48_skl,sK47_skl)))
| r3 ),
inference(cnf_transformation,[status(thm)],[f144]) ).
fof(f155,plain,
( ! [X,Y] : or(X,Y) = not(and(not(X),not(Y)))
| ~ op_or ),
inference(pre_NNF_transformation,[status(thm)],[f27]) ).
fof(f156,plain,
! [X0,X1] :
( or(X0,X1) = not(and(not(X0),not(X1)))
| ~ op_or ),
inference(cnf_transformation,[status(thm)],[f155]) ).
fof(f159,plain,
( ! [X,Y] : implies(X,Y) = not(and(X,not(Y)))
| ~ op_implies_and ),
inference(pre_NNF_transformation,[status(thm)],[f29]) ).
fof(f160,plain,
! [X0,X1] :
( implies(X0,X1) = not(and(X0,not(X1)))
| ~ op_implies_and ),
inference(cnf_transformation,[status(thm)],[f159]) ).
fof(f163,plain,
( ! [X,Y] : equiv(X,Y) = and(implies(X,Y),implies(Y,X))
| ~ op_equiv ),
inference(pre_NNF_transformation,[status(thm)],[f31]) ).
fof(f164,plain,
! [X0,X1] :
( equiv(X0,X1) = and(implies(X0,X1),implies(X1,X0))
| ~ op_equiv ),
inference(cnf_transformation,[status(thm)],[f163]) ).
fof(f165,plain,
op_or,
inference(cnf_transformation,[status(thm)],[f32]) ).
fof(f166,plain,
op_implies_and,
inference(cnf_transformation,[status(thm)],[f33]) ).
fof(f167,plain,
op_equiv,
inference(cnf_transformation,[status(thm)],[f34]) ).
fof(f168,plain,
modus_ponens,
inference(cnf_transformation,[status(thm)],[f35]) ).
fof(f169,plain,
kn1,
inference(cnf_transformation,[status(thm)],[f36]) ).
fof(f170,plain,
kn2,
inference(cnf_transformation,[status(thm)],[f37]) ).
fof(f171,plain,
kn3,
inference(cnf_transformation,[status(thm)],[f38]) ).
fof(f172,plain,
substitution_of_equivalents,
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f176,plain,
~ implies_2,
inference(cnf_transformation,[status(thm)],[f44]) ).
fof(f177,definition,
( sQ0_spl
<=> modus_ponens ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f179,plain,
( sQ0_spl
| ~ modus_ponens ),
inference(component_clause,[status(thm)],[f177]) ).
fof(f180,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(f181,plain,
! [X0,X1] :
( ~ sQ1_spl
| is_a_theorem(X1)
| ~ is_a_theorem(implies(X0,X1))
| ~ is_a_theorem(X0) ),
inference(component_clause,[status(thm)],[f180]) ).
fof(f183,plain,
( sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f49,f177,f180]) ).
fof(f196,definition,
( sQ5_spl
<=> substitution_of_equivalents ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f198,plain,
( sQ5_spl
| ~ substitution_of_equivalents ),
inference(component_clause,[status(thm)],[f196]) ).
fof(f199,definition,
! [X0,X1] :
( sQ6_spl
<=> ( X0 = X1
| ~ is_a_theorem(equiv(X0,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f200,plain,
! [X0,X1] :
( ~ sQ6_spl
| X0 = X1
| ~ is_a_theorem(equiv(X0,X1)) ),
inference(component_clause,[status(thm)],[f199]) ).
fof(f202,plain,
( sQ6_spl
| ~ sQ5_spl ),
inference(split_clause,[status(thm)],[f56,f196,f199]) ).
fof(f233,definition,
( sQ15_spl
<=> implies_2 ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f234,plain,
( ~ sQ15_spl
| implies_2 ),
inference(component_clause,[status(thm)],[f233]) ).
fof(f236,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(f237,plain,
! [X0,X1] :
( ~ sQ16_spl
| is_a_theorem(implies(implies(X0,implies(X0,X1)),implies(X0,X1))) ),
inference(component_clause,[status(thm)],[f236]) ).
fof(f240,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(f242,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)],[f240]) ).
fof(f243,plain,
( ~ sQ17_spl
| sQ15_spl ),
inference(split_clause,[status(thm)],[f70,f233,f240]) ).
fof(f258,definition,
! [X0,X1] :
( sQ22_spl
<=> is_a_theorem(implies(and(X0,X1),X0)) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f259,plain,
! [X0,X1] :
( ~ sQ22_spl
| is_a_theorem(implies(and(X0,X1),X0)) ),
inference(component_clause,[status(thm)],[f258]) ).
fof(f291,definition,
! [X0,X1] :
( sQ31_spl
<=> is_a_theorem(implies(X0,or(X0,X1))) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f292,plain,
! [X0,X1] :
( ~ sQ31_spl
| is_a_theorem(implies(X0,or(X0,X1))) ),
inference(component_clause,[status(thm)],[f291]) ).
fof(f302,definition,
! [X0,X1] :
( sQ34_spl
<=> is_a_theorem(implies(X0,or(X1,X0))) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f303,plain,
! [X0,X1] :
( ~ sQ34_spl
| is_a_theorem(implies(X0,or(X1,X0))) ),
inference(component_clause,[status(thm)],[f302]) ).
fof(f354,definition,
( sQ48_spl
<=> kn1 ),
introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition]) ).
fof(f356,plain,
( sQ48_spl
| ~ kn1 ),
inference(component_clause,[status(thm)],[f354]) ).
fof(f357,definition,
! [X0] :
( sQ49_spl
<=> is_a_theorem(implies(X0,and(X0,X0))) ),
introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition]) ).
fof(f358,plain,
! [X0] :
( ~ sQ49_spl
| is_a_theorem(implies(X0,and(X0,X0))) ),
inference(component_clause,[status(thm)],[f357]) ).
fof(f360,plain,
( sQ49_spl
| ~ sQ48_spl ),
inference(split_clause,[status(thm)],[f113,f354,f357]) ).
fof(f365,definition,
( sQ51_spl
<=> kn2 ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f367,plain,
( sQ51_spl
| ~ kn2 ),
inference(component_clause,[status(thm)],[f365]) ).
fof(f368,plain,
( sQ22_spl
| ~ sQ51_spl ),
inference(split_clause,[status(thm)],[f117,f365,f258]) ).
fof(f373,definition,
( sQ53_spl
<=> kn3 ),
introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition]) ).
fof(f375,plain,
( sQ53_spl
| ~ kn3 ),
inference(component_clause,[status(thm)],[f373]) ).
fof(f376,definition,
! [X0,X1,X2] :
( sQ54_spl
<=> is_a_theorem(implies(implies(X0,X1),implies(not(and(X1,X2)),not(and(X2,X0))))) ),
introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition]) ).
fof(f377,plain,
! [X0,X1,X2] :
( ~ sQ54_spl
| is_a_theorem(implies(implies(X0,X1),implies(not(and(X1,X2)),not(and(X2,X0))))) ),
inference(component_clause,[status(thm)],[f376]) ).
fof(f379,plain,
( sQ54_spl
| ~ sQ53_spl ),
inference(split_clause,[status(thm)],[f121,f373,f376]) ).
fof(f417,definition,
! [X0] :
( sQ65_spl
<=> is_a_theorem(implies(or(X0,X0),X0)) ),
introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition]) ).
fof(f418,plain,
! [X0] :
( ~ sQ65_spl
| is_a_theorem(implies(or(X0,X0),X0)) ),
inference(component_clause,[status(thm)],[f417]) ).
fof(f433,definition,
( sQ69_spl
<=> r3 ),
introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition]) ).
fof(f436,definition,
! [X0,X1] :
( sQ70_spl
<=> is_a_theorem(implies(or(X0,X1),or(X1,X0))) ),
introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition]) ).
fof(f437,plain,
! [X0,X1] :
( ~ sQ70_spl
| is_a_theorem(implies(or(X0,X1),or(X1,X0))) ),
inference(component_clause,[status(thm)],[f436]) ).
fof(f439,plain,
( sQ70_spl
| ~ sQ69_spl ),
inference(split_clause,[status(thm)],[f145,f433,f436]) ).
fof(f440,definition,
( sQ71_spl
<=> is_a_theorem(implies(or(sK47_skl,sK48_skl),or(sK48_skl,sK47_skl))) ),
introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition]) ).
fof(f442,plain,
( sQ71_spl
| ~ is_a_theorem(implies(or(sK47_skl,sK48_skl),or(sK48_skl,sK47_skl))) ),
inference(component_clause,[status(thm)],[f440]) ).
fof(f443,plain,
( ~ sQ71_spl
| sQ69_spl ),
inference(split_clause,[status(thm)],[f146,f433,f440]) ).
fof(f466,definition,
( sQ78_spl
<=> op_or ),
introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition]) ).
fof(f468,plain,
( sQ78_spl
| ~ op_or ),
inference(component_clause,[status(thm)],[f466]) ).
fof(f469,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(f470,plain,
! [X0,X1] :
( ~ sQ79_spl
| or(X0,X1) = not(and(not(X0),not(X1))) ),
inference(component_clause,[status(thm)],[f469]) ).
fof(f472,plain,
( sQ79_spl
| ~ sQ78_spl ),
inference(split_clause,[status(thm)],[f156,f466,f469]) ).
fof(f480,definition,
( sQ82_spl
<=> op_implies_and ),
introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition]) ).
fof(f482,plain,
( sQ82_spl
| ~ op_implies_and ),
inference(component_clause,[status(thm)],[f480]) ).
fof(f483,definition,
! [X0,X1] :
( sQ83_spl
<=> implies(X0,X1) = not(and(X0,not(X1))) ),
introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition]) ).
fof(f484,plain,
! [X0,X1] :
( ~ sQ83_spl
| implies(X0,X1) = not(and(X0,not(X1))) ),
inference(component_clause,[status(thm)],[f483]) ).
fof(f486,plain,
( sQ83_spl
| ~ sQ82_spl ),
inference(split_clause,[status(thm)],[f160,f480,f483]) ).
fof(f494,definition,
( sQ86_spl
<=> op_equiv ),
introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition]) ).
fof(f496,plain,
( sQ86_spl
| ~ op_equiv ),
inference(component_clause,[status(thm)],[f494]) ).
fof(f497,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(f498,plain,
! [X0,X1] :
( ~ sQ87_spl
| equiv(X0,X1) = and(implies(X0,X1),implies(X1,X0)) ),
inference(component_clause,[status(thm)],[f497]) ).
fof(f500,plain,
( sQ87_spl
| ~ sQ86_spl ),
inference(split_clause,[status(thm)],[f164,f494,f497]) ).
fof(f501,plain,
( sQ86_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f496,f167]) ).
fof(f502,plain,
sQ86_spl,
inference(contradiction_clause,[status(thm)],[f501]) ).
fof(f503,plain,
( sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f179,f168]) ).
fof(f504,plain,
sQ0_spl,
inference(contradiction_clause,[status(thm)],[f503]) ).
fof(f505,plain,
( sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f198,f172]) ).
fof(f506,plain,
sQ5_spl,
inference(contradiction_clause,[status(thm)],[f505]) ).
fof(f507,plain,
( sQ82_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f482,f166]) ).
fof(f508,plain,
sQ82_spl,
inference(contradiction_clause,[status(thm)],[f507]) ).
fof(f509,plain,
( sQ78_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f468,f165]) ).
fof(f510,plain,
sQ78_spl,
inference(contradiction_clause,[status(thm)],[f509]) ).
fof(f521,plain,
( sQ51_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f367,f170]) ).
fof(f522,plain,
sQ51_spl,
inference(contradiction_clause,[status(thm)],[f521]) ).
fof(f525,plain,
( sQ48_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f356,f169]) ).
fof(f526,plain,
sQ48_spl,
inference(contradiction_clause,[status(thm)],[f525]) ).
fof(f566,plain,
! [X0,X1,X2] :
( ~ sQ83_spl
| implies(X0,and(X1,not(X2))) = not(and(X0,implies(X1,X2))) ),
inference(paramodulation,[status(thm)],[f484,f484]) ).
fof(f568,plain,
! [X0,X1,X2] :
( ~ sQ83_spl
| ~ sQ54_spl
| is_a_theorem(implies(implies(X0,X1),implies(implies(X1,X2),not(and(not(X2),X0))))) ),
inference(paramodulation,[status(thm)],[f484,f377]) ).
fof(f569,plain,
! [X0,X1,X2] :
( ~ sQ83_spl
| ~ sQ54_spl
| is_a_theorem(implies(implies(not(X0),X1),implies(not(and(X1,X2)),implies(X2,X0)))) ),
inference(paramodulation,[status(thm)],[f484,f377]) ).
fof(f580,definition,
! [X0] :
( sQ90_spl
<=> ~ is_a_theorem(X0) ),
introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition]) ).
fof(f581,plain,
! [X0] :
( ~ sQ90_spl
| ~ is_a_theorem(X0) ),
inference(component_clause,[status(thm)],[f580]) ).
fof(f604,plain,
! [X0,X1,X2] :
( ~ sQ54_spl
| ~ sQ79_spl
| ~ sQ83_spl
| is_a_theorem(implies(implies(X0,X1),or(and(X1,X2),not(and(X2,X0))))) ),
inference(backward_demodulation,[status(thm)],[f605,f377]) ).
fof(f605,plain,
! [X0,X1] :
( ~ sQ79_spl
| ~ sQ83_spl
| or(X0,X1) = implies(not(X0),X1) ),
inference(forward_demodulation,[status(thm)],[f484,f470]) ).
fof(f606,plain,
! [X0,X1,X2] :
( ~ sQ83_spl
| ~ sQ79_spl
| or(and(X0,not(X1)),X2) = implies(implies(X0,X1),X2) ),
inference(paramodulation,[status(thm)],[f484,f605]) ).
fof(f607,plain,
! [X0] :
( ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ49_spl
| is_a_theorem(or(X0,and(not(X0),not(X0)))) ),
inference(paramodulation,[status(thm)],[f605,f358]) ).
fof(f613,plain,
! [X0,X1] :
( ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ87_spl
| equiv(X0,not(X1)) = and(implies(X0,not(X1)),or(X1,X0)) ),
inference(paramodulation,[status(thm)],[f605,f498]) ).
fof(f615,plain,
! [X0,X1] :
( ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ1_spl
| is_a_theorem(X1)
| ~ is_a_theorem(or(X0,X1))
| ~ is_a_theorem(not(X0)) ),
inference(paramodulation,[status(thm)],[f605,f181]) ).
fof(f654,plain,
( sQ17_spl
| ~ sQ16_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f242,f237]) ).
fof(f655,plain,
( sQ17_spl
| ~ sQ16_spl ),
inference(contradiction_clause,[status(thm)],[f654]) ).
fof(f688,plain,
! [X0] :
( ~ sQ83_spl
| ~ sQ49_spl
| is_a_theorem(not(and(not(X0),implies(not(X0),X0)))) ),
inference(paramodulation,[status(thm)],[f566,f358]) ).
fof(f696,plain,
! [X0] :
( ~ sQ83_spl
| ~ sQ49_spl
| ~ sQ79_spl
| is_a_theorem(not(and(not(X0),or(X0,X0)))) ),
inference(forward_demodulation,[status(thm)],[f605,f688]) ).
fof(f698,plain,
! [X0,X1] :
( ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ1_spl
| ~ sQ49_spl
| is_a_theorem(X1)
| ~ is_a_theorem(or(and(not(X0),or(X0,X0)),X1)) ),
inference(resolution,[status(thm)],[f696,f615]) ).
fof(f786,plain,
! [X0,X1,X2] :
( ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ54_spl
| is_a_theorem(implies(or(X0,X1),or(and(X1,X2),not(and(X2,not(X0)))))) ),
inference(paramodulation,[status(thm)],[f605,f604]) ).
fof(f796,plain,
! [X0,X1,X2] :
( ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ54_spl
| is_a_theorem(implies(or(X0,X1),or(and(X1,X2),implies(X2,X0)))) ),
inference(forward_demodulation,[status(thm)],[f484,f786]) ).
fof(f799,plain,
! [X0,X1,X2] :
( ~ sQ1_spl
| ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ54_spl
| is_a_theorem(or(and(X1,X2),implies(X2,X0)))
| ~ is_a_theorem(or(X0,X1)) ),
inference(resolution,[status(thm)],[f796,f181]) ).
fof(f801,plain,
! [X0,X1,X2] :
( ~ sQ83_spl
| ~ sQ79_spl
| ~ sQ54_spl
| is_a_theorem(implies(or(X0,X1),implies(implies(X1,X2),implies(not(X2),X0)))) ),
inference(paramodulation,[status(thm)],[f606,f796]) ).
fof(f808,plain,
! [X0,X1,X2] :
( ~ sQ83_spl
| ~ sQ79_spl
| ~ sQ54_spl
| is_a_theorem(implies(or(X0,X1),implies(implies(X1,X2),or(X2,X0)))) ),
inference(forward_demodulation,[status(thm)],[f605,f801]) ).
fof(f814,plain,
! [X0,X1,X2] :
( ~ sQ1_spl
| ~ sQ83_spl
| ~ sQ79_spl
| ~ sQ54_spl
| is_a_theorem(implies(implies(X1,X2),or(X2,X0)))
| ~ is_a_theorem(or(X0,X1)) ),
inference(resolution,[status(thm)],[f808,f181]) ).
fof(f823,plain,
! [X0,X1] :
( ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ49_spl
| ~ sQ1_spl
| ~ sQ54_spl
| is_a_theorem(implies(implies(and(not(X0),not(X0)),X1),or(X1,X0))) ),
inference(resolution,[status(thm)],[f814,f607]) ).
fof(f840,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ49_spl
| ~ sQ54_spl
| is_a_theorem(or(X1,X0))
| ~ is_a_theorem(implies(and(not(X0),not(X0)),X1)) ),
inference(resolution,[status(thm)],[f823,f181]) ).
fof(f851,plain,
! [X0] :
( ~ sQ22_spl
| ~ sQ1_spl
| ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ49_spl
| ~ sQ54_spl
| is_a_theorem(or(not(X0),X0)) ),
inference(resolution,[status(thm)],[f840,f259]) ).
fof(f859,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ sQ83_spl
| ~ sQ79_spl
| ~ sQ54_spl
| ~ sQ22_spl
| ~ sQ49_spl
| is_a_theorem(implies(implies(X0,X1),or(X1,not(X0)))) ),
inference(resolution,[status(thm)],[f851,f814]) ).
fof(f860,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ54_spl
| ~ sQ22_spl
| ~ sQ49_spl
| is_a_theorem(or(and(X0,X1),implies(X1,not(X0)))) ),
inference(resolution,[status(thm)],[f851,f799]) ).
fof(f862,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ sQ83_spl
| ~ sQ79_spl
| ~ sQ54_spl
| ~ sQ22_spl
| ~ sQ49_spl
| is_a_theorem(or(X1,not(X0)))
| ~ is_a_theorem(implies(X0,X1)) ),
inference(resolution,[status(thm)],[f859,f181]) ).
fof(f871,plain,
! [X0] :
( ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ1_spl
| ~ sQ49_spl
| ~ sQ54_spl
| ~ sQ22_spl
| is_a_theorem(implies(or(X0,X0),not(not(X0)))) ),
inference(resolution,[status(thm)],[f860,f698]) ).
fof(f882,plain,
! [X0] :
( ~ sQ1_spl
| ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ49_spl
| ~ sQ54_spl
| ~ sQ22_spl
| is_a_theorem(not(not(X0)))
| ~ is_a_theorem(or(X0,X0)) ),
inference(resolution,[status(thm)],[f871,f181]) ).
fof(f904,plain,
! [X0,X1,X2] :
( ~ sQ1_spl
| ~ sQ83_spl
| ~ sQ79_spl
| ~ sQ54_spl
| ~ sQ22_spl
| ~ sQ49_spl
| is_a_theorem(implies(implies(not(X0),X2),or(X2,X1)))
| ~ is_a_theorem(implies(X0,X1)) ),
inference(resolution,[status(thm)],[f862,f814]) ).
fof(f908,plain,
! [X0,X1,X2] :
( ~ sQ83_spl
| ~ sQ1_spl
| ~ sQ79_spl
| ~ sQ54_spl
| ~ sQ22_spl
| ~ sQ49_spl
| is_a_theorem(or(X2,implies(X0,X1)))
| ~ is_a_theorem(implies(and(X0,not(X1)),X2)) ),
inference(paramodulation,[status(thm)],[f484,f862]) ).
fof(f909,plain,
! [X0,X1,X2] :
( ~ sQ1_spl
| ~ sQ83_spl
| ~ sQ79_spl
| ~ sQ54_spl
| ~ sQ22_spl
| ~ sQ49_spl
| is_a_theorem(implies(or(X0,X2),or(X2,X1)))
| ~ is_a_theorem(implies(X0,X1)) ),
inference(forward_demodulation,[status(thm)],[f605,f904]) ).
fof(f943,plain,
! [X0,X1,X2] :
( ~ sQ1_spl
| ~ sQ83_spl
| ~ sQ54_spl
| is_a_theorem(implies(implies(X1,X2),not(and(not(X2),X0))))
| ~ is_a_theorem(implies(X0,X1)) ),
inference(resolution,[status(thm)],[f568,f181]) ).
fof(f959,plain,
( sQ71_spl
| ~ sQ1_spl
| ~ sQ83_spl
| ~ sQ79_spl
| ~ sQ54_spl
| ~ sQ22_spl
| ~ sQ49_spl
| ~ is_a_theorem(implies(sK47_skl,sK47_skl)) ),
inference(resolution,[status(thm)],[f909,f442]) ).
fof(f1027,plain,
( sQ53_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f375,f171]) ).
fof(f1028,plain,
sQ53_spl,
inference(contradiction_clause,[status(thm)],[f1027]) ).
fof(f1029,plain,
! [X0,X1,X2] :
( ~ sQ83_spl
| ~ sQ54_spl
| ~ sQ79_spl
| is_a_theorem(implies(or(X0,X1),implies(not(and(X1,X2)),implies(X2,X0)))) ),
inference(forward_demodulation,[status(thm)],[f605,f569]) ).
fof(f1030,plain,
! [X0,X1,X2] :
( ~ sQ83_spl
| ~ sQ54_spl
| ~ sQ79_spl
| is_a_theorem(implies(or(X0,X1),or(and(X1,X2),implies(X2,X0)))) ),
inference(forward_demodulation,[status(thm)],[f605,f1029]) ).
fof(f1219,plain,
! [X0,X1] :
( ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ1_spl
| ~ sQ49_spl
| ~ sQ54_spl
| is_a_theorem(implies(or(X1,X1),X0))
| ~ is_a_theorem(or(X0,not(X1))) ),
inference(resolution,[status(thm)],[f799,f698]) ).
fof(f1232,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ sQ83_spl
| ~ sQ79_spl
| ~ sQ54_spl
| ~ sQ22_spl
| ~ sQ49_spl
| ~ is_a_theorem(implies(X0,X1))
| is_a_theorem(implies(or(X0,X0),X1)) ),
inference(resolution,[status(thm)],[f1219,f862]) ).
fof(f1244,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ sQ83_spl
| ~ sQ79_spl
| ~ sQ54_spl
| ~ sQ22_spl
| ~ sQ49_spl
| is_a_theorem(X1)
| ~ is_a_theorem(or(X0,X0))
| ~ is_a_theorem(implies(X0,X1)) ),
inference(resolution,[status(thm)],[f1232,f181]) ).
fof(f1286,plain,
! [X0,X1,X2] :
( ~ sQ1_spl
| ~ sQ83_spl
| ~ sQ79_spl
| ~ sQ54_spl
| is_a_theorem(or(X2,X0))
| ~ is_a_theorem(implies(X1,X2))
| ~ is_a_theorem(or(X0,X1)) ),
inference(resolution,[status(thm)],[f814,f181]) ).
fof(f1970,plain,
! [X0,X1] :
( ~ sQ22_spl
| ~ sQ83_spl
| ~ sQ1_spl
| ~ sQ79_spl
| ~ sQ54_spl
| ~ sQ49_spl
| is_a_theorem(or(X0,implies(X0,X1))) ),
inference(resolution,[status(thm)],[f908,f259]) ).
fof(f1981,plain,
! [X0,X1,X2] :
( ~ sQ83_spl
| ~ sQ79_spl
| ~ sQ22_spl
| ~ sQ1_spl
| ~ sQ54_spl
| ~ sQ49_spl
| is_a_theorem(implies(implies(X0,X1),implies(and(X0,not(X1)),X2))) ),
inference(paramodulation,[status(thm)],[f606,f1970]) ).
fof(f1982,plain,
! [X0,X1] :
( ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ22_spl
| ~ sQ1_spl
| ~ sQ54_spl
| ~ sQ49_spl
| is_a_theorem(or(not(X0),or(X0,X1))) ),
inference(paramodulation,[status(thm)],[f605,f1970]) ).
fof(f2095,plain,
! [X0,X1,X2] :
( ~ sQ1_spl
| ~ sQ83_spl
| ~ sQ79_spl
| ~ sQ22_spl
| ~ sQ54_spl
| ~ sQ49_spl
| is_a_theorem(implies(and(X0,not(X1)),X2))
| ~ is_a_theorem(implies(X0,X1)) ),
inference(resolution,[status(thm)],[f1981,f181]) ).
fof(f2106,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ49_spl
| ~ sQ54_spl
| ~ sQ22_spl
| is_a_theorem(or(X1,X0))
| ~ is_a_theorem(implies(not(X0),X0)) ),
inference(resolution,[status(thm)],[f2095,f840]) ).
fof(f2119,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ49_spl
| ~ sQ54_spl
| ~ sQ22_spl
| is_a_theorem(or(X1,X0))
| ~ is_a_theorem(or(X0,X0)) ),
inference(forward_demodulation,[status(thm)],[f605,f2106]) ).
fof(f2157,plain,
! [X0,X1,X2] :
( ~ sQ1_spl
| ~ sQ83_spl
| ~ sQ79_spl
| ~ sQ54_spl
| ~ sQ49_spl
| ~ sQ22_spl
| ~ is_a_theorem(implies(X2,X1))
| ~ is_a_theorem(or(X1,X2))
| is_a_theorem(or(X0,X1)) ),
inference(resolution,[status(thm)],[f2119,f1286]) ).
fof(f2358,plain,
! [X0,X1] :
( ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ1_spl
| ~ sQ49_spl
| ~ sQ54_spl
| ~ sQ22_spl
| is_a_theorem(X0)
| ~ is_a_theorem(implies(X1,X0))
| ~ is_a_theorem(or(X0,X1)) ),
inference(resolution,[status(thm)],[f2157,f698]) ).
fof(f2388,plain,
! [X0,X1] :
( ~ sQ22_spl
| ~ sQ83_spl
| ~ sQ1_spl
| ~ sQ79_spl
| ~ sQ54_spl
| ~ sQ49_spl
| is_a_theorem(X0)
| ~ is_a_theorem(implies(implies(X0,X1),X0)) ),
inference(resolution,[status(thm)],[f2358,f1970]) ).
fof(f2393,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ sQ83_spl
| ~ sQ79_spl
| ~ sQ54_spl
| ~ sQ22_spl
| ~ sQ49_spl
| ~ is_a_theorem(implies(X0,X1))
| is_a_theorem(X1)
| ~ is_a_theorem(implies(not(X0),X1)) ),
inference(resolution,[status(thm)],[f2358,f862]) ).
fof(f2408,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ sQ83_spl
| ~ sQ79_spl
| ~ sQ54_spl
| ~ sQ22_spl
| ~ sQ49_spl
| ~ is_a_theorem(implies(X0,X1))
| is_a_theorem(X1)
| ~ is_a_theorem(or(X0,X1)) ),
inference(forward_demodulation,[status(thm)],[f605,f2393]) ).
fof(f2410,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ sQ83_spl
| ~ sQ79_spl
| ~ sQ54_spl
| ~ sQ22_spl
| ~ sQ49_spl
| ~ is_a_theorem(or(X1,or(X0,X1)))
| is_a_theorem(or(X0,X1)) ),
inference(resolution,[status(thm)],[f2388,f814]) ).
fof(f2501,plain,
! [X0] :
( ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ22_spl
| ~ sQ1_spl
| ~ sQ54_spl
| ~ sQ49_spl
| is_a_theorem(or(X0,not(X0))) ),
inference(resolution,[status(thm)],[f2410,f1982]) ).
fof(f2511,plain,
! [X0] :
( ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ1_spl
| ~ sQ49_spl
| ~ sQ54_spl
| ~ sQ22_spl
| is_a_theorem(implies(or(X0,X0),X0)) ),
inference(resolution,[status(thm)],[f2501,f1219]) ).
fof(f2519,plain,
( ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ1_spl
| ~ sQ49_spl
| ~ sQ54_spl
| ~ sQ22_spl
| sQ65_spl ),
inference(split_clause,[status(thm)],[f2511,f417,f258,f376,f357,f180,f483,f469]) ).
fof(f3044,plain,
! [X0,X1] :
( ~ sQ22_spl
| ~ sQ1_spl
| ~ sQ83_spl
| ~ sQ79_spl
| ~ sQ54_spl
| ~ sQ49_spl
| is_a_theorem(X0)
| ~ is_a_theorem(or(and(X0,X1),X0)) ),
inference(resolution,[status(thm)],[f2408,f259]) ).
fof(f3051,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ54_spl
| ~ sQ22_spl
| ~ sQ49_spl
| ~ is_a_theorem(or(X1,implies(X0,X1)))
| is_a_theorem(implies(X0,X1)) ),
inference(resolution,[status(thm)],[f3044,f799]) ).
fof(f3154,plain,
! [X0] :
( ~ sQ22_spl
| ~ sQ83_spl
| ~ sQ1_spl
| ~ sQ79_spl
| ~ sQ54_spl
| ~ sQ49_spl
| is_a_theorem(implies(X0,X0)) ),
inference(resolution,[status(thm)],[f3051,f1970]) ).
fof(f3163,plain,
( sQ71_spl
| ~ sQ1_spl
| ~ sQ83_spl
| ~ sQ79_spl
| ~ sQ54_spl
| ~ sQ22_spl
| ~ sQ49_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f959,f3154]) ).
fof(f3171,plain,
( sQ71_spl
| ~ sQ1_spl
| ~ sQ83_spl
| ~ sQ79_spl
| ~ sQ54_spl
| ~ sQ22_spl
| ~ sQ49_spl ),
inference(contradiction_clause,[status(thm)],[f3163]) ).
fof(f3178,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ sQ70_spl
| is_a_theorem(or(X1,X0))
| ~ is_a_theorem(or(X0,X1)) ),
inference(resolution,[status(thm)],[f437,f181]) ).
fof(f3186,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ54_spl
| ~ sQ22_spl
| ~ sQ49_spl
| ~ sQ70_spl
| is_a_theorem(implies(X0,X1))
| ~ is_a_theorem(or(implies(X0,X1),X1)) ),
inference(resolution,[status(thm)],[f3178,f3051]) ).
fof(f3252,plain,
( ~ sQ1_spl
| ~ sQ83_spl
| ~ sQ79_spl
| ~ sQ54_spl
| ~ sQ22_spl
| ~ sQ49_spl
| ~ sQ90_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f859,f581]) ).
fof(f3294,plain,
( ~ sQ1_spl
| ~ sQ83_spl
| ~ sQ79_spl
| ~ sQ54_spl
| ~ sQ22_spl
| ~ sQ49_spl
| ~ sQ90_spl ),
inference(contradiction_clause,[status(thm)],[f3252]) ).
fof(f3322,plain,
! [X0,X1] :
( ~ sQ22_spl
| ~ sQ83_spl
| ~ sQ1_spl
| ~ sQ79_spl
| ~ sQ54_spl
| ~ sQ49_spl
| is_a_theorem(X1)
| ~ is_a_theorem(implies(implies(X0,X0),X1)) ),
inference(resolution,[status(thm)],[f181,f3154]) ).
fof(f3325,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ sQ22_spl
| ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ49_spl
| ~ sQ54_spl
| is_a_theorem(X1)
| ~ is_a_theorem(implies(or(not(X0),X0),X1)) ),
inference(resolution,[status(thm)],[f851,f181]) ).
fof(f3346,plain,
! [X0,X1,X2] :
( ~ sQ1_spl
| ~ sQ22_spl
| is_a_theorem(X2)
| ~ is_a_theorem(implies(implies(and(X0,X1),X0),X2)) ),
inference(resolution,[status(thm)],[f259,f181]) ).
fof(f3354,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ sQ65_spl
| is_a_theorem(X1)
| ~ is_a_theorem(implies(implies(or(X0,X0),X0),X1)) ),
inference(resolution,[status(thm)],[f418,f181]) ).
fof(f3363,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ sQ49_spl
| is_a_theorem(X1)
| ~ is_a_theorem(implies(implies(X0,and(X0,X0)),X1)) ),
inference(resolution,[status(thm)],[f358,f181]) ).
fof(f3369,plain,
! [X0,X1,X2] :
( ~ sQ1_spl
| ~ sQ22_spl
| ~ sQ83_spl
| ~ sQ79_spl
| ~ sQ54_spl
| ~ sQ49_spl
| is_a_theorem(X2)
| ~ is_a_theorem(implies(or(X0,implies(X0,X1)),X2)) ),
inference(resolution,[status(thm)],[f1970,f181]) ).
fof(f3416,plain,
! [X0,X1] :
( ~ sQ22_spl
| ~ sQ83_spl
| ~ sQ1_spl
| ~ sQ79_spl
| ~ sQ54_spl
| ~ sQ49_spl
| ~ sQ70_spl
| is_a_theorem(or(implies(X0,X1),X0)) ),
inference(resolution,[status(thm)],[f3178,f1970]) ).
fof(f3422,plain,
! [X0,X1,X2] :
( ~ sQ1_spl
| ~ sQ22_spl
| ~ sQ83_spl
| ~ sQ79_spl
| ~ sQ54_spl
| ~ sQ49_spl
| ~ sQ70_spl
| is_a_theorem(X2)
| ~ is_a_theorem(implies(or(implies(X0,X1),X0),X2)) ),
inference(resolution,[status(thm)],[f3416,f181]) ).
fof(f3492,plain,
! [X0,X1] :
( ~ sQ54_spl
| ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ22_spl
| ~ sQ1_spl
| ~ sQ49_spl
| is_a_theorem(or(and(X0,X1),not(and(X1,X0)))) ),
inference(resolution,[status(thm)],[f3322,f604]) ).
fof(f3685,plain,
! [X0,X1,X2] :
( ~ sQ83_spl
| ~ sQ79_spl
| ~ sQ54_spl
| is_a_theorem(implies(or(X0,X1),implies(implies(X1,X2),implies(not(X2),X0)))) ),
inference(paramodulation,[status(thm)],[f606,f1030]) ).
fof(f3695,plain,
! [X0,X1,X2] :
( ~ sQ83_spl
| ~ sQ79_spl
| ~ sQ54_spl
| is_a_theorem(implies(or(X0,X1),implies(implies(X1,X2),or(X2,X0)))) ),
inference(forward_demodulation,[status(thm)],[f605,f3685]) ).
fof(f4211,plain,
! [X0,X1] :
( ~ sQ83_spl
| ~ sQ54_spl
| ~ sQ1_spl
| ~ sQ49_spl
| is_a_theorem(implies(implies(and(X0,X0),X1),not(and(not(X1),X0)))) ),
inference(resolution,[status(thm)],[f3363,f568]) ).
fof(f4467,plain,
! [X0,X1,X2] :
( ~ sQ1_spl
| ~ sQ22_spl
| ~ sQ83_spl
| ~ sQ54_spl
| is_a_theorem(not(and(not(X1),X0)))
| ~ is_a_theorem(implies(X0,and(X1,X2))) ),
inference(resolution,[status(thm)],[f943,f3346]) ).
fof(f5296,plain,
! [X0,X1,X2] :
( ~ sQ83_spl
| ~ sQ54_spl
| ~ sQ79_spl
| ~ sQ1_spl
| ~ sQ22_spl
| ~ sQ49_spl
| is_a_theorem(or(and(implies(X0,X1),X2),implies(X2,X0))) ),
inference(resolution,[status(thm)],[f3369,f1030]) ).
fof(f5317,plain,
! [X0,X1,X2] :
( ~ sQ83_spl
| ~ sQ54_spl
| ~ sQ79_spl
| ~ sQ1_spl
| ~ sQ22_spl
| ~ sQ49_spl
| ~ sQ70_spl
| is_a_theorem(or(and(X0,X1),implies(X1,implies(X0,X2)))) ),
inference(resolution,[status(thm)],[f3422,f1030]) ).
fof(f5926,plain,
! [X0,X1,X2] :
( ~ sQ83_spl
| ~ sQ79_spl
| ~ sQ54_spl
| ~ sQ1_spl
| ~ sQ22_spl
| ~ sQ49_spl
| is_a_theorem(implies(implies(implies(X0,X1),X2),implies(not(X2),X0))) ),
inference(paramodulation,[status(thm)],[f606,f5296]) ).
fof(f5934,plain,
! [X0,X1,X2] :
( ~ sQ83_spl
| ~ sQ79_spl
| ~ sQ54_spl
| ~ sQ1_spl
| ~ sQ22_spl
| ~ sQ49_spl
| is_a_theorem(implies(implies(implies(X0,X1),X2),or(X2,X0))) ),
inference(forward_demodulation,[status(thm)],[f605,f5926]) ).
fof(f5939,plain,
! [X0,X1,X2] :
( ~ sQ83_spl
| ~ sQ79_spl
| ~ sQ54_spl
| ~ sQ1_spl
| ~ sQ22_spl
| ~ sQ49_spl
| ~ sQ70_spl
| is_a_theorem(implies(implies(X0,X1),implies(not(X1),implies(X0,X2)))) ),
inference(paramodulation,[status(thm)],[f606,f5317]) ).
fof(f5949,plain,
! [X0,X1,X2] :
( ~ sQ83_spl
| ~ sQ79_spl
| ~ sQ54_spl
| ~ sQ1_spl
| ~ sQ22_spl
| ~ sQ49_spl
| ~ sQ70_spl
| is_a_theorem(implies(implies(X0,X1),or(X1,implies(X0,X2)))) ),
inference(forward_demodulation,[status(thm)],[f605,f5939]) ).
fof(f6781,plain,
! [X0,X1,X2] :
( ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ54_spl
| ~ sQ1_spl
| ~ sQ22_spl
| ~ sQ49_spl
| ~ sQ70_spl
| is_a_theorem(implies(or(X0,X1),or(X1,implies(not(X0),X2)))) ),
inference(paramodulation,[status(thm)],[f605,f5949]) ).
fof(f6786,plain,
! [X0,X1,X2] :
( ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ54_spl
| ~ sQ1_spl
| ~ sQ22_spl
| ~ sQ49_spl
| ~ sQ70_spl
| is_a_theorem(implies(or(X0,X1),or(X1,or(X0,X2)))) ),
inference(forward_demodulation,[status(thm)],[f605,f6781]) ).
fof(f11445,plain,
! [X0,X1,X2] :
( ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ54_spl
| ~ sQ1_spl
| ~ sQ22_spl
| ~ sQ49_spl
| ~ sQ70_spl
| is_a_theorem(or(X0,or(implies(X0,X1),X2))) ),
inference(resolution,[status(thm)],[f3422,f6786]) ).
fof(f11477,plain,
! [X0,X1,X2] :
( ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ54_spl
| ~ sQ1_spl
| ~ sQ22_spl
| ~ sQ49_spl
| ~ sQ70_spl
| is_a_theorem(or(not(X0),or(or(X0,X1),X2))) ),
inference(paramodulation,[status(thm)],[f605,f11445]) ).
fof(f11598,plain,
! [X0,X1,X2] :
( ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ54_spl
| ~ sQ1_spl
| ~ sQ22_spl
| ~ sQ49_spl
| ~ sQ70_spl
| is_a_theorem(or(implies(X0,X1),or(X0,X2))) ),
inference(resolution,[status(thm)],[f3369,f6786]) ).
fof(f11629,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ54_spl
| ~ sQ22_spl
| ~ sQ49_spl
| ~ sQ70_spl
| is_a_theorem(implies(X0,or(X0,X1))) ),
inference(resolution,[status(thm)],[f11598,f3186]) ).
fof(f11634,plain,
( ~ sQ1_spl
| ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ54_spl
| ~ sQ22_spl
| ~ sQ49_spl
| ~ sQ70_spl
| sQ31_spl ),
inference(split_clause,[status(thm)],[f11629,f291,f436,f357,f258,f376,f483,f469,f180]) ).
fof(f11653,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ sQ31_spl
| is_a_theorem(or(X0,X1))
| ~ is_a_theorem(X0) ),
inference(resolution,[status(thm)],[f292,f181]) ).
fof(f11696,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ sQ83_spl
| ~ sQ79_spl
| ~ sQ54_spl
| ~ sQ22_spl
| ~ sQ49_spl
| ~ sQ31_spl
| is_a_theorem(or(X1,X0))
| ~ is_a_theorem(X0) ),
inference(resolution,[status(thm)],[f11653,f2410]) ).
fof(f11701,plain,
! [X0] :
( ~ sQ1_spl
| ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ49_spl
| ~ sQ54_spl
| ~ sQ22_spl
| ~ sQ31_spl
| is_a_theorem(not(not(X0)))
| ~ is_a_theorem(X0) ),
inference(resolution,[status(thm)],[f11653,f882]) ).
fof(f11823,plain,
! [X0,X1] :
( ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ1_spl
| ~ sQ49_spl
| ~ sQ54_spl
| ~ sQ22_spl
| ~ sQ31_spl
| is_a_theorem(X1)
| ~ is_a_theorem(or(not(X0),X1))
| ~ is_a_theorem(X0) ),
inference(resolution,[status(thm)],[f11701,f615]) ).
fof(f12616,plain,
! [X0,X1,X2] :
( ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ54_spl
| ~ sQ1_spl
| ~ sQ22_spl
| ~ sQ49_spl
| ~ sQ70_spl
| ~ sQ31_spl
| is_a_theorem(or(or(X0,X1),X2))
| ~ is_a_theorem(X0) ),
inference(resolution,[status(thm)],[f11823,f11477]) ).
fof(f12658,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ sQ70_spl
| ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ49_spl
| ~ sQ54_spl
| ~ sQ22_spl
| ~ sQ31_spl
| ~ is_a_theorem(or(X1,not(X0)))
| is_a_theorem(X1)
| ~ is_a_theorem(X0) ),
inference(resolution,[status(thm)],[f11823,f3178]) ).
fof(f14709,plain,
! [X0] :
( ~ sQ1_spl
| ~ sQ22_spl
| ~ sQ83_spl
| ~ sQ54_spl
| ~ sQ49_spl
| is_a_theorem(not(and(not(X0),X0))) ),
inference(resolution,[status(thm)],[f4211,f3346]) ).
fof(f14961,plain,
! [X0,X1] :
( ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ1_spl
| ~ sQ22_spl
| ~ sQ54_spl
| ~ sQ49_spl
| is_a_theorem(X1)
| ~ is_a_theorem(or(and(not(X0),X0),X1)) ),
inference(resolution,[status(thm)],[f14709,f615]) ).
fof(f16577,plain,
! [X0] :
( ~ sQ1_spl
| ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ54_spl
| ~ sQ22_spl
| ~ sQ49_spl
| is_a_theorem(implies(X0,not(not(X0)))) ),
inference(resolution,[status(thm)],[f14961,f860]) ).
fof(f16578,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ54_spl
| ~ sQ22_spl
| ~ sQ49_spl
| ~ is_a_theorem(or(X1,not(X0)))
| is_a_theorem(implies(X0,X1)) ),
inference(resolution,[status(thm)],[f14961,f799]) ).
fof(f22039,plain,
( ~ sQ15_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f234,f176]) ).
fof(f22040,plain,
~ sQ15_spl,
inference(contradiction_clause,[status(thm)],[f22039]) ).
fof(f23313,plain,
! [X0,X1] :
( ~ sQ54_spl
| ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ22_spl
| ~ sQ1_spl
| ~ sQ49_spl
| is_a_theorem(implies(and(X0,X1),and(X1,X0))) ),
inference(resolution,[status(thm)],[f16578,f3492]) ).
fof(f23350,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ sQ83_spl
| ~ sQ79_spl
| ~ sQ54_spl
| ~ sQ22_spl
| ~ sQ49_spl
| ~ sQ31_spl
| ~ is_a_theorem(not(X0))
| is_a_theorem(implies(X0,X1)) ),
inference(resolution,[status(thm)],[f16578,f11696]) ).
fof(f28650,plain,
! [X0,X1,X2] :
( ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ54_spl
| ~ sQ1_spl
| ~ sQ22_spl
| ~ sQ49_spl
| ~ sQ70_spl
| ~ sQ31_spl
| ~ is_a_theorem(X0)
| is_a_theorem(X2)
| ~ is_a_theorem(implies(or(X0,X1),X2)) ),
inference(resolution,[status(thm)],[f1244,f12616]) ).
fof(f29320,plain,
! [X0,X1,X2] :
( ~ sQ1_spl
| ~ sQ83_spl
| ~ sQ79_spl
| ~ sQ54_spl
| ~ sQ22_spl
| ~ sQ49_spl
| is_a_theorem(or(X2,X0))
| ~ is_a_theorem(implies(implies(X0,X1),X2)) ),
inference(resolution,[status(thm)],[f5934,f181]) ).
fof(f41181,plain,
! [X0,X1,X2] :
( ~ sQ83_spl
| ~ sQ79_spl
| ~ sQ54_spl
| ~ sQ1_spl
| ~ sQ22_spl
| ~ sQ49_spl
| ~ sQ70_spl
| ~ sQ31_spl
| ~ is_a_theorem(X2)
| is_a_theorem(implies(implies(X0,X1),or(X1,X2))) ),
inference(resolution,[status(thm)],[f28650,f3695]) ).
fof(f44769,plain,
! [X0,X1,X2] :
( ~ sQ1_spl
| ~ sQ83_spl
| ~ sQ79_spl
| ~ sQ54_spl
| ~ sQ22_spl
| ~ sQ49_spl
| ~ sQ70_spl
| ~ sQ31_spl
| is_a_theorem(or(or(X1,X0),X2))
| ~ is_a_theorem(X0) ),
inference(resolution,[status(thm)],[f41181,f29320]) ).
fof(f44811,plain,
! [X0,X1,X2] :
( ~ sQ1_spl
| ~ sQ83_spl
| ~ sQ79_spl
| ~ sQ54_spl
| ~ sQ22_spl
| ~ sQ49_spl
| ~ sQ70_spl
| ~ sQ31_spl
| is_a_theorem(X2)
| ~ is_a_theorem(implies(or(X1,X0),X2))
| ~ is_a_theorem(X0) ),
inference(resolution,[status(thm)],[f44769,f1244]) ).
fof(f49867,plain,
! [X0,X1,X2] :
( ~ sQ83_spl
| ~ sQ54_spl
| ~ sQ79_spl
| ~ sQ1_spl
| ~ sQ22_spl
| ~ sQ49_spl
| ~ sQ70_spl
| ~ sQ31_spl
| is_a_theorem(or(and(X0,X1),implies(X1,X2)))
| ~ is_a_theorem(X0) ),
inference(resolution,[status(thm)],[f44811,f1030]) ).
fof(f52875,plain,
! [X0,X1] :
( ~ sQ54_spl
| ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ22_spl
| ~ sQ1_spl
| ~ sQ49_spl
| is_a_theorem(not(and(not(X0),and(X1,X0)))) ),
inference(resolution,[status(thm)],[f4467,f23313]) ).
fof(f52933,plain,
! [X0,X1,X2] :
( ~ sQ1_spl
| ~ sQ83_spl
| ~ sQ79_spl
| ~ sQ54_spl
| ~ sQ22_spl
| ~ sQ49_spl
| ~ sQ31_spl
| is_a_theorem(implies(and(not(X0),and(X1,X0)),X2)) ),
inference(resolution,[status(thm)],[f52875,f23350]) ).
fof(f57492,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ54_spl
| ~ sQ22_spl
| ~ sQ49_spl
| ~ sQ70_spl
| ~ sQ31_spl
| is_a_theorem(implies(X1,and(X0,X1)))
| ~ is_a_theorem(X0) ),
inference(resolution,[status(thm)],[f49867,f3051]) ).
fof(f57531,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ sQ22_spl
| ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ49_spl
| ~ sQ54_spl
| ~ sQ70_spl
| ~ sQ31_spl
| is_a_theorem(and(X0,or(not(X1),X1)))
| ~ is_a_theorem(X0) ),
inference(resolution,[status(thm)],[f57492,f3325]) ).
fof(f57552,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ sQ65_spl
| ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ54_spl
| ~ sQ22_spl
| ~ sQ49_spl
| ~ sQ70_spl
| ~ sQ31_spl
| is_a_theorem(and(X0,implies(or(X1,X1),X1)))
| ~ is_a_theorem(X0) ),
inference(resolution,[status(thm)],[f57492,f3354]) ).
fof(f60227,plain,
! [X0] :
( ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ87_spl
| ~ sQ1_spl
| ~ sQ22_spl
| ~ sQ49_spl
| ~ sQ54_spl
| ~ sQ70_spl
| ~ sQ31_spl
| is_a_theorem(equiv(X0,not(not(X0))))
| ~ is_a_theorem(implies(X0,not(not(X0)))) ),
inference(paramodulation,[status(thm)],[f613,f57531]) ).
fof(f60240,plain,
! [X0] :
( ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ87_spl
| ~ sQ1_spl
| ~ sQ22_spl
| ~ sQ49_spl
| ~ sQ54_spl
| ~ sQ70_spl
| ~ sQ31_spl
| is_a_theorem(equiv(X0,not(not(X0)))) ),
inference(forward_subsumption_resolution,[status(thm)],[f60227,f16577]) ).
fof(f60253,plain,
! [X0] :
( ~ sQ6_spl
| ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ87_spl
| ~ sQ1_spl
| ~ sQ22_spl
| ~ sQ49_spl
| ~ sQ54_spl
| ~ sQ70_spl
| ~ sQ31_spl
| X0 = not(not(X0)) ),
inference(resolution,[status(thm)],[f60240,f200]) ).
fof(f60375,plain,
! [X0,X1] :
( ~ sQ83_spl
| ~ sQ6_spl
| ~ sQ79_spl
| ~ sQ87_spl
| ~ sQ1_spl
| ~ sQ22_spl
| ~ sQ49_spl
| ~ sQ54_spl
| ~ sQ70_spl
| ~ sQ31_spl
| and(X0,not(X1)) = not(implies(X0,X1)) ),
inference(paramodulation,[status(thm)],[f484,f60253]) ).
fof(f60918,plain,
! [X0,X1] :
( ~ sQ6_spl
| ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ87_spl
| ~ sQ1_spl
| ~ sQ22_spl
| ~ sQ49_spl
| ~ sQ54_spl
| ~ sQ70_spl
| ~ sQ31_spl
| or(not(X0),X1) = implies(X0,X1) ),
inference(paramodulation,[status(thm)],[f60253,f605]) ).
fof(f62440,plain,
! [X0,X1] :
( ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ6_spl
| ~ sQ87_spl
| ~ sQ1_spl
| ~ sQ22_spl
| ~ sQ49_spl
| ~ sQ54_spl
| ~ sQ70_spl
| ~ sQ31_spl
| and(not(X0),not(X1)) = not(or(X0,X1)) ),
inference(paramodulation,[status(thm)],[f605,f60375]) ).
fof(f74594,plain,
! [X0,X1,X2] :
( ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ6_spl
| ~ sQ87_spl
| ~ sQ1_spl
| ~ sQ22_spl
| ~ sQ49_spl
| ~ sQ54_spl
| ~ sQ70_spl
| ~ sQ31_spl
| is_a_theorem(implies(and(not(not(X0)),not(or(X1,X0))),X2)) ),
inference(paramodulation,[status(thm)],[f62440,f52933]) ).
fof(f75346,plain,
! [X0,X1,X2] :
( ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ6_spl
| ~ sQ87_spl
| ~ sQ1_spl
| ~ sQ22_spl
| ~ sQ49_spl
| ~ sQ54_spl
| ~ sQ70_spl
| ~ sQ31_spl
| is_a_theorem(implies(not(or(not(X0),or(X1,X0))),X2)) ),
inference(forward_demodulation,[status(thm)],[f62440,f74594]) ).
fof(f75347,plain,
! [X0,X1,X2] :
( ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ6_spl
| ~ sQ87_spl
| ~ sQ1_spl
| ~ sQ22_spl
| ~ sQ49_spl
| ~ sQ54_spl
| ~ sQ70_spl
| ~ sQ31_spl
| is_a_theorem(or(or(not(X0),or(X1,X0)),X2)) ),
inference(forward_demodulation,[status(thm)],[f605,f75346]) ).
fof(f75348,plain,
! [X0,X1,X2] :
( ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ6_spl
| ~ sQ87_spl
| ~ sQ1_spl
| ~ sQ22_spl
| ~ sQ49_spl
| ~ sQ54_spl
| ~ sQ70_spl
| ~ sQ31_spl
| is_a_theorem(or(implies(X0,or(X1,X0)),X2)) ),
inference(forward_demodulation,[status(thm)],[f60918,f75347]) ).
fof(f75722,plain,
! [X0,X1,X2] :
( ~ sQ1_spl
| ~ sQ70_spl
| ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ49_spl
| ~ sQ54_spl
| ~ sQ22_spl
| ~ sQ31_spl
| ~ sQ6_spl
| ~ sQ87_spl
| is_a_theorem(implies(X1,or(X2,X1)))
| ~ is_a_theorem(X0) ),
inference(resolution,[status(thm)],[f75348,f12658]) ).
fof(f75747,plain,
( ~ sQ1_spl
| ~ sQ70_spl
| ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ49_spl
| ~ sQ54_spl
| ~ sQ22_spl
| ~ sQ31_spl
| ~ sQ6_spl
| ~ sQ87_spl
| sQ34_spl
| sQ90_spl ),
inference(split_clause,[status(thm)],[f75722,f580,f302,f497,f199,f291,f258,f376,f357,f483,f469,f436,f180]) ).
fof(f102573,plain,
! [X0] :
( ~ sQ87_spl
| ~ sQ1_spl
| ~ sQ65_spl
| ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ54_spl
| ~ sQ22_spl
| ~ sQ49_spl
| ~ sQ70_spl
| ~ sQ31_spl
| is_a_theorem(equiv(X0,or(X0,X0)))
| ~ is_a_theorem(implies(X0,or(X0,X0))) ),
inference(paramodulation,[status(thm)],[f498,f57552]) ).
fof(f102589,plain,
! [X0] :
( ~ sQ87_spl
| ~ sQ1_spl
| ~ sQ65_spl
| ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ54_spl
| ~ sQ22_spl
| ~ sQ49_spl
| ~ sQ70_spl
| ~ sQ31_spl
| ~ sQ34_spl
| is_a_theorem(equiv(X0,or(X0,X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[f102573,f303]) ).
fof(f102624,plain,
! [X0] :
( ~ sQ6_spl
| ~ sQ87_spl
| ~ sQ1_spl
| ~ sQ65_spl
| ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ54_spl
| ~ sQ22_spl
| ~ sQ49_spl
| ~ sQ70_spl
| ~ sQ31_spl
| ~ sQ34_spl
| X0 = or(X0,X0) ),
inference(resolution,[status(thm)],[f102589,f200]) ).
fof(f103147,plain,
! [X0,X1] :
( ~ sQ6_spl
| ~ sQ87_spl
| ~ sQ1_spl
| ~ sQ65_spl
| ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ54_spl
| ~ sQ22_spl
| ~ sQ49_spl
| ~ sQ70_spl
| ~ sQ31_spl
| ~ sQ34_spl
| is_a_theorem(implies(implies(X0,implies(X0,X1)),implies(X0,X1))) ),
inference(paramodulation,[status(thm)],[f102624,f5949]) ).
fof(f103636,plain,
( ~ sQ6_spl
| ~ sQ87_spl
| ~ sQ1_spl
| ~ sQ65_spl
| ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ54_spl
| ~ sQ22_spl
| ~ sQ49_spl
| ~ sQ70_spl
| ~ sQ31_spl
| ~ sQ34_spl
| sQ16_spl ),
inference(split_clause,[status(thm)],[f103147,f236,f302,f291,f436,f357,f258,f376,f483,f469,f417,f180,f497,f199]) ).
fof(f103792,plain,
$false,
inference(sat_refutation,[status(thm)],[f183,f202,f243,f360,f368,f379,f439,f443,f472,f486,f500,f502,f504,f506,f508,f510,f522,f526,f655,f1028,f2519,f3171,f3294,f11634,f22040,f75747,f103636]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL504+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n020.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Mon Sep 21 00:36:48 UTC 2026
% 0.08/0.37 % CPUTime :
% 0.13/0.38 % Drodi V4.1.1
% 143.58/18.59 % Refutation found
% 143.58/18.59 % SZS status Theorem for theBenchmark: Theorem is valid
% 143.58/18.59 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 105.61/19.81 % Elapsed time: 19.229744 seconds
% 105.61/19.81 % CPU time: 141.114850 seconds
% 105.61/19.81 % Total memory used: 1.236 GB
% 105.61/19.81 % Net memory used: 1.161 GB
%------------------------------------------------------------------------------