Problem AProVE 04 JFP Ex51

TIMEOUT

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

Strict Trs:
  { minus_active(x, y) -> minus(x, y)
  , minus_active(0(), y) -> 0()
  , minus_active(s(x), s(y)) -> minus_active(x, y)
  , mark(0()) -> 0()
  , mark(s(x)) -> s(mark(x))
  , mark(minus(x, y)) -> minus_active(x, y)
  , mark(ge(x, y)) -> ge_active(x, y)
  , mark(div(x, y)) -> div_active(mark(x), y)
  , mark(if(x, y, z)) -> if_active(mark(x), y, z)
  , ge_active(x, y) -> ge(x, y)
  , ge_active(x, 0()) -> true()
  , ge_active(0(), s(y)) -> false()
  , ge_active(s(x), s(y)) -> ge_active(x, y)
  , div_active(x, y) -> div(x, y)
  , div_active(0(), s(y)) -> 0()
  , div_active(s(x), s(y)) ->
    if_active(ge_active(x, y), s(div(minus(x, y), s(y))), 0())
  , if_active(x, y, z) -> if(x, y, z)
  , if_active(true(), x, y) -> mark(x)
  , if_active(false(), x, y) -> mark(y) }
Obligation:
  innermost runtime complexity
Answer:
  TIMEOUT

Computation stopped due to timeout after 20.0 seconds.

Arrrr..

MAYBE

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

Strict Trs:
  { minus_active(0(), y) -> 0()
  , mark(0()) -> 0()
  , minus_active(s(x), s(y)) -> minus_active(x, y)
  , mark(s(x)) -> s(mark(x))
  , ge_active(x, 0()) -> true()
  , mark(minus(x, y)) -> minus_active(x, y)
  , ge_active(0(), s(y)) -> false()
  , mark(ge(x, y)) -> ge_active(x, y)
  , ge_active(s(x), s(y)) -> ge_active(x, y)
  , mark(div(x, y)) -> div_active(mark(x), y)
  , div_active(0(), s(y)) -> 0()
  , mark(if(x, y, z)) -> if_active(mark(x), y, z)
  , div_active(s(x), s(y)) ->
    if_active(ge_active(x, y), s(div(minus(x, y), s(y))), 0())
  , if_active(true(), x, y) -> mark(x)
  , minus_active(x, y) -> minus(x, y)
  , if_active(false(), x, y) -> mark(y)
  , ge_active(x, y) -> ge(x, y)
  , if_active(x, y, z) -> if(x, y, z)
  , div_active(x, y) -> div(x, y) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The input cannot be shown compatible

Arrrr..

MAYBE

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

Strict Trs:
  { minus_active(0(), y) -> 0()
  , mark(0()) -> 0()
  , minus_active(s(x), s(y)) -> minus_active(x, y)
  , mark(s(x)) -> s(mark(x))
  , ge_active(x, 0()) -> true()
  , mark(minus(x, y)) -> minus_active(x, y)
  , ge_active(0(), s(y)) -> false()
  , mark(ge(x, y)) -> ge_active(x, y)
  , ge_active(s(x), s(y)) -> ge_active(x, y)
  , mark(div(x, y)) -> div_active(mark(x), y)
  , div_active(0(), s(y)) -> 0()
  , mark(if(x, y, z)) -> if_active(mark(x), y, z)
  , div_active(s(x), s(y)) ->
    if_active(ge_active(x, y), s(div(minus(x, y), s(y))), 0())
  , if_active(true(), x, y) -> mark(x)
  , minus_active(x, y) -> minus(x, y)
  , if_active(false(), x, y) -> mark(y)
  , ge_active(x, y) -> ge(x, y)
  , if_active(x, y, z) -> if(x, y, z)
  , div_active(x, y) -> div(x, y) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The input cannot be shown compatible

Arrrr..

MAYBE

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

Strict Trs:
  { minus_active(0(), y) -> 0()
  , mark(0()) -> 0()
  , minus_active(s(x), s(y)) -> minus_active(x, y)
  , mark(s(x)) -> s(mark(x))
  , ge_active(x, 0()) -> true()
  , mark(minus(x, y)) -> minus_active(x, y)
  , ge_active(0(), s(y)) -> false()
  , mark(ge(x, y)) -> ge_active(x, y)
  , ge_active(s(x), s(y)) -> ge_active(x, y)
  , mark(div(x, y)) -> div_active(mark(x), y)
  , div_active(0(), s(y)) -> 0()
  , mark(if(x, y, z)) -> if_active(mark(x), y, z)
  , div_active(s(x), s(y)) ->
    if_active(ge_active(x, y), s(div(minus(x, y), s(y))), 0())
  , if_active(true(), x, y) -> mark(x)
  , minus_active(x, y) -> minus(x, y)
  , if_active(false(), x, y) -> mark(y)
  , ge_active(x, y) -> ge(x, y)
  , if_active(x, y, z) -> if(x, y, z)
  , div_active(x, y) -> div(x, y) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The input cannot be shown compatible

Arrrr..

MAYBE

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

Strict Trs:
  { minus_active(0(), y) -> 0()
  , mark(0()) -> 0()
  , minus_active(s(x), s(y)) -> minus_active(x, y)
  , mark(s(x)) -> s(mark(x))
  , ge_active(x, 0()) -> true()
  , mark(minus(x, y)) -> minus_active(x, y)
  , ge_active(0(), s(y)) -> false()
  , mark(ge(x, y)) -> ge_active(x, y)
  , ge_active(s(x), s(y)) -> ge_active(x, y)
  , mark(div(x, y)) -> div_active(mark(x), y)
  , div_active(0(), s(y)) -> 0()
  , mark(if(x, y, z)) -> if_active(mark(x), y, z)
  , div_active(s(x), s(y)) ->
    if_active(ge_active(x, y), s(div(minus(x, y), s(y))), 0())
  , if_active(true(), x, y) -> mark(x)
  , minus_active(x, y) -> minus(x, y)
  , if_active(false(), x, y) -> mark(y)
  , ge_active(x, y) -> ge(x, y)
  , if_active(x, y, z) -> if(x, y, z)
  , div_active(x, y) -> div(x, y) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The input cannot be shown compatible

Arrrr..