YES(?,PRIMREC) * Step 1: TrivialSCCs MAYBE + Considered Problem: Rules: 0. 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) -> f13(A,0,0,2*A,4*A,3 + 4*A,4 + 4*A,A,C1,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [1 >= A*B1 && A*B1 + B1 >= 2 && C1 >= B1 && 1 >= A*D1 && A*D1 + D1 >= 2 && D1 >= C1] (1,1) 1. f13(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) -> f24(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) [A + -1*H >= 0 && -1*A + H >= 0 && -1*C >= 0 && C >= 0 && J >= 1 + D] (?,1) 2. f13(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) -> f13(A,1 + B + -2*C1 + C1^2,C,D,E,F,G,H,I,1 + J,C1,1 + -1*C1,1 + -2*C1 + C1^2,N,O,P,Q,R,S,T,U,V,W,X,Y,Z[A + -1*H >= 0 && -1*A + H >= 0 && -1*C >= 0 && C >= 0 && 0 >= C1 && D >= J] (?,1) ,A1) 3. f13(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) -> f13(A,1 + B + -2*C1 + C1^2,C,D,E,F,G,H,I,1 + J,C1,1 + -1*C1,1 + -2*C1 + C1^2,N,O,P,Q,R,S,T,U,V,W,X,Y,Z[A + -1*H >= 0 && -1*A + H >= 0 && -1*C >= 0 && C >= 0 && C1 >= 2 && D >= J] (?,1) ,A1) 4. f13(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) -> f13(A,B,C,D,E,F,G,H,I,1 + J,1,0,0,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [A + -1*H >= 0 && -1*A + H >= 0 && -1*C >= 0 && C >= 0 && D >= J] (?,1) 5. f24(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) -> f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,0,Q,R,S,T,U,V,W,X,Y,Z,A1) [A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1*C >= 0 && C >= 0 && J >= 1 + A && P = 0] (?,1) 6. f24(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) -> f31(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) [A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1*C >= 0 && C >= 0 && P >= 1 && J >= 1 + A] (?,1) 7. f24(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) -> f31(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) [A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1*C >= 0 && C >= 0 && 0 >= 1 + P && J >= 1 + A] (?,1) 8. f24(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) -> f24(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) [A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1*C >= 0 && C >= 0 && A >= J] (?,1) 9. f37(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) -> f118(A,B,C*E,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*A + J >= 0 && O >= 1 + N] 10. f37(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) -> f40(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) [-1 + -1*H + J >= 0 && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*A + J >= 0 && N >= O] (?,1) 11. f31(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) -> f37(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) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + J >= 0 && J >= 1 + A] 12. f118(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) -> 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) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*N + O >= 0 && -1 + -1*A + J >= 0 && J >= 1 + A] 13. f40(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) -> f71(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) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && Q >= 1] 14. f40(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) -> f64(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,0,Q,R,S,T,U,V,W,X,Y,Z,A1) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && 0 >= Q && P = 0] 15. f40(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) -> f44(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) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && P >= 1 && 0 >= Q] 16. f40(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) -> f44(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) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && 0 >= 1 + P && 0 >= Q] 17. f71(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) -> f86(A,B,C,D,E,F,G,H,I,J,K,C1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,B1^2,A1) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1 + Q >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && B1 >= 1 && J >= 1 + D] 18. f71(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) -> f86(A,B,C,D,E,F,G,H,I,J,K,C1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,B1^2,A1) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1 + Q >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && 0 >= 1 + B1 && J >= 1 + D] 19. f71(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) -> f86(A,B,C,D,E,F,G,H,I,J,K,C1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,0,A1) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1 + Q >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && J >= 1 + D] 20. f64(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) -> f40(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,1 + Q,R,S,T,U,V,W,X,Y,Z,A1) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1*Q >= 0 && P + -1*Q >= 0 && -1*P + -1*Q >= 0 && -1*P >= 0 && P >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && J >= 1 + E] 21. f64(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) -> f64(A,B,C,D,E,F,G,H,I,2 + J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1*Q >= 0 && P + -1*Q >= 0 && -1*P + -1*Q >= 0 && -1*P >= 0 && P >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && E >= J] 22. f44(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) -> f50(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) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1*Q >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && J >= 1 + A] 23. f50(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) -> f57(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,D + Q) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1*Q >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && J >= 1 + A] 24. f86(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) -> f91(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,L^2,V,W,X,Y,Z,A1) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1 + Q >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && L >= 1] 25. f86(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) -> f91(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,L^2,V,W,X,Y,Z,A1) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1 + Q >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && 0 >= 1 + L] 26. f86(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) -> f91(A,B,C,D,E,F,G,H,I,J,K,0,M,N,O,P,Q,R,S,T,0,V,W,X,Y,Z,A1) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1 + Q >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && L = 0] 27. f57(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) -> f40(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,1 + Q,R,S,T,U,V,W,X,Y,Z,A1) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1*A1 + D >= 0 && -1 + -1*A1 + J >= 0 && -1*Q >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && J >= 1 + A] 28. f91(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) -> f37(A,B,B + C,D,E,F,G,H,I,J,K,L,M,N,1 + O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1 + Q >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && J >= 1 + A] Signature: {(f1,27) ;(f118,27) ;(f13,27) ;(f2,27) ;(f24,27) ;(f31,27) ;(f37,27) ;(f40,27) ;(f44,27) ;(f50,27) ;(f57,27) ;(f64,27) ;(f71,27) ;(f86,27) ;(f91,27)} Flow Graph: [0->{1,2,3,4},1->{5,6,7,8},2->{1,2,3,4},3->{1,2,3,4},4->{1,2,3,4},5->{9,10},6->{11},7->{11},8->{5,6,7,8} ,9->{12},10->{13,14,15,16},11->{9,10},12->{},13->{17,18,19},14->{20,21},15->{22},16->{22},17->{24,25,26} ,18->{24,25,26},19->{24,25,26},20->{13,14,15,16},21->{20,21},22->{23},23->{27},24->{28},25->{28},26->{28} ,27->{13,14,15,16},28->{9,10}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: UnsatPaths MAYBE + Considered Problem: Rules: 0. 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) -> f13(A,0,0,2*A,4*A,3 + 4*A,4 + 4*A,A,C1,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [1 >= A*B1 && A*B1 + B1 >= 2 && C1 >= B1 && 1 >= A*D1 && A*D1 + D1 >= 2 && D1 >= C1] (1,1) 1. f13(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) -> f24(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) [A + -1*H >= 0 && -1*A + H >= 0 && -1*C >= 0 && C >= 0 && J >= 1 + D] (1,1) 2. f13(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) -> f13(A,1 + B + -2*C1 + C1^2,C,D,E,F,G,H,I,1 + J,C1,1 + -1*C1,1 + -2*C1 + C1^2,N,O,P,Q,R,S,T,U,V,W,X,Y,Z[A + -1*H >= 0 && -1*A + H >= 0 && -1*C >= 0 && C >= 0 && 0 >= C1 && D >= J] (?,1) ,A1) 3. f13(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) -> f13(A,1 + B + -2*C1 + C1^2,C,D,E,F,G,H,I,1 + J,C1,1 + -1*C1,1 + -2*C1 + C1^2,N,O,P,Q,R,S,T,U,V,W,X,Y,Z[A + -1*H >= 0 && -1*A + H >= 0 && -1*C >= 0 && C >= 0 && C1 >= 2 && D >= J] (?,1) ,A1) 4. f13(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) -> f13(A,B,C,D,E,F,G,H,I,1 + J,1,0,0,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [A + -1*H >= 0 && -1*A + H >= 0 && -1*C >= 0 && C >= 0 && D >= J] (?,1) 5. f24(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) -> f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,0,Q,R,S,T,U,V,W,X,Y,Z,A1) [A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1*C >= 0 && C >= 0 && J >= 1 + A && P = 0] (1,1) 6. f24(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) -> f31(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) [A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1*C >= 0 && C >= 0 && P >= 1 && J >= 1 + A] (1,1) 7. f24(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) -> f31(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) [A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1*C >= 0 && C >= 0 && 0 >= 1 + P && J >= 1 + A] (1,1) 8. f24(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) -> f24(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) [A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1*C >= 0 && C >= 0 && A >= J] (?,1) 9. f37(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) -> f118(A,B,C*E,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [-1 + -1*H + J >= 0 (1,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*A + J >= 0 && O >= 1 + N] 10. f37(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) -> f40(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) [-1 + -1*H + J >= 0 && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*A + J >= 0 && N >= O] (?,1) 11. f31(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) -> f37(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) [-1 + -1*H + J >= 0 (1,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + J >= 0 && J >= 1 + A] 12. f118(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) -> 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) [-1 + -1*H + J >= 0 (1,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*N + O >= 0 && -1 + -1*A + J >= 0 && J >= 1 + A] 13. f40(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) -> f71(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) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && Q >= 1] 14. f40(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) -> f64(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,0,Q,R,S,T,U,V,W,X,Y,Z,A1) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && 0 >= Q && P = 0] 15. f40(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) -> f44(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) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && P >= 1 && 0 >= Q] 16. f40(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) -> f44(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) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && 0 >= 1 + P && 0 >= Q] 17. f71(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) -> f86(A,B,C,D,E,F,G,H,I,J,K,C1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,B1^2,A1) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1 + Q >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && B1 >= 1 && J >= 1 + D] 18. f71(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) -> f86(A,B,C,D,E,F,G,H,I,J,K,C1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,B1^2,A1) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1 + Q >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && 0 >= 1 + B1 && J >= 1 + D] 19. f71(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) -> f86(A,B,C,D,E,F,G,H,I,J,K,C1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,0,A1) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1 + Q >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && J >= 1 + D] 20. f64(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) -> f40(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,1 + Q,R,S,T,U,V,W,X,Y,Z,A1) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1*Q >= 0 && P + -1*Q >= 0 && -1*P + -1*Q >= 0 && -1*P >= 0 && P >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && J >= 1 + E] 21. f64(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) -> f64(A,B,C,D,E,F,G,H,I,2 + J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1*Q >= 0 && P + -1*Q >= 0 && -1*P + -1*Q >= 0 && -1*P >= 0 && P >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && E >= J] 22. f44(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) -> f50(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) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1*Q >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && J >= 1 + A] 23. f50(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) -> f57(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,D + Q) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1*Q >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && J >= 1 + A] 24. f86(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) -> f91(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,L^2,V,W,X,Y,Z,A1) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1 + Q >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && L >= 1] 25. f86(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) -> f91(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,L^2,V,W,X,Y,Z,A1) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1 + Q >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && 0 >= 1 + L] 26. f86(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) -> f91(A,B,C,D,E,F,G,H,I,J,K,0,M,N,O,P,Q,R,S,T,0,V,W,X,Y,Z,A1) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1 + Q >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && L = 0] 27. f57(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) -> f40(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,1 + Q,R,S,T,U,V,W,X,Y,Z,A1) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1*A1 + D >= 0 && -1 + -1*A1 + J >= 0 && -1*Q >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && J >= 1 + A] 28. f91(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) -> f37(A,B,B + C,D,E,F,G,H,I,J,K,L,M,N,1 + O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1 + Q >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && J >= 1 + A] Signature: {(f1,27) ;(f118,27) ;(f13,27) ;(f2,27) ;(f24,27) ;(f31,27) ;(f37,27) ;(f40,27) ;(f44,27) ;(f50,27) ;(f57,27) ;(f64,27) ;(f71,27) ;(f86,27) ;(f91,27)} Flow Graph: [0->{1,2,3,4},1->{5,6,7,8},2->{1,2,3,4},3->{1,2,3,4},4->{1,2,3,4},5->{9,10},6->{11},7->{11},8->{5,6,7,8} ,9->{12},10->{13,14,15,16},11->{9,10},12->{},13->{17,18,19},14->{20,21},15->{22},16->{22},17->{24,25,26} ,18->{24,25,26},19->{24,25,26},20->{13,14,15,16},21->{20,21},22->{23},23->{27},24->{28},25->{28},26->{28} ,27->{13,14,15,16},28->{9,10}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(20,15),(20,16)] * Step 3: AddSinks MAYBE + Considered Problem: Rules: 0. 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) -> f13(A,0,0,2*A,4*A,3 + 4*A,4 + 4*A,A,C1,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [1 >= A*B1 && A*B1 + B1 >= 2 && C1 >= B1 && 1 >= A*D1 && A*D1 + D1 >= 2 && D1 >= C1] (1,1) 1. f13(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) -> f24(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) [A + -1*H >= 0 && -1*A + H >= 0 && -1*C >= 0 && C >= 0 && J >= 1 + D] (1,1) 2. f13(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) -> f13(A,1 + B + -2*C1 + C1^2,C,D,E,F,G,H,I,1 + J,C1,1 + -1*C1,1 + -2*C1 + C1^2,N,O,P,Q,R,S,T,U,V,W,X,Y,Z[A + -1*H >= 0 && -1*A + H >= 0 && -1*C >= 0 && C >= 0 && 0 >= C1 && D >= J] (?,1) ,A1) 3. f13(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) -> f13(A,1 + B + -2*C1 + C1^2,C,D,E,F,G,H,I,1 + J,C1,1 + -1*C1,1 + -2*C1 + C1^2,N,O,P,Q,R,S,T,U,V,W,X,Y,Z[A + -1*H >= 0 && -1*A + H >= 0 && -1*C >= 0 && C >= 0 && C1 >= 2 && D >= J] (?,1) ,A1) 4. f13(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) -> f13(A,B,C,D,E,F,G,H,I,1 + J,1,0,0,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [A + -1*H >= 0 && -1*A + H >= 0 && -1*C >= 0 && C >= 0 && D >= J] (?,1) 5. f24(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) -> f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,0,Q,R,S,T,U,V,W,X,Y,Z,A1) [A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1*C >= 0 && C >= 0 && J >= 1 + A && P = 0] (1,1) 6. f24(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) -> f31(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) [A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1*C >= 0 && C >= 0 && P >= 1 && J >= 1 + A] (1,1) 7. f24(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) -> f31(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) [A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1*C >= 0 && C >= 0 && 0 >= 1 + P && J >= 1 + A] (1,1) 8. f24(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) -> f24(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) [A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1*C >= 0 && C >= 0 && A >= J] (?,1) 9. f37(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) -> f118(A,B,C*E,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [-1 + -1*H + J >= 0 (1,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*A + J >= 0 && O >= 1 + N] 10. f37(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) -> f40(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) [-1 + -1*H + J >= 0 && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*A + J >= 0 && N >= O] (?,1) 11. f31(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) -> f37(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) [-1 + -1*H + J >= 0 (1,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + J >= 0 && J >= 1 + A] 12. f118(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) -> 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) [-1 + -1*H + J >= 0 (1,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*N + O >= 0 && -1 + -1*A + J >= 0 && J >= 1 + A] 13. f40(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) -> f71(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) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && Q >= 1] 14. f40(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) -> f64(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,0,Q,R,S,T,U,V,W,X,Y,Z,A1) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && 0 >= Q && P = 0] 15. f40(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) -> f44(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) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && P >= 1 && 0 >= Q] 16. f40(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) -> f44(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) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && 0 >= 1 + P && 0 >= Q] 17. f71(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) -> f86(A,B,C,D,E,F,G,H,I,J,K,C1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,B1^2,A1) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1 + Q >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && B1 >= 1 && J >= 1 + D] 18. f71(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) -> f86(A,B,C,D,E,F,G,H,I,J,K,C1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,B1^2,A1) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1 + Q >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && 0 >= 1 + B1 && J >= 1 + D] 19. f71(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) -> f86(A,B,C,D,E,F,G,H,I,J,K,C1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,0,A1) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1 + Q >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && J >= 1 + D] 20. f64(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) -> f40(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,1 + Q,R,S,T,U,V,W,X,Y,Z,A1) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1*Q >= 0 && P + -1*Q >= 0 && -1*P + -1*Q >= 0 && -1*P >= 0 && P >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && J >= 1 + E] 21. f64(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) -> f64(A,B,C,D,E,F,G,H,I,2 + J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1*Q >= 0 && P + -1*Q >= 0 && -1*P + -1*Q >= 0 && -1*P >= 0 && P >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && E >= J] 22. f44(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) -> f50(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) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1*Q >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && J >= 1 + A] 23. f50(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) -> f57(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,D + Q) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1*Q >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && J >= 1 + A] 24. f86(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) -> f91(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,L^2,V,W,X,Y,Z,A1) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1 + Q >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && L >= 1] 25. f86(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) -> f91(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,L^2,V,W,X,Y,Z,A1) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1 + Q >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && 0 >= 1 + L] 26. f86(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) -> f91(A,B,C,D,E,F,G,H,I,J,K,0,M,N,O,P,Q,R,S,T,0,V,W,X,Y,Z,A1) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1 + Q >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && L = 0] 27. f57(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) -> f40(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,1 + Q,R,S,T,U,V,W,X,Y,Z,A1) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1*A1 + D >= 0 && -1 + -1*A1 + J >= 0 && -1*Q >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && J >= 1 + A] 28. f91(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) -> f37(A,B,B + C,D,E,F,G,H,I,J,K,L,M,N,1 + O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1 + Q >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && J >= 1 + A] Signature: {(f1,27) ;(f118,27) ;(f13,27) ;(f2,27) ;(f24,27) ;(f31,27) ;(f37,27) ;(f40,27) ;(f44,27) ;(f50,27) ;(f57,27) ;(f64,27) ;(f71,27) ;(f86,27) ;(f91,27)} Flow Graph: [0->{1,2,3,4},1->{5,6,7,8},2->{1,2,3,4},3->{1,2,3,4},4->{1,2,3,4},5->{9,10},6->{11},7->{11},8->{5,6,7,8} ,9->{12},10->{13,14,15,16},11->{9,10},12->{},13->{17,18,19},14->{20,21},15->{22},16->{22},17->{24,25,26} ,18->{24,25,26},19->{24,25,26},20->{13,14},21->{20,21},22->{23},23->{27},24->{28},25->{28},26->{28},27->{13 ,14,15,16},28->{9,10}] + Applied Processor: AddSinks + Details: () * Step 4: UnsatPaths MAYBE + Considered Problem: Rules: 0. 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) -> f13(A,0,0,2*A,4*A,3 + 4*A,4 + 4*A,A,C1,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [1 >= A*B1 && A*B1 + B1 >= 2 && C1 >= B1 && 1 >= A*D1 && A*D1 + D1 >= 2 && D1 >= C1] (1,1) 1. f13(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) -> f24(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) [A + -1*H >= 0 && -1*A + H >= 0 && -1*C >= 0 && C >= 0 && J >= 1 + D] (?,1) 2. f13(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) -> f13(A,1 + B + -2*C1 + C1^2,C,D,E,F,G,H,I,1 + J,C1,1 + -1*C1,1 + -2*C1 + C1^2,N,O,P,Q,R,S,T,U,V,W,X,Y,Z[A + -1*H >= 0 && -1*A + H >= 0 && -1*C >= 0 && C >= 0 && 0 >= C1 && D >= J] (?,1) ,A1) 3. f13(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) -> f13(A,1 + B + -2*C1 + C1^2,C,D,E,F,G,H,I,1 + J,C1,1 + -1*C1,1 + -2*C1 + C1^2,N,O,P,Q,R,S,T,U,V,W,X,Y,Z[A + -1*H >= 0 && -1*A + H >= 0 && -1*C >= 0 && C >= 0 && C1 >= 2 && D >= J] (?,1) ,A1) 4. f13(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) -> f13(A,B,C,D,E,F,G,H,I,1 + J,1,0,0,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [A + -1*H >= 0 && -1*A + H >= 0 && -1*C >= 0 && C >= 0 && D >= J] (?,1) 5. f24(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) -> f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,0,Q,R,S,T,U,V,W,X,Y,Z,A1) [A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1*C >= 0 && C >= 0 && J >= 1 + A && P = 0] (?,1) 6. f24(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) -> f31(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) [A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1*C >= 0 && C >= 0 && P >= 1 && J >= 1 + A] (?,1) 7. f24(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) -> f31(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) [A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1*C >= 0 && C >= 0 && 0 >= 1 + P && J >= 1 + A] (?,1) 8. f24(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) -> f24(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) [A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1*C >= 0 && C >= 0 && A >= J] (?,1) 9. f37(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) -> f118(A,B,C*E,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*A + J >= 0 && O >= 1 + N] 10. f37(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) -> f40(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) [-1 + -1*H + J >= 0 && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*A + J >= 0 && N >= O] (?,1) 11. f31(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) -> f37(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) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + J >= 0 && J >= 1 + A] 12. f118(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) -> 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) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*N + O >= 0 && -1 + -1*A + J >= 0 && J >= 1 + A] 13. f40(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) -> f71(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) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && Q >= 1] 14. f40(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) -> f64(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,0,Q,R,S,T,U,V,W,X,Y,Z,A1) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && 0 >= Q && P = 0] 15. f40(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) -> f44(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) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && P >= 1 && 0 >= Q] 16. f40(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) -> f44(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) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && 0 >= 1 + P && 0 >= Q] 17. f71(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) -> f86(A,B,C,D,E,F,G,H,I,J,K,C1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,B1^2,A1) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1 + Q >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && B1 >= 1 && J >= 1 + D] 18. f71(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) -> f86(A,B,C,D,E,F,G,H,I,J,K,C1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,B1^2,A1) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1 + Q >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && 0 >= 1 + B1 && J >= 1 + D] 19. f71(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) -> f86(A,B,C,D,E,F,G,H,I,J,K,C1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,0,A1) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1 + Q >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && J >= 1 + D] 20. f64(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) -> f40(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,1 + Q,R,S,T,U,V,W,X,Y,Z,A1) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1*Q >= 0 && P + -1*Q >= 0 && -1*P + -1*Q >= 0 && -1*P >= 0 && P >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && J >= 1 + E] 21. f64(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) -> f64(A,B,C,D,E,F,G,H,I,2 + J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1*Q >= 0 && P + -1*Q >= 0 && -1*P + -1*Q >= 0 && -1*P >= 0 && P >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && E >= J] 22. f44(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) -> f50(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) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1*Q >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && J >= 1 + A] 23. f50(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) -> f57(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,D + Q) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1*Q >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && J >= 1 + A] 24. f86(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) -> f91(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,L^2,V,W,X,Y,Z,A1) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1 + Q >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && L >= 1] 25. f86(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) -> f91(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,L^2,V,W,X,Y,Z,A1) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1 + Q >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && 0 >= 1 + L] 26. f86(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) -> f91(A,B,C,D,E,F,G,H,I,J,K,0,M,N,O,P,Q,R,S,T,0,V,W,X,Y,Z,A1) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1 + Q >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && L = 0] 27. f57(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) -> f40(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,1 + Q,R,S,T,U,V,W,X,Y,Z,A1) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1*A1 + D >= 0 && -1 + -1*A1 + J >= 0 && -1*Q >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && J >= 1 + A] 28. f91(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) -> f37(A,B,B + C,D,E,F,G,H,I,J,K,L,M,N,1 + O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1 + Q >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && J >= 1 + A] 29. f118(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) -> exitus616(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) True (?,1) Signature: {(exitus616,27) ;(f1,27) ;(f118,27) ;(f13,27) ;(f2,27) ;(f24,27) ;(f31,27) ;(f37,27) ;(f40,27) ;(f44,27) ;(f50,27) ;(f57,27) ;(f64,27) ;(f71,27) ;(f86,27) ;(f91,27)} Flow Graph: [0->{1,2,3,4},1->{5,6,7,8},2->{1,2,3,4},3->{1,2,3,4},4->{1,2,3,4},5->{9,10},6->{11},7->{11},8->{5,6,7,8} ,9->{12,29},10->{13,14,15,16},11->{9,10},12->{},13->{17,18,19},14->{20,21},15->{22},16->{22},17->{24,25,26} ,18->{24,25,26},19->{24,25,26},20->{13,14,15,16},21->{20,21},22->{23},23->{27},24->{28},25->{28},26->{28} ,27->{13,14,15,16},28->{9,10},29->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(20,15),(20,16)] * Step 5: LooptreeTransformer MAYBE + Considered Problem: Rules: 0. 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) -> f13(A,0,0,2*A,4*A,3 + 4*A,4 + 4*A,A,C1,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [1 >= A*B1 && A*B1 + B1 >= 2 && C1 >= B1 && 1 >= A*D1 && A*D1 + D1 >= 2 && D1 >= C1] (1,1) 1. f13(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) -> f24(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) [A + -1*H >= 0 && -1*A + H >= 0 && -1*C >= 0 && C >= 0 && J >= 1 + D] (?,1) 2. f13(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) -> f13(A,1 + B + -2*C1 + C1^2,C,D,E,F,G,H,I,1 + J,C1,1 + -1*C1,1 + -2*C1 + C1^2,N,O,P,Q,R,S,T,U,V,W,X,Y,Z[A + -1*H >= 0 && -1*A + H >= 0 && -1*C >= 0 && C >= 0 && 0 >= C1 && D >= J] (?,1) ,A1) 3. f13(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) -> f13(A,1 + B + -2*C1 + C1^2,C,D,E,F,G,H,I,1 + J,C1,1 + -1*C1,1 + -2*C1 + C1^2,N,O,P,Q,R,S,T,U,V,W,X,Y,Z[A + -1*H >= 0 && -1*A + H >= 0 && -1*C >= 0 && C >= 0 && C1 >= 2 && D >= J] (?,1) ,A1) 4. f13(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) -> f13(A,B,C,D,E,F,G,H,I,1 + J,1,0,0,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [A + -1*H >= 0 && -1*A + H >= 0 && -1*C >= 0 && C >= 0 && D >= J] (?,1) 5. f24(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) -> f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,0,Q,R,S,T,U,V,W,X,Y,Z,A1) [A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1*C >= 0 && C >= 0 && J >= 1 + A && P = 0] (?,1) 6. f24(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) -> f31(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) [A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1*C >= 0 && C >= 0 && P >= 1 && J >= 1 + A] (?,1) 7. f24(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) -> f31(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) [A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1*C >= 0 && C >= 0 && 0 >= 1 + P && J >= 1 + A] (?,1) 8. f24(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) -> f24(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) [A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1*C >= 0 && C >= 0 && A >= J] (?,1) 9. f37(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) -> f118(A,B,C*E,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*A + J >= 0 && O >= 1 + N] 10. f37(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) -> f40(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) [-1 + -1*H + J >= 0 && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*A + J >= 0 && N >= O] (?,1) 11. f31(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) -> f37(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) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + J >= 0 && J >= 1 + A] 12. f118(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) -> 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) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*N + O >= 0 && -1 + -1*A + J >= 0 && J >= 1 + A] 13. f40(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) -> f71(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) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && Q >= 1] 14. f40(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) -> f64(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,0,Q,R,S,T,U,V,W,X,Y,Z,A1) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && 0 >= Q && P = 0] 15. f40(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) -> f44(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) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && P >= 1 && 0 >= Q] 16. f40(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) -> f44(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) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && 0 >= 1 + P && 0 >= Q] 17. f71(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) -> f86(A,B,C,D,E,F,G,H,I,J,K,C1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,B1^2,A1) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1 + Q >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && B1 >= 1 && J >= 1 + D] 18. f71(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) -> f86(A,B,C,D,E,F,G,H,I,J,K,C1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,B1^2,A1) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1 + Q >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && 0 >= 1 + B1 && J >= 1 + D] 19. f71(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) -> f86(A,B,C,D,E,F,G,H,I,J,K,C1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,0,A1) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1 + Q >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && J >= 1 + D] 20. f64(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) -> f40(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,1 + Q,R,S,T,U,V,W,X,Y,Z,A1) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1*Q >= 0 && P + -1*Q >= 0 && -1*P + -1*Q >= 0 && -1*P >= 0 && P >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && J >= 1 + E] 21. f64(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) -> f64(A,B,C,D,E,F,G,H,I,2 + J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1*Q >= 0 && P + -1*Q >= 0 && -1*P + -1*Q >= 0 && -1*P >= 0 && P >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && E >= J] 22. f44(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) -> f50(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) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1*Q >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && J >= 1 + A] 23. f50(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) -> f57(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,D + Q) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1*Q >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && J >= 1 + A] 24. f86(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) -> f91(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,L^2,V,W,X,Y,Z,A1) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1 + Q >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && L >= 1] 25. f86(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) -> f91(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,L^2,V,W,X,Y,Z,A1) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1 + Q >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && 0 >= 1 + L] 26. f86(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) -> f91(A,B,C,D,E,F,G,H,I,J,K,0,M,N,O,P,Q,R,S,T,0,V,W,X,Y,Z,A1) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1 + Q >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && L = 0] 27. f57(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) -> f40(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,1 + Q,R,S,T,U,V,W,X,Y,Z,A1) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1*A1 + D >= 0 && -1 + -1*A1 + J >= 0 && -1*Q >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && J >= 1 + A] 28. f91(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) -> f37(A,B,B + C,D,E,F,G,H,I,J,K,L,M,N,1 + O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1 + Q >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && J >= 1 + A] 29. f118(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) -> exitus616(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) True (?,1) Signature: {(exitus616,27) ;(f1,27) ;(f118,27) ;(f13,27) ;(f2,27) ;(f24,27) ;(f31,27) ;(f37,27) ;(f40,27) ;(f44,27) ;(f50,27) ;(f57,27) ;(f64,27) ;(f71,27) ;(f86,27) ;(f91,27)} Flow Graph: [0->{1,2,3,4},1->{5,6,7,8},2->{1,2,3,4},3->{1,2,3,4},4->{1,2,3,4},5->{9,10},6->{11},7->{11},8->{5,6,7,8} ,9->{12,29},10->{13,14,15,16},11->{9,10},12->{},13->{17,18,19},14->{20,21},15->{22},16->{22},17->{24,25,26} ,18->{24,25,26},19->{24,25,26},20->{13,14},21->{20,21},22->{23},23->{27},24->{28},25->{28},26->{28},27->{13 ,14,15,16},28->{9,10},29->{}] + 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] | +- p:[2,3,4] c: [4] | | | `- p:[2,3] c: [3] | | | `- p:[2] c: [2] | +- p:[8] c: [8] | `- p:[10,28,24,17,13,20,14,27,23,22,15,16,21,18,19,25,26] c: [28] | +- p:[15,27,23,22,16] c: [27] | `- p:[14,20,21] c: [21] | `- p:[14,20] c: [20] * Step 6: SizeAbstraction MAYBE + Considered Problem: (Rules: 0. 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) -> f13(A,0,0,2*A,4*A,3 + 4*A,4 + 4*A,A,C1,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [1 >= A*B1 && A*B1 + B1 >= 2 && C1 >= B1 && 1 >= A*D1 && A*D1 + D1 >= 2 && D1 >= C1] (1,1) 1. f13(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) -> f24(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) [A + -1*H >= 0 && -1*A + H >= 0 && -1*C >= 0 && C >= 0 && J >= 1 + D] (?,1) 2. f13(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) -> f13(A,1 + B + -2*C1 + C1^2,C,D,E,F,G,H,I,1 + J,C1,1 + -1*C1,1 + -2*C1 + C1^2,N,O,P,Q,R,S,T,U,V,W,X,Y,Z[A + -1*H >= 0 && -1*A + H >= 0 && -1*C >= 0 && C >= 0 && 0 >= C1 && D >= J] (?,1) ,A1) 3. f13(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) -> f13(A,1 + B + -2*C1 + C1^2,C,D,E,F,G,H,I,1 + J,C1,1 + -1*C1,1 + -2*C1 + C1^2,N,O,P,Q,R,S,T,U,V,W,X,Y,Z[A + -1*H >= 0 && -1*A + H >= 0 && -1*C >= 0 && C >= 0 && C1 >= 2 && D >= J] (?,1) ,A1) 4. f13(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) -> f13(A,B,C,D,E,F,G,H,I,1 + J,1,0,0,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [A + -1*H >= 0 && -1*A + H >= 0 && -1*C >= 0 && C >= 0 && D >= J] (?,1) 5. f24(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) -> f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,0,Q,R,S,T,U,V,W,X,Y,Z,A1) [A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1*C >= 0 && C >= 0 && J >= 1 + A && P = 0] (?,1) 6. f24(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) -> f31(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) [A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1*C >= 0 && C >= 0 && P >= 1 && J >= 1 + A] (?,1) 7. f24(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) -> f31(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) [A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1*C >= 0 && C >= 0 && 0 >= 1 + P && J >= 1 + A] (?,1) 8. f24(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) -> f24(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) [A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1*C >= 0 && C >= 0 && A >= J] (?,1) 9. f37(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) -> f118(A,B,C*E,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*A + J >= 0 && O >= 1 + N] 10. f37(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) -> f40(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) [-1 + -1*H + J >= 0 && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*A + J >= 0 && N >= O] (?,1) 11. f31(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) -> f37(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) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1*C >= 0 && C >= 0 && -1 + -1*A + J >= 0 && J >= 1 + A] 12. f118(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) -> 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) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1 + -1*N + O >= 0 && -1 + -1*A + J >= 0 && J >= 1 + A] 13. f40(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) -> f71(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) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && Q >= 1] 14. f40(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) -> f64(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,0,Q,R,S,T,U,V,W,X,Y,Z,A1) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && 0 >= Q && P = 0] 15. f40(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) -> f44(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) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && P >= 1 && 0 >= Q] 16. f40(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) -> f44(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) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && 0 >= 1 + P && 0 >= Q] 17. f71(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) -> f86(A,B,C,D,E,F,G,H,I,J,K,C1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,B1^2,A1) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1 + Q >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && B1 >= 1 && J >= 1 + D] 18. f71(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) -> f86(A,B,C,D,E,F,G,H,I,J,K,C1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,B1^2,A1) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1 + Q >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && 0 >= 1 + B1 && J >= 1 + D] 19. f71(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) -> f86(A,B,C,D,E,F,G,H,I,J,K,C1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,0,A1) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1 + Q >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && J >= 1 + D] 20. f64(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) -> f40(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,1 + Q,R,S,T,U,V,W,X,Y,Z,A1) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1*Q >= 0 && P + -1*Q >= 0 && -1*P + -1*Q >= 0 && -1*P >= 0 && P >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && J >= 1 + E] 21. f64(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) -> f64(A,B,C,D,E,F,G,H,I,2 + J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1*Q >= 0 && P + -1*Q >= 0 && -1*P + -1*Q >= 0 && -1*P >= 0 && P >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && E >= J] 22. f44(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) -> f50(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) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1*Q >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && J >= 1 + A] 23. f50(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) -> f57(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,D + Q) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1*Q >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && J >= 1 + A] 24. f86(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) -> f91(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,L^2,V,W,X,Y,Z,A1) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1 + Q >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && L >= 1] 25. f86(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) -> f91(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,L^2,V,W,X,Y,Z,A1) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1 + Q >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && 0 >= 1 + L] 26. f86(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) -> f91(A,B,C,D,E,F,G,H,I,J,K,0,M,N,O,P,Q,R,S,T,0,V,W,X,Y,Z,A1) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1 + Q >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && L = 0] 27. f57(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) -> f40(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,1 + Q,R,S,T,U,V,W,X,Y,Z,A1) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1*A1 + D >= 0 && -1 + -1*A1 + J >= 0 && -1*Q >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && J >= 1 + A] 28. f91(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) -> f37(A,B,B + C,D,E,F,G,H,I,J,K,L,M,N,1 + O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [-1 + -1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1*A + H >= 0 && -1 + -1*D + J >= 0 && -1 + Q >= 0 && N + -1*O >= 0 && -1 + -1*A + J >= 0 && J >= 1 + A] 29. f118(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) -> exitus616(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) True (?,1) Signature: {(exitus616,27) ;(f1,27) ;(f118,27) ;(f13,27) ;(f2,27) ;(f24,27) ;(f31,27) ;(f37,27) ;(f40,27) ;(f44,27) ;(f50,27) ;(f57,27) ;(f64,27) ;(f71,27) ;(f86,27) ;(f91,27)} Flow Graph: [0->{1,2,3,4},1->{5,6,7,8},2->{1,2,3,4},3->{1,2,3,4},4->{1,2,3,4},5->{9,10},6->{11},7->{11},8->{5,6,7,8} ,9->{12,29},10->{13,14,15,16},11->{9,10},12->{},13->{17,18,19},14->{20,21},15->{22},16->{22},17->{24,25,26} ,18->{24,25,26},19->{24,25,26},20->{13,14},21->{20,21},22->{23},23->{27},24->{28},25->{28},26->{28},27->{13 ,14,15,16},28->{9,10},29->{}] ,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] | +- p:[2,3,4] c: [4] | | | `- p:[2,3] c: [3] | | | `- p:[2] c: [2] | +- p:[8] c: [8] | `- p:[10,28,24,17,13,20,14,27,23,22,15,16,21,18,19,25,26] c: [28] | +- p:[15,27,23,22,16] c: [27] | `- p:[14,20,21] c: [21] | `- p:[14,20] c: [20]) + Applied Processor: SizeAbstraction UseCFG Minimize + Details: () * Step 7: FlowAbstraction MAYBE + Considered Problem: Program: Domain: [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 ,0.0 ,0.0.0 ,0.0.0.0 ,0.1 ,0.2 ,0.2.0 ,0.2.1 ,0.2.1.0] f2 ~> f13 [A <= A, B <= 0*K, C <= 0*K, D <= 2*A, E <= 4*A, F <= 3*K + 4*A, G <= 4*K + 4*A, H <= A, I <= unknown, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1] f13 ~> f24 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1] f13 ~> f13 [A <= A, B <= unknown, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= K + J, K <= unknown, L <= unknown, M <= unknown, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1] f13 ~> f13 [A <= A, B <= unknown, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= K + J, K <= unknown, L <= unknown, M <= unknown, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1] f13 ~> f13 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= K + J, K <= K, L <= 0*K, M <= 0*K, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1] f24 ~> f37 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= 0*K, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1] f24 ~> f31 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1] f24 ~> f31 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1] f24 ~> f24 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= K + J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1] f37 ~> f118 [A <= A, B <= B, C <= unknown, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1] f37 ~> f40 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1] f31 ~> f37 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1] f118 ~> f1 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1] f40 ~> f71 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1] f40 ~> f64 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= 0*K, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1] f40 ~> f44 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1] f40 ~> f44 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1] f71 ~> f86 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= unknown, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= unknown, A1 <= A1] f71 ~> f86 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= unknown, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= unknown, A1 <= A1] f71 ~> f86 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= unknown, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= 0*K, A1 <= A1] f64 ~> f40 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= K + Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1] f64 ~> f64 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= 2*K + J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1] f44 ~> f50 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1] f50 ~> f57 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= D + Q] f86 ~> f91 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= unknown, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1] f86 ~> f91 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= unknown, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1] f86 ~> f91 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= 0*K, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= 0*K, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1] f57 ~> f40 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= K + Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1] f91 ~> f37 [A <= A, B <= B, C <= B + C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= K + O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1] f118 ~> exitus616 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1] + Loop: [0.0 <= K + D + J] f13 ~> f13 [A <= A, B <= unknown, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= K + J, K <= unknown, L <= unknown, M <= unknown, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1] f13 ~> f13 [A <= A, B <= unknown, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= K + J, K <= unknown, L <= unknown, M <= unknown, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1] f13 ~> f13 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= K + J, K <= K, L <= 0*K, M <= 0*K, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1] + Loop: [0.0.0 <= K + D + J] f13 ~> f13 [A <= A, B <= unknown, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= K + J, K <= unknown, L <= unknown, M <= unknown, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1] f13 ~> f13 [A <= A, B <= unknown, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= K + J, K <= unknown, L <= unknown, M <= unknown, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1] + Loop: [0.0.0.0 <= K + D + J] f13 ~> f13 [A <= A, B <= unknown, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= K + J, K <= unknown, L <= unknown, M <= unknown, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1] + Loop: [0.1 <= K + A + J] f24 ~> f24 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= K + J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1] + Loop: [0.2 <= K + N + O] f37 ~> f40 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1] f91 ~> f37 [A <= A, B <= B, C <= B + C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= K + O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1] f86 ~> f91 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= unknown, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1] f71 ~> f86 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= unknown, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= unknown, A1 <= A1] f40 ~> f71 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1] f64 ~> f40 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= K + Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1] f40 ~> f64 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= 0*K, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1] f57 ~> f40 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= K + Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1] f50 ~> f57 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= D + Q] f44 ~> f50 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1] f40 ~> f44 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1] f40 ~> f44 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1] f64 ~> f64 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= 2*K + J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1] f71 ~> f86 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= unknown, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= unknown, A1 <= A1] f71 ~> f86 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= unknown, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= 0*K, A1 <= A1] f86 ~> f91 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= unknown, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1] f86 ~> f91 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= 0*K, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= 0*K, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1] + Loop: [0.2.0 <= K + Q] f40 ~> f44 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1] f57 ~> f40 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= K + Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1] f50 ~> f57 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= D + Q] f44 ~> f50 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1] f40 ~> f44 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1] + Loop: [0.2.1 <= 2*E + H + J] f40 ~> f64 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= 0*K, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1] f64 ~> f40 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= K + Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1] f64 ~> f64 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= 2*K + J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1] + Loop: [0.2.1.0 <= K + Q] f40 ~> f64 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= 0*K, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1] f64 ~> f40 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= K + Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1] + Applied Processor: FlowAbstraction + Details: () * Step 8: LareProcessor MAYBE + Considered Problem: Program: Domain: [tick ,huge ,K ,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 ,0.0 ,0.0.0 ,0.0.0.0 ,0.1 ,0.2 ,0.2.0 ,0.2.1 ,0.2.1.0] f2 ~> f13 [A ~=> H ,K ~=> B ,K ~=> C ,huge ~=> I ,A ~*> D ,A ~*> E ,A ~*> F ,A ~*> G ,K ~*> F ,K ~*> G] f13 ~> f24 [] f13 ~> f13 [huge ~=> B,huge ~=> K,huge ~=> L,huge ~=> M,J ~+> J,K ~+> J] f13 ~> f13 [huge ~=> B,huge ~=> K,huge ~=> L,huge ~=> M,J ~+> J,K ~+> J] f13 ~> f13 [K ~=> K,K ~=> L,K ~=> M,J ~+> J,K ~+> J] f24 ~> f37 [K ~=> P] f24 ~> f31 [] f24 ~> f31 [] f24 ~> f24 [J ~+> J,K ~+> J] f37 ~> f118 [huge ~=> C] f37 ~> f40 [] f31 ~> f37 [] f118 ~> f1 [] f40 ~> f71 [] f40 ~> f64 [K ~=> P] f40 ~> f44 [] f40 ~> f44 [] f71 ~> f86 [huge ~=> L,huge ~=> Z] f71 ~> f86 [huge ~=> L,huge ~=> Z] f71 ~> f86 [K ~=> Z,huge ~=> L] f64 ~> f40 [Q ~+> Q,K ~+> Q] f64 ~> f64 [J ~+> J,K ~*> J] f44 ~> f50 [] f50 ~> f57 [D ~+> A1,Q ~+> A1] f86 ~> f91 [huge ~=> U] f86 ~> f91 [huge ~=> U] f86 ~> f91 [K ~=> L,K ~=> U] f57 ~> f40 [Q ~+> Q,K ~+> Q] f91 ~> f37 [B ~+> C,C ~+> C,O ~+> O,K ~+> O] f118 ~> exitus616 [] + Loop: [D ~+> 0.0,J ~+> 0.0,K ~+> 0.0] f13 ~> f13 [huge ~=> B,huge ~=> K,huge ~=> L,huge ~=> M,J ~+> J,K ~+> J] f13 ~> f13 [huge ~=> B,huge ~=> K,huge ~=> L,huge ~=> M,J ~+> J,K ~+> J] f13 ~> f13 [K ~=> K,K ~=> L,K ~=> M,J ~+> J,K ~+> J] + Loop: [D ~+> 0.0.0,J ~+> 0.0.0,K ~+> 0.0.0] f13 ~> f13 [huge ~=> B,huge ~=> K,huge ~=> L,huge ~=> M,J ~+> J,K ~+> J] f13 ~> f13 [huge ~=> B,huge ~=> K,huge ~=> L,huge ~=> M,J ~+> J,K ~+> J] + Loop: [D ~+> 0.0.0.0,J ~+> 0.0.0.0,K ~+> 0.0.0.0] f13 ~> f13 [huge ~=> B,huge ~=> K,huge ~=> L,huge ~=> M,J ~+> J,K ~+> J] + Loop: [A ~+> 0.1,J ~+> 0.1,K ~+> 0.1] f24 ~> f24 [J ~+> J,K ~+> J] + Loop: [N ~+> 0.2,O ~+> 0.2,K ~+> 0.2] f37 ~> f40 [] f91 ~> f37 [B ~+> C,C ~+> C,O ~+> O,K ~+> O] f86 ~> f91 [huge ~=> U] f71 ~> f86 [huge ~=> L,huge ~=> Z] f40 ~> f71 [] f64 ~> f40 [Q ~+> Q,K ~+> Q] f40 ~> f64 [K ~=> P] f57 ~> f40 [Q ~+> Q,K ~+> Q] f50 ~> f57 [D ~+> A1,Q ~+> A1] f44 ~> f50 [] f40 ~> f44 [] f40 ~> f44 [] f64 ~> f64 [J ~+> J,K ~*> J] f71 ~> f86 [huge ~=> L,huge ~=> Z] f71 ~> f86 [K ~=> Z,huge ~=> L] f86 ~> f91 [huge ~=> U] f86 ~> f91 [K ~=> L,K ~=> U] + Loop: [Q ~+> 0.2.0,K ~+> 0.2.0] f40 ~> f44 [] f57 ~> f40 [Q ~+> Q,K ~+> Q] f50 ~> f57 [D ~+> A1,Q ~+> A1] f44 ~> f50 [] f40 ~> f44 [] + Loop: [H ~+> 0.2.1,J ~+> 0.2.1,E ~*> 0.2.1] f40 ~> f64 [K ~=> P] f64 ~> f40 [Q ~+> Q,K ~+> Q] f64 ~> f64 [J ~+> J,K ~*> J] + Loop: [Q ~+> 0.2.1.0,K ~+> 0.2.1.0] f40 ~> f64 [K ~=> P] f64 ~> f40 [Q ~+> Q,K ~+> Q] + Applied Processor: LareProcessor + Details: f2 ~> exitus616 [A ~=> H ,K ~=> B ,K ~=> K ,K ~=> L ,K ~=> M ,K ~=> P ,K ~=> U ,K ~=> Z ,huge ~=> B ,huge ~=> C ,huge ~=> I ,huge ~=> K ,huge ~=> L ,huge ~=> M ,huge ~=> U ,huge ~=> Z ,A ~+> 0.1 ,A ~+> 0.2.1 ,A ~+> tick ,J ~+> J ,J ~+> 0.0 ,J ~+> 0.0.0 ,J ~+> 0.0.0.0 ,J ~+> 0.1 ,J ~+> 0.2.1 ,J ~+> tick ,N ~+> 0.2 ,N ~+> tick ,O ~+> O ,O ~+> 0.2 ,O ~+> tick ,Q ~+> A1 ,Q ~+> Q ,Q ~+> 0.2.0 ,Q ~+> 0.2.1.0 ,Q ~+> tick ,tick ~+> tick ,K ~+> A1 ,K ~+> J ,K ~+> O ,K ~+> Q ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> 0.0.0.0 ,K ~+> 0.1 ,K ~+> 0.2 ,K ~+> 0.2.0 ,K ~+> 0.2.1 ,K ~+> 0.2.1.0 ,K ~+> tick ,A ~*> A1 ,A ~*> D ,A ~*> E ,A ~*> F ,A ~*> G ,A ~*> J ,A ~*> Q ,A ~*> 0.0 ,A ~*> 0.0.0 ,A ~*> 0.0.0.0 ,A ~*> 0.1 ,A ~*> 0.2.0 ,A ~*> 0.2.1 ,A ~*> 0.2.1.0 ,A ~*> tick ,J ~*> A1 ,J ~*> J ,J ~*> Q ,J ~*> 0.0.0 ,J ~*> 0.0.0.0 ,J ~*> 0.1 ,J ~*> 0.2.0 ,J ~*> 0.2.1 ,J ~*> 0.2.1.0 ,J ~*> tick ,N ~*> A1 ,N ~*> J ,N ~*> O ,N ~*> Q ,N ~*> 0.2.0 ,N ~*> 0.2.1 ,N ~*> 0.2.1.0 ,N ~*> tick ,O ~*> A1 ,O ~*> J ,O ~*> O ,O ~*> Q ,O ~*> 0.2.0 ,O ~*> 0.2.1 ,O ~*> 0.2.1.0 ,O ~*> tick ,Q ~*> A1 ,Q ~*> Q ,Q ~*> 0.2.0 ,Q ~*> 0.2.1.0 ,Q ~*> tick ,K ~*> A1 ,K ~*> F ,K ~*> G ,K ~*> J ,K ~*> O ,K ~*> Q ,K ~*> 0.0.0 ,K ~*> 0.0.0.0 ,K ~*> 0.1 ,K ~*> 0.2.0 ,K ~*> 0.2.1 ,K ~*> 0.2.1.0 ,K ~*> tick ,A ~^> A1 ,A ~^> J ,A ~^> Q ,A ~^> 0.0.0 ,A ~^> 0.0.0.0 ,A ~^> 0.1 ,A ~^> 0.2.0 ,A ~^> 0.2.1 ,A ~^> 0.2.1.0 ,A ~^> tick ,J ~^> A1 ,J ~^> J ,J ~^> Q ,J ~^> 0.0.0 ,J ~^> 0.0.0.0 ,J ~^> 0.1 ,J ~^> 0.2.0 ,J ~^> 0.2.1 ,J ~^> 0.2.1.0 ,J ~^> tick ,N ~^> A1 ,N ~^> J ,N ~^> Q ,N ~^> 0.2.0 ,N ~^> 0.2.1 ,N ~^> 0.2.1.0 ,N ~^> tick ,O ~^> A1 ,O ~^> J ,O ~^> Q ,O ~^> 0.2.0 ,O ~^> 0.2.1 ,O ~^> 0.2.1.0 ,O ~^> tick ,K ~^> A1 ,K ~^> J ,K ~^> Q ,K ~^> 0.0.0 ,K ~^> 0.0.0.0 ,K ~^> 0.1 ,K ~^> 0.2.0 ,K ~^> 0.2.1 ,K ~^> 0.2.1.0 ,K ~^> tick] f2 ~> f1 [A ~=> H ,K ~=> B ,K ~=> K ,K ~=> L ,K ~=> M ,K ~=> P ,K ~=> U ,K ~=> Z ,huge ~=> B ,huge ~=> C ,huge ~=> I ,huge ~=> K ,huge ~=> L ,huge ~=> M ,huge ~=> U ,huge ~=> Z ,A ~+> 0.1 ,A ~+> 0.2.1 ,A ~+> tick ,J ~+> J ,J ~+> 0.0 ,J ~+> 0.0.0 ,J ~+> 0.0.0.0 ,J ~+> 0.1 ,J ~+> 0.2.1 ,J ~+> tick ,N ~+> 0.2 ,N ~+> tick ,O ~+> O ,O ~+> 0.2 ,O ~+> tick ,Q ~+> A1 ,Q ~+> Q ,Q ~+> 0.2.0 ,Q ~+> 0.2.1.0 ,Q ~+> tick ,tick ~+> tick ,K ~+> A1 ,K ~+> J ,K ~+> O ,K ~+> Q ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> 0.0.0.0 ,K ~+> 0.1 ,K ~+> 0.2 ,K ~+> 0.2.0 ,K ~+> 0.2.1 ,K ~+> 0.2.1.0 ,K ~+> tick ,A ~*> A1 ,A ~*> D ,A ~*> E ,A ~*> F ,A ~*> G ,A ~*> J ,A ~*> Q ,A ~*> 0.0 ,A ~*> 0.0.0 ,A ~*> 0.0.0.0 ,A ~*> 0.1 ,A ~*> 0.2.0 ,A ~*> 0.2.1 ,A ~*> 0.2.1.0 ,A ~*> tick ,J ~*> A1 ,J ~*> J ,J ~*> Q ,J ~*> 0.0.0 ,J ~*> 0.0.0.0 ,J ~*> 0.1 ,J ~*> 0.2.0 ,J ~*> 0.2.1 ,J ~*> 0.2.1.0 ,J ~*> tick ,N ~*> A1 ,N ~*> J ,N ~*> O ,N ~*> Q ,N ~*> 0.2.0 ,N ~*> 0.2.1 ,N ~*> 0.2.1.0 ,N ~*> tick ,O ~*> A1 ,O ~*> J ,O ~*> O ,O ~*> Q ,O ~*> 0.2.0 ,O ~*> 0.2.1 ,O ~*> 0.2.1.0 ,O ~*> tick ,Q ~*> A1 ,Q ~*> Q ,Q ~*> 0.2.0 ,Q ~*> 0.2.1.0 ,Q ~*> tick ,K ~*> A1 ,K ~*> F ,K ~*> G ,K ~*> J ,K ~*> O ,K ~*> Q ,K ~*> 0.0.0 ,K ~*> 0.0.0.0 ,K ~*> 0.1 ,K ~*> 0.2.0 ,K ~*> 0.2.1 ,K ~*> 0.2.1.0 ,K ~*> tick ,A ~^> A1 ,A ~^> J ,A ~^> Q ,A ~^> 0.0.0 ,A ~^> 0.0.0.0 ,A ~^> 0.1 ,A ~^> 0.2.0 ,A ~^> 0.2.1 ,A ~^> 0.2.1.0 ,A ~^> tick ,J ~^> A1 ,J ~^> J ,J ~^> Q ,J ~^> 0.0.0 ,J ~^> 0.0.0.0 ,J ~^> 0.1 ,J ~^> 0.2.0 ,J ~^> 0.2.1 ,J ~^> 0.2.1.0 ,J ~^> tick ,N ~^> A1 ,N ~^> J ,N ~^> Q ,N ~^> 0.2.0 ,N ~^> 0.2.1 ,N ~^> 0.2.1.0 ,N ~^> tick ,O ~^> A1 ,O ~^> J ,O ~^> Q ,O ~^> 0.2.0 ,O ~^> 0.2.1 ,O ~^> 0.2.1.0 ,O ~^> tick ,K ~^> A1 ,K ~^> J ,K ~^> Q ,K ~^> 0.0.0 ,K ~^> 0.0.0.0 ,K ~^> 0.1 ,K ~^> 0.2.0 ,K ~^> 0.2.1 ,K ~^> 0.2.1.0 ,K ~^> tick] + f13> [K ~=> K ,K ~=> L ,K ~=> M ,huge ~=> B ,huge ~=> K ,huge ~=> L ,huge ~=> M ,D ~+> 0.0 ,D ~+> 0.0.0 ,D ~+> 0.0.0.0 ,D ~+> tick ,J ~+> J ,J ~+> 0.0 ,J ~+> 0.0.0 ,J ~+> 0.0.0.0 ,J ~+> tick ,tick ~+> tick ,K ~+> J ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> 0.0.0.0 ,K ~+> tick ,D ~*> J ,D ~*> 0.0.0 ,D ~*> 0.0.0.0 ,D ~*> tick ,J ~*> J ,J ~*> 0.0.0 ,J ~*> 0.0.0.0 ,J ~*> tick ,K ~*> J ,K ~*> 0.0.0 ,K ~*> 0.0.0.0 ,K ~*> tick ,D ~^> J ,D ~^> 0.0.0 ,D ~^> 0.0.0.0 ,D ~^> tick ,J ~^> J ,J ~^> 0.0.0 ,J ~^> 0.0.0.0 ,J ~^> tick ,K ~^> J ,K ~^> 0.0.0 ,K ~^> 0.0.0.0 ,K ~^> tick] + f13> [huge ~=> B ,huge ~=> K ,huge ~=> L ,huge ~=> M ,D ~+> 0.0.0 ,D ~+> 0.0.0.0 ,D ~+> tick ,J ~+> J ,J ~+> 0.0.0 ,J ~+> 0.0.0.0 ,J ~+> tick ,tick ~+> tick ,K ~+> J ,K ~+> 0.0.0 ,K ~+> 0.0.0.0 ,K ~+> tick ,D ~*> J ,D ~*> 0.0.0.0 ,D ~*> tick ,J ~*> J ,J ~*> 0.0.0.0 ,J ~*> tick ,K ~*> J ,K ~*> 0.0.0.0 ,K ~*> tick ,D ~^> J ,J ~^> J ,K ~^> J] + f13> [huge ~=> B ,huge ~=> K ,huge ~=> L ,huge ~=> M ,D ~+> 0.0.0.0 ,D ~+> tick ,J ~+> J ,J ~+> 0.0.0.0 ,J ~+> tick ,tick ~+> tick ,K ~+> J ,K ~+> 0.0.0.0 ,K ~+> tick ,D ~*> J ,J ~*> J ,K ~*> J] + f24> [A ~+> 0.1 ,A ~+> tick ,J ~+> J ,J ~+> 0.1 ,J ~+> tick ,tick ~+> tick ,K ~+> J ,K ~+> 0.1 ,K ~+> tick ,A ~*> J ,J ~*> J ,K ~*> J] + f37> [K ~=> L ,K ~=> P ,K ~=> U ,K ~=> Z ,huge ~=> L ,huge ~=> U ,huge ~=> Z ,B ~+> C ,C ~+> C ,D ~+> A1 ,H ~+> 0.2.1 ,H ~+> tick ,J ~+> J ,J ~+> 0.2.1 ,J ~+> tick ,N ~+> 0.2 ,N ~+> tick ,O ~+> O ,O ~+> 0.2 ,O ~+> tick ,Q ~+> A1 ,Q ~+> Q ,Q ~+> 0.2.0 ,Q ~+> 0.2.1.0 ,Q ~+> tick ,tick ~+> tick ,K ~+> A1 ,K ~+> O ,K ~+> Q ,K ~+> 0.2 ,K ~+> 0.2.0 ,K ~+> 0.2.1.0 ,K ~+> tick ,B ~*> C ,E ~*> A1 ,E ~*> J ,E ~*> Q ,E ~*> 0.2.0 ,E ~*> 0.2.1 ,E ~*> 0.2.1.0 ,E ~*> tick ,H ~*> A1 ,H ~*> J ,H ~*> Q ,H ~*> 0.2.0 ,H ~*> 0.2.1 ,H ~*> 0.2.1.0 ,H ~*> tick ,J ~*> A1 ,J ~*> J ,J ~*> Q ,J ~*> 0.2.0 ,J ~*> 0.2.1 ,J ~*> 0.2.1.0 ,J ~*> tick ,N ~*> A1 ,N ~*> C ,N ~*> J ,N ~*> O ,N ~*> Q ,N ~*> 0.2.0 ,N ~*> 0.2.1 ,N ~*> 0.2.1.0 ,N ~*> tick ,O ~*> A1 ,O ~*> C ,O ~*> J ,O ~*> O ,O ~*> Q ,O ~*> 0.2.0 ,O ~*> 0.2.1 ,O ~*> 0.2.1.0 ,O ~*> tick ,Q ~*> A1 ,Q ~*> Q ,Q ~*> 0.2.0 ,Q ~*> 0.2.1.0 ,Q ~*> tick ,K ~*> A1 ,K ~*> C ,K ~*> J ,K ~*> O ,K ~*> Q ,K ~*> 0.2.0 ,K ~*> 0.2.1 ,K ~*> 0.2.1.0 ,K ~*> tick ,E ~^> A1 ,E ~^> Q ,E ~^> 0.2.0 ,E ~^> 0.2.1.0 ,E ~^> tick ,H ~^> A1 ,H ~^> Q ,H ~^> 0.2.0 ,H ~^> 0.2.1.0 ,H ~^> tick ,J ~^> A1 ,J ~^> Q ,J ~^> 0.2.0 ,J ~^> 0.2.1.0 ,J ~^> tick ,N ~^> A1 ,N ~^> J ,N ~^> Q ,N ~^> 0.2.0 ,N ~^> 0.2.1 ,N ~^> 0.2.1.0 ,N ~^> tick ,O ~^> A1 ,O ~^> J ,O ~^> Q ,O ~^> 0.2.0 ,O ~^> 0.2.1 ,O ~^> 0.2.1.0 ,O ~^> tick ,K ~^> A1 ,K ~^> J ,K ~^> Q ,K ~^> 0.2.0 ,K ~^> 0.2.1 ,K ~^> 0.2.1.0 ,K ~^> tick] + f40> [D ~+> A1 ,Q ~+> A1 ,Q ~+> Q ,Q ~+> 0.2.0 ,Q ~+> tick ,tick ~+> tick ,K ~+> A1 ,K ~+> Q ,K ~+> 0.2.0 ,K ~+> tick ,Q ~*> Q ,K ~*> Q] + f40> [K ~=> P ,H ~+> 0.2.1 ,H ~+> tick ,J ~+> J ,J ~+> 0.2.1 ,J ~+> tick ,Q ~+> Q ,Q ~+> 0.2.1.0 ,Q ~+> tick ,tick ~+> tick ,K ~+> Q ,K ~+> 0.2.1.0 ,K ~+> tick ,E ~*> J ,E ~*> Q ,E ~*> 0.2.1 ,E ~*> 0.2.1.0 ,E ~*> tick ,H ~*> J ,H ~*> Q ,H ~*> 0.2.1.0 ,H ~*> tick ,J ~*> J ,J ~*> Q ,J ~*> 0.2.1.0 ,J ~*> tick ,Q ~*> Q ,Q ~*> 0.2.1.0 ,Q ~*> tick ,K ~*> J ,K ~*> Q ,K ~*> 0.2.1.0 ,K ~*> tick ,E ~^> Q ,E ~^> 0.2.1.0 ,E ~^> tick ,H ~^> Q ,H ~^> 0.2.1.0 ,H ~^> tick ,J ~^> Q ,J ~^> 0.2.1.0 ,J ~^> tick] + f64> [K ~=> P ,Q ~+> Q ,Q ~+> 0.2.1.0 ,Q ~+> tick ,tick ~+> tick ,K ~+> Q ,K ~+> 0.2.1.0 ,K ~+> tick ,Q ~*> Q ,K ~*> Q] f40> [K ~=> P ,Q ~+> Q ,Q ~+> 0.2.1.0 ,Q ~+> tick ,tick ~+> tick ,K ~+> Q ,K ~+> 0.2.1.0 ,K ~+> tick ,Q ~*> Q ,K ~*> Q] f64> [K ~=> P ,Q ~+> Q ,Q ~+> 0.2.1.0 ,Q ~+> tick ,tick ~+> tick ,K ~+> Q ,K ~+> 0.2.1.0 ,K ~+> tick ,Q ~*> Q ,K ~*> Q] f40> [K ~=> P ,Q ~+> Q ,Q ~+> 0.2.1.0 ,Q ~+> tick ,tick ~+> tick ,K ~+> Q ,K ~+> 0.2.1.0 ,K ~+> tick ,Q ~*> Q ,K ~*> Q] YES(?,PRIMREC)