YES(?,PRIMREC) * Step 1: ArgumentFilter MAYBE + Considered Problem: Rules: 0. start(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) True (1,1) 1. f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [B >= 1 + A && C >= 1] (?,1) 2. f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [B >= 1 + A && 0 >= C] (?,1) 3. f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f2(A,1 + B,E1,D1,E1,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [A >= B && D1 >= 1 + C] (?,1) 4. f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f2(A,1 + B,C,D1,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [A >= B && C >= D1] (?,1) 5. f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f26(A,B,C,D,E,F,G,H,1,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [-1 + C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A] (?,1) 6. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [1 + -1*I >= 0 && -1 + -1*A + B >= 0 && J >= 201] (?,1) 7. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f30(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [1 + -1*I >= 0 && -1 + -1*A + B >= 0 && I >= 1 && 200 >= J] (?,1) 8. f30(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f42(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] (?,1) 9. f42(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f68(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && L >= A] (?,1) 10. f42(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f42(A,B,C,D,E,F,G,H,I,J,K,1 + L,0,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && A >= 1 + L] (?,1) 11. f42(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f47(A,B,C,D,E,F,G,H,I,J,K,L,D1,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && A >= 1 + L && D1 >= 1] (?,1) 12. f42(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f47(A,B,C,D,E,F,G,H,I,J,K,L,D1,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [1 + -1*I >= 0 (?,1) && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && A >= 1 + L && 0 >= 1 + D1] 13. f68(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f152(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [1 + -1*I >= 0 (?,1) && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && -1*A + L >= 0 && 200 + -1*J >= 0 && B >= 1 + A] 14. f47(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f42(A,B,C,D,E,F,G,H,I,J,K,1 + L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [1 + -1*I >= 0 (?,1) && 201 + -1*I + -1*J >= 0 && -2 + B + -1*L >= 0 && -1 + -1*A + B >= 0 && -1 + A + -1*L >= 0 && 200 + -1*J >= 0 && K >= 1 + A] 15. f47(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f51(A,B,C,D,E,F,G,0,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [1 + -1*I >= 0 (?,1) && 201 + -1*I + -1*J >= 0 && -2 + B + -1*L >= 0 && -1 + -1*A + B >= 0 && -1 + A + -1*L >= 0 && 200 + -1*J >= 0 && A >= K] 16. f152(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f164(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] (?,1) 17. f51(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f58(A,B,C,D,E,F,G,D1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [1 + -1*I >= 0 (?,1) && 1 + H + -1*I >= 0 && 1 + -1*H + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1*H >= 0 && 200 + -1*H + -1*J >= 0 && H >= 0 && 200 + H + -1*J >= 0 && -2 + B + -1*L >= 0 && -1 + B + -1*K >= 0 && -1 + -1*A + B >= 0 && -1 + A + -1*L >= 0 && A + -1*K >= 0 && 200 + -1*J >= 0 && B >= 1 + A] 18. f58(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f47(A,B,C,D,E,F,G,H,I,J,1 + K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [1 + -1*I >= 0 (?,1) && 201 + -1*I + -1*J >= 0 && -2 + B + -1*L >= 0 && -1 + B + -1*K >= 0 && -1 + -1*A + B >= 0 && -1 + A + -1*L >= 0 && A + -1*K >= 0 && 200 + -1*J >= 0 && B >= 1 + A] 19. f164(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f176(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && 200 + -1*J >= 0 && 0 >= B] (?,1) 20. f164(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f167(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && 200 + -1*J >= 0 && B >= 1] (?,1) 21. f176(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f184(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,D1,Z,A1,B1,C1) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && 200 + -1*J >= 0 && B >= 1 + A] (?,1) 22. f176(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f176(A,1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && 200 + -1*J >= 0 && A >= B] (?,1) 23. f167(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f164(A,-1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [1 + -1*I >= 0 (?,1) && B + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + B >= 0 && 199 + B + -1*J >= 0 && 200 + -1*J >= 0 && K >= 1 + B] 24. f167(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f167(A,B,C,D,E,F,G,D1,I,J,1 + K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [1 + -1*I >= 0 (?,1) && B + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + B >= 0 && 199 + B + -1*J >= 0 && 200 + -1*J >= 0 && B >= K] 25. f184(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f199(A,B,0,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] (?,1) 26. f199(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f218(A,B,0,D,E,F,G,H,0,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,0,Y,Z,A1,B1,C1) [1 + -1*I >= 0 (?,1) && 1 + C + -1*I >= 0 && 1 + -1*C + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1*C >= 0 && 200 + -1*C + -1*J >= 0 && C >= 0 && 200 + C + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] 27. f199(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f210(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,D1,Y,Z,A1,B1,C1) [1 + -1*I >= 0 (?,1) && 1 + C + -1*I >= 0 && 1 + -1*C + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1*C >= 0 && 200 + -1*C + -1*J >= 0 && C >= 0 && 200 + C + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A && D1 >= 1] 28. f199(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f210(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,D1,Y,Z,A1,B1,C1) [1 + -1*I >= 0 (?,1) && 1 + C + -1*I >= 0 && 1 + -1*C + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1*C >= 0 && 200 + -1*C + -1*J >= 0 && C >= 0 && 200 + C + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A && 0 >= 1 + D1] 29. f218(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f26(A,B,C,D,E,F,G,H,I,1 + J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [-1*I >= 0 (?,1) && C + -1*I >= 0 && -1*C + -1*I >= 0 && -1*I + X >= 0 && -1*I + -1*X >= 0 && 200 + -1*I + -1*J >= 0 && I >= 0 && C + I >= 0 && -1*C + I >= 0 && I + X >= 0 && I + -1*X >= 0 && 200 + I + -1*J >= 0 && -1*C >= 0 && -1*C + X >= 0 && -1*C + -1*X >= 0 && 200 + -1*C + -1*J >= 0 && C >= 0 && C + X >= 0 && C + -1*X >= 0 && 200 + C + -1*J >= 0 && -1*X >= 0 && 200 + -1*J + -1*X >= 0 && X >= 0 && 200 + -1*J + X >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] 30. f210(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f26(A,B,C,D,E,F,G,H,I,1 + J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [1 + -1*I >= 0 (?,1) && 1 + C + -1*I >= 0 && 1 + -1*C + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1*C >= 0 && 200 + -1*C + -1*J >= 0 && C >= 0 && 200 + C + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] 31. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f81(A,B,C,D,E,F,G,H,0,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [1 + -1*I >= 0 && -1 + -1*A + B >= 0 && 200 >= J && I = 0] (?,1) 32. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f30(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [1 + -1*I >= 0 && -1 + -1*A + B >= 0 && 0 >= 1 + I && 200 >= J] (?,1) 33. f81(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f87(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [-1*I >= 0 (?,1) && 200 + -1*I + -1*J >= 0 && I >= 0 && 200 + I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] 34. f87(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f100(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,1,A1,B1,C1) [-1*I >= 0 (?,1) && 200 + -1*I + -1*J >= 0 && I >= 0 && 200 + I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] 35. f100(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) -> f152(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1) [-1*I >= 0 (?,1) && -1 + -1*I + Z >= 0 && 1 + -1*I + -1*Z >= 0 && 200 + -1*I + -1*J >= 0 && I >= 0 && -1 + I + Z >= 0 && 1 + I + -1*Z >= 0 && 200 + I + -1*J >= 0 && 1 + -1*Z >= 0 && 201 + -1*J + -1*Z >= 0 && -1 + Z >= 0 && 199 + -1*J + Z >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A && Z >= 1] Signature: {(f1,29) ;(f100,29) ;(f15,29) ;(f152,29) ;(f164,29) ;(f167,29) ;(f176,29) ;(f184,29) ;(f199,29) ;(f2,29) ;(f210,29) ;(f218,29) ;(f26,29) ;(f30,29) ;(f42,29) ;(f47,29) ;(f51,29) ;(f58,29) ;(f68,29) ;(f81,29) ;(f87,29) ;(start,29)} Flow Graph: [0->{1,2,3,4},1->{5},2->{},3->{1,2,3,4},4->{1,2,3,4},5->{6,7,31,32},6->{},7->{8},8->{9,10,11,12},9->{13} ,10->{9,10,11,12},11->{14,15},12->{14,15},13->{16},14->{9,10,11,12},15->{17},16->{19,20},17->{18},18->{14 ,15},19->{21,22},20->{23,24},21->{25},22->{21,22},23->{19,20},24->{23,24},25->{26,27,28},26->{29},27->{30} ,28->{30},29->{6,7,31,32},30->{6,7,31,32},31->{33},32->{8},33->{34},34->{35},35->{16}] + Applied Processor: ArgumentFilter [3,4,5,6,12,13,14,15,16,17,18,19,20,21,22,24,26,27,28] + Details: We remove following argument positions: [3,4,5,6,12,13,14,15,16,17,18,19,20,21,22,24,26,27,28]. * Step 2: UnsatPaths MAYBE + Considered Problem: Rules: 0. start(A,B,C,H,I,J,K,L,X,Z) -> f2(A,B,C,H,I,J,K,L,X,Z) True (1,1) 1. f2(A,B,C,H,I,J,K,L,X,Z) -> f15(A,B,C,H,I,J,K,L,X,Z) [B >= 1 + A && C >= 1] (?,1) 2. f2(A,B,C,H,I,J,K,L,X,Z) -> f1(A,B,C,H,I,J,K,L,X,Z) [B >= 1 + A && 0 >= C] (?,1) 3. f2(A,B,C,H,I,J,K,L,X,Z) -> f2(A,1 + B,E1,H,I,J,K,L,X,Z) [A >= B && D1 >= 1 + C] (?,1) 4. f2(A,B,C,H,I,J,K,L,X,Z) -> f2(A,1 + B,C,H,I,J,K,L,X,Z) [A >= B && C >= D1] (?,1) 5. f15(A,B,C,H,I,J,K,L,X,Z) -> f26(A,B,C,H,1,J,K,L,X,Z) [-1 + C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A] (?,1) 6. f26(A,B,C,H,I,J,K,L,X,Z) -> f1(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && -1 + -1*A + B >= 0 && J >= 201] (?,1) 7. f26(A,B,C,H,I,J,K,L,X,Z) -> f30(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && -1 + -1*A + B >= 0 && I >= 1 && 200 >= J] (?,1) 8. f30(A,B,C,H,I,J,K,L,X,Z) -> f42(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] (?,1) 9. f42(A,B,C,H,I,J,K,L,X,Z) -> f68(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && L >= A] (?,1) 10. f42(A,B,C,H,I,J,K,L,X,Z) -> f42(A,B,C,H,I,J,K,1 + L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && A >= 1 + L] (?,1) 11. f42(A,B,C,H,I,J,K,L,X,Z) -> f47(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && A >= 1 + L && D1 >= 1] (?,1) 12. f42(A,B,C,H,I,J,K,L,X,Z) -> f47(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 (?,1) && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && A >= 1 + L && 0 >= 1 + D1] 13. f68(A,B,C,H,I,J,K,L,X,Z) -> f152(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 (?,1) && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && -1*A + L >= 0 && 200 + -1*J >= 0 && B >= 1 + A] 14. f47(A,B,C,H,I,J,K,L,X,Z) -> f42(A,B,C,H,I,J,K,1 + L,X,Z) [1 + -1*I >= 0 (?,1) && 201 + -1*I + -1*J >= 0 && -2 + B + -1*L >= 0 && -1 + -1*A + B >= 0 && -1 + A + -1*L >= 0 && 200 + -1*J >= 0 && K >= 1 + A] 15. f47(A,B,C,H,I,J,K,L,X,Z) -> f51(A,B,C,0,I,J,K,L,X,Z) [1 + -1*I >= 0 (?,1) && 201 + -1*I + -1*J >= 0 && -2 + B + -1*L >= 0 && -1 + -1*A + B >= 0 && -1 + A + -1*L >= 0 && 200 + -1*J >= 0 && A >= K] 16. f152(A,B,C,H,I,J,K,L,X,Z) -> f164(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] (?,1) 17. f51(A,B,C,H,I,J,K,L,X,Z) -> f58(A,B,C,D1,I,J,K,L,X,Z) [1 + -1*I >= 0 (?,1) && 1 + H + -1*I >= 0 && 1 + -1*H + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1*H >= 0 && 200 + -1*H + -1*J >= 0 && H >= 0 && 200 + H + -1*J >= 0 && -2 + B + -1*L >= 0 && -1 + B + -1*K >= 0 && -1 + -1*A + B >= 0 && -1 + A + -1*L >= 0 && A + -1*K >= 0 && 200 + -1*J >= 0 && B >= 1 + A] 18. f58(A,B,C,H,I,J,K,L,X,Z) -> f47(A,B,C,H,I,J,1 + K,L,X,Z) [1 + -1*I >= 0 (?,1) && 201 + -1*I + -1*J >= 0 && -2 + B + -1*L >= 0 && -1 + B + -1*K >= 0 && -1 + -1*A + B >= 0 && -1 + A + -1*L >= 0 && A + -1*K >= 0 && 200 + -1*J >= 0 && B >= 1 + A] 19. f164(A,B,C,H,I,J,K,L,X,Z) -> f176(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && 200 + -1*J >= 0 && 0 >= B] (?,1) 20. f164(A,B,C,H,I,J,K,L,X,Z) -> f167(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && 200 + -1*J >= 0 && B >= 1] (?,1) 21. f176(A,B,C,H,I,J,K,L,X,Z) -> f184(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && 200 + -1*J >= 0 && B >= 1 + A] (?,1) 22. f176(A,B,C,H,I,J,K,L,X,Z) -> f176(A,1 + B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && 200 + -1*J >= 0 && A >= B] (?,1) 23. f167(A,B,C,H,I,J,K,L,X,Z) -> f164(A,-1 + B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 (?,1) && B + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + B >= 0 && 199 + B + -1*J >= 0 && 200 + -1*J >= 0 && K >= 1 + B] 24. f167(A,B,C,H,I,J,K,L,X,Z) -> f167(A,B,C,D1,I,J,1 + K,L,X,Z) [1 + -1*I >= 0 (?,1) && B + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + B >= 0 && 199 + B + -1*J >= 0 && 200 + -1*J >= 0 && B >= K] 25. f184(A,B,C,H,I,J,K,L,X,Z) -> f199(A,B,0,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] (?,1) 26. f199(A,B,C,H,I,J,K,L,X,Z) -> f218(A,B,0,H,0,J,K,L,0,Z) [1 + -1*I >= 0 (?,1) && 1 + C + -1*I >= 0 && 1 + -1*C + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1*C >= 0 && 200 + -1*C + -1*J >= 0 && C >= 0 && 200 + C + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] 27. f199(A,B,C,H,I,J,K,L,X,Z) -> f210(A,B,C,H,I,J,K,L,D1,Z) [1 + -1*I >= 0 (?,1) && 1 + C + -1*I >= 0 && 1 + -1*C + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1*C >= 0 && 200 + -1*C + -1*J >= 0 && C >= 0 && 200 + C + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A && D1 >= 1] 28. f199(A,B,C,H,I,J,K,L,X,Z) -> f210(A,B,C,H,I,J,K,L,D1,Z) [1 + -1*I >= 0 (?,1) && 1 + C + -1*I >= 0 && 1 + -1*C + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1*C >= 0 && 200 + -1*C + -1*J >= 0 && C >= 0 && 200 + C + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A && 0 >= 1 + D1] 29. f218(A,B,C,H,I,J,K,L,X,Z) -> f26(A,B,C,H,I,1 + J,K,L,X,Z) [-1*I >= 0 (?,1) && C + -1*I >= 0 && -1*C + -1*I >= 0 && -1*I + X >= 0 && -1*I + -1*X >= 0 && 200 + -1*I + -1*J >= 0 && I >= 0 && C + I >= 0 && -1*C + I >= 0 && I + X >= 0 && I + -1*X >= 0 && 200 + I + -1*J >= 0 && -1*C >= 0 && -1*C + X >= 0 && -1*C + -1*X >= 0 && 200 + -1*C + -1*J >= 0 && C >= 0 && C + X >= 0 && C + -1*X >= 0 && 200 + C + -1*J >= 0 && -1*X >= 0 && 200 + -1*J + -1*X >= 0 && X >= 0 && 200 + -1*J + X >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] 30. f210(A,B,C,H,I,J,K,L,X,Z) -> f26(A,B,C,H,I,1 + J,K,L,X,Z) [1 + -1*I >= 0 (?,1) && 1 + C + -1*I >= 0 && 1 + -1*C + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1*C >= 0 && 200 + -1*C + -1*J >= 0 && C >= 0 && 200 + C + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] 31. f26(A,B,C,H,I,J,K,L,X,Z) -> f81(A,B,C,H,0,J,K,L,X,Z) [1 + -1*I >= 0 && -1 + -1*A + B >= 0 && 200 >= J && I = 0] (?,1) 32. f26(A,B,C,H,I,J,K,L,X,Z) -> f30(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && -1 + -1*A + B >= 0 && 0 >= 1 + I && 200 >= J] (?,1) 33. f81(A,B,C,H,I,J,K,L,X,Z) -> f87(A,B,C,H,I,J,K,L,X,Z) [-1*I >= 0 (?,1) && 200 + -1*I + -1*J >= 0 && I >= 0 && 200 + I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] 34. f87(A,B,C,H,I,J,K,L,X,Z) -> f100(A,B,C,H,I,J,K,L,X,1) [-1*I >= 0 (?,1) && 200 + -1*I + -1*J >= 0 && I >= 0 && 200 + I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] 35. f100(A,B,C,H,I,J,K,L,X,Z) -> f152(A,B,C,H,I,J,K,L,X,Z) [-1*I >= 0 (?,1) && -1 + -1*I + Z >= 0 && 1 + -1*I + -1*Z >= 0 && 200 + -1*I + -1*J >= 0 && I >= 0 && -1 + I + Z >= 0 && 1 + I + -1*Z >= 0 && 200 + I + -1*J >= 0 && 1 + -1*Z >= 0 && 201 + -1*J + -1*Z >= 0 && -1 + Z >= 0 && 199 + -1*J + Z >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A && Z >= 1] Signature: {(f1,29) ;(f100,29) ;(f15,29) ;(f152,29) ;(f164,29) ;(f167,29) ;(f176,29) ;(f184,29) ;(f199,29) ;(f2,29) ;(f210,29) ;(f218,29) ;(f26,29) ;(f30,29) ;(f42,29) ;(f47,29) ;(f51,29) ;(f58,29) ;(f68,29) ;(f81,29) ;(f87,29) ;(start,29)} Flow Graph: [0->{1,2,3,4},1->{5},2->{},3->{1,2,3,4},4->{1,2,3,4},5->{6,7,31,32},6->{},7->{8},8->{9,10,11,12},9->{13} ,10->{9,10,11,12},11->{14,15},12->{14,15},13->{16},14->{9,10,11,12},15->{17},16->{19,20},17->{18},18->{14 ,15},19->{21,22},20->{23,24},21->{25},22->{21,22},23->{19,20},24->{23,24},25->{26,27,28},26->{29},27->{30} ,28->{30},29->{6,7,31,32},30->{6,7,31,32},31->{33},32->{8},33->{34},34->{35},35->{16}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(5,31),(5,32),(29,7),(29,32)] * Step 3: FromIts MAYBE + Considered Problem: Rules: 0. start(A,B,C,H,I,J,K,L,X,Z) -> f2(A,B,C,H,I,J,K,L,X,Z) True (1,1) 1. f2(A,B,C,H,I,J,K,L,X,Z) -> f15(A,B,C,H,I,J,K,L,X,Z) [B >= 1 + A && C >= 1] (?,1) 2. f2(A,B,C,H,I,J,K,L,X,Z) -> f1(A,B,C,H,I,J,K,L,X,Z) [B >= 1 + A && 0 >= C] (?,1) 3. f2(A,B,C,H,I,J,K,L,X,Z) -> f2(A,1 + B,E1,H,I,J,K,L,X,Z) [A >= B && D1 >= 1 + C] (?,1) 4. f2(A,B,C,H,I,J,K,L,X,Z) -> f2(A,1 + B,C,H,I,J,K,L,X,Z) [A >= B && C >= D1] (?,1) 5. f15(A,B,C,H,I,J,K,L,X,Z) -> f26(A,B,C,H,1,J,K,L,X,Z) [-1 + C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A] (?,1) 6. f26(A,B,C,H,I,J,K,L,X,Z) -> f1(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && -1 + -1*A + B >= 0 && J >= 201] (?,1) 7. f26(A,B,C,H,I,J,K,L,X,Z) -> f30(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && -1 + -1*A + B >= 0 && I >= 1 && 200 >= J] (?,1) 8. f30(A,B,C,H,I,J,K,L,X,Z) -> f42(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] (?,1) 9. f42(A,B,C,H,I,J,K,L,X,Z) -> f68(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && L >= A] (?,1) 10. f42(A,B,C,H,I,J,K,L,X,Z) -> f42(A,B,C,H,I,J,K,1 + L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && A >= 1 + L] (?,1) 11. f42(A,B,C,H,I,J,K,L,X,Z) -> f47(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && A >= 1 + L && D1 >= 1] (?,1) 12. f42(A,B,C,H,I,J,K,L,X,Z) -> f47(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 (?,1) && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && A >= 1 + L && 0 >= 1 + D1] 13. f68(A,B,C,H,I,J,K,L,X,Z) -> f152(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 (?,1) && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && -1*A + L >= 0 && 200 + -1*J >= 0 && B >= 1 + A] 14. f47(A,B,C,H,I,J,K,L,X,Z) -> f42(A,B,C,H,I,J,K,1 + L,X,Z) [1 + -1*I >= 0 (?,1) && 201 + -1*I + -1*J >= 0 && -2 + B + -1*L >= 0 && -1 + -1*A + B >= 0 && -1 + A + -1*L >= 0 && 200 + -1*J >= 0 && K >= 1 + A] 15. f47(A,B,C,H,I,J,K,L,X,Z) -> f51(A,B,C,0,I,J,K,L,X,Z) [1 + -1*I >= 0 (?,1) && 201 + -1*I + -1*J >= 0 && -2 + B + -1*L >= 0 && -1 + -1*A + B >= 0 && -1 + A + -1*L >= 0 && 200 + -1*J >= 0 && A >= K] 16. f152(A,B,C,H,I,J,K,L,X,Z) -> f164(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] (?,1) 17. f51(A,B,C,H,I,J,K,L,X,Z) -> f58(A,B,C,D1,I,J,K,L,X,Z) [1 + -1*I >= 0 (?,1) && 1 + H + -1*I >= 0 && 1 + -1*H + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1*H >= 0 && 200 + -1*H + -1*J >= 0 && H >= 0 && 200 + H + -1*J >= 0 && -2 + B + -1*L >= 0 && -1 + B + -1*K >= 0 && -1 + -1*A + B >= 0 && -1 + A + -1*L >= 0 && A + -1*K >= 0 && 200 + -1*J >= 0 && B >= 1 + A] 18. f58(A,B,C,H,I,J,K,L,X,Z) -> f47(A,B,C,H,I,J,1 + K,L,X,Z) [1 + -1*I >= 0 (?,1) && 201 + -1*I + -1*J >= 0 && -2 + B + -1*L >= 0 && -1 + B + -1*K >= 0 && -1 + -1*A + B >= 0 && -1 + A + -1*L >= 0 && A + -1*K >= 0 && 200 + -1*J >= 0 && B >= 1 + A] 19. f164(A,B,C,H,I,J,K,L,X,Z) -> f176(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && 200 + -1*J >= 0 && 0 >= B] (?,1) 20. f164(A,B,C,H,I,J,K,L,X,Z) -> f167(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && 200 + -1*J >= 0 && B >= 1] (?,1) 21. f176(A,B,C,H,I,J,K,L,X,Z) -> f184(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && 200 + -1*J >= 0 && B >= 1 + A] (?,1) 22. f176(A,B,C,H,I,J,K,L,X,Z) -> f176(A,1 + B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && 200 + -1*J >= 0 && A >= B] (?,1) 23. f167(A,B,C,H,I,J,K,L,X,Z) -> f164(A,-1 + B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 (?,1) && B + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + B >= 0 && 199 + B + -1*J >= 0 && 200 + -1*J >= 0 && K >= 1 + B] 24. f167(A,B,C,H,I,J,K,L,X,Z) -> f167(A,B,C,D1,I,J,1 + K,L,X,Z) [1 + -1*I >= 0 (?,1) && B + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + B >= 0 && 199 + B + -1*J >= 0 && 200 + -1*J >= 0 && B >= K] 25. f184(A,B,C,H,I,J,K,L,X,Z) -> f199(A,B,0,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] (?,1) 26. f199(A,B,C,H,I,J,K,L,X,Z) -> f218(A,B,0,H,0,J,K,L,0,Z) [1 + -1*I >= 0 (?,1) && 1 + C + -1*I >= 0 && 1 + -1*C + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1*C >= 0 && 200 + -1*C + -1*J >= 0 && C >= 0 && 200 + C + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] 27. f199(A,B,C,H,I,J,K,L,X,Z) -> f210(A,B,C,H,I,J,K,L,D1,Z) [1 + -1*I >= 0 (?,1) && 1 + C + -1*I >= 0 && 1 + -1*C + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1*C >= 0 && 200 + -1*C + -1*J >= 0 && C >= 0 && 200 + C + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A && D1 >= 1] 28. f199(A,B,C,H,I,J,K,L,X,Z) -> f210(A,B,C,H,I,J,K,L,D1,Z) [1 + -1*I >= 0 (?,1) && 1 + C + -1*I >= 0 && 1 + -1*C + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1*C >= 0 && 200 + -1*C + -1*J >= 0 && C >= 0 && 200 + C + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A && 0 >= 1 + D1] 29. f218(A,B,C,H,I,J,K,L,X,Z) -> f26(A,B,C,H,I,1 + J,K,L,X,Z) [-1*I >= 0 (?,1) && C + -1*I >= 0 && -1*C + -1*I >= 0 && -1*I + X >= 0 && -1*I + -1*X >= 0 && 200 + -1*I + -1*J >= 0 && I >= 0 && C + I >= 0 && -1*C + I >= 0 && I + X >= 0 && I + -1*X >= 0 && 200 + I + -1*J >= 0 && -1*C >= 0 && -1*C + X >= 0 && -1*C + -1*X >= 0 && 200 + -1*C + -1*J >= 0 && C >= 0 && C + X >= 0 && C + -1*X >= 0 && 200 + C + -1*J >= 0 && -1*X >= 0 && 200 + -1*J + -1*X >= 0 && X >= 0 && 200 + -1*J + X >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] 30. f210(A,B,C,H,I,J,K,L,X,Z) -> f26(A,B,C,H,I,1 + J,K,L,X,Z) [1 + -1*I >= 0 (?,1) && 1 + C + -1*I >= 0 && 1 + -1*C + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1*C >= 0 && 200 + -1*C + -1*J >= 0 && C >= 0 && 200 + C + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] 31. f26(A,B,C,H,I,J,K,L,X,Z) -> f81(A,B,C,H,0,J,K,L,X,Z) [1 + -1*I >= 0 && -1 + -1*A + B >= 0 && 200 >= J && I = 0] (?,1) 32. f26(A,B,C,H,I,J,K,L,X,Z) -> f30(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && -1 + -1*A + B >= 0 && 0 >= 1 + I && 200 >= J] (?,1) 33. f81(A,B,C,H,I,J,K,L,X,Z) -> f87(A,B,C,H,I,J,K,L,X,Z) [-1*I >= 0 (?,1) && 200 + -1*I + -1*J >= 0 && I >= 0 && 200 + I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] 34. f87(A,B,C,H,I,J,K,L,X,Z) -> f100(A,B,C,H,I,J,K,L,X,1) [-1*I >= 0 (?,1) && 200 + -1*I + -1*J >= 0 && I >= 0 && 200 + I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] 35. f100(A,B,C,H,I,J,K,L,X,Z) -> f152(A,B,C,H,I,J,K,L,X,Z) [-1*I >= 0 (?,1) && -1 + -1*I + Z >= 0 && 1 + -1*I + -1*Z >= 0 && 200 + -1*I + -1*J >= 0 && I >= 0 && -1 + I + Z >= 0 && 1 + I + -1*Z >= 0 && 200 + I + -1*J >= 0 && 1 + -1*Z >= 0 && 201 + -1*J + -1*Z >= 0 && -1 + Z >= 0 && 199 + -1*J + Z >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A && Z >= 1] Signature: {(f1,29) ;(f100,29) ;(f15,29) ;(f152,29) ;(f164,29) ;(f167,29) ;(f176,29) ;(f184,29) ;(f199,29) ;(f2,29) ;(f210,29) ;(f218,29) ;(f26,29) ;(f30,29) ;(f42,29) ;(f47,29) ;(f51,29) ;(f58,29) ;(f68,29) ;(f81,29) ;(f87,29) ;(start,29)} Flow Graph: [0->{1,2,3,4},1->{5},2->{},3->{1,2,3,4},4->{1,2,3,4},5->{6,7},6->{},7->{8},8->{9,10,11,12},9->{13},10->{9 ,10,11,12},11->{14,15},12->{14,15},13->{16},14->{9,10,11,12},15->{17},16->{19,20},17->{18},18->{14,15} ,19->{21,22},20->{23,24},21->{25},22->{21,22},23->{19,20},24->{23,24},25->{26,27,28},26->{29},27->{30} ,28->{30},29->{6,31},30->{6,7,31,32},31->{33},32->{8},33->{34},34->{35},35->{16}] + Applied Processor: FromIts + Details: () * Step 4: Unfold MAYBE + Considered Problem: Rules: start(A,B,C,H,I,J,K,L,X,Z) -> f2(A,B,C,H,I,J,K,L,X,Z) True f2(A,B,C,H,I,J,K,L,X,Z) -> f15(A,B,C,H,I,J,K,L,X,Z) [B >= 1 + A && C >= 1] f2(A,B,C,H,I,J,K,L,X,Z) -> f1(A,B,C,H,I,J,K,L,X,Z) [B >= 1 + A && 0 >= C] f2(A,B,C,H,I,J,K,L,X,Z) -> f2(A,1 + B,E1,H,I,J,K,L,X,Z) [A >= B && D1 >= 1 + C] f2(A,B,C,H,I,J,K,L,X,Z) -> f2(A,1 + B,C,H,I,J,K,L,X,Z) [A >= B && C >= D1] f15(A,B,C,H,I,J,K,L,X,Z) -> f26(A,B,C,H,1,J,K,L,X,Z) [-1 + C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A] f26(A,B,C,H,I,J,K,L,X,Z) -> f1(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && -1 + -1*A + B >= 0 && J >= 201] f26(A,B,C,H,I,J,K,L,X,Z) -> f30(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && -1 + -1*A + B >= 0 && I >= 1 && 200 >= J] f30(A,B,C,H,I,J,K,L,X,Z) -> f42(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f42(A,B,C,H,I,J,K,L,X,Z) -> f68(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && L >= A] f42(A,B,C,H,I,J,K,L,X,Z) -> f42(A,B,C,H,I,J,K,1 + L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && A >= 1 + L] f42(A,B,C,H,I,J,K,L,X,Z) -> f47(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && A >= 1 + L && D1 >= 1] f42(A,B,C,H,I,J,K,L,X,Z) -> f47(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && A >= 1 + L && 0 >= 1 + D1] f68(A,B,C,H,I,J,K,L,X,Z) -> f152(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && -1*A + L >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f47(A,B,C,H,I,J,K,L,X,Z) -> f42(A,B,C,H,I,J,K,1 + L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -2 + B + -1*L >= 0 && -1 + -1*A + B >= 0 && -1 + A + -1*L >= 0 && 200 + -1*J >= 0 && K >= 1 + A] f47(A,B,C,H,I,J,K,L,X,Z) -> f51(A,B,C,0,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -2 + B + -1*L >= 0 && -1 + -1*A + B >= 0 && -1 + A + -1*L >= 0 && 200 + -1*J >= 0 && A >= K] f152(A,B,C,H,I,J,K,L,X,Z) -> f164(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f51(A,B,C,H,I,J,K,L,X,Z) -> f58(A,B,C,D1,I,J,K,L,X,Z) [1 + -1*I >= 0 && 1 + H + -1*I >= 0 && 1 + -1*H + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1*H >= 0 && 200 + -1*H + -1*J >= 0 && H >= 0 && 200 + H + -1*J >= 0 && -2 + B + -1*L >= 0 && -1 + B + -1*K >= 0 && -1 + -1*A + B >= 0 && -1 + A + -1*L >= 0 && A + -1*K >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f58(A,B,C,H,I,J,K,L,X,Z) -> f47(A,B,C,H,I,J,1 + K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -2 + B + -1*L >= 0 && -1 + B + -1*K >= 0 && -1 + -1*A + B >= 0 && -1 + A + -1*L >= 0 && A + -1*K >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f164(A,B,C,H,I,J,K,L,X,Z) -> f176(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && 200 + -1*J >= 0 && 0 >= B] f164(A,B,C,H,I,J,K,L,X,Z) -> f167(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && 200 + -1*J >= 0 && B >= 1] f176(A,B,C,H,I,J,K,L,X,Z) -> f184(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f176(A,B,C,H,I,J,K,L,X,Z) -> f176(A,1 + B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && 200 + -1*J >= 0 && A >= B] f167(A,B,C,H,I,J,K,L,X,Z) -> f164(A,-1 + B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && B + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + B >= 0 && 199 + B + -1*J >= 0 && 200 + -1*J >= 0 && K >= 1 + B] f167(A,B,C,H,I,J,K,L,X,Z) -> f167(A,B,C,D1,I,J,1 + K,L,X,Z) [1 + -1*I >= 0 && B + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + B >= 0 && 199 + B + -1*J >= 0 && 200 + -1*J >= 0 && B >= K] f184(A,B,C,H,I,J,K,L,X,Z) -> f199(A,B,0,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f199(A,B,C,H,I,J,K,L,X,Z) -> f218(A,B,0,H,0,J,K,L,0,Z) [1 + -1*I >= 0 && 1 + C + -1*I >= 0 && 1 + -1*C + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1*C >= 0 && 200 + -1*C + -1*J >= 0 && C >= 0 && 200 + C + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f199(A,B,C,H,I,J,K,L,X,Z) -> f210(A,B,C,H,I,J,K,L,D1,Z) [1 + -1*I >= 0 && 1 + C + -1*I >= 0 && 1 + -1*C + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1*C >= 0 && 200 + -1*C + -1*J >= 0 && C >= 0 && 200 + C + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A && D1 >= 1] f199(A,B,C,H,I,J,K,L,X,Z) -> f210(A,B,C,H,I,J,K,L,D1,Z) [1 + -1*I >= 0 && 1 + C + -1*I >= 0 && 1 + -1*C + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1*C >= 0 && 200 + -1*C + -1*J >= 0 && C >= 0 && 200 + C + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A && 0 >= 1 + D1] f218(A,B,C,H,I,J,K,L,X,Z) -> f26(A,B,C,H,I,1 + J,K,L,X,Z) [-1*I >= 0 && C + -1*I >= 0 && -1*C + -1*I >= 0 && -1*I + X >= 0 && -1*I + -1*X >= 0 && 200 + -1*I + -1*J >= 0 && I >= 0 && C + I >= 0 && -1*C + I >= 0 && I + X >= 0 && I + -1*X >= 0 && 200 + I + -1*J >= 0 && -1*C >= 0 && -1*C + X >= 0 && -1*C + -1*X >= 0 && 200 + -1*C + -1*J >= 0 && C >= 0 && C + X >= 0 && C + -1*X >= 0 && 200 + C + -1*J >= 0 && -1*X >= 0 && 200 + -1*J + -1*X >= 0 && X >= 0 && 200 + -1*J + X >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f210(A,B,C,H,I,J,K,L,X,Z) -> f26(A,B,C,H,I,1 + J,K,L,X,Z) [1 + -1*I >= 0 && 1 + C + -1*I >= 0 && 1 + -1*C + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1*C >= 0 && 200 + -1*C + -1*J >= 0 && C >= 0 && 200 + C + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f26(A,B,C,H,I,J,K,L,X,Z) -> f81(A,B,C,H,0,J,K,L,X,Z) [1 + -1*I >= 0 && -1 + -1*A + B >= 0 && 200 >= J && I = 0] f26(A,B,C,H,I,J,K,L,X,Z) -> f30(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && -1 + -1*A + B >= 0 && 0 >= 1 + I && 200 >= J] f81(A,B,C,H,I,J,K,L,X,Z) -> f87(A,B,C,H,I,J,K,L,X,Z) [-1*I >= 0 && 200 + -1*I + -1*J >= 0 && I >= 0 && 200 + I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f87(A,B,C,H,I,J,K,L,X,Z) -> f100(A,B,C,H,I,J,K,L,X,1) [-1*I >= 0 && 200 + -1*I + -1*J >= 0 && I >= 0 && 200 + I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f100(A,B,C,H,I,J,K,L,X,Z) -> f152(A,B,C,H,I,J,K,L,X,Z) [-1*I >= 0 && -1 + -1*I + Z >= 0 && 1 + -1*I + -1*Z >= 0 && 200 + -1*I + -1*J >= 0 && I >= 0 && -1 + I + Z >= 0 && 1 + I + -1*Z >= 0 && 200 + I + -1*J >= 0 && 1 + -1*Z >= 0 && 201 + -1*J + -1*Z >= 0 && -1 + Z >= 0 && 199 + -1*J + Z >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A && Z >= 1] Signature: {(f1,29) ;(f100,29) ;(f15,29) ;(f152,29) ;(f164,29) ;(f167,29) ;(f176,29) ;(f184,29) ;(f199,29) ;(f2,29) ;(f210,29) ;(f218,29) ;(f26,29) ;(f30,29) ;(f42,29) ;(f47,29) ;(f51,29) ;(f58,29) ;(f68,29) ;(f81,29) ;(f87,29) ;(start,29)} Rule Graph: [0->{1,2,3,4},1->{5},2->{},3->{1,2,3,4},4->{1,2,3,4},5->{6,7},6->{},7->{8},8->{9,10,11,12},9->{13},10->{9 ,10,11,12},11->{14,15},12->{14,15},13->{16},14->{9,10,11,12},15->{17},16->{19,20},17->{18},18->{14,15} ,19->{21,22},20->{23,24},21->{25},22->{21,22},23->{19,20},24->{23,24},25->{26,27,28},26->{29},27->{30} ,28->{30},29->{6,31},30->{6,7,31,32},31->{33},32->{8},33->{34},34->{35},35->{16}] + Applied Processor: Unfold + Details: () * Step 5: AddSinks MAYBE + Considered Problem: Rules: start.0(A,B,C,H,I,J,K,L,X,Z) -> f2.1(A,B,C,H,I,J,K,L,X,Z) True start.0(A,B,C,H,I,J,K,L,X,Z) -> f2.2(A,B,C,H,I,J,K,L,X,Z) True start.0(A,B,C,H,I,J,K,L,X,Z) -> f2.3(A,B,C,H,I,J,K,L,X,Z) True start.0(A,B,C,H,I,J,K,L,X,Z) -> f2.4(A,B,C,H,I,J,K,L,X,Z) True f2.1(A,B,C,H,I,J,K,L,X,Z) -> f15.5(A,B,C,H,I,J,K,L,X,Z) [B >= 1 + A && C >= 1] f2.2(A,B,C,H,I,J,K,L,X,Z) -> f1.36(A,B,C,H,I,J,K,L,X,Z) [B >= 1 + A && 0 >= C] f2.3(A,B,C,H,I,J,K,L,X,Z) -> f2.1(A,1 + B,E1,H,I,J,K,L,X,Z) [A >= B && D1 >= 1 + C] f2.3(A,B,C,H,I,J,K,L,X,Z) -> f2.2(A,1 + B,E1,H,I,J,K,L,X,Z) [A >= B && D1 >= 1 + C] f2.3(A,B,C,H,I,J,K,L,X,Z) -> f2.3(A,1 + B,E1,H,I,J,K,L,X,Z) [A >= B && D1 >= 1 + C] f2.3(A,B,C,H,I,J,K,L,X,Z) -> f2.4(A,1 + B,E1,H,I,J,K,L,X,Z) [A >= B && D1 >= 1 + C] f2.4(A,B,C,H,I,J,K,L,X,Z) -> f2.1(A,1 + B,C,H,I,J,K,L,X,Z) [A >= B && C >= D1] f2.4(A,B,C,H,I,J,K,L,X,Z) -> f2.2(A,1 + B,C,H,I,J,K,L,X,Z) [A >= B && C >= D1] f2.4(A,B,C,H,I,J,K,L,X,Z) -> f2.3(A,1 + B,C,H,I,J,K,L,X,Z) [A >= B && C >= D1] f2.4(A,B,C,H,I,J,K,L,X,Z) -> f2.4(A,1 + B,C,H,I,J,K,L,X,Z) [A >= B && C >= D1] f15.5(A,B,C,H,I,J,K,L,X,Z) -> f26.6(A,B,C,H,1,J,K,L,X,Z) [-1 + C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A] f15.5(A,B,C,H,I,J,K,L,X,Z) -> f26.7(A,B,C,H,1,J,K,L,X,Z) [-1 + C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A] f26.6(A,B,C,H,I,J,K,L,X,Z) -> f1.36(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && -1 + -1*A + B >= 0 && J >= 201] f26.7(A,B,C,H,I,J,K,L,X,Z) -> f30.8(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && -1 + -1*A + B >= 0 && I >= 1 && 200 >= J] f30.8(A,B,C,H,I,J,K,L,X,Z) -> f42.9(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f30.8(A,B,C,H,I,J,K,L,X,Z) -> f42.10(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f30.8(A,B,C,H,I,J,K,L,X,Z) -> f42.11(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f30.8(A,B,C,H,I,J,K,L,X,Z) -> f42.12(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f42.9(A,B,C,H,I,J,K,L,X,Z) -> f68.13(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && L >= A] f42.10(A,B,C,H,I,J,K,L,X,Z) -> f42.9(A,B,C,H,I,J,K,1 + L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && A >= 1 + L] f42.10(A,B,C,H,I,J,K,L,X,Z) -> f42.10(A,B,C,H,I,J,K,1 + L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && A >= 1 + L] f42.10(A,B,C,H,I,J,K,L,X,Z) -> f42.11(A,B,C,H,I,J,K,1 + L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && A >= 1 + L] f42.10(A,B,C,H,I,J,K,L,X,Z) -> f42.12(A,B,C,H,I,J,K,1 + L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && A >= 1 + L] f42.11(A,B,C,H,I,J,K,L,X,Z) -> f47.14(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && A >= 1 + L && D1 >= 1] f42.11(A,B,C,H,I,J,K,L,X,Z) -> f47.15(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && A >= 1 + L && D1 >= 1] f42.12(A,B,C,H,I,J,K,L,X,Z) -> f47.14(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && A >= 1 + L && 0 >= 1 + D1] f42.12(A,B,C,H,I,J,K,L,X,Z) -> f47.15(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && A >= 1 + L && 0 >= 1 + D1] f68.13(A,B,C,H,I,J,K,L,X,Z) -> f152.16(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && -1*A + L >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f47.14(A,B,C,H,I,J,K,L,X,Z) -> f42.9(A,B,C,H,I,J,K,1 + L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -2 + B + -1*L >= 0 && -1 + -1*A + B >= 0 && -1 + A + -1*L >= 0 && 200 + -1*J >= 0 && K >= 1 + A] f47.14(A,B,C,H,I,J,K,L,X,Z) -> f42.10(A,B,C,H,I,J,K,1 + L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -2 + B + -1*L >= 0 && -1 + -1*A + B >= 0 && -1 + A + -1*L >= 0 && 200 + -1*J >= 0 && K >= 1 + A] f47.14(A,B,C,H,I,J,K,L,X,Z) -> f42.11(A,B,C,H,I,J,K,1 + L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -2 + B + -1*L >= 0 && -1 + -1*A + B >= 0 && -1 + A + -1*L >= 0 && 200 + -1*J >= 0 && K >= 1 + A] f47.14(A,B,C,H,I,J,K,L,X,Z) -> f42.12(A,B,C,H,I,J,K,1 + L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -2 + B + -1*L >= 0 && -1 + -1*A + B >= 0 && -1 + A + -1*L >= 0 && 200 + -1*J >= 0 && K >= 1 + A] f47.15(A,B,C,H,I,J,K,L,X,Z) -> f51.17(A,B,C,0,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -2 + B + -1*L >= 0 && -1 + -1*A + B >= 0 && -1 + A + -1*L >= 0 && 200 + -1*J >= 0 && A >= K] f152.16(A,B,C,H,I,J,K,L,X,Z) -> f164.19(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f152.16(A,B,C,H,I,J,K,L,X,Z) -> f164.20(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f51.17(A,B,C,H,I,J,K,L,X,Z) -> f58.18(A,B,C,D1,I,J,K,L,X,Z) [1 + -1*I >= 0 && 1 + H + -1*I >= 0 && 1 + -1*H + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1*H >= 0 && 200 + -1*H + -1*J >= 0 && H >= 0 && 200 + H + -1*J >= 0 && -2 + B + -1*L >= 0 && -1 + B + -1*K >= 0 && -1 + -1*A + B >= 0 && -1 + A + -1*L >= 0 && A + -1*K >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f58.18(A,B,C,H,I,J,K,L,X,Z) -> f47.14(A,B,C,H,I,J,1 + K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -2 + B + -1*L >= 0 && -1 + B + -1*K >= 0 && -1 + -1*A + B >= 0 && -1 + A + -1*L >= 0 && A + -1*K >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f58.18(A,B,C,H,I,J,K,L,X,Z) -> f47.15(A,B,C,H,I,J,1 + K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -2 + B + -1*L >= 0 && -1 + B + -1*K >= 0 && -1 + -1*A + B >= 0 && -1 + A + -1*L >= 0 && A + -1*K >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f164.19(A,B,C,H,I,J,K,L,X,Z) -> f176.21(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && 200 + -1*J >= 0 && 0 >= B] f164.19(A,B,C,H,I,J,K,L,X,Z) -> f176.22(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && 200 + -1*J >= 0 && 0 >= B] f164.20(A,B,C,H,I,J,K,L,X,Z) -> f167.23(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && 200 + -1*J >= 0 && B >= 1] f164.20(A,B,C,H,I,J,K,L,X,Z) -> f167.24(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && 200 + -1*J >= 0 && B >= 1] f176.21(A,B,C,H,I,J,K,L,X,Z) -> f184.25(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f176.22(A,B,C,H,I,J,K,L,X,Z) -> f176.21(A,1 + B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && 200 + -1*J >= 0 && A >= B] f176.22(A,B,C,H,I,J,K,L,X,Z) -> f176.22(A,1 + B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && 200 + -1*J >= 0 && A >= B] f167.23(A,B,C,H,I,J,K,L,X,Z) -> f164.19(A,-1 + B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && B + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + B >= 0 && 199 + B + -1*J >= 0 && 200 + -1*J >= 0 && K >= 1 + B] f167.23(A,B,C,H,I,J,K,L,X,Z) -> f164.20(A,-1 + B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && B + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + B >= 0 && 199 + B + -1*J >= 0 && 200 + -1*J >= 0 && K >= 1 + B] f167.24(A,B,C,H,I,J,K,L,X,Z) -> f167.23(A,B,C,D1,I,J,1 + K,L,X,Z) [1 + -1*I >= 0 && B + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + B >= 0 && 199 + B + -1*J >= 0 && 200 + -1*J >= 0 && B >= K] f167.24(A,B,C,H,I,J,K,L,X,Z) -> f167.24(A,B,C,D1,I,J,1 + K,L,X,Z) [1 + -1*I >= 0 && B + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + B >= 0 && 199 + B + -1*J >= 0 && 200 + -1*J >= 0 && B >= K] f184.25(A,B,C,H,I,J,K,L,X,Z) -> f199.26(A,B,0,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f184.25(A,B,C,H,I,J,K,L,X,Z) -> f199.27(A,B,0,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f184.25(A,B,C,H,I,J,K,L,X,Z) -> f199.28(A,B,0,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f199.26(A,B,C,H,I,J,K,L,X,Z) -> f218.29(A,B,0,H,0,J,K,L,0,Z) [1 + -1*I >= 0 && 1 + C + -1*I >= 0 && 1 + -1*C + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1*C >= 0 && 200 + -1*C + -1*J >= 0 && C >= 0 && 200 + C + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f199.27(A,B,C,H,I,J,K,L,X,Z) -> f210.30(A,B,C,H,I,J,K,L,D1,Z) [1 + -1*I >= 0 && 1 + C + -1*I >= 0 && 1 + -1*C + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1*C >= 0 && 200 + -1*C + -1*J >= 0 && C >= 0 && 200 + C + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A && D1 >= 1] f199.28(A,B,C,H,I,J,K,L,X,Z) -> f210.30(A,B,C,H,I,J,K,L,D1,Z) [1 + -1*I >= 0 && 1 + C + -1*I >= 0 && 1 + -1*C + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1*C >= 0 && 200 + -1*C + -1*J >= 0 && C >= 0 && 200 + C + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A && 0 >= 1 + D1] f218.29(A,B,C,H,I,J,K,L,X,Z) -> f26.6(A,B,C,H,I,1 + J,K,L,X,Z) [-1*I >= 0 && C + -1*I >= 0 && -1*C + -1*I >= 0 && -1*I + X >= 0 && -1*I + -1*X >= 0 && 200 + -1*I + -1*J >= 0 && I >= 0 && C + I >= 0 && -1*C + I >= 0 && I + X >= 0 && I + -1*X >= 0 && 200 + I + -1*J >= 0 && -1*C >= 0 && -1*C + X >= 0 && -1*C + -1*X >= 0 && 200 + -1*C + -1*J >= 0 && C >= 0 && C + X >= 0 && C + -1*X >= 0 && 200 + C + -1*J >= 0 && -1*X >= 0 && 200 + -1*J + -1*X >= 0 && X >= 0 && 200 + -1*J + X >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f218.29(A,B,C,H,I,J,K,L,X,Z) -> f26.31(A,B,C,H,I,1 + J,K,L,X,Z) [-1*I >= 0 && C + -1*I >= 0 && -1*C + -1*I >= 0 && -1*I + X >= 0 && -1*I + -1*X >= 0 && 200 + -1*I + -1*J >= 0 && I >= 0 && C + I >= 0 && -1*C + I >= 0 && I + X >= 0 && I + -1*X >= 0 && 200 + I + -1*J >= 0 && -1*C >= 0 && -1*C + X >= 0 && -1*C + -1*X >= 0 && 200 + -1*C + -1*J >= 0 && C >= 0 && C + X >= 0 && C + -1*X >= 0 && 200 + C + -1*J >= 0 && -1*X >= 0 && 200 + -1*J + -1*X >= 0 && X >= 0 && 200 + -1*J + X >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f210.30(A,B,C,H,I,J,K,L,X,Z) -> f26.6(A,B,C,H,I,1 + J,K,L,X,Z) [1 + -1*I >= 0 && 1 + C + -1*I >= 0 && 1 + -1*C + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1*C >= 0 && 200 + -1*C + -1*J >= 0 && C >= 0 && 200 + C + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f210.30(A,B,C,H,I,J,K,L,X,Z) -> f26.7(A,B,C,H,I,1 + J,K,L,X,Z) [1 + -1*I >= 0 && 1 + C + -1*I >= 0 && 1 + -1*C + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1*C >= 0 && 200 + -1*C + -1*J >= 0 && C >= 0 && 200 + C + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f210.30(A,B,C,H,I,J,K,L,X,Z) -> f26.31(A,B,C,H,I,1 + J,K,L,X,Z) [1 + -1*I >= 0 && 1 + C + -1*I >= 0 && 1 + -1*C + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1*C >= 0 && 200 + -1*C + -1*J >= 0 && C >= 0 && 200 + C + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f210.30(A,B,C,H,I,J,K,L,X,Z) -> f26.32(A,B,C,H,I,1 + J,K,L,X,Z) [1 + -1*I >= 0 && 1 + C + -1*I >= 0 && 1 + -1*C + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1*C >= 0 && 200 + -1*C + -1*J >= 0 && C >= 0 && 200 + C + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f26.31(A,B,C,H,I,J,K,L,X,Z) -> f81.33(A,B,C,H,0,J,K,L,X,Z) [1 + -1*I >= 0 && -1 + -1*A + B >= 0 && 200 >= J && I = 0] f26.32(A,B,C,H,I,J,K,L,X,Z) -> f30.8(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && -1 + -1*A + B >= 0 && 0 >= 1 + I && 200 >= J] f81.33(A,B,C,H,I,J,K,L,X,Z) -> f87.34(A,B,C,H,I,J,K,L,X,Z) [-1*I >= 0 && 200 + -1*I + -1*J >= 0 && I >= 0 && 200 + I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f87.34(A,B,C,H,I,J,K,L,X,Z) -> f100.35(A,B,C,H,I,J,K,L,X,1) [-1*I >= 0 && 200 + -1*I + -1*J >= 0 && I >= 0 && 200 + I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f100.35(A,B,C,H,I,J,K,L,X,Z) -> f152.16(A,B,C,H,I,J,K,L,X,Z) [-1*I >= 0 && -1 + -1*I + Z >= 0 && 1 + -1*I + -1*Z >= 0 && 200 + -1*I + -1*J >= 0 && I >= 0 && -1 + I + Z >= 0 && 1 + I + -1*Z >= 0 && 200 + I + -1*J >= 0 && 1 + -1*Z >= 0 && 201 + -1*J + -1*Z >= 0 && -1 + Z >= 0 && 199 + -1*J + Z >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A && Z >= 1] Signature: {(f1.36,10) ;(f100.35,10) ;(f15.5,10) ;(f152.16,10) ;(f164.19,10) ;(f164.20,10) ;(f167.23,10) ;(f167.24,10) ;(f176.21,10) ;(f176.22,10) ;(f184.25,10) ;(f199.26,10) ;(f199.27,10) ;(f199.28,10) ;(f2.1,10) ;(f2.2,10) ;(f2.3,10) ;(f2.4,10) ;(f210.30,10) ;(f218.29,10) ;(f26.31,10) ;(f26.32,10) ;(f26.6,10) ;(f26.7,10) ;(f30.8,10) ;(f42.10,10) ;(f42.11,10) ;(f42.12,10) ;(f42.9,10) ;(f47.14,10) ;(f47.15,10) ;(f51.17,10) ;(f58.18,10) ;(f68.13,10) ;(f81.33,10) ;(f87.34,10) ;(start.0,10)} Rule Graph: [0->{4},1->{5},2->{6,7,8,9},3->{10,11,12,13},4->{14,15},5->{},6->{4},7->{5},8->{6,7,8,9},9->{10,11,12,13} ,10->{4},11->{5},12->{6,7,8,9},13->{10,11,12,13},14->{16},15->{17},16->{},17->{18,19,20,21},18->{22},19->{23 ,24,25,26},20->{27,28},21->{29,30},22->{31},23->{22},24->{23,24,25,26},25->{27,28},26->{29,30},27->{32,33,34 ,35},28->{36},29->{32,33,34,35},30->{36},31->{37,38},32->{22},33->{23,24,25,26},34->{27,28},35->{29,30} ,36->{39},37->{42,43},38->{44,45},39->{40,41},40->{32,33,34,35},41->{36},42->{46},43->{47,48},44->{49,50} ,45->{51,52},46->{53,54,55},47->{46},48->{47,48},49->{42,43},50->{44,45},51->{49,50},52->{51,52},53->{56} ,54->{57},55->{58},56->{59,60},57->{61,62,63,64},58->{61,62,63,64},59->{16},60->{65},61->{16},62->{17} ,63->{65},64->{66},65->{67},66->{18,19,20,21},67->{68},68->{69},69->{37,38}] + Applied Processor: AddSinks + Details: () * Step 6: Decompose MAYBE + Considered Problem: Rules: start.0(A,B,C,H,I,J,K,L,X,Z) -> f2.1(A,B,C,H,I,J,K,L,X,Z) True start.0(A,B,C,H,I,J,K,L,X,Z) -> f2.2(A,B,C,H,I,J,K,L,X,Z) True start.0(A,B,C,H,I,J,K,L,X,Z) -> f2.3(A,B,C,H,I,J,K,L,X,Z) True start.0(A,B,C,H,I,J,K,L,X,Z) -> f2.4(A,B,C,H,I,J,K,L,X,Z) True f2.1(A,B,C,H,I,J,K,L,X,Z) -> f15.5(A,B,C,H,I,J,K,L,X,Z) [B >= 1 + A && C >= 1] f2.2(A,B,C,H,I,J,K,L,X,Z) -> f1.36(A,B,C,H,I,J,K,L,X,Z) [B >= 1 + A && 0 >= C] f2.3(A,B,C,H,I,J,K,L,X,Z) -> f2.1(A,1 + B,E1,H,I,J,K,L,X,Z) [A >= B && D1 >= 1 + C] f2.3(A,B,C,H,I,J,K,L,X,Z) -> f2.2(A,1 + B,E1,H,I,J,K,L,X,Z) [A >= B && D1 >= 1 + C] f2.3(A,B,C,H,I,J,K,L,X,Z) -> f2.3(A,1 + B,E1,H,I,J,K,L,X,Z) [A >= B && D1 >= 1 + C] f2.3(A,B,C,H,I,J,K,L,X,Z) -> f2.4(A,1 + B,E1,H,I,J,K,L,X,Z) [A >= B && D1 >= 1 + C] f2.4(A,B,C,H,I,J,K,L,X,Z) -> f2.1(A,1 + B,C,H,I,J,K,L,X,Z) [A >= B && C >= D1] f2.4(A,B,C,H,I,J,K,L,X,Z) -> f2.2(A,1 + B,C,H,I,J,K,L,X,Z) [A >= B && C >= D1] f2.4(A,B,C,H,I,J,K,L,X,Z) -> f2.3(A,1 + B,C,H,I,J,K,L,X,Z) [A >= B && C >= D1] f2.4(A,B,C,H,I,J,K,L,X,Z) -> f2.4(A,1 + B,C,H,I,J,K,L,X,Z) [A >= B && C >= D1] f15.5(A,B,C,H,I,J,K,L,X,Z) -> f26.6(A,B,C,H,1,J,K,L,X,Z) [-1 + C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A] f15.5(A,B,C,H,I,J,K,L,X,Z) -> f26.7(A,B,C,H,1,J,K,L,X,Z) [-1 + C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A] f26.6(A,B,C,H,I,J,K,L,X,Z) -> f1.36(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && -1 + -1*A + B >= 0 && J >= 201] f26.7(A,B,C,H,I,J,K,L,X,Z) -> f30.8(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && -1 + -1*A + B >= 0 && I >= 1 && 200 >= J] f30.8(A,B,C,H,I,J,K,L,X,Z) -> f42.9(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f30.8(A,B,C,H,I,J,K,L,X,Z) -> f42.10(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f30.8(A,B,C,H,I,J,K,L,X,Z) -> f42.11(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f30.8(A,B,C,H,I,J,K,L,X,Z) -> f42.12(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f42.9(A,B,C,H,I,J,K,L,X,Z) -> f68.13(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && L >= A] f42.10(A,B,C,H,I,J,K,L,X,Z) -> f42.9(A,B,C,H,I,J,K,1 + L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && A >= 1 + L] f42.10(A,B,C,H,I,J,K,L,X,Z) -> f42.10(A,B,C,H,I,J,K,1 + L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && A >= 1 + L] f42.10(A,B,C,H,I,J,K,L,X,Z) -> f42.11(A,B,C,H,I,J,K,1 + L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && A >= 1 + L] f42.10(A,B,C,H,I,J,K,L,X,Z) -> f42.12(A,B,C,H,I,J,K,1 + L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && A >= 1 + L] f42.11(A,B,C,H,I,J,K,L,X,Z) -> f47.14(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && A >= 1 + L && D1 >= 1] f42.11(A,B,C,H,I,J,K,L,X,Z) -> f47.15(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && A >= 1 + L && D1 >= 1] f42.12(A,B,C,H,I,J,K,L,X,Z) -> f47.14(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && A >= 1 + L && 0 >= 1 + D1] f42.12(A,B,C,H,I,J,K,L,X,Z) -> f47.15(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && A >= 1 + L && 0 >= 1 + D1] f68.13(A,B,C,H,I,J,K,L,X,Z) -> f152.16(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && -1*A + L >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f47.14(A,B,C,H,I,J,K,L,X,Z) -> f42.9(A,B,C,H,I,J,K,1 + L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -2 + B + -1*L >= 0 && -1 + -1*A + B >= 0 && -1 + A + -1*L >= 0 && 200 + -1*J >= 0 && K >= 1 + A] f47.14(A,B,C,H,I,J,K,L,X,Z) -> f42.10(A,B,C,H,I,J,K,1 + L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -2 + B + -1*L >= 0 && -1 + -1*A + B >= 0 && -1 + A + -1*L >= 0 && 200 + -1*J >= 0 && K >= 1 + A] f47.14(A,B,C,H,I,J,K,L,X,Z) -> f42.11(A,B,C,H,I,J,K,1 + L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -2 + B + -1*L >= 0 && -1 + -1*A + B >= 0 && -1 + A + -1*L >= 0 && 200 + -1*J >= 0 && K >= 1 + A] f47.14(A,B,C,H,I,J,K,L,X,Z) -> f42.12(A,B,C,H,I,J,K,1 + L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -2 + B + -1*L >= 0 && -1 + -1*A + B >= 0 && -1 + A + -1*L >= 0 && 200 + -1*J >= 0 && K >= 1 + A] f47.15(A,B,C,H,I,J,K,L,X,Z) -> f51.17(A,B,C,0,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -2 + B + -1*L >= 0 && -1 + -1*A + B >= 0 && -1 + A + -1*L >= 0 && 200 + -1*J >= 0 && A >= K] f152.16(A,B,C,H,I,J,K,L,X,Z) -> f164.19(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f152.16(A,B,C,H,I,J,K,L,X,Z) -> f164.20(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f51.17(A,B,C,H,I,J,K,L,X,Z) -> f58.18(A,B,C,D1,I,J,K,L,X,Z) [1 + -1*I >= 0 && 1 + H + -1*I >= 0 && 1 + -1*H + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1*H >= 0 && 200 + -1*H + -1*J >= 0 && H >= 0 && 200 + H + -1*J >= 0 && -2 + B + -1*L >= 0 && -1 + B + -1*K >= 0 && -1 + -1*A + B >= 0 && -1 + A + -1*L >= 0 && A + -1*K >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f58.18(A,B,C,H,I,J,K,L,X,Z) -> f47.14(A,B,C,H,I,J,1 + K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -2 + B + -1*L >= 0 && -1 + B + -1*K >= 0 && -1 + -1*A + B >= 0 && -1 + A + -1*L >= 0 && A + -1*K >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f58.18(A,B,C,H,I,J,K,L,X,Z) -> f47.15(A,B,C,H,I,J,1 + K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -2 + B + -1*L >= 0 && -1 + B + -1*K >= 0 && -1 + -1*A + B >= 0 && -1 + A + -1*L >= 0 && A + -1*K >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f164.19(A,B,C,H,I,J,K,L,X,Z) -> f176.21(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && 200 + -1*J >= 0 && 0 >= B] f164.19(A,B,C,H,I,J,K,L,X,Z) -> f176.22(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && 200 + -1*J >= 0 && 0 >= B] f164.20(A,B,C,H,I,J,K,L,X,Z) -> f167.23(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && 200 + -1*J >= 0 && B >= 1] f164.20(A,B,C,H,I,J,K,L,X,Z) -> f167.24(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && 200 + -1*J >= 0 && B >= 1] f176.21(A,B,C,H,I,J,K,L,X,Z) -> f184.25(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f176.22(A,B,C,H,I,J,K,L,X,Z) -> f176.21(A,1 + B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && 200 + -1*J >= 0 && A >= B] f176.22(A,B,C,H,I,J,K,L,X,Z) -> f176.22(A,1 + B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && 200 + -1*J >= 0 && A >= B] f167.23(A,B,C,H,I,J,K,L,X,Z) -> f164.19(A,-1 + B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && B + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + B >= 0 && 199 + B + -1*J >= 0 && 200 + -1*J >= 0 && K >= 1 + B] f167.23(A,B,C,H,I,J,K,L,X,Z) -> f164.20(A,-1 + B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && B + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + B >= 0 && 199 + B + -1*J >= 0 && 200 + -1*J >= 0 && K >= 1 + B] f167.24(A,B,C,H,I,J,K,L,X,Z) -> f167.23(A,B,C,D1,I,J,1 + K,L,X,Z) [1 + -1*I >= 0 && B + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + B >= 0 && 199 + B + -1*J >= 0 && 200 + -1*J >= 0 && B >= K] f167.24(A,B,C,H,I,J,K,L,X,Z) -> f167.24(A,B,C,D1,I,J,1 + K,L,X,Z) [1 + -1*I >= 0 && B + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + B >= 0 && 199 + B + -1*J >= 0 && 200 + -1*J >= 0 && B >= K] f184.25(A,B,C,H,I,J,K,L,X,Z) -> f199.26(A,B,0,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f184.25(A,B,C,H,I,J,K,L,X,Z) -> f199.27(A,B,0,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f184.25(A,B,C,H,I,J,K,L,X,Z) -> f199.28(A,B,0,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f199.26(A,B,C,H,I,J,K,L,X,Z) -> f218.29(A,B,0,H,0,J,K,L,0,Z) [1 + -1*I >= 0 && 1 + C + -1*I >= 0 && 1 + -1*C + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1*C >= 0 && 200 + -1*C + -1*J >= 0 && C >= 0 && 200 + C + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f199.27(A,B,C,H,I,J,K,L,X,Z) -> f210.30(A,B,C,H,I,J,K,L,D1,Z) [1 + -1*I >= 0 && 1 + C + -1*I >= 0 && 1 + -1*C + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1*C >= 0 && 200 + -1*C + -1*J >= 0 && C >= 0 && 200 + C + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A && D1 >= 1] f199.28(A,B,C,H,I,J,K,L,X,Z) -> f210.30(A,B,C,H,I,J,K,L,D1,Z) [1 + -1*I >= 0 && 1 + C + -1*I >= 0 && 1 + -1*C + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1*C >= 0 && 200 + -1*C + -1*J >= 0 && C >= 0 && 200 + C + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A && 0 >= 1 + D1] f218.29(A,B,C,H,I,J,K,L,X,Z) -> f26.6(A,B,C,H,I,1 + J,K,L,X,Z) [-1*I >= 0 && C + -1*I >= 0 && -1*C + -1*I >= 0 && -1*I + X >= 0 && -1*I + -1*X >= 0 && 200 + -1*I + -1*J >= 0 && I >= 0 && C + I >= 0 && -1*C + I >= 0 && I + X >= 0 && I + -1*X >= 0 && 200 + I + -1*J >= 0 && -1*C >= 0 && -1*C + X >= 0 && -1*C + -1*X >= 0 && 200 + -1*C + -1*J >= 0 && C >= 0 && C + X >= 0 && C + -1*X >= 0 && 200 + C + -1*J >= 0 && -1*X >= 0 && 200 + -1*J + -1*X >= 0 && X >= 0 && 200 + -1*J + X >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f218.29(A,B,C,H,I,J,K,L,X,Z) -> f26.31(A,B,C,H,I,1 + J,K,L,X,Z) [-1*I >= 0 && C + -1*I >= 0 && -1*C + -1*I >= 0 && -1*I + X >= 0 && -1*I + -1*X >= 0 && 200 + -1*I + -1*J >= 0 && I >= 0 && C + I >= 0 && -1*C + I >= 0 && I + X >= 0 && I + -1*X >= 0 && 200 + I + -1*J >= 0 && -1*C >= 0 && -1*C + X >= 0 && -1*C + -1*X >= 0 && 200 + -1*C + -1*J >= 0 && C >= 0 && C + X >= 0 && C + -1*X >= 0 && 200 + C + -1*J >= 0 && -1*X >= 0 && 200 + -1*J + -1*X >= 0 && X >= 0 && 200 + -1*J + X >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f210.30(A,B,C,H,I,J,K,L,X,Z) -> f26.6(A,B,C,H,I,1 + J,K,L,X,Z) [1 + -1*I >= 0 && 1 + C + -1*I >= 0 && 1 + -1*C + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1*C >= 0 && 200 + -1*C + -1*J >= 0 && C >= 0 && 200 + C + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f210.30(A,B,C,H,I,J,K,L,X,Z) -> f26.7(A,B,C,H,I,1 + J,K,L,X,Z) [1 + -1*I >= 0 && 1 + C + -1*I >= 0 && 1 + -1*C + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1*C >= 0 && 200 + -1*C + -1*J >= 0 && C >= 0 && 200 + C + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f210.30(A,B,C,H,I,J,K,L,X,Z) -> f26.31(A,B,C,H,I,1 + J,K,L,X,Z) [1 + -1*I >= 0 && 1 + C + -1*I >= 0 && 1 + -1*C + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1*C >= 0 && 200 + -1*C + -1*J >= 0 && C >= 0 && 200 + C + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f210.30(A,B,C,H,I,J,K,L,X,Z) -> f26.32(A,B,C,H,I,1 + J,K,L,X,Z) [1 + -1*I >= 0 && 1 + C + -1*I >= 0 && 1 + -1*C + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1*C >= 0 && 200 + -1*C + -1*J >= 0 && C >= 0 && 200 + C + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f26.31(A,B,C,H,I,J,K,L,X,Z) -> f81.33(A,B,C,H,0,J,K,L,X,Z) [1 + -1*I >= 0 && -1 + -1*A + B >= 0 && 200 >= J && I = 0] f26.32(A,B,C,H,I,J,K,L,X,Z) -> f30.8(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && -1 + -1*A + B >= 0 && 0 >= 1 + I && 200 >= J] f81.33(A,B,C,H,I,J,K,L,X,Z) -> f87.34(A,B,C,H,I,J,K,L,X,Z) [-1*I >= 0 && 200 + -1*I + -1*J >= 0 && I >= 0 && 200 + I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f87.34(A,B,C,H,I,J,K,L,X,Z) -> f100.35(A,B,C,H,I,J,K,L,X,1) [-1*I >= 0 && 200 + -1*I + -1*J >= 0 && I >= 0 && 200 + I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f100.35(A,B,C,H,I,J,K,L,X,Z) -> f152.16(A,B,C,H,I,J,K,L,X,Z) [-1*I >= 0 && -1 + -1*I + Z >= 0 && 1 + -1*I + -1*Z >= 0 && 200 + -1*I + -1*J >= 0 && I >= 0 && -1 + I + Z >= 0 && 1 + I + -1*Z >= 0 && 200 + I + -1*J >= 0 && 1 + -1*Z >= 0 && 201 + -1*J + -1*Z >= 0 && -1 + Z >= 0 && 199 + -1*J + Z >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A && Z >= 1] f1.36(A,B,C,H,I,J,K,L,X,Z) -> exitus616(A,B,C,H,I,J,K,L,X,Z) True f1.36(A,B,C,H,I,J,K,L,X,Z) -> exitus616(A,B,C,H,I,J,K,L,X,Z) True f1.36(A,B,C,H,I,J,K,L,X,Z) -> exitus616(A,B,C,H,I,J,K,L,X,Z) True f1.36(A,B,C,H,I,J,K,L,X,Z) -> exitus616(A,B,C,H,I,J,K,L,X,Z) True f1.36(A,B,C,H,I,J,K,L,X,Z) -> exitus616(A,B,C,H,I,J,K,L,X,Z) True f1.36(A,B,C,H,I,J,K,L,X,Z) -> exitus616(A,B,C,H,I,J,K,L,X,Z) True f1.36(A,B,C,H,I,J,K,L,X,Z) -> exitus616(A,B,C,H,I,J,K,L,X,Z) True f1.36(A,B,C,H,I,J,K,L,X,Z) -> exitus616(A,B,C,H,I,J,K,L,X,Z) True f1.36(A,B,C,H,I,J,K,L,X,Z) -> exitus616(A,B,C,H,I,J,K,L,X,Z) True f1.36(A,B,C,H,I,J,K,L,X,Z) -> exitus616(A,B,C,H,I,J,K,L,X,Z) True f1.36(A,B,C,H,I,J,K,L,X,Z) -> exitus616(A,B,C,H,I,J,K,L,X,Z) True f1.36(A,B,C,H,I,J,K,L,X,Z) -> exitus616(A,B,C,H,I,J,K,L,X,Z) True f1.36(A,B,C,H,I,J,K,L,X,Z) -> exitus616(A,B,C,H,I,J,K,L,X,Z) True f1.36(A,B,C,H,I,J,K,L,X,Z) -> exitus616(A,B,C,H,I,J,K,L,X,Z) True f1.36(A,B,C,H,I,J,K,L,X,Z) -> exitus616(A,B,C,H,I,J,K,L,X,Z) True f1.36(A,B,C,H,I,J,K,L,X,Z) -> exitus616(A,B,C,H,I,J,K,L,X,Z) True f1.36(A,B,C,H,I,J,K,L,X,Z) -> exitus616(A,B,C,H,I,J,K,L,X,Z) True f1.36(A,B,C,H,I,J,K,L,X,Z) -> exitus616(A,B,C,H,I,J,K,L,X,Z) True f1.36(A,B,C,H,I,J,K,L,X,Z) -> exitus616(A,B,C,H,I,J,K,L,X,Z) True f1.36(A,B,C,H,I,J,K,L,X,Z) -> exitus616(A,B,C,H,I,J,K,L,X,Z) True Signature: {(exitus616,10) ;(f1.36,10) ;(f100.35,10) ;(f15.5,10) ;(f152.16,10) ;(f164.19,10) ;(f164.20,10) ;(f167.23,10) ;(f167.24,10) ;(f176.21,10) ;(f176.22,10) ;(f184.25,10) ;(f199.26,10) ;(f199.27,10) ;(f199.28,10) ;(f2.1,10) ;(f2.2,10) ;(f2.3,10) ;(f2.4,10) ;(f210.30,10) ;(f218.29,10) ;(f26.31,10) ;(f26.32,10) ;(f26.6,10) ;(f26.7,10) ;(f30.8,10) ;(f42.10,10) ;(f42.11,10) ;(f42.12,10) ;(f42.9,10) ;(f47.14,10) ;(f47.15,10) ;(f51.17,10) ;(f58.18,10) ;(f68.13,10) ;(f81.33,10) ;(f87.34,10) ;(start.0,10)} Rule Graph: [0->{4},1->{5},2->{6,7,8,9},3->{10,11,12,13},4->{14,15},5->{70,74,78,82,86},6->{4},7->{5},8->{6,7,8,9} ,9->{10,11,12,13},10->{4},11->{5},12->{6,7,8,9},13->{10,11,12,13},14->{16},15->{17},16->{71,72,73,75,76,77 ,79,80,81,83,84,85,87,88,89},17->{18,19,20,21},18->{22},19->{23,24,25,26},20->{27,28},21->{29,30},22->{31} ,23->{22},24->{23,24,25,26},25->{27,28},26->{29,30},27->{32,33,34,35},28->{36},29->{32,33,34,35},30->{36} ,31->{37,38},32->{22},33->{23,24,25,26},34->{27,28},35->{29,30},36->{39},37->{42,43},38->{44,45},39->{40,41} ,40->{32,33,34,35},41->{36},42->{46},43->{47,48},44->{49,50},45->{51,52},46->{53,54,55},47->{46},48->{47,48} ,49->{42,43},50->{44,45},51->{49,50},52->{51,52},53->{56},54->{57},55->{58},56->{59,60},57->{61,62,63,64} ,58->{61,62,63,64},59->{16},60->{65},61->{16},62->{17},63->{65},64->{66},65->{67},66->{18,19,20,21},67->{68} ,68->{69},69->{37,38}] + 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,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82,83,84,85,86,87,88,89] | +- p:[8,12,9,13] c: [8,9,12,13] | `- p:[17,62,57,54,46,42,37,31,22,18,66,64,58,55,23,19,24,33,27,20,25,34,29,21,26,35,40,39,36,28,30,41,32,69,68,67,65,60,56,53,63,49,44,38,50,51,45,52,47,43,48] c: [17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,46,47,49,53,54,55,56,57,58,60,62,63,64,65,66,67,68,69] | +- p:[48] c: [48] | `- p:[44,50,51,45,52] c: [44,45,50,51,52] * Step 7: AbstractSize MAYBE + Considered Problem: (Rules: start.0(A,B,C,H,I,J,K,L,X,Z) -> f2.1(A,B,C,H,I,J,K,L,X,Z) True start.0(A,B,C,H,I,J,K,L,X,Z) -> f2.2(A,B,C,H,I,J,K,L,X,Z) True start.0(A,B,C,H,I,J,K,L,X,Z) -> f2.3(A,B,C,H,I,J,K,L,X,Z) True start.0(A,B,C,H,I,J,K,L,X,Z) -> f2.4(A,B,C,H,I,J,K,L,X,Z) True f2.1(A,B,C,H,I,J,K,L,X,Z) -> f15.5(A,B,C,H,I,J,K,L,X,Z) [B >= 1 + A && C >= 1] f2.2(A,B,C,H,I,J,K,L,X,Z) -> f1.36(A,B,C,H,I,J,K,L,X,Z) [B >= 1 + A && 0 >= C] f2.3(A,B,C,H,I,J,K,L,X,Z) -> f2.1(A,1 + B,E1,H,I,J,K,L,X,Z) [A >= B && D1 >= 1 + C] f2.3(A,B,C,H,I,J,K,L,X,Z) -> f2.2(A,1 + B,E1,H,I,J,K,L,X,Z) [A >= B && D1 >= 1 + C] f2.3(A,B,C,H,I,J,K,L,X,Z) -> f2.3(A,1 + B,E1,H,I,J,K,L,X,Z) [A >= B && D1 >= 1 + C] f2.3(A,B,C,H,I,J,K,L,X,Z) -> f2.4(A,1 + B,E1,H,I,J,K,L,X,Z) [A >= B && D1 >= 1 + C] f2.4(A,B,C,H,I,J,K,L,X,Z) -> f2.1(A,1 + B,C,H,I,J,K,L,X,Z) [A >= B && C >= D1] f2.4(A,B,C,H,I,J,K,L,X,Z) -> f2.2(A,1 + B,C,H,I,J,K,L,X,Z) [A >= B && C >= D1] f2.4(A,B,C,H,I,J,K,L,X,Z) -> f2.3(A,1 + B,C,H,I,J,K,L,X,Z) [A >= B && C >= D1] f2.4(A,B,C,H,I,J,K,L,X,Z) -> f2.4(A,1 + B,C,H,I,J,K,L,X,Z) [A >= B && C >= D1] f15.5(A,B,C,H,I,J,K,L,X,Z) -> f26.6(A,B,C,H,1,J,K,L,X,Z) [-1 + C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A] f15.5(A,B,C,H,I,J,K,L,X,Z) -> f26.7(A,B,C,H,1,J,K,L,X,Z) [-1 + C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A] f26.6(A,B,C,H,I,J,K,L,X,Z) -> f1.36(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && -1 + -1*A + B >= 0 && J >= 201] f26.7(A,B,C,H,I,J,K,L,X,Z) -> f30.8(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && -1 + -1*A + B >= 0 && I >= 1 && 200 >= J] f30.8(A,B,C,H,I,J,K,L,X,Z) -> f42.9(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f30.8(A,B,C,H,I,J,K,L,X,Z) -> f42.10(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f30.8(A,B,C,H,I,J,K,L,X,Z) -> f42.11(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f30.8(A,B,C,H,I,J,K,L,X,Z) -> f42.12(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f42.9(A,B,C,H,I,J,K,L,X,Z) -> f68.13(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && L >= A] f42.10(A,B,C,H,I,J,K,L,X,Z) -> f42.9(A,B,C,H,I,J,K,1 + L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && A >= 1 + L] f42.10(A,B,C,H,I,J,K,L,X,Z) -> f42.10(A,B,C,H,I,J,K,1 + L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && A >= 1 + L] f42.10(A,B,C,H,I,J,K,L,X,Z) -> f42.11(A,B,C,H,I,J,K,1 + L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && A >= 1 + L] f42.10(A,B,C,H,I,J,K,L,X,Z) -> f42.12(A,B,C,H,I,J,K,1 + L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && A >= 1 + L] f42.11(A,B,C,H,I,J,K,L,X,Z) -> f47.14(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && A >= 1 + L && D1 >= 1] f42.11(A,B,C,H,I,J,K,L,X,Z) -> f47.15(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && A >= 1 + L && D1 >= 1] f42.12(A,B,C,H,I,J,K,L,X,Z) -> f47.14(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && A >= 1 + L && 0 >= 1 + D1] f42.12(A,B,C,H,I,J,K,L,X,Z) -> f47.15(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && A >= 1 + L && 0 >= 1 + D1] f68.13(A,B,C,H,I,J,K,L,X,Z) -> f152.16(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && -1*A + L >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f47.14(A,B,C,H,I,J,K,L,X,Z) -> f42.9(A,B,C,H,I,J,K,1 + L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -2 + B + -1*L >= 0 && -1 + -1*A + B >= 0 && -1 + A + -1*L >= 0 && 200 + -1*J >= 0 && K >= 1 + A] f47.14(A,B,C,H,I,J,K,L,X,Z) -> f42.10(A,B,C,H,I,J,K,1 + L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -2 + B + -1*L >= 0 && -1 + -1*A + B >= 0 && -1 + A + -1*L >= 0 && 200 + -1*J >= 0 && K >= 1 + A] f47.14(A,B,C,H,I,J,K,L,X,Z) -> f42.11(A,B,C,H,I,J,K,1 + L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -2 + B + -1*L >= 0 && -1 + -1*A + B >= 0 && -1 + A + -1*L >= 0 && 200 + -1*J >= 0 && K >= 1 + A] f47.14(A,B,C,H,I,J,K,L,X,Z) -> f42.12(A,B,C,H,I,J,K,1 + L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -2 + B + -1*L >= 0 && -1 + -1*A + B >= 0 && -1 + A + -1*L >= 0 && 200 + -1*J >= 0 && K >= 1 + A] f47.15(A,B,C,H,I,J,K,L,X,Z) -> f51.17(A,B,C,0,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -2 + B + -1*L >= 0 && -1 + -1*A + B >= 0 && -1 + A + -1*L >= 0 && 200 + -1*J >= 0 && A >= K] f152.16(A,B,C,H,I,J,K,L,X,Z) -> f164.19(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f152.16(A,B,C,H,I,J,K,L,X,Z) -> f164.20(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f51.17(A,B,C,H,I,J,K,L,X,Z) -> f58.18(A,B,C,D1,I,J,K,L,X,Z) [1 + -1*I >= 0 && 1 + H + -1*I >= 0 && 1 + -1*H + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1*H >= 0 && 200 + -1*H + -1*J >= 0 && H >= 0 && 200 + H + -1*J >= 0 && -2 + B + -1*L >= 0 && -1 + B + -1*K >= 0 && -1 + -1*A + B >= 0 && -1 + A + -1*L >= 0 && A + -1*K >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f58.18(A,B,C,H,I,J,K,L,X,Z) -> f47.14(A,B,C,H,I,J,1 + K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -2 + B + -1*L >= 0 && -1 + B + -1*K >= 0 && -1 + -1*A + B >= 0 && -1 + A + -1*L >= 0 && A + -1*K >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f58.18(A,B,C,H,I,J,K,L,X,Z) -> f47.15(A,B,C,H,I,J,1 + K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -2 + B + -1*L >= 0 && -1 + B + -1*K >= 0 && -1 + -1*A + B >= 0 && -1 + A + -1*L >= 0 && A + -1*K >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f164.19(A,B,C,H,I,J,K,L,X,Z) -> f176.21(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && 200 + -1*J >= 0 && 0 >= B] f164.19(A,B,C,H,I,J,K,L,X,Z) -> f176.22(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && 200 + -1*J >= 0 && 0 >= B] f164.20(A,B,C,H,I,J,K,L,X,Z) -> f167.23(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && 200 + -1*J >= 0 && B >= 1] f164.20(A,B,C,H,I,J,K,L,X,Z) -> f167.24(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && 200 + -1*J >= 0 && B >= 1] f176.21(A,B,C,H,I,J,K,L,X,Z) -> f184.25(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f176.22(A,B,C,H,I,J,K,L,X,Z) -> f176.21(A,1 + B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && 200 + -1*J >= 0 && A >= B] f176.22(A,B,C,H,I,J,K,L,X,Z) -> f176.22(A,1 + B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && 200 + -1*J >= 0 && A >= B] f167.23(A,B,C,H,I,J,K,L,X,Z) -> f164.19(A,-1 + B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && B + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + B >= 0 && 199 + B + -1*J >= 0 && 200 + -1*J >= 0 && K >= 1 + B] f167.23(A,B,C,H,I,J,K,L,X,Z) -> f164.20(A,-1 + B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && B + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + B >= 0 && 199 + B + -1*J >= 0 && 200 + -1*J >= 0 && K >= 1 + B] f167.24(A,B,C,H,I,J,K,L,X,Z) -> f167.23(A,B,C,D1,I,J,1 + K,L,X,Z) [1 + -1*I >= 0 && B + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + B >= 0 && 199 + B + -1*J >= 0 && 200 + -1*J >= 0 && B >= K] f167.24(A,B,C,H,I,J,K,L,X,Z) -> f167.24(A,B,C,D1,I,J,1 + K,L,X,Z) [1 + -1*I >= 0 && B + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + B >= 0 && 199 + B + -1*J >= 0 && 200 + -1*J >= 0 && B >= K] f184.25(A,B,C,H,I,J,K,L,X,Z) -> f199.26(A,B,0,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f184.25(A,B,C,H,I,J,K,L,X,Z) -> f199.27(A,B,0,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f184.25(A,B,C,H,I,J,K,L,X,Z) -> f199.28(A,B,0,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f199.26(A,B,C,H,I,J,K,L,X,Z) -> f218.29(A,B,0,H,0,J,K,L,0,Z) [1 + -1*I >= 0 && 1 + C + -1*I >= 0 && 1 + -1*C + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1*C >= 0 && 200 + -1*C + -1*J >= 0 && C >= 0 && 200 + C + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f199.27(A,B,C,H,I,J,K,L,X,Z) -> f210.30(A,B,C,H,I,J,K,L,D1,Z) [1 + -1*I >= 0 && 1 + C + -1*I >= 0 && 1 + -1*C + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1*C >= 0 && 200 + -1*C + -1*J >= 0 && C >= 0 && 200 + C + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A && D1 >= 1] f199.28(A,B,C,H,I,J,K,L,X,Z) -> f210.30(A,B,C,H,I,J,K,L,D1,Z) [1 + -1*I >= 0 && 1 + C + -1*I >= 0 && 1 + -1*C + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1*C >= 0 && 200 + -1*C + -1*J >= 0 && C >= 0 && 200 + C + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A && 0 >= 1 + D1] f218.29(A,B,C,H,I,J,K,L,X,Z) -> f26.6(A,B,C,H,I,1 + J,K,L,X,Z) [-1*I >= 0 && C + -1*I >= 0 && -1*C + -1*I >= 0 && -1*I + X >= 0 && -1*I + -1*X >= 0 && 200 + -1*I + -1*J >= 0 && I >= 0 && C + I >= 0 && -1*C + I >= 0 && I + X >= 0 && I + -1*X >= 0 && 200 + I + -1*J >= 0 && -1*C >= 0 && -1*C + X >= 0 && -1*C + -1*X >= 0 && 200 + -1*C + -1*J >= 0 && C >= 0 && C + X >= 0 && C + -1*X >= 0 && 200 + C + -1*J >= 0 && -1*X >= 0 && 200 + -1*J + -1*X >= 0 && X >= 0 && 200 + -1*J + X >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f218.29(A,B,C,H,I,J,K,L,X,Z) -> f26.31(A,B,C,H,I,1 + J,K,L,X,Z) [-1*I >= 0 && C + -1*I >= 0 && -1*C + -1*I >= 0 && -1*I + X >= 0 && -1*I + -1*X >= 0 && 200 + -1*I + -1*J >= 0 && I >= 0 && C + I >= 0 && -1*C + I >= 0 && I + X >= 0 && I + -1*X >= 0 && 200 + I + -1*J >= 0 && -1*C >= 0 && -1*C + X >= 0 && -1*C + -1*X >= 0 && 200 + -1*C + -1*J >= 0 && C >= 0 && C + X >= 0 && C + -1*X >= 0 && 200 + C + -1*J >= 0 && -1*X >= 0 && 200 + -1*J + -1*X >= 0 && X >= 0 && 200 + -1*J + X >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f210.30(A,B,C,H,I,J,K,L,X,Z) -> f26.6(A,B,C,H,I,1 + J,K,L,X,Z) [1 + -1*I >= 0 && 1 + C + -1*I >= 0 && 1 + -1*C + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1*C >= 0 && 200 + -1*C + -1*J >= 0 && C >= 0 && 200 + C + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f210.30(A,B,C,H,I,J,K,L,X,Z) -> f26.7(A,B,C,H,I,1 + J,K,L,X,Z) [1 + -1*I >= 0 && 1 + C + -1*I >= 0 && 1 + -1*C + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1*C >= 0 && 200 + -1*C + -1*J >= 0 && C >= 0 && 200 + C + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f210.30(A,B,C,H,I,J,K,L,X,Z) -> f26.31(A,B,C,H,I,1 + J,K,L,X,Z) [1 + -1*I >= 0 && 1 + C + -1*I >= 0 && 1 + -1*C + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1*C >= 0 && 200 + -1*C + -1*J >= 0 && C >= 0 && 200 + C + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f210.30(A,B,C,H,I,J,K,L,X,Z) -> f26.32(A,B,C,H,I,1 + J,K,L,X,Z) [1 + -1*I >= 0 && 1 + C + -1*I >= 0 && 1 + -1*C + -1*I >= 0 && 201 + -1*I + -1*J >= 0 && -1*C >= 0 && 200 + -1*C + -1*J >= 0 && C >= 0 && 200 + C + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f26.31(A,B,C,H,I,J,K,L,X,Z) -> f81.33(A,B,C,H,0,J,K,L,X,Z) [1 + -1*I >= 0 && -1 + -1*A + B >= 0 && 200 >= J && I = 0] f26.32(A,B,C,H,I,J,K,L,X,Z) -> f30.8(A,B,C,H,I,J,K,L,X,Z) [1 + -1*I >= 0 && -1 + -1*A + B >= 0 && 0 >= 1 + I && 200 >= J] f81.33(A,B,C,H,I,J,K,L,X,Z) -> f87.34(A,B,C,H,I,J,K,L,X,Z) [-1*I >= 0 && 200 + -1*I + -1*J >= 0 && I >= 0 && 200 + I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f87.34(A,B,C,H,I,J,K,L,X,Z) -> f100.35(A,B,C,H,I,J,K,L,X,1) [-1*I >= 0 && 200 + -1*I + -1*J >= 0 && I >= 0 && 200 + I + -1*J >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A] f100.35(A,B,C,H,I,J,K,L,X,Z) -> f152.16(A,B,C,H,I,J,K,L,X,Z) [-1*I >= 0 && -1 + -1*I + Z >= 0 && 1 + -1*I + -1*Z >= 0 && 200 + -1*I + -1*J >= 0 && I >= 0 && -1 + I + Z >= 0 && 1 + I + -1*Z >= 0 && 200 + I + -1*J >= 0 && 1 + -1*Z >= 0 && 201 + -1*J + -1*Z >= 0 && -1 + Z >= 0 && 199 + -1*J + Z >= 0 && -1 + -1*A + B >= 0 && 200 + -1*J >= 0 && B >= 1 + A && Z >= 1] f1.36(A,B,C,H,I,J,K,L,X,Z) -> exitus616(A,B,C,H,I,J,K,L,X,Z) True f1.36(A,B,C,H,I,J,K,L,X,Z) -> exitus616(A,B,C,H,I,J,K,L,X,Z) True f1.36(A,B,C,H,I,J,K,L,X,Z) -> exitus616(A,B,C,H,I,J,K,L,X,Z) True f1.36(A,B,C,H,I,J,K,L,X,Z) -> exitus616(A,B,C,H,I,J,K,L,X,Z) True f1.36(A,B,C,H,I,J,K,L,X,Z) -> exitus616(A,B,C,H,I,J,K,L,X,Z) True f1.36(A,B,C,H,I,J,K,L,X,Z) -> exitus616(A,B,C,H,I,J,K,L,X,Z) True f1.36(A,B,C,H,I,J,K,L,X,Z) -> exitus616(A,B,C,H,I,J,K,L,X,Z) True f1.36(A,B,C,H,I,J,K,L,X,Z) -> exitus616(A,B,C,H,I,J,K,L,X,Z) True f1.36(A,B,C,H,I,J,K,L,X,Z) -> exitus616(A,B,C,H,I,J,K,L,X,Z) True f1.36(A,B,C,H,I,J,K,L,X,Z) -> exitus616(A,B,C,H,I,J,K,L,X,Z) True f1.36(A,B,C,H,I,J,K,L,X,Z) -> exitus616(A,B,C,H,I,J,K,L,X,Z) True f1.36(A,B,C,H,I,J,K,L,X,Z) -> exitus616(A,B,C,H,I,J,K,L,X,Z) True f1.36(A,B,C,H,I,J,K,L,X,Z) -> exitus616(A,B,C,H,I,J,K,L,X,Z) True f1.36(A,B,C,H,I,J,K,L,X,Z) -> exitus616(A,B,C,H,I,J,K,L,X,Z) True f1.36(A,B,C,H,I,J,K,L,X,Z) -> exitus616(A,B,C,H,I,J,K,L,X,Z) True f1.36(A,B,C,H,I,J,K,L,X,Z) -> exitus616(A,B,C,H,I,J,K,L,X,Z) True f1.36(A,B,C,H,I,J,K,L,X,Z) -> exitus616(A,B,C,H,I,J,K,L,X,Z) True f1.36(A,B,C,H,I,J,K,L,X,Z) -> exitus616(A,B,C,H,I,J,K,L,X,Z) True f1.36(A,B,C,H,I,J,K,L,X,Z) -> exitus616(A,B,C,H,I,J,K,L,X,Z) True f1.36(A,B,C,H,I,J,K,L,X,Z) -> exitus616(A,B,C,H,I,J,K,L,X,Z) True Signature: {(exitus616,10) ;(f1.36,10) ;(f100.35,10) ;(f15.5,10) ;(f152.16,10) ;(f164.19,10) ;(f164.20,10) ;(f167.23,10) ;(f167.24,10) ;(f176.21,10) ;(f176.22,10) ;(f184.25,10) ;(f199.26,10) ;(f199.27,10) ;(f199.28,10) ;(f2.1,10) ;(f2.2,10) ;(f2.3,10) ;(f2.4,10) ;(f210.30,10) ;(f218.29,10) ;(f26.31,10) ;(f26.32,10) ;(f26.6,10) ;(f26.7,10) ;(f30.8,10) ;(f42.10,10) ;(f42.11,10) ;(f42.12,10) ;(f42.9,10) ;(f47.14,10) ;(f47.15,10) ;(f51.17,10) ;(f58.18,10) ;(f68.13,10) ;(f81.33,10) ;(f87.34,10) ;(start.0,10)} Rule Graph: [0->{4},1->{5},2->{6,7,8,9},3->{10,11,12,13},4->{14,15},5->{70,74,78,82,86},6->{4},7->{5},8->{6,7,8,9} ,9->{10,11,12,13},10->{4},11->{5},12->{6,7,8,9},13->{10,11,12,13},14->{16},15->{17},16->{71,72,73,75,76,77 ,79,80,81,83,84,85,87,88,89},17->{18,19,20,21},18->{22},19->{23,24,25,26},20->{27,28},21->{29,30},22->{31} ,23->{22},24->{23,24,25,26},25->{27,28},26->{29,30},27->{32,33,34,35},28->{36},29->{32,33,34,35},30->{36} ,31->{37,38},32->{22},33->{23,24,25,26},34->{27,28},35->{29,30},36->{39},37->{42,43},38->{44,45},39->{40,41} ,40->{32,33,34,35},41->{36},42->{46},43->{47,48},44->{49,50},45->{51,52},46->{53,54,55},47->{46},48->{47,48} ,49->{42,43},50->{44,45},51->{49,50},52->{51,52},53->{56},54->{57},55->{58},56->{59,60},57->{61,62,63,64} ,58->{61,62,63,64},59->{16},60->{65},61->{16},62->{17},63->{65},64->{66},65->{67},66->{18,19,20,21},67->{68} ,68->{69},69->{37,38}] ,We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82,83,84,85,86,87,88,89] | +- p:[8,12,9,13] c: [8,9,12,13] | `- p:[17,62,57,54,46,42,37,31,22,18,66,64,58,55,23,19,24,33,27,20,25,34,29,21,26,35,40,39,36,28,30,41,32,69,68,67,65,60,56,53,63,49,44,38,50,51,45,52,47,43,48] c: [17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,46,47,49,53,54,55,56,57,58,60,62,63,64,65,66,67,68,69] | +- p:[48] c: [48] | `- p:[44,50,51,45,52] c: [44,45,50,51,52]) + Applied Processor: AbstractSize Minimize + Details: () * Step 8: AbstractFlow MAYBE + Considered Problem: Program: Domain: [A,B,C,H,I,J,K,L,X,Z,0.0,0.1,0.1.0,0.1.1] start.0 ~> f2.1 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] start.0 ~> f2.2 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] start.0 ~> f2.3 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] start.0 ~> f2.4 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f2.1 ~> f15.5 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f2.2 ~> f1.36 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f2.3 ~> f2.1 [A <= A, B <= K + B, C <= unknown, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f2.3 ~> f2.2 [A <= A, B <= K + B, C <= unknown, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f2.3 ~> f2.3 [A <= A, B <= K + B, C <= unknown, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f2.3 ~> f2.4 [A <= A, B <= K + B, C <= unknown, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f2.4 ~> f2.1 [A <= A, B <= K + B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f2.4 ~> f2.2 [A <= A, B <= K + B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f2.4 ~> f2.3 [A <= A, B <= K + B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f2.4 ~> f2.4 [A <= A, B <= K + B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f15.5 ~> f26.6 [A <= A, B <= B, C <= C, H <= H, I <= K, J <= J, K <= K, L <= L, X <= X, Z <= Z] f15.5 ~> f26.7 [A <= A, B <= B, C <= C, H <= H, I <= K, J <= J, K <= K, L <= L, X <= X, Z <= Z] f26.6 ~> f1.36 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f26.7 ~> f30.8 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f30.8 ~> f42.9 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f30.8 ~> f42.10 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f30.8 ~> f42.11 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f30.8 ~> f42.12 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f42.9 ~> f68.13 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f42.10 ~> f42.9 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= A + L, X <= X, Z <= Z] f42.10 ~> f42.10 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= A + L, X <= X, Z <= Z] f42.10 ~> f42.11 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= A + L, X <= X, Z <= Z] f42.10 ~> f42.12 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= A + L, X <= X, Z <= Z] f42.11 ~> f47.14 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f42.11 ~> f47.15 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f42.12 ~> f47.14 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f42.12 ~> f47.15 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f68.13 ~> f152.16 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f47.14 ~> f42.9 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= A + L, X <= X, Z <= Z] f47.14 ~> f42.10 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= A + L, X <= X, Z <= Z] f47.14 ~> f42.11 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= A + L, X <= X, Z <= Z] f47.14 ~> f42.12 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= A + L, X <= X, Z <= Z] f47.15 ~> f51.17 [A <= A, B <= B, C <= C, H <= 0*K, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f152.16 ~> f164.19 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f152.16 ~> f164.20 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f51.17 ~> f58.18 [A <= A, B <= B, C <= C, H <= unknown, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f58.18 ~> f47.14 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K + K, L <= L, X <= X, Z <= Z] f58.18 ~> f47.15 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K + K, L <= L, X <= X, Z <= Z] f164.19 ~> f176.21 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f164.19 ~> f176.22 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f164.20 ~> f167.23 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f164.20 ~> f167.24 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f176.21 ~> f184.25 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f176.22 ~> f176.21 [A <= A, B <= K + B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f176.22 ~> f176.22 [A <= A, B <= K + B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f167.23 ~> f164.19 [A <= A, B <= K, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f167.23 ~> f164.20 [A <= A, B <= K, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f167.24 ~> f167.23 [A <= A, B <= B, C <= C, H <= unknown, I <= I, J <= J, K <= B + K, L <= L, X <= X, Z <= Z] f167.24 ~> f167.24 [A <= A, B <= B, C <= C, H <= unknown, I <= I, J <= J, K <= B + K, L <= L, X <= X, Z <= Z] f184.25 ~> f199.26 [A <= A, B <= B, C <= 0*K, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f184.25 ~> f199.27 [A <= A, B <= B, C <= 0*K, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f184.25 ~> f199.28 [A <= A, B <= B, C <= 0*K, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f199.26 ~> f218.29 [A <= A, B <= B, C <= 0*K, H <= H, I <= 0*K, J <= J, K <= K, L <= L, X <= 0*K, Z <= Z] f199.27 ~> f210.30 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= unknown, Z <= Z] f199.28 ~> f210.30 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= unknown, Z <= Z] f218.29 ~> f26.6 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= K + J, K <= K, L <= L, X <= X, Z <= Z] f218.29 ~> f26.31 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= K + J, K <= K, L <= L, X <= X, Z <= Z] f210.30 ~> f26.6 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= K + J, K <= K, L <= L, X <= X, Z <= Z] f210.30 ~> f26.7 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= K + J, K <= K, L <= L, X <= X, Z <= Z] f210.30 ~> f26.31 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= K + J, K <= K, L <= L, X <= X, Z <= Z] f210.30 ~> f26.32 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= K + J, K <= K, L <= L, X <= X, Z <= Z] f26.31 ~> f81.33 [A <= A, B <= B, C <= C, H <= H, I <= 0*K, J <= J, K <= K, L <= L, X <= X, Z <= Z] f26.32 ~> f30.8 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f81.33 ~> f87.34 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f87.34 ~> f100.35 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= K] f100.35 ~> f152.16 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f1.36 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f1.36 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f1.36 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f1.36 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f1.36 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f1.36 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f1.36 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f1.36 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f1.36 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f1.36 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f1.36 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f1.36 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f1.36 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f1.36 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f1.36 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f1.36 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f1.36 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f1.36 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f1.36 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f1.36 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] + Loop: [0.0 <= K + A + B] f2.3 ~> f2.3 [A <= A, B <= K + B, C <= unknown, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f2.4 ~> f2.3 [A <= A, B <= K + B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f2.3 ~> f2.4 [A <= A, B <= K + B, C <= unknown, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f2.4 ~> f2.4 [A <= A, B <= K + B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] + Loop: [0.1 <= 201*K + A + J + K + L] f26.7 ~> f30.8 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f210.30 ~> f26.7 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= K + J, K <= K, L <= L, X <= X, Z <= Z] f199.27 ~> f210.30 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= unknown, Z <= Z] f184.25 ~> f199.27 [A <= A, B <= B, C <= 0*K, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f176.21 ~> f184.25 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f164.19 ~> f176.21 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f152.16 ~> f164.19 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f68.13 ~> f152.16 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f42.9 ~> f68.13 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f30.8 ~> f42.9 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f26.32 ~> f30.8 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f210.30 ~> f26.32 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= K + J, K <= K, L <= L, X <= X, Z <= Z] f199.28 ~> f210.30 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= unknown, Z <= Z] f184.25 ~> f199.28 [A <= A, B <= B, C <= 0*K, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f42.10 ~> f42.9 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= A + L, X <= X, Z <= Z] f30.8 ~> f42.10 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f42.10 ~> f42.10 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= A + L, X <= X, Z <= Z] f47.14 ~> f42.10 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= A + L, X <= X, Z <= Z] f42.11 ~> f47.14 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f30.8 ~> f42.11 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f42.10 ~> f42.11 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= A + L, X <= X, Z <= Z] f47.14 ~> f42.11 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= A + L, X <= X, Z <= Z] f42.12 ~> f47.14 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f30.8 ~> f42.12 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f42.10 ~> f42.12 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= A + L, X <= X, Z <= Z] f47.14 ~> f42.12 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= A + L, X <= X, Z <= Z] f58.18 ~> f47.14 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K + K, L <= L, X <= X, Z <= Z] f51.17 ~> f58.18 [A <= A, B <= B, C <= C, H <= unknown, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f47.15 ~> f51.17 [A <= A, B <= B, C <= C, H <= 0*K, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f42.11 ~> f47.15 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f42.12 ~> f47.15 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f58.18 ~> f47.15 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K + K, L <= L, X <= X, Z <= Z] f47.14 ~> f42.9 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= A + L, X <= X, Z <= Z] f100.35 ~> f152.16 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f87.34 ~> f100.35 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= K] f81.33 ~> f87.34 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f26.31 ~> f81.33 [A <= A, B <= B, C <= C, H <= H, I <= 0*K, J <= J, K <= K, L <= L, X <= X, Z <= Z] f218.29 ~> f26.31 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= K + J, K <= K, L <= L, X <= X, Z <= Z] f199.26 ~> f218.29 [A <= A, B <= B, C <= 0*K, H <= H, I <= 0*K, J <= J, K <= K, L <= L, X <= 0*K, Z <= Z] f184.25 ~> f199.26 [A <= A, B <= B, C <= 0*K, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f210.30 ~> f26.31 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= K + J, K <= K, L <= L, X <= X, Z <= Z] f167.23 ~> f164.19 [A <= A, B <= K, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f164.20 ~> f167.23 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f152.16 ~> f164.20 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f167.23 ~> f164.20 [A <= A, B <= K, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f167.24 ~> f167.23 [A <= A, B <= B, C <= C, H <= unknown, I <= I, J <= J, K <= B + K, L <= L, X <= X, Z <= Z] f164.20 ~> f167.24 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f167.24 ~> f167.24 [A <= A, B <= B, C <= C, H <= unknown, I <= I, J <= J, K <= B + K, L <= L, X <= X, Z <= Z] f176.22 ~> f176.21 [A <= A, B <= K + B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f164.19 ~> f176.22 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f176.22 ~> f176.22 [A <= A, B <= K + B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] + Loop: [0.1.0 <= A + B] f176.22 ~> f176.22 [A <= A, B <= K + B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] + Loop: [0.1.1 <= B + I + K] f164.20 ~> f167.23 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f167.23 ~> f164.20 [A <= A, B <= K, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f167.24 ~> f167.23 [A <= A, B <= B, C <= C, H <= unknown, I <= I, J <= J, K <= B + K, L <= L, X <= X, Z <= Z] f164.20 ~> f167.24 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f167.24 ~> f167.24 [A <= A, B <= B, C <= C, H <= unknown, I <= I, J <= J, K <= B + K, L <= L, X <= X, Z <= Z] + Applied Processor: AbstractFlow + Details: () * Step 9: Lare MAYBE + Considered Problem: Program: Domain: [tick,huge,K,A,B,C,H,I,J,K,L,X,Z,0.0,0.1,0.1.0,0.1.1] start.0 ~> f2.1 [] start.0 ~> f2.2 [] start.0 ~> f2.3 [] start.0 ~> f2.4 [] f2.1 ~> f15.5 [] f2.2 ~> f1.36 [] f2.3 ~> f2.1 [huge ~=> C,B ~+> B,K ~+> B] f2.3 ~> f2.2 [huge ~=> C,B ~+> B,K ~+> B] f2.3 ~> f2.3 [huge ~=> C,B ~+> B,K ~+> B] f2.3 ~> f2.4 [huge ~=> C,B ~+> B,K ~+> B] f2.4 ~> f2.1 [B ~+> B,K ~+> B] f2.4 ~> f2.2 [B ~+> B,K ~+> B] f2.4 ~> f2.3 [B ~+> B,K ~+> B] f2.4 ~> f2.4 [B ~+> B,K ~+> B] f15.5 ~> f26.6 [K ~=> I] f15.5 ~> f26.7 [K ~=> I] f26.6 ~> f1.36 [] f26.7 ~> f30.8 [] f30.8 ~> f42.9 [] f30.8 ~> f42.10 [] f30.8 ~> f42.11 [] f30.8 ~> f42.12 [] f42.9 ~> f68.13 [] f42.10 ~> f42.9 [A ~+> L,L ~+> L] f42.10 ~> f42.10 [A ~+> L,L ~+> L] f42.10 ~> f42.11 [A ~+> L,L ~+> L] f42.10 ~> f42.12 [A ~+> L,L ~+> L] f42.11 ~> f47.14 [] f42.11 ~> f47.15 [] f42.12 ~> f47.14 [] f42.12 ~> f47.15 [] f68.13 ~> f152.16 [] f47.14 ~> f42.9 [A ~+> L,L ~+> L] f47.14 ~> f42.10 [A ~+> L,L ~+> L] f47.14 ~> f42.11 [A ~+> L,L ~+> L] f47.14 ~> f42.12 [A ~+> L,L ~+> L] f47.15 ~> f51.17 [K ~=> H] f152.16 ~> f164.19 [] f152.16 ~> f164.20 [] f51.17 ~> f58.18 [huge ~=> H] f58.18 ~> f47.14 [K ~+> K,K ~+> K] f58.18 ~> f47.15 [K ~+> K,K ~+> K] f164.19 ~> f176.21 [] f164.19 ~> f176.22 [] f164.20 ~> f167.23 [] f164.20 ~> f167.24 [] f176.21 ~> f184.25 [] f176.22 ~> f176.21 [B ~+> B,K ~+> B] f176.22 ~> f176.22 [B ~+> B,K ~+> B] f167.23 ~> f164.19 [K ~=> B] f167.23 ~> f164.20 [K ~=> B] f167.24 ~> f167.23 [huge ~=> H,B ~+> K,K ~+> K] f167.24 ~> f167.24 [huge ~=> H,B ~+> K,K ~+> K] f184.25 ~> f199.26 [K ~=> C] f184.25 ~> f199.27 [K ~=> C] f184.25 ~> f199.28 [K ~=> C] f199.26 ~> f218.29 [K ~=> C,K ~=> I,K ~=> X] f199.27 ~> f210.30 [huge ~=> X] f199.28 ~> f210.30 [huge ~=> X] f218.29 ~> f26.6 [J ~+> J,K ~+> J] f218.29 ~> f26.31 [J ~+> J,K ~+> J] f210.30 ~> f26.6 [J ~+> J,K ~+> J] f210.30 ~> f26.7 [J ~+> J,K ~+> J] f210.30 ~> f26.31 [J ~+> J,K ~+> J] f210.30 ~> f26.32 [J ~+> J,K ~+> J] f26.31 ~> f81.33 [K ~=> I] f26.32 ~> f30.8 [] f81.33 ~> f87.34 [] f87.34 ~> f100.35 [K ~=> Z] f100.35 ~> f152.16 [] f1.36 ~> exitus616 [] f1.36 ~> exitus616 [] f1.36 ~> exitus616 [] f1.36 ~> exitus616 [] f1.36 ~> exitus616 [] f1.36 ~> exitus616 [] f1.36 ~> exitus616 [] f1.36 ~> exitus616 [] f1.36 ~> exitus616 [] f1.36 ~> exitus616 [] f1.36 ~> exitus616 [] f1.36 ~> exitus616 [] f1.36 ~> exitus616 [] f1.36 ~> exitus616 [] f1.36 ~> exitus616 [] f1.36 ~> exitus616 [] f1.36 ~> exitus616 [] f1.36 ~> exitus616 [] f1.36 ~> exitus616 [] f1.36 ~> exitus616 [] + Loop: [A ~+> 0.0,B ~+> 0.0,K ~+> 0.0] f2.3 ~> f2.3 [huge ~=> C,B ~+> B,K ~+> B] f2.4 ~> f2.3 [B ~+> B,K ~+> B] f2.3 ~> f2.4 [huge ~=> C,B ~+> B,K ~+> B] f2.4 ~> f2.4 [B ~+> B,K ~+> B] + Loop: [A ~+> 0.1,J ~+> 0.1,K ~+> 0.1,L ~+> 0.1,K ~*> 0.1] f26.7 ~> f30.8 [] f210.30 ~> f26.7 [J ~+> J,K ~+> J] f199.27 ~> f210.30 [huge ~=> X] f184.25 ~> f199.27 [K ~=> C] f176.21 ~> f184.25 [] f164.19 ~> f176.21 [] f152.16 ~> f164.19 [] f68.13 ~> f152.16 [] f42.9 ~> f68.13 [] f30.8 ~> f42.9 [] f26.32 ~> f30.8 [] f210.30 ~> f26.32 [J ~+> J,K ~+> J] f199.28 ~> f210.30 [huge ~=> X] f184.25 ~> f199.28 [K ~=> C] f42.10 ~> f42.9 [A ~+> L,L ~+> L] f30.8 ~> f42.10 [] f42.10 ~> f42.10 [A ~+> L,L ~+> L] f47.14 ~> f42.10 [A ~+> L,L ~+> L] f42.11 ~> f47.14 [] f30.8 ~> f42.11 [] f42.10 ~> f42.11 [A ~+> L,L ~+> L] f47.14 ~> f42.11 [A ~+> L,L ~+> L] f42.12 ~> f47.14 [] f30.8 ~> f42.12 [] f42.10 ~> f42.12 [A ~+> L,L ~+> L] f47.14 ~> f42.12 [A ~+> L,L ~+> L] f58.18 ~> f47.14 [K ~+> K,K ~+> K] f51.17 ~> f58.18 [huge ~=> H] f47.15 ~> f51.17 [K ~=> H] f42.11 ~> f47.15 [] f42.12 ~> f47.15 [] f58.18 ~> f47.15 [K ~+> K,K ~+> K] f47.14 ~> f42.9 [A ~+> L,L ~+> L] f100.35 ~> f152.16 [] f87.34 ~> f100.35 [K ~=> Z] f81.33 ~> f87.34 [] f26.31 ~> f81.33 [K ~=> I] f218.29 ~> f26.31 [J ~+> J,K ~+> J] f199.26 ~> f218.29 [K ~=> C,K ~=> I,K ~=> X] f184.25 ~> f199.26 [K ~=> C] f210.30 ~> f26.31 [J ~+> J,K ~+> J] f167.23 ~> f164.19 [K ~=> B] f164.20 ~> f167.23 [] f152.16 ~> f164.20 [] f167.23 ~> f164.20 [K ~=> B] f167.24 ~> f167.23 [huge ~=> H,B ~+> K,K ~+> K] f164.20 ~> f167.24 [] f167.24 ~> f167.24 [huge ~=> H,B ~+> K,K ~+> K] f176.22 ~> f176.21 [B ~+> B,K ~+> B] f164.19 ~> f176.22 [] f176.22 ~> f176.22 [B ~+> B,K ~+> B] + Loop: [A ~+> 0.1.0,B ~+> 0.1.0] f176.22 ~> f176.22 [B ~+> B,K ~+> B] + Loop: [B ~+> 0.1.1,I ~+> 0.1.1,K ~+> 0.1.1] f164.20 ~> f167.23 [] f167.23 ~> f164.20 [K ~=> B] f167.24 ~> f167.23 [huge ~=> H,B ~+> K,K ~+> K] f164.20 ~> f167.24 [] f167.24 ~> f167.24 [huge ~=> H,B ~+> K,K ~+> K] + Applied Processor: Lare + Details: start.0 ~> exitus616 [K ~=> B ,K ~=> C ,K ~=> I ,K ~=> X ,K ~=> Z ,huge ~=> C ,huge ~=> H ,huge ~=> X ,A ~+> L ,A ~+> 0.0 ,A ~+> 0.1 ,A ~+> 0.1.0 ,A ~+> tick ,B ~+> B ,B ~+> K ,B ~+> 0.0 ,B ~+> 0.1.0 ,B ~+> 0.1.1 ,B ~+> tick ,J ~+> J ,J ~+> 0.1 ,J ~+> tick ,K ~+> B ,K ~+> K ,K ~+> 0.1 ,K ~+> 0.1.0 ,K ~+> 0.1.1 ,K ~+> tick ,L ~+> L ,L ~+> 0.1 ,L ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> J ,K ~+> K ,K ~+> 0.0 ,K ~+> 0.1.0 ,K ~+> 0.1.1 ,K ~+> tick ,A ~*> B ,A ~*> J ,A ~*> K ,A ~*> L ,A ~*> 0.0 ,A ~*> 0.1.0 ,A ~*> 0.1.1 ,A ~*> tick ,B ~*> B ,B ~*> K ,B ~*> 0.0 ,B ~*> 0.1.0 ,B ~*> 0.1.1 ,B ~*> tick ,J ~*> B ,J ~*> J ,J ~*> K ,J ~*> L ,J ~*> 0.1.0 ,J ~*> 0.1.1 ,J ~*> tick ,K ~*> B ,K ~*> J ,K ~*> K ,K ~*> L ,K ~*> 0.1.0 ,K ~*> 0.1.1 ,K ~*> tick ,L ~*> B ,L ~*> J ,L ~*> K ,L ~*> L ,L ~*> 0.1.0 ,L ~*> 0.1.1 ,L ~*> tick ,K ~*> B ,K ~*> J ,K ~*> K ,K ~*> L ,K ~*> 0.0 ,K ~*> 0.1 ,K ~*> 0.1.0 ,K ~*> 0.1.1 ,K ~*> tick ,A ~^> B ,A ~^> K ,A ~^> 0.1.0 ,A ~^> 0.1.1 ,A ~^> tick ,B ~^> B ,B ~^> K ,B ~^> 0.1.0 ,B ~^> 0.1.1 ,B ~^> tick ,J ~^> B ,J ~^> K ,J ~^> 0.1.0 ,J ~^> 0.1.1 ,J ~^> tick ,K ~^> B ,K ~^> K ,K ~^> 0.1.0 ,K ~^> 0.1.1 ,K ~^> tick ,L ~^> B ,L ~^> K ,L ~^> 0.1.0 ,L ~^> 0.1.1 ,L ~^> tick ,K ~^> B ,K ~^> K ,K ~^> 0.1.0 ,K ~^> 0.1.1 ,K ~^> tick] + f2.3> [huge ~=> C ,A ~+> 0.0 ,A ~+> tick ,B ~+> B ,B ~+> 0.0 ,B ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> 0.0 ,K ~+> tick ,A ~*> B ,B ~*> B ,K ~*> B] f2.4> [huge ~=> C ,A ~+> 0.0 ,A ~+> tick ,B ~+> B ,B ~+> 0.0 ,B ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> 0.0 ,K ~+> tick ,A ~*> B ,B ~*> B ,K ~*> B] f2.3> [huge ~=> C ,A ~+> 0.0 ,A ~+> tick ,B ~+> B ,B ~+> 0.0 ,B ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> 0.0 ,K ~+> tick ,A ~*> B ,B ~*> B ,K ~*> B] f2.4> [huge ~=> C ,A ~+> 0.0 ,A ~+> tick ,B ~+> B ,B ~+> 0.0 ,B ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> 0.0 ,K ~+> tick ,A ~*> B ,B ~*> B ,K ~*> B] + f210.30> [K ~=> B ,K ~=> C ,K ~=> I ,K ~=> X ,K ~=> Z ,huge ~=> H ,huge ~=> X ,A ~+> L ,A ~+> 0.1 ,A ~+> 0.1.0 ,A ~+> tick ,B ~+> B ,B ~+> K ,B ~+> 0.1.0 ,B ~+> 0.1.1 ,B ~+> tick ,I ~+> 0.1.1 ,I ~+> tick ,J ~+> J ,J ~+> 0.1 ,J ~+> tick ,K ~+> B ,K ~+> K ,K ~+> 0.1 ,K ~+> 0.1.0 ,K ~+> 0.1.1 ,K ~+> tick ,L ~+> L ,L ~+> 0.1 ,L ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> J ,K ~+> K ,K ~+> 0.1.0 ,K ~+> 0.1.1 ,K ~+> tick ,A ~*> B ,A ~*> J ,A ~*> K ,A ~*> L ,A ~*> 0.1.0 ,A ~*> 0.1.1 ,A ~*> tick ,B ~*> B ,B ~*> K ,B ~*> 0.1.0 ,B ~*> 0.1.1 ,B ~*> tick ,I ~*> B ,I ~*> K ,I ~*> 0.1.0 ,I ~*> 0.1.1 ,I ~*> tick ,J ~*> B ,J ~*> J ,J ~*> K ,J ~*> L ,J ~*> 0.1.0 ,J ~*> 0.1.1 ,J ~*> tick ,K ~*> B ,K ~*> J ,K ~*> K ,K ~*> L ,K ~*> 0.1.0 ,K ~*> 0.1.1 ,K ~*> tick ,L ~*> B ,L ~*> J ,L ~*> K ,L ~*> L ,L ~*> 0.1.0 ,L ~*> 0.1.1 ,L ~*> tick ,K ~*> B ,K ~*> J ,K ~*> K ,K ~*> L ,K ~*> 0.1 ,K ~*> 0.1.0 ,K ~*> 0.1.1 ,K ~*> tick ,A ~^> B ,A ~^> K ,A ~^> 0.1.0 ,A ~^> 0.1.1 ,A ~^> tick ,B ~^> B ,B ~^> K ,B ~^> 0.1.0 ,B ~^> 0.1.1 ,B ~^> tick ,I ~^> B ,I ~^> K ,I ~^> 0.1.0 ,I ~^> 0.1.1 ,I ~^> tick ,J ~^> B ,J ~^> K ,J ~^> 0.1.0 ,J ~^> 0.1.1 ,J ~^> tick ,K ~^> B ,K ~^> K ,K ~^> 0.1.0 ,K ~^> 0.1.1 ,K ~^> tick ,L ~^> B ,L ~^> K ,L ~^> 0.1.0 ,L ~^> 0.1.1 ,L ~^> tick ,K ~^> B ,K ~^> K ,K ~^> 0.1.0 ,K ~^> 0.1.1 ,K ~^> tick] f218.29> [K ~=> B ,K ~=> C ,K ~=> I ,K ~=> X ,K ~=> Z ,huge ~=> H ,huge ~=> X ,A ~+> L ,A ~+> 0.1 ,A ~+> 0.1.0 ,A ~+> tick ,B ~+> B ,B ~+> K ,B ~+> 0.1.0 ,B ~+> 0.1.1 ,B ~+> tick ,I ~+> 0.1.1 ,I ~+> tick ,J ~+> J ,J ~+> 0.1 ,J ~+> tick ,K ~+> B ,K ~+> K ,K ~+> 0.1 ,K ~+> 0.1.0 ,K ~+> 0.1.1 ,K ~+> tick ,L ~+> L ,L ~+> 0.1 ,L ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> J ,K ~+> K ,K ~+> 0.1.0 ,K ~+> 0.1.1 ,K ~+> tick ,A ~*> B ,A ~*> J ,A ~*> K ,A ~*> L ,A ~*> 0.1.0 ,A ~*> 0.1.1 ,A ~*> tick ,B ~*> B ,B ~*> K ,B ~*> 0.1.0 ,B ~*> 0.1.1 ,B ~*> tick ,I ~*> B ,I ~*> K ,I ~*> 0.1.0 ,I ~*> 0.1.1 ,I ~*> tick ,J ~*> B ,J ~*> J ,J ~*> K ,J ~*> L ,J ~*> 0.1.0 ,J ~*> 0.1.1 ,J ~*> tick ,K ~*> B ,K ~*> J ,K ~*> K ,K ~*> L ,K ~*> 0.1.0 ,K ~*> 0.1.1 ,K ~*> tick ,L ~*> B ,L ~*> J ,L ~*> K ,L ~*> L ,L ~*> 0.1.0 ,L ~*> 0.1.1 ,L ~*> tick ,K ~*> B ,K ~*> J ,K ~*> K ,K ~*> L ,K ~*> 0.1 ,K ~*> 0.1.0 ,K ~*> 0.1.1 ,K ~*> tick ,A ~^> B ,A ~^> K ,A ~^> 0.1.0 ,A ~^> 0.1.1 ,A ~^> tick ,B ~^> B ,B ~^> K ,B ~^> 0.1.0 ,B ~^> 0.1.1 ,B ~^> tick ,I ~^> B ,I ~^> K ,I ~^> 0.1.0 ,I ~^> 0.1.1 ,I ~^> tick ,J ~^> B ,J ~^> K ,J ~^> 0.1.0 ,J ~^> 0.1.1 ,J ~^> tick ,K ~^> B ,K ~^> K ,K ~^> 0.1.0 ,K ~^> 0.1.1 ,K ~^> tick ,L ~^> B ,L ~^> K ,L ~^> 0.1.0 ,L ~^> 0.1.1 ,L ~^> tick ,K ~^> B ,K ~^> K ,K ~^> 0.1.0 ,K ~^> 0.1.1 ,K ~^> tick] + f176.22> [A ~+> 0.1.0 ,A ~+> tick ,B ~+> B ,B ~+> 0.1.0 ,B ~+> tick ,tick ~+> tick ,K ~+> B ,A ~*> B ,B ~*> B ,K ~*> B] + f167.23> [K ~=> B ,huge ~=> H ,B ~+> B ,B ~+> K ,B ~+> 0.1.1 ,B ~+> tick ,I ~+> 0.1.1 ,I ~+> tick ,K ~+> B ,K ~+> K ,K ~+> 0.1.1 ,K ~+> tick ,tick ~+> tick ,B ~*> B ,B ~*> K ,I ~*> B ,I ~*> K ,K ~*> B ,K ~*> K ,B ~^> B ,B ~^> K ,I ~^> B ,I ~^> K ,K ~^> B ,K ~^> K] YES(?,PRIMREC)