%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWC013+1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n006.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:35 PM UTC 2026
% Result : Theorem 2.20s 0.83s
% Output : CNFRefutation 2.20s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 115
% Syntax : Number of formulae : 436 ( 10 unt; 99 def)
% Number of atoms : 2183 ( 290 equ)
% Maximal formula atoms : 21 ( 5 avg)
% Number of connectives : 2993 (1246 ~;1418 |; 165 &)
% ( 112 <=>; 52 =>; 0 <=; 0 <~>)
% Maximal formula depth : 22 ( 8 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 111 ( 109 usr; 98 prp; 0-4 aty)
% Number of functors : 33 ( 33 usr; 5 con; 0-4 aty)
% Number of variables : 1006 ( 954 !; 52 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssItem(V)
=> ( memberP(U,V)
<=> ? [W] :
( ? [X] :
( app(W,cons(V,X)) = U
& ssList(X) )
& ssList(W) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [U] :
( ssList(U)
=> ( singletonP(U)
<=> ? [V] :
( cons(V,nil) = U
& ssItem(V) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [U] :
( ssList(U)
=> ( cyclefreeP(U)
<=> ! [V] :
( ssItem(V)
=> ! [W] :
( ssItem(W)
=> ! [X] :
( ssList(X)
=> ! [Y] :
( ssList(Y)
=> ! [Z] :
( ssList(Z)
=> ( app(app(X,cons(V,Y)),cons(W,Z)) = U
=> ~ ( leq(W,V)
& leq(V,W) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [U] :
( ssList(U)
=> ( totalorderP(U)
<=> ! [V] :
( ssItem(V)
=> ! [W] :
( ssItem(W)
=> ! [X] :
( ssList(X)
=> ! [Y] :
( ssList(Y)
=> ! [Z] :
( ssList(Z)
=> ( app(app(X,cons(V,Y)),cons(W,Z)) = U
=> ( leq(W,V)
| leq(V,W) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [U] :
( ssList(U)
=> ( strictorderP(U)
<=> ! [V] :
( ssItem(V)
=> ! [W] :
( ssItem(W)
=> ! [X] :
( ssList(X)
=> ! [Y] :
( ssList(Y)
=> ! [Z] :
( ssList(Z)
=> ( app(app(X,cons(V,Y)),cons(W,Z)) = U
=> ( lt(W,V)
| lt(V,W) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ( neq(U,V)
<=> U != V ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f16,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssItem(V)
=> ssList(cons(V,U)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f17,axiom,
ssList(nil),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f18,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssItem(V)
=> cons(V,U) != U ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f19,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ! [W] :
( ssItem(W)
=> ! [X] :
( ssItem(X)
=> ( cons(W,U) = cons(X,V)
=> ( V = U
& W = X ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f20,axiom,
! [U] :
( ssList(U)
=> ( ? [V] :
( ? [W] :
( cons(W,V) = U
& ssItem(W) )
& ssList(V) )
| nil = U ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f21,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssItem(V)
=> nil != cons(V,U) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f22,axiom,
! [U] :
( ssList(U)
=> ( nil != U
=> ssItem(hd(U)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f23,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssItem(V)
=> hd(cons(V,U)) = V ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f25,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssItem(V)
=> tl(cons(V,U)) = U ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f96,conjecture,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ! [W] :
( ssList(W)
=> ! [X] :
( ssList(X)
=> ( ( ( neq(X,nil)
| ~ neq(V,nil) )
& ( ? [X1] :
( ? [X2] :
( neq(nil,V)
& hd(V) = X2
& cons(X2,nil) = X1
& ssItem(X2) )
& U = X1
& ssList(X1) )
| ? [Y] :
( ? [Z] :
( neq(nil,X)
& hd(X) = Z
& cons(Z,nil) = Y
& ssItem(Z) )
& W != Y
& ssList(Y) )
| ~ neq(V,nil) ) )
| U != W
| V != X ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f97,negated_conjecture,
~ ! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ! [W] :
( ssList(W)
=> ! [X] :
( ssList(X)
=> ( ( ( neq(X,nil)
| ~ neq(V,nil) )
& ( ? [X1] :
( ? [X2] :
( neq(nil,V)
& hd(V) = X2
& cons(X2,nil) = X1
& ssItem(X2) )
& U = X1
& ssList(X1) )
| ? [Y] :
( ? [Z] :
( neq(nil,X)
& hd(X) = Z
& cons(Z,nil) = Y
& ssItem(Z) )
& W != Y
& ssList(Y) )
| ~ neq(V,nil) ) )
| U != W
| V != X ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f96]) ).
fof(f106,plain,
! [U] :
( ! [V] :
( ( memberP(U,V)
<=> ? [W] :
( ? [X] :
( app(W,cons(V,X)) = U
& ssList(X) )
& ssList(W) ) )
| ~ ssItem(V) )
| ~ ssList(U) ),
inference(pre_NNF_transformation,[status(thm)],[f3]) ).
fof(f107,plain,
! [U] :
( ! [V] :
( ( ( ! [W] :
( ! [X] :
( app(W,cons(V,X)) != U
| ~ ssList(X) )
| ~ ssList(W) )
| memberP(U,V) )
& ( ? [W] :
( ? [X] :
( app(W,cons(V,X)) = U
& ssList(X) )
& ssList(W) )
| ~ memberP(U,V) ) )
| ~ ssItem(V) )
| ~ ssList(U) ),
inference(NNF_transformation,[status(thm)],[f106]) ).
fof(f108,plain,
! [U] :
( ! [V] :
( ( ( ! [W] :
( ! [X] :
( app(W,cons(V,X)) != U
| ~ ssList(X) )
| ~ ssList(W) )
| memberP(U,V) )
& ( ( app(sK2_skl(V,U),cons(V,sK3_skl(V,U))) = U
& ssList(sK3_skl(V,U))
& ssList(sK2_skl(V,U)) )
| ~ memberP(U,V) ) )
| ~ ssItem(V) )
| ~ ssList(U) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl,sK3_skl]),skolemize(W,sK2_skl(V,U)),skolemize(X,sK3_skl(V,U))],[f107]) ).
fof(f112,plain,
! [X0,X1,X2,X3] :
( app(X2,cons(X1,X3)) != X0
| ~ ssList(X3)
| ~ ssList(X2)
| memberP(X0,X1)
| ~ ssItem(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f108]) ).
fof(f113,plain,
! [U] :
( ( singletonP(U)
<=> ? [V] :
( cons(V,nil) = U
& ssItem(V) ) )
| ~ ssList(U) ),
inference(pre_NNF_transformation,[status(thm)],[f4]) ).
fof(f114,plain,
! [U] :
( ( ( ! [V] :
( cons(V,nil) != U
| ~ ssItem(V) )
| singletonP(U) )
& ( ? [V] :
( cons(V,nil) = U
& ssItem(V) )
| ~ singletonP(U) ) )
| ~ ssList(U) ),
inference(NNF_transformation,[status(thm)],[f113]) ).
fof(f115,plain,
! [U] :
( ( ( ! [V] :
( cons(V,nil) != U
| ~ ssItem(V) )
| singletonP(U) )
& ( ( cons(sK4_skl(U),nil) = U
& ssItem(sK4_skl(U)) )
| ~ singletonP(U) ) )
| ~ ssList(U) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl]),skolemize(V,sK4_skl(U))],[f114]) ).
fof(f116,plain,
! [X0] :
( ssItem(sK4_skl(X0))
| ~ singletonP(X0)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f115]) ).
fof(f117,plain,
! [X0] :
( cons(sK4_skl(X0),nil) = X0
| ~ singletonP(X0)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f115]) ).
fof(f118,plain,
! [X0,X1] :
( cons(X1,nil) != X0
| ~ ssItem(X1)
| singletonP(X0)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f115]) ).
fof(f138,plain,
! [U] :
( ( cyclefreeP(U)
<=> ! [V] :
( ! [W] :
( ! [X] :
( ! [Y] :
( ! [Z] :
( ~ leq(W,V)
| ~ leq(V,W)
| app(app(X,cons(V,Y)),cons(W,Z)) != U
| ~ ssList(Z) )
| ~ ssList(Y) )
| ~ ssList(X) )
| ~ ssItem(W) )
| ~ ssItem(V) ) )
| ~ ssList(U) ),
inference(pre_NNF_transformation,[status(thm)],[f8]) ).
fof(f139,plain,
! [U] :
( ( ( ? [V] :
( ? [W] :
( ? [X] :
( ? [Y] :
( ? [Z] :
( leq(W,V)
& leq(V,W)
& app(app(X,cons(V,Y)),cons(W,Z)) = U
& ssList(Z) )
& ssList(Y) )
& ssList(X) )
& ssItem(W) )
& ssItem(V) )
| cyclefreeP(U) )
& ( ! [V] :
( ! [W] :
( ! [X] :
( ! [Y] :
( ! [Z] :
( ~ leq(W,V)
| ~ leq(V,W)
| app(app(X,cons(V,Y)),cons(W,Z)) != U
| ~ ssList(Z) )
| ~ ssList(Y) )
| ~ ssList(X) )
| ~ ssItem(W) )
| ~ ssItem(V) )
| ~ cyclefreeP(U) ) )
| ~ ssList(U) ),
inference(NNF_transformation,[status(thm)],[f138]) ).
fof(f140,plain,
! [U] :
( ( ( ( leq(sK10_skl(U),sK9_skl(U))
& leq(sK9_skl(U),sK10_skl(U))
& app(app(sK11_skl(U),cons(sK9_skl(U),sK12_skl(U))),cons(sK10_skl(U),sK13_skl(U))) = U
& ssList(sK13_skl(U))
& ssList(sK12_skl(U))
& ssList(sK11_skl(U))
& ssItem(sK10_skl(U))
& ssItem(sK9_skl(U)) )
| cyclefreeP(U) )
& ( ! [V] :
( ! [W] :
( ! [X] :
( ! [Y] :
( ! [Z] :
( ~ leq(W,V)
| ~ leq(V,W)
| app(app(X,cons(V,Y)),cons(W,Z)) != U
| ~ ssList(Z) )
| ~ ssList(Y) )
| ~ ssList(X) )
| ~ ssItem(W) )
| ~ ssItem(V) )
| ~ cyclefreeP(U) ) )
| ~ ssList(U) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl,sK10_skl,sK11_skl,sK12_skl,sK13_skl]),skolemize(V,sK9_skl(U)),skolemize(W,sK10_skl(U)),skolemize(X,sK11_skl(U)),skolemize(Y,sK12_skl(U)),skolemize(Z,sK13_skl(U))],[f139]) ).
fof(f141,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ leq(X2,X1)
| ~ leq(X1,X2)
| app(app(X3,cons(X1,X4)),cons(X2,X5)) != X0
| ~ ssList(X5)
| ~ ssList(X4)
| ~ ssList(X3)
| ~ ssItem(X2)
| ~ ssItem(X1)
| ~ cyclefreeP(X0)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f140]) ).
fof(f150,plain,
! [U] :
( ( totalorderP(U)
<=> ! [V] :
( ! [W] :
( ! [X] :
( ! [Y] :
( ! [Z] :
( leq(W,V)
| leq(V,W)
| app(app(X,cons(V,Y)),cons(W,Z)) != U
| ~ ssList(Z) )
| ~ ssList(Y) )
| ~ ssList(X) )
| ~ ssItem(W) )
| ~ ssItem(V) ) )
| ~ ssList(U) ),
inference(pre_NNF_transformation,[status(thm)],[f9]) ).
fof(f151,plain,
! [U] :
( ( ( ? [V] :
( ? [W] :
( ? [X] :
( ? [Y] :
( ? [Z] :
( ~ leq(W,V)
& ~ leq(V,W)
& app(app(X,cons(V,Y)),cons(W,Z)) = U
& ssList(Z) )
& ssList(Y) )
& ssList(X) )
& ssItem(W) )
& ssItem(V) )
| totalorderP(U) )
& ( ! [V] :
( ! [W] :
( ! [X] :
( ! [Y] :
( ! [Z] :
( leq(W,V)
| leq(V,W)
| app(app(X,cons(V,Y)),cons(W,Z)) != U
| ~ ssList(Z) )
| ~ ssList(Y) )
| ~ ssList(X) )
| ~ ssItem(W) )
| ~ ssItem(V) )
| ~ totalorderP(U) ) )
| ~ ssList(U) ),
inference(NNF_transformation,[status(thm)],[f150]) ).
fof(f152,plain,
! [U] :
( ( ( ( ~ leq(sK15_skl(U),sK14_skl(U))
& ~ leq(sK14_skl(U),sK15_skl(U))
& app(app(sK16_skl(U),cons(sK14_skl(U),sK17_skl(U))),cons(sK15_skl(U),sK18_skl(U))) = U
& ssList(sK18_skl(U))
& ssList(sK17_skl(U))
& ssList(sK16_skl(U))
& ssItem(sK15_skl(U))
& ssItem(sK14_skl(U)) )
| totalorderP(U) )
& ( ! [V] :
( ! [W] :
( ! [X] :
( ! [Y] :
( ! [Z] :
( leq(W,V)
| leq(V,W)
| app(app(X,cons(V,Y)),cons(W,Z)) != U
| ~ ssList(Z) )
| ~ ssList(Y) )
| ~ ssList(X) )
| ~ ssItem(W) )
| ~ ssItem(V) )
| ~ totalorderP(U) ) )
| ~ ssList(U) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14_skl,sK15_skl,sK16_skl,sK17_skl,sK18_skl]),skolemize(V,sK14_skl(U)),skolemize(W,sK15_skl(U)),skolemize(X,sK16_skl(U)),skolemize(Y,sK17_skl(U)),skolemize(Z,sK18_skl(U))],[f151]) ).
fof(f153,plain,
! [X0,X1,X2,X3,X4,X5] :
( leq(X2,X1)
| leq(X1,X2)
| app(app(X3,cons(X1,X4)),cons(X2,X5)) != X0
| ~ ssList(X5)
| ~ ssList(X4)
| ~ ssList(X3)
| ~ ssItem(X2)
| ~ ssItem(X1)
| ~ totalorderP(X0)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f152]) ).
fof(f162,plain,
! [U] :
( ( strictorderP(U)
<=> ! [V] :
( ! [W] :
( ! [X] :
( ! [Y] :
( ! [Z] :
( lt(W,V)
| lt(V,W)
| app(app(X,cons(V,Y)),cons(W,Z)) != U
| ~ ssList(Z) )
| ~ ssList(Y) )
| ~ ssList(X) )
| ~ ssItem(W) )
| ~ ssItem(V) ) )
| ~ ssList(U) ),
inference(pre_NNF_transformation,[status(thm)],[f10]) ).
fof(f163,plain,
! [U] :
( ( ( ? [V] :
( ? [W] :
( ? [X] :
( ? [Y] :
( ? [Z] :
( ~ lt(W,V)
& ~ lt(V,W)
& app(app(X,cons(V,Y)),cons(W,Z)) = U
& ssList(Z) )
& ssList(Y) )
& ssList(X) )
& ssItem(W) )
& ssItem(V) )
| strictorderP(U) )
& ( ! [V] :
( ! [W] :
( ! [X] :
( ! [Y] :
( ! [Z] :
( lt(W,V)
| lt(V,W)
| app(app(X,cons(V,Y)),cons(W,Z)) != U
| ~ ssList(Z) )
| ~ ssList(Y) )
| ~ ssList(X) )
| ~ ssItem(W) )
| ~ ssItem(V) )
| ~ strictorderP(U) ) )
| ~ ssList(U) ),
inference(NNF_transformation,[status(thm)],[f162]) ).
fof(f164,plain,
! [U] :
( ( ( ( ~ lt(sK20_skl(U),sK19_skl(U))
& ~ lt(sK19_skl(U),sK20_skl(U))
& app(app(sK21_skl(U),cons(sK19_skl(U),sK22_skl(U))),cons(sK20_skl(U),sK23_skl(U))) = U
& ssList(sK23_skl(U))
& ssList(sK22_skl(U))
& ssList(sK21_skl(U))
& ssItem(sK20_skl(U))
& ssItem(sK19_skl(U)) )
| strictorderP(U) )
& ( ! [V] :
( ! [W] :
( ! [X] :
( ! [Y] :
( ! [Z] :
( lt(W,V)
| lt(V,W)
| app(app(X,cons(V,Y)),cons(W,Z)) != U
| ~ ssList(Z) )
| ~ ssList(Y) )
| ~ ssList(X) )
| ~ ssItem(W) )
| ~ ssItem(V) )
| ~ strictorderP(U) ) )
| ~ ssList(U) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK19_skl,sK20_skl,sK21_skl,sK22_skl,sK23_skl]),skolemize(V,sK19_skl(U)),skolemize(W,sK20_skl(U)),skolemize(X,sK21_skl(U)),skolemize(Y,sK22_skl(U)),skolemize(Z,sK23_skl(U))],[f163]) ).
fof(f165,plain,
! [X0,X1,X2,X3,X4,X5] :
( lt(X2,X1)
| lt(X1,X2)
| app(app(X3,cons(X1,X4)),cons(X2,X5)) != X0
| ~ ssList(X5)
| ~ ssList(X4)
| ~ ssList(X3)
| ~ ssItem(X2)
| ~ ssItem(X1)
| ~ strictorderP(X0)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f164]) ).
fof(f217,plain,
! [U] :
( ! [V] :
( ( neq(U,V)
<=> U != V )
| ~ ssList(V) )
| ~ ssList(U) ),
inference(pre_NNF_transformation,[status(thm)],[f15]) ).
fof(f218,plain,
! [U] :
( ! [V] :
( ( ( U = V
| neq(U,V) )
& ( U != V
| ~ neq(U,V) ) )
| ~ ssList(V) )
| ~ ssList(U) ),
inference(NNF_transformation,[status(thm)],[f217]) ).
fof(f219,plain,
! [X0,X1] :
( X0 != X1
| ~ neq(X0,X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f218]) ).
fof(f220,plain,
! [X0,X1] :
( X0 = X1
| neq(X0,X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f218]) ).
fof(f221,plain,
! [U] :
( ! [V] :
( ssList(cons(V,U))
| ~ ssItem(V) )
| ~ ssList(U) ),
inference(pre_NNF_transformation,[status(thm)],[f16]) ).
fof(f222,plain,
! [X0,X1] :
( ssList(cons(X1,X0))
| ~ ssItem(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f221]) ).
fof(f223,plain,
ssList(nil),
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f224,plain,
! [U] :
( ! [V] :
( cons(V,U) != U
| ~ ssItem(V) )
| ~ ssList(U) ),
inference(pre_NNF_transformation,[status(thm)],[f18]) ).
fof(f225,plain,
! [X0,X1] :
( cons(X1,X0) != X0
| ~ ssItem(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f224]) ).
fof(f226,plain,
! [U] :
( ! [V] :
( ! [W] :
( ! [X] :
( ( V = U
& W = X )
| cons(W,U) != cons(X,V)
| ~ ssItem(X) )
| ~ ssItem(W) )
| ~ ssList(V) )
| ~ ssList(U) ),
inference(pre_NNF_transformation,[status(thm)],[f19]) ).
fof(f227,plain,
! [X0,X1,X2,X3] :
( X2 = X3
| cons(X2,X0) != cons(X3,X1)
| ~ ssItem(X3)
| ~ ssItem(X2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f226]) ).
fof(f228,plain,
! [X0,X1,X2,X3] :
( X1 = X0
| cons(X2,X0) != cons(X3,X1)
| ~ ssItem(X3)
| ~ ssItem(X2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f226]) ).
fof(f229,plain,
! [U] :
( ? [V] :
( ? [W] :
( cons(W,V) = U
& ssItem(W) )
& ssList(V) )
| nil = U
| ~ ssList(U) ),
inference(pre_NNF_transformation,[status(thm)],[f20]) ).
fof(f230,plain,
! [U] :
( ( cons(sK44_skl(U),sK43_skl(U)) = U
& ssItem(sK44_skl(U))
& ssList(sK43_skl(U)) )
| nil = U
| ~ ssList(U) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK43_skl,sK44_skl]),skolemize(V,sK43_skl(U)),skolemize(W,sK44_skl(U))],[f229]) ).
fof(f231,plain,
! [X0] :
( ssList(sK43_skl(X0))
| nil = X0
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f230]) ).
fof(f232,plain,
! [X0] :
( ssItem(sK44_skl(X0))
| nil = X0
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f230]) ).
fof(f233,plain,
! [X0] :
( cons(sK44_skl(X0),sK43_skl(X0)) = X0
| nil = X0
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f230]) ).
fof(f234,plain,
! [U] :
( ! [V] :
( nil != cons(V,U)
| ~ ssItem(V) )
| ~ ssList(U) ),
inference(pre_NNF_transformation,[status(thm)],[f21]) ).
fof(f235,plain,
! [X0,X1] :
( nil != cons(X1,X0)
| ~ ssItem(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f234]) ).
fof(f236,plain,
! [U] :
( ssItem(hd(U))
| nil = U
| ~ ssList(U) ),
inference(pre_NNF_transformation,[status(thm)],[f22]) ).
fof(f237,plain,
! [X0] :
( ssItem(hd(X0))
| nil = X0
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f236]) ).
fof(f238,plain,
! [U] :
( ! [V] :
( hd(cons(V,U)) = V
| ~ ssItem(V) )
| ~ ssList(U) ),
inference(pre_NNF_transformation,[status(thm)],[f23]) ).
fof(f239,plain,
! [X0,X1] :
( hd(cons(X1,X0)) = X1
| ~ ssItem(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f238]) ).
fof(f242,plain,
! [U] :
( ! [V] :
( tl(cons(V,U)) = U
| ~ ssItem(V) )
| ~ ssList(U) ),
inference(pre_NNF_transformation,[status(thm)],[f25]) ).
fof(f243,plain,
! [X0,X1] :
( tl(cons(X1,X0)) = X0
| ~ ssItem(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f242]) ).
fof(f415,plain,
? [U] :
( ? [V] :
( ? [W] :
( ? [X] :
( ( ( ~ neq(X,nil)
& neq(V,nil) )
| ( ! [X1] :
( ! [X2] :
( ~ neq(nil,V)
| hd(V) != X2
| cons(X2,nil) != X1
| ~ ssItem(X2) )
| U != X1
| ~ ssList(X1) )
& ! [Y] :
( ! [Z] :
( ~ neq(nil,X)
| hd(X) != Z
| cons(Z,nil) != Y
| ~ ssItem(Z) )
| W = Y
| ~ ssList(Y) )
& neq(V,nil) ) )
& U = W
& V = X
& ssList(X) )
& ssList(W) )
& ssList(V) )
& ssList(U) ),
inference(pre_NNF_transformation,[status(thm)],[f97]) ).
fof(f416,definition,
! [U,V,W,X] :
( sP0_prd(X,W,V,U)
<=> ( ! [X1] :
( ! [X2] :
( ~ neq(nil,V)
| hd(V) != X2
| cons(X2,nil) != X1
| ~ ssItem(X2) )
| U != X1
| ~ ssList(X1) )
& ! [Y] :
( ! [Z] :
( ~ neq(nil,X)
| hd(X) != Z
| cons(Z,nil) != Y
| ~ ssItem(Z) )
| W = Y
| ~ ssList(Y) )
& neq(V,nil) ) ),
introduced(definition,[new_symbols(definition,[sP0_prd])],[]) ).
fof(f417,plain,
? [U] :
( ? [V] :
( ? [W] :
( ? [X] :
( ( ( ~ neq(X,nil)
& neq(V,nil) )
| sP0_prd(X,W,V,U) )
& U = W
& V = X
& ssList(X) )
& ssList(W) )
& ssList(V) )
& ssList(U) ),
inference(formula_renaming,[status(thm)],[f415,f416]) ).
fof(f418,plain,
( ( ( ~ neq(sK50_skl,nil)
& neq(sK48_skl,nil) )
| sP0_prd(sK50_skl,sK49_skl,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)],[f417]) ).
fof(f419,plain,
ssList(sK47_skl),
inference(cnf_transformation,[status(thm)],[f418]) ).
fof(f420,plain,
ssList(sK48_skl),
inference(cnf_transformation,[status(thm)],[f418]) ).
fof(f423,plain,
sK48_skl = sK50_skl,
inference(cnf_transformation,[status(thm)],[f418]) ).
fof(f424,plain,
sK47_skl = sK49_skl,
inference(cnf_transformation,[status(thm)],[f418]) ).
fof(f425,plain,
( neq(sK48_skl,nil)
| sP0_prd(sK50_skl,sK49_skl,sK48_skl,sK47_skl) ),
inference(cnf_transformation,[status(thm)],[f418]) ).
fof(f426,plain,
( ~ neq(sK50_skl,nil)
| sP0_prd(sK50_skl,sK49_skl,sK48_skl,sK47_skl) ),
inference(cnf_transformation,[status(thm)],[f418]) ).
fof(f427,definition,
! [W,X,Y] :
( sP1_prd(Y,X,W)
<=> ( ! [Z] :
( ~ neq(nil,X)
| hd(X) != Z
| cons(Z,nil) != Y
| ~ ssItem(Z) )
| W = Y
| ~ ssList(Y) ) ),
introduced(definition,[new_symbols(definition,[sP1_prd])],[]) ).
fof(f428,plain,
! [U,V,W,X] :
( sP0_prd(X,W,V,U)
<=> ( ! [X1] :
( ! [X2] :
( ~ neq(nil,V)
| hd(V) != X2
| cons(X2,nil) != X1
| ~ ssItem(X2) )
| U != X1
| ~ ssList(X1) )
& ! [Y] : sP1_prd(Y,X,W)
& neq(V,nil) ) ),
inference(formula_renaming,[status(thm)],[f416,f427]) ).
fof(f429,plain,
! [U,V,W,X] :
( ( ? [X1] :
( ? [X2] :
( neq(nil,V)
& hd(V) = X2
& cons(X2,nil) = X1
& ssItem(X2) )
& U = X1
& ssList(X1) )
| ? [Y] : ~ sP1_prd(Y,X,W)
| ~ neq(V,nil)
| sP0_prd(X,W,V,U) )
& ( ( ! [X1] :
( ! [X2] :
( ~ neq(nil,V)
| hd(V) != X2
| cons(X2,nil) != X1
| ~ ssItem(X2) )
| U != X1
| ~ ssList(X1) )
& ! [Y] : sP1_prd(Y,X,W)
& neq(V,nil) )
| ~ sP0_prd(X,W,V,U) ) ),
inference(NNF_transformation,[status(thm)],[f428]) ).
fof(f430,plain,
( ! [U,V,W,X] :
( ? [X1] :
( neq(nil,V)
& ? [X2] :
( hd(V) = X2
& cons(X2,nil) = X1
& ssItem(X2) )
& U = X1
& ssList(X1) )
| ? [Y] : ~ sP1_prd(Y,X,W)
| ~ neq(V,nil)
| sP0_prd(X,W,V,U) )
& ! [U,V,W,X] :
( ( ! [X1] :
( ~ neq(nil,V)
| ! [X2] :
( hd(V) != X2
| cons(X2,nil) != X1
| ~ ssItem(X2) )
| U != X1
| ~ ssList(X1) )
& ! [Y] : sP1_prd(Y,X,W)
& neq(V,nil) )
| ~ sP0_prd(X,W,V,U) ) ),
inference(miniscoping,[status(thm)],[f429]) ).
fof(f431,plain,
( ! [U,V,W,X] :
( ( neq(nil,V)
& hd(V) = sK53_skl(X,W,V,U)
& cons(sK53_skl(X,W,V,U),nil) = sK52_skl(X,W,V,U)
& ssItem(sK53_skl(X,W,V,U))
& U = sK52_skl(X,W,V,U)
& ssList(sK52_skl(X,W,V,U)) )
| ~ sP1_prd(sK51_skl(X,W,V,U),X,W)
| ~ neq(V,nil)
| sP0_prd(X,W,V,U) )
& ! [U,V,W,X] :
( ( ! [X1] :
( ~ neq(nil,V)
| ! [X2] :
( hd(V) != X2
| cons(X2,nil) != X1
| ~ ssItem(X2) )
| U != X1
| ~ ssList(X1) )
& ! [Y] : sP1_prd(Y,X,W)
& neq(V,nil) )
| ~ sP0_prd(X,W,V,U) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK51_skl,sK52_skl,sK53_skl]),skolemize(Y,sK51_skl(X,W,V,U)),skolemize(X1,sK52_skl(X,W,V,U)),skolemize(X2,sK53_skl(X,W,V,U))],[f430]) ).
fof(f432,plain,
! [X0,X1,X2,X3] :
( neq(X2,nil)
| ~ sP0_prd(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f431]) ).
fof(f433,plain,
! [X0,X1,X2,X3,X4] :
( sP1_prd(X4,X0,X1)
| ~ sP0_prd(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f431]) ).
fof(f434,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ neq(nil,X2)
| hd(X2) != X5
| cons(X5,nil) != X4
| ~ ssItem(X5)
| X3 != X4
| ~ ssList(X4)
| ~ sP0_prd(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f431]) ).
fof(f440,plain,
! [X0,X1,X2,X3] :
( neq(nil,X2)
| ~ sP1_prd(sK51_skl(X0,X1,X2,X3),X0,X1)
| ~ neq(X2,nil)
| sP0_prd(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f431]) ).
fof(f441,plain,
! [W,X,Y] :
( ( ( ? [Z] :
( neq(nil,X)
& hd(X) = Z
& cons(Z,nil) = Y
& ssItem(Z) )
& W != Y
& ssList(Y) )
| sP1_prd(Y,X,W) )
& ( ! [Z] :
( ~ neq(nil,X)
| hd(X) != Z
| cons(Z,nil) != Y
| ~ ssItem(Z) )
| W = Y
| ~ ssList(Y)
| ~ sP1_prd(Y,X,W) ) ),
inference(NNF_transformation,[status(thm)],[f427]) ).
fof(f442,plain,
( ! [W,X,Y] :
( ( neq(nil,X)
& ? [Z] :
( hd(X) = Z
& cons(Z,nil) = Y
& ssItem(Z) )
& W != Y
& ssList(Y) )
| sP1_prd(Y,X,W) )
& ! [W,X,Y] :
( ~ neq(nil,X)
| ! [Z] :
( hd(X) != Z
| cons(Z,nil) != Y
| ~ ssItem(Z) )
| W = Y
| ~ ssList(Y)
| ~ sP1_prd(Y,X,W) ) ),
inference(miniscoping,[status(thm)],[f441]) ).
fof(f443,plain,
( ! [W,X,Y] :
( ( neq(nil,X)
& hd(X) = sK54_skl(Y,X,W)
& cons(sK54_skl(Y,X,W),nil) = Y
& ssItem(sK54_skl(Y,X,W))
& W != Y
& ssList(Y) )
| sP1_prd(Y,X,W) )
& ! [W,X,Y] :
( ~ neq(nil,X)
| ! [Z] :
( hd(X) != Z
| cons(Z,nil) != Y
| ~ ssItem(Z) )
| W = Y
| ~ ssList(Y)
| ~ sP1_prd(Y,X,W) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK54_skl]),skolemize(Z,sK54_skl(Y,X,W))],[f442]) ).
fof(f444,plain,
! [X0,X1,X2,X3] :
( ~ neq(nil,X1)
| hd(X1) != X3
| cons(X3,nil) != X0
| ~ ssItem(X3)
| X2 = X0
| ~ ssList(X0)
| ~ sP1_prd(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f443]) ).
fof(f447,plain,
! [X0,X1,X2] :
( ssItem(sK54_skl(X0,X1,X2))
| sP1_prd(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f443]) ).
fof(f448,plain,
! [X0,X1,X2] :
( cons(sK54_skl(X0,X1,X2),nil) = X0
| sP1_prd(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f443]) ).
fof(f449,plain,
! [X0,X1,X2] :
( hd(X1) = sK54_skl(X0,X1,X2)
| sP1_prd(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f443]) ).
fof(f450,plain,
! [X0,X1,X2] :
( neq(nil,X1)
| sP1_prd(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f443]) ).
fof(f451,definition,
( sQ0_spl
<=> sP0_prd(sK50_skl,sK49_skl,sK48_skl,sK47_skl) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f452,plain,
( ~ sQ0_spl
| sP0_prd(sK50_skl,sK49_skl,sK48_skl,sK47_skl) ),
inference(component_clause,[status(thm)],[f451]) ).
fof(f454,definition,
( sQ1_spl
<=> neq(sK48_skl,nil) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f455,plain,
( ~ sQ1_spl
| neq(sK48_skl,nil) ),
inference(component_clause,[status(thm)],[f454]) ).
fof(f457,plain,
( sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f425,f451,f454]) ).
fof(f458,definition,
( sQ2_spl
<=> neq(sK50_skl,nil) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f460,plain,
( sQ2_spl
| ~ neq(sK50_skl,nil) ),
inference(component_clause,[status(thm)],[f458]) ).
fof(f461,plain,
( ~ sQ2_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f426,f451,f458]) ).
fof(f464,plain,
! [X0,X1,X2] :
( ~ ssList(X2)
| ~ ssList(X0)
| memberP(app(X0,cons(X1,X2)),X1)
| ~ ssItem(X1)
| ~ ssList(app(X0,cons(X1,X2))) ),
inference(destructive_equality_resolution,[status(thm)],[f112]) ).
fof(f465,plain,
! [X0] :
( ~ ssItem(X0)
| singletonP(cons(X0,nil))
| ~ ssList(cons(X0,nil)) ),
inference(destructive_equality_resolution,[status(thm)],[f118]) ).
fof(f469,plain,
! [X0,X1,X2,X3,X4] :
( ~ leq(X3,X1)
| ~ leq(X1,X3)
| ~ ssList(X4)
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssItem(X3)
| ~ ssItem(X1)
| ~ cyclefreeP(app(app(X0,cons(X1,X2)),cons(X3,X4)))
| ~ ssList(app(app(X0,cons(X1,X2)),cons(X3,X4))) ),
inference(destructive_equality_resolution,[status(thm)],[f141]) ).
fof(f470,plain,
! [X0,X1,X2,X3,X4] :
( leq(X3,X1)
| leq(X1,X3)
| ~ ssList(X4)
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssItem(X3)
| ~ ssItem(X1)
| ~ totalorderP(app(app(X0,cons(X1,X2)),cons(X3,X4)))
| ~ ssList(app(app(X0,cons(X1,X2)),cons(X3,X4))) ),
inference(destructive_equality_resolution,[status(thm)],[f153]) ).
fof(f471,plain,
! [X0,X1,X2,X3,X4] :
( lt(X3,X1)
| lt(X1,X3)
| ~ ssList(X4)
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssItem(X3)
| ~ ssItem(X1)
| ~ strictorderP(app(app(X0,cons(X1,X2)),cons(X3,X4)))
| ~ ssList(app(app(X0,cons(X1,X2)),cons(X3,X4))) ),
inference(destructive_equality_resolution,[status(thm)],[f165]) ).
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,X1,X2] :
( ~ neq(nil,X2)
| ~ ssItem(hd(X2))
| ~ ssList(cons(hd(X2),nil))
| ~ sP0_prd(X0,X1,X2,cons(hd(X2),nil)) ),
inference(destructive_equality_resolution,[status(thm)],[f434]) ).
fof(f493,plain,
! [X0,X1] :
( ~ neq(nil,X0)
| ~ ssItem(hd(X0))
| X1 = cons(hd(X0),nil)
| ~ ssList(cons(hd(X0),nil))
| ~ sP1_prd(cons(hd(X0),nil),X0,X1) ),
inference(destructive_equality_resolution,[status(thm)],[f444]) ).
fof(f501,plain,
! [X0,X1] :
( ~ ssItem(sK54_skl(nil,X0,X1))
| ~ ssList(nil)
| sP1_prd(nil,X0,X1) ),
inference(resolution,[status(thm)],[f448,f225]) ).
fof(f502,plain,
! [X0,X1,X2] :
( sP1_prd(X0,X1,X2)
| ssList(X0)
| ~ ssItem(sK54_skl(X0,X1,X2))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f448,f222]) ).
fof(f503,plain,
! [X0,X1,X2] :
( sP1_prd(X0,X1,X2)
| X0 != nil
| ~ ssItem(sK54_skl(X0,X1,X2))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f448,f225]) ).
fof(f504,definition,
! [X0,X1] :
( sQ3_spl
<=> ( ~ ssItem(sK54_skl(nil,X0,X1))
| sP1_prd(nil,X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f507,definition,
( sQ4_spl
<=> ssList(nil) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f509,plain,
( sQ4_spl
| ~ ssList(nil) ),
inference(component_clause,[status(thm)],[f507]) ).
fof(f510,plain,
( ~ sQ4_spl
| sQ3_spl ),
inference(split_clause,[status(thm)],[f501,f504,f507]) ).
fof(f511,definition,
! [X0,X1,X2] :
( sQ5_spl
<=> ( sP1_prd(X0,X1,X2)
| ssList(X0)
| ~ ssItem(sK54_skl(X0,X1,X2)) ) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f514,plain,
( sQ5_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f502,f507,f511]) ).
fof(f515,definition,
! [X0,X1,X2] :
( sQ6_spl
<=> ( sP1_prd(X0,X1,X2)
| X0 != nil
| ~ ssItem(sK54_skl(X0,X1,X2)) ) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f518,plain,
( sQ6_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f503,f507,f515]) ).
fof(f519,plain,
( sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f509,f223]) ).
fof(f520,plain,
sQ4_spl,
inference(contradiction_clause,[status(thm)],[f519]) ).
fof(f530,plain,
! [X0,X1,X2] :
( sP1_prd(X0,X1,X2)
| hd(X0) = sK54_skl(X0,X1,X2)
| ~ ssItem(sK54_skl(X0,X1,X2))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f448,f239]) ).
fof(f531,definition,
! [X0,X1,X2] :
( sQ7_spl
<=> ( sP1_prd(X0,X1,X2)
| hd(X0) = sK54_skl(X0,X1,X2)
| ~ ssItem(sK54_skl(X0,X1,X2)) ) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f532,plain,
! [X0,X1,X2] :
( ~ sQ7_spl
| sP1_prd(X0,X1,X2)
| hd(X0) = sK54_skl(X0,X1,X2)
| ~ ssItem(sK54_skl(X0,X1,X2)) ),
inference(component_clause,[status(thm)],[f531]) ).
fof(f534,plain,
( sQ7_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f530,f507,f531]) ).
fof(f535,plain,
! [X0,X1,X2] :
( ~ sQ7_spl
| sP1_prd(X0,X1,X2)
| hd(X0) = sK54_skl(X0,X1,X2) ),
inference(forward_subsumption_resolution,[status(thm)],[f532,f447]) ).
fof(f538,plain,
( ~ sQ0_spl
| sP0_prd(sK48_skl,sK49_skl,sK48_skl,sK47_skl) ),
inference(forward_demodulation,[status(thm)],[f423,f452]) ).
fof(f539,plain,
( ~ sQ0_spl
| sP0_prd(sK48_skl,sK47_skl,sK48_skl,sK47_skl) ),
inference(forward_demodulation,[status(thm)],[f424,f538]) ).
fof(f540,plain,
! [X0] :
( ~ sQ0_spl
| sP1_prd(X0,sK48_skl,sK47_skl) ),
inference(resolution,[status(thm)],[f539,f433]) ).
fof(f541,plain,
( ~ sQ0_spl
| neq(sK48_skl,nil) ),
inference(resolution,[status(thm)],[f539,f432]) ).
fof(f544,plain,
! [X0,X1,X2,X3] :
( sP1_prd(cons(X1,X0),X2,X3)
| sK54_skl(cons(X1,X0),X2,X3) = X1
| ~ ssItem(X1)
| ~ ssItem(sK54_skl(cons(X1,X0),X2,X3))
| ~ ssList(X0)
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f227,f448]) ).
fof(f546,plain,
! [X0,X1,X2,X3,X4] :
( sP1_prd(X1,X2,X3)
| sK54_skl(X1,X2,X3) = X4
| X1 != cons(X4,X0)
| ~ ssItem(X4)
| ~ ssItem(sK54_skl(X1,X2,X3))
| ~ ssList(X0)
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f448,f227]) ).
fof(f548,plain,
! [X0,X1] :
( X1 = X1
| ~ ssItem(X1)
| ~ ssItem(X1)
| ~ ssList(X0)
| ~ ssList(X0) ),
inference(equality_resolution,[status(thm)],[f227]) ).
fof(f549,definition,
! [X0,X1,X2,X3] :
( sQ8_spl
<=> ( sP1_prd(cons(X1,X0),X2,X3)
| sK54_skl(cons(X1,X0),X2,X3) = X1
| ~ ssItem(X1)
| ~ ssItem(sK54_skl(cons(X1,X0),X2,X3))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f552,plain,
( sQ8_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f544,f507,f549]) ).
fof(f554,definition,
! [X0,X1,X2,X3,X4] :
( sQ9_spl
<=> ( sP1_prd(X1,X2,X3)
| sK54_skl(X1,X2,X3) = X4
| X1 != cons(X4,X0)
| ~ ssItem(X4)
| ~ ssItem(sK54_skl(X1,X2,X3))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f557,plain,
( sQ9_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f546,f507,f554]) ).
fof(f559,definition,
! [X0] :
( sQ10_spl
<=> ( ~ ssList(X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f560,plain,
! [X0] :
( ~ sQ10_spl
| ~ ssList(X0)
| ~ ssList(X0) ),
inference(component_clause,[status(thm)],[f559]) ).
fof(f562,definition,
! [X1] :
( sQ11_spl
<=> ( X1 = X1
| ~ ssItem(X1)
| ~ ssItem(X1) ) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f565,plain,
( sQ11_spl
| sQ10_spl ),
inference(split_clause,[status(thm)],[f548,f559,f562]) ).
fof(f569,plain,
! [X0] :
( ~ sQ10_spl
| ~ ssList(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f560]) ).
fof(f570,plain,
! [X0,X1,X2,X3] :
( sP1_prd(cons(X1,X0),X2,X3)
| X0 = nil
| ~ ssItem(X1)
| ~ ssItem(sK54_skl(cons(X1,X0),X2,X3))
| ~ ssList(X0)
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f228,f448]) ).
fof(f572,plain,
! [X0,X1,X2,X3,X4] :
( sP1_prd(X1,X2,X3)
| X0 = nil
| X1 != cons(X4,X0)
| ~ ssItem(X4)
| ~ ssItem(sK54_skl(X1,X2,X3))
| ~ ssList(X0)
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f448,f228]) ).
fof(f575,definition,
! [X0,X1,X2,X3] :
( sQ12_spl
<=> ( sP1_prd(cons(X1,X0),X2,X3)
| X0 = nil
| ~ ssItem(X1)
| ~ ssItem(sK54_skl(cons(X1,X0),X2,X3))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f578,plain,
( sQ12_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f570,f507,f575]) ).
fof(f580,definition,
! [X0,X1,X2,X3,X4] :
( sQ13_spl
<=> ( sP1_prd(X1,X2,X3)
| X0 = nil
| X1 != cons(X4,X0)
| ~ ssItem(X4)
| ~ ssItem(sK54_skl(X1,X2,X3))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f583,plain,
( sQ13_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f572,f507,f580]) ).
fof(f600,plain,
( ~ sQ10_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f223,f569]) ).
fof(f604,plain,
~ sQ10_spl,
inference(contradiction_clause,[status(thm)],[f600]) ).
fof(f607,plain,
! [X0,X1,X2,X3] :
( sP1_prd(X1,X2,X3)
| ~ ssList(nil)
| ~ ssList(X0)
| memberP(app(X0,X1),sK54_skl(X1,X2,X3))
| ~ ssItem(sK54_skl(X1,X2,X3))
| ~ ssList(app(X0,cons(sK54_skl(X1,X2,X3),nil))) ),
inference(paramodulation,[status(thm)],[f448,f464]) ).
fof(f608,definition,
! [X0,X1,X2,X3] :
( sQ16_spl
<=> ( sP1_prd(X1,X2,X3)
| ~ ssList(X0)
| memberP(app(X0,X1),sK54_skl(X1,X2,X3))
| ~ ssItem(sK54_skl(X1,X2,X3))
| ~ ssList(app(X0,cons(sK54_skl(X1,X2,X3),nil))) ) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f611,plain,
( ~ sQ4_spl
| sQ16_spl ),
inference(split_clause,[status(thm)],[f607,f608,f507]) ).
fof(f616,plain,
( ~ singletonP(nil)
| ~ ssList(nil)
| ~ ssItem(sK4_skl(nil))
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f225,f117]) ).
fof(f619,definition,
( sQ17_spl
<=> ssItem(sK4_skl(nil)) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f621,plain,
( sQ17_spl
| ~ ssItem(sK4_skl(nil)) ),
inference(component_clause,[status(thm)],[f619]) ).
fof(f622,definition,
( sQ18_spl
<=> singletonP(nil) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f625,plain,
( ~ sQ18_spl
| ~ sQ17_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f616,f507,f619,f622]) ).
fof(f640,plain,
! [X0,X1,X2] :
( sP1_prd(X0,X1,X2)
| cons(hd(X1),nil) = X0
| sP1_prd(X0,X1,X2) ),
inference(paramodulation,[status(thm)],[f449,f448]) ).
fof(f641,plain,
! [X0,X1,X2] :
( sP1_prd(X0,X1,X2)
| ssItem(hd(X1))
| sP1_prd(X0,X1,X2) ),
inference(paramodulation,[status(thm)],[f449,f447]) ).
fof(f642,plain,
! [X0,X1,X2] :
( cons(hd(X1),nil) = X0
| sP1_prd(X0,X1,X2) ),
inference(duplicate_literals_removal,[status(thm)],[f640]) ).
fof(f643,plain,
! [X0,X1,X2] :
( ssItem(hd(X1))
| sP1_prd(X0,X1,X2) ),
inference(duplicate_literals_removal,[status(thm)],[f641]) ).
fof(f650,plain,
! [X0,X1,X2] :
( sP1_prd(X0,X1,X2)
| ~ ssItem(sK54_skl(X0,X1,X2))
| singletonP(X0)
| ~ ssList(cons(sK54_skl(X0,X1,X2),nil)) ),
inference(paramodulation,[status(thm)],[f448,f465]) ).
fof(f651,plain,
! [X0,X1,X2] :
( sP1_prd(X0,X1,X2)
| singletonP(X0)
| ~ ssList(cons(sK54_skl(X0,X1,X2),nil)) ),
inference(forward_subsumption_resolution,[status(thm)],[f650,f447]) ).
fof(f652,plain,
! [X0,X1,X2] :
( ~ ssItem(sK54_skl(X0,X1,X2))
| ~ ssList(nil)
| sP1_prd(X0,X1,X2)
| singletonP(X0) ),
inference(resolution,[status(thm)],[f651,f222]) ).
fof(f655,definition,
! [X0,X1,X2] :
( sQ19_spl
<=> ( ~ ssItem(sK54_skl(X0,X1,X2))
| sP1_prd(X0,X1,X2)
| singletonP(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f658,plain,
( ~ sQ4_spl
| sQ19_spl ),
inference(split_clause,[status(thm)],[f652,f655,f507]) ).
fof(f667,plain,
! [X0,X1,X2] :
( ~ sQ7_spl
| sP1_prd(X0,X1,X2)
| cons(hd(X0),nil) = X0
| sP1_prd(X0,X1,X2) ),
inference(paramodulation,[status(thm)],[f535,f448]) ).
fof(f671,plain,
! [X0,X1,X2] :
( ~ sQ7_spl
| cons(hd(X0),nil) = X0
| sP1_prd(X0,X1,X2) ),
inference(duplicate_literals_removal,[status(thm)],[f667]) ).
fof(f684,plain,
! [X0,X1] :
( ~ ssItem(hd(X0))
| ~ ssList(nil)
| sP1_prd(nil,X0,X1) ),
inference(resolution,[status(thm)],[f642,f225]) ).
fof(f691,plain,
! [X0,X1,X2] :
( sP1_prd(X1,X0,X2)
| hd(X1) = hd(X0)
| ~ ssItem(hd(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f642,f239]) ).
fof(f692,plain,
! [X0,X1,X2] :
( sP1_prd(X1,X0,X2)
| ssList(X1)
| ~ ssItem(hd(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f642,f222]) ).
fof(f693,plain,
! [X0,X1,X2] :
( sP1_prd(X1,X0,X2)
| nil != X1
| ~ ssItem(hd(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f642,f235]) ).
fof(f695,plain,
! [X0,X1,X2,X3] :
( sP1_prd(X2,X1,X3)
| ~ ssList(nil)
| ~ ssList(X0)
| memberP(app(X0,X2),hd(X1))
| ~ ssItem(hd(X1))
| ~ ssList(app(X0,cons(hd(X1),nil))) ),
inference(paramodulation,[status(thm)],[f642,f464]) ).
fof(f696,definition,
! [X0,X1] :
( sQ20_spl
<=> ( ~ ssItem(hd(X0))
| sP1_prd(nil,X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f699,plain,
( ~ sQ4_spl
| sQ20_spl ),
inference(split_clause,[status(thm)],[f684,f696,f507]) ).
fof(f702,definition,
! [X0,X1,X2] :
( sQ21_spl
<=> ( sP1_prd(X1,X0,X2)
| hd(X1) = hd(X0)
| ~ ssItem(hd(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f705,plain,
( sQ21_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f691,f507,f702]) ).
fof(f706,definition,
! [X0,X1,X2] :
( sQ22_spl
<=> ( sP1_prd(X1,X0,X2)
| ssList(X1)
| ~ ssItem(hd(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f709,plain,
( sQ22_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f692,f507,f706]) ).
fof(f710,definition,
! [X0,X1,X2] :
( sQ23_spl
<=> ( sP1_prd(X1,X0,X2)
| nil != X1
| ~ ssItem(hd(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f713,plain,
( sQ23_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f693,f507,f710]) ).
fof(f715,definition,
! [X0,X1,X2,X3] :
( sQ24_spl
<=> ( sP1_prd(X2,X1,X3)
| ~ ssList(X0)
| memberP(app(X0,X2),hd(X1))
| ~ ssItem(hd(X1))
| ~ ssList(app(X0,cons(hd(X1),nil))) ) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f718,plain,
( ~ sQ4_spl
| sQ24_spl ),
inference(split_clause,[status(thm)],[f695,f715,f507]) ).
fof(f724,plain,
! [X0,X1] :
( ~ sQ7_spl
| ~ ssItem(hd(nil))
| ~ ssList(nil)
| sP1_prd(nil,X0,X1) ),
inference(resolution,[status(thm)],[f671,f225]) ).
fof(f732,plain,
! [X0,X1,X2] :
( ~ sQ7_spl
| sP1_prd(X0,X1,X2)
| hd(X0) = hd(X0)
| ~ ssItem(hd(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f671,f239]) ).
fof(f733,plain,
! [X0,X1,X2] :
( ~ sQ7_spl
| sP1_prd(X0,X1,X2)
| ssList(X0)
| ~ ssItem(hd(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f671,f222]) ).
fof(f734,plain,
! [X0,X1,X2] :
( ~ sQ7_spl
| sP1_prd(X0,X1,X2)
| nil != X0
| ~ ssItem(hd(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f671,f235]) ).
fof(f736,plain,
! [X0,X1,X2,X3] :
( ~ sQ7_spl
| sP1_prd(X1,X2,X3)
| ~ ssList(nil)
| ~ ssList(X0)
| memberP(app(X0,X1),hd(X1))
| ~ ssItem(hd(X1))
| ~ ssList(app(X0,cons(hd(X1),nil))) ),
inference(paramodulation,[status(thm)],[f671,f464]) ).
fof(f737,definition,
! [X0,X1] :
( sQ25_spl
<=> sP1_prd(nil,X0,X1) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f740,definition,
( sQ26_spl
<=> ssItem(hd(nil)) ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f743,plain,
( ~ sQ7_spl
| ~ sQ26_spl
| ~ sQ4_spl
| sQ25_spl ),
inference(split_clause,[status(thm)],[f724,f737,f507,f740,f531]) ).
fof(f746,definition,
! [X0,X1,X2] :
( sQ27_spl
<=> ( sP1_prd(X0,X1,X2)
| hd(X0) = hd(X0)
| ~ ssItem(hd(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f749,plain,
( ~ sQ7_spl
| sQ27_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f732,f507,f746,f531]) ).
fof(f750,definition,
! [X0,X1,X2] :
( sQ28_spl
<=> ( sP1_prd(X0,X1,X2)
| ssList(X0)
| ~ ssItem(hd(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f753,plain,
( ~ sQ7_spl
| sQ28_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f733,f507,f750,f531]) ).
fof(f754,definition,
! [X0,X1,X2] :
( sQ29_spl
<=> ( sP1_prd(X0,X1,X2)
| nil != X0
| ~ ssItem(hd(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f757,plain,
( ~ sQ7_spl
| sQ29_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f734,f507,f754,f531]) ).
fof(f759,definition,
! [X0,X1,X2,X3] :
( sQ30_spl
<=> ( sP1_prd(X1,X2,X3)
| ~ ssList(X0)
| memberP(app(X0,X1),hd(X1))
| ~ ssItem(hd(X1))
| ~ ssList(app(X0,cons(hd(X1),nil))) ) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f762,plain,
( ~ sQ7_spl
| ~ sQ4_spl
| sQ30_spl ),
inference(split_clause,[status(thm)],[f736,f759,f507,f531]) ).
fof(f775,definition,
( sQ32_spl
<=> nil = nil ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f844,plain,
! [X0,X1,X2,X3] :
( ~ sQ7_spl
| sP1_prd(cons(X1,X0),X2,X3)
| X0 = nil
| ~ ssItem(X1)
| ~ ssItem(hd(cons(X1,X0)))
| ~ ssList(X0)
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f228,f671]) ).
fof(f845,plain,
! [X0,X1,X2,X3] :
( sP1_prd(cons(X2,X0),X1,X3)
| X0 = nil
| ~ ssItem(X2)
| ~ ssItem(hd(X1))
| ~ ssList(X0)
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f228,f642]) ).
fof(f846,plain,
! [X0,X1] :
( ~ singletonP(cons(X1,X0))
| ~ ssList(cons(X1,X0))
| X0 = nil
| ~ ssItem(X1)
| ~ ssItem(sK4_skl(cons(X1,X0)))
| ~ ssList(X0)
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f228,f117]) ).
fof(f853,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ7_spl
| sP1_prd(X1,X3,X4)
| X0 = nil
| X1 != cons(X2,X0)
| ~ ssItem(X2)
| ~ ssItem(hd(X1))
| ~ ssList(X0)
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f671,f228]) ).
fof(f854,plain,
! [X0,X1,X2,X3,X4] :
( sP1_prd(X3,X1,X4)
| X0 = nil
| X3 != cons(X2,X0)
| ~ ssItem(X2)
| ~ ssItem(hd(X1))
| ~ ssList(X0)
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f642,f228]) ).
fof(f861,definition,
! [X0,X1,X2,X3] :
( sQ39_spl
<=> ( sP1_prd(cons(X1,X0),X2,X3)
| X0 = nil
| ~ ssItem(X1)
| ~ ssItem(hd(cons(X1,X0)))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f864,plain,
( ~ sQ7_spl
| sQ39_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f844,f507,f861,f531]) ).
fof(f865,definition,
! [X0,X1,X2,X3] :
( sQ40_spl
<=> ( sP1_prd(cons(X2,X0),X1,X3)
| X0 = nil
| ~ ssItem(X2)
| ~ ssItem(hd(X1))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f868,plain,
( sQ40_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f845,f507,f865]) ).
fof(f869,definition,
! [X0,X1] :
( sQ41_spl
<=> ( ~ singletonP(cons(X1,X0))
| ~ ssList(cons(X1,X0))
| X0 = nil
| ~ ssItem(X1)
| ~ ssItem(sK4_skl(cons(X1,X0)))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition]) ).
fof(f872,plain,
( sQ41_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f846,f507,f869]) ).
fof(f878,definition,
! [X0,X1,X2,X3,X4] :
( sQ42_spl
<=> ( sP1_prd(X1,X3,X4)
| X0 = nil
| X1 != cons(X2,X0)
| ~ ssItem(X2)
| ~ ssItem(hd(X1))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f881,plain,
( ~ sQ7_spl
| sQ42_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f853,f507,f878,f531]) ).
fof(f882,definition,
! [X0,X1,X2,X3,X4] :
( sQ43_spl
<=> ( sP1_prd(X3,X1,X4)
| X0 = nil
| X3 != cons(X2,X0)
| ~ ssItem(X2)
| ~ ssItem(hd(X1))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f885,plain,
( sQ43_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f854,f507,f882]) ).
fof(f894,plain,
! [X0,X1,X2,X3] :
( ~ sQ7_spl
| sP1_prd(cons(X1,X0),X2,X3)
| hd(cons(X1,X0)) = X1
| ~ ssItem(X1)
| ~ ssItem(hd(cons(X1,X0)))
| ~ ssList(X0)
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f227,f671]) ).
fof(f895,plain,
! [X0,X1,X2,X3] :
( sP1_prd(cons(X2,X0),X1,X3)
| hd(X1) = X2
| ~ ssItem(X2)
| ~ ssItem(hd(X1))
| ~ ssList(X0)
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f227,f642]) ).
fof(f896,plain,
! [X0,X1] :
( ~ singletonP(cons(X1,X0))
| ~ ssList(cons(X1,X0))
| sK4_skl(cons(X1,X0)) = X1
| ~ ssItem(X1)
| ~ ssItem(sK4_skl(cons(X1,X0)))
| ~ ssList(X0)
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f227,f117]) ).
fof(f903,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ7_spl
| sP1_prd(X1,X3,X4)
| hd(X1) = X2
| X1 != cons(X2,X0)
| ~ ssItem(X2)
| ~ ssItem(hd(X1))
| ~ ssList(X0)
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f671,f227]) ).
fof(f904,plain,
! [X0,X1,X2,X3,X4] :
( sP1_prd(X3,X1,X4)
| hd(X1) = X2
| X3 != cons(X2,X0)
| ~ ssItem(X2)
| ~ ssItem(hd(X1))
| ~ ssList(X0)
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f642,f227]) ).
fof(f911,definition,
! [X0,X1,X2,X3] :
( sQ44_spl
<=> ( sP1_prd(cons(X1,X0),X2,X3)
| hd(cons(X1,X0)) = X1
| ~ ssItem(X1)
| ~ ssItem(hd(cons(X1,X0)))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition]) ).
fof(f914,plain,
( ~ sQ7_spl
| sQ44_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f894,f507,f911,f531]) ).
fof(f915,definition,
! [X0,X1,X2,X3] :
( sQ45_spl
<=> ( sP1_prd(cons(X2,X0),X1,X3)
| hd(X1) = X2
| ~ ssItem(X2)
| ~ ssItem(hd(X1))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition]) ).
fof(f916,plain,
! [X0,X1,X2,X3] :
( ~ sQ45_spl
| sP1_prd(cons(X2,X0),X1,X3)
| hd(X1) = X2
| ~ ssItem(X2)
| ~ ssItem(hd(X1))
| ~ ssList(X0) ),
inference(component_clause,[status(thm)],[f915]) ).
fof(f918,plain,
( sQ45_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f895,f507,f915]) ).
fof(f919,definition,
! [X0,X1] :
( sQ46_spl
<=> ( ~ singletonP(cons(X1,X0))
| ~ ssList(cons(X1,X0))
| sK4_skl(cons(X1,X0)) = X1
| ~ ssItem(X1)
| ~ ssItem(sK4_skl(cons(X1,X0)))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition]) ).
fof(f922,plain,
( sQ46_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f896,f507,f919]) ).
fof(f928,definition,
! [X0,X1,X2,X3,X4] :
( sQ47_spl
<=> ( sP1_prd(X1,X3,X4)
| hd(X1) = X2
| X1 != cons(X2,X0)
| ~ ssItem(X2)
| ~ ssItem(hd(X1))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition]) ).
fof(f931,plain,
( ~ sQ7_spl
| sQ47_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f903,f507,f928,f531]) ).
fof(f932,definition,
! [X0,X1,X2,X3,X4] :
( sQ48_spl
<=> ( sP1_prd(X3,X1,X4)
| hd(X1) = X2
| X3 != cons(X2,X0)
| ~ ssItem(X2)
| ~ ssItem(hd(X1))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition]) ).
fof(f935,plain,
( sQ48_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f904,f507,f932]) ).
fof(f942,plain,
! [X0,X1,X2,X3] :
( ~ sQ45_spl
| sP1_prd(cons(X1,X0),X2,X3)
| hd(X2) = X1
| ~ ssItem(X1)
| ~ ssList(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f916,f643]) ).
fof(f947,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ7_spl
| ~ sQ45_spl
| sP1_prd(X0,X3,X4)
| sP1_prd(X0,X1,X2)
| hd(X1) = hd(X0)
| ~ ssItem(hd(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f671,f942]) ).
fof(f948,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ45_spl
| sP1_prd(X2,X0,X4)
| sP1_prd(X2,X1,X3)
| hd(X1) = hd(X0)
| ~ ssItem(hd(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f642,f942]) ).
fof(f949,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ45_spl
| sP1_prd(X0,X1,X2)
| sP1_prd(X0,X3,X4)
| hd(X3) = sK54_skl(X0,X1,X2)
| ~ ssItem(sK54_skl(X0,X1,X2))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f448,f942]) ).
fof(f950,definition,
! [X0,X1,X2,X3,X4] :
( sQ49_spl
<=> ( sP1_prd(X0,X3,X4)
| sP1_prd(X0,X1,X2)
| hd(X1) = hd(X0)
| ~ ssItem(hd(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition]) ).
fof(f953,plain,
( ~ sQ7_spl
| ~ sQ45_spl
| sQ49_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f947,f507,f950,f915,f531]) ).
fof(f954,definition,
! [X0,X1,X2,X3,X4] :
( sQ50_spl
<=> ( sP1_prd(X2,X0,X4)
| sP1_prd(X2,X1,X3)
| hd(X1) = hd(X0)
| ~ ssItem(hd(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition]) ).
fof(f957,plain,
( ~ sQ45_spl
| sQ50_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f948,f507,f954,f915]) ).
fof(f958,definition,
! [X0,X1,X2,X3,X4] :
( sQ51_spl
<=> ( sP1_prd(X0,X1,X2)
| sP1_prd(X0,X3,X4)
| hd(X3) = sK54_skl(X0,X1,X2)
| ~ ssItem(sK54_skl(X0,X1,X2)) ) ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f961,plain,
( ~ sQ45_spl
| sQ51_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f949,f507,f958,f915]) ).
fof(f1028,plain,
! [X0,X1,X2,X3] :
( ssItem(hd(X0))
| neq(nil,X2)
| ~ neq(X2,nil)
| sP0_prd(X0,X1,X2,X3) ),
inference(resolution,[status(thm)],[f440,f643]) ).
fof(f1030,plain,
! [X0,X1,X2,X3] :
( neq(nil,X0)
| neq(nil,X2)
| ~ neq(X2,nil)
| sP0_prd(X0,X1,X2,X3) ),
inference(resolution,[status(thm)],[f440,f450]) ).
fof(f1034,plain,
( sQ17_spl
| ~ singletonP(nil)
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f116,f621]) ).
fof(f1036,plain,
( sQ17_spl
| ~ sQ18_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f1034,f507,f622,f619]) ).
fof(f1041,plain,
! [X0,X1,X2] :
( ~ sQ7_spl
| sP1_prd(X0,X1,X2)
| tl(X0) = nil
| ~ ssItem(hd(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f671,f243]) ).
fof(f1042,plain,
! [X0,X1,X2] :
( sP1_prd(X1,X0,X2)
| tl(X1) = nil
| ~ ssItem(hd(X0))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f642,f243]) ).
fof(f1043,plain,
! [X0,X1,X2] :
( sP1_prd(X0,X1,X2)
| tl(X0) = nil
| ~ ssItem(sK54_skl(X0,X1,X2))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f448,f243]) ).
fof(f1044,definition,
! [X0,X1,X2] :
( sQ52_spl
<=> ( sP1_prd(X0,X1,X2)
| tl(X0) = nil
| ~ ssItem(hd(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition]) ).
fof(f1047,plain,
( ~ sQ7_spl
| sQ52_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f1041,f507,f1044,f531]) ).
fof(f1048,definition,
! [X0,X1,X2] :
( sQ53_spl
<=> ( sP1_prd(X1,X0,X2)
| tl(X1) = nil
| ~ ssItem(hd(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition]) ).
fof(f1051,plain,
( sQ53_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f1042,f507,f1048]) ).
fof(f1052,definition,
! [X0,X1,X2] :
( sQ54_spl
<=> ( sP1_prd(X0,X1,X2)
| tl(X0) = nil
| ~ ssItem(sK54_skl(X0,X1,X2)) ) ),
introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition]) ).
fof(f1055,plain,
( sQ54_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f1043,f507,f1052]) ).
fof(f1073,plain,
( ~ ssItem(sK44_skl(nil))
| ~ ssList(sK43_skl(nil))
| nil = nil
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f233,f235]) ).
fof(f1077,plain,
! [X0,X1,X2] :
( sP1_prd(sK44_skl(X0),X1,X2)
| cons(cons(hd(X1),nil),sK43_skl(X0)) = X0
| nil = X0
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f642,f233]) ).
fof(f1078,plain,
! [X0,X1,X2] :
( sP1_prd(sK43_skl(X0),X1,X2)
| cons(sK44_skl(X0),cons(hd(X1),nil)) = X0
| nil = X0
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f642,f233]) ).
fof(f1081,definition,
( sQ55_spl
<=> ssList(sK43_skl(nil)) ),
introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition]) ).
fof(f1083,plain,
( sQ55_spl
| ~ ssList(sK43_skl(nil)) ),
inference(component_clause,[status(thm)],[f1081]) ).
fof(f1084,definition,
( sQ56_spl
<=> ssItem(sK44_skl(nil)) ),
introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition]) ).
fof(f1086,plain,
( sQ56_spl
| ~ ssItem(sK44_skl(nil)) ),
inference(component_clause,[status(thm)],[f1084]) ).
fof(f1087,plain,
( ~ sQ56_spl
| ~ sQ55_spl
| sQ32_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f1073,f507,f775,f1081,f1084]) ).
fof(f1101,definition,
! [X0] :
( sQ57_spl
<=> ( neq(nil,X0)
| ~ neq(X0,nil) ) ),
introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition]) ).
fof(f1102,plain,
! [X0] :
( ~ sQ57_spl
| neq(nil,X0)
| ~ neq(X0,nil) ),
inference(component_clause,[status(thm)],[f1101]) ).
fof(f1108,plain,
( ~ sQ57_spl
| ~ ssList(nil)
| ~ neq(nil,nil) ),
inference(resolution,[status(thm)],[f1102,f478]) ).
fof(f1110,definition,
( sQ59_spl
<=> neq(nil,nil) ),
introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition]) ).
fof(f1113,plain,
( ~ sQ57_spl
| ~ sQ4_spl
| ~ sQ59_spl ),
inference(split_clause,[status(thm)],[f1108,f1110,f507,f1101]) ).
fof(f1128,plain,
! [X0,X1,X2,X3] :
( sP1_prd(X2,X1,X3)
| ssItem(hd(X1))
| neq(nil,X0)
| ~ neq(X0,nil) ),
inference(resolution,[status(thm)],[f1028,f433]) ).
fof(f1130,definition,
! [X0] :
( sQ61_spl
<=> ( ~ neq(nil,X0)
| ~ ssItem(hd(X0))
| ~ ssList(cons(hd(X0),nil))
| neq(nil,X0)
| ~ neq(X0,nil) ) ),
introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition]) ).
fof(f1137,definition,
! [X1,X2,X3] :
( sQ63_spl
<=> ( sP1_prd(X2,X1,X3)
| ssItem(hd(X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition]) ).
fof(f1140,plain,
( sQ63_spl
| sQ57_spl ),
inference(split_clause,[status(thm)],[f1128,f1101,f1137]) ).
fof(f1141,definition,
! [X0] :
( sQ64_spl
<=> ( neq(X0,nil)
| neq(nil,X0)
| ~ neq(X0,nil) ) ),
introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition]) ).
fof(f1145,plain,
! [X0,X1] :
( ~ sQ45_spl
| hd(X0) = hd(X0)
| ~ ssItem(hd(X0))
| ~ ssList(nil)
| ~ neq(nil,X0)
| ~ ssItem(hd(X0))
| X1 = cons(hd(X0),nil)
| ~ ssList(cons(hd(X0),nil)) ),
inference(resolution,[status(thm)],[f493,f942]) ).
fof(f1147,plain,
( ~ sQ0_spl
| ~ neq(nil,sK48_skl)
| ~ ssItem(hd(sK48_skl))
| sK47_skl = cons(hd(sK48_skl),nil)
| ~ ssList(cons(hd(sK48_skl),nil)) ),
inference(resolution,[status(thm)],[f493,f540]) ).
fof(f1166,definition,
! [X0,X1] :
( sQ65_spl
<=> ( hd(X0) = hd(X0)
| ~ ssItem(hd(X0))
| ~ neq(nil,X0)
| ~ ssItem(hd(X0))
| X1 = cons(hd(X0),nil)
| ~ ssList(cons(hd(X0),nil)) ) ),
introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition]) ).
fof(f1169,plain,
( ~ sQ45_spl
| ~ sQ4_spl
| sQ65_spl ),
inference(split_clause,[status(thm)],[f1145,f1166,f507,f915]) ).
fof(f1174,definition,
( sQ67_spl
<=> ssList(cons(hd(sK48_skl),nil)) ),
introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition]) ).
fof(f1176,plain,
( sQ67_spl
| ~ ssList(cons(hd(sK48_skl),nil)) ),
inference(component_clause,[status(thm)],[f1174]) ).
fof(f1177,definition,
( sQ68_spl
<=> sK47_skl = cons(hd(sK48_skl),nil) ),
introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition]) ).
fof(f1178,plain,
( ~ sQ68_spl
| sK47_skl = cons(hd(sK48_skl),nil) ),
inference(component_clause,[status(thm)],[f1177]) ).
fof(f1180,definition,
( sQ69_spl
<=> ssItem(hd(sK48_skl)) ),
introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition]) ).
fof(f1182,plain,
( sQ69_spl
| ~ ssItem(hd(sK48_skl)) ),
inference(component_clause,[status(thm)],[f1180]) ).
fof(f1183,definition,
( sQ70_spl
<=> neq(nil,sK48_skl) ),
introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition]) ).
fof(f1185,plain,
( sQ70_spl
| ~ neq(nil,sK48_skl) ),
inference(component_clause,[status(thm)],[f1183]) ).
fof(f1186,plain,
( ~ sQ0_spl
| ~ sQ70_spl
| ~ sQ69_spl
| sQ68_spl
| ~ sQ67_spl ),
inference(split_clause,[status(thm)],[f1147,f1174,f1177,f1180,f1183,f451]) ).
fof(f1193,plain,
( sQ2_spl
| ~ neq(sK48_skl,nil) ),
inference(forward_demodulation,[status(thm)],[f423,f460]) ).
fof(f1203,plain,
( sQ2_spl
| ~ sQ1_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1193,f455]) ).
fof(f1204,plain,
( sQ2_spl
| ~ sQ1_spl ),
inference(contradiction_clause,[status(thm)],[f1203]) ).
fof(f1205,plain,
( ~ sQ0_spl
| sQ1_spl ),
inference(split_clause,[status(thm)],[f541,f454,f451]) ).
fof(f1207,plain,
( sQ70_spl
| nil = sK48_skl
| ~ ssList(sK48_skl)
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f1185,f220]) ).
fof(f1209,definition,
( sQ71_spl
<=> ssList(sK48_skl) ),
introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition]) ).
fof(f1211,plain,
( sQ71_spl
| ~ ssList(sK48_skl) ),
inference(component_clause,[status(thm)],[f1209]) ).
fof(f1212,definition,
( sQ72_spl
<=> nil = sK48_skl ),
introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition]) ).
fof(f1213,plain,
( ~ sQ72_spl
| nil = sK48_skl ),
inference(component_clause,[status(thm)],[f1212]) ).
fof(f1215,plain,
( sQ70_spl
| sQ72_spl
| ~ sQ71_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f1207,f507,f1209,f1212,f1183]) ).
fof(f1220,plain,
( sQ71_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1211,f420]) ).
fof(f1221,plain,
sQ71_spl,
inference(contradiction_clause,[status(thm)],[f1220]) ).
fof(f1243,plain,
! [X0,X1,X2,X3] :
( neq(nil,X0)
| neq(nil,X2)
| ~ neq(X2,nil)
| sP0_prd(X0,X1,X2,X3) ),
inference(resolution,[status(thm)],[f440,f450]) ).
fof(f1254,plain,
! [X0,X1,X2,X3] :
( sP1_prd(X2,X1,X3)
| neq(nil,X1)
| neq(nil,X0)
| ~ neq(X0,nil) ),
inference(resolution,[status(thm)],[f1030,f433]) ).
fof(f1255,plain,
! [X0,X1] :
( neq(X0,nil)
| neq(nil,X1)
| neq(nil,X0)
| ~ neq(X0,nil) ),
inference(resolution,[status(thm)],[f1030,f432]) ).
fof(f1256,definition,
! [X1,X2,X3] :
( sQ74_spl
<=> ( sP1_prd(X2,X1,X3)
| neq(nil,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition]) ).
fof(f1259,plain,
( sQ74_spl
| sQ57_spl ),
inference(split_clause,[status(thm)],[f1254,f1101,f1256]) ).
fof(f1260,definition,
! [X1] :
( sQ75_spl
<=> neq(nil,X1) ),
introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition]) ).
fof(f1261,plain,
! [X0] :
( ~ sQ75_spl
| neq(nil,X0) ),
inference(component_clause,[status(thm)],[f1260]) ).
fof(f1263,plain,
( sQ75_spl
| sQ64_spl ),
inference(split_clause,[status(thm)],[f1255,f1141,f1260]) ).
fof(f1264,plain,
( ~ sQ75_spl
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f1261,f478]) ).
fof(f1266,plain,
( ~ sQ75_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f1264,f507,f1260]) ).
fof(f1291,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ sQ7_spl
| sP1_prd(X1,X4,X5)
| ~ leq(X2,hd(X1))
| ~ leq(hd(X1),X2)
| ~ ssList(X3)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssItem(X2)
| ~ ssItem(hd(X1))
| ~ cyclefreeP(app(app(X0,X1),cons(X2,X3)))
| ~ ssList(app(app(X0,cons(hd(X1),nil)),cons(X2,X3))) ),
inference(paramodulation,[status(thm)],[f671,f469]) ).
fof(f1292,plain,
! [X0,X1,X2,X3,X4,X5] :
( sP1_prd(X4,X1,X5)
| ~ leq(X2,hd(X1))
| ~ leq(hd(X1),X2)
| ~ ssList(X3)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssItem(X2)
| ~ ssItem(hd(X1))
| ~ cyclefreeP(app(app(X0,X4),cons(X2,X3)))
| ~ ssList(app(app(X0,cons(hd(X1),nil)),cons(X2,X3))) ),
inference(paramodulation,[status(thm)],[f642,f469]) ).
fof(f1293,plain,
! [X0,X1,X2,X3,X4,X5] :
( sP1_prd(X1,X2,X3)
| ~ leq(X4,sK54_skl(X1,X2,X3))
| ~ leq(sK54_skl(X1,X2,X3),X4)
| ~ ssList(X5)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssItem(X4)
| ~ ssItem(sK54_skl(X1,X2,X3))
| ~ cyclefreeP(app(app(X0,X1),cons(X4,X5)))
| ~ ssList(app(app(X0,cons(sK54_skl(X1,X2,X3),nil)),cons(X4,X5))) ),
inference(paramodulation,[status(thm)],[f448,f469]) ).
fof(f1295,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ sQ7_spl
| sP1_prd(X3,X4,X5)
| ~ leq(hd(X3),X1)
| ~ leq(X1,hd(X3))
| ~ ssList(nil)
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssItem(hd(X3))
| ~ ssItem(X1)
| ~ cyclefreeP(app(app(X0,cons(X1,X2)),X3))
| ~ ssList(app(app(X0,cons(X1,X2)),cons(hd(X3),nil))) ),
inference(paramodulation,[status(thm)],[f671,f469]) ).
fof(f1296,plain,
! [X0,X1,X2,X3,X4,X5] :
( sP1_prd(X4,X3,X5)
| ~ leq(hd(X3),X1)
| ~ leq(X1,hd(X3))
| ~ ssList(nil)
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssItem(hd(X3))
| ~ ssItem(X1)
| ~ cyclefreeP(app(app(X0,cons(X1,X2)),X4))
| ~ ssList(app(app(X0,cons(X1,X2)),cons(hd(X3),nil))) ),
inference(paramodulation,[status(thm)],[f642,f469]) ).
fof(f1297,plain,
! [X0,X1,X2,X3,X4,X5] :
( sP1_prd(X3,X4,X5)
| ~ leq(sK54_skl(X3,X4,X5),X1)
| ~ leq(X1,sK54_skl(X3,X4,X5))
| ~ ssList(nil)
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssItem(sK54_skl(X3,X4,X5))
| ~ ssItem(X1)
| ~ cyclefreeP(app(app(X0,cons(X1,X2)),X3))
| ~ ssList(app(app(X0,cons(X1,X2)),cons(sK54_skl(X3,X4,X5),nil))) ),
inference(paramodulation,[status(thm)],[f448,f469]) ).
fof(f1299,definition,
! [X0,X1,X2,X3,X4,X5] :
( sQ76_spl
<=> ( sP1_prd(X1,X4,X5)
| ~ leq(X2,hd(X1))
| ~ leq(hd(X1),X2)
| ~ ssList(X3)
| ~ ssList(X0)
| ~ ssItem(X2)
| ~ ssItem(hd(X1))
| ~ cyclefreeP(app(app(X0,X1),cons(X2,X3)))
| ~ ssList(app(app(X0,cons(hd(X1),nil)),cons(X2,X3))) ) ),
introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition]) ).
fof(f1302,plain,
( ~ sQ7_spl
| ~ sQ4_spl
| sQ76_spl ),
inference(split_clause,[status(thm)],[f1291,f1299,f507,f531]) ).
fof(f1303,definition,
! [X0,X1,X2,X3,X4,X5] :
( sQ77_spl
<=> ( sP1_prd(X4,X1,X5)
| ~ leq(X2,hd(X1))
| ~ leq(hd(X1),X2)
| ~ ssList(X3)
| ~ ssList(X0)
| ~ ssItem(X2)
| ~ ssItem(hd(X1))
| ~ cyclefreeP(app(app(X0,X4),cons(X2,X3)))
| ~ ssList(app(app(X0,cons(hd(X1),nil)),cons(X2,X3))) ) ),
introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition]) ).
fof(f1306,plain,
( ~ sQ4_spl
| sQ77_spl ),
inference(split_clause,[status(thm)],[f1292,f1303,f507]) ).
fof(f1307,definition,
! [X0,X1,X2,X3,X4,X5] :
( sQ78_spl
<=> ( sP1_prd(X1,X2,X3)
| ~ leq(X4,sK54_skl(X1,X2,X3))
| ~ leq(sK54_skl(X1,X2,X3),X4)
| ~ ssList(X5)
| ~ ssList(X0)
| ~ ssItem(X4)
| ~ ssItem(sK54_skl(X1,X2,X3))
| ~ cyclefreeP(app(app(X0,X1),cons(X4,X5)))
| ~ ssList(app(app(X0,cons(sK54_skl(X1,X2,X3),nil)),cons(X4,X5))) ) ),
introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition]) ).
fof(f1310,plain,
( ~ sQ4_spl
| sQ78_spl ),
inference(split_clause,[status(thm)],[f1293,f1307,f507]) ).
fof(f1311,definition,
! [X0,X1,X2,X3,X4,X5] :
( sQ79_spl
<=> ( sP1_prd(X3,X4,X5)
| ~ leq(hd(X3),X1)
| ~ leq(X1,hd(X3))
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssItem(hd(X3))
| ~ ssItem(X1)
| ~ cyclefreeP(app(app(X0,cons(X1,X2)),X3))
| ~ ssList(app(app(X0,cons(X1,X2)),cons(hd(X3),nil))) ) ),
introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition]) ).
fof(f1314,plain,
( ~ sQ7_spl
| ~ sQ4_spl
| sQ79_spl ),
inference(split_clause,[status(thm)],[f1295,f1311,f507,f531]) ).
fof(f1315,definition,
! [X0,X1,X2,X3,X4,X5] :
( sQ80_spl
<=> ( sP1_prd(X4,X3,X5)
| ~ leq(hd(X3),X1)
| ~ leq(X1,hd(X3))
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssItem(hd(X3))
| ~ ssItem(X1)
| ~ cyclefreeP(app(app(X0,cons(X1,X2)),X4))
| ~ ssList(app(app(X0,cons(X1,X2)),cons(hd(X3),nil))) ) ),
introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition]) ).
fof(f1318,plain,
( ~ sQ4_spl
| sQ80_spl ),
inference(split_clause,[status(thm)],[f1296,f1315,f507]) ).
fof(f1319,definition,
! [X0,X1,X2,X3,X4,X5] :
( sQ81_spl
<=> ( sP1_prd(X3,X4,X5)
| ~ leq(sK54_skl(X3,X4,X5),X1)
| ~ leq(X1,sK54_skl(X3,X4,X5))
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssItem(sK54_skl(X3,X4,X5))
| ~ ssItem(X1)
| ~ cyclefreeP(app(app(X0,cons(X1,X2)),X3))
| ~ ssList(app(app(X0,cons(X1,X2)),cons(sK54_skl(X3,X4,X5),nil))) ) ),
introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition]) ).
fof(f1322,plain,
( ~ sQ4_spl
| sQ81_spl ),
inference(split_clause,[status(thm)],[f1297,f1319,f507]) ).
fof(f1391,plain,
( sQ55_spl
| nil = nil
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f1083,f231]) ).
fof(f1392,plain,
( sQ55_spl
| sQ32_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f1391,f507,f775,f1081]) ).
fof(f1416,plain,
( sQ56_spl
| nil = nil
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f1086,f232]) ).
fof(f1417,plain,
( sQ56_spl
| sQ32_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f1416,f507,f775,f1084]) ).
fof(f1421,plain,
( ~ sQ1_spl
| ~ sQ72_spl
| neq(nil,nil) ),
inference(backward_demodulation,[status(thm)],[f1213,f455]) ).
fof(f1425,plain,
( ~ sQ1_spl
| ~ sQ72_spl
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f1421,f478]) ).
fof(f1427,plain,
( ~ sQ1_spl
| ~ sQ72_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f1425,f507,f1212,f454]) ).
fof(f1428,plain,
! [X0,X1] :
( neq(nil,X1)
| neq(nil,X0)
| ~ neq(X0,nil)
| ~ neq(nil,X0)
| ~ ssItem(hd(X0))
| ~ ssList(cons(hd(X0),nil)) ),
inference(resolution,[status(thm)],[f492,f1243]) ).
fof(f1435,plain,
( sQ75_spl
| sQ61_spl ),
inference(split_clause,[status(thm)],[f1428,f1130,f1260]) ).
fof(f1515,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ sQ7_spl
| sP1_prd(X1,X4,X5)
| leq(X2,hd(X1))
| leq(hd(X1),X2)
| ~ ssList(X3)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssItem(X2)
| ~ ssItem(hd(X1))
| ~ totalorderP(app(app(X0,X1),cons(X2,X3)))
| ~ ssList(app(app(X0,cons(hd(X1),nil)),cons(X2,X3))) ),
inference(paramodulation,[status(thm)],[f671,f470]) ).
fof(f1516,plain,
! [X0,X1,X2,X3,X4,X5] :
( sP1_prd(X4,X1,X5)
| leq(X2,hd(X1))
| leq(hd(X1),X2)
| ~ ssList(X3)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssItem(X2)
| ~ ssItem(hd(X1))
| ~ totalorderP(app(app(X0,X4),cons(X2,X3)))
| ~ ssList(app(app(X0,cons(hd(X1),nil)),cons(X2,X3))) ),
inference(paramodulation,[status(thm)],[f642,f470]) ).
fof(f1517,plain,
! [X0,X1,X2,X3,X4,X5] :
( sP1_prd(X1,X2,X3)
| leq(X4,sK54_skl(X1,X2,X3))
| leq(sK54_skl(X1,X2,X3),X4)
| ~ ssList(X5)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssItem(X4)
| ~ ssItem(sK54_skl(X1,X2,X3))
| ~ totalorderP(app(app(X0,X1),cons(X4,X5)))
| ~ ssList(app(app(X0,cons(sK54_skl(X1,X2,X3),nil)),cons(X4,X5))) ),
inference(paramodulation,[status(thm)],[f448,f470]) ).
fof(f1519,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ sQ7_spl
| sP1_prd(X3,X4,X5)
| leq(hd(X3),X1)
| leq(X1,hd(X3))
| ~ ssList(nil)
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssItem(hd(X3))
| ~ ssItem(X1)
| ~ totalorderP(app(app(X0,cons(X1,X2)),X3))
| ~ ssList(app(app(X0,cons(X1,X2)),cons(hd(X3),nil))) ),
inference(paramodulation,[status(thm)],[f671,f470]) ).
fof(f1520,plain,
! [X0,X1,X2,X3,X4,X5] :
( sP1_prd(X4,X3,X5)
| leq(hd(X3),X1)
| leq(X1,hd(X3))
| ~ ssList(nil)
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssItem(hd(X3))
| ~ ssItem(X1)
| ~ totalorderP(app(app(X0,cons(X1,X2)),X4))
| ~ ssList(app(app(X0,cons(X1,X2)),cons(hd(X3),nil))) ),
inference(paramodulation,[status(thm)],[f642,f470]) ).
fof(f1521,plain,
! [X0,X1,X2,X3,X4,X5] :
( sP1_prd(X3,X4,X5)
| leq(sK54_skl(X3,X4,X5),X1)
| leq(X1,sK54_skl(X3,X4,X5))
| ~ ssList(nil)
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssItem(sK54_skl(X3,X4,X5))
| ~ ssItem(X1)
| ~ totalorderP(app(app(X0,cons(X1,X2)),X3))
| ~ ssList(app(app(X0,cons(X1,X2)),cons(sK54_skl(X3,X4,X5),nil))) ),
inference(paramodulation,[status(thm)],[f448,f470]) ).
fof(f1523,definition,
! [X0,X1,X2,X3,X4,X5] :
( sQ86_spl
<=> ( sP1_prd(X1,X4,X5)
| leq(X2,hd(X1))
| leq(hd(X1),X2)
| ~ ssList(X3)
| ~ ssList(X0)
| ~ ssItem(X2)
| ~ ssItem(hd(X1))
| ~ totalorderP(app(app(X0,X1),cons(X2,X3)))
| ~ ssList(app(app(X0,cons(hd(X1),nil)),cons(X2,X3))) ) ),
introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition]) ).
fof(f1526,plain,
( ~ sQ7_spl
| ~ sQ4_spl
| sQ86_spl ),
inference(split_clause,[status(thm)],[f1515,f1523,f507,f531]) ).
fof(f1527,definition,
! [X0,X1,X2,X3,X4,X5] :
( sQ87_spl
<=> ( sP1_prd(X4,X1,X5)
| leq(X2,hd(X1))
| leq(hd(X1),X2)
| ~ ssList(X3)
| ~ ssList(X0)
| ~ ssItem(X2)
| ~ ssItem(hd(X1))
| ~ totalorderP(app(app(X0,X4),cons(X2,X3)))
| ~ ssList(app(app(X0,cons(hd(X1),nil)),cons(X2,X3))) ) ),
introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition]) ).
fof(f1530,plain,
( ~ sQ4_spl
| sQ87_spl ),
inference(split_clause,[status(thm)],[f1516,f1527,f507]) ).
fof(f1531,definition,
! [X0,X1,X2,X3,X4,X5] :
( sQ88_spl
<=> ( sP1_prd(X1,X2,X3)
| leq(X4,sK54_skl(X1,X2,X3))
| leq(sK54_skl(X1,X2,X3),X4)
| ~ ssList(X5)
| ~ ssList(X0)
| ~ ssItem(X4)
| ~ ssItem(sK54_skl(X1,X2,X3))
| ~ totalorderP(app(app(X0,X1),cons(X4,X5)))
| ~ ssList(app(app(X0,cons(sK54_skl(X1,X2,X3),nil)),cons(X4,X5))) ) ),
introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition]) ).
fof(f1534,plain,
( ~ sQ4_spl
| sQ88_spl ),
inference(split_clause,[status(thm)],[f1517,f1531,f507]) ).
fof(f1535,definition,
! [X0,X1,X2,X3,X4,X5] :
( sQ89_spl
<=> ( sP1_prd(X3,X4,X5)
| leq(hd(X3),X1)
| leq(X1,hd(X3))
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssItem(hd(X3))
| ~ ssItem(X1)
| ~ totalorderP(app(app(X0,cons(X1,X2)),X3))
| ~ ssList(app(app(X0,cons(X1,X2)),cons(hd(X3),nil))) ) ),
introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition]) ).
fof(f1538,plain,
( ~ sQ7_spl
| ~ sQ4_spl
| sQ89_spl ),
inference(split_clause,[status(thm)],[f1519,f1535,f507,f531]) ).
fof(f1539,definition,
! [X0,X1,X2,X3,X4,X5] :
( sQ90_spl
<=> ( sP1_prd(X4,X3,X5)
| leq(hd(X3),X1)
| leq(X1,hd(X3))
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssItem(hd(X3))
| ~ ssItem(X1)
| ~ totalorderP(app(app(X0,cons(X1,X2)),X4))
| ~ ssList(app(app(X0,cons(X1,X2)),cons(hd(X3),nil))) ) ),
introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition]) ).
fof(f1542,plain,
( ~ sQ4_spl
| sQ90_spl ),
inference(split_clause,[status(thm)],[f1520,f1539,f507]) ).
fof(f1543,definition,
! [X0,X1,X2,X3,X4,X5] :
( sQ91_spl
<=> ( sP1_prd(X3,X4,X5)
| leq(sK54_skl(X3,X4,X5),X1)
| leq(X1,sK54_skl(X3,X4,X5))
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssItem(sK54_skl(X3,X4,X5))
| ~ ssItem(X1)
| ~ totalorderP(app(app(X0,cons(X1,X2)),X3))
| ~ ssList(app(app(X0,cons(X1,X2)),cons(sK54_skl(X3,X4,X5),nil))) ) ),
introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition]) ).
fof(f1546,plain,
( ~ sQ4_spl
| sQ91_spl ),
inference(split_clause,[status(thm)],[f1521,f1543,f507]) ).
fof(f1621,plain,
! [X0,X1] :
( ~ sQ68_spl
| ~ neq(nil,sK48_skl)
| ~ ssItem(hd(sK48_skl))
| ~ ssList(cons(hd(sK48_skl),nil))
| ~ sP0_prd(X0,X1,sK48_skl,sK47_skl) ),
inference(paramodulation,[status(thm)],[f1178,f492]) ).
fof(f1622,plain,
! [X0,X1] :
( ~ sQ68_spl
| sP1_prd(sK43_skl(X0),sK48_skl,X1)
| cons(sK44_skl(X0),sK47_skl) = X0
| nil = X0
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f1178,f1078]) ).
fof(f1623,plain,
! [X0,X1] :
( ~ sQ68_spl
| sP1_prd(sK44_skl(X0),sK48_skl,X1)
| cons(sK47_skl,sK43_skl(X0)) = X0
| nil = X0
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f1178,f1077]) ).
fof(f1627,plain,
( ~ sQ68_spl
| ~ ssItem(hd(sK48_skl))
| singletonP(sK47_skl)
| ~ ssList(cons(hd(sK48_skl),nil)) ),
inference(paramodulation,[status(thm)],[f1178,f465]) ).
fof(f1628,plain,
! [X0,X1,X2] :
( ~ sQ68_spl
| leq(hd(sK48_skl),X1)
| leq(X1,hd(sK48_skl))
| ~ ssList(nil)
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssItem(hd(sK48_skl))
| ~ ssItem(X1)
| ~ totalorderP(app(app(X0,cons(X1,X2)),sK47_skl))
| ~ ssList(app(app(X0,cons(X1,X2)),cons(hd(sK48_skl),nil))) ),
inference(paramodulation,[status(thm)],[f1178,f470]) ).
fof(f1629,plain,
! [X0,X1,X2] :
( ~ sQ68_spl
| leq(X1,hd(sK48_skl))
| leq(hd(sK48_skl),X1)
| ~ ssList(X2)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssItem(X1)
| ~ ssItem(hd(sK48_skl))
| ~ totalorderP(app(app(X0,sK47_skl),cons(X1,X2)))
| ~ ssList(app(app(X0,cons(hd(sK48_skl),nil)),cons(X1,X2))) ),
inference(paramodulation,[status(thm)],[f1178,f470]) ).
fof(f1630,plain,
! [X0,X1,X2] :
( ~ sQ68_spl
| ~ leq(hd(sK48_skl),X1)
| ~ leq(X1,hd(sK48_skl))
| ~ ssList(nil)
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssItem(hd(sK48_skl))
| ~ ssItem(X1)
| ~ cyclefreeP(app(app(X0,cons(X1,X2)),sK47_skl))
| ~ ssList(app(app(X0,cons(X1,X2)),cons(hd(sK48_skl),nil))) ),
inference(paramodulation,[status(thm)],[f1178,f469]) ).
fof(f1631,plain,
! [X0,X1,X2] :
( ~ sQ68_spl
| ~ leq(X1,hd(sK48_skl))
| ~ leq(hd(sK48_skl),X1)
| ~ ssList(X2)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssItem(X1)
| ~ ssItem(hd(sK48_skl))
| ~ cyclefreeP(app(app(X0,sK47_skl),cons(X1,X2)))
| ~ ssList(app(app(X0,cons(hd(sK48_skl),nil)),cons(X1,X2))) ),
inference(paramodulation,[status(thm)],[f1178,f469]) ).
fof(f1632,plain,
( ~ sQ68_spl
| tl(sK47_skl) = nil
| ~ ssItem(hd(sK48_skl))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f1178,f243]) ).
fof(f1633,plain,
! [X0,X1] :
( ~ sQ68_spl
| ~ sQ45_spl
| sP1_prd(sK47_skl,X0,X1)
| hd(X0) = hd(sK48_skl)
| ~ ssItem(hd(sK48_skl))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f1178,f942]) ).
fof(f1634,plain,
! [X0,X1] :
( ~ sQ68_spl
| X1 = hd(sK48_skl)
| cons(X1,X0) != sK47_skl
| ~ ssItem(hd(sK48_skl))
| ~ ssItem(X1)
| ~ ssList(nil)
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f1178,f227]) ).
fof(f1636,plain,
! [X0,X1] :
( ~ sQ68_spl
| nil = X0
| cons(X1,X0) != sK47_skl
| ~ ssItem(hd(sK48_skl))
| ~ ssItem(X1)
| ~ ssList(nil)
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f1178,f228]) ).
fof(f1639,plain,
( ~ sQ68_spl
| hd(sK47_skl) = hd(sK48_skl)
| ~ ssItem(hd(sK48_skl))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f1178,f239]) ).
fof(f1640,plain,
( ~ sQ68_spl
| ssList(sK47_skl)
| ~ ssItem(hd(sK48_skl))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f1178,f222]) ).
fof(f1641,plain,
( ~ sQ68_spl
| nil != sK47_skl
| ~ ssItem(hd(sK48_skl))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f1178,f235]) ).
fof(f1643,plain,
! [X0] :
( ~ sQ68_spl
| ~ ssList(nil)
| ~ ssList(X0)
| memberP(app(X0,sK47_skl),hd(sK48_skl))
| ~ ssItem(hd(sK48_skl))
| ~ ssList(app(X0,cons(hd(sK48_skl),nil))) ),
inference(paramodulation,[status(thm)],[f1178,f464]) ).
fof(f1663,definition,
! [X0,X1] :
( sQ97_spl
<=> ~ sP0_prd(X0,X1,sK48_skl,sK47_skl) ),
introduced(definition,[new_symbols(definition,[sQ97_spl])],[split_symbol_definition]) ).
fof(f1664,plain,
! [X0,X1] :
( ~ sQ97_spl
| ~ sP0_prd(X0,X1,sK48_skl,sK47_skl) ),
inference(component_clause,[status(thm)],[f1663]) ).
fof(f1666,plain,
( ~ sQ68_spl
| ~ sQ70_spl
| ~ sQ69_spl
| ~ sQ67_spl
| sQ97_spl ),
inference(split_clause,[status(thm)],[f1621,f1663,f1174,f1180,f1183,f1177]) ).
fof(f1672,definition,
( sQ99_spl
<=> singletonP(sK47_skl) ),
introduced(definition,[new_symbols(definition,[sQ99_spl])],[split_symbol_definition]) ).
fof(f1675,plain,
( ~ sQ68_spl
| ~ sQ69_spl
| sQ99_spl
| ~ sQ67_spl ),
inference(split_clause,[status(thm)],[f1627,f1174,f1672,f1180,f1177]) ).
fof(f1676,definition,
! [X0,X1,X2] :
( sQ100_spl
<=> ( leq(hd(sK48_skl),X1)
| leq(X1,hd(sK48_skl))
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssItem(X1)
| ~ totalorderP(app(app(X0,cons(X1,X2)),sK47_skl))
| ~ ssList(app(app(X0,cons(X1,X2)),cons(hd(sK48_skl),nil))) ) ),
introduced(definition,[new_symbols(definition,[sQ100_spl])],[split_symbol_definition]) ).
fof(f1679,plain,
( ~ sQ68_spl
| ~ sQ4_spl
| ~ sQ69_spl
| sQ100_spl ),
inference(split_clause,[status(thm)],[f1628,f1676,f1180,f507,f1177]) ).
fof(f1680,definition,
! [X0,X1,X2] :
( sQ101_spl
<=> ( leq(X1,hd(sK48_skl))
| leq(hd(sK48_skl),X1)
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssItem(X1)
| ~ totalorderP(app(app(X0,sK47_skl),cons(X1,X2)))
| ~ ssList(app(app(X0,cons(hd(sK48_skl),nil)),cons(X1,X2))) ) ),
introduced(definition,[new_symbols(definition,[sQ101_spl])],[split_symbol_definition]) ).
fof(f1683,plain,
( ~ sQ68_spl
| ~ sQ4_spl
| ~ sQ69_spl
| sQ101_spl ),
inference(split_clause,[status(thm)],[f1629,f1680,f1180,f507,f1177]) ).
fof(f1684,definition,
! [X0,X1,X2] :
( sQ102_spl
<=> ( ~ leq(hd(sK48_skl),X1)
| ~ leq(X1,hd(sK48_skl))
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssItem(X1)
| ~ cyclefreeP(app(app(X0,cons(X1,X2)),sK47_skl))
| ~ ssList(app(app(X0,cons(X1,X2)),cons(hd(sK48_skl),nil))) ) ),
introduced(definition,[new_symbols(definition,[sQ102_spl])],[split_symbol_definition]) ).
fof(f1687,plain,
( ~ sQ68_spl
| ~ sQ4_spl
| ~ sQ69_spl
| sQ102_spl ),
inference(split_clause,[status(thm)],[f1630,f1684,f1180,f507,f1177]) ).
fof(f1688,definition,
! [X0,X1,X2] :
( sQ103_spl
<=> ( ~ leq(X1,hd(sK48_skl))
| ~ leq(hd(sK48_skl),X1)
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssItem(X1)
| ~ cyclefreeP(app(app(X0,sK47_skl),cons(X1,X2)))
| ~ ssList(app(app(X0,cons(hd(sK48_skl),nil)),cons(X1,X2))) ) ),
introduced(definition,[new_symbols(definition,[sQ103_spl])],[split_symbol_definition]) ).
fof(f1691,plain,
( ~ sQ68_spl
| ~ sQ4_spl
| ~ sQ69_spl
| sQ103_spl ),
inference(split_clause,[status(thm)],[f1631,f1688,f1180,f507,f1177]) ).
fof(f1692,definition,
( sQ104_spl
<=> tl(sK47_skl) = nil ),
introduced(definition,[new_symbols(definition,[sQ104_spl])],[split_symbol_definition]) ).
fof(f1695,plain,
( ~ sQ68_spl
| sQ104_spl
| ~ sQ69_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f1632,f507,f1180,f1692,f1177]) ).
fof(f1696,definition,
! [X0,X1] :
( sQ105_spl
<=> ( sP1_prd(sK47_skl,X0,X1)
| hd(X0) = hd(sK48_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ105_spl])],[split_symbol_definition]) ).
fof(f1699,plain,
( ~ sQ68_spl
| ~ sQ45_spl
| sQ105_spl
| ~ sQ69_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f1633,f507,f1180,f1696,f915,f1177]) ).
fof(f1700,definition,
! [X0,X1] :
( sQ106_spl
<=> ( X1 = hd(sK48_skl)
| cons(X1,X0) != sK47_skl
| ~ ssItem(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ106_spl])],[split_symbol_definition]) ).
fof(f1703,plain,
( ~ sQ68_spl
| ~ sQ69_spl
| ~ sQ4_spl
| sQ106_spl ),
inference(split_clause,[status(thm)],[f1634,f1700,f507,f1180,f1177]) ).
fof(f1705,definition,
! [X0,X1] :
( sQ107_spl
<=> ( nil = X0
| cons(X1,X0) != sK47_skl
| ~ ssItem(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ107_spl])],[split_symbol_definition]) ).
fof(f1708,plain,
( ~ sQ68_spl
| ~ sQ69_spl
| ~ sQ4_spl
| sQ107_spl ),
inference(split_clause,[status(thm)],[f1636,f1705,f507,f1180,f1177]) ).
fof(f1714,definition,
( sQ109_spl
<=> hd(sK47_skl) = hd(sK48_skl) ),
introduced(definition,[new_symbols(definition,[sQ109_spl])],[split_symbol_definition]) ).
fof(f1715,plain,
( ~ sQ109_spl
| hd(sK47_skl) = hd(sK48_skl) ),
inference(component_clause,[status(thm)],[f1714]) ).
fof(f1717,plain,
( ~ sQ68_spl
| sQ109_spl
| ~ sQ69_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f1639,f507,f1180,f1714,f1177]) ).
fof(f1718,definition,
( sQ110_spl
<=> ssList(sK47_skl) ),
introduced(definition,[new_symbols(definition,[sQ110_spl])],[split_symbol_definition]) ).
fof(f1721,plain,
( ~ sQ68_spl
| sQ110_spl
| ~ sQ69_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f1640,f507,f1180,f1718,f1177]) ).
fof(f1722,definition,
( sQ111_spl
<=> nil = sK47_skl ),
introduced(definition,[new_symbols(definition,[sQ111_spl])],[split_symbol_definition]) ).
fof(f1725,plain,
( ~ sQ68_spl
| ~ sQ111_spl
| ~ sQ69_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f1641,f507,f1180,f1722,f1177]) ).
fof(f1727,definition,
! [X0] :
( sQ112_spl
<=> ( ~ ssList(X0)
| memberP(app(X0,sK47_skl),hd(sK48_skl))
| ~ ssList(app(X0,cons(hd(sK48_skl),nil))) ) ),
introduced(definition,[new_symbols(definition,[sQ112_spl])],[split_symbol_definition]) ).
fof(f1730,plain,
( ~ sQ68_spl
| ~ sQ4_spl
| ~ sQ69_spl
| sQ112_spl ),
inference(split_clause,[status(thm)],[f1643,f1727,f1180,f507,f1177]) ).
fof(f1731,plain,
( sQ67_spl
| ~ sQ68_spl
| ~ ssList(sK47_skl) ),
inference(forward_demodulation,[status(thm)],[f1178,f1176]) ).
fof(f1732,plain,
( sQ67_spl
| ~ sQ68_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1731,f419]) ).
fof(f1733,plain,
( sQ67_spl
| ~ sQ68_spl ),
inference(contradiction_clause,[status(thm)],[f1732]) ).
fof(f1734,plain,
( sQ69_spl
| nil = sK48_skl
| ~ ssList(sK48_skl) ),
inference(resolution,[status(thm)],[f1182,f237]) ).
fof(f1735,plain,
( sQ69_spl
| sQ72_spl
| ~ sQ71_spl ),
inference(split_clause,[status(thm)],[f1734,f1209,f1212,f1180]) ).
fof(f1761,plain,
! [X0,X1,X2,X3] :
( ~ sQ68_spl
| sP1_prd(sK43_skl(X0),X1,X3)
| sP1_prd(cons(hd(X1),nil),sK48_skl,X2)
| cons(sK44_skl(X0),sK47_skl) = X0
| nil = X0
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f642,f1622]) ).
fof(f1762,plain,
! [X0,X1,X2,X3] :
( ~ sQ68_spl
| sP1_prd(sK44_skl(X0),X1,X3)
| sP1_prd(cons(hd(X1),nil),sK48_skl,X2)
| cons(sK47_skl,sK43_skl(X0)) = X0
| nil = X0
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f642,f1623]) ).
fof(f1768,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ sQ7_spl
| sP1_prd(X1,X4,X5)
| lt(X2,hd(X1))
| lt(hd(X1),X2)
| ~ ssList(X3)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssItem(X2)
| ~ ssItem(hd(X1))
| ~ strictorderP(app(app(X0,X1),cons(X2,X3)))
| ~ ssList(app(app(X0,cons(hd(X1),nil)),cons(X2,X3))) ),
inference(paramodulation,[status(thm)],[f671,f471]) ).
fof(f1769,plain,
! [X0,X1,X2,X3,X4,X5] :
( sP1_prd(X4,X1,X5)
| lt(X2,hd(X1))
| lt(hd(X1),X2)
| ~ ssList(X3)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssItem(X2)
| ~ ssItem(hd(X1))
| ~ strictorderP(app(app(X0,X4),cons(X2,X3)))
| ~ ssList(app(app(X0,cons(hd(X1),nil)),cons(X2,X3))) ),
inference(paramodulation,[status(thm)],[f642,f471]) ).
fof(f1770,plain,
! [X0,X1,X2,X3,X4,X5] :
( sP1_prd(X1,X2,X3)
| lt(X4,sK54_skl(X1,X2,X3))
| lt(sK54_skl(X1,X2,X3),X4)
| ~ ssList(X5)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssItem(X4)
| ~ ssItem(sK54_skl(X1,X2,X3))
| ~ strictorderP(app(app(X0,X1),cons(X4,X5)))
| ~ ssList(app(app(X0,cons(sK54_skl(X1,X2,X3),nil)),cons(X4,X5))) ),
inference(paramodulation,[status(thm)],[f448,f471]) ).
fof(f1772,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ sQ7_spl
| sP1_prd(X3,X4,X5)
| lt(hd(X3),X1)
| lt(X1,hd(X3))
| ~ ssList(nil)
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssItem(hd(X3))
| ~ ssItem(X1)
| ~ strictorderP(app(app(X0,cons(X1,X2)),X3))
| ~ ssList(app(app(X0,cons(X1,X2)),cons(hd(X3),nil))) ),
inference(paramodulation,[status(thm)],[f671,f471]) ).
fof(f1773,plain,
! [X0,X1,X2,X3,X4,X5] :
( sP1_prd(X4,X3,X5)
| lt(hd(X3),X1)
| lt(X1,hd(X3))
| ~ ssList(nil)
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssItem(hd(X3))
| ~ ssItem(X1)
| ~ strictorderP(app(app(X0,cons(X1,X2)),X4))
| ~ ssList(app(app(X0,cons(X1,X2)),cons(hd(X3),nil))) ),
inference(paramodulation,[status(thm)],[f642,f471]) ).
fof(f1774,plain,
! [X0,X1,X2,X3,X4,X5] :
( sP1_prd(X3,X4,X5)
| lt(sK54_skl(X3,X4,X5),X1)
| lt(X1,sK54_skl(X3,X4,X5))
| ~ ssList(nil)
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssItem(sK54_skl(X3,X4,X5))
| ~ ssItem(X1)
| ~ strictorderP(app(app(X0,cons(X1,X2)),X3))
| ~ ssList(app(app(X0,cons(X1,X2)),cons(sK54_skl(X3,X4,X5),nil))) ),
inference(paramodulation,[status(thm)],[f448,f471]) ).
fof(f1776,definition,
! [X0,X1,X2,X3,X4,X5] :
( sQ113_spl
<=> ( sP1_prd(X1,X4,X5)
| lt(X2,hd(X1))
| lt(hd(X1),X2)
| ~ ssList(X3)
| ~ ssList(X0)
| ~ ssItem(X2)
| ~ ssItem(hd(X1))
| ~ strictorderP(app(app(X0,X1),cons(X2,X3)))
| ~ ssList(app(app(X0,cons(hd(X1),nil)),cons(X2,X3))) ) ),
introduced(definition,[new_symbols(definition,[sQ113_spl])],[split_symbol_definition]) ).
fof(f1779,plain,
( ~ sQ7_spl
| ~ sQ4_spl
| sQ113_spl ),
inference(split_clause,[status(thm)],[f1768,f1776,f507,f531]) ).
fof(f1780,definition,
! [X0,X1,X2,X3,X4,X5] :
( sQ114_spl
<=> ( sP1_prd(X4,X1,X5)
| lt(X2,hd(X1))
| lt(hd(X1),X2)
| ~ ssList(X3)
| ~ ssList(X0)
| ~ ssItem(X2)
| ~ ssItem(hd(X1))
| ~ strictorderP(app(app(X0,X4),cons(X2,X3)))
| ~ ssList(app(app(X0,cons(hd(X1),nil)),cons(X2,X3))) ) ),
introduced(definition,[new_symbols(definition,[sQ114_spl])],[split_symbol_definition]) ).
fof(f1783,plain,
( ~ sQ4_spl
| sQ114_spl ),
inference(split_clause,[status(thm)],[f1769,f1780,f507]) ).
fof(f1784,definition,
! [X0,X1,X2,X3,X4,X5] :
( sQ115_spl
<=> ( sP1_prd(X1,X2,X3)
| lt(X4,sK54_skl(X1,X2,X3))
| lt(sK54_skl(X1,X2,X3),X4)
| ~ ssList(X5)
| ~ ssList(X0)
| ~ ssItem(X4)
| ~ ssItem(sK54_skl(X1,X2,X3))
| ~ strictorderP(app(app(X0,X1),cons(X4,X5)))
| ~ ssList(app(app(X0,cons(sK54_skl(X1,X2,X3),nil)),cons(X4,X5))) ) ),
introduced(definition,[new_symbols(definition,[sQ115_spl])],[split_symbol_definition]) ).
fof(f1787,plain,
( ~ sQ4_spl
| sQ115_spl ),
inference(split_clause,[status(thm)],[f1770,f1784,f507]) ).
fof(f1788,definition,
! [X0,X1,X2,X3,X4,X5] :
( sQ116_spl
<=> ( sP1_prd(X3,X4,X5)
| lt(hd(X3),X1)
| lt(X1,hd(X3))
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssItem(hd(X3))
| ~ ssItem(X1)
| ~ strictorderP(app(app(X0,cons(X1,X2)),X3))
| ~ ssList(app(app(X0,cons(X1,X2)),cons(hd(X3),nil))) ) ),
introduced(definition,[new_symbols(definition,[sQ116_spl])],[split_symbol_definition]) ).
fof(f1791,plain,
( ~ sQ7_spl
| ~ sQ4_spl
| sQ116_spl ),
inference(split_clause,[status(thm)],[f1772,f1788,f507,f531]) ).
fof(f1792,definition,
! [X0,X1,X2,X3,X4,X5] :
( sQ117_spl
<=> ( sP1_prd(X4,X3,X5)
| lt(hd(X3),X1)
| lt(X1,hd(X3))
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssItem(hd(X3))
| ~ ssItem(X1)
| ~ strictorderP(app(app(X0,cons(X1,X2)),X4))
| ~ ssList(app(app(X0,cons(X1,X2)),cons(hd(X3),nil))) ) ),
introduced(definition,[new_symbols(definition,[sQ117_spl])],[split_symbol_definition]) ).
fof(f1795,plain,
( ~ sQ4_spl
| sQ117_spl ),
inference(split_clause,[status(thm)],[f1773,f1792,f507]) ).
fof(f1796,definition,
! [X0,X1,X2,X3,X4,X5] :
( sQ118_spl
<=> ( sP1_prd(X3,X4,X5)
| lt(sK54_skl(X3,X4,X5),X1)
| lt(X1,sK54_skl(X3,X4,X5))
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssItem(sK54_skl(X3,X4,X5))
| ~ ssItem(X1)
| ~ strictorderP(app(app(X0,cons(X1,X2)),X3))
| ~ ssList(app(app(X0,cons(X1,X2)),cons(sK54_skl(X3,X4,X5),nil))) ) ),
introduced(definition,[new_symbols(definition,[sQ118_spl])],[split_symbol_definition]) ).
fof(f1799,plain,
( ~ sQ4_spl
| sQ118_spl ),
inference(split_clause,[status(thm)],[f1774,f1796,f507]) ).
fof(f1821,definition,
! [X0,X1] :
( sQ119_spl
<=> ( sP1_prd(sK43_skl(X0),sK48_skl,X1)
| cons(sK44_skl(X0),sK47_skl) = X0
| nil = X0
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ119_spl])],[split_symbol_definition]) ).
fof(f1831,definition,
! [X0,X1] :
( sQ120_spl
<=> ( sP1_prd(sK44_skl(X0),sK48_skl,X1)
| cons(sK47_skl,sK43_skl(X0)) = X0
| nil = X0
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ120_spl])],[split_symbol_definition]) ).
fof(f1846,plain,
! [X0,X1,X2] :
( ~ sQ109_spl
| ~ sQ68_spl
| sP1_prd(sK44_skl(X0),sK48_skl,X2)
| sP1_prd(cons(hd(sK47_skl),nil),sK48_skl,X1)
| cons(sK47_skl,sK43_skl(X0)) = X0
| nil = X0
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f1715,f1762]) ).
fof(f1847,plain,
! [X0,X1,X2] :
( ~ sQ109_spl
| ~ sQ68_spl
| sP1_prd(sK43_skl(X0),sK48_skl,X2)
| sP1_prd(cons(hd(sK47_skl),nil),sK48_skl,X1)
| cons(sK44_skl(X0),sK47_skl) = X0
| nil = X0
| ~ ssList(X0) ),
inference(paramodulation,[status(thm)],[f1715,f1761]) ).
fof(f1867,definition,
! [X1] :
( sQ121_spl
<=> sP1_prd(cons(hd(sK47_skl),nil),sK48_skl,X1) ),
introduced(definition,[new_symbols(definition,[sQ121_spl])],[split_symbol_definition]) ).
fof(f1870,plain,
( ~ sQ109_spl
| ~ sQ68_spl
| sQ121_spl
| sQ120_spl ),
inference(split_clause,[status(thm)],[f1846,f1831,f1867,f1177,f1714]) ).
fof(f1871,plain,
( ~ sQ109_spl
| ~ sQ68_spl
| sQ121_spl
| sQ119_spl ),
inference(split_clause,[status(thm)],[f1847,f1821,f1867,f1177,f1714]) ).
fof(f1928,plain,
( ~ sQ0_spl
| ~ sQ97_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f539,f1664]) ).
fof(f1932,plain,
( ~ sQ0_spl
| ~ sQ97_spl ),
inference(contradiction_clause,[status(thm)],[f1928]) ).
fof(f1933,plain,
( sQ67_spl
| ~ ssItem(hd(sK48_skl))
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f1176,f222]) ).
fof(f1937,plain,
( sQ67_spl
| ~ sQ69_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f1933,f507,f1180,f1174]) ).
fof(f1940,plain,
$false,
inference(sat_refutation,[status(thm)],[f457,f461,f510,f514,f518,f520,f534,f552,f557,f565,f578,f583,f604,f611,f625,f658,f699,f705,f709,f713,f718,f743,f749,f753,f757,f762,f864,f868,f872,f881,f885,f914,f918,f922,f931,f935,f953,f957,f961,f1036,f1047,f1051,f1055,f1087,f1113,f1140,f1169,f1186,f1204,f1205,f1215,f1221,f1259,f1263,f1266,f1302,f1306,f1310,f1314,f1318,f1322,f1392,f1417,f1427,f1435,f1526,f1530,f1534,f1538,f1542,f1546,f1666,f1675,f1679,f1683,f1687,f1691,f1695,f1699,f1703,f1708,f1717,f1721,f1725,f1730,f1733,f1735,f1779,f1783,f1787,f1791,f1795,f1799,f1870,f1871,f1932,f1937]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWC013+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/0.35 % Computer : n006.cluster.edu
% 0.11/0.35 % Model : x86_64 x86_64
% 0.11/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.35 % Memory : 8046.5625MB
% 0.11/0.35 % OS : Linux 6.8.0-71-generic
% 0.11/0.35 % CPULimit : 300
% 0.11/0.35 % WCLimit : 300
% 0.11/0.35 % DateTime : Mon Sep 21 07:48:58 UTC 2026
% 0.11/0.35 % CPUTime :
% 0.16/0.37 % Drodi V4.1.1
% 2.20/0.83 % Refutation found
% 2.20/0.83 % SZS status Theorem for theBenchmark: Theorem is valid
% 2.20/0.83 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 2.20/0.86 % Elapsed time: 0.497458 seconds
% 2.20/0.86 % CPU time: 3.617392 seconds
% 2.20/0.86 % Total memory used: 147.795 MB
% 2.20/0.86 % Net memory used: 144.170 MB
%------------------------------------------------------------------------------