Term Rewriting System R:
[a, b, c, d]
f(f(f(f(j, a), b), c), d) -> f(f(a, b), f(f(a, d), c))

Termination of R to be shown.

`   R`
`     ↳Overlay and local confluence Check`

The TRS is overlay and locally confluent (all critical pairs are trivially joinable).Hence, we can switch to innermost.

`   R`
`     ↳OC`
`       →TRS2`
`         ↳Dependency Pair Analysis`

R contains the following Dependency Pairs:

F(f(f(f(j, a), b), c), d) -> F(f(a, b), f(f(a, d), c))
F(f(f(f(j, a), b), c), d) -> F(a, b)
F(f(f(f(j, a), b), c), d) -> F(f(a, d), c)
F(f(f(f(j, a), b), c), d) -> F(a, d)

Furthermore, R contains one SCC.

`   R`
`     ↳OC`
`       →TRS2`
`         ↳DPs`
`           →DP Problem 1`
`             ↳Remaining Obligation(s)`

The following remains to be proven:
Dependency Pairs:

F(f(f(f(j, a), b), c), d) -> F(a, d)
F(f(f(f(j, a), b), c), d) -> F(f(a, d), c)
F(f(f(f(j, a), b), c), d) -> F(a, b)
F(f(f(f(j, a), b), c), d) -> F(f(a, b), f(f(a, d), c))

Rule:

f(f(f(f(j, a), b), c), d) -> f(f(a, b), f(f(a, d), c))

Strategy:

innermost

The Proof could not be continued due to a Timeout.
Termination of R could not be shown.
Duration:
1:04 minutes