TIMEOUT

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (53ms).
 | – Problem 2 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (11ms), PolynomialLinearRange4iUR (1334ms), DependencyGraph (7ms), PolynomialLinearRange8NegiUR (12144ms), DependencyGraph (10ms), ReductionPairSAT (timeout)].

The following open problems remain:

Open Dependency Pair Problem 2

Dependency Pairs

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

Rewrite Rules

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

Original Signature

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

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

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

Original Signature

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

Strategy

The following SCCs where found

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