Problem AProVE 07 thiemann25

LMPO

Execution Time (secs)
0.086
Answer
MAYBE
InputAProVE 07 thiemann25
MAYBE

We consider the following Problem:

  Strict Trs:
    {  plus(0(), y) -> y
     , plus(s(x), y) -> s(plus(x, y))
     , lt(0(), s(y)) -> true()
     , lt(x, 0()) -> false()
     , lt(s(x), s(y)) -> lt(x, y)
     , fib(x) -> fibiter(x, 0(), 0(), s(0()))
     , fibiter(b, c, x, y) -> if(lt(c, b), b, c, x, y)
     , if(false(), b, c, x, y) -> x
     , if(true(), b, c, x, y) -> fibiter(b, s(c), y, plus(x, y))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

MPO

Execution Time (secs)
0.082
Answer
MAYBE
InputAProVE 07 thiemann25
MAYBE

We consider the following Problem:

  Strict Trs:
    {  plus(0(), y) -> y
     , plus(s(x), y) -> s(plus(x, y))
     , lt(0(), s(y)) -> true()
     , lt(x, 0()) -> false()
     , lt(s(x), s(y)) -> lt(x, y)
     , fib(x) -> fibiter(x, 0(), 0(), s(0()))
     , fibiter(b, c, x, y) -> if(lt(c, b), b, c, x, y)
     , if(false(), b, c, x, y) -> x
     , if(true(), b, c, x, y) -> fibiter(b, s(c), y, plus(x, y))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

POP*

Execution Time (secs)
0.075
Answer
MAYBE
InputAProVE 07 thiemann25
MAYBE

We consider the following Problem:

  Strict Trs:
    {  plus(0(), y) -> y
     , plus(s(x), y) -> s(plus(x, y))
     , lt(0(), s(y)) -> true()
     , lt(x, 0()) -> false()
     , lt(s(x), s(y)) -> lt(x, y)
     , fib(x) -> fibiter(x, 0(), 0(), s(0()))
     , fibiter(b, c, x, y) -> if(lt(c, b), b, c, x, y)
     , if(false(), b, c, x, y) -> x
     , if(true(), b, c, x, y) -> fibiter(b, s(c), y, plus(x, y))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

POP* (PS)

Execution Time (secs)
0.081
Answer
MAYBE
InputAProVE 07 thiemann25
MAYBE

We consider the following Problem:

  Strict Trs:
    {  plus(0(), y) -> y
     , plus(s(x), y) -> s(plus(x, y))
     , lt(0(), s(y)) -> true()
     , lt(x, 0()) -> false()
     , lt(s(x), s(y)) -> lt(x, y)
     , fib(x) -> fibiter(x, 0(), 0(), s(0()))
     , fibiter(b, c, x, y) -> if(lt(c, b), b, c, x, y)
     , if(false(), b, c, x, y) -> x
     , if(true(), b, c, x, y) -> fibiter(b, s(c), y, plus(x, y))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

Small POP*

Execution Time (secs)
0.064
Answer
MAYBE
InputAProVE 07 thiemann25
MAYBE

We consider the following Problem:

  Strict Trs:
    {  plus(0(), y) -> y
     , plus(s(x), y) -> s(plus(x, y))
     , lt(0(), s(y)) -> true()
     , lt(x, 0()) -> false()
     , lt(s(x), s(y)) -> lt(x, y)
     , fib(x) -> fibiter(x, 0(), 0(), s(0()))
     , fibiter(b, c, x, y) -> if(lt(c, b), b, c, x, y)
     , if(false(), b, c, x, y) -> x
     , if(true(), b, c, x, y) -> fibiter(b, s(c), y, plus(x, y))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

Small POP* (PS)

Execution Time (secs)
0.092
Answer
MAYBE
InputAProVE 07 thiemann25
MAYBE

We consider the following Problem:

  Strict Trs:
    {  plus(0(), y) -> y
     , plus(s(x), y) -> s(plus(x, y))
     , lt(0(), s(y)) -> true()
     , lt(x, 0()) -> false()
     , lt(s(x), s(y)) -> lt(x, y)
     , fib(x) -> fibiter(x, 0(), 0(), s(0()))
     , fibiter(b, c, x, y) -> if(lt(c, b), b, c, x, y)
     , if(false(), b, c, x, y) -> x
     , if(true(), b, c, x, y) -> fibiter(b, s(c), y, plus(x, y))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..