Termination Proof using AProVE

Term Rewriting System R:
[y, x]
ack(0, y) -> s(y)
ack(s(x), 0) -> ack(x, s(0))
ack(s(x), s(y)) -> ack(x, ack(s(x), y))
ack(s(x), y) -> f(x, x)
f(s(x), y) -> f(x, s(x))
f(x, s(y)) -> f(y, x)
f(x, y) -> ack(x, y)

Innermost Termination of R to be shown.

     ↳Dependency Pair Analysis

R contains the following Dependency Pairs:

ACK(s(x), 0) -> ACK(x, s(0))
ACK(s(x), s(y)) -> ACK(x, ack(s(x), y))
ACK(s(x), s(y)) -> ACK(s(x), y)
ACK(s(x), y) -> F(x, x)
F(s(x), y) -> F(x, s(x))
F(x, s(y)) -> F(y, x)
F(x, y) -> ACK(x, y)

Furthermore, R contains one SCC.

     ↳DPs

       →DP Problem 1

         ↳Narrowing Transformation

Dependency Pairs:

F(x, y) -> ACK(x, y)
F(x, s(y)) -> F(y, x)
F(s(x), y) -> F(x, s(x))
ACK(s(x), y) -> F(x, x)
ACK(s(x), s(y)) -> ACK(s(x), y)
ACK(s(x), s(y)) -> ACK(x, ack(s(x), y))
ACK(s(x), 0) -> ACK(x, s(0))

Rules:

ack(0, y) -> s(y)
ack(s(x), 0) -> ack(x, s(0))
ack(s(x), s(y)) -> ack(x, ack(s(x), y))
ack(s(x), y) -> f(x, x)
f(s(x), y) -> f(x, s(x))
f(x, s(y)) -> f(y, x)
f(x, y) -> ack(x, y)

Strategy:

innermost

On this DP problem, a Narrowing SCC transformation can be performed.
As a result of transforming the rule

ACK(s(x), s(y)) -> ACK(x, ack(s(x), y))

three new Dependency Pairs are created:

ACK(s(x''), s(0)) -> ACK(x'', ack(x'', s(0)))
ACK(s(x''), s(s(y''))) -> ACK(x'', ack(x'', ack(s(x''), y'')))
ACK(s(x''), s(y'')) -> ACK(x'', f(x'', x''))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Forward Instantiation Transformation

Dependency Pairs:

ACK(s(x''), s(y'')) -> ACK(x'', f(x'', x''))
ACK(s(x''), s(s(y''))) -> ACK(x'', ack(x'', ack(s(x''), y'')))
ACK(s(x''), s(0)) -> ACK(x'', ack(x'', s(0)))
F(x, s(y)) -> F(y, x)
F(s(x), y) -> F(x, s(x))
ACK(s(x), y) -> F(x, x)
ACK(s(x), s(y)) -> ACK(s(x), y)
ACK(s(x), 0) -> ACK(x, s(0))
F(x, y) -> ACK(x, y)

Rules:

ack(0, y) -> s(y)
ack(s(x), 0) -> ack(x, s(0))
ack(s(x), s(y)) -> ack(x, ack(s(x), y))
ack(s(x), y) -> f(x, x)
f(s(x), y) -> f(x, s(x))
f(x, s(y)) -> f(y, x)
f(x, y) -> ack(x, y)

Strategy:

innermost

On this DP problem, a Forward Instantiation SCC transformation can be performed.
As a result of transforming the rule

ACK(s(x), 0) -> ACK(x, s(0))

two new Dependency Pairs are created:

ACK(s(s(x'')), 0) -> ACK(s(x''), s(0))
ACK(s(s(x'''')), 0) -> ACK(s(x''''), s(0))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳FwdInst

...

               →DP Problem 3

                 ↳Forward Instantiation Transformation

Dependency Pairs:

ACK(s(s(x'''')), 0) -> ACK(s(x''''), s(0))
ACK(s(s(x'')), 0) -> ACK(s(x''), s(0))
ACK(s(x''), s(s(y''))) -> ACK(x'', ack(x'', ack(s(x''), y'')))
ACK(s(x''), s(0)) -> ACK(x'', ack(x'', s(0)))
F(x, y) -> ACK(x, y)
F(x, s(y)) -> F(y, x)
F(s(x), y) -> F(x, s(x))
ACK(s(x), y) -> F(x, x)
ACK(s(x), s(y)) -> ACK(s(x), y)
ACK(s(x''), s(y'')) -> ACK(x'', f(x'', x''))

Rules:

ack(0, y) -> s(y)
ack(s(x), 0) -> ack(x, s(0))
ack(s(x), s(y)) -> ack(x, ack(s(x), y))
ack(s(x), y) -> f(x, x)
f(s(x), y) -> f(x, s(x))
f(x, s(y)) -> f(y, x)
f(x, y) -> ack(x, y)

Strategy:

innermost

On this DP problem, a Forward Instantiation SCC transformation can be performed.
As a result of transforming the rule

F(x, y) -> ACK(x, y)

seven new Dependency Pairs are created:

F(s(x''), s(y'')) -> ACK(s(x''), s(y''))
F(s(x''), y'') -> ACK(s(x''), y'')
F(s(x''''), s(0)) -> ACK(s(x''''), s(0))
F(s(x''''), s(s(y''''))) -> ACK(s(x''''), s(s(y'''')))
F(s(x''''), s(y'''')) -> ACK(s(x''''), s(y''''))
F(s(s(x'''')), 0) -> ACK(s(s(x'''')), 0)
F(s(s(x'''''')), 0) -> ACK(s(s(x'''''')), 0)

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳FwdInst

...

               →DP Problem 4

                 ↳Forward Instantiation Transformation

Dependency Pairs:

F(s(s(x'''''')), 0) -> ACK(s(s(x'''''')), 0)
F(s(s(x'''')), 0) -> ACK(s(s(x'''')), 0)
F(s(x''''), s(y'''')) -> ACK(s(x''''), s(y''''))
F(s(x''''), s(s(y''''))) -> ACK(s(x''''), s(s(y'''')))
F(s(x''''), s(0)) -> ACK(s(x''''), s(0))
F(s(x''), y'') -> ACK(s(x''), y'')
ACK(s(s(x'')), 0) -> ACK(s(x''), s(0))
ACK(s(x''), s(y'')) -> ACK(x'', f(x'', x''))
ACK(s(x''), s(s(y''))) -> ACK(x'', ack(x'', ack(s(x''), y'')))
ACK(s(x''), s(0)) -> ACK(x'', ack(x'', s(0)))
F(s(x''), s(y'')) -> ACK(s(x''), s(y''))
F(x, s(y)) -> F(y, x)
F(s(x), y) -> F(x, s(x))
ACK(s(x), y) -> F(x, x)
ACK(s(x), s(y)) -> ACK(s(x), y)
ACK(s(s(x'''')), 0) -> ACK(s(x''''), s(0))

Rules:

ack(0, y) -> s(y)
ack(s(x), 0) -> ack(x, s(0))
ack(s(x), s(y)) -> ack(x, ack(s(x), y))
ack(s(x), y) -> f(x, x)
f(s(x), y) -> f(x, s(x))
f(x, s(y)) -> f(y, x)
f(x, y) -> ack(x, y)

Strategy:

innermost

On this DP problem, a Forward Instantiation SCC transformation can be performed.
As a result of transforming the rule

ACK(s(x), y) -> F(x, x)

six new Dependency Pairs are created:

ACK(s(s(x'')), y) -> F(s(x''), s(x''))
ACK(s(s(y'')), y) -> F(s(y''), s(y''))
ACK(s(s(x'''')), y) -> F(s(x''''), s(x''''))
ACK(s(s(0)), y) -> F(s(0), s(0))
ACK(s(s(s(y''''''))), y) -> F(s(s(y'''''')), s(s(y'''''')))
ACK(s(s(x'''''')), y) -> F(s(x''''''), s(x''''''))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳FwdInst

...

               →DP Problem 5

                 ↳Forward Instantiation Transformation

Dependency Pairs:

F(s(s(x'''')), 0) -> ACK(s(s(x'''')), 0)
ACK(s(s(x'''''')), y) -> F(s(x''''''), s(x''''''))
F(s(x''''), s(s(y''''))) -> ACK(s(x''''), s(s(y'''')))
ACK(s(s(s(y''''''))), y) -> F(s(s(y'''''')), s(s(y'''''')))
F(s(x''''), s(y'''')) -> ACK(s(x''''), s(y''''))
ACK(s(s(0)), y) -> F(s(0), s(0))
F(s(x''''), s(0)) -> ACK(s(x''''), s(0))
ACK(s(s(x'''')), y) -> F(s(x''''), s(x''''))
F(s(x''), y'') -> ACK(s(x''), y'')
ACK(s(s(y'')), y) -> F(s(y''), s(y''))
F(s(x''), s(y'')) -> ACK(s(x''), s(y''))
F(x, s(y)) -> F(y, x)
F(s(x), y) -> F(x, s(x))
ACK(s(s(x'')), y) -> F(s(x''), s(x''))
ACK(s(s(x'''')), 0) -> ACK(s(x''''), s(0))
ACK(s(x''), s(y'')) -> ACK(x'', f(x'', x''))
ACK(s(x''), s(s(y''))) -> ACK(x'', ack(x'', ack(s(x''), y'')))
ACK(s(x''), s(0)) -> ACK(x'', ack(x'', s(0)))
ACK(s(x), s(y)) -> ACK(s(x), y)
ACK(s(s(x'')), 0) -> ACK(s(x''), s(0))
F(s(s(x'''''')), 0) -> ACK(s(s(x'''''')), 0)

Rules:

ack(0, y) -> s(y)
ack(s(x), 0) -> ack(x, s(0))
ack(s(x), s(y)) -> ack(x, ack(s(x), y))
ack(s(x), y) -> f(x, x)
f(s(x), y) -> f(x, s(x))
f(x, s(y)) -> f(y, x)
f(x, y) -> ack(x, y)

Strategy:

innermost

On this DP problem, a Forward Instantiation SCC transformation can be performed.
As a result of transforming the rule

ACK(s(x), s(y)) -> ACK(s(x), y)

12 new Dependency Pairs are created:

ACK(s(x''), s(s(y''))) -> ACK(s(x''), s(y''))
ACK(s(x'), s(s(0))) -> ACK(s(x'), s(0))
ACK(s(x'), s(s(s(y'''')))) -> ACK(s(x'), s(s(y'''')))
ACK(s(x'), s(s(y''''))) -> ACK(s(x'), s(y''''))
ACK(s(s(x'''')), s(0)) -> ACK(s(s(x'''')), 0)
ACK(s(s(x'''''')), s(0)) -> ACK(s(s(x'''''')), 0)
ACK(s(s(x'''')), s(y'')) -> ACK(s(s(x'''')), y'')
ACK(s(s(y'''')), s(y'')) -> ACK(s(s(y'''')), y'')
ACK(s(s(x'''''')), s(y'')) -> ACK(s(s(x'''''')), y'')
ACK(s(s(0)), s(y'')) -> ACK(s(s(0)), y'')
ACK(s(s(s(y''''''''))), s(y'')) -> ACK(s(s(s(y''''''''))), y'')
ACK(s(s(x'''''''')), s(y'')) -> ACK(s(s(x'''''''')), y'')

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳FwdInst

...

               →DP Problem 6

                 ↳Forward Instantiation Transformation

Dependency Pairs:

F(s(s(x'''''')), 0) -> ACK(s(s(x'''''')), 0)
ACK(s(s(s(y''''''''))), s(y'')) -> ACK(s(s(s(y''''''''))), y'')
ACK(s(s(x'''''''')), s(y'')) -> ACK(s(s(x'''''''')), y'')
ACK(s(s(0)), s(y'')) -> ACK(s(s(0)), y'')
ACK(s(s(x'''''')), s(y'')) -> ACK(s(s(x'''''')), y'')
ACK(s(s(y'''')), s(y'')) -> ACK(s(s(y'''')), y'')
ACK(s(x'), s(s(y''''))) -> ACK(s(x'), s(y''''))
ACK(s(x'), s(s(s(y'''')))) -> ACK(s(x'), s(s(y'''')))
ACK(s(s(x'''')), s(y'')) -> ACK(s(s(x'''')), y'')
ACK(s(s(x'''''')), s(0)) -> ACK(s(s(x'''''')), 0)
ACK(s(s(x'''')), s(0)) -> ACK(s(s(x'''')), 0)
ACK(s(x'), s(s(0))) -> ACK(s(x'), s(0))
ACK(s(x''), s(s(y''))) -> ACK(s(x''), s(y''))
ACK(s(s(x'''''')), y) -> F(s(x''''''), s(x''''''))
F(s(x''''), s(s(y''''))) -> ACK(s(x''''), s(s(y'''')))
ACK(s(s(s(y''''''))), y) -> F(s(s(y'''''')), s(s(y'''''')))
F(s(x''''), s(y'''')) -> ACK(s(x''''), s(y''''))
ACK(s(s(0)), y) -> F(s(0), s(0))
F(s(x''''), s(0)) -> ACK(s(x''''), s(0))
ACK(s(s(x'''')), y) -> F(s(x''''), s(x''''))
F(s(x''), y'') -> ACK(s(x''), y'')
ACK(s(s(y'')), y) -> F(s(y''), s(y''))
F(s(x''), s(y'')) -> ACK(s(x''), s(y''))
F(x, s(y)) -> F(y, x)
F(s(x), y) -> F(x, s(x))
ACK(s(s(x'')), y) -> F(s(x''), s(x''))
ACK(s(s(x'''')), 0) -> ACK(s(x''''), s(0))
ACK(s(x''), s(y'')) -> ACK(x'', f(x'', x''))
ACK(s(x''), s(s(y''))) -> ACK(x'', ack(x'', ack(s(x''), y'')))
ACK(s(x''), s(0)) -> ACK(x'', ack(x'', s(0)))
ACK(s(s(x'')), 0) -> ACK(s(x''), s(0))
F(s(s(x'''')), 0) -> ACK(s(s(x'''')), 0)

Rules:

ack(0, y) -> s(y)
ack(s(x), 0) -> ack(x, s(0))
ack(s(x), s(y)) -> ack(x, ack(s(x), y))
ack(s(x), y) -> f(x, x)
f(s(x), y) -> f(x, s(x))
f(x, s(y)) -> f(y, x)
f(x, y) -> ack(x, y)

Strategy:

innermost

On this DP problem, a Forward Instantiation SCC transformation can be performed.
As a result of transforming the rule

F(x, s(y)) -> F(y, x)

nine new Dependency Pairs are created:

F(s(y''), s(y0)) -> F(y0, s(y''))
F(x0, s(s(x''))) -> F(s(x''), x0)
F(s(y''''), s(s(x''''))) -> F(s(x''''), s(y''''))
F(x', s(s(x''''))) -> F(s(x''''), x')
F(s(0), s(s(x''''''))) -> F(s(x''''''), s(0))
F(s(s(y'''''')), s(s(x''''''))) -> F(s(x''''''), s(s(y'''''')))
F(s(y''''''), s(s(x''''''))) -> F(s(x''''''), s(y''''''))
F(0, s(s(s(x'''''')))) -> F(s(s(x'''''')), 0)
F(0, s(s(s(x'''''''')))) -> F(s(s(x'''''''')), 0)

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳FwdInst

...

               →DP Problem 7

                 ↳Forward Instantiation Transformation

Dependency Pairs:

ACK(s(s(s(y''''''''))), s(y'')) -> ACK(s(s(s(y''''''''))), y'')
ACK(s(s(x'''''''')), s(y'')) -> ACK(s(s(x'''''''')), y'')
ACK(s(s(0)), s(y'')) -> ACK(s(s(0)), y'')
ACK(s(s(x'''''')), s(y'')) -> ACK(s(s(x'''''')), y'')
ACK(s(s(y'''')), s(y'')) -> ACK(s(s(y'''')), y'')
ACK(s(x'), s(s(y''''))) -> ACK(s(x'), s(y''''))
ACK(s(x'), s(s(s(y'''')))) -> ACK(s(x'), s(s(y'''')))
ACK(s(s(x'''')), s(y'')) -> ACK(s(s(x'''')), y'')
ACK(s(s(x'''''')), s(0)) -> ACK(s(s(x'''''')), 0)
ACK(s(s(x'''')), s(0)) -> ACK(s(s(x'''')), 0)
ACK(s(x'), s(s(0))) -> ACK(s(x'), s(0))
ACK(s(x''), s(s(y''))) -> ACK(s(x''), s(y''))
F(0, s(s(s(x'''''''')))) -> F(s(s(x'''''''')), 0)
F(0, s(s(s(x'''''')))) -> F(s(s(x'''''')), 0)
F(s(y''''''), s(s(x''''''))) -> F(s(x''''''), s(y''''''))
F(s(s(y'''''')), s(s(x''''''))) -> F(s(x''''''), s(s(y'''''')))
F(s(0), s(s(x''''''))) -> F(s(x''''''), s(0))
F(x', s(s(x''''))) -> F(s(x''''), x')
F(s(y''''), s(s(x''''))) -> F(s(x''''), s(y''''))
F(s(s(x'''')), 0) -> ACK(s(s(x'''')), 0)
F(x0, s(s(x''))) -> F(s(x''), x0)
F(s(y''), s(y0)) -> F(y0, s(y''))
ACK(s(s(x'''''')), y) -> F(s(x''''''), s(x''''''))
F(s(x''''), s(s(y''''))) -> ACK(s(x''''), s(s(y'''')))
ACK(s(s(s(y''''''))), y) -> F(s(s(y'''''')), s(s(y'''''')))
F(s(x''''), s(y'''')) -> ACK(s(x''''), s(y''''))
ACK(s(s(0)), y) -> F(s(0), s(0))
F(s(x''''), s(0)) -> ACK(s(x''''), s(0))
ACK(s(s(x'''')), y) -> F(s(x''''), s(x''''))
F(s(x''), y'') -> ACK(s(x''), y'')
ACK(s(s(y'')), y) -> F(s(y''), s(y''))
F(s(x''), s(y'')) -> ACK(s(x''), s(y''))
F(s(x), y) -> F(x, s(x))
ACK(s(s(x'')), y) -> F(s(x''), s(x''))
ACK(s(s(x'''')), 0) -> ACK(s(x''''), s(0))
ACK(s(x''), s(y'')) -> ACK(x'', f(x'', x''))
ACK(s(x''), s(s(y''))) -> ACK(x'', ack(x'', ack(s(x''), y'')))
ACK(s(x''), s(0)) -> ACK(x'', ack(x'', s(0)))
ACK(s(s(x'')), 0) -> ACK(s(x''), s(0))
F(s(s(x'''''')), 0) -> ACK(s(s(x'''''')), 0)

Rules:

ack(0, y) -> s(y)
ack(s(x), 0) -> ack(x, s(0))
ack(s(x), s(y)) -> ack(x, ack(s(x), y))
ack(s(x), y) -> f(x, x)
f(s(x), y) -> f(x, s(x))
f(x, s(y)) -> f(y, x)
f(x, y) -> ack(x, y)

Strategy:

innermost

On this DP problem, a Forward Instantiation SCC transformation can be performed.
As a result of transforming the rule

F(s(x), y) -> F(x, s(x))

eight new Dependency Pairs are created:

F(s(s(x'')), y) -> F(s(x''), s(s(x'')))
F(s(s(x'''')), y) -> F(s(x''''), s(s(x'''')))
F(s(s(x'''''')), y) -> F(s(x''''''), s(s(x'''''')))
F(s(s(y'''')), y) -> F(s(y''''), s(s(y'''')))
F(s(s(y'''''')), y) -> F(s(y''''''), s(s(y'''''')))
F(s(s(0)), y) -> F(s(0), s(s(0)))
F(s(s(s(y''''''''))), y) -> F(s(s(y'''''''')), s(s(s(y''''''''))))
F(s(s(y'''''''')), y) -> F(s(y''''''''), s(s(y'''''''')))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳FwdInst

...

               →DP Problem 8

                 ↳Remaining Obligation(s)

The following remains to be proven:
Dependency Pairs:

ACK(s(s(x'''''''')), s(y'')) -> ACK(s(s(x'''''''')), y'')
ACK(s(s(0)), s(y'')) -> ACK(s(s(0)), y'')
ACK(s(s(x'''''')), s(y'')) -> ACK(s(s(x'''''')), y'')
ACK(s(s(y'''')), s(y'')) -> ACK(s(s(y'''')), y'')
ACK(s(x'), s(s(y''''))) -> ACK(s(x'), s(y''''))
ACK(s(x'), s(s(s(y'''')))) -> ACK(s(x'), s(s(y'''')))
ACK(s(s(x'''')), s(y'')) -> ACK(s(s(x'''')), y'')
ACK(s(s(x'''''')), s(0)) -> ACK(s(s(x'''''')), 0)
ACK(s(s(x'''')), s(0)) -> ACK(s(s(x'''')), 0)
ACK(s(x'), s(s(0))) -> ACK(s(x'), s(0))
ACK(s(x''), s(s(y''))) -> ACK(s(x''), s(y''))
F(0, s(s(s(x'''''''')))) -> F(s(s(x'''''''')), 0)
F(0, s(s(s(x'''''')))) -> F(s(s(x'''''')), 0)
F(s(s(y'''''''')), y) -> F(s(y''''''''), s(s(y'''''''')))
F(s(s(s(y''''''''))), y) -> F(s(s(y'''''''')), s(s(s(y''''''''))))
F(s(s(0)), y) -> F(s(0), s(s(0)))
F(s(s(y'''''')), y) -> F(s(y''''''), s(s(y'''''')))
F(s(s(y'''')), y) -> F(s(y''''), s(s(y'''')))
F(s(s(x'''''')), y) -> F(s(x''''''), s(s(x'''''')))
F(s(s(x'''')), y) -> F(s(x''''), s(s(x'''')))
F(s(y''''''), s(s(x''''''))) -> F(s(x''''''), s(y''''''))
F(s(s(y'''''')), s(s(x''''''))) -> F(s(x''''''), s(s(y'''''')))
F(s(s(x'')), y) -> F(s(x''), s(s(x'')))
F(s(0), s(s(x''''''))) -> F(s(x''''''), s(0))
F(x', s(s(x''''))) -> F(s(x''''), x')
F(s(y''''), s(s(x''''))) -> F(s(x''''), s(y''''))
F(s(s(x'''''')), 0) -> ACK(s(s(x'''''')), 0)
F(s(s(x'''')), 0) -> ACK(s(s(x'''')), 0)
F(x0, s(s(x''))) -> F(s(x''), x0)
F(s(y''), s(y0)) -> F(y0, s(y''))
ACK(s(s(x'''''')), y) -> F(s(x''''''), s(x''''''))
F(s(x''''), s(s(y''''))) -> ACK(s(x''''), s(s(y'''')))
ACK(s(s(s(y''''''))), y) -> F(s(s(y'''''')), s(s(y'''''')))
F(s(x''''), s(y'''')) -> ACK(s(x''''), s(y''''))
ACK(s(s(0)), y) -> F(s(0), s(0))
F(s(x''''), s(0)) -> ACK(s(x''''), s(0))
ACK(s(s(x'''')), y) -> F(s(x''''), s(x''''))
ACK(s(s(x'''')), 0) -> ACK(s(x''''), s(0))
F(s(x''), y'') -> ACK(s(x''), y'')
ACK(s(s(y'')), y) -> F(s(y''), s(y''))
F(s(x''), s(y'')) -> ACK(s(x''), s(y''))
ACK(s(s(x'')), y) -> F(s(x''), s(x''))
ACK(s(s(x'')), 0) -> ACK(s(x''), s(0))
ACK(s(x''), s(y'')) -> ACK(x'', f(x'', x''))
ACK(s(x''), s(s(y''))) -> ACK(x'', ack(x'', ack(s(x''), y'')))
ACK(s(x''), s(0)) -> ACK(x'', ack(x'', s(0)))
ACK(s(s(s(y''''''''))), s(y'')) -> ACK(s(s(s(y''''''''))), y'')

Rules:

ack(0, y) -> s(y)
ack(s(x), 0) -> ack(x, s(0))
ack(s(x), s(y)) -> ack(x, ack(s(x), y))
ack(s(x), y) -> f(x, x)
f(s(x), y) -> f(x, s(x))
f(x, s(y)) -> f(y, x)
f(x, y) -> ack(x, y)

Strategy:

innermost

Innermost Termination of R could not be shown.
Duration:
0:28 minutes