MAYBE

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict Trs:
  { 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)
  , times(x, y) -> ifTimes(ge(0(), x), 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() }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We add following dependency tuples:

Strict DPs:
  { lcm^#(x, y) ->
    c_1(lcmIter^#(x, y, 0(), times(x, y)), times^#(x, y))
  , lcmIter^#(x, y, z, u) ->
    c_2(if^#(or(ge(0(), x), ge(z, u)), x, y, z, u),
        or^#(ge(0(), x), ge(z, u)),
        ge^#(0(), x),
        ge^#(z, u))
  , times^#(x, y) -> c_3(ifTimes^#(ge(0(), x), x, y), ge^#(0(), x))
  , if^#(true(), x, y, z, u) -> c_4()
  , if^#(false(), x, y, z, u) ->
    c_5(if2^#(divisible(z, y), x, y, z, u), divisible^#(z, y))
  , or^#(true(), y) -> c_6()
  , or^#(false(), y) -> c_7()
  , ge^#(x, 0()) -> c_8()
  , ge^#(0(), s(y)) -> c_9()
  , ge^#(s(x), s(y)) -> c_10(ge^#(x, y))
  , ifTimes^#(true(), x, y) -> c_17()
  , ifTimes^#(false(), x, y) ->
    c_18(plus^#(y, times(y, p(x))), times^#(y, p(x)), p^#(x))
  , if2^#(true(), x, y, z, u) -> c_11()
  , if2^#(false(), x, y, z, u) ->
    c_12(lcmIter^#(x, y, plus(x, z), u), plus^#(x, z))
  , divisible^#(0(), s(y)) -> c_13()
  , divisible^#(s(x), s(y)) -> c_14(div^#(s(x), s(y), s(y)))
  , plus^#(0(), y) -> c_15()
  , plus^#(s(x), y) -> c_16(plus^#(x, y))
  , div^#(x, y, 0()) -> c_21(divisible^#(x, y))
  , div^#(0(), y, s(z)) -> c_22()
  , div^#(s(x), y, s(z)) -> c_23(div^#(x, y, z))
  , p^#(0()) -> c_19()
  , p^#(s(x)) -> c_20()
  , a^#() -> c_24()
  , a^#() -> c_25() }

and mark the set of starting terms.

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict DPs:
  { lcm^#(x, y) ->
    c_1(lcmIter^#(x, y, 0(), times(x, y)), times^#(x, y))
  , lcmIter^#(x, y, z, u) ->
    c_2(if^#(or(ge(0(), x), ge(z, u)), x, y, z, u),
        or^#(ge(0(), x), ge(z, u)),
        ge^#(0(), x),
        ge^#(z, u))
  , times^#(x, y) -> c_3(ifTimes^#(ge(0(), x), x, y), ge^#(0(), x))
  , if^#(true(), x, y, z, u) -> c_4()
  , if^#(false(), x, y, z, u) ->
    c_5(if2^#(divisible(z, y), x, y, z, u), divisible^#(z, y))
  , or^#(true(), y) -> c_6()
  , or^#(false(), y) -> c_7()
  , ge^#(x, 0()) -> c_8()
  , ge^#(0(), s(y)) -> c_9()
  , ge^#(s(x), s(y)) -> c_10(ge^#(x, y))
  , ifTimes^#(true(), x, y) -> c_17()
  , ifTimes^#(false(), x, y) ->
    c_18(plus^#(y, times(y, p(x))), times^#(y, p(x)), p^#(x))
  , if2^#(true(), x, y, z, u) -> c_11()
  , if2^#(false(), x, y, z, u) ->
    c_12(lcmIter^#(x, y, plus(x, z), u), plus^#(x, z))
  , divisible^#(0(), s(y)) -> c_13()
  , divisible^#(s(x), s(y)) -> c_14(div^#(s(x), s(y), s(y)))
  , plus^#(0(), y) -> c_15()
  , plus^#(s(x), y) -> c_16(plus^#(x, y))
  , div^#(x, y, 0()) -> c_21(divisible^#(x, y))
  , div^#(0(), y, s(z)) -> c_22()
  , div^#(s(x), y, s(z)) -> c_23(div^#(x, y, z))
  , p^#(0()) -> c_19()
  , p^#(s(x)) -> c_20()
  , a^#() -> c_24()
  , a^#() -> c_25() }
Weak Trs:
  { 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)
  , times(x, y) -> ifTimes(ge(0(), x), 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() }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We estimate the number of application of
{4,6,7,8,9,11,13,15,17,20,22,23,24,25} by applications of
Pre({4,6,7,8,9,11,13,15,17,20,22,23,24,25}) =
{2,3,5,10,12,14,18,19,21}. Here rules are labeled as follows:

  DPs:
    { 1: lcm^#(x, y) ->
         c_1(lcmIter^#(x, y, 0(), times(x, y)), times^#(x, y))
    , 2: lcmIter^#(x, y, z, u) ->
         c_2(if^#(or(ge(0(), x), ge(z, u)), x, y, z, u),
             or^#(ge(0(), x), ge(z, u)),
             ge^#(0(), x),
             ge^#(z, u))
    , 3: times^#(x, y) ->
         c_3(ifTimes^#(ge(0(), x), x, y), ge^#(0(), x))
    , 4: if^#(true(), x, y, z, u) -> c_4()
    , 5: if^#(false(), x, y, z, u) ->
         c_5(if2^#(divisible(z, y), x, y, z, u), divisible^#(z, y))
    , 6: or^#(true(), y) -> c_6()
    , 7: or^#(false(), y) -> c_7()
    , 8: ge^#(x, 0()) -> c_8()
    , 9: ge^#(0(), s(y)) -> c_9()
    , 10: ge^#(s(x), s(y)) -> c_10(ge^#(x, y))
    , 11: ifTimes^#(true(), x, y) -> c_17()
    , 12: ifTimes^#(false(), x, y) ->
          c_18(plus^#(y, times(y, p(x))), times^#(y, p(x)), p^#(x))
    , 13: if2^#(true(), x, y, z, u) -> c_11()
    , 14: if2^#(false(), x, y, z, u) ->
          c_12(lcmIter^#(x, y, plus(x, z), u), plus^#(x, z))
    , 15: divisible^#(0(), s(y)) -> c_13()
    , 16: divisible^#(s(x), s(y)) -> c_14(div^#(s(x), s(y), s(y)))
    , 17: plus^#(0(), y) -> c_15()
    , 18: plus^#(s(x), y) -> c_16(plus^#(x, y))
    , 19: div^#(x, y, 0()) -> c_21(divisible^#(x, y))
    , 20: div^#(0(), y, s(z)) -> c_22()
    , 21: div^#(s(x), y, s(z)) -> c_23(div^#(x, y, z))
    , 22: p^#(0()) -> c_19()
    , 23: p^#(s(x)) -> c_20()
    , 24: a^#() -> c_24()
    , 25: a^#() -> c_25() }

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict DPs:
  { lcm^#(x, y) ->
    c_1(lcmIter^#(x, y, 0(), times(x, y)), times^#(x, y))
  , lcmIter^#(x, y, z, u) ->
    c_2(if^#(or(ge(0(), x), ge(z, u)), x, y, z, u),
        or^#(ge(0(), x), ge(z, u)),
        ge^#(0(), x),
        ge^#(z, u))
  , times^#(x, y) -> c_3(ifTimes^#(ge(0(), x), x, y), ge^#(0(), x))
  , if^#(false(), x, y, z, u) ->
    c_5(if2^#(divisible(z, y), x, y, z, u), divisible^#(z, y))
  , ge^#(s(x), s(y)) -> c_10(ge^#(x, y))
  , ifTimes^#(false(), x, y) ->
    c_18(plus^#(y, times(y, p(x))), times^#(y, p(x)), p^#(x))
  , if2^#(false(), x, y, z, u) ->
    c_12(lcmIter^#(x, y, plus(x, z), u), plus^#(x, z))
  , divisible^#(s(x), s(y)) -> c_14(div^#(s(x), s(y), s(y)))
  , plus^#(s(x), y) -> c_16(plus^#(x, y))
  , div^#(x, y, 0()) -> c_21(divisible^#(x, y))
  , div^#(s(x), y, s(z)) -> c_23(div^#(x, y, z)) }
Weak DPs:
  { if^#(true(), x, y, z, u) -> c_4()
  , or^#(true(), y) -> c_6()
  , or^#(false(), y) -> c_7()
  , ge^#(x, 0()) -> c_8()
  , ge^#(0(), s(y)) -> c_9()
  , ifTimes^#(true(), x, y) -> c_17()
  , if2^#(true(), x, y, z, u) -> c_11()
  , divisible^#(0(), s(y)) -> c_13()
  , plus^#(0(), y) -> c_15()
  , div^#(0(), y, s(z)) -> c_22()
  , p^#(0()) -> c_19()
  , p^#(s(x)) -> c_20()
  , a^#() -> c_24()
  , a^#() -> c_25() }
Weak Trs:
  { 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)
  , times(x, y) -> ifTimes(ge(0(), x), 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() }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The following weak DPs constitute a sub-graph of the DG that is
closed under successors. The DPs are removed.

{ if^#(true(), x, y, z, u) -> c_4()
, or^#(true(), y) -> c_6()
, or^#(false(), y) -> c_7()
, ge^#(x, 0()) -> c_8()
, ge^#(0(), s(y)) -> c_9()
, ifTimes^#(true(), x, y) -> c_17()
, if2^#(true(), x, y, z, u) -> c_11()
, divisible^#(0(), s(y)) -> c_13()
, plus^#(0(), y) -> c_15()
, div^#(0(), y, s(z)) -> c_22()
, p^#(0()) -> c_19()
, p^#(s(x)) -> c_20()
, a^#() -> c_24()
, a^#() -> c_25() }

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict DPs:
  { lcm^#(x, y) ->
    c_1(lcmIter^#(x, y, 0(), times(x, y)), times^#(x, y))
  , lcmIter^#(x, y, z, u) ->
    c_2(if^#(or(ge(0(), x), ge(z, u)), x, y, z, u),
        or^#(ge(0(), x), ge(z, u)),
        ge^#(0(), x),
        ge^#(z, u))
  , times^#(x, y) -> c_3(ifTimes^#(ge(0(), x), x, y), ge^#(0(), x))
  , if^#(false(), x, y, z, u) ->
    c_5(if2^#(divisible(z, y), x, y, z, u), divisible^#(z, y))
  , ge^#(s(x), s(y)) -> c_10(ge^#(x, y))
  , ifTimes^#(false(), x, y) ->
    c_18(plus^#(y, times(y, p(x))), times^#(y, p(x)), p^#(x))
  , if2^#(false(), x, y, z, u) ->
    c_12(lcmIter^#(x, y, plus(x, z), u), plus^#(x, z))
  , divisible^#(s(x), s(y)) -> c_14(div^#(s(x), s(y), s(y)))
  , plus^#(s(x), y) -> c_16(plus^#(x, y))
  , div^#(x, y, 0()) -> c_21(divisible^#(x, y))
  , div^#(s(x), y, s(z)) -> c_23(div^#(x, y, z)) }
Weak Trs:
  { 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)
  , times(x, y) -> ifTimes(ge(0(), x), 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() }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

Due to missing edges in the dependency-graph, the right-hand sides
of following rules could be simplified:

  { lcmIter^#(x, y, z, u) ->
    c_2(if^#(or(ge(0(), x), ge(z, u)), x, y, z, u),
        or^#(ge(0(), x), ge(z, u)),
        ge^#(0(), x),
        ge^#(z, u))
  , times^#(x, y) -> c_3(ifTimes^#(ge(0(), x), x, y), ge^#(0(), x))
  , ifTimes^#(false(), x, y) ->
    c_18(plus^#(y, times(y, p(x))), times^#(y, p(x)), p^#(x)) }

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict DPs:
  { lcm^#(x, y) ->
    c_1(lcmIter^#(x, y, 0(), times(x, y)), times^#(x, y))
  , lcmIter^#(x, y, z, u) ->
    c_2(if^#(or(ge(0(), x), ge(z, u)), x, y, z, u), ge^#(z, u))
  , times^#(x, y) -> c_3(ifTimes^#(ge(0(), x), x, y))
  , if^#(false(), x, y, z, u) ->
    c_4(if2^#(divisible(z, y), x, y, z, u), divisible^#(z, y))
  , ge^#(s(x), s(y)) -> c_5(ge^#(x, y))
  , ifTimes^#(false(), x, y) ->
    c_6(plus^#(y, times(y, p(x))), times^#(y, p(x)))
  , if2^#(false(), x, y, z, u) ->
    c_7(lcmIter^#(x, y, plus(x, z), u), plus^#(x, z))
  , divisible^#(s(x), s(y)) -> c_8(div^#(s(x), s(y), s(y)))
  , plus^#(s(x), y) -> c_9(plus^#(x, y))
  , div^#(x, y, 0()) -> c_10(divisible^#(x, y))
  , div^#(s(x), y, s(z)) -> c_11(div^#(x, y, z)) }
Weak Trs:
  { 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)
  , times(x, y) -> ifTimes(ge(0(), x), 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() }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We replace rewrite rules by usable rules:

  Weak Usable Rules:
    { times(x, y) -> ifTimes(ge(0(), x), x, y)
    , 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)
    , 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) }

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict DPs:
  { lcm^#(x, y) ->
    c_1(lcmIter^#(x, y, 0(), times(x, y)), times^#(x, y))
  , lcmIter^#(x, y, z, u) ->
    c_2(if^#(or(ge(0(), x), ge(z, u)), x, y, z, u), ge^#(z, u))
  , times^#(x, y) -> c_3(ifTimes^#(ge(0(), x), x, y))
  , if^#(false(), x, y, z, u) ->
    c_4(if2^#(divisible(z, y), x, y, z, u), divisible^#(z, y))
  , ge^#(s(x), s(y)) -> c_5(ge^#(x, y))
  , ifTimes^#(false(), x, y) ->
    c_6(plus^#(y, times(y, p(x))), times^#(y, p(x)))
  , if2^#(false(), x, y, z, u) ->
    c_7(lcmIter^#(x, y, plus(x, z), u), plus^#(x, z))
  , divisible^#(s(x), s(y)) -> c_8(div^#(s(x), s(y), s(y)))
  , plus^#(s(x), y) -> c_9(plus^#(x, y))
  , div^#(x, y, 0()) -> c_10(divisible^#(x, y))
  , div^#(s(x), y, s(z)) -> c_11(div^#(x, y, z)) }
Weak Trs:
  { times(x, y) -> ifTimes(ge(0(), x), x, y)
  , 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)
  , 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) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

None of the processors succeeded.

Details of failed attempt(s):
-----------------------------
1) 'matrices' failed due to the following reason:
   
   None of the processors succeeded.
   
   Details of failed attempt(s):
   -----------------------------
   1) 'matrix interpretation of dimension 4' failed due to the
      following reason:
      
      Following exception was raised:
        stack overflow
   
   2) 'matrix interpretation of dimension 3' failed due to the
      following reason:
      
      The input cannot be shown compatible
   
   3) 'matrix interpretation of dimension 3' failed due to the
      following reason:
      
      The input cannot be shown compatible
   
   4) 'matrix interpretation of dimension 2' failed due to the
      following reason:
      
      The input cannot be shown compatible
   
   5) 'matrix interpretation of dimension 2' failed due to the
      following reason:
      
      The input cannot be shown compatible
   
   6) 'matrix interpretation of dimension 1' failed due to the
      following reason:
      
      The input cannot be shown compatible
   

2) 'empty' failed due to the following reason:
   
   Empty strict component of the problem is NOT empty.


Arrrr..