YES
Time: 0.098600
TRS:
 {p(p(b a x0, x1), p(x2, x3)) -> p(p(b x2, a a b x1), p(x3, x0))}
 DP:
  DP:
   {p#(p(b a x0, x1), p(x2, x3)) -> p#(x3, x0),
    p#(p(b a x0, x1), p(x2, x3)) -> p#(p(b x2, a a b x1), p(x3, x0)),
    p#(p(b a x0, x1), p(x2, x3)) -> p#(b x2, a a b x1)}
  TRS:
  {p(p(b a x0, x1), p(x2, x3)) -> p(p(b x2, a a b x1), p(x3, x0))}
  EDG:
   {(p#(p(b a x0, x1), p(x2, x3)) -> p#(p(b x2, a a b x1), p(x3, x0)), p#(p(b a x0, x1), p(x2, x3)) -> p#(b x2, a a b x1))
    (p#(p(b a x0, x1), p(x2, x3)) -> p#(p(b x2, a a b x1), p(x3, x0)), p#(p(b a x0, x1), p(x2, x3)) -> p#(p(b x2, a a b x1), p(x3, x0)))
    (p#(p(b a x0, x1), p(x2, x3)) -> p#(p(b x2, a a b x1), p(x3, x0)), p#(p(b a x0, x1), p(x2, x3)) -> p#(x3, x0))
    (p#(p(b a x0, x1), p(x2, x3)) -> p#(x3, x0), p#(p(b a x0, x1), p(x2, x3)) -> p#(x3, x0))
    (p#(p(b a x0, x1), p(x2, x3)) -> p#(x3, x0), p#(p(b a x0, x1), p(x2, x3)) -> p#(p(b x2, a a b x1), p(x3, x0)))
    (p#(p(b a x0, x1), p(x2, x3)) -> p#(x3, x0), p#(p(b a x0, x1), p(x2, x3)) -> p#(b x2, a a b x1))}
   SCCS (1):
    Scc:
     {p#(p(b a x0, x1), p(x2, x3)) -> p#(x3, x0),
      p#(p(b a x0, x1), p(x2, x3)) -> p#(p(b x2, a a b x1), p(x3, x0))}
    SCC (2):
     Strict:
      {p#(p(b a x0, x1), p(x2, x3)) -> p#(x3, x0),
       p#(p(b a x0, x1), p(x2, x3)) -> p#(p(b x2, a a b x1), p(x3, x0))}
     Weak:
     {p(p(b a x0, x1), p(x2, x3)) -> p(p(b x2, a a b x1), p(x3, x0))}
     POLY:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [p](x0, x1) = x0 + x1 + 1,
       
       [b](x0) = x0,
       
       [a](x0) = x0,
       
       [p#](x0, x1) = x0 + x1
      Strict:
       p#(p(b a x0, x1), p(x2, x3)) -> p#(p(b x2, a a b x1), p(x3, x0))
       2 + 1x2 + 1x1 + 1x3 + 1x0 >= 2 + 1x2 + 1x1 + 1x3 + 1x0
       p#(p(b a x0, x1), p(x2, x3)) -> p#(x3, x0)
       2 + 1x2 + 1x1 + 1x3 + 1x0 >= 0 + 1x3 + 1x0
      Weak:
       
     EDG:
      {(p#(p(b a x0, x1), p(x2, x3)) -> p#(p(b x2, a a b x1), p(x3, x0)), p#(p(b a x0, x1), p(x2, x3)) -> p#(p(b x2, a a b x1), p(x3, x0)))}
      SCCS (1):
       Scc:
        {p#(p(b a x0, x1), p(x2, x3)) -> p#(p(b x2, a a b x1), p(x3, x0))}
       SCC (1):
        Strict:
         {p#(p(b a x0, x1), p(x2, x3)) -> p#(p(b x2, a a b x1), p(x3, x0))}
        Weak:
        {p(p(b a x0, x1), p(x2, x3)) -> p(p(b x2, a a b x1), p(x3, x0))}
        BOUND:
         Bound: match(-raise)-bounded by 1
         Automaton:
          {    a_1(4) -> 5*
               a_1(3) -> 4*
               a_0(1) -> 1*
               b_1(7) -> 2*
               b_1(6) -> 2*
               b_1(5) -> 3*
               b_1(1) -> 3 | 2
               b_0(1) -> 1*
           p#_1(6, 7) -> 1*
           p#_0(1, 1) -> 1*
            p_1(7, 1) -> 7*
            p_1(6, 7) -> 7 | 1
            p_1(2, 5) -> 6*
            p_1(1, 1) -> 7*
            p_0(1, 1) -> 1*}
         Strict:
          {}
         Qed