Problem Secret 06 TRS reverse

Tool CaT

Execution Time	Unknown
Answer	MAYBE
Input	Secret 06 TRS reverse

stdout:

MAYBE

Problem:
isEmpty(nil()) -> true()
isEmpty(cons(x,xs)) -> false()
last(cons(x,nil())) -> x
last(cons(x,cons(y,ys))) -> last(cons(y,ys))
dropLast(nil()) -> nil()
dropLast(cons(x,nil())) -> nil()
dropLast(cons(x,cons(y,ys))) -> cons(x,dropLast(cons(y,ys)))
append(nil(),ys) -> ys
append(cons(x,xs),ys) -> cons(x,append(xs,ys))
reverse(xs) -> rev(xs,nil())
rev(xs,ys) -> if(isEmpty(xs),dropLast(xs),append(ys,last(xs)),ys)
if(true(),xs,ys,zs) -> zs
if(false(),xs,ys,zs) -> rev(xs,ys)

Proof:
Open

Tool IRC1

Execution Time	Unknown
Answer	MAYBE
Input	Secret 06 TRS reverse

stdout:

MAYBE

Tool IRC2

Execution Time	Unknown
Answer	TIMEOUT
Input	Secret 06 TRS reverse

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    innermost runtime-complexity with respect to
  Rules:
    {  isEmpty(nil()) -> true()
     , isEmpty(cons(x, xs)) -> false()
     , last(cons(x, nil())) -> x
     , last(cons(x, cons(y, ys))) -> last(cons(y, ys))
     , dropLast(nil()) -> nil()
     , dropLast(cons(x, nil())) -> nil()
     , dropLast(cons(x, cons(y, ys))) -> cons(x, dropLast(cons(y, ys)))
     , append(nil(), ys) -> ys
     , append(cons(x, xs), ys) -> cons(x, append(xs, ys))
     , reverse(xs) -> rev(xs, nil())
     , rev(xs, ys) ->
       if(isEmpty(xs), dropLast(xs), append(ys, last(xs)), ys)
     , if(true(), xs, ys, zs) -> zs
     , if(false(), xs, ys, zs) -> rev(xs, ys)}

Proof Output:
  Computation stopped due to timeout after 60.0 seconds

Tool RC1

Execution Time	Unknown
Answer	MAYBE
Input	Secret 06 TRS reverse

stdout:

MAYBE

Tool RC2

Execution Time	Unknown
Answer	TIMEOUT
Input	Secret 06 TRS reverse

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    runtime-complexity with respect to
  Rules:
    {  isEmpty(nil()) -> true()
     , isEmpty(cons(x, xs)) -> false()
     , last(cons(x, nil())) -> x
     , last(cons(x, cons(y, ys))) -> last(cons(y, ys))
     , dropLast(nil()) -> nil()
     , dropLast(cons(x, nil())) -> nil()
     , dropLast(cons(x, cons(y, ys))) -> cons(x, dropLast(cons(y, ys)))
     , append(nil(), ys) -> ys
     , append(cons(x, xs), ys) -> cons(x, append(xs, ys))
     , reverse(xs) -> rev(xs, nil())
     , rev(xs, ys) ->
       if(isEmpty(xs), dropLast(xs), append(ys, last(xs)), ys)
     , if(true(), xs, ys, zs) -> zs
     , if(false(), xs, ys, zs) -> rev(xs, ys)}

Proof Output:
  Computation stopped due to timeout after 60.0 seconds