%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWC401+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 : n012.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 02:41:05 PM UTC 2026
% Result : Theorem 166.41s 21.35s
% Output : CNFRefutation 166.41s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 63
% Syntax : Number of formulae : 307 ( 85 unt; 50 def)
% Number of atoms : 706 ( 116 equ)
% Maximal formula atoms : 16 ( 2 avg)
% Number of connectives : 726 ( 327 ~; 273 |; 46 &)
% ( 54 <=>; 26 =>; 0 <=; 0 <~>)
% Maximal formula depth : 20 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 59 ( 57 usr; 51 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 8 con; 0-2 aty)
% Number of variables : 136 ( 121 !; 15 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
? [U] :
( ? [V] :
( U != V
& ssItem(V) )
& ssItem(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ( segmentP(U,V)
<=> ? [W] :
( ? [X] :
( app(app(W,V),X) = U
& ssList(X) )
& ssList(W) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(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(f21,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssItem(V)
=> nil != cons(V,U) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f26,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ssList(app(U,V)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f28,axiom,
! [U] :
( ssList(U)
=> app(nil,U) = U ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(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/sandbox2/benchmark/theBenchmark.p') ).
fof(f38,axiom,
! [U] :
( ssItem(U)
=> ~ memberP(nil,U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f39,axiom,
~ singletonP(nil),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f84,axiom,
! [U] :
( ssList(U)
=> app(U,nil) = U ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f96,conjecture,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ! [W] :
( ssList(W)
=> ! [X] :
( ssList(X)
=> ( ! [Z] :
( ssItem(Z)
=> ( memberP(V,Z)
| ~ memberP(U,Z) ) )
| ? [Y] :
( totalorderedP(Y)
& segmentP(Y,W)
& segmentP(X,Y)
& neq(W,Y)
& ssList(Y) )
| ~ totalorderedP(W)
| ~ segmentP(X,W)
| 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)
=> ( ! [Z] :
( ssItem(Z)
=> ( memberP(V,Z)
| ~ memberP(U,Z) ) )
| ? [Y] :
( totalorderedP(Y)
& segmentP(Y,W)
& segmentP(X,Y)
& neq(W,Y)
& ssList(Y) )
| ~ totalorderedP(W)
| ~ segmentP(X,W)
| 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(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(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] :
( ? [Z] :
( ~ memberP(V,Z)
& memberP(U,Z)
& ssItem(Z) )
& ! [Y] :
( ~ totalorderedP(Y)
| ~ segmentP(Y,W)
| ~ segmentP(X,Y)
| ~ neq(W,Y)
| ~ ssList(Y) )
& totalorderedP(W)
& segmentP(X,W)
& U = W
& V = X
& ssList(X) )
& ssList(W) )
& ssList(V) )
& ssList(U) ),
inference(pre_NNF_transformation,[status(thm)],[f97]) ).
fof(f416,plain,
( ~ memberP(sK48_skl,sK51_skl)
& memberP(sK47_skl,sK51_skl)
& ssItem(sK51_skl)
& ! [Y] :
( ~ totalorderedP(Y)
| ~ segmentP(Y,sK49_skl)
| ~ segmentP(sK50_skl,Y)
| ~ neq(sK49_skl,Y)
| ~ ssList(Y) )
& totalorderedP(sK49_skl)
& segmentP(sK50_skl,sK49_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(Z,sK51_skl)],[f415]) ).
fof(f419,plain,
ssList(sK49_skl),
inference(cnf_transformation,[status(thm)],[f416]) ).
fof(f420,plain,
ssList(sK50_skl),
inference(cnf_transformation,[status(thm)],[f416]) ).
fof(f421,plain,
sK48_skl = sK50_skl,
inference(cnf_transformation,[status(thm)],[f416]) ).
fof(f422,plain,
sK47_skl = sK49_skl,
inference(cnf_transformation,[status(thm)],[f416]) ).
fof(f423,plain,
segmentP(sK50_skl,sK49_skl),
inference(cnf_transformation,[status(thm)],[f416]) ).
fof(f424,plain,
totalorderedP(sK49_skl),
inference(cnf_transformation,[status(thm)],[f416]) ).
fof(f426,plain,
ssItem(sK51_skl),
inference(cnf_transformation,[status(thm)],[f416]) ).
fof(f427,plain,
memberP(sK47_skl,sK51_skl),
inference(cnf_transformation,[status(thm)],[f416]) ).
fof(f428,plain,
~ memberP(sK48_skl,sK51_skl),
inference(cnf_transformation,[status(thm)],[f416]) ).
fof(f467,plain,
memberP(sK49_skl,sK51_skl),
inference(forward_demodulation,[status(thm)],[f422,f427]) ).
fof(f469,definition,
( sQ0_spl
<=> ssList(sK49_skl) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f471,plain,
( sQ0_spl
| ~ ssList(sK49_skl) ),
inference(component_clause,[status(thm)],[f469]) ).
fof(f472,definition,
( sQ1_spl
<=> ssItem(sK51_skl) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f474,plain,
( sQ1_spl
| ~ ssItem(sK51_skl) ),
inference(component_clause,[status(thm)],[f472]) ).
fof(f479,plain,
~ memberP(sK50_skl,sK51_skl),
inference(forward_demodulation,[status(thm)],[f421,f428]) ).
fof(f485,plain,
( sQ1_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f474,f426]) ).
fof(f486,plain,
sQ1_spl,
inference(contradiction_clause,[status(thm)],[f485]) ).
fof(f487,plain,
( sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f471,f419]) ).
fof(f488,plain,
sQ0_spl,
inference(contradiction_clause,[status(thm)],[f487]) ).
fof(f621,definition,
( sQ26_spl
<=> ssList(nil) ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f623,plain,
( sQ26_spl
| ~ ssList(nil) ),
inference(component_clause,[status(thm)],[f621]) ).
fof(f629,plain,
( sQ26_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f623,f223]) ).
fof(f630,plain,
sQ26_spl,
inference(contradiction_clause,[status(thm)],[f629]) ).
fof(f647,definition,
( sQ32_spl
<=> ssItem(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f649,plain,
( sQ32_spl
| ~ ssItem(sK0_skl) ),
inference(component_clause,[status(thm)],[f647]) ).
fof(f658,definition,
! [X0] :
( sQ34_spl
<=> ( memberP(app(X0,sK49_skl),sK51_skl)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f659,plain,
! [X0] :
( ~ sQ34_spl
| memberP(app(X0,sK49_skl),sK51_skl)
| ~ ssList(X0) ),
inference(component_clause,[status(thm)],[f658]) ).
fof(f674,plain,
( 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,f423]) ).
fof(f677,definition,
( sQ37_spl
<=> ssList(sK50_skl) ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f679,plain,
( sQ37_spl
| ~ ssList(sK50_skl) ),
inference(component_clause,[status(thm)],[f677]) ).
fof(f680,definition,
( sQ38_spl
<=> app(app(sK7_skl(sK49_skl,sK50_skl),sK49_skl),sK8_skl(sK49_skl,sK50_skl)) = sK50_skl ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f681,plain,
( ~ sQ38_spl
| app(app(sK7_skl(sK49_skl,sK50_skl),sK49_skl),sK8_skl(sK49_skl,sK50_skl)) = sK50_skl ),
inference(component_clause,[status(thm)],[f680]) ).
fof(f683,plain,
( sQ38_spl
| ~ sQ0_spl
| ~ sQ37_spl ),
inference(split_clause,[status(thm)],[f674,f677,f469,f680]) ).
fof(f690,plain,
( sQ37_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f679,f420]) ).
fof(f691,plain,
sQ37_spl,
inference(contradiction_clause,[status(thm)],[f690]) ).
fof(f707,definition,
( sQ44_spl
<=> segmentP(sK50_skl,sK49_skl) ),
introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition]) ).
fof(f709,plain,
( sQ44_spl
| ~ segmentP(sK50_skl,sK49_skl) ),
inference(component_clause,[status(thm)],[f707]) ).
fof(f710,definition,
( sQ45_spl
<=> totalorderedP(sK49_skl) ),
introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition]) ).
fof(f712,plain,
( sQ45_spl
| ~ totalorderedP(sK49_skl) ),
inference(component_clause,[status(thm)],[f710]) ).
fof(f714,plain,
( sQ45_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f712,f424]) ).
fof(f715,plain,
sQ45_spl,
inference(contradiction_clause,[status(thm)],[f714]) ).
fof(f716,plain,
( sQ44_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f709,f423]) ).
fof(f717,plain,
sQ44_spl,
inference(contradiction_clause,[status(thm)],[f716]) ).
fof(f734,definition,
( sQ50_spl
<=> ssItem(sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition]) ).
fof(f736,plain,
( sQ50_spl
| ~ ssItem(sK1_skl) ),
inference(component_clause,[status(thm)],[f734]) ).
fof(f739,plain,
( sQ50_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f736,f104]) ).
fof(f740,plain,
sQ50_spl,
inference(contradiction_clause,[status(thm)],[f739]) ).
fof(f756,plain,
( sQ32_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f649,f103]) ).
fof(f757,plain,
sQ32_spl,
inference(contradiction_clause,[status(thm)],[f756]) ).
fof(f865,plain,
app(nil,sK50_skl) = sK50_skl,
inference(resolution,[status(thm)],[f249,f420]) ).
fof(f874,plain,
app(nil,nil) = nil,
inference(resolution,[status(thm)],[f249,f223]) ).
fof(f1058,definition,
! [X0] :
( sQ92_spl
<=> ( ~ ssItem(X0)
| ~ ssItem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ92_spl])],[split_symbol_definition]) ).
fof(f1059,plain,
! [X0] :
( ~ sQ92_spl
| ~ ssItem(X0)
| ~ ssItem(X0) ),
inference(component_clause,[status(thm)],[f1058]) ).
fof(f1065,plain,
! [X0] :
( ~ sQ92_spl
| ~ ssItem(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1059]) ).
fof(f1069,plain,
( ~ sQ92_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f103,f1065]) ).
fof(f1072,plain,
~ sQ92_spl,
inference(contradiction_clause,[status(thm)],[f1069]) ).
fof(f1100,definition,
( sQ97_spl
<=> ssList(sK7_skl(sK49_skl,sK50_skl)) ),
introduced(definition,[new_symbols(definition,[sQ97_spl])],[split_symbol_definition]) ).
fof(f1103,definition,
( sQ98_spl
<=> ssList(sK8_skl(sK49_skl,sK50_skl)) ),
introduced(definition,[new_symbols(definition,[sQ98_spl])],[split_symbol_definition]) ).
fof(f1156,plain,
app(sK49_skl,nil) = sK49_skl,
inference(resolution,[status(thm)],[f389,f419]) ).
fof(f1239,definition,
! [X0] :
( sQ118_spl
<=> ( sK51_skl = X0
| ~ ssItem(X0)
| ~ ssItem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ118_spl])],[split_symbol_definition]) ).
fof(f1240,plain,
! [X0] :
( ~ sQ118_spl
| sK51_skl = X0
| ~ ssItem(X0)
| ~ ssItem(X0) ),
inference(component_clause,[status(thm)],[f1239]) ).
fof(f1243,plain,
! [X0] :
( ~ sQ118_spl
| sK51_skl = X0
| ~ ssItem(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1240]) ).
fof(f1273,plain,
( ~ sQ118_spl
| sK51_skl = sK1_skl ),
inference(resolution,[status(thm)],[f1243,f104]) ).
fof(f1274,plain,
( ~ sQ118_spl
| sK51_skl = sK0_skl ),
inference(resolution,[status(thm)],[f1243,f103]) ).
fof(f1280,plain,
( ~ sQ118_spl
| sK0_skl != sK51_skl ),
inference(backward_demodulation,[status(thm)],[f1273,f105]) ).
fof(f1284,plain,
! [X0,X1] :
( ~ memberP(X0,sK51_skl)
| memberP(app(X0,X1),sK51_skl)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f271,f426]) ).
fof(f1294,plain,
( ~ sQ118_spl
| sK51_skl != sK51_skl ),
inference(forward_demodulation,[status(thm)],[f1274,f1280]) ).
fof(f1295,plain,
( ~ sQ118_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f1294]) ).
fof(f1296,plain,
~ sQ118_spl,
inference(contradiction_clause,[status(thm)],[f1295]) ).
fof(f1330,definition,
! [X0] :
( sQ128_spl
<=> ( memberP(X0,sK51_skl)
| ~ memberP(app(X0,sK50_skl),sK51_skl)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ128_spl])],[split_symbol_definition]) ).
fof(f1331,plain,
! [X0] :
( ~ sQ128_spl
| memberP(X0,sK51_skl)
| ~ memberP(app(X0,sK50_skl),sK51_skl)
| ~ ssList(X0) ),
inference(component_clause,[status(thm)],[f1330]) ).
fof(f1653,plain,
! [X0,X1] :
( ~ sQ34_spl
| ~ ssList(X0)
| memberP(app(app(X0,sK49_skl),X1),sK51_skl)
| ~ ssList(X1)
| ~ ssList(app(X0,sK49_skl)) ),
inference(resolution,[status(thm)],[f1284,f659]) ).
fof(f1695,plain,
! [X0] :
( cons(sK1_skl,X0) != X0
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f225,f104]) ).
fof(f1696,plain,
! [X0] :
( cons(sK0_skl,X0) != X0
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f225,f103]) ).
fof(f1699,plain,
! [X0] :
( cons(sK51_skl,X0) != X0
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f225,f426]) ).
fof(f1706,plain,
cons(sK1_skl,sK50_skl) != sK50_skl,
inference(resolution,[status(thm)],[f1695,f420]) ).
fof(f1717,plain,
cons(sK1_skl,nil) != nil,
inference(resolution,[status(thm)],[f1695,f223]) ).
fof(f1718,plain,
cons(sK1_skl,sK49_skl) != sK49_skl,
inference(resolution,[status(thm)],[f1695,f419]) ).
fof(f1722,plain,
( ~ sQ128_spl
| memberP(nil,sK51_skl)
| ~ memberP(sK50_skl,sK51_skl)
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f865,f1331]) ).
fof(f1728,definition,
( sQ169_spl
<=> memberP(sK50_skl,sK51_skl) ),
introduced(definition,[new_symbols(definition,[sQ169_spl])],[split_symbol_definition]) ).
fof(f1735,definition,
( sQ171_spl
<=> memberP(nil,sK51_skl) ),
introduced(definition,[new_symbols(definition,[sQ171_spl])],[split_symbol_definition]) ).
fof(f1736,plain,
( ~ sQ171_spl
| memberP(nil,sK51_skl) ),
inference(component_clause,[status(thm)],[f1735]) ).
fof(f1738,plain,
( ~ sQ128_spl
| sQ171_spl
| ~ sQ169_spl
| ~ sQ26_spl ),
inference(split_clause,[status(thm)],[f1722,f621,f1728,f1735,f1330]) ).
fof(f1739,plain,
( ~ sQ171_spl
| ~ ssItem(sK51_skl) ),
inference(resolution,[status(thm)],[f1736,f279]) ).
fof(f1742,plain,
( ~ sQ171_spl
| ~ sQ1_spl ),
inference(split_clause,[status(thm)],[f1739,f472,f1735]) ).
fof(f1762,plain,
cons(sK51_skl,sK50_skl) != sK50_skl,
inference(resolution,[status(thm)],[f1699,f420]) ).
fof(f1773,plain,
cons(sK51_skl,nil) != nil,
inference(resolution,[status(thm)],[f1699,f223]) ).
fof(f1774,plain,
cons(sK51_skl,sK49_skl) != sK49_skl,
inference(resolution,[status(thm)],[f1699,f419]) ).
fof(f1801,plain,
cons(sK0_skl,sK50_skl) != sK50_skl,
inference(resolution,[status(thm)],[f1696,f420]) ).
fof(f1812,plain,
cons(sK0_skl,nil) != nil,
inference(resolution,[status(thm)],[f1696,f223]) ).
fof(f1813,plain,
cons(sK0_skl,sK49_skl) != sK49_skl,
inference(resolution,[status(thm)],[f1696,f419]) ).
fof(f1816,plain,
! [X0] :
( ssList(cons(sK1_skl,X0))
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f222,f104]) ).
fof(f1817,plain,
! [X0] :
( ssList(cons(sK0_skl,X0))
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f222,f103]) ).
fof(f1820,plain,
! [X0] :
( ssList(cons(sK51_skl,X0))
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f222,f426]) ).
fof(f2159,plain,
! [X0] :
( nil != cons(sK0_skl,X0)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f235,f103]) ).
fof(f2160,plain,
! [X0] :
( nil != cons(sK1_skl,X0)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f235,f104]) ).
fof(f2166,plain,
! [X0] :
( nil != cons(sK51_skl,X0)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f235,f426]) ).
fof(f2782,plain,
nil != cons(sK51_skl,sK50_skl),
inference(resolution,[status(thm)],[f2166,f420]) ).
fof(f2783,plain,
nil != cons(sK51_skl,sK49_skl),
inference(resolution,[status(thm)],[f2166,f419]) ).
fof(f2957,definition,
! [X0] :
( sQ279_spl
<=> ( ~ ssItem(X0)
| ~ ssItem(X0)
| ~ ssItem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ279_spl])],[split_symbol_definition]) ).
fof(f2958,plain,
! [X0] :
( ~ sQ279_spl
| ~ ssItem(X0)
| ~ ssItem(X0)
| ~ ssItem(X0) ),
inference(component_clause,[status(thm)],[f2957]) ).
fof(f2973,plain,
! [X0] :
( ~ sQ279_spl
| ~ ssItem(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f2958]) ).
fof(f3051,plain,
( ~ sQ279_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f103,f2973]) ).
fof(f3061,plain,
~ sQ279_spl,
inference(contradiction_clause,[status(thm)],[f3051]) ).
fof(f3326,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,f426]) ).
fof(f3474,plain,
nil != cons(sK0_skl,sK50_skl),
inference(resolution,[status(thm)],[f2159,f420]) ).
fof(f3475,plain,
nil != cons(sK0_skl,sK49_skl),
inference(resolution,[status(thm)],[f2159,f419]) ).
fof(f3497,plain,
nil != cons(sK1_skl,sK50_skl),
inference(resolution,[status(thm)],[f2160,f420]) ).
fof(f3498,plain,
nil != cons(sK1_skl,sK49_skl),
inference(resolution,[status(thm)],[f2160,f419]) ).
fof(f3629,definition,
! [X0] :
( sQ338_spl
<=> ( ~ ssList(X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ338_spl])],[split_symbol_definition]) ).
fof(f3630,plain,
! [X0] :
( ~ sQ338_spl
| ~ ssList(X0)
| ~ ssList(X0) ),
inference(component_clause,[status(thm)],[f3629]) ).
fof(f3634,plain,
! [X0] :
( ~ sQ338_spl
| ~ ssList(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f3630]) ).
fof(f3635,plain,
( ~ sQ338_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f420,f3634]) ).
fof(f3639,plain,
~ sQ338_spl,
inference(contradiction_clause,[status(thm)],[f3635]) ).
fof(f3667,plain,
! [X0,X1] :
( ~ memberP(sK49_skl,X0)
| memberP(app(X1,sK49_skl),X0)
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(resolution,[status(thm)],[f272,f419]) ).
fof(f3705,definition,
! [X0] :
( sQ339_spl
<=> ( nil != app(X0,nil)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ339_spl])],[split_symbol_definition]) ).
fof(f3706,plain,
! [X0] :
( ~ sQ339_spl
| nil != app(X0,nil)
| ~ ssList(X0) ),
inference(component_clause,[status(thm)],[f3705]) ).
fof(f3938,plain,
ssList(cons(sK0_skl,nil)),
inference(resolution,[status(thm)],[f1817,f223]) ).
fof(f3972,definition,
( sQ354_spl
<=> nil = cons(sK0_skl,nil) ),
introduced(definition,[new_symbols(definition,[sQ354_spl])],[split_symbol_definition]) ).
fof(f3973,plain,
( ~ sQ354_spl
| nil = cons(sK0_skl,nil) ),
inference(component_clause,[status(thm)],[f3972]) ).
fof(f3976,plain,
( ~ sQ354_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3973,f1812]) ).
fof(f3977,plain,
~ sQ354_spl,
inference(contradiction_clause,[status(thm)],[f3976]) ).
fof(f4011,definition,
( sQ356_spl
<=> nil = cons(sK0_skl,sK49_skl) ),
introduced(definition,[new_symbols(definition,[sQ356_spl])],[split_symbol_definition]) ).
fof(f4012,plain,
( ~ sQ356_spl
| nil = cons(sK0_skl,sK49_skl) ),
inference(component_clause,[status(thm)],[f4011]) ).
fof(f4015,plain,
( ~ sQ356_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4012,f3475]) ).
fof(f4016,plain,
~ sQ356_spl,
inference(contradiction_clause,[status(thm)],[f4015]) ).
fof(f4047,definition,
( sQ358_spl
<=> nil = cons(sK0_skl,sK50_skl) ),
introduced(definition,[new_symbols(definition,[sQ358_spl])],[split_symbol_definition]) ).
fof(f4048,plain,
( ~ sQ358_spl
| nil = cons(sK0_skl,sK50_skl) ),
inference(component_clause,[status(thm)],[f4047]) ).
fof(f4051,plain,
( ~ sQ358_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4048,f3474]) ).
fof(f4052,plain,
~ sQ358_spl,
inference(contradiction_clause,[status(thm)],[f4051]) ).
fof(f4063,plain,
ssList(cons(sK51_skl,nil)),
inference(resolution,[status(thm)],[f1820,f223]) ).
fof(f4065,plain,
ssList(cons(sK51_skl,sK49_skl)),
inference(resolution,[status(thm)],[f1820,f419]) ).
fof(f4066,plain,
ssList(cons(sK51_skl,sK50_skl)),
inference(resolution,[status(thm)],[f1820,f420]) ).
fof(f4099,definition,
( sQ360_spl
<=> nil = cons(sK51_skl,nil) ),
introduced(definition,[new_symbols(definition,[sQ360_spl])],[split_symbol_definition]) ).
fof(f4100,plain,
( ~ sQ360_spl
| nil = cons(sK51_skl,nil) ),
inference(component_clause,[status(thm)],[f4099]) ).
fof(f4103,plain,
( ~ sQ360_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4100,f1773]) ).
fof(f4104,plain,
~ sQ360_spl,
inference(contradiction_clause,[status(thm)],[f4103]) ).
fof(f4137,definition,
( sQ362_spl
<=> nil = cons(sK51_skl,sK49_skl) ),
introduced(definition,[new_symbols(definition,[sQ362_spl])],[split_symbol_definition]) ).
fof(f4138,plain,
( ~ sQ362_spl
| nil = cons(sK51_skl,sK49_skl) ),
inference(component_clause,[status(thm)],[f4137]) ).
fof(f4141,plain,
( ~ sQ362_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4138,f2783]) ).
fof(f4142,plain,
~ sQ362_spl,
inference(contradiction_clause,[status(thm)],[f4141]) ).
fof(f4175,definition,
( sQ364_spl
<=> nil = cons(sK51_skl,sK50_skl) ),
introduced(definition,[new_symbols(definition,[sQ364_spl])],[split_symbol_definition]) ).
fof(f4176,plain,
( ~ sQ364_spl
| nil = cons(sK51_skl,sK50_skl) ),
inference(component_clause,[status(thm)],[f4175]) ).
fof(f4179,plain,
( ~ sQ364_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4176,f2782]) ).
fof(f4180,plain,
~ sQ364_spl,
inference(contradiction_clause,[status(thm)],[f4179]) ).
fof(f4208,plain,
ssList(cons(sK1_skl,nil)),
inference(resolution,[status(thm)],[f1816,f223]) ).
fof(f4245,definition,
( sQ369_spl
<=> nil = cons(sK1_skl,nil) ),
introduced(definition,[new_symbols(definition,[sQ369_spl])],[split_symbol_definition]) ).
fof(f4246,plain,
( ~ sQ369_spl
| nil = cons(sK1_skl,nil) ),
inference(component_clause,[status(thm)],[f4245]) ).
fof(f4249,plain,
( ~ sQ369_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4246,f1717]) ).
fof(f4250,plain,
~ sQ369_spl,
inference(contradiction_clause,[status(thm)],[f4249]) ).
fof(f4284,definition,
( sQ371_spl
<=> nil = cons(sK1_skl,sK49_skl) ),
introduced(definition,[new_symbols(definition,[sQ371_spl])],[split_symbol_definition]) ).
fof(f4285,plain,
( ~ sQ371_spl
| nil = cons(sK1_skl,sK49_skl) ),
inference(component_clause,[status(thm)],[f4284]) ).
fof(f4288,plain,
( ~ sQ371_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4285,f3498]) ).
fof(f4289,plain,
~ sQ371_spl,
inference(contradiction_clause,[status(thm)],[f4288]) ).
fof(f4323,definition,
( sQ373_spl
<=> nil = cons(sK1_skl,sK50_skl) ),
introduced(definition,[new_symbols(definition,[sQ373_spl])],[split_symbol_definition]) ).
fof(f4324,plain,
( ~ sQ373_spl
| nil = cons(sK1_skl,sK50_skl) ),
inference(component_clause,[status(thm)],[f4323]) ).
fof(f4327,plain,
( ~ sQ373_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4324,f3497]) ).
fof(f4328,plain,
~ sQ373_spl,
inference(contradiction_clause,[status(thm)],[f4327]) ).
fof(f4444,plain,
( ~ sQ339_spl
| nil != app(nil,nil) ),
inference(resolution,[status(thm)],[f3706,f223]) ).
fof(f4448,plain,
( ~ sQ339_spl
| nil != nil ),
inference(forward_demodulation,[status(thm)],[f874,f4444]) ).
fof(f4449,plain,
( ~ sQ339_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f4448]) ).
fof(f4450,plain,
~ sQ339_spl,
inference(contradiction_clause,[status(thm)],[f4449]) ).
fof(f5006,plain,
! [X0] :
( memberP(X0,sK51_skl)
| ~ memberP(app(X0,sK50_skl),sK51_skl)
| ~ ssList(sK50_skl)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f3326,f479]) ).
fof(f5013,plain,
( ~ sQ37_spl
| sQ128_spl ),
inference(split_clause,[status(thm)],[f5006,f1330,f677]) ).
fof(f5071,definition,
( sQ413_spl
<=> ssList(cons(sK51_skl,sK50_skl)) ),
introduced(definition,[new_symbols(definition,[sQ413_spl])],[split_symbol_definition]) ).
fof(f5073,plain,
( sQ413_spl
| ~ ssList(cons(sK51_skl,sK50_skl)) ),
inference(component_clause,[status(thm)],[f5071]) ).
fof(f5075,definition,
( sQ414_spl
<=> ssList(cons(sK51_skl,sK49_skl)) ),
introduced(definition,[new_symbols(definition,[sQ414_spl])],[split_symbol_definition]) ).
fof(f5077,plain,
( sQ414_spl
| ~ ssList(cons(sK51_skl,sK49_skl)) ),
inference(component_clause,[status(thm)],[f5075]) ).
fof(f5079,definition,
( sQ415_spl
<=> ssList(cons(sK51_skl,nil)) ),
introduced(definition,[new_symbols(definition,[sQ415_spl])],[split_symbol_definition]) ).
fof(f5081,plain,
( sQ415_spl
| ~ ssList(cons(sK51_skl,nil)) ),
inference(component_clause,[status(thm)],[f5079]) ).
fof(f6077,plain,
( sQ415_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5081,f4063]) ).
fof(f6078,plain,
sQ415_spl,
inference(contradiction_clause,[status(thm)],[f6077]) ).
fof(f6079,plain,
( sQ414_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5077,f4065]) ).
fof(f6080,plain,
sQ414_spl,
inference(contradiction_clause,[status(thm)],[f6079]) ).
fof(f6081,plain,
( sQ413_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5073,f4066]) ).
fof(f6082,plain,
sQ413_spl,
inference(contradiction_clause,[status(thm)],[f6081]) ).
fof(f8109,plain,
! [X0] :
( ssList(app(X0,sK49_skl))
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f245,f419]) ).
fof(f8222,definition,
( sQ699_spl
<=> sK49_skl = cons(sK1_skl,sK49_skl) ),
introduced(definition,[new_symbols(definition,[sQ699_spl])],[split_symbol_definition]) ).
fof(f8223,plain,
( ~ sQ699_spl
| sK49_skl = cons(sK1_skl,sK49_skl) ),
inference(component_clause,[status(thm)],[f8222]) ).
fof(f8250,definition,
( sQ707_spl
<=> sK49_skl = cons(sK51_skl,sK49_skl) ),
introduced(definition,[new_symbols(definition,[sQ707_spl])],[split_symbol_definition]) ).
fof(f8251,plain,
( ~ sQ707_spl
| sK49_skl = cons(sK51_skl,sK49_skl) ),
inference(component_clause,[status(thm)],[f8250]) ).
fof(f8278,definition,
( sQ715_spl
<=> sK49_skl = cons(sK0_skl,sK49_skl) ),
introduced(definition,[new_symbols(definition,[sQ715_spl])],[split_symbol_definition]) ).
fof(f8279,plain,
( ~ sQ715_spl
| sK49_skl = cons(sK0_skl,sK49_skl) ),
inference(component_clause,[status(thm)],[f8278]) ).
fof(f8300,definition,
( sQ721_spl
<=> app(sK49_skl,sK49_skl) = app(sK49_skl,sK49_skl) ),
introduced(definition,[new_symbols(definition,[sQ721_spl])],[split_symbol_definition]) ).
fof(f8302,plain,
( sQ721_spl
| app(sK49_skl,sK49_skl) != app(sK49_skl,sK49_skl) ),
inference(component_clause,[status(thm)],[f8300]) ).
fof(f9149,definition,
( sQ819_spl
<=> sK50_skl = cons(sK1_skl,sK50_skl) ),
introduced(definition,[new_symbols(definition,[sQ819_spl])],[split_symbol_definition]) ).
fof(f9150,plain,
( ~ sQ819_spl
| sK50_skl = cons(sK1_skl,sK50_skl) ),
inference(component_clause,[status(thm)],[f9149]) ).
fof(f9177,definition,
( sQ827_spl
<=> sK50_skl = cons(sK51_skl,sK50_skl) ),
introduced(definition,[new_symbols(definition,[sQ827_spl])],[split_symbol_definition]) ).
fof(f9178,plain,
( ~ sQ827_spl
| sK50_skl = cons(sK51_skl,sK50_skl) ),
inference(component_clause,[status(thm)],[f9177]) ).
fof(f9205,definition,
( sQ835_spl
<=> sK50_skl = cons(sK0_skl,sK50_skl) ),
introduced(definition,[new_symbols(definition,[sQ835_spl])],[split_symbol_definition]) ).
fof(f9206,plain,
( ~ sQ835_spl
| sK50_skl = cons(sK0_skl,sK50_skl) ),
inference(component_clause,[status(thm)],[f9205]) ).
fof(f9238,definition,
( sQ844_spl
<=> app(sK50_skl,sK50_skl) = app(sK50_skl,sK50_skl) ),
introduced(definition,[new_symbols(definition,[sQ844_spl])],[split_symbol_definition]) ).
fof(f9240,plain,
( sQ844_spl
| app(sK50_skl,sK50_skl) != app(sK50_skl,sK50_skl) ),
inference(component_clause,[status(thm)],[f9238]) ).
fof(f10127,plain,
( ~ sQ715_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8279,f1813]) ).
fof(f10128,plain,
~ sQ715_spl,
inference(contradiction_clause,[status(thm)],[f10127]) ).
fof(f10129,plain,
( ~ sQ707_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8251,f1774]) ).
fof(f10130,plain,
~ sQ707_spl,
inference(contradiction_clause,[status(thm)],[f10129]) ).
fof(f10131,plain,
( ~ sQ699_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8223,f1718]) ).
fof(f10132,plain,
~ sQ699_spl,
inference(contradiction_clause,[status(thm)],[f10131]) ).
fof(f11065,plain,
( ~ sQ835_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f9206,f1801]) ).
fof(f11066,plain,
~ sQ835_spl,
inference(contradiction_clause,[status(thm)],[f11065]) ).
fof(f11067,plain,
( ~ sQ827_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f9178,f1762]) ).
fof(f11068,plain,
~ sQ827_spl,
inference(contradiction_clause,[status(thm)],[f11067]) ).
fof(f11069,plain,
( ~ sQ819_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f9150,f1706]) ).
fof(f11070,plain,
~ sQ819_spl,
inference(contradiction_clause,[status(thm)],[f11069]) ).
fof(f11881,plain,
! [X0] :
( memberP(app(X0,sK49_skl),sK51_skl)
| ~ ssList(X0)
| ~ ssItem(sK51_skl) ),
inference(resolution,[status(thm)],[f3667,f467]) ).
fof(f11886,plain,
( sQ34_spl
| ~ sQ1_spl ),
inference(split_clause,[status(thm)],[f11881,f472,f658]) ).
fof(f12362,definition,
( sQ1115_spl
<=> ssList(cons(sK0_skl,nil)) ),
introduced(definition,[new_symbols(definition,[sQ1115_spl])],[split_symbol_definition]) ).
fof(f12364,plain,
( sQ1115_spl
| ~ ssList(cons(sK0_skl,nil)) ),
inference(component_clause,[status(thm)],[f12362]) ).
fof(f12752,definition,
( sQ1169_spl
<=> ssList(cons(sK1_skl,nil)) ),
introduced(definition,[new_symbols(definition,[sQ1169_spl])],[split_symbol_definition]) ).
fof(f12754,plain,
( sQ1169_spl
| ~ ssList(cons(sK1_skl,nil)) ),
inference(component_clause,[status(thm)],[f12752]) ).
fof(f13328,plain,
( ssList(sK8_skl(sK49_skl,sK50_skl))
| ~ ssList(sK49_skl)
| ~ ssList(sK50_skl) ),
inference(resolution,[status(thm)],[f135,f423]) ).
fof(f13336,plain,
( sQ98_spl
| ~ sQ0_spl
| ~ sQ37_spl ),
inference(split_clause,[status(thm)],[f13328,f677,f469,f1103]) ).
fof(f13345,plain,
( ssList(sK7_skl(sK49_skl,sK50_skl))
| ~ ssList(sK49_skl)
| ~ ssList(sK50_skl) ),
inference(resolution,[status(thm)],[f134,f423]) ).
fof(f13353,plain,
( sQ97_spl
| ~ sQ0_spl
| ~ sQ37_spl ),
inference(split_clause,[status(thm)],[f13345,f677,f469,f1100]) ).
fof(f16809,plain,
( sQ1115_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3938,f12364]) ).
fof(f16810,plain,
sQ1115_spl,
inference(contradiction_clause,[status(thm)],[f16809]) ).
fof(f17127,definition,
( sQ1647_spl
<=> hd(sK49_skl) = hd(sK49_skl) ),
introduced(definition,[new_symbols(definition,[sQ1647_spl])],[split_symbol_definition]) ).
fof(f17129,plain,
( sQ1647_spl
| hd(sK49_skl) != hd(sK49_skl) ),
inference(component_clause,[status(thm)],[f17127]) ).
fof(f17130,definition,
( sQ1648_spl
<=> tl(sK49_skl) = tl(sK49_skl) ),
introduced(definition,[new_symbols(definition,[sQ1648_spl])],[split_symbol_definition]) ).
fof(f17132,plain,
( sQ1648_spl
| tl(sK49_skl) != tl(sK49_skl) ),
inference(component_clause,[status(thm)],[f17130]) ).
fof(f17142,plain,
( sQ1648_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f17132]) ).
fof(f17143,plain,
sQ1648_spl,
inference(contradiction_clause,[status(thm)],[f17142]) ).
fof(f17144,plain,
( sQ1647_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f17129]) ).
fof(f17145,plain,
sQ1647_spl,
inference(contradiction_clause,[status(thm)],[f17144]) ).
fof(f17293,plain,
( sQ844_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f9240]) ).
fof(f17294,plain,
sQ844_spl,
inference(contradiction_clause,[status(thm)],[f17293]) ).
fof(f17317,plain,
( sQ721_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f8302]) ).
fof(f17318,plain,
sQ721_spl,
inference(contradiction_clause,[status(thm)],[f17317]) ).
fof(f17390,definition,
( sQ1663_spl
<=> hd(sK50_skl) = hd(sK50_skl) ),
introduced(definition,[new_symbols(definition,[sQ1663_spl])],[split_symbol_definition]) ).
fof(f17392,plain,
( sQ1663_spl
| hd(sK50_skl) != hd(sK50_skl) ),
inference(component_clause,[status(thm)],[f17390]) ).
fof(f17394,plain,
( sQ1663_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f17392]) ).
fof(f17395,plain,
sQ1663_spl,
inference(contradiction_clause,[status(thm)],[f17394]) ).
fof(f20201,definition,
( sQ1816_spl
<=> tl(sK50_skl) = tl(sK50_skl) ),
introduced(definition,[new_symbols(definition,[sQ1816_spl])],[split_symbol_definition]) ).
fof(f20203,plain,
( sQ1816_spl
| tl(sK50_skl) != tl(sK50_skl) ),
inference(component_clause,[status(thm)],[f20201]) ).
fof(f20205,plain,
( sQ1816_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f20203]) ).
fof(f20206,plain,
sQ1816_spl,
inference(contradiction_clause,[status(thm)],[f20205]) ).
fof(f25460,plain,
( sQ1169_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4208,f12754]) ).
fof(f25461,plain,
sQ1169_spl,
inference(contradiction_clause,[status(thm)],[f25460]) ).
fof(f30593,definition,
( sQ2950_spl
<=> sK1_skl = sK0_skl ),
introduced(definition,[new_symbols(definition,[sQ2950_spl])],[split_symbol_definition]) ).
fof(f30594,plain,
( ~ sQ2950_spl
| sK1_skl = sK0_skl ),
inference(component_clause,[status(thm)],[f30593]) ).
fof(f30597,plain,
( ~ sQ2950_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f30594,f105]) ).
fof(f30598,plain,
~ sQ2950_spl,
inference(contradiction_clause,[status(thm)],[f30597]) ).
fof(f31507,definition,
( sQ3077_spl
<=> hd(nil) = hd(nil) ),
introduced(definition,[new_symbols(definition,[sQ3077_spl])],[split_symbol_definition]) ).
fof(f31509,plain,
( sQ3077_spl
| hd(nil) != hd(nil) ),
inference(component_clause,[status(thm)],[f31507]) ).
fof(f31513,plain,
( sQ3077_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f31509]) ).
fof(f31514,plain,
sQ3077_spl,
inference(contradiction_clause,[status(thm)],[f31513]) ).
fof(f31567,definition,
( sQ3079_spl
<=> singletonP(nil) ),
introduced(definition,[new_symbols(definition,[sQ3079_spl])],[split_symbol_definition]) ).
fof(f31568,plain,
( ~ sQ3079_spl
| singletonP(nil) ),
inference(component_clause,[status(thm)],[f31567]) ).
fof(f31593,definition,
( sQ3085_spl
<=> ssList(app(sK49_skl,nil)) ),
introduced(definition,[new_symbols(definition,[sQ3085_spl])],[split_symbol_definition]) ).
fof(f31595,plain,
( sQ3085_spl
| ~ ssList(app(sK49_skl,nil)) ),
inference(component_clause,[status(thm)],[f31593]) ).
fof(f31749,plain,
( sQ3085_spl
| ~ ssList(sK49_skl) ),
inference(forward_demodulation,[status(thm)],[f1156,f31595]) ).
fof(f31750,plain,
( sQ3085_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f31749,f419]) ).
fof(f31751,plain,
sQ3085_spl,
inference(contradiction_clause,[status(thm)],[f31750]) ).
fof(f31753,plain,
( ~ sQ3079_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f31568,f280]) ).
fof(f31754,plain,
~ sQ3079_spl,
inference(contradiction_clause,[status(thm)],[f31753]) ).
fof(f35453,plain,
! [X0,X1] :
( ~ sQ34_spl
| ~ ssList(X1)
| memberP(app(app(X1,sK49_skl),X0),sK51_skl)
| ~ ssList(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1653,f8109]) ).
fof(f35462,plain,
( ~ sQ38_spl
| ~ sQ34_spl
| ~ ssList(sK7_skl(sK49_skl,sK50_skl))
| memberP(sK50_skl,sK51_skl)
| ~ ssList(sK8_skl(sK49_skl,sK50_skl)) ),
inference(paramodulation,[status(thm)],[f681,f35453]) ).
fof(f35473,plain,
( ~ sQ38_spl
| ~ sQ34_spl
| ~ sQ97_spl
| sQ169_spl
| ~ sQ98_spl ),
inference(split_clause,[status(thm)],[f35462,f1103,f1728,f1100,f658,f680]) ).
fof(f35476,plain,
$false,
inference(sat_refutation,[status(thm)],[f486,f488,f630,f683,f691,f715,f717,f740,f757,f1072,f1296,f1738,f1742,f3061,f3639,f3977,f4016,f4052,f4104,f4142,f4180,f4250,f4289,f4328,f4450,f5013,f6078,f6080,f6082,f10128,f10130,f10132,f11066,f11068,f11070,f11886,f13336,f13353,f16810,f17143,f17145,f17294,f17318,f17395,f20206,f25461,f30598,f31514,f31751,f31754,f35473]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWC401+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n012.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Mon Sep 21 08:21:22 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.12/0.37 % Drodi V4.1.1
% 166.41/21.35 % Refutation found
% 166.41/21.35 % SZS status Theorem for theBenchmark: Theorem is valid
% 166.41/21.35 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 10.41/21.41 % Elapsed time: 21.041535 seconds
% 10.41/21.41 % CPU time: 167.206686 seconds
% 10.41/21.41 % Total memory used: 604.872 MB
% 10.41/21.41 % Net memory used: 559.586 MB
%------------------------------------------------------------------------------