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)-DP-bounded by 1
       Automaton:
        {     b_1(23) -> 24*
              b_1(20) -> 25*
              b_1(19) -> 25*
              b_1(18) -> 25*
              b_1(17) -> 25*
              b_1(16) -> 25*
              b_1(12) -> 25*
              b_0(20) -> 16*
              b_0(19) -> 16*
              b_0(18) -> 16*
              b_0(17) -> 19*
              b_0(16) -> 16*
              b_0(12) -> 16*
              a_1(27) -> 23*
              a_1(24) -> 27*
              a_1(21) -> 23*
              a_1(19) -> 21*
              a_1(17) -> 23*
              a_0(20) -> 17*
              a_0(19) -> 17*
              a_0(18) -> 17*
              a_0(17) -> 17*
              a_0(16) -> 17*
              a_0(12) -> 17*
         p#_1(22, 26) -> 5*
         p#_0(18, 20) -> 5*
          p_1(25, 27) -> 22*
          p_1(24, 25) -> 26*
          p_1(19, 21) -> 22*
          p_1(16, 21) -> 22*
          p_0(20, 20) -> 12*
          p_0(20, 19) -> 12*
          p_0(20, 18) -> 12*
          p_0(20, 17) -> 18*
          p_0(20, 16) -> 12*
          p_0(20, 12) -> 12*
          p_0(19, 20) -> 12*
          p_0(19, 19) -> 20*
          p_0(19, 18) -> 12*
          p_0(19, 17) -> 18*
          p_0(19, 16) -> 20*
          p_0(19, 12) -> 12*
          p_0(18, 20) -> 12*
          p_0(18, 19) -> 12*
          p_0(18, 18) -> 12*
          p_0(18, 17) -> 18*
          p_0(18, 16) -> 12*
          p_0(18, 12) -> 12*
          p_0(17, 20) -> 12*
          p_0(17, 19) -> 12*
          p_0(17, 18) -> 12*
          p_0(17, 17) -> 18*
          p_0(17, 16) -> 12*
          p_0(17, 12) -> 12*
          p_0(16, 20) -> 12*
          p_0(16, 19) -> 12*
          p_0(16, 18) -> 12*
          p_0(16, 17) -> 18*
          p_0(16, 16) -> 12*
          p_0(16, 12) -> 12*
          p_0(12, 20) -> 12*
          p_0(12, 19) -> 12*
          p_0(12, 18) -> 12*
          p_0(12, 17) -> 18*
          p_0(12, 16) -> 12*
          p_0(12, 12) -> 12*}
       Strict:
        {}
       Qed