%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWC394+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 : 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:41:04 PM UTC 2026
% Result : Theorem 269.20s 34.70s
% Output : CNFRefutation 222.73s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 56
% Syntax : Number of formulae : 275 ( 72 unt; 44 def)
% Number of atoms : 665 ( 104 equ)
% Maximal formula atoms : 13 ( 2 avg)
% Number of connectives : 680 ( 290 ~; 263 |; 54 &)
% ( 48 <=>; 25 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 52 ( 50 usr; 44 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 8 con; 0-2 aty)
% Number of variables : 137 ( 119 !; 18 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
? [U] :
( ? [V] :
( U != V
& ssItem(V) )
& ssItem(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ( segmentP(U,V)
<=> ? [W] :
( ? [X] :
( app(app(W,V),X) = U
& ssList(X) )
& ssList(W) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(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(f18,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssItem(V)
=> cons(V,U) != U ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f21,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssItem(V)
=> nil != cons(V,U) ) ),
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(f28,axiom,
! [U] :
( ssList(U)
=> app(nil,U) = U ),
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(f39,axiom,
~ singletonP(nil),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f84,axiom,
! [U] :
( ssList(U)
=> app(U,nil) = U ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f96,conjecture,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ! [W] :
( ssList(W)
=> ! [X] :
( ssList(X)
=> ( ( ( ~ segmentP(X,W)
| ~ neq(W,nil) )
& ( nil != W
| nil != X ) )
| ! [Y] :
( ssItem(Y)
=> ( memberP(V,Y)
| ~ memberP(U,Y) ) )
| 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)
=> ( ( ( ~ segmentP(X,W)
| ~ neq(W,nil) )
& ( nil != W
| nil != X ) )
| ! [Y] :
( ssItem(Y)
=> ( memberP(V,Y)
| ~ memberP(U,Y) ) )
| U != W
| V != X ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f96]) ).
fof(f102,plain,
( sK0_skl != sK1_skl
& ssItem(sK1_skl)
& ssItem(sK0_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(U,sK0_skl),skolemize(V,sK1_skl)],[f2]) ).
fof(f103,plain,
ssItem(sK0_skl),
inference(cnf_transformation,[status(thm)],[f102]) ).
fof(f104,plain,
ssItem(sK1_skl),
inference(cnf_transformation,[status(thm)],[f102]) ).
fof(f105,plain,
sK0_skl != sK1_skl,
inference(cnf_transformation,[status(thm)],[f102]) ).
fof(f131,plain,
! [U] :
( ! [V] :
( ( segmentP(U,V)
<=> ? [W] :
( ? [X] :
( app(app(W,V),X) = U
& ssList(X) )
& ssList(W) ) )
| ~ ssList(V) )
| ~ ssList(U) ),
inference(pre_NNF_transformation,[status(thm)],[f7]) ).
fof(f132,plain,
! [U] :
( ! [V] :
( ( ( ! [W] :
( ! [X] :
( app(app(W,V),X) != U
| ~ ssList(X) )
| ~ ssList(W) )
| segmentP(U,V) )
& ( ? [W] :
( ? [X] :
( app(app(W,V),X) = U
& ssList(X) )
& ssList(W) )
| ~ segmentP(U,V) ) )
| ~ ssList(V) )
| ~ ssList(U) ),
inference(NNF_transformation,[status(thm)],[f131]) ).
fof(f133,plain,
! [U] :
( ! [V] :
( ( ( ! [W] :
( ! [X] :
( app(app(W,V),X) != U
| ~ ssList(X) )
| ~ ssList(W) )
| segmentP(U,V) )
& ( ( app(app(sK7_skl(V,U),V),sK8_skl(V,U)) = U
& ssList(sK8_skl(V,U))
& ssList(sK7_skl(V,U)) )
| ~ segmentP(U,V) ) )
| ~ ssList(V) )
| ~ ssList(U) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl,sK8_skl]),skolemize(W,sK7_skl(V,U)),skolemize(X,sK8_skl(V,U))],[f132]) ).
fof(f134,plain,
! [X0,X1] :
( ssList(sK7_skl(X1,X0))
| ~ segmentP(X0,X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f133]) ).
fof(f135,plain,
! [X0,X1] :
( ssList(sK8_skl(X1,X0))
| ~ segmentP(X0,X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f133]) ).
fof(f136,plain,
! [X0,X1] :
( app(app(sK7_skl(X1,X0),X1),sK8_skl(X1,X0)) = X0
| ~ segmentP(X0,X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f133]) ).
fof(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(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(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(f248,plain,
! [U] :
( app(nil,U) = U
| ~ ssList(U) ),
inference(pre_NNF_transformation,[status(thm)],[f28]) ).
fof(f249,plain,
! [X0] :
( app(nil,X0) = X0
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f248]) ).
fof(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(f270,plain,
! [X0,X1,X2] :
( memberP(X2,X0)
| memberP(X1,X0)
| ~ memberP(app(X1,X2),X0)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(thm)],[f269]) ).
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(f272,plain,
! [X0,X1,X2] :
( ~ memberP(X2,X0)
| memberP(app(X1,X2),X0)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(thm)],[f269]) ).
fof(f280,plain,
~ singletonP(nil),
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f388,plain,
! [U] :
( app(U,nil) = U
| ~ ssList(U) ),
inference(pre_NNF_transformation,[status(thm)],[f84]) ).
fof(f389,plain,
! [X0] :
( app(X0,nil) = X0
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f388]) ).
fof(f415,plain,
? [U] :
( ? [V] :
( ? [W] :
( ? [X] :
( ( ( segmentP(X,W)
& neq(W,nil) )
| ( nil = W
& nil = X ) )
& ? [Y] :
( ~ memberP(V,Y)
& memberP(U,Y)
& 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] :
( sP0_prd(X,W)
<=> ( nil = W
& nil = X ) ),
introduced(definition,[new_symbols(definition,[sP0_prd])],[]) ).
fof(f417,plain,
? [U] :
( ? [V] :
( ? [W] :
( ? [X] :
( ( ( segmentP(X,W)
& neq(W,nil) )
| sP0_prd(X,W) )
& ? [Y] :
( ~ memberP(V,Y)
& memberP(U,Y)
& ssItem(Y) )
& U = W
& V = X
& ssList(X) )
& ssList(W) )
& ssList(V) )
& ssList(U) ),
inference(formula_renaming,[status(thm)],[f415,f416]) ).
fof(f418,plain,
( ( ( segmentP(sK50_skl,sK49_skl)
& neq(sK49_skl,nil) )
| sP0_prd(sK50_skl,sK49_skl) )
& ~ memberP(sK48_skl,sK51_skl)
& memberP(sK47_skl,sK51_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]),skolemize(U,sK47_skl),skolemize(V,sK48_skl),skolemize(W,sK49_skl),skolemize(X,sK50_skl),skolemize(Y,sK51_skl)],[f417]) ).
fof(f421,plain,
ssList(sK49_skl),
inference(cnf_transformation,[status(thm)],[f418]) ).
fof(f422,plain,
ssList(sK50_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,
ssItem(sK51_skl),
inference(cnf_transformation,[status(thm)],[f418]) ).
fof(f426,plain,
memberP(sK47_skl,sK51_skl),
inference(cnf_transformation,[status(thm)],[f418]) ).
fof(f427,plain,
~ memberP(sK48_skl,sK51_skl),
inference(cnf_transformation,[status(thm)],[f418]) ).
fof(f429,plain,
( segmentP(sK50_skl,sK49_skl)
| sP0_prd(sK50_skl,sK49_skl) ),
inference(cnf_transformation,[status(thm)],[f418]) ).
fof(f430,plain,
! [W,X] :
( ( nil != W
| nil != X
| sP0_prd(X,W) )
& ( ( nil = W
& nil = X )
| ~ sP0_prd(X,W) ) ),
inference(NNF_transformation,[status(thm)],[f416]) ).
fof(f431,plain,
( ! [W,X] :
( nil != W
| nil != X
| sP0_prd(X,W) )
& ! [W,X] :
( ( nil = W
& nil = X )
| ~ sP0_prd(X,W) ) ),
inference(miniscoping,[status(thm)],[f430]) ).
fof(f432,plain,
! [X0,X1] :
( nil = X0
| ~ sP0_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f431]) ).
fof(f433,plain,
! [X0,X1] :
( nil = X1
| ~ sP0_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f431]) ).
fof(f435,definition,
( sQ0_spl
<=> sP0_prd(sK50_skl,sK49_skl) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f436,plain,
( ~ sQ0_spl
| sP0_prd(sK50_skl,sK49_skl) ),
inference(component_clause,[status(thm)],[f435]) ).
fof(f442,definition,
( sQ2_spl
<=> segmentP(sK50_skl,sK49_skl) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f443,plain,
( ~ sQ2_spl
| segmentP(sK50_skl,sK49_skl) ),
inference(component_clause,[status(thm)],[f442]) ).
fof(f445,plain,
( sQ2_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f429,f435,f442]) ).
fof(f485,plain,
memberP(sK49_skl,sK51_skl),
inference(forward_demodulation,[status(thm)],[f424,f426]) ).
fof(f487,definition,
( sQ3_spl
<=> ssList(sK49_skl) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f489,plain,
( sQ3_spl
| ~ ssList(sK49_skl) ),
inference(component_clause,[status(thm)],[f487]) ).
fof(f490,definition,
( sQ4_spl
<=> ssItem(sK51_skl) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f492,plain,
( sQ4_spl
| ~ ssItem(sK51_skl) ),
inference(component_clause,[status(thm)],[f490]) ).
fof(f497,plain,
~ memberP(sK50_skl,sK51_skl),
inference(forward_demodulation,[status(thm)],[f423,f427]) ).
fof(f498,plain,
( ~ sQ0_spl
| nil = sK50_skl ),
inference(resolution,[status(thm)],[f432,f436]) ).
fof(f500,plain,
( ~ sQ0_spl
| sP0_prd(nil,sK49_skl) ),
inference(backward_demodulation,[status(thm)],[f498,f436]) ).
fof(f501,plain,
( ~ sQ0_spl
| ~ memberP(nil,sK51_skl) ),
inference(backward_demodulation,[status(thm)],[f498,f497]) ).
fof(f505,plain,
( ~ sQ0_spl
| nil = sK49_skl ),
inference(resolution,[status(thm)],[f500,f433]) ).
fof(f508,plain,
( ~ sQ0_spl
| memberP(nil,sK51_skl) ),
inference(backward_demodulation,[status(thm)],[f505,f485]) ).
fof(f514,plain,
( ~ sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f508,f501]) ).
fof(f515,plain,
~ sQ0_spl,
inference(contradiction_clause,[status(thm)],[f514]) ).
fof(f525,plain,
( sQ3_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f489,f421]) ).
fof(f526,plain,
sQ3_spl,
inference(contradiction_clause,[status(thm)],[f525]) ).
fof(f527,plain,
( sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f492,f425]) ).
fof(f528,plain,
sQ4_spl,
inference(contradiction_clause,[status(thm)],[f527]) ).
fof(f552,definition,
( sQ10_spl
<=> ssList(sK50_skl) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f554,plain,
( sQ10_spl
| ~ ssList(sK50_skl) ),
inference(component_clause,[status(thm)],[f552]) ).
fof(f559,plain,
( sQ10_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f554,f422]) ).
fof(f560,plain,
sQ10_spl,
inference(contradiction_clause,[status(thm)],[f559]) ).
fof(f563,definition,
( sQ12_spl
<=> ssList(nil) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f565,plain,
( sQ12_spl
| ~ ssList(nil) ),
inference(component_clause,[status(thm)],[f563]) ).
fof(f571,plain,
( sQ12_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f565,f223]) ).
fof(f572,plain,
sQ12_spl,
inference(contradiction_clause,[status(thm)],[f571]) ).
fof(f575,definition,
( sQ14_spl
<=> ssItem(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f577,plain,
( sQ14_spl
| ~ ssItem(sK0_skl) ),
inference(component_clause,[status(thm)],[f575]) ).
fof(f586,plain,
( sQ14_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f577,f103]) ).
fof(f587,plain,
sQ14_spl,
inference(contradiction_clause,[status(thm)],[f586]) ).
fof(f589,definition,
! [X0] :
( sQ17_spl
<=> ( memberP(app(X0,sK49_skl),sK51_skl)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f590,plain,
! [X0] :
( ~ sQ17_spl
| memberP(app(X0,sK49_skl),sK51_skl)
| ~ ssList(X0) ),
inference(component_clause,[status(thm)],[f589]) ).
fof(f616,plain,
app(nil,nil) = nil,
inference(resolution,[status(thm)],[f249,f223]) ).
fof(f659,plain,
( ~ sQ2_spl
| app(app(sK7_skl(sK49_skl,sK50_skl),sK49_skl),sK8_skl(sK49_skl,sK50_skl)) = sK50_skl
| ~ ssList(sK49_skl)
| ~ ssList(sK50_skl) ),
inference(resolution,[status(thm)],[f136,f443]) ).
fof(f662,definition,
( sQ28_spl
<=> app(app(sK7_skl(sK49_skl,sK50_skl),sK49_skl),sK8_skl(sK49_skl,sK50_skl)) = sK50_skl ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f663,plain,
( ~ sQ28_spl
| app(app(sK7_skl(sK49_skl,sK50_skl),sK49_skl),sK8_skl(sK49_skl,sK50_skl)) = sK50_skl ),
inference(component_clause,[status(thm)],[f662]) ).
fof(f665,plain,
( ~ sQ2_spl
| sQ28_spl
| ~ sQ3_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f659,f552,f487,f662,f442]) ).
fof(f811,plain,
app(sK49_skl,nil) = sK49_skl,
inference(resolution,[status(thm)],[f389,f421]) ).
fof(f938,definition,
( sQ74_spl
<=> sK49_skl = sK50_skl ),
introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition]) ).
fof(f939,plain,
( ~ sQ74_spl
| sK49_skl = sK50_skl ),
inference(component_clause,[status(thm)],[f938]) ).
fof(f962,plain,
( ~ sQ74_spl
| ~ memberP(sK49_skl,sK51_skl) ),
inference(backward_demodulation,[status(thm)],[f939,f497]) ).
fof(f971,plain,
( ~ sQ74_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f962,f485]) ).
fof(f972,plain,
~ sQ74_spl,
inference(contradiction_clause,[status(thm)],[f971]) ).
fof(f1017,definition,
( sQ79_spl
<=> ssItem(sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition]) ).
fof(f1019,plain,
( sQ79_spl
| ~ ssItem(sK1_skl) ),
inference(component_clause,[status(thm)],[f1017]) ).
fof(f1028,plain,
( sQ79_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1019,f104]) ).
fof(f1029,plain,
sQ79_spl,
inference(contradiction_clause,[status(thm)],[f1028]) ).
fof(f1063,plain,
! [X0,X1] :
( ~ sQ17_spl
| memberP(app(app(X0,sK49_skl),X1),sK51_skl)
| ~ ssList(X1)
| ~ ssList(app(X0,sK49_skl))
| ~ ssItem(sK51_skl)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f590,f271]) ).
fof(f1075,definition,
! [X0,X1] :
( sQ84_spl
<=> ( memberP(app(app(X0,sK49_skl),X1),sK51_skl)
| ~ ssList(X1)
| ~ ssList(app(X0,sK49_skl))
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition]) ).
fof(f1076,plain,
! [X0,X1] :
( ~ sQ84_spl
| memberP(app(app(X0,sK49_skl),X1),sK51_skl)
| ~ ssList(X1)
| ~ ssList(app(X0,sK49_skl))
| ~ ssList(X0) ),
inference(component_clause,[status(thm)],[f1075]) ).
fof(f1078,plain,
( ~ sQ17_spl
| ~ sQ4_spl
| sQ84_spl ),
inference(split_clause,[status(thm)],[f1063,f1075,f490,f589]) ).
fof(f1137,definition,
( sQ93_spl
<=> ssList(sK7_skl(sK49_skl,sK50_skl)) ),
introduced(definition,[new_symbols(definition,[sQ93_spl])],[split_symbol_definition]) ).
fof(f1139,plain,
( sQ93_spl
| ~ ssList(sK7_skl(sK49_skl,sK50_skl)) ),
inference(component_clause,[status(thm)],[f1137]) ).
fof(f1140,definition,
( sQ94_spl
<=> ssList(sK8_skl(sK49_skl,sK50_skl)) ),
introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition]) ).
fof(f1142,plain,
( sQ94_spl
| ~ ssList(sK8_skl(sK49_skl,sK50_skl)) ),
inference(component_clause,[status(thm)],[f1140]) ).
fof(f1166,plain,
( sQ94_spl
| ~ segmentP(sK50_skl,sK49_skl)
| ~ ssList(sK49_skl)
| ~ ssList(sK50_skl) ),
inference(resolution,[status(thm)],[f1142,f135]) ).
fof(f1167,plain,
( sQ94_spl
| ~ sQ2_spl
| ~ sQ3_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f1166,f552,f487,f442,f1140]) ).
fof(f1382,definition,
( sQ132_spl
<=> ssList(cons(sK1_skl,sK49_skl)) ),
introduced(definition,[new_symbols(definition,[sQ132_spl])],[split_symbol_definition]) ).
fof(f1384,plain,
( sQ132_spl
| ~ ssList(cons(sK1_skl,sK49_skl)) ),
inference(component_clause,[status(thm)],[f1382]) ).
fof(f1455,definition,
( sQ143_spl
<=> ssList(cons(sK0_skl,sK49_skl)) ),
introduced(definition,[new_symbols(definition,[sQ143_spl])],[split_symbol_definition]) ).
fof(f1457,plain,
( sQ143_spl
| ~ ssList(cons(sK0_skl,sK49_skl)) ),
inference(component_clause,[status(thm)],[f1455]) ).
fof(f1952,plain,
! [X0] :
( cons(sK51_skl,X0) != X0
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f225,f425]) ).
fof(f1953,plain,
! [X0] :
( cons(sK1_skl,X0) != X0
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f225,f104]) ).
fof(f1954,plain,
! [X0] :
( cons(sK0_skl,X0) != X0
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f225,f103]) ).
fof(f1961,plain,
cons(sK51_skl,sK50_skl) != sK50_skl,
inference(resolution,[status(thm)],[f1952,f422]) ).
fof(f1975,plain,
cons(sK51_skl,sK49_skl) != sK49_skl,
inference(resolution,[status(thm)],[f1952,f421]) ).
fof(f1980,plain,
cons(sK51_skl,nil) != nil,
inference(resolution,[status(thm)],[f1952,f223]) ).
fof(f2075,plain,
cons(sK1_skl,sK50_skl) != sK50_skl,
inference(resolution,[status(thm)],[f1953,f422]) ).
fof(f2089,plain,
cons(sK1_skl,sK49_skl) != sK49_skl,
inference(resolution,[status(thm)],[f1953,f421]) ).
fof(f2094,plain,
cons(sK1_skl,nil) != nil,
inference(resolution,[status(thm)],[f1953,f223]) ).
fof(f2095,plain,
cons(sK0_skl,sK50_skl) != sK50_skl,
inference(resolution,[status(thm)],[f1954,f422]) ).
fof(f2109,plain,
cons(sK0_skl,sK49_skl) != sK49_skl,
inference(resolution,[status(thm)],[f1954,f421]) ).
fof(f2114,plain,
cons(sK0_skl,nil) != nil,
inference(resolution,[status(thm)],[f1954,f223]) ).
fof(f2273,plain,
! [X0] :
( ssList(cons(sK1_skl,X0))
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f222,f104]) ).
fof(f2274,plain,
! [X0] :
( ssList(cons(sK0_skl,X0))
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f222,f103]) ).
fof(f2548,plain,
! [X0] :
( nil != cons(sK51_skl,X0)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f235,f425]) ).
fof(f2807,plain,
! [X0] :
( ssList(app(X0,sK49_skl))
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f245,f421]) ).
fof(f2848,plain,
! [X0] :
( ssList(app(X0,sK50_skl))
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f422,f245]) ).
fof(f3025,definition,
( sQ280_spl
<=> nil = cons(sK51_skl,nil) ),
introduced(definition,[new_symbols(definition,[sQ280_spl])],[split_symbol_definition]) ).
fof(f3026,plain,
( ~ sQ280_spl
| nil = cons(sK51_skl,nil) ),
inference(component_clause,[status(thm)],[f3025]) ).
fof(f3032,plain,
( ~ sQ280_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3026,f1980]) ).
fof(f3033,plain,
~ sQ280_spl,
inference(contradiction_clause,[status(thm)],[f3032]) ).
fof(f3176,plain,
nil != cons(sK51_skl,sK50_skl),
inference(resolution,[status(thm)],[f2548,f422]) ).
fof(f3412,definition,
! [X0] :
( sQ312_spl
<=> ( ~ ssItem(X0)
| ~ ssItem(X0)
| ~ ssItem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ312_spl])],[split_symbol_definition]) ).
fof(f3413,plain,
! [X0] :
( ~ sQ312_spl
| ~ ssItem(X0)
| ~ ssItem(X0)
| ~ ssItem(X0) ),
inference(component_clause,[status(thm)],[f3412]) ).
fof(f3429,plain,
! [X0] :
( ~ sQ312_spl
| ~ ssItem(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f3413]) ).
fof(f3495,plain,
( ~ sQ312_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f104,f3429]) ).
fof(f3500,plain,
~ sQ312_spl,
inference(contradiction_clause,[status(thm)],[f3495]) ).
fof(f3695,plain,
! [X0,X1] :
( ~ memberP(X1,sK51_skl)
| memberP(app(X0,X1),sK51_skl)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f272,f425]) ).
fof(f3698,plain,
! [X0,X1] :
( ~ memberP(X0,sK51_skl)
| memberP(app(X0,X1),sK51_skl)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f271,f425]) ).
fof(f3811,definition,
! [X0] :
( sQ344_spl
<=> ( memberP(X0,sK51_skl)
| ~ memberP(app(X0,sK50_skl),sK51_skl)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ344_spl])],[split_symbol_definition]) ).
fof(f3812,plain,
! [X0] :
( ~ sQ344_spl
| memberP(X0,sK51_skl)
| ~ memberP(app(X0,sK50_skl),sK51_skl)
| ~ ssList(X0) ),
inference(component_clause,[status(thm)],[f3811]) ).
fof(f4331,plain,
ssList(cons(sK1_skl,sK50_skl)),
inference(resolution,[status(thm)],[f2273,f422]) ).
fof(f4332,plain,
ssList(cons(sK1_skl,sK49_skl)),
inference(resolution,[status(thm)],[f2273,f421]) ).
fof(f4343,plain,
ssList(cons(sK1_skl,nil)),
inference(resolution,[status(thm)],[f2273,f223]) ).
fof(f4344,plain,
( sQ132_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4332,f1384]) ).
fof(f4345,plain,
sQ132_spl,
inference(contradiction_clause,[status(thm)],[f4344]) ).
fof(f4434,definition,
( sQ384_spl
<=> nil = cons(sK1_skl,nil) ),
introduced(definition,[new_symbols(definition,[sQ384_spl])],[split_symbol_definition]) ).
fof(f4435,plain,
( ~ sQ384_spl
| nil = cons(sK1_skl,nil) ),
inference(component_clause,[status(thm)],[f4434]) ).
fof(f4446,plain,
( ~ sQ384_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4435,f2094]) ).
fof(f4447,plain,
~ sQ384_spl,
inference(contradiction_clause,[status(thm)],[f4446]) ).
fof(f4669,plain,
ssList(cons(sK0_skl,sK50_skl)),
inference(resolution,[status(thm)],[f2274,f422]) ).
fof(f4670,plain,
ssList(cons(sK0_skl,sK49_skl)),
inference(resolution,[status(thm)],[f2274,f421]) ).
fof(f4684,plain,
ssList(cons(sK0_skl,nil)),
inference(resolution,[status(thm)],[f2274,f223]) ).
fof(f4685,plain,
( sQ143_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4670,f1457]) ).
fof(f4686,plain,
sQ143_spl,
inference(contradiction_clause,[status(thm)],[f4685]) ).
fof(f4781,definition,
( sQ405_spl
<=> nil = cons(sK0_skl,nil) ),
introduced(definition,[new_symbols(definition,[sQ405_spl])],[split_symbol_definition]) ).
fof(f4782,plain,
( ~ sQ405_spl
| nil = cons(sK0_skl,nil) ),
inference(component_clause,[status(thm)],[f4781]) ).
fof(f4793,plain,
( ~ sQ405_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4782,f2114]) ).
fof(f4794,plain,
~ sQ405_spl,
inference(contradiction_clause,[status(thm)],[f4793]) ).
fof(f4972,plain,
ssList(app(sK49_skl,sK49_skl)),
inference(resolution,[status(thm)],[f2807,f421]) ).
fof(f5263,plain,
ssList(app(sK50_skl,sK50_skl)),
inference(resolution,[status(thm)],[f2848,f422]) ).
fof(f5264,plain,
ssList(app(sK49_skl,sK50_skl)),
inference(resolution,[status(thm)],[f2848,f421]) ).
fof(f5487,definition,
( sQ447_spl
<=> nil = cons(sK51_skl,sK50_skl) ),
introduced(definition,[new_symbols(definition,[sQ447_spl])],[split_symbol_definition]) ).
fof(f5488,plain,
( ~ sQ447_spl
| nil = cons(sK51_skl,sK50_skl) ),
inference(component_clause,[status(thm)],[f5487]) ).
fof(f5511,plain,
( ~ sQ447_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5488,f3176]) ).
fof(f5512,plain,
~ sQ447_spl,
inference(contradiction_clause,[status(thm)],[f5511]) ).
fof(f6259,definition,
( sQ517_spl
<=> memberP(sK50_skl,sK51_skl) ),
introduced(definition,[new_symbols(definition,[sQ517_spl])],[split_symbol_definition]) ).
fof(f6539,definition,
( sQ544_spl
<=> ssList(cons(sK1_skl,sK50_skl)) ),
introduced(definition,[new_symbols(definition,[sQ544_spl])],[split_symbol_definition]) ).
fof(f6541,plain,
( sQ544_spl
| ~ ssList(cons(sK1_skl,sK50_skl)) ),
inference(component_clause,[status(thm)],[f6539]) ).
fof(f6552,plain,
( sQ544_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6541,f4331]) ).
fof(f6553,plain,
sQ544_spl,
inference(contradiction_clause,[status(thm)],[f6552]) ).
fof(f6645,definition,
( sQ559_spl
<=> ssList(cons(sK1_skl,nil)) ),
introduced(definition,[new_symbols(definition,[sQ559_spl])],[split_symbol_definition]) ).
fof(f6647,plain,
( sQ559_spl
| ~ ssList(cons(sK1_skl,nil)) ),
inference(component_clause,[status(thm)],[f6645]) ).
fof(f6658,plain,
( sQ559_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6647,f4343]) ).
fof(f6659,plain,
sQ559_spl,
inference(contradiction_clause,[status(thm)],[f6658]) ).
fof(f6737,definition,
( sQ568_spl
<=> ssList(cons(sK0_skl,sK50_skl)) ),
introduced(definition,[new_symbols(definition,[sQ568_spl])],[split_symbol_definition]) ).
fof(f6739,plain,
( sQ568_spl
| ~ ssList(cons(sK0_skl,sK50_skl)) ),
inference(component_clause,[status(thm)],[f6737]) ).
fof(f6750,plain,
( sQ568_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6739,f4669]) ).
fof(f6751,plain,
sQ568_spl,
inference(contradiction_clause,[status(thm)],[f6750]) ).
fof(f6772,definition,
( sQ573_spl
<=> ssList(cons(sK0_skl,nil)) ),
introduced(definition,[new_symbols(definition,[sQ573_spl])],[split_symbol_definition]) ).
fof(f6774,plain,
( sQ573_spl
| ~ ssList(cons(sK0_skl,nil)) ),
inference(component_clause,[status(thm)],[f6772]) ).
fof(f6785,plain,
( sQ573_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6774,f4684]) ).
fof(f6786,plain,
sQ573_spl,
inference(contradiction_clause,[status(thm)],[f6785]) ).
fof(f6850,plain,
( ~ sQ344_spl
| ~ memberP(app(sK50_skl,sK50_skl),sK51_skl)
| ~ ssList(sK50_skl) ),
inference(resolution,[status(thm)],[f3812,f497]) ).
fof(f6853,definition,
( sQ586_spl
<=> memberP(app(sK50_skl,sK50_skl),sK51_skl) ),
introduced(definition,[new_symbols(definition,[sQ586_spl])],[split_symbol_definition]) ).
fof(f6855,plain,
( sQ586_spl
| ~ memberP(app(sK50_skl,sK50_skl),sK51_skl) ),
inference(component_clause,[status(thm)],[f6853]) ).
fof(f6856,plain,
( ~ sQ344_spl
| ~ sQ586_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f6850,f552,f6853,f3811]) ).
fof(f7010,plain,
( sQ586_spl
| ~ memberP(sK50_skl,sK51_skl)
| ~ ssList(sK50_skl)
| ~ ssList(sK50_skl) ),
inference(resolution,[status(thm)],[f6855,f3698]) ).
fof(f7015,plain,
( sQ586_spl
| ~ sQ517_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f7010,f552,f6259,f6853]) ).
fof(f7017,definition,
( sQ595_spl
<=> ssList(app(sK50_skl,sK50_skl)) ),
introduced(definition,[new_symbols(definition,[sQ595_spl])],[split_symbol_definition]) ).
fof(f7019,plain,
( sQ595_spl
| ~ ssList(app(sK50_skl,sK50_skl)) ),
inference(component_clause,[status(thm)],[f7017]) ).
fof(f7032,plain,
( sQ595_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7019,f5263]) ).
fof(f7033,plain,
sQ595_spl,
inference(contradiction_clause,[status(thm)],[f7032]) ).
fof(f7801,definition,
( sQ699_spl
<=> app(sK50_skl,sK50_skl) = app(sK50_skl,sK50_skl) ),
introduced(definition,[new_symbols(definition,[sQ699_spl])],[split_symbol_definition]) ).
fof(f7803,plain,
( sQ699_spl
| app(sK50_skl,sK50_skl) != app(sK50_skl,sK50_skl) ),
inference(component_clause,[status(thm)],[f7801]) ).
fof(f7812,definition,
( sQ702_spl
<=> sK50_skl = cons(sK0_skl,sK50_skl) ),
introduced(definition,[new_symbols(definition,[sQ702_spl])],[split_symbol_definition]) ).
fof(f7813,plain,
( ~ sQ702_spl
| sK50_skl = cons(sK0_skl,sK50_skl) ),
inference(component_clause,[status(thm)],[f7812]) ).
fof(f7833,definition,
( sQ708_spl
<=> sK50_skl = cons(sK1_skl,sK50_skl) ),
introduced(definition,[new_symbols(definition,[sQ708_spl])],[split_symbol_definition]) ).
fof(f7834,plain,
( ~ sQ708_spl
| sK50_skl = cons(sK1_skl,sK50_skl) ),
inference(component_clause,[status(thm)],[f7833]) ).
fof(f7854,definition,
( sQ714_spl
<=> sK50_skl = cons(sK51_skl,sK50_skl) ),
introduced(definition,[new_symbols(definition,[sQ714_spl])],[split_symbol_definition]) ).
fof(f7855,plain,
( ~ sQ714_spl
| sK50_skl = cons(sK51_skl,sK50_skl) ),
inference(component_clause,[status(thm)],[f7854]) ).
fof(f8008,definition,
( sQ731_spl
<=> app(sK49_skl,sK49_skl) = app(sK49_skl,sK49_skl) ),
introduced(definition,[new_symbols(definition,[sQ731_spl])],[split_symbol_definition]) ).
fof(f8010,plain,
( sQ731_spl
| app(sK49_skl,sK49_skl) != app(sK49_skl,sK49_skl) ),
inference(component_clause,[status(thm)],[f8008]) ).
fof(f8022,definition,
( sQ735_spl
<=> sK49_skl = cons(sK0_skl,sK49_skl) ),
introduced(definition,[new_symbols(definition,[sQ735_spl])],[split_symbol_definition]) ).
fof(f8023,plain,
( ~ sQ735_spl
| sK49_skl = cons(sK0_skl,sK49_skl) ),
inference(component_clause,[status(thm)],[f8022]) ).
fof(f8043,definition,
( sQ741_spl
<=> sK49_skl = cons(sK1_skl,sK49_skl) ),
introduced(definition,[new_symbols(definition,[sQ741_spl])],[split_symbol_definition]) ).
fof(f8044,plain,
( ~ sQ741_spl
| sK49_skl = cons(sK1_skl,sK49_skl) ),
inference(component_clause,[status(thm)],[f8043]) ).
fof(f8064,definition,
( sQ747_spl
<=> sK49_skl = cons(sK51_skl,sK49_skl) ),
introduced(definition,[new_symbols(definition,[sQ747_spl])],[split_symbol_definition]) ).
fof(f8065,plain,
( ~ sQ747_spl
| sK49_skl = cons(sK51_skl,sK49_skl) ),
inference(component_clause,[status(thm)],[f8064]) ).
fof(f8303,definition,
( sQ781_spl
<=> nil = app(nil,nil) ),
introduced(definition,[new_symbols(definition,[sQ781_spl])],[split_symbol_definition]) ).
fof(f8305,plain,
( sQ781_spl
| nil != app(nil,nil) ),
inference(component_clause,[status(thm)],[f8303]) ).
fof(f8819,plain,
( ~ sQ714_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7855,f1961]) ).
fof(f8820,plain,
~ sQ714_spl,
inference(contradiction_clause,[status(thm)],[f8819]) ).
fof(f8821,plain,
( ~ sQ708_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7834,f2075]) ).
fof(f8822,plain,
~ sQ708_spl,
inference(contradiction_clause,[status(thm)],[f8821]) ).
fof(f8823,plain,
( ~ sQ702_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7813,f2095]) ).
fof(f8824,plain,
~ sQ702_spl,
inference(contradiction_clause,[status(thm)],[f8823]) ).
fof(f10341,plain,
( sQ781_spl
| nil != nil ),
inference(forward_demodulation,[status(thm)],[f616,f8305]) ).
fof(f10342,plain,
( sQ781_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f10341]) ).
fof(f10343,plain,
sQ781_spl,
inference(contradiction_clause,[status(thm)],[f10342]) ).
fof(f10346,plain,
( ~ sQ747_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8065,f1975]) ).
fof(f10347,plain,
~ sQ747_spl,
inference(contradiction_clause,[status(thm)],[f10346]) ).
fof(f10348,plain,
( ~ sQ741_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8044,f2089]) ).
fof(f10349,plain,
~ sQ741_spl,
inference(contradiction_clause,[status(thm)],[f10348]) ).
fof(f10350,plain,
( sQ731_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f8010]) ).
fof(f10351,plain,
sQ731_spl,
inference(contradiction_clause,[status(thm)],[f10350]) ).
fof(f10355,plain,
( sQ699_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f7803]) ).
fof(f10356,plain,
sQ699_spl,
inference(contradiction_clause,[status(thm)],[f10355]) ).
fof(f13590,plain,
( ~ sQ735_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8023,f2109]) ).
fof(f13591,plain,
~ sQ735_spl,
inference(contradiction_clause,[status(thm)],[f13590]) ).
fof(f15751,definition,
( sQ1474_spl
<=> sK0_skl = sK1_skl ),
introduced(definition,[new_symbols(definition,[sQ1474_spl])],[split_symbol_definition]) ).
fof(f15752,plain,
( ~ sQ1474_spl
| sK0_skl = sK1_skl ),
inference(component_clause,[status(thm)],[f15751]) ).
fof(f15755,plain,
( ~ sQ1474_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f15752,f105]) ).
fof(f15756,plain,
~ sQ1474_spl,
inference(contradiction_clause,[status(thm)],[f15755]) ).
fof(f17305,plain,
! [X0] :
( memberP(app(X0,sK49_skl),sK51_skl)
| ~ ssList(sK49_skl)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f3695,f485]) ).
fof(f17314,plain,
( ~ sQ3_spl
| sQ17_spl ),
inference(split_clause,[status(thm)],[f17305,f589,f487]) ).
fof(f21575,definition,
( sQ2204_spl
<=> ssList(app(sK49_skl,sK49_skl)) ),
introduced(definition,[new_symbols(definition,[sQ2204_spl])],[split_symbol_definition]) ).
fof(f21577,plain,
( sQ2204_spl
| ~ ssList(app(sK49_skl,sK49_skl)) ),
inference(component_clause,[status(thm)],[f21575]) ).
fof(f21588,definition,
( sQ2208_spl
<=> ssList(app(sK49_skl,sK50_skl)) ),
introduced(definition,[new_symbols(definition,[sQ2208_spl])],[split_symbol_definition]) ).
fof(f21590,plain,
( sQ2208_spl
| ~ ssList(app(sK49_skl,sK50_skl)) ),
inference(component_clause,[status(thm)],[f21588]) ).
fof(f21603,plain,
( sQ2204_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f21577,f4972]) ).
fof(f21604,plain,
sQ2204_spl,
inference(contradiction_clause,[status(thm)],[f21603]) ).
fof(f21605,plain,
( sQ2208_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f21590,f5264]) ).
fof(f21606,plain,
sQ2208_spl,
inference(contradiction_clause,[status(thm)],[f21605]) ).
fof(f23097,plain,
! [X0,X1] :
( ~ sQ84_spl
| memberP(app(app(X0,sK49_skl),X1),sK51_skl)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1076,f2807]) ).
fof(f23234,plain,
( ~ sQ28_spl
| ~ sQ84_spl
| memberP(sK50_skl,sK51_skl)
| ~ ssList(sK8_skl(sK49_skl,sK50_skl))
| ~ ssList(sK7_skl(sK49_skl,sK50_skl)) ),
inference(paramodulation,[status(thm)],[f663,f23097]) ).
fof(f23240,plain,
( ~ sQ28_spl
| ~ sQ84_spl
| sQ517_spl
| ~ sQ94_spl
| ~ sQ93_spl ),
inference(split_clause,[status(thm)],[f23234,f1137,f1140,f6259,f1075,f662]) ).
fof(f24147,definition,
( sQ2509_spl
<=> ssList(app(sK49_skl,nil)) ),
introduced(definition,[new_symbols(definition,[sQ2509_spl])],[split_symbol_definition]) ).
fof(f24149,plain,
( sQ2509_spl
| ~ ssList(app(sK49_skl,nil)) ),
inference(component_clause,[status(thm)],[f24147]) ).
fof(f24193,plain,
( sQ2509_spl
| ~ ssList(sK49_skl) ),
inference(forward_demodulation,[status(thm)],[f811,f24149]) ).
fof(f24194,plain,
( sQ2509_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f24193,f421]) ).
fof(f24195,plain,
sQ2509_spl,
inference(contradiction_clause,[status(thm)],[f24194]) ).
fof(f24249,definition,
( sQ2514_spl
<=> singletonP(nil) ),
introduced(definition,[new_symbols(definition,[sQ2514_spl])],[split_symbol_definition]) ).
fof(f24250,plain,
( ~ sQ2514_spl
| singletonP(nil) ),
inference(component_clause,[status(thm)],[f24249]) ).
fof(f24440,plain,
( ~ sQ2514_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f24250,f280]) ).
fof(f24441,plain,
~ sQ2514_spl,
inference(contradiction_clause,[status(thm)],[f24440]) ).
fof(f29978,plain,
! [X0,X1] :
( memberP(X1,sK51_skl)
| memberP(X0,sK51_skl)
| ~ memberP(app(X0,X1),sK51_skl)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f270,f425]) ).
fof(f31370,plain,
! [X0] :
( memberP(X0,sK51_skl)
| ~ memberP(app(X0,sK50_skl),sK51_skl)
| ~ ssList(sK50_skl)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f29978,f497]) ).
fof(f31377,plain,
( ~ sQ10_spl
| sQ344_spl ),
inference(split_clause,[status(thm)],[f31370,f3811,f552]) ).
fof(f33652,plain,
( sQ93_spl
| ~ segmentP(sK50_skl,sK49_skl)
| ~ ssList(sK49_skl)
| ~ ssList(sK50_skl) ),
inference(resolution,[status(thm)],[f1139,f134]) ).
fof(f33653,plain,
( sQ93_spl
| ~ sQ2_spl
| ~ sQ3_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f33652,f552,f487,f442,f1137]) ).
fof(f33654,plain,
$false,
inference(sat_refutation,[status(thm)],[f445,f515,f526,f528,f560,f572,f587,f665,f972,f1029,f1078,f1167,f3033,f3500,f4345,f4447,f4686,f4794,f5512,f6553,f6659,f6751,f6786,f6856,f7015,f7033,f8820,f8822,f8824,f10343,f10347,f10349,f10351,f10356,f13591,f15756,f17314,f21604,f21606,f23240,f24195,f24441,f31377,f33653]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWC394+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.15/0.64 % Computer : n006.cluster.edu
% 0.15/0.64 % Model : x86_64 x86_64
% 0.15/0.64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.64 % Memory : 8046.5625MB
% 0.15/0.64 % OS : Linux 6.8.0-71-generic
% 0.15/0.64 % CPULimit : 300
% 0.15/0.64 % WCLimit : 300
% 0.15/0.64 % DateTime : Mon Sep 21 08:20:28 UTC 2026
% 0.15/0.64 % CPUTime :
% 0.21/0.67 % Drodi V4.1.1
% 269.20/34.70 % Refutation found
% 269.20/34.70 % SZS status Theorem for theBenchmark: Theorem is valid
% 269.20/34.70 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 12.24/34.94 % Elapsed time: 34.285423 seconds
% 12.24/34.94 % CPU time: 270.126642 seconds
% 12.24/34.94 % Total memory used: 520.216 MB
% 12.24/34.94 % Net memory used: 480.423 MB
%------------------------------------------------------------------------------