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,D,E,F,G,H,I,J,K,0) [-9 + F >= 0 (?,1) && -19 + C + F >= 0 && 1 + -1*C + F >= 0 && -1 + B + F >= 0 && -8 + -1*B + F >= 0 && -10 + A + F >= 0 && -8 + -1*A + F >= 0 && 10 + -1*C >= 0 && 11 + -1*B + -1*C >= 0 && 9 + A + -1*C >= 0 && 11 + -1*A + -1*C >= 0 && -10 + C >= 0 && -9 + -1*B + C >= 0 && -11 + A + C >= 0 && -9 + -1*A + C >= 0 && 1 + -1*B >= 0 && A + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && 0 >= 1 + B] 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) [-9 + F >= 0 (?,1) && -19 + C + F >= 0 && 1 + -1*C + F >= 0 && -1 + B + F >= 0 && -8 + -1*B + F >= 0 && -10 + A + F >= 0 && -8 + -1*A + F >= 0 && 10 + -1*C >= 0 && 11 + -1*B + -1*C >= 0 && 9 + A + -1*C >= 0 && 11 + -1*A + -1*C >= 0 && -10 + C >= 0 && -9 + -1*B + C >= 0 && -11 + A + C >= 0 && -9 + -1*A + C >= 0 && 1 + -1*B >= 0 && A + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && B >= 1] 2. f63(A,B,C,D,E,F,G,H,I,J,K,L) -> f71(A,0,C,D,E,F,G,H,I,J,K,1) [-9 + F >= 0 (?,1) && -19 + C + F >= 0 && 1 + -1*C + F >= 0 && -1 + B + F >= 0 && -8 + -1*B + F >= 0 && -10 + A + F >= 0 && -8 + -1*A + F >= 0 && 10 + -1*C >= 0 && 11 + -1*B + -1*C >= 0 && 9 + A + -1*C >= 0 && 11 + -1*A + -1*C >= 0 && -10 + C >= 0 && -9 + -1*B + C >= 0 && -11 + A + C >= 0 && -9 + -1*A + C >= 0 && 1 + -1*B >= 0 && A + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && B = 0] 3. f52(A,B,C,D,E,F,G,H,I,J,K,L) -> f52(A,0,C,D,E,1 + F,G,H,I,J,0,L) [F >= 0 (?,1) && -10 + C + F >= 0 && 10 + -1*C + F >= 0 && -1 + B + F >= 0 && 1 + -1*B + F >= 0 && A + F >= 0 && 1 + -1*A + F >= 0 && 10 + -1*C >= 0 && 11 + -1*B + -1*C >= 0 && 10 + A + -1*C >= 0 && 11 + -1*A + -1*C >= 0 && -10 + C >= 0 && -9 + -1*B + C >= 0 && -10 + A + C >= 0 && -9 + -1*A + C >= 0 && 1 + -1*B >= 0 && 1 + A + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && 1 + -1*A >= 0 && A >= 0 && C >= 2 + F && B = 0] 4. f52(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) [F >= 0 (?,1) && -10 + C + F >= 0 && 10 + -1*C + F >= 0 && -1 + B + F >= 0 && 1 + -1*B + F >= 0 && A + F >= 0 && 1 + -1*A + F >= 0 && 10 + -1*C >= 0 && 11 + -1*B + -1*C >= 0 && 10 + A + -1*C >= 0 && 11 + -1*A + -1*C >= 0 && -10 + C >= 0 && -9 + -1*B + C >= 0 && -10 + A + C >= 0 && -9 + -1*A + C >= 0 && 1 + -1*B >= 0 && 1 + A + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && 1 + -1*A >= 0 && A >= 0 && A >= 1 && 1 + F >= C] 5. f52(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) [F >= 0 (?,1) && -10 + C + F >= 0 && 10 + -1*C + F >= 0 && -1 + B + F >= 0 && 1 + -1*B + F >= 0 && A + F >= 0 && 1 + -1*A + F >= 0 && 10 + -1*C >= 0 && 11 + -1*B + -1*C >= 0 && 10 + A + -1*C >= 0 && 11 + -1*A + -1*C >= 0 && -10 + C >= 0 && -9 + -1*B + C >= 0 && -10 + A + C >= 0 && -9 + -1*A + C >= 0 && 1 + -1*B >= 0 && 1 + A + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && 1 + -1*A >= 0 && A >= 0 && 1 + F >= C && A = 0] 6. f55(A,B,C,D,E,F,G,H,I,J,K,L) -> f52(A,1,C,D,E,1 + F,G,H,I,J,1,L) [8 + -1*F >= 0 (?,1) && -2 + C + -1*F >= 0 && 18 + -1*C + -1*F >= 0 && 15 + B + -1*F >= 0 && 9 + -1*B + -1*F >= 0 && 8 + A + -1*F >= 0 && 9 + -1*A + -1*F >= 0 && F >= 0 && -10 + C + F >= 0 && 10 + -1*C + F >= 0 && -1 + B + F >= 0 && 1 + -1*B + F >= 0 && A + F >= 0 && 1 + -1*A + F >= 0 && 10 + -1*C >= 0 && 17 + B + -1*C >= 0 && 11 + -1*B + -1*C >= 0 && 10 + A + -1*C >= 0 && 11 + -1*A + -1*C >= 0 && -10 + C >= 0 && -3 + B + C >= 0 && -9 + -1*B + C >= 0 && -10 + A + C >= 0 && -9 + -1*A + C >= 0 && 1 + -1*B >= 0 && 1 + A + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && 7 + B >= 0 && 7 + A + B >= 0 && 8 + -1*A + B >= 0 && 1 + -1*A >= 0 && A >= 0 && M >= 1 + N] 7. f55(A,B,C,D,E,F,G,H,I,J,K,L) -> f52(A,0,C,D,E,1 + F,G,H,I,J,0,L) [8 + -1*F >= 0 (?,1) && -2 + C + -1*F >= 0 && 18 + -1*C + -1*F >= 0 && 15 + B + -1*F >= 0 && 9 + -1*B + -1*F >= 0 && 8 + A + -1*F >= 0 && 9 + -1*A + -1*F >= 0 && F >= 0 && -10 + C + F >= 0 && 10 + -1*C + F >= 0 && -1 + B + F >= 0 && 1 + -1*B + F >= 0 && A + F >= 0 && 1 + -1*A + F >= 0 && 10 + -1*C >= 0 && 17 + B + -1*C >= 0 && 11 + -1*B + -1*C >= 0 && 10 + A + -1*C >= 0 && 11 + -1*A + -1*C >= 0 && -10 + C >= 0 && -3 + B + C >= 0 && -9 + -1*B + C >= 0 && -10 + A + C >= 0 && -9 + -1*A + C >= 0 && 1 + -1*B >= 0 && 1 + A + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && 7 + B >= 0 && 7 + A + B >= 0 && 8 + -1*A + B >= 0 && 1 + -1*A >= 0 && A >= 0] 8. f52(A,B,C,D,E,F,G,H,I,J,K,L) -> f55(A,B,C,D,E,F,G,H,I,J,K,L) [F >= 0 (?,1) && -10 + C + F >= 0 && 10 + -1*C + F >= 0 && -1 + B + F >= 0 && 1 + -1*B + F >= 0 && A + F >= 0 && 1 + -1*A + F >= 0 && 10 + -1*C >= 0 && 11 + -1*B + -1*C >= 0 && 10 + A + -1*C >= 0 && 11 + -1*A + -1*C >= 0 && -10 + C >= 0 && -9 + -1*B + C >= 0 && -10 + A + C >= 0 && -9 + -1*A + C >= 0 && 1 + -1*B >= 0 && 1 + A + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && 1 + -1*A >= 0 && A >= 0 && B >= 1 && C >= 2 + F] 9. f44(A,B,C,D,E,F,G,H,I,J,K,L) -> f29(1,B,C,D,E,1 + F,G,H,I,1,K,L) [-10 + H >= 0 (?,1) && -10 + G + H >= 0 && -1*G + H >= 0 && -10 + F + H >= 0 && -20 + C + H >= 0 && -1*C + H >= 0 && -11 + B + H >= 0 && -9 + -1*B + H >= 0 && -9 + -1*A + H >= 0 && G >= 0 && F + G >= 0 && -10 + C + G >= 0 && 10 + -1*C + G >= 0 && -1 + B + G >= 0 && 1 + -1*B + G >= 0 && 1 + -1*A + G >= 0 && F >= 0 && -10 + C + F >= 0 && 10 + -1*C + F >= 0 && -1 + B + F >= 0 && 1 + -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && 10 + -1*C >= 0 && 9 + B + -1*C >= 0 && 11 + -1*B + -1*C >= 0 && 11 + -1*A + -1*C >= 0 && -10 + C >= 0 && -11 + B + C >= 0 && -9 + -1*B + C >= 0 && -9 + -1*A + C >= 0 && 1 + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && -1 + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && G >= 1] 10. f44(A,B,C,D,E,F,G,H,I,J,K,L) -> f29(0,B,C,D,E,1 + F,0,H,I,0,K,L) [-10 + H >= 0 (?,1) && -10 + G + H >= 0 && -1*G + H >= 0 && -10 + F + H >= 0 && -20 + C + H >= 0 && -1*C + H >= 0 && -11 + B + H >= 0 && -9 + -1*B + H >= 0 && -9 + -1*A + H >= 0 && G >= 0 && F + G >= 0 && -10 + C + G >= 0 && 10 + -1*C + G >= 0 && -1 + B + G >= 0 && 1 + -1*B + G >= 0 && 1 + -1*A + G >= 0 && F >= 0 && -10 + C + F >= 0 && 10 + -1*C + F >= 0 && -1 + B + F >= 0 && 1 + -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && 10 + -1*C >= 0 && 9 + B + -1*C >= 0 && 11 + -1*B + -1*C >= 0 && 11 + -1*A + -1*C >= 0 && -10 + C >= 0 && -11 + B + C >= 0 && -9 + -1*B + C >= 0 && -9 + -1*A + C >= 0 && 1 + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && -1 + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && G = 0] 11. f29(A,B,C,D,E,F,G,H,I,J,K,L) -> f52(A,B,C,D,E,0,G,H,I,J,K,L) [F >= 0 (?,1) && -10 + C + F >= 0 && 10 + -1*C + F >= 0 && -1 + B + F >= 0 && 1 + -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && 10 + -1*C >= 0 && 9 + B + -1*C >= 0 && 11 + -1*B + -1*C >= 0 && 10 + A + -1*C >= 0 && 11 + -1*A + -1*C >= 0 && -10 + C >= 0 && -11 + B + C >= 0 && -9 + -1*B + C >= 0 && -10 + A + C >= 0 && -9 + -1*A + C >= 0 && 1 + -1*B >= 0 && 1 + A + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && A >= 0 && F >= C] 12. f33(A,B,C,D,E,F,G,H,I,J,K,L) -> f33(A,B,C,D,E,F,1,1 + H,1,J,K,L) [H >= 0 (?,1) && G + H >= 0 && -1*G + H >= 0 && F + H >= 0 && -10 + C + H >= 0 && 10 + -1*C + H >= 0 && -1 + B + H >= 0 && 1 + -1*B + H >= 0 && 1 + -1*A + H >= 0 && G >= 0 && F + G >= 0 && -10 + C + G >= 0 && 10 + -1*C + G >= 0 && -1 + B + G >= 0 && 1 + -1*B + G >= 0 && 1 + -1*A + G >= 0 && F >= 0 && -10 + C + F >= 0 && 10 + -1*C + F >= 0 && -1 + B + F >= 0 && 1 + -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && 10 + -1*C >= 0 && 9 + B + -1*C >= 0 && 11 + -1*B + -1*C >= 0 && 11 + -1*A + -1*C >= 0 && -10 + C >= 0 && -11 + B + C >= 0 && -9 + -1*B + C >= 0 && -9 + -1*A + C >= 0 && 1 + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && -1 + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && G >= 1 && C >= 1 + H] 13. f33(A,B,C,D,E,F,G,H,I,J,K,L) -> f44(A,B,C,D,E,F,G,H,I,J,K,L) [H >= 0 (?,1) && G + H >= 0 && -1*G + H >= 0 && F + H >= 0 && -10 + C + H >= 0 && 10 + -1*C + H >= 0 && -1 + B + H >= 0 && 1 + -1*B + H >= 0 && 1 + -1*A + H >= 0 && G >= 0 && F + G >= 0 && -10 + C + G >= 0 && 10 + -1*C + G >= 0 && -1 + B + G >= 0 && 1 + -1*B + G >= 0 && 1 + -1*A + G >= 0 && F >= 0 && -10 + C + F >= 0 && 10 + -1*C + F >= 0 && -1 + B + F >= 0 && 1 + -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && 10 + -1*C >= 0 && 9 + B + -1*C >= 0 && 11 + -1*B + -1*C >= 0 && 11 + -1*A + -1*C >= 0 && -10 + C >= 0 && -11 + B + C >= 0 && -9 + -1*B + C >= 0 && -9 + -1*A + C >= 0 && 1 + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && -1 + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && 0 >= 1 + A && H >= C] 14. f33(A,B,C,D,E,F,G,H,I,J,K,L) -> f44(A,B,C,D,E,F,G,H,I,J,K,L) [H >= 0 (?,1) && G + H >= 0 && -1*G + H >= 0 && F + H >= 0 && -10 + C + H >= 0 && 10 + -1*C + H >= 0 && -1 + B + H >= 0 && 1 + -1*B + H >= 0 && 1 + -1*A + H >= 0 && G >= 0 && F + G >= 0 && -10 + C + G >= 0 && 10 + -1*C + G >= 0 && -1 + B + G >= 0 && 1 + -1*B + G >= 0 && 1 + -1*A + G >= 0 && F >= 0 && -10 + C + F >= 0 && 10 + -1*C + F >= 0 && -1 + B + F >= 0 && 1 + -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && 10 + -1*C >= 0 && 9 + B + -1*C >= 0 && 11 + -1*B + -1*C >= 0 && 11 + -1*A + -1*C >= 0 && -10 + C >= 0 && -11 + B + C >= 0 && -9 + -1*B + C >= 0 && -9 + -1*A + C >= 0 && 1 + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && -1 + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && A >= 1 && H >= C] 15. f33(A,B,C,D,E,F,G,H,I,J,K,L) -> f29(0,B,C,D,E,1 + F,G,H,I,0,K,L) [H >= 0 (?,1) && G + H >= 0 && -1*G + H >= 0 && F + H >= 0 && -10 + C + H >= 0 && 10 + -1*C + H >= 0 && -1 + B + H >= 0 && 1 + -1*B + H >= 0 && 1 + -1*A + H >= 0 && G >= 0 && F + G >= 0 && -10 + C + G >= 0 && 10 + -1*C + G >= 0 && -1 + B + G >= 0 && 1 + -1*B + G >= 0 && 1 + -1*A + G >= 0 && F >= 0 && -10 + C + F >= 0 && 10 + -1*C + F >= 0 && -1 + B + F >= 0 && 1 + -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && 10 + -1*C >= 0 && 9 + B + -1*C >= 0 && 11 + -1*B + -1*C >= 0 && 11 + -1*A + -1*C >= 0 && -10 + C >= 0 && -11 + B + C >= 0 && -9 + -1*B + C >= 0 && -9 + -1*A + C >= 0 && 1 + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && -1 + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && H >= C && A = 0] 16. f33(A,B,C,D,E,F,G,H,I,J,K,L) -> f33(A,B,C,D,E,F,1,1 + H,1,J,K,L) [H >= 0 (?,1) && G + H >= 0 && -1*G + H >= 0 && F + H >= 0 && -10 + C + H >= 0 && 10 + -1*C + H >= 0 && -1 + B + H >= 0 && 1 + -1*B + H >= 0 && 1 + -1*A + H >= 0 && G >= 0 && F + G >= 0 && -10 + C + G >= 0 && 10 + -1*C + G >= 0 && -1 + B + G >= 0 && 1 + -1*B + G >= 0 && 1 + -1*A + G >= 0 && F >= 0 && -10 + C + F >= 0 && 10 + -1*C + F >= 0 && -1 + B + F >= 0 && 1 + -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && 10 + -1*C >= 0 && 9 + B + -1*C >= 0 && 11 + -1*B + -1*C >= 0 && 11 + -1*A + -1*C >= 0 && -10 + C >= 0 && -11 + B + C >= 0 && -9 + -1*B + C >= 0 && -9 + -1*A + C >= 0 && 1 + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && -1 + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && C >= 1 + H && G = 0] 17. f33(A,B,C,D,E,F,G,H,I,J,K,L) -> f33(A,B,C,D,E,F,0,1 + H,0,J,K,L) [H >= 0 (?,1) && G + H >= 0 && -1*G + H >= 0 && F + H >= 0 && -10 + C + H >= 0 && 10 + -1*C + H >= 0 && -1 + B + H >= 0 && 1 + -1*B + H >= 0 && 1 + -1*A + H >= 0 && G >= 0 && F + G >= 0 && -10 + C + G >= 0 && 10 + -1*C + G >= 0 && -1 + B + G >= 0 && 1 + -1*B + G >= 0 && 1 + -1*A + G >= 0 && F >= 0 && -10 + C + F >= 0 && 10 + -1*C + F >= 0 && -1 + B + F >= 0 && 1 + -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && 10 + -1*C >= 0 && 9 + B + -1*C >= 0 && 11 + -1*B + -1*C >= 0 && 11 + -1*A + -1*C >= 0 && -10 + C >= 0 && -11 + B + C >= 0 && -9 + -1*B + C >= 0 && -9 + -1*A + C >= 0 && 1 + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && -1 + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && M >= 1 + N && C >= 1 + H && G = 0] 18. f33(A,B,C,D,E,F,G,H,I,J,K,L) -> f33(A,B,C,D,E,F,0,1 + H,0,J,K,L) [H >= 0 (?,1) && G + H >= 0 && -1*G + H >= 0 && F + H >= 0 && -10 + C + H >= 0 && 10 + -1*C + H >= 0 && -1 + B + H >= 0 && 1 + -1*B + H >= 0 && 1 + -1*A + H >= 0 && G >= 0 && F + G >= 0 && -10 + C + G >= 0 && 10 + -1*C + G >= 0 && -1 + B + G >= 0 && 1 + -1*B + G >= 0 && 1 + -1*A + G >= 0 && F >= 0 && -10 + C + F >= 0 && 10 + -1*C + F >= 0 && -1 + B + F >= 0 && 1 + -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && 10 + -1*C >= 0 && 9 + B + -1*C >= 0 && 11 + -1*B + -1*C >= 0 && 11 + -1*A + -1*C >= 0 && -10 + C >= 0 && -11 + B + C >= 0 && -9 + -1*B + C >= 0 && -9 + -1*A + C >= 0 && 1 + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && -1 + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && C >= 1 + H && G = 0] 19. f29(A,B,C,D,E,F,G,H,I,J,K,L) -> f33(A,B,C,D,E,F,0,0,I,J,K,L) [F >= 0 (?,1) && -10 + C + F >= 0 && 10 + -1*C + F >= 0 && -1 + B + F >= 0 && 1 + -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && 10 + -1*C >= 0 && 9 + B + -1*C >= 0 && 11 + -1*B + -1*C >= 0 && 10 + A + -1*C >= 0 && 11 + -1*A + -1*C >= 0 && -10 + C >= 0 && -11 + B + C >= 0 && -9 + -1*B + C >= 0 && -10 + A + C >= 0 && -9 + -1*A + C >= 0 && 1 + -1*B >= 0 && 1 + A + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && A >= 0 && C >= 1 + F] 20. f23(A,B,C,D,E,F,G,H,I,J,K,L) -> f29(A,B,C,D,E,0,G,H,I,J,K,L) [F >= 0 (?,1) && -10 + C + F >= 0 && 10 + -1*C + F >= 0 && -1 + B + F >= 0 && 1 + -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && 10 + -1*C >= 0 && 9 + B + -1*C >= 0 && 11 + -1*B + -1*C >= 0 && 9 + A + -1*C >= 0 && 11 + -1*A + -1*C >= 0 && -10 + C >= 0 && -11 + B + C >= 0 && -9 + -1*B + C >= 0 && -11 + A + C >= 0 && -9 + -1*A + C >= 0 && 1 + -1*B >= 0 && A + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && F >= C] 21. f23(A,B,C,D,E,F,G,H,I,J,K,L) -> f23(A,B,C,D,E,1 + F,G,H,I,J,K,L) [F >= 0 (?,1) && -10 + C + F >= 0 && 10 + -1*C + F >= 0 && -1 + B + F >= 0 && 1 + -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && 10 + -1*C >= 0 && 9 + B + -1*C >= 0 && 11 + -1*B + -1*C >= 0 && 9 + A + -1*C >= 0 && 11 + -1*A + -1*C >= 0 && -10 + C >= 0 && -11 + B + C >= 0 && -9 + -1*B + C >= 0 && -11 + A + C >= 0 && -9 + -1*A + C >= 0 && 1 + -1*B >= 0 && A + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && C >= 1 + F] 22. f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f23(1,1,10,M,N,0,G,H,I,J,K,L) True (1,1) Signature: {(f0,12);(f23,12);(f29,12);(f33,12);(f44,12);(f52,12);(f55,12);(f63,12);(f71,12)} Flow Graph: [0->{},1->{},2->{},3->{3,4,5,8},4->{0,1,2},5->{},6->{3,4,5,8},7->{3,4,5,8},8->{6,7},9->{11,19},10->{11,19} ,11->{3,4,5,8},12->{12,13,14,15,16,17,18},13->{9,10},14->{9,10},15->{11,19},16->{12,13,14,15,16,17,18} ,17->{12,13,14,15,16,17,18},18->{12,13,14,15,16,17,18},19->{12,13,14,15,16,17,18},20->{11,19},21->{20,21} ,22->{20,21}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(3,8) ,(6,3) ,(7,8) ,(11,3) ,(11,4) ,(11,5) ,(12,16) ,(12,17) ,(12,18) ,(16,16) ,(16,17) ,(16,18) ,(17,12) ,(18,12) ,(19,12) ,(19,13) ,(19,14) ,(19,15) ,(20,11) ,(22,20)] * 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,D,E,F,G,H,I,J,K,0) [-9 + F >= 0 (?,1) && -19 + C + F >= 0 && 1 + -1*C + F >= 0 && -1 + B + F >= 0 && -8 + -1*B + F >= 0 && -10 + A + F >= 0 && -8 + -1*A + F >= 0 && 10 + -1*C >= 0 && 11 + -1*B + -1*C >= 0 && 9 + A + -1*C >= 0 && 11 + -1*A + -1*C >= 0 && -10 + C >= 0 && -9 + -1*B + C >= 0 && -11 + A + C >= 0 && -9 + -1*A + C >= 0 && 1 + -1*B >= 0 && A + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && 0 >= 1 + B] 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) [-9 + F >= 0 (?,1) && -19 + C + F >= 0 && 1 + -1*C + F >= 0 && -1 + B + F >= 0 && -8 + -1*B + F >= 0 && -10 + A + F >= 0 && -8 + -1*A + F >= 0 && 10 + -1*C >= 0 && 11 + -1*B + -1*C >= 0 && 9 + A + -1*C >= 0 && 11 + -1*A + -1*C >= 0 && -10 + C >= 0 && -9 + -1*B + C >= 0 && -11 + A + C >= 0 && -9 + -1*A + C >= 0 && 1 + -1*B >= 0 && A + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && B >= 1] 2. f63(A,B,C,D,E,F,G,H,I,J,K,L) -> f71(A,0,C,D,E,F,G,H,I,J,K,1) [-9 + F >= 0 (?,1) && -19 + C + F >= 0 && 1 + -1*C + F >= 0 && -1 + B + F >= 0 && -8 + -1*B + F >= 0 && -10 + A + F >= 0 && -8 + -1*A + F >= 0 && 10 + -1*C >= 0 && 11 + -1*B + -1*C >= 0 && 9 + A + -1*C >= 0 && 11 + -1*A + -1*C >= 0 && -10 + C >= 0 && -9 + -1*B + C >= 0 && -11 + A + C >= 0 && -9 + -1*A + C >= 0 && 1 + -1*B >= 0 && A + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && B = 0] 3. f52(A,B,C,D,E,F,G,H,I,J,K,L) -> f52(A,0,C,D,E,1 + F,G,H,I,J,0,L) [F >= 0 (?,1) && -10 + C + F >= 0 && 10 + -1*C + F >= 0 && -1 + B + F >= 0 && 1 + -1*B + F >= 0 && A + F >= 0 && 1 + -1*A + F >= 0 && 10 + -1*C >= 0 && 11 + -1*B + -1*C >= 0 && 10 + A + -1*C >= 0 && 11 + -1*A + -1*C >= 0 && -10 + C >= 0 && -9 + -1*B + C >= 0 && -10 + A + C >= 0 && -9 + -1*A + C >= 0 && 1 + -1*B >= 0 && 1 + A + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && 1 + -1*A >= 0 && A >= 0 && C >= 2 + F && B = 0] 4. f52(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) [F >= 0 (?,1) && -10 + C + F >= 0 && 10 + -1*C + F >= 0 && -1 + B + F >= 0 && 1 + -1*B + F >= 0 && A + F >= 0 && 1 + -1*A + F >= 0 && 10 + -1*C >= 0 && 11 + -1*B + -1*C >= 0 && 10 + A + -1*C >= 0 && 11 + -1*A + -1*C >= 0 && -10 + C >= 0 && -9 + -1*B + C >= 0 && -10 + A + C >= 0 && -9 + -1*A + C >= 0 && 1 + -1*B >= 0 && 1 + A + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && 1 + -1*A >= 0 && A >= 0 && A >= 1 && 1 + F >= C] 5. f52(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) [F >= 0 (?,1) && -10 + C + F >= 0 && 10 + -1*C + F >= 0 && -1 + B + F >= 0 && 1 + -1*B + F >= 0 && A + F >= 0 && 1 + -1*A + F >= 0 && 10 + -1*C >= 0 && 11 + -1*B + -1*C >= 0 && 10 + A + -1*C >= 0 && 11 + -1*A + -1*C >= 0 && -10 + C >= 0 && -9 + -1*B + C >= 0 && -10 + A + C >= 0 && -9 + -1*A + C >= 0 && 1 + -1*B >= 0 && 1 + A + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && 1 + -1*A >= 0 && A >= 0 && 1 + F >= C && A = 0] 6. f55(A,B,C,D,E,F,G,H,I,J,K,L) -> f52(A,1,C,D,E,1 + F,G,H,I,J,1,L) [8 + -1*F >= 0 (?,1) && -2 + C + -1*F >= 0 && 18 + -1*C + -1*F >= 0 && 15 + B + -1*F >= 0 && 9 + -1*B + -1*F >= 0 && 8 + A + -1*F >= 0 && 9 + -1*A + -1*F >= 0 && F >= 0 && -10 + C + F >= 0 && 10 + -1*C + F >= 0 && -1 + B + F >= 0 && 1 + -1*B + F >= 0 && A + F >= 0 && 1 + -1*A + F >= 0 && 10 + -1*C >= 0 && 17 + B + -1*C >= 0 && 11 + -1*B + -1*C >= 0 && 10 + A + -1*C >= 0 && 11 + -1*A + -1*C >= 0 && -10 + C >= 0 && -3 + B + C >= 0 && -9 + -1*B + C >= 0 && -10 + A + C >= 0 && -9 + -1*A + C >= 0 && 1 + -1*B >= 0 && 1 + A + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && 7 + B >= 0 && 7 + A + B >= 0 && 8 + -1*A + B >= 0 && 1 + -1*A >= 0 && A >= 0 && M >= 1 + N] 7. f55(A,B,C,D,E,F,G,H,I,J,K,L) -> f52(A,0,C,D,E,1 + F,G,H,I,J,0,L) [8 + -1*F >= 0 (?,1) && -2 + C + -1*F >= 0 && 18 + -1*C + -1*F >= 0 && 15 + B + -1*F >= 0 && 9 + -1*B + -1*F >= 0 && 8 + A + -1*F >= 0 && 9 + -1*A + -1*F >= 0 && F >= 0 && -10 + C + F >= 0 && 10 + -1*C + F >= 0 && -1 + B + F >= 0 && 1 + -1*B + F >= 0 && A + F >= 0 && 1 + -1*A + F >= 0 && 10 + -1*C >= 0 && 17 + B + -1*C >= 0 && 11 + -1*B + -1*C >= 0 && 10 + A + -1*C >= 0 && 11 + -1*A + -1*C >= 0 && -10 + C >= 0 && -3 + B + C >= 0 && -9 + -1*B + C >= 0 && -10 + A + C >= 0 && -9 + -1*A + C >= 0 && 1 + -1*B >= 0 && 1 + A + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && 7 + B >= 0 && 7 + A + B >= 0 && 8 + -1*A + B >= 0 && 1 + -1*A >= 0 && A >= 0] 8. f52(A,B,C,D,E,F,G,H,I,J,K,L) -> f55(A,B,C,D,E,F,G,H,I,J,K,L) [F >= 0 (?,1) && -10 + C + F >= 0 && 10 + -1*C + F >= 0 && -1 + B + F >= 0 && 1 + -1*B + F >= 0 && A + F >= 0 && 1 + -1*A + F >= 0 && 10 + -1*C >= 0 && 11 + -1*B + -1*C >= 0 && 10 + A + -1*C >= 0 && 11 + -1*A + -1*C >= 0 && -10 + C >= 0 && -9 + -1*B + C >= 0 && -10 + A + C >= 0 && -9 + -1*A + C >= 0 && 1 + -1*B >= 0 && 1 + A + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && 1 + -1*A >= 0 && A >= 0 && B >= 1 && C >= 2 + F] 9. f44(A,B,C,D,E,F,G,H,I,J,K,L) -> f29(1,B,C,D,E,1 + F,G,H,I,1,K,L) [-10 + H >= 0 (?,1) && -10 + G + H >= 0 && -1*G + H >= 0 && -10 + F + H >= 0 && -20 + C + H >= 0 && -1*C + H >= 0 && -11 + B + H >= 0 && -9 + -1*B + H >= 0 && -9 + -1*A + H >= 0 && G >= 0 && F + G >= 0 && -10 + C + G >= 0 && 10 + -1*C + G >= 0 && -1 + B + G >= 0 && 1 + -1*B + G >= 0 && 1 + -1*A + G >= 0 && F >= 0 && -10 + C + F >= 0 && 10 + -1*C + F >= 0 && -1 + B + F >= 0 && 1 + -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && 10 + -1*C >= 0 && 9 + B + -1*C >= 0 && 11 + -1*B + -1*C >= 0 && 11 + -1*A + -1*C >= 0 && -10 + C >= 0 && -11 + B + C >= 0 && -9 + -1*B + C >= 0 && -9 + -1*A + C >= 0 && 1 + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && -1 + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && G >= 1] 10. f44(A,B,C,D,E,F,G,H,I,J,K,L) -> f29(0,B,C,D,E,1 + F,0,H,I,0,K,L) [-10 + H >= 0 (?,1) && -10 + G + H >= 0 && -1*G + H >= 0 && -10 + F + H >= 0 && -20 + C + H >= 0 && -1*C + H >= 0 && -11 + B + H >= 0 && -9 + -1*B + H >= 0 && -9 + -1*A + H >= 0 && G >= 0 && F + G >= 0 && -10 + C + G >= 0 && 10 + -1*C + G >= 0 && -1 + B + G >= 0 && 1 + -1*B + G >= 0 && 1 + -1*A + G >= 0 && F >= 0 && -10 + C + F >= 0 && 10 + -1*C + F >= 0 && -1 + B + F >= 0 && 1 + -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && 10 + -1*C >= 0 && 9 + B + -1*C >= 0 && 11 + -1*B + -1*C >= 0 && 11 + -1*A + -1*C >= 0 && -10 + C >= 0 && -11 + B + C >= 0 && -9 + -1*B + C >= 0 && -9 + -1*A + C >= 0 && 1 + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && -1 + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && G = 0] 11. f29(A,B,C,D,E,F,G,H,I,J,K,L) -> f52(A,B,C,D,E,0,G,H,I,J,K,L) [F >= 0 (?,1) && -10 + C + F >= 0 && 10 + -1*C + F >= 0 && -1 + B + F >= 0 && 1 + -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && 10 + -1*C >= 0 && 9 + B + -1*C >= 0 && 11 + -1*B + -1*C >= 0 && 10 + A + -1*C >= 0 && 11 + -1*A + -1*C >= 0 && -10 + C >= 0 && -11 + B + C >= 0 && -9 + -1*B + C >= 0 && -10 + A + C >= 0 && -9 + -1*A + C >= 0 && 1 + -1*B >= 0 && 1 + A + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && A >= 0 && F >= C] 12. f33(A,B,C,D,E,F,G,H,I,J,K,L) -> f33(A,B,C,D,E,F,1,1 + H,1,J,K,L) [H >= 0 (?,1) && G + H >= 0 && -1*G + H >= 0 && F + H >= 0 && -10 + C + H >= 0 && 10 + -1*C + H >= 0 && -1 + B + H >= 0 && 1 + -1*B + H >= 0 && 1 + -1*A + H >= 0 && G >= 0 && F + G >= 0 && -10 + C + G >= 0 && 10 + -1*C + G >= 0 && -1 + B + G >= 0 && 1 + -1*B + G >= 0 && 1 + -1*A + G >= 0 && F >= 0 && -10 + C + F >= 0 && 10 + -1*C + F >= 0 && -1 + B + F >= 0 && 1 + -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && 10 + -1*C >= 0 && 9 + B + -1*C >= 0 && 11 + -1*B + -1*C >= 0 && 11 + -1*A + -1*C >= 0 && -10 + C >= 0 && -11 + B + C >= 0 && -9 + -1*B + C >= 0 && -9 + -1*A + C >= 0 && 1 + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && -1 + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && G >= 1 && C >= 1 + H] 13. f33(A,B,C,D,E,F,G,H,I,J,K,L) -> f44(A,B,C,D,E,F,G,H,I,J,K,L) [H >= 0 (?,1) && G + H >= 0 && -1*G + H >= 0 && F + H >= 0 && -10 + C + H >= 0 && 10 + -1*C + H >= 0 && -1 + B + H >= 0 && 1 + -1*B + H >= 0 && 1 + -1*A + H >= 0 && G >= 0 && F + G >= 0 && -10 + C + G >= 0 && 10 + -1*C + G >= 0 && -1 + B + G >= 0 && 1 + -1*B + G >= 0 && 1 + -1*A + G >= 0 && F >= 0 && -10 + C + F >= 0 && 10 + -1*C + F >= 0 && -1 + B + F >= 0 && 1 + -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && 10 + -1*C >= 0 && 9 + B + -1*C >= 0 && 11 + -1*B + -1*C >= 0 && 11 + -1*A + -1*C >= 0 && -10 + C >= 0 && -11 + B + C >= 0 && -9 + -1*B + C >= 0 && -9 + -1*A + C >= 0 && 1 + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && -1 + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && 0 >= 1 + A && H >= C] 14. f33(A,B,C,D,E,F,G,H,I,J,K,L) -> f44(A,B,C,D,E,F,G,H,I,J,K,L) [H >= 0 (?,1) && G + H >= 0 && -1*G + H >= 0 && F + H >= 0 && -10 + C + H >= 0 && 10 + -1*C + H >= 0 && -1 + B + H >= 0 && 1 + -1*B + H >= 0 && 1 + -1*A + H >= 0 && G >= 0 && F + G >= 0 && -10 + C + G >= 0 && 10 + -1*C + G >= 0 && -1 + B + G >= 0 && 1 + -1*B + G >= 0 && 1 + -1*A + G >= 0 && F >= 0 && -10 + C + F >= 0 && 10 + -1*C + F >= 0 && -1 + B + F >= 0 && 1 + -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && 10 + -1*C >= 0 && 9 + B + -1*C >= 0 && 11 + -1*B + -1*C >= 0 && 11 + -1*A + -1*C >= 0 && -10 + C >= 0 && -11 + B + C >= 0 && -9 + -1*B + C >= 0 && -9 + -1*A + C >= 0 && 1 + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && -1 + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && A >= 1 && H >= C] 15. f33(A,B,C,D,E,F,G,H,I,J,K,L) -> f29(0,B,C,D,E,1 + F,G,H,I,0,K,L) [H >= 0 (?,1) && G + H >= 0 && -1*G + H >= 0 && F + H >= 0 && -10 + C + H >= 0 && 10 + -1*C + H >= 0 && -1 + B + H >= 0 && 1 + -1*B + H >= 0 && 1 + -1*A + H >= 0 && G >= 0 && F + G >= 0 && -10 + C + G >= 0 && 10 + -1*C + G >= 0 && -1 + B + G >= 0 && 1 + -1*B + G >= 0 && 1 + -1*A + G >= 0 && F >= 0 && -10 + C + F >= 0 && 10 + -1*C + F >= 0 && -1 + B + F >= 0 && 1 + -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && 10 + -1*C >= 0 && 9 + B + -1*C >= 0 && 11 + -1*B + -1*C >= 0 && 11 + -1*A + -1*C >= 0 && -10 + C >= 0 && -11 + B + C >= 0 && -9 + -1*B + C >= 0 && -9 + -1*A + C >= 0 && 1 + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && -1 + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && H >= C && A = 0] 16. f33(A,B,C,D,E,F,G,H,I,J,K,L) -> f33(A,B,C,D,E,F,1,1 + H,1,J,K,L) [H >= 0 (?,1) && G + H >= 0 && -1*G + H >= 0 && F + H >= 0 && -10 + C + H >= 0 && 10 + -1*C + H >= 0 && -1 + B + H >= 0 && 1 + -1*B + H >= 0 && 1 + -1*A + H >= 0 && G >= 0 && F + G >= 0 && -10 + C + G >= 0 && 10 + -1*C + G >= 0 && -1 + B + G >= 0 && 1 + -1*B + G >= 0 && 1 + -1*A + G >= 0 && F >= 0 && -10 + C + F >= 0 && 10 + -1*C + F >= 0 && -1 + B + F >= 0 && 1 + -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && 10 + -1*C >= 0 && 9 + B + -1*C >= 0 && 11 + -1*B + -1*C >= 0 && 11 + -1*A + -1*C >= 0 && -10 + C >= 0 && -11 + B + C >= 0 && -9 + -1*B + C >= 0 && -9 + -1*A + C >= 0 && 1 + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && -1 + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && C >= 1 + H && G = 0] 17. f33(A,B,C,D,E,F,G,H,I,J,K,L) -> f33(A,B,C,D,E,F,0,1 + H,0,J,K,L) [H >= 0 (?,1) && G + H >= 0 && -1*G + H >= 0 && F + H >= 0 && -10 + C + H >= 0 && 10 + -1*C + H >= 0 && -1 + B + H >= 0 && 1 + -1*B + H >= 0 && 1 + -1*A + H >= 0 && G >= 0 && F + G >= 0 && -10 + C + G >= 0 && 10 + -1*C + G >= 0 && -1 + B + G >= 0 && 1 + -1*B + G >= 0 && 1 + -1*A + G >= 0 && F >= 0 && -10 + C + F >= 0 && 10 + -1*C + F >= 0 && -1 + B + F >= 0 && 1 + -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && 10 + -1*C >= 0 && 9 + B + -1*C >= 0 && 11 + -1*B + -1*C >= 0 && 11 + -1*A + -1*C >= 0 && -10 + C >= 0 && -11 + B + C >= 0 && -9 + -1*B + C >= 0 && -9 + -1*A + C >= 0 && 1 + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && -1 + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && M >= 1 + N && C >= 1 + H && G = 0] 18. f33(A,B,C,D,E,F,G,H,I,J,K,L) -> f33(A,B,C,D,E,F,0,1 + H,0,J,K,L) [H >= 0 (?,1) && G + H >= 0 && -1*G + H >= 0 && F + H >= 0 && -10 + C + H >= 0 && 10 + -1*C + H >= 0 && -1 + B + H >= 0 && 1 + -1*B + H >= 0 && 1 + -1*A + H >= 0 && G >= 0 && F + G >= 0 && -10 + C + G >= 0 && 10 + -1*C + G >= 0 && -1 + B + G >= 0 && 1 + -1*B + G >= 0 && 1 + -1*A + G >= 0 && F >= 0 && -10 + C + F >= 0 && 10 + -1*C + F >= 0 && -1 + B + F >= 0 && 1 + -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && 10 + -1*C >= 0 && 9 + B + -1*C >= 0 && 11 + -1*B + -1*C >= 0 && 11 + -1*A + -1*C >= 0 && -10 + C >= 0 && -11 + B + C >= 0 && -9 + -1*B + C >= 0 && -9 + -1*A + C >= 0 && 1 + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && -1 + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && C >= 1 + H && G = 0] 19. f29(A,B,C,D,E,F,G,H,I,J,K,L) -> f33(A,B,C,D,E,F,0,0,I,J,K,L) [F >= 0 (?,1) && -10 + C + F >= 0 && 10 + -1*C + F >= 0 && -1 + B + F >= 0 && 1 + -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && 10 + -1*C >= 0 && 9 + B + -1*C >= 0 && 11 + -1*B + -1*C >= 0 && 10 + A + -1*C >= 0 && 11 + -1*A + -1*C >= 0 && -10 + C >= 0 && -11 + B + C >= 0 && -9 + -1*B + C >= 0 && -10 + A + C >= 0 && -9 + -1*A + C >= 0 && 1 + -1*B >= 0 && 1 + A + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && A >= 0 && C >= 1 + F] 20. f23(A,B,C,D,E,F,G,H,I,J,K,L) -> f29(A,B,C,D,E,0,G,H,I,J,K,L) [F >= 0 (?,1) && -10 + C + F >= 0 && 10 + -1*C + F >= 0 && -1 + B + F >= 0 && 1 + -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && 10 + -1*C >= 0 && 9 + B + -1*C >= 0 && 11 + -1*B + -1*C >= 0 && 9 + A + -1*C >= 0 && 11 + -1*A + -1*C >= 0 && -10 + C >= 0 && -11 + B + C >= 0 && -9 + -1*B + C >= 0 && -11 + A + C >= 0 && -9 + -1*A + C >= 0 && 1 + -1*B >= 0 && A + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && F >= C] 21. f23(A,B,C,D,E,F,G,H,I,J,K,L) -> f23(A,B,C,D,E,1 + F,G,H,I,J,K,L) [F >= 0 (?,1) && -10 + C + F >= 0 && 10 + -1*C + F >= 0 && -1 + B + F >= 0 && 1 + -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && 10 + -1*C >= 0 && 9 + B + -1*C >= 0 && 11 + -1*B + -1*C >= 0 && 9 + A + -1*C >= 0 && 11 + -1*A + -1*C >= 0 && -10 + C >= 0 && -11 + B + C >= 0 && -9 + -1*B + C >= 0 && -11 + A + C >= 0 && -9 + -1*A + C >= 0 && 1 + -1*B >= 0 && A + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && C >= 1 + F] 22. f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f23(1,1,10,M,N,0,G,H,I,J,K,L) True (1,1) Signature: {(f0,12);(f23,12);(f29,12);(f33,12);(f44,12);(f52,12);(f55,12);(f63,12);(f71,12)} Flow Graph: [0->{},1->{},2->{},3->{3,4,5},4->{0,1,2},5->{},6->{4,5,8},7->{3,4,5},8->{6,7},9->{11,19},10->{11,19} ,11->{8},12->{12,13,14,15},13->{9,10},14->{9,10},15->{11,19},16->{12,13,14,15},17->{13,14,15,16,17,18} ,18->{13,14,15,16,17,18},19->{16,17,18},20->{19},21->{20,21},22->{21}] + 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,D,E,F,G,H,I,J,K,0) [-9 + F >= 0 && -19 + C + F >= 0 && 1 + -1*C + F >= 0 && -1 + B + F >= 0 && -8 + -1*B + F >= 0 && -10 + A + F >= 0 && -8 + -1*A + F >= 0 && 10 + -1*C >= 0 && 11 + -1*B + -1*C >= 0 && 9 + A + -1*C >= 0 && 11 + -1*A + -1*C >= 0 && -10 + C >= 0 && -9 + -1*B + C >= 0 && -11 + A + C >= 0 && -9 + -1*A + C >= 0 && 1 + -1*B >= 0 && A + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && 0 >= 1 + B] 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) [-9 + F >= 0 && -19 + C + F >= 0 && 1 + -1*C + F >= 0 && -1 + B + F >= 0 && -8 + -1*B + F >= 0 && -10 + A + F >= 0 && -8 + -1*A + F >= 0 && 10 + -1*C >= 0 && 11 + -1*B + -1*C >= 0 && 9 + A + -1*C >= 0 && 11 + -1*A + -1*C >= 0 && -10 + C >= 0 && -9 + -1*B + C >= 0 && -11 + A + C >= 0 && -9 + -1*A + C >= 0 && 1 + -1*B >= 0 && A + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && B >= 1] f63(A,B,C,D,E,F,G,H,I,J,K,L) -> f71(A,0,C,D,E,F,G,H,I,J,K,1) [-9 + F >= 0 && -19 + C + F >= 0 && 1 + -1*C + F >= 0 && -1 + B + F >= 0 && -8 + -1*B + F >= 0 && -10 + A + F >= 0 && -8 + -1*A + F >= 0 && 10 + -1*C >= 0 && 11 + -1*B + -1*C >= 0 && 9 + A + -1*C >= 0 && 11 + -1*A + -1*C >= 0 && -10 + C >= 0 && -9 + -1*B + C >= 0 && -11 + A + C >= 0 && -9 + -1*A + C >= 0 && 1 + -1*B >= 0 && A + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && B = 0] f52(A,B,C,D,E,F,G,H,I,J,K,L) -> f52(A,0,C,D,E,1 + F,G,H,I,J,0,L) [F >= 0 && -10 + C + F >= 0 && 10 + -1*C + F >= 0 && -1 + B + F >= 0 && 1 + -1*B + F >= 0 && A + F >= 0 && 1 + -1*A + F >= 0 && 10 + -1*C >= 0 && 11 + -1*B + -1*C >= 0 && 10 + A + -1*C >= 0 && 11 + -1*A + -1*C >= 0 && -10 + C >= 0 && -9 + -1*B + C >= 0 && -10 + A + C >= 0 && -9 + -1*A + C >= 0 && 1 + -1*B >= 0 && 1 + A + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && 1 + -1*A >= 0 && A >= 0 && C >= 2 + F && B = 0] f52(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) [F >= 0 && -10 + C + F >= 0 && 10 + -1*C + F >= 0 && -1 + B + F >= 0 && 1 + -1*B + F >= 0 && A + F >= 0 && 1 + -1*A + F >= 0 && 10 + -1*C >= 0 && 11 + -1*B + -1*C >= 0 && 10 + A + -1*C >= 0 && 11 + -1*A + -1*C >= 0 && -10 + C >= 0 && -9 + -1*B + C >= 0 && -10 + A + C >= 0 && -9 + -1*A + C >= 0 && 1 + -1*B >= 0 && 1 + A + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && 1 + -1*A >= 0 && A >= 0 && A >= 1 && 1 + F >= C] f52(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) [F >= 0 && -10 + C + F >= 0 && 10 + -1*C + F >= 0 && -1 + B + F >= 0 && 1 + -1*B + F >= 0 && A + F >= 0 && 1 + -1*A + F >= 0 && 10 + -1*C >= 0 && 11 + -1*B + -1*C >= 0 && 10 + A + -1*C >= 0 && 11 + -1*A + -1*C >= 0 && -10 + C >= 0 && -9 + -1*B + C >= 0 && -10 + A + C >= 0 && -9 + -1*A + C >= 0 && 1 + -1*B >= 0 && 1 + A + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && 1 + -1*A >= 0 && A >= 0 && 1 + F >= C && A = 0] f55(A,B,C,D,E,F,G,H,I,J,K,L) -> f52(A,1,C,D,E,1 + F,G,H,I,J,1,L) [8 + -1*F >= 0 && -2 + C + -1*F >= 0 && 18 + -1*C + -1*F >= 0 && 15 + B + -1*F >= 0 && 9 + -1*B + -1*F >= 0 && 8 + A + -1*F >= 0 && 9 + -1*A + -1*F >= 0 && F >= 0 && -10 + C + F >= 0 && 10 + -1*C + F >= 0 && -1 + B + F >= 0 && 1 + -1*B + F >= 0 && A + F >= 0 && 1 + -1*A + F >= 0 && 10 + -1*C >= 0 && 17 + B + -1*C >= 0 && 11 + -1*B + -1*C >= 0 && 10 + A + -1*C >= 0 && 11 + -1*A + -1*C >= 0 && -10 + C >= 0 && -3 + B + C >= 0 && -9 + -1*B + C >= 0 && -10 + A + C >= 0 && -9 + -1*A + C >= 0 && 1 + -1*B >= 0 && 1 + A + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && 7 + B >= 0 && 7 + A + B >= 0 && 8 + -1*A + B >= 0 && 1 + -1*A >= 0 && A >= 0 && M >= 1 + N] f55(A,B,C,D,E,F,G,H,I,J,K,L) -> f52(A,0,C,D,E,1 + F,G,H,I,J,0,L) [8 + -1*F >= 0 && -2 + C + -1*F >= 0 && 18 + -1*C + -1*F >= 0 && 15 + B + -1*F >= 0 && 9 + -1*B + -1*F >= 0 && 8 + A + -1*F >= 0 && 9 + -1*A + -1*F >= 0 && F >= 0 && -10 + C + F >= 0 && 10 + -1*C + F >= 0 && -1 + B + F >= 0 && 1 + -1*B + F >= 0 && A + F >= 0 && 1 + -1*A + F >= 0 && 10 + -1*C >= 0 && 17 + B + -1*C >= 0 && 11 + -1*B + -1*C >= 0 && 10 + A + -1*C >= 0 && 11 + -1*A + -1*C >= 0 && -10 + C >= 0 && -3 + B + C >= 0 && -9 + -1*B + C >= 0 && -10 + A + C >= 0 && -9 + -1*A + C >= 0 && 1 + -1*B >= 0 && 1 + A + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && 7 + B >= 0 && 7 + A + B >= 0 && 8 + -1*A + B >= 0 && 1 + -1*A >= 0 && A >= 0] f52(A,B,C,D,E,F,G,H,I,J,K,L) -> f55(A,B,C,D,E,F,G,H,I,J,K,L) [F >= 0 && -10 + C + F >= 0 && 10 + -1*C + F >= 0 && -1 + B + F >= 0 && 1 + -1*B + F >= 0 && A + F >= 0 && 1 + -1*A + F >= 0 && 10 + -1*C >= 0 && 11 + -1*B + -1*C >= 0 && 10 + A + -1*C >= 0 && 11 + -1*A + -1*C >= 0 && -10 + C >= 0 && -9 + -1*B + C >= 0 && -10 + A + C >= 0 && -9 + -1*A + C >= 0 && 1 + -1*B >= 0 && 1 + A + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && 1 + -1*A >= 0 && A >= 0 && B >= 1 && C >= 2 + F] f44(A,B,C,D,E,F,G,H,I,J,K,L) -> f29(1,B,C,D,E,1 + F,G,H,I,1,K,L) [-10 + H >= 0 && -10 + G + H >= 0 && -1*G + H >= 0 && -10 + F + H >= 0 && -20 + C + H >= 0 && -1*C + H >= 0 && -11 + B + H >= 0 && -9 + -1*B + H >= 0 && -9 + -1*A + H >= 0 && G >= 0 && F + G >= 0 && -10 + C + G >= 0 && 10 + -1*C + G >= 0 && -1 + B + G >= 0 && 1 + -1*B + G >= 0 && 1 + -1*A + G >= 0 && F >= 0 && -10 + C + F >= 0 && 10 + -1*C + F >= 0 && -1 + B + F >= 0 && 1 + -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && 10 + -1*C >= 0 && 9 + B + -1*C >= 0 && 11 + -1*B + -1*C >= 0 && 11 + -1*A + -1*C >= 0 && -10 + C >= 0 && -11 + B + C >= 0 && -9 + -1*B + C >= 0 && -9 + -1*A + C >= 0 && 1 + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && -1 + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && G >= 1] f44(A,B,C,D,E,F,G,H,I,J,K,L) -> f29(0,B,C,D,E,1 + F,0,H,I,0,K,L) [-10 + H >= 0 && -10 + G + H >= 0 && -1*G + H >= 0 && -10 + F + H >= 0 && -20 + C + H >= 0 && -1*C + H >= 0 && -11 + B + H >= 0 && -9 + -1*B + H >= 0 && -9 + -1*A + H >= 0 && G >= 0 && F + G >= 0 && -10 + C + G >= 0 && 10 + -1*C + G >= 0 && -1 + B + G >= 0 && 1 + -1*B + G >= 0 && 1 + -1*A + G >= 0 && F >= 0 && -10 + C + F >= 0 && 10 + -1*C + F >= 0 && -1 + B + F >= 0 && 1 + -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && 10 + -1*C >= 0 && 9 + B + -1*C >= 0 && 11 + -1*B + -1*C >= 0 && 11 + -1*A + -1*C >= 0 && -10 + C >= 0 && -11 + B + C >= 0 && -9 + -1*B + C >= 0 && -9 + -1*A + C >= 0 && 1 + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && -1 + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && G = 0] f29(A,B,C,D,E,F,G,H,I,J,K,L) -> f52(A,B,C,D,E,0,G,H,I,J,K,L) [F >= 0 && -10 + C + F >= 0 && 10 + -1*C + F >= 0 && -1 + B + F >= 0 && 1 + -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && 10 + -1*C >= 0 && 9 + B + -1*C >= 0 && 11 + -1*B + -1*C >= 0 && 10 + A + -1*C >= 0 && 11 + -1*A + -1*C >= 0 && -10 + C >= 0 && -11 + B + C >= 0 && -9 + -1*B + C >= 0 && -10 + A + C >= 0 && -9 + -1*A + C >= 0 && 1 + -1*B >= 0 && 1 + A + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && A >= 0 && F >= C] f33(A,B,C,D,E,F,G,H,I,J,K,L) -> f33(A,B,C,D,E,F,1,1 + H,1,J,K,L) [H >= 0 && G + H >= 0 && -1*G + H >= 0 && F + H >= 0 && -10 + C + H >= 0 && 10 + -1*C + H >= 0 && -1 + B + H >= 0 && 1 + -1*B + H >= 0 && 1 + -1*A + H >= 0 && G >= 0 && F + G >= 0 && -10 + C + G >= 0 && 10 + -1*C + G >= 0 && -1 + B + G >= 0 && 1 + -1*B + G >= 0 && 1 + -1*A + G >= 0 && F >= 0 && -10 + C + F >= 0 && 10 + -1*C + F >= 0 && -1 + B + F >= 0 && 1 + -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && 10 + -1*C >= 0 && 9 + B + -1*C >= 0 && 11 + -1*B + -1*C >= 0 && 11 + -1*A + -1*C >= 0 && -10 + C >= 0 && -11 + B + C >= 0 && -9 + -1*B + C >= 0 && -9 + -1*A + C >= 0 && 1 + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && -1 + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && G >= 1 && C >= 1 + H] f33(A,B,C,D,E,F,G,H,I,J,K,L) -> f44(A,B,C,D,E,F,G,H,I,J,K,L) [H >= 0 && G + H >= 0 && -1*G + H >= 0 && F + H >= 0 && -10 + C + H >= 0 && 10 + -1*C + H >= 0 && -1 + B + H >= 0 && 1 + -1*B + H >= 0 && 1 + -1*A + H >= 0 && G >= 0 && F + G >= 0 && -10 + C + G >= 0 && 10 + -1*C + G >= 0 && -1 + B + G >= 0 && 1 + -1*B + G >= 0 && 1 + -1*A + G >= 0 && F >= 0 && -10 + C + F >= 0 && 10 + -1*C + F >= 0 && -1 + B + F >= 0 && 1 + -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && 10 + -1*C >= 0 && 9 + B + -1*C >= 0 && 11 + -1*B + -1*C >= 0 && 11 + -1*A + -1*C >= 0 && -10 + C >= 0 && -11 + B + C >= 0 && -9 + -1*B + C >= 0 && -9 + -1*A + C >= 0 && 1 + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && -1 + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && 0 >= 1 + A && H >= C] f33(A,B,C,D,E,F,G,H,I,J,K,L) -> f44(A,B,C,D,E,F,G,H,I,J,K,L) [H >= 0 && G + H >= 0 && -1*G + H >= 0 && F + H >= 0 && -10 + C + H >= 0 && 10 + -1*C + H >= 0 && -1 + B + H >= 0 && 1 + -1*B + H >= 0 && 1 + -1*A + H >= 0 && G >= 0 && F + G >= 0 && -10 + C + G >= 0 && 10 + -1*C + G >= 0 && -1 + B + G >= 0 && 1 + -1*B + G >= 0 && 1 + -1*A + G >= 0 && F >= 0 && -10 + C + F >= 0 && 10 + -1*C + F >= 0 && -1 + B + F >= 0 && 1 + -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && 10 + -1*C >= 0 && 9 + B + -1*C >= 0 && 11 + -1*B + -1*C >= 0 && 11 + -1*A + -1*C >= 0 && -10 + C >= 0 && -11 + B + C >= 0 && -9 + -1*B + C >= 0 && -9 + -1*A + C >= 0 && 1 + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && -1 + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && A >= 1 && H >= C] f33(A,B,C,D,E,F,G,H,I,J,K,L) -> f29(0,B,C,D,E,1 + F,G,H,I,0,K,L) [H >= 0 && G + H >= 0 && -1*G + H >= 0 && F + H >= 0 && -10 + C + H >= 0 && 10 + -1*C + H >= 0 && -1 + B + H >= 0 && 1 + -1*B + H >= 0 && 1 + -1*A + H >= 0 && G >= 0 && F + G >= 0 && -10 + C + G >= 0 && 10 + -1*C + G >= 0 && -1 + B + G >= 0 && 1 + -1*B + G >= 0 && 1 + -1*A + G >= 0 && F >= 0 && -10 + C + F >= 0 && 10 + -1*C + F >= 0 && -1 + B + F >= 0 && 1 + -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && 10 + -1*C >= 0 && 9 + B + -1*C >= 0 && 11 + -1*B + -1*C >= 0 && 11 + -1*A + -1*C >= 0 && -10 + C >= 0 && -11 + B + C >= 0 && -9 + -1*B + C >= 0 && -9 + -1*A + C >= 0 && 1 + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && -1 + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && H >= C && A = 0] f33(A,B,C,D,E,F,G,H,I,J,K,L) -> f33(A,B,C,D,E,F,1,1 + H,1,J,K,L) [H >= 0 && G + H >= 0 && -1*G + H >= 0 && F + H >= 0 && -10 + C + H >= 0 && 10 + -1*C + H >= 0 && -1 + B + H >= 0 && 1 + -1*B + H >= 0 && 1 + -1*A + H >= 0 && G >= 0 && F + G >= 0 && -10 + C + G >= 0 && 10 + -1*C + G >= 0 && -1 + B + G >= 0 && 1 + -1*B + G >= 0 && 1 + -1*A + G >= 0 && F >= 0 && -10 + C + F >= 0 && 10 + -1*C + F >= 0 && -1 + B + F >= 0 && 1 + -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && 10 + -1*C >= 0 && 9 + B + -1*C >= 0 && 11 + -1*B + -1*C >= 0 && 11 + -1*A + -1*C >= 0 && -10 + C >= 0 && -11 + B + C >= 0 && -9 + -1*B + C >= 0 && -9 + -1*A + C >= 0 && 1 + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && -1 + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && C >= 1 + H && G = 0] f33(A,B,C,D,E,F,G,H,I,J,K,L) -> f33(A,B,C,D,E,F,0,1 + H,0,J,K,L) [H >= 0 && G + H >= 0 && -1*G + H >= 0 && F + H >= 0 && -10 + C + H >= 0 && 10 + -1*C + H >= 0 && -1 + B + H >= 0 && 1 + -1*B + H >= 0 && 1 + -1*A + H >= 0 && G >= 0 && F + G >= 0 && -10 + C + G >= 0 && 10 + -1*C + G >= 0 && -1 + B + G >= 0 && 1 + -1*B + G >= 0 && 1 + -1*A + G >= 0 && F >= 0 && -10 + C + F >= 0 && 10 + -1*C + F >= 0 && -1 + B + F >= 0 && 1 + -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && 10 + -1*C >= 0 && 9 + B + -1*C >= 0 && 11 + -1*B + -1*C >= 0 && 11 + -1*A + -1*C >= 0 && -10 + C >= 0 && -11 + B + C >= 0 && -9 + -1*B + C >= 0 && -9 + -1*A + C >= 0 && 1 + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && -1 + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && M >= 1 + N && C >= 1 + H && G = 0] f33(A,B,C,D,E,F,G,H,I,J,K,L) -> f33(A,B,C,D,E,F,0,1 + H,0,J,K,L) [H >= 0 && G + H >= 0 && -1*G + H >= 0 && F + H >= 0 && -10 + C + H >= 0 && 10 + -1*C + H >= 0 && -1 + B + H >= 0 && 1 + -1*B + H >= 0 && 1 + -1*A + H >= 0 && G >= 0 && F + G >= 0 && -10 + C + G >= 0 && 10 + -1*C + G >= 0 && -1 + B + G >= 0 && 1 + -1*B + G >= 0 && 1 + -1*A + G >= 0 && F >= 0 && -10 + C + F >= 0 && 10 + -1*C + F >= 0 && -1 + B + F >= 0 && 1 + -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && 10 + -1*C >= 0 && 9 + B + -1*C >= 0 && 11 + -1*B + -1*C >= 0 && 11 + -1*A + -1*C >= 0 && -10 + C >= 0 && -11 + B + C >= 0 && -9 + -1*B + C >= 0 && -9 + -1*A + C >= 0 && 1 + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && -1 + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && C >= 1 + H && G = 0] f29(A,B,C,D,E,F,G,H,I,J,K,L) -> f33(A,B,C,D,E,F,0,0,I,J,K,L) [F >= 0 && -10 + C + F >= 0 && 10 + -1*C + F >= 0 && -1 + B + F >= 0 && 1 + -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && 10 + -1*C >= 0 && 9 + B + -1*C >= 0 && 11 + -1*B + -1*C >= 0 && 10 + A + -1*C >= 0 && 11 + -1*A + -1*C >= 0 && -10 + C >= 0 && -11 + B + C >= 0 && -9 + -1*B + C >= 0 && -10 + A + C >= 0 && -9 + -1*A + C >= 0 && 1 + -1*B >= 0 && 1 + A + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && A >= 0 && C >= 1 + F] f23(A,B,C,D,E,F,G,H,I,J,K,L) -> f29(A,B,C,D,E,0,G,H,I,J,K,L) [F >= 0 && -10 + C + F >= 0 && 10 + -1*C + F >= 0 && -1 + B + F >= 0 && 1 + -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && 10 + -1*C >= 0 && 9 + B + -1*C >= 0 && 11 + -1*B + -1*C >= 0 && 9 + A + -1*C >= 0 && 11 + -1*A + -1*C >= 0 && -10 + C >= 0 && -11 + B + C >= 0 && -9 + -1*B + C >= 0 && -11 + A + C >= 0 && -9 + -1*A + C >= 0 && 1 + -1*B >= 0 && A + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && F >= C] f23(A,B,C,D,E,F,G,H,I,J,K,L) -> f23(A,B,C,D,E,1 + F,G,H,I,J,K,L) [F >= 0 && -10 + C + F >= 0 && 10 + -1*C + F >= 0 && -1 + B + F >= 0 && 1 + -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && 10 + -1*C >= 0 && 9 + B + -1*C >= 0 && 11 + -1*B + -1*C >= 0 && 9 + A + -1*C >= 0 && 11 + -1*A + -1*C >= 0 && -10 + C >= 0 && -11 + B + C >= 0 && -9 + -1*B + C >= 0 && -11 + A + C >= 0 && -9 + -1*A + C >= 0 && 1 + -1*B >= 0 && A + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && C >= 1 + F] f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f23(1,1,10,M,N,0,G,H,I,J,K,L) True Signature: {(f0,12);(f23,12);(f29,12);(f33,12);(f44,12);(f52,12);(f55,12);(f63,12);(f71,12)} Rule Graph: [0->{},1->{},2->{},3->{3,4,5},4->{0,1,2},5->{},6->{4,5,8},7->{3,4,5},8->{6,7},9->{11,19},10->{11,19} ,11->{8},12->{12,13,14,15},13->{9,10},14->{9,10},15->{11,19},16->{12,13,14,15},17->{13,14,15,16,17,18} ,18->{13,14,15,16,17,18},19->{16,17,18},20->{19},21->{20,21},22->{21}] + 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] | +- p:[21] c: [21] | +- p:[9,13,12,16,17,18,19,10,14,15] c: [9,10,13,14,15,19] | | | +- p:[17,18] c: [18] | | | | | `- p:[17] c: [17] | | | `- p:[12] c: [12] | +- p:[6,8] c: [6,8] | `- p:[3] c: [3] * Step 4: CloseWith YES + Considered Problem: (Rules: 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) [-9 + F >= 0 && -19 + C + F >= 0 && 1 + -1*C + F >= 0 && -1 + B + F >= 0 && -8 + -1*B + F >= 0 && -10 + A + F >= 0 && -8 + -1*A + F >= 0 && 10 + -1*C >= 0 && 11 + -1*B + -1*C >= 0 && 9 + A + -1*C >= 0 && 11 + -1*A + -1*C >= 0 && -10 + C >= 0 && -9 + -1*B + C >= 0 && -11 + A + C >= 0 && -9 + -1*A + C >= 0 && 1 + -1*B >= 0 && A + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && 0 >= 1 + B] 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) [-9 + F >= 0 && -19 + C + F >= 0 && 1 + -1*C + F >= 0 && -1 + B + F >= 0 && -8 + -1*B + F >= 0 && -10 + A + F >= 0 && -8 + -1*A + F >= 0 && 10 + -1*C >= 0 && 11 + -1*B + -1*C >= 0 && 9 + A + -1*C >= 0 && 11 + -1*A + -1*C >= 0 && -10 + C >= 0 && -9 + -1*B + C >= 0 && -11 + A + C >= 0 && -9 + -1*A + C >= 0 && 1 + -1*B >= 0 && A + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && B >= 1] f63(A,B,C,D,E,F,G,H,I,J,K,L) -> f71(A,0,C,D,E,F,G,H,I,J,K,1) [-9 + F >= 0 && -19 + C + F >= 0 && 1 + -1*C + F >= 0 && -1 + B + F >= 0 && -8 + -1*B + F >= 0 && -10 + A + F >= 0 && -8 + -1*A + F >= 0 && 10 + -1*C >= 0 && 11 + -1*B + -1*C >= 0 && 9 + A + -1*C >= 0 && 11 + -1*A + -1*C >= 0 && -10 + C >= 0 && -9 + -1*B + C >= 0 && -11 + A + C >= 0 && -9 + -1*A + C >= 0 && 1 + -1*B >= 0 && A + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && B = 0] f52(A,B,C,D,E,F,G,H,I,J,K,L) -> f52(A,0,C,D,E,1 + F,G,H,I,J,0,L) [F >= 0 && -10 + C + F >= 0 && 10 + -1*C + F >= 0 && -1 + B + F >= 0 && 1 + -1*B + F >= 0 && A + F >= 0 && 1 + -1*A + F >= 0 && 10 + -1*C >= 0 && 11 + -1*B + -1*C >= 0 && 10 + A + -1*C >= 0 && 11 + -1*A + -1*C >= 0 && -10 + C >= 0 && -9 + -1*B + C >= 0 && -10 + A + C >= 0 && -9 + -1*A + C >= 0 && 1 + -1*B >= 0 && 1 + A + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && 1 + -1*A >= 0 && A >= 0 && C >= 2 + F && B = 0] f52(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) [F >= 0 && -10 + C + F >= 0 && 10 + -1*C + F >= 0 && -1 + B + F >= 0 && 1 + -1*B + F >= 0 && A + F >= 0 && 1 + -1*A + F >= 0 && 10 + -1*C >= 0 && 11 + -1*B + -1*C >= 0 && 10 + A + -1*C >= 0 && 11 + -1*A + -1*C >= 0 && -10 + C >= 0 && -9 + -1*B + C >= 0 && -10 + A + C >= 0 && -9 + -1*A + C >= 0 && 1 + -1*B >= 0 && 1 + A + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && 1 + -1*A >= 0 && A >= 0 && A >= 1 && 1 + F >= C] f52(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) [F >= 0 && -10 + C + F >= 0 && 10 + -1*C + F >= 0 && -1 + B + F >= 0 && 1 + -1*B + F >= 0 && A + F >= 0 && 1 + -1*A + F >= 0 && 10 + -1*C >= 0 && 11 + -1*B + -1*C >= 0 && 10 + A + -1*C >= 0 && 11 + -1*A + -1*C >= 0 && -10 + C >= 0 && -9 + -1*B + C >= 0 && -10 + A + C >= 0 && -9 + -1*A + C >= 0 && 1 + -1*B >= 0 && 1 + A + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && 1 + -1*A >= 0 && A >= 0 && 1 + F >= C && A = 0] f55(A,B,C,D,E,F,G,H,I,J,K,L) -> f52(A,1,C,D,E,1 + F,G,H,I,J,1,L) [8 + -1*F >= 0 && -2 + C + -1*F >= 0 && 18 + -1*C + -1*F >= 0 && 15 + B + -1*F >= 0 && 9 + -1*B + -1*F >= 0 && 8 + A + -1*F >= 0 && 9 + -1*A + -1*F >= 0 && F >= 0 && -10 + C + F >= 0 && 10 + -1*C + F >= 0 && -1 + B + F >= 0 && 1 + -1*B + F >= 0 && A + F >= 0 && 1 + -1*A + F >= 0 && 10 + -1*C >= 0 && 17 + B + -1*C >= 0 && 11 + -1*B + -1*C >= 0 && 10 + A + -1*C >= 0 && 11 + -1*A + -1*C >= 0 && -10 + C >= 0 && -3 + B + C >= 0 && -9 + -1*B + C >= 0 && -10 + A + C >= 0 && -9 + -1*A + C >= 0 && 1 + -1*B >= 0 && 1 + A + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && 7 + B >= 0 && 7 + A + B >= 0 && 8 + -1*A + B >= 0 && 1 + -1*A >= 0 && A >= 0 && M >= 1 + N] f55(A,B,C,D,E,F,G,H,I,J,K,L) -> f52(A,0,C,D,E,1 + F,G,H,I,J,0,L) [8 + -1*F >= 0 && -2 + C + -1*F >= 0 && 18 + -1*C + -1*F >= 0 && 15 + B + -1*F >= 0 && 9 + -1*B + -1*F >= 0 && 8 + A + -1*F >= 0 && 9 + -1*A + -1*F >= 0 && F >= 0 && -10 + C + F >= 0 && 10 + -1*C + F >= 0 && -1 + B + F >= 0 && 1 + -1*B + F >= 0 && A + F >= 0 && 1 + -1*A + F >= 0 && 10 + -1*C >= 0 && 17 + B + -1*C >= 0 && 11 + -1*B + -1*C >= 0 && 10 + A + -1*C >= 0 && 11 + -1*A + -1*C >= 0 && -10 + C >= 0 && -3 + B + C >= 0 && -9 + -1*B + C >= 0 && -10 + A + C >= 0 && -9 + -1*A + C >= 0 && 1 + -1*B >= 0 && 1 + A + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && 7 + B >= 0 && 7 + A + B >= 0 && 8 + -1*A + B >= 0 && 1 + -1*A >= 0 && A >= 0] f52(A,B,C,D,E,F,G,H,I,J,K,L) -> f55(A,B,C,D,E,F,G,H,I,J,K,L) [F >= 0 && -10 + C + F >= 0 && 10 + -1*C + F >= 0 && -1 + B + F >= 0 && 1 + -1*B + F >= 0 && A + F >= 0 && 1 + -1*A + F >= 0 && 10 + -1*C >= 0 && 11 + -1*B + -1*C >= 0 && 10 + A + -1*C >= 0 && 11 + -1*A + -1*C >= 0 && -10 + C >= 0 && -9 + -1*B + C >= 0 && -10 + A + C >= 0 && -9 + -1*A + C >= 0 && 1 + -1*B >= 0 && 1 + A + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && 1 + -1*A >= 0 && A >= 0 && B >= 1 && C >= 2 + F] f44(A,B,C,D,E,F,G,H,I,J,K,L) -> f29(1,B,C,D,E,1 + F,G,H,I,1,K,L) [-10 + H >= 0 && -10 + G + H >= 0 && -1*G + H >= 0 && -10 + F + H >= 0 && -20 + C + H >= 0 && -1*C + H >= 0 && -11 + B + H >= 0 && -9 + -1*B + H >= 0 && -9 + -1*A + H >= 0 && G >= 0 && F + G >= 0 && -10 + C + G >= 0 && 10 + -1*C + G >= 0 && -1 + B + G >= 0 && 1 + -1*B + G >= 0 && 1 + -1*A + G >= 0 && F >= 0 && -10 + C + F >= 0 && 10 + -1*C + F >= 0 && -1 + B + F >= 0 && 1 + -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && 10 + -1*C >= 0 && 9 + B + -1*C >= 0 && 11 + -1*B + -1*C >= 0 && 11 + -1*A + -1*C >= 0 && -10 + C >= 0 && -11 + B + C >= 0 && -9 + -1*B + C >= 0 && -9 + -1*A + C >= 0 && 1 + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && -1 + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && G >= 1] f44(A,B,C,D,E,F,G,H,I,J,K,L) -> f29(0,B,C,D,E,1 + F,0,H,I,0,K,L) [-10 + H >= 0 && -10 + G + H >= 0 && -1*G + H >= 0 && -10 + F + H >= 0 && -20 + C + H >= 0 && -1*C + H >= 0 && -11 + B + H >= 0 && -9 + -1*B + H >= 0 && -9 + -1*A + H >= 0 && G >= 0 && F + G >= 0 && -10 + C + G >= 0 && 10 + -1*C + G >= 0 && -1 + B + G >= 0 && 1 + -1*B + G >= 0 && 1 + -1*A + G >= 0 && F >= 0 && -10 + C + F >= 0 && 10 + -1*C + F >= 0 && -1 + B + F >= 0 && 1 + -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && 10 + -1*C >= 0 && 9 + B + -1*C >= 0 && 11 + -1*B + -1*C >= 0 && 11 + -1*A + -1*C >= 0 && -10 + C >= 0 && -11 + B + C >= 0 && -9 + -1*B + C >= 0 && -9 + -1*A + C >= 0 && 1 + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && -1 + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && G = 0] f29(A,B,C,D,E,F,G,H,I,J,K,L) -> f52(A,B,C,D,E,0,G,H,I,J,K,L) [F >= 0 && -10 + C + F >= 0 && 10 + -1*C + F >= 0 && -1 + B + F >= 0 && 1 + -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && 10 + -1*C >= 0 && 9 + B + -1*C >= 0 && 11 + -1*B + -1*C >= 0 && 10 + A + -1*C >= 0 && 11 + -1*A + -1*C >= 0 && -10 + C >= 0 && -11 + B + C >= 0 && -9 + -1*B + C >= 0 && -10 + A + C >= 0 && -9 + -1*A + C >= 0 && 1 + -1*B >= 0 && 1 + A + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && A >= 0 && F >= C] f33(A,B,C,D,E,F,G,H,I,J,K,L) -> f33(A,B,C,D,E,F,1,1 + H,1,J,K,L) [H >= 0 && G + H >= 0 && -1*G + H >= 0 && F + H >= 0 && -10 + C + H >= 0 && 10 + -1*C + H >= 0 && -1 + B + H >= 0 && 1 + -1*B + H >= 0 && 1 + -1*A + H >= 0 && G >= 0 && F + G >= 0 && -10 + C + G >= 0 && 10 + -1*C + G >= 0 && -1 + B + G >= 0 && 1 + -1*B + G >= 0 && 1 + -1*A + G >= 0 && F >= 0 && -10 + C + F >= 0 && 10 + -1*C + F >= 0 && -1 + B + F >= 0 && 1 + -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && 10 + -1*C >= 0 && 9 + B + -1*C >= 0 && 11 + -1*B + -1*C >= 0 && 11 + -1*A + -1*C >= 0 && -10 + C >= 0 && -11 + B + C >= 0 && -9 + -1*B + C >= 0 && -9 + -1*A + C >= 0 && 1 + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && -1 + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && G >= 1 && C >= 1 + H] f33(A,B,C,D,E,F,G,H,I,J,K,L) -> f44(A,B,C,D,E,F,G,H,I,J,K,L) [H >= 0 && G + H >= 0 && -1*G + H >= 0 && F + H >= 0 && -10 + C + H >= 0 && 10 + -1*C + H >= 0 && -1 + B + H >= 0 && 1 + -1*B + H >= 0 && 1 + -1*A + H >= 0 && G >= 0 && F + G >= 0 && -10 + C + G >= 0 && 10 + -1*C + G >= 0 && -1 + B + G >= 0 && 1 + -1*B + G >= 0 && 1 + -1*A + G >= 0 && F >= 0 && -10 + C + F >= 0 && 10 + -1*C + F >= 0 && -1 + B + F >= 0 && 1 + -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && 10 + -1*C >= 0 && 9 + B + -1*C >= 0 && 11 + -1*B + -1*C >= 0 && 11 + -1*A + -1*C >= 0 && -10 + C >= 0 && -11 + B + C >= 0 && -9 + -1*B + C >= 0 && -9 + -1*A + C >= 0 && 1 + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && -1 + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && 0 >= 1 + A && H >= C] f33(A,B,C,D,E,F,G,H,I,J,K,L) -> f44(A,B,C,D,E,F,G,H,I,J,K,L) [H >= 0 && G + H >= 0 && -1*G + H >= 0 && F + H >= 0 && -10 + C + H >= 0 && 10 + -1*C + H >= 0 && -1 + B + H >= 0 && 1 + -1*B + H >= 0 && 1 + -1*A + H >= 0 && G >= 0 && F + G >= 0 && -10 + C + G >= 0 && 10 + -1*C + G >= 0 && -1 + B + G >= 0 && 1 + -1*B + G >= 0 && 1 + -1*A + G >= 0 && F >= 0 && -10 + C + F >= 0 && 10 + -1*C + F >= 0 && -1 + B + F >= 0 && 1 + -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && 10 + -1*C >= 0 && 9 + B + -1*C >= 0 && 11 + -1*B + -1*C >= 0 && 11 + -1*A + -1*C >= 0 && -10 + C >= 0 && -11 + B + C >= 0 && -9 + -1*B + C >= 0 && -9 + -1*A + C >= 0 && 1 + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && -1 + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && A >= 1 && H >= C] f33(A,B,C,D,E,F,G,H,I,J,K,L) -> f29(0,B,C,D,E,1 + F,G,H,I,0,K,L) [H >= 0 && G + H >= 0 && -1*G + H >= 0 && F + H >= 0 && -10 + C + H >= 0 && 10 + -1*C + H >= 0 && -1 + B + H >= 0 && 1 + -1*B + H >= 0 && 1 + -1*A + H >= 0 && G >= 0 && F + G >= 0 && -10 + C + G >= 0 && 10 + -1*C + G >= 0 && -1 + B + G >= 0 && 1 + -1*B + G >= 0 && 1 + -1*A + G >= 0 && F >= 0 && -10 + C + F >= 0 && 10 + -1*C + F >= 0 && -1 + B + F >= 0 && 1 + -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && 10 + -1*C >= 0 && 9 + B + -1*C >= 0 && 11 + -1*B + -1*C >= 0 && 11 + -1*A + -1*C >= 0 && -10 + C >= 0 && -11 + B + C >= 0 && -9 + -1*B + C >= 0 && -9 + -1*A + C >= 0 && 1 + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && -1 + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && H >= C && A = 0] f33(A,B,C,D,E,F,G,H,I,J,K,L) -> f33(A,B,C,D,E,F,1,1 + H,1,J,K,L) [H >= 0 && G + H >= 0 && -1*G + H >= 0 && F + H >= 0 && -10 + C + H >= 0 && 10 + -1*C + H >= 0 && -1 + B + H >= 0 && 1 + -1*B + H >= 0 && 1 + -1*A + H >= 0 && G >= 0 && F + G >= 0 && -10 + C + G >= 0 && 10 + -1*C + G >= 0 && -1 + B + G >= 0 && 1 + -1*B + G >= 0 && 1 + -1*A + G >= 0 && F >= 0 && -10 + C + F >= 0 && 10 + -1*C + F >= 0 && -1 + B + F >= 0 && 1 + -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && 10 + -1*C >= 0 && 9 + B + -1*C >= 0 && 11 + -1*B + -1*C >= 0 && 11 + -1*A + -1*C >= 0 && -10 + C >= 0 && -11 + B + C >= 0 && -9 + -1*B + C >= 0 && -9 + -1*A + C >= 0 && 1 + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && -1 + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && C >= 1 + H && G = 0] f33(A,B,C,D,E,F,G,H,I,J,K,L) -> f33(A,B,C,D,E,F,0,1 + H,0,J,K,L) [H >= 0 && G + H >= 0 && -1*G + H >= 0 && F + H >= 0 && -10 + C + H >= 0 && 10 + -1*C + H >= 0 && -1 + B + H >= 0 && 1 + -1*B + H >= 0 && 1 + -1*A + H >= 0 && G >= 0 && F + G >= 0 && -10 + C + G >= 0 && 10 + -1*C + G >= 0 && -1 + B + G >= 0 && 1 + -1*B + G >= 0 && 1 + -1*A + G >= 0 && F >= 0 && -10 + C + F >= 0 && 10 + -1*C + F >= 0 && -1 + B + F >= 0 && 1 + -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && 10 + -1*C >= 0 && 9 + B + -1*C >= 0 && 11 + -1*B + -1*C >= 0 && 11 + -1*A + -1*C >= 0 && -10 + C >= 0 && -11 + B + C >= 0 && -9 + -1*B + C >= 0 && -9 + -1*A + C >= 0 && 1 + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && -1 + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && M >= 1 + N && C >= 1 + H && G = 0] f33(A,B,C,D,E,F,G,H,I,J,K,L) -> f33(A,B,C,D,E,F,0,1 + H,0,J,K,L) [H >= 0 && G + H >= 0 && -1*G + H >= 0 && F + H >= 0 && -10 + C + H >= 0 && 10 + -1*C + H >= 0 && -1 + B + H >= 0 && 1 + -1*B + H >= 0 && 1 + -1*A + H >= 0 && G >= 0 && F + G >= 0 && -10 + C + G >= 0 && 10 + -1*C + G >= 0 && -1 + B + G >= 0 && 1 + -1*B + G >= 0 && 1 + -1*A + G >= 0 && F >= 0 && -10 + C + F >= 0 && 10 + -1*C + F >= 0 && -1 + B + F >= 0 && 1 + -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && 10 + -1*C >= 0 && 9 + B + -1*C >= 0 && 11 + -1*B + -1*C >= 0 && 11 + -1*A + -1*C >= 0 && -10 + C >= 0 && -11 + B + C >= 0 && -9 + -1*B + C >= 0 && -9 + -1*A + C >= 0 && 1 + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && -1 + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && C >= 1 + H && G = 0] f29(A,B,C,D,E,F,G,H,I,J,K,L) -> f33(A,B,C,D,E,F,0,0,I,J,K,L) [F >= 0 && -10 + C + F >= 0 && 10 + -1*C + F >= 0 && -1 + B + F >= 0 && 1 + -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && 10 + -1*C >= 0 && 9 + B + -1*C >= 0 && 11 + -1*B + -1*C >= 0 && 10 + A + -1*C >= 0 && 11 + -1*A + -1*C >= 0 && -10 + C >= 0 && -11 + B + C >= 0 && -9 + -1*B + C >= 0 && -10 + A + C >= 0 && -9 + -1*A + C >= 0 && 1 + -1*B >= 0 && 1 + A + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && A >= 0 && C >= 1 + F] f23(A,B,C,D,E,F,G,H,I,J,K,L) -> f29(A,B,C,D,E,0,G,H,I,J,K,L) [F >= 0 && -10 + C + F >= 0 && 10 + -1*C + F >= 0 && -1 + B + F >= 0 && 1 + -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && 10 + -1*C >= 0 && 9 + B + -1*C >= 0 && 11 + -1*B + -1*C >= 0 && 9 + A + -1*C >= 0 && 11 + -1*A + -1*C >= 0 && -10 + C >= 0 && -11 + B + C >= 0 && -9 + -1*B + C >= 0 && -11 + A + C >= 0 && -9 + -1*A + C >= 0 && 1 + -1*B >= 0 && A + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && F >= C] f23(A,B,C,D,E,F,G,H,I,J,K,L) -> f23(A,B,C,D,E,1 + F,G,H,I,J,K,L) [F >= 0 && -10 + C + F >= 0 && 10 + -1*C + F >= 0 && -1 + B + F >= 0 && 1 + -1*B + F >= 0 && -1 + A + F >= 0 && 1 + -1*A + F >= 0 && 10 + -1*C >= 0 && 9 + B + -1*C >= 0 && 11 + -1*B + -1*C >= 0 && 9 + A + -1*C >= 0 && 11 + -1*A + -1*C >= 0 && -10 + C >= 0 && -11 + B + C >= 0 && -9 + -1*B + C >= 0 && -11 + A + C >= 0 && -9 + -1*A + C >= 0 && 1 + -1*B >= 0 && A + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && C >= 1 + F] f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f23(1,1,10,M,N,0,G,H,I,J,K,L) True Signature: {(f0,12);(f23,12);(f29,12);(f33,12);(f44,12);(f52,12);(f55,12);(f63,12);(f71,12)} Rule Graph: [0->{},1->{},2->{},3->{3,4,5},4->{0,1,2},5->{},6->{4,5,8},7->{3,4,5},8->{6,7},9->{11,19},10->{11,19} ,11->{8},12->{12,13,14,15},13->{9,10},14->{9,10},15->{11,19},16->{12,13,14,15},17->{13,14,15,16,17,18} ,18->{13,14,15,16,17,18},19->{16,17,18},20->{19},21->{20,21},22->{21}] ,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] | +- p:[21] c: [21] | +- p:[9,13,12,16,17,18,19,10,14,15] c: [9,10,13,14,15,19] | | | +- p:[17,18] c: [18] | | | | | `- p:[17] c: [17] | | | `- p:[12] c: [12] | +- p:[6,8] c: [6,8] | `- p:[3] c: [3]) + Applied Processor: CloseWith True + Details: () YES