YES

The TRS could be proven terminating. The proof took 55 ms.

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (6ms).

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

p#(f(f(x))) → q#(f(g(x)))q#(f(f(x))) → p#(f(g(x)))
q#(g(g(x))) → p#(g(f(x)))p#(g(g(x))) → q#(g(f(x)))

Rewrite Rules

p(f(f(x))) → q(f(g(x)))p(g(g(x))) → q(g(f(x)))
q(f(f(x))) → p(f(g(x)))q(g(g(x))) → p(g(f(x)))

Original Signature

Termination of terms over the following signature is verified: f, g, q, p

Strategy

There are no SCCs!