MAYBE
TRS:
 {b(0(), a(1(), a(x, y))) -> b(1(), a(0(), a(x, y))),
                a(0(), x) -> b(0(), b(0(), x)),
        a(0(), b(0(), x)) -> b(0(), a(0(), x)),
          a(0(), a(x, y)) -> a(1(), a(1(), a(x, y))),
  a(0(), a(1(), a(x, y))) -> a(1(), a(0(), a(x, y)))}
 DP:
  Strict:
   {b#(0(), a(1(), a(x, y))) -> b#(1(), a(0(), a(x, y))),
    b#(0(), a(1(), a(x, y))) -> a#(0(), a(x, y)),
                  a#(0(), x) -> b#(0(), x),
                  a#(0(), x) -> b#(0(), b(0(), x)),
          a#(0(), b(0(), x)) -> b#(0(), a(0(), x)),
          a#(0(), b(0(), x)) -> a#(0(), x),
            a#(0(), a(x, y)) -> a#(1(), a(x, y)),
            a#(0(), a(x, y)) -> a#(1(), a(1(), a(x, y))),
    a#(0(), a(1(), a(x, y))) -> a#(0(), a(x, y)),
    a#(0(), a(1(), a(x, y))) -> a#(1(), a(0(), a(x, y)))}
  Weak:
  {b(0(), a(1(), a(x, y))) -> b(1(), a(0(), a(x, y))),
                 a(0(), x) -> b(0(), b(0(), x)),
         a(0(), b(0(), x)) -> b(0(), a(0(), x)),
           a(0(), a(x, y)) -> a(1(), a(1(), a(x, y))),
   a(0(), a(1(), a(x, y))) -> a(1(), a(0(), a(x, y)))}
  EDG:
   {(a#(0(), x) -> b#(0(), x), b#(0(), a(1(), a(x, y))) -> a#(0(), a(x, y)))
    (a#(0(), x) -> b#(0(), x), b#(0(), a(1(), a(x, y))) -> b#(1(), a(0(), a(x, y))))
    (a#(0(), b(0(), x)) -> b#(0(), a(0(), x)), b#(0(), a(1(), a(x, y))) -> a#(0(), a(x, y)))
    (a#(0(), b(0(), x)) -> b#(0(), a(0(), x)), b#(0(), a(1(), a(x, y))) -> b#(1(), a(0(), a(x, y))))
    (a#(0(), a(1(), a(x, y))) -> a#(0(), a(x, y)), a#(0(), x) -> b#(0(), x))
    (a#(0(), a(1(), a(x, y))) -> a#(0(), a(x, y)), a#(0(), x) -> b#(0(), b(0(), x)))
    (a#(0(), a(1(), a(x, y))) -> a#(0(), a(x, y)), a#(0(), b(0(), x)) -> b#(0(), a(0(), x)))
    (a#(0(), a(1(), a(x, y))) -> a#(0(), a(x, y)), a#(0(), b(0(), x)) -> a#(0(), x))
    (a#(0(), a(1(), a(x, y))) -> a#(0(), a(x, y)), a#(0(), a(x, y)) -> a#(1(), a(x, y)))
    (a#(0(), a(1(), a(x, y))) -> a#(0(), a(x, y)), a#(0(), a(x, y)) -> a#(1(), a(1(), a(x, y))))
    (a#(0(), a(1(), a(x, y))) -> a#(0(), a(x, y)), a#(0(), a(1(), a(x, y))) -> a#(0(), a(x, y)))
    (a#(0(), a(1(), a(x, y))) -> a#(0(), a(x, y)), a#(0(), a(1(), a(x, y))) -> a#(1(), a(0(), a(x, y))))
    (a#(0(), b(0(), x)) -> a#(0(), x), a#(0(), x) -> b#(0(), x))
    (a#(0(), b(0(), x)) -> a#(0(), x), a#(0(), x) -> b#(0(), b(0(), x)))
    (a#(0(), b(0(), x)) -> a#(0(), x), a#(0(), b(0(), x)) -> b#(0(), a(0(), x)))
    (a#(0(), b(0(), x)) -> a#(0(), x), a#(0(), b(0(), x)) -> a#(0(), x))
    (a#(0(), b(0(), x)) -> a#(0(), x), a#(0(), a(x, y)) -> a#(1(), a(x, y)))
    (a#(0(), b(0(), x)) -> a#(0(), x), a#(0(), a(x, y)) -> a#(1(), a(1(), a(x, y))))
    (a#(0(), b(0(), x)) -> a#(0(), x), a#(0(), a(1(), a(x, y))) -> a#(0(), a(x, y)))
    (a#(0(), b(0(), x)) -> a#(0(), x), a#(0(), a(1(), a(x, y))) -> a#(1(), a(0(), a(x, y))))
    (a#(0(), x) -> b#(0(), b(0(), x)), b#(0(), a(1(), a(x, y))) -> b#(1(), a(0(), a(x, y))))
    (a#(0(), x) -> b#(0(), b(0(), x)), b#(0(), a(1(), a(x, y))) -> a#(0(), a(x, y)))
    (b#(0(), a(1(), a(x, y))) -> a#(0(), a(x, y)), a#(0(), x) -> b#(0(), x))
    (b#(0(), a(1(), a(x, y))) -> a#(0(), a(x, y)), a#(0(), x) -> b#(0(), b(0(), x)))
    (b#(0(), a(1(), a(x, y))) -> a#(0(), a(x, y)), a#(0(), b(0(), x)) -> b#(0(), a(0(), x)))
    (b#(0(), a(1(), a(x, y))) -> a#(0(), a(x, y)), a#(0(), b(0(), x)) -> a#(0(), x))
    (b#(0(), a(1(), a(x, y))) -> a#(0(), a(x, y)), a#(0(), a(x, y)) -> a#(1(), a(x, y)))
    (b#(0(), a(1(), a(x, y))) -> a#(0(), a(x, y)), a#(0(), a(x, y)) -> a#(1(), a(1(), a(x, y))))
    (b#(0(), a(1(), a(x, y))) -> a#(0(), a(x, y)), a#(0(), a(1(), a(x, y))) -> a#(0(), a(x, y)))
    (b#(0(), a(1(), a(x, y))) -> a#(0(), a(x, y)), a#(0(), a(1(), a(x, y))) -> a#(1(), a(0(), a(x, y))))}
   SCCS:
    Scc:
     {b#(0(), a(1(), a(x, y))) -> a#(0(), a(x, y)),
                    a#(0(), x) -> b#(0(), x),
                    a#(0(), x) -> b#(0(), b(0(), x)),
            a#(0(), b(0(), x)) -> b#(0(), a(0(), x)),
            a#(0(), b(0(), x)) -> a#(0(), x),
      a#(0(), a(1(), a(x, y))) -> a#(0(), a(x, y))}
    SCC:
     Strict:
      {b#(0(), a(1(), a(x, y))) -> a#(0(), a(x, y)),
                     a#(0(), x) -> b#(0(), x),
                     a#(0(), x) -> b#(0(), b(0(), x)),
             a#(0(), b(0(), x)) -> b#(0(), a(0(), x)),
             a#(0(), b(0(), x)) -> a#(0(), x),
       a#(0(), a(1(), a(x, y))) -> a#(0(), a(x, y))}
     Weak:
     {b(0(), a(1(), a(x, y))) -> b(1(), a(0(), a(x, y))),
                    a(0(), x) -> b(0(), b(0(), x)),
            a(0(), b(0(), x)) -> b(0(), a(0(), x)),
              a(0(), a(x, y)) -> a(1(), a(1(), a(x, y))),
      a(0(), a(1(), a(x, y))) -> a(1(), a(0(), a(x, y)))}
     POLY:
      Argument Filtering:
       pi(1) = [], pi(a#) = [1], pi(a) = [0,1], pi(0) = [], pi(b#) = 1, pi(b) = [0,1]
      Usable Rules:
       {}
      Interpretation:
       [a#](x0) = x0 + 1,
       [a](x0, x1) = x0 + x1 + 1,
       [b](x0, x1) = x0 + x1,
       [1] = 0,
       [0] = 1
      Strict:
       {b#(0(), a(1(), a(x, y))) -> a#(0(), a(x, y)),
                      a#(0(), x) -> b#(0(), b(0(), x)),
              a#(0(), b(0(), x)) -> b#(0(), a(0(), x))}
      Weak:
       {b(0(), a(1(), a(x, y))) -> b(1(), a(0(), a(x, y))),
                      a(0(), x) -> b(0(), b(0(), x)),
              a(0(), b(0(), x)) -> b(0(), a(0(), x)),
                a(0(), a(x, y)) -> a(1(), a(1(), a(x, y))),
        a(0(), a(1(), a(x, y))) -> a(1(), a(0(), a(x, y)))}
      EDG:
       {(a#(0(), x) -> b#(0(), b(0(), x)), b#(0(), a(1(), a(x, y))) -> a#(0(), a(x, y)))
        (a#(0(), b(0(), x)) -> b#(0(), a(0(), x)), b#(0(), a(1(), a(x, y))) -> a#(0(), a(x, y)))
        (b#(0(), a(1(), a(x, y))) -> a#(0(), a(x, y)), a#(0(), x) -> b#(0(), b(0(), x)))
        (b#(0(), a(1(), a(x, y))) -> a#(0(), a(x, y)), a#(0(), b(0(), x)) -> b#(0(), a(0(), x)))}
       SCCS:
        Scc:
         {b#(0(), a(1(), a(x, y))) -> a#(0(), a(x, y)),
                        a#(0(), x) -> b#(0(), b(0(), x)),
                a#(0(), b(0(), x)) -> b#(0(), a(0(), x))}
        SCC:
         Strict:
          {b#(0(), a(1(), a(x, y))) -> a#(0(), a(x, y)),
                         a#(0(), x) -> b#(0(), b(0(), x)),
                 a#(0(), b(0(), x)) -> b#(0(), a(0(), x))}
         Weak:
         {b(0(), a(1(), a(x, y))) -> b(1(), a(0(), a(x, y))),
                        a(0(), x) -> b(0(), b(0(), x)),
                a(0(), b(0(), x)) -> b(0(), a(0(), x)),
                  a(0(), a(x, y)) -> a(1(), a(1(), a(x, y))),
          a(0(), a(1(), a(x, y))) -> a(1(), a(0(), a(x, y)))}
         POLY:
          Argument Filtering:
           pi(1) = [], pi(a#) = [], pi(a) = [], pi(0) = [], pi(b#) = 1, pi(b) = []
          Usable Rules:
           {}
          Interpretation:
           [a#] = 1,
           [a] = 1,
           [b] = 0
          Strict:
           {b#(0(), a(1(), a(x, y))) -> a#(0(), a(x, y)),
                  a#(0(), b(0(), x)) -> b#(0(), a(0(), x))}
          Weak:
           {b(0(), a(1(), a(x, y))) -> b(1(), a(0(), a(x, y))),
                          a(0(), x) -> b(0(), b(0(), x)),
                  a(0(), b(0(), x)) -> b(0(), a(0(), x)),
                    a(0(), a(x, y)) -> a(1(), a(1(), a(x, y))),
            a(0(), a(1(), a(x, y))) -> a(1(), a(0(), a(x, y)))}
          EDG:
           {(a#(0(), b(0(), x)) -> b#(0(), a(0(), x)), b#(0(), a(1(), a(x, y))) -> a#(0(), a(x, y)))
            (b#(0(), a(1(), a(x, y))) -> a#(0(), a(x, y)), a#(0(), b(0(), x)) -> b#(0(), a(0(), x)))}
           SCCS:
            Scc:
             {b#(0(), a(1(), a(x, y))) -> a#(0(), a(x, y)),
                    a#(0(), b(0(), x)) -> b#(0(), a(0(), x))}
            SCC:
             Strict:
              {b#(0(), a(1(), a(x, y))) -> a#(0(), a(x, y)),
                     a#(0(), b(0(), x)) -> b#(0(), a(0(), x))}
             Weak:
             {b(0(), a(1(), a(x, y))) -> b(1(), a(0(), a(x, y))),
                            a(0(), x) -> b(0(), b(0(), x)),
                    a(0(), b(0(), x)) -> b(0(), a(0(), x)),
                      a(0(), a(x, y)) -> a(1(), a(1(), a(x, y))),
              a(0(), a(1(), a(x, y))) -> a(1(), a(0(), a(x, y)))}
             Fail