Problem AProVE 07 thiemann03

TIMEOUT

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

Strict Trs:
  { null(nil()) -> true()
  , null(add(n, x)) -> false()
  , tail(nil()) -> nil()
  , tail(add(n, x)) -> x
  , head(add(n, x)) -> n
  , app(nil(), y) -> y
  , app(add(n, x), y) -> add(n, app(x, y))
  , reverse(nil()) -> nil()
  , reverse(add(n, x)) -> app(reverse(x), add(n, nil()))
  , shuffle(x) -> shuff(x, nil())
  , shuff(x, y) -> if(null(x), x, y, app(y, add(head(x), nil())))
  , if(true(), x, y, z) -> y
  , if(false(), x, y, z) -> shuff(reverse(tail(x)), z) }
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:
  { null(nil()) -> true()
  , null(add(n, x)) -> false()
  , tail(add(n, x)) -> x
  , tail(nil()) -> nil()
  , head(add(n, x)) -> n
  , app(nil(), y) -> y
  , app(add(n, x), y) -> add(n, app(x, y))
  , reverse(nil()) -> nil()
  , reverse(add(n, x)) -> app(reverse(x), add(n, nil()))
  , shuffle(x) -> shuff(x, nil())
  , shuff(x, y) -> if(null(x), x, y, app(y, add(head(x), nil())))
  , if(true(), x, y, z) -> y
  , if(false(), x, y, z) -> shuff(reverse(tail(x)), z) }
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:
  { null(nil()) -> true()
  , null(add(n, x)) -> false()
  , tail(add(n, x)) -> x
  , tail(nil()) -> nil()
  , head(add(n, x)) -> n
  , app(nil(), y) -> y
  , app(add(n, x), y) -> add(n, app(x, y))
  , reverse(nil()) -> nil()
  , reverse(add(n, x)) -> app(reverse(x), add(n, nil()))
  , shuffle(x) -> shuff(x, nil())
  , shuff(x, y) -> if(null(x), x, y, app(y, add(head(x), nil())))
  , if(true(), x, y, z) -> y
  , if(false(), x, y, z) -> shuff(reverse(tail(x)), z) }
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:
  { null(nil()) -> true()
  , null(add(n, x)) -> false()
  , tail(add(n, x)) -> x
  , tail(nil()) -> nil()
  , head(add(n, x)) -> n
  , app(nil(), y) -> y
  , app(add(n, x), y) -> add(n, app(x, y))
  , reverse(nil()) -> nil()
  , reverse(add(n, x)) -> app(reverse(x), add(n, nil()))
  , shuffle(x) -> shuff(x, nil())
  , shuff(x, y) -> if(null(x), x, y, app(y, add(head(x), nil())))
  , if(true(), x, y, z) -> y
  , if(false(), x, y, z) -> shuff(reverse(tail(x)), z) }
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:
  { null(nil()) -> true()
  , null(add(n, x)) -> false()
  , tail(add(n, x)) -> x
  , tail(nil()) -> nil()
  , head(add(n, x)) -> n
  , app(nil(), y) -> y
  , app(add(n, x), y) -> add(n, app(x, y))
  , reverse(nil()) -> nil()
  , reverse(add(n, x)) -> app(reverse(x), add(n, nil()))
  , shuffle(x) -> shuff(x, nil())
  , shuff(x, y) -> if(null(x), x, y, app(y, add(head(x), nil())))
  , if(true(), x, y, z) -> y
  , if(false(), x, y, z) -> shuff(reverse(tail(x)), z) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The input cannot be shown compatible

Arrrr..