Problem AProVE 07 thiemann07

Tool CaT

Execution Time	Unknown
Answer	MAYBE
Input	AProVE 07 thiemann07

stdout:

MAYBE

Problem:
car(cons(x,l)) -> x
cddr(nil()) -> nil()
cddr(cons(x,nil())) -> nil()
cddr(cons(x,cons(y,l))) -> l
cadr(cons(x,cons(y,l))) -> y
isZero(0()) -> true()
isZero(s(x)) -> false()
plus(x,y) -> ifplus(isZero(x),x,y)
ifplus(true(),x,y) -> y
ifplus(false(),x,y) -> s(plus(p(x),y))
times(x,y) -> iftimes(isZero(x),x,y)
iftimes(true(),x,y) -> 0()
iftimes(false(),x,y) -> plus(y,times(p(x),y))
p(s(x)) -> x
p(0()) -> 0()
shorter(nil(),y) -> true()
shorter(cons(x,l),0()) -> false()
shorter(cons(x,l),s(y)) -> shorter(l,y)
prod(l) -> if(shorter(l,0()),shorter(l,s(0())),l)
if(true(),b,l) -> s(0())
if(false(),b,l) -> if2(b,l)
if2(true(),l) -> car(l)
if2(false(),l) -> prod(cons(times(car(l),cadr(l)),cddr(l)))

Proof:
Open

Tool IRC1

Execution Time	Unknown
Answer	MAYBE
Input	AProVE 07 thiemann07

stdout:

MAYBE

Tool IRC2

Execution Time	Unknown
Answer	TIMEOUT
Input	AProVE 07 thiemann07

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    innermost runtime-complexity with respect to
  Rules:
    {  car(cons(x, l)) -> x
     , cddr(nil()) -> nil()
     , cddr(cons(x, nil())) -> nil()
     , cddr(cons(x, cons(y, l))) -> l
     , cadr(cons(x, cons(y, l))) -> y
     , isZero(0()) -> true()
     , isZero(s(x)) -> false()
     , plus(x, y) -> ifplus(isZero(x), x, y)
     , ifplus(true(), x, y) -> y
     , ifplus(false(), x, y) -> s(plus(p(x), y))
     , times(x, y) -> iftimes(isZero(x), x, y)
     , iftimes(true(), x, y) -> 0()
     , iftimes(false(), x, y) -> plus(y, times(p(x), y))
     , p(s(x)) -> x
     , p(0()) -> 0()
     , shorter(nil(), y) -> true()
     , shorter(cons(x, l), 0()) -> false()
     , shorter(cons(x, l), s(y)) -> shorter(l, y)
     , prod(l) -> if(shorter(l, 0()), shorter(l, s(0())), l)
     , if(true(), b, l) -> s(0())
     , if(false(), b, l) -> if2(b, l)
     , if2(true(), l) -> car(l)
     , if2(false(), l) -> prod(cons(times(car(l), cadr(l)), cddr(l)))}

Proof Output:
  Computation stopped due to timeout after 60.0 seconds

Tool RC1

Execution Time	Unknown
Answer	MAYBE
Input	AProVE 07 thiemann07

stdout:

MAYBE

Tool RC2

Execution Time	Unknown
Answer	TIMEOUT
Input	AProVE 07 thiemann07

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    runtime-complexity with respect to
  Rules:
    {  car(cons(x, l)) -> x
     , cddr(nil()) -> nil()
     , cddr(cons(x, nil())) -> nil()
     , cddr(cons(x, cons(y, l))) -> l
     , cadr(cons(x, cons(y, l))) -> y
     , isZero(0()) -> true()
     , isZero(s(x)) -> false()
     , plus(x, y) -> ifplus(isZero(x), x, y)
     , ifplus(true(), x, y) -> y
     , ifplus(false(), x, y) -> s(plus(p(x), y))
     , times(x, y) -> iftimes(isZero(x), x, y)
     , iftimes(true(), x, y) -> 0()
     , iftimes(false(), x, y) -> plus(y, times(p(x), y))
     , p(s(x)) -> x
     , p(0()) -> 0()
     , shorter(nil(), y) -> true()
     , shorter(cons(x, l), 0()) -> false()
     , shorter(cons(x, l), s(y)) -> shorter(l, y)
     , prod(l) -> if(shorter(l, 0()), shorter(l, s(0())), l)
     , if(true(), b, l) -> s(0())
     , if(false(), b, l) -> if2(b, l)
     , if2(true(), l) -> car(l)
     , if2(false(), l) -> prod(cons(times(car(l), cadr(l)), cddr(l)))}

Proof Output:
  Computation stopped due to timeout after 60.0 seconds