YES(?,O(1)) * Step 1: ArgumentFilter WORST_CASE(?,O(1)) + 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: ArgumentFilter [3,4,8,9,10,11] + Details: We remove following argument positions: [3,4,8,9,10,11]. * Step 2: UnsatPaths WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. f63(A,B,C,F,G,H) -> f71(A,B,C,F,G,H) [-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,F,G,H) -> f71(A,B,C,F,G,H) [-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,F,G,H) -> f71(A,0,C,F,G,H) [-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,F,G,H) -> f52(A,0,C,1 + F,G,H) [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,F,G,H) -> f63(A,B,C,F,G,H) [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,F,G,H) -> f71(0,B,C,F,G,H) [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,F,G,H) -> f52(A,1,C,1 + F,G,H) [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,F,G,H) -> f52(A,0,C,1 + F,G,H) [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,F,G,H) -> f55(A,B,C,F,G,H) [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,F,G,H) -> f29(1,B,C,1 + F,G,H) [-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,F,G,H) -> f29(0,B,C,1 + F,0,H) [-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,F,G,H) -> f52(A,B,C,0,G,H) [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,F,G,H) -> f33(A,B,C,F,1,1 + H) [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,F,G,H) -> f44(A,B,C,F,G,H) [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,F,G,H) -> f44(A,B,C,F,G,H) [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,F,G,H) -> f29(0,B,C,1 + F,G,H) [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,F,G,H) -> f33(A,B,C,F,1,1 + H) [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,F,G,H) -> f33(A,B,C,F,0,1 + H) [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,F,G,H) -> f33(A,B,C,F,0,1 + H) [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,F,G,H) -> f33(A,B,C,F,0,0) [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,F,G,H) -> f29(A,B,C,0,G,H) [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,F,G,H) -> f23(A,B,C,1 + F,G,H) [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,F,G,H) -> f23(1,1,10,0,G,H) 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 3: FromIts WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. f63(A,B,C,F,G,H) -> f71(A,B,C,F,G,H) [-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,F,G,H) -> f71(A,B,C,F,G,H) [-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,F,G,H) -> f71(A,0,C,F,G,H) [-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,F,G,H) -> f52(A,0,C,1 + F,G,H) [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,F,G,H) -> f63(A,B,C,F,G,H) [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,F,G,H) -> f71(0,B,C,F,G,H) [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,F,G,H) -> f52(A,1,C,1 + F,G,H) [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,F,G,H) -> f52(A,0,C,1 + F,G,H) [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,F,G,H) -> f55(A,B,C,F,G,H) [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,F,G,H) -> f29(1,B,C,1 + F,G,H) [-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,F,G,H) -> f29(0,B,C,1 + F,0,H) [-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,F,G,H) -> f52(A,B,C,0,G,H) [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,F,G,H) -> f33(A,B,C,F,1,1 + H) [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,F,G,H) -> f44(A,B,C,F,G,H) [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,F,G,H) -> f44(A,B,C,F,G,H) [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,F,G,H) -> f29(0,B,C,1 + F,G,H) [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,F,G,H) -> f33(A,B,C,F,1,1 + H) [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,F,G,H) -> f33(A,B,C,F,0,1 + H) [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,F,G,H) -> f33(A,B,C,F,0,1 + H) [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,F,G,H) -> f33(A,B,C,F,0,0) [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,F,G,H) -> f29(A,B,C,0,G,H) [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,F,G,H) -> f23(A,B,C,1 + F,G,H) [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,F,G,H) -> f23(1,1,10,0,G,H) 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 4: AddSinks WORST_CASE(?,O(1)) + Considered Problem: Rules: f63(A,B,C,F,G,H) -> f71(A,B,C,F,G,H) [-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,F,G,H) -> f71(A,B,C,F,G,H) [-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,F,G,H) -> f71(A,0,C,F,G,H) [-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,F,G,H) -> f52(A,0,C,1 + F,G,H) [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,F,G,H) -> f63(A,B,C,F,G,H) [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,F,G,H) -> f71(0,B,C,F,G,H) [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,F,G,H) -> f52(A,1,C,1 + F,G,H) [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,F,G,H) -> f52(A,0,C,1 + F,G,H) [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,F,G,H) -> f55(A,B,C,F,G,H) [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,F,G,H) -> f29(1,B,C,1 + F,G,H) [-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,F,G,H) -> f29(0,B,C,1 + F,0,H) [-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,F,G,H) -> f52(A,B,C,0,G,H) [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,F,G,H) -> f33(A,B,C,F,1,1 + H) [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,F,G,H) -> f44(A,B,C,F,G,H) [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,F,G,H) -> f44(A,B,C,F,G,H) [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,F,G,H) -> f29(0,B,C,1 + F,G,H) [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,F,G,H) -> f33(A,B,C,F,1,1 + H) [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,F,G,H) -> f33(A,B,C,F,0,1 + H) [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,F,G,H) -> f33(A,B,C,F,0,1 + H) [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,F,G,H) -> f33(A,B,C,F,0,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 && 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,F,G,H) -> f29(A,B,C,0,G,H) [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,F,G,H) -> f23(A,B,C,1 + F,G,H) [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,F,G,H) -> f23(1,1,10,0,G,H) 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: AddSinks + Details: () * Step 5: Decompose WORST_CASE(?,O(1)) + Considered Problem: Rules: f63(A,B,C,F,G,H) -> f71(A,B,C,F,G,H) [-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,F,G,H) -> f71(A,B,C,F,G,H) [-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,F,G,H) -> f71(A,0,C,F,G,H) [-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,F,G,H) -> f52(A,0,C,1 + F,G,H) [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,F,G,H) -> f63(A,B,C,F,G,H) [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,F,G,H) -> f71(0,B,C,F,G,H) [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,F,G,H) -> f52(A,1,C,1 + F,G,H) [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,F,G,H) -> f52(A,0,C,1 + F,G,H) [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,F,G,H) -> f55(A,B,C,F,G,H) [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,F,G,H) -> f29(1,B,C,1 + F,G,H) [-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,F,G,H) -> f29(0,B,C,1 + F,0,H) [-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,F,G,H) -> f52(A,B,C,0,G,H) [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,F,G,H) -> f33(A,B,C,F,1,1 + H) [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,F,G,H) -> f44(A,B,C,F,G,H) [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,F,G,H) -> f44(A,B,C,F,G,H) [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,F,G,H) -> f29(0,B,C,1 + F,G,H) [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,F,G,H) -> f33(A,B,C,F,1,1 + H) [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,F,G,H) -> f33(A,B,C,F,0,1 + H) [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,F,G,H) -> f33(A,B,C,F,0,1 + H) [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,F,G,H) -> f33(A,B,C,F,0,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 && 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,F,G,H) -> f29(A,B,C,0,G,H) [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,F,G,H) -> f23(A,B,C,1 + F,G,H) [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,F,G,H) -> f23(1,1,10,0,G,H) True f71(A,B,C,F,G,H) -> exitus616(A,B,C,F,G,H) True f71(A,B,C,F,G,H) -> exitus616(A,B,C,F,G,H) True f71(A,B,C,F,G,H) -> exitus616(A,B,C,F,G,H) True f71(A,B,C,F,G,H) -> exitus616(A,B,C,F,G,H) True Signature: {(exitus616,6);(f0,12);(f23,12);(f29,12);(f33,12);(f44,12);(f52,12);(f55,12);(f63,12);(f71,12)} Rule Graph: [0->{26},1->{25},2->{24},3->{3,4,5},4->{0,1,2},5->{23},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 Greedy + 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] | +- 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: [17,18] | | | `- p:[12] c: [12] | +- p:[6,8] c: [6,8] | `- p:[3] c: [3] * Step 6: AbstractSize WORST_CASE(?,O(1)) + Considered Problem: (Rules: f63(A,B,C,F,G,H) -> f71(A,B,C,F,G,H) [-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,F,G,H) -> f71(A,B,C,F,G,H) [-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,F,G,H) -> f71(A,0,C,F,G,H) [-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,F,G,H) -> f52(A,0,C,1 + F,G,H) [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,F,G,H) -> f63(A,B,C,F,G,H) [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,F,G,H) -> f71(0,B,C,F,G,H) [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,F,G,H) -> f52(A,1,C,1 + F,G,H) [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,F,G,H) -> f52(A,0,C,1 + F,G,H) [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,F,G,H) -> f55(A,B,C,F,G,H) [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,F,G,H) -> f29(1,B,C,1 + F,G,H) [-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,F,G,H) -> f29(0,B,C,1 + F,0,H) [-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,F,G,H) -> f52(A,B,C,0,G,H) [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,F,G,H) -> f33(A,B,C,F,1,1 + H) [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,F,G,H) -> f44(A,B,C,F,G,H) [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,F,G,H) -> f44(A,B,C,F,G,H) [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,F,G,H) -> f29(0,B,C,1 + F,G,H) [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,F,G,H) -> f33(A,B,C,F,1,1 + H) [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,F,G,H) -> f33(A,B,C,F,0,1 + H) [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,F,G,H) -> f33(A,B,C,F,0,1 + H) [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,F,G,H) -> f33(A,B,C,F,0,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 && 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,F,G,H) -> f29(A,B,C,0,G,H) [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,F,G,H) -> f23(A,B,C,1 + F,G,H) [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,F,G,H) -> f23(1,1,10,0,G,H) True f71(A,B,C,F,G,H) -> exitus616(A,B,C,F,G,H) True f71(A,B,C,F,G,H) -> exitus616(A,B,C,F,G,H) True f71(A,B,C,F,G,H) -> exitus616(A,B,C,F,G,H) True f71(A,B,C,F,G,H) -> exitus616(A,B,C,F,G,H) True Signature: {(exitus616,6);(f0,12);(f23,12);(f29,12);(f33,12);(f44,12);(f52,12);(f55,12);(f63,12);(f71,12)} Rule Graph: [0->{26},1->{25},2->{24},3->{3,4,5},4->{0,1,2},5->{23},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,23,24,25,26] | +- 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: [17,18] | | | `- p:[12] c: [12] | +- p:[6,8] c: [6,8] | `- p:[3] c: [3]) + Applied Processor: AbstractSize Minimize + Details: () * Step 7: AbstractFlow WORST_CASE(?,O(1)) + Considered Problem: Program: Domain: [A,B,C,F,G,H,0.0,0.1,0.1.0,0.1.1,0.2,0.3] f63 ~> f71 [A <= A, B <= B, C <= C, F <= F, G <= G, H <= H] f63 ~> f71 [A <= A, B <= B, C <= C, F <= F, G <= G, H <= H] f63 ~> f71 [A <= A, B <= 0*K, C <= C, F <= F, G <= G, H <= H] f52 ~> f52 [A <= A, B <= 0*K, C <= C, F <= 9*K, G <= G, H <= H] f52 ~> f63 [A <= A, B <= B, C <= C, F <= F, G <= G, H <= H] f52 ~> f71 [A <= 0*K, B <= B, C <= C, F <= F, G <= G, H <= H] f55 ~> f52 [A <= A, B <= K, C <= C, F <= 9*K, G <= G, H <= H] f55 ~> f52 [A <= A, B <= 0*K, C <= C, F <= 9*K, G <= G, H <= H] f52 ~> f55 [A <= A, B <= B, C <= C, F <= F, G <= G, H <= H] f44 ~> f29 [A <= K, B <= B, C <= C, F <= F + H, G <= G, H <= H] f44 ~> f29 [A <= 0*K, B <= B, C <= C, F <= F + H, G <= 0*K, H <= H] f29 ~> f52 [A <= A, B <= B, C <= C, F <= 0*K, G <= G, H <= H] f33 ~> f33 [A <= A, B <= B, C <= C, F <= F, G <= K, H <= 10*K] f33 ~> f44 [A <= A, B <= B, C <= C, F <= F, G <= G, H <= H] f33 ~> f44 [A <= A, B <= B, C <= C, F <= F, G <= G, H <= H] f33 ~> f29 [A <= 0*K, B <= B, C <= C, F <= F + H, G <= G, H <= H] f33 ~> f33 [A <= A, B <= B, C <= C, F <= F, G <= K, H <= 10*K] f33 ~> f33 [A <= A, B <= B, C <= C, F <= F, G <= 0*K, H <= 10*K] f33 ~> f33 [A <= A, B <= B, C <= C, F <= F, G <= 0*K, H <= 10*K] f29 ~> f33 [A <= A, B <= B, C <= C, F <= F, G <= 0*K, H <= 0*K] f23 ~> f29 [A <= A, B <= B, C <= C, F <= 0*K, G <= G, H <= H] f23 ~> f23 [A <= A, B <= B, C <= C, F <= 10*K, G <= G, H <= H] f0 ~> f23 [A <= K, B <= K, C <= 10*K, F <= 0*K, G <= G, H <= H] f71 ~> exitus616 [A <= A, B <= B, C <= C, F <= F, G <= G, H <= H] f71 ~> exitus616 [A <= A, B <= B, C <= C, F <= F, G <= G, H <= H] f71 ~> exitus616 [A <= A, B <= B, C <= C, F <= F, G <= G, H <= H] f71 ~> exitus616 [A <= A, B <= B, C <= C, F <= F, G <= G, H <= H] + Loop: [0.0 <= K + C + F] f23 ~> f23 [A <= A, B <= B, C <= C, F <= 10*K, G <= G, H <= H] + Loop: [0.1 <= 9*K + F] f44 ~> f29 [A <= K, B <= B, C <= C, F <= F + H, G <= G, H <= H] f33 ~> f44 [A <= A, B <= B, C <= C, F <= F, G <= G, H <= H] f33 ~> f33 [A <= A, B <= B, C <= C, F <= F, G <= K, H <= 10*K] f33 ~> f33 [A <= A, B <= B, C <= C, F <= F, G <= K, H <= 10*K] f33 ~> f33 [A <= A, B <= B, C <= C, F <= F, G <= 0*K, H <= 10*K] f33 ~> f33 [A <= A, B <= B, C <= C, F <= F, G <= 0*K, H <= 10*K] f29 ~> f33 [A <= A, B <= B, C <= C, F <= F, G <= 0*K, H <= 0*K] f44 ~> f29 [A <= 0*K, B <= B, C <= C, F <= F + H, G <= 0*K, H <= H] f33 ~> f44 [A <= A, B <= B, C <= C, F <= F, G <= G, H <= H] f33 ~> f29 [A <= 0*K, B <= B, C <= C, F <= F + H, G <= G, H <= H] + Loop: [0.1.0 <= K + C + H] f33 ~> f33 [A <= A, B <= B, C <= C, F <= F, G <= 0*K, H <= 10*K] f33 ~> f33 [A <= A, B <= B, C <= C, F <= F, G <= 0*K, H <= 10*K] + Loop: [0.1.1 <= K + C + H] f33 ~> f33 [A <= A, B <= B, C <= C, F <= F, G <= K, H <= 10*K] + Loop: [0.2 <= 2*K + C + F] f55 ~> f52 [A <= A, B <= K, C <= C, F <= 9*K, G <= G, H <= H] f52 ~> f55 [A <= A, B <= B, C <= C, F <= F, G <= G, H <= H] + Loop: [0.3 <= 2*K + C + F] f52 ~> f52 [A <= A, B <= 0*K, C <= C, F <= 9*K, G <= G, H <= H] + Applied Processor: AbstractFlow + Details: () * Step 8: Lare WORST_CASE(?,O(1)) + Considered Problem: Program: Domain: [tick,huge,K,A,B,C,F,G,H,0.0,0.1,0.1.0,0.1.1,0.2,0.3] f63 ~> f71 [] f63 ~> f71 [] f63 ~> f71 [K ~=> B] f52 ~> f52 [K ~=> B,K ~=> F] f52 ~> f63 [] f52 ~> f71 [K ~=> A] f55 ~> f52 [K ~=> B,K ~=> F] f55 ~> f52 [K ~=> B,K ~=> F] f52 ~> f55 [] f44 ~> f29 [K ~=> A,F ~+> F,H ~+> F] f44 ~> f29 [K ~=> A,K ~=> G,F ~+> F,H ~+> F] f29 ~> f52 [K ~=> F] f33 ~> f33 [K ~=> G,K ~=> H] f33 ~> f44 [] f33 ~> f44 [] f33 ~> f29 [K ~=> A,F ~+> F,H ~+> F] f33 ~> f33 [K ~=> G,K ~=> H] f33 ~> f33 [K ~=> G,K ~=> H] f33 ~> f33 [K ~=> G,K ~=> H] f29 ~> f33 [K ~=> G,K ~=> H] f23 ~> f29 [K ~=> F] f23 ~> f23 [K ~=> F] f0 ~> f23 [K ~=> A,K ~=> B,K ~=> C,K ~=> F] f71 ~> exitus616 [] f71 ~> exitus616 [] f71 ~> exitus616 [] f71 ~> exitus616 [] + Loop: [C ~+> 0.0,F ~+> 0.0,K ~+> 0.0] f23 ~> f23 [K ~=> F] + Loop: [F ~+> 0.1,K ~*> 0.1] f44 ~> f29 [K ~=> A,F ~+> F,H ~+> F] f33 ~> f44 [] f33 ~> f33 [K ~=> G,K ~=> H] f33 ~> f33 [K ~=> G,K ~=> H] f33 ~> f33 [K ~=> G,K ~=> H] f33 ~> f33 [K ~=> G,K ~=> H] f29 ~> f33 [K ~=> G,K ~=> H] f44 ~> f29 [K ~=> A,K ~=> G,F ~+> F,H ~+> F] f33 ~> f44 [] f33 ~> f29 [K ~=> A,F ~+> F,H ~+> F] + Loop: [C ~+> 0.1.0,H ~+> 0.1.0,K ~+> 0.1.0] f33 ~> f33 [K ~=> G,K ~=> H] f33 ~> f33 [K ~=> G,K ~=> H] + Loop: [C ~+> 0.1.1,H ~+> 0.1.1,K ~+> 0.1.1] f33 ~> f33 [K ~=> G,K ~=> H] + Loop: [C ~+> 0.2,F ~+> 0.2,K ~*> 0.2] f55 ~> f52 [K ~=> B,K ~=> F] f52 ~> f55 [] + Loop: [C ~+> 0.3,F ~+> 0.3,K ~*> 0.3] f52 ~> f52 [K ~=> B,K ~=> F] + Applied Processor: Lare + Details: f0 ~> exitus616 [K ~=> A ,K ~=> B ,K ~=> C ,K ~=> F ,K ~=> G ,K ~=> H ,tick ~+> tick ,K ~+> 0.0 ,K ~+> 0.1 ,K ~+> 0.1.0 ,K ~+> 0.1.1 ,K ~+> 0.2 ,K ~+> 0.3 ,K ~+> tick ,K ~*> 0.0 ,K ~*> 0.1 ,K ~*> 0.1.0 ,K ~*> 0.1.1 ,K ~*> 0.2 ,K ~*> 0.3 ,K ~*> tick] f0 ~> f55 [K ~=> A ,K ~=> B ,K ~=> C ,K ~=> F ,K ~=> G ,K ~=> H ,tick ~+> tick ,K ~+> 0.0 ,K ~+> 0.1 ,K ~+> 0.1.0 ,K ~+> 0.1.1 ,K ~+> 0.2 ,K ~+> 0.3 ,K ~+> tick ,K ~*> 0.0 ,K ~*> 0.1 ,K ~*> 0.1.0 ,K ~*> 0.1.1 ,K ~*> 0.2 ,K ~*> 0.3 ,K ~*> tick] + f23> [K ~=> F,C ~+> 0.0,C ~+> tick,F ~+> 0.0,F ~+> tick,tick ~+> tick,K ~+> 0.0,K ~+> tick] + f29> [K ~=> A ,K ~=> G ,K ~=> H ,C ~+> 0.1.0 ,C ~+> 0.1.1 ,C ~+> tick ,F ~+> F ,F ~+> 0.1 ,F ~+> tick ,tick ~+> tick ,K ~+> F ,K ~+> 0.1.0 ,K ~+> 0.1.1 ,K ~+> tick ,C ~*> tick ,F ~*> F ,F ~*> tick ,K ~*> F ,K ~*> 0.1 ,K ~*> 0.1.0 ,K ~*> 0.1.1 ,K ~*> tick] + f33> [K ~=> G ,K ~=> H ,C ~+> 0.1.0 ,C ~+> tick ,H ~+> 0.1.0 ,H ~+> tick ,tick ~+> tick ,K ~+> 0.1.0 ,K ~+> tick] + f33> [K ~=> G ,K ~=> H ,C ~+> 0.1.1 ,C ~+> tick ,H ~+> 0.1.1 ,H ~+> tick ,tick ~+> tick ,K ~+> 0.1.1 ,K ~+> tick] + f52> [K ~=> B ,K ~=> F ,C ~+> 0.2 ,C ~+> tick ,F ~+> 0.2 ,F ~+> tick ,tick ~+> tick ,K ~*> 0.2 ,K ~*> tick] f55> [K ~=> B ,K ~=> F ,C ~+> 0.2 ,C ~+> tick ,F ~+> 0.2 ,F ~+> tick ,tick ~+> tick ,K ~*> 0.2 ,K ~*> tick] + f52> [K ~=> B ,K ~=> F ,C ~+> 0.3 ,C ~+> tick ,F ~+> 0.3 ,F ~+> tick ,tick ~+> tick ,K ~*> 0.3 ,K ~*> tick] YES(?,O(1))