YES
TRS:
 {p(p(b(a(x0)), x1), p(x2, x3)) -> p(p(x3, a(x2)), p(b(a(x1)), b(x0)))}
 DP:
  Strict:
   {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))}
  Weak:
  {p(p(b(a(x0)), x1), p(x2, x3)) -> p(p(x3, a(x2)), 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)))}
   SCCS:
    Scc:
     {p#(p(b(a(x0)), x1), p(x2, x3)) -> p#(p(x3, a(x2)), p(b(a(x1)), b(x0)))}
    SCC:
     Strict:
      {p#(p(b(a(x0)), x1), p(x2, x3)) -> p#(p(x3, a(x2)), p(b(a(x1)), b(x0)))}
     Weak:
     {p(p(b(a(x0)), x1), p(x2, x3)) -> p(p(x3, a(x2)), p(b(a(x1)), b(x0)))}
     UR:
      {}
      BOUND:
       Bound: match(-raise)-bounded by 0
       Automaton:
        {     c_0() -> 2*
             b_0(5) -> 6*
             b_0(2) -> 7*
             a_0(9) -> 5*
             a_0(6) -> 9*
             a_0(3) -> 5*
             a_0(2) -> 5 | 3
         p#_0(4, 8) -> 1*
          p_0(7, 9) -> 4*
          p_0(6, 7) -> 8*
          p_0(2, 3) -> 4*}
       Strict:
        {}
       Qed