%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : LCL485+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 : n005.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:50 PM UTC 2026
% Result : Theorem 107.92s 14.09s
% Output : CNFRefutation 41.21s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 55
% Syntax : Number of formulae : 237 ( 41 unt; 29 def)
% Number of atoms : 817 ( 50 equ)
% Maximal formula atoms : 15 ( 3 avg)
% Number of connectives : 1078 ( 498 ~; 508 |; 26 &)
% ( 39 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 19 ( 5 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 45 ( 43 usr; 43 prp; 0-2 aty)
% Number of functors : 22 ( 22 usr; 17 con; 0-2 aty)
% Number of variables : 300 ( 281 !; 19 ?)
% 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(f22,axiom,
( r1
<=> ! [P] : is_a_theorem(implies(or(P,P),P)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f23,axiom,
( r2
<=> ! [P,Q] : is_a_theorem(implies(Q,or(P,Q))) ),
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(f25,axiom,
( r4
<=> ! [P,Q,R] : is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f26,axiom,
( r5
<=> ! [P,Q,R] : is_a_theorem(implies(implies(Q,R),implies(or(P,Q),or(P,R)))) ),
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(f28,axiom,
( op_and
=> ! [X,Y] : and(X,Y) = not(or(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(f30,axiom,
( op_implies_or
=> ! [X,Y] : implies(X,Y) = or(not(X),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_implies_or,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f33,axiom,
op_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,
r1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f37,axiom,
r2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f38,axiom,
r3,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f39,axiom,
r4,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f40,axiom,
r5,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f41,axiom,
substitution_of_equivalents,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f42,axiom,
op_or,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f43,axiom,
op_implies_and,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f45,conjecture,
implies_2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f46,negated_conjecture,
~ implies_2,
inference(negated_conjecture,[status(cth)],[f45]) ).
fof(f47,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(f48,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)],[f47]) ).
fof(f49,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)],[f48]) ).
fof(f50,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)],[f49]) ).
fof(f51,plain,
! [X0,X1] :
( is_a_theorem(X1)
| ~ is_a_theorem(implies(X0,X1))
| ~ is_a_theorem(X0)
| ~ modus_ponens ),
inference(cnf_transformation,[status(thm)],[f50]) ).
fof(f55,plain,
( substitution_of_equivalents
<=> ! [X,Y] :
( X = Y
| ~ is_a_theorem(equiv(X,Y)) ) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f56,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)],[f55]) ).
fof(f57,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)],[f56]) ).
fof(f58,plain,
! [X0,X1] :
( X0 = X1
| ~ is_a_theorem(equiv(X0,X1))
| ~ substitution_of_equivalents ),
inference(cnf_transformation,[status(thm)],[f57]) ).
fof(f69,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(f70,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)],[f69]) ).
fof(f72,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)],[f70]) ).
fof(f137,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(f138,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)],[f137]) ).
fof(f139,plain,
! [X0] :
( is_a_theorem(implies(or(X0,X0),X0))
| ~ r1 ),
inference(cnf_transformation,[status(thm)],[f138]) ).
fof(f141,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(f142,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)],[f141]) ).
fof(f143,plain,
! [X0,X1] :
( is_a_theorem(implies(X0,or(X1,X0)))
| ~ r2 ),
inference(cnf_transformation,[status(thm)],[f142]) ).
fof(f145,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(f146,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)],[f145]) ).
fof(f147,plain,
! [X0,X1] :
( is_a_theorem(implies(or(X0,X1),or(X1,X0)))
| ~ r3 ),
inference(cnf_transformation,[status(thm)],[f146]) ).
fof(f149,plain,
( ( ? [P,Q,R] : ~ is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R))))
| r4 )
& ( ! [P,Q,R] : is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R))))
| ~ r4 ) ),
inference(NNF_transformation,[status(thm)],[f25]) ).
fof(f150,plain,
( ( ~ is_a_theorem(implies(or(sK49_skl,or(sK50_skl,sK51_skl)),or(sK50_skl,or(sK49_skl,sK51_skl))))
| r4 )
& ( ! [P,Q,R] : is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R))))
| ~ r4 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK49_skl,sK50_skl,sK51_skl]),skolemize(P,sK49_skl),skolemize(Q,sK50_skl),skolemize(R,sK51_skl)],[f149]) ).
fof(f151,plain,
! [X0,X1,X2] :
( is_a_theorem(implies(or(X0,or(X1,X2)),or(X1,or(X0,X2))))
| ~ r4 ),
inference(cnf_transformation,[status(thm)],[f150]) ).
fof(f153,plain,
( ( ? [P,Q,R] : ~ is_a_theorem(implies(implies(Q,R),implies(or(P,Q),or(P,R))))
| r5 )
& ( ! [P,Q,R] : is_a_theorem(implies(implies(Q,R),implies(or(P,Q),or(P,R))))
| ~ r5 ) ),
inference(NNF_transformation,[status(thm)],[f26]) ).
fof(f154,plain,
( ( ~ is_a_theorem(implies(implies(sK53_skl,sK54_skl),implies(or(sK52_skl,sK53_skl),or(sK52_skl,sK54_skl))))
| r5 )
& ( ! [P,Q,R] : is_a_theorem(implies(implies(Q,R),implies(or(P,Q),or(P,R))))
| ~ r5 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK52_skl,sK53_skl,sK54_skl]),skolemize(P,sK52_skl),skolemize(Q,sK53_skl),skolemize(R,sK54_skl)],[f153]) ).
fof(f155,plain,
! [X0,X1,X2] :
( is_a_theorem(implies(implies(X0,X1),implies(or(X2,X0),or(X2,X1))))
| ~ r5 ),
inference(cnf_transformation,[status(thm)],[f154]) ).
fof(f157,plain,
( ! [X,Y] : or(X,Y) = not(and(not(X),not(Y)))
| ~ op_or ),
inference(pre_NNF_transformation,[status(thm)],[f27]) ).
fof(f158,plain,
! [X0,X1] :
( or(X0,X1) = not(and(not(X0),not(X1)))
| ~ op_or ),
inference(cnf_transformation,[status(thm)],[f157]) ).
fof(f159,plain,
( ! [X,Y] : and(X,Y) = not(or(not(X),not(Y)))
| ~ op_and ),
inference(pre_NNF_transformation,[status(thm)],[f28]) ).
fof(f160,plain,
! [X0,X1] :
( and(X0,X1) = not(or(not(X0),not(X1)))
| ~ op_and ),
inference(cnf_transformation,[status(thm)],[f159]) ).
fof(f161,plain,
( ! [X,Y] : implies(X,Y) = not(and(X,not(Y)))
| ~ op_implies_and ),
inference(pre_NNF_transformation,[status(thm)],[f29]) ).
fof(f162,plain,
! [X0,X1] :
( implies(X0,X1) = not(and(X0,not(X1)))
| ~ op_implies_and ),
inference(cnf_transformation,[status(thm)],[f161]) ).
fof(f163,plain,
( ! [X,Y] : implies(X,Y) = or(not(X),Y)
| ~ op_implies_or ),
inference(pre_NNF_transformation,[status(thm)],[f30]) ).
fof(f164,plain,
! [X0,X1] :
( implies(X0,X1) = or(not(X0),X1)
| ~ op_implies_or ),
inference(cnf_transformation,[status(thm)],[f163]) ).
fof(f165,plain,
( ! [X,Y] : equiv(X,Y) = and(implies(X,Y),implies(Y,X))
| ~ op_equiv ),
inference(pre_NNF_transformation,[status(thm)],[f31]) ).
fof(f166,plain,
! [X0,X1] :
( equiv(X0,X1) = and(implies(X0,X1),implies(X1,X0))
| ~ op_equiv ),
inference(cnf_transformation,[status(thm)],[f165]) ).
fof(f167,plain,
op_implies_or,
inference(cnf_transformation,[status(thm)],[f32]) ).
fof(f168,plain,
op_and,
inference(cnf_transformation,[status(thm)],[f33]) ).
fof(f169,plain,
op_equiv,
inference(cnf_transformation,[status(thm)],[f34]) ).
fof(f170,plain,
modus_ponens,
inference(cnf_transformation,[status(thm)],[f35]) ).
fof(f171,plain,
r1,
inference(cnf_transformation,[status(thm)],[f36]) ).
fof(f172,plain,
r2,
inference(cnf_transformation,[status(thm)],[f37]) ).
fof(f173,plain,
r3,
inference(cnf_transformation,[status(thm)],[f38]) ).
fof(f174,plain,
r4,
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f175,plain,
r5,
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f176,plain,
substitution_of_equivalents,
inference(cnf_transformation,[status(thm)],[f41]) ).
fof(f177,plain,
op_or,
inference(cnf_transformation,[status(thm)],[f42]) ).
fof(f178,plain,
op_implies_and,
inference(cnf_transformation,[status(thm)],[f43]) ).
fof(f180,plain,
~ implies_2,
inference(cnf_transformation,[status(thm)],[f46]) ).
fof(f181,definition,
( sQ0_spl
<=> modus_ponens ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f183,plain,
( sQ0_spl
| ~ modus_ponens ),
inference(component_clause,[status(thm)],[f181]) ).
fof(f184,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(f185,plain,
! [X0,X1] :
( ~ sQ1_spl
| is_a_theorem(X1)
| ~ is_a_theorem(implies(X0,X1))
| ~ is_a_theorem(X0) ),
inference(component_clause,[status(thm)],[f184]) ).
fof(f187,plain,
( sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f51,f181,f184]) ).
fof(f200,definition,
( sQ5_spl
<=> substitution_of_equivalents ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f202,plain,
( sQ5_spl
| ~ substitution_of_equivalents ),
inference(component_clause,[status(thm)],[f200]) ).
fof(f203,definition,
! [X0,X1] :
( sQ6_spl
<=> ( X0 = X1
| ~ is_a_theorem(equiv(X0,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f204,plain,
! [X0,X1] :
( ~ sQ6_spl
| X0 = X1
| ~ is_a_theorem(equiv(X0,X1)) ),
inference(component_clause,[status(thm)],[f203]) ).
fof(f206,plain,
( sQ6_spl
| ~ sQ5_spl ),
inference(split_clause,[status(thm)],[f58,f200,f203]) ).
fof(f229,definition,
! [X0,X1] :
( sQ13_spl
<=> is_a_theorem(implies(X0,implies(X1,X0))) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f230,plain,
! [X0,X1] :
( ~ sQ13_spl
| is_a_theorem(implies(X0,implies(X1,X0))) ),
inference(component_clause,[status(thm)],[f229]) ).
fof(f237,definition,
( sQ15_spl
<=> implies_2 ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f238,plain,
( ~ sQ15_spl
| implies_2 ),
inference(component_clause,[status(thm)],[f237]) ).
fof(f240,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(f241,plain,
! [X0,X1] :
( ~ sQ16_spl
| is_a_theorem(implies(implies(X0,implies(X0,X1)),implies(X0,X1))) ),
inference(component_clause,[status(thm)],[f240]) ).
fof(f244,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(f246,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)],[f244]) ).
fof(f247,plain,
( ~ sQ17_spl
| sQ15_spl ),
inference(split_clause,[status(thm)],[f72,f237,f244]) ).
fof(f273,definition,
! [X0,X1] :
( sQ25_spl
<=> is_a_theorem(implies(and(X0,X1),X1)) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f274,plain,
! [X0,X1] :
( ~ sQ25_spl
| is_a_theorem(implies(and(X0,X1),X1)) ),
inference(component_clause,[status(thm)],[f273]) ).
fof(f306,definition,
! [X0,X1] :
( sQ34_spl
<=> is_a_theorem(implies(X0,or(X1,X0))) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f307,plain,
! [X0,X1] :
( ~ sQ34_spl
| is_a_theorem(implies(X0,or(X1,X0))) ),
inference(component_clause,[status(thm)],[f306]) ).
fof(f418,definition,
( sQ64_spl
<=> r1 ),
introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition]) ).
fof(f420,plain,
( sQ64_spl
| ~ r1 ),
inference(component_clause,[status(thm)],[f418]) ).
fof(f421,definition,
! [X0] :
( sQ65_spl
<=> is_a_theorem(implies(or(X0,X0),X0)) ),
introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition]) ).
fof(f422,plain,
! [X0] :
( ~ sQ65_spl
| is_a_theorem(implies(or(X0,X0),X0)) ),
inference(component_clause,[status(thm)],[f421]) ).
fof(f424,plain,
( sQ65_spl
| ~ sQ64_spl ),
inference(split_clause,[status(thm)],[f139,f418,f421]) ).
fof(f429,definition,
( sQ67_spl
<=> r2 ),
introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition]) ).
fof(f431,plain,
( sQ67_spl
| ~ r2 ),
inference(component_clause,[status(thm)],[f429]) ).
fof(f432,plain,
( sQ34_spl
| ~ sQ67_spl ),
inference(split_clause,[status(thm)],[f143,f429,f306]) ).
fof(f437,definition,
( sQ69_spl
<=> r3 ),
introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition]) ).
fof(f439,plain,
( sQ69_spl
| ~ r3 ),
inference(component_clause,[status(thm)],[f437]) ).
fof(f440,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(f441,plain,
! [X0,X1] :
( ~ sQ70_spl
| is_a_theorem(implies(or(X0,X1),or(X1,X0))) ),
inference(component_clause,[status(thm)],[f440]) ).
fof(f443,plain,
( sQ70_spl
| ~ sQ69_spl ),
inference(split_clause,[status(thm)],[f147,f437,f440]) ).
fof(f448,definition,
( sQ72_spl
<=> r4 ),
introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition]) ).
fof(f450,plain,
( sQ72_spl
| ~ r4 ),
inference(component_clause,[status(thm)],[f448]) ).
fof(f451,definition,
! [X0,X1,X2] :
( sQ73_spl
<=> is_a_theorem(implies(or(X0,or(X1,X2)),or(X1,or(X0,X2)))) ),
introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition]) ).
fof(f452,plain,
! [X0,X1,X2] :
( ~ sQ73_spl
| is_a_theorem(implies(or(X0,or(X1,X2)),or(X1,or(X0,X2)))) ),
inference(component_clause,[status(thm)],[f451]) ).
fof(f454,plain,
( sQ73_spl
| ~ sQ72_spl ),
inference(split_clause,[status(thm)],[f151,f448,f451]) ).
fof(f459,definition,
( sQ75_spl
<=> r5 ),
introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition]) ).
fof(f461,plain,
( sQ75_spl
| ~ r5 ),
inference(component_clause,[status(thm)],[f459]) ).
fof(f462,definition,
! [X0,X1,X2] :
( sQ76_spl
<=> is_a_theorem(implies(implies(X0,X1),implies(or(X2,X0),or(X2,X1)))) ),
introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition]) ).
fof(f463,plain,
! [X0,X1,X2] :
( ~ sQ76_spl
| is_a_theorem(implies(implies(X0,X1),implies(or(X2,X0),or(X2,X1)))) ),
inference(component_clause,[status(thm)],[f462]) ).
fof(f465,plain,
( sQ76_spl
| ~ sQ75_spl ),
inference(split_clause,[status(thm)],[f155,f459,f462]) ).
fof(f470,definition,
( sQ78_spl
<=> op_or ),
introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition]) ).
fof(f472,plain,
( sQ78_spl
| ~ op_or ),
inference(component_clause,[status(thm)],[f470]) ).
fof(f473,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(f474,plain,
! [X0,X1] :
( ~ sQ79_spl
| or(X0,X1) = not(and(not(X0),not(X1))) ),
inference(component_clause,[status(thm)],[f473]) ).
fof(f476,plain,
( sQ79_spl
| ~ sQ78_spl ),
inference(split_clause,[status(thm)],[f158,f470,f473]) ).
fof(f477,definition,
( sQ80_spl
<=> op_and ),
introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition]) ).
fof(f479,plain,
( sQ80_spl
| ~ op_and ),
inference(component_clause,[status(thm)],[f477]) ).
fof(f480,definition,
! [X0,X1] :
( sQ81_spl
<=> and(X0,X1) = not(or(not(X0),not(X1))) ),
introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition]) ).
fof(f481,plain,
! [X0,X1] :
( ~ sQ81_spl
| and(X0,X1) = not(or(not(X0),not(X1))) ),
inference(component_clause,[status(thm)],[f480]) ).
fof(f483,plain,
( sQ81_spl
| ~ sQ80_spl ),
inference(split_clause,[status(thm)],[f160,f477,f480]) ).
fof(f484,definition,
( sQ82_spl
<=> op_implies_and ),
introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition]) ).
fof(f486,plain,
( sQ82_spl
| ~ op_implies_and ),
inference(component_clause,[status(thm)],[f484]) ).
fof(f487,definition,
! [X0,X1] :
( sQ83_spl
<=> implies(X0,X1) = not(and(X0,not(X1))) ),
introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition]) ).
fof(f488,plain,
! [X0,X1] :
( ~ sQ83_spl
| implies(X0,X1) = not(and(X0,not(X1))) ),
inference(component_clause,[status(thm)],[f487]) ).
fof(f490,plain,
( sQ83_spl
| ~ sQ82_spl ),
inference(split_clause,[status(thm)],[f162,f484,f487]) ).
fof(f491,definition,
( sQ84_spl
<=> op_implies_or ),
introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition]) ).
fof(f493,plain,
( sQ84_spl
| ~ op_implies_or ),
inference(component_clause,[status(thm)],[f491]) ).
fof(f494,definition,
! [X0,X1] :
( sQ85_spl
<=> implies(X0,X1) = or(not(X0),X1) ),
introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition]) ).
fof(f495,plain,
! [X0,X1] :
( ~ sQ85_spl
| implies(X0,X1) = or(not(X0),X1) ),
inference(component_clause,[status(thm)],[f494]) ).
fof(f497,plain,
( sQ85_spl
| ~ sQ84_spl ),
inference(split_clause,[status(thm)],[f164,f491,f494]) ).
fof(f498,definition,
( sQ86_spl
<=> op_equiv ),
introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition]) ).
fof(f500,plain,
( sQ86_spl
| ~ op_equiv ),
inference(component_clause,[status(thm)],[f498]) ).
fof(f501,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(f502,plain,
! [X0,X1] :
( ~ sQ87_spl
| equiv(X0,X1) = and(implies(X0,X1),implies(X1,X0)) ),
inference(component_clause,[status(thm)],[f501]) ).
fof(f504,plain,
( sQ87_spl
| ~ sQ86_spl ),
inference(split_clause,[status(thm)],[f166,f498,f501]) ).
fof(f505,plain,
( sQ86_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f500,f169]) ).
fof(f506,plain,
sQ86_spl,
inference(contradiction_clause,[status(thm)],[f505]) ).
fof(f507,plain,
( sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f183,f170]) ).
fof(f508,plain,
sQ0_spl,
inference(contradiction_clause,[status(thm)],[f507]) ).
fof(f509,plain,
( sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f202,f176]) ).
fof(f510,plain,
sQ5_spl,
inference(contradiction_clause,[status(thm)],[f509]) ).
fof(f511,plain,
( sQ84_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f493,f167]) ).
fof(f512,plain,
sQ84_spl,
inference(contradiction_clause,[status(thm)],[f511]) ).
fof(f513,plain,
( sQ82_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f486,f178]) ).
fof(f514,plain,
sQ82_spl,
inference(contradiction_clause,[status(thm)],[f513]) ).
fof(f515,plain,
( sQ80_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f479,f168]) ).
fof(f516,plain,
sQ80_spl,
inference(contradiction_clause,[status(thm)],[f515]) ).
fof(f517,plain,
( sQ78_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f472,f177]) ).
fof(f518,plain,
sQ78_spl,
inference(contradiction_clause,[status(thm)],[f517]) ).
fof(f521,plain,
( sQ75_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f461,f175]) ).
fof(f522,plain,
sQ75_spl,
inference(contradiction_clause,[status(thm)],[f521]) ).
fof(f524,plain,
! [X0] :
( ~ sQ85_spl
| ~ sQ65_spl
| is_a_theorem(implies(implies(X0,not(X0)),not(X0))) ),
inference(paramodulation,[status(thm)],[f495,f422]) ).
fof(f532,plain,
( sQ72_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f450,f174]) ).
fof(f533,plain,
sQ72_spl,
inference(contradiction_clause,[status(thm)],[f532]) ).
fof(f539,plain,
! [X0,X1] :
( ~ sQ85_spl
| ~ sQ70_spl
| is_a_theorem(implies(implies(X0,X1),or(X1,not(X0)))) ),
inference(paramodulation,[status(thm)],[f495,f441]) ).
fof(f542,plain,
( sQ69_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f439,f173]) ).
fof(f543,plain,
sQ69_spl,
inference(contradiction_clause,[status(thm)],[f542]) ).
fof(f546,plain,
( sQ67_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f431,f172]) ).
fof(f547,plain,
sQ67_spl,
inference(contradiction_clause,[status(thm)],[f546]) ).
fof(f548,plain,
! [X0,X1] :
( ~ sQ85_spl
| ~ sQ34_spl
| is_a_theorem(implies(X0,implies(X1,X0))) ),
inference(paramodulation,[status(thm)],[f495,f307]) ).
fof(f551,plain,
( sQ64_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f420,f171]) ).
fof(f552,plain,
sQ64_spl,
inference(contradiction_clause,[status(thm)],[f551]) ).
fof(f587,plain,
( ~ sQ85_spl
| ~ sQ34_spl
| sQ13_spl ),
inference(split_clause,[status(thm)],[f548,f229,f306,f494]) ).
fof(f589,plain,
( sQ17_spl
| ~ sQ16_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f246,f241]) ).
fof(f590,plain,
( sQ17_spl
| ~ sQ16_spl ),
inference(contradiction_clause,[status(thm)],[f589]) ).
fof(f593,plain,
! [X0] :
( ~ sQ65_spl
| ~ sQ1_spl
| is_a_theorem(X0)
| ~ is_a_theorem(or(X0,X0)) ),
inference(resolution,[status(thm)],[f185,f422]) ).
fof(f609,plain,
! [X0,X1,X2] :
( ~ sQ83_spl
| ~ sQ85_spl
| implies(and(X0,not(X1)),X2) = or(implies(X0,X1),X2) ),
inference(paramodulation,[status(thm)],[f488,f495]) ).
fof(f610,plain,
! [X0,X1] :
( ~ sQ81_spl
| ~ sQ85_spl
| and(X0,X1) = not(implies(X0,not(X1))) ),
inference(forward_demodulation,[status(thm)],[f495,f481]) ).
fof(f614,plain,
! [X0,X1,X2] :
( ~ sQ81_spl
| ~ sQ85_spl
| implies(implies(X0,not(X1)),X2) = or(and(X0,X1),X2) ),
inference(paramodulation,[status(thm)],[f610,f495]) ).
fof(f615,plain,
! [X0,X1] :
( ~ sQ79_spl
| ~ sQ83_spl
| or(X0,X1) = implies(not(X0),X1) ),
inference(forward_demodulation,[status(thm)],[f488,f474]) ).
fof(f616,plain,
! [X0,X1,X2] :
( ~ sQ81_spl
| ~ sQ85_spl
| ~ sQ79_spl
| ~ sQ83_spl
| or(implies(X0,not(X1)),X2) = implies(and(X0,X1),X2) ),
inference(paramodulation,[status(thm)],[f610,f615]) ).
fof(f618,plain,
! [X0,X1] :
( ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ81_spl
| ~ sQ85_spl
| and(not(X0),X1) = not(or(X0,not(X1))) ),
inference(paramodulation,[status(thm)],[f615,f610]) ).
fof(f619,plain,
! [X0,X1] :
( ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ34_spl
| is_a_theorem(or(X0,or(X1,not(X0)))) ),
inference(paramodulation,[status(thm)],[f615,f307]) ).
fof(f620,plain,
! [X0,X1] :
( ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ13_spl
| is_a_theorem(or(X0,implies(X1,not(X0)))) ),
inference(paramodulation,[status(thm)],[f615,f230]) ).
fof(f622,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)],[f615,f502]) ).
fof(f634,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ sQ70_spl
| is_a_theorem(or(X1,X0))
| ~ is_a_theorem(or(X0,X1)) ),
inference(resolution,[status(thm)],[f441,f185]) ).
fof(f637,plain,
! [X0,X1,X2] :
( ~ sQ1_spl
| ~ sQ76_spl
| is_a_theorem(implies(or(X2,X0),or(X2,X1)))
| ~ is_a_theorem(implies(X0,X1)) ),
inference(resolution,[status(thm)],[f463,f185]) ).
fof(f643,plain,
! [X0,X1,X2] :
( ~ sQ1_spl
| ~ sQ73_spl
| is_a_theorem(or(X1,or(X0,X2)))
| ~ is_a_theorem(or(X0,or(X1,X2))) ),
inference(resolution,[status(thm)],[f452,f185]) ).
fof(f675,plain,
! [X0,X1] :
( ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ13_spl
| ~ sQ1_spl
| ~ sQ70_spl
| is_a_theorem(or(implies(X0,not(X1)),X1)) ),
inference(resolution,[status(thm)],[f634,f620]) ).
fof(f906,plain,
! [X0] :
( ~ sQ85_spl
| ~ sQ65_spl
| ~ sQ81_spl
| is_a_theorem(or(and(X0,X0),not(X0))) ),
inference(backward_demodulation,[status(thm)],[f614,f524]) ).
fof(f922,plain,
! [X0,X1,X2] :
( ~ sQ81_spl
| ~ sQ85_spl
| and(implies(X0,not(X1)),X2) = not(or(and(X0,X1),not(X2))) ),
inference(paramodulation,[status(thm)],[f614,f610]) ).
fof(f956,plain,
! [X0,X1] :
( ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ13_spl
| ~ sQ1_spl
| ~ sQ70_spl
| ~ sQ81_spl
| ~ sQ85_spl
| is_a_theorem(implies(and(X0,X1),X1)) ),
inference(backward_demodulation,[status(thm)],[f616,f675]) ).
fof(f987,plain,
( ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ13_spl
| ~ sQ1_spl
| ~ sQ70_spl
| ~ sQ81_spl
| ~ sQ85_spl
| sQ25_spl ),
inference(split_clause,[status(thm)],[f956,f273,f494,f480,f440,f184,f229,f487,f473]) ).
fof(f1015,plain,
! [X0,X1] :
( ~ sQ83_spl
| ~ sQ85_spl
| ~ sQ25_spl
| is_a_theorem(or(implies(X0,X1),not(X1))) ),
inference(paramodulation,[status(thm)],[f609,f274]) ).
fof(f1029,plain,
! [X0] :
( ~ sQ1_spl
| ~ sQ70_spl
| ~ sQ85_spl
| ~ sQ65_spl
| ~ sQ81_spl
| is_a_theorem(or(not(X0),and(X0,X0))) ),
inference(resolution,[status(thm)],[f906,f634]) ).
fof(f1035,plain,
! [X0] :
( ~ sQ1_spl
| ~ sQ70_spl
| ~ sQ85_spl
| ~ sQ65_spl
| ~ sQ81_spl
| is_a_theorem(implies(X0,and(X0,X0))) ),
inference(forward_demodulation,[status(thm)],[f495,f1029]) ).
fof(f1049,plain,
! [X0] :
( ~ sQ1_spl
| ~ sQ70_spl
| ~ sQ85_spl
| ~ sQ65_spl
| ~ sQ81_spl
| is_a_theorem(and(X0,X0))
| ~ is_a_theorem(X0) ),
inference(resolution,[status(thm)],[f1035,f185]) ).
fof(f1403,plain,
! [X0,X1,X2] :
( ~ sQ1_spl
| ~ sQ76_spl
| is_a_theorem(or(X2,X1))
| ~ is_a_theorem(or(X2,X0))
| ~ is_a_theorem(implies(X0,X1)) ),
inference(resolution,[status(thm)],[f637,f185]) ).
fof(f1584,plain,
! [X0,X1,X2] :
( ~ sQ85_spl
| ~ sQ76_spl
| is_a_theorem(implies(implies(X0,X1),implies(implies(X2,X0),or(not(X2),X1)))) ),
inference(paramodulation,[status(thm)],[f495,f463]) ).
fof(f1592,plain,
! [X0,X1,X2] :
( ~ sQ85_spl
| ~ sQ76_spl
| is_a_theorem(implies(implies(X0,X1),implies(implies(X2,X0),implies(X2,X1)))) ),
inference(forward_demodulation,[status(thm)],[f495,f1584]) ).
fof(f1871,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ sQ73_spl
| ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ34_spl
| is_a_theorem(or(X0,or(X1,not(X1)))) ),
inference(resolution,[status(thm)],[f619,f643]) ).
fof(f1939,plain,
! [X0,X1] :
( ~ sQ81_spl
| ~ sQ85_spl
| ~ sQ70_spl
| is_a_theorem(or(and(X0,X1),or(not(X1),not(X0)))) ),
inference(paramodulation,[status(thm)],[f614,f539]) ).
fof(f1952,plain,
! [X0,X1] :
( ~ sQ81_spl
| ~ sQ85_spl
| ~ sQ70_spl
| is_a_theorem(or(and(X0,X1),implies(X1,not(X0)))) ),
inference(forward_demodulation,[status(thm)],[f495,f1939]) ).
fof(f1996,plain,
! [X0] :
( ~ sQ65_spl
| ~ sQ1_spl
| ~ sQ73_spl
| ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ34_spl
| is_a_theorem(or(X0,not(X0))) ),
inference(resolution,[status(thm)],[f1871,f593]) ).
fof(f2011,plain,
! [X0] :
( ~ sQ1_spl
| ~ sQ70_spl
| ~ sQ65_spl
| ~ sQ73_spl
| ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ34_spl
| is_a_theorem(or(not(X0),X0)) ),
inference(resolution,[status(thm)],[f1996,f634]) ).
fof(f2019,plain,
! [X0] :
( ~ sQ1_spl
| ~ sQ70_spl
| ~ sQ65_spl
| ~ sQ73_spl
| ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ34_spl
| ~ sQ85_spl
| is_a_theorem(implies(X0,X0)) ),
inference(forward_demodulation,[status(thm)],[f495,f2011]) ).
fof(f2335,plain,
! [X0] :
( ~ sQ87_spl
| ~ sQ1_spl
| ~ sQ70_spl
| ~ sQ85_spl
| ~ sQ65_spl
| ~ sQ81_spl
| is_a_theorem(equiv(X0,X0))
| ~ is_a_theorem(implies(X0,X0)) ),
inference(paramodulation,[status(thm)],[f502,f1049]) ).
fof(f2338,plain,
! [X0] :
( ~ sQ87_spl
| ~ sQ1_spl
| ~ sQ70_spl
| ~ sQ85_spl
| ~ sQ65_spl
| ~ sQ81_spl
| ~ sQ73_spl
| ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ34_spl
| is_a_theorem(equiv(X0,X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f2335,f2019]) ).
fof(f5934,plain,
( ~ sQ15_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f238,f180]) ).
fof(f5935,plain,
~ sQ15_spl,
inference(contradiction_clause,[status(thm)],[f5934]) ).
fof(f8272,plain,
! [X0,X1] :
( ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ87_spl
| ~ sQ81_spl
| ~ sQ85_spl
| equiv(X0,not(X1)) = and(not(and(X0,X1)),or(X1,X0)) ),
inference(backward_demodulation,[status(thm)],[f8276,f622]) ).
fof(f8276,plain,
! [X0,X1,X2] :
( ~ sQ81_spl
| ~ sQ85_spl
| ~ sQ79_spl
| ~ sQ83_spl
| and(implies(X0,not(X1)),X2) = and(not(and(X0,X1)),X2) ),
inference(forward_demodulation,[status(thm)],[f618,f922]) ).
fof(f8447,plain,
! [X0,X1] :
( ~ sQ83_spl
| ~ sQ79_spl
| ~ sQ87_spl
| ~ sQ81_spl
| ~ sQ85_spl
| equiv(X0,not(not(X1))) = and(implies(X0,X1),or(not(X1),X0)) ),
inference(paramodulation,[status(thm)],[f488,f8272]) ).
fof(f8485,plain,
! [X0,X1] :
( ~ sQ83_spl
| ~ sQ79_spl
| ~ sQ87_spl
| ~ sQ81_spl
| ~ sQ85_spl
| equiv(X0,not(not(X1))) = and(implies(X0,X1),implies(X1,X0)) ),
inference(forward_demodulation,[status(thm)],[f495,f8447]) ).
fof(f8486,plain,
! [X0,X1] :
( ~ sQ83_spl
| ~ sQ79_spl
| ~ sQ87_spl
| ~ sQ81_spl
| ~ sQ85_spl
| equiv(X0,not(not(X1))) = equiv(X0,X1) ),
inference(forward_demodulation,[status(thm)],[f502,f8485]) ).
fof(f11006,plain,
! [X0] :
( ~ sQ83_spl
| ~ sQ79_spl
| ~ sQ87_spl
| ~ sQ81_spl
| ~ sQ85_spl
| ~ sQ1_spl
| ~ sQ70_spl
| ~ sQ65_spl
| ~ sQ73_spl
| ~ sQ34_spl
| is_a_theorem(equiv(not(not(X0)),X0)) ),
inference(paramodulation,[status(thm)],[f8486,f2338]) ).
fof(f11031,plain,
! [X0] :
( ~ sQ6_spl
| ~ sQ83_spl
| ~ sQ79_spl
| ~ sQ87_spl
| ~ sQ81_spl
| ~ sQ85_spl
| ~ sQ1_spl
| ~ sQ70_spl
| ~ sQ65_spl
| ~ sQ73_spl
| ~ sQ34_spl
| not(not(X0)) = X0 ),
inference(resolution,[status(thm)],[f11006,f204]) ).
fof(f11056,plain,
! [X0,X1] :
( ~ sQ81_spl
| ~ sQ85_spl
| ~ sQ6_spl
| ~ sQ83_spl
| ~ sQ79_spl
| ~ sQ87_spl
| ~ sQ1_spl
| ~ sQ70_spl
| ~ sQ65_spl
| ~ sQ73_spl
| ~ sQ34_spl
| not(and(X0,X1)) = implies(X0,not(X1)) ),
inference(paramodulation,[status(thm)],[f610,f11031]) ).
fof(f11060,plain,
! [X0,X1] :
( ~ sQ83_spl
| ~ sQ6_spl
| ~ sQ79_spl
| ~ sQ87_spl
| ~ sQ81_spl
| ~ sQ85_spl
| ~ sQ1_spl
| ~ sQ70_spl
| ~ sQ65_spl
| ~ sQ73_spl
| ~ sQ34_spl
| not(implies(X0,X1)) = and(X0,not(X1)) ),
inference(paramodulation,[status(thm)],[f488,f11031]) ).
fof(f12651,plain,
! [X0,X1] :
( ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ13_spl
| ~ sQ81_spl
| ~ sQ85_spl
| ~ sQ6_spl
| ~ sQ87_spl
| ~ sQ1_spl
| ~ sQ70_spl
| ~ sQ65_spl
| ~ sQ73_spl
| ~ sQ34_spl
| is_a_theorem(or(X0,not(and(X1,X0)))) ),
inference(backward_demodulation,[status(thm)],[f11056,f620]) ).
fof(f17990,plain,
! [X0,X1,X2] :
( ~ sQ83_spl
| ~ sQ85_spl
| ~ sQ25_spl
| ~ sQ1_spl
| ~ sQ76_spl
| is_a_theorem(or(implies(X2,X0),X1))
| ~ is_a_theorem(implies(not(X0),X1)) ),
inference(resolution,[status(thm)],[f1403,f1015]) ).
fof(f18003,plain,
! [X0,X1,X2] :
( ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ13_spl
| ~ sQ81_spl
| ~ sQ85_spl
| ~ sQ6_spl
| ~ sQ87_spl
| ~ sQ1_spl
| ~ sQ70_spl
| ~ sQ65_spl
| ~ sQ73_spl
| ~ sQ34_spl
| ~ sQ76_spl
| is_a_theorem(or(X1,X2))
| ~ is_a_theorem(implies(not(and(X0,X1)),X2)) ),
inference(resolution,[status(thm)],[f1403,f12651]) ).
fof(f18021,plain,
! [X0,X1,X2] :
( ~ sQ83_spl
| ~ sQ85_spl
| ~ sQ25_spl
| ~ sQ1_spl
| ~ sQ76_spl
| ~ sQ79_spl
| is_a_theorem(or(implies(X2,X0),X1))
| ~ is_a_theorem(or(X0,X1)) ),
inference(forward_demodulation,[status(thm)],[f615,f17990]) ).
fof(f18023,plain,
! [X0,X1,X2] :
( ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ13_spl
| ~ sQ81_spl
| ~ sQ85_spl
| ~ sQ6_spl
| ~ sQ87_spl
| ~ sQ1_spl
| ~ sQ70_spl
| ~ sQ65_spl
| ~ sQ73_spl
| ~ sQ34_spl
| ~ sQ76_spl
| is_a_theorem(or(X1,X2))
| ~ is_a_theorem(or(and(X0,X1),X2)) ),
inference(forward_demodulation,[status(thm)],[f615,f18003]) ).
fof(f19145,plain,
! [X0,X1] :
( ~ sQ81_spl
| ~ sQ85_spl
| ~ sQ70_spl
| ~ sQ6_spl
| ~ sQ83_spl
| ~ sQ79_spl
| ~ sQ87_spl
| ~ sQ1_spl
| ~ sQ65_spl
| ~ sQ73_spl
| ~ sQ34_spl
| is_a_theorem(or(and(X0,X1),not(and(X1,X0)))) ),
inference(forward_demodulation,[status(thm)],[f11056,f1952]) ).
fof(f26512,plain,
! [X0,X1] :
( ~ sQ65_spl
| ~ sQ1_spl
| ~ sQ83_spl
| ~ sQ85_spl
| ~ sQ25_spl
| ~ sQ76_spl
| ~ sQ79_spl
| is_a_theorem(implies(X1,X0))
| ~ is_a_theorem(or(X0,implies(X1,X0))) ),
inference(resolution,[status(thm)],[f18021,f593]) ).
fof(f27470,plain,
! [X0,X1] :
( ~ sQ81_spl
| ~ sQ85_spl
| ~ sQ70_spl
| ~ sQ6_spl
| ~ sQ83_spl
| ~ sQ79_spl
| ~ sQ87_spl
| ~ sQ1_spl
| ~ sQ65_spl
| ~ sQ73_spl
| ~ sQ34_spl
| ~ sQ13_spl
| ~ sQ76_spl
| is_a_theorem(or(X0,not(and(X0,X1)))) ),
inference(resolution,[status(thm)],[f18023,f19145]) ).
fof(f27571,plain,
! [X0,X1] :
( ~ sQ83_spl
| ~ sQ6_spl
| ~ sQ79_spl
| ~ sQ87_spl
| ~ sQ81_spl
| ~ sQ85_spl
| ~ sQ1_spl
| ~ sQ70_spl
| ~ sQ65_spl
| ~ sQ73_spl
| ~ sQ34_spl
| ~ sQ13_spl
| ~ sQ76_spl
| is_a_theorem(or(X0,not(not(implies(X0,X1))))) ),
inference(paramodulation,[status(thm)],[f11060,f27470]) ).
fof(f27595,plain,
! [X0,X1] :
( ~ sQ83_spl
| ~ sQ6_spl
| ~ sQ79_spl
| ~ sQ87_spl
| ~ sQ81_spl
| ~ sQ85_spl
| ~ sQ1_spl
| ~ sQ70_spl
| ~ sQ65_spl
| ~ sQ73_spl
| ~ sQ34_spl
| ~ sQ13_spl
| ~ sQ76_spl
| is_a_theorem(or(X0,implies(X0,X1))) ),
inference(forward_demodulation,[status(thm)],[f11031,f27571]) ).
fof(f27634,plain,
! [X0,X1,X2] :
( ~ sQ1_spl
| ~ sQ76_spl
| ~ sQ83_spl
| ~ sQ6_spl
| ~ sQ79_spl
| ~ sQ87_spl
| ~ sQ81_spl
| ~ sQ85_spl
| ~ sQ70_spl
| ~ sQ65_spl
| ~ sQ73_spl
| ~ sQ34_spl
| ~ sQ13_spl
| is_a_theorem(or(X0,X2))
| ~ is_a_theorem(implies(implies(X0,X1),X2)) ),
inference(resolution,[status(thm)],[f27595,f1403]) ).
fof(f46756,plain,
! [X0,X1,X2] :
( ~ sQ85_spl
| ~ sQ76_spl
| ~ sQ1_spl
| ~ sQ83_spl
| ~ sQ6_spl
| ~ sQ79_spl
| ~ sQ87_spl
| ~ sQ81_spl
| ~ sQ70_spl
| ~ sQ65_spl
| ~ sQ73_spl
| ~ sQ34_spl
| ~ sQ13_spl
| is_a_theorem(or(X0,implies(implies(X1,X0),implies(X1,X2)))) ),
inference(resolution,[status(thm)],[f27634,f1592]) ).
fof(f73026,plain,
! [X0,X1] :
( ~ sQ65_spl
| ~ sQ1_spl
| ~ sQ83_spl
| ~ sQ85_spl
| ~ sQ25_spl
| ~ sQ76_spl
| ~ sQ79_spl
| ~ sQ6_spl
| ~ sQ87_spl
| ~ sQ81_spl
| ~ sQ70_spl
| ~ sQ73_spl
| ~ sQ34_spl
| ~ sQ13_spl
| is_a_theorem(implies(implies(X0,implies(X0,X1)),implies(X0,X1))) ),
inference(resolution,[status(thm)],[f46756,f26512]) ).
fof(f73052,plain,
( ~ sQ65_spl
| ~ sQ1_spl
| ~ sQ83_spl
| ~ sQ85_spl
| ~ sQ25_spl
| ~ sQ76_spl
| ~ sQ79_spl
| ~ sQ6_spl
| ~ sQ87_spl
| ~ sQ81_spl
| ~ sQ70_spl
| ~ sQ73_spl
| ~ sQ34_spl
| ~ sQ13_spl
| sQ16_spl ),
inference(split_clause,[status(thm)],[f73026,f240,f229,f306,f451,f440,f480,f501,f203,f473,f462,f273,f494,f487,f184,f421]) ).
fof(f73069,plain,
$false,
inference(sat_refutation,[status(thm)],[f187,f206,f247,f424,f432,f443,f454,f465,f476,f483,f490,f497,f504,f506,f508,f510,f512,f514,f516,f518,f522,f533,f543,f547,f552,f587,f590,f987,f5935,f73052]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL485+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n005.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Mon Sep 21 00:33:49 UTC 2026
% 0.12/0.35 % CPUTime :
% 0.12/0.37 % Drodi V4.1.1
% 107.92/14.09 % Refutation found
% 107.92/14.09 % SZS status Theorem for theBenchmark: Theorem is valid
% 107.92/14.09 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 7.20/14.48 % Elapsed time: 14.105991 seconds
% 7.20/14.48 % CPU time: 110.016573 seconds
% 7.20/14.48 % Total memory used: 1.361 GB
% 7.20/14.48 % Net memory used: 1.273 GB
%------------------------------------------------------------------------------