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(p(b(a(x0)), x1), p(x2, x3)) → p(p(x3, a(x2)), p(b(a(x1)), b(x0)))

Q is empty.