TIME: 260 SCC: 17 ================================= Global Ranking Function: nat(1*A+ -1*B+1) Recursions_rec4(II)V(A,B) :- Recursions_rec4(II)V(C,D) [1*A+ -1*D>=0,1*A+ -1*C=1,1*B+ -1*D=0] ================================= SCC: 18 ================================= Global Ranking Function: nat(-1*A+1*B+1) Recursions_rec3(IIIII)V(A,B,C,D,E) :- Recursions_rec3(IIIII)V(F,G,H,I,J) [-1*A+1*G>=0,1*D+ -1*I=0,1*C+ -1*H=0,1*B+ -1*G=0,1*E+ -1*J=0,1*A+ -1*F= -1] ================================= SCC: 19 ================================= Global Ranking Function: nat(1*A+ -1*B+1) Recursions_rec2(IIII)V(A,B,C,D) :- Recursions_rec2(IIII)V(E,F,G,H) [1*A+ -1*F>=0,1*C+ -1*G=0,1*B+ -1*F=0,1*A+ -1*E=1,1*D+ -1*H=0] ================================= SCC: 20 ================================= Global Ranking Function: nat(-1*A+1*B+1) Recursions_rec1(III)V(A,B,C) :- Recursions_rec1(III)V(D,E,F) [-1*A+1*E>=0,1*B+ -1*E=0,1*C+ -1*F=0,1*A+ -1*D= -1] ================================= SCC: 21 ================================= Global Ranking Function: nat(-1*A+1*B+1) Recursions_rec0(II)V(A,B) :- Recursions_rec0(II)V(C,D) [-1*A+1*D>=0,1*B+ -1*D=0,1*A+ -1*C= -1] ================================= SCC: 22 ================================= Global Ranking Function: nat(1*A+ -1*B) 2_loop(A,B) :- 2_loop(C,D) [-1*B+1*C>=1,1*C>=1,1*A+ -1*C=0,1*B+ -1*D= -1] =================================