MAYBE
Time: 0.021106
TRS:
 {f(0(), 1(), g(x, y), z) -> f(g(x, y), g(x, y), g(x, y), h x),
              g(0(), 1()) -> 0(),
              g(0(), 1()) -> 1(),
                h g(x, y) -> h x}
 DP:
  DP:
   {f#(0(), 1(), g(x, y), z) -> f#(g(x, y), g(x, y), g(x, y), h x),
    f#(0(), 1(), g(x, y), z) -> h# x,
                  h# g(x, y) -> h# x}
  TRS:
  {f(0(), 1(), g(x, y), z) -> f(g(x, y), g(x, y), g(x, y), h x),
               g(0(), 1()) -> 0(),
               g(0(), 1()) -> 1(),
                 h g(x, y) -> h x}
  UR:
   {g(0(), 1()) -> 0(),
    g(0(), 1()) -> 1(),
      h g(x, y) -> h x}
   EDG:
    {(h# g(x, y) -> h# x, h# g(x, y) -> h# x)
     (f#(0(), 1(), g(x, y), z) -> f#(g(x, y), g(x, y), g(x, y), h x), f#(0(), 1(), g(x, y), z) -> f#(g(x, y), g(x, y), g(x, y), h x))
     (f#(0(), 1(), g(x, y), z) -> f#(g(x, y), g(x, y), g(x, y), h x), f#(0(), 1(), g(x, y), z) -> h# x)
     (f#(0(), 1(), g(x, y), z) -> h# x, h# g(x, y) -> h# x)}
    STATUS:
     arrows: 0.555556
     SCCS (2):
      Scc:
       {f#(0(), 1(), g(x, y), z) -> f#(g(x, y), g(x, y), g(x, y), h x)}
      Scc:
       {h# g(x, y) -> h# x}
      
      SCC (1):
       Strict:
        {f#(0(), 1(), g(x, y), z) -> f#(g(x, y), g(x, y), g(x, y), h x)}
       Weak:
       {f(0(), 1(), g(x, y), z) -> f(g(x, y), g(x, y), g(x, y), h x),
                    g(0(), 1()) -> 0(),
                    g(0(), 1()) -> 1(),
                      h g(x, y) -> h x}
       Fail
      
      SCC (1):
       Strict:
        {h# g(x, y) -> h# x}
       Weak:
       {f(0(), 1(), g(x, y), z) -> f(g(x, y), g(x, y), g(x, y), h x),
                    g(0(), 1()) -> 0(),
                    g(0(), 1()) -> 1(),
                      h g(x, y) -> h x}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [f](x0, x1, x2, x3) = x0 + x1 + x2 + x3 + 1,
         
         [g](x0, x1) = x0 + x1 + 1,
         
         [h](x0) = 1,
         
         [0] = 0,
         
         [1] = 1,
         
         [h#](x0) = x0 + 1
        Strict:
         h# g(x, y) -> h# x
         2 + 1x + 1y >= 1 + 1x
        Weak:
         h g(x, y) -> h x
         1 + 0x + 0y >= 1 + 0x
         g(0(), 1()) -> 1()
         2 >= 1
         g(0(), 1()) -> 0()
         2 >= 0
         f(0(), 1(), g(x, y), z) -> f(g(x, y), g(x, y), g(x, y), h x)
         3 + 1x + 1y + 1z >= 5 + 3x + 3y
       Qed