YES
Time: 3.387626
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:
   {(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 (1):
    Scc:
     {p#(p(b a x0, x1), p(x2, x3)) -> p#(p(x3, a x2), p(b a x1, b x0))}
    SCC (1):
     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))}
     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) -> 18*
             b_0(16) -> 16*
             b_0(12) -> 16*
             a_1(27) -> 23*
             a_1(24) -> 27*
             a_1(21) -> 23*
             a_1(18) -> 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(19, 20) -> 5*
         p_1(25, 27) -> 22*
         p_1(24, 25) -> 26*
         p_1(18, 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) -> 19*
         p_0(20, 16) -> 12*
         p_0(20, 12) -> 12*
         p_0(19, 20) -> 12*
         p_0(19, 19) -> 12*
         p_0(19, 18) -> 12*
         p_0(19, 17) -> 19*
         p_0(19, 16) -> 12*
         p_0(19, 12) -> 12*
         p_0(18, 20) -> 12*
         p_0(18, 19) -> 12*
         p_0(18, 18) -> 20*
         p_0(18, 17) -> 19*
         p_0(18, 16) -> 20*
         p_0(18, 12) -> 12*
         p_0(17, 20) -> 12*
         p_0(17, 19) -> 12*
         p_0(17, 18) -> 12*
         p_0(17, 17) -> 19*
         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) -> 19*
         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) -> 19*
         p_0(12, 16) -> 12*
         p_0(12, 12) -> 12*}
      Strict:
       {}
      Qed