MAYBE
Time: 0.009939
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:
  DP:
   {     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)}
  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()}
  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))
    (if#(false(), x, y, z, u) -> if2#(divisible(z, y), x, y, z, u), if2#(false(), x, y, z, u) -> plus#(x, z))
    (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))
    (lcm#(x, y) -> lcmIter#(x, y, 0(), times(x, y)), lcmIter#(x, y, z, u) -> ge#(0(), x))
    (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) -> or#(ge(0(), x), ge(z, u)))
    (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) -> 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))
    (div#(x, y, 0()) -> divisible#(x, y), divisible#(s x, s y) -> div#(s x, s y, s y))
    (times#(x, y) -> ifTimes#(ge(0(), x), x, y), ifTimes#(false(), x, 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) -> times#(y, p x))
    (divisible#(s x, s y) -> div#(s x, s y, s y), div#(s x, y, s z) -> div#(x, y, z))
    (plus#(s x, y) -> plus#(x, y), plus#(s x, y) -> plus#(x, y))
    (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))
    (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))
    (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) -> ge#(z, u))
    (if2#(false(), x, y, z, u) -> lcmIter#(x, y, plus(x, z), u), lcmIter#(x, y, z, u) -> ge#(0(), x))
    (lcmIter#(x, y, z, u) -> ge#(z, u), ge#(s x, s y) -> ge#(x, y))
    (div#(s x, y, s z) -> div#(x, y, z), div#(x, y, 0()) -> divisible#(x, y))
    (div#(s x, y, s z) -> div#(x, y, z), div#(s x, y, s z) -> div#(x, y, z))
    (ifTimes#(false(), x, y) -> plus#(y, times(y, p x)), plus#(s x, y) -> plus#(x, y))}
   STATUS:
    arrows: 0.927500
    SCCS (5):
     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:
      {ge#(s x, s y) -> ge#(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:
      {           times#(x, y) -> ifTimes#(ge(0(), x), x, y),
       ifTimes#(false(), x, y) -> times#(y, p x)}
     Scc:
      {plus#(s x, y) -> plus#(x, y)}
     
     
     
     SCC (3):
      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()}
      Open
     
     
     
     SCC (1):
      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()}
      Open
     
     SCC (3):
      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()}
      Open
     SCC (2):
      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()}
      Open
     
     
     SCC (1):
      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()}
      Open