YES * Step 1: TrivialSCCs YES + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f15(50,5,0,D,E,F,G,H,I,J,K,L,M) True (1,1) 1. f15(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f19(A,B,C,0,0,F,G,H,I,J,K,L,M) [C >= 0 (?,1) && -5 + B + C >= 0 && 5 + -1*B + C >= 0 && -50 + A + C >= 0 && 50 + -1*A + C >= 0 && 5 + -1*B >= 0 && -45 + A + -1*B >= 0 && 55 + -1*A + -1*B >= 0 && -5 + B >= 0 && -55 + A + B >= 0 && 45 + -1*A + B >= 0 && 50 + -1*A >= 0 && -50 + A >= 0 && B >= C] 2. f19(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f19(A,B,C,D + N,1 + E,F,G,H,I,J,K,L,M) [E >= 0 (?,1) && C + E >= 0 && -5 + B + E >= 0 && 5 + -1*B + E >= 0 && -50 + A + E >= 0 && 50 + -1*A + E >= 0 && C >= 0 && -5 + B + C >= 0 && 5 + -1*B + C >= 0 && -50 + A + C >= 0 && 50 + -1*A + C >= 0 && 5 + -1*B >= 0 && -45 + A + -1*B >= 0 && 55 + -1*A + -1*B >= 0 && -5 + B >= 0 && -55 + A + B >= 0 && 45 + -1*A + B >= 0 && 50 + -1*A >= 0 && -50 + A >= 0 && B >= E && E >= 1 + C] 3. f19(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f19(A,B,C,D + N,1 + E,F,G,H,I,J,K,L,M) [E >= 0 (?,1) && C + E >= 0 && -5 + B + E >= 0 && 5 + -1*B + E >= 0 && -50 + A + E >= 0 && 50 + -1*A + E >= 0 && C >= 0 && -5 + B + C >= 0 && 5 + -1*B + C >= 0 && -50 + A + C >= 0 && 50 + -1*A + C >= 0 && 5 + -1*B >= 0 && -45 + A + -1*B >= 0 && 55 + -1*A + -1*B >= 0 && -5 + B >= 0 && -55 + A + B >= 0 && 45 + -1*A + B >= 0 && 50 + -1*A >= 0 && -50 + A >= 0 && C >= 1 + E && B >= E] 4. f19(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f19(A,B,C,D + N,1 + C,F,G,H,I,J,K,L,M) [E >= 0 (?,1) && C + E >= 0 && -5 + B + E >= 0 && 5 + -1*B + E >= 0 && -50 + A + E >= 0 && 50 + -1*A + E >= 0 && C >= 0 && -5 + B + C >= 0 && 5 + -1*B + C >= 0 && -50 + A + C >= 0 && 50 + -1*A + C >= 0 && 5 + -1*B >= 0 && -45 + A + -1*B >= 0 && 55 + -1*A + -1*B >= 0 && -5 + B >= 0 && -55 + A + B >= 0 && 45 + -1*A + B >= 0 && 50 + -1*A >= 0 && -50 + A >= 0 && B >= E && C = E] 5. f33(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f36(A,B,C,D,E,F,G,1 + G,I,J,K,L,M) [G >= 0 (?,1) && -5 + F + G >= 0 && 5 + -1*F + G >= 0 && -6 + C + G >= 0 && -5 + B + G >= 0 && 5 + -1*B + G >= 0 && -50 + G + M >= 0 && 50 + G + -1*M >= 0 && -50 + A + G >= 0 && 50 + -1*A + G >= 0 && 5 + -1*F >= 0 && -1 + C + -1*F >= 0 && B + -1*F >= 0 && 10 + -1*B + -1*F >= 0 && -45 + -1*F + M >= 0 && 55 + -1*F + -1*M >= 0 && -45 + A + -1*F >= 0 && 55 + -1*A + -1*F >= 0 && -5 + F >= 0 && -11 + C + F >= 0 && -10 + B + F >= 0 && -1*B + F >= 0 && -55 + F + M >= 0 && 45 + F + -1*M >= 0 && -55 + A + F >= 0 && 45 + -1*A + F >= 0 && -6 + C >= 0 && -11 + B + C >= 0 && -1 + -1*B + C >= 0 && -56 + C + M >= 0 && 44 + C + -1*M >= 0 && -56 + A + C >= 0 && 44 + -1*A + C >= 0 && 5 + -1*B >= 0 && -45 + -1*B + M >= 0 && 55 + -1*B + -1*M >= 0 && -45 + A + -1*B >= 0 && 55 + -1*A + -1*B >= 0 && -5 + B >= 0 && -55 + B + M >= 0 && 45 + B + -1*M >= 0 && -55 + A + B >= 0 && 45 + -1*A + B >= 0 && 50 + -1*M >= 0 && A + -1*M >= 0 && 100 + -1*A + -1*M >= 0 && -50 + M >= 0 && -100 + A + M >= 0 && -1*A + M >= 0 && 50 + -1*A >= 0 && -50 + A >= 0 && F >= 1 + G] 6. f36(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f41(A,B,C,D,E,F,G,H,N,0,K,L,M) [-1 + H >= 0 (?,1) && -1 + G + H >= 0 && -1 + -1*G + H >= 0 && -6 + F + H >= 0 && 4 + -1*F + H >= 0 && -7 + C + H >= 0 && -6 + B + H >= 0 && 4 + -1*B + H >= 0 && -51 + H + M >= 0 && 49 + H + -1*M >= 0 && -51 + A + H >= 0 && 49 + -1*A + H >= 0 && 4 + -1*G >= 0 && -1 + F + -1*G >= 0 && 9 + -1*F + -1*G >= 0 && -2 + C + -1*G >= 0 && -1 + B + -1*G >= 0 && 9 + -1*B + -1*G >= 0 && -46 + -1*G + M >= 0 && 54 + -1*G + -1*M >= 0 && -46 + A + -1*G >= 0 && 54 + -1*A + -1*G >= 0 && G >= 0 && -5 + F + G >= 0 && 5 + -1*F + G >= 0 && -6 + C + G >= 0 && -5 + B + G >= 0 && 5 + -1*B + G >= 0 && -50 + G + M >= 0 && 50 + G + -1*M >= 0 && -50 + A + G >= 0 && 50 + -1*A + G >= 0 && 5 + -1*F >= 0 && -1 + C + -1*F >= 0 && B + -1*F >= 0 && 10 + -1*B + -1*F >= 0 && -45 + -1*F + M >= 0 && 55 + -1*F + -1*M >= 0 && -45 + A + -1*F >= 0 && 55 + -1*A + -1*F >= 0 && -5 + F >= 0 && -11 + C + F >= 0 && -10 + B + F >= 0 && -1*B + F >= 0 && -55 + F + M >= 0 && 45 + F + -1*M >= 0 && -55 + A + F >= 0 && 45 + -1*A + F >= 0 && -6 + C >= 0 && -11 + B + C >= 0 && -1 + -1*B + C >= 0 && -56 + C + M >= 0 && 44 + C + -1*M >= 0 && -56 + A + C >= 0 && 44 + -1*A + C >= 0 && 5 + -1*B >= 0 && -45 + -1*B + M >= 0 && 55 + -1*B + -1*M >= 0 && -45 + A + -1*B >= 0 && 55 + -1*A + -1*B >= 0 && -5 + B >= 0 && -55 + B + M >= 0 && 45 + B + -1*M >= 0 && -55 + A + B >= 0 && 45 + -1*A + B >= 0 && 50 + -1*M >= 0 && A + -1*M >= 0 && 100 + -1*A + -1*M >= 0 && -50 + M >= 0 && -100 + A + M >= 0 && -1*A + M >= 0 && 50 + -1*A >= 0 && -50 + A >= 0 && G >= 1 && F >= H] 7. f41(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f41(A,B,C,D,E,F,G,H,N,1 + J,K,L,M) [5 + -1*H >= 0 (?,1) && 4 + G + -1*H >= 0 && 9 + -1*G + -1*H >= 0 && F + -1*H >= 0 && 10 + -1*F + -1*H >= 0 && -1 + C + -1*H >= 0 && B + -1*H >= 0 && 10 + -1*B + -1*H >= 0 && -45 + -1*H + M >= 0 && 55 + -1*H + -1*M >= 0 && 5 + -1*H + J >= 0 && -45 + A + -1*H >= 0 && 55 + -1*A + -1*H >= 0 && -2 + H >= 0 && -3 + G + H >= 0 && -1 + -1*G + H >= 0 && -7 + F + H >= 0 && 3 + -1*F + H >= 0 && -8 + C + H >= 0 && -7 + B + H >= 0 && 3 + -1*B + H >= 0 && -52 + H + M >= 0 && 48 + H + -1*M >= 0 && -2 + H + J >= 0 && -52 + A + H >= 0 && 48 + -1*A + H >= 0 && 4 + -1*G >= 0 && -1 + F + -1*G >= 0 && 9 + -1*F + -1*G >= 0 && -2 + C + -1*G >= 0 && -1 + B + -1*G >= 0 && 9 + -1*B + -1*G >= 0 && -46 + -1*G + M >= 0 && 54 + -1*G + -1*M >= 0 && 4 + -1*G + J >= 0 && -46 + A + -1*G >= 0 && 54 + -1*A + -1*G >= 0 && -1 + G >= 0 && -6 + F + G >= 0 && 4 + -1*F + G >= 0 && -7 + C + G >= 0 && -6 + B + G >= 0 && 4 + -1*B + G >= 0 && -51 + G + M >= 0 && 49 + G + -1*M >= 0 && -1 + G + J >= 0 && -51 + A + G >= 0 && 49 + -1*A + G >= 0 && 5 + -1*F >= 0 && -1 + C + -1*F >= 0 && B + -1*F >= 0 && 10 + -1*B + -1*F >= 0 && -45 + -1*F + M >= 0 && 55 + -1*F + -1*M >= 0 && 5 + -1*F + J >= 0 && -45 + A + -1*F >= 0 && 55 + -1*A + -1*F >= 0 && -5 + F >= 0 && -11 + C + F >= 0 && -10 + B + F >= 0 && -1*B + F >= 0 && -55 + F + M >= 0 && 45 + F + -1*M >= 0 && -5 + F + J >= 0 && -55 + A + F >= 0 && 45 + -1*A + F >= 0 && -6 + C >= 0 && -11 + B + C >= 0 && -1 + -1*B + C >= 0 && -56 + C + M >= 0 && 44 + C + -1*M >= 0 && -6 + C + J >= 0 && -56 + A + C >= 0 && 44 + -1*A + C >= 0 && 5 + -1*B >= 0 && -45 + -1*B + M >= 0 && 55 + -1*B + -1*M >= 0 && 5 + -1*B + J >= 0 && -45 + A + -1*B >= 0 && 55 + -1*A + -1*B >= 0 && -5 + B >= 0 && -55 + B + M >= 0 && 45 + B + -1*M >= 0 && -5 + B + J >= 0 && -55 + A + B >= 0 && 45 + -1*A + B >= 0 && 50 + -1*M >= 0 && 50 + J + -1*M >= 0 && A + -1*M >= 0 && 100 + -1*A + -1*M >= 0 && -50 + M >= 0 && -50 + J + M >= 0 && -100 + A + M >= 0 && -1*A + M >= 0 && J >= 0 && -50 + A + J >= 0 && 50 + -1*A + J >= 0 && 50 + -1*A >= 0 && -50 + A >= 0 && G >= 1 + J] 8. f36(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f36(A,B,C,D,E,F,0,1 + H,N,J,K,L,M) [-1 + H >= 0 (?,1) && -1 + G + H >= 0 && -1 + -1*G + H >= 0 && -6 + F + H >= 0 && 4 + -1*F + H >= 0 && -7 + C + H >= 0 && -6 + B + H >= 0 && 4 + -1*B + H >= 0 && -51 + H + M >= 0 && 49 + H + -1*M >= 0 && -51 + A + H >= 0 && 49 + -1*A + H >= 0 && 4 + -1*G >= 0 && -1 + F + -1*G >= 0 && 9 + -1*F + -1*G >= 0 && -2 + C + -1*G >= 0 && -1 + B + -1*G >= 0 && 9 + -1*B + -1*G >= 0 && -46 + -1*G + M >= 0 && 54 + -1*G + -1*M >= 0 && -46 + A + -1*G >= 0 && 54 + -1*A + -1*G >= 0 && G >= 0 && -5 + F + G >= 0 && 5 + -1*F + G >= 0 && -6 + C + G >= 0 && -5 + B + G >= 0 && 5 + -1*B + G >= 0 && -50 + G + M >= 0 && 50 + G + -1*M >= 0 && -50 + A + G >= 0 && 50 + -1*A + G >= 0 && 5 + -1*F >= 0 && -1 + C + -1*F >= 0 && B + -1*F >= 0 && 10 + -1*B + -1*F >= 0 && -45 + -1*F + M >= 0 && 55 + -1*F + -1*M >= 0 && -45 + A + -1*F >= 0 && 55 + -1*A + -1*F >= 0 && -5 + F >= 0 && -11 + C + F >= 0 && -10 + B + F >= 0 && -1*B + F >= 0 && -55 + F + M >= 0 && 45 + F + -1*M >= 0 && -55 + A + F >= 0 && 45 + -1*A + F >= 0 && -6 + C >= 0 && -11 + B + C >= 0 && -1 + -1*B + C >= 0 && -56 + C + M >= 0 && 44 + C + -1*M >= 0 && -56 + A + C >= 0 && 44 + -1*A + C >= 0 && 5 + -1*B >= 0 && -45 + -1*B + M >= 0 && 55 + -1*B + -1*M >= 0 && -45 + A + -1*B >= 0 && 55 + -1*A + -1*B >= 0 && -5 + B >= 0 && -55 + B + M >= 0 && 45 + B + -1*M >= 0 && -55 + A + B >= 0 && 45 + -1*A + B >= 0 && 50 + -1*M >= 0 && A + -1*M >= 0 && 100 + -1*A + -1*M >= 0 && -50 + M >= 0 && -100 + A + M >= 0 && -1*A + M >= 0 && 50 + -1*A >= 0 && -50 + A >= 0 && F >= H && G = 0] 9. f50(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f54(A,B,C,D,E,F,G,H,N,0,K,L,M) [-1 + H >= 0 (?,1) && -1 + G + H >= 0 && -1 + -1*G + H >= 0 && -6 + F + H >= 0 && 4 + -1*F + H >= 0 && -7 + C + H >= 0 && -6 + B + H >= 0 && 4 + -1*B + H >= 0 && -51 + H + M >= 0 && 49 + H + -1*M >= 0 && -51 + A + H >= 0 && 49 + -1*A + H >= 0 && G >= 0 && -5 + F + G >= 0 && 5 + -1*F + G >= 0 && -6 + C + G >= 0 && -5 + B + G >= 0 && 5 + -1*B + G >= 0 && -50 + G + M >= 0 && 50 + G + -1*M >= 0 && -50 + A + G >= 0 && 50 + -1*A + G >= 0 && 5 + -1*F >= 0 && -1 + C + -1*F >= 0 && B + -1*F >= 0 && 10 + -1*B + -1*F >= 0 && -45 + -1*F + M >= 0 && 55 + -1*F + -1*M >= 0 && -45 + A + -1*F >= 0 && 55 + -1*A + -1*F >= 0 && -5 + F >= 0 && -11 + C + F >= 0 && -10 + B + F >= 0 && -1*B + F >= 0 && -55 + F + M >= 0 && 45 + F + -1*M >= 0 && -55 + A + F >= 0 && 45 + -1*A + F >= 0 && -6 + C >= 0 && -11 + B + C >= 0 && -1 + -1*B + C >= 0 && -56 + C + M >= 0 && 44 + C + -1*M >= 0 && -56 + A + C >= 0 && 44 + -1*A + C >= 0 && 5 + -1*B >= 0 && -45 + -1*B + M >= 0 && 55 + -1*B + -1*M >= 0 && -45 + A + -1*B >= 0 && 55 + -1*A + -1*B >= 0 && -5 + B >= 0 && -55 + B + M >= 0 && 45 + B + -1*M >= 0 && -55 + A + B >= 0 && 45 + -1*A + B >= 0 && 50 + -1*M >= 0 && A + -1*M >= 0 && 100 + -1*A + -1*M >= 0 && -50 + M >= 0 && -100 + A + M >= 0 && -1*A + M >= 0 && 50 + -1*A >= 0 && -50 + A >= 0 && F >= H] 10. f54(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f54(A,B,C,D,E,F,G,H,N,1 + J,K,L,M) [-1 + H >= 0 (?,1) && -1 + G + H >= 0 && -1 + -1*G + H >= 0 && -6 + F + H >= 0 && 4 + -1*F + H >= 0 && -7 + C + H >= 0 && -6 + B + H >= 0 && 4 + -1*B + H >= 0 && -51 + H + M >= 0 && 49 + H + -1*M >= 0 && -1 + H + J >= 0 && -51 + A + H >= 0 && 49 + -1*A + H >= 0 && 4 + -1*G >= 0 && -1 + F + -1*G >= 0 && 9 + -1*F + -1*G >= 0 && -2 + C + -1*G >= 0 && -1 + B + -1*G >= 0 && 9 + -1*B + -1*G >= 0 && -46 + -1*G + M >= 0 && 54 + -1*G + -1*M >= 0 && 4 + -1*G + J >= 0 && -46 + A + -1*G >= 0 && 54 + -1*A + -1*G >= 0 && G >= 0 && -5 + F + G >= 0 && 5 + -1*F + G >= 0 && -6 + C + G >= 0 && -5 + B + G >= 0 && 5 + -1*B + G >= 0 && -50 + G + M >= 0 && 50 + G + -1*M >= 0 && G + J >= 0 && -50 + A + G >= 0 && 50 + -1*A + G >= 0 && 5 + -1*F >= 0 && -1 + C + -1*F >= 0 && B + -1*F >= 0 && 10 + -1*B + -1*F >= 0 && -45 + -1*F + M >= 0 && 55 + -1*F + -1*M >= 0 && 5 + -1*F + J >= 0 && -45 + A + -1*F >= 0 && 55 + -1*A + -1*F >= 0 && -5 + F >= 0 && -11 + C + F >= 0 && -10 + B + F >= 0 && -1*B + F >= 0 && -55 + F + M >= 0 && 45 + F + -1*M >= 0 && -5 + F + J >= 0 && -55 + A + F >= 0 && 45 + -1*A + F >= 0 && -6 + C >= 0 && -11 + B + C >= 0 && -1 + -1*B + C >= 0 && -56 + C + M >= 0 && 44 + C + -1*M >= 0 && -6 + C + J >= 0 && -56 + A + C >= 0 && 44 + -1*A + C >= 0 && 5 + -1*B >= 0 && -45 + -1*B + M >= 0 && 55 + -1*B + -1*M >= 0 && 5 + -1*B + J >= 0 && -45 + A + -1*B >= 0 && 55 + -1*A + -1*B >= 0 && -5 + B >= 0 && -55 + B + M >= 0 && 45 + B + -1*M >= 0 && -5 + B + J >= 0 && -55 + A + B >= 0 && 45 + -1*A + B >= 0 && 50 + -1*M >= 0 && 50 + J + -1*M >= 0 && A + -1*M >= 0 && 100 + -1*A + -1*M >= 0 && -50 + M >= 0 && -50 + J + M >= 0 && -100 + A + M >= 0 && -1*A + M >= 0 && J >= 0 && -50 + A + J >= 0 && 50 + -1*A + J >= 0 && 50 + -1*A >= 0 && -50 + A >= 0 && G >= J] 11. f66(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f70(A,B,C,D,E,F,G,0,N,J,K,L,M) [-1 + G >= 0 (?,1) && -6 + F + G >= 0 && 4 + -1*F + G >= 0 && -7 + C + G >= 0 && -6 + B + G >= 0 && 4 + -1*B + G >= 0 && -51 + G + M >= 0 && 49 + G + -1*M >= 0 && -51 + A + G >= 0 && 49 + -1*A + G >= 0 && 5 + -1*F >= 0 && -1 + C + -1*F >= 0 && B + -1*F >= 0 && 10 + -1*B + -1*F >= 0 && -45 + -1*F + M >= 0 && 55 + -1*F + -1*M >= 0 && -45 + A + -1*F >= 0 && 55 + -1*A + -1*F >= 0 && -5 + F >= 0 && -11 + C + F >= 0 && -10 + B + F >= 0 && -1*B + F >= 0 && -55 + F + M >= 0 && 45 + F + -1*M >= 0 && -55 + A + F >= 0 && 45 + -1*A + F >= 0 && -6 + C >= 0 && -11 + B + C >= 0 && -1 + -1*B + C >= 0 && -56 + C + M >= 0 && 44 + C + -1*M >= 0 && -56 + A + C >= 0 && 44 + -1*A + C >= 0 && 5 + -1*B >= 0 && -45 + -1*B + M >= 0 && 55 + -1*B + -1*M >= 0 && -45 + A + -1*B >= 0 && 55 + -1*A + -1*B >= 0 && -5 + B >= 0 && -55 + B + M >= 0 && 45 + B + -1*M >= 0 && -55 + A + B >= 0 && 45 + -1*A + B >= 0 && 50 + -1*M >= 0 && A + -1*M >= 0 && 100 + -1*A + -1*M >= 0 && -50 + M >= 0 && -100 + A + M >= 0 && -1*A + M >= 0 && 50 + -1*A >= 0 && -50 + A >= 0 && F >= G] 12. f70(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f70(A,B,C,D,E,F,G,1 + H,N,J,K,L,M) [H >= 0 (?,1) && -1 + G + H >= 0 && -5 + F + H >= 0 && 5 + -1*F + H >= 0 && -6 + C + H >= 0 && -5 + B + H >= 0 && 5 + -1*B + H >= 0 && -50 + H + M >= 0 && 50 + H + -1*M >= 0 && -50 + A + H >= 0 && 50 + -1*A + H >= 0 && -1 + G >= 0 && -6 + F + G >= 0 && 4 + -1*F + G >= 0 && -7 + C + G >= 0 && -6 + B + G >= 0 && 4 + -1*B + G >= 0 && -51 + G + M >= 0 && 49 + G + -1*M >= 0 && -51 + A + G >= 0 && 49 + -1*A + G >= 0 && 5 + -1*F >= 0 && -1 + C + -1*F >= 0 && B + -1*F >= 0 && 10 + -1*B + -1*F >= 0 && -45 + -1*F + M >= 0 && 55 + -1*F + -1*M >= 0 && -45 + A + -1*F >= 0 && 55 + -1*A + -1*F >= 0 && -5 + F >= 0 && -11 + C + F >= 0 && -10 + B + F >= 0 && -1*B + F >= 0 && -55 + F + M >= 0 && 45 + F + -1*M >= 0 && -55 + A + F >= 0 && 45 + -1*A + F >= 0 && -6 + C >= 0 && -11 + B + C >= 0 && -1 + -1*B + C >= 0 && -56 + C + M >= 0 && 44 + C + -1*M >= 0 && -56 + A + C >= 0 && 44 + -1*A + C >= 0 && 5 + -1*B >= 0 && -45 + -1*B + M >= 0 && 55 + -1*B + -1*M >= 0 && -45 + A + -1*B >= 0 && 55 + -1*A + -1*B >= 0 && -5 + B >= 0 && -55 + B + M >= 0 && 45 + B + -1*M >= 0 && -55 + A + B >= 0 && 45 + -1*A + B >= 0 && 50 + -1*M >= 0 && A + -1*M >= 0 && 100 + -1*A + -1*M >= 0 && -50 + M >= 0 && -100 + A + M >= 0 && -1*A + M >= 0 && 50 + -1*A >= 0 && -50 + A >= 0 && G >= 1 + H] 13. f80(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f84(A,B,C,D,E,F,G,1 + G,N,J,K,L,M) [4 + -1*G >= 0 (?,1) && -1 + F + -1*G >= 0 && 9 + -1*F + -1*G >= 0 && -2 + C + -1*G >= 0 && -1 + B + -1*G >= 0 && 9 + -1*B + -1*G >= 0 && -46 + -1*G + M >= 0 && 54 + -1*G + -1*M >= 0 && -46 + A + -1*G >= 0 && 54 + -1*A + -1*G >= 0 && 5 + -1*F >= 0 && -1 + C + -1*F >= 0 && B + -1*F >= 0 && 10 + -1*B + -1*F >= 0 && -45 + -1*F + M >= 0 && 55 + -1*F + -1*M >= 0 && -45 + A + -1*F >= 0 && 55 + -1*A + -1*F >= 0 && -5 + F >= 0 && -11 + C + F >= 0 && -10 + B + F >= 0 && -1*B + F >= 0 && -55 + F + M >= 0 && 45 + F + -1*M >= 0 && -55 + A + F >= 0 && 45 + -1*A + F >= 0 && -6 + C >= 0 && -11 + B + C >= 0 && -1 + -1*B + C >= 0 && -56 + C + M >= 0 && 44 + C + -1*M >= 0 && -56 + A + C >= 0 && 44 + -1*A + C >= 0 && 5 + -1*B >= 0 && -45 + -1*B + M >= 0 && 55 + -1*B + -1*M >= 0 && -45 + A + -1*B >= 0 && 55 + -1*A + -1*B >= 0 && -5 + B >= 0 && -55 + B + M >= 0 && 45 + B + -1*M >= 0 && -55 + A + B >= 0 && 45 + -1*A + B >= 0 && 50 + -1*M >= 0 && A + -1*M >= 0 && 100 + -1*A + -1*M >= 0 && -50 + M >= 0 && -100 + A + M >= 0 && -1*A + M >= 0 && 50 + -1*A >= 0 && -50 + A >= 0 && G >= 0] 14. f84(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f84(A,B,C,D,E,F,G,1 + H,N,J,K,L,M) [-1 + -1*G + H >= 0 (?,1) && 4 + -1*G >= 0 && -1 + F + -1*G >= 0 && 9 + -1*F + -1*G >= 0 && -2 + C + -1*G >= 0 && -1 + B + -1*G >= 0 && 9 + -1*B + -1*G >= 0 && -46 + -1*G + M >= 0 && 54 + -1*G + -1*M >= 0 && -46 + A + -1*G >= 0 && 54 + -1*A + -1*G >= 0 && 5 + -1*F >= 0 && -1 + C + -1*F >= 0 && B + -1*F >= 0 && 10 + -1*B + -1*F >= 0 && -45 + -1*F + M >= 0 && 55 + -1*F + -1*M >= 0 && -45 + A + -1*F >= 0 && 55 + -1*A + -1*F >= 0 && -5 + F >= 0 && -11 + C + F >= 0 && -10 + B + F >= 0 && -1*B + F >= 0 && -55 + F + M >= 0 && 45 + F + -1*M >= 0 && -55 + A + F >= 0 && 45 + -1*A + F >= 0 && -6 + C >= 0 && -11 + B + C >= 0 && -1 + -1*B + C >= 0 && -56 + C + M >= 0 && 44 + C + -1*M >= 0 && -56 + A + C >= 0 && 44 + -1*A + C >= 0 && 5 + -1*B >= 0 && -45 + -1*B + M >= 0 && 55 + -1*B + -1*M >= 0 && -45 + A + -1*B >= 0 && 55 + -1*A + -1*B >= 0 && -5 + B >= 0 && -55 + B + M >= 0 && 45 + B + -1*M >= 0 && -55 + A + B >= 0 && 45 + -1*A + B >= 0 && 50 + -1*M >= 0 && A + -1*M >= 0 && 100 + -1*A + -1*M >= 0 && -50 + M >= 0 && -100 + A + M >= 0 && -1*A + M >= 0 && 50 + -1*A >= 0 && -50 + A >= 0 && F >= H] 15. f84(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f80(A,B,C,D,E,F,-1 + G,H,I,J,K,L,M) [-1 + -1*G + H >= 0 (?,1) && 4 + -1*G >= 0 && -1 + F + -1*G >= 0 && 9 + -1*F + -1*G >= 0 && -2 + C + -1*G >= 0 && -1 + B + -1*G >= 0 && 9 + -1*B + -1*G >= 0 && -46 + -1*G + M >= 0 && 54 + -1*G + -1*M >= 0 && -46 + A + -1*G >= 0 && 54 + -1*A + -1*G >= 0 && 5 + -1*F >= 0 && -1 + C + -1*F >= 0 && B + -1*F >= 0 && 10 + -1*B + -1*F >= 0 && -45 + -1*F + M >= 0 && 55 + -1*F + -1*M >= 0 && -45 + A + -1*F >= 0 && 55 + -1*A + -1*F >= 0 && -5 + F >= 0 && -11 + C + F >= 0 && -10 + B + F >= 0 && -1*B + F >= 0 && -55 + F + M >= 0 && 45 + F + -1*M >= 0 && -55 + A + F >= 0 && 45 + -1*A + F >= 0 && -6 + C >= 0 && -11 + B + C >= 0 && -1 + -1*B + C >= 0 && -56 + C + M >= 0 && 44 + C + -1*M >= 0 && -56 + A + C >= 0 && 44 + -1*A + C >= 0 && 5 + -1*B >= 0 && -45 + -1*B + M >= 0 && 55 + -1*B + -1*M >= 0 && -45 + A + -1*B >= 0 && 55 + -1*A + -1*B >= 0 && -5 + B >= 0 && -55 + B + M >= 0 && 45 + B + -1*M >= 0 && -55 + A + B >= 0 && 45 + -1*A + B >= 0 && 50 + -1*M >= 0 && A + -1*M >= 0 && 100 + -1*A + -1*M >= 0 && -50 + M >= 0 && -100 + A + M >= 0 && -1*A + M >= 0 && 50 + -1*A >= 0 && -50 + A >= 0 && H >= 1 + F] 16. f80(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f96(A,B,C,D,E,F,G,H,I,J,0,0,M) [4 + -1*G >= 0 (?,1) && -1 + F + -1*G >= 0 && 9 + -1*F + -1*G >= 0 && -2 + C + -1*G >= 0 && -1 + B + -1*G >= 0 && 9 + -1*B + -1*G >= 0 && -46 + -1*G + M >= 0 && 54 + -1*G + -1*M >= 0 && -46 + A + -1*G >= 0 && 54 + -1*A + -1*G >= 0 && 5 + -1*F >= 0 && -1 + C + -1*F >= 0 && B + -1*F >= 0 && 10 + -1*B + -1*F >= 0 && -45 + -1*F + M >= 0 && 55 + -1*F + -1*M >= 0 && -45 + A + -1*F >= 0 && 55 + -1*A + -1*F >= 0 && -5 + F >= 0 && -11 + C + F >= 0 && -10 + B + F >= 0 && -1*B + F >= 0 && -55 + F + M >= 0 && 45 + F + -1*M >= 0 && -55 + A + F >= 0 && 45 + -1*A + F >= 0 && -6 + C >= 0 && -11 + B + C >= 0 && -1 + -1*B + C >= 0 && -56 + C + M >= 0 && 44 + C + -1*M >= 0 && -56 + A + C >= 0 && 44 + -1*A + C >= 0 && 5 + -1*B >= 0 && -45 + -1*B + M >= 0 && 55 + -1*B + -1*M >= 0 && -45 + A + -1*B >= 0 && 55 + -1*A + -1*B >= 0 && -5 + B >= 0 && -55 + B + M >= 0 && 45 + B + -1*M >= 0 && -55 + A + B >= 0 && 45 + -1*A + B >= 0 && 50 + -1*M >= 0 && A + -1*M >= 0 && 100 + -1*A + -1*M >= 0 && -50 + M >= 0 && -100 + A + M >= 0 && -1*A + M >= 0 && 50 + -1*A >= 0 && -50 + A >= 0 && 0 >= 1 + G] 17. f70(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f66(A,B,C,D,E,F,1 + G,H,I,J,K,L,M) [H >= 0 (?,1) && -1 + G + H >= 0 && -5 + F + H >= 0 && 5 + -1*F + H >= 0 && -6 + C + H >= 0 && -5 + B + H >= 0 && 5 + -1*B + H >= 0 && -50 + H + M >= 0 && 50 + H + -1*M >= 0 && -50 + A + H >= 0 && 50 + -1*A + H >= 0 && -1 + G >= 0 && -6 + F + G >= 0 && 4 + -1*F + G >= 0 && -7 + C + G >= 0 && -6 + B + G >= 0 && 4 + -1*B + G >= 0 && -51 + G + M >= 0 && 49 + G + -1*M >= 0 && -51 + A + G >= 0 && 49 + -1*A + G >= 0 && 5 + -1*F >= 0 && -1 + C + -1*F >= 0 && B + -1*F >= 0 && 10 + -1*B + -1*F >= 0 && -45 + -1*F + M >= 0 && 55 + -1*F + -1*M >= 0 && -45 + A + -1*F >= 0 && 55 + -1*A + -1*F >= 0 && -5 + F >= 0 && -11 + C + F >= 0 && -10 + B + F >= 0 && -1*B + F >= 0 && -55 + F + M >= 0 && 45 + F + -1*M >= 0 && -55 + A + F >= 0 && 45 + -1*A + F >= 0 && -6 + C >= 0 && -11 + B + C >= 0 && -1 + -1*B + C >= 0 && -56 + C + M >= 0 && 44 + C + -1*M >= 0 && -56 + A + C >= 0 && 44 + -1*A + C >= 0 && 5 + -1*B >= 0 && -45 + -1*B + M >= 0 && 55 + -1*B + -1*M >= 0 && -45 + A + -1*B >= 0 && 55 + -1*A + -1*B >= 0 && -5 + B >= 0 && -55 + B + M >= 0 && 45 + B + -1*M >= 0 && -55 + A + B >= 0 && 45 + -1*A + B >= 0 && 50 + -1*M >= 0 && A + -1*M >= 0 && 100 + -1*A + -1*M >= 0 && -50 + M >= 0 && -100 + A + M >= 0 && -1*A + M >= 0 && 50 + -1*A >= 0 && -50 + A >= 0 && H >= G] 18. f66(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f80(A,B,C,D,E,F,-1 + F,H,I,J,K,L,M) [-1 + G >= 0 (?,1) && -6 + F + G >= 0 && 4 + -1*F + G >= 0 && -7 + C + G >= 0 && -6 + B + G >= 0 && 4 + -1*B + G >= 0 && -51 + G + M >= 0 && 49 + G + -1*M >= 0 && -51 + A + G >= 0 && 49 + -1*A + G >= 0 && 5 + -1*F >= 0 && -1 + C + -1*F >= 0 && B + -1*F >= 0 && 10 + -1*B + -1*F >= 0 && -45 + -1*F + M >= 0 && 55 + -1*F + -1*M >= 0 && -45 + A + -1*F >= 0 && 55 + -1*A + -1*F >= 0 && -5 + F >= 0 && -11 + C + F >= 0 && -10 + B + F >= 0 && -1*B + F >= 0 && -55 + F + M >= 0 && 45 + F + -1*M >= 0 && -55 + A + F >= 0 && 45 + -1*A + F >= 0 && -6 + C >= 0 && -11 + B + C >= 0 && -1 + -1*B + C >= 0 && -56 + C + M >= 0 && 44 + C + -1*M >= 0 && -56 + A + C >= 0 && 44 + -1*A + C >= 0 && 5 + -1*B >= 0 && -45 + -1*B + M >= 0 && 55 + -1*B + -1*M >= 0 && -45 + A + -1*B >= 0 && 55 + -1*A + -1*B >= 0 && -5 + B >= 0 && -55 + B + M >= 0 && 45 + B + -1*M >= 0 && -55 + A + B >= 0 && 45 + -1*A + B >= 0 && 50 + -1*M >= 0 && A + -1*M >= 0 && 100 + -1*A + -1*M >= 0 && -50 + M >= 0 && -100 + A + M >= 0 && -1*A + M >= 0 && 50 + -1*A >= 0 && -50 + A >= 0 && G >= 1 + F] 19. f54(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f50(A,B,C,D,E,F,G,1 + H,I,J,K,L,M) [-1 + H >= 0 (?,1) && -1 + G + H >= 0 && -1 + -1*G + H >= 0 && -6 + F + H >= 0 && 4 + -1*F + H >= 0 && -7 + C + H >= 0 && -6 + B + H >= 0 && 4 + -1*B + H >= 0 && -51 + H + M >= 0 && 49 + H + -1*M >= 0 && -1 + H + J >= 0 && -51 + A + H >= 0 && 49 + -1*A + H >= 0 && 4 + -1*G >= 0 && -1 + F + -1*G >= 0 && 9 + -1*F + -1*G >= 0 && -2 + C + -1*G >= 0 && -1 + B + -1*G >= 0 && 9 + -1*B + -1*G >= 0 && -46 + -1*G + M >= 0 && 54 + -1*G + -1*M >= 0 && 4 + -1*G + J >= 0 && -46 + A + -1*G >= 0 && 54 + -1*A + -1*G >= 0 && G >= 0 && -5 + F + G >= 0 && 5 + -1*F + G >= 0 && -6 + C + G >= 0 && -5 + B + G >= 0 && 5 + -1*B + G >= 0 && -50 + G + M >= 0 && 50 + G + -1*M >= 0 && G + J >= 0 && -50 + A + G >= 0 && 50 + -1*A + G >= 0 && 5 + -1*F >= 0 && -1 + C + -1*F >= 0 && B + -1*F >= 0 && 10 + -1*B + -1*F >= 0 && -45 + -1*F + M >= 0 && 55 + -1*F + -1*M >= 0 && 5 + -1*F + J >= 0 && -45 + A + -1*F >= 0 && 55 + -1*A + -1*F >= 0 && -5 + F >= 0 && -11 + C + F >= 0 && -10 + B + F >= 0 && -1*B + F >= 0 && -55 + F + M >= 0 && 45 + F + -1*M >= 0 && -5 + F + J >= 0 && -55 + A + F >= 0 && 45 + -1*A + F >= 0 && -6 + C >= 0 && -11 + B + C >= 0 && -1 + -1*B + C >= 0 && -56 + C + M >= 0 && 44 + C + -1*M >= 0 && -6 + C + J >= 0 && -56 + A + C >= 0 && 44 + -1*A + C >= 0 && 5 + -1*B >= 0 && -45 + -1*B + M >= 0 && 55 + -1*B + -1*M >= 0 && 5 + -1*B + J >= 0 && -45 + A + -1*B >= 0 && 55 + -1*A + -1*B >= 0 && -5 + B >= 0 && -55 + B + M >= 0 && 45 + B + -1*M >= 0 && -5 + B + J >= 0 && -55 + A + B >= 0 && 45 + -1*A + B >= 0 && 50 + -1*M >= 0 && 50 + J + -1*M >= 0 && A + -1*M >= 0 && 100 + -1*A + -1*M >= 0 && -50 + M >= 0 && -50 + J + M >= 0 && -100 + A + M >= 0 && -1*A + M >= 0 && J >= 0 && -50 + A + J >= 0 && 50 + -1*A + J >= 0 && 50 + -1*A >= 0 && -50 + A >= 0 && J >= 1 + G] 20. f50(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f33(A,B,C,D,E,F,1 + G,H,I,J,K,L,M) [-1 + H >= 0 (?,1) && -1 + G + H >= 0 && -1 + -1*G + H >= 0 && -6 + F + H >= 0 && 4 + -1*F + H >= 0 && -7 + C + H >= 0 && -6 + B + H >= 0 && 4 + -1*B + H >= 0 && -51 + H + M >= 0 && 49 + H + -1*M >= 0 && -51 + A + H >= 0 && 49 + -1*A + H >= 0 && G >= 0 && -5 + F + G >= 0 && 5 + -1*F + G >= 0 && -6 + C + G >= 0 && -5 + B + G >= 0 && 5 + -1*B + G >= 0 && -50 + G + M >= 0 && 50 + G + -1*M >= 0 && -50 + A + G >= 0 && 50 + -1*A + G >= 0 && 5 + -1*F >= 0 && -1 + C + -1*F >= 0 && B + -1*F >= 0 && 10 + -1*B + -1*F >= 0 && -45 + -1*F + M >= 0 && 55 + -1*F + -1*M >= 0 && -45 + A + -1*F >= 0 && 55 + -1*A + -1*F >= 0 && -5 + F >= 0 && -11 + C + F >= 0 && -10 + B + F >= 0 && -1*B + F >= 0 && -55 + F + M >= 0 && 45 + F + -1*M >= 0 && -55 + A + F >= 0 && 45 + -1*A + F >= 0 && -6 + C >= 0 && -11 + B + C >= 0 && -1 + -1*B + C >= 0 && -56 + C + M >= 0 && 44 + C + -1*M >= 0 && -56 + A + C >= 0 && 44 + -1*A + C >= 0 && 5 + -1*B >= 0 && -45 + -1*B + M >= 0 && 55 + -1*B + -1*M >= 0 && -45 + A + -1*B >= 0 && 55 + -1*A + -1*B >= 0 && -5 + B >= 0 && -55 + B + M >= 0 && 45 + B + -1*M >= 0 && -55 + A + B >= 0 && 45 + -1*A + B >= 0 && 50 + -1*M >= 0 && A + -1*M >= 0 && 100 + -1*A + -1*M >= 0 && -50 + M >= 0 && -100 + A + M >= 0 && -1*A + M >= 0 && 50 + -1*A >= 0 && -50 + A >= 0 && H >= 1 + F] 21. f41(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f36(A,B,C,D,E,F,G,1 + H,I,J,K,L,M) [5 + -1*H >= 0 (?,1) && 4 + G + -1*H >= 0 && 9 + -1*G + -1*H >= 0 && F + -1*H >= 0 && 10 + -1*F + -1*H >= 0 && -1 + C + -1*H >= 0 && B + -1*H >= 0 && 10 + -1*B + -1*H >= 0 && -45 + -1*H + M >= 0 && 55 + -1*H + -1*M >= 0 && 5 + -1*H + J >= 0 && -45 + A + -1*H >= 0 && 55 + -1*A + -1*H >= 0 && -2 + H >= 0 && -3 + G + H >= 0 && -1 + -1*G + H >= 0 && -7 + F + H >= 0 && 3 + -1*F + H >= 0 && -8 + C + H >= 0 && -7 + B + H >= 0 && 3 + -1*B + H >= 0 && -52 + H + M >= 0 && 48 + H + -1*M >= 0 && -2 + H + J >= 0 && -52 + A + H >= 0 && 48 + -1*A + H >= 0 && 4 + -1*G >= 0 && -1 + F + -1*G >= 0 && 9 + -1*F + -1*G >= 0 && -2 + C + -1*G >= 0 && -1 + B + -1*G >= 0 && 9 + -1*B + -1*G >= 0 && -46 + -1*G + M >= 0 && 54 + -1*G + -1*M >= 0 && 4 + -1*G + J >= 0 && -46 + A + -1*G >= 0 && 54 + -1*A + -1*G >= 0 && -1 + G >= 0 && -6 + F + G >= 0 && 4 + -1*F + G >= 0 && -7 + C + G >= 0 && -6 + B + G >= 0 && 4 + -1*B + G >= 0 && -51 + G + M >= 0 && 49 + G + -1*M >= 0 && -1 + G + J >= 0 && -51 + A + G >= 0 && 49 + -1*A + G >= 0 && 5 + -1*F >= 0 && -1 + C + -1*F >= 0 && B + -1*F >= 0 && 10 + -1*B + -1*F >= 0 && -45 + -1*F + M >= 0 && 55 + -1*F + -1*M >= 0 && 5 + -1*F + J >= 0 && -45 + A + -1*F >= 0 && 55 + -1*A + -1*F >= 0 && -5 + F >= 0 && -11 + C + F >= 0 && -10 + B + F >= 0 && -1*B + F >= 0 && -55 + F + M >= 0 && 45 + F + -1*M >= 0 && -5 + F + J >= 0 && -55 + A + F >= 0 && 45 + -1*A + F >= 0 && -6 + C >= 0 && -11 + B + C >= 0 && -1 + -1*B + C >= 0 && -56 + C + M >= 0 && 44 + C + -1*M >= 0 && -6 + C + J >= 0 && -56 + A + C >= 0 && 44 + -1*A + C >= 0 && 5 + -1*B >= 0 && -45 + -1*B + M >= 0 && 55 + -1*B + -1*M >= 0 && 5 + -1*B + J >= 0 && -45 + A + -1*B >= 0 && 55 + -1*A + -1*B >= 0 && -5 + B >= 0 && -55 + B + M >= 0 && 45 + B + -1*M >= 0 && -5 + B + J >= 0 && -55 + A + B >= 0 && 45 + -1*A + B >= 0 && 50 + -1*M >= 0 && 50 + J + -1*M >= 0 && A + -1*M >= 0 && 100 + -1*A + -1*M >= 0 && -50 + M >= 0 && -50 + J + M >= 0 && -100 + A + M >= 0 && -1*A + M >= 0 && J >= 0 && -50 + A + J >= 0 && 50 + -1*A + J >= 0 && 50 + -1*A >= 0 && -50 + A >= 0 && J >= G] 22. f36(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f50(A,B,C,D,E,F,G,1 + G,I,J,K,L,M) [-1 + H >= 0 (?,1) && -1 + G + H >= 0 && -1 + -1*G + H >= 0 && -6 + F + H >= 0 && 4 + -1*F + H >= 0 && -7 + C + H >= 0 && -6 + B + H >= 0 && 4 + -1*B + H >= 0 && -51 + H + M >= 0 && 49 + H + -1*M >= 0 && -51 + A + H >= 0 && 49 + -1*A + H >= 0 && 4 + -1*G >= 0 && -1 + F + -1*G >= 0 && 9 + -1*F + -1*G >= 0 && -2 + C + -1*G >= 0 && -1 + B + -1*G >= 0 && 9 + -1*B + -1*G >= 0 && -46 + -1*G + M >= 0 && 54 + -1*G + -1*M >= 0 && -46 + A + -1*G >= 0 && 54 + -1*A + -1*G >= 0 && G >= 0 && -5 + F + G >= 0 && 5 + -1*F + G >= 0 && -6 + C + G >= 0 && -5 + B + G >= 0 && 5 + -1*B + G >= 0 && -50 + G + M >= 0 && 50 + G + -1*M >= 0 && -50 + A + G >= 0 && 50 + -1*A + G >= 0 && 5 + -1*F >= 0 && -1 + C + -1*F >= 0 && B + -1*F >= 0 && 10 + -1*B + -1*F >= 0 && -45 + -1*F + M >= 0 && 55 + -1*F + -1*M >= 0 && -45 + A + -1*F >= 0 && 55 + -1*A + -1*F >= 0 && -5 + F >= 0 && -11 + C + F >= 0 && -10 + B + F >= 0 && -1*B + F >= 0 && -55 + F + M >= 0 && 45 + F + -1*M >= 0 && -55 + A + F >= 0 && 45 + -1*A + F >= 0 && -6 + C >= 0 && -11 + B + C >= 0 && -1 + -1*B + C >= 0 && -56 + C + M >= 0 && 44 + C + -1*M >= 0 && -56 + A + C >= 0 && 44 + -1*A + C >= 0 && 5 + -1*B >= 0 && -45 + -1*B + M >= 0 && 55 + -1*B + -1*M >= 0 && -45 + A + -1*B >= 0 && 55 + -1*A + -1*B >= 0 && -5 + B >= 0 && -55 + B + M >= 0 && 45 + B + -1*M >= 0 && -55 + A + B >= 0 && 45 + -1*A + B >= 0 && 50 + -1*M >= 0 && A + -1*M >= 0 && 100 + -1*A + -1*M >= 0 && -50 + M >= 0 && -100 + A + M >= 0 && -1*A + M >= 0 && 50 + -1*A >= 0 && -50 + A >= 0 && H >= 1 + F] 23. f33(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f66(A,B,C,D,E,F,1,H,I,J,K,L,M) [G >= 0 (?,1) && -5 + F + G >= 0 && 5 + -1*F + G >= 0 && -6 + C + G >= 0 && -5 + B + G >= 0 && 5 + -1*B + G >= 0 && -50 + G + M >= 0 && 50 + G + -1*M >= 0 && -50 + A + G >= 0 && 50 + -1*A + G >= 0 && 5 + -1*F >= 0 && -1 + C + -1*F >= 0 && B + -1*F >= 0 && 10 + -1*B + -1*F >= 0 && -45 + -1*F + M >= 0 && 55 + -1*F + -1*M >= 0 && -45 + A + -1*F >= 0 && 55 + -1*A + -1*F >= 0 && -5 + F >= 0 && -11 + C + F >= 0 && -10 + B + F >= 0 && -1*B + F >= 0 && -55 + F + M >= 0 && 45 + F + -1*M >= 0 && -55 + A + F >= 0 && 45 + -1*A + F >= 0 && -6 + C >= 0 && -11 + B + C >= 0 && -1 + -1*B + C >= 0 && -56 + C + M >= 0 && 44 + C + -1*M >= 0 && -56 + A + C >= 0 && 44 + -1*A + C >= 0 && 5 + -1*B >= 0 && -45 + -1*B + M >= 0 && 55 + -1*B + -1*M >= 0 && -45 + A + -1*B >= 0 && 55 + -1*A + -1*B >= 0 && -5 + B >= 0 && -55 + B + M >= 0 && 45 + B + -1*M >= 0 && -55 + A + B >= 0 && 45 + -1*A + B >= 0 && 50 + -1*M >= 0 && A + -1*M >= 0 && 100 + -1*A + -1*M >= 0 && -50 + M >= 0 && -100 + A + M >= 0 && -1*A + M >= 0 && 50 + -1*A >= 0 && -50 + A >= 0 && G >= F] 24. f19(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f15(A,B,1 + C,D,E,F,G,H,I,J,K,L,M) [E >= 0 (?,1) && C + E >= 0 && -5 + B + E >= 0 && 5 + -1*B + E >= 0 && -50 + A + E >= 0 && 50 + -1*A + E >= 0 && C >= 0 && -5 + B + C >= 0 && 5 + -1*B + C >= 0 && -50 + A + C >= 0 && 50 + -1*A + C >= 0 && 5 + -1*B >= 0 && -45 + A + -1*B >= 0 && 55 + -1*A + -1*B >= 0 && -5 + B >= 0 && -55 + A + B >= 0 && 45 + -1*A + B >= 0 && 50 + -1*A >= 0 && -50 + A >= 0 && E >= 1 + B] 25. f15(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f33(A,B,C,D,E,B,0,H,I,J,K,L,A) [C >= 0 (?,1) && -5 + B + C >= 0 && 5 + -1*B + C >= 0 && -50 + A + C >= 0 && 50 + -1*A + C >= 0 && 5 + -1*B >= 0 && -45 + A + -1*B >= 0 && 55 + -1*A + -1*B >= 0 && -5 + B >= 0 && -55 + A + B >= 0 && 45 + -1*A + B >= 0 && 50 + -1*A >= 0 && -50 + A >= 0 && C >= 1 + B] Signature: {(f0,13) ;(f15,13) ;(f19,13) ;(f33,13) ;(f36,13) ;(f41,13) ;(f50,13) ;(f54,13) ;(f66,13) ;(f70,13) ;(f80,13) ;(f84,13) ;(f96,13)} Flow Graph: [0->{1,25},1->{2,3,4,24},2->{2,3,4,24},3->{2,3,4,24},4->{2,3,4,24},5->{6,8,22},6->{7,21},7->{7,21},8->{6,8 ,22},9->{10,19},10->{10,19},11->{12,17},12->{12,17},13->{14,15},14->{14,15},15->{13,16},16->{},17->{11,18} ,18->{13,16},19->{9,20},20->{5,23},21->{6,8,22},22->{9,20},23->{11,18},24->{1,25},25->{5,23}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: UnsatPaths YES + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f15(50,5,0,D,E,F,G,H,I,J,K,L,M) True (1,1) 1. f15(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f19(A,B,C,0,0,F,G,H,I,J,K,L,M) [C >= 0 (?,1) && -5 + B + C >= 0 && 5 + -1*B + C >= 0 && -50 + A + C >= 0 && 50 + -1*A + C >= 0 && 5 + -1*B >= 0 && -45 + A + -1*B >= 0 && 55 + -1*A + -1*B >= 0 && -5 + B >= 0 && -55 + A + B >= 0 && 45 + -1*A + B >= 0 && 50 + -1*A >= 0 && -50 + A >= 0 && B >= C] 2. f19(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f19(A,B,C,D + N,1 + E,F,G,H,I,J,K,L,M) [E >= 0 (?,1) && C + E >= 0 && -5 + B + E >= 0 && 5 + -1*B + E >= 0 && -50 + A + E >= 0 && 50 + -1*A + E >= 0 && C >= 0 && -5 + B + C >= 0 && 5 + -1*B + C >= 0 && -50 + A + C >= 0 && 50 + -1*A + C >= 0 && 5 + -1*B >= 0 && -45 + A + -1*B >= 0 && 55 + -1*A + -1*B >= 0 && -5 + B >= 0 && -55 + A + B >= 0 && 45 + -1*A + B >= 0 && 50 + -1*A >= 0 && -50 + A >= 0 && B >= E && E >= 1 + C] 3. f19(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f19(A,B,C,D + N,1 + E,F,G,H,I,J,K,L,M) [E >= 0 (?,1) && C + E >= 0 && -5 + B + E >= 0 && 5 + -1*B + E >= 0 && -50 + A + E >= 0 && 50 + -1*A + E >= 0 && C >= 0 && -5 + B + C >= 0 && 5 + -1*B + C >= 0 && -50 + A + C >= 0 && 50 + -1*A + C >= 0 && 5 + -1*B >= 0 && -45 + A + -1*B >= 0 && 55 + -1*A + -1*B >= 0 && -5 + B >= 0 && -55 + A + B >= 0 && 45 + -1*A + B >= 0 && 50 + -1*A >= 0 && -50 + A >= 0 && C >= 1 + E && B >= E] 4. f19(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f19(A,B,C,D + N,1 + C,F,G,H,I,J,K,L,M) [E >= 0 (?,1) && C + E >= 0 && -5 + B + E >= 0 && 5 + -1*B + E >= 0 && -50 + A + E >= 0 && 50 + -1*A + E >= 0 && C >= 0 && -5 + B + C >= 0 && 5 + -1*B + C >= 0 && -50 + A + C >= 0 && 50 + -1*A + C >= 0 && 5 + -1*B >= 0 && -45 + A + -1*B >= 0 && 55 + -1*A + -1*B >= 0 && -5 + B >= 0 && -55 + A + B >= 0 && 45 + -1*A + B >= 0 && 50 + -1*A >= 0 && -50 + A >= 0 && B >= E && C = E] 5. f33(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f36(A,B,C,D,E,F,G,1 + G,I,J,K,L,M) [G >= 0 (?,1) && -5 + F + G >= 0 && 5 + -1*F + G >= 0 && -6 + C + G >= 0 && -5 + B + G >= 0 && 5 + -1*B + G >= 0 && -50 + G + M >= 0 && 50 + G + -1*M >= 0 && -50 + A + G >= 0 && 50 + -1*A + G >= 0 && 5 + -1*F >= 0 && -1 + C + -1*F >= 0 && B + -1*F >= 0 && 10 + -1*B + -1*F >= 0 && -45 + -1*F + M >= 0 && 55 + -1*F + -1*M >= 0 && -45 + A + -1*F >= 0 && 55 + -1*A + -1*F >= 0 && -5 + F >= 0 && -11 + C + F >= 0 && -10 + B + F >= 0 && -1*B + F >= 0 && -55 + F + M >= 0 && 45 + F + -1*M >= 0 && -55 + A + F >= 0 && 45 + -1*A + F >= 0 && -6 + C >= 0 && -11 + B + C >= 0 && -1 + -1*B + C >= 0 && -56 + C + M >= 0 && 44 + C + -1*M >= 0 && -56 + A + C >= 0 && 44 + -1*A + C >= 0 && 5 + -1*B >= 0 && -45 + -1*B + M >= 0 && 55 + -1*B + -1*M >= 0 && -45 + A + -1*B >= 0 && 55 + -1*A + -1*B >= 0 && -5 + B >= 0 && -55 + B + M >= 0 && 45 + B + -1*M >= 0 && -55 + A + B >= 0 && 45 + -1*A + B >= 0 && 50 + -1*M >= 0 && A + -1*M >= 0 && 100 + -1*A + -1*M >= 0 && -50 + M >= 0 && -100 + A + M >= 0 && -1*A + M >= 0 && 50 + -1*A >= 0 && -50 + A >= 0 && F >= 1 + G] 6. f36(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f41(A,B,C,D,E,F,G,H,N,0,K,L,M) [-1 + H >= 0 (?,1) && -1 + G + H >= 0 && -1 + -1*G + H >= 0 && -6 + F + H >= 0 && 4 + -1*F + H >= 0 && -7 + C + H >= 0 && -6 + B + H >= 0 && 4 + -1*B + H >= 0 && -51 + H + M >= 0 && 49 + H + -1*M >= 0 && -51 + A + H >= 0 && 49 + -1*A + H >= 0 && 4 + -1*G >= 0 && -1 + F + -1*G >= 0 && 9 + -1*F + -1*G >= 0 && -2 + C + -1*G >= 0 && -1 + B + -1*G >= 0 && 9 + -1*B + -1*G >= 0 && -46 + -1*G + M >= 0 && 54 + -1*G + -1*M >= 0 && -46 + A + -1*G >= 0 && 54 + -1*A + -1*G >= 0 && G >= 0 && -5 + F + G >= 0 && 5 + -1*F + G >= 0 && -6 + C + G >= 0 && -5 + B + G >= 0 && 5 + -1*B + G >= 0 && -50 + G + M >= 0 && 50 + G + -1*M >= 0 && -50 + A + G >= 0 && 50 + -1*A + G >= 0 && 5 + -1*F >= 0 && -1 + C + -1*F >= 0 && B + -1*F >= 0 && 10 + -1*B + -1*F >= 0 && -45 + -1*F + M >= 0 && 55 + -1*F + -1*M >= 0 && -45 + A + -1*F >= 0 && 55 + -1*A + -1*F >= 0 && -5 + F >= 0 && -11 + C + F >= 0 && -10 + B + F >= 0 && -1*B + F >= 0 && -55 + F + M >= 0 && 45 + F + -1*M >= 0 && -55 + A + F >= 0 && 45 + -1*A + F >= 0 && -6 + C >= 0 && -11 + B + C >= 0 && -1 + -1*B + C >= 0 && -56 + C + M >= 0 && 44 + C + -1*M >= 0 && -56 + A + C >= 0 && 44 + -1*A + C >= 0 && 5 + -1*B >= 0 && -45 + -1*B + M >= 0 && 55 + -1*B + -1*M >= 0 && -45 + A + -1*B >= 0 && 55 + -1*A + -1*B >= 0 && -5 + B >= 0 && -55 + B + M >= 0 && 45 + B + -1*M >= 0 && -55 + A + B >= 0 && 45 + -1*A + B >= 0 && 50 + -1*M >= 0 && A + -1*M >= 0 && 100 + -1*A + -1*M >= 0 && -50 + M >= 0 && -100 + A + M >= 0 && -1*A + M >= 0 && 50 + -1*A >= 0 && -50 + A >= 0 && G >= 1 && F >= H] 7. f41(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f41(A,B,C,D,E,F,G,H,N,1 + J,K,L,M) [5 + -1*H >= 0 (?,1) && 4 + G + -1*H >= 0 && 9 + -1*G + -1*H >= 0 && F + -1*H >= 0 && 10 + -1*F + -1*H >= 0 && -1 + C + -1*H >= 0 && B + -1*H >= 0 && 10 + -1*B + -1*H >= 0 && -45 + -1*H + M >= 0 && 55 + -1*H + -1*M >= 0 && 5 + -1*H + J >= 0 && -45 + A + -1*H >= 0 && 55 + -1*A + -1*H >= 0 && -2 + H >= 0 && -3 + G + H >= 0 && -1 + -1*G + H >= 0 && -7 + F + H >= 0 && 3 + -1*F + H >= 0 && -8 + C + H >= 0 && -7 + B + H >= 0 && 3 + -1*B + H >= 0 && -52 + H + M >= 0 && 48 + H + -1*M >= 0 && -2 + H + J >= 0 && -52 + A + H >= 0 && 48 + -1*A + H >= 0 && 4 + -1*G >= 0 && -1 + F + -1*G >= 0 && 9 + -1*F + -1*G >= 0 && -2 + C + -1*G >= 0 && -1 + B + -1*G >= 0 && 9 + -1*B + -1*G >= 0 && -46 + -1*G + M >= 0 && 54 + -1*G + -1*M >= 0 && 4 + -1*G + J >= 0 && -46 + A + -1*G >= 0 && 54 + -1*A + -1*G >= 0 && -1 + G >= 0 && -6 + F + G >= 0 && 4 + -1*F + G >= 0 && -7 + C + G >= 0 && -6 + B + G >= 0 && 4 + -1*B + G >= 0 && -51 + G + M >= 0 && 49 + G + -1*M >= 0 && -1 + G + J >= 0 && -51 + A + G >= 0 && 49 + -1*A + G >= 0 && 5 + -1*F >= 0 && -1 + C + -1*F >= 0 && B + -1*F >= 0 && 10 + -1*B + -1*F >= 0 && -45 + -1*F + M >= 0 && 55 + -1*F + -1*M >= 0 && 5 + -1*F + J >= 0 && -45 + A + -1*F >= 0 && 55 + -1*A + -1*F >= 0 && -5 + F >= 0 && -11 + C + F >= 0 && -10 + B + F >= 0 && -1*B + F >= 0 && -55 + F + M >= 0 && 45 + F + -1*M >= 0 && -5 + F + J >= 0 && -55 + A + F >= 0 && 45 + -1*A + F >= 0 && -6 + C >= 0 && -11 + B + C >= 0 && -1 + -1*B + C >= 0 && -56 + C + M >= 0 && 44 + C + -1*M >= 0 && -6 + C + J >= 0 && -56 + A + C >= 0 && 44 + -1*A + C >= 0 && 5 + -1*B >= 0 && -45 + -1*B + M >= 0 && 55 + -1*B + -1*M >= 0 && 5 + -1*B + J >= 0 && -45 + A + -1*B >= 0 && 55 + -1*A + -1*B >= 0 && -5 + B >= 0 && -55 + B + M >= 0 && 45 + B + -1*M >= 0 && -5 + B + J >= 0 && -55 + A + B >= 0 && 45 + -1*A + B >= 0 && 50 + -1*M >= 0 && 50 + J + -1*M >= 0 && A + -1*M >= 0 && 100 + -1*A + -1*M >= 0 && -50 + M >= 0 && -50 + J + M >= 0 && -100 + A + M >= 0 && -1*A + M >= 0 && J >= 0 && -50 + A + J >= 0 && 50 + -1*A + J >= 0 && 50 + -1*A >= 0 && -50 + A >= 0 && G >= 1 + J] 8. f36(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f36(A,B,C,D,E,F,0,1 + H,N,J,K,L,M) [-1 + H >= 0 (?,1) && -1 + G + H >= 0 && -1 + -1*G + H >= 0 && -6 + F + H >= 0 && 4 + -1*F + H >= 0 && -7 + C + H >= 0 && -6 + B + H >= 0 && 4 + -1*B + H >= 0 && -51 + H + M >= 0 && 49 + H + -1*M >= 0 && -51 + A + H >= 0 && 49 + -1*A + H >= 0 && 4 + -1*G >= 0 && -1 + F + -1*G >= 0 && 9 + -1*F + -1*G >= 0 && -2 + C + -1*G >= 0 && -1 + B + -1*G >= 0 && 9 + -1*B + -1*G >= 0 && -46 + -1*G + M >= 0 && 54 + -1*G + -1*M >= 0 && -46 + A + -1*G >= 0 && 54 + -1*A + -1*G >= 0 && G >= 0 && -5 + F + G >= 0 && 5 + -1*F + G >= 0 && -6 + C + G >= 0 && -5 + B + G >= 0 && 5 + -1*B + G >= 0 && -50 + G + M >= 0 && 50 + G + -1*M >= 0 && -50 + A + G >= 0 && 50 + -1*A + G >= 0 && 5 + -1*F >= 0 && -1 + C + -1*F >= 0 && B + -1*F >= 0 && 10 + -1*B + -1*F >= 0 && -45 + -1*F + M >= 0 && 55 + -1*F + -1*M >= 0 && -45 + A + -1*F >= 0 && 55 + -1*A + -1*F >= 0 && -5 + F >= 0 && -11 + C + F >= 0 && -10 + B + F >= 0 && -1*B + F >= 0 && -55 + F + M >= 0 && 45 + F + -1*M >= 0 && -55 + A + F >= 0 && 45 + -1*A + F >= 0 && -6 + C >= 0 && -11 + B + C >= 0 && -1 + -1*B + C >= 0 && -56 + C + M >= 0 && 44 + C + -1*M >= 0 && -56 + A + C >= 0 && 44 + -1*A + C >= 0 && 5 + -1*B >= 0 && -45 + -1*B + M >= 0 && 55 + -1*B + -1*M >= 0 && -45 + A + -1*B >= 0 && 55 + -1*A + -1*B >= 0 && -5 + B >= 0 && -55 + B + M >= 0 && 45 + B + -1*M >= 0 && -55 + A + B >= 0 && 45 + -1*A + B >= 0 && 50 + -1*M >= 0 && A + -1*M >= 0 && 100 + -1*A + -1*M >= 0 && -50 + M >= 0 && -100 + A + M >= 0 && -1*A + M >= 0 && 50 + -1*A >= 0 && -50 + A >= 0 && F >= H && G = 0] 9. f50(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f54(A,B,C,D,E,F,G,H,N,0,K,L,M) [-1 + H >= 0 (?,1) && -1 + G + H >= 0 && -1 + -1*G + H >= 0 && -6 + F + H >= 0 && 4 + -1*F + H >= 0 && -7 + C + H >= 0 && -6 + B + H >= 0 && 4 + -1*B + H >= 0 && -51 + H + M >= 0 && 49 + H + -1*M >= 0 && -51 + A + H >= 0 && 49 + -1*A + H >= 0 && G >= 0 && -5 + F + G >= 0 && 5 + -1*F + G >= 0 && -6 + C + G >= 0 && -5 + B + G >= 0 && 5 + -1*B + G >= 0 && -50 + G + M >= 0 && 50 + G + -1*M >= 0 && -50 + A + G >= 0 && 50 + -1*A + G >= 0 && 5 + -1*F >= 0 && -1 + C + -1*F >= 0 && B + -1*F >= 0 && 10 + -1*B + -1*F >= 0 && -45 + -1*F + M >= 0 && 55 + -1*F + -1*M >= 0 && -45 + A + -1*F >= 0 && 55 + -1*A + -1*F >= 0 && -5 + F >= 0 && -11 + C + F >= 0 && -10 + B + F >= 0 && -1*B + F >= 0 && -55 + F + M >= 0 && 45 + F + -1*M >= 0 && -55 + A + F >= 0 && 45 + -1*A + F >= 0 && -6 + C >= 0 && -11 + B + C >= 0 && -1 + -1*B + C >= 0 && -56 + C + M >= 0 && 44 + C + -1*M >= 0 && -56 + A + C >= 0 && 44 + -1*A + C >= 0 && 5 + -1*B >= 0 && -45 + -1*B + M >= 0 && 55 + -1*B + -1*M >= 0 && -45 + A + -1*B >= 0 && 55 + -1*A + -1*B >= 0 && -5 + B >= 0 && -55 + B + M >= 0 && 45 + B + -1*M >= 0 && -55 + A + B >= 0 && 45 + -1*A + B >= 0 && 50 + -1*M >= 0 && A + -1*M >= 0 && 100 + -1*A + -1*M >= 0 && -50 + M >= 0 && -100 + A + M >= 0 && -1*A + M >= 0 && 50 + -1*A >= 0 && -50 + A >= 0 && F >= H] 10. f54(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f54(A,B,C,D,E,F,G,H,N,1 + J,K,L,M) [-1 + H >= 0 (?,1) && -1 + G + H >= 0 && -1 + -1*G + H >= 0 && -6 + F + H >= 0 && 4 + -1*F + H >= 0 && -7 + C + H >= 0 && -6 + B + H >= 0 && 4 + -1*B + H >= 0 && -51 + H + M >= 0 && 49 + H + -1*M >= 0 && -1 + H + J >= 0 && -51 + A + H >= 0 && 49 + -1*A + H >= 0 && 4 + -1*G >= 0 && -1 + F + -1*G >= 0 && 9 + -1*F + -1*G >= 0 && -2 + C + -1*G >= 0 && -1 + B + -1*G >= 0 && 9 + -1*B + -1*G >= 0 && -46 + -1*G + M >= 0 && 54 + -1*G + -1*M >= 0 && 4 + -1*G + J >= 0 && -46 + A + -1*G >= 0 && 54 + -1*A + -1*G >= 0 && G >= 0 && -5 + F + G >= 0 && 5 + -1*F + G >= 0 && -6 + C + G >= 0 && -5 + B + G >= 0 && 5 + -1*B + G >= 0 && -50 + G + M >= 0 && 50 + G + -1*M >= 0 && G + J >= 0 && -50 + A + G >= 0 && 50 + -1*A + G >= 0 && 5 + -1*F >= 0 && -1 + C + -1*F >= 0 && B + -1*F >= 0 && 10 + -1*B + -1*F >= 0 && -45 + -1*F + M >= 0 && 55 + -1*F + -1*M >= 0 && 5 + -1*F + J >= 0 && -45 + A + -1*F >= 0 && 55 + -1*A + -1*F >= 0 && -5 + F >= 0 && -11 + C + F >= 0 && -10 + B + F >= 0 && -1*B + F >= 0 && -55 + F + M >= 0 && 45 + F + -1*M >= 0 && -5 + F + J >= 0 && -55 + A + F >= 0 && 45 + -1*A + F >= 0 && -6 + C >= 0 && -11 + B + C >= 0 && -1 + -1*B + C >= 0 && -56 + C + M >= 0 && 44 + C + -1*M >= 0 && -6 + C + J >= 0 && -56 + A + C >= 0 && 44 + -1*A + C >= 0 && 5 + -1*B >= 0 && -45 + -1*B + M >= 0 && 55 + -1*B + -1*M >= 0 && 5 + -1*B + J >= 0 && -45 + A + -1*B >= 0 && 55 + -1*A + -1*B >= 0 && -5 + B >= 0 && -55 + B + M >= 0 && 45 + B + -1*M >= 0 && -5 + B + J >= 0 && -55 + A + B >= 0 && 45 + -1*A + B >= 0 && 50 + -1*M >= 0 && 50 + J + -1*M >= 0 && A + -1*M >= 0 && 100 + -1*A + -1*M >= 0 && -50 + M >= 0 && -50 + J + M >= 0 && -100 + A + M >= 0 && -1*A + M >= 0 && J >= 0 && -50 + A + J >= 0 && 50 + -1*A + J >= 0 && 50 + -1*A >= 0 && -50 + A >= 0 && G >= J] 11. f66(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f70(A,B,C,D,E,F,G,0,N,J,K,L,M) [-1 + G >= 0 (?,1) && -6 + F + G >= 0 && 4 + -1*F + G >= 0 && -7 + C + G >= 0 && -6 + B + G >= 0 && 4 + -1*B + G >= 0 && -51 + G + M >= 0 && 49 + G + -1*M >= 0 && -51 + A + G >= 0 && 49 + -1*A + G >= 0 && 5 + -1*F >= 0 && -1 + C + -1*F >= 0 && B + -1*F >= 0 && 10 + -1*B + -1*F >= 0 && -45 + -1*F + M >= 0 && 55 + -1*F + -1*M >= 0 && -45 + A + -1*F >= 0 && 55 + -1*A + -1*F >= 0 && -5 + F >= 0 && -11 + C + F >= 0 && -10 + B + F >= 0 && -1*B + F >= 0 && -55 + F + M >= 0 && 45 + F + -1*M >= 0 && -55 + A + F >= 0 && 45 + -1*A + F >= 0 && -6 + C >= 0 && -11 + B + C >= 0 && -1 + -1*B + C >= 0 && -56 + C + M >= 0 && 44 + C + -1*M >= 0 && -56 + A + C >= 0 && 44 + -1*A + C >= 0 && 5 + -1*B >= 0 && -45 + -1*B + M >= 0 && 55 + -1*B + -1*M >= 0 && -45 + A + -1*B >= 0 && 55 + -1*A + -1*B >= 0 && -5 + B >= 0 && -55 + B + M >= 0 && 45 + B + -1*M >= 0 && -55 + A + B >= 0 && 45 + -1*A + B >= 0 && 50 + -1*M >= 0 && A + -1*M >= 0 && 100 + -1*A + -1*M >= 0 && -50 + M >= 0 && -100 + A + M >= 0 && -1*A + M >= 0 && 50 + -1*A >= 0 && -50 + A >= 0 && F >= G] 12. f70(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f70(A,B,C,D,E,F,G,1 + H,N,J,K,L,M) [H >= 0 (?,1) && -1 + G + H >= 0 && -5 + F + H >= 0 && 5 + -1*F + H >= 0 && -6 + C + H >= 0 && -5 + B + H >= 0 && 5 + -1*B + H >= 0 && -50 + H + M >= 0 && 50 + H + -1*M >= 0 && -50 + A + H >= 0 && 50 + -1*A + H >= 0 && -1 + G >= 0 && -6 + F + G >= 0 && 4 + -1*F + G >= 0 && -7 + C + G >= 0 && -6 + B + G >= 0 && 4 + -1*B + G >= 0 && -51 + G + M >= 0 && 49 + G + -1*M >= 0 && -51 + A + G >= 0 && 49 + -1*A + G >= 0 && 5 + -1*F >= 0 && -1 + C + -1*F >= 0 && B + -1*F >= 0 && 10 + -1*B + -1*F >= 0 && -45 + -1*F + M >= 0 && 55 + -1*F + -1*M >= 0 && -45 + A + -1*F >= 0 && 55 + -1*A + -1*F >= 0 && -5 + F >= 0 && -11 + C + F >= 0 && -10 + B + F >= 0 && -1*B + F >= 0 && -55 + F + M >= 0 && 45 + F + -1*M >= 0 && -55 + A + F >= 0 && 45 + -1*A + F >= 0 && -6 + C >= 0 && -11 + B + C >= 0 && -1 + -1*B + C >= 0 && -56 + C + M >= 0 && 44 + C + -1*M >= 0 && -56 + A + C >= 0 && 44 + -1*A + C >= 0 && 5 + -1*B >= 0 && -45 + -1*B + M >= 0 && 55 + -1*B + -1*M >= 0 && -45 + A + -1*B >= 0 && 55 + -1*A + -1*B >= 0 && -5 + B >= 0 && -55 + B + M >= 0 && 45 + B + -1*M >= 0 && -55 + A + B >= 0 && 45 + -1*A + B >= 0 && 50 + -1*M >= 0 && A + -1*M >= 0 && 100 + -1*A + -1*M >= 0 && -50 + M >= 0 && -100 + A + M >= 0 && -1*A + M >= 0 && 50 + -1*A >= 0 && -50 + A >= 0 && G >= 1 + H] 13. f80(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f84(A,B,C,D,E,F,G,1 + G,N,J,K,L,M) [4 + -1*G >= 0 (?,1) && -1 + F + -1*G >= 0 && 9 + -1*F + -1*G >= 0 && -2 + C + -1*G >= 0 && -1 + B + -1*G >= 0 && 9 + -1*B + -1*G >= 0 && -46 + -1*G + M >= 0 && 54 + -1*G + -1*M >= 0 && -46 + A + -1*G >= 0 && 54 + -1*A + -1*G >= 0 && 5 + -1*F >= 0 && -1 + C + -1*F >= 0 && B + -1*F >= 0 && 10 + -1*B + -1*F >= 0 && -45 + -1*F + M >= 0 && 55 + -1*F + -1*M >= 0 && -45 + A + -1*F >= 0 && 55 + -1*A + -1*F >= 0 && -5 + F >= 0 && -11 + C + F >= 0 && -10 + B + F >= 0 && -1*B + F >= 0 && -55 + F + M >= 0 && 45 + F + -1*M >= 0 && -55 + A + F >= 0 && 45 + -1*A + F >= 0 && -6 + C >= 0 && -11 + B + C >= 0 && -1 + -1*B + C >= 0 && -56 + C + M >= 0 && 44 + C + -1*M >= 0 && -56 + A + C >= 0 && 44 + -1*A + C >= 0 && 5 + -1*B >= 0 && -45 + -1*B + M >= 0 && 55 + -1*B + -1*M >= 0 && -45 + A + -1*B >= 0 && 55 + -1*A + -1*B >= 0 && -5 + B >= 0 && -55 + B + M >= 0 && 45 + B + -1*M >= 0 && -55 + A + B >= 0 && 45 + -1*A + B >= 0 && 50 + -1*M >= 0 && A + -1*M >= 0 && 100 + -1*A + -1*M >= 0 && -50 + M >= 0 && -100 + A + M >= 0 && -1*A + M >= 0 && 50 + -1*A >= 0 && -50 + A >= 0 && G >= 0] 14. f84(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f84(A,B,C,D,E,F,G,1 + H,N,J,K,L,M) [-1 + -1*G + H >= 0 (?,1) && 4 + -1*G >= 0 && -1 + F + -1*G >= 0 && 9 + -1*F + -1*G >= 0 && -2 + C + -1*G >= 0 && -1 + B + -1*G >= 0 && 9 + -1*B + -1*G >= 0 && -46 + -1*G + M >= 0 && 54 + -1*G + -1*M >= 0 && -46 + A + -1*G >= 0 && 54 + -1*A + -1*G >= 0 && 5 + -1*F >= 0 && -1 + C + -1*F >= 0 && B + -1*F >= 0 && 10 + -1*B + -1*F >= 0 && -45 + -1*F + M >= 0 && 55 + -1*F + -1*M >= 0 && -45 + A + -1*F >= 0 && 55 + -1*A + -1*F >= 0 && -5 + F >= 0 && -11 + C + F >= 0 && -10 + B + F >= 0 && -1*B + F >= 0 && -55 + F + M >= 0 && 45 + F + -1*M >= 0 && -55 + A + F >= 0 && 45 + -1*A + F >= 0 && -6 + C >= 0 && -11 + B + C >= 0 && -1 + -1*B + C >= 0 && -56 + C + M >= 0 && 44 + C + -1*M >= 0 && -56 + A + C >= 0 && 44 + -1*A + C >= 0 && 5 + -1*B >= 0 && -45 + -1*B + M >= 0 && 55 + -1*B + -1*M >= 0 && -45 + A + -1*B >= 0 && 55 + -1*A + -1*B >= 0 && -5 + B >= 0 && -55 + B + M >= 0 && 45 + B + -1*M >= 0 && -55 + A + B >= 0 && 45 + -1*A + B >= 0 && 50 + -1*M >= 0 && A + -1*M >= 0 && 100 + -1*A + -1*M >= 0 && -50 + M >= 0 && -100 + A + M >= 0 && -1*A + M >= 0 && 50 + -1*A >= 0 && -50 + A >= 0 && F >= H] 15. f84(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f80(A,B,C,D,E,F,-1 + G,H,I,J,K,L,M) [-1 + -1*G + H >= 0 (?,1) && 4 + -1*G >= 0 && -1 + F + -1*G >= 0 && 9 + -1*F + -1*G >= 0 && -2 + C + -1*G >= 0 && -1 + B + -1*G >= 0 && 9 + -1*B + -1*G >= 0 && -46 + -1*G + M >= 0 && 54 + -1*G + -1*M >= 0 && -46 + A + -1*G >= 0 && 54 + -1*A + -1*G >= 0 && 5 + -1*F >= 0 && -1 + C + -1*F >= 0 && B + -1*F >= 0 && 10 + -1*B + -1*F >= 0 && -45 + -1*F + M >= 0 && 55 + -1*F + -1*M >= 0 && -45 + A + -1*F >= 0 && 55 + -1*A + -1*F >= 0 && -5 + F >= 0 && -11 + C + F >= 0 && -10 + B + F >= 0 && -1*B + F >= 0 && -55 + F + M >= 0 && 45 + F + -1*M >= 0 && -55 + A + F >= 0 && 45 + -1*A + F >= 0 && -6 + C >= 0 && -11 + B + C >= 0 && -1 + -1*B + C >= 0 && -56 + C + M >= 0 && 44 + C + -1*M >= 0 && -56 + A + C >= 0 && 44 + -1*A + C >= 0 && 5 + -1*B >= 0 && -45 + -1*B + M >= 0 && 55 + -1*B + -1*M >= 0 && -45 + A + -1*B >= 0 && 55 + -1*A + -1*B >= 0 && -5 + B >= 0 && -55 + B + M >= 0 && 45 + B + -1*M >= 0 && -55 + A + B >= 0 && 45 + -1*A + B >= 0 && 50 + -1*M >= 0 && A + -1*M >= 0 && 100 + -1*A + -1*M >= 0 && -50 + M >= 0 && -100 + A + M >= 0 && -1*A + M >= 0 && 50 + -1*A >= 0 && -50 + A >= 0 && H >= 1 + F] 16. f80(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f96(A,B,C,D,E,F,G,H,I,J,0,0,M) [4 + -1*G >= 0 (1,1) && -1 + F + -1*G >= 0 && 9 + -1*F + -1*G >= 0 && -2 + C + -1*G >= 0 && -1 + B + -1*G >= 0 && 9 + -1*B + -1*G >= 0 && -46 + -1*G + M >= 0 && 54 + -1*G + -1*M >= 0 && -46 + A + -1*G >= 0 && 54 + -1*A + -1*G >= 0 && 5 + -1*F >= 0 && -1 + C + -1*F >= 0 && B + -1*F >= 0 && 10 + -1*B + -1*F >= 0 && -45 + -1*F + M >= 0 && 55 + -1*F + -1*M >= 0 && -45 + A + -1*F >= 0 && 55 + -1*A + -1*F >= 0 && -5 + F >= 0 && -11 + C + F >= 0 && -10 + B + F >= 0 && -1*B + F >= 0 && -55 + F + M >= 0 && 45 + F + -1*M >= 0 && -55 + A + F >= 0 && 45 + -1*A + F >= 0 && -6 + C >= 0 && -11 + B + C >= 0 && -1 + -1*B + C >= 0 && -56 + C + M >= 0 && 44 + C + -1*M >= 0 && -56 + A + C >= 0 && 44 + -1*A + C >= 0 && 5 + -1*B >= 0 && -45 + -1*B + M >= 0 && 55 + -1*B + -1*M >= 0 && -45 + A + -1*B >= 0 && 55 + -1*A + -1*B >= 0 && -5 + B >= 0 && -55 + B + M >= 0 && 45 + B + -1*M >= 0 && -55 + A + B >= 0 && 45 + -1*A + B >= 0 && 50 + -1*M >= 0 && A + -1*M >= 0 && 100 + -1*A + -1*M >= 0 && -50 + M >= 0 && -100 + A + M >= 0 && -1*A + M >= 0 && 50 + -1*A >= 0 && -50 + A >= 0 && 0 >= 1 + G] 17. f70(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f66(A,B,C,D,E,F,1 + G,H,I,J,K,L,M) [H >= 0 (?,1) && -1 + G + H >= 0 && -5 + F + H >= 0 && 5 + -1*F + H >= 0 && -6 + C + H >= 0 && -5 + B + H >= 0 && 5 + -1*B + H >= 0 && -50 + H + M >= 0 && 50 + H + -1*M >= 0 && -50 + A + H >= 0 && 50 + -1*A + H >= 0 && -1 + G >= 0 && -6 + F + G >= 0 && 4 + -1*F + G >= 0 && -7 + C + G >= 0 && -6 + B + G >= 0 && 4 + -1*B + G >= 0 && -51 + G + M >= 0 && 49 + G + -1*M >= 0 && -51 + A + G >= 0 && 49 + -1*A + G >= 0 && 5 + -1*F >= 0 && -1 + C + -1*F >= 0 && B + -1*F >= 0 && 10 + -1*B + -1*F >= 0 && -45 + -1*F + M >= 0 && 55 + -1*F + -1*M >= 0 && -45 + A + -1*F >= 0 && 55 + -1*A + -1*F >= 0 && -5 + F >= 0 && -11 + C + F >= 0 && -10 + B + F >= 0 && -1*B + F >= 0 && -55 + F + M >= 0 && 45 + F + -1*M >= 0 && -55 + A + F >= 0 && 45 + -1*A + F >= 0 && -6 + C >= 0 && -11 + B + C >= 0 && -1 + -1*B + C >= 0 && -56 + C + M >= 0 && 44 + C + -1*M >= 0 && -56 + A + C >= 0 && 44 + -1*A + C >= 0 && 5 + -1*B >= 0 && -45 + -1*B + M >= 0 && 55 + -1*B + -1*M >= 0 && -45 + A + -1*B >= 0 && 55 + -1*A + -1*B >= 0 && -5 + B >= 0 && -55 + B + M >= 0 && 45 + B + -1*M >= 0 && -55 + A + B >= 0 && 45 + -1*A + B >= 0 && 50 + -1*M >= 0 && A + -1*M >= 0 && 100 + -1*A + -1*M >= 0 && -50 + M >= 0 && -100 + A + M >= 0 && -1*A + M >= 0 && 50 + -1*A >= 0 && -50 + A >= 0 && H >= G] 18. f66(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f80(A,B,C,D,E,F,-1 + F,H,I,J,K,L,M) [-1 + G >= 0 (1,1) && -6 + F + G >= 0 && 4 + -1*F + G >= 0 && -7 + C + G >= 0 && -6 + B + G >= 0 && 4 + -1*B + G >= 0 && -51 + G + M >= 0 && 49 + G + -1*M >= 0 && -51 + A + G >= 0 && 49 + -1*A + G >= 0 && 5 + -1*F >= 0 && -1 + C + -1*F >= 0 && B + -1*F >= 0 && 10 + -1*B + -1*F >= 0 && -45 + -1*F + M >= 0 && 55 + -1*F + -1*M >= 0 && -45 + A + -1*F >= 0 && 55 + -1*A + -1*F >= 0 && -5 + F >= 0 && -11 + C + F >= 0 && -10 + B + F >= 0 && -1*B + F >= 0 && -55 + F + M >= 0 && 45 + F + -1*M >= 0 && -55 + A + F >= 0 && 45 + -1*A + F >= 0 && -6 + C >= 0 && -11 + B + C >= 0 && -1 + -1*B + C >= 0 && -56 + C + M >= 0 && 44 + C + -1*M >= 0 && -56 + A + C >= 0 && 44 + -1*A + C >= 0 && 5 + -1*B >= 0 && -45 + -1*B + M >= 0 && 55 + -1*B + -1*M >= 0 && -45 + A + -1*B >= 0 && 55 + -1*A + -1*B >= 0 && -5 + B >= 0 && -55 + B + M >= 0 && 45 + B + -1*M >= 0 && -55 + A + B >= 0 && 45 + -1*A + B >= 0 && 50 + -1*M >= 0 && A + -1*M >= 0 && 100 + -1*A + -1*M >= 0 && -50 + M >= 0 && -100 + A + M >= 0 && -1*A + M >= 0 && 50 + -1*A >= 0 && -50 + A >= 0 && G >= 1 + F] 19. f54(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f50(A,B,C,D,E,F,G,1 + H,I,J,K,L,M) [-1 + H >= 0 (?,1) && -1 + G + H >= 0 && -1 + -1*G + H >= 0 && -6 + F + H >= 0 && 4 + -1*F + H >= 0 && -7 + C + H >= 0 && -6 + B + H >= 0 && 4 + -1*B + H >= 0 && -51 + H + M >= 0 && 49 + H + -1*M >= 0 && -1 + H + J >= 0 && -51 + A + H >= 0 && 49 + -1*A + H >= 0 && 4 + -1*G >= 0 && -1 + F + -1*G >= 0 && 9 + -1*F + -1*G >= 0 && -2 + C + -1*G >= 0 && -1 + B + -1*G >= 0 && 9 + -1*B + -1*G >= 0 && -46 + -1*G + M >= 0 && 54 + -1*G + -1*M >= 0 && 4 + -1*G + J >= 0 && -46 + A + -1*G >= 0 && 54 + -1*A + -1*G >= 0 && G >= 0 && -5 + F + G >= 0 && 5 + -1*F + G >= 0 && -6 + C + G >= 0 && -5 + B + G >= 0 && 5 + -1*B + G >= 0 && -50 + G + M >= 0 && 50 + G + -1*M >= 0 && G + J >= 0 && -50 + A + G >= 0 && 50 + -1*A + G >= 0 && 5 + -1*F >= 0 && -1 + C + -1*F >= 0 && B + -1*F >= 0 && 10 + -1*B + -1*F >= 0 && -45 + -1*F + M >= 0 && 55 + -1*F + -1*M >= 0 && 5 + -1*F + J >= 0 && -45 + A + -1*F >= 0 && 55 + -1*A + -1*F >= 0 && -5 + F >= 0 && -11 + C + F >= 0 && -10 + B + F >= 0 && -1*B + F >= 0 && -55 + F + M >= 0 && 45 + F + -1*M >= 0 && -5 + F + J >= 0 && -55 + A + F >= 0 && 45 + -1*A + F >= 0 && -6 + C >= 0 && -11 + B + C >= 0 && -1 + -1*B + C >= 0 && -56 + C + M >= 0 && 44 + C + -1*M >= 0 && -6 + C + J >= 0 && -56 + A + C >= 0 && 44 + -1*A + C >= 0 && 5 + -1*B >= 0 && -45 + -1*B + M >= 0 && 55 + -1*B + -1*M >= 0 && 5 + -1*B + J >= 0 && -45 + A + -1*B >= 0 && 55 + -1*A + -1*B >= 0 && -5 + B >= 0 && -55 + B + M >= 0 && 45 + B + -1*M >= 0 && -5 + B + J >= 0 && -55 + A + B >= 0 && 45 + -1*A + B >= 0 && 50 + -1*M >= 0 && 50 + J + -1*M >= 0 && A + -1*M >= 0 && 100 + -1*A + -1*M >= 0 && -50 + M >= 0 && -50 + J + M >= 0 && -100 + A + M >= 0 && -1*A + M >= 0 && J >= 0 && -50 + A + J >= 0 && 50 + -1*A + J >= 0 && 50 + -1*A >= 0 && -50 + A >= 0 && J >= 1 + G] 20. f50(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f33(A,B,C,D,E,F,1 + G,H,I,J,K,L,M) [-1 + H >= 0 (?,1) && -1 + G + H >= 0 && -1 + -1*G + H >= 0 && -6 + F + H >= 0 && 4 + -1*F + H >= 0 && -7 + C + H >= 0 && -6 + B + H >= 0 && 4 + -1*B + H >= 0 && -51 + H + M >= 0 && 49 + H + -1*M >= 0 && -51 + A + H >= 0 && 49 + -1*A + H >= 0 && G >= 0 && -5 + F + G >= 0 && 5 + -1*F + G >= 0 && -6 + C + G >= 0 && -5 + B + G >= 0 && 5 + -1*B + G >= 0 && -50 + G + M >= 0 && 50 + G + -1*M >= 0 && -50 + A + G >= 0 && 50 + -1*A + G >= 0 && 5 + -1*F >= 0 && -1 + C + -1*F >= 0 && B + -1*F >= 0 && 10 + -1*B + -1*F >= 0 && -45 + -1*F + M >= 0 && 55 + -1*F + -1*M >= 0 && -45 + A + -1*F >= 0 && 55 + -1*A + -1*F >= 0 && -5 + F >= 0 && -11 + C + F >= 0 && -10 + B + F >= 0 && -1*B + F >= 0 && -55 + F + M >= 0 && 45 + F + -1*M >= 0 && -55 + A + F >= 0 && 45 + -1*A + F >= 0 && -6 + C >= 0 && -11 + B + C >= 0 && -1 + -1*B + C >= 0 && -56 + C + M >= 0 && 44 + C + -1*M >= 0 && -56 + A + C >= 0 && 44 + -1*A + C >= 0 && 5 + -1*B >= 0 && -45 + -1*B + M >= 0 && 55 + -1*B + -1*M >= 0 && -45 + A + -1*B >= 0 && 55 + -1*A + -1*B >= 0 && -5 + B >= 0 && -55 + B + M >= 0 && 45 + B + -1*M >= 0 && -55 + A + B >= 0 && 45 + -1*A + B >= 0 && 50 + -1*M >= 0 && A + -1*M >= 0 && 100 + -1*A + -1*M >= 0 && -50 + M >= 0 && -100 + A + M >= 0 && -1*A + M >= 0 && 50 + -1*A >= 0 && -50 + A >= 0 && H >= 1 + F] 21. f41(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f36(A,B,C,D,E,F,G,1 + H,I,J,K,L,M) [5 + -1*H >= 0 (?,1) && 4 + G + -1*H >= 0 && 9 + -1*G + -1*H >= 0 && F + -1*H >= 0 && 10 + -1*F + -1*H >= 0 && -1 + C + -1*H >= 0 && B + -1*H >= 0 && 10 + -1*B + -1*H >= 0 && -45 + -1*H + M >= 0 && 55 + -1*H + -1*M >= 0 && 5 + -1*H + J >= 0 && -45 + A + -1*H >= 0 && 55 + -1*A + -1*H >= 0 && -2 + H >= 0 && -3 + G + H >= 0 && -1 + -1*G + H >= 0 && -7 + F + H >= 0 && 3 + -1*F + H >= 0 && -8 + C + H >= 0 && -7 + B + H >= 0 && 3 + -1*B + H >= 0 && -52 + H + M >= 0 && 48 + H + -1*M >= 0 && -2 + H + J >= 0 && -52 + A + H >= 0 && 48 + -1*A + H >= 0 && 4 + -1*G >= 0 && -1 + F + -1*G >= 0 && 9 + -1*F + -1*G >= 0 && -2 + C + -1*G >= 0 && -1 + B + -1*G >= 0 && 9 + -1*B + -1*G >= 0 && -46 + -1*G + M >= 0 && 54 + -1*G + -1*M >= 0 && 4 + -1*G + J >= 0 && -46 + A + -1*G >= 0 && 54 + -1*A + -1*G >= 0 && -1 + G >= 0 && -6 + F + G >= 0 && 4 + -1*F + G >= 0 && -7 + C + G >= 0 && -6 + B + G >= 0 && 4 + -1*B + G >= 0 && -51 + G + M >= 0 && 49 + G + -1*M >= 0 && -1 + G + J >= 0 && -51 + A + G >= 0 && 49 + -1*A + G >= 0 && 5 + -1*F >= 0 && -1 + C + -1*F >= 0 && B + -1*F >= 0 && 10 + -1*B + -1*F >= 0 && -45 + -1*F + M >= 0 && 55 + -1*F + -1*M >= 0 && 5 + -1*F + J >= 0 && -45 + A + -1*F >= 0 && 55 + -1*A + -1*F >= 0 && -5 + F >= 0 && -11 + C + F >= 0 && -10 + B + F >= 0 && -1*B + F >= 0 && -55 + F + M >= 0 && 45 + F + -1*M >= 0 && -5 + F + J >= 0 && -55 + A + F >= 0 && 45 + -1*A + F >= 0 && -6 + C >= 0 && -11 + B + C >= 0 && -1 + -1*B + C >= 0 && -56 + C + M >= 0 && 44 + C + -1*M >= 0 && -6 + C + J >= 0 && -56 + A + C >= 0 && 44 + -1*A + C >= 0 && 5 + -1*B >= 0 && -45 + -1*B + M >= 0 && 55 + -1*B + -1*M >= 0 && 5 + -1*B + J >= 0 && -45 + A + -1*B >= 0 && 55 + -1*A + -1*B >= 0 && -5 + B >= 0 && -55 + B + M >= 0 && 45 + B + -1*M >= 0 && -5 + B + J >= 0 && -55 + A + B >= 0 && 45 + -1*A + B >= 0 && 50 + -1*M >= 0 && 50 + J + -1*M >= 0 && A + -1*M >= 0 && 100 + -1*A + -1*M >= 0 && -50 + M >= 0 && -50 + J + M >= 0 && -100 + A + M >= 0 && -1*A + M >= 0 && J >= 0 && -50 + A + J >= 0 && 50 + -1*A + J >= 0 && 50 + -1*A >= 0 && -50 + A >= 0 && J >= G] 22. f36(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f50(A,B,C,D,E,F,G,1 + G,I,J,K,L,M) [-1 + H >= 0 (?,1) && -1 + G + H >= 0 && -1 + -1*G + H >= 0 && -6 + F + H >= 0 && 4 + -1*F + H >= 0 && -7 + C + H >= 0 && -6 + B + H >= 0 && 4 + -1*B + H >= 0 && -51 + H + M >= 0 && 49 + H + -1*M >= 0 && -51 + A + H >= 0 && 49 + -1*A + H >= 0 && 4 + -1*G >= 0 && -1 + F + -1*G >= 0 && 9 + -1*F + -1*G >= 0 && -2 + C + -1*G >= 0 && -1 + B + -1*G >= 0 && 9 + -1*B + -1*G >= 0 && -46 + -1*G + M >= 0 && 54 + -1*G + -1*M >= 0 && -46 + A + -1*G >= 0 && 54 + -1*A + -1*G >= 0 && G >= 0 && -5 + F + G >= 0 && 5 + -1*F + G >= 0 && -6 + C + G >= 0 && -5 + B + G >= 0 && 5 + -1*B + G >= 0 && -50 + G + M >= 0 && 50 + G + -1*M >= 0 && -50 + A + G >= 0 && 50 + -1*A + G >= 0 && 5 + -1*F >= 0 && -1 + C + -1*F >= 0 && B + -1*F >= 0 && 10 + -1*B + -1*F >= 0 && -45 + -1*F + M >= 0 && 55 + -1*F + -1*M >= 0 && -45 + A + -1*F >= 0 && 55 + -1*A + -1*F >= 0 && -5 + F >= 0 && -11 + C + F >= 0 && -10 + B + F >= 0 && -1*B + F >= 0 && -55 + F + M >= 0 && 45 + F + -1*M >= 0 && -55 + A + F >= 0 && 45 + -1*A + F >= 0 && -6 + C >= 0 && -11 + B + C >= 0 && -1 + -1*B + C >= 0 && -56 + C + M >= 0 && 44 + C + -1*M >= 0 && -56 + A + C >= 0 && 44 + -1*A + C >= 0 && 5 + -1*B >= 0 && -45 + -1*B + M >= 0 && 55 + -1*B + -1*M >= 0 && -45 + A + -1*B >= 0 && 55 + -1*A + -1*B >= 0 && -5 + B >= 0 && -55 + B + M >= 0 && 45 + B + -1*M >= 0 && -55 + A + B >= 0 && 45 + -1*A + B >= 0 && 50 + -1*M >= 0 && A + -1*M >= 0 && 100 + -1*A + -1*M >= 0 && -50 + M >= 0 && -100 + A + M >= 0 && -1*A + M >= 0 && 50 + -1*A >= 0 && -50 + A >= 0 && H >= 1 + F] 23. f33(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f66(A,B,C,D,E,F,1,H,I,J,K,L,M) [G >= 0 (1,1) && -5 + F + G >= 0 && 5 + -1*F + G >= 0 && -6 + C + G >= 0 && -5 + B + G >= 0 && 5 + -1*B + G >= 0 && -50 + G + M >= 0 && 50 + G + -1*M >= 0 && -50 + A + G >= 0 && 50 + -1*A + G >= 0 && 5 + -1*F >= 0 && -1 + C + -1*F >= 0 && B + -1*F >= 0 && 10 + -1*B + -1*F >= 0 && -45 + -1*F + M >= 0 && 55 + -1*F + -1*M >= 0 && -45 + A + -1*F >= 0 && 55 + -1*A + -1*F >= 0 && -5 + F >= 0 && -11 + C + F >= 0 && -10 + B + F >= 0 && -1*B + F >= 0 && -55 + F + M >= 0 && 45 + F + -1*M >= 0 && -55 + A + F >= 0 && 45 + -1*A + F >= 0 && -6 + C >= 0 && -11 + B + C >= 0 && -1 + -1*B + C >= 0 && -56 + C + M >= 0 && 44 + C + -1*M >= 0 && -56 + A + C >= 0 && 44 + -1*A + C >= 0 && 5 + -1*B >= 0 && -45 + -1*B + M >= 0 && 55 + -1*B + -1*M >= 0 && -45 + A + -1*B >= 0 && 55 + -1*A + -1*B >= 0 && -5 + B >= 0 && -55 + B + M >= 0 && 45 + B + -1*M >= 0 && -55 + A + B >= 0 && 45 + -1*A + B >= 0 && 50 + -1*M >= 0 && A + -1*M >= 0 && 100 + -1*A + -1*M >= 0 && -50 + M >= 0 && -100 + A + M >= 0 && -1*A + M >= 0 && 50 + -1*A >= 0 && -50 + A >= 0 && G >= F] 24. f19(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f15(A,B,1 + C,D,E,F,G,H,I,J,K,L,M) [E >= 0 (?,1) && C + E >= 0 && -5 + B + E >= 0 && 5 + -1*B + E >= 0 && -50 + A + E >= 0 && 50 + -1*A + E >= 0 && C >= 0 && -5 + B + C >= 0 && 5 + -1*B + C >= 0 && -50 + A + C >= 0 && 50 + -1*A + C >= 0 && 5 + -1*B >= 0 && -45 + A + -1*B >= 0 && 55 + -1*A + -1*B >= 0 && -5 + B >= 0 && -55 + A + B >= 0 && 45 + -1*A + B >= 0 && 50 + -1*A >= 0 && -50 + A >= 0 && E >= 1 + B] 25. f15(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f33(A,B,C,D,E,B,0,H,I,J,K,L,A) [C >= 0 (1,1) && -5 + B + C >= 0 && 5 + -1*B + C >= 0 && -50 + A + C >= 0 && 50 + -1*A + C >= 0 && 5 + -1*B >= 0 && -45 + A + -1*B >= 0 && 55 + -1*A + -1*B >= 0 && -5 + B >= 0 && -55 + A + B >= 0 && 45 + -1*A + B >= 0 && 50 + -1*A >= 0 && -50 + A >= 0 && C >= 1 + B] Signature: {(f0,13) ;(f15,13) ;(f19,13) ;(f33,13) ;(f36,13) ;(f41,13) ;(f50,13) ;(f54,13) ;(f66,13) ;(f70,13) ;(f80,13) ;(f84,13) ;(f96,13)} Flow Graph: [0->{1,25},1->{2,3,4,24},2->{2,3,4,24},3->{2,3,4,24},4->{2,3,4,24},5->{6,8,22},6->{7,21},7->{7,21},8->{6,8 ,22},9->{10,19},10->{10,19},11->{12,17},12->{12,17},13->{14,15},14->{14,15},15->{13,16},16->{},17->{11,18} ,18->{13,16},19->{9,20},20->{5,23},21->{6,8,22},22->{9,20},23->{11,18},24->{1,25},25->{5,23}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(0,25) ,(1,2) ,(1,24) ,(2,3) ,(2,4) ,(3,2) ,(4,3) ,(4,4) ,(5,22) ,(6,21) ,(8,6) ,(9,19) ,(11,17) ,(13,15) ,(18,16) ,(21,8) ,(22,20) ,(23,18) ,(25,23)] * Step 3: Looptree YES + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f15(50,5,0,D,E,F,G,H,I,J,K,L,M) True (1,1) 1. f15(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f19(A,B,C,0,0,F,G,H,I,J,K,L,M) [C >= 0 (?,1) && -5 + B + C >= 0 && 5 + -1*B + C >= 0 && -50 + A + C >= 0 && 50 + -1*A + C >= 0 && 5 + -1*B >= 0 && -45 + A + -1*B >= 0 && 55 + -1*A + -1*B >= 0 && -5 + B >= 0 && -55 + A + B >= 0 && 45 + -1*A + B >= 0 && 50 + -1*A >= 0 && -50 + A >= 0 && B >= C] 2. f19(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f19(A,B,C,D + N,1 + E,F,G,H,I,J,K,L,M) [E >= 0 (?,1) && C + E >= 0 && -5 + B + E >= 0 && 5 + -1*B + E >= 0 && -50 + A + E >= 0 && 50 + -1*A + E >= 0 && C >= 0 && -5 + B + C >= 0 && 5 + -1*B + C >= 0 && -50 + A + C >= 0 && 50 + -1*A + C >= 0 && 5 + -1*B >= 0 && -45 + A + -1*B >= 0 && 55 + -1*A + -1*B >= 0 && -5 + B >= 0 && -55 + A + B >= 0 && 45 + -1*A + B >= 0 && 50 + -1*A >= 0 && -50 + A >= 0 && B >= E && E >= 1 + C] 3. f19(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f19(A,B,C,D + N,1 + E,F,G,H,I,J,K,L,M) [E >= 0 (?,1) && C + E >= 0 && -5 + B + E >= 0 && 5 + -1*B + E >= 0 && -50 + A + E >= 0 && 50 + -1*A + E >= 0 && C >= 0 && -5 + B + C >= 0 && 5 + -1*B + C >= 0 && -50 + A + C >= 0 && 50 + -1*A + C >= 0 && 5 + -1*B >= 0 && -45 + A + -1*B >= 0 && 55 + -1*A + -1*B >= 0 && -5 + B >= 0 && -55 + A + B >= 0 && 45 + -1*A + B >= 0 && 50 + -1*A >= 0 && -50 + A >= 0 && C >= 1 + E && B >= E] 4. f19(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f19(A,B,C,D + N,1 + C,F,G,H,I,J,K,L,M) [E >= 0 (?,1) && C + E >= 0 && -5 + B + E >= 0 && 5 + -1*B + E >= 0 && -50 + A + E >= 0 && 50 + -1*A + E >= 0 && C >= 0 && -5 + B + C >= 0 && 5 + -1*B + C >= 0 && -50 + A + C >= 0 && 50 + -1*A + C >= 0 && 5 + -1*B >= 0 && -45 + A + -1*B >= 0 && 55 + -1*A + -1*B >= 0 && -5 + B >= 0 && -55 + A + B >= 0 && 45 + -1*A + B >= 0 && 50 + -1*A >= 0 && -50 + A >= 0 && B >= E && C = E] 5. f33(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f36(A,B,C,D,E,F,G,1 + G,I,J,K,L,M) [G >= 0 (?,1) && -5 + F + G >= 0 && 5 + -1*F + G >= 0 && -6 + C + G >= 0 && -5 + B + G >= 0 && 5 + -1*B + G >= 0 && -50 + G + M >= 0 && 50 + G + -1*M >= 0 && -50 + A + G >= 0 && 50 + -1*A + G >= 0 && 5 + -1*F >= 0 && -1 + C + -1*F >= 0 && B + -1*F >= 0 && 10 + -1*B + -1*F >= 0 && -45 + -1*F + M >= 0 && 55 + -1*F + -1*M >= 0 && -45 + A + -1*F >= 0 && 55 + -1*A + -1*F >= 0 && -5 + F >= 0 && -11 + C + F >= 0 && -10 + B + F >= 0 && -1*B + F >= 0 && -55 + F + M >= 0 && 45 + F + -1*M >= 0 && -55 + A + F >= 0 && 45 + -1*A + F >= 0 && -6 + C >= 0 && -11 + B + C >= 0 && -1 + -1*B + C >= 0 && -56 + C + M >= 0 && 44 + C + -1*M >= 0 && -56 + A + C >= 0 && 44 + -1*A + C >= 0 && 5 + -1*B >= 0 && -45 + -1*B + M >= 0 && 55 + -1*B + -1*M >= 0 && -45 + A + -1*B >= 0 && 55 + -1*A + -1*B >= 0 && -5 + B >= 0 && -55 + B + M >= 0 && 45 + B + -1*M >= 0 && -55 + A + B >= 0 && 45 + -1*A + B >= 0 && 50 + -1*M >= 0 && A + -1*M >= 0 && 100 + -1*A + -1*M >= 0 && -50 + M >= 0 && -100 + A + M >= 0 && -1*A + M >= 0 && 50 + -1*A >= 0 && -50 + A >= 0 && F >= 1 + G] 6. f36(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f41(A,B,C,D,E,F,G,H,N,0,K,L,M) [-1 + H >= 0 (?,1) && -1 + G + H >= 0 && -1 + -1*G + H >= 0 && -6 + F + H >= 0 && 4 + -1*F + H >= 0 && -7 + C + H >= 0 && -6 + B + H >= 0 && 4 + -1*B + H >= 0 && -51 + H + M >= 0 && 49 + H + -1*M >= 0 && -51 + A + H >= 0 && 49 + -1*A + H >= 0 && 4 + -1*G >= 0 && -1 + F + -1*G >= 0 && 9 + -1*F + -1*G >= 0 && -2 + C + -1*G >= 0 && -1 + B + -1*G >= 0 && 9 + -1*B + -1*G >= 0 && -46 + -1*G + M >= 0 && 54 + -1*G + -1*M >= 0 && -46 + A + -1*G >= 0 && 54 + -1*A + -1*G >= 0 && G >= 0 && -5 + F + G >= 0 && 5 + -1*F + G >= 0 && -6 + C + G >= 0 && -5 + B + G >= 0 && 5 + -1*B + G >= 0 && -50 + G + M >= 0 && 50 + G + -1*M >= 0 && -50 + A + G >= 0 && 50 + -1*A + G >= 0 && 5 + -1*F >= 0 && -1 + C + -1*F >= 0 && B + -1*F >= 0 && 10 + -1*B + -1*F >= 0 && -45 + -1*F + M >= 0 && 55 + -1*F + -1*M >= 0 && -45 + A + -1*F >= 0 && 55 + -1*A + -1*F >= 0 && -5 + F >= 0 && -11 + C + F >= 0 && -10 + B + F >= 0 && -1*B + F >= 0 && -55 + F + M >= 0 && 45 + F + -1*M >= 0 && -55 + A + F >= 0 && 45 + -1*A + F >= 0 && -6 + C >= 0 && -11 + B + C >= 0 && -1 + -1*B + C >= 0 && -56 + C + M >= 0 && 44 + C + -1*M >= 0 && -56 + A + C >= 0 && 44 + -1*A + C >= 0 && 5 + -1*B >= 0 && -45 + -1*B + M >= 0 && 55 + -1*B + -1*M >= 0 && -45 + A + -1*B >= 0 && 55 + -1*A + -1*B >= 0 && -5 + B >= 0 && -55 + B + M >= 0 && 45 + B + -1*M >= 0 && -55 + A + B >= 0 && 45 + -1*A + B >= 0 && 50 + -1*M >= 0 && A + -1*M >= 0 && 100 + -1*A + -1*M >= 0 && -50 + M >= 0 && -100 + A + M >= 0 && -1*A + M >= 0 && 50 + -1*A >= 0 && -50 + A >= 0 && G >= 1 && F >= H] 7. f41(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f41(A,B,C,D,E,F,G,H,N,1 + J,K,L,M) [5 + -1*H >= 0 (?,1) && 4 + G + -1*H >= 0 && 9 + -1*G + -1*H >= 0 && F + -1*H >= 0 && 10 + -1*F + -1*H >= 0 && -1 + C + -1*H >= 0 && B + -1*H >= 0 && 10 + -1*B + -1*H >= 0 && -45 + -1*H + M >= 0 && 55 + -1*H + -1*M >= 0 && 5 + -1*H + J >= 0 && -45 + A + -1*H >= 0 && 55 + -1*A + -1*H >= 0 && -2 + H >= 0 && -3 + G + H >= 0 && -1 + -1*G + H >= 0 && -7 + F + H >= 0 && 3 + -1*F + H >= 0 && -8 + C + H >= 0 && -7 + B + H >= 0 && 3 + -1*B + H >= 0 && -52 + H + M >= 0 && 48 + H + -1*M >= 0 && -2 + H + J >= 0 && -52 + A + H >= 0 && 48 + -1*A + H >= 0 && 4 + -1*G >= 0 && -1 + F + -1*G >= 0 && 9 + -1*F + -1*G >= 0 && -2 + C + -1*G >= 0 && -1 + B + -1*G >= 0 && 9 + -1*B + -1*G >= 0 && -46 + -1*G + M >= 0 && 54 + -1*G + -1*M >= 0 && 4 + -1*G + J >= 0 && -46 + A + -1*G >= 0 && 54 + -1*A + -1*G >= 0 && -1 + G >= 0 && -6 + F + G >= 0 && 4 + -1*F + G >= 0 && -7 + C + G >= 0 && -6 + B + G >= 0 && 4 + -1*B + G >= 0 && -51 + G + M >= 0 && 49 + G + -1*M >= 0 && -1 + G + J >= 0 && -51 + A + G >= 0 && 49 + -1*A + G >= 0 && 5 + -1*F >= 0 && -1 + C + -1*F >= 0 && B + -1*F >= 0 && 10 + -1*B + -1*F >= 0 && -45 + -1*F + M >= 0 && 55 + -1*F + -1*M >= 0 && 5 + -1*F + J >= 0 && -45 + A + -1*F >= 0 && 55 + -1*A + -1*F >= 0 && -5 + F >= 0 && -11 + C + F >= 0 && -10 + B + F >= 0 && -1*B + F >= 0 && -55 + F + M >= 0 && 45 + F + -1*M >= 0 && -5 + F + J >= 0 && -55 + A + F >= 0 && 45 + -1*A + F >= 0 && -6 + C >= 0 && -11 + B + C >= 0 && -1 + -1*B + C >= 0 && -56 + C + M >= 0 && 44 + C + -1*M >= 0 && -6 + C + J >= 0 && -56 + A + C >= 0 && 44 + -1*A + C >= 0 && 5 + -1*B >= 0 && -45 + -1*B + M >= 0 && 55 + -1*B + -1*M >= 0 && 5 + -1*B + J >= 0 && -45 + A + -1*B >= 0 && 55 + -1*A + -1*B >= 0 && -5 + B >= 0 && -55 + B + M >= 0 && 45 + B + -1*M >= 0 && -5 + B + J >= 0 && -55 + A + B >= 0 && 45 + -1*A + B >= 0 && 50 + -1*M >= 0 && 50 + J + -1*M >= 0 && A + -1*M >= 0 && 100 + -1*A + -1*M >= 0 && -50 + M >= 0 && -50 + J + M >= 0 && -100 + A + M >= 0 && -1*A + M >= 0 && J >= 0 && -50 + A + J >= 0 && 50 + -1*A + J >= 0 && 50 + -1*A >= 0 && -50 + A >= 0 && G >= 1 + J] 8. f36(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f36(A,B,C,D,E,F,0,1 + H,N,J,K,L,M) [-1 + H >= 0 (?,1) && -1 + G + H >= 0 && -1 + -1*G + H >= 0 && -6 + F + H >= 0 && 4 + -1*F + H >= 0 && -7 + C + H >= 0 && -6 + B + H >= 0 && 4 + -1*B + H >= 0 && -51 + H + M >= 0 && 49 + H + -1*M >= 0 && -51 + A + H >= 0 && 49 + -1*A + H >= 0 && 4 + -1*G >= 0 && -1 + F + -1*G >= 0 && 9 + -1*F + -1*G >= 0 && -2 + C + -1*G >= 0 && -1 + B + -1*G >= 0 && 9 + -1*B + -1*G >= 0 && -46 + -1*G + M >= 0 && 54 + -1*G + -1*M >= 0 && -46 + A + -1*G >= 0 && 54 + -1*A + -1*G >= 0 && G >= 0 && -5 + F + G >= 0 && 5 + -1*F + G >= 0 && -6 + C + G >= 0 && -5 + B + G >= 0 && 5 + -1*B + G >= 0 && -50 + G + M >= 0 && 50 + G + -1*M >= 0 && -50 + A + G >= 0 && 50 + -1*A + G >= 0 && 5 + -1*F >= 0 && -1 + C + -1*F >= 0 && B + -1*F >= 0 && 10 + -1*B + -1*F >= 0 && -45 + -1*F + M >= 0 && 55 + -1*F + -1*M >= 0 && -45 + A + -1*F >= 0 && 55 + -1*A + -1*F >= 0 && -5 + F >= 0 && -11 + C + F >= 0 && -10 + B + F >= 0 && -1*B + F >= 0 && -55 + F + M >= 0 && 45 + F + -1*M >= 0 && -55 + A + F >= 0 && 45 + -1*A + F >= 0 && -6 + C >= 0 && -11 + B + C >= 0 && -1 + -1*B + C >= 0 && -56 + C + M >= 0 && 44 + C + -1*M >= 0 && -56 + A + C >= 0 && 44 + -1*A + C >= 0 && 5 + -1*B >= 0 && -45 + -1*B + M >= 0 && 55 + -1*B + -1*M >= 0 && -45 + A + -1*B >= 0 && 55 + -1*A + -1*B >= 0 && -5 + B >= 0 && -55 + B + M >= 0 && 45 + B + -1*M >= 0 && -55 + A + B >= 0 && 45 + -1*A + B >= 0 && 50 + -1*M >= 0 && A + -1*M >= 0 && 100 + -1*A + -1*M >= 0 && -50 + M >= 0 && -100 + A + M >= 0 && -1*A + M >= 0 && 50 + -1*A >= 0 && -50 + A >= 0 && F >= H && G = 0] 9. f50(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f54(A,B,C,D,E,F,G,H,N,0,K,L,M) [-1 + H >= 0 (?,1) && -1 + G + H >= 0 && -1 + -1*G + H >= 0 && -6 + F + H >= 0 && 4 + -1*F + H >= 0 && -7 + C + H >= 0 && -6 + B + H >= 0 && 4 + -1*B + H >= 0 && -51 + H + M >= 0 && 49 + H + -1*M >= 0 && -51 + A + H >= 0 && 49 + -1*A + H >= 0 && G >= 0 && -5 + F + G >= 0 && 5 + -1*F + G >= 0 && -6 + C + G >= 0 && -5 + B + G >= 0 && 5 + -1*B + G >= 0 && -50 + G + M >= 0 && 50 + G + -1*M >= 0 && -50 + A + G >= 0 && 50 + -1*A + G >= 0 && 5 + -1*F >= 0 && -1 + C + -1*F >= 0 && B + -1*F >= 0 && 10 + -1*B + -1*F >= 0 && -45 + -1*F + M >= 0 && 55 + -1*F + -1*M >= 0 && -45 + A + -1*F >= 0 && 55 + -1*A + -1*F >= 0 && -5 + F >= 0 && -11 + C + F >= 0 && -10 + B + F >= 0 && -1*B + F >= 0 && -55 + F + M >= 0 && 45 + F + -1*M >= 0 && -55 + A + F >= 0 && 45 + -1*A + F >= 0 && -6 + C >= 0 && -11 + B + C >= 0 && -1 + -1*B + C >= 0 && -56 + C + M >= 0 && 44 + C + -1*M >= 0 && -56 + A + C >= 0 && 44 + -1*A + C >= 0 && 5 + -1*B >= 0 && -45 + -1*B + M >= 0 && 55 + -1*B + -1*M >= 0 && -45 + A + -1*B >= 0 && 55 + -1*A + -1*B >= 0 && -5 + B >= 0 && -55 + B + M >= 0 && 45 + B + -1*M >= 0 && -55 + A + B >= 0 && 45 + -1*A + B >= 0 && 50 + -1*M >= 0 && A + -1*M >= 0 && 100 + -1*A + -1*M >= 0 && -50 + M >= 0 && -100 + A + M >= 0 && -1*A + M >= 0 && 50 + -1*A >= 0 && -50 + A >= 0 && F >= H] 10. f54(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f54(A,B,C,D,E,F,G,H,N,1 + J,K,L,M) [-1 + H >= 0 (?,1) && -1 + G + H >= 0 && -1 + -1*G + H >= 0 && -6 + F + H >= 0 && 4 + -1*F + H >= 0 && -7 + C + H >= 0 && -6 + B + H >= 0 && 4 + -1*B + H >= 0 && -51 + H + M >= 0 && 49 + H + -1*M >= 0 && -1 + H + J >= 0 && -51 + A + H >= 0 && 49 + -1*A + H >= 0 && 4 + -1*G >= 0 && -1 + F + -1*G >= 0 && 9 + -1*F + -1*G >= 0 && -2 + C + -1*G >= 0 && -1 + B + -1*G >= 0 && 9 + -1*B + -1*G >= 0 && -46 + -1*G + M >= 0 && 54 + -1*G + -1*M >= 0 && 4 + -1*G + J >= 0 && -46 + A + -1*G >= 0 && 54 + -1*A + -1*G >= 0 && G >= 0 && -5 + F + G >= 0 && 5 + -1*F + G >= 0 && -6 + C + G >= 0 && -5 + B + G >= 0 && 5 + -1*B + G >= 0 && -50 + G + M >= 0 && 50 + G + -1*M >= 0 && G + J >= 0 && -50 + A + G >= 0 && 50 + -1*A + G >= 0 && 5 + -1*F >= 0 && -1 + C + -1*F >= 0 && B + -1*F >= 0 && 10 + -1*B + -1*F >= 0 && -45 + -1*F + M >= 0 && 55 + -1*F + -1*M >= 0 && 5 + -1*F + J >= 0 && -45 + A + -1*F >= 0 && 55 + -1*A + -1*F >= 0 && -5 + F >= 0 && -11 + C + F >= 0 && -10 + B + F >= 0 && -1*B + F >= 0 && -55 + F + M >= 0 && 45 + F + -1*M >= 0 && -5 + F + J >= 0 && -55 + A + F >= 0 && 45 + -1*A + F >= 0 && -6 + C >= 0 && -11 + B + C >= 0 && -1 + -1*B + C >= 0 && -56 + C + M >= 0 && 44 + C + -1*M >= 0 && -6 + C + J >= 0 && -56 + A + C >= 0 && 44 + -1*A + C >= 0 && 5 + -1*B >= 0 && -45 + -1*B + M >= 0 && 55 + -1*B + -1*M >= 0 && 5 + -1*B + J >= 0 && -45 + A + -1*B >= 0 && 55 + -1*A + -1*B >= 0 && -5 + B >= 0 && -55 + B + M >= 0 && 45 + B + -1*M >= 0 && -5 + B + J >= 0 && -55 + A + B >= 0 && 45 + -1*A + B >= 0 && 50 + -1*M >= 0 && 50 + J + -1*M >= 0 && A + -1*M >= 0 && 100 + -1*A + -1*M >= 0 && -50 + M >= 0 && -50 + J + M >= 0 && -100 + A + M >= 0 && -1*A + M >= 0 && J >= 0 && -50 + A + J >= 0 && 50 + -1*A + J >= 0 && 50 + -1*A >= 0 && -50 + A >= 0 && G >= J] 11. f66(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f70(A,B,C,D,E,F,G,0,N,J,K,L,M) [-1 + G >= 0 (?,1) && -6 + F + G >= 0 && 4 + -1*F + G >= 0 && -7 + C + G >= 0 && -6 + B + G >= 0 && 4 + -1*B + G >= 0 && -51 + G + M >= 0 && 49 + G + -1*M >= 0 && -51 + A + G >= 0 && 49 + -1*A + G >= 0 && 5 + -1*F >= 0 && -1 + C + -1*F >= 0 && B + -1*F >= 0 && 10 + -1*B + -1*F >= 0 && -45 + -1*F + M >= 0 && 55 + -1*F + -1*M >= 0 && -45 + A + -1*F >= 0 && 55 + -1*A + -1*F >= 0 && -5 + F >= 0 && -11 + C + F >= 0 && -10 + B + F >= 0 && -1*B + F >= 0 && -55 + F + M >= 0 && 45 + F + -1*M >= 0 && -55 + A + F >= 0 && 45 + -1*A + F >= 0 && -6 + C >= 0 && -11 + B + C >= 0 && -1 + -1*B + C >= 0 && -56 + C + M >= 0 && 44 + C + -1*M >= 0 && -56 + A + C >= 0 && 44 + -1*A + C >= 0 && 5 + -1*B >= 0 && -45 + -1*B + M >= 0 && 55 + -1*B + -1*M >= 0 && -45 + A + -1*B >= 0 && 55 + -1*A + -1*B >= 0 && -5 + B >= 0 && -55 + B + M >= 0 && 45 + B + -1*M >= 0 && -55 + A + B >= 0 && 45 + -1*A + B >= 0 && 50 + -1*M >= 0 && A + -1*M >= 0 && 100 + -1*A + -1*M >= 0 && -50 + M >= 0 && -100 + A + M >= 0 && -1*A + M >= 0 && 50 + -1*A >= 0 && -50 + A >= 0 && F >= G] 12. f70(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f70(A,B,C,D,E,F,G,1 + H,N,J,K,L,M) [H >= 0 (?,1) && -1 + G + H >= 0 && -5 + F + H >= 0 && 5 + -1*F + H >= 0 && -6 + C + H >= 0 && -5 + B + H >= 0 && 5 + -1*B + H >= 0 && -50 + H + M >= 0 && 50 + H + -1*M >= 0 && -50 + A + H >= 0 && 50 + -1*A + H >= 0 && -1 + G >= 0 && -6 + F + G >= 0 && 4 + -1*F + G >= 0 && -7 + C + G >= 0 && -6 + B + G >= 0 && 4 + -1*B + G >= 0 && -51 + G + M >= 0 && 49 + G + -1*M >= 0 && -51 + A + G >= 0 && 49 + -1*A + G >= 0 && 5 + -1*F >= 0 && -1 + C + -1*F >= 0 && B + -1*F >= 0 && 10 + -1*B + -1*F >= 0 && -45 + -1*F + M >= 0 && 55 + -1*F + -1*M >= 0 && -45 + A + -1*F >= 0 && 55 + -1*A + -1*F >= 0 && -5 + F >= 0 && -11 + C + F >= 0 && -10 + B + F >= 0 && -1*B + F >= 0 && -55 + F + M >= 0 && 45 + F + -1*M >= 0 && -55 + A + F >= 0 && 45 + -1*A + F >= 0 && -6 + C >= 0 && -11 + B + C >= 0 && -1 + -1*B + C >= 0 && -56 + C + M >= 0 && 44 + C + -1*M >= 0 && -56 + A + C >= 0 && 44 + -1*A + C >= 0 && 5 + -1*B >= 0 && -45 + -1*B + M >= 0 && 55 + -1*B + -1*M >= 0 && -45 + A + -1*B >= 0 && 55 + -1*A + -1*B >= 0 && -5 + B >= 0 && -55 + B + M >= 0 && 45 + B + -1*M >= 0 && -55 + A + B >= 0 && 45 + -1*A + B >= 0 && 50 + -1*M >= 0 && A + -1*M >= 0 && 100 + -1*A + -1*M >= 0 && -50 + M >= 0 && -100 + A + M >= 0 && -1*A + M >= 0 && 50 + -1*A >= 0 && -50 + A >= 0 && G >= 1 + H] 13. f80(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f84(A,B,C,D,E,F,G,1 + G,N,J,K,L,M) [4 + -1*G >= 0 (?,1) && -1 + F + -1*G >= 0 && 9 + -1*F + -1*G >= 0 && -2 + C + -1*G >= 0 && -1 + B + -1*G >= 0 && 9 + -1*B + -1*G >= 0 && -46 + -1*G + M >= 0 && 54 + -1*G + -1*M >= 0 && -46 + A + -1*G >= 0 && 54 + -1*A + -1*G >= 0 && 5 + -1*F >= 0 && -1 + C + -1*F >= 0 && B + -1*F >= 0 && 10 + -1*B + -1*F >= 0 && -45 + -1*F + M >= 0 && 55 + -1*F + -1*M >= 0 && -45 + A + -1*F >= 0 && 55 + -1*A + -1*F >= 0 && -5 + F >= 0 && -11 + C + F >= 0 && -10 + B + F >= 0 && -1*B + F >= 0 && -55 + F + M >= 0 && 45 + F + -1*M >= 0 && -55 + A + F >= 0 && 45 + -1*A + F >= 0 && -6 + C >= 0 && -11 + B + C >= 0 && -1 + -1*B + C >= 0 && -56 + C + M >= 0 && 44 + C + -1*M >= 0 && -56 + A + C >= 0 && 44 + -1*A + C >= 0 && 5 + -1*B >= 0 && -45 + -1*B + M >= 0 && 55 + -1*B + -1*M >= 0 && -45 + A + -1*B >= 0 && 55 + -1*A + -1*B >= 0 && -5 + B >= 0 && -55 + B + M >= 0 && 45 + B + -1*M >= 0 && -55 + A + B >= 0 && 45 + -1*A + B >= 0 && 50 + -1*M >= 0 && A + -1*M >= 0 && 100 + -1*A + -1*M >= 0 && -50 + M >= 0 && -100 + A + M >= 0 && -1*A + M >= 0 && 50 + -1*A >= 0 && -50 + A >= 0 && G >= 0] 14. f84(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f84(A,B,C,D,E,F,G,1 + H,N,J,K,L,M) [-1 + -1*G + H >= 0 (?,1) && 4 + -1*G >= 0 && -1 + F + -1*G >= 0 && 9 + -1*F + -1*G >= 0 && -2 + C + -1*G >= 0 && -1 + B + -1*G >= 0 && 9 + -1*B + -1*G >= 0 && -46 + -1*G + M >= 0 && 54 + -1*G + -1*M >= 0 && -46 + A + -1*G >= 0 && 54 + -1*A + -1*G >= 0 && 5 + -1*F >= 0 && -1 + C + -1*F >= 0 && B + -1*F >= 0 && 10 + -1*B + -1*F >= 0 && -45 + -1*F + M >= 0 && 55 + -1*F + -1*M >= 0 && -45 + A + -1*F >= 0 && 55 + -1*A + -1*F >= 0 && -5 + F >= 0 && -11 + C + F >= 0 && -10 + B + F >= 0 && -1*B + F >= 0 && -55 + F + M >= 0 && 45 + F + -1*M >= 0 && -55 + A + F >= 0 && 45 + -1*A + F >= 0 && -6 + C >= 0 && -11 + B + C >= 0 && -1 + -1*B + C >= 0 && -56 + C + M >= 0 && 44 + C + -1*M >= 0 && -56 + A + C >= 0 && 44 + -1*A + C >= 0 && 5 + -1*B >= 0 && -45 + -1*B + M >= 0 && 55 + -1*B + -1*M >= 0 && -45 + A + -1*B >= 0 && 55 + -1*A + -1*B >= 0 && -5 + B >= 0 && -55 + B + M >= 0 && 45 + B + -1*M >= 0 && -55 + A + B >= 0 && 45 + -1*A + B >= 0 && 50 + -1*M >= 0 && A + -1*M >= 0 && 100 + -1*A + -1*M >= 0 && -50 + M >= 0 && -100 + A + M >= 0 && -1*A + M >= 0 && 50 + -1*A >= 0 && -50 + A >= 0 && F >= H] 15. f84(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f80(A,B,C,D,E,F,-1 + G,H,I,J,K,L,M) [-1 + -1*G + H >= 0 (?,1) && 4 + -1*G >= 0 && -1 + F + -1*G >= 0 && 9 + -1*F + -1*G >= 0 && -2 + C + -1*G >= 0 && -1 + B + -1*G >= 0 && 9 + -1*B + -1*G >= 0 && -46 + -1*G + M >= 0 && 54 + -1*G + -1*M >= 0 && -46 + A + -1*G >= 0 && 54 + -1*A + -1*G >= 0 && 5 + -1*F >= 0 && -1 + C + -1*F >= 0 && B + -1*F >= 0 && 10 + -1*B + -1*F >= 0 && -45 + -1*F + M >= 0 && 55 + -1*F + -1*M >= 0 && -45 + A + -1*F >= 0 && 55 + -1*A + -1*F >= 0 && -5 + F >= 0 && -11 + C + F >= 0 && -10 + B + F >= 0 && -1*B + F >= 0 && -55 + F + M >= 0 && 45 + F + -1*M >= 0 && -55 + A + F >= 0 && 45 + -1*A + F >= 0 && -6 + C >= 0 && -11 + B + C >= 0 && -1 + -1*B + C >= 0 && -56 + C + M >= 0 && 44 + C + -1*M >= 0 && -56 + A + C >= 0 && 44 + -1*A + C >= 0 && 5 + -1*B >= 0 && -45 + -1*B + M >= 0 && 55 + -1*B + -1*M >= 0 && -45 + A + -1*B >= 0 && 55 + -1*A + -1*B >= 0 && -5 + B >= 0 && -55 + B + M >= 0 && 45 + B + -1*M >= 0 && -55 + A + B >= 0 && 45 + -1*A + B >= 0 && 50 + -1*M >= 0 && A + -1*M >= 0 && 100 + -1*A + -1*M >= 0 && -50 + M >= 0 && -100 + A + M >= 0 && -1*A + M >= 0 && 50 + -1*A >= 0 && -50 + A >= 0 && H >= 1 + F] 16. f80(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f96(A,B,C,D,E,F,G,H,I,J,0,0,M) [4 + -1*G >= 0 (1,1) && -1 + F + -1*G >= 0 && 9 + -1*F + -1*G >= 0 && -2 + C + -1*G >= 0 && -1 + B + -1*G >= 0 && 9 + -1*B + -1*G >= 0 && -46 + -1*G + M >= 0 && 54 + -1*G + -1*M >= 0 && -46 + A + -1*G >= 0 && 54 + -1*A + -1*G >= 0 && 5 + -1*F >= 0 && -1 + C + -1*F >= 0 && B + -1*F >= 0 && 10 + -1*B + -1*F >= 0 && -45 + -1*F + M >= 0 && 55 + -1*F + -1*M >= 0 && -45 + A + -1*F >= 0 && 55 + -1*A + -1*F >= 0 && -5 + F >= 0 && -11 + C + F >= 0 && -10 + B + F >= 0 && -1*B + F >= 0 && -55 + F + M >= 0 && 45 + F + -1*M >= 0 && -55 + A + F >= 0 && 45 + -1*A + F >= 0 && -6 + C >= 0 && -11 + B + C >= 0 && -1 + -1*B + C >= 0 && -56 + C + M >= 0 && 44 + C + -1*M >= 0 && -56 + A + C >= 0 && 44 + -1*A + C >= 0 && 5 + -1*B >= 0 && -45 + -1*B + M >= 0 && 55 + -1*B + -1*M >= 0 && -45 + A + -1*B >= 0 && 55 + -1*A + -1*B >= 0 && -5 + B >= 0 && -55 + B + M >= 0 && 45 + B + -1*M >= 0 && -55 + A + B >= 0 && 45 + -1*A + B >= 0 && 50 + -1*M >= 0 && A + -1*M >= 0 && 100 + -1*A + -1*M >= 0 && -50 + M >= 0 && -100 + A + M >= 0 && -1*A + M >= 0 && 50 + -1*A >= 0 && -50 + A >= 0 && 0 >= 1 + G] 17. f70(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f66(A,B,C,D,E,F,1 + G,H,I,J,K,L,M) [H >= 0 (?,1) && -1 + G + H >= 0 && -5 + F + H >= 0 && 5 + -1*F + H >= 0 && -6 + C + H >= 0 && -5 + B + H >= 0 && 5 + -1*B + H >= 0 && -50 + H + M >= 0 && 50 + H + -1*M >= 0 && -50 + A + H >= 0 && 50 + -1*A + H >= 0 && -1 + G >= 0 && -6 + F + G >= 0 && 4 + -1*F + G >= 0 && -7 + C + G >= 0 && -6 + B + G >= 0 && 4 + -1*B + G >= 0 && -51 + G + M >= 0 && 49 + G + -1*M >= 0 && -51 + A + G >= 0 && 49 + -1*A + G >= 0 && 5 + -1*F >= 0 && -1 + C + -1*F >= 0 && B + -1*F >= 0 && 10 + -1*B + -1*F >= 0 && -45 + -1*F + M >= 0 && 55 + -1*F + -1*M >= 0 && -45 + A + -1*F >= 0 && 55 + -1*A + -1*F >= 0 && -5 + F >= 0 && -11 + C + F >= 0 && -10 + B + F >= 0 && -1*B + F >= 0 && -55 + F + M >= 0 && 45 + F + -1*M >= 0 && -55 + A + F >= 0 && 45 + -1*A + F >= 0 && -6 + C >= 0 && -11 + B + C >= 0 && -1 + -1*B + C >= 0 && -56 + C + M >= 0 && 44 + C + -1*M >= 0 && -56 + A + C >= 0 && 44 + -1*A + C >= 0 && 5 + -1*B >= 0 && -45 + -1*B + M >= 0 && 55 + -1*B + -1*M >= 0 && -45 + A + -1*B >= 0 && 55 + -1*A + -1*B >= 0 && -5 + B >= 0 && -55 + B + M >= 0 && 45 + B + -1*M >= 0 && -55 + A + B >= 0 && 45 + -1*A + B >= 0 && 50 + -1*M >= 0 && A + -1*M >= 0 && 100 + -1*A + -1*M >= 0 && -50 + M >= 0 && -100 + A + M >= 0 && -1*A + M >= 0 && 50 + -1*A >= 0 && -50 + A >= 0 && H >= G] 18. f66(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f80(A,B,C,D,E,F,-1 + F,H,I,J,K,L,M) [-1 + G >= 0 (1,1) && -6 + F + G >= 0 && 4 + -1*F + G >= 0 && -7 + C + G >= 0 && -6 + B + G >= 0 && 4 + -1*B + G >= 0 && -51 + G + M >= 0 && 49 + G + -1*M >= 0 && -51 + A + G >= 0 && 49 + -1*A + G >= 0 && 5 + -1*F >= 0 && -1 + C + -1*F >= 0 && B + -1*F >= 0 && 10 + -1*B + -1*F >= 0 && -45 + -1*F + M >= 0 && 55 + -1*F + -1*M >= 0 && -45 + A + -1*F >= 0 && 55 + -1*A + -1*F >= 0 && -5 + F >= 0 && -11 + C + F >= 0 && -10 + B + F >= 0 && -1*B + F >= 0 && -55 + F + M >= 0 && 45 + F + -1*M >= 0 && -55 + A + F >= 0 && 45 + -1*A + F >= 0 && -6 + C >= 0 && -11 + B + C >= 0 && -1 + -1*B + C >= 0 && -56 + C + M >= 0 && 44 + C + -1*M >= 0 && -56 + A + C >= 0 && 44 + -1*A + C >= 0 && 5 + -1*B >= 0 && -45 + -1*B + M >= 0 && 55 + -1*B + -1*M >= 0 && -45 + A + -1*B >= 0 && 55 + -1*A + -1*B >= 0 && -5 + B >= 0 && -55 + B + M >= 0 && 45 + B + -1*M >= 0 && -55 + A + B >= 0 && 45 + -1*A + B >= 0 && 50 + -1*M >= 0 && A + -1*M >= 0 && 100 + -1*A + -1*M >= 0 && -50 + M >= 0 && -100 + A + M >= 0 && -1*A + M >= 0 && 50 + -1*A >= 0 && -50 + A >= 0 && G >= 1 + F] 19. f54(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f50(A,B,C,D,E,F,G,1 + H,I,J,K,L,M) [-1 + H >= 0 (?,1) && -1 + G + H >= 0 && -1 + -1*G + H >= 0 && -6 + F + H >= 0 && 4 + -1*F + H >= 0 && -7 + C + H >= 0 && -6 + B + H >= 0 && 4 + -1*B + H >= 0 && -51 + H + M >= 0 && 49 + H + -1*M >= 0 && -1 + H + J >= 0 && -51 + A + H >= 0 && 49 + -1*A + H >= 0 && 4 + -1*G >= 0 && -1 + F + -1*G >= 0 && 9 + -1*F + -1*G >= 0 && -2 + C + -1*G >= 0 && -1 + B + -1*G >= 0 && 9 + -1*B + -1*G >= 0 && -46 + -1*G + M >= 0 && 54 + -1*G + -1*M >= 0 && 4 + -1*G + J >= 0 && -46 + A + -1*G >= 0 && 54 + -1*A + -1*G >= 0 && G >= 0 && -5 + F + G >= 0 && 5 + -1*F + G >= 0 && -6 + C + G >= 0 && -5 + B + G >= 0 && 5 + -1*B + G >= 0 && -50 + G + M >= 0 && 50 + G + -1*M >= 0 && G + J >= 0 && -50 + A + G >= 0 && 50 + -1*A + G >= 0 && 5 + -1*F >= 0 && -1 + C + -1*F >= 0 && B + -1*F >= 0 && 10 + -1*B + -1*F >= 0 && -45 + -1*F + M >= 0 && 55 + -1*F + -1*M >= 0 && 5 + -1*F + J >= 0 && -45 + A + -1*F >= 0 && 55 + -1*A + -1*F >= 0 && -5 + F >= 0 && -11 + C + F >= 0 && -10 + B + F >= 0 && -1*B + F >= 0 && -55 + F + M >= 0 && 45 + F + -1*M >= 0 && -5 + F + J >= 0 && -55 + A + F >= 0 && 45 + -1*A + F >= 0 && -6 + C >= 0 && -11 + B + C >= 0 && -1 + -1*B + C >= 0 && -56 + C + M >= 0 && 44 + C + -1*M >= 0 && -6 + C + J >= 0 && -56 + A + C >= 0 && 44 + -1*A + C >= 0 && 5 + -1*B >= 0 && -45 + -1*B + M >= 0 && 55 + -1*B + -1*M >= 0 && 5 + -1*B + J >= 0 && -45 + A + -1*B >= 0 && 55 + -1*A + -1*B >= 0 && -5 + B >= 0 && -55 + B + M >= 0 && 45 + B + -1*M >= 0 && -5 + B + J >= 0 && -55 + A + B >= 0 && 45 + -1*A + B >= 0 && 50 + -1*M >= 0 && 50 + J + -1*M >= 0 && A + -1*M >= 0 && 100 + -1*A + -1*M >= 0 && -50 + M >= 0 && -50 + J + M >= 0 && -100 + A + M >= 0 && -1*A + M >= 0 && J >= 0 && -50 + A + J >= 0 && 50 + -1*A + J >= 0 && 50 + -1*A >= 0 && -50 + A >= 0 && J >= 1 + G] 20. f50(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f33(A,B,C,D,E,F,1 + G,H,I,J,K,L,M) [-1 + H >= 0 (?,1) && -1 + G + H >= 0 && -1 + -1*G + H >= 0 && -6 + F + H >= 0 && 4 + -1*F + H >= 0 && -7 + C + H >= 0 && -6 + B + H >= 0 && 4 + -1*B + H >= 0 && -51 + H + M >= 0 && 49 + H + -1*M >= 0 && -51 + A + H >= 0 && 49 + -1*A + H >= 0 && G >= 0 && -5 + F + G >= 0 && 5 + -1*F + G >= 0 && -6 + C + G >= 0 && -5 + B + G >= 0 && 5 + -1*B + G >= 0 && -50 + G + M >= 0 && 50 + G + -1*M >= 0 && -50 + A + G >= 0 && 50 + -1*A + G >= 0 && 5 + -1*F >= 0 && -1 + C + -1*F >= 0 && B + -1*F >= 0 && 10 + -1*B + -1*F >= 0 && -45 + -1*F + M >= 0 && 55 + -1*F + -1*M >= 0 && -45 + A + -1*F >= 0 && 55 + -1*A + -1*F >= 0 && -5 + F >= 0 && -11 + C + F >= 0 && -10 + B + F >= 0 && -1*B + F >= 0 && -55 + F + M >= 0 && 45 + F + -1*M >= 0 && -55 + A + F >= 0 && 45 + -1*A + F >= 0 && -6 + C >= 0 && -11 + B + C >= 0 && -1 + -1*B + C >= 0 && -56 + C + M >= 0 && 44 + C + -1*M >= 0 && -56 + A + C >= 0 && 44 + -1*A + C >= 0 && 5 + -1*B >= 0 && -45 + -1*B + M >= 0 && 55 + -1*B + -1*M >= 0 && -45 + A + -1*B >= 0 && 55 + -1*A + -1*B >= 0 && -5 + B >= 0 && -55 + B + M >= 0 && 45 + B + -1*M >= 0 && -55 + A + B >= 0 && 45 + -1*A + B >= 0 && 50 + -1*M >= 0 && A + -1*M >= 0 && 100 + -1*A + -1*M >= 0 && -50 + M >= 0 && -100 + A + M >= 0 && -1*A + M >= 0 && 50 + -1*A >= 0 && -50 + A >= 0 && H >= 1 + F] 21. f41(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f36(A,B,C,D,E,F,G,1 + H,I,J,K,L,M) [5 + -1*H >= 0 (?,1) && 4 + G + -1*H >= 0 && 9 + -1*G + -1*H >= 0 && F + -1*H >= 0 && 10 + -1*F + -1*H >= 0 && -1 + C + -1*H >= 0 && B + -1*H >= 0 && 10 + -1*B + -1*H >= 0 && -45 + -1*H + M >= 0 && 55 + -1*H + -1*M >= 0 && 5 + -1*H + J >= 0 && -45 + A + -1*H >= 0 && 55 + -1*A + -1*H >= 0 && -2 + H >= 0 && -3 + G + H >= 0 && -1 + -1*G + H >= 0 && -7 + F + H >= 0 && 3 + -1*F + H >= 0 && -8 + C + H >= 0 && -7 + B + H >= 0 && 3 + -1*B + H >= 0 && -52 + H + M >= 0 && 48 + H + -1*M >= 0 && -2 + H + J >= 0 && -52 + A + H >= 0 && 48 + -1*A + H >= 0 && 4 + -1*G >= 0 && -1 + F + -1*G >= 0 && 9 + -1*F + -1*G >= 0 && -2 + C + -1*G >= 0 && -1 + B + -1*G >= 0 && 9 + -1*B + -1*G >= 0 && -46 + -1*G + M >= 0 && 54 + -1*G + -1*M >= 0 && 4 + -1*G + J >= 0 && -46 + A + -1*G >= 0 && 54 + -1*A + -1*G >= 0 && -1 + G >= 0 && -6 + F + G >= 0 && 4 + -1*F + G >= 0 && -7 + C + G >= 0 && -6 + B + G >= 0 && 4 + -1*B + G >= 0 && -51 + G + M >= 0 && 49 + G + -1*M >= 0 && -1 + G + J >= 0 && -51 + A + G >= 0 && 49 + -1*A + G >= 0 && 5 + -1*F >= 0 && -1 + C + -1*F >= 0 && B + -1*F >= 0 && 10 + -1*B + -1*F >= 0 && -45 + -1*F + M >= 0 && 55 + -1*F + -1*M >= 0 && 5 + -1*F + J >= 0 && -45 + A + -1*F >= 0 && 55 + -1*A + -1*F >= 0 && -5 + F >= 0 && -11 + C + F >= 0 && -10 + B + F >= 0 && -1*B + F >= 0 && -55 + F + M >= 0 && 45 + F + -1*M >= 0 && -5 + F + J >= 0 && -55 + A + F >= 0 && 45 + -1*A + F >= 0 && -6 + C >= 0 && -11 + B + C >= 0 && -1 + -1*B + C >= 0 && -56 + C + M >= 0 && 44 + C + -1*M >= 0 && -6 + C + J >= 0 && -56 + A + C >= 0 && 44 + -1*A + C >= 0 && 5 + -1*B >= 0 && -45 + -1*B + M >= 0 && 55 + -1*B + -1*M >= 0 && 5 + -1*B + J >= 0 && -45 + A + -1*B >= 0 && 55 + -1*A + -1*B >= 0 && -5 + B >= 0 && -55 + B + M >= 0 && 45 + B + -1*M >= 0 && -5 + B + J >= 0 && -55 + A + B >= 0 && 45 + -1*A + B >= 0 && 50 + -1*M >= 0 && 50 + J + -1*M >= 0 && A + -1*M >= 0 && 100 + -1*A + -1*M >= 0 && -50 + M >= 0 && -50 + J + M >= 0 && -100 + A + M >= 0 && -1*A + M >= 0 && J >= 0 && -50 + A + J >= 0 && 50 + -1*A + J >= 0 && 50 + -1*A >= 0 && -50 + A >= 0 && J >= G] 22. f36(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f50(A,B,C,D,E,F,G,1 + G,I,J,K,L,M) [-1 + H >= 0 (?,1) && -1 + G + H >= 0 && -1 + -1*G + H >= 0 && -6 + F + H >= 0 && 4 + -1*F + H >= 0 && -7 + C + H >= 0 && -6 + B + H >= 0 && 4 + -1*B + H >= 0 && -51 + H + M >= 0 && 49 + H + -1*M >= 0 && -51 + A + H >= 0 && 49 + -1*A + H >= 0 && 4 + -1*G >= 0 && -1 + F + -1*G >= 0 && 9 + -1*F + -1*G >= 0 && -2 + C + -1*G >= 0 && -1 + B + -1*G >= 0 && 9 + -1*B + -1*G >= 0 && -46 + -1*G + M >= 0 && 54 + -1*G + -1*M >= 0 && -46 + A + -1*G >= 0 && 54 + -1*A + -1*G >= 0 && G >= 0 && -5 + F + G >= 0 && 5 + -1*F + G >= 0 && -6 + C + G >= 0 && -5 + B + G >= 0 && 5 + -1*B + G >= 0 && -50 + G + M >= 0 && 50 + G + -1*M >= 0 && -50 + A + G >= 0 && 50 + -1*A + G >= 0 && 5 + -1*F >= 0 && -1 + C + -1*F >= 0 && B + -1*F >= 0 && 10 + -1*B + -1*F >= 0 && -45 + -1*F + M >= 0 && 55 + -1*F + -1*M >= 0 && -45 + A + -1*F >= 0 && 55 + -1*A + -1*F >= 0 && -5 + F >= 0 && -11 + C + F >= 0 && -10 + B + F >= 0 && -1*B + F >= 0 && -55 + F + M >= 0 && 45 + F + -1*M >= 0 && -55 + A + F >= 0 && 45 + -1*A + F >= 0 && -6 + C >= 0 && -11 + B + C >= 0 && -1 + -1*B + C >= 0 && -56 + C + M >= 0 && 44 + C + -1*M >= 0 && -56 + A + C >= 0 && 44 + -1*A + C >= 0 && 5 + -1*B >= 0 && -45 + -1*B + M >= 0 && 55 + -1*B + -1*M >= 0 && -45 + A + -1*B >= 0 && 55 + -1*A + -1*B >= 0 && -5 + B >= 0 && -55 + B + M >= 0 && 45 + B + -1*M >= 0 && -55 + A + B >= 0 && 45 + -1*A + B >= 0 && 50 + -1*M >= 0 && A + -1*M >= 0 && 100 + -1*A + -1*M >= 0 && -50 + M >= 0 && -100 + A + M >= 0 && -1*A + M >= 0 && 50 + -1*A >= 0 && -50 + A >= 0 && H >= 1 + F] 23. f33(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f66(A,B,C,D,E,F,1,H,I,J,K,L,M) [G >= 0 (1,1) && -5 + F + G >= 0 && 5 + -1*F + G >= 0 && -6 + C + G >= 0 && -5 + B + G >= 0 && 5 + -1*B + G >= 0 && -50 + G + M >= 0 && 50 + G + -1*M >= 0 && -50 + A + G >= 0 && 50 + -1*A + G >= 0 && 5 + -1*F >= 0 && -1 + C + -1*F >= 0 && B + -1*F >= 0 && 10 + -1*B + -1*F >= 0 && -45 + -1*F + M >= 0 && 55 + -1*F + -1*M >= 0 && -45 + A + -1*F >= 0 && 55 + -1*A + -1*F >= 0 && -5 + F >= 0 && -11 + C + F >= 0 && -10 + B + F >= 0 && -1*B + F >= 0 && -55 + F + M >= 0 && 45 + F + -1*M >= 0 && -55 + A + F >= 0 && 45 + -1*A + F >= 0 && -6 + C >= 0 && -11 + B + C >= 0 && -1 + -1*B + C >= 0 && -56 + C + M >= 0 && 44 + C + -1*M >= 0 && -56 + A + C >= 0 && 44 + -1*A + C >= 0 && 5 + -1*B >= 0 && -45 + -1*B + M >= 0 && 55 + -1*B + -1*M >= 0 && -45 + A + -1*B >= 0 && 55 + -1*A + -1*B >= 0 && -5 + B >= 0 && -55 + B + M >= 0 && 45 + B + -1*M >= 0 && -55 + A + B >= 0 && 45 + -1*A + B >= 0 && 50 + -1*M >= 0 && A + -1*M >= 0 && 100 + -1*A + -1*M >= 0 && -50 + M >= 0 && -100 + A + M >= 0 && -1*A + M >= 0 && 50 + -1*A >= 0 && -50 + A >= 0 && G >= F] 24. f19(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f15(A,B,1 + C,D,E,F,G,H,I,J,K,L,M) [E >= 0 (?,1) && C + E >= 0 && -5 + B + E >= 0 && 5 + -1*B + E >= 0 && -50 + A + E >= 0 && 50 + -1*A + E >= 0 && C >= 0 && -5 + B + C >= 0 && 5 + -1*B + C >= 0 && -50 + A + C >= 0 && 50 + -1*A + C >= 0 && 5 + -1*B >= 0 && -45 + A + -1*B >= 0 && 55 + -1*A + -1*B >= 0 && -5 + B >= 0 && -55 + A + B >= 0 && 45 + -1*A + B >= 0 && 50 + -1*A >= 0 && -50 + A >= 0 && E >= 1 + B] 25. f15(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f33(A,B,C,D,E,B,0,H,I,J,K,L,A) [C >= 0 (1,1) && -5 + B + C >= 0 && 5 + -1*B + C >= 0 && -50 + A + C >= 0 && 50 + -1*A + C >= 0 && 5 + -1*B >= 0 && -45 + A + -1*B >= 0 && 55 + -1*A + -1*B >= 0 && -5 + B >= 0 && -55 + A + B >= 0 && 45 + -1*A + B >= 0 && 50 + -1*A >= 0 && -50 + A >= 0 && C >= 1 + B] Signature: {(f0,13) ;(f15,13) ;(f19,13) ;(f33,13) ;(f36,13) ;(f41,13) ;(f50,13) ;(f54,13) ;(f66,13) ;(f70,13) ;(f80,13) ;(f84,13) ;(f96,13)} Flow Graph: [0->{1},1->{3,4},2->{2,24},3->{3,4,24},4->{2,24},5->{6,8},6->{7},7->{7,21},8->{8,22},9->{10},10->{10,19} ,11->{12},12->{12,17},13->{14},14->{14,15},15->{13,16},16->{},17->{11,18},18->{13},19->{9,20},20->{5,23} ,21->{6,22},22->{9},23->{11},24->{1,25},25->{5}] + 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,19,20,21,22,23,24,25] | +- p:[1,24,2,4,3] c: [1] | | | +- p:[3] c: [3] | | | `- p:[2] c: [2] | +- p:[5,20,19,10,9,22,8,21,7,6] c: [22] | | | +- p:[9,19,10] c: [9] | | | | | `- p:[10] c: [10] | | | +- p:[8] c: [8] | | | `- p:[6,21,7] c: [21] | | | `- p:[7] c: [7] | +- p:[11,17,12] c: [11] | | | `- p:[12] c: [12] | `- p:[13,15,14] c: [13] | `- p:[14] c: [14] YES