YES
Time: 0.004349
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))}
  UR:
   {}
   EDG:
    {(p#(p(b a x0, x1), p(x2, x3)) -> p#(x3, a x2), p#(p(b a x0, x1), p(x2, x3)) -> p#(b a x1, b x0))
     (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#(x3, a x2), p#(p(b a x0, x1), p(x2, x3)) -> p#(x3, a x2))
     (p#(p(b a x0, x1), p(x2, x3)) -> p#(b a x1, b x0), p#(p(b a x0, x1), p(x2, x3)) -> p#(x3, a x2))
     (p#(p(b a x0, x1), p(x2, x3)) -> p#(b a x1, b x0), 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), p#(p(b a x0, x1), p(x2, x3)) -> p#(b a x1, b x0))
     (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#(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#(p(x3, a x2), p(b a x1, b x0)))
     (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))}
    EDG:
     {(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#(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#(p(x3, a x2), p(b a x1, b x0)))
      (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))}
     EDG:
      {}
      EDG:
       {}
       STATUS:
        arrows: 1.000000
        SCCS (0):