%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWC306+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 : n005.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 02:40:43 PM UTC 2026
% Result : Theorem 100.16s 13.21s
% Output : CNFRefutation 92.69s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 44
% Syntax : Number of formulae : 200 ( 18 unt; 32 def)
% Number of atoms : 842 ( 65 equ)
% Maximal formula atoms : 18 ( 4 avg)
% Number of connectives : 1143 ( 501 ~; 489 |; 70 &)
% ( 38 <=>; 45 =>; 0 <=; 0 <~>)
% Maximal formula depth : 25 ( 6 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 39 ( 37 usr; 32 prp; 0-3 aty)
% Number of functors : 15 ( 15 usr; 11 con; 0-2 aty)
% Number of variables : 231 ( 205 !; 26 ?)
% 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/sandbox/benchmark/theBenchmark.p') ).
fof(f16,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssItem(V)
=> ssList(cons(V,U)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f17,axiom,
ssList(nil),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f26,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ssList(app(U,V)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f31,axiom,
! [U] :
( ssItem(U)
=> leq(U,U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f33,axiom,
! [U] :
( ssItem(U)
=> ! [V] :
( ssItem(V)
=> ( lt(U,V)
=> ~ lt(V,U) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f34,axiom,
! [U] :
( ssItem(U)
=> ! [V] :
( ssItem(V)
=> ! [W] :
( ssItem(W)
=> ( ( lt(V,W)
& lt(U,V) )
=> lt(U,W) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f36,axiom,
! [U] :
( ssItem(U)
=> ! [V] :
( ssList(V)
=> ! [W] :
( ssList(W)
=> ( memberP(app(V,W),U)
<=> ( memberP(W,U)
| memberP(V,U) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f37,axiom,
! [U] :
( ssItem(U)
=> ! [V] :
( ssItem(V)
=> ! [W] :
( ssList(W)
=> ( memberP(cons(V,W),U)
<=> ( memberP(W,U)
| U = V ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f38,axiom,
! [U] :
( ssItem(U)
=> ~ memberP(nil,U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f91,axiom,
! [U] :
( ssItem(U)
=> ! [V] :
( ssItem(V)
=> ! [W] :
( ssItem(W)
=> ( ( lt(V,W)
& leq(U,V) )
=> lt(U,W) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f96,conjecture,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ! [W] :
( ssList(W)
=> ! [X] :
( ssList(X)
=> ( ( ( nil != W
| nil != X )
& ! [X4] :
( ssItem(X4)
=> ( ~ memberP(X,X4)
| cons(X4,nil) != W ) ) )
| ! [Y] :
( ssItem(Y)
=> ! [Z] :
( ssItem(Z)
=> ! [X1] :
( ssList(X1)
=> ! [X2] :
( ssList(X2)
=> ! [X3] :
( ssList(X3)
=> ( ~ lt(Z,Y)
| app(app(app(app(X1,cons(Y,nil)),X2),cons(Z,nil)),X3) != U ) ) ) ) ) )
| U != W
| V != X ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f97,negated_conjecture,
~ ! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ! [W] :
( ssList(W)
=> ! [X] :
( ssList(X)
=> ( ( ( nil != W
| nil != X )
& ! [X4] :
( ssItem(X4)
=> ( ~ memberP(X,X4)
| cons(X4,nil) != W ) ) )
| ! [Y] :
( ssItem(Y)
=> ! [Z] :
( ssItem(Z)
=> ! [X1] :
( ssList(X1)
=> ! [X2] :
( ssList(X2)
=> ! [X3] :
( ssList(X3)
=> ( ~ lt(Z,Y)
| app(app(app(app(X1,cons(Y,nil)),X2),cons(Z,nil)),X3) != U ) ) ) ) ) )
| 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(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(f244,plain,
! [U] :
( ! [V] :
( ssList(app(U,V))
| ~ ssList(V) )
| ~ ssList(U) ),
inference(pre_NNF_transformation,[status(thm)],[f26]) ).
fof(f245,plain,
! [X0,X1] :
( ssList(app(X0,X1))
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f244]) ).
fof(f254,plain,
! [U] :
( leq(U,U)
| ~ ssItem(U) ),
inference(pre_NNF_transformation,[status(thm)],[f31]) ).
fof(f255,plain,
! [X0] :
( leq(X0,X0)
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(thm)],[f254]) ).
fof(f260,plain,
! [U] :
( ! [V] :
( ~ lt(V,U)
| ~ lt(U,V)
| ~ ssItem(V) )
| ~ ssItem(U) ),
inference(pre_NNF_transformation,[status(thm)],[f33]) ).
fof(f261,plain,
! [X0,X1] :
( ~ lt(X1,X0)
| ~ lt(X0,X1)
| ~ ssItem(X1)
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(thm)],[f260]) ).
fof(f262,plain,
! [U] :
( ! [V] :
( ! [W] :
( lt(U,W)
| ~ lt(V,W)
| ~ lt(U,V)
| ~ ssItem(W) )
| ~ ssItem(V) )
| ~ ssItem(U) ),
inference(pre_NNF_transformation,[status(thm)],[f34]) ).
fof(f263,plain,
! [X0,X1,X2] :
( lt(X0,X2)
| ~ lt(X1,X2)
| ~ lt(X0,X1)
| ~ ssItem(X2)
| ~ ssItem(X1)
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(thm)],[f262]) ).
fof(f268,plain,
! [U] :
( ! [V] :
( ! [W] :
( ( memberP(app(V,W),U)
<=> ( memberP(W,U)
| memberP(V,U) ) )
| ~ ssList(W) )
| ~ ssList(V) )
| ~ ssItem(U) ),
inference(pre_NNF_transformation,[status(thm)],[f36]) ).
fof(f269,plain,
! [U] :
( ! [V] :
( ! [W] :
( ( ( ( ~ memberP(W,U)
& ~ memberP(V,U) )
| memberP(app(V,W),U) )
& ( memberP(W,U)
| memberP(V,U)
| ~ memberP(app(V,W),U) ) )
| ~ ssList(W) )
| ~ ssList(V) )
| ~ ssItem(U) ),
inference(NNF_transformation,[status(thm)],[f268]) ).
fof(f271,plain,
! [X0,X1,X2] :
( ~ memberP(X1,X0)
| memberP(app(X1,X2),X0)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(thm)],[f269]) ).
fof(f273,plain,
! [U] :
( ! [V] :
( ! [W] :
( ( memberP(cons(V,W),U)
<=> ( memberP(W,U)
| U = V ) )
| ~ ssList(W) )
| ~ ssItem(V) )
| ~ ssItem(U) ),
inference(pre_NNF_transformation,[status(thm)],[f37]) ).
fof(f274,plain,
! [U] :
( ! [V] :
( ! [W] :
( ( ( ( ~ memberP(W,U)
& U != V )
| memberP(cons(V,W),U) )
& ( memberP(W,U)
| U = V
| ~ memberP(cons(V,W),U) ) )
| ~ ssList(W) )
| ~ ssItem(V) )
| ~ ssItem(U) ),
inference(NNF_transformation,[status(thm)],[f273]) ).
fof(f275,plain,
! [X0,X1,X2] :
( memberP(X2,X0)
| X0 = X1
| ~ memberP(cons(X1,X2),X0)
| ~ ssList(X2)
| ~ ssItem(X1)
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(thm)],[f274]) ).
fof(f278,plain,
! [U] :
( ~ memberP(nil,U)
| ~ ssItem(U) ),
inference(pre_NNF_transformation,[status(thm)],[f38]) ).
fof(f279,plain,
! [X0] :
( ~ memberP(nil,X0)
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(thm)],[f278]) ).
fof(f402,plain,
! [U] :
( ! [V] :
( ! [W] :
( lt(U,W)
| ~ lt(V,W)
| ~ leq(U,V)
| ~ ssItem(W) )
| ~ ssItem(V) )
| ~ ssItem(U) ),
inference(pre_NNF_transformation,[status(thm)],[f91]) ).
fof(f403,plain,
! [X0,X1,X2] :
( lt(X0,X2)
| ~ lt(X1,X2)
| ~ leq(X0,X1)
| ~ ssItem(X2)
| ~ ssItem(X1)
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(thm)],[f402]) ).
fof(f415,plain,
? [U] :
( ? [V] :
( ? [W] :
( ? [X] :
( ( ( nil = W
& nil = X )
| ? [X4] :
( memberP(X,X4)
& cons(X4,nil) = W
& ssItem(X4) ) )
& ? [Y] :
( ? [Z] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( lt(Z,Y)
& app(app(app(app(X1,cons(Y,nil)),X2),cons(Z,nil)),X3) = U
& ssList(X3) )
& ssList(X2) )
& ssList(X1) )
& ssItem(Z) )
& ssItem(Y) )
& U = W
& V = X
& ssList(X) )
& ssList(W) )
& ssList(V) )
& ssList(U) ),
inference(pre_NNF_transformation,[status(thm)],[f97]) ).
fof(f416,definition,
! [W,X,X4] :
( sP0_prd(X4,X,W)
<=> ( memberP(X,X4)
& cons(X4,nil) = W
& ssItem(X4) ) ),
introduced(definition,[new_symbols(definition,[sP0_prd])],[]) ).
fof(f417,plain,
? [U] :
( ? [V] :
( ? [W] :
( ? [X] :
( ( ( nil = W
& nil = X )
| ? [X4] : sP0_prd(X4,X,W) )
& ? [Y] :
( ? [Z] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( lt(Z,Y)
& app(app(app(app(X1,cons(Y,nil)),X2),cons(Z,nil)),X3) = U
& ssList(X3) )
& ssList(X2) )
& ssList(X1) )
& ssItem(Z) )
& ssItem(Y) )
& U = W
& V = X
& ssList(X) )
& ssList(W) )
& ssList(V) )
& ssList(U) ),
inference(formula_renaming,[status(thm)],[f415,f416]) ).
fof(f418,plain,
( ( ( nil = sK49_skl
& nil = sK50_skl )
| sP0_prd(sK56_skl,sK50_skl,sK49_skl) )
& lt(sK52_skl,sK51_skl)
& app(app(app(app(sK53_skl,cons(sK51_skl,nil)),sK54_skl),cons(sK52_skl,nil)),sK55_skl) = sK47_skl
& ssList(sK55_skl)
& ssList(sK54_skl)
& ssList(sK53_skl)
& ssItem(sK52_skl)
& ssItem(sK51_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,sK51_skl,sK52_skl,sK53_skl,sK54_skl,sK55_skl,sK56_skl]),skolemize(U,sK47_skl),skolemize(V,sK48_skl),skolemize(W,sK49_skl),skolemize(X,sK50_skl),skolemize(Y,sK51_skl),skolemize(Z,sK52_skl),skolemize(X1,sK53_skl),skolemize(X2,sK54_skl),skolemize(X3,sK55_skl),skolemize(X4,sK56_skl)],[f417]) ).
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,
ssItem(sK51_skl),
inference(cnf_transformation,[status(thm)],[f418]) ).
fof(f426,plain,
ssItem(sK52_skl),
inference(cnf_transformation,[status(thm)],[f418]) ).
fof(f427,plain,
ssList(sK53_skl),
inference(cnf_transformation,[status(thm)],[f418]) ).
fof(f428,plain,
ssList(sK54_skl),
inference(cnf_transformation,[status(thm)],[f418]) ).
fof(f429,plain,
ssList(sK55_skl),
inference(cnf_transformation,[status(thm)],[f418]) ).
fof(f430,plain,
app(app(app(app(sK53_skl,cons(sK51_skl,nil)),sK54_skl),cons(sK52_skl,nil)),sK55_skl) = sK47_skl,
inference(cnf_transformation,[status(thm)],[f418]) ).
fof(f431,plain,
lt(sK52_skl,sK51_skl),
inference(cnf_transformation,[status(thm)],[f418]) ).
fof(f433,plain,
( nil = sK49_skl
| sP0_prd(sK56_skl,sK50_skl,sK49_skl) ),
inference(cnf_transformation,[status(thm)],[f418]) ).
fof(f434,plain,
! [W,X,X4] :
( ( ~ memberP(X,X4)
| cons(X4,nil) != W
| ~ ssItem(X4)
| sP0_prd(X4,X,W) )
& ( ( memberP(X,X4)
& cons(X4,nil) = W
& ssItem(X4) )
| ~ sP0_prd(X4,X,W) ) ),
inference(NNF_transformation,[status(thm)],[f416]) ).
fof(f435,plain,
( ! [W,X,X4] :
( ~ memberP(X,X4)
| cons(X4,nil) != W
| ~ ssItem(X4)
| sP0_prd(X4,X,W) )
& ! [W,X,X4] :
( ( memberP(X,X4)
& cons(X4,nil) = W
& ssItem(X4) )
| ~ sP0_prd(X4,X,W) ) ),
inference(miniscoping,[status(thm)],[f434]) ).
fof(f436,plain,
! [X0,X1,X2] :
( ssItem(X0)
| ~ sP0_prd(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f435]) ).
fof(f437,plain,
! [X0,X1,X2] :
( cons(X0,nil) = X2
| ~ sP0_prd(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f435]) ).
fof(f440,definition,
( sQ0_spl
<=> sP0_prd(sK56_skl,sK50_skl,sK49_skl) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f441,plain,
( ~ sQ0_spl
| sP0_prd(sK56_skl,sK50_skl,sK49_skl) ),
inference(component_clause,[status(thm)],[f440]) ).
fof(f447,definition,
( sQ2_spl
<=> nil = sK49_skl ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f448,plain,
( ~ sQ2_spl
| nil = sK49_skl ),
inference(component_clause,[status(thm)],[f447]) ).
fof(f450,plain,
( sQ2_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f433,f440,f447]) ).
fof(f453,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(f486,plain,
( ~ sQ0_spl
| sP0_prd(sK56_skl,sK48_skl,sK49_skl) ),
inference(forward_demodulation,[status(thm)],[f423,f441]) ).
fof(f487,plain,
( ~ sQ0_spl
| sP0_prd(sK56_skl,sK48_skl,sK47_skl) ),
inference(forward_demodulation,[status(thm)],[f424,f486]) ).
fof(f489,plain,
( ~ sQ0_spl
| ssItem(sK56_skl) ),
inference(resolution,[status(thm)],[f487,f436]) ).
fof(f490,plain,
( ~ sQ0_spl
| cons(sK56_skl,nil) = sK47_skl ),
inference(resolution,[status(thm)],[f437,f487]) ).
fof(f494,definition,
( sQ3_spl
<=> ssList(nil) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f496,plain,
( sQ3_spl
| ~ ssList(nil) ),
inference(component_clause,[status(thm)],[f494]) ).
fof(f497,definition,
( sQ4_spl
<=> ssItem(sK56_skl) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f499,plain,
( sQ4_spl
| ~ ssItem(sK56_skl) ),
inference(component_clause,[status(thm)],[f497]) ).
fof(f512,plain,
( sQ4_spl
| ~ sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f499,f489]) ).
fof(f513,plain,
( sQ4_spl
| ~ sQ0_spl ),
inference(contradiction_clause,[status(thm)],[f512]) ).
fof(f518,definition,
( sQ8_spl
<=> ssList(app(app(app(sK53_skl,cons(sK51_skl,nil)),sK54_skl),cons(sK52_skl,nil))) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f520,plain,
( sQ8_spl
| ~ ssList(app(app(app(sK53_skl,cons(sK51_skl,nil)),sK54_skl),cons(sK52_skl,nil))) ),
inference(component_clause,[status(thm)],[f518]) ).
fof(f521,definition,
( sQ9_spl
<=> ssList(sK55_skl) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f523,plain,
( sQ9_spl
| ~ ssList(sK55_skl) ),
inference(component_clause,[status(thm)],[f521]) ).
fof(f525,plain,
( sQ3_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f496,f223]) ).
fof(f526,plain,
sQ3_spl,
inference(contradiction_clause,[status(thm)],[f525]) ).
fof(f541,definition,
( sQ11_spl
<=> ssItem(sK51_skl) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f543,plain,
( sQ11_spl
| ~ ssItem(sK51_skl) ),
inference(component_clause,[status(thm)],[f541]) ).
fof(f544,definition,
( sQ12_spl
<=> ssItem(sK52_skl) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f546,plain,
( sQ12_spl
| ~ ssItem(sK52_skl) ),
inference(component_clause,[status(thm)],[f544]) ).
fof(f556,plain,
( sQ11_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f543,f425]) ).
fof(f557,plain,
sQ11_spl,
inference(contradiction_clause,[status(thm)],[f556]) ).
fof(f558,plain,
( sQ12_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f546,f426]) ).
fof(f559,plain,
sQ12_spl,
inference(contradiction_clause,[status(thm)],[f558]) ).
fof(f661,plain,
! [X0] :
( ~ memberP(app(app(app(sK53_skl,cons(sK51_skl,nil)),sK54_skl),cons(sK52_skl,nil)),X0)
| memberP(sK47_skl,X0)
| ~ ssList(sK55_skl)
| ~ ssList(app(app(app(sK53_skl,cons(sK51_skl,nil)),sK54_skl),cons(sK52_skl,nil)))
| ~ ssItem(X0) ),
inference(paramodulation,[status(thm)],[f430,f271]) ).
fof(f662,definition,
! [X0] :
( sQ30_spl
<=> ( ~ memberP(app(app(app(sK53_skl,cons(sK51_skl,nil)),sK54_skl),cons(sK52_skl,nil)),X0)
| memberP(sK47_skl,X0)
| ~ ssItem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f663,plain,
! [X0] :
( ~ sQ30_spl
| ~ memberP(app(app(app(sK53_skl,cons(sK51_skl,nil)),sK54_skl),cons(sK52_skl,nil)),X0)
| memberP(sK47_skl,X0)
| ~ ssItem(X0) ),
inference(component_clause,[status(thm)],[f662]) ).
fof(f665,plain,
( ~ sQ9_spl
| ~ sQ8_spl
| sQ30_spl ),
inference(split_clause,[status(thm)],[f661,f662,f518,f521]) ).
fof(f666,plain,
( sQ9_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f523,f429]) ).
fof(f667,plain,
sQ9_spl,
inference(contradiction_clause,[status(thm)],[f666]) ).
fof(f678,plain,
! [X0] :
( lt(X0,sK51_skl)
| ~ lt(X0,sK52_skl)
| ~ ssItem(sK51_skl)
| ~ ssItem(sK52_skl)
| ~ ssItem(X0) ),
inference(resolution,[status(thm)],[f263,f431]) ).
fof(f679,plain,
! [X0,X1,X2,X3] :
( ~ lt(X3,X2)
| ~ lt(X1,X3)
| ~ ssItem(X2)
| ~ ssItem(X3)
| ~ ssItem(X1)
| lt(X0,X2)
| ~ lt(X0,X1)
| ~ ssItem(X2)
| ~ ssItem(X1)
| ~ ssItem(X0) ),
inference(resolution,[status(thm)],[f263,f263]) ).
fof(f685,definition,
! [X0] :
( sQ33_spl
<=> ( lt(X0,sK51_skl)
| ~ lt(X0,sK52_skl)
| ~ ssItem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f686,plain,
! [X0] :
( ~ sQ33_spl
| lt(X0,sK51_skl)
| ~ lt(X0,sK52_skl)
| ~ ssItem(X0) ),
inference(component_clause,[status(thm)],[f685]) ).
fof(f688,plain,
( ~ sQ11_spl
| ~ sQ12_spl
| sQ33_spl ),
inference(split_clause,[status(thm)],[f678,f685,f544,f541]) ).
fof(f689,plain,
! [X0,X1,X2,X3] :
( ~ lt(X3,X2)
| ~ lt(X1,X3)
| ~ ssItem(X3)
| lt(X0,X2)
| ~ lt(X0,X1)
| ~ ssItem(X2)
| ~ ssItem(X1)
| ~ ssItem(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f679]) ).
fof(f761,plain,
! [X0,X1] :
( ~ sQ33_spl
| lt(X0,sK51_skl)
| ~ ssItem(X0)
| ~ lt(X1,sK52_skl)
| ~ leq(X0,X1)
| ~ ssItem(sK52_skl)
| ~ ssItem(X1)
| ~ ssItem(X0) ),
inference(resolution,[status(thm)],[f403,f686]) ).
fof(f789,definition,
! [X0,X1] :
( sQ46_spl
<=> ( lt(X0,sK51_skl)
| ~ ssItem(X0)
| ~ lt(X1,sK52_skl)
| ~ leq(X0,X1)
| ~ ssItem(X1)
| ~ ssItem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition]) ).
fof(f790,plain,
! [X0,X1] :
( ~ sQ46_spl
| lt(X0,sK51_skl)
| ~ ssItem(X0)
| ~ lt(X1,sK52_skl)
| ~ leq(X0,X1)
| ~ ssItem(X1)
| ~ ssItem(X0) ),
inference(component_clause,[status(thm)],[f789]) ).
fof(f792,plain,
( ~ sQ33_spl
| ~ sQ12_spl
| sQ46_spl ),
inference(split_clause,[status(thm)],[f761,f789,f544,f685]) ).
fof(f801,plain,
! [X0,X1] :
( ~ sQ46_spl
| lt(X0,sK51_skl)
| ~ lt(X1,sK52_skl)
| ~ leq(X0,X1)
| ~ ssItem(X1)
| ~ ssItem(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f790]) ).
fof(f917,plain,
! [X0] :
( ~ sQ0_spl
| memberP(nil,X0)
| X0 = sK56_skl
| ~ memberP(sK47_skl,X0)
| ~ ssList(nil)
| ~ ssItem(sK56_skl)
| ~ ssItem(X0) ),
inference(paramodulation,[status(thm)],[f490,f275]) ).
fof(f918,definition,
! [X0] :
( sQ62_spl
<=> ( memberP(nil,X0)
| X0 = sK56_skl
| ~ memberP(sK47_skl,X0)
| ~ ssItem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition]) ).
fof(f919,plain,
! [X0] :
( ~ sQ62_spl
| memberP(nil,X0)
| X0 = sK56_skl
| ~ memberP(sK47_skl,X0)
| ~ ssItem(X0) ),
inference(component_clause,[status(thm)],[f918]) ).
fof(f921,plain,
( ~ sQ0_spl
| ~ sQ3_spl
| ~ sQ4_spl
| sQ62_spl ),
inference(split_clause,[status(thm)],[f917,f918,f497,f494,f440]) ).
fof(f922,plain,
! [X0] :
( ~ sQ62_spl
| X0 = sK56_skl
| ~ memberP(sK47_skl,X0)
| ~ ssItem(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f919,f279]) ).
fof(f943,plain,
! [X0,X1] :
( ~ sQ46_spl
| ~ lt(sK51_skl,X0)
| ~ ssItem(X0)
| ~ ssItem(sK51_skl)
| ~ lt(X1,sK52_skl)
| ~ leq(X0,X1)
| ~ ssItem(X1)
| ~ ssItem(X0) ),
inference(resolution,[status(thm)],[f801,f261]) ).
fof(f964,definition,
! [X0,X1] :
( sQ67_spl
<=> ( ~ lt(sK51_skl,X0)
| ~ ssItem(X0)
| ~ lt(X1,sK52_skl)
| ~ leq(X0,X1)
| ~ ssItem(X1)
| ~ ssItem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition]) ).
fof(f965,plain,
! [X0,X1] :
( ~ sQ67_spl
| ~ lt(sK51_skl,X0)
| ~ ssItem(X0)
| ~ lt(X1,sK52_skl)
| ~ leq(X0,X1)
| ~ ssItem(X1)
| ~ ssItem(X0) ),
inference(component_clause,[status(thm)],[f964]) ).
fof(f967,plain,
( ~ sQ46_spl
| ~ sQ11_spl
| sQ67_spl ),
inference(split_clause,[status(thm)],[f943,f964,f541,f789]) ).
fof(f972,plain,
! [X0,X1] :
( ~ sQ67_spl
| ~ lt(sK51_skl,X0)
| ~ lt(X1,sK52_skl)
| ~ leq(X0,X1)
| ~ ssItem(X1)
| ~ ssItem(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f965]) ).
fof(f1138,definition,
( sQ88_spl
<=> lt(sK51_skl,sK51_skl) ),
introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition]) ).
fof(f1140,plain,
( sQ88_spl
| ~ lt(sK51_skl,sK51_skl) ),
inference(component_clause,[status(thm)],[f1138]) ).
fof(f1158,plain,
( sQ8_spl
| ~ ssList(cons(sK52_skl,nil))
| ~ ssList(app(app(sK53_skl,cons(sK51_skl,nil)),sK54_skl)) ),
inference(resolution,[status(thm)],[f520,f245]) ).
fof(f1159,definition,
( sQ91_spl
<=> ssList(app(app(sK53_skl,cons(sK51_skl,nil)),sK54_skl)) ),
introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition]) ).
fof(f1161,plain,
( sQ91_spl
| ~ ssList(app(app(sK53_skl,cons(sK51_skl,nil)),sK54_skl)) ),
inference(component_clause,[status(thm)],[f1159]) ).
fof(f1162,definition,
( sQ92_spl
<=> ssList(cons(sK52_skl,nil)) ),
introduced(definition,[new_symbols(definition,[sQ92_spl])],[split_symbol_definition]) ).
fof(f1164,plain,
( sQ92_spl
| ~ ssList(cons(sK52_skl,nil)) ),
inference(component_clause,[status(thm)],[f1162]) ).
fof(f1165,plain,
( sQ8_spl
| ~ sQ92_spl
| ~ sQ91_spl ),
inference(split_clause,[status(thm)],[f1158,f1159,f1162,f518]) ).
fof(f1169,plain,
! [X0,X1,X2] :
( ~ sQ67_spl
| ~ lt(X2,sK52_skl)
| ~ lt(X1,X2)
| ~ ssItem(sK52_skl)
| ~ ssItem(X2)
| ~ ssItem(X1)
| ~ lt(sK51_skl,X0)
| ~ leq(X0,X1)
| ~ ssItem(X1)
| ~ ssItem(X0) ),
inference(resolution,[status(thm)],[f972,f263]) ).
fof(f1183,definition,
! [X0,X1,X2] :
( sQ94_spl
<=> ( ~ lt(X2,sK52_skl)
| ~ lt(X1,X2)
| ~ ssItem(X2)
| ~ ssItem(X1)
| ~ lt(sK51_skl,X0)
| ~ leq(X0,X1)
| ~ ssItem(X1)
| ~ ssItem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition]) ).
fof(f1184,plain,
! [X0,X1,X2] :
( ~ sQ94_spl
| ~ lt(X2,sK52_skl)
| ~ lt(X1,X2)
| ~ ssItem(X2)
| ~ ssItem(X1)
| ~ lt(sK51_skl,X0)
| ~ leq(X0,X1)
| ~ ssItem(X1)
| ~ ssItem(X0) ),
inference(component_clause,[status(thm)],[f1183]) ).
fof(f1186,plain,
( ~ sQ67_spl
| ~ sQ12_spl
| sQ94_spl ),
inference(split_clause,[status(thm)],[f1169,f1183,f544,f964]) ).
fof(f1198,plain,
! [X0,X1,X2] :
( ~ sQ94_spl
| ~ lt(X2,sK52_skl)
| ~ lt(X1,X2)
| ~ ssItem(X2)
| ~ lt(sK51_skl,X0)
| ~ leq(X0,X1)
| ~ ssItem(X1)
| ~ ssItem(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1184]) ).
fof(f1372,definition,
( sQ106_spl
<=> leq(sK51_skl,sK51_skl) ),
introduced(definition,[new_symbols(definition,[sQ106_spl])],[split_symbol_definition]) ).
fof(f1374,plain,
( sQ106_spl
| ~ leq(sK51_skl,sK51_skl) ),
inference(component_clause,[status(thm)],[f1372]) ).
fof(f2154,definition,
! [X0,X1] :
( sQ164_spl
<=> ( ~ lt(X1,sK51_skl)
| ~ lt(X0,X1)
| ~ ssItem(X1)
| ~ lt(sK51_skl,X0)
| ~ ssItem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ164_spl])],[split_symbol_definition]) ).
fof(f2155,plain,
! [X0,X1] :
( ~ sQ164_spl
| ~ lt(X1,sK51_skl)
| ~ lt(X0,X1)
| ~ ssItem(X1)
| ~ lt(sK51_skl,X0)
| ~ ssItem(X0) ),
inference(component_clause,[status(thm)],[f2154]) ).
fof(f4409,plain,
! [X0,X1,X2] :
( ~ sQ164_spl
| ~ lt(X2,X0)
| ~ lt(sK51_skl,X2)
| ~ ssItem(X0)
| ~ ssItem(X2)
| ~ ssItem(sK51_skl)
| ~ lt(X1,sK51_skl)
| ~ lt(X0,X1)
| ~ ssItem(X1)
| ~ ssItem(X0) ),
inference(resolution,[status(thm)],[f2155,f263]) ).
fof(f4414,definition,
! [X0,X1,X3] :
( sQ337_spl
<=> ( ~ lt(X3,X0)
| ~ lt(sK51_skl,X3)
| ~ ssItem(X3)
| ~ ssItem(X0)
| ~ lt(X1,sK51_skl)
| ~ lt(X0,X1)
| ~ ssItem(X1)
| ~ ssItem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ337_spl])],[split_symbol_definition]) ).
fof(f4415,plain,
! [X0,X1,X2] :
( ~ sQ337_spl
| ~ lt(X2,X0)
| ~ lt(sK51_skl,X2)
| ~ ssItem(X2)
| ~ ssItem(X0)
| ~ lt(X1,sK51_skl)
| ~ lt(X0,X1)
| ~ ssItem(X1)
| ~ ssItem(X0) ),
inference(component_clause,[status(thm)],[f4414]) ).
fof(f4431,plain,
( ~ sQ164_spl
| ~ sQ11_spl
| sQ337_spl ),
inference(split_clause,[status(thm)],[f4409,f4414,f541,f2154]) ).
fof(f4432,plain,
! [X0,X1,X2] :
( ~ sQ337_spl
| ~ lt(X2,X0)
| ~ lt(sK51_skl,X2)
| ~ ssItem(X2)
| ~ lt(X1,sK51_skl)
| ~ lt(X0,X1)
| ~ ssItem(X1)
| ~ ssItem(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f4415]) ).
fof(f4488,plain,
( ~ sQ337_spl
| ~ ssItem(sK51_skl)
| ~ lt(sK51_skl,sK51_skl)
| ~ lt(sK51_skl,sK51_skl)
| ~ ssItem(sK51_skl)
| ~ ssItem(sK51_skl) ),
inference(factoring,[status(thm)],[f4432]) ).
fof(f4557,plain,
( ~ sQ337_spl
| ~ sQ88_spl
| ~ sQ11_spl ),
inference(split_clause,[status(thm)],[f4488,f541,f1138,f4414]) ).
fof(f4862,plain,
( sQ106_spl
| ~ ssItem(sK51_skl) ),
inference(resolution,[status(thm)],[f1374,f255]) ).
fof(f4864,plain,
( sQ106_spl
| ~ sQ11_spl ),
inference(split_clause,[status(thm)],[f4862,f541,f1372]) ).
fof(f4887,plain,
( sQ92_spl
| ~ ssItem(sK52_skl)
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f1164,f222]) ).
fof(f4888,plain,
( sQ92_spl
| ~ sQ12_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f4887,f494,f544,f1162]) ).
fof(f5458,plain,
! [X0] :
( ~ sQ30_spl
| ~ memberP(app(app(sK53_skl,cons(sK51_skl,nil)),sK54_skl),X0)
| ~ ssList(cons(sK52_skl,nil))
| ~ ssList(app(app(sK53_skl,cons(sK51_skl,nil)),sK54_skl))
| ~ ssItem(X0)
| memberP(sK47_skl,X0)
| ~ ssItem(X0) ),
inference(resolution,[status(thm)],[f663,f271]) ).
fof(f5463,definition,
! [X0] :
( sQ427_spl
<=> ( ~ memberP(app(app(sK53_skl,cons(sK51_skl,nil)),sK54_skl),X0)
| ~ ssItem(X0)
| memberP(sK47_skl,X0)
| ~ ssItem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ427_spl])],[split_symbol_definition]) ).
fof(f5464,plain,
! [X0] :
( ~ sQ427_spl
| ~ memberP(app(app(sK53_skl,cons(sK51_skl,nil)),sK54_skl),X0)
| ~ ssItem(X0)
| memberP(sK47_skl,X0)
| ~ ssItem(X0) ),
inference(component_clause,[status(thm)],[f5463]) ).
fof(f5466,plain,
( ~ sQ30_spl
| ~ sQ92_spl
| ~ sQ91_spl
| sQ427_spl ),
inference(split_clause,[status(thm)],[f5458,f5463,f1159,f1162,f662]) ).
fof(f9082,definition,
( sQ602_spl
<=> sK51_skl = sK52_skl ),
introduced(definition,[new_symbols(definition,[sQ602_spl])],[split_symbol_definition]) ).
fof(f9083,plain,
( ~ sQ602_spl
| sK51_skl = sK52_skl ),
inference(component_clause,[status(thm)],[f9082]) ).
fof(f10190,definition,
! [X0,X1,X2] :
( sQ686_spl
<=> ( ~ lt(X2,sK51_skl)
| ~ lt(X1,X2)
| ~ ssItem(X2)
| ~ lt(sK51_skl,X0)
| ~ leq(X0,X1)
| ~ ssItem(X1)
| ~ ssItem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ686_spl])],[split_symbol_definition]) ).
fof(f10191,plain,
! [X0,X1,X2] :
( ~ sQ686_spl
| ~ lt(X2,sK51_skl)
| ~ lt(X1,X2)
| ~ ssItem(X2)
| ~ lt(sK51_skl,X0)
| ~ leq(X0,X1)
| ~ ssItem(X1)
| ~ ssItem(X0) ),
inference(component_clause,[status(thm)],[f10190]) ).
fof(f10322,plain,
! [X0,X1] :
( ~ sQ686_spl
| ~ lt(X1,sK51_skl)
| ~ lt(X0,X1)
| ~ ssItem(X1)
| ~ lt(sK51_skl,X0)
| ~ ssItem(sK51_skl)
| ~ ssItem(X0)
| ~ ssItem(sK51_skl)
| ~ ssItem(sK51_skl)
| ~ leq(sK51_skl,sK51_skl)
| ~ ssItem(sK51_skl)
| ~ ssItem(sK51_skl) ),
inference(resolution,[status(thm)],[f10191,f689]) ).
fof(f10383,plain,
( ~ sQ686_spl
| sQ164_spl
| ~ sQ106_spl
| ~ sQ11_spl ),
inference(split_clause,[status(thm)],[f10322,f541,f1372,f2154,f10190]) ).
fof(f10840,plain,
( ~ sQ2_spl
| sK47_skl = nil ),
inference(backward_demodulation,[status(thm)],[f448,f424]) ).
fof(f10849,plain,
( ~ sQ30_spl
| memberP(sK47_skl,sK52_skl)
| ~ ssItem(sK52_skl)
| ~ ssList(nil)
| ~ ssList(app(app(sK53_skl,cons(sK51_skl,nil)),sK54_skl))
| ~ ssItem(sK52_skl)
| ~ ssList(app(app(app(sK53_skl,cons(sK51_skl,nil)),sK54_skl),cons(sK52_skl,nil))) ),
inference(resolution,[status(thm)],[f453,f663]) ).
fof(f10851,definition,
( sQ706_spl
<=> memberP(sK47_skl,sK52_skl) ),
introduced(definition,[new_symbols(definition,[sQ706_spl])],[split_symbol_definition]) ).
fof(f10852,plain,
( ~ sQ706_spl
| memberP(sK47_skl,sK52_skl) ),
inference(component_clause,[status(thm)],[f10851]) ).
fof(f10854,plain,
( ~ sQ30_spl
| sQ706_spl
| ~ sQ3_spl
| ~ sQ91_spl
| ~ sQ12_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f10849,f518,f544,f1159,f494,f10851,f662]) ).
fof(f10879,plain,
( sQ91_spl
| ~ ssList(sK54_skl)
| ~ ssList(app(sK53_skl,cons(sK51_skl,nil))) ),
inference(resolution,[status(thm)],[f1161,f245]) ).
fof(f10880,definition,
( sQ708_spl
<=> ssList(app(sK53_skl,cons(sK51_skl,nil))) ),
introduced(definition,[new_symbols(definition,[sQ708_spl])],[split_symbol_definition]) ).
fof(f10882,plain,
( sQ708_spl
| ~ ssList(app(sK53_skl,cons(sK51_skl,nil))) ),
inference(component_clause,[status(thm)],[f10880]) ).
fof(f10883,definition,
( sQ709_spl
<=> ssList(sK54_skl) ),
introduced(definition,[new_symbols(definition,[sQ709_spl])],[split_symbol_definition]) ).
fof(f10885,plain,
( sQ709_spl
| ~ ssList(sK54_skl) ),
inference(component_clause,[status(thm)],[f10883]) ).
fof(f10886,plain,
( sQ91_spl
| ~ sQ709_spl
| ~ sQ708_spl ),
inference(split_clause,[status(thm)],[f10879,f10880,f10883,f1159]) ).
fof(f10887,plain,
( sQ708_spl
| ~ ssList(cons(sK51_skl,nil))
| ~ ssList(sK53_skl) ),
inference(resolution,[status(thm)],[f10882,f245]) ).
fof(f10888,definition,
( sQ710_spl
<=> ssList(sK53_skl) ),
introduced(definition,[new_symbols(definition,[sQ710_spl])],[split_symbol_definition]) ).
fof(f10890,plain,
( sQ710_spl
| ~ ssList(sK53_skl) ),
inference(component_clause,[status(thm)],[f10888]) ).
fof(f10891,definition,
( sQ711_spl
<=> ssList(cons(sK51_skl,nil)) ),
introduced(definition,[new_symbols(definition,[sQ711_spl])],[split_symbol_definition]) ).
fof(f10893,plain,
( sQ711_spl
| ~ ssList(cons(sK51_skl,nil)) ),
inference(component_clause,[status(thm)],[f10891]) ).
fof(f10894,plain,
( sQ708_spl
| ~ sQ711_spl
| ~ sQ710_spl ),
inference(split_clause,[status(thm)],[f10887,f10888,f10891,f10880]) ).
fof(f10895,plain,
( sQ709_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f10885,f428]) ).
fof(f10896,plain,
sQ709_spl,
inference(contradiction_clause,[status(thm)],[f10895]) ).
fof(f10897,plain,
( sQ710_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f10890,f427]) ).
fof(f10898,plain,
sQ710_spl,
inference(contradiction_clause,[status(thm)],[f10897]) ).
fof(f10899,plain,
( sQ711_spl
| ~ ssItem(sK51_skl)
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f10893,f222]) ).
fof(f10900,plain,
( sQ711_spl
| ~ sQ11_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f10899,f494,f541,f10891]) ).
fof(f10907,plain,
( ~ sQ706_spl
| ~ sQ2_spl
| memberP(nil,sK52_skl) ),
inference(forward_demodulation,[status(thm)],[f10840,f10852]) ).
fof(f10912,plain,
( ~ sQ706_spl
| ~ sQ2_spl
| ~ ssItem(sK52_skl) ),
inference(resolution,[status(thm)],[f10907,f279]) ).
fof(f10913,plain,
( ~ sQ706_spl
| ~ sQ2_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f10912,f544,f447,f10851]) ).
fof(f10915,plain,
! [X0] :
( ~ sQ427_spl
| ~ memberP(app(app(sK53_skl,cons(sK51_skl,nil)),sK54_skl),X0)
| memberP(sK47_skl,X0)
| ~ ssItem(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f5464]) ).
fof(f11038,plain,
( ~ sQ706_spl
| ~ sQ62_spl
| sK52_skl = sK56_skl
| ~ ssItem(sK52_skl) ),
inference(resolution,[status(thm)],[f922,f10852]) ).
fof(f11040,definition,
( sQ715_spl
<=> sK52_skl = sK56_skl ),
introduced(definition,[new_symbols(definition,[sQ715_spl])],[split_symbol_definition]) ).
fof(f11041,plain,
( ~ sQ715_spl
| sK52_skl = sK56_skl ),
inference(component_clause,[status(thm)],[f11040]) ).
fof(f11043,plain,
( ~ sQ706_spl
| ~ sQ62_spl
| sQ715_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f11038,f544,f11040,f918,f10851]) ).
fof(f11044,plain,
! [X0] :
( ~ sQ62_spl
| ~ sQ715_spl
| X0 = sK52_skl
| ~ memberP(sK47_skl,X0)
| ~ ssItem(X0) ),
inference(backward_demodulation,[status(thm)],[f11041,f922]) ).
fof(f11198,plain,
! [X0] :
( ~ sQ427_spl
| ~ memberP(app(sK53_skl,cons(sK51_skl,nil)),X0)
| ~ ssList(sK54_skl)
| ~ ssList(app(sK53_skl,cons(sK51_skl,nil)))
| ~ ssItem(X0)
| memberP(sK47_skl,X0)
| ~ ssItem(X0) ),
inference(resolution,[status(thm)],[f10915,f271]) ).
fof(f11203,definition,
! [X0] :
( sQ738_spl
<=> ( ~ memberP(app(sK53_skl,cons(sK51_skl,nil)),X0)
| ~ ssItem(X0)
| memberP(sK47_skl,X0)
| ~ ssItem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ738_spl])],[split_symbol_definition]) ).
fof(f11204,plain,
! [X0] :
( ~ sQ738_spl
| ~ memberP(app(sK53_skl,cons(sK51_skl,nil)),X0)
| ~ ssItem(X0)
| memberP(sK47_skl,X0)
| ~ ssItem(X0) ),
inference(component_clause,[status(thm)],[f11203]) ).
fof(f11206,plain,
( ~ sQ427_spl
| ~ sQ709_spl
| ~ sQ708_spl
| sQ738_spl ),
inference(split_clause,[status(thm)],[f11198,f11203,f10880,f10883,f5463]) ).
fof(f11208,plain,
! [X0] :
( ~ sQ738_spl
| ~ memberP(app(sK53_skl,cons(sK51_skl,nil)),X0)
| memberP(sK47_skl,X0)
| ~ ssItem(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f11204]) ).
fof(f11209,plain,
( ~ sQ738_spl
| ~ ssList(nil)
| ~ ssList(sK53_skl)
| ~ ssItem(sK51_skl)
| ~ ssList(app(sK53_skl,cons(sK51_skl,nil)))
| memberP(sK47_skl,sK51_skl)
| ~ ssItem(sK51_skl) ),
inference(resolution,[status(thm)],[f11208,f453]) ).
fof(f11212,definition,
( sQ739_spl
<=> memberP(sK47_skl,sK51_skl) ),
introduced(definition,[new_symbols(definition,[sQ739_spl])],[split_symbol_definition]) ).
fof(f11213,plain,
( ~ sQ739_spl
| memberP(sK47_skl,sK51_skl) ),
inference(component_clause,[status(thm)],[f11212]) ).
fof(f11215,plain,
( ~ sQ738_spl
| ~ sQ3_spl
| ~ sQ710_spl
| ~ sQ708_spl
| sQ739_spl
| ~ sQ11_spl ),
inference(split_clause,[status(thm)],[f11209,f541,f11212,f10880,f10888,f494,f11203]) ).
fof(f11226,plain,
( ~ sQ62_spl
| ~ sQ715_spl
| ~ sQ739_spl
| sK51_skl = sK52_skl
| ~ ssItem(sK51_skl) ),
inference(resolution,[status(thm)],[f11213,f11044]) ).
fof(f11227,plain,
( ~ sQ62_spl
| ~ sQ715_spl
| ~ sQ739_spl
| sQ602_spl
| ~ sQ11_spl ),
inference(split_clause,[status(thm)],[f11226,f541,f9082,f11212,f11040,f918]) ).
fof(f11264,plain,
! [X0,X1,X2] :
( ~ sQ94_spl
| ~ sQ602_spl
| ~ lt(X2,sK51_skl)
| ~ lt(X1,X2)
| ~ ssItem(X2)
| ~ lt(sK51_skl,X0)
| ~ leq(X0,X1)
| ~ ssItem(X1)
| ~ ssItem(X0) ),
inference(backward_demodulation,[status(thm)],[f9083,f1198]) ).
fof(f11294,plain,
( ~ sQ602_spl
| lt(sK51_skl,sK51_skl) ),
inference(backward_demodulation,[status(thm)],[f9083,f431]) ).
fof(f11311,plain,
( ~ sQ94_spl
| ~ sQ602_spl
| sQ686_spl ),
inference(split_clause,[status(thm)],[f11264,f10190,f9082,f1183]) ).
fof(f11317,plain,
( ~ sQ602_spl
| sQ88_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11294,f1140]) ).
fof(f11318,plain,
( ~ sQ602_spl
| sQ88_spl ),
inference(contradiction_clause,[status(thm)],[f11317]) ).
fof(f11319,plain,
$false,
inference(sat_refutation,[status(thm)],[f450,f513,f526,f557,f559,f665,f667,f688,f792,f921,f967,f1165,f1186,f4431,f4557,f4864,f4888,f5466,f10383,f10854,f10886,f10894,f10896,f10898,f10900,f10913,f11043,f11206,f11215,f11227,f11311,f11318]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWC306+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.14/0.39 % Computer : n005.cluster.edu
% 0.14/0.39 % Model : x86_64 x86_64
% 0.14/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.39 % Memory : 8046.5625MB
% 0.14/0.39 % OS : Linux 6.8.0-71-generic
% 0.14/0.39 % CPULimit : 300
% 0.14/0.39 % WCLimit : 300
% 0.14/0.39 % DateTime : Mon Sep 21 08:13:33 UTC 2026
% 0.14/0.39 % CPUTime :
% 0.19/0.42 % Drodi V4.1.1
% 100.16/13.21 % Refutation found
% 100.16/13.21 % SZS status Theorem for theBenchmark: Theorem is valid
% 100.16/13.21 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 92.69/13.27 % Elapsed time: 12.853667 seconds
% 92.69/13.27 % CPU time: 101.267780 seconds
% 92.69/13.27 % Total memory used: 395.737 MB
% 92.69/13.27 % Net memory used: 366.716 MB
%------------------------------------------------------------------------------