TIME: 4820


SCC: 56
=================================
Global Ranking Function: nat(1/2*B+ -1/2)

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

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

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

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

  27_loop(A,B,C,D) :- 27_loop(E,F,G,H) [F>=H,1*E=<2,H>D,F>D,1*C>=1,B>=H,F=B,B>D,E=A,1*A=<2]
  RF: 1*B+ -1*D

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

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

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

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

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