YES(?,O(n^1))
TRS:
 {p(p(b a x0, x1), p(x2, x3)) -> p(p(b x2, a a b x1), p(x3, x0))}
 DUP: We consider a non-duplicating system.
  Trs:
   {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(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