TIME: 500 SCC: 10 ================================= Global Ranking Function: nat(1*A+1) 17_loop(A) :- 17_loop(B) [1*A+ -1*B=1,1*B>= -1] ================================= SCC: 11 ================================= Global Ranking Function: nat(1*D+ -1*E) 14_loop(A,B,C,D,E,F) :- 14_loop(G,H,I,J,K,L) [-1*L>=1,1*J+ -1*K>=0,1000*A+100*B+10*C+1*K+ -1*L>=1,1*D+ -1*J=0,1*E+ -1*K= -1,1*B+ -1*H=0,1*C+ -1*I=0,1*A+ -1*G=0] ================================= SCC: 12 ================================= Global Ranking Function: nat(1*C+1) 11_loop(A,B,C,D,E,F) :- 11_loop(G,H,I,J,K,L) [1*C>=0,-2*A+ -4*C+ -3*H+1*K>=0,1*K>=0,1*C+ -1*I=1,1*B+ -1*H=0,1*A+ -1*G=0,2*A+4*C+3*H+ -1*J=0] ================================= SCC: 14 ================================= Global Ranking Function: nat(1*B+ -1*C) 8_loop(A,B,C,D,E,F,G) :- 8_loop(H,I,J,K,L,M,N) [-1*K>=1,1*I+ -1*J>=0,1*A+1*J+ -1*K>=1,1*B+ -1*I=0,1*C+ -1*J= -1,1*A+ -1*H=0] ================================= SCC: 15 ================================= Global Ranking Function: nat(1*A+ -1*B) 2_loop(A,B,C,D,E,F,G,H) :- 2_loop(I,J,K,L,M,N,O,P) [1*A+ -1*B>=1,-2*B+1*L>=0,1*L>=0,1*A>=1,1*B+ -1*J= -1,1*A+ -1*I=0,2*B+ -1*K=0] =================================