MAYBE
Time: 0.040864
TRS:
 {a(1(), x) -> c b x,
  a(0(), x) -> c c x,
  b c b c x -> a(0(), a(1(), x)),
  c c c b x -> a(1(), b c x)}
 DP:
  DP:
   {a#(1(), x) -> b# x,
    a#(1(), x) -> c# b x,
    a#(0(), x) -> c# x,
    a#(0(), x) -> c# c x,
    b# c b c x -> a#(1(), x),
    b# c b c x -> a#(0(), a(1(), x)),
    c# c c b x -> a#(1(), b c x),
    c# c c b x -> b# c x,
    c# c c b x -> c# x}
  TRS:
  {a(1(), x) -> c b x,
   a(0(), x) -> c c x,
   b c b c x -> a(0(), a(1(), x)),
   c c c b x -> a(1(), b c x)}
  UR:
   {a(1(), x) -> c b x,
    a(0(), x) -> c c x,
    b c b c x -> a(0(), a(1(), x)),
    c c c b x -> a(1(), b c x)}
   EDG:
    {(a#(0(), x) -> c# x, c# c c b x -> c# x)
     (a#(0(), x) -> c# x, c# c c b x -> b# c x)
     (a#(0(), x) -> c# x, c# c c b x -> a#(1(), b c x))
     (a#(1(), x) -> c# b x, c# c c b x -> c# x)
     (a#(1(), x) -> c# b x, c# c c b x -> b# c x)
     (a#(1(), x) -> c# b x, c# c c b x -> a#(1(), b c x))
     (c# c c b x -> a#(1(), b c x), a#(0(), x) -> c# c x)
     (c# c c b x -> a#(1(), b c x), a#(0(), x) -> c# x)
     (c# c c b x -> a#(1(), b c x), a#(1(), x) -> c# b x)
     (c# c c b x -> a#(1(), b c x), a#(1(), x) -> b# x)
     (b# c b c x -> a#(0(), a(1(), x)), a#(0(), x) -> c# c x)
     (b# c b c x -> a#(0(), a(1(), x)), a#(0(), x) -> c# x)
     (b# c b c x -> a#(0(), a(1(), x)), a#(1(), x) -> c# b x)
     (b# c b c x -> a#(0(), a(1(), x)), a#(1(), x) -> b# x)
     (b# c b c x -> a#(1(), x), a#(1(), x) -> b# x)
     (b# c b c x -> a#(1(), x), a#(1(), x) -> c# b x)
     (b# c b c x -> a#(1(), x), a#(0(), x) -> c# x)
     (b# c b c x -> a#(1(), x), a#(0(), x) -> c# c x)
     (c# c c b x -> b# c x, b# c b c x -> a#(1(), x))
     (c# c c b x -> b# c x, b# c b c x -> a#(0(), a(1(), x)))
     (a#(0(), x) -> c# c x, c# c c b x -> a#(1(), b c x))
     (a#(0(), x) -> c# c x, c# c c b x -> b# c x)
     (a#(0(), x) -> c# c x, c# c c b x -> c# x)
     (c# c c b x -> c# x, c# c c b x -> a#(1(), b c x))
     (c# c c b x -> c# x, c# c c b x -> b# c x)
     (c# c c b x -> c# x, c# c c b x -> c# x)
     (a#(1(), x) -> b# x, b# c b c x -> a#(1(), x))
     (a#(1(), x) -> b# x, b# c b c x -> a#(0(), a(1(), x)))}
    STATUS:
     arrows: 0.654321
     SCCS (1):
      Scc:
       {a#(1(), x) -> b# x,
        a#(1(), x) -> c# b x,
        a#(0(), x) -> c# x,
        a#(0(), x) -> c# c x,
        b# c b c x -> a#(1(), x),
        b# c b c x -> a#(0(), a(1(), x)),
        c# c c b x -> a#(1(), b c x),
        c# c c b x -> b# c x,
        c# c c b x -> c# x}
      
      SCC (9):
       Strict:
        {a#(1(), x) -> b# x,
         a#(1(), x) -> c# b x,
         a#(0(), x) -> c# x,
         a#(0(), x) -> c# c x,
         b# c b c x -> a#(1(), x),
         b# c b c x -> a#(0(), a(1(), x)),
         c# c c b x -> a#(1(), b c x),
         c# c c b x -> b# c x,
         c# c c b x -> c# x}
       Weak:
       {a(1(), x) -> c b x,
        a(0(), x) -> c c x,
        b c b c x -> a(0(), a(1(), x)),
        c c c b x -> a(1(), b c x)}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [a](x0, x1) = x0 + x1 + 1,
         
         [b](x0) = x0 + 1,
         
         [c](x0) = x0 + 1,
         
         [1] = 1,
         
         [0] = 1,
         
         [a#](x0, x1) = x0 + x1,
         
         [b#](x0) = x0,
         
         [c#](x0) = x0
        Strict:
         c# c c b x -> c# x
         3 + 1x >= 0 + 1x
         c# c c b x -> b# c x
         3 + 1x >= 1 + 1x
         c# c c b x -> a#(1(), b c x)
         3 + 1x >= 3 + 1x
         b# c b c x -> a#(0(), a(1(), x))
         3 + 1x >= 3 + 1x
         b# c b c x -> a#(1(), x)
         3 + 1x >= 1 + 1x
         a#(0(), x) -> c# c x
         1 + 1x >= 1 + 1x
         a#(0(), x) -> c# x
         1 + 1x >= 0 + 1x
         a#(1(), x) -> c# b x
         1 + 1x >= 1 + 1x
         a#(1(), x) -> b# x
         1 + 1x >= 0 + 1x
        Weak:
         c c c b x -> a(1(), b c x)
         4 + 1x >= 4 + 1x
         b c b c x -> a(0(), a(1(), x))
         4 + 1x >= 4 + 1x
         a(0(), x) -> c c x
         2 + 1x >= 2 + 1x
         a(1(), x) -> c b x
         2 + 1x >= 2 + 1x
       SCCS (1):
        Scc:
         {a#(1(), x) -> c# b x,
          a#(0(), x) -> c# c x,
          c# c c b x -> a#(1(), b c x)}
        
        
        SCC (3):
         Strict:
          {a#(1(), x) -> c# b x,
           a#(0(), x) -> c# c x,
           c# c c b x -> a#(1(), b c x)}
         Weak:
         {a(1(), x) -> c b x,
          a(0(), x) -> c c x,
          b c b c x -> a(0(), a(1(), x)),
          c c c b x -> a(1(), b c x)}
         POLY:
          Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
          Interpretation:
           [a](x0, x1) = 0,
           
           [b](x0) = 0,
           
           [c](x0) = 0,
           
           [1] = 0,
           
           [0] = 1,
           
           [a#](x0, x1) = x0,
           
           [c#](x0) = 0
          Strict:
           c# c c b x -> a#(1(), b c x)
           0 + 0x >= 0 + 0x
           a#(0(), x) -> c# c x
           1 + 0x >= 0 + 0x
           a#(1(), x) -> c# b x
           0 + 0x >= 0 + 0x
          Weak:
           c c c b x -> a(1(), b c x)
           0 + 0x >= 0 + 0x
           b c b c x -> a(0(), a(1(), x))
           0 + 0x >= 0 + 0x
           a(0(), x) -> c c x
           0 + 0x >= 0 + 0x
           a(1(), x) -> c b x
           0 + 0x >= 0 + 0x
         SCCS (1):
          Scc:
           {a#(1(), x) -> c# b x,
            c# c c b x -> a#(1(), b c x)}
          
          SCC (2):
           Strict:
            {a#(1(), x) -> c# b x,
             c# c c b x -> a#(1(), b c x)}
           Weak:
           {a(1(), x) -> c b x,
            a(0(), x) -> c c x,
            b c b c x -> a(0(), a(1(), x)),
            c c c b x -> a(1(), b c x)}
           Fail