MAYBE
Time: 0.022343
TRS:
 {            f(x, g(y, z)) -> g(f(x, y), z),
                f(x, nil()) -> g(nil(), x),
             ++(x, g(y, z)) -> g(++(x, y), z),
               ++(x, nil()) -> x,
               null g(x, y) -> false(),
                 null nil() -> true(),
              mem(x, max x) -> not null x,
            mem(g(x, y), z) -> or(=(y, z), mem(x, z)),
              mem(nil(), y) -> false(),
  max g(g(g(x, y), z), u()) -> max'(max g(g(x, y), z), u()),
      max g(g(nil(), x), y) -> max'(x, y)}
 DP:
  DP:
   {            f#(x, g(y, z)) -> f#(x, y),
               ++#(x, g(y, z)) -> ++#(x, y),
                mem#(x, max x) -> null# x,
              mem#(g(x, y), z) -> mem#(x, z),
    max# g(g(g(x, y), z), u()) -> max# g(g(x, y), z)}
  TRS:
  {            f(x, g(y, z)) -> g(f(x, y), z),
                 f(x, nil()) -> g(nil(), x),
              ++(x, g(y, z)) -> g(++(x, y), z),
                ++(x, nil()) -> x,
                null g(x, y) -> false(),
                  null nil() -> true(),
               mem(x, max x) -> not null x,
             mem(g(x, y), z) -> or(=(y, z), mem(x, z)),
               mem(nil(), y) -> false(),
   max g(g(g(x, y), z), u()) -> max'(max g(g(x, y), z), u()),
       max g(g(nil(), x), y) -> max'(x, y)}
  UR:
   {}
   EDG:
    {(++#(x, g(y, z)) -> ++#(x, y), ++#(x, g(y, z)) -> ++#(x, y))
     (mem#(g(x, y), z) -> mem#(x, z), mem#(x, max x) -> null# x)
     (mem#(g(x, y), z) -> mem#(x, z), mem#(g(x, y), z) -> mem#(x, z))
     (max# g(g(g(x, y), z), u()) -> max# g(g(x, y), z), max# g(g(g(x, y), z), u()) -> max# g(g(x, y), z))
     (f#(x, g(y, z)) -> f#(x, y), f#(x, g(y, z)) -> f#(x, y))}
    STATUS:
     arrows: 0.800000
     SCCS (4):
      Scc:
       {mem#(g(x, y), z) -> mem#(x, z)}
      Scc:
       {max# g(g(g(x, y), z), u()) -> max# g(g(x, y), z)}
      Scc:
       {++#(x, g(y, z)) -> ++#(x, y)}
      Scc:
       {f#(x, g(y, z)) -> f#(x, y)}
      
      SCC (1):
       Strict:
        {mem#(g(x, y), z) -> mem#(x, z)}
       Weak:
       {            f(x, g(y, z)) -> g(f(x, y), z),
                      f(x, nil()) -> g(nil(), x),
                   ++(x, g(y, z)) -> g(++(x, y), z),
                     ++(x, nil()) -> x,
                     null g(x, y) -> false(),
                       null nil() -> true(),
                    mem(x, max x) -> not null x,
                  mem(g(x, y), z) -> or(=(y, z), mem(x, z)),
                    mem(nil(), y) -> false(),
        max g(g(g(x, y), z), u()) -> max'(max g(g(x, y), z), u()),
            max g(g(nil(), x), y) -> max'(x, y)}
       Open
      
      SCC (1):
       Strict:
        {max# g(g(g(x, y), z), u()) -> max# g(g(x, y), z)}
       Weak:
       {            f(x, g(y, z)) -> g(f(x, y), z),
                      f(x, nil()) -> g(nil(), x),
                   ++(x, g(y, z)) -> g(++(x, y), z),
                     ++(x, nil()) -> x,
                     null g(x, y) -> false(),
                       null nil() -> true(),
                    mem(x, max x) -> not null x,
                  mem(g(x, y), z) -> or(=(y, z), mem(x, z)),
                    mem(nil(), y) -> false(),
        max g(g(g(x, y), z), u()) -> max'(max g(g(x, y), z), u()),
            max g(g(nil(), x), y) -> max'(x, y)}
       Open
      SCC (1):
       Strict:
        {++#(x, g(y, z)) -> ++#(x, y)}
       Weak:
       {            f(x, g(y, z)) -> g(f(x, y), z),
                      f(x, nil()) -> g(nil(), x),
                   ++(x, g(y, z)) -> g(++(x, y), z),
                     ++(x, nil()) -> x,
                     null g(x, y) -> false(),
                       null nil() -> true(),
                    mem(x, max x) -> not null x,
                  mem(g(x, y), z) -> or(=(y, z), mem(x, z)),
                    mem(nil(), y) -> false(),
        max g(g(g(x, y), z), u()) -> max'(max g(g(x, y), z), u()),
            max g(g(nil(), x), y) -> max'(x, y)}
       Open
      SCC (1):
       Strict:
        {f#(x, g(y, z)) -> f#(x, y)}
       Weak:
       {            f(x, g(y, z)) -> g(f(x, y), z),
                      f(x, nil()) -> g(nil(), x),
                   ++(x, g(y, z)) -> g(++(x, y), z),
                     ++(x, nil()) -> x,
                     null g(x, y) -> false(),
                       null nil() -> true(),
                    mem(x, max x) -> not null x,
                  mem(g(x, y), z) -> or(=(y, z), mem(x, z)),
                    mem(nil(), y) -> false(),
        max g(g(g(x, y), z), u()) -> max'(max g(g(x, y), z), u()),
            max g(g(nil(), x), y) -> max'(x, y)}
       Open