%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWC190+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 : n001.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:20 PM UTC 2026
% Result : Theorem 0.02s 0.42s
% Output : CNFRefutation 0.02s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 24
% Syntax : Number of formulae : 113 ( 18 unt; 18 def)
% Number of atoms : 403 ( 42 equ)
% Maximal formula atoms : 16 ( 3 avg)
% Number of connectives : 484 ( 194 ~; 197 |; 47 &)
% ( 22 <=>; 24 =>; 0 <=; 0 <~>)
% Maximal formula depth : 23 ( 5 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 23 ( 21 usr; 19 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 10 con; 0-2 aty)
% Number of variables : 100 ( 80 !; 20 ?)
% Comments :
%------------------------------------------------------------------------------
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(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(f37,axiom,
! [U] :
( ssItem(U)
=> ! [V] :
( ssItem(V)
=> ! [W] :
( ssList(W)
=> ( memberP(cons(V,W),U)
<=> ( memberP(W,U)
| U = V ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f96,conjecture,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ! [W] :
( ssList(W)
=> ! [X] :
( ! [X3] :
( ssItem(X3)
=> ? [X4] :
( memberP(W,X4)
& X3 != X4
& ssItem(X4) ) )
| ! [Y] :
( ssItem(Y)
=> ! [Z] :
( ssItem(Z)
=> ! [X1] :
( ssList(X1)
=> ! [X2] :
( Y = Z
| app(app(app(X1,cons(Y,nil)),cons(Z,nil)),X2) != U
| ~ ssList(X2) ) ) ) )
| 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] :
( ! [X3] :
( ssItem(X3)
=> ? [X4] :
( memberP(W,X4)
& X3 != X4
& ssItem(X4) ) )
| ! [Y] :
( ssItem(Y)
=> ! [Z] :
( ssItem(Z)
=> ! [X1] :
( ssList(X1)
=> ! [X2] :
( Y = Z
| app(app(app(X1,cons(Y,nil)),cons(Z,nil)),X2) != U
| ~ ssList(X2) ) ) ) )
| U != W
| V != X
| ~ ssList(X) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f96]) ).
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(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(f273,plain,
! [U] :
( ! [V] :
( ! [W] :
( ( memberP(cons(V,W),U)
<=> ( memberP(W,U)
| U = V ) )
| ~ ssList(W) )
| ~ ssItem(V) )
| ~ ssItem(U) ),
inference(pre_NNF_transformation,[status(thm)],[f37]) ).
fof(f274,plain,
! [U] :
( ! [V] :
( ! [W] :
( ( ( ( ~ memberP(W,U)
& U != V )
| memberP(cons(V,W),U) )
& ( memberP(W,U)
| U = V
| ~ memberP(cons(V,W),U) ) )
| ~ ssList(W) )
| ~ ssItem(V) )
| ~ ssItem(U) ),
inference(NNF_transformation,[status(thm)],[f273]) ).
fof(f276,plain,
! [X0,X1,X2] :
( X0 != X1
| memberP(cons(X1,X2),X0)
| ~ ssList(X2)
| ~ ssItem(X1)
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(thm)],[f274]) ).
fof(f415,plain,
? [U] :
( ? [V] :
( ? [W] :
( ? [X] :
( ? [X3] :
( ! [X4] :
( ~ memberP(W,X4)
| X3 = X4
| ~ ssItem(X4) )
& ssItem(X3) )
& ? [Y] :
( ? [Z] :
( ? [X1] :
( ? [X2] :
( Y != Z
& app(app(app(X1,cons(Y,nil)),cons(Z,nil)),X2) = U
& ssList(X2) )
& ssList(X1) )
& ssItem(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,
? [U] :
( ? [V] :
( ? [W] :
( ? [X3] :
( ! [X4] :
( ~ memberP(W,X4)
| X3 = X4
| ~ ssItem(X4) )
& ssItem(X3) )
& ? [Y] :
( ? [Z] :
( ? [X1] :
( Y != Z
& ? [X2] :
( app(app(app(X1,cons(Y,nil)),cons(Z,nil)),X2) = U
& ssList(X2) )
& ssList(X1) )
& ssItem(Z) )
& ssItem(Y) )
& U = W
& ? [X] :
( V = X
& ssList(X) )
& ssList(W) )
& ssList(V) )
& ssList(U) ),
inference(miniscoping,[status(thm)],[f415]) ).
fof(f417,plain,
( ! [X4] :
( ~ memberP(sK49_skl,X4)
| sK55_skl = X4
| ~ ssItem(X4) )
& ssItem(sK55_skl)
& sK51_skl != sK52_skl
& app(app(app(sK53_skl,cons(sK51_skl,nil)),cons(sK52_skl,nil)),sK54_skl) = sK47_skl
& ssList(sK54_skl)
& ssList(sK53_skl)
& ssItem(sK52_skl)
& ssItem(sK51_skl)
& sK47_skl = sK49_skl
& sK48_skl = sK50_skl
& ssList(sK50_skl)
& ssList(sK49_skl)
& ssList(sK48_skl)
& ssList(sK47_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK47_skl,sK48_skl,sK49_skl,sK50_skl,sK51_skl,sK52_skl,sK53_skl,sK54_skl,sK55_skl]),skolemize(U,sK47_skl),skolemize(V,sK48_skl),skolemize(W,sK49_skl),skolemize(X,sK50_skl),skolemize(Y,sK51_skl),skolemize(Z,sK52_skl),skolemize(X1,sK53_skl),skolemize(X2,sK54_skl),skolemize(X3,sK55_skl)],[f416]) ).
fof(f423,plain,
sK47_skl = sK49_skl,
inference(cnf_transformation,[status(thm)],[f417]) ).
fof(f424,plain,
ssItem(sK51_skl),
inference(cnf_transformation,[status(thm)],[f417]) ).
fof(f425,plain,
ssItem(sK52_skl),
inference(cnf_transformation,[status(thm)],[f417]) ).
fof(f426,plain,
ssList(sK53_skl),
inference(cnf_transformation,[status(thm)],[f417]) ).
fof(f427,plain,
ssList(sK54_skl),
inference(cnf_transformation,[status(thm)],[f417]) ).
fof(f428,plain,
app(app(app(sK53_skl,cons(sK51_skl,nil)),cons(sK52_skl,nil)),sK54_skl) = sK47_skl,
inference(cnf_transformation,[status(thm)],[f417]) ).
fof(f429,plain,
sK51_skl != sK52_skl,
inference(cnf_transformation,[status(thm)],[f417]) ).
fof(f430,plain,
ssItem(sK55_skl),
inference(cnf_transformation,[status(thm)],[f417]) ).
fof(f431,plain,
! [X0] :
( ~ memberP(sK49_skl,X0)
| sK55_skl = X0
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(thm)],[f417]) ).
fof(f449,plain,
! [X1,X2] :
( memberP(cons(X1,X2),X1)
| ~ ssList(X2)
| ~ ssItem(X1)
| ~ ssItem(X1) ),
inference(destructive_equality_resolution,[status(thm)],[f276]) ).
fof(f450,plain,
! [X0,X1] :
( memberP(cons(X0,X1),X0)
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f449]) ).
fof(f466,plain,
app(app(app(sK53_skl,cons(sK51_skl,nil)),cons(sK52_skl,nil)),sK54_skl) = sK49_skl,
inference(forward_demodulation,[status(thm)],[f423,f428]) ).
fof(f468,definition,
( sQ0_spl
<=> ssList(app(app(sK53_skl,cons(sK51_skl,nil)),cons(sK52_skl,nil))) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f470,plain,
( sQ0_spl
| ~ ssList(app(app(sK53_skl,cons(sK51_skl,nil)),cons(sK52_skl,nil))) ),
inference(component_clause,[status(thm)],[f468]) ).
fof(f471,definition,
( sQ1_spl
<=> ssList(sK54_skl) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f473,plain,
( sQ1_spl
| ~ ssList(sK54_skl) ),
inference(component_clause,[status(thm)],[f471]) ).
fof(f514,definition,
( sQ9_spl
<=> ssList(nil) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f516,plain,
( sQ9_spl
| ~ ssList(nil) ),
inference(component_clause,[status(thm)],[f514]) ).
fof(f526,plain,
( sQ9_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f516,f223]) ).
fof(f527,plain,
sQ9_spl,
inference(contradiction_clause,[status(thm)],[f526]) ).
fof(f529,plain,
( sQ0_spl
| ~ ssList(cons(sK52_skl,nil))
| ~ ssList(app(sK53_skl,cons(sK51_skl,nil))) ),
inference(resolution,[status(thm)],[f245,f470]) ).
fof(f531,definition,
( sQ12_spl
<=> ssList(app(sK53_skl,cons(sK51_skl,nil))) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f533,plain,
( sQ12_spl
| ~ ssList(app(sK53_skl,cons(sK51_skl,nil))) ),
inference(component_clause,[status(thm)],[f531]) ).
fof(f534,definition,
( sQ13_spl
<=> ssList(cons(sK52_skl,nil)) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f536,plain,
( sQ13_spl
| ~ ssList(cons(sK52_skl,nil)) ),
inference(component_clause,[status(thm)],[f534]) ).
fof(f537,plain,
( sQ0_spl
| ~ sQ13_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f529,f531,f534,f468]) ).
fof(f539,plain,
( sQ1_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f473,f427]) ).
fof(f540,plain,
sQ1_spl,
inference(contradiction_clause,[status(thm)],[f539]) ).
fof(f541,plain,
( sQ12_spl
| ~ ssList(cons(sK51_skl,nil))
| ~ ssList(sK53_skl) ),
inference(resolution,[status(thm)],[f533,f245]) ).
fof(f542,definition,
( sQ14_spl
<=> ssList(sK53_skl) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f544,plain,
( sQ14_spl
| ~ ssList(sK53_skl) ),
inference(component_clause,[status(thm)],[f542]) ).
fof(f545,definition,
( sQ15_spl
<=> ssList(cons(sK51_skl,nil)) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f547,plain,
( sQ15_spl
| ~ ssList(cons(sK51_skl,nil)) ),
inference(component_clause,[status(thm)],[f545]) ).
fof(f548,plain,
( sQ12_spl
| ~ sQ15_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f541,f542,f545,f531]) ).
fof(f553,plain,
( sQ15_spl
| ~ ssItem(sK51_skl)
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f222,f547]) ).
fof(f554,plain,
( sQ13_spl
| ~ ssItem(sK52_skl)
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f222,f536]) ).
fof(f555,definition,
( sQ16_spl
<=> ssItem(sK51_skl) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f557,plain,
( sQ16_spl
| ~ ssItem(sK51_skl) ),
inference(component_clause,[status(thm)],[f555]) ).
fof(f558,plain,
( sQ15_spl
| ~ sQ16_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f553,f514,f555,f545]) ).
fof(f559,definition,
( sQ17_spl
<=> ssItem(sK52_skl) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f561,plain,
( sQ17_spl
| ~ ssItem(sK52_skl) ),
inference(component_clause,[status(thm)],[f559]) ).
fof(f562,plain,
( sQ13_spl
| ~ sQ17_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f554,f514,f559,f534]) ).
fof(f563,plain,
( sQ16_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f557,f424]) ).
fof(f564,plain,
sQ16_spl,
inference(contradiction_clause,[status(thm)],[f563]) ).
fof(f565,plain,
( sQ17_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f561,f425]) ).
fof(f566,plain,
sQ17_spl,
inference(contradiction_clause,[status(thm)],[f565]) ).
fof(f567,plain,
( sQ14_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f544,f426]) ).
fof(f568,plain,
sQ14_spl,
inference(contradiction_clause,[status(thm)],[f567]) ).
fof(f609,plain,
! [X0] :
( ~ memberP(app(app(sK53_skl,cons(sK51_skl,nil)),cons(sK52_skl,nil)),X0)
| memberP(sK49_skl,X0)
| ~ ssList(sK54_skl)
| ~ ssList(app(app(sK53_skl,cons(sK51_skl,nil)),cons(sK52_skl,nil)))
| ~ ssItem(X0) ),
inference(paramodulation,[status(thm)],[f466,f271]) ).
fof(f610,definition,
! [X0] :
( sQ25_spl
<=> ( ~ memberP(app(app(sK53_skl,cons(sK51_skl,nil)),cons(sK52_skl,nil)),X0)
| memberP(sK49_skl,X0)
| ~ ssItem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f611,plain,
! [X0] :
( ~ sQ25_spl
| ~ memberP(app(app(sK53_skl,cons(sK51_skl,nil)),cons(sK52_skl,nil)),X0)
| memberP(sK49_skl,X0)
| ~ ssItem(X0) ),
inference(component_clause,[status(thm)],[f610]) ).
fof(f613,plain,
( ~ sQ1_spl
| ~ sQ0_spl
| sQ25_spl ),
inference(split_clause,[status(thm)],[f609,f610,f468,f471]) ).
fof(f642,plain,
! [X0] :
( ~ sQ25_spl
| ~ memberP(app(sK53_skl,cons(sK51_skl,nil)),X0)
| ~ ssList(cons(sK52_skl,nil))
| ~ ssList(app(sK53_skl,cons(sK51_skl,nil)))
| ~ ssItem(X0)
| memberP(sK49_skl,X0)
| ~ ssItem(X0) ),
inference(resolution,[status(thm)],[f611,f271]) ).
fof(f643,definition,
! [X0] :
( sQ31_spl
<=> ( ~ memberP(app(sK53_skl,cons(sK51_skl,nil)),X0)
| ~ ssItem(X0)
| memberP(sK49_skl,X0)
| ~ ssItem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f644,plain,
! [X0] :
( ~ sQ31_spl
| ~ memberP(app(sK53_skl,cons(sK51_skl,nil)),X0)
| ~ ssItem(X0)
| memberP(sK49_skl,X0)
| ~ ssItem(X0) ),
inference(component_clause,[status(thm)],[f643]) ).
fof(f646,plain,
( ~ sQ25_spl
| ~ sQ13_spl
| ~ sQ12_spl
| sQ31_spl ),
inference(split_clause,[status(thm)],[f642,f643,f531,f534,f610]) ).
fof(f647,plain,
! [X0] :
( ~ sQ31_spl
| ~ memberP(app(sK53_skl,cons(sK51_skl,nil)),X0)
| memberP(sK49_skl,X0)
| ~ ssItem(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f644]) ).
fof(f707,plain,
! [X0] :
( ~ sQ31_spl
| memberP(sK49_skl,X0)
| ~ ssItem(X0)
| ~ memberP(cons(sK51_skl,nil),X0)
| ~ ssList(cons(sK51_skl,nil))
| ~ ssList(sK53_skl)
| ~ ssItem(X0) ),
inference(resolution,[status(thm)],[f272,f647]) ).
fof(f708,plain,
! [X0] :
( ~ sQ25_spl
| memberP(sK49_skl,X0)
| ~ ssItem(X0)
| ~ memberP(cons(sK52_skl,nil),X0)
| ~ ssList(cons(sK52_skl,nil))
| ~ ssList(app(sK53_skl,cons(sK51_skl,nil)))
| ~ ssItem(X0) ),
inference(resolution,[status(thm)],[f272,f611]) ).
fof(f711,definition,
! [X0] :
( sQ39_spl
<=> ( memberP(sK49_skl,X0)
| ~ ssItem(X0)
| ~ memberP(cons(sK51_skl,nil),X0)
| ~ ssItem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f712,plain,
! [X0] :
( ~ sQ39_spl
| memberP(sK49_skl,X0)
| ~ ssItem(X0)
| ~ memberP(cons(sK51_skl,nil),X0)
| ~ ssItem(X0) ),
inference(component_clause,[status(thm)],[f711]) ).
fof(f714,plain,
( ~ sQ31_spl
| ~ sQ15_spl
| ~ sQ14_spl
| sQ39_spl ),
inference(split_clause,[status(thm)],[f707,f711,f542,f545,f643]) ).
fof(f715,definition,
! [X0] :
( sQ40_spl
<=> ( memberP(sK49_skl,X0)
| ~ ssItem(X0)
| ~ memberP(cons(sK52_skl,nil),X0)
| ~ ssItem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f716,plain,
! [X0] :
( ~ sQ40_spl
| memberP(sK49_skl,X0)
| ~ ssItem(X0)
| ~ memberP(cons(sK52_skl,nil),X0)
| ~ ssItem(X0) ),
inference(component_clause,[status(thm)],[f715]) ).
fof(f718,plain,
( ~ sQ25_spl
| ~ sQ13_spl
| ~ sQ12_spl
| sQ40_spl ),
inference(split_clause,[status(thm)],[f708,f715,f531,f534,f610]) ).
fof(f723,plain,
! [X0] :
( ~ sQ39_spl
| memberP(sK49_skl,X0)
| ~ memberP(cons(sK51_skl,nil),X0)
| ~ ssItem(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f712]) ).
fof(f724,plain,
! [X0] :
( ~ sQ40_spl
| memberP(sK49_skl,X0)
| ~ memberP(cons(sK52_skl,nil),X0)
| ~ ssItem(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f716]) ).
fof(f725,plain,
( ~ sQ39_spl
| ~ ssList(nil)
| ~ ssItem(sK51_skl)
| memberP(sK49_skl,sK51_skl)
| ~ ssItem(sK51_skl) ),
inference(resolution,[status(thm)],[f723,f450]) ).
fof(f726,definition,
( sQ42_spl
<=> memberP(sK49_skl,sK51_skl) ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f727,plain,
( ~ sQ42_spl
| memberP(sK49_skl,sK51_skl) ),
inference(component_clause,[status(thm)],[f726]) ).
fof(f729,plain,
( ~ sQ39_spl
| ~ sQ9_spl
| sQ42_spl
| ~ sQ16_spl ),
inference(split_clause,[status(thm)],[f725,f555,f726,f514,f711]) ).
fof(f730,plain,
( ~ sQ42_spl
| sK55_skl = sK51_skl
| ~ ssItem(sK51_skl) ),
inference(resolution,[status(thm)],[f727,f431]) ).
fof(f731,definition,
( sQ43_spl
<=> sK55_skl = sK51_skl ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f732,plain,
( ~ sQ43_spl
| sK55_skl = sK51_skl ),
inference(component_clause,[status(thm)],[f731]) ).
fof(f734,plain,
( ~ sQ42_spl
| sQ43_spl
| ~ sQ16_spl ),
inference(split_clause,[status(thm)],[f730,f555,f731,f726]) ).
fof(f753,plain,
( ~ sQ43_spl
| sK55_skl != sK52_skl ),
inference(backward_demodulation,[status(thm)],[f732,f429]) ).
fof(f756,definition,
( sQ45_spl
<=> ssItem(sK55_skl) ),
introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition]) ).
fof(f758,plain,
( sQ45_spl
| ~ ssItem(sK55_skl) ),
inference(component_clause,[status(thm)],[f756]) ).
fof(f763,plain,
( sQ45_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f758,f430]) ).
fof(f764,plain,
sQ45_spl,
inference(contradiction_clause,[status(thm)],[f763]) ).
fof(f785,plain,
( ~ sQ40_spl
| ~ ssList(nil)
| ~ ssItem(sK52_skl)
| memberP(sK49_skl,sK52_skl)
| ~ ssItem(sK52_skl) ),
inference(resolution,[status(thm)],[f724,f450]) ).
fof(f787,definition,
( sQ49_spl
<=> memberP(sK49_skl,sK52_skl) ),
introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition]) ).
fof(f788,plain,
( ~ sQ49_spl
| memberP(sK49_skl,sK52_skl) ),
inference(component_clause,[status(thm)],[f787]) ).
fof(f790,plain,
( ~ sQ40_spl
| ~ sQ9_spl
| sQ49_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f785,f559,f787,f514,f715]) ).
fof(f791,plain,
( ~ sQ49_spl
| sK55_skl = sK52_skl
| ~ ssItem(sK52_skl) ),
inference(resolution,[status(thm)],[f788,f431]) ).
fof(f792,definition,
( sQ50_spl
<=> sK55_skl = sK52_skl ),
introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition]) ).
fof(f793,plain,
( ~ sQ50_spl
| sK55_skl = sK52_skl ),
inference(component_clause,[status(thm)],[f792]) ).
fof(f795,plain,
( ~ sQ49_spl
| sQ50_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f791,f559,f792,f787]) ).
fof(f796,plain,
( ~ sQ50_spl
| ~ sQ43_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f793,f753]) ).
fof(f797,plain,
( ~ sQ50_spl
| ~ sQ43_spl ),
inference(contradiction_clause,[status(thm)],[f796]) ).
fof(f798,plain,
$false,
inference(sat_refutation,[status(thm)],[f527,f537,f540,f548,f558,f562,f564,f566,f568,f613,f646,f714,f718,f729,f734,f764,f790,f795,f797]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWC190+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.36 % Computer : n001.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 08:08:44 UTC 2026
% 0.02/0.36 % CPUTime :
% 0.02/0.38 % Drodi V4.1.1
% 0.02/0.42 % Refutation found
% 0.02/0.42 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.02/0.42 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.02/0.45 % Elapsed time: 0.071945 seconds
% 0.02/0.45 % CPU time: 0.245821 seconds
% 0.02/0.45 % Total memory used: 112.156 MB
% 0.02/0.45 % Net memory used: 111.852 MB
%------------------------------------------------------------------------------