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: TrivialSCCs 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: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 3: 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,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,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,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,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 4: AddSinks 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,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,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,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,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: AddSinks + Details: () * Step 5: 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] 36. f2(A,B,C,H,I,J,K,L,X,Z) -> exitus616(A,B,C,H,I,J,K,L,X,Z) True (?,1) 37. f26(A,B,C,H,I,J,K,L,X,Z) -> exitus616(A,B,C,H,I,J,K,L,X,Z) True (?,1) Signature: {(exitus616,10) ;(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,36},1->{5},2->{},3->{1,2,3,4,36},4->{1,2,3,4,36},5->{6,7,31,32,37},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,37},30->{6,7,31,32,37},31->{33},32->{8},33->{34},34->{35} ,35->{16},36->{},37->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(5,31),(5,32),(29,7),(29,32)] * Step 6: LooptreeTransformer 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] 36. f2(A,B,C,H,I,J,K,L,X,Z) -> exitus616(A,B,C,H,I,J,K,L,X,Z) True (?,1) 37. f26(A,B,C,H,I,J,K,L,X,Z) -> exitus616(A,B,C,H,I,J,K,L,X,Z) True (?,1) Signature: {(exitus616,10) ;(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,36},1->{5},2->{},3->{1,2,3,4,36},4->{1,2,3,4,36},5->{6,7,37},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,37},30->{6,7,31,32,37},31->{33},32->{8},33->{34},34->{35},35->{16},36->{} ,37->{}] + Applied Processor: LooptreeTransformer + 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] | +- p:[3,4] c: [4] | | | `- p:[3] c: [3] | `- p:[7,30,27,25,21,19,16,13,9,8,32,10,14,11,12,18,17,15,35,34,33,31,29,26,23,20,24,22,28] c: [35] | `- p:[7,30,27,25,21,19,16,13,9,8,32,10,14,11,12,18,17,15,23,20,24,22,28] c: [32] | `- p:[7,30,27,25,21,19,16,13,9,8,10,14,11,12,18,17,15,23,20,24,22,28] c: [30] | +- p:[10,14,11,12,18,17,15] c: [18] | | | `- p:[10,14,11,12] c: [14] | | | `- p:[10] c: [10] | +- p:[20,23,24] c: [24] | | | `- p:[20,23] c: [23] | `- p:[22] c: [22] * Step 7: SizeAbstraction 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] 36. f2(A,B,C,H,I,J,K,L,X,Z) -> exitus616(A,B,C,H,I,J,K,L,X,Z) True (?,1) 37. f26(A,B,C,H,I,J,K,L,X,Z) -> exitus616(A,B,C,H,I,J,K,L,X,Z) True (?,1) Signature: {(exitus616,10) ;(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,36},1->{5},2->{},3->{1,2,3,4,36},4->{1,2,3,4,36},5->{6,7,37},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,37},30->{6,7,31,32,37},31->{33},32->{8},33->{34},34->{35},35->{16},36->{} ,37->{}] ,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] | +- p:[3,4] c: [4] | | | `- p:[3] c: [3] | `- p:[7,30,27,25,21,19,16,13,9,8,32,10,14,11,12,18,17,15,35,34,33,31,29,26,23,20,24,22,28] c: [35] | `- p:[7,30,27,25,21,19,16,13,9,8,32,10,14,11,12,18,17,15,23,20,24,22,28] c: [32] | `- p:[7,30,27,25,21,19,16,13,9,8,10,14,11,12,18,17,15,23,20,24,22,28] c: [30] | +- p:[10,14,11,12,18,17,15] c: [18] | | | `- p:[10,14,11,12] c: [14] | | | `- p:[10] c: [10] | +- p:[20,23,24] c: [24] | | | `- p:[20,23] c: [23] | `- p:[22] c: [22]) + Applied Processor: SizeAbstraction UseCFG Minimize + Details: () * Step 8: FlowAbstraction MAYBE + Considered Problem: Program: Domain: [A ,B ,C ,H ,I ,J ,K ,L ,X ,Z ,0.0 ,0.0.0 ,0.1 ,0.1.0 ,0.1.0.0 ,0.1.0.0.0 ,0.1.0.0.0.0 ,0.1.0.0.0.0.0 ,0.1.0.0.1 ,0.1.0.0.1.0 ,0.1.0.0.2] start ~> f2 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f2 ~> f15 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f2 ~> f1 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f2 ~> f2 [A <= A, B <= K + B, C <= unknown, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f2 ~> f2 [A <= A, B <= K + B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f15 ~> f26 [A <= A, B <= B, C <= C, H <= H, I <= K, J <= J, K <= K, L <= L, X <= X, Z <= Z] f26 ~> f1 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f26 ~> f30 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f30 ~> f42 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f42 ~> f68 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f42 ~> f42 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= A + L, X <= X, Z <= Z] f42 ~> f47 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f42 ~> f47 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f68 ~> f152 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f47 ~> f42 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= A + L, X <= X, Z <= Z] f47 ~> f51 [A <= A, B <= B, C <= C, H <= 0*K, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f152 ~> f164 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f51 ~> f58 [A <= A, B <= B, C <= C, H <= unknown, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f58 ~> f47 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K + K, L <= L, X <= X, Z <= Z] f164 ~> f176 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f164 ~> f167 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f176 ~> f184 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f176 ~> f176 [A <= A, B <= K + B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f167 ~> f164 [A <= A, B <= K, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f167 ~> f167 [A <= A, B <= B, C <= C, H <= unknown, I <= I, J <= J, K <= B + K, L <= L, X <= X, Z <= Z] f184 ~> f199 [A <= A, B <= B, C <= 0*K, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f199 ~> f218 [A <= A, B <= B, C <= 0*K, H <= H, I <= 0*K, J <= J, K <= K, L <= L, X <= 0*K, Z <= Z] f199 ~> f210 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= unknown, Z <= Z] f199 ~> f210 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= unknown, Z <= Z] f218 ~> f26 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= K + J, K <= K, L <= L, X <= X, Z <= Z] f210 ~> f26 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= K + J, K <= K, L <= L, X <= X, Z <= Z] f26 ~> f81 [A <= A, B <= B, C <= C, H <= H, I <= 0*K, J <= J, K <= K, L <= L, X <= X, Z <= Z] f26 ~> f30 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f81 ~> f87 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f87 ~> f100 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= K] f100 ~> f152 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f2 ~> exitus616 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f26 ~> 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 ~> f2 [A <= A, B <= K + B, C <= unknown, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f2 ~> f2 [A <= A, B <= K + B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] + Loop: [0.0.0 <= K + A + B] f2 ~> f2 [A <= A, B <= K + B, C <= unknown, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] + Loop: [0.1 <= 201*K + J] f26 ~> f30 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f210 ~> f26 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= K + J, K <= K, L <= L, X <= X, Z <= Z] f199 ~> f210 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= unknown, Z <= Z] f184 ~> f199 [A <= A, B <= B, C <= 0*K, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f176 ~> f184 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f164 ~> f176 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f152 ~> f164 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f68 ~> f152 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f42 ~> f68 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f30 ~> f42 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f26 ~> f30 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f42 ~> f42 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= A + L, X <= X, Z <= Z] f47 ~> f42 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= A + L, X <= X, Z <= Z] f42 ~> f47 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f42 ~> f47 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f58 ~> f47 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K + K, L <= L, X <= X, Z <= Z] f51 ~> f58 [A <= A, B <= B, C <= C, H <= unknown, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f47 ~> f51 [A <= A, B <= B, C <= C, H <= 0*K, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f100 ~> f152 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f87 ~> f100 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= K] f81 ~> f87 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f26 ~> f81 [A <= A, B <= B, C <= C, H <= H, I <= 0*K, J <= J, K <= K, L <= L, X <= X, Z <= Z] f218 ~> f26 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= K + J, K <= K, L <= L, X <= X, Z <= Z] f199 ~> f218 [A <= A, B <= B, C <= 0*K, H <= H, I <= 0*K, J <= J, K <= K, L <= L, X <= 0*K, Z <= Z] f167 ~> f164 [A <= A, B <= K, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f164 ~> f167 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f167 ~> f167 [A <= A, B <= B, C <= C, H <= unknown, I <= I, J <= J, K <= B + K, L <= L, X <= X, Z <= Z] f176 ~> f176 [A <= A, B <= K + B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f199 ~> f210 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= unknown, Z <= Z] + Loop: [0.1.0 <= K + 200*I + J] f26 ~> f30 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f210 ~> f26 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= K + J, K <= K, L <= L, X <= X, Z <= Z] f199 ~> f210 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= unknown, Z <= Z] f184 ~> f199 [A <= A, B <= B, C <= 0*K, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f176 ~> f184 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f164 ~> f176 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f152 ~> f164 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f68 ~> f152 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f42 ~> f68 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f30 ~> f42 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f26 ~> f30 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f42 ~> f42 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= A + L, X <= X, Z <= Z] f47 ~> f42 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= A + L, X <= X, Z <= Z] f42 ~> f47 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f42 ~> f47 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f58 ~> f47 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K + K, L <= L, X <= X, Z <= Z] f51 ~> f58 [A <= A, B <= B, C <= C, H <= unknown, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f47 ~> f51 [A <= A, B <= B, C <= C, H <= 0*K, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f167 ~> f164 [A <= A, B <= K, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f164 ~> f167 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f167 ~> f167 [A <= A, B <= B, C <= C, H <= unknown, I <= I, J <= J, K <= B + K, L <= L, X <= X, Z <= Z] f176 ~> f176 [A <= A, B <= K + B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f199 ~> f210 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= unknown, Z <= Z] + Loop: [0.1.0.0 <= 201*K + J] f26 ~> f30 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f210 ~> f26 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= K + J, K <= K, L <= L, X <= X, Z <= Z] f199 ~> f210 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= unknown, Z <= Z] f184 ~> f199 [A <= A, B <= B, C <= 0*K, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f176 ~> f184 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f164 ~> f176 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f152 ~> f164 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f68 ~> f152 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f42 ~> f68 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f30 ~> f42 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f42 ~> f42 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= A + L, X <= X, Z <= Z] f47 ~> f42 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= A + L, X <= X, Z <= Z] f42 ~> f47 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f42 ~> f47 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f58 ~> f47 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K + K, L <= L, X <= X, Z <= Z] f51 ~> f58 [A <= A, B <= B, C <= C, H <= unknown, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f47 ~> f51 [A <= A, B <= B, C <= C, H <= 0*K, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f167 ~> f164 [A <= A, B <= K, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f164 ~> f167 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f167 ~> f167 [A <= A, B <= B, C <= C, H <= unknown, I <= I, J <= J, K <= B + K, L <= L, X <= X, Z <= Z] f176 ~> f176 [A <= A, B <= K + B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f199 ~> f210 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= unknown, Z <= Z] + Loop: [0.1.0.0.0 <= B + K] f42 ~> f42 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= A + L, X <= X, Z <= Z] f47 ~> f42 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= A + L, X <= X, Z <= Z] f42 ~> f47 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f42 ~> f47 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f58 ~> f47 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K + K, L <= L, X <= X, Z <= Z] f51 ~> f58 [A <= A, B <= B, C <= C, H <= unknown, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f47 ~> f51 [A <= A, B <= B, C <= C, H <= 0*K, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] + Loop: [0.1.0.0.0.0 <= A + L] f42 ~> f42 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= A + L, X <= X, Z <= Z] f47 ~> f42 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= A + L, X <= X, Z <= Z] f42 ~> f47 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f42 ~> f47 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] + Loop: [0.1.0.0.0.0.0 <= A + L] f42 ~> f42 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= A + L, X <= X, Z <= Z] + Loop: [0.1.0.0.1 <= K + B + K] f164 ~> f167 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f167 ~> f164 [A <= A, B <= K, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f167 ~> f167 [A <= A, B <= B, C <= C, H <= unknown, I <= I, J <= J, K <= B + K, L <= L, X <= X, Z <= Z] + Loop: [0.1.0.0.1.0 <= B] f164 ~> f167 [A <= A, B <= B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] f167 ~> f164 [A <= A, B <= K, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] + Loop: [0.1.0.0.2 <= K + A + B] f176 ~> f176 [A <= A, B <= K + B, C <= C, H <= H, I <= I, J <= J, K <= K, L <= L, X <= X, Z <= Z] + Applied Processor: FlowAbstraction + Details: () * Step 9: LareProcessor MAYBE + Considered Problem: Program: Domain: [tick ,huge ,K ,A ,B ,C ,H ,I ,J ,K ,L ,X ,Z ,0.0 ,0.0.0 ,0.1 ,0.1.0 ,0.1.0.0 ,0.1.0.0.0 ,0.1.0.0.0.0 ,0.1.0.0.0.0.0 ,0.1.0.0.1 ,0.1.0.0.1.0 ,0.1.0.0.2] start ~> f2 [] f2 ~> f15 [] f2 ~> f1 [] f2 ~> f2 [huge ~=> C,B ~+> B,K ~+> B] f2 ~> f2 [B ~+> B,K ~+> B] f15 ~> f26 [K ~=> I] f26 ~> f1 [] f26 ~> f30 [] f30 ~> f42 [] f42 ~> f68 [] f42 ~> f42 [A ~+> L,L ~+> L] f42 ~> f47 [] f42 ~> f47 [] f68 ~> f152 [] f47 ~> f42 [A ~+> L,L ~+> L] f47 ~> f51 [K ~=> H] f152 ~> f164 [] f51 ~> f58 [huge ~=> H] f58 ~> f47 [K ~+> K,K ~+> K] f164 ~> f176 [] f164 ~> f167 [] f176 ~> f184 [] f176 ~> f176 [B ~+> B,K ~+> B] f167 ~> f164 [K ~=> B] f167 ~> f167 [huge ~=> H,B ~+> K,K ~+> K] f184 ~> f199 [K ~=> C] f199 ~> f218 [K ~=> C,K ~=> I,K ~=> X] f199 ~> f210 [huge ~=> X] f199 ~> f210 [huge ~=> X] f218 ~> f26 [J ~+> J,K ~+> J] f210 ~> f26 [J ~+> J,K ~+> J] f26 ~> f81 [K ~=> I] f26 ~> f30 [] f81 ~> f87 [] f87 ~> f100 [K ~=> Z] f100 ~> f152 [] f2 ~> exitus616 [] f26 ~> exitus616 [] + Loop: [A ~+> 0.0,B ~+> 0.0,K ~+> 0.0] f2 ~> f2 [huge ~=> C,B ~+> B,K ~+> B] f2 ~> f2 [B ~+> B,K ~+> B] + Loop: [A ~+> 0.0.0,B ~+> 0.0.0,K ~+> 0.0.0] f2 ~> f2 [huge ~=> C,B ~+> B,K ~+> B] + Loop: [J ~+> 0.1,K ~*> 0.1] f26 ~> f30 [] f210 ~> f26 [J ~+> J,K ~+> J] f199 ~> f210 [huge ~=> X] f184 ~> f199 [K ~=> C] f176 ~> f184 [] f164 ~> f176 [] f152 ~> f164 [] f68 ~> f152 [] f42 ~> f68 [] f30 ~> f42 [] f26 ~> f30 [] f42 ~> f42 [A ~+> L,L ~+> L] f47 ~> f42 [A ~+> L,L ~+> L] f42 ~> f47 [] f42 ~> f47 [] f58 ~> f47 [K ~+> K,K ~+> K] f51 ~> f58 [huge ~=> H] f47 ~> f51 [K ~=> H] f100 ~> f152 [] f87 ~> f100 [K ~=> Z] f81 ~> f87 [] f26 ~> f81 [K ~=> I] f218 ~> f26 [J ~+> J,K ~+> J] f199 ~> f218 [K ~=> C,K ~=> I,K ~=> X] f167 ~> f164 [K ~=> B] f164 ~> f167 [] f167 ~> f167 [huge ~=> H,B ~+> K,K ~+> K] f176 ~> f176 [B ~+> B,K ~+> B] f199 ~> f210 [huge ~=> X] + Loop: [J ~+> 0.1.0,K ~+> 0.1.0,I ~*> 0.1.0] f26 ~> f30 [] f210 ~> f26 [J ~+> J,K ~+> J] f199 ~> f210 [huge ~=> X] f184 ~> f199 [K ~=> C] f176 ~> f184 [] f164 ~> f176 [] f152 ~> f164 [] f68 ~> f152 [] f42 ~> f68 [] f30 ~> f42 [] f26 ~> f30 [] f42 ~> f42 [A ~+> L,L ~+> L] f47 ~> f42 [A ~+> L,L ~+> L] f42 ~> f47 [] f42 ~> f47 [] f58 ~> f47 [K ~+> K,K ~+> K] f51 ~> f58 [huge ~=> H] f47 ~> f51 [K ~=> H] f167 ~> f164 [K ~=> B] f164 ~> f167 [] f167 ~> f167 [huge ~=> H,B ~+> K,K ~+> K] f176 ~> f176 [B ~+> B,K ~+> B] f199 ~> f210 [huge ~=> X] + Loop: [J ~+> 0.1.0.0,K ~*> 0.1.0.0] f26 ~> f30 [] f210 ~> f26 [J ~+> J,K ~+> J] f199 ~> f210 [huge ~=> X] f184 ~> f199 [K ~=> C] f176 ~> f184 [] f164 ~> f176 [] f152 ~> f164 [] f68 ~> f152 [] f42 ~> f68 [] f30 ~> f42 [] f42 ~> f42 [A ~+> L,L ~+> L] f47 ~> f42 [A ~+> L,L ~+> L] f42 ~> f47 [] f42 ~> f47 [] f58 ~> f47 [K ~+> K,K ~+> K] f51 ~> f58 [huge ~=> H] f47 ~> f51 [K ~=> H] f167 ~> f164 [K ~=> B] f164 ~> f167 [] f167 ~> f167 [huge ~=> H,B ~+> K,K ~+> K] f176 ~> f176 [B ~+> B,K ~+> B] f199 ~> f210 [huge ~=> X] + Loop: [B ~+> 0.1.0.0.0,K ~+> 0.1.0.0.0] f42 ~> f42 [A ~+> L,L ~+> L] f47 ~> f42 [A ~+> L,L ~+> L] f42 ~> f47 [] f42 ~> f47 [] f58 ~> f47 [K ~+> K,K ~+> K] f51 ~> f58 [huge ~=> H] f47 ~> f51 [K ~=> H] + Loop: [A ~+> 0.1.0.0.0.0,L ~+> 0.1.0.0.0.0] f42 ~> f42 [A ~+> L,L ~+> L] f47 ~> f42 [A ~+> L,L ~+> L] f42 ~> f47 [] f42 ~> f47 [] + Loop: [A ~+> 0.1.0.0.0.0.0,L ~+> 0.1.0.0.0.0.0] f42 ~> f42 [A ~+> L,L ~+> L] + Loop: [B ~+> 0.1.0.0.1,K ~+> 0.1.0.0.1,K ~+> 0.1.0.0.1] f164 ~> f167 [] f167 ~> f164 [K ~=> B] f167 ~> f167 [huge ~=> H,B ~+> K,K ~+> K] + Loop: [B ~=> 0.1.0.0.1.0] f164 ~> f167 [] f167 ~> f164 [K ~=> B] + Loop: [A ~+> 0.1.0.0.2,B ~+> 0.1.0.0.2,K ~+> 0.1.0.0.2] f176 ~> f176 [B ~+> B,K ~+> B] + Applied Processor: LareProcessor + Details: start ~> exitus616 [B ~=> 0.1.0.0.1.0 ,K ~=> B ,K ~=> 0.1.0.0.1.0 ,K ~=> C ,K ~=> I ,K ~=> X ,K ~=> Z ,huge ~=> C ,huge ~=> H ,huge ~=> X ,A ~+> L ,A ~+> 0.0 ,A ~+> 0.0.0 ,A ~+> 0.1.0.0.0.0 ,A ~+> 0.1.0.0.0.0.0 ,A ~+> 0.1.0.0.2 ,A ~+> tick ,B ~+> B ,B ~+> K ,B ~+> 0.0 ,B ~+> 0.0.0 ,B ~+> 0.1.0.0.0 ,B ~+> 0.1.0.0.1 ,B ~+> 0.1.0.0.1.0 ,B ~+> 0.1.0.0.2 ,B ~+> tick ,J ~+> J ,J ~+> 0.1 ,J ~+> 0.1.0 ,J ~+> 0.1.0.0 ,J ~+> tick ,K ~+> B ,K ~+> K ,K ~+> 0.1.0.0.0 ,K ~+> 0.1.0.0.1 ,K ~+> 0.1.0.0.1.0 ,K ~+> 0.1.0.0.2 ,K ~+> tick ,L ~+> L ,L ~+> 0.1.0.0.0.0 ,L ~+> 0.1.0.0.0.0.0 ,L ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> J ,K ~+> K ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> 0.1.0 ,K ~+> 0.1.0.0 ,K ~+> 0.1.0.0.0 ,K ~+> 0.1.0.0.1 ,K ~+> 0.1.0.0.1.0 ,K ~+> 0.1.0.0.2 ,K ~+> tick ,A ~*> B ,A ~*> K ,A ~*> L ,A ~*> 0.1.0.0.0 ,A ~*> 0.1.0.0.0.0 ,A ~*> 0.1.0.0.0.0.0 ,A ~*> 0.1.0.0.1 ,A ~*> 0.1.0.0.1.0 ,A ~*> 0.1.0.0.2 ,A ~*> tick ,B ~*> B ,B ~*> K ,B ~*> L ,B ~*> 0.1.0.0.0 ,B ~*> 0.1.0.0.0.0 ,B ~*> 0.1.0.0.0.0.0 ,B ~*> 0.1.0.0.1 ,B ~*> 0.1.0.0.1.0 ,B ~*> 0.1.0.0.2 ,B ~*> tick ,J ~*> B ,J ~*> J ,J ~*> K ,J ~*> L ,J ~*> 0.1.0 ,J ~*> 0.1.0.0 ,J ~*> 0.1.0.0.0 ,J ~*> 0.1.0.0.0.0 ,J ~*> 0.1.0.0.0.0.0 ,J ~*> 0.1.0.0.1 ,J ~*> 0.1.0.0.1.0 ,J ~*> 0.1.0.0.2 ,J ~*> tick ,K ~*> B ,K ~*> K ,K ~*> L ,K ~*> 0.1.0.0.0 ,K ~*> 0.1.0.0.0.0 ,K ~*> 0.1.0.0.0.0.0 ,K ~*> 0.1.0.0.1 ,K ~*> 0.1.0.0.1.0 ,K ~*> 0.1.0.0.2 ,K ~*> tick ,L ~*> L ,L ~*> 0.1.0.0.0.0 ,L ~*> 0.1.0.0.0.0.0 ,L ~*> tick ,K ~*> B ,K ~*> J ,K ~*> K ,K ~*> L ,K ~*> 0.1 ,K ~*> 0.1.0 ,K ~*> 0.1.0.0 ,K ~*> 0.1.0.0.0 ,K ~*> 0.1.0.0.0.0 ,K ~*> 0.1.0.0.0.0.0 ,K ~*> 0.1.0.0.1 ,K ~*> 0.1.0.0.1.0 ,K ~*> 0.1.0.0.2 ,K ~*> tick ,A ~^> B ,A ~^> K ,A ~^> L ,A ~^> 0.1.0.0.0 ,A ~^> 0.1.0.0.0.0 ,A ~^> 0.1.0.0.0.0.0 ,A ~^> 0.1.0.0.1 ,A ~^> 0.1.0.0.1.0 ,A ~^> 0.1.0.0.2 ,A ~^> tick ,B ~^> B ,B ~^> K ,B ~^> L ,B ~^> 0.1.0.0.0 ,B ~^> 0.1.0.0.0.0 ,B ~^> 0.1.0.0.0.0.0 ,B ~^> 0.1.0.0.1 ,B ~^> 0.1.0.0.1.0 ,B ~^> 0.1.0.0.2 ,B ~^> tick ,J ~^> B ,J ~^> J ,J ~^> K ,J ~^> L ,J ~^> 0.1.0 ,J ~^> 0.1.0.0 ,J ~^> 0.1.0.0.0 ,J ~^> 0.1.0.0.0.0 ,J ~^> 0.1.0.0.0.0.0 ,J ~^> 0.1.0.0.1 ,J ~^> 0.1.0.0.1.0 ,J ~^> 0.1.0.0.2 ,J ~^> tick ,K ~^> B ,K ~^> K ,K ~^> L ,K ~^> 0.1.0.0.0 ,K ~^> 0.1.0.0.0.0 ,K ~^> 0.1.0.0.0.0.0 ,K ~^> 0.1.0.0.1 ,K ~^> 0.1.0.0.1.0 ,K ~^> 0.1.0.0.2 ,K ~^> tick ,L ~^> L ,L ~^> 0.1.0.0.0.0 ,L ~^> 0.1.0.0.0.0.0 ,L ~^> tick ,K ~^> B ,K ~^> J ,K ~^> K ,K ~^> L ,K ~^> 0.1.0 ,K ~^> 0.1.0.0 ,K ~^> 0.1.0.0.0 ,K ~^> 0.1.0.0.0.0 ,K ~^> 0.1.0.0.0.0.0 ,K ~^> 0.1.0.0.1 ,K ~^> 0.1.0.0.1.0 ,K ~^> 0.1.0.0.2 ,K ~^> tick] start ~> f1 [B ~=> 0.1.0.0.1.0 ,K ~=> B ,K ~=> 0.1.0.0.1.0 ,K ~=> C ,K ~=> I ,K ~=> X ,K ~=> Z ,huge ~=> C ,huge ~=> H ,huge ~=> X ,A ~+> L ,A ~+> 0.0 ,A ~+> 0.0.0 ,A ~+> 0.1.0.0.0.0 ,A ~+> 0.1.0.0.0.0.0 ,A ~+> 0.1.0.0.2 ,A ~+> tick ,B ~+> B ,B ~+> K ,B ~+> 0.0 ,B ~+> 0.0.0 ,B ~+> 0.1.0.0.0 ,B ~+> 0.1.0.0.1 ,B ~+> 0.1.0.0.1.0 ,B ~+> 0.1.0.0.2 ,B ~+> tick ,J ~+> J ,J ~+> 0.1 ,J ~+> 0.1.0 ,J ~+> 0.1.0.0 ,J ~+> tick ,K ~+> B ,K ~+> K ,K ~+> 0.1.0.0.0 ,K ~+> 0.1.0.0.1 ,K ~+> 0.1.0.0.1.0 ,K ~+> 0.1.0.0.2 ,K ~+> tick ,L ~+> L ,L ~+> 0.1.0.0.0.0 ,L ~+> 0.1.0.0.0.0.0 ,L ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> J ,K ~+> K ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> 0.1.0 ,K ~+> 0.1.0.0 ,K ~+> 0.1.0.0.0 ,K ~+> 0.1.0.0.1 ,K ~+> 0.1.0.0.1.0 ,K ~+> 0.1.0.0.2 ,K ~+> tick ,A ~*> B ,A ~*> K ,A ~*> L ,A ~*> 0.1.0.0.0 ,A ~*> 0.1.0.0.0.0 ,A ~*> 0.1.0.0.0.0.0 ,A ~*> 0.1.0.0.1 ,A ~*> 0.1.0.0.1.0 ,A ~*> 0.1.0.0.2 ,A ~*> tick ,B ~*> B ,B ~*> K ,B ~*> L ,B ~*> 0.1.0.0.0 ,B ~*> 0.1.0.0.0.0 ,B ~*> 0.1.0.0.0.0.0 ,B ~*> 0.1.0.0.1 ,B ~*> 0.1.0.0.1.0 ,B ~*> 0.1.0.0.2 ,B ~*> tick ,J ~*> B ,J ~*> J ,J ~*> K ,J ~*> L ,J ~*> 0.1.0 ,J ~*> 0.1.0.0 ,J ~*> 0.1.0.0.0 ,J ~*> 0.1.0.0.0.0 ,J ~*> 0.1.0.0.0.0.0 ,J ~*> 0.1.0.0.1 ,J ~*> 0.1.0.0.1.0 ,J ~*> 0.1.0.0.2 ,J ~*> tick ,K ~*> B ,K ~*> K ,K ~*> L ,K ~*> 0.1.0.0.0 ,K ~*> 0.1.0.0.0.0 ,K ~*> 0.1.0.0.0.0.0 ,K ~*> 0.1.0.0.1 ,K ~*> 0.1.0.0.1.0 ,K ~*> 0.1.0.0.2 ,K ~*> tick ,L ~*> L ,L ~*> 0.1.0.0.0.0 ,L ~*> 0.1.0.0.0.0.0 ,L ~*> tick ,K ~*> B ,K ~*> J ,K ~*> K ,K ~*> L ,K ~*> 0.1 ,K ~*> 0.1.0 ,K ~*> 0.1.0.0 ,K ~*> 0.1.0.0.0 ,K ~*> 0.1.0.0.0.0 ,K ~*> 0.1.0.0.0.0.0 ,K ~*> 0.1.0.0.1 ,K ~*> 0.1.0.0.1.0 ,K ~*> 0.1.0.0.2 ,K ~*> tick ,A ~^> B ,A ~^> K ,A ~^> L ,A ~^> 0.1.0.0.0 ,A ~^> 0.1.0.0.0.0 ,A ~^> 0.1.0.0.0.0.0 ,A ~^> 0.1.0.0.1 ,A ~^> 0.1.0.0.1.0 ,A ~^> 0.1.0.0.2 ,A ~^> tick ,B ~^> B ,B ~^> K ,B ~^> L ,B ~^> 0.1.0.0.0 ,B ~^> 0.1.0.0.0.0 ,B ~^> 0.1.0.0.0.0.0 ,B ~^> 0.1.0.0.1 ,B ~^> 0.1.0.0.1.0 ,B ~^> 0.1.0.0.2 ,B ~^> tick ,J ~^> B ,J ~^> J ,J ~^> K ,J ~^> L ,J ~^> 0.1.0 ,J ~^> 0.1.0.0 ,J ~^> 0.1.0.0.0 ,J ~^> 0.1.0.0.0.0 ,J ~^> 0.1.0.0.0.0.0 ,J ~^> 0.1.0.0.1 ,J ~^> 0.1.0.0.1.0 ,J ~^> 0.1.0.0.2 ,J ~^> tick ,K ~^> B ,K ~^> K ,K ~^> L ,K ~^> 0.1.0.0.0 ,K ~^> 0.1.0.0.0.0 ,K ~^> 0.1.0.0.0.0.0 ,K ~^> 0.1.0.0.1 ,K ~^> 0.1.0.0.1.0 ,K ~^> 0.1.0.0.2 ,K ~^> tick ,L ~^> L ,L ~^> 0.1.0.0.0.0 ,L ~^> 0.1.0.0.0.0.0 ,L ~^> tick ,K ~^> B ,K ~^> J ,K ~^> K ,K ~^> L ,K ~^> 0.1.0 ,K ~^> 0.1.0.0 ,K ~^> 0.1.0.0.0 ,K ~^> 0.1.0.0.0.0 ,K ~^> 0.1.0.0.0.0.0 ,K ~^> 0.1.0.0.1 ,K ~^> 0.1.0.0.1.0 ,K ~^> 0.1.0.0.2 ,K ~^> tick] + f2> [huge ~=> C ,A ~+> 0.0 ,A ~+> 0.0.0 ,A ~+> tick ,B ~+> B ,B ~+> 0.0 ,B ~+> 0.0.0 ,B ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> tick ,A ~*> B ,A ~*> tick ,B ~*> B ,B ~*> tick ,K ~*> B ,K ~*> tick ,A ~^> B ,B ~^> B ,K ~^> B] + f2> [huge ~=> C ,A ~+> 0.0.0 ,A ~+> tick ,B ~+> B ,B ~+> 0.0.0 ,B ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> 0.0.0 ,K ~+> tick ,A ~*> B ,B ~*> B ,K ~*> B] + f26> [B ~=> 0.1.0.0.1.0 ,K ~=> B ,K ~=> 0.1.0.0.1.0 ,K ~=> C ,K ~=> I ,K ~=> X ,K ~=> Z ,huge ~=> H ,huge ~=> X ,A ~+> L ,A ~+> 0.1.0.0.0.0 ,A ~+> 0.1.0.0.0.0.0 ,A ~+> 0.1.0.0.2 ,A ~+> tick ,B ~+> B ,B ~+> K ,B ~+> 0.1.0.0.0 ,B ~+> 0.1.0.0.1 ,B ~+> 0.1.0.0.1.0 ,B ~+> 0.1.0.0.2 ,B ~+> tick ,J ~+> J ,J ~+> 0.1 ,J ~+> 0.1.0 ,J ~+> 0.1.0.0 ,J ~+> tick ,K ~+> B ,K ~+> K ,K ~+> 0.1.0.0.0 ,K ~+> 0.1.0.0.1 ,K ~+> 0.1.0.0.1.0 ,K ~+> 0.1.0.0.2 ,K ~+> tick ,L ~+> L ,L ~+> 0.1.0.0.0.0 ,L ~+> 0.1.0.0.0.0.0 ,L ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> J ,K ~+> K ,K ~+> 0.1.0 ,K ~+> 0.1.0.0 ,K ~+> 0.1.0.0.0 ,K ~+> 0.1.0.0.1 ,K ~+> 0.1.0.0.1.0 ,K ~+> 0.1.0.0.2 ,K ~+> tick ,A ~*> B ,A ~*> K ,A ~*> L ,A ~*> 0.1.0.0.0 ,A ~*> 0.1.0.0.0.0 ,A ~*> 0.1.0.0.0.0.0 ,A ~*> 0.1.0.0.1 ,A ~*> 0.1.0.0.1.0 ,A ~*> 0.1.0.0.2 ,A ~*> tick ,B ~*> B ,B ~*> K ,B ~*> L ,B ~*> 0.1.0.0.0 ,B ~*> 0.1.0.0.0.0 ,B ~*> 0.1.0.0.0.0.0 ,B ~*> 0.1.0.0.1 ,B ~*> 0.1.0.0.1.0 ,B ~*> 0.1.0.0.2 ,B ~*> tick ,I ~*> B ,I ~*> J ,I ~*> K ,I ~*> L ,I ~*> 0.1.0 ,I ~*> 0.1.0.0 ,I ~*> 0.1.0.0.0 ,I ~*> 0.1.0.0.0.0 ,I ~*> 0.1.0.0.0.0.0 ,I ~*> 0.1.0.0.1 ,I ~*> 0.1.0.0.1.0 ,I ~*> 0.1.0.0.2 ,I ~*> tick ,J ~*> B ,J ~*> J ,J ~*> K ,J ~*> L ,J ~*> 0.1.0 ,J ~*> 0.1.0.0 ,J ~*> 0.1.0.0.0 ,J ~*> 0.1.0.0.0.0 ,J ~*> 0.1.0.0.0.0.0 ,J ~*> 0.1.0.0.1 ,J ~*> 0.1.0.0.1.0 ,J ~*> 0.1.0.0.2 ,J ~*> tick ,K ~*> B ,K ~*> K ,K ~*> L ,K ~*> 0.1.0.0.0 ,K ~*> 0.1.0.0.0.0 ,K ~*> 0.1.0.0.0.0.0 ,K ~*> 0.1.0.0.1 ,K ~*> 0.1.0.0.1.0 ,K ~*> 0.1.0.0.2 ,K ~*> tick ,L ~*> L ,L ~*> 0.1.0.0.0.0 ,L ~*> 0.1.0.0.0.0.0 ,L ~*> tick ,K ~*> B ,K ~*> J ,K ~*> K ,K ~*> L ,K ~*> 0.1 ,K ~*> 0.1.0 ,K ~*> 0.1.0.0 ,K ~*> 0.1.0.0.0 ,K ~*> 0.1.0.0.0.0 ,K ~*> 0.1.0.0.0.0.0 ,K ~*> 0.1.0.0.1 ,K ~*> 0.1.0.0.1.0 ,K ~*> 0.1.0.0.2 ,K ~*> tick ,A ~^> B ,A ~^> K ,A ~^> L ,A ~^> 0.1.0.0.0 ,A ~^> 0.1.0.0.0.0 ,A ~^> 0.1.0.0.0.0.0 ,A ~^> 0.1.0.0.1 ,A ~^> 0.1.0.0.1.0 ,A ~^> 0.1.0.0.2 ,A ~^> tick ,B ~^> B ,B ~^> K ,B ~^> L ,B ~^> 0.1.0.0.0 ,B ~^> 0.1.0.0.0.0 ,B ~^> 0.1.0.0.0.0.0 ,B ~^> 0.1.0.0.1 ,B ~^> 0.1.0.0.1.0 ,B ~^> 0.1.0.0.2 ,B ~^> tick ,I ~^> B ,I ~^> J ,I ~^> K ,I ~^> L ,I ~^> 0.1.0 ,I ~^> 0.1.0.0 ,I ~^> 0.1.0.0.0 ,I ~^> 0.1.0.0.0.0 ,I ~^> 0.1.0.0.0.0.0 ,I ~^> 0.1.0.0.1 ,I ~^> 0.1.0.0.1.0 ,I ~^> 0.1.0.0.2 ,I ~^> tick ,J ~^> B ,J ~^> J ,J ~^> K ,J ~^> L ,J ~^> 0.1.0 ,J ~^> 0.1.0.0 ,J ~^> 0.1.0.0.0 ,J ~^> 0.1.0.0.0.0 ,J ~^> 0.1.0.0.0.0.0 ,J ~^> 0.1.0.0.1 ,J ~^> 0.1.0.0.1.0 ,J ~^> 0.1.0.0.2 ,J ~^> tick ,K ~^> B ,K ~^> K ,K ~^> L ,K ~^> 0.1.0.0.0 ,K ~^> 0.1.0.0.0.0 ,K ~^> 0.1.0.0.0.0.0 ,K ~^> 0.1.0.0.1 ,K ~^> 0.1.0.0.1.0 ,K ~^> 0.1.0.0.2 ,K ~^> tick ,L ~^> L ,L ~^> 0.1.0.0.0.0 ,L ~^> 0.1.0.0.0.0.0 ,L ~^> tick ,K ~^> B ,K ~^> J ,K ~^> K ,K ~^> L ,K ~^> 0.1.0 ,K ~^> 0.1.0.0 ,K ~^> 0.1.0.0.0 ,K ~^> 0.1.0.0.0.0 ,K ~^> 0.1.0.0.0.0.0 ,K ~^> 0.1.0.0.1 ,K ~^> 0.1.0.0.1.0 ,K ~^> 0.1.0.0.2 ,K ~^> tick] + f26> [B ~=> 0.1.0.0.1.0 ,K ~=> B ,K ~=> 0.1.0.0.1.0 ,K ~=> C ,huge ~=> H ,huge ~=> X ,A ~+> L ,A ~+> 0.1.0.0.0.0 ,A ~+> 0.1.0.0.0.0.0 ,A ~+> 0.1.0.0.2 ,A ~+> tick ,B ~+> B ,B ~+> K ,B ~+> 0.1.0.0.0 ,B ~+> 0.1.0.0.1 ,B ~+> 0.1.0.0.1.0 ,B ~+> 0.1.0.0.2 ,B ~+> tick ,J ~+> J ,J ~+> 0.1.0 ,J ~+> 0.1.0.0 ,J ~+> tick ,K ~+> B ,K ~+> K ,K ~+> 0.1.0.0.0 ,K ~+> 0.1.0.0.1 ,K ~+> 0.1.0.0.1.0 ,K ~+> 0.1.0.0.2 ,K ~+> tick ,L ~+> L ,L ~+> 0.1.0.0.0.0 ,L ~+> 0.1.0.0.0.0.0 ,L ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> J ,K ~+> K ,K ~+> 0.1.0 ,K ~+> 0.1.0.0 ,K ~+> 0.1.0.0.0 ,K ~+> 0.1.0.0.1 ,K ~+> 0.1.0.0.1.0 ,K ~+> 0.1.0.0.2 ,K ~+> tick ,A ~*> B ,A ~*> K ,A ~*> L ,A ~*> 0.1.0.0.0 ,A ~*> 0.1.0.0.0.0 ,A ~*> 0.1.0.0.0.0.0 ,A ~*> 0.1.0.0.1 ,A ~*> 0.1.0.0.1.0 ,A ~*> 0.1.0.0.2 ,A ~*> tick ,B ~*> B ,B ~*> K ,B ~*> L ,B ~*> 0.1.0.0.0 ,B ~*> 0.1.0.0.0.0 ,B ~*> 0.1.0.0.0.0.0 ,B ~*> 0.1.0.0.1 ,B ~*> 0.1.0.0.1.0 ,B ~*> 0.1.0.0.2 ,B ~*> tick ,I ~*> B ,I ~*> J ,I ~*> K ,I ~*> L ,I ~*> 0.1.0 ,I ~*> 0.1.0.0 ,I ~*> 0.1.0.0.0 ,I ~*> 0.1.0.0.0.0 ,I ~*> 0.1.0.0.0.0.0 ,I ~*> 0.1.0.0.1 ,I ~*> 0.1.0.0.1.0 ,I ~*> 0.1.0.0.2 ,I ~*> tick ,J ~*> B ,J ~*> J ,J ~*> K ,J ~*> L ,J ~*> 0.1.0.0 ,J ~*> 0.1.0.0.0 ,J ~*> 0.1.0.0.0.0 ,J ~*> 0.1.0.0.0.0.0 ,J ~*> 0.1.0.0.1 ,J ~*> 0.1.0.0.1.0 ,J ~*> 0.1.0.0.2 ,J ~*> tick ,K ~*> B ,K ~*> K ,K ~*> L ,K ~*> 0.1.0.0.0 ,K ~*> 0.1.0.0.0.0 ,K ~*> 0.1.0.0.0.0.0 ,K ~*> 0.1.0.0.1 ,K ~*> 0.1.0.0.1.0 ,K ~*> 0.1.0.0.2 ,K ~*> tick ,L ~*> L ,L ~*> 0.1.0.0.0.0 ,L ~*> 0.1.0.0.0.0.0 ,L ~*> tick ,K ~*> B ,K ~*> J ,K ~*> K ,K ~*> L ,K ~*> 0.1.0.0 ,K ~*> 0.1.0.0.0 ,K ~*> 0.1.0.0.0.0 ,K ~*> 0.1.0.0.0.0.0 ,K ~*> 0.1.0.0.1 ,K ~*> 0.1.0.0.1.0 ,K ~*> 0.1.0.0.2 ,K ~*> tick ,A ~^> B ,A ~^> K ,A ~^> L ,A ~^> 0.1.0.0.0 ,A ~^> 0.1.0.0.0.0 ,A ~^> 0.1.0.0.0.0.0 ,A ~^> 0.1.0.0.1 ,A ~^> 0.1.0.0.1.0 ,A ~^> 0.1.0.0.2 ,A ~^> tick ,B ~^> B ,B ~^> K ,B ~^> L ,B ~^> 0.1.0.0.0 ,B ~^> 0.1.0.0.0.0 ,B ~^> 0.1.0.0.0.0.0 ,B ~^> 0.1.0.0.1 ,B ~^> 0.1.0.0.1.0 ,B ~^> 0.1.0.0.2 ,B ~^> tick ,I ~^> B ,I ~^> J ,I ~^> K ,I ~^> L ,I ~^> 0.1.0.0 ,I ~^> 0.1.0.0.0 ,I ~^> 0.1.0.0.0.0 ,I ~^> 0.1.0.0.0.0.0 ,I ~^> 0.1.0.0.1 ,I ~^> 0.1.0.0.1.0 ,I ~^> 0.1.0.0.2 ,I ~^> tick ,J ~^> B ,J ~^> J ,J ~^> K ,J ~^> L ,J ~^> 0.1.0.0 ,J ~^> 0.1.0.0.0 ,J ~^> 0.1.0.0.0.0 ,J ~^> 0.1.0.0.0.0.0 ,J ~^> 0.1.0.0.1 ,J ~^> 0.1.0.0.1.0 ,J ~^> 0.1.0.0.2 ,J ~^> tick ,K ~^> B ,K ~^> K ,K ~^> L ,K ~^> 0.1.0.0.0 ,K ~^> 0.1.0.0.0.0 ,K ~^> 0.1.0.0.0.0.0 ,K ~^> 0.1.0.0.1 ,K ~^> 0.1.0.0.1.0 ,K ~^> 0.1.0.0.2 ,K ~^> tick ,L ~^> L ,L ~^> 0.1.0.0.0.0 ,L ~^> 0.1.0.0.0.0.0 ,L ~^> tick ,K ~^> B ,K ~^> J ,K ~^> K ,K ~^> L ,K ~^> 0.1.0.0 ,K ~^> 0.1.0.0.0 ,K ~^> 0.1.0.0.0.0 ,K ~^> 0.1.0.0.0.0.0 ,K ~^> 0.1.0.0.1 ,K ~^> 0.1.0.0.1.0 ,K ~^> 0.1.0.0.2 ,K ~^> tick] f199> [B ~=> 0.1.0.0.1.0 ,K ~=> B ,K ~=> 0.1.0.0.1.0 ,K ~=> C ,huge ~=> H ,huge ~=> X ,A ~+> L ,A ~+> 0.1.0.0.0.0 ,A ~+> 0.1.0.0.0.0.0 ,A ~+> 0.1.0.0.2 ,A ~+> tick ,B ~+> B ,B ~+> K ,B ~+> 0.1.0.0.0 ,B ~+> 0.1.0.0.1 ,B ~+> 0.1.0.0.1.0 ,B ~+> 0.1.0.0.2 ,B ~+> tick ,J ~+> J ,J ~+> 0.1.0 ,J ~+> 0.1.0.0 ,J ~+> tick ,K ~+> B ,K ~+> K ,K ~+> 0.1.0.0.0 ,K ~+> 0.1.0.0.1 ,K ~+> 0.1.0.0.1.0 ,K ~+> 0.1.0.0.2 ,K ~+> tick ,L ~+> L ,L ~+> 0.1.0.0.0.0 ,L ~+> 0.1.0.0.0.0.0 ,L ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> J ,K ~+> K ,K ~+> 0.1.0 ,K ~+> 0.1.0.0 ,K ~+> 0.1.0.0.0 ,K ~+> 0.1.0.0.1 ,K ~+> 0.1.0.0.1.0 ,K ~+> 0.1.0.0.2 ,K ~+> tick ,A ~*> B ,A ~*> K ,A ~*> L ,A ~*> 0.1.0.0.0 ,A ~*> 0.1.0.0.0.0 ,A ~*> 0.1.0.0.0.0.0 ,A ~*> 0.1.0.0.1 ,A ~*> 0.1.0.0.1.0 ,A ~*> 0.1.0.0.2 ,A ~*> tick ,B ~*> B ,B ~*> K ,B ~*> L ,B ~*> 0.1.0.0.0 ,B ~*> 0.1.0.0.0.0 ,B ~*> 0.1.0.0.0.0.0 ,B ~*> 0.1.0.0.1 ,B ~*> 0.1.0.0.1.0 ,B ~*> 0.1.0.0.2 ,B ~*> tick ,I ~*> B ,I ~*> J ,I ~*> K ,I ~*> L ,I ~*> 0.1.0 ,I ~*> 0.1.0.0 ,I ~*> 0.1.0.0.0 ,I ~*> 0.1.0.0.0.0 ,I ~*> 0.1.0.0.0.0.0 ,I ~*> 0.1.0.0.1 ,I ~*> 0.1.0.0.1.0 ,I ~*> 0.1.0.0.2 ,I ~*> tick ,J ~*> B ,J ~*> J ,J ~*> K ,J ~*> L ,J ~*> 0.1.0.0 ,J ~*> 0.1.0.0.0 ,J ~*> 0.1.0.0.0.0 ,J ~*> 0.1.0.0.0.0.0 ,J ~*> 0.1.0.0.1 ,J ~*> 0.1.0.0.1.0 ,J ~*> 0.1.0.0.2 ,J ~*> tick ,K ~*> B ,K ~*> K ,K ~*> L ,K ~*> 0.1.0.0.0 ,K ~*> 0.1.0.0.0.0 ,K ~*> 0.1.0.0.0.0.0 ,K ~*> 0.1.0.0.1 ,K ~*> 0.1.0.0.1.0 ,K ~*> 0.1.0.0.2 ,K ~*> tick ,L ~*> L ,L ~*> 0.1.0.0.0.0 ,L ~*> 0.1.0.0.0.0.0 ,L ~*> tick ,K ~*> B ,K ~*> J ,K ~*> K ,K ~*> L ,K ~*> 0.1.0.0 ,K ~*> 0.1.0.0.0 ,K ~*> 0.1.0.0.0.0 ,K ~*> 0.1.0.0.0.0.0 ,K ~*> 0.1.0.0.1 ,K ~*> 0.1.0.0.1.0 ,K ~*> 0.1.0.0.2 ,K ~*> tick ,A ~^> B ,A ~^> K ,A ~^> L ,A ~^> 0.1.0.0.0 ,A ~^> 0.1.0.0.0.0 ,A ~^> 0.1.0.0.0.0.0 ,A ~^> 0.1.0.0.1 ,A ~^> 0.1.0.0.1.0 ,A ~^> 0.1.0.0.2 ,A ~^> tick ,B ~^> B ,B ~^> K ,B ~^> L ,B ~^> 0.1.0.0.0 ,B ~^> 0.1.0.0.0.0 ,B ~^> 0.1.0.0.0.0.0 ,B ~^> 0.1.0.0.1 ,B ~^> 0.1.0.0.1.0 ,B ~^> 0.1.0.0.2 ,B ~^> tick ,I ~^> B ,I ~^> J ,I ~^> K ,I ~^> L ,I ~^> 0.1.0.0 ,I ~^> 0.1.0.0.0 ,I ~^> 0.1.0.0.0.0 ,I ~^> 0.1.0.0.0.0.0 ,I ~^> 0.1.0.0.1 ,I ~^> 0.1.0.0.1.0 ,I ~^> 0.1.0.0.2 ,I ~^> tick ,J ~^> B ,J ~^> J ,J ~^> K ,J ~^> L ,J ~^> 0.1.0.0 ,J ~^> 0.1.0.0.0 ,J ~^> 0.1.0.0.0.0 ,J ~^> 0.1.0.0.0.0.0 ,J ~^> 0.1.0.0.1 ,J ~^> 0.1.0.0.1.0 ,J ~^> 0.1.0.0.2 ,J ~^> tick ,K ~^> B ,K ~^> K ,K ~^> L ,K ~^> 0.1.0.0.0 ,K ~^> 0.1.0.0.0.0 ,K ~^> 0.1.0.0.0.0.0 ,K ~^> 0.1.0.0.1 ,K ~^> 0.1.0.0.1.0 ,K ~^> 0.1.0.0.2 ,K ~^> tick ,L ~^> L ,L ~^> 0.1.0.0.0.0 ,L ~^> 0.1.0.0.0.0.0 ,L ~^> tick ,K ~^> B ,K ~^> J ,K ~^> K ,K ~^> L ,K ~^> 0.1.0.0 ,K ~^> 0.1.0.0.0 ,K ~^> 0.1.0.0.0.0 ,K ~^> 0.1.0.0.0.0.0 ,K ~^> 0.1.0.0.1 ,K ~^> 0.1.0.0.1.0 ,K ~^> 0.1.0.0.2 ,K ~^> tick] f26> [B ~=> 0.1.0.0.1.0 ,K ~=> B ,K ~=> 0.1.0.0.1.0 ,K ~=> C ,huge ~=> H ,huge ~=> X ,A ~+> L ,A ~+> 0.1.0.0.0.0 ,A ~+> 0.1.0.0.0.0.0 ,A ~+> 0.1.0.0.2 ,A ~+> tick ,B ~+> B ,B ~+> K ,B ~+> 0.1.0.0.0 ,B ~+> 0.1.0.0.1 ,B ~+> 0.1.0.0.1.0 ,B ~+> 0.1.0.0.2 ,B ~+> tick ,J ~+> J ,J ~+> 0.1.0 ,J ~+> 0.1.0.0 ,J ~+> tick ,K ~+> B ,K ~+> K ,K ~+> 0.1.0.0.0 ,K ~+> 0.1.0.0.1 ,K ~+> 0.1.0.0.1.0 ,K ~+> 0.1.0.0.2 ,K ~+> tick ,L ~+> L ,L ~+> 0.1.0.0.0.0 ,L ~+> 0.1.0.0.0.0.0 ,L ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> J ,K ~+> K ,K ~+> 0.1.0 ,K ~+> 0.1.0.0 ,K ~+> 0.1.0.0.0 ,K ~+> 0.1.0.0.1 ,K ~+> 0.1.0.0.1.0 ,K ~+> 0.1.0.0.2 ,K ~+> tick ,A ~*> B ,A ~*> K ,A ~*> L ,A ~*> 0.1.0.0.0 ,A ~*> 0.1.0.0.0.0 ,A ~*> 0.1.0.0.0.0.0 ,A ~*> 0.1.0.0.1 ,A ~*> 0.1.0.0.1.0 ,A ~*> 0.1.0.0.2 ,A ~*> tick ,B ~*> B ,B ~*> K ,B ~*> L ,B ~*> 0.1.0.0.0 ,B ~*> 0.1.0.0.0.0 ,B ~*> 0.1.0.0.0.0.0 ,B ~*> 0.1.0.0.1 ,B ~*> 0.1.0.0.1.0 ,B ~*> 0.1.0.0.2 ,B ~*> tick ,I ~*> B ,I ~*> J ,I ~*> K ,I ~*> L ,I ~*> 0.1.0 ,I ~*> tick ,J ~*> B ,J ~*> J ,J ~*> K ,J ~*> L ,J ~*> 0.1.0.0 ,J ~*> 0.1.0.0.0 ,J ~*> 0.1.0.0.0.0 ,J ~*> 0.1.0.0.0.0.0 ,J ~*> 0.1.0.0.1 ,J ~*> 0.1.0.0.1.0 ,J ~*> 0.1.0.0.2 ,J ~*> tick ,K ~*> B ,K ~*> K ,K ~*> L ,K ~*> 0.1.0.0.0 ,K ~*> 0.1.0.0.0.0 ,K ~*> 0.1.0.0.0.0.0 ,K ~*> 0.1.0.0.1 ,K ~*> 0.1.0.0.1.0 ,K ~*> 0.1.0.0.2 ,K ~*> tick ,L ~*> L ,L ~*> 0.1.0.0.0.0 ,L ~*> 0.1.0.0.0.0.0 ,L ~*> tick ,K ~*> B ,K ~*> J ,K ~*> K ,K ~*> L ,K ~*> 0.1.0.0 ,K ~*> 0.1.0.0.0 ,K ~*> 0.1.0.0.0.0 ,K ~*> 0.1.0.0.0.0.0 ,K ~*> 0.1.0.0.1 ,K ~*> 0.1.0.0.1.0 ,K ~*> 0.1.0.0.2 ,K ~*> tick ,A ~^> B ,A ~^> K ,A ~^> L ,A ~^> 0.1.0.0.0 ,A ~^> 0.1.0.0.0.0 ,A ~^> 0.1.0.0.0.0.0 ,A ~^> 0.1.0.0.1 ,A ~^> 0.1.0.0.1.0 ,A ~^> 0.1.0.0.2 ,A ~^> tick ,B ~^> B ,B ~^> K ,B ~^> L ,B ~^> 0.1.0.0.0 ,B ~^> 0.1.0.0.0.0 ,B ~^> 0.1.0.0.0.0.0 ,B ~^> 0.1.0.0.1 ,B ~^> 0.1.0.0.1.0 ,B ~^> 0.1.0.0.2 ,B ~^> tick ,I ~^> B ,I ~^> J ,I ~^> K ,I ~^> L ,J ~^> B ,J ~^> J ,J ~^> K ,J ~^> L ,J ~^> 0.1.0.0.0 ,J ~^> 0.1.0.0.0.0 ,J ~^> 0.1.0.0.0.0.0 ,J ~^> 0.1.0.0.1 ,J ~^> 0.1.0.0.1.0 ,J ~^> 0.1.0.0.2 ,J ~^> tick ,K ~^> B ,K ~^> K ,K ~^> L ,K ~^> 0.1.0.0.0 ,K ~^> 0.1.0.0.0.0 ,K ~^> 0.1.0.0.0.0.0 ,K ~^> 0.1.0.0.1 ,K ~^> 0.1.0.0.1.0 ,K ~^> 0.1.0.0.2 ,K ~^> tick ,L ~^> L ,L ~^> 0.1.0.0.0.0 ,L ~^> 0.1.0.0.0.0.0 ,L ~^> tick ,K ~^> B ,K ~^> J ,K ~^> K ,K ~^> L ,K ~^> 0.1.0.0.0 ,K ~^> 0.1.0.0.0.0 ,K ~^> 0.1.0.0.0.0.0 ,K ~^> 0.1.0.0.1 ,K ~^> 0.1.0.0.1.0 ,K ~^> 0.1.0.0.2 ,K ~^> tick] f199> [B ~=> 0.1.0.0.1.0 ,K ~=> B ,K ~=> 0.1.0.0.1.0 ,K ~=> C ,huge ~=> H ,huge ~=> X ,A ~+> L ,A ~+> 0.1.0.0.0.0 ,A ~+> 0.1.0.0.0.0.0 ,A ~+> 0.1.0.0.2 ,A ~+> tick ,B ~+> B ,B ~+> K ,B ~+> 0.1.0.0.0 ,B ~+> 0.1.0.0.1 ,B ~+> 0.1.0.0.1.0 ,B ~+> 0.1.0.0.2 ,B ~+> tick ,J ~+> J ,J ~+> 0.1.0 ,J ~+> 0.1.0.0 ,J ~+> tick ,K ~+> B ,K ~+> K ,K ~+> 0.1.0.0.0 ,K ~+> 0.1.0.0.1 ,K ~+> 0.1.0.0.1.0 ,K ~+> 0.1.0.0.2 ,K ~+> tick ,L ~+> L ,L ~+> 0.1.0.0.0.0 ,L ~+> 0.1.0.0.0.0.0 ,L ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> J ,K ~+> K ,K ~+> 0.1.0 ,K ~+> 0.1.0.0 ,K ~+> 0.1.0.0.0 ,K ~+> 0.1.0.0.1 ,K ~+> 0.1.0.0.1.0 ,K ~+> 0.1.0.0.2 ,K ~+> tick ,A ~*> B ,A ~*> K ,A ~*> L ,A ~*> 0.1.0.0.0 ,A ~*> 0.1.0.0.0.0 ,A ~*> 0.1.0.0.0.0.0 ,A ~*> 0.1.0.0.1 ,A ~*> 0.1.0.0.1.0 ,A ~*> 0.1.0.0.2 ,A ~*> tick ,B ~*> B ,B ~*> K ,B ~*> L ,B ~*> 0.1.0.0.0 ,B ~*> 0.1.0.0.0.0 ,B ~*> 0.1.0.0.0.0.0 ,B ~*> 0.1.0.0.1 ,B ~*> 0.1.0.0.1.0 ,B ~*> 0.1.0.0.2 ,B ~*> tick ,I ~*> B ,I ~*> J ,I ~*> K ,I ~*> L ,I ~*> 0.1.0 ,I ~*> 0.1.0.0 ,I ~*> 0.1.0.0.0 ,I ~*> 0.1.0.0.0.0 ,I ~*> 0.1.0.0.0.0.0 ,I ~*> 0.1.0.0.1 ,I ~*> 0.1.0.0.1.0 ,I ~*> 0.1.0.0.2 ,I ~*> tick ,J ~*> B ,J ~*> J ,J ~*> K ,J ~*> L ,J ~*> 0.1.0.0 ,J ~*> 0.1.0.0.0 ,J ~*> 0.1.0.0.0.0 ,J ~*> 0.1.0.0.0.0.0 ,J ~*> 0.1.0.0.1 ,J ~*> 0.1.0.0.1.0 ,J ~*> 0.1.0.0.2 ,J ~*> tick ,K ~*> B ,K ~*> K ,K ~*> L ,K ~*> 0.1.0.0.0 ,K ~*> 0.1.0.0.0.0 ,K ~*> 0.1.0.0.0.0.0 ,K ~*> 0.1.0.0.1 ,K ~*> 0.1.0.0.1.0 ,K ~*> 0.1.0.0.2 ,K ~*> tick ,L ~*> L ,L ~*> 0.1.0.0.0.0 ,L ~*> 0.1.0.0.0.0.0 ,L ~*> tick ,K ~*> B ,K ~*> J ,K ~*> K ,K ~*> L ,K ~*> 0.1.0.0 ,K ~*> 0.1.0.0.0 ,K ~*> 0.1.0.0.0.0 ,K ~*> 0.1.0.0.0.0.0 ,K ~*> 0.1.0.0.1 ,K ~*> 0.1.0.0.1.0 ,K ~*> 0.1.0.0.2 ,K ~*> tick ,A ~^> B ,A ~^> K ,A ~^> L ,A ~^> 0.1.0.0.0 ,A ~^> 0.1.0.0.0.0 ,A ~^> 0.1.0.0.0.0.0 ,A ~^> 0.1.0.0.1 ,A ~^> 0.1.0.0.1.0 ,A ~^> 0.1.0.0.2 ,A ~^> tick ,B ~^> B ,B ~^> K ,B ~^> L ,B ~^> 0.1.0.0.0 ,B ~^> 0.1.0.0.0.0 ,B ~^> 0.1.0.0.0.0.0 ,B ~^> 0.1.0.0.1 ,B ~^> 0.1.0.0.1.0 ,B ~^> 0.1.0.0.2 ,B ~^> tick ,I ~^> B ,I ~^> J ,I ~^> K ,I ~^> L ,I ~^> 0.1.0.0 ,I ~^> 0.1.0.0.0 ,I ~^> 0.1.0.0.0.0 ,I ~^> 0.1.0.0.0.0.0 ,I ~^> 0.1.0.0.1 ,I ~^> 0.1.0.0.1.0 ,I ~^> 0.1.0.0.2 ,I ~^> tick ,J ~^> B ,J ~^> J ,J ~^> K ,J ~^> L ,J ~^> 0.1.0.0 ,J ~^> 0.1.0.0.0 ,J ~^> 0.1.0.0.0.0 ,J ~^> 0.1.0.0.0.0.0 ,J ~^> 0.1.0.0.1 ,J ~^> 0.1.0.0.1.0 ,J ~^> 0.1.0.0.2 ,J ~^> tick ,K ~^> B ,K ~^> K ,K ~^> L ,K ~^> 0.1.0.0.0 ,K ~^> 0.1.0.0.0.0 ,K ~^> 0.1.0.0.0.0.0 ,K ~^> 0.1.0.0.1 ,K ~^> 0.1.0.0.1.0 ,K ~^> 0.1.0.0.2 ,K ~^> tick ,L ~^> L ,L ~^> 0.1.0.0.0.0 ,L ~^> 0.1.0.0.0.0.0 ,L ~^> tick ,K ~^> B ,K ~^> J ,K ~^> K ,K ~^> L ,K ~^> 0.1.0.0 ,K ~^> 0.1.0.0.0 ,K ~^> 0.1.0.0.0.0 ,K ~^> 0.1.0.0.0.0.0 ,K ~^> 0.1.0.0.1 ,K ~^> 0.1.0.0.1.0 ,K ~^> 0.1.0.0.2 ,K ~^> tick] + f26> [B ~=> 0.1.0.0.1.0 ,K ~=> B ,K ~=> 0.1.0.0.1.0 ,K ~=> C ,huge ~=> H ,huge ~=> X ,A ~+> L ,A ~+> 0.1.0.0.0.0 ,A ~+> 0.1.0.0.0.0.0 ,A ~+> 0.1.0.0.2 ,A ~+> tick ,B ~+> B ,B ~+> K ,B ~+> 0.1.0.0.0 ,B ~+> 0.1.0.0.1 ,B ~+> 0.1.0.0.1.0 ,B ~+> 0.1.0.0.2 ,B ~+> tick ,J ~+> J ,J ~+> 0.1.0.0 ,J ~+> tick ,K ~+> B ,K ~+> K ,K ~+> 0.1.0.0.0 ,K ~+> 0.1.0.0.1 ,K ~+> 0.1.0.0.1.0 ,K ~+> 0.1.0.0.2 ,K ~+> tick ,L ~+> L ,L ~+> 0.1.0.0.0.0 ,L ~+> 0.1.0.0.0.0.0 ,L ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> J ,K ~+> K ,K ~+> 0.1.0.0.0 ,K ~+> 0.1.0.0.1 ,K ~+> 0.1.0.0.1.0 ,K ~+> 0.1.0.0.2 ,K ~+> tick ,A ~*> B ,A ~*> K ,A ~*> L ,A ~*> 0.1.0.0.0 ,A ~*> 0.1.0.0.0.0 ,A ~*> 0.1.0.0.0.0.0 ,A ~*> 0.1.0.0.1 ,A ~*> 0.1.0.0.1.0 ,A ~*> 0.1.0.0.2 ,A ~*> tick ,B ~*> B ,B ~*> K ,B ~*> L ,B ~*> 0.1.0.0.0 ,B ~*> 0.1.0.0.0.0 ,B ~*> 0.1.0.0.0.0.0 ,B ~*> 0.1.0.0.1 ,B ~*> 0.1.0.0.1.0 ,B ~*> 0.1.0.0.2 ,B ~*> tick ,J ~*> B ,J ~*> J ,J ~*> K ,J ~*> L ,J ~*> 0.1.0.0.0 ,J ~*> 0.1.0.0.0.0 ,J ~*> 0.1.0.0.0.0.0 ,J ~*> 0.1.0.0.1 ,J ~*> 0.1.0.0.1.0 ,J ~*> 0.1.0.0.2 ,J ~*> tick ,K ~*> B ,K ~*> K ,K ~*> L ,K ~*> 0.1.0.0.0 ,K ~*> 0.1.0.0.0.0 ,K ~*> 0.1.0.0.0.0.0 ,K ~*> 0.1.0.0.1 ,K ~*> 0.1.0.0.1.0 ,K ~*> 0.1.0.0.2 ,K ~*> tick ,L ~*> L ,L ~*> 0.1.0.0.0.0 ,L ~*> 0.1.0.0.0.0.0 ,L ~*> tick ,K ~*> B ,K ~*> J ,K ~*> K ,K ~*> L ,K ~*> 0.1.0.0 ,K ~*> 0.1.0.0.0 ,K ~*> 0.1.0.0.0.0 ,K ~*> 0.1.0.0.0.0.0 ,K ~*> 0.1.0.0.1 ,K ~*> 0.1.0.0.1.0 ,K ~*> 0.1.0.0.2 ,K ~*> tick ,A ~^> B ,A ~^> K ,A ~^> L ,A ~^> 0.1.0.0.0 ,A ~^> 0.1.0.0.0.0 ,A ~^> 0.1.0.0.0.0.0 ,A ~^> 0.1.0.0.1 ,A ~^> 0.1.0.0.1.0 ,A ~^> 0.1.0.0.2 ,A ~^> tick ,B ~^> B ,B ~^> K ,B ~^> L ,B ~^> 0.1.0.0.0 ,B ~^> 0.1.0.0.0.0 ,B ~^> 0.1.0.0.0.0.0 ,B ~^> 0.1.0.0.1 ,B ~^> 0.1.0.0.1.0 ,B ~^> 0.1.0.0.2 ,B ~^> tick ,J ~^> B ,J ~^> K ,J ~^> L ,J ~^> 0.1.0.0.0 ,J ~^> 0.1.0.0.0.0 ,J ~^> 0.1.0.0.0.0.0 ,J ~^> 0.1.0.0.1 ,J ~^> 0.1.0.0.1.0 ,J ~^> 0.1.0.0.2 ,J ~^> tick ,K ~^> B ,K ~^> K ,K ~^> L ,K ~^> 0.1.0.0.0 ,K ~^> 0.1.0.0.0.0 ,K ~^> 0.1.0.0.0.0.0 ,K ~^> 0.1.0.0.1 ,K ~^> 0.1.0.0.1.0 ,K ~^> 0.1.0.0.2 ,K ~^> tick ,L ~^> L ,L ~^> 0.1.0.0.0.0 ,L ~^> 0.1.0.0.0.0.0 ,L ~^> tick ,K ~^> B ,K ~^> K ,K ~^> L ,K ~^> 0.1.0.0.0 ,K ~^> 0.1.0.0.0.0 ,K ~^> 0.1.0.0.0.0.0 ,K ~^> 0.1.0.0.1 ,K ~^> 0.1.0.0.1.0 ,K ~^> 0.1.0.0.2 ,K ~^> tick] f199> [B ~=> 0.1.0.0.1.0 ,K ~=> B ,K ~=> 0.1.0.0.1.0 ,K ~=> C ,huge ~=> H ,huge ~=> X ,A ~+> L ,A ~+> 0.1.0.0.0.0 ,A ~+> 0.1.0.0.0.0.0 ,A ~+> 0.1.0.0.2 ,A ~+> tick ,B ~+> B ,B ~+> K ,B ~+> 0.1.0.0.0 ,B ~+> 0.1.0.0.1 ,B ~+> 0.1.0.0.1.0 ,B ~+> 0.1.0.0.2 ,B ~+> tick ,J ~+> J ,J ~+> 0.1.0.0 ,J ~+> tick ,K ~+> B ,K ~+> K ,K ~+> 0.1.0.0.0 ,K ~+> 0.1.0.0.1 ,K ~+> 0.1.0.0.1.0 ,K ~+> 0.1.0.0.2 ,K ~+> tick ,L ~+> L ,L ~+> 0.1.0.0.0.0 ,L ~+> 0.1.0.0.0.0.0 ,L ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> J ,K ~+> K ,K ~+> 0.1.0.0.0 ,K ~+> 0.1.0.0.1 ,K ~+> 0.1.0.0.1.0 ,K ~+> 0.1.0.0.2 ,K ~+> tick ,A ~*> B ,A ~*> K ,A ~*> L ,A ~*> 0.1.0.0.0 ,A ~*> 0.1.0.0.0.0 ,A ~*> 0.1.0.0.0.0.0 ,A ~*> 0.1.0.0.1 ,A ~*> 0.1.0.0.1.0 ,A ~*> 0.1.0.0.2 ,A ~*> tick ,B ~*> B ,B ~*> K ,B ~*> L ,B ~*> 0.1.0.0.0 ,B ~*> 0.1.0.0.0.0 ,B ~*> 0.1.0.0.0.0.0 ,B ~*> 0.1.0.0.1 ,B ~*> 0.1.0.0.1.0 ,B ~*> 0.1.0.0.2 ,B ~*> tick ,J ~*> B ,J ~*> J ,J ~*> K ,J ~*> L ,J ~*> 0.1.0.0.0 ,J ~*> 0.1.0.0.0.0 ,J ~*> 0.1.0.0.0.0.0 ,J ~*> 0.1.0.0.1 ,J ~*> 0.1.0.0.1.0 ,J ~*> 0.1.0.0.2 ,J ~*> tick ,K ~*> B ,K ~*> K ,K ~*> L ,K ~*> 0.1.0.0.0 ,K ~*> 0.1.0.0.0.0 ,K ~*> 0.1.0.0.0.0.0 ,K ~*> 0.1.0.0.1 ,K ~*> 0.1.0.0.1.0 ,K ~*> 0.1.0.0.2 ,K ~*> tick ,L ~*> L ,L ~*> 0.1.0.0.0.0 ,L ~*> 0.1.0.0.0.0.0 ,L ~*> tick ,K ~*> B ,K ~*> J ,K ~*> K ,K ~*> L ,K ~*> 0.1.0.0 ,K ~*> 0.1.0.0.0 ,K ~*> 0.1.0.0.0.0 ,K ~*> 0.1.0.0.0.0.0 ,K ~*> 0.1.0.0.1 ,K ~*> 0.1.0.0.1.0 ,K ~*> 0.1.0.0.2 ,K ~*> tick ,A ~^> B ,A ~^> K ,A ~^> L ,A ~^> 0.1.0.0.0 ,A ~^> 0.1.0.0.0.0 ,A ~^> 0.1.0.0.0.0.0 ,A ~^> 0.1.0.0.1 ,A ~^> 0.1.0.0.1.0 ,A ~^> 0.1.0.0.2 ,A ~^> tick ,B ~^> B ,B ~^> K ,B ~^> L ,B ~^> 0.1.0.0.0 ,B ~^> 0.1.0.0.0.0 ,B ~^> 0.1.0.0.0.0.0 ,B ~^> 0.1.0.0.1 ,B ~^> 0.1.0.0.1.0 ,B ~^> 0.1.0.0.2 ,B ~^> tick ,J ~^> B ,J ~^> K ,J ~^> L ,J ~^> 0.1.0.0.0 ,J ~^> 0.1.0.0.0.0 ,J ~^> 0.1.0.0.0.0.0 ,J ~^> 0.1.0.0.1 ,J ~^> 0.1.0.0.1.0 ,J ~^> 0.1.0.0.2 ,J ~^> tick ,K ~^> B ,K ~^> K ,K ~^> L ,K ~^> 0.1.0.0.0 ,K ~^> 0.1.0.0.0.0 ,K ~^> 0.1.0.0.0.0.0 ,K ~^> 0.1.0.0.1 ,K ~^> 0.1.0.0.1.0 ,K ~^> 0.1.0.0.2 ,K ~^> tick ,L ~^> L ,L ~^> 0.1.0.0.0.0 ,L ~^> 0.1.0.0.0.0.0 ,L ~^> tick ,K ~^> B ,K ~^> K ,K ~^> L ,K ~^> 0.1.0.0.0 ,K ~^> 0.1.0.0.0.0 ,K ~^> 0.1.0.0.0.0.0 ,K ~^> 0.1.0.0.1 ,K ~^> 0.1.0.0.1.0 ,K ~^> 0.1.0.0.2 ,K ~^> tick] f26> [B ~=> 0.1.0.0.1.0 ,K ~=> B ,K ~=> 0.1.0.0.1.0 ,K ~=> C ,huge ~=> H ,huge ~=> X ,A ~+> L ,A ~+> 0.1.0.0.0.0 ,A ~+> 0.1.0.0.0.0.0 ,A ~+> 0.1.0.0.2 ,A ~+> tick ,B ~+> B ,B ~+> K ,B ~+> 0.1.0.0.0 ,B ~+> 0.1.0.0.1 ,B ~+> 0.1.0.0.1.0 ,B ~+> 0.1.0.0.2 ,B ~+> tick ,J ~+> J ,J ~+> 0.1.0.0 ,J ~+> tick ,K ~+> B ,K ~+> K ,K ~+> 0.1.0.0.0 ,K ~+> 0.1.0.0.1 ,K ~+> 0.1.0.0.1.0 ,K ~+> 0.1.0.0.2 ,K ~+> tick ,L ~+> L ,L ~+> 0.1.0.0.0.0 ,L ~+> 0.1.0.0.0.0.0 ,L ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> J ,K ~+> K ,K ~+> 0.1.0.0.0 ,K ~+> 0.1.0.0.1 ,K ~+> 0.1.0.0.1.0 ,K ~+> 0.1.0.0.2 ,K ~+> tick ,A ~*> B ,A ~*> K ,A ~*> L ,A ~*> 0.1.0.0.0 ,A ~*> 0.1.0.0.0.0 ,A ~*> 0.1.0.0.0.0.0 ,A ~*> 0.1.0.0.1 ,A ~*> 0.1.0.0.1.0 ,A ~*> 0.1.0.0.2 ,A ~*> tick ,B ~*> B ,B ~*> K ,B ~*> L ,B ~*> 0.1.0.0.0 ,B ~*> 0.1.0.0.0.0 ,B ~*> 0.1.0.0.0.0.0 ,B ~*> 0.1.0.0.1 ,B ~*> 0.1.0.0.1.0 ,B ~*> 0.1.0.0.2 ,B ~*> tick ,J ~*> B ,J ~*> J ,J ~*> K ,J ~*> L ,J ~*> 0.1.0.0.0 ,J ~*> 0.1.0.0.0.0 ,J ~*> 0.1.0.0.0.0.0 ,J ~*> 0.1.0.0.1 ,J ~*> 0.1.0.0.1.0 ,J ~*> 0.1.0.0.2 ,J ~*> tick ,K ~*> B ,K ~*> K ,K ~*> L ,K ~*> 0.1.0.0.0 ,K ~*> 0.1.0.0.0.0 ,K ~*> 0.1.0.0.0.0.0 ,K ~*> 0.1.0.0.1 ,K ~*> 0.1.0.0.1.0 ,K ~*> 0.1.0.0.2 ,K ~*> tick ,L ~*> L ,L ~*> 0.1.0.0.0.0 ,L ~*> 0.1.0.0.0.0.0 ,L ~*> tick ,K ~*> B ,K ~*> J ,K ~*> K ,K ~*> L ,K ~*> 0.1.0.0 ,K ~*> 0.1.0.0.0 ,K ~*> 0.1.0.0.0.0 ,K ~*> 0.1.0.0.0.0.0 ,K ~*> 0.1.0.0.1 ,K ~*> 0.1.0.0.1.0 ,K ~*> 0.1.0.0.2 ,K ~*> tick ,A ~^> B ,A ~^> K ,A ~^> L ,A ~^> 0.1.0.0.0 ,A ~^> 0.1.0.0.0.0 ,A ~^> 0.1.0.0.0.0.0 ,A ~^> 0.1.0.0.1 ,A ~^> 0.1.0.0.1.0 ,A ~^> 0.1.0.0.2 ,A ~^> tick ,B ~^> B ,B ~^> K ,B ~^> L ,B ~^> 0.1.0.0.0 ,B ~^> 0.1.0.0.0.0 ,B ~^> 0.1.0.0.0.0.0 ,B ~^> 0.1.0.0.1 ,B ~^> 0.1.0.0.1.0 ,B ~^> 0.1.0.0.2 ,B ~^> tick ,J ~^> B ,J ~^> K ,J ~^> L ,J ~^> 0.1.0.0.0 ,J ~^> 0.1.0.0.0.0 ,J ~^> 0.1.0.0.0.0.0 ,J ~^> 0.1.0.0.1 ,J ~^> 0.1.0.0.1.0 ,J ~^> 0.1.0.0.2 ,J ~^> tick ,K ~^> B ,K ~^> K ,K ~^> L ,K ~^> 0.1.0.0.0 ,K ~^> 0.1.0.0.0.0 ,K ~^> 0.1.0.0.0.0.0 ,K ~^> 0.1.0.0.1 ,K ~^> 0.1.0.0.1.0 ,K ~^> 0.1.0.0.2 ,K ~^> tick ,L ~^> L ,L ~^> 0.1.0.0.0.0 ,L ~^> 0.1.0.0.0.0.0 ,L ~^> tick ,K ~^> B ,K ~^> K ,K ~^> L ,K ~^> 0.1.0.0.0 ,K ~^> 0.1.0.0.0.0 ,K ~^> 0.1.0.0.0.0.0 ,K ~^> 0.1.0.0.1 ,K ~^> 0.1.0.0.1.0 ,K ~^> 0.1.0.0.2 ,K ~^> tick] f199> [B ~=> 0.1.0.0.1.0 ,K ~=> B ,K ~=> 0.1.0.0.1.0 ,K ~=> C ,huge ~=> H ,huge ~=> X ,A ~+> L ,A ~+> 0.1.0.0.0.0 ,A ~+> 0.1.0.0.0.0.0 ,A ~+> 0.1.0.0.2 ,A ~+> tick ,B ~+> B ,B ~+> K ,B ~+> 0.1.0.0.0 ,B ~+> 0.1.0.0.1 ,B ~+> 0.1.0.0.1.0 ,B ~+> 0.1.0.0.2 ,B ~+> tick ,J ~+> J ,J ~+> 0.1.0.0 ,J ~+> tick ,K ~+> B ,K ~+> K ,K ~+> 0.1.0.0.0 ,K ~+> 0.1.0.0.1 ,K ~+> 0.1.0.0.1.0 ,K ~+> 0.1.0.0.2 ,K ~+> tick ,L ~+> L ,L ~+> 0.1.0.0.0.0 ,L ~+> 0.1.0.0.0.0.0 ,L ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> J ,K ~+> K ,K ~+> 0.1.0.0.0 ,K ~+> 0.1.0.0.1 ,K ~+> 0.1.0.0.1.0 ,K ~+> 0.1.0.0.2 ,K ~+> tick ,A ~*> B ,A ~*> K ,A ~*> L ,A ~*> 0.1.0.0.0 ,A ~*> 0.1.0.0.0.0 ,A ~*> 0.1.0.0.0.0.0 ,A ~*> 0.1.0.0.1 ,A ~*> 0.1.0.0.1.0 ,A ~*> 0.1.0.0.2 ,A ~*> tick ,B ~*> B ,B ~*> K ,B ~*> L ,B ~*> 0.1.0.0.0 ,B ~*> 0.1.0.0.0.0 ,B ~*> 0.1.0.0.0.0.0 ,B ~*> 0.1.0.0.1 ,B ~*> 0.1.0.0.1.0 ,B ~*> 0.1.0.0.2 ,B ~*> tick ,J ~*> B ,J ~*> J ,J ~*> K ,J ~*> L ,J ~*> 0.1.0.0.0 ,J ~*> 0.1.0.0.0.0 ,J ~*> 0.1.0.0.0.0.0 ,J ~*> 0.1.0.0.1 ,J ~*> 0.1.0.0.1.0 ,J ~*> 0.1.0.0.2 ,J ~*> tick ,K ~*> B ,K ~*> K ,K ~*> L ,K ~*> 0.1.0.0.0 ,K ~*> 0.1.0.0.0.0 ,K ~*> 0.1.0.0.0.0.0 ,K ~*> 0.1.0.0.1 ,K ~*> 0.1.0.0.1.0 ,K ~*> 0.1.0.0.2 ,K ~*> tick ,L ~*> L ,L ~*> 0.1.0.0.0.0 ,L ~*> 0.1.0.0.0.0.0 ,L ~*> tick ,K ~*> B ,K ~*> J ,K ~*> K ,K ~*> L ,K ~*> 0.1.0.0 ,K ~*> 0.1.0.0.0 ,K ~*> 0.1.0.0.0.0 ,K ~*> 0.1.0.0.0.0.0 ,K ~*> 0.1.0.0.1 ,K ~*> 0.1.0.0.1.0 ,K ~*> 0.1.0.0.2 ,K ~*> tick ,A ~^> B ,A ~^> K ,A ~^> L ,A ~^> 0.1.0.0.0 ,A ~^> 0.1.0.0.0.0 ,A ~^> 0.1.0.0.0.0.0 ,A ~^> 0.1.0.0.1 ,A ~^> 0.1.0.0.1.0 ,A ~^> 0.1.0.0.2 ,A ~^> tick ,B ~^> B ,B ~^> K ,B ~^> L ,B ~^> 0.1.0.0.0 ,B ~^> 0.1.0.0.0.0 ,B ~^> 0.1.0.0.0.0.0 ,B ~^> 0.1.0.0.1 ,B ~^> 0.1.0.0.1.0 ,B ~^> 0.1.0.0.2 ,B ~^> tick ,J ~^> B ,J ~^> K ,J ~^> L ,J ~^> 0.1.0.0.0 ,J ~^> 0.1.0.0.0.0 ,J ~^> 0.1.0.0.0.0.0 ,J ~^> 0.1.0.0.1 ,J ~^> 0.1.0.0.1.0 ,J ~^> 0.1.0.0.2 ,J ~^> tick ,K ~^> B ,K ~^> K ,K ~^> L ,K ~^> 0.1.0.0.0 ,K ~^> 0.1.0.0.0.0 ,K ~^> 0.1.0.0.0.0.0 ,K ~^> 0.1.0.0.1 ,K ~^> 0.1.0.0.1.0 ,K ~^> 0.1.0.0.2 ,K ~^> tick ,L ~^> L ,L ~^> 0.1.0.0.0.0 ,L ~^> 0.1.0.0.0.0.0 ,L ~^> tick ,K ~^> B ,K ~^> K ,K ~^> L ,K ~^> 0.1.0.0.0 ,K ~^> 0.1.0.0.0.0 ,K ~^> 0.1.0.0.0.0.0 ,K ~^> 0.1.0.0.1 ,K ~^> 0.1.0.0.1.0 ,K ~^> 0.1.0.0.2 ,K ~^> tick] + f42> [huge ~=> H ,A ~+> L ,A ~+> 0.1.0.0.0.0 ,A ~+> 0.1.0.0.0.0.0 ,A ~+> tick ,B ~+> 0.1.0.0.0 ,B ~+> tick ,K ~+> K ,K ~+> 0.1.0.0.0 ,K ~+> tick ,L ~+> L ,L ~+> 0.1.0.0.0.0 ,L ~+> 0.1.0.0.0.0.0 ,L ~+> tick ,tick ~+> tick ,K ~+> K ,A ~*> L ,A ~*> 0.1.0.0.0.0 ,A ~*> 0.1.0.0.0.0.0 ,A ~*> tick ,B ~*> K ,B ~*> L ,B ~*> 0.1.0.0.0.0 ,B ~*> 0.1.0.0.0.0.0 ,B ~*> tick ,K ~*> K ,K ~*> L ,K ~*> 0.1.0.0.0.0 ,K ~*> 0.1.0.0.0.0.0 ,K ~*> tick ,L ~*> L ,L ~*> 0.1.0.0.0.0 ,L ~*> 0.1.0.0.0.0.0 ,L ~*> tick ,K ~*> K ,A ~^> L ,A ~^> 0.1.0.0.0.0 ,A ~^> 0.1.0.0.0.0.0 ,A ~^> tick ,B ~^> L ,B ~^> 0.1.0.0.0.0 ,B ~^> 0.1.0.0.0.0.0 ,B ~^> tick ,K ~^> L ,K ~^> 0.1.0.0.0.0 ,K ~^> 0.1.0.0.0.0.0 ,K ~^> tick ,L ~^> L ,L ~^> 0.1.0.0.0.0 ,L ~^> 0.1.0.0.0.0.0 ,L ~^> tick] + f42> [A ~+> L ,A ~+> 0.1.0.0.0.0 ,A ~+> 0.1.0.0.0.0.0 ,A ~+> tick ,L ~+> L ,L ~+> 0.1.0.0.0.0 ,L ~+> 0.1.0.0.0.0.0 ,L ~+> tick ,tick ~+> tick ,A ~*> L ,A ~*> tick ,L ~*> L ,L ~*> tick ,A ~^> L ,L ~^> L] f47> [A ~+> L ,A ~+> 0.1.0.0.0.0 ,A ~+> 0.1.0.0.0.0.0 ,A ~+> tick ,L ~+> L ,L ~+> 0.1.0.0.0.0 ,L ~+> 0.1.0.0.0.0.0 ,L ~+> tick ,tick ~+> tick ,A ~*> L ,A ~*> tick ,L ~*> L ,L ~*> tick ,A ~^> L ,L ~^> L] f42> [A ~+> L ,A ~+> 0.1.0.0.0.0 ,A ~+> 0.1.0.0.0.0.0 ,A ~+> tick ,L ~+> L ,L ~+> 0.1.0.0.0.0 ,L ~+> 0.1.0.0.0.0.0 ,L ~+> tick ,tick ~+> tick ,A ~*> L ,A ~*> 0.1.0.0.0.0.0 ,A ~*> tick ,L ~*> L ,L ~*> 0.1.0.0.0.0.0 ,L ~*> tick ,A ~^> L ,A ~^> 0.1.0.0.0.0.0 ,A ~^> tick ,L ~^> L ,L ~^> 0.1.0.0.0.0.0 ,L ~^> tick] f47> [A ~+> L ,A ~+> 0.1.0.0.0.0 ,A ~+> 0.1.0.0.0.0.0 ,A ~+> tick ,L ~+> L ,L ~+> 0.1.0.0.0.0 ,L ~+> 0.1.0.0.0.0.0 ,L ~+> tick ,tick ~+> tick ,A ~*> L ,A ~*> 0.1.0.0.0.0.0 ,A ~*> tick ,L ~*> L ,L ~*> 0.1.0.0.0.0.0 ,L ~*> tick ,A ~^> L ,A ~^> 0.1.0.0.0.0.0 ,A ~^> tick ,L ~^> L ,L ~^> 0.1.0.0.0.0.0 ,L ~^> tick] + f42> [A ~+> L ,A ~+> 0.1.0.0.0.0.0 ,A ~+> tick ,L ~+> L ,L ~+> 0.1.0.0.0.0.0 ,L ~+> tick ,tick ~+> tick ,A ~*> L ,L ~*> L] + f164> [B ~=> 0.1.0.0.1.0 ,K ~=> B ,K ~=> 0.1.0.0.1.0 ,huge ~=> H ,B ~+> B ,B ~+> K ,B ~+> 0.1.0.0.1 ,B ~+> 0.1.0.0.1.0 ,B ~+> tick ,K ~+> B ,K ~+> K ,K ~+> 0.1.0.0.1 ,K ~+> 0.1.0.0.1.0 ,K ~+> tick ,tick ~+> tick ,K ~+> 0.1.0.0.1 ,K ~+> tick ,B ~*> B ,B ~*> K ,B ~*> 0.1.0.0.1.0 ,B ~*> tick ,K ~*> B ,K ~*> K ,K ~*> 0.1.0.0.1.0 ,K ~*> tick ,K ~*> B ,K ~*> K ,K ~*> 0.1.0.0.1.0 ,K ~*> tick ,B ~^> B ,B ~^> K ,B ~^> 0.1.0.0.1.0 ,B ~^> tick ,K ~^> B ,K ~^> K ,K ~^> 0.1.0.0.1.0 ,K ~^> tick ,K ~^> B ,K ~^> K ,K ~^> 0.1.0.0.1.0 ,K ~^> tick] + f167> [B ~=> 0.1.0.0.1.0,K ~=> B,B ~+> tick,tick ~+> tick] f164> [B ~=> 0.1.0.0.1.0,K ~=> B,B ~+> tick,tick ~+> tick] f167> [B ~=> 0.1.0.0.1.0,K ~=> B,B ~+> tick,tick ~+> tick] f164> [B ~=> 0.1.0.0.1.0,K ~=> B,B ~+> tick,tick ~+> tick] + f176> [A ~+> 0.1.0.0.2 ,A ~+> tick ,B ~+> B ,B ~+> 0.1.0.0.2 ,B ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> 0.1.0.0.2 ,K ~+> tick ,A ~*> B ,B ~*> B ,K ~*> B] YES(?,PRIMREC)