MAYBE
Time: 2.280887
TRS:
 {              h(e x, y) -> h(d(x, y), s y),
            d(g(x, y), z) -> g(d(x, z), e y),
  d(g(g(0(), x), y), s z) -> g(e x, d(g(g(0(), x), y), z)),
  d(g(g(0(), x), y), 0()) -> e y,
          d(g(0(), x), y) -> e x,
              g(e x, e y) -> e g(x, y)}
 DP:
  DP:
   {              h#(e x, y) -> h#(d(x, y), s y),
                  h#(e x, y) -> d#(x, y),
              d#(g(x, y), z) -> d#(x, z),
              d#(g(x, y), z) -> g#(d(x, z), e y),
    d#(g(g(0(), x), y), s z) -> d#(g(g(0(), x), y), z),
    d#(g(g(0(), x), y), s z) -> g#(e x, d(g(g(0(), x), y), z)),
                g#(e x, e y) -> g#(x, y)}
  TRS:
  {              h(e x, y) -> h(d(x, y), s y),
             d(g(x, y), z) -> g(d(x, z), e y),
   d(g(g(0(), x), y), s z) -> g(e x, d(g(g(0(), x), y), z)),
   d(g(g(0(), x), y), 0()) -> e y,
           d(g(0(), x), y) -> e x,
               g(e x, e y) -> e g(x, y)}
  UR:
   {          d(g(x, y), z) -> g(d(x, z), e y),
    d(g(g(0(), x), y), s z) -> g(e x, d(g(g(0(), x), y), z)),
    d(g(g(0(), x), y), 0()) -> e y,
            d(g(0(), x), y) -> e x,
                g(e x, e y) -> e g(x, y),
                    a(w, v) -> w,
                    a(w, v) -> v}
   EDG:
    {(h#(e x, y) -> h#(d(x, y), s y), h#(e x, y) -> d#(x, y))
     (h#(e x, y) -> h#(d(x, y), s y), h#(e x, y) -> h#(d(x, y), s y))
     (d#(g(g(0(), x), y), s z) -> d#(g(g(0(), x), y), z), d#(g(g(0(), x), y), s z) -> g#(e x, d(g(g(0(), x), y), z)))
     (d#(g(g(0(), x), y), s z) -> d#(g(g(0(), x), y), z), d#(g(g(0(), x), y), s z) -> d#(g(g(0(), x), y), z))
     (d#(g(g(0(), x), y), s z) -> d#(g(g(0(), x), y), z), d#(g(x, y), z) -> g#(d(x, z), e y))
     (d#(g(g(0(), x), y), s z) -> d#(g(g(0(), x), y), z), d#(g(x, y), z) -> d#(x, z))
     (g#(e x, e y) -> g#(x, y), g#(e x, e y) -> g#(x, y))
     (d#(g(x, y), z) -> d#(x, z), d#(g(x, y), z) -> d#(x, z))
     (d#(g(x, y), z) -> d#(x, z), d#(g(x, y), z) -> g#(d(x, z), e y))
     (d#(g(x, y), z) -> d#(x, z), d#(g(g(0(), x), y), s z) -> d#(g(g(0(), x), y), z))
     (d#(g(x, y), z) -> d#(x, z), d#(g(g(0(), x), y), s z) -> g#(e x, d(g(g(0(), x), y), z)))
     (h#(e x, y) -> d#(x, y), d#(g(x, y), z) -> d#(x, z))
     (h#(e x, y) -> d#(x, y), d#(g(x, y), z) -> g#(d(x, z), e y))
     (h#(e x, y) -> d#(x, y), d#(g(g(0(), x), y), s z) -> d#(g(g(0(), x), y), z))
     (h#(e x, y) -> d#(x, y), d#(g(g(0(), x), y), s z) -> g#(e x, d(g(g(0(), x), y), z)))
     (d#(g(x, y), z) -> g#(d(x, z), e y), g#(e x, e y) -> g#(x, y))
     (d#(g(g(0(), x), y), s z) -> g#(e x, d(g(g(0(), x), y), z)), g#(e x, e y) -> g#(x, y))}
    STATUS:
     arrows: 0.653061
     SCCS (3):
      Scc:
       {h#(e x, y) -> h#(d(x, y), s y)}
      Scc:
       {          d#(g(x, y), z) -> d#(x, z),
        d#(g(g(0(), x), y), s z) -> d#(g(g(0(), x), y), z)}
      Scc:
       {g#(e x, e y) -> g#(x, y)}
      
      SCC (1):
       Strict:
        {h#(e x, y) -> h#(d(x, y), s y)}
       Weak:
       {              h(e x, y) -> h(d(x, y), s y),
                  d(g(x, y), z) -> g(d(x, z), e y),
        d(g(g(0(), x), y), s z) -> g(e x, d(g(g(0(), x), y), z)),
        d(g(g(0(), x), y), 0()) -> e y,
                d(g(0(), x), y) -> e x,
                    g(e x, e y) -> e g(x, y)}
       Fail
      
      SCC (2):
       Strict:
        {          d#(g(x, y), z) -> d#(x, z),
         d#(g(g(0(), x), y), s z) -> d#(g(g(0(), x), y), z)}
       Weak:
       {              h(e x, y) -> h(d(x, y), s y),
                  d(g(x, y), z) -> g(d(x, z), e y),
        d(g(g(0(), x), y), s z) -> g(e x, d(g(g(0(), x), y), z)),
        d(g(g(0(), x), y), 0()) -> e y,
                d(g(0(), x), y) -> e x,
                    g(e x, e y) -> e g(x, y)}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [h](x0, x1) = 0,
         
         [d](x0, x1) = 0,
         
         [g](x0, x1) = x0 + 1,
         
         [s](x0) = x0 + 1,
         
         [e](x0) = 0,
         
         [0] = 1,
         
         [d#](x0, x1) = x0
        Strict:
         d#(g(g(0(), x), y), s z) -> d#(g(g(0(), x), y), z)
         1 + 0x + 0y + 1z >= 0 + 0x + 0y + 1z
         d#(g(x, y), z) -> d#(x, z)
         0 + 0x + 0y + 1z >= 0 + 0x + 1z
        Weak:
         g(e x, e y) -> e g(x, y)
         1 + 0x + 0y >= 0 + 0x + 0y
         d(g(0(), x), y) -> e x
         0 + 0x + 0y >= 0 + 0x
         d(g(g(0(), x), y), 0()) -> e y
         0 + 0x + 0y >= 0 + 0y
         d(g(g(0(), x), y), s z) -> g(e x, d(g(g(0(), x), y), z))
         0 + 0x + 0y + 0z >= 1 + 0x + 0y + 0z
         d(g(x, y), z) -> g(d(x, z), e y)
         0 + 0x + 0y + 0z >= 1 + 0x + 0y + 0z
         h(e x, y) -> h(d(x, y), s y)
         0 + 0x + 0y >= 0 + 0x + 0y
       SCCS (1):
        Scc:
         {d#(g(x, y), z) -> d#(x, z)}
        
        SCC (1):
         Strict:
          {d#(g(x, y), z) -> d#(x, z)}
         Weak:
         {              h(e x, y) -> h(d(x, y), s y),
                    d(g(x, y), z) -> g(d(x, z), e y),
          d(g(g(0(), x), y), s z) -> g(e x, d(g(g(0(), x), y), z)),
          d(g(g(0(), x), y), 0()) -> e y,
                  d(g(0(), x), y) -> e x,
                      g(e x, e y) -> e g(x, y)}
         POLY:
          Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
          Interpretation:
           [h](x0, x1) = x0 + x1 + 1,
           
           [d](x0, x1) = x0,
           
           [g](x0, x1) = x0 + 1,
           
           [s](x0) = x0,
           
           [e](x0) = 1,
           
           [0] = 0,
           
           [d#](x0, x1) = x0
          Strict:
           d#(g(x, y), z) -> d#(x, z)
           1 + 1x + 0y + 0z >= 0 + 1x + 0z
          Weak:
           g(e x, e y) -> e g(x, y)
           2 + 0x + 0y >= 1 + 0x + 0y
           d(g(0(), x), y) -> e x
           0 + 0x + 1y >= 1 + 0x
           d(g(g(0(), x), y), 0()) -> e y
           0 + 0x + 0y >= 1 + 0y
           d(g(g(0(), x), y), s z) -> g(e x, d(g(g(0(), x), y), z))
           0 + 0x + 0y + 1z >= 2 + 0x + 0y + 0z
           d(g(x, y), z) -> g(d(x, z), e y)
           0 + 0x + 0y + 1z >= 1 + 0x + 0y + 1z
           h(e x, y) -> h(d(x, y), s y)
           2 + 0x + 1y >= 1 + 0x + 2y
         Qed
     
     
     SCC (1):
      Strict:
       {g#(e x, e y) -> g#(x, y)}
      Weak:
      {              h(e x, y) -> h(d(x, y), s y),
                 d(g(x, y), z) -> g(d(x, z), e y),
       d(g(g(0(), x), y), s z) -> g(e x, d(g(g(0(), x), y), z)),
       d(g(g(0(), x), y), 0()) -> e y,
               d(g(0(), x), y) -> e x,
                   g(e x, e y) -> e g(x, y)}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [h](x0, x1) = x0 + x1 + 1,
        
        [d](x0, x1) = x0 + x1,
        
        [g](x0, x1) = x0,
        
        [s](x0) = x0,
        
        [e](x0) = x0 + 1,
        
        [0] = 1,
        
        [g#](x0, x1) = x0 + 1
       Strict:
        g#(e x, e y) -> g#(x, y)
        2 + 1x + 0y >= 1 + 1x + 0y
       Weak:
        g(e x, e y) -> e g(x, y)
        1 + 1x + 0y >= 1 + 1x + 0y
        d(g(0(), x), y) -> e x
        1 + 0x + 1y >= 1 + 1x
        d(g(g(0(), x), y), 0()) -> e y
        2 + 0x + 0y >= 1 + 1y
        d(g(g(0(), x), y), s z) -> g(e x, d(g(g(0(), x), y), z))
        1 + 0x + 0y + 1z >= 1 + 1x + 0y + 0z
        d(g(x, y), z) -> g(d(x, z), e y)
        0 + 1x + 0y + 1z >= 0 + 1x + 0y + 1z
        h(e x, y) -> h(d(x, y), s y)
        2 + 1x + 1y >= 1 + 1x + 2y
      Qed