Termination w.r.t. Q of the given QTRS could not be shown:

(0) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

p(a(x0), p(a(a(a(x1))), x2)) → p(a(x2), p(a(a(b(x0))), x2))

Q is empty.