%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWX042+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:13 PM UTC 2026
% Result : Theorem 216.17s 27.79s
% Output : CNFRefutation 142.02s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 78
% Syntax : Number of formulae : 343 ( 65 unt; 58 def)
% Number of atoms : 926 ( 256 equ)
% Maximal formula atoms : 18 ( 2 avg)
% Number of connectives : 951 ( 368 ~; 366 |; 133 &)
% ( 69 <=>; 15 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 71 ( 68 usr; 56 prp; 0-5 aty)
% Number of functors : 29 ( 29 usr; 8 con; 0-3 aty)
% Number of variables : 403 ( 358 !; 45 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [Xx3] : '0' != s(Xx3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,axiom,
gr('0'),
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p') ).
fof(f16,axiom,
! [Xx1,Xx2,Xx3] :
( times_fails(Xx1,Xx2,Xx3)
<=> ( ( Xx3 != '0'
| Xx1 != '0' )
& ! [Xx4,Xx5] :
( plus_fails(Xx2,Xx5,Xx3)
| times_fails(Xx4,Xx2,Xx5)
| Xx1 != s(Xx4) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f18,axiom,
! [Xx1,Xx2,Xx3] :
( plus_succeeds(Xx1,Xx2,Xx3)
<=> ( ( Xx3 = Xx2
& Xx1 = '0' )
| ? [Xx4,Xx5] :
( plus_succeeds(Xx4,Xx2,Xx5)
& Xx3 = s(Xx5)
& Xx1 = s(Xx4) ) ) ),
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(f24,axiom,
! [Xx1,Xx2] :
( '@<_succeeds'(Xx1,Xx2)
<=> ( ? [Xx5] :
( Xx2 = s(Xx5)
& Xx1 = '0' )
| ? [Xx3,Xx4] :
( '@<_succeeds'(Xx3,Xx4)
& Xx2 = s(Xx4)
& Xx1 = s(Xx3) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f26,axiom,
! [Xx1,Xx2] :
( '@<_terminates'(Xx1,Xx2)
<=> ( ! [Xx5] :
( ( $true
| Xx1 != '0' )
& $true )
& ! [Xx3,Xx4] :
( ( ( ( '@<_terminates'(Xx3,Xx4)
| Xx2 != s(Xx4) )
& $true )
| Xx1 != s(Xx3) )
& $true ) ) ),
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(f28,axiom,
! [Xx1] :
( nat_fails(Xx1)
<=> ( Xx1 != '0'
& ! [Xx2] :
( nat_fails(Xx2)
| Xx1 != s(Xx2) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f30,axiom,
! [Xx,Xy,Xz] :
( nat_succeeds(Xx)
=> ( '@+'(Xx,Xy) = Xz
<=> plus_succeeds(Xx,Xy,Xz) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f36,axiom,
! [Xx,Xy,Xz] :
( plus_succeeds(Xx,Xy,Xz)
=> nat_succeeds(Xx) ),
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(f49,axiom,
! [Xx] :
( nat_succeeds(Xx)
=> '@+'(Xx,'0') = Xx ),
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(f103,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(f104,conjecture,
! [Xx,Xy,Xz] :
( ( '@<_succeeds'(Xy,Xz)
& nat_succeeds(Xx) )
=> '@<_succeeds'('@+'(Xx,Xy),'@+'(Xx,Xz)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f105,negated_conjecture,
~ ! [Xx,Xy,Xz] :
( ( '@<_succeeds'(Xy,Xz)
& nat_succeeds(Xx) )
=> '@<_succeeds'('@+'(Xx,Xy),'@+'(Xx,Xz)) ),
inference(negated_conjecture,[status(cth)],[f104]) ).
fof(f106,plain,
! [X0] : s(X0) != '0',
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f109,plain,
gr('0'),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f134,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(f143,definition,
! [Xx1,Xx2,Xx3,Xx4,Xx5] :
( sP1_prd(Xx5,Xx4,Xx3,Xx2,Xx1)
<=> ( plus_fails(Xx2,Xx5,Xx3)
| times_fails(Xx4,Xx2,Xx5)
| Xx1 != s(Xx4) ) ),
introduced(definition,[new_symbols(definition,[sP1_prd])],[]) ).
fof(f161,definition,
! [Xx1,Xx2,Xx3,Xx4,Xx5] :
( sP2_prd(Xx5,Xx4,Xx3,Xx2,Xx1)
<=> ( plus_succeeds(Xx4,Xx2,Xx5)
& Xx3 = s(Xx5)
& Xx1 = s(Xx4) ) ),
introduced(definition,[new_symbols(definition,[sP2_prd])],[]) ).
fof(f187,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(f188,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)],[f187]) ).
fof(f189,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))],[f188]) ).
fof(f194,plain,
! [X0,X1] :
( X0 != '0'
| '@=<_succeeds'(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f189]) ).
fof(f211,definition,
! [Xx1,Xx2,Xx3,Xx4] :
( sP4_prd(Xx4,Xx3,Xx2,Xx1)
<=> ( '@<_succeeds'(Xx3,Xx4)
& Xx2 = s(Xx4)
& Xx1 = s(Xx3) ) ),
introduced(definition,[new_symbols(definition,[sP4_prd])],[]) ).
fof(f212,plain,
! [Xx1,Xx2] :
( '@<_succeeds'(Xx1,Xx2)
<=> ( ? [Xx5] :
( Xx2 = s(Xx5)
& Xx1 = '0' )
| ? [Xx3,Xx4] : sP4_prd(Xx4,Xx3,Xx2,Xx1) ) ),
inference(formula_renaming,[status(thm)],[f24,f211]) ).
fof(f213,plain,
! [Xx1,Xx2] :
( ( ( ! [Xx5] :
( Xx2 != s(Xx5)
| Xx1 != '0' )
& ! [Xx3,Xx4] : ~ sP4_prd(Xx4,Xx3,Xx2,Xx1) )
| '@<_succeeds'(Xx1,Xx2) )
& ( ? [Xx5] :
( Xx2 = s(Xx5)
& Xx1 = '0' )
| ? [Xx3,Xx4] : sP4_prd(Xx4,Xx3,Xx2,Xx1)
| ~ '@<_succeeds'(Xx1,Xx2) ) ),
inference(NNF_transformation,[status(thm)],[f212]) ).
fof(f214,plain,
( ! [Xx1,Xx2] :
( ( ( ! [Xx5] : Xx2 != s(Xx5)
| Xx1 != '0' )
& ! [Xx3,Xx4] : ~ sP4_prd(Xx4,Xx3,Xx2,Xx1) )
| '@<_succeeds'(Xx1,Xx2) )
& ! [Xx1,Xx2] :
( ( ? [Xx5] : Xx2 = s(Xx5)
& Xx1 = '0' )
| ? [Xx3,Xx4] : sP4_prd(Xx4,Xx3,Xx2,Xx1)
| ~ '@<_succeeds'(Xx1,Xx2) ) ),
inference(miniscoping,[status(thm)],[f213]) ).
fof(f215,plain,
( ! [Xx1,Xx2] :
( ( ( ! [Xx5] : Xx2 != s(Xx5)
| Xx1 != '0' )
& ! [Xx3,Xx4] : ~ sP4_prd(Xx4,Xx3,Xx2,Xx1) )
| '@<_succeeds'(Xx1,Xx2) )
& ! [Xx1,Xx2] :
( ( Xx2 = s(sK21_skl(Xx2,Xx1))
& Xx1 = '0' )
| sP4_prd(sK20_skl(Xx2,Xx1),sK19_skl(Xx2,Xx1),Xx2,Xx1)
| ~ '@<_succeeds'(Xx1,Xx2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK19_skl,sK20_skl,sK21_skl]),skolemize(Xx3,sK19_skl(Xx2,Xx1)),skolemize(Xx4,sK20_skl(Xx2,Xx1)),skolemize(Xx5,sK21_skl(Xx2,Xx1))],[f214]) ).
fof(f218,plain,
! [X0,X1,X2,X3] :
( ~ sP4_prd(X2,X3,X1,X0)
| '@<_succeeds'(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f215]) ).
fof(f229,plain,
! [Xx1,Xx2] :
( ( ? [Xx5] :
( ( $false
& Xx1 = '0' )
| $false )
| ? [Xx3,Xx4] :
( ( ( ( ~ '@<_terminates'(Xx3,Xx4)
& Xx2 = s(Xx4) )
| $false )
& Xx1 = s(Xx3) )
| $false )
| '@<_terminates'(Xx1,Xx2) )
& ( ( ! [Xx5] :
( ( $true
| Xx1 != '0' )
& $true )
& ! [Xx3,Xx4] :
( ( ( ( '@<_terminates'(Xx3,Xx4)
| Xx2 != s(Xx4) )
& $true )
| Xx1 != s(Xx3) )
& $true ) )
| ~ '@<_terminates'(Xx1,Xx2) ) ),
inference(NNF_transformation,[status(thm)],[f26]) ).
fof(f230,plain,
( ! [Xx1,Xx2] :
( ( $false
& Xx1 = '0' )
| $false
| ? [Xx3] :
( ( ? [Xx4] :
( ~ '@<_terminates'(Xx3,Xx4)
& Xx2 = s(Xx4) )
| $false )
& Xx1 = s(Xx3) )
| $false
| '@<_terminates'(Xx1,Xx2) )
& ! [Xx1,Xx2] :
( ( ( $true
| Xx1 != '0' )
& $true
& ! [Xx3] :
( ( ! [Xx4] :
( '@<_terminates'(Xx3,Xx4)
| Xx2 != s(Xx4) )
& $true )
| Xx1 != s(Xx3) )
& $true )
| ~ '@<_terminates'(Xx1,Xx2) ) ),
inference(miniscoping,[status(thm)],[f229]) ).
fof(f231,plain,
( ! [Xx1,Xx2] :
( ( $false
& Xx1 = '0' )
| $false
| ( ( ( ~ '@<_terminates'(sK25_skl(Xx2,Xx1),sK26_skl(Xx2,Xx1))
& Xx2 = s(sK26_skl(Xx2,Xx1)) )
| $false )
& Xx1 = s(sK25_skl(Xx2,Xx1)) )
| $false
| '@<_terminates'(Xx1,Xx2) )
& ! [Xx1,Xx2] :
( ( ( $true
| Xx1 != '0' )
& $true
& ! [Xx3] :
( ( ! [Xx4] :
( '@<_terminates'(Xx3,Xx4)
| Xx2 != s(Xx4) )
& $true )
| Xx1 != s(Xx3) )
& $true )
| ~ '@<_terminates'(Xx1,Xx2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK25_skl,sK26_skl]),skolemize(Xx3,sK25_skl(Xx2,Xx1)),skolemize(Xx4,sK26_skl(Xx2,Xx1))],[f230]) ).
fof(f232,plain,
( ! [Xx1,Xx2] :
( ? [Xx3] :
( ? [Xx4] :
( ~ '@<_terminates'(sK25_skl(Xx2,Xx1),sK26_skl(Xx2,Xx1))
& Xx2 = s(sK26_skl(Xx2,Xx1)) )
& Xx1 = s(sK25_skl(Xx2,Xx1)) )
| '@<_terminates'(Xx1,Xx2) )
& ! [Xx1,Xx2] :
( ! [Xx3] :
( ! [Xx4] :
( '@<_terminates'(Xx3,Xx4)
| Xx2 != s(Xx4) )
| Xx1 != s(Xx3) )
| ~ '@<_terminates'(Xx1,Xx2) ) ),
inference(true_and_false_simplification,[status(thm)],[f231]) ).
fof(f234,plain,
! [X0,X1] :
( s(sK25_skl(X1,X0)) = X0
| '@<_terminates'(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f232]) ).
fof(f237,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(f238,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)],[f237]) ).
fof(f239,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))],[f238]) ).
fof(f243,plain,
! [X0] :
( X0 != '0'
| nat_succeeds(X0) ),
inference(cnf_transformation,[status(thm)],[f239]) ).
fof(f244,plain,
! [Xx1] :
( ( Xx1 = '0'
| ? [Xx2] :
( ~ nat_fails(Xx2)
& Xx1 = s(Xx2) )
| nat_fails(Xx1) )
& ( ( Xx1 != '0'
& ! [Xx2] :
( nat_fails(Xx2)
| Xx1 != s(Xx2) ) )
| ~ nat_fails(Xx1) ) ),
inference(NNF_transformation,[status(thm)],[f28]) ).
fof(f245,plain,
( ! [Xx1] :
( Xx1 = '0'
| ? [Xx2] :
( ~ nat_fails(Xx2)
& Xx1 = s(Xx2) )
| nat_fails(Xx1) )
& ! [Xx1] :
( ( Xx1 != '0'
& ! [Xx2] :
( nat_fails(Xx2)
| Xx1 != s(Xx2) ) )
| ~ nat_fails(Xx1) ) ),
inference(miniscoping,[status(thm)],[f244]) ).
fof(f246,plain,
( ! [Xx1] :
( Xx1 = '0'
| ( ~ nat_fails(sK28_skl(Xx1))
& Xx1 = s(sK28_skl(Xx1)) )
| nat_fails(Xx1) )
& ! [Xx1] :
( ( Xx1 != '0'
& ! [Xx2] :
( nat_fails(Xx2)
| Xx1 != s(Xx2) ) )
| ~ nat_fails(Xx1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK28_skl]),skolemize(Xx2,sK28_skl(Xx1))],[f245]) ).
fof(f248,plain,
! [X0] :
( X0 != '0'
| ~ nat_fails(X0) ),
inference(cnf_transformation,[status(thm)],[f246]) ).
fof(f258,plain,
! [Xx,Xy,Xz] :
( ( '@+'(Xx,Xy) = Xz
<=> plus_succeeds(Xx,Xy,Xz) )
| ~ nat_succeeds(Xx) ),
inference(pre_NNF_transformation,[status(thm)],[f30]) ).
fof(f259,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)],[f258]) ).
fof(f260,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)],[f259]) ).
fof(f261,plain,
! [X0,X1,X2] :
( plus_succeeds(X0,X1,X2)
| '@+'(X0,X1) != X2
| ~ nat_succeeds(X0) ),
inference(cnf_transformation,[status(thm)],[f260]) ).
fof(f278,plain,
! [Xx,Xy,Xz] :
( nat_succeeds(Xx)
| ~ plus_succeeds(Xx,Xy,Xz) ),
inference(pre_NNF_transformation,[status(thm)],[f36]) ).
fof(f279,plain,
! [Xx] :
( nat_succeeds(Xx)
| ! [Xy,Xz] : ~ plus_succeeds(Xx,Xy,Xz) ),
inference(miniscoping,[status(thm)],[f278]) ).
fof(f280,plain,
! [X0,X1,X2] :
( nat_succeeds(X0)
| ~ plus_succeeds(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f279]) ).
fof(f305,plain,
! [X0] : X0 = '@+'('0',X0),
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f306,plain,
! [Xx,Xy] :
( '@+'(s(Xx),Xy) = s('@+'(Xx,Xy))
| ~ nat_succeeds(Xx) ),
inference(pre_NNF_transformation,[status(thm)],[f46]) ).
fof(f307,plain,
! [Xx] :
( ! [Xy] : '@+'(s(Xx),Xy) = s('@+'(Xx,Xy))
| ~ nat_succeeds(Xx) ),
inference(miniscoping,[status(thm)],[f306]) ).
fof(f308,plain,
! [X0,X1] :
( ~ nat_succeeds(X0)
| s('@+'(X0,X1)) = '@+'(s(X0),X1) ),
inference(cnf_transformation,[status(thm)],[f307]) ).
fof(f313,plain,
! [Xx] :
( '@+'(Xx,'0') = Xx
| ~ nat_succeeds(Xx) ),
inference(pre_NNF_transformation,[status(thm)],[f49]) ).
fof(f314,plain,
! [X0] :
( '@+'(X0,'0') = X0
| ~ nat_succeeds(X0) ),
inference(cnf_transformation,[status(thm)],[f313]) ).
fof(f371,plain,
! [Xx,Xy] :
( nat_succeeds(Xx)
| ~ '@<_succeeds'(Xx,Xy) ),
inference(pre_NNF_transformation,[status(thm)],[f73]) ).
fof(f372,plain,
! [Xx] :
( nat_succeeds(Xx)
| ! [Xy] : ~ '@<_succeeds'(Xx,Xy) ),
inference(miniscoping,[status(thm)],[f371]) ).
fof(f373,plain,
! [X0,X1] :
( ~ '@<_succeeds'(X0,X1)
| nat_succeeds(X0) ),
inference(cnf_transformation,[status(thm)],[f372]) ).
fof(f374,plain,
! [Xx,Xy] :
( ? [Xz] : Xy = s(Xz)
| ~ '@<_succeeds'(Xx,Xy) ),
inference(pre_NNF_transformation,[status(thm)],[f74]) ).
fof(f375,plain,
! [Xy] :
( ? [Xz] : Xy = s(Xz)
| ! [Xx] : ~ '@<_succeeds'(Xx,Xy) ),
inference(miniscoping,[status(thm)],[f374]) ).
fof(f376,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))],[f375]) ).
fof(f377,plain,
! [X0,X1] :
( X1 = s(sK32_skl(X1))
| ~ '@<_succeeds'(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f376]) ).
fof(f388,plain,
! [Xx] :
( ~ '@<_succeeds'(Xx,Xx)
| ~ nat_succeeds(Xx) ),
inference(pre_NNF_transformation,[status(thm)],[f79]) ).
fof(f389,plain,
! [X0] :
( ~ nat_succeeds(X0)
| ~ '@<_succeeds'(X0,X0) ),
inference(cnf_transformation,[status(thm)],[f388]) ).
fof(f446,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)],[f103]) ).
fof(f447,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)],[f446]) ).
fof(f448,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)],[f447]) ).
fof(f449,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)],[f447]) ).
fof(f450,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)],[f447]) ).
fof(f451,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)],[f447]) ).
fof(f452,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)],[f447]) ).
fof(f453,plain,
? [Xx,Xy,Xz] :
( ~ '@<_succeeds'('@+'(Xx,Xy),'@+'(Xx,Xz))
& '@<_succeeds'(Xy,Xz)
& nat_succeeds(Xx) ),
inference(pre_NNF_transformation,[status(thm)],[f105]) ).
fof(f454,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)],[f453]) ).
fof(f455,plain,
nat_succeeds(sK41_skl),
inference(cnf_transformation,[status(thm)],[f454]) ).
fof(f456,plain,
'@<_succeeds'(sK42_skl,sK43_skl),
inference(cnf_transformation,[status(thm)],[f454]) ).
fof(f457,plain,
~ '@<_succeeds'('@+'(sK41_skl,sK42_skl),'@+'(sK41_skl,sK43_skl)),
inference(cnf_transformation,[status(thm)],[f454]) ).
fof(f458,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)],[f134]) ).
fof(f459,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)],[f458]) ).
fof(f460,plain,
! [X0,X1,X2,X3,X4] :
( ~ sP0_prd(X2,X1,X3,X4,X0)
| X0 = s(X1) ),
inference(cnf_transformation,[status(thm)],[f459]) ).
fof(f464,plain,
! [Xx1,Xx2,Xx3,Xx4,Xx5] :
( ( ( ~ plus_fails(Xx2,Xx5,Xx3)
& ~ times_fails(Xx4,Xx2,Xx5)
& Xx1 = s(Xx4) )
| sP1_prd(Xx5,Xx4,Xx3,Xx2,Xx1) )
& ( plus_fails(Xx2,Xx5,Xx3)
| times_fails(Xx4,Xx2,Xx5)
| Xx1 != s(Xx4)
| ~ sP1_prd(Xx5,Xx4,Xx3,Xx2,Xx1) ) ),
inference(NNF_transformation,[status(thm)],[f143]) ).
fof(f465,plain,
( ! [Xx1,Xx2,Xx3,Xx4,Xx5] :
( ( ~ plus_fails(Xx2,Xx5,Xx3)
& ~ times_fails(Xx4,Xx2,Xx5)
& Xx1 = s(Xx4) )
| sP1_prd(Xx5,Xx4,Xx3,Xx2,Xx1) )
& ! [Xx1,Xx2,Xx3,Xx4,Xx5] :
( plus_fails(Xx2,Xx5,Xx3)
| times_fails(Xx4,Xx2,Xx5)
| Xx1 != s(Xx4)
| ~ sP1_prd(Xx5,Xx4,Xx3,Xx2,Xx1) ) ),
inference(miniscoping,[status(thm)],[f464]) ).
fof(f467,plain,
! [X0,X1,X2,X3,X4] :
( sP1_prd(X2,X1,X3,X4,X0)
| X0 = s(X1) ),
inference(cnf_transformation,[status(thm)],[f465]) ).
fof(f470,plain,
! [Xx1,Xx2,Xx3,Xx4,Xx5] :
( ( ~ plus_succeeds(Xx4,Xx2,Xx5)
| Xx3 != s(Xx5)
| Xx1 != s(Xx4)
| sP2_prd(Xx5,Xx4,Xx3,Xx2,Xx1) )
& ( ( plus_succeeds(Xx4,Xx2,Xx5)
& Xx3 = s(Xx5)
& Xx1 = s(Xx4) )
| ~ sP2_prd(Xx5,Xx4,Xx3,Xx2,Xx1) ) ),
inference(NNF_transformation,[status(thm)],[f161]) ).
fof(f471,plain,
( ! [Xx1,Xx2,Xx3,Xx4,Xx5] :
( ~ plus_succeeds(Xx4,Xx2,Xx5)
| Xx3 != s(Xx5)
| Xx1 != s(Xx4)
| sP2_prd(Xx5,Xx4,Xx3,Xx2,Xx1) )
& ! [Xx1,Xx2,Xx3,Xx4,Xx5] :
( ( plus_succeeds(Xx4,Xx2,Xx5)
& Xx3 = s(Xx5)
& Xx1 = s(Xx4) )
| ~ sP2_prd(Xx5,Xx4,Xx3,Xx2,Xx1) ) ),
inference(miniscoping,[status(thm)],[f470]) ).
fof(f472,plain,
! [X0,X1,X2,X3,X4] :
( ~ sP2_prd(X2,X1,X3,X4,X0)
| X0 = s(X1) ),
inference(cnf_transformation,[status(thm)],[f471]) ).
fof(f482,plain,
! [Xx1,Xx2,Xx3,Xx4] :
( ( ~ '@<_succeeds'(Xx3,Xx4)
| Xx2 != s(Xx4)
| Xx1 != s(Xx3)
| sP4_prd(Xx4,Xx3,Xx2,Xx1) )
& ( ( '@<_succeeds'(Xx3,Xx4)
& Xx2 = s(Xx4)
& Xx1 = s(Xx3) )
| ~ sP4_prd(Xx4,Xx3,Xx2,Xx1) ) ),
inference(NNF_transformation,[status(thm)],[f211]) ).
fof(f483,plain,
( ! [Xx1,Xx2,Xx3,Xx4] :
( ~ '@<_succeeds'(Xx3,Xx4)
| Xx2 != s(Xx4)
| Xx1 != s(Xx3)
| sP4_prd(Xx4,Xx3,Xx2,Xx1) )
& ! [Xx1,Xx2,Xx3,Xx4] :
( ( '@<_succeeds'(Xx3,Xx4)
& Xx2 = s(Xx4)
& Xx1 = s(Xx3) )
| ~ sP4_prd(Xx4,Xx3,Xx2,Xx1) ) ),
inference(miniscoping,[status(thm)],[f482]) ).
fof(f487,plain,
! [X0,X1,X2,X3] :
( ~ '@<_succeeds'(X1,X0)
| X2 != s(X0)
| X3 != s(X1)
| sP4_prd(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f483]) ).
fof(f494,definition,
( sQ0_spl
<=> sK37_skl = s(sK38_skl) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f495,plain,
( ~ sQ0_spl
| sK37_skl = s(sK38_skl) ),
inference(component_clause,[status(thm)],[f494]) ).
fof(f497,definition,
( sQ1_spl
<=> sK37_skl = '0' ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f498,plain,
( ~ sQ1_spl
| sK37_skl = '0' ),
inference(component_clause,[status(thm)],[f497]) ).
fof(f500,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(f501,plain,
! [X0,X1,X2] :
( ~ sQ2_spl
| ~ nat_succeeds(X2)
| '@<_succeeds'('@+'(X2,X0),'@+'(X2,X1))
| ~ '@<_succeeds'(X0,X1) ),
inference(component_clause,[status(thm)],[f500]) ).
fof(f503,plain,
( sQ2_spl
| sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f448,f494,f497,f500]) ).
fof(f504,definition,
( sQ3_spl
<=> nat_succeeds(sK38_skl) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f505,plain,
( ~ sQ3_spl
| nat_succeeds(sK38_skl) ),
inference(component_clause,[status(thm)],[f504]) ).
fof(f507,plain,
( sQ2_spl
| sQ1_spl
| sQ3_spl ),
inference(split_clause,[status(thm)],[f449,f504,f497,f500]) ).
fof(f508,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(f509,plain,
! [X0,X1] :
( ~ sQ4_spl
| ~ '@<_succeeds'(X0,X1)
| '@<_succeeds'('@+'(sK38_skl,X0),'@+'(sK38_skl,X1)) ),
inference(component_clause,[status(thm)],[f508]) ).
fof(f511,plain,
( sQ2_spl
| sQ1_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f450,f508,f497,f500]) ).
fof(f512,definition,
( sQ5_spl
<=> '@<_succeeds'(sK39_skl,sK40_skl) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f513,plain,
( ~ sQ5_spl
| '@<_succeeds'(sK39_skl,sK40_skl) ),
inference(component_clause,[status(thm)],[f512]) ).
fof(f515,plain,
( sQ2_spl
| sQ5_spl ),
inference(split_clause,[status(thm)],[f451,f512,f500]) ).
fof(f516,definition,
( sQ6_spl
<=> '@<_succeeds'('@+'(sK37_skl,sK39_skl),'@+'(sK37_skl,sK40_skl)) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f518,plain,
( sQ6_spl
| ~ '@<_succeeds'('@+'(sK37_skl,sK39_skl),'@+'(sK37_skl,sK40_skl)) ),
inference(component_clause,[status(thm)],[f516]) ).
fof(f519,plain,
( sQ2_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f452,f516,f500]) ).
fof(f522,plain,
! [X0,X1] :
( plus_succeeds(X0,X1,'@+'(X0,X1))
| ~ nat_succeeds(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f261]) ).
fof(f528,plain,
nat_succeeds('0'),
inference(destructive_equality_resolution,[status(thm)],[f243]) ).
fof(f534,plain,
! [X0,X1] :
( sP4_prd(X1,X0,s(X1),s(X0))
| ~ '@<_succeeds'(X0,X1) ),
inference(destructive_equality_resolution,[status(thm)],[f487]) ).
fof(f539,plain,
~ nat_fails('0'),
inference(destructive_equality_resolution,[status(thm)],[f248]) ).
fof(f546,plain,
! [X0] : '@=<_succeeds'('0',X0),
inference(destructive_equality_resolution,[status(thm)],[f194]) ).
fof(f604,plain,
! [X0] : ~ '@<_succeeds'(X0,X0),
inference(forward_subsumption_resolution,[status(thm)],[f389,f373]) ).
fof(f1827,plain,
! [X0,X1] :
( ~ '@<_succeeds'(X0,X1)
| '@<_succeeds'(s(X0),s(X1)) ),
inference(resolution,[status(thm)],[f534,f218]) ).
fof(f1884,plain,
! [X0,X1] :
( ~ sQ2_spl
| '@<_succeeds'('@+'(sK41_skl,X0),'@+'(sK41_skl,X1))
| ~ '@<_succeeds'(X0,X1) ),
inference(resolution,[status(thm)],[f501,f455]) ).
fof(f2528,plain,
! [X0] : plus_succeeds('0',X0,'@+'('0',X0)),
inference(resolution,[status(thm)],[f528,f522]) ).
fof(f2536,plain,
! [X0] : plus_succeeds('0',X0,X0),
inference(forward_demodulation,[status(thm)],[f305,f2528]) ).
fof(f2614,definition,
! [X0] :
( sQ114_spl
<=> s(sK15_skl(X0,'0')) = '0' ),
introduced(definition,[new_symbols(definition,[sQ114_spl])],[split_symbol_definition]) ).
fof(f2615,plain,
! [X0] :
( ~ sQ114_spl
| '0' = s(sK15_skl(X0,'0')) ),
inference(component_clause,[status(thm)],[f2614]) ).
fof(f2773,definition,
! [X0] :
( sQ126_spl
<=> ~ sP1_prd(sK3_skl('0',X0,'0'),sK2_skl('0',X0,'0'),'0',X0,'0') ),
introduced(definition,[new_symbols(definition,[sQ126_spl])],[split_symbol_definition]) ).
fof(f2774,plain,
! [X0] :
( ~ sQ126_spl
| ~ sP1_prd(sK3_skl('0',X0,'0'),sK2_skl('0',X0,'0'),'0',X0,'0') ),
inference(component_clause,[status(thm)],[f2773]) ).
fof(f4072,plain,
( ~ sQ5_spl
| ~ sQ4_spl
| '@<_succeeds'('@+'(sK38_skl,sK39_skl),'@+'(sK38_skl,sK40_skl)) ),
inference(resolution,[status(thm)],[f509,f513]) ).
fof(f4291,plain,
! [X0] :
( ~ sQ3_spl
| '@+'(s(sK38_skl),X0) = s('@+'(sK38_skl,X0)) ),
inference(resolution,[status(thm)],[f505,f308]) ).
fof(f4548,definition,
! [X0] :
( sQ198_spl
<=> sP2_prd(sK8_skl(X0,X0,'0'),sK7_skl(X0,X0,'0'),X0,X0,'0') ),
introduced(definition,[new_symbols(definition,[sQ198_spl])],[split_symbol_definition]) ).
fof(f4549,plain,
! [X0] :
( ~ sQ198_spl
| sP2_prd(sK8_skl(X0,X0,'0'),sK7_skl(X0,X0,'0'),X0,X0,'0') ),
inference(component_clause,[status(thm)],[f4548]) ).
fof(f4773,definition,
! [X0] :
( sQ204_spl
<=> X0 = s(sK14_skl(X0,'0')) ),
introduced(definition,[new_symbols(definition,[sQ204_spl])],[split_symbol_definition]) ).
fof(f4774,plain,
! [X0] :
( ~ sQ204_spl
| s(sK14_skl(X0,'0')) = X0 ),
inference(component_clause,[status(thm)],[f4773]) ).
fof(f4819,definition,
! [X0] :
( sQ206_spl
<=> s(sK16_skl(X0,'0')) = X0 ),
introduced(definition,[new_symbols(definition,[sQ206_spl])],[split_symbol_definition]) ).
fof(f4820,plain,
! [X0] :
( ~ sQ206_spl
| X0 = s(sK16_skl(X0,'0')) ),
inference(component_clause,[status(thm)],[f4819]) ).
fof(f4956,definition,
! [X0] :
( sQ220_spl
<=> sP0_prd(sK1_skl('0',X0,'0'),sK0_skl('0',X0,'0'),'0',X0,'0') ),
introduced(definition,[new_symbols(definition,[sQ220_spl])],[split_symbol_definition]) ).
fof(f4957,plain,
! [X0] :
( ~ sQ220_spl
| sP0_prd(sK1_skl('0',X0,'0'),sK0_skl('0',X0,'0'),'0',X0,'0') ),
inference(component_clause,[status(thm)],[f4956]) ).
fof(f5082,plain,
! [X0] :
( ~ sQ1_spl
| X0 = '@+'(X0,sK37_skl)
| ~ nat_succeeds(X0) ),
inference(forward_demodulation,[status(thm)],[f498,f314]) ).
fof(f6448,plain,
nat_succeeds('0'),
inference(resolution,[status(thm)],[f2536,f280]) ).
fof(f7278,plain,
( ~ sQ1_spl
| '0' = '@+'('0',sK37_skl) ),
inference(resolution,[status(thm)],[f5082,f6448]) ).
fof(f7282,plain,
( ~ sQ1_spl
| '0' = sK37_skl ),
inference(forward_demodulation,[status(thm)],[f305,f7278]) ).
fof(f8412,plain,
( ~ sQ2_spl
| '@<_succeeds'('@+'(sK41_skl,sK42_skl),'@+'(sK41_skl,sK43_skl)) ),
inference(resolution,[status(thm)],[f456,f1884]) ).
fof(f8424,plain,
( ~ sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8412,f457]) ).
fof(f8425,plain,
~ sQ2_spl,
inference(contradiction_clause,[status(thm)],[f8424]) ).
fof(f8507,plain,
! [X0] :
( ~ sQ3_spl
| ~ sQ0_spl
| '@+'(sK37_skl,X0) = s('@+'(sK38_skl,X0)) ),
inference(forward_demodulation,[status(thm)],[f495,f4291]) ).
fof(f8794,plain,
! [X0] :
( ~ sQ1_spl
| X0 = '@+'(sK37_skl,X0) ),
inference(backward_demodulation,[status(thm)],[f7282,f305]) ).
fof(f9167,plain,
( sQ6_spl
| ~ sQ1_spl
| ~ '@<_succeeds'('@+'(sK37_skl,sK39_skl),sK40_skl) ),
inference(backward_demodulation,[status(thm)],[f8794,f518]) ).
fof(f9168,plain,
( sQ6_spl
| ~ sQ1_spl
| ~ '@<_succeeds'(sK39_skl,sK40_skl) ),
inference(forward_demodulation,[status(thm)],[f8794,f9167]) ).
fof(f9169,plain,
( sQ6_spl
| ~ sQ1_spl
| ~ sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f9168,f513]) ).
fof(f9170,plain,
( sQ6_spl
| ~ sQ1_spl
| ~ sQ5_spl ),
inference(contradiction_clause,[status(thm)],[f9169]) ).
fof(f9904,definition,
( sQ324_spl
<=> s(sK37_skl) = '0' ),
introduced(definition,[new_symbols(definition,[sQ324_spl])],[split_symbol_definition]) ).
fof(f9905,plain,
( ~ sQ324_spl
| '0' = s(sK37_skl) ),
inference(component_clause,[status(thm)],[f9904]) ).
fof(f10111,definition,
( sQ328_spl
<=> '@<_succeeds'(sK38_skl,sK38_skl) ),
introduced(definition,[new_symbols(definition,[sQ328_spl])],[split_symbol_definition]) ).
fof(f10112,plain,
( ~ sQ328_spl
| '@<_succeeds'(sK38_skl,sK38_skl) ),
inference(component_clause,[status(thm)],[f10111]) ).
fof(f10121,plain,
( ~ sQ328_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f10112,f604]) ).
fof(f10122,plain,
~ sQ328_spl,
inference(contradiction_clause,[status(thm)],[f10121]) ).
fof(f11737,definition,
( sQ403_spl
<=> '@<_succeeds'(sK39_skl,'0') ),
introduced(definition,[new_symbols(definition,[sQ403_spl])],[split_symbol_definition]) ).
fof(f11738,plain,
( ~ sQ403_spl
| '@<_succeeds'(sK39_skl,'0') ),
inference(component_clause,[status(thm)],[f11737]) ).
fof(f11744,definition,
( sQ405_spl
<=> '@<_succeeds'(sK38_skl,'0') ),
introduced(definition,[new_symbols(definition,[sQ405_spl])],[split_symbol_definition]) ).
fof(f11745,plain,
( ~ sQ405_spl
| '@<_succeeds'(sK38_skl,'0') ),
inference(component_clause,[status(thm)],[f11744]) ).
fof(f12202,definition,
( sQ409_spl
<=> '@<_terminates'('0',sK37_skl) ),
introduced(definition,[new_symbols(definition,[sQ409_spl])],[split_symbol_definition]) ).
fof(f12204,plain,
( sQ409_spl
| ~ '@<_terminates'('0',sK37_skl) ),
inference(component_clause,[status(thm)],[f12202]) ).
fof(f13402,definition,
( sQ435_spl
<=> '0' = s(sK13_skl(s('0'),'0')) ),
introduced(definition,[new_symbols(definition,[sQ435_spl])],[split_symbol_definition]) ).
fof(f13403,plain,
( ~ sQ435_spl
| '0' = s(sK13_skl(s('0'),'0')) ),
inference(component_clause,[status(thm)],[f13402]) ).
fof(f13415,plain,
( ~ sQ435_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f13403,f106]) ).
fof(f13416,plain,
~ sQ435_spl,
inference(contradiction_clause,[status(thm)],[f13415]) ).
fof(f13425,definition,
( sQ438_spl
<=> '0' = s(sK13_skl(sK43_skl,'0')) ),
introduced(definition,[new_symbols(definition,[sQ438_spl])],[split_symbol_definition]) ).
fof(f13426,plain,
( ~ sQ438_spl
| '0' = s(sK13_skl(sK43_skl,'0')) ),
inference(component_clause,[status(thm)],[f13425]) ).
fof(f13429,definition,
! [X0] :
( sQ439_spl
<=> '0' = s(sK13_skl(s(X0),'0')) ),
introduced(definition,[new_symbols(definition,[sQ439_spl])],[split_symbol_definition]) ).
fof(f13430,plain,
! [X0] :
( ~ sQ439_spl
| '0' = s(sK13_skl(s(X0),'0')) ),
inference(component_clause,[status(thm)],[f13429]) ).
fof(f13433,definition,
( sQ440_spl
<=> '0' = s(sK13_skl(sK37_skl,'0')) ),
introduced(definition,[new_symbols(definition,[sQ440_spl])],[split_symbol_definition]) ).
fof(f13434,plain,
( ~ sQ440_spl
| '0' = s(sK13_skl(sK37_skl,'0')) ),
inference(component_clause,[status(thm)],[f13433]) ).
fof(f13441,definition,
( sQ442_spl
<=> '0' = s(sK13_skl(sK38_skl,'0')) ),
introduced(definition,[new_symbols(definition,[sQ442_spl])],[split_symbol_definition]) ).
fof(f13442,plain,
( ~ sQ442_spl
| '0' = s(sK13_skl(sK38_skl,'0')) ),
inference(component_clause,[status(thm)],[f13441]) ).
fof(f13449,plain,
( ~ sQ439_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f13430,f106]) ).
fof(f13450,plain,
~ sQ439_spl,
inference(contradiction_clause,[status(thm)],[f13449]) ).
fof(f13451,plain,
( ~ sQ438_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f13426,f106]) ).
fof(f13452,plain,
~ sQ438_spl,
inference(contradiction_clause,[status(thm)],[f13451]) ).
fof(f13453,plain,
( ~ sQ440_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f13434,f106]) ).
fof(f13454,plain,
~ sQ440_spl,
inference(contradiction_clause,[status(thm)],[f13453]) ).
fof(f13455,plain,
( ~ sQ442_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f13442,f106]) ).
fof(f13456,plain,
~ sQ442_spl,
inference(contradiction_clause,[status(thm)],[f13455]) ).
fof(f15012,plain,
( ~ sQ405_spl
| '0' = s(sK32_skl('0')) ),
inference(resolution,[status(thm)],[f11745,f377]) ).
fof(f15019,definition,
( sQ466_spl
<=> s(sK20_skl('0',sK38_skl)) = '0' ),
introduced(definition,[new_symbols(definition,[sQ466_spl])],[split_symbol_definition]) ).
fof(f15020,plain,
( ~ sQ466_spl
| s(sK20_skl('0',sK38_skl)) = '0' ),
inference(component_clause,[status(thm)],[f15019]) ).
fof(f15022,definition,
( sQ467_spl
<=> '0' = s(sK21_skl('0',sK38_skl)) ),
introduced(definition,[new_symbols(definition,[sQ467_spl])],[split_symbol_definition]) ).
fof(f15023,plain,
( ~ sQ467_spl
| '0' = s(sK21_skl('0',sK38_skl)) ),
inference(component_clause,[status(thm)],[f15022]) ).
fof(f15026,plain,
( ~ sQ405_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f15012,f106]) ).
fof(f15027,plain,
~ sQ405_spl,
inference(contradiction_clause,[status(thm)],[f15026]) ).
fof(f15028,plain,
( ~ sQ467_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f15023,f106]) ).
fof(f15029,plain,
~ sQ467_spl,
inference(contradiction_clause,[status(thm)],[f15028]) ).
fof(f15030,plain,
( ~ sQ466_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f15020,f106]) ).
fof(f15031,plain,
~ sQ466_spl,
inference(contradiction_clause,[status(thm)],[f15030]) ).
fof(f15137,plain,
( ~ sQ403_spl
| '0' = s(sK32_skl('0')) ),
inference(resolution,[status(thm)],[f11738,f377]) ).
fof(f15142,definition,
( sQ471_spl
<=> s(sK20_skl('0',sK39_skl)) = '0' ),
introduced(definition,[new_symbols(definition,[sQ471_spl])],[split_symbol_definition]) ).
fof(f15143,plain,
( ~ sQ471_spl
| s(sK20_skl('0',sK39_skl)) = '0' ),
inference(component_clause,[status(thm)],[f15142]) ).
fof(f15145,definition,
( sQ472_spl
<=> '0' = s(sK21_skl('0',sK39_skl)) ),
introduced(definition,[new_symbols(definition,[sQ472_spl])],[split_symbol_definition]) ).
fof(f15146,plain,
( ~ sQ472_spl
| '0' = s(sK21_skl('0',sK39_skl)) ),
inference(component_clause,[status(thm)],[f15145]) ).
fof(f15149,plain,
( ~ sQ403_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f15137,f106]) ).
fof(f15150,plain,
~ sQ403_spl,
inference(contradiction_clause,[status(thm)],[f15149]) ).
fof(f15151,plain,
( ~ sQ472_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f15146,f106]) ).
fof(f15152,plain,
~ sQ472_spl,
inference(contradiction_clause,[status(thm)],[f15151]) ).
fof(f15153,plain,
( ~ sQ471_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f15143,f106]) ).
fof(f15154,plain,
~ sQ471_spl,
inference(contradiction_clause,[status(thm)],[f15153]) ).
fof(f15430,plain,
( sQ409_spl
| s(sK25_skl(sK37_skl,'0')) = '0' ),
inference(resolution,[status(thm)],[f12204,f234]) ).
fof(f15434,plain,
( sQ409_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f15430,f106]) ).
fof(f15435,plain,
sQ409_spl,
inference(contradiction_clause,[status(thm)],[f15434]) ).
fof(f15821,definition,
( sQ496_spl
<=> s(sK29_skl('0')) = '0' ),
introduced(definition,[new_symbols(definition,[sQ496_spl])],[split_symbol_definition]) ).
fof(f15822,plain,
( ~ sQ496_spl
| s(sK29_skl('0')) = '0' ),
inference(component_clause,[status(thm)],[f15821]) ).
fof(f15825,plain,
( ~ sQ496_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f15822,f106]) ).
fof(f15826,plain,
~ sQ496_spl,
inference(contradiction_clause,[status(thm)],[f15825]) ).
fof(f16044,definition,
( sQ512_spl
<=> nat_fails('0') ),
introduced(definition,[new_symbols(definition,[sQ512_spl])],[split_symbol_definition]) ).
fof(f16045,plain,
( ~ sQ512_spl
| nat_fails('0') ),
inference(component_clause,[status(thm)],[f16044]) ).
fof(f16048,plain,
( ~ sQ512_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f16045,f539]) ).
fof(f16049,plain,
~ sQ512_spl,
inference(contradiction_clause,[status(thm)],[f16048]) ).
fof(f16405,plain,
( ~ sQ114_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2615,f106]) ).
fof(f16406,plain,
~ sQ114_spl,
inference(contradiction_clause,[status(thm)],[f16405]) ).
fof(f16423,definition,
( sQ545_spl
<=> '@=<_succeeds'('0',sK42_skl) ),
introduced(definition,[new_symbols(definition,[sQ545_spl])],[split_symbol_definition]) ).
fof(f16425,plain,
( sQ545_spl
| ~ '@=<_succeeds'('0',sK42_skl) ),
inference(component_clause,[status(thm)],[f16423]) ).
fof(f16428,definition,
( sQ546_spl
<=> s(sK14_skl('0',sK42_skl)) = '0' ),
introduced(definition,[new_symbols(definition,[sQ546_spl])],[split_symbol_definition]) ).
fof(f16429,plain,
( ~ sQ546_spl
| s(sK14_skl('0',sK42_skl)) = '0' ),
inference(component_clause,[status(thm)],[f16428]) ).
fof(f16449,plain,
( ~ sQ546_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f16429,f106]) ).
fof(f16450,plain,
~ sQ546_spl,
inference(contradiction_clause,[status(thm)],[f16449]) ).
fof(f16451,plain,
( sQ545_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f16425,f546]) ).
fof(f16452,plain,
sQ545_spl,
inference(contradiction_clause,[status(thm)],[f16451]) ).
fof(f16482,definition,
( sQ554_spl
<=> s(sK14_skl('0',sK37_skl)) = '0' ),
introduced(definition,[new_symbols(definition,[sQ554_spl])],[split_symbol_definition]) ).
fof(f16483,plain,
( ~ sQ554_spl
| s(sK14_skl('0',sK37_skl)) = '0' ),
inference(component_clause,[status(thm)],[f16482]) ).
fof(f16487,definition,
( sQ555_spl
<=> '@=<_succeeds'('0',sK37_skl) ),
introduced(definition,[new_symbols(definition,[sQ555_spl])],[split_symbol_definition]) ).
fof(f16489,plain,
( sQ555_spl
| ~ '@=<_succeeds'('0',sK37_skl) ),
inference(component_clause,[status(thm)],[f16487]) ).
fof(f16495,plain,
( sQ555_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f16489,f546]) ).
fof(f16496,plain,
sQ555_spl,
inference(contradiction_clause,[status(thm)],[f16495]) ).
fof(f16497,plain,
( ~ sQ554_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f16483,f106]) ).
fof(f16498,plain,
~ sQ554_spl,
inference(contradiction_clause,[status(thm)],[f16497]) ).
fof(f16518,definition,
( sQ557_spl
<=> s(sK19_skl(sK42_skl,'0')) = '0' ),
introduced(definition,[new_symbols(definition,[sQ557_spl])],[split_symbol_definition]) ).
fof(f16519,plain,
( ~ sQ557_spl
| s(sK19_skl(sK42_skl,'0')) = '0' ),
inference(component_clause,[status(thm)],[f16518]) ).
fof(f16530,definition,
( sQ560_spl
<=> s(sK19_skl(sK41_skl,'0')) = '0' ),
introduced(definition,[new_symbols(definition,[sQ560_spl])],[split_symbol_definition]) ).
fof(f16531,plain,
( ~ sQ560_spl
| s(sK19_skl(sK41_skl,'0')) = '0' ),
inference(component_clause,[status(thm)],[f16530]) ).
fof(f16538,definition,
( sQ562_spl
<=> s(sK19_skl(sK38_skl,'0')) = '0' ),
introduced(definition,[new_symbols(definition,[sQ562_spl])],[split_symbol_definition]) ).
fof(f16539,plain,
( ~ sQ562_spl
| s(sK19_skl(sK38_skl,'0')) = '0' ),
inference(component_clause,[status(thm)],[f16538]) ).
fof(f16551,definition,
( sQ565_spl
<=> s(sK19_skl(sK37_skl,'0')) = '0' ),
introduced(definition,[new_symbols(definition,[sQ565_spl])],[split_symbol_definition]) ).
fof(f16552,plain,
( ~ sQ565_spl
| s(sK19_skl(sK37_skl,'0')) = '0' ),
inference(component_clause,[status(thm)],[f16551]) ).
fof(f16559,definition,
( sQ567_spl
<=> s(sK19_skl(sK43_skl,'0')) = '0' ),
introduced(definition,[new_symbols(definition,[sQ567_spl])],[split_symbol_definition]) ).
fof(f16560,plain,
( ~ sQ567_spl
| s(sK19_skl(sK43_skl,'0')) = '0' ),
inference(component_clause,[status(thm)],[f16559]) ).
fof(f16579,definition,
( sQ572_spl
<=> s(sK19_skl(sK39_skl,'0')) = '0' ),
introduced(definition,[new_symbols(definition,[sQ572_spl])],[split_symbol_definition]) ).
fof(f16580,plain,
( ~ sQ572_spl
| s(sK19_skl(sK39_skl,'0')) = '0' ),
inference(component_clause,[status(thm)],[f16579]) ).
fof(f16583,plain,
( ~ sQ557_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f16519,f106]) ).
fof(f16584,plain,
~ sQ557_spl,
inference(contradiction_clause,[status(thm)],[f16583]) ).
fof(f16585,plain,
( ~ sQ567_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f16560,f106]) ).
fof(f16586,plain,
~ sQ567_spl,
inference(contradiction_clause,[status(thm)],[f16585]) ).
fof(f16587,plain,
( ~ sQ565_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f16552,f106]) ).
fof(f16588,plain,
~ sQ565_spl,
inference(contradiction_clause,[status(thm)],[f16587]) ).
fof(f16589,plain,
( ~ sQ562_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f16539,f106]) ).
fof(f16590,plain,
~ sQ562_spl,
inference(contradiction_clause,[status(thm)],[f16589]) ).
fof(f16591,plain,
( ~ sQ560_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f16531,f106]) ).
fof(f16592,plain,
~ sQ560_spl,
inference(contradiction_clause,[status(thm)],[f16591]) ).
fof(f16593,plain,
( ~ sQ572_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f16580,f106]) ).
fof(f16594,plain,
~ sQ572_spl,
inference(contradiction_clause,[status(thm)],[f16593]) ).
fof(f16688,definition,
( sQ579_spl
<=> s(sK14_skl('0',sK39_skl)) = '0' ),
introduced(definition,[new_symbols(definition,[sQ579_spl])],[split_symbol_definition]) ).
fof(f16689,plain,
( ~ sQ579_spl
| s(sK14_skl('0',sK39_skl)) = '0' ),
inference(component_clause,[status(thm)],[f16688]) ).
fof(f16696,definition,
( sQ581_spl
<=> '@=<_succeeds'('0',sK39_skl) ),
introduced(definition,[new_symbols(definition,[sQ581_spl])],[split_symbol_definition]) ).
fof(f16698,plain,
( sQ581_spl
| ~ '@=<_succeeds'('0',sK39_skl) ),
inference(component_clause,[status(thm)],[f16696]) ).
fof(f16710,plain,
( ~ sQ579_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f16689,f106]) ).
fof(f16711,plain,
~ sQ579_spl,
inference(contradiction_clause,[status(thm)],[f16710]) ).
fof(f16712,plain,
( sQ581_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f16698,f546]) ).
fof(f16713,plain,
sQ581_spl,
inference(contradiction_clause,[status(thm)],[f16712]) ).
fof(f16759,plain,
! [X0] :
( ~ sQ126_spl
| '0' = s(sK2_skl('0',X0,'0')) ),
inference(resolution,[status(thm)],[f2774,f467]) ).
fof(f16760,plain,
( ~ sQ126_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f16759,f106]) ).
fof(f16761,plain,
~ sQ126_spl,
inference(contradiction_clause,[status(thm)],[f16760]) ).
fof(f16888,definition,
( sQ592_spl
<=> '@=<_succeeds'('0',sK38_skl) ),
introduced(definition,[new_symbols(definition,[sQ592_spl])],[split_symbol_definition]) ).
fof(f16890,plain,
( sQ592_spl
| ~ '@=<_succeeds'('0',sK38_skl) ),
inference(component_clause,[status(thm)],[f16888]) ).
fof(f16906,definition,
( sQ596_spl
<=> s(sK14_skl('0',sK38_skl)) = '0' ),
introduced(definition,[new_symbols(definition,[sQ596_spl])],[split_symbol_definition]) ).
fof(f16907,plain,
( ~ sQ596_spl
| s(sK14_skl('0',sK38_skl)) = '0' ),
inference(component_clause,[status(thm)],[f16906]) ).
fof(f16915,plain,
( sQ592_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f16890,f546]) ).
fof(f16916,plain,
sQ592_spl,
inference(contradiction_clause,[status(thm)],[f16915]) ).
fof(f16917,plain,
( ~ sQ596_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f16907,f106]) ).
fof(f16918,plain,
~ sQ596_spl,
inference(contradiction_clause,[status(thm)],[f16917]) ).
fof(f17177,definition,
( sQ628_spl
<=> gr('0') ),
introduced(definition,[new_symbols(definition,[sQ628_spl])],[split_symbol_definition]) ).
fof(f17179,plain,
( sQ628_spl
| ~ gr('0') ),
inference(component_clause,[status(thm)],[f17177]) ).
fof(f17193,plain,
( sQ628_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f17179,f109]) ).
fof(f17194,plain,
sQ628_spl,
inference(contradiction_clause,[status(thm)],[f17193]) ).
fof(f17221,definition,
( sQ633_spl
<=> s(sK19_skl(sK40_skl,'0')) = '0' ),
introduced(definition,[new_symbols(definition,[sQ633_spl])],[split_symbol_definition]) ).
fof(f17222,plain,
( ~ sQ633_spl
| s(sK19_skl(sK40_skl,'0')) = '0' ),
inference(component_clause,[status(thm)],[f17221]) ).
fof(f17232,plain,
( ~ sQ633_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f17222,f106]) ).
fof(f17233,plain,
~ sQ633_spl,
inference(contradiction_clause,[status(thm)],[f17232]) ).
fof(f17523,definition,
( sQ651_spl
<=> '@<_terminates'('0',sK41_skl) ),
introduced(definition,[new_symbols(definition,[sQ651_spl])],[split_symbol_definition]) ).
fof(f17525,plain,
( sQ651_spl
| ~ '@<_terminates'('0',sK41_skl) ),
inference(component_clause,[status(thm)],[f17523]) ).
fof(f17735,plain,
( sQ651_spl
| s(sK25_skl(sK41_skl,'0')) = '0' ),
inference(resolution,[status(thm)],[f17525,f234]) ).
fof(f17740,plain,
( sQ651_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f17735,f106]) ).
fof(f17741,plain,
sQ651_spl,
inference(contradiction_clause,[status(thm)],[f17740]) ).
fof(f18513,definition,
! [X0] :
( sQ698_spl
<=> s(sK14_skl(X0,sK39_skl)) = X0 ),
introduced(definition,[new_symbols(definition,[sQ698_spl])],[split_symbol_definition]) ).
fof(f18514,plain,
! [X0] :
( ~ sQ698_spl
| s(sK14_skl(X0,sK39_skl)) = X0 ),
inference(component_clause,[status(thm)],[f18513]) ).
fof(f21186,plain,
! [X0] :
( ~ sQ198_spl
| '0' = s(sK7_skl(X0,X0,'0')) ),
inference(resolution,[status(thm)],[f4549,f472]) ).
fof(f21188,plain,
( ~ sQ198_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f21186,f106]) ).
fof(f21189,plain,
~ sQ198_spl,
inference(contradiction_clause,[status(thm)],[f21188]) ).
fof(f21567,definition,
( sQ775_spl
<=> '0' = s(sK13_skl(sK42_skl,'0')) ),
introduced(definition,[new_symbols(definition,[sQ775_spl])],[split_symbol_definition]) ).
fof(f21568,plain,
( ~ sQ775_spl
| '0' = s(sK13_skl(sK42_skl,'0')) ),
inference(component_clause,[status(thm)],[f21567]) ).
fof(f21571,definition,
( sQ776_spl
<=> '0' = s(sK13_skl(sK41_skl,'0')) ),
introduced(definition,[new_symbols(definition,[sQ776_spl])],[split_symbol_definition]) ).
fof(f21572,plain,
( ~ sQ776_spl
| '0' = s(sK13_skl(sK41_skl,'0')) ),
inference(component_clause,[status(thm)],[f21571]) ).
fof(f21590,definition,
( sQ779_spl
<=> '0' = s(sK13_skl(sK40_skl,'0')) ),
introduced(definition,[new_symbols(definition,[sQ779_spl])],[split_symbol_definition]) ).
fof(f21591,plain,
( ~ sQ779_spl
| '0' = s(sK13_skl(sK40_skl,'0')) ),
inference(component_clause,[status(thm)],[f21590]) ).
fof(f21595,plain,
( ~ sQ779_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f21591,f106]) ).
fof(f21596,plain,
~ sQ779_spl,
inference(contradiction_clause,[status(thm)],[f21595]) ).
fof(f21597,plain,
( ~ sQ775_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f21568,f106]) ).
fof(f21598,plain,
~ sQ775_spl,
inference(contradiction_clause,[status(thm)],[f21597]) ).
fof(f21599,plain,
( ~ sQ776_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f21572,f106]) ).
fof(f21600,plain,
~ sQ776_spl,
inference(contradiction_clause,[status(thm)],[f21599]) ).
fof(f23496,definition,
( sQ806_spl
<=> '@<_terminates'('0',sK38_skl) ),
introduced(definition,[new_symbols(definition,[sQ806_spl])],[split_symbol_definition]) ).
fof(f23498,plain,
( sQ806_spl
| ~ '@<_terminates'('0',sK38_skl) ),
inference(component_clause,[status(thm)],[f23496]) ).
fof(f23871,plain,
( ~ sQ204_spl
| $false ),
inference(resolution,[status(thm)],[f4774,f106]) ).
fof(f23906,plain,
~ sQ204_spl,
inference(contradiction_clause,[status(thm)],[f23871]) ).
fof(f24004,plain,
! [X0] :
( ~ sQ206_spl
| '0' != X0 ),
inference(paramodulation,[status(thm)],[f4820,f106]) ).
fof(f24044,plain,
( ~ sQ206_spl
| $false ),
inference(destructive_equality_resolution,[status(thm)],[f24004]) ).
fof(f24045,plain,
~ sQ206_spl,
inference(contradiction_clause,[status(thm)],[f24044]) ).
fof(f24101,plain,
! [X0] :
( ~ sQ220_spl
| '0' = s(sK0_skl('0',X0,'0')) ),
inference(resolution,[status(thm)],[f4957,f460]) ).
fof(f24104,plain,
( ~ sQ220_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f24101,f106]) ).
fof(f24105,plain,
~ sQ220_spl,
inference(contradiction_clause,[status(thm)],[f24104]) ).
fof(f24448,definition,
! [X0] :
( sQ833_spl
<=> '0' = s(sK19_skl(s(X0),'0')) ),
introduced(definition,[new_symbols(definition,[sQ833_spl])],[split_symbol_definition]) ).
fof(f24449,plain,
! [X0] :
( ~ sQ833_spl
| '0' = s(sK19_skl(s(X0),'0')) ),
inference(component_clause,[status(thm)],[f24448]) ).
fof(f24454,plain,
( ~ sQ833_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f24449,f106]) ).
fof(f24455,plain,
~ sQ833_spl,
inference(contradiction_clause,[status(thm)],[f24454]) ).
fof(f25568,plain,
( sQ806_spl
| s(sK25_skl(sK38_skl,'0')) = '0' ),
inference(resolution,[status(thm)],[f23498,f234]) ).
fof(f25574,plain,
( sQ806_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f25568,f106]) ).
fof(f25575,plain,
sQ806_spl,
inference(contradiction_clause,[status(thm)],[f25574]) ).
fof(f25897,definition,
( sQ864_spl
<=> s(sK13_skl(sK39_skl,'0')) = '0' ),
introduced(definition,[new_symbols(definition,[sQ864_spl])],[split_symbol_definition]) ).
fof(f25898,plain,
( ~ sQ864_spl
| s(sK13_skl(sK39_skl,'0')) = '0' ),
inference(component_clause,[status(thm)],[f25897]) ).
fof(f25923,plain,
( ~ sQ864_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f25898,f106]) ).
fof(f25924,plain,
~ sQ864_spl,
inference(contradiction_clause,[status(thm)],[f25923]) ).
fof(f27673,definition,
( sQ1013_spl
<=> '@<_terminates'('0',sK39_skl) ),
introduced(definition,[new_symbols(definition,[sQ1013_spl])],[split_symbol_definition]) ).
fof(f27675,plain,
( sQ1013_spl
| ~ '@<_terminates'('0',sK39_skl) ),
inference(component_clause,[status(thm)],[f27673]) ).
fof(f27767,plain,
( sQ1013_spl
| s(sK25_skl(sK39_skl,'0')) = '0' ),
inference(resolution,[status(thm)],[f27675,f234]) ).
fof(f27771,plain,
( sQ1013_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f27767,f106]) ).
fof(f27772,plain,
sQ1013_spl,
inference(contradiction_clause,[status(thm)],[f27771]) ).
fof(f27803,plain,
( ~ sQ698_spl
| $false ),
inference(resolution,[status(thm)],[f18514,f106]) ).
fof(f27859,plain,
~ sQ698_spl,
inference(contradiction_clause,[status(thm)],[f27803]) ).
fof(f28141,plain,
( ~ sQ324_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f9905,f106]) ).
fof(f28142,plain,
~ sQ324_spl,
inference(contradiction_clause,[status(thm)],[f28141]) ).
fof(f30467,plain,
( ~ sQ5_spl
| ~ sQ4_spl
| '@<_succeeds'(s('@+'(sK38_skl,sK39_skl)),s('@+'(sK38_skl,sK40_skl))) ),
inference(resolution,[status(thm)],[f4072,f1827]) ).
fof(f30480,plain,
( ~ sQ5_spl
| ~ sQ4_spl
| ~ sQ3_spl
| ~ sQ0_spl
| '@<_succeeds'('@+'(sK37_skl,sK39_skl),s('@+'(sK38_skl,sK40_skl))) ),
inference(forward_demodulation,[status(thm)],[f8507,f30467]) ).
fof(f30481,plain,
( ~ sQ5_spl
| ~ sQ4_spl
| ~ sQ3_spl
| ~ sQ0_spl
| '@<_succeeds'('@+'(sK37_skl,sK39_skl),'@+'(sK37_skl,sK40_skl)) ),
inference(forward_demodulation,[status(thm)],[f8507,f30480]) ).
fof(f30482,plain,
( ~ sQ5_spl
| ~ sQ4_spl
| ~ sQ3_spl
| ~ sQ0_spl
| sQ6_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f30481,f518]) ).
fof(f30483,plain,
( ~ sQ5_spl
| ~ sQ4_spl
| ~ sQ3_spl
| ~ sQ0_spl
| sQ6_spl ),
inference(contradiction_clause,[status(thm)],[f30482]) ).
fof(f30484,plain,
$false,
inference(sat_refutation,[status(thm)],[f503,f507,f511,f515,f519,f8425,f9170,f10122,f13416,f13450,f13452,f13454,f13456,f15027,f15029,f15031,f15150,f15152,f15154,f15435,f15826,f16049,f16406,f16450,f16452,f16496,f16498,f16584,f16586,f16588,f16590,f16592,f16594,f16711,f16713,f16761,f16916,f16918,f17194,f17233,f17741,f21189,f21596,f21598,f21600,f23906,f24045,f24105,f24455,f25575,f25924,f27772,f27859,f28142,f30483]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWX042+1 : TPTP v9.3.1. Released v9.1.0.
% 0.00/0.04 % 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:23:35 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.37 % Drodi V4.1.1
% 216.17/27.79 % Refutation found
% 216.17/27.79 % SZS status Theorem for theBenchmark: Theorem is valid
% 216.17/27.79 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 142.02/27.89 % Elapsed time: 27.514691 seconds
% 142.02/27.89 % CPU time: 217.331607 seconds
% 142.02/27.89 % Total memory used: 647.925 MB
% 142.02/27.89 % Net memory used: 583.958 MB
%------------------------------------------------------------------------------