Termination Proof using AProVE

Term Rewriting System R:
[x, y, z]
f(f(f(a, b), c), x) -> f(b, f(a, f(c, f(b, x))))
f(x, f(y, z)) -> f(f(x, y), z)

Innermost Termination of R to be shown.

     ↳Dependency Pair Analysis

R contains the following Dependency Pairs:

F(f(f(a, b), c), x) -> F(b, f(a, f(c, f(b, x))))
F(f(f(a, b), c), x) -> F(a, f(c, f(b, x)))
F(f(f(a, b), c), x) -> F(c, f(b, x))
F(f(f(a, b), c), x) -> F(b, x)
F(x, f(y, z)) -> F(f(x, y), z)
F(x, f(y, z)) -> F(x, y)

Furthermore, R contains one SCC.

     ↳DPs

       →DP Problem 1

         ↳Narrowing Transformation

Dependency Pairs:

F(f(f(a, b), c), x) -> F(b, x)
F(f(f(a, b), c), x) -> F(c, f(b, x))
F(x, f(y, z)) -> F(x, y)
F(f(f(a, b), c), x) -> F(a, f(c, f(b, x)))
F(x, f(y, z)) -> F(f(x, y), z)
F(f(f(a, b), c), x) -> F(b, f(a, f(c, f(b, x))))

Rules:

f(f(f(a, b), c), x) -> f(b, f(a, f(c, f(b, x))))
f(x, f(y, z)) -> f(f(x, y), z)

Strategy:

innermost

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

F(f(f(a, b), c), x) -> F(b, f(a, f(c, f(b, x))))

three new Dependency Pairs are created:

F(f(f(a, b), c), x'') -> F(b, f(f(a, c), f(b, x'')))
F(f(f(a, b), c), x'') -> F(b, f(a, f(f(c, b), x'')))
F(f(f(a, b), c), f(y', z')) -> F(b, f(a, f(c, f(f(b, y'), z'))))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Narrowing Transformation

Dependency Pairs:

F(f(f(a, b), c), f(y', z')) -> F(b, f(a, f(c, f(f(b, y'), z'))))
F(f(f(a, b), c), x'') -> F(b, f(a, f(f(c, b), x'')))
F(f(f(a, b), c), x'') -> F(b, f(f(a, c), f(b, x'')))
F(f(f(a, b), c), x) -> F(c, f(b, x))
F(x, f(y, z)) -> F(x, y)
F(f(f(a, b), c), x) -> F(a, f(c, f(b, x)))
F(x, f(y, z)) -> F(f(x, y), z)
F(f(f(a, b), c), x) -> F(b, x)

Rules:

f(f(f(a, b), c), x) -> f(b, f(a, f(c, f(b, x))))
f(x, f(y, z)) -> f(f(x, y), z)

Strategy:

innermost

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

F(f(f(a, b), c), x) -> F(a, f(c, f(b, x)))

two new Dependency Pairs are created:

F(f(f(a, b), c), x'') -> F(a, f(f(c, b), x''))
F(f(f(a, b), c), f(y', z')) -> F(a, f(c, f(f(b, y'), z')))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Nar

...

               →DP Problem 3

                 ↳Narrowing Transformation

Dependency Pairs:

F(f(f(a, b), c), f(y', z')) -> F(a, f(c, f(f(b, y'), z')))
F(f(f(a, b), c), x'') -> F(a, f(f(c, b), x''))
F(f(f(a, b), c), x'') -> F(b, f(a, f(f(c, b), x'')))
F(f(f(a, b), c), x'') -> F(b, f(f(a, c), f(b, x'')))
F(f(f(a, b), c), x) -> F(b, x)
F(x, f(y, z)) -> F(x, y)
F(f(f(a, b), c), x) -> F(c, f(b, x))
F(x, f(y, z)) -> F(f(x, y), z)
F(f(f(a, b), c), f(y', z')) -> F(b, f(a, f(c, f(f(b, y'), z'))))

Rules:

f(f(f(a, b), c), x) -> f(b, f(a, f(c, f(b, x))))
f(x, f(y, z)) -> f(f(x, y), z)

Strategy:

innermost

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

F(f(f(a, b), c), x'') -> F(b, f(f(a, c), f(b, x'')))

two new Dependency Pairs are created:

F(f(f(a, b), c), x''') -> F(b, f(f(f(a, c), b), x'''))
F(f(f(a, b), c), f(y', z')) -> F(b, f(f(a, c), f(f(b, y'), z')))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Nar

...

               →DP Problem 4

                 ↳Narrowing Transformation

Dependency Pairs:

F(f(f(a, b), c), f(y', z')) -> F(b, f(f(a, c), f(f(b, y'), z')))
F(f(f(a, b), c), x''') -> F(b, f(f(f(a, c), b), x'''))
F(f(f(a, b), c), x'') -> F(a, f(f(c, b), x''))
F(f(f(a, b), c), f(y', z')) -> F(b, f(a, f(c, f(f(b, y'), z'))))
F(f(f(a, b), c), x'') -> F(b, f(a, f(f(c, b), x'')))
F(f(f(a, b), c), x) -> F(b, x)
F(x, f(y, z)) -> F(x, y)
F(f(f(a, b), c), x) -> F(c, f(b, x))
F(x, f(y, z)) -> F(f(x, y), z)
F(f(f(a, b), c), f(y', z')) -> F(a, f(c, f(f(b, y'), z')))

Rules:

f(f(f(a, b), c), x) -> f(b, f(a, f(c, f(b, x))))
f(x, f(y, z)) -> f(f(x, y), z)

Strategy:

innermost

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

F(f(f(a, b), c), x'') -> F(b, f(a, f(f(c, b), x'')))

two new Dependency Pairs are created:

F(f(f(a, b), c), x''') -> F(b, f(f(a, f(c, b)), x'''))
F(f(f(a, b), c), f(y', z')) -> F(b, f(a, f(f(f(c, b), y'), z')))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Nar

...

               →DP Problem 5

                 ↳Narrowing Transformation

Dependency Pairs:

F(f(f(a, b), c), f(y', z')) -> F(b, f(a, f(f(f(c, b), y'), z')))
F(f(f(a, b), c), x''') -> F(b, f(f(a, f(c, b)), x'''))
F(f(f(a, b), c), x''') -> F(b, f(f(f(a, c), b), x'''))
F(f(f(a, b), c), f(y', z')) -> F(a, f(c, f(f(b, y'), z')))
F(f(f(a, b), c), x'') -> F(a, f(f(c, b), x''))
F(f(f(a, b), c), f(y', z')) -> F(b, f(a, f(c, f(f(b, y'), z'))))
F(f(f(a, b), c), x) -> F(b, x)
F(x, f(y, z)) -> F(x, y)
F(f(f(a, b), c), x) -> F(c, f(b, x))
F(x, f(y, z)) -> F(f(x, y), z)
F(f(f(a, b), c), f(y', z')) -> F(b, f(f(a, c), f(f(b, y'), z')))

Rules:

f(f(f(a, b), c), x) -> f(b, f(a, f(c, f(b, x))))
f(x, f(y, z)) -> f(f(x, y), z)

Strategy:

innermost

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

F(f(f(a, b), c), f(y', z')) -> F(b, f(a, f(c, f(f(b, y'), z'))))

three new Dependency Pairs are created:

F(f(f(a, b), c), f(y'', z'')) -> F(b, f(f(a, c), f(f(b, y''), z'')))
F(f(f(a, b), c), f(y'', z'')) -> F(b, f(a, f(f(c, f(b, y'')), z'')))
F(f(f(a, b), c), f(f(y'', z''), z')) -> F(b, f(a, f(c, f(f(f(b, y''), z''), z'))))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Nar

...

               →DP Problem 6

                 ↳Narrowing Transformation

Dependency Pairs:

F(f(f(a, b), c), f(f(y'', z''), z')) -> F(b, f(a, f(c, f(f(f(b, y''), z''), z'))))
F(f(f(a, b), c), f(y'', z'')) -> F(b, f(a, f(f(c, f(b, y'')), z'')))
F(f(f(a, b), c), f(y'', z'')) -> F(b, f(f(a, c), f(f(b, y''), z'')))
F(f(f(a, b), c), x''') -> F(b, f(f(a, f(c, b)), x'''))
F(f(f(a, b), c), f(y', z')) -> F(b, f(f(a, c), f(f(b, y'), z')))
F(f(f(a, b), c), x''') -> F(b, f(f(f(a, c), b), x'''))
F(f(f(a, b), c), f(y', z')) -> F(a, f(c, f(f(b, y'), z')))
F(f(f(a, b), c), x'') -> F(a, f(f(c, b), x''))
F(f(f(a, b), c), x) -> F(b, x)
F(x, f(y, z)) -> F(x, y)
F(f(f(a, b), c), x) -> F(c, f(b, x))
F(x, f(y, z)) -> F(f(x, y), z)
F(f(f(a, b), c), f(y', z')) -> F(b, f(a, f(f(f(c, b), y'), z')))

Rules:

f(f(f(a, b), c), x) -> f(b, f(a, f(c, f(b, x))))
f(x, f(y, z)) -> f(f(x, y), z)

Strategy:

innermost

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

F(f(f(a, b), c), f(y', z')) -> F(a, f(c, f(f(b, y'), z')))

two new Dependency Pairs are created:

F(f(f(a, b), c), f(y'', z'')) -> F(a, f(f(c, f(b, y'')), z''))
F(f(f(a, b), c), f(f(y'', z''), z')) -> F(a, f(c, f(f(f(b, y''), z''), z')))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Nar

...

               →DP Problem 7

                 ↳Forward Instantiation Transformation

Dependency Pairs:

F(f(f(a, b), c), f(f(y'', z''), z')) -> F(a, f(c, f(f(f(b, y''), z''), z')))
F(f(f(a, b), c), f(y'', z'')) -> F(a, f(f(c, f(b, y'')), z''))
F(f(f(a, b), c), f(y'', z'')) -> F(b, f(a, f(f(c, f(b, y'')), z'')))
F(f(f(a, b), c), f(y'', z'')) -> F(b, f(f(a, c), f(f(b, y''), z'')))
F(f(f(a, b), c), f(y', z')) -> F(b, f(a, f(f(f(c, b), y'), z')))
F(f(f(a, b), c), x''') -> F(b, f(f(a, f(c, b)), x'''))
F(f(f(a, b), c), f(y', z')) -> F(b, f(f(a, c), f(f(b, y'), z')))
F(f(f(a, b), c), x''') -> F(b, f(f(f(a, c), b), x'''))
F(f(f(a, b), c), x'') -> F(a, f(f(c, b), x''))
F(f(f(a, b), c), x) -> F(b, x)
F(x, f(y, z)) -> F(x, y)
F(f(f(a, b), c), x) -> F(c, f(b, x))
F(x, f(y, z)) -> F(f(x, y), z)
F(f(f(a, b), c), f(f(y'', z''), z')) -> F(b, f(a, f(c, f(f(f(b, y''), z''), z'))))

Rules:

f(f(f(a, b), c), x) -> f(b, f(a, f(c, f(b, x))))
f(x, f(y, z)) -> f(f(x, y), z)

Strategy:

innermost

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

F(f(f(a, b), c), x) -> F(b, x)

one new Dependency Pair is created:

F(f(f(a, b), c), f(y'', z'')) -> F(b, f(y'', z''))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Nar

...

               →DP Problem 8

                 ↳Forward Instantiation Transformation

Dependency Pairs:

F(f(f(a, b), c), f(y'', z'')) -> F(b, f(y'', z''))
F(f(f(a, b), c), f(y'', z'')) -> F(a, f(f(c, f(b, y'')), z''))
F(f(f(a, b), c), f(f(y'', z''), z')) -> F(b, f(a, f(c, f(f(f(b, y''), z''), z'))))
F(f(f(a, b), c), f(y'', z'')) -> F(b, f(a, f(f(c, f(b, y'')), z'')))
F(f(f(a, b), c), f(y'', z'')) -> F(b, f(f(a, c), f(f(b, y''), z'')))
F(f(f(a, b), c), f(y', z')) -> F(b, f(a, f(f(f(c, b), y'), z')))
F(f(f(a, b), c), x''') -> F(b, f(f(a, f(c, b)), x'''))
F(f(f(a, b), c), f(y', z')) -> F(b, f(f(a, c), f(f(b, y'), z')))
F(f(f(a, b), c), x''') -> F(b, f(f(f(a, c), b), x'''))
F(f(f(a, b), c), x'') -> F(a, f(f(c, b), x''))
F(x, f(y, z)) -> F(x, y)
F(f(f(a, b), c), x) -> F(c, f(b, x))
F(x, f(y, z)) -> F(f(x, y), z)
F(f(f(a, b), c), f(f(y'', z''), z')) -> F(a, f(c, f(f(f(b, y''), z''), z')))

Rules:

f(f(f(a, b), c), x) -> f(b, f(a, f(c, f(b, x))))
f(x, f(y, z)) -> f(f(x, y), z)

Strategy:

innermost

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

F(x, f(y, z)) -> F(x, y)

five new Dependency Pairs are created:

F(x'', f(f(y'', z''), z)) -> F(x'', f(y'', z''))
F(f(f(a, b), c), f(y', z)) -> F(f(f(a, b), c), y')
F(f(f(a, b), c), f(f(y''', z'''), z)) -> F(f(f(a, b), c), f(y''', z'''))
F(f(f(a, b), c), f(f(y'''', z''''), z)) -> F(f(f(a, b), c), f(y'''', z''''))
F(f(f(a, b), c), f(f(f(y'''', z''''), z'0'), z)) -> F(f(f(a, b), c), f(f(y'''', z''''), z'0'))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Nar

...

               →DP Problem 9

                 ↳Argument Filtering and Ordering

Dependency Pairs:

F(f(f(a, b), c), f(f(f(y'''', z''''), z'0'), z)) -> F(f(f(a, b), c), f(f(y'''', z''''), z'0'))
F(f(f(a, b), c), f(f(y'''', z''''), z)) -> F(f(f(a, b), c), f(y'''', z''''))
F(f(f(a, b), c), f(f(y''', z'''), z)) -> F(f(f(a, b), c), f(y''', z'''))
F(f(f(a, b), c), f(y', z)) -> F(f(f(a, b), c), y')
F(f(f(a, b), c), f(f(y'', z''), z')) -> F(a, f(c, f(f(f(b, y''), z''), z')))
F(f(f(a, b), c), f(y'', z'')) -> F(a, f(f(c, f(b, y'')), z''))
F(f(f(a, b), c), f(f(y'', z''), z')) -> F(b, f(a, f(c, f(f(f(b, y''), z''), z'))))
F(f(f(a, b), c), f(y'', z'')) -> F(b, f(a, f(f(c, f(b, y'')), z'')))
F(f(f(a, b), c), f(y'', z'')) -> F(b, f(f(a, c), f(f(b, y''), z'')))
F(f(f(a, b), c), f(y', z')) -> F(b, f(a, f(f(f(c, b), y'), z')))
F(f(f(a, b), c), x''') -> F(b, f(f(a, f(c, b)), x'''))
F(f(f(a, b), c), f(y', z')) -> F(b, f(f(a, c), f(f(b, y'), z')))
F(f(f(a, b), c), x''') -> F(b, f(f(f(a, c), b), x'''))
F(f(f(a, b), c), x'') -> F(a, f(f(c, b), x''))
F(x'', f(f(y'', z''), z)) -> F(x'', f(y'', z''))
F(f(f(a, b), c), x) -> F(c, f(b, x))
F(x, f(y, z)) -> F(f(x, y), z)
F(f(f(a, b), c), f(y'', z'')) -> F(b, f(y'', z''))

Rules:

f(f(f(a, b), c), x) -> f(b, f(a, f(c, f(b, x))))
f(x, f(y, z)) -> f(f(x, y), z)

Strategy:

innermost

The following dependency pairs can be strictly oriented:

F(f(f(a, b), c), x) -> F(c, f(b, x))
F(f(f(a, b), c), f(y'', z'')) -> F(b, f(y'', z''))

The following usable rules for innermost w.r.t. to the AFS can be oriented:

f(f(f(a, b), c), x) -> f(b, f(a, f(c, f(b, x))))
f(x, f(y, z)) -> f(f(x, y), z)

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(c) = 0

POL(b) = 0

POL(a) = 1

POL(F(x₁, x₂)) = 1 + x₁ + x₂

POL(f(x₁, x₂)) = x₁ + x₂

resulting in one new DP problem.
Used Argument Filtering System:

F(x₁, x₂) -> F(x₁, x₂)
f(x₁, x₂) -> f(x₁, x₂)

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Nar

...

               →DP Problem 10

                 ↳Argument Filtering and Ordering

Dependency Pairs:

Rules:

f(f(f(a, b), c), x) -> f(b, f(a, f(c, f(b, x))))
f(x, f(y, z)) -> f(f(x, y), z)

Strategy:

innermost

The following dependency pairs can be strictly oriented:

F(f(f(a, b), c), f(f(y'', z''), z')) -> F(b, f(a, f(c, f(f(f(b, y''), z''), z'))))
F(f(f(a, b), c), f(y'', z'')) -> F(b, f(a, f(f(c, f(b, y'')), z'')))
F(f(f(a, b), c), f(y'', z'')) -> F(b, f(f(a, c), f(f(b, y''), z'')))
F(f(f(a, b), c), f(y', z')) -> F(b, f(a, f(f(f(c, b), y'), z')))
F(f(f(a, b), c), x''') -> F(b, f(f(a, f(c, b)), x'''))
F(f(f(a, b), c), f(y', z')) -> F(b, f(f(a, c), f(f(b, y'), z')))
F(f(f(a, b), c), x''') -> F(b, f(f(f(a, c), b), x'''))

The following usable rules for innermost w.r.t. to the AFS can be oriented:

f(f(f(a, b), c), x) -> f(b, f(a, f(c, f(b, x))))
f(x, f(y, z)) -> f(f(x, y), z)

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(b) = 0

POL(a) = 1

resulting in one new DP problem.
Used Argument Filtering System:

F(x₁, x₂) -> x₁
f(x₁, x₂) -> x₁

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Nar

...

               →DP Problem 11

                 ↳Narrowing Transformation

Dependency Pairs:

Rules:

f(f(f(a, b), c), x) -> f(b, f(a, f(c, f(b, x))))
f(x, f(y, z)) -> f(f(x, y), z)

Strategy:

innermost

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

F(f(f(a, b), c), f(y'', z'')) -> F(a, f(f(c, f(b, y'')), z''))

two new Dependency Pairs are created:

F(f(f(a, b), c), f(y''', z'')) -> F(a, f(f(f(c, b), y'''), z''))
F(f(f(a, b), c), f(f(y', z'), z'')) -> F(a, f(f(c, f(f(b, y'), z')), z''))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Nar

...

               →DP Problem 12

                 ↳Narrowing Transformation

Dependency Pairs:

F(f(f(a, b), c), f(f(y', z'), z'')) -> F(a, f(f(c, f(f(b, y'), z')), z''))
F(f(f(a, b), c), f(y''', z'')) -> F(a, f(f(f(c, b), y'''), z''))
F(f(f(a, b), c), f(f(y'''', z''''), z)) -> F(f(f(a, b), c), f(y'''', z''''))
F(f(f(a, b), c), f(f(y''', z'''), z)) -> F(f(f(a, b), c), f(y''', z'''))
F(f(f(a, b), c), f(y', z)) -> F(f(f(a, b), c), y')
F(f(f(a, b), c), f(f(y'', z''), z')) -> F(a, f(c, f(f(f(b, y''), z''), z')))
F(x'', f(f(y'', z''), z)) -> F(x'', f(y'', z''))
F(f(f(a, b), c), x'') -> F(a, f(f(c, b), x''))
F(x, f(y, z)) -> F(f(x, y), z)
F(f(f(a, b), c), f(f(f(y'''', z''''), z'0'), z)) -> F(f(f(a, b), c), f(f(y'''', z''''), z'0'))

Rules:

f(f(f(a, b), c), x) -> f(b, f(a, f(c, f(b, x))))
f(x, f(y, z)) -> f(f(x, y), z)

Strategy:

innermost

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

F(f(f(a, b), c), f(f(y'', z''), z')) -> F(a, f(c, f(f(f(b, y''), z''), z')))

two new Dependency Pairs are created:

F(f(f(a, b), c), f(f(y''', z'''), z'0)) -> F(a, f(f(c, f(f(b, y'''), z''')), z'0))
F(f(f(a, b), c), f(f(f(y', z0), z''), z')) -> F(a, f(c, f(f(f(f(b, y'), z0), z''), z')))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Nar

...

               →DP Problem 13

                 ↳Narrowing Transformation

Dependency Pairs:

F(f(f(a, b), c), f(f(f(y', z0), z''), z')) -> F(a, f(c, f(f(f(f(b, y'), z0), z''), z')))
F(f(f(a, b), c), f(f(y''', z'''), z'0)) -> F(a, f(f(c, f(f(b, y'''), z''')), z'0))
F(f(f(a, b), c), f(y''', z'')) -> F(a, f(f(f(c, b), y'''), z''))
F(f(f(a, b), c), f(f(f(y'''', z''''), z'0'), z)) -> F(f(f(a, b), c), f(f(y'''', z''''), z'0'))
F(f(f(a, b), c), f(f(y'''', z''''), z)) -> F(f(f(a, b), c), f(y'''', z''''))
F(f(f(a, b), c), f(f(y''', z'''), z)) -> F(f(f(a, b), c), f(y''', z'''))
F(f(f(a, b), c), f(y', z)) -> F(f(f(a, b), c), y')
F(x'', f(f(y'', z''), z)) -> F(x'', f(y'', z''))
F(f(f(a, b), c), x'') -> F(a, f(f(c, b), x''))
F(x, f(y, z)) -> F(f(x, y), z)
F(f(f(a, b), c), f(f(y', z'), z'')) -> F(a, f(f(c, f(f(b, y'), z')), z''))

Rules:

f(f(f(a, b), c), x) -> f(b, f(a, f(c, f(b, x))))
f(x, f(y, z)) -> f(f(x, y), z)

Strategy:

innermost

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

F(f(f(a, b), c), f(f(y', z'), z'')) -> F(a, f(f(c, f(f(b, y'), z')), z''))

two new Dependency Pairs are created:

F(f(f(a, b), c), f(f(y'', z'''), z'')) -> F(a, f(f(f(c, f(b, y'')), z'''), z''))
F(f(f(a, b), c), f(f(f(y'', z0), z'), z'')) -> F(a, f(f(c, f(f(f(b, y''), z0), z')), z''))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Nar

...

               →DP Problem 14

                 ↳Narrowing Transformation

Dependency Pairs:

F(f(f(a, b), c), f(f(f(y'', z0), z'), z'')) -> F(a, f(f(c, f(f(f(b, y''), z0), z')), z''))
F(f(f(a, b), c), f(f(y'', z'''), z'')) -> F(a, f(f(f(c, f(b, y'')), z'''), z''))
F(f(f(a, b), c), f(f(y''', z'''), z'0)) -> F(a, f(f(c, f(f(b, y'''), z''')), z'0))
F(f(f(a, b), c), f(y''', z'')) -> F(a, f(f(f(c, b), y'''), z''))
F(f(f(a, b), c), f(f(f(y'''', z''''), z'0'), z)) -> F(f(f(a, b), c), f(f(y'''', z''''), z'0'))
F(f(f(a, b), c), f(f(y'''', z''''), z)) -> F(f(f(a, b), c), f(y'''', z''''))
F(f(f(a, b), c), f(f(y''', z'''), z)) -> F(f(f(a, b), c), f(y''', z'''))
F(f(f(a, b), c), f(y', z)) -> F(f(f(a, b), c), y')
F(x'', f(f(y'', z''), z)) -> F(x'', f(y'', z''))
F(f(f(a, b), c), x'') -> F(a, f(f(c, b), x''))
F(x, f(y, z)) -> F(f(x, y), z)
F(f(f(a, b), c), f(f(f(y', z0), z''), z')) -> F(a, f(c, f(f(f(f(b, y'), z0), z''), z')))

Rules:

f(f(f(a, b), c), x) -> f(b, f(a, f(c, f(b, x))))
f(x, f(y, z)) -> f(f(x, y), z)

Strategy:

innermost

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

F(f(f(a, b), c), f(f(y''', z'''), z'0)) -> F(a, f(f(c, f(f(b, y'''), z''')), z'0))

two new Dependency Pairs are created:

F(f(f(a, b), c), f(f(y'''', z''''), z'0)) -> F(a, f(f(f(c, f(b, y'''')), z''''), z'0))
F(f(f(a, b), c), f(f(f(y', z'), z'''), z'0)) -> F(a, f(f(c, f(f(f(b, y'), z'), z''')), z'0))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Nar

...

               →DP Problem 15

                 ↳Narrowing Transformation

Dependency Pairs:

F(f(f(a, b), c), f(f(f(y', z'), z'''), z'0)) -> F(a, f(f(c, f(f(f(b, y'), z'), z''')), z'0))
F(f(f(a, b), c), f(f(y'''', z''''), z'0)) -> F(a, f(f(f(c, f(b, y'''')), z''''), z'0))
F(f(f(a, b), c), f(f(y'', z'''), z'')) -> F(a, f(f(f(c, f(b, y'')), z'''), z''))
F(f(f(a, b), c), f(f(f(y', z0), z''), z')) -> F(a, f(c, f(f(f(f(b, y'), z0), z''), z')))
F(f(f(a, b), c), f(y''', z'')) -> F(a, f(f(f(c, b), y'''), z''))
F(f(f(a, b), c), f(f(f(y'''', z''''), z'0'), z)) -> F(f(f(a, b), c), f(f(y'''', z''''), z'0'))
F(f(f(a, b), c), f(f(y'''', z''''), z)) -> F(f(f(a, b), c), f(y'''', z''''))
F(f(f(a, b), c), f(f(y''', z'''), z)) -> F(f(f(a, b), c), f(y''', z'''))
F(f(f(a, b), c), f(y', z)) -> F(f(f(a, b), c), y')
F(x'', f(f(y'', z''), z)) -> F(x'', f(y'', z''))
F(f(f(a, b), c), x'') -> F(a, f(f(c, b), x''))
F(x, f(y, z)) -> F(f(x, y), z)
F(f(f(a, b), c), f(f(f(y'', z0), z'), z'')) -> F(a, f(f(c, f(f(f(b, y''), z0), z')), z''))

Rules:

f(f(f(a, b), c), x) -> f(b, f(a, f(c, f(b, x))))
f(x, f(y, z)) -> f(f(x, y), z)

Strategy:

innermost

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

F(f(f(a, b), c), f(f(f(y', z0), z''), z')) -> F(a, f(c, f(f(f(f(b, y'), z0), z''), z')))

two new Dependency Pairs are created:

F(f(f(a, b), c), f(f(f(y'', z0'), z'''), z'0)) -> F(a, f(f(c, f(f(f(b, y''), z0'), z''')), z'0))
F(f(f(a, b), c), f(f(f(f(y'', z1), z0), z''), z')) -> F(a, f(c, f(f(f(f(f(b, y''), z1), z0), z''), z')))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Nar

...

               →DP Problem 16

                 ↳Narrowing Transformation

Dependency Pairs:

F(f(f(a, b), c), f(f(f(f(y'', z1), z0), z''), z')) -> F(a, f(c, f(f(f(f(f(b, y''), z1), z0), z''), z')))
F(f(f(a, b), c), f(f(f(y'', z0'), z'''), z'0)) -> F(a, f(f(c, f(f(f(b, y''), z0'), z''')), z'0))
F(f(f(a, b), c), f(f(y'''', z''''), z'0)) -> F(a, f(f(f(c, f(b, y'''')), z''''), z'0))
F(f(f(a, b), c), f(f(f(y'', z0), z'), z'')) -> F(a, f(f(c, f(f(f(b, y''), z0), z')), z''))
F(f(f(a, b), c), f(f(y'', z'''), z'')) -> F(a, f(f(f(c, f(b, y'')), z'''), z''))
F(f(f(a, b), c), f(y''', z'')) -> F(a, f(f(f(c, b), y'''), z''))
F(f(f(a, b), c), f(f(f(y'''', z''''), z'0'), z)) -> F(f(f(a, b), c), f(f(y'''', z''''), z'0'))
F(f(f(a, b), c), f(f(y'''', z''''), z)) -> F(f(f(a, b), c), f(y'''', z''''))
F(f(f(a, b), c), f(f(y''', z'''), z)) -> F(f(f(a, b), c), f(y''', z'''))
F(f(f(a, b), c), f(y', z)) -> F(f(f(a, b), c), y')
F(x'', f(f(y'', z''), z)) -> F(x'', f(y'', z''))
F(f(f(a, b), c), x'') -> F(a, f(f(c, b), x''))
F(x, f(y, z)) -> F(f(x, y), z)
F(f(f(a, b), c), f(f(f(y', z'), z'''), z'0)) -> F(a, f(f(c, f(f(f(b, y'), z'), z''')), z'0))

Rules:

f(f(f(a, b), c), x) -> f(b, f(a, f(c, f(b, x))))
f(x, f(y, z)) -> f(f(x, y), z)

Strategy:

innermost

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

F(f(f(a, b), c), f(f(y'', z'''), z'')) -> F(a, f(f(f(c, f(b, y'')), z'''), z''))

two new Dependency Pairs are created:

F(f(f(a, b), c), f(f(y''', z'''), z'')) -> F(a, f(f(f(f(c, b), y'''), z'''), z''))
F(f(f(a, b), c), f(f(f(y', z'), z'''), z'')) -> F(a, f(f(f(c, f(f(b, y'), z')), z'''), z''))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Nar

...

               →DP Problem 17

                 ↳Narrowing Transformation

Dependency Pairs:

F(f(f(a, b), c), f(f(f(y', z'), z'''), z'')) -> F(a, f(f(f(c, f(f(b, y'), z')), z'''), z''))
F(f(f(a, b), c), f(f(y''', z'''), z'')) -> F(a, f(f(f(f(c, b), y'''), z'''), z''))
F(f(f(a, b), c), f(f(f(y'', z0'), z'''), z'0)) -> F(a, f(f(c, f(f(f(b, y''), z0'), z''')), z'0))
F(f(f(a, b), c), f(f(f(y', z'), z'''), z'0)) -> F(a, f(f(c, f(f(f(b, y'), z'), z''')), z'0))
F(f(f(a, b), c), f(f(y'''', z''''), z'0)) -> F(a, f(f(f(c, f(b, y'''')), z''''), z'0))
F(f(f(a, b), c), f(f(f(y'', z0), z'), z'')) -> F(a, f(f(c, f(f(f(b, y''), z0), z')), z''))
F(f(f(a, b), c), f(y''', z'')) -> F(a, f(f(f(c, b), y'''), z''))
F(f(f(a, b), c), f(f(f(y'''', z''''), z'0'), z)) -> F(f(f(a, b), c), f(f(y'''', z''''), z'0'))
F(f(f(a, b), c), f(f(y'''', z''''), z)) -> F(f(f(a, b), c), f(y'''', z''''))
F(f(f(a, b), c), f(f(y''', z'''), z)) -> F(f(f(a, b), c), f(y''', z'''))
F(f(f(a, b), c), f(y', z)) -> F(f(f(a, b), c), y')
F(x'', f(f(y'', z''), z)) -> F(x'', f(y'', z''))
F(f(f(a, b), c), x'') -> F(a, f(f(c, b), x''))
F(x, f(y, z)) -> F(f(x, y), z)
F(f(f(a, b), c), f(f(f(f(y'', z1), z0), z''), z')) -> F(a, f(c, f(f(f(f(f(b, y''), z1), z0), z''), z')))

Rules:

f(f(f(a, b), c), x) -> f(b, f(a, f(c, f(b, x))))
f(x, f(y, z)) -> f(f(x, y), z)

Strategy:

innermost

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

F(f(f(a, b), c), f(f(f(y'', z0), z'), z'')) -> F(a, f(f(c, f(f(f(b, y''), z0), z')), z''))

two new Dependency Pairs are created:

F(f(f(a, b), c), f(f(f(y''', z0'), z'''), z'')) -> F(a, f(f(f(c, f(f(b, y'''), z0')), z'''), z''))
F(f(f(a, b), c), f(f(f(f(y', z1), z0), z'), z'')) -> F(a, f(f(c, f(f(f(f(b, y'), z1), z0), z')), z''))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Nar

...

               →DP Problem 18

                 ↳Narrowing Transformation

Dependency Pairs:

F(f(f(a, b), c), f(f(f(f(y', z1), z0), z'), z'')) -> F(a, f(f(c, f(f(f(f(b, y'), z1), z0), z')), z''))
F(f(f(a, b), c), f(f(f(y''', z0'), z'''), z'')) -> F(a, f(f(f(c, f(f(b, y'''), z0')), z'''), z''))
F(f(f(a, b), c), f(f(y''', z'''), z'')) -> F(a, f(f(f(f(c, b), y'''), z'''), z''))
F(f(f(a, b), c), f(f(f(f(y'', z1), z0), z''), z')) -> F(a, f(c, f(f(f(f(f(b, y''), z1), z0), z''), z')))
F(f(f(a, b), c), f(f(f(y'', z0'), z'''), z'0)) -> F(a, f(f(c, f(f(f(b, y''), z0'), z''')), z'0))
F(f(f(a, b), c), f(f(f(y', z'), z'''), z'0)) -> F(a, f(f(c, f(f(f(b, y'), z'), z''')), z'0))
F(f(f(a, b), c), f(f(y'''', z''''), z'0)) -> F(a, f(f(f(c, f(b, y'''')), z''''), z'0))
F(f(f(a, b), c), f(y''', z'')) -> F(a, f(f(f(c, b), y'''), z''))
F(f(f(a, b), c), f(f(f(y'''', z''''), z'0'), z)) -> F(f(f(a, b), c), f(f(y'''', z''''), z'0'))
F(f(f(a, b), c), f(f(y'''', z''''), z)) -> F(f(f(a, b), c), f(y'''', z''''))
F(f(f(a, b), c), f(f(y''', z'''), z)) -> F(f(f(a, b), c), f(y''', z'''))
F(f(f(a, b), c), f(y', z)) -> F(f(f(a, b), c), y')
F(x'', f(f(y'', z''), z)) -> F(x'', f(y'', z''))
F(f(f(a, b), c), x'') -> F(a, f(f(c, b), x''))
F(x, f(y, z)) -> F(f(x, y), z)
F(f(f(a, b), c), f(f(f(y', z'), z'''), z'')) -> F(a, f(f(f(c, f(f(b, y'), z')), z'''), z''))

Rules:

f(f(f(a, b), c), x) -> f(b, f(a, f(c, f(b, x))))
f(x, f(y, z)) -> f(f(x, y), z)

Strategy:

innermost

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

F(f(f(a, b), c), f(f(y'''', z''''), z'0)) -> F(a, f(f(f(c, f(b, y'''')), z''''), z'0))

two new Dependency Pairs are created:

F(f(f(a, b), c), f(f(y''''', z''''), z'0)) -> F(a, f(f(f(f(c, b), y'''''), z''''), z'0))
F(f(f(a, b), c), f(f(f(y', z'), z''''), z'0)) -> F(a, f(f(f(c, f(f(b, y'), z')), z''''), z'0))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Nar

...

               →DP Problem 19

                 ↳Narrowing Transformation

Dependency Pairs:

F(f(f(a, b), c), f(f(f(y', z'), z''''), z'0)) -> F(a, f(f(f(c, f(f(b, y'), z')), z''''), z'0))
F(f(f(a, b), c), f(f(y''''', z''''), z'0)) -> F(a, f(f(f(f(c, b), y'''''), z''''), z'0))
F(f(f(a, b), c), f(f(f(y''', z0'), z'''), z'')) -> F(a, f(f(f(c, f(f(b, y'''), z0')), z'''), z''))
F(f(f(a, b), c), f(f(f(y', z'), z'''), z'')) -> F(a, f(f(f(c, f(f(b, y'), z')), z'''), z''))
F(f(f(a, b), c), f(f(y''', z'''), z'')) -> F(a, f(f(f(f(c, b), y'''), z'''), z''))
F(f(f(a, b), c), f(f(f(f(y'', z1), z0), z''), z')) -> F(a, f(c, f(f(f(f(f(b, y''), z1), z0), z''), z')))
F(f(f(a, b), c), f(f(f(y'', z0'), z'''), z'0)) -> F(a, f(f(c, f(f(f(b, y''), z0'), z''')), z'0))
F(f(f(a, b), c), f(f(f(y', z'), z'''), z'0)) -> F(a, f(f(c, f(f(f(b, y'), z'), z''')), z'0))
F(f(f(a, b), c), f(y''', z'')) -> F(a, f(f(f(c, b), y'''), z''))
F(f(f(a, b), c), f(f(f(y'''', z''''), z'0'), z)) -> F(f(f(a, b), c), f(f(y'''', z''''), z'0'))
F(f(f(a, b), c), f(f(y'''', z''''), z)) -> F(f(f(a, b), c), f(y'''', z''''))
F(f(f(a, b), c), f(f(y''', z'''), z)) -> F(f(f(a, b), c), f(y''', z'''))
F(f(f(a, b), c), f(y', z)) -> F(f(f(a, b), c), y')
F(x'', f(f(y'', z''), z)) -> F(x'', f(y'', z''))
F(f(f(a, b), c), x'') -> F(a, f(f(c, b), x''))
F(x, f(y, z)) -> F(f(x, y), z)
F(f(f(a, b), c), f(f(f(f(y', z1), z0), z'), z'')) -> F(a, f(f(c, f(f(f(f(b, y'), z1), z0), z')), z''))

Rules:

f(f(f(a, b), c), x) -> f(b, f(a, f(c, f(b, x))))
f(x, f(y, z)) -> f(f(x, y), z)

Strategy:

innermost

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

F(f(f(a, b), c), f(f(f(y', z'), z'''), z'0)) -> F(a, f(f(c, f(f(f(b, y'), z'), z''')), z'0))

two new Dependency Pairs are created:

F(f(f(a, b), c), f(f(f(y'', z''), z''''), z'0)) -> F(a, f(f(f(c, f(f(b, y''), z'')), z''''), z'0))
F(f(f(a, b), c), f(f(f(f(y'', z''), z'), z'''), z'0)) -> F(a, f(f(c, f(f(f(f(b, y''), z''), z'), z''')), z'0))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Nar

...

               →DP Problem 20

                 ↳Narrowing Transformation

Dependency Pairs:

F(f(f(a, b), c), f(f(f(f(y'', z''), z'), z'''), z'0)) -> F(a, f(f(c, f(f(f(f(b, y''), z''), z'), z''')), z'0))
F(f(f(a, b), c), f(f(f(y'', z''), z''''), z'0)) -> F(a, f(f(f(c, f(f(b, y''), z'')), z''''), z'0))
F(f(f(a, b), c), f(f(y''''', z''''), z'0)) -> F(a, f(f(f(f(c, b), y'''''), z''''), z'0))
F(f(f(a, b), c), f(f(f(f(y', z1), z0), z'), z'')) -> F(a, f(f(c, f(f(f(f(b, y'), z1), z0), z')), z''))
F(f(f(a, b), c), f(f(f(y''', z0'), z'''), z'')) -> F(a, f(f(f(c, f(f(b, y'''), z0')), z'''), z''))
F(f(f(a, b), c), f(f(f(y', z'), z'''), z'')) -> F(a, f(f(f(c, f(f(b, y'), z')), z'''), z''))
F(f(f(a, b), c), f(f(y''', z'''), z'')) -> F(a, f(f(f(f(c, b), y'''), z'''), z''))
F(f(f(a, b), c), f(f(f(f(y'', z1), z0), z''), z')) -> F(a, f(c, f(f(f(f(f(b, y''), z1), z0), z''), z')))
F(f(f(a, b), c), f(f(f(y'', z0'), z'''), z'0)) -> F(a, f(f(c, f(f(f(b, y''), z0'), z''')), z'0))
F(f(f(a, b), c), f(y''', z'')) -> F(a, f(f(f(c, b), y'''), z''))
F(f(f(a, b), c), f(f(f(y'''', z''''), z'0'), z)) -> F(f(f(a, b), c), f(f(y'''', z''''), z'0'))
F(f(f(a, b), c), f(f(y'''', z''''), z)) -> F(f(f(a, b), c), f(y'''', z''''))
F(f(f(a, b), c), f(f(y''', z'''), z)) -> F(f(f(a, b), c), f(y''', z'''))
F(f(f(a, b), c), f(y', z)) -> F(f(f(a, b), c), y')
F(x'', f(f(y'', z''), z)) -> F(x'', f(y'', z''))
F(f(f(a, b), c), x'') -> F(a, f(f(c, b), x''))
F(x, f(y, z)) -> F(f(x, y), z)
F(f(f(a, b), c), f(f(f(y', z'), z''''), z'0)) -> F(a, f(f(f(c, f(f(b, y'), z')), z''''), z'0))

Rules:

f(f(f(a, b), c), x) -> f(b, f(a, f(c, f(b, x))))
f(x, f(y, z)) -> f(f(x, y), z)

Strategy:

innermost

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

F(f(f(a, b), c), f(f(f(y'', z0'), z'''), z'0)) -> F(a, f(f(c, f(f(f(b, y''), z0'), z''')), z'0))

two new Dependency Pairs are created:

F(f(f(a, b), c), f(f(f(y''', z0''), z''''), z'0)) -> F(a, f(f(f(c, f(f(b, y'''), z0'')), z''''), z'0))
F(f(f(a, b), c), f(f(f(f(y', z'), z0'), z'''), z'0)) -> F(a, f(f(c, f(f(f(f(b, y'), z'), z0'), z''')), z'0))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Nar

...

               →DP Problem 21

                 ↳Narrowing Transformation

Dependency Pairs:

F(f(f(a, b), c), f(f(f(f(y', z'), z0'), z'''), z'0)) -> F(a, f(f(c, f(f(f(f(b, y'), z'), z0'), z''')), z'0))
F(f(f(a, b), c), f(f(f(y''', z0''), z''''), z'0)) -> F(a, f(f(f(c, f(f(b, y'''), z0'')), z''''), z'0))
F(f(f(a, b), c), f(f(f(y'', z''), z''''), z'0)) -> F(a, f(f(f(c, f(f(b, y''), z'')), z''''), z'0))
F(f(f(a, b), c), f(f(f(y', z'), z''''), z'0)) -> F(a, f(f(f(c, f(f(b, y'), z')), z''''), z'0))
F(f(f(a, b), c), f(f(y''''', z''''), z'0)) -> F(a, f(f(f(f(c, b), y'''''), z''''), z'0))
F(f(f(a, b), c), f(f(f(f(y', z1), z0), z'), z'')) -> F(a, f(f(c, f(f(f(f(b, y'), z1), z0), z')), z''))
F(f(f(a, b), c), f(f(f(y''', z0'), z'''), z'')) -> F(a, f(f(f(c, f(f(b, y'''), z0')), z'''), z''))
F(f(f(a, b), c), f(f(f(y', z'), z'''), z'')) -> F(a, f(f(f(c, f(f(b, y'), z')), z'''), z''))
F(f(f(a, b), c), f(f(y''', z'''), z'')) -> F(a, f(f(f(f(c, b), y'''), z'''), z''))
F(f(f(a, b), c), f(f(f(f(y'', z1), z0), z''), z')) -> F(a, f(c, f(f(f(f(f(b, y''), z1), z0), z''), z')))
F(f(f(a, b), c), f(y''', z'')) -> F(a, f(f(f(c, b), y'''), z''))
F(f(f(a, b), c), f(f(f(y'''', z''''), z'0'), z)) -> F(f(f(a, b), c), f(f(y'''', z''''), z'0'))
F(f(f(a, b), c), f(f(y'''', z''''), z)) -> F(f(f(a, b), c), f(y'''', z''''))
F(f(f(a, b), c), f(f(y''', z'''), z)) -> F(f(f(a, b), c), f(y''', z'''))
F(f(f(a, b), c), f(y', z)) -> F(f(f(a, b), c), y')
F(x'', f(f(y'', z''), z)) -> F(x'', f(y'', z''))
F(f(f(a, b), c), x'') -> F(a, f(f(c, b), x''))
F(x, f(y, z)) -> F(f(x, y), z)
F(f(f(a, b), c), f(f(f(f(y'', z''), z'), z'''), z'0)) -> F(a, f(f(c, f(f(f(f(b, y''), z''), z'), z''')), z'0))

Rules:

f(f(f(a, b), c), x) -> f(b, f(a, f(c, f(b, x))))
f(x, f(y, z)) -> f(f(x, y), z)

Strategy:

innermost

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

F(f(f(a, b), c), f(f(f(f(y'', z1), z0), z''), z')) -> F(a, f(c, f(f(f(f(f(b, y''), z1), z0), z''), z')))

two new Dependency Pairs are created:

F(f(f(a, b), c), f(f(f(f(y''', z1'), z0'), z'''), z'0)) -> F(a, f(f(c, f(f(f(f(b, y'''), z1'), z0'), z''')), z'0))
F(f(f(a, b), c), f(f(f(f(f(y', z2), z1), z0), z''), z')) -> F(a, f(c, f(f(f(f(f(f(b, y'), z2), z1), z0), z''), z')))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Nar

...

               →DP Problem 22

                 ↳Remaining Obligation(s)

The following remains to be proven:
Dependency Pairs:

F(f(f(a, b), c), f(f(f(f(f(y', z2), z1), z0), z''), z')) -> F(a, f(c, f(f(f(f(f(f(b, y'), z2), z1), z0), z''), z')))
F(f(f(a, b), c), f(f(f(f(y''', z1'), z0'), z'''), z'0)) -> F(a, f(f(c, f(f(f(f(b, y'''), z1'), z0'), z''')), z'0))
F(f(f(a, b), c), f(f(f(y''', z0''), z''''), z'0)) -> F(a, f(f(f(c, f(f(b, y'''), z0'')), z''''), z'0))
F(f(f(a, b), c), f(f(f(f(y'', z''), z'), z'''), z'0)) -> F(a, f(f(c, f(f(f(f(b, y''), z''), z'), z''')), z'0))
F(f(f(a, b), c), f(f(f(y'', z''), z''''), z'0)) -> F(a, f(f(f(c, f(f(b, y''), z'')), z''''), z'0))
F(f(f(a, b), c), f(f(f(y', z'), z''''), z'0)) -> F(a, f(f(f(c, f(f(b, y'), z')), z''''), z'0))
F(f(f(a, b), c), f(f(y''''', z''''), z'0)) -> F(a, f(f(f(f(c, b), y'''''), z''''), z'0))
F(f(f(a, b), c), f(f(f(f(y', z1), z0), z'), z'')) -> F(a, f(f(c, f(f(f(f(b, y'), z1), z0), z')), z''))
F(f(f(a, b), c), f(f(f(y''', z0'), z'''), z'')) -> F(a, f(f(f(c, f(f(b, y'''), z0')), z'''), z''))
F(f(f(a, b), c), f(f(f(y', z'), z'''), z'')) -> F(a, f(f(f(c, f(f(b, y'), z')), z'''), z''))
F(f(f(a, b), c), f(f(y''', z'''), z'')) -> F(a, f(f(f(f(c, b), y'''), z'''), z''))
F(f(f(a, b), c), f(y''', z'')) -> F(a, f(f(f(c, b), y'''), z''))
F(f(f(a, b), c), f(f(f(y'''', z''''), z'0'), z)) -> F(f(f(a, b), c), f(f(y'''', z''''), z'0'))
F(f(f(a, b), c), f(f(y'''', z''''), z)) -> F(f(f(a, b), c), f(y'''', z''''))
F(f(f(a, b), c), f(f(y''', z'''), z)) -> F(f(f(a, b), c), f(y''', z'''))
F(f(f(a, b), c), f(y', z)) -> F(f(f(a, b), c), y')
F(x'', f(f(y'', z''), z)) -> F(x'', f(y'', z''))
F(f(f(a, b), c), x'') -> F(a, f(f(c, b), x''))
F(x, f(y, z)) -> F(f(x, y), z)
F(f(f(a, b), c), f(f(f(f(y', z'), z0'), z'''), z'0)) -> F(a, f(f(c, f(f(f(f(b, y'), z'), z0'), z''')), z'0))

Rules:

f(f(f(a, b), c), x) -> f(b, f(a, f(c, f(b, x))))
f(x, f(y, z)) -> f(f(x, y), z)

Strategy:

innermost

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

POL(c)	= 0
POL(b)	= 0
POL(a)	= 1
POL(F(x₁, x₂))	= 1 + x₁ + x₂
POL(f(x₁, x₂))	= x₁ + x₂