NO * Step 1: UnsatPaths NO + Considered Problem: Rules: 0. f30(A,B,C,D,E,F,G,H,I,J) -> f30(L,K,-1 + C,-1 + C,1,F,G,H,I,J) [-1 + I >= 0 (?,1) && -2 + H + I >= 0 && -1 + F + I >= 0 && -1 + -1*F + I >= 0 && -2 + E + I >= 0 && -1*E + I >= 0 && -1 + D + I >= 0 && -1 + C + I >= 0 && -1 + H >= 0 && -1 + F + H >= 0 && -1 + -1*F + H >= 0 && -2 + E + H >= 0 && -1*E + H >= 0 && -1 + D + H >= 0 && -1 + C + H >= 0 && -1*F >= 0 && -1 + E + -1*F >= 0 && 1 + -1*E + -1*F >= 0 && D + -1*F >= 0 && C + -1*F >= 0 && F >= 0 && -1 + E + F >= 0 && 1 + -1*E + F >= 0 && D + F >= 0 && C + F >= 0 && 1 + -1*E >= 0 && 1 + D + -1*E >= 0 && 1 + C + -1*E >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && -1 + C + E >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1*C + D >= 0 && C >= 0 && I >= 1 + D && C >= H && D >= 1 && C >= 1 && 0 >= 1 + K && C + D >= 1 && E = 1] 1. f30(A,B,C,D,E,F,G,H,I,J) -> f30(L,K,-1 + C,-1 + C,1,F,G,H,I,J) [-1 + I >= 0 (?,1) && -2 + H + I >= 0 && -1 + F + I >= 0 && -1 + -1*F + I >= 0 && -2 + E + I >= 0 && -1*E + I >= 0 && -1 + D + I >= 0 && -1 + C + I >= 0 && -1 + H >= 0 && -1 + F + H >= 0 && -1 + -1*F + H >= 0 && -2 + E + H >= 0 && -1*E + H >= 0 && -1 + D + H >= 0 && -1 + C + H >= 0 && -1*F >= 0 && -1 + E + -1*F >= 0 && 1 + -1*E + -1*F >= 0 && D + -1*F >= 0 && C + -1*F >= 0 && F >= 0 && -1 + E + F >= 0 && 1 + -1*E + F >= 0 && D + F >= 0 && C + F >= 0 && 1 + -1*E >= 0 && 1 + D + -1*E >= 0 && 1 + C + -1*E >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && -1 + C + E >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1*C + D >= 0 && C >= 0 && I >= 1 + D && C >= H && D >= 1 && C >= 1 && K >= 1 && C + D >= 1 && E = 1] 2. f30(A,B,C,D,E,F,G,H,I,J) -> f28(L,0,-2 + D,-1 + D,1,F,G,H,I,J) [-1 + I >= 0 (?,1) && -2 + H + I >= 0 && -1 + F + I >= 0 && -1 + -1*F + I >= 0 && -2 + E + I >= 0 && -1*E + I >= 0 && -1 + D + I >= 0 && -1 + C + I >= 0 && -1 + H >= 0 && -1 + F + H >= 0 && -1 + -1*F + H >= 0 && -2 + E + H >= 0 && -1*E + H >= 0 && -1 + D + H >= 0 && -1 + C + H >= 0 && -1*F >= 0 && -1 + E + -1*F >= 0 && 1 + -1*E + -1*F >= 0 && D + -1*F >= 0 && C + -1*F >= 0 && F >= 0 && -1 + E + F >= 0 && 1 + -1*E + F >= 0 && D + F >= 0 && C + F >= 0 && 1 + -1*E >= 0 && 1 + D + -1*E >= 0 && 1 + C + -1*E >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && -1 + C + E >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1*C + D >= 0 && C >= 0 && I >= 1 + D && C >= H && D >= 1 && C + D >= 1 && C >= 1 && E = 1] 3. f30(A,B,C,D,E,F,G,H,I,J) -> f30(L,K,-1 + C,-1 + C,1,F,G,H,I,J) [-1 + I >= 0 (?,1) && -2 + H + I >= 0 && -1 + F + I >= 0 && -1 + -1*F + I >= 0 && -2 + E + I >= 0 && -1*E + I >= 0 && -1 + D + I >= 0 && -1 + C + I >= 0 && -1 + H >= 0 && -1 + F + H >= 0 && -1 + -1*F + H >= 0 && -2 + E + H >= 0 && -1*E + H >= 0 && -1 + D + H >= 0 && -1 + C + H >= 0 && -1*F >= 0 && -1 + E + -1*F >= 0 && 1 + -1*E + -1*F >= 0 && D + -1*F >= 0 && C + -1*F >= 0 && F >= 0 && -1 + E + F >= 0 && 1 + -1*E + F >= 0 && D + F >= 0 && C + F >= 0 && 1 + -1*E >= 0 && 1 + D + -1*E >= 0 && 1 + C + -1*E >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && -1 + C + E >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1*C + D >= 0 && C >= 0 && H >= 1 + C && D >= 1 && C >= 1 && 0 >= 1 + K && C + D >= 1 && E = 1] 4. f30(A,B,C,D,E,F,G,H,I,J) -> f30(L,K,-1 + C,-1 + C,1,F,G,H,I,J) [-1 + I >= 0 (?,1) && -2 + H + I >= 0 && -1 + F + I >= 0 && -1 + -1*F + I >= 0 && -2 + E + I >= 0 && -1*E + I >= 0 && -1 + D + I >= 0 && -1 + C + I >= 0 && -1 + H >= 0 && -1 + F + H >= 0 && -1 + -1*F + H >= 0 && -2 + E + H >= 0 && -1*E + H >= 0 && -1 + D + H >= 0 && -1 + C + H >= 0 && -1*F >= 0 && -1 + E + -1*F >= 0 && 1 + -1*E + -1*F >= 0 && D + -1*F >= 0 && C + -1*F >= 0 && F >= 0 && -1 + E + F >= 0 && 1 + -1*E + F >= 0 && D + F >= 0 && C + F >= 0 && 1 + -1*E >= 0 && 1 + D + -1*E >= 0 && 1 + C + -1*E >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && -1 + C + E >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1*C + D >= 0 && C >= 0 && H >= 1 + C && D >= 1 && C >= 1 && K >= 1 && C + D >= 1 && E = 1] 5. f30(A,B,C,D,E,F,G,H,I,J) -> f28(L,0,-2 + D,-1 + D,1,F,G,H,I,J) [-1 + I >= 0 (?,1) && -2 + H + I >= 0 && -1 + F + I >= 0 && -1 + -1*F + I >= 0 && -2 + E + I >= 0 && -1*E + I >= 0 && -1 + D + I >= 0 && -1 + C + I >= 0 && -1 + H >= 0 && -1 + F + H >= 0 && -1 + -1*F + H >= 0 && -2 + E + H >= 0 && -1*E + H >= 0 && -1 + D + H >= 0 && -1 + C + H >= 0 && -1*F >= 0 && -1 + E + -1*F >= 0 && 1 + -1*E + -1*F >= 0 && D + -1*F >= 0 && C + -1*F >= 0 && F >= 0 && -1 + E + F >= 0 && 1 + -1*E + F >= 0 && D + F >= 0 && C + F >= 0 && 1 + -1*E >= 0 && 1 + D + -1*E >= 0 && 1 + C + -1*E >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && -1 + C + E >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1*C + D >= 0 && C >= 0 && H >= 1 + C && D >= 1 && C + D >= 1 && C >= 1 && E = 1] 6. f30(A,B,C,D,E,F,G,H,I,J) -> f9(A,B,C,D,E,F,G,H,I,L) [-1 + I >= 0 (?,1) && -2 + H + I >= 0 && -1 + F + I >= 0 && -1 + -1*F + I >= 0 && -2 + E + I >= 0 && -1*E + I >= 0 && -1 + D + I >= 0 && -1 + C + I >= 0 && -1 + H >= 0 && -1 + F + H >= 0 && -1 + -1*F + H >= 0 && -2 + E + H >= 0 && -1*E + H >= 0 && -1 + D + H >= 0 && -1 + C + H >= 0 && -1*F >= 0 && -1 + E + -1*F >= 0 && 1 + -1*E + -1*F >= 0 && D + -1*F >= 0 && C + -1*F >= 0 && F >= 0 && -1 + E + F >= 0 && 1 + -1*E + F >= 0 && D + F >= 0 && C + F >= 0 && 1 + -1*E >= 0 && 1 + D + -1*E >= 0 && 1 + C + -1*E >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && -1 + C + E >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1*C + D >= 0 && C >= 0 && 0 >= C] 7. f28(A,B,C,D,E,F,G,H,I,J) -> f30(L,K,-1 + C,-1 + C,1,F,G,H,I,J) [-1 + I >= 0 (?,1) && -2 + H + I >= 0 && -1 + F + I >= 0 && -1 + -1*F + I >= 0 && -2 + E + I >= 0 && -1*E + I >= 0 && -1 + D + I >= 0 && C + I >= 0 && -1 + B + I >= 0 && -1 + -1*B + I >= 0 && -1 + H >= 0 && -1 + F + H >= 0 && -1 + -1*F + H >= 0 && -2 + E + H >= 0 && -1*E + H >= 0 && -1 + D + H >= 0 && C + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -1*F >= 0 && -1 + E + -1*F >= 0 && 1 + -1*E + -1*F >= 0 && D + -1*F >= 0 && 1 + C + -1*F >= 0 && B + -1*F >= 0 && -1*B + -1*F >= 0 && F >= 0 && -1 + E + F >= 0 && 1 + -1*E + F >= 0 && D + F >= 0 && 1 + C + F >= 0 && B + F >= 0 && -1*B + F >= 0 && 1 + -1*E >= 0 && 1 + D + -1*E >= 0 && 2 + C + -1*E >= 0 && 1 + B + -1*E >= 0 && 1 + -1*B + -1*E >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && C + E >= 0 && -1 + B + E >= 0 && -1 + -1*B + E >= 0 && 1 + C + -1*D >= 0 && D >= 0 && 1 + C + D >= 0 && -1 + -1*C + D >= 0 && B + D >= 0 && -1*B + D >= 0 && 1 + C >= 0 && 1 + B + C >= 0 && 1 + -1*B + C >= 0 && -1*B >= 0 && B >= 0 && H >= 1 + C && D >= 1 && C >= 1 && 0 >= 1 + K && C + D >= 1 && E = 1] 8. f28(A,B,C,D,E,F,G,H,I,J) -> f30(L,K,-1 + C,-1 + C,1,F,G,H,I,J) [-1 + I >= 0 (?,1) && -2 + H + I >= 0 && -1 + F + I >= 0 && -1 + -1*F + I >= 0 && -2 + E + I >= 0 && -1*E + I >= 0 && -1 + D + I >= 0 && C + I >= 0 && -1 + B + I >= 0 && -1 + -1*B + I >= 0 && -1 + H >= 0 && -1 + F + H >= 0 && -1 + -1*F + H >= 0 && -2 + E + H >= 0 && -1*E + H >= 0 && -1 + D + H >= 0 && C + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -1*F >= 0 && -1 + E + -1*F >= 0 && 1 + -1*E + -1*F >= 0 && D + -1*F >= 0 && 1 + C + -1*F >= 0 && B + -1*F >= 0 && -1*B + -1*F >= 0 && F >= 0 && -1 + E + F >= 0 && 1 + -1*E + F >= 0 && D + F >= 0 && 1 + C + F >= 0 && B + F >= 0 && -1*B + F >= 0 && 1 + -1*E >= 0 && 1 + D + -1*E >= 0 && 2 + C + -1*E >= 0 && 1 + B + -1*E >= 0 && 1 + -1*B + -1*E >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && C + E >= 0 && -1 + B + E >= 0 && -1 + -1*B + E >= 0 && 1 + C + -1*D >= 0 && D >= 0 && 1 + C + D >= 0 && -1 + -1*C + D >= 0 && B + D >= 0 && -1*B + D >= 0 && 1 + C >= 0 && 1 + B + C >= 0 && 1 + -1*B + C >= 0 && -1*B >= 0 && B >= 0 && H >= 1 + C && D >= 1 && C >= 1 && K >= 1 && C + D >= 1 && E = 1] 9. f28(A,B,C,D,E,F,G,H,I,J) -> f28(L,0,-2 + D,-1 + D,1,F,G,H,I,J) [-1 + I >= 0 (?,1) && -2 + H + I >= 0 && -1 + F + I >= 0 && -1 + -1*F + I >= 0 && -2 + E + I >= 0 && -1*E + I >= 0 && -1 + D + I >= 0 && C + I >= 0 && -1 + B + I >= 0 && -1 + -1*B + I >= 0 && -1 + H >= 0 && -1 + F + H >= 0 && -1 + -1*F + H >= 0 && -2 + E + H >= 0 && -1*E + H >= 0 && -1 + D + H >= 0 && C + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -1*F >= 0 && -1 + E + -1*F >= 0 && 1 + -1*E + -1*F >= 0 && D + -1*F >= 0 && 1 + C + -1*F >= 0 && B + -1*F >= 0 && -1*B + -1*F >= 0 && F >= 0 && -1 + E + F >= 0 && 1 + -1*E + F >= 0 && D + F >= 0 && 1 + C + F >= 0 && B + F >= 0 && -1*B + F >= 0 && 1 + -1*E >= 0 && 1 + D + -1*E >= 0 && 2 + C + -1*E >= 0 && 1 + B + -1*E >= 0 && 1 + -1*B + -1*E >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && C + E >= 0 && -1 + B + E >= 0 && -1 + -1*B + E >= 0 && 1 + C + -1*D >= 0 && D >= 0 && 1 + C + D >= 0 && -1 + -1*C + D >= 0 && B + D >= 0 && -1*B + D >= 0 && 1 + C >= 0 && 1 + B + C >= 0 && 1 + -1*B + C >= 0 && -1*B >= 0 && B >= 0 && H >= 1 + C && D >= 1 && C + D >= 1 && C >= 1 && E = 1] 10. f28(A,B,C,D,E,F,G,H,I,J) -> f30(L,K,-1 + C,-1 + C,1,F,G,H,I,J) [-1 + I >= 0 (?,1) && -2 + H + I >= 0 && -1 + F + I >= 0 && -1 + -1*F + I >= 0 && -2 + E + I >= 0 && -1*E + I >= 0 && -1 + D + I >= 0 && C + I >= 0 && -1 + B + I >= 0 && -1 + -1*B + I >= 0 && -1 + H >= 0 && -1 + F + H >= 0 && -1 + -1*F + H >= 0 && -2 + E + H >= 0 && -1*E + H >= 0 && -1 + D + H >= 0 && C + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -1*F >= 0 && -1 + E + -1*F >= 0 && 1 + -1*E + -1*F >= 0 && D + -1*F >= 0 && 1 + C + -1*F >= 0 && B + -1*F >= 0 && -1*B + -1*F >= 0 && F >= 0 && -1 + E + F >= 0 && 1 + -1*E + F >= 0 && D + F >= 0 && 1 + C + F >= 0 && B + F >= 0 && -1*B + F >= 0 && 1 + -1*E >= 0 && 1 + D + -1*E >= 0 && 2 + C + -1*E >= 0 && 1 + B + -1*E >= 0 && 1 + -1*B + -1*E >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && C + E >= 0 && -1 + B + E >= 0 && -1 + -1*B + E >= 0 && 1 + C + -1*D >= 0 && D >= 0 && 1 + C + D >= 0 && -1 + -1*C + D >= 0 && B + D >= 0 && -1*B + D >= 0 && 1 + C >= 0 && 1 + B + C >= 0 && 1 + -1*B + C >= 0 && -1*B >= 0 && B >= 0 && I >= 1 + D && C >= H && D >= 1 && C >= 1 && 0 >= 1 + K && C + D >= 1 && E = 1] 11. f28(A,B,C,D,E,F,G,H,I,J) -> f30(L,K,-1 + C,-1 + C,1,F,G,H,I,J) [-1 + I >= 0 (?,1) && -2 + H + I >= 0 && -1 + F + I >= 0 && -1 + -1*F + I >= 0 && -2 + E + I >= 0 && -1*E + I >= 0 && -1 + D + I >= 0 && C + I >= 0 && -1 + B + I >= 0 && -1 + -1*B + I >= 0 && -1 + H >= 0 && -1 + F + H >= 0 && -1 + -1*F + H >= 0 && -2 + E + H >= 0 && -1*E + H >= 0 && -1 + D + H >= 0 && C + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -1*F >= 0 && -1 + E + -1*F >= 0 && 1 + -1*E + -1*F >= 0 && D + -1*F >= 0 && 1 + C + -1*F >= 0 && B + -1*F >= 0 && -1*B + -1*F >= 0 && F >= 0 && -1 + E + F >= 0 && 1 + -1*E + F >= 0 && D + F >= 0 && 1 + C + F >= 0 && B + F >= 0 && -1*B + F >= 0 && 1 + -1*E >= 0 && 1 + D + -1*E >= 0 && 2 + C + -1*E >= 0 && 1 + B + -1*E >= 0 && 1 + -1*B + -1*E >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && C + E >= 0 && -1 + B + E >= 0 && -1 + -1*B + E >= 0 && 1 + C + -1*D >= 0 && D >= 0 && 1 + C + D >= 0 && -1 + -1*C + D >= 0 && B + D >= 0 && -1*B + D >= 0 && 1 + C >= 0 && 1 + B + C >= 0 && 1 + -1*B + C >= 0 && -1*B >= 0 && B >= 0 && I >= 1 + D && C >= H && D >= 1 && C >= 1 && K >= 1 && C + D >= 1 && E = 1] 12. f28(A,B,C,D,E,F,G,H,I,J) -> f28(L,0,-2 + D,-1 + D,1,F,G,H,I,J) [-1 + I >= 0 (?,1) && -2 + H + I >= 0 && -1 + F + I >= 0 && -1 + -1*F + I >= 0 && -2 + E + I >= 0 && -1*E + I >= 0 && -1 + D + I >= 0 && C + I >= 0 && -1 + B + I >= 0 && -1 + -1*B + I >= 0 && -1 + H >= 0 && -1 + F + H >= 0 && -1 + -1*F + H >= 0 && -2 + E + H >= 0 && -1*E + H >= 0 && -1 + D + H >= 0 && C + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -1*F >= 0 && -1 + E + -1*F >= 0 && 1 + -1*E + -1*F >= 0 && D + -1*F >= 0 && 1 + C + -1*F >= 0 && B + -1*F >= 0 && -1*B + -1*F >= 0 && F >= 0 && -1 + E + F >= 0 && 1 + -1*E + F >= 0 && D + F >= 0 && 1 + C + F >= 0 && B + F >= 0 && -1*B + F >= 0 && 1 + -1*E >= 0 && 1 + D + -1*E >= 0 && 2 + C + -1*E >= 0 && 1 + B + -1*E >= 0 && 1 + -1*B + -1*E >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && C + E >= 0 && -1 + B + E >= 0 && -1 + -1*B + E >= 0 && 1 + C + -1*D >= 0 && D >= 0 && 1 + C + D >= 0 && -1 + -1*C + D >= 0 && B + D >= 0 && -1*B + D >= 0 && 1 + C >= 0 && 1 + B + C >= 0 && 1 + -1*B + C >= 0 && -1*B >= 0 && B >= 0 && I >= 1 + D && C >= H && D >= 1 && C + D >= 1 && C >= 1 && E = 1] 13. f28(A,B,C,D,E,F,G,H,I,J) -> f9(A,B,C,D,E,F,G,H,I,L) [-1 + I >= 0 (?,1) && -2 + H + I >= 0 && -1 + F + I >= 0 && -1 + -1*F + I >= 0 && -2 + E + I >= 0 && -1*E + I >= 0 && -1 + D + I >= 0 && C + I >= 0 && -1 + B + I >= 0 && -1 + -1*B + I >= 0 && -1 + H >= 0 && -1 + F + H >= 0 && -1 + -1*F + H >= 0 && -2 + E + H >= 0 && -1*E + H >= 0 && -1 + D + H >= 0 && C + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -1*F >= 0 && -1 + E + -1*F >= 0 && 1 + -1*E + -1*F >= 0 && D + -1*F >= 0 && 1 + C + -1*F >= 0 && B + -1*F >= 0 && -1*B + -1*F >= 0 && F >= 0 && -1 + E + F >= 0 && 1 + -1*E + F >= 0 && D + F >= 0 && 1 + C + F >= 0 && B + F >= 0 && -1*B + F >= 0 && 1 + -1*E >= 0 && 1 + D + -1*E >= 0 && 2 + C + -1*E >= 0 && 1 + B + -1*E >= 0 && 1 + -1*B + -1*E >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && C + E >= 0 && -1 + B + E >= 0 && -1 + -1*B + E >= 0 && 1 + C + -1*D >= 0 && D >= 0 && 1 + C + D >= 0 && -1 + -1*C + D >= 0 && B + D >= 0 && -1*B + D >= 0 && 1 + C >= 0 && 1 + B + C >= 0 && 1 + -1*B + C >= 0 && -1*B >= 0 && B >= 0 && 0 >= C] 14. f27(A,B,C,D,E,F,G,H,I,J) -> f27(L,0,-2 + D,-1 + D,0,F,0,H,I,J) [-1*F >= 0 (?,1) && E + -1*F >= 0 && -1*E + -1*F >= 0 && F >= 0 && E + F >= 0 && -1*E + F >= 0 && -1*E >= 0 && E >= 0 && D >= 1 && C + D >= 1 && C >= 1 && E = 0] 15. f27(A,B,C,D,E,F,G,H,I,J) -> f27(L,K,-1 + C,-1 + C,0,F,0,H,I,J) [-1*F >= 0 (?,1) && E + -1*F >= 0 && -1*E + -1*F >= 0 && F >= 0 && E + F >= 0 && -1*E + F >= 0 && -1*E >= 0 && E >= 0 && D >= 1 && C >= 1 && 0 >= 1 + K && C + D >= 1 && E = 0] 16. f27(A,B,C,D,E,F,G,H,I,J) -> f27(L,K,-1 + C,-1 + C,0,F,0,H,I,J) [-1*F >= 0 (?,1) && E + -1*F >= 0 && -1*E + -1*F >= 0 && F >= 0 && E + F >= 0 && -1*E + F >= 0 && -1*E >= 0 && E >= 0 && D >= 1 && C >= 1 && K >= 1 && C + D >= 1 && E = 0] 17. f27(A,B,C,D,E,F,G,H,I,J) -> f30(L,K,-1 + C,-1 + C,1,F,M,C,D,J) [-1*F >= 0 (?,1) && E + -1*F >= 0 && -1*E + -1*F >= 0 && F >= 0 && E + F >= 0 && -1*E + F >= 0 && -1*E >= 0 && E >= 0 && D >= 1 && C >= 1 && C + D >= 1 && 0 >= 1 + K && 0 >= 1 + M && E = 0] 18. f27(A,B,C,D,E,F,G,H,I,J) -> f30(L,K,-1 + C,-1 + C,1,F,M,C,D,J) [-1*F >= 0 (?,1) && E + -1*F >= 0 && -1*E + -1*F >= 0 && F >= 0 && E + F >= 0 && -1*E + F >= 0 && -1*E >= 0 && E >= 0 && D >= 1 && C >= 1 && C + D >= 1 && 0 >= 1 + K && M >= 1 && E = 0] 19. f27(A,B,C,D,E,F,G,H,I,J) -> f30(L,K,-1 + C,-1 + C,1,F,M,C,D,J) [-1*F >= 0 (?,1) && E + -1*F >= 0 && -1*E + -1*F >= 0 && F >= 0 && E + F >= 0 && -1*E + F >= 0 && -1*E >= 0 && E >= 0 && D >= 1 && C >= 1 && C + D >= 1 && K >= 1 && 0 >= 1 + M && E = 0] 20. f27(A,B,C,D,E,F,G,H,I,J) -> f30(L,K,-1 + C,-1 + C,1,F,M,C,D,J) [-1*F >= 0 (?,1) && E + -1*F >= 0 && -1*E + -1*F >= 0 && F >= 0 && E + F >= 0 && -1*E + F >= 0 && -1*E >= 0 && E >= 0 && D >= 1 && C >= 1 && C + D >= 1 && K >= 1 && M >= 1 && E = 0] 21. f27(A,B,C,D,E,F,G,H,I,J) -> f28(L,0,-2 + D,-1 + D,1,F,K,C,D,J) [-1*F >= 0 (?,1) && E + -1*F >= 0 && -1*E + -1*F >= 0 && F >= 0 && E + F >= 0 && -1*E + F >= 0 && -1*E >= 0 && E >= 0 && D >= 1 && C >= 1 && 0 >= 1 + K && C + D >= 1 && E = 0] 22. f27(A,B,C,D,E,F,G,H,I,J) -> f28(L,0,-2 + D,-1 + D,1,F,K,C,D,J) [-1*F >= 0 (?,1) && E + -1*F >= 0 && -1*E + -1*F >= 0 && F >= 0 && E + F >= 0 && -1*E + F >= 0 && -1*E >= 0 && E >= 0 && D >= 1 && C >= 1 && K >= 1 && C + D >= 1 && E = 0] 23. f27(A,B,C,D,E,F,G,H,I,J) -> f9(A,B,C,D,E,F,G,H,I,L) [-1*F >= 0 (?,1) && E + -1*F >= 0 && -1*E + -1*F >= 0 && F >= 0 && E + F >= 0 && -1*E + F >= 0 && -1*E >= 0 && E >= 0 && 0 >= C] 24. f27(A,B,C,D,E,F,G,H,I,J) -> f9(A,B,C,D,E,F,G,H,I,L) [-1*F >= 0 (?,1) && E + -1*F >= 0 && -1*E + -1*F >= 0 && F >= 0 && E + F >= 0 && -1*E + F >= 0 && -1*E >= 0 && E >= 0 && C >= 1 && 0 >= D] 25. f8(A,B,C,D,E,F,G,H,I,J) -> f27(A,B,C,D,0,0,G,H,I,J) True (1,1) Signature: {(f27,10);(f28,10);(f30,10);(f8,10);(f9,10)} Flow Graph: [0->{0,1,2,3,4,5,6},1->{0,1,2,3,4,5,6},2->{7,8,9,10,11,12,13},3->{0,1,2,3,4,5,6},4->{0,1,2,3,4,5,6},5->{7 ,8,9,10,11,12,13},6->{},7->{0,1,2,3,4,5,6},8->{0,1,2,3,4,5,6},9->{7,8,9,10,11,12,13},10->{0,1,2,3,4,5,6} ,11->{0,1,2,3,4,5,6},12->{7,8,9,10,11,12,13},13->{},14->{14,15,16,17,18,19,20,21,22,23,24},15->{14,15,16,17 ,18,19,20,21,22,23,24},16->{14,15,16,17,18,19,20,21,22,23,24},17->{0,1,2,3,4,5,6},18->{0,1,2,3,4,5,6},19->{0 ,1,2,3,4,5,6},20->{0,1,2,3,4,5,6},21->{7,8,9,10,11,12,13},22->{7,8,9,10,11,12,13},23->{},24->{},25->{14,15 ,16,17,18,19,20,21,22,23,24}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(3,0) ,(3,1) ,(3,2) ,(4,0) ,(4,1) ,(4,2) ,(5,10) ,(5,11) ,(5,12) ,(7,0) ,(7,1) ,(7,2) ,(8,0) ,(8,1) ,(8,2) ,(9,10) ,(9,11) ,(9,12) ,(14,24) ,(15,24) ,(16,24) ,(17,0) ,(17,1) ,(17,2) ,(18,0) ,(18,1) ,(18,2) ,(19,0) ,(19,1) ,(19,2) ,(20,0) ,(20,1) ,(20,2)] * Step 2: FromIts NO + Considered Problem: Rules: 0. f30(A,B,C,D,E,F,G,H,I,J) -> f30(L,K,-1 + C,-1 + C,1,F,G,H,I,J) [-1 + I >= 0 (?,1) && -2 + H + I >= 0 && -1 + F + I >= 0 && -1 + -1*F + I >= 0 && -2 + E + I >= 0 && -1*E + I >= 0 && -1 + D + I >= 0 && -1 + C + I >= 0 && -1 + H >= 0 && -1 + F + H >= 0 && -1 + -1*F + H >= 0 && -2 + E + H >= 0 && -1*E + H >= 0 && -1 + D + H >= 0 && -1 + C + H >= 0 && -1*F >= 0 && -1 + E + -1*F >= 0 && 1 + -1*E + -1*F >= 0 && D + -1*F >= 0 && C + -1*F >= 0 && F >= 0 && -1 + E + F >= 0 && 1 + -1*E + F >= 0 && D + F >= 0 && C + F >= 0 && 1 + -1*E >= 0 && 1 + D + -1*E >= 0 && 1 + C + -1*E >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && -1 + C + E >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1*C + D >= 0 && C >= 0 && I >= 1 + D && C >= H && D >= 1 && C >= 1 && 0 >= 1 + K && C + D >= 1 && E = 1] 1. f30(A,B,C,D,E,F,G,H,I,J) -> f30(L,K,-1 + C,-1 + C,1,F,G,H,I,J) [-1 + I >= 0 (?,1) && -2 + H + I >= 0 && -1 + F + I >= 0 && -1 + -1*F + I >= 0 && -2 + E + I >= 0 && -1*E + I >= 0 && -1 + D + I >= 0 && -1 + C + I >= 0 && -1 + H >= 0 && -1 + F + H >= 0 && -1 + -1*F + H >= 0 && -2 + E + H >= 0 && -1*E + H >= 0 && -1 + D + H >= 0 && -1 + C + H >= 0 && -1*F >= 0 && -1 + E + -1*F >= 0 && 1 + -1*E + -1*F >= 0 && D + -1*F >= 0 && C + -1*F >= 0 && F >= 0 && -1 + E + F >= 0 && 1 + -1*E + F >= 0 && D + F >= 0 && C + F >= 0 && 1 + -1*E >= 0 && 1 + D + -1*E >= 0 && 1 + C + -1*E >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && -1 + C + E >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1*C + D >= 0 && C >= 0 && I >= 1 + D && C >= H && D >= 1 && C >= 1 && K >= 1 && C + D >= 1 && E = 1] 2. f30(A,B,C,D,E,F,G,H,I,J) -> f28(L,0,-2 + D,-1 + D,1,F,G,H,I,J) [-1 + I >= 0 (?,1) && -2 + H + I >= 0 && -1 + F + I >= 0 && -1 + -1*F + I >= 0 && -2 + E + I >= 0 && -1*E + I >= 0 && -1 + D + I >= 0 && -1 + C + I >= 0 && -1 + H >= 0 && -1 + F + H >= 0 && -1 + -1*F + H >= 0 && -2 + E + H >= 0 && -1*E + H >= 0 && -1 + D + H >= 0 && -1 + C + H >= 0 && -1*F >= 0 && -1 + E + -1*F >= 0 && 1 + -1*E + -1*F >= 0 && D + -1*F >= 0 && C + -1*F >= 0 && F >= 0 && -1 + E + F >= 0 && 1 + -1*E + F >= 0 && D + F >= 0 && C + F >= 0 && 1 + -1*E >= 0 && 1 + D + -1*E >= 0 && 1 + C + -1*E >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && -1 + C + E >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1*C + D >= 0 && C >= 0 && I >= 1 + D && C >= H && D >= 1 && C + D >= 1 && C >= 1 && E = 1] 3. f30(A,B,C,D,E,F,G,H,I,J) -> f30(L,K,-1 + C,-1 + C,1,F,G,H,I,J) [-1 + I >= 0 (?,1) && -2 + H + I >= 0 && -1 + F + I >= 0 && -1 + -1*F + I >= 0 && -2 + E + I >= 0 && -1*E + I >= 0 && -1 + D + I >= 0 && -1 + C + I >= 0 && -1 + H >= 0 && -1 + F + H >= 0 && -1 + -1*F + H >= 0 && -2 + E + H >= 0 && -1*E + H >= 0 && -1 + D + H >= 0 && -1 + C + H >= 0 && -1*F >= 0 && -1 + E + -1*F >= 0 && 1 + -1*E + -1*F >= 0 && D + -1*F >= 0 && C + -1*F >= 0 && F >= 0 && -1 + E + F >= 0 && 1 + -1*E + F >= 0 && D + F >= 0 && C + F >= 0 && 1 + -1*E >= 0 && 1 + D + -1*E >= 0 && 1 + C + -1*E >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && -1 + C + E >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1*C + D >= 0 && C >= 0 && H >= 1 + C && D >= 1 && C >= 1 && 0 >= 1 + K && C + D >= 1 && E = 1] 4. f30(A,B,C,D,E,F,G,H,I,J) -> f30(L,K,-1 + C,-1 + C,1,F,G,H,I,J) [-1 + I >= 0 (?,1) && -2 + H + I >= 0 && -1 + F + I >= 0 && -1 + -1*F + I >= 0 && -2 + E + I >= 0 && -1*E + I >= 0 && -1 + D + I >= 0 && -1 + C + I >= 0 && -1 + H >= 0 && -1 + F + H >= 0 && -1 + -1*F + H >= 0 && -2 + E + H >= 0 && -1*E + H >= 0 && -1 + D + H >= 0 && -1 + C + H >= 0 && -1*F >= 0 && -1 + E + -1*F >= 0 && 1 + -1*E + -1*F >= 0 && D + -1*F >= 0 && C + -1*F >= 0 && F >= 0 && -1 + E + F >= 0 && 1 + -1*E + F >= 0 && D + F >= 0 && C + F >= 0 && 1 + -1*E >= 0 && 1 + D + -1*E >= 0 && 1 + C + -1*E >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && -1 + C + E >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1*C + D >= 0 && C >= 0 && H >= 1 + C && D >= 1 && C >= 1 && K >= 1 && C + D >= 1 && E = 1] 5. f30(A,B,C,D,E,F,G,H,I,J) -> f28(L,0,-2 + D,-1 + D,1,F,G,H,I,J) [-1 + I >= 0 (?,1) && -2 + H + I >= 0 && -1 + F + I >= 0 && -1 + -1*F + I >= 0 && -2 + E + I >= 0 && -1*E + I >= 0 && -1 + D + I >= 0 && -1 + C + I >= 0 && -1 + H >= 0 && -1 + F + H >= 0 && -1 + -1*F + H >= 0 && -2 + E + H >= 0 && -1*E + H >= 0 && -1 + D + H >= 0 && -1 + C + H >= 0 && -1*F >= 0 && -1 + E + -1*F >= 0 && 1 + -1*E + -1*F >= 0 && D + -1*F >= 0 && C + -1*F >= 0 && F >= 0 && -1 + E + F >= 0 && 1 + -1*E + F >= 0 && D + F >= 0 && C + F >= 0 && 1 + -1*E >= 0 && 1 + D + -1*E >= 0 && 1 + C + -1*E >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && -1 + C + E >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1*C + D >= 0 && C >= 0 && H >= 1 + C && D >= 1 && C + D >= 1 && C >= 1 && E = 1] 6. f30(A,B,C,D,E,F,G,H,I,J) -> f9(A,B,C,D,E,F,G,H,I,L) [-1 + I >= 0 (?,1) && -2 + H + I >= 0 && -1 + F + I >= 0 && -1 + -1*F + I >= 0 && -2 + E + I >= 0 && -1*E + I >= 0 && -1 + D + I >= 0 && -1 + C + I >= 0 && -1 + H >= 0 && -1 + F + H >= 0 && -1 + -1*F + H >= 0 && -2 + E + H >= 0 && -1*E + H >= 0 && -1 + D + H >= 0 && -1 + C + H >= 0 && -1*F >= 0 && -1 + E + -1*F >= 0 && 1 + -1*E + -1*F >= 0 && D + -1*F >= 0 && C + -1*F >= 0 && F >= 0 && -1 + E + F >= 0 && 1 + -1*E + F >= 0 && D + F >= 0 && C + F >= 0 && 1 + -1*E >= 0 && 1 + D + -1*E >= 0 && 1 + C + -1*E >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && -1 + C + E >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1*C + D >= 0 && C >= 0 && 0 >= C] 7. f28(A,B,C,D,E,F,G,H,I,J) -> f30(L,K,-1 + C,-1 + C,1,F,G,H,I,J) [-1 + I >= 0 (?,1) && -2 + H + I >= 0 && -1 + F + I >= 0 && -1 + -1*F + I >= 0 && -2 + E + I >= 0 && -1*E + I >= 0 && -1 + D + I >= 0 && C + I >= 0 && -1 + B + I >= 0 && -1 + -1*B + I >= 0 && -1 + H >= 0 && -1 + F + H >= 0 && -1 + -1*F + H >= 0 && -2 + E + H >= 0 && -1*E + H >= 0 && -1 + D + H >= 0 && C + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -1*F >= 0 && -1 + E + -1*F >= 0 && 1 + -1*E + -1*F >= 0 && D + -1*F >= 0 && 1 + C + -1*F >= 0 && B + -1*F >= 0 && -1*B + -1*F >= 0 && F >= 0 && -1 + E + F >= 0 && 1 + -1*E + F >= 0 && D + F >= 0 && 1 + C + F >= 0 && B + F >= 0 && -1*B + F >= 0 && 1 + -1*E >= 0 && 1 + D + -1*E >= 0 && 2 + C + -1*E >= 0 && 1 + B + -1*E >= 0 && 1 + -1*B + -1*E >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && C + E >= 0 && -1 + B + E >= 0 && -1 + -1*B + E >= 0 && 1 + C + -1*D >= 0 && D >= 0 && 1 + C + D >= 0 && -1 + -1*C + D >= 0 && B + D >= 0 && -1*B + D >= 0 && 1 + C >= 0 && 1 + B + C >= 0 && 1 + -1*B + C >= 0 && -1*B >= 0 && B >= 0 && H >= 1 + C && D >= 1 && C >= 1 && 0 >= 1 + K && C + D >= 1 && E = 1] 8. f28(A,B,C,D,E,F,G,H,I,J) -> f30(L,K,-1 + C,-1 + C,1,F,G,H,I,J) [-1 + I >= 0 (?,1) && -2 + H + I >= 0 && -1 + F + I >= 0 && -1 + -1*F + I >= 0 && -2 + E + I >= 0 && -1*E + I >= 0 && -1 + D + I >= 0 && C + I >= 0 && -1 + B + I >= 0 && -1 + -1*B + I >= 0 && -1 + H >= 0 && -1 + F + H >= 0 && -1 + -1*F + H >= 0 && -2 + E + H >= 0 && -1*E + H >= 0 && -1 + D + H >= 0 && C + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -1*F >= 0 && -1 + E + -1*F >= 0 && 1 + -1*E + -1*F >= 0 && D + -1*F >= 0 && 1 + C + -1*F >= 0 && B + -1*F >= 0 && -1*B + -1*F >= 0 && F >= 0 && -1 + E + F >= 0 && 1 + -1*E + F >= 0 && D + F >= 0 && 1 + C + F >= 0 && B + F >= 0 && -1*B + F >= 0 && 1 + -1*E >= 0 && 1 + D + -1*E >= 0 && 2 + C + -1*E >= 0 && 1 + B + -1*E >= 0 && 1 + -1*B + -1*E >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && C + E >= 0 && -1 + B + E >= 0 && -1 + -1*B + E >= 0 && 1 + C + -1*D >= 0 && D >= 0 && 1 + C + D >= 0 && -1 + -1*C + D >= 0 && B + D >= 0 && -1*B + D >= 0 && 1 + C >= 0 && 1 + B + C >= 0 && 1 + -1*B + C >= 0 && -1*B >= 0 && B >= 0 && H >= 1 + C && D >= 1 && C >= 1 && K >= 1 && C + D >= 1 && E = 1] 9. f28(A,B,C,D,E,F,G,H,I,J) -> f28(L,0,-2 + D,-1 + D,1,F,G,H,I,J) [-1 + I >= 0 (?,1) && -2 + H + I >= 0 && -1 + F + I >= 0 && -1 + -1*F + I >= 0 && -2 + E + I >= 0 && -1*E + I >= 0 && -1 + D + I >= 0 && C + I >= 0 && -1 + B + I >= 0 && -1 + -1*B + I >= 0 && -1 + H >= 0 && -1 + F + H >= 0 && -1 + -1*F + H >= 0 && -2 + E + H >= 0 && -1*E + H >= 0 && -1 + D + H >= 0 && C + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -1*F >= 0 && -1 + E + -1*F >= 0 && 1 + -1*E + -1*F >= 0 && D + -1*F >= 0 && 1 + C + -1*F >= 0 && B + -1*F >= 0 && -1*B + -1*F >= 0 && F >= 0 && -1 + E + F >= 0 && 1 + -1*E + F >= 0 && D + F >= 0 && 1 + C + F >= 0 && B + F >= 0 && -1*B + F >= 0 && 1 + -1*E >= 0 && 1 + D + -1*E >= 0 && 2 + C + -1*E >= 0 && 1 + B + -1*E >= 0 && 1 + -1*B + -1*E >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && C + E >= 0 && -1 + B + E >= 0 && -1 + -1*B + E >= 0 && 1 + C + -1*D >= 0 && D >= 0 && 1 + C + D >= 0 && -1 + -1*C + D >= 0 && B + D >= 0 && -1*B + D >= 0 && 1 + C >= 0 && 1 + B + C >= 0 && 1 + -1*B + C >= 0 && -1*B >= 0 && B >= 0 && H >= 1 + C && D >= 1 && C + D >= 1 && C >= 1 && E = 1] 10. f28(A,B,C,D,E,F,G,H,I,J) -> f30(L,K,-1 + C,-1 + C,1,F,G,H,I,J) [-1 + I >= 0 (?,1) && -2 + H + I >= 0 && -1 + F + I >= 0 && -1 + -1*F + I >= 0 && -2 + E + I >= 0 && -1*E + I >= 0 && -1 + D + I >= 0 && C + I >= 0 && -1 + B + I >= 0 && -1 + -1*B + I >= 0 && -1 + H >= 0 && -1 + F + H >= 0 && -1 + -1*F + H >= 0 && -2 + E + H >= 0 && -1*E + H >= 0 && -1 + D + H >= 0 && C + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -1*F >= 0 && -1 + E + -1*F >= 0 && 1 + -1*E + -1*F >= 0 && D + -1*F >= 0 && 1 + C + -1*F >= 0 && B + -1*F >= 0 && -1*B + -1*F >= 0 && F >= 0 && -1 + E + F >= 0 && 1 + -1*E + F >= 0 && D + F >= 0 && 1 + C + F >= 0 && B + F >= 0 && -1*B + F >= 0 && 1 + -1*E >= 0 && 1 + D + -1*E >= 0 && 2 + C + -1*E >= 0 && 1 + B + -1*E >= 0 && 1 + -1*B + -1*E >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && C + E >= 0 && -1 + B + E >= 0 && -1 + -1*B + E >= 0 && 1 + C + -1*D >= 0 && D >= 0 && 1 + C + D >= 0 && -1 + -1*C + D >= 0 && B + D >= 0 && -1*B + D >= 0 && 1 + C >= 0 && 1 + B + C >= 0 && 1 + -1*B + C >= 0 && -1*B >= 0 && B >= 0 && I >= 1 + D && C >= H && D >= 1 && C >= 1 && 0 >= 1 + K && C + D >= 1 && E = 1] 11. f28(A,B,C,D,E,F,G,H,I,J) -> f30(L,K,-1 + C,-1 + C,1,F,G,H,I,J) [-1 + I >= 0 (?,1) && -2 + H + I >= 0 && -1 + F + I >= 0 && -1 + -1*F + I >= 0 && -2 + E + I >= 0 && -1*E + I >= 0 && -1 + D + I >= 0 && C + I >= 0 && -1 + B + I >= 0 && -1 + -1*B + I >= 0 && -1 + H >= 0 && -1 + F + H >= 0 && -1 + -1*F + H >= 0 && -2 + E + H >= 0 && -1*E + H >= 0 && -1 + D + H >= 0 && C + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -1*F >= 0 && -1 + E + -1*F >= 0 && 1 + -1*E + -1*F >= 0 && D + -1*F >= 0 && 1 + C + -1*F >= 0 && B + -1*F >= 0 && -1*B + -1*F >= 0 && F >= 0 && -1 + E + F >= 0 && 1 + -1*E + F >= 0 && D + F >= 0 && 1 + C + F >= 0 && B + F >= 0 && -1*B + F >= 0 && 1 + -1*E >= 0 && 1 + D + -1*E >= 0 && 2 + C + -1*E >= 0 && 1 + B + -1*E >= 0 && 1 + -1*B + -1*E >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && C + E >= 0 && -1 + B + E >= 0 && -1 + -1*B + E >= 0 && 1 + C + -1*D >= 0 && D >= 0 && 1 + C + D >= 0 && -1 + -1*C + D >= 0 && B + D >= 0 && -1*B + D >= 0 && 1 + C >= 0 && 1 + B + C >= 0 && 1 + -1*B + C >= 0 && -1*B >= 0 && B >= 0 && I >= 1 + D && C >= H && D >= 1 && C >= 1 && K >= 1 && C + D >= 1 && E = 1] 12. f28(A,B,C,D,E,F,G,H,I,J) -> f28(L,0,-2 + D,-1 + D,1,F,G,H,I,J) [-1 + I >= 0 (?,1) && -2 + H + I >= 0 && -1 + F + I >= 0 && -1 + -1*F + I >= 0 && -2 + E + I >= 0 && -1*E + I >= 0 && -1 + D + I >= 0 && C + I >= 0 && -1 + B + I >= 0 && -1 + -1*B + I >= 0 && -1 + H >= 0 && -1 + F + H >= 0 && -1 + -1*F + H >= 0 && -2 + E + H >= 0 && -1*E + H >= 0 && -1 + D + H >= 0 && C + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -1*F >= 0 && -1 + E + -1*F >= 0 && 1 + -1*E + -1*F >= 0 && D + -1*F >= 0 && 1 + C + -1*F >= 0 && B + -1*F >= 0 && -1*B + -1*F >= 0 && F >= 0 && -1 + E + F >= 0 && 1 + -1*E + F >= 0 && D + F >= 0 && 1 + C + F >= 0 && B + F >= 0 && -1*B + F >= 0 && 1 + -1*E >= 0 && 1 + D + -1*E >= 0 && 2 + C + -1*E >= 0 && 1 + B + -1*E >= 0 && 1 + -1*B + -1*E >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && C + E >= 0 && -1 + B + E >= 0 && -1 + -1*B + E >= 0 && 1 + C + -1*D >= 0 && D >= 0 && 1 + C + D >= 0 && -1 + -1*C + D >= 0 && B + D >= 0 && -1*B + D >= 0 && 1 + C >= 0 && 1 + B + C >= 0 && 1 + -1*B + C >= 0 && -1*B >= 0 && B >= 0 && I >= 1 + D && C >= H && D >= 1 && C + D >= 1 && C >= 1 && E = 1] 13. f28(A,B,C,D,E,F,G,H,I,J) -> f9(A,B,C,D,E,F,G,H,I,L) [-1 + I >= 0 (?,1) && -2 + H + I >= 0 && -1 + F + I >= 0 && -1 + -1*F + I >= 0 && -2 + E + I >= 0 && -1*E + I >= 0 && -1 + D + I >= 0 && C + I >= 0 && -1 + B + I >= 0 && -1 + -1*B + I >= 0 && -1 + H >= 0 && -1 + F + H >= 0 && -1 + -1*F + H >= 0 && -2 + E + H >= 0 && -1*E + H >= 0 && -1 + D + H >= 0 && C + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -1*F >= 0 && -1 + E + -1*F >= 0 && 1 + -1*E + -1*F >= 0 && D + -1*F >= 0 && 1 + C + -1*F >= 0 && B + -1*F >= 0 && -1*B + -1*F >= 0 && F >= 0 && -1 + E + F >= 0 && 1 + -1*E + F >= 0 && D + F >= 0 && 1 + C + F >= 0 && B + F >= 0 && -1*B + F >= 0 && 1 + -1*E >= 0 && 1 + D + -1*E >= 0 && 2 + C + -1*E >= 0 && 1 + B + -1*E >= 0 && 1 + -1*B + -1*E >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && C + E >= 0 && -1 + B + E >= 0 && -1 + -1*B + E >= 0 && 1 + C + -1*D >= 0 && D >= 0 && 1 + C + D >= 0 && -1 + -1*C + D >= 0 && B + D >= 0 && -1*B + D >= 0 && 1 + C >= 0 && 1 + B + C >= 0 && 1 + -1*B + C >= 0 && -1*B >= 0 && B >= 0 && 0 >= C] 14. f27(A,B,C,D,E,F,G,H,I,J) -> f27(L,0,-2 + D,-1 + D,0,F,0,H,I,J) [-1*F >= 0 (?,1) && E + -1*F >= 0 && -1*E + -1*F >= 0 && F >= 0 && E + F >= 0 && -1*E + F >= 0 && -1*E >= 0 && E >= 0 && D >= 1 && C + D >= 1 && C >= 1 && E = 0] 15. f27(A,B,C,D,E,F,G,H,I,J) -> f27(L,K,-1 + C,-1 + C,0,F,0,H,I,J) [-1*F >= 0 (?,1) && E + -1*F >= 0 && -1*E + -1*F >= 0 && F >= 0 && E + F >= 0 && -1*E + F >= 0 && -1*E >= 0 && E >= 0 && D >= 1 && C >= 1 && 0 >= 1 + K && C + D >= 1 && E = 0] 16. f27(A,B,C,D,E,F,G,H,I,J) -> f27(L,K,-1 + C,-1 + C,0,F,0,H,I,J) [-1*F >= 0 (?,1) && E + -1*F >= 0 && -1*E + -1*F >= 0 && F >= 0 && E + F >= 0 && -1*E + F >= 0 && -1*E >= 0 && E >= 0 && D >= 1 && C >= 1 && K >= 1 && C + D >= 1 && E = 0] 17. f27(A,B,C,D,E,F,G,H,I,J) -> f30(L,K,-1 + C,-1 + C,1,F,M,C,D,J) [-1*F >= 0 (?,1) && E + -1*F >= 0 && -1*E + -1*F >= 0 && F >= 0 && E + F >= 0 && -1*E + F >= 0 && -1*E >= 0 && E >= 0 && D >= 1 && C >= 1 && C + D >= 1 && 0 >= 1 + K && 0 >= 1 + M && E = 0] 18. f27(A,B,C,D,E,F,G,H,I,J) -> f30(L,K,-1 + C,-1 + C,1,F,M,C,D,J) [-1*F >= 0 (?,1) && E + -1*F >= 0 && -1*E + -1*F >= 0 && F >= 0 && E + F >= 0 && -1*E + F >= 0 && -1*E >= 0 && E >= 0 && D >= 1 && C >= 1 && C + D >= 1 && 0 >= 1 + K && M >= 1 && E = 0] 19. f27(A,B,C,D,E,F,G,H,I,J) -> f30(L,K,-1 + C,-1 + C,1,F,M,C,D,J) [-1*F >= 0 (?,1) && E + -1*F >= 0 && -1*E + -1*F >= 0 && F >= 0 && E + F >= 0 && -1*E + F >= 0 && -1*E >= 0 && E >= 0 && D >= 1 && C >= 1 && C + D >= 1 && K >= 1 && 0 >= 1 + M && E = 0] 20. f27(A,B,C,D,E,F,G,H,I,J) -> f30(L,K,-1 + C,-1 + C,1,F,M,C,D,J) [-1*F >= 0 (?,1) && E + -1*F >= 0 && -1*E + -1*F >= 0 && F >= 0 && E + F >= 0 && -1*E + F >= 0 && -1*E >= 0 && E >= 0 && D >= 1 && C >= 1 && C + D >= 1 && K >= 1 && M >= 1 && E = 0] 21. f27(A,B,C,D,E,F,G,H,I,J) -> f28(L,0,-2 + D,-1 + D,1,F,K,C,D,J) [-1*F >= 0 (?,1) && E + -1*F >= 0 && -1*E + -1*F >= 0 && F >= 0 && E + F >= 0 && -1*E + F >= 0 && -1*E >= 0 && E >= 0 && D >= 1 && C >= 1 && 0 >= 1 + K && C + D >= 1 && E = 0] 22. f27(A,B,C,D,E,F,G,H,I,J) -> f28(L,0,-2 + D,-1 + D,1,F,K,C,D,J) [-1*F >= 0 (?,1) && E + -1*F >= 0 && -1*E + -1*F >= 0 && F >= 0 && E + F >= 0 && -1*E + F >= 0 && -1*E >= 0 && E >= 0 && D >= 1 && C >= 1 && K >= 1 && C + D >= 1 && E = 0] 23. f27(A,B,C,D,E,F,G,H,I,J) -> f9(A,B,C,D,E,F,G,H,I,L) [-1*F >= 0 (?,1) && E + -1*F >= 0 && -1*E + -1*F >= 0 && F >= 0 && E + F >= 0 && -1*E + F >= 0 && -1*E >= 0 && E >= 0 && 0 >= C] 24. f27(A,B,C,D,E,F,G,H,I,J) -> f9(A,B,C,D,E,F,G,H,I,L) [-1*F >= 0 (?,1) && E + -1*F >= 0 && -1*E + -1*F >= 0 && F >= 0 && E + F >= 0 && -1*E + F >= 0 && -1*E >= 0 && E >= 0 && C >= 1 && 0 >= D] 25. f8(A,B,C,D,E,F,G,H,I,J) -> f27(A,B,C,D,0,0,G,H,I,J) True (1,1) Signature: {(f27,10);(f28,10);(f30,10);(f8,10);(f9,10)} Flow Graph: [0->{0,1,2,3,4,5,6},1->{0,1,2,3,4,5,6},2->{7,8,9,10,11,12,13},3->{3,4,5,6},4->{3,4,5,6},5->{7,8,9,13} ,6->{},7->{3,4,5,6},8->{3,4,5,6},9->{7,8,9,13},10->{0,1,2,3,4,5,6},11->{0,1,2,3,4,5,6},12->{7,8,9,10,11,12 ,13},13->{},14->{14,15,16,17,18,19,20,21,22,23},15->{14,15,16,17,18,19,20,21,22,23},16->{14,15,16,17,18,19 ,20,21,22,23},17->{3,4,5,6},18->{3,4,5,6},19->{3,4,5,6},20->{3,4,5,6},21->{7,8,9,10,11,12,13},22->{7,8,9,10 ,11,12,13},23->{},24->{},25->{14,15,16,17,18,19,20,21,22,23,24}] + Applied Processor: FromIts + Details: () * Step 3: CloseWith NO + Considered Problem: Rules: f30(A,B,C,D,E,F,G,H,I,J) -> f30(L,K,-1 + C,-1 + C,1,F,G,H,I,J) [-1 + I >= 0 && -2 + H + I >= 0 && -1 + F + I >= 0 && -1 + -1*F + I >= 0 && -2 + E + I >= 0 && -1*E + I >= 0 && -1 + D + I >= 0 && -1 + C + I >= 0 && -1 + H >= 0 && -1 + F + H >= 0 && -1 + -1*F + H >= 0 && -2 + E + H >= 0 && -1*E + H >= 0 && -1 + D + H >= 0 && -1 + C + H >= 0 && -1*F >= 0 && -1 + E + -1*F >= 0 && 1 + -1*E + -1*F >= 0 && D + -1*F >= 0 && C + -1*F >= 0 && F >= 0 && -1 + E + F >= 0 && 1 + -1*E + F >= 0 && D + F >= 0 && C + F >= 0 && 1 + -1*E >= 0 && 1 + D + -1*E >= 0 && 1 + C + -1*E >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && -1 + C + E >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1*C + D >= 0 && C >= 0 && I >= 1 + D && C >= H && D >= 1 && C >= 1 && 0 >= 1 + K && C + D >= 1 && E = 1] f30(A,B,C,D,E,F,G,H,I,J) -> f30(L,K,-1 + C,-1 + C,1,F,G,H,I,J) [-1 + I >= 0 && -2 + H + I >= 0 && -1 + F + I >= 0 && -1 + -1*F + I >= 0 && -2 + E + I >= 0 && -1*E + I >= 0 && -1 + D + I >= 0 && -1 + C + I >= 0 && -1 + H >= 0 && -1 + F + H >= 0 && -1 + -1*F + H >= 0 && -2 + E + H >= 0 && -1*E + H >= 0 && -1 + D + H >= 0 && -1 + C + H >= 0 && -1*F >= 0 && -1 + E + -1*F >= 0 && 1 + -1*E + -1*F >= 0 && D + -1*F >= 0 && C + -1*F >= 0 && F >= 0 && -1 + E + F >= 0 && 1 + -1*E + F >= 0 && D + F >= 0 && C + F >= 0 && 1 + -1*E >= 0 && 1 + D + -1*E >= 0 && 1 + C + -1*E >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && -1 + C + E >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1*C + D >= 0 && C >= 0 && I >= 1 + D && C >= H && D >= 1 && C >= 1 && K >= 1 && C + D >= 1 && E = 1] f30(A,B,C,D,E,F,G,H,I,J) -> f28(L,0,-2 + D,-1 + D,1,F,G,H,I,J) [-1 + I >= 0 && -2 + H + I >= 0 && -1 + F + I >= 0 && -1 + -1*F + I >= 0 && -2 + E + I >= 0 && -1*E + I >= 0 && -1 + D + I >= 0 && -1 + C + I >= 0 && -1 + H >= 0 && -1 + F + H >= 0 && -1 + -1*F + H >= 0 && -2 + E + H >= 0 && -1*E + H >= 0 && -1 + D + H >= 0 && -1 + C + H >= 0 && -1*F >= 0 && -1 + E + -1*F >= 0 && 1 + -1*E + -1*F >= 0 && D + -1*F >= 0 && C + -1*F >= 0 && F >= 0 && -1 + E + F >= 0 && 1 + -1*E + F >= 0 && D + F >= 0 && C + F >= 0 && 1 + -1*E >= 0 && 1 + D + -1*E >= 0 && 1 + C + -1*E >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && -1 + C + E >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1*C + D >= 0 && C >= 0 && I >= 1 + D && C >= H && D >= 1 && C + D >= 1 && C >= 1 && E = 1] f30(A,B,C,D,E,F,G,H,I,J) -> f30(L,K,-1 + C,-1 + C,1,F,G,H,I,J) [-1 + I >= 0 && -2 + H + I >= 0 && -1 + F + I >= 0 && -1 + -1*F + I >= 0 && -2 + E + I >= 0 && -1*E + I >= 0 && -1 + D + I >= 0 && -1 + C + I >= 0 && -1 + H >= 0 && -1 + F + H >= 0 && -1 + -1*F + H >= 0 && -2 + E + H >= 0 && -1*E + H >= 0 && -1 + D + H >= 0 && -1 + C + H >= 0 && -1*F >= 0 && -1 + E + -1*F >= 0 && 1 + -1*E + -1*F >= 0 && D + -1*F >= 0 && C + -1*F >= 0 && F >= 0 && -1 + E + F >= 0 && 1 + -1*E + F >= 0 && D + F >= 0 && C + F >= 0 && 1 + -1*E >= 0 && 1 + D + -1*E >= 0 && 1 + C + -1*E >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && -1 + C + E >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1*C + D >= 0 && C >= 0 && H >= 1 + C && D >= 1 && C >= 1 && 0 >= 1 + K && C + D >= 1 && E = 1] f30(A,B,C,D,E,F,G,H,I,J) -> f30(L,K,-1 + C,-1 + C,1,F,G,H,I,J) [-1 + I >= 0 && -2 + H + I >= 0 && -1 + F + I >= 0 && -1 + -1*F + I >= 0 && -2 + E + I >= 0 && -1*E + I >= 0 && -1 + D + I >= 0 && -1 + C + I >= 0 && -1 + H >= 0 && -1 + F + H >= 0 && -1 + -1*F + H >= 0 && -2 + E + H >= 0 && -1*E + H >= 0 && -1 + D + H >= 0 && -1 + C + H >= 0 && -1*F >= 0 && -1 + E + -1*F >= 0 && 1 + -1*E + -1*F >= 0 && D + -1*F >= 0 && C + -1*F >= 0 && F >= 0 && -1 + E + F >= 0 && 1 + -1*E + F >= 0 && D + F >= 0 && C + F >= 0 && 1 + -1*E >= 0 && 1 + D + -1*E >= 0 && 1 + C + -1*E >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && -1 + C + E >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1*C + D >= 0 && C >= 0 && H >= 1 + C && D >= 1 && C >= 1 && K >= 1 && C + D >= 1 && E = 1] f30(A,B,C,D,E,F,G,H,I,J) -> f28(L,0,-2 + D,-1 + D,1,F,G,H,I,J) [-1 + I >= 0 && -2 + H + I >= 0 && -1 + F + I >= 0 && -1 + -1*F + I >= 0 && -2 + E + I >= 0 && -1*E + I >= 0 && -1 + D + I >= 0 && -1 + C + I >= 0 && -1 + H >= 0 && -1 + F + H >= 0 && -1 + -1*F + H >= 0 && -2 + E + H >= 0 && -1*E + H >= 0 && -1 + D + H >= 0 && -1 + C + H >= 0 && -1*F >= 0 && -1 + E + -1*F >= 0 && 1 + -1*E + -1*F >= 0 && D + -1*F >= 0 && C + -1*F >= 0 && F >= 0 && -1 + E + F >= 0 && 1 + -1*E + F >= 0 && D + F >= 0 && C + F >= 0 && 1 + -1*E >= 0 && 1 + D + -1*E >= 0 && 1 + C + -1*E >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && -1 + C + E >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1*C + D >= 0 && C >= 0 && H >= 1 + C && D >= 1 && C + D >= 1 && C >= 1 && E = 1] f30(A,B,C,D,E,F,G,H,I,J) -> f9(A,B,C,D,E,F,G,H,I,L) [-1 + I >= 0 && -2 + H + I >= 0 && -1 + F + I >= 0 && -1 + -1*F + I >= 0 && -2 + E + I >= 0 && -1*E + I >= 0 && -1 + D + I >= 0 && -1 + C + I >= 0 && -1 + H >= 0 && -1 + F + H >= 0 && -1 + -1*F + H >= 0 && -2 + E + H >= 0 && -1*E + H >= 0 && -1 + D + H >= 0 && -1 + C + H >= 0 && -1*F >= 0 && -1 + E + -1*F >= 0 && 1 + -1*E + -1*F >= 0 && D + -1*F >= 0 && C + -1*F >= 0 && F >= 0 && -1 + E + F >= 0 && 1 + -1*E + F >= 0 && D + F >= 0 && C + F >= 0 && 1 + -1*E >= 0 && 1 + D + -1*E >= 0 && 1 + C + -1*E >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && -1 + C + E >= 0 && C + -1*D >= 0 && D >= 0 && C + D >= 0 && -1*C + D >= 0 && C >= 0 && 0 >= C] f28(A,B,C,D,E,F,G,H,I,J) -> f30(L,K,-1 + C,-1 + C,1,F,G,H,I,J) [-1 + I >= 0 && -2 + H + I >= 0 && -1 + F + I >= 0 && -1 + -1*F + I >= 0 && -2 + E + I >= 0 && -1*E + I >= 0 && -1 + D + I >= 0 && C + I >= 0 && -1 + B + I >= 0 && -1 + -1*B + I >= 0 && -1 + H >= 0 && -1 + F + H >= 0 && -1 + -1*F + H >= 0 && -2 + E + H >= 0 && -1*E + H >= 0 && -1 + D + H >= 0 && C + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -1*F >= 0 && -1 + E + -1*F >= 0 && 1 + -1*E + -1*F >= 0 && D + -1*F >= 0 && 1 + C + -1*F >= 0 && B + -1*F >= 0 && -1*B + -1*F >= 0 && F >= 0 && -1 + E + F >= 0 && 1 + -1*E + F >= 0 && D + F >= 0 && 1 + C + F >= 0 && B + F >= 0 && -1*B + F >= 0 && 1 + -1*E >= 0 && 1 + D + -1*E >= 0 && 2 + C + -1*E >= 0 && 1 + B + -1*E >= 0 && 1 + -1*B + -1*E >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && C + E >= 0 && -1 + B + E >= 0 && -1 + -1*B + E >= 0 && 1 + C + -1*D >= 0 && D >= 0 && 1 + C + D >= 0 && -1 + -1*C + D >= 0 && B + D >= 0 && -1*B + D >= 0 && 1 + C >= 0 && 1 + B + C >= 0 && 1 + -1*B + C >= 0 && -1*B >= 0 && B >= 0 && H >= 1 + C && D >= 1 && C >= 1 && 0 >= 1 + K && C + D >= 1 && E = 1] f28(A,B,C,D,E,F,G,H,I,J) -> f30(L,K,-1 + C,-1 + C,1,F,G,H,I,J) [-1 + I >= 0 && -2 + H + I >= 0 && -1 + F + I >= 0 && -1 + -1*F + I >= 0 && -2 + E + I >= 0 && -1*E + I >= 0 && -1 + D + I >= 0 && C + I >= 0 && -1 + B + I >= 0 && -1 + -1*B + I >= 0 && -1 + H >= 0 && -1 + F + H >= 0 && -1 + -1*F + H >= 0 && -2 + E + H >= 0 && -1*E + H >= 0 && -1 + D + H >= 0 && C + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -1*F >= 0 && -1 + E + -1*F >= 0 && 1 + -1*E + -1*F >= 0 && D + -1*F >= 0 && 1 + C + -1*F >= 0 && B + -1*F >= 0 && -1*B + -1*F >= 0 && F >= 0 && -1 + E + F >= 0 && 1 + -1*E + F >= 0 && D + F >= 0 && 1 + C + F >= 0 && B + F >= 0 && -1*B + F >= 0 && 1 + -1*E >= 0 && 1 + D + -1*E >= 0 && 2 + C + -1*E >= 0 && 1 + B + -1*E >= 0 && 1 + -1*B + -1*E >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && C + E >= 0 && -1 + B + E >= 0 && -1 + -1*B + E >= 0 && 1 + C + -1*D >= 0 && D >= 0 && 1 + C + D >= 0 && -1 + -1*C + D >= 0 && B + D >= 0 && -1*B + D >= 0 && 1 + C >= 0 && 1 + B + C >= 0 && 1 + -1*B + C >= 0 && -1*B >= 0 && B >= 0 && H >= 1 + C && D >= 1 && C >= 1 && K >= 1 && C + D >= 1 && E = 1] f28(A,B,C,D,E,F,G,H,I,J) -> f28(L,0,-2 + D,-1 + D,1,F,G,H,I,J) [-1 + I >= 0 && -2 + H + I >= 0 && -1 + F + I >= 0 && -1 + -1*F + I >= 0 && -2 + E + I >= 0 && -1*E + I >= 0 && -1 + D + I >= 0 && C + I >= 0 && -1 + B + I >= 0 && -1 + -1*B + I >= 0 && -1 + H >= 0 && -1 + F + H >= 0 && -1 + -1*F + H >= 0 && -2 + E + H >= 0 && -1*E + H >= 0 && -1 + D + H >= 0 && C + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -1*F >= 0 && -1 + E + -1*F >= 0 && 1 + -1*E + -1*F >= 0 && D + -1*F >= 0 && 1 + C + -1*F >= 0 && B + -1*F >= 0 && -1*B + -1*F >= 0 && F >= 0 && -1 + E + F >= 0 && 1 + -1*E + F >= 0 && D + F >= 0 && 1 + C + F >= 0 && B + F >= 0 && -1*B + F >= 0 && 1 + -1*E >= 0 && 1 + D + -1*E >= 0 && 2 + C + -1*E >= 0 && 1 + B + -1*E >= 0 && 1 + -1*B + -1*E >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && C + E >= 0 && -1 + B + E >= 0 && -1 + -1*B + E >= 0 && 1 + C + -1*D >= 0 && D >= 0 && 1 + C + D >= 0 && -1 + -1*C + D >= 0 && B + D >= 0 && -1*B + D >= 0 && 1 + C >= 0 && 1 + B + C >= 0 && 1 + -1*B + C >= 0 && -1*B >= 0 && B >= 0 && H >= 1 + C && D >= 1 && C + D >= 1 && C >= 1 && E = 1] f28(A,B,C,D,E,F,G,H,I,J) -> f30(L,K,-1 + C,-1 + C,1,F,G,H,I,J) [-1 + I >= 0 && -2 + H + I >= 0 && -1 + F + I >= 0 && -1 + -1*F + I >= 0 && -2 + E + I >= 0 && -1*E + I >= 0 && -1 + D + I >= 0 && C + I >= 0 && -1 + B + I >= 0 && -1 + -1*B + I >= 0 && -1 + H >= 0 && -1 + F + H >= 0 && -1 + -1*F + H >= 0 && -2 + E + H >= 0 && -1*E + H >= 0 && -1 + D + H >= 0 && C + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -1*F >= 0 && -1 + E + -1*F >= 0 && 1 + -1*E + -1*F >= 0 && D + -1*F >= 0 && 1 + C + -1*F >= 0 && B + -1*F >= 0 && -1*B + -1*F >= 0 && F >= 0 && -1 + E + F >= 0 && 1 + -1*E + F >= 0 && D + F >= 0 && 1 + C + F >= 0 && B + F >= 0 && -1*B + F >= 0 && 1 + -1*E >= 0 && 1 + D + -1*E >= 0 && 2 + C + -1*E >= 0 && 1 + B + -1*E >= 0 && 1 + -1*B + -1*E >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && C + E >= 0 && -1 + B + E >= 0 && -1 + -1*B + E >= 0 && 1 + C + -1*D >= 0 && D >= 0 && 1 + C + D >= 0 && -1 + -1*C + D >= 0 && B + D >= 0 && -1*B + D >= 0 && 1 + C >= 0 && 1 + B + C >= 0 && 1 + -1*B + C >= 0 && -1*B >= 0 && B >= 0 && I >= 1 + D && C >= H && D >= 1 && C >= 1 && 0 >= 1 + K && C + D >= 1 && E = 1] f28(A,B,C,D,E,F,G,H,I,J) -> f30(L,K,-1 + C,-1 + C,1,F,G,H,I,J) [-1 + I >= 0 && -2 + H + I >= 0 && -1 + F + I >= 0 && -1 + -1*F + I >= 0 && -2 + E + I >= 0 && -1*E + I >= 0 && -1 + D + I >= 0 && C + I >= 0 && -1 + B + I >= 0 && -1 + -1*B + I >= 0 && -1 + H >= 0 && -1 + F + H >= 0 && -1 + -1*F + H >= 0 && -2 + E + H >= 0 && -1*E + H >= 0 && -1 + D + H >= 0 && C + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -1*F >= 0 && -1 + E + -1*F >= 0 && 1 + -1*E + -1*F >= 0 && D + -1*F >= 0 && 1 + C + -1*F >= 0 && B + -1*F >= 0 && -1*B + -1*F >= 0 && F >= 0 && -1 + E + F >= 0 && 1 + -1*E + F >= 0 && D + F >= 0 && 1 + C + F >= 0 && B + F >= 0 && -1*B + F >= 0 && 1 + -1*E >= 0 && 1 + D + -1*E >= 0 && 2 + C + -1*E >= 0 && 1 + B + -1*E >= 0 && 1 + -1*B + -1*E >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && C + E >= 0 && -1 + B + E >= 0 && -1 + -1*B + E >= 0 && 1 + C + -1*D >= 0 && D >= 0 && 1 + C + D >= 0 && -1 + -1*C + D >= 0 && B + D >= 0 && -1*B + D >= 0 && 1 + C >= 0 && 1 + B + C >= 0 && 1 + -1*B + C >= 0 && -1*B >= 0 && B >= 0 && I >= 1 + D && C >= H && D >= 1 && C >= 1 && K >= 1 && C + D >= 1 && E = 1] f28(A,B,C,D,E,F,G,H,I,J) -> f28(L,0,-2 + D,-1 + D,1,F,G,H,I,J) [-1 + I >= 0 && -2 + H + I >= 0 && -1 + F + I >= 0 && -1 + -1*F + I >= 0 && -2 + E + I >= 0 && -1*E + I >= 0 && -1 + D + I >= 0 && C + I >= 0 && -1 + B + I >= 0 && -1 + -1*B + I >= 0 && -1 + H >= 0 && -1 + F + H >= 0 && -1 + -1*F + H >= 0 && -2 + E + H >= 0 && -1*E + H >= 0 && -1 + D + H >= 0 && C + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -1*F >= 0 && -1 + E + -1*F >= 0 && 1 + -1*E + -1*F >= 0 && D + -1*F >= 0 && 1 + C + -1*F >= 0 && B + -1*F >= 0 && -1*B + -1*F >= 0 && F >= 0 && -1 + E + F >= 0 && 1 + -1*E + F >= 0 && D + F >= 0 && 1 + C + F >= 0 && B + F >= 0 && -1*B + F >= 0 && 1 + -1*E >= 0 && 1 + D + -1*E >= 0 && 2 + C + -1*E >= 0 && 1 + B + -1*E >= 0 && 1 + -1*B + -1*E >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && C + E >= 0 && -1 + B + E >= 0 && -1 + -1*B + E >= 0 && 1 + C + -1*D >= 0 && D >= 0 && 1 + C + D >= 0 && -1 + -1*C + D >= 0 && B + D >= 0 && -1*B + D >= 0 && 1 + C >= 0 && 1 + B + C >= 0 && 1 + -1*B + C >= 0 && -1*B >= 0 && B >= 0 && I >= 1 + D && C >= H && D >= 1 && C + D >= 1 && C >= 1 && E = 1] f28(A,B,C,D,E,F,G,H,I,J) -> f9(A,B,C,D,E,F,G,H,I,L) [-1 + I >= 0 && -2 + H + I >= 0 && -1 + F + I >= 0 && -1 + -1*F + I >= 0 && -2 + E + I >= 0 && -1*E + I >= 0 && -1 + D + I >= 0 && C + I >= 0 && -1 + B + I >= 0 && -1 + -1*B + I >= 0 && -1 + H >= 0 && -1 + F + H >= 0 && -1 + -1*F + H >= 0 && -2 + E + H >= 0 && -1*E + H >= 0 && -1 + D + H >= 0 && C + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -1*F >= 0 && -1 + E + -1*F >= 0 && 1 + -1*E + -1*F >= 0 && D + -1*F >= 0 && 1 + C + -1*F >= 0 && B + -1*F >= 0 && -1*B + -1*F >= 0 && F >= 0 && -1 + E + F >= 0 && 1 + -1*E + F >= 0 && D + F >= 0 && 1 + C + F >= 0 && B + F >= 0 && -1*B + F >= 0 && 1 + -1*E >= 0 && 1 + D + -1*E >= 0 && 2 + C + -1*E >= 0 && 1 + B + -1*E >= 0 && 1 + -1*B + -1*E >= 0 && -1 + E >= 0 && -1 + D + E >= 0 && C + E >= 0 && -1 + B + E >= 0 && -1 + -1*B + E >= 0 && 1 + C + -1*D >= 0 && D >= 0 && 1 + C + D >= 0 && -1 + -1*C + D >= 0 && B + D >= 0 && -1*B + D >= 0 && 1 + C >= 0 && 1 + B + C >= 0 && 1 + -1*B + C >= 0 && -1*B >= 0 && B >= 0 && 0 >= C] f27(A,B,C,D,E,F,G,H,I,J) -> f27(L,0,-2 + D,-1 + D,0,F,0,H,I,J) [-1*F >= 0 && E + -1*F >= 0 && -1*E + -1*F >= 0 && F >= 0 && E + F >= 0 && -1*E + F >= 0 && -1*E >= 0 && E >= 0 && D >= 1 && C + D >= 1 && C >= 1 && E = 0] f27(A,B,C,D,E,F,G,H,I,J) -> f27(L,K,-1 + C,-1 + C,0,F,0,H,I,J) [-1*F >= 0 && E + -1*F >= 0 && -1*E + -1*F >= 0 && F >= 0 && E + F >= 0 && -1*E + F >= 0 && -1*E >= 0 && E >= 0 && D >= 1 && C >= 1 && 0 >= 1 + K && C + D >= 1 && E = 0] f27(A,B,C,D,E,F,G,H,I,J) -> f27(L,K,-1 + C,-1 + C,0,F,0,H,I,J) [-1*F >= 0 && E + -1*F >= 0 && -1*E + -1*F >= 0 && F >= 0 && E + F >= 0 && -1*E + F >= 0 && -1*E >= 0 && E >= 0 && D >= 1 && C >= 1 && K >= 1 && C + D >= 1 && E = 0] f27(A,B,C,D,E,F,G,H,I,J) -> f30(L,K,-1 + C,-1 + C,1,F,M,C,D,J) [-1*F >= 0 && E + -1*F >= 0 && -1*E + -1*F >= 0 && F >= 0 && E + F >= 0 && -1*E + F >= 0 && -1*E >= 0 && E >= 0 && D >= 1 && C >= 1 && C + D >= 1 && 0 >= 1 + K && 0 >= 1 + M && E = 0] f27(A,B,C,D,E,F,G,H,I,J) -> f30(L,K,-1 + C,-1 + C,1,F,M,C,D,J) [-1*F >= 0 && E + -1*F >= 0 && -1*E + -1*F >= 0 && F >= 0 && E + F >= 0 && -1*E + F >= 0 && -1*E >= 0 && E >= 0 && D >= 1 && C >= 1 && C + D >= 1 && 0 >= 1 + K && M >= 1 && E = 0] f27(A,B,C,D,E,F,G,H,I,J) -> f30(L,K,-1 + C,-1 + C,1,F,M,C,D,J) [-1*F >= 0 && E + -1*F >= 0 && -1*E + -1*F >= 0 && F >= 0 && E + F >= 0 && -1*E + F >= 0 && -1*E >= 0 && E >= 0 && D >= 1 && C >= 1 && C + D >= 1 && K >= 1 && 0 >= 1 + M && E = 0] f27(A,B,C,D,E,F,G,H,I,J) -> f30(L,K,-1 + C,-1 + C,1,F,M,C,D,J) [-1*F >= 0 && E + -1*F >= 0 && -1*E + -1*F >= 0 && F >= 0 && E + F >= 0 && -1*E + F >= 0 && -1*E >= 0 && E >= 0 && D >= 1 && C >= 1 && C + D >= 1 && K >= 1 && M >= 1 && E = 0] f27(A,B,C,D,E,F,G,H,I,J) -> f28(L,0,-2 + D,-1 + D,1,F,K,C,D,J) [-1*F >= 0 && E + -1*F >= 0 && -1*E + -1*F >= 0 && F >= 0 && E + F >= 0 && -1*E + F >= 0 && -1*E >= 0 && E >= 0 && D >= 1 && C >= 1 && 0 >= 1 + K && C + D >= 1 && E = 0] f27(A,B,C,D,E,F,G,H,I,J) -> f28(L,0,-2 + D,-1 + D,1,F,K,C,D,J) [-1*F >= 0 && E + -1*F >= 0 && -1*E + -1*F >= 0 && F >= 0 && E + F >= 0 && -1*E + F >= 0 && -1*E >= 0 && E >= 0 && D >= 1 && C >= 1 && K >= 1 && C + D >= 1 && E = 0] f27(A,B,C,D,E,F,G,H,I,J) -> f9(A,B,C,D,E,F,G,H,I,L) [-1*F >= 0 && E + -1*F >= 0 && -1*E + -1*F >= 0 && F >= 0 && E + F >= 0 && -1*E + F >= 0 && -1*E >= 0 && E >= 0 && 0 >= C] f27(A,B,C,D,E,F,G,H,I,J) -> f9(A,B,C,D,E,F,G,H,I,L) [-1*F >= 0 && E + -1*F >= 0 && -1*E + -1*F >= 0 && F >= 0 && E + F >= 0 && -1*E + F >= 0 && -1*E >= 0 && E >= 0 && C >= 1 && 0 >= D] f8(A,B,C,D,E,F,G,H,I,J) -> f27(A,B,C,D,0,0,G,H,I,J) True Signature: {(f27,10);(f28,10);(f30,10);(f8,10);(f9,10)} Rule Graph: [0->{0,1,2,3,4,5,6},1->{0,1,2,3,4,5,6},2->{7,8,9,10,11,12,13},3->{3,4,5,6},4->{3,4,5,6},5->{7,8,9,13} ,6->{},7->{3,4,5,6},8->{3,4,5,6},9->{7,8,9,13},10->{0,1,2,3,4,5,6},11->{0,1,2,3,4,5,6},12->{7,8,9,10,11,12 ,13},13->{},14->{14,15,16,17,18,19,20,21,22,23},15->{14,15,16,17,18,19,20,21,22,23},16->{14,15,16,17,18,19 ,20,21,22,23},17->{3,4,5,6},18->{3,4,5,6},19->{3,4,5,6},20->{3,4,5,6},21->{7,8,9,10,11,12,13},22->{7,8,9,10 ,11,12,13},23->{},24->{},25->{14,15,16,17,18,19,20,21,22,23,24}] + Applied Processor: CloseWith False + Details: () NO