%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWC122+1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n018.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 02:40:03 PM UTC 2026
% Result : Theorem 0.21s 0.69s
% Output : CNFRefutation 0.21s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 207
% Syntax : Number of formulae : 732 ( 19 unt; 187 def)
% Number of atoms : 3410 ( 202 equ)
% Maximal formula atoms : 14 ( 4 avg)
% Number of connectives : 5058 (2380 ~;2380 |; 54 &)
% ( 197 <=>; 47 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 7 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 194 ( 192 usr; 188 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 5 con; 0-2 aty)
% Number of variables : 836 ( 820 !; 16 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f5,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ( frontsegP(U,V)
<=> ? [W] :
( app(V,W) = U
& ssList(W) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ( rearsegP(U,V)
<=> ? [W] :
( app(W,V) = U
& ssList(W) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ( segmentP(U,V)
<=> ? [W] :
( ? [X] :
( app(app(W,V),X) = U
& ssList(X) )
& ssList(W) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ( neq(U,V)
<=> U != V ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f17,axiom,
ssList(nil),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f28,axiom,
! [U] :
( ssList(U)
=> app(nil,U) = U ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f45,axiom,
! [U] :
( ssList(U)
=> frontsegP(U,nil) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f47,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ! [W] :
( ssList(W)
=> ( ( rearsegP(V,W)
& rearsegP(U,V) )
=> rearsegP(U,W) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f48,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ( ( rearsegP(V,U)
& rearsegP(U,V) )
=> U = V ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f49,axiom,
! [U] :
( ssList(U)
=> rearsegP(U,U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f50,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ! [W] :
( ssList(W)
=> ( rearsegP(U,V)
=> rearsegP(app(W,U),V) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f51,axiom,
! [U] :
( ssList(U)
=> rearsegP(U,nil) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f52,axiom,
! [U] :
( ssList(U)
=> ( rearsegP(nil,U)
<=> nil = U ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f53,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ! [W] :
( ssList(W)
=> ( ( segmentP(V,W)
& segmentP(U,V) )
=> segmentP(U,W) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f54,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ( ( segmentP(V,U)
& segmentP(U,V) )
=> U = V ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f55,axiom,
! [U] :
( ssList(U)
=> segmentP(U,U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f56,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ! [W] :
( ssList(W)
=> ! [X] :
( ssList(X)
=> ( segmentP(U,V)
=> segmentP(app(app(W,U),X),V) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f57,axiom,
! [U] :
( ssList(U)
=> segmentP(U,nil) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f84,axiom,
! [U] :
( ssList(U)
=> app(U,nil) = U ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f96,conjecture,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ! [W] :
( ssList(W)
=> ! [X] :
( ssList(X)
=> ( ( ( ~ rearsegP(X,W)
| ~ neq(W,nil) )
& neq(X,nil) )
| ( segmentP(V,U)
& neq(U,nil) )
| ( nil = X
& nil != W )
| ~ neq(V,nil)
| U != W
| V != X ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f97,negated_conjecture,
~ ! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ! [W] :
( ssList(W)
=> ! [X] :
( ssList(X)
=> ( ( ( ~ rearsegP(X,W)
| ~ neq(W,nil) )
& neq(X,nil) )
| ( segmentP(V,U)
& neq(U,nil) )
| ( nil = X
& nil != W )
| ~ neq(V,nil)
| U != W
| V != X ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f96]) ).
fof(f119,plain,
! [U] :
( ! [V] :
( ( frontsegP(U,V)
<=> ? [W] :
( app(V,W) = U
& ssList(W) ) )
| ~ ssList(V) )
| ~ ssList(U) ),
inference(pre_NNF_transformation,[status(thm)],[f5]) ).
fof(f120,plain,
! [U] :
( ! [V] :
( ( ( ! [W] :
( app(V,W) != U
| ~ ssList(W) )
| frontsegP(U,V) )
& ( ? [W] :
( app(V,W) = U
& ssList(W) )
| ~ frontsegP(U,V) ) )
| ~ ssList(V) )
| ~ ssList(U) ),
inference(NNF_transformation,[status(thm)],[f119]) ).
fof(f121,plain,
! [U] :
( ! [V] :
( ( ( ! [W] :
( app(V,W) != U
| ~ ssList(W) )
| frontsegP(U,V) )
& ( ( app(V,sK5_skl(V,U)) = U
& ssList(sK5_skl(V,U)) )
| ~ frontsegP(U,V) ) )
| ~ ssList(V) )
| ~ ssList(U) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl]),skolemize(W,sK5_skl(V,U))],[f120]) ).
fof(f122,plain,
! [X0,X1] :
( ssList(sK5_skl(X1,X0))
| ~ frontsegP(X0,X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f121]) ).
fof(f123,plain,
! [X0,X1] :
( app(X1,sK5_skl(X1,X0)) = X0
| ~ frontsegP(X0,X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f121]) ).
fof(f124,plain,
! [X0,X1,X2] :
( app(X1,X2) != X0
| ~ ssList(X2)
| frontsegP(X0,X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f121]) ).
fof(f125,plain,
! [U] :
( ! [V] :
( ( rearsegP(U,V)
<=> ? [W] :
( app(W,V) = U
& ssList(W) ) )
| ~ ssList(V) )
| ~ ssList(U) ),
inference(pre_NNF_transformation,[status(thm)],[f6]) ).
fof(f126,plain,
! [U] :
( ! [V] :
( ( ( ! [W] :
( app(W,V) != U
| ~ ssList(W) )
| rearsegP(U,V) )
& ( ? [W] :
( app(W,V) = U
& ssList(W) )
| ~ rearsegP(U,V) ) )
| ~ ssList(V) )
| ~ ssList(U) ),
inference(NNF_transformation,[status(thm)],[f125]) ).
fof(f127,plain,
! [U] :
( ! [V] :
( ( ( ! [W] :
( app(W,V) != U
| ~ ssList(W) )
| rearsegP(U,V) )
& ( ( app(sK6_skl(V,U),V) = U
& ssList(sK6_skl(V,U)) )
| ~ rearsegP(U,V) ) )
| ~ ssList(V) )
| ~ ssList(U) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6_skl]),skolemize(W,sK6_skl(V,U))],[f126]) ).
fof(f128,plain,
! [X0,X1] :
( ssList(sK6_skl(X1,X0))
| ~ rearsegP(X0,X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f127]) ).
fof(f129,plain,
! [X0,X1] :
( app(sK6_skl(X1,X0),X1) = X0
| ~ rearsegP(X0,X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f127]) ).
fof(f131,plain,
! [U] :
( ! [V] :
( ( segmentP(U,V)
<=> ? [W] :
( ? [X] :
( app(app(W,V),X) = U
& ssList(X) )
& ssList(W) ) )
| ~ ssList(V) )
| ~ ssList(U) ),
inference(pre_NNF_transformation,[status(thm)],[f7]) ).
fof(f132,plain,
! [U] :
( ! [V] :
( ( ( ! [W] :
( ! [X] :
( app(app(W,V),X) != U
| ~ ssList(X) )
| ~ ssList(W) )
| segmentP(U,V) )
& ( ? [W] :
( ? [X] :
( app(app(W,V),X) = U
& ssList(X) )
& ssList(W) )
| ~ segmentP(U,V) ) )
| ~ ssList(V) )
| ~ ssList(U) ),
inference(NNF_transformation,[status(thm)],[f131]) ).
fof(f133,plain,
! [U] :
( ! [V] :
( ( ( ! [W] :
( ! [X] :
( app(app(W,V),X) != U
| ~ ssList(X) )
| ~ ssList(W) )
| segmentP(U,V) )
& ( ( app(app(sK7_skl(V,U),V),sK8_skl(V,U)) = U
& ssList(sK8_skl(V,U))
& ssList(sK7_skl(V,U)) )
| ~ segmentP(U,V) ) )
| ~ ssList(V) )
| ~ ssList(U) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl,sK8_skl]),skolemize(W,sK7_skl(V,U)),skolemize(X,sK8_skl(V,U))],[f132]) ).
fof(f136,plain,
! [X0,X1] :
( app(app(sK7_skl(X1,X0),X1),sK8_skl(X1,X0)) = X0
| ~ segmentP(X0,X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f133]) ).
fof(f137,plain,
! [X0,X1,X2,X3] :
( app(app(X2,X1),X3) != X0
| ~ ssList(X3)
| ~ ssList(X2)
| segmentP(X0,X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f133]) ).
fof(f217,plain,
! [U] :
( ! [V] :
( ( neq(U,V)
<=> U != V )
| ~ ssList(V) )
| ~ ssList(U) ),
inference(pre_NNF_transformation,[status(thm)],[f15]) ).
fof(f218,plain,
! [U] :
( ! [V] :
( ( ( U = V
| neq(U,V) )
& ( U != V
| ~ neq(U,V) ) )
| ~ ssList(V) )
| ~ ssList(U) ),
inference(NNF_transformation,[status(thm)],[f217]) ).
fof(f219,plain,
! [X0,X1] :
( X0 != X1
| ~ neq(X0,X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f218]) ).
fof(f220,plain,
! [X0,X1] :
( X0 = X1
| neq(X0,X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f218]) ).
fof(f223,plain,
ssList(nil),
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f248,plain,
! [U] :
( app(nil,U) = U
| ~ ssList(U) ),
inference(pre_NNF_transformation,[status(thm)],[f28]) ).
fof(f249,plain,
! [X0] :
( app(nil,X0) = X0
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f248]) ).
fof(f294,plain,
! [U] :
( frontsegP(U,nil)
| ~ ssList(U) ),
inference(pre_NNF_transformation,[status(thm)],[f45]) ).
fof(f295,plain,
! [X0] :
( frontsegP(X0,nil)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f294]) ).
fof(f300,plain,
! [U] :
( ! [V] :
( ! [W] :
( rearsegP(U,W)
| ~ rearsegP(V,W)
| ~ rearsegP(U,V)
| ~ ssList(W) )
| ~ ssList(V) )
| ~ ssList(U) ),
inference(pre_NNF_transformation,[status(thm)],[f47]) ).
fof(f301,plain,
! [X0,X1,X2] :
( rearsegP(X0,X2)
| ~ rearsegP(X1,X2)
| ~ rearsegP(X0,X1)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f300]) ).
fof(f302,plain,
! [U] :
( ! [V] :
( U = V
| ~ rearsegP(V,U)
| ~ rearsegP(U,V)
| ~ ssList(V) )
| ~ ssList(U) ),
inference(pre_NNF_transformation,[status(thm)],[f48]) ).
fof(f303,plain,
! [X0,X1] :
( X0 = X1
| ~ rearsegP(X1,X0)
| ~ rearsegP(X0,X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f302]) ).
fof(f304,plain,
! [U] :
( rearsegP(U,U)
| ~ ssList(U) ),
inference(pre_NNF_transformation,[status(thm)],[f49]) ).
fof(f305,plain,
! [X0] :
( rearsegP(X0,X0)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f304]) ).
fof(f306,plain,
! [U] :
( ! [V] :
( ! [W] :
( rearsegP(app(W,U),V)
| ~ rearsegP(U,V)
| ~ ssList(W) )
| ~ ssList(V) )
| ~ ssList(U) ),
inference(pre_NNF_transformation,[status(thm)],[f50]) ).
fof(f307,plain,
! [X0,X1,X2] :
( rearsegP(app(X2,X0),X1)
| ~ rearsegP(X0,X1)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f306]) ).
fof(f308,plain,
! [U] :
( rearsegP(U,nil)
| ~ ssList(U) ),
inference(pre_NNF_transformation,[status(thm)],[f51]) ).
fof(f309,plain,
! [X0] :
( rearsegP(X0,nil)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f308]) ).
fof(f310,plain,
! [U] :
( ( rearsegP(nil,U)
<=> nil = U )
| ~ ssList(U) ),
inference(pre_NNF_transformation,[status(thm)],[f52]) ).
fof(f311,plain,
! [U] :
( ( ( nil != U
| rearsegP(nil,U) )
& ( nil = U
| ~ rearsegP(nil,U) ) )
| ~ ssList(U) ),
inference(NNF_transformation,[status(thm)],[f310]) ).
fof(f312,plain,
! [X0] :
( nil = X0
| ~ rearsegP(nil,X0)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f311]) ).
fof(f314,plain,
! [U] :
( ! [V] :
( ! [W] :
( segmentP(U,W)
| ~ segmentP(V,W)
| ~ segmentP(U,V)
| ~ ssList(W) )
| ~ ssList(V) )
| ~ ssList(U) ),
inference(pre_NNF_transformation,[status(thm)],[f53]) ).
fof(f315,plain,
! [X0,X1,X2] :
( segmentP(X0,X2)
| ~ segmentP(X1,X2)
| ~ segmentP(X0,X1)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f314]) ).
fof(f316,plain,
! [U] :
( ! [V] :
( U = V
| ~ segmentP(V,U)
| ~ segmentP(U,V)
| ~ ssList(V) )
| ~ ssList(U) ),
inference(pre_NNF_transformation,[status(thm)],[f54]) ).
fof(f317,plain,
! [X0,X1] :
( X0 = X1
| ~ segmentP(X1,X0)
| ~ segmentP(X0,X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f316]) ).
fof(f318,plain,
! [U] :
( segmentP(U,U)
| ~ ssList(U) ),
inference(pre_NNF_transformation,[status(thm)],[f55]) ).
fof(f319,plain,
! [X0] :
( segmentP(X0,X0)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f318]) ).
fof(f320,plain,
! [U] :
( ! [V] :
( ! [W] :
( ! [X] :
( segmentP(app(app(W,U),X),V)
| ~ segmentP(U,V)
| ~ ssList(X) )
| ~ ssList(W) )
| ~ ssList(V) )
| ~ ssList(U) ),
inference(pre_NNF_transformation,[status(thm)],[f56]) ).
fof(f321,plain,
! [X0,X1,X2,X3] :
( segmentP(app(app(X2,X0),X3),X1)
| ~ segmentP(X0,X1)
| ~ ssList(X3)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f320]) ).
fof(f322,plain,
! [U] :
( segmentP(U,nil)
| ~ ssList(U) ),
inference(pre_NNF_transformation,[status(thm)],[f57]) ).
fof(f323,plain,
! [X0] :
( segmentP(X0,nil)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f322]) ).
fof(f388,plain,
! [U] :
( app(U,nil) = U
| ~ ssList(U) ),
inference(pre_NNF_transformation,[status(thm)],[f84]) ).
fof(f389,plain,
! [X0] :
( app(X0,nil) = X0
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f388]) ).
fof(f415,plain,
? [U] :
( ? [V] :
( ? [W] :
( ? [X] :
( ( ( rearsegP(X,W)
& neq(W,nil) )
| ~ neq(X,nil) )
& ( ~ segmentP(V,U)
| ~ neq(U,nil) )
& ( nil != X
| nil = W )
& neq(V,nil)
& U = W
& V = X
& ssList(X) )
& ssList(W) )
& ssList(V) )
& ssList(U) ),
inference(pre_NNF_transformation,[status(thm)],[f97]) ).
fof(f416,plain,
( ( ( rearsegP(sK50_skl,sK49_skl)
& neq(sK49_skl,nil) )
| ~ neq(sK50_skl,nil) )
& ( ~ segmentP(sK48_skl,sK47_skl)
| ~ neq(sK47_skl,nil) )
& ( nil != sK50_skl
| nil = sK49_skl )
& neq(sK48_skl,nil)
& sK47_skl = sK49_skl
& sK48_skl = sK50_skl
& ssList(sK50_skl)
& ssList(sK49_skl)
& ssList(sK48_skl)
& ssList(sK47_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK47_skl,sK48_skl,sK49_skl,sK50_skl]),skolemize(U,sK47_skl),skolemize(V,sK48_skl),skolemize(W,sK49_skl),skolemize(X,sK50_skl)],[f415]) ).
fof(f419,plain,
ssList(sK49_skl),
inference(cnf_transformation,[status(thm)],[f416]) ).
fof(f420,plain,
ssList(sK50_skl),
inference(cnf_transformation,[status(thm)],[f416]) ).
fof(f421,plain,
sK48_skl = sK50_skl,
inference(cnf_transformation,[status(thm)],[f416]) ).
fof(f422,plain,
sK47_skl = sK49_skl,
inference(cnf_transformation,[status(thm)],[f416]) ).
fof(f423,plain,
neq(sK48_skl,nil),
inference(cnf_transformation,[status(thm)],[f416]) ).
fof(f424,plain,
( nil != sK50_skl
| nil = sK49_skl ),
inference(cnf_transformation,[status(thm)],[f416]) ).
fof(f425,plain,
( ~ segmentP(sK48_skl,sK47_skl)
| ~ neq(sK47_skl,nil) ),
inference(cnf_transformation,[status(thm)],[f416]) ).
fof(f426,plain,
( neq(sK49_skl,nil)
| ~ neq(sK50_skl,nil) ),
inference(cnf_transformation,[status(thm)],[f416]) ).
fof(f427,plain,
( rearsegP(sK50_skl,sK49_skl)
| ~ neq(sK50_skl,nil) ),
inference(cnf_transformation,[status(thm)],[f416]) ).
fof(f428,definition,
( sQ0_spl
<=> nil = sK49_skl ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f429,plain,
( ~ sQ0_spl
| nil = sK49_skl ),
inference(component_clause,[status(thm)],[f428]) ).
fof(f431,definition,
( sQ1_spl
<=> nil = sK50_skl ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f434,plain,
( ~ sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f424,f428,f431]) ).
fof(f435,definition,
( sQ2_spl
<=> neq(sK47_skl,nil) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f437,plain,
( sQ2_spl
| ~ neq(sK47_skl,nil) ),
inference(component_clause,[status(thm)],[f435]) ).
fof(f438,definition,
( sQ3_spl
<=> segmentP(sK48_skl,sK47_skl) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f440,plain,
( sQ3_spl
| ~ segmentP(sK48_skl,sK47_skl) ),
inference(component_clause,[status(thm)],[f438]) ).
fof(f441,plain,
( ~ sQ3_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f425,f435,f438]) ).
fof(f442,definition,
( sQ4_spl
<=> neq(sK50_skl,nil) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f444,plain,
( sQ4_spl
| ~ neq(sK50_skl,nil) ),
inference(component_clause,[status(thm)],[f442]) ).
fof(f445,definition,
( sQ5_spl
<=> neq(sK49_skl,nil) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f446,plain,
( ~ sQ5_spl
| neq(sK49_skl,nil) ),
inference(component_clause,[status(thm)],[f445]) ).
fof(f448,plain,
( sQ5_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f426,f442,f445]) ).
fof(f449,definition,
( sQ6_spl
<=> rearsegP(sK50_skl,sK49_skl) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f450,plain,
( ~ sQ6_spl
| rearsegP(sK50_skl,sK49_skl) ),
inference(component_clause,[status(thm)],[f449]) ).
fof(f452,plain,
( sQ6_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f427,f442,f449]) ).
fof(f457,plain,
! [X0,X1] :
( ~ ssList(X1)
| frontsegP(app(X0,X1),X0)
| ~ ssList(X0)
| ~ ssList(app(X0,X1)) ),
inference(destructive_equality_resolution,[status(thm)],[f124]) ).
fof(f459,plain,
! [X0,X1,X2] :
( ~ ssList(X2)
| ~ ssList(X0)
| segmentP(app(app(X0,X1),X2),X1)
| ~ ssList(X1)
| ~ ssList(app(app(X0,X1),X2)) ),
inference(destructive_equality_resolution,[status(thm)],[f137]) ).
fof(f468,plain,
! [X1] :
( ~ neq(X1,X1)
| ~ ssList(X1)
| ~ ssList(X1) ),
inference(destructive_equality_resolution,[status(thm)],[f219]) ).
fof(f469,plain,
! [X0] :
( ~ neq(X0,X0)
| ~ ssList(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f468]) ).
fof(f494,plain,
neq(sK50_skl,nil),
inference(forward_demodulation,[status(thm)],[f421,f423]) ).
fof(f495,plain,
( ~ sQ0_spl
| neq(sK50_skl,sK49_skl) ),
inference(forward_demodulation,[status(thm)],[f429,f494]) ).
fof(f496,plain,
( sQ4_spl
| ~ sQ0_spl
| ~ neq(sK50_skl,sK49_skl) ),
inference(forward_demodulation,[status(thm)],[f429,f444]) ).
fof(f497,plain,
( sQ4_spl
| ~ sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f496,f495]) ).
fof(f498,plain,
( sQ4_spl
| ~ sQ0_spl ),
inference(contradiction_clause,[status(thm)],[f497]) ).
fof(f500,plain,
( sQ2_spl
| ~ neq(sK49_skl,nil) ),
inference(forward_demodulation,[status(thm)],[f422,f437]) ).
fof(f501,plain,
( sQ2_spl
| sK49_skl = nil
| ~ ssList(nil)
| ~ ssList(sK49_skl) ),
inference(resolution,[status(thm)],[f500,f220]) ).
fof(f502,definition,
( sQ7_spl
<=> ssList(sK49_skl) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f504,plain,
( sQ7_spl
| ~ ssList(sK49_skl) ),
inference(component_clause,[status(thm)],[f502]) ).
fof(f505,definition,
( sQ8_spl
<=> ssList(nil) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f507,plain,
( sQ8_spl
| ~ ssList(nil) ),
inference(component_clause,[status(thm)],[f505]) ).
fof(f508,plain,
( sQ2_spl
| sQ0_spl
| ~ sQ8_spl
| ~ sQ7_spl ),
inference(split_clause,[status(thm)],[f501,f502,f505,f428,f435]) ).
fof(f509,plain,
( sQ3_spl
| ~ segmentP(sK50_skl,sK47_skl) ),
inference(forward_demodulation,[status(thm)],[f421,f440]) ).
fof(f510,plain,
( sQ3_spl
| ~ segmentP(sK50_skl,sK49_skl) ),
inference(forward_demodulation,[status(thm)],[f422,f509]) ).
fof(f511,plain,
( sQ8_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f507,f223]) ).
fof(f512,plain,
sQ8_spl,
inference(contradiction_clause,[status(thm)],[f511]) ).
fof(f513,plain,
( sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f504,f419]) ).
fof(f514,plain,
sQ7_spl,
inference(contradiction_clause,[status(thm)],[f513]) ).
fof(f522,plain,
! [X0,X1,X2,X3] :
( ~ rearsegP(X3,X2)
| ~ rearsegP(X1,X3)
| ~ ssList(X2)
| ~ ssList(X3)
| ~ ssList(X1)
| rearsegP(X0,X2)
| ~ rearsegP(X0,X1)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f301,f301]) ).
fof(f524,plain,
! [X0,X1,X2,X3] :
( ~ rearsegP(X3,X2)
| ~ rearsegP(X1,X3)
| ~ ssList(X3)
| rearsegP(X0,X2)
| ~ rearsegP(X0,X1)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f522]) ).
fof(f526,plain,
! [X0,X1,X2] :
( ~ rearsegP(X2,X0)
| ~ rearsegP(X1,X2)
| ~ ssList(X0)
| ~ ssList(X2)
| ~ ssList(X1)
| X0 = X1
| ~ rearsegP(X0,X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f303,f301]) ).
fof(f527,plain,
! [X0,X1,X2] :
( ~ rearsegP(X2,X0)
| ~ rearsegP(X1,X2)
| ~ ssList(X2)
| X0 = X1
| ~ rearsegP(X0,X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f526]) ).
fof(f531,plain,
! [X0,X1,X2] :
( ~ rearsegP(X2,X1)
| ~ rearsegP(X0,X2)
| ~ ssList(X1)
| ~ ssList(X2)
| ~ ssList(X0)
| app(sK6_skl(X1,X0),X1) = X0
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f129,f301]) ).
fof(f532,plain,
! [X0,X1,X2] :
( ~ rearsegP(X2,X1)
| ~ rearsegP(X0,X2)
| ~ ssList(X2)
| app(sK6_skl(X1,X0),X1) = X0
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f531]) ).
fof(f533,plain,
! [X0] :
( app(sK6_skl(X0,X0),X0) = X0
| ~ ssList(X0)
| ~ ssList(X0)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f305,f129]) ).
fof(f536,plain,
! [X0] :
( app(sK6_skl(X0,X0),X0) = X0
| ~ ssList(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f533]) ).
fof(f537,plain,
! [X0,X1] :
( ~ ssList(X0)
| rearsegP(app(X1,X0),X0)
| ~ ssList(X1)
| ~ ssList(X0)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f307,f305]) ).
fof(f538,plain,
! [X0,X1,X2,X3] :
( ~ rearsegP(X3,X1)
| ~ rearsegP(X0,X3)
| ~ ssList(X1)
| ~ ssList(X3)
| ~ ssList(X0)
| rearsegP(app(X2,X0),X1)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f307,f301]) ).
fof(f539,plain,
! [X0,X1] :
( rearsegP(app(X1,X0),X0)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f537]) ).
fof(f540,plain,
! [X0,X1,X2,X3] :
( ~ rearsegP(X3,X1)
| ~ rearsegP(X0,X3)
| ~ ssList(X3)
| rearsegP(app(X2,X0),X1)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f538]) ).
fof(f543,plain,
( ~ sQ5_spl
| ~ sQ0_spl
| neq(sK49_skl,sK49_skl) ),
inference(forward_demodulation,[status(thm)],[f429,f446]) ).
fof(f544,plain,
( ~ sQ5_spl
| ~ sQ0_spl
| ~ ssList(sK49_skl) ),
inference(resolution,[status(thm)],[f543,f469]) ).
fof(f545,plain,
( ~ sQ5_spl
| ~ sQ0_spl
| ~ sQ7_spl ),
inference(split_clause,[status(thm)],[f544,f502,f428,f445]) ).
fof(f547,plain,
! [X0,X1] :
( rearsegP(app(X1,X0),nil)
| ~ ssList(X1)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f309,f307]) ).
fof(f548,plain,
! [X0] :
( app(sK6_skl(nil,X0),nil) = X0
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f309,f129]) ).
fof(f549,plain,
! [X0] :
( nil = X0
| ~ rearsegP(nil,X0)
| ~ ssList(X0)
| ~ ssList(nil)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f309,f303]) ).
fof(f550,plain,
! [X0,X1] :
( rearsegP(X1,nil)
| ~ rearsegP(X1,X0)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f309,f301]) ).
fof(f551,definition,
! [X0,X1] :
( sQ9_spl
<=> ( rearsegP(app(X1,X0),nil)
| ~ ssList(X1)
| ~ ssList(X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f552,plain,
! [X0,X1] :
( ~ sQ9_spl
| rearsegP(app(X1,X0),nil)
| ~ ssList(X1)
| ~ ssList(X0)
| ~ ssList(X0) ),
inference(component_clause,[status(thm)],[f551]) ).
fof(f554,plain,
( ~ sQ8_spl
| sQ9_spl ),
inference(split_clause,[status(thm)],[f547,f551,f505]) ).
fof(f555,definition,
! [X0] :
( sQ10_spl
<=> ( app(sK6_skl(nil,X0),nil) = X0
| ~ ssList(X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f558,plain,
( ~ sQ8_spl
| sQ10_spl ),
inference(split_clause,[status(thm)],[f548,f555,f505]) ).
fof(f559,definition,
! [X0] :
( sQ11_spl
<=> ( nil = X0
| ~ rearsegP(nil,X0)
| ~ ssList(X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f562,plain,
( ~ sQ8_spl
| sQ11_spl ),
inference(split_clause,[status(thm)],[f549,f559,f505]) ).
fof(f563,definition,
! [X0,X1] :
( sQ12_spl
<=> ( rearsegP(X1,nil)
| ~ rearsegP(X1,X0)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f566,plain,
( ~ sQ8_spl
| sQ12_spl ),
inference(split_clause,[status(thm)],[f550,f563,f505]) ).
fof(f567,plain,
! [X0,X1] :
( ~ sQ9_spl
| rearsegP(app(X1,X0),nil)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f552]) ).
fof(f571,plain,
( ~ ssList(nil)
| nil = nil
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f312,f309]) ).
fof(f573,plain,
! [X0,X1] :
( ~ rearsegP(X1,X0)
| ~ rearsegP(nil,X1)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(nil)
| nil = X0
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f312,f301]) ).
fof(f574,definition,
( sQ13_spl
<=> nil = nil ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f577,plain,
( sQ13_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f571,f505,f574]) ).
fof(f579,definition,
! [X0,X1] :
( sQ14_spl
<=> ( ~ rearsegP(X1,X0)
| ~ rearsegP(nil,X1)
| ~ ssList(X0)
| ~ ssList(X1)
| nil = X0
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f580,plain,
! [X0,X1] :
( ~ sQ14_spl
| ~ rearsegP(X1,X0)
| ~ rearsegP(nil,X1)
| ~ ssList(X0)
| ~ ssList(X1)
| nil = X0
| ~ ssList(X0) ),
inference(component_clause,[status(thm)],[f579]) ).
fof(f582,plain,
( ~ sQ8_spl
| sQ14_spl ),
inference(split_clause,[status(thm)],[f573,f579,f505]) ).
fof(f583,plain,
! [X0,X1] :
( ~ sQ14_spl
| ~ rearsegP(X1,X0)
| ~ rearsegP(nil,X1)
| ~ ssList(X1)
| nil = X0
| ~ ssList(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f580]) ).
fof(f588,plain,
( sQ4_spl
| sK50_skl = nil
| ~ ssList(nil)
| ~ ssList(sK50_skl) ),
inference(resolution,[status(thm)],[f444,f220]) ).
fof(f589,definition,
( sQ15_spl
<=> ssList(sK50_skl) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f591,plain,
( sQ15_spl
| ~ ssList(sK50_skl) ),
inference(component_clause,[status(thm)],[f589]) ).
fof(f592,plain,
( sQ4_spl
| sQ1_spl
| ~ sQ8_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f588,f589,f505,f431,f442]) ).
fof(f593,plain,
( sQ15_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f591,f420]) ).
fof(f594,plain,
sQ15_spl,
inference(contradiction_clause,[status(thm)],[f593]) ).
fof(f616,plain,
( ~ sQ6_spl
| app(sK6_skl(sK49_skl,sK50_skl),sK49_skl) = sK50_skl
| ~ ssList(sK49_skl)
| ~ ssList(sK50_skl) ),
inference(resolution,[status(thm)],[f450,f129]) ).
fof(f623,definition,
( sQ21_spl
<=> app(sK6_skl(sK49_skl,sK50_skl),sK49_skl) = sK50_skl ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f624,plain,
( ~ sQ21_spl
| app(sK6_skl(sK49_skl,sK50_skl),sK49_skl) = sK50_skl ),
inference(component_clause,[status(thm)],[f623]) ).
fof(f626,plain,
( ~ sQ6_spl
| sQ21_spl
| ~ sQ7_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f616,f589,f502,f623,f449]) ).
fof(f651,plain,
! [X0,X1,X2] :
( ~ ssList(X0)
| segmentP(app(app(X1,X0),X2),X0)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f321,f319]) ).
fof(f652,plain,
! [X0,X1,X2] :
( segmentP(app(app(X1,X0),X2),X0)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f651]) ).
fof(f653,plain,
! [X0,X1,X2] :
( segmentP(app(app(X1,X0),X2),nil)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f323,f321]) ).
fof(f654,plain,
! [X0] :
( nil = X0
| ~ segmentP(nil,X0)
| ~ ssList(X0)
| ~ ssList(nil)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f323,f317]) ).
fof(f655,plain,
! [X0,X1] :
( segmentP(X1,nil)
| ~ segmentP(X1,X0)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f323,f315]) ).
fof(f656,plain,
! [X0] :
( app(app(sK7_skl(nil,X0),nil),sK8_skl(nil,X0)) = X0
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f323,f136]) ).
fof(f657,definition,
! [X0,X1,X2] :
( sQ26_spl
<=> ( segmentP(app(app(X1,X0),X2),nil)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f658,plain,
! [X0,X1,X2] :
( ~ sQ26_spl
| segmentP(app(app(X1,X0),X2),nil)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0)
| ~ ssList(X0) ),
inference(component_clause,[status(thm)],[f657]) ).
fof(f660,plain,
( ~ sQ8_spl
| sQ26_spl ),
inference(split_clause,[status(thm)],[f653,f657,f505]) ).
fof(f661,definition,
! [X0] :
( sQ27_spl
<=> ( nil = X0
| ~ segmentP(nil,X0)
| ~ ssList(X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f664,plain,
( ~ sQ8_spl
| sQ27_spl ),
inference(split_clause,[status(thm)],[f654,f661,f505]) ).
fof(f665,definition,
! [X0,X1] :
( sQ28_spl
<=> ( segmentP(X1,nil)
| ~ segmentP(X1,X0)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f668,plain,
( ~ sQ8_spl
| sQ28_spl ),
inference(split_clause,[status(thm)],[f655,f665,f505]) ).
fof(f669,definition,
! [X0] :
( sQ29_spl
<=> ( app(app(sK7_skl(nil,X0),nil),sK8_skl(nil,X0)) = X0
| ~ ssList(X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f672,plain,
( ~ sQ8_spl
| sQ29_spl ),
inference(split_clause,[status(thm)],[f656,f669,f505]) ).
fof(f673,plain,
! [X0,X1,X2] :
( ~ sQ26_spl
| segmentP(app(app(X1,X0),X2),nil)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f658]) ).
fof(f681,definition,
! [X0] :
( sQ30_spl
<=> ( rearsegP(app(X0,sK50_skl),sK50_skl)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f682,plain,
! [X0] :
( ~ sQ30_spl
| rearsegP(app(X0,sK50_skl),sK50_skl)
| ~ ssList(X0) ),
inference(component_clause,[status(thm)],[f681]) ).
fof(f685,definition,
( sQ31_spl
<=> app(sK6_skl(sK50_skl,sK50_skl),sK50_skl) = sK50_skl ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f686,plain,
( ~ sQ31_spl
| app(sK6_skl(sK50_skl,sK50_skl),sK50_skl) = sK50_skl ),
inference(component_clause,[status(thm)],[f685]) ).
fof(f689,definition,
( sQ32_spl
<=> rearsegP(sK50_skl,sK50_skl) ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f690,plain,
( ~ sQ32_spl
| rearsegP(sK50_skl,sK50_skl) ),
inference(component_clause,[status(thm)],[f689]) ).
fof(f692,definition,
( sQ33_spl
<=> sK50_skl = sK50_skl ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f696,definition,
! [X0] :
( sQ34_spl
<=> ( rearsegP(X0,sK50_skl)
| ~ rearsegP(X0,sK50_skl)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f758,plain,
! [X0] :
( ~ ssList(nil)
| ~ ssList(nil)
| rearsegP(X0,nil)
| ~ rearsegP(X0,nil)
| ~ ssList(nil)
| ~ ssList(nil)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f524,f309]) ).
fof(f759,plain,
! [X0,X1,X2] :
( ~ ssList(X1)
| ~ rearsegP(nil,X2)
| ~ ssList(nil)
| rearsegP(X0,X2)
| ~ rearsegP(X0,X1)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f524,f309]) ).
fof(f763,plain,
! [X0,X1,X2,X3,X4] :
( ~ rearsegP(X4,X3)
| ~ rearsegP(X1,X4)
| ~ ssList(X3)
| ~ ssList(X4)
| ~ ssList(X1)
| ~ rearsegP(X3,X2)
| ~ ssList(X3)
| rearsegP(X0,X2)
| ~ rearsegP(X0,X1)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f524,f301]) ).
fof(f766,plain,
! [X0,X1,X2] :
( ~ ssList(X2)
| ~ rearsegP(X1,X2)
| ~ ssList(X2)
| rearsegP(X0,nil)
| ~ rearsegP(X0,X1)
| ~ ssList(nil)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f524,f309]) ).
fof(f777,definition,
! [X0] :
( sQ43_spl
<=> ( rearsegP(X0,nil)
| ~ rearsegP(X0,nil)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f780,plain,
( ~ sQ8_spl
| sQ43_spl ),
inference(split_clause,[status(thm)],[f758,f777,f505]) ).
fof(f781,definition,
! [X0,X1,X2] :
( sQ44_spl
<=> ( ~ ssList(X1)
| ~ rearsegP(nil,X2)
| rearsegP(X0,X2)
| ~ rearsegP(X0,X1)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition]) ).
fof(f782,plain,
! [X0,X1,X2] :
( ~ sQ44_spl
| ~ ssList(X1)
| ~ rearsegP(nil,X2)
| rearsegP(X0,X2)
| ~ rearsegP(X0,X1)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(component_clause,[status(thm)],[f781]) ).
fof(f784,plain,
( ~ sQ8_spl
| sQ44_spl ),
inference(split_clause,[status(thm)],[f759,f781,f505]) ).
fof(f786,plain,
! [X0,X1,X2,X3,X4] :
( ~ rearsegP(X4,X3)
| ~ rearsegP(X1,X4)
| ~ ssList(X4)
| ~ rearsegP(X3,X2)
| ~ ssList(X3)
| rearsegP(X0,X2)
| ~ rearsegP(X0,X1)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f763]) ).
fof(f795,definition,
! [X0,X1,X2] :
( sQ47_spl
<=> ( ~ ssList(X2)
| ~ rearsegP(X1,X2)
| ~ ssList(X2)
| rearsegP(X0,nil)
| ~ rearsegP(X0,X1)
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition]) ).
fof(f798,plain,
( ~ sQ8_spl
| sQ47_spl ),
inference(split_clause,[status(thm)],[f766,f795,f505]) ).
fof(f801,plain,
! [X0,X1,X2] :
( ~ sQ44_spl
| ~ rearsegP(nil,X2)
| rearsegP(X0,X2)
| ~ rearsegP(X0,X1)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f782]) ).
fof(f808,plain,
! [X0] :
( ~ sQ21_spl
| ~ ssList(X0)
| ~ ssList(sK6_skl(sK49_skl,sK50_skl))
| segmentP(app(app(sK6_skl(sK49_skl,sK50_skl),sK49_skl),X0),sK49_skl)
| ~ ssList(sK49_skl)
| ~ ssList(app(sK50_skl,X0)) ),
inference(paramodulation,[status(thm)],[f624,f459]) ).
fof(f810,definition,
( sQ48_spl
<=> ssList(sK6_skl(sK49_skl,sK50_skl)) ),
introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition]) ).
fof(f812,plain,
( sQ48_spl
| ~ ssList(sK6_skl(sK49_skl,sK50_skl)) ),
inference(component_clause,[status(thm)],[f810]) ).
fof(f817,definition,
! [X0] :
( sQ50_spl
<=> ( ~ ssList(X0)
| segmentP(app(app(sK6_skl(sK49_skl,sK50_skl),sK49_skl),X0),sK49_skl)
| ~ ssList(app(sK50_skl,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition]) ).
fof(f818,plain,
! [X0] :
( ~ sQ50_spl
| ~ ssList(X0)
| segmentP(app(app(sK6_skl(sK49_skl,sK50_skl),sK49_skl),X0),sK49_skl)
| ~ ssList(app(sK50_skl,X0)) ),
inference(component_clause,[status(thm)],[f817]) ).
fof(f820,plain,
( ~ sQ21_spl
| ~ sQ48_spl
| ~ sQ7_spl
| sQ50_spl ),
inference(split_clause,[status(thm)],[f808,f817,f502,f810,f623]) ).
fof(f833,plain,
( sQ48_spl
| ~ rearsegP(sK50_skl,sK49_skl)
| ~ ssList(sK49_skl)
| ~ ssList(sK50_skl) ),
inference(resolution,[status(thm)],[f812,f128]) ).
fof(f834,plain,
( sQ48_spl
| ~ sQ6_spl
| ~ sQ7_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f833,f589,f502,f449,f810]) ).
fof(f836,plain,
! [X0] :
( ~ sQ50_spl
| ~ sQ21_spl
| ~ ssList(X0)
| segmentP(app(sK50_skl,X0),sK49_skl)
| ~ ssList(app(sK50_skl,X0)) ),
inference(forward_demodulation,[status(thm)],[f624,f818]) ).
fof(f841,plain,
! [X0,X1] :
( ~ ssList(X1)
| ~ rearsegP(nil,X0)
| ~ ssList(nil)
| X0 = X1
| ~ rearsegP(X0,X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f527,f309]) ).
fof(f848,plain,
! [X0,X1] :
( ~ ssList(X1)
| ~ rearsegP(X0,X1)
| ~ ssList(X1)
| nil = X0
| ~ rearsegP(nil,X0)
| ~ ssList(X0)
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f527,f309]) ).
fof(f859,definition,
( sQ55_spl
<=> rearsegP(nil,nil) ),
introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition]) ).
fof(f860,plain,
( ~ sQ55_spl
| rearsegP(nil,nil) ),
inference(component_clause,[status(thm)],[f859]) ).
fof(f863,definition,
! [X0,X1] :
( sQ56_spl
<=> ( ~ ssList(X1)
| ~ rearsegP(nil,X0)
| X0 = X1
| ~ rearsegP(X0,X1)
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition]) ).
fof(f866,plain,
( ~ sQ8_spl
| sQ56_spl ),
inference(split_clause,[status(thm)],[f841,f863,f505]) ).
fof(f877,definition,
! [X0,X1] :
( sQ59_spl
<=> ( ~ ssList(X1)
| ~ rearsegP(X0,X1)
| ~ ssList(X1)
| nil = X0
| ~ rearsegP(nil,X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition]) ).
fof(f880,plain,
( sQ59_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f848,f505,f877]) ).
fof(f887,plain,
! [X0,X1] :
( ~ ssList(X1)
| ~ rearsegP(X0,X1)
| ~ ssList(X1)
| app(sK6_skl(nil,X0),nil) = X0
| ~ ssList(nil)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f532,f309]) ).
fof(f898,definition,
! [X0,X1] :
( sQ62_spl
<=> ( ~ ssList(X1)
| ~ rearsegP(X0,X1)
| ~ ssList(X1)
| app(sK6_skl(nil,X0),nil) = X0
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition]) ).
fof(f901,plain,
( ~ sQ8_spl
| sQ62_spl ),
inference(split_clause,[status(thm)],[f887,f898,f505]) ).
fof(f925,plain,
app(sK6_skl(sK49_skl,sK49_skl),sK49_skl) = sK49_skl,
inference(resolution,[status(thm)],[f536,f419]) ).
fof(f929,plain,
app(sK6_skl(nil,nil),nil) = nil,
inference(resolution,[status(thm)],[f536,f223]) ).
fof(f971,plain,
! [X0,X1,X2] :
( ~ ssList(X2)
| ~ rearsegP(X0,X2)
| ~ ssList(X2)
| rearsegP(app(X1,X0),nil)
| ~ ssList(X1)
| ~ ssList(nil)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f540,f309]) ).
fof(f983,definition,
! [X0,X1,X2] :
( sQ69_spl
<=> ( ~ ssList(X2)
| ~ rearsegP(X0,X2)
| ~ ssList(X2)
| rearsegP(app(X1,X0),nil)
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition]) ).
fof(f986,plain,
( ~ sQ8_spl
| sQ69_spl ),
inference(split_clause,[status(thm)],[f971,f983,f505]) ).
fof(f990,plain,
! [X0] :
( app(nil,sK5_skl(nil,X0)) = X0
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f295,f123]) ).
fof(f991,definition,
! [X0] :
( sQ70_spl
<=> ( app(nil,sK5_skl(nil,X0)) = X0
| ~ ssList(X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition]) ).
fof(f994,plain,
( ~ sQ8_spl
| sQ70_spl ),
inference(split_clause,[status(thm)],[f990,f991,f505]) ).
fof(f999,plain,
app(nil,sK49_skl) = sK49_skl,
inference(resolution,[status(thm)],[f249,f419]) ).
fof(f1003,plain,
app(nil,nil) = nil,
inference(resolution,[status(thm)],[f249,f223]) ).
fof(f1009,plain,
app(nil,sK50_skl) = sK50_skl,
inference(resolution,[status(thm)],[f249,f420]) ).
fof(f1012,plain,
( rearsegP(sK49_skl,sK49_skl)
| ~ ssList(nil)
| ~ ssList(sK49_skl) ),
inference(paramodulation,[status(thm)],[f999,f539]) ).
fof(f1013,plain,
( ~ ssList(sK49_skl)
| frontsegP(app(nil,sK49_skl),nil)
| ~ ssList(nil)
| ~ ssList(sK49_skl) ),
inference(paramodulation,[status(thm)],[f999,f457]) ).
fof(f1014,plain,
! [X0] :
( ~ ssList(X0)
| ~ ssList(nil)
| segmentP(app(app(nil,sK49_skl),X0),sK49_skl)
| ~ ssList(sK49_skl)
| ~ ssList(app(sK49_skl,X0)) ),
inference(paramodulation,[status(thm)],[f999,f459]) ).
fof(f1015,definition,
( sQ71_spl
<=> rearsegP(sK49_skl,sK49_skl) ),
introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition]) ).
fof(f1016,plain,
( ~ sQ71_spl
| rearsegP(sK49_skl,sK49_skl) ),
inference(component_clause,[status(thm)],[f1015]) ).
fof(f1018,plain,
( sQ71_spl
| ~ sQ8_spl
| ~ sQ7_spl ),
inference(split_clause,[status(thm)],[f1012,f502,f505,f1015]) ).
fof(f1019,definition,
( sQ72_spl
<=> frontsegP(app(nil,sK49_skl),nil) ),
introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition]) ).
fof(f1020,plain,
( ~ sQ72_spl
| frontsegP(app(nil,sK49_skl),nil) ),
inference(component_clause,[status(thm)],[f1019]) ).
fof(f1022,plain,
( sQ72_spl
| ~ sQ8_spl
| ~ sQ7_spl ),
inference(split_clause,[status(thm)],[f1013,f502,f505,f1019]) ).
fof(f1023,definition,
! [X0] :
( sQ73_spl
<=> ( ~ ssList(X0)
| segmentP(app(app(nil,sK49_skl),X0),sK49_skl)
| ~ ssList(app(sK49_skl,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition]) ).
fof(f1026,plain,
( ~ sQ8_spl
| ~ sQ7_spl
| sQ73_spl ),
inference(split_clause,[status(thm)],[f1014,f1023,f502,f505]) ).
fof(f1027,plain,
( ~ sQ72_spl
| frontsegP(sK49_skl,nil) ),
inference(forward_demodulation,[status(thm)],[f999,f1020]) ).
fof(f1035,plain,
! [X0,X1] :
( ~ sQ71_spl
| ~ rearsegP(X0,sK49_skl)
| ~ ssList(sK49_skl)
| rearsegP(app(X1,X0),sK49_skl)
| ~ ssList(X1)
| ~ ssList(sK49_skl)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f1016,f540]) ).
fof(f1036,plain,
! [X0] :
( ~ sQ71_spl
| ~ rearsegP(X0,sK49_skl)
| ~ ssList(sK49_skl)
| app(sK6_skl(sK49_skl,X0),sK49_skl) = X0
| ~ ssList(sK49_skl)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f1016,f532]) ).
fof(f1037,plain,
( ~ sQ71_spl
| ~ ssList(sK49_skl)
| sK49_skl = sK49_skl
| ~ rearsegP(sK49_skl,sK49_skl)
| ~ ssList(sK49_skl)
| ~ ssList(sK49_skl) ),
inference(resolution,[status(thm)],[f1016,f527]) ).
fof(f1038,plain,
! [X0] :
( ~ sQ71_spl
| ~ rearsegP(X0,sK49_skl)
| ~ ssList(sK49_skl)
| sK49_skl = X0
| ~ rearsegP(sK49_skl,X0)
| ~ ssList(X0)
| ~ ssList(sK49_skl) ),
inference(resolution,[status(thm)],[f1016,f527]) ).
fof(f1041,plain,
! [X0] :
( ~ sQ71_spl
| ~ ssList(sK49_skl)
| rearsegP(X0,sK49_skl)
| ~ rearsegP(X0,sK49_skl)
| ~ ssList(sK49_skl)
| ~ ssList(sK49_skl)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f1016,f524]) ).
fof(f1042,plain,
! [X0,X1] :
( ~ sQ71_spl
| ~ rearsegP(X1,sK49_skl)
| ~ ssList(sK49_skl)
| rearsegP(X0,sK49_skl)
| ~ rearsegP(X0,X1)
| ~ ssList(sK49_skl)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f1016,f524]) ).
fof(f1044,plain,
! [X0,X1] :
( ~ sQ71_spl
| ~ rearsegP(sK49_skl,X1)
| ~ ssList(sK49_skl)
| rearsegP(X0,X1)
| ~ rearsegP(X0,sK49_skl)
| ~ ssList(X1)
| ~ ssList(sK49_skl)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f1016,f524]) ).
fof(f1045,plain,
! [X0] :
( ~ sQ71_spl
| rearsegP(app(X0,sK49_skl),sK49_skl)
| ~ ssList(X0)
| ~ ssList(sK49_skl)
| ~ ssList(sK49_skl) ),
inference(resolution,[status(thm)],[f1016,f307]) ).
fof(f1046,plain,
( ~ sQ71_spl
| app(sK6_skl(sK49_skl,sK49_skl),sK49_skl) = sK49_skl
| ~ ssList(sK49_skl)
| ~ ssList(sK49_skl) ),
inference(resolution,[status(thm)],[f1016,f129]) ).
fof(f1049,definition,
! [X0,X1] :
( sQ74_spl
<=> ( ~ rearsegP(X0,sK49_skl)
| rearsegP(app(X1,X0),sK49_skl)
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition]) ).
fof(f1052,plain,
( ~ sQ71_spl
| ~ sQ7_spl
| sQ74_spl ),
inference(split_clause,[status(thm)],[f1035,f1049,f502,f1015]) ).
fof(f1053,definition,
! [X0] :
( sQ75_spl
<=> ( ~ rearsegP(X0,sK49_skl)
| app(sK6_skl(sK49_skl,X0),sK49_skl) = X0
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition]) ).
fof(f1056,plain,
( ~ sQ71_spl
| ~ sQ7_spl
| sQ75_spl ),
inference(split_clause,[status(thm)],[f1036,f1053,f502,f1015]) ).
fof(f1057,definition,
( sQ76_spl
<=> sK49_skl = sK49_skl ),
introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition]) ).
fof(f1060,plain,
( sQ76_spl
| ~ sQ71_spl
| ~ sQ7_spl ),
inference(split_clause,[status(thm)],[f1037,f502,f1015,f1057]) ).
fof(f1061,definition,
! [X0] :
( sQ77_spl
<=> ( ~ rearsegP(X0,sK49_skl)
| sK49_skl = X0
| ~ rearsegP(sK49_skl,X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition]) ).
fof(f1064,plain,
( ~ sQ71_spl
| sQ77_spl
| ~ sQ7_spl ),
inference(split_clause,[status(thm)],[f1038,f502,f1061,f1015]) ).
fof(f1067,definition,
! [X0] :
( sQ78_spl
<=> ( rearsegP(X0,sK49_skl)
| ~ rearsegP(X0,sK49_skl)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition]) ).
fof(f1070,plain,
( ~ sQ71_spl
| ~ sQ7_spl
| sQ78_spl ),
inference(split_clause,[status(thm)],[f1041,f1067,f502,f1015]) ).
fof(f1071,definition,
! [X0,X1] :
( sQ79_spl
<=> ( ~ rearsegP(X1,sK49_skl)
| rearsegP(X0,sK49_skl)
| ~ rearsegP(X0,X1)
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition]) ).
fof(f1074,plain,
( ~ sQ71_spl
| ~ sQ7_spl
| sQ79_spl ),
inference(split_clause,[status(thm)],[f1042,f1071,f502,f1015]) ).
fof(f1076,definition,
! [X0,X1] :
( sQ80_spl
<=> ( ~ rearsegP(sK49_skl,X1)
| rearsegP(X0,X1)
| ~ rearsegP(X0,sK49_skl)
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition]) ).
fof(f1079,plain,
( ~ sQ71_spl
| ~ sQ7_spl
| sQ80_spl ),
inference(split_clause,[status(thm)],[f1044,f1076,f502,f1015]) ).
fof(f1080,definition,
! [X0] :
( sQ81_spl
<=> ( rearsegP(app(X0,sK49_skl),sK49_skl)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition]) ).
fof(f1081,plain,
! [X0] :
( ~ sQ81_spl
| rearsegP(app(X0,sK49_skl),sK49_skl)
| ~ ssList(X0) ),
inference(component_clause,[status(thm)],[f1080]) ).
fof(f1083,plain,
( ~ sQ71_spl
| sQ81_spl
| ~ sQ7_spl ),
inference(split_clause,[status(thm)],[f1045,f502,f1080,f1015]) ).
fof(f1084,definition,
( sQ82_spl
<=> app(sK6_skl(sK49_skl,sK49_skl),sK49_skl) = sK49_skl ),
introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition]) ).
fof(f1087,plain,
( ~ sQ71_spl
| sQ82_spl
| ~ sQ7_spl ),
inference(split_clause,[status(thm)],[f1046,f502,f1084,f1015]) ).
fof(f1091,plain,
( rearsegP(sK50_skl,sK50_skl)
| ~ ssList(nil)
| ~ ssList(sK50_skl) ),
inference(paramodulation,[status(thm)],[f1009,f539]) ).
fof(f1092,plain,
( ~ ssList(sK50_skl)
| frontsegP(app(nil,sK50_skl),nil)
| ~ ssList(nil)
| ~ ssList(sK50_skl) ),
inference(paramodulation,[status(thm)],[f1009,f457]) ).
fof(f1093,plain,
! [X0] :
( ~ ssList(X0)
| ~ ssList(nil)
| segmentP(app(app(nil,sK50_skl),X0),sK50_skl)
| ~ ssList(sK50_skl)
| ~ ssList(app(sK50_skl,X0)) ),
inference(paramodulation,[status(thm)],[f1009,f459]) ).
fof(f1095,plain,
( sQ32_spl
| ~ sQ8_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f1091,f589,f505,f689]) ).
fof(f1096,definition,
( sQ83_spl
<=> frontsegP(app(nil,sK50_skl),nil) ),
introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition]) ).
fof(f1097,plain,
( ~ sQ83_spl
| frontsegP(app(nil,sK50_skl),nil) ),
inference(component_clause,[status(thm)],[f1096]) ).
fof(f1099,plain,
( sQ83_spl
| ~ sQ8_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f1092,f589,f505,f1096]) ).
fof(f1100,definition,
! [X0] :
( sQ84_spl
<=> ( ~ ssList(X0)
| segmentP(app(app(nil,sK50_skl),X0),sK50_skl)
| ~ ssList(app(sK50_skl,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition]) ).
fof(f1103,plain,
( ~ sQ8_spl
| ~ sQ15_spl
| sQ84_spl ),
inference(split_clause,[status(thm)],[f1093,f1100,f589,f505]) ).
fof(f1104,plain,
( ~ sQ83_spl
| frontsegP(sK50_skl,nil) ),
inference(forward_demodulation,[status(thm)],[f1009,f1097]) ).
fof(f1106,plain,
( ~ sQ72_spl
| app(nil,sK5_skl(nil,sK49_skl)) = sK49_skl
| ~ ssList(nil)
| ~ ssList(sK49_skl) ),
inference(resolution,[status(thm)],[f1027,f123]) ).
fof(f1107,definition,
( sQ85_spl
<=> app(nil,sK5_skl(nil,sK49_skl)) = sK49_skl ),
introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition]) ).
fof(f1108,plain,
( ~ sQ85_spl
| app(nil,sK5_skl(nil,sK49_skl)) = sK49_skl ),
inference(component_clause,[status(thm)],[f1107]) ).
fof(f1110,plain,
( ~ sQ72_spl
| sQ85_spl
| ~ sQ8_spl
| ~ sQ7_spl ),
inference(split_clause,[status(thm)],[f1106,f502,f505,f1107,f1019]) ).
fof(f1111,plain,
( ~ sQ83_spl
| app(nil,sK5_skl(nil,sK50_skl)) = sK50_skl
| ~ ssList(nil)
| ~ ssList(sK50_skl) ),
inference(resolution,[status(thm)],[f1104,f123]) ).
fof(f1112,definition,
( sQ86_spl
<=> app(nil,sK5_skl(nil,sK50_skl)) = sK50_skl ),
introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition]) ).
fof(f1113,plain,
( ~ sQ86_spl
| app(nil,sK5_skl(nil,sK50_skl)) = sK50_skl ),
inference(component_clause,[status(thm)],[f1112]) ).
fof(f1115,plain,
( ~ sQ83_spl
| sQ86_spl
| ~ sQ8_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f1111,f589,f505,f1112,f1096]) ).
fof(f1116,plain,
! [X0,X1,X2,X3] :
( ~ sQ9_spl
| ~ rearsegP(X2,app(X1,X0))
| ~ ssList(app(X1,X0))
| rearsegP(app(X3,X2),nil)
| ~ ssList(X3)
| ~ ssList(nil)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f567,f540]) ).
fof(f1117,plain,
! [X0,X1,X2] :
( ~ sQ9_spl
| ~ rearsegP(X2,app(X1,X0))
| ~ ssList(app(X1,X0))
| app(sK6_skl(nil,X2),nil) = X2
| ~ ssList(nil)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f567,f532]) ).
fof(f1118,plain,
! [X0,X1,X2] :
( ~ sQ9_spl
| ~ rearsegP(X2,app(X1,X0))
| ~ ssList(app(X1,X0))
| nil = X2
| ~ rearsegP(nil,X2)
| ~ ssList(X2)
| ~ ssList(nil)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f567,f527]) ).
fof(f1119,plain,
! [X0,X1,X2] :
( ~ sQ9_spl
| ~ rearsegP(nil,X2)
| ~ ssList(nil)
| X2 = app(X1,X0)
| ~ rearsegP(X2,app(X1,X0))
| ~ ssList(app(X1,X0))
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f567,f527]) ).
fof(f1120,plain,
! [X0,X1,X2,X3] :
( ~ sQ9_spl
| ~ rearsegP(X3,app(X1,X0))
| ~ ssList(app(X1,X0))
| rearsegP(X2,nil)
| ~ rearsegP(X2,X3)
| ~ ssList(nil)
| ~ ssList(X3)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f567,f524]) ).
fof(f1121,plain,
! [X0,X1,X2,X3] :
( ~ sQ9_spl
| ~ rearsegP(nil,X3)
| ~ ssList(nil)
| rearsegP(X2,X3)
| ~ rearsegP(X2,app(X1,X0))
| ~ ssList(X3)
| ~ ssList(app(X1,X0))
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f567,f524]) ).
fof(f1122,plain,
! [X0,X1,X2] :
( ~ sQ9_spl
| rearsegP(app(X2,app(X1,X0)),nil)
| ~ ssList(X2)
| ~ ssList(nil)
| ~ ssList(app(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f567,f307]) ).
fof(f1123,plain,
! [X0,X1] :
( ~ sQ9_spl
| app(sK6_skl(nil,app(X1,X0)),nil) = app(X1,X0)
| ~ ssList(nil)
| ~ ssList(app(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f567,f129]) ).
fof(f1124,plain,
! [X0,X1] :
( ~ sQ9_spl
| nil = app(X1,X0)
| ~ rearsegP(nil,app(X1,X0))
| ~ ssList(app(X1,X0))
| ~ ssList(nil)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f567,f303]) ).
fof(f1125,plain,
! [X0,X1,X2] :
( ~ sQ9_spl
| rearsegP(X2,nil)
| ~ rearsegP(X2,app(X1,X0))
| ~ ssList(nil)
| ~ ssList(app(X1,X0))
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f567,f301]) ).
fof(f1129,definition,
! [X0,X1,X2,X3] :
( sQ87_spl
<=> ( ~ rearsegP(X2,app(X1,X0))
| ~ ssList(app(X1,X0))
| rearsegP(app(X3,X2),nil)
| ~ ssList(X3)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition]) ).
fof(f1132,plain,
( ~ sQ9_spl
| ~ sQ8_spl
| sQ87_spl ),
inference(split_clause,[status(thm)],[f1116,f1129,f505,f551]) ).
fof(f1133,definition,
! [X0,X1,X2] :
( sQ88_spl
<=> ( ~ rearsegP(X2,app(X1,X0))
| ~ ssList(app(X1,X0))
| app(sK6_skl(nil,X2),nil) = X2
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition]) ).
fof(f1136,plain,
( ~ sQ9_spl
| ~ sQ8_spl
| sQ88_spl ),
inference(split_clause,[status(thm)],[f1117,f1133,f505,f551]) ).
fof(f1137,definition,
! [X0,X1,X2] :
( sQ89_spl
<=> ( ~ rearsegP(X2,app(X1,X0))
| ~ ssList(app(X1,X0))
| nil = X2
| ~ rearsegP(nil,X2)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition]) ).
fof(f1140,plain,
( ~ sQ9_spl
| ~ sQ8_spl
| sQ89_spl ),
inference(split_clause,[status(thm)],[f1118,f1137,f505,f551]) ).
fof(f1141,definition,
! [X0,X1,X2] :
( sQ90_spl
<=> ( ~ rearsegP(nil,X2)
| X2 = app(X1,X0)
| ~ rearsegP(X2,app(X1,X0))
| ~ ssList(app(X1,X0))
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition]) ).
fof(f1144,plain,
( ~ sQ9_spl
| ~ sQ8_spl
| sQ90_spl ),
inference(split_clause,[status(thm)],[f1119,f1141,f505,f551]) ).
fof(f1145,definition,
! [X0,X1,X2,X3] :
( sQ91_spl
<=> ( ~ rearsegP(X3,app(X1,X0))
| ~ ssList(app(X1,X0))
| rearsegP(X2,nil)
| ~ rearsegP(X2,X3)
| ~ ssList(X3)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition]) ).
fof(f1148,plain,
( ~ sQ9_spl
| ~ sQ8_spl
| sQ91_spl ),
inference(split_clause,[status(thm)],[f1120,f1145,f505,f551]) ).
fof(f1149,definition,
! [X0,X1,X2,X3] :
( sQ92_spl
<=> ( ~ rearsegP(nil,X3)
| rearsegP(X2,X3)
| ~ rearsegP(X2,app(X1,X0))
| ~ ssList(X3)
| ~ ssList(app(X1,X0))
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ92_spl])],[split_symbol_definition]) ).
fof(f1152,plain,
( ~ sQ9_spl
| ~ sQ8_spl
| sQ92_spl ),
inference(split_clause,[status(thm)],[f1121,f1149,f505,f551]) ).
fof(f1153,definition,
! [X0,X1,X2] :
( sQ93_spl
<=> ( rearsegP(app(X2,app(X1,X0)),nil)
| ~ ssList(X2)
| ~ ssList(app(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ93_spl])],[split_symbol_definition]) ).
fof(f1156,plain,
( ~ sQ9_spl
| ~ sQ8_spl
| sQ93_spl ),
inference(split_clause,[status(thm)],[f1122,f1153,f505,f551]) ).
fof(f1157,definition,
! [X0,X1] :
( sQ94_spl
<=> ( app(sK6_skl(nil,app(X1,X0)),nil) = app(X1,X0)
| ~ ssList(app(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition]) ).
fof(f1160,plain,
( ~ sQ9_spl
| ~ sQ8_spl
| sQ94_spl ),
inference(split_clause,[status(thm)],[f1123,f1157,f505,f551]) ).
fof(f1161,definition,
! [X0,X1] :
( sQ95_spl
<=> ( nil = app(X1,X0)
| ~ rearsegP(nil,app(X1,X0))
| ~ ssList(app(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ95_spl])],[split_symbol_definition]) ).
fof(f1164,plain,
( ~ sQ9_spl
| ~ sQ8_spl
| sQ95_spl ),
inference(split_clause,[status(thm)],[f1124,f1161,f505,f551]) ).
fof(f1165,definition,
! [X0,X1,X2] :
( sQ96_spl
<=> ( rearsegP(X2,nil)
| ~ rearsegP(X2,app(X1,X0))
| ~ ssList(app(X1,X0))
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition]) ).
fof(f1168,plain,
( ~ sQ9_spl
| ~ sQ8_spl
| sQ96_spl ),
inference(split_clause,[status(thm)],[f1125,f1165,f505,f551]) ).
fof(f1169,definition,
( sQ97_spl
<=> rearsegP(sK50_skl,nil) ),
introduced(definition,[new_symbols(definition,[sQ97_spl])],[split_symbol_definition]) ).
fof(f1170,plain,
( ~ sQ97_spl
| rearsegP(sK50_skl,nil) ),
inference(component_clause,[status(thm)],[f1169]) ).
fof(f1173,definition,
( sQ98_spl
<=> rearsegP(sK49_skl,nil) ),
introduced(definition,[new_symbols(definition,[sQ98_spl])],[split_symbol_definition]) ).
fof(f1174,plain,
( ~ sQ98_spl
| rearsegP(sK49_skl,nil) ),
inference(component_clause,[status(thm)],[f1173]) ).
fof(f1196,plain,
! [X0,X1] :
( ~ sQ32_spl
| ~ rearsegP(X0,sK50_skl)
| ~ ssList(sK50_skl)
| rearsegP(app(X1,X0),sK50_skl)
| ~ ssList(X1)
| ~ ssList(sK50_skl)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f690,f540]) ).
fof(f1197,plain,
! [X0] :
( ~ sQ32_spl
| ~ rearsegP(X0,sK50_skl)
| ~ ssList(sK50_skl)
| app(sK6_skl(sK50_skl,X0),sK50_skl) = X0
| ~ ssList(sK50_skl)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f690,f532]) ).
fof(f1198,plain,
( ~ sQ32_spl
| ~ ssList(sK50_skl)
| sK50_skl = sK50_skl
| ~ rearsegP(sK50_skl,sK50_skl)
| ~ ssList(sK50_skl)
| ~ ssList(sK50_skl) ),
inference(resolution,[status(thm)],[f690,f527]) ).
fof(f1199,plain,
! [X0] :
( ~ sQ32_spl
| ~ rearsegP(X0,sK50_skl)
| ~ ssList(sK50_skl)
| sK50_skl = X0
| ~ rearsegP(sK50_skl,X0)
| ~ ssList(X0)
| ~ ssList(sK50_skl) ),
inference(resolution,[status(thm)],[f690,f527]) ).
fof(f1202,plain,
! [X0] :
( ~ sQ32_spl
| ~ ssList(sK50_skl)
| rearsegP(X0,sK50_skl)
| ~ rearsegP(X0,sK50_skl)
| ~ ssList(sK50_skl)
| ~ ssList(sK50_skl)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f690,f524]) ).
fof(f1203,plain,
! [X0,X1] :
( ~ sQ32_spl
| ~ rearsegP(X1,sK50_skl)
| ~ ssList(sK50_skl)
| rearsegP(X0,sK50_skl)
| ~ rearsegP(X0,X1)
| ~ ssList(sK50_skl)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f690,f524]) ).
fof(f1205,plain,
! [X0,X1] :
( ~ sQ32_spl
| ~ rearsegP(sK50_skl,X1)
| ~ ssList(sK50_skl)
| rearsegP(X0,X1)
| ~ rearsegP(X0,sK50_skl)
| ~ ssList(X1)
| ~ ssList(sK50_skl)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f690,f524]) ).
fof(f1206,plain,
! [X0] :
( ~ sQ32_spl
| rearsegP(app(X0,sK50_skl),sK50_skl)
| ~ ssList(X0)
| ~ ssList(sK50_skl)
| ~ ssList(sK50_skl) ),
inference(resolution,[status(thm)],[f690,f307]) ).
fof(f1207,plain,
( ~ sQ32_spl
| app(sK6_skl(sK50_skl,sK50_skl),sK50_skl) = sK50_skl
| ~ ssList(sK50_skl)
| ~ ssList(sK50_skl) ),
inference(resolution,[status(thm)],[f690,f129]) ).
fof(f1212,definition,
! [X0,X1] :
( sQ99_spl
<=> ( ~ rearsegP(X0,sK50_skl)
| rearsegP(app(X1,X0),sK50_skl)
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ99_spl])],[split_symbol_definition]) ).
fof(f1215,plain,
( ~ sQ32_spl
| ~ sQ15_spl
| sQ99_spl ),
inference(split_clause,[status(thm)],[f1196,f1212,f589,f689]) ).
fof(f1216,definition,
! [X0] :
( sQ100_spl
<=> ( ~ rearsegP(X0,sK50_skl)
| app(sK6_skl(sK50_skl,X0),sK50_skl) = X0
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ100_spl])],[split_symbol_definition]) ).
fof(f1219,plain,
( ~ sQ32_spl
| ~ sQ15_spl
| sQ100_spl ),
inference(split_clause,[status(thm)],[f1197,f1216,f589,f689]) ).
fof(f1220,plain,
( sQ33_spl
| ~ sQ32_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f1198,f589,f689,f692]) ).
fof(f1221,definition,
! [X0] :
( sQ101_spl
<=> ( ~ rearsegP(X0,sK50_skl)
| sK50_skl = X0
| ~ rearsegP(sK50_skl,X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ101_spl])],[split_symbol_definition]) ).
fof(f1224,plain,
( ~ sQ32_spl
| sQ101_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f1199,f589,f1221,f689]) ).
fof(f1227,plain,
( ~ sQ32_spl
| ~ sQ15_spl
| sQ34_spl ),
inference(split_clause,[status(thm)],[f1202,f696,f589,f689]) ).
fof(f1228,definition,
! [X0,X1] :
( sQ102_spl
<=> ( ~ rearsegP(X1,sK50_skl)
| rearsegP(X0,sK50_skl)
| ~ rearsegP(X0,X1)
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ102_spl])],[split_symbol_definition]) ).
fof(f1231,plain,
( ~ sQ32_spl
| ~ sQ15_spl
| sQ102_spl ),
inference(split_clause,[status(thm)],[f1203,f1228,f589,f689]) ).
fof(f1233,definition,
! [X0,X1] :
( sQ103_spl
<=> ( ~ rearsegP(sK50_skl,X1)
| rearsegP(X0,X1)
| ~ rearsegP(X0,sK50_skl)
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ103_spl])],[split_symbol_definition]) ).
fof(f1236,plain,
( ~ sQ32_spl
| ~ sQ15_spl
| sQ103_spl ),
inference(split_clause,[status(thm)],[f1205,f1233,f589,f689]) ).
fof(f1237,plain,
( ~ sQ32_spl
| sQ30_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f1206,f589,f681,f689]) ).
fof(f1238,plain,
( ~ sQ32_spl
| sQ31_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f1207,f589,f685,f689]) ).
fof(f1241,plain,
! [X0,X1] :
( ~ sQ97_spl
| ~ rearsegP(X0,sK50_skl)
| ~ ssList(sK50_skl)
| rearsegP(app(X1,X0),nil)
| ~ ssList(X1)
| ~ ssList(nil)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f1170,f540]) ).
fof(f1242,plain,
! [X0] :
( ~ sQ97_spl
| ~ rearsegP(X0,sK50_skl)
| ~ ssList(sK50_skl)
| app(sK6_skl(nil,X0),nil) = X0
| ~ ssList(nil)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f1170,f532]) ).
fof(f1243,plain,
! [X0] :
( ~ sQ97_spl
| ~ rearsegP(X0,sK50_skl)
| ~ ssList(sK50_skl)
| nil = X0
| ~ rearsegP(nil,X0)
| ~ ssList(X0)
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f1170,f527]) ).
fof(f1244,plain,
! [X0] :
( ~ sQ97_spl
| ~ rearsegP(nil,X0)
| ~ ssList(nil)
| X0 = sK50_skl
| ~ rearsegP(X0,sK50_skl)
| ~ ssList(sK50_skl)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f1170,f527]) ).
fof(f1245,plain,
! [X0,X1] :
( ~ sQ97_spl
| ~ rearsegP(X1,sK50_skl)
| ~ ssList(sK50_skl)
| rearsegP(X0,nil)
| ~ rearsegP(X0,X1)
| ~ ssList(nil)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f1170,f524]) ).
fof(f1246,plain,
! [X0,X1] :
( ~ sQ97_spl
| ~ rearsegP(nil,X1)
| ~ ssList(nil)
| rearsegP(X0,X1)
| ~ rearsegP(X0,sK50_skl)
| ~ ssList(X1)
| ~ ssList(sK50_skl)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f1170,f524]) ).
fof(f1247,plain,
! [X0] :
( ~ sQ97_spl
| rearsegP(app(X0,sK50_skl),nil)
| ~ ssList(X0)
| ~ ssList(nil)
| ~ ssList(sK50_skl) ),
inference(resolution,[status(thm)],[f1170,f307]) ).
fof(f1248,plain,
( ~ sQ97_spl
| app(sK6_skl(nil,sK50_skl),nil) = sK50_skl
| ~ ssList(nil)
| ~ ssList(sK50_skl) ),
inference(resolution,[status(thm)],[f1170,f129]) ).
fof(f1250,plain,
! [X0] :
( ~ sQ97_spl
| rearsegP(X0,nil)
| ~ rearsegP(X0,sK50_skl)
| ~ ssList(nil)
| ~ ssList(sK50_skl)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f1170,f301]) ).
fof(f1251,definition,
! [X0,X1] :
( sQ104_spl
<=> ( ~ rearsegP(X0,sK50_skl)
| rearsegP(app(X1,X0),nil)
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ104_spl])],[split_symbol_definition]) ).
fof(f1254,plain,
( ~ sQ97_spl
| ~ sQ15_spl
| ~ sQ8_spl
| sQ104_spl ),
inference(split_clause,[status(thm)],[f1241,f1251,f505,f589,f1169]) ).
fof(f1255,definition,
! [X0] :
( sQ105_spl
<=> ( ~ rearsegP(X0,sK50_skl)
| app(sK6_skl(nil,X0),nil) = X0
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ105_spl])],[split_symbol_definition]) ).
fof(f1258,plain,
( ~ sQ97_spl
| ~ sQ15_spl
| ~ sQ8_spl
| sQ105_spl ),
inference(split_clause,[status(thm)],[f1242,f1255,f505,f589,f1169]) ).
fof(f1259,definition,
! [X0] :
( sQ106_spl
<=> ( ~ rearsegP(X0,sK50_skl)
| nil = X0
| ~ rearsegP(nil,X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ106_spl])],[split_symbol_definition]) ).
fof(f1262,plain,
( ~ sQ97_spl
| ~ sQ15_spl
| sQ106_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f1243,f505,f1259,f589,f1169]) ).
fof(f1263,definition,
! [X0] :
( sQ107_spl
<=> ( ~ rearsegP(nil,X0)
| X0 = sK50_skl
| ~ rearsegP(X0,sK50_skl)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ107_spl])],[split_symbol_definition]) ).
fof(f1266,plain,
( ~ sQ97_spl
| ~ sQ8_spl
| ~ sQ15_spl
| sQ107_spl ),
inference(split_clause,[status(thm)],[f1244,f1263,f589,f505,f1169]) ).
fof(f1267,definition,
! [X0,X1] :
( sQ108_spl
<=> ( ~ rearsegP(X1,sK50_skl)
| rearsegP(X0,nil)
| ~ rearsegP(X0,X1)
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ108_spl])],[split_symbol_definition]) ).
fof(f1270,plain,
( ~ sQ97_spl
| ~ sQ15_spl
| ~ sQ8_spl
| sQ108_spl ),
inference(split_clause,[status(thm)],[f1245,f1267,f505,f589,f1169]) ).
fof(f1271,definition,
! [X0,X1] :
( sQ109_spl
<=> ( ~ rearsegP(nil,X1)
| rearsegP(X0,X1)
| ~ rearsegP(X0,sK50_skl)
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ109_spl])],[split_symbol_definition]) ).
fof(f1274,plain,
( ~ sQ97_spl
| ~ sQ8_spl
| ~ sQ15_spl
| sQ109_spl ),
inference(split_clause,[status(thm)],[f1246,f1271,f589,f505,f1169]) ).
fof(f1275,definition,
! [X0] :
( sQ110_spl
<=> ( rearsegP(app(X0,sK50_skl),nil)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ110_spl])],[split_symbol_definition]) ).
fof(f1278,plain,
( ~ sQ97_spl
| sQ110_spl
| ~ sQ8_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f1247,f589,f505,f1275,f1169]) ).
fof(f1279,definition,
( sQ111_spl
<=> app(sK6_skl(nil,sK50_skl),nil) = sK50_skl ),
introduced(definition,[new_symbols(definition,[sQ111_spl])],[split_symbol_definition]) ).
fof(f1282,plain,
( ~ sQ97_spl
| sQ111_spl
| ~ sQ8_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f1248,f589,f505,f1279,f1169]) ).
fof(f1287,definition,
! [X0] :
( sQ113_spl
<=> ( rearsegP(X0,nil)
| ~ rearsegP(X0,sK50_skl)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ113_spl])],[split_symbol_definition]) ).
fof(f1290,plain,
( ~ sQ97_spl
| ~ sQ8_spl
| ~ sQ15_spl
| sQ113_spl ),
inference(split_clause,[status(thm)],[f1250,f1287,f589,f505,f1169]) ).
fof(f1291,plain,
! [X0,X1] :
( ~ sQ98_spl
| ~ rearsegP(X0,sK49_skl)
| ~ ssList(sK49_skl)
| rearsegP(app(X1,X0),nil)
| ~ ssList(X1)
| ~ ssList(nil)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f1174,f540]) ).
fof(f1292,plain,
! [X0] :
( ~ sQ98_spl
| ~ rearsegP(X0,sK49_skl)
| ~ ssList(sK49_skl)
| app(sK6_skl(nil,X0),nil) = X0
| ~ ssList(nil)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f1174,f532]) ).
fof(f1293,plain,
! [X0] :
( ~ sQ98_spl
| ~ rearsegP(X0,sK49_skl)
| ~ ssList(sK49_skl)
| nil = X0
| ~ rearsegP(nil,X0)
| ~ ssList(X0)
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f1174,f527]) ).
fof(f1294,plain,
! [X0] :
( ~ sQ98_spl
| ~ rearsegP(nil,X0)
| ~ ssList(nil)
| X0 = sK49_skl
| ~ rearsegP(X0,sK49_skl)
| ~ ssList(sK49_skl)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f1174,f527]) ).
fof(f1295,plain,
! [X0,X1] :
( ~ sQ98_spl
| ~ rearsegP(X1,sK49_skl)
| ~ ssList(sK49_skl)
| rearsegP(X0,nil)
| ~ rearsegP(X0,X1)
| ~ ssList(nil)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f1174,f524]) ).
fof(f1296,plain,
! [X0,X1] :
( ~ sQ98_spl
| ~ rearsegP(nil,X1)
| ~ ssList(nil)
| rearsegP(X0,X1)
| ~ rearsegP(X0,sK49_skl)
| ~ ssList(X1)
| ~ ssList(sK49_skl)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f1174,f524]) ).
fof(f1297,plain,
! [X0] :
( ~ sQ98_spl
| rearsegP(app(X0,sK49_skl),nil)
| ~ ssList(X0)
| ~ ssList(nil)
| ~ ssList(sK49_skl) ),
inference(resolution,[status(thm)],[f1174,f307]) ).
fof(f1298,plain,
( ~ sQ98_spl
| app(sK6_skl(nil,sK49_skl),nil) = sK49_skl
| ~ ssList(nil)
| ~ ssList(sK49_skl) ),
inference(resolution,[status(thm)],[f1174,f129]) ).
fof(f1300,plain,
! [X0] :
( ~ sQ98_spl
| rearsegP(X0,nil)
| ~ rearsegP(X0,sK49_skl)
| ~ ssList(nil)
| ~ ssList(sK49_skl)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f1174,f301]) ).
fof(f1301,definition,
! [X0,X1] :
( sQ114_spl
<=> ( ~ rearsegP(X0,sK49_skl)
| rearsegP(app(X1,X0),nil)
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ114_spl])],[split_symbol_definition]) ).
fof(f1304,plain,
( ~ sQ98_spl
| ~ sQ7_spl
| ~ sQ8_spl
| sQ114_spl ),
inference(split_clause,[status(thm)],[f1291,f1301,f505,f502,f1173]) ).
fof(f1305,definition,
! [X0] :
( sQ115_spl
<=> ( ~ rearsegP(X0,sK49_skl)
| app(sK6_skl(nil,X0),nil) = X0
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ115_spl])],[split_symbol_definition]) ).
fof(f1308,plain,
( ~ sQ98_spl
| ~ sQ7_spl
| ~ sQ8_spl
| sQ115_spl ),
inference(split_clause,[status(thm)],[f1292,f1305,f505,f502,f1173]) ).
fof(f1309,definition,
! [X0] :
( sQ116_spl
<=> ( ~ rearsegP(X0,sK49_skl)
| nil = X0
| ~ rearsegP(nil,X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ116_spl])],[split_symbol_definition]) ).
fof(f1312,plain,
( ~ sQ98_spl
| ~ sQ7_spl
| sQ116_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f1293,f505,f1309,f502,f1173]) ).
fof(f1313,definition,
! [X0] :
( sQ117_spl
<=> ( ~ rearsegP(nil,X0)
| X0 = sK49_skl
| ~ rearsegP(X0,sK49_skl)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ117_spl])],[split_symbol_definition]) ).
fof(f1316,plain,
( ~ sQ98_spl
| ~ sQ8_spl
| ~ sQ7_spl
| sQ117_spl ),
inference(split_clause,[status(thm)],[f1294,f1313,f502,f505,f1173]) ).
fof(f1317,definition,
! [X0,X1] :
( sQ118_spl
<=> ( ~ rearsegP(X1,sK49_skl)
| rearsegP(X0,nil)
| ~ rearsegP(X0,X1)
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ118_spl])],[split_symbol_definition]) ).
fof(f1320,plain,
( ~ sQ98_spl
| ~ sQ7_spl
| ~ sQ8_spl
| sQ118_spl ),
inference(split_clause,[status(thm)],[f1295,f1317,f505,f502,f1173]) ).
fof(f1321,definition,
! [X0,X1] :
( sQ119_spl
<=> ( ~ rearsegP(nil,X1)
| rearsegP(X0,X1)
| ~ rearsegP(X0,sK49_skl)
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ119_spl])],[split_symbol_definition]) ).
fof(f1324,plain,
( ~ sQ98_spl
| ~ sQ8_spl
| ~ sQ7_spl
| sQ119_spl ),
inference(split_clause,[status(thm)],[f1296,f1321,f502,f505,f1173]) ).
fof(f1325,definition,
! [X0] :
( sQ120_spl
<=> ( rearsegP(app(X0,sK49_skl),nil)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ120_spl])],[split_symbol_definition]) ).
fof(f1328,plain,
( ~ sQ98_spl
| sQ120_spl
| ~ sQ8_spl
| ~ sQ7_spl ),
inference(split_clause,[status(thm)],[f1297,f502,f505,f1325,f1173]) ).
fof(f1329,definition,
( sQ121_spl
<=> app(sK6_skl(nil,sK49_skl),nil) = sK49_skl ),
introduced(definition,[new_symbols(definition,[sQ121_spl])],[split_symbol_definition]) ).
fof(f1332,plain,
( ~ sQ98_spl
| sQ121_spl
| ~ sQ8_spl
| ~ sQ7_spl ),
inference(split_clause,[status(thm)],[f1298,f502,f505,f1329,f1173]) ).
fof(f1337,definition,
! [X0] :
( sQ123_spl
<=> ( rearsegP(X0,nil)
| ~ rearsegP(X0,sK49_skl)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ123_spl])],[split_symbol_definition]) ).
fof(f1340,plain,
( ~ sQ98_spl
| ~ sQ8_spl
| ~ sQ7_spl
| sQ123_spl ),
inference(split_clause,[status(thm)],[f1300,f1337,f502,f505,f1173]) ).
fof(f1350,plain,
! [X0,X1,X2] :
( ~ sQ30_spl
| ~ rearsegP(X1,app(X0,sK50_skl))
| ~ ssList(app(X0,sK50_skl))
| rearsegP(app(X2,X1),sK50_skl)
| ~ ssList(X2)
| ~ ssList(sK50_skl)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f682,f540]) ).
fof(f1351,plain,
! [X0,X1] :
( ~ sQ30_spl
| ~ rearsegP(X1,app(X0,sK50_skl))
| ~ ssList(app(X0,sK50_skl))
| app(sK6_skl(sK50_skl,X1),sK50_skl) = X1
| ~ ssList(sK50_skl)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f682,f532]) ).
fof(f1352,plain,
! [X0,X1] :
( ~ sQ30_spl
| ~ rearsegP(X1,app(X0,sK50_skl))
| ~ ssList(app(X0,sK50_skl))
| sK50_skl = X1
| ~ rearsegP(sK50_skl,X1)
| ~ ssList(X1)
| ~ ssList(sK50_skl)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f682,f527]) ).
fof(f1353,plain,
! [X0,X1] :
( ~ sQ30_spl
| ~ rearsegP(sK50_skl,X1)
| ~ ssList(sK50_skl)
| X1 = app(X0,sK50_skl)
| ~ rearsegP(X1,app(X0,sK50_skl))
| ~ ssList(app(X0,sK50_skl))
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f682,f527]) ).
fof(f1354,plain,
! [X0,X1,X2] :
( ~ sQ30_spl
| ~ rearsegP(X2,app(X0,sK50_skl))
| ~ ssList(app(X0,sK50_skl))
| rearsegP(X1,sK50_skl)
| ~ rearsegP(X1,X2)
| ~ ssList(sK50_skl)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f682,f524]) ).
fof(f1355,plain,
! [X0,X1,X2] :
( ~ sQ30_spl
| ~ rearsegP(sK50_skl,X2)
| ~ ssList(sK50_skl)
| rearsegP(X1,X2)
| ~ rearsegP(X1,app(X0,sK50_skl))
| ~ ssList(X2)
| ~ ssList(app(X0,sK50_skl))
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f682,f524]) ).
fof(f1356,plain,
! [X0,X1] :
( ~ sQ30_spl
| rearsegP(app(X1,app(X0,sK50_skl)),sK50_skl)
| ~ ssList(X1)
| ~ ssList(sK50_skl)
| ~ ssList(app(X0,sK50_skl))
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f682,f307]) ).
fof(f1357,plain,
! [X0] :
( ~ sQ30_spl
| app(sK6_skl(sK50_skl,app(X0,sK50_skl)),sK50_skl) = app(X0,sK50_skl)
| ~ ssList(sK50_skl)
| ~ ssList(app(X0,sK50_skl))
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f682,f129]) ).
fof(f1358,plain,
! [X0] :
( ~ sQ30_spl
| sK50_skl = app(X0,sK50_skl)
| ~ rearsegP(sK50_skl,app(X0,sK50_skl))
| ~ ssList(app(X0,sK50_skl))
| ~ ssList(sK50_skl)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f682,f303]) ).
fof(f1359,plain,
! [X0,X1] :
( ~ sQ30_spl
| rearsegP(X1,sK50_skl)
| ~ rearsegP(X1,app(X0,sK50_skl))
| ~ ssList(sK50_skl)
| ~ ssList(app(X0,sK50_skl))
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f682,f301]) ).
fof(f1361,definition,
! [X0,X1,X2] :
( sQ125_spl
<=> ( ~ rearsegP(X1,app(X0,sK50_skl))
| ~ ssList(app(X0,sK50_skl))
| rearsegP(app(X2,X1),sK50_skl)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ125_spl])],[split_symbol_definition]) ).
fof(f1364,plain,
( ~ sQ30_spl
| ~ sQ15_spl
| sQ125_spl ),
inference(split_clause,[status(thm)],[f1350,f1361,f589,f681]) ).
fof(f1365,definition,
! [X0,X1] :
( sQ126_spl
<=> ( ~ rearsegP(X1,app(X0,sK50_skl))
| ~ ssList(app(X0,sK50_skl))
| app(sK6_skl(sK50_skl,X1),sK50_skl) = X1
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ126_spl])],[split_symbol_definition]) ).
fof(f1368,plain,
( ~ sQ30_spl
| ~ sQ15_spl
| sQ126_spl ),
inference(split_clause,[status(thm)],[f1351,f1365,f589,f681]) ).
fof(f1369,definition,
! [X0,X1] :
( sQ127_spl
<=> ( ~ rearsegP(X1,app(X0,sK50_skl))
| ~ ssList(app(X0,sK50_skl))
| sK50_skl = X1
| ~ rearsegP(sK50_skl,X1)
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ127_spl])],[split_symbol_definition]) ).
fof(f1372,plain,
( ~ sQ30_spl
| ~ sQ15_spl
| sQ127_spl ),
inference(split_clause,[status(thm)],[f1352,f1369,f589,f681]) ).
fof(f1373,definition,
! [X0,X1] :
( sQ128_spl
<=> ( ~ rearsegP(sK50_skl,X1)
| X1 = app(X0,sK50_skl)
| ~ rearsegP(X1,app(X0,sK50_skl))
| ~ ssList(app(X0,sK50_skl))
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ128_spl])],[split_symbol_definition]) ).
fof(f1376,plain,
( ~ sQ30_spl
| ~ sQ15_spl
| sQ128_spl ),
inference(split_clause,[status(thm)],[f1353,f1373,f589,f681]) ).
fof(f1377,definition,
! [X0,X1,X2] :
( sQ129_spl
<=> ( ~ rearsegP(X2,app(X0,sK50_skl))
| ~ ssList(app(X0,sK50_skl))
| rearsegP(X1,sK50_skl)
| ~ rearsegP(X1,X2)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ129_spl])],[split_symbol_definition]) ).
fof(f1380,plain,
( ~ sQ30_spl
| ~ sQ15_spl
| sQ129_spl ),
inference(split_clause,[status(thm)],[f1354,f1377,f589,f681]) ).
fof(f1381,definition,
! [X0,X1,X2] :
( sQ130_spl
<=> ( ~ rearsegP(sK50_skl,X2)
| rearsegP(X1,X2)
| ~ rearsegP(X1,app(X0,sK50_skl))
| ~ ssList(X2)
| ~ ssList(app(X0,sK50_skl))
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ130_spl])],[split_symbol_definition]) ).
fof(f1384,plain,
( ~ sQ30_spl
| ~ sQ15_spl
| sQ130_spl ),
inference(split_clause,[status(thm)],[f1355,f1381,f589,f681]) ).
fof(f1385,definition,
! [X0,X1] :
( sQ131_spl
<=> ( rearsegP(app(X1,app(X0,sK50_skl)),sK50_skl)
| ~ ssList(X1)
| ~ ssList(app(X0,sK50_skl))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ131_spl])],[split_symbol_definition]) ).
fof(f1388,plain,
( ~ sQ30_spl
| ~ sQ15_spl
| sQ131_spl ),
inference(split_clause,[status(thm)],[f1356,f1385,f589,f681]) ).
fof(f1389,definition,
! [X0] :
( sQ132_spl
<=> ( app(sK6_skl(sK50_skl,app(X0,sK50_skl)),sK50_skl) = app(X0,sK50_skl)
| ~ ssList(app(X0,sK50_skl))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ132_spl])],[split_symbol_definition]) ).
fof(f1392,plain,
( ~ sQ30_spl
| ~ sQ15_spl
| sQ132_spl ),
inference(split_clause,[status(thm)],[f1357,f1389,f589,f681]) ).
fof(f1393,definition,
! [X0] :
( sQ133_spl
<=> ( sK50_skl = app(X0,sK50_skl)
| ~ rearsegP(sK50_skl,app(X0,sK50_skl))
| ~ ssList(app(X0,sK50_skl))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ133_spl])],[split_symbol_definition]) ).
fof(f1396,plain,
( ~ sQ30_spl
| ~ sQ15_spl
| sQ133_spl ),
inference(split_clause,[status(thm)],[f1358,f1393,f589,f681]) ).
fof(f1397,definition,
! [X0,X1] :
( sQ134_spl
<=> ( rearsegP(X1,sK50_skl)
| ~ rearsegP(X1,app(X0,sK50_skl))
| ~ ssList(app(X0,sK50_skl))
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ134_spl])],[split_symbol_definition]) ).
fof(f1400,plain,
( ~ sQ30_spl
| ~ sQ15_spl
| sQ134_spl ),
inference(split_clause,[status(thm)],[f1359,f1397,f589,f681]) ).
fof(f1408,plain,
( rearsegP(nil,nil)
| ~ ssList(nil)
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f1003,f539]) ).
fof(f1409,plain,
( ~ ssList(nil)
| frontsegP(app(nil,nil),nil)
| ~ ssList(nil)
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f1003,f457]) ).
fof(f1410,plain,
! [X0] :
( ~ ssList(X0)
| ~ ssList(nil)
| segmentP(app(app(nil,nil),X0),nil)
| ~ ssList(nil)
| ~ ssList(app(nil,X0)) ),
inference(paramodulation,[status(thm)],[f1003,f459]) ).
fof(f1412,plain,
( sQ55_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f1408,f505,f859]) ).
fof(f1413,definition,
( sQ136_spl
<=> frontsegP(app(nil,nil),nil) ),
introduced(definition,[new_symbols(definition,[sQ136_spl])],[split_symbol_definition]) ).
fof(f1414,plain,
( ~ sQ136_spl
| frontsegP(app(nil,nil),nil) ),
inference(component_clause,[status(thm)],[f1413]) ).
fof(f1416,plain,
( sQ136_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f1409,f505,f1413]) ).
fof(f1417,definition,
! [X0] :
( sQ137_spl
<=> ( ~ ssList(X0)
| segmentP(app(app(nil,nil),X0),nil)
| ~ ssList(app(nil,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ137_spl])],[split_symbol_definition]) ).
fof(f1420,plain,
( ~ sQ8_spl
| sQ137_spl ),
inference(split_clause,[status(thm)],[f1410,f1417,f505]) ).
fof(f1421,plain,
( ~ sQ136_spl
| frontsegP(nil,nil) ),
inference(forward_demodulation,[status(thm)],[f1003,f1414]) ).
fof(f1423,plain,
! [X0] :
( ~ sQ14_spl
| ~ ssList(nil)
| ~ rearsegP(nil,X0)
| ~ ssList(nil)
| nil = X0
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f583,f309]) ).
fof(f1425,plain,
! [X0,X1,X2] :
( ~ sQ14_spl
| ~ rearsegP(X2,X1)
| ~ rearsegP(nil,X2)
| ~ ssList(X1)
| ~ ssList(X2)
| ~ ssList(nil)
| ~ rearsegP(X1,X0)
| ~ ssList(X1)
| nil = X0
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f583,f301]) ).
fof(f1426,definition,
! [X0] :
( sQ138_spl
<=> ( ~ rearsegP(nil,X0)
| nil = X0
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ138_spl])],[split_symbol_definition]) ).
fof(f1429,plain,
( ~ sQ14_spl
| ~ sQ8_spl
| sQ138_spl ),
inference(split_clause,[status(thm)],[f1423,f1426,f505,f579]) ).
fof(f1431,definition,
! [X0,X1,X2] :
( sQ139_spl
<=> ( ~ rearsegP(X2,X1)
| ~ rearsegP(nil,X2)
| ~ ssList(X1)
| ~ ssList(X2)
| ~ rearsegP(X1,X0)
| ~ ssList(X1)
| nil = X0
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ139_spl])],[split_symbol_definition]) ).
fof(f1434,plain,
( ~ sQ14_spl
| ~ sQ8_spl
| sQ139_spl ),
inference(split_clause,[status(thm)],[f1425,f1431,f505,f579]) ).
fof(f1454,plain,
! [X0,X1] :
( ~ sQ55_spl
| ~ rearsegP(X0,nil)
| ~ ssList(nil)
| rearsegP(app(X1,X0),nil)
| ~ ssList(X1)
| ~ ssList(nil)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f860,f540]) ).
fof(f1455,plain,
! [X0] :
( ~ sQ55_spl
| ~ rearsegP(X0,nil)
| ~ ssList(nil)
| app(sK6_skl(nil,X0),nil) = X0
| ~ ssList(nil)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f860,f532]) ).
fof(f1457,plain,
! [X0] :
( ~ sQ55_spl
| ~ rearsegP(X0,nil)
| ~ ssList(nil)
| nil = X0
| ~ rearsegP(nil,X0)
| ~ ssList(X0)
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f860,f527]) ).
fof(f1461,plain,
! [X0,X1] :
( ~ sQ55_spl
| ~ rearsegP(X1,nil)
| ~ ssList(nil)
| rearsegP(X0,nil)
| ~ rearsegP(X0,X1)
| ~ ssList(nil)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f860,f524]) ).
fof(f1464,plain,
! [X0] :
( ~ sQ55_spl
| rearsegP(app(X0,nil),nil)
| ~ ssList(X0)
| ~ ssList(nil)
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f860,f307]) ).
fof(f1465,plain,
( ~ sQ55_spl
| app(sK6_skl(nil,nil),nil) = nil
| ~ ssList(nil)
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f860,f129]) ).
fof(f1470,definition,
! [X0,X1] :
( sQ140_spl
<=> ( ~ rearsegP(X0,nil)
| rearsegP(app(X1,X0),nil)
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ140_spl])],[split_symbol_definition]) ).
fof(f1473,plain,
( ~ sQ55_spl
| ~ sQ8_spl
| sQ140_spl ),
inference(split_clause,[status(thm)],[f1454,f1470,f505,f859]) ).
fof(f1474,definition,
! [X0] :
( sQ141_spl
<=> ( ~ rearsegP(X0,nil)
| app(sK6_skl(nil,X0),nil) = X0
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ141_spl])],[split_symbol_definition]) ).
fof(f1477,plain,
( ~ sQ55_spl
| ~ sQ8_spl
| sQ141_spl ),
inference(split_clause,[status(thm)],[f1455,f1474,f505,f859]) ).
fof(f1479,definition,
! [X0] :
( sQ142_spl
<=> ( ~ rearsegP(X0,nil)
| nil = X0
| ~ rearsegP(nil,X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ142_spl])],[split_symbol_definition]) ).
fof(f1482,plain,
( ~ sQ55_spl
| sQ142_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f1457,f505,f1479,f859]) ).
fof(f1486,definition,
! [X0,X1] :
( sQ143_spl
<=> ( ~ rearsegP(X1,nil)
| rearsegP(X0,nil)
| ~ rearsegP(X0,X1)
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ143_spl])],[split_symbol_definition]) ).
fof(f1489,plain,
( ~ sQ55_spl
| ~ sQ8_spl
| sQ143_spl ),
inference(split_clause,[status(thm)],[f1461,f1486,f505,f859]) ).
fof(f1491,definition,
! [X0,X1] :
( sQ144_spl
<=> ( ~ rearsegP(nil,X1)
| rearsegP(X0,X1)
| ~ rearsegP(X0,nil)
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ144_spl])],[split_symbol_definition]) ).
fof(f1495,definition,
! [X0] :
( sQ145_spl
<=> ( rearsegP(app(X0,nil),nil)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ145_spl])],[split_symbol_definition]) ).
fof(f1498,plain,
( ~ sQ55_spl
| sQ145_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f1464,f505,f1495,f859]) ).
fof(f1499,definition,
( sQ146_spl
<=> app(sK6_skl(nil,nil),nil) = nil ),
introduced(definition,[new_symbols(definition,[sQ146_spl])],[split_symbol_definition]) ).
fof(f1502,plain,
( ~ sQ55_spl
| sQ146_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f1465,f505,f1499,f859]) ).
fof(f1506,plain,
( ~ sQ136_spl
| app(nil,sK5_skl(nil,nil)) = nil
| ~ ssList(nil)
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f1421,f123]) ).
fof(f1507,definition,
( sQ147_spl
<=> app(nil,sK5_skl(nil,nil)) = nil ),
introduced(definition,[new_symbols(definition,[sQ147_spl])],[split_symbol_definition]) ).
fof(f1510,plain,
( ~ sQ136_spl
| sQ147_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f1506,f505,f1507,f1413]) ).
fof(f1514,plain,
app(sK49_skl,nil) = sK49_skl,
inference(resolution,[status(thm)],[f389,f419]) ).
fof(f1524,plain,
app(sK50_skl,nil) = sK50_skl,
inference(resolution,[status(thm)],[f389,f420]) ).
fof(f1533,plain,
( ~ ssList(nil)
| frontsegP(app(sK49_skl,nil),sK49_skl)
| ~ ssList(sK49_skl)
| ~ ssList(sK49_skl) ),
inference(paramodulation,[status(thm)],[f1514,f457]) ).
fof(f1534,plain,
! [X0] :
( ~ ssList(X0)
| ~ ssList(sK49_skl)
| segmentP(app(app(sK49_skl,nil),X0),nil)
| ~ ssList(nil)
| ~ ssList(app(sK49_skl,X0)) ),
inference(paramodulation,[status(thm)],[f1514,f459]) ).
fof(f1537,definition,
( sQ148_spl
<=> frontsegP(app(sK49_skl,nil),sK49_skl) ),
introduced(definition,[new_symbols(definition,[sQ148_spl])],[split_symbol_definition]) ).
fof(f1538,plain,
( ~ sQ148_spl
| frontsegP(app(sK49_skl,nil),sK49_skl) ),
inference(component_clause,[status(thm)],[f1537]) ).
fof(f1540,plain,
( ~ sQ8_spl
| sQ148_spl
| ~ sQ7_spl ),
inference(split_clause,[status(thm)],[f1533,f502,f1537,f505]) ).
fof(f1541,definition,
! [X0] :
( sQ149_spl
<=> ( ~ ssList(X0)
| segmentP(app(app(sK49_skl,nil),X0),nil)
| ~ ssList(app(sK49_skl,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ149_spl])],[split_symbol_definition]) ).
fof(f1544,plain,
( ~ sQ7_spl
| ~ sQ8_spl
| sQ149_spl ),
inference(split_clause,[status(thm)],[f1534,f1541,f505,f502]) ).
fof(f1545,plain,
( ~ sQ148_spl
| frontsegP(sK49_skl,sK49_skl) ),
inference(forward_demodulation,[status(thm)],[f1514,f1538]) ).
fof(f1549,plain,
( ~ sQ31_spl
| ~ sQ9_spl
| rearsegP(sK50_skl,nil)
| ~ ssList(sK6_skl(sK50_skl,sK50_skl))
| ~ ssList(sK50_skl) ),
inference(paramodulation,[status(thm)],[f686,f567]) ).
fof(f1551,plain,
( ~ sQ31_spl
| ~ ssList(sK50_skl)
| frontsegP(app(sK6_skl(sK50_skl,sK50_skl),sK50_skl),sK6_skl(sK50_skl,sK50_skl))
| ~ ssList(sK6_skl(sK50_skl,sK50_skl))
| ~ ssList(sK50_skl) ),
inference(paramodulation,[status(thm)],[f686,f457]) ).
fof(f1552,plain,
! [X0] :
( ~ sQ31_spl
| ~ ssList(X0)
| ~ ssList(sK6_skl(sK50_skl,sK50_skl))
| segmentP(app(app(sK6_skl(sK50_skl,sK50_skl),sK50_skl),X0),sK50_skl)
| ~ ssList(sK50_skl)
| ~ ssList(app(sK50_skl,X0)) ),
inference(paramodulation,[status(thm)],[f686,f459]) ).
fof(f1553,definition,
( sQ150_spl
<=> ssList(sK6_skl(sK50_skl,sK50_skl)) ),
introduced(definition,[new_symbols(definition,[sQ150_spl])],[split_symbol_definition]) ).
fof(f1555,plain,
( sQ150_spl
| ~ ssList(sK6_skl(sK50_skl,sK50_skl)) ),
inference(component_clause,[status(thm)],[f1553]) ).
fof(f1558,plain,
( ~ sQ31_spl
| ~ sQ9_spl
| sQ97_spl
| ~ sQ150_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f1549,f589,f1553,f1169,f551,f685]) ).
fof(f1560,definition,
( sQ151_spl
<=> frontsegP(app(sK6_skl(sK50_skl,sK50_skl),sK50_skl),sK6_skl(sK50_skl,sK50_skl)) ),
introduced(definition,[new_symbols(definition,[sQ151_spl])],[split_symbol_definition]) ).
fof(f1561,plain,
( ~ sQ151_spl
| frontsegP(app(sK6_skl(sK50_skl,sK50_skl),sK50_skl),sK6_skl(sK50_skl,sK50_skl)) ),
inference(component_clause,[status(thm)],[f1560]) ).
fof(f1563,plain,
( ~ sQ31_spl
| sQ151_spl
| ~ sQ150_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f1551,f589,f1553,f1560,f685]) ).
fof(f1564,definition,
! [X0] :
( sQ152_spl
<=> ( ~ ssList(X0)
| segmentP(app(app(sK6_skl(sK50_skl,sK50_skl),sK50_skl),X0),sK50_skl)
| ~ ssList(app(sK50_skl,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ152_spl])],[split_symbol_definition]) ).
fof(f1567,plain,
( ~ sQ31_spl
| ~ sQ150_spl
| ~ sQ15_spl
| sQ152_spl ),
inference(split_clause,[status(thm)],[f1552,f1564,f589,f1553,f685]) ).
fof(f1568,plain,
( ~ sQ148_spl
| app(sK49_skl,sK5_skl(sK49_skl,sK49_skl)) = sK49_skl
| ~ ssList(sK49_skl)
| ~ ssList(sK49_skl) ),
inference(resolution,[status(thm)],[f1545,f123]) ).
fof(f1569,definition,
( sQ153_spl
<=> app(sK49_skl,sK5_skl(sK49_skl,sK49_skl)) = sK49_skl ),
introduced(definition,[new_symbols(definition,[sQ153_spl])],[split_symbol_definition]) ).
fof(f1572,plain,
( ~ sQ148_spl
| sQ153_spl
| ~ sQ7_spl ),
inference(split_clause,[status(thm)],[f1568,f502,f1569,f1537]) ).
fof(f1575,plain,
( ~ ssList(nil)
| frontsegP(app(sK50_skl,nil),sK50_skl)
| ~ ssList(sK50_skl)
| ~ ssList(sK50_skl) ),
inference(paramodulation,[status(thm)],[f1524,f457]) ).
fof(f1576,plain,
! [X0] :
( ~ ssList(X0)
| ~ ssList(sK50_skl)
| segmentP(app(app(sK50_skl,nil),X0),nil)
| ~ ssList(nil)
| ~ ssList(app(sK50_skl,X0)) ),
inference(paramodulation,[status(thm)],[f1524,f459]) ).
fof(f1579,definition,
( sQ154_spl
<=> frontsegP(app(sK50_skl,nil),sK50_skl) ),
introduced(definition,[new_symbols(definition,[sQ154_spl])],[split_symbol_definition]) ).
fof(f1580,plain,
( ~ sQ154_spl
| frontsegP(app(sK50_skl,nil),sK50_skl) ),
inference(component_clause,[status(thm)],[f1579]) ).
fof(f1582,plain,
( ~ sQ8_spl
| sQ154_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f1575,f589,f1579,f505]) ).
fof(f1583,definition,
! [X0] :
( sQ155_spl
<=> ( ~ ssList(X0)
| segmentP(app(app(sK50_skl,nil),X0),nil)
| ~ ssList(app(sK50_skl,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ155_spl])],[split_symbol_definition]) ).
fof(f1586,plain,
( ~ sQ15_spl
| ~ sQ8_spl
| sQ155_spl ),
inference(split_clause,[status(thm)],[f1576,f1583,f505,f589]) ).
fof(f1587,plain,
( ~ sQ154_spl
| frontsegP(sK50_skl,sK50_skl) ),
inference(forward_demodulation,[status(thm)],[f1524,f1580]) ).
fof(f1595,plain,
! [X0] :
( segmentP(app(nil,X0),nil)
| ~ ssList(X0)
| ~ ssList(nil)
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f1003,f652]) ).
fof(f1598,plain,
! [X0] :
( ~ sQ31_spl
| segmentP(app(sK50_skl,X0),sK50_skl)
| ~ ssList(X0)
| ~ ssList(sK6_skl(sK50_skl,sK50_skl))
| ~ ssList(sK50_skl) ),
inference(paramodulation,[status(thm)],[f686,f652]) ).
fof(f1604,definition,
! [X0] :
( sQ156_spl
<=> ( segmentP(app(sK50_skl,X0),nil)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ156_spl])],[split_symbol_definition]) ).
fof(f1608,definition,
! [X0] :
( sQ157_spl
<=> ( segmentP(app(sK49_skl,X0),nil)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ157_spl])],[split_symbol_definition]) ).
fof(f1612,definition,
! [X0] :
( sQ158_spl
<=> ( segmentP(app(nil,X0),nil)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ158_spl])],[split_symbol_definition]) ).
fof(f1615,plain,
( sQ158_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f1595,f505,f1612]) ).
fof(f1616,definition,
! [X0] :
( sQ159_spl
<=> ( segmentP(app(sK50_skl,X0),sK50_skl)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ159_spl])],[split_symbol_definition]) ).
fof(f1620,definition,
! [X0] :
( sQ160_spl
<=> ( segmentP(app(sK49_skl,X0),sK49_skl)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ160_spl])],[split_symbol_definition]) ).
fof(f1624,plain,
( ~ sQ31_spl
| sQ159_spl
| ~ sQ150_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f1598,f589,f1553,f1616,f685]) ).
fof(f1629,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ26_spl
| segmentP(app(app(X3,app(app(X1,X0),X2)),X4),nil)
| ~ ssList(X4)
| ~ ssList(X3)
| ~ ssList(nil)
| ~ ssList(app(app(X1,X0),X2))
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f673,f321]) ).
fof(f1630,plain,
! [X0,X1,X2] :
( ~ sQ26_spl
| nil = app(app(X1,X0),X2)
| ~ segmentP(nil,app(app(X1,X0),X2))
| ~ ssList(app(app(X1,X0),X2))
| ~ ssList(nil)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f673,f317]) ).
fof(f1631,plain,
! [X0,X1,X2,X3] :
( ~ sQ26_spl
| segmentP(X3,nil)
| ~ segmentP(X3,app(app(X1,X0),X2))
| ~ ssList(nil)
| ~ ssList(app(app(X1,X0),X2))
| ~ ssList(X3)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f673,f315]) ).
fof(f1632,plain,
! [X0,X1,X2] :
( ~ sQ26_spl
| app(app(sK7_skl(nil,app(app(X1,X0),X2)),nil),sK8_skl(nil,app(app(X1,X0),X2))) = app(app(X1,X0),X2)
| ~ ssList(nil)
| ~ ssList(app(app(X1,X0),X2))
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f673,f136]) ).
fof(f1638,plain,
! [X0] :
( ~ sQ31_spl
| ~ sQ26_spl
| segmentP(app(sK50_skl,X0),nil)
| ~ ssList(X0)
| ~ ssList(sK6_skl(sK50_skl,sK50_skl))
| ~ ssList(sK50_skl) ),
inference(paramodulation,[status(thm)],[f686,f673]) ).
fof(f1640,definition,
! [X0,X1,X2,X3,X4] :
( sQ162_spl
<=> ( segmentP(app(app(X3,app(app(X1,X0),X2)),X4),nil)
| ~ ssList(X4)
| ~ ssList(X3)
| ~ ssList(app(app(X1,X0),X2))
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ162_spl])],[split_symbol_definition]) ).
fof(f1643,plain,
( ~ sQ26_spl
| ~ sQ8_spl
| sQ162_spl ),
inference(split_clause,[status(thm)],[f1629,f1640,f505,f657]) ).
fof(f1644,definition,
! [X0,X1,X2] :
( sQ163_spl
<=> ( nil = app(app(X1,X0),X2)
| ~ segmentP(nil,app(app(X1,X0),X2))
| ~ ssList(app(app(X1,X0),X2))
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ163_spl])],[split_symbol_definition]) ).
fof(f1647,plain,
( ~ sQ26_spl
| ~ sQ8_spl
| sQ163_spl ),
inference(split_clause,[status(thm)],[f1630,f1644,f505,f657]) ).
fof(f1648,definition,
! [X0,X1,X2,X3] :
( sQ164_spl
<=> ( segmentP(X3,nil)
| ~ segmentP(X3,app(app(X1,X0),X2))
| ~ ssList(app(app(X1,X0),X2))
| ~ ssList(X3)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ164_spl])],[split_symbol_definition]) ).
fof(f1651,plain,
( ~ sQ26_spl
| ~ sQ8_spl
| sQ164_spl ),
inference(split_clause,[status(thm)],[f1631,f1648,f505,f657]) ).
fof(f1652,definition,
! [X0,X1,X2] :
( sQ165_spl
<=> ( app(app(sK7_skl(nil,app(app(X1,X0),X2)),nil),sK8_skl(nil,app(app(X1,X0),X2))) = app(app(X1,X0),X2)
| ~ ssList(app(app(X1,X0),X2))
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ165_spl])],[split_symbol_definition]) ).
fof(f1655,plain,
( ~ sQ26_spl
| ~ sQ8_spl
| sQ165_spl ),
inference(split_clause,[status(thm)],[f1632,f1652,f505,f657]) ).
fof(f1661,plain,
( ~ sQ31_spl
| ~ sQ26_spl
| sQ156_spl
| ~ sQ150_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f1638,f589,f1553,f1604,f657,f685]) ).
fof(f1663,plain,
( ~ sQ154_spl
| app(sK50_skl,sK5_skl(sK50_skl,sK50_skl)) = sK50_skl
| ~ ssList(sK50_skl)
| ~ ssList(sK50_skl) ),
inference(resolution,[status(thm)],[f1587,f123]) ).
fof(f1664,definition,
( sQ166_spl
<=> app(sK50_skl,sK5_skl(sK50_skl,sK50_skl)) = sK50_skl ),
introduced(definition,[new_symbols(definition,[sQ166_spl])],[split_symbol_definition]) ).
fof(f1667,plain,
( ~ sQ154_spl
| sQ166_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f1663,f589,f1664,f1579]) ).
fof(f1668,plain,
( sQ150_spl
| ~ rearsegP(sK50_skl,sK50_skl)
| ~ ssList(sK50_skl)
| ~ ssList(sK50_skl) ),
inference(resolution,[status(thm)],[f1555,f128]) ).
fof(f1669,plain,
( sQ150_spl
| ~ sQ32_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f1668,f589,f689,f1553]) ).
fof(f1670,plain,
( ~ sQ151_spl
| ~ sQ31_spl
| frontsegP(sK50_skl,sK6_skl(sK50_skl,sK50_skl)) ),
inference(forward_demodulation,[status(thm)],[f686,f1561]) ).
fof(f1683,plain,
( ~ sQ151_spl
| ~ sQ31_spl
| app(sK6_skl(sK50_skl,sK50_skl),sK5_skl(sK6_skl(sK50_skl,sK50_skl),sK50_skl)) = sK50_skl
| ~ ssList(sK6_skl(sK50_skl,sK50_skl))
| ~ ssList(sK50_skl) ),
inference(resolution,[status(thm)],[f1670,f123]) ).
fof(f1684,definition,
( sQ167_spl
<=> app(sK6_skl(sK50_skl,sK50_skl),sK5_skl(sK6_skl(sK50_skl,sK50_skl),sK50_skl)) = sK50_skl ),
introduced(definition,[new_symbols(definition,[sQ167_spl])],[split_symbol_definition]) ).
fof(f1687,plain,
( ~ sQ151_spl
| ~ sQ31_spl
| sQ167_spl
| ~ sQ150_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f1683,f589,f1553,f1684,f685,f1560]) ).
fof(f1700,plain,
! [X0] :
( ~ sQ26_spl
| segmentP(app(sK49_skl,X0),nil)
| ~ ssList(X0)
| ~ ssList(sK6_skl(sK49_skl,sK49_skl))
| ~ ssList(sK49_skl) ),
inference(paramodulation,[status(thm)],[f925,f673]) ).
fof(f1701,plain,
! [X0] :
( segmentP(app(sK49_skl,X0),sK49_skl)
| ~ ssList(X0)
| ~ ssList(sK6_skl(sK49_skl,sK49_skl))
| ~ ssList(sK49_skl) ),
inference(paramodulation,[status(thm)],[f925,f652]) ).
fof(f1702,plain,
( ~ sQ9_spl
| rearsegP(sK49_skl,nil)
| ~ ssList(sK6_skl(sK49_skl,sK49_skl))
| ~ ssList(sK49_skl) ),
inference(paramodulation,[status(thm)],[f925,f567]) ).
fof(f1704,plain,
( ~ ssList(sK49_skl)
| frontsegP(app(sK6_skl(sK49_skl,sK49_skl),sK49_skl),sK6_skl(sK49_skl,sK49_skl))
| ~ ssList(sK6_skl(sK49_skl,sK49_skl))
| ~ ssList(sK49_skl) ),
inference(paramodulation,[status(thm)],[f925,f457]) ).
fof(f1705,definition,
( sQ170_spl
<=> ssList(sK6_skl(sK49_skl,sK49_skl)) ),
introduced(definition,[new_symbols(definition,[sQ170_spl])],[split_symbol_definition]) ).
fof(f1707,plain,
( sQ170_spl
| ~ ssList(sK6_skl(sK49_skl,sK49_skl)) ),
inference(component_clause,[status(thm)],[f1705]) ).
fof(f1708,plain,
( ~ sQ26_spl
| sQ157_spl
| ~ sQ170_spl
| ~ sQ7_spl ),
inference(split_clause,[status(thm)],[f1700,f502,f1705,f1608,f657]) ).
fof(f1709,plain,
( sQ160_spl
| ~ sQ170_spl
| ~ sQ7_spl ),
inference(split_clause,[status(thm)],[f1701,f502,f1705,f1620]) ).
fof(f1710,plain,
( ~ sQ9_spl
| sQ98_spl
| ~ sQ170_spl
| ~ sQ7_spl ),
inference(split_clause,[status(thm)],[f1702,f502,f1705,f1173,f551]) ).
fof(f1712,definition,
( sQ171_spl
<=> frontsegP(app(sK6_skl(sK49_skl,sK49_skl),sK49_skl),sK6_skl(sK49_skl,sK49_skl)) ),
introduced(definition,[new_symbols(definition,[sQ171_spl])],[split_symbol_definition]) ).
fof(f1713,plain,
( ~ sQ171_spl
| frontsegP(app(sK6_skl(sK49_skl,sK49_skl),sK49_skl),sK6_skl(sK49_skl,sK49_skl)) ),
inference(component_clause,[status(thm)],[f1712]) ).
fof(f1715,plain,
( sQ171_spl
| ~ sQ170_spl
| ~ sQ7_spl ),
inference(split_clause,[status(thm)],[f1704,f502,f1705,f1712]) ).
fof(f1747,plain,
( sQ170_spl
| ~ rearsegP(sK49_skl,sK49_skl)
| ~ ssList(sK49_skl)
| ~ ssList(sK49_skl) ),
inference(resolution,[status(thm)],[f1707,f128]) ).
fof(f1748,plain,
( sQ170_spl
| ~ sQ71_spl
| ~ sQ7_spl ),
inference(split_clause,[status(thm)],[f1747,f502,f1015,f1705]) ).
fof(f1749,plain,
( ~ sQ171_spl
| frontsegP(sK49_skl,sK6_skl(sK49_skl,sK49_skl)) ),
inference(forward_demodulation,[status(thm)],[f925,f1713]) ).
fof(f1758,plain,
( ~ sQ171_spl
| app(sK6_skl(sK49_skl,sK49_skl),sK5_skl(sK6_skl(sK49_skl,sK49_skl),sK49_skl)) = sK49_skl
| ~ ssList(sK6_skl(sK49_skl,sK49_skl))
| ~ ssList(sK49_skl) ),
inference(resolution,[status(thm)],[f1749,f123]) ).
fof(f1759,definition,
( sQ174_spl
<=> app(sK6_skl(sK49_skl,sK49_skl),sK5_skl(sK6_skl(sK49_skl,sK49_skl),sK49_skl)) = sK49_skl ),
introduced(definition,[new_symbols(definition,[sQ174_spl])],[split_symbol_definition]) ).
fof(f1762,plain,
( ~ sQ171_spl
| sQ174_spl
| ~ sQ170_spl
| ~ sQ7_spl ),
inference(split_clause,[status(thm)],[f1758,f502,f1705,f1759,f1712]) ).
fof(f1785,plain,
( ~ ssList(nil)
| frontsegP(app(sK6_skl(nil,nil),nil),sK6_skl(nil,nil))
| ~ ssList(sK6_skl(nil,nil))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f929,f457]) ).
fof(f1786,definition,
( sQ179_spl
<=> ssList(sK6_skl(nil,nil)) ),
introduced(definition,[new_symbols(definition,[sQ179_spl])],[split_symbol_definition]) ).
fof(f1788,plain,
( sQ179_spl
| ~ ssList(sK6_skl(nil,nil)) ),
inference(component_clause,[status(thm)],[f1786]) ).
fof(f1793,definition,
( sQ180_spl
<=> frontsegP(app(sK6_skl(nil,nil),nil),sK6_skl(nil,nil)) ),
introduced(definition,[new_symbols(definition,[sQ180_spl])],[split_symbol_definition]) ).
fof(f1796,plain,
( sQ180_spl
| ~ sQ179_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f1785,f505,f1786,f1793]) ).
fof(f1797,plain,
( sQ179_spl
| ~ rearsegP(nil,nil)
| ~ ssList(nil)
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f1788,f128]) ).
fof(f1798,plain,
( sQ179_spl
| ~ sQ55_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f1797,f505,f859,f1786]) ).
fof(f1813,plain,
! [X0,X1,X2] :
( ~ sQ55_spl
| ~ rearsegP(X2,nil)
| ~ rearsegP(X1,X2)
| ~ ssList(X2)
| ~ ssList(nil)
| rearsegP(X0,nil)
| ~ rearsegP(X0,X1)
| ~ ssList(nil)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f786,f860]) ).
fof(f1815,plain,
! [X0,X1,X2] :
( ~ sQ98_spl
| ~ rearsegP(X2,sK49_skl)
| ~ rearsegP(X1,X2)
| ~ ssList(X2)
| ~ ssList(sK49_skl)
| rearsegP(X0,nil)
| ~ rearsegP(X0,X1)
| ~ ssList(nil)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f786,f1174]) ).
fof(f1817,plain,
! [X0,X1,X2] :
( ~ sQ71_spl
| ~ rearsegP(X2,sK49_skl)
| ~ rearsegP(X1,X2)
| ~ ssList(X2)
| ~ ssList(sK49_skl)
| rearsegP(X0,sK49_skl)
| ~ rearsegP(X0,X1)
| ~ ssList(sK49_skl)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f786,f1016]) ).
fof(f1818,plain,
! [X0,X1] :
( ~ sQ30_spl
| ~ ssList(X1)
| ~ rearsegP(sK50_skl,app(X1,sK50_skl))
| ~ ssList(sK50_skl)
| ~ ssList(app(X1,sK50_skl))
| rearsegP(X0,sK50_skl)
| ~ rearsegP(X0,app(X1,sK50_skl))
| ~ ssList(sK50_skl)
| ~ ssList(app(X1,sK50_skl))
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f786,f682]) ).
fof(f1819,plain,
! [X0,X1,X2,X3] :
( ~ sQ30_spl
| ~ ssList(X2)
| ~ rearsegP(X3,app(X2,sK50_skl))
| ~ rearsegP(X1,X3)
| ~ ssList(X3)
| ~ ssList(app(X2,sK50_skl))
| rearsegP(X0,sK50_skl)
| ~ rearsegP(X0,X1)
| ~ ssList(sK50_skl)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f786,f682]) ).
fof(f1822,plain,
! [X0,X1,X2] :
( ~ sQ9_spl
| ~ ssList(X1)
| ~ ssList(X2)
| ~ rearsegP(nil,app(X1,X2))
| ~ ssList(nil)
| ~ ssList(app(X1,X2))
| rearsegP(X0,nil)
| ~ rearsegP(X0,app(X1,X2))
| ~ ssList(nil)
| ~ ssList(app(X1,X2))
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f786,f567]) ).
fof(f1823,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ9_spl
| ~ ssList(X2)
| ~ ssList(X3)
| ~ rearsegP(X4,app(X2,X3))
| ~ rearsegP(X1,X4)
| ~ ssList(X4)
| ~ ssList(app(X2,X3))
| rearsegP(X0,nil)
| ~ rearsegP(X0,X1)
| ~ ssList(nil)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f786,f567]) ).
fof(f1827,plain,
! [X0,X1,X2] :
( ~ sQ97_spl
| ~ rearsegP(X2,sK50_skl)
| ~ rearsegP(X1,X2)
| ~ ssList(X2)
| ~ ssList(sK50_skl)
| rearsegP(X0,nil)
| ~ rearsegP(X0,X1)
| ~ ssList(nil)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f786,f1170]) ).
fof(f1829,plain,
! [X0,X1,X2] :
( ~ sQ32_spl
| ~ rearsegP(X2,sK50_skl)
| ~ rearsegP(X1,X2)
| ~ ssList(X2)
| ~ ssList(sK50_skl)
| rearsegP(X0,sK50_skl)
| ~ rearsegP(X0,X1)
| ~ ssList(sK50_skl)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f786,f690]) ).
fof(f1833,plain,
! [X0,X1,X2,X3] :
( ~ ssList(X2)
| ~ rearsegP(X3,X2)
| ~ rearsegP(X1,X3)
| ~ ssList(X3)
| ~ ssList(X2)
| rearsegP(X0,nil)
| ~ rearsegP(X0,X1)
| ~ ssList(nil)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f786,f309]) ).
fof(f1839,plain,
! [X0,X1,X2] :
( ~ sQ55_spl
| ~ rearsegP(nil,X2)
| ~ ssList(nil)
| ~ rearsegP(X2,X1)
| ~ ssList(X2)
| rearsegP(X0,X1)
| ~ rearsegP(X0,nil)
| ~ ssList(X1)
| ~ ssList(nil)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f786,f860]) ).
fof(f1840,plain,
! [X0,X1,X2] :
( ~ sQ98_spl
| ~ rearsegP(nil,X2)
| ~ ssList(nil)
| ~ rearsegP(X2,X1)
| ~ ssList(X2)
| rearsegP(X0,X1)
| ~ rearsegP(X0,sK49_skl)
| ~ ssList(X1)
| ~ ssList(sK49_skl)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f786,f1174]) ).
fof(f1842,plain,
! [X0,X1,X2] :
( ~ sQ71_spl
| ~ rearsegP(sK49_skl,X2)
| ~ ssList(sK49_skl)
| ~ rearsegP(X2,X1)
| ~ ssList(X2)
| rearsegP(X0,X1)
| ~ rearsegP(X0,sK49_skl)
| ~ ssList(X1)
| ~ ssList(sK49_skl)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f786,f1016]) ).
fof(f1843,plain,
! [X0,X1,X2,X3] :
( ~ sQ30_spl
| ~ ssList(X1)
| ~ rearsegP(sK50_skl,X3)
| ~ ssList(sK50_skl)
| ~ rearsegP(X3,X2)
| ~ ssList(X3)
| rearsegP(X0,X2)
| ~ rearsegP(X0,app(X1,sK50_skl))
| ~ ssList(X2)
| ~ ssList(app(X1,sK50_skl))
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f786,f682]) ).
fof(f1845,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ9_spl
| ~ ssList(X1)
| ~ ssList(X2)
| ~ rearsegP(nil,X4)
| ~ ssList(nil)
| ~ rearsegP(X4,X3)
| ~ ssList(X4)
| rearsegP(X0,X3)
| ~ rearsegP(X0,app(X1,X2))
| ~ ssList(X3)
| ~ ssList(app(X1,X2))
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f786,f567]) ).
fof(f1847,plain,
! [X0,X1,X2] :
( ~ sQ97_spl
| ~ rearsegP(nil,X2)
| ~ ssList(nil)
| ~ rearsegP(X2,X1)
| ~ ssList(X2)
| rearsegP(X0,X1)
| ~ rearsegP(X0,sK50_skl)
| ~ ssList(X1)
| ~ ssList(sK50_skl)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f786,f1170]) ).
fof(f1849,plain,
! [X0,X1,X2] :
( ~ sQ32_spl
| ~ rearsegP(sK50_skl,X2)
| ~ ssList(sK50_skl)
| ~ rearsegP(X2,X1)
| ~ ssList(X2)
| rearsegP(X0,X1)
| ~ rearsegP(X0,sK50_skl)
| ~ ssList(X1)
| ~ ssList(sK50_skl)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f786,f690]) ).
fof(f1851,plain,
! [X0,X1] :
( ~ ssList(nil)
| ~ ssList(nil)
| ~ rearsegP(nil,X1)
| ~ ssList(nil)
| rearsegP(X0,X1)
| ~ rearsegP(X0,nil)
| ~ ssList(X1)
| ~ ssList(nil)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f786,f309]) ).
fof(f1852,plain,
! [X0,X1,X2,X3] :
( ~ ssList(X1)
| ~ rearsegP(nil,X3)
| ~ ssList(nil)
| ~ rearsegP(X3,X2)
| ~ ssList(X3)
| rearsegP(X0,X2)
| ~ rearsegP(X0,X1)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f786,f309]) ).
fof(f1857,plain,
! [X0,X1,X2] :
( ~ sQ55_spl
| ~ rearsegP(X1,nil)
| ~ ssList(nil)
| ~ rearsegP(nil,X2)
| ~ ssList(nil)
| rearsegP(X0,X2)
| ~ rearsegP(X0,X1)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f786,f860]) ).
fof(f1858,plain,
! [X0,X1,X2] :
( ~ sQ98_spl
| ~ rearsegP(X1,sK49_skl)
| ~ ssList(sK49_skl)
| ~ rearsegP(nil,X2)
| ~ ssList(nil)
| rearsegP(X0,X2)
| ~ rearsegP(X0,X1)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f786,f1174]) ).
fof(f1859,plain,
! [X0,X1,X2] :
( ~ sQ71_spl
| ~ rearsegP(X1,sK49_skl)
| ~ ssList(sK49_skl)
| ~ rearsegP(sK49_skl,X2)
| ~ ssList(sK49_skl)
| rearsegP(X0,X2)
| ~ rearsegP(X0,X1)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f786,f1016]) ).
fof(f1860,plain,
! [X0,X1,X2,X3] :
( ~ sQ30_spl
| ~ ssList(X3)
| ~ rearsegP(X1,app(X3,sK50_skl))
| ~ ssList(app(X3,sK50_skl))
| ~ rearsegP(sK50_skl,X2)
| ~ ssList(sK50_skl)
| rearsegP(X0,X2)
| ~ rearsegP(X0,X1)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f786,f682]) ).
fof(f1862,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ9_spl
| ~ ssList(X3)
| ~ ssList(X4)
| ~ rearsegP(X1,app(X3,X4))
| ~ ssList(app(X3,X4))
| ~ rearsegP(nil,X2)
| ~ ssList(nil)
| rearsegP(X0,X2)
| ~ rearsegP(X0,X1)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f786,f567]) ).
fof(f1864,plain,
! [X0,X1,X2] :
( ~ sQ97_spl
| ~ rearsegP(X1,sK50_skl)
| ~ ssList(sK50_skl)
| ~ rearsegP(nil,X2)
| ~ ssList(nil)
| rearsegP(X0,X2)
| ~ rearsegP(X0,X1)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f786,f1170]) ).
fof(f1865,plain,
! [X0,X1,X2] :
( ~ sQ32_spl
| ~ rearsegP(X1,sK50_skl)
| ~ ssList(sK50_skl)
| ~ rearsegP(sK50_skl,X2)
| ~ ssList(sK50_skl)
| rearsegP(X0,X2)
| ~ rearsegP(X0,X1)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f786,f690]) ).
fof(f1867,plain,
! [X0,X1,X2,X3] :
( ~ ssList(X3)
| ~ rearsegP(X1,X3)
| ~ ssList(X3)
| ~ rearsegP(nil,X2)
| ~ ssList(nil)
| rearsegP(X0,X2)
| ~ rearsegP(X0,X1)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f786,f309]) ).
fof(f1871,definition,
! [X0,X1,X2] :
( sQ183_spl
<=> ( ~ rearsegP(X2,nil)
| ~ rearsegP(X1,X2)
| ~ ssList(X2)
| rearsegP(X0,nil)
| ~ rearsegP(X0,X1)
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ183_spl])],[split_symbol_definition]) ).
fof(f1874,plain,
( ~ sQ55_spl
| ~ sQ8_spl
| sQ183_spl ),
inference(split_clause,[status(thm)],[f1813,f1871,f505,f859]) ).
fof(f1876,definition,
! [X0,X1,X2] :
( sQ184_spl
<=> ( ~ rearsegP(X2,sK49_skl)
| ~ rearsegP(X1,X2)
| ~ ssList(X2)
| rearsegP(X0,nil)
| ~ rearsegP(X0,X1)
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ184_spl])],[split_symbol_definition]) ).
fof(f1879,plain,
( ~ sQ98_spl
| ~ sQ7_spl
| ~ sQ8_spl
| sQ184_spl ),
inference(split_clause,[status(thm)],[f1815,f1876,f505,f502,f1173]) ).
fof(f1881,definition,
! [X0,X1,X2] :
( sQ185_spl
<=> ( ~ rearsegP(X2,sK49_skl)
| ~ rearsegP(X1,X2)
| ~ ssList(X2)
| rearsegP(X0,sK49_skl)
| ~ rearsegP(X0,X1)
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ185_spl])],[split_symbol_definition]) ).
fof(f1884,plain,
( ~ sQ71_spl
| ~ sQ7_spl
| sQ185_spl ),
inference(split_clause,[status(thm)],[f1817,f1881,f502,f1015]) ).
fof(f1885,definition,
! [X0,X1] :
( sQ186_spl
<=> ( ~ ssList(X1)
| ~ rearsegP(sK50_skl,app(X1,sK50_skl))
| ~ ssList(app(X1,sK50_skl))
| rearsegP(X0,sK50_skl)
| ~ rearsegP(X0,app(X1,sK50_skl))
| ~ ssList(app(X1,sK50_skl))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ186_spl])],[split_symbol_definition]) ).
fof(f1888,plain,
( ~ sQ30_spl
| ~ sQ15_spl
| sQ186_spl ),
inference(split_clause,[status(thm)],[f1818,f1885,f589,f681]) ).
fof(f1889,definition,
! [X0,X1,X2,X3] :
( sQ187_spl
<=> ( ~ ssList(X2)
| ~ rearsegP(X3,app(X2,sK50_skl))
| ~ rearsegP(X1,X3)
| ~ ssList(X3)
| ~ ssList(app(X2,sK50_skl))
| rearsegP(X0,sK50_skl)
| ~ rearsegP(X0,X1)
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ187_spl])],[split_symbol_definition]) ).
fof(f1892,plain,
( ~ sQ30_spl
| ~ sQ15_spl
| sQ187_spl ),
inference(split_clause,[status(thm)],[f1819,f1889,f589,f681]) ).
fof(f1901,definition,
! [X0,X1,X2] :
( sQ190_spl
<=> ( ~ ssList(X1)
| ~ ssList(X2)
| ~ rearsegP(nil,app(X1,X2))
| ~ ssList(app(X1,X2))
| rearsegP(X0,nil)
| ~ rearsegP(X0,app(X1,X2))
| ~ ssList(app(X1,X2))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ190_spl])],[split_symbol_definition]) ).
fof(f1904,plain,
( ~ sQ9_spl
| ~ sQ8_spl
| sQ190_spl ),
inference(split_clause,[status(thm)],[f1822,f1901,f505,f551]) ).
fof(f1905,definition,
! [X0,X1,X2,X3,X4] :
( sQ191_spl
<=> ( ~ ssList(X2)
| ~ ssList(X3)
| ~ rearsegP(X4,app(X2,X3))
| ~ rearsegP(X1,X4)
| ~ ssList(X4)
| ~ ssList(app(X2,X3))
| rearsegP(X0,nil)
| ~ rearsegP(X0,X1)
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ191_spl])],[split_symbol_definition]) ).
fof(f1908,plain,
( ~ sQ9_spl
| ~ sQ8_spl
| sQ191_spl ),
inference(split_clause,[status(thm)],[f1823,f1905,f505,f551]) ).
fof(f1912,definition,
! [X0,X1,X2] :
( sQ192_spl
<=> ( ~ rearsegP(X2,sK50_skl)
| ~ rearsegP(X1,X2)
| ~ ssList(X2)
| rearsegP(X0,nil)
| ~ rearsegP(X0,X1)
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ192_spl])],[split_symbol_definition]) ).
fof(f1915,plain,
( ~ sQ97_spl
| ~ sQ15_spl
| ~ sQ8_spl
| sQ192_spl ),
inference(split_clause,[status(thm)],[f1827,f1912,f505,f589,f1169]) ).
fof(f1917,definition,
! [X0,X1,X2] :
( sQ193_spl
<=> ( ~ rearsegP(X2,sK50_skl)
| ~ rearsegP(X1,X2)
| ~ ssList(X2)
| rearsegP(X0,sK50_skl)
| ~ rearsegP(X0,X1)
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ193_spl])],[split_symbol_definition]) ).
fof(f1920,plain,
( ~ sQ32_spl
| ~ sQ15_spl
| sQ193_spl ),
inference(split_clause,[status(thm)],[f1829,f1917,f589,f689]) ).
fof(f1927,definition,
! [X0,X1,X2,X3] :
( sQ195_spl
<=> ( ~ ssList(X2)
| ~ rearsegP(X3,X2)
| ~ rearsegP(X1,X3)
| ~ ssList(X3)
| ~ ssList(X2)
| rearsegP(X0,nil)
| ~ rearsegP(X0,X1)
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ195_spl])],[split_symbol_definition]) ).
fof(f1930,plain,
( ~ sQ8_spl
| sQ195_spl ),
inference(split_clause,[status(thm)],[f1833,f1927,f505]) ).
fof(f1934,definition,
! [X0,X1,X2] :
( sQ196_spl
<=> ( ~ rearsegP(nil,X2)
| ~ rearsegP(X2,X1)
| ~ ssList(X2)
| rearsegP(X0,X1)
| ~ rearsegP(X0,nil)
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ196_spl])],[split_symbol_definition]) ).
fof(f1937,plain,
( ~ sQ55_spl
| ~ sQ8_spl
| sQ196_spl ),
inference(split_clause,[status(thm)],[f1839,f1934,f505,f859]) ).
fof(f1938,definition,
! [X0,X1,X2] :
( sQ197_spl
<=> ( ~ rearsegP(nil,X2)
| ~ rearsegP(X2,X1)
| ~ ssList(X2)
| rearsegP(X0,X1)
| ~ rearsegP(X0,sK49_skl)
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ197_spl])],[split_symbol_definition]) ).
fof(f1941,plain,
( ~ sQ98_spl
| ~ sQ8_spl
| ~ sQ7_spl
| sQ197_spl ),
inference(split_clause,[status(thm)],[f1840,f1938,f502,f505,f1173]) ).
fof(f1943,definition,
! [X0,X1,X2] :
( sQ198_spl
<=> ( ~ rearsegP(sK49_skl,X2)
| ~ rearsegP(X2,X1)
| ~ ssList(X2)
| rearsegP(X0,X1)
| ~ rearsegP(X0,sK49_skl)
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ198_spl])],[split_symbol_definition]) ).
fof(f1946,plain,
( ~ sQ71_spl
| ~ sQ7_spl
| sQ198_spl ),
inference(split_clause,[status(thm)],[f1842,f1943,f502,f1015]) ).
fof(f1947,definition,
! [X0,X1,X2,X3] :
( sQ199_spl
<=> ( ~ ssList(X1)
| ~ rearsegP(sK50_skl,X3)
| ~ rearsegP(X3,X2)
| ~ ssList(X3)
| rearsegP(X0,X2)
| ~ rearsegP(X0,app(X1,sK50_skl))
| ~ ssList(X2)
| ~ ssList(app(X1,sK50_skl))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ199_spl])],[split_symbol_definition]) ).
fof(f1950,plain,
( ~ sQ30_spl
| ~ sQ15_spl
| sQ199_spl ),
inference(split_clause,[status(thm)],[f1843,f1947,f589,f681]) ).
fof(f1955,definition,
! [X0,X1,X2,X3,X4] :
( sQ201_spl
<=> ( ~ ssList(X1)
| ~ ssList(X2)
| ~ rearsegP(nil,X4)
| ~ rearsegP(X4,X3)
| ~ ssList(X4)
| rearsegP(X0,X3)
| ~ rearsegP(X0,app(X1,X2))
| ~ ssList(X3)
| ~ ssList(app(X1,X2))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ201_spl])],[split_symbol_definition]) ).
fof(f1958,plain,
( ~ sQ9_spl
| ~ sQ8_spl
| sQ201_spl ),
inference(split_clause,[status(thm)],[f1845,f1955,f505,f551]) ).
fof(f1960,definition,
! [X0,X1,X2] :
( sQ202_spl
<=> ( ~ rearsegP(nil,X2)
| ~ rearsegP(X2,X1)
| ~ ssList(X2)
| rearsegP(X0,X1)
| ~ rearsegP(X0,sK50_skl)
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ202_spl])],[split_symbol_definition]) ).
fof(f1963,plain,
( ~ sQ97_spl
| ~ sQ8_spl
| ~ sQ15_spl
| sQ202_spl ),
inference(split_clause,[status(thm)],[f1847,f1960,f589,f505,f1169]) ).
fof(f1965,definition,
! [X0,X1,X2] :
( sQ203_spl
<=> ( ~ rearsegP(sK50_skl,X2)
| ~ rearsegP(X2,X1)
| ~ ssList(X2)
| rearsegP(X0,X1)
| ~ rearsegP(X0,sK50_skl)
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ203_spl])],[split_symbol_definition]) ).
fof(f1968,plain,
( ~ sQ32_spl
| ~ sQ15_spl
| sQ203_spl ),
inference(split_clause,[status(thm)],[f1849,f1965,f589,f689]) ).
fof(f1973,plain,
( ~ sQ8_spl
| sQ144_spl ),
inference(split_clause,[status(thm)],[f1851,f1491,f505]) ).
fof(f1974,definition,
! [X0,X1,X2,X3] :
( sQ205_spl
<=> ( ~ ssList(X1)
| ~ rearsegP(nil,X3)
| ~ rearsegP(X3,X2)
| ~ ssList(X3)
| rearsegP(X0,X2)
| ~ rearsegP(X0,X1)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ205_spl])],[split_symbol_definition]) ).
fof(f1977,plain,
( ~ sQ8_spl
| sQ205_spl ),
inference(split_clause,[status(thm)],[f1852,f1974,f505]) ).
fof(f1982,definition,
! [X0,X1,X2] :
( sQ206_spl
<=> ( ~ rearsegP(X1,nil)
| ~ rearsegP(nil,X2)
| rearsegP(X0,X2)
| ~ rearsegP(X0,X1)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ206_spl])],[split_symbol_definition]) ).
fof(f1985,plain,
( ~ sQ55_spl
| ~ sQ8_spl
| sQ206_spl ),
inference(split_clause,[status(thm)],[f1857,f1982,f505,f859]) ).
fof(f1986,definition,
! [X0,X1,X2] :
( sQ207_spl
<=> ( ~ rearsegP(X1,sK49_skl)
| ~ rearsegP(nil,X2)
| rearsegP(X0,X2)
| ~ rearsegP(X0,X1)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ207_spl])],[split_symbol_definition]) ).
fof(f1989,plain,
( ~ sQ98_spl
| ~ sQ7_spl
| ~ sQ8_spl
| sQ207_spl ),
inference(split_clause,[status(thm)],[f1858,f1986,f505,f502,f1173]) ).
fof(f1990,definition,
! [X0,X1,X2] :
( sQ208_spl
<=> ( ~ rearsegP(X1,sK49_skl)
| ~ rearsegP(sK49_skl,X2)
| rearsegP(X0,X2)
| ~ rearsegP(X0,X1)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ208_spl])],[split_symbol_definition]) ).
fof(f1993,plain,
( ~ sQ71_spl
| ~ sQ7_spl
| sQ208_spl ),
inference(split_clause,[status(thm)],[f1859,f1990,f502,f1015]) ).
fof(f1994,definition,
! [X0,X1,X2,X3] :
( sQ209_spl
<=> ( ~ ssList(X3)
| ~ rearsegP(X1,app(X3,sK50_skl))
| ~ ssList(app(X3,sK50_skl))
| ~ rearsegP(sK50_skl,X2)
| rearsegP(X0,X2)
| ~ rearsegP(X0,X1)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ209_spl])],[split_symbol_definition]) ).
fof(f1997,plain,
( ~ sQ30_spl
| ~ sQ15_spl
| sQ209_spl ),
inference(split_clause,[status(thm)],[f1860,f1994,f589,f681]) ).
fof(f2002,definition,
! [X0,X1,X2,X3,X4] :
( sQ211_spl
<=> ( ~ ssList(X3)
| ~ ssList(X4)
| ~ rearsegP(X1,app(X3,X4))
| ~ ssList(app(X3,X4))
| ~ rearsegP(nil,X2)
| rearsegP(X0,X2)
| ~ rearsegP(X0,X1)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ211_spl])],[split_symbol_definition]) ).
fof(f2005,plain,
( ~ sQ9_spl
| ~ sQ8_spl
| sQ211_spl ),
inference(split_clause,[status(thm)],[f1862,f2002,f505,f551]) ).
fof(f2007,definition,
! [X0,X1,X2] :
( sQ212_spl
<=> ( ~ rearsegP(X1,sK50_skl)
| ~ rearsegP(nil,X2)
| rearsegP(X0,X2)
| ~ rearsegP(X0,X1)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ212_spl])],[split_symbol_definition]) ).
fof(f2010,plain,
( ~ sQ97_spl
| ~ sQ15_spl
| ~ sQ8_spl
| sQ212_spl ),
inference(split_clause,[status(thm)],[f1864,f2007,f505,f589,f1169]) ).
fof(f2011,definition,
! [X0,X1,X2] :
( sQ213_spl
<=> ( ~ rearsegP(X1,sK50_skl)
| ~ rearsegP(sK50_skl,X2)
| rearsegP(X0,X2)
| ~ rearsegP(X0,X1)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ213_spl])],[split_symbol_definition]) ).
fof(f2014,plain,
( ~ sQ32_spl
| ~ sQ15_spl
| sQ213_spl ),
inference(split_clause,[status(thm)],[f1865,f2011,f589,f689]) ).
fof(f2019,definition,
! [X0,X1,X2,X3] :
( sQ215_spl
<=> ( ~ ssList(X3)
| ~ rearsegP(X1,X3)
| ~ ssList(X3)
| ~ rearsegP(nil,X2)
| rearsegP(X0,X2)
| ~ rearsegP(X0,X1)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ215_spl])],[split_symbol_definition]) ).
fof(f2022,plain,
( ~ sQ8_spl
| sQ215_spl ),
inference(split_clause,[status(thm)],[f1867,f2019,f505]) ).
fof(f2063,plain,
! [X0,X1,X2,X3] :
( ~ sQ81_spl
| ~ rearsegP(X2,app(X0,sK49_skl))
| ~ ssList(app(X0,sK49_skl))
| ~ rearsegP(sK49_skl,X3)
| ~ ssList(sK49_skl)
| rearsegP(X1,X3)
| ~ rearsegP(X1,X2)
| ~ ssList(X3)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f1081,f786]) ).
fof(f2064,plain,
! [X0,X1] :
( ~ sQ81_spl
| ~ rearsegP(sK49_skl,app(X0,sK49_skl))
| ~ ssList(sK49_skl)
| ~ ssList(app(X0,sK49_skl))
| rearsegP(X1,sK49_skl)
| ~ rearsegP(X1,app(X0,sK49_skl))
| ~ ssList(sK49_skl)
| ~ ssList(app(X0,sK49_skl))
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f1081,f786]) ).
fof(f2065,plain,
! [X0,X1,X2,X3] :
( ~ sQ81_spl
| ~ rearsegP(sK49_skl,X3)
| ~ ssList(sK49_skl)
| ~ rearsegP(X3,X2)
| ~ ssList(X3)
| rearsegP(X1,X2)
| ~ rearsegP(X1,app(X0,sK49_skl))
| ~ ssList(X2)
| ~ ssList(app(X0,sK49_skl))
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f1081,f786]) ).
fof(f2067,plain,
! [X0,X1,X2,X3] :
( ~ sQ81_spl
| ~ rearsegP(X3,app(X0,sK49_skl))
| ~ rearsegP(X2,X3)
| ~ ssList(X3)
| ~ ssList(app(X0,sK49_skl))
| rearsegP(X1,sK49_skl)
| ~ rearsegP(X1,X2)
| ~ ssList(sK49_skl)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f1081,f786]) ).
fof(f2068,plain,
! [X0,X1,X2] :
( ~ sQ81_spl
| ~ rearsegP(X1,app(X0,sK49_skl))
| ~ ssList(app(X0,sK49_skl))
| rearsegP(app(X2,X1),sK49_skl)
| ~ ssList(X2)
| ~ ssList(sK49_skl)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f1081,f540]) ).
fof(f2069,plain,
! [X0,X1] :
( ~ sQ81_spl
| ~ rearsegP(X1,app(X0,sK49_skl))
| ~ ssList(app(X0,sK49_skl))
| app(sK6_skl(sK49_skl,X1),sK49_skl) = X1
| ~ ssList(sK49_skl)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f1081,f532]) ).
fof(f2070,plain,
! [X0,X1] :
( ~ sQ81_spl
| ~ rearsegP(X1,app(X0,sK49_skl))
| ~ ssList(app(X0,sK49_skl))
| sK49_skl = X1
| ~ rearsegP(sK49_skl,X1)
| ~ ssList(X1)
| ~ ssList(sK49_skl)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f1081,f527]) ).
fof(f2071,plain,
! [X0,X1] :
( ~ sQ81_spl
| ~ rearsegP(sK49_skl,X1)
| ~ ssList(sK49_skl)
| X1 = app(X0,sK49_skl)
| ~ rearsegP(X1,app(X0,sK49_skl))
| ~ ssList(app(X0,sK49_skl))
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f1081,f527]) ).
fof(f2072,plain,
! [X0,X1,X2] :
( ~ sQ81_spl
| ~ rearsegP(X2,app(X0,sK49_skl))
| ~ ssList(app(X0,sK49_skl))
| rearsegP(X1,sK49_skl)
| ~ rearsegP(X1,X2)
| ~ ssList(sK49_skl)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f1081,f524]) ).
fof(f2073,plain,
! [X0,X1,X2] :
( ~ sQ81_spl
| ~ rearsegP(sK49_skl,X2)
| ~ ssList(sK49_skl)
| rearsegP(X1,X2)
| ~ rearsegP(X1,app(X0,sK49_skl))
| ~ ssList(X2)
| ~ ssList(app(X0,sK49_skl))
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f1081,f524]) ).
fof(f2074,plain,
! [X0,X1] :
( ~ sQ81_spl
| rearsegP(app(X1,app(X0,sK49_skl)),sK49_skl)
| ~ ssList(X1)
| ~ ssList(sK49_skl)
| ~ ssList(app(X0,sK49_skl))
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f1081,f307]) ).
fof(f2075,plain,
! [X0] :
( ~ sQ81_spl
| app(sK6_skl(sK49_skl,app(X0,sK49_skl)),sK49_skl) = app(X0,sK49_skl)
| ~ ssList(sK49_skl)
| ~ ssList(app(X0,sK49_skl))
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f1081,f129]) ).
fof(f2076,plain,
! [X0] :
( ~ sQ81_spl
| sK49_skl = app(X0,sK49_skl)
| ~ rearsegP(sK49_skl,app(X0,sK49_skl))
| ~ ssList(app(X0,sK49_skl))
| ~ ssList(sK49_skl)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f1081,f303]) ).
fof(f2077,plain,
! [X0,X1] :
( ~ sQ81_spl
| rearsegP(X1,sK49_skl)
| ~ rearsegP(X1,app(X0,sK49_skl))
| ~ ssList(sK49_skl)
| ~ ssList(app(X0,sK49_skl))
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f1081,f301]) ).
fof(f2081,definition,
! [X0,X1,X2,X3] :
( sQ218_spl
<=> ( ~ rearsegP(X2,app(X0,sK49_skl))
| ~ ssList(app(X0,sK49_skl))
| ~ rearsegP(sK49_skl,X3)
| rearsegP(X1,X3)
| ~ rearsegP(X1,X2)
| ~ ssList(X3)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ218_spl])],[split_symbol_definition]) ).
fof(f2084,plain,
( ~ sQ81_spl
| ~ sQ7_spl
| sQ218_spl ),
inference(split_clause,[status(thm)],[f2063,f2081,f502,f1080]) ).
fof(f2085,definition,
! [X0,X1] :
( sQ219_spl
<=> ( ~ rearsegP(sK49_skl,app(X0,sK49_skl))
| ~ ssList(app(X0,sK49_skl))
| rearsegP(X1,sK49_skl)
| ~ rearsegP(X1,app(X0,sK49_skl))
| ~ ssList(app(X0,sK49_skl))
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ219_spl])],[split_symbol_definition]) ).
fof(f2088,plain,
( ~ sQ81_spl
| ~ sQ7_spl
| sQ219_spl ),
inference(split_clause,[status(thm)],[f2064,f2085,f502,f1080]) ).
fof(f2089,definition,
! [X0,X1,X2,X3] :
( sQ220_spl
<=> ( ~ rearsegP(sK49_skl,X3)
| ~ rearsegP(X3,X2)
| ~ ssList(X3)
| rearsegP(X1,X2)
| ~ rearsegP(X1,app(X0,sK49_skl))
| ~ ssList(X2)
| ~ ssList(app(X0,sK49_skl))
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ220_spl])],[split_symbol_definition]) ).
fof(f2092,plain,
( ~ sQ81_spl
| ~ sQ7_spl
| sQ220_spl ),
inference(split_clause,[status(thm)],[f2065,f2089,f502,f1080]) ).
fof(f2094,definition,
! [X0,X1,X2,X3] :
( sQ221_spl
<=> ( ~ rearsegP(X3,app(X0,sK49_skl))
| ~ rearsegP(X2,X3)
| ~ ssList(X3)
| ~ ssList(app(X0,sK49_skl))
| rearsegP(X1,sK49_skl)
| ~ rearsegP(X1,X2)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ221_spl])],[split_symbol_definition]) ).
fof(f2097,plain,
( ~ sQ81_spl
| ~ sQ7_spl
| sQ221_spl ),
inference(split_clause,[status(thm)],[f2067,f2094,f502,f1080]) ).
fof(f2098,definition,
! [X0,X1,X2] :
( sQ222_spl
<=> ( ~ rearsegP(X1,app(X0,sK49_skl))
| ~ ssList(app(X0,sK49_skl))
| rearsegP(app(X2,X1),sK49_skl)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ222_spl])],[split_symbol_definition]) ).
fof(f2101,plain,
( ~ sQ81_spl
| ~ sQ7_spl
| sQ222_spl ),
inference(split_clause,[status(thm)],[f2068,f2098,f502,f1080]) ).
fof(f2102,definition,
! [X0,X1] :
( sQ223_spl
<=> ( ~ rearsegP(X1,app(X0,sK49_skl))
| ~ ssList(app(X0,sK49_skl))
| app(sK6_skl(sK49_skl,X1),sK49_skl) = X1
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ223_spl])],[split_symbol_definition]) ).
fof(f2105,plain,
( ~ sQ81_spl
| ~ sQ7_spl
| sQ223_spl ),
inference(split_clause,[status(thm)],[f2069,f2102,f502,f1080]) ).
fof(f2106,definition,
! [X0,X1] :
( sQ224_spl
<=> ( ~ rearsegP(X1,app(X0,sK49_skl))
| ~ ssList(app(X0,sK49_skl))
| sK49_skl = X1
| ~ rearsegP(sK49_skl,X1)
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ224_spl])],[split_symbol_definition]) ).
fof(f2109,plain,
( ~ sQ81_spl
| ~ sQ7_spl
| sQ224_spl ),
inference(split_clause,[status(thm)],[f2070,f2106,f502,f1080]) ).
fof(f2110,definition,
! [X0,X1] :
( sQ225_spl
<=> ( ~ rearsegP(sK49_skl,X1)
| X1 = app(X0,sK49_skl)
| ~ rearsegP(X1,app(X0,sK49_skl))
| ~ ssList(app(X0,sK49_skl))
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ225_spl])],[split_symbol_definition]) ).
fof(f2113,plain,
( ~ sQ81_spl
| ~ sQ7_spl
| sQ225_spl ),
inference(split_clause,[status(thm)],[f2071,f2110,f502,f1080]) ).
fof(f2114,definition,
! [X0,X1,X2] :
( sQ226_spl
<=> ( ~ rearsegP(X2,app(X0,sK49_skl))
| ~ ssList(app(X0,sK49_skl))
| rearsegP(X1,sK49_skl)
| ~ rearsegP(X1,X2)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ226_spl])],[split_symbol_definition]) ).
fof(f2117,plain,
( ~ sQ81_spl
| ~ sQ7_spl
| sQ226_spl ),
inference(split_clause,[status(thm)],[f2072,f2114,f502,f1080]) ).
fof(f2118,definition,
! [X0,X1,X2] :
( sQ227_spl
<=> ( ~ rearsegP(sK49_skl,X2)
| rearsegP(X1,X2)
| ~ rearsegP(X1,app(X0,sK49_skl))
| ~ ssList(X2)
| ~ ssList(app(X0,sK49_skl))
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ227_spl])],[split_symbol_definition]) ).
fof(f2121,plain,
( ~ sQ81_spl
| ~ sQ7_spl
| sQ227_spl ),
inference(split_clause,[status(thm)],[f2073,f2118,f502,f1080]) ).
fof(f2122,definition,
! [X0,X1] :
( sQ228_spl
<=> ( rearsegP(app(X1,app(X0,sK49_skl)),sK49_skl)
| ~ ssList(X1)
| ~ ssList(app(X0,sK49_skl))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ228_spl])],[split_symbol_definition]) ).
fof(f2125,plain,
( ~ sQ81_spl
| ~ sQ7_spl
| sQ228_spl ),
inference(split_clause,[status(thm)],[f2074,f2122,f502,f1080]) ).
fof(f2126,definition,
! [X0] :
( sQ229_spl
<=> ( app(sK6_skl(sK49_skl,app(X0,sK49_skl)),sK49_skl) = app(X0,sK49_skl)
| ~ ssList(app(X0,sK49_skl))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ229_spl])],[split_symbol_definition]) ).
fof(f2129,plain,
( ~ sQ81_spl
| ~ sQ7_spl
| sQ229_spl ),
inference(split_clause,[status(thm)],[f2075,f2126,f502,f1080]) ).
fof(f2130,definition,
! [X0] :
( sQ230_spl
<=> ( sK49_skl = app(X0,sK49_skl)
| ~ rearsegP(sK49_skl,app(X0,sK49_skl))
| ~ ssList(app(X0,sK49_skl))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ230_spl])],[split_symbol_definition]) ).
fof(f2133,plain,
( ~ sQ81_spl
| ~ sQ7_spl
| sQ230_spl ),
inference(split_clause,[status(thm)],[f2076,f2130,f502,f1080]) ).
fof(f2134,definition,
! [X0,X1] :
( sQ231_spl
<=> ( rearsegP(X1,sK49_skl)
| ~ rearsegP(X1,app(X0,sK49_skl))
| ~ ssList(app(X0,sK49_skl))
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ231_spl])],[split_symbol_definition]) ).
fof(f2137,plain,
( ~ sQ81_spl
| ~ sQ7_spl
| sQ231_spl ),
inference(split_clause,[status(thm)],[f2077,f2134,f502,f1080]) ).
fof(f2143,plain,
! [X0,X1] :
( ~ sQ44_spl
| ~ ssList(nil)
| rearsegP(X0,nil)
| ~ rearsegP(X0,X1)
| ~ ssList(nil)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f801,f309]) ).
fof(f2145,plain,
! [X0,X1,X2,X3] :
( ~ sQ44_spl
| ~ rearsegP(X3,X2)
| ~ rearsegP(nil,X3)
| ~ ssList(X2)
| ~ ssList(X3)
| ~ ssList(nil)
| rearsegP(X0,X2)
| ~ rearsegP(X0,X1)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f801,f301]) ).
fof(f2146,definition,
! [X0,X1] :
( sQ232_spl
<=> ( rearsegP(X0,nil)
| ~ rearsegP(X0,X1)
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ232_spl])],[split_symbol_definition]) ).
fof(f2150,plain,
( ~ sQ44_spl
| ~ sQ8_spl
| sQ232_spl ),
inference(split_clause,[status(thm)],[f2143,f2146,f505,f781]) ).
fof(f2152,definition,
! [X0,X1,X2,X3] :
( sQ233_spl
<=> ( ~ rearsegP(X3,X2)
| ~ rearsegP(nil,X3)
| ~ ssList(X2)
| ~ ssList(X3)
| rearsegP(X0,X2)
| ~ rearsegP(X0,X1)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ233_spl])],[split_symbol_definition]) ).
fof(f2155,plain,
( ~ sQ44_spl
| ~ sQ8_spl
| sQ233_spl ),
inference(split_clause,[status(thm)],[f2145,f2152,f505,f781]) ).
fof(f2176,plain,
! [X0] :
( ~ sQ85_spl
| segmentP(app(sK49_skl,X0),sK5_skl(nil,sK49_skl))
| ~ ssList(X0)
| ~ ssList(nil)
| ~ ssList(sK5_skl(nil,sK49_skl)) ),
inference(paramodulation,[status(thm)],[f1108,f652]) ).
fof(f2178,plain,
( ~ sQ85_spl
| rearsegP(sK49_skl,sK5_skl(nil,sK49_skl))
| ~ ssList(nil)
| ~ ssList(sK5_skl(nil,sK49_skl)) ),
inference(paramodulation,[status(thm)],[f1108,f539]) ).
fof(f2179,plain,
( ~ sQ85_spl
| ~ ssList(sK5_skl(nil,sK49_skl))
| frontsegP(app(nil,sK5_skl(nil,sK49_skl)),nil)
| ~ ssList(nil)
| ~ ssList(sK49_skl) ),
inference(paramodulation,[status(thm)],[f1108,f457]) ).
fof(f2180,definition,
( sQ236_spl
<=> ssList(sK5_skl(nil,sK49_skl)) ),
introduced(definition,[new_symbols(definition,[sQ236_spl])],[split_symbol_definition]) ).
fof(f2182,plain,
( sQ236_spl
| ~ ssList(sK5_skl(nil,sK49_skl)) ),
inference(component_clause,[status(thm)],[f2180]) ).
fof(f2184,definition,
! [X0] :
( sQ237_spl
<=> ( segmentP(app(sK49_skl,X0),sK5_skl(nil,sK49_skl))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ237_spl])],[split_symbol_definition]) ).
fof(f2187,plain,
( ~ sQ85_spl
| sQ237_spl
| ~ sQ8_spl
| ~ sQ236_spl ),
inference(split_clause,[status(thm)],[f2176,f2180,f505,f2184,f1107]) ).
fof(f2189,definition,
( sQ238_spl
<=> rearsegP(sK49_skl,sK5_skl(nil,sK49_skl)) ),
introduced(definition,[new_symbols(definition,[sQ238_spl])],[split_symbol_definition]) ).
fof(f2192,plain,
( ~ sQ85_spl
| sQ238_spl
| ~ sQ8_spl
| ~ sQ236_spl ),
inference(split_clause,[status(thm)],[f2178,f2180,f505,f2189,f1107]) ).
fof(f2193,definition,
( sQ239_spl
<=> frontsegP(app(nil,sK5_skl(nil,sK49_skl)),nil) ),
introduced(definition,[new_symbols(definition,[sQ239_spl])],[split_symbol_definition]) ).
fof(f2196,plain,
( ~ sQ85_spl
| ~ sQ236_spl
| sQ239_spl
| ~ sQ8_spl
| ~ sQ7_spl ),
inference(split_clause,[status(thm)],[f2179,f502,f505,f2193,f2180,f1107]) ).
fof(f2197,plain,
( sQ236_spl
| ~ frontsegP(sK49_skl,nil)
| ~ ssList(nil)
| ~ ssList(sK49_skl) ),
inference(resolution,[status(thm)],[f2182,f122]) ).
fof(f2198,definition,
( sQ240_spl
<=> frontsegP(sK49_skl,nil) ),
introduced(definition,[new_symbols(definition,[sQ240_spl])],[split_symbol_definition]) ).
fof(f2200,plain,
( sQ240_spl
| ~ frontsegP(sK49_skl,nil) ),
inference(component_clause,[status(thm)],[f2198]) ).
fof(f2201,plain,
( sQ236_spl
| ~ sQ240_spl
| ~ sQ8_spl
| ~ sQ7_spl ),
inference(split_clause,[status(thm)],[f2197,f502,f505,f2198,f2180]) ).
fof(f2202,plain,
( sQ240_spl
| ~ sQ72_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2200,f1027]) ).
fof(f2203,plain,
( sQ240_spl
| ~ sQ72_spl ),
inference(contradiction_clause,[status(thm)],[f2202]) ).
fof(f2247,plain,
! [X0] :
( ~ sQ86_spl
| segmentP(app(sK50_skl,X0),sK5_skl(nil,sK50_skl))
| ~ ssList(X0)
| ~ ssList(nil)
| ~ ssList(sK5_skl(nil,sK50_skl)) ),
inference(paramodulation,[status(thm)],[f1113,f652]) ).
fof(f2249,plain,
( ~ sQ86_spl
| rearsegP(sK50_skl,sK5_skl(nil,sK50_skl))
| ~ ssList(nil)
| ~ ssList(sK5_skl(nil,sK50_skl)) ),
inference(paramodulation,[status(thm)],[f1113,f539]) ).
fof(f2250,plain,
( ~ sQ86_spl
| ~ ssList(sK5_skl(nil,sK50_skl))
| frontsegP(app(nil,sK5_skl(nil,sK50_skl)),nil)
| ~ ssList(nil)
| ~ ssList(sK50_skl) ),
inference(paramodulation,[status(thm)],[f1113,f457]) ).
fof(f2251,definition,
( sQ243_spl
<=> ssList(sK5_skl(nil,sK50_skl)) ),
introduced(definition,[new_symbols(definition,[sQ243_spl])],[split_symbol_definition]) ).
fof(f2253,plain,
( sQ243_spl
| ~ ssList(sK5_skl(nil,sK50_skl)) ),
inference(component_clause,[status(thm)],[f2251]) ).
fof(f2255,definition,
! [X0] :
( sQ244_spl
<=> ( segmentP(app(sK50_skl,X0),sK5_skl(nil,sK50_skl))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ244_spl])],[split_symbol_definition]) ).
fof(f2258,plain,
( ~ sQ86_spl
| sQ244_spl
| ~ sQ8_spl
| ~ sQ243_spl ),
inference(split_clause,[status(thm)],[f2247,f2251,f505,f2255,f1112]) ).
fof(f2260,definition,
( sQ245_spl
<=> rearsegP(sK50_skl,sK5_skl(nil,sK50_skl)) ),
introduced(definition,[new_symbols(definition,[sQ245_spl])],[split_symbol_definition]) ).
fof(f2263,plain,
( ~ sQ86_spl
| sQ245_spl
| ~ sQ8_spl
| ~ sQ243_spl ),
inference(split_clause,[status(thm)],[f2249,f2251,f505,f2260,f1112]) ).
fof(f2264,definition,
( sQ246_spl
<=> frontsegP(app(nil,sK5_skl(nil,sK50_skl)),nil) ),
introduced(definition,[new_symbols(definition,[sQ246_spl])],[split_symbol_definition]) ).
fof(f2267,plain,
( ~ sQ86_spl
| ~ sQ243_spl
| sQ246_spl
| ~ sQ8_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f2250,f589,f505,f2264,f2251,f1112]) ).
fof(f2268,plain,
( sQ243_spl
| ~ frontsegP(sK50_skl,nil)
| ~ ssList(nil)
| ~ ssList(sK50_skl) ),
inference(resolution,[status(thm)],[f2253,f122]) ).
fof(f2269,definition,
( sQ247_spl
<=> frontsegP(sK50_skl,nil) ),
introduced(definition,[new_symbols(definition,[sQ247_spl])],[split_symbol_definition]) ).
fof(f2271,plain,
( sQ247_spl
| ~ frontsegP(sK50_skl,nil) ),
inference(component_clause,[status(thm)],[f2269]) ).
fof(f2272,plain,
( sQ243_spl
| ~ sQ247_spl
| ~ sQ8_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f2268,f589,f505,f2269,f2251]) ).
fof(f2273,plain,
( sQ247_spl
| ~ sQ83_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2271,f1104]) ).
fof(f2274,plain,
( sQ247_spl
| ~ sQ83_spl ),
inference(contradiction_clause,[status(thm)],[f2273]) ).
fof(f2276,plain,
( ~ sQ50_spl
| ~ sQ21_spl
| ~ ssList(nil)
| segmentP(app(sK50_skl,nil),sK49_skl)
| ~ ssList(sK50_skl) ),
inference(paramodulation,[status(thm)],[f1524,f836]) ).
fof(f2277,definition,
( sQ248_spl
<=> segmentP(app(sK50_skl,nil),sK49_skl) ),
introduced(definition,[new_symbols(definition,[sQ248_spl])],[split_symbol_definition]) ).
fof(f2278,plain,
( ~ sQ248_spl
| segmentP(app(sK50_skl,nil),sK49_skl) ),
inference(component_clause,[status(thm)],[f2277]) ).
fof(f2280,plain,
( ~ sQ50_spl
| ~ sQ21_spl
| ~ sQ8_spl
| sQ248_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f2276,f589,f2277,f505,f623,f817]) ).
fof(f2281,plain,
( ~ sQ248_spl
| segmentP(sK50_skl,sK49_skl) ),
inference(forward_demodulation,[status(thm)],[f1524,f2278]) ).
fof(f2282,plain,
( ~ sQ248_spl
| sQ3_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2281,f510]) ).
fof(f2283,plain,
( ~ sQ248_spl
| sQ3_spl ),
inference(contradiction_clause,[status(thm)],[f2282]) ).
fof(f2284,plain,
$false,
inference(sat_refutation,[status(thm)],[f434,f441,f448,f452,f498,f508,f512,f514,f545,f554,f558,f562,f566,f577,f582,f592,f594,f626,f660,f664,f668,f672,f780,f784,f798,f820,f834,f866,f880,f901,f986,f994,f1018,f1022,f1026,f1052,f1056,f1060,f1064,f1070,f1074,f1079,f1083,f1087,f1095,f1099,f1103,f1110,f1115,f1132,f1136,f1140,f1144,f1148,f1152,f1156,f1160,f1164,f1168,f1215,f1219,f1220,f1224,f1227,f1231,f1236,f1237,f1238,f1254,f1258,f1262,f1266,f1270,f1274,f1278,f1282,f1290,f1304,f1308,f1312,f1316,f1320,f1324,f1328,f1332,f1340,f1364,f1368,f1372,f1376,f1380,f1384,f1388,f1392,f1396,f1400,f1412,f1416,f1420,f1429,f1434,f1473,f1477,f1482,f1489,f1498,f1502,f1510,f1540,f1544,f1558,f1563,f1567,f1572,f1582,f1586,f1615,f1624,f1643,f1647,f1651,f1655,f1661,f1667,f1669,f1687,f1708,f1709,f1710,f1715,f1748,f1762,f1796,f1798,f1874,f1879,f1884,f1888,f1892,f1904,f1908,f1915,f1920,f1930,f1937,f1941,f1946,f1950,f1958,f1963,f1968,f1973,f1977,f1985,f1989,f1993,f1997,f2005,f2010,f2014,f2022,f2084,f2088,f2092,f2097,f2101,f2105,f2109,f2113,f2117,f2121,f2125,f2129,f2133,f2137,f2150,f2155,f2187,f2192,f2196,f2201,f2203,f2258,f2263,f2267,f2272,f2274,f2280,f2283]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWC122+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.05 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/0.47 % Computer : n018.cluster.edu
% 0.16/0.47 % Model : x86_64 x86_64
% 0.16/0.47 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.47 % Memory : 8046.5625MB
% 0.16/0.47 % OS : Linux 6.8.0-71-generic
% 0.16/0.47 % CPULimit : 300
% 0.16/0.47 % WCLimit : 300
% 0.16/0.47 % DateTime : Mon Sep 21 07:58:58 UTC 2026
% 0.16/0.47 % CPUTime :
% 0.16/0.50 % Drodi V4.1.1
% 0.21/0.69 % Refutation found
% 0.21/0.69 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.21/0.69 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.21/0.74 % Elapsed time: 0.244928 seconds
% 0.21/0.74 % CPU time: 1.257537 seconds
% 0.21/0.74 % Total memory used: 122.793 MB
% 0.21/0.74 % Net memory used: 121.740 MB
%------------------------------------------------------------------------------