YES
Time: 0.004278
TRS:
 {p(p(b a x0, x1), p(x2, x3)) -> p(p(x3, a x2), p(b a x1, b x0))}
 DP:
  DP:
   {p#(p(b a x0, x1), p(x2, x3)) -> p#(x3, a x2),
    p#(p(b a x0, x1), p(x2, x3)) -> p#(p(x3, a x2), p(b a x1, b x0)),
    p#(p(b a x0, x1), p(x2, x3)) -> p#(b a x1, b x0)}
  TRS:
  {p(p(b a x0, x1), p(x2, x3)) -> p(p(x3, a x2), p(b a x1, b x0))}
  EDG:
   {}
   STATUS:
    arrows: 1.000000
    SCCS (0):