TIME: 13460 SCC: 45 ================================= Global Ranking Function: nat(1*A) 64_loop(A,B) :- 64_loop(C,D) [1*A+ -1*C>=1,1*C>=0,1*B+ -1*D= -1] ================================= SCC: 49 (loops closed under composition) ================================= 15(A,B,C,D) :- 15(E,F,G,H) [1*H>=0,1*G>=0,1*F>=0,H=D,1*D>=0,G=C,1*C>=0,B>F,1*B>=1,E=A] RF: 1*B 15(A,B,C,D) :- 15(E,F,G,H) [1*H>=0,D>H,1*D>=1,1*C>=0,1*B>=0,E=A] RF: 1*D 15(A,B,C,D) :- 15(E,F,G,H) [1*H>=0,1*G>=0,1*F>=0,H=D,1*D>=0,C>G,1*C>=1,F=B,1*B>=0,E=A] RF: 1*C 15(A,B,C,D) :- 15(E,F,G,H) [1*F>=0,1*G>=0,1*B>=1,1*B+ -1*F>0,1*C+ -1*G>0,1*D>=0,1*C>=1,1*A+ -1*E=0,1*D+ -1*H=0] RF: 1*C ================================= SCC: 63 ================================= Global Ranking Function: nat(1*A) 47_loop(A,B) :- 47_loop(C,D) [1*B>= -1,1*C>=0,1*A+ -1*C=1] =================================