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