YES
(VAR x0 x1 x2 x3)
(RULES 
p(a(x0),p(b(x1),p(a(x2),x3))) -> p(x2,p(a(a(x0)),p(b(x1),x3)))
)

Proving termination of rewriting for pair3rotate:

-> Dependency pairs:
nF_p(a(x0),p(b(x1),p(a(x2),x3))) -> nF_p(x2,p(a(a(x0)),p(b(x1),x3)))
nF_p(a(x0),p(b(x1),p(a(x2),x3))) -> nF_p(a(a(x0)),p(b(x1),x3))
nF_p(a(x0),p(b(x1),p(a(x2),x3))) -> nF_p(b(x1),x3)

-> Dependency pairs narrowed: 
nF_p(a(x0),p(b(x1),p(a(x2),x3))) -> nF_p(x2,p(a(a(x0)),p(b(x1),x3)))

-> New dependency pairs: 
nF_p(a(x0),p(b(x1),p(a(x2),p(a(x2),x3)))) -> nF_p(x2,p(x2,p(a(a(a(x0))),p(b(x1),x3))))

-> Proof of termination for pair3rotate_1:
-> -> Dependency pairs in cycle:
nF_p(a(x0),p(b(x1),p(a(x2),x3))) -> nF_p(a(a(x0)),p(b(x1),x3))
nF_p(a(x0),p(b(x1),p(a(x2),p(a(x2),x3)))) -> nF_p(x2,p(x2,p(a(a(a(x0))),p(b(x1),x3))))

UsableRules:
p(a(x0),p(b(x1),p(a(x2),x3))) -> p(x2,p(a(a(x0)),p(b(x1),x3)))

Polynomial Interpretation:

[p](X1,X2) = 2.X1 + 2.X2
[a](X) = 1/2.X + 2
[b](X) = 0
[nF_p](X1,X2) = 2.X1 + 2.X2

TIME: 1.773e-3

-> -> Dependency pairs in cycle:
nF_p(a(x0),p(b(x1),p(a(x2),x3))) -> nF_p(a(a(x0)),p(b(x1),x3))

UsableRules:
p(a(x0),p(b(x1),p(a(x2),x3))) -> p(x2,p(a(a(x0)),p(b(x1),x3)))

Polynomial Interpretation:

[p](X1,X2) = 2.X2 + 2
[a](X) = 0
[b](X) = 0
[nF_p](X1,X2) = 2.X2

TIME: 1.48e-4


SETTINGS:
Base ordering: Polynomial ordering
Proof mode: SCCs in DG + base ordering
Upper bound for coeffs: 2
Rationals below 1 for all non-replacing args: No
Polynomial interpretation: Linear
Coeffs in polynomials: All rationals
Delta: automatic



Termination was proved succesfully.