%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWC272+1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n006.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 02:40:35 PM UTC 2026
% Result : Theorem 208.25s 26.94s
% Output : CNFRefutation 208.25s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 61
% Syntax : Number of formulae : 290 ( 79 unt; 48 def)
% Number of atoms : 758 ( 142 equ)
% Maximal formula atoms : 19 ( 2 avg)
% Number of connectives : 773 ( 305 ~; 293 |; 87 &)
% ( 56 <=>; 32 =>; 0 <=; 0 <~>)
% Maximal formula depth : 27 ( 4 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 57 ( 55 usr; 49 prp; 0-2 aty)
% Number of functors : 20 ( 20 usr; 8 con; 0-2 aty)
% Number of variables : 168 ( 138 !; 30 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
? [U] :
( ? [V] :
( U != V
& ssItem(V) )
& ssItem(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [U] :
( ssList(U)
=> ( totalorderedP(U)
<=> ! [V] :
( ssItem(V)
=> ! [W] :
( ssItem(W)
=> ! [X] :
( ssList(X)
=> ! [Y] :
( ssList(Y)
=> ! [Z] :
( ssList(Z)
=> ( app(app(X,cons(V,Y)),cons(W,Z)) = U
=> leq(V,W) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [U] :
( ssList(U)
=> ( strictorderedP(U)
<=> ! [V] :
( ssItem(V)
=> ! [W] :
( ssItem(W)
=> ! [X] :
( ssList(X)
=> ! [Y] :
( ssList(Y)
=> ! [Z] :
( ssList(Z)
=> ( app(app(X,cons(V,Y)),cons(W,Z)) = U
=> lt(V,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(f26,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ssList(app(U,V)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f55,axiom,
! [U] :
( ssList(U)
=> segmentP(U,U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f66,axiom,
totalorderedP(nil),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f83,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ( nil = app(U,V)
<=> ( nil = U
& nil = V ) ) ) ),
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(f93,axiom,
! [U] :
( ssItem(U)
=> ! [V] :
( ssItem(V)
=> ( lt(U,V)
<=> ( leq(U,V)
& U != V ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f96,conjecture,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ! [W] :
( ssList(W)
=> ! [X] :
( ( nil = W
& nil != X )
| totalorderedP(U)
| ! [Y] :
( ? [Z] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( lt(X2,Z)
& app(X3,cons(X2,nil)) = W
& ssList(X3) )
& ssItem(X2) )
& app(cons(Z,nil),X1) = Y
& ssList(X1) )
& ssItem(Z) )
| ~ strictorderedP(W)
| app(W,Y) != X
| ~ ssList(Y) )
| U != W
| V != X
| ~ ssList(X) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f97,negated_conjecture,
~ ! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ! [W] :
( ssList(W)
=> ! [X] :
( ( nil = W
& nil != X )
| totalorderedP(U)
| ! [Y] :
( ? [Z] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( lt(X2,Z)
& app(X3,cons(X2,nil)) = W
& ssList(X3) )
& ssItem(X2) )
& app(cons(Z,nil),X1) = Y
& ssList(X1) )
& ssItem(Z) )
| ~ strictorderedP(W)
| app(W,Y) != X
| ~ ssList(Y) )
| U != W
| V != X
| ~ ssList(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(f174,plain,
! [U] :
( ( totalorderedP(U)
<=> ! [V] :
( ! [W] :
( ! [X] :
( ! [Y] :
( ! [Z] :
( leq(V,W)
| app(app(X,cons(V,Y)),cons(W,Z)) != U
| ~ ssList(Z) )
| ~ ssList(Y) )
| ~ ssList(X) )
| ~ ssItem(W) )
| ~ ssItem(V) ) )
| ~ ssList(U) ),
inference(pre_NNF_transformation,[status(thm)],[f11]) ).
fof(f175,plain,
! [U] :
( ( ( ? [V] :
( ? [W] :
( ? [X] :
( ? [Y] :
( ? [Z] :
( ~ leq(V,W)
& app(app(X,cons(V,Y)),cons(W,Z)) = U
& ssList(Z) )
& ssList(Y) )
& ssList(X) )
& ssItem(W) )
& ssItem(V) )
| totalorderedP(U) )
& ( ! [V] :
( ! [W] :
( ! [X] :
( ! [Y] :
( ! [Z] :
( leq(V,W)
| app(app(X,cons(V,Y)),cons(W,Z)) != U
| ~ ssList(Z) )
| ~ ssList(Y) )
| ~ ssList(X) )
| ~ ssItem(W) )
| ~ ssItem(V) )
| ~ totalorderedP(U) ) )
| ~ ssList(U) ),
inference(NNF_transformation,[status(thm)],[f174]) ).
fof(f176,plain,
! [U] :
( ( ( ( ~ leq(sK24_skl(U),sK25_skl(U))
& app(app(sK26_skl(U),cons(sK24_skl(U),sK27_skl(U))),cons(sK25_skl(U),sK28_skl(U))) = U
& ssList(sK28_skl(U))
& ssList(sK27_skl(U))
& ssList(sK26_skl(U))
& ssItem(sK25_skl(U))
& ssItem(sK24_skl(U)) )
| totalorderedP(U) )
& ( ! [V] :
( ! [W] :
( ! [X] :
( ! [Y] :
( ! [Z] :
( leq(V,W)
| app(app(X,cons(V,Y)),cons(W,Z)) != U
| ~ ssList(Z) )
| ~ ssList(Y) )
| ~ ssList(X) )
| ~ ssItem(W) )
| ~ ssItem(V) )
| ~ totalorderedP(U) ) )
| ~ ssList(U) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK24_skl,sK25_skl,sK26_skl,sK27_skl,sK28_skl]),skolemize(V,sK24_skl(U)),skolemize(W,sK25_skl(U)),skolemize(X,sK26_skl(U)),skolemize(Y,sK27_skl(U)),skolemize(Z,sK28_skl(U))],[f175]) ).
fof(f178,plain,
! [X0] :
( ssItem(sK24_skl(X0))
| totalorderedP(X0)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f176]) ).
fof(f179,plain,
! [X0] :
( ~ ssList(X0)
| ssItem(sK25_skl(X0))
| totalorderedP(X0) ),
inference(cnf_transformation,[status(thm)],[f176]) ).
fof(f180,plain,
! [X0] :
( totalorderedP(X0)
| ssList(sK26_skl(X0))
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f176]) ).
fof(f181,plain,
! [X0] :
( totalorderedP(X0)
| ~ ssList(X0)
| ssList(sK27_skl(X0)) ),
inference(cnf_transformation,[status(thm)],[f176]) ).
fof(f182,plain,
! [X0] :
( ~ ssList(X0)
| ssList(sK28_skl(X0))
| totalorderedP(X0) ),
inference(cnf_transformation,[status(thm)],[f176]) ).
fof(f183,plain,
! [X0] :
( ~ ssList(X0)
| totalorderedP(X0)
| X0 = app(app(sK26_skl(X0),cons(sK24_skl(X0),sK27_skl(X0))),cons(sK25_skl(X0),sK28_skl(X0))) ),
inference(cnf_transformation,[status(thm)],[f176]) ).
fof(f184,plain,
! [X0] :
( totalorderedP(X0)
| ~ ssList(X0)
| ~ leq(sK24_skl(X0),sK25_skl(X0)) ),
inference(cnf_transformation,[status(thm)],[f176]) ).
fof(f185,plain,
! [U] :
( ( strictorderedP(U)
<=> ! [V] :
( ! [W] :
( ! [X] :
( ! [Y] :
( ! [Z] :
( lt(V,W)
| app(app(X,cons(V,Y)),cons(W,Z)) != U
| ~ ssList(Z) )
| ~ ssList(Y) )
| ~ ssList(X) )
| ~ ssItem(W) )
| ~ ssItem(V) ) )
| ~ ssList(U) ),
inference(pre_NNF_transformation,[status(thm)],[f12]) ).
fof(f186,plain,
! [U] :
( ( ( ? [V] :
( ? [W] :
( ? [X] :
( ? [Y] :
( ? [Z] :
( ~ lt(V,W)
& app(app(X,cons(V,Y)),cons(W,Z)) = U
& ssList(Z) )
& ssList(Y) )
& ssList(X) )
& ssItem(W) )
& ssItem(V) )
| strictorderedP(U) )
& ( ! [V] :
( ! [W] :
( ! [X] :
( ! [Y] :
( ! [Z] :
( lt(V,W)
| app(app(X,cons(V,Y)),cons(W,Z)) != U
| ~ ssList(Z) )
| ~ ssList(Y) )
| ~ ssList(X) )
| ~ ssItem(W) )
| ~ ssItem(V) )
| ~ strictorderedP(U) ) )
| ~ ssList(U) ),
inference(NNF_transformation,[status(thm)],[f185]) ).
fof(f187,plain,
! [U] :
( ( ( ( ~ lt(sK29_skl(U),sK30_skl(U))
& app(app(sK31_skl(U),cons(sK29_skl(U),sK32_skl(U))),cons(sK30_skl(U),sK33_skl(U))) = U
& ssList(sK33_skl(U))
& ssList(sK32_skl(U))
& ssList(sK31_skl(U))
& ssItem(sK30_skl(U))
& ssItem(sK29_skl(U)) )
| strictorderedP(U) )
& ( ! [V] :
( ! [W] :
( ! [X] :
( ! [Y] :
( ! [Z] :
( lt(V,W)
| app(app(X,cons(V,Y)),cons(W,Z)) != U
| ~ ssList(Z) )
| ~ ssList(Y) )
| ~ ssList(X) )
| ~ ssItem(W) )
| ~ ssItem(V) )
| ~ strictorderedP(U) ) )
| ~ ssList(U) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK29_skl,sK30_skl,sK31_skl,sK32_skl,sK33_skl]),skolemize(V,sK29_skl(U)),skolemize(W,sK30_skl(U)),skolemize(X,sK31_skl(U)),skolemize(Y,sK32_skl(U)),skolemize(Z,sK33_skl(U))],[f186]) ).
fof(f188,plain,
! [X0,X1,X2,X3,X4,X5] :
( lt(X1,X2)
| app(app(X3,cons(X1,X4)),cons(X2,X5)) != X0
| ~ ssList(X5)
| ~ ssList(X4)
| ~ ssList(X3)
| ~ ssItem(X2)
| ~ ssItem(X1)
| ~ strictorderedP(X0)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f187]) ).
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] :
( ~ ssItem(X0)
| ~ ssList(X1)
| ssList(cons(X0,X1)) ),
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(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(f318,plain,
! [U] :
( segmentP(U,U)
| ~ ssList(U) ),
inference(pre_NNF_transformation,[status(thm)],[f55]) ).
fof(f319,plain,
! [X0] :
( segmentP(X0,X0)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f318]) ).
fof(f339,plain,
totalorderedP(nil),
inference(cnf_transformation,[status(thm)],[f66]) ).
fof(f383,plain,
! [U] :
( ! [V] :
( ( nil = app(U,V)
<=> ( nil = U
& nil = V ) )
| ~ ssList(V) )
| ~ ssList(U) ),
inference(pre_NNF_transformation,[status(thm)],[f83]) ).
fof(f384,plain,
! [U] :
( ! [V] :
( ( ( nil != U
| nil != V
| nil = app(U,V) )
& ( ( nil = U
& nil = V )
| nil != app(U,V) ) )
| ~ ssList(V) )
| ~ ssList(U) ),
inference(NNF_transformation,[status(thm)],[f383]) ).
fof(f387,plain,
! [X0,X1] :
( nil != X0
| nil != X1
| nil = app(X0,X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f384]) ).
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(f406,plain,
! [U] :
( ! [V] :
( ( lt(U,V)
<=> ( leq(U,V)
& U != V ) )
| ~ ssItem(V) )
| ~ ssItem(U) ),
inference(pre_NNF_transformation,[status(thm)],[f93]) ).
fof(f407,plain,
! [U] :
( ! [V] :
( ( ( ~ leq(U,V)
| U = V
| lt(U,V) )
& ( ( leq(U,V)
& U != V )
| ~ lt(U,V) ) )
| ~ ssItem(V) )
| ~ ssItem(U) ),
inference(NNF_transformation,[status(thm)],[f406]) ).
fof(f408,plain,
! [X0,X1] :
( X0 != X1
| ~ lt(X0,X1)
| ~ ssItem(X1)
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(thm)],[f407]) ).
fof(f409,plain,
! [X0,X1] :
( leq(X0,X1)
| ~ ssItem(X0)
| ~ ssItem(X1)
| ~ lt(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f407]) ).
fof(f415,plain,
? [U] :
( ? [V] :
( ? [W] :
( ? [X] :
( ( nil != W
| nil = X )
& ~ totalorderedP(U)
& ? [Y] :
( ! [Z] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ~ lt(X2,Z)
| app(X3,cons(X2,nil)) != W
| ~ ssList(X3) )
| ~ ssItem(X2) )
| app(cons(Z,nil),X1) != Y
| ~ ssList(X1) )
| ~ ssItem(Z) )
& strictorderedP(W)
& app(W,Y) = X
& ssList(Y) )
& 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 != W
| nil = X )
& ~ totalorderedP(U)
& ? [Y] :
( ! [Z] :
( ! [X2] :
( ~ lt(X2,Z)
| ! [X3] :
( app(X3,cons(X2,nil)) != W
| ~ ssList(X3) )
| ~ ssItem(X2) )
| ! [X1] :
( app(cons(Z,nil),X1) != Y
| ~ ssList(X1) )
| ~ ssItem(Z) )
& strictorderedP(W)
& app(W,Y) = X
& ssList(Y) )
& U = W
& V = X
& ssList(X) )
& ssList(W) )
& ssList(V) )
& ssList(U) ),
inference(miniscoping,[status(thm)],[f415]) ).
fof(f417,plain,
( ( nil != sK49_skl
| nil = sK50_skl )
& ~ totalorderedP(sK47_skl)
& ! [Z] :
( ! [X2] :
( ~ lt(X2,Z)
| ! [X3] :
( app(X3,cons(X2,nil)) != sK49_skl
| ~ ssList(X3) )
| ~ ssItem(X2) )
| ! [X1] :
( app(cons(Z,nil),X1) != sK51_skl
| ~ ssList(X1) )
| ~ ssItem(Z) )
& strictorderedP(sK49_skl)
& app(sK49_skl,sK51_skl) = sK50_skl
& ssList(sK51_skl)
& sK47_skl = sK49_skl
& sK48_skl = sK50_skl
& ssList(sK50_skl)
& ssList(sK49_skl)
& ssList(sK48_skl)
& ssList(sK47_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK47_skl,sK48_skl,sK49_skl,sK50_skl,sK51_skl]),skolemize(U,sK47_skl),skolemize(V,sK48_skl),skolemize(W,sK49_skl),skolemize(X,sK50_skl),skolemize(Y,sK51_skl)],[f416]) ).
fof(f418,plain,
ssList(sK47_skl),
inference(cnf_transformation,[status(thm)],[f417]) ).
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(f423,plain,
sK47_skl = sK49_skl,
inference(cnf_transformation,[status(thm)],[f417]) ).
fof(f424,plain,
ssList(sK51_skl),
inference(cnf_transformation,[status(thm)],[f417]) ).
fof(f426,plain,
strictorderedP(sK49_skl),
inference(cnf_transformation,[status(thm)],[f417]) ).
fof(f428,plain,
~ totalorderedP(sK47_skl),
inference(cnf_transformation,[status(thm)],[f417]) ).
fof(f437,plain,
! [X1] :
( ~ lt(X1,X1)
| ~ ssItem(X1)
| ~ ssItem(X1) ),
inference(destructive_equality_resolution,[status(thm)],[f408]) ).
fof(f438,plain,
! [X0] :
( ~ lt(X0,X0)
| ~ ssItem(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f437]) ).
fof(f441,plain,
( nil = app(nil,nil)
| ~ ssList(nil)
| ~ ssList(nil) ),
inference(destructive_equality_resolution,[status(thm)],[f387]) ).
fof(f442,plain,
( ~ ssList(nil)
| nil = app(nil,nil) ),
inference(duplicate_literals_removal,[status(thm)],[f441]) ).
fof(f463,plain,
! [X0,X1,X2,X3,X4] :
( ~ ssList(X2)
| ~ ssItem(X1)
| ~ ssItem(X3)
| ~ ssList(app(app(X0,cons(X1,X2)),cons(X3,X4)))
| ~ ssList(X4)
| lt(X1,X3)
| ~ ssList(X0)
| ~ strictorderedP(app(app(X0,cons(X1,X2)),cons(X3,X4))) ),
inference(destructive_equality_resolution,[status(thm)],[f188]) ).
fof(f475,plain,
segmentP(sK49_skl,sK49_skl),
inference(resolution,[status(thm)],[f420,f319]) ).
fof(f565,plain,
segmentP(sK51_skl,sK51_skl),
inference(resolution,[status(thm)],[f424,f319]) ).
fof(f638,plain,
app(nil,nil) = nil,
inference(forward_subsumption_resolution,[status(thm)],[f442,f223]) ).
fof(f656,plain,
strictorderedP(sK47_skl),
inference(forward_demodulation,[status(thm)],[f423,f426]) ).
fof(f657,plain,
( ~ ssList(sK47_skl)
| sK47_skl = app(app(sK26_skl(sK47_skl),cons(sK24_skl(sK47_skl),sK27_skl(sK47_skl))),cons(sK25_skl(sK47_skl),sK28_skl(sK47_skl))) ),
inference(resolution,[status(thm)],[f428,f183]) ).
fof(f658,plain,
( ~ ssList(sK47_skl)
| ssList(sK27_skl(sK47_skl)) ),
inference(resolution,[status(thm)],[f428,f181]) ).
fof(f659,definition,
( sQ36_spl
<=> sK47_skl = app(app(sK26_skl(sK47_skl),cons(sK24_skl(sK47_skl),sK27_skl(sK47_skl))),cons(sK25_skl(sK47_skl),sK28_skl(sK47_skl))) ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f660,plain,
( ~ sQ36_spl
| sK47_skl = app(app(sK26_skl(sK47_skl),cons(sK24_skl(sK47_skl),sK27_skl(sK47_skl))),cons(sK25_skl(sK47_skl),sK28_skl(sK47_skl))) ),
inference(component_clause,[status(thm)],[f659]) ).
fof(f662,definition,
( sQ37_spl
<=> ssList(sK47_skl) ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f664,plain,
( sQ37_spl
| ~ ssList(sK47_skl) ),
inference(component_clause,[status(thm)],[f662]) ).
fof(f665,plain,
( ~ sQ37_spl
| sQ36_spl ),
inference(split_clause,[status(thm)],[f657,f659,f662]) ).
fof(f666,definition,
( sQ38_spl
<=> ssList(sK27_skl(sK47_skl)) ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f669,plain,
( ~ sQ37_spl
| sQ38_spl ),
inference(split_clause,[status(thm)],[f658,f666,f662]) ).
fof(f684,definition,
( sQ40_spl
<=> nil = sK47_skl ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f685,plain,
( ~ sQ40_spl
| nil = sK47_skl ),
inference(component_clause,[status(thm)],[f684]) ).
fof(f724,plain,
! [X0] :
( X0 != cons(sK1_skl,X0)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f104,f225]) ).
fof(f727,plain,
! [X0] :
( ssList(cons(sK1_skl,X0))
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f104,f222]) ).
fof(f731,plain,
~ lt(sK1_skl,sK1_skl),
inference(resolution,[status(thm)],[f104,f438]) ).
fof(f774,plain,
! [X0] :
( ~ ssList(X0)
| cons(sK0_skl,X0) != X0 ),
inference(resolution,[status(thm)],[f103,f225]) ).
fof(f777,plain,
! [X0] :
( ssList(cons(sK0_skl,X0))
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f103,f222]) ).
fof(f781,plain,
~ lt(sK0_skl,sK0_skl),
inference(resolution,[status(thm)],[f103,f438]) ).
fof(f792,plain,
app(sK47_skl,nil) = sK47_skl,
inference(resolution,[status(thm)],[f389,f418]) ).
fof(f797,plain,
( sQ37_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f664,f418]) ).
fof(f798,plain,
sQ37_spl,
inference(contradiction_clause,[status(thm)],[f797]) ).
fof(f802,plain,
( ~ sQ40_spl
| ~ totalorderedP(nil) ),
inference(backward_demodulation,[status(thm)],[f685,f428]) ).
fof(f805,plain,
( ~ sQ40_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f802,f339]) ).
fof(f806,plain,
~ sQ40_spl,
inference(contradiction_clause,[status(thm)],[f805]) ).
fof(f843,plain,
nil != cons(sK1_skl,nil),
inference(resolution,[status(thm)],[f724,f223]) ).
fof(f873,plain,
nil != cons(sK0_skl,nil),
inference(resolution,[status(thm)],[f774,f223]) ).
fof(f894,plain,
ssList(cons(sK0_skl,sK47_skl)),
inference(resolution,[status(thm)],[f418,f777]) ).
fof(f896,plain,
cons(sK0_skl,sK47_skl) != sK47_skl,
inference(resolution,[status(thm)],[f418,f774]) ).
fof(f902,plain,
ssList(cons(sK1_skl,sK47_skl)),
inference(resolution,[status(thm)],[f418,f727]) ).
fof(f904,plain,
cons(sK1_skl,sK47_skl) != sK47_skl,
inference(resolution,[status(thm)],[f418,f724]) ).
fof(f1160,definition,
( sQ83_spl
<=> nil = cons(sK1_skl,nil) ),
introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition]) ).
fof(f1161,plain,
( ~ sQ83_spl
| nil = cons(sK1_skl,nil) ),
inference(component_clause,[status(thm)],[f1160]) ).
fof(f1192,plain,
( ~ sQ83_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1161,f843]) ).
fof(f1193,plain,
~ sQ83_spl,
inference(contradiction_clause,[status(thm)],[f1192]) ).
fof(f1284,definition,
( sQ101_spl
<=> nil = cons(sK0_skl,nil) ),
introduced(definition,[new_symbols(definition,[sQ101_spl])],[split_symbol_definition]) ).
fof(f1285,plain,
( ~ sQ101_spl
| nil = cons(sK0_skl,nil) ),
inference(component_clause,[status(thm)],[f1284]) ).
fof(f1313,plain,
( ~ sQ101_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1285,f873]) ).
fof(f1314,plain,
~ sQ101_spl,
inference(contradiction_clause,[status(thm)],[f1313]) ).
fof(f1370,plain,
! [X0] :
( ssList(app(sK51_skl,X0))
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f424,f245]) ).
fof(f1628,definition,
( sQ140_spl
<=> app(sK47_skl,sK47_skl) = app(sK47_skl,app(sK47_skl,nil)) ),
introduced(definition,[new_symbols(definition,[sQ140_spl])],[split_symbol_definition]) ).
fof(f1630,plain,
( sQ140_spl
| app(sK47_skl,app(sK47_skl,nil)) != app(sK47_skl,sK47_skl) ),
inference(component_clause,[status(thm)],[f1628]) ).
fof(f1638,definition,
( sQ143_spl
<=> cons(sK0_skl,sK47_skl) = sK47_skl ),
introduced(definition,[new_symbols(definition,[sQ143_spl])],[split_symbol_definition]) ).
fof(f1639,plain,
( ~ sQ143_spl
| cons(sK0_skl,sK47_skl) = sK47_skl ),
inference(component_clause,[status(thm)],[f1638]) ).
fof(f1763,definition,
( sQ162_spl
<=> cons(sK1_skl,sK47_skl) = sK47_skl ),
introduced(definition,[new_symbols(definition,[sQ162_spl])],[split_symbol_definition]) ).
fof(f1764,plain,
( ~ sQ162_spl
| cons(sK1_skl,sK47_skl) = sK47_skl ),
inference(component_clause,[status(thm)],[f1763]) ).
fof(f1860,definition,
( sQ169_spl
<=> app(sK47_skl,sK47_skl) = app(sK47_skl,sK47_skl) ),
introduced(definition,[new_symbols(definition,[sQ169_spl])],[split_symbol_definition]) ).
fof(f1862,plain,
( sQ169_spl
| app(sK47_skl,sK47_skl) != app(sK47_skl,sK47_skl) ),
inference(component_clause,[status(thm)],[f1860]) ).
fof(f1871,plain,
( sQ169_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f1862]) ).
fof(f1872,plain,
sQ169_spl,
inference(contradiction_clause,[status(thm)],[f1871]) ).
fof(f1987,plain,
ssList(cons(sK0_skl,sK50_skl)),
inference(resolution,[status(thm)],[f421,f777]) ).
fof(f1989,plain,
sK50_skl != cons(sK0_skl,sK50_skl),
inference(resolution,[status(thm)],[f421,f774]) ).
fof(f1992,plain,
ssList(cons(sK1_skl,sK50_skl)),
inference(resolution,[status(thm)],[f421,f727]) ).
fof(f1994,plain,
cons(sK1_skl,sK50_skl) != sK50_skl,
inference(resolution,[status(thm)],[f421,f724]) ).
fof(f2008,plain,
! [X0] :
( ssList(app(sK50_skl,X0))
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f421,f245]) ).
fof(f2101,plain,
segmentP(sK47_skl,sK49_skl),
inference(forward_demodulation,[status(thm)],[f423,f475]) ).
fof(f2102,plain,
segmentP(sK47_skl,sK47_skl),
inference(forward_demodulation,[status(thm)],[f423,f2101]) ).
fof(f2217,definition,
( sQ190_spl
<=> ssItem(sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ190_spl])],[split_symbol_definition]) ).
fof(f2219,plain,
( sQ190_spl
| ~ ssItem(sK1_skl) ),
inference(component_clause,[status(thm)],[f2217]) ).
fof(f2255,plain,
( sQ190_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2219,f104]) ).
fof(f2256,plain,
sQ190_spl,
inference(contradiction_clause,[status(thm)],[f2255]) ).
fof(f2453,definition,
( sQ230_spl
<=> ssItem(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ230_spl])],[split_symbol_definition]) ).
fof(f2455,plain,
( sQ230_spl
| ~ ssItem(sK0_skl) ),
inference(component_clause,[status(thm)],[f2453]) ).
fof(f2486,plain,
( sQ230_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2455,f103]) ).
fof(f2487,plain,
sQ230_spl,
inference(contradiction_clause,[status(thm)],[f2486]) ).
fof(f2514,plain,
ssList(cons(sK0_skl,sK51_skl)),
inference(resolution,[status(thm)],[f424,f777]) ).
fof(f2515,plain,
sK51_skl != cons(sK0_skl,sK51_skl),
inference(resolution,[status(thm)],[f424,f774]) ).
fof(f2518,plain,
ssList(cons(sK1_skl,sK51_skl)),
inference(resolution,[status(thm)],[f424,f727]) ).
fof(f2520,plain,
cons(sK1_skl,sK51_skl) != sK51_skl,
inference(resolution,[status(thm)],[f424,f724]) ).
fof(f2717,definition,
( sQ260_spl
<=> ssList(cons(sK1_skl,sK47_skl)) ),
introduced(definition,[new_symbols(definition,[sQ260_spl])],[split_symbol_definition]) ).
fof(f2719,plain,
( sQ260_spl
| ~ ssList(cons(sK1_skl,sK47_skl)) ),
inference(component_clause,[status(thm)],[f2717]) ).
fof(f2724,plain,
( sQ260_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2719,f902]) ).
fof(f2725,plain,
sQ260_spl,
inference(contradiction_clause,[status(thm)],[f2724]) ).
fof(f3335,plain,
ssList(app(sK51_skl,sK50_skl)),
inference(resolution,[status(thm)],[f1370,f421]) ).
fof(f3366,definition,
( sQ362_spl
<=> ssList(sK50_skl) ),
introduced(definition,[new_symbols(definition,[sQ362_spl])],[split_symbol_definition]) ).
fof(f3368,plain,
( sQ362_spl
| ~ ssList(sK50_skl) ),
inference(component_clause,[status(thm)],[f3366]) ).
fof(f3386,plain,
( sQ362_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3368,f421]) ).
fof(f3387,plain,
sQ362_spl,
inference(contradiction_clause,[status(thm)],[f3386]) ).
fof(f3537,plain,
( ssList(sK26_skl(sK47_skl))
| ~ ssList(sK47_skl) ),
inference(resolution,[status(thm)],[f180,f428]) ).
fof(f3538,definition,
( sQ395_spl
<=> ssList(sK26_skl(sK47_skl)) ),
introduced(definition,[new_symbols(definition,[sQ395_spl])],[split_symbol_definition]) ).
fof(f3541,plain,
( sQ395_spl
| ~ sQ37_spl ),
inference(split_clause,[status(thm)],[f3537,f662,f3538]) ).
fof(f3626,definition,
( sQ410_spl
<=> app(cons(sK0_skl,sK47_skl),cons(sK0_skl,sK47_skl)) = app(cons(sK0_skl,sK47_skl),cons(sK0_skl,sK47_skl)) ),
introduced(definition,[new_symbols(definition,[sQ410_spl])],[split_symbol_definition]) ).
fof(f3628,plain,
( sQ410_spl
| app(cons(sK0_skl,sK47_skl),cons(sK0_skl,sK47_skl)) != app(cons(sK0_skl,sK47_skl),cons(sK0_skl,sK47_skl)) ),
inference(component_clause,[status(thm)],[f3626]) ).
fof(f3648,plain,
( ~ sQ143_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1639,f896]) ).
fof(f3649,plain,
~ sQ143_spl,
inference(contradiction_clause,[status(thm)],[f3648]) ).
fof(f3650,plain,
( sQ410_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f3628]) ).
fof(f3651,plain,
sQ410_spl,
inference(contradiction_clause,[status(thm)],[f3650]) ).
fof(f3662,definition,
( sQ417_spl
<=> ssList(cons(sK0_skl,sK47_skl)) ),
introduced(definition,[new_symbols(definition,[sQ417_spl])],[split_symbol_definition]) ).
fof(f3664,plain,
( sQ417_spl
| ~ ssList(cons(sK0_skl,sK47_skl)) ),
inference(component_clause,[status(thm)],[f3662]) ).
fof(f3673,plain,
( sQ417_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3664,f894]) ).
fof(f3674,plain,
sQ417_spl,
inference(contradiction_clause,[status(thm)],[f3673]) ).
fof(f3825,definition,
( sQ443_spl
<=> totalorderedP(sK47_skl) ),
introduced(definition,[new_symbols(definition,[sQ443_spl])],[split_symbol_definition]) ).
fof(f3826,plain,
( ~ sQ443_spl
| totalorderedP(sK47_skl) ),
inference(component_clause,[status(thm)],[f3825]) ).
fof(f4159,plain,
( sQ140_spl
| app(sK47_skl,sK47_skl) != app(sK47_skl,sK47_skl) ),
inference(forward_demodulation,[status(thm)],[f792,f1630]) ).
fof(f4160,plain,
( sQ140_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f4159]) ).
fof(f4161,plain,
sQ140_spl,
inference(contradiction_clause,[status(thm)],[f4160]) ).
fof(f4249,definition,
( sQ511_spl
<=> app(cons(sK1_skl,sK47_skl),cons(sK1_skl,sK47_skl)) = app(cons(sK1_skl,sK47_skl),cons(sK1_skl,sK47_skl)) ),
introduced(definition,[new_symbols(definition,[sQ511_spl])],[split_symbol_definition]) ).
fof(f4251,plain,
( sQ511_spl
| app(cons(sK1_skl,sK47_skl),cons(sK1_skl,sK47_skl)) != app(cons(sK1_skl,sK47_skl),cons(sK1_skl,sK47_skl)) ),
inference(component_clause,[status(thm)],[f4249]) ).
fof(f4264,plain,
( ~ sQ162_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1764,f904]) ).
fof(f4265,plain,
~ sQ162_spl,
inference(contradiction_clause,[status(thm)],[f4264]) ).
fof(f4266,plain,
( sQ511_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f4251]) ).
fof(f4267,plain,
sQ511_spl,
inference(contradiction_clause,[status(thm)],[f4266]) ).
fof(f5438,plain,
ssList(app(sK50_skl,sK50_skl)),
inference(resolution,[status(thm)],[f2008,f421]) ).
fof(f6041,plain,
( ~ ssList(sK47_skl)
| ~ leq(sK24_skl(sK47_skl),sK25_skl(sK47_skl)) ),
inference(resolution,[status(thm)],[f184,f428]) ).
fof(f6042,definition,
( sQ731_spl
<=> leq(sK24_skl(sK47_skl),sK25_skl(sK47_skl)) ),
introduced(definition,[new_symbols(definition,[sQ731_spl])],[split_symbol_definition]) ).
fof(f6044,plain,
( sQ731_spl
| ~ leq(sK24_skl(sK47_skl),sK25_skl(sK47_skl)) ),
inference(component_clause,[status(thm)],[f6042]) ).
fof(f6045,plain,
( ~ sQ37_spl
| ~ sQ731_spl ),
inference(split_clause,[status(thm)],[f6041,f6042,f662]) ).
fof(f6185,definition,
( sQ757_spl
<=> app(sK47_skl,cons(sK1_skl,nil)) = app(sK47_skl,cons(sK1_skl,nil)) ),
introduced(definition,[new_symbols(definition,[sQ757_spl])],[split_symbol_definition]) ).
fof(f6187,plain,
( sQ757_spl
| app(sK47_skl,cons(sK1_skl,nil)) != app(sK47_skl,cons(sK1_skl,nil)) ),
inference(component_clause,[status(thm)],[f6185]) ).
fof(f6201,plain,
( sQ757_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f6187]) ).
fof(f6202,plain,
sQ757_spl,
inference(contradiction_clause,[status(thm)],[f6201]) ).
fof(f6258,definition,
( sQ768_spl
<=> app(sK51_skl,sK47_skl) = app(sK51_skl,sK47_skl) ),
introduced(definition,[new_symbols(definition,[sQ768_spl])],[split_symbol_definition]) ).
fof(f6260,plain,
( sQ768_spl
| app(sK51_skl,sK47_skl) != app(sK51_skl,sK47_skl) ),
inference(component_clause,[status(thm)],[f6258]) ).
fof(f6270,plain,
( sQ768_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f6260]) ).
fof(f6271,plain,
sQ768_spl,
inference(contradiction_clause,[status(thm)],[f6270]) ).
fof(f6992,plain,
( ~ sQ443_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3826,f428]) ).
fof(f6993,plain,
~ sQ443_spl,
inference(contradiction_clause,[status(thm)],[f6992]) ).
fof(f7680,definition,
( sQ937_spl
<=> sK51_skl = cons(sK0_skl,sK51_skl) ),
introduced(definition,[new_symbols(definition,[sQ937_spl])],[split_symbol_definition]) ).
fof(f7681,plain,
( ~ sQ937_spl
| sK51_skl = cons(sK0_skl,sK51_skl) ),
inference(component_clause,[status(thm)],[f7680]) ).
fof(f7936,definition,
( sQ964_spl
<=> sK51_skl = cons(sK1_skl,sK51_skl) ),
introduced(definition,[new_symbols(definition,[sQ964_spl])],[split_symbol_definition]) ).
fof(f7937,plain,
( ~ sQ964_spl
| sK51_skl = cons(sK1_skl,sK51_skl) ),
inference(component_clause,[status(thm)],[f7936]) ).
fof(f8001,definition,
( sQ970_spl
<=> ssList(cons(sK0_skl,sK51_skl)) ),
introduced(definition,[new_symbols(definition,[sQ970_spl])],[split_symbol_definition]) ).
fof(f8003,plain,
( sQ970_spl
| ~ ssList(cons(sK0_skl,sK51_skl)) ),
inference(component_clause,[status(thm)],[f8001]) ).
fof(f8008,plain,
( sQ970_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8003,f2514]) ).
fof(f8009,plain,
sQ970_spl,
inference(contradiction_clause,[status(thm)],[f8008]) ).
fof(f9146,definition,
( sQ1165_spl
<=> app(cons(sK0_skl,sK51_skl),cons(sK0_skl,sK51_skl)) = app(cons(sK0_skl,sK51_skl),cons(sK0_skl,sK51_skl)) ),
introduced(definition,[new_symbols(definition,[sQ1165_spl])],[split_symbol_definition]) ).
fof(f9148,plain,
( sQ1165_spl
| app(cons(sK0_skl,sK51_skl),cons(sK0_skl,sK51_skl)) != app(cons(sK0_skl,sK51_skl),cons(sK0_skl,sK51_skl)) ),
inference(component_clause,[status(thm)],[f9146]) ).
fof(f9178,plain,
( ~ sQ937_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7681,f2515]) ).
fof(f9179,plain,
~ sQ937_spl,
inference(contradiction_clause,[status(thm)],[f9178]) ).
fof(f9180,plain,
( sQ1165_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f9148]) ).
fof(f9181,plain,
sQ1165_spl,
inference(contradiction_clause,[status(thm)],[f9180]) ).
fof(f9344,definition,
( sQ1201_spl
<=> sK1_skl = sK0_skl ),
introduced(definition,[new_symbols(definition,[sQ1201_spl])],[split_symbol_definition]) ).
fof(f9345,plain,
( ~ sQ1201_spl
| sK1_skl = sK0_skl ),
inference(component_clause,[status(thm)],[f9344]) ).
fof(f9491,definition,
( sQ1223_spl
<=> ssList(cons(sK1_skl,sK51_skl)) ),
introduced(definition,[new_symbols(definition,[sQ1223_spl])],[split_symbol_definition]) ).
fof(f9493,plain,
( sQ1223_spl
| ~ ssList(cons(sK1_skl,sK51_skl)) ),
inference(component_clause,[status(thm)],[f9491]) ).
fof(f9498,plain,
( sQ1223_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f9493,f2518]) ).
fof(f9499,plain,
sQ1223_spl,
inference(contradiction_clause,[status(thm)],[f9498]) ).
fof(f9547,plain,
( ~ sQ964_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7937,f2520]) ).
fof(f9548,plain,
~ sQ964_spl,
inference(contradiction_clause,[status(thm)],[f9547]) ).
fof(f9584,plain,
( ~ sQ36_spl
| ~ ssList(sK27_skl(sK47_skl))
| ~ ssItem(sK24_skl(sK47_skl))
| ~ ssItem(sK25_skl(sK47_skl))
| ~ ssList(sK47_skl)
| ~ ssList(sK28_skl(sK47_skl))
| lt(sK24_skl(sK47_skl),sK25_skl(sK47_skl))
| ~ ssList(sK26_skl(sK47_skl))
| ~ strictorderedP(app(app(sK26_skl(sK47_skl),cons(sK24_skl(sK47_skl),sK27_skl(sK47_skl))),cons(sK25_skl(sK47_skl),sK28_skl(sK47_skl)))) ),
inference(paramodulation,[status(thm)],[f660,f463]) ).
fof(f9597,definition,
( sQ1246_spl
<=> strictorderedP(app(app(sK26_skl(sK47_skl),cons(sK24_skl(sK47_skl),sK27_skl(sK47_skl))),cons(sK25_skl(sK47_skl),sK28_skl(sK47_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ1246_spl])],[split_symbol_definition]) ).
fof(f9599,plain,
( sQ1246_spl
| ~ strictorderedP(app(app(sK26_skl(sK47_skl),cons(sK24_skl(sK47_skl),sK27_skl(sK47_skl))),cons(sK25_skl(sK47_skl),sK28_skl(sK47_skl)))) ),
inference(component_clause,[status(thm)],[f9597]) ).
fof(f9600,definition,
( sQ1247_spl
<=> lt(sK24_skl(sK47_skl),sK25_skl(sK47_skl)) ),
introduced(definition,[new_symbols(definition,[sQ1247_spl])],[split_symbol_definition]) ).
fof(f9603,definition,
( sQ1248_spl
<=> ssList(sK28_skl(sK47_skl)) ),
introduced(definition,[new_symbols(definition,[sQ1248_spl])],[split_symbol_definition]) ).
fof(f9606,definition,
( sQ1249_spl
<=> ssItem(sK25_skl(sK47_skl)) ),
introduced(definition,[new_symbols(definition,[sQ1249_spl])],[split_symbol_definition]) ).
fof(f9609,definition,
( sQ1250_spl
<=> ssItem(sK24_skl(sK47_skl)) ),
introduced(definition,[new_symbols(definition,[sQ1250_spl])],[split_symbol_definition]) ).
fof(f9612,plain,
( ~ sQ36_spl
| ~ sQ38_spl
| ~ sQ1250_spl
| ~ sQ1249_spl
| ~ sQ37_spl
| ~ sQ1248_spl
| sQ1247_spl
| ~ sQ395_spl
| ~ sQ1246_spl ),
inference(split_clause,[status(thm)],[f9584,f9597,f3538,f9600,f9603,f662,f9606,f9609,f666,f659]) ).
fof(f10491,definition,
( sQ1372_spl
<=> segmentP(sK47_skl,sK47_skl) ),
introduced(definition,[new_symbols(definition,[sQ1372_spl])],[split_symbol_definition]) ).
fof(f10493,plain,
( sQ1372_spl
| ~ segmentP(sK47_skl,sK47_skl) ),
inference(component_clause,[status(thm)],[f10491]) ).
fof(f10499,definition,
( sQ1374_spl
<=> segmentP(sK51_skl,sK51_skl) ),
introduced(definition,[new_symbols(definition,[sQ1374_spl])],[split_symbol_definition]) ).
fof(f10501,plain,
( sQ1374_spl
| ~ segmentP(sK51_skl,sK51_skl) ),
inference(component_clause,[status(thm)],[f10499]) ).
fof(f10756,definition,
( sQ1411_spl
<=> app(nil,nil) = nil ),
introduced(definition,[new_symbols(definition,[sQ1411_spl])],[split_symbol_definition]) ).
fof(f10758,plain,
( sQ1411_spl
| app(nil,nil) != nil ),
inference(component_clause,[status(thm)],[f10756]) ).
fof(f10783,definition,
( sQ1415_spl
<=> ssList(app(sK51_skl,sK50_skl)) ),
introduced(definition,[new_symbols(definition,[sQ1415_spl])],[split_symbol_definition]) ).
fof(f10785,plain,
( sQ1415_spl
| ~ ssList(app(sK51_skl,sK50_skl)) ),
inference(component_clause,[status(thm)],[f10783]) ).
fof(f10824,plain,
( sQ1415_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f10785,f3335]) ).
fof(f10825,plain,
sQ1415_spl,
inference(contradiction_clause,[status(thm)],[f10824]) ).
fof(f11264,plain,
( ~ ssList(sK47_skl)
| ssItem(sK25_skl(sK47_skl)) ),
inference(resolution,[status(thm)],[f179,f428]) ).
fof(f11265,plain,
( ~ sQ37_spl
| sQ1249_spl ),
inference(split_clause,[status(thm)],[f11264,f9606,f662]) ).
fof(f11444,plain,
( ~ ssList(sK47_skl)
| ssList(sK28_skl(sK47_skl)) ),
inference(resolution,[status(thm)],[f182,f428]) ).
fof(f11445,plain,
( ~ sQ37_spl
| sQ1248_spl ),
inference(split_clause,[status(thm)],[f11444,f9603,f662]) ).
fof(f11446,plain,
( sQ1411_spl
| nil != nil ),
inference(forward_demodulation,[status(thm)],[f638,f10758]) ).
fof(f11447,plain,
( sQ1411_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f11446]) ).
fof(f11448,plain,
sQ1411_spl,
inference(contradiction_clause,[status(thm)],[f11447]) ).
fof(f11450,plain,
( sQ1374_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f10501,f565]) ).
fof(f11451,plain,
sQ1374_spl,
inference(contradiction_clause,[status(thm)],[f11450]) ).
fof(f11458,plain,
( sQ1372_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f10493,f2102]) ).
fof(f11459,plain,
sQ1372_spl,
inference(contradiction_clause,[status(thm)],[f11458]) ).
fof(f12418,plain,
( ssItem(sK24_skl(sK47_skl))
| ~ ssList(sK47_skl) ),
inference(resolution,[status(thm)],[f178,f428]) ).
fof(f12419,plain,
( sQ1250_spl
| ~ sQ37_spl ),
inference(split_clause,[status(thm)],[f12418,f662,f9609]) ).
fof(f12420,plain,
( sQ1246_spl
| ~ sQ36_spl
| ~ strictorderedP(sK47_skl) ),
inference(forward_demodulation,[status(thm)],[f660,f9599]) ).
fof(f12421,plain,
( sQ1246_spl
| ~ sQ36_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f12420,f656]) ).
fof(f12422,plain,
( sQ1246_spl
| ~ sQ36_spl ),
inference(contradiction_clause,[status(thm)],[f12421]) ).
fof(f13480,definition,
( sQ1709_spl
<=> app(app(sK51_skl,sK51_skl),app(sK51_skl,sK51_skl)) = app(app(sK51_skl,sK51_skl),app(sK51_skl,sK51_skl)) ),
introduced(definition,[new_symbols(definition,[sQ1709_spl])],[split_symbol_definition]) ).
fof(f13482,plain,
( sQ1709_spl
| app(app(sK51_skl,sK51_skl),app(sK51_skl,sK51_skl)) != app(app(sK51_skl,sK51_skl),app(sK51_skl,sK51_skl)) ),
inference(component_clause,[status(thm)],[f13480]) ).
fof(f13484,plain,
( sQ1709_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f13482]) ).
fof(f13485,plain,
sQ1709_spl,
inference(contradiction_clause,[status(thm)],[f13484]) ).
fof(f13933,definition,
( sQ1754_spl
<=> app(app(sK51_skl,sK50_skl),app(sK51_skl,sK50_skl)) = app(app(sK51_skl,sK50_skl),app(sK51_skl,sK50_skl)) ),
introduced(definition,[new_symbols(definition,[sQ1754_spl])],[split_symbol_definition]) ).
fof(f13935,plain,
( sQ1754_spl
| app(app(sK51_skl,sK50_skl),app(sK51_skl,sK50_skl)) != app(app(sK51_skl,sK50_skl),app(sK51_skl,sK50_skl)) ),
inference(component_clause,[status(thm)],[f13933]) ).
fof(f14051,definition,
( sQ1774_spl
<=> app(sK50_skl,app(sK51_skl,sK50_skl)) = app(sK50_skl,app(sK51_skl,sK50_skl)) ),
introduced(definition,[new_symbols(definition,[sQ1774_spl])],[split_symbol_definition]) ).
fof(f14053,plain,
( sQ1774_spl
| app(sK50_skl,app(sK51_skl,sK50_skl)) != app(sK50_skl,app(sK51_skl,sK50_skl)) ),
inference(component_clause,[status(thm)],[f14051]) ).
fof(f14081,definition,
( sQ1782_spl
<=> sK50_skl = cons(sK0_skl,sK50_skl) ),
introduced(definition,[new_symbols(definition,[sQ1782_spl])],[split_symbol_definition]) ).
fof(f14082,plain,
( ~ sQ1782_spl
| sK50_skl = cons(sK0_skl,sK50_skl) ),
inference(component_clause,[status(thm)],[f14081]) ).
fof(f14095,definition,
( sQ1786_spl
<=> sK50_skl = cons(sK1_skl,sK50_skl) ),
introduced(definition,[new_symbols(definition,[sQ1786_spl])],[split_symbol_definition]) ).
fof(f14096,plain,
( ~ sQ1786_spl
| sK50_skl = cons(sK1_skl,sK50_skl) ),
inference(component_clause,[status(thm)],[f14095]) ).
fof(f14147,plain,
( ~ sQ1786_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f14096,f1994]) ).
fof(f14148,plain,
~ sQ1786_spl,
inference(contradiction_clause,[status(thm)],[f14147]) ).
fof(f14150,plain,
( ~ sQ1782_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f14082,f1989]) ).
fof(f14151,plain,
~ sQ1782_spl,
inference(contradiction_clause,[status(thm)],[f14150]) ).
fof(f14155,plain,
( sQ1774_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f14053]) ).
fof(f14156,plain,
sQ1774_spl,
inference(contradiction_clause,[status(thm)],[f14155]) ).
fof(f14161,plain,
( sQ1754_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f13935]) ).
fof(f14162,plain,
sQ1754_spl,
inference(contradiction_clause,[status(thm)],[f14161]) ).
fof(f14248,definition,
( sQ1803_spl
<=> ssList(cons(sK0_skl,sK50_skl)) ),
introduced(definition,[new_symbols(definition,[sQ1803_spl])],[split_symbol_definition]) ).
fof(f14250,plain,
( sQ1803_spl
| ~ ssList(cons(sK0_skl,sK50_skl)) ),
inference(component_clause,[status(thm)],[f14248]) ).
fof(f14264,plain,
( sQ1803_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f14250,f1987]) ).
fof(f14265,plain,
sQ1803_spl,
inference(contradiction_clause,[status(thm)],[f14264]) ).
fof(f14372,definition,
( sQ1818_spl
<=> app(cons(sK0_skl,sK50_skl),cons(sK0_skl,sK50_skl)) = app(cons(sK0_skl,sK50_skl),cons(sK0_skl,sK50_skl)) ),
introduced(definition,[new_symbols(definition,[sQ1818_spl])],[split_symbol_definition]) ).
fof(f14374,plain,
( sQ1818_spl
| app(cons(sK0_skl,sK50_skl),cons(sK0_skl,sK50_skl)) != app(cons(sK0_skl,sK50_skl),cons(sK0_skl,sK50_skl)) ),
inference(component_clause,[status(thm)],[f14372]) ).
fof(f14432,plain,
( sQ1818_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f14374]) ).
fof(f14433,plain,
sQ1818_spl,
inference(contradiction_clause,[status(thm)],[f14432]) ).
fof(f14577,definition,
( sQ1854_spl
<=> lt(sK0_skl,sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ1854_spl])],[split_symbol_definition]) ).
fof(f14578,plain,
( ~ sQ1854_spl
| lt(sK0_skl,sK0_skl) ),
inference(component_clause,[status(thm)],[f14577]) ).
fof(f14602,plain,
( ~ sQ1854_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f14578,f781]) ).
fof(f14603,plain,
~ sQ1854_spl,
inference(contradiction_clause,[status(thm)],[f14602]) ).
fof(f14604,plain,
( ~ sQ1201_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f9345,f105]) ).
fof(f14605,plain,
~ sQ1201_spl,
inference(contradiction_clause,[status(thm)],[f14604]) ).
fof(f14627,definition,
( sQ1866_spl
<=> lt(sK1_skl,sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ1866_spl])],[split_symbol_definition]) ).
fof(f14628,plain,
( ~ sQ1866_spl
| lt(sK1_skl,sK1_skl) ),
inference(component_clause,[status(thm)],[f14627]) ).
fof(f14638,plain,
( ~ sQ1866_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f14628,f731]) ).
fof(f14639,plain,
~ sQ1866_spl,
inference(contradiction_clause,[status(thm)],[f14638]) ).
fof(f15664,definition,
( sQ2009_spl
<=> ssList(app(sK50_skl,sK50_skl)) ),
introduced(definition,[new_symbols(definition,[sQ2009_spl])],[split_symbol_definition]) ).
fof(f15666,plain,
( sQ2009_spl
| ~ ssList(app(sK50_skl,sK50_skl)) ),
inference(component_clause,[status(thm)],[f15664]) ).
fof(f15707,plain,
( sQ2009_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f15666,f5438]) ).
fof(f15708,plain,
sQ2009_spl,
inference(contradiction_clause,[status(thm)],[f15707]) ).
fof(f15827,definition,
( sQ2040_spl
<=> ssList(cons(sK1_skl,sK50_skl)) ),
introduced(definition,[new_symbols(definition,[sQ2040_spl])],[split_symbol_definition]) ).
fof(f15829,plain,
( sQ2040_spl
| ~ ssList(cons(sK1_skl,sK50_skl)) ),
inference(component_clause,[status(thm)],[f15827]) ).
fof(f15834,plain,
( sQ2040_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f15829,f1992]) ).
fof(f15835,plain,
sQ2040_spl,
inference(contradiction_clause,[status(thm)],[f15834]) ).
fof(f23297,plain,
( sQ731_spl
| ~ ssItem(sK24_skl(sK47_skl))
| ~ ssItem(sK25_skl(sK47_skl))
| ~ lt(sK24_skl(sK47_skl),sK25_skl(sK47_skl)) ),
inference(resolution,[status(thm)],[f6044,f409]) ).
fof(f23302,plain,
( sQ731_spl
| ~ sQ1250_spl
| ~ sQ1249_spl
| ~ sQ1247_spl ),
inference(split_clause,[status(thm)],[f23297,f9600,f9606,f9609,f6042]) ).
fof(f23318,plain,
$false,
inference(sat_refutation,[status(thm)],[f665,f669,f798,f806,f1193,f1314,f1872,f2256,f2487,f2725,f3387,f3541,f3649,f3651,f3674,f4161,f4265,f4267,f6045,f6202,f6271,f6993,f8009,f9179,f9181,f9499,f9548,f9612,f10825,f11265,f11445,f11448,f11451,f11459,f12419,f12422,f13485,f14148,f14151,f14156,f14162,f14265,f14433,f14603,f14605,f14639,f15708,f15835,f23302]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWC272+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.07 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.44 % Computer : n006.cluster.edu
% 0.17/0.44 % Model : x86_64 x86_64
% 0.17/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.44 % Memory : 8046.5625MB
% 0.17/0.44 % OS : Linux 6.8.0-71-generic
% 0.17/0.44 % CPULimit : 300
% 0.17/0.44 % WCLimit : 300
% 0.17/0.44 % DateTime : Mon Sep 21 08:10:27 UTC 2026
% 0.17/0.45 % CPUTime :
% 0.17/0.47 % Drodi V4.1.1
% 208.25/26.94 % Refutation found
% 208.25/26.94 % SZS status Theorem for theBenchmark: Theorem is valid
% 208.25/26.94 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 4.86/27.21 % Elapsed time: 26.754103 seconds
% 4.86/27.21 % CPU time: 209.842978 seconds
% 4.86/27.21 % Total memory used: 449.770 MB
% 4.86/27.21 % Net memory used: 412.932 MB
%------------------------------------------------------------------------------