%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWC058+1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n012.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:47 PM UTC 2026
% Result : Theorem 0.08s 0.45s
% Output : CNFRefutation 0.08s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 176
% Syntax : Number of formulae : 671 ( 21 unt; 155 def)
% Number of atoms : 2498 ( 271 equ)
% Maximal formula atoms : 17 ( 3 avg)
% Number of connectives : 3355 (1528 ~;1532 |; 82 &)
% ( 167 <=>; 46 =>; 0 <=; 0 <~>)
% Maximal formula depth : 19 ( 5 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 163 ( 161 usr; 154 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 7 con; 0-2 aty)
% Number of variables : 407 ( 383 !; 24 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [U] :
( ssItem(U)
=> ! [V] :
( ssItem(V)
=> ( neq(U,V)
<=> U != V ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,axiom,
? [U] :
( ? [V] :
( U != V
& ssItem(V) )
& ssItem(U) ),
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ( rearsegP(U,V)
<=> ? [W] :
( app(W,V) = U
& ssList(W) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ( segmentP(U,V)
<=> ? [W] :
( ? [X] :
( app(app(W,V),X) = U
& ssList(X) )
& ssList(W) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ( neq(U,V)
<=> U != V ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f17,axiom,
ssList(nil),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f28,axiom,
! [U] :
( ssList(U)
=> app(nil,U) = U ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f45,axiom,
! [U] :
( ssList(U)
=> frontsegP(U,nil) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f47,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ! [W] :
( ssList(W)
=> ( ( rearsegP(V,W)
& rearsegP(U,V) )
=> rearsegP(U,W) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f48,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ( ( rearsegP(V,U)
& rearsegP(U,V) )
=> U = V ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f50,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ! [W] :
( ssList(W)
=> ( rearsegP(U,V)
=> rearsegP(app(W,U),V) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f51,axiom,
! [U] :
( ssList(U)
=> rearsegP(U,nil) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f52,axiom,
! [U] :
( ssList(U)
=> ( rearsegP(nil,U)
<=> nil = U ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f53,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ! [W] :
( ssList(W)
=> ( ( segmentP(V,W)
& segmentP(U,V) )
=> segmentP(U,W) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f54,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ( ( segmentP(V,U)
& segmentP(U,V) )
=> U = V ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f55,axiom,
! [U] :
( ssList(U)
=> segmentP(U,U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f56,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ! [W] :
( ssList(W)
=> ! [X] :
( ssList(X)
=> ( segmentP(U,V)
=> segmentP(app(app(W,U),X),V) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f57,axiom,
! [U] :
( ssList(U)
=> segmentP(U,nil) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f84,axiom,
! [U] :
( ssList(U)
=> app(U,nil) = U ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f96,conjecture,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ! [W] :
( ssList(W)
=> ! [X] :
( ( ( ~ rearsegP(X,W)
| ~ neq(W,nil) )
& ( nil != W
| nil != X ) )
| ( ( ? [Y] :
( segmentP(U,Y)
& segmentP(V,Y)
& neq(Y,nil)
& ssList(Y) )
| ~ neq(V,nil) )
& ( nil = U
| nil != V ) )
| U != W
| V != X
| ~ ssList(X) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f97,negated_conjecture,
~ ! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ! [W] :
( ssList(W)
=> ! [X] :
( ( ( ~ rearsegP(X,W)
| ~ neq(W,nil) )
& ( nil != W
| nil != X ) )
| ( ( ? [Y] :
( segmentP(U,Y)
& segmentP(V,Y)
& neq(Y,nil)
& ssList(Y) )
| ~ neq(V,nil) )
& ( nil = U
| nil != V ) )
| U != W
| V != X
| ~ ssList(X) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f96]) ).
fof(f98,plain,
! [U] :
( ! [V] :
( ( neq(U,V)
<=> U != V )
| ~ ssItem(V) )
| ~ ssItem(U) ),
inference(pre_NNF_transformation,[status(thm)],[f1]) ).
fof(f99,plain,
! [U] :
( ! [V] :
( ( ( U = V
| neq(U,V) )
& ( U != V
| ~ neq(U,V) ) )
| ~ ssItem(V) )
| ~ ssItem(U) ),
inference(NNF_transformation,[status(thm)],[f98]) ).
fof(f101,plain,
! [X0,X1] :
( X0 = X1
| neq(X0,X1)
| ~ ssItem(X1)
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(thm)],[f99]) ).
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(f103,plain,
ssItem(sK0_skl),
inference(cnf_transformation,[status(thm)],[f102]) ).
fof(f104,plain,
ssItem(sK1_skl),
inference(cnf_transformation,[status(thm)],[f102]) ).
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(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(f318,plain,
! [U] :
( segmentP(U,U)
| ~ ssList(U) ),
inference(pre_NNF_transformation,[status(thm)],[f55]) ).
fof(f319,plain,
! [X0] :
( segmentP(X0,X0)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f318]) ).
fof(f320,plain,
! [U] :
( ! [V] :
( ! [W] :
( ! [X] :
( segmentP(app(app(W,U),X),V)
| ~ segmentP(U,V)
| ~ ssList(X) )
| ~ ssList(W) )
| ~ ssList(V) )
| ~ ssList(U) ),
inference(pre_NNF_transformation,[status(thm)],[f56]) ).
fof(f321,plain,
! [X0,X1,X2,X3] :
( segmentP(app(app(X2,X0),X3),X1)
| ~ segmentP(X0,X1)
| ~ ssList(X3)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f320]) ).
fof(f322,plain,
! [U] :
( segmentP(U,nil)
| ~ ssList(U) ),
inference(pre_NNF_transformation,[status(thm)],[f57]) ).
fof(f323,plain,
! [X0] :
( segmentP(X0,nil)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f322]) ).
fof(f388,plain,
! [U] :
( app(U,nil) = U
| ~ ssList(U) ),
inference(pre_NNF_transformation,[status(thm)],[f84]) ).
fof(f389,plain,
! [X0] :
( app(X0,nil) = X0
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f388]) ).
fof(f415,plain,
? [U] :
( ? [V] :
( ? [W] :
( ? [X] :
( ( ( rearsegP(X,W)
& neq(W,nil) )
| ( nil = W
& nil = X ) )
& ( ( ! [Y] :
( ~ segmentP(U,Y)
| ~ segmentP(V,Y)
| ~ neq(Y,nil)
| ~ ssList(Y) )
& 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) )
& ( ( ! [Y] :
( ~ segmentP(U,Y)
| ~ segmentP(V,Y)
| ~ neq(Y,nil)
| ~ ssList(Y) )
& 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) )
& ( ( ! [Y] :
( ~ segmentP(sK47_skl,Y)
| ~ segmentP(sK48_skl,Y)
| ~ neq(Y,nil)
| ~ ssList(Y) )
& 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(f422,plain,
ssList(sK49_skl),
inference(cnf_transformation,[status(thm)],[f419]) ).
fof(f423,plain,
ssList(sK50_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,
! [X0] :
( ~ segmentP(sK47_skl,X0)
| ~ segmentP(sK48_skl,X0)
| ~ neq(X0,nil)
| ~ ssList(X0)
| 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,
! [X0] :
( sQ2_spl
<=> ( ~ segmentP(sK47_skl,X0)
| ~ segmentP(sK48_skl,X0)
| ~ neq(X0,nil)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f448,plain,
! [X0] :
( ~ sQ2_spl
| ~ segmentP(sK47_skl,X0)
| ~ segmentP(sK48_skl,X0)
| ~ neq(X0,nil)
| ~ ssList(X0) ),
inference(component_clause,[status(thm)],[f447]) ).
fof(f450,plain,
( sQ2_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f427,f440,f447]) ).
fof(f451,definition,
( sQ3_spl
<=> sP1_prd(sK50_skl,sK49_skl) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f452,plain,
( ~ sQ3_spl
| sP1_prd(sK50_skl,sK49_skl) ),
inference(component_clause,[status(thm)],[f451]) ).
fof(f454,definition,
( sQ4_spl
<=> neq(sK49_skl,nil) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f455,plain,
( ~ sQ4_spl
| neq(sK49_skl,nil) ),
inference(component_clause,[status(thm)],[f454]) ).
fof(f457,plain,
( sQ4_spl
| sQ3_spl ),
inference(split_clause,[status(thm)],[f428,f451,f454]) ).
fof(f458,definition,
( sQ5_spl
<=> rearsegP(sK50_skl,sK49_skl) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f459,plain,
( ~ sQ5_spl
| rearsegP(sK50_skl,sK49_skl) ),
inference(component_clause,[status(thm)],[f458]) ).
fof(f461,plain,
( sQ5_spl
| sQ3_spl ),
inference(split_clause,[status(thm)],[f429,f451,f458]) ).
fof(f466,plain,
! [X0,X1] :
( ~ ssList(X1)
| frontsegP(app(X0,X1),X0)
| ~ ssList(X0)
| ~ ssList(app(X0,X1)) ),
inference(destructive_equality_resolution,[status(thm)],[f124]) ).
fof(f467,plain,
! [X0,X1] :
( ~ ssList(X0)
| rearsegP(app(X0,X1),X1)
| ~ ssList(X1)
| ~ ssList(app(X0,X1)) ),
inference(destructive_equality_resolution,[status(thm)],[f130]) ).
fof(f468,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(f477,plain,
! [X1] :
( ~ neq(X1,X1)
| ~ ssList(X1)
| ~ ssList(X1) ),
inference(destructive_equality_resolution,[status(thm)],[f219]) ).
fof(f478,plain,
! [X0] :
( ~ neq(X0,X0)
| ~ ssList(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f477]) ).
fof(f492,plain,
! [X0] : ~ sP0_prd(X0,nil),
inference(destructive_equality_resolution,[status(thm)],[f433]) ).
fof(f493,plain,
! [X0] :
( nil = X0
| sP0_prd(nil,X0) ),
inference(destructive_equality_resolution,[status(thm)],[f434]) ).
fof(f497,plain,
( ~ sQ0_spl
| sP0_prd(sK50_skl,sK47_skl) ),
inference(forward_demodulation,[status(thm)],[f424,f441]) ).
fof(f498,plain,
( ~ sQ0_spl
| sP0_prd(sK50_skl,sK49_skl) ),
inference(forward_demodulation,[status(thm)],[f425,f497]) ).
fof(f499,plain,
! [X0] :
( X0 = sK0_skl
| neq(X0,sK0_skl)
| ~ ssItem(X0) ),
inference(resolution,[status(thm)],[f103,f101]) ).
fof(f501,plain,
! [X0] :
( X0 = sK1_skl
| neq(X0,sK1_skl)
| ~ ssItem(X0) ),
inference(resolution,[status(thm)],[f104,f101]) ).
fof(f503,plain,
( ~ sQ0_spl
| nil = sK50_skl ),
inference(resolution,[status(thm)],[f432,f498]) ).
fof(f504,plain,
( ~ sQ0_spl
| sP0_prd(nil,sK49_skl) ),
inference(backward_demodulation,[status(thm)],[f503,f498]) ).
fof(f505,plain,
( ~ sQ3_spl
| ~ sQ0_spl
| sP1_prd(nil,sK49_skl) ),
inference(backward_demodulation,[status(thm)],[f503,f452]) ).
fof(f510,plain,
! [X0] :
( nil = nil
| nil = X0 ),
inference(resolution,[status(thm)],[f493,f432]) ).
fof(f511,definition,
! [X0] :
( sQ6_spl
<=> nil = X0 ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f512,plain,
! [X0] :
( ~ sQ6_spl
| nil = X0 ),
inference(component_clause,[status(thm)],[f511]) ).
fof(f514,definition,
( sQ7_spl
<=> nil = nil ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f517,plain,
( sQ7_spl
| sQ6_spl ),
inference(split_clause,[status(thm)],[f510,f511,f514]) ).
fof(f518,plain,
! [X0,X1] :
( ~ sQ6_spl
| X0 = X1 ),
inference(paramodulation,[status(thm)],[f512,f512]) ).
fof(f532,plain,
( ~ sQ6_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f105,f518]) ).
fof(f533,plain,
~ sQ6_spl,
inference(contradiction_clause,[status(thm)],[f532]) ).
fof(f553,plain,
( ~ sQ3_spl
| ~ sQ0_spl
| nil = sK49_skl ),
inference(resolution,[status(thm)],[f438,f505]) ).
fof(f557,plain,
( ~ sQ0_spl
| ~ sQ3_spl
| sP0_prd(nil,nil) ),
inference(backward_demodulation,[status(thm)],[f553,f504]) ).
fof(f559,plain,
( ~ sQ0_spl
| ~ sQ3_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f557,f492]) ).
fof(f560,plain,
( ~ sQ0_spl
| ~ sQ3_spl ),
inference(contradiction_clause,[status(thm)],[f559]) ).
fof(f561,plain,
( ~ sQ5_spl
| ~ sQ0_spl
| rearsegP(nil,sK49_skl) ),
inference(forward_demodulation,[status(thm)],[f503,f459]) ).
fof(f567,plain,
! [X0] :
( ~ sQ2_spl
| ~ segmentP(sK49_skl,X0)
| ~ segmentP(sK48_skl,X0)
| ~ neq(X0,nil)
| ~ ssList(X0) ),
inference(forward_demodulation,[status(thm)],[f425,f448]) ).
fof(f569,plain,
( ~ sQ1_spl
| neq(sK50_skl,nil) ),
inference(forward_demodulation,[status(thm)],[f424,f444]) ).
fof(f571,plain,
( ~ sQ3_spl
| nil = sK50_skl ),
inference(resolution,[status(thm)],[f452,f437]) ).
fof(f575,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(f577,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)],[f575]) ).
fof(f578,plain,
( ~ sQ1_spl
| ~ sQ3_spl
| neq(nil,nil) ),
inference(backward_demodulation,[status(thm)],[f571,f569]) ).
fof(f584,plain,
( ~ sQ1_spl
| ~ sQ3_spl
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f578,f478]) ).
fof(f585,plain,
( ~ sQ1_spl
| ~ sQ3_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f584,f223]) ).
fof(f586,plain,
( ~ sQ1_spl
| ~ sQ3_spl ),
inference(contradiction_clause,[status(thm)],[f585]) ).
fof(f591,plain,
( ~ sQ5_spl
| ~ sQ0_spl
| sK49_skl = nil
| ~ rearsegP(sK49_skl,nil)
| ~ ssList(nil)
| ~ ssList(sK49_skl) ),
inference(resolution,[status(thm)],[f561,f303]) ).
fof(f592,definition,
( sQ12_spl
<=> ssList(sK49_skl) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f594,plain,
( sQ12_spl
| ~ ssList(sK49_skl) ),
inference(component_clause,[status(thm)],[f592]) ).
fof(f595,definition,
( sQ13_spl
<=> ssList(nil) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f597,plain,
( sQ13_spl
| ~ ssList(nil) ),
inference(component_clause,[status(thm)],[f595]) ).
fof(f598,definition,
( sQ14_spl
<=> rearsegP(sK49_skl,nil) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f599,plain,
( ~ sQ14_spl
| rearsegP(sK49_skl,nil) ),
inference(component_clause,[status(thm)],[f598]) ).
fof(f600,plain,
( sQ14_spl
| ~ rearsegP(sK49_skl,nil) ),
inference(component_clause,[status(thm)],[f598]) ).
fof(f601,definition,
( sQ15_spl
<=> sK49_skl = nil ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f602,plain,
( ~ sQ15_spl
| sK49_skl = nil ),
inference(component_clause,[status(thm)],[f601]) ).
fof(f604,plain,
( ~ sQ5_spl
| ~ sQ0_spl
| sQ15_spl
| ~ sQ14_spl
| ~ sQ13_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f591,f592,f595,f598,f601,f440,f458]) ).
fof(f606,plain,
( ~ sQ4_spl
| ~ sQ15_spl
| neq(nil,nil) ),
inference(backward_demodulation,[status(thm)],[f602,f455]) ).
fof(f612,definition,
( sQ16_spl
<=> rearsegP(nil,nil) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f614,plain,
( sQ16_spl
| ~ rearsegP(nil,nil) ),
inference(component_clause,[status(thm)],[f612]) ).
fof(f617,definition,
( sQ17_spl
<=> ssList(sK50_skl) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f619,plain,
( sQ17_spl
| ~ ssList(sK50_skl) ),
inference(component_clause,[status(thm)],[f617]) ).
fof(f627,plain,
( sQ12_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f594,f422]) ).
fof(f628,plain,
sQ12_spl,
inference(contradiction_clause,[status(thm)],[f627]) ).
fof(f630,plain,
( sQ13_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f597,f223]) ).
fof(f631,plain,
sQ13_spl,
inference(contradiction_clause,[status(thm)],[f630]) ).
fof(f636,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(f637,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)],[f636]) ).
fof(f638,plain,
! [X0] :
( nil = X0
| ~ rearsegP(nil,X0)
| ~ ssList(X0)
| ~ ssList(nil)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f309,f303]) ).
fof(f639,definition,
! [X0] :
( sQ20_spl
<=> ( nil = X0
| ~ rearsegP(nil,X0)
| ~ ssList(X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f642,plain,
( ~ sQ13_spl
| sQ20_spl ),
inference(split_clause,[status(thm)],[f638,f639,f595]) ).
fof(f650,plain,
( sQ14_spl
| ~ ssList(sK49_skl) ),
inference(resolution,[status(thm)],[f600,f309]) ).
fof(f652,plain,
( sQ14_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f650,f592,f598]) ).
fof(f662,plain,
( sQ17_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f619,f423]) ).
fof(f663,plain,
sQ17_spl,
inference(contradiction_clause,[status(thm)],[f662]) ).
fof(f666,plain,
( ~ sQ5_spl
| app(sK6_skl(sK49_skl,sK50_skl),sK49_skl) = sK50_skl
| ~ ssList(sK49_skl)
| ~ ssList(sK50_skl) ),
inference(resolution,[status(thm)],[f129,f459]) ).
fof(f667,plain,
! [X0,X1,X2] :
( ~ rearsegP(X1,X2)
| ~ ssList(X0)
| ~ ssList(X2)
| ~ ssList(X1)
| app(sK6_skl(X2,app(X0,X1)),X2) = app(X0,X1)
| ~ ssList(X2)
| ~ ssList(app(X0,X1)) ),
inference(resolution,[status(thm)],[f129,f307]) ).
fof(f668,plain,
! [X0] :
( ~ ssList(X0)
| app(sK6_skl(nil,X0),nil) = X0
| ~ ssList(nil)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f129,f309]) ).
fof(f669,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(f671,definition,
( sQ23_spl
<=> app(sK6_skl(sK49_skl,sK50_skl),sK49_skl) = sK50_skl ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f672,plain,
( ~ sQ23_spl
| app(sK6_skl(sK49_skl,sK50_skl),sK49_skl) = sK50_skl ),
inference(component_clause,[status(thm)],[f671]) ).
fof(f674,plain,
( ~ sQ5_spl
| sQ23_spl
| ~ sQ12_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f666,f617,f592,f671,f458]) ).
fof(f675,plain,
! [X0,X1,X2] :
( ~ rearsegP(X1,X2)
| ~ ssList(X0)
| ~ ssList(X1)
| app(sK6_skl(X2,app(X0,X1)),X2) = app(X0,X1)
| ~ ssList(X2)
| ~ ssList(app(X0,X1)) ),
inference(duplicate_literals_removal,[status(thm)],[f667]) ).
fof(f676,definition,
! [X0] :
( sQ24_spl
<=> ( ~ ssList(X0)
| app(sK6_skl(nil,X0),nil) = X0
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f679,plain,
( ~ sQ13_spl
| sQ24_spl ),
inference(split_clause,[status(thm)],[f668,f676,f595]) ).
fof(f680,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)],[f669]) ).
fof(f684,plain,
( ~ sQ14_spl
| app(sK6_skl(nil,sK49_skl),nil) = sK49_skl
| ~ ssList(nil)
| ~ ssList(sK49_skl) ),
inference(resolution,[status(thm)],[f599,f129]) ).
fof(f685,plain,
( ~ sQ14_spl
| nil = sK49_skl
| ~ rearsegP(nil,sK49_skl)
| ~ ssList(sK49_skl)
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f599,f303]) ).
fof(f686,definition,
( sQ25_spl
<=> app(sK6_skl(nil,sK49_skl),nil) = sK49_skl ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f687,plain,
( ~ sQ25_spl
| app(sK6_skl(nil,sK49_skl),nil) = sK49_skl ),
inference(component_clause,[status(thm)],[f686]) ).
fof(f689,plain,
( ~ sQ14_spl
| sQ25_spl
| ~ sQ13_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f684,f592,f595,f686,f598]) ).
fof(f690,definition,
( sQ26_spl
<=> rearsegP(nil,sK49_skl) ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f692,plain,
( sQ26_spl
| ~ rearsegP(nil,sK49_skl) ),
inference(component_clause,[status(thm)],[f690]) ).
fof(f693,plain,
( ~ sQ14_spl
| sQ15_spl
| ~ sQ26_spl
| ~ sQ12_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f685,f595,f592,f690,f601,f598]) ).
fof(f694,plain,
! [X0] :
( ~ sQ2_spl
| ~ segmentP(sK49_skl,X0)
| ~ segmentP(sK50_skl,X0)
| ~ neq(X0,nil)
| ~ ssList(X0) ),
inference(forward_demodulation,[status(thm)],[f424,f567]) ).
fof(f695,plain,
( ~ sQ2_spl
| ~ ssList(sK49_skl)
| ~ segmentP(sK50_skl,sK49_skl)
| ~ neq(sK49_skl,nil)
| ~ ssList(sK49_skl) ),
inference(resolution,[status(thm)],[f694,f319]) ).
fof(f696,definition,
( sQ27_spl
<=> segmentP(sK50_skl,sK49_skl) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f698,plain,
( sQ27_spl
| ~ segmentP(sK50_skl,sK49_skl) ),
inference(component_clause,[status(thm)],[f696]) ).
fof(f699,plain,
( ~ sQ2_spl
| ~ sQ27_spl
| ~ sQ4_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f695,f592,f454,f696,f447]) ).
fof(f718,plain,
( ~ sQ4_spl
| ~ sQ15_spl
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f606,f478]) ).
fof(f719,plain,
( ~ sQ4_spl
| ~ sQ15_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f718,f595,f601,f454]) ).
fof(f721,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(f724,definition,
! [X0,X1] :
( sQ29_spl
<=> ( ~ rearsegP(X1,X0)
| ~ rearsegP(nil,X1)
| ~ ssList(X0)
| ~ ssList(X1)
| nil = X0
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f725,plain,
! [X0,X1] :
( ~ sQ29_spl
| ~ rearsegP(X1,X0)
| ~ rearsegP(nil,X1)
| ~ ssList(X0)
| ~ ssList(X1)
| nil = X0
| ~ ssList(X0) ),
inference(component_clause,[status(thm)],[f724]) ).
fof(f727,plain,
( ~ sQ13_spl
| sQ29_spl ),
inference(split_clause,[status(thm)],[f721,f724,f595]) ).
fof(f729,plain,
! [X0,X1] :
( ~ sQ29_spl
| ~ rearsegP(X1,X0)
| ~ rearsegP(nil,X1)
| ~ ssList(X1)
| nil = X0
| ~ ssList(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f725]) ).
fof(f742,plain,
! [X0] :
( app(nil,sK5_skl(nil,X0)) = X0
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f295,f123]) ).
fof(f743,definition,
! [X0] :
( sQ30_spl
<=> ( app(nil,sK5_skl(nil,X0)) = X0
| ~ ssList(X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f746,plain,
( ~ sQ13_spl
| sQ30_spl ),
inference(split_clause,[status(thm)],[f742,f743,f595]) ).
fof(f752,plain,
! [X0] :
( ~ sQ23_spl
| ~ ssList(X0)
| ~ ssList(sK6_skl(sK49_skl,sK50_skl))
| segmentP(app(app(sK6_skl(sK49_skl,sK50_skl),sK49_skl),X0),sK49_skl)
| ~ ssList(sK49_skl)
| ~ ssList(app(sK50_skl,X0)) ),
inference(paramodulation,[status(thm)],[f672,f468]) ).
fof(f754,definition,
( sQ31_spl
<=> ssList(sK6_skl(sK49_skl,sK50_skl)) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f756,plain,
( sQ31_spl
| ~ ssList(sK6_skl(sK49_skl,sK50_skl)) ),
inference(component_clause,[status(thm)],[f754]) ).
fof(f765,definition,
! [X0] :
( sQ34_spl
<=> ( ~ ssList(X0)
| segmentP(app(app(sK6_skl(sK49_skl,sK50_skl),sK49_skl),X0),sK49_skl)
| ~ ssList(app(sK50_skl,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f766,plain,
! [X0] :
( ~ sQ34_spl
| ~ ssList(X0)
| segmentP(app(app(sK6_skl(sK49_skl,sK50_skl),sK49_skl),X0),sK49_skl)
| ~ ssList(app(sK50_skl,X0)) ),
inference(component_clause,[status(thm)],[f765]) ).
fof(f768,plain,
( ~ sQ23_spl
| ~ sQ31_spl
| ~ sQ12_spl
| sQ34_spl ),
inference(split_clause,[status(thm)],[f752,f765,f592,f754,f671]) ).
fof(f773,plain,
( sQ31_spl
| ~ rearsegP(sK50_skl,sK49_skl)
| ~ ssList(sK49_skl)
| ~ ssList(sK50_skl) ),
inference(resolution,[status(thm)],[f756,f128]) ).
fof(f774,plain,
( sQ31_spl
| ~ sQ5_spl
| ~ sQ12_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f773,f617,f592,f458,f754]) ).
fof(f776,plain,
! [X0] :
( ~ sQ34_spl
| ~ sQ23_spl
| ~ ssList(X0)
| segmentP(app(sK50_skl,X0),sK49_skl)
| ~ ssList(app(sK50_skl,X0)) ),
inference(forward_demodulation,[status(thm)],[f672,f766]) ).
fof(f786,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(f794,definition,
! [X0] :
( sQ39_spl
<=> ( app(app(sK7_skl(nil,X0),nil),sK8_skl(nil,X0)) = X0
| ~ ssList(X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f797,plain,
( ~ sQ13_spl
| sQ39_spl ),
inference(split_clause,[status(thm)],[f786,f794,f595]) ).
fof(f805,plain,
( sK1_skl = sK0_skl
| neq(sK1_skl,sK0_skl) ),
inference(resolution,[status(thm)],[f499,f104]) ).
fof(f807,definition,
( sQ40_spl
<=> neq(sK1_skl,sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f810,definition,
( sQ41_spl
<=> sK1_skl = sK0_skl ),
introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition]) ).
fof(f811,plain,
( ~ sQ41_spl
| sK1_skl = sK0_skl ),
inference(component_clause,[status(thm)],[f810]) ).
fof(f813,plain,
( sQ41_spl
| sQ40_spl ),
inference(split_clause,[status(thm)],[f805,f807,f810]) ).
fof(f819,plain,
( sK0_skl = sK1_skl
| neq(sK0_skl,sK1_skl) ),
inference(resolution,[status(thm)],[f501,f103]) ).
fof(f824,definition,
( sQ44_spl
<=> neq(sK0_skl,sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition]) ).
fof(f827,plain,
( sQ41_spl
| sQ44_spl ),
inference(split_clause,[status(thm)],[f819,f824,f810]) ).
fof(f828,plain,
( ~ sQ41_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f811,f105]) ).
fof(f829,plain,
~ sQ41_spl,
inference(contradiction_clause,[status(thm)],[f828]) ).
fof(f830,plain,
! [X0,X1] :
( ~ ssList(X1)
| segmentP(X0,nil)
| ~ segmentP(X0,X1)
| ~ ssList(nil)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f315,f323]) ).
fof(f832,definition,
! [X0,X1] :
( sQ45_spl
<=> ( ~ ssList(X1)
| segmentP(X0,nil)
| ~ segmentP(X0,X1)
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition]) ).
fof(f835,plain,
( ~ sQ13_spl
| sQ45_spl ),
inference(split_clause,[status(thm)],[f830,f832,f595]) ).
fof(f837,plain,
! [X0] :
( ~ ssList(X0)
| nil = X0
| ~ segmentP(nil,X0)
| ~ ssList(X0)
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f317,f323]) ).
fof(f839,definition,
! [X0] :
( sQ46_spl
<=> ( ~ ssList(X0)
| nil = X0
| ~ segmentP(nil,X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition]) ).
fof(f842,plain,
( sQ46_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f837,f595,f839]) ).
fof(f846,plain,
app(nil,sK49_skl) = sK49_skl,
inference(resolution,[status(thm)],[f249,f422]) ).
fof(f849,plain,
app(nil,sK50_skl) = sK50_skl,
inference(resolution,[status(thm)],[f249,f423]) ).
fof(f853,plain,
app(nil,nil) = nil,
inference(resolution,[status(thm)],[f249,f223]) ).
fof(f854,plain,
( ~ ssList(sK49_skl)
| frontsegP(app(nil,sK49_skl),nil)
| ~ ssList(nil)
| ~ ssList(sK49_skl) ),
inference(paramodulation,[status(thm)],[f846,f466]) ).
fof(f855,plain,
! [X0] :
( rearsegP(sK49_skl,X0)
| ~ rearsegP(sK49_skl,X0)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(sK49_skl) ),
inference(paramodulation,[status(thm)],[f846,f307]) ).
fof(f856,plain,
! [X0] :
( ~ ssList(X0)
| ~ ssList(nil)
| segmentP(app(app(nil,sK49_skl),X0),sK49_skl)
| ~ ssList(sK49_skl)
| ~ ssList(app(sK49_skl,X0)) ),
inference(paramodulation,[status(thm)],[f846,f468]) ).
fof(f857,plain,
( ~ ssList(nil)
| rearsegP(app(nil,sK49_skl),sK49_skl)
| ~ ssList(sK49_skl)
| ~ ssList(sK49_skl) ),
inference(paramodulation,[status(thm)],[f846,f467]) ).
fof(f858,definition,
( sQ47_spl
<=> frontsegP(app(nil,sK49_skl),nil) ),
introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition]) ).
fof(f859,plain,
( ~ sQ47_spl
| frontsegP(app(nil,sK49_skl),nil) ),
inference(component_clause,[status(thm)],[f858]) ).
fof(f861,plain,
( sQ47_spl
| ~ sQ13_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f854,f592,f595,f858]) ).
fof(f862,definition,
! [X0] :
( sQ48_spl
<=> ( rearsegP(sK49_skl,X0)
| ~ rearsegP(sK49_skl,X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition]) ).
fof(f865,plain,
( ~ sQ13_spl
| sQ48_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f855,f592,f862,f595]) ).
fof(f866,definition,
! [X0] :
( sQ49_spl
<=> ( ~ ssList(X0)
| segmentP(app(app(nil,sK49_skl),X0),sK49_skl)
| ~ ssList(app(sK49_skl,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition]) ).
fof(f869,plain,
( ~ sQ13_spl
| ~ sQ12_spl
| sQ49_spl ),
inference(split_clause,[status(thm)],[f856,f866,f592,f595]) ).
fof(f870,definition,
( sQ50_spl
<=> rearsegP(app(nil,sK49_skl),sK49_skl) ),
introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition]) ).
fof(f871,plain,
( ~ sQ50_spl
| rearsegP(app(nil,sK49_skl),sK49_skl) ),
inference(component_clause,[status(thm)],[f870]) ).
fof(f873,plain,
( ~ sQ13_spl
| sQ50_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f857,f592,f870,f595]) ).
fof(f874,plain,
( ~ sQ47_spl
| frontsegP(sK49_skl,nil) ),
inference(forward_demodulation,[status(thm)],[f846,f859]) ).
fof(f876,plain,
( ~ sQ50_spl
| rearsegP(sK49_skl,sK49_skl) ),
inference(forward_demodulation,[status(thm)],[f846,f871]) ).
fof(f877,plain,
( ~ sQ47_spl
| app(nil,sK5_skl(nil,sK49_skl)) = sK49_skl
| ~ ssList(nil)
| ~ ssList(sK49_skl) ),
inference(resolution,[status(thm)],[f874,f123]) ).
fof(f878,definition,
( sQ51_spl
<=> app(nil,sK5_skl(nil,sK49_skl)) = sK49_skl ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f879,plain,
( ~ sQ51_spl
| app(nil,sK5_skl(nil,sK49_skl)) = sK49_skl ),
inference(component_clause,[status(thm)],[f878]) ).
fof(f881,plain,
( ~ sQ47_spl
| sQ51_spl
| ~ sQ13_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f877,f592,f595,f878,f858]) ).
fof(f882,plain,
( ~ sQ50_spl
| app(sK6_skl(sK49_skl,sK49_skl),sK49_skl) = sK49_skl
| ~ ssList(sK49_skl)
| ~ ssList(sK49_skl) ),
inference(resolution,[status(thm)],[f876,f129]) ).
fof(f883,plain,
( ~ sQ50_spl
| sK49_skl = sK49_skl
| ~ rearsegP(sK49_skl,sK49_skl)
| ~ ssList(sK49_skl)
| ~ ssList(sK49_skl) ),
inference(resolution,[status(thm)],[f876,f303]) ).
fof(f884,definition,
( sQ52_spl
<=> app(sK6_skl(sK49_skl,sK49_skl),sK49_skl) = sK49_skl ),
introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition]) ).
fof(f885,plain,
( ~ sQ52_spl
| app(sK6_skl(sK49_skl,sK49_skl),sK49_skl) = sK49_skl ),
inference(component_clause,[status(thm)],[f884]) ).
fof(f887,plain,
( ~ sQ50_spl
| sQ52_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f882,f592,f884,f870]) ).
fof(f888,definition,
( sQ53_spl
<=> rearsegP(sK49_skl,sK49_skl) ),
introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition]) ).
fof(f890,plain,
( sQ53_spl
| ~ rearsegP(sK49_skl,sK49_skl) ),
inference(component_clause,[status(thm)],[f888]) ).
fof(f891,definition,
( sQ54_spl
<=> sK49_skl = sK49_skl ),
introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition]) ).
fof(f894,plain,
( ~ sQ50_spl
| sQ54_spl
| ~ sQ53_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f883,f592,f888,f891,f870]) ).
fof(f895,plain,
( sQ53_spl
| ~ sQ50_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f890,f876]) ).
fof(f896,plain,
( sQ53_spl
| ~ sQ50_spl ),
inference(contradiction_clause,[status(thm)],[f895]) ).
fof(f897,plain,
( ~ ssList(sK50_skl)
| frontsegP(app(nil,sK50_skl),nil)
| ~ ssList(nil)
| ~ ssList(sK50_skl) ),
inference(paramodulation,[status(thm)],[f849,f466]) ).
fof(f898,plain,
! [X0] :
( rearsegP(sK50_skl,X0)
| ~ rearsegP(sK50_skl,X0)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(sK50_skl) ),
inference(paramodulation,[status(thm)],[f849,f307]) ).
fof(f899,plain,
! [X0] :
( ~ ssList(X0)
| ~ ssList(nil)
| segmentP(app(app(nil,sK50_skl),X0),sK50_skl)
| ~ ssList(sK50_skl)
| ~ ssList(app(sK50_skl,X0)) ),
inference(paramodulation,[status(thm)],[f849,f468]) ).
fof(f900,plain,
( ~ ssList(nil)
| rearsegP(app(nil,sK50_skl),sK50_skl)
| ~ ssList(sK50_skl)
| ~ ssList(sK50_skl) ),
inference(paramodulation,[status(thm)],[f849,f467]) ).
fof(f901,definition,
( sQ55_spl
<=> frontsegP(app(nil,sK50_skl),nil) ),
introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition]) ).
fof(f902,plain,
( ~ sQ55_spl
| frontsegP(app(nil,sK50_skl),nil) ),
inference(component_clause,[status(thm)],[f901]) ).
fof(f904,plain,
( sQ55_spl
| ~ sQ13_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f897,f617,f595,f901]) ).
fof(f905,definition,
! [X0] :
( sQ56_spl
<=> ( rearsegP(sK50_skl,X0)
| ~ rearsegP(sK50_skl,X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition]) ).
fof(f908,plain,
( ~ sQ13_spl
| sQ56_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f898,f617,f905,f595]) ).
fof(f909,definition,
! [X0] :
( sQ57_spl
<=> ( ~ ssList(X0)
| segmentP(app(app(nil,sK50_skl),X0),sK50_skl)
| ~ ssList(app(sK50_skl,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition]) ).
fof(f912,plain,
( ~ sQ13_spl
| ~ sQ17_spl
| sQ57_spl ),
inference(split_clause,[status(thm)],[f899,f909,f617,f595]) ).
fof(f913,definition,
( sQ58_spl
<=> rearsegP(app(nil,sK50_skl),sK50_skl) ),
introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition]) ).
fof(f914,plain,
( ~ sQ58_spl
| rearsegP(app(nil,sK50_skl),sK50_skl) ),
inference(component_clause,[status(thm)],[f913]) ).
fof(f916,plain,
( ~ sQ13_spl
| sQ58_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f900,f617,f913,f595]) ).
fof(f917,plain,
( ~ sQ55_spl
| frontsegP(sK50_skl,nil) ),
inference(forward_demodulation,[status(thm)],[f849,f902]) ).
fof(f919,plain,
( ~ sQ58_spl
| rearsegP(sK50_skl,sK50_skl) ),
inference(forward_demodulation,[status(thm)],[f849,f914]) ).
fof(f920,plain,
( ~ sQ55_spl
| app(nil,sK5_skl(nil,sK50_skl)) = sK50_skl
| ~ ssList(nil)
| ~ ssList(sK50_skl) ),
inference(resolution,[status(thm)],[f917,f123]) ).
fof(f921,definition,
( sQ59_spl
<=> app(nil,sK5_skl(nil,sK50_skl)) = sK50_skl ),
introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition]) ).
fof(f922,plain,
( ~ sQ59_spl
| app(nil,sK5_skl(nil,sK50_skl)) = sK50_skl ),
inference(component_clause,[status(thm)],[f921]) ).
fof(f924,plain,
( ~ sQ55_spl
| sQ59_spl
| ~ sQ13_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f920,f617,f595,f921,f901]) ).
fof(f925,plain,
( ~ sQ58_spl
| app(sK6_skl(sK50_skl,sK50_skl),sK50_skl) = sK50_skl
| ~ ssList(sK50_skl)
| ~ ssList(sK50_skl) ),
inference(resolution,[status(thm)],[f919,f129]) ).
fof(f926,plain,
( ~ sQ58_spl
| sK50_skl = sK50_skl
| ~ rearsegP(sK50_skl,sK50_skl)
| ~ ssList(sK50_skl)
| ~ ssList(sK50_skl) ),
inference(resolution,[status(thm)],[f919,f303]) ).
fof(f927,definition,
( sQ60_spl
<=> app(sK6_skl(sK50_skl,sK50_skl),sK50_skl) = sK50_skl ),
introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition]) ).
fof(f928,plain,
( ~ sQ60_spl
| app(sK6_skl(sK50_skl,sK50_skl),sK50_skl) = sK50_skl ),
inference(component_clause,[status(thm)],[f927]) ).
fof(f930,plain,
( ~ sQ58_spl
| sQ60_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f925,f617,f927,f913]) ).
fof(f931,definition,
( sQ61_spl
<=> rearsegP(sK50_skl,sK50_skl) ),
introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition]) ).
fof(f933,plain,
( sQ61_spl
| ~ rearsegP(sK50_skl,sK50_skl) ),
inference(component_clause,[status(thm)],[f931]) ).
fof(f934,definition,
( sQ62_spl
<=> sK50_skl = sK50_skl ),
introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition]) ).
fof(f937,plain,
( ~ sQ58_spl
| sQ62_spl
| ~ sQ61_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f926,f617,f931,f934,f913]) ).
fof(f938,plain,
( sQ61_spl
| ~ sQ58_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f933,f919]) ).
fof(f939,plain,
( sQ61_spl
| ~ sQ58_spl ),
inference(contradiction_clause,[status(thm)],[f938]) ).
fof(f940,plain,
( ~ ssList(nil)
| frontsegP(app(nil,nil),nil)
| ~ ssList(nil)
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f853,f466]) ).
fof(f941,plain,
! [X0] :
( rearsegP(nil,X0)
| ~ rearsegP(nil,X0)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f853,f307]) ).
fof(f942,plain,
! [X0] :
( ~ ssList(X0)
| ~ ssList(nil)
| segmentP(app(app(nil,nil),X0),nil)
| ~ ssList(nil)
| ~ ssList(app(nil,X0)) ),
inference(paramodulation,[status(thm)],[f853,f468]) ).
fof(f943,plain,
( ~ ssList(nil)
| rearsegP(app(nil,nil),nil)
| ~ ssList(nil)
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f853,f467]) ).
fof(f944,definition,
( sQ63_spl
<=> frontsegP(app(nil,nil),nil) ),
introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition]) ).
fof(f945,plain,
( ~ sQ63_spl
| frontsegP(app(nil,nil),nil) ),
inference(component_clause,[status(thm)],[f944]) ).
fof(f947,plain,
( sQ63_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f940,f595,f944]) ).
fof(f948,definition,
! [X0] :
( sQ64_spl
<=> ( rearsegP(nil,X0)
| ~ rearsegP(nil,X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition]) ).
fof(f951,plain,
( sQ64_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f941,f595,f948]) ).
fof(f952,definition,
! [X0] :
( sQ65_spl
<=> ( ~ ssList(X0)
| segmentP(app(app(nil,nil),X0),nil)
| ~ ssList(app(nil,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition]) ).
fof(f955,plain,
( ~ sQ13_spl
| sQ65_spl ),
inference(split_clause,[status(thm)],[f942,f952,f595]) ).
fof(f956,definition,
( sQ66_spl
<=> rearsegP(app(nil,nil),nil) ),
introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition]) ).
fof(f957,plain,
( ~ sQ66_spl
| rearsegP(app(nil,nil),nil) ),
inference(component_clause,[status(thm)],[f956]) ).
fof(f959,plain,
( sQ66_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f943,f595,f956]) ).
fof(f960,plain,
( ~ sQ63_spl
| frontsegP(nil,nil) ),
inference(forward_demodulation,[status(thm)],[f853,f945]) ).
fof(f962,plain,
( ~ sQ66_spl
| rearsegP(nil,nil) ),
inference(forward_demodulation,[status(thm)],[f853,f957]) ).
fof(f963,plain,
( ~ sQ63_spl
| app(nil,sK5_skl(nil,nil)) = nil
| ~ ssList(nil)
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f960,f123]) ).
fof(f964,definition,
( sQ67_spl
<=> app(nil,sK5_skl(nil,nil)) = nil ),
introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition]) ).
fof(f965,plain,
( ~ sQ67_spl
| app(nil,sK5_skl(nil,nil)) = nil ),
inference(component_clause,[status(thm)],[f964]) ).
fof(f967,plain,
( ~ sQ63_spl
| sQ67_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f963,f595,f964,f944]) ).
fof(f969,plain,
( ~ sQ66_spl
| app(sK6_skl(nil,nil),nil) = nil
| ~ ssList(nil)
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f962,f129]) ).
fof(f972,definition,
( sQ68_spl
<=> app(sK6_skl(nil,nil),nil) = nil ),
introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition]) ).
fof(f975,plain,
( ~ sQ66_spl
| sQ68_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f969,f595,f972,f956]) ).
fof(f979,plain,
app(sK49_skl,nil) = sK49_skl,
inference(resolution,[status(thm)],[f389,f422]) ).
fof(f982,plain,
app(sK50_skl,nil) = sK50_skl,
inference(resolution,[status(thm)],[f389,f423]) ).
fof(f987,plain,
( ~ ssList(nil)
| frontsegP(app(sK49_skl,nil),sK49_skl)
| ~ ssList(sK49_skl)
| ~ ssList(sK49_skl) ),
inference(paramodulation,[status(thm)],[f979,f466]) ).
fof(f989,plain,
! [X0] :
( ~ ssList(X0)
| ~ ssList(sK49_skl)
| segmentP(app(app(sK49_skl,nil),X0),nil)
| ~ ssList(nil)
| ~ ssList(app(sK49_skl,X0)) ),
inference(paramodulation,[status(thm)],[f979,f468]) ).
fof(f990,plain,
( ~ ssList(sK49_skl)
| rearsegP(app(sK49_skl,nil),nil)
| ~ ssList(nil)
| ~ ssList(sK49_skl) ),
inference(paramodulation,[status(thm)],[f979,f467]) ).
fof(f991,definition,
( sQ69_spl
<=> frontsegP(app(sK49_skl,nil),sK49_skl) ),
introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition]) ).
fof(f992,plain,
( ~ sQ69_spl
| frontsegP(app(sK49_skl,nil),sK49_skl) ),
inference(component_clause,[status(thm)],[f991]) ).
fof(f994,plain,
( ~ sQ13_spl
| sQ69_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f987,f592,f991,f595]) ).
fof(f995,definition,
! [X0] :
( sQ70_spl
<=> ( rearsegP(sK49_skl,X0)
| ~ rearsegP(nil,X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition]) ).
fof(f999,definition,
! [X0] :
( sQ71_spl
<=> ( ~ ssList(X0)
| segmentP(app(app(sK49_skl,nil),X0),nil)
| ~ ssList(app(sK49_skl,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition]) ).
fof(f1002,plain,
( ~ sQ12_spl
| ~ sQ13_spl
| sQ71_spl ),
inference(split_clause,[status(thm)],[f989,f999,f595,f592]) ).
fof(f1003,definition,
( sQ72_spl
<=> rearsegP(app(sK49_skl,nil),nil) ),
introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition]) ).
fof(f1006,plain,
( sQ72_spl
| ~ sQ13_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f990,f592,f595,f1003]) ).
fof(f1007,plain,
( ~ sQ69_spl
| frontsegP(sK49_skl,sK49_skl) ),
inference(forward_demodulation,[status(thm)],[f979,f992]) ).
fof(f1010,plain,
( ~ sQ69_spl
| app(sK49_skl,sK5_skl(sK49_skl,sK49_skl)) = sK49_skl
| ~ ssList(sK49_skl)
| ~ ssList(sK49_skl) ),
inference(resolution,[status(thm)],[f1007,f123]) ).
fof(f1011,definition,
( sQ73_spl
<=> app(sK49_skl,sK5_skl(sK49_skl,sK49_skl)) = sK49_skl ),
introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition]) ).
fof(f1012,plain,
( ~ sQ73_spl
| app(sK49_skl,sK5_skl(sK49_skl,sK49_skl)) = sK49_skl ),
inference(component_clause,[status(thm)],[f1011]) ).
fof(f1014,plain,
( ~ sQ69_spl
| sQ73_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f1010,f592,f1011,f991]) ).
fof(f1015,plain,
( ~ ssList(nil)
| frontsegP(app(sK50_skl,nil),sK50_skl)
| ~ ssList(sK50_skl)
| ~ ssList(sK50_skl) ),
inference(paramodulation,[status(thm)],[f982,f466]) ).
fof(f1016,plain,
! [X0] :
( rearsegP(sK50_skl,X0)
| ~ rearsegP(nil,X0)
| ~ ssList(sK50_skl)
| ~ ssList(X0)
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f982,f307]) ).
fof(f1017,plain,
! [X0] :
( ~ ssList(X0)
| ~ ssList(sK50_skl)
| segmentP(app(app(sK50_skl,nil),X0),nil)
| ~ ssList(nil)
| ~ ssList(app(sK50_skl,X0)) ),
inference(paramodulation,[status(thm)],[f982,f468]) ).
fof(f1018,plain,
( ~ ssList(sK50_skl)
| rearsegP(app(sK50_skl,nil),nil)
| ~ ssList(nil)
| ~ ssList(sK50_skl) ),
inference(paramodulation,[status(thm)],[f982,f467]) ).
fof(f1019,definition,
( sQ74_spl
<=> frontsegP(app(sK50_skl,nil),sK50_skl) ),
introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition]) ).
fof(f1020,plain,
( ~ sQ74_spl
| frontsegP(app(sK50_skl,nil),sK50_skl) ),
inference(component_clause,[status(thm)],[f1019]) ).
fof(f1022,plain,
( ~ sQ13_spl
| sQ74_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f1015,f617,f1019,f595]) ).
fof(f1023,definition,
! [X0] :
( sQ75_spl
<=> ( rearsegP(sK50_skl,X0)
| ~ rearsegP(nil,X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition]) ).
fof(f1026,plain,
( ~ sQ17_spl
| sQ75_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f1016,f595,f1023,f617]) ).
fof(f1027,definition,
! [X0] :
( sQ76_spl
<=> ( ~ ssList(X0)
| segmentP(app(app(sK50_skl,nil),X0),nil)
| ~ ssList(app(sK50_skl,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition]) ).
fof(f1030,plain,
( ~ sQ17_spl
| ~ sQ13_spl
| sQ76_spl ),
inference(split_clause,[status(thm)],[f1017,f1027,f595,f617]) ).
fof(f1031,definition,
( sQ77_spl
<=> rearsegP(app(sK50_skl,nil),nil) ),
introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition]) ).
fof(f1032,plain,
( ~ sQ77_spl
| rearsegP(app(sK50_skl,nil),nil) ),
inference(component_clause,[status(thm)],[f1031]) ).
fof(f1034,plain,
( sQ77_spl
| ~ sQ13_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f1018,f617,f595,f1031]) ).
fof(f1035,plain,
( ~ sQ74_spl
| frontsegP(sK50_skl,sK50_skl) ),
inference(forward_demodulation,[status(thm)],[f982,f1020]) ).
fof(f1037,plain,
( ~ sQ77_spl
| rearsegP(sK50_skl,nil) ),
inference(forward_demodulation,[status(thm)],[f982,f1032]) ).
fof(f1038,plain,
( ~ sQ74_spl
| app(sK50_skl,sK5_skl(sK50_skl,sK50_skl)) = sK50_skl
| ~ ssList(sK50_skl)
| ~ ssList(sK50_skl) ),
inference(resolution,[status(thm)],[f1035,f123]) ).
fof(f1039,definition,
( sQ78_spl
<=> app(sK50_skl,sK5_skl(sK50_skl,sK50_skl)) = sK50_skl ),
introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition]) ).
fof(f1040,plain,
( ~ sQ78_spl
| app(sK50_skl,sK5_skl(sK50_skl,sK50_skl)) = sK50_skl ),
inference(component_clause,[status(thm)],[f1039]) ).
fof(f1042,plain,
( ~ sQ74_spl
| sQ78_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f1038,f617,f1039,f1019]) ).
fof(f1058,plain,
( ~ sQ77_spl
| app(sK6_skl(nil,sK50_skl),nil) = sK50_skl
| ~ ssList(nil)
| ~ ssList(sK50_skl) ),
inference(resolution,[status(thm)],[f1037,f129]) ).
fof(f1059,plain,
( ~ sQ77_spl
| nil = sK50_skl
| ~ rearsegP(nil,sK50_skl)
| ~ ssList(sK50_skl)
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f1037,f303]) ).
fof(f1060,definition,
( sQ81_spl
<=> app(sK6_skl(nil,sK50_skl),nil) = sK50_skl ),
introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition]) ).
fof(f1063,plain,
( ~ sQ77_spl
| sQ81_spl
| ~ sQ13_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f1058,f617,f595,f1060,f1031]) ).
fof(f1064,definition,
( sQ82_spl
<=> rearsegP(nil,sK50_skl) ),
introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition]) ).
fof(f1066,plain,
( sQ82_spl
| ~ rearsegP(nil,sK50_skl) ),
inference(component_clause,[status(thm)],[f1064]) ).
fof(f1067,definition,
( sQ83_spl
<=> nil = sK50_skl ),
introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition]) ).
fof(f1068,plain,
( ~ sQ83_spl
| nil = sK50_skl ),
inference(component_clause,[status(thm)],[f1067]) ).
fof(f1070,plain,
( ~ sQ77_spl
| sQ83_spl
| ~ sQ82_spl
| ~ sQ17_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f1059,f595,f617,f1064,f1067,f1031]) ).
fof(f1071,plain,
! [X0] :
( sQ82_spl
| ~ rearsegP(X0,sK50_skl)
| ~ rearsegP(nil,X0)
| ~ ssList(sK50_skl)
| ~ ssList(X0)
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f1066,f301]) ).
fof(f1072,definition,
! [X0] :
( sQ84_spl
<=> ( ~ rearsegP(X0,sK50_skl)
| ~ rearsegP(nil,X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition]) ).
fof(f1075,plain,
( sQ82_spl
| ~ sQ17_spl
| sQ84_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f1071,f595,f1072,f617,f1064]) ).
fof(f1087,plain,
( ~ sQ5_spl
| ~ sQ83_spl
| rearsegP(nil,sK49_skl) ),
inference(backward_demodulation,[status(thm)],[f1068,f459]) ).
fof(f1102,plain,
( ~ sQ5_spl
| ~ sQ83_spl
| sQ26_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1087,f692]) ).
fof(f1103,plain,
( ~ sQ5_spl
| ~ sQ83_spl
| sQ26_spl ),
inference(contradiction_clause,[status(thm)],[f1102]) ).
fof(f1112,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(f1114,definition,
! [X0,X1,X2] :
( sQ85_spl
<=> ( ~ ssList(X0)
| segmentP(app(app(X1,X0),X2),nil)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition]) ).
fof(f1117,plain,
( ~ sQ13_spl
| sQ85_spl ),
inference(split_clause,[status(thm)],[f1112,f1114,f595]) ).
fof(f1156,plain,
( ~ sQ25_spl
| ~ ssList(nil)
| frontsegP(app(sK6_skl(nil,sK49_skl),nil),sK6_skl(nil,sK49_skl))
| ~ ssList(sK6_skl(nil,sK49_skl))
| ~ ssList(sK49_skl) ),
inference(paramodulation,[status(thm)],[f687,f466]) ).
fof(f1157,plain,
! [X0] :
( ~ sQ25_spl
| rearsegP(sK49_skl,X0)
| ~ rearsegP(nil,X0)
| ~ ssList(sK6_skl(nil,sK49_skl))
| ~ ssList(X0)
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f687,f307]) ).
fof(f1158,plain,
! [X0] :
( ~ sQ25_spl
| ~ ssList(X0)
| ~ ssList(sK6_skl(nil,sK49_skl))
| segmentP(app(app(sK6_skl(nil,sK49_skl),nil),X0),nil)
| ~ ssList(nil)
| ~ ssList(app(sK49_skl,X0)) ),
inference(paramodulation,[status(thm)],[f687,f468]) ).
fof(f1159,plain,
( ~ sQ25_spl
| ~ ssList(sK6_skl(nil,sK49_skl))
| rearsegP(app(sK6_skl(nil,sK49_skl),nil),nil)
| ~ ssList(nil)
| ~ ssList(sK49_skl) ),
inference(paramodulation,[status(thm)],[f687,f467]) ).
fof(f1160,definition,
( sQ86_spl
<=> ssList(sK6_skl(nil,sK49_skl)) ),
introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition]) ).
fof(f1162,plain,
( sQ86_spl
| ~ ssList(sK6_skl(nil,sK49_skl)) ),
inference(component_clause,[status(thm)],[f1160]) ).
fof(f1163,definition,
( sQ87_spl
<=> frontsegP(app(sK6_skl(nil,sK49_skl),nil),sK6_skl(nil,sK49_skl)) ),
introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition]) ).
fof(f1166,plain,
( ~ sQ25_spl
| ~ sQ13_spl
| sQ87_spl
| ~ sQ86_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f1156,f592,f1160,f1163,f595,f686]) ).
fof(f1167,plain,
( ~ sQ25_spl
| ~ sQ86_spl
| sQ70_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f1157,f595,f995,f1160,f686]) ).
fof(f1168,definition,
! [X0] :
( sQ88_spl
<=> ( ~ ssList(X0)
| segmentP(app(app(sK6_skl(nil,sK49_skl),nil),X0),nil)
| ~ ssList(app(sK49_skl,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition]) ).
fof(f1171,plain,
( ~ sQ25_spl
| ~ sQ86_spl
| ~ sQ13_spl
| sQ88_spl ),
inference(split_clause,[status(thm)],[f1158,f1168,f595,f1160,f686]) ).
fof(f1172,definition,
( sQ89_spl
<=> rearsegP(app(sK6_skl(nil,sK49_skl),nil),nil) ),
introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition]) ).
fof(f1175,plain,
( ~ sQ25_spl
| ~ sQ86_spl
| sQ89_spl
| ~ sQ13_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f1159,f592,f595,f1172,f1160,f686]) ).
fof(f1180,plain,
( sQ86_spl
| ~ rearsegP(sK49_skl,nil)
| ~ ssList(nil)
| ~ ssList(sK49_skl) ),
inference(resolution,[status(thm)],[f1162,f128]) ).
fof(f1181,plain,
( sQ86_spl
| ~ sQ14_spl
| ~ sQ13_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f1180,f592,f595,f598,f1160]) ).
fof(f1203,plain,
( ~ sQ51_spl
| ~ ssList(sK5_skl(nil,sK49_skl))
| frontsegP(app(nil,sK5_skl(nil,sK49_skl)),nil)
| ~ ssList(nil)
| ~ ssList(sK49_skl) ),
inference(paramodulation,[status(thm)],[f879,f466]) ).
fof(f1204,plain,
! [X0] :
( ~ sQ51_spl
| rearsegP(sK49_skl,X0)
| ~ rearsegP(sK5_skl(nil,sK49_skl),X0)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(sK5_skl(nil,sK49_skl)) ),
inference(paramodulation,[status(thm)],[f879,f307]) ).
fof(f1205,plain,
! [X0] :
( ~ sQ51_spl
| ~ ssList(X0)
| ~ ssList(nil)
| segmentP(app(app(nil,sK5_skl(nil,sK49_skl)),X0),sK5_skl(nil,sK49_skl))
| ~ ssList(sK5_skl(nil,sK49_skl))
| ~ ssList(app(sK49_skl,X0)) ),
inference(paramodulation,[status(thm)],[f879,f468]) ).
fof(f1206,plain,
( ~ sQ51_spl
| ~ ssList(nil)
| rearsegP(app(nil,sK5_skl(nil,sK49_skl)),sK5_skl(nil,sK49_skl))
| ~ ssList(sK5_skl(nil,sK49_skl))
| ~ ssList(sK49_skl) ),
inference(paramodulation,[status(thm)],[f879,f467]) ).
fof(f1207,definition,
( sQ90_spl
<=> frontsegP(app(nil,sK5_skl(nil,sK49_skl)),nil) ),
introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition]) ).
fof(f1210,definition,
( sQ91_spl
<=> ssList(sK5_skl(nil,sK49_skl)) ),
introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition]) ).
fof(f1212,plain,
( sQ91_spl
| ~ ssList(sK5_skl(nil,sK49_skl)) ),
inference(component_clause,[status(thm)],[f1210]) ).
fof(f1213,plain,
( ~ sQ51_spl
| ~ sQ91_spl
| sQ90_spl
| ~ sQ13_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f1203,f592,f595,f1207,f1210,f878]) ).
fof(f1214,definition,
! [X0] :
( sQ92_spl
<=> ( rearsegP(sK49_skl,X0)
| ~ rearsegP(sK5_skl(nil,sK49_skl),X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ92_spl])],[split_symbol_definition]) ).
fof(f1217,plain,
( ~ sQ51_spl
| ~ sQ13_spl
| sQ92_spl
| ~ sQ91_spl ),
inference(split_clause,[status(thm)],[f1204,f1210,f1214,f595,f878]) ).
fof(f1218,definition,
! [X0] :
( sQ93_spl
<=> ( ~ ssList(X0)
| segmentP(app(app(nil,sK5_skl(nil,sK49_skl)),X0),sK5_skl(nil,sK49_skl))
| ~ ssList(app(sK49_skl,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ93_spl])],[split_symbol_definition]) ).
fof(f1221,plain,
( ~ sQ51_spl
| ~ sQ13_spl
| ~ sQ91_spl
| sQ93_spl ),
inference(split_clause,[status(thm)],[f1205,f1218,f1210,f595,f878]) ).
fof(f1222,definition,
( sQ94_spl
<=> rearsegP(app(nil,sK5_skl(nil,sK49_skl)),sK5_skl(nil,sK49_skl)) ),
introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition]) ).
fof(f1225,plain,
( ~ sQ51_spl
| ~ sQ13_spl
| sQ94_spl
| ~ sQ91_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f1206,f592,f1210,f1222,f595,f878]) ).
fof(f1226,plain,
( sQ91_spl
| ~ frontsegP(sK49_skl,nil)
| ~ ssList(nil)
| ~ ssList(sK49_skl) ),
inference(resolution,[status(thm)],[f1212,f122]) ).
fof(f1227,definition,
( sQ95_spl
<=> frontsegP(sK49_skl,nil) ),
introduced(definition,[new_symbols(definition,[sQ95_spl])],[split_symbol_definition]) ).
fof(f1229,plain,
( sQ95_spl
| ~ frontsegP(sK49_skl,nil) ),
inference(component_clause,[status(thm)],[f1227]) ).
fof(f1230,plain,
( sQ91_spl
| ~ sQ95_spl
| ~ sQ13_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f1226,f592,f595,f1227,f1210]) ).
fof(f1231,plain,
( sQ95_spl
| ~ sQ47_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1229,f874]) ).
fof(f1232,plain,
( sQ95_spl
| ~ sQ47_spl ),
inference(contradiction_clause,[status(thm)],[f1231]) ).
fof(f1236,plain,
! [X0] :
( ~ rearsegP(sK50_skl,X0)
| ~ rearsegP(sK50_skl,sK50_skl)
| X0 = sK50_skl
| ~ rearsegP(X0,sK50_skl)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f577,f423]) ).
fof(f1242,plain,
! [X0] :
( ~ rearsegP(sK49_skl,X0)
| ~ rearsegP(sK49_skl,sK49_skl)
| X0 = sK49_skl
| ~ rearsegP(X0,sK49_skl)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f577,f422]) ).
fof(f1254,plain,
! [X0] :
( ~ rearsegP(nil,X0)
| ~ rearsegP(nil,nil)
| X0 = nil
| ~ rearsegP(X0,nil)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f577,f223]) ).
fof(f1266,definition,
! [X0] :
( sQ96_spl
<=> ( ~ rearsegP(sK50_skl,X0)
| X0 = sK50_skl
| ~ rearsegP(X0,sK50_skl)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition]) ).
fof(f1269,plain,
( ~ sQ61_spl
| sQ96_spl ),
inference(split_clause,[status(thm)],[f1236,f1266,f931]) ).
fof(f1270,definition,
! [X0] :
( sQ97_spl
<=> ( ~ rearsegP(sK49_skl,X0)
| X0 = sK49_skl
| ~ rearsegP(X0,sK49_skl)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ97_spl])],[split_symbol_definition]) ).
fof(f1273,plain,
( ~ sQ53_spl
| sQ97_spl ),
inference(split_clause,[status(thm)],[f1242,f1270,f888]) ).
fof(f1281,definition,
! [X0] :
( sQ100_spl
<=> ( ~ rearsegP(nil,X0)
| X0 = nil
| ~ rearsegP(X0,nil)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ100_spl])],[split_symbol_definition]) ).
fof(f1284,plain,
( ~ sQ16_spl
| sQ100_spl ),
inference(split_clause,[status(thm)],[f1254,f1281,f612]) ).
fof(f1287,plain,
( sQ16_spl
| ~ sQ66_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f614,f962]) ).
fof(f1288,plain,
( sQ16_spl
| ~ sQ66_spl ),
inference(contradiction_clause,[status(thm)],[f1287]) ).
fof(f1289,plain,
! [X0] :
( X0 = app(sK50_skl,nil)
| ~ rearsegP(X0,app(sK50_skl,nil))
| ~ ssList(sK50_skl)
| ~ rearsegP(nil,X0)
| ~ ssList(sK50_skl)
| ~ ssList(X0)
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f982,f637]) ).
fof(f1290,plain,
! [X0] :
( X0 = app(sK49_skl,nil)
| ~ rearsegP(X0,app(sK49_skl,nil))
| ~ ssList(sK49_skl)
| ~ rearsegP(nil,X0)
| ~ ssList(sK49_skl)
| ~ ssList(X0)
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f979,f637]) ).
fof(f1291,plain,
! [X0] :
( ~ sQ51_spl
| X0 = app(nil,sK5_skl(nil,sK49_skl))
| ~ rearsegP(X0,app(nil,sK5_skl(nil,sK49_skl)))
| ~ ssList(sK49_skl)
| ~ rearsegP(sK5_skl(nil,sK49_skl),X0)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(sK5_skl(nil,sK49_skl)) ),
inference(paramodulation,[status(thm)],[f879,f637]) ).
fof(f1292,plain,
! [X0] :
( X0 = app(nil,sK50_skl)
| ~ rearsegP(X0,app(nil,sK50_skl))
| ~ ssList(sK50_skl)
| ~ rearsegP(sK50_skl,X0)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(sK50_skl) ),
inference(paramodulation,[status(thm)],[f849,f637]) ).
fof(f1293,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)],[f853,f637]) ).
fof(f1294,plain,
! [X0] :
( X0 = app(nil,sK49_skl)
| ~ rearsegP(X0,app(nil,sK49_skl))
| ~ ssList(sK49_skl)
| ~ rearsegP(sK49_skl,X0)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(sK49_skl) ),
inference(paramodulation,[status(thm)],[f846,f637]) ).
fof(f1295,definition,
! [X0] :
( sQ101_spl
<=> ( X0 = app(sK50_skl,nil)
| ~ rearsegP(X0,app(sK50_skl,nil))
| ~ rearsegP(nil,X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ101_spl])],[split_symbol_definition]) ).
fof(f1298,plain,
( ~ sQ17_spl
| sQ101_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f1289,f595,f1295,f617]) ).
fof(f1299,definition,
! [X0] :
( sQ102_spl
<=> ( X0 = app(sK49_skl,nil)
| ~ rearsegP(X0,app(sK49_skl,nil))
| ~ rearsegP(nil,X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ102_spl])],[split_symbol_definition]) ).
fof(f1302,plain,
( ~ sQ12_spl
| sQ102_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f1290,f595,f1299,f592]) ).
fof(f1303,definition,
! [X0] :
( sQ103_spl
<=> ( X0 = app(nil,sK5_skl(nil,sK49_skl))
| ~ rearsegP(X0,app(nil,sK5_skl(nil,sK49_skl)))
| ~ rearsegP(sK5_skl(nil,sK49_skl),X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ103_spl])],[split_symbol_definition]) ).
fof(f1306,plain,
( ~ sQ51_spl
| ~ sQ12_spl
| ~ sQ13_spl
| sQ103_spl
| ~ sQ91_spl ),
inference(split_clause,[status(thm)],[f1291,f1210,f1303,f595,f592,f878]) ).
fof(f1307,definition,
! [X0] :
( sQ104_spl
<=> ( X0 = app(nil,sK50_skl)
| ~ rearsegP(X0,app(nil,sK50_skl))
| ~ rearsegP(sK50_skl,X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ104_spl])],[split_symbol_definition]) ).
fof(f1310,plain,
( ~ sQ13_spl
| sQ104_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f1292,f617,f1307,f595]) ).
fof(f1311,definition,
! [X0] :
( sQ105_spl
<=> ( X0 = app(nil,nil)
| ~ rearsegP(X0,app(nil,nil))
| ~ rearsegP(nil,X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ105_spl])],[split_symbol_definition]) ).
fof(f1314,plain,
( sQ105_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f1293,f595,f1311]) ).
fof(f1315,definition,
! [X0] :
( sQ106_spl
<=> ( X0 = app(nil,sK49_skl)
| ~ rearsegP(X0,app(nil,sK49_skl))
| ~ rearsegP(sK49_skl,X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ106_spl])],[split_symbol_definition]) ).
fof(f1318,plain,
( ~ sQ13_spl
| sQ106_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f1294,f592,f1315,f595]) ).
fof(f1352,plain,
! [X0] :
( ~ sQ52_spl
| X0 = app(sK6_skl(sK49_skl,sK49_skl),sK49_skl)
| ~ rearsegP(X0,app(sK6_skl(sK49_skl,sK49_skl),sK49_skl))
| ~ ssList(sK49_skl)
| ~ rearsegP(sK49_skl,X0)
| ~ ssList(sK6_skl(sK49_skl,sK49_skl))
| ~ ssList(X0)
| ~ ssList(sK49_skl) ),
inference(paramodulation,[status(thm)],[f885,f637]) ).
fof(f1353,plain,
( ~ sQ52_spl
| ~ ssList(sK49_skl)
| frontsegP(app(sK6_skl(sK49_skl,sK49_skl),sK49_skl),sK6_skl(sK49_skl,sK49_skl))
| ~ ssList(sK6_skl(sK49_skl,sK49_skl))
| ~ ssList(sK49_skl) ),
inference(paramodulation,[status(thm)],[f885,f466]) ).
fof(f1355,plain,
! [X0] :
( ~ sQ52_spl
| ~ ssList(X0)
| ~ ssList(sK6_skl(sK49_skl,sK49_skl))
| segmentP(app(app(sK6_skl(sK49_skl,sK49_skl),sK49_skl),X0),sK49_skl)
| ~ ssList(sK49_skl)
| ~ ssList(app(sK49_skl,X0)) ),
inference(paramodulation,[status(thm)],[f885,f468]) ).
fof(f1356,plain,
( ~ sQ52_spl
| ~ ssList(sK6_skl(sK49_skl,sK49_skl))
| rearsegP(app(sK6_skl(sK49_skl,sK49_skl),sK49_skl),sK49_skl)
| ~ ssList(sK49_skl)
| ~ ssList(sK49_skl) ),
inference(paramodulation,[status(thm)],[f885,f467]) ).
fof(f1357,definition,
! [X0] :
( sQ109_spl
<=> ( X0 = app(sK6_skl(sK49_skl,sK49_skl),sK49_skl)
| ~ rearsegP(X0,app(sK6_skl(sK49_skl,sK49_skl),sK49_skl))
| ~ rearsegP(sK49_skl,X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ109_spl])],[split_symbol_definition]) ).
fof(f1360,definition,
( sQ110_spl
<=> ssList(sK6_skl(sK49_skl,sK49_skl)) ),
introduced(definition,[new_symbols(definition,[sQ110_spl])],[split_symbol_definition]) ).
fof(f1362,plain,
( sQ110_spl
| ~ ssList(sK6_skl(sK49_skl,sK49_skl)) ),
inference(component_clause,[status(thm)],[f1360]) ).
fof(f1363,plain,
( ~ sQ52_spl
| ~ sQ110_spl
| sQ109_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f1352,f592,f1357,f1360,f884]) ).
fof(f1364,definition,
( sQ111_spl
<=> frontsegP(app(sK6_skl(sK49_skl,sK49_skl),sK49_skl),sK6_skl(sK49_skl,sK49_skl)) ),
introduced(definition,[new_symbols(definition,[sQ111_spl])],[split_symbol_definition]) ).
fof(f1365,plain,
( ~ sQ111_spl
| frontsegP(app(sK6_skl(sK49_skl,sK49_skl),sK49_skl),sK6_skl(sK49_skl,sK49_skl)) ),
inference(component_clause,[status(thm)],[f1364]) ).
fof(f1367,plain,
( ~ sQ52_spl
| sQ111_spl
| ~ sQ110_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f1353,f592,f1360,f1364,f884]) ).
fof(f1369,definition,
! [X0] :
( sQ112_spl
<=> ( ~ ssList(X0)
| segmentP(app(app(sK6_skl(sK49_skl,sK49_skl),sK49_skl),X0),sK49_skl)
| ~ ssList(app(sK49_skl,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ112_spl])],[split_symbol_definition]) ).
fof(f1372,plain,
( ~ sQ52_spl
| ~ sQ110_spl
| ~ sQ12_spl
| sQ112_spl ),
inference(split_clause,[status(thm)],[f1355,f1369,f592,f1360,f884]) ).
fof(f1373,definition,
( sQ113_spl
<=> rearsegP(app(sK6_skl(sK49_skl,sK49_skl),sK49_skl),sK49_skl) ),
introduced(definition,[new_symbols(definition,[sQ113_spl])],[split_symbol_definition]) ).
fof(f1376,plain,
( ~ sQ52_spl
| ~ sQ110_spl
| sQ113_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f1356,f592,f1373,f1360,f884]) ).
fof(f1377,plain,
( sQ110_spl
| ~ rearsegP(sK49_skl,sK49_skl)
| ~ ssList(sK49_skl)
| ~ ssList(sK49_skl) ),
inference(resolution,[status(thm)],[f1362,f128]) ).
fof(f1378,plain,
( sQ110_spl
| ~ sQ53_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f1377,f592,f888,f1360]) ).
fof(f1381,plain,
( ~ sQ111_spl
| ~ sQ52_spl
| frontsegP(sK49_skl,sK6_skl(sK49_skl,sK49_skl)) ),
inference(forward_demodulation,[status(thm)],[f885,f1365]) ).
fof(f1399,plain,
( ~ sQ111_spl
| ~ sQ52_spl
| app(sK6_skl(sK49_skl,sK49_skl),sK5_skl(sK6_skl(sK49_skl,sK49_skl),sK49_skl)) = sK49_skl
| ~ ssList(sK6_skl(sK49_skl,sK49_skl))
| ~ ssList(sK49_skl) ),
inference(resolution,[status(thm)],[f1381,f123]) ).
fof(f1400,definition,
( sQ116_spl
<=> app(sK6_skl(sK49_skl,sK49_skl),sK5_skl(sK6_skl(sK49_skl,sK49_skl),sK49_skl)) = sK49_skl ),
introduced(definition,[new_symbols(definition,[sQ116_spl])],[split_symbol_definition]) ).
fof(f1403,plain,
( ~ sQ111_spl
| ~ sQ52_spl
| sQ116_spl
| ~ sQ110_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f1399,f592,f1360,f1400,f884,f1364]) ).
fof(f1419,plain,
! [X0] :
( ~ sQ59_spl
| X0 = app(nil,sK5_skl(nil,sK50_skl))
| ~ rearsegP(X0,app(nil,sK5_skl(nil,sK50_skl)))
| ~ ssList(sK50_skl)
| ~ rearsegP(sK5_skl(nil,sK50_skl),X0)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(sK5_skl(nil,sK50_skl)) ),
inference(paramodulation,[status(thm)],[f922,f637]) ).
fof(f1420,plain,
( ~ sQ59_spl
| ~ ssList(sK5_skl(nil,sK50_skl))
| frontsegP(app(nil,sK5_skl(nil,sK50_skl)),nil)
| ~ ssList(nil)
| ~ ssList(sK50_skl) ),
inference(paramodulation,[status(thm)],[f922,f466]) ).
fof(f1421,plain,
! [X0] :
( ~ sQ59_spl
| rearsegP(sK50_skl,X0)
| ~ rearsegP(sK5_skl(nil,sK50_skl),X0)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(sK5_skl(nil,sK50_skl)) ),
inference(paramodulation,[status(thm)],[f922,f307]) ).
fof(f1422,plain,
! [X0] :
( ~ sQ59_spl
| ~ ssList(X0)
| ~ ssList(nil)
| segmentP(app(app(nil,sK5_skl(nil,sK50_skl)),X0),sK5_skl(nil,sK50_skl))
| ~ ssList(sK5_skl(nil,sK50_skl))
| ~ ssList(app(sK50_skl,X0)) ),
inference(paramodulation,[status(thm)],[f922,f468]) ).
fof(f1423,plain,
( ~ sQ59_spl
| ~ ssList(nil)
| rearsegP(app(nil,sK5_skl(nil,sK50_skl)),sK5_skl(nil,sK50_skl))
| ~ ssList(sK5_skl(nil,sK50_skl))
| ~ ssList(sK50_skl) ),
inference(paramodulation,[status(thm)],[f922,f467]) ).
fof(f1424,definition,
( sQ118_spl
<=> ssList(sK5_skl(nil,sK50_skl)) ),
introduced(definition,[new_symbols(definition,[sQ118_spl])],[split_symbol_definition]) ).
fof(f1426,plain,
( sQ118_spl
| ~ ssList(sK5_skl(nil,sK50_skl)) ),
inference(component_clause,[status(thm)],[f1424]) ).
fof(f1427,definition,
! [X0] :
( sQ119_spl
<=> ( X0 = app(nil,sK5_skl(nil,sK50_skl))
| ~ rearsegP(X0,app(nil,sK5_skl(nil,sK50_skl)))
| ~ rearsegP(sK5_skl(nil,sK50_skl),X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ119_spl])],[split_symbol_definition]) ).
fof(f1430,plain,
( ~ sQ59_spl
| ~ sQ17_spl
| ~ sQ13_spl
| sQ119_spl
| ~ sQ118_spl ),
inference(split_clause,[status(thm)],[f1419,f1424,f1427,f595,f617,f921]) ).
fof(f1431,definition,
( sQ120_spl
<=> frontsegP(app(nil,sK5_skl(nil,sK50_skl)),nil) ),
introduced(definition,[new_symbols(definition,[sQ120_spl])],[split_symbol_definition]) ).
fof(f1434,plain,
( ~ sQ59_spl
| ~ sQ118_spl
| sQ120_spl
| ~ sQ13_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f1420,f617,f595,f1431,f1424,f921]) ).
fof(f1435,definition,
! [X0] :
( sQ121_spl
<=> ( rearsegP(sK50_skl,X0)
| ~ rearsegP(sK5_skl(nil,sK50_skl),X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ121_spl])],[split_symbol_definition]) ).
fof(f1438,plain,
( ~ sQ59_spl
| ~ sQ13_spl
| sQ121_spl
| ~ sQ118_spl ),
inference(split_clause,[status(thm)],[f1421,f1424,f1435,f595,f921]) ).
fof(f1439,definition,
! [X0] :
( sQ122_spl
<=> ( ~ ssList(X0)
| segmentP(app(app(nil,sK5_skl(nil,sK50_skl)),X0),sK5_skl(nil,sK50_skl))
| ~ ssList(app(sK50_skl,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ122_spl])],[split_symbol_definition]) ).
fof(f1442,plain,
( ~ sQ59_spl
| ~ sQ13_spl
| ~ sQ118_spl
| sQ122_spl ),
inference(split_clause,[status(thm)],[f1422,f1439,f1424,f595,f921]) ).
fof(f1443,definition,
( sQ123_spl
<=> rearsegP(app(nil,sK5_skl(nil,sK50_skl)),sK5_skl(nil,sK50_skl)) ),
introduced(definition,[new_symbols(definition,[sQ123_spl])],[split_symbol_definition]) ).
fof(f1446,plain,
( ~ sQ59_spl
| ~ sQ13_spl
| sQ123_spl
| ~ sQ118_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f1423,f617,f1424,f1443,f595,f921]) ).
fof(f1447,plain,
( sQ118_spl
| ~ frontsegP(sK50_skl,nil)
| ~ ssList(nil)
| ~ ssList(sK50_skl) ),
inference(resolution,[status(thm)],[f1426,f122]) ).
fof(f1448,definition,
( sQ124_spl
<=> frontsegP(sK50_skl,nil) ),
introduced(definition,[new_symbols(definition,[sQ124_spl])],[split_symbol_definition]) ).
fof(f1450,plain,
( sQ124_spl
| ~ frontsegP(sK50_skl,nil) ),
inference(component_clause,[status(thm)],[f1448]) ).
fof(f1451,plain,
( sQ118_spl
| ~ sQ124_spl
| ~ sQ13_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f1447,f617,f595,f1448,f1424]) ).
fof(f1452,plain,
( sQ124_spl
| ~ sQ55_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1450,f917]) ).
fof(f1453,plain,
( sQ124_spl
| ~ sQ55_spl ),
inference(contradiction_clause,[status(thm)],[f1452]) ).
fof(f1480,plain,
! [X0] :
( ~ sQ60_spl
| X0 = app(sK6_skl(sK50_skl,sK50_skl),sK50_skl)
| ~ rearsegP(X0,app(sK6_skl(sK50_skl,sK50_skl),sK50_skl))
| ~ ssList(sK50_skl)
| ~ rearsegP(sK50_skl,X0)
| ~ ssList(sK6_skl(sK50_skl,sK50_skl))
| ~ ssList(X0)
| ~ ssList(sK50_skl) ),
inference(paramodulation,[status(thm)],[f928,f637]) ).
fof(f1481,plain,
( ~ sQ60_spl
| ~ ssList(sK50_skl)
| frontsegP(app(sK6_skl(sK50_skl,sK50_skl),sK50_skl),sK6_skl(sK50_skl,sK50_skl))
| ~ ssList(sK6_skl(sK50_skl,sK50_skl))
| ~ ssList(sK50_skl) ),
inference(paramodulation,[status(thm)],[f928,f466]) ).
fof(f1483,plain,
! [X0] :
( ~ sQ60_spl
| ~ ssList(X0)
| ~ ssList(sK6_skl(sK50_skl,sK50_skl))
| segmentP(app(app(sK6_skl(sK50_skl,sK50_skl),sK50_skl),X0),sK50_skl)
| ~ ssList(sK50_skl)
| ~ ssList(app(sK50_skl,X0)) ),
inference(paramodulation,[status(thm)],[f928,f468]) ).
fof(f1484,plain,
( ~ sQ60_spl
| ~ ssList(sK6_skl(sK50_skl,sK50_skl))
| rearsegP(app(sK6_skl(sK50_skl,sK50_skl),sK50_skl),sK50_skl)
| ~ ssList(sK50_skl)
| ~ ssList(sK50_skl) ),
inference(paramodulation,[status(thm)],[f928,f467]) ).
fof(f1485,definition,
! [X0] :
( sQ127_spl
<=> ( X0 = app(sK6_skl(sK50_skl,sK50_skl),sK50_skl)
| ~ rearsegP(X0,app(sK6_skl(sK50_skl,sK50_skl),sK50_skl))
| ~ rearsegP(sK50_skl,X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ127_spl])],[split_symbol_definition]) ).
fof(f1488,definition,
( sQ128_spl
<=> ssList(sK6_skl(sK50_skl,sK50_skl)) ),
introduced(definition,[new_symbols(definition,[sQ128_spl])],[split_symbol_definition]) ).
fof(f1490,plain,
( sQ128_spl
| ~ ssList(sK6_skl(sK50_skl,sK50_skl)) ),
inference(component_clause,[status(thm)],[f1488]) ).
fof(f1491,plain,
( ~ sQ60_spl
| ~ sQ128_spl
| sQ127_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f1480,f617,f1485,f1488,f927]) ).
fof(f1492,definition,
( sQ129_spl
<=> frontsegP(app(sK6_skl(sK50_skl,sK50_skl),sK50_skl),sK6_skl(sK50_skl,sK50_skl)) ),
introduced(definition,[new_symbols(definition,[sQ129_spl])],[split_symbol_definition]) ).
fof(f1493,plain,
( ~ sQ129_spl
| frontsegP(app(sK6_skl(sK50_skl,sK50_skl),sK50_skl),sK6_skl(sK50_skl,sK50_skl)) ),
inference(component_clause,[status(thm)],[f1492]) ).
fof(f1495,plain,
( ~ sQ60_spl
| sQ129_spl
| ~ sQ128_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f1481,f617,f1488,f1492,f927]) ).
fof(f1497,definition,
! [X0] :
( sQ130_spl
<=> ( ~ ssList(X0)
| segmentP(app(app(sK6_skl(sK50_skl,sK50_skl),sK50_skl),X0),sK50_skl)
| ~ ssList(app(sK50_skl,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ130_spl])],[split_symbol_definition]) ).
fof(f1500,plain,
( ~ sQ60_spl
| ~ sQ128_spl
| ~ sQ17_spl
| sQ130_spl ),
inference(split_clause,[status(thm)],[f1483,f1497,f617,f1488,f927]) ).
fof(f1501,definition,
( sQ131_spl
<=> rearsegP(app(sK6_skl(sK50_skl,sK50_skl),sK50_skl),sK50_skl) ),
introduced(definition,[new_symbols(definition,[sQ131_spl])],[split_symbol_definition]) ).
fof(f1504,plain,
( ~ sQ60_spl
| ~ sQ128_spl
| sQ131_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f1484,f617,f1501,f1488,f927]) ).
fof(f1505,plain,
( sQ128_spl
| ~ rearsegP(sK50_skl,sK50_skl)
| ~ ssList(sK50_skl)
| ~ ssList(sK50_skl) ),
inference(resolution,[status(thm)],[f1490,f128]) ).
fof(f1506,plain,
( sQ128_spl
| ~ sQ61_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f1505,f617,f931,f1488]) ).
fof(f1509,plain,
( ~ sQ129_spl
| ~ sQ60_spl
| frontsegP(sK50_skl,sK6_skl(sK50_skl,sK50_skl)) ),
inference(forward_demodulation,[status(thm)],[f928,f1493]) ).
fof(f1527,plain,
! [X0] :
( ~ sQ60_spl
| ~ rearsegP(sK50_skl,X0)
| ~ ssList(sK6_skl(sK50_skl,sK50_skl))
| ~ ssList(sK50_skl)
| app(sK6_skl(X0,app(sK6_skl(sK50_skl,sK50_skl),sK50_skl)),X0) = app(sK6_skl(sK50_skl,sK50_skl),sK50_skl)
| ~ ssList(X0)
| ~ ssList(sK50_skl) ),
inference(paramodulation,[status(thm)],[f928,f675]) ).
fof(f1529,plain,
! [X0] :
( ~ sQ52_spl
| ~ rearsegP(sK49_skl,X0)
| ~ ssList(sK6_skl(sK49_skl,sK49_skl))
| ~ ssList(sK49_skl)
| app(sK6_skl(X0,app(sK6_skl(sK49_skl,sK49_skl),sK49_skl)),X0) = app(sK6_skl(sK49_skl,sK49_skl),sK49_skl)
| ~ ssList(X0)
| ~ ssList(sK49_skl) ),
inference(paramodulation,[status(thm)],[f885,f675]) ).
fof(f1530,plain,
! [X0] :
( ~ rearsegP(nil,X0)
| ~ ssList(sK50_skl)
| ~ ssList(nil)
| app(sK6_skl(X0,app(sK50_skl,nil)),X0) = app(sK50_skl,nil)
| ~ ssList(X0)
| ~ ssList(sK50_skl) ),
inference(paramodulation,[status(thm)],[f982,f675]) ).
fof(f1531,plain,
! [X0] :
( ~ rearsegP(nil,X0)
| ~ ssList(sK49_skl)
| ~ ssList(nil)
| app(sK6_skl(X0,app(sK49_skl,nil)),X0) = app(sK49_skl,nil)
| ~ ssList(X0)
| ~ ssList(sK49_skl) ),
inference(paramodulation,[status(thm)],[f979,f675]) ).
fof(f1532,plain,
! [X0] :
( ~ rearsegP(sK50_skl,X0)
| ~ ssList(nil)
| ~ ssList(sK50_skl)
| app(sK6_skl(X0,app(nil,sK50_skl)),X0) = app(nil,sK50_skl)
| ~ ssList(X0)
| ~ ssList(sK50_skl) ),
inference(paramodulation,[status(thm)],[f849,f675]) ).
fof(f1533,plain,
! [X0] :
( ~ rearsegP(nil,X0)
| ~ ssList(nil)
| ~ ssList(nil)
| app(sK6_skl(X0,app(nil,nil)),X0) = app(nil,nil)
| ~ ssList(X0)
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f853,f675]) ).
fof(f1534,plain,
! [X0] :
( ~ rearsegP(sK49_skl,X0)
| ~ ssList(nil)
| ~ ssList(sK49_skl)
| app(sK6_skl(X0,app(nil,sK49_skl)),X0) = app(nil,sK49_skl)
| ~ ssList(X0)
| ~ ssList(sK49_skl) ),
inference(paramodulation,[status(thm)],[f846,f675]) ).
fof(f1535,definition,
! [X0] :
( sQ134_spl
<=> ( ~ rearsegP(sK50_skl,X0)
| app(sK6_skl(X0,app(sK6_skl(sK50_skl,sK50_skl),sK50_skl)),X0) = app(sK6_skl(sK50_skl,sK50_skl),sK50_skl)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ134_spl])],[split_symbol_definition]) ).
fof(f1538,plain,
( ~ sQ60_spl
| ~ sQ128_spl
| sQ134_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f1527,f617,f1535,f1488,f927]) ).
fof(f1543,definition,
! [X0] :
( sQ136_spl
<=> ( ~ rearsegP(sK49_skl,X0)
| app(sK6_skl(X0,app(sK6_skl(sK49_skl,sK49_skl),sK49_skl)),X0) = app(sK6_skl(sK49_skl,sK49_skl),sK49_skl)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ136_spl])],[split_symbol_definition]) ).
fof(f1546,plain,
( ~ sQ52_spl
| ~ sQ110_spl
| sQ136_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f1529,f592,f1543,f1360,f884]) ).
fof(f1547,definition,
! [X0] :
( sQ137_spl
<=> ( ~ rearsegP(nil,X0)
| app(sK6_skl(X0,app(sK50_skl,nil)),X0) = app(sK50_skl,nil)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ137_spl])],[split_symbol_definition]) ).
fof(f1550,plain,
( ~ sQ13_spl
| sQ137_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f1530,f617,f1547,f595]) ).
fof(f1551,definition,
! [X0] :
( sQ138_spl
<=> ( ~ rearsegP(nil,X0)
| app(sK6_skl(X0,app(sK49_skl,nil)),X0) = app(sK49_skl,nil)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ138_spl])],[split_symbol_definition]) ).
fof(f1554,plain,
( ~ sQ13_spl
| sQ138_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f1531,f592,f1551,f595]) ).
fof(f1555,definition,
! [X0] :
( sQ139_spl
<=> ( ~ rearsegP(sK50_skl,X0)
| app(sK6_skl(X0,app(nil,sK50_skl)),X0) = app(nil,sK50_skl)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ139_spl])],[split_symbol_definition]) ).
fof(f1558,plain,
( ~ sQ13_spl
| sQ139_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f1532,f617,f1555,f595]) ).
fof(f1559,definition,
! [X0] :
( sQ140_spl
<=> ( ~ rearsegP(nil,X0)
| app(sK6_skl(X0,app(nil,nil)),X0) = app(nil,nil)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ140_spl])],[split_symbol_definition]) ).
fof(f1562,plain,
( sQ140_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f1533,f595,f1559]) ).
fof(f1563,definition,
! [X0] :
( sQ141_spl
<=> ( ~ rearsegP(sK49_skl,X0)
| app(sK6_skl(X0,app(nil,sK49_skl)),X0) = app(nil,sK49_skl)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ141_spl])],[split_symbol_definition]) ).
fof(f1566,plain,
( ~ sQ13_spl
| sQ141_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f1534,f592,f1563,f595]) ).
fof(f1584,plain,
! [X0] :
( ~ sQ58_spl
| ~ rearsegP(X0,sK50_skl)
| ~ ssList(sK50_skl)
| app(sK6_skl(sK50_skl,X0),sK50_skl) = X0
| ~ ssList(sK50_skl)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f680,f919]) ).
fof(f1585,plain,
! [X0] :
( ~ sQ77_spl
| ~ rearsegP(X0,sK50_skl)
| ~ ssList(sK50_skl)
| app(sK6_skl(nil,X0),nil) = X0
| ~ ssList(nil)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f680,f1037]) ).
fof(f1586,plain,
! [X0] :
( ~ sQ66_spl
| ~ rearsegP(X0,nil)
| ~ ssList(nil)
| app(sK6_skl(nil,X0),nil) = X0
| ~ ssList(nil)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f680,f962]) ).
fof(f1587,plain,
! [X0] :
( ~ sQ50_spl
| ~ rearsegP(X0,sK49_skl)
| ~ ssList(sK49_skl)
| app(sK6_skl(sK49_skl,X0),sK49_skl) = X0
| ~ ssList(sK49_skl)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f680,f876]) ).
fof(f1588,plain,
! [X0] :
( ~ sQ14_spl
| ~ rearsegP(X0,sK49_skl)
| ~ ssList(sK49_skl)
| app(sK6_skl(nil,X0),nil) = X0
| ~ ssList(nil)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f680,f599]) ).
fof(f1590,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)],[f680,f309]) ).
fof(f1597,definition,
! [X0] :
( sQ143_spl
<=> ( ~ rearsegP(X0,sK50_skl)
| app(sK6_skl(sK50_skl,X0),sK50_skl) = X0
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ143_spl])],[split_symbol_definition]) ).
fof(f1600,plain,
( ~ sQ58_spl
| ~ sQ17_spl
| sQ143_spl ),
inference(split_clause,[status(thm)],[f1584,f1597,f617,f913]) ).
fof(f1601,definition,
! [X0] :
( sQ144_spl
<=> ( ~ rearsegP(X0,sK50_skl)
| app(sK6_skl(nil,X0),nil) = X0
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ144_spl])],[split_symbol_definition]) ).
fof(f1604,plain,
( ~ sQ77_spl
| ~ sQ17_spl
| ~ sQ13_spl
| sQ144_spl ),
inference(split_clause,[status(thm)],[f1585,f1601,f595,f617,f1031]) ).
fof(f1605,definition,
! [X0] :
( sQ145_spl
<=> ( ~ rearsegP(X0,nil)
| app(sK6_skl(nil,X0),nil) = X0
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ145_spl])],[split_symbol_definition]) ).
fof(f1608,plain,
( ~ sQ66_spl
| ~ sQ13_spl
| sQ145_spl ),
inference(split_clause,[status(thm)],[f1586,f1605,f595,f956]) ).
fof(f1609,definition,
! [X0] :
( sQ146_spl
<=> ( ~ rearsegP(X0,sK49_skl)
| app(sK6_skl(sK49_skl,X0),sK49_skl) = X0
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ146_spl])],[split_symbol_definition]) ).
fof(f1612,plain,
( ~ sQ50_spl
| ~ sQ12_spl
| sQ146_spl ),
inference(split_clause,[status(thm)],[f1587,f1609,f592,f870]) ).
fof(f1613,definition,
! [X0] :
( sQ147_spl
<=> ( ~ rearsegP(X0,sK49_skl)
| app(sK6_skl(nil,X0),nil) = X0
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ147_spl])],[split_symbol_definition]) ).
fof(f1616,plain,
( ~ sQ14_spl
| ~ sQ12_spl
| ~ sQ13_spl
| sQ147_spl ),
inference(split_clause,[status(thm)],[f1588,f1613,f595,f592,f598]) ).
fof(f1618,definition,
! [X0,X1] :
( sQ148_spl
<=> ( ~ ssList(X1)
| ~ rearsegP(X0,X1)
| ~ ssList(X1)
| app(sK6_skl(nil,X0),nil) = X0
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ148_spl])],[split_symbol_definition]) ).
fof(f1621,plain,
( ~ sQ13_spl
| sQ148_spl ),
inference(split_clause,[status(thm)],[f1590,f1618,f595]) ).
fof(f1626,plain,
( ~ sQ129_spl
| ~ sQ60_spl
| app(sK6_skl(sK50_skl,sK50_skl),sK5_skl(sK6_skl(sK50_skl,sK50_skl),sK50_skl)) = sK50_skl
| ~ ssList(sK6_skl(sK50_skl,sK50_skl))
| ~ ssList(sK50_skl) ),
inference(resolution,[status(thm)],[f1509,f123]) ).
fof(f1627,definition,
( sQ149_spl
<=> app(sK6_skl(sK50_skl,sK50_skl),sK5_skl(sK6_skl(sK50_skl,sK50_skl),sK50_skl)) = sK50_skl ),
introduced(definition,[new_symbols(definition,[sQ149_spl])],[split_symbol_definition]) ).
fof(f1630,plain,
( ~ sQ129_spl
| ~ sQ60_spl
| sQ149_spl
| ~ sQ128_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f1626,f617,f1488,f1627,f927,f1492]) ).
fof(f1631,plain,
! [X0] :
( ~ sQ73_spl
| ~ rearsegP(sK5_skl(sK49_skl,sK49_skl),X0)
| ~ ssList(sK49_skl)
| ~ ssList(sK5_skl(sK49_skl,sK49_skl))
| app(sK6_skl(X0,app(sK49_skl,sK5_skl(sK49_skl,sK49_skl))),X0) = app(sK49_skl,sK5_skl(sK49_skl,sK49_skl))
| ~ ssList(X0)
| ~ ssList(sK49_skl) ),
inference(paramodulation,[status(thm)],[f1012,f675]) ).
fof(f1632,plain,
! [X0] :
( ~ sQ73_spl
| X0 = app(sK49_skl,sK5_skl(sK49_skl,sK49_skl))
| ~ rearsegP(X0,app(sK49_skl,sK5_skl(sK49_skl,sK49_skl)))
| ~ ssList(sK49_skl)
| ~ rearsegP(sK5_skl(sK49_skl,sK49_skl),X0)
| ~ ssList(sK49_skl)
| ~ ssList(X0)
| ~ ssList(sK5_skl(sK49_skl,sK49_skl)) ),
inference(paramodulation,[status(thm)],[f1012,f637]) ).
fof(f1633,plain,
( ~ sQ73_spl
| ~ ssList(sK5_skl(sK49_skl,sK49_skl))
| frontsegP(app(sK49_skl,sK5_skl(sK49_skl,sK49_skl)),sK49_skl)
| ~ ssList(sK49_skl)
| ~ ssList(sK49_skl) ),
inference(paramodulation,[status(thm)],[f1012,f466]) ).
fof(f1634,plain,
! [X0] :
( ~ sQ73_spl
| rearsegP(sK49_skl,X0)
| ~ rearsegP(sK5_skl(sK49_skl,sK49_skl),X0)
| ~ ssList(sK49_skl)
| ~ ssList(X0)
| ~ ssList(sK5_skl(sK49_skl,sK49_skl)) ),
inference(paramodulation,[status(thm)],[f1012,f307]) ).
fof(f1635,plain,
! [X0] :
( ~ sQ73_spl
| ~ ssList(X0)
| ~ ssList(sK49_skl)
| segmentP(app(app(sK49_skl,sK5_skl(sK49_skl,sK49_skl)),X0),sK5_skl(sK49_skl,sK49_skl))
| ~ ssList(sK5_skl(sK49_skl,sK49_skl))
| ~ ssList(app(sK49_skl,X0)) ),
inference(paramodulation,[status(thm)],[f1012,f468]) ).
fof(f1636,plain,
( ~ sQ73_spl
| ~ ssList(sK49_skl)
| rearsegP(app(sK49_skl,sK5_skl(sK49_skl,sK49_skl)),sK5_skl(sK49_skl,sK49_skl))
| ~ ssList(sK5_skl(sK49_skl,sK49_skl))
| ~ ssList(sK49_skl) ),
inference(paramodulation,[status(thm)],[f1012,f467]) ).
fof(f1637,definition,
! [X0] :
( sQ150_spl
<=> ( ~ rearsegP(sK5_skl(sK49_skl,sK49_skl),X0)
| app(sK6_skl(X0,app(sK49_skl,sK5_skl(sK49_skl,sK49_skl))),X0) = app(sK49_skl,sK5_skl(sK49_skl,sK49_skl))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ150_spl])],[split_symbol_definition]) ).
fof(f1640,definition,
( sQ151_spl
<=> ssList(sK5_skl(sK49_skl,sK49_skl)) ),
introduced(definition,[new_symbols(definition,[sQ151_spl])],[split_symbol_definition]) ).
fof(f1642,plain,
( sQ151_spl
| ~ ssList(sK5_skl(sK49_skl,sK49_skl)) ),
inference(component_clause,[status(thm)],[f1640]) ).
fof(f1643,plain,
( ~ sQ73_spl
| ~ sQ151_spl
| sQ150_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f1631,f592,f1637,f1640,f1011]) ).
fof(f1644,definition,
! [X0] :
( sQ152_spl
<=> ( X0 = app(sK49_skl,sK5_skl(sK49_skl,sK49_skl))
| ~ rearsegP(X0,app(sK49_skl,sK5_skl(sK49_skl,sK49_skl)))
| ~ rearsegP(sK5_skl(sK49_skl,sK49_skl),X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ152_spl])],[split_symbol_definition]) ).
fof(f1647,plain,
( ~ sQ73_spl
| ~ sQ12_spl
| sQ152_spl
| ~ sQ151_spl ),
inference(split_clause,[status(thm)],[f1632,f1640,f1644,f592,f1011]) ).
fof(f1648,definition,
( sQ153_spl
<=> frontsegP(app(sK49_skl,sK5_skl(sK49_skl,sK49_skl)),sK49_skl) ),
introduced(definition,[new_symbols(definition,[sQ153_spl])],[split_symbol_definition]) ).
fof(f1651,plain,
( ~ sQ73_spl
| ~ sQ151_spl
| sQ153_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f1633,f592,f1648,f1640,f1011]) ).
fof(f1652,definition,
! [X0] :
( sQ154_spl
<=> ( rearsegP(sK49_skl,X0)
| ~ rearsegP(sK5_skl(sK49_skl,sK49_skl),X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ154_spl])],[split_symbol_definition]) ).
fof(f1655,plain,
( ~ sQ73_spl
| ~ sQ12_spl
| sQ154_spl
| ~ sQ151_spl ),
inference(split_clause,[status(thm)],[f1634,f1640,f1652,f592,f1011]) ).
fof(f1656,definition,
! [X0] :
( sQ155_spl
<=> ( ~ ssList(X0)
| segmentP(app(app(sK49_skl,sK5_skl(sK49_skl,sK49_skl)),X0),sK5_skl(sK49_skl,sK49_skl))
| ~ ssList(app(sK49_skl,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ155_spl])],[split_symbol_definition]) ).
fof(f1659,plain,
( ~ sQ73_spl
| ~ sQ12_spl
| ~ sQ151_spl
| sQ155_spl ),
inference(split_clause,[status(thm)],[f1635,f1656,f1640,f592,f1011]) ).
fof(f1660,definition,
( sQ156_spl
<=> rearsegP(app(sK49_skl,sK5_skl(sK49_skl,sK49_skl)),sK5_skl(sK49_skl,sK49_skl)) ),
introduced(definition,[new_symbols(definition,[sQ156_spl])],[split_symbol_definition]) ).
fof(f1661,plain,
( ~ sQ156_spl
| rearsegP(app(sK49_skl,sK5_skl(sK49_skl,sK49_skl)),sK5_skl(sK49_skl,sK49_skl)) ),
inference(component_clause,[status(thm)],[f1660]) ).
fof(f1663,plain,
( ~ sQ73_spl
| sQ156_spl
| ~ sQ151_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f1636,f592,f1640,f1660,f1011]) ).
fof(f1664,plain,
( sQ151_spl
| ~ frontsegP(sK49_skl,sK49_skl)
| ~ ssList(sK49_skl)
| ~ ssList(sK49_skl) ),
inference(resolution,[status(thm)],[f1642,f122]) ).
fof(f1665,definition,
( sQ157_spl
<=> frontsegP(sK49_skl,sK49_skl) ),
introduced(definition,[new_symbols(definition,[sQ157_spl])],[split_symbol_definition]) ).
fof(f1667,plain,
( sQ157_spl
| ~ frontsegP(sK49_skl,sK49_skl) ),
inference(component_clause,[status(thm)],[f1665]) ).
fof(f1668,plain,
( sQ151_spl
| ~ sQ157_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f1664,f592,f1665,f1640]) ).
fof(f1669,plain,
( sQ157_spl
| ~ sQ69_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1667,f1007]) ).
fof(f1670,plain,
( sQ157_spl
| ~ sQ69_spl ),
inference(contradiction_clause,[status(thm)],[f1669]) ).
fof(f1677,plain,
( ~ sQ156_spl
| ~ sQ73_spl
| rearsegP(sK49_skl,sK5_skl(sK49_skl,sK49_skl)) ),
inference(forward_demodulation,[status(thm)],[f1012,f1661]) ).
fof(f1693,plain,
! [X0] :
( ~ sQ156_spl
| ~ sQ73_spl
| ~ rearsegP(X0,sK49_skl)
| ~ ssList(sK49_skl)
| app(sK6_skl(sK5_skl(sK49_skl,sK49_skl),X0),sK5_skl(sK49_skl,sK49_skl)) = X0
| ~ ssList(sK5_skl(sK49_skl,sK49_skl))
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f1677,f680]) ).
fof(f1694,plain,
( ~ sQ156_spl
| ~ sQ73_spl
| app(sK6_skl(sK5_skl(sK49_skl,sK49_skl),sK49_skl),sK5_skl(sK49_skl,sK49_skl)) = sK49_skl
| ~ ssList(sK5_skl(sK49_skl,sK49_skl))
| ~ ssList(sK49_skl) ),
inference(resolution,[status(thm)],[f1677,f129]) ).
fof(f1696,definition,
! [X0] :
( sQ160_spl
<=> ( ~ rearsegP(X0,sK49_skl)
| app(sK6_skl(sK5_skl(sK49_skl,sK49_skl),X0),sK5_skl(sK49_skl,sK49_skl)) = X0
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ160_spl])],[split_symbol_definition]) ).
fof(f1699,plain,
( ~ sQ156_spl
| ~ sQ73_spl
| ~ sQ12_spl
| ~ sQ151_spl
| sQ160_spl ),
inference(split_clause,[status(thm)],[f1693,f1696,f1640,f592,f1011,f1660]) ).
fof(f1700,definition,
( sQ161_spl
<=> app(sK6_skl(sK5_skl(sK49_skl,sK49_skl),sK49_skl),sK5_skl(sK49_skl,sK49_skl)) = sK49_skl ),
introduced(definition,[new_symbols(definition,[sQ161_spl])],[split_symbol_definition]) ).
fof(f1703,plain,
( ~ sQ156_spl
| ~ sQ73_spl
| sQ161_spl
| ~ sQ151_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f1694,f592,f1640,f1700,f1011,f1660]) ).
fof(f1773,plain,
! [X0] :
( ~ sQ67_spl
| ~ rearsegP(sK5_skl(nil,nil),X0)
| ~ ssList(nil)
| ~ ssList(sK5_skl(nil,nil))
| app(sK6_skl(X0,app(nil,sK5_skl(nil,nil))),X0) = app(nil,sK5_skl(nil,nil))
| ~ ssList(X0)
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f965,f675]) ).
fof(f1774,plain,
! [X0] :
( ~ sQ67_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)],[f965,f637]) ).
fof(f1775,plain,
( ~ sQ67_spl
| ~ ssList(sK5_skl(nil,nil))
| frontsegP(app(nil,sK5_skl(nil,nil)),nil)
| ~ ssList(nil)
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f965,f466]) ).
fof(f1776,plain,
! [X0] :
( ~ sQ67_spl
| rearsegP(nil,X0)
| ~ rearsegP(sK5_skl(nil,nil),X0)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(sK5_skl(nil,nil)) ),
inference(paramodulation,[status(thm)],[f965,f307]) ).
fof(f1777,plain,
! [X0] :
( ~ sQ67_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)],[f965,f468]) ).
fof(f1778,plain,
( ~ sQ67_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)],[f965,f467]) ).
fof(f1779,definition,
! [X0] :
( sQ173_spl
<=> ( ~ rearsegP(sK5_skl(nil,nil),X0)
| app(sK6_skl(X0,app(nil,sK5_skl(nil,nil))),X0) = app(nil,sK5_skl(nil,nil))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ173_spl])],[split_symbol_definition]) ).
fof(f1782,definition,
( sQ174_spl
<=> ssList(sK5_skl(nil,nil)) ),
introduced(definition,[new_symbols(definition,[sQ174_spl])],[split_symbol_definition]) ).
fof(f1784,plain,
( sQ174_spl
| ~ ssList(sK5_skl(nil,nil)) ),
inference(component_clause,[status(thm)],[f1782]) ).
fof(f1785,plain,
( ~ sQ67_spl
| ~ sQ174_spl
| sQ173_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f1773,f595,f1779,f1782,f964]) ).
fof(f1786,definition,
! [X0] :
( sQ175_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,[sQ175_spl])],[split_symbol_definition]) ).
fof(f1789,plain,
( ~ sQ67_spl
| ~ sQ13_spl
| sQ175_spl
| ~ sQ174_spl ),
inference(split_clause,[status(thm)],[f1774,f1782,f1786,f595,f964]) ).
fof(f1790,definition,
( sQ176_spl
<=> frontsegP(app(nil,sK5_skl(nil,nil)),nil) ),
introduced(definition,[new_symbols(definition,[sQ176_spl])],[split_symbol_definition]) ).
fof(f1793,plain,
( ~ sQ67_spl
| ~ sQ174_spl
| sQ176_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f1775,f595,f1790,f1782,f964]) ).
fof(f1794,definition,
! [X0] :
( sQ177_spl
<=> ( rearsegP(nil,X0)
| ~ rearsegP(sK5_skl(nil,nil),X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ177_spl])],[split_symbol_definition]) ).
fof(f1797,plain,
( ~ sQ67_spl
| ~ sQ13_spl
| sQ177_spl
| ~ sQ174_spl ),
inference(split_clause,[status(thm)],[f1776,f1782,f1794,f595,f964]) ).
fof(f1798,definition,
! [X0] :
( sQ178_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,[sQ178_spl])],[split_symbol_definition]) ).
fof(f1801,plain,
( ~ sQ67_spl
| ~ sQ13_spl
| ~ sQ174_spl
| sQ178_spl ),
inference(split_clause,[status(thm)],[f1777,f1798,f1782,f595,f964]) ).
fof(f1802,definition,
( sQ179_spl
<=> rearsegP(app(nil,sK5_skl(nil,nil)),sK5_skl(nil,nil)) ),
introduced(definition,[new_symbols(definition,[sQ179_spl])],[split_symbol_definition]) ).
fof(f1805,plain,
( ~ sQ67_spl
| sQ179_spl
| ~ sQ174_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f1778,f595,f1782,f1802,f964]) ).
fof(f1806,plain,
( sQ174_spl
| ~ frontsegP(nil,nil)
| ~ ssList(nil)
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f1784,f122]) ).
fof(f1807,definition,
( sQ180_spl
<=> frontsegP(nil,nil) ),
introduced(definition,[new_symbols(definition,[sQ180_spl])],[split_symbol_definition]) ).
fof(f1809,plain,
( sQ180_spl
| ~ frontsegP(nil,nil) ),
inference(component_clause,[status(thm)],[f1807]) ).
fof(f1810,plain,
( sQ174_spl
| ~ sQ180_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f1806,f595,f1807,f1782]) ).
fof(f1811,plain,
( sQ180_spl
| ~ sQ63_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1809,f960]) ).
fof(f1812,plain,
( sQ180_spl
| ~ sQ63_spl ),
inference(contradiction_clause,[status(thm)],[f1811]) ).
fof(f1856,plain,
! [X0] :
( ~ sQ29_spl
| ~ ssList(nil)
| ~ rearsegP(nil,X0)
| ~ ssList(nil)
| nil = X0
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f729,f309]) ).
fof(f1857,plain,
! [X0,X1,X2] :
( ~ sQ29_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)],[f729,f301]) ).
fof(f1859,definition,
! [X0] :
( sQ183_spl
<=> ( ~ rearsegP(nil,X0)
| nil = X0
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ183_spl])],[split_symbol_definition]) ).
fof(f1863,plain,
( ~ sQ29_spl
| ~ sQ13_spl
| sQ183_spl ),
inference(split_clause,[status(thm)],[f1856,f1859,f595,f724]) ).
fof(f1864,definition,
! [X0,X1,X2] :
( sQ184_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,[sQ184_spl])],[split_symbol_definition]) ).
fof(f1867,plain,
( ~ sQ29_spl
| ~ sQ13_spl
| sQ184_spl ),
inference(split_clause,[status(thm)],[f1857,f1864,f595,f724]) ).
fof(f1870,plain,
! [X0] :
( ~ sQ78_spl
| ~ rearsegP(sK5_skl(sK50_skl,sK50_skl),X0)
| ~ ssList(sK50_skl)
| ~ ssList(sK5_skl(sK50_skl,sK50_skl))
| app(sK6_skl(X0,app(sK50_skl,sK5_skl(sK50_skl,sK50_skl))),X0) = app(sK50_skl,sK5_skl(sK50_skl,sK50_skl))
| ~ ssList(X0)
| ~ ssList(sK50_skl) ),
inference(paramodulation,[status(thm)],[f1040,f675]) ).
fof(f1871,plain,
! [X0] :
( ~ sQ78_spl
| X0 = app(sK50_skl,sK5_skl(sK50_skl,sK50_skl))
| ~ rearsegP(X0,app(sK50_skl,sK5_skl(sK50_skl,sK50_skl)))
| ~ ssList(sK50_skl)
| ~ rearsegP(sK5_skl(sK50_skl,sK50_skl),X0)
| ~ ssList(sK50_skl)
| ~ ssList(X0)
| ~ ssList(sK5_skl(sK50_skl,sK50_skl)) ),
inference(paramodulation,[status(thm)],[f1040,f637]) ).
fof(f1872,plain,
( ~ sQ78_spl
| ~ ssList(sK5_skl(sK50_skl,sK50_skl))
| frontsegP(app(sK50_skl,sK5_skl(sK50_skl,sK50_skl)),sK50_skl)
| ~ ssList(sK50_skl)
| ~ ssList(sK50_skl) ),
inference(paramodulation,[status(thm)],[f1040,f466]) ).
fof(f1873,plain,
! [X0] :
( ~ sQ78_spl
| rearsegP(sK50_skl,X0)
| ~ rearsegP(sK5_skl(sK50_skl,sK50_skl),X0)
| ~ ssList(sK50_skl)
| ~ ssList(X0)
| ~ ssList(sK5_skl(sK50_skl,sK50_skl)) ),
inference(paramodulation,[status(thm)],[f1040,f307]) ).
fof(f1874,plain,
! [X0] :
( ~ sQ78_spl
| ~ ssList(X0)
| ~ ssList(sK50_skl)
| segmentP(app(app(sK50_skl,sK5_skl(sK50_skl,sK50_skl)),X0),sK5_skl(sK50_skl,sK50_skl))
| ~ ssList(sK5_skl(sK50_skl,sK50_skl))
| ~ ssList(app(sK50_skl,X0)) ),
inference(paramodulation,[status(thm)],[f1040,f468]) ).
fof(f1875,plain,
( ~ sQ78_spl
| ~ ssList(sK50_skl)
| rearsegP(app(sK50_skl,sK5_skl(sK50_skl,sK50_skl)),sK5_skl(sK50_skl,sK50_skl))
| ~ ssList(sK5_skl(sK50_skl,sK50_skl))
| ~ ssList(sK50_skl) ),
inference(paramodulation,[status(thm)],[f1040,f467]) ).
fof(f1876,definition,
! [X0] :
( sQ185_spl
<=> ( ~ rearsegP(sK5_skl(sK50_skl,sK50_skl),X0)
| app(sK6_skl(X0,app(sK50_skl,sK5_skl(sK50_skl,sK50_skl))),X0) = app(sK50_skl,sK5_skl(sK50_skl,sK50_skl))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ185_spl])],[split_symbol_definition]) ).
fof(f1879,definition,
( sQ186_spl
<=> ssList(sK5_skl(sK50_skl,sK50_skl)) ),
introduced(definition,[new_symbols(definition,[sQ186_spl])],[split_symbol_definition]) ).
fof(f1880,plain,
( ~ sQ186_spl
| ssList(sK5_skl(sK50_skl,sK50_skl)) ),
inference(component_clause,[status(thm)],[f1879]) ).
fof(f1881,plain,
( sQ186_spl
| ~ ssList(sK5_skl(sK50_skl,sK50_skl)) ),
inference(component_clause,[status(thm)],[f1879]) ).
fof(f1882,plain,
( ~ sQ78_spl
| ~ sQ186_spl
| sQ185_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f1870,f617,f1876,f1879,f1039]) ).
fof(f1883,definition,
! [X0] :
( sQ187_spl
<=> ( X0 = app(sK50_skl,sK5_skl(sK50_skl,sK50_skl))
| ~ rearsegP(X0,app(sK50_skl,sK5_skl(sK50_skl,sK50_skl)))
| ~ rearsegP(sK5_skl(sK50_skl,sK50_skl),X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ187_spl])],[split_symbol_definition]) ).
fof(f1886,plain,
( ~ sQ78_spl
| ~ sQ17_spl
| sQ187_spl
| ~ sQ186_spl ),
inference(split_clause,[status(thm)],[f1871,f1879,f1883,f617,f1039]) ).
fof(f1887,definition,
( sQ188_spl
<=> frontsegP(app(sK50_skl,sK5_skl(sK50_skl,sK50_skl)),sK50_skl) ),
introduced(definition,[new_symbols(definition,[sQ188_spl])],[split_symbol_definition]) ).
fof(f1890,plain,
( ~ sQ78_spl
| ~ sQ186_spl
| sQ188_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f1872,f617,f1887,f1879,f1039]) ).
fof(f1891,definition,
! [X0] :
( sQ189_spl
<=> ( rearsegP(sK50_skl,X0)
| ~ rearsegP(sK5_skl(sK50_skl,sK50_skl),X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ189_spl])],[split_symbol_definition]) ).
fof(f1894,plain,
( ~ sQ78_spl
| ~ sQ17_spl
| sQ189_spl
| ~ sQ186_spl ),
inference(split_clause,[status(thm)],[f1873,f1879,f1891,f617,f1039]) ).
fof(f1895,definition,
! [X0] :
( sQ190_spl
<=> ( ~ ssList(X0)
| segmentP(app(app(sK50_skl,sK5_skl(sK50_skl,sK50_skl)),X0),sK5_skl(sK50_skl,sK50_skl))
| ~ ssList(app(sK50_skl,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ190_spl])],[split_symbol_definition]) ).
fof(f1898,plain,
( ~ sQ78_spl
| ~ sQ17_spl
| ~ sQ186_spl
| sQ190_spl ),
inference(split_clause,[status(thm)],[f1874,f1895,f1879,f617,f1039]) ).
fof(f1899,definition,
( sQ191_spl
<=> rearsegP(app(sK50_skl,sK5_skl(sK50_skl,sK50_skl)),sK5_skl(sK50_skl,sK50_skl)) ),
introduced(definition,[new_symbols(definition,[sQ191_spl])],[split_symbol_definition]) ).
fof(f1900,plain,
( ~ sQ191_spl
| rearsegP(app(sK50_skl,sK5_skl(sK50_skl,sK50_skl)),sK5_skl(sK50_skl,sK50_skl)) ),
inference(component_clause,[status(thm)],[f1899]) ).
fof(f1902,plain,
( ~ sQ78_spl
| sQ191_spl
| ~ sQ186_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f1875,f617,f1879,f1899,f1039]) ).
fof(f1903,plain,
( sQ186_spl
| ~ frontsegP(sK50_skl,sK50_skl)
| ~ ssList(sK50_skl)
| ~ ssList(sK50_skl) ),
inference(resolution,[status(thm)],[f1881,f122]) ).
fof(f1904,definition,
( sQ192_spl
<=> frontsegP(sK50_skl,sK50_skl) ),
introduced(definition,[new_symbols(definition,[sQ192_spl])],[split_symbol_definition]) ).
fof(f1906,plain,
( sQ192_spl
| ~ frontsegP(sK50_skl,sK50_skl) ),
inference(component_clause,[status(thm)],[f1904]) ).
fof(f1907,plain,
( sQ186_spl
| ~ sQ192_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f1903,f617,f1904,f1879]) ).
fof(f1908,plain,
( sQ192_spl
| ~ sQ74_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1906,f1035]) ).
fof(f1909,plain,
( sQ192_spl
| ~ sQ74_spl ),
inference(contradiction_clause,[status(thm)],[f1908]) ).
fof(f1916,plain,
( ~ sQ191_spl
| ~ sQ78_spl
| rearsegP(sK50_skl,sK5_skl(sK50_skl,sK50_skl)) ),
inference(forward_demodulation,[status(thm)],[f1040,f1900]) ).
fof(f1918,plain,
! [X0] :
( ~ sQ186_spl
| ~ rearsegP(sK5_skl(sK50_skl,sK50_skl),X0)
| ~ rearsegP(sK5_skl(sK50_skl,sK50_skl),sK5_skl(sK50_skl,sK50_skl))
| X0 = sK5_skl(sK50_skl,sK50_skl)
| ~ rearsegP(X0,sK5_skl(sK50_skl,sK50_skl))
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f1880,f577]) ).
fof(f1925,definition,
! [X0] :
( sQ193_spl
<=> ( ~ rearsegP(sK5_skl(sK50_skl,sK50_skl),X0)
| X0 = sK5_skl(sK50_skl,sK50_skl)
| ~ rearsegP(X0,sK5_skl(sK50_skl,sK50_skl))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ193_spl])],[split_symbol_definition]) ).
fof(f1928,definition,
( sQ194_spl
<=> rearsegP(sK5_skl(sK50_skl,sK50_skl),sK5_skl(sK50_skl,sK50_skl)) ),
introduced(definition,[new_symbols(definition,[sQ194_spl])],[split_symbol_definition]) ).
fof(f1931,plain,
( ~ sQ186_spl
| ~ sQ194_spl
| sQ193_spl ),
inference(split_clause,[status(thm)],[f1918,f1925,f1928,f1879]) ).
fof(f1933,plain,
! [X0] :
( ~ sQ191_spl
| ~ sQ78_spl
| ~ rearsegP(X0,sK50_skl)
| ~ ssList(sK50_skl)
| app(sK6_skl(sK5_skl(sK50_skl,sK50_skl),X0),sK5_skl(sK50_skl,sK50_skl)) = X0
| ~ ssList(sK5_skl(sK50_skl,sK50_skl))
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f1916,f680]) ).
fof(f1934,plain,
( ~ sQ191_spl
| ~ sQ78_spl
| app(sK6_skl(sK5_skl(sK50_skl,sK50_skl),sK50_skl),sK5_skl(sK50_skl,sK50_skl)) = sK50_skl
| ~ ssList(sK5_skl(sK50_skl,sK50_skl))
| ~ ssList(sK50_skl) ),
inference(resolution,[status(thm)],[f1916,f129]) ).
fof(f1935,plain,
( ~ sQ191_spl
| ~ sQ78_spl
| sK5_skl(sK50_skl,sK50_skl) = sK50_skl
| ~ rearsegP(sK5_skl(sK50_skl,sK50_skl),sK50_skl)
| ~ ssList(sK50_skl)
| ~ ssList(sK5_skl(sK50_skl,sK50_skl)) ),
inference(resolution,[status(thm)],[f1916,f303]) ).
fof(f1936,definition,
! [X0] :
( sQ195_spl
<=> ( ~ rearsegP(X0,sK50_skl)
| app(sK6_skl(sK5_skl(sK50_skl,sK50_skl),X0),sK5_skl(sK50_skl,sK50_skl)) = X0
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ195_spl])],[split_symbol_definition]) ).
fof(f1939,plain,
( ~ sQ191_spl
| ~ sQ78_spl
| ~ sQ17_spl
| ~ sQ186_spl
| sQ195_spl ),
inference(split_clause,[status(thm)],[f1933,f1936,f1879,f617,f1039,f1899]) ).
fof(f1940,definition,
( sQ196_spl
<=> app(sK6_skl(sK5_skl(sK50_skl,sK50_skl),sK50_skl),sK5_skl(sK50_skl,sK50_skl)) = sK50_skl ),
introduced(definition,[new_symbols(definition,[sQ196_spl])],[split_symbol_definition]) ).
fof(f1943,plain,
( ~ sQ191_spl
| ~ sQ78_spl
| sQ196_spl
| ~ sQ186_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f1934,f617,f1879,f1940,f1039,f1899]) ).
fof(f1944,definition,
( sQ197_spl
<=> rearsegP(sK5_skl(sK50_skl,sK50_skl),sK50_skl) ),
introduced(definition,[new_symbols(definition,[sQ197_spl])],[split_symbol_definition]) ).
fof(f1947,definition,
( sQ198_spl
<=> sK5_skl(sK50_skl,sK50_skl) = sK50_skl ),
introduced(definition,[new_symbols(definition,[sQ198_spl])],[split_symbol_definition]) ).
fof(f1950,plain,
( ~ sQ191_spl
| ~ sQ78_spl
| sQ198_spl
| ~ sQ197_spl
| ~ sQ17_spl
| ~ sQ186_spl ),
inference(split_clause,[status(thm)],[f1935,f1879,f617,f1944,f1947,f1039,f1899]) ).
fof(f1951,plain,
( ~ sQ78_spl
| ~ sQ34_spl
| ~ sQ23_spl
| ~ ssList(sK5_skl(sK50_skl,sK50_skl))
| segmentP(app(sK50_skl,sK5_skl(sK50_skl,sK50_skl)),sK49_skl)
| ~ ssList(sK50_skl) ),
inference(paramodulation,[status(thm)],[f1040,f776]) ).
fof(f1953,definition,
( sQ199_spl
<=> segmentP(app(sK50_skl,sK5_skl(sK50_skl,sK50_skl)),sK49_skl) ),
introduced(definition,[new_symbols(definition,[sQ199_spl])],[split_symbol_definition]) ).
fof(f1954,plain,
( ~ sQ199_spl
| segmentP(app(sK50_skl,sK5_skl(sK50_skl,sK50_skl)),sK49_skl) ),
inference(component_clause,[status(thm)],[f1953]) ).
fof(f1956,plain,
( ~ sQ78_spl
| ~ sQ34_spl
| ~ sQ23_spl
| ~ sQ186_spl
| sQ199_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f1951,f617,f1953,f1879,f671,f765,f1039]) ).
fof(f1961,plain,
( ~ sQ199_spl
| ~ sQ78_spl
| segmentP(sK50_skl,sK49_skl) ),
inference(forward_demodulation,[status(thm)],[f1040,f1954]) ).
fof(f1962,plain,
( ~ sQ199_spl
| ~ sQ78_spl
| sQ27_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1961,f698]) ).
fof(f1963,plain,
( ~ sQ199_spl
| ~ sQ78_spl
| sQ27_spl ),
inference(contradiction_clause,[status(thm)],[f1962]) ).
fof(f1964,plain,
$false,
inference(sat_refutation,[status(thm)],[f446,f450,f457,f461,f517,f533,f560,f586,f604,f628,f631,f642,f652,f663,f674,f679,f689,f693,f699,f719,f727,f746,f768,f774,f797,f813,f827,f829,f835,f842,f861,f865,f869,f873,f881,f887,f894,f896,f904,f908,f912,f916,f924,f930,f937,f939,f947,f951,f955,f959,f967,f975,f994,f1002,f1006,f1014,f1022,f1026,f1030,f1034,f1042,f1063,f1070,f1075,f1103,f1117,f1166,f1167,f1171,f1175,f1181,f1213,f1217,f1221,f1225,f1230,f1232,f1269,f1273,f1284,f1288,f1298,f1302,f1306,f1310,f1314,f1318,f1363,f1367,f1372,f1376,f1378,f1403,f1430,f1434,f1438,f1442,f1446,f1451,f1453,f1491,f1495,f1500,f1504,f1506,f1538,f1546,f1550,f1554,f1558,f1562,f1566,f1600,f1604,f1608,f1612,f1616,f1621,f1630,f1643,f1647,f1651,f1655,f1659,f1663,f1668,f1670,f1699,f1703,f1785,f1789,f1793,f1797,f1801,f1805,f1810,f1812,f1863,f1867,f1882,f1886,f1890,f1894,f1898,f1902,f1907,f1909,f1931,f1939,f1943,f1950,f1956,f1963]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWC058+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n012.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Mon Sep 21 07:51:51 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.38 % Drodi V4.1.1
% 0.08/0.45 % Refutation found
% 0.08/0.45 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.08/0.45 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.08/0.49 % Elapsed time: 0.109884 seconds
% 0.08/0.49 % CPU time: 0.565109 seconds
% 0.08/0.49 % Total memory used: 98.544 MB
% 0.08/0.49 % Net memory used: 97.896 MB
%------------------------------------------------------------------------------