%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWC108+1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/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:39:59 PM UTC 2026
% Result : Theorem 0.11s 0.51s
% Output : CNFRefutation 0.11s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 194
% Syntax : Number of formulae : 731 ( 18 unt; 175 def)
% Number of atoms : 2894 ( 275 equ)
% Maximal formula atoms : 15 ( 3 avg)
% Number of connectives : 4011 (1848 ~;1856 |; 77 &)
% ( 185 <=>; 45 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 5 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 183 ( 181 usr; 174 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 7 con; 0-2 aty)
% Number of variables : 492 ( 470 !; 22 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
? [U] :
( ? [V] :
( U != V
& ssItem(V) )
& ssItem(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ( frontsegP(U,V)
<=> ? [W] :
( app(V,W) = U
& ssList(W) ) ) ) ),
file('/export/starexec/sandbox2/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/sandbox2/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/sandbox2/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ( neq(U,V)
<=> U != V ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f17,axiom,
ssList(nil),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f28,axiom,
! [U] :
( ssList(U)
=> app(nil,U) = U ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f45,axiom,
! [U] :
( ssList(U)
=> frontsegP(U,nil) ),
file('/export/starexec/sandbox2/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/sandbox2/benchmark/theBenchmark.p') ).
fof(f48,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ( ( rearsegP(V,U)
& rearsegP(U,V) )
=> U = V ) ) ),
file('/export/starexec/sandbox2/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/sandbox2/benchmark/theBenchmark.p') ).
fof(f51,axiom,
! [U] :
( ssList(U)
=> rearsegP(U,nil) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f52,axiom,
! [U] :
( ssList(U)
=> ( rearsegP(nil,U)
<=> nil = U ) ),
file('/export/starexec/sandbox2/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/sandbox2/benchmark/theBenchmark.p') ).
fof(f54,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ( ( segmentP(V,U)
& segmentP(U,V) )
=> U = V ) ) ),
file('/export/starexec/sandbox2/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/sandbox2/benchmark/theBenchmark.p') ).
fof(f57,axiom,
! [U] :
( ssList(U)
=> segmentP(U,nil) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f84,axiom,
! [U] :
( ssList(U)
=> app(U,nil) = U ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f96,conjecture,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ! [W] :
( ssList(W)
=> ! [X] :
( ssList(X)
=> ( ( ( ~ rearsegP(X,W)
| ~ neq(W,nil) )
& ( nil != W
| nil != X ) )
| ( ( ( segmentP(V,U)
& neq(U,nil) )
| ~ neq(V,nil) )
& ( nil = U
| nil != V ) )
| U != W
| V != X ) ) ) ) ),
file('/export/starexec/sandbox2/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) )
& ( nil != W
| nil != X ) )
| ( ( ( segmentP(V,U)
& neq(U,nil) )
| ~ neq(V,nil) )
& ( nil = U
| nil != V ) )
| U != W
| V != X ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f96]) ).
fof(f102,plain,
( sK0_skl != sK1_skl
& ssItem(sK1_skl)
& ssItem(sK0_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(U,sK0_skl),skolemize(V,sK1_skl)],[f2]) ).
fof(f105,plain,
sK0_skl != sK1_skl,
inference(cnf_transformation,[status(thm)],[f102]) ).
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(f130,plain,
! [X0,X1,X2] :
( app(X2,X1) != X0
| ~ ssList(X2)
| 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(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(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) )
| ( nil = W
& nil = X ) )
& ( ( ( ~ segmentP(V,U)
| ~ neq(U,nil) )
& neq(V,nil) )
| ( nil != U
& nil = V ) )
& U = W
& V = X
& ssList(X) )
& ssList(W) )
& ssList(V) )
& ssList(U) ),
inference(pre_NNF_transformation,[status(thm)],[f97]) ).
fof(f416,definition,
! [U,V] :
( sP0_prd(V,U)
<=> ( nil != U
& nil = V ) ),
introduced(definition,[new_symbols(definition,[sP0_prd])],[]) ).
fof(f417,definition,
! [W,X] :
( sP1_prd(X,W)
<=> ( nil = W
& nil = X ) ),
introduced(definition,[new_symbols(definition,[sP1_prd])],[]) ).
fof(f418,plain,
? [U] :
( ? [V] :
( ? [W] :
( ? [X] :
( ( ( rearsegP(X,W)
& neq(W,nil) )
| sP1_prd(X,W) )
& ( ( ( ~ segmentP(V,U)
| ~ neq(U,nil) )
& neq(V,nil) )
| sP0_prd(V,U) )
& U = W
& V = X
& ssList(X) )
& ssList(W) )
& ssList(V) )
& ssList(U) ),
inference(formula_renaming,[status(thm)],[f415,f417,f416]) ).
fof(f419,plain,
( ( ( rearsegP(sK50_skl,sK49_skl)
& neq(sK49_skl,nil) )
| sP1_prd(sK50_skl,sK49_skl) )
& ( ( ( ~ segmentP(sK48_skl,sK47_skl)
| ~ neq(sK47_skl,nil) )
& neq(sK48_skl,nil) )
| sP0_prd(sK48_skl,sK47_skl) )
& 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)],[f418]) ).
fof(f420,plain,
ssList(sK47_skl),
inference(cnf_transformation,[status(thm)],[f419]) ).
fof(f421,plain,
ssList(sK48_skl),
inference(cnf_transformation,[status(thm)],[f419]) ).
fof(f424,plain,
sK48_skl = sK50_skl,
inference(cnf_transformation,[status(thm)],[f419]) ).
fof(f425,plain,
sK47_skl = sK49_skl,
inference(cnf_transformation,[status(thm)],[f419]) ).
fof(f426,plain,
( neq(sK48_skl,nil)
| sP0_prd(sK48_skl,sK47_skl) ),
inference(cnf_transformation,[status(thm)],[f419]) ).
fof(f427,plain,
( ~ segmentP(sK48_skl,sK47_skl)
| ~ neq(sK47_skl,nil)
| sP0_prd(sK48_skl,sK47_skl) ),
inference(cnf_transformation,[status(thm)],[f419]) ).
fof(f428,plain,
( neq(sK49_skl,nil)
| sP1_prd(sK50_skl,sK49_skl) ),
inference(cnf_transformation,[status(thm)],[f419]) ).
fof(f429,plain,
( rearsegP(sK50_skl,sK49_skl)
| sP1_prd(sK50_skl,sK49_skl) ),
inference(cnf_transformation,[status(thm)],[f419]) ).
fof(f430,plain,
! [U,V] :
( ( nil = U
| nil != V
| sP0_prd(V,U) )
& ( ( nil != U
& nil = V )
| ~ sP0_prd(V,U) ) ),
inference(NNF_transformation,[status(thm)],[f416]) ).
fof(f431,plain,
( ! [U,V] :
( nil = U
| nil != V
| sP0_prd(V,U) )
& ! [U,V] :
( ( nil != U
& nil = V )
| ~ sP0_prd(V,U) ) ),
inference(miniscoping,[status(thm)],[f430]) ).
fof(f432,plain,
! [X0,X1] :
( nil = X0
| ~ sP0_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f431]) ).
fof(f433,plain,
! [X0,X1] :
( nil != X1
| ~ sP0_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f431]) ).
fof(f434,plain,
! [X0,X1] :
( nil = X1
| nil != X0
| sP0_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f431]) ).
fof(f435,plain,
! [W,X] :
( ( nil != W
| nil != X
| sP1_prd(X,W) )
& ( ( nil = W
& nil = X )
| ~ sP1_prd(X,W) ) ),
inference(NNF_transformation,[status(thm)],[f417]) ).
fof(f436,plain,
( ! [W,X] :
( nil != W
| nil != X
| sP1_prd(X,W) )
& ! [W,X] :
( ( nil = W
& nil = X )
| ~ sP1_prd(X,W) ) ),
inference(miniscoping,[status(thm)],[f435]) ).
fof(f437,plain,
! [X0,X1] :
( nil = X0
| ~ sP1_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f436]) ).
fof(f438,plain,
! [X0,X1] :
( nil = X1
| ~ sP1_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f436]) ).
fof(f440,definition,
( sQ0_spl
<=> sP0_prd(sK48_skl,sK47_skl) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f441,plain,
( ~ sQ0_spl
| sP0_prd(sK48_skl,sK47_skl) ),
inference(component_clause,[status(thm)],[f440]) ).
fof(f443,definition,
( sQ1_spl
<=> neq(sK48_skl,nil) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f444,plain,
( ~ sQ1_spl
| neq(sK48_skl,nil) ),
inference(component_clause,[status(thm)],[f443]) ).
fof(f446,plain,
( sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f426,f440,f443]) ).
fof(f447,definition,
( sQ2_spl
<=> neq(sK47_skl,nil) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f449,plain,
( sQ2_spl
| ~ neq(sK47_skl,nil) ),
inference(component_clause,[status(thm)],[f447]) ).
fof(f450,definition,
( sQ3_spl
<=> segmentP(sK48_skl,sK47_skl) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f452,plain,
( sQ3_spl
| ~ segmentP(sK48_skl,sK47_skl) ),
inference(component_clause,[status(thm)],[f450]) ).
fof(f453,plain,
( ~ sQ3_spl
| ~ sQ2_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f427,f440,f447,f450]) ).
fof(f454,definition,
( sQ4_spl
<=> sP1_prd(sK50_skl,sK49_skl) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f455,plain,
( ~ sQ4_spl
| sP1_prd(sK50_skl,sK49_skl) ),
inference(component_clause,[status(thm)],[f454]) ).
fof(f457,definition,
( sQ5_spl
<=> neq(sK49_skl,nil) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f458,plain,
( ~ sQ5_spl
| neq(sK49_skl,nil) ),
inference(component_clause,[status(thm)],[f457]) ).
fof(f460,plain,
( sQ5_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f428,f454,f457]) ).
fof(f461,definition,
( sQ6_spl
<=> rearsegP(sK50_skl,sK49_skl) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f462,plain,
( ~ sQ6_spl
| rearsegP(sK50_skl,sK49_skl) ),
inference(component_clause,[status(thm)],[f461]) ).
fof(f464,plain,
( sQ6_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f429,f454,f461]) ).
fof(f469,plain,
! [X0,X1] :
( ~ ssList(X1)
| frontsegP(app(X0,X1),X0)
| ~ ssList(X0)
| ~ ssList(app(X0,X1)) ),
inference(destructive_equality_resolution,[status(thm)],[f124]) ).
fof(f470,plain,
! [X0,X1] :
( ~ ssList(X0)
| rearsegP(app(X0,X1),X1)
| ~ ssList(X1)
| ~ ssList(app(X0,X1)) ),
inference(destructive_equality_resolution,[status(thm)],[f130]) ).
fof(f471,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(f480,plain,
! [X1] :
( ~ neq(X1,X1)
| ~ ssList(X1)
| ~ ssList(X1) ),
inference(destructive_equality_resolution,[status(thm)],[f219]) ).
fof(f481,plain,
! [X0] :
( ~ neq(X0,X0)
| ~ ssList(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f480]) ).
fof(f495,plain,
! [X0] : ~ sP0_prd(X0,nil),
inference(destructive_equality_resolution,[status(thm)],[f433]) ).
fof(f496,plain,
! [X0] :
( nil = X0
| sP0_prd(nil,X0) ),
inference(destructive_equality_resolution,[status(thm)],[f434]) ).
fof(f500,plain,
( ~ sQ4_spl
| sP1_prd(sK48_skl,sK49_skl) ),
inference(forward_demodulation,[status(thm)],[f424,f455]) ).
fof(f501,plain,
( ~ sQ4_spl
| sP1_prd(sK48_skl,sK47_skl) ),
inference(forward_demodulation,[status(thm)],[f425,f500]) ).
fof(f506,plain,
( ~ sQ0_spl
| nil = sK48_skl ),
inference(resolution,[status(thm)],[f432,f441]) ).
fof(f507,plain,
( ~ sQ0_spl
| sP0_prd(nil,sK47_skl) ),
inference(backward_demodulation,[status(thm)],[f506,f441]) ).
fof(f508,plain,
( ~ sQ4_spl
| ~ sQ0_spl
| sP1_prd(nil,sK47_skl) ),
inference(backward_demodulation,[status(thm)],[f506,f501]) ).
fof(f509,plain,
( ~ sQ0_spl
| nil = sK50_skl ),
inference(backward_demodulation,[status(thm)],[f506,f424]) ).
fof(f512,plain,
! [X0] :
( nil = nil
| nil = X0 ),
inference(resolution,[status(thm)],[f496,f432]) ).
fof(f513,definition,
! [X0] :
( sQ7_spl
<=> nil = X0 ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f514,plain,
! [X0] :
( ~ sQ7_spl
| nil = X0 ),
inference(component_clause,[status(thm)],[f513]) ).
fof(f516,definition,
( sQ8_spl
<=> nil = nil ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f519,plain,
( sQ8_spl
| sQ7_spl ),
inference(split_clause,[status(thm)],[f512,f513,f516]) ).
fof(f520,plain,
! [X0,X1] :
( ~ sQ7_spl
| X0 = X1 ),
inference(paramodulation,[status(thm)],[f514,f514]) ).
fof(f531,plain,
( ~ sQ7_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f105,f520]) ).
fof(f532,plain,
~ sQ7_spl,
inference(contradiction_clause,[status(thm)],[f531]) ).
fof(f535,plain,
( ~ sQ4_spl
| ~ sQ0_spl
| nil = sK47_skl ),
inference(resolution,[status(thm)],[f438,f508]) ).
fof(f538,plain,
( ~ sQ0_spl
| ~ sQ4_spl
| sP0_prd(nil,nil) ),
inference(backward_demodulation,[status(thm)],[f535,f507]) ).
fof(f541,plain,
( ~ sQ0_spl
| ~ sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f538,f495]) ).
fof(f542,plain,
( ~ sQ0_spl
| ~ sQ4_spl ),
inference(contradiction_clause,[status(thm)],[f541]) ).
fof(f546,plain,
( ~ sQ5_spl
| neq(sK47_skl,nil) ),
inference(forward_demodulation,[status(thm)],[f425,f458]) ).
fof(f566,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(f568,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)],[f566]) ).
fof(f570,plain,
( sQ2_spl
| sK47_skl = nil
| ~ ssList(nil)
| ~ ssList(sK47_skl) ),
inference(resolution,[status(thm)],[f449,f220]) ).
fof(f571,definition,
( sQ13_spl
<=> ssList(sK47_skl) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f573,plain,
( sQ13_spl
| ~ ssList(sK47_skl) ),
inference(component_clause,[status(thm)],[f571]) ).
fof(f574,definition,
( sQ14_spl
<=> ssList(nil) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f576,plain,
( sQ14_spl
| ~ ssList(nil) ),
inference(component_clause,[status(thm)],[f574]) ).
fof(f577,definition,
( sQ15_spl
<=> sK47_skl = nil ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f578,plain,
( ~ sQ15_spl
| sK47_skl = nil ),
inference(component_clause,[status(thm)],[f577]) ).
fof(f580,plain,
( sQ2_spl
| sQ15_spl
| ~ sQ14_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f570,f571,f574,f577,f447]) ).
fof(f583,plain,
( ~ sQ4_spl
| ~ sQ15_spl
| sP1_prd(sK48_skl,nil) ),
inference(forward_demodulation,[status(thm)],[f578,f501]) ).
fof(f585,plain,
( ~ sQ4_spl
| ~ sQ15_spl
| nil = sK48_skl ),
inference(resolution,[status(thm)],[f583,f437]) ).
fof(f589,plain,
( ~ sQ1_spl
| ~ sQ4_spl
| ~ sQ15_spl
| neq(nil,nil) ),
inference(backward_demodulation,[status(thm)],[f585,f444]) ).
fof(f598,plain,
( ~ sQ1_spl
| ~ sQ4_spl
| ~ sQ15_spl
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f589,f481]) ).
fof(f599,plain,
( ~ sQ1_spl
| ~ sQ4_spl
| ~ sQ15_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f598,f223]) ).
fof(f600,plain,
( ~ sQ1_spl
| ~ sQ4_spl
| ~ sQ15_spl ),
inference(contradiction_clause,[status(thm)],[f599]) ).
fof(f601,plain,
( sQ14_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f576,f223]) ).
fof(f602,plain,
sQ14_spl,
inference(contradiction_clause,[status(thm)],[f601]) ).
fof(f603,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(f604,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)],[f603]) ).
fof(f607,plain,
( sQ13_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f573,f420]) ).
fof(f608,plain,
sQ13_spl,
inference(contradiction_clause,[status(thm)],[f607]) ).
fof(f610,plain,
( ~ sQ0_spl
| nil = sK50_skl ),
inference(backward_demodulation,[status(thm)],[f612,f424]) ).
fof(f612,plain,
( ~ sQ0_spl
| nil = sK48_skl ),
inference(forward_demodulation,[status(thm)],[f424,f509]) ).
fof(f615,plain,
( ~ sQ5_spl
| ~ sQ15_spl
| neq(nil,nil) ),
inference(forward_demodulation,[status(thm)],[f578,f546]) ).
fof(f616,plain,
( ~ sQ5_spl
| ~ sQ15_spl
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f615,f481]) ).
fof(f617,plain,
( ~ sQ5_spl
| ~ sQ15_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f616,f574,f577,f457]) ).
fof(f619,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(f621,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)],[f619]) ).
fof(f622,plain,
( ~ sQ6_spl
| ~ sQ0_spl
| rearsegP(nil,sK49_skl) ),
inference(forward_demodulation,[status(thm)],[f610,f462]) ).
fof(f623,plain,
( ~ sQ6_spl
| ~ sQ0_spl
| rearsegP(nil,sK47_skl) ),
inference(forward_demodulation,[status(thm)],[f425,f622]) ).
fof(f625,plain,
( ~ sQ6_spl
| ~ sQ0_spl
| sK47_skl = nil
| ~ rearsegP(sK47_skl,nil)
| ~ ssList(nil)
| ~ ssList(sK47_skl) ),
inference(resolution,[status(thm)],[f623,f303]) ).
fof(f631,definition,
( sQ17_spl
<=> rearsegP(sK47_skl,nil) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f632,plain,
( ~ sQ17_spl
| rearsegP(sK47_skl,nil) ),
inference(component_clause,[status(thm)],[f631]) ).
fof(f633,plain,
( sQ17_spl
| ~ rearsegP(sK47_skl,nil) ),
inference(component_clause,[status(thm)],[f631]) ).
fof(f634,plain,
( ~ sQ6_spl
| ~ sQ0_spl
| sQ15_spl
| ~ sQ17_spl
| ~ sQ14_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f625,f571,f574,f631,f577,f440,f461]) ).
fof(f647,plain,
! [X0,X1,X2] :
( app(sK6_skl(X1,app(X2,X0)),X1) = app(X2,X0)
| ~ ssList(X1)
| ~ ssList(app(X2,X0))
| ~ rearsegP(X0,X1)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f307,f129]) ).
fof(f648,plain,
! [X0,X1,X2] :
( X1 = app(X2,X0)
| ~ rearsegP(X1,app(X2,X0))
| ~ ssList(app(X2,X0))
| ~ ssList(X1)
| ~ rearsegP(X0,X1)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f307,f303]) ).
fof(f649,plain,
! [X0,X1,X2,X3] :
( rearsegP(X3,X1)
| ~ rearsegP(X3,app(X2,X0))
| ~ ssList(X1)
| ~ ssList(app(X2,X0))
| ~ ssList(X3)
| ~ rearsegP(X0,X1)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f307,f301]) ).
fof(f650,plain,
! [X0,X1,X2] :
( app(sK6_skl(X1,app(X2,X0)),X1) = app(X2,X0)
| ~ ssList(app(X2,X0))
| ~ rearsegP(X0,X1)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f647]) ).
fof(f651,plain,
! [X0,X1,X2] :
( X1 = app(X2,X0)
| ~ rearsegP(X1,app(X2,X0))
| ~ ssList(app(X2,X0))
| ~ rearsegP(X0,X1)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f648]) ).
fof(f652,plain,
! [X0,X1,X2,X3] :
( rearsegP(X3,X1)
| ~ rearsegP(X3,app(X2,X0))
| ~ ssList(app(X2,X0))
| ~ ssList(X3)
| ~ rearsegP(X0,X1)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f649]) ).
fof(f653,plain,
( sQ17_spl
| ~ ssList(sK47_skl) ),
inference(resolution,[status(thm)],[f309,f633]) ).
fof(f654,plain,
! [X0] :
( app(sK6_skl(nil,X0),nil) = X0
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f309,f129]) ).
fof(f655,plain,
! [X0] :
( nil = X0
| ~ rearsegP(nil,X0)
| ~ ssList(X0)
| ~ ssList(nil)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f309,f303]) ).
fof(f656,plain,
! [X0,X1] :
( rearsegP(X1,nil)
| ~ rearsegP(X1,X0)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f309,f301]) ).
fof(f657,plain,
( sQ17_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f653,f571,f631]) ).
fof(f658,definition,
! [X0] :
( sQ20_spl
<=> ( app(sK6_skl(nil,X0),nil) = X0
| ~ ssList(X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f661,plain,
( ~ sQ14_spl
| sQ20_spl ),
inference(split_clause,[status(thm)],[f654,f658,f574]) ).
fof(f662,definition,
! [X0] :
( sQ21_spl
<=> ( nil = X0
| ~ rearsegP(nil,X0)
| ~ ssList(X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f665,plain,
( ~ sQ14_spl
| sQ21_spl ),
inference(split_clause,[status(thm)],[f655,f662,f574]) ).
fof(f666,definition,
! [X0,X1] :
( sQ22_spl
<=> ( rearsegP(X1,nil)
| ~ rearsegP(X1,X0)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f669,plain,
( ~ sQ14_spl
| sQ22_spl ),
inference(split_clause,[status(thm)],[f656,f666,f574]) ).
fof(f673,plain,
( ~ sQ17_spl
| app(sK6_skl(nil,sK47_skl),nil) = sK47_skl
| ~ ssList(nil)
| ~ ssList(sK47_skl) ),
inference(resolution,[status(thm)],[f632,f129]) ).
fof(f675,plain,
! [X0] :
( ~ sQ17_spl
| rearsegP(X0,nil)
| ~ rearsegP(X0,sK47_skl)
| ~ ssList(nil)
| ~ ssList(sK47_skl)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f632,f301]) ).
fof(f676,definition,
( sQ23_spl
<=> app(sK6_skl(nil,sK47_skl),nil) = sK47_skl ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f677,plain,
( ~ sQ23_spl
| app(sK6_skl(nil,sK47_skl),nil) = sK47_skl ),
inference(component_clause,[status(thm)],[f676]) ).
fof(f679,plain,
( ~ sQ17_spl
| sQ23_spl
| ~ sQ14_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f673,f571,f574,f676,f631]) ).
fof(f684,definition,
! [X0] :
( sQ25_spl
<=> ( rearsegP(X0,nil)
| ~ rearsegP(X0,sK47_skl)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f687,plain,
( ~ sQ17_spl
| ~ sQ14_spl
| ~ sQ13_spl
| sQ25_spl ),
inference(split_clause,[status(thm)],[f675,f684,f571,f574,f631]) ).
fof(f688,plain,
( ~ sQ4_spl
| nil = sK47_skl ),
inference(resolution,[status(thm)],[f501,f438]) ).
fof(f690,plain,
( ~ sQ4_spl
| sQ15_spl ),
inference(split_clause,[status(thm)],[f688,f577,f454]) ).
fof(f691,plain,
( ~ sQ6_spl
| rearsegP(sK48_skl,sK49_skl) ),
inference(forward_demodulation,[status(thm)],[f424,f462]) ).
fof(f692,plain,
( ~ sQ6_spl
| rearsegP(sK48_skl,sK47_skl) ),
inference(forward_demodulation,[status(thm)],[f425,f691]) ).
fof(f700,plain,
( ~ sQ6_spl
| app(sK6_skl(sK47_skl,sK48_skl),sK47_skl) = sK48_skl
| ~ ssList(sK47_skl)
| ~ ssList(sK48_skl) ),
inference(resolution,[status(thm)],[f692,f129]) ).
fof(f703,definition,
( sQ27_spl
<=> ssList(sK48_skl) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f705,plain,
( sQ27_spl
| ~ ssList(sK48_skl) ),
inference(component_clause,[status(thm)],[f703]) ).
fof(f706,definition,
( sQ28_spl
<=> app(sK6_skl(sK47_skl,sK48_skl),sK47_skl) = sK48_skl ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f707,plain,
( ~ sQ28_spl
| app(sK6_skl(sK47_skl,sK48_skl),sK47_skl) = sK48_skl ),
inference(component_clause,[status(thm)],[f706]) ).
fof(f709,plain,
( ~ sQ6_spl
| sQ28_spl
| ~ sQ13_spl
| ~ sQ27_spl ),
inference(split_clause,[status(thm)],[f700,f703,f571,f706,f461]) ).
fof(f721,plain,
( sQ27_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f705,f421]) ).
fof(f722,plain,
sQ27_spl,
inference(contradiction_clause,[status(thm)],[f721]) ).
fof(f725,plain,
! [X0] :
( ~ sQ28_spl
| ~ ssList(X0)
| ~ ssList(sK6_skl(sK47_skl,sK48_skl))
| segmentP(app(app(sK6_skl(sK47_skl,sK48_skl),sK47_skl),X0),sK47_skl)
| ~ ssList(sK47_skl)
| ~ ssList(app(sK48_skl,X0)) ),
inference(paramodulation,[status(thm)],[f707,f471]) ).
fof(f730,definition,
( sQ33_spl
<=> ssList(sK6_skl(sK47_skl,sK48_skl)) ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f732,plain,
( sQ33_spl
| ~ ssList(sK6_skl(sK47_skl,sK48_skl)) ),
inference(component_clause,[status(thm)],[f730]) ).
fof(f738,definition,
! [X0] :
( sQ35_spl
<=> ( ~ ssList(X0)
| segmentP(app(app(sK6_skl(sK47_skl,sK48_skl),sK47_skl),X0),sK47_skl)
| ~ ssList(app(sK48_skl,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f739,plain,
! [X0] :
( ~ sQ35_spl
| ~ ssList(X0)
| segmentP(app(app(sK6_skl(sK47_skl,sK48_skl),sK47_skl),X0),sK47_skl)
| ~ ssList(app(sK48_skl,X0)) ),
inference(component_clause,[status(thm)],[f738]) ).
fof(f741,plain,
( ~ sQ28_spl
| ~ sQ33_spl
| ~ sQ13_spl
| sQ35_spl ),
inference(split_clause,[status(thm)],[f725,f738,f571,f730,f706]) ).
fof(f763,definition,
( sQ38_spl
<=> app(sK6_skl(sK47_skl,sK47_skl),sK47_skl) = sK47_skl ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f764,plain,
( ~ sQ38_spl
| app(sK6_skl(sK47_skl,sK47_skl),sK47_skl) = sK47_skl ),
inference(component_clause,[status(thm)],[f763]) ).
fof(f767,definition,
( sQ39_spl
<=> rearsegP(sK47_skl,sK47_skl) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f769,plain,
( sQ39_spl
| ~ rearsegP(sK47_skl,sK47_skl) ),
inference(component_clause,[status(thm)],[f767]) ).
fof(f770,definition,
( sQ40_spl
<=> sK47_skl = sK47_skl ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f774,definition,
! [X0] :
( sQ41_spl
<=> ( rearsegP(X0,sK47_skl)
| ~ rearsegP(X0,sK47_skl)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition]) ).
fof(f782,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(f785,definition,
! [X0,X1] :
( sQ42_spl
<=> ( ~ rearsegP(X1,X0)
| ~ rearsegP(nil,X1)
| ~ ssList(X0)
| ~ ssList(X1)
| nil = X0
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f786,plain,
! [X0,X1] :
( ~ sQ42_spl
| ~ rearsegP(X1,X0)
| ~ rearsegP(nil,X1)
| ~ ssList(X0)
| ~ ssList(X1)
| nil = X0
| ~ ssList(X0) ),
inference(component_clause,[status(thm)],[f785]) ).
fof(f788,plain,
( ~ sQ14_spl
| sQ42_spl ),
inference(split_clause,[status(thm)],[f782,f785,f574]) ).
fof(f789,plain,
! [X0,X1] :
( ~ sQ42_spl
| ~ rearsegP(X1,X0)
| ~ rearsegP(nil,X1)
| ~ ssList(X1)
| nil = X0
| ~ ssList(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f786]) ).
fof(f804,plain,
( sQ33_spl
| ~ rearsegP(sK48_skl,sK47_skl)
| ~ ssList(sK47_skl)
| ~ ssList(sK48_skl) ),
inference(resolution,[status(thm)],[f732,f128]) ).
fof(f805,definition,
( sQ43_spl
<=> rearsegP(sK48_skl,sK47_skl) ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f807,plain,
( sQ43_spl
| ~ rearsegP(sK48_skl,sK47_skl) ),
inference(component_clause,[status(thm)],[f805]) ).
fof(f808,plain,
( sQ33_spl
| ~ sQ43_spl
| ~ sQ13_spl
| ~ sQ27_spl ),
inference(split_clause,[status(thm)],[f804,f703,f571,f805,f730]) ).
fof(f809,plain,
( sQ43_spl
| ~ sQ6_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f807,f692]) ).
fof(f810,plain,
( sQ43_spl
| ~ sQ6_spl ),
inference(contradiction_clause,[status(thm)],[f809]) ).
fof(f824,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(f825,definition,
! [X0] :
( sQ46_spl
<=> ( app(app(sK7_skl(nil,X0),nil),sK8_skl(nil,X0)) = X0
| ~ ssList(X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition]) ).
fof(f828,plain,
( ~ sQ14_spl
| sQ46_spl ),
inference(split_clause,[status(thm)],[f824,f825,f574]) ).
fof(f848,plain,
! [X0,X1] :
( ~ ssList(X1)
| segmentP(X0,nil)
| ~ segmentP(X0,X1)
| ~ ssList(nil)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f315,f323]) ).
fof(f850,definition,
! [X0,X1] :
( sQ49_spl
<=> ( ~ ssList(X1)
| segmentP(X0,nil)
| ~ segmentP(X0,X1)
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition]) ).
fof(f853,plain,
( ~ sQ14_spl
| sQ49_spl ),
inference(split_clause,[status(thm)],[f848,f850,f574]) ).
fof(f855,plain,
! [X0] :
( ~ ssList(X0)
| nil = X0
| ~ segmentP(nil,X0)
| ~ ssList(X0)
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f317,f323]) ).
fof(f857,definition,
! [X0] :
( sQ50_spl
<=> ( ~ ssList(X0)
| nil = X0
| ~ segmentP(nil,X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition]) ).
fof(f860,plain,
( sQ50_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f855,f574,f857]) ).
fof(f862,plain,
! [X0] :
( app(nil,sK5_skl(nil,X0)) = X0
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f295,f123]) ).
fof(f863,definition,
! [X0] :
( sQ51_spl
<=> ( app(nil,sK5_skl(nil,X0)) = X0
| ~ ssList(X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f866,plain,
( ~ sQ14_spl
| sQ51_spl ),
inference(split_clause,[status(thm)],[f862,f863,f574]) ).
fof(f868,plain,
app(nil,sK48_skl) = sK48_skl,
inference(resolution,[status(thm)],[f249,f421]) ).
fof(f871,plain,
app(nil,sK47_skl) = sK47_skl,
inference(resolution,[status(thm)],[f249,f420]) ).
fof(f877,plain,
app(nil,nil) = nil,
inference(resolution,[status(thm)],[f249,f223]) ).
fof(f878,plain,
! [X0] :
( rearsegP(sK48_skl,X0)
| ~ rearsegP(sK48_skl,X0)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(sK48_skl) ),
inference(paramodulation,[status(thm)],[f868,f307]) ).
fof(f879,plain,
( ~ ssList(sK48_skl)
| frontsegP(app(nil,sK48_skl),nil)
| ~ ssList(nil)
| ~ ssList(sK48_skl) ),
inference(paramodulation,[status(thm)],[f868,f469]) ).
fof(f880,plain,
! [X0] :
( ~ ssList(X0)
| ~ ssList(nil)
| segmentP(app(app(nil,sK48_skl),X0),sK48_skl)
| ~ ssList(sK48_skl)
| ~ ssList(app(sK48_skl,X0)) ),
inference(paramodulation,[status(thm)],[f868,f471]) ).
fof(f881,plain,
( ~ ssList(nil)
| rearsegP(app(nil,sK48_skl),sK48_skl)
| ~ ssList(sK48_skl)
| ~ ssList(sK48_skl) ),
inference(paramodulation,[status(thm)],[f868,f470]) ).
fof(f882,definition,
! [X0] :
( sQ52_spl
<=> ( rearsegP(sK48_skl,X0)
| ~ rearsegP(sK48_skl,X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition]) ).
fof(f885,plain,
( ~ sQ14_spl
| sQ52_spl
| ~ sQ27_spl ),
inference(split_clause,[status(thm)],[f878,f703,f882,f574]) ).
fof(f886,definition,
( sQ53_spl
<=> frontsegP(app(nil,sK48_skl),nil) ),
introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition]) ).
fof(f887,plain,
( ~ sQ53_spl
| frontsegP(app(nil,sK48_skl),nil) ),
inference(component_clause,[status(thm)],[f886]) ).
fof(f889,plain,
( sQ53_spl
| ~ sQ14_spl
| ~ sQ27_spl ),
inference(split_clause,[status(thm)],[f879,f703,f574,f886]) ).
fof(f890,definition,
! [X0] :
( sQ54_spl
<=> ( ~ ssList(X0)
| segmentP(app(app(nil,sK48_skl),X0),sK48_skl)
| ~ ssList(app(sK48_skl,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition]) ).
fof(f893,plain,
( ~ sQ14_spl
| ~ sQ27_spl
| sQ54_spl ),
inference(split_clause,[status(thm)],[f880,f890,f703,f574]) ).
fof(f894,definition,
( sQ55_spl
<=> rearsegP(app(nil,sK48_skl),sK48_skl) ),
introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition]) ).
fof(f895,plain,
( ~ sQ55_spl
| rearsegP(app(nil,sK48_skl),sK48_skl) ),
inference(component_clause,[status(thm)],[f894]) ).
fof(f897,plain,
( ~ sQ14_spl
| sQ55_spl
| ~ sQ27_spl ),
inference(split_clause,[status(thm)],[f881,f703,f894,f574]) ).
fof(f898,plain,
( ~ sQ53_spl
| frontsegP(sK48_skl,nil) ),
inference(forward_demodulation,[status(thm)],[f868,f887]) ).
fof(f900,plain,
( ~ sQ55_spl
| rearsegP(sK48_skl,sK48_skl) ),
inference(forward_demodulation,[status(thm)],[f868,f895]) ).
fof(f901,plain,
( ~ sQ53_spl
| app(nil,sK5_skl(nil,sK48_skl)) = sK48_skl
| ~ ssList(nil)
| ~ ssList(sK48_skl) ),
inference(resolution,[status(thm)],[f898,f123]) ).
fof(f902,definition,
( sQ56_spl
<=> app(nil,sK5_skl(nil,sK48_skl)) = sK48_skl ),
introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition]) ).
fof(f903,plain,
( ~ sQ56_spl
| app(nil,sK5_skl(nil,sK48_skl)) = sK48_skl ),
inference(component_clause,[status(thm)],[f902]) ).
fof(f905,plain,
( ~ sQ53_spl
| sQ56_spl
| ~ sQ14_spl
| ~ sQ27_spl ),
inference(split_clause,[status(thm)],[f901,f703,f574,f902,f886]) ).
fof(f907,plain,
( ~ sQ55_spl
| app(sK6_skl(sK48_skl,sK48_skl),sK48_skl) = sK48_skl
| ~ ssList(sK48_skl)
| ~ ssList(sK48_skl) ),
inference(resolution,[status(thm)],[f900,f129]) ).
fof(f908,plain,
( ~ sQ55_spl
| sK48_skl = sK48_skl
| ~ rearsegP(sK48_skl,sK48_skl)
| ~ ssList(sK48_skl)
| ~ ssList(sK48_skl) ),
inference(resolution,[status(thm)],[f900,f303]) ).
fof(f909,plain,
! [X0] :
( ~ sQ55_spl
| rearsegP(X0,sK48_skl)
| ~ rearsegP(X0,sK48_skl)
| ~ ssList(sK48_skl)
| ~ ssList(sK48_skl)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f900,f301]) ).
fof(f911,definition,
( sQ57_spl
<=> app(sK6_skl(sK48_skl,sK48_skl),sK48_skl) = sK48_skl ),
introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition]) ).
fof(f912,plain,
( ~ sQ57_spl
| app(sK6_skl(sK48_skl,sK48_skl),sK48_skl) = sK48_skl ),
inference(component_clause,[status(thm)],[f911]) ).
fof(f914,plain,
( ~ sQ55_spl
| sQ57_spl
| ~ sQ27_spl ),
inference(split_clause,[status(thm)],[f907,f703,f911,f894]) ).
fof(f915,definition,
( sQ58_spl
<=> rearsegP(sK48_skl,sK48_skl) ),
introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition]) ).
fof(f917,plain,
( sQ58_spl
| ~ rearsegP(sK48_skl,sK48_skl) ),
inference(component_clause,[status(thm)],[f915]) ).
fof(f918,definition,
( sQ59_spl
<=> sK48_skl = sK48_skl ),
introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition]) ).
fof(f921,plain,
( ~ sQ55_spl
| sQ59_spl
| ~ sQ58_spl
| ~ sQ27_spl ),
inference(split_clause,[status(thm)],[f908,f703,f915,f918,f894]) ).
fof(f922,definition,
! [X0] :
( sQ60_spl
<=> ( rearsegP(X0,sK48_skl)
| ~ rearsegP(X0,sK48_skl)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition]) ).
fof(f925,plain,
( ~ sQ55_spl
| ~ sQ27_spl
| sQ60_spl ),
inference(split_clause,[status(thm)],[f909,f922,f703,f894]) ).
fof(f926,plain,
( sQ58_spl
| ~ sQ55_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f917,f900]) ).
fof(f927,plain,
( sQ58_spl
| ~ sQ55_spl ),
inference(contradiction_clause,[status(thm)],[f926]) ).
fof(f931,plain,
! [X0] :
( rearsegP(sK47_skl,X0)
| ~ rearsegP(sK47_skl,X0)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(sK47_skl) ),
inference(paramodulation,[status(thm)],[f871,f307]) ).
fof(f932,plain,
( ~ ssList(sK47_skl)
| frontsegP(app(nil,sK47_skl),nil)
| ~ ssList(nil)
| ~ ssList(sK47_skl) ),
inference(paramodulation,[status(thm)],[f871,f469]) ).
fof(f933,plain,
! [X0] :
( ~ ssList(X0)
| ~ ssList(nil)
| segmentP(app(app(nil,sK47_skl),X0),sK47_skl)
| ~ ssList(sK47_skl)
| ~ ssList(app(sK47_skl,X0)) ),
inference(paramodulation,[status(thm)],[f871,f471]) ).
fof(f934,plain,
( ~ ssList(nil)
| rearsegP(app(nil,sK47_skl),sK47_skl)
| ~ ssList(sK47_skl)
| ~ ssList(sK47_skl) ),
inference(paramodulation,[status(thm)],[f871,f470]) ).
fof(f935,definition,
! [X0] :
( sQ61_spl
<=> ( rearsegP(sK47_skl,X0)
| ~ rearsegP(sK47_skl,X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition]) ).
fof(f938,plain,
( ~ sQ14_spl
| sQ61_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f931,f571,f935,f574]) ).
fof(f939,definition,
( sQ62_spl
<=> frontsegP(app(nil,sK47_skl),nil) ),
introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition]) ).
fof(f940,plain,
( ~ sQ62_spl
| frontsegP(app(nil,sK47_skl),nil) ),
inference(component_clause,[status(thm)],[f939]) ).
fof(f942,plain,
( sQ62_spl
| ~ sQ14_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f932,f571,f574,f939]) ).
fof(f943,definition,
! [X0] :
( sQ63_spl
<=> ( ~ ssList(X0)
| segmentP(app(app(nil,sK47_skl),X0),sK47_skl)
| ~ ssList(app(sK47_skl,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition]) ).
fof(f946,plain,
( ~ sQ14_spl
| ~ sQ13_spl
| sQ63_spl ),
inference(split_clause,[status(thm)],[f933,f943,f571,f574]) ).
fof(f947,definition,
( sQ64_spl
<=> rearsegP(app(nil,sK47_skl),sK47_skl) ),
introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition]) ).
fof(f948,plain,
( ~ sQ64_spl
| rearsegP(app(nil,sK47_skl),sK47_skl) ),
inference(component_clause,[status(thm)],[f947]) ).
fof(f950,plain,
( ~ sQ14_spl
| sQ64_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f934,f571,f947,f574]) ).
fof(f951,plain,
( ~ sQ62_spl
| frontsegP(sK47_skl,nil) ),
inference(forward_demodulation,[status(thm)],[f871,f940]) ).
fof(f953,plain,
( ~ sQ64_spl
| rearsegP(sK47_skl,sK47_skl) ),
inference(forward_demodulation,[status(thm)],[f871,f948]) ).
fof(f954,plain,
( ~ sQ62_spl
| app(nil,sK5_skl(nil,sK47_skl)) = sK47_skl
| ~ ssList(nil)
| ~ ssList(sK47_skl) ),
inference(resolution,[status(thm)],[f951,f123]) ).
fof(f955,definition,
( sQ65_spl
<=> app(nil,sK5_skl(nil,sK47_skl)) = sK47_skl ),
introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition]) ).
fof(f956,plain,
( ~ sQ65_spl
| app(nil,sK5_skl(nil,sK47_skl)) = sK47_skl ),
inference(component_clause,[status(thm)],[f955]) ).
fof(f958,plain,
( ~ sQ62_spl
| sQ65_spl
| ~ sQ14_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f954,f571,f574,f955,f939]) ).
fof(f959,plain,
( ~ sQ64_spl
| app(sK6_skl(sK47_skl,sK47_skl),sK47_skl) = sK47_skl
| ~ ssList(sK47_skl)
| ~ ssList(sK47_skl) ),
inference(resolution,[status(thm)],[f953,f129]) ).
fof(f960,plain,
( ~ sQ64_spl
| sK47_skl = sK47_skl
| ~ rearsegP(sK47_skl,sK47_skl)
| ~ ssList(sK47_skl)
| ~ ssList(sK47_skl) ),
inference(resolution,[status(thm)],[f953,f303]) ).
fof(f961,plain,
! [X0] :
( ~ sQ64_spl
| rearsegP(X0,sK47_skl)
| ~ rearsegP(X0,sK47_skl)
| ~ ssList(sK47_skl)
| ~ ssList(sK47_skl)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f953,f301]) ).
fof(f962,plain,
( ~ sQ64_spl
| sQ38_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f959,f571,f763,f947]) ).
fof(f963,plain,
( ~ sQ64_spl
| sQ40_spl
| ~ sQ39_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f960,f571,f767,f770,f947]) ).
fof(f964,plain,
( ~ sQ64_spl
| ~ sQ13_spl
| sQ41_spl ),
inference(split_clause,[status(thm)],[f961,f774,f571,f947]) ).
fof(f973,plain,
! [X0] :
( rearsegP(nil,X0)
| ~ rearsegP(nil,X0)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f877,f307]) ).
fof(f974,plain,
( ~ ssList(nil)
| frontsegP(app(nil,nil),nil)
| ~ ssList(nil)
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f877,f469]) ).
fof(f975,plain,
! [X0] :
( ~ ssList(X0)
| ~ ssList(nil)
| segmentP(app(app(nil,nil),X0),nil)
| ~ ssList(nil)
| ~ ssList(app(nil,X0)) ),
inference(paramodulation,[status(thm)],[f877,f471]) ).
fof(f976,plain,
( ~ ssList(nil)
| rearsegP(app(nil,nil),nil)
| ~ ssList(nil)
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f877,f470]) ).
fof(f977,definition,
! [X0] :
( sQ66_spl
<=> ( rearsegP(nil,X0)
| ~ rearsegP(nil,X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition]) ).
fof(f980,plain,
( sQ66_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f973,f574,f977]) ).
fof(f981,definition,
( sQ67_spl
<=> frontsegP(app(nil,nil),nil) ),
introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition]) ).
fof(f982,plain,
( ~ sQ67_spl
| frontsegP(app(nil,nil),nil) ),
inference(component_clause,[status(thm)],[f981]) ).
fof(f984,plain,
( sQ67_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f974,f574,f981]) ).
fof(f985,definition,
! [X0] :
( sQ68_spl
<=> ( ~ ssList(X0)
| segmentP(app(app(nil,nil),X0),nil)
| ~ ssList(app(nil,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition]) ).
fof(f988,plain,
( ~ sQ14_spl
| sQ68_spl ),
inference(split_clause,[status(thm)],[f975,f985,f574]) ).
fof(f989,definition,
( sQ69_spl
<=> rearsegP(app(nil,nil),nil) ),
introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition]) ).
fof(f990,plain,
( ~ sQ69_spl
| rearsegP(app(nil,nil),nil) ),
inference(component_clause,[status(thm)],[f989]) ).
fof(f992,plain,
( sQ69_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f976,f574,f989]) ).
fof(f993,plain,
( ~ sQ67_spl
| frontsegP(nil,nil) ),
inference(forward_demodulation,[status(thm)],[f877,f982]) ).
fof(f995,plain,
( ~ sQ69_spl
| rearsegP(nil,nil) ),
inference(forward_demodulation,[status(thm)],[f877,f990]) ).
fof(f996,plain,
( ~ sQ67_spl
| app(nil,sK5_skl(nil,nil)) = nil
| ~ ssList(nil)
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f993,f123]) ).
fof(f997,definition,
( sQ70_spl
<=> app(nil,sK5_skl(nil,nil)) = nil ),
introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition]) ).
fof(f998,plain,
( ~ sQ70_spl
| app(nil,sK5_skl(nil,nil)) = nil ),
inference(component_clause,[status(thm)],[f997]) ).
fof(f1000,plain,
( ~ sQ67_spl
| sQ70_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f996,f574,f997,f981]) ).
fof(f1002,plain,
( ~ sQ69_spl
| app(sK6_skl(nil,nil),nil) = nil
| ~ ssList(nil)
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f995,f129]) ).
fof(f1004,plain,
! [X0] :
( ~ sQ69_spl
| rearsegP(X0,nil)
| ~ rearsegP(X0,nil)
| ~ ssList(nil)
| ~ ssList(nil)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f995,f301]) ).
fof(f1006,definition,
( sQ71_spl
<=> app(sK6_skl(nil,nil),nil) = nil ),
introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition]) ).
fof(f1007,plain,
( ~ sQ71_spl
| app(sK6_skl(nil,nil),nil) = nil ),
inference(component_clause,[status(thm)],[f1006]) ).
fof(f1009,plain,
( ~ sQ69_spl
| sQ71_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f1002,f574,f1006,f989]) ).
fof(f1010,definition,
( sQ72_spl
<=> rearsegP(nil,nil) ),
introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition]) ).
fof(f1012,plain,
( sQ72_spl
| ~ rearsegP(nil,nil) ),
inference(component_clause,[status(thm)],[f1010]) ).
fof(f1014,definition,
! [X0] :
( sQ73_spl
<=> ( rearsegP(X0,nil)
| ~ rearsegP(X0,nil)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition]) ).
fof(f1017,plain,
( ~ sQ69_spl
| ~ sQ14_spl
| sQ73_spl ),
inference(split_clause,[status(thm)],[f1004,f1014,f574,f989]) ).
fof(f1036,plain,
! [X0,X1,X2] :
( ~ ssList(X0)
| segmentP(app(app(X1,X0),X2),nil)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(nil)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f321,f323]) ).
fof(f1038,definition,
! [X0,X1,X2] :
( sQ74_spl
<=> ( ~ ssList(X0)
| segmentP(app(app(X1,X0),X2),nil)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition]) ).
fof(f1041,plain,
( ~ sQ14_spl
| sQ74_spl ),
inference(split_clause,[status(thm)],[f1036,f1038,f574]) ).
fof(f1046,plain,
! [X0,X1,X2] :
( nil = X1
| ~ ssList(X1)
| ~ rearsegP(X2,X1)
| ~ rearsegP(X0,X2)
| ~ ssList(X2)
| ~ rearsegP(nil,X0)
| ~ ssList(X1)
| ~ ssList(X0)
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f568,f312]) ).
fof(f1059,definition,
! [X0,X1,X2] :
( sQ77_spl
<=> ( nil = X1
| ~ ssList(X1)
| ~ rearsegP(X2,X1)
| ~ rearsegP(X0,X2)
| ~ ssList(X2)
| ~ rearsegP(nil,X0)
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition]) ).
fof(f1062,plain,
( sQ77_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f1046,f574,f1059]) ).
fof(f1075,plain,
app(sK48_skl,nil) = sK48_skl,
inference(resolution,[status(thm)],[f389,f421]) ).
fof(f1078,plain,
app(sK47_skl,nil) = sK47_skl,
inference(resolution,[status(thm)],[f389,f420]) ).
fof(f1085,plain,
! [X0] :
( rearsegP(sK48_skl,X0)
| ~ rearsegP(nil,X0)
| ~ ssList(sK48_skl)
| ~ ssList(X0)
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f1075,f307]) ).
fof(f1086,plain,
( ~ ssList(nil)
| frontsegP(app(sK48_skl,nil),sK48_skl)
| ~ ssList(sK48_skl)
| ~ ssList(sK48_skl) ),
inference(paramodulation,[status(thm)],[f1075,f469]) ).
fof(f1087,plain,
! [X0] :
( ~ ssList(X0)
| ~ ssList(sK48_skl)
| segmentP(app(app(sK48_skl,nil),X0),nil)
| ~ ssList(nil)
| ~ ssList(app(sK48_skl,X0)) ),
inference(paramodulation,[status(thm)],[f1075,f471]) ).
fof(f1088,plain,
( ~ ssList(sK48_skl)
| rearsegP(app(sK48_skl,nil),nil)
| ~ ssList(nil)
| ~ ssList(sK48_skl) ),
inference(paramodulation,[status(thm)],[f1075,f470]) ).
fof(f1089,definition,
! [X0] :
( sQ79_spl
<=> ( rearsegP(sK48_skl,X0)
| ~ rearsegP(nil,X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition]) ).
fof(f1092,plain,
( ~ sQ27_spl
| sQ79_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f1085,f574,f1089,f703]) ).
fof(f1093,definition,
( sQ80_spl
<=> frontsegP(app(sK48_skl,nil),sK48_skl) ),
introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition]) ).
fof(f1094,plain,
( ~ sQ80_spl
| frontsegP(app(sK48_skl,nil),sK48_skl) ),
inference(component_clause,[status(thm)],[f1093]) ).
fof(f1096,plain,
( ~ sQ14_spl
| sQ80_spl
| ~ sQ27_spl ),
inference(split_clause,[status(thm)],[f1086,f703,f1093,f574]) ).
fof(f1097,definition,
! [X0] :
( sQ81_spl
<=> ( ~ ssList(X0)
| segmentP(app(app(sK48_skl,nil),X0),nil)
| ~ ssList(app(sK48_skl,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition]) ).
fof(f1100,plain,
( ~ sQ27_spl
| ~ sQ14_spl
| sQ81_spl ),
inference(split_clause,[status(thm)],[f1087,f1097,f574,f703]) ).
fof(f1101,definition,
( sQ82_spl
<=> rearsegP(app(sK48_skl,nil),nil) ),
introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition]) ).
fof(f1102,plain,
( ~ sQ82_spl
| rearsegP(app(sK48_skl,nil),nil) ),
inference(component_clause,[status(thm)],[f1101]) ).
fof(f1104,plain,
( sQ82_spl
| ~ sQ14_spl
| ~ sQ27_spl ),
inference(split_clause,[status(thm)],[f1088,f703,f574,f1101]) ).
fof(f1105,plain,
( ~ sQ80_spl
| frontsegP(sK48_skl,sK48_skl) ),
inference(forward_demodulation,[status(thm)],[f1075,f1094]) ).
fof(f1107,plain,
( ~ sQ82_spl
| rearsegP(sK48_skl,nil) ),
inference(forward_demodulation,[status(thm)],[f1075,f1102]) ).
fof(f1108,plain,
( ~ sQ80_spl
| app(sK48_skl,sK5_skl(sK48_skl,sK48_skl)) = sK48_skl
| ~ ssList(sK48_skl)
| ~ ssList(sK48_skl) ),
inference(resolution,[status(thm)],[f1105,f123]) ).
fof(f1109,definition,
( sQ83_spl
<=> app(sK48_skl,sK5_skl(sK48_skl,sK48_skl)) = sK48_skl ),
introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition]) ).
fof(f1110,plain,
( ~ sQ83_spl
| app(sK48_skl,sK5_skl(sK48_skl,sK48_skl)) = sK48_skl ),
inference(component_clause,[status(thm)],[f1109]) ).
fof(f1112,plain,
( ~ sQ80_spl
| sQ83_spl
| ~ sQ27_spl ),
inference(split_clause,[status(thm)],[f1108,f703,f1109,f1093]) ).
fof(f1113,plain,
( ~ sQ82_spl
| app(sK6_skl(nil,sK48_skl),nil) = sK48_skl
| ~ ssList(nil)
| ~ ssList(sK48_skl) ),
inference(resolution,[status(thm)],[f1107,f129]) ).
fof(f1115,plain,
! [X0] :
( ~ sQ82_spl
| rearsegP(X0,nil)
| ~ rearsegP(X0,sK48_skl)
| ~ ssList(nil)
| ~ ssList(sK48_skl)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f1107,f301]) ).
fof(f1116,definition,
( sQ84_spl
<=> app(sK6_skl(nil,sK48_skl),nil) = sK48_skl ),
introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition]) ).
fof(f1119,plain,
( ~ sQ82_spl
| sQ84_spl
| ~ sQ14_spl
| ~ sQ27_spl ),
inference(split_clause,[status(thm)],[f1113,f703,f574,f1116,f1101]) ).
fof(f1127,definition,
! [X0] :
( sQ87_spl
<=> ( rearsegP(X0,nil)
| ~ rearsegP(X0,sK48_skl)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition]) ).
fof(f1130,plain,
( ~ sQ82_spl
| ~ sQ14_spl
| ~ sQ27_spl
| sQ87_spl ),
inference(split_clause,[status(thm)],[f1115,f1127,f703,f574,f1101]) ).
fof(f1141,plain,
! [X0] :
( rearsegP(sK47_skl,X0)
| ~ rearsegP(nil,X0)
| ~ ssList(sK47_skl)
| ~ ssList(X0)
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f1078,f307]) ).
fof(f1142,plain,
( ~ ssList(nil)
| frontsegP(app(sK47_skl,nil),sK47_skl)
| ~ ssList(sK47_skl)
| ~ ssList(sK47_skl) ),
inference(paramodulation,[status(thm)],[f1078,f469]) ).
fof(f1143,plain,
! [X0] :
( ~ ssList(X0)
| ~ ssList(sK47_skl)
| segmentP(app(app(sK47_skl,nil),X0),nil)
| ~ ssList(nil)
| ~ ssList(app(sK47_skl,X0)) ),
inference(paramodulation,[status(thm)],[f1078,f471]) ).
fof(f1144,plain,
( ~ ssList(sK47_skl)
| rearsegP(app(sK47_skl,nil),nil)
| ~ ssList(nil)
| ~ ssList(sK47_skl) ),
inference(paramodulation,[status(thm)],[f1078,f470]) ).
fof(f1145,definition,
! [X0] :
( sQ90_spl
<=> ( rearsegP(sK47_skl,X0)
| ~ rearsegP(nil,X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition]) ).
fof(f1148,plain,
( ~ sQ13_spl
| sQ90_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f1141,f574,f1145,f571]) ).
fof(f1149,definition,
( sQ91_spl
<=> frontsegP(app(sK47_skl,nil),sK47_skl) ),
introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition]) ).
fof(f1150,plain,
( ~ sQ91_spl
| frontsegP(app(sK47_skl,nil),sK47_skl) ),
inference(component_clause,[status(thm)],[f1149]) ).
fof(f1152,plain,
( ~ sQ14_spl
| sQ91_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f1142,f571,f1149,f574]) ).
fof(f1153,definition,
! [X0] :
( sQ92_spl
<=> ( ~ ssList(X0)
| segmentP(app(app(sK47_skl,nil),X0),nil)
| ~ ssList(app(sK47_skl,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ92_spl])],[split_symbol_definition]) ).
fof(f1156,plain,
( ~ sQ13_spl
| ~ sQ14_spl
| sQ92_spl ),
inference(split_clause,[status(thm)],[f1143,f1153,f574,f571]) ).
fof(f1157,definition,
( sQ93_spl
<=> rearsegP(app(sK47_skl,nil),nil) ),
introduced(definition,[new_symbols(definition,[sQ93_spl])],[split_symbol_definition]) ).
fof(f1160,plain,
( sQ93_spl
| ~ sQ14_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f1144,f571,f574,f1157]) ).
fof(f1161,plain,
( ~ sQ91_spl
| frontsegP(sK47_skl,sK47_skl) ),
inference(forward_demodulation,[status(thm)],[f1078,f1150]) ).
fof(f1164,plain,
( ~ sQ91_spl
| app(sK47_skl,sK5_skl(sK47_skl,sK47_skl)) = sK47_skl
| ~ ssList(sK47_skl)
| ~ ssList(sK47_skl) ),
inference(resolution,[status(thm)],[f1161,f123]) ).
fof(f1165,definition,
( sQ94_spl
<=> app(sK47_skl,sK5_skl(sK47_skl,sK47_skl)) = sK47_skl ),
introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition]) ).
fof(f1166,plain,
( ~ sQ94_spl
| app(sK47_skl,sK5_skl(sK47_skl,sK47_skl)) = sK47_skl ),
inference(component_clause,[status(thm)],[f1165]) ).
fof(f1168,plain,
( ~ sQ91_spl
| sQ94_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f1164,f571,f1165,f1149]) ).
fof(f1172,plain,
( ~ sQ23_spl
| ~ ssList(nil)
| frontsegP(app(sK6_skl(nil,sK47_skl),nil),sK6_skl(nil,sK47_skl))
| ~ ssList(sK6_skl(nil,sK47_skl))
| ~ ssList(sK47_skl) ),
inference(paramodulation,[status(thm)],[f677,f469]) ).
fof(f1173,plain,
! [X0] :
( ~ sQ23_spl
| ~ ssList(X0)
| ~ ssList(sK6_skl(nil,sK47_skl))
| segmentP(app(app(sK6_skl(nil,sK47_skl),nil),X0),nil)
| ~ ssList(nil)
| ~ ssList(app(sK47_skl,X0)) ),
inference(paramodulation,[status(thm)],[f677,f471]) ).
fof(f1174,plain,
( ~ sQ23_spl
| ~ ssList(sK6_skl(nil,sK47_skl))
| rearsegP(app(sK6_skl(nil,sK47_skl),nil),nil)
| ~ ssList(nil)
| ~ ssList(sK47_skl) ),
inference(paramodulation,[status(thm)],[f677,f470]) ).
fof(f1175,definition,
( sQ95_spl
<=> ssList(sK6_skl(nil,sK47_skl)) ),
introduced(definition,[new_symbols(definition,[sQ95_spl])],[split_symbol_definition]) ).
fof(f1177,plain,
( sQ95_spl
| ~ ssList(sK6_skl(nil,sK47_skl)) ),
inference(component_clause,[status(thm)],[f1175]) ).
fof(f1179,definition,
( sQ96_spl
<=> frontsegP(app(sK6_skl(nil,sK47_skl),nil),sK6_skl(nil,sK47_skl)) ),
introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition]) ).
fof(f1182,plain,
( ~ sQ23_spl
| ~ sQ14_spl
| sQ96_spl
| ~ sQ95_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f1172,f571,f1175,f1179,f574,f676]) ).
fof(f1183,definition,
! [X0] :
( sQ97_spl
<=> ( ~ ssList(X0)
| segmentP(app(app(sK6_skl(nil,sK47_skl),nil),X0),nil)
| ~ ssList(app(sK47_skl,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ97_spl])],[split_symbol_definition]) ).
fof(f1186,plain,
( ~ sQ23_spl
| ~ sQ95_spl
| ~ sQ14_spl
| sQ97_spl ),
inference(split_clause,[status(thm)],[f1173,f1183,f574,f1175,f676]) ).
fof(f1187,definition,
( sQ98_spl
<=> rearsegP(app(sK6_skl(nil,sK47_skl),nil),nil) ),
introduced(definition,[new_symbols(definition,[sQ98_spl])],[split_symbol_definition]) ).
fof(f1190,plain,
( ~ sQ23_spl
| ~ sQ95_spl
| sQ98_spl
| ~ sQ14_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f1174,f571,f574,f1187,f1175,f676]) ).
fof(f1191,plain,
( sQ95_spl
| ~ rearsegP(sK47_skl,nil)
| ~ ssList(nil)
| ~ ssList(sK47_skl) ),
inference(resolution,[status(thm)],[f1177,f128]) ).
fof(f1192,plain,
( sQ95_spl
| ~ sQ17_spl
| ~ sQ14_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f1191,f571,f574,f631,f1175]) ).
fof(f1201,plain,
( ~ sQ38_spl
| ~ ssList(sK47_skl)
| frontsegP(app(sK6_skl(sK47_skl,sK47_skl),sK47_skl),sK6_skl(sK47_skl,sK47_skl))
| ~ ssList(sK6_skl(sK47_skl,sK47_skl))
| ~ ssList(sK47_skl) ),
inference(paramodulation,[status(thm)],[f764,f469]) ).
fof(f1202,plain,
! [X0] :
( ~ sQ38_spl
| ~ ssList(X0)
| ~ ssList(sK6_skl(sK47_skl,sK47_skl))
| segmentP(app(app(sK6_skl(sK47_skl,sK47_skl),sK47_skl),X0),sK47_skl)
| ~ ssList(sK47_skl)
| ~ ssList(app(sK47_skl,X0)) ),
inference(paramodulation,[status(thm)],[f764,f471]) ).
fof(f1203,plain,
( ~ sQ38_spl
| ~ ssList(sK6_skl(sK47_skl,sK47_skl))
| rearsegP(app(sK6_skl(sK47_skl,sK47_skl),sK47_skl),sK47_skl)
| ~ ssList(sK47_skl)
| ~ ssList(sK47_skl) ),
inference(paramodulation,[status(thm)],[f764,f470]) ).
fof(f1204,definition,
( sQ99_spl
<=> ssList(sK6_skl(sK47_skl,sK47_skl)) ),
introduced(definition,[new_symbols(definition,[sQ99_spl])],[split_symbol_definition]) ).
fof(f1206,plain,
( sQ99_spl
| ~ ssList(sK6_skl(sK47_skl,sK47_skl)) ),
inference(component_clause,[status(thm)],[f1204]) ).
fof(f1208,definition,
( sQ100_spl
<=> frontsegP(app(sK6_skl(sK47_skl,sK47_skl),sK47_skl),sK6_skl(sK47_skl,sK47_skl)) ),
introduced(definition,[new_symbols(definition,[sQ100_spl])],[split_symbol_definition]) ).
fof(f1209,plain,
( ~ sQ100_spl
| frontsegP(app(sK6_skl(sK47_skl,sK47_skl),sK47_skl),sK6_skl(sK47_skl,sK47_skl)) ),
inference(component_clause,[status(thm)],[f1208]) ).
fof(f1211,plain,
( ~ sQ38_spl
| sQ100_spl
| ~ sQ99_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f1201,f571,f1204,f1208,f763]) ).
fof(f1212,definition,
! [X0] :
( sQ101_spl
<=> ( ~ ssList(X0)
| segmentP(app(app(sK6_skl(sK47_skl,sK47_skl),sK47_skl),X0),sK47_skl)
| ~ ssList(app(sK47_skl,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ101_spl])],[split_symbol_definition]) ).
fof(f1215,plain,
( ~ sQ38_spl
| ~ sQ99_spl
| ~ sQ13_spl
| sQ101_spl ),
inference(split_clause,[status(thm)],[f1202,f1212,f571,f1204,f763]) ).
fof(f1216,definition,
( sQ102_spl
<=> rearsegP(app(sK6_skl(sK47_skl,sK47_skl),sK47_skl),sK47_skl) ),
introduced(definition,[new_symbols(definition,[sQ102_spl])],[split_symbol_definition]) ).
fof(f1219,plain,
( ~ sQ38_spl
| ~ sQ99_spl
| sQ102_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f1203,f571,f1216,f1204,f763]) ).
fof(f1224,plain,
( sQ99_spl
| ~ rearsegP(sK47_skl,sK47_skl)
| ~ ssList(sK47_skl)
| ~ ssList(sK47_skl) ),
inference(resolution,[status(thm)],[f1206,f128]) ).
fof(f1225,plain,
( sQ99_spl
| ~ sQ39_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f1224,f571,f767,f1204]) ).
fof(f1226,plain,
( sQ39_spl
| ~ sQ64_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f769,f953]) ).
fof(f1227,plain,
( sQ39_spl
| ~ sQ64_spl ),
inference(contradiction_clause,[status(thm)],[f1226]) ).
fof(f1228,plain,
( ~ sQ100_spl
| ~ sQ38_spl
| frontsegP(sK47_skl,sK6_skl(sK47_skl,sK47_skl)) ),
inference(forward_demodulation,[status(thm)],[f764,f1209]) ).
fof(f1235,plain,
( ~ sQ100_spl
| ~ sQ38_spl
| app(sK6_skl(sK47_skl,sK47_skl),sK5_skl(sK6_skl(sK47_skl,sK47_skl),sK47_skl)) = sK47_skl
| ~ ssList(sK6_skl(sK47_skl,sK47_skl))
| ~ ssList(sK47_skl) ),
inference(resolution,[status(thm)],[f1228,f123]) ).
fof(f1236,definition,
( sQ103_spl
<=> app(sK6_skl(sK47_skl,sK47_skl),sK5_skl(sK6_skl(sK47_skl,sK47_skl),sK47_skl)) = sK47_skl ),
introduced(definition,[new_symbols(definition,[sQ103_spl])],[split_symbol_definition]) ).
fof(f1239,plain,
( ~ sQ100_spl
| ~ sQ38_spl
| sQ103_spl
| ~ sQ99_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f1235,f571,f1204,f1236,f763,f1208]) ).
fof(f1240,plain,
! [X0] :
( ~ sQ56_spl
| rearsegP(sK48_skl,X0)
| ~ rearsegP(sK5_skl(nil,sK48_skl),X0)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(sK5_skl(nil,sK48_skl)) ),
inference(paramodulation,[status(thm)],[f903,f307]) ).
fof(f1241,plain,
( ~ sQ56_spl
| ~ ssList(sK5_skl(nil,sK48_skl))
| frontsegP(app(nil,sK5_skl(nil,sK48_skl)),nil)
| ~ ssList(nil)
| ~ ssList(sK48_skl) ),
inference(paramodulation,[status(thm)],[f903,f469]) ).
fof(f1242,plain,
! [X0] :
( ~ sQ56_spl
| ~ ssList(X0)
| ~ ssList(nil)
| segmentP(app(app(nil,sK5_skl(nil,sK48_skl)),X0),sK5_skl(nil,sK48_skl))
| ~ ssList(sK5_skl(nil,sK48_skl))
| ~ ssList(app(sK48_skl,X0)) ),
inference(paramodulation,[status(thm)],[f903,f471]) ).
fof(f1243,plain,
( ~ sQ56_spl
| ~ ssList(nil)
| rearsegP(app(nil,sK5_skl(nil,sK48_skl)),sK5_skl(nil,sK48_skl))
| ~ ssList(sK5_skl(nil,sK48_skl))
| ~ ssList(sK48_skl) ),
inference(paramodulation,[status(thm)],[f903,f470]) ).
fof(f1244,definition,
( sQ104_spl
<=> ssList(sK5_skl(nil,sK48_skl)) ),
introduced(definition,[new_symbols(definition,[sQ104_spl])],[split_symbol_definition]) ).
fof(f1246,plain,
( sQ104_spl
| ~ ssList(sK5_skl(nil,sK48_skl)) ),
inference(component_clause,[status(thm)],[f1244]) ).
fof(f1247,definition,
! [X0] :
( sQ105_spl
<=> ( rearsegP(sK48_skl,X0)
| ~ rearsegP(sK5_skl(nil,sK48_skl),X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ105_spl])],[split_symbol_definition]) ).
fof(f1250,plain,
( ~ sQ56_spl
| ~ sQ14_spl
| sQ105_spl
| ~ sQ104_spl ),
inference(split_clause,[status(thm)],[f1240,f1244,f1247,f574,f902]) ).
fof(f1251,definition,
( sQ106_spl
<=> frontsegP(app(nil,sK5_skl(nil,sK48_skl)),nil) ),
introduced(definition,[new_symbols(definition,[sQ106_spl])],[split_symbol_definition]) ).
fof(f1254,plain,
( ~ sQ56_spl
| ~ sQ104_spl
| sQ106_spl
| ~ sQ14_spl
| ~ sQ27_spl ),
inference(split_clause,[status(thm)],[f1241,f703,f574,f1251,f1244,f902]) ).
fof(f1255,definition,
! [X0] :
( sQ107_spl
<=> ( ~ ssList(X0)
| segmentP(app(app(nil,sK5_skl(nil,sK48_skl)),X0),sK5_skl(nil,sK48_skl))
| ~ ssList(app(sK48_skl,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ107_spl])],[split_symbol_definition]) ).
fof(f1258,plain,
( ~ sQ56_spl
| ~ sQ14_spl
| ~ sQ104_spl
| sQ107_spl ),
inference(split_clause,[status(thm)],[f1242,f1255,f1244,f574,f902]) ).
fof(f1259,definition,
( sQ108_spl
<=> rearsegP(app(nil,sK5_skl(nil,sK48_skl)),sK5_skl(nil,sK48_skl)) ),
introduced(definition,[new_symbols(definition,[sQ108_spl])],[split_symbol_definition]) ).
fof(f1262,plain,
( ~ sQ56_spl
| ~ sQ14_spl
| sQ108_spl
| ~ sQ104_spl
| ~ sQ27_spl ),
inference(split_clause,[status(thm)],[f1243,f703,f1244,f1259,f574,f902]) ).
fof(f1264,plain,
! [X0] :
( ~ sQ69_spl
| ~ rearsegP(nil,X0)
| ~ ssList(nil)
| X0 = nil
| ~ rearsegP(X0,nil)
| ~ ssList(nil)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f604,f995]) ).
fof(f1265,plain,
! [X0] :
( ~ sQ82_spl
| ~ rearsegP(nil,X0)
| ~ ssList(nil)
| X0 = sK48_skl
| ~ rearsegP(X0,sK48_skl)
| ~ ssList(sK48_skl)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f604,f1107]) ).
fof(f1267,plain,
! [X0] :
( ~ sQ55_spl
| ~ rearsegP(sK48_skl,X0)
| ~ ssList(sK48_skl)
| X0 = sK48_skl
| ~ rearsegP(X0,sK48_skl)
| ~ ssList(sK48_skl)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f604,f900]) ).
fof(f1270,plain,
! [X0] :
( ~ sQ64_spl
| ~ rearsegP(sK47_skl,X0)
| ~ ssList(sK47_skl)
| X0 = sK47_skl
| ~ rearsegP(X0,sK47_skl)
| ~ ssList(sK47_skl)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f604,f953]) ).
fof(f1271,plain,
! [X0] :
( ~ sQ17_spl
| ~ rearsegP(nil,X0)
| ~ ssList(nil)
| X0 = sK47_skl
| ~ rearsegP(X0,sK47_skl)
| ~ ssList(sK47_skl)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f604,f632]) ).
fof(f1275,plain,
! [X0,X1] :
( ~ ssList(X1)
| ~ rearsegP(nil,X0)
| ~ ssList(nil)
| X0 = X1
| ~ rearsegP(X0,X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f604,f309]) ).
fof(f1283,plain,
! [X0] :
( ~ sQ82_spl
| ~ rearsegP(X0,sK48_skl)
| ~ ssList(sK48_skl)
| nil = X0
| ~ rearsegP(nil,X0)
| ~ ssList(X0)
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f604,f1107]) ).
fof(f1287,plain,
! [X0] :
( ~ sQ17_spl
| ~ rearsegP(X0,sK47_skl)
| ~ ssList(sK47_skl)
| nil = X0
| ~ rearsegP(nil,X0)
| ~ ssList(X0)
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f604,f632]) ).
fof(f1289,plain,
! [X0,X1] :
( ~ ssList(X1)
| ~ rearsegP(X0,X1)
| ~ ssList(X1)
| nil = X0
| ~ rearsegP(nil,X0)
| ~ ssList(X0)
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f604,f309]) ).
fof(f1294,definition,
! [X0] :
( sQ109_spl
<=> ( ~ rearsegP(nil,X0)
| X0 = nil
| ~ rearsegP(X0,nil)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ109_spl])],[split_symbol_definition]) ).
fof(f1297,plain,
( ~ sQ69_spl
| ~ sQ14_spl
| sQ109_spl ),
inference(split_clause,[status(thm)],[f1264,f1294,f574,f989]) ).
fof(f1298,definition,
! [X0] :
( sQ110_spl
<=> ( ~ rearsegP(nil,X0)
| X0 = sK48_skl
| ~ rearsegP(X0,sK48_skl)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ110_spl])],[split_symbol_definition]) ).
fof(f1301,plain,
( ~ sQ82_spl
| ~ sQ14_spl
| ~ sQ27_spl
| sQ110_spl ),
inference(split_clause,[status(thm)],[f1265,f1298,f703,f574,f1101]) ).
fof(f1303,definition,
! [X0] :
( sQ111_spl
<=> ( ~ rearsegP(sK48_skl,X0)
| X0 = sK48_skl
| ~ rearsegP(X0,sK48_skl)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ111_spl])],[split_symbol_definition]) ).
fof(f1306,plain,
( ~ sQ55_spl
| ~ sQ27_spl
| sQ111_spl ),
inference(split_clause,[status(thm)],[f1267,f1303,f703,f894]) ).
fof(f1312,definition,
! [X0] :
( sQ113_spl
<=> ( ~ rearsegP(sK47_skl,X0)
| X0 = sK47_skl
| ~ rearsegP(X0,sK47_skl)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ113_spl])],[split_symbol_definition]) ).
fof(f1315,plain,
( ~ sQ64_spl
| ~ sQ13_spl
| sQ113_spl ),
inference(split_clause,[status(thm)],[f1270,f1312,f571,f947]) ).
fof(f1316,definition,
! [X0] :
( sQ114_spl
<=> ( ~ rearsegP(nil,X0)
| X0 = sK47_skl
| ~ rearsegP(X0,sK47_skl)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ114_spl])],[split_symbol_definition]) ).
fof(f1319,plain,
( ~ sQ17_spl
| ~ sQ14_spl
| ~ sQ13_spl
| sQ114_spl ),
inference(split_clause,[status(thm)],[f1271,f1316,f571,f574,f631]) ).
fof(f1322,definition,
! [X0,X1] :
( sQ115_spl
<=> ( ~ ssList(X1)
| ~ rearsegP(nil,X0)
| X0 = X1
| ~ rearsegP(X0,X1)
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ115_spl])],[split_symbol_definition]) ).
fof(f1325,plain,
( ~ sQ14_spl
| sQ115_spl ),
inference(split_clause,[status(thm)],[f1275,f1322,f574]) ).
fof(f1330,definition,
! [X0] :
( sQ116_spl
<=> ( ~ rearsegP(X0,sK48_skl)
| nil = X0
| ~ rearsegP(nil,X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ116_spl])],[split_symbol_definition]) ).
fof(f1333,plain,
( ~ sQ82_spl
| ~ sQ27_spl
| sQ116_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f1283,f574,f1330,f703,f1101]) ).
fof(f1340,definition,
! [X0] :
( sQ118_spl
<=> ( ~ rearsegP(X0,sK47_skl)
| nil = X0
| ~ rearsegP(nil,X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ118_spl])],[split_symbol_definition]) ).
fof(f1343,plain,
( ~ sQ17_spl
| ~ sQ13_spl
| sQ118_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f1287,f574,f1340,f571,f631]) ).
fof(f1345,definition,
! [X0,X1] :
( sQ119_spl
<=> ( ~ ssList(X1)
| ~ rearsegP(X0,X1)
| ~ ssList(X1)
| nil = X0
| ~ rearsegP(nil,X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ119_spl])],[split_symbol_definition]) ).
fof(f1348,plain,
( sQ119_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f1289,f574,f1345]) ).
fof(f1354,plain,
( sQ104_spl
| ~ frontsegP(sK48_skl,nil)
| ~ ssList(nil)
| ~ ssList(sK48_skl) ),
inference(resolution,[status(thm)],[f1246,f122]) ).
fof(f1355,definition,
( sQ120_spl
<=> frontsegP(sK48_skl,nil) ),
introduced(definition,[new_symbols(definition,[sQ120_spl])],[split_symbol_definition]) ).
fof(f1357,plain,
( sQ120_spl
| ~ frontsegP(sK48_skl,nil) ),
inference(component_clause,[status(thm)],[f1355]) ).
fof(f1358,plain,
( sQ104_spl
| ~ sQ120_spl
| ~ sQ14_spl
| ~ sQ27_spl ),
inference(split_clause,[status(thm)],[f1354,f703,f574,f1355,f1244]) ).
fof(f1359,plain,
( sQ120_spl
| ~ sQ53_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1357,f898]) ).
fof(f1360,plain,
( sQ120_spl
| ~ sQ53_spl ),
inference(contradiction_clause,[status(thm)],[f1359]) ).
fof(f1376,plain,
( ~ sQ57_spl
| ~ ssList(sK48_skl)
| frontsegP(app(sK6_skl(sK48_skl,sK48_skl),sK48_skl),sK6_skl(sK48_skl,sK48_skl))
| ~ ssList(sK6_skl(sK48_skl,sK48_skl))
| ~ ssList(sK48_skl) ),
inference(paramodulation,[status(thm)],[f912,f469]) ).
fof(f1377,plain,
! [X0] :
( ~ sQ57_spl
| ~ ssList(X0)
| ~ ssList(sK6_skl(sK48_skl,sK48_skl))
| segmentP(app(app(sK6_skl(sK48_skl,sK48_skl),sK48_skl),X0),sK48_skl)
| ~ ssList(sK48_skl)
| ~ ssList(app(sK48_skl,X0)) ),
inference(paramodulation,[status(thm)],[f912,f471]) ).
fof(f1378,plain,
( ~ sQ57_spl
| ~ ssList(sK6_skl(sK48_skl,sK48_skl))
| rearsegP(app(sK6_skl(sK48_skl,sK48_skl),sK48_skl),sK48_skl)
| ~ ssList(sK48_skl)
| ~ ssList(sK48_skl) ),
inference(paramodulation,[status(thm)],[f912,f470]) ).
fof(f1379,definition,
( sQ121_spl
<=> ssList(sK6_skl(sK48_skl,sK48_skl)) ),
introduced(definition,[new_symbols(definition,[sQ121_spl])],[split_symbol_definition]) ).
fof(f1381,plain,
( sQ121_spl
| ~ ssList(sK6_skl(sK48_skl,sK48_skl)) ),
inference(component_clause,[status(thm)],[f1379]) ).
fof(f1383,definition,
( sQ122_spl
<=> frontsegP(app(sK6_skl(sK48_skl,sK48_skl),sK48_skl),sK6_skl(sK48_skl,sK48_skl)) ),
introduced(definition,[new_symbols(definition,[sQ122_spl])],[split_symbol_definition]) ).
fof(f1384,plain,
( ~ sQ122_spl
| frontsegP(app(sK6_skl(sK48_skl,sK48_skl),sK48_skl),sK6_skl(sK48_skl,sK48_skl)) ),
inference(component_clause,[status(thm)],[f1383]) ).
fof(f1386,plain,
( ~ sQ57_spl
| sQ122_spl
| ~ sQ121_spl
| ~ sQ27_spl ),
inference(split_clause,[status(thm)],[f1376,f703,f1379,f1383,f911]) ).
fof(f1387,definition,
! [X0] :
( sQ123_spl
<=> ( ~ ssList(X0)
| segmentP(app(app(sK6_skl(sK48_skl,sK48_skl),sK48_skl),X0),sK48_skl)
| ~ ssList(app(sK48_skl,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ123_spl])],[split_symbol_definition]) ).
fof(f1390,plain,
( ~ sQ57_spl
| ~ sQ121_spl
| ~ sQ27_spl
| sQ123_spl ),
inference(split_clause,[status(thm)],[f1377,f1387,f703,f1379,f911]) ).
fof(f1391,definition,
( sQ124_spl
<=> rearsegP(app(sK6_skl(sK48_skl,sK48_skl),sK48_skl),sK48_skl) ),
introduced(definition,[new_symbols(definition,[sQ124_spl])],[split_symbol_definition]) ).
fof(f1394,plain,
( ~ sQ57_spl
| ~ sQ121_spl
| sQ124_spl
| ~ sQ27_spl ),
inference(split_clause,[status(thm)],[f1378,f703,f1391,f1379,f911]) ).
fof(f1395,plain,
( sQ121_spl
| ~ rearsegP(sK48_skl,sK48_skl)
| ~ ssList(sK48_skl)
| ~ ssList(sK48_skl) ),
inference(resolution,[status(thm)],[f1381,f128]) ).
fof(f1396,plain,
( sQ121_spl
| ~ sQ58_spl
| ~ sQ27_spl ),
inference(split_clause,[status(thm)],[f1395,f703,f915,f1379]) ).
fof(f1397,plain,
( ~ sQ122_spl
| ~ sQ57_spl
| frontsegP(sK48_skl,sK6_skl(sK48_skl,sK48_skl)) ),
inference(forward_demodulation,[status(thm)],[f912,f1384]) ).
fof(f1424,plain,
( ~ sQ122_spl
| ~ sQ57_spl
| app(sK6_skl(sK48_skl,sK48_skl),sK5_skl(sK6_skl(sK48_skl,sK48_skl),sK48_skl)) = sK48_skl
| ~ ssList(sK6_skl(sK48_skl,sK48_skl))
| ~ ssList(sK48_skl) ),
inference(resolution,[status(thm)],[f1397,f123]) ).
fof(f1425,definition,
( sQ128_spl
<=> app(sK6_skl(sK48_skl,sK48_skl),sK5_skl(sK6_skl(sK48_skl,sK48_skl),sK48_skl)) = sK48_skl ),
introduced(definition,[new_symbols(definition,[sQ128_spl])],[split_symbol_definition]) ).
fof(f1428,plain,
( ~ sQ122_spl
| ~ sQ57_spl
| sQ128_spl
| ~ sQ121_spl
| ~ sQ27_spl ),
inference(split_clause,[status(thm)],[f1424,f703,f1379,f1425,f911,f1383]) ).
fof(f1429,plain,
! [X0] :
( ~ sQ65_spl
| rearsegP(sK47_skl,X0)
| ~ rearsegP(sK5_skl(nil,sK47_skl),X0)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(sK5_skl(nil,sK47_skl)) ),
inference(paramodulation,[status(thm)],[f956,f307]) ).
fof(f1430,plain,
( ~ sQ65_spl
| ~ ssList(sK5_skl(nil,sK47_skl))
| frontsegP(app(nil,sK5_skl(nil,sK47_skl)),nil)
| ~ ssList(nil)
| ~ ssList(sK47_skl) ),
inference(paramodulation,[status(thm)],[f956,f469]) ).
fof(f1431,plain,
! [X0] :
( ~ sQ65_spl
| ~ ssList(X0)
| ~ ssList(nil)
| segmentP(app(app(nil,sK5_skl(nil,sK47_skl)),X0),sK5_skl(nil,sK47_skl))
| ~ ssList(sK5_skl(nil,sK47_skl))
| ~ ssList(app(sK47_skl,X0)) ),
inference(paramodulation,[status(thm)],[f956,f471]) ).
fof(f1432,plain,
( ~ sQ65_spl
| ~ ssList(nil)
| rearsegP(app(nil,sK5_skl(nil,sK47_skl)),sK5_skl(nil,sK47_skl))
| ~ ssList(sK5_skl(nil,sK47_skl))
| ~ ssList(sK47_skl) ),
inference(paramodulation,[status(thm)],[f956,f470]) ).
fof(f1433,definition,
( sQ129_spl
<=> ssList(sK5_skl(nil,sK47_skl)) ),
introduced(definition,[new_symbols(definition,[sQ129_spl])],[split_symbol_definition]) ).
fof(f1435,plain,
( sQ129_spl
| ~ ssList(sK5_skl(nil,sK47_skl)) ),
inference(component_clause,[status(thm)],[f1433]) ).
fof(f1436,definition,
! [X0] :
( sQ130_spl
<=> ( rearsegP(sK47_skl,X0)
| ~ rearsegP(sK5_skl(nil,sK47_skl),X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ130_spl])],[split_symbol_definition]) ).
fof(f1439,plain,
( ~ sQ65_spl
| ~ sQ14_spl
| sQ130_spl
| ~ sQ129_spl ),
inference(split_clause,[status(thm)],[f1429,f1433,f1436,f574,f955]) ).
fof(f1440,definition,
( sQ131_spl
<=> frontsegP(app(nil,sK5_skl(nil,sK47_skl)),nil) ),
introduced(definition,[new_symbols(definition,[sQ131_spl])],[split_symbol_definition]) ).
fof(f1443,plain,
( ~ sQ65_spl
| ~ sQ129_spl
| sQ131_spl
| ~ sQ14_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f1430,f571,f574,f1440,f1433,f955]) ).
fof(f1444,definition,
! [X0] :
( sQ132_spl
<=> ( ~ ssList(X0)
| segmentP(app(app(nil,sK5_skl(nil,sK47_skl)),X0),sK5_skl(nil,sK47_skl))
| ~ ssList(app(sK47_skl,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ132_spl])],[split_symbol_definition]) ).
fof(f1447,plain,
( ~ sQ65_spl
| ~ sQ14_spl
| ~ sQ129_spl
| sQ132_spl ),
inference(split_clause,[status(thm)],[f1431,f1444,f1433,f574,f955]) ).
fof(f1448,definition,
( sQ133_spl
<=> rearsegP(app(nil,sK5_skl(nil,sK47_skl)),sK5_skl(nil,sK47_skl)) ),
introduced(definition,[new_symbols(definition,[sQ133_spl])],[split_symbol_definition]) ).
fof(f1451,plain,
( ~ sQ65_spl
| ~ sQ14_spl
| sQ133_spl
| ~ sQ129_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f1432,f571,f1433,f1448,f574,f955]) ).
fof(f1452,plain,
( sQ129_spl
| ~ frontsegP(sK47_skl,nil)
| ~ ssList(nil)
| ~ ssList(sK47_skl) ),
inference(resolution,[status(thm)],[f1435,f122]) ).
fof(f1453,definition,
( sQ134_spl
<=> frontsegP(sK47_skl,nil) ),
introduced(definition,[new_symbols(definition,[sQ134_spl])],[split_symbol_definition]) ).
fof(f1455,plain,
( sQ134_spl
| ~ frontsegP(sK47_skl,nil) ),
inference(component_clause,[status(thm)],[f1453]) ).
fof(f1456,plain,
( sQ129_spl
| ~ sQ134_spl
| ~ sQ14_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f1452,f571,f574,f1453,f1433]) ).
fof(f1457,plain,
( sQ134_spl
| ~ sQ62_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1455,f951]) ).
fof(f1458,plain,
( sQ134_spl
| ~ sQ62_spl ),
inference(contradiction_clause,[status(thm)],[f1457]) ).
fof(f1470,plain,
! [X0] :
( ~ sQ69_spl
| ~ rearsegP(X0,nil)
| ~ ssList(nil)
| app(sK6_skl(nil,X0),nil) = X0
| ~ ssList(nil)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f621,f995]) ).
fof(f1471,plain,
! [X0] :
( ~ sQ82_spl
| ~ rearsegP(X0,sK48_skl)
| ~ ssList(sK48_skl)
| app(sK6_skl(nil,X0),nil) = X0
| ~ ssList(nil)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f621,f1107]) ).
fof(f1472,plain,
! [X0] :
( ~ sQ55_spl
| ~ rearsegP(X0,sK48_skl)
| ~ ssList(sK48_skl)
| app(sK6_skl(sK48_skl,X0),sK48_skl) = X0
| ~ ssList(sK48_skl)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f621,f900]) ).
fof(f1474,plain,
! [X0] :
( ~ sQ64_spl
| ~ rearsegP(X0,sK47_skl)
| ~ ssList(sK47_skl)
| app(sK6_skl(sK47_skl,X0),sK47_skl) = X0
| ~ ssList(sK47_skl)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f621,f953]) ).
fof(f1475,plain,
! [X0] :
( ~ sQ17_spl
| ~ rearsegP(X0,sK47_skl)
| ~ ssList(sK47_skl)
| app(sK6_skl(nil,X0),nil) = X0
| ~ ssList(nil)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f621,f632]) ).
fof(f1477,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)],[f621,f309]) ).
fof(f1481,definition,
! [X0] :
( sQ135_spl
<=> ( ~ rearsegP(X0,nil)
| app(sK6_skl(nil,X0),nil) = X0
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ135_spl])],[split_symbol_definition]) ).
fof(f1484,plain,
( ~ sQ69_spl
| ~ sQ14_spl
| sQ135_spl ),
inference(split_clause,[status(thm)],[f1470,f1481,f574,f989]) ).
fof(f1485,definition,
! [X0] :
( sQ136_spl
<=> ( ~ rearsegP(X0,sK48_skl)
| app(sK6_skl(nil,X0),nil) = X0
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ136_spl])],[split_symbol_definition]) ).
fof(f1488,plain,
( ~ sQ82_spl
| ~ sQ27_spl
| ~ sQ14_spl
| sQ136_spl ),
inference(split_clause,[status(thm)],[f1471,f1485,f574,f703,f1101]) ).
fof(f1489,definition,
! [X0] :
( sQ137_spl
<=> ( ~ rearsegP(X0,sK48_skl)
| app(sK6_skl(sK48_skl,X0),sK48_skl) = X0
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ137_spl])],[split_symbol_definition]) ).
fof(f1492,plain,
( ~ sQ55_spl
| ~ sQ27_spl
| sQ137_spl ),
inference(split_clause,[status(thm)],[f1472,f1489,f703,f894]) ).
fof(f1497,definition,
! [X0] :
( sQ139_spl
<=> ( ~ rearsegP(X0,sK47_skl)
| app(sK6_skl(sK47_skl,X0),sK47_skl) = X0
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ139_spl])],[split_symbol_definition]) ).
fof(f1500,plain,
( ~ sQ64_spl
| ~ sQ13_spl
| sQ139_spl ),
inference(split_clause,[status(thm)],[f1474,f1497,f571,f947]) ).
fof(f1501,definition,
! [X0] :
( sQ140_spl
<=> ( ~ rearsegP(X0,sK47_skl)
| app(sK6_skl(nil,X0),nil) = X0
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ140_spl])],[split_symbol_definition]) ).
fof(f1504,plain,
( ~ sQ17_spl
| ~ sQ13_spl
| ~ sQ14_spl
| sQ140_spl ),
inference(split_clause,[status(thm)],[f1475,f1501,f574,f571,f631]) ).
fof(f1506,definition,
! [X0,X1] :
( sQ141_spl
<=> ( ~ ssList(X1)
| ~ rearsegP(X0,X1)
| ~ ssList(X1)
| app(sK6_skl(nil,X0),nil) = X0
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ141_spl])],[split_symbol_definition]) ).
fof(f1509,plain,
( ~ sQ14_spl
| sQ141_spl ),
inference(split_clause,[status(thm)],[f1477,f1506,f574]) ).
fof(f1515,plain,
! [X0] :
( app(sK6_skl(X0,app(sK47_skl,nil)),X0) = app(sK47_skl,nil)
| ~ ssList(sK47_skl)
| ~ rearsegP(nil,X0)
| ~ ssList(sK47_skl)
| ~ ssList(X0)
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f1078,f650]) ).
fof(f1516,plain,
! [X0] :
( app(sK6_skl(X0,app(sK48_skl,nil)),X0) = app(sK48_skl,nil)
| ~ ssList(sK48_skl)
| ~ rearsegP(nil,X0)
| ~ ssList(sK48_skl)
| ~ ssList(X0)
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f1075,f650]) ).
fof(f1517,plain,
! [X0] :
( ~ sQ57_spl
| app(sK6_skl(X0,app(sK6_skl(sK48_skl,sK48_skl),sK48_skl)),X0) = app(sK6_skl(sK48_skl,sK48_skl),sK48_skl)
| ~ ssList(sK48_skl)
| ~ rearsegP(sK48_skl,X0)
| ~ ssList(sK6_skl(sK48_skl,sK48_skl))
| ~ ssList(X0)
| ~ ssList(sK48_skl) ),
inference(paramodulation,[status(thm)],[f912,f650]) ).
fof(f1518,plain,
! [X0] :
( ~ sQ38_spl
| app(sK6_skl(X0,app(sK6_skl(sK47_skl,sK47_skl),sK47_skl)),X0) = app(sK6_skl(sK47_skl,sK47_skl),sK47_skl)
| ~ ssList(sK47_skl)
| ~ rearsegP(sK47_skl,X0)
| ~ ssList(sK6_skl(sK47_skl,sK47_skl))
| ~ ssList(X0)
| ~ ssList(sK47_skl) ),
inference(paramodulation,[status(thm)],[f764,f650]) ).
fof(f1520,plain,
! [X0] :
( app(sK6_skl(X0,app(nil,nil)),X0) = app(nil,nil)
| ~ ssList(nil)
| ~ rearsegP(nil,X0)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f877,f650]) ).
fof(f1521,plain,
! [X0] :
( app(sK6_skl(X0,app(nil,sK47_skl)),X0) = app(nil,sK47_skl)
| ~ ssList(sK47_skl)
| ~ rearsegP(sK47_skl,X0)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(sK47_skl) ),
inference(paramodulation,[status(thm)],[f871,f650]) ).
fof(f1522,plain,
! [X0] :
( app(sK6_skl(X0,app(nil,sK48_skl)),X0) = app(nil,sK48_skl)
| ~ ssList(sK48_skl)
| ~ rearsegP(sK48_skl,X0)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(sK48_skl) ),
inference(paramodulation,[status(thm)],[f868,f650]) ).
fof(f1523,definition,
! [X0] :
( sQ142_spl
<=> ( app(sK6_skl(X0,app(sK47_skl,nil)),X0) = app(sK47_skl,nil)
| ~ rearsegP(nil,X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ142_spl])],[split_symbol_definition]) ).
fof(f1526,plain,
( ~ sQ13_spl
| sQ142_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f1515,f574,f1523,f571]) ).
fof(f1527,definition,
! [X0] :
( sQ143_spl
<=> ( app(sK6_skl(X0,app(sK48_skl,nil)),X0) = app(sK48_skl,nil)
| ~ rearsegP(nil,X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ143_spl])],[split_symbol_definition]) ).
fof(f1530,plain,
( ~ sQ27_spl
| sQ143_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f1516,f574,f1527,f703]) ).
fof(f1531,definition,
! [X0] :
( sQ144_spl
<=> ( app(sK6_skl(X0,app(sK6_skl(sK48_skl,sK48_skl),sK48_skl)),X0) = app(sK6_skl(sK48_skl,sK48_skl),sK48_skl)
| ~ rearsegP(sK48_skl,X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ144_spl])],[split_symbol_definition]) ).
fof(f1534,plain,
( ~ sQ57_spl
| ~ sQ121_spl
| sQ144_spl
| ~ sQ27_spl ),
inference(split_clause,[status(thm)],[f1517,f703,f1531,f1379,f911]) ).
fof(f1535,definition,
! [X0] :
( sQ145_spl
<=> ( app(sK6_skl(X0,app(sK6_skl(sK47_skl,sK47_skl),sK47_skl)),X0) = app(sK6_skl(sK47_skl,sK47_skl),sK47_skl)
| ~ rearsegP(sK47_skl,X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ145_spl])],[split_symbol_definition]) ).
fof(f1538,plain,
( ~ sQ38_spl
| ~ sQ99_spl
| sQ145_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f1518,f571,f1535,f1204,f763]) ).
fof(f1543,definition,
! [X0] :
( sQ147_spl
<=> ( app(sK6_skl(X0,app(nil,nil)),X0) = app(nil,nil)
| ~ rearsegP(nil,X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ147_spl])],[split_symbol_definition]) ).
fof(f1546,plain,
( sQ147_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f1520,f574,f1543]) ).
fof(f1547,definition,
! [X0] :
( sQ148_spl
<=> ( app(sK6_skl(X0,app(nil,sK47_skl)),X0) = app(nil,sK47_skl)
| ~ rearsegP(sK47_skl,X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ148_spl])],[split_symbol_definition]) ).
fof(f1550,plain,
( ~ sQ14_spl
| sQ148_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f1521,f571,f1547,f574]) ).
fof(f1551,definition,
! [X0] :
( sQ149_spl
<=> ( app(sK6_skl(X0,app(nil,sK48_skl)),X0) = app(nil,sK48_skl)
| ~ rearsegP(sK48_skl,X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ149_spl])],[split_symbol_definition]) ).
fof(f1554,plain,
( ~ sQ14_spl
| sQ149_spl
| ~ sQ27_spl ),
inference(split_clause,[status(thm)],[f1522,f703,f1551,f574]) ).
fof(f1580,plain,
! [X0] :
( ~ sQ83_spl
| app(sK6_skl(X0,app(sK48_skl,sK5_skl(sK48_skl,sK48_skl))),X0) = app(sK48_skl,sK5_skl(sK48_skl,sK48_skl))
| ~ ssList(sK48_skl)
| ~ rearsegP(sK5_skl(sK48_skl,sK48_skl),X0)
| ~ ssList(sK48_skl)
| ~ ssList(X0)
| ~ ssList(sK5_skl(sK48_skl,sK48_skl)) ),
inference(paramodulation,[status(thm)],[f1110,f650]) ).
fof(f1581,plain,
! [X0] :
( ~ sQ83_spl
| rearsegP(sK48_skl,X0)
| ~ rearsegP(sK5_skl(sK48_skl,sK48_skl),X0)
| ~ ssList(sK48_skl)
| ~ ssList(X0)
| ~ ssList(sK5_skl(sK48_skl,sK48_skl)) ),
inference(paramodulation,[status(thm)],[f1110,f307]) ).
fof(f1582,plain,
( ~ sQ83_spl
| ~ ssList(sK5_skl(sK48_skl,sK48_skl))
| frontsegP(app(sK48_skl,sK5_skl(sK48_skl,sK48_skl)),sK48_skl)
| ~ ssList(sK48_skl)
| ~ ssList(sK48_skl) ),
inference(paramodulation,[status(thm)],[f1110,f469]) ).
fof(f1583,plain,
! [X0] :
( ~ sQ83_spl
| ~ ssList(X0)
| ~ ssList(sK48_skl)
| segmentP(app(app(sK48_skl,sK5_skl(sK48_skl,sK48_skl)),X0),sK5_skl(sK48_skl,sK48_skl))
| ~ ssList(sK5_skl(sK48_skl,sK48_skl))
| ~ ssList(app(sK48_skl,X0)) ),
inference(paramodulation,[status(thm)],[f1110,f471]) ).
fof(f1584,plain,
( ~ sQ83_spl
| ~ ssList(sK48_skl)
| rearsegP(app(sK48_skl,sK5_skl(sK48_skl,sK48_skl)),sK5_skl(sK48_skl,sK48_skl))
| ~ ssList(sK5_skl(sK48_skl,sK48_skl))
| ~ ssList(sK48_skl) ),
inference(paramodulation,[status(thm)],[f1110,f470]) ).
fof(f1585,definition,
( sQ150_spl
<=> ssList(sK5_skl(sK48_skl,sK48_skl)) ),
introduced(definition,[new_symbols(definition,[sQ150_spl])],[split_symbol_definition]) ).
fof(f1587,plain,
( sQ150_spl
| ~ ssList(sK5_skl(sK48_skl,sK48_skl)) ),
inference(component_clause,[status(thm)],[f1585]) ).
fof(f1588,definition,
! [X0] :
( sQ151_spl
<=> ( app(sK6_skl(X0,app(sK48_skl,sK5_skl(sK48_skl,sK48_skl))),X0) = app(sK48_skl,sK5_skl(sK48_skl,sK48_skl))
| ~ rearsegP(sK5_skl(sK48_skl,sK48_skl),X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ151_spl])],[split_symbol_definition]) ).
fof(f1591,plain,
( ~ sQ83_spl
| ~ sQ27_spl
| sQ151_spl
| ~ sQ150_spl ),
inference(split_clause,[status(thm)],[f1580,f1585,f1588,f703,f1109]) ).
fof(f1592,definition,
! [X0] :
( sQ152_spl
<=> ( rearsegP(sK48_skl,X0)
| ~ rearsegP(sK5_skl(sK48_skl,sK48_skl),X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ152_spl])],[split_symbol_definition]) ).
fof(f1595,plain,
( ~ sQ83_spl
| ~ sQ27_spl
| sQ152_spl
| ~ sQ150_spl ),
inference(split_clause,[status(thm)],[f1581,f1585,f1592,f703,f1109]) ).
fof(f1596,definition,
( sQ153_spl
<=> frontsegP(app(sK48_skl,sK5_skl(sK48_skl,sK48_skl)),sK48_skl) ),
introduced(definition,[new_symbols(definition,[sQ153_spl])],[split_symbol_definition]) ).
fof(f1599,plain,
( ~ sQ83_spl
| ~ sQ150_spl
| sQ153_spl
| ~ sQ27_spl ),
inference(split_clause,[status(thm)],[f1582,f703,f1596,f1585,f1109]) ).
fof(f1600,definition,
! [X0] :
( sQ154_spl
<=> ( ~ ssList(X0)
| segmentP(app(app(sK48_skl,sK5_skl(sK48_skl,sK48_skl)),X0),sK5_skl(sK48_skl,sK48_skl))
| ~ ssList(app(sK48_skl,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ154_spl])],[split_symbol_definition]) ).
fof(f1603,plain,
( ~ sQ83_spl
| ~ sQ27_spl
| ~ sQ150_spl
| sQ154_spl ),
inference(split_clause,[status(thm)],[f1583,f1600,f1585,f703,f1109]) ).
fof(f1604,definition,
( sQ155_spl
<=> rearsegP(app(sK48_skl,sK5_skl(sK48_skl,sK48_skl)),sK5_skl(sK48_skl,sK48_skl)) ),
introduced(definition,[new_symbols(definition,[sQ155_spl])],[split_symbol_definition]) ).
fof(f1605,plain,
( ~ sQ155_spl
| rearsegP(app(sK48_skl,sK5_skl(sK48_skl,sK48_skl)),sK5_skl(sK48_skl,sK48_skl)) ),
inference(component_clause,[status(thm)],[f1604]) ).
fof(f1607,plain,
( ~ sQ83_spl
| sQ155_spl
| ~ sQ150_spl
| ~ sQ27_spl ),
inference(split_clause,[status(thm)],[f1584,f703,f1585,f1604,f1109]) ).
fof(f1631,plain,
( sQ150_spl
| ~ frontsegP(sK48_skl,sK48_skl)
| ~ ssList(sK48_skl)
| ~ ssList(sK48_skl) ),
inference(resolution,[status(thm)],[f1587,f122]) ).
fof(f1632,definition,
( sQ159_spl
<=> frontsegP(sK48_skl,sK48_skl) ),
introduced(definition,[new_symbols(definition,[sQ159_spl])],[split_symbol_definition]) ).
fof(f1634,plain,
( sQ159_spl
| ~ frontsegP(sK48_skl,sK48_skl) ),
inference(component_clause,[status(thm)],[f1632]) ).
fof(f1635,plain,
( sQ150_spl
| ~ sQ159_spl
| ~ sQ27_spl ),
inference(split_clause,[status(thm)],[f1631,f703,f1632,f1585]) ).
fof(f1636,plain,
( sQ159_spl
| ~ sQ80_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1634,f1105]) ).
fof(f1637,plain,
( sQ159_spl
| ~ sQ80_spl ),
inference(contradiction_clause,[status(thm)],[f1636]) ).
fof(f1642,plain,
( ~ sQ155_spl
| ~ sQ83_spl
| rearsegP(sK48_skl,sK5_skl(sK48_skl,sK48_skl)) ),
inference(forward_demodulation,[status(thm)],[f1110,f1605]) ).
fof(f1646,plain,
! [X0] :
( ~ sQ155_spl
| ~ sQ83_spl
| ~ rearsegP(X0,sK48_skl)
| ~ ssList(sK48_skl)
| app(sK6_skl(sK5_skl(sK48_skl,sK48_skl),X0),sK5_skl(sK48_skl,sK48_skl)) = X0
| ~ ssList(sK5_skl(sK48_skl,sK48_skl))
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f1642,f621]) ).
fof(f1647,plain,
! [X0] :
( ~ sQ155_spl
| ~ sQ83_spl
| ~ rearsegP(X0,sK48_skl)
| ~ ssList(sK48_skl)
| sK5_skl(sK48_skl,sK48_skl) = X0
| ~ rearsegP(sK5_skl(sK48_skl,sK48_skl),X0)
| ~ ssList(X0)
| ~ ssList(sK5_skl(sK48_skl,sK48_skl)) ),
inference(resolution,[status(thm)],[f1642,f604]) ).
fof(f1648,plain,
! [X0] :
( ~ sQ155_spl
| ~ sQ83_spl
| ~ rearsegP(sK5_skl(sK48_skl,sK48_skl),X0)
| ~ ssList(sK5_skl(sK48_skl,sK48_skl))
| X0 = sK48_skl
| ~ rearsegP(X0,sK48_skl)
| ~ ssList(sK48_skl)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f1642,f604]) ).
fof(f1649,plain,
( ~ sQ155_spl
| ~ sQ83_spl
| app(sK6_skl(sK5_skl(sK48_skl,sK48_skl),sK48_skl),sK5_skl(sK48_skl,sK48_skl)) = sK48_skl
| ~ ssList(sK5_skl(sK48_skl,sK48_skl))
| ~ ssList(sK48_skl) ),
inference(resolution,[status(thm)],[f1642,f129]) ).
fof(f1651,plain,
! [X0] :
( ~ sQ155_spl
| ~ sQ83_spl
| rearsegP(X0,sK5_skl(sK48_skl,sK48_skl))
| ~ rearsegP(X0,sK48_skl)
| ~ ssList(sK5_skl(sK48_skl,sK48_skl))
| ~ ssList(sK48_skl)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f1642,f301]) ).
fof(f1652,definition,
! [X0] :
( sQ160_spl
<=> ( ~ rearsegP(X0,sK48_skl)
| app(sK6_skl(sK5_skl(sK48_skl,sK48_skl),X0),sK5_skl(sK48_skl,sK48_skl)) = X0
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ160_spl])],[split_symbol_definition]) ).
fof(f1655,plain,
( ~ sQ155_spl
| ~ sQ83_spl
| ~ sQ27_spl
| ~ sQ150_spl
| sQ160_spl ),
inference(split_clause,[status(thm)],[f1646,f1652,f1585,f703,f1109,f1604]) ).
fof(f1656,definition,
! [X0] :
( sQ161_spl
<=> ( ~ rearsegP(X0,sK48_skl)
| sK5_skl(sK48_skl,sK48_skl) = X0
| ~ rearsegP(sK5_skl(sK48_skl,sK48_skl),X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ161_spl])],[split_symbol_definition]) ).
fof(f1659,plain,
( ~ sQ155_spl
| ~ sQ83_spl
| ~ sQ27_spl
| sQ161_spl
| ~ sQ150_spl ),
inference(split_clause,[status(thm)],[f1647,f1585,f1656,f703,f1109,f1604]) ).
fof(f1660,definition,
! [X0] :
( sQ162_spl
<=> ( ~ rearsegP(sK5_skl(sK48_skl,sK48_skl),X0)
| X0 = sK48_skl
| ~ rearsegP(X0,sK48_skl)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ162_spl])],[split_symbol_definition]) ).
fof(f1663,plain,
( ~ sQ155_spl
| ~ sQ83_spl
| ~ sQ150_spl
| ~ sQ27_spl
| sQ162_spl ),
inference(split_clause,[status(thm)],[f1648,f1660,f703,f1585,f1109,f1604]) ).
fof(f1664,definition,
( sQ163_spl
<=> app(sK6_skl(sK5_skl(sK48_skl,sK48_skl),sK48_skl),sK5_skl(sK48_skl,sK48_skl)) = sK48_skl ),
introduced(definition,[new_symbols(definition,[sQ163_spl])],[split_symbol_definition]) ).
fof(f1667,plain,
( ~ sQ155_spl
| ~ sQ83_spl
| sQ163_spl
| ~ sQ150_spl
| ~ sQ27_spl ),
inference(split_clause,[status(thm)],[f1649,f703,f1585,f1664,f1109,f1604]) ).
fof(f1675,definition,
! [X0] :
( sQ166_spl
<=> ( rearsegP(X0,sK5_skl(sK48_skl,sK48_skl))
| ~ rearsegP(X0,sK48_skl)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ166_spl])],[split_symbol_definition]) ).
fof(f1678,plain,
( ~ sQ155_spl
| ~ sQ83_spl
| ~ sQ150_spl
| ~ sQ27_spl
| sQ166_spl ),
inference(split_clause,[status(thm)],[f1651,f1675,f703,f1585,f1109,f1604]) ).
fof(f1689,plain,
! [X0] :
( ~ sQ70_spl
| app(sK6_skl(X0,app(nil,sK5_skl(nil,nil))),X0) = app(nil,sK5_skl(nil,nil))
| ~ ssList(nil)
| ~ rearsegP(sK5_skl(nil,nil),X0)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(sK5_skl(nil,nil)) ),
inference(paramodulation,[status(thm)],[f998,f650]) ).
fof(f1690,plain,
! [X0] :
( ~ sQ70_spl
| rearsegP(nil,X0)
| ~ rearsegP(sK5_skl(nil,nil),X0)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(sK5_skl(nil,nil)) ),
inference(paramodulation,[status(thm)],[f998,f307]) ).
fof(f1691,plain,
( ~ sQ70_spl
| ~ ssList(sK5_skl(nil,nil))
| frontsegP(app(nil,sK5_skl(nil,nil)),nil)
| ~ ssList(nil)
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f998,f469]) ).
fof(f1692,plain,
! [X0] :
( ~ sQ70_spl
| ~ ssList(X0)
| ~ ssList(nil)
| segmentP(app(app(nil,sK5_skl(nil,nil)),X0),sK5_skl(nil,nil))
| ~ ssList(sK5_skl(nil,nil))
| ~ ssList(app(nil,X0)) ),
inference(paramodulation,[status(thm)],[f998,f471]) ).
fof(f1693,plain,
( ~ sQ70_spl
| ~ ssList(nil)
| rearsegP(app(nil,sK5_skl(nil,nil)),sK5_skl(nil,nil))
| ~ ssList(sK5_skl(nil,nil))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f998,f470]) ).
fof(f1694,definition,
( sQ169_spl
<=> ssList(sK5_skl(nil,nil)) ),
introduced(definition,[new_symbols(definition,[sQ169_spl])],[split_symbol_definition]) ).
fof(f1696,plain,
( sQ169_spl
| ~ ssList(sK5_skl(nil,nil)) ),
inference(component_clause,[status(thm)],[f1694]) ).
fof(f1697,definition,
! [X0] :
( sQ170_spl
<=> ( app(sK6_skl(X0,app(nil,sK5_skl(nil,nil))),X0) = app(nil,sK5_skl(nil,nil))
| ~ rearsegP(sK5_skl(nil,nil),X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ170_spl])],[split_symbol_definition]) ).
fof(f1700,plain,
( ~ sQ70_spl
| ~ sQ14_spl
| sQ170_spl
| ~ sQ169_spl ),
inference(split_clause,[status(thm)],[f1689,f1694,f1697,f574,f997]) ).
fof(f1701,definition,
! [X0] :
( sQ171_spl
<=> ( rearsegP(nil,X0)
| ~ rearsegP(sK5_skl(nil,nil),X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ171_spl])],[split_symbol_definition]) ).
fof(f1704,plain,
( ~ sQ70_spl
| ~ sQ14_spl
| sQ171_spl
| ~ sQ169_spl ),
inference(split_clause,[status(thm)],[f1690,f1694,f1701,f574,f997]) ).
fof(f1705,definition,
( sQ172_spl
<=> frontsegP(app(nil,sK5_skl(nil,nil)),nil) ),
introduced(definition,[new_symbols(definition,[sQ172_spl])],[split_symbol_definition]) ).
fof(f1708,plain,
( ~ sQ70_spl
| ~ sQ169_spl
| sQ172_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f1691,f574,f1705,f1694,f997]) ).
fof(f1709,definition,
! [X0] :
( sQ173_spl
<=> ( ~ ssList(X0)
| segmentP(app(app(nil,sK5_skl(nil,nil)),X0),sK5_skl(nil,nil))
| ~ ssList(app(nil,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ173_spl])],[split_symbol_definition]) ).
fof(f1712,plain,
( ~ sQ70_spl
| ~ sQ14_spl
| ~ sQ169_spl
| sQ173_spl ),
inference(split_clause,[status(thm)],[f1692,f1709,f1694,f574,f997]) ).
fof(f1713,definition,
( sQ174_spl
<=> rearsegP(app(nil,sK5_skl(nil,nil)),sK5_skl(nil,nil)) ),
introduced(definition,[new_symbols(definition,[sQ174_spl])],[split_symbol_definition]) ).
fof(f1716,plain,
( ~ sQ70_spl
| sQ174_spl
| ~ sQ169_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f1693,f574,f1694,f1713,f997]) ).
fof(f1717,plain,
( sQ169_spl
| ~ frontsegP(nil,nil)
| ~ ssList(nil)
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f1696,f122]) ).
fof(f1718,definition,
( sQ175_spl
<=> frontsegP(nil,nil) ),
introduced(definition,[new_symbols(definition,[sQ175_spl])],[split_symbol_definition]) ).
fof(f1720,plain,
( sQ175_spl
| ~ frontsegP(nil,nil) ),
inference(component_clause,[status(thm)],[f1718]) ).
fof(f1721,plain,
( sQ169_spl
| ~ sQ175_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f1717,f574,f1718,f1694]) ).
fof(f1722,plain,
( sQ175_spl
| ~ sQ67_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1720,f993]) ).
fof(f1723,plain,
( sQ175_spl
| ~ sQ67_spl ),
inference(contradiction_clause,[status(thm)],[f1722]) ).
fof(f1729,plain,
! [X0] :
( X0 = app(sK47_skl,nil)
| ~ rearsegP(X0,app(sK47_skl,nil))
| ~ ssList(sK47_skl)
| ~ rearsegP(nil,X0)
| ~ ssList(sK47_skl)
| ~ ssList(X0)
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f1078,f651]) ).
fof(f1730,plain,
! [X0] :
( ~ sQ83_spl
| X0 = app(sK48_skl,sK5_skl(sK48_skl,sK48_skl))
| ~ rearsegP(X0,app(sK48_skl,sK5_skl(sK48_skl,sK48_skl)))
| ~ ssList(sK48_skl)
| ~ rearsegP(sK5_skl(sK48_skl,sK48_skl),X0)
| ~ ssList(sK48_skl)
| ~ ssList(X0)
| ~ ssList(sK5_skl(sK48_skl,sK48_skl)) ),
inference(paramodulation,[status(thm)],[f1110,f651]) ).
fof(f1731,plain,
! [X0] :
( X0 = app(sK48_skl,nil)
| ~ rearsegP(X0,app(sK48_skl,nil))
| ~ ssList(sK48_skl)
| ~ rearsegP(nil,X0)
| ~ ssList(sK48_skl)
| ~ ssList(X0)
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f1075,f651]) ).
fof(f1732,plain,
! [X0] :
( ~ sQ57_spl
| X0 = app(sK6_skl(sK48_skl,sK48_skl),sK48_skl)
| ~ rearsegP(X0,app(sK6_skl(sK48_skl,sK48_skl),sK48_skl))
| ~ ssList(sK48_skl)
| ~ rearsegP(sK48_skl,X0)
| ~ ssList(sK6_skl(sK48_skl,sK48_skl))
| ~ ssList(X0)
| ~ ssList(sK48_skl) ),
inference(paramodulation,[status(thm)],[f912,f651]) ).
fof(f1733,plain,
! [X0] :
( ~ sQ38_spl
| X0 = app(sK6_skl(sK47_skl,sK47_skl),sK47_skl)
| ~ rearsegP(X0,app(sK6_skl(sK47_skl,sK47_skl),sK47_skl))
| ~ ssList(sK47_skl)
| ~ rearsegP(sK47_skl,X0)
| ~ ssList(sK6_skl(sK47_skl,sK47_skl))
| ~ ssList(X0)
| ~ ssList(sK47_skl) ),
inference(paramodulation,[status(thm)],[f764,f651]) ).
fof(f1735,plain,
! [X0] :
( ~ sQ70_spl
| X0 = app(nil,sK5_skl(nil,nil))
| ~ rearsegP(X0,app(nil,sK5_skl(nil,nil)))
| ~ ssList(nil)
| ~ rearsegP(sK5_skl(nil,nil),X0)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(sK5_skl(nil,nil)) ),
inference(paramodulation,[status(thm)],[f998,f651]) ).
fof(f1736,plain,
! [X0] :
( X0 = app(nil,nil)
| ~ rearsegP(X0,app(nil,nil))
| ~ ssList(nil)
| ~ rearsegP(nil,X0)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f877,f651]) ).
fof(f1737,plain,
! [X0] :
( X0 = app(nil,sK47_skl)
| ~ rearsegP(X0,app(nil,sK47_skl))
| ~ ssList(sK47_skl)
| ~ rearsegP(sK47_skl,X0)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(sK47_skl) ),
inference(paramodulation,[status(thm)],[f871,f651]) ).
fof(f1738,plain,
! [X0] :
( X0 = app(nil,sK48_skl)
| ~ rearsegP(X0,app(nil,sK48_skl))
| ~ ssList(sK48_skl)
| ~ rearsegP(sK48_skl,X0)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(sK48_skl) ),
inference(paramodulation,[status(thm)],[f868,f651]) ).
fof(f1739,definition,
! [X0] :
( sQ176_spl
<=> ( X0 = app(sK47_skl,nil)
| ~ rearsegP(X0,app(sK47_skl,nil))
| ~ rearsegP(nil,X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ176_spl])],[split_symbol_definition]) ).
fof(f1742,plain,
( ~ sQ13_spl
| sQ176_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f1729,f574,f1739,f571]) ).
fof(f1743,definition,
! [X0] :
( sQ177_spl
<=> ( X0 = app(sK48_skl,sK5_skl(sK48_skl,sK48_skl))
| ~ rearsegP(X0,app(sK48_skl,sK5_skl(sK48_skl,sK48_skl)))
| ~ rearsegP(sK5_skl(sK48_skl,sK48_skl),X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ177_spl])],[split_symbol_definition]) ).
fof(f1746,plain,
( ~ sQ83_spl
| ~ sQ27_spl
| sQ177_spl
| ~ sQ150_spl ),
inference(split_clause,[status(thm)],[f1730,f1585,f1743,f703,f1109]) ).
fof(f1747,definition,
! [X0] :
( sQ178_spl
<=> ( X0 = app(sK48_skl,nil)
| ~ rearsegP(X0,app(sK48_skl,nil))
| ~ rearsegP(nil,X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ178_spl])],[split_symbol_definition]) ).
fof(f1750,plain,
( ~ sQ27_spl
| sQ178_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f1731,f574,f1747,f703]) ).
fof(f1751,definition,
! [X0] :
( sQ179_spl
<=> ( X0 = app(sK6_skl(sK48_skl,sK48_skl),sK48_skl)
| ~ rearsegP(X0,app(sK6_skl(sK48_skl,sK48_skl),sK48_skl))
| ~ rearsegP(sK48_skl,X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ179_spl])],[split_symbol_definition]) ).
fof(f1754,plain,
( ~ sQ57_spl
| ~ sQ121_spl
| sQ179_spl
| ~ sQ27_spl ),
inference(split_clause,[status(thm)],[f1732,f703,f1751,f1379,f911]) ).
fof(f1755,definition,
! [X0] :
( sQ180_spl
<=> ( X0 = app(sK6_skl(sK47_skl,sK47_skl),sK47_skl)
| ~ rearsegP(X0,app(sK6_skl(sK47_skl,sK47_skl),sK47_skl))
| ~ rearsegP(sK47_skl,X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ180_spl])],[split_symbol_definition]) ).
fof(f1758,plain,
( ~ sQ38_spl
| ~ sQ99_spl
| sQ180_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f1733,f571,f1755,f1204,f763]) ).
fof(f1763,definition,
! [X0] :
( sQ182_spl
<=> ( X0 = app(nil,sK5_skl(nil,nil))
| ~ rearsegP(X0,app(nil,sK5_skl(nil,nil)))
| ~ rearsegP(sK5_skl(nil,nil),X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ182_spl])],[split_symbol_definition]) ).
fof(f1766,plain,
( ~ sQ70_spl
| ~ sQ14_spl
| sQ182_spl
| ~ sQ169_spl ),
inference(split_clause,[status(thm)],[f1735,f1694,f1763,f574,f997]) ).
fof(f1767,definition,
! [X0] :
( sQ183_spl
<=> ( X0 = app(nil,nil)
| ~ rearsegP(X0,app(nil,nil))
| ~ rearsegP(nil,X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ183_spl])],[split_symbol_definition]) ).
fof(f1770,plain,
( sQ183_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f1736,f574,f1767]) ).
fof(f1771,definition,
! [X0] :
( sQ184_spl
<=> ( X0 = app(nil,sK47_skl)
| ~ rearsegP(X0,app(nil,sK47_skl))
| ~ rearsegP(sK47_skl,X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ184_spl])],[split_symbol_definition]) ).
fof(f1774,plain,
( ~ sQ14_spl
| sQ184_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f1737,f571,f1771,f574]) ).
fof(f1775,definition,
! [X0] :
( sQ185_spl
<=> ( X0 = app(nil,sK48_skl)
| ~ rearsegP(X0,app(nil,sK48_skl))
| ~ rearsegP(sK48_skl,X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ185_spl])],[split_symbol_definition]) ).
fof(f1778,plain,
( ~ sQ14_spl
| sQ185_spl
| ~ sQ27_spl ),
inference(split_clause,[status(thm)],[f1738,f703,f1775,f574]) ).
fof(f1800,plain,
! [X0,X1] :
( rearsegP(X1,X0)
| ~ rearsegP(X1,app(sK47_skl,nil))
| ~ ssList(sK47_skl)
| ~ ssList(X1)
| ~ rearsegP(nil,X0)
| ~ ssList(sK47_skl)
| ~ ssList(X0)
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f1078,f652]) ).
fof(f1801,plain,
! [X0,X1] :
( ~ sQ83_spl
| rearsegP(X1,X0)
| ~ rearsegP(X1,app(sK48_skl,sK5_skl(sK48_skl,sK48_skl)))
| ~ ssList(sK48_skl)
| ~ ssList(X1)
| ~ rearsegP(sK5_skl(sK48_skl,sK48_skl),X0)
| ~ ssList(sK48_skl)
| ~ ssList(X0)
| ~ ssList(sK5_skl(sK48_skl,sK48_skl)) ),
inference(paramodulation,[status(thm)],[f1110,f652]) ).
fof(f1802,plain,
! [X0,X1] :
( rearsegP(X1,X0)
| ~ rearsegP(X1,app(sK48_skl,nil))
| ~ ssList(sK48_skl)
| ~ ssList(X1)
| ~ rearsegP(nil,X0)
| ~ ssList(sK48_skl)
| ~ ssList(X0)
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f1075,f652]) ).
fof(f1803,plain,
! [X0,X1] :
( ~ sQ57_spl
| rearsegP(X1,X0)
| ~ rearsegP(X1,app(sK6_skl(sK48_skl,sK48_skl),sK48_skl))
| ~ ssList(sK48_skl)
| ~ ssList(X1)
| ~ rearsegP(sK48_skl,X0)
| ~ ssList(sK6_skl(sK48_skl,sK48_skl))
| ~ ssList(X0)
| ~ ssList(sK48_skl) ),
inference(paramodulation,[status(thm)],[f912,f652]) ).
fof(f1804,plain,
! [X0,X1] :
( ~ sQ38_spl
| rearsegP(X1,X0)
| ~ rearsegP(X1,app(sK6_skl(sK47_skl,sK47_skl),sK47_skl))
| ~ ssList(sK47_skl)
| ~ ssList(X1)
| ~ rearsegP(sK47_skl,X0)
| ~ ssList(sK6_skl(sK47_skl,sK47_skl))
| ~ ssList(X0)
| ~ ssList(sK47_skl) ),
inference(paramodulation,[status(thm)],[f764,f652]) ).
fof(f1806,plain,
! [X0,X1] :
( ~ sQ70_spl
| rearsegP(X1,X0)
| ~ rearsegP(X1,app(nil,sK5_skl(nil,nil)))
| ~ ssList(nil)
| ~ ssList(X1)
| ~ rearsegP(sK5_skl(nil,nil),X0)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(sK5_skl(nil,nil)) ),
inference(paramodulation,[status(thm)],[f998,f652]) ).
fof(f1807,plain,
! [X0,X1] :
( rearsegP(X1,X0)
| ~ rearsegP(X1,app(nil,nil))
| ~ ssList(nil)
| ~ ssList(X1)
| ~ rearsegP(nil,X0)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f877,f652]) ).
fof(f1808,plain,
! [X0,X1] :
( rearsegP(X1,X0)
| ~ rearsegP(X1,app(nil,sK47_skl))
| ~ ssList(sK47_skl)
| ~ ssList(X1)
| ~ rearsegP(sK47_skl,X0)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(sK47_skl) ),
inference(paramodulation,[status(thm)],[f871,f652]) ).
fof(f1809,plain,
! [X0,X1] :
( rearsegP(X1,X0)
| ~ rearsegP(X1,app(nil,sK48_skl))
| ~ ssList(sK48_skl)
| ~ ssList(X1)
| ~ rearsegP(sK48_skl,X0)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(sK48_skl) ),
inference(paramodulation,[status(thm)],[f868,f652]) ).
fof(f1810,definition,
! [X0,X1] :
( sQ186_spl
<=> ( rearsegP(X1,X0)
| ~ rearsegP(X1,app(sK47_skl,nil))
| ~ ssList(X1)
| ~ rearsegP(nil,X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ186_spl])],[split_symbol_definition]) ).
fof(f1813,plain,
( ~ sQ13_spl
| sQ186_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f1800,f574,f1810,f571]) ).
fof(f1814,definition,
! [X0,X1] :
( sQ187_spl
<=> ( rearsegP(X1,X0)
| ~ rearsegP(X1,app(sK48_skl,sK5_skl(sK48_skl,sK48_skl)))
| ~ ssList(X1)
| ~ rearsegP(sK5_skl(sK48_skl,sK48_skl),X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ187_spl])],[split_symbol_definition]) ).
fof(f1817,plain,
( ~ sQ83_spl
| ~ sQ27_spl
| sQ187_spl
| ~ sQ150_spl ),
inference(split_clause,[status(thm)],[f1801,f1585,f1814,f703,f1109]) ).
fof(f1818,definition,
! [X0,X1] :
( sQ188_spl
<=> ( rearsegP(X1,X0)
| ~ rearsegP(X1,app(sK48_skl,nil))
| ~ ssList(X1)
| ~ rearsegP(nil,X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ188_spl])],[split_symbol_definition]) ).
fof(f1821,plain,
( ~ sQ27_spl
| sQ188_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f1802,f574,f1818,f703]) ).
fof(f1822,definition,
! [X0,X1] :
( sQ189_spl
<=> ( rearsegP(X1,X0)
| ~ rearsegP(X1,app(sK6_skl(sK48_skl,sK48_skl),sK48_skl))
| ~ ssList(X1)
| ~ rearsegP(sK48_skl,X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ189_spl])],[split_symbol_definition]) ).
fof(f1825,plain,
( ~ sQ57_spl
| ~ sQ121_spl
| sQ189_spl
| ~ sQ27_spl ),
inference(split_clause,[status(thm)],[f1803,f703,f1822,f1379,f911]) ).
fof(f1826,definition,
! [X0,X1] :
( sQ190_spl
<=> ( rearsegP(X1,X0)
| ~ rearsegP(X1,app(sK6_skl(sK47_skl,sK47_skl),sK47_skl))
| ~ ssList(X1)
| ~ rearsegP(sK47_skl,X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ190_spl])],[split_symbol_definition]) ).
fof(f1829,plain,
( ~ sQ38_spl
| ~ sQ99_spl
| sQ190_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f1804,f571,f1826,f1204,f763]) ).
fof(f1834,definition,
! [X0,X1] :
( sQ192_spl
<=> ( rearsegP(X1,X0)
| ~ rearsegP(X1,app(nil,sK5_skl(nil,nil)))
| ~ ssList(X1)
| ~ rearsegP(sK5_skl(nil,nil),X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ192_spl])],[split_symbol_definition]) ).
fof(f1837,plain,
( ~ sQ70_spl
| ~ sQ14_spl
| sQ192_spl
| ~ sQ169_spl ),
inference(split_clause,[status(thm)],[f1806,f1694,f1834,f574,f997]) ).
fof(f1838,definition,
! [X0,X1] :
( sQ193_spl
<=> ( rearsegP(X1,X0)
| ~ rearsegP(X1,app(nil,nil))
| ~ ssList(X1)
| ~ rearsegP(nil,X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ193_spl])],[split_symbol_definition]) ).
fof(f1841,plain,
( sQ193_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f1807,f574,f1838]) ).
fof(f1842,definition,
! [X0,X1] :
( sQ194_spl
<=> ( rearsegP(X1,X0)
| ~ rearsegP(X1,app(nil,sK47_skl))
| ~ ssList(X1)
| ~ rearsegP(sK47_skl,X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ194_spl])],[split_symbol_definition]) ).
fof(f1845,plain,
( ~ sQ14_spl
| sQ194_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f1808,f571,f1842,f574]) ).
fof(f1846,definition,
! [X0,X1] :
( sQ195_spl
<=> ( rearsegP(X1,X0)
| ~ rearsegP(X1,app(nil,sK48_skl))
| ~ ssList(X1)
| ~ rearsegP(sK48_skl,X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ195_spl])],[split_symbol_definition]) ).
fof(f1849,plain,
( ~ sQ14_spl
| sQ195_spl
| ~ sQ27_spl ),
inference(split_clause,[status(thm)],[f1809,f703,f1846,f574]) ).
fof(f1931,plain,
! [X0,X1] :
( ~ sQ71_spl
| rearsegP(X1,X0)
| ~ rearsegP(X1,app(sK6_skl(nil,nil),nil))
| ~ ssList(nil)
| ~ ssList(X1)
| ~ rearsegP(nil,X0)
| ~ ssList(sK6_skl(nil,nil))
| ~ ssList(X0)
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f1007,f652]) ).
fof(f1932,plain,
! [X0] :
( ~ sQ71_spl
| X0 = app(sK6_skl(nil,nil),nil)
| ~ rearsegP(X0,app(sK6_skl(nil,nil),nil))
| ~ ssList(nil)
| ~ rearsegP(nil,X0)
| ~ ssList(sK6_skl(nil,nil))
| ~ ssList(X0)
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f1007,f651]) ).
fof(f1933,plain,
! [X0] :
( ~ sQ71_spl
| app(sK6_skl(X0,app(sK6_skl(nil,nil),nil)),X0) = app(sK6_skl(nil,nil),nil)
| ~ ssList(nil)
| ~ rearsegP(nil,X0)
| ~ ssList(sK6_skl(nil,nil))
| ~ ssList(X0)
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f1007,f650]) ).
fof(f1935,plain,
( ~ sQ71_spl
| ~ ssList(nil)
| frontsegP(app(sK6_skl(nil,nil),nil),sK6_skl(nil,nil))
| ~ ssList(sK6_skl(nil,nil))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f1007,f469]) ).
fof(f1936,plain,
! [X0] :
( ~ sQ71_spl
| ~ ssList(X0)
| ~ ssList(sK6_skl(nil,nil))
| segmentP(app(app(sK6_skl(nil,nil),nil),X0),nil)
| ~ ssList(nil)
| ~ ssList(app(nil,X0)) ),
inference(paramodulation,[status(thm)],[f1007,f471]) ).
fof(f1937,plain,
( ~ sQ71_spl
| ~ ssList(sK6_skl(nil,nil))
| rearsegP(app(sK6_skl(nil,nil),nil),nil)
| ~ ssList(nil)
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f1007,f470]) ).
fof(f1938,definition,
! [X0,X1] :
( sQ204_spl
<=> ( rearsegP(X1,X0)
| ~ rearsegP(X1,app(sK6_skl(nil,nil),nil))
| ~ ssList(X1)
| ~ rearsegP(nil,X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ204_spl])],[split_symbol_definition]) ).
fof(f1941,definition,
( sQ205_spl
<=> ssList(sK6_skl(nil,nil)) ),
introduced(definition,[new_symbols(definition,[sQ205_spl])],[split_symbol_definition]) ).
fof(f1943,plain,
( sQ205_spl
| ~ ssList(sK6_skl(nil,nil)) ),
inference(component_clause,[status(thm)],[f1941]) ).
fof(f1944,plain,
( ~ sQ71_spl
| ~ sQ205_spl
| sQ204_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f1931,f574,f1938,f1941,f1006]) ).
fof(f1945,definition,
! [X0] :
( sQ206_spl
<=> ( X0 = app(sK6_skl(nil,nil),nil)
| ~ rearsegP(X0,app(sK6_skl(nil,nil),nil))
| ~ rearsegP(nil,X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ206_spl])],[split_symbol_definition]) ).
fof(f1948,plain,
( ~ sQ71_spl
| ~ sQ205_spl
| sQ206_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f1932,f574,f1945,f1941,f1006]) ).
fof(f1949,definition,
! [X0] :
( sQ207_spl
<=> ( app(sK6_skl(X0,app(sK6_skl(nil,nil),nil)),X0) = app(sK6_skl(nil,nil),nil)
| ~ rearsegP(nil,X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ207_spl])],[split_symbol_definition]) ).
fof(f1952,plain,
( ~ sQ71_spl
| ~ sQ205_spl
| sQ207_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f1933,f574,f1949,f1941,f1006]) ).
fof(f1954,definition,
( sQ208_spl
<=> frontsegP(app(sK6_skl(nil,nil),nil),sK6_skl(nil,nil)) ),
introduced(definition,[new_symbols(definition,[sQ208_spl])],[split_symbol_definition]) ).
fof(f1957,plain,
( ~ sQ71_spl
| sQ208_spl
| ~ sQ205_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f1935,f574,f1941,f1954,f1006]) ).
fof(f1958,definition,
! [X0] :
( sQ209_spl
<=> ( ~ ssList(X0)
| segmentP(app(app(sK6_skl(nil,nil),nil),X0),nil)
| ~ ssList(app(nil,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ209_spl])],[split_symbol_definition]) ).
fof(f1961,plain,
( ~ sQ71_spl
| ~ sQ205_spl
| ~ sQ14_spl
| sQ209_spl ),
inference(split_clause,[status(thm)],[f1936,f1958,f574,f1941,f1006]) ).
fof(f1962,definition,
( sQ210_spl
<=> rearsegP(app(sK6_skl(nil,nil),nil),nil) ),
introduced(definition,[new_symbols(definition,[sQ210_spl])],[split_symbol_definition]) ).
fof(f1965,plain,
( ~ sQ71_spl
| ~ sQ205_spl
| sQ210_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f1937,f574,f1962,f1941,f1006]) ).
fof(f1966,plain,
( sQ205_spl
| ~ rearsegP(nil,nil)
| ~ ssList(nil)
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f1943,f128]) ).
fof(f1967,plain,
( sQ205_spl
| ~ sQ72_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f1966,f574,f1010,f1941]) ).
fof(f1968,plain,
( sQ72_spl
| ~ sQ69_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1012,f995]) ).
fof(f1969,plain,
( sQ72_spl
| ~ sQ69_spl ),
inference(contradiction_clause,[status(thm)],[f1968]) ).
fof(f2007,plain,
! [X0] :
( ~ sQ42_spl
| ~ ssList(nil)
| ~ rearsegP(nil,X0)
| ~ ssList(nil)
| nil = X0
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f789,f309]) ).
fof(f2008,plain,
! [X0,X1,X2,X3] :
( ~ sQ42_spl
| ~ rearsegP(X3,X1)
| ~ rearsegP(X2,X3)
| ~ ssList(X3)
| ~ rearsegP(nil,X2)
| ~ ssList(X1)
| ~ ssList(X2)
| ~ ssList(nil)
| ~ rearsegP(X1,X0)
| ~ ssList(X1)
| nil = X0
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f789,f568]) ).
fof(f2010,plain,
! [X0,X1,X2] :
( ~ sQ42_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)],[f789,f301]) ).
fof(f2011,definition,
! [X0] :
( sQ211_spl
<=> ( ~ rearsegP(nil,X0)
| nil = X0
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ211_spl])],[split_symbol_definition]) ).
fof(f2015,plain,
( ~ sQ42_spl
| ~ sQ14_spl
| sQ211_spl ),
inference(split_clause,[status(thm)],[f2007,f2011,f574,f785]) ).
fof(f2016,definition,
! [X0,X1,X2,X3] :
( sQ212_spl
<=> ( ~ rearsegP(X3,X1)
| ~ rearsegP(X2,X3)
| ~ ssList(X3)
| ~ rearsegP(nil,X2)
| ~ ssList(X1)
| ~ ssList(X2)
| ~ rearsegP(X1,X0)
| ~ ssList(X1)
| nil = X0
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ212_spl])],[split_symbol_definition]) ).
fof(f2019,plain,
( ~ sQ42_spl
| ~ sQ14_spl
| sQ212_spl ),
inference(split_clause,[status(thm)],[f2008,f2016,f574,f785]) ).
fof(f2021,definition,
! [X0,X1,X2] :
( sQ213_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,[sQ213_spl])],[split_symbol_definition]) ).
fof(f2024,plain,
( ~ sQ42_spl
| ~ sQ14_spl
| sQ213_spl ),
inference(split_clause,[status(thm)],[f2010,f2021,f574,f785]) ).
fof(f2028,plain,
! [X0,X1] :
( ~ sQ94_spl
| rearsegP(X1,X0)
| ~ rearsegP(X1,app(sK47_skl,sK5_skl(sK47_skl,sK47_skl)))
| ~ ssList(sK47_skl)
| ~ ssList(X1)
| ~ rearsegP(sK5_skl(sK47_skl,sK47_skl),X0)
| ~ ssList(sK47_skl)
| ~ ssList(X0)
| ~ ssList(sK5_skl(sK47_skl,sK47_skl)) ),
inference(paramodulation,[status(thm)],[f1166,f652]) ).
fof(f2029,plain,
! [X0] :
( ~ sQ94_spl
| X0 = app(sK47_skl,sK5_skl(sK47_skl,sK47_skl))
| ~ rearsegP(X0,app(sK47_skl,sK5_skl(sK47_skl,sK47_skl)))
| ~ ssList(sK47_skl)
| ~ rearsegP(sK5_skl(sK47_skl,sK47_skl),X0)
| ~ ssList(sK47_skl)
| ~ ssList(X0)
| ~ ssList(sK5_skl(sK47_skl,sK47_skl)) ),
inference(paramodulation,[status(thm)],[f1166,f651]) ).
fof(f2030,plain,
! [X0] :
( ~ sQ94_spl
| app(sK6_skl(X0,app(sK47_skl,sK5_skl(sK47_skl,sK47_skl))),X0) = app(sK47_skl,sK5_skl(sK47_skl,sK47_skl))
| ~ ssList(sK47_skl)
| ~ rearsegP(sK5_skl(sK47_skl,sK47_skl),X0)
| ~ ssList(sK47_skl)
| ~ ssList(X0)
| ~ ssList(sK5_skl(sK47_skl,sK47_skl)) ),
inference(paramodulation,[status(thm)],[f1166,f650]) ).
fof(f2031,plain,
! [X0] :
( ~ sQ94_spl
| rearsegP(sK47_skl,X0)
| ~ rearsegP(sK5_skl(sK47_skl,sK47_skl),X0)
| ~ ssList(sK47_skl)
| ~ ssList(X0)
| ~ ssList(sK5_skl(sK47_skl,sK47_skl)) ),
inference(paramodulation,[status(thm)],[f1166,f307]) ).
fof(f2032,plain,
( ~ sQ94_spl
| ~ ssList(sK5_skl(sK47_skl,sK47_skl))
| frontsegP(app(sK47_skl,sK5_skl(sK47_skl,sK47_skl)),sK47_skl)
| ~ ssList(sK47_skl)
| ~ ssList(sK47_skl) ),
inference(paramodulation,[status(thm)],[f1166,f469]) ).
fof(f2033,plain,
! [X0] :
( ~ sQ94_spl
| ~ ssList(X0)
| ~ ssList(sK47_skl)
| segmentP(app(app(sK47_skl,sK5_skl(sK47_skl,sK47_skl)),X0),sK5_skl(sK47_skl,sK47_skl))
| ~ ssList(sK5_skl(sK47_skl,sK47_skl))
| ~ ssList(app(sK47_skl,X0)) ),
inference(paramodulation,[status(thm)],[f1166,f471]) ).
fof(f2034,plain,
( ~ sQ94_spl
| ~ ssList(sK47_skl)
| rearsegP(app(sK47_skl,sK5_skl(sK47_skl,sK47_skl)),sK5_skl(sK47_skl,sK47_skl))
| ~ ssList(sK5_skl(sK47_skl,sK47_skl))
| ~ ssList(sK47_skl) ),
inference(paramodulation,[status(thm)],[f1166,f470]) ).
fof(f2035,definition,
( sQ214_spl
<=> ssList(sK5_skl(sK47_skl,sK47_skl)) ),
introduced(definition,[new_symbols(definition,[sQ214_spl])],[split_symbol_definition]) ).
fof(f2037,plain,
( sQ214_spl
| ~ ssList(sK5_skl(sK47_skl,sK47_skl)) ),
inference(component_clause,[status(thm)],[f2035]) ).
fof(f2038,definition,
! [X0,X1] :
( sQ215_spl
<=> ( rearsegP(X1,X0)
| ~ rearsegP(X1,app(sK47_skl,sK5_skl(sK47_skl,sK47_skl)))
| ~ ssList(X1)
| ~ rearsegP(sK5_skl(sK47_skl,sK47_skl),X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ215_spl])],[split_symbol_definition]) ).
fof(f2041,plain,
( ~ sQ94_spl
| ~ sQ13_spl
| sQ215_spl
| ~ sQ214_spl ),
inference(split_clause,[status(thm)],[f2028,f2035,f2038,f571,f1165]) ).
fof(f2042,definition,
! [X0] :
( sQ216_spl
<=> ( X0 = app(sK47_skl,sK5_skl(sK47_skl,sK47_skl))
| ~ rearsegP(X0,app(sK47_skl,sK5_skl(sK47_skl,sK47_skl)))
| ~ rearsegP(sK5_skl(sK47_skl,sK47_skl),X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ216_spl])],[split_symbol_definition]) ).
fof(f2045,plain,
( ~ sQ94_spl
| ~ sQ13_spl
| sQ216_spl
| ~ sQ214_spl ),
inference(split_clause,[status(thm)],[f2029,f2035,f2042,f571,f1165]) ).
fof(f2046,definition,
! [X0] :
( sQ217_spl
<=> ( app(sK6_skl(X0,app(sK47_skl,sK5_skl(sK47_skl,sK47_skl))),X0) = app(sK47_skl,sK5_skl(sK47_skl,sK47_skl))
| ~ rearsegP(sK5_skl(sK47_skl,sK47_skl),X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ217_spl])],[split_symbol_definition]) ).
fof(f2049,plain,
( ~ sQ94_spl
| ~ sQ13_spl
| sQ217_spl
| ~ sQ214_spl ),
inference(split_clause,[status(thm)],[f2030,f2035,f2046,f571,f1165]) ).
fof(f2050,definition,
! [X0] :
( sQ218_spl
<=> ( rearsegP(sK47_skl,X0)
| ~ rearsegP(sK5_skl(sK47_skl,sK47_skl),X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ218_spl])],[split_symbol_definition]) ).
fof(f2053,plain,
( ~ sQ94_spl
| ~ sQ13_spl
| sQ218_spl
| ~ sQ214_spl ),
inference(split_clause,[status(thm)],[f2031,f2035,f2050,f571,f1165]) ).
fof(f2054,definition,
( sQ219_spl
<=> frontsegP(app(sK47_skl,sK5_skl(sK47_skl,sK47_skl)),sK47_skl) ),
introduced(definition,[new_symbols(definition,[sQ219_spl])],[split_symbol_definition]) ).
fof(f2057,plain,
( ~ sQ94_spl
| ~ sQ214_spl
| sQ219_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f2032,f571,f2054,f2035,f1165]) ).
fof(f2058,definition,
! [X0] :
( sQ220_spl
<=> ( ~ ssList(X0)
| segmentP(app(app(sK47_skl,sK5_skl(sK47_skl,sK47_skl)),X0),sK5_skl(sK47_skl,sK47_skl))
| ~ ssList(app(sK47_skl,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ220_spl])],[split_symbol_definition]) ).
fof(f2061,plain,
( ~ sQ94_spl
| ~ sQ13_spl
| ~ sQ214_spl
| sQ220_spl ),
inference(split_clause,[status(thm)],[f2033,f2058,f2035,f571,f1165]) ).
fof(f2062,definition,
( sQ221_spl
<=> rearsegP(app(sK47_skl,sK5_skl(sK47_skl,sK47_skl)),sK5_skl(sK47_skl,sK47_skl)) ),
introduced(definition,[new_symbols(definition,[sQ221_spl])],[split_symbol_definition]) ).
fof(f2065,plain,
( ~ sQ94_spl
| sQ221_spl
| ~ sQ214_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f2034,f571,f2035,f2062,f1165]) ).
fof(f2066,plain,
( sQ214_spl
| ~ frontsegP(sK47_skl,sK47_skl)
| ~ ssList(sK47_skl)
| ~ ssList(sK47_skl) ),
inference(resolution,[status(thm)],[f2037,f122]) ).
fof(f2067,definition,
( sQ222_spl
<=> frontsegP(sK47_skl,sK47_skl) ),
introduced(definition,[new_symbols(definition,[sQ222_spl])],[split_symbol_definition]) ).
fof(f2069,plain,
( sQ222_spl
| ~ frontsegP(sK47_skl,sK47_skl) ),
inference(component_clause,[status(thm)],[f2067]) ).
fof(f2070,plain,
( sQ214_spl
| ~ sQ222_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f2066,f571,f2067,f2035]) ).
fof(f2071,plain,
( sQ222_spl
| ~ sQ91_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2069,f1161]) ).
fof(f2072,plain,
( sQ222_spl
| ~ sQ91_spl ),
inference(contradiction_clause,[status(thm)],[f2071]) ).
fof(f2085,plain,
! [X0] :
( ~ sQ35_spl
| ~ sQ28_spl
| ~ ssList(X0)
| segmentP(app(sK48_skl,X0),sK47_skl)
| ~ ssList(app(sK48_skl,X0)) ),
inference(forward_demodulation,[status(thm)],[f707,f739]) ).
fof(f2086,plain,
( ~ sQ83_spl
| ~ sQ35_spl
| ~ sQ28_spl
| ~ ssList(sK5_skl(sK48_skl,sK48_skl))
| segmentP(app(sK48_skl,sK5_skl(sK48_skl,sK48_skl)),sK47_skl)
| ~ ssList(sK48_skl) ),
inference(paramodulation,[status(thm)],[f1110,f2085]) ).
fof(f2088,definition,
( sQ223_spl
<=> segmentP(app(sK48_skl,sK5_skl(sK48_skl,sK48_skl)),sK47_skl) ),
introduced(definition,[new_symbols(definition,[sQ223_spl])],[split_symbol_definition]) ).
fof(f2089,plain,
( ~ sQ223_spl
| segmentP(app(sK48_skl,sK5_skl(sK48_skl,sK48_skl)),sK47_skl) ),
inference(component_clause,[status(thm)],[f2088]) ).
fof(f2091,plain,
( ~ sQ83_spl
| ~ sQ35_spl
| ~ sQ28_spl
| ~ sQ150_spl
| sQ223_spl
| ~ sQ27_spl ),
inference(split_clause,[status(thm)],[f2086,f703,f2088,f1585,f706,f738,f1109]) ).
fof(f2096,plain,
( ~ sQ223_spl
| ~ sQ83_spl
| segmentP(sK48_skl,sK47_skl) ),
inference(forward_demodulation,[status(thm)],[f1110,f2089]) ).
fof(f2097,plain,
( ~ sQ223_spl
| ~ sQ83_spl
| sQ3_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2096,f452]) ).
fof(f2098,plain,
( ~ sQ223_spl
| ~ sQ83_spl
| sQ3_spl ),
inference(contradiction_clause,[status(thm)],[f2097]) ).
fof(f2099,plain,
$false,
inference(sat_refutation,[status(thm)],[f446,f453,f460,f464,f519,f532,f542,f580,f600,f602,f608,f617,f634,f657,f661,f665,f669,f679,f687,f690,f709,f722,f741,f788,f808,f810,f828,f853,f860,f866,f885,f889,f893,f897,f905,f914,f921,f925,f927,f938,f942,f946,f950,f958,f962,f963,f964,f980,f984,f988,f992,f1000,f1009,f1017,f1041,f1062,f1092,f1096,f1100,f1104,f1112,f1119,f1130,f1148,f1152,f1156,f1160,f1168,f1182,f1186,f1190,f1192,f1211,f1215,f1219,f1225,f1227,f1239,f1250,f1254,f1258,f1262,f1297,f1301,f1306,f1315,f1319,f1325,f1333,f1343,f1348,f1358,f1360,f1386,f1390,f1394,f1396,f1428,f1439,f1443,f1447,f1451,f1456,f1458,f1484,f1488,f1492,f1500,f1504,f1509,f1526,f1530,f1534,f1538,f1546,f1550,f1554,f1591,f1595,f1599,f1603,f1607,f1635,f1637,f1655,f1659,f1663,f1667,f1678,f1700,f1704,f1708,f1712,f1716,f1721,f1723,f1742,f1746,f1750,f1754,f1758,f1766,f1770,f1774,f1778,f1813,f1817,f1821,f1825,f1829,f1837,f1841,f1845,f1849,f1944,f1948,f1952,f1957,f1961,f1965,f1967,f1969,f2015,f2019,f2024,f2041,f2045,f2049,f2053,f2057,f2061,f2065,f2070,f2072,f2091,f2098]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWC108+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.34 % Computer : n018.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/0.34 % CPULimit : 300
% 0.08/0.34 % WCLimit : 300
% 0.08/0.34 % DateTime : Mon Sep 21 07:57:59 UTC 2026
% 0.08/0.34 % CPUTime :
% 0.08/0.35 % Drodi V4.1.1
% 0.11/0.51 % Refutation found
% 0.11/0.51 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.11/0.51 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.25/0.55 % Elapsed time: 0.194698 seconds
% 0.25/0.55 % CPU time: 1.223274 seconds
% 0.25/0.55 % Total memory used: 120.987 MB
% 0.25/0.55 % Net memory used: 120.053 MB
%------------------------------------------------------------------------------