NO * Step 1: TrivialSCCs NO + Considered Problem: Rules: 0. f63(A,B,C,D,E,F,G,H,I,J,K) -> f11(A,B,C,D,E,F,G,H,I,J,K) [-1*G >= 0 (?,1) && -1 + F + -1*G >= 0 && 1 + -1*F + -1*G >= 0 && 20 + -1*E + -1*G >= 0 && -1 + D + -1*G >= 0 && -20 + C + -1*G >= 0 && 20 + -1*C + -1*G >= 0 && -10 + B + -1*G >= 0 && 10 + -1*B + -1*G >= 0 && -2 + -1*G + J >= 0 && 20 + -1*A + -1*G >= 0 && G >= 0 && -1 + F + G >= 0 && 1 + -1*F + G >= 0 && 20 + -1*E + G >= 0 && -1 + D + G >= 0 && -20 + C + G >= 0 && 20 + -1*C + G >= 0 && -10 + B + G >= 0 && 10 + -1*B + G >= 0 && -2 + G + J >= 0 && 20 + -1*A + G >= 0 && 1 + -1*F >= 0 && 21 + -1*E + -1*F >= 0 && D + -1*F >= 0 && -19 + C + -1*F >= 0 && 21 + -1*C + -1*F >= 0 && -9 + B + -1*F >= 0 && 11 + -1*B + -1*F >= 0 && -1 + -1*F + J >= 0 && 21 + -1*A + -1*F >= 0 && -1 + F >= 0 && 19 + -1*E + F >= 0 && -2 + D + F >= 0 && -21 + C + F >= 0 && 19 + -1*C + F >= 0 && -11 + B + F >= 0 && 9 + -1*B + F >= 0 && -3 + F + J >= 0 && 19 + -1*A + F >= 0 && 20 + -1*E >= 0 && 19 + D + -1*E >= 0 && C + -1*E >= 0 && 40 + -1*C + -1*E >= 0 && 10 + B + -1*E >= 0 && 30 + -1*B + -1*E >= 0 && 18 + -1*E + J >= 0 && 39 + -1*A + -1*E >= 0 && 1 + -1*A + E >= 0 && -1 + -1*D + J >= 0 && -1 + D >= 0 && -21 + C + D >= 0 && 19 + -1*C + D >= 0 && -11 + B + D >= 0 && 9 + -1*B + D >= 0 && -3 + D + J >= 0 && 19 + -1*A + D >= 0 && 20 + -1*C >= 0 && 10 + B + -1*C >= 0 && 30 + -1*B + -1*C >= 0 && 18 + -1*C + J >= 0 && 40 + -1*A + -1*C >= 0 && -20 + C >= 0 && -30 + B + C >= 0 && -10 + -1*B + C >= 0 && -22 + C + J >= 0 && -1*A + C >= 0 && 10 + -1*B >= 0 && 8 + -1*B + J >= 0 && 30 + -1*A + -1*B >= 0 && -10 + B >= 0 && -12 + B + J >= 0 && 10 + -1*A + B >= 0 && -2 + J >= 0 && 18 + -1*A + J >= 0 && 20 + -1*A >= 0 && A >= 1 + B] 1. f0(A,B,C,D,E,F,G,H,I,J,K) -> f11(A,10,20,1,20,0,0,H,I,J,K) True (1,1) 2. f11(A,B,C,D,E,F,G,H,I,J,K) -> f11(A,B,C,D,E,F,1,H,I,J,K) [G >= 0 (?,1) && F + G >= 0 && 1 + -1*F + G >= 0 && 20 + -1*E + G >= 0 && -1 + D + G >= 0 && -20 + C + G >= 0 && 20 + -1*C + G >= 0 && -10 + B + G >= 0 && 10 + -1*B + G >= 0 && 1 + -1*F >= 0 && 21 + -1*E + -1*F >= 0 && D + -1*F >= 0 && -19 + C + -1*F >= 0 && 21 + -1*C + -1*F >= 0 && -9 + B + -1*F >= 0 && 11 + -1*B + -1*F >= 0 && F >= 0 && 20 + -1*E + F >= 0 && -1 + D + F >= 0 && -20 + C + F >= 0 && 20 + -1*C + F >= 0 && -10 + B + F >= 0 && 10 + -1*B + F >= 0 && 20 + -1*E >= 0 && 19 + D + -1*E >= 0 && C + -1*E >= 0 && 40 + -1*C + -1*E >= 0 && 10 + B + -1*E >= 0 && 30 + -1*B + -1*E >= 0 && -1 + D >= 0 && -21 + C + D >= 0 && 19 + -1*C + D >= 0 && -11 + B + D >= 0 && 9 + -1*B + D >= 0 && 20 + -1*C >= 0 && 10 + B + -1*C >= 0 && 30 + -1*B + -1*C >= 0 && -20 + C >= 0 && -30 + B + C >= 0 && -10 + -1*B + C >= 0 && 10 + -1*B >= 0 && -10 + B >= 0 && D >= E && G = 0] 3. f11(A,B,C,D,E,F,G,H,I,J,K) -> f11(A,B,C,D,1 + D,F,1,H,I,J,K) [G >= 0 (?,1) && F + G >= 0 && 1 + -1*F + G >= 0 && 20 + -1*E + G >= 0 && -1 + D + G >= 0 && -20 + C + G >= 0 && 20 + -1*C + G >= 0 && -10 + B + G >= 0 && 10 + -1*B + G >= 0 && 1 + -1*F >= 0 && 21 + -1*E + -1*F >= 0 && D + -1*F >= 0 && -19 + C + -1*F >= 0 && 21 + -1*C + -1*F >= 0 && -9 + B + -1*F >= 0 && 11 + -1*B + -1*F >= 0 && F >= 0 && 20 + -1*E + F >= 0 && -1 + D + F >= 0 && -20 + C + F >= 0 && 20 + -1*C + F >= 0 && -10 + B + F >= 0 && 10 + -1*B + F >= 0 && 20 + -1*E >= 0 && 19 + D + -1*E >= 0 && C + -1*E >= 0 && 40 + -1*C + -1*E >= 0 && 10 + B + -1*E >= 0 && 30 + -1*B + -1*E >= 0 && -1 + D >= 0 && -21 + C + D >= 0 && 19 + -1*C + D >= 0 && -11 + B + D >= 0 && 9 + -1*B + D >= 0 && 20 + -1*C >= 0 && 10 + B + -1*C >= 0 && 30 + -1*B + -1*C >= 0 && -20 + C >= 0 && -30 + B + C >= 0 && -10 + -1*B + C >= 0 && 10 + -1*B >= 0 && -10 + B >= 0 && E = 1 + D && G = 0] 4. f11(A,B,C,D,E,F,G,H,I,J,K) -> f11(A,B,C,D,1 + D,F,1,N,I,J,K) [G >= 0 (?,1) && F + G >= 0 && 1 + -1*F + G >= 0 && 20 + -1*E + G >= 0 && -1 + D + G >= 0 && -20 + C + G >= 0 && 20 + -1*C + G >= 0 && -10 + B + G >= 0 && 10 + -1*B + G >= 0 && 1 + -1*F >= 0 && 21 + -1*E + -1*F >= 0 && D + -1*F >= 0 && -19 + C + -1*F >= 0 && 21 + -1*C + -1*F >= 0 && -9 + B + -1*F >= 0 && 11 + -1*B + -1*F >= 0 && F >= 0 && 20 + -1*E + F >= 0 && -1 + D + F >= 0 && -20 + C + F >= 0 && 20 + -1*C + F >= 0 && -10 + B + F >= 0 && 10 + -1*B + F >= 0 && 20 + -1*E >= 0 && 19 + D + -1*E >= 0 && C + -1*E >= 0 && 40 + -1*C + -1*E >= 0 && 10 + B + -1*E >= 0 && 30 + -1*B + -1*E >= 0 && -1 + D >= 0 && -21 + C + D >= 0 && 19 + -1*C + D >= 0 && -11 + B + D >= 0 && 9 + -1*B + D >= 0 && 20 + -1*C >= 0 && 10 + B + -1*C >= 0 && 30 + -1*B + -1*C >= 0 && -20 + C >= 0 && -30 + B + C >= 0 && -10 + -1*B + C >= 0 && 10 + -1*B >= 0 && -10 + B >= 0 && L >= 1 + M && E = 1 + D && G = 0] 5. f11(A,B,C,D,E,F,G,H,I,J,K) -> f40(E,B,C,D,E,F,0,N,L,1 + D,M) [G >= 0 (?,1) && F + G >= 0 && 1 + -1*F + G >= 0 && 20 + -1*E + G >= 0 && -1 + D + G >= 0 && -20 + C + G >= 0 && 20 + -1*C + G >= 0 && -10 + B + G >= 0 && 10 + -1*B + G >= 0 && 1 + -1*F >= 0 && 21 + -1*E + -1*F >= 0 && D + -1*F >= 0 && -19 + C + -1*F >= 0 && 21 + -1*C + -1*F >= 0 && -9 + B + -1*F >= 0 && 11 + -1*B + -1*F >= 0 && F >= 0 && 20 + -1*E + F >= 0 && -1 + D + F >= 0 && -20 + C + F >= 0 && 20 + -1*C + F >= 0 && -10 + B + F >= 0 && 10 + -1*B + F >= 0 && 20 + -1*E >= 0 && 19 + D + -1*E >= 0 && C + -1*E >= 0 && 40 + -1*C + -1*E >= 0 && 10 + B + -1*E >= 0 && 30 + -1*B + -1*E >= 0 && -1 + D >= 0 && -21 + C + D >= 0 && 19 + -1*C + D >= 0 && -11 + B + D >= 0 && 9 + -1*B + D >= 0 && 20 + -1*C >= 0 && 10 + B + -1*C >= 0 && 30 + -1*B + -1*C >= 0 && -20 + C >= 0 && -30 + B + C >= 0 && -10 + -1*B + C >= 0 && 10 + -1*B >= 0 && -10 + B >= 0 && E >= 2 + D && G = 0] 6. f40(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,H,I,J,K) [-1*G >= 0 (?,1) && F + -1*G >= 0 && 1 + -1*F + -1*G >= 0 && 20 + -1*E + -1*G >= 0 && -1 + D + -1*G >= 0 && -20 + C + -1*G >= 0 && 20 + -1*C + -1*G >= 0 && -10 + B + -1*G >= 0 && 10 + -1*B + -1*G >= 0 && -2 + -1*G + J >= 0 && 20 + -1*A + -1*G >= 0 && G >= 0 && F + G >= 0 && 1 + -1*F + G >= 0 && 20 + -1*E + G >= 0 && -1 + D + G >= 0 && -20 + C + G >= 0 && 20 + -1*C + G >= 0 && -10 + B + G >= 0 && 10 + -1*B + G >= 0 && -2 + G + J >= 0 && 20 + -1*A + G >= 0 && 1 + -1*F >= 0 && 21 + -1*E + -1*F >= 0 && D + -1*F >= 0 && -19 + C + -1*F >= 0 && 21 + -1*C + -1*F >= 0 && -9 + B + -1*F >= 0 && 11 + -1*B + -1*F >= 0 && -1 + -1*F + J >= 0 && 21 + -1*A + -1*F >= 0 && F >= 0 && 20 + -1*E + F >= 0 && -1 + D + F >= 0 && -20 + C + F >= 0 && 20 + -1*C + F >= 0 && -10 + B + F >= 0 && 10 + -1*B + F >= 0 && -2 + F + J >= 0 && 20 + -1*A + F >= 0 && 20 + -1*E >= 0 && 19 + D + -1*E >= 0 && C + -1*E >= 0 && 40 + -1*C + -1*E >= 0 && 10 + B + -1*E >= 0 && 30 + -1*B + -1*E >= 0 && 18 + -1*E + J >= 0 && 40 + -1*A + -1*E >= 0 && -1*A + E >= 0 && -1 + -1*D + J >= 0 && -1 + D >= 0 && -21 + C + D >= 0 && 19 + -1*C + D >= 0 && -11 + B + D >= 0 && 9 + -1*B + D >= 0 && -3 + D + J >= 0 && 19 + -1*A + D >= 0 && 20 + -1*C >= 0 && 10 + B + -1*C >= 0 && 30 + -1*B + -1*C >= 0 && 18 + -1*C + J >= 0 && 40 + -1*A + -1*C >= 0 && -20 + C >= 0 && -30 + B + C >= 0 && -10 + -1*B + C >= 0 && -22 + C + J >= 0 && -1*A + C >= 0 && 10 + -1*B >= 0 && 8 + -1*B + J >= 0 && 30 + -1*A + -1*B >= 0 && -10 + B >= 0 && -12 + B + J >= 0 && 10 + -1*A + B >= 0 && -2 + J >= 0 && 18 + -1*A + J >= 0 && 20 + -1*A >= 0 && F >= 1] 7. f40(A,B,C,D,E,F,G,H,I,J,K) -> f43(A,B,C,D,E,0,G,H,I,1 + J,K) [-1*G >= 0 (?,1) && F + -1*G >= 0 && 1 + -1*F + -1*G >= 0 && 20 + -1*E + -1*G >= 0 && -1 + D + -1*G >= 0 && -20 + C + -1*G >= 0 && 20 + -1*C + -1*G >= 0 && -10 + B + -1*G >= 0 && 10 + -1*B + -1*G >= 0 && -2 + -1*G + J >= 0 && 20 + -1*A + -1*G >= 0 && G >= 0 && F + G >= 0 && 1 + -1*F + G >= 0 && 20 + -1*E + G >= 0 && -1 + D + G >= 0 && -20 + C + G >= 0 && 20 + -1*C + G >= 0 && -10 + B + G >= 0 && 10 + -1*B + G >= 0 && -2 + G + J >= 0 && 20 + -1*A + G >= 0 && 1 + -1*F >= 0 && 21 + -1*E + -1*F >= 0 && D + -1*F >= 0 && -19 + C + -1*F >= 0 && 21 + -1*C + -1*F >= 0 && -9 + B + -1*F >= 0 && 11 + -1*B + -1*F >= 0 && -1 + -1*F + J >= 0 && 21 + -1*A + -1*F >= 0 && F >= 0 && 20 + -1*E + F >= 0 && -1 + D + F >= 0 && -20 + C + F >= 0 && 20 + -1*C + F >= 0 && -10 + B + F >= 0 && 10 + -1*B + F >= 0 && -2 + F + J >= 0 && 20 + -1*A + F >= 0 && 20 + -1*E >= 0 && 19 + D + -1*E >= 0 && C + -1*E >= 0 && 40 + -1*C + -1*E >= 0 && 10 + B + -1*E >= 0 && 30 + -1*B + -1*E >= 0 && 18 + -1*E + J >= 0 && 40 + -1*A + -1*E >= 0 && -1*A + E >= 0 && -1 + -1*D + J >= 0 && -1 + D >= 0 && -21 + C + D >= 0 && 19 + -1*C + D >= 0 && -11 + B + D >= 0 && 9 + -1*B + D >= 0 && -3 + D + J >= 0 && 19 + -1*A + D >= 0 && 20 + -1*C >= 0 && 10 + B + -1*C >= 0 && 30 + -1*B + -1*C >= 0 && 18 + -1*C + J >= 0 && 40 + -1*A + -1*C >= 0 && -20 + C >= 0 && -30 + B + C >= 0 && -10 + -1*B + C >= 0 && -22 + C + J >= 0 && -1*A + C >= 0 && 10 + -1*B >= 0 && 8 + -1*B + J >= 0 && 30 + -1*A + -1*B >= 0 && -10 + B >= 0 && -12 + B + J >= 0 && 10 + -1*A + B >= 0 && -2 + J >= 0 && 18 + -1*A + J >= 0 && 20 + -1*A >= 0 && F = 0] 8. f43(A,B,C,D,E,F,G,H,I,J,K) -> f43(A,B,C,D,E,F,G,H,I,1 + J,K) [-1*G >= 0 (?,1) && F + -1*G >= 0 && -1*F + -1*G >= 0 && 20 + -1*E + -1*G >= 0 && -1 + D + -1*G >= 0 && -20 + C + -1*G >= 0 && 20 + -1*C + -1*G >= 0 && -10 + B + -1*G >= 0 && 10 + -1*B + -1*G >= 0 && -3 + -1*G + J >= 0 && 20 + -1*A + -1*G >= 0 && G >= 0 && F + G >= 0 && -1*F + G >= 0 && 20 + -1*E + G >= 0 && -1 + D + G >= 0 && -20 + C + G >= 0 && 20 + -1*C + G >= 0 && -10 + B + G >= 0 && 10 + -1*B + G >= 0 && -3 + G + J >= 0 && 20 + -1*A + G >= 0 && -1*F >= 0 && 20 + -1*E + -1*F >= 0 && -1 + D + -1*F >= 0 && -20 + C + -1*F >= 0 && 20 + -1*C + -1*F >= 0 && -10 + B + -1*F >= 0 && 10 + -1*B + -1*F >= 0 && -3 + -1*F + J >= 0 && 20 + -1*A + -1*F >= 0 && F >= 0 && 20 + -1*E + F >= 0 && -1 + D + F >= 0 && -20 + C + F >= 0 && 20 + -1*C + F >= 0 && -10 + B + F >= 0 && 10 + -1*B + F >= 0 && -3 + F + J >= 0 && 20 + -1*A + F >= 0 && 20 + -1*E >= 0 && 19 + D + -1*E >= 0 && C + -1*E >= 0 && 40 + -1*C + -1*E >= 0 && 10 + B + -1*E >= 0 && 30 + -1*B + -1*E >= 0 && 17 + -1*E + J >= 0 && 40 + -1*A + -1*E >= 0 && -1*A + E >= 0 && -2 + -1*D + J >= 0 && -1 + D >= 0 && -21 + C + D >= 0 && 19 + -1*C + D >= 0 && -11 + B + D >= 0 && 9 + -1*B + D >= 0 && -4 + D + J >= 0 && 19 + -1*A + D >= 0 && 20 + -1*C >= 0 && 10 + B + -1*C >= 0 && 30 + -1*B + -1*C >= 0 && 17 + -1*C + J >= 0 && 40 + -1*A + -1*C >= 0 && -20 + C >= 0 && -30 + B + C >= 0 && -10 + -1*B + C >= 0 && -23 + C + J >= 0 && -1*A + C >= 0 && 10 + -1*B >= 0 && 7 + -1*B + J >= 0 && 30 + -1*A + -1*B >= 0 && -10 + B >= 0 && -13 + B + J >= 0 && 10 + -1*A + B >= 0 && -3 + J >= 0 && 17 + -1*A + J >= 0 && 20 + -1*A >= 0 && K >= 1 + N] 9. f48(A,B,C,D,E,F,G,H,I,J,K) -> f48(-1 + A,B,C,D,E,F,G,H,I,J,K) [-1*G >= 0 (?,1) && F + -1*G >= 0 && -1*F + -1*G >= 0 && 20 + -1*E + -1*G >= 0 && -1 + D + -1*G >= 0 && -20 + C + -1*G >= 0 && 20 + -1*C + -1*G >= 0 && -10 + B + -1*G >= 0 && 10 + -1*B + -1*G >= 0 && -3 + -1*G + J >= 0 && 19 + -1*A + -1*G >= 0 && G >= 0 && F + G >= 0 && -1*F + G >= 0 && 20 + -1*E + G >= 0 && -1 + D + G >= 0 && -20 + C + G >= 0 && 20 + -1*C + G >= 0 && -10 + B + G >= 0 && 10 + -1*B + G >= 0 && -3 + G + J >= 0 && 19 + -1*A + G >= 0 && -1*F >= 0 && 20 + -1*E + -1*F >= 0 && -1 + D + -1*F >= 0 && -20 + C + -1*F >= 0 && 20 + -1*C + -1*F >= 0 && -10 + B + -1*F >= 0 && 10 + -1*B + -1*F >= 0 && -3 + -1*F + J >= 0 && 19 + -1*A + -1*F >= 0 && F >= 0 && 20 + -1*E + F >= 0 && -1 + D + F >= 0 && -20 + C + F >= 0 && 20 + -1*C + F >= 0 && -10 + B + F >= 0 && 10 + -1*B + F >= 0 && -3 + F + J >= 0 && 19 + -1*A + F >= 0 && 20 + -1*E >= 0 && 19 + D + -1*E >= 0 && C + -1*E >= 0 && 40 + -1*C + -1*E >= 0 && 10 + B + -1*E >= 0 && 30 + -1*B + -1*E >= 0 && 17 + -1*E + J >= 0 && 39 + -1*A + -1*E >= 0 && -1 + -1*A + E >= 0 && -2 + -1*D + J >= 0 && -1 + D >= 0 && -21 + C + D >= 0 && 19 + -1*C + D >= 0 && -11 + B + D >= 0 && 9 + -1*B + D >= 0 && -4 + D + J >= 0 && 18 + -1*A + D >= 0 && 20 + -1*C >= 0 && 10 + B + -1*C >= 0 && 30 + -1*B + -1*C >= 0 && 17 + -1*C + J >= 0 && 39 + -1*A + -1*C >= 0 && -20 + C >= 0 && -30 + B + C >= 0 && -10 + -1*B + C >= 0 && -23 + C + J >= 0 && -1 + -1*A + C >= 0 && 10 + -1*B >= 0 && 7 + -1*B + J >= 0 && 29 + -1*A + -1*B >= 0 && -10 + B >= 0 && -13 + B + J >= 0 && 9 + -1*A + B >= 0 && -3 + J >= 0 && 16 + -1*A + J >= 0 && 19 + -1*A >= 0] 10. f54(A,B,C,D,E,F,G,H,I,J,K) -> f40(A,B,C,D,E,F,G,H,I,J,K) [-1*G >= 0 (?,1) && F + -1*G >= 0 && 1 + -1*F + -1*G >= 0 && 20 + -1*E + -1*G >= 0 && -1 + D + -1*G >= 0 && -20 + C + -1*G >= 0 && 20 + -1*C + -1*G >= 0 && -10 + B + -1*G >= 0 && 10 + -1*B + -1*G >= 0 && -3 + -1*G + J >= 0 && 19 + -1*A + -1*G >= 0 && G >= 0 && F + G >= 0 && 1 + -1*F + G >= 0 && 20 + -1*E + G >= 0 && -1 + D + G >= 0 && -20 + C + G >= 0 && 20 + -1*C + G >= 0 && -10 + B + G >= 0 && 10 + -1*B + G >= 0 && -3 + G + J >= 0 && 19 + -1*A + G >= 0 && 1 + -1*F >= 0 && 21 + -1*E + -1*F >= 0 && D + -1*F >= 0 && -19 + C + -1*F >= 0 && 21 + -1*C + -1*F >= 0 && -9 + B + -1*F >= 0 && 11 + -1*B + -1*F >= 0 && -2 + -1*F + J >= 0 && 20 + -1*A + -1*F >= 0 && F >= 0 && 20 + -1*E + F >= 0 && -1 + D + F >= 0 && -20 + C + F >= 0 && 20 + -1*C + F >= 0 && -10 + B + F >= 0 && 10 + -1*B + F >= 0 && -3 + F + J >= 0 && 19 + -1*A + F >= 0 && 20 + -1*E >= 0 && 19 + D + -1*E >= 0 && C + -1*E >= 0 && 40 + -1*C + -1*E >= 0 && 10 + B + -1*E >= 0 && 30 + -1*B + -1*E >= 0 && 17 + -1*E + J >= 0 && 39 + -1*A + -1*E >= 0 && -1 + -1*A + E >= 0 && -2 + -1*D + J >= 0 && -1 + D >= 0 && -21 + C + D >= 0 && 19 + -1*C + D >= 0 && -11 + B + D >= 0 && 9 + -1*B + D >= 0 && -4 + D + J >= 0 && 18 + -1*A + D >= 0 && 20 + -1*C >= 0 && 10 + B + -1*C >= 0 && 30 + -1*B + -1*C >= 0 && 17 + -1*C + J >= 0 && 39 + -1*A + -1*C >= 0 && -20 + C >= 0 && -30 + B + C >= 0 && -10 + -1*B + C >= 0 && -23 + C + J >= 0 && -1 + -1*A + C >= 0 && 10 + -1*B >= 0 && 7 + -1*B + J >= 0 && 29 + -1*A + -1*B >= 0 && -10 + B >= 0 && -13 + B + J >= 0 && 9 + -1*A + B >= 0 && -3 + J >= 0 && 16 + -1*A + J >= 0 && 19 + -1*A >= 0 && F >= 1] 11. f54(A,B,C,D,E,F,G,H,I,J,K) -> f40(A,B,C,D,E,0,G,N,I,J,K) [-1*G >= 0 (?,1) && F + -1*G >= 0 && 1 + -1*F + -1*G >= 0 && 20 + -1*E + -1*G >= 0 && -1 + D + -1*G >= 0 && -20 + C + -1*G >= 0 && 20 + -1*C + -1*G >= 0 && -10 + B + -1*G >= 0 && 10 + -1*B + -1*G >= 0 && -3 + -1*G + J >= 0 && 19 + -1*A + -1*G >= 0 && G >= 0 && F + G >= 0 && 1 + -1*F + G >= 0 && 20 + -1*E + G >= 0 && -1 + D + G >= 0 && -20 + C + G >= 0 && 20 + -1*C + G >= 0 && -10 + B + G >= 0 && 10 + -1*B + G >= 0 && -3 + G + J >= 0 && 19 + -1*A + G >= 0 && 1 + -1*F >= 0 && 21 + -1*E + -1*F >= 0 && D + -1*F >= 0 && -19 + C + -1*F >= 0 && 21 + -1*C + -1*F >= 0 && -9 + B + -1*F >= 0 && 11 + -1*B + -1*F >= 0 && -2 + -1*F + J >= 0 && 20 + -1*A + -1*F >= 0 && F >= 0 && 20 + -1*E + F >= 0 && -1 + D + F >= 0 && -20 + C + F >= 0 && 20 + -1*C + F >= 0 && -10 + B + F >= 0 && 10 + -1*B + F >= 0 && -3 + F + J >= 0 && 19 + -1*A + F >= 0 && 20 + -1*E >= 0 && 19 + D + -1*E >= 0 && C + -1*E >= 0 && 40 + -1*C + -1*E >= 0 && 10 + B + -1*E >= 0 && 30 + -1*B + -1*E >= 0 && 17 + -1*E + J >= 0 && 39 + -1*A + -1*E >= 0 && -1 + -1*A + E >= 0 && -2 + -1*D + J >= 0 && -1 + D >= 0 && -21 + C + D >= 0 && 19 + -1*C + D >= 0 && -11 + B + D >= 0 && 9 + -1*B + D >= 0 && -4 + D + J >= 0 && 18 + -1*A + D >= 0 && 20 + -1*C >= 0 && 10 + B + -1*C >= 0 && 30 + -1*B + -1*C >= 0 && 17 + -1*C + J >= 0 && 39 + -1*A + -1*C >= 0 && -20 + C >= 0 && -30 + B + C >= 0 && -10 + -1*B + C >= 0 && -23 + C + J >= 0 && -1 + -1*A + C >= 0 && 10 + -1*B >= 0 && 7 + -1*B + J >= 0 && 29 + -1*A + -1*B >= 0 && -10 + B >= 0 && -13 + B + J >= 0 && 9 + -1*A + B >= 0 && -3 + J >= 0 && 16 + -1*A + J >= 0 && 19 + -1*A >= 0 && F = 0] 12. f59(A,B,C,D,E,F,G,H,I,J,K) -> f63(A,B,C,D,E,F,G,H,I,J,K) [-1*G >= 0 (?,1) && -1 + F + -1*G >= 0 && 1 + -1*F + -1*G >= 0 && 20 + -1*E + -1*G >= 0 && -1 + D + -1*G >= 0 && -20 + C + -1*G >= 0 && 20 + -1*C + -1*G >= 0 && -10 + B + -1*G >= 0 && 10 + -1*B + -1*G >= 0 && -2 + -1*G + J >= 0 && 20 + -1*A + -1*G >= 0 && G >= 0 && -1 + F + G >= 0 && 1 + -1*F + G >= 0 && 20 + -1*E + G >= 0 && -1 + D + G >= 0 && -20 + C + G >= 0 && 20 + -1*C + G >= 0 && -10 + B + G >= 0 && 10 + -1*B + G >= 0 && -2 + G + J >= 0 && 20 + -1*A + G >= 0 && 1 + -1*F >= 0 && 21 + -1*E + -1*F >= 0 && D + -1*F >= 0 && -19 + C + -1*F >= 0 && 21 + -1*C + -1*F >= 0 && -9 + B + -1*F >= 0 && 11 + -1*B + -1*F >= 0 && -1 + -1*F + J >= 0 && 21 + -1*A + -1*F >= 0 && -1 + F >= 0 && 19 + -1*E + F >= 0 && -2 + D + F >= 0 && -21 + C + F >= 0 && 19 + -1*C + F >= 0 && -11 + B + F >= 0 && 9 + -1*B + F >= 0 && -3 + F + J >= 0 && 19 + -1*A + F >= 0 && 20 + -1*E >= 0 && 19 + D + -1*E >= 0 && C + -1*E >= 0 && 40 + -1*C + -1*E >= 0 && 10 + B + -1*E >= 0 && 30 + -1*B + -1*E >= 0 && 18 + -1*E + J >= 0 && 40 + -1*A + -1*E >= 0 && -1*A + E >= 0 && -1 + -1*D + J >= 0 && -1 + D >= 0 && -21 + C + D >= 0 && 19 + -1*C + D >= 0 && -11 + B + D >= 0 && 9 + -1*B + D >= 0 && -3 + D + J >= 0 && 19 + -1*A + D >= 0 && 20 + -1*C >= 0 && 10 + B + -1*C >= 0 && 30 + -1*B + -1*C >= 0 && 18 + -1*C + J >= 0 && 40 + -1*A + -1*C >= 0 && -20 + C >= 0 && -30 + B + C >= 0 && -10 + -1*B + C >= 0 && -22 + C + J >= 0 && -1*A + C >= 0 && 10 + -1*B >= 0 && 8 + -1*B + J >= 0 && 30 + -1*A + -1*B >= 0 && -10 + B >= 0 && -12 + B + J >= 0 && 10 + -1*A + B >= 0 && -2 + J >= 0 && 18 + -1*A + J >= 0 && 20 + -1*A >= 0 && B >= 1 + A] 13. f59(A,B,C,D,E,F,G,H,I,J,K) -> f63(A,B,C,D,-1 + A,F,G,H,I,J,K) [-1*G >= 0 (?,1) && -1 + F + -1*G >= 0 && 1 + -1*F + -1*G >= 0 && 20 + -1*E + -1*G >= 0 && -1 + D + -1*G >= 0 && -20 + C + -1*G >= 0 && 20 + -1*C + -1*G >= 0 && -10 + B + -1*G >= 0 && 10 + -1*B + -1*G >= 0 && -2 + -1*G + J >= 0 && 20 + -1*A + -1*G >= 0 && G >= 0 && -1 + F + G >= 0 && 1 + -1*F + G >= 0 && 20 + -1*E + G >= 0 && -1 + D + G >= 0 && -20 + C + G >= 0 && 20 + -1*C + G >= 0 && -10 + B + G >= 0 && 10 + -1*B + G >= 0 && -2 + G + J >= 0 && 20 + -1*A + G >= 0 && 1 + -1*F >= 0 && 21 + -1*E + -1*F >= 0 && D + -1*F >= 0 && -19 + C + -1*F >= 0 && 21 + -1*C + -1*F >= 0 && -9 + B + -1*F >= 0 && 11 + -1*B + -1*F >= 0 && -1 + -1*F + J >= 0 && 21 + -1*A + -1*F >= 0 && -1 + F >= 0 && 19 + -1*E + F >= 0 && -2 + D + F >= 0 && -21 + C + F >= 0 && 19 + -1*C + F >= 0 && -11 + B + F >= 0 && 9 + -1*B + F >= 0 && -3 + F + J >= 0 && 19 + -1*A + F >= 0 && 20 + -1*E >= 0 && 19 + D + -1*E >= 0 && C + -1*E >= 0 && 40 + -1*C + -1*E >= 0 && 10 + B + -1*E >= 0 && 30 + -1*B + -1*E >= 0 && 18 + -1*E + J >= 0 && 40 + -1*A + -1*E >= 0 && -1*A + E >= 0 && -1 + -1*D + J >= 0 && -1 + D >= 0 && -21 + C + D >= 0 && 19 + -1*C + D >= 0 && -11 + B + D >= 0 && 9 + -1*B + D >= 0 && -3 + D + J >= 0 && 19 + -1*A + D >= 0 && 20 + -1*C >= 0 && 10 + B + -1*C >= 0 && 30 + -1*B + -1*C >= 0 && 18 + -1*C + J >= 0 && 40 + -1*A + -1*C >= 0 && -20 + C >= 0 && -30 + B + C >= 0 && -10 + -1*B + C >= 0 && -22 + C + J >= 0 && -1*A + C >= 0 && 10 + -1*B >= 0 && 8 + -1*B + J >= 0 && 30 + -1*A + -1*B >= 0 && -10 + B >= 0 && -12 + B + J >= 0 && 10 + -1*A + B >= 0 && -2 + J >= 0 && 18 + -1*A + J >= 0 && 20 + -1*A >= 0 && A >= B] 14. f63(A,B,C,D,E,F,G,H,I,J,K) -> f11(A,B,C,J,E,F,G,H,I,J,K) [-1*G >= 0 (?,1) && -1 + F + -1*G >= 0 && 1 + -1*F + -1*G >= 0 && 20 + -1*E + -1*G >= 0 && -1 + D + -1*G >= 0 && -20 + C + -1*G >= 0 && 20 + -1*C + -1*G >= 0 && -10 + B + -1*G >= 0 && 10 + -1*B + -1*G >= 0 && -2 + -1*G + J >= 0 && 20 + -1*A + -1*G >= 0 && G >= 0 && -1 + F + G >= 0 && 1 + -1*F + G >= 0 && 20 + -1*E + G >= 0 && -1 + D + G >= 0 && -20 + C + G >= 0 && 20 + -1*C + G >= 0 && -10 + B + G >= 0 && 10 + -1*B + G >= 0 && -2 + G + J >= 0 && 20 + -1*A + G >= 0 && 1 + -1*F >= 0 && 21 + -1*E + -1*F >= 0 && D + -1*F >= 0 && -19 + C + -1*F >= 0 && 21 + -1*C + -1*F >= 0 && -9 + B + -1*F >= 0 && 11 + -1*B + -1*F >= 0 && -1 + -1*F + J >= 0 && 21 + -1*A + -1*F >= 0 && -1 + F >= 0 && 19 + -1*E + F >= 0 && -2 + D + F >= 0 && -21 + C + F >= 0 && 19 + -1*C + F >= 0 && -11 + B + F >= 0 && 9 + -1*B + F >= 0 && -3 + F + J >= 0 && 19 + -1*A + F >= 0 && 20 + -1*E >= 0 && 19 + D + -1*E >= 0 && C + -1*E >= 0 && 40 + -1*C + -1*E >= 0 && 10 + B + -1*E >= 0 && 30 + -1*B + -1*E >= 0 && 18 + -1*E + J >= 0 && 39 + -1*A + -1*E >= 0 && 1 + -1*A + E >= 0 && -1 + -1*D + J >= 0 && -1 + D >= 0 && -21 + C + D >= 0 && 19 + -1*C + D >= 0 && -11 + B + D >= 0 && 9 + -1*B + D >= 0 && -3 + D + J >= 0 && 19 + -1*A + D >= 0 && 20 + -1*C >= 0 && 10 + B + -1*C >= 0 && 30 + -1*B + -1*C >= 0 && 18 + -1*C + J >= 0 && 40 + -1*A + -1*C >= 0 && -20 + C >= 0 && -30 + B + C >= 0 && -10 + -1*B + C >= 0 && -22 + C + J >= 0 && -1*A + C >= 0 && 10 + -1*B >= 0 && 8 + -1*B + J >= 0 && 30 + -1*A + -1*B >= 0 && -10 + B >= 0 && -12 + B + J >= 0 && 10 + -1*A + B >= 0 && -2 + J >= 0 && 18 + -1*A + J >= 0 && 20 + -1*A >= 0 && B >= A] 15. f48(A,B,C,D,E,F,G,H,I,J,K) -> f54(A,B,C,D,E,F,G,H,I,J,K) [-1*G >= 0 (?,1) && F + -1*G >= 0 && -1*F + -1*G >= 0 && 20 + -1*E + -1*G >= 0 && -1 + D + -1*G >= 0 && -20 + C + -1*G >= 0 && 20 + -1*C + -1*G >= 0 && -10 + B + -1*G >= 0 && 10 + -1*B + -1*G >= 0 && -3 + -1*G + J >= 0 && 19 + -1*A + -1*G >= 0 && G >= 0 && F + G >= 0 && -1*F + G >= 0 && 20 + -1*E + G >= 0 && -1 + D + G >= 0 && -20 + C + G >= 0 && 20 + -1*C + G >= 0 && -10 + B + G >= 0 && 10 + -1*B + G >= 0 && -3 + G + J >= 0 && 19 + -1*A + G >= 0 && -1*F >= 0 && 20 + -1*E + -1*F >= 0 && -1 + D + -1*F >= 0 && -20 + C + -1*F >= 0 && 20 + -1*C + -1*F >= 0 && -10 + B + -1*F >= 0 && 10 + -1*B + -1*F >= 0 && -3 + -1*F + J >= 0 && 19 + -1*A + -1*F >= 0 && F >= 0 && 20 + -1*E + F >= 0 && -1 + D + F >= 0 && -20 + C + F >= 0 && 20 + -1*C + F >= 0 && -10 + B + F >= 0 && 10 + -1*B + F >= 0 && -3 + F + J >= 0 && 19 + -1*A + F >= 0 && 20 + -1*E >= 0 && 19 + D + -1*E >= 0 && C + -1*E >= 0 && 40 + -1*C + -1*E >= 0 && 10 + B + -1*E >= 0 && 30 + -1*B + -1*E >= 0 && 17 + -1*E + J >= 0 && 39 + -1*A + -1*E >= 0 && -1 + -1*A + E >= 0 && -2 + -1*D + J >= 0 && -1 + D >= 0 && -21 + C + D >= 0 && 19 + -1*C + D >= 0 && -11 + B + D >= 0 && 9 + -1*B + D >= 0 && -4 + D + J >= 0 && 18 + -1*A + D >= 0 && 20 + -1*C >= 0 && 10 + B + -1*C >= 0 && 30 + -1*B + -1*C >= 0 && 17 + -1*C + J >= 0 && 39 + -1*A + -1*C >= 0 && -20 + C >= 0 && -30 + B + C >= 0 && -10 + -1*B + C >= 0 && -23 + C + J >= 0 && -1 + -1*A + C >= 0 && 10 + -1*B >= 0 && 7 + -1*B + J >= 0 && 29 + -1*A + -1*B >= 0 && -10 + B >= 0 && -13 + B + J >= 0 && 9 + -1*A + B >= 0 && -3 + J >= 0 && 16 + -1*A + J >= 0 && 19 + -1*A >= 0 && A >= J] 16. f48(A,B,C,D,E,F,G,H,I,J,K) -> f54(A,B,C,D,E,1,G,H,I,J,K) [-1*G >= 0 (?,1) && F + -1*G >= 0 && -1*F + -1*G >= 0 && 20 + -1*E + -1*G >= 0 && -1 + D + -1*G >= 0 && -20 + C + -1*G >= 0 && 20 + -1*C + -1*G >= 0 && -10 + B + -1*G >= 0 && 10 + -1*B + -1*G >= 0 && -3 + -1*G + J >= 0 && 19 + -1*A + -1*G >= 0 && G >= 0 && F + G >= 0 && -1*F + G >= 0 && 20 + -1*E + G >= 0 && -1 + D + G >= 0 && -20 + C + G >= 0 && 20 + -1*C + G >= 0 && -10 + B + G >= 0 && 10 + -1*B + G >= 0 && -3 + G + J >= 0 && 19 + -1*A + G >= 0 && -1*F >= 0 && 20 + -1*E + -1*F >= 0 && -1 + D + -1*F >= 0 && -20 + C + -1*F >= 0 && 20 + -1*C + -1*F >= 0 && -10 + B + -1*F >= 0 && 10 + -1*B + -1*F >= 0 && -3 + -1*F + J >= 0 && 19 + -1*A + -1*F >= 0 && F >= 0 && 20 + -1*E + F >= 0 && -1 + D + F >= 0 && -20 + C + F >= 0 && 20 + -1*C + F >= 0 && -10 + B + F >= 0 && 10 + -1*B + F >= 0 && -3 + F + J >= 0 && 19 + -1*A + F >= 0 && 20 + -1*E >= 0 && 19 + D + -1*E >= 0 && C + -1*E >= 0 && 40 + -1*C + -1*E >= 0 && 10 + B + -1*E >= 0 && 30 + -1*B + -1*E >= 0 && 17 + -1*E + J >= 0 && 39 + -1*A + -1*E >= 0 && -1 + -1*A + E >= 0 && -2 + -1*D + J >= 0 && -1 + D >= 0 && -21 + C + D >= 0 && 19 + -1*C + D >= 0 && -11 + B + D >= 0 && 9 + -1*B + D >= 0 && -4 + D + J >= 0 && 18 + -1*A + D >= 0 && 20 + -1*C >= 0 && 10 + B + -1*C >= 0 && 30 + -1*B + -1*C >= 0 && 17 + -1*C + J >= 0 && 39 + -1*A + -1*C >= 0 && -20 + C >= 0 && -30 + B + C >= 0 && -10 + -1*B + C >= 0 && -23 + C + J >= 0 && -1 + -1*A + C >= 0 && 10 + -1*B >= 0 && 7 + -1*B + J >= 0 && 29 + -1*A + -1*B >= 0 && -10 + B >= 0 && -13 + B + J >= 0 && 9 + -1*A + B >= 0 && -3 + J >= 0 && 16 + -1*A + J >= 0 && 19 + -1*A >= 0 && J >= 1 + A] 17. f43(A,B,C,D,E,F,G,H,I,J,K) -> f48(-1 + A,B,C,D,E,F,G,H,I,J,K) [-1*G >= 0 (?,1) && F + -1*G >= 0 && -1*F + -1*G >= 0 && 20 + -1*E + -1*G >= 0 && -1 + D + -1*G >= 0 && -20 + C + -1*G >= 0 && 20 + -1*C + -1*G >= 0 && -10 + B + -1*G >= 0 && 10 + -1*B + -1*G >= 0 && -3 + -1*G + J >= 0 && 20 + -1*A + -1*G >= 0 && G >= 0 && F + G >= 0 && -1*F + G >= 0 && 20 + -1*E + G >= 0 && -1 + D + G >= 0 && -20 + C + G >= 0 && 20 + -1*C + G >= 0 && -10 + B + G >= 0 && 10 + -1*B + G >= 0 && -3 + G + J >= 0 && 20 + -1*A + G >= 0 && -1*F >= 0 && 20 + -1*E + -1*F >= 0 && -1 + D + -1*F >= 0 && -20 + C + -1*F >= 0 && 20 + -1*C + -1*F >= 0 && -10 + B + -1*F >= 0 && 10 + -1*B + -1*F >= 0 && -3 + -1*F + J >= 0 && 20 + -1*A + -1*F >= 0 && F >= 0 && 20 + -1*E + F >= 0 && -1 + D + F >= 0 && -20 + C + F >= 0 && 20 + -1*C + F >= 0 && -10 + B + F >= 0 && 10 + -1*B + F >= 0 && -3 + F + J >= 0 && 20 + -1*A + F >= 0 && 20 + -1*E >= 0 && 19 + D + -1*E >= 0 && C + -1*E >= 0 && 40 + -1*C + -1*E >= 0 && 10 + B + -1*E >= 0 && 30 + -1*B + -1*E >= 0 && 17 + -1*E + J >= 0 && 40 + -1*A + -1*E >= 0 && -1*A + E >= 0 && -2 + -1*D + J >= 0 && -1 + D >= 0 && -21 + C + D >= 0 && 19 + -1*C + D >= 0 && -11 + B + D >= 0 && 9 + -1*B + D >= 0 && -4 + D + J >= 0 && 19 + -1*A + D >= 0 && 20 + -1*C >= 0 && 10 + B + -1*C >= 0 && 30 + -1*B + -1*C >= 0 && 17 + -1*C + J >= 0 && 40 + -1*A + -1*C >= 0 && -20 + C >= 0 && -30 + B + C >= 0 && -10 + -1*B + C >= 0 && -23 + C + J >= 0 && -1*A + C >= 0 && 10 + -1*B >= 0 && 7 + -1*B + J >= 0 && 30 + -1*A + -1*B >= 0 && -10 + B >= 0 && -13 + B + J >= 0 && 10 + -1*A + B >= 0 && -3 + J >= 0 && 17 + -1*A + J >= 0 && 20 + -1*A >= 0] 18. f11(A,B,C,D,E,F,G,H,I,J,K) -> f69(A,B,C,D,E,F,G,H,I,J,K) [G >= 0 (?,1) && F + G >= 0 && 1 + -1*F + G >= 0 && 20 + -1*E + G >= 0 && -1 + D + G >= 0 && -20 + C + G >= 0 && 20 + -1*C + G >= 0 && -10 + B + G >= 0 && 10 + -1*B + G >= 0 && 1 + -1*F >= 0 && 21 + -1*E + -1*F >= 0 && D + -1*F >= 0 && -19 + C + -1*F >= 0 && 21 + -1*C + -1*F >= 0 && -9 + B + -1*F >= 0 && 11 + -1*B + -1*F >= 0 && F >= 0 && 20 + -1*E + F >= 0 && -1 + D + F >= 0 && -20 + C + F >= 0 && 20 + -1*C + F >= 0 && -10 + B + F >= 0 && 10 + -1*B + F >= 0 && 20 + -1*E >= 0 && 19 + D + -1*E >= 0 && C + -1*E >= 0 && 40 + -1*C + -1*E >= 0 && 10 + B + -1*E >= 0 && 30 + -1*B + -1*E >= 0 && -1 + D >= 0 && -21 + C + D >= 0 && 19 + -1*C + D >= 0 && -11 + B + D >= 0 && 9 + -1*B + D >= 0 && 20 + -1*C >= 0 && 10 + B + -1*C >= 0 && 30 + -1*B + -1*C >= 0 && -20 + C >= 0 && -30 + B + C >= 0 && -10 + -1*B + C >= 0 && 10 + -1*B >= 0 && -10 + B >= 0 && G >= 1] Signature: {(f0,11);(f11,11);(f40,11);(f43,11);(f48,11);(f54,11);(f59,11);(f63,11);(f69,11)} Flow Graph: [0->{2,3,4,5,18},1->{2,3,4,5,18},2->{2,3,4,5,18},3->{2,3,4,5,18},4->{2,3,4,5,18},5->{6,7},6->{12,13},7->{8 ,17},8->{8,17},9->{9,15,16},10->{6,7},11->{6,7},12->{0,14},13->{0,14},14->{2,3,4,5,18},15->{10,11},16->{10 ,11},17->{9,15,16},18->{}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: UnsatPaths NO + Considered Problem: Rules: 0. f63(A,B,C,D,E,F,G,H,I,J,K) -> f11(A,B,C,D,E,F,G,H,I,J,K) [-1*G >= 0 (?,1) && -1 + F + -1*G >= 0 && 1 + -1*F + -1*G >= 0 && 20 + -1*E + -1*G >= 0 && -1 + D + -1*G >= 0 && -20 + C + -1*G >= 0 && 20 + -1*C + -1*G >= 0 && -10 + B + -1*G >= 0 && 10 + -1*B + -1*G >= 0 && -2 + -1*G + J >= 0 && 20 + -1*A + -1*G >= 0 && G >= 0 && -1 + F + G >= 0 && 1 + -1*F + G >= 0 && 20 + -1*E + G >= 0 && -1 + D + G >= 0 && -20 + C + G >= 0 && 20 + -1*C + G >= 0 && -10 + B + G >= 0 && 10 + -1*B + G >= 0 && -2 + G + J >= 0 && 20 + -1*A + G >= 0 && 1 + -1*F >= 0 && 21 + -1*E + -1*F >= 0 && D + -1*F >= 0 && -19 + C + -1*F >= 0 && 21 + -1*C + -1*F >= 0 && -9 + B + -1*F >= 0 && 11 + -1*B + -1*F >= 0 && -1 + -1*F + J >= 0 && 21 + -1*A + -1*F >= 0 && -1 + F >= 0 && 19 + -1*E + F >= 0 && -2 + D + F >= 0 && -21 + C + F >= 0 && 19 + -1*C + F >= 0 && -11 + B + F >= 0 && 9 + -1*B + F >= 0 && -3 + F + J >= 0 && 19 + -1*A + F >= 0 && 20 + -1*E >= 0 && 19 + D + -1*E >= 0 && C + -1*E >= 0 && 40 + -1*C + -1*E >= 0 && 10 + B + -1*E >= 0 && 30 + -1*B + -1*E >= 0 && 18 + -1*E + J >= 0 && 39 + -1*A + -1*E >= 0 && 1 + -1*A + E >= 0 && -1 + -1*D + J >= 0 && -1 + D >= 0 && -21 + C + D >= 0 && 19 + -1*C + D >= 0 && -11 + B + D >= 0 && 9 + -1*B + D >= 0 && -3 + D + J >= 0 && 19 + -1*A + D >= 0 && 20 + -1*C >= 0 && 10 + B + -1*C >= 0 && 30 + -1*B + -1*C >= 0 && 18 + -1*C + J >= 0 && 40 + -1*A + -1*C >= 0 && -20 + C >= 0 && -30 + B + C >= 0 && -10 + -1*B + C >= 0 && -22 + C + J >= 0 && -1*A + C >= 0 && 10 + -1*B >= 0 && 8 + -1*B + J >= 0 && 30 + -1*A + -1*B >= 0 && -10 + B >= 0 && -12 + B + J >= 0 && 10 + -1*A + B >= 0 && -2 + J >= 0 && 18 + -1*A + J >= 0 && 20 + -1*A >= 0 && A >= 1 + B] 1. f0(A,B,C,D,E,F,G,H,I,J,K) -> f11(A,10,20,1,20,0,0,H,I,J,K) True (1,1) 2. f11(A,B,C,D,E,F,G,H,I,J,K) -> f11(A,B,C,D,E,F,1,H,I,J,K) [G >= 0 (?,1) && F + G >= 0 && 1 + -1*F + G >= 0 && 20 + -1*E + G >= 0 && -1 + D + G >= 0 && -20 + C + G >= 0 && 20 + -1*C + G >= 0 && -10 + B + G >= 0 && 10 + -1*B + G >= 0 && 1 + -1*F >= 0 && 21 + -1*E + -1*F >= 0 && D + -1*F >= 0 && -19 + C + -1*F >= 0 && 21 + -1*C + -1*F >= 0 && -9 + B + -1*F >= 0 && 11 + -1*B + -1*F >= 0 && F >= 0 && 20 + -1*E + F >= 0 && -1 + D + F >= 0 && -20 + C + F >= 0 && 20 + -1*C + F >= 0 && -10 + B + F >= 0 && 10 + -1*B + F >= 0 && 20 + -1*E >= 0 && 19 + D + -1*E >= 0 && C + -1*E >= 0 && 40 + -1*C + -1*E >= 0 && 10 + B + -1*E >= 0 && 30 + -1*B + -1*E >= 0 && -1 + D >= 0 && -21 + C + D >= 0 && 19 + -1*C + D >= 0 && -11 + B + D >= 0 && 9 + -1*B + D >= 0 && 20 + -1*C >= 0 && 10 + B + -1*C >= 0 && 30 + -1*B + -1*C >= 0 && -20 + C >= 0 && -30 + B + C >= 0 && -10 + -1*B + C >= 0 && 10 + -1*B >= 0 && -10 + B >= 0 && D >= E && G = 0] 3. f11(A,B,C,D,E,F,G,H,I,J,K) -> f11(A,B,C,D,1 + D,F,1,H,I,J,K) [G >= 0 (?,1) && F + G >= 0 && 1 + -1*F + G >= 0 && 20 + -1*E + G >= 0 && -1 + D + G >= 0 && -20 + C + G >= 0 && 20 + -1*C + G >= 0 && -10 + B + G >= 0 && 10 + -1*B + G >= 0 && 1 + -1*F >= 0 && 21 + -1*E + -1*F >= 0 && D + -1*F >= 0 && -19 + C + -1*F >= 0 && 21 + -1*C + -1*F >= 0 && -9 + B + -1*F >= 0 && 11 + -1*B + -1*F >= 0 && F >= 0 && 20 + -1*E + F >= 0 && -1 + D + F >= 0 && -20 + C + F >= 0 && 20 + -1*C + F >= 0 && -10 + B + F >= 0 && 10 + -1*B + F >= 0 && 20 + -1*E >= 0 && 19 + D + -1*E >= 0 && C + -1*E >= 0 && 40 + -1*C + -1*E >= 0 && 10 + B + -1*E >= 0 && 30 + -1*B + -1*E >= 0 && -1 + D >= 0 && -21 + C + D >= 0 && 19 + -1*C + D >= 0 && -11 + B + D >= 0 && 9 + -1*B + D >= 0 && 20 + -1*C >= 0 && 10 + B + -1*C >= 0 && 30 + -1*B + -1*C >= 0 && -20 + C >= 0 && -30 + B + C >= 0 && -10 + -1*B + C >= 0 && 10 + -1*B >= 0 && -10 + B >= 0 && E = 1 + D && G = 0] 4. f11(A,B,C,D,E,F,G,H,I,J,K) -> f11(A,B,C,D,1 + D,F,1,N,I,J,K) [G >= 0 (?,1) && F + G >= 0 && 1 + -1*F + G >= 0 && 20 + -1*E + G >= 0 && -1 + D + G >= 0 && -20 + C + G >= 0 && 20 + -1*C + G >= 0 && -10 + B + G >= 0 && 10 + -1*B + G >= 0 && 1 + -1*F >= 0 && 21 + -1*E + -1*F >= 0 && D + -1*F >= 0 && -19 + C + -1*F >= 0 && 21 + -1*C + -1*F >= 0 && -9 + B + -1*F >= 0 && 11 + -1*B + -1*F >= 0 && F >= 0 && 20 + -1*E + F >= 0 && -1 + D + F >= 0 && -20 + C + F >= 0 && 20 + -1*C + F >= 0 && -10 + B + F >= 0 && 10 + -1*B + F >= 0 && 20 + -1*E >= 0 && 19 + D + -1*E >= 0 && C + -1*E >= 0 && 40 + -1*C + -1*E >= 0 && 10 + B + -1*E >= 0 && 30 + -1*B + -1*E >= 0 && -1 + D >= 0 && -21 + C + D >= 0 && 19 + -1*C + D >= 0 && -11 + B + D >= 0 && 9 + -1*B + D >= 0 && 20 + -1*C >= 0 && 10 + B + -1*C >= 0 && 30 + -1*B + -1*C >= 0 && -20 + C >= 0 && -30 + B + C >= 0 && -10 + -1*B + C >= 0 && 10 + -1*B >= 0 && -10 + B >= 0 && L >= 1 + M && E = 1 + D && G = 0] 5. f11(A,B,C,D,E,F,G,H,I,J,K) -> f40(E,B,C,D,E,F,0,N,L,1 + D,M) [G >= 0 (?,1) && F + G >= 0 && 1 + -1*F + G >= 0 && 20 + -1*E + G >= 0 && -1 + D + G >= 0 && -20 + C + G >= 0 && 20 + -1*C + G >= 0 && -10 + B + G >= 0 && 10 + -1*B + G >= 0 && 1 + -1*F >= 0 && 21 + -1*E + -1*F >= 0 && D + -1*F >= 0 && -19 + C + -1*F >= 0 && 21 + -1*C + -1*F >= 0 && -9 + B + -1*F >= 0 && 11 + -1*B + -1*F >= 0 && F >= 0 && 20 + -1*E + F >= 0 && -1 + D + F >= 0 && -20 + C + F >= 0 && 20 + -1*C + F >= 0 && -10 + B + F >= 0 && 10 + -1*B + F >= 0 && 20 + -1*E >= 0 && 19 + D + -1*E >= 0 && C + -1*E >= 0 && 40 + -1*C + -1*E >= 0 && 10 + B + -1*E >= 0 && 30 + -1*B + -1*E >= 0 && -1 + D >= 0 && -21 + C + D >= 0 && 19 + -1*C + D >= 0 && -11 + B + D >= 0 && 9 + -1*B + D >= 0 && 20 + -1*C >= 0 && 10 + B + -1*C >= 0 && 30 + -1*B + -1*C >= 0 && -20 + C >= 0 && -30 + B + C >= 0 && -10 + -1*B + C >= 0 && 10 + -1*B >= 0 && -10 + B >= 0 && E >= 2 + D && G = 0] 6. f40(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,H,I,J,K) [-1*G >= 0 (?,1) && F + -1*G >= 0 && 1 + -1*F + -1*G >= 0 && 20 + -1*E + -1*G >= 0 && -1 + D + -1*G >= 0 && -20 + C + -1*G >= 0 && 20 + -1*C + -1*G >= 0 && -10 + B + -1*G >= 0 && 10 + -1*B + -1*G >= 0 && -2 + -1*G + J >= 0 && 20 + -1*A + -1*G >= 0 && G >= 0 && F + G >= 0 && 1 + -1*F + G >= 0 && 20 + -1*E + G >= 0 && -1 + D + G >= 0 && -20 + C + G >= 0 && 20 + -1*C + G >= 0 && -10 + B + G >= 0 && 10 + -1*B + G >= 0 && -2 + G + J >= 0 && 20 + -1*A + G >= 0 && 1 + -1*F >= 0 && 21 + -1*E + -1*F >= 0 && D + -1*F >= 0 && -19 + C + -1*F >= 0 && 21 + -1*C + -1*F >= 0 && -9 + B + -1*F >= 0 && 11 + -1*B + -1*F >= 0 && -1 + -1*F + J >= 0 && 21 + -1*A + -1*F >= 0 && F >= 0 && 20 + -1*E + F >= 0 && -1 + D + F >= 0 && -20 + C + F >= 0 && 20 + -1*C + F >= 0 && -10 + B + F >= 0 && 10 + -1*B + F >= 0 && -2 + F + J >= 0 && 20 + -1*A + F >= 0 && 20 + -1*E >= 0 && 19 + D + -1*E >= 0 && C + -1*E >= 0 && 40 + -1*C + -1*E >= 0 && 10 + B + -1*E >= 0 && 30 + -1*B + -1*E >= 0 && 18 + -1*E + J >= 0 && 40 + -1*A + -1*E >= 0 && -1*A + E >= 0 && -1 + -1*D + J >= 0 && -1 + D >= 0 && -21 + C + D >= 0 && 19 + -1*C + D >= 0 && -11 + B + D >= 0 && 9 + -1*B + D >= 0 && -3 + D + J >= 0 && 19 + -1*A + D >= 0 && 20 + -1*C >= 0 && 10 + B + -1*C >= 0 && 30 + -1*B + -1*C >= 0 && 18 + -1*C + J >= 0 && 40 + -1*A + -1*C >= 0 && -20 + C >= 0 && -30 + B + C >= 0 && -10 + -1*B + C >= 0 && -22 + C + J >= 0 && -1*A + C >= 0 && 10 + -1*B >= 0 && 8 + -1*B + J >= 0 && 30 + -1*A + -1*B >= 0 && -10 + B >= 0 && -12 + B + J >= 0 && 10 + -1*A + B >= 0 && -2 + J >= 0 && 18 + -1*A + J >= 0 && 20 + -1*A >= 0 && F >= 1] 7. f40(A,B,C,D,E,F,G,H,I,J,K) -> f43(A,B,C,D,E,0,G,H,I,1 + J,K) [-1*G >= 0 (?,1) && F + -1*G >= 0 && 1 + -1*F + -1*G >= 0 && 20 + -1*E + -1*G >= 0 && -1 + D + -1*G >= 0 && -20 + C + -1*G >= 0 && 20 + -1*C + -1*G >= 0 && -10 + B + -1*G >= 0 && 10 + -1*B + -1*G >= 0 && -2 + -1*G + J >= 0 && 20 + -1*A + -1*G >= 0 && G >= 0 && F + G >= 0 && 1 + -1*F + G >= 0 && 20 + -1*E + G >= 0 && -1 + D + G >= 0 && -20 + C + G >= 0 && 20 + -1*C + G >= 0 && -10 + B + G >= 0 && 10 + -1*B + G >= 0 && -2 + G + J >= 0 && 20 + -1*A + G >= 0 && 1 + -1*F >= 0 && 21 + -1*E + -1*F >= 0 && D + -1*F >= 0 && -19 + C + -1*F >= 0 && 21 + -1*C + -1*F >= 0 && -9 + B + -1*F >= 0 && 11 + -1*B + -1*F >= 0 && -1 + -1*F + J >= 0 && 21 + -1*A + -1*F >= 0 && F >= 0 && 20 + -1*E + F >= 0 && -1 + D + F >= 0 && -20 + C + F >= 0 && 20 + -1*C + F >= 0 && -10 + B + F >= 0 && 10 + -1*B + F >= 0 && -2 + F + J >= 0 && 20 + -1*A + F >= 0 && 20 + -1*E >= 0 && 19 + D + -1*E >= 0 && C + -1*E >= 0 && 40 + -1*C + -1*E >= 0 && 10 + B + -1*E >= 0 && 30 + -1*B + -1*E >= 0 && 18 + -1*E + J >= 0 && 40 + -1*A + -1*E >= 0 && -1*A + E >= 0 && -1 + -1*D + J >= 0 && -1 + D >= 0 && -21 + C + D >= 0 && 19 + -1*C + D >= 0 && -11 + B + D >= 0 && 9 + -1*B + D >= 0 && -3 + D + J >= 0 && 19 + -1*A + D >= 0 && 20 + -1*C >= 0 && 10 + B + -1*C >= 0 && 30 + -1*B + -1*C >= 0 && 18 + -1*C + J >= 0 && 40 + -1*A + -1*C >= 0 && -20 + C >= 0 && -30 + B + C >= 0 && -10 + -1*B + C >= 0 && -22 + C + J >= 0 && -1*A + C >= 0 && 10 + -1*B >= 0 && 8 + -1*B + J >= 0 && 30 + -1*A + -1*B >= 0 && -10 + B >= 0 && -12 + B + J >= 0 && 10 + -1*A + B >= 0 && -2 + J >= 0 && 18 + -1*A + J >= 0 && 20 + -1*A >= 0 && F = 0] 8. f43(A,B,C,D,E,F,G,H,I,J,K) -> f43(A,B,C,D,E,F,G,H,I,1 + J,K) [-1*G >= 0 (?,1) && F + -1*G >= 0 && -1*F + -1*G >= 0 && 20 + -1*E + -1*G >= 0 && -1 + D + -1*G >= 0 && -20 + C + -1*G >= 0 && 20 + -1*C + -1*G >= 0 && -10 + B + -1*G >= 0 && 10 + -1*B + -1*G >= 0 && -3 + -1*G + J >= 0 && 20 + -1*A + -1*G >= 0 && G >= 0 && F + G >= 0 && -1*F + G >= 0 && 20 + -1*E + G >= 0 && -1 + D + G >= 0 && -20 + C + G >= 0 && 20 + -1*C + G >= 0 && -10 + B + G >= 0 && 10 + -1*B + G >= 0 && -3 + G + J >= 0 && 20 + -1*A + G >= 0 && -1*F >= 0 && 20 + -1*E + -1*F >= 0 && -1 + D + -1*F >= 0 && -20 + C + -1*F >= 0 && 20 + -1*C + -1*F >= 0 && -10 + B + -1*F >= 0 && 10 + -1*B + -1*F >= 0 && -3 + -1*F + J >= 0 && 20 + -1*A + -1*F >= 0 && F >= 0 && 20 + -1*E + F >= 0 && -1 + D + F >= 0 && -20 + C + F >= 0 && 20 + -1*C + F >= 0 && -10 + B + F >= 0 && 10 + -1*B + F >= 0 && -3 + F + J >= 0 && 20 + -1*A + F >= 0 && 20 + -1*E >= 0 && 19 + D + -1*E >= 0 && C + -1*E >= 0 && 40 + -1*C + -1*E >= 0 && 10 + B + -1*E >= 0 && 30 + -1*B + -1*E >= 0 && 17 + -1*E + J >= 0 && 40 + -1*A + -1*E >= 0 && -1*A + E >= 0 && -2 + -1*D + J >= 0 && -1 + D >= 0 && -21 + C + D >= 0 && 19 + -1*C + D >= 0 && -11 + B + D >= 0 && 9 + -1*B + D >= 0 && -4 + D + J >= 0 && 19 + -1*A + D >= 0 && 20 + -1*C >= 0 && 10 + B + -1*C >= 0 && 30 + -1*B + -1*C >= 0 && 17 + -1*C + J >= 0 && 40 + -1*A + -1*C >= 0 && -20 + C >= 0 && -30 + B + C >= 0 && -10 + -1*B + C >= 0 && -23 + C + J >= 0 && -1*A + C >= 0 && 10 + -1*B >= 0 && 7 + -1*B + J >= 0 && 30 + -1*A + -1*B >= 0 && -10 + B >= 0 && -13 + B + J >= 0 && 10 + -1*A + B >= 0 && -3 + J >= 0 && 17 + -1*A + J >= 0 && 20 + -1*A >= 0 && K >= 1 + N] 9. f48(A,B,C,D,E,F,G,H,I,J,K) -> f48(-1 + A,B,C,D,E,F,G,H,I,J,K) [-1*G >= 0 (?,1) && F + -1*G >= 0 && -1*F + -1*G >= 0 && 20 + -1*E + -1*G >= 0 && -1 + D + -1*G >= 0 && -20 + C + -1*G >= 0 && 20 + -1*C + -1*G >= 0 && -10 + B + -1*G >= 0 && 10 + -1*B + -1*G >= 0 && -3 + -1*G + J >= 0 && 19 + -1*A + -1*G >= 0 && G >= 0 && F + G >= 0 && -1*F + G >= 0 && 20 + -1*E + G >= 0 && -1 + D + G >= 0 && -20 + C + G >= 0 && 20 + -1*C + G >= 0 && -10 + B + G >= 0 && 10 + -1*B + G >= 0 && -3 + G + J >= 0 && 19 + -1*A + G >= 0 && -1*F >= 0 && 20 + -1*E + -1*F >= 0 && -1 + D + -1*F >= 0 && -20 + C + -1*F >= 0 && 20 + -1*C + -1*F >= 0 && -10 + B + -1*F >= 0 && 10 + -1*B + -1*F >= 0 && -3 + -1*F + J >= 0 && 19 + -1*A + -1*F >= 0 && F >= 0 && 20 + -1*E + F >= 0 && -1 + D + F >= 0 && -20 + C + F >= 0 && 20 + -1*C + F >= 0 && -10 + B + F >= 0 && 10 + -1*B + F >= 0 && -3 + F + J >= 0 && 19 + -1*A + F >= 0 && 20 + -1*E >= 0 && 19 + D + -1*E >= 0 && C + -1*E >= 0 && 40 + -1*C + -1*E >= 0 && 10 + B + -1*E >= 0 && 30 + -1*B + -1*E >= 0 && 17 + -1*E + J >= 0 && 39 + -1*A + -1*E >= 0 && -1 + -1*A + E >= 0 && -2 + -1*D + J >= 0 && -1 + D >= 0 && -21 + C + D >= 0 && 19 + -1*C + D >= 0 && -11 + B + D >= 0 && 9 + -1*B + D >= 0 && -4 + D + J >= 0 && 18 + -1*A + D >= 0 && 20 + -1*C >= 0 && 10 + B + -1*C >= 0 && 30 + -1*B + -1*C >= 0 && 17 + -1*C + J >= 0 && 39 + -1*A + -1*C >= 0 && -20 + C >= 0 && -30 + B + C >= 0 && -10 + -1*B + C >= 0 && -23 + C + J >= 0 && -1 + -1*A + C >= 0 && 10 + -1*B >= 0 && 7 + -1*B + J >= 0 && 29 + -1*A + -1*B >= 0 && -10 + B >= 0 && -13 + B + J >= 0 && 9 + -1*A + B >= 0 && -3 + J >= 0 && 16 + -1*A + J >= 0 && 19 + -1*A >= 0] 10. f54(A,B,C,D,E,F,G,H,I,J,K) -> f40(A,B,C,D,E,F,G,H,I,J,K) [-1*G >= 0 (?,1) && F + -1*G >= 0 && 1 + -1*F + -1*G >= 0 && 20 + -1*E + -1*G >= 0 && -1 + D + -1*G >= 0 && -20 + C + -1*G >= 0 && 20 + -1*C + -1*G >= 0 && -10 + B + -1*G >= 0 && 10 + -1*B + -1*G >= 0 && -3 + -1*G + J >= 0 && 19 + -1*A + -1*G >= 0 && G >= 0 && F + G >= 0 && 1 + -1*F + G >= 0 && 20 + -1*E + G >= 0 && -1 + D + G >= 0 && -20 + C + G >= 0 && 20 + -1*C + G >= 0 && -10 + B + G >= 0 && 10 + -1*B + G >= 0 && -3 + G + J >= 0 && 19 + -1*A + G >= 0 && 1 + -1*F >= 0 && 21 + -1*E + -1*F >= 0 && D + -1*F >= 0 && -19 + C + -1*F >= 0 && 21 + -1*C + -1*F >= 0 && -9 + B + -1*F >= 0 && 11 + -1*B + -1*F >= 0 && -2 + -1*F + J >= 0 && 20 + -1*A + -1*F >= 0 && F >= 0 && 20 + -1*E + F >= 0 && -1 + D + F >= 0 && -20 + C + F >= 0 && 20 + -1*C + F >= 0 && -10 + B + F >= 0 && 10 + -1*B + F >= 0 && -3 + F + J >= 0 && 19 + -1*A + F >= 0 && 20 + -1*E >= 0 && 19 + D + -1*E >= 0 && C + -1*E >= 0 && 40 + -1*C + -1*E >= 0 && 10 + B + -1*E >= 0 && 30 + -1*B + -1*E >= 0 && 17 + -1*E + J >= 0 && 39 + -1*A + -1*E >= 0 && -1 + -1*A + E >= 0 && -2 + -1*D + J >= 0 && -1 + D >= 0 && -21 + C + D >= 0 && 19 + -1*C + D >= 0 && -11 + B + D >= 0 && 9 + -1*B + D >= 0 && -4 + D + J >= 0 && 18 + -1*A + D >= 0 && 20 + -1*C >= 0 && 10 + B + -1*C >= 0 && 30 + -1*B + -1*C >= 0 && 17 + -1*C + J >= 0 && 39 + -1*A + -1*C >= 0 && -20 + C >= 0 && -30 + B + C >= 0 && -10 + -1*B + C >= 0 && -23 + C + J >= 0 && -1 + -1*A + C >= 0 && 10 + -1*B >= 0 && 7 + -1*B + J >= 0 && 29 + -1*A + -1*B >= 0 && -10 + B >= 0 && -13 + B + J >= 0 && 9 + -1*A + B >= 0 && -3 + J >= 0 && 16 + -1*A + J >= 0 && 19 + -1*A >= 0 && F >= 1] 11. f54(A,B,C,D,E,F,G,H,I,J,K) -> f40(A,B,C,D,E,0,G,N,I,J,K) [-1*G >= 0 (?,1) && F + -1*G >= 0 && 1 + -1*F + -1*G >= 0 && 20 + -1*E + -1*G >= 0 && -1 + D + -1*G >= 0 && -20 + C + -1*G >= 0 && 20 + -1*C + -1*G >= 0 && -10 + B + -1*G >= 0 && 10 + -1*B + -1*G >= 0 && -3 + -1*G + J >= 0 && 19 + -1*A + -1*G >= 0 && G >= 0 && F + G >= 0 && 1 + -1*F + G >= 0 && 20 + -1*E + G >= 0 && -1 + D + G >= 0 && -20 + C + G >= 0 && 20 + -1*C + G >= 0 && -10 + B + G >= 0 && 10 + -1*B + G >= 0 && -3 + G + J >= 0 && 19 + -1*A + G >= 0 && 1 + -1*F >= 0 && 21 + -1*E + -1*F >= 0 && D + -1*F >= 0 && -19 + C + -1*F >= 0 && 21 + -1*C + -1*F >= 0 && -9 + B + -1*F >= 0 && 11 + -1*B + -1*F >= 0 && -2 + -1*F + J >= 0 && 20 + -1*A + -1*F >= 0 && F >= 0 && 20 + -1*E + F >= 0 && -1 + D + F >= 0 && -20 + C + F >= 0 && 20 + -1*C + F >= 0 && -10 + B + F >= 0 && 10 + -1*B + F >= 0 && -3 + F + J >= 0 && 19 + -1*A + F >= 0 && 20 + -1*E >= 0 && 19 + D + -1*E >= 0 && C + -1*E >= 0 && 40 + -1*C + -1*E >= 0 && 10 + B + -1*E >= 0 && 30 + -1*B + -1*E >= 0 && 17 + -1*E + J >= 0 && 39 + -1*A + -1*E >= 0 && -1 + -1*A + E >= 0 && -2 + -1*D + J >= 0 && -1 + D >= 0 && -21 + C + D >= 0 && 19 + -1*C + D >= 0 && -11 + B + D >= 0 && 9 + -1*B + D >= 0 && -4 + D + J >= 0 && 18 + -1*A + D >= 0 && 20 + -1*C >= 0 && 10 + B + -1*C >= 0 && 30 + -1*B + -1*C >= 0 && 17 + -1*C + J >= 0 && 39 + -1*A + -1*C >= 0 && -20 + C >= 0 && -30 + B + C >= 0 && -10 + -1*B + C >= 0 && -23 + C + J >= 0 && -1 + -1*A + C >= 0 && 10 + -1*B >= 0 && 7 + -1*B + J >= 0 && 29 + -1*A + -1*B >= 0 && -10 + B >= 0 && -13 + B + J >= 0 && 9 + -1*A + B >= 0 && -3 + J >= 0 && 16 + -1*A + J >= 0 && 19 + -1*A >= 0 && F = 0] 12. f59(A,B,C,D,E,F,G,H,I,J,K) -> f63(A,B,C,D,E,F,G,H,I,J,K) [-1*G >= 0 (?,1) && -1 + F + -1*G >= 0 && 1 + -1*F + -1*G >= 0 && 20 + -1*E + -1*G >= 0 && -1 + D + -1*G >= 0 && -20 + C + -1*G >= 0 && 20 + -1*C + -1*G >= 0 && -10 + B + -1*G >= 0 && 10 + -1*B + -1*G >= 0 && -2 + -1*G + J >= 0 && 20 + -1*A + -1*G >= 0 && G >= 0 && -1 + F + G >= 0 && 1 + -1*F + G >= 0 && 20 + -1*E + G >= 0 && -1 + D + G >= 0 && -20 + C + G >= 0 && 20 + -1*C + G >= 0 && -10 + B + G >= 0 && 10 + -1*B + G >= 0 && -2 + G + J >= 0 && 20 + -1*A + G >= 0 && 1 + -1*F >= 0 && 21 + -1*E + -1*F >= 0 && D + -1*F >= 0 && -19 + C + -1*F >= 0 && 21 + -1*C + -1*F >= 0 && -9 + B + -1*F >= 0 && 11 + -1*B + -1*F >= 0 && -1 + -1*F + J >= 0 && 21 + -1*A + -1*F >= 0 && -1 + F >= 0 && 19 + -1*E + F >= 0 && -2 + D + F >= 0 && -21 + C + F >= 0 && 19 + -1*C + F >= 0 && -11 + B + F >= 0 && 9 + -1*B + F >= 0 && -3 + F + J >= 0 && 19 + -1*A + F >= 0 && 20 + -1*E >= 0 && 19 + D + -1*E >= 0 && C + -1*E >= 0 && 40 + -1*C + -1*E >= 0 && 10 + B + -1*E >= 0 && 30 + -1*B + -1*E >= 0 && 18 + -1*E + J >= 0 && 40 + -1*A + -1*E >= 0 && -1*A + E >= 0 && -1 + -1*D + J >= 0 && -1 + D >= 0 && -21 + C + D >= 0 && 19 + -1*C + D >= 0 && -11 + B + D >= 0 && 9 + -1*B + D >= 0 && -3 + D + J >= 0 && 19 + -1*A + D >= 0 && 20 + -1*C >= 0 && 10 + B + -1*C >= 0 && 30 + -1*B + -1*C >= 0 && 18 + -1*C + J >= 0 && 40 + -1*A + -1*C >= 0 && -20 + C >= 0 && -30 + B + C >= 0 && -10 + -1*B + C >= 0 && -22 + C + J >= 0 && -1*A + C >= 0 && 10 + -1*B >= 0 && 8 + -1*B + J >= 0 && 30 + -1*A + -1*B >= 0 && -10 + B >= 0 && -12 + B + J >= 0 && 10 + -1*A + B >= 0 && -2 + J >= 0 && 18 + -1*A + J >= 0 && 20 + -1*A >= 0 && B >= 1 + A] 13. f59(A,B,C,D,E,F,G,H,I,J,K) -> f63(A,B,C,D,-1 + A,F,G,H,I,J,K) [-1*G >= 0 (?,1) && -1 + F + -1*G >= 0 && 1 + -1*F + -1*G >= 0 && 20 + -1*E + -1*G >= 0 && -1 + D + -1*G >= 0 && -20 + C + -1*G >= 0 && 20 + -1*C + -1*G >= 0 && -10 + B + -1*G >= 0 && 10 + -1*B + -1*G >= 0 && -2 + -1*G + J >= 0 && 20 + -1*A + -1*G >= 0 && G >= 0 && -1 + F + G >= 0 && 1 + -1*F + G >= 0 && 20 + -1*E + G >= 0 && -1 + D + G >= 0 && -20 + C + G >= 0 && 20 + -1*C + G >= 0 && -10 + B + G >= 0 && 10 + -1*B + G >= 0 && -2 + G + J >= 0 && 20 + -1*A + G >= 0 && 1 + -1*F >= 0 && 21 + -1*E + -1*F >= 0 && D + -1*F >= 0 && -19 + C + -1*F >= 0 && 21 + -1*C + -1*F >= 0 && -9 + B + -1*F >= 0 && 11 + -1*B + -1*F >= 0 && -1 + -1*F + J >= 0 && 21 + -1*A + -1*F >= 0 && -1 + F >= 0 && 19 + -1*E + F >= 0 && -2 + D + F >= 0 && -21 + C + F >= 0 && 19 + -1*C + F >= 0 && -11 + B + F >= 0 && 9 + -1*B + F >= 0 && -3 + F + J >= 0 && 19 + -1*A + F >= 0 && 20 + -1*E >= 0 && 19 + D + -1*E >= 0 && C + -1*E >= 0 && 40 + -1*C + -1*E >= 0 && 10 + B + -1*E >= 0 && 30 + -1*B + -1*E >= 0 && 18 + -1*E + J >= 0 && 40 + -1*A + -1*E >= 0 && -1*A + E >= 0 && -1 + -1*D + J >= 0 && -1 + D >= 0 && -21 + C + D >= 0 && 19 + -1*C + D >= 0 && -11 + B + D >= 0 && 9 + -1*B + D >= 0 && -3 + D + J >= 0 && 19 + -1*A + D >= 0 && 20 + -1*C >= 0 && 10 + B + -1*C >= 0 && 30 + -1*B + -1*C >= 0 && 18 + -1*C + J >= 0 && 40 + -1*A + -1*C >= 0 && -20 + C >= 0 && -30 + B + C >= 0 && -10 + -1*B + C >= 0 && -22 + C + J >= 0 && -1*A + C >= 0 && 10 + -1*B >= 0 && 8 + -1*B + J >= 0 && 30 + -1*A + -1*B >= 0 && -10 + B >= 0 && -12 + B + J >= 0 && 10 + -1*A + B >= 0 && -2 + J >= 0 && 18 + -1*A + J >= 0 && 20 + -1*A >= 0 && A >= B] 14. f63(A,B,C,D,E,F,G,H,I,J,K) -> f11(A,B,C,J,E,F,G,H,I,J,K) [-1*G >= 0 (?,1) && -1 + F + -1*G >= 0 && 1 + -1*F + -1*G >= 0 && 20 + -1*E + -1*G >= 0 && -1 + D + -1*G >= 0 && -20 + C + -1*G >= 0 && 20 + -1*C + -1*G >= 0 && -10 + B + -1*G >= 0 && 10 + -1*B + -1*G >= 0 && -2 + -1*G + J >= 0 && 20 + -1*A + -1*G >= 0 && G >= 0 && -1 + F + G >= 0 && 1 + -1*F + G >= 0 && 20 + -1*E + G >= 0 && -1 + D + G >= 0 && -20 + C + G >= 0 && 20 + -1*C + G >= 0 && -10 + B + G >= 0 && 10 + -1*B + G >= 0 && -2 + G + J >= 0 && 20 + -1*A + G >= 0 && 1 + -1*F >= 0 && 21 + -1*E + -1*F >= 0 && D + -1*F >= 0 && -19 + C + -1*F >= 0 && 21 + -1*C + -1*F >= 0 && -9 + B + -1*F >= 0 && 11 + -1*B + -1*F >= 0 && -1 + -1*F + J >= 0 && 21 + -1*A + -1*F >= 0 && -1 + F >= 0 && 19 + -1*E + F >= 0 && -2 + D + F >= 0 && -21 + C + F >= 0 && 19 + -1*C + F >= 0 && -11 + B + F >= 0 && 9 + -1*B + F >= 0 && -3 + F + J >= 0 && 19 + -1*A + F >= 0 && 20 + -1*E >= 0 && 19 + D + -1*E >= 0 && C + -1*E >= 0 && 40 + -1*C + -1*E >= 0 && 10 + B + -1*E >= 0 && 30 + -1*B + -1*E >= 0 && 18 + -1*E + J >= 0 && 39 + -1*A + -1*E >= 0 && 1 + -1*A + E >= 0 && -1 + -1*D + J >= 0 && -1 + D >= 0 && -21 + C + D >= 0 && 19 + -1*C + D >= 0 && -11 + B + D >= 0 && 9 + -1*B + D >= 0 && -3 + D + J >= 0 && 19 + -1*A + D >= 0 && 20 + -1*C >= 0 && 10 + B + -1*C >= 0 && 30 + -1*B + -1*C >= 0 && 18 + -1*C + J >= 0 && 40 + -1*A + -1*C >= 0 && -20 + C >= 0 && -30 + B + C >= 0 && -10 + -1*B + C >= 0 && -22 + C + J >= 0 && -1*A + C >= 0 && 10 + -1*B >= 0 && 8 + -1*B + J >= 0 && 30 + -1*A + -1*B >= 0 && -10 + B >= 0 && -12 + B + J >= 0 && 10 + -1*A + B >= 0 && -2 + J >= 0 && 18 + -1*A + J >= 0 && 20 + -1*A >= 0 && B >= A] 15. f48(A,B,C,D,E,F,G,H,I,J,K) -> f54(A,B,C,D,E,F,G,H,I,J,K) [-1*G >= 0 (?,1) && F + -1*G >= 0 && -1*F + -1*G >= 0 && 20 + -1*E + -1*G >= 0 && -1 + D + -1*G >= 0 && -20 + C + -1*G >= 0 && 20 + -1*C + -1*G >= 0 && -10 + B + -1*G >= 0 && 10 + -1*B + -1*G >= 0 && -3 + -1*G + J >= 0 && 19 + -1*A + -1*G >= 0 && G >= 0 && F + G >= 0 && -1*F + G >= 0 && 20 + -1*E + G >= 0 && -1 + D + G >= 0 && -20 + C + G >= 0 && 20 + -1*C + G >= 0 && -10 + B + G >= 0 && 10 + -1*B + G >= 0 && -3 + G + J >= 0 && 19 + -1*A + G >= 0 && -1*F >= 0 && 20 + -1*E + -1*F >= 0 && -1 + D + -1*F >= 0 && -20 + C + -1*F >= 0 && 20 + -1*C + -1*F >= 0 && -10 + B + -1*F >= 0 && 10 + -1*B + -1*F >= 0 && -3 + -1*F + J >= 0 && 19 + -1*A + -1*F >= 0 && F >= 0 && 20 + -1*E + F >= 0 && -1 + D + F >= 0 && -20 + C + F >= 0 && 20 + -1*C + F >= 0 && -10 + B + F >= 0 && 10 + -1*B + F >= 0 && -3 + F + J >= 0 && 19 + -1*A + F >= 0 && 20 + -1*E >= 0 && 19 + D + -1*E >= 0 && C + -1*E >= 0 && 40 + -1*C + -1*E >= 0 && 10 + B + -1*E >= 0 && 30 + -1*B + -1*E >= 0 && 17 + -1*E + J >= 0 && 39 + -1*A + -1*E >= 0 && -1 + -1*A + E >= 0 && -2 + -1*D + J >= 0 && -1 + D >= 0 && -21 + C + D >= 0 && 19 + -1*C + D >= 0 && -11 + B + D >= 0 && 9 + -1*B + D >= 0 && -4 + D + J >= 0 && 18 + -1*A + D >= 0 && 20 + -1*C >= 0 && 10 + B + -1*C >= 0 && 30 + -1*B + -1*C >= 0 && 17 + -1*C + J >= 0 && 39 + -1*A + -1*C >= 0 && -20 + C >= 0 && -30 + B + C >= 0 && -10 + -1*B + C >= 0 && -23 + C + J >= 0 && -1 + -1*A + C >= 0 && 10 + -1*B >= 0 && 7 + -1*B + J >= 0 && 29 + -1*A + -1*B >= 0 && -10 + B >= 0 && -13 + B + J >= 0 && 9 + -1*A + B >= 0 && -3 + J >= 0 && 16 + -1*A + J >= 0 && 19 + -1*A >= 0 && A >= J] 16. f48(A,B,C,D,E,F,G,H,I,J,K) -> f54(A,B,C,D,E,1,G,H,I,J,K) [-1*G >= 0 (?,1) && F + -1*G >= 0 && -1*F + -1*G >= 0 && 20 + -1*E + -1*G >= 0 && -1 + D + -1*G >= 0 && -20 + C + -1*G >= 0 && 20 + -1*C + -1*G >= 0 && -10 + B + -1*G >= 0 && 10 + -1*B + -1*G >= 0 && -3 + -1*G + J >= 0 && 19 + -1*A + -1*G >= 0 && G >= 0 && F + G >= 0 && -1*F + G >= 0 && 20 + -1*E + G >= 0 && -1 + D + G >= 0 && -20 + C + G >= 0 && 20 + -1*C + G >= 0 && -10 + B + G >= 0 && 10 + -1*B + G >= 0 && -3 + G + J >= 0 && 19 + -1*A + G >= 0 && -1*F >= 0 && 20 + -1*E + -1*F >= 0 && -1 + D + -1*F >= 0 && -20 + C + -1*F >= 0 && 20 + -1*C + -1*F >= 0 && -10 + B + -1*F >= 0 && 10 + -1*B + -1*F >= 0 && -3 + -1*F + J >= 0 && 19 + -1*A + -1*F >= 0 && F >= 0 && 20 + -1*E + F >= 0 && -1 + D + F >= 0 && -20 + C + F >= 0 && 20 + -1*C + F >= 0 && -10 + B + F >= 0 && 10 + -1*B + F >= 0 && -3 + F + J >= 0 && 19 + -1*A + F >= 0 && 20 + -1*E >= 0 && 19 + D + -1*E >= 0 && C + -1*E >= 0 && 40 + -1*C + -1*E >= 0 && 10 + B + -1*E >= 0 && 30 + -1*B + -1*E >= 0 && 17 + -1*E + J >= 0 && 39 + -1*A + -1*E >= 0 && -1 + -1*A + E >= 0 && -2 + -1*D + J >= 0 && -1 + D >= 0 && -21 + C + D >= 0 && 19 + -1*C + D >= 0 && -11 + B + D >= 0 && 9 + -1*B + D >= 0 && -4 + D + J >= 0 && 18 + -1*A + D >= 0 && 20 + -1*C >= 0 && 10 + B + -1*C >= 0 && 30 + -1*B + -1*C >= 0 && 17 + -1*C + J >= 0 && 39 + -1*A + -1*C >= 0 && -20 + C >= 0 && -30 + B + C >= 0 && -10 + -1*B + C >= 0 && -23 + C + J >= 0 && -1 + -1*A + C >= 0 && 10 + -1*B >= 0 && 7 + -1*B + J >= 0 && 29 + -1*A + -1*B >= 0 && -10 + B >= 0 && -13 + B + J >= 0 && 9 + -1*A + B >= 0 && -3 + J >= 0 && 16 + -1*A + J >= 0 && 19 + -1*A >= 0 && J >= 1 + A] 17. f43(A,B,C,D,E,F,G,H,I,J,K) -> f48(-1 + A,B,C,D,E,F,G,H,I,J,K) [-1*G >= 0 (?,1) && F + -1*G >= 0 && -1*F + -1*G >= 0 && 20 + -1*E + -1*G >= 0 && -1 + D + -1*G >= 0 && -20 + C + -1*G >= 0 && 20 + -1*C + -1*G >= 0 && -10 + B + -1*G >= 0 && 10 + -1*B + -1*G >= 0 && -3 + -1*G + J >= 0 && 20 + -1*A + -1*G >= 0 && G >= 0 && F + G >= 0 && -1*F + G >= 0 && 20 + -1*E + G >= 0 && -1 + D + G >= 0 && -20 + C + G >= 0 && 20 + -1*C + G >= 0 && -10 + B + G >= 0 && 10 + -1*B + G >= 0 && -3 + G + J >= 0 && 20 + -1*A + G >= 0 && -1*F >= 0 && 20 + -1*E + -1*F >= 0 && -1 + D + -1*F >= 0 && -20 + C + -1*F >= 0 && 20 + -1*C + -1*F >= 0 && -10 + B + -1*F >= 0 && 10 + -1*B + -1*F >= 0 && -3 + -1*F + J >= 0 && 20 + -1*A + -1*F >= 0 && F >= 0 && 20 + -1*E + F >= 0 && -1 + D + F >= 0 && -20 + C + F >= 0 && 20 + -1*C + F >= 0 && -10 + B + F >= 0 && 10 + -1*B + F >= 0 && -3 + F + J >= 0 && 20 + -1*A + F >= 0 && 20 + -1*E >= 0 && 19 + D + -1*E >= 0 && C + -1*E >= 0 && 40 + -1*C + -1*E >= 0 && 10 + B + -1*E >= 0 && 30 + -1*B + -1*E >= 0 && 17 + -1*E + J >= 0 && 40 + -1*A + -1*E >= 0 && -1*A + E >= 0 && -2 + -1*D + J >= 0 && -1 + D >= 0 && -21 + C + D >= 0 && 19 + -1*C + D >= 0 && -11 + B + D >= 0 && 9 + -1*B + D >= 0 && -4 + D + J >= 0 && 19 + -1*A + D >= 0 && 20 + -1*C >= 0 && 10 + B + -1*C >= 0 && 30 + -1*B + -1*C >= 0 && 17 + -1*C + J >= 0 && 40 + -1*A + -1*C >= 0 && -20 + C >= 0 && -30 + B + C >= 0 && -10 + -1*B + C >= 0 && -23 + C + J >= 0 && -1*A + C >= 0 && 10 + -1*B >= 0 && 7 + -1*B + J >= 0 && 30 + -1*A + -1*B >= 0 && -10 + B >= 0 && -13 + B + J >= 0 && 10 + -1*A + B >= 0 && -3 + J >= 0 && 17 + -1*A + J >= 0 && 20 + -1*A >= 0] 18. f11(A,B,C,D,E,F,G,H,I,J,K) -> f69(A,B,C,D,E,F,G,H,I,J,K) [G >= 0 (1,1) && F + G >= 0 && 1 + -1*F + G >= 0 && 20 + -1*E + G >= 0 && -1 + D + G >= 0 && -20 + C + G >= 0 && 20 + -1*C + G >= 0 && -10 + B + G >= 0 && 10 + -1*B + G >= 0 && 1 + -1*F >= 0 && 21 + -1*E + -1*F >= 0 && D + -1*F >= 0 && -19 + C + -1*F >= 0 && 21 + -1*C + -1*F >= 0 && -9 + B + -1*F >= 0 && 11 + -1*B + -1*F >= 0 && F >= 0 && 20 + -1*E + F >= 0 && -1 + D + F >= 0 && -20 + C + F >= 0 && 20 + -1*C + F >= 0 && -10 + B + F >= 0 && 10 + -1*B + F >= 0 && 20 + -1*E >= 0 && 19 + D + -1*E >= 0 && C + -1*E >= 0 && 40 + -1*C + -1*E >= 0 && 10 + B + -1*E >= 0 && 30 + -1*B + -1*E >= 0 && -1 + D >= 0 && -21 + C + D >= 0 && 19 + -1*C + D >= 0 && -11 + B + D >= 0 && 9 + -1*B + D >= 0 && 20 + -1*C >= 0 && 10 + B + -1*C >= 0 && 30 + -1*B + -1*C >= 0 && -20 + C >= 0 && -30 + B + C >= 0 && -10 + -1*B + C >= 0 && 10 + -1*B >= 0 && -10 + B >= 0 && G >= 1] Signature: {(f0,11);(f11,11);(f40,11);(f43,11);(f48,11);(f54,11);(f59,11);(f63,11);(f69,11)} Flow Graph: [0->{2,3,4,5,18},1->{2,3,4,5,18},2->{2,3,4,5,18},3->{2,3,4,5,18},4->{2,3,4,5,18},5->{6,7},6->{12,13},7->{8 ,17},8->{8,17},9->{9,15,16},10->{6,7},11->{6,7},12->{0,14},13->{0,14},14->{2,3,4,5,18},15->{10,11},16->{10 ,11},17->{9,15,16},18->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(0,18) ,(1,2) ,(1,3) ,(1,4) ,(1,18) ,(2,2) ,(2,3) ,(2,4) ,(2,5) ,(3,2) ,(3,3) ,(3,4) ,(3,5) ,(4,2) ,(4,3) ,(4,4) ,(4,5) ,(10,7) ,(11,6) ,(12,0) ,(14,18) ,(15,10) ,(16,11)] * Step 3: Looptree NO + Considered Problem: Rules: 0. f63(A,B,C,D,E,F,G,H,I,J,K) -> f11(A,B,C,D,E,F,G,H,I,J,K) [-1*G >= 0 (?,1) && -1 + F + -1*G >= 0 && 1 + -1*F + -1*G >= 0 && 20 + -1*E + -1*G >= 0 && -1 + D + -1*G >= 0 && -20 + C + -1*G >= 0 && 20 + -1*C + -1*G >= 0 && -10 + B + -1*G >= 0 && 10 + -1*B + -1*G >= 0 && -2 + -1*G + J >= 0 && 20 + -1*A + -1*G >= 0 && G >= 0 && -1 + F + G >= 0 && 1 + -1*F + G >= 0 && 20 + -1*E + G >= 0 && -1 + D + G >= 0 && -20 + C + G >= 0 && 20 + -1*C + G >= 0 && -10 + B + G >= 0 && 10 + -1*B + G >= 0 && -2 + G + J >= 0 && 20 + -1*A + G >= 0 && 1 + -1*F >= 0 && 21 + -1*E + -1*F >= 0 && D + -1*F >= 0 && -19 + C + -1*F >= 0 && 21 + -1*C + -1*F >= 0 && -9 + B + -1*F >= 0 && 11 + -1*B + -1*F >= 0 && -1 + -1*F + J >= 0 && 21 + -1*A + -1*F >= 0 && -1 + F >= 0 && 19 + -1*E + F >= 0 && -2 + D + F >= 0 && -21 + C + F >= 0 && 19 + -1*C + F >= 0 && -11 + B + F >= 0 && 9 + -1*B + F >= 0 && -3 + F + J >= 0 && 19 + -1*A + F >= 0 && 20 + -1*E >= 0 && 19 + D + -1*E >= 0 && C + -1*E >= 0 && 40 + -1*C + -1*E >= 0 && 10 + B + -1*E >= 0 && 30 + -1*B + -1*E >= 0 && 18 + -1*E + J >= 0 && 39 + -1*A + -1*E >= 0 && 1 + -1*A + E >= 0 && -1 + -1*D + J >= 0 && -1 + D >= 0 && -21 + C + D >= 0 && 19 + -1*C + D >= 0 && -11 + B + D >= 0 && 9 + -1*B + D >= 0 && -3 + D + J >= 0 && 19 + -1*A + D >= 0 && 20 + -1*C >= 0 && 10 + B + -1*C >= 0 && 30 + -1*B + -1*C >= 0 && 18 + -1*C + J >= 0 && 40 + -1*A + -1*C >= 0 && -20 + C >= 0 && -30 + B + C >= 0 && -10 + -1*B + C >= 0 && -22 + C + J >= 0 && -1*A + C >= 0 && 10 + -1*B >= 0 && 8 + -1*B + J >= 0 && 30 + -1*A + -1*B >= 0 && -10 + B >= 0 && -12 + B + J >= 0 && 10 + -1*A + B >= 0 && -2 + J >= 0 && 18 + -1*A + J >= 0 && 20 + -1*A >= 0 && A >= 1 + B] 1. f0(A,B,C,D,E,F,G,H,I,J,K) -> f11(A,10,20,1,20,0,0,H,I,J,K) True (1,1) 2. f11(A,B,C,D,E,F,G,H,I,J,K) -> f11(A,B,C,D,E,F,1,H,I,J,K) [G >= 0 (?,1) && F + G >= 0 && 1 + -1*F + G >= 0 && 20 + -1*E + G >= 0 && -1 + D + G >= 0 && -20 + C + G >= 0 && 20 + -1*C + G >= 0 && -10 + B + G >= 0 && 10 + -1*B + G >= 0 && 1 + -1*F >= 0 && 21 + -1*E + -1*F >= 0 && D + -1*F >= 0 && -19 + C + -1*F >= 0 && 21 + -1*C + -1*F >= 0 && -9 + B + -1*F >= 0 && 11 + -1*B + -1*F >= 0 && F >= 0 && 20 + -1*E + F >= 0 && -1 + D + F >= 0 && -20 + C + F >= 0 && 20 + -1*C + F >= 0 && -10 + B + F >= 0 && 10 + -1*B + F >= 0 && 20 + -1*E >= 0 && 19 + D + -1*E >= 0 && C + -1*E >= 0 && 40 + -1*C + -1*E >= 0 && 10 + B + -1*E >= 0 && 30 + -1*B + -1*E >= 0 && -1 + D >= 0 && -21 + C + D >= 0 && 19 + -1*C + D >= 0 && -11 + B + D >= 0 && 9 + -1*B + D >= 0 && 20 + -1*C >= 0 && 10 + B + -1*C >= 0 && 30 + -1*B + -1*C >= 0 && -20 + C >= 0 && -30 + B + C >= 0 && -10 + -1*B + C >= 0 && 10 + -1*B >= 0 && -10 + B >= 0 && D >= E && G = 0] 3. f11(A,B,C,D,E,F,G,H,I,J,K) -> f11(A,B,C,D,1 + D,F,1,H,I,J,K) [G >= 0 (?,1) && F + G >= 0 && 1 + -1*F + G >= 0 && 20 + -1*E + G >= 0 && -1 + D + G >= 0 && -20 + C + G >= 0 && 20 + -1*C + G >= 0 && -10 + B + G >= 0 && 10 + -1*B + G >= 0 && 1 + -1*F >= 0 && 21 + -1*E + -1*F >= 0 && D + -1*F >= 0 && -19 + C + -1*F >= 0 && 21 + -1*C + -1*F >= 0 && -9 + B + -1*F >= 0 && 11 + -1*B + -1*F >= 0 && F >= 0 && 20 + -1*E + F >= 0 && -1 + D + F >= 0 && -20 + C + F >= 0 && 20 + -1*C + F >= 0 && -10 + B + F >= 0 && 10 + -1*B + F >= 0 && 20 + -1*E >= 0 && 19 + D + -1*E >= 0 && C + -1*E >= 0 && 40 + -1*C + -1*E >= 0 && 10 + B + -1*E >= 0 && 30 + -1*B + -1*E >= 0 && -1 + D >= 0 && -21 + C + D >= 0 && 19 + -1*C + D >= 0 && -11 + B + D >= 0 && 9 + -1*B + D >= 0 && 20 + -1*C >= 0 && 10 + B + -1*C >= 0 && 30 + -1*B + -1*C >= 0 && -20 + C >= 0 && -30 + B + C >= 0 && -10 + -1*B + C >= 0 && 10 + -1*B >= 0 && -10 + B >= 0 && E = 1 + D && G = 0] 4. f11(A,B,C,D,E,F,G,H,I,J,K) -> f11(A,B,C,D,1 + D,F,1,N,I,J,K) [G >= 0 (?,1) && F + G >= 0 && 1 + -1*F + G >= 0 && 20 + -1*E + G >= 0 && -1 + D + G >= 0 && -20 + C + G >= 0 && 20 + -1*C + G >= 0 && -10 + B + G >= 0 && 10 + -1*B + G >= 0 && 1 + -1*F >= 0 && 21 + -1*E + -1*F >= 0 && D + -1*F >= 0 && -19 + C + -1*F >= 0 && 21 + -1*C + -1*F >= 0 && -9 + B + -1*F >= 0 && 11 + -1*B + -1*F >= 0 && F >= 0 && 20 + -1*E + F >= 0 && -1 + D + F >= 0 && -20 + C + F >= 0 && 20 + -1*C + F >= 0 && -10 + B + F >= 0 && 10 + -1*B + F >= 0 && 20 + -1*E >= 0 && 19 + D + -1*E >= 0 && C + -1*E >= 0 && 40 + -1*C + -1*E >= 0 && 10 + B + -1*E >= 0 && 30 + -1*B + -1*E >= 0 && -1 + D >= 0 && -21 + C + D >= 0 && 19 + -1*C + D >= 0 && -11 + B + D >= 0 && 9 + -1*B + D >= 0 && 20 + -1*C >= 0 && 10 + B + -1*C >= 0 && 30 + -1*B + -1*C >= 0 && -20 + C >= 0 && -30 + B + C >= 0 && -10 + -1*B + C >= 0 && 10 + -1*B >= 0 && -10 + B >= 0 && L >= 1 + M && E = 1 + D && G = 0] 5. f11(A,B,C,D,E,F,G,H,I,J,K) -> f40(E,B,C,D,E,F,0,N,L,1 + D,M) [G >= 0 (?,1) && F + G >= 0 && 1 + -1*F + G >= 0 && 20 + -1*E + G >= 0 && -1 + D + G >= 0 && -20 + C + G >= 0 && 20 + -1*C + G >= 0 && -10 + B + G >= 0 && 10 + -1*B + G >= 0 && 1 + -1*F >= 0 && 21 + -1*E + -1*F >= 0 && D + -1*F >= 0 && -19 + C + -1*F >= 0 && 21 + -1*C + -1*F >= 0 && -9 + B + -1*F >= 0 && 11 + -1*B + -1*F >= 0 && F >= 0 && 20 + -1*E + F >= 0 && -1 + D + F >= 0 && -20 + C + F >= 0 && 20 + -1*C + F >= 0 && -10 + B + F >= 0 && 10 + -1*B + F >= 0 && 20 + -1*E >= 0 && 19 + D + -1*E >= 0 && C + -1*E >= 0 && 40 + -1*C + -1*E >= 0 && 10 + B + -1*E >= 0 && 30 + -1*B + -1*E >= 0 && -1 + D >= 0 && -21 + C + D >= 0 && 19 + -1*C + D >= 0 && -11 + B + D >= 0 && 9 + -1*B + D >= 0 && 20 + -1*C >= 0 && 10 + B + -1*C >= 0 && 30 + -1*B + -1*C >= 0 && -20 + C >= 0 && -30 + B + C >= 0 && -10 + -1*B + C >= 0 && 10 + -1*B >= 0 && -10 + B >= 0 && E >= 2 + D && G = 0] 6. f40(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,H,I,J,K) [-1*G >= 0 (?,1) && F + -1*G >= 0 && 1 + -1*F + -1*G >= 0 && 20 + -1*E + -1*G >= 0 && -1 + D + -1*G >= 0 && -20 + C + -1*G >= 0 && 20 + -1*C + -1*G >= 0 && -10 + B + -1*G >= 0 && 10 + -1*B + -1*G >= 0 && -2 + -1*G + J >= 0 && 20 + -1*A + -1*G >= 0 && G >= 0 && F + G >= 0 && 1 + -1*F + G >= 0 && 20 + -1*E + G >= 0 && -1 + D + G >= 0 && -20 + C + G >= 0 && 20 + -1*C + G >= 0 && -10 + B + G >= 0 && 10 + -1*B + G >= 0 && -2 + G + J >= 0 && 20 + -1*A + G >= 0 && 1 + -1*F >= 0 && 21 + -1*E + -1*F >= 0 && D + -1*F >= 0 && -19 + C + -1*F >= 0 && 21 + -1*C + -1*F >= 0 && -9 + B + -1*F >= 0 && 11 + -1*B + -1*F >= 0 && -1 + -1*F + J >= 0 && 21 + -1*A + -1*F >= 0 && F >= 0 && 20 + -1*E + F >= 0 && -1 + D + F >= 0 && -20 + C + F >= 0 && 20 + -1*C + F >= 0 && -10 + B + F >= 0 && 10 + -1*B + F >= 0 && -2 + F + J >= 0 && 20 + -1*A + F >= 0 && 20 + -1*E >= 0 && 19 + D + -1*E >= 0 && C + -1*E >= 0 && 40 + -1*C + -1*E >= 0 && 10 + B + -1*E >= 0 && 30 + -1*B + -1*E >= 0 && 18 + -1*E + J >= 0 && 40 + -1*A + -1*E >= 0 && -1*A + E >= 0 && -1 + -1*D + J >= 0 && -1 + D >= 0 && -21 + C + D >= 0 && 19 + -1*C + D >= 0 && -11 + B + D >= 0 && 9 + -1*B + D >= 0 && -3 + D + J >= 0 && 19 + -1*A + D >= 0 && 20 + -1*C >= 0 && 10 + B + -1*C >= 0 && 30 + -1*B + -1*C >= 0 && 18 + -1*C + J >= 0 && 40 + -1*A + -1*C >= 0 && -20 + C >= 0 && -30 + B + C >= 0 && -10 + -1*B + C >= 0 && -22 + C + J >= 0 && -1*A + C >= 0 && 10 + -1*B >= 0 && 8 + -1*B + J >= 0 && 30 + -1*A + -1*B >= 0 && -10 + B >= 0 && -12 + B + J >= 0 && 10 + -1*A + B >= 0 && -2 + J >= 0 && 18 + -1*A + J >= 0 && 20 + -1*A >= 0 && F >= 1] 7. f40(A,B,C,D,E,F,G,H,I,J,K) -> f43(A,B,C,D,E,0,G,H,I,1 + J,K) [-1*G >= 0 (?,1) && F + -1*G >= 0 && 1 + -1*F + -1*G >= 0 && 20 + -1*E + -1*G >= 0 && -1 + D + -1*G >= 0 && -20 + C + -1*G >= 0 && 20 + -1*C + -1*G >= 0 && -10 + B + -1*G >= 0 && 10 + -1*B + -1*G >= 0 && -2 + -1*G + J >= 0 && 20 + -1*A + -1*G >= 0 && G >= 0 && F + G >= 0 && 1 + -1*F + G >= 0 && 20 + -1*E + G >= 0 && -1 + D + G >= 0 && -20 + C + G >= 0 && 20 + -1*C + G >= 0 && -10 + B + G >= 0 && 10 + -1*B + G >= 0 && -2 + G + J >= 0 && 20 + -1*A + G >= 0 && 1 + -1*F >= 0 && 21 + -1*E + -1*F >= 0 && D + -1*F >= 0 && -19 + C + -1*F >= 0 && 21 + -1*C + -1*F >= 0 && -9 + B + -1*F >= 0 && 11 + -1*B + -1*F >= 0 && -1 + -1*F + J >= 0 && 21 + -1*A + -1*F >= 0 && F >= 0 && 20 + -1*E + F >= 0 && -1 + D + F >= 0 && -20 + C + F >= 0 && 20 + -1*C + F >= 0 && -10 + B + F >= 0 && 10 + -1*B + F >= 0 && -2 + F + J >= 0 && 20 + -1*A + F >= 0 && 20 + -1*E >= 0 && 19 + D + -1*E >= 0 && C + -1*E >= 0 && 40 + -1*C + -1*E >= 0 && 10 + B + -1*E >= 0 && 30 + -1*B + -1*E >= 0 && 18 + -1*E + J >= 0 && 40 + -1*A + -1*E >= 0 && -1*A + E >= 0 && -1 + -1*D + J >= 0 && -1 + D >= 0 && -21 + C + D >= 0 && 19 + -1*C + D >= 0 && -11 + B + D >= 0 && 9 + -1*B + D >= 0 && -3 + D + J >= 0 && 19 + -1*A + D >= 0 && 20 + -1*C >= 0 && 10 + B + -1*C >= 0 && 30 + -1*B + -1*C >= 0 && 18 + -1*C + J >= 0 && 40 + -1*A + -1*C >= 0 && -20 + C >= 0 && -30 + B + C >= 0 && -10 + -1*B + C >= 0 && -22 + C + J >= 0 && -1*A + C >= 0 && 10 + -1*B >= 0 && 8 + -1*B + J >= 0 && 30 + -1*A + -1*B >= 0 && -10 + B >= 0 && -12 + B + J >= 0 && 10 + -1*A + B >= 0 && -2 + J >= 0 && 18 + -1*A + J >= 0 && 20 + -1*A >= 0 && F = 0] 8. f43(A,B,C,D,E,F,G,H,I,J,K) -> f43(A,B,C,D,E,F,G,H,I,1 + J,K) [-1*G >= 0 (?,1) && F + -1*G >= 0 && -1*F + -1*G >= 0 && 20 + -1*E + -1*G >= 0 && -1 + D + -1*G >= 0 && -20 + C + -1*G >= 0 && 20 + -1*C + -1*G >= 0 && -10 + B + -1*G >= 0 && 10 + -1*B + -1*G >= 0 && -3 + -1*G + J >= 0 && 20 + -1*A + -1*G >= 0 && G >= 0 && F + G >= 0 && -1*F + G >= 0 && 20 + -1*E + G >= 0 && -1 + D + G >= 0 && -20 + C + G >= 0 && 20 + -1*C + G >= 0 && -10 + B + G >= 0 && 10 + -1*B + G >= 0 && -3 + G + J >= 0 && 20 + -1*A + G >= 0 && -1*F >= 0 && 20 + -1*E + -1*F >= 0 && -1 + D + -1*F >= 0 && -20 + C + -1*F >= 0 && 20 + -1*C + -1*F >= 0 && -10 + B + -1*F >= 0 && 10 + -1*B + -1*F >= 0 && -3 + -1*F + J >= 0 && 20 + -1*A + -1*F >= 0 && F >= 0 && 20 + -1*E + F >= 0 && -1 + D + F >= 0 && -20 + C + F >= 0 && 20 + -1*C + F >= 0 && -10 + B + F >= 0 && 10 + -1*B + F >= 0 && -3 + F + J >= 0 && 20 + -1*A + F >= 0 && 20 + -1*E >= 0 && 19 + D + -1*E >= 0 && C + -1*E >= 0 && 40 + -1*C + -1*E >= 0 && 10 + B + -1*E >= 0 && 30 + -1*B + -1*E >= 0 && 17 + -1*E + J >= 0 && 40 + -1*A + -1*E >= 0 && -1*A + E >= 0 && -2 + -1*D + J >= 0 && -1 + D >= 0 && -21 + C + D >= 0 && 19 + -1*C + D >= 0 && -11 + B + D >= 0 && 9 + -1*B + D >= 0 && -4 + D + J >= 0 && 19 + -1*A + D >= 0 && 20 + -1*C >= 0 && 10 + B + -1*C >= 0 && 30 + -1*B + -1*C >= 0 && 17 + -1*C + J >= 0 && 40 + -1*A + -1*C >= 0 && -20 + C >= 0 && -30 + B + C >= 0 && -10 + -1*B + C >= 0 && -23 + C + J >= 0 && -1*A + C >= 0 && 10 + -1*B >= 0 && 7 + -1*B + J >= 0 && 30 + -1*A + -1*B >= 0 && -10 + B >= 0 && -13 + B + J >= 0 && 10 + -1*A + B >= 0 && -3 + J >= 0 && 17 + -1*A + J >= 0 && 20 + -1*A >= 0 && K >= 1 + N] 9. f48(A,B,C,D,E,F,G,H,I,J,K) -> f48(-1 + A,B,C,D,E,F,G,H,I,J,K) [-1*G >= 0 (?,1) && F + -1*G >= 0 && -1*F + -1*G >= 0 && 20 + -1*E + -1*G >= 0 && -1 + D + -1*G >= 0 && -20 + C + -1*G >= 0 && 20 + -1*C + -1*G >= 0 && -10 + B + -1*G >= 0 && 10 + -1*B + -1*G >= 0 && -3 + -1*G + J >= 0 && 19 + -1*A + -1*G >= 0 && G >= 0 && F + G >= 0 && -1*F + G >= 0 && 20 + -1*E + G >= 0 && -1 + D + G >= 0 && -20 + C + G >= 0 && 20 + -1*C + G >= 0 && -10 + B + G >= 0 && 10 + -1*B + G >= 0 && -3 + G + J >= 0 && 19 + -1*A + G >= 0 && -1*F >= 0 && 20 + -1*E + -1*F >= 0 && -1 + D + -1*F >= 0 && -20 + C + -1*F >= 0 && 20 + -1*C + -1*F >= 0 && -10 + B + -1*F >= 0 && 10 + -1*B + -1*F >= 0 && -3 + -1*F + J >= 0 && 19 + -1*A + -1*F >= 0 && F >= 0 && 20 + -1*E + F >= 0 && -1 + D + F >= 0 && -20 + C + F >= 0 && 20 + -1*C + F >= 0 && -10 + B + F >= 0 && 10 + -1*B + F >= 0 && -3 + F + J >= 0 && 19 + -1*A + F >= 0 && 20 + -1*E >= 0 && 19 + D + -1*E >= 0 && C + -1*E >= 0 && 40 + -1*C + -1*E >= 0 && 10 + B + -1*E >= 0 && 30 + -1*B + -1*E >= 0 && 17 + -1*E + J >= 0 && 39 + -1*A + -1*E >= 0 && -1 + -1*A + E >= 0 && -2 + -1*D + J >= 0 && -1 + D >= 0 && -21 + C + D >= 0 && 19 + -1*C + D >= 0 && -11 + B + D >= 0 && 9 + -1*B + D >= 0 && -4 + D + J >= 0 && 18 + -1*A + D >= 0 && 20 + -1*C >= 0 && 10 + B + -1*C >= 0 && 30 + -1*B + -1*C >= 0 && 17 + -1*C + J >= 0 && 39 + -1*A + -1*C >= 0 && -20 + C >= 0 && -30 + B + C >= 0 && -10 + -1*B + C >= 0 && -23 + C + J >= 0 && -1 + -1*A + C >= 0 && 10 + -1*B >= 0 && 7 + -1*B + J >= 0 && 29 + -1*A + -1*B >= 0 && -10 + B >= 0 && -13 + B + J >= 0 && 9 + -1*A + B >= 0 && -3 + J >= 0 && 16 + -1*A + J >= 0 && 19 + -1*A >= 0] 10. f54(A,B,C,D,E,F,G,H,I,J,K) -> f40(A,B,C,D,E,F,G,H,I,J,K) [-1*G >= 0 (?,1) && F + -1*G >= 0 && 1 + -1*F + -1*G >= 0 && 20 + -1*E + -1*G >= 0 && -1 + D + -1*G >= 0 && -20 + C + -1*G >= 0 && 20 + -1*C + -1*G >= 0 && -10 + B + -1*G >= 0 && 10 + -1*B + -1*G >= 0 && -3 + -1*G + J >= 0 && 19 + -1*A + -1*G >= 0 && G >= 0 && F + G >= 0 && 1 + -1*F + G >= 0 && 20 + -1*E + G >= 0 && -1 + D + G >= 0 && -20 + C + G >= 0 && 20 + -1*C + G >= 0 && -10 + B + G >= 0 && 10 + -1*B + G >= 0 && -3 + G + J >= 0 && 19 + -1*A + G >= 0 && 1 + -1*F >= 0 && 21 + -1*E + -1*F >= 0 && D + -1*F >= 0 && -19 + C + -1*F >= 0 && 21 + -1*C + -1*F >= 0 && -9 + B + -1*F >= 0 && 11 + -1*B + -1*F >= 0 && -2 + -1*F + J >= 0 && 20 + -1*A + -1*F >= 0 && F >= 0 && 20 + -1*E + F >= 0 && -1 + D + F >= 0 && -20 + C + F >= 0 && 20 + -1*C + F >= 0 && -10 + B + F >= 0 && 10 + -1*B + F >= 0 && -3 + F + J >= 0 && 19 + -1*A + F >= 0 && 20 + -1*E >= 0 && 19 + D + -1*E >= 0 && C + -1*E >= 0 && 40 + -1*C + -1*E >= 0 && 10 + B + -1*E >= 0 && 30 + -1*B + -1*E >= 0 && 17 + -1*E + J >= 0 && 39 + -1*A + -1*E >= 0 && -1 + -1*A + E >= 0 && -2 + -1*D + J >= 0 && -1 + D >= 0 && -21 + C + D >= 0 && 19 + -1*C + D >= 0 && -11 + B + D >= 0 && 9 + -1*B + D >= 0 && -4 + D + J >= 0 && 18 + -1*A + D >= 0 && 20 + -1*C >= 0 && 10 + B + -1*C >= 0 && 30 + -1*B + -1*C >= 0 && 17 + -1*C + J >= 0 && 39 + -1*A + -1*C >= 0 && -20 + C >= 0 && -30 + B + C >= 0 && -10 + -1*B + C >= 0 && -23 + C + J >= 0 && -1 + -1*A + C >= 0 && 10 + -1*B >= 0 && 7 + -1*B + J >= 0 && 29 + -1*A + -1*B >= 0 && -10 + B >= 0 && -13 + B + J >= 0 && 9 + -1*A + B >= 0 && -3 + J >= 0 && 16 + -1*A + J >= 0 && 19 + -1*A >= 0 && F >= 1] 11. f54(A,B,C,D,E,F,G,H,I,J,K) -> f40(A,B,C,D,E,0,G,N,I,J,K) [-1*G >= 0 (?,1) && F + -1*G >= 0 && 1 + -1*F + -1*G >= 0 && 20 + -1*E + -1*G >= 0 && -1 + D + -1*G >= 0 && -20 + C + -1*G >= 0 && 20 + -1*C + -1*G >= 0 && -10 + B + -1*G >= 0 && 10 + -1*B + -1*G >= 0 && -3 + -1*G + J >= 0 && 19 + -1*A + -1*G >= 0 && G >= 0 && F + G >= 0 && 1 + -1*F + G >= 0 && 20 + -1*E + G >= 0 && -1 + D + G >= 0 && -20 + C + G >= 0 && 20 + -1*C + G >= 0 && -10 + B + G >= 0 && 10 + -1*B + G >= 0 && -3 + G + J >= 0 && 19 + -1*A + G >= 0 && 1 + -1*F >= 0 && 21 + -1*E + -1*F >= 0 && D + -1*F >= 0 && -19 + C + -1*F >= 0 && 21 + -1*C + -1*F >= 0 && -9 + B + -1*F >= 0 && 11 + -1*B + -1*F >= 0 && -2 + -1*F + J >= 0 && 20 + -1*A + -1*F >= 0 && F >= 0 && 20 + -1*E + F >= 0 && -1 + D + F >= 0 && -20 + C + F >= 0 && 20 + -1*C + F >= 0 && -10 + B + F >= 0 && 10 + -1*B + F >= 0 && -3 + F + J >= 0 && 19 + -1*A + F >= 0 && 20 + -1*E >= 0 && 19 + D + -1*E >= 0 && C + -1*E >= 0 && 40 + -1*C + -1*E >= 0 && 10 + B + -1*E >= 0 && 30 + -1*B + -1*E >= 0 && 17 + -1*E + J >= 0 && 39 + -1*A + -1*E >= 0 && -1 + -1*A + E >= 0 && -2 + -1*D + J >= 0 && -1 + D >= 0 && -21 + C + D >= 0 && 19 + -1*C + D >= 0 && -11 + B + D >= 0 && 9 + -1*B + D >= 0 && -4 + D + J >= 0 && 18 + -1*A + D >= 0 && 20 + -1*C >= 0 && 10 + B + -1*C >= 0 && 30 + -1*B + -1*C >= 0 && 17 + -1*C + J >= 0 && 39 + -1*A + -1*C >= 0 && -20 + C >= 0 && -30 + B + C >= 0 && -10 + -1*B + C >= 0 && -23 + C + J >= 0 && -1 + -1*A + C >= 0 && 10 + -1*B >= 0 && 7 + -1*B + J >= 0 && 29 + -1*A + -1*B >= 0 && -10 + B >= 0 && -13 + B + J >= 0 && 9 + -1*A + B >= 0 && -3 + J >= 0 && 16 + -1*A + J >= 0 && 19 + -1*A >= 0 && F = 0] 12. f59(A,B,C,D,E,F,G,H,I,J,K) -> f63(A,B,C,D,E,F,G,H,I,J,K) [-1*G >= 0 (?,1) && -1 + F + -1*G >= 0 && 1 + -1*F + -1*G >= 0 && 20 + -1*E + -1*G >= 0 && -1 + D + -1*G >= 0 && -20 + C + -1*G >= 0 && 20 + -1*C + -1*G >= 0 && -10 + B + -1*G >= 0 && 10 + -1*B + -1*G >= 0 && -2 + -1*G + J >= 0 && 20 + -1*A + -1*G >= 0 && G >= 0 && -1 + F + G >= 0 && 1 + -1*F + G >= 0 && 20 + -1*E + G >= 0 && -1 + D + G >= 0 && -20 + C + G >= 0 && 20 + -1*C + G >= 0 && -10 + B + G >= 0 && 10 + -1*B + G >= 0 && -2 + G + J >= 0 && 20 + -1*A + G >= 0 && 1 + -1*F >= 0 && 21 + -1*E + -1*F >= 0 && D + -1*F >= 0 && -19 + C + -1*F >= 0 && 21 + -1*C + -1*F >= 0 && -9 + B + -1*F >= 0 && 11 + -1*B + -1*F >= 0 && -1 + -1*F + J >= 0 && 21 + -1*A + -1*F >= 0 && -1 + F >= 0 && 19 + -1*E + F >= 0 && -2 + D + F >= 0 && -21 + C + F >= 0 && 19 + -1*C + F >= 0 && -11 + B + F >= 0 && 9 + -1*B + F >= 0 && -3 + F + J >= 0 && 19 + -1*A + F >= 0 && 20 + -1*E >= 0 && 19 + D + -1*E >= 0 && C + -1*E >= 0 && 40 + -1*C + -1*E >= 0 && 10 + B + -1*E >= 0 && 30 + -1*B + -1*E >= 0 && 18 + -1*E + J >= 0 && 40 + -1*A + -1*E >= 0 && -1*A + E >= 0 && -1 + -1*D + J >= 0 && -1 + D >= 0 && -21 + C + D >= 0 && 19 + -1*C + D >= 0 && -11 + B + D >= 0 && 9 + -1*B + D >= 0 && -3 + D + J >= 0 && 19 + -1*A + D >= 0 && 20 + -1*C >= 0 && 10 + B + -1*C >= 0 && 30 + -1*B + -1*C >= 0 && 18 + -1*C + J >= 0 && 40 + -1*A + -1*C >= 0 && -20 + C >= 0 && -30 + B + C >= 0 && -10 + -1*B + C >= 0 && -22 + C + J >= 0 && -1*A + C >= 0 && 10 + -1*B >= 0 && 8 + -1*B + J >= 0 && 30 + -1*A + -1*B >= 0 && -10 + B >= 0 && -12 + B + J >= 0 && 10 + -1*A + B >= 0 && -2 + J >= 0 && 18 + -1*A + J >= 0 && 20 + -1*A >= 0 && B >= 1 + A] 13. f59(A,B,C,D,E,F,G,H,I,J,K) -> f63(A,B,C,D,-1 + A,F,G,H,I,J,K) [-1*G >= 0 (?,1) && -1 + F + -1*G >= 0 && 1 + -1*F + -1*G >= 0 && 20 + -1*E + -1*G >= 0 && -1 + D + -1*G >= 0 && -20 + C + -1*G >= 0 && 20 + -1*C + -1*G >= 0 && -10 + B + -1*G >= 0 && 10 + -1*B + -1*G >= 0 && -2 + -1*G + J >= 0 && 20 + -1*A + -1*G >= 0 && G >= 0 && -1 + F + G >= 0 && 1 + -1*F + G >= 0 && 20 + -1*E + G >= 0 && -1 + D + G >= 0 && -20 + C + G >= 0 && 20 + -1*C + G >= 0 && -10 + B + G >= 0 && 10 + -1*B + G >= 0 && -2 + G + J >= 0 && 20 + -1*A + G >= 0 && 1 + -1*F >= 0 && 21 + -1*E + -1*F >= 0 && D + -1*F >= 0 && -19 + C + -1*F >= 0 && 21 + -1*C + -1*F >= 0 && -9 + B + -1*F >= 0 && 11 + -1*B + -1*F >= 0 && -1 + -1*F + J >= 0 && 21 + -1*A + -1*F >= 0 && -1 + F >= 0 && 19 + -1*E + F >= 0 && -2 + D + F >= 0 && -21 + C + F >= 0 && 19 + -1*C + F >= 0 && -11 + B + F >= 0 && 9 + -1*B + F >= 0 && -3 + F + J >= 0 && 19 + -1*A + F >= 0 && 20 + -1*E >= 0 && 19 + D + -1*E >= 0 && C + -1*E >= 0 && 40 + -1*C + -1*E >= 0 && 10 + B + -1*E >= 0 && 30 + -1*B + -1*E >= 0 && 18 + -1*E + J >= 0 && 40 + -1*A + -1*E >= 0 && -1*A + E >= 0 && -1 + -1*D + J >= 0 && -1 + D >= 0 && -21 + C + D >= 0 && 19 + -1*C + D >= 0 && -11 + B + D >= 0 && 9 + -1*B + D >= 0 && -3 + D + J >= 0 && 19 + -1*A + D >= 0 && 20 + -1*C >= 0 && 10 + B + -1*C >= 0 && 30 + -1*B + -1*C >= 0 && 18 + -1*C + J >= 0 && 40 + -1*A + -1*C >= 0 && -20 + C >= 0 && -30 + B + C >= 0 && -10 + -1*B + C >= 0 && -22 + C + J >= 0 && -1*A + C >= 0 && 10 + -1*B >= 0 && 8 + -1*B + J >= 0 && 30 + -1*A + -1*B >= 0 && -10 + B >= 0 && -12 + B + J >= 0 && 10 + -1*A + B >= 0 && -2 + J >= 0 && 18 + -1*A + J >= 0 && 20 + -1*A >= 0 && A >= B] 14. f63(A,B,C,D,E,F,G,H,I,J,K) -> f11(A,B,C,J,E,F,G,H,I,J,K) [-1*G >= 0 (?,1) && -1 + F + -1*G >= 0 && 1 + -1*F + -1*G >= 0 && 20 + -1*E + -1*G >= 0 && -1 + D + -1*G >= 0 && -20 + C + -1*G >= 0 && 20 + -1*C + -1*G >= 0 && -10 + B + -1*G >= 0 && 10 + -1*B + -1*G >= 0 && -2 + -1*G + J >= 0 && 20 + -1*A + -1*G >= 0 && G >= 0 && -1 + F + G >= 0 && 1 + -1*F + G >= 0 && 20 + -1*E + G >= 0 && -1 + D + G >= 0 && -20 + C + G >= 0 && 20 + -1*C + G >= 0 && -10 + B + G >= 0 && 10 + -1*B + G >= 0 && -2 + G + J >= 0 && 20 + -1*A + G >= 0 && 1 + -1*F >= 0 && 21 + -1*E + -1*F >= 0 && D + -1*F >= 0 && -19 + C + -1*F >= 0 && 21 + -1*C + -1*F >= 0 && -9 + B + -1*F >= 0 && 11 + -1*B + -1*F >= 0 && -1 + -1*F + J >= 0 && 21 + -1*A + -1*F >= 0 && -1 + F >= 0 && 19 + -1*E + F >= 0 && -2 + D + F >= 0 && -21 + C + F >= 0 && 19 + -1*C + F >= 0 && -11 + B + F >= 0 && 9 + -1*B + F >= 0 && -3 + F + J >= 0 && 19 + -1*A + F >= 0 && 20 + -1*E >= 0 && 19 + D + -1*E >= 0 && C + -1*E >= 0 && 40 + -1*C + -1*E >= 0 && 10 + B + -1*E >= 0 && 30 + -1*B + -1*E >= 0 && 18 + -1*E + J >= 0 && 39 + -1*A + -1*E >= 0 && 1 + -1*A + E >= 0 && -1 + -1*D + J >= 0 && -1 + D >= 0 && -21 + C + D >= 0 && 19 + -1*C + D >= 0 && -11 + B + D >= 0 && 9 + -1*B + D >= 0 && -3 + D + J >= 0 && 19 + -1*A + D >= 0 && 20 + -1*C >= 0 && 10 + B + -1*C >= 0 && 30 + -1*B + -1*C >= 0 && 18 + -1*C + J >= 0 && 40 + -1*A + -1*C >= 0 && -20 + C >= 0 && -30 + B + C >= 0 && -10 + -1*B + C >= 0 && -22 + C + J >= 0 && -1*A + C >= 0 && 10 + -1*B >= 0 && 8 + -1*B + J >= 0 && 30 + -1*A + -1*B >= 0 && -10 + B >= 0 && -12 + B + J >= 0 && 10 + -1*A + B >= 0 && -2 + J >= 0 && 18 + -1*A + J >= 0 && 20 + -1*A >= 0 && B >= A] 15. f48(A,B,C,D,E,F,G,H,I,J,K) -> f54(A,B,C,D,E,F,G,H,I,J,K) [-1*G >= 0 (?,1) && F + -1*G >= 0 && -1*F + -1*G >= 0 && 20 + -1*E + -1*G >= 0 && -1 + D + -1*G >= 0 && -20 + C + -1*G >= 0 && 20 + -1*C + -1*G >= 0 && -10 + B + -1*G >= 0 && 10 + -1*B + -1*G >= 0 && -3 + -1*G + J >= 0 && 19 + -1*A + -1*G >= 0 && G >= 0 && F + G >= 0 && -1*F + G >= 0 && 20 + -1*E + G >= 0 && -1 + D + G >= 0 && -20 + C + G >= 0 && 20 + -1*C + G >= 0 && -10 + B + G >= 0 && 10 + -1*B + G >= 0 && -3 + G + J >= 0 && 19 + -1*A + G >= 0 && -1*F >= 0 && 20 + -1*E + -1*F >= 0 && -1 + D + -1*F >= 0 && -20 + C + -1*F >= 0 && 20 + -1*C + -1*F >= 0 && -10 + B + -1*F >= 0 && 10 + -1*B + -1*F >= 0 && -3 + -1*F + J >= 0 && 19 + -1*A + -1*F >= 0 && F >= 0 && 20 + -1*E + F >= 0 && -1 + D + F >= 0 && -20 + C + F >= 0 && 20 + -1*C + F >= 0 && -10 + B + F >= 0 && 10 + -1*B + F >= 0 && -3 + F + J >= 0 && 19 + -1*A + F >= 0 && 20 + -1*E >= 0 && 19 + D + -1*E >= 0 && C + -1*E >= 0 && 40 + -1*C + -1*E >= 0 && 10 + B + -1*E >= 0 && 30 + -1*B + -1*E >= 0 && 17 + -1*E + J >= 0 && 39 + -1*A + -1*E >= 0 && -1 + -1*A + E >= 0 && -2 + -1*D + J >= 0 && -1 + D >= 0 && -21 + C + D >= 0 && 19 + -1*C + D >= 0 && -11 + B + D >= 0 && 9 + -1*B + D >= 0 && -4 + D + J >= 0 && 18 + -1*A + D >= 0 && 20 + -1*C >= 0 && 10 + B + -1*C >= 0 && 30 + -1*B + -1*C >= 0 && 17 + -1*C + J >= 0 && 39 + -1*A + -1*C >= 0 && -20 + C >= 0 && -30 + B + C >= 0 && -10 + -1*B + C >= 0 && -23 + C + J >= 0 && -1 + -1*A + C >= 0 && 10 + -1*B >= 0 && 7 + -1*B + J >= 0 && 29 + -1*A + -1*B >= 0 && -10 + B >= 0 && -13 + B + J >= 0 && 9 + -1*A + B >= 0 && -3 + J >= 0 && 16 + -1*A + J >= 0 && 19 + -1*A >= 0 && A >= J] 16. f48(A,B,C,D,E,F,G,H,I,J,K) -> f54(A,B,C,D,E,1,G,H,I,J,K) [-1*G >= 0 (?,1) && F + -1*G >= 0 && -1*F + -1*G >= 0 && 20 + -1*E + -1*G >= 0 && -1 + D + -1*G >= 0 && -20 + C + -1*G >= 0 && 20 + -1*C + -1*G >= 0 && -10 + B + -1*G >= 0 && 10 + -1*B + -1*G >= 0 && -3 + -1*G + J >= 0 && 19 + -1*A + -1*G >= 0 && G >= 0 && F + G >= 0 && -1*F + G >= 0 && 20 + -1*E + G >= 0 && -1 + D + G >= 0 && -20 + C + G >= 0 && 20 + -1*C + G >= 0 && -10 + B + G >= 0 && 10 + -1*B + G >= 0 && -3 + G + J >= 0 && 19 + -1*A + G >= 0 && -1*F >= 0 && 20 + -1*E + -1*F >= 0 && -1 + D + -1*F >= 0 && -20 + C + -1*F >= 0 && 20 + -1*C + -1*F >= 0 && -10 + B + -1*F >= 0 && 10 + -1*B + -1*F >= 0 && -3 + -1*F + J >= 0 && 19 + -1*A + -1*F >= 0 && F >= 0 && 20 + -1*E + F >= 0 && -1 + D + F >= 0 && -20 + C + F >= 0 && 20 + -1*C + F >= 0 && -10 + B + F >= 0 && 10 + -1*B + F >= 0 && -3 + F + J >= 0 && 19 + -1*A + F >= 0 && 20 + -1*E >= 0 && 19 + D + -1*E >= 0 && C + -1*E >= 0 && 40 + -1*C + -1*E >= 0 && 10 + B + -1*E >= 0 && 30 + -1*B + -1*E >= 0 && 17 + -1*E + J >= 0 && 39 + -1*A + -1*E >= 0 && -1 + -1*A + E >= 0 && -2 + -1*D + J >= 0 && -1 + D >= 0 && -21 + C + D >= 0 && 19 + -1*C + D >= 0 && -11 + B + D >= 0 && 9 + -1*B + D >= 0 && -4 + D + J >= 0 && 18 + -1*A + D >= 0 && 20 + -1*C >= 0 && 10 + B + -1*C >= 0 && 30 + -1*B + -1*C >= 0 && 17 + -1*C + J >= 0 && 39 + -1*A + -1*C >= 0 && -20 + C >= 0 && -30 + B + C >= 0 && -10 + -1*B + C >= 0 && -23 + C + J >= 0 && -1 + -1*A + C >= 0 && 10 + -1*B >= 0 && 7 + -1*B + J >= 0 && 29 + -1*A + -1*B >= 0 && -10 + B >= 0 && -13 + B + J >= 0 && 9 + -1*A + B >= 0 && -3 + J >= 0 && 16 + -1*A + J >= 0 && 19 + -1*A >= 0 && J >= 1 + A] 17. f43(A,B,C,D,E,F,G,H,I,J,K) -> f48(-1 + A,B,C,D,E,F,G,H,I,J,K) [-1*G >= 0 (?,1) && F + -1*G >= 0 && -1*F + -1*G >= 0 && 20 + -1*E + -1*G >= 0 && -1 + D + -1*G >= 0 && -20 + C + -1*G >= 0 && 20 + -1*C + -1*G >= 0 && -10 + B + -1*G >= 0 && 10 + -1*B + -1*G >= 0 && -3 + -1*G + J >= 0 && 20 + -1*A + -1*G >= 0 && G >= 0 && F + G >= 0 && -1*F + G >= 0 && 20 + -1*E + G >= 0 && -1 + D + G >= 0 && -20 + C + G >= 0 && 20 + -1*C + G >= 0 && -10 + B + G >= 0 && 10 + -1*B + G >= 0 && -3 + G + J >= 0 && 20 + -1*A + G >= 0 && -1*F >= 0 && 20 + -1*E + -1*F >= 0 && -1 + D + -1*F >= 0 && -20 + C + -1*F >= 0 && 20 + -1*C + -1*F >= 0 && -10 + B + -1*F >= 0 && 10 + -1*B + -1*F >= 0 && -3 + -1*F + J >= 0 && 20 + -1*A + -1*F >= 0 && F >= 0 && 20 + -1*E + F >= 0 && -1 + D + F >= 0 && -20 + C + F >= 0 && 20 + -1*C + F >= 0 && -10 + B + F >= 0 && 10 + -1*B + F >= 0 && -3 + F + J >= 0 && 20 + -1*A + F >= 0 && 20 + -1*E >= 0 && 19 + D + -1*E >= 0 && C + -1*E >= 0 && 40 + -1*C + -1*E >= 0 && 10 + B + -1*E >= 0 && 30 + -1*B + -1*E >= 0 && 17 + -1*E + J >= 0 && 40 + -1*A + -1*E >= 0 && -1*A + E >= 0 && -2 + -1*D + J >= 0 && -1 + D >= 0 && -21 + C + D >= 0 && 19 + -1*C + D >= 0 && -11 + B + D >= 0 && 9 + -1*B + D >= 0 && -4 + D + J >= 0 && 19 + -1*A + D >= 0 && 20 + -1*C >= 0 && 10 + B + -1*C >= 0 && 30 + -1*B + -1*C >= 0 && 17 + -1*C + J >= 0 && 40 + -1*A + -1*C >= 0 && -20 + C >= 0 && -30 + B + C >= 0 && -10 + -1*B + C >= 0 && -23 + C + J >= 0 && -1*A + C >= 0 && 10 + -1*B >= 0 && 7 + -1*B + J >= 0 && 30 + -1*A + -1*B >= 0 && -10 + B >= 0 && -13 + B + J >= 0 && 10 + -1*A + B >= 0 && -3 + J >= 0 && 17 + -1*A + J >= 0 && 20 + -1*A >= 0] 18. f11(A,B,C,D,E,F,G,H,I,J,K) -> f69(A,B,C,D,E,F,G,H,I,J,K) [G >= 0 (1,1) && F + G >= 0 && 1 + -1*F + G >= 0 && 20 + -1*E + G >= 0 && -1 + D + G >= 0 && -20 + C + G >= 0 && 20 + -1*C + G >= 0 && -10 + B + G >= 0 && 10 + -1*B + G >= 0 && 1 + -1*F >= 0 && 21 + -1*E + -1*F >= 0 && D + -1*F >= 0 && -19 + C + -1*F >= 0 && 21 + -1*C + -1*F >= 0 && -9 + B + -1*F >= 0 && 11 + -1*B + -1*F >= 0 && F >= 0 && 20 + -1*E + F >= 0 && -1 + D + F >= 0 && -20 + C + F >= 0 && 20 + -1*C + F >= 0 && -10 + B + F >= 0 && 10 + -1*B + F >= 0 && 20 + -1*E >= 0 && 19 + D + -1*E >= 0 && C + -1*E >= 0 && 40 + -1*C + -1*E >= 0 && 10 + B + -1*E >= 0 && 30 + -1*B + -1*E >= 0 && -1 + D >= 0 && -21 + C + D >= 0 && 19 + -1*C + D >= 0 && -11 + B + D >= 0 && 9 + -1*B + D >= 0 && 20 + -1*C >= 0 && 10 + B + -1*C >= 0 && 30 + -1*B + -1*C >= 0 && -20 + C >= 0 && -30 + B + C >= 0 && -10 + -1*B + C >= 0 && 10 + -1*B >= 0 && -10 + B >= 0 && G >= 1] Signature: {(f0,11);(f11,11);(f40,11);(f43,11);(f48,11);(f54,11);(f59,11);(f63,11);(f69,11)} Flow Graph: [0->{2,3,4,5},1->{5},2->{18},3->{18},4->{18},5->{6,7},6->{12,13},7->{8,17},8->{8,17},9->{9,15,16},10->{6} ,11->{7},12->{14},13->{0,14},14->{2,3,4,5},15->{11},16->{10},17->{9,15,16},18->{}] + 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,18] | `- p:[0,13,6,5,14,12,10,16,9,17,7,11,15,8] c: [16] | +- p:[0,13,6,5,14,12] c: [13] | | | `- p:[5,14,12,6] c: [5] | `- p:[7,11,15,9,17,8] c: [15] | +- p:[8] c: [] | `- p:[9] c: [] NO