TIME: 780 SCC: 13 (loops closed under composition) ================================= 11_loop(A,B) :- 11_loop(C,D) [1*D=<2,1*D>=2,1*C>=1,1*B>=1,A>=D,A>C,A>B,1*A>=2] RF: 1*A+ -1 11_loop(A,B) :- 11_loop(C,D) [1*D>=0,B>D,B>=C,1*B>=1,C=A,B>=A] RF: 1*B 11_loop(A,B) :- 11_loop(C,D) [1*D>=0,C>D,1*C>=2,B>D,C>B,1*B>=1,A>D,C=A,A>B,1*A>=2] RF: 1*B 11_loop(A,B) :- 11_loop(C,D) [1*B>=1,1*D>=0,1*C>=1,1*A>=2,-1*D> -2,1*A+ -1*B>0,-1*C>= -2,1*A+ -1*C>0] RF: 1*A+ -1 11_loop(A,B) :- 11_loop(C,D) [1*B>=1,1*D>=0,1*A+ -1*B>0,-1*D> -2,1*A+ -1*C>0,1*C>2] RF: 1*A+ -3 11_loop(A,B) :- 11_loop(C,D) [1*A>=2,1*A+ -1*C>0,1*C>=1,-1*A+1*B>=0,1*D=2] RF: 1*A+ -1 11_loop(A,B) :- 11_loop(C,D) [1*A>=2,1*D>=0,1*C>=1,-1*C>= -2,1*A+ -1*C>0,-1*D> -2,-1*A+1*B>=0] RF: 1*B+ -1 11_loop(A,B) :- 11_loop(C,D) [-1*D> -2,1*D>=0,1*A+ -1*C>0,1*C>2,-1*A+1*B>=0] RF: 1/3*B+ -1/3 =================================