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()}
 DP:
  Strict:
   {     lcmIter#(x, y, z, u) -> if#(or(ge(0(), x), ge(z, u)), x, y, z, u),
         lcmIter#(x, y, z, u) -> or#(ge(0(), x), ge(z, u)),
         lcmIter#(x, y, z, u) -> ge#(z, u),
         lcmIter#(x, y, z, u) -> ge#(0(), x),
                 times#(x, y) -> ge#(0(), x),
                 times#(x, y) -> ifTimes#(ge(0(), x), x, y),
                   lcm#(x, y) -> lcmIter#(x, y, 0(), times(x, y)),
                   lcm#(x, y) -> times#(x, y),
     if#(false(), x, y, z, u) -> if2#(divisible(z, y), x, y, z, u),
     if#(false(), x, y, z, u) -> divisible#(z, y),
              ge#(s(x), s(y)) -> ge#(x, y),
    if2#(false(), x, y, z, u) -> lcmIter#(x, y, plus(x, z), u),
    if2#(false(), x, y, z, u) -> plus#(x, z),
       divisible#(s(x), s(y)) -> div#(s(x), s(y), s(y)),
               plus#(s(x), y) -> plus#(x, y),
      ifTimes#(false(), x, y) -> times#(y, p(x)),
      ifTimes#(false(), x, y) -> plus#(y, times(y, p(x))),
      ifTimes#(false(), x, y) -> p#(x),
              div#(x, y, 0()) -> divisible#(x, y),
          div#(s(x), y, s(z)) -> div#(x, y, z)}
  Weak:
  {     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()}
  EDG:
   {(ifTimes#(false(), x, y) -> times#(y, p(x)), times#(x, y) -> ifTimes#(ge(0(), x), x, y))
    (ifTimes#(false(), x, y) -> times#(y, p(x)), times#(x, y) -> ge#(0(), x))
    (lcmIter#(x, y, z, u) -> if#(or(ge(0(), x), ge(z, u)), x, y, z, u), if#(false(), x, y, z, u) -> divisible#(z, y))
    (lcmIter#(x, y, z, u) -> if#(or(ge(0(), x), ge(z, u)), x, y, z, u), if#(false(), x, y, z, u) -> if2#(divisible(z, y), x, y, z, u))
    (lcmIter#(x, y, z, u) -> ge#(z, u), ge#(s(x), s(y)) -> ge#(x, y))
    (if2#(false(), x, y, z, u) -> lcmIter#(x, y, plus(x, z), u), lcmIter#(x, y, z, u) -> ge#(0(), x))
    (if2#(false(), x, y, z, u) -> lcmIter#(x, y, plus(x, z), u), lcmIter#(x, y, z, u) -> ge#(z, u))
    (if2#(false(), x, y, z, u) -> lcmIter#(x, y, plus(x, z), u), lcmIter#(x, y, z, u) -> or#(ge(0(), x), ge(z, u)))
    (if2#(false(), x, y, z, u) -> lcmIter#(x, y, plus(x, z), u), lcmIter#(x, y, z, u) -> if#(or(ge(0(), x), ge(z, u)), x, y, z, u))
    (lcm#(x, y) -> times#(x, y), times#(x, y) -> ifTimes#(ge(0(), x), x, y))
    (lcm#(x, y) -> times#(x, y), times#(x, y) -> ge#(0(), x))
    (ge#(s(x), s(y)) -> ge#(x, y), ge#(s(x), s(y)) -> ge#(x, y))
    (plus#(s(x), y) -> plus#(x, y), plus#(s(x), y) -> plus#(x, y))
    (div#(s(x), y, s(z)) -> div#(x, y, z), div#(s(x), y, s(z)) -> div#(x, y, z))
    (div#(s(x), y, s(z)) -> div#(x, y, z), div#(x, y, 0()) -> divisible#(x, y))
    (div#(x, y, 0()) -> divisible#(x, y), divisible#(s(x), s(y)) -> div#(s(x), s(y), s(y)))
    (divisible#(s(x), s(y)) -> div#(s(x), s(y), s(y)), div#(s(x), y, s(z)) -> div#(x, y, z))
    (if#(false(), x, y, z, u) -> divisible#(z, y), divisible#(s(x), s(y)) -> div#(s(x), s(y), s(y)))
    (if2#(false(), x, y, z, u) -> plus#(x, z), plus#(s(x), y) -> plus#(x, y))
    (lcm#(x, y) -> lcmIter#(x, y, 0(), times(x, y)), lcmIter#(x, y, z, u) -> if#(or(ge(0(), x), ge(z, u)), x, y, z, u))
    (lcm#(x, y) -> lcmIter#(x, y, 0(), times(x, y)), lcmIter#(x, y, z, u) -> or#(ge(0(), x), ge(z, u)))
    (lcm#(x, y) -> lcmIter#(x, y, 0(), times(x, y)), lcmIter#(x, y, z, u) -> ge#(z, u))
    (lcm#(x, y) -> lcmIter#(x, y, 0(), times(x, y)), lcmIter#(x, y, z, u) -> ge#(0(), x))
    (if#(false(), x, y, z, u) -> if2#(divisible(z, y), x, y, z, u), if2#(false(), x, y, z, u) -> lcmIter#(x, y, plus(x, z), u))
    (if#(false(), x, y, z, u) -> if2#(divisible(z, y), x, y, z, u), if2#(false(), x, y, z, u) -> plus#(x, z))
    (times#(x, y) -> ifTimes#(ge(0(), x), x, y), ifTimes#(false(), x, y) -> times#(y, p(x)))
    (times#(x, y) -> ifTimes#(ge(0(), x), x, y), ifTimes#(false(), x, y) -> plus#(y, times(y, p(x))))
    (times#(x, y) -> ifTimes#(ge(0(), x), x, y), ifTimes#(false(), x, y) -> p#(x))
    (ifTimes#(false(), x, y) -> plus#(y, times(y, p(x))), plus#(s(x), y) -> plus#(x, y))}
   SCCS:
    Scc:
     {plus#(s(x), y) -> plus#(x, y)}
    Scc:
     {divisible#(s(x), s(y)) -> div#(s(x), s(y), s(y)),
             div#(x, y, 0()) -> divisible#(x, y),
         div#(s(x), y, s(z)) -> div#(x, y, z)}
    Scc:
     {ge#(s(x), s(y)) -> ge#(x, y)}
    Scc:
     {           times#(x, y) -> ifTimes#(ge(0(), x), x, y),
      ifTimes#(false(), x, y) -> times#(y, p(x))}
    Scc:
     {     lcmIter#(x, y, z, u) -> if#(or(ge(0(), x), ge(z, u)), x, y, z, u),
       if#(false(), x, y, z, u) -> if2#(divisible(z, y), x, y, z, u),
      if2#(false(), x, y, z, u) -> lcmIter#(x, y, plus(x, z), u)}
    SCC:
     Strict:
      {plus#(s(x), y) -> plus#(x, y)}
     Weak:
     {     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()}
     SPSC:
      Simple Projection:
       pi(plus#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {divisible#(s(x), s(y)) -> div#(s(x), s(y), s(y)),
              div#(x, y, 0()) -> divisible#(x, y),
          div#(s(x), y, s(z)) -> div#(x, y, z)}
     Weak:
     {     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()}
     SPSC:
      Simple Projection:
       pi(div#) = 0, pi(divisible#) = 0
      Strict:
       {divisible#(s(x), s(y)) -> div#(s(x), s(y), s(y)),
               div#(x, y, 0()) -> divisible#(x, y)}
      EDG:
       {(div#(x, y, 0()) -> divisible#(x, y), divisible#(s(x), s(y)) -> div#(s(x), s(y), s(y)))}
       SCCS:
        
        Qed
    SCC:
     Strict:
      {ge#(s(x), s(y)) -> ge#(x, y)}
     Weak:
     {     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()}
     SPSC:
      Simple Projection:
       pi(ge#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {           times#(x, y) -> ifTimes#(ge(0(), x), x, y),
       ifTimes#(false(), x, y) -> times#(y, p(x))}
     Weak:
     {     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
    SCC:
     Strict:
      {     lcmIter#(x, y, z, u) -> if#(or(ge(0(), x), ge(z, u)), x, y, z, u),
        if#(false(), x, y, z, u) -> if2#(divisible(z, y), x, y, z, u),
       if2#(false(), x, y, z, u) -> lcmIter#(x, y, plus(x, z), u)}
     Weak:
     {     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