YES
Time: 0.188663
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)-bounded by 1
      Automaton:
       {    b_1(4) -> 5*
            b_1(1) -> 6*
            b_0(1) -> 1*
            a_1(8) -> 4*
            a_1(5) -> 8*
            a_1(3) -> 9*
            a_1(2) -> 4*
            a_1(1) -> 4 | 2
            a_0(1) -> 1*
        p#_1(3, 7) -> 1*
        p#_0(1, 1) -> 1*
         p_1(7, 9) -> 3*
         p_1(6, 8) -> 3*
         p_1(5, 6) -> 7*
         p_1(3, 7) -> 1*
         p_1(1, 2) -> 3*
         p_0(1, 1) -> 1*}
      Strict:
       {}
      Qed