TIME: 659


SCC: 15
=================================
Global Ranking Function: nat(1*A+ -1)

  BTree_height()I(A) :- BTree_height()I(B) [1*A+ -1*B>=1,1*B>=1]
=================================

SCC: 30
=================================
Global Ranking Function: nat(1*B+ -1)

  BTree_(I)V(A,B) :- BTree_(I)V(C,D) [1*B>=2,1*A>=1,1*C=1,1*B+ -1*D=1]
=================================