YES(?,O(1)) * Step 1: TrivialSCCs WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f11(100,O,0,D,E,F,G,H,I,J,K,L,M,N) True (1,1) 1. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f11(100,O,1,D,E,F,G,H,I,J,K,L,M,N) True (1,1) 2. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f36(A,B,C,C,C,F,G,H,I,100,K,L,M,N) [1 + -1*C >= 0 (?,1) && -99 + A + -1*C >= 0 && 101 + -1*A + -1*C >= 0 && C >= 0 && -100 + A + C >= 0 && 100 + -1*A + C >= 0 && 100 + -1*A >= 0 && -100 + A >= 0 && 0 >= C] 3. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f23(A,B,1,1,1,100,O,0,I,J,K,L,M,N) [1 + -1*C >= 0 (?,1) && -99 + A + -1*C >= 0 && 101 + -1*A + -1*C >= 0 && C >= 0 && -100 + A + C >= 0 && 100 + -1*A + C >= 0 && 100 + -1*A >= 0 && -100 + A >= 0 && C = 1] 4. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f23(A,B,1,1,1,100,O,1,I,J,K,L,M,N) [1 + -1*C >= 0 (?,1) && -99 + A + -1*C >= 0 && 101 + -1*A + -1*C >= 0 && C >= 0 && -100 + A + C >= 0 && 100 + -1*A + C >= 0 && 100 + -1*A >= 0 && -100 + A >= 0 && C = 1] 5. f36(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f32(A,B,C,D,E,F,G,H,I,J,K,L,M,N) [-1*E >= 0 (?,1) && D + -1*E >= 0 && -1*D + -1*E >= 0 && C + -1*E >= 0 && -1*C + -1*E >= 0 && -100 + -1*E + J >= 0 && 100 + -1*E + -1*J >= 0 && -100 + A + -1*E >= 0 && 100 + -1*A + -1*E >= 0 && E >= 0 && D + E >= 0 && -1*D + E >= 0 && C + E >= 0 && -1*C + E >= 0 && -100 + E + J >= 0 && 100 + E + -1*J >= 0 && -100 + A + E >= 0 && 100 + -1*A + E >= 0 && -1*D >= 0 && C + -1*D >= 0 && -1*C + -1*D >= 0 && -100 + -1*D + J >= 0 && 100 + -1*D + -1*J >= 0 && -100 + A + -1*D >= 0 && 100 + -1*A + -1*D >= 0 && D >= 0 && C + D >= 0 && -1*C + D >= 0 && -100 + D + J >= 0 && 100 + D + -1*J >= 0 && -100 + A + D >= 0 && 100 + -1*A + D >= 0 && -1*C >= 0 && -100 + -1*C + J >= 0 && 100 + -1*C + -1*J >= 0 && -100 + A + -1*C >= 0 && 100 + -1*A + -1*C >= 0 && C >= 0 && -100 + C + J >= 0 && 100 + C + -1*J >= 0 && -100 + A + C >= 0 && 100 + -1*A + C >= 0 && 100 + -1*J >= 0 && A + -1*J >= 0 && 200 + -1*A + -1*J >= 0 && -100 + J >= 0 && -200 + A + J >= 0 && -1*A + J >= 0 && 100 + -1*A >= 0 && -100 + A >= 0] 6. f36(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f32(A,B,C,D,E,F,G,H,I,J,K,L,M,N) [-1*E >= 0 (?,1) && D + -1*E >= 0 && -1*D + -1*E >= 0 && C + -1*E >= 0 && -1*C + -1*E >= 0 && -100 + -1*E + J >= 0 && 100 + -1*E + -1*J >= 0 && -100 + A + -1*E >= 0 && 100 + -1*A + -1*E >= 0 && E >= 0 && D + E >= 0 && -1*D + E >= 0 && C + E >= 0 && -1*C + E >= 0 && -100 + E + J >= 0 && 100 + E + -1*J >= 0 && -100 + A + E >= 0 && 100 + -1*A + E >= 0 && -1*D >= 0 && C + -1*D >= 0 && -1*C + -1*D >= 0 && -100 + -1*D + J >= 0 && 100 + -1*D + -1*J >= 0 && -100 + A + -1*D >= 0 && 100 + -1*A + -1*D >= 0 && D >= 0 && C + D >= 0 && -1*C + D >= 0 && -100 + D + J >= 0 && 100 + D + -1*J >= 0 && -100 + A + D >= 0 && 100 + -1*A + D >= 0 && -1*C >= 0 && -100 + -1*C + J >= 0 && 100 + -1*C + -1*J >= 0 && -100 + A + -1*C >= 0 && 100 + -1*A + -1*C >= 0 && C >= 0 && -100 + C + J >= 0 && 100 + C + -1*J >= 0 && -100 + A + C >= 0 && 100 + -1*A + C >= 0 && 100 + -1*J >= 0 && A + -1*J >= 0 && 200 + -1*A + -1*J >= 0 && -100 + J >= 0 && -200 + A + J >= 0 && -1*A + J >= 0 && 100 + -1*A >= 0 && -100 + A >= 0 && 0 >= 1 + O] 7. f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f26(A,B,C,D,H,F,G,H,100,J,K,L,M,N) [1 + -1*H >= 0 (?,1) && -99 + F + -1*H >= 0 && 101 + -1*F + -1*H >= 0 && E + -1*H >= 0 && 2 + -1*E + -1*H >= 0 && D + -1*H >= 0 && 2 + -1*D + -1*H >= 0 && C + -1*H >= 0 && 2 + -1*C + -1*H >= 0 && -99 + A + -1*H >= 0 && 101 + -1*A + -1*H >= 0 && H >= 0 && -100 + F + H >= 0 && 100 + -1*F + H >= 0 && -1 + E + H >= 0 && 1 + -1*E + H >= 0 && -1 + D + H >= 0 && 1 + -1*D + H >= 0 && -1 + C + H >= 0 && 1 + -1*C + H >= 0 && -100 + A + H >= 0 && 100 + -1*A + H >= 0 && 100 + -1*F >= 0 && 99 + E + -1*F >= 0 && 101 + -1*E + -1*F >= 0 && 99 + D + -1*F >= 0 && 101 + -1*D + -1*F >= 0 && 99 + C + -1*F >= 0 && 101 + -1*C + -1*F >= 0 && A + -1*F >= 0 && 200 + -1*A + -1*F >= 0 && -100 + F >= 0 && -101 + E + F >= 0 && -99 + -1*E + F >= 0 && -101 + D + F >= 0 && -99 + -1*D + F >= 0 && -101 + C + F >= 0 && -99 + -1*C + F >= 0 && -200 + A + F >= 0 && -1*A + F >= 0 && 1 + -1*E >= 0 && D + -1*E >= 0 && 2 + -1*D + -1*E >= 0 && C + -1*E >= 0 && 2 + -1*C + -1*E >= 0 && -99 + A + -1*E >= 0 && 101 + -1*A + -1*E >= 0 && -1 + E >= 0 && -2 + D + E >= 0 && -1*D + E >= 0 && -2 + C + E >= 0 && -1*C + E >= 0 && -101 + A + E >= 0 && 99 + -1*A + E >= 0 && 1 + -1*D >= 0 && C + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -99 + A + -1*D >= 0 && 101 + -1*A + -1*D >= 0 && -1 + D >= 0 && -2 + C + D >= 0 && -1*C + D >= 0 && -101 + A + D >= 0 && 99 + -1*A + D >= 0 && 1 + -1*C >= 0 && -99 + A + -1*C >= 0 && 101 + -1*A + -1*C >= 0 && -1 + C >= 0 && -101 + A + C >= 0 && 99 + -1*A + C >= 0 && 100 + -1*A >= 0 && -100 + A >= 0 && 0 >= H] 8. f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f32(A,B,C,D,1,F,G,1,I,J,-1,L,100,O) [1 + -1*H >= 0 (?,1) && -99 + F + -1*H >= 0 && 101 + -1*F + -1*H >= 0 && E + -1*H >= 0 && 2 + -1*E + -1*H >= 0 && D + -1*H >= 0 && 2 + -1*D + -1*H >= 0 && C + -1*H >= 0 && 2 + -1*C + -1*H >= 0 && -99 + A + -1*H >= 0 && 101 + -1*A + -1*H >= 0 && H >= 0 && -100 + F + H >= 0 && 100 + -1*F + H >= 0 && -1 + E + H >= 0 && 1 + -1*E + H >= 0 && -1 + D + H >= 0 && 1 + -1*D + H >= 0 && -1 + C + H >= 0 && 1 + -1*C + H >= 0 && -100 + A + H >= 0 && 100 + -1*A + H >= 0 && 100 + -1*F >= 0 && 99 + E + -1*F >= 0 && 101 + -1*E + -1*F >= 0 && 99 + D + -1*F >= 0 && 101 + -1*D + -1*F >= 0 && 99 + C + -1*F >= 0 && 101 + -1*C + -1*F >= 0 && A + -1*F >= 0 && 200 + -1*A + -1*F >= 0 && -100 + F >= 0 && -101 + E + F >= 0 && -99 + -1*E + F >= 0 && -101 + D + F >= 0 && -99 + -1*D + F >= 0 && -101 + C + F >= 0 && -99 + -1*C + F >= 0 && -200 + A + F >= 0 && -1*A + F >= 0 && 1 + -1*E >= 0 && D + -1*E >= 0 && 2 + -1*D + -1*E >= 0 && C + -1*E >= 0 && 2 + -1*C + -1*E >= 0 && -99 + A + -1*E >= 0 && 101 + -1*A + -1*E >= 0 && -1 + E >= 0 && -2 + D + E >= 0 && -1*D + E >= 0 && -2 + C + E >= 0 && -1*C + E >= 0 && -101 + A + E >= 0 && 99 + -1*A + E >= 0 && 1 + -1*D >= 0 && C + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -99 + A + -1*D >= 0 && 101 + -1*A + -1*D >= 0 && -1 + D >= 0 && -2 + C + D >= 0 && -1*C + D >= 0 && -101 + A + D >= 0 && 99 + -1*A + D >= 0 && 1 + -1*C >= 0 && -99 + A + -1*C >= 0 && 101 + -1*A + -1*C >= 0 && -1 + C >= 0 && -101 + A + C >= 0 && 99 + -1*A + C >= 0 && 100 + -1*A >= 0 && -100 + A >= 0 && H = 1] 9. f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f32(A,B,C,D,1,F,G,1,I,J,O,P,M,N) [1 + -1*H >= 0 (?,1) && -99 + F + -1*H >= 0 && 101 + -1*F + -1*H >= 0 && E + -1*H >= 0 && 2 + -1*E + -1*H >= 0 && D + -1*H >= 0 && 2 + -1*D + -1*H >= 0 && C + -1*H >= 0 && 2 + -1*C + -1*H >= 0 && -99 + A + -1*H >= 0 && 101 + -1*A + -1*H >= 0 && H >= 0 && -100 + F + H >= 0 && 100 + -1*F + H >= 0 && -1 + E + H >= 0 && 1 + -1*E + H >= 0 && -1 + D + H >= 0 && 1 + -1*D + H >= 0 && -1 + C + H >= 0 && 1 + -1*C + H >= 0 && -100 + A + H >= 0 && 100 + -1*A + H >= 0 && 100 + -1*F >= 0 && 99 + E + -1*F >= 0 && 101 + -1*E + -1*F >= 0 && 99 + D + -1*F >= 0 && 101 + -1*D + -1*F >= 0 && 99 + C + -1*F >= 0 && 101 + -1*C + -1*F >= 0 && A + -1*F >= 0 && 200 + -1*A + -1*F >= 0 && -100 + F >= 0 && -101 + E + F >= 0 && -99 + -1*E + F >= 0 && -101 + D + F >= 0 && -99 + -1*D + F >= 0 && -101 + C + F >= 0 && -99 + -1*C + F >= 0 && -200 + A + F >= 0 && -1*A + F >= 0 && 1 + -1*E >= 0 && D + -1*E >= 0 && 2 + -1*D + -1*E >= 0 && C + -1*E >= 0 && 2 + -1*C + -1*E >= 0 && -99 + A + -1*E >= 0 && 101 + -1*A + -1*E >= 0 && -1 + E >= 0 && -2 + D + E >= 0 && -1*D + E >= 0 && -2 + C + E >= 0 && -1*C + E >= 0 && -101 + A + E >= 0 && 99 + -1*A + E >= 0 && 1 + -1*D >= 0 && C + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -99 + A + -1*D >= 0 && 101 + -1*A + -1*D >= 0 && -1 + D >= 0 && -2 + C + D >= 0 && -1*C + D >= 0 && -101 + A + D >= 0 && 99 + -1*A + D >= 0 && 1 + -1*C >= 0 && -99 + A + -1*C >= 0 && 101 + -1*A + -1*C >= 0 && -1 + C >= 0 && -101 + A + C >= 0 && 99 + -1*A + C >= 0 && 100 + -1*A >= 0 && -100 + A >= 0 && O >= 0 && H = 1] 10. f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f32(A,B,C,D,1,F,G,1,I,J,O,P,M,N) [1 + -1*H >= 0 (?,1) && -99 + F + -1*H >= 0 && 101 + -1*F + -1*H >= 0 && E + -1*H >= 0 && 2 + -1*E + -1*H >= 0 && D + -1*H >= 0 && 2 + -1*D + -1*H >= 0 && C + -1*H >= 0 && 2 + -1*C + -1*H >= 0 && -99 + A + -1*H >= 0 && 101 + -1*A + -1*H >= 0 && H >= 0 && -100 + F + H >= 0 && 100 + -1*F + H >= 0 && -1 + E + H >= 0 && 1 + -1*E + H >= 0 && -1 + D + H >= 0 && 1 + -1*D + H >= 0 && -1 + C + H >= 0 && 1 + -1*C + H >= 0 && -100 + A + H >= 0 && 100 + -1*A + H >= 0 && 100 + -1*F >= 0 && 99 + E + -1*F >= 0 && 101 + -1*E + -1*F >= 0 && 99 + D + -1*F >= 0 && 101 + -1*D + -1*F >= 0 && 99 + C + -1*F >= 0 && 101 + -1*C + -1*F >= 0 && A + -1*F >= 0 && 200 + -1*A + -1*F >= 0 && -100 + F >= 0 && -101 + E + F >= 0 && -99 + -1*E + F >= 0 && -101 + D + F >= 0 && -99 + -1*D + F >= 0 && -101 + C + F >= 0 && -99 + -1*C + F >= 0 && -200 + A + F >= 0 && -1*A + F >= 0 && 1 + -1*E >= 0 && D + -1*E >= 0 && 2 + -1*D + -1*E >= 0 && C + -1*E >= 0 && 2 + -1*C + -1*E >= 0 && -99 + A + -1*E >= 0 && 101 + -1*A + -1*E >= 0 && -1 + E >= 0 && -2 + D + E >= 0 && -1*D + E >= 0 && -2 + C + E >= 0 && -1*C + E >= 0 && -101 + A + E >= 0 && 99 + -1*A + E >= 0 && 1 + -1*D >= 0 && C + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -99 + A + -1*D >= 0 && 101 + -1*A + -1*D >= 0 && -1 + D >= 0 && -2 + C + D >= 0 && -1*C + D >= 0 && -101 + A + D >= 0 && 99 + -1*A + D >= 0 && 1 + -1*C >= 0 && -99 + A + -1*C >= 0 && 101 + -1*A + -1*C >= 0 && -1 + C >= 0 && -101 + A + C >= 0 && 99 + -1*A + C >= 0 && 100 + -1*A >= 0 && -100 + A >= 0 && 0 >= 2 + O && H = 1] 11. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f32(A,B,C,D,E,F,G,H,I,J,K,L,M,N) [100 + -1*I >= 0 (?,1) && 100 + H + -1*I >= 0 && 100 + -1*H + -1*I >= 0 && F + -1*I >= 0 && 200 + -1*F + -1*I >= 0 && 100 + E + -1*I >= 0 && 100 + -1*E + -1*I >= 0 && 99 + D + -1*I >= 0 && 101 + -1*D + -1*I >= 0 && 99 + C + -1*I >= 0 && 101 + -1*C + -1*I >= 0 && A + -1*I >= 0 && 200 + -1*A + -1*I >= 0 && -100 + I >= 0 && -100 + H + I >= 0 && -100 + -1*H + I >= 0 && -200 + F + I >= 0 && -1*F + I >= 0 && -100 + E + I >= 0 && -100 + -1*E + I >= 0 && -101 + D + I >= 0 && -99 + -1*D + I >= 0 && -101 + C + I >= 0 && -99 + -1*C + I >= 0 && -200 + A + I >= 0 && -1*A + I >= 0 && -1*H >= 0 && -100 + F + -1*H >= 0 && 100 + -1*F + -1*H >= 0 && E + -1*H >= 0 && -1*E + -1*H >= 0 && -1 + D + -1*H >= 0 && 1 + -1*D + -1*H >= 0 && -1 + C + -1*H >= 0 && 1 + -1*C + -1*H >= 0 && -100 + A + -1*H >= 0 && 100 + -1*A + -1*H >= 0 && H >= 0 && -100 + F + H >= 0 && 100 + -1*F + H >= 0 && E + H >= 0 && -1*E + H >= 0 && -1 + D + H >= 0 && 1 + -1*D + H >= 0 && -1 + C + H >= 0 && 1 + -1*C + H >= 0 && -100 + A + H >= 0 && 100 + -1*A + H >= 0 && 100 + -1*F >= 0 && 100 + E + -1*F >= 0 && 100 + -1*E + -1*F >= 0 && 99 + D + -1*F >= 0 && 101 + -1*D + -1*F >= 0 && 99 + C + -1*F >= 0 && 101 + -1*C + -1*F >= 0 && A + -1*F >= 0 && 200 + -1*A + -1*F >= 0 && -100 + F >= 0 && -100 + E + F >= 0 && -100 + -1*E + F >= 0 && -101 + D + F >= 0 && -99 + -1*D + F >= 0 && -101 + C + F >= 0 && -99 + -1*C + F >= 0 && -200 + A + F >= 0 && -1*A + F >= 0 && -1*E >= 0 && -1 + D + -1*E >= 0 && 1 + -1*D + -1*E >= 0 && -1 + C + -1*E >= 0 && 1 + -1*C + -1*E >= 0 && -100 + A + -1*E >= 0 && 100 + -1*A + -1*E >= 0 && E >= 0 && -1 + D + E >= 0 && 1 + -1*D + E >= 0 && -1 + C + E >= 0 && 1 + -1*C + E >= 0 && -100 + A + E >= 0 && 100 + -1*A + E >= 0 && 1 + -1*D >= 0 && C + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -99 + A + -1*D >= 0 && 101 + -1*A + -1*D >= 0 && -1 + D >= 0 && -2 + C + D >= 0 && -1*C + D >= 0 && -101 + A + D >= 0 && 99 + -1*A + D >= 0 && 1 + -1*C >= 0 && -99 + A + -1*C >= 0 && 101 + -1*A + -1*C >= 0 && -1 + C >= 0 && -101 + A + C >= 0 && 99 + -1*A + C >= 0 && 100 + -1*A >= 0 && -100 + A >= 0] 12. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f32(A,B,C,D,E,F,G,H,I,J,K,L,M,N) [100 + -1*I >= 0 (?,1) && 100 + H + -1*I >= 0 && 100 + -1*H + -1*I >= 0 && F + -1*I >= 0 && 200 + -1*F + -1*I >= 0 && 100 + E + -1*I >= 0 && 100 + -1*E + -1*I >= 0 && 99 + D + -1*I >= 0 && 101 + -1*D + -1*I >= 0 && 99 + C + -1*I >= 0 && 101 + -1*C + -1*I >= 0 && A + -1*I >= 0 && 200 + -1*A + -1*I >= 0 && -100 + I >= 0 && -100 + H + I >= 0 && -100 + -1*H + I >= 0 && -200 + F + I >= 0 && -1*F + I >= 0 && -100 + E + I >= 0 && -100 + -1*E + I >= 0 && -101 + D + I >= 0 && -99 + -1*D + I >= 0 && -101 + C + I >= 0 && -99 + -1*C + I >= 0 && -200 + A + I >= 0 && -1*A + I >= 0 && -1*H >= 0 && -100 + F + -1*H >= 0 && 100 + -1*F + -1*H >= 0 && E + -1*H >= 0 && -1*E + -1*H >= 0 && -1 + D + -1*H >= 0 && 1 + -1*D + -1*H >= 0 && -1 + C + -1*H >= 0 && 1 + -1*C + -1*H >= 0 && -100 + A + -1*H >= 0 && 100 + -1*A + -1*H >= 0 && H >= 0 && -100 + F + H >= 0 && 100 + -1*F + H >= 0 && E + H >= 0 && -1*E + H >= 0 && -1 + D + H >= 0 && 1 + -1*D + H >= 0 && -1 + C + H >= 0 && 1 + -1*C + H >= 0 && -100 + A + H >= 0 && 100 + -1*A + H >= 0 && 100 + -1*F >= 0 && 100 + E + -1*F >= 0 && 100 + -1*E + -1*F >= 0 && 99 + D + -1*F >= 0 && 101 + -1*D + -1*F >= 0 && 99 + C + -1*F >= 0 && 101 + -1*C + -1*F >= 0 && A + -1*F >= 0 && 200 + -1*A + -1*F >= 0 && -100 + F >= 0 && -100 + E + F >= 0 && -100 + -1*E + F >= 0 && -101 + D + F >= 0 && -99 + -1*D + F >= 0 && -101 + C + F >= 0 && -99 + -1*C + F >= 0 && -200 + A + F >= 0 && -1*A + F >= 0 && -1*E >= 0 && -1 + D + -1*E >= 0 && 1 + -1*D + -1*E >= 0 && -1 + C + -1*E >= 0 && 1 + -1*C + -1*E >= 0 && -100 + A + -1*E >= 0 && 100 + -1*A + -1*E >= 0 && E >= 0 && -1 + D + E >= 0 && 1 + -1*D + E >= 0 && -1 + C + E >= 0 && 1 + -1*C + E >= 0 && -100 + A + E >= 0 && 100 + -1*A + E >= 0 && 1 + -1*D >= 0 && C + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -99 + A + -1*D >= 0 && 101 + -1*A + -1*D >= 0 && -1 + D >= 0 && -2 + C + D >= 0 && -1*C + D >= 0 && -101 + A + D >= 0 && 99 + -1*A + D >= 0 && 1 + -1*C >= 0 && -99 + A + -1*C >= 0 && 101 + -1*A + -1*C >= 0 && -1 + C >= 0 && -101 + A + C >= 0 && 99 + -1*A + C >= 0 && 100 + -1*A >= 0 && -100 + A >= 0 && 0 >= 1 + O] Signature: {(f0,14);(f11,14);(f23,14);(f26,14);(f32,14);(f36,14)} Flow Graph: [0->{2,3,4},1->{2,3,4},2->{5,6},3->{7,8,9,10},4->{7,8,9,10},5->{},6->{},7->{11,12},8->{},9->{},10->{} ,11->{},12->{}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: UnsatRules WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f11(100,O,0,D,E,F,G,H,I,J,K,L,M,N) True (1,1) 1. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f11(100,O,1,D,E,F,G,H,I,J,K,L,M,N) True (1,1) 2. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f36(A,B,C,C,C,F,G,H,I,100,K,L,M,N) [1 + -1*C >= 0 (1,1) && -99 + A + -1*C >= 0 && 101 + -1*A + -1*C >= 0 && C >= 0 && -100 + A + C >= 0 && 100 + -1*A + C >= 0 && 100 + -1*A >= 0 && -100 + A >= 0 && 0 >= C] 3. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f23(A,B,1,1,1,100,O,0,I,J,K,L,M,N) [1 + -1*C >= 0 (1,1) && -99 + A + -1*C >= 0 && 101 + -1*A + -1*C >= 0 && C >= 0 && -100 + A + C >= 0 && 100 + -1*A + C >= 0 && 100 + -1*A >= 0 && -100 + A >= 0 && C = 1] 4. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f23(A,B,1,1,1,100,O,1,I,J,K,L,M,N) [1 + -1*C >= 0 (1,1) && -99 + A + -1*C >= 0 && 101 + -1*A + -1*C >= 0 && C >= 0 && -100 + A + C >= 0 && 100 + -1*A + C >= 0 && 100 + -1*A >= 0 && -100 + A >= 0 && C = 1] 5. f36(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f32(A,B,C,D,E,F,G,H,I,J,K,L,M,N) [-1*E >= 0 (1,1) && D + -1*E >= 0 && -1*D + -1*E >= 0 && C + -1*E >= 0 && -1*C + -1*E >= 0 && -100 + -1*E + J >= 0 && 100 + -1*E + -1*J >= 0 && -100 + A + -1*E >= 0 && 100 + -1*A + -1*E >= 0 && E >= 0 && D + E >= 0 && -1*D + E >= 0 && C + E >= 0 && -1*C + E >= 0 && -100 + E + J >= 0 && 100 + E + -1*J >= 0 && -100 + A + E >= 0 && 100 + -1*A + E >= 0 && -1*D >= 0 && C + -1*D >= 0 && -1*C + -1*D >= 0 && -100 + -1*D + J >= 0 && 100 + -1*D + -1*J >= 0 && -100 + A + -1*D >= 0 && 100 + -1*A + -1*D >= 0 && D >= 0 && C + D >= 0 && -1*C + D >= 0 && -100 + D + J >= 0 && 100 + D + -1*J >= 0 && -100 + A + D >= 0 && 100 + -1*A + D >= 0 && -1*C >= 0 && -100 + -1*C + J >= 0 && 100 + -1*C + -1*J >= 0 && -100 + A + -1*C >= 0 && 100 + -1*A + -1*C >= 0 && C >= 0 && -100 + C + J >= 0 && 100 + C + -1*J >= 0 && -100 + A + C >= 0 && 100 + -1*A + C >= 0 && 100 + -1*J >= 0 && A + -1*J >= 0 && 200 + -1*A + -1*J >= 0 && -100 + J >= 0 && -200 + A + J >= 0 && -1*A + J >= 0 && 100 + -1*A >= 0 && -100 + A >= 0] 6. f36(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f32(A,B,C,D,E,F,G,H,I,J,K,L,M,N) [-1*E >= 0 (1,1) && D + -1*E >= 0 && -1*D + -1*E >= 0 && C + -1*E >= 0 && -1*C + -1*E >= 0 && -100 + -1*E + J >= 0 && 100 + -1*E + -1*J >= 0 && -100 + A + -1*E >= 0 && 100 + -1*A + -1*E >= 0 && E >= 0 && D + E >= 0 && -1*D + E >= 0 && C + E >= 0 && -1*C + E >= 0 && -100 + E + J >= 0 && 100 + E + -1*J >= 0 && -100 + A + E >= 0 && 100 + -1*A + E >= 0 && -1*D >= 0 && C + -1*D >= 0 && -1*C + -1*D >= 0 && -100 + -1*D + J >= 0 && 100 + -1*D + -1*J >= 0 && -100 + A + -1*D >= 0 && 100 + -1*A + -1*D >= 0 && D >= 0 && C + D >= 0 && -1*C + D >= 0 && -100 + D + J >= 0 && 100 + D + -1*J >= 0 && -100 + A + D >= 0 && 100 + -1*A + D >= 0 && -1*C >= 0 && -100 + -1*C + J >= 0 && 100 + -1*C + -1*J >= 0 && -100 + A + -1*C >= 0 && 100 + -1*A + -1*C >= 0 && C >= 0 && -100 + C + J >= 0 && 100 + C + -1*J >= 0 && -100 + A + C >= 0 && 100 + -1*A + C >= 0 && 100 + -1*J >= 0 && A + -1*J >= 0 && 200 + -1*A + -1*J >= 0 && -100 + J >= 0 && -200 + A + J >= 0 && -1*A + J >= 0 && 100 + -1*A >= 0 && -100 + A >= 0 && 0 >= 1 + O] 7. f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f26(A,B,C,D,H,F,G,H,100,J,K,L,M,N) [1 + -1*H >= 0 (1,1) && -99 + F + -1*H >= 0 && 101 + -1*F + -1*H >= 0 && E + -1*H >= 0 && 2 + -1*E + -1*H >= 0 && D + -1*H >= 0 && 2 + -1*D + -1*H >= 0 && C + -1*H >= 0 && 2 + -1*C + -1*H >= 0 && -99 + A + -1*H >= 0 && 101 + -1*A + -1*H >= 0 && H >= 0 && -100 + F + H >= 0 && 100 + -1*F + H >= 0 && -1 + E + H >= 0 && 1 + -1*E + H >= 0 && -1 + D + H >= 0 && 1 + -1*D + H >= 0 && -1 + C + H >= 0 && 1 + -1*C + H >= 0 && -100 + A + H >= 0 && 100 + -1*A + H >= 0 && 100 + -1*F >= 0 && 99 + E + -1*F >= 0 && 101 + -1*E + -1*F >= 0 && 99 + D + -1*F >= 0 && 101 + -1*D + -1*F >= 0 && 99 + C + -1*F >= 0 && 101 + -1*C + -1*F >= 0 && A + -1*F >= 0 && 200 + -1*A + -1*F >= 0 && -100 + F >= 0 && -101 + E + F >= 0 && -99 + -1*E + F >= 0 && -101 + D + F >= 0 && -99 + -1*D + F >= 0 && -101 + C + F >= 0 && -99 + -1*C + F >= 0 && -200 + A + F >= 0 && -1*A + F >= 0 && 1 + -1*E >= 0 && D + -1*E >= 0 && 2 + -1*D + -1*E >= 0 && C + -1*E >= 0 && 2 + -1*C + -1*E >= 0 && -99 + A + -1*E >= 0 && 101 + -1*A + -1*E >= 0 && -1 + E >= 0 && -2 + D + E >= 0 && -1*D + E >= 0 && -2 + C + E >= 0 && -1*C + E >= 0 && -101 + A + E >= 0 && 99 + -1*A + E >= 0 && 1 + -1*D >= 0 && C + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -99 + A + -1*D >= 0 && 101 + -1*A + -1*D >= 0 && -1 + D >= 0 && -2 + C + D >= 0 && -1*C + D >= 0 && -101 + A + D >= 0 && 99 + -1*A + D >= 0 && 1 + -1*C >= 0 && -99 + A + -1*C >= 0 && 101 + -1*A + -1*C >= 0 && -1 + C >= 0 && -101 + A + C >= 0 && 99 + -1*A + C >= 0 && 100 + -1*A >= 0 && -100 + A >= 0 && 0 >= H] 8. f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f32(A,B,C,D,1,F,G,1,I,J,-1,L,100,O) [1 + -1*H >= 0 (1,1) && -99 + F + -1*H >= 0 && 101 + -1*F + -1*H >= 0 && E + -1*H >= 0 && 2 + -1*E + -1*H >= 0 && D + -1*H >= 0 && 2 + -1*D + -1*H >= 0 && C + -1*H >= 0 && 2 + -1*C + -1*H >= 0 && -99 + A + -1*H >= 0 && 101 + -1*A + -1*H >= 0 && H >= 0 && -100 + F + H >= 0 && 100 + -1*F + H >= 0 && -1 + E + H >= 0 && 1 + -1*E + H >= 0 && -1 + D + H >= 0 && 1 + -1*D + H >= 0 && -1 + C + H >= 0 && 1 + -1*C + H >= 0 && -100 + A + H >= 0 && 100 + -1*A + H >= 0 && 100 + -1*F >= 0 && 99 + E + -1*F >= 0 && 101 + -1*E + -1*F >= 0 && 99 + D + -1*F >= 0 && 101 + -1*D + -1*F >= 0 && 99 + C + -1*F >= 0 && 101 + -1*C + -1*F >= 0 && A + -1*F >= 0 && 200 + -1*A + -1*F >= 0 && -100 + F >= 0 && -101 + E + F >= 0 && -99 + -1*E + F >= 0 && -101 + D + F >= 0 && -99 + -1*D + F >= 0 && -101 + C + F >= 0 && -99 + -1*C + F >= 0 && -200 + A + F >= 0 && -1*A + F >= 0 && 1 + -1*E >= 0 && D + -1*E >= 0 && 2 + -1*D + -1*E >= 0 && C + -1*E >= 0 && 2 + -1*C + -1*E >= 0 && -99 + A + -1*E >= 0 && 101 + -1*A + -1*E >= 0 && -1 + E >= 0 && -2 + D + E >= 0 && -1*D + E >= 0 && -2 + C + E >= 0 && -1*C + E >= 0 && -101 + A + E >= 0 && 99 + -1*A + E >= 0 && 1 + -1*D >= 0 && C + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -99 + A + -1*D >= 0 && 101 + -1*A + -1*D >= 0 && -1 + D >= 0 && -2 + C + D >= 0 && -1*C + D >= 0 && -101 + A + D >= 0 && 99 + -1*A + D >= 0 && 1 + -1*C >= 0 && -99 + A + -1*C >= 0 && 101 + -1*A + -1*C >= 0 && -1 + C >= 0 && -101 + A + C >= 0 && 99 + -1*A + C >= 0 && 100 + -1*A >= 0 && -100 + A >= 0 && H = 1] 9. f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f32(A,B,C,D,1,F,G,1,I,J,O,P,M,N) [1 + -1*H >= 0 (1,1) && -99 + F + -1*H >= 0 && 101 + -1*F + -1*H >= 0 && E + -1*H >= 0 && 2 + -1*E + -1*H >= 0 && D + -1*H >= 0 && 2 + -1*D + -1*H >= 0 && C + -1*H >= 0 && 2 + -1*C + -1*H >= 0 && -99 + A + -1*H >= 0 && 101 + -1*A + -1*H >= 0 && H >= 0 && -100 + F + H >= 0 && 100 + -1*F + H >= 0 && -1 + E + H >= 0 && 1 + -1*E + H >= 0 && -1 + D + H >= 0 && 1 + -1*D + H >= 0 && -1 + C + H >= 0 && 1 + -1*C + H >= 0 && -100 + A + H >= 0 && 100 + -1*A + H >= 0 && 100 + -1*F >= 0 && 99 + E + -1*F >= 0 && 101 + -1*E + -1*F >= 0 && 99 + D + -1*F >= 0 && 101 + -1*D + -1*F >= 0 && 99 + C + -1*F >= 0 && 101 + -1*C + -1*F >= 0 && A + -1*F >= 0 && 200 + -1*A + -1*F >= 0 && -100 + F >= 0 && -101 + E + F >= 0 && -99 + -1*E + F >= 0 && -101 + D + F >= 0 && -99 + -1*D + F >= 0 && -101 + C + F >= 0 && -99 + -1*C + F >= 0 && -200 + A + F >= 0 && -1*A + F >= 0 && 1 + -1*E >= 0 && D + -1*E >= 0 && 2 + -1*D + -1*E >= 0 && C + -1*E >= 0 && 2 + -1*C + -1*E >= 0 && -99 + A + -1*E >= 0 && 101 + -1*A + -1*E >= 0 && -1 + E >= 0 && -2 + D + E >= 0 && -1*D + E >= 0 && -2 + C + E >= 0 && -1*C + E >= 0 && -101 + A + E >= 0 && 99 + -1*A + E >= 0 && 1 + -1*D >= 0 && C + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -99 + A + -1*D >= 0 && 101 + -1*A + -1*D >= 0 && -1 + D >= 0 && -2 + C + D >= 0 && -1*C + D >= 0 && -101 + A + D >= 0 && 99 + -1*A + D >= 0 && 1 + -1*C >= 0 && -99 + A + -1*C >= 0 && 101 + -1*A + -1*C >= 0 && -1 + C >= 0 && -101 + A + C >= 0 && 99 + -1*A + C >= 0 && 100 + -1*A >= 0 && -100 + A >= 0 && O >= 0 && H = 1] 10. f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f32(A,B,C,D,1,F,G,1,I,J,O,P,M,N) [1 + -1*H >= 0 (1,1) && -99 + F + -1*H >= 0 && 101 + -1*F + -1*H >= 0 && E + -1*H >= 0 && 2 + -1*E + -1*H >= 0 && D + -1*H >= 0 && 2 + -1*D + -1*H >= 0 && C + -1*H >= 0 && 2 + -1*C + -1*H >= 0 && -99 + A + -1*H >= 0 && 101 + -1*A + -1*H >= 0 && H >= 0 && -100 + F + H >= 0 && 100 + -1*F + H >= 0 && -1 + E + H >= 0 && 1 + -1*E + H >= 0 && -1 + D + H >= 0 && 1 + -1*D + H >= 0 && -1 + C + H >= 0 && 1 + -1*C + H >= 0 && -100 + A + H >= 0 && 100 + -1*A + H >= 0 && 100 + -1*F >= 0 && 99 + E + -1*F >= 0 && 101 + -1*E + -1*F >= 0 && 99 + D + -1*F >= 0 && 101 + -1*D + -1*F >= 0 && 99 + C + -1*F >= 0 && 101 + -1*C + -1*F >= 0 && A + -1*F >= 0 && 200 + -1*A + -1*F >= 0 && -100 + F >= 0 && -101 + E + F >= 0 && -99 + -1*E + F >= 0 && -101 + D + F >= 0 && -99 + -1*D + F >= 0 && -101 + C + F >= 0 && -99 + -1*C + F >= 0 && -200 + A + F >= 0 && -1*A + F >= 0 && 1 + -1*E >= 0 && D + -1*E >= 0 && 2 + -1*D + -1*E >= 0 && C + -1*E >= 0 && 2 + -1*C + -1*E >= 0 && -99 + A + -1*E >= 0 && 101 + -1*A + -1*E >= 0 && -1 + E >= 0 && -2 + D + E >= 0 && -1*D + E >= 0 && -2 + C + E >= 0 && -1*C + E >= 0 && -101 + A + E >= 0 && 99 + -1*A + E >= 0 && 1 + -1*D >= 0 && C + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -99 + A + -1*D >= 0 && 101 + -1*A + -1*D >= 0 && -1 + D >= 0 && -2 + C + D >= 0 && -1*C + D >= 0 && -101 + A + D >= 0 && 99 + -1*A + D >= 0 && 1 + -1*C >= 0 && -99 + A + -1*C >= 0 && 101 + -1*A + -1*C >= 0 && -1 + C >= 0 && -101 + A + C >= 0 && 99 + -1*A + C >= 0 && 100 + -1*A >= 0 && -100 + A >= 0 && 0 >= 2 + O && H = 1] 11. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f32(A,B,C,D,E,F,G,H,I,J,K,L,M,N) [100 + -1*I >= 0 (1,1) && 100 + H + -1*I >= 0 && 100 + -1*H + -1*I >= 0 && F + -1*I >= 0 && 200 + -1*F + -1*I >= 0 && 100 + E + -1*I >= 0 && 100 + -1*E + -1*I >= 0 && 99 + D + -1*I >= 0 && 101 + -1*D + -1*I >= 0 && 99 + C + -1*I >= 0 && 101 + -1*C + -1*I >= 0 && A + -1*I >= 0 && 200 + -1*A + -1*I >= 0 && -100 + I >= 0 && -100 + H + I >= 0 && -100 + -1*H + I >= 0 && -200 + F + I >= 0 && -1*F + I >= 0 && -100 + E + I >= 0 && -100 + -1*E + I >= 0 && -101 + D + I >= 0 && -99 + -1*D + I >= 0 && -101 + C + I >= 0 && -99 + -1*C + I >= 0 && -200 + A + I >= 0 && -1*A + I >= 0 && -1*H >= 0 && -100 + F + -1*H >= 0 && 100 + -1*F + -1*H >= 0 && E + -1*H >= 0 && -1*E + -1*H >= 0 && -1 + D + -1*H >= 0 && 1 + -1*D + -1*H >= 0 && -1 + C + -1*H >= 0 && 1 + -1*C + -1*H >= 0 && -100 + A + -1*H >= 0 && 100 + -1*A + -1*H >= 0 && H >= 0 && -100 + F + H >= 0 && 100 + -1*F + H >= 0 && E + H >= 0 && -1*E + H >= 0 && -1 + D + H >= 0 && 1 + -1*D + H >= 0 && -1 + C + H >= 0 && 1 + -1*C + H >= 0 && -100 + A + H >= 0 && 100 + -1*A + H >= 0 && 100 + -1*F >= 0 && 100 + E + -1*F >= 0 && 100 + -1*E + -1*F >= 0 && 99 + D + -1*F >= 0 && 101 + -1*D + -1*F >= 0 && 99 + C + -1*F >= 0 && 101 + -1*C + -1*F >= 0 && A + -1*F >= 0 && 200 + -1*A + -1*F >= 0 && -100 + F >= 0 && -100 + E + F >= 0 && -100 + -1*E + F >= 0 && -101 + D + F >= 0 && -99 + -1*D + F >= 0 && -101 + C + F >= 0 && -99 + -1*C + F >= 0 && -200 + A + F >= 0 && -1*A + F >= 0 && -1*E >= 0 && -1 + D + -1*E >= 0 && 1 + -1*D + -1*E >= 0 && -1 + C + -1*E >= 0 && 1 + -1*C + -1*E >= 0 && -100 + A + -1*E >= 0 && 100 + -1*A + -1*E >= 0 && E >= 0 && -1 + D + E >= 0 && 1 + -1*D + E >= 0 && -1 + C + E >= 0 && 1 + -1*C + E >= 0 && -100 + A + E >= 0 && 100 + -1*A + E >= 0 && 1 + -1*D >= 0 && C + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -99 + A + -1*D >= 0 && 101 + -1*A + -1*D >= 0 && -1 + D >= 0 && -2 + C + D >= 0 && -1*C + D >= 0 && -101 + A + D >= 0 && 99 + -1*A + D >= 0 && 1 + -1*C >= 0 && -99 + A + -1*C >= 0 && 101 + -1*A + -1*C >= 0 && -1 + C >= 0 && -101 + A + C >= 0 && 99 + -1*A + C >= 0 && 100 + -1*A >= 0 && -100 + A >= 0] 12. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f32(A,B,C,D,E,F,G,H,I,J,K,L,M,N) [100 + -1*I >= 0 (1,1) && 100 + H + -1*I >= 0 && 100 + -1*H + -1*I >= 0 && F + -1*I >= 0 && 200 + -1*F + -1*I >= 0 && 100 + E + -1*I >= 0 && 100 + -1*E + -1*I >= 0 && 99 + D + -1*I >= 0 && 101 + -1*D + -1*I >= 0 && 99 + C + -1*I >= 0 && 101 + -1*C + -1*I >= 0 && A + -1*I >= 0 && 200 + -1*A + -1*I >= 0 && -100 + I >= 0 && -100 + H + I >= 0 && -100 + -1*H + I >= 0 && -200 + F + I >= 0 && -1*F + I >= 0 && -100 + E + I >= 0 && -100 + -1*E + I >= 0 && -101 + D + I >= 0 && -99 + -1*D + I >= 0 && -101 + C + I >= 0 && -99 + -1*C + I >= 0 && -200 + A + I >= 0 && -1*A + I >= 0 && -1*H >= 0 && -100 + F + -1*H >= 0 && 100 + -1*F + -1*H >= 0 && E + -1*H >= 0 && -1*E + -1*H >= 0 && -1 + D + -1*H >= 0 && 1 + -1*D + -1*H >= 0 && -1 + C + -1*H >= 0 && 1 + -1*C + -1*H >= 0 && -100 + A + -1*H >= 0 && 100 + -1*A + -1*H >= 0 && H >= 0 && -100 + F + H >= 0 && 100 + -1*F + H >= 0 && E + H >= 0 && -1*E + H >= 0 && -1 + D + H >= 0 && 1 + -1*D + H >= 0 && -1 + C + H >= 0 && 1 + -1*C + H >= 0 && -100 + A + H >= 0 && 100 + -1*A + H >= 0 && 100 + -1*F >= 0 && 100 + E + -1*F >= 0 && 100 + -1*E + -1*F >= 0 && 99 + D + -1*F >= 0 && 101 + -1*D + -1*F >= 0 && 99 + C + -1*F >= 0 && 101 + -1*C + -1*F >= 0 && A + -1*F >= 0 && 200 + -1*A + -1*F >= 0 && -100 + F >= 0 && -100 + E + F >= 0 && -100 + -1*E + F >= 0 && -101 + D + F >= 0 && -99 + -1*D + F >= 0 && -101 + C + F >= 0 && -99 + -1*C + F >= 0 && -200 + A + F >= 0 && -1*A + F >= 0 && -1*E >= 0 && -1 + D + -1*E >= 0 && 1 + -1*D + -1*E >= 0 && -1 + C + -1*E >= 0 && 1 + -1*C + -1*E >= 0 && -100 + A + -1*E >= 0 && 100 + -1*A + -1*E >= 0 && E >= 0 && -1 + D + E >= 0 && 1 + -1*D + E >= 0 && -1 + C + E >= 0 && 1 + -1*C + E >= 0 && -100 + A + E >= 0 && 100 + -1*A + E >= 0 && 1 + -1*D >= 0 && C + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -99 + A + -1*D >= 0 && 101 + -1*A + -1*D >= 0 && -1 + D >= 0 && -2 + C + D >= 0 && -1*C + D >= 0 && -101 + A + D >= 0 && 99 + -1*A + D >= 0 && 1 + -1*C >= 0 && -99 + A + -1*C >= 0 && 101 + -1*A + -1*C >= 0 && -1 + C >= 0 && -101 + A + C >= 0 && 99 + -1*A + C >= 0 && 100 + -1*A >= 0 && -100 + A >= 0 && 0 >= 1 + O] Signature: {(f0,14);(f11,14);(f23,14);(f26,14);(f32,14);(f36,14)} Flow Graph: [0->{2,3,4},1->{2,3,4},2->{5,6},3->{7,8,9,10},4->{7,8,9,10},5->{},6->{},7->{11,12},8->{},9->{},10->{} ,11->{},12->{}] + Applied Processor: UnsatRules + Details: The problem is already solved. YES(?,O(1))