%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWX035+1 : TPTP v9.3.1. Released v9.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n019.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 03:13:12 PM UTC 2026
% Result : Theorem 166.58s 24.58s
% Output : CNFRefutation 166.58s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 21
% Syntax : Number of formulae : 101 ( 19 unt; 14 def)
% Number of atoms : 261 ( 69 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 280 ( 120 ~; 102 |; 32 &)
% ( 20 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 19 ( 17 usr; 14 prp; 0-5 aty)
% Number of functors : 9 ( 9 usr; 3 con; 0-3 aty)
% Number of variables : 149 ( 139 !; 10 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [Xx3] : '0' != s(Xx3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [Xx4,Xx5] :
( s(Xx4) = s(Xx5)
=> Xx4 = Xx5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [Xx1,Xx2,Xx3] :
( times_succeeds(Xx1,Xx2,Xx3)
<=> ( ( Xx3 = '0'
& Xx1 = '0' )
| ? [Xx4,Xx5] :
( plus_succeeds(Xx2,Xx5,Xx3)
& times_succeeds(Xx4,Xx2,Xx5)
& Xx1 = s(Xx4) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f30,axiom,
! [Xx,Xy,Xz] :
( nat_succeeds(Xx)
=> ( '@+'(Xx,Xy) = Xz
<=> plus_succeeds(Xx,Xy,Xz) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f31,axiom,
! [Xx,Xy,Xz] :
( ( nat_succeeds(Xy)
& nat_succeeds(Xx) )
=> ( '@*'(Xx,Xy) = Xz
<=> times_succeeds(Xx,Xy,Xz) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f53,axiom,
! [Xx,Xy,Xz] :
( times_succeeds(Xx,Xy,Xz)
=> nat_succeeds(Xx) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f62,conjecture,
! [Xx,Xy] :
( ( nat_succeeds(Xy)
& nat_succeeds(Xx) )
=> '@*'(s(Xx),Xy) = '@+'(Xy,'@*'(Xx,Xy)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f63,negated_conjecture,
~ ! [Xx,Xy] :
( ( nat_succeeds(Xy)
& nat_succeeds(Xx) )
=> '@*'(s(Xx),Xy) = '@+'(Xy,'@*'(Xx,Xy)) ),
inference(negated_conjecture,[status(cth)],[f62]) ).
fof(f64,plain,
! [X0] : '0' != s(X0),
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f65,plain,
! [Xx4,Xx5] :
( Xx4 = Xx5
| s(Xx4) != s(Xx5) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f66,plain,
! [X0,X1] :
( X0 = X1
| s(X0) != s(X1) ),
inference(cnf_transformation,[status(thm)],[f65]) ).
fof(f92,definition,
! [Xx1,Xx2,Xx3,Xx4,Xx5] :
( sP0_prd(Xx5,Xx4,Xx3,Xx2,Xx1)
<=> ( plus_succeeds(Xx2,Xx5,Xx3)
& times_succeeds(Xx4,Xx2,Xx5)
& Xx1 = s(Xx4) ) ),
introduced(definition,[new_symbols(definition,[sP0_prd])],[]) ).
fof(f93,plain,
! [Xx1,Xx2,Xx3] :
( times_succeeds(Xx1,Xx2,Xx3)
<=> ( ( Xx3 = '0'
& Xx1 = '0' )
| ? [Xx4,Xx5] : sP0_prd(Xx5,Xx4,Xx3,Xx2,Xx1) ) ),
inference(formula_renaming,[status(thm)],[f15,f92]) ).
fof(f94,plain,
! [Xx1,Xx2,Xx3] :
( ( ( ( Xx3 != '0'
| Xx1 != '0' )
& ! [Xx4,Xx5] : ~ sP0_prd(Xx5,Xx4,Xx3,Xx2,Xx1) )
| times_succeeds(Xx1,Xx2,Xx3) )
& ( ( Xx3 = '0'
& Xx1 = '0' )
| ? [Xx4,Xx5] : sP0_prd(Xx5,Xx4,Xx3,Xx2,Xx1)
| ~ times_succeeds(Xx1,Xx2,Xx3) ) ),
inference(NNF_transformation,[status(thm)],[f93]) ).
fof(f95,plain,
( ! [Xx1,Xx2,Xx3] :
( ( ( Xx3 != '0'
| Xx1 != '0' )
& ! [Xx4,Xx5] : ~ sP0_prd(Xx5,Xx4,Xx3,Xx2,Xx1) )
| times_succeeds(Xx1,Xx2,Xx3) )
& ! [Xx1,Xx2,Xx3] :
( ( Xx3 = '0'
& Xx1 = '0' )
| ? [Xx4,Xx5] : sP0_prd(Xx5,Xx4,Xx3,Xx2,Xx1)
| ~ times_succeeds(Xx1,Xx2,Xx3) ) ),
inference(miniscoping,[status(thm)],[f94]) ).
fof(f96,plain,
( ! [Xx1,Xx2,Xx3] :
( ( ( Xx3 != '0'
| Xx1 != '0' )
& ! [Xx4,Xx5] : ~ sP0_prd(Xx5,Xx4,Xx3,Xx2,Xx1) )
| times_succeeds(Xx1,Xx2,Xx3) )
& ! [Xx1,Xx2,Xx3] :
( ( Xx3 = '0'
& Xx1 = '0' )
| sP0_prd(sK1_skl(Xx3,Xx2,Xx1),sK0_skl(Xx3,Xx2,Xx1),Xx3,Xx2,Xx1)
| ~ times_succeeds(Xx1,Xx2,Xx3) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(Xx4,sK0_skl(Xx3,Xx2,Xx1)),skolemize(Xx5,sK1_skl(Xx3,Xx2,Xx1))],[f95]) ).
fof(f99,plain,
! [X0,X1,X2,X3,X4] :
( ~ sP0_prd(X3,X4,X2,X1,X0)
| times_succeeds(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f96]) ).
fof(f100,plain,
! [X0,X1,X2] :
( X2 != '0'
| X0 != '0'
| times_succeeds(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f96]) ).
fof(f216,plain,
! [Xx,Xy,Xz] :
( ( '@+'(Xx,Xy) = Xz
<=> plus_succeeds(Xx,Xy,Xz) )
| ~ nat_succeeds(Xx) ),
inference(pre_NNF_transformation,[status(thm)],[f30]) ).
fof(f217,plain,
! [Xx,Xy,Xz] :
( ( ( ~ plus_succeeds(Xx,Xy,Xz)
| '@+'(Xx,Xy) = Xz )
& ( plus_succeeds(Xx,Xy,Xz)
| '@+'(Xx,Xy) != Xz ) )
| ~ nat_succeeds(Xx) ),
inference(NNF_transformation,[status(thm)],[f216]) ).
fof(f218,plain,
! [Xx] :
( ( ! [Xy,Xz] :
( ~ plus_succeeds(Xx,Xy,Xz)
| '@+'(Xx,Xy) = Xz )
& ! [Xy,Xz] :
( plus_succeeds(Xx,Xy,Xz)
| '@+'(Xx,Xy) != Xz ) )
| ~ nat_succeeds(Xx) ),
inference(miniscoping,[status(thm)],[f217]) ).
fof(f219,plain,
! [X0,X1,X2] :
( plus_succeeds(X0,X1,X2)
| '@+'(X0,X1) != X2
| ~ nat_succeeds(X0) ),
inference(cnf_transformation,[status(thm)],[f218]) ).
fof(f221,plain,
! [Xx,Xy,Xz] :
( ( '@*'(Xx,Xy) = Xz
<=> times_succeeds(Xx,Xy,Xz) )
| ~ nat_succeeds(Xy)
| ~ nat_succeeds(Xx) ),
inference(pre_NNF_transformation,[status(thm)],[f31]) ).
fof(f222,plain,
! [Xx,Xy,Xz] :
( ( ( ~ times_succeeds(Xx,Xy,Xz)
| '@*'(Xx,Xy) = Xz )
& ( times_succeeds(Xx,Xy,Xz)
| '@*'(Xx,Xy) != Xz ) )
| ~ nat_succeeds(Xy)
| ~ nat_succeeds(Xx) ),
inference(NNF_transformation,[status(thm)],[f221]) ).
fof(f223,plain,
! [Xx,Xy] :
( ( ! [Xz] :
( ~ times_succeeds(Xx,Xy,Xz)
| '@*'(Xx,Xy) = Xz )
& ! [Xz] :
( times_succeeds(Xx,Xy,Xz)
| '@*'(Xx,Xy) != Xz ) )
| ~ nat_succeeds(Xy)
| ~ nat_succeeds(Xx) ),
inference(miniscoping,[status(thm)],[f222]) ).
fof(f224,plain,
! [X0,X1,X2] :
( times_succeeds(X0,X1,X2)
| '@*'(X0,X1) != X2
| ~ nat_succeeds(X1)
| ~ nat_succeeds(X0) ),
inference(cnf_transformation,[status(thm)],[f223]) ).
fof(f225,plain,
! [X0,X1,X2] :
( ~ times_succeeds(X0,X1,X2)
| '@*'(X0,X1) = X2
| ~ nat_succeeds(X1)
| ~ nat_succeeds(X0) ),
inference(cnf_transformation,[status(thm)],[f223]) ).
fof(f280,plain,
! [Xx,Xy,Xz] :
( nat_succeeds(Xx)
| ~ times_succeeds(Xx,Xy,Xz) ),
inference(pre_NNF_transformation,[status(thm)],[f53]) ).
fof(f281,plain,
! [Xx] :
( nat_succeeds(Xx)
| ! [Xy,Xz] : ~ times_succeeds(Xx,Xy,Xz) ),
inference(miniscoping,[status(thm)],[f280]) ).
fof(f282,plain,
! [X0,X1,X2] :
( nat_succeeds(X0)
| ~ times_succeeds(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f281]) ).
fof(f310,plain,
? [Xx,Xy] :
( '@*'(s(Xx),Xy) != '@+'(Xy,'@*'(Xx,Xy))
& nat_succeeds(Xy)
& nat_succeeds(Xx) ),
inference(pre_NNF_transformation,[status(thm)],[f63]) ).
fof(f311,plain,
( '@*'(s(sK35_skl),sK36_skl) != '@+'(sK36_skl,'@*'(sK35_skl,sK36_skl))
& nat_succeeds(sK36_skl)
& nat_succeeds(sK35_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK35_skl,sK36_skl]),skolemize(Xx,sK35_skl),skolemize(Xy,sK36_skl)],[f310]) ).
fof(f312,plain,
nat_succeeds(sK35_skl),
inference(cnf_transformation,[status(thm)],[f311]) ).
fof(f313,plain,
nat_succeeds(sK36_skl),
inference(cnf_transformation,[status(thm)],[f311]) ).
fof(f314,plain,
'@*'(s(sK35_skl),sK36_skl) != '@+'(sK36_skl,'@*'(sK35_skl,sK36_skl)),
inference(cnf_transformation,[status(thm)],[f311]) ).
fof(f315,plain,
! [Xx1,Xx2,Xx3,Xx4,Xx5] :
( ( ~ plus_succeeds(Xx2,Xx5,Xx3)
| ~ times_succeeds(Xx4,Xx2,Xx5)
| Xx1 != s(Xx4)
| sP0_prd(Xx5,Xx4,Xx3,Xx2,Xx1) )
& ( ( plus_succeeds(Xx2,Xx5,Xx3)
& times_succeeds(Xx4,Xx2,Xx5)
& Xx1 = s(Xx4) )
| ~ sP0_prd(Xx5,Xx4,Xx3,Xx2,Xx1) ) ),
inference(NNF_transformation,[status(thm)],[f92]) ).
fof(f316,plain,
( ! [Xx1,Xx2,Xx3,Xx4,Xx5] :
( ~ plus_succeeds(Xx2,Xx5,Xx3)
| ~ times_succeeds(Xx4,Xx2,Xx5)
| Xx1 != s(Xx4)
| sP0_prd(Xx5,Xx4,Xx3,Xx2,Xx1) )
& ! [Xx1,Xx2,Xx3,Xx4,Xx5] :
( ( plus_succeeds(Xx2,Xx5,Xx3)
& times_succeeds(Xx4,Xx2,Xx5)
& Xx1 = s(Xx4) )
| ~ sP0_prd(Xx5,Xx4,Xx3,Xx2,Xx1) ) ),
inference(miniscoping,[status(thm)],[f315]) ).
fof(f320,plain,
! [X0,X1,X2,X3,X4] :
( ~ plus_succeeds(X3,X0,X2)
| ~ times_succeeds(X1,X3,X0)
| X4 != s(X1)
| sP0_prd(X0,X1,X2,X3,X4) ),
inference(cnf_transformation,[status(thm)],[f316]) ).
fof(f377,plain,
! [X0] : times_succeeds('0',X0,'0'),
inference(destructive_equality_resolution,[status(thm)],[f100]) ).
fof(f397,plain,
! [X0,X1] :
( plus_succeeds(X0,X1,'@+'(X0,X1))
| ~ nat_succeeds(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f219]) ).
fof(f398,plain,
! [X0,X1] :
( times_succeeds(X0,X1,'@*'(X0,X1))
| ~ nat_succeeds(X1)
| ~ nat_succeeds(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f224]) ).
fof(f399,plain,
! [X0,X1,X2,X3] :
( ~ plus_succeeds(X3,X0,X2)
| ~ times_succeeds(X1,X3,X0)
| sP0_prd(X0,X1,X2,X3,s(X1)) ),
inference(destructive_equality_resolution,[status(thm)],[f320]) ).
fof(f413,plain,
s('@*'(s(sK35_skl),sK36_skl)) != s('@+'(sK36_skl,'@*'(sK35_skl,sK36_skl))),
inference(resolution,[status(thm)],[f66,f314]) ).
fof(f3624,definition,
( sQ82_spl
<=> nat_succeeds(sK35_skl) ),
introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition]) ).
fof(f3626,plain,
( sQ82_spl
| ~ nat_succeeds(sK35_skl) ),
inference(component_clause,[status(thm)],[f3624]) ).
fof(f3659,definition,
( sQ91_spl
<=> nat_succeeds(sK36_skl) ),
introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition]) ).
fof(f3661,plain,
( sQ91_spl
| ~ nat_succeeds(sK36_skl) ),
inference(component_clause,[status(thm)],[f3659]) ).
fof(f3882,plain,
( sQ91_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3661,f313]) ).
fof(f3883,plain,
sQ91_spl,
inference(contradiction_clause,[status(thm)],[f3882]) ).
fof(f3884,plain,
( sQ82_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3626,f312]) ).
fof(f3885,plain,
sQ82_spl,
inference(contradiction_clause,[status(thm)],[f3884]) ).
fof(f3887,definition,
( sQ147_spl
<=> times_succeeds(s(sK35_skl),sK36_skl,'@+'(sK36_skl,'@*'(sK35_skl,sK36_skl))) ),
introduced(definition,[new_symbols(definition,[sQ147_spl])],[split_symbol_definition]) ).
fof(f3889,plain,
( sQ147_spl
| ~ times_succeeds(s(sK35_skl),sK36_skl,'@+'(sK36_skl,'@*'(sK35_skl,sK36_skl))) ),
inference(component_clause,[status(thm)],[f3887]) ).
fof(f3972,plain,
! [X0,X1] :
( sQ147_spl
| ~ sP0_prd(X0,X1,'@+'(sK36_skl,'@*'(sK35_skl,sK36_skl)),sK36_skl,s(sK35_skl)) ),
inference(resolution,[status(thm)],[f3889,f99]) ).
fof(f6333,definition,
( sQ166_spl
<=> s('0') = '0' ),
introduced(definition,[new_symbols(definition,[sQ166_spl])],[split_symbol_definition]) ).
fof(f6334,plain,
( ~ sQ166_spl
| s('0') = '0' ),
inference(component_clause,[status(thm)],[f6333]) ).
fof(f6341,plain,
( ~ sQ166_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6334,f64]) ).
fof(f6342,plain,
~ sQ166_spl,
inference(contradiction_clause,[status(thm)],[f6341]) ).
fof(f6343,plain,
! [X0,X1,X2] :
( ~ times_succeeds(X1,X0,X2)
| '@*'(X1,X0) = X2
| ~ nat_succeeds(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f225,f282]) ).
fof(f8351,definition,
( sQ170_spl
<=> s('@+'(sK36_skl,'@*'(sK35_skl,sK36_skl))) = s('@*'(s(sK35_skl),sK36_skl)) ),
introduced(definition,[new_symbols(definition,[sQ170_spl])],[split_symbol_definition]) ).
fof(f8352,plain,
( ~ sQ170_spl
| s('@+'(sK36_skl,'@*'(sK35_skl,sK36_skl))) = s('@*'(s(sK35_skl),sK36_skl)) ),
inference(component_clause,[status(thm)],[f8351]) ).
fof(f8361,definition,
( sQ172_spl
<=> '@+'(sK36_skl,'@*'(sK35_skl,sK36_skl)) = '@*'(s(sK35_skl),sK36_skl) ),
introduced(definition,[new_symbols(definition,[sQ172_spl])],[split_symbol_definition]) ).
fof(f8362,plain,
( ~ sQ172_spl
| '@+'(sK36_skl,'@*'(sK35_skl,sK36_skl)) = '@*'(s(sK35_skl),sK36_skl) ),
inference(component_clause,[status(thm)],[f8361]) ).
fof(f10100,definition,
( sQ177_spl
<=> s(s('0')) = '0' ),
introduced(definition,[new_symbols(definition,[sQ177_spl])],[split_symbol_definition]) ).
fof(f10101,plain,
( ~ sQ177_spl
| s(s('0')) = '0' ),
inference(component_clause,[status(thm)],[f10100]) ).
fof(f10108,plain,
( ~ sQ177_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f10101,f64]) ).
fof(f10109,plain,
~ sQ177_spl,
inference(contradiction_clause,[status(thm)],[f10108]) ).
fof(f12209,definition,
( sQ200_spl
<=> s(s(s('0'))) = '0' ),
introduced(definition,[new_symbols(definition,[sQ200_spl])],[split_symbol_definition]) ).
fof(f12210,plain,
( ~ sQ200_spl
| s(s(s('0'))) = '0' ),
inference(component_clause,[status(thm)],[f12209]) ).
fof(f12217,plain,
( ~ sQ200_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f12210,f64]) ).
fof(f12218,plain,
~ sQ200_spl,
inference(contradiction_clause,[status(thm)],[f12217]) ).
fof(f12651,plain,
! [X0] :
( sQ147_spl
| ~ plus_succeeds(sK36_skl,X0,'@+'(sK36_skl,'@*'(sK35_skl,sK36_skl)))
| ~ times_succeeds(sK35_skl,sK36_skl,X0) ),
inference(resolution,[status(thm)],[f399,f3972]) ).
fof(f12663,definition,
! [X0] :
( sQ209_spl
<=> ~ times_succeeds(X0,sK36_skl,'0') ),
introduced(definition,[new_symbols(definition,[sQ209_spl])],[split_symbol_definition]) ).
fof(f12664,plain,
! [X0] :
( ~ sQ209_spl
| ~ times_succeeds(X0,sK36_skl,'0') ),
inference(component_clause,[status(thm)],[f12663]) ).
fof(f13361,definition,
( sQ226_spl
<=> s(sK28_skl(s('0'))) = '0' ),
introduced(definition,[new_symbols(definition,[sQ226_spl])],[split_symbol_definition]) ).
fof(f13362,plain,
( ~ sQ226_spl
| s(sK28_skl(s('0'))) = '0' ),
inference(component_clause,[status(thm)],[f13361]) ).
fof(f13369,plain,
( ~ sQ226_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f13362,f64]) ).
fof(f13370,plain,
~ sQ226_spl,
inference(contradiction_clause,[status(thm)],[f13369]) ).
fof(f13595,plain,
( ~ sQ172_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8362,f314]) ).
fof(f13596,plain,
~ sQ172_spl,
inference(contradiction_clause,[status(thm)],[f13595]) ).
fof(f13597,plain,
( ~ sQ170_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8352,f413]) ).
fof(f13598,plain,
~ sQ170_spl,
inference(contradiction_clause,[status(thm)],[f13597]) ).
fof(f14056,definition,
! [X0] :
( sQ232_spl
<=> ~ times_succeeds(X0,'0','0') ),
introduced(definition,[new_symbols(definition,[sQ232_spl])],[split_symbol_definition]) ).
fof(f14057,plain,
! [X0] :
( ~ sQ232_spl
| ~ times_succeeds(X0,'0','0') ),
inference(component_clause,[status(thm)],[f14056]) ).
fof(f14313,plain,
( ~ sQ209_spl
| $false ),
inference(resolution,[status(thm)],[f12664,f377]) ).
fof(f14316,plain,
~ sQ209_spl,
inference(contradiction_clause,[status(thm)],[f14313]) ).
fof(f14477,plain,
( ~ sQ232_spl
| $false ),
inference(resolution,[status(thm)],[f14057,f377]) ).
fof(f14480,plain,
~ sQ232_spl,
inference(contradiction_clause,[status(thm)],[f14477]) ).
fof(f14612,definition,
( sQ240_spl
<=> s(s(s(s('0')))) = '0' ),
introduced(definition,[new_symbols(definition,[sQ240_spl])],[split_symbol_definition]) ).
fof(f14613,plain,
( ~ sQ240_spl
| s(s(s(s('0')))) = '0' ),
inference(component_clause,[status(thm)],[f14612]) ).
fof(f14620,plain,
( ~ sQ240_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f14613,f64]) ).
fof(f14621,plain,
~ sQ240_spl,
inference(contradiction_clause,[status(thm)],[f14620]) ).
fof(f14649,plain,
( ~ times_succeeds(s(sK35_skl),sK36_skl,'@+'(sK36_skl,'@*'(sK35_skl,sK36_skl)))
| ~ nat_succeeds(sK36_skl) ),
inference(resolution,[status(thm)],[f6343,f314]) ).
fof(f14654,plain,
( ~ sQ147_spl
| ~ sQ91_spl ),
inference(split_clause,[status(thm)],[f14649,f3659,f3887]) ).
fof(f15145,plain,
( sQ147_spl
| ~ nat_succeeds(sK36_skl)
| ~ times_succeeds(sK35_skl,sK36_skl,'@*'(sK35_skl,sK36_skl)) ),
inference(resolution,[status(thm)],[f12651,f397]) ).
fof(f15149,definition,
( sQ257_spl
<=> times_succeeds(sK35_skl,sK36_skl,'@*'(sK35_skl,sK36_skl)) ),
introduced(definition,[new_symbols(definition,[sQ257_spl])],[split_symbol_definition]) ).
fof(f15151,plain,
( sQ257_spl
| ~ times_succeeds(sK35_skl,sK36_skl,'@*'(sK35_skl,sK36_skl)) ),
inference(component_clause,[status(thm)],[f15149]) ).
fof(f15152,plain,
( sQ147_spl
| ~ sQ91_spl
| ~ sQ257_spl ),
inference(split_clause,[status(thm)],[f15145,f15149,f3659,f3887]) ).
fof(f16652,plain,
( sQ257_spl
| ~ nat_succeeds(sK36_skl)
| ~ nat_succeeds(sK35_skl) ),
inference(resolution,[status(thm)],[f15151,f398]) ).
fof(f16655,plain,
( sQ257_spl
| ~ sQ91_spl
| ~ sQ82_spl ),
inference(split_clause,[status(thm)],[f16652,f3624,f3659,f15149]) ).
fof(f16656,plain,
$false,
inference(sat_refutation,[status(thm)],[f3883,f3885,f6342,f10109,f12218,f13370,f13596,f13598,f14316,f14480,f14621,f14654,f15152,f16655]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWX035+1 : TPTP v9.3.1. Released v9.1.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/0.40 % Computer : n019.cluster.edu
% 0.16/0.40 % Model : x86_64 x86_64
% 0.16/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.40 % Memory : 8046.5625MB
% 0.16/0.40 % OS : Linux 6.8.0-71-generic
% 0.16/0.40 % CPULimit : 300
% 0.16/0.40 % WCLimit : 300
% 0.16/0.40 % DateTime : Mon Sep 21 10:22:37 UTC 2026
% 0.16/0.41 % CPUTime :
% 0.20/0.43 % Drodi V4.1.1
% 166.58/24.58 % Refutation found
% 166.58/24.58 % SZS status Theorem for theBenchmark: Theorem is valid
% 166.58/24.58 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 17.92/24.75 % Elapsed time: 24.318793 seconds
% 17.92/24.75 % CPU time: 191.541439 seconds
% 17.92/24.75 % Total memory used: 596.201 MB
% 17.92/24.75 % Net memory used: 544.940 MB
%------------------------------------------------------------------------------