%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWX033+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 : n014.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 7.94s 1.45s
% Output : CNFRefutation 7.94s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 15
% Syntax : Number of formulae : 71 ( 8 unt; 10 def)
% Number of atoms : 210 ( 99 equ)
% Maximal formula atoms : 10 ( 2 avg)
% Number of connectives : 226 ( 87 ~; 101 |; 18 &)
% ( 10 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 13 ( 11 usr; 11 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 8 con; 0-2 aty)
% Number of variables : 84 ( 73 !; 11 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
! [Xx4,Xx5] :
( s(Xx4) = s(Xx5)
=> Xx4 = Xx5 ),
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(f52,axiom,
( ! [Xx] :
( ( Xx = '0'
| ? [Xx2] :
( ! [Xy,Xz] :
( '@+'(Xx2,Xy) = '@+'(Xx2,Xz)
=> Xy = Xz )
& nat_succeeds(Xx2)
& Xx = s(Xx2) ) )
=> ! [Xy,Xz] :
( '@+'(Xx,Xy) = '@+'(Xx,Xz)
=> Xy = Xz ) )
=> ! [Xx] :
( nat_succeeds(Xx)
=> ! [Xy,Xz] :
( '@+'(Xx,Xy) = '@+'(Xx,Xz)
=> Xy = Xz ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f53,conjecture,
! [Xx,Xy,Xz] :
( ( '@+'(Xx,Xy) = '@+'(Xx,Xz)
& nat_succeeds(Xx) )
=> Xy = Xz ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f54,negated_conjecture,
~ ! [Xx,Xy,Xz] :
( ( '@+'(Xx,Xy) = '@+'(Xx,Xz)
& nat_succeeds(Xx) )
=> Xy = Xz ),
inference(negated_conjecture,[status(cth)],[f53]) ).
fof(f56,plain,
! [Xx4,Xx5] :
( Xx4 = Xx5
| s(Xx4) != s(Xx5) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f57,plain,
! [X0,X1] :
( X0 = X1
| s(X0) != s(X1) ),
inference(cnf_transformation,[status(thm)],[f56]) ).
fof(f254,plain,
! [X0] : '@+'('0',X0) = X0,
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f255,plain,
! [Xx,Xy] :
( '@+'(s(Xx),Xy) = s('@+'(Xx,Xy))
| ~ nat_succeeds(Xx) ),
inference(pre_NNF_transformation,[status(thm)],[f46]) ).
fof(f256,plain,
! [Xx] :
( ! [Xy] : '@+'(s(Xx),Xy) = s('@+'(Xx,Xy))
| ~ nat_succeeds(Xx) ),
inference(miniscoping,[status(thm)],[f255]) ).
fof(f257,plain,
! [X0,X1] :
( '@+'(s(X0),X1) = s('@+'(X0,X1))
| ~ nat_succeeds(X0) ),
inference(cnf_transformation,[status(thm)],[f256]) ).
fof(f268,plain,
( ! [Xx] :
( ! [Xy,Xz] :
( Xy = Xz
| '@+'(Xx,Xy) != '@+'(Xx,Xz) )
| ~ nat_succeeds(Xx) )
| ? [Xx] :
( ? [Xy,Xz] :
( Xy != Xz
& '@+'(Xx,Xy) = '@+'(Xx,Xz) )
& ( Xx = '0'
| ? [Xx2] :
( ! [Xy,Xz] :
( Xy = Xz
| '@+'(Xx2,Xy) != '@+'(Xx2,Xz) )
& nat_succeeds(Xx2)
& Xx = s(Xx2) ) ) ) ),
inference(pre_NNF_transformation,[status(thm)],[f52]) ).
fof(f269,plain,
( ! [Xx] :
( ! [Xy,Xz] :
( Xy = Xz
| '@+'(Xx,Xy) != '@+'(Xx,Xz) )
| ~ nat_succeeds(Xx) )
| ( sK33_skl != sK34_skl
& '@+'(sK31_skl,sK33_skl) = '@+'(sK31_skl,sK34_skl)
& ( sK31_skl = '0'
| ( ! [Xy,Xz] :
( Xy = Xz
| '@+'(sK32_skl,Xy) != '@+'(sK32_skl,Xz) )
& nat_succeeds(sK32_skl)
& sK31_skl = s(sK32_skl) ) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK31_skl,sK32_skl,sK33_skl,sK34_skl]),skolemize(Xx,sK31_skl),skolemize(Xx2,sK32_skl),skolemize(Xy,sK33_skl),skolemize(Xz,sK34_skl)],[f268]) ).
fof(f270,plain,
! [X0,X1,X2] :
( X1 = X2
| '@+'(X0,X1) != '@+'(X0,X2)
| ~ nat_succeeds(X0)
| sK31_skl = '0'
| sK31_skl = s(sK32_skl) ),
inference(cnf_transformation,[status(thm)],[f269]) ).
fof(f271,plain,
! [X0,X1,X2] :
( X1 = X2
| '@+'(X0,X1) != '@+'(X0,X2)
| ~ nat_succeeds(X0)
| sK31_skl = '0'
| nat_succeeds(sK32_skl) ),
inference(cnf_transformation,[status(thm)],[f269]) ).
fof(f272,plain,
! [X0,X1,X2,X3,X4] :
( X3 = X4
| '@+'(X2,X3) != '@+'(X2,X4)
| ~ nat_succeeds(X2)
| sK31_skl = '0'
| X0 = X1
| '@+'(sK32_skl,X0) != '@+'(sK32_skl,X1) ),
inference(cnf_transformation,[status(thm)],[f269]) ).
fof(f273,plain,
! [X0,X1,X2] :
( X1 = X2
| '@+'(X0,X1) != '@+'(X0,X2)
| ~ nat_succeeds(X0)
| '@+'(sK31_skl,sK33_skl) = '@+'(sK31_skl,sK34_skl) ),
inference(cnf_transformation,[status(thm)],[f269]) ).
fof(f274,plain,
! [X0,X1,X2] :
( X1 = X2
| '@+'(X0,X1) != '@+'(X0,X2)
| ~ nat_succeeds(X0)
| sK33_skl != sK34_skl ),
inference(cnf_transformation,[status(thm)],[f269]) ).
fof(f275,plain,
? [Xx,Xy,Xz] :
( Xy != Xz
& '@+'(Xx,Xy) = '@+'(Xx,Xz)
& nat_succeeds(Xx) ),
inference(pre_NNF_transformation,[status(thm)],[f54]) ).
fof(f276,plain,
? [Xy,Xz] :
( Xy != Xz
& ? [Xx] :
( '@+'(Xx,Xy) = '@+'(Xx,Xz)
& nat_succeeds(Xx) ) ),
inference(miniscoping,[status(thm)],[f275]) ).
fof(f277,plain,
( sK35_skl != sK36_skl
& '@+'(sK37_skl,sK35_skl) = '@+'(sK37_skl,sK36_skl)
& nat_succeeds(sK37_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK35_skl,sK36_skl,sK37_skl]),skolemize(Xy,sK35_skl),skolemize(Xz,sK36_skl),skolemize(Xx,sK37_skl)],[f276]) ).
fof(f278,plain,
nat_succeeds(sK37_skl),
inference(cnf_transformation,[status(thm)],[f277]) ).
fof(f279,plain,
'@+'(sK37_skl,sK35_skl) = '@+'(sK37_skl,sK36_skl),
inference(cnf_transformation,[status(thm)],[f277]) ).
fof(f280,plain,
sK35_skl != sK36_skl,
inference(cnf_transformation,[status(thm)],[f277]) ).
fof(f317,definition,
( sQ0_spl
<=> sK31_skl = s(sK32_skl) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f318,plain,
( ~ sQ0_spl
| sK31_skl = s(sK32_skl) ),
inference(component_clause,[status(thm)],[f317]) ).
fof(f320,definition,
( sQ1_spl
<=> sK31_skl = '0' ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f321,plain,
( ~ sQ1_spl
| sK31_skl = '0' ),
inference(component_clause,[status(thm)],[f320]) ).
fof(f323,definition,
! [X0,X1,X2] :
( sQ2_spl
<=> ( X1 = X2
| '@+'(X0,X1) != '@+'(X0,X2)
| ~ nat_succeeds(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f324,plain,
! [X0,X1,X2] :
( ~ sQ2_spl
| X1 = X2
| '@+'(X0,X1) != '@+'(X0,X2)
| ~ nat_succeeds(X0) ),
inference(component_clause,[status(thm)],[f323]) ).
fof(f326,plain,
( sQ2_spl
| sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f270,f317,f320,f323]) ).
fof(f327,definition,
( sQ3_spl
<=> nat_succeeds(sK32_skl) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f330,plain,
( sQ2_spl
| sQ1_spl
| sQ3_spl ),
inference(split_clause,[status(thm)],[f271,f327,f320,f323]) ).
fof(f331,definition,
! [X0,X1] :
( sQ4_spl
<=> ( X0 = X1
| '@+'(sK32_skl,X0) != '@+'(sK32_skl,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f332,plain,
! [X0,X1] :
( ~ sQ4_spl
| X0 = X1
| '@+'(sK32_skl,X0) != '@+'(sK32_skl,X1) ),
inference(component_clause,[status(thm)],[f331]) ).
fof(f334,plain,
( sQ2_spl
| sQ1_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f272,f331,f320,f323]) ).
fof(f335,definition,
( sQ5_spl
<=> '@+'(sK31_skl,sK33_skl) = '@+'(sK31_skl,sK34_skl) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f336,plain,
( ~ sQ5_spl
| '@+'(sK31_skl,sK33_skl) = '@+'(sK31_skl,sK34_skl) ),
inference(component_clause,[status(thm)],[f335]) ).
fof(f338,plain,
( sQ2_spl
| sQ5_spl ),
inference(split_clause,[status(thm)],[f273,f335,f323]) ).
fof(f339,definition,
( sQ6_spl
<=> sK33_skl = sK34_skl ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f341,plain,
( sQ6_spl
| sK33_skl != sK34_skl ),
inference(component_clause,[status(thm)],[f339]) ).
fof(f342,plain,
( sQ2_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f274,f339,f323]) ).
fof(f381,definition,
( sQ9_spl
<=> nat_succeeds(sK37_skl) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f383,plain,
( sQ9_spl
| ~ nat_succeeds(sK37_skl) ),
inference(component_clause,[status(thm)],[f381]) ).
fof(f781,plain,
( sQ9_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f383,f278]) ).
fof(f782,plain,
sQ9_spl,
inference(contradiction_clause,[status(thm)],[f781]) ).
fof(f1721,plain,
( ~ sQ2_spl
| sK35_skl = sK36_skl
| ~ nat_succeeds(sK37_skl) ),
inference(resolution,[status(thm)],[f324,f279]) ).
fof(f1732,definition,
( sQ53_spl
<=> sK35_skl = sK36_skl ),
introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition]) ).
fof(f1733,plain,
( ~ sQ53_spl
| sK35_skl = sK36_skl ),
inference(component_clause,[status(thm)],[f1732]) ).
fof(f1735,plain,
( ~ sQ2_spl
| sQ53_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f1721,f381,f1732,f323]) ).
fof(f1763,plain,
( ~ sQ53_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1733,f280]) ).
fof(f1764,plain,
~ sQ53_spl,
inference(contradiction_clause,[status(thm)],[f1763]) ).
fof(f1765,plain,
( ~ sQ5_spl
| ~ sQ1_spl
| '@+'('0',sK33_skl) = '@+'(sK31_skl,sK34_skl) ),
inference(forward_demodulation,[status(thm)],[f321,f336]) ).
fof(f1766,plain,
( ~ sQ5_spl
| ~ sQ1_spl
| sK33_skl = '@+'(sK31_skl,sK34_skl) ),
inference(forward_demodulation,[status(thm)],[f254,f1765]) ).
fof(f1767,plain,
( ~ sQ5_spl
| ~ sQ1_spl
| sK33_skl = '@+'('0',sK34_skl) ),
inference(forward_demodulation,[status(thm)],[f321,f1766]) ).
fof(f1768,plain,
( ~ sQ5_spl
| ~ sQ1_spl
| sK33_skl = sK34_skl ),
inference(forward_demodulation,[status(thm)],[f254,f1767]) ).
fof(f1769,plain,
( sQ6_spl
| ~ sQ5_spl
| ~ sQ1_spl
| sK33_skl != sK33_skl ),
inference(forward_demodulation,[status(thm)],[f1768,f341]) ).
fof(f1770,plain,
( sQ6_spl
| ~ sQ5_spl
| ~ sQ1_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f1769]) ).
fof(f1771,plain,
( sQ6_spl
| ~ sQ5_spl
| ~ sQ1_spl ),
inference(contradiction_clause,[status(thm)],[f1770]) ).
fof(f1928,plain,
! [X0] :
( ~ sQ0_spl
| '@+'(sK31_skl,X0) = s('@+'(sK32_skl,X0))
| ~ nat_succeeds(sK32_skl) ),
inference(paramodulation,[status(thm)],[f318,f257]) ).
fof(f1966,definition,
! [X0] :
( sQ58_spl
<=> '@+'(sK31_skl,X0) = s('@+'(sK32_skl,X0)) ),
introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition]) ).
fof(f1967,plain,
! [X0] :
( ~ sQ58_spl
| '@+'(sK31_skl,X0) = s('@+'(sK32_skl,X0)) ),
inference(component_clause,[status(thm)],[f1966]) ).
fof(f1969,plain,
( ~ sQ0_spl
| sQ58_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f1928,f327,f1966,f317]) ).
fof(f2186,plain,
! [X0,X1] :
( ~ sQ58_spl
| X0 = '@+'(sK32_skl,X1)
| s(X0) != '@+'(sK31_skl,X1) ),
inference(paramodulation,[status(thm)],[f1967,f57]) ).
fof(f2988,plain,
! [X0] :
( ~ sQ5_spl
| ~ sQ58_spl
| X0 = '@+'(sK32_skl,sK34_skl)
| s(X0) != '@+'(sK31_skl,sK33_skl) ),
inference(paramodulation,[status(thm)],[f336,f2186]) ).
fof(f3016,plain,
( ~ sQ58_spl
| ~ sQ5_spl
| '@+'(sK32_skl,sK33_skl) = '@+'(sK32_skl,sK34_skl) ),
inference(resolution,[status(thm)],[f2988,f1967]) ).
fof(f3143,plain,
( ~ sQ4_spl
| ~ sQ58_spl
| ~ sQ5_spl
| sK33_skl = sK34_skl ),
inference(resolution,[status(thm)],[f3016,f332]) ).
fof(f3163,plain,
( ~ sQ4_spl
| ~ sQ58_spl
| ~ sQ5_spl
| sQ6_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3143,f341]) ).
fof(f3164,plain,
( ~ sQ4_spl
| ~ sQ58_spl
| ~ sQ5_spl
| sQ6_spl ),
inference(contradiction_clause,[status(thm)],[f3163]) ).
fof(f3165,plain,
$false,
inference(sat_refutation,[status(thm)],[f326,f330,f334,f338,f342,f782,f1735,f1764,f1771,f1969,f3164]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWX033+1 : TPTP v9.3.1. Released v9.1.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n014.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 10:22:20 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.13/0.37 % Drodi V4.1.1
% 7.94/1.45 % Refutation found
% 7.94/1.45 % SZS status Theorem for theBenchmark: Theorem is valid
% 7.94/1.45 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 7.94/1.48 % Elapsed time: 1.107491 seconds
% 7.94/1.48 % CPU time: 8.455190 seconds
% 7.94/1.48 % Total memory used: 209.488 MB
% 7.94/1.48 % Net memory used: 198.803 MB
%------------------------------------------------------------------------------