Runtime Complexity TRS:
The TRS R consists of the following 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)

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

Runtime Complexity TRS:
The TRS R consists of the following 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')

Rewrite Strategy: INNERMOST

Infered types.

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')

Types:
isEmpty' :: empty':node':y' → true':false'
empty' :: empty':node':y'
true' :: true':false'
node' :: empty':node':y' → elem' → empty':node':y' → empty':node':y'
false' :: true':false'
left' :: empty':node':y' → empty':node':y'
right' :: empty':node':y' → empty':node':y'
elem' :: empty':node':y' → elem'
append' :: nil':cons' → empty':node':y' → nil':cons'
nil' :: nil':cons'
cons' :: empty':node':y' → nil':cons' → nil':cons'
y' :: empty':node':y'
listify' :: empty':node':y' → nil':cons' → nil':cons'
if' :: true':false' → true':false' → empty':node':y' → empty':node':y' → nil':cons' → nil':cons' → nil':cons'
toList' :: empty':node':y' → nil':cons'
_hole_true':false'1 :: true':false'
_hole_empty':node':y'2 :: empty':node':y'
_hole_elem'3 :: elem'
_hole_nil':cons'4 :: nil':cons'
_gen_empty':node':y'5 :: Nat → empty':node':y'
_gen_nil':cons'6 :: Nat → nil':cons'

Heuristically decided to analyse the following defined symbols:
append', listify'

They will be analysed ascendingly in the following order:
append' < listify'

Generator Equations:
_gen_empty':node':y'5(0) ⇔ empty'
_gen_empty':node':y'5(+(x, 1)) ⇔ node'(empty', _hole_elem'3, _gen_empty':node':y'5(x))
_gen_nil':cons'6(0) ⇔ nil'
_gen_nil':cons'6(+(x, 1)) ⇔ cons'(empty', _gen_nil':cons'6(x))

The following defined symbols remain to be analysed:
append', listify'

They will be analysed ascendingly in the following order:
append' < listify'

Could not prove a rewrite lemma for the defined symbol append'.

The following defined symbols remain to be analysed:
listify'

Could not prove a rewrite lemma for the defined symbol listify'.

The following conjecture could not be proven:

listify'(_gen_empty':node':y'5(_n24), _gen_nil':cons'6(0)) →^? _*7

No more defined symbols left to analyse.