TIME: 2359


SCC: 14
=================================
Global Ranking Function: nat(1*C+ -1*D)

  28_loop(A,B,C,D) :- 28_loop(E,F,G,H) [1*D+ -1*H= -1,1*A+ -1*E=0,1*B+ -1*F=0,1*C+ -1*G=0,1*H>=1,1*E+ -1*H>= -1,1*B+ -1*H>=0,1*C+ -1*H>=0]
=================================

SCC: 18
=================================
Global Ranking Function: nat(1*C+ -1*E)

  31_loop(A,B,C,D,E) :- 31_loop(F,G,H,I,J) [1*E+ -1*J= -1,1*A+ -1*F=0,1*B+ -1*G=0,1*C+ -1*H=0,1*D+ -1*I=0,1*J>=1,1*F+ -1*J>= -1,1*F+1*G+ -1*J>= -2,1*H+ -1*J>=0,-1*F+ -1*G+1*I+1*J>=3]
=================================

SCC: 22
=================================
Global Ranking Function: nat(1*C+ -1*D+1*E)

  36_loop(A,B,C,D,E,F) :- 36_loop(G,H,I,J,K,L) [1*F+ -1*L= -1,1*A+ -1*G=0,1*B+ -1*H=0,1*C+ -1*I=0,1*D+ -1*J=0,1*E+ -1*K=1,1*L>=1,1*G+ -1*L>= -1,1*B+ -1*L>=0,1*J>=0,1*K>= -1,1*C+ -1*J>=1,1*C+ -1*K>=2]
  36_loop(A,B,C,D,E,F) :- 36_loop(G,H,I,J,K,L) [1*F+ -1*L= -1,1*A+ -1*G=0,1*B+ -1*H=0,1*C+ -1*I=0,1*D+ -1*J= -1,1*E+ -1*K=0,1*L>=1,1*G+ -1*L>= -1,1*B+ -1*L>=0,1*J>=1,1*K>=0,1*C+ -1*J>=0,1*C+ -1*K>=1]
=================================

SCC: 44
=================================
Global Ranking Function: log(2,nat(-1/2*A+1/2*B+ -1/2)+1)

  MergeSort_sort(II[I)V(A,B,C) :- MergeSort_sort(II[I)V(D,E,F) [-1*A+ -1*B+2*E>= -1,1*B+ -1*E>=2,1*A+1*B+ -2*E>=0,1*F>=0,1*C+ -1*F=0,1*A+ -1*D=0]
  MergeSort_sort(II[I)V(A,B,C) :- MergeSort_sort(II[I)V(D,E,F) [-1*A+2*D+ -1*E>=1,1*A+ -2*D+1*E>= -2,-1*D+1*E>=1,1*C>=0,1*C+ -1*F=0,1*B+ -1*E=0]
=================================

SCC: 50
=================================
Global Ranking Function: nat(1*C+ -1*D)

  5_loop(A,B,C,D) :- 5_loop(E,F,G,H) [1*C+ -1*H>=0,1*B+ -1*H>=0,1*A+ -1*H>=0,1*H>=1,1*D+ -1*H= -1,1*C+ -1*G=0,1*B+ -1*F=0,1*A+ -1*E=0]
=================================