MAYBE
Time: 0.008458
TRS:
 {                 isEmpty empty() -> true(),
                isEmpty node(l, r) -> false(),
                      left empty() -> empty(),
                   left node(l, r) -> l,
                     right empty() -> empty(),
                  right node(l, r) -> r,
                           inc s x -> s inc x,
                           inc 0() -> s 0(),
         if(true(), b, n, m, x, y) -> x,
   if(false(), true(), n, m, x, y) -> count(n, y),
  if(false(), false(), n, m, x, y) -> count(m, x),
                       count(n, x) -> if(isEmpty n, isEmpty left n, right n, node(left left n, node(right left n, right n)), x, inc x),
                       nrOfNodes n -> count(n, 0())}
 DP:
  DP:
   {                         inc# s x -> inc# x,
     if#(false(), true(), n, m, x, y) -> count#(n, y),
    if#(false(), false(), n, m, x, y) -> count#(m, x),
                         count#(n, x) -> isEmpty# n,
                         count#(n, x) -> isEmpty# left n,
                         count#(n, x) -> left# n,
                         count#(n, x) -> left# left n,
                         count#(n, x) -> right# n,
                         count#(n, x) -> right# left n,
                         count#(n, x) -> inc# x,
                         count#(n, x) -> if#(isEmpty n, isEmpty left n, right n, node(left left n, node(right left n, right n)), x, inc x),
                         nrOfNodes# n -> count#(n, 0())}
  TRS:
  {                 isEmpty empty() -> true(),
                 isEmpty node(l, r) -> false(),
                       left empty() -> empty(),
                    left node(l, r) -> l,
                      right empty() -> empty(),
                   right node(l, r) -> r,
                            inc s x -> s inc x,
                            inc 0() -> s 0(),
          if(true(), b, n, m, x, y) -> x,
    if(false(), true(), n, m, x, y) -> count(n, y),
   if(false(), false(), n, m, x, y) -> count(m, x),
                        count(n, x) -> if(isEmpty n, isEmpty left n, right n, node(left left n, node(right left n, right n)), x, inc x),
                        nrOfNodes n -> count(n, 0())}
  EDG:
   {(count#(n, x) -> inc# x, inc# s x -> inc# x)
    (if#(false(), true(), n, m, x, y) -> count#(n, y), count#(n, x) -> if#(isEmpty n, isEmpty left n, right n, node(left left n, node(right left n, right n)), x, inc x))
    (if#(false(), true(), n, m, x, y) -> count#(n, y), count#(n, x) -> inc# x)
    (if#(false(), true(), n, m, x, y) -> count#(n, y), count#(n, x) -> right# left n)
    (if#(false(), true(), n, m, x, y) -> count#(n, y), count#(n, x) -> right# n)
    (if#(false(), true(), n, m, x, y) -> count#(n, y), count#(n, x) -> left# left n)
    (if#(false(), true(), n, m, x, y) -> count#(n, y), count#(n, x) -> left# n)
    (if#(false(), true(), n, m, x, y) -> count#(n, y), count#(n, x) -> isEmpty# left n)
    (if#(false(), true(), n, m, x, y) -> count#(n, y), count#(n, x) -> isEmpty# n)
    (count#(n, x) -> if#(isEmpty n, isEmpty left n, right n, node(left left n, node(right left n, right n)), x, inc x), if#(false(), false(), n, m, x, y) -> count#(m, x))
    (count#(n, x) -> if#(isEmpty n, isEmpty left n, right n, node(left left n, node(right left n, right n)), x, inc x), if#(false(), true(), n, m, x, y) -> count#(n, y))
    (if#(false(), false(), n, m, x, y) -> count#(m, x), count#(n, x) -> isEmpty# n)
    (if#(false(), false(), n, m, x, y) -> count#(m, x), count#(n, x) -> isEmpty# left n)
    (if#(false(), false(), n, m, x, y) -> count#(m, x), count#(n, x) -> left# n)
    (if#(false(), false(), n, m, x, y) -> count#(m, x), count#(n, x) -> left# left n)
    (if#(false(), false(), n, m, x, y) -> count#(m, x), count#(n, x) -> right# n)
    (if#(false(), false(), n, m, x, y) -> count#(m, x), count#(n, x) -> right# left n)
    (if#(false(), false(), n, m, x, y) -> count#(m, x), count#(n, x) -> inc# x)
    (if#(false(), false(), n, m, x, y) -> count#(m, x), count#(n, x) -> if#(isEmpty n, isEmpty left n, right n, node(left left n, node(right left n, right n)), x, inc x))
    (nrOfNodes# n -> count#(n, 0()), count#(n, x) -> isEmpty# n)
    (nrOfNodes# n -> count#(n, 0()), count#(n, x) -> isEmpty# left n)
    (nrOfNodes# n -> count#(n, 0()), count#(n, x) -> left# n)
    (nrOfNodes# n -> count#(n, 0()), count#(n, x) -> left# left n)
    (nrOfNodes# n -> count#(n, 0()), count#(n, x) -> right# n)
    (nrOfNodes# n -> count#(n, 0()), count#(n, x) -> right# left n)
    (nrOfNodes# n -> count#(n, 0()), count#(n, x) -> inc# x)
    (nrOfNodes# n -> count#(n, 0()), count#(n, x) -> if#(isEmpty n, isEmpty left n, right n, node(left left n, node(right left n, right n)), x, inc x))
    (inc# s x -> inc# x, inc# s x -> inc# x)}
   STATUS:
    arrows: 0.805556
    SCCS (2):
     Scc:
      { if#(false(), true(), n, m, x, y) -> count#(n, y),
       if#(false(), false(), n, m, x, y) -> count#(m, x),
                            count#(n, x) -> if#(isEmpty n, isEmpty left n, right n, node(left left n, node(right left n, right n)), x, inc x)}
     Scc:
      {inc# s x -> inc# x}
     
     
     SCC (3):
      Strict:
       { if#(false(), true(), n, m, x, y) -> count#(n, y),
        if#(false(), false(), n, m, x, y) -> count#(m, x),
                             count#(n, x) -> if#(isEmpty n, isEmpty left n, right n, node(left left n, node(right left n, right n)), x, inc x)}
      Weak:
      {                 isEmpty empty() -> true(),
                     isEmpty node(l, r) -> false(),
                           left empty() -> empty(),
                        left node(l, r) -> l,
                          right empty() -> empty(),
                       right node(l, r) -> r,
                                inc s x -> s inc x,
                                inc 0() -> s 0(),
              if(true(), b, n, m, x, y) -> x,
        if(false(), true(), n, m, x, y) -> count(n, y),
       if(false(), false(), n, m, x, y) -> count(m, x),
                            count(n, x) -> if(isEmpty n, isEmpty left n, right n, node(left left n, node(right left n, right n)), x, inc x),
                            nrOfNodes n -> count(n, 0())}
      Open
     
     
     
     
     
     
     
     SCC (1):
      Strict:
       {inc# s x -> inc# x}
      Weak:
      {                 isEmpty empty() -> true(),
                     isEmpty node(l, r) -> false(),
                           left empty() -> empty(),
                        left node(l, r) -> l,
                          right empty() -> empty(),
                       right node(l, r) -> r,
                                inc s x -> s inc x,
                                inc 0() -> s 0(),
              if(true(), b, n, m, x, y) -> x,
        if(false(), true(), n, m, x, y) -> count(n, y),
       if(false(), false(), n, m, x, y) -> count(m, x),
                            count(n, x) -> if(isEmpty n, isEmpty left n, right n, node(left left n, node(right left n, right n)), x, inc x),
                            nrOfNodes n -> count(n, 0())}
      Open