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

Proving termination of rewriting for pair3swap:

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

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

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

Polynomial Interpretation:

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

TIME: 3.22e-4

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

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

Polynomial Interpretation:

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

TIME: 1.0763e-2

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

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

Polynomial Interpretation:

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

TIME: 1.717e-3


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



Termination was proved succesfully.