%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWX043+1 : TPTP v9.3.1. Released v9.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/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 03:13:13 PM UTC 2026
% Result : Theorem 34.07s 9.78s
% Output : CNFRefutation 15.33s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 34
% Syntax : Number of formulae : 159 ( 28 unt; 23 def)
% Number of atoms : 416 ( 97 equ)
% Maximal formula atoms : 10 ( 2 avg)
% Number of connectives : 439 ( 182 ~; 178 |; 41 &)
% ( 25 <=>; 13 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 28 ( 26 usr; 24 prp; 0-2 aty)
% Number of functors : 19 ( 19 usr; 8 con; 0-3 aty)
% Number of variables : 167 ( 147 !; 20 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [Xx3] : '0' != s(Xx3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f21,axiom,
! [Xx1,Xx2] :
( '@=<_succeeds'(Xx1,Xx2)
<=> ( Xx1 = '0'
| ? [Xx3,Xx4] :
( '@=<_succeeds'(Xx3,Xx4)
& Xx2 = s(Xx4)
& Xx1 = s(Xx3) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f27,axiom,
! [Xx1] :
( nat_succeeds(Xx1)
<=> ( Xx1 = '0'
| ? [Xx2] :
( nat_succeeds(Xx2)
& Xx1 = s(Xx2) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f45,axiom,
! [Xy] : '@+'('0',Xy) = Xy,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f46,axiom,
! [Xx,Xy] :
( nat_succeeds(Xx)
=> '@+'(s(Xx),Xy) = s('@+'(Xx,Xy)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f73,axiom,
! [Xx,Xy] :
( '@<_succeeds'(Xx,Xy)
=> nat_succeeds(Xx) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f74,axiom,
! [Xx,Xy] :
( '@<_succeeds'(Xx,Xy)
=> ? [Xz] : Xy = s(Xz) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f79,axiom,
! [Xx] :
( nat_succeeds(Xx)
=> ~ '@<_succeeds'(Xx,Xx) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f100,axiom,
! [Xx,Xy] :
( ( '@=<_succeeds'(Xy,Xx)
& '@=<_succeeds'(Xx,Xy) )
=> Xx = Xy ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f107,axiom,
( ! [Xx] :
( ( Xx = '0'
| ? [Xx2] :
( ! [Xy,Xz] :
( '@=<_succeeds'(Xy,Xz)
=> '@=<_succeeds'('@+'(Xx2,Xy),'@+'(Xx2,Xz)) )
& nat_succeeds(Xx2)
& Xx = s(Xx2) ) )
=> ! [Xy,Xz] :
( '@=<_succeeds'(Xy,Xz)
=> '@=<_succeeds'('@+'(Xx,Xy),'@+'(Xx,Xz)) ) )
=> ! [Xx] :
( nat_succeeds(Xx)
=> ! [Xy,Xz] :
( '@=<_succeeds'(Xy,Xz)
=> '@=<_succeeds'('@+'(Xx,Xy),'@+'(Xx,Xz)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f108,conjecture,
! [Xx,Xy,Xz] :
( ( '@=<_succeeds'(Xy,Xz)
& nat_succeeds(Xx) )
=> '@=<_succeeds'('@+'(Xx,Xy),'@+'(Xx,Xz)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f109,negated_conjecture,
~ ! [Xx,Xy,Xz] :
( ( '@=<_succeeds'(Xy,Xz)
& nat_succeeds(Xx) )
=> '@=<_succeeds'('@+'(Xx,Xy),'@+'(Xx,Xz)) ),
inference(negated_conjecture,[status(cth)],[f108]) ).
fof(f110,plain,
! [X0] : '0' != s(X0),
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f191,plain,
! [Xx1,Xx2] :
( ( ( Xx1 != '0'
& ! [Xx3,Xx4] :
( ~ '@=<_succeeds'(Xx3,Xx4)
| Xx2 != s(Xx4)
| Xx1 != s(Xx3) ) )
| '@=<_succeeds'(Xx1,Xx2) )
& ( Xx1 = '0'
| ? [Xx3,Xx4] :
( '@=<_succeeds'(Xx3,Xx4)
& Xx2 = s(Xx4)
& Xx1 = s(Xx3) )
| ~ '@=<_succeeds'(Xx1,Xx2) ) ),
inference(NNF_transformation,[status(thm)],[f21]) ).
fof(f192,plain,
( ! [Xx1,Xx2] :
( ( Xx1 != '0'
& ! [Xx3,Xx4] :
( ~ '@=<_succeeds'(Xx3,Xx4)
| Xx2 != s(Xx4)
| Xx1 != s(Xx3) ) )
| '@=<_succeeds'(Xx1,Xx2) )
& ! [Xx1,Xx2] :
( Xx1 = '0'
| ? [Xx3,Xx4] :
( '@=<_succeeds'(Xx3,Xx4)
& Xx2 = s(Xx4)
& Xx1 = s(Xx3) )
| ~ '@=<_succeeds'(Xx1,Xx2) ) ),
inference(miniscoping,[status(thm)],[f191]) ).
fof(f193,plain,
( ! [Xx1,Xx2] :
( ( Xx1 != '0'
& ! [Xx3,Xx4] :
( ~ '@=<_succeeds'(Xx3,Xx4)
| Xx2 != s(Xx4)
| Xx1 != s(Xx3) ) )
| '@=<_succeeds'(Xx1,Xx2) )
& ! [Xx1,Xx2] :
( Xx1 = '0'
| ( '@=<_succeeds'(sK13_skl(Xx2,Xx1),sK14_skl(Xx2,Xx1))
& Xx2 = s(sK14_skl(Xx2,Xx1))
& Xx1 = s(sK13_skl(Xx2,Xx1)) )
| ~ '@=<_succeeds'(Xx1,Xx2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13_skl,sK14_skl]),skolemize(Xx3,sK13_skl(Xx2,Xx1)),skolemize(Xx4,sK14_skl(Xx2,Xx1))],[f192]) ).
fof(f197,plain,
! [X0,X1,X2,X3] :
( ~ '@=<_succeeds'(X2,X3)
| X1 != s(X3)
| X0 != s(X2)
| '@=<_succeeds'(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f193]) ).
fof(f198,plain,
! [X0,X1] :
( X0 != '0'
| '@=<_succeeds'(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f193]) ).
fof(f241,plain,
! [Xx1] :
( ( ( Xx1 != '0'
& ! [Xx2] :
( ~ nat_succeeds(Xx2)
| Xx1 != s(Xx2) ) )
| nat_succeeds(Xx1) )
& ( Xx1 = '0'
| ? [Xx2] :
( nat_succeeds(Xx2)
& Xx1 = s(Xx2) )
| ~ nat_succeeds(Xx1) ) ),
inference(NNF_transformation,[status(thm)],[f27]) ).
fof(f242,plain,
( ! [Xx1] :
( ( Xx1 != '0'
& ! [Xx2] :
( ~ nat_succeeds(Xx2)
| Xx1 != s(Xx2) ) )
| nat_succeeds(Xx1) )
& ! [Xx1] :
( Xx1 = '0'
| ? [Xx2] :
( nat_succeeds(Xx2)
& Xx1 = s(Xx2) )
| ~ nat_succeeds(Xx1) ) ),
inference(miniscoping,[status(thm)],[f241]) ).
fof(f243,plain,
( ! [Xx1] :
( ( Xx1 != '0'
& ! [Xx2] :
( ~ nat_succeeds(Xx2)
| Xx1 != s(Xx2) ) )
| nat_succeeds(Xx1) )
& ! [Xx1] :
( Xx1 = '0'
| ( nat_succeeds(sK27_skl(Xx1))
& Xx1 = s(sK27_skl(Xx1)) )
| ~ nat_succeeds(Xx1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK27_skl]),skolemize(Xx2,sK27_skl(Xx1))],[f242]) ).
fof(f246,plain,
! [X0,X1] :
( ~ nat_succeeds(X1)
| X0 != s(X1)
| nat_succeeds(X0) ),
inference(cnf_transformation,[status(thm)],[f243]) ).
fof(f309,plain,
! [X0] : '@+'('0',X0) = X0,
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f310,plain,
! [Xx,Xy] :
( '@+'(s(Xx),Xy) = s('@+'(Xx,Xy))
| ~ nat_succeeds(Xx) ),
inference(pre_NNF_transformation,[status(thm)],[f46]) ).
fof(f311,plain,
! [Xx] :
( ! [Xy] : '@+'(s(Xx),Xy) = s('@+'(Xx,Xy))
| ~ nat_succeeds(Xx) ),
inference(miniscoping,[status(thm)],[f310]) ).
fof(f312,plain,
! [X0,X1] :
( '@+'(s(X0),X1) = s('@+'(X0,X1))
| ~ nat_succeeds(X0) ),
inference(cnf_transformation,[status(thm)],[f311]) ).
fof(f375,plain,
! [Xx,Xy] :
( nat_succeeds(Xx)
| ~ '@<_succeeds'(Xx,Xy) ),
inference(pre_NNF_transformation,[status(thm)],[f73]) ).
fof(f376,plain,
! [Xx] :
( nat_succeeds(Xx)
| ! [Xy] : ~ '@<_succeeds'(Xx,Xy) ),
inference(miniscoping,[status(thm)],[f375]) ).
fof(f377,plain,
! [X0,X1] :
( nat_succeeds(X0)
| ~ '@<_succeeds'(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f376]) ).
fof(f378,plain,
! [Xx,Xy] :
( ? [Xz] : Xy = s(Xz)
| ~ '@<_succeeds'(Xx,Xy) ),
inference(pre_NNF_transformation,[status(thm)],[f74]) ).
fof(f379,plain,
! [Xy] :
( ? [Xz] : Xy = s(Xz)
| ! [Xx] : ~ '@<_succeeds'(Xx,Xy) ),
inference(miniscoping,[status(thm)],[f378]) ).
fof(f380,plain,
! [Xy] :
( Xy = s(sK32_skl(Xy))
| ! [Xx] : ~ '@<_succeeds'(Xx,Xy) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK32_skl]),skolemize(Xz,sK32_skl(Xy))],[f379]) ).
fof(f381,plain,
! [X0,X1] :
( X1 = s(sK32_skl(X1))
| ~ '@<_succeeds'(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f380]) ).
fof(f392,plain,
! [Xx] :
( ~ '@<_succeeds'(Xx,Xx)
| ~ nat_succeeds(Xx) ),
inference(pre_NNF_transformation,[status(thm)],[f79]) ).
fof(f393,plain,
! [X0] :
( ~ '@<_succeeds'(X0,X0)
| ~ nat_succeeds(X0) ),
inference(cnf_transformation,[status(thm)],[f392]) ).
fof(f444,plain,
! [Xx,Xy] :
( Xx = Xy
| ~ '@=<_succeeds'(Xy,Xx)
| ~ '@=<_succeeds'(Xx,Xy) ),
inference(pre_NNF_transformation,[status(thm)],[f100]) ).
fof(f445,plain,
! [X0,X1] :
( X0 = X1
| ~ '@=<_succeeds'(X1,X0)
| ~ '@=<_succeeds'(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f444]) ).
fof(f459,plain,
( ! [Xx] :
( ! [Xy,Xz] :
( '@=<_succeeds'('@+'(Xx,Xy),'@+'(Xx,Xz))
| ~ '@=<_succeeds'(Xy,Xz) )
| ~ nat_succeeds(Xx) )
| ? [Xx] :
( ? [Xy,Xz] :
( ~ '@=<_succeeds'('@+'(Xx,Xy),'@+'(Xx,Xz))
& '@=<_succeeds'(Xy,Xz) )
& ( Xx = '0'
| ? [Xx2] :
( ! [Xy,Xz] :
( '@=<_succeeds'('@+'(Xx2,Xy),'@+'(Xx2,Xz))
| ~ '@=<_succeeds'(Xy,Xz) )
& nat_succeeds(Xx2)
& Xx = s(Xx2) ) ) ) ),
inference(pre_NNF_transformation,[status(thm)],[f107]) ).
fof(f460,plain,
( ! [Xx] :
( ! [Xy,Xz] :
( '@=<_succeeds'('@+'(Xx,Xy),'@+'(Xx,Xz))
| ~ '@=<_succeeds'(Xy,Xz) )
| ~ nat_succeeds(Xx) )
| ( ~ '@=<_succeeds'('@+'(sK37_skl,sK39_skl),'@+'(sK37_skl,sK40_skl))
& '@=<_succeeds'(sK39_skl,sK40_skl)
& ( sK37_skl = '0'
| ( ! [Xy,Xz] :
( '@=<_succeeds'('@+'(sK38_skl,Xy),'@+'(sK38_skl,Xz))
| ~ '@=<_succeeds'(Xy,Xz) )
& nat_succeeds(sK38_skl)
& sK37_skl = s(sK38_skl) ) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK37_skl,sK38_skl,sK39_skl,sK40_skl]),skolemize(Xx,sK37_skl),skolemize(Xx2,sK38_skl),skolemize(Xy,sK39_skl),skolemize(Xz,sK40_skl)],[f459]) ).
fof(f461,plain,
! [X0,X1,X2] :
( '@=<_succeeds'('@+'(X0,X1),'@+'(X0,X2))
| ~ '@=<_succeeds'(X1,X2)
| ~ nat_succeeds(X0)
| sK37_skl = '0'
| sK37_skl = s(sK38_skl) ),
inference(cnf_transformation,[status(thm)],[f460]) ).
fof(f462,plain,
! [X0,X1,X2] :
( '@=<_succeeds'('@+'(X0,X1),'@+'(X0,X2))
| ~ '@=<_succeeds'(X1,X2)
| ~ nat_succeeds(X0)
| sK37_skl = '0'
| nat_succeeds(sK38_skl) ),
inference(cnf_transformation,[status(thm)],[f460]) ).
fof(f463,plain,
! [X0,X1,X2,X3,X4] :
( '@=<_succeeds'('@+'(X2,X3),'@+'(X2,X4))
| ~ '@=<_succeeds'(X3,X4)
| ~ nat_succeeds(X2)
| sK37_skl = '0'
| '@=<_succeeds'('@+'(sK38_skl,X0),'@+'(sK38_skl,X1))
| ~ '@=<_succeeds'(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f460]) ).
fof(f464,plain,
! [X0,X1,X2] :
( '@=<_succeeds'('@+'(X0,X1),'@+'(X0,X2))
| ~ '@=<_succeeds'(X1,X2)
| ~ nat_succeeds(X0)
| '@=<_succeeds'(sK39_skl,sK40_skl) ),
inference(cnf_transformation,[status(thm)],[f460]) ).
fof(f465,plain,
! [X0,X1,X2] :
( '@=<_succeeds'('@+'(X0,X1),'@+'(X0,X2))
| ~ '@=<_succeeds'(X1,X2)
| ~ nat_succeeds(X0)
| ~ '@=<_succeeds'('@+'(sK37_skl,sK39_skl),'@+'(sK37_skl,sK40_skl)) ),
inference(cnf_transformation,[status(thm)],[f460]) ).
fof(f466,plain,
? [Xx,Xy,Xz] :
( ~ '@=<_succeeds'('@+'(Xx,Xy),'@+'(Xx,Xz))
& '@=<_succeeds'(Xy,Xz)
& nat_succeeds(Xx) ),
inference(pre_NNF_transformation,[status(thm)],[f109]) ).
fof(f467,plain,
( ~ '@=<_succeeds'('@+'(sK41_skl,sK42_skl),'@+'(sK41_skl,sK43_skl))
& '@=<_succeeds'(sK42_skl,sK43_skl)
& nat_succeeds(sK41_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK41_skl,sK42_skl,sK43_skl]),skolemize(Xx,sK41_skl),skolemize(Xy,sK42_skl),skolemize(Xz,sK43_skl)],[f466]) ).
fof(f468,plain,
nat_succeeds(sK41_skl),
inference(cnf_transformation,[status(thm)],[f467]) ).
fof(f469,plain,
'@=<_succeeds'(sK42_skl,sK43_skl),
inference(cnf_transformation,[status(thm)],[f467]) ).
fof(f470,plain,
~ '@=<_succeeds'('@+'(sK41_skl,sK42_skl),'@+'(sK41_skl,sK43_skl)),
inference(cnf_transformation,[status(thm)],[f467]) ).
fof(f507,definition,
( sQ0_spl
<=> sK37_skl = s(sK38_skl) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f508,plain,
( ~ sQ0_spl
| sK37_skl = s(sK38_skl) ),
inference(component_clause,[status(thm)],[f507]) ).
fof(f510,definition,
( sQ1_spl
<=> sK37_skl = '0' ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f511,plain,
( ~ sQ1_spl
| sK37_skl = '0' ),
inference(component_clause,[status(thm)],[f510]) ).
fof(f513,definition,
! [X0,X1,X2] :
( sQ2_spl
<=> ( '@=<_succeeds'('@+'(X0,X1),'@+'(X0,X2))
| ~ '@=<_succeeds'(X1,X2)
| ~ nat_succeeds(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f514,plain,
! [X0,X1,X2] :
( ~ sQ2_spl
| '@=<_succeeds'('@+'(X0,X1),'@+'(X0,X2))
| ~ '@=<_succeeds'(X1,X2)
| ~ nat_succeeds(X0) ),
inference(component_clause,[status(thm)],[f513]) ).
fof(f516,plain,
( sQ2_spl
| sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f461,f507,f510,f513]) ).
fof(f517,definition,
( sQ3_spl
<=> nat_succeeds(sK38_skl) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f518,plain,
( ~ sQ3_spl
| nat_succeeds(sK38_skl) ),
inference(component_clause,[status(thm)],[f517]) ).
fof(f520,plain,
( sQ2_spl
| sQ1_spl
| sQ3_spl ),
inference(split_clause,[status(thm)],[f462,f517,f510,f513]) ).
fof(f521,definition,
! [X0,X1] :
( sQ4_spl
<=> ( '@=<_succeeds'('@+'(sK38_skl,X0),'@+'(sK38_skl,X1))
| ~ '@=<_succeeds'(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f522,plain,
! [X0,X1] :
( ~ sQ4_spl
| '@=<_succeeds'('@+'(sK38_skl,X0),'@+'(sK38_skl,X1))
| ~ '@=<_succeeds'(X0,X1) ),
inference(component_clause,[status(thm)],[f521]) ).
fof(f524,plain,
( sQ2_spl
| sQ1_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f463,f521,f510,f513]) ).
fof(f525,definition,
( sQ5_spl
<=> '@=<_succeeds'(sK39_skl,sK40_skl) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f526,plain,
( ~ sQ5_spl
| '@=<_succeeds'(sK39_skl,sK40_skl) ),
inference(component_clause,[status(thm)],[f525]) ).
fof(f528,plain,
( sQ2_spl
| sQ5_spl ),
inference(split_clause,[status(thm)],[f464,f525,f513]) ).
fof(f529,definition,
( sQ6_spl
<=> '@=<_succeeds'('@+'(sK37_skl,sK39_skl),'@+'(sK37_skl,sK40_skl)) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f531,plain,
( sQ6_spl
| ~ '@=<_succeeds'('@+'(sK37_skl,sK39_skl),'@+'(sK37_skl,sK40_skl)) ),
inference(component_clause,[status(thm)],[f529]) ).
fof(f532,plain,
( sQ2_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f465,f529,f513]) ).
fof(f540,plain,
! [X0,X1] :
( ~ '@=<_succeeds'(X0,X1)
| '@=<_succeeds'(s(X0),s(X1)) ),
inference(destructive_equality_resolution,[status(thm)],[f197]) ).
fof(f541,plain,
! [X0] : '@=<_succeeds'('0',X0),
inference(destructive_equality_resolution,[status(thm)],[f198]) ).
fof(f548,plain,
! [X0] :
( ~ nat_succeeds(X0)
| nat_succeeds(s(X0)) ),
inference(destructive_equality_resolution,[status(thm)],[f246]) ).
fof(f640,plain,
! [X0] :
( '0' = X0
| ~ '@=<_succeeds'(X0,'0') ),
inference(resolution,[status(thm)],[f445,f541]) ).
fof(f1007,definition,
( sQ43_spl
<=> nat_succeeds(s(sK41_skl)) ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f1009,plain,
( sQ43_spl
| ~ nat_succeeds(s(sK41_skl)) ),
inference(component_clause,[status(thm)],[f1007]) ).
fof(f1197,plain,
! [X0] :
( ~ sQ1_spl
| '@=<_succeeds'(sK37_skl,X0) ),
inference(backward_demodulation,[status(thm)],[f511,f541]) ).
fof(f2056,plain,
! [X0] : ~ '@<_succeeds'(X0,X0),
inference(forward_subsumption_resolution,[status(thm)],[f393,f377]) ).
fof(f2578,plain,
( ~ sQ1_spl
| '0' = sK37_skl ),
inference(resolution,[status(thm)],[f1197,f640]) ).
fof(f3031,plain,
! [X0,X1] :
( ~ sQ2_spl
| '@=<_succeeds'('@+'(sK41_skl,X0),'@+'(sK41_skl,X1))
| ~ '@=<_succeeds'(X0,X1) ),
inference(resolution,[status(thm)],[f468,f514]) ).
fof(f3055,plain,
nat_succeeds(s(sK41_skl)),
inference(resolution,[status(thm)],[f468,f548]) ).
fof(f3173,definition,
! [X0] :
( sQ126_spl
<=> '0' = s(sK13_skl(X0,'0')) ),
introduced(definition,[new_symbols(definition,[sQ126_spl])],[split_symbol_definition]) ).
fof(f3174,plain,
! [X0] :
( ~ sQ126_spl
| '0' = s(sK13_skl(X0,'0')) ),
inference(component_clause,[status(thm)],[f3173]) ).
fof(f3187,definition,
! [X0] :
( sQ128_spl
<=> X0 = s(sK14_skl(X0,'0')) ),
introduced(definition,[new_symbols(definition,[sQ128_spl])],[split_symbol_definition]) ).
fof(f3188,plain,
! [X0] :
( ~ sQ128_spl
| X0 = s(sK14_skl(X0,'0')) ),
inference(component_clause,[status(thm)],[f3187]) ).
fof(f3534,definition,
( sQ149_spl
<=> '@<_succeeds'(sK41_skl,'0') ),
introduced(definition,[new_symbols(definition,[sQ149_spl])],[split_symbol_definition]) ).
fof(f3535,plain,
( ~ sQ149_spl
| '@<_succeeds'(sK41_skl,'0') ),
inference(component_clause,[status(thm)],[f3534]) ).
fof(f3664,plain,
! [X0] :
( ~ sQ1_spl
| '@+'(sK37_skl,X0) = X0 ),
inference(backward_demodulation,[status(thm)],[f2578,f309]) ).
fof(f5135,plain,
( ~ sQ2_spl
| '@=<_succeeds'('@+'(sK41_skl,sK42_skl),'@+'(sK41_skl,sK43_skl)) ),
inference(resolution,[status(thm)],[f3031,f469]) ).
fof(f5137,plain,
( ~ sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5135,f470]) ).
fof(f5138,plain,
~ sQ2_spl,
inference(contradiction_clause,[status(thm)],[f5137]) ).
fof(f5559,plain,
( ~ sQ4_spl
| ~ sQ5_spl
| '@=<_succeeds'('@+'(sK38_skl,sK39_skl),'@+'(sK38_skl,sK40_skl)) ),
inference(resolution,[status(thm)],[f526,f522]) ).
fof(f6666,definition,
( sQ225_spl
<=> '@<_succeeds'(sK39_skl,sK39_skl) ),
introduced(definition,[new_symbols(definition,[sQ225_spl])],[split_symbol_definition]) ).
fof(f6667,plain,
( ~ sQ225_spl
| '@<_succeeds'(sK39_skl,sK39_skl) ),
inference(component_clause,[status(thm)],[f6666]) ).
fof(f6670,plain,
( ~ sQ225_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6667,f2056]) ).
fof(f6671,plain,
~ sQ225_spl,
inference(contradiction_clause,[status(thm)],[f6670]) ).
fof(f6880,definition,
! [X0] :
( sQ230_spl
<=> X0 = s(sK14_skl(X0,sK39_skl)) ),
introduced(definition,[new_symbols(definition,[sQ230_spl])],[split_symbol_definition]) ).
fof(f6881,plain,
! [X0] :
( ~ sQ230_spl
| X0 = s(sK14_skl(X0,sK39_skl)) ),
inference(component_clause,[status(thm)],[f6880]) ).
fof(f7280,plain,
! [X0] :
( ~ sQ3_spl
| '@+'(s(sK38_skl),X0) = s('@+'(sK38_skl,X0)) ),
inference(resolution,[status(thm)],[f518,f312]) ).
fof(f7655,definition,
( sQ246_spl
<=> '@<_succeeds'(sK38_skl,sK38_skl) ),
introduced(definition,[new_symbols(definition,[sQ246_spl])],[split_symbol_definition]) ).
fof(f7656,plain,
( ~ sQ246_spl
| '@<_succeeds'(sK38_skl,sK38_skl) ),
inference(component_clause,[status(thm)],[f7655]) ).
fof(f7668,plain,
( ~ sQ246_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7656,f2056]) ).
fof(f7669,plain,
~ sQ246_spl,
inference(contradiction_clause,[status(thm)],[f7668]) ).
fof(f8038,plain,
( ~ sQ126_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3174,f110]) ).
fof(f8039,plain,
~ sQ126_spl,
inference(contradiction_clause,[status(thm)],[f8038]) ).
fof(f8054,definition,
( sQ256_spl
<=> s('0') = '0' ),
introduced(definition,[new_symbols(definition,[sQ256_spl])],[split_symbol_definition]) ).
fof(f8055,plain,
( ~ sQ256_spl
| s('0') = '0' ),
inference(component_clause,[status(thm)],[f8054]) ).
fof(f8063,plain,
( ~ sQ256_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8055,f110]) ).
fof(f8064,plain,
~ sQ256_spl,
inference(contradiction_clause,[status(thm)],[f8063]) ).
fof(f8094,plain,
( ~ sQ128_spl
| $false ),
inference(resolution,[status(thm)],[f3188,f110]) ).
fof(f8122,plain,
~ sQ128_spl,
inference(contradiction_clause,[status(thm)],[f8094]) ).
fof(f8222,plain,
( sQ43_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1009,f3055]) ).
fof(f8223,plain,
sQ43_spl,
inference(contradiction_clause,[status(thm)],[f8222]) ).
fof(f8869,plain,
( ~ sQ149_spl
| '0' = s(sK32_skl('0')) ),
inference(resolution,[status(thm)],[f3535,f381]) ).
fof(f8884,plain,
( ~ sQ149_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8869,f110]) ).
fof(f8885,plain,
~ sQ149_spl,
inference(contradiction_clause,[status(thm)],[f8884]) ).
fof(f9110,definition,
( sQ323_spl
<=> '0' = s(sK18_skl('0',sK41_skl)) ),
introduced(definition,[new_symbols(definition,[sQ323_spl])],[split_symbol_definition]) ).
fof(f9111,plain,
( ~ sQ323_spl
| '0' = s(sK18_skl('0',sK41_skl)) ),
inference(component_clause,[status(thm)],[f9110]) ).
fof(f9123,plain,
( ~ sQ323_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f9111,f110]) ).
fof(f9124,plain,
~ sQ323_spl,
inference(contradiction_clause,[status(thm)],[f9123]) ).
fof(f10823,definition,
( sQ399_spl
<=> '@<_succeeds'(sK37_skl,sK37_skl) ),
introduced(definition,[new_symbols(definition,[sQ399_spl])],[split_symbol_definition]) ).
fof(f10824,plain,
( ~ sQ399_spl
| '@<_succeeds'(sK37_skl,sK37_skl) ),
inference(component_clause,[status(thm)],[f10823]) ).
fof(f10846,plain,
( ~ sQ399_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f10824,f2056]) ).
fof(f10847,plain,
~ sQ399_spl,
inference(contradiction_clause,[status(thm)],[f10846]) ).
fof(f14553,definition,
( sQ558_spl
<=> s(sK39_skl) = '0' ),
introduced(definition,[new_symbols(definition,[sQ558_spl])],[split_symbol_definition]) ).
fof(f14554,plain,
( ~ sQ558_spl
| s(sK39_skl) = '0' ),
inference(component_clause,[status(thm)],[f14553]) ).
fof(f18354,definition,
( sQ705_spl
<=> '0' = s(sK26_skl('0',sK41_skl)) ),
introduced(definition,[new_symbols(definition,[sQ705_spl])],[split_symbol_definition]) ).
fof(f18355,plain,
( ~ sQ705_spl
| '0' = s(sK26_skl('0',sK41_skl)) ),
inference(component_clause,[status(thm)],[f18354]) ).
fof(f18365,plain,
( ~ sQ705_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f18355,f110]) ).
fof(f18366,plain,
~ sQ705_spl,
inference(contradiction_clause,[status(thm)],[f18365]) ).
fof(f18376,definition,
( sQ710_spl
<=> '0' = s(sK22_skl(sK41_skl,'0')) ),
introduced(definition,[new_symbols(definition,[sQ710_spl])],[split_symbol_definition]) ).
fof(f18377,plain,
( ~ sQ710_spl
| '0' = s(sK22_skl(sK41_skl,'0')) ),
inference(component_clause,[status(thm)],[f18376]) ).
fof(f18380,plain,
( ~ sQ710_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f18377,f110]) ).
fof(f18381,plain,
~ sQ710_spl,
inference(contradiction_clause,[status(thm)],[f18380]) ).
fof(f18398,definition,
! [X0] :
( sQ712_spl
<=> '0' = s(sK9_skl(X0,X0,'0')) ),
introduced(definition,[new_symbols(definition,[sQ712_spl])],[split_symbol_definition]) ).
fof(f18399,plain,
! [X0] :
( ~ sQ712_spl
| '0' = s(sK9_skl(X0,X0,'0')) ),
inference(component_clause,[status(thm)],[f18398]) ).
fof(f18402,plain,
( ~ sQ712_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f18399,f110]) ).
fof(f18403,plain,
~ sQ712_spl,
inference(contradiction_clause,[status(thm)],[f18402]) ).
fof(f18408,definition,
! [X0] :
( sQ713_spl
<=> '0' = s(sK2_skl('0',X0,'0')) ),
introduced(definition,[new_symbols(definition,[sQ713_spl])],[split_symbol_definition]) ).
fof(f18409,plain,
! [X0] :
( ~ sQ713_spl
| '0' = s(sK2_skl('0',X0,'0')) ),
inference(component_clause,[status(thm)],[f18408]) ).
fof(f18412,plain,
( ~ sQ713_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f18409,f110]) ).
fof(f18413,plain,
~ sQ713_spl,
inference(contradiction_clause,[status(thm)],[f18412]) ).
fof(f18591,plain,
( ~ sQ230_spl
| $false ),
inference(resolution,[status(thm)],[f6881,f110]) ).
fof(f18632,plain,
~ sQ230_spl,
inference(contradiction_clause,[status(thm)],[f18591]) ).
fof(f18864,plain,
( ~ sQ558_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f14554,f110]) ).
fof(f18865,plain,
~ sQ558_spl,
inference(contradiction_clause,[status(thm)],[f18864]) ).
fof(f23840,definition,
( sQ927_spl
<=> '0' = s(sK22_skl(sK39_skl,'0')) ),
introduced(definition,[new_symbols(definition,[sQ927_spl])],[split_symbol_definition]) ).
fof(f23841,plain,
( ~ sQ927_spl
| '0' = s(sK22_skl(sK39_skl,'0')) ),
inference(component_clause,[status(thm)],[f23840]) ).
fof(f23844,plain,
( ~ sQ927_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f23841,f110]) ).
fof(f23845,plain,
~ sQ927_spl,
inference(contradiction_clause,[status(thm)],[f23844]) ).
fof(f24518,plain,
! [X0] :
( ~ sQ3_spl
| ~ sQ0_spl
| '@+'(sK37_skl,X0) = s('@+'(sK38_skl,X0)) ),
inference(forward_demodulation,[status(thm)],[f508,f7280]) ).
fof(f24890,plain,
( ~ sQ4_spl
| ~ sQ5_spl
| '@=<_succeeds'(s('@+'(sK38_skl,sK39_skl)),s('@+'(sK38_skl,sK40_skl))) ),
inference(resolution,[status(thm)],[f5559,f540]) ).
fof(f24920,plain,
( ~ sQ4_spl
| ~ sQ5_spl
| ~ sQ3_spl
| ~ sQ0_spl
| '@=<_succeeds'('@+'(sK37_skl,sK39_skl),s('@+'(sK38_skl,sK40_skl))) ),
inference(forward_demodulation,[status(thm)],[f24518,f24890]) ).
fof(f24921,plain,
( ~ sQ4_spl
| ~ sQ5_spl
| ~ sQ3_spl
| ~ sQ0_spl
| '@=<_succeeds'('@+'(sK37_skl,sK39_skl),'@+'(sK37_skl,sK40_skl)) ),
inference(forward_demodulation,[status(thm)],[f24518,f24920]) ).
fof(f24922,plain,
( ~ sQ4_spl
| ~ sQ5_spl
| ~ sQ3_spl
| ~ sQ0_spl
| sQ6_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f24921,f531]) ).
fof(f24923,plain,
( ~ sQ4_spl
| ~ sQ5_spl
| ~ sQ3_spl
| ~ sQ0_spl
| sQ6_spl ),
inference(contradiction_clause,[status(thm)],[f24922]) ).
fof(f25046,plain,
( sQ6_spl
| ~ sQ1_spl
| ~ '@=<_succeeds'('@+'(sK37_skl,sK39_skl),sK40_skl) ),
inference(backward_demodulation,[status(thm)],[f3664,f531]) ).
fof(f25047,plain,
( sQ6_spl
| ~ sQ1_spl
| ~ '@=<_succeeds'(sK39_skl,sK40_skl) ),
inference(forward_demodulation,[status(thm)],[f3664,f25046]) ).
fof(f25048,plain,
( sQ6_spl
| ~ sQ1_spl
| ~ sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f25047,f526]) ).
fof(f25049,plain,
( sQ6_spl
| ~ sQ1_spl
| ~ sQ5_spl ),
inference(contradiction_clause,[status(thm)],[f25048]) ).
fof(f25050,plain,
$false,
inference(sat_refutation,[status(thm)],[f516,f520,f524,f528,f532,f5138,f6671,f7669,f8039,f8064,f8122,f8223,f8885,f9124,f10847,f18366,f18381,f18403,f18413,f18632,f18865,f23845,f24923,f25049]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWX043+1 : TPTP v9.3.1. Released v9.1.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/5.38 % Computer : n006.cluster.edu
% 0.09/5.38 % Model : x86_64 x86_64
% 0.09/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.38 % Memory : 8046.5625MB
% 0.09/5.38 % OS : Linux 6.8.0-71-generic
% 0.09/5.38 % CPULimit : 300
% 0.09/5.38 % WCLimit : 300
% 0.09/5.38 % DateTime : Mon Sep 21 10:23:34 UTC 2026
% 0.09/5.38 % CPUTime :
% 0.09/5.40 % Drodi V4.1.1
% 34.07/9.78 % Refutation found
% 34.07/9.78 % SZS status Theorem for theBenchmark: Theorem is valid
% 34.07/9.78 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 32.97/9.91 % Elapsed time: 4.510904 seconds
% 32.97/9.91 % CPU time: 34.974876 seconds
% 32.97/9.91 % Total memory used: 344.815 MB
% 32.97/9.91 % Net memory used: 308.003 MB
%------------------------------------------------------------------------------