NO * Step 1: TrivialSCCs NO + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G,H,I,J) -> f16(1,0,1,N,0,M,L,K,I,J) [K >= 0 && L >= K && L >= 0 && M >= L && N >= 0 && M >= 0] (1,1) 1. f16(A,B,C,D,E,F,G,H,I,J) -> f25(A,B,C,D,1 + E,F,G,H,0,J) [G + -1*H >= 0 (?,1) && F + -1*H >= 0 && H >= 0 && G + H >= 0 && F + H >= 0 && E + H >= 0 && D + H >= 0 && B + H >= 0 && -1 + A + H >= 0 && F + -1*G >= 0 && G >= 0 && F + G >= 0 && E + G >= 0 && -1*E + G >= 0 && D + G >= 0 && -1 + C + G >= 0 && B + G >= 0 && -1*B + G >= 0 && -1 + A + G >= 0 && F >= 0 && E + F >= 0 && -1*E + F >= 0 && D + F >= 0 && -1 + C + F >= 0 && 1 + -1*C + F >= 0 && B + F >= 0 && -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && B + E >= 0 && -1*B + E >= 0 && -1 + A + E >= 0 && D >= 0 && B + D >= 0 && -1 + A + D >= 0 && A + -1*C >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0 && H >= 1 && 0 >= E && 0 >= D] 2. f16(A,B,C,D,E,F,G,H,I,J) -> f25(A,B,C,D,E,F,G,H,N,J) [G + -1*H >= 0 (?,1) && F + -1*H >= 0 && H >= 0 && G + H >= 0 && F + H >= 0 && E + H >= 0 && D + H >= 0 && B + H >= 0 && -1 + A + H >= 0 && F + -1*G >= 0 && G >= 0 && F + G >= 0 && E + G >= 0 && -1*E + G >= 0 && D + G >= 0 && -1 + C + G >= 0 && B + G >= 0 && -1*B + G >= 0 && -1 + A + G >= 0 && F >= 0 && E + F >= 0 && -1*E + F >= 0 && D + F >= 0 && -1 + C + F >= 0 && 1 + -1*C + F >= 0 && B + F >= 0 && -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && B + E >= 0 && -1*B + E >= 0 && -1 + A + E >= 0 && D >= 0 && B + D >= 0 && -1 + A + D >= 0 && A + -1*C >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0 && H >= 1 && E >= 2 && 0 >= D && 1 >= N && N >= 0] 3. f16(A,B,C,D,E,F,G,H,I,J) -> f25(A,1 + B,C,D,E,F,G,H,1,J) [G + -1*H >= 0 (?,1) && F + -1*H >= 0 && H >= 0 && G + H >= 0 && F + H >= 0 && E + H >= 0 && D + H >= 0 && B + H >= 0 && -1 + A + H >= 0 && F + -1*G >= 0 && G >= 0 && F + G >= 0 && E + G >= 0 && -1*E + G >= 0 && D + G >= 0 && -1 + C + G >= 0 && B + G >= 0 && -1*B + G >= 0 && -1 + A + G >= 0 && F >= 0 && E + F >= 0 && -1*E + F >= 0 && D + F >= 0 && -1 + C + F >= 0 && 1 + -1*C + F >= 0 && B + F >= 0 && -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && B + E >= 0 && -1*B + E >= 0 && -1 + A + E >= 0 && D >= 0 && B + D >= 0 && -1 + A + D >= 0 && A + -1*C >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0 && H >= 1 && 0 >= D && 0 >= B && E = 1] 4. f16(A,B,C,D,E,F,G,H,I,J) -> f25(A,0,-1 + C,D,E,F,G,H,0,J) [G + -1*H >= 0 (?,1) && F + -1*H >= 0 && H >= 0 && G + H >= 0 && F + H >= 0 && E + H >= 0 && D + H >= 0 && B + H >= 0 && -1 + A + H >= 0 && F + -1*G >= 0 && G >= 0 && F + G >= 0 && E + G >= 0 && -1*E + G >= 0 && D + G >= 0 && -1 + C + G >= 0 && B + G >= 0 && -1*B + G >= 0 && -1 + A + G >= 0 && F >= 0 && E + F >= 0 && -1*E + F >= 0 && D + F >= 0 && -1 + C + F >= 0 && 1 + -1*C + F >= 0 && B + F >= 0 && -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && B + E >= 0 && -1*B + E >= 0 && -1 + A + E >= 0 && D >= 0 && B + D >= 0 && -1 + A + D >= 0 && A + -1*C >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0 && H >= 1 && 0 >= D && C >= 1 && E = 1 && B = 1] 5. f16(A,B,C,D,E,F,G,H,I,J) -> f25(1 + A,0,1 + A,N,0,F,G,H,M,J) [G + -1*H >= 0 (?,1) && F + -1*H >= 0 && H >= 0 && G + H >= 0 && F + H >= 0 && E + H >= 0 && D + H >= 0 && B + H >= 0 && -1 + A + H >= 0 && F + -1*G >= 0 && G >= 0 && F + G >= 0 && E + G >= 0 && -1*E + G >= 0 && D + G >= 0 && -1 + C + G >= 0 && B + G >= 0 && -1*B + G >= 0 && -1 + A + G >= 0 && F >= 0 && E + F >= 0 && -1*E + F >= 0 && D + F >= 0 && -1 + C + F >= 0 && 1 + -1*C + F >= 0 && B + F >= 0 && -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && B + E >= 0 && -1*B + E >= 0 && -1 + A + E >= 0 && D >= 0 && B + D >= 0 && -1 + A + D >= 0 && A + -1*C >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0 && H >= 1 && 0 >= D && 0 >= C && M >= 0 && 1 >= M && N >= 0 && E = 1 && B = 1] 6. f16(A,B,C,D,E,F,G,H,I,J) -> f25(A,B,C,-1 + D,E,F,G,H,N,J) [G + -1*H >= 0 (?,1) && F + -1*H >= 0 && H >= 0 && G + H >= 0 && F + H >= 0 && E + H >= 0 && D + H >= 0 && B + H >= 0 && -1 + A + H >= 0 && F + -1*G >= 0 && G >= 0 && F + G >= 0 && E + G >= 0 && -1*E + G >= 0 && D + G >= 0 && -1 + C + G >= 0 && B + G >= 0 && -1*B + G >= 0 && -1 + A + G >= 0 && F >= 0 && E + F >= 0 && -1*E + F >= 0 && D + F >= 0 && -1 + C + F >= 0 && 1 + -1*C + F >= 0 && B + F >= 0 && -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && B + E >= 0 && -1*B + E >= 0 && -1 + A + E >= 0 && D >= 0 && B + D >= 0 && -1 + A + D >= 0 && A + -1*C >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0 && H >= 1 && D >= 1 && 1 >= N && N >= 0] 7. f25(A,B,C,D,E,F,G,H,I,J) -> f50(A,B,C,D,1 + E,F,G,H,I,0) [1 + -1*I >= 0 (?,1) && H + -1*I >= 0 && G + -1*I >= 0 && F + -1*I >= 0 && 1 + E + -1*I >= 0 && 1 + D + -1*I >= 0 && 1 + B + -1*I >= 0 && A + -1*I >= 0 && I >= 0 && -1 + H + I >= 0 && -1 + G + I >= 0 && -1 + F + I >= 0 && E + I >= 0 && D + I >= 0 && B + I >= 0 && -1 + A + I >= 0 && G + -1*H >= 0 && F + -1*H >= 0 && -1 + H >= 0 && -2 + G + H >= 0 && -2 + F + H >= 0 && -1 + E + H >= 0 && -1 + D + H >= 0 && -1 + B + H >= 0 && -2 + A + H >= 0 && F + -1*G >= 0 && -1 + G >= 0 && -2 + F + G >= 0 && -1 + E + G >= 0 && -1*E + G >= 0 && -1 + D + G >= 0 && -1 + C + G >= 0 && -1 + B + G >= 0 && -1*B + G >= 0 && -2 + A + G >= 0 && -1 + F >= 0 && -1 + E + F >= 0 && -1*E + F >= 0 && -1 + D + F >= 0 && -1 + C + F >= 0 && 2 + -1*C + F >= 0 && -1 + B + F >= 0 && -1*B + F >= 0 && -2 + A + F >= 0 && 2 + -1*A + F >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && B + E >= 0 && -1*B + E >= 0 && -1 + A + E >= 0 && D >= 0 && B + D >= 0 && -1 + A + D >= 0 && A + -1*C >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0 && I >= 1 && 0 >= E && 0 >= D] 8. f25(A,B,C,D,E,F,G,H,I,J) -> f50(A,B,C,D,E,F,G,H,I,N) [1 + -1*I >= 0 (?,1) && H + -1*I >= 0 && G + -1*I >= 0 && F + -1*I >= 0 && 1 + E + -1*I >= 0 && 1 + D + -1*I >= 0 && 1 + B + -1*I >= 0 && A + -1*I >= 0 && I >= 0 && -1 + H + I >= 0 && -1 + G + I >= 0 && -1 + F + I >= 0 && E + I >= 0 && D + I >= 0 && B + I >= 0 && -1 + A + I >= 0 && G + -1*H >= 0 && F + -1*H >= 0 && -1 + H >= 0 && -2 + G + H >= 0 && -2 + F + H >= 0 && -1 + E + H >= 0 && -1 + D + H >= 0 && -1 + B + H >= 0 && -2 + A + H >= 0 && F + -1*G >= 0 && -1 + G >= 0 && -2 + F + G >= 0 && -1 + E + G >= 0 && -1*E + G >= 0 && -1 + D + G >= 0 && -1 + C + G >= 0 && -1 + B + G >= 0 && -1*B + G >= 0 && -2 + A + G >= 0 && -1 + F >= 0 && -1 + E + F >= 0 && -1*E + F >= 0 && -1 + D + F >= 0 && -1 + C + F >= 0 && 2 + -1*C + F >= 0 && -1 + B + F >= 0 && -1*B + F >= 0 && -2 + A + F >= 0 && 2 + -1*A + F >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && B + E >= 0 && -1*B + E >= 0 && -1 + A + E >= 0 && D >= 0 && B + D >= 0 && -1 + A + D >= 0 && A + -1*C >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0 && I >= 1 && E >= 2 && 0 >= D && 1 >= N && N >= 0] 9. f25(A,B,C,D,E,F,G,H,I,J) -> f50(A,1 + B,C,D,E,F,G,H,I,1) [1 + -1*I >= 0 (?,1) && H + -1*I >= 0 && G + -1*I >= 0 && F + -1*I >= 0 && 1 + E + -1*I >= 0 && 1 + D + -1*I >= 0 && 1 + B + -1*I >= 0 && A + -1*I >= 0 && I >= 0 && -1 + H + I >= 0 && -1 + G + I >= 0 && -1 + F + I >= 0 && E + I >= 0 && D + I >= 0 && B + I >= 0 && -1 + A + I >= 0 && G + -1*H >= 0 && F + -1*H >= 0 && -1 + H >= 0 && -2 + G + H >= 0 && -2 + F + H >= 0 && -1 + E + H >= 0 && -1 + D + H >= 0 && -1 + B + H >= 0 && -2 + A + H >= 0 && F + -1*G >= 0 && -1 + G >= 0 && -2 + F + G >= 0 && -1 + E + G >= 0 && -1*E + G >= 0 && -1 + D + G >= 0 && -1 + C + G >= 0 && -1 + B + G >= 0 && -1*B + G >= 0 && -2 + A + G >= 0 && -1 + F >= 0 && -1 + E + F >= 0 && -1*E + F >= 0 && -1 + D + F >= 0 && -1 + C + F >= 0 && 2 + -1*C + F >= 0 && -1 + B + F >= 0 && -1*B + F >= 0 && -2 + A + F >= 0 && 2 + -1*A + F >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && B + E >= 0 && -1*B + E >= 0 && -1 + A + E >= 0 && D >= 0 && B + D >= 0 && -1 + A + D >= 0 && A + -1*C >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0 && I >= 1 && 0 >= D && 0 >= B && E = 1] 10. f25(A,B,C,D,E,F,G,H,I,J) -> f50(A,0,-1 + C,D,E,F,G,H,I,0) [1 + -1*I >= 0 (?,1) && H + -1*I >= 0 && G + -1*I >= 0 && F + -1*I >= 0 && 1 + E + -1*I >= 0 && 1 + D + -1*I >= 0 && 1 + B + -1*I >= 0 && A + -1*I >= 0 && I >= 0 && -1 + H + I >= 0 && -1 + G + I >= 0 && -1 + F + I >= 0 && E + I >= 0 && D + I >= 0 && B + I >= 0 && -1 + A + I >= 0 && G + -1*H >= 0 && F + -1*H >= 0 && -1 + H >= 0 && -2 + G + H >= 0 && -2 + F + H >= 0 && -1 + E + H >= 0 && -1 + D + H >= 0 && -1 + B + H >= 0 && -2 + A + H >= 0 && F + -1*G >= 0 && -1 + G >= 0 && -2 + F + G >= 0 && -1 + E + G >= 0 && -1*E + G >= 0 && -1 + D + G >= 0 && -1 + C + G >= 0 && -1 + B + G >= 0 && -1*B + G >= 0 && -2 + A + G >= 0 && -1 + F >= 0 && -1 + E + F >= 0 && -1*E + F >= 0 && -1 + D + F >= 0 && -1 + C + F >= 0 && 2 + -1*C + F >= 0 && -1 + B + F >= 0 && -1*B + F >= 0 && -2 + A + F >= 0 && 2 + -1*A + F >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && B + E >= 0 && -1*B + E >= 0 && -1 + A + E >= 0 && D >= 0 && B + D >= 0 && -1 + A + D >= 0 && A + -1*C >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0 && I >= 1 && 0 >= D && C >= 1 && E = 1 && B = 1] 11. f25(A,B,C,D,E,F,G,H,I,J) -> f50(1 + A,0,1 + A,N,0,F,G,H,I,M) [1 + -1*I >= 0 (?,1) && H + -1*I >= 0 && G + -1*I >= 0 && F + -1*I >= 0 && 1 + E + -1*I >= 0 && 1 + D + -1*I >= 0 && 1 + B + -1*I >= 0 && A + -1*I >= 0 && I >= 0 && -1 + H + I >= 0 && -1 + G + I >= 0 && -1 + F + I >= 0 && E + I >= 0 && D + I >= 0 && B + I >= 0 && -1 + A + I >= 0 && G + -1*H >= 0 && F + -1*H >= 0 && -1 + H >= 0 && -2 + G + H >= 0 && -2 + F + H >= 0 && -1 + E + H >= 0 && -1 + D + H >= 0 && -1 + B + H >= 0 && -2 + A + H >= 0 && F + -1*G >= 0 && -1 + G >= 0 && -2 + F + G >= 0 && -1 + E + G >= 0 && -1*E + G >= 0 && -1 + D + G >= 0 && -1 + C + G >= 0 && -1 + B + G >= 0 && -1*B + G >= 0 && -2 + A + G >= 0 && -1 + F >= 0 && -1 + E + F >= 0 && -1*E + F >= 0 && -1 + D + F >= 0 && -1 + C + F >= 0 && 2 + -1*C + F >= 0 && -1 + B + F >= 0 && -1*B + F >= 0 && -2 + A + F >= 0 && 2 + -1*A + F >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && B + E >= 0 && -1*B + E >= 0 && -1 + A + E >= 0 && D >= 0 && B + D >= 0 && -1 + A + D >= 0 && A + -1*C >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0 && I >= 1 && 0 >= D && 0 >= C && M >= 0 && 1 >= M && N >= 0 && E = 1 && B = 1] 12. f25(A,B,C,D,E,F,G,H,I,J) -> f50(A,B,C,-1 + D,E,F,G,H,I,N) [1 + -1*I >= 0 (?,1) && H + -1*I >= 0 && G + -1*I >= 0 && F + -1*I >= 0 && 1 + E + -1*I >= 0 && 1 + D + -1*I >= 0 && 1 + B + -1*I >= 0 && A + -1*I >= 0 && I >= 0 && -1 + H + I >= 0 && -1 + G + I >= 0 && -1 + F + I >= 0 && E + I >= 0 && D + I >= 0 && B + I >= 0 && -1 + A + I >= 0 && G + -1*H >= 0 && F + -1*H >= 0 && -1 + H >= 0 && -2 + G + H >= 0 && -2 + F + H >= 0 && -1 + E + H >= 0 && -1 + D + H >= 0 && -1 + B + H >= 0 && -2 + A + H >= 0 && F + -1*G >= 0 && -1 + G >= 0 && -2 + F + G >= 0 && -1 + E + G >= 0 && -1*E + G >= 0 && -1 + D + G >= 0 && -1 + C + G >= 0 && -1 + B + G >= 0 && -1*B + G >= 0 && -2 + A + G >= 0 && -1 + F >= 0 && -1 + E + F >= 0 && -1*E + F >= 0 && -1 + D + F >= 0 && -1 + C + F >= 0 && 2 + -1*C + F >= 0 && -1 + B + F >= 0 && -1*B + F >= 0 && -2 + A + F >= 0 && 2 + -1*A + F >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && B + E >= 0 && -1*B + E >= 0 && -1 + A + E >= 0 && D >= 0 && B + D >= 0 && -1 + A + D >= 0 && A + -1*C >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0 && I >= 1 && D >= 1 && 1 >= N && N >= 0] 13. f25(A,B,C,D,E,F,G,H,I,J) -> f16(A,B,C,D,E,F,G,H,I,J) [1 + -1*I >= 0 (?,1) && H + -1*I >= 0 && G + -1*I >= 0 && F + -1*I >= 0 && 1 + E + -1*I >= 0 && 1 + D + -1*I >= 0 && 1 + B + -1*I >= 0 && A + -1*I >= 0 && I >= 0 && -1 + H + I >= 0 && -1 + G + I >= 0 && -1 + F + I >= 0 && E + I >= 0 && D + I >= 0 && B + I >= 0 && -1 + A + I >= 0 && G + -1*H >= 0 && F + -1*H >= 0 && -1 + H >= 0 && -2 + G + H >= 0 && -2 + F + H >= 0 && -1 + E + H >= 0 && -1 + D + H >= 0 && -1 + B + H >= 0 && -2 + A + H >= 0 && F + -1*G >= 0 && -1 + G >= 0 && -2 + F + G >= 0 && -1 + E + G >= 0 && -1*E + G >= 0 && -1 + D + G >= 0 && -1 + C + G >= 0 && -1 + B + G >= 0 && -1*B + G >= 0 && -2 + A + G >= 0 && -1 + F >= 0 && -1 + E + F >= 0 && -1*E + F >= 0 && -1 + D + F >= 0 && -1 + C + F >= 0 && 2 + -1*C + F >= 0 && -1 + B + F >= 0 && -1*B + F >= 0 && -2 + A + F >= 0 && 2 + -1*A + F >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && B + E >= 0 && -1*B + E >= 0 && -1 + A + E >= 0 && D >= 0 && B + D >= 0 && -1 + A + D >= 0 && A + -1*C >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0 && 1 + F >= A && 0 >= I] 14. f50(A,B,C,D,E,F,G,H,I,J) -> f16(A,B,C,D,E,F,G,H,I,J) [1 + -1*I >= 0 (?,1) && H + -1*I >= 0 && G + -1*I >= 0 && F + -1*I >= 0 && 1 + E + -1*I >= 0 && 1 + D + -1*I >= 0 && 1 + B + -1*I >= 0 && 1 + -1*I + J >= 0 && 2 + -1*I + -1*J >= 0 && A + -1*I >= 0 && -1 + I >= 0 && -2 + H + I >= 0 && -2 + G + I >= 0 && -2 + F + I >= 0 && -1 + E + I >= 0 && -1 + D + I >= 0 && -1 + B + I >= 0 && -1 + I + J >= 0 && I + -1*J >= 0 && -2 + A + I >= 0 && G + -1*H >= 0 && F + -1*H >= 0 && -1 + H >= 0 && -2 + G + H >= 0 && -2 + F + H >= 0 && -1 + E + H >= 0 && -1 + D + H >= 0 && -1 + B + H >= 0 && -1 + H + J >= 0 && H + -1*J >= 0 && -2 + A + H >= 0 && F + -1*G >= 0 && -1 + G >= 0 && -2 + F + G >= 0 && -1 + E + G >= 0 && -1*E + G >= 0 && -1 + D + G >= 0 && -1 + C + G >= 0 && -1 + B + G >= 0 && -1*B + G >= 0 && -1 + G + J >= 0 && G + -1*J >= 0 && -2 + A + G >= 0 && -1 + F >= 0 && -1 + E + F >= 0 && -1*E + F >= 0 && -1 + D + F >= 0 && -1 + C + F >= 0 && 3 + -1*C + F >= 0 && -1 + B + F >= 0 && -1*B + F >= 0 && -1 + F + J >= 0 && F + -1*J >= 0 && -2 + A + F >= 0 && 3 + -1*A + F >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && B + E >= 0 && -1*B + E >= 0 && E + J >= 0 && 1 + E + -1*J >= 0 && -1 + A + E >= 0 && D >= 0 && B + D >= 0 && D + J >= 0 && 1 + D + -1*J >= 0 && -1 + A + D >= 0 && A + -1*C >= 0 && B >= 0 && B + J >= 0 && 1 + B + -1*J >= 0 && -1 + A + B >= 0 && 1 + -1*J >= 0 && A + -1*J >= 0 && J >= 0 && -1 + A + J >= 0 && -1 + A >= 0 && J >= 1 && 1 + F >= A && H >= G] 15. f50(A,B,C,D,E,F,G,H,I,J) -> f16(A,B,C,D,E,F,G,1 + H,I,J) [1 + -1*I >= 0 (?,1) && H + -1*I >= 0 && G + -1*I >= 0 && F + -1*I >= 0 && 1 + E + -1*I >= 0 && 1 + D + -1*I >= 0 && 1 + B + -1*I >= 0 && 1 + -1*I + J >= 0 && 2 + -1*I + -1*J >= 0 && A + -1*I >= 0 && -1 + I >= 0 && -2 + H + I >= 0 && -2 + G + I >= 0 && -2 + F + I >= 0 && -1 + E + I >= 0 && -1 + D + I >= 0 && -1 + B + I >= 0 && -1 + I + J >= 0 && I + -1*J >= 0 && -2 + A + I >= 0 && G + -1*H >= 0 && F + -1*H >= 0 && -1 + H >= 0 && -2 + G + H >= 0 && -2 + F + H >= 0 && -1 + E + H >= 0 && -1 + D + H >= 0 && -1 + B + H >= 0 && -1 + H + J >= 0 && H + -1*J >= 0 && -2 + A + H >= 0 && F + -1*G >= 0 && -1 + G >= 0 && -2 + F + G >= 0 && -1 + E + G >= 0 && -1*E + G >= 0 && -1 + D + G >= 0 && -1 + C + G >= 0 && -1 + B + G >= 0 && -1*B + G >= 0 && -1 + G + J >= 0 && G + -1*J >= 0 && -2 + A + G >= 0 && -1 + F >= 0 && -1 + E + F >= 0 && -1*E + F >= 0 && -1 + D + F >= 0 && -1 + C + F >= 0 && 3 + -1*C + F >= 0 && -1 + B + F >= 0 && -1*B + F >= 0 && -1 + F + J >= 0 && F + -1*J >= 0 && -2 + A + F >= 0 && 3 + -1*A + F >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && B + E >= 0 && -1*B + E >= 0 && E + J >= 0 && 1 + E + -1*J >= 0 && -1 + A + E >= 0 && D >= 0 && B + D >= 0 && D + J >= 0 && 1 + D + -1*J >= 0 && -1 + A + D >= 0 && A + -1*C >= 0 && B >= 0 && B + J >= 0 && 1 + B + -1*J >= 0 && -1 + A + B >= 0 && 1 + -1*J >= 0 && A + -1*J >= 0 && J >= 0 && -1 + A + J >= 0 && -1 + A >= 0 && J >= 1 && 1 + F >= A && G >= 1 + H] 16. f50(A,B,C,D,E,F,G,H,I,J) -> f16(A,B,C,D,E,F,G,-1 + H,I,J) [1 + -1*I >= 0 (?,1) && H + -1*I >= 0 && G + -1*I >= 0 && F + -1*I >= 0 && 1 + E + -1*I >= 0 && 1 + D + -1*I >= 0 && 1 + B + -1*I >= 0 && 1 + -1*I + J >= 0 && 2 + -1*I + -1*J >= 0 && A + -1*I >= 0 && -1 + I >= 0 && -2 + H + I >= 0 && -2 + G + I >= 0 && -2 + F + I >= 0 && -1 + E + I >= 0 && -1 + D + I >= 0 && -1 + B + I >= 0 && -1 + I + J >= 0 && I + -1*J >= 0 && -2 + A + I >= 0 && G + -1*H >= 0 && F + -1*H >= 0 && -1 + H >= 0 && -2 + G + H >= 0 && -2 + F + H >= 0 && -1 + E + H >= 0 && -1 + D + H >= 0 && -1 + B + H >= 0 && -1 + H + J >= 0 && H + -1*J >= 0 && -2 + A + H >= 0 && F + -1*G >= 0 && -1 + G >= 0 && -2 + F + G >= 0 && -1 + E + G >= 0 && -1*E + G >= 0 && -1 + D + G >= 0 && -1 + C + G >= 0 && -1 + B + G >= 0 && -1*B + G >= 0 && -1 + G + J >= 0 && G + -1*J >= 0 && -2 + A + G >= 0 && -1 + F >= 0 && -1 + E + F >= 0 && -1*E + F >= 0 && -1 + D + F >= 0 && -1 + C + F >= 0 && 3 + -1*C + F >= 0 && -1 + B + F >= 0 && -1*B + F >= 0 && -1 + F + J >= 0 && F + -1*J >= 0 && -2 + A + F >= 0 && 3 + -1*A + F >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && B + E >= 0 && -1*B + E >= 0 && E + J >= 0 && 1 + E + -1*J >= 0 && -1 + A + E >= 0 && D >= 0 && B + D >= 0 && D + J >= 0 && 1 + D + -1*J >= 0 && -1 + A + D >= 0 && A + -1*C >= 0 && B >= 0 && B + J >= 0 && 1 + B + -1*J >= 0 && -1 + A + B >= 0 && 1 + -1*J >= 0 && A + -1*J >= 0 && J >= 0 && -1 + A + J >= 0 && -1 + A >= 0 && 1 + F >= A && 0 >= J] 17. f16(A,B,C,D,E,F,G,H,I,J) -> f74(A,B,C,D,E,F,G,H,I,J) [G + -1*H >= 0 (?,1) && F + -1*H >= 0 && H >= 0 && G + H >= 0 && F + H >= 0 && E + H >= 0 && D + H >= 0 && B + H >= 0 && -1 + A + H >= 0 && F + -1*G >= 0 && G >= 0 && F + G >= 0 && E + G >= 0 && -1*E + G >= 0 && D + G >= 0 && -1 + C + G >= 0 && B + G >= 0 && -1*B + G >= 0 && -1 + A + G >= 0 && F >= 0 && E + F >= 0 && -1*E + F >= 0 && D + F >= 0 && -1 + C + F >= 0 && 1 + -1*C + F >= 0 && B + F >= 0 && -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && B + E >= 0 && -1*B + E >= 0 && -1 + A + E >= 0 && D >= 0 && B + D >= 0 && -1 + A + D >= 0 && A + -1*C >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0 && 0 >= H] Signature: {(f0,10);(f16,10);(f25,10);(f50,10);(f74,10)} Flow Graph: [0->{1,2,3,4,5,6,17},1->{7,8,9,10,11,12,13},2->{7,8,9,10,11,12,13},3->{7,8,9,10,11,12,13},4->{7,8,9,10,11 ,12,13},5->{7,8,9,10,11,12,13},6->{7,8,9,10,11,12,13},7->{14,15,16},8->{14,15,16},9->{14,15,16},10->{14,15 ,16},11->{14,15,16},12->{14,15,16},13->{1,2,3,4,5,6,17},14->{1,2,3,4,5,6,17},15->{1,2,3,4,5,6,17},16->{1,2,3 ,4,5,6,17},17->{}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: UnsatPaths NO + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G,H,I,J) -> f16(1,0,1,N,0,M,L,K,I,J) [K >= 0 && L >= K && L >= 0 && M >= L && N >= 0 && M >= 0] (1,1) 1. f16(A,B,C,D,E,F,G,H,I,J) -> f25(A,B,C,D,1 + E,F,G,H,0,J) [G + -1*H >= 0 (?,1) && F + -1*H >= 0 && H >= 0 && G + H >= 0 && F + H >= 0 && E + H >= 0 && D + H >= 0 && B + H >= 0 && -1 + A + H >= 0 && F + -1*G >= 0 && G >= 0 && F + G >= 0 && E + G >= 0 && -1*E + G >= 0 && D + G >= 0 && -1 + C + G >= 0 && B + G >= 0 && -1*B + G >= 0 && -1 + A + G >= 0 && F >= 0 && E + F >= 0 && -1*E + F >= 0 && D + F >= 0 && -1 + C + F >= 0 && 1 + -1*C + F >= 0 && B + F >= 0 && -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && B + E >= 0 && -1*B + E >= 0 && -1 + A + E >= 0 && D >= 0 && B + D >= 0 && -1 + A + D >= 0 && A + -1*C >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0 && H >= 1 && 0 >= E && 0 >= D] 2. f16(A,B,C,D,E,F,G,H,I,J) -> f25(A,B,C,D,E,F,G,H,N,J) [G + -1*H >= 0 (?,1) && F + -1*H >= 0 && H >= 0 && G + H >= 0 && F + H >= 0 && E + H >= 0 && D + H >= 0 && B + H >= 0 && -1 + A + H >= 0 && F + -1*G >= 0 && G >= 0 && F + G >= 0 && E + G >= 0 && -1*E + G >= 0 && D + G >= 0 && -1 + C + G >= 0 && B + G >= 0 && -1*B + G >= 0 && -1 + A + G >= 0 && F >= 0 && E + F >= 0 && -1*E + F >= 0 && D + F >= 0 && -1 + C + F >= 0 && 1 + -1*C + F >= 0 && B + F >= 0 && -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && B + E >= 0 && -1*B + E >= 0 && -1 + A + E >= 0 && D >= 0 && B + D >= 0 && -1 + A + D >= 0 && A + -1*C >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0 && H >= 1 && E >= 2 && 0 >= D && 1 >= N && N >= 0] 3. f16(A,B,C,D,E,F,G,H,I,J) -> f25(A,1 + B,C,D,E,F,G,H,1,J) [G + -1*H >= 0 (?,1) && F + -1*H >= 0 && H >= 0 && G + H >= 0 && F + H >= 0 && E + H >= 0 && D + H >= 0 && B + H >= 0 && -1 + A + H >= 0 && F + -1*G >= 0 && G >= 0 && F + G >= 0 && E + G >= 0 && -1*E + G >= 0 && D + G >= 0 && -1 + C + G >= 0 && B + G >= 0 && -1*B + G >= 0 && -1 + A + G >= 0 && F >= 0 && E + F >= 0 && -1*E + F >= 0 && D + F >= 0 && -1 + C + F >= 0 && 1 + -1*C + F >= 0 && B + F >= 0 && -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && B + E >= 0 && -1*B + E >= 0 && -1 + A + E >= 0 && D >= 0 && B + D >= 0 && -1 + A + D >= 0 && A + -1*C >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0 && H >= 1 && 0 >= D && 0 >= B && E = 1] 4. f16(A,B,C,D,E,F,G,H,I,J) -> f25(A,0,-1 + C,D,E,F,G,H,0,J) [G + -1*H >= 0 (?,1) && F + -1*H >= 0 && H >= 0 && G + H >= 0 && F + H >= 0 && E + H >= 0 && D + H >= 0 && B + H >= 0 && -1 + A + H >= 0 && F + -1*G >= 0 && G >= 0 && F + G >= 0 && E + G >= 0 && -1*E + G >= 0 && D + G >= 0 && -1 + C + G >= 0 && B + G >= 0 && -1*B + G >= 0 && -1 + A + G >= 0 && F >= 0 && E + F >= 0 && -1*E + F >= 0 && D + F >= 0 && -1 + C + F >= 0 && 1 + -1*C + F >= 0 && B + F >= 0 && -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && B + E >= 0 && -1*B + E >= 0 && -1 + A + E >= 0 && D >= 0 && B + D >= 0 && -1 + A + D >= 0 && A + -1*C >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0 && H >= 1 && 0 >= D && C >= 1 && E = 1 && B = 1] 5. f16(A,B,C,D,E,F,G,H,I,J) -> f25(1 + A,0,1 + A,N,0,F,G,H,M,J) [G + -1*H >= 0 (?,1) && F + -1*H >= 0 && H >= 0 && G + H >= 0 && F + H >= 0 && E + H >= 0 && D + H >= 0 && B + H >= 0 && -1 + A + H >= 0 && F + -1*G >= 0 && G >= 0 && F + G >= 0 && E + G >= 0 && -1*E + G >= 0 && D + G >= 0 && -1 + C + G >= 0 && B + G >= 0 && -1*B + G >= 0 && -1 + A + G >= 0 && F >= 0 && E + F >= 0 && -1*E + F >= 0 && D + F >= 0 && -1 + C + F >= 0 && 1 + -1*C + F >= 0 && B + F >= 0 && -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && B + E >= 0 && -1*B + E >= 0 && -1 + A + E >= 0 && D >= 0 && B + D >= 0 && -1 + A + D >= 0 && A + -1*C >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0 && H >= 1 && 0 >= D && 0 >= C && M >= 0 && 1 >= M && N >= 0 && E = 1 && B = 1] 6. f16(A,B,C,D,E,F,G,H,I,J) -> f25(A,B,C,-1 + D,E,F,G,H,N,J) [G + -1*H >= 0 (?,1) && F + -1*H >= 0 && H >= 0 && G + H >= 0 && F + H >= 0 && E + H >= 0 && D + H >= 0 && B + H >= 0 && -1 + A + H >= 0 && F + -1*G >= 0 && G >= 0 && F + G >= 0 && E + G >= 0 && -1*E + G >= 0 && D + G >= 0 && -1 + C + G >= 0 && B + G >= 0 && -1*B + G >= 0 && -1 + A + G >= 0 && F >= 0 && E + F >= 0 && -1*E + F >= 0 && D + F >= 0 && -1 + C + F >= 0 && 1 + -1*C + F >= 0 && B + F >= 0 && -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && B + E >= 0 && -1*B + E >= 0 && -1 + A + E >= 0 && D >= 0 && B + D >= 0 && -1 + A + D >= 0 && A + -1*C >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0 && H >= 1 && D >= 1 && 1 >= N && N >= 0] 7. f25(A,B,C,D,E,F,G,H,I,J) -> f50(A,B,C,D,1 + E,F,G,H,I,0) [1 + -1*I >= 0 (?,1) && H + -1*I >= 0 && G + -1*I >= 0 && F + -1*I >= 0 && 1 + E + -1*I >= 0 && 1 + D + -1*I >= 0 && 1 + B + -1*I >= 0 && A + -1*I >= 0 && I >= 0 && -1 + H + I >= 0 && -1 + G + I >= 0 && -1 + F + I >= 0 && E + I >= 0 && D + I >= 0 && B + I >= 0 && -1 + A + I >= 0 && G + -1*H >= 0 && F + -1*H >= 0 && -1 + H >= 0 && -2 + G + H >= 0 && -2 + F + H >= 0 && -1 + E + H >= 0 && -1 + D + H >= 0 && -1 + B + H >= 0 && -2 + A + H >= 0 && F + -1*G >= 0 && -1 + G >= 0 && -2 + F + G >= 0 && -1 + E + G >= 0 && -1*E + G >= 0 && -1 + D + G >= 0 && -1 + C + G >= 0 && -1 + B + G >= 0 && -1*B + G >= 0 && -2 + A + G >= 0 && -1 + F >= 0 && -1 + E + F >= 0 && -1*E + F >= 0 && -1 + D + F >= 0 && -1 + C + F >= 0 && 2 + -1*C + F >= 0 && -1 + B + F >= 0 && -1*B + F >= 0 && -2 + A + F >= 0 && 2 + -1*A + F >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && B + E >= 0 && -1*B + E >= 0 && -1 + A + E >= 0 && D >= 0 && B + D >= 0 && -1 + A + D >= 0 && A + -1*C >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0 && I >= 1 && 0 >= E && 0 >= D] 8. f25(A,B,C,D,E,F,G,H,I,J) -> f50(A,B,C,D,E,F,G,H,I,N) [1 + -1*I >= 0 (?,1) && H + -1*I >= 0 && G + -1*I >= 0 && F + -1*I >= 0 && 1 + E + -1*I >= 0 && 1 + D + -1*I >= 0 && 1 + B + -1*I >= 0 && A + -1*I >= 0 && I >= 0 && -1 + H + I >= 0 && -1 + G + I >= 0 && -1 + F + I >= 0 && E + I >= 0 && D + I >= 0 && B + I >= 0 && -1 + A + I >= 0 && G + -1*H >= 0 && F + -1*H >= 0 && -1 + H >= 0 && -2 + G + H >= 0 && -2 + F + H >= 0 && -1 + E + H >= 0 && -1 + D + H >= 0 && -1 + B + H >= 0 && -2 + A + H >= 0 && F + -1*G >= 0 && -1 + G >= 0 && -2 + F + G >= 0 && -1 + E + G >= 0 && -1*E + G >= 0 && -1 + D + G >= 0 && -1 + C + G >= 0 && -1 + B + G >= 0 && -1*B + G >= 0 && -2 + A + G >= 0 && -1 + F >= 0 && -1 + E + F >= 0 && -1*E + F >= 0 && -1 + D + F >= 0 && -1 + C + F >= 0 && 2 + -1*C + F >= 0 && -1 + B + F >= 0 && -1*B + F >= 0 && -2 + A + F >= 0 && 2 + -1*A + F >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && B + E >= 0 && -1*B + E >= 0 && -1 + A + E >= 0 && D >= 0 && B + D >= 0 && -1 + A + D >= 0 && A + -1*C >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0 && I >= 1 && E >= 2 && 0 >= D && 1 >= N && N >= 0] 9. f25(A,B,C,D,E,F,G,H,I,J) -> f50(A,1 + B,C,D,E,F,G,H,I,1) [1 + -1*I >= 0 (?,1) && H + -1*I >= 0 && G + -1*I >= 0 && F + -1*I >= 0 && 1 + E + -1*I >= 0 && 1 + D + -1*I >= 0 && 1 + B + -1*I >= 0 && A + -1*I >= 0 && I >= 0 && -1 + H + I >= 0 && -1 + G + I >= 0 && -1 + F + I >= 0 && E + I >= 0 && D + I >= 0 && B + I >= 0 && -1 + A + I >= 0 && G + -1*H >= 0 && F + -1*H >= 0 && -1 + H >= 0 && -2 + G + H >= 0 && -2 + F + H >= 0 && -1 + E + H >= 0 && -1 + D + H >= 0 && -1 + B + H >= 0 && -2 + A + H >= 0 && F + -1*G >= 0 && -1 + G >= 0 && -2 + F + G >= 0 && -1 + E + G >= 0 && -1*E + G >= 0 && -1 + D + G >= 0 && -1 + C + G >= 0 && -1 + B + G >= 0 && -1*B + G >= 0 && -2 + A + G >= 0 && -1 + F >= 0 && -1 + E + F >= 0 && -1*E + F >= 0 && -1 + D + F >= 0 && -1 + C + F >= 0 && 2 + -1*C + F >= 0 && -1 + B + F >= 0 && -1*B + F >= 0 && -2 + A + F >= 0 && 2 + -1*A + F >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && B + E >= 0 && -1*B + E >= 0 && -1 + A + E >= 0 && D >= 0 && B + D >= 0 && -1 + A + D >= 0 && A + -1*C >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0 && I >= 1 && 0 >= D && 0 >= B && E = 1] 10. f25(A,B,C,D,E,F,G,H,I,J) -> f50(A,0,-1 + C,D,E,F,G,H,I,0) [1 + -1*I >= 0 (?,1) && H + -1*I >= 0 && G + -1*I >= 0 && F + -1*I >= 0 && 1 + E + -1*I >= 0 && 1 + D + -1*I >= 0 && 1 + B + -1*I >= 0 && A + -1*I >= 0 && I >= 0 && -1 + H + I >= 0 && -1 + G + I >= 0 && -1 + F + I >= 0 && E + I >= 0 && D + I >= 0 && B + I >= 0 && -1 + A + I >= 0 && G + -1*H >= 0 && F + -1*H >= 0 && -1 + H >= 0 && -2 + G + H >= 0 && -2 + F + H >= 0 && -1 + E + H >= 0 && -1 + D + H >= 0 && -1 + B + H >= 0 && -2 + A + H >= 0 && F + -1*G >= 0 && -1 + G >= 0 && -2 + F + G >= 0 && -1 + E + G >= 0 && -1*E + G >= 0 && -1 + D + G >= 0 && -1 + C + G >= 0 && -1 + B + G >= 0 && -1*B + G >= 0 && -2 + A + G >= 0 && -1 + F >= 0 && -1 + E + F >= 0 && -1*E + F >= 0 && -1 + D + F >= 0 && -1 + C + F >= 0 && 2 + -1*C + F >= 0 && -1 + B + F >= 0 && -1*B + F >= 0 && -2 + A + F >= 0 && 2 + -1*A + F >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && B + E >= 0 && -1*B + E >= 0 && -1 + A + E >= 0 && D >= 0 && B + D >= 0 && -1 + A + D >= 0 && A + -1*C >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0 && I >= 1 && 0 >= D && C >= 1 && E = 1 && B = 1] 11. f25(A,B,C,D,E,F,G,H,I,J) -> f50(1 + A,0,1 + A,N,0,F,G,H,I,M) [1 + -1*I >= 0 (?,1) && H + -1*I >= 0 && G + -1*I >= 0 && F + -1*I >= 0 && 1 + E + -1*I >= 0 && 1 + D + -1*I >= 0 && 1 + B + -1*I >= 0 && A + -1*I >= 0 && I >= 0 && -1 + H + I >= 0 && -1 + G + I >= 0 && -1 + F + I >= 0 && E + I >= 0 && D + I >= 0 && B + I >= 0 && -1 + A + I >= 0 && G + -1*H >= 0 && F + -1*H >= 0 && -1 + H >= 0 && -2 + G + H >= 0 && -2 + F + H >= 0 && -1 + E + H >= 0 && -1 + D + H >= 0 && -1 + B + H >= 0 && -2 + A + H >= 0 && F + -1*G >= 0 && -1 + G >= 0 && -2 + F + G >= 0 && -1 + E + G >= 0 && -1*E + G >= 0 && -1 + D + G >= 0 && -1 + C + G >= 0 && -1 + B + G >= 0 && -1*B + G >= 0 && -2 + A + G >= 0 && -1 + F >= 0 && -1 + E + F >= 0 && -1*E + F >= 0 && -1 + D + F >= 0 && -1 + C + F >= 0 && 2 + -1*C + F >= 0 && -1 + B + F >= 0 && -1*B + F >= 0 && -2 + A + F >= 0 && 2 + -1*A + F >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && B + E >= 0 && -1*B + E >= 0 && -1 + A + E >= 0 && D >= 0 && B + D >= 0 && -1 + A + D >= 0 && A + -1*C >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0 && I >= 1 && 0 >= D && 0 >= C && M >= 0 && 1 >= M && N >= 0 && E = 1 && B = 1] 12. f25(A,B,C,D,E,F,G,H,I,J) -> f50(A,B,C,-1 + D,E,F,G,H,I,N) [1 + -1*I >= 0 (?,1) && H + -1*I >= 0 && G + -1*I >= 0 && F + -1*I >= 0 && 1 + E + -1*I >= 0 && 1 + D + -1*I >= 0 && 1 + B + -1*I >= 0 && A + -1*I >= 0 && I >= 0 && -1 + H + I >= 0 && -1 + G + I >= 0 && -1 + F + I >= 0 && E + I >= 0 && D + I >= 0 && B + I >= 0 && -1 + A + I >= 0 && G + -1*H >= 0 && F + -1*H >= 0 && -1 + H >= 0 && -2 + G + H >= 0 && -2 + F + H >= 0 && -1 + E + H >= 0 && -1 + D + H >= 0 && -1 + B + H >= 0 && -2 + A + H >= 0 && F + -1*G >= 0 && -1 + G >= 0 && -2 + F + G >= 0 && -1 + E + G >= 0 && -1*E + G >= 0 && -1 + D + G >= 0 && -1 + C + G >= 0 && -1 + B + G >= 0 && -1*B + G >= 0 && -2 + A + G >= 0 && -1 + F >= 0 && -1 + E + F >= 0 && -1*E + F >= 0 && -1 + D + F >= 0 && -1 + C + F >= 0 && 2 + -1*C + F >= 0 && -1 + B + F >= 0 && -1*B + F >= 0 && -2 + A + F >= 0 && 2 + -1*A + F >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && B + E >= 0 && -1*B + E >= 0 && -1 + A + E >= 0 && D >= 0 && B + D >= 0 && -1 + A + D >= 0 && A + -1*C >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0 && I >= 1 && D >= 1 && 1 >= N && N >= 0] 13. f25(A,B,C,D,E,F,G,H,I,J) -> f16(A,B,C,D,E,F,G,H,I,J) [1 + -1*I >= 0 (?,1) && H + -1*I >= 0 && G + -1*I >= 0 && F + -1*I >= 0 && 1 + E + -1*I >= 0 && 1 + D + -1*I >= 0 && 1 + B + -1*I >= 0 && A + -1*I >= 0 && I >= 0 && -1 + H + I >= 0 && -1 + G + I >= 0 && -1 + F + I >= 0 && E + I >= 0 && D + I >= 0 && B + I >= 0 && -1 + A + I >= 0 && G + -1*H >= 0 && F + -1*H >= 0 && -1 + H >= 0 && -2 + G + H >= 0 && -2 + F + H >= 0 && -1 + E + H >= 0 && -1 + D + H >= 0 && -1 + B + H >= 0 && -2 + A + H >= 0 && F + -1*G >= 0 && -1 + G >= 0 && -2 + F + G >= 0 && -1 + E + G >= 0 && -1*E + G >= 0 && -1 + D + G >= 0 && -1 + C + G >= 0 && -1 + B + G >= 0 && -1*B + G >= 0 && -2 + A + G >= 0 && -1 + F >= 0 && -1 + E + F >= 0 && -1*E + F >= 0 && -1 + D + F >= 0 && -1 + C + F >= 0 && 2 + -1*C + F >= 0 && -1 + B + F >= 0 && -1*B + F >= 0 && -2 + A + F >= 0 && 2 + -1*A + F >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && B + E >= 0 && -1*B + E >= 0 && -1 + A + E >= 0 && D >= 0 && B + D >= 0 && -1 + A + D >= 0 && A + -1*C >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0 && 1 + F >= A && 0 >= I] 14. f50(A,B,C,D,E,F,G,H,I,J) -> f16(A,B,C,D,E,F,G,H,I,J) [1 + -1*I >= 0 (?,1) && H + -1*I >= 0 && G + -1*I >= 0 && F + -1*I >= 0 && 1 + E + -1*I >= 0 && 1 + D + -1*I >= 0 && 1 + B + -1*I >= 0 && 1 + -1*I + J >= 0 && 2 + -1*I + -1*J >= 0 && A + -1*I >= 0 && -1 + I >= 0 && -2 + H + I >= 0 && -2 + G + I >= 0 && -2 + F + I >= 0 && -1 + E + I >= 0 && -1 + D + I >= 0 && -1 + B + I >= 0 && -1 + I + J >= 0 && I + -1*J >= 0 && -2 + A + I >= 0 && G + -1*H >= 0 && F + -1*H >= 0 && -1 + H >= 0 && -2 + G + H >= 0 && -2 + F + H >= 0 && -1 + E + H >= 0 && -1 + D + H >= 0 && -1 + B + H >= 0 && -1 + H + J >= 0 && H + -1*J >= 0 && -2 + A + H >= 0 && F + -1*G >= 0 && -1 + G >= 0 && -2 + F + G >= 0 && -1 + E + G >= 0 && -1*E + G >= 0 && -1 + D + G >= 0 && -1 + C + G >= 0 && -1 + B + G >= 0 && -1*B + G >= 0 && -1 + G + J >= 0 && G + -1*J >= 0 && -2 + A + G >= 0 && -1 + F >= 0 && -1 + E + F >= 0 && -1*E + F >= 0 && -1 + D + F >= 0 && -1 + C + F >= 0 && 3 + -1*C + F >= 0 && -1 + B + F >= 0 && -1*B + F >= 0 && -1 + F + J >= 0 && F + -1*J >= 0 && -2 + A + F >= 0 && 3 + -1*A + F >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && B + E >= 0 && -1*B + E >= 0 && E + J >= 0 && 1 + E + -1*J >= 0 && -1 + A + E >= 0 && D >= 0 && B + D >= 0 && D + J >= 0 && 1 + D + -1*J >= 0 && -1 + A + D >= 0 && A + -1*C >= 0 && B >= 0 && B + J >= 0 && 1 + B + -1*J >= 0 && -1 + A + B >= 0 && 1 + -1*J >= 0 && A + -1*J >= 0 && J >= 0 && -1 + A + J >= 0 && -1 + A >= 0 && J >= 1 && 1 + F >= A && H >= G] 15. f50(A,B,C,D,E,F,G,H,I,J) -> f16(A,B,C,D,E,F,G,1 + H,I,J) [1 + -1*I >= 0 (?,1) && H + -1*I >= 0 && G + -1*I >= 0 && F + -1*I >= 0 && 1 + E + -1*I >= 0 && 1 + D + -1*I >= 0 && 1 + B + -1*I >= 0 && 1 + -1*I + J >= 0 && 2 + -1*I + -1*J >= 0 && A + -1*I >= 0 && -1 + I >= 0 && -2 + H + I >= 0 && -2 + G + I >= 0 && -2 + F + I >= 0 && -1 + E + I >= 0 && -1 + D + I >= 0 && -1 + B + I >= 0 && -1 + I + J >= 0 && I + -1*J >= 0 && -2 + A + I >= 0 && G + -1*H >= 0 && F + -1*H >= 0 && -1 + H >= 0 && -2 + G + H >= 0 && -2 + F + H >= 0 && -1 + E + H >= 0 && -1 + D + H >= 0 && -1 + B + H >= 0 && -1 + H + J >= 0 && H + -1*J >= 0 && -2 + A + H >= 0 && F + -1*G >= 0 && -1 + G >= 0 && -2 + F + G >= 0 && -1 + E + G >= 0 && -1*E + G >= 0 && -1 + D + G >= 0 && -1 + C + G >= 0 && -1 + B + G >= 0 && -1*B + G >= 0 && -1 + G + J >= 0 && G + -1*J >= 0 && -2 + A + G >= 0 && -1 + F >= 0 && -1 + E + F >= 0 && -1*E + F >= 0 && -1 + D + F >= 0 && -1 + C + F >= 0 && 3 + -1*C + F >= 0 && -1 + B + F >= 0 && -1*B + F >= 0 && -1 + F + J >= 0 && F + -1*J >= 0 && -2 + A + F >= 0 && 3 + -1*A + F >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && B + E >= 0 && -1*B + E >= 0 && E + J >= 0 && 1 + E + -1*J >= 0 && -1 + A + E >= 0 && D >= 0 && B + D >= 0 && D + J >= 0 && 1 + D + -1*J >= 0 && -1 + A + D >= 0 && A + -1*C >= 0 && B >= 0 && B + J >= 0 && 1 + B + -1*J >= 0 && -1 + A + B >= 0 && 1 + -1*J >= 0 && A + -1*J >= 0 && J >= 0 && -1 + A + J >= 0 && -1 + A >= 0 && J >= 1 && 1 + F >= A && G >= 1 + H] 16. f50(A,B,C,D,E,F,G,H,I,J) -> f16(A,B,C,D,E,F,G,-1 + H,I,J) [1 + -1*I >= 0 (?,1) && H + -1*I >= 0 && G + -1*I >= 0 && F + -1*I >= 0 && 1 + E + -1*I >= 0 && 1 + D + -1*I >= 0 && 1 + B + -1*I >= 0 && 1 + -1*I + J >= 0 && 2 + -1*I + -1*J >= 0 && A + -1*I >= 0 && -1 + I >= 0 && -2 + H + I >= 0 && -2 + G + I >= 0 && -2 + F + I >= 0 && -1 + E + I >= 0 && -1 + D + I >= 0 && -1 + B + I >= 0 && -1 + I + J >= 0 && I + -1*J >= 0 && -2 + A + I >= 0 && G + -1*H >= 0 && F + -1*H >= 0 && -1 + H >= 0 && -2 + G + H >= 0 && -2 + F + H >= 0 && -1 + E + H >= 0 && -1 + D + H >= 0 && -1 + B + H >= 0 && -1 + H + J >= 0 && H + -1*J >= 0 && -2 + A + H >= 0 && F + -1*G >= 0 && -1 + G >= 0 && -2 + F + G >= 0 && -1 + E + G >= 0 && -1*E + G >= 0 && -1 + D + G >= 0 && -1 + C + G >= 0 && -1 + B + G >= 0 && -1*B + G >= 0 && -1 + G + J >= 0 && G + -1*J >= 0 && -2 + A + G >= 0 && -1 + F >= 0 && -1 + E + F >= 0 && -1*E + F >= 0 && -1 + D + F >= 0 && -1 + C + F >= 0 && 3 + -1*C + F >= 0 && -1 + B + F >= 0 && -1*B + F >= 0 && -1 + F + J >= 0 && F + -1*J >= 0 && -2 + A + F >= 0 && 3 + -1*A + F >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && B + E >= 0 && -1*B + E >= 0 && E + J >= 0 && 1 + E + -1*J >= 0 && -1 + A + E >= 0 && D >= 0 && B + D >= 0 && D + J >= 0 && 1 + D + -1*J >= 0 && -1 + A + D >= 0 && A + -1*C >= 0 && B >= 0 && B + J >= 0 && 1 + B + -1*J >= 0 && -1 + A + B >= 0 && 1 + -1*J >= 0 && A + -1*J >= 0 && J >= 0 && -1 + A + J >= 0 && -1 + A >= 0 && 1 + F >= A && 0 >= J] 17. f16(A,B,C,D,E,F,G,H,I,J) -> f74(A,B,C,D,E,F,G,H,I,J) [G + -1*H >= 0 (1,1) && F + -1*H >= 0 && H >= 0 && G + H >= 0 && F + H >= 0 && E + H >= 0 && D + H >= 0 && B + H >= 0 && -1 + A + H >= 0 && F + -1*G >= 0 && G >= 0 && F + G >= 0 && E + G >= 0 && -1*E + G >= 0 && D + G >= 0 && -1 + C + G >= 0 && B + G >= 0 && -1*B + G >= 0 && -1 + A + G >= 0 && F >= 0 && E + F >= 0 && -1*E + F >= 0 && D + F >= 0 && -1 + C + F >= 0 && 1 + -1*C + F >= 0 && B + F >= 0 && -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && B + E >= 0 && -1*B + E >= 0 && -1 + A + E >= 0 && D >= 0 && B + D >= 0 && -1 + A + D >= 0 && A + -1*C >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0 && 0 >= H] Signature: {(f0,10);(f16,10);(f25,10);(f50,10);(f74,10)} Flow Graph: [0->{1,2,3,4,5,6,17},1->{7,8,9,10,11,12,13},2->{7,8,9,10,11,12,13},3->{7,8,9,10,11,12,13},4->{7,8,9,10,11 ,12,13},5->{7,8,9,10,11,12,13},6->{7,8,9,10,11,12,13},7->{14,15,16},8->{14,15,16},9->{14,15,16},10->{14,15 ,16},11->{14,15,16},12->{14,15,16},13->{1,2,3,4,5,6,17},14->{1,2,3,4,5,6,17},15->{1,2,3,4,5,6,17},16->{1,2,3 ,4,5,6,17},17->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(0,2) ,(0,3) ,(0,4) ,(0,5) ,(1,7) ,(1,8) ,(1,9) ,(1,10) ,(1,11) ,(1,12) ,(2,7) ,(2,9) ,(2,10) ,(2,11) ,(2,12) ,(3,7) ,(3,8) ,(3,9) ,(3,12) ,(3,13) ,(4,7) ,(4,8) ,(4,9) ,(4,10) ,(4,11) ,(4,12) ,(5,8) ,(5,9) ,(5,10) ,(5,11) ,(7,14) ,(7,15) ,(9,16) ,(10,14) ,(10,15) ,(13,17) ,(14,17) ,(15,17)] * Step 3: Looptree NO + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G,H,I,J) -> f16(1,0,1,N,0,M,L,K,I,J) [K >= 0 && L >= K && L >= 0 && M >= L && N >= 0 && M >= 0] (1,1) 1. f16(A,B,C,D,E,F,G,H,I,J) -> f25(A,B,C,D,1 + E,F,G,H,0,J) [G + -1*H >= 0 (?,1) && F + -1*H >= 0 && H >= 0 && G + H >= 0 && F + H >= 0 && E + H >= 0 && D + H >= 0 && B + H >= 0 && -1 + A + H >= 0 && F + -1*G >= 0 && G >= 0 && F + G >= 0 && E + G >= 0 && -1*E + G >= 0 && D + G >= 0 && -1 + C + G >= 0 && B + G >= 0 && -1*B + G >= 0 && -1 + A + G >= 0 && F >= 0 && E + F >= 0 && -1*E + F >= 0 && D + F >= 0 && -1 + C + F >= 0 && 1 + -1*C + F >= 0 && B + F >= 0 && -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && B + E >= 0 && -1*B + E >= 0 && -1 + A + E >= 0 && D >= 0 && B + D >= 0 && -1 + A + D >= 0 && A + -1*C >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0 && H >= 1 && 0 >= E && 0 >= D] 2. f16(A,B,C,D,E,F,G,H,I,J) -> f25(A,B,C,D,E,F,G,H,N,J) [G + -1*H >= 0 (?,1) && F + -1*H >= 0 && H >= 0 && G + H >= 0 && F + H >= 0 && E + H >= 0 && D + H >= 0 && B + H >= 0 && -1 + A + H >= 0 && F + -1*G >= 0 && G >= 0 && F + G >= 0 && E + G >= 0 && -1*E + G >= 0 && D + G >= 0 && -1 + C + G >= 0 && B + G >= 0 && -1*B + G >= 0 && -1 + A + G >= 0 && F >= 0 && E + F >= 0 && -1*E + F >= 0 && D + F >= 0 && -1 + C + F >= 0 && 1 + -1*C + F >= 0 && B + F >= 0 && -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && B + E >= 0 && -1*B + E >= 0 && -1 + A + E >= 0 && D >= 0 && B + D >= 0 && -1 + A + D >= 0 && A + -1*C >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0 && H >= 1 && E >= 2 && 0 >= D && 1 >= N && N >= 0] 3. f16(A,B,C,D,E,F,G,H,I,J) -> f25(A,1 + B,C,D,E,F,G,H,1,J) [G + -1*H >= 0 (?,1) && F + -1*H >= 0 && H >= 0 && G + H >= 0 && F + H >= 0 && E + H >= 0 && D + H >= 0 && B + H >= 0 && -1 + A + H >= 0 && F + -1*G >= 0 && G >= 0 && F + G >= 0 && E + G >= 0 && -1*E + G >= 0 && D + G >= 0 && -1 + C + G >= 0 && B + G >= 0 && -1*B + G >= 0 && -1 + A + G >= 0 && F >= 0 && E + F >= 0 && -1*E + F >= 0 && D + F >= 0 && -1 + C + F >= 0 && 1 + -1*C + F >= 0 && B + F >= 0 && -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && B + E >= 0 && -1*B + E >= 0 && -1 + A + E >= 0 && D >= 0 && B + D >= 0 && -1 + A + D >= 0 && A + -1*C >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0 && H >= 1 && 0 >= D && 0 >= B && E = 1] 4. f16(A,B,C,D,E,F,G,H,I,J) -> f25(A,0,-1 + C,D,E,F,G,H,0,J) [G + -1*H >= 0 (?,1) && F + -1*H >= 0 && H >= 0 && G + H >= 0 && F + H >= 0 && E + H >= 0 && D + H >= 0 && B + H >= 0 && -1 + A + H >= 0 && F + -1*G >= 0 && G >= 0 && F + G >= 0 && E + G >= 0 && -1*E + G >= 0 && D + G >= 0 && -1 + C + G >= 0 && B + G >= 0 && -1*B + G >= 0 && -1 + A + G >= 0 && F >= 0 && E + F >= 0 && -1*E + F >= 0 && D + F >= 0 && -1 + C + F >= 0 && 1 + -1*C + F >= 0 && B + F >= 0 && -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && B + E >= 0 && -1*B + E >= 0 && -1 + A + E >= 0 && D >= 0 && B + D >= 0 && -1 + A + D >= 0 && A + -1*C >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0 && H >= 1 && 0 >= D && C >= 1 && E = 1 && B = 1] 5. f16(A,B,C,D,E,F,G,H,I,J) -> f25(1 + A,0,1 + A,N,0,F,G,H,M,J) [G + -1*H >= 0 (?,1) && F + -1*H >= 0 && H >= 0 && G + H >= 0 && F + H >= 0 && E + H >= 0 && D + H >= 0 && B + H >= 0 && -1 + A + H >= 0 && F + -1*G >= 0 && G >= 0 && F + G >= 0 && E + G >= 0 && -1*E + G >= 0 && D + G >= 0 && -1 + C + G >= 0 && B + G >= 0 && -1*B + G >= 0 && -1 + A + G >= 0 && F >= 0 && E + F >= 0 && -1*E + F >= 0 && D + F >= 0 && -1 + C + F >= 0 && 1 + -1*C + F >= 0 && B + F >= 0 && -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && B + E >= 0 && -1*B + E >= 0 && -1 + A + E >= 0 && D >= 0 && B + D >= 0 && -1 + A + D >= 0 && A + -1*C >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0 && H >= 1 && 0 >= D && 0 >= C && M >= 0 && 1 >= M && N >= 0 && E = 1 && B = 1] 6. f16(A,B,C,D,E,F,G,H,I,J) -> f25(A,B,C,-1 + D,E,F,G,H,N,J) [G + -1*H >= 0 (?,1) && F + -1*H >= 0 && H >= 0 && G + H >= 0 && F + H >= 0 && E + H >= 0 && D + H >= 0 && B + H >= 0 && -1 + A + H >= 0 && F + -1*G >= 0 && G >= 0 && F + G >= 0 && E + G >= 0 && -1*E + G >= 0 && D + G >= 0 && -1 + C + G >= 0 && B + G >= 0 && -1*B + G >= 0 && -1 + A + G >= 0 && F >= 0 && E + F >= 0 && -1*E + F >= 0 && D + F >= 0 && -1 + C + F >= 0 && 1 + -1*C + F >= 0 && B + F >= 0 && -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && B + E >= 0 && -1*B + E >= 0 && -1 + A + E >= 0 && D >= 0 && B + D >= 0 && -1 + A + D >= 0 && A + -1*C >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0 && H >= 1 && D >= 1 && 1 >= N && N >= 0] 7. f25(A,B,C,D,E,F,G,H,I,J) -> f50(A,B,C,D,1 + E,F,G,H,I,0) [1 + -1*I >= 0 (?,1) && H + -1*I >= 0 && G + -1*I >= 0 && F + -1*I >= 0 && 1 + E + -1*I >= 0 && 1 + D + -1*I >= 0 && 1 + B + -1*I >= 0 && A + -1*I >= 0 && I >= 0 && -1 + H + I >= 0 && -1 + G + I >= 0 && -1 + F + I >= 0 && E + I >= 0 && D + I >= 0 && B + I >= 0 && -1 + A + I >= 0 && G + -1*H >= 0 && F + -1*H >= 0 && -1 + H >= 0 && -2 + G + H >= 0 && -2 + F + H >= 0 && -1 + E + H >= 0 && -1 + D + H >= 0 && -1 + B + H >= 0 && -2 + A + H >= 0 && F + -1*G >= 0 && -1 + G >= 0 && -2 + F + G >= 0 && -1 + E + G >= 0 && -1*E + G >= 0 && -1 + D + G >= 0 && -1 + C + G >= 0 && -1 + B + G >= 0 && -1*B + G >= 0 && -2 + A + G >= 0 && -1 + F >= 0 && -1 + E + F >= 0 && -1*E + F >= 0 && -1 + D + F >= 0 && -1 + C + F >= 0 && 2 + -1*C + F >= 0 && -1 + B + F >= 0 && -1*B + F >= 0 && -2 + A + F >= 0 && 2 + -1*A + F >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && B + E >= 0 && -1*B + E >= 0 && -1 + A + E >= 0 && D >= 0 && B + D >= 0 && -1 + A + D >= 0 && A + -1*C >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0 && I >= 1 && 0 >= E && 0 >= D] 8. f25(A,B,C,D,E,F,G,H,I,J) -> f50(A,B,C,D,E,F,G,H,I,N) [1 + -1*I >= 0 (?,1) && H + -1*I >= 0 && G + -1*I >= 0 && F + -1*I >= 0 && 1 + E + -1*I >= 0 && 1 + D + -1*I >= 0 && 1 + B + -1*I >= 0 && A + -1*I >= 0 && I >= 0 && -1 + H + I >= 0 && -1 + G + I >= 0 && -1 + F + I >= 0 && E + I >= 0 && D + I >= 0 && B + I >= 0 && -1 + A + I >= 0 && G + -1*H >= 0 && F + -1*H >= 0 && -1 + H >= 0 && -2 + G + H >= 0 && -2 + F + H >= 0 && -1 + E + H >= 0 && -1 + D + H >= 0 && -1 + B + H >= 0 && -2 + A + H >= 0 && F + -1*G >= 0 && -1 + G >= 0 && -2 + F + G >= 0 && -1 + E + G >= 0 && -1*E + G >= 0 && -1 + D + G >= 0 && -1 + C + G >= 0 && -1 + B + G >= 0 && -1*B + G >= 0 && -2 + A + G >= 0 && -1 + F >= 0 && -1 + E + F >= 0 && -1*E + F >= 0 && -1 + D + F >= 0 && -1 + C + F >= 0 && 2 + -1*C + F >= 0 && -1 + B + F >= 0 && -1*B + F >= 0 && -2 + A + F >= 0 && 2 + -1*A + F >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && B + E >= 0 && -1*B + E >= 0 && -1 + A + E >= 0 && D >= 0 && B + D >= 0 && -1 + A + D >= 0 && A + -1*C >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0 && I >= 1 && E >= 2 && 0 >= D && 1 >= N && N >= 0] 9. f25(A,B,C,D,E,F,G,H,I,J) -> f50(A,1 + B,C,D,E,F,G,H,I,1) [1 + -1*I >= 0 (?,1) && H + -1*I >= 0 && G + -1*I >= 0 && F + -1*I >= 0 && 1 + E + -1*I >= 0 && 1 + D + -1*I >= 0 && 1 + B + -1*I >= 0 && A + -1*I >= 0 && I >= 0 && -1 + H + I >= 0 && -1 + G + I >= 0 && -1 + F + I >= 0 && E + I >= 0 && D + I >= 0 && B + I >= 0 && -1 + A + I >= 0 && G + -1*H >= 0 && F + -1*H >= 0 && -1 + H >= 0 && -2 + G + H >= 0 && -2 + F + H >= 0 && -1 + E + H >= 0 && -1 + D + H >= 0 && -1 + B + H >= 0 && -2 + A + H >= 0 && F + -1*G >= 0 && -1 + G >= 0 && -2 + F + G >= 0 && -1 + E + G >= 0 && -1*E + G >= 0 && -1 + D + G >= 0 && -1 + C + G >= 0 && -1 + B + G >= 0 && -1*B + G >= 0 && -2 + A + G >= 0 && -1 + F >= 0 && -1 + E + F >= 0 && -1*E + F >= 0 && -1 + D + F >= 0 && -1 + C + F >= 0 && 2 + -1*C + F >= 0 && -1 + B + F >= 0 && -1*B + F >= 0 && -2 + A + F >= 0 && 2 + -1*A + F >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && B + E >= 0 && -1*B + E >= 0 && -1 + A + E >= 0 && D >= 0 && B + D >= 0 && -1 + A + D >= 0 && A + -1*C >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0 && I >= 1 && 0 >= D && 0 >= B && E = 1] 10. f25(A,B,C,D,E,F,G,H,I,J) -> f50(A,0,-1 + C,D,E,F,G,H,I,0) [1 + -1*I >= 0 (?,1) && H + -1*I >= 0 && G + -1*I >= 0 && F + -1*I >= 0 && 1 + E + -1*I >= 0 && 1 + D + -1*I >= 0 && 1 + B + -1*I >= 0 && A + -1*I >= 0 && I >= 0 && -1 + H + I >= 0 && -1 + G + I >= 0 && -1 + F + I >= 0 && E + I >= 0 && D + I >= 0 && B + I >= 0 && -1 + A + I >= 0 && G + -1*H >= 0 && F + -1*H >= 0 && -1 + H >= 0 && -2 + G + H >= 0 && -2 + F + H >= 0 && -1 + E + H >= 0 && -1 + D + H >= 0 && -1 + B + H >= 0 && -2 + A + H >= 0 && F + -1*G >= 0 && -1 + G >= 0 && -2 + F + G >= 0 && -1 + E + G >= 0 && -1*E + G >= 0 && -1 + D + G >= 0 && -1 + C + G >= 0 && -1 + B + G >= 0 && -1*B + G >= 0 && -2 + A + G >= 0 && -1 + F >= 0 && -1 + E + F >= 0 && -1*E + F >= 0 && -1 + D + F >= 0 && -1 + C + F >= 0 && 2 + -1*C + F >= 0 && -1 + B + F >= 0 && -1*B + F >= 0 && -2 + A + F >= 0 && 2 + -1*A + F >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && B + E >= 0 && -1*B + E >= 0 && -1 + A + E >= 0 && D >= 0 && B + D >= 0 && -1 + A + D >= 0 && A + -1*C >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0 && I >= 1 && 0 >= D && C >= 1 && E = 1 && B = 1] 11. f25(A,B,C,D,E,F,G,H,I,J) -> f50(1 + A,0,1 + A,N,0,F,G,H,I,M) [1 + -1*I >= 0 (?,1) && H + -1*I >= 0 && G + -1*I >= 0 && F + -1*I >= 0 && 1 + E + -1*I >= 0 && 1 + D + -1*I >= 0 && 1 + B + -1*I >= 0 && A + -1*I >= 0 && I >= 0 && -1 + H + I >= 0 && -1 + G + I >= 0 && -1 + F + I >= 0 && E + I >= 0 && D + I >= 0 && B + I >= 0 && -1 + A + I >= 0 && G + -1*H >= 0 && F + -1*H >= 0 && -1 + H >= 0 && -2 + G + H >= 0 && -2 + F + H >= 0 && -1 + E + H >= 0 && -1 + D + H >= 0 && -1 + B + H >= 0 && -2 + A + H >= 0 && F + -1*G >= 0 && -1 + G >= 0 && -2 + F + G >= 0 && -1 + E + G >= 0 && -1*E + G >= 0 && -1 + D + G >= 0 && -1 + C + G >= 0 && -1 + B + G >= 0 && -1*B + G >= 0 && -2 + A + G >= 0 && -1 + F >= 0 && -1 + E + F >= 0 && -1*E + F >= 0 && -1 + D + F >= 0 && -1 + C + F >= 0 && 2 + -1*C + F >= 0 && -1 + B + F >= 0 && -1*B + F >= 0 && -2 + A + F >= 0 && 2 + -1*A + F >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && B + E >= 0 && -1*B + E >= 0 && -1 + A + E >= 0 && D >= 0 && B + D >= 0 && -1 + A + D >= 0 && A + -1*C >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0 && I >= 1 && 0 >= D && 0 >= C && M >= 0 && 1 >= M && N >= 0 && E = 1 && B = 1] 12. f25(A,B,C,D,E,F,G,H,I,J) -> f50(A,B,C,-1 + D,E,F,G,H,I,N) [1 + -1*I >= 0 (?,1) && H + -1*I >= 0 && G + -1*I >= 0 && F + -1*I >= 0 && 1 + E + -1*I >= 0 && 1 + D + -1*I >= 0 && 1 + B + -1*I >= 0 && A + -1*I >= 0 && I >= 0 && -1 + H + I >= 0 && -1 + G + I >= 0 && -1 + F + I >= 0 && E + I >= 0 && D + I >= 0 && B + I >= 0 && -1 + A + I >= 0 && G + -1*H >= 0 && F + -1*H >= 0 && -1 + H >= 0 && -2 + G + H >= 0 && -2 + F + H >= 0 && -1 + E + H >= 0 && -1 + D + H >= 0 && -1 + B + H >= 0 && -2 + A + H >= 0 && F + -1*G >= 0 && -1 + G >= 0 && -2 + F + G >= 0 && -1 + E + G >= 0 && -1*E + G >= 0 && -1 + D + G >= 0 && -1 + C + G >= 0 && -1 + B + G >= 0 && -1*B + G >= 0 && -2 + A + G >= 0 && -1 + F >= 0 && -1 + E + F >= 0 && -1*E + F >= 0 && -1 + D + F >= 0 && -1 + C + F >= 0 && 2 + -1*C + F >= 0 && -1 + B + F >= 0 && -1*B + F >= 0 && -2 + A + F >= 0 && 2 + -1*A + F >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && B + E >= 0 && -1*B + E >= 0 && -1 + A + E >= 0 && D >= 0 && B + D >= 0 && -1 + A + D >= 0 && A + -1*C >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0 && I >= 1 && D >= 1 && 1 >= N && N >= 0] 13. f25(A,B,C,D,E,F,G,H,I,J) -> f16(A,B,C,D,E,F,G,H,I,J) [1 + -1*I >= 0 (?,1) && H + -1*I >= 0 && G + -1*I >= 0 && F + -1*I >= 0 && 1 + E + -1*I >= 0 && 1 + D + -1*I >= 0 && 1 + B + -1*I >= 0 && A + -1*I >= 0 && I >= 0 && -1 + H + I >= 0 && -1 + G + I >= 0 && -1 + F + I >= 0 && E + I >= 0 && D + I >= 0 && B + I >= 0 && -1 + A + I >= 0 && G + -1*H >= 0 && F + -1*H >= 0 && -1 + H >= 0 && -2 + G + H >= 0 && -2 + F + H >= 0 && -1 + E + H >= 0 && -1 + D + H >= 0 && -1 + B + H >= 0 && -2 + A + H >= 0 && F + -1*G >= 0 && -1 + G >= 0 && -2 + F + G >= 0 && -1 + E + G >= 0 && -1*E + G >= 0 && -1 + D + G >= 0 && -1 + C + G >= 0 && -1 + B + G >= 0 && -1*B + G >= 0 && -2 + A + G >= 0 && -1 + F >= 0 && -1 + E + F >= 0 && -1*E + F >= 0 && -1 + D + F >= 0 && -1 + C + F >= 0 && 2 + -1*C + F >= 0 && -1 + B + F >= 0 && -1*B + F >= 0 && -2 + A + F >= 0 && 2 + -1*A + F >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && B + E >= 0 && -1*B + E >= 0 && -1 + A + E >= 0 && D >= 0 && B + D >= 0 && -1 + A + D >= 0 && A + -1*C >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0 && 1 + F >= A && 0 >= I] 14. f50(A,B,C,D,E,F,G,H,I,J) -> f16(A,B,C,D,E,F,G,H,I,J) [1 + -1*I >= 0 (?,1) && H + -1*I >= 0 && G + -1*I >= 0 && F + -1*I >= 0 && 1 + E + -1*I >= 0 && 1 + D + -1*I >= 0 && 1 + B + -1*I >= 0 && 1 + -1*I + J >= 0 && 2 + -1*I + -1*J >= 0 && A + -1*I >= 0 && -1 + I >= 0 && -2 + H + I >= 0 && -2 + G + I >= 0 && -2 + F + I >= 0 && -1 + E + I >= 0 && -1 + D + I >= 0 && -1 + B + I >= 0 && -1 + I + J >= 0 && I + -1*J >= 0 && -2 + A + I >= 0 && G + -1*H >= 0 && F + -1*H >= 0 && -1 + H >= 0 && -2 + G + H >= 0 && -2 + F + H >= 0 && -1 + E + H >= 0 && -1 + D + H >= 0 && -1 + B + H >= 0 && -1 + H + J >= 0 && H + -1*J >= 0 && -2 + A + H >= 0 && F + -1*G >= 0 && -1 + G >= 0 && -2 + F + G >= 0 && -1 + E + G >= 0 && -1*E + G >= 0 && -1 + D + G >= 0 && -1 + C + G >= 0 && -1 + B + G >= 0 && -1*B + G >= 0 && -1 + G + J >= 0 && G + -1*J >= 0 && -2 + A + G >= 0 && -1 + F >= 0 && -1 + E + F >= 0 && -1*E + F >= 0 && -1 + D + F >= 0 && -1 + C + F >= 0 && 3 + -1*C + F >= 0 && -1 + B + F >= 0 && -1*B + F >= 0 && -1 + F + J >= 0 && F + -1*J >= 0 && -2 + A + F >= 0 && 3 + -1*A + F >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && B + E >= 0 && -1*B + E >= 0 && E + J >= 0 && 1 + E + -1*J >= 0 && -1 + A + E >= 0 && D >= 0 && B + D >= 0 && D + J >= 0 && 1 + D + -1*J >= 0 && -1 + A + D >= 0 && A + -1*C >= 0 && B >= 0 && B + J >= 0 && 1 + B + -1*J >= 0 && -1 + A + B >= 0 && 1 + -1*J >= 0 && A + -1*J >= 0 && J >= 0 && -1 + A + J >= 0 && -1 + A >= 0 && J >= 1 && 1 + F >= A && H >= G] 15. f50(A,B,C,D,E,F,G,H,I,J) -> f16(A,B,C,D,E,F,G,1 + H,I,J) [1 + -1*I >= 0 (?,1) && H + -1*I >= 0 && G + -1*I >= 0 && F + -1*I >= 0 && 1 + E + -1*I >= 0 && 1 + D + -1*I >= 0 && 1 + B + -1*I >= 0 && 1 + -1*I + J >= 0 && 2 + -1*I + -1*J >= 0 && A + -1*I >= 0 && -1 + I >= 0 && -2 + H + I >= 0 && -2 + G + I >= 0 && -2 + F + I >= 0 && -1 + E + I >= 0 && -1 + D + I >= 0 && -1 + B + I >= 0 && -1 + I + J >= 0 && I + -1*J >= 0 && -2 + A + I >= 0 && G + -1*H >= 0 && F + -1*H >= 0 && -1 + H >= 0 && -2 + G + H >= 0 && -2 + F + H >= 0 && -1 + E + H >= 0 && -1 + D + H >= 0 && -1 + B + H >= 0 && -1 + H + J >= 0 && H + -1*J >= 0 && -2 + A + H >= 0 && F + -1*G >= 0 && -1 + G >= 0 && -2 + F + G >= 0 && -1 + E + G >= 0 && -1*E + G >= 0 && -1 + D + G >= 0 && -1 + C + G >= 0 && -1 + B + G >= 0 && -1*B + G >= 0 && -1 + G + J >= 0 && G + -1*J >= 0 && -2 + A + G >= 0 && -1 + F >= 0 && -1 + E + F >= 0 && -1*E + F >= 0 && -1 + D + F >= 0 && -1 + C + F >= 0 && 3 + -1*C + F >= 0 && -1 + B + F >= 0 && -1*B + F >= 0 && -1 + F + J >= 0 && F + -1*J >= 0 && -2 + A + F >= 0 && 3 + -1*A + F >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && B + E >= 0 && -1*B + E >= 0 && E + J >= 0 && 1 + E + -1*J >= 0 && -1 + A + E >= 0 && D >= 0 && B + D >= 0 && D + J >= 0 && 1 + D + -1*J >= 0 && -1 + A + D >= 0 && A + -1*C >= 0 && B >= 0 && B + J >= 0 && 1 + B + -1*J >= 0 && -1 + A + B >= 0 && 1 + -1*J >= 0 && A + -1*J >= 0 && J >= 0 && -1 + A + J >= 0 && -1 + A >= 0 && J >= 1 && 1 + F >= A && G >= 1 + H] 16. f50(A,B,C,D,E,F,G,H,I,J) -> f16(A,B,C,D,E,F,G,-1 + H,I,J) [1 + -1*I >= 0 (?,1) && H + -1*I >= 0 && G + -1*I >= 0 && F + -1*I >= 0 && 1 + E + -1*I >= 0 && 1 + D + -1*I >= 0 && 1 + B + -1*I >= 0 && 1 + -1*I + J >= 0 && 2 + -1*I + -1*J >= 0 && A + -1*I >= 0 && -1 + I >= 0 && -2 + H + I >= 0 && -2 + G + I >= 0 && -2 + F + I >= 0 && -1 + E + I >= 0 && -1 + D + I >= 0 && -1 + B + I >= 0 && -1 + I + J >= 0 && I + -1*J >= 0 && -2 + A + I >= 0 && G + -1*H >= 0 && F + -1*H >= 0 && -1 + H >= 0 && -2 + G + H >= 0 && -2 + F + H >= 0 && -1 + E + H >= 0 && -1 + D + H >= 0 && -1 + B + H >= 0 && -1 + H + J >= 0 && H + -1*J >= 0 && -2 + A + H >= 0 && F + -1*G >= 0 && -1 + G >= 0 && -2 + F + G >= 0 && -1 + E + G >= 0 && -1*E + G >= 0 && -1 + D + G >= 0 && -1 + C + G >= 0 && -1 + B + G >= 0 && -1*B + G >= 0 && -1 + G + J >= 0 && G + -1*J >= 0 && -2 + A + G >= 0 && -1 + F >= 0 && -1 + E + F >= 0 && -1*E + F >= 0 && -1 + D + F >= 0 && -1 + C + F >= 0 && 3 + -1*C + F >= 0 && -1 + B + F >= 0 && -1*B + F >= 0 && -1 + F + J >= 0 && F + -1*J >= 0 && -2 + A + F >= 0 && 3 + -1*A + F >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && B + E >= 0 && -1*B + E >= 0 && E + J >= 0 && 1 + E + -1*J >= 0 && -1 + A + E >= 0 && D >= 0 && B + D >= 0 && D + J >= 0 && 1 + D + -1*J >= 0 && -1 + A + D >= 0 && A + -1*C >= 0 && B >= 0 && B + J >= 0 && 1 + B + -1*J >= 0 && -1 + A + B >= 0 && 1 + -1*J >= 0 && A + -1*J >= 0 && J >= 0 && -1 + A + J >= 0 && -1 + A >= 0 && 1 + F >= A && 0 >= J] 17. f16(A,B,C,D,E,F,G,H,I,J) -> f74(A,B,C,D,E,F,G,H,I,J) [G + -1*H >= 0 (1,1) && F + -1*H >= 0 && H >= 0 && G + H >= 0 && F + H >= 0 && E + H >= 0 && D + H >= 0 && B + H >= 0 && -1 + A + H >= 0 && F + -1*G >= 0 && G >= 0 && F + G >= 0 && E + G >= 0 && -1*E + G >= 0 && D + G >= 0 && -1 + C + G >= 0 && B + G >= 0 && -1*B + G >= 0 && -1 + A + G >= 0 && F >= 0 && E + F >= 0 && -1*E + F >= 0 && D + F >= 0 && -1 + C + F >= 0 && 1 + -1*C + F >= 0 && B + F >= 0 && -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && E >= 0 && D + E >= 0 && -1 + C + E >= 0 && B + E >= 0 && -1*B + E >= 0 && -1 + A + E >= 0 && D >= 0 && B + D >= 0 && -1 + A + D >= 0 && A + -1*C >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0 && 0 >= H] Signature: {(f0,10);(f16,10);(f25,10);(f50,10);(f74,10)} Flow Graph: [0->{1,6,17},1->{13},2->{8,13},3->{10,11},4->{13},5->{7,12,13},6->{7,8,9,10,11,12,13},7->{16},8->{14,15 ,16},9->{14,15},10->{16},11->{14,15,16},12->{14,15,16},13->{1,2,3,4,5,6},14->{1,2,3,4,5,6},15->{1,2,3,4,5,6} ,16->{1,2,3,4,5,6,17},17->{}] + Applied Processor: Looptree + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17] | `- p:[1,13,2,14,8,6,15,9,11,3,16,7,5,10,12,4] c: [11] | `- p:[1,13,2,14,8,6,15,9,12,5,16,7,10,3,4] c: [7] | `- p:[1,13,2,14,8,6,15,9,12,5,16,10,3,4] c: [5] | `- p:[1,13,2,14,8,6,15,9,12,16,10,3,4] c: [12] | `- p:[1,13,2,14,8,6,15,9,16,10,3,4] c: [10] | `- p:[1,13,2,14,8,6,15,9,16,4] c: [9] | `- p:[1,13,2,14,8,6,15,16,4] c: [6] | `- p:[1,13,2,14,8,15,16,4] c: [4] | `- p:[1,13,2,14,8,15,16] c: [1] | `- p:[2,13,14,8,15,16] c: [] NO