TIMEOUT

The TRS could not be proven terminating. The proof attempt took 60020 ms.

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (54ms).
 | – Problem 2 was processed with processor PolynomialLinearRange4iUR (3574ms).
 |    | – Problem 3 remains open; application of the following processors failed [DependencyGraph (3ms), PolynomialLinearRange4iUR (2298ms), DependencyGraph (3ms), PolynomialLinearRange8NegiUR (timeout), DependencyGraph (4ms), ReductionPairSAT (timeout)].

The following open problems remain:

Open Dependency Pair Problem 3

Dependency Pairs

f#(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) → f#(a, f(a, f(a, f(b, x))))f#(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) → f#(a, f(a, f(b, x)))
f#(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) → f#(a, f(a, f(b, f(a, f(a, f(a, f(b, x)))))))

Rewrite Rules

f(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) → f(a, f(b, f(a, f(a, f(b, f(a, f(a, f(a, f(b, x)))))))))

Original Signature

Termination of terms over the following signature is verified: f, b, a

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

f#(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) → f#(a, f(a, f(a, f(b, x))))f#(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) → f#(a, f(b, x))
f#(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) → f#(a, f(b, f(a, f(a, f(b, f(a, f(a, f(a, f(b, x)))))))))f#(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) → f#(a, f(a, f(b, x)))
f#(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) → f#(b, f(a, f(a, f(b, f(a, f(a, f(a, f(b, x))))))))f#(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) → f#(a, f(a, f(b, f(a, f(a, f(a, f(b, x)))))))
f#(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) → f#(b, x)f#(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) → f#(b, f(a, f(a, f(a, f(b, x)))))
f#(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) → f#(a, f(b, f(a, f(a, f(a, f(b, x))))))

Rewrite Rules

f(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) → f(a, f(b, f(a, f(a, f(b, f(a, f(a, f(a, f(b, x)))))))))

Original Signature

Termination of terms over the following signature is verified: f, b, a

Strategy

The following SCCs where found

f#(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) → f#(a, f(a, f(a, f(b, x))))f#(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) → f#(a, f(b, x))
f#(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) → f#(a, f(b, f(a, f(a, f(b, f(a, f(a, f(a, f(b, x)))))))))f#(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) → f#(a, f(a, f(b, x)))
f#(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) → f#(a, f(a, f(b, f(a, f(a, f(a, f(b, x)))))))f#(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) → f#(a, f(b, f(a, f(a, f(a, f(b, x))))))

Problem 2: PolynomialLinearRange4iUR

Dependency Pair Problem

Dependency Pairs

f#(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) → f#(a, f(a, f(a, f(b, x))))f#(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) → f#(a, f(b, x))
f#(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) → f#(a, f(b, f(a, f(a, f(b, f(a, f(a, f(a, f(b, x)))))))))f#(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) → f#(a, f(a, f(b, x)))
f#(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) → f#(a, f(a, f(b, f(a, f(a, f(a, f(b, x)))))))f#(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) → f#(a, f(b, f(a, f(a, f(a, f(b, x))))))

Rewrite Rules

f(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) → f(a, f(b, f(a, f(a, f(b, f(a, f(a, f(a, f(b, x)))))))))

Original Signature

Termination of terms over the following signature is verified: f, b, a

Strategy

Polynomial Interpretation

Improved Usable rules

f(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) → f(a, f(b, f(a, f(a, f(b, f(a, f(a, f(a, f(b, x)))))))))

The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:

f#(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) → f#(a, f(b, x))f#(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) → f#(a, f(b, f(a, f(a, f(b, f(a, f(a, f(a, f(b, x)))))))))
f#(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) → f#(a, f(b, f(a, f(a, f(a, f(b, x))))))