MAYBE
Time: 0.025765
TRS:
 {f(g x, g y) -> f(p f(g x, s y), g s p x),
        p 0() -> g 0(),
      g s p x -> p x}
 DP:
  DP:
   {f#(g x, g y) -> f#(p f(g x, s y), g s p x),
    f#(g x, g y) -> f#(g x, s y),
    f#(g x, g y) -> p# x,
    f#(g x, g y) -> p# f(g x, s y),
    f#(g x, g y) -> g# s p x,
          p# 0() -> g# 0()}
  TRS:
  {f(g x, g y) -> f(p f(g x, s y), g s p x),
         p 0() -> g 0(),
       g s p x -> p x}
  UR:
   {  p 0() -> g 0(),
    g s p x -> p x}
   EDG:
    {(f#(g x, g y) -> f#(p f(g x, s y), g s p x), f#(g x, g y) -> g# s p x)
     (f#(g x, g y) -> f#(p f(g x, s y), g s p x), f#(g x, g y) -> p# f(g x, s y))
     (f#(g x, g y) -> f#(p f(g x, s y), g s p x), f#(g x, g y) -> p# x)
     (f#(g x, g y) -> f#(p f(g x, s y), g s p x), f#(g x, g y) -> f#(g x, s y))
     (f#(g x, g y) -> f#(p f(g x, s y), g s p x), f#(g x, g y) -> f#(p f(g x, s y), g s p x))
     (f#(g x, g y) -> p# f(g x, s y), p# 0() -> g# 0())
     (f#(g x, g y) -> p# x, p# 0() -> g# 0())
     (f#(g x, g y) -> f#(g x, s y), f#(g x, g y) -> f#(p f(g x, s y), g s p x))
     (f#(g x, g y) -> f#(g x, s y), f#(g x, g y) -> f#(g x, s y))
     (f#(g x, g y) -> f#(g x, s y), f#(g x, g y) -> p# x)
     (f#(g x, g y) -> f#(g x, s y), f#(g x, g y) -> p# f(g x, s y))
     (f#(g x, g y) -> f#(g x, s y), f#(g x, g y) -> g# s p x)}
    STATUS:
     arrows: 0.666667
     SCCS (1):
      Scc:
       {f#(g x, g y) -> f#(p f(g x, s y), g s p x),
        f#(g x, g y) -> f#(g x, s y)}
      
      SCC (2):
       Strict:
        {f#(g x, g y) -> f#(p f(g x, s y), g s p x),
         f#(g x, g y) -> f#(g x, s y)}
       Weak:
       {f(g x, g y) -> f(p f(g x, s y), g s p x),
              p 0() -> g 0(),
            g s p x -> p x}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [f](x0, x1) = 0,
         
         [p](x0) = 1,
         
         [g](x0) = 1,
         
         [s](x0) = 0,
         
         [0] = 0,
         
         [f#](x0, x1) = x0
        Strict:
         f#(g x, g y) -> f#(g x, s y)
         1 + 0x + 0y >= 0 + 0x + 0y
         f#(g x, g y) -> f#(p f(g x, s y), g s p x)
         1 + 0x + 0y >= 1 + 0x + 0y
        Weak:
         g s p x -> p x
         1 + 0x >= 1 + 0x
         p 0() -> g 0()
         1 >= 1
         f(g x, g y) -> f(p f(g x, s y), g s p x)
         0 + 0x + 0y >= 0 + 0x + 0y
       SCCS (1):
        Scc:
         {f#(g x, g y) -> f#(p f(g x, s y), g s p x)}
        
        SCC (1):
         Strict:
          {f#(g x, g y) -> f#(p f(g x, s y), g s p x)}
         Weak:
         {f(g x, g y) -> f(p f(g x, s y), g s p x),
                p 0() -> g 0(),
              g s p x -> p x}
         Fail