MAYBE
Time: 1.011930
TRS:
 {   if(true(), x, y) -> x,
    if(false(), x, y) -> y,
      and(x, false()) -> false(),
  and(true(), true()) -> true(),
                f s x -> h x,
                f 0() -> true(),
                  t x -> p(x, x),
          g(s x, s y) -> if(and(f s x, f s y), t g(k(minus(m(x, y), n(x, y)), s s 0()), k(n(s x, s y), s s 0())), g(minus(m(x, y), n(x, y)), n(s x, s y))),
          k(s x, s y) -> s k(minus(x, y), s y),
          k(0(), s y) -> 0(),
        minus(x, 0()) -> x,
      minus(s x, s y) -> minus(x, y),
            m(x, 0()) -> x,
          m(s x, s y) -> s m(x, y),
            m(0(), y) -> y,
            n(x, 0()) -> 0(),
          n(s x, s y) -> s n(x, y),
            n(0(), y) -> 0(),
            p(s x, x) -> p(if(gt(x, x), id x, id x), s x),
          p(s x, s y) -> s s p(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)),
            p(0(), y) -> y,
         p(id x, s y) -> s p(x, if(gt(s y, y), y, s y)),
         gt(s x, s y) -> gt(x, y),
         gt(s x, 0()) -> true(),
           gt(0(), y) -> false(),
                not x -> if(x, false(), true()),
                 id x -> x,
                h s x -> f x,
                h 0() -> false()}
 DP:
  DP:
   {          f# s x -> h# x,
                t# x -> p#(x, x),
        g#(s x, s y) -> if#(and(f s x, f s y), t g(k(minus(m(x, y), n(x, y)), s s 0()), k(n(s x, s y), s s 0())), g(minus(m(x, y), n(x, y)), n(s x, s y))),
        g#(s x, s y) -> and#(f s x, f s y),
        g#(s x, s y) -> f# s x,
        g#(s x, s y) -> f# s y,
        g#(s x, s y) -> t# g(k(minus(m(x, y), n(x, y)), s s 0()), k(n(s x, s y), s s 0())),
        g#(s x, s y) -> g#(k(minus(m(x, y), n(x, y)), s s 0()), k(n(s x, s y), s s 0())),
        g#(s x, s y) -> g#(minus(m(x, y), n(x, y)), n(s x, s y)),
        g#(s x, s y) -> k#(minus(m(x, y), n(x, y)), s s 0()),
        g#(s x, s y) -> k#(n(s x, s y), s s 0()),
        g#(s x, s y) -> minus#(m(x, y), n(x, y)),
        g#(s x, s y) -> m#(x, y),
        g#(s x, s y) -> n#(x, y),
        g#(s x, s y) -> n#(s x, s y),
        k#(s x, s y) -> k#(minus(x, y), s y),
        k#(s x, s y) -> minus#(x, y),
    minus#(s x, s y) -> minus#(x, y),
        m#(s x, s y) -> m#(x, y),
        n#(s x, s y) -> n#(x, y),
          p#(s x, x) -> if#(gt(x, x), id x, id x),
          p#(s x, x) -> p#(if(gt(x, x), id x, id x), s x),
          p#(s x, x) -> gt#(x, x),
          p#(s x, x) -> id# x,
        p#(s x, s y) -> if#(gt(x, y), x, y),
        p#(s x, s y) -> if#(not gt(x, y), id x, id y),
        p#(s x, s y) -> p#(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)),
        p#(s x, s y) -> gt#(x, y),
        p#(s x, s y) -> not# gt(x, y),
        p#(s x, s y) -> id# x,
        p#(s x, s y) -> id# y,
       p#(id x, s y) -> if#(gt(s y, y), y, s y),
       p#(id x, s y) -> p#(x, if(gt(s y, y), y, s y)),
       p#(id x, s y) -> gt#(s y, y),
       gt#(s x, s y) -> gt#(x, y),
              not# x -> if#(x, false(), true()),
              h# s x -> f# x}
  TRS:
  {   if(true(), x, y) -> x,
     if(false(), x, y) -> y,
       and(x, false()) -> false(),
   and(true(), true()) -> true(),
                 f s x -> h x,
                 f 0() -> true(),
                   t x -> p(x, x),
           g(s x, s y) -> if(and(f s x, f s y), t g(k(minus(m(x, y), n(x, y)), s s 0()), k(n(s x, s y), s s 0())), g(minus(m(x, y), n(x, y)), n(s x, s y))),
           k(s x, s y) -> s k(minus(x, y), s y),
           k(0(), s y) -> 0(),
         minus(x, 0()) -> x,
       minus(s x, s y) -> minus(x, y),
             m(x, 0()) -> x,
           m(s x, s y) -> s m(x, y),
             m(0(), y) -> y,
             n(x, 0()) -> 0(),
           n(s x, s y) -> s n(x, y),
             n(0(), y) -> 0(),
             p(s x, x) -> p(if(gt(x, x), id x, id x), s x),
           p(s x, s y) -> s s p(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)),
             p(0(), y) -> y,
          p(id x, s y) -> s p(x, if(gt(s y, y), y, s y)),
          gt(s x, s y) -> gt(x, y),
          gt(s x, 0()) -> true(),
            gt(0(), y) -> false(),
                 not x -> if(x, false(), true()),
                  id x -> x,
                 h s x -> f x,
                 h 0() -> false()}
  EDG:
   {(g#(s x, s y) -> f# s y, f# s x -> h# x)
    (g#(s x, s y) -> n#(s x, s y), n#(s x, s y) -> n#(x, y))
    (p#(s x, x) -> p#(if(gt(x, x), id x, id x), s x), p#(id x, s y) -> gt#(s y, y))
    (p#(s x, x) -> p#(if(gt(x, x), id x, id x), s x), p#(id x, s y) -> p#(x, if(gt(s y, y), y, s y)))
    (p#(s x, x) -> p#(if(gt(x, x), id x, id x), s x), p#(id x, s y) -> if#(gt(s y, y), y, s y))
    (p#(s x, x) -> p#(if(gt(x, x), id x, id x), s x), p#(s x, s y) -> id# y)
    (p#(s x, x) -> p#(if(gt(x, x), id x, id x), s x), p#(s x, s y) -> id# x)
    (p#(s x, x) -> p#(if(gt(x, x), id x, id x), s x), p#(s x, s y) -> not# gt(x, y))
    (p#(s x, x) -> p#(if(gt(x, x), id x, id x), s x), p#(s x, s y) -> gt#(x, y))
    (p#(s x, x) -> p#(if(gt(x, x), id x, id x), s x), p#(s x, s y) -> p#(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)))
    (p#(s x, x) -> p#(if(gt(x, x), id x, id x), s x), p#(s x, s y) -> if#(not gt(x, y), id x, id y))
    (p#(s x, x) -> p#(if(gt(x, x), id x, id x), s x), p#(s x, s y) -> if#(gt(x, y), x, y))
    (p#(s x, x) -> p#(if(gt(x, x), id x, id x), s x), p#(s x, x) -> id# x)
    (p#(s x, x) -> p#(if(gt(x, x), id x, id x), s x), p#(s x, x) -> gt#(x, x))
    (p#(s x, x) -> p#(if(gt(x, x), id x, id x), s x), p#(s x, x) -> p#(if(gt(x, x), id x, id x), s x))
    (p#(s x, x) -> p#(if(gt(x, x), id x, id x), s x), p#(s x, x) -> if#(gt(x, x), id x, id x))
    (g#(s x, s y) -> k#(minus(m(x, y), n(x, y)), s s 0()), k#(s x, s y) -> minus#(x, y))
    (g#(s x, s y) -> k#(minus(m(x, y), n(x, y)), s s 0()), k#(s x, s y) -> k#(minus(x, y), s y))
    (f# s x -> h# x, h# s x -> f# x)
    (g#(s x, s y) -> g#(k(minus(m(x, y), n(x, y)), s s 0()), k(n(s x, s y), s s 0())), g#(s x, s y) -> n#(s x, s y))
    (g#(s x, s y) -> g#(k(minus(m(x, y), n(x, y)), s s 0()), k(n(s x, s y), s s 0())), g#(s x, s y) -> n#(x, y))
    (g#(s x, s y) -> g#(k(minus(m(x, y), n(x, y)), s s 0()), k(n(s x, s y), s s 0())), g#(s x, s y) -> m#(x, y))
    (g#(s x, s y) -> g#(k(minus(m(x, y), n(x, y)), s s 0()), k(n(s x, s y), s s 0())), g#(s x, s y) -> minus#(m(x, y), n(x, y)))
    (g#(s x, s y) -> g#(k(minus(m(x, y), n(x, y)), s s 0()), k(n(s x, s y), s s 0())), g#(s x, s y) -> k#(n(s x, s y), s s 0()))
    (g#(s x, s y) -> g#(k(minus(m(x, y), n(x, y)), s s 0()), k(n(s x, s y), s s 0())), g#(s x, s y) -> k#(minus(m(x, y), n(x, y)), s s 0()))
    (g#(s x, s y) -> g#(k(minus(m(x, y), n(x, y)), s s 0()), k(n(s x, s y), s s 0())), g#(s x, s y) -> g#(minus(m(x, y), n(x, y)), n(s x, s y)))
    (g#(s x, s y) -> g#(k(minus(m(x, y), n(x, y)), s s 0()), k(n(s x, s y), s s 0())), g#(s x, s y) -> g#(k(minus(m(x, y), n(x, y)), s s 0()), k(n(s x, s y), s s 0())))
    (g#(s x, s y) -> g#(k(minus(m(x, y), n(x, y)), s s 0()), k(n(s x, s y), s s 0())), g#(s x, s y) -> t# g(k(minus(m(x, y), n(x, y)), s s 0()), k(n(s x, s y), s s 0())))
    (g#(s x, s y) -> g#(k(minus(m(x, y), n(x, y)), s s 0()), k(n(s x, s y), s s 0())), g#(s x, s y) -> f# s y)
    (g#(s x, s y) -> g#(k(minus(m(x, y), n(x, y)), s s 0()), k(n(s x, s y), s s 0())), g#(s x, s y) -> f# s x)
    (g#(s x, s y) -> g#(k(minus(m(x, y), n(x, y)), s s 0()), k(n(s x, s y), s s 0())), g#(s x, s y) -> and#(f s x, f s y))
    (g#(s x, s y) -> g#(k(minus(m(x, y), n(x, y)), s s 0()), k(n(s x, s y), s s 0())), g#(s x, s y) -> if#(and(f s x, f s y), t g(k(minus(m(x, y), n(x, y)), s s 0()), k(n(s x, s y), s s 0())), g(minus(m(x, y), n(x, y)), n(s x, s y))))
    (t# x -> p#(x, x), p#(id x, s y) -> gt#(s y, y))
    (t# x -> p#(x, x), p#(id x, s y) -> p#(x, if(gt(s y, y), y, s y)))
    (t# x -> p#(x, x), p#(id x, s y) -> if#(gt(s y, y), y, s y))
    (t# x -> p#(x, x), p#(s x, s y) -> id# y)
    (t# x -> p#(x, x), p#(s x, s y) -> id# x)
    (t# x -> p#(x, x), p#(s x, s y) -> not# gt(x, y))
    (t# x -> p#(x, x), p#(s x, s y) -> gt#(x, y))
    (t# x -> p#(x, x), p#(s x, s y) -> p#(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)))
    (t# x -> p#(x, x), p#(s x, s y) -> if#(not gt(x, y), id x, id y))
    (t# x -> p#(x, x), p#(s x, s y) -> if#(gt(x, y), x, y))
    (t# x -> p#(x, x), p#(s x, x) -> id# x)
    (t# x -> p#(x, x), p#(s x, x) -> gt#(x, x))
    (t# x -> p#(x, x), p#(s x, x) -> p#(if(gt(x, x), id x, id x), s x))
    (t# x -> p#(x, x), p#(s x, x) -> if#(gt(x, x), id x, id x))
    (g#(s x, s y) -> m#(x, y), m#(s x, s y) -> m#(x, y))
    (k#(s x, s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y))
    (m#(s x, s y) -> m#(x, y), m#(s x, s y) -> m#(x, y))
    (p#(s x, s y) -> gt#(x, y), gt#(s x, s y) -> gt#(x, y))
    (g#(s x, s y) -> t# g(k(minus(m(x, y), n(x, y)), s s 0()), k(n(s x, s y), s s 0())), t# x -> p#(x, x))
    (p#(id x, s y) -> p#(x, if(gt(s y, y), y, s y)), p#(id x, s y) -> gt#(s y, y))
    (p#(id x, s y) -> p#(x, if(gt(s y, y), y, s y)), p#(id x, s y) -> p#(x, if(gt(s y, y), y, s y)))
    (p#(id x, s y) -> p#(x, if(gt(s y, y), y, s y)), p#(id x, s y) -> if#(gt(s y, y), y, s y))
    (p#(id x, s y) -> p#(x, if(gt(s y, y), y, s y)), p#(s x, s y) -> id# y)
    (p#(id x, s y) -> p#(x, if(gt(s y, y), y, s y)), p#(s x, s y) -> id# x)
    (p#(id x, s y) -> p#(x, if(gt(s y, y), y, s y)), p#(s x, s y) -> not# gt(x, y))
    (p#(id x, s y) -> p#(x, if(gt(s y, y), y, s y)), p#(s x, s y) -> gt#(x, y))
    (p#(id x, s y) -> p#(x, if(gt(s y, y), y, s y)), p#(s x, s y) -> p#(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)))
    (p#(id x, s y) -> p#(x, if(gt(s y, y), y, s y)), p#(s x, s y) -> if#(not gt(x, y), id x, id y))
    (p#(id x, s y) -> p#(x, if(gt(s y, y), y, s y)), p#(s x, s y) -> if#(gt(x, y), x, y))
    (p#(id x, s y) -> p#(x, if(gt(s y, y), y, s y)), p#(s x, x) -> id# x)
    (p#(id x, s y) -> p#(x, if(gt(s y, y), y, s y)), p#(s x, x) -> gt#(x, x))
    (p#(id x, s y) -> p#(x, if(gt(s y, y), y, s y)), p#(s x, x) -> p#(if(gt(x, x), id x, id x), s x))
    (p#(id x, s y) -> p#(x, if(gt(s y, y), y, s y)), p#(s x, x) -> if#(gt(x, x), id x, id x))
    (g#(s x, s y) -> minus#(m(x, y), n(x, y)), minus#(s x, s y) -> minus#(x, y))
    (p#(s x, s y) -> p#(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)), p#(s x, x) -> if#(gt(x, x), id x, id x))
    (p#(s x, s y) -> p#(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)), p#(s x, x) -> p#(if(gt(x, x), id x, id x), s x))
    (p#(s x, s y) -> p#(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)), p#(s x, x) -> gt#(x, x))
    (p#(s x, s y) -> p#(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)), p#(s x, x) -> id# x)
    (p#(s x, s y) -> p#(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)), p#(s x, s y) -> if#(gt(x, y), x, y))
    (p#(s x, s y) -> p#(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)), p#(s x, s y) -> if#(not gt(x, y), id x, id y))
    (p#(s x, s y) -> p#(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)), p#(s x, s y) -> p#(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)))
    (p#(s x, s y) -> p#(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)), p#(s x, s y) -> gt#(x, y))
    (p#(s x, s y) -> p#(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)), p#(s x, s y) -> not# gt(x, y))
    (p#(s x, s y) -> p#(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)), p#(s x, s y) -> id# x)
    (p#(s x, s y) -> p#(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)), p#(s x, s y) -> id# y)
    (p#(s x, s y) -> p#(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)), p#(id x, s y) -> if#(gt(s y, y), y, s y))
    (p#(s x, s y) -> p#(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)), p#(id x, s y) -> p#(x, if(gt(s y, y), y, s y)))
    (p#(s x, s y) -> p#(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)), p#(id x, s y) -> gt#(s y, y))
    (gt#(s x, s y) -> gt#(x, y), gt#(s x, s y) -> gt#(x, y))
    (n#(s x, s y) -> n#(x, y), n#(s x, s y) -> n#(x, y))
    (minus#(s x, s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y))
    (g#(s x, s y) -> n#(x, y), n#(s x, s y) -> n#(x, y))
    (p#(s x, s y) -> not# gt(x, y), not# x -> if#(x, false(), true()))
    (p#(s x, x) -> gt#(x, x), gt#(s x, s y) -> gt#(x, y))
    (g#(s x, s y) -> g#(minus(m(x, y), n(x, y)), n(s x, s y)), g#(s x, s y) -> if#(and(f s x, f s y), t g(k(minus(m(x, y), n(x, y)), s s 0()), k(n(s x, s y), s s 0())), g(minus(m(x, y), n(x, y)), n(s x, s y))))
    (g#(s x, s y) -> g#(minus(m(x, y), n(x, y)), n(s x, s y)), g#(s x, s y) -> and#(f s x, f s y))
    (g#(s x, s y) -> g#(minus(m(x, y), n(x, y)), n(s x, s y)), g#(s x, s y) -> f# s x)
    (g#(s x, s y) -> g#(minus(m(x, y), n(x, y)), n(s x, s y)), g#(s x, s y) -> f# s y)
    (g#(s x, s y) -> g#(minus(m(x, y), n(x, y)), n(s x, s y)), g#(s x, s y) -> t# g(k(minus(m(x, y), n(x, y)), s s 0()), k(n(s x, s y), s s 0())))
    (g#(s x, s y) -> g#(minus(m(x, y), n(x, y)), n(s x, s y)), g#(s x, s y) -> g#(k(minus(m(x, y), n(x, y)), s s 0()), k(n(s x, s y), s s 0())))
    (g#(s x, s y) -> g#(minus(m(x, y), n(x, y)), n(s x, s y)), g#(s x, s y) -> g#(minus(m(x, y), n(x, y)), n(s x, s y)))
    (g#(s x, s y) -> g#(minus(m(x, y), n(x, y)), n(s x, s y)), g#(s x, s y) -> k#(minus(m(x, y), n(x, y)), s s 0()))
    (g#(s x, s y) -> g#(minus(m(x, y), n(x, y)), n(s x, s y)), g#(s x, s y) -> k#(n(s x, s y), s s 0()))
    (g#(s x, s y) -> g#(minus(m(x, y), n(x, y)), n(s x, s y)), g#(s x, s y) -> minus#(m(x, y), n(x, y)))
    (g#(s x, s y) -> g#(minus(m(x, y), n(x, y)), n(s x, s y)), g#(s x, s y) -> m#(x, y))
    (g#(s x, s y) -> g#(minus(m(x, y), n(x, y)), n(s x, s y)), g#(s x, s y) -> n#(x, y))
    (g#(s x, s y) -> g#(minus(m(x, y), n(x, y)), n(s x, s y)), g#(s x, s y) -> n#(s x, s y))
    (p#(id x, s y) -> gt#(s y, y), gt#(s x, s y) -> gt#(x, y))
    (h# s x -> f# x, f# s x -> h# x)
    (g#(s x, s y) -> k#(n(s x, s y), s s 0()), k#(s x, s y) -> k#(minus(x, y), s y))
    (g#(s x, s y) -> k#(n(s x, s y), s s 0()), k#(s x, s y) -> minus#(x, y))
    (k#(s x, s y) -> k#(minus(x, y), s y), k#(s x, s y) -> k#(minus(x, y), s y))
    (k#(s x, s y) -> k#(minus(x, y), s y), k#(s x, s y) -> minus#(x, y))
    (g#(s x, s y) -> f# s x, f# s x -> h# x)}
   STATUS:
    arrows: 0.922571
    SCCS (8):
     Scc:
      {g#(s x, s y) -> g#(k(minus(m(x, y), n(x, y)), s s 0()), k(n(s x, s y), s s 0())),
       g#(s x, s y) -> g#(minus(m(x, y), n(x, y)), n(s x, s y))}
     Scc:
      {m#(s x, s y) -> m#(x, y)}
     Scc:
      {   p#(s x, x) -> p#(if(gt(x, x), id x, id x), s x),
        p#(s x, s y) -> p#(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)),
       p#(id x, s y) -> p#(x, if(gt(s y, y), y, s y))}
     Scc:
      {gt#(s x, s y) -> gt#(x, y)}
     Scc:
      {k#(s x, s y) -> k#(minus(x, y), s y)}
     Scc:
      {minus#(s x, s y) -> minus#(x, y)}
     Scc:
      {n#(s x, s y) -> n#(x, y)}
     Scc:
      {f# s x -> h# x,
       h# s x -> f# x}
     
     SCC (2):
      Strict:
       {g#(s x, s y) -> g#(k(minus(m(x, y), n(x, y)), s s 0()), k(n(s x, s y), s s 0())),
        g#(s x, s y) -> g#(minus(m(x, y), n(x, y)), n(s x, s y))}
      Weak:
      {   if(true(), x, y) -> x,
         if(false(), x, y) -> y,
           and(x, false()) -> false(),
       and(true(), true()) -> true(),
                     f s x -> h x,
                     f 0() -> true(),
                       t x -> p(x, x),
               g(s x, s y) -> if(and(f s x, f s y), t g(k(minus(m(x, y), n(x, y)), s s 0()), k(n(s x, s y), s s 0())), g(minus(m(x, y), n(x, y)), n(s x, s y))),
               k(s x, s y) -> s k(minus(x, y), s y),
               k(0(), s y) -> 0(),
             minus(x, 0()) -> x,
           minus(s x, s y) -> minus(x, y),
                 m(x, 0()) -> x,
               m(s x, s y) -> s m(x, y),
                 m(0(), y) -> y,
                 n(x, 0()) -> 0(),
               n(s x, s y) -> s n(x, y),
                 n(0(), y) -> 0(),
                 p(s x, x) -> p(if(gt(x, x), id x, id x), s x),
               p(s x, s y) -> s s p(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)),
                 p(0(), y) -> y,
              p(id x, s y) -> s p(x, if(gt(s y, y), y, s y)),
              gt(s x, s y) -> gt(x, y),
              gt(s x, 0()) -> true(),
                gt(0(), y) -> false(),
                     not x -> if(x, false(), true()),
                      id x -> x,
                     h s x -> f x,
                     h 0() -> false()}
      Open
     
     
     SCC (1):
      Strict:
       {m#(s x, s y) -> m#(x, y)}
      Weak:
      {   if(true(), x, y) -> x,
         if(false(), x, y) -> y,
           and(x, false()) -> false(),
       and(true(), true()) -> true(),
                     f s x -> h x,
                     f 0() -> true(),
                       t x -> p(x, x),
               g(s x, s y) -> if(and(f s x, f s y), t g(k(minus(m(x, y), n(x, y)), s s 0()), k(n(s x, s y), s s 0())), g(minus(m(x, y), n(x, y)), n(s x, s y))),
               k(s x, s y) -> s k(minus(x, y), s y),
               k(0(), s y) -> 0(),
             minus(x, 0()) -> x,
           minus(s x, s y) -> minus(x, y),
                 m(x, 0()) -> x,
               m(s x, s y) -> s m(x, y),
                 m(0(), y) -> y,
                 n(x, 0()) -> 0(),
               n(s x, s y) -> s n(x, y),
                 n(0(), y) -> 0(),
                 p(s x, x) -> p(if(gt(x, x), id x, id x), s x),
               p(s x, s y) -> s s p(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)),
                 p(0(), y) -> y,
              p(id x, s y) -> s p(x, if(gt(s y, y), y, s y)),
              gt(s x, s y) -> gt(x, y),
              gt(s x, 0()) -> true(),
                gt(0(), y) -> false(),
                     not x -> if(x, false(), true()),
                      id x -> x,
                     h s x -> f x,
                     h 0() -> false()}
      Open
     
     
     
     
     
     
     
     SCC (3):
      Strict:
       {   p#(s x, x) -> p#(if(gt(x, x), id x, id x), s x),
         p#(s x, s y) -> p#(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)),
        p#(id x, s y) -> p#(x, if(gt(s y, y), y, s y))}
      Weak:
      {   if(true(), x, y) -> x,
         if(false(), x, y) -> y,
           and(x, false()) -> false(),
       and(true(), true()) -> true(),
                     f s x -> h x,
                     f 0() -> true(),
                       t x -> p(x, x),
               g(s x, s y) -> if(and(f s x, f s y), t g(k(minus(m(x, y), n(x, y)), s s 0()), k(n(s x, s y), s s 0())), g(minus(m(x, y), n(x, y)), n(s x, s y))),
               k(s x, s y) -> s k(minus(x, y), s y),
               k(0(), s y) -> 0(),
             minus(x, 0()) -> x,
           minus(s x, s y) -> minus(x, y),
                 m(x, 0()) -> x,
               m(s x, s y) -> s m(x, y),
                 m(0(), y) -> y,
                 n(x, 0()) -> 0(),
               n(s x, s y) -> s n(x, y),
                 n(0(), y) -> 0(),
                 p(s x, x) -> p(if(gt(x, x), id x, id x), s x),
               p(s x, s y) -> s s p(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)),
                 p(0(), y) -> y,
              p(id x, s y) -> s p(x, if(gt(s y, y), y, s y)),
              gt(s x, s y) -> gt(x, y),
              gt(s x, 0()) -> true(),
                gt(0(), y) -> false(),
                     not x -> if(x, false(), true()),
                      id x -> x,
                     h s x -> f x,
                     h 0() -> false()}
      Open
     
     
     
     
     
     
     
     
     
     
     SCC (1):
      Strict:
       {gt#(s x, s y) -> gt#(x, y)}
      Weak:
      {   if(true(), x, y) -> x,
         if(false(), x, y) -> y,
           and(x, false()) -> false(),
       and(true(), true()) -> true(),
                     f s x -> h x,
                     f 0() -> true(),
                       t x -> p(x, x),
               g(s x, s y) -> if(and(f s x, f s y), t g(k(minus(m(x, y), n(x, y)), s s 0()), k(n(s x, s y), s s 0())), g(minus(m(x, y), n(x, y)), n(s x, s y))),
               k(s x, s y) -> s k(minus(x, y), s y),
               k(0(), s y) -> 0(),
             minus(x, 0()) -> x,
           minus(s x, s y) -> minus(x, y),
                 m(x, 0()) -> x,
               m(s x, s y) -> s m(x, y),
                 m(0(), y) -> y,
                 n(x, 0()) -> 0(),
               n(s x, s y) -> s n(x, y),
                 n(0(), y) -> 0(),
                 p(s x, x) -> p(if(gt(x, x), id x, id x), s x),
               p(s x, s y) -> s s p(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)),
                 p(0(), y) -> y,
              p(id x, s y) -> s p(x, if(gt(s y, y), y, s y)),
              gt(s x, s y) -> gt(x, y),
              gt(s x, 0()) -> true(),
                gt(0(), y) -> false(),
                     not x -> if(x, false(), true()),
                      id x -> x,
                     h s x -> f x,
                     h 0() -> false()}
      Open
     
     SCC (1):
      Strict:
       {k#(s x, s y) -> k#(minus(x, y), s y)}
      Weak:
      {   if(true(), x, y) -> x,
         if(false(), x, y) -> y,
           and(x, false()) -> false(),
       and(true(), true()) -> true(),
                     f s x -> h x,
                     f 0() -> true(),
                       t x -> p(x, x),
               g(s x, s y) -> if(and(f s x, f s y), t g(k(minus(m(x, y), n(x, y)), s s 0()), k(n(s x, s y), s s 0())), g(minus(m(x, y), n(x, y)), n(s x, s y))),
               k(s x, s y) -> s k(minus(x, y), s y),
               k(0(), s y) -> 0(),
             minus(x, 0()) -> x,
           minus(s x, s y) -> minus(x, y),
                 m(x, 0()) -> x,
               m(s x, s y) -> s m(x, y),
                 m(0(), y) -> y,
                 n(x, 0()) -> 0(),
               n(s x, s y) -> s n(x, y),
                 n(0(), y) -> 0(),
                 p(s x, x) -> p(if(gt(x, x), id x, id x), s x),
               p(s x, s y) -> s s p(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)),
                 p(0(), y) -> y,
              p(id x, s y) -> s p(x, if(gt(s y, y), y, s y)),
              gt(s x, s y) -> gt(x, y),
              gt(s x, 0()) -> true(),
                gt(0(), y) -> false(),
                     not x -> if(x, false(), true()),
                      id x -> x,
                     h s x -> f x,
                     h 0() -> false()}
      Open
     
     SCC (1):
      Strict:
       {minus#(s x, s y) -> minus#(x, y)}
      Weak:
      {   if(true(), x, y) -> x,
         if(false(), x, y) -> y,
           and(x, false()) -> false(),
       and(true(), true()) -> true(),
                     f s x -> h x,
                     f 0() -> true(),
                       t x -> p(x, x),
               g(s x, s y) -> if(and(f s x, f s y), t g(k(minus(m(x, y), n(x, y)), s s 0()), k(n(s x, s y), s s 0())), g(minus(m(x, y), n(x, y)), n(s x, s y))),
               k(s x, s y) -> s k(minus(x, y), s y),
               k(0(), s y) -> 0(),
             minus(x, 0()) -> x,
           minus(s x, s y) -> minus(x, y),
                 m(x, 0()) -> x,
               m(s x, s y) -> s m(x, y),
                 m(0(), y) -> y,
                 n(x, 0()) -> 0(),
               n(s x, s y) -> s n(x, y),
                 n(0(), y) -> 0(),
                 p(s x, x) -> p(if(gt(x, x), id x, id x), s x),
               p(s x, s y) -> s s p(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)),
                 p(0(), y) -> y,
              p(id x, s y) -> s p(x, if(gt(s y, y), y, s y)),
              gt(s x, s y) -> gt(x, y),
              gt(s x, 0()) -> true(),
                gt(0(), y) -> false(),
                     not x -> if(x, false(), true()),
                      id x -> x,
                     h s x -> f x,
                     h 0() -> false()}
      Open
     
     SCC (1):
      Strict:
       {n#(s x, s y) -> n#(x, y)}
      Weak:
      {   if(true(), x, y) -> x,
         if(false(), x, y) -> y,
           and(x, false()) -> false(),
       and(true(), true()) -> true(),
                     f s x -> h x,
                     f 0() -> true(),
                       t x -> p(x, x),
               g(s x, s y) -> if(and(f s x, f s y), t g(k(minus(m(x, y), n(x, y)), s s 0()), k(n(s x, s y), s s 0())), g(minus(m(x, y), n(x, y)), n(s x, s y))),
               k(s x, s y) -> s k(minus(x, y), s y),
               k(0(), s y) -> 0(),
             minus(x, 0()) -> x,
           minus(s x, s y) -> minus(x, y),
                 m(x, 0()) -> x,
               m(s x, s y) -> s m(x, y),
                 m(0(), y) -> y,
                 n(x, 0()) -> 0(),
               n(s x, s y) -> s n(x, y),
                 n(0(), y) -> 0(),
                 p(s x, x) -> p(if(gt(x, x), id x, id x), s x),
               p(s x, s y) -> s s p(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)),
                 p(0(), y) -> y,
              p(id x, s y) -> s p(x, if(gt(s y, y), y, s y)),
              gt(s x, s y) -> gt(x, y),
              gt(s x, 0()) -> true(),
                gt(0(), y) -> false(),
                     not x -> if(x, false(), true()),
                      id x -> x,
                     h s x -> f x,
                     h 0() -> false()}
      Open
     
     
     SCC (2):
      Strict:
       {f# s x -> h# x,
        h# s x -> f# x}
      Weak:
      {   if(true(), x, y) -> x,
         if(false(), x, y) -> y,
           and(x, false()) -> false(),
       and(true(), true()) -> true(),
                     f s x -> h x,
                     f 0() -> true(),
                       t x -> p(x, x),
               g(s x, s y) -> if(and(f s x, f s y), t g(k(minus(m(x, y), n(x, y)), s s 0()), k(n(s x, s y), s s 0())), g(minus(m(x, y), n(x, y)), n(s x, s y))),
               k(s x, s y) -> s k(minus(x, y), s y),
               k(0(), s y) -> 0(),
             minus(x, 0()) -> x,
           minus(s x, s y) -> minus(x, y),
                 m(x, 0()) -> x,
               m(s x, s y) -> s m(x, y),
                 m(0(), y) -> y,
                 n(x, 0()) -> 0(),
               n(s x, s y) -> s n(x, y),
                 n(0(), y) -> 0(),
                 p(s x, x) -> p(if(gt(x, x), id x, id x), s x),
               p(s x, s y) -> s s p(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)),
                 p(0(), y) -> y,
              p(id x, s y) -> s p(x, if(gt(s y, y), y, s y)),
              gt(s x, s y) -> gt(x, y),
              gt(s x, 0()) -> true(),
                gt(0(), y) -> false(),
                     not x -> if(x, false(), true()),
                      id x -> x,
                     h s x -> f x,
                     h 0() -> false()}
      Open