TIME: 5600


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

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

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

  68_loop(A,B) :- 68_loop(C,D) [1*A+ -1*C=1,1*C>= -1,1*D>=0,1*B>=2,1*B+ -1*D>=1]
=================================

SCC: 70
=================================
Global Ranking Function: nat(1/2*B)

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

SCC: 76
=================================
Global Ranking Function: nat(1*B)

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

SCC: 113 (loops closed under composition)
=================================
  35_loop(A,B,C) :- 35_loop(D,E,F) [1*F>=1,F>E,1*E=<0,1*E>=0,D>E,1*D>=1,C>E,1*C>=1,A>E,A>D,1*A>=2]
  RF: 1*A+ -1

  35_loop(A,B,C) :- 35_loop(D,E,F) [1*F>=0,1*D>=2,C>F,1*C>=1,D=A,1*A>=2]
  RF: 1*C

  35_loop(A,B,C) :- 35_loop(D,E,F) [1*F>=0,1*D=<1,C>F,C>=D,1*C>=1,D=A,C>=A,1*A=<1]
  RF: 1*C

  35_loop(A,B,C) :- 35_loop(D,E,F) [1*F>=0,1*C>=1,1*A+ -1*D>0,1*D>=2]
  RF: 1*A+ -2

  35_loop(A,B,C) :- 35_loop(D,E,F) [1*F>=0,1*C>=1,1*A>=2,1*D=1]
  RF: 1*A+ -1

=================================