MAYBE
Time: 0.004410
TRS:
 {                   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(cons(y(), ys), x) -> cons(y(), append(ys, x)),
                    append(nil(), x) -> cons(x, nil()),
         if(true(), b, n, m, xs, ys) -> xs,
   if(false(), true(), n, m, xs, ys) -> listify(n, ys),
  if(false(), false(), n, m, xs, ys) -> listify(m, xs),
                      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)),
                            toList n -> listify(n, nil())}
 DP:
  DP:
   {          append#(cons(y(), ys), x) -> append#(ys, x),
     if#(false(), true(), n, m, xs, ys) -> listify#(n, ys),
    if#(false(), false(), n, m, xs, ys) -> listify#(m, xs),
                        listify#(n, xs) -> isEmpty# n,
                        listify#(n, xs) -> isEmpty# left n,
                        listify#(n, xs) -> left# n,
                        listify#(n, xs) -> left# left n,
                        listify#(n, xs) -> right# n,
                        listify#(n, xs) -> right# left n,
                        listify#(n, xs) -> elem# n,
                        listify#(n, xs) -> elem# left n,
                        listify#(n, xs) -> append#(xs, n),
                        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)),
                              toList# n -> listify#(n, nil())}
  TRS:
  {                   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(cons(y(), ys), x) -> cons(y(), append(ys, x)),
                     append(nil(), x) -> cons(x, nil()),
          if(true(), b, n, m, xs, ys) -> xs,
    if(false(), true(), n, m, xs, ys) -> listify(n, ys),
   if(false(), false(), n, m, xs, ys) -> listify(m, xs),
                       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)),
                             toList n -> listify(n, nil())}
  UR:
   {         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(cons(y(), ys), x) -> cons(y(), append(ys, x)),
            append(nil(), x) -> cons(x, nil()),
                     a(y, z) -> y,
                     a(y, z) -> z}
   EDG:
    {(append#(cons(y(), ys), x) -> append#(ys, x), append#(cons(y(), ys), x) -> append#(ys, x))
     (listify#(n, xs) -> append#(xs, n), append#(cons(y(), ys), x) -> append#(ys, x))
     (if#(false(), false(), n, m, xs, ys) -> listify#(m, xs), 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#(false(), false(), n, m, xs, ys) -> listify#(m, xs), listify#(n, xs) -> append#(xs, n))
     (if#(false(), false(), n, m, xs, ys) -> listify#(m, xs), listify#(n, xs) -> elem# left n)
     (if#(false(), false(), n, m, xs, ys) -> listify#(m, xs), listify#(n, xs) -> elem# n)
     (if#(false(), false(), n, m, xs, ys) -> listify#(m, xs), listify#(n, xs) -> right# left n)
     (if#(false(), false(), n, m, xs, ys) -> listify#(m, xs), listify#(n, xs) -> right# n)
     (if#(false(), false(), n, m, xs, ys) -> listify#(m, xs), listify#(n, xs) -> left# left n)
     (if#(false(), false(), n, m, xs, ys) -> listify#(m, xs), listify#(n, xs) -> left# n)
     (if#(false(), false(), n, m, xs, ys) -> listify#(m, xs), listify#(n, xs) -> isEmpty# left n)
     (if#(false(), false(), n, m, xs, ys) -> listify#(m, xs), listify#(n, xs) -> isEmpty# n)
     (toList# n -> listify#(n, nil()), listify#(n, xs) -> isEmpty# n)
     (toList# n -> listify#(n, nil()), listify#(n, xs) -> isEmpty# left n)
     (toList# n -> listify#(n, nil()), listify#(n, xs) -> left# n)
     (toList# n -> listify#(n, nil()), listify#(n, xs) -> left# left n)
     (toList# n -> listify#(n, nil()), listify#(n, xs) -> right# n)
     (toList# n -> listify#(n, nil()), listify#(n, xs) -> right# left n)
     (toList# n -> listify#(n, nil()), listify#(n, xs) -> elem# n)
     (toList# n -> listify#(n, nil()), listify#(n, xs) -> elem# left n)
     (toList# n -> listify#(n, nil()), listify#(n, xs) -> append#(xs, n))
     (toList# n -> listify#(n, nil()), 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#(false(), true(), n, m, xs, ys) -> listify#(n, ys), listify#(n, xs) -> isEmpty# n)
     (if#(false(), true(), n, m, xs, ys) -> listify#(n, ys), listify#(n, xs) -> isEmpty# left n)
     (if#(false(), true(), n, m, xs, ys) -> listify#(n, ys), listify#(n, xs) -> left# n)
     (if#(false(), true(), n, m, xs, ys) -> listify#(n, ys), listify#(n, xs) -> left# left n)
     (if#(false(), true(), n, m, xs, ys) -> listify#(n, ys), listify#(n, xs) -> right# n)
     (if#(false(), true(), n, m, xs, ys) -> listify#(n, ys), listify#(n, xs) -> right# left n)
     (if#(false(), true(), n, m, xs, ys) -> listify#(n, ys), listify#(n, xs) -> elem# n)
     (if#(false(), true(), n, m, xs, ys) -> listify#(n, ys), listify#(n, xs) -> elem# left n)
     (if#(false(), true(), n, m, xs, ys) -> listify#(n, ys), listify#(n, xs) -> append#(xs, n))
     (if#(false(), true(), n, m, xs, ys) -> listify#(n, ys), 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)))
     (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#(false(), true(), n, m, xs, ys) -> listify#(n, ys))
     (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#(false(), false(), n, m, xs, ys) -> listify#(m, xs))}
    STATUS:
     arrows: 0.826531
     SCCS (2):
      Scc:
       { if#(false(), true(), n, m, xs, ys) -> listify#(n, ys),
        if#(false(), false(), n, m, xs, ys) -> listify#(m, xs),
                            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))}
      Scc:
       {append#(cons(y(), ys), x) -> append#(ys, x)}
      
      
      SCC (3):
       Strict:
        { if#(false(), true(), n, m, xs, ys) -> listify#(n, ys),
         if#(false(), false(), n, m, xs, ys) -> listify#(m, xs),
                             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))}
       Weak:
       {                   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(cons(y(), ys), x) -> cons(y(), append(ys, x)),
                          append(nil(), x) -> cons(x, nil()),
               if(true(), b, n, m, xs, ys) -> xs,
         if(false(), true(), n, m, xs, ys) -> listify(n, ys),
        if(false(), false(), n, m, xs, ys) -> listify(m, xs),
                            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)),
                                  toList n -> listify(n, nil())}
       Open
      
      SCC (1):
       Strict:
        {append#(cons(y(), ys), x) -> append#(ys, x)}
       Weak:
       {                   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(cons(y(), ys), x) -> cons(y(), append(ys, x)),
                          append(nil(), x) -> cons(x, nil()),
               if(true(), b, n, m, xs, ys) -> xs,
         if(false(), true(), n, m, xs, ys) -> listify(n, ys),
        if(false(), false(), n, m, xs, ys) -> listify(m, xs),
                            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)),
                                  toList n -> listify(n, nil())}
       Open