MAYBE
Time: 0.019916
TRS:
 {p(a a x0, p(x1, p(a x2, x3))) -> p(x2, p(a a b x1, p(a a x0, x3)))}
 DP:
  DP:
   {p#(a a x0, p(x1, p(a x2, x3))) -> p#(x2, p(a a b x1, p(a a x0, x3))),
    p#(a a x0, p(x1, p(a x2, x3))) -> p#(a a x0, x3),
    p#(a a x0, p(x1, p(a x2, x3))) -> p#(a a b x1, p(a a x0, x3))}
  TRS:
  {p(a a x0, p(x1, p(a x2, x3))) -> p(x2, p(a a b x1, p(a a x0, x3)))}
  EDG:
   {(p#(a a x0, p(x1, p(a x2, x3))) -> p#(a a b x1, p(a a x0, x3)), p#(a a x0, p(x1, p(a x2, x3))) -> p#(a a b x1, p(a a x0, x3)))
    (p#(a a x0, p(x1, p(a x2, x3))) -> p#(a a b x1, p(a a x0, x3)), p#(a a x0, p(x1, p(a x2, x3))) -> p#(a a x0, x3))
    (p#(a a x0, p(x1, p(a x2, x3))) -> p#(a a b x1, p(a a x0, x3)), p#(a a x0, p(x1, p(a x2, x3))) -> p#(x2, p(a a b x1, p(a a x0, x3))))
    (p#(a a x0, p(x1, p(a x2, x3))) -> p#(a a x0, x3), p#(a a x0, p(x1, p(a x2, x3))) -> p#(x2, p(a a b x1, p(a a x0, x3))))
    (p#(a a x0, p(x1, p(a x2, x3))) -> p#(a a x0, x3), p#(a a x0, p(x1, p(a x2, x3))) -> p#(a a x0, x3))
    (p#(a a x0, p(x1, p(a x2, x3))) -> p#(a a x0, x3), p#(a a x0, p(x1, p(a x2, x3))) -> p#(a a b x1, p(a a x0, x3)))
    (p#(a a x0, p(x1, p(a x2, x3))) -> p#(x2, p(a a b x1, p(a a x0, x3))), p#(a a x0, p(x1, p(a x2, x3))) -> p#(x2, p(a a b x1, p(a a x0, x3))))
    (p#(a a x0, p(x1, p(a x2, x3))) -> p#(x2, p(a a b x1, p(a a x0, x3))), p#(a a x0, p(x1, p(a x2, x3))) -> p#(a a x0, x3))
    (p#(a a x0, p(x1, p(a x2, x3))) -> p#(x2, p(a a b x1, p(a a x0, x3))), p#(a a x0, p(x1, p(a x2, x3))) -> p#(a a b x1, p(a a x0, x3)))}
   SCCS (1):
    Scc:
     {p#(a a x0, p(x1, p(a x2, x3))) -> p#(x2, p(a a b x1, p(a a x0, x3))),
      p#(a a x0, p(x1, p(a x2, x3))) -> p#(a a x0, x3),
      p#(a a x0, p(x1, p(a x2, x3))) -> p#(a a b x1, p(a a x0, x3))}
    SCC (3):
     Strict:
      {p#(a a x0, p(x1, p(a x2, x3))) -> p#(x2, p(a a b x1, p(a a x0, x3))),
       p#(a a x0, p(x1, p(a x2, x3))) -> p#(a a x0, x3),
       p#(a a x0, p(x1, p(a x2, x3))) -> p#(a a b x1, p(a a x0, x3))}
     Weak:
     {p(a a x0, p(x1, p(a x2, x3))) -> p(x2, p(a a b x1, p(a a x0, x3)))}
     POLY:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [p](x0, x1) = x0 + 1,
       
       [a](x0) = 0,
       
       [b](x0) = 0,
       
       [p#](x0, x1) = x0
      Strict:
       p#(a a x0, p(x1, p(a x2, x3))) -> p#(a a b x1, p(a a x0, x3))
       2 + 0x2 + 0x1 + 0x0 + 1x3 >= 1 + 0x1 + 0x0 + 1x3
       p#(a a x0, p(x1, p(a x2, x3))) -> p#(a a x0, x3)
       2 + 0x2 + 0x1 + 0x0 + 1x3 >= 0 + 0x0 + 1x3
       p#(a a x0, p(x1, p(a x2, x3))) -> p#(x2, p(a a b x1, p(a a x0, x3)))
       2 + 0x2 + 0x1 + 0x0 + 1x3 >= 2 + 0x2 + 0x1 + 0x0 + 1x3
      Weak:
       
     EDG:
      {(p#(a a x0, p(x1, p(a x2, x3))) -> p#(x2, p(a a b x1, p(a a x0, x3))), p#(a a x0, p(x1, p(a x2, x3))) -> p#(x2, p(a a b x1, p(a a x0, x3))))}
      SCCS (1):
       Scc:
        {p#(a a x0, p(x1, p(a x2, x3))) -> p#(x2, p(a a b x1, p(a a x0, x3)))}
       SCC (1):
        Strict:
         {p#(a a x0, p(x1, p(a x2, x3))) -> p#(x2, p(a a b x1, p(a a x0, x3)))}
        Weak:
        {p(a a x0, p(x1, p(a x2, x3))) -> p(x2, p(a a b x1, p(a a x0, x3)))}
        Fail