Problem Secret 06 TRS toList

Tool CaT

Execution TimeUnknown
Answer
MAYBE
InputSecret 06 TRS toList

stdout:

MAYBE

Problem:
 isEmpty(empty()) -> true()
 isEmpty(node(l,x,r)) -> false()
 left(empty()) -> empty()
 left(node(l,x,r)) -> l
 right(empty()) -> empty()
 right(node(l,x,r)) -> r
 elem(node(l,x,r)) -> x
 append(nil(),x) -> cons(x,nil())
 append(cons(y(),ys),x) -> cons(y(),append(ys,x))
 listify(n,xs) ->
 if(isEmpty(n),isEmpty(left(n)),right(n),node(left(left(n)),elem(left(n)),
                                              node(right(left(n)),elem(n),right(n))),
    xs,append(xs,n))
 if(true(),b,n,m,xs,ys) -> xs
 if(false(),false(),n,m,xs,ys) -> listify(m,xs)
 if(false(),true(),n,m,xs,ys) -> listify(n,ys)
 toList(n) -> listify(n,nil())

Proof:
 Open

Tool IRC1

Execution TimeUnknown
Answer
MAYBE
InputSecret 06 TRS toList

stdout:

MAYBE

Tool IRC2

Execution TimeUnknown
Answer
TIMEOUT
InputSecret 06 TRS toList

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    innermost runtime-complexity with respect to
  Rules:
    {  isEmpty(empty()) -> true()
     , isEmpty(node(l, x, r)) -> false()
     , left(empty()) -> empty()
     , left(node(l, x, r)) -> l
     , right(empty()) -> empty()
     , right(node(l, x, r)) -> r
     , elem(node(l, x, r)) -> x
     , append(nil(), x) -> cons(x, nil())
     , append(cons(y(), ys), x) -> cons(y(), append(ys, x))
     , listify(n, xs) ->
       if(isEmpty(n),
          isEmpty(left(n)),
          right(n),
          node(left(left(n)),
               elem(left(n)),
               node(right(left(n)), elem(n), right(n))),
          xs,
          append(xs, n))
     , if(true(), b, n, m, xs, ys) -> xs
     , if(false(), false(), n, m, xs, ys) -> listify(m, xs)
     , if(false(), true(), n, m, xs, ys) -> listify(n, ys)
     , toList(n) -> listify(n, nil())}

Proof Output:    
  Computation stopped due to timeout after 60.0 seconds

Tool RC1

Execution TimeUnknown
Answer
MAYBE
InputSecret 06 TRS toList

stdout:

MAYBE

Tool RC2

Execution TimeUnknown
Answer
TIMEOUT
InputSecret 06 TRS toList

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    runtime-complexity with respect to
  Rules:
    {  isEmpty(empty()) -> true()
     , isEmpty(node(l, x, r)) -> false()
     , left(empty()) -> empty()
     , left(node(l, x, r)) -> l
     , right(empty()) -> empty()
     , right(node(l, x, r)) -> r
     , elem(node(l, x, r)) -> x
     , append(nil(), x) -> cons(x, nil())
     , append(cons(y(), ys), x) -> cons(y(), append(ys, x))
     , listify(n, xs) ->
       if(isEmpty(n),
          isEmpty(left(n)),
          right(n),
          node(left(left(n)),
               elem(left(n)),
               node(right(left(n)), elem(n), right(n))),
          xs,
          append(xs, n))
     , if(true(), b, n, m, xs, ys) -> xs
     , if(false(), false(), n, m, xs, ys) -> listify(m, xs)
     , if(false(), true(), n, m, xs, ys) -> listify(n, ys)
     , toList(n) -> listify(n, nil())}

Proof Output:    
  Computation stopped due to timeout after 60.0 seconds