%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWC308+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 : n007.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:44 PM UTC 2026
% Result : Theorem 268.30s 34.56s
% Output : CNFRefutation 270.06s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 82
% Syntax : Number of formulae : 397 ( 103 unt; 63 def)
% Number of atoms : 933 ( 253 equ)
% Maximal formula atoms : 24 ( 2 avg)
% Number of connectives : 929 ( 393 ~; 379 |; 60 &)
% ( 65 <=>; 32 =>; 0 <=; 0 <~>)
% Maximal formula depth : 28 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 72 ( 70 usr; 64 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 7 con; 0-2 aty)
% Number of variables : 149 ( 127 !; 22 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
? [U] :
( ? [V] :
( U != V
& ssItem(V) )
& ssItem(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ( neq(U,V)
<=> U != V ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f16,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssItem(V)
=> ssList(cons(V,U)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f17,axiom,
ssList(nil),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f18,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssItem(V)
=> cons(V,U) != U ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f21,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssItem(V)
=> nil != cons(V,U) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f22,axiom,
! [U] :
( ssList(U)
=> ( nil != U
=> ssItem(hd(U)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f24,axiom,
! [U] :
( ssList(U)
=> ( nil != U
=> ssList(tl(U)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f25,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssItem(V)
=> tl(cons(V,U)) = U ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(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(f31,axiom,
! [U] :
( ssItem(U)
=> leq(U,U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f39,axiom,
~ singletonP(nil),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f42,axiom,
! [U] :
( ssList(U)
=> frontsegP(U,U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f66,axiom,
totalorderedP(nil),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f78,axiom,
! [U] :
( ssList(U)
=> ( nil != U
=> cons(hd(U),tl(U)) = U ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f81,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssItem(V)
=> cons(V,U) = app(cons(V,nil),U) ) ),
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)
=> ( ( nil = X
& nil != W )
| ? [X3] :
( ? [X4] :
( app(cons(X3,nil),X4) = X
& app(X4,cons(X3,nil)) != W
& ssList(X4) )
& ssItem(X3) )
| ? [Y] :
( ? [Z] :
( ? [X1] :
( neq(nil,V)
& ? [X2] :
( neq(nil,V)
& hd(V) = X2
& cons(X2,nil) = X1
& ssItem(X2) )
& app(Z,X1) = Y
& tl(V) = Z
& ssList(X1) )
& ssList(Z) )
& U = Y
& ssList(Y) )
| ~ neq(V,nil)
| U != W
| V != X ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f97,negated_conjecture,
~ ! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ! [W] :
( ssList(W)
=> ! [X] :
( ssList(X)
=> ( ( nil = X
& nil != W )
| ? [X3] :
( ? [X4] :
( app(cons(X3,nil),X4) = X
& app(X4,cons(X3,nil)) != W
& ssList(X4) )
& ssItem(X3) )
| ? [Y] :
( ? [Z] :
( ? [X1] :
( neq(nil,V)
& ? [X2] :
( neq(nil,V)
& hd(V) = X2
& cons(X2,nil) = X1
& ssItem(X2) )
& app(Z,X1) = Y
& tl(V) = Z
& ssList(X1) )
& ssList(Z) )
& U = Y
& ssList(Y) )
| ~ neq(V,nil)
| 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(f217,plain,
! [U] :
( ! [V] :
( ( neq(U,V)
<=> U != V )
| ~ ssList(V) )
| ~ ssList(U) ),
inference(pre_NNF_transformation,[status(thm)],[f15]) ).
fof(f218,plain,
! [U] :
( ! [V] :
( ( ( U = V
| neq(U,V) )
& ( U != V
| ~ neq(U,V) ) )
| ~ ssList(V) )
| ~ ssList(U) ),
inference(NNF_transformation,[status(thm)],[f217]) ).
fof(f219,plain,
! [X0,X1] :
( X0 != X1
| ~ neq(X0,X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f218]) ).
fof(f220,plain,
! [X0,X1] :
( ~ ssList(X1)
| neq(X0,X1)
| X0 = X1
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f218]) ).
fof(f221,plain,
! [U] :
( ! [V] :
( ssList(cons(V,U))
| ~ ssItem(V) )
| ~ ssList(U) ),
inference(pre_NNF_transformation,[status(thm)],[f16]) ).
fof(f222,plain,
! [X0,X1] :
( ~ ssList(X1)
| ssList(cons(X0,X1))
| ~ ssItem(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] :
( ~ ssItem(X0)
| ~ ssList(X1)
| cons(X0,X1) != nil ),
inference(cnf_transformation,[status(thm)],[f234]) ).
fof(f236,plain,
! [U] :
( ssItem(hd(U))
| nil = U
| ~ ssList(U) ),
inference(pre_NNF_transformation,[status(thm)],[f22]) ).
fof(f237,plain,
! [X0] :
( X0 = nil
| ~ ssList(X0)
| ssItem(hd(X0)) ),
inference(cnf_transformation,[status(thm)],[f236]) ).
fof(f240,plain,
! [U] :
( ssList(tl(U))
| nil = U
| ~ ssList(U) ),
inference(pre_NNF_transformation,[status(thm)],[f24]) ).
fof(f241,plain,
! [X0] :
( ~ ssList(X0)
| X0 = nil
| ssList(tl(X0)) ),
inference(cnf_transformation,[status(thm)],[f240]) ).
fof(f242,plain,
! [U] :
( ! [V] :
( tl(cons(V,U)) = U
| ~ ssItem(V) )
| ~ ssList(U) ),
inference(pre_NNF_transformation,[status(thm)],[f25]) ).
fof(f243,plain,
! [X0,X1] :
( ~ ssItem(X1)
| ~ ssList(X0)
| X0 = tl(cons(X1,X0)) ),
inference(cnf_transformation,[status(thm)],[f242]) ).
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(X1,X0))
| ~ 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] :
( ~ ssList(X0)
| X0 = app(nil,X0) ),
inference(cnf_transformation,[status(thm)],[f248]) ).
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(f280,plain,
~ singletonP(nil),
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f285,plain,
! [U] :
( frontsegP(U,U)
| ~ ssList(U) ),
inference(pre_NNF_transformation,[status(thm)],[f42]) ).
fof(f286,plain,
! [X0] :
( frontsegP(X0,X0)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f285]) ).
fof(f339,plain,
totalorderedP(nil),
inference(cnf_transformation,[status(thm)],[f66]) ).
fof(f373,plain,
! [U] :
( cons(hd(U),tl(U)) = U
| nil = U
| ~ ssList(U) ),
inference(pre_NNF_transformation,[status(thm)],[f78]) ).
fof(f374,plain,
! [X0] :
( X0 = cons(hd(X0),tl(X0))
| ~ ssList(X0)
| X0 = nil ),
inference(cnf_transformation,[status(thm)],[f373]) ).
fof(f379,plain,
! [U] :
( ! [V] :
( cons(V,U) = app(cons(V,nil),U)
| ~ ssItem(V) )
| ~ ssList(U) ),
inference(pre_NNF_transformation,[status(thm)],[f81]) ).
fof(f380,plain,
! [X0,X1] :
( ~ ssItem(X1)
| app(cons(X1,nil),X0) = cons(X1,X0)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f379]) ).
fof(f388,plain,
! [U] :
( app(U,nil) = U
| ~ ssList(U) ),
inference(pre_NNF_transformation,[status(thm)],[f84]) ).
fof(f389,plain,
! [X0] :
( ~ ssList(X0)
| X0 = app(X0,nil) ),
inference(cnf_transformation,[status(thm)],[f388]) ).
fof(f415,plain,
? [U] :
( ? [V] :
( ? [W] :
( ? [X] :
( ( nil != X
| nil = W )
& ! [X3] :
( ! [X4] :
( app(cons(X3,nil),X4) != X
| app(X4,cons(X3,nil)) = W
| ~ ssList(X4) )
| ~ ssItem(X3) )
& ! [Y] :
( ! [Z] :
( ! [X1] :
( ~ neq(nil,V)
| ! [X2] :
( ~ neq(nil,V)
| hd(V) != X2
| cons(X2,nil) != X1
| ~ ssItem(X2) )
| app(Z,X1) != Y
| tl(V) != Z
| ~ ssList(X1) )
| ~ ssList(Z) )
| U != Y
| ~ ssList(Y) )
& neq(V,nil)
& U = W
& V = X
& ssList(X) )
& ssList(W) )
& ssList(V) )
& ssList(U) ),
inference(pre_NNF_transformation,[status(thm)],[f97]) ).
fof(f416,plain,
? [U] :
( ? [V] :
( ? [W] :
( ? [X] :
( ( nil != X
| nil = W )
& ! [X3] :
( ! [X4] :
( app(cons(X3,nil),X4) != X
| app(X4,cons(X3,nil)) = W
| ~ ssList(X4) )
| ~ ssItem(X3) )
& ! [Y] :
( ! [Z] :
( ~ neq(nil,V)
| ! [X1] :
( ~ neq(nil,V)
| ! [X2] :
( hd(V) != X2
| cons(X2,nil) != X1
| ~ ssItem(X2) )
| app(Z,X1) != Y
| tl(V) != Z
| ~ ssList(X1) )
| ~ ssList(Z) )
| U != Y
| ~ ssList(Y) )
& neq(V,nil)
& U = W
& V = X
& ssList(X) )
& ssList(W) )
& ssList(V) )
& ssList(U) ),
inference(miniscoping,[status(thm)],[f415]) ).
fof(f417,plain,
( ( nil != sK50_skl
| nil = sK49_skl )
& ! [X3] :
( ! [X4] :
( app(cons(X3,nil),X4) != sK50_skl
| app(X4,cons(X3,nil)) = sK49_skl
| ~ ssList(X4) )
| ~ ssItem(X3) )
& ! [Y] :
( ! [Z] :
( ~ neq(nil,sK48_skl)
| ! [X1] :
( ~ neq(nil,sK48_skl)
| ! [X2] :
( hd(sK48_skl) != X2
| cons(X2,nil) != X1
| ~ ssItem(X2) )
| app(Z,X1) != Y
| tl(sK48_skl) != Z
| ~ ssList(X1) )
| ~ ssList(Z) )
| sK47_skl != Y
| ~ ssList(Y) )
& neq(sK48_skl,nil)
& sK47_skl = sK49_skl
& sK48_skl = sK50_skl
& ssList(sK50_skl)
& ssList(sK49_skl)
& ssList(sK48_skl)
& ssList(sK47_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK47_skl,sK48_skl,sK49_skl,sK50_skl]),skolemize(U,sK47_skl),skolemize(V,sK48_skl),skolemize(W,sK49_skl),skolemize(X,sK50_skl)],[f416]) ).
fof(f420,plain,
ssList(sK49_skl),
inference(cnf_transformation,[status(thm)],[f417]) ).
fof(f421,plain,
ssList(sK50_skl),
inference(cnf_transformation,[status(thm)],[f417]) ).
fof(f422,plain,
sK48_skl = sK50_skl,
inference(cnf_transformation,[status(thm)],[f417]) ).
fof(f423,plain,
sK49_skl = sK47_skl,
inference(cnf_transformation,[status(thm)],[f417]) ).
fof(f424,plain,
neq(sK48_skl,nil),
inference(cnf_transformation,[status(thm)],[f417]) ).
fof(f425,plain,
! [X0,X1,X2,X3] :
( ~ neq(nil,sK48_skl)
| ~ neq(nil,sK48_skl)
| hd(sK48_skl) != X3
| cons(X3,nil) != X2
| ~ ssItem(X3)
| app(X1,X2) != X0
| tl(sK48_skl) != X1
| ~ ssList(X2)
| ~ ssList(X1)
| sK47_skl != X0
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f417]) ).
fof(f426,plain,
! [X0,X1] :
( ~ ssList(X1)
| ~ ssItem(X0)
| app(X1,cons(X0,nil)) = sK49_skl
| app(cons(X0,nil),X1) != sK50_skl ),
inference(cnf_transformation,[status(thm)],[f417]) ).
fof(f428,definition,
! [X0,X1,X2,X3] :
( sQ0_spl
<=> ( hd(sK48_skl) != X3
| cons(X3,nil) != X2
| ~ ssItem(X3)
| app(X1,X2) != X0
| tl(sK48_skl) != X1
| ~ ssList(X2)
| ~ ssList(X1)
| sK47_skl != X0
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f429,plain,
! [X0,X1,X2,X3] :
( ~ sQ0_spl
| hd(sK48_skl) != X3
| cons(X3,nil) != X2
| ~ ssItem(X3)
| app(X1,X2) != X0
| tl(sK48_skl) != X1
| ~ ssList(X2)
| ~ ssList(X1)
| sK47_skl != X0
| ~ ssList(X0) ),
inference(component_clause,[status(thm)],[f428]) ).
fof(f431,definition,
( sQ1_spl
<=> neq(nil,sK48_skl) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f433,plain,
( sQ1_spl
| ~ neq(nil,sK48_skl) ),
inference(component_clause,[status(thm)],[f431]) ).
fof(f434,plain,
( ~ sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f425,f428,f431]) ).
fof(f438,definition,
( sQ3_spl
<=> nil = sK50_skl ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f439,plain,
( ~ sQ3_spl
| sK50_skl = nil ),
inference(component_clause,[status(thm)],[f438]) ).
fof(f449,plain,
! [X1] :
( ~ neq(X1,X1)
| ~ ssList(X1)
| ~ ssList(X1) ),
inference(destructive_equality_resolution,[status(thm)],[f219]) ).
fof(f450,plain,
! [X0] :
( ~ ssList(X0)
| ~ neq(X0,X0) ),
inference(duplicate_literals_removal,[status(thm)],[f449]) ).
fof(f466,plain,
( ~ sQ0_spl
| ~ ssList(tl(sK48_skl))
| ~ ssList(sK47_skl)
| ~ ssItem(hd(sK48_skl))
| app(tl(sK48_skl),cons(hd(sK48_skl),nil)) != sK47_skl
| ~ ssList(cons(hd(sK48_skl),nil)) ),
inference(destructive_equality_resolution,[status(thm)],[f429]) ).
fof(f479,plain,
sK50_skl = app(sK50_skl,nil),
inference(resolution,[status(thm)],[f421,f389]) ).
fof(f482,definition,
( sQ4_spl
<=> ssList(nil) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f484,plain,
( sQ4_spl
| ~ ssList(nil) ),
inference(component_clause,[status(thm)],[f482]) ).
fof(f495,plain,
neq(sK50_skl,nil),
inference(backward_demodulation,[status(thm)],[f422,f424]) ).
fof(f516,plain,
app(nil,nil) = nil,
inference(resolution,[status(thm)],[f223,f389]) ).
fof(f518,plain,
! [X0] :
( ssList(app(X0,nil))
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f245,f223]) ).
fof(f519,plain,
! [X0] :
( ~ ssList(X0)
| ssList(app(X0,sK49_skl)) ),
inference(resolution,[status(thm)],[f245,f420]) ).
fof(f524,plain,
( cons(hd(sK50_skl),tl(sK50_skl)) = sK50_skl
| sK50_skl = nil ),
inference(resolution,[status(thm)],[f374,f421]) ).
fof(f526,definition,
( sQ6_spl
<=> cons(hd(sK50_skl),tl(sK50_skl)) = sK50_skl ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f527,plain,
( ~ sQ6_spl
| cons(hd(sK50_skl),tl(sK50_skl)) = sK50_skl ),
inference(component_clause,[status(thm)],[f526]) ).
fof(f529,plain,
( sQ6_spl
| sQ3_spl ),
inference(split_clause,[status(thm)],[f524,f438,f526]) ).
fof(f541,plain,
( ~ sQ0_spl
| ~ ssList(tl(sK48_skl))
| ~ ssList(sK47_skl)
| ~ ssItem(hd(sK48_skl))
| app(tl(sK48_skl),cons(hd(sK48_skl),nil)) != sK47_skl
| ~ ssList(cons(hd(sK50_skl),nil)) ),
inference(forward_demodulation,[status(thm)],[f422,f466]) ).
fof(f542,plain,
( ~ sQ0_spl
| ~ ssList(tl(sK48_skl))
| ~ ssList(sK47_skl)
| ~ ssItem(hd(sK48_skl))
| app(tl(sK50_skl),cons(hd(sK48_skl),nil)) != sK47_skl
| ~ ssList(cons(hd(sK50_skl),nil)) ),
inference(forward_demodulation,[status(thm)],[f422,f541]) ).
fof(f543,plain,
( ~ sQ0_spl
| ~ ssList(tl(sK48_skl))
| ~ ssList(sK47_skl)
| ~ ssItem(hd(sK48_skl))
| app(tl(sK50_skl),cons(hd(sK50_skl),nil)) != sK47_skl
| ~ ssList(cons(hd(sK50_skl),nil)) ),
inference(forward_demodulation,[status(thm)],[f422,f542]) ).
fof(f544,plain,
( ~ sQ0_spl
| ~ ssList(tl(sK48_skl))
| ~ ssList(sK47_skl)
| ~ ssItem(hd(sK48_skl))
| app(tl(sK50_skl),cons(hd(sK50_skl),nil)) != sK49_skl
| ~ ssList(cons(hd(sK50_skl),nil)) ),
inference(forward_demodulation,[status(thm)],[f423,f543]) ).
fof(f545,plain,
( ~ sQ0_spl
| ~ ssList(tl(sK48_skl))
| ~ ssList(sK47_skl)
| ~ ssItem(hd(sK50_skl))
| app(tl(sK50_skl),cons(hd(sK50_skl),nil)) != sK49_skl
| ~ ssList(cons(hd(sK50_skl),nil)) ),
inference(forward_demodulation,[status(thm)],[f422,f544]) ).
fof(f546,plain,
( ~ sQ0_spl
| ~ ssList(tl(sK48_skl))
| ~ ssList(sK49_skl)
| ~ ssItem(hd(sK50_skl))
| app(tl(sK50_skl),cons(hd(sK50_skl),nil)) != sK49_skl
| ~ ssList(cons(hd(sK50_skl),nil)) ),
inference(forward_demodulation,[status(thm)],[f423,f545]) ).
fof(f547,plain,
( ~ sQ0_spl
| ~ ssList(tl(sK50_skl))
| ~ ssList(sK49_skl)
| ~ ssItem(hd(sK50_skl))
| app(tl(sK50_skl),cons(hd(sK50_skl),nil)) != sK49_skl
| ~ ssList(cons(hd(sK50_skl),nil)) ),
inference(forward_demodulation,[status(thm)],[f422,f546]) ).
fof(f548,plain,
( ~ sQ0_spl
| ~ ssList(cons(hd(sK50_skl),nil))
| ~ ssList(tl(sK50_skl))
| app(tl(sK50_skl),cons(hd(sK50_skl),nil)) != sK49_skl
| ~ ssItem(hd(sK50_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f547,f420]) ).
fof(f553,definition,
( sQ10_spl
<=> ssItem(hd(sK50_skl)) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f554,plain,
( ~ sQ10_spl
| ssItem(hd(sK50_skl)) ),
inference(component_clause,[status(thm)],[f553]) ).
fof(f559,definition,
( sQ12_spl
<=> ssList(tl(sK50_skl)) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f560,plain,
( ~ sQ12_spl
| ssList(tl(sK50_skl)) ),
inference(component_clause,[status(thm)],[f559]) ).
fof(f562,definition,
( sQ13_spl
<=> ssList(cons(hd(sK50_skl),nil)) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f566,plain,
( sQ1_spl
| ~ neq(nil,sK50_skl) ),
inference(forward_demodulation,[status(thm)],[f422,f433]) ).
fof(f570,plain,
! [X0] :
( ssList(cons(sK0_skl,X0))
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f103,f222]) ).
fof(f574,plain,
! [X0] :
( X0 = tl(cons(sK0_skl,X0))
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f103,f243]) ).
fof(f576,plain,
leq(sK0_skl,sK0_skl),
inference(resolution,[status(thm)],[f103,f255]) ).
fof(f577,plain,
! [X0] :
( ~ ssList(X0)
| cons(sK0_skl,X0) != nil ),
inference(resolution,[status(thm)],[f103,f235]) ).
fof(f578,plain,
! [X0] :
( ~ ssList(X0)
| cons(sK0_skl,X0) != X0 ),
inference(resolution,[status(thm)],[f103,f225]) ).
fof(f581,plain,
! [X0] :
( ~ ssList(X0)
| cons(sK0_skl,X0) = app(cons(sK0_skl,nil),X0) ),
inference(resolution,[status(thm)],[f380,f103]) ).
fof(f604,plain,
frontsegP(nil,nil),
inference(resolution,[status(thm)],[f286,f223]) ).
fof(f605,plain,
frontsegP(sK50_skl,sK50_skl),
inference(resolution,[status(thm)],[f286,f421]) ).
fof(f621,definition,
( sQ20_spl
<=> ssList(sK50_skl) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f623,plain,
( sQ20_spl
| ~ ssList(sK50_skl) ),
inference(component_clause,[status(thm)],[f621]) ).
fof(f628,plain,
( sQ20_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f623,f421]) ).
fof(f629,plain,
sQ20_spl,
inference(contradiction_clause,[status(thm)],[f628]) ).
fof(f642,plain,
! [X0] :
( cons(sK1_skl,X0) = app(cons(sK1_skl,nil),X0)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f104,f380]) ).
fof(f646,plain,
! [X0] :
( ~ ssList(X0)
| ssList(cons(sK1_skl,X0)) ),
inference(resolution,[status(thm)],[f104,f222]) ).
fof(f650,plain,
! [X0] :
( tl(cons(sK1_skl,X0)) = X0
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f104,f243]) ).
fof(f652,plain,
leq(sK1_skl,sK1_skl),
inference(resolution,[status(thm)],[f104,f255]) ).
fof(f653,plain,
! [X0] :
( ~ ssList(X0)
| nil != cons(sK1_skl,X0) ),
inference(resolution,[status(thm)],[f104,f235]) ).
fof(f654,plain,
! [X0] :
( ~ ssList(X0)
| cons(sK1_skl,X0) != X0 ),
inference(resolution,[status(thm)],[f104,f225]) ).
fof(f656,plain,
( sK50_skl = nil
| ssItem(hd(sK50_skl)) ),
inference(resolution,[status(thm)],[f237,f421]) ).
fof(f662,plain,
( sQ3_spl
| sQ10_spl ),
inference(split_clause,[status(thm)],[f656,f553,f438]) ).
fof(f700,definition,
( sQ27_spl
<=> ssList(sK49_skl) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f702,plain,
( sQ27_spl
| ~ ssList(sK49_skl) ),
inference(component_clause,[status(thm)],[f700]) ).
fof(f707,plain,
( sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f484,f223]) ).
fof(f708,plain,
sQ4_spl,
inference(contradiction_clause,[status(thm)],[f707]) ).
fof(f733,plain,
( sQ1_spl
| ~ ssList(sK50_skl)
| sK50_skl = nil
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f566,f220]) ).
fof(f734,plain,
( sQ1_spl
| ~ sQ20_spl
| sQ3_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f733,f482,f438,f621,f431]) ).
fof(f735,definition,
( sQ29_spl
<=> app(tl(sK50_skl),cons(hd(sK50_skl),nil)) = sK49_skl ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f738,plain,
( ~ sQ0_spl
| ~ sQ13_spl
| ~ sQ12_spl
| ~ sQ29_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f548,f553,f735,f559,f562,f428]) ).
fof(f747,plain,
ssList(app(nil,sK49_skl)),
inference(resolution,[status(thm)],[f519,f223]) ).
fof(f776,plain,
cons(sK0_skl,nil) != nil,
inference(resolution,[status(thm)],[f578,f223]) ).
fof(f777,plain,
cons(sK0_skl,sK50_skl) != sK50_skl,
inference(resolution,[status(thm)],[f578,f421]) ).
fof(f781,plain,
ssList(cons(sK0_skl,nil)),
inference(resolution,[status(thm)],[f570,f223]) ).
fof(f784,plain,
nil = tl(cons(sK0_skl,nil)),
inference(resolution,[status(thm)],[f574,f223]) ).
fof(f785,plain,
sK50_skl = tl(cons(sK0_skl,sK50_skl)),
inference(resolution,[status(thm)],[f574,f421]) ).
fof(f825,plain,
ssList(cons(sK1_skl,nil)),
inference(resolution,[status(thm)],[f646,f223]) ).
fof(f826,plain,
ssList(cons(sK1_skl,sK50_skl)),
inference(resolution,[status(thm)],[f646,f421]) ).
fof(f831,plain,
nil = tl(cons(sK1_skl,nil)),
inference(resolution,[status(thm)],[f650,f223]) ).
fof(f834,plain,
nil != cons(sK1_skl,nil),
inference(resolution,[status(thm)],[f654,f223]) ).
fof(f848,plain,
ssList(cons(sK1_skl,sK49_skl)),
inference(resolution,[status(thm)],[f420,f646]) ).
fof(f854,plain,
sK49_skl = tl(cons(sK0_skl,sK49_skl)),
inference(resolution,[status(thm)],[f420,f574]) ).
fof(f855,plain,
ssList(cons(sK0_skl,sK49_skl)),
inference(resolution,[status(thm)],[f420,f570]) ).
fof(f860,plain,
ssList(app(sK49_skl,sK49_skl)),
inference(resolution,[status(thm)],[f420,f519]) ).
fof(f873,plain,
frontsegP(sK49_skl,sK49_skl),
inference(resolution,[status(thm)],[f420,f286]) ).
fof(f884,plain,
sK49_skl = app(nil,sK49_skl),
inference(resolution,[status(thm)],[f420,f249]) ).
fof(f1025,plain,
( ~ sQ3_spl
| neq(nil,nil) ),
inference(backward_demodulation,[status(thm)],[f439,f495]) ).
fof(f1117,plain,
cons(sK1_skl,cons(sK0_skl,nil)) = app(cons(sK1_skl,nil),cons(sK0_skl,nil)),
inference(resolution,[status(thm)],[f781,f642]) ).
fof(f1121,plain,
app(cons(sK0_skl,nil),cons(sK0_skl,nil)) = cons(sK0_skl,cons(sK0_skl,nil)),
inference(resolution,[status(thm)],[f781,f581]) ).
fof(f1146,plain,
app(nil,cons(sK0_skl,nil)) = cons(sK0_skl,nil),
inference(resolution,[status(thm)],[f781,f249]) ).
fof(f1147,definition,
( sQ54_spl
<=> nil = cons(sK0_skl,nil) ),
introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition]) ).
fof(f1148,plain,
( ~ sQ54_spl
| nil = cons(sK0_skl,nil) ),
inference(component_clause,[status(thm)],[f1147]) ).
fof(f1200,plain,
( ~ sQ54_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1148,f776]) ).
fof(f1201,plain,
~ sQ54_spl,
inference(contradiction_clause,[status(thm)],[f1200]) ).
fof(f1205,definition,
( sQ68_spl
<=> ssList(cons(sK0_skl,nil)) ),
introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition]) ).
fof(f1207,plain,
( sQ68_spl
| ~ ssList(cons(sK0_skl,nil)) ),
inference(component_clause,[status(thm)],[f1205]) ).
fof(f1267,plain,
( ~ sQ3_spl
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f1025,f450]) ).
fof(f1268,plain,
( ~ sQ3_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f1267,f482,f438]) ).
fof(f1278,plain,
( sQ68_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1207,f781]) ).
fof(f1279,plain,
sQ68_spl,
inference(contradiction_clause,[status(thm)],[f1278]) ).
fof(f1401,plain,
! [X0] :
( ~ sQ10_spl
| cons(hd(sK50_skl),X0) = app(cons(hd(sK50_skl),nil),X0)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f554,f380]) ).
fof(f1405,plain,
! [X0] :
( ~ sQ10_spl
| ~ ssList(X0)
| ssList(cons(hd(sK50_skl),X0)) ),
inference(resolution,[status(thm)],[f554,f222]) ).
fof(f1459,definition,
( sQ91_spl
<=> nil = cons(sK1_skl,nil) ),
introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition]) ).
fof(f1460,plain,
( ~ sQ91_spl
| cons(sK1_skl,nil) = nil ),
inference(component_clause,[status(thm)],[f1459]) ).
fof(f1570,definition,
( sQ108_spl
<=> nil = cons(sK1_skl,sK50_skl) ),
introduced(definition,[new_symbols(definition,[sQ108_spl])],[split_symbol_definition]) ).
fof(f1571,plain,
( ~ sQ108_spl
| cons(sK1_skl,sK50_skl) = nil ),
inference(component_clause,[status(thm)],[f1570]) ).
fof(f1637,definition,
( sQ125_spl
<=> ssList(cons(sK1_skl,nil)) ),
introduced(definition,[new_symbols(definition,[sQ125_spl])],[split_symbol_definition]) ).
fof(f1639,plain,
( sQ125_spl
| ~ ssList(cons(sK1_skl,nil)) ),
inference(component_clause,[status(thm)],[f1637]) ).
fof(f1664,plain,
( sQ125_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1639,f825]) ).
fof(f1665,plain,
sQ125_spl,
inference(contradiction_clause,[status(thm)],[f1664]) ).
fof(f1701,definition,
( sQ138_spl
<=> ssList(cons(sK1_skl,sK50_skl)) ),
introduced(definition,[new_symbols(definition,[sQ138_spl])],[split_symbol_definition]) ).
fof(f1703,plain,
( sQ138_spl
| ~ ssList(cons(sK1_skl,sK50_skl)) ),
inference(component_clause,[status(thm)],[f1701]) ).
fof(f2184,definition,
( sQ192_spl
<=> nil = app(nil,nil) ),
introduced(definition,[new_symbols(definition,[sQ192_spl])],[split_symbol_definition]) ).
fof(f2186,plain,
( sQ192_spl
| nil != app(nil,nil) ),
inference(component_clause,[status(thm)],[f2184]) ).
fof(f2217,plain,
! [X0] :
( ~ sQ10_spl
| ~ ssList(X0)
| sK50_skl != app(cons(hd(sK50_skl),nil),X0)
| app(X0,cons(hd(sK50_skl),nil)) = sK49_skl ),
inference(resolution,[status(thm)],[f426,f554]) ).
fof(f2269,definition,
( sQ203_spl
<=> ssItem(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ203_spl])],[split_symbol_definition]) ).
fof(f2271,plain,
( sQ203_spl
| ~ ssItem(sK0_skl) ),
inference(component_clause,[status(thm)],[f2269]) ).
fof(f2287,plain,
( sQ203_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2271,f103]) ).
fof(f2288,plain,
sQ203_spl,
inference(contradiction_clause,[status(thm)],[f2287]) ).
fof(f2381,definition,
( sQ223_spl
<=> totalorderedP(nil) ),
introduced(definition,[new_symbols(definition,[sQ223_spl])],[split_symbol_definition]) ).
fof(f2383,plain,
( sQ223_spl
| ~ totalorderedP(nil) ),
inference(component_clause,[status(thm)],[f2381]) ).
fof(f2397,plain,
( sQ192_spl
| nil != nil ),
inference(forward_demodulation,[status(thm)],[f516,f2186]) ).
fof(f2398,plain,
( sQ192_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f2397]) ).
fof(f2399,plain,
sQ192_spl,
inference(contradiction_clause,[status(thm)],[f2398]) ).
fof(f2443,plain,
( sQ138_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1703,f826]) ).
fof(f2444,plain,
sQ138_spl,
inference(contradiction_clause,[status(thm)],[f2443]) ).
fof(f2551,plain,
cons(sK1_skl,sK49_skl) != sK49_skl,
inference(resolution,[status(thm)],[f420,f654]) ).
fof(f2552,plain,
sK49_skl = tl(cons(sK1_skl,sK49_skl)),
inference(resolution,[status(thm)],[f420,f650]) ).
fof(f2562,plain,
sK49_skl != cons(sK0_skl,sK49_skl),
inference(resolution,[status(thm)],[f420,f578]) ).
fof(f2564,plain,
ssList(app(sK49_skl,nil)),
inference(resolution,[status(thm)],[f420,f518]) ).
fof(f2581,plain,
sK49_skl = app(sK49_skl,nil),
inference(resolution,[status(thm)],[f420,f389]) ).
fof(f4105,plain,
( ~ sQ10_spl
| ssList(cons(hd(sK50_skl),nil)) ),
inference(resolution,[status(thm)],[f1405,f223]) ).
fof(f4108,plain,
( ~ sQ10_spl
| sQ13_spl ),
inference(split_clause,[status(thm)],[f4105,f562,f553]) ).
fof(f4147,definition,
( sQ416_spl
<=> ssItem(sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ416_spl])],[split_symbol_definition]) ).
fof(f4149,plain,
( sQ416_spl
| ~ ssItem(sK1_skl) ),
inference(component_clause,[status(thm)],[f4147]) ).
fof(f4159,plain,
( sQ416_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4149,f104]) ).
fof(f4160,plain,
sQ416_spl,
inference(contradiction_clause,[status(thm)],[f4159]) ).
fof(f4520,definition,
( sQ452_spl
<=> frontsegP(sK50_skl,sK50_skl) ),
introduced(definition,[new_symbols(definition,[sQ452_spl])],[split_symbol_definition]) ).
fof(f4522,plain,
( sQ452_spl
| ~ frontsegP(sK50_skl,sK50_skl) ),
inference(component_clause,[status(thm)],[f4520]) ).
fof(f4524,plain,
( sQ452_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4522,f605]) ).
fof(f4525,plain,
sQ452_spl,
inference(contradiction_clause,[status(thm)],[f4524]) ).
fof(f4789,definition,
( sQ493_spl
<=> cons(sK0_skl,sK50_skl) = sK50_skl ),
introduced(definition,[new_symbols(definition,[sQ493_spl])],[split_symbol_definition]) ).
fof(f4790,plain,
( ~ sQ493_spl
| cons(sK0_skl,sK50_skl) = sK50_skl ),
inference(component_clause,[status(thm)],[f4789]) ).
fof(f4794,plain,
( ~ sQ493_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4790,f777]) ).
fof(f4795,plain,
~ sQ493_spl,
inference(contradiction_clause,[status(thm)],[f4794]) ).
fof(f4812,plain,
( ~ sQ91_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1460,f834]) ).
fof(f4813,plain,
~ sQ91_spl,
inference(contradiction_clause,[status(thm)],[f4812]) ).
fof(f4861,definition,
( sQ503_spl
<=> frontsegP(nil,nil) ),
introduced(definition,[new_symbols(definition,[sQ503_spl])],[split_symbol_definition]) ).
fof(f4863,plain,
( sQ503_spl
| ~ frontsegP(nil,nil) ),
inference(component_clause,[status(thm)],[f4861]) ).
fof(f5104,definition,
( sQ530_spl
<=> sK50_skl = app(sK50_skl,nil) ),
introduced(definition,[new_symbols(definition,[sQ530_spl])],[split_symbol_definition]) ).
fof(f5106,plain,
( sQ530_spl
| sK50_skl != app(sK50_skl,nil) ),
inference(component_clause,[status(thm)],[f5104]) ).
fof(f5142,plain,
( sQ530_spl
| sK50_skl != sK50_skl ),
inference(forward_demodulation,[status(thm)],[f479,f5106]) ).
fof(f5143,plain,
( sQ530_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f5142]) ).
fof(f5144,plain,
sQ530_spl,
inference(contradiction_clause,[status(thm)],[f5143]) ).
fof(f5197,definition,
! [X0] :
( sQ550_spl
<=> ( app(X0,sK49_skl) != app(X0,sK49_skl)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ550_spl])],[split_symbol_definition]) ).
fof(f5198,plain,
! [X0] :
( ~ sQ550_spl
| app(X0,sK49_skl) != app(X0,sK49_skl)
| ~ ssList(X0) ),
inference(component_clause,[status(thm)],[f5197]) ).
fof(f5211,plain,
! [X0] :
( ~ sQ550_spl
| ~ ssList(X0) ),
inference(trivial_equality_resolution,[status(thm)],[f5198]) ).
fof(f5233,definition,
( sQ558_spl
<=> frontsegP(sK49_skl,sK49_skl) ),
introduced(definition,[new_symbols(definition,[sQ558_spl])],[split_symbol_definition]) ).
fof(f5235,plain,
( sQ558_spl
| ~ frontsegP(sK49_skl,sK49_skl) ),
inference(component_clause,[status(thm)],[f5233]) ).
fof(f5237,plain,
( sQ558_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5235,f873]) ).
fof(f5238,plain,
sQ558_spl,
inference(contradiction_clause,[status(thm)],[f5237]) ).
fof(f5720,definition,
( sQ631_spl
<=> ssList(cons(sK1_skl,sK49_skl)) ),
introduced(definition,[new_symbols(definition,[sQ631_spl])],[split_symbol_definition]) ).
fof(f5722,plain,
( sQ631_spl
| ~ ssList(cons(sK1_skl,sK49_skl)) ),
inference(component_clause,[status(thm)],[f5720]) ).
fof(f5725,plain,
( sQ631_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5722,f848]) ).
fof(f5726,plain,
sQ631_spl,
inference(contradiction_clause,[status(thm)],[f5725]) ).
fof(f6500,definition,
( sQ713_spl
<=> ssList(app(sK49_skl,sK49_skl)) ),
introduced(definition,[new_symbols(definition,[sQ713_spl])],[split_symbol_definition]) ).
fof(f6502,plain,
( sQ713_spl
| ~ ssList(app(sK49_skl,sK49_skl)) ),
inference(component_clause,[status(thm)],[f6500]) ).
fof(f6507,plain,
( sQ713_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6502,f860]) ).
fof(f6508,plain,
sQ713_spl,
inference(contradiction_clause,[status(thm)],[f6507]) ).
fof(f6527,plain,
( sQ27_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f702,f420]) ).
fof(f6528,plain,
sQ27_spl,
inference(contradiction_clause,[status(thm)],[f6527]) ).
fof(f6630,plain,
nil != cons(sK0_skl,app(nil,sK49_skl)),
inference(resolution,[status(thm)],[f747,f577]) ).
fof(f7020,definition,
( sQ761_spl
<=> cons(sK0_skl,sK49_skl) = nil ),
introduced(definition,[new_symbols(definition,[sQ761_spl])],[split_symbol_definition]) ).
fof(f7021,plain,
( ~ sQ761_spl
| nil = cons(sK0_skl,sK49_skl) ),
inference(component_clause,[status(thm)],[f7020]) ).
fof(f7574,definition,
( sQ843_spl
<=> ssList(cons(sK0_skl,sK49_skl)) ),
introduced(definition,[new_symbols(definition,[sQ843_spl])],[split_symbol_definition]) ).
fof(f7576,plain,
( sQ843_spl
| ~ ssList(cons(sK0_skl,sK49_skl)) ),
inference(component_clause,[status(thm)],[f7574]) ).
fof(f7582,plain,
( sQ843_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7576,f855]) ).
fof(f7583,plain,
sQ843_spl,
inference(contradiction_clause,[status(thm)],[f7582]) ).
fof(f7687,definition,
( sQ863_spl
<=> sK1_skl = sK0_skl ),
introduced(definition,[new_symbols(definition,[sQ863_spl])],[split_symbol_definition]) ).
fof(f7688,plain,
( ~ sQ863_spl
| sK1_skl = sK0_skl ),
inference(component_clause,[status(thm)],[f7687]) ).
fof(f7691,plain,
( ~ sQ863_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7688,f105]) ).
fof(f7692,plain,
~ sQ863_spl,
inference(contradiction_clause,[status(thm)],[f7691]) ).
fof(f8284,plain,
( ~ sQ10_spl
| ~ sQ12_spl
| sK50_skl != app(cons(hd(sK50_skl),nil),tl(sK50_skl))
| app(tl(sK50_skl),cons(hd(sK50_skl),nil)) = sK49_skl ),
inference(resolution,[status(thm)],[f560,f2217]) ).
fof(f8312,plain,
( ~ sQ10_spl
| ~ sQ12_spl
| cons(hd(sK50_skl),tl(sK50_skl)) = app(cons(hd(sK50_skl),nil),tl(sK50_skl)) ),
inference(resolution,[status(thm)],[f560,f1401]) ).
fof(f8421,plain,
( ~ sQ10_spl
| ~ sQ12_spl
| ~ sQ6_spl
| app(cons(hd(sK50_skl),nil),tl(sK50_skl)) = sK50_skl ),
inference(forward_demodulation,[status(thm)],[f527,f8312]) ).
fof(f8434,definition,
( sQ965_spl
<=> sK50_skl = app(cons(hd(sK50_skl),nil),tl(sK50_skl)) ),
introduced(definition,[new_symbols(definition,[sQ965_spl])],[split_symbol_definition]) ).
fof(f8436,plain,
( sQ965_spl
| sK50_skl != app(cons(hd(sK50_skl),nil),tl(sK50_skl)) ),
inference(component_clause,[status(thm)],[f8434]) ).
fof(f8437,plain,
( ~ sQ10_spl
| ~ sQ12_spl
| ~ sQ965_spl
| sQ29_spl ),
inference(split_clause,[status(thm)],[f8284,f735,f8434,f559,f553]) ).
fof(f8922,definition,
( sQ1028_spl
<=> ssList(app(sK49_skl,nil)) ),
introduced(definition,[new_symbols(definition,[sQ1028_spl])],[split_symbol_definition]) ).
fof(f8924,plain,
( sQ1028_spl
| ~ ssList(app(sK49_skl,nil)) ),
inference(component_clause,[status(thm)],[f8922]) ).
fof(f8929,plain,
( sQ1028_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8924,f2564]) ).
fof(f8930,plain,
sQ1028_spl,
inference(contradiction_clause,[status(thm)],[f8929]) ).
fof(f9278,definition,
( sQ1053_spl
<=> app(sK49_skl,nil) = sK49_skl ),
introduced(definition,[new_symbols(definition,[sQ1053_spl])],[split_symbol_definition]) ).
fof(f9280,plain,
( sQ1053_spl
| app(sK49_skl,nil) != sK49_skl ),
inference(component_clause,[status(thm)],[f9278]) ).
fof(f9315,plain,
( sQ1053_spl
| sK49_skl != sK49_skl ),
inference(forward_demodulation,[status(thm)],[f2581,f9280]) ).
fof(f9316,plain,
( sQ1053_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f9315]) ).
fof(f9317,plain,
sQ1053_spl,
inference(contradiction_clause,[status(thm)],[f9316]) ).
fof(f9570,definition,
( sQ1100_spl
<=> tl(sK50_skl) = tl(sK50_skl) ),
introduced(definition,[new_symbols(definition,[sQ1100_spl])],[split_symbol_definition]) ).
fof(f9572,plain,
( sQ1100_spl
| tl(sK50_skl) != tl(sK50_skl) ),
inference(component_clause,[status(thm)],[f9570]) ).
fof(f9611,plain,
( sQ1100_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f9572]) ).
fof(f9612,plain,
sQ1100_spl,
inference(contradiction_clause,[status(thm)],[f9611]) ).
fof(f9633,plain,
cons(sK1_skl,sK50_skl) != nil,
inference(resolution,[status(thm)],[f653,f421]) ).
fof(f9643,plain,
( ~ sQ108_spl
| nil != nil ),
inference(forward_demodulation,[status(thm)],[f1571,f9633]) ).
fof(f9644,plain,
( ~ sQ108_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f9643]) ).
fof(f9645,plain,
~ sQ108_spl,
inference(contradiction_clause,[status(thm)],[f9644]) ).
fof(f10014,definition,
( sQ1154_spl
<=> app(cons(sK0_skl,nil),cons(sK0_skl,nil)) = cons(sK0_skl,cons(sK0_skl,nil)) ),
introduced(definition,[new_symbols(definition,[sQ1154_spl])],[split_symbol_definition]) ).
fof(f10016,plain,
( sQ1154_spl
| app(cons(sK0_skl,nil),cons(sK0_skl,nil)) != cons(sK0_skl,cons(sK0_skl,nil)) ),
inference(component_clause,[status(thm)],[f10014]) ).
fof(f10077,plain,
( sQ1154_spl
| cons(sK0_skl,cons(sK0_skl,nil)) != cons(sK0_skl,cons(sK0_skl,nil)) ),
inference(forward_demodulation,[status(thm)],[f1121,f10016]) ).
fof(f10078,plain,
( sQ1154_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f10077]) ).
fof(f10079,plain,
sQ1154_spl,
inference(contradiction_clause,[status(thm)],[f10078]) ).
fof(f10109,definition,
( sQ1174_spl
<=> app(sK50_skl,cons(sK0_skl,nil)) = app(sK50_skl,cons(sK0_skl,nil)) ),
introduced(definition,[new_symbols(definition,[sQ1174_spl])],[split_symbol_definition]) ).
fof(f10111,plain,
( sQ1174_spl
| app(sK50_skl,cons(sK0_skl,nil)) != app(sK50_skl,cons(sK0_skl,nil)) ),
inference(component_clause,[status(thm)],[f10109]) ).
fof(f10141,plain,
( sQ1174_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f10111]) ).
fof(f10142,plain,
sQ1174_spl,
inference(contradiction_clause,[status(thm)],[f10141]) ).
fof(f10158,definition,
( sQ1182_spl
<=> app(sK49_skl,cons(sK0_skl,nil)) = app(sK49_skl,cons(sK0_skl,nil)) ),
introduced(definition,[new_symbols(definition,[sQ1182_spl])],[split_symbol_definition]) ).
fof(f10160,plain,
( sQ1182_spl
| app(sK49_skl,cons(sK0_skl,nil)) != app(sK49_skl,cons(sK0_skl,nil)) ),
inference(component_clause,[status(thm)],[f10158]) ).
fof(f10207,plain,
( sQ1182_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f10160]) ).
fof(f10208,plain,
sQ1182_spl,
inference(contradiction_clause,[status(thm)],[f10207]) ).
fof(f10263,definition,
( sQ1204_spl
<=> cons(sK1_skl,cons(sK0_skl,nil)) = app(cons(sK1_skl,nil),cons(sK0_skl,nil)) ),
introduced(definition,[new_symbols(definition,[sQ1204_spl])],[split_symbol_definition]) ).
fof(f10265,plain,
( sQ1204_spl
| cons(sK1_skl,cons(sK0_skl,nil)) != app(cons(sK1_skl,nil),cons(sK0_skl,nil)) ),
inference(component_clause,[status(thm)],[f10263]) ).
fof(f10272,plain,
( sQ1204_spl
| cons(sK1_skl,cons(sK0_skl,nil)) != cons(sK1_skl,cons(sK0_skl,nil)) ),
inference(forward_demodulation,[status(thm)],[f1117,f10265]) ).
fof(f10273,plain,
( sQ1204_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f10272]) ).
fof(f10274,plain,
sQ1204_spl,
inference(contradiction_clause,[status(thm)],[f10273]) ).
fof(f10322,definition,
( sQ1214_spl
<=> cons(sK0_skl,nil) = app(nil,cons(sK0_skl,nil)) ),
introduced(definition,[new_symbols(definition,[sQ1214_spl])],[split_symbol_definition]) ).
fof(f10324,plain,
( sQ1214_spl
| cons(sK0_skl,nil) != app(nil,cons(sK0_skl,nil)) ),
inference(component_clause,[status(thm)],[f10322]) ).
fof(f10339,plain,
( sQ1214_spl
| cons(sK0_skl,nil) != cons(sK0_skl,nil) ),
inference(forward_demodulation,[status(thm)],[f1146,f10324]) ).
fof(f10340,plain,
( sQ1214_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f10339]) ).
fof(f10341,plain,
sQ1214_spl,
inference(contradiction_clause,[status(thm)],[f10340]) ).
fof(f10367,definition,
( sQ1220_spl
<=> app(cons(sK1_skl,sK50_skl),cons(sK0_skl,nil)) = app(cons(sK1_skl,sK50_skl),cons(sK0_skl,nil)) ),
introduced(definition,[new_symbols(definition,[sQ1220_spl])],[split_symbol_definition]) ).
fof(f10369,plain,
( sQ1220_spl
| app(cons(sK1_skl,sK50_skl),cons(sK0_skl,nil)) != app(cons(sK1_skl,sK50_skl),cons(sK0_skl,nil)) ),
inference(component_clause,[status(thm)],[f10367]) ).
fof(f10407,plain,
( sQ1220_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f10369]) ).
fof(f10408,plain,
sQ1220_spl,
inference(contradiction_clause,[status(thm)],[f10407]) ).
fof(f10542,definition,
( sQ1252_spl
<=> sK49_skl = cons(sK0_skl,sK49_skl) ),
introduced(definition,[new_symbols(definition,[sQ1252_spl])],[split_symbol_definition]) ).
fof(f10543,plain,
( ~ sQ1252_spl
| sK49_skl = cons(sK0_skl,sK49_skl) ),
inference(component_clause,[status(thm)],[f10542]) ).
fof(f10549,plain,
( ~ sQ1252_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f10543,f2562]) ).
fof(f10550,plain,
~ sQ1252_spl,
inference(contradiction_clause,[status(thm)],[f10549]) ).
fof(f10906,definition,
( sQ1312_spl
<=> tl(cons(sK0_skl,sK49_skl)) = cons(sK0_skl,sK49_skl) ),
introduced(definition,[new_symbols(definition,[sQ1312_spl])],[split_symbol_definition]) ).
fof(f10907,plain,
( ~ sQ1312_spl
| tl(cons(sK0_skl,sK49_skl)) = cons(sK0_skl,sK49_skl) ),
inference(component_clause,[status(thm)],[f10906]) ).
fof(f10913,definition,
( sQ1314_spl
<=> tl(cons(sK0_skl,nil)) = cons(sK0_skl,nil) ),
introduced(definition,[new_symbols(definition,[sQ1314_spl])],[split_symbol_definition]) ).
fof(f10914,plain,
( ~ sQ1314_spl
| tl(cons(sK0_skl,nil)) = cons(sK0_skl,nil) ),
inference(component_clause,[status(thm)],[f10913]) ).
fof(f10920,definition,
( sQ1316_spl
<=> tl(cons(sK0_skl,sK50_skl)) = cons(sK0_skl,sK50_skl) ),
introduced(definition,[new_symbols(definition,[sQ1316_spl])],[split_symbol_definition]) ).
fof(f10921,plain,
( ~ sQ1316_spl
| tl(cons(sK0_skl,sK50_skl)) = cons(sK0_skl,sK50_skl) ),
inference(component_clause,[status(thm)],[f10920]) ).
fof(f10953,definition,
( sQ1325_spl
<=> tl(cons(sK1_skl,nil)) = cons(sK1_skl,nil) ),
introduced(definition,[new_symbols(definition,[sQ1325_spl])],[split_symbol_definition]) ).
fof(f10954,plain,
( ~ sQ1325_spl
| tl(cons(sK1_skl,nil)) = cons(sK1_skl,nil) ),
inference(component_clause,[status(thm)],[f10953]) ).
fof(f10960,definition,
( sQ1327_spl
<=> tl(cons(sK1_skl,sK49_skl)) = cons(sK1_skl,sK49_skl) ),
introduced(definition,[new_symbols(definition,[sQ1327_spl])],[split_symbol_definition]) ).
fof(f10961,plain,
( ~ sQ1327_spl
| tl(cons(sK1_skl,sK49_skl)) = cons(sK1_skl,sK49_skl) ),
inference(component_clause,[status(thm)],[f10960]) ).
fof(f11005,plain,
( ~ sQ1314_spl
| nil = cons(sK0_skl,nil) ),
inference(forward_demodulation,[status(thm)],[f784,f10914]) ).
fof(f11006,plain,
( ~ sQ1314_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11005,f776]) ).
fof(f11007,plain,
~ sQ1314_spl,
inference(contradiction_clause,[status(thm)],[f11006]) ).
fof(f11012,plain,
( ~ sQ1312_spl
| sK49_skl = cons(sK0_skl,sK49_skl) ),
inference(forward_demodulation,[status(thm)],[f854,f10907]) ).
fof(f11013,plain,
( ~ sQ1312_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11012,f2562]) ).
fof(f11014,plain,
~ sQ1312_spl,
inference(contradiction_clause,[status(thm)],[f11013]) ).
fof(f11016,plain,
( ~ sQ1316_spl
| sK50_skl = cons(sK0_skl,sK50_skl) ),
inference(forward_demodulation,[status(thm)],[f785,f10921]) ).
fof(f11017,plain,
( ~ sQ1316_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11016,f777]) ).
fof(f11018,plain,
~ sQ1316_spl,
inference(contradiction_clause,[status(thm)],[f11017]) ).
fof(f11028,plain,
( ~ sQ1325_spl
| nil = cons(sK1_skl,nil) ),
inference(forward_demodulation,[status(thm)],[f831,f10954]) ).
fof(f11029,plain,
( ~ sQ1325_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11028,f834]) ).
fof(f11030,plain,
~ sQ1325_spl,
inference(contradiction_clause,[status(thm)],[f11029]) ).
fof(f11035,plain,
( ~ sQ1327_spl
| sK49_skl = cons(sK1_skl,sK49_skl) ),
inference(forward_demodulation,[status(thm)],[f2552,f10961]) ).
fof(f11036,plain,
( ~ sQ1327_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11035,f2551]) ).
fof(f11037,plain,
~ sQ1327_spl,
inference(contradiction_clause,[status(thm)],[f11036]) ).
fof(f11076,definition,
( sQ1342_spl
<=> app(sK43_skl(cons(sK0_skl,nil)),cons(sK0_skl,nil)) = app(sK43_skl(cons(sK0_skl,nil)),cons(sK0_skl,nil)) ),
introduced(definition,[new_symbols(definition,[sQ1342_spl])],[split_symbol_definition]) ).
fof(f11078,plain,
( sQ1342_spl
| app(sK43_skl(cons(sK0_skl,nil)),cons(sK0_skl,nil)) != app(sK43_skl(cons(sK0_skl,nil)),cons(sK0_skl,nil)) ),
inference(component_clause,[status(thm)],[f11076]) ).
fof(f11120,plain,
( sQ1342_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f11078]) ).
fof(f11121,plain,
sQ1342_spl,
inference(contradiction_clause,[status(thm)],[f11120]) ).
fof(f12019,definition,
( sQ1473_spl
<=> app(app(sK50_skl,sK50_skl),cons(sK0_skl,nil)) = app(app(sK50_skl,sK50_skl),cons(sK0_skl,nil)) ),
introduced(definition,[new_symbols(definition,[sQ1473_spl])],[split_symbol_definition]) ).
fof(f12021,plain,
( sQ1473_spl
| app(app(sK50_skl,sK50_skl),cons(sK0_skl,nil)) != app(app(sK50_skl,sK50_skl),cons(sK0_skl,nil)) ),
inference(component_clause,[status(thm)],[f12019]) ).
fof(f12045,plain,
( sQ1473_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f12021]) ).
fof(f12046,plain,
sQ1473_spl,
inference(contradiction_clause,[status(thm)],[f12045]) ).
fof(f12887,plain,
( sQ223_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2383,f339]) ).
fof(f12888,plain,
sQ223_spl,
inference(contradiction_clause,[status(thm)],[f12887]) ).
fof(f13951,definition,
( sQ1730_spl
<=> app(cons(sK0_skl,sK50_skl),cons(sK0_skl,nil)) = app(cons(sK0_skl,sK50_skl),cons(sK0_skl,nil)) ),
introduced(definition,[new_symbols(definition,[sQ1730_spl])],[split_symbol_definition]) ).
fof(f13953,plain,
( sQ1730_spl
| app(cons(sK0_skl,sK50_skl),cons(sK0_skl,nil)) != app(cons(sK0_skl,sK50_skl),cons(sK0_skl,nil)) ),
inference(component_clause,[status(thm)],[f13951]) ).
fof(f13955,plain,
( sQ1730_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f13953]) ).
fof(f13956,plain,
sQ1730_spl,
inference(contradiction_clause,[status(thm)],[f13955]) ).
fof(f14223,definition,
( sQ1763_spl
<=> singletonP(nil) ),
introduced(definition,[new_symbols(definition,[sQ1763_spl])],[split_symbol_definition]) ).
fof(f14224,plain,
( ~ sQ1763_spl
| singletonP(nil) ),
inference(component_clause,[status(thm)],[f14223]) ).
fof(f14241,plain,
( ~ sQ1763_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f14224,f280]) ).
fof(f14242,plain,
~ sQ1763_spl,
inference(contradiction_clause,[status(thm)],[f14241]) ).
fof(f15348,definition,
( sQ1868_spl
<=> app(tl(sK50_skl),cons(sK0_skl,nil)) = app(tl(sK50_skl),cons(sK0_skl,nil)) ),
introduced(definition,[new_symbols(definition,[sQ1868_spl])],[split_symbol_definition]) ).
fof(f15350,plain,
( sQ1868_spl
| app(tl(sK50_skl),cons(sK0_skl,nil)) != app(tl(sK50_skl),cons(sK0_skl,nil)) ),
inference(component_clause,[status(thm)],[f15348]) ).
fof(f15385,plain,
( sQ1868_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f15350]) ).
fof(f15386,plain,
sQ1868_spl,
inference(contradiction_clause,[status(thm)],[f15385]) ).
fof(f16133,plain,
( sQ503_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4863,f604]) ).
fof(f16134,plain,
sQ503_spl,
inference(contradiction_clause,[status(thm)],[f16133]) ).
fof(f16809,definition,
( sQ2080_spl
<=> leq(sK0_skl,sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ2080_spl])],[split_symbol_definition]) ).
fof(f16811,plain,
( sQ2080_spl
| ~ leq(sK0_skl,sK0_skl) ),
inference(component_clause,[status(thm)],[f16809]) ).
fof(f16825,plain,
( sQ2080_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f16811,f576]) ).
fof(f16826,plain,
sQ2080_spl,
inference(contradiction_clause,[status(thm)],[f16825]) ).
fof(f16950,definition,
( sQ2112_spl
<=> tl(sK49_skl) = tl(sK49_skl) ),
introduced(definition,[new_symbols(definition,[sQ2112_spl])],[split_symbol_definition]) ).
fof(f16952,plain,
( sQ2112_spl
| tl(sK49_skl) != tl(sK49_skl) ),
inference(component_clause,[status(thm)],[f16950]) ).
fof(f16957,plain,
( sQ2112_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f16952]) ).
fof(f16958,plain,
sQ2112_spl,
inference(contradiction_clause,[status(thm)],[f16957]) ).
fof(f17034,definition,
( sQ2121_spl
<=> leq(sK1_skl,sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ2121_spl])],[split_symbol_definition]) ).
fof(f17036,plain,
( sQ2121_spl
| ~ leq(sK1_skl,sK1_skl) ),
inference(component_clause,[status(thm)],[f17034]) ).
fof(f17058,plain,
( sQ2121_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f17036,f652]) ).
fof(f17059,plain,
sQ2121_spl,
inference(contradiction_clause,[status(thm)],[f17058]) ).
fof(f21050,definition,
( sQ2667_spl
<=> tl(cons(sK0_skl,nil)) = cons(sK1_skl,nil) ),
introduced(definition,[new_symbols(definition,[sQ2667_spl])],[split_symbol_definition]) ).
fof(f21051,plain,
( ~ sQ2667_spl
| tl(cons(sK0_skl,nil)) = cons(sK1_skl,nil) ),
inference(component_clause,[status(thm)],[f21050]) ).
fof(f21137,plain,
( ~ sQ2667_spl
| nil = cons(sK1_skl,nil) ),
inference(forward_demodulation,[status(thm)],[f784,f21051]) ).
fof(f21138,plain,
( ~ sQ2667_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f21137,f834]) ).
fof(f21139,plain,
~ sQ2667_spl,
inference(contradiction_clause,[status(thm)],[f21138]) ).
fof(f21522,plain,
( nil = sK50_skl
| ssList(tl(sK50_skl)) ),
inference(resolution,[status(thm)],[f241,f421]) ).
fof(f21526,plain,
( sQ3_spl
| sQ12_spl ),
inference(split_clause,[status(thm)],[f21522,f559,f438]) ).
fof(f21597,definition,
( sQ2700_spl
<=> app(cons(hd(sK50_skl),nil),cons(sK0_skl,nil)) = app(cons(hd(sK50_skl),nil),cons(sK0_skl,nil)) ),
introduced(definition,[new_symbols(definition,[sQ2700_spl])],[split_symbol_definition]) ).
fof(f21599,plain,
( sQ2700_spl
| app(cons(hd(sK50_skl),nil),cons(sK0_skl,nil)) != app(cons(hd(sK50_skl),nil),cons(sK0_skl,nil)) ),
inference(component_clause,[status(thm)],[f21597]) ).
fof(f21610,plain,
( sQ2700_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f21599]) ).
fof(f21611,plain,
sQ2700_spl,
inference(contradiction_clause,[status(thm)],[f21610]) ).
fof(f21664,definition,
( sQ2707_spl
<=> app(cons(hd(sK50_skl),nil),cons(sK1_skl,nil)) = app(cons(hd(sK50_skl),nil),cons(sK1_skl,nil)) ),
introduced(definition,[new_symbols(definition,[sQ2707_spl])],[split_symbol_definition]) ).
fof(f21666,plain,
( sQ2707_spl
| app(cons(hd(sK50_skl),nil),cons(sK1_skl,nil)) != app(cons(hd(sK50_skl),nil),cons(sK1_skl,nil)) ),
inference(component_clause,[status(thm)],[f21664]) ).
fof(f21681,plain,
( sQ2707_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f21666]) ).
fof(f21682,plain,
sQ2707_spl,
inference(contradiction_clause,[status(thm)],[f21681]) ).
fof(f21764,definition,
( sQ2723_spl
<=> app(sK50_skl,cons(sK1_skl,nil)) = app(sK50_skl,cons(sK1_skl,nil)) ),
introduced(definition,[new_symbols(definition,[sQ2723_spl])],[split_symbol_definition]) ).
fof(f21766,plain,
( sQ2723_spl
| app(sK50_skl,cons(sK1_skl,nil)) != app(sK50_skl,cons(sK1_skl,nil)) ),
inference(component_clause,[status(thm)],[f21764]) ).
fof(f21773,plain,
( sQ2723_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f21766]) ).
fof(f21774,plain,
sQ2723_spl,
inference(contradiction_clause,[status(thm)],[f21773]) ).
fof(f21842,definition,
( sQ2737_spl
<=> app(tl(sK50_skl),cons(sK1_skl,nil)) = app(tl(sK50_skl),cons(sK1_skl,nil)) ),
introduced(definition,[new_symbols(definition,[sQ2737_spl])],[split_symbol_definition]) ).
fof(f21844,plain,
( sQ2737_spl
| app(tl(sK50_skl),cons(sK1_skl,nil)) != app(tl(sK50_skl),cons(sK1_skl,nil)) ),
inference(component_clause,[status(thm)],[f21842]) ).
fof(f21847,plain,
( sQ2737_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f21844]) ).
fof(f21848,plain,
sQ2737_spl,
inference(contradiction_clause,[status(thm)],[f21847]) ).
fof(f21887,definition,
( sQ2745_spl
<=> app(sK49_skl,cons(sK1_skl,nil)) = app(sK49_skl,cons(sK1_skl,nil)) ),
introduced(definition,[new_symbols(definition,[sQ2745_spl])],[split_symbol_definition]) ).
fof(f21889,plain,
( sQ2745_spl
| app(sK49_skl,cons(sK1_skl,nil)) != app(sK49_skl,cons(sK1_skl,nil)) ),
inference(component_clause,[status(thm)],[f21887]) ).
fof(f21897,plain,
( sQ2745_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f21889]) ).
fof(f21898,plain,
sQ2745_spl,
inference(contradiction_clause,[status(thm)],[f21897]) ).
fof(f22583,plain,
( ~ sQ550_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f420,f5211]) ).
fof(f22584,plain,
~ sQ550_spl,
inference(contradiction_clause,[status(thm)],[f22583]) ).
fof(f24174,plain,
nil != cons(sK0_skl,sK49_skl),
inference(forward_demodulation,[status(thm)],[f884,f6630]) ).
fof(f25299,plain,
( ~ sQ761_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7021,f24174]) ).
fof(f25300,plain,
~ sQ761_spl,
inference(contradiction_clause,[status(thm)],[f25299]) ).
fof(f26725,definition,
( sQ3063_spl
<=> app(tl(sK50_skl),sK49_skl) = app(tl(sK50_skl),sK49_skl) ),
introduced(definition,[new_symbols(definition,[sQ3063_spl])],[split_symbol_definition]) ).
fof(f26727,plain,
( sQ3063_spl
| app(tl(sK50_skl),sK49_skl) != app(tl(sK50_skl),sK49_skl) ),
inference(component_clause,[status(thm)],[f26725]) ).
fof(f26769,plain,
( sQ3063_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f26727]) ).
fof(f26770,plain,
sQ3063_spl,
inference(contradiction_clause,[status(thm)],[f26769]) ).
fof(f29691,plain,
( sQ965_spl
| ~ sQ10_spl
| ~ sQ12_spl
| ~ sQ6_spl
| sK50_skl != sK50_skl ),
inference(forward_demodulation,[status(thm)],[f8421,f8436]) ).
fof(f29692,plain,
( sQ965_spl
| ~ sQ10_spl
| ~ sQ12_spl
| ~ sQ6_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f29691]) ).
fof(f29693,plain,
( sQ965_spl
| ~ sQ10_spl
| ~ sQ12_spl
| ~ sQ6_spl ),
inference(contradiction_clause,[status(thm)],[f29692]) ).
fof(f29694,plain,
$false,
inference(sat_refutation,[status(thm)],[f434,f529,f629,f662,f708,f734,f738,f1201,f1268,f1279,f1665,f2288,f2399,f2444,f4108,f4160,f4525,f4795,f4813,f5144,f5238,f5726,f6508,f6528,f7583,f7692,f8437,f8930,f9317,f9612,f9645,f10079,f10142,f10208,f10274,f10341,f10408,f10550,f11007,f11014,f11018,f11030,f11037,f11121,f12046,f12888,f13956,f14242,f15386,f16134,f16826,f16958,f17059,f21139,f21526,f21611,f21682,f21774,f21848,f21898,f22584,f25300,f26770,f29693]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWC308+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.05 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.13/0.40 % Computer : n007.cluster.edu
% 0.13/0.40 % Model : x86_64 x86_64
% 0.13/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.40 % Memory : 8046.5625MB
% 0.13/0.40 % OS : Linux 6.8.0-71-generic
% 0.13/0.40 % CPULimit : 300
% 0.13/0.40 % WCLimit : 300
% 0.13/0.40 % DateTime : Mon Sep 21 08:12:05 UTC 2026
% 0.13/0.40 % CPUTime :
% 0.17/0.42 % Drodi V4.1.1
% 268.30/34.56 % Refutation found
% 268.30/34.56 % SZS status Theorem for theBenchmark: Theorem is valid
% 268.30/34.56 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 270.06/34.64 % Elapsed time: 34.224272 seconds
% 270.06/34.64 % CPU time: 270.631805 seconds
% 270.06/34.64 % Total memory used: 562.112 MB
% 270.06/34.64 % Net memory used: 536.062 MB
%------------------------------------------------------------------------------