MAYBE
TRS:
 {          plus(s(x), x) -> plus(if(gt(x, x), id(x), id(x)), s(x)),
         plus(s(x), s(y)) -> s(s(plus(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y))))),
        plus(id(x), s(y)) -> s(plus(x, if(gt(s(y), y), y, s(y)))),
          plus(zero(), y) -> y,
  times(x, plus(y, s(z))) -> plus(times(x, plus(y, times(s(z), 0()))), times(x, s(z))),
           times(x, s(y)) -> plus(times(x, y), x),
            times(x, 0()) -> 0(),
         if(true(), x, y) -> x,
        if(false(), x, y) -> y,
           gt(s(x), s(y)) -> gt(x, y),
         gt(s(x), zero()) -> true(),
            gt(zero(), y) -> false(),
                   not(x) -> if(x, false(), true()),
                    id(x) -> x}
 DP:
  Strict:
   {          plus#(s(x), x) -> plus#(if(gt(x, x), id(x), id(x)), s(x)),
              plus#(s(x), x) -> if#(gt(x, x), id(x), id(x)),
              plus#(s(x), x) -> gt#(x, x),
              plus#(s(x), x) -> id#(x),
           plus#(s(x), s(y)) -> plus#(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y))),
           plus#(s(x), s(y)) -> if#(gt(x, y), x, y),
           plus#(s(x), s(y)) -> if#(not(gt(x, y)), id(x), id(y)),
           plus#(s(x), s(y)) -> gt#(x, y),
           plus#(s(x), s(y)) -> not#(gt(x, y)),
           plus#(s(x), s(y)) -> id#(x),
           plus#(s(x), s(y)) -> id#(y),
          plus#(id(x), s(y)) -> plus#(x, if(gt(s(y), y), y, s(y))),
          plus#(id(x), s(y)) -> if#(gt(s(y), y), y, s(y)),
          plus#(id(x), s(y)) -> gt#(s(y), y),
    times#(x, plus(y, s(z))) -> plus#(y, times(s(z), 0())),
    times#(x, plus(y, s(z))) -> plus#(times(x, plus(y, times(s(z), 0()))), times(x, s(z))),
    times#(x, plus(y, s(z))) -> times#(x, plus(y, times(s(z), 0()))),
    times#(x, plus(y, s(z))) -> times#(x, s(z)),
    times#(x, plus(y, s(z))) -> times#(s(z), 0()),
             times#(x, s(y)) -> plus#(times(x, y), x),
             times#(x, s(y)) -> times#(x, y),
             gt#(s(x), s(y)) -> gt#(x, y),
                     not#(x) -> if#(x, false(), true())}
  Weak:
  {          plus(s(x), x) -> plus(if(gt(x, x), id(x), id(x)), s(x)),
          plus(s(x), s(y)) -> s(s(plus(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y))))),
         plus(id(x), s(y)) -> s(plus(x, if(gt(s(y), y), y, s(y)))),
           plus(zero(), y) -> y,
   times(x, plus(y, s(z))) -> plus(times(x, plus(y, times(s(z), 0()))), times(x, s(z))),
            times(x, s(y)) -> plus(times(x, y), x),
             times(x, 0()) -> 0(),
          if(true(), x, y) -> x,
         if(false(), x, y) -> y,
            gt(s(x), s(y)) -> gt(x, y),
          gt(s(x), zero()) -> true(),
             gt(zero(), y) -> false(),
                    not(x) -> if(x, false(), true()),
                     id(x) -> x}
  EDG:
   {
    (times#(x, plus(y, s(z))) -> plus#(y, times(s(z), 0())), plus#(id(x), s(y)) -> gt#(s(y), y))
    (times#(x, plus(y, s(z))) -> plus#(y, times(s(z), 0())), plus#(id(x), s(y)) -> if#(gt(s(y), y), y, s(y)))
    (times#(x, plus(y, s(z))) -> plus#(y, times(s(z), 0())), plus#(id(x), s(y)) -> plus#(x, if(gt(s(y), y), y, s(y))))
    (times#(x, plus(y, s(z))) -> plus#(y, times(s(z), 0())), plus#(s(x), s(y)) -> id#(y))
    (times#(x, plus(y, s(z))) -> plus#(y, times(s(z), 0())), plus#(s(x), s(y)) -> id#(x))
    (times#(x, plus(y, s(z))) -> plus#(y, times(s(z), 0())), plus#(s(x), s(y)) -> not#(gt(x, y)))
    (times#(x, plus(y, s(z))) -> plus#(y, times(s(z), 0())), plus#(s(x), s(y)) -> gt#(x, y))
    (times#(x, plus(y, s(z))) -> plus#(y, times(s(z), 0())), plus#(s(x), s(y)) -> if#(not(gt(x, y)), id(x), id(y)))
    (times#(x, plus(y, s(z))) -> plus#(y, times(s(z), 0())), plus#(s(x), s(y)) -> if#(gt(x, y), x, y))
    (times#(x, plus(y, s(z))) -> plus#(y, times(s(z), 0())), plus#(s(x), s(y)) -> plus#(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y))))
    (times#(x, plus(y, s(z))) -> plus#(y, times(s(z), 0())), plus#(s(x), x) -> id#(x))
    (times#(x, plus(y, s(z))) -> plus#(y, times(s(z), 0())), plus#(s(x), x) -> gt#(x, x))
    (times#(x, plus(y, s(z))) -> plus#(y, times(s(z), 0())), plus#(s(x), x) -> if#(gt(x, x), id(x), id(x)))
    (times#(x, plus(y, s(z))) -> plus#(y, times(s(z), 0())), plus#(s(x), x) -> plus#(if(gt(x, x), id(x), id(x)), s(x)))
    (plus#(s(x), x) -> plus#(if(gt(x, x), id(x), id(x)), s(x)), plus#(id(x), s(y)) -> gt#(s(y), y))
    (plus#(s(x), x) -> plus#(if(gt(x, x), id(x), id(x)), s(x)), plus#(id(x), s(y)) -> if#(gt(s(y), y), y, s(y)))
    (plus#(s(x), x) -> plus#(if(gt(x, x), id(x), id(x)), s(x)), plus#(id(x), s(y)) -> plus#(x, if(gt(s(y), y), y, s(y))))
    (plus#(s(x), x) -> plus#(if(gt(x, x), id(x), id(x)), s(x)), plus#(s(x), s(y)) -> id#(y))
    (plus#(s(x), x) -> plus#(if(gt(x, x), id(x), id(x)), s(x)), plus#(s(x), s(y)) -> id#(x))
    (plus#(s(x), x) -> plus#(if(gt(x, x), id(x), id(x)), s(x)), plus#(s(x), s(y)) -> not#(gt(x, y)))
    (plus#(s(x), x) -> plus#(if(gt(x, x), id(x), id(x)), s(x)), plus#(s(x), s(y)) -> gt#(x, y))
    (plus#(s(x), x) -> plus#(if(gt(x, x), id(x), id(x)), s(x)), plus#(s(x), s(y)) -> if#(not(gt(x, y)), id(x), id(y)))
    (plus#(s(x), x) -> plus#(if(gt(x, x), id(x), id(x)), s(x)), plus#(s(x), s(y)) -> if#(gt(x, y), x, y))
    (plus#(s(x), x) -> plus#(if(gt(x, x), id(x), id(x)), s(x)), plus#(s(x), s(y)) -> plus#(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y))))
    (plus#(s(x), x) -> plus#(if(gt(x, x), id(x), id(x)), s(x)), plus#(s(x), x) -> id#(x))
    (plus#(s(x), x) -> plus#(if(gt(x, x), id(x), id(x)), s(x)), plus#(s(x), x) -> gt#(x, x))
    (plus#(s(x), x) -> plus#(if(gt(x, x), id(x), id(x)), s(x)), plus#(s(x), x) -> if#(gt(x, x), id(x), id(x)))
    (plus#(s(x), x) -> plus#(if(gt(x, x), id(x), id(x)), s(x)), plus#(s(x), x) -> plus#(if(gt(x, x), id(x), id(x)), s(x)))
    (plus#(id(x), s(y)) -> gt#(s(y), y), gt#(s(x), s(y)) -> gt#(x, y))
    (plus#(id(x), s(y)) -> plus#(x, if(gt(s(y), y), y, s(y))), plus#(id(x), s(y)) -> gt#(s(y), y))
    (plus#(id(x), s(y)) -> plus#(x, if(gt(s(y), y), y, s(y))), plus#(id(x), s(y)) -> if#(gt(s(y), y), y, s(y)))
    (plus#(id(x), s(y)) -> plus#(x, if(gt(s(y), y), y, s(y))), plus#(id(x), s(y)) -> plus#(x, if(gt(s(y), y), y, s(y))))
    (plus#(id(x), s(y)) -> plus#(x, if(gt(s(y), y), y, s(y))), plus#(s(x), s(y)) -> id#(y))
    (plus#(id(x), s(y)) -> plus#(x, if(gt(s(y), y), y, s(y))), plus#(s(x), s(y)) -> id#(x))
    (plus#(id(x), s(y)) -> plus#(x, if(gt(s(y), y), y, s(y))), plus#(s(x), s(y)) -> not#(gt(x, y)))
    (plus#(id(x), s(y)) -> plus#(x, if(gt(s(y), y), y, s(y))), plus#(s(x), s(y)) -> gt#(x, y))
    (plus#(id(x), s(y)) -> plus#(x, if(gt(s(y), y), y, s(y))), plus#(s(x), s(y)) -> if#(not(gt(x, y)), id(x), id(y)))
    (plus#(id(x), s(y)) -> plus#(x, if(gt(s(y), y), y, s(y))), plus#(s(x), s(y)) -> if#(gt(x, y), x, y))
    (plus#(id(x), s(y)) -> plus#(x, if(gt(s(y), y), y, s(y))), plus#(s(x), s(y)) -> plus#(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y))))
    (plus#(id(x), s(y)) -> plus#(x, if(gt(s(y), y), y, s(y))), plus#(s(x), x) -> id#(x))
    (plus#(id(x), s(y)) -> plus#(x, if(gt(s(y), y), y, s(y))), plus#(s(x), x) -> gt#(x, x))
    (plus#(id(x), s(y)) -> plus#(x, if(gt(s(y), y), y, s(y))), plus#(s(x), x) -> if#(gt(x, x), id(x), id(x)))
    (plus#(id(x), s(y)) -> plus#(x, if(gt(s(y), y), y, s(y))), plus#(s(x), x) -> plus#(if(gt(x, x), id(x), id(x)), s(x)))
    (times#(x, s(y)) -> times#(x, y), times#(x, s(y)) -> times#(x, y))
    (times#(x, s(y)) -> times#(x, y), times#(x, s(y)) -> plus#(times(x, y), x))
    (times#(x, s(y)) -> times#(x, y), times#(x, plus(y, s(z))) -> times#(s(z), 0()))
    (times#(x, s(y)) -> times#(x, y), times#(x, plus(y, s(z))) -> times#(x, s(z)))
    (times#(x, s(y)) -> times#(x, y), times#(x, plus(y, s(z))) -> times#(x, plus(y, times(s(z), 0()))))
    (times#(x, s(y)) -> times#(x, y), times#(x, plus(y, s(z))) -> plus#(times(x, plus(y, times(s(z), 0()))), times(x, s(z))))
    (times#(x, s(y)) -> times#(x, y), times#(x, plus(y, s(z))) -> plus#(y, times(s(z), 0())))
    (times#(x, plus(y, s(z))) -> plus#(times(x, plus(y, times(s(z), 0()))), times(x, s(z))), plus#(id(x), s(y)) -> gt#(s(y), y))
    (times#(x, plus(y, s(z))) -> plus#(times(x, plus(y, times(s(z), 0()))), times(x, s(z))), plus#(id(x), s(y)) -> if#(gt(s(y), y), y, s(y)))
    (times#(x, plus(y, s(z))) -> plus#(times(x, plus(y, times(s(z), 0()))), times(x, s(z))), plus#(id(x), s(y)) -> plus#(x, if(gt(s(y), y), y, s(y))))
    (times#(x, plus(y, s(z))) -> plus#(times(x, plus(y, times(s(z), 0()))), times(x, s(z))), plus#(s(x), s(y)) -> id#(y))
    (times#(x, plus(y, s(z))) -> plus#(times(x, plus(y, times(s(z), 0()))), times(x, s(z))), plus#(s(x), s(y)) -> id#(x))
    (times#(x, plus(y, s(z))) -> plus#(times(x, plus(y, times(s(z), 0()))), times(x, s(z))), plus#(s(x), s(y)) -> not#(gt(x, y)))
    (times#(x, plus(y, s(z))) -> plus#(times(x, plus(y, times(s(z), 0()))), times(x, s(z))), plus#(s(x), s(y)) -> gt#(x, y))
    (times#(x, plus(y, s(z))) -> plus#(times(x, plus(y, times(s(z), 0()))), times(x, s(z))), plus#(s(x), s(y)) -> if#(not(gt(x, y)), id(x), id(y)))
    (times#(x, plus(y, s(z))) -> plus#(times(x, plus(y, times(s(z), 0()))), times(x, s(z))), plus#(s(x), s(y)) -> if#(gt(x, y), x, y))
    (times#(x, plus(y, s(z))) -> plus#(times(x, plus(y, times(s(z), 0()))), times(x, s(z))), plus#(s(x), s(y)) -> plus#(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y))))
    (times#(x, plus(y, s(z))) -> plus#(times(x, plus(y, times(s(z), 0()))), times(x, s(z))), plus#(s(x), x) -> id#(x))
    (times#(x, plus(y, s(z))) -> plus#(times(x, plus(y, times(s(z), 0()))), times(x, s(z))), plus#(s(x), x) -> gt#(x, x))
    (times#(x, plus(y, s(z))) -> plus#(times(x, plus(y, times(s(z), 0()))), times(x, s(z))), plus#(s(x), x) -> if#(gt(x, x), id(x), id(x)))
    (times#(x, plus(y, s(z))) -> plus#(times(x, plus(y, times(s(z), 0()))), times(x, s(z))), plus#(s(x), x) -> plus#(if(gt(x, x), id(x), id(x)), s(x)))
    (times#(x, plus(y, s(z))) -> times#(x, plus(y, times(s(z), 0()))), times#(x, plus(y, s(z))) -> plus#(y, times(s(z), 0())))
    (times#(x, plus(y, s(z))) -> times#(x, plus(y, times(s(z), 0()))), times#(x, plus(y, s(z))) -> plus#(times(x, plus(y, times(s(z), 0()))), times(x, s(z))))
    (times#(x, plus(y, s(z))) -> times#(x, plus(y, times(s(z), 0()))), times#(x, plus(y, s(z))) -> times#(x, plus(y, times(s(z), 0()))))
    (times#(x, plus(y, s(z))) -> times#(x, plus(y, times(s(z), 0()))), times#(x, plus(y, s(z))) -> times#(x, s(z)))
    (times#(x, plus(y, s(z))) -> times#(x, plus(y, times(s(z), 0()))), times#(x, plus(y, s(z))) -> times#(s(z), 0()))
    (times#(x, plus(y, s(z))) -> times#(x, plus(y, times(s(z), 0()))), times#(x, s(y)) -> plus#(times(x, y), x))
    (times#(x, plus(y, s(z))) -> times#(x, plus(y, times(s(z), 0()))), times#(x, s(y)) -> times#(x, y))
    (gt#(s(x), s(y)) -> gt#(x, y), gt#(s(x), s(y)) -> gt#(x, y))
    (plus#(s(x), s(y)) -> gt#(x, y), gt#(s(x), s(y)) -> gt#(x, y))
    (plus#(s(x), x) -> gt#(x, x), gt#(s(x), s(y)) -> gt#(x, y))
    (plus#(s(x), s(y)) -> plus#(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y))), plus#(s(x), x) -> plus#(if(gt(x, x), id(x), id(x)), s(x)))
    (plus#(s(x), s(y)) -> plus#(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y))), plus#(s(x), x) -> if#(gt(x, x), id(x), id(x)))
    (plus#(s(x), s(y)) -> plus#(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y))), plus#(s(x), x) -> gt#(x, x))
    (plus#(s(x), s(y)) -> plus#(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y))), plus#(s(x), x) -> id#(x))
    (plus#(s(x), s(y)) -> plus#(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y))), plus#(s(x), s(y)) -> plus#(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y))))
    (plus#(s(x), s(y)) -> plus#(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y))), plus#(s(x), s(y)) -> if#(gt(x, y), x, y))
    (plus#(s(x), s(y)) -> plus#(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y))), plus#(s(x), s(y)) -> if#(not(gt(x, y)), id(x), id(y)))
    (plus#(s(x), s(y)) -> plus#(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y))), plus#(s(x), s(y)) -> gt#(x, y))
    (plus#(s(x), s(y)) -> plus#(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y))), plus#(s(x), s(y)) -> not#(gt(x, y)))
    (plus#(s(x), s(y)) -> plus#(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y))), plus#(s(x), s(y)) -> id#(x))
    (plus#(s(x), s(y)) -> plus#(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y))), plus#(s(x), s(y)) -> id#(y))
    (plus#(s(x), s(y)) -> plus#(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y))), plus#(id(x), s(y)) -> plus#(x, if(gt(s(y), y), y, s(y))))
    (plus#(s(x), s(y)) -> plus#(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y))), plus#(id(x), s(y)) -> if#(gt(s(y), y), y, s(y)))
    (plus#(s(x), s(y)) -> plus#(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y))), plus#(id(x), s(y)) -> gt#(s(y), y))
    (times#(x, plus(y, s(z))) -> times#(x, s(z)), times#(x, s(y)) -> plus#(times(x, y), x))
    (times#(x, plus(y, s(z))) -> times#(x, s(z)), times#(x, s(y)) -> times#(x, y))
    (times#(x, s(y)) -> plus#(times(x, y), x), plus#(s(x), x) -> plus#(if(gt(x, x), id(x), id(x)), s(x)))
    (times#(x, s(y)) -> plus#(times(x, y), x), plus#(s(x), x) -> if#(gt(x, x), id(x), id(x)))
    (times#(x, s(y)) -> plus#(times(x, y), x), plus#(s(x), x) -> gt#(x, x))
    (times#(x, s(y)) -> plus#(times(x, y), x), plus#(s(x), x) -> id#(x))
    (times#(x, s(y)) -> plus#(times(x, y), x), plus#(s(x), s(y)) -> plus#(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y))))
    (times#(x, s(y)) -> plus#(times(x, y), x), plus#(s(x), s(y)) -> if#(gt(x, y), x, y))
    (times#(x, s(y)) -> plus#(times(x, y), x), plus#(s(x), s(y)) -> if#(not(gt(x, y)), id(x), id(y)))
    (times#(x, s(y)) -> plus#(times(x, y), x), plus#(s(x), s(y)) -> gt#(x, y))
    (times#(x, s(y)) -> plus#(times(x, y), x), plus#(s(x), s(y)) -> not#(gt(x, y)))
    (times#(x, s(y)) -> plus#(times(x, y), x), plus#(s(x), s(y)) -> id#(x))
    (times#(x, s(y)) -> plus#(times(x, y), x), plus#(s(x), s(y)) -> id#(y))
    (times#(x, s(y)) -> plus#(times(x, y), x), plus#(id(x), s(y)) -> plus#(x, if(gt(s(y), y), y, s(y))))
    (times#(x, s(y)) -> plus#(times(x, y), x), plus#(id(x), s(y)) -> if#(gt(s(y), y), y, s(y)))
    (times#(x, s(y)) -> plus#(times(x, y), x), plus#(id(x), s(y)) -> gt#(s(y), y))
    (plus#(s(x), s(y)) -> not#(gt(x, y)), not#(x) -> if#(x, false(), true()))
   }
   SCCS:
    Scc:
     {gt#(s(x), s(y)) -> gt#(x, y)}
    Scc:
     {times#(x, plus(y, s(z))) -> times#(x, plus(y, times(s(z), 0()))),
      times#(x, plus(y, s(z))) -> times#(x, s(z)),
               times#(x, s(y)) -> times#(x, y)}
    Scc:
     {    plus#(s(x), x) -> plus#(if(gt(x, x), id(x), id(x)), s(x)),
       plus#(s(x), s(y)) -> plus#(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y))),
      plus#(id(x), s(y)) -> plus#(x, if(gt(s(y), y), y, s(y)))}
    SCC:
     Strict:
      {gt#(s(x), s(y)) -> gt#(x, y)}
     Weak:
     {          plus(s(x), x) -> plus(if(gt(x, x), id(x), id(x)), s(x)),
             plus(s(x), s(y)) -> s(s(plus(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y))))),
            plus(id(x), s(y)) -> s(plus(x, if(gt(s(y), y), y, s(y)))),
              plus(zero(), y) -> y,
      times(x, plus(y, s(z))) -> plus(times(x, plus(y, times(s(z), 0()))), times(x, s(z))),
               times(x, s(y)) -> plus(times(x, y), x),
                times(x, 0()) -> 0(),
             if(true(), x, y) -> x,
            if(false(), x, y) -> y,
               gt(s(x), s(y)) -> gt(x, y),
             gt(s(x), zero()) -> true(),
                gt(zero(), y) -> false(),
                       not(x) -> if(x, false(), true()),
                        id(x) -> x}
     SPSC:
      Simple Projection:
       pi(gt#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {times#(x, plus(y, s(z))) -> times#(x, plus(y, times(s(z), 0()))),
       times#(x, plus(y, s(z))) -> times#(x, s(z)),
                times#(x, s(y)) -> times#(x, y)}
     Weak:
     {          plus(s(x), x) -> plus(if(gt(x, x), id(x), id(x)), s(x)),
             plus(s(x), s(y)) -> s(s(plus(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y))))),
            plus(id(x), s(y)) -> s(plus(x, if(gt(s(y), y), y, s(y)))),
              plus(zero(), y) -> y,
      times(x, plus(y, s(z))) -> plus(times(x, plus(y, times(s(z), 0()))), times(x, s(z))),
               times(x, s(y)) -> plus(times(x, y), x),
                times(x, 0()) -> 0(),
             if(true(), x, y) -> x,
            if(false(), x, y) -> y,
               gt(s(x), s(y)) -> gt(x, y),
             gt(s(x), zero()) -> true(),
                gt(zero(), y) -> false(),
                       not(x) -> if(x, false(), true()),
                        id(x) -> x}
     Fail
    SCC:
     Strict:
      {    plus#(s(x), x) -> plus#(if(gt(x, x), id(x), id(x)), s(x)),
        plus#(s(x), s(y)) -> plus#(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y))),
       plus#(id(x), s(y)) -> plus#(x, if(gt(s(y), y), y, s(y)))}
     Weak:
     {          plus(s(x), x) -> plus(if(gt(x, x), id(x), id(x)), s(x)),
             plus(s(x), s(y)) -> s(s(plus(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y))))),
            plus(id(x), s(y)) -> s(plus(x, if(gt(s(y), y), y, s(y)))),
              plus(zero(), y) -> y,
      times(x, plus(y, s(z))) -> plus(times(x, plus(y, times(s(z), 0()))), times(x, s(z))),
               times(x, s(y)) -> plus(times(x, y), x),
                times(x, 0()) -> 0(),
             if(true(), x, y) -> x,
            if(false(), x, y) -> y,
               gt(s(x), s(y)) -> gt(x, y),
             gt(s(x), zero()) -> true(),
                gt(zero(), y) -> false(),
                       not(x) -> if(x, false(), true()),
                        id(x) -> x}
     Fail