%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWC155+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 : n004.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:11 PM UTC 2026
% Result : Theorem 0.13s 0.74s
% Output : CNFRefutation 0.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 37
% Syntax : Number of formulae : 169 ( 18 unt; 29 def)
% Number of atoms : 642 ( 47 equ)
% Maximal formula atoms : 27 ( 3 avg)
% Number of connectives : 806 ( 333 ~; 340 |; 65 &)
% ( 33 <=>; 35 =>; 0 <=; 0 <~>)
% Maximal formula depth : 30 ( 5 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 35 ( 33 usr; 30 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 11 con; 0-2 aty)
% Number of variables : 139 ( 115 !; 24 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssItem(V)
=> ( memberP(U,V)
<=> ? [W] :
( ? [X] :
( app(W,cons(V,X)) = U
& ssList(X) )
& ssList(W) ) ) ) ),
file('/export/starexec/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(f26,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ssList(app(U,V)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f29,axiom,
! [U] :
( ssItem(U)
=> ! [V] :
( ssItem(V)
=> ( ( leq(V,U)
& leq(U,V) )
=> U = V ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f36,axiom,
! [U] :
( ssItem(U)
=> ! [V] :
( ssList(V)
=> ! [W] :
( ssList(W)
=> ( memberP(app(V,W),U)
<=> ( memberP(W,U)
| memberP(V,U) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f82,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ! [W] :
( ssList(W)
=> app(app(U,V),W) = app(U,app(V,W)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f96,conjecture,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ! [W] :
( ssList(W)
=> ! [X] :
( ssList(X)
=> ( ! [X3] :
( ssItem(X3)
=> ! [X4] :
( ssItem(X4)
=> ! [X5] :
( ssList(X5)
=> ! [X6] :
( ssList(X6)
=> ! [X7] :
( ssList(X7)
=> ( ( leq(X3,X4)
& ! [X8] :
( ssItem(X8)
=> ( ( leq(X8,X4)
& leq(X3,X8) )
| ~ memberP(X6,X8) ) ) )
| ~ leq(X4,X3)
| app(app(app(app(X5,cons(X3,nil)),X6),cons(X4,nil)),X7) != U ) ) ) ) ) )
| ? [Y] :
( ? [Z] :
( ? [X1] :
( ? [X2] :
( ( ( memberP(Z,X2)
& ~ leq(X2,Y) )
| ( memberP(X1,X2)
& ~ leq(Y,X2) ) )
& ssItem(X2) )
& app(app(Z,cons(Y,nil)),X1) = W
& ssList(X1) )
& ssList(Z) )
& ssItem(Y) )
| 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)
=> ( ! [X3] :
( ssItem(X3)
=> ! [X4] :
( ssItem(X4)
=> ! [X5] :
( ssList(X5)
=> ! [X6] :
( ssList(X6)
=> ! [X7] :
( ssList(X7)
=> ( ( leq(X3,X4)
& ! [X8] :
( ssItem(X8)
=> ( ( leq(X8,X4)
& leq(X3,X8) )
| ~ memberP(X6,X8) ) ) )
| ~ leq(X4,X3)
| app(app(app(app(X5,cons(X3,nil)),X6),cons(X4,nil)),X7) != U ) ) ) ) ) )
| ? [Y] :
( ? [Z] :
( ? [X1] :
( ? [X2] :
( ( ( memberP(Z,X2)
& ~ leq(X2,Y) )
| ( memberP(X1,X2)
& ~ leq(Y,X2) ) )
& ssItem(X2) )
& app(app(Z,cons(Y,nil)),X1) = W
& ssList(X1) )
& ssList(Z) )
& ssItem(Y) )
| U != W
| V != X ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f96]) ).
fof(f106,plain,
! [U] :
( ! [V] :
( ( memberP(U,V)
<=> ? [W] :
( ? [X] :
( app(W,cons(V,X)) = U
& ssList(X) )
& ssList(W) ) )
| ~ ssItem(V) )
| ~ ssList(U) ),
inference(pre_NNF_transformation,[status(thm)],[f3]) ).
fof(f107,plain,
! [U] :
( ! [V] :
( ( ( ! [W] :
( ! [X] :
( app(W,cons(V,X)) != U
| ~ ssList(X) )
| ~ ssList(W) )
| memberP(U,V) )
& ( ? [W] :
( ? [X] :
( app(W,cons(V,X)) = U
& ssList(X) )
& ssList(W) )
| ~ memberP(U,V) ) )
| ~ ssItem(V) )
| ~ ssList(U) ),
inference(NNF_transformation,[status(thm)],[f106]) ).
fof(f108,plain,
! [U] :
( ! [V] :
( ( ( ! [W] :
( ! [X] :
( app(W,cons(V,X)) != U
| ~ ssList(X) )
| ~ ssList(W) )
| memberP(U,V) )
& ( ( app(sK2_skl(V,U),cons(V,sK3_skl(V,U))) = U
& ssList(sK3_skl(V,U))
& ssList(sK2_skl(V,U)) )
| ~ memberP(U,V) ) )
| ~ ssItem(V) )
| ~ ssList(U) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl,sK3_skl]),skolemize(W,sK2_skl(V,U)),skolemize(X,sK3_skl(V,U))],[f107]) ).
fof(f112,plain,
! [X0,X1,X2,X3] :
( app(X2,cons(X1,X3)) != X0
| ~ ssList(X3)
| ~ ssList(X2)
| memberP(X0,X1)
| ~ ssItem(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f108]) ).
fof(f221,plain,
! [U] :
( ! [V] :
( ssList(cons(V,U))
| ~ ssItem(V) )
| ~ ssList(U) ),
inference(pre_NNF_transformation,[status(thm)],[f16]) ).
fof(f222,plain,
! [X0,X1] :
( ssList(cons(X1,X0))
| ~ ssItem(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f221]) ).
fof(f223,plain,
ssList(nil),
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f244,plain,
! [U] :
( ! [V] :
( ssList(app(U,V))
| ~ ssList(V) )
| ~ ssList(U) ),
inference(pre_NNF_transformation,[status(thm)],[f26]) ).
fof(f245,plain,
! [X0,X1] :
( ssList(app(X0,X1))
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f244]) ).
fof(f250,plain,
! [U] :
( ! [V] :
( U = V
| ~ leq(V,U)
| ~ leq(U,V)
| ~ ssItem(V) )
| ~ ssItem(U) ),
inference(pre_NNF_transformation,[status(thm)],[f29]) ).
fof(f251,plain,
! [X0,X1] :
( X0 = X1
| ~ leq(X1,X0)
| ~ leq(X0,X1)
| ~ ssItem(X1)
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(thm)],[f250]) ).
fof(f268,plain,
! [U] :
( ! [V] :
( ! [W] :
( ( memberP(app(V,W),U)
<=> ( memberP(W,U)
| memberP(V,U) ) )
| ~ ssList(W) )
| ~ ssList(V) )
| ~ ssItem(U) ),
inference(pre_NNF_transformation,[status(thm)],[f36]) ).
fof(f269,plain,
! [U] :
( ! [V] :
( ! [W] :
( ( ( ( ~ memberP(W,U)
& ~ memberP(V,U) )
| memberP(app(V,W),U) )
& ( memberP(W,U)
| memberP(V,U)
| ~ memberP(app(V,W),U) ) )
| ~ ssList(W) )
| ~ ssList(V) )
| ~ ssItem(U) ),
inference(NNF_transformation,[status(thm)],[f268]) ).
fof(f271,plain,
! [X0,X1,X2] :
( ~ memberP(X1,X0)
| memberP(app(X1,X2),X0)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(thm)],[f269]) ).
fof(f272,plain,
! [X0,X1,X2] :
( ~ memberP(X2,X0)
| memberP(app(X1,X2),X0)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(thm)],[f269]) ).
fof(f381,plain,
! [U] :
( ! [V] :
( ! [W] :
( app(app(U,V),W) = app(U,app(V,W))
| ~ ssList(W) )
| ~ ssList(V) )
| ~ ssList(U) ),
inference(pre_NNF_transformation,[status(thm)],[f82]) ).
fof(f382,plain,
! [X0,X1,X2] :
( app(app(X0,X1),X2) = app(X0,app(X1,X2))
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f381]) ).
fof(f415,plain,
? [U] :
( ? [V] :
( ? [W] :
( ? [X] :
( ? [X3] :
( ? [X4] :
( ? [X5] :
( ? [X6] :
( ? [X7] :
( ( ~ leq(X3,X4)
| ? [X8] :
( ( ~ leq(X8,X4)
| ~ leq(X3,X8) )
& memberP(X6,X8)
& ssItem(X8) ) )
& leq(X4,X3)
& app(app(app(app(X5,cons(X3,nil)),X6),cons(X4,nil)),X7) = U
& ssList(X7) )
& ssList(X6) )
& ssList(X5) )
& ssItem(X4) )
& ssItem(X3) )
& ! [Y] :
( ! [Z] :
( ! [X1] :
( ! [X2] :
( ( ( ~ memberP(Z,X2)
| leq(X2,Y) )
& ( ~ memberP(X1,X2)
| leq(Y,X2) ) )
| ~ ssItem(X2) )
| app(app(Z,cons(Y,nil)),X1) != W
| ~ ssList(X1) )
| ~ ssList(Z) )
| ~ ssItem(Y) )
& U = W
& V = X
& ssList(X) )
& ssList(W) )
& ssList(V) )
& ssList(U) ),
inference(pre_NNF_transformation,[status(thm)],[f97]) ).
fof(f416,plain,
( ( ~ leq(sK51_skl,sK52_skl)
| ( ( ~ leq(sK56_skl,sK52_skl)
| ~ leq(sK51_skl,sK56_skl) )
& memberP(sK54_skl,sK56_skl)
& ssItem(sK56_skl) ) )
& leq(sK52_skl,sK51_skl)
& app(app(app(app(sK53_skl,cons(sK51_skl,nil)),sK54_skl),cons(sK52_skl,nil)),sK55_skl) = sK47_skl
& ssList(sK55_skl)
& ssList(sK54_skl)
& ssList(sK53_skl)
& ssItem(sK52_skl)
& ssItem(sK51_skl)
& ! [Y] :
( ! [Z] :
( ! [X1] :
( ! [X2] :
( ( ( ~ memberP(Z,X2)
| leq(X2,Y) )
& ( ~ memberP(X1,X2)
| leq(Y,X2) ) )
| ~ ssItem(X2) )
| app(app(Z,cons(Y,nil)),X1) != sK49_skl
| ~ ssList(X1) )
| ~ ssList(Z) )
| ~ ssItem(Y) )
& sK47_skl = sK49_skl
& sK48_skl = sK50_skl
& ssList(sK50_skl)
& ssList(sK49_skl)
& ssList(sK48_skl)
& ssList(sK47_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK47_skl,sK48_skl,sK49_skl,sK50_skl,sK51_skl,sK52_skl,sK53_skl,sK54_skl,sK55_skl,sK56_skl]),skolemize(U,sK47_skl),skolemize(V,sK48_skl),skolemize(W,sK49_skl),skolemize(X,sK50_skl),skolemize(X3,sK51_skl),skolemize(X4,sK52_skl),skolemize(X5,sK53_skl),skolemize(X6,sK54_skl),skolemize(X7,sK55_skl),skolemize(X8,sK56_skl)],[f415]) ).
fof(f422,plain,
sK47_skl = sK49_skl,
inference(cnf_transformation,[status(thm)],[f416]) ).
fof(f423,plain,
! [X0,X1,X2,X3] :
( ~ memberP(X2,X3)
| leq(X0,X3)
| ~ ssItem(X3)
| app(app(X1,cons(X0,nil)),X2) != sK49_skl
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(thm)],[f416]) ).
fof(f424,plain,
! [X0,X1,X2,X3] :
( ~ memberP(X1,X3)
| leq(X3,X0)
| ~ ssItem(X3)
| app(app(X1,cons(X0,nil)),X2) != sK49_skl
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(thm)],[f416]) ).
fof(f425,plain,
ssItem(sK51_skl),
inference(cnf_transformation,[status(thm)],[f416]) ).
fof(f426,plain,
ssItem(sK52_skl),
inference(cnf_transformation,[status(thm)],[f416]) ).
fof(f427,plain,
ssList(sK53_skl),
inference(cnf_transformation,[status(thm)],[f416]) ).
fof(f428,plain,
ssList(sK54_skl),
inference(cnf_transformation,[status(thm)],[f416]) ).
fof(f429,plain,
ssList(sK55_skl),
inference(cnf_transformation,[status(thm)],[f416]) ).
fof(f430,plain,
app(app(app(app(sK53_skl,cons(sK51_skl,nil)),sK54_skl),cons(sK52_skl,nil)),sK55_skl) = sK47_skl,
inference(cnf_transformation,[status(thm)],[f416]) ).
fof(f431,plain,
leq(sK52_skl,sK51_skl),
inference(cnf_transformation,[status(thm)],[f416]) ).
fof(f432,plain,
( ~ leq(sK51_skl,sK52_skl)
| ssItem(sK56_skl) ),
inference(cnf_transformation,[status(thm)],[f416]) ).
fof(f433,plain,
( ~ leq(sK51_skl,sK52_skl)
| memberP(sK54_skl,sK56_skl) ),
inference(cnf_transformation,[status(thm)],[f416]) ).
fof(f434,plain,
( ~ leq(sK51_skl,sK52_skl)
| ~ leq(sK56_skl,sK52_skl)
| ~ leq(sK51_skl,sK56_skl) ),
inference(cnf_transformation,[status(thm)],[f416]) ).
fof(f435,definition,
( sQ0_spl
<=> ssItem(sK56_skl) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f438,definition,
( sQ1_spl
<=> leq(sK51_skl,sK52_skl) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f441,plain,
( ~ sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f432,f435,f438]) ).
fof(f442,definition,
( sQ2_spl
<=> memberP(sK54_skl,sK56_skl) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f443,plain,
( ~ sQ2_spl
| memberP(sK54_skl,sK56_skl) ),
inference(component_clause,[status(thm)],[f442]) ).
fof(f445,plain,
( ~ sQ1_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f433,f442,f438]) ).
fof(f446,definition,
( sQ3_spl
<=> leq(sK51_skl,sK56_skl) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f448,plain,
( sQ3_spl
| ~ leq(sK51_skl,sK56_skl) ),
inference(component_clause,[status(thm)],[f446]) ).
fof(f449,definition,
( sQ4_spl
<=> leq(sK56_skl,sK52_skl) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f450,plain,
( ~ sQ4_spl
| leq(sK56_skl,sK52_skl) ),
inference(component_clause,[status(thm)],[f449]) ).
fof(f452,plain,
( ~ sQ1_spl
| ~ sQ4_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f434,f446,f449,f438]) ).
fof(f455,plain,
! [X0,X1,X2] :
( ~ ssList(X2)
| ~ ssList(X0)
| memberP(app(X0,cons(X1,X2)),X1)
| ~ ssItem(X1)
| ~ ssList(app(X0,cons(X1,X2))) ),
inference(destructive_equality_resolution,[status(thm)],[f112]) ).
fof(f487,plain,
app(app(app(app(sK53_skl,cons(sK51_skl,nil)),sK54_skl),cons(sK52_skl,nil)),sK55_skl) = sK49_skl,
inference(forward_demodulation,[status(thm)],[f422,f430]) ).
fof(f505,plain,
( sK51_skl = sK52_skl
| ~ leq(sK51_skl,sK52_skl)
| ~ ssItem(sK52_skl)
| ~ ssItem(sK51_skl) ),
inference(resolution,[status(thm)],[f251,f431]) ).
fof(f507,definition,
( sQ7_spl
<=> ssItem(sK51_skl) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f509,plain,
( sQ7_spl
| ~ ssItem(sK51_skl) ),
inference(component_clause,[status(thm)],[f507]) ).
fof(f510,definition,
( sQ8_spl
<=> ssItem(sK52_skl) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f512,plain,
( sQ8_spl
| ~ ssItem(sK52_skl) ),
inference(component_clause,[status(thm)],[f510]) ).
fof(f513,definition,
( sQ9_spl
<=> sK51_skl = sK52_skl ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f514,plain,
( ~ sQ9_spl
| sK51_skl = sK52_skl ),
inference(component_clause,[status(thm)],[f513]) ).
fof(f516,plain,
( sQ9_spl
| ~ sQ1_spl
| ~ sQ8_spl
| ~ sQ7_spl ),
inference(split_clause,[status(thm)],[f505,f507,f510,f438,f513]) ).
fof(f523,plain,
( sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f509,f425]) ).
fof(f524,plain,
sQ7_spl,
inference(contradiction_clause,[status(thm)],[f523]) ).
fof(f525,plain,
( sQ8_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f512,f426]) ).
fof(f526,plain,
sQ8_spl,
inference(contradiction_clause,[status(thm)],[f525]) ).
fof(f534,definition,
( sQ12_spl
<=> ssList(app(app(sK53_skl,cons(sK51_skl,nil)),sK54_skl)) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f535,plain,
( ~ sQ12_spl
| ssList(app(app(sK53_skl,cons(sK51_skl,nil)),sK54_skl)) ),
inference(component_clause,[status(thm)],[f534]) ).
fof(f536,plain,
( sQ12_spl
| ~ ssList(app(app(sK53_skl,cons(sK51_skl,nil)),sK54_skl)) ),
inference(component_clause,[status(thm)],[f534]) ).
fof(f537,definition,
( sQ13_spl
<=> ssList(sK55_skl) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f539,plain,
( sQ13_spl
| ~ ssList(sK55_skl) ),
inference(component_clause,[status(thm)],[f537]) ).
fof(f548,plain,
! [X0] :
( ~ memberP(app(app(sK53_skl,cons(sK51_skl,nil)),sK54_skl),X0)
| leq(X0,sK52_skl)
| ~ ssItem(X0)
| ~ ssList(sK55_skl)
| ~ ssList(app(app(sK53_skl,cons(sK51_skl,nil)),sK54_skl))
| ~ ssItem(sK52_skl) ),
inference(resolution,[status(thm)],[f424,f487]) ).
fof(f550,definition,
! [X0] :
( sQ16_spl
<=> ( ~ memberP(app(app(sK53_skl,cons(sK51_skl,nil)),sK54_skl),X0)
| leq(X0,sK52_skl)
| ~ ssItem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f551,plain,
! [X0] :
( ~ sQ16_spl
| ~ memberP(app(app(sK53_skl,cons(sK51_skl,nil)),sK54_skl),X0)
| leq(X0,sK52_skl)
| ~ ssItem(X0) ),
inference(component_clause,[status(thm)],[f550]) ).
fof(f553,plain,
( sQ16_spl
| ~ sQ13_spl
| ~ sQ12_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f548,f510,f534,f537,f550]) ).
fof(f555,plain,
( sQ13_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f539,f429]) ).
fof(f556,plain,
sQ13_spl,
inference(contradiction_clause,[status(thm)],[f555]) ).
fof(f557,plain,
( sQ12_spl
| ~ ssList(sK54_skl)
| ~ ssList(app(sK53_skl,cons(sK51_skl,nil))) ),
inference(resolution,[status(thm)],[f245,f536]) ).
fof(f559,definition,
( sQ17_spl
<=> ssList(app(sK53_skl,cons(sK51_skl,nil))) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f560,plain,
( ~ sQ17_spl
| ssList(app(sK53_skl,cons(sK51_skl,nil))) ),
inference(component_clause,[status(thm)],[f559]) ).
fof(f561,plain,
( sQ17_spl
| ~ ssList(app(sK53_skl,cons(sK51_skl,nil))) ),
inference(component_clause,[status(thm)],[f559]) ).
fof(f562,definition,
( sQ18_spl
<=> ssList(sK54_skl) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f564,plain,
( sQ18_spl
| ~ ssList(sK54_skl) ),
inference(component_clause,[status(thm)],[f562]) ).
fof(f565,plain,
( sQ12_spl
| ~ sQ18_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f557,f559,f562,f534]) ).
fof(f573,plain,
( sQ17_spl
| ~ ssList(cons(sK51_skl,nil))
| ~ ssList(sK53_skl) ),
inference(resolution,[status(thm)],[f561,f245]) ).
fof(f574,definition,
( sQ21_spl
<=> ssList(sK53_skl) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f576,plain,
( sQ21_spl
| ~ ssList(sK53_skl) ),
inference(component_clause,[status(thm)],[f574]) ).
fof(f577,definition,
( sQ22_spl
<=> ssList(cons(sK51_skl,nil)) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f578,plain,
( ~ sQ22_spl
| ssList(cons(sK51_skl,nil)) ),
inference(component_clause,[status(thm)],[f577]) ).
fof(f579,plain,
( sQ22_spl
| ~ ssList(cons(sK51_skl,nil)) ),
inference(component_clause,[status(thm)],[f577]) ).
fof(f580,plain,
( sQ17_spl
| ~ sQ22_spl
| ~ sQ21_spl ),
inference(split_clause,[status(thm)],[f573,f574,f577,f559]) ).
fof(f581,plain,
( sQ18_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f564,f428]) ).
fof(f582,plain,
sQ18_spl,
inference(contradiction_clause,[status(thm)],[f581]) ).
fof(f583,plain,
( sQ21_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f576,f427]) ).
fof(f584,plain,
sQ21_spl,
inference(contradiction_clause,[status(thm)],[f583]) ).
fof(f585,plain,
( sQ22_spl
| ~ ssItem(sK51_skl)
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f579,f222]) ).
fof(f586,definition,
( sQ23_spl
<=> ssList(nil) ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f588,plain,
( sQ23_spl
| ~ ssList(nil) ),
inference(component_clause,[status(thm)],[f586]) ).
fof(f589,plain,
( sQ22_spl
| ~ sQ7_spl
| ~ sQ23_spl ),
inference(split_clause,[status(thm)],[f585,f586,f507,f577]) ).
fof(f590,plain,
( sQ23_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f588,f223]) ).
fof(f591,plain,
sQ23_spl,
inference(contradiction_clause,[status(thm)],[f590]) ).
fof(f632,definition,
( sQ30_spl
<=> ssList(cons(sK52_skl,nil)) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f634,plain,
( sQ30_spl
| ~ ssList(cons(sK52_skl,nil)) ),
inference(component_clause,[status(thm)],[f632]) ).
fof(f685,plain,
! [X0] :
( ~ sQ16_spl
| leq(X0,sK52_skl)
| ~ ssItem(X0)
| ~ memberP(sK54_skl,X0)
| ~ ssList(sK54_skl)
| ~ ssList(app(sK53_skl,cons(sK51_skl,nil)))
| ~ ssItem(X0) ),
inference(resolution,[status(thm)],[f272,f551]) ).
fof(f687,definition,
! [X0] :
( sQ38_spl
<=> ( leq(X0,sK52_skl)
| ~ ssItem(X0)
| ~ memberP(sK54_skl,X0)
| ~ ssItem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f688,plain,
! [X0] :
( ~ sQ38_spl
| leq(X0,sK52_skl)
| ~ ssItem(X0)
| ~ memberP(sK54_skl,X0)
| ~ ssItem(X0) ),
inference(component_clause,[status(thm)],[f687]) ).
fof(f690,plain,
( ~ sQ16_spl
| ~ sQ18_spl
| ~ sQ17_spl
| sQ38_spl ),
inference(split_clause,[status(thm)],[f685,f687,f559,f562,f550]) ).
fof(f695,plain,
! [X0] :
( ~ sQ38_spl
| leq(X0,sK52_skl)
| ~ memberP(sK54_skl,X0)
| ~ ssItem(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f688]) ).
fof(f696,plain,
! [X0] :
( ~ sQ16_spl
| leq(X0,sK52_skl)
| ~ ssItem(X0)
| ~ memberP(app(sK53_skl,cons(sK51_skl,nil)),X0)
| ~ ssList(sK54_skl)
| ~ ssList(app(sK53_skl,cons(sK51_skl,nil)))
| ~ ssItem(X0) ),
inference(resolution,[status(thm)],[f271,f551]) ).
fof(f698,definition,
! [X0] :
( sQ40_spl
<=> ( leq(X0,sK52_skl)
| ~ ssItem(X0)
| ~ memberP(app(sK53_skl,cons(sK51_skl,nil)),X0)
| ~ ssItem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f699,plain,
! [X0] :
( ~ sQ40_spl
| leq(X0,sK52_skl)
| ~ ssItem(X0)
| ~ memberP(app(sK53_skl,cons(sK51_skl,nil)),X0)
| ~ ssItem(X0) ),
inference(component_clause,[status(thm)],[f698]) ).
fof(f701,plain,
( ~ sQ16_spl
| ~ sQ18_spl
| ~ sQ17_spl
| sQ40_spl ),
inference(split_clause,[status(thm)],[f696,f698,f559,f562,f550]) ).
fof(f706,plain,
! [X0] :
( ~ sQ40_spl
| leq(X0,sK52_skl)
| ~ memberP(app(sK53_skl,cons(sK51_skl,nil)),X0)
| ~ ssItem(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f699]) ).
fof(f707,plain,
( ~ sQ40_spl
| ~ ssList(nil)
| ~ ssList(sK53_skl)
| ~ ssItem(sK51_skl)
| ~ ssList(app(sK53_skl,cons(sK51_skl,nil)))
| leq(sK51_skl,sK52_skl)
| ~ ssItem(sK51_skl) ),
inference(resolution,[status(thm)],[f706,f455]) ).
fof(f710,plain,
( ~ sQ40_spl
| ~ sQ23_spl
| ~ sQ21_spl
| ~ sQ17_spl
| sQ1_spl
| ~ sQ7_spl ),
inference(split_clause,[status(thm)],[f707,f507,f438,f559,f574,f586,f698]) ).
fof(f721,plain,
( ~ sQ12_spl
| ~ sQ9_spl
| ssList(app(app(sK53_skl,cons(sK52_skl,nil)),sK54_skl)) ),
inference(backward_demodulation,[status(thm)],[f514,f535]) ).
fof(f723,plain,
( ~ sQ17_spl
| ~ sQ9_spl
| ssList(app(sK53_skl,cons(sK52_skl,nil))) ),
inference(backward_demodulation,[status(thm)],[f514,f560]) ).
fof(f724,plain,
( ~ sQ22_spl
| ~ sQ9_spl
| ssList(cons(sK52_skl,nil)) ),
inference(backward_demodulation,[status(thm)],[f514,f578]) ).
fof(f725,plain,
( ~ sQ9_spl
| app(app(app(app(sK53_skl,cons(sK52_skl,nil)),sK54_skl),cons(sK52_skl,nil)),sK55_skl) = sK49_skl ),
inference(backward_demodulation,[status(thm)],[f514,f487]) ).
fof(f737,plain,
( sQ3_spl
| ~ sQ9_spl
| ~ leq(sK52_skl,sK56_skl) ),
inference(forward_demodulation,[status(thm)],[f514,f448]) ).
fof(f741,plain,
( ~ sQ38_spl
| ~ sQ2_spl
| leq(sK56_skl,sK52_skl)
| ~ ssItem(sK56_skl) ),
inference(resolution,[status(thm)],[f443,f695]) ).
fof(f742,plain,
( ~ sQ38_spl
| ~ sQ2_spl
| sQ4_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f741,f435,f449,f442,f687]) ).
fof(f767,plain,
( ~ sQ4_spl
| sK52_skl = sK56_skl
| ~ leq(sK52_skl,sK56_skl)
| ~ ssItem(sK56_skl)
| ~ ssItem(sK52_skl) ),
inference(resolution,[status(thm)],[f450,f251]) ).
fof(f776,definition,
( sQ50_spl
<=> leq(sK52_skl,sK56_skl) ),
introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition]) ).
fof(f779,definition,
( sQ51_spl
<=> sK52_skl = sK56_skl ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f780,plain,
( ~ sQ51_spl
| sK52_skl = sK56_skl ),
inference(component_clause,[status(thm)],[f779]) ).
fof(f782,plain,
( ~ sQ4_spl
| sQ51_spl
| ~ sQ50_spl
| ~ sQ0_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f767,f510,f435,f776,f779,f449]) ).
fof(f810,definition,
( sQ53_spl
<=> ssList(app(sK53_skl,cons(sK52_skl,nil))) ),
introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition]) ).
fof(f812,plain,
( sQ53_spl
| ~ ssList(app(sK53_skl,cons(sK52_skl,nil))) ),
inference(component_clause,[status(thm)],[f810]) ).
fof(f819,plain,
( sQ30_spl
| ~ sQ22_spl
| ~ sQ9_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f634,f724]) ).
fof(f820,plain,
( sQ30_spl
| ~ sQ22_spl
| ~ sQ9_spl ),
inference(contradiction_clause,[status(thm)],[f819]) ).
fof(f826,plain,
( ~ sQ9_spl
| sK49_skl = app(app(app(sK53_skl,cons(sK52_skl,nil)),sK54_skl),app(cons(sK52_skl,nil),sK55_skl))
| ~ ssList(sK55_skl)
| ~ ssList(cons(sK52_skl,nil))
| ~ ssList(app(app(sK53_skl,cons(sK52_skl,nil)),sK54_skl)) ),
inference(paramodulation,[status(thm)],[f725,f382]) ).
fof(f839,definition,
( sQ55_spl
<=> ssList(app(app(sK53_skl,cons(sK52_skl,nil)),sK54_skl)) ),
introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition]) ).
fof(f841,plain,
( sQ55_spl
| ~ ssList(app(app(sK53_skl,cons(sK52_skl,nil)),sK54_skl)) ),
inference(component_clause,[status(thm)],[f839]) ).
fof(f849,definition,
( sQ57_spl
<=> sK49_skl = app(app(app(sK53_skl,cons(sK52_skl,nil)),sK54_skl),app(cons(sK52_skl,nil),sK55_skl)) ),
introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition]) ).
fof(f850,plain,
( ~ sQ57_spl
| sK49_skl = app(app(app(sK53_skl,cons(sK52_skl,nil)),sK54_skl),app(cons(sK52_skl,nil),sK55_skl)) ),
inference(component_clause,[status(thm)],[f849]) ).
fof(f852,plain,
( ~ sQ9_spl
| sQ57_spl
| ~ sQ13_spl
| ~ sQ30_spl
| ~ sQ55_spl ),
inference(split_clause,[status(thm)],[f826,f839,f632,f537,f849,f513]) ).
fof(f888,plain,
( sQ55_spl
| ~ sQ12_spl
| ~ sQ9_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f841,f721]) ).
fof(f889,plain,
( sQ55_spl
| ~ sQ12_spl
| ~ sQ9_spl ),
inference(contradiction_clause,[status(thm)],[f888]) ).
fof(f916,plain,
( sQ53_spl
| ~ sQ17_spl
| ~ sQ9_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f812,f723]) ).
fof(f917,plain,
( sQ53_spl
| ~ sQ17_spl
| ~ sQ9_spl ),
inference(contradiction_clause,[status(thm)],[f916]) ).
fof(f919,plain,
( ~ sQ57_spl
| sK49_skl = app(app(sK53_skl,cons(sK52_skl,nil)),app(sK54_skl,app(cons(sK52_skl,nil),sK55_skl)))
| ~ ssList(app(cons(sK52_skl,nil),sK55_skl))
| ~ ssList(sK54_skl)
| ~ ssList(app(sK53_skl,cons(sK52_skl,nil))) ),
inference(paramodulation,[status(thm)],[f850,f382]) ).
fof(f934,definition,
( sQ69_spl
<=> ssList(app(cons(sK52_skl,nil),sK55_skl)) ),
introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition]) ).
fof(f936,plain,
( sQ69_spl
| ~ ssList(app(cons(sK52_skl,nil),sK55_skl)) ),
inference(component_clause,[status(thm)],[f934]) ).
fof(f937,definition,
( sQ70_spl
<=> sK49_skl = app(app(sK53_skl,cons(sK52_skl,nil)),app(sK54_skl,app(cons(sK52_skl,nil),sK55_skl))) ),
introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition]) ).
fof(f938,plain,
( ~ sQ70_spl
| sK49_skl = app(app(sK53_skl,cons(sK52_skl,nil)),app(sK54_skl,app(cons(sK52_skl,nil),sK55_skl))) ),
inference(component_clause,[status(thm)],[f937]) ).
fof(f940,plain,
( ~ sQ57_spl
| sQ70_spl
| ~ sQ69_spl
| ~ sQ18_spl
| ~ sQ53_spl ),
inference(split_clause,[status(thm)],[f919,f810,f562,f934,f937,f849]) ).
fof(f988,plain,
( sQ69_spl
| ~ ssList(sK55_skl)
| ~ ssList(cons(sK52_skl,nil)) ),
inference(resolution,[status(thm)],[f936,f245]) ).
fof(f989,plain,
( sQ69_spl
| ~ sQ13_spl
| ~ sQ30_spl ),
inference(split_clause,[status(thm)],[f988,f632,f537,f934]) ).
fof(f1050,plain,
( ~ sQ4_spl
| ~ sQ51_spl
| leq(sK56_skl,sK56_skl) ),
inference(backward_demodulation,[status(thm)],[f780,f450]) ).
fof(f1053,plain,
( sQ3_spl
| ~ sQ9_spl
| ~ sQ51_spl
| ~ leq(sK56_skl,sK56_skl) ),
inference(backward_demodulation,[status(thm)],[f780,f737]) ).
fof(f1086,plain,
( sQ3_spl
| ~ sQ9_spl
| ~ sQ51_spl
| ~ sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1053,f1050]) ).
fof(f1087,plain,
( sQ3_spl
| ~ sQ9_spl
| ~ sQ51_spl
| ~ sQ4_spl ),
inference(contradiction_clause,[status(thm)],[f1086]) ).
fof(f1455,plain,
! [X0] :
( ~ sQ70_spl
| ~ memberP(app(sK54_skl,app(cons(sK52_skl,nil),sK55_skl)),X0)
| leq(sK52_skl,X0)
| ~ ssItem(X0)
| ~ ssList(app(sK54_skl,app(cons(sK52_skl,nil),sK55_skl)))
| ~ ssList(sK53_skl)
| ~ ssItem(sK52_skl) ),
inference(resolution,[status(thm)],[f938,f423]) ).
fof(f1473,definition,
( sQ125_spl
<=> ssList(app(sK54_skl,app(cons(sK52_skl,nil),sK55_skl))) ),
introduced(definition,[new_symbols(definition,[sQ125_spl])],[split_symbol_definition]) ).
fof(f1475,plain,
( sQ125_spl
| ~ ssList(app(sK54_skl,app(cons(sK52_skl,nil),sK55_skl))) ),
inference(component_clause,[status(thm)],[f1473]) ).
fof(f1480,definition,
! [X0] :
( sQ127_spl
<=> ( ~ memberP(app(sK54_skl,app(cons(sK52_skl,nil),sK55_skl)),X0)
| leq(sK52_skl,X0)
| ~ ssItem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ127_spl])],[split_symbol_definition]) ).
fof(f1481,plain,
! [X0] :
( ~ sQ127_spl
| ~ memberP(app(sK54_skl,app(cons(sK52_skl,nil),sK55_skl)),X0)
| leq(sK52_skl,X0)
| ~ ssItem(X0) ),
inference(component_clause,[status(thm)],[f1480]) ).
fof(f1483,plain,
( ~ sQ70_spl
| sQ127_spl
| ~ sQ125_spl
| ~ sQ21_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f1455,f510,f574,f1473,f1480,f937]) ).
fof(f1537,plain,
( sQ125_spl
| ~ ssList(app(cons(sK52_skl,nil),sK55_skl))
| ~ ssList(sK54_skl) ),
inference(resolution,[status(thm)],[f1475,f245]) ).
fof(f1538,plain,
( sQ125_spl
| ~ sQ69_spl
| ~ sQ18_spl ),
inference(split_clause,[status(thm)],[f1537,f562,f934,f1473]) ).
fof(f1572,plain,
! [X0] :
( ~ sQ127_spl
| ~ memberP(sK54_skl,X0)
| ~ ssList(app(cons(sK52_skl,nil),sK55_skl))
| ~ ssList(sK54_skl)
| ~ ssItem(X0)
| leq(sK52_skl,X0)
| ~ ssItem(X0) ),
inference(resolution,[status(thm)],[f1481,f271]) ).
fof(f1574,definition,
! [X0] :
( sQ145_spl
<=> ( ~ memberP(sK54_skl,X0)
| ~ ssItem(X0)
| leq(sK52_skl,X0)
| ~ ssItem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ145_spl])],[split_symbol_definition]) ).
fof(f1575,plain,
! [X0] :
( ~ sQ145_spl
| ~ memberP(sK54_skl,X0)
| ~ ssItem(X0)
| leq(sK52_skl,X0)
| ~ ssItem(X0) ),
inference(component_clause,[status(thm)],[f1574]) ).
fof(f1577,plain,
( ~ sQ127_spl
| ~ sQ69_spl
| ~ sQ18_spl
| sQ145_spl ),
inference(split_clause,[status(thm)],[f1572,f1574,f562,f934,f1480]) ).
fof(f1582,plain,
! [X0] :
( ~ sQ145_spl
| ~ memberP(sK54_skl,X0)
| leq(sK52_skl,X0)
| ~ ssItem(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1575]) ).
fof(f1595,plain,
( ~ sQ2_spl
| ~ sQ145_spl
| leq(sK52_skl,sK56_skl)
| ~ ssItem(sK56_skl) ),
inference(resolution,[status(thm)],[f1582,f443]) ).
fof(f1596,plain,
( ~ sQ2_spl
| ~ sQ145_spl
| sQ50_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f1595,f435,f776,f1574,f442]) ).
fof(f1597,plain,
$false,
inference(sat_refutation,[status(thm)],[f441,f445,f452,f516,f524,f526,f553,f556,f565,f580,f582,f584,f589,f591,f690,f701,f710,f742,f782,f820,f852,f889,f917,f940,f989,f1087,f1483,f1538,f1577,f1596]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWC155+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.56 % Computer : n004.cluster.edu
% 0.09/0.56 % Model : x86_64 x86_64
% 0.09/0.56 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.56 % Memory : 8046.5625MB
% 0.09/0.56 % OS : Linux 6.8.0-71-generic
% 0.09/0.56 % CPULimit : 300
% 0.09/0.56 % WCLimit : 300
% 0.09/0.56 % DateTime : Mon Sep 21 07:59:53 UTC 2026
% 0.09/0.57 % CPUTime :
% 0.09/0.58 % Drodi V4.1.1
% 0.13/0.74 % Refutation found
% 0.13/0.74 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.13/0.74 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.13/0.74 % Elapsed time: 0.171966 seconds
% 0.13/0.74 % CPU time: 1.106043 seconds
% 0.13/0.74 % Total memory used: 127.511 MB
% 0.13/0.74 % Net memory used: 125.986 MB
%------------------------------------------------------------------------------