MAYBE
MAYBE
TRS:
 {
       lcmIter(x, y, z, u) -> if(or(ge(0(), x), ge(z, u)), x, y, z, u),
               times(x, y) -> ifTimes(ge(0(), x), x, y),
                 lcm(x, y) -> lcmIter(x, y, 0(), times(x, y)),
    if(true(), x, y, z, u) -> z,
   if(false(), x, y, z, u) -> if2(divisible(z, y), x, y, z, u),
             or(true(), y) -> true(),
            or(false(), y) -> y,
                ge(x, 0()) -> true(),
             ge(0(), s(y)) -> false(),
            ge(s(x), s(y)) -> ge(x, y),
   if2(true(), x, y, z, u) -> z,
  if2(false(), x, y, z, u) -> lcmIter(x, y, plus(x, z), u),
      divisible(0(), s(y)) -> true(),
     divisible(s(x), s(y)) -> div(s(x), s(y), s(y)),
              plus(0(), y) -> y,
             plus(s(x), y) -> s(plus(x, y)),
     ifTimes(true(), x, y) -> 0(),
    ifTimes(false(), x, y) -> plus(y, times(y, p(x))),
                    p(0()) -> s(s(0())),
                   p(s(x)) -> x,
            div(x, y, 0()) -> divisible(x, y),
         div(0(), y, s(z)) -> false(),
        div(s(x), y, s(z)) -> div(x, y, z),
                       a() -> b(),
                       a() -> c()
 }
 DUP: We consider a duplicating system.
  Trs:
   {
         lcmIter(x, y, z, u) -> if(or(ge(0(), x), ge(z, u)), x, y, z, u),
                 times(x, y) -> ifTimes(ge(0(), x), x, y),
                   lcm(x, y) -> lcmIter(x, y, 0(), times(x, y)),
      if(true(), x, y, z, u) -> z,
     if(false(), x, y, z, u) -> if2(divisible(z, y), x, y, z, u),
               or(true(), y) -> true(),
              or(false(), y) -> y,
                  ge(x, 0()) -> true(),
               ge(0(), s(y)) -> false(),
              ge(s(x), s(y)) -> ge(x, y),
     if2(true(), x, y, z, u) -> z,
    if2(false(), x, y, z, u) -> lcmIter(x, y, plus(x, z), u),
        divisible(0(), s(y)) -> true(),
       divisible(s(x), s(y)) -> div(s(x), s(y), s(y)),
                plus(0(), y) -> y,
               plus(s(x), y) -> s(plus(x, y)),
       ifTimes(true(), x, y) -> 0(),
      ifTimes(false(), x, y) -> plus(y, times(y, p(x))),
                      p(0()) -> s(s(0())),
                     p(s(x)) -> x,
              div(x, y, 0()) -> divisible(x, y),
           div(0(), y, s(z)) -> false(),
          div(s(x), y, s(z)) -> div(x, y, z),
                         a() -> b(),
                         a() -> c()
   }
  Fail