MAYBE
Time: 0.018484
TRS:
 {p(a x0, p(a b x1, x2)) -> p(a b a x2, p(a a x1, x2))}
 DP:
  DP:
   {p#(a x0, p(a b x1, x2)) -> p#(a a x1, x2),
    p#(a x0, p(a b x1, x2)) -> p#(a b a x2, p(a a x1, x2))}
  TRS:
  {p(a x0, p(a b x1, x2)) -> p(a b a x2, p(a a x1, x2))}
  UR:
   {p(a x0, p(a b x1, x2)) -> p(a b a x2, p(a a x1, x2)),
                   c(x, y) -> x,
                   c(x, y) -> y}
   EDG:
    {(p#(a x0, p(a b x1, x2)) -> p#(a b a x2, p(a a x1, x2)), p#(a x0, p(a b x1, x2)) -> p#(a b a x2, p(a a x1, x2)))
     (p#(a x0, p(a b x1, x2)) -> p#(a b a x2, p(a a x1, x2)), p#(a x0, p(a b x1, x2)) -> p#(a a x1, x2))
     (p#(a x0, p(a b x1, x2)) -> p#(a a x1, x2), p#(a x0, p(a b x1, x2)) -> p#(a a x1, x2))
     (p#(a x0, p(a b x1, x2)) -> p#(a a x1, x2), p#(a x0, p(a b x1, x2)) -> p#(a b a x2, p(a a x1, x2)))}
    EDG:
     {(p#(a x0, p(a b x1, x2)) -> p#(a b a x2, p(a a x1, x2)), p#(a x0, p(a b x1, x2)) -> p#(a b a x2, p(a a x1, x2)))
      (p#(a x0, p(a b x1, x2)) -> p#(a b a x2, p(a a x1, x2)), p#(a x0, p(a b x1, x2)) -> p#(a a x1, x2))
      (p#(a x0, p(a b x1, x2)) -> p#(a a x1, x2), p#(a x0, p(a b x1, x2)) -> p#(a a x1, x2))
      (p#(a x0, p(a b x1, x2)) -> p#(a a x1, x2), p#(a x0, p(a b x1, x2)) -> p#(a b a x2, p(a a x1, x2)))}
     EDG:
      {(p#(a x0, p(a b x1, x2)) -> p#(a b a x2, p(a a x1, x2)), p#(a x0, p(a b x1, x2)) -> p#(a b a x2, p(a a x1, x2)))
       (p#(a x0, p(a b x1, x2)) -> p#(a b a x2, p(a a x1, x2)), p#(a x0, p(a b x1, x2)) -> p#(a a x1, x2))
       (p#(a x0, p(a b x1, x2)) -> p#(a a x1, x2), p#(a x0, p(a b x1, x2)) -> p#(a a x1, x2))
       (p#(a x0, p(a b x1, x2)) -> p#(a a x1, x2), p#(a x0, p(a b x1, x2)) -> p#(a b a x2, p(a a x1, x2)))}
      EDG:
       {(p#(a x0, p(a b x1, x2)) -> p#(a b a x2, p(a a x1, x2)), p#(a x0, p(a b x1, x2)) -> p#(a b a x2, p(a a x1, x2)))
        (p#(a x0, p(a b x1, x2)) -> p#(a b a x2, p(a a x1, x2)), p#(a x0, p(a b x1, x2)) -> p#(a a x1, x2))
        (p#(a x0, p(a b x1, x2)) -> p#(a a x1, x2), p#(a x0, p(a b x1, x2)) -> p#(a a x1, x2))
        (p#(a x0, p(a b x1, x2)) -> p#(a a x1, x2), p#(a x0, p(a b x1, x2)) -> p#(a b a x2, p(a a x1, x2)))}
       STATUS:
        arrows: 0.000000
        SCCS (1):
         Scc:
          {p#(a x0, p(a b x1, x2)) -> p#(a a x1, x2),
           p#(a x0, p(a b x1, x2)) -> p#(a b a x2, p(a a x1, x2))}
         
         SCC (2):
          Strict:
           {p#(a x0, p(a b x1, x2)) -> p#(a a x1, x2),
            p#(a x0, p(a b x1, x2)) -> p#(a b a x2, p(a a x1, x2))}
          Weak:
          {p(a x0, p(a b x1, x2)) -> p(a b a x2, p(a a x1, x2))}
          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 x0, p(a b x1, x2)) -> p#(a b a x2, p(a a x1, x2))
            1 + 1x2 + 0x1 + 0x0 >= 1 + 1x2 + 0x1
            p#(a x0, p(a b x1, x2)) -> p#(a a x1, x2)
            1 + 1x2 + 0x1 + 0x0 >= 0 + 1x2 + 0x1
           Weak:
            p(a x0, p(a b x1, x2)) -> p(a b a x2, p(a a x1, x2))
            2 + 1x2 + 0x1 + 0x0 >= 2 + 1x2 + 0x1
          SCCS (1):
           Scc:
            {p#(a x0, p(a b x1, x2)) -> p#(a b a x2, p(a a x1, x2))}
           
           SCC (1):
            Strict:
             {p#(a x0, p(a b x1, x2)) -> p#(a b a x2, p(a a x1, x2))}
            Weak:
            {p(a x0, p(a b x1, x2)) -> p(a b a x2, p(a a x1, x2))}
            Fail