YES * Step 1: UnsatPaths YES + Considered Problem: Rules: 0. f63(A,B,C,D,E,F,G,H,I,J,K,L) -> f71(A,B,C,0,E,F,G,H,I,J,K,1) [-11 + F >= 0 (?,1) && -1 + D + F >= 0 && -10 + -1*D + F >= 0 && -10 + -1*C + F >= 0 && -23 + B + F >= 0 && 1 + -1*B + F >= 0 && -10 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && D = 0] 1. f63(A,B,C,D,E,F,G,H,I,J,K,L) -> f71(A,B,C,D,E,F,G,H,I,J,K,0) [-11 + F >= 0 (?,1) && -1 + D + F >= 0 && -10 + -1*D + F >= 0 && -10 + -1*C + F >= 0 && -23 + B + F >= 0 && 1 + -1*B + F >= 0 && -10 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && D >= 1] 2. f63(A,B,C,D,E,F,G,H,I,J,K,L) -> f71(A,B,C,D,E,F,G,H,I,J,K,0) [-11 + F >= 0 (?,1) && -1 + D + F >= 0 && -10 + -1*D + F >= 0 && -10 + -1*C + F >= 0 && -23 + B + F >= 0 && 1 + -1*B + F >= 0 && -10 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && 0 >= 1 + D] 3. f62(A,B,C,D,E,F,G,H,I,J,K,L) -> f71(0,B,C,D,E,F,G,H,I,J,K,1) [-11 + F >= 0 (?,1) && -1 + D + F >= 0 && -10 + -1*D + F >= 0 && -10 + -1*C + F >= 0 && -23 + B + F >= 0 && 1 + -1*B + F >= 0 && -10 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && A = 0] 4. f62(A,B,C,D,E,F,G,H,I,J,K,L) -> f63(A,B,C,D,E,F,G,H,I,J,K,L) [-11 + F >= 0 (?,1) && -1 + D + F >= 0 && -10 + -1*D + F >= 0 && -10 + -1*C + F >= 0 && -23 + B + F >= 0 && 1 + -1*B + F >= 0 && -10 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && A >= 1] 5. f62(A,B,C,D,E,F,G,H,I,J,K,L) -> f63(A,B,C,D,E,F,G,H,I,J,K,L) [-11 + F >= 0 (?,1) && -1 + D + F >= 0 && -10 + -1*D + F >= 0 && -10 + -1*C + F >= 0 && -23 + B + F >= 0 && 1 + -1*B + F >= 0 && -10 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && 0 >= 1 + A] 6. f48(A,B,C,D,E,F,G,H,I,J,K,L) -> f48(A,B,C,0,E,1 + F,G,H,I,M,0,L) [F >= 0 (?,1) && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && B >= 2 + F && D = 0] 7. f48(A,B,C,D,E,F,G,H,I,J,K,L) -> f71(A,B,0,D,E,F,G,H,I,J,K,1) [F >= 0 (?,1) && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && 1 + F >= B && C = 0] 8. f48(A,B,C,D,E,F,G,H,I,J,K,L) -> f62(A,B,C,D,E,F,G,H,I,J,K,L) [F >= 0 (?,1) && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && C >= 1 && 1 + F >= B] 9. f48(A,B,C,D,E,F,G,H,I,J,K,L) -> f62(A,B,C,D,E,F,G,H,I,J,K,L) [F >= 0 (?,1) && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && 0 >= 1 + C && 1 + F >= B] 10. f52(A,B,C,D,E,F,G,H,I,J,K,L) -> f48(A,B,C,0,E,1 + F,G,H,I,J,0,L) [10 + -1*F >= 0 (?,1) && 19 + D + -1*F >= 0 && 11 + -1*D + -1*F >= 0 && 11 + -1*C + -1*F >= 0 && -2 + B + -1*F >= 0 && 22 + -1*B + -1*F >= 0 && 11 + -1*A + -1*F >= 0 && F >= 0 && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && 9 + D >= 0 && 10 + -1*C + D >= 0 && -3 + B + D >= 0 && 21 + -1*B + D >= 0 && 10 + -1*A + D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0] 11. f52(A,B,C,D,E,F,G,H,I,J,K,L) -> f48(A,B,C,0,E,1 + F,G,H,I,0,0,L) [10 + -1*F >= 0 (?,1) && 19 + D + -1*F >= 0 && 11 + -1*D + -1*F >= 0 && 11 + -1*C + -1*F >= 0 && -2 + B + -1*F >= 0 && 22 + -1*B + -1*F >= 0 && 11 + -1*A + -1*F >= 0 && F >= 0 && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && 9 + D >= 0 && 10 + -1*C + D >= 0 && -3 + B + D >= 0 && 21 + -1*B + D >= 0 && 10 + -1*A + D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && J = 0] 12. f52(A,B,C,D,E,F,G,H,I,J,K,L) -> f48(A,B,C,1,E,1 + F,G,H,I,J,1,L) [10 + -1*F >= 0 (?,1) && 19 + D + -1*F >= 0 && 11 + -1*D + -1*F >= 0 && 11 + -1*C + -1*F >= 0 && -2 + B + -1*F >= 0 && 22 + -1*B + -1*F >= 0 && 11 + -1*A + -1*F >= 0 && F >= 0 && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && 9 + D >= 0 && 10 + -1*C + D >= 0 && -3 + B + D >= 0 && 21 + -1*B + D >= 0 && 10 + -1*A + D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && J >= 1] 13. f52(A,B,C,D,E,F,G,H,I,J,K,L) -> f48(A,B,C,1,E,1 + F,G,H,I,J,1,L) [10 + -1*F >= 0 (?,1) && 19 + D + -1*F >= 0 && 11 + -1*D + -1*F >= 0 && 11 + -1*C + -1*F >= 0 && -2 + B + -1*F >= 0 && 22 + -1*B + -1*F >= 0 && 11 + -1*A + -1*F >= 0 && F >= 0 && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && 9 + D >= 0 && 10 + -1*C + D >= 0 && -3 + B + D >= 0 && 21 + -1*B + D >= 0 && 10 + -1*A + D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && 0 >= 1 + J] 14. f48(A,B,C,D,E,F,G,H,I,J,K,L) -> f52(A,B,C,D,E,F,G,H,I,M,K,L) [F >= 0 (?,1) && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && D >= 1 && B >= 2 + F] 15. f32(A,B,C,D,E,F,G,H,I,J,K,L) -> f48(A,B,C,D,E,0,G,H,I,J,K,L) [F >= 0 (?,1) && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && -1 + D >= 0 && -1*C + D >= 0 && -13 + B + D >= 0 && 11 + -1*B + D >= 0 && -1*A + D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && 1 + F >= B] 16. f35(A,B,C,D,E,F,G,H,I,J,K,L) -> f32(A,B,C,D,E,1 + F,G,H,I,J,K,L) [-1 + H >= 0 (?,1) && -1 + F + H >= 0 && -1 + -1*F + H >= 0 && -2 + D + H >= 0 && -1*D + H >= 0 && -1*C + H >= 0 && -13 + B + H >= 0 && 11 + -1*B + H >= 0 && -1*A + H >= 0 && F >= 0 && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && -1 + D >= 0 && -1*C + D >= 0 && -13 + B + D >= 0 && 11 + -1*B + D >= 0 && -1*A + D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && H >= B] 17. f38(A,B,C,D,E,F,G,H,I,J,K,L) -> f35(0,B,C,D,E,F,G,1 + H,0,J,K,L) [11 + -1*H >= 0 (?,1) && 11 + F + -1*H >= 0 && 21 + -1*F + -1*H >= 0 && 10 + D + -1*H >= 0 && 12 + -1*D + -1*H >= 0 && 12 + -1*C + -1*H >= 0 && -1 + B + -1*H >= 0 && 23 + -1*B + -1*H >= 0 && 12 + -1*A + -1*H >= 0 && -1 + H >= 0 && -1 + F + H >= 0 && -1 + -1*F + H >= 0 && -2 + D + H >= 0 && -1*D + H >= 0 && -1*C + H >= 0 && -13 + B + H >= 0 && 11 + -1*B + H >= 0 && -1*A + H >= 0 && 10 + -1*F >= 0 && 9 + D + -1*F >= 0 && 11 + -1*D + -1*F >= 0 && 11 + -1*C + -1*F >= 0 && -2 + B + -1*F >= 0 && 22 + -1*B + -1*F >= 0 && 11 + -1*A + -1*F >= 0 && F >= 0 && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && -1 + D >= 0 && -1*C + D >= 0 && -13 + B + D >= 0 && 11 + -1*B + D >= 0 && -1*A + D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0] 18. f38(A,B,C,D,E,F,G,H,I,J,K,L) -> f35(1,B,C,D,E,F,G,1 + H,1,J,K,L) [11 + -1*H >= 0 (?,1) && 11 + F + -1*H >= 0 && 21 + -1*F + -1*H >= 0 && 10 + D + -1*H >= 0 && 12 + -1*D + -1*H >= 0 && 12 + -1*C + -1*H >= 0 && -1 + B + -1*H >= 0 && 23 + -1*B + -1*H >= 0 && 12 + -1*A + -1*H >= 0 && -1 + H >= 0 && -1 + F + H >= 0 && -1 + -1*F + H >= 0 && -2 + D + H >= 0 && -1*D + H >= 0 && -1*C + H >= 0 && -13 + B + H >= 0 && 11 + -1*B + H >= 0 && -1*A + H >= 0 && 10 + -1*F >= 0 && 9 + D + -1*F >= 0 && 11 + -1*D + -1*F >= 0 && 11 + -1*C + -1*F >= 0 && -2 + B + -1*F >= 0 && 22 + -1*B + -1*F >= 0 && 11 + -1*A + -1*F >= 0 && F >= 0 && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && -1 + D >= 0 && -1*C + D >= 0 && -13 + B + D >= 0 && 11 + -1*B + D >= 0 && -1*A + D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0] 19. f38(A,B,C,D,E,F,G,H,I,J,K,L) -> f35(1,B,C,D,E,F,G,1 + H,1,J,K,L) [11 + -1*H >= 0 (?,1) && 11 + F + -1*H >= 0 && 21 + -1*F + -1*H >= 0 && 10 + D + -1*H >= 0 && 12 + -1*D + -1*H >= 0 && 12 + -1*C + -1*H >= 0 && -1 + B + -1*H >= 0 && 23 + -1*B + -1*H >= 0 && 12 + -1*A + -1*H >= 0 && -1 + H >= 0 && -1 + F + H >= 0 && -1 + -1*F + H >= 0 && -2 + D + H >= 0 && -1*D + H >= 0 && -1*C + H >= 0 && -13 + B + H >= 0 && 11 + -1*B + H >= 0 && -1*A + H >= 0 && 10 + -1*F >= 0 && 9 + D + -1*F >= 0 && 11 + -1*D + -1*F >= 0 && 11 + -1*C + -1*F >= 0 && -2 + B + -1*F >= 0 && 22 + -1*B + -1*F >= 0 && 11 + -1*A + -1*F >= 0 && F >= 0 && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && -1 + D >= 0 && -1*C + D >= 0 && -13 + B + D >= 0 && 11 + -1*B + D >= 0 && -1*A + D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && M >= 1 + N] 20. f35(A,B,C,D,E,F,G,H,I,J,K,L) -> f35(0,B,C,D,E,F,G,1 + H,0,J,K,L) [-1 + H >= 0 (?,1) && -1 + F + H >= 0 && -1 + -1*F + H >= 0 && -2 + D + H >= 0 && -1*D + H >= 0 && -1*C + H >= 0 && -13 + B + H >= 0 && 11 + -1*B + H >= 0 && -1*A + H >= 0 && F >= 0 && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && -1 + D >= 0 && -1*C + D >= 0 && -13 + B + D >= 0 && 11 + -1*B + D >= 0 && -1*A + D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && B >= 1 + H && A = 0] 21. f35(A,B,C,D,E,F,G,H,I,J,K,L) -> f38(A,B,C,D,E,F,G,H,I,J,K,L) [-1 + H >= 0 (?,1) && -1 + F + H >= 0 && -1 + -1*F + H >= 0 && -2 + D + H >= 0 && -1*D + H >= 0 && -1*C + H >= 0 && -13 + B + H >= 0 && 11 + -1*B + H >= 0 && -1*A + H >= 0 && F >= 0 && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && -1 + D >= 0 && -1*C + D >= 0 && -13 + B + D >= 0 && 11 + -1*B + D >= 0 && -1*A + D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && A >= 1 && B >= 1 + H] 22. f35(A,B,C,D,E,F,G,H,I,J,K,L) -> f38(A,B,C,D,E,F,G,H,I,J,K,L) [-1 + H >= 0 (?,1) && -1 + F + H >= 0 && -1 + -1*F + H >= 0 && -2 + D + H >= 0 && -1*D + H >= 0 && -1*C + H >= 0 && -13 + B + H >= 0 && 11 + -1*B + H >= 0 && -1*A + H >= 0 && F >= 0 && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && -1 + D >= 0 && -1*C + D >= 0 && -13 + B + D >= 0 && 11 + -1*B + D >= 0 && -1*A + D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && 0 >= 1 + A && B >= 1 + H] 23. f32(A,B,C,D,E,F,G,H,I,J,K,L) -> f35(A,B,C,D,E,F,G,1 + F,I,J,K,L) [F >= 0 (?,1) && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && -1 + D >= 0 && -1*C + D >= 0 && -13 + B + D >= 0 && 11 + -1*B + D >= 0 && -1*A + D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && B >= 2 + F] 24. f19(A,B,C,D,E,F,G,H,I,J,K,L) -> f19(A,B,0,D,E,1 + F,0,H,I,J,K,L) [F >= 0 (?,1) && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && -1 + C + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && A + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && -1 + D >= 0 && -1*C + D >= 0 && -13 + B + D >= 0 && 11 + -1*B + D >= 0 && -2 + A + D >= 0 && -1*A + D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && A + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 11 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -13 + A + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && B >= 1 + F && C = 0] 25. f19(A,B,C,D,E,F,G,H,I,J,K,L) -> f32(A,B,C,D,E,0,G,H,I,J,K,L) [F >= 0 (?,1) && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && -1 + C + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && A + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && -1 + D >= 0 && -1*C + D >= 0 && -13 + B + D >= 0 && 11 + -1*B + D >= 0 && -2 + A + D >= 0 && -1*A + D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && A + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 11 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -13 + A + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && F >= B] 26. f22(A,B,C,D,E,F,G,H,I,J,K,L) -> f19(A,B,0,D,E,1 + F,0,H,I,J,K,L) [11 + -1*F >= 0 (?,1) && 10 + D + -1*F >= 0 && 12 + -1*D + -1*F >= 0 && 21 + C + -1*F >= 0 && 12 + -1*C + -1*F >= 0 && -1 + B + -1*F >= 0 && 23 + -1*B + -1*F >= 0 && 10 + A + -1*F >= 0 && 12 + -1*A + -1*F >= 0 && F >= 0 && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && -1 + C + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 11 + C + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && A + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && -1 + D >= 0 && 9 + C + D >= 0 && -1*C + D >= 0 && -13 + B + D >= 0 && 11 + -1*B + D >= 0 && -2 + A + D >= 0 && -1*A + D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && A + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 10 + C >= 0 && -2 + B + C >= 0 && 22 + -1*B + C >= 0 && 9 + A + C >= 0 && 11 + -1*A + C >= 0 && 12 + -1*B >= 0 && 11 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -13 + A + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && 0 >= 1 + M] 27. f22(A,B,C,D,E,F,G,H,I,J,K,L) -> f19(A,B,0,D,E,1 + F,0,H,I,J,K,L) [11 + -1*F >= 0 (?,1) && 10 + D + -1*F >= 0 && 12 + -1*D + -1*F >= 0 && 21 + C + -1*F >= 0 && 12 + -1*C + -1*F >= 0 && -1 + B + -1*F >= 0 && 23 + -1*B + -1*F >= 0 && 10 + A + -1*F >= 0 && 12 + -1*A + -1*F >= 0 && F >= 0 && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && -1 + C + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 11 + C + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && A + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && -1 + D >= 0 && 9 + C + D >= 0 && -1*C + D >= 0 && -13 + B + D >= 0 && 11 + -1*B + D >= 0 && -2 + A + D >= 0 && -1*A + D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && A + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 10 + C >= 0 && -2 + B + C >= 0 && 22 + -1*B + C >= 0 && 9 + A + C >= 0 && 11 + -1*A + C >= 0 && 12 + -1*B >= 0 && 11 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -13 + A + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && M >= 0] 28. f22(A,B,C,D,E,F,G,H,I,J,K,L) -> f19(A,B,1,D,E,1 + F,1,H,I,J,K,L) [11 + -1*F >= 0 (?,1) && 10 + D + -1*F >= 0 && 12 + -1*D + -1*F >= 0 && 21 + C + -1*F >= 0 && 12 + -1*C + -1*F >= 0 && -1 + B + -1*F >= 0 && 23 + -1*B + -1*F >= 0 && 10 + A + -1*F >= 0 && 12 + -1*A + -1*F >= 0 && F >= 0 && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && -1 + C + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 11 + C + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && A + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && -1 + D >= 0 && 9 + C + D >= 0 && -1*C + D >= 0 && -13 + B + D >= 0 && 11 + -1*B + D >= 0 && -2 + A + D >= 0 && -1*A + D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && A + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 10 + C >= 0 && -2 + B + C >= 0 && 22 + -1*B + C >= 0 && 9 + A + C >= 0 && 11 + -1*A + C >= 0 && 12 + -1*B >= 0 && 11 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -13 + A + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && M >= 0 && B >= 1 + N] 29. f19(A,B,C,D,E,F,G,H,I,J,K,L) -> f22(A,B,C,D,E,F,G,H,I,J,K,L) [F >= 0 (?,1) && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && -1 + C + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && A + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && -1 + D >= 0 && -1*C + D >= 0 && -13 + B + D >= 0 && 11 + -1*B + D >= 0 && -2 + A + D >= 0 && -1*A + D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && A + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 11 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -13 + A + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && C >= 1 && B >= 1 + F] 30. f13(A,B,C,D,E,F,G,H,I,J,K,L) -> f19(A,B,C,D,E,0,G,H,I,J,K,L) [F >= 0 (?,1) && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && -1 + C + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && C + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && A + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && -1 + D >= 0 && -2 + C + D >= 0 && -1*C + D >= 0 && -13 + B + D >= 0 && 11 + -1*B + D >= 0 && -2 + A + D >= 0 && -1*A + D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && A + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && -1 + C >= 0 && -13 + B + C >= 0 && 11 + -1*B + C >= 0 && -2 + A + C >= 0 && -1*A + C >= 0 && 12 + -1*B >= 0 && 11 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -13 + A + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && F >= B] 31. f13(A,B,C,D,E,F,G,H,I,J,K,L) -> f13(A,B,C,D,E,1 + F,G,H,I,J,K,L) [F >= 0 (?,1) && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && -1 + C + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && C + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && A + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && -1 + D >= 0 && -2 + C + D >= 0 && -1*C + D >= 0 && -13 + B + D >= 0 && 11 + -1*B + D >= 0 && -2 + A + D >= 0 && -1*A + D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && A + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && -1 + C >= 0 && -13 + B + C >= 0 && 11 + -1*B + C >= 0 && -2 + A + C >= 0 && -1*A + C >= 0 && 12 + -1*B >= 0 && 11 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -13 + A + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && B >= 1 + F] 32. f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f13(1,12,1,1,M,0,G,H,I,J,K,L) True (1,1) Signature: {(f0,12) ;(f13,12) ;(f19,12) ;(f22,12) ;(f32,12) ;(f35,12) ;(f38,12) ;(f48,12) ;(f52,12) ;(f62,12) ;(f63,12) ;(f71,12)} Flow Graph: [0->{},1->{},2->{},3->{},4->{0,1,2},5->{0,1,2},6->{6,7,8,9,14},7->{},8->{3,4,5},9->{3,4,5},10->{6,7,8,9 ,14},11->{6,7,8,9,14},12->{6,7,8,9,14},13->{6,7,8,9,14},14->{10,11,12,13},15->{6,7,8,9,14},16->{15,23} ,17->{16,20,21,22},18->{16,20,21,22},19->{16,20,21,22},20->{16,20,21,22},21->{17,18,19},22->{17,18,19} ,23->{16,20,21,22},24->{24,25,29},25->{15,23},26->{24,25,29},27->{24,25,29},28->{24,25,29},29->{26,27,28} ,30->{24,25,29},31->{30,31},32->{30,31}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(6,14) ,(10,14) ,(11,14) ,(12,6) ,(13,6) ,(15,6) ,(15,7) ,(15,8) ,(15,9) ,(17,21) ,(17,22) ,(18,20) ,(18,22) ,(19,20) ,(19,22) ,(20,21) ,(20,22) ,(23,16) ,(24,29) ,(25,15) ,(26,29) ,(27,29) ,(28,24) ,(30,24) ,(30,25) ,(32,30)] * Step 2: FromIts YES + Considered Problem: Rules: 0. f63(A,B,C,D,E,F,G,H,I,J,K,L) -> f71(A,B,C,0,E,F,G,H,I,J,K,1) [-11 + F >= 0 (?,1) && -1 + D + F >= 0 && -10 + -1*D + F >= 0 && -10 + -1*C + F >= 0 && -23 + B + F >= 0 && 1 + -1*B + F >= 0 && -10 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && D = 0] 1. f63(A,B,C,D,E,F,G,H,I,J,K,L) -> f71(A,B,C,D,E,F,G,H,I,J,K,0) [-11 + F >= 0 (?,1) && -1 + D + F >= 0 && -10 + -1*D + F >= 0 && -10 + -1*C + F >= 0 && -23 + B + F >= 0 && 1 + -1*B + F >= 0 && -10 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && D >= 1] 2. f63(A,B,C,D,E,F,G,H,I,J,K,L) -> f71(A,B,C,D,E,F,G,H,I,J,K,0) [-11 + F >= 0 (?,1) && -1 + D + F >= 0 && -10 + -1*D + F >= 0 && -10 + -1*C + F >= 0 && -23 + B + F >= 0 && 1 + -1*B + F >= 0 && -10 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && 0 >= 1 + D] 3. f62(A,B,C,D,E,F,G,H,I,J,K,L) -> f71(0,B,C,D,E,F,G,H,I,J,K,1) [-11 + F >= 0 (?,1) && -1 + D + F >= 0 && -10 + -1*D + F >= 0 && -10 + -1*C + F >= 0 && -23 + B + F >= 0 && 1 + -1*B + F >= 0 && -10 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && A = 0] 4. f62(A,B,C,D,E,F,G,H,I,J,K,L) -> f63(A,B,C,D,E,F,G,H,I,J,K,L) [-11 + F >= 0 (?,1) && -1 + D + F >= 0 && -10 + -1*D + F >= 0 && -10 + -1*C + F >= 0 && -23 + B + F >= 0 && 1 + -1*B + F >= 0 && -10 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && A >= 1] 5. f62(A,B,C,D,E,F,G,H,I,J,K,L) -> f63(A,B,C,D,E,F,G,H,I,J,K,L) [-11 + F >= 0 (?,1) && -1 + D + F >= 0 && -10 + -1*D + F >= 0 && -10 + -1*C + F >= 0 && -23 + B + F >= 0 && 1 + -1*B + F >= 0 && -10 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && 0 >= 1 + A] 6. f48(A,B,C,D,E,F,G,H,I,J,K,L) -> f48(A,B,C,0,E,1 + F,G,H,I,M,0,L) [F >= 0 (?,1) && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && B >= 2 + F && D = 0] 7. f48(A,B,C,D,E,F,G,H,I,J,K,L) -> f71(A,B,0,D,E,F,G,H,I,J,K,1) [F >= 0 (?,1) && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && 1 + F >= B && C = 0] 8. f48(A,B,C,D,E,F,G,H,I,J,K,L) -> f62(A,B,C,D,E,F,G,H,I,J,K,L) [F >= 0 (?,1) && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && C >= 1 && 1 + F >= B] 9. f48(A,B,C,D,E,F,G,H,I,J,K,L) -> f62(A,B,C,D,E,F,G,H,I,J,K,L) [F >= 0 (?,1) && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && 0 >= 1 + C && 1 + F >= B] 10. f52(A,B,C,D,E,F,G,H,I,J,K,L) -> f48(A,B,C,0,E,1 + F,G,H,I,J,0,L) [10 + -1*F >= 0 (?,1) && 19 + D + -1*F >= 0 && 11 + -1*D + -1*F >= 0 && 11 + -1*C + -1*F >= 0 && -2 + B + -1*F >= 0 && 22 + -1*B + -1*F >= 0 && 11 + -1*A + -1*F >= 0 && F >= 0 && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && 9 + D >= 0 && 10 + -1*C + D >= 0 && -3 + B + D >= 0 && 21 + -1*B + D >= 0 && 10 + -1*A + D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0] 11. f52(A,B,C,D,E,F,G,H,I,J,K,L) -> f48(A,B,C,0,E,1 + F,G,H,I,0,0,L) [10 + -1*F >= 0 (?,1) && 19 + D + -1*F >= 0 && 11 + -1*D + -1*F >= 0 && 11 + -1*C + -1*F >= 0 && -2 + B + -1*F >= 0 && 22 + -1*B + -1*F >= 0 && 11 + -1*A + -1*F >= 0 && F >= 0 && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && 9 + D >= 0 && 10 + -1*C + D >= 0 && -3 + B + D >= 0 && 21 + -1*B + D >= 0 && 10 + -1*A + D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && J = 0] 12. f52(A,B,C,D,E,F,G,H,I,J,K,L) -> f48(A,B,C,1,E,1 + F,G,H,I,J,1,L) [10 + -1*F >= 0 (?,1) && 19 + D + -1*F >= 0 && 11 + -1*D + -1*F >= 0 && 11 + -1*C + -1*F >= 0 && -2 + B + -1*F >= 0 && 22 + -1*B + -1*F >= 0 && 11 + -1*A + -1*F >= 0 && F >= 0 && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && 9 + D >= 0 && 10 + -1*C + D >= 0 && -3 + B + D >= 0 && 21 + -1*B + D >= 0 && 10 + -1*A + D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && J >= 1] 13. f52(A,B,C,D,E,F,G,H,I,J,K,L) -> f48(A,B,C,1,E,1 + F,G,H,I,J,1,L) [10 + -1*F >= 0 (?,1) && 19 + D + -1*F >= 0 && 11 + -1*D + -1*F >= 0 && 11 + -1*C + -1*F >= 0 && -2 + B + -1*F >= 0 && 22 + -1*B + -1*F >= 0 && 11 + -1*A + -1*F >= 0 && F >= 0 && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && 9 + D >= 0 && 10 + -1*C + D >= 0 && -3 + B + D >= 0 && 21 + -1*B + D >= 0 && 10 + -1*A + D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && 0 >= 1 + J] 14. f48(A,B,C,D,E,F,G,H,I,J,K,L) -> f52(A,B,C,D,E,F,G,H,I,M,K,L) [F >= 0 (?,1) && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && D >= 1 && B >= 2 + F] 15. f32(A,B,C,D,E,F,G,H,I,J,K,L) -> f48(A,B,C,D,E,0,G,H,I,J,K,L) [F >= 0 (?,1) && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && -1 + D >= 0 && -1*C + D >= 0 && -13 + B + D >= 0 && 11 + -1*B + D >= 0 && -1*A + D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && 1 + F >= B] 16. f35(A,B,C,D,E,F,G,H,I,J,K,L) -> f32(A,B,C,D,E,1 + F,G,H,I,J,K,L) [-1 + H >= 0 (?,1) && -1 + F + H >= 0 && -1 + -1*F + H >= 0 && -2 + D + H >= 0 && -1*D + H >= 0 && -1*C + H >= 0 && -13 + B + H >= 0 && 11 + -1*B + H >= 0 && -1*A + H >= 0 && F >= 0 && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && -1 + D >= 0 && -1*C + D >= 0 && -13 + B + D >= 0 && 11 + -1*B + D >= 0 && -1*A + D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && H >= B] 17. f38(A,B,C,D,E,F,G,H,I,J,K,L) -> f35(0,B,C,D,E,F,G,1 + H,0,J,K,L) [11 + -1*H >= 0 (?,1) && 11 + F + -1*H >= 0 && 21 + -1*F + -1*H >= 0 && 10 + D + -1*H >= 0 && 12 + -1*D + -1*H >= 0 && 12 + -1*C + -1*H >= 0 && -1 + B + -1*H >= 0 && 23 + -1*B + -1*H >= 0 && 12 + -1*A + -1*H >= 0 && -1 + H >= 0 && -1 + F + H >= 0 && -1 + -1*F + H >= 0 && -2 + D + H >= 0 && -1*D + H >= 0 && -1*C + H >= 0 && -13 + B + H >= 0 && 11 + -1*B + H >= 0 && -1*A + H >= 0 && 10 + -1*F >= 0 && 9 + D + -1*F >= 0 && 11 + -1*D + -1*F >= 0 && 11 + -1*C + -1*F >= 0 && -2 + B + -1*F >= 0 && 22 + -1*B + -1*F >= 0 && 11 + -1*A + -1*F >= 0 && F >= 0 && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && -1 + D >= 0 && -1*C + D >= 0 && -13 + B + D >= 0 && 11 + -1*B + D >= 0 && -1*A + D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0] 18. f38(A,B,C,D,E,F,G,H,I,J,K,L) -> f35(1,B,C,D,E,F,G,1 + H,1,J,K,L) [11 + -1*H >= 0 (?,1) && 11 + F + -1*H >= 0 && 21 + -1*F + -1*H >= 0 && 10 + D + -1*H >= 0 && 12 + -1*D + -1*H >= 0 && 12 + -1*C + -1*H >= 0 && -1 + B + -1*H >= 0 && 23 + -1*B + -1*H >= 0 && 12 + -1*A + -1*H >= 0 && -1 + H >= 0 && -1 + F + H >= 0 && -1 + -1*F + H >= 0 && -2 + D + H >= 0 && -1*D + H >= 0 && -1*C + H >= 0 && -13 + B + H >= 0 && 11 + -1*B + H >= 0 && -1*A + H >= 0 && 10 + -1*F >= 0 && 9 + D + -1*F >= 0 && 11 + -1*D + -1*F >= 0 && 11 + -1*C + -1*F >= 0 && -2 + B + -1*F >= 0 && 22 + -1*B + -1*F >= 0 && 11 + -1*A + -1*F >= 0 && F >= 0 && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && -1 + D >= 0 && -1*C + D >= 0 && -13 + B + D >= 0 && 11 + -1*B + D >= 0 && -1*A + D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0] 19. f38(A,B,C,D,E,F,G,H,I,J,K,L) -> f35(1,B,C,D,E,F,G,1 + H,1,J,K,L) [11 + -1*H >= 0 (?,1) && 11 + F + -1*H >= 0 && 21 + -1*F + -1*H >= 0 && 10 + D + -1*H >= 0 && 12 + -1*D + -1*H >= 0 && 12 + -1*C + -1*H >= 0 && -1 + B + -1*H >= 0 && 23 + -1*B + -1*H >= 0 && 12 + -1*A + -1*H >= 0 && -1 + H >= 0 && -1 + F + H >= 0 && -1 + -1*F + H >= 0 && -2 + D + H >= 0 && -1*D + H >= 0 && -1*C + H >= 0 && -13 + B + H >= 0 && 11 + -1*B + H >= 0 && -1*A + H >= 0 && 10 + -1*F >= 0 && 9 + D + -1*F >= 0 && 11 + -1*D + -1*F >= 0 && 11 + -1*C + -1*F >= 0 && -2 + B + -1*F >= 0 && 22 + -1*B + -1*F >= 0 && 11 + -1*A + -1*F >= 0 && F >= 0 && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && -1 + D >= 0 && -1*C + D >= 0 && -13 + B + D >= 0 && 11 + -1*B + D >= 0 && -1*A + D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && M >= 1 + N] 20. f35(A,B,C,D,E,F,G,H,I,J,K,L) -> f35(0,B,C,D,E,F,G,1 + H,0,J,K,L) [-1 + H >= 0 (?,1) && -1 + F + H >= 0 && -1 + -1*F + H >= 0 && -2 + D + H >= 0 && -1*D + H >= 0 && -1*C + H >= 0 && -13 + B + H >= 0 && 11 + -1*B + H >= 0 && -1*A + H >= 0 && F >= 0 && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && -1 + D >= 0 && -1*C + D >= 0 && -13 + B + D >= 0 && 11 + -1*B + D >= 0 && -1*A + D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && B >= 1 + H && A = 0] 21. f35(A,B,C,D,E,F,G,H,I,J,K,L) -> f38(A,B,C,D,E,F,G,H,I,J,K,L) [-1 + H >= 0 (?,1) && -1 + F + H >= 0 && -1 + -1*F + H >= 0 && -2 + D + H >= 0 && -1*D + H >= 0 && -1*C + H >= 0 && -13 + B + H >= 0 && 11 + -1*B + H >= 0 && -1*A + H >= 0 && F >= 0 && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && -1 + D >= 0 && -1*C + D >= 0 && -13 + B + D >= 0 && 11 + -1*B + D >= 0 && -1*A + D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && A >= 1 && B >= 1 + H] 22. f35(A,B,C,D,E,F,G,H,I,J,K,L) -> f38(A,B,C,D,E,F,G,H,I,J,K,L) [-1 + H >= 0 (?,1) && -1 + F + H >= 0 && -1 + -1*F + H >= 0 && -2 + D + H >= 0 && -1*D + H >= 0 && -1*C + H >= 0 && -13 + B + H >= 0 && 11 + -1*B + H >= 0 && -1*A + H >= 0 && F >= 0 && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && -1 + D >= 0 && -1*C + D >= 0 && -13 + B + D >= 0 && 11 + -1*B + D >= 0 && -1*A + D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && 0 >= 1 + A && B >= 1 + H] 23. f32(A,B,C,D,E,F,G,H,I,J,K,L) -> f35(A,B,C,D,E,F,G,1 + F,I,J,K,L) [F >= 0 (?,1) && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && -1 + D >= 0 && -1*C + D >= 0 && -13 + B + D >= 0 && 11 + -1*B + D >= 0 && -1*A + D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && B >= 2 + F] 24. f19(A,B,C,D,E,F,G,H,I,J,K,L) -> f19(A,B,0,D,E,1 + F,0,H,I,J,K,L) [F >= 0 (?,1) && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && -1 + C + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && A + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && -1 + D >= 0 && -1*C + D >= 0 && -13 + B + D >= 0 && 11 + -1*B + D >= 0 && -2 + A + D >= 0 && -1*A + D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && A + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 11 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -13 + A + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && B >= 1 + F && C = 0] 25. f19(A,B,C,D,E,F,G,H,I,J,K,L) -> f32(A,B,C,D,E,0,G,H,I,J,K,L) [F >= 0 (?,1) && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && -1 + C + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && A + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && -1 + D >= 0 && -1*C + D >= 0 && -13 + B + D >= 0 && 11 + -1*B + D >= 0 && -2 + A + D >= 0 && -1*A + D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && A + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 11 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -13 + A + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && F >= B] 26. f22(A,B,C,D,E,F,G,H,I,J,K,L) -> f19(A,B,0,D,E,1 + F,0,H,I,J,K,L) [11 + -1*F >= 0 (?,1) && 10 + D + -1*F >= 0 && 12 + -1*D + -1*F >= 0 && 21 + C + -1*F >= 0 && 12 + -1*C + -1*F >= 0 && -1 + B + -1*F >= 0 && 23 + -1*B + -1*F >= 0 && 10 + A + -1*F >= 0 && 12 + -1*A + -1*F >= 0 && F >= 0 && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && -1 + C + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 11 + C + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && A + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && -1 + D >= 0 && 9 + C + D >= 0 && -1*C + D >= 0 && -13 + B + D >= 0 && 11 + -1*B + D >= 0 && -2 + A + D >= 0 && -1*A + D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && A + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 10 + C >= 0 && -2 + B + C >= 0 && 22 + -1*B + C >= 0 && 9 + A + C >= 0 && 11 + -1*A + C >= 0 && 12 + -1*B >= 0 && 11 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -13 + A + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && 0 >= 1 + M] 27. f22(A,B,C,D,E,F,G,H,I,J,K,L) -> f19(A,B,0,D,E,1 + F,0,H,I,J,K,L) [11 + -1*F >= 0 (?,1) && 10 + D + -1*F >= 0 && 12 + -1*D + -1*F >= 0 && 21 + C + -1*F >= 0 && 12 + -1*C + -1*F >= 0 && -1 + B + -1*F >= 0 && 23 + -1*B + -1*F >= 0 && 10 + A + -1*F >= 0 && 12 + -1*A + -1*F >= 0 && F >= 0 && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && -1 + C + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 11 + C + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && A + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && -1 + D >= 0 && 9 + C + D >= 0 && -1*C + D >= 0 && -13 + B + D >= 0 && 11 + -1*B + D >= 0 && -2 + A + D >= 0 && -1*A + D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && A + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 10 + C >= 0 && -2 + B + C >= 0 && 22 + -1*B + C >= 0 && 9 + A + C >= 0 && 11 + -1*A + C >= 0 && 12 + -1*B >= 0 && 11 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -13 + A + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && M >= 0] 28. f22(A,B,C,D,E,F,G,H,I,J,K,L) -> f19(A,B,1,D,E,1 + F,1,H,I,J,K,L) [11 + -1*F >= 0 (?,1) && 10 + D + -1*F >= 0 && 12 + -1*D + -1*F >= 0 && 21 + C + -1*F >= 0 && 12 + -1*C + -1*F >= 0 && -1 + B + -1*F >= 0 && 23 + -1*B + -1*F >= 0 && 10 + A + -1*F >= 0 && 12 + -1*A + -1*F >= 0 && F >= 0 && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && -1 + C + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 11 + C + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && A + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && -1 + D >= 0 && 9 + C + D >= 0 && -1*C + D >= 0 && -13 + B + D >= 0 && 11 + -1*B + D >= 0 && -2 + A + D >= 0 && -1*A + D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && A + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 10 + C >= 0 && -2 + B + C >= 0 && 22 + -1*B + C >= 0 && 9 + A + C >= 0 && 11 + -1*A + C >= 0 && 12 + -1*B >= 0 && 11 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -13 + A + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && M >= 0 && B >= 1 + N] 29. f19(A,B,C,D,E,F,G,H,I,J,K,L) -> f22(A,B,C,D,E,F,G,H,I,J,K,L) [F >= 0 (?,1) && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && -1 + C + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && A + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && -1 + D >= 0 && -1*C + D >= 0 && -13 + B + D >= 0 && 11 + -1*B + D >= 0 && -2 + A + D >= 0 && -1*A + D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && A + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 11 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -13 + A + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && C >= 1 && B >= 1 + F] 30. f13(A,B,C,D,E,F,G,H,I,J,K,L) -> f19(A,B,C,D,E,0,G,H,I,J,K,L) [F >= 0 (?,1) && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && -1 + C + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && C + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && A + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && -1 + D >= 0 && -2 + C + D >= 0 && -1*C + D >= 0 && -13 + B + D >= 0 && 11 + -1*B + D >= 0 && -2 + A + D >= 0 && -1*A + D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && A + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && -1 + C >= 0 && -13 + B + C >= 0 && 11 + -1*B + C >= 0 && -2 + A + C >= 0 && -1*A + C >= 0 && 12 + -1*B >= 0 && 11 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -13 + A + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && F >= B] 31. f13(A,B,C,D,E,F,G,H,I,J,K,L) -> f13(A,B,C,D,E,1 + F,G,H,I,J,K,L) [F >= 0 (?,1) && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && -1 + C + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && C + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && A + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && -1 + D >= 0 && -2 + C + D >= 0 && -1*C + D >= 0 && -13 + B + D >= 0 && 11 + -1*B + D >= 0 && -2 + A + D >= 0 && -1*A + D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && A + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && -1 + C >= 0 && -13 + B + C >= 0 && 11 + -1*B + C >= 0 && -2 + A + C >= 0 && -1*A + C >= 0 && 12 + -1*B >= 0 && 11 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -13 + A + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && B >= 1 + F] 32. f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f13(1,12,1,1,M,0,G,H,I,J,K,L) True (1,1) Signature: {(f0,12) ;(f13,12) ;(f19,12) ;(f22,12) ;(f32,12) ;(f35,12) ;(f38,12) ;(f48,12) ;(f52,12) ;(f62,12) ;(f63,12) ;(f71,12)} Flow Graph: [0->{},1->{},2->{},3->{},4->{0,1,2},5->{0,1,2},6->{6,7,8,9},7->{},8->{3,4,5},9->{3,4,5},10->{6,7,8,9} ,11->{6,7,8,9},12->{7,8,9,14},13->{7,8,9,14},14->{10,11,12,13},15->{14},16->{15,23},17->{16,20},18->{16,21} ,19->{16,21},20->{16,20},21->{17,18,19},22->{17,18,19},23->{20,21,22},24->{24,25},25->{23},26->{24,25} ,27->{24,25},28->{25,29},29->{26,27,28},30->{29},31->{30,31},32->{31}] + Applied Processor: FromIts + Details: () * Step 3: Decompose YES + Considered Problem: Rules: f63(A,B,C,D,E,F,G,H,I,J,K,L) -> f71(A,B,C,0,E,F,G,H,I,J,K,1) [-11 + F >= 0 && -1 + D + F >= 0 && -10 + -1*D + F >= 0 && -10 + -1*C + F >= 0 && -23 + B + F >= 0 && 1 + -1*B + F >= 0 && -10 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && D = 0] f63(A,B,C,D,E,F,G,H,I,J,K,L) -> f71(A,B,C,D,E,F,G,H,I,J,K,0) [-11 + F >= 0 && -1 + D + F >= 0 && -10 + -1*D + F >= 0 && -10 + -1*C + F >= 0 && -23 + B + F >= 0 && 1 + -1*B + F >= 0 && -10 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && D >= 1] f63(A,B,C,D,E,F,G,H,I,J,K,L) -> f71(A,B,C,D,E,F,G,H,I,J,K,0) [-11 + F >= 0 && -1 + D + F >= 0 && -10 + -1*D + F >= 0 && -10 + -1*C + F >= 0 && -23 + B + F >= 0 && 1 + -1*B + F >= 0 && -10 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && 0 >= 1 + D] f62(A,B,C,D,E,F,G,H,I,J,K,L) -> f71(0,B,C,D,E,F,G,H,I,J,K,1) [-11 + F >= 0 && -1 + D + F >= 0 && -10 + -1*D + F >= 0 && -10 + -1*C + F >= 0 && -23 + B + F >= 0 && 1 + -1*B + F >= 0 && -10 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && A = 0] f62(A,B,C,D,E,F,G,H,I,J,K,L) -> f63(A,B,C,D,E,F,G,H,I,J,K,L) [-11 + F >= 0 && -1 + D + F >= 0 && -10 + -1*D + F >= 0 && -10 + -1*C + F >= 0 && -23 + B + F >= 0 && 1 + -1*B + F >= 0 && -10 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && A >= 1] f62(A,B,C,D,E,F,G,H,I,J,K,L) -> f63(A,B,C,D,E,F,G,H,I,J,K,L) [-11 + F >= 0 && -1 + D + F >= 0 && -10 + -1*D + F >= 0 && -10 + -1*C + F >= 0 && -23 + B + F >= 0 && 1 + -1*B + F >= 0 && -10 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && 0 >= 1 + A] f48(A,B,C,D,E,F,G,H,I,J,K,L) -> f48(A,B,C,0,E,1 + F,G,H,I,M,0,L) [F >= 0 && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && B >= 2 + F && D = 0] f48(A,B,C,D,E,F,G,H,I,J,K,L) -> f71(A,B,0,D,E,F,G,H,I,J,K,1) [F >= 0 && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && 1 + F >= B && C = 0] f48(A,B,C,D,E,F,G,H,I,J,K,L) -> f62(A,B,C,D,E,F,G,H,I,J,K,L) [F >= 0 && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && C >= 1 && 1 + F >= B] f48(A,B,C,D,E,F,G,H,I,J,K,L) -> f62(A,B,C,D,E,F,G,H,I,J,K,L) [F >= 0 && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && 0 >= 1 + C && 1 + F >= B] f52(A,B,C,D,E,F,G,H,I,J,K,L) -> f48(A,B,C,0,E,1 + F,G,H,I,J,0,L) [10 + -1*F >= 0 && 19 + D + -1*F >= 0 && 11 + -1*D + -1*F >= 0 && 11 + -1*C + -1*F >= 0 && -2 + B + -1*F >= 0 && 22 + -1*B + -1*F >= 0 && 11 + -1*A + -1*F >= 0 && F >= 0 && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && 9 + D >= 0 && 10 + -1*C + D >= 0 && -3 + B + D >= 0 && 21 + -1*B + D >= 0 && 10 + -1*A + D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0] f52(A,B,C,D,E,F,G,H,I,J,K,L) -> f48(A,B,C,0,E,1 + F,G,H,I,0,0,L) [10 + -1*F >= 0 && 19 + D + -1*F >= 0 && 11 + -1*D + -1*F >= 0 && 11 + -1*C + -1*F >= 0 && -2 + B + -1*F >= 0 && 22 + -1*B + -1*F >= 0 && 11 + -1*A + -1*F >= 0 && F >= 0 && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && 9 + D >= 0 && 10 + -1*C + D >= 0 && -3 + B + D >= 0 && 21 + -1*B + D >= 0 && 10 + -1*A + D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && J = 0] f52(A,B,C,D,E,F,G,H,I,J,K,L) -> f48(A,B,C,1,E,1 + F,G,H,I,J,1,L) [10 + -1*F >= 0 && 19 + D + -1*F >= 0 && 11 + -1*D + -1*F >= 0 && 11 + -1*C + -1*F >= 0 && -2 + B + -1*F >= 0 && 22 + -1*B + -1*F >= 0 && 11 + -1*A + -1*F >= 0 && F >= 0 && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && 9 + D >= 0 && 10 + -1*C + D >= 0 && -3 + B + D >= 0 && 21 + -1*B + D >= 0 && 10 + -1*A + D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && J >= 1] f52(A,B,C,D,E,F,G,H,I,J,K,L) -> f48(A,B,C,1,E,1 + F,G,H,I,J,1,L) [10 + -1*F >= 0 && 19 + D + -1*F >= 0 && 11 + -1*D + -1*F >= 0 && 11 + -1*C + -1*F >= 0 && -2 + B + -1*F >= 0 && 22 + -1*B + -1*F >= 0 && 11 + -1*A + -1*F >= 0 && F >= 0 && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && 9 + D >= 0 && 10 + -1*C + D >= 0 && -3 + B + D >= 0 && 21 + -1*B + D >= 0 && 10 + -1*A + D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && 0 >= 1 + J] f48(A,B,C,D,E,F,G,H,I,J,K,L) -> f52(A,B,C,D,E,F,G,H,I,M,K,L) [F >= 0 && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && D >= 1 && B >= 2 + F] f32(A,B,C,D,E,F,G,H,I,J,K,L) -> f48(A,B,C,D,E,0,G,H,I,J,K,L) [F >= 0 && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && -1 + D >= 0 && -1*C + D >= 0 && -13 + B + D >= 0 && 11 + -1*B + D >= 0 && -1*A + D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && 1 + F >= B] f35(A,B,C,D,E,F,G,H,I,J,K,L) -> f32(A,B,C,D,E,1 + F,G,H,I,J,K,L) [-1 + H >= 0 && -1 + F + H >= 0 && -1 + -1*F + H >= 0 && -2 + D + H >= 0 && -1*D + H >= 0 && -1*C + H >= 0 && -13 + B + H >= 0 && 11 + -1*B + H >= 0 && -1*A + H >= 0 && F >= 0 && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && -1 + D >= 0 && -1*C + D >= 0 && -13 + B + D >= 0 && 11 + -1*B + D >= 0 && -1*A + D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && H >= B] f38(A,B,C,D,E,F,G,H,I,J,K,L) -> f35(0,B,C,D,E,F,G,1 + H,0,J,K,L) [11 + -1*H >= 0 && 11 + F + -1*H >= 0 && 21 + -1*F + -1*H >= 0 && 10 + D + -1*H >= 0 && 12 + -1*D + -1*H >= 0 && 12 + -1*C + -1*H >= 0 && -1 + B + -1*H >= 0 && 23 + -1*B + -1*H >= 0 && 12 + -1*A + -1*H >= 0 && -1 + H >= 0 && -1 + F + H >= 0 && -1 + -1*F + H >= 0 && -2 + D + H >= 0 && -1*D + H >= 0 && -1*C + H >= 0 && -13 + B + H >= 0 && 11 + -1*B + H >= 0 && -1*A + H >= 0 && 10 + -1*F >= 0 && 9 + D + -1*F >= 0 && 11 + -1*D + -1*F >= 0 && 11 + -1*C + -1*F >= 0 && -2 + B + -1*F >= 0 && 22 + -1*B + -1*F >= 0 && 11 + -1*A + -1*F >= 0 && F >= 0 && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && -1 + D >= 0 && -1*C + D >= 0 && -13 + B + D >= 0 && 11 + -1*B + D >= 0 && -1*A + D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0] f38(A,B,C,D,E,F,G,H,I,J,K,L) -> f35(1,B,C,D,E,F,G,1 + H,1,J,K,L) [11 + -1*H >= 0 && 11 + F + -1*H >= 0 && 21 + -1*F + -1*H >= 0 && 10 + D + -1*H >= 0 && 12 + -1*D + -1*H >= 0 && 12 + -1*C + -1*H >= 0 && -1 + B + -1*H >= 0 && 23 + -1*B + -1*H >= 0 && 12 + -1*A + -1*H >= 0 && -1 + H >= 0 && -1 + F + H >= 0 && -1 + -1*F + H >= 0 && -2 + D + H >= 0 && -1*D + H >= 0 && -1*C + H >= 0 && -13 + B + H >= 0 && 11 + -1*B + H >= 0 && -1*A + H >= 0 && 10 + -1*F >= 0 && 9 + D + -1*F >= 0 && 11 + -1*D + -1*F >= 0 && 11 + -1*C + -1*F >= 0 && -2 + B + -1*F >= 0 && 22 + -1*B + -1*F >= 0 && 11 + -1*A + -1*F >= 0 && F >= 0 && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && -1 + D >= 0 && -1*C + D >= 0 && -13 + B + D >= 0 && 11 + -1*B + D >= 0 && -1*A + D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0] f38(A,B,C,D,E,F,G,H,I,J,K,L) -> f35(1,B,C,D,E,F,G,1 + H,1,J,K,L) [11 + -1*H >= 0 && 11 + F + -1*H >= 0 && 21 + -1*F + -1*H >= 0 && 10 + D + -1*H >= 0 && 12 + -1*D + -1*H >= 0 && 12 + -1*C + -1*H >= 0 && -1 + B + -1*H >= 0 && 23 + -1*B + -1*H >= 0 && 12 + -1*A + -1*H >= 0 && -1 + H >= 0 && -1 + F + H >= 0 && -1 + -1*F + H >= 0 && -2 + D + H >= 0 && -1*D + H >= 0 && -1*C + H >= 0 && -13 + B + H >= 0 && 11 + -1*B + H >= 0 && -1*A + H >= 0 && 10 + -1*F >= 0 && 9 + D + -1*F >= 0 && 11 + -1*D + -1*F >= 0 && 11 + -1*C + -1*F >= 0 && -2 + B + -1*F >= 0 && 22 + -1*B + -1*F >= 0 && 11 + -1*A + -1*F >= 0 && F >= 0 && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && -1 + D >= 0 && -1*C + D >= 0 && -13 + B + D >= 0 && 11 + -1*B + D >= 0 && -1*A + D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && M >= 1 + N] f35(A,B,C,D,E,F,G,H,I,J,K,L) -> f35(0,B,C,D,E,F,G,1 + H,0,J,K,L) [-1 + H >= 0 && -1 + F + H >= 0 && -1 + -1*F + H >= 0 && -2 + D + H >= 0 && -1*D + H >= 0 && -1*C + H >= 0 && -13 + B + H >= 0 && 11 + -1*B + H >= 0 && -1*A + H >= 0 && F >= 0 && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && -1 + D >= 0 && -1*C + D >= 0 && -13 + B + D >= 0 && 11 + -1*B + D >= 0 && -1*A + D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && B >= 1 + H && A = 0] f35(A,B,C,D,E,F,G,H,I,J,K,L) -> f38(A,B,C,D,E,F,G,H,I,J,K,L) [-1 + H >= 0 && -1 + F + H >= 0 && -1 + -1*F + H >= 0 && -2 + D + H >= 0 && -1*D + H >= 0 && -1*C + H >= 0 && -13 + B + H >= 0 && 11 + -1*B + H >= 0 && -1*A + H >= 0 && F >= 0 && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && -1 + D >= 0 && -1*C + D >= 0 && -13 + B + D >= 0 && 11 + -1*B + D >= 0 && -1*A + D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && A >= 1 && B >= 1 + H] f35(A,B,C,D,E,F,G,H,I,J,K,L) -> f38(A,B,C,D,E,F,G,H,I,J,K,L) [-1 + H >= 0 && -1 + F + H >= 0 && -1 + -1*F + H >= 0 && -2 + D + H >= 0 && -1*D + H >= 0 && -1*C + H >= 0 && -13 + B + H >= 0 && 11 + -1*B + H >= 0 && -1*A + H >= 0 && F >= 0 && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && -1 + D >= 0 && -1*C + D >= 0 && -13 + B + D >= 0 && 11 + -1*B + D >= 0 && -1*A + D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && 0 >= 1 + A && B >= 1 + H] f32(A,B,C,D,E,F,G,H,I,J,K,L) -> f35(A,B,C,D,E,F,G,1 + F,I,J,K,L) [F >= 0 && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && -1 + D >= 0 && -1*C + D >= 0 && -13 + B + D >= 0 && 11 + -1*B + D >= 0 && -1*A + D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && B >= 2 + F] f19(A,B,C,D,E,F,G,H,I,J,K,L) -> f19(A,B,0,D,E,1 + F,0,H,I,J,K,L) [F >= 0 && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && -1 + C + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && A + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && -1 + D >= 0 && -1*C + D >= 0 && -13 + B + D >= 0 && 11 + -1*B + D >= 0 && -2 + A + D >= 0 && -1*A + D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && A + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 11 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -13 + A + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && B >= 1 + F && C = 0] f19(A,B,C,D,E,F,G,H,I,J,K,L) -> f32(A,B,C,D,E,0,G,H,I,J,K,L) [F >= 0 && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && -1 + C + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && A + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && -1 + D >= 0 && -1*C + D >= 0 && -13 + B + D >= 0 && 11 + -1*B + D >= 0 && -2 + A + D >= 0 && -1*A + D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && A + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 11 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -13 + A + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && F >= B] f22(A,B,C,D,E,F,G,H,I,J,K,L) -> f19(A,B,0,D,E,1 + F,0,H,I,J,K,L) [11 + -1*F >= 0 && 10 + D + -1*F >= 0 && 12 + -1*D + -1*F >= 0 && 21 + C + -1*F >= 0 && 12 + -1*C + -1*F >= 0 && -1 + B + -1*F >= 0 && 23 + -1*B + -1*F >= 0 && 10 + A + -1*F >= 0 && 12 + -1*A + -1*F >= 0 && F >= 0 && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && -1 + C + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 11 + C + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && A + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && -1 + D >= 0 && 9 + C + D >= 0 && -1*C + D >= 0 && -13 + B + D >= 0 && 11 + -1*B + D >= 0 && -2 + A + D >= 0 && -1*A + D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && A + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 10 + C >= 0 && -2 + B + C >= 0 && 22 + -1*B + C >= 0 && 9 + A + C >= 0 && 11 + -1*A + C >= 0 && 12 + -1*B >= 0 && 11 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -13 + A + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && 0 >= 1 + M] f22(A,B,C,D,E,F,G,H,I,J,K,L) -> f19(A,B,0,D,E,1 + F,0,H,I,J,K,L) [11 + -1*F >= 0 && 10 + D + -1*F >= 0 && 12 + -1*D + -1*F >= 0 && 21 + C + -1*F >= 0 && 12 + -1*C + -1*F >= 0 && -1 + B + -1*F >= 0 && 23 + -1*B + -1*F >= 0 && 10 + A + -1*F >= 0 && 12 + -1*A + -1*F >= 0 && F >= 0 && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && -1 + C + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 11 + C + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && A + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && -1 + D >= 0 && 9 + C + D >= 0 && -1*C + D >= 0 && -13 + B + D >= 0 && 11 + -1*B + D >= 0 && -2 + A + D >= 0 && -1*A + D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && A + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 10 + C >= 0 && -2 + B + C >= 0 && 22 + -1*B + C >= 0 && 9 + A + C >= 0 && 11 + -1*A + C >= 0 && 12 + -1*B >= 0 && 11 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -13 + A + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && M >= 0] f22(A,B,C,D,E,F,G,H,I,J,K,L) -> f19(A,B,1,D,E,1 + F,1,H,I,J,K,L) [11 + -1*F >= 0 && 10 + D + -1*F >= 0 && 12 + -1*D + -1*F >= 0 && 21 + C + -1*F >= 0 && 12 + -1*C + -1*F >= 0 && -1 + B + -1*F >= 0 && 23 + -1*B + -1*F >= 0 && 10 + A + -1*F >= 0 && 12 + -1*A + -1*F >= 0 && F >= 0 && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && -1 + C + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 11 + C + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && A + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && -1 + D >= 0 && 9 + C + D >= 0 && -1*C + D >= 0 && -13 + B + D >= 0 && 11 + -1*B + D >= 0 && -2 + A + D >= 0 && -1*A + D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && A + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 10 + C >= 0 && -2 + B + C >= 0 && 22 + -1*B + C >= 0 && 9 + A + C >= 0 && 11 + -1*A + C >= 0 && 12 + -1*B >= 0 && 11 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -13 + A + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && M >= 0 && B >= 1 + N] f19(A,B,C,D,E,F,G,H,I,J,K,L) -> f22(A,B,C,D,E,F,G,H,I,J,K,L) [F >= 0 && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && -1 + C + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && A + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && -1 + D >= 0 && -1*C + D >= 0 && -13 + B + D >= 0 && 11 + -1*B + D >= 0 && -2 + A + D >= 0 && -1*A + D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && A + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 11 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -13 + A + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && C >= 1 && B >= 1 + F] f13(A,B,C,D,E,F,G,H,I,J,K,L) -> f19(A,B,C,D,E,0,G,H,I,J,K,L) [F >= 0 && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && -1 + C + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && C + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && A + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && -1 + D >= 0 && -2 + C + D >= 0 && -1*C + D >= 0 && -13 + B + D >= 0 && 11 + -1*B + D >= 0 && -2 + A + D >= 0 && -1*A + D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && A + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && -1 + C >= 0 && -13 + B + C >= 0 && 11 + -1*B + C >= 0 && -2 + A + C >= 0 && -1*A + C >= 0 && 12 + -1*B >= 0 && 11 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -13 + A + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && F >= B] f13(A,B,C,D,E,F,G,H,I,J,K,L) -> f13(A,B,C,D,E,1 + F,G,H,I,J,K,L) [F >= 0 && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && -1 + C + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && C + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && A + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && -1 + D >= 0 && -2 + C + D >= 0 && -1*C + D >= 0 && -13 + B + D >= 0 && 11 + -1*B + D >= 0 && -2 + A + D >= 0 && -1*A + D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && A + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && -1 + C >= 0 && -13 + B + C >= 0 && 11 + -1*B + C >= 0 && -2 + A + C >= 0 && -1*A + C >= 0 && 12 + -1*B >= 0 && 11 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -13 + A + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && B >= 1 + F] f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f13(1,12,1,1,M,0,G,H,I,J,K,L) True Signature: {(f0,12) ;(f13,12) ;(f19,12) ;(f22,12) ;(f32,12) ;(f35,12) ;(f38,12) ;(f48,12) ;(f52,12) ;(f62,12) ;(f63,12) ;(f71,12)} Rule Graph: [0->{},1->{},2->{},3->{},4->{0,1,2},5->{0,1,2},6->{6,7,8,9},7->{},8->{3,4,5},9->{3,4,5},10->{6,7,8,9} ,11->{6,7,8,9},12->{7,8,9,14},13->{7,8,9,14},14->{10,11,12,13},15->{14},16->{15,23},17->{16,20},18->{16,21} ,19->{16,21},20->{16,20},21->{17,18,19},22->{17,18,19},23->{20,21,22},24->{24,25},25->{23},26->{24,25} ,27->{24,25},28->{25,29},29->{26,27,28},30->{29},31->{30,31},32->{31}] + Applied Processor: Decompose NoGreedy + 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,26,27,28,29,30,31,32] | +- p:[31] c: [31] | +- p:[28,29] c: [28,29] | +- p:[24] c: [24] | +- p:[16,17,21,18,22,23,19,20] c: [16,22,23] | | | +- p:[18,21,19] c: [18,19,21] | | | `- p:[20] c: [20] | +- p:[12,14,13] c: [12,13,14] | `- p:[6] c: [6] * Step 4: CloseWith YES + Considered Problem: (Rules: f63(A,B,C,D,E,F,G,H,I,J,K,L) -> f71(A,B,C,0,E,F,G,H,I,J,K,1) [-11 + F >= 0 && -1 + D + F >= 0 && -10 + -1*D + F >= 0 && -10 + -1*C + F >= 0 && -23 + B + F >= 0 && 1 + -1*B + F >= 0 && -10 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && D = 0] f63(A,B,C,D,E,F,G,H,I,J,K,L) -> f71(A,B,C,D,E,F,G,H,I,J,K,0) [-11 + F >= 0 && -1 + D + F >= 0 && -10 + -1*D + F >= 0 && -10 + -1*C + F >= 0 && -23 + B + F >= 0 && 1 + -1*B + F >= 0 && -10 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && D >= 1] f63(A,B,C,D,E,F,G,H,I,J,K,L) -> f71(A,B,C,D,E,F,G,H,I,J,K,0) [-11 + F >= 0 && -1 + D + F >= 0 && -10 + -1*D + F >= 0 && -10 + -1*C + F >= 0 && -23 + B + F >= 0 && 1 + -1*B + F >= 0 && -10 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && 0 >= 1 + D] f62(A,B,C,D,E,F,G,H,I,J,K,L) -> f71(0,B,C,D,E,F,G,H,I,J,K,1) [-11 + F >= 0 && -1 + D + F >= 0 && -10 + -1*D + F >= 0 && -10 + -1*C + F >= 0 && -23 + B + F >= 0 && 1 + -1*B + F >= 0 && -10 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && A = 0] f62(A,B,C,D,E,F,G,H,I,J,K,L) -> f63(A,B,C,D,E,F,G,H,I,J,K,L) [-11 + F >= 0 && -1 + D + F >= 0 && -10 + -1*D + F >= 0 && -10 + -1*C + F >= 0 && -23 + B + F >= 0 && 1 + -1*B + F >= 0 && -10 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && A >= 1] f62(A,B,C,D,E,F,G,H,I,J,K,L) -> f63(A,B,C,D,E,F,G,H,I,J,K,L) [-11 + F >= 0 && -1 + D + F >= 0 && -10 + -1*D + F >= 0 && -10 + -1*C + F >= 0 && -23 + B + F >= 0 && 1 + -1*B + F >= 0 && -10 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && 0 >= 1 + A] f48(A,B,C,D,E,F,G,H,I,J,K,L) -> f48(A,B,C,0,E,1 + F,G,H,I,M,0,L) [F >= 0 && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && B >= 2 + F && D = 0] f48(A,B,C,D,E,F,G,H,I,J,K,L) -> f71(A,B,0,D,E,F,G,H,I,J,K,1) [F >= 0 && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && 1 + F >= B && C = 0] f48(A,B,C,D,E,F,G,H,I,J,K,L) -> f62(A,B,C,D,E,F,G,H,I,J,K,L) [F >= 0 && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && C >= 1 && 1 + F >= B] f48(A,B,C,D,E,F,G,H,I,J,K,L) -> f62(A,B,C,D,E,F,G,H,I,J,K,L) [F >= 0 && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && 0 >= 1 + C && 1 + F >= B] f52(A,B,C,D,E,F,G,H,I,J,K,L) -> f48(A,B,C,0,E,1 + F,G,H,I,J,0,L) [10 + -1*F >= 0 && 19 + D + -1*F >= 0 && 11 + -1*D + -1*F >= 0 && 11 + -1*C + -1*F >= 0 && -2 + B + -1*F >= 0 && 22 + -1*B + -1*F >= 0 && 11 + -1*A + -1*F >= 0 && F >= 0 && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && 9 + D >= 0 && 10 + -1*C + D >= 0 && -3 + B + D >= 0 && 21 + -1*B + D >= 0 && 10 + -1*A + D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0] f52(A,B,C,D,E,F,G,H,I,J,K,L) -> f48(A,B,C,0,E,1 + F,G,H,I,0,0,L) [10 + -1*F >= 0 && 19 + D + -1*F >= 0 && 11 + -1*D + -1*F >= 0 && 11 + -1*C + -1*F >= 0 && -2 + B + -1*F >= 0 && 22 + -1*B + -1*F >= 0 && 11 + -1*A + -1*F >= 0 && F >= 0 && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && 9 + D >= 0 && 10 + -1*C + D >= 0 && -3 + B + D >= 0 && 21 + -1*B + D >= 0 && 10 + -1*A + D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && J = 0] f52(A,B,C,D,E,F,G,H,I,J,K,L) -> f48(A,B,C,1,E,1 + F,G,H,I,J,1,L) [10 + -1*F >= 0 && 19 + D + -1*F >= 0 && 11 + -1*D + -1*F >= 0 && 11 + -1*C + -1*F >= 0 && -2 + B + -1*F >= 0 && 22 + -1*B + -1*F >= 0 && 11 + -1*A + -1*F >= 0 && F >= 0 && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && 9 + D >= 0 && 10 + -1*C + D >= 0 && -3 + B + D >= 0 && 21 + -1*B + D >= 0 && 10 + -1*A + D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && J >= 1] f52(A,B,C,D,E,F,G,H,I,J,K,L) -> f48(A,B,C,1,E,1 + F,G,H,I,J,1,L) [10 + -1*F >= 0 && 19 + D + -1*F >= 0 && 11 + -1*D + -1*F >= 0 && 11 + -1*C + -1*F >= 0 && -2 + B + -1*F >= 0 && 22 + -1*B + -1*F >= 0 && 11 + -1*A + -1*F >= 0 && F >= 0 && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && 9 + D >= 0 && 10 + -1*C + D >= 0 && -3 + B + D >= 0 && 21 + -1*B + D >= 0 && 10 + -1*A + D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && 0 >= 1 + J] f48(A,B,C,D,E,F,G,H,I,J,K,L) -> f52(A,B,C,D,E,F,G,H,I,M,K,L) [F >= 0 && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && D >= 1 && B >= 2 + F] f32(A,B,C,D,E,F,G,H,I,J,K,L) -> f48(A,B,C,D,E,0,G,H,I,J,K,L) [F >= 0 && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && -1 + D >= 0 && -1*C + D >= 0 && -13 + B + D >= 0 && 11 + -1*B + D >= 0 && -1*A + D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && 1 + F >= B] f35(A,B,C,D,E,F,G,H,I,J,K,L) -> f32(A,B,C,D,E,1 + F,G,H,I,J,K,L) [-1 + H >= 0 && -1 + F + H >= 0 && -1 + -1*F + H >= 0 && -2 + D + H >= 0 && -1*D + H >= 0 && -1*C + H >= 0 && -13 + B + H >= 0 && 11 + -1*B + H >= 0 && -1*A + H >= 0 && F >= 0 && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && -1 + D >= 0 && -1*C + D >= 0 && -13 + B + D >= 0 && 11 + -1*B + D >= 0 && -1*A + D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && H >= B] f38(A,B,C,D,E,F,G,H,I,J,K,L) -> f35(0,B,C,D,E,F,G,1 + H,0,J,K,L) [11 + -1*H >= 0 && 11 + F + -1*H >= 0 && 21 + -1*F + -1*H >= 0 && 10 + D + -1*H >= 0 && 12 + -1*D + -1*H >= 0 && 12 + -1*C + -1*H >= 0 && -1 + B + -1*H >= 0 && 23 + -1*B + -1*H >= 0 && 12 + -1*A + -1*H >= 0 && -1 + H >= 0 && -1 + F + H >= 0 && -1 + -1*F + H >= 0 && -2 + D + H >= 0 && -1*D + H >= 0 && -1*C + H >= 0 && -13 + B + H >= 0 && 11 + -1*B + H >= 0 && -1*A + H >= 0 && 10 + -1*F >= 0 && 9 + D + -1*F >= 0 && 11 + -1*D + -1*F >= 0 && 11 + -1*C + -1*F >= 0 && -2 + B + -1*F >= 0 && 22 + -1*B + -1*F >= 0 && 11 + -1*A + -1*F >= 0 && F >= 0 && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && -1 + D >= 0 && -1*C + D >= 0 && -13 + B + D >= 0 && 11 + -1*B + D >= 0 && -1*A + D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0] f38(A,B,C,D,E,F,G,H,I,J,K,L) -> f35(1,B,C,D,E,F,G,1 + H,1,J,K,L) [11 + -1*H >= 0 && 11 + F + -1*H >= 0 && 21 + -1*F + -1*H >= 0 && 10 + D + -1*H >= 0 && 12 + -1*D + -1*H >= 0 && 12 + -1*C + -1*H >= 0 && -1 + B + -1*H >= 0 && 23 + -1*B + -1*H >= 0 && 12 + -1*A + -1*H >= 0 && -1 + H >= 0 && -1 + F + H >= 0 && -1 + -1*F + H >= 0 && -2 + D + H >= 0 && -1*D + H >= 0 && -1*C + H >= 0 && -13 + B + H >= 0 && 11 + -1*B + H >= 0 && -1*A + H >= 0 && 10 + -1*F >= 0 && 9 + D + -1*F >= 0 && 11 + -1*D + -1*F >= 0 && 11 + -1*C + -1*F >= 0 && -2 + B + -1*F >= 0 && 22 + -1*B + -1*F >= 0 && 11 + -1*A + -1*F >= 0 && F >= 0 && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && -1 + D >= 0 && -1*C + D >= 0 && -13 + B + D >= 0 && 11 + -1*B + D >= 0 && -1*A + D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0] f38(A,B,C,D,E,F,G,H,I,J,K,L) -> f35(1,B,C,D,E,F,G,1 + H,1,J,K,L) [11 + -1*H >= 0 && 11 + F + -1*H >= 0 && 21 + -1*F + -1*H >= 0 && 10 + D + -1*H >= 0 && 12 + -1*D + -1*H >= 0 && 12 + -1*C + -1*H >= 0 && -1 + B + -1*H >= 0 && 23 + -1*B + -1*H >= 0 && 12 + -1*A + -1*H >= 0 && -1 + H >= 0 && -1 + F + H >= 0 && -1 + -1*F + H >= 0 && -2 + D + H >= 0 && -1*D + H >= 0 && -1*C + H >= 0 && -13 + B + H >= 0 && 11 + -1*B + H >= 0 && -1*A + H >= 0 && 10 + -1*F >= 0 && 9 + D + -1*F >= 0 && 11 + -1*D + -1*F >= 0 && 11 + -1*C + -1*F >= 0 && -2 + B + -1*F >= 0 && 22 + -1*B + -1*F >= 0 && 11 + -1*A + -1*F >= 0 && F >= 0 && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && -1 + D >= 0 && -1*C + D >= 0 && -13 + B + D >= 0 && 11 + -1*B + D >= 0 && -1*A + D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && M >= 1 + N] f35(A,B,C,D,E,F,G,H,I,J,K,L) -> f35(0,B,C,D,E,F,G,1 + H,0,J,K,L) [-1 + H >= 0 && -1 + F + H >= 0 && -1 + -1*F + H >= 0 && -2 + D + H >= 0 && -1*D + H >= 0 && -1*C + H >= 0 && -13 + B + H >= 0 && 11 + -1*B + H >= 0 && -1*A + H >= 0 && F >= 0 && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && -1 + D >= 0 && -1*C + D >= 0 && -13 + B + D >= 0 && 11 + -1*B + D >= 0 && -1*A + D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && B >= 1 + H && A = 0] f35(A,B,C,D,E,F,G,H,I,J,K,L) -> f38(A,B,C,D,E,F,G,H,I,J,K,L) [-1 + H >= 0 && -1 + F + H >= 0 && -1 + -1*F + H >= 0 && -2 + D + H >= 0 && -1*D + H >= 0 && -1*C + H >= 0 && -13 + B + H >= 0 && 11 + -1*B + H >= 0 && -1*A + H >= 0 && F >= 0 && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && -1 + D >= 0 && -1*C + D >= 0 && -13 + B + D >= 0 && 11 + -1*B + D >= 0 && -1*A + D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && A >= 1 && B >= 1 + H] f35(A,B,C,D,E,F,G,H,I,J,K,L) -> f38(A,B,C,D,E,F,G,H,I,J,K,L) [-1 + H >= 0 && -1 + F + H >= 0 && -1 + -1*F + H >= 0 && -2 + D + H >= 0 && -1*D + H >= 0 && -1*C + H >= 0 && -13 + B + H >= 0 && 11 + -1*B + H >= 0 && -1*A + H >= 0 && F >= 0 && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && -1 + D >= 0 && -1*C + D >= 0 && -13 + B + D >= 0 && 11 + -1*B + D >= 0 && -1*A + D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && 0 >= 1 + A && B >= 1 + H] f32(A,B,C,D,E,F,G,H,I,J,K,L) -> f35(A,B,C,D,E,F,G,1 + F,I,J,K,L) [F >= 0 && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && -1 + D >= 0 && -1*C + D >= 0 && -13 + B + D >= 0 && 11 + -1*B + D >= 0 && -1*A + D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && B >= 2 + F] f19(A,B,C,D,E,F,G,H,I,J,K,L) -> f19(A,B,0,D,E,1 + F,0,H,I,J,K,L) [F >= 0 && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && -1 + C + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && A + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && -1 + D >= 0 && -1*C + D >= 0 && -13 + B + D >= 0 && 11 + -1*B + D >= 0 && -2 + A + D >= 0 && -1*A + D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && A + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 11 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -13 + A + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && B >= 1 + F && C = 0] f19(A,B,C,D,E,F,G,H,I,J,K,L) -> f32(A,B,C,D,E,0,G,H,I,J,K,L) [F >= 0 && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && -1 + C + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && A + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && -1 + D >= 0 && -1*C + D >= 0 && -13 + B + D >= 0 && 11 + -1*B + D >= 0 && -2 + A + D >= 0 && -1*A + D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && A + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 11 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -13 + A + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && F >= B] f22(A,B,C,D,E,F,G,H,I,J,K,L) -> f19(A,B,0,D,E,1 + F,0,H,I,J,K,L) [11 + -1*F >= 0 && 10 + D + -1*F >= 0 && 12 + -1*D + -1*F >= 0 && 21 + C + -1*F >= 0 && 12 + -1*C + -1*F >= 0 && -1 + B + -1*F >= 0 && 23 + -1*B + -1*F >= 0 && 10 + A + -1*F >= 0 && 12 + -1*A + -1*F >= 0 && F >= 0 && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && -1 + C + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 11 + C + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && A + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && -1 + D >= 0 && 9 + C + D >= 0 && -1*C + D >= 0 && -13 + B + D >= 0 && 11 + -1*B + D >= 0 && -2 + A + D >= 0 && -1*A + D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && A + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 10 + C >= 0 && -2 + B + C >= 0 && 22 + -1*B + C >= 0 && 9 + A + C >= 0 && 11 + -1*A + C >= 0 && 12 + -1*B >= 0 && 11 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -13 + A + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && 0 >= 1 + M] f22(A,B,C,D,E,F,G,H,I,J,K,L) -> f19(A,B,0,D,E,1 + F,0,H,I,J,K,L) [11 + -1*F >= 0 && 10 + D + -1*F >= 0 && 12 + -1*D + -1*F >= 0 && 21 + C + -1*F >= 0 && 12 + -1*C + -1*F >= 0 && -1 + B + -1*F >= 0 && 23 + -1*B + -1*F >= 0 && 10 + A + -1*F >= 0 && 12 + -1*A + -1*F >= 0 && F >= 0 && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && -1 + C + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 11 + C + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && A + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && -1 + D >= 0 && 9 + C + D >= 0 && -1*C + D >= 0 && -13 + B + D >= 0 && 11 + -1*B + D >= 0 && -2 + A + D >= 0 && -1*A + D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && A + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 10 + C >= 0 && -2 + B + C >= 0 && 22 + -1*B + C >= 0 && 9 + A + C >= 0 && 11 + -1*A + C >= 0 && 12 + -1*B >= 0 && 11 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -13 + A + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && M >= 0] f22(A,B,C,D,E,F,G,H,I,J,K,L) -> f19(A,B,1,D,E,1 + F,1,H,I,J,K,L) [11 + -1*F >= 0 && 10 + D + -1*F >= 0 && 12 + -1*D + -1*F >= 0 && 21 + C + -1*F >= 0 && 12 + -1*C + -1*F >= 0 && -1 + B + -1*F >= 0 && 23 + -1*B + -1*F >= 0 && 10 + A + -1*F >= 0 && 12 + -1*A + -1*F >= 0 && F >= 0 && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && -1 + C + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 11 + C + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && A + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && -1 + D >= 0 && 9 + C + D >= 0 && -1*C + D >= 0 && -13 + B + D >= 0 && 11 + -1*B + D >= 0 && -2 + A + D >= 0 && -1*A + D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && A + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 10 + C >= 0 && -2 + B + C >= 0 && 22 + -1*B + C >= 0 && 9 + A + C >= 0 && 11 + -1*A + C >= 0 && 12 + -1*B >= 0 && 11 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -13 + A + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && M >= 0 && B >= 1 + N] f19(A,B,C,D,E,F,G,H,I,J,K,L) -> f22(A,B,C,D,E,F,G,H,I,J,K,L) [F >= 0 && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && -1 + C + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && A + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && -1 + D >= 0 && -1*C + D >= 0 && -13 + B + D >= 0 && 11 + -1*B + D >= 0 && -2 + A + D >= 0 && -1*A + D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && A + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && 12 + -1*B >= 0 && 11 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -13 + A + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && C >= 1 && B >= 1 + F] f13(A,B,C,D,E,F,G,H,I,J,K,L) -> f19(A,B,C,D,E,0,G,H,I,J,K,L) [F >= 0 && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && -1 + C + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && C + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && A + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && -1 + D >= 0 && -2 + C + D >= 0 && -1*C + D >= 0 && -13 + B + D >= 0 && 11 + -1*B + D >= 0 && -2 + A + D >= 0 && -1*A + D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && A + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && -1 + C >= 0 && -13 + B + C >= 0 && 11 + -1*B + C >= 0 && -2 + A + C >= 0 && -1*A + C >= 0 && 12 + -1*B >= 0 && 11 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -13 + A + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && F >= B] f13(A,B,C,D,E,F,G,H,I,J,K,L) -> f13(A,B,C,D,E,1 + F,G,H,I,J,K,L) [F >= 0 && -1 + D + F >= 0 && 1 + -1*D + F >= 0 && -1 + C + F >= 0 && 1 + -1*C + F >= 0 && -12 + B + F >= 0 && 12 + -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && 1 + -1*D >= 0 && C + -1*D >= 0 && 2 + -1*C + -1*D >= 0 && -11 + B + -1*D >= 0 && 13 + -1*B + -1*D >= 0 && A + -1*D >= 0 && 2 + -1*A + -1*D >= 0 && -1 + D >= 0 && -2 + C + D >= 0 && -1*C + D >= 0 && -13 + B + D >= 0 && 11 + -1*B + D >= 0 && -2 + A + D >= 0 && -1*A + D >= 0 && 1 + -1*C >= 0 && -11 + B + -1*C >= 0 && 13 + -1*B + -1*C >= 0 && A + -1*C >= 0 && 2 + -1*A + -1*C >= 0 && -1 + C >= 0 && -13 + B + C >= 0 && 11 + -1*B + C >= 0 && -2 + A + C >= 0 && -1*A + C >= 0 && 12 + -1*B >= 0 && 11 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -12 + B >= 0 && -13 + A + B >= 0 && -11 + -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && B >= 1 + F] f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f13(1,12,1,1,M,0,G,H,I,J,K,L) True Signature: {(f0,12) ;(f13,12) ;(f19,12) ;(f22,12) ;(f32,12) ;(f35,12) ;(f38,12) ;(f48,12) ;(f52,12) ;(f62,12) ;(f63,12) ;(f71,12)} Rule Graph: [0->{},1->{},2->{},3->{},4->{0,1,2},5->{0,1,2},6->{6,7,8,9},7->{},8->{3,4,5},9->{3,4,5},10->{6,7,8,9} ,11->{6,7,8,9},12->{7,8,9,14},13->{7,8,9,14},14->{10,11,12,13},15->{14},16->{15,23},17->{16,20},18->{16,21} ,19->{16,21},20->{16,20},21->{17,18,19},22->{17,18,19},23->{20,21,22},24->{24,25},25->{23},26->{24,25} ,27->{24,25},28->{25,29},29->{26,27,28},30->{29},31->{30,31},32->{31}] ,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,26,27,28,29,30,31,32] | +- p:[31] c: [31] | +- p:[28,29] c: [28,29] | +- p:[24] c: [24] | +- p:[16,17,21,18,22,23,19,20] c: [16,22,23] | | | +- p:[18,21,19] c: [18,19,21] | | | `- p:[20] c: [20] | +- p:[12,14,13] c: [12,13,14] | `- p:[6] c: [6]) + Applied Processor: CloseWith True + Details: () YES