Problem Secret 06 TRS addList

Tool CaT

Execution Time	Unknown
Answer	MAYBE
Input	Secret 06 TRS addList

stdout:

MAYBE

Problem:
isEmpty(cons(x,xs)) -> false()
isEmpty(nil()) -> true()
isZero(0()) -> true()
isZero(s(x)) -> false()
head(cons(x,xs)) -> x
tail(cons(x,xs)) -> xs
tail(nil()) -> nil()
append(nil(),x) -> cons(x,nil())
append(cons(y,ys),x) -> cons(y,append(ys,x))
p(s(s(x))) -> s(p(s(x)))
p(s(0())) -> 0()
p(0()) -> 0()
inc(s(x)) -> s(inc(x))
inc(0()) -> s(0())
addLists(xs,ys,zs) ->
if(isEmpty(xs),isEmpty(ys),isZero(head(xs)),tail(xs),tail(ys),cons(p(head(xs)),tail(xs)),
cons(inc(head(ys)),tail(ys)),zs,append(zs,head(ys)))
if(true(),true(),b,xs,ys,xs2,ys2,zs,zs2) -> zs
if(true(),false(),b,xs,ys,xs2,ys2,zs,zs2) -> differentLengthError()
if(false(),true(),b,xs,ys,xs2,ys2,zs,zs2) -> differentLengthError()
if(false(),false(),false(),xs,ys,xs2,ys2,zs,zs2) -> addLists(xs2,ys2,zs)
if(false(),false(),true(),xs,ys,xs2,ys2,zs,zs2) -> addLists(xs,ys,zs2)
addList(xs,ys) -> addLists(xs,ys,nil())

Proof:
Open

Tool IRC1

Execution Time	Unknown
Answer	MAYBE
Input	Secret 06 TRS addList

stdout:

MAYBE

Tool IRC2

Execution Time	Unknown
Answer	TIMEOUT
Input	Secret 06 TRS addList

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    innermost runtime-complexity with respect to
  Rules:
    {  isEmpty(cons(x, xs)) -> false()
     , isEmpty(nil()) -> true()
     , isZero(0()) -> true()
     , isZero(s(x)) -> false()
     , head(cons(x, xs)) -> x
     , tail(cons(x, xs)) -> xs
     , tail(nil()) -> nil()
     , append(nil(), x) -> cons(x, nil())
     , append(cons(y, ys), x) -> cons(y, append(ys, x))
     , p(s(s(x))) -> s(p(s(x)))
     , p(s(0())) -> 0()
     , p(0()) -> 0()
     , inc(s(x)) -> s(inc(x))
     , inc(0()) -> s(0())
     , addLists(xs, ys, zs) ->
       if(isEmpty(xs),
          isEmpty(ys),
          isZero(head(xs)),
          tail(xs),
          tail(ys),
          cons(p(head(xs)), tail(xs)),
          cons(inc(head(ys)), tail(ys)),
          zs,
          append(zs, head(ys)))
     , if(true(), true(), b, xs, ys, xs2, ys2, zs, zs2) -> zs
     , if(true(), false(), b, xs, ys, xs2, ys2, zs, zs2) ->
       differentLengthError()
     , if(false(), true(), b, xs, ys, xs2, ys2, zs, zs2) ->
       differentLengthError()
     , if(false(), false(), false(), xs, ys, xs2, ys2, zs, zs2) ->
       addLists(xs2, ys2, zs)
     , if(false(), false(), true(), xs, ys, xs2, ys2, zs, zs2) ->
       addLists(xs, ys, zs2)
     , addList(xs, ys) -> addLists(xs, ys, nil())}

Proof Output:
  Computation stopped due to timeout after 60.0 seconds

Tool RC1

Execution Time	Unknown
Answer	MAYBE
Input	Secret 06 TRS addList

stdout:

MAYBE

Tool RC2

Execution Time	Unknown
Answer	TIMEOUT
Input	Secret 06 TRS addList

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    runtime-complexity with respect to
  Rules:
    {  isEmpty(cons(x, xs)) -> false()
     , isEmpty(nil()) -> true()
     , isZero(0()) -> true()
     , isZero(s(x)) -> false()
     , head(cons(x, xs)) -> x
     , tail(cons(x, xs)) -> xs
     , tail(nil()) -> nil()
     , append(nil(), x) -> cons(x, nil())
     , append(cons(y, ys), x) -> cons(y, append(ys, x))
     , p(s(s(x))) -> s(p(s(x)))
     , p(s(0())) -> 0()
     , p(0()) -> 0()
     , inc(s(x)) -> s(inc(x))
     , inc(0()) -> s(0())
     , addLists(xs, ys, zs) ->
       if(isEmpty(xs),
          isEmpty(ys),
          isZero(head(xs)),
          tail(xs),
          tail(ys),
          cons(p(head(xs)), tail(xs)),
          cons(inc(head(ys)), tail(ys)),
          zs,
          append(zs, head(ys)))
     , if(true(), true(), b, xs, ys, xs2, ys2, zs, zs2) -> zs
     , if(true(), false(), b, xs, ys, xs2, ys2, zs, zs2) ->
       differentLengthError()
     , if(false(), true(), b, xs, ys, xs2, ys2, zs, zs2) ->
       differentLengthError()
     , if(false(), false(), false(), xs, ys, xs2, ys2, zs, zs2) ->
       addLists(xs2, ys2, zs)
     , if(false(), false(), true(), xs, ys, xs2, ys2, zs, zs2) ->
       addLists(xs, ys, zs2)
     , addList(xs, ys) -> addLists(xs, ys, nil())}

Proof Output:
  Computation stopped due to timeout after 60.0 seconds