MAYBE * Step 1: ArgumentFilter MAYBE + Considered Problem: Rules: 0. 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,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f20(D,Y1,Z1,D,0,W1,A2,B2,C2,D2,E2,C,C,C,X1,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1 [A >= B && A >= 0 && W1 >= 2 && 0 >= 1 + C && X1 >= W1 && D >= W1 && E = 0] (?,1) ,R1,S1,T1,U1,V1) ,N1,O1,P1,Q1,R1,S1,T1,U1,V1) 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,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f20(D,Y1,Z1,D,0,W1,A2,B2,C2,D2,E2,C,C,C,X1,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1 [A >= B && A >= 0 && W1 >= 2 && C >= 1 && X1 >= W1 && D >= W1 && E = 0] (?,1) ,R1,S1,T1,U1,V1) ,N1,O1,P1,Q1,R1,S1,T1,U1,V1) 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,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f13(1 + A,B,K,D,E,F,G,H,I,K,W1,L,M,N,O,Y1,A,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1 [B >= 1 + A && A >= 0] (?,1) ,R1,S1,T1,U1,V1) ,O1,P1,Q1,R1,S1,T1,U1,V1) 3. f16(A,B,C,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,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f20(A,B,C,D,1,W1,G,H,I,J,K,Y1,Y1,N,O,P,Q,Z1,1 + D,A2,D,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1 [A >= 0 && W1 >= 2 && 0 >= 1 + N && B2 >= W1 && 0 >= 1 + Y1 && E = 1] (?,1) ,R1,S1,T1,U1,V1) ,N1,O1,P1,Q1,R1,S1,T1,U1,V1) 4. f16(A,B,C,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,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f20(A,B,C,D,1,W1,G,H,I,J,K,Y1,Y1,N,O,P,Q,Z1,1 + D,A2,D,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1 [A >= 0 && W1 >= 2 && 0 >= 1 + N && B2 >= W1 && Y1 >= 1 && E = 1] (?,1) ,R1,S1,T1,U1,V1) ,N1,O1,P1,Q1,R1,S1,T1,U1,V1) 5. f16(A,B,C,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,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f20(A,B,C,D,1,W1,G,H,I,J,K,Y1,Y1,N,O,P,Q,Z1,1 + D,A2,D,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1 [A >= 0 && W1 >= 2 && N >= 1 && B2 >= W1 && 0 >= 1 + Y1 && E = 1] (?,1) ,R1,S1,T1,U1,V1) ,N1,O1,P1,Q1,R1,S1,T1,U1,V1) 6. f16(A,B,C,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,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f20(A,B,C,D,1,W1,G,H,I,J,K,Y1,Y1,N,O,P,Q,Z1,1 + D,A2,D,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1 [A >= 0 && W1 >= 2 && N >= 1 && B2 >= W1 && Y1 >= 1 && E = 1] (?,1) ,R1,S1,T1,U1,V1) ,N1,O1,P1,Q1,R1,S1,T1,U1,V1) 7. f17(A,B,C,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,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f20(A,B,C,D,E,W1,G,H,I,J,K,Y1,Y1,N,O,P,Q,R,S,T,U,Z1,A2,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1 [U >= 0 && W1 >= 2 && 0 >= 1 + N && 0 >= 1 + Y1 && 0 >= 1 + A2] (?,1) ,R1,S1,T1,U1,V1) ,O1,P1,Q1,R1,S1,T1,U1,V1) 8. f17(A,B,C,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,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f20(A,B,C,D,E,W1,G,H,I,J,K,Y1,Y1,N,O,P,Q,R,S,T,U,Z1,A2,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1 [U >= 0 && W1 >= 2 && 0 >= 1 + N && 0 >= 1 + Y1 && A2 >= 1] (?,1) ,R1,S1,T1,U1,V1) ,O1,P1,Q1,R1,S1,T1,U1,V1) 9. f17(A,B,C,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,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f20(A,B,C,D,E,W1,G,H,I,J,K,Y1,Y1,N,O,P,Q,R,S,T,U,Z1,A2,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1 [U >= 0 && W1 >= 2 && 0 >= 1 + N && Y1 >= 1 && 0 >= 1 + A2] (?,1) ,R1,S1,T1,U1,V1) ,O1,P1,Q1,R1,S1,T1,U1,V1) 10. f17(A,B,C,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,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f20(A,B,C,D,E,W1,G,H,I,J,K,Y1,Y1,N,O,P,Q,R,S,T,U,Z1,A2,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1 [U >= 0 && W1 >= 2 && 0 >= 1 + N && Y1 >= 1 && A2 >= 1] (?,1) ,R1,S1,T1,U1,V1) ,O1,P1,Q1,R1,S1,T1,U1,V1) 11. f17(A,B,C,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,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f20(A,B,C,D,E,W1,G,H,I,J,K,Y1,Y1,N,O,P,Q,R,S,T,U,Z1,A2,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1 [U >= 0 && W1 >= 2 && N >= 1 && 0 >= 1 + Y1 && 0 >= 1 + A2] (?,1) ,R1,S1,T1,U1,V1) ,O1,P1,Q1,R1,S1,T1,U1,V1) 12. f17(A,B,C,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,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f20(A,B,C,D,E,W1,G,H,I,J,K,Y1,Y1,N,O,P,Q,R,S,T,U,Z1,A2,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1 [U >= 0 && W1 >= 2 && N >= 1 && 0 >= 1 + Y1 && A2 >= 1] (?,1) ,R1,S1,T1,U1,V1) ,O1,P1,Q1,R1,S1,T1,U1,V1) 13. f17(A,B,C,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,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f20(A,B,C,D,E,W1,G,H,I,J,K,Y1,Y1,N,O,P,Q,R,S,T,U,Z1,A2,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1 [U >= 0 && W1 >= 2 && N >= 1 && Y1 >= 1 && 0 >= 1 + A2] (?,1) ,R1,S1,T1,U1,V1) ,O1,P1,Q1,R1,S1,T1,U1,V1) 14. f17(A,B,C,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,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f20(A,B,C,D,E,W1,G,H,I,J,K,Y1,Y1,N,O,P,Q,R,S,T,U,Z1,A2,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1 [U >= 0 && W1 >= 2 && N >= 1 && Y1 >= 1 && A2 >= 1] (?,1) ,R1,S1,T1,U1,V1) ,O1,P1,Q1,R1,S1,T1,U1,V1) 15. f20(A,B,C,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,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f11(A,B,C,D,E,W1,G,H,I,J,K,L,L,L,O,P,Q,R,S,T,U,V,W,E,0,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1[E >= 0 && D >= 0 && W1 >= 2 && 0 >= 1 + L && X = E && N = 0 && Y = 0] (?,1) ,R1,S1,T1,U1,V1) ,Q1,R1,S1,T1,U1,V1) 16. f20(A,B,C,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,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f11(A,B,C,D,E,W1,G,H,I,J,K,L,L,L,O,P,Q,R,S,T,U,V,W,E,0,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1[E >= 0 && D >= 0 && W1 >= 2 && L >= 1 && X = E && N = 0 && Y = 0] (?,1) ,R1,S1,T1,U1,V1) ,Q1,R1,S1,T1,U1,V1) 17. f20(A,B,C,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,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f20(A,B,C,-1 + D,1 + E,W1,G,H,I,J,K,Y1,Y1,N,O,P,Q,Z1,S,T,U,V,W,X,Y,N,A2,1 + E,-1 + D,D1,E1,F1,G1,H1,I1 [E >= 0 && D >= 0 && W1 >= 2 && 0 >= 1 + B2 && 0 >= 1 + Y1 && 0 >= 1 + A2] (?,1) ,R1,S1,T1,U1,V1) ,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1) 18. f20(A,B,C,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,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f20(A,B,C,-1 + D,1 + E,W1,G,H,I,J,K,Y1,Y1,N,O,P,Q,Z1,S,T,U,V,W,X,Y,N,A2,1 + E,-1 + D,D1,E1,F1,G1,H1,I1 [E >= 0 && D >= 0 && W1 >= 2 && 0 >= 1 + B2 && 0 >= 1 + Y1 && A2 >= 1] (?,1) ,R1,S1,T1,U1,V1) ,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1) 19. f20(A,B,C,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,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f20(A,B,C,-1 + D,1 + E,W1,G,H,I,J,K,Y1,Y1,N,O,P,Q,Z1,S,T,U,V,W,X,Y,N,A2,1 + E,-1 + D,D1,E1,F1,G1,H1,I1 [E >= 0 && D >= 0 && W1 >= 2 && 0 >= 1 + B2 && Y1 >= 1 && 0 >= 1 + A2] (?,1) ,R1,S1,T1,U1,V1) ,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1) 20. f20(A,B,C,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,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f20(A,B,C,-1 + D,1 + E,W1,G,H,I,J,K,Y1,Y1,N,O,P,Q,Z1,S,T,U,V,W,X,Y,N,A2,1 + E,-1 + D,D1,E1,F1,G1,H1,I1 [E >= 0 && D >= 0 && W1 >= 2 && 0 >= 1 + B2 && Y1 >= 1 && A2 >= 1] (?,1) ,R1,S1,T1,U1,V1) ,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1) 21. f20(A,B,C,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,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f20(A,B,C,-1 + D,1 + E,W1,G,H,I,J,K,Y1,Y1,N,O,P,Q,Z1,S,T,U,V,W,X,Y,N,A2,1 + E,-1 + D,D1,E1,F1,G1,H1,I1 [E >= 0 && D >= 0 && W1 >= 2 && B2 >= 1 && 0 >= 1 + Y1 && 0 >= 1 + A2] (?,1) ,R1,S1,T1,U1,V1) ,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1) 22. f20(A,B,C,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,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f20(A,B,C,-1 + D,1 + E,W1,G,H,I,J,K,Y1,Y1,N,O,P,Q,Z1,S,T,U,V,W,X,Y,N,A2,1 + E,-1 + D,D1,E1,F1,G1,H1,I1 [E >= 0 && D >= 0 && W1 >= 2 && B2 >= 1 && 0 >= 1 + Y1 && A2 >= 1] (?,1) ,R1,S1,T1,U1,V1) ,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1) 23. f20(A,B,C,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,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f20(A,B,C,-1 + D,1 + E,W1,G,H,I,J,K,Y1,Y1,N,O,P,Q,Z1,S,T,U,V,W,X,Y,N,A2,1 + E,-1 + D,D1,E1,F1,G1,H1,I1 [E >= 0 && D >= 0 && W1 >= 2 && B2 >= 1 && Y1 >= 1 && 0 >= 1 + A2] (?,1) ,R1,S1,T1,U1,V1) ,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1) 24. f20(A,B,C,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,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f20(A,B,C,-1 + D,1 + E,W1,G,H,I,J,K,Y1,Y1,N,O,P,Q,Z1,S,T,U,V,W,X,Y,N,A2,1 + E,-1 + D,D1,E1,F1,G1,H1,I1 [E >= 0 && D >= 0 && W1 >= 2 && B2 >= 1 && Y1 >= 1 && A2 >= 1] (?,1) ,R1,S1,T1,U1,V1) ,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1) 25. f7(A,B,C,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,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f11(A,B,C,D,E,W1,G,H,I,J,K,Y1,Y1,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,Z1,A2,G1,H1,I1,J1,K1,L1,M1,N1,O1 [D1 >= 0 && W1 >= 2 && 0 >= 1 + N && 0 >= 1 + Y1 && 0 >= 1 + A2] (?,1) ,S1,T1,U1,V1) ,P1,Q1,R1,S1,T1,U1,V1) 26. f7(A,B,C,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,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f11(A,B,C,D,E,W1,G,H,I,J,K,Y1,Y1,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,Z1,A2,G1,H1,I1,J1,K1,L1,M1,N1,O1 [D1 >= 0 && W1 >= 2 && 0 >= 1 + N && 0 >= 1 + Y1 && A2 >= 1] (?,1) ,S1,T1,U1,V1) ,P1,Q1,R1,S1,T1,U1,V1) 27. f7(A,B,C,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,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f11(A,B,C,D,E,W1,G,H,I,J,K,Y1,Y1,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,Z1,A2,G1,H1,I1,J1,K1,L1,M1,N1,O1 [D1 >= 0 && W1 >= 2 && 0 >= 1 + N && Y1 >= 1 && 0 >= 1 + A2] (?,1) ,S1,T1,U1,V1) ,P1,Q1,R1,S1,T1,U1,V1) 28. f7(A,B,C,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,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f11(A,B,C,D,E,W1,G,H,I,J,K,Y1,Y1,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,Z1,A2,G1,H1,I1,J1,K1,L1,M1,N1,O1 [D1 >= 0 && W1 >= 2 && 0 >= 1 + N && Y1 >= 1 && A2 >= 1] (?,1) ,S1,T1,U1,V1) ,P1,Q1,R1,S1,T1,U1,V1) 29. f7(A,B,C,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,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f11(A,B,C,D,E,W1,G,H,I,J,K,Y1,Y1,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,Z1,A2,G1,H1,I1,J1,K1,L1,M1,N1,O1 [D1 >= 0 && W1 >= 2 && N >= 1 && 0 >= 1 + Y1 && 0 >= 1 + A2] (?,1) ,S1,T1,U1,V1) ,P1,Q1,R1,S1,T1,U1,V1) 30. f7(A,B,C,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,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f11(A,B,C,D,E,W1,G,H,I,J,K,Y1,Y1,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,Z1,A2,G1,H1,I1,J1,K1,L1,M1,N1,O1 [D1 >= 0 && W1 >= 2 && N >= 1 && 0 >= 1 + Y1 && A2 >= 1] (?,1) ,S1,T1,U1,V1) ,P1,Q1,R1,S1,T1,U1,V1) 31. f7(A,B,C,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,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f11(A,B,C,D,E,W1,G,H,I,J,K,Y1,Y1,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,Z1,A2,G1,H1,I1,J1,K1,L1,M1,N1,O1 [D1 >= 0 && W1 >= 2 && N >= 1 && Y1 >= 1 && 0 >= 1 + A2] (?,1) ,S1,T1,U1,V1) ,P1,Q1,R1,S1,T1,U1,V1) 32. f7(A,B,C,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,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f11(A,B,C,D,E,W1,G,H,I,J,K,Y1,Y1,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,Z1,A2,G1,H1,I1,J1,K1,L1,M1,N1,O1 [D1 >= 0 && W1 >= 2 && N >= 1 && Y1 >= 1 && A2 >= 1] (?,1) ,S1,T1,U1,V1) ,P1,Q1,R1,S1,T1,U1,V1) 33. f11(A,B,C,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,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f11(A,B,C,D,E,W1,G,H,I,J,K,Y1,Y1,N,O,P,Q,Z1,S,T,U,V,W,-1 + X,1 + Y,Z,A1,B1,C1,D1,E1,F1,N,A2,1 + Y,-1 + X[Y >= 0 && X >= 0 && W1 >= 2 && 0 >= 1 + B2 && 0 >= 1 + Y1 && 0 >= 1 + A2] (?,1) ,R1,S1,T1,U1,V1) ,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1) 34. f11(A,B,C,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,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f11(A,B,C,D,E,W1,G,H,I,J,K,Y1,Y1,N,O,P,Q,Z1,S,T,U,V,W,-1 + X,1 + Y,Z,A1,B1,C1,D1,E1,F1,N,A2,1 + Y,-1 + X[Y >= 0 && X >= 0 && W1 >= 2 && 0 >= 1 + B2 && 0 >= 1 + Y1 && A2 >= 1] (?,1) ,R1,S1,T1,U1,V1) ,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1) 35. f11(A,B,C,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,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f11(A,B,C,D,E,W1,G,H,I,J,K,Y1,Y1,N,O,P,Q,Z1,S,T,U,V,W,-1 + X,1 + Y,Z,A1,B1,C1,D1,E1,F1,N,A2,1 + Y,-1 + X[Y >= 0 && X >= 0 && W1 >= 2 && 0 >= 1 + B2 && Y1 >= 1 && 0 >= 1 + A2] (?,1) ,R1,S1,T1,U1,V1) ,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1) 36. f11(A,B,C,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,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f11(A,B,C,D,E,W1,G,H,I,J,K,Y1,Y1,N,O,P,Q,Z1,S,T,U,V,W,-1 + X,1 + Y,Z,A1,B1,C1,D1,E1,F1,N,A2,1 + Y,-1 + X[Y >= 0 && X >= 0 && W1 >= 2 && 0 >= 1 + B2 && Y1 >= 1 && A2 >= 1] (?,1) ,R1,S1,T1,U1,V1) ,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1) 37. f11(A,B,C,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,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f11(A,B,C,D,E,W1,G,H,I,J,K,Y1,Y1,N,O,P,Q,Z1,S,T,U,V,W,-1 + X,1 + Y,Z,A1,B1,C1,D1,E1,F1,N,A2,1 + Y,-1 + X[Y >= 0 && X >= 0 && W1 >= 2 && B2 >= 1 && 0 >= 1 + Y1 && 0 >= 1 + A2] (?,1) ,R1,S1,T1,U1,V1) ,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1) 38. f11(A,B,C,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,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f11(A,B,C,D,E,W1,G,H,I,J,K,Y1,Y1,N,O,P,Q,Z1,S,T,U,V,W,-1 + X,1 + Y,Z,A1,B1,C1,D1,E1,F1,N,A2,1 + Y,-1 + X[Y >= 0 && X >= 0 && W1 >= 2 && B2 >= 1 && 0 >= 1 + Y1 && A2 >= 1] (?,1) ,R1,S1,T1,U1,V1) ,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1) 39. f11(A,B,C,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,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f11(A,B,C,D,E,W1,G,H,I,J,K,Y1,Y1,N,O,P,Q,Z1,S,T,U,V,W,-1 + X,1 + Y,Z,A1,B1,C1,D1,E1,F1,N,A2,1 + Y,-1 + X[Y >= 0 && X >= 0 && W1 >= 2 && B2 >= 1 && Y1 >= 1 && 0 >= 1 + A2] (?,1) ,R1,S1,T1,U1,V1) ,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1) 40. f11(A,B,C,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,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f11(A,B,C,D,E,W1,G,H,I,J,K,Y1,Y1,N,O,P,Q,Z1,S,T,U,V,W,-1 + X,1 + Y,Z,A1,B1,C1,D1,E1,F1,N,A2,1 + Y,-1 + X[Y >= 0 && X >= 0 && W1 >= 2 && B2 >= 1 && Y1 >= 1 && A2 >= 1] (?,1) ,R1,S1,T1,U1,V1) ,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1) 41. f4(A,B,C,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,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f5(A,B,C,D,E,W1,G,H,I,J,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,0,Y1,0,Y1 [Z1 >= 1 + K1 && L1 >= 0 && W1 >= 2 && Y1 >= 1 + Z1 && 0 >= 1 + Y1 && M1 = 0] (?,1) ,S1,T1,U1,V1) ,K1,R1,S1,T1,U1,V1) 42. f4(A,B,C,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,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f5(A,B,C,D,E,W1,G,H,I,J,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,0,Y1,0,Y1 [Z1 >= 1 + K1 && L1 >= 0 && W1 >= 2 && Y1 >= 1 + Z1 && Y1 >= 1 && M1 = 0] (?,1) ,S1,T1,U1,V1) ,K1,R1,S1,T1,U1,V1) 43. f4(A,B,C,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,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f5(A,B,C,D,E,W1,G,H,I,J,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,0,Y1,0,Y1 [Z1 >= 1 + K1 && L1 >= 0 && W1 >= 2 && Z1 >= 1 + Y1 && 0 >= 1 + Y1 && M1 = 0] (?,1) ,S1,T1,U1,V1) ,K1,R1,S1,T1,U1,V1) 44. f4(A,B,C,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,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f5(A,B,C,D,E,W1,G,H,I,J,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,0,Y1,0,Y1 [Z1 >= 1 + K1 && L1 >= 0 && W1 >= 2 && Z1 >= 1 + Y1 && Y1 >= 1 && M1 = 0] (?,1) ,S1,T1,U1,V1) ,K1,R1,S1,T1,U1,V1) 45. f4(A,B,C,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,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f5(A,B,C,D,E,W1,G,H,I,J,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,0,Y1,0,Y1 [K1 >= 1 + Z1 && L1 >= 0 && W1 >= 2 && Y1 >= 1 + Z1 && 0 >= 1 + Y1 && M1 = 0] (?,1) ,S1,T1,U1,V1) ,K1,R1,S1,T1,U1,V1) 46. f4(A,B,C,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,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f5(A,B,C,D,E,W1,G,H,I,J,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,0,Y1,0,Y1 [K1 >= 1 + Z1 && L1 >= 0 && W1 >= 2 && Y1 >= 1 + Z1 && Y1 >= 1 && M1 = 0] (?,1) ,S1,T1,U1,V1) ,K1,R1,S1,T1,U1,V1) 47. f4(A,B,C,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,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f5(A,B,C,D,E,W1,G,H,I,J,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,0,Y1,0,Y1 [K1 >= 1 + Z1 && L1 >= 0 && W1 >= 2 && Z1 >= 1 + Y1 && 0 >= 1 + Y1 && M1 = 0] (?,1) ,S1,T1,U1,V1) ,K1,R1,S1,T1,U1,V1) 48. f4(A,B,C,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,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f5(A,B,C,D,E,W1,G,H,I,J,K,Y1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,0,Y1,0,Y1 [K1 >= 1 + Z1 && L1 >= 0 && W1 >= 2 && Z1 >= 1 + Y1 && Y1 >= 1 && M1 = 0] (?,1) ,S1,T1,U1,V1) ,K1,R1,S1,T1,U1,V1) 49. f4(A,B,C,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,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f22(A,B,C,D,E,W1,G,Y1,I,J,K,Z1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,E2,L1,D2,A2,B2 [L1 >= 0 && 0 >= 1 + Z1 && W1 >= 2 && M1 = K1] (?,1) ,S1,T1,U1,V1) ,C2,X1,R1,S1,T1,U1,V1) 50. f4(A,B,C,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,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f22(A,B,C,D,E,W1,G,Y1,I,J,K,Z1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,E2,L1,D2,A2,B2 [L1 >= 0 && Z1 >= 1 && W1 >= 2 && M1 = K1] (?,1) ,S1,T1,U1,V1) ,C2,X1,R1,S1,T1,U1,V1) 51. f5(A,B,C,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,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f5(A,B,C,D,E,W1,G,H,I,J,K,Y1,M,N,O,P,Q,Z1,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,0,Y1,0,Y1 [A2 >= 1 + K1 && R1 >= 0 && W1 >= 2 && Y1 >= 1 + A2 && 0 >= 1 + Y1 && M1 = 0] (?,1) ,S1,T1,U1,V1) ,K1,-1 + R1,-1 + R1,T1,U1,V1) 52. f5(A,B,C,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,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f5(A,B,C,D,E,W1,G,H,I,J,K,Y1,M,N,O,P,Q,Z1,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,0,Y1,0,Y1 [A2 >= 1 + K1 && R1 >= 0 && W1 >= 2 && Y1 >= 1 + A2 && Y1 >= 1 && M1 = 0] (?,1) ,S1,T1,U1,V1) ,K1,-1 + R1,-1 + R1,T1,U1,V1) 53. f5(A,B,C,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,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f5(A,B,C,D,E,W1,G,H,I,J,K,Y1,M,N,O,P,Q,Z1,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,0,Y1,0,Y1 [A2 >= 1 + K1 && R1 >= 0 && W1 >= 2 && A2 >= 1 + Y1 && 0 >= 1 + Y1 && M1 = 0] (?,1) ,S1,T1,U1,V1) ,K1,-1 + R1,-1 + R1,T1,U1,V1) 54. f5(A,B,C,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,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f5(A,B,C,D,E,W1,G,H,I,J,K,Y1,M,N,O,P,Q,Z1,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,0,Y1,0,Y1 [A2 >= 1 + K1 && R1 >= 0 && W1 >= 2 && A2 >= 1 + Y1 && Y1 >= 1 && M1 = 0] (?,1) ,S1,T1,U1,V1) ,K1,-1 + R1,-1 + R1,T1,U1,V1) 55. f5(A,B,C,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,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f5(A,B,C,D,E,W1,G,H,I,J,K,Y1,M,N,O,P,Q,Z1,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,0,Y1,0,Y1 [K1 >= 1 + A2 && R1 >= 0 && W1 >= 2 && Y1 >= 1 + A2 && 0 >= 1 + Y1 && M1 = 0] (?,1) ,S1,T1,U1,V1) ,K1,-1 + R1,-1 + R1,T1,U1,V1) 56. f5(A,B,C,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,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f5(A,B,C,D,E,W1,G,H,I,J,K,Y1,M,N,O,P,Q,Z1,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,0,Y1,0,Y1 [K1 >= 1 + A2 && R1 >= 0 && W1 >= 2 && Y1 >= 1 + A2 && Y1 >= 1 && M1 = 0] (?,1) ,S1,T1,U1,V1) ,K1,-1 + R1,-1 + R1,T1,U1,V1) 57. f5(A,B,C,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,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f5(A,B,C,D,E,W1,G,H,I,J,K,Y1,M,N,O,P,Q,Z1,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,0,Y1,0,Y1 [K1 >= 1 + A2 && R1 >= 0 && W1 >= 2 && A2 >= 1 + Y1 && 0 >= 1 + Y1 && M1 = 0] (?,1) ,S1,T1,U1,V1) ,K1,-1 + R1,-1 + R1,T1,U1,V1) 58. f5(A,B,C,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,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f5(A,B,C,D,E,W1,G,H,I,J,K,Y1,M,N,O,P,Q,Z1,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,0,Y1,0,Y1 [K1 >= 1 + A2 && R1 >= 0 && W1 >= 2 && A2 >= 1 + Y1 && Y1 >= 1 && M1 = 0] (?,1) ,S1,T1,U1,V1) ,K1,-1 + R1,-1 + R1,T1,U1,V1) 59. f5(A,B,C,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,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f22(A,B,C,D,E,W1,G,Y1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,D2,L1,C2,Z1,A2 [W1 >= 2 && R1 >= 0 && M1 = K1] (?,1) ,S1,T1,U1,V1) ,B2,E2,R1,S1,T1,U1,V1) 60. f21(A,B,C,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,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f13(2,Y1,Z1,D,E,Y1,G,H,Z1,Z1,A2,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1 [Y1 >= 2] (1,1) ,R1,S1,T1,U1,V1) ,O1,P1,Q1,R1,S1,W1,B2,V1) 61. f17(A,B,C,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,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f11(A,B,C,D,1 + X,W1,G,H,I,J,K,Y1,Y1,L,O,P,Q,Z1,S,T,U,V,W,X,1,Z,A1,B1,C1,X,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1[B2 >= 2 && W1 >= 2 && U >= 0 && 0 >= 1 + L && 0 >= 1 + Y1 && N = 0 && E = 1 && Y = 1] (?,1) ,R1,S1,T1,U1,V1) ,O1,P1,Q1,R1,S1,T1,U1,A2) 62. f17(A,B,C,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,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f11(A,B,C,D,1 + X,W1,G,H,I,J,K,Y1,Y1,L,O,P,Q,Z1,S,T,U,V,W,X,1,Z,A1,B1,C1,X,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1[B2 >= 2 && W1 >= 2 && U >= 0 && 0 >= 1 + L && Y1 >= 1 && N = 0 && E = 1 && Y = 1] (?,1) ,R1,S1,T1,U1,V1) ,O1,P1,Q1,R1,S1,T1,U1,A2) 63. f17(A,B,C,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,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f11(A,B,C,D,1 + X,W1,G,H,I,J,K,Y1,Y1,L,O,P,Q,Z1,S,T,U,V,W,X,1,Z,A1,B1,C1,X,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1[B2 >= 2 && W1 >= 2 && U >= 0 && L >= 1 && 0 >= 1 + Y1 && N = 0 && E = 1 && Y = 1] (?,1) ,R1,S1,T1,U1,V1) ,O1,P1,Q1,R1,S1,T1,U1,A2) 64. f17(A,B,C,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,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f11(A,B,C,D,1 + X,W1,G,H,I,J,K,Y1,Y1,L,O,P,Q,Z1,S,T,U,V,W,X,1,Z,A1,B1,C1,X,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1[B2 >= 2 && W1 >= 2 && U >= 0 && L >= 1 && Y1 >= 1 && N = 0 && E = 1 && Y = 1] (?,1) ,R1,S1,T1,U1,V1) ,O1,P1,Q1,R1,S1,T1,U1,A2) 65. f21(A,B,C,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,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f22(B2,Z1,A2,D,E,Y1,C2,D2,E2,X1,J2,0,K2,L2,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,Q2,L1 [0 >= F2 && 0 >= G2 && 0 >= H2 && 0 >= Y1 && 0 >= I2] (1,1) ,R1,S1,T1,U1,V1) ,P2,M2,N2,O2,R2,R1,S1,W1,U1,V1) 66. f7(A,B,C,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,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f5(A,B,C,D,E,W1,G,H,I,J,K,L,Y1,Z1,O,P,Q,R,S,T,U,V,W,X,1 + R1,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,L,R1,0,L,0 [A2 >= 2 && W1 >= 2 && D1 >= 0 && L >= 1 && 0 >= 1 + L && N = 0 && Y = 1] (?,1) ,S1,T1,U1,V1) ,L,L,R1,S1,T1,U1,V1) 67. f7(A,B,C,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,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f5(A,B,C,D,E,W1,G,H,I,J,K,L,Y1,Z1,O,P,Q,R,S,T,U,V,W,X,1 + R1,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,L,R1,0,L,0 [A2 >= 2 && W1 >= 2 && D1 >= 0 && L >= 1 && N = 0 && Y = 1] (?,1) ,S1,T1,U1,V1) ,L,L,R1,S1,T1,U1,V1) 68. f7(A,B,C,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,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f5(A,B,C,D,E,W1,G,H,I,J,K,L,Y1,Z1,O,P,Q,R,S,T,U,V,W,X,1 + R1,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,L,R1,0,L,0 [A2 >= 2 && W1 >= 2 && D1 >= 0 && 0 >= 1 + L && N = 0 && Y = 1] (?,1) ,S1,T1,U1,V1) ,L,L,R1,S1,T1,U1,V1) 69. f7(A,B,C,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,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f5(A,B,C,D,E,W1,G,H,I,J,K,L,Y1,Z1,O,P,Q,R,S,T,U,V,W,X,1 + R1,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,L,R1,0,L,0 [A2 >= 2 && W1 >= 2 && D1 >= 0 && 0 >= 1 + L && L >= 1 && N = 0 && Y = 1] (?,1) ,S1,T1,U1,V1) ,L,L,R1,S1,T1,U1,V1) 70. f11(A,B,C,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,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f5(A,B,C,D,E,W1,G,H,I,J,K,L,Y1,Z1,O,P,Q,R,S,T,U,V,W,X,1 + R1,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,L,R1,0,L,0 [A2 >= 2 && W1 >= 2 && X >= 0 && Y >= 0 && L >= 1 && 0 >= 1 + L && N = 0] (?,1) ,R1,S1,T1,U1,V1) ,L,L,R1,S1,T1,U1,V1) 71. f11(A,B,C,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,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f5(A,B,C,D,E,W1,G,H,I,J,K,L,Y1,Z1,O,P,Q,R,S,T,U,V,W,X,1 + R1,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,L,R1,0,L,0 [A2 >= 2 && W1 >= 2 && X >= 0 && Y >= 0 && L >= 1 && N = 0] (?,1) ,R1,S1,T1,U1,V1) ,L,L,R1,S1,T1,U1,V1) 72. f11(A,B,C,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,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f5(A,B,C,D,E,W1,G,H,I,J,K,L,Y1,Z1,O,P,Q,R,S,T,U,V,W,X,1 + R1,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,L,R1,0,L,0 [A2 >= 2 && W1 >= 2 && X >= 0 && Y >= 0 && 0 >= 1 + L && N = 0] (?,1) ,R1,S1,T1,U1,V1) ,L,L,R1,S1,T1,U1,V1) 73. f11(A,B,C,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,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f5(A,B,C,D,E,W1,G,H,I,J,K,L,Y1,Z1,O,P,Q,R,S,T,U,V,W,X,1 + R1,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,L,R1,0,L,0 [A2 >= 2 && W1 >= 2 && X >= 0 && Y >= 0 && 0 >= 1 + L && L >= 1 && N = 0] (?,1) ,R1,S1,T1,U1,V1) ,L,L,R1,S1,T1,U1,V1) Signature: {(f11,48);(f13,48);(f16,48);(f17,48);(f20,48);(f21,48);(f22,48);(f4,48);(f5,48);(f7,48)} Flow Graph: [0->{15,16,17,18,19,20,21,22,23,24},1->{15,16,17,18,19,20,21,22,23,24},2->{0,1,2},3->{15,16,17,18,19,20,21 ,22,23,24},4->{15,16,17,18,19,20,21,22,23,24},5->{15,16,17,18,19,20,21,22,23,24},6->{15,16,17,18,19,20,21,22 ,23,24},7->{15,16,17,18,19,20,21,22,23,24},8->{15,16,17,18,19,20,21,22,23,24},9->{15,16,17,18,19,20,21,22,23 ,24},10->{15,16,17,18,19,20,21,22,23,24},11->{15,16,17,18,19,20,21,22,23,24},12->{15,16,17,18,19,20,21,22,23 ,24},13->{15,16,17,18,19,20,21,22,23,24},14->{15,16,17,18,19,20,21,22,23,24},15->{33,34,35,36,37,38,39,40,70 ,71,72,73},16->{33,34,35,36,37,38,39,40,70,71,72,73},17->{15,16,17,18,19,20,21,22,23,24},18->{15,16,17,18,19 ,20,21,22,23,24},19->{15,16,17,18,19,20,21,22,23,24},20->{15,16,17,18,19,20,21,22,23,24},21->{15,16,17,18,19 ,20,21,22,23,24},22->{15,16,17,18,19,20,21,22,23,24},23->{15,16,17,18,19,20,21,22,23,24},24->{15,16,17,18,19 ,20,21,22,23,24},25->{33,34,35,36,37,38,39,40,70,71,72,73},26->{33,34,35,36,37,38,39,40,70,71,72,73},27->{33 ,34,35,36,37,38,39,40,70,71,72,73},28->{33,34,35,36,37,38,39,40,70,71,72,73},29->{33,34,35,36,37,38,39,40,70 ,71,72,73},30->{33,34,35,36,37,38,39,40,70,71,72,73},31->{33,34,35,36,37,38,39,40,70,71,72,73},32->{33,34,35 ,36,37,38,39,40,70,71,72,73},33->{33,34,35,36,37,38,39,40,70,71,72,73},34->{33,34,35,36,37,38,39,40,70,71,72 ,73},35->{33,34,35,36,37,38,39,40,70,71,72,73},36->{33,34,35,36,37,38,39,40,70,71,72,73},37->{33,34,35,36,37 ,38,39,40,70,71,72,73},38->{33,34,35,36,37,38,39,40,70,71,72,73},39->{33,34,35,36,37,38,39,40,70,71,72,73} ,40->{33,34,35,36,37,38,39,40,70,71,72,73},41->{51,52,53,54,55,56,57,58,59},42->{51,52,53,54,55,56,57,58,59} ,43->{51,52,53,54,55,56,57,58,59},44->{51,52,53,54,55,56,57,58,59},45->{51,52,53,54,55,56,57,58,59},46->{51 ,52,53,54,55,56,57,58,59},47->{51,52,53,54,55,56,57,58,59},48->{51,52,53,54,55,56,57,58,59},49->{},50->{} ,51->{51,52,53,54,55,56,57,58,59},52->{51,52,53,54,55,56,57,58,59},53->{51,52,53,54,55,56,57,58,59},54->{51 ,52,53,54,55,56,57,58,59},55->{51,52,53,54,55,56,57,58,59},56->{51,52,53,54,55,56,57,58,59},57->{51,52,53,54 ,55,56,57,58,59},58->{51,52,53,54,55,56,57,58,59},59->{},60->{0,1,2},61->{33,34,35,36,37,38,39,40,70,71,72 ,73},62->{33,34,35,36,37,38,39,40,70,71,72,73},63->{33,34,35,36,37,38,39,40,70,71,72,73},64->{33,34,35,36,37 ,38,39,40,70,71,72,73},65->{},66->{51,52,53,54,55,56,57,58,59},67->{51,52,53,54,55,56,57,58,59},68->{51,52 ,53,54,55,56,57,58,59},69->{51,52,53,54,55,56,57,58,59},70->{51,52,53,54,55,56,57,58,59},71->{51,52,53,54,55 ,56,57,58,59},72->{51,52,53,54,55,56,57,58,59},73->{51,52,53,54,55,56,57,58,59}] + Applied Processor: ArgumentFilter [5,6,7,8,9,10,12,14,15,16,17,18,19,21,22,25,26,27,28,30,31,32,33,34,35,39,40,41,42,44,45,46,47] + Details: We remove following argument positions: [5 ,6 ,7 ,8 ,9 ,10 ,12 ,14 ,15 ,16 ,17 ,18 ,19 ,21 ,22 ,25 ,26 ,27 ,28 ,30 ,31 ,32 ,33 ,34 ,35 ,39 ,40 ,41 ,42 ,44 ,45 ,46 ,47]. * Step 2: UnsatRules MAYBE + Considered Problem: Rules: 0. f13(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(D,Y1,Z1,D,0,C,C,U,X,Y,D1,K1,L1,M1,R1) [A >= B && A >= 0 && W1 >= 2 && 0 >= 1 + C && X1 >= W1 && D >= W1 && E = 0] (?,1) 1. f13(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(D,Y1,Z1,D,0,C,C,U,X,Y,D1,K1,L1,M1,R1) [A >= B && A >= 0 && W1 >= 2 && C >= 1 && X1 >= W1 && D >= W1 && E = 0] (?,1) 2. f13(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f13(1 + A,B,K,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) [B >= 1 + A && A >= 0] (?,1) 3. f16(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,D,1,Y1,N,D,X,Y,D1,K1,L1,M1,R1) [A >= 0 && W1 >= 2 && 0 >= 1 + N && B2 >= W1 && 0 >= 1 + Y1 && E = 1] (?,1) 4. f16(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,D,1,Y1,N,D,X,Y,D1,K1,L1,M1,R1) [A >= 0 && W1 >= 2 && 0 >= 1 + N && B2 >= W1 && Y1 >= 1 && E = 1] (?,1) 5. f16(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,D,1,Y1,N,D,X,Y,D1,K1,L1,M1,R1) [A >= 0 && W1 >= 2 && N >= 1 && B2 >= W1 && 0 >= 1 + Y1 && E = 1] (?,1) 6. f16(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,D,1,Y1,N,D,X,Y,D1,K1,L1,M1,R1) [A >= 0 && W1 >= 2 && N >= 1 && B2 >= W1 && Y1 >= 1 && E = 1] (?,1) 7. f17(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [U >= 0 && W1 >= 2 && 0 >= 1 + N && 0 >= 1 + Y1 && 0 >= 1 + A2] (?,1) 8. f17(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [U >= 0 && W1 >= 2 && 0 >= 1 + N && 0 >= 1 + Y1 && A2 >= 1] (?,1) 9. f17(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [U >= 0 && W1 >= 2 && 0 >= 1 + N && Y1 >= 1 && 0 >= 1 + A2] (?,1) 10. f17(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [U >= 0 && W1 >= 2 && 0 >= 1 + N && Y1 >= 1 && A2 >= 1] (?,1) 11. f17(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [U >= 0 && W1 >= 2 && N >= 1 && 0 >= 1 + Y1 && 0 >= 1 + A2] (?,1) 12. f17(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [U >= 0 && W1 >= 2 && N >= 1 && 0 >= 1 + Y1 && A2 >= 1] (?,1) 13. f17(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [U >= 0 && W1 >= 2 && N >= 1 && Y1 >= 1 && 0 >= 1 + A2] (?,1) 14. f17(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [U >= 0 && W1 >= 2 && N >= 1 && Y1 >= 1 && A2 >= 1] (?,1) 15. f20(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,L,L,U,E,0,D1,K1,L1,M1,R1) [E >= 0 && D >= 0 && W1 >= 2 && 0 >= 1 + L && X = E && N = 0 && Y = 0] (?,1) 16. f20(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,L,L,U,E,0,D1,K1,L1,M1,R1) [E >= 0 && D >= 0 && W1 >= 2 && L >= 1 && X = E && N = 0 && Y = 0] (?,1) 17. f20(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,-1 + D,1 + E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [E >= 0 && D >= 0 && W1 >= 2 && 0 >= 1 + B2 && 0 >= 1 + Y1 && 0 >= 1 + A2] (?,1) 18. f20(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,-1 + D,1 + E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [E >= 0 && D >= 0 && W1 >= 2 && 0 >= 1 + B2 && 0 >= 1 + Y1 && A2 >= 1] (?,1) 19. f20(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,-1 + D,1 + E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [E >= 0 && D >= 0 && W1 >= 2 && 0 >= 1 + B2 && Y1 >= 1 && 0 >= 1 + A2] (?,1) 20. f20(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,-1 + D,1 + E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [E >= 0 && D >= 0 && W1 >= 2 && 0 >= 1 + B2 && Y1 >= 1 && A2 >= 1] (?,1) 21. f20(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,-1 + D,1 + E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [E >= 0 && D >= 0 && W1 >= 2 && B2 >= 1 && 0 >= 1 + Y1 && 0 >= 1 + A2] (?,1) 22. f20(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,-1 + D,1 + E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [E >= 0 && D >= 0 && W1 >= 2 && B2 >= 1 && 0 >= 1 + Y1 && A2 >= 1] (?,1) 23. f20(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,-1 + D,1 + E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [E >= 0 && D >= 0 && W1 >= 2 && B2 >= 1 && Y1 >= 1 && 0 >= 1 + A2] (?,1) 24. f20(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,-1 + D,1 + E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [E >= 0 && D >= 0 && W1 >= 2 && B2 >= 1 && Y1 >= 1 && A2 >= 1] (?,1) 25. f7(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [D1 >= 0 && W1 >= 2 && 0 >= 1 + N && 0 >= 1 + Y1 && 0 >= 1 + A2] (?,1) 26. f7(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [D1 >= 0 && W1 >= 2 && 0 >= 1 + N && 0 >= 1 + Y1 && A2 >= 1] (?,1) 27. f7(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [D1 >= 0 && W1 >= 2 && 0 >= 1 + N && Y1 >= 1 && 0 >= 1 + A2] (?,1) 28. f7(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [D1 >= 0 && W1 >= 2 && 0 >= 1 + N && Y1 >= 1 && A2 >= 1] (?,1) 29. f7(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [D1 >= 0 && W1 >= 2 && N >= 1 && 0 >= 1 + Y1 && 0 >= 1 + A2] (?,1) 30. f7(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [D1 >= 0 && W1 >= 2 && N >= 1 && 0 >= 1 + Y1 && A2 >= 1] (?,1) 31. f7(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [D1 >= 0 && W1 >= 2 && N >= 1 && Y1 >= 1 && 0 >= 1 + A2] (?,1) 32. f7(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [D1 >= 0 && W1 >= 2 && N >= 1 && Y1 >= 1 && A2 >= 1] (?,1) 33. f11(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,Y1,N,U,-1 + X,1 + Y,D1,K1,L1,M1,R1) [Y >= 0 && X >= 0 && W1 >= 2 && 0 >= 1 + B2 && 0 >= 1 + Y1 && 0 >= 1 + A2] (?,1) 34. f11(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,Y1,N,U,-1 + X,1 + Y,D1,K1,L1,M1,R1) [Y >= 0 && X >= 0 && W1 >= 2 && 0 >= 1 + B2 && 0 >= 1 + Y1 && A2 >= 1] (?,1) 35. f11(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,Y1,N,U,-1 + X,1 + Y,D1,K1,L1,M1,R1) [Y >= 0 && X >= 0 && W1 >= 2 && 0 >= 1 + B2 && Y1 >= 1 && 0 >= 1 + A2] (?,1) 36. f11(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,Y1,N,U,-1 + X,1 + Y,D1,K1,L1,M1,R1) [Y >= 0 && X >= 0 && W1 >= 2 && 0 >= 1 + B2 && Y1 >= 1 && A2 >= 1] (?,1) 37. f11(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,Y1,N,U,-1 + X,1 + Y,D1,K1,L1,M1,R1) [Y >= 0 && X >= 0 && W1 >= 2 && B2 >= 1 && 0 >= 1 + Y1 && 0 >= 1 + A2] (?,1) 38. f11(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,Y1,N,U,-1 + X,1 + Y,D1,K1,L1,M1,R1) [Y >= 0 && X >= 0 && W1 >= 2 && B2 >= 1 && 0 >= 1 + Y1 && A2 >= 1] (?,1) 39. f11(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,Y1,N,U,-1 + X,1 + Y,D1,K1,L1,M1,R1) [Y >= 0 && X >= 0 && W1 >= 2 && B2 >= 1 && Y1 >= 1 && 0 >= 1 + A2] (?,1) 40. f11(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,Y1,N,U,-1 + X,1 + Y,D1,K1,L1,M1,R1) [Y >= 0 && X >= 0 && W1 >= 2 && B2 >= 1 && Y1 >= 1 && A2 >= 1] (?,1) 41. f4(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,0,R1) [Z1 >= 1 + K1 && L1 >= 0 && W1 >= 2 && Y1 >= 1 + Z1 && 0 >= 1 + Y1 && M1 = 0] (?,1) 42. f4(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,0,R1) [Z1 >= 1 + K1 && L1 >= 0 && W1 >= 2 && Y1 >= 1 + Z1 && Y1 >= 1 && M1 = 0] (?,1) 43. f4(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,0,R1) [Z1 >= 1 + K1 && L1 >= 0 && W1 >= 2 && Z1 >= 1 + Y1 && 0 >= 1 + Y1 && M1 = 0] (?,1) 44. f4(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,0,R1) [Z1 >= 1 + K1 && L1 >= 0 && W1 >= 2 && Z1 >= 1 + Y1 && Y1 >= 1 && M1 = 0] (?,1) 45. f4(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,0,R1) [K1 >= 1 + Z1 && L1 >= 0 && W1 >= 2 && Y1 >= 1 + Z1 && 0 >= 1 + Y1 && M1 = 0] (?,1) 46. f4(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,0,R1) [K1 >= 1 + Z1 && L1 >= 0 && W1 >= 2 && Y1 >= 1 + Z1 && Y1 >= 1 && M1 = 0] (?,1) 47. f4(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,0,R1) [K1 >= 1 + Z1 && L1 >= 0 && W1 >= 2 && Z1 >= 1 + Y1 && 0 >= 1 + Y1 && M1 = 0] (?,1) 48. f4(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,0,R1) [K1 >= 1 + Z1 && L1 >= 0 && W1 >= 2 && Z1 >= 1 + Y1 && Y1 >= 1 && M1 = 0] (?,1) 49. f4(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f22(A,B,C,D,E,Z1,N,U,X,Y,D1,E2,L1,D2,R1) [L1 >= 0 && 0 >= 1 + Z1 && W1 >= 2 && M1 = K1] (?,1) 50. f4(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f22(A,B,C,D,E,Z1,N,U,X,Y,D1,E2,L1,D2,R1) [L1 >= 0 && Z1 >= 1 && W1 >= 2 && M1 = K1] (?,1) 51. f5(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,0,-1 + R1) [A2 >= 1 + K1 && R1 >= 0 && W1 >= 2 && Y1 >= 1 + A2 && 0 >= 1 + Y1 && M1 = 0] (?,1) 52. f5(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,0,-1 + R1) [A2 >= 1 + K1 && R1 >= 0 && W1 >= 2 && Y1 >= 1 + A2 && Y1 >= 1 && M1 = 0] (?,1) 53. f5(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,0,-1 + R1) [A2 >= 1 + K1 && R1 >= 0 && W1 >= 2 && A2 >= 1 + Y1 && 0 >= 1 + Y1 && M1 = 0] (?,1) 54. f5(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,0,-1 + R1) [A2 >= 1 + K1 && R1 >= 0 && W1 >= 2 && A2 >= 1 + Y1 && Y1 >= 1 && M1 = 0] (?,1) 55. f5(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,0,-1 + R1) [K1 >= 1 + A2 && R1 >= 0 && W1 >= 2 && Y1 >= 1 + A2 && 0 >= 1 + Y1 && M1 = 0] (?,1) 56. f5(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,0,-1 + R1) [K1 >= 1 + A2 && R1 >= 0 && W1 >= 2 && Y1 >= 1 + A2 && Y1 >= 1 && M1 = 0] (?,1) 57. f5(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,0,-1 + R1) [K1 >= 1 + A2 && R1 >= 0 && W1 >= 2 && A2 >= 1 + Y1 && 0 >= 1 + Y1 && M1 = 0] (?,1) 58. f5(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,0,-1 + R1) [K1 >= 1 + A2 && R1 >= 0 && W1 >= 2 && A2 >= 1 + Y1 && Y1 >= 1 && M1 = 0] (?,1) 59. f5(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f22(A,B,C,D,E,L,N,U,X,Y,D1,D2,L1,C2,R1) [W1 >= 2 && R1 >= 0 && M1 = K1] (?,1) 60. f21(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f13(2,Y1,Z1,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) [Y1 >= 2] (1,1) 61. f17(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,1 + X,Y1,L,U,X,1,X,K1,L1,M1,R1) [B2 >= 2 && W1 >= 2 && U >= 0 && 0 >= 1 + L && 0 >= 1 + Y1 && N = 0 && E = 1 && Y = 1] (?,1) 62. f17(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,1 + X,Y1,L,U,X,1,X,K1,L1,M1,R1) [B2 >= 2 && W1 >= 2 && U >= 0 && 0 >= 1 + L && Y1 >= 1 && N = 0 && E = 1 && Y = 1] (?,1) 63. f17(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,1 + X,Y1,L,U,X,1,X,K1,L1,M1,R1) [B2 >= 2 && W1 >= 2 && U >= 0 && L >= 1 && 0 >= 1 + Y1 && N = 0 && E = 1 && Y = 1] (?,1) 64. f17(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,1 + X,Y1,L,U,X,1,X,K1,L1,M1,R1) [B2 >= 2 && W1 >= 2 && U >= 0 && L >= 1 && Y1 >= 1 && N = 0 && E = 1 && Y = 1] (?,1) 65. f21(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f22(B2,Z1,A2,D,E,0,L2,U,X,Y,D1,Q2,L1,P2,R1) [0 >= F2 && 0 >= G2 && 0 >= H2 && 0 >= Y1 && 0 >= I2] (1,1) 66. f7(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,L,Z1,U,X,1 + R1,D1,L,R1,0,R1) [A2 >= 2 && W1 >= 2 && D1 >= 0 && L >= 1 && 0 >= 1 + L && N = 0 && Y = 1] (?,1) 67. f7(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,L,Z1,U,X,1 + R1,D1,L,R1,0,R1) [A2 >= 2 && W1 >= 2 && D1 >= 0 && L >= 1 && N = 0 && Y = 1] (?,1) 68. f7(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,L,Z1,U,X,1 + R1,D1,L,R1,0,R1) [A2 >= 2 && W1 >= 2 && D1 >= 0 && 0 >= 1 + L && N = 0 && Y = 1] (?,1) 69. f7(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,L,Z1,U,X,1 + R1,D1,L,R1,0,R1) [A2 >= 2 && W1 >= 2 && D1 >= 0 && 0 >= 1 + L && L >= 1 && N = 0 && Y = 1] (?,1) 70. f11(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,L,Z1,U,X,1 + R1,D1,L,R1,0,R1) [A2 >= 2 && W1 >= 2 && X >= 0 && Y >= 0 && L >= 1 && 0 >= 1 + L && N = 0] (?,1) 71. f11(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,L,Z1,U,X,1 + R1,D1,L,R1,0,R1) [A2 >= 2 && W1 >= 2 && X >= 0 && Y >= 0 && L >= 1 && N = 0] (?,1) 72. f11(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,L,Z1,U,X,1 + R1,D1,L,R1,0,R1) [A2 >= 2 && W1 >= 2 && X >= 0 && Y >= 0 && 0 >= 1 + L && N = 0] (?,1) 73. f11(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,L,Z1,U,X,1 + R1,D1,L,R1,0,R1) [A2 >= 2 && W1 >= 2 && X >= 0 && Y >= 0 && 0 >= 1 + L && L >= 1 && N = 0] (?,1) Signature: {(f11,48);(f13,48);(f16,48);(f17,48);(f20,48);(f21,48);(f22,48);(f4,48);(f5,48);(f7,48)} Flow Graph: [0->{15,16,17,18,19,20,21,22,23,24},1->{15,16,17,18,19,20,21,22,23,24},2->{0,1,2},3->{15,16,17,18,19,20,21 ,22,23,24},4->{15,16,17,18,19,20,21,22,23,24},5->{15,16,17,18,19,20,21,22,23,24},6->{15,16,17,18,19,20,21,22 ,23,24},7->{15,16,17,18,19,20,21,22,23,24},8->{15,16,17,18,19,20,21,22,23,24},9->{15,16,17,18,19,20,21,22,23 ,24},10->{15,16,17,18,19,20,21,22,23,24},11->{15,16,17,18,19,20,21,22,23,24},12->{15,16,17,18,19,20,21,22,23 ,24},13->{15,16,17,18,19,20,21,22,23,24},14->{15,16,17,18,19,20,21,22,23,24},15->{33,34,35,36,37,38,39,40,70 ,71,72,73},16->{33,34,35,36,37,38,39,40,70,71,72,73},17->{15,16,17,18,19,20,21,22,23,24},18->{15,16,17,18,19 ,20,21,22,23,24},19->{15,16,17,18,19,20,21,22,23,24},20->{15,16,17,18,19,20,21,22,23,24},21->{15,16,17,18,19 ,20,21,22,23,24},22->{15,16,17,18,19,20,21,22,23,24},23->{15,16,17,18,19,20,21,22,23,24},24->{15,16,17,18,19 ,20,21,22,23,24},25->{33,34,35,36,37,38,39,40,70,71,72,73},26->{33,34,35,36,37,38,39,40,70,71,72,73},27->{33 ,34,35,36,37,38,39,40,70,71,72,73},28->{33,34,35,36,37,38,39,40,70,71,72,73},29->{33,34,35,36,37,38,39,40,70 ,71,72,73},30->{33,34,35,36,37,38,39,40,70,71,72,73},31->{33,34,35,36,37,38,39,40,70,71,72,73},32->{33,34,35 ,36,37,38,39,40,70,71,72,73},33->{33,34,35,36,37,38,39,40,70,71,72,73},34->{33,34,35,36,37,38,39,40,70,71,72 ,73},35->{33,34,35,36,37,38,39,40,70,71,72,73},36->{33,34,35,36,37,38,39,40,70,71,72,73},37->{33,34,35,36,37 ,38,39,40,70,71,72,73},38->{33,34,35,36,37,38,39,40,70,71,72,73},39->{33,34,35,36,37,38,39,40,70,71,72,73} ,40->{33,34,35,36,37,38,39,40,70,71,72,73},41->{51,52,53,54,55,56,57,58,59},42->{51,52,53,54,55,56,57,58,59} ,43->{51,52,53,54,55,56,57,58,59},44->{51,52,53,54,55,56,57,58,59},45->{51,52,53,54,55,56,57,58,59},46->{51 ,52,53,54,55,56,57,58,59},47->{51,52,53,54,55,56,57,58,59},48->{51,52,53,54,55,56,57,58,59},49->{},50->{} ,51->{51,52,53,54,55,56,57,58,59},52->{51,52,53,54,55,56,57,58,59},53->{51,52,53,54,55,56,57,58,59},54->{51 ,52,53,54,55,56,57,58,59},55->{51,52,53,54,55,56,57,58,59},56->{51,52,53,54,55,56,57,58,59},57->{51,52,53,54 ,55,56,57,58,59},58->{51,52,53,54,55,56,57,58,59},59->{},60->{0,1,2},61->{33,34,35,36,37,38,39,40,70,71,72 ,73},62->{33,34,35,36,37,38,39,40,70,71,72,73},63->{33,34,35,36,37,38,39,40,70,71,72,73},64->{33,34,35,36,37 ,38,39,40,70,71,72,73},65->{},66->{51,52,53,54,55,56,57,58,59},67->{51,52,53,54,55,56,57,58,59},68->{51,52 ,53,54,55,56,57,58,59},69->{51,52,53,54,55,56,57,58,59},70->{51,52,53,54,55,56,57,58,59},71->{51,52,53,54,55 ,56,57,58,59},72->{51,52,53,54,55,56,57,58,59},73->{51,52,53,54,55,56,57,58,59}] + Applied Processor: UnsatRules + Details: Following transitions have unsatisfiable constraints and are removed: [66,69,70,73] * Step 3: UnsatPaths MAYBE + Considered Problem: Rules: 0. f13(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(D,Y1,Z1,D,0,C,C,U,X,Y,D1,K1,L1,M1,R1) [A >= B && A >= 0 && W1 >= 2 && 0 >= 1 + C && X1 >= W1 && D >= W1 && E = 0] (?,1) 1. f13(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(D,Y1,Z1,D,0,C,C,U,X,Y,D1,K1,L1,M1,R1) [A >= B && A >= 0 && W1 >= 2 && C >= 1 && X1 >= W1 && D >= W1 && E = 0] (?,1) 2. f13(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f13(1 + A,B,K,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) [B >= 1 + A && A >= 0] (?,1) 3. f16(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,D,1,Y1,N,D,X,Y,D1,K1,L1,M1,R1) [A >= 0 && W1 >= 2 && 0 >= 1 + N && B2 >= W1 && 0 >= 1 + Y1 && E = 1] (?,1) 4. f16(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,D,1,Y1,N,D,X,Y,D1,K1,L1,M1,R1) [A >= 0 && W1 >= 2 && 0 >= 1 + N && B2 >= W1 && Y1 >= 1 && E = 1] (?,1) 5. f16(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,D,1,Y1,N,D,X,Y,D1,K1,L1,M1,R1) [A >= 0 && W1 >= 2 && N >= 1 && B2 >= W1 && 0 >= 1 + Y1 && E = 1] (?,1) 6. f16(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,D,1,Y1,N,D,X,Y,D1,K1,L1,M1,R1) [A >= 0 && W1 >= 2 && N >= 1 && B2 >= W1 && Y1 >= 1 && E = 1] (?,1) 7. f17(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [U >= 0 && W1 >= 2 && 0 >= 1 + N && 0 >= 1 + Y1 && 0 >= 1 + A2] (?,1) 8. f17(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [U >= 0 && W1 >= 2 && 0 >= 1 + N && 0 >= 1 + Y1 && A2 >= 1] (?,1) 9. f17(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [U >= 0 && W1 >= 2 && 0 >= 1 + N && Y1 >= 1 && 0 >= 1 + A2] (?,1) 10. f17(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [U >= 0 && W1 >= 2 && 0 >= 1 + N && Y1 >= 1 && A2 >= 1] (?,1) 11. f17(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [U >= 0 && W1 >= 2 && N >= 1 && 0 >= 1 + Y1 && 0 >= 1 + A2] (?,1) 12. f17(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [U >= 0 && W1 >= 2 && N >= 1 && 0 >= 1 + Y1 && A2 >= 1] (?,1) 13. f17(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [U >= 0 && W1 >= 2 && N >= 1 && Y1 >= 1 && 0 >= 1 + A2] (?,1) 14. f17(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [U >= 0 && W1 >= 2 && N >= 1 && Y1 >= 1 && A2 >= 1] (?,1) 15. f20(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,L,L,U,E,0,D1,K1,L1,M1,R1) [E >= 0 && D >= 0 && W1 >= 2 && 0 >= 1 + L && X = E && N = 0 && Y = 0] (?,1) 16. f20(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,L,L,U,E,0,D1,K1,L1,M1,R1) [E >= 0 && D >= 0 && W1 >= 2 && L >= 1 && X = E && N = 0 && Y = 0] (?,1) 17. f20(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,-1 + D,1 + E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [E >= 0 && D >= 0 && W1 >= 2 && 0 >= 1 + B2 && 0 >= 1 + Y1 && 0 >= 1 + A2] (?,1) 18. f20(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,-1 + D,1 + E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [E >= 0 && D >= 0 && W1 >= 2 && 0 >= 1 + B2 && 0 >= 1 + Y1 && A2 >= 1] (?,1) 19. f20(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,-1 + D,1 + E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [E >= 0 && D >= 0 && W1 >= 2 && 0 >= 1 + B2 && Y1 >= 1 && 0 >= 1 + A2] (?,1) 20. f20(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,-1 + D,1 + E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [E >= 0 && D >= 0 && W1 >= 2 && 0 >= 1 + B2 && Y1 >= 1 && A2 >= 1] (?,1) 21. f20(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,-1 + D,1 + E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [E >= 0 && D >= 0 && W1 >= 2 && B2 >= 1 && 0 >= 1 + Y1 && 0 >= 1 + A2] (?,1) 22. f20(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,-1 + D,1 + E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [E >= 0 && D >= 0 && W1 >= 2 && B2 >= 1 && 0 >= 1 + Y1 && A2 >= 1] (?,1) 23. f20(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,-1 + D,1 + E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [E >= 0 && D >= 0 && W1 >= 2 && B2 >= 1 && Y1 >= 1 && 0 >= 1 + A2] (?,1) 24. f20(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,-1 + D,1 + E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [E >= 0 && D >= 0 && W1 >= 2 && B2 >= 1 && Y1 >= 1 && A2 >= 1] (?,1) 25. f7(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [D1 >= 0 && W1 >= 2 && 0 >= 1 + N && 0 >= 1 + Y1 && 0 >= 1 + A2] (?,1) 26. f7(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [D1 >= 0 && W1 >= 2 && 0 >= 1 + N && 0 >= 1 + Y1 && A2 >= 1] (?,1) 27. f7(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [D1 >= 0 && W1 >= 2 && 0 >= 1 + N && Y1 >= 1 && 0 >= 1 + A2] (?,1) 28. f7(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [D1 >= 0 && W1 >= 2 && 0 >= 1 + N && Y1 >= 1 && A2 >= 1] (?,1) 29. f7(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [D1 >= 0 && W1 >= 2 && N >= 1 && 0 >= 1 + Y1 && 0 >= 1 + A2] (?,1) 30. f7(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [D1 >= 0 && W1 >= 2 && N >= 1 && 0 >= 1 + Y1 && A2 >= 1] (?,1) 31. f7(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [D1 >= 0 && W1 >= 2 && N >= 1 && Y1 >= 1 && 0 >= 1 + A2] (?,1) 32. f7(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [D1 >= 0 && W1 >= 2 && N >= 1 && Y1 >= 1 && A2 >= 1] (?,1) 33. f11(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,Y1,N,U,-1 + X,1 + Y,D1,K1,L1,M1,R1) [Y >= 0 && X >= 0 && W1 >= 2 && 0 >= 1 + B2 && 0 >= 1 + Y1 && 0 >= 1 + A2] (?,1) 34. f11(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,Y1,N,U,-1 + X,1 + Y,D1,K1,L1,M1,R1) [Y >= 0 && X >= 0 && W1 >= 2 && 0 >= 1 + B2 && 0 >= 1 + Y1 && A2 >= 1] (?,1) 35. f11(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,Y1,N,U,-1 + X,1 + Y,D1,K1,L1,M1,R1) [Y >= 0 && X >= 0 && W1 >= 2 && 0 >= 1 + B2 && Y1 >= 1 && 0 >= 1 + A2] (?,1) 36. f11(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,Y1,N,U,-1 + X,1 + Y,D1,K1,L1,M1,R1) [Y >= 0 && X >= 0 && W1 >= 2 && 0 >= 1 + B2 && Y1 >= 1 && A2 >= 1] (?,1) 37. f11(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,Y1,N,U,-1 + X,1 + Y,D1,K1,L1,M1,R1) [Y >= 0 && X >= 0 && W1 >= 2 && B2 >= 1 && 0 >= 1 + Y1 && 0 >= 1 + A2] (?,1) 38. f11(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,Y1,N,U,-1 + X,1 + Y,D1,K1,L1,M1,R1) [Y >= 0 && X >= 0 && W1 >= 2 && B2 >= 1 && 0 >= 1 + Y1 && A2 >= 1] (?,1) 39. f11(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,Y1,N,U,-1 + X,1 + Y,D1,K1,L1,M1,R1) [Y >= 0 && X >= 0 && W1 >= 2 && B2 >= 1 && Y1 >= 1 && 0 >= 1 + A2] (?,1) 40. f11(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,Y1,N,U,-1 + X,1 + Y,D1,K1,L1,M1,R1) [Y >= 0 && X >= 0 && W1 >= 2 && B2 >= 1 && Y1 >= 1 && A2 >= 1] (?,1) 41. f4(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,0,R1) [Z1 >= 1 + K1 && L1 >= 0 && W1 >= 2 && Y1 >= 1 + Z1 && 0 >= 1 + Y1 && M1 = 0] (?,1) 42. f4(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,0,R1) [Z1 >= 1 + K1 && L1 >= 0 && W1 >= 2 && Y1 >= 1 + Z1 && Y1 >= 1 && M1 = 0] (?,1) 43. f4(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,0,R1) [Z1 >= 1 + K1 && L1 >= 0 && W1 >= 2 && Z1 >= 1 + Y1 && 0 >= 1 + Y1 && M1 = 0] (?,1) 44. f4(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,0,R1) [Z1 >= 1 + K1 && L1 >= 0 && W1 >= 2 && Z1 >= 1 + Y1 && Y1 >= 1 && M1 = 0] (?,1) 45. f4(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,0,R1) [K1 >= 1 + Z1 && L1 >= 0 && W1 >= 2 && Y1 >= 1 + Z1 && 0 >= 1 + Y1 && M1 = 0] (?,1) 46. f4(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,0,R1) [K1 >= 1 + Z1 && L1 >= 0 && W1 >= 2 && Y1 >= 1 + Z1 && Y1 >= 1 && M1 = 0] (?,1) 47. f4(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,0,R1) [K1 >= 1 + Z1 && L1 >= 0 && W1 >= 2 && Z1 >= 1 + Y1 && 0 >= 1 + Y1 && M1 = 0] (?,1) 48. f4(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,0,R1) [K1 >= 1 + Z1 && L1 >= 0 && W1 >= 2 && Z1 >= 1 + Y1 && Y1 >= 1 && M1 = 0] (?,1) 49. f4(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f22(A,B,C,D,E,Z1,N,U,X,Y,D1,E2,L1,D2,R1) [L1 >= 0 && 0 >= 1 + Z1 && W1 >= 2 && M1 = K1] (?,1) 50. f4(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f22(A,B,C,D,E,Z1,N,U,X,Y,D1,E2,L1,D2,R1) [L1 >= 0 && Z1 >= 1 && W1 >= 2 && M1 = K1] (?,1) 51. f5(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,0,-1 + R1) [A2 >= 1 + K1 && R1 >= 0 && W1 >= 2 && Y1 >= 1 + A2 && 0 >= 1 + Y1 && M1 = 0] (?,1) 52. f5(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,0,-1 + R1) [A2 >= 1 + K1 && R1 >= 0 && W1 >= 2 && Y1 >= 1 + A2 && Y1 >= 1 && M1 = 0] (?,1) 53. f5(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,0,-1 + R1) [A2 >= 1 + K1 && R1 >= 0 && W1 >= 2 && A2 >= 1 + Y1 && 0 >= 1 + Y1 && M1 = 0] (?,1) 54. f5(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,0,-1 + R1) [A2 >= 1 + K1 && R1 >= 0 && W1 >= 2 && A2 >= 1 + Y1 && Y1 >= 1 && M1 = 0] (?,1) 55. f5(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,0,-1 + R1) [K1 >= 1 + A2 && R1 >= 0 && W1 >= 2 && Y1 >= 1 + A2 && 0 >= 1 + Y1 && M1 = 0] (?,1) 56. f5(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,0,-1 + R1) [K1 >= 1 + A2 && R1 >= 0 && W1 >= 2 && Y1 >= 1 + A2 && Y1 >= 1 && M1 = 0] (?,1) 57. f5(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,0,-1 + R1) [K1 >= 1 + A2 && R1 >= 0 && W1 >= 2 && A2 >= 1 + Y1 && 0 >= 1 + Y1 && M1 = 0] (?,1) 58. f5(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,0,-1 + R1) [K1 >= 1 + A2 && R1 >= 0 && W1 >= 2 && A2 >= 1 + Y1 && Y1 >= 1 && M1 = 0] (?,1) 59. f5(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f22(A,B,C,D,E,L,N,U,X,Y,D1,D2,L1,C2,R1) [W1 >= 2 && R1 >= 0 && M1 = K1] (?,1) 60. f21(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f13(2,Y1,Z1,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) [Y1 >= 2] (1,1) 61. f17(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,1 + X,Y1,L,U,X,1,X,K1,L1,M1,R1) [B2 >= 2 && W1 >= 2 && U >= 0 && 0 >= 1 + L && 0 >= 1 + Y1 && N = 0 && E = 1 && Y = 1] (?,1) 62. f17(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,1 + X,Y1,L,U,X,1,X,K1,L1,M1,R1) [B2 >= 2 && W1 >= 2 && U >= 0 && 0 >= 1 + L && Y1 >= 1 && N = 0 && E = 1 && Y = 1] (?,1) 63. f17(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,1 + X,Y1,L,U,X,1,X,K1,L1,M1,R1) [B2 >= 2 && W1 >= 2 && U >= 0 && L >= 1 && 0 >= 1 + Y1 && N = 0 && E = 1 && Y = 1] (?,1) 64. f17(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,1 + X,Y1,L,U,X,1,X,K1,L1,M1,R1) [B2 >= 2 && W1 >= 2 && U >= 0 && L >= 1 && Y1 >= 1 && N = 0 && E = 1 && Y = 1] (?,1) 65. f21(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f22(B2,Z1,A2,D,E,0,L2,U,X,Y,D1,Q2,L1,P2,R1) [0 >= F2 && 0 >= G2 && 0 >= H2 && 0 >= Y1 && 0 >= I2] (1,1) 67. f7(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,L,Z1,U,X,1 + R1,D1,L,R1,0,R1) [A2 >= 2 && W1 >= 2 && D1 >= 0 && L >= 1 && N = 0 && Y = 1] (?,1) 68. f7(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,L,Z1,U,X,1 + R1,D1,L,R1,0,R1) [A2 >= 2 && W1 >= 2 && D1 >= 0 && 0 >= 1 + L && N = 0 && Y = 1] (?,1) 71. f11(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,L,Z1,U,X,1 + R1,D1,L,R1,0,R1) [A2 >= 2 && W1 >= 2 && X >= 0 && Y >= 0 && L >= 1 && N = 0] (?,1) 72. f11(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,L,Z1,U,X,1 + R1,D1,L,R1,0,R1) [A2 >= 2 && W1 >= 2 && X >= 0 && Y >= 0 && 0 >= 1 + L && N = 0] (?,1) Signature: {(f11,48);(f13,48);(f16,48);(f17,48);(f20,48);(f21,48);(f22,48);(f4,48);(f5,48);(f7,48)} Flow Graph: [0->{15,16,17,18,19,20,21,22,23,24},1->{15,16,17,18,19,20,21,22,23,24},2->{0,1,2},3->{15,16,17,18,19,20,21 ,22,23,24},4->{15,16,17,18,19,20,21,22,23,24},5->{15,16,17,18,19,20,21,22,23,24},6->{15,16,17,18,19,20,21,22 ,23,24},7->{15,16,17,18,19,20,21,22,23,24},8->{15,16,17,18,19,20,21,22,23,24},9->{15,16,17,18,19,20,21,22,23 ,24},10->{15,16,17,18,19,20,21,22,23,24},11->{15,16,17,18,19,20,21,22,23,24},12->{15,16,17,18,19,20,21,22,23 ,24},13->{15,16,17,18,19,20,21,22,23,24},14->{15,16,17,18,19,20,21,22,23,24},15->{33,34,35,36,37,38,39,40,71 ,72},16->{33,34,35,36,37,38,39,40,71,72},17->{15,16,17,18,19,20,21,22,23,24},18->{15,16,17,18,19,20,21,22,23 ,24},19->{15,16,17,18,19,20,21,22,23,24},20->{15,16,17,18,19,20,21,22,23,24},21->{15,16,17,18,19,20,21,22,23 ,24},22->{15,16,17,18,19,20,21,22,23,24},23->{15,16,17,18,19,20,21,22,23,24},24->{15,16,17,18,19,20,21,22,23 ,24},25->{33,34,35,36,37,38,39,40,71,72},26->{33,34,35,36,37,38,39,40,71,72},27->{33,34,35,36,37,38,39,40,71 ,72},28->{33,34,35,36,37,38,39,40,71,72},29->{33,34,35,36,37,38,39,40,71,72},30->{33,34,35,36,37,38,39,40,71 ,72},31->{33,34,35,36,37,38,39,40,71,72},32->{33,34,35,36,37,38,39,40,71,72},33->{33,34,35,36,37,38,39,40,71 ,72},34->{33,34,35,36,37,38,39,40,71,72},35->{33,34,35,36,37,38,39,40,71,72},36->{33,34,35,36,37,38,39,40,71 ,72},37->{33,34,35,36,37,38,39,40,71,72},38->{33,34,35,36,37,38,39,40,71,72},39->{33,34,35,36,37,38,39,40,71 ,72},40->{33,34,35,36,37,38,39,40,71,72},41->{51,52,53,54,55,56,57,58,59},42->{51,52,53,54,55,56,57,58,59} ,43->{51,52,53,54,55,56,57,58,59},44->{51,52,53,54,55,56,57,58,59},45->{51,52,53,54,55,56,57,58,59},46->{51 ,52,53,54,55,56,57,58,59},47->{51,52,53,54,55,56,57,58,59},48->{51,52,53,54,55,56,57,58,59},49->{},50->{} ,51->{51,52,53,54,55,56,57,58,59},52->{51,52,53,54,55,56,57,58,59},53->{51,52,53,54,55,56,57,58,59},54->{51 ,52,53,54,55,56,57,58,59},55->{51,52,53,54,55,56,57,58,59},56->{51,52,53,54,55,56,57,58,59},57->{51,52,53,54 ,55,56,57,58,59},58->{51,52,53,54,55,56,57,58,59},59->{},60->{0,1,2},61->{33,34,35,36,37,38,39,40,71,72} ,62->{33,34,35,36,37,38,39,40,71,72},63->{33,34,35,36,37,38,39,40,71,72},64->{33,34,35,36,37,38,39,40,71,72} ,65->{},67->{51,52,53,54,55,56,57,58,59},68->{51,52,53,54,55,56,57,58,59},71->{51,52,53,54,55,56,57,58,59} ,72->{51,52,53,54,55,56,57,58,59}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(0,15) ,(0,16) ,(1,15) ,(1,16) ,(3,15) ,(3,16) ,(4,15) ,(4,16) ,(5,15) ,(5,16) ,(6,15) ,(6,16) ,(7,15) ,(7,16) ,(8,15) ,(8,16) ,(9,15) ,(9,16) ,(10,15) ,(10,16) ,(11,15) ,(11,16) ,(12,15) ,(12,16) ,(13,15) ,(13,16) ,(14,15) ,(14,16) ,(15,71) ,(15,72) ,(16,71) ,(16,72) ,(17,16) ,(18,16) ,(19,15) ,(20,15) ,(21,16) ,(22,16) ,(23,15) ,(24,15) ,(25,71) ,(25,72) ,(26,71) ,(26,72) ,(27,71) ,(27,72) ,(28,71) ,(28,72) ,(29,71) ,(29,72) ,(30,71) ,(30,72) ,(31,71) ,(31,72) ,(32,71) ,(32,72) ,(33,71) ,(34,71) ,(35,72) ,(36,72) ,(37,71) ,(38,71) ,(39,72) ,(40,72) ,(41,58) ,(41,59) ,(48,51) ,(48,59) ,(51,58) ,(51,59) ,(58,51) ,(58,59) ,(61,71) ,(61,72) ,(62,71) ,(62,72) ,(63,71) ,(63,72) ,(64,71) ,(64,72) ,(67,51) ,(67,59) ,(68,58) ,(68,59) ,(71,51) ,(71,59) ,(72,58) ,(72,59)] * Step 4: UnreachableRules MAYBE + Considered Problem: Rules: 0. f13(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(D,Y1,Z1,D,0,C,C,U,X,Y,D1,K1,L1,M1,R1) [A >= B && A >= 0 && W1 >= 2 && 0 >= 1 + C && X1 >= W1 && D >= W1 && E = 0] (?,1) 1. f13(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(D,Y1,Z1,D,0,C,C,U,X,Y,D1,K1,L1,M1,R1) [A >= B && A >= 0 && W1 >= 2 && C >= 1 && X1 >= W1 && D >= W1 && E = 0] (?,1) 2. f13(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f13(1 + A,B,K,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) [B >= 1 + A && A >= 0] (?,1) 3. f16(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,D,1,Y1,N,D,X,Y,D1,K1,L1,M1,R1) [A >= 0 && W1 >= 2 && 0 >= 1 + N && B2 >= W1 && 0 >= 1 + Y1 && E = 1] (?,1) 4. f16(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,D,1,Y1,N,D,X,Y,D1,K1,L1,M1,R1) [A >= 0 && W1 >= 2 && 0 >= 1 + N && B2 >= W1 && Y1 >= 1 && E = 1] (?,1) 5. f16(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,D,1,Y1,N,D,X,Y,D1,K1,L1,M1,R1) [A >= 0 && W1 >= 2 && N >= 1 && B2 >= W1 && 0 >= 1 + Y1 && E = 1] (?,1) 6. f16(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,D,1,Y1,N,D,X,Y,D1,K1,L1,M1,R1) [A >= 0 && W1 >= 2 && N >= 1 && B2 >= W1 && Y1 >= 1 && E = 1] (?,1) 7. f17(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [U >= 0 && W1 >= 2 && 0 >= 1 + N && 0 >= 1 + Y1 && 0 >= 1 + A2] (?,1) 8. f17(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [U >= 0 && W1 >= 2 && 0 >= 1 + N && 0 >= 1 + Y1 && A2 >= 1] (?,1) 9. f17(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [U >= 0 && W1 >= 2 && 0 >= 1 + N && Y1 >= 1 && 0 >= 1 + A2] (?,1) 10. f17(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [U >= 0 && W1 >= 2 && 0 >= 1 + N && Y1 >= 1 && A2 >= 1] (?,1) 11. f17(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [U >= 0 && W1 >= 2 && N >= 1 && 0 >= 1 + Y1 && 0 >= 1 + A2] (?,1) 12. f17(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [U >= 0 && W1 >= 2 && N >= 1 && 0 >= 1 + Y1 && A2 >= 1] (?,1) 13. f17(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [U >= 0 && W1 >= 2 && N >= 1 && Y1 >= 1 && 0 >= 1 + A2] (?,1) 14. f17(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [U >= 0 && W1 >= 2 && N >= 1 && Y1 >= 1 && A2 >= 1] (?,1) 15. f20(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,L,L,U,E,0,D1,K1,L1,M1,R1) [E >= 0 && D >= 0 && W1 >= 2 && 0 >= 1 + L && X = E && N = 0 && Y = 0] (?,1) 16. f20(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,L,L,U,E,0,D1,K1,L1,M1,R1) [E >= 0 && D >= 0 && W1 >= 2 && L >= 1 && X = E && N = 0 && Y = 0] (?,1) 17. f20(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,-1 + D,1 + E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [E >= 0 && D >= 0 && W1 >= 2 && 0 >= 1 + B2 && 0 >= 1 + Y1 && 0 >= 1 + A2] (?,1) 18. f20(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,-1 + D,1 + E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [E >= 0 && D >= 0 && W1 >= 2 && 0 >= 1 + B2 && 0 >= 1 + Y1 && A2 >= 1] (?,1) 19. f20(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,-1 + D,1 + E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [E >= 0 && D >= 0 && W1 >= 2 && 0 >= 1 + B2 && Y1 >= 1 && 0 >= 1 + A2] (?,1) 20. f20(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,-1 + D,1 + E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [E >= 0 && D >= 0 && W1 >= 2 && 0 >= 1 + B2 && Y1 >= 1 && A2 >= 1] (?,1) 21. f20(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,-1 + D,1 + E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [E >= 0 && D >= 0 && W1 >= 2 && B2 >= 1 && 0 >= 1 + Y1 && 0 >= 1 + A2] (?,1) 22. f20(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,-1 + D,1 + E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [E >= 0 && D >= 0 && W1 >= 2 && B2 >= 1 && 0 >= 1 + Y1 && A2 >= 1] (?,1) 23. f20(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,-1 + D,1 + E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [E >= 0 && D >= 0 && W1 >= 2 && B2 >= 1 && Y1 >= 1 && 0 >= 1 + A2] (?,1) 24. f20(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,-1 + D,1 + E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [E >= 0 && D >= 0 && W1 >= 2 && B2 >= 1 && Y1 >= 1 && A2 >= 1] (?,1) 25. f7(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [D1 >= 0 && W1 >= 2 && 0 >= 1 + N && 0 >= 1 + Y1 && 0 >= 1 + A2] (?,1) 26. f7(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [D1 >= 0 && W1 >= 2 && 0 >= 1 + N && 0 >= 1 + Y1 && A2 >= 1] (?,1) 27. f7(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [D1 >= 0 && W1 >= 2 && 0 >= 1 + N && Y1 >= 1 && 0 >= 1 + A2] (?,1) 28. f7(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [D1 >= 0 && W1 >= 2 && 0 >= 1 + N && Y1 >= 1 && A2 >= 1] (?,1) 29. f7(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [D1 >= 0 && W1 >= 2 && N >= 1 && 0 >= 1 + Y1 && 0 >= 1 + A2] (?,1) 30. f7(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [D1 >= 0 && W1 >= 2 && N >= 1 && 0 >= 1 + Y1 && A2 >= 1] (?,1) 31. f7(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [D1 >= 0 && W1 >= 2 && N >= 1 && Y1 >= 1 && 0 >= 1 + A2] (?,1) 32. f7(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [D1 >= 0 && W1 >= 2 && N >= 1 && Y1 >= 1 && A2 >= 1] (?,1) 33. f11(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,Y1,N,U,-1 + X,1 + Y,D1,K1,L1,M1,R1) [Y >= 0 && X >= 0 && W1 >= 2 && 0 >= 1 + B2 && 0 >= 1 + Y1 && 0 >= 1 + A2] (?,1) 34. f11(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,Y1,N,U,-1 + X,1 + Y,D1,K1,L1,M1,R1) [Y >= 0 && X >= 0 && W1 >= 2 && 0 >= 1 + B2 && 0 >= 1 + Y1 && A2 >= 1] (?,1) 35. f11(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,Y1,N,U,-1 + X,1 + Y,D1,K1,L1,M1,R1) [Y >= 0 && X >= 0 && W1 >= 2 && 0 >= 1 + B2 && Y1 >= 1 && 0 >= 1 + A2] (?,1) 36. f11(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,Y1,N,U,-1 + X,1 + Y,D1,K1,L1,M1,R1) [Y >= 0 && X >= 0 && W1 >= 2 && 0 >= 1 + B2 && Y1 >= 1 && A2 >= 1] (?,1) 37. f11(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,Y1,N,U,-1 + X,1 + Y,D1,K1,L1,M1,R1) [Y >= 0 && X >= 0 && W1 >= 2 && B2 >= 1 && 0 >= 1 + Y1 && 0 >= 1 + A2] (?,1) 38. f11(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,Y1,N,U,-1 + X,1 + Y,D1,K1,L1,M1,R1) [Y >= 0 && X >= 0 && W1 >= 2 && B2 >= 1 && 0 >= 1 + Y1 && A2 >= 1] (?,1) 39. f11(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,Y1,N,U,-1 + X,1 + Y,D1,K1,L1,M1,R1) [Y >= 0 && X >= 0 && W1 >= 2 && B2 >= 1 && Y1 >= 1 && 0 >= 1 + A2] (?,1) 40. f11(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,Y1,N,U,-1 + X,1 + Y,D1,K1,L1,M1,R1) [Y >= 0 && X >= 0 && W1 >= 2 && B2 >= 1 && Y1 >= 1 && A2 >= 1] (?,1) 41. f4(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,0,R1) [Z1 >= 1 + K1 && L1 >= 0 && W1 >= 2 && Y1 >= 1 + Z1 && 0 >= 1 + Y1 && M1 = 0] (?,1) 42. f4(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,0,R1) [Z1 >= 1 + K1 && L1 >= 0 && W1 >= 2 && Y1 >= 1 + Z1 && Y1 >= 1 && M1 = 0] (?,1) 43. f4(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,0,R1) [Z1 >= 1 + K1 && L1 >= 0 && W1 >= 2 && Z1 >= 1 + Y1 && 0 >= 1 + Y1 && M1 = 0] (?,1) 44. f4(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,0,R1) [Z1 >= 1 + K1 && L1 >= 0 && W1 >= 2 && Z1 >= 1 + Y1 && Y1 >= 1 && M1 = 0] (?,1) 45. f4(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,0,R1) [K1 >= 1 + Z1 && L1 >= 0 && W1 >= 2 && Y1 >= 1 + Z1 && 0 >= 1 + Y1 && M1 = 0] (?,1) 46. f4(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,0,R1) [K1 >= 1 + Z1 && L1 >= 0 && W1 >= 2 && Y1 >= 1 + Z1 && Y1 >= 1 && M1 = 0] (?,1) 47. f4(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,0,R1) [K1 >= 1 + Z1 && L1 >= 0 && W1 >= 2 && Z1 >= 1 + Y1 && 0 >= 1 + Y1 && M1 = 0] (?,1) 48. f4(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,0,R1) [K1 >= 1 + Z1 && L1 >= 0 && W1 >= 2 && Z1 >= 1 + Y1 && Y1 >= 1 && M1 = 0] (?,1) 49. f4(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f22(A,B,C,D,E,Z1,N,U,X,Y,D1,E2,L1,D2,R1) [L1 >= 0 && 0 >= 1 + Z1 && W1 >= 2 && M1 = K1] (?,1) 50. f4(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f22(A,B,C,D,E,Z1,N,U,X,Y,D1,E2,L1,D2,R1) [L1 >= 0 && Z1 >= 1 && W1 >= 2 && M1 = K1] (?,1) 51. f5(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,0,-1 + R1) [A2 >= 1 + K1 && R1 >= 0 && W1 >= 2 && Y1 >= 1 + A2 && 0 >= 1 + Y1 && M1 = 0] (?,1) 52. f5(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,0,-1 + R1) [A2 >= 1 + K1 && R1 >= 0 && W1 >= 2 && Y1 >= 1 + A2 && Y1 >= 1 && M1 = 0] (?,1) 53. f5(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,0,-1 + R1) [A2 >= 1 + K1 && R1 >= 0 && W1 >= 2 && A2 >= 1 + Y1 && 0 >= 1 + Y1 && M1 = 0] (?,1) 54. f5(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,0,-1 + R1) [A2 >= 1 + K1 && R1 >= 0 && W1 >= 2 && A2 >= 1 + Y1 && Y1 >= 1 && M1 = 0] (?,1) 55. f5(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,0,-1 + R1) [K1 >= 1 + A2 && R1 >= 0 && W1 >= 2 && Y1 >= 1 + A2 && 0 >= 1 + Y1 && M1 = 0] (?,1) 56. f5(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,0,-1 + R1) [K1 >= 1 + A2 && R1 >= 0 && W1 >= 2 && Y1 >= 1 + A2 && Y1 >= 1 && M1 = 0] (?,1) 57. f5(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,0,-1 + R1) [K1 >= 1 + A2 && R1 >= 0 && W1 >= 2 && A2 >= 1 + Y1 && 0 >= 1 + Y1 && M1 = 0] (?,1) 58. f5(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,0,-1 + R1) [K1 >= 1 + A2 && R1 >= 0 && W1 >= 2 && A2 >= 1 + Y1 && Y1 >= 1 && M1 = 0] (?,1) 59. f5(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f22(A,B,C,D,E,L,N,U,X,Y,D1,D2,L1,C2,R1) [W1 >= 2 && R1 >= 0 && M1 = K1] (?,1) 60. f21(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f13(2,Y1,Z1,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) [Y1 >= 2] (1,1) 61. f17(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,1 + X,Y1,L,U,X,1,X,K1,L1,M1,R1) [B2 >= 2 && W1 >= 2 && U >= 0 && 0 >= 1 + L && 0 >= 1 + Y1 && N = 0 && E = 1 && Y = 1] (?,1) 62. f17(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,1 + X,Y1,L,U,X,1,X,K1,L1,M1,R1) [B2 >= 2 && W1 >= 2 && U >= 0 && 0 >= 1 + L && Y1 >= 1 && N = 0 && E = 1 && Y = 1] (?,1) 63. f17(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,1 + X,Y1,L,U,X,1,X,K1,L1,M1,R1) [B2 >= 2 && W1 >= 2 && U >= 0 && L >= 1 && 0 >= 1 + Y1 && N = 0 && E = 1 && Y = 1] (?,1) 64. f17(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,1 + X,Y1,L,U,X,1,X,K1,L1,M1,R1) [B2 >= 2 && W1 >= 2 && U >= 0 && L >= 1 && Y1 >= 1 && N = 0 && E = 1 && Y = 1] (?,1) 65. f21(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f22(B2,Z1,A2,D,E,0,L2,U,X,Y,D1,Q2,L1,P2,R1) [0 >= F2 && 0 >= G2 && 0 >= H2 && 0 >= Y1 && 0 >= I2] (1,1) 67. f7(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,L,Z1,U,X,1 + R1,D1,L,R1,0,R1) [A2 >= 2 && W1 >= 2 && D1 >= 0 && L >= 1 && N = 0 && Y = 1] (?,1) 68. f7(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,L,Z1,U,X,1 + R1,D1,L,R1,0,R1) [A2 >= 2 && W1 >= 2 && D1 >= 0 && 0 >= 1 + L && N = 0 && Y = 1] (?,1) 71. f11(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,L,Z1,U,X,1 + R1,D1,L,R1,0,R1) [A2 >= 2 && W1 >= 2 && X >= 0 && Y >= 0 && L >= 1 && N = 0] (?,1) 72. f11(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,L,Z1,U,X,1 + R1,D1,L,R1,0,R1) [A2 >= 2 && W1 >= 2 && X >= 0 && Y >= 0 && 0 >= 1 + L && N = 0] (?,1) Signature: {(f11,48);(f13,48);(f16,48);(f17,48);(f20,48);(f21,48);(f22,48);(f4,48);(f5,48);(f7,48)} Flow Graph: [0->{17,18,19,20,21,22,23,24},1->{17,18,19,20,21,22,23,24},2->{0,1,2},3->{17,18,19,20,21,22,23,24},4->{17 ,18,19,20,21,22,23,24},5->{17,18,19,20,21,22,23,24},6->{17,18,19,20,21,22,23,24},7->{17,18,19,20,21,22,23 ,24},8->{17,18,19,20,21,22,23,24},9->{17,18,19,20,21,22,23,24},10->{17,18,19,20,21,22,23,24},11->{17,18,19 ,20,21,22,23,24},12->{17,18,19,20,21,22,23,24},13->{17,18,19,20,21,22,23,24},14->{17,18,19,20,21,22,23,24} ,15->{33,34,35,36,37,38,39,40},16->{33,34,35,36,37,38,39,40},17->{15,17,18,19,20,21,22,23,24},18->{15,17,18 ,19,20,21,22,23,24},19->{16,17,18,19,20,21,22,23,24},20->{16,17,18,19,20,21,22,23,24},21->{15,17,18,19,20,21 ,22,23,24},22->{15,17,18,19,20,21,22,23,24},23->{16,17,18,19,20,21,22,23,24},24->{16,17,18,19,20,21,22,23 ,24},25->{33,34,35,36,37,38,39,40},26->{33,34,35,36,37,38,39,40},27->{33,34,35,36,37,38,39,40},28->{33,34,35 ,36,37,38,39,40},29->{33,34,35,36,37,38,39,40},30->{33,34,35,36,37,38,39,40},31->{33,34,35,36,37,38,39,40} ,32->{33,34,35,36,37,38,39,40},33->{33,34,35,36,37,38,39,40,72},34->{33,34,35,36,37,38,39,40,72},35->{33,34 ,35,36,37,38,39,40,71},36->{33,34,35,36,37,38,39,40,71},37->{33,34,35,36,37,38,39,40,72},38->{33,34,35,36,37 ,38,39,40,72},39->{33,34,35,36,37,38,39,40,71},40->{33,34,35,36,37,38,39,40,71},41->{51,52,53,54,55,56,57} ,42->{51,52,53,54,55,56,57,58,59},43->{51,52,53,54,55,56,57,58,59},44->{51,52,53,54,55,56,57,58,59},45->{51 ,52,53,54,55,56,57,58,59},46->{51,52,53,54,55,56,57,58,59},47->{51,52,53,54,55,56,57,58,59},48->{52,53,54,55 ,56,57,58},49->{},50->{},51->{51,52,53,54,55,56,57},52->{51,52,53,54,55,56,57,58,59},53->{51,52,53,54,55,56 ,57,58,59},54->{51,52,53,54,55,56,57,58,59},55->{51,52,53,54,55,56,57,58,59},56->{51,52,53,54,55,56,57,58 ,59},57->{51,52,53,54,55,56,57,58,59},58->{52,53,54,55,56,57,58},59->{},60->{0,1,2},61->{33,34,35,36,37,38 ,39,40},62->{33,34,35,36,37,38,39,40},63->{33,34,35,36,37,38,39,40},64->{33,34,35,36,37,38,39,40},65->{} ,67->{52,53,54,55,56,57,58},68->{51,52,53,54,55,56,57},71->{52,53,54,55,56,57,58},72->{51,52,53,54,55,56 ,57}] + Applied Processor: UnreachableRules + Details: Following transitions are not reachable from the starting states and are revomed: [3 ,4 ,5 ,6 ,7 ,8 ,9 ,10 ,11 ,12 ,13 ,14 ,25 ,26 ,27 ,28 ,29 ,30 ,31 ,32 ,41 ,42 ,43 ,44 ,45 ,46 ,47 ,48 ,49 ,50 ,61 ,62 ,63 ,64 ,67 ,68] * Step 5: FromIts MAYBE + Considered Problem: Rules: 0. f13(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(D,Y1,Z1,D,0,C,C,U,X,Y,D1,K1,L1,M1,R1) [A >= B && A >= 0 && W1 >= 2 && 0 >= 1 + C && X1 >= W1 && D >= W1 && E = 0] (?,1) 1. f13(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(D,Y1,Z1,D,0,C,C,U,X,Y,D1,K1,L1,M1,R1) [A >= B && A >= 0 && W1 >= 2 && C >= 1 && X1 >= W1 && D >= W1 && E = 0] (?,1) 2. f13(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f13(1 + A,B,K,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) [B >= 1 + A && A >= 0] (?,1) 15. f20(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,L,L,U,E,0,D1,K1,L1,M1,R1) [E >= 0 && D >= 0 && W1 >= 2 && 0 >= 1 + L && X = E && N = 0 && Y = 0] (?,1) 16. f20(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,L,L,U,E,0,D1,K1,L1,M1,R1) [E >= 0 && D >= 0 && W1 >= 2 && L >= 1 && X = E && N = 0 && Y = 0] (?,1) 17. f20(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,-1 + D,1 + E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [E >= 0 && D >= 0 && W1 >= 2 && 0 >= 1 + B2 && 0 >= 1 + Y1 && 0 >= 1 + A2] (?,1) 18. f20(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,-1 + D,1 + E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [E >= 0 && D >= 0 && W1 >= 2 && 0 >= 1 + B2 && 0 >= 1 + Y1 && A2 >= 1] (?,1) 19. f20(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,-1 + D,1 + E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [E >= 0 && D >= 0 && W1 >= 2 && 0 >= 1 + B2 && Y1 >= 1 && 0 >= 1 + A2] (?,1) 20. f20(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,-1 + D,1 + E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [E >= 0 && D >= 0 && W1 >= 2 && 0 >= 1 + B2 && Y1 >= 1 && A2 >= 1] (?,1) 21. f20(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,-1 + D,1 + E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [E >= 0 && D >= 0 && W1 >= 2 && B2 >= 1 && 0 >= 1 + Y1 && 0 >= 1 + A2] (?,1) 22. f20(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,-1 + D,1 + E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [E >= 0 && D >= 0 && W1 >= 2 && B2 >= 1 && 0 >= 1 + Y1 && A2 >= 1] (?,1) 23. f20(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,-1 + D,1 + E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [E >= 0 && D >= 0 && W1 >= 2 && B2 >= 1 && Y1 >= 1 && 0 >= 1 + A2] (?,1) 24. f20(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,-1 + D,1 + E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [E >= 0 && D >= 0 && W1 >= 2 && B2 >= 1 && Y1 >= 1 && A2 >= 1] (?,1) 33. f11(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,Y1,N,U,-1 + X,1 + Y,D1,K1,L1,M1,R1) [Y >= 0 && X >= 0 && W1 >= 2 && 0 >= 1 + B2 && 0 >= 1 + Y1 && 0 >= 1 + A2] (?,1) 34. f11(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,Y1,N,U,-1 + X,1 + Y,D1,K1,L1,M1,R1) [Y >= 0 && X >= 0 && W1 >= 2 && 0 >= 1 + B2 && 0 >= 1 + Y1 && A2 >= 1] (?,1) 35. f11(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,Y1,N,U,-1 + X,1 + Y,D1,K1,L1,M1,R1) [Y >= 0 && X >= 0 && W1 >= 2 && 0 >= 1 + B2 && Y1 >= 1 && 0 >= 1 + A2] (?,1) 36. f11(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,Y1,N,U,-1 + X,1 + Y,D1,K1,L1,M1,R1) [Y >= 0 && X >= 0 && W1 >= 2 && 0 >= 1 + B2 && Y1 >= 1 && A2 >= 1] (?,1) 37. f11(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,Y1,N,U,-1 + X,1 + Y,D1,K1,L1,M1,R1) [Y >= 0 && X >= 0 && W1 >= 2 && B2 >= 1 && 0 >= 1 + Y1 && 0 >= 1 + A2] (?,1) 38. f11(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,Y1,N,U,-1 + X,1 + Y,D1,K1,L1,M1,R1) [Y >= 0 && X >= 0 && W1 >= 2 && B2 >= 1 && 0 >= 1 + Y1 && A2 >= 1] (?,1) 39. f11(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,Y1,N,U,-1 + X,1 + Y,D1,K1,L1,M1,R1) [Y >= 0 && X >= 0 && W1 >= 2 && B2 >= 1 && Y1 >= 1 && 0 >= 1 + A2] (?,1) 40. f11(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,Y1,N,U,-1 + X,1 + Y,D1,K1,L1,M1,R1) [Y >= 0 && X >= 0 && W1 >= 2 && B2 >= 1 && Y1 >= 1 && A2 >= 1] (?,1) 51. f5(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,0,-1 + R1) [A2 >= 1 + K1 && R1 >= 0 && W1 >= 2 && Y1 >= 1 + A2 && 0 >= 1 + Y1 && M1 = 0] (?,1) 52. f5(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,0,-1 + R1) [A2 >= 1 + K1 && R1 >= 0 && W1 >= 2 && Y1 >= 1 + A2 && Y1 >= 1 && M1 = 0] (?,1) 53. f5(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,0,-1 + R1) [A2 >= 1 + K1 && R1 >= 0 && W1 >= 2 && A2 >= 1 + Y1 && 0 >= 1 + Y1 && M1 = 0] (?,1) 54. f5(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,0,-1 + R1) [A2 >= 1 + K1 && R1 >= 0 && W1 >= 2 && A2 >= 1 + Y1 && Y1 >= 1 && M1 = 0] (?,1) 55. f5(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,0,-1 + R1) [K1 >= 1 + A2 && R1 >= 0 && W1 >= 2 && Y1 >= 1 + A2 && 0 >= 1 + Y1 && M1 = 0] (?,1) 56. f5(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,0,-1 + R1) [K1 >= 1 + A2 && R1 >= 0 && W1 >= 2 && Y1 >= 1 + A2 && Y1 >= 1 && M1 = 0] (?,1) 57. f5(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,0,-1 + R1) [K1 >= 1 + A2 && R1 >= 0 && W1 >= 2 && A2 >= 1 + Y1 && 0 >= 1 + Y1 && M1 = 0] (?,1) 58. f5(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,0,-1 + R1) [K1 >= 1 + A2 && R1 >= 0 && W1 >= 2 && A2 >= 1 + Y1 && Y1 >= 1 && M1 = 0] (?,1) 59. f5(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f22(A,B,C,D,E,L,N,U,X,Y,D1,D2,L1,C2,R1) [W1 >= 2 && R1 >= 0 && M1 = K1] (?,1) 60. f21(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f13(2,Y1,Z1,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) [Y1 >= 2] (1,1) 65. f21(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f22(B2,Z1,A2,D,E,0,L2,U,X,Y,D1,Q2,L1,P2,R1) [0 >= F2 && 0 >= G2 && 0 >= H2 && 0 >= Y1 && 0 >= I2] (1,1) 71. f11(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,L,Z1,U,X,1 + R1,D1,L,R1,0,R1) [A2 >= 2 && W1 >= 2 && X >= 0 && Y >= 0 && L >= 1 && N = 0] (?,1) 72. f11(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,L,Z1,U,X,1 + R1,D1,L,R1,0,R1) [A2 >= 2 && W1 >= 2 && X >= 0 && Y >= 0 && 0 >= 1 + L && N = 0] (?,1) Signature: {(f11,48);(f13,48);(f16,48);(f17,48);(f20,48);(f21,48);(f22,48);(f4,48);(f5,48);(f7,48)} Flow Graph: [0->{17,18,19,20,21,22,23,24},1->{17,18,19,20,21,22,23,24},2->{0,1,2},15->{33,34,35,36,37,38,39,40} ,16->{33,34,35,36,37,38,39,40},17->{15,17,18,19,20,21,22,23,24},18->{15,17,18,19,20,21,22,23,24},19->{16,17 ,18,19,20,21,22,23,24},20->{16,17,18,19,20,21,22,23,24},21->{15,17,18,19,20,21,22,23,24},22->{15,17,18,19,20 ,21,22,23,24},23->{16,17,18,19,20,21,22,23,24},24->{16,17,18,19,20,21,22,23,24},33->{33,34,35,36,37,38,39,40 ,72},34->{33,34,35,36,37,38,39,40,72},35->{33,34,35,36,37,38,39,40,71},36->{33,34,35,36,37,38,39,40,71} ,37->{33,34,35,36,37,38,39,40,72},38->{33,34,35,36,37,38,39,40,72},39->{33,34,35,36,37,38,39,40,71},40->{33 ,34,35,36,37,38,39,40,71},51->{51,52,53,54,55,56,57},52->{51,52,53,54,55,56,57,58,59},53->{51,52,53,54,55,56 ,57,58,59},54->{51,52,53,54,55,56,57,58,59},55->{51,52,53,54,55,56,57,58,59},56->{51,52,53,54,55,56,57,58 ,59},57->{51,52,53,54,55,56,57,58,59},58->{52,53,54,55,56,57,58},59->{},60->{0,1,2},65->{},71->{52,53,54,55 ,56,57,58},72->{51,52,53,54,55,56,57}] + Applied Processor: FromIts + Details: () * Step 6: AddSinks MAYBE + Considered Problem: Rules: f13(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(D,Y1,Z1,D,0,C,C,U,X,Y,D1,K1,L1,M1,R1) [A >= B && A >= 0 && W1 >= 2 && 0 >= 1 + C && X1 >= W1 && D >= W1 && E = 0] f13(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(D,Y1,Z1,D,0,C,C,U,X,Y,D1,K1,L1,M1,R1) [A >= B && A >= 0 && W1 >= 2 && C >= 1 && X1 >= W1 && D >= W1 && E = 0] f13(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f13(1 + A,B,K,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) [B >= 1 + A && A >= 0] f20(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,L,L,U,E,0,D1,K1,L1,M1,R1) [E >= 0 && D >= 0 && W1 >= 2 && 0 >= 1 + L && X = E && N = 0 && Y = 0] f20(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,L,L,U,E,0,D1,K1,L1,M1,R1) [E >= 0 && D >= 0 && W1 >= 2 && L >= 1 && X = E && N = 0 && Y = 0] f20(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,-1 + D,1 + E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [E >= 0 && D >= 0 && W1 >= 2 && 0 >= 1 + B2 && 0 >= 1 + Y1 && 0 >= 1 + A2] f20(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,-1 + D,1 + E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [E >= 0 && D >= 0 && W1 >= 2 && 0 >= 1 + B2 && 0 >= 1 + Y1 && A2 >= 1] f20(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,-1 + D,1 + E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [E >= 0 && D >= 0 && W1 >= 2 && 0 >= 1 + B2 && Y1 >= 1 && 0 >= 1 + A2] f20(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,-1 + D,1 + E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [E >= 0 && D >= 0 && W1 >= 2 && 0 >= 1 + B2 && Y1 >= 1 && A2 >= 1] f20(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,-1 + D,1 + E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [E >= 0 && D >= 0 && W1 >= 2 && B2 >= 1 && 0 >= 1 + Y1 && 0 >= 1 + A2] f20(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,-1 + D,1 + E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [E >= 0 && D >= 0 && W1 >= 2 && B2 >= 1 && 0 >= 1 + Y1 && A2 >= 1] f20(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,-1 + D,1 + E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [E >= 0 && D >= 0 && W1 >= 2 && B2 >= 1 && Y1 >= 1 && 0 >= 1 + A2] f20(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,-1 + D,1 + E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [E >= 0 && D >= 0 && W1 >= 2 && B2 >= 1 && Y1 >= 1 && A2 >= 1] f11(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,Y1,N,U,-1 + X,1 + Y,D1,K1,L1,M1,R1) [Y >= 0 && X >= 0 && W1 >= 2 && 0 >= 1 + B2 && 0 >= 1 + Y1 && 0 >= 1 + A2] f11(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,Y1,N,U,-1 + X,1 + Y,D1,K1,L1,M1,R1) [Y >= 0 && X >= 0 && W1 >= 2 && 0 >= 1 + B2 && 0 >= 1 + Y1 && A2 >= 1] f11(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,Y1,N,U,-1 + X,1 + Y,D1,K1,L1,M1,R1) [Y >= 0 && X >= 0 && W1 >= 2 && 0 >= 1 + B2 && Y1 >= 1 && 0 >= 1 + A2] f11(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,Y1,N,U,-1 + X,1 + Y,D1,K1,L1,M1,R1) [Y >= 0 && X >= 0 && W1 >= 2 && 0 >= 1 + B2 && Y1 >= 1 && A2 >= 1] f11(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,Y1,N,U,-1 + X,1 + Y,D1,K1,L1,M1,R1) [Y >= 0 && X >= 0 && W1 >= 2 && B2 >= 1 && 0 >= 1 + Y1 && 0 >= 1 + A2] f11(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,Y1,N,U,-1 + X,1 + Y,D1,K1,L1,M1,R1) [Y >= 0 && X >= 0 && W1 >= 2 && B2 >= 1 && 0 >= 1 + Y1 && A2 >= 1] f11(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,Y1,N,U,-1 + X,1 + Y,D1,K1,L1,M1,R1) [Y >= 0 && X >= 0 && W1 >= 2 && B2 >= 1 && Y1 >= 1 && 0 >= 1 + A2] f11(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,Y1,N,U,-1 + X,1 + Y,D1,K1,L1,M1,R1) [Y >= 0 && X >= 0 && W1 >= 2 && B2 >= 1 && Y1 >= 1 && A2 >= 1] f5(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,0,-1 + R1) [A2 >= 1 + K1 && R1 >= 0 && W1 >= 2 && Y1 >= 1 + A2 && 0 >= 1 + Y1 && M1 = 0] f5(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,0,-1 + R1) [A2 >= 1 + K1 && R1 >= 0 && W1 >= 2 && Y1 >= 1 + A2 && Y1 >= 1 && M1 = 0] f5(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,0,-1 + R1) [A2 >= 1 + K1 && R1 >= 0 && W1 >= 2 && A2 >= 1 + Y1 && 0 >= 1 + Y1 && M1 = 0] f5(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,0,-1 + R1) [A2 >= 1 + K1 && R1 >= 0 && W1 >= 2 && A2 >= 1 + Y1 && Y1 >= 1 && M1 = 0] f5(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,0,-1 + R1) [K1 >= 1 + A2 && R1 >= 0 && W1 >= 2 && Y1 >= 1 + A2 && 0 >= 1 + Y1 && M1 = 0] f5(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,0,-1 + R1) [K1 >= 1 + A2 && R1 >= 0 && W1 >= 2 && Y1 >= 1 + A2 && Y1 >= 1 && M1 = 0] f5(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,0,-1 + R1) [K1 >= 1 + A2 && R1 >= 0 && W1 >= 2 && A2 >= 1 + Y1 && 0 >= 1 + Y1 && M1 = 0] f5(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,0,-1 + R1) [K1 >= 1 + A2 && R1 >= 0 && W1 >= 2 && A2 >= 1 + Y1 && Y1 >= 1 && M1 = 0] f5(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f22(A,B,C,D,E,L,N,U,X,Y,D1,D2,L1,C2,R1) [W1 >= 2 && R1 >= 0 && M1 = K1] f21(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f13(2,Y1,Z1,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) [Y1 >= 2] f21(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f22(B2,Z1,A2,D,E,0,L2,U,X,Y,D1,Q2,L1,P2,R1) [0 >= F2 && 0 >= G2 && 0 >= H2 && 0 >= Y1 && 0 >= I2] f11(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,L,Z1,U,X,1 + R1,D1,L,R1,0,R1) [A2 >= 2 && W1 >= 2 && X >= 0 && Y >= 0 && L >= 1 && N = 0] f11(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,L,Z1,U,X,1 + R1,D1,L,R1,0,R1) [A2 >= 2 && W1 >= 2 && X >= 0 && Y >= 0 && 0 >= 1 + L && N = 0] Signature: {(f11,48);(f13,48);(f16,48);(f17,48);(f20,48);(f21,48);(f22,48);(f4,48);(f5,48);(f7,48)} Rule Graph: [0->{17,18,19,20,21,22,23,24},1->{17,18,19,20,21,22,23,24},2->{0,1,2},15->{33,34,35,36,37,38,39,40} ,16->{33,34,35,36,37,38,39,40},17->{15,17,18,19,20,21,22,23,24},18->{15,17,18,19,20,21,22,23,24},19->{16,17 ,18,19,20,21,22,23,24},20->{16,17,18,19,20,21,22,23,24},21->{15,17,18,19,20,21,22,23,24},22->{15,17,18,19,20 ,21,22,23,24},23->{16,17,18,19,20,21,22,23,24},24->{16,17,18,19,20,21,22,23,24},33->{33,34,35,36,37,38,39,40 ,72},34->{33,34,35,36,37,38,39,40,72},35->{33,34,35,36,37,38,39,40,71},36->{33,34,35,36,37,38,39,40,71} ,37->{33,34,35,36,37,38,39,40,72},38->{33,34,35,36,37,38,39,40,72},39->{33,34,35,36,37,38,39,40,71},40->{33 ,34,35,36,37,38,39,40,71},51->{51,52,53,54,55,56,57},52->{51,52,53,54,55,56,57,58,59},53->{51,52,53,54,55,56 ,57,58,59},54->{51,52,53,54,55,56,57,58,59},55->{51,52,53,54,55,56,57,58,59},56->{51,52,53,54,55,56,57,58 ,59},57->{51,52,53,54,55,56,57,58,59},58->{52,53,54,55,56,57,58},59->{},60->{0,1,2},65->{},71->{52,53,54,55 ,56,57,58},72->{51,52,53,54,55,56,57}] + Applied Processor: AddSinks + Details: () * Step 7: Decompose MAYBE + Considered Problem: Rules: f13(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(D,Y1,Z1,D,0,C,C,U,X,Y,D1,K1,L1,M1,R1) [A >= B && A >= 0 && W1 >= 2 && 0 >= 1 + C && X1 >= W1 && D >= W1 && E = 0] f13(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(D,Y1,Z1,D,0,C,C,U,X,Y,D1,K1,L1,M1,R1) [A >= B && A >= 0 && W1 >= 2 && C >= 1 && X1 >= W1 && D >= W1 && E = 0] f13(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f13(1 + A,B,K,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) [B >= 1 + A && A >= 0] f20(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,L,L,U,E,0,D1,K1,L1,M1,R1) [E >= 0 && D >= 0 && W1 >= 2 && 0 >= 1 + L && X = E && N = 0 && Y = 0] f20(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,L,L,U,E,0,D1,K1,L1,M1,R1) [E >= 0 && D >= 0 && W1 >= 2 && L >= 1 && X = E && N = 0 && Y = 0] f20(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,-1 + D,1 + E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [E >= 0 && D >= 0 && W1 >= 2 && 0 >= 1 + B2 && 0 >= 1 + Y1 && 0 >= 1 + A2] f20(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,-1 + D,1 + E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [E >= 0 && D >= 0 && W1 >= 2 && 0 >= 1 + B2 && 0 >= 1 + Y1 && A2 >= 1] f20(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,-1 + D,1 + E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [E >= 0 && D >= 0 && W1 >= 2 && 0 >= 1 + B2 && Y1 >= 1 && 0 >= 1 + A2] f20(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,-1 + D,1 + E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [E >= 0 && D >= 0 && W1 >= 2 && 0 >= 1 + B2 && Y1 >= 1 && A2 >= 1] f20(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,-1 + D,1 + E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [E >= 0 && D >= 0 && W1 >= 2 && B2 >= 1 && 0 >= 1 + Y1 && 0 >= 1 + A2] f20(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,-1 + D,1 + E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [E >= 0 && D >= 0 && W1 >= 2 && B2 >= 1 && 0 >= 1 + Y1 && A2 >= 1] f20(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,-1 + D,1 + E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [E >= 0 && D >= 0 && W1 >= 2 && B2 >= 1 && Y1 >= 1 && 0 >= 1 + A2] f20(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,-1 + D,1 + E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [E >= 0 && D >= 0 && W1 >= 2 && B2 >= 1 && Y1 >= 1 && A2 >= 1] f11(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,Y1,N,U,-1 + X,1 + Y,D1,K1,L1,M1,R1) [Y >= 0 && X >= 0 && W1 >= 2 && 0 >= 1 + B2 && 0 >= 1 + Y1 && 0 >= 1 + A2] f11(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,Y1,N,U,-1 + X,1 + Y,D1,K1,L1,M1,R1) [Y >= 0 && X >= 0 && W1 >= 2 && 0 >= 1 + B2 && 0 >= 1 + Y1 && A2 >= 1] f11(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,Y1,N,U,-1 + X,1 + Y,D1,K1,L1,M1,R1) [Y >= 0 && X >= 0 && W1 >= 2 && 0 >= 1 + B2 && Y1 >= 1 && 0 >= 1 + A2] f11(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,Y1,N,U,-1 + X,1 + Y,D1,K1,L1,M1,R1) [Y >= 0 && X >= 0 && W1 >= 2 && 0 >= 1 + B2 && Y1 >= 1 && A2 >= 1] f11(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,Y1,N,U,-1 + X,1 + Y,D1,K1,L1,M1,R1) [Y >= 0 && X >= 0 && W1 >= 2 && B2 >= 1 && 0 >= 1 + Y1 && 0 >= 1 + A2] f11(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,Y1,N,U,-1 + X,1 + Y,D1,K1,L1,M1,R1) [Y >= 0 && X >= 0 && W1 >= 2 && B2 >= 1 && 0 >= 1 + Y1 && A2 >= 1] f11(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,Y1,N,U,-1 + X,1 + Y,D1,K1,L1,M1,R1) [Y >= 0 && X >= 0 && W1 >= 2 && B2 >= 1 && Y1 >= 1 && 0 >= 1 + A2] f11(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,Y1,N,U,-1 + X,1 + Y,D1,K1,L1,M1,R1) [Y >= 0 && X >= 0 && W1 >= 2 && B2 >= 1 && Y1 >= 1 && A2 >= 1] f5(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,0,-1 + R1) [A2 >= 1 + K1 && R1 >= 0 && W1 >= 2 && Y1 >= 1 + A2 && 0 >= 1 + Y1 && M1 = 0] f5(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,0,-1 + R1) [A2 >= 1 + K1 && R1 >= 0 && W1 >= 2 && Y1 >= 1 + A2 && Y1 >= 1 && M1 = 0] f5(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,0,-1 + R1) [A2 >= 1 + K1 && R1 >= 0 && W1 >= 2 && A2 >= 1 + Y1 && 0 >= 1 + Y1 && M1 = 0] f5(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,0,-1 + R1) [A2 >= 1 + K1 && R1 >= 0 && W1 >= 2 && A2 >= 1 + Y1 && Y1 >= 1 && M1 = 0] f5(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,0,-1 + R1) [K1 >= 1 + A2 && R1 >= 0 && W1 >= 2 && Y1 >= 1 + A2 && 0 >= 1 + Y1 && M1 = 0] f5(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,0,-1 + R1) [K1 >= 1 + A2 && R1 >= 0 && W1 >= 2 && Y1 >= 1 + A2 && Y1 >= 1 && M1 = 0] f5(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,0,-1 + R1) [K1 >= 1 + A2 && R1 >= 0 && W1 >= 2 && A2 >= 1 + Y1 && 0 >= 1 + Y1 && M1 = 0] f5(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,0,-1 + R1) [K1 >= 1 + A2 && R1 >= 0 && W1 >= 2 && A2 >= 1 + Y1 && Y1 >= 1 && M1 = 0] f5(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f22(A,B,C,D,E,L,N,U,X,Y,D1,D2,L1,C2,R1) [W1 >= 2 && R1 >= 0 && M1 = K1] f21(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f13(2,Y1,Z1,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) [Y1 >= 2] f21(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f22(B2,Z1,A2,D,E,0,L2,U,X,Y,D1,Q2,L1,P2,R1) [0 >= F2 && 0 >= G2 && 0 >= H2 && 0 >= Y1 && 0 >= I2] f11(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,L,Z1,U,X,1 + R1,D1,L,R1,0,R1) [A2 >= 2 && W1 >= 2 && X >= 0 && Y >= 0 && L >= 1 && N = 0] f11(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,L,Z1,U,X,1 + R1,D1,L,R1,0,R1) [A2 >= 2 && W1 >= 2 && X >= 0 && Y >= 0 && 0 >= 1 + L && N = 0] f22(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> exitus616(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) True f22(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> exitus616(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) True f22(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> exitus616(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) True f22(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> exitus616(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) True f22(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> exitus616(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) True f22(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> exitus616(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) True f22(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> exitus616(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) True f22(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> exitus616(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) True f22(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> exitus616(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) True Signature: {(exitus616,15);(f11,48);(f13,48);(f16,48);(f17,48);(f20,48);(f21,48);(f22,48);(f4,48);(f5,48);(f7,48)} Rule Graph: [0->{17,18,19,20,21,22,23,24},1->{17,18,19,20,21,22,23,24},2->{0,1,2},15->{33,34,35,36,37,38,39,40} ,16->{33,34,35,36,37,38,39,40},17->{15,17,18,19,20,21,22,23,24},18->{15,17,18,19,20,21,22,23,24},19->{16,17 ,18,19,20,21,22,23,24},20->{16,17,18,19,20,21,22,23,24},21->{15,17,18,19,20,21,22,23,24},22->{15,17,18,19,20 ,21,22,23,24},23->{16,17,18,19,20,21,22,23,24},24->{16,17,18,19,20,21,22,23,24},33->{33,34,35,36,37,38,39,40 ,72},34->{33,34,35,36,37,38,39,40,72},35->{33,34,35,36,37,38,39,40,71},36->{33,34,35,36,37,38,39,40,71} ,37->{33,34,35,36,37,38,39,40,72},38->{33,34,35,36,37,38,39,40,72},39->{33,34,35,36,37,38,39,40,71},40->{33 ,34,35,36,37,38,39,40,71},51->{51,52,53,54,55,56,57},52->{51,52,53,54,55,56,57,58,59},53->{51,52,53,54,55,56 ,57,58,59},54->{51,52,53,54,55,56,57,58,59},55->{51,52,53,54,55,56,57,58,59},56->{51,52,53,54,55,56,57,58 ,59},57->{51,52,53,54,55,56,57,58,59},58->{52,53,54,55,56,57,58},59->{74,75,76,77,78,79,80,81},60->{0,1,2} ,65->{73},71->{52,53,54,55,56,57,58},72->{51,52,53,54,55,56,57}] + Applied Processor: Decompose Greedy + Details: We construct a looptree: P: [0,1,2,15,16,17,18,19,20,21,22,23,24,33,34,35,36,37,38,39,40,51,52,53,54,55,56,57,58,59,60,65,71,72,73,74,75,76,77,78,79,80,81] | +- p:[2] c: [2] | +- p:[17,18,19,20,21,22,23,24] c: [17,18,19,20,21,22,23,24] | +- p:[33,34,35,36,37,38,39,40] c: [33,34,35,36,37,38,39,40] | `- p:[52,51,53,54,55,56,57,58] c: [51,52,53,54,55,56,57,58] * Step 8: AbstractSize MAYBE + Considered Problem: (Rules: f13(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(D,Y1,Z1,D,0,C,C,U,X,Y,D1,K1,L1,M1,R1) [A >= B && A >= 0 && W1 >= 2 && 0 >= 1 + C && X1 >= W1 && D >= W1 && E = 0] f13(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(D,Y1,Z1,D,0,C,C,U,X,Y,D1,K1,L1,M1,R1) [A >= B && A >= 0 && W1 >= 2 && C >= 1 && X1 >= W1 && D >= W1 && E = 0] f13(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f13(1 + A,B,K,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) [B >= 1 + A && A >= 0] f20(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,L,L,U,E,0,D1,K1,L1,M1,R1) [E >= 0 && D >= 0 && W1 >= 2 && 0 >= 1 + L && X = E && N = 0 && Y = 0] f20(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,L,L,U,E,0,D1,K1,L1,M1,R1) [E >= 0 && D >= 0 && W1 >= 2 && L >= 1 && X = E && N = 0 && Y = 0] f20(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,-1 + D,1 + E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [E >= 0 && D >= 0 && W1 >= 2 && 0 >= 1 + B2 && 0 >= 1 + Y1 && 0 >= 1 + A2] f20(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,-1 + D,1 + E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [E >= 0 && D >= 0 && W1 >= 2 && 0 >= 1 + B2 && 0 >= 1 + Y1 && A2 >= 1] f20(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,-1 + D,1 + E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [E >= 0 && D >= 0 && W1 >= 2 && 0 >= 1 + B2 && Y1 >= 1 && 0 >= 1 + A2] f20(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,-1 + D,1 + E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [E >= 0 && D >= 0 && W1 >= 2 && 0 >= 1 + B2 && Y1 >= 1 && A2 >= 1] f20(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,-1 + D,1 + E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [E >= 0 && D >= 0 && W1 >= 2 && B2 >= 1 && 0 >= 1 + Y1 && 0 >= 1 + A2] f20(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,-1 + D,1 + E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [E >= 0 && D >= 0 && W1 >= 2 && B2 >= 1 && 0 >= 1 + Y1 && A2 >= 1] f20(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,-1 + D,1 + E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [E >= 0 && D >= 0 && W1 >= 2 && B2 >= 1 && Y1 >= 1 && 0 >= 1 + A2] f20(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f20(A,B,C,-1 + D,1 + E,Y1,N,U,X,Y,D1,K1,L1,M1,R1) [E >= 0 && D >= 0 && W1 >= 2 && B2 >= 1 && Y1 >= 1 && A2 >= 1] f11(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,Y1,N,U,-1 + X,1 + Y,D1,K1,L1,M1,R1) [Y >= 0 && X >= 0 && W1 >= 2 && 0 >= 1 + B2 && 0 >= 1 + Y1 && 0 >= 1 + A2] f11(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,Y1,N,U,-1 + X,1 + Y,D1,K1,L1,M1,R1) [Y >= 0 && X >= 0 && W1 >= 2 && 0 >= 1 + B2 && 0 >= 1 + Y1 && A2 >= 1] f11(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,Y1,N,U,-1 + X,1 + Y,D1,K1,L1,M1,R1) [Y >= 0 && X >= 0 && W1 >= 2 && 0 >= 1 + B2 && Y1 >= 1 && 0 >= 1 + A2] f11(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,Y1,N,U,-1 + X,1 + Y,D1,K1,L1,M1,R1) [Y >= 0 && X >= 0 && W1 >= 2 && 0 >= 1 + B2 && Y1 >= 1 && A2 >= 1] f11(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,Y1,N,U,-1 + X,1 + Y,D1,K1,L1,M1,R1) [Y >= 0 && X >= 0 && W1 >= 2 && B2 >= 1 && 0 >= 1 + Y1 && 0 >= 1 + A2] f11(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,Y1,N,U,-1 + X,1 + Y,D1,K1,L1,M1,R1) [Y >= 0 && X >= 0 && W1 >= 2 && B2 >= 1 && 0 >= 1 + Y1 && A2 >= 1] f11(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,Y1,N,U,-1 + X,1 + Y,D1,K1,L1,M1,R1) [Y >= 0 && X >= 0 && W1 >= 2 && B2 >= 1 && Y1 >= 1 && 0 >= 1 + A2] f11(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f11(A,B,C,D,E,Y1,N,U,-1 + X,1 + Y,D1,K1,L1,M1,R1) [Y >= 0 && X >= 0 && W1 >= 2 && B2 >= 1 && Y1 >= 1 && A2 >= 1] f5(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,0,-1 + R1) [A2 >= 1 + K1 && R1 >= 0 && W1 >= 2 && Y1 >= 1 + A2 && 0 >= 1 + Y1 && M1 = 0] f5(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,0,-1 + R1) [A2 >= 1 + K1 && R1 >= 0 && W1 >= 2 && Y1 >= 1 + A2 && Y1 >= 1 && M1 = 0] f5(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,0,-1 + R1) [A2 >= 1 + K1 && R1 >= 0 && W1 >= 2 && A2 >= 1 + Y1 && 0 >= 1 + Y1 && M1 = 0] f5(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,0,-1 + R1) [A2 >= 1 + K1 && R1 >= 0 && W1 >= 2 && A2 >= 1 + Y1 && Y1 >= 1 && M1 = 0] f5(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,0,-1 + R1) [K1 >= 1 + A2 && R1 >= 0 && W1 >= 2 && Y1 >= 1 + A2 && 0 >= 1 + Y1 && M1 = 0] f5(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,0,-1 + R1) [K1 >= 1 + A2 && R1 >= 0 && W1 >= 2 && Y1 >= 1 + A2 && Y1 >= 1 && M1 = 0] f5(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,0,-1 + R1) [K1 >= 1 + A2 && R1 >= 0 && W1 >= 2 && A2 >= 1 + Y1 && 0 >= 1 + Y1 && M1 = 0] f5(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,Y1,N,U,X,Y,D1,K1,L1,0,-1 + R1) [K1 >= 1 + A2 && R1 >= 0 && W1 >= 2 && A2 >= 1 + Y1 && Y1 >= 1 && M1 = 0] f5(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f22(A,B,C,D,E,L,N,U,X,Y,D1,D2,L1,C2,R1) [W1 >= 2 && R1 >= 0 && M1 = K1] f21(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f13(2,Y1,Z1,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) [Y1 >= 2] f21(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f22(B2,Z1,A2,D,E,0,L2,U,X,Y,D1,Q2,L1,P2,R1) [0 >= F2 && 0 >= G2 && 0 >= H2 && 0 >= Y1 && 0 >= I2] f11(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,L,Z1,U,X,1 + R1,D1,L,R1,0,R1) [A2 >= 2 && W1 >= 2 && X >= 0 && Y >= 0 && L >= 1 && N = 0] f11(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> f5(A,B,C,D,E,L,Z1,U,X,1 + R1,D1,L,R1,0,R1) [A2 >= 2 && W1 >= 2 && X >= 0 && Y >= 0 && 0 >= 1 + L && N = 0] f22(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> exitus616(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) True f22(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> exitus616(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) True f22(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> exitus616(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) True f22(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> exitus616(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) True f22(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> exitus616(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) True f22(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> exitus616(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) True f22(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> exitus616(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) True f22(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> exitus616(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) True f22(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) -> exitus616(A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1) True Signature: {(exitus616,15);(f11,48);(f13,48);(f16,48);(f17,48);(f20,48);(f21,48);(f22,48);(f4,48);(f5,48);(f7,48)} Rule Graph: [0->{17,18,19,20,21,22,23,24},1->{17,18,19,20,21,22,23,24},2->{0,1,2},15->{33,34,35,36,37,38,39,40} ,16->{33,34,35,36,37,38,39,40},17->{15,17,18,19,20,21,22,23,24},18->{15,17,18,19,20,21,22,23,24},19->{16,17 ,18,19,20,21,22,23,24},20->{16,17,18,19,20,21,22,23,24},21->{15,17,18,19,20,21,22,23,24},22->{15,17,18,19,20 ,21,22,23,24},23->{16,17,18,19,20,21,22,23,24},24->{16,17,18,19,20,21,22,23,24},33->{33,34,35,36,37,38,39,40 ,72},34->{33,34,35,36,37,38,39,40,72},35->{33,34,35,36,37,38,39,40,71},36->{33,34,35,36,37,38,39,40,71} ,37->{33,34,35,36,37,38,39,40,72},38->{33,34,35,36,37,38,39,40,72},39->{33,34,35,36,37,38,39,40,71},40->{33 ,34,35,36,37,38,39,40,71},51->{51,52,53,54,55,56,57},52->{51,52,53,54,55,56,57,58,59},53->{51,52,53,54,55,56 ,57,58,59},54->{51,52,53,54,55,56,57,58,59},55->{51,52,53,54,55,56,57,58,59},56->{51,52,53,54,55,56,57,58 ,59},57->{51,52,53,54,55,56,57,58,59},58->{52,53,54,55,56,57,58},59->{74,75,76,77,78,79,80,81},60->{0,1,2} ,65->{73},71->{52,53,54,55,56,57,58},72->{51,52,53,54,55,56,57}] ,We construct a looptree: P: [0,1,2,15,16,17,18,19,20,21,22,23,24,33,34,35,36,37,38,39,40,51,52,53,54,55,56,57,58,59,60,65,71,72,73,74,75,76,77,78,79,80,81] | +- p:[2] c: [2] | +- p:[17,18,19,20,21,22,23,24] c: [17,18,19,20,21,22,23,24] | +- p:[33,34,35,36,37,38,39,40] c: [33,34,35,36,37,38,39,40] | `- p:[52,51,53,54,55,56,57,58] c: [51,52,53,54,55,56,57,58]) + Applied Processor: AbstractSize Minimize + Details: () * Step 9: AbstractFlow MAYBE + Considered Problem: Program: Domain: [A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1,0.0,0.1,0.2,0.3] f13 ~> f20 [A <= D, B <= unknown, C <= unknown, D <= D, E <= 0*K, L <= C, N <= C, U <= U, X <= X, Y <= Y, D1 <= D1, K1 <= K1, L1 <= L1, M1 <= M1, R1 <= R1] f13 ~> f20 [A <= D, B <= unknown, C <= unknown, D <= D, E <= 0*K, L <= C, N <= C, U <= U, X <= X, Y <= Y, D1 <= D1, K1 <= K1, L1 <= L1, M1 <= M1, R1 <= R1] f13 ~> f13 [A <= B, B <= B, C <= unknown, D <= D, E <= E, L <= L, N <= N, U <= U, X <= X, Y <= Y, D1 <= D1, K1 <= K1, L1 <= L1, M1 <= M1, R1 <= R1] f20 ~> f11 [A <= A, B <= B, C <= C, D <= D, E <= E, L <= L, N <= L, U <= U, X <= E, Y <= 0*K, D1 <= D1, K1 <= K1, L1 <= L1, M1 <= M1, R1 <= R1] f20 ~> f11 [A <= A, B <= B, C <= C, D <= D, E <= E, L <= L, N <= L, U <= U, X <= E, Y <= 0*K, D1 <= D1, K1 <= K1, L1 <= L1, M1 <= M1, R1 <= R1] f20 ~> f20 [A <= A, B <= B, C <= C, D <= K + D, E <= K + E, L <= unknown, N <= N, U <= U, X <= X, Y <= Y, D1 <= D1, K1 <= K1, L1 <= L1, M1 <= M1, R1 <= R1] f20 ~> f20 [A <= A, B <= B, C <= C, D <= K + D, E <= K + E, L <= unknown, N <= N, U <= U, X <= X, Y <= Y, D1 <= D1, K1 <= K1, L1 <= L1, M1 <= M1, R1 <= R1] f20 ~> f20 [A <= A, B <= B, C <= C, D <= K + D, E <= K + E, L <= unknown, N <= N, U <= U, X <= X, Y <= Y, D1 <= D1, K1 <= K1, L1 <= L1, M1 <= M1, R1 <= R1] f20 ~> f20 [A <= A, B <= B, C <= C, D <= K + D, E <= K + E, L <= unknown, N <= N, U <= U, X <= X, Y <= Y, D1 <= D1, K1 <= K1, L1 <= L1, M1 <= M1, R1 <= R1] f20 ~> f20 [A <= A, B <= B, C <= C, D <= K + D, E <= K + E, L <= unknown, N <= N, U <= U, X <= X, Y <= Y, D1 <= D1, K1 <= K1, L1 <= L1, M1 <= M1, R1 <= R1] f20 ~> f20 [A <= A, B <= B, C <= C, D <= K + D, E <= K + E, L <= unknown, N <= N, U <= U, X <= X, Y <= Y, D1 <= D1, K1 <= K1, L1 <= L1, M1 <= M1, R1 <= R1] f20 ~> f20 [A <= A, B <= B, C <= C, D <= K + D, E <= K + E, L <= unknown, N <= N, U <= U, X <= X, Y <= Y, D1 <= D1, K1 <= K1, L1 <= L1, M1 <= M1, R1 <= R1] f20 ~> f20 [A <= A, B <= B, C <= C, D <= K + D, E <= K + E, L <= unknown, N <= N, U <= U, X <= X, Y <= Y, D1 <= D1, K1 <= K1, L1 <= L1, M1 <= M1, R1 <= R1] f11 ~> f11 [A <= A, B <= B, C <= C, D <= D, E <= E, L <= unknown, N <= N, U <= U, X <= K + X, Y <= K + Y, D1 <= D1, K1 <= K1, L1 <= L1, M1 <= M1, R1 <= R1] f11 ~> f11 [A <= A, B <= B, C <= C, D <= D, E <= E, L <= unknown, N <= N, U <= U, X <= K + X, Y <= K + Y, D1 <= D1, K1 <= K1, L1 <= L1, M1 <= M1, R1 <= R1] f11 ~> f11 [A <= A, B <= B, C <= C, D <= D, E <= E, L <= unknown, N <= N, U <= U, X <= K + X, Y <= K + Y, D1 <= D1, K1 <= K1, L1 <= L1, M1 <= M1, R1 <= R1] f11 ~> f11 [A <= A, B <= B, C <= C, D <= D, E <= E, L <= unknown, N <= N, U <= U, X <= K + X, Y <= K + Y, D1 <= D1, K1 <= K1, L1 <= L1, M1 <= M1, R1 <= R1] f11 ~> f11 [A <= A, B <= B, C <= C, D <= D, E <= E, L <= unknown, N <= N, U <= U, X <= K + X, Y <= K + Y, D1 <= D1, K1 <= K1, L1 <= L1, M1 <= M1, R1 <= R1] f11 ~> f11 [A <= A, B <= B, C <= C, D <= D, E <= E, L <= unknown, N <= N, U <= U, X <= K + X, Y <= K + Y, D1 <= D1, K1 <= K1, L1 <= L1, M1 <= M1, R1 <= R1] f11 ~> f11 [A <= A, B <= B, C <= C, D <= D, E <= E, L <= unknown, N <= N, U <= U, X <= K + X, Y <= K + Y, D1 <= D1, K1 <= K1, L1 <= L1, M1 <= M1, R1 <= R1] f11 ~> f11 [A <= A, B <= B, C <= C, D <= D, E <= E, L <= unknown, N <= N, U <= U, X <= K + X, Y <= K + Y, D1 <= D1, K1 <= K1, L1 <= L1, M1 <= M1, R1 <= R1] f5 ~> f5 [A <= A, B <= B, C <= C, D <= D, E <= E, L <= K1, N <= N, U <= U, X <= X, Y <= Y, D1 <= D1, K1 <= K1, L1 <= L1, M1 <= 0*K, R1 <= K + R1] f5 ~> f5 [A <= A, B <= B, C <= C, D <= D, E <= E, L <= unknown, N <= N, U <= U, X <= X, Y <= Y, D1 <= D1, K1 <= K1, L1 <= L1, M1 <= 0*K, R1 <= K + R1] f5 ~> f5 [A <= A, B <= B, C <= C, D <= D, E <= E, L <= unknown, N <= N, U <= U, X <= X, Y <= Y, D1 <= D1, K1 <= K1, L1 <= L1, M1 <= 0*K, R1 <= K + R1] f5 ~> f5 [A <= A, B <= B, C <= C, D <= D, E <= E, L <= unknown, N <= N, U <= U, X <= X, Y <= Y, D1 <= D1, K1 <= K1, L1 <= L1, M1 <= 0*K, R1 <= K + R1] f5 ~> f5 [A <= A, B <= B, C <= C, D <= D, E <= E, L <= unknown, N <= N, U <= U, X <= X, Y <= Y, D1 <= D1, K1 <= K1, L1 <= L1, M1 <= 0*K, R1 <= K + R1] f5 ~> f5 [A <= A, B <= B, C <= C, D <= D, E <= E, L <= unknown, N <= N, U <= U, X <= X, Y <= Y, D1 <= D1, K1 <= K1, L1 <= L1, M1 <= 0*K, R1 <= K + R1] f5 ~> f5 [A <= A, B <= B, C <= C, D <= D, E <= E, L <= unknown, N <= N, U <= U, X <= X, Y <= Y, D1 <= D1, K1 <= K1, L1 <= L1, M1 <= 0*K, R1 <= K + R1] f5 ~> f5 [A <= A, B <= B, C <= C, D <= D, E <= E, L <= K1, N <= N, U <= U, X <= X, Y <= Y, D1 <= D1, K1 <= K1, L1 <= L1, M1 <= 0*K, R1 <= K + R1] f5 ~> f22 [A <= A, B <= B, C <= C, D <= D, E <= E, L <= L, N <= N, U <= U, X <= X, Y <= Y, D1 <= D1, K1 <= unknown, L1 <= L1, M1 <= unknown, R1 <= R1] f21 ~> f13 [A <= 2*K, B <= unknown, C <= unknown, D <= D, E <= E, L <= L, N <= N, U <= U, X <= X, Y <= Y, D1 <= D1, K1 <= K1, L1 <= L1, M1 <= M1, R1 <= R1] f21 ~> f22 [A <= unknown, B <= unknown, C <= unknown, D <= D, E <= E, L <= 0*K, N <= unknown, U <= U, X <= X, Y <= Y, D1 <= D1, K1 <= unknown, L1 <= L1, M1 <= unknown, R1 <= R1] f11 ~> f5 [A <= A, B <= B, C <= C, D <= D, E <= E, L <= L, N <= unknown, U <= U, X <= X, Y <= K + R1, D1 <= D1, K1 <= L, L1 <= R1, M1 <= 0*K, R1 <= R1] f11 ~> f5 [A <= A, B <= B, C <= C, D <= D, E <= E, L <= L, N <= unknown, U <= U, X <= X, Y <= K + R1, D1 <= D1, K1 <= L, L1 <= R1, M1 <= 0*K, R1 <= R1] f22 ~> exitus616 [A <= A, B <= B, C <= C, D <= D, E <= E, L <= L, N <= N, U <= U, X <= X, Y <= Y, D1 <= D1, K1 <= K1, L1 <= L1, M1 <= M1, R1 <= R1] f22 ~> exitus616 [A <= A, B <= B, C <= C, D <= D, E <= E, L <= L, N <= N, U <= U, X <= X, Y <= Y, D1 <= D1, K1 <= K1, L1 <= L1, M1 <= M1, R1 <= R1] f22 ~> exitus616 [A <= A, B <= B, C <= C, D <= D, E <= E, L <= L, N <= N, U <= U, X <= X, Y <= Y, D1 <= D1, K1 <= K1, L1 <= L1, M1 <= M1, R1 <= R1] f22 ~> exitus616 [A <= A, B <= B, C <= C, D <= D, E <= E, L <= L, N <= N, U <= U, X <= X, Y <= Y, D1 <= D1, K1 <= K1, L1 <= L1, M1 <= M1, R1 <= R1] f22 ~> exitus616 [A <= A, B <= B, C <= C, D <= D, E <= E, L <= L, N <= N, U <= U, X <= X, Y <= Y, D1 <= D1, K1 <= K1, L1 <= L1, M1 <= M1, R1 <= R1] f22 ~> exitus616 [A <= A, B <= B, C <= C, D <= D, E <= E, L <= L, N <= N, U <= U, X <= X, Y <= Y, D1 <= D1, K1 <= K1, L1 <= L1, M1 <= M1, R1 <= R1] f22 ~> exitus616 [A <= A, B <= B, C <= C, D <= D, E <= E, L <= L, N <= N, U <= U, X <= X, Y <= Y, D1 <= D1, K1 <= K1, L1 <= L1, M1 <= M1, R1 <= R1] f22 ~> exitus616 [A <= A, B <= B, C <= C, D <= D, E <= E, L <= L, N <= N, U <= U, X <= X, Y <= Y, D1 <= D1, K1 <= K1, L1 <= L1, M1 <= M1, R1 <= R1] f22 ~> exitus616 [A <= A, B <= B, C <= C, D <= D, E <= E, L <= L, N <= N, U <= U, X <= X, Y <= Y, D1 <= D1, K1 <= K1, L1 <= L1, M1 <= M1, R1 <= R1] + Loop: [0.0 <= K + A + B] f13 ~> f13 [A <= B, B <= B, C <= unknown, D <= D, E <= E, L <= L, N <= N, U <= U, X <= X, Y <= Y, D1 <= D1, K1 <= K1, L1 <= L1, M1 <= M1, R1 <= R1] + Loop: [0.1 <= D] f20 ~> f20 [A <= A, B <= B, C <= C, D <= K + D, E <= K + E, L <= unknown, N <= N, U <= U, X <= X, Y <= Y, D1 <= D1, K1 <= K1, L1 <= L1, M1 <= M1, R1 <= R1] f20 ~> f20 [A <= A, B <= B, C <= C, D <= K + D, E <= K + E, L <= unknown, N <= N, U <= U, X <= X, Y <= Y, D1 <= D1, K1 <= K1, L1 <= L1, M1 <= M1, R1 <= R1] f20 ~> f20 [A <= A, B <= B, C <= C, D <= K + D, E <= K + E, L <= unknown, N <= N, U <= U, X <= X, Y <= Y, D1 <= D1, K1 <= K1, L1 <= L1, M1 <= M1, R1 <= R1] f20 ~> f20 [A <= A, B <= B, C <= C, D <= K + D, E <= K + E, L <= unknown, N <= N, U <= U, X <= X, Y <= Y, D1 <= D1, K1 <= K1, L1 <= L1, M1 <= M1, R1 <= R1] f20 ~> f20 [A <= A, B <= B, C <= C, D <= K + D, E <= K + E, L <= unknown, N <= N, U <= U, X <= X, Y <= Y, D1 <= D1, K1 <= K1, L1 <= L1, M1 <= M1, R1 <= R1] f20 ~> f20 [A <= A, B <= B, C <= C, D <= K + D, E <= K + E, L <= unknown, N <= N, U <= U, X <= X, Y <= Y, D1 <= D1, K1 <= K1, L1 <= L1, M1 <= M1, R1 <= R1] f20 ~> f20 [A <= A, B <= B, C <= C, D <= K + D, E <= K + E, L <= unknown, N <= N, U <= U, X <= X, Y <= Y, D1 <= D1, K1 <= K1, L1 <= L1, M1 <= M1, R1 <= R1] f20 ~> f20 [A <= A, B <= B, C <= C, D <= K + D, E <= K + E, L <= unknown, N <= N, U <= U, X <= X, Y <= Y, D1 <= D1, K1 <= K1, L1 <= L1, M1 <= M1, R1 <= R1] + Loop: [0.2 <= X] f11 ~> f11 [A <= A, B <= B, C <= C, D <= D, E <= E, L <= unknown, N <= N, U <= U, X <= K + X, Y <= K + Y, D1 <= D1, K1 <= K1, L1 <= L1, M1 <= M1, R1 <= R1] f11 ~> f11 [A <= A, B <= B, C <= C, D <= D, E <= E, L <= unknown, N <= N, U <= U, X <= K + X, Y <= K + Y, D1 <= D1, K1 <= K1, L1 <= L1, M1 <= M1, R1 <= R1] f11 ~> f11 [A <= A, B <= B, C <= C, D <= D, E <= E, L <= unknown, N <= N, U <= U, X <= K + X, Y <= K + Y, D1 <= D1, K1 <= K1, L1 <= L1, M1 <= M1, R1 <= R1] f11 ~> f11 [A <= A, B <= B, C <= C, D <= D, E <= E, L <= unknown, N <= N, U <= U, X <= K + X, Y <= K + Y, D1 <= D1, K1 <= K1, L1 <= L1, M1 <= M1, R1 <= R1] f11 ~> f11 [A <= A, B <= B, C <= C, D <= D, E <= E, L <= unknown, N <= N, U <= U, X <= K + X, Y <= K + Y, D1 <= D1, K1 <= K1, L1 <= L1, M1 <= M1, R1 <= R1] f11 ~> f11 [A <= A, B <= B, C <= C, D <= D, E <= E, L <= unknown, N <= N, U <= U, X <= K + X, Y <= K + Y, D1 <= D1, K1 <= K1, L1 <= L1, M1 <= M1, R1 <= R1] f11 ~> f11 [A <= A, B <= B, C <= C, D <= D, E <= E, L <= unknown, N <= N, U <= U, X <= K + X, Y <= K + Y, D1 <= D1, K1 <= K1, L1 <= L1, M1 <= M1, R1 <= R1] f11 ~> f11 [A <= A, B <= B, C <= C, D <= D, E <= E, L <= unknown, N <= N, U <= U, X <= K + X, Y <= K + Y, D1 <= D1, K1 <= K1, L1 <= L1, M1 <= M1, R1 <= R1] + Loop: [0.3 <= R1] f5 ~> f5 [A <= A, B <= B, C <= C, D <= D, E <= E, L <= unknown, N <= N, U <= U, X <= X, Y <= Y, D1 <= D1, K1 <= K1, L1 <= L1, M1 <= 0*K, R1 <= K + R1] f5 ~> f5 [A <= A, B <= B, C <= C, D <= D, E <= E, L <= K1, N <= N, U <= U, X <= X, Y <= Y, D1 <= D1, K1 <= K1, L1 <= L1, M1 <= 0*K, R1 <= K + R1] f5 ~> f5 [A <= A, B <= B, C <= C, D <= D, E <= E, L <= unknown, N <= N, U <= U, X <= X, Y <= Y, D1 <= D1, K1 <= K1, L1 <= L1, M1 <= 0*K, R1 <= K + R1] f5 ~> f5 [A <= A, B <= B, C <= C, D <= D, E <= E, L <= unknown, N <= N, U <= U, X <= X, Y <= Y, D1 <= D1, K1 <= K1, L1 <= L1, M1 <= 0*K, R1 <= K + R1] f5 ~> f5 [A <= A, B <= B, C <= C, D <= D, E <= E, L <= unknown, N <= N, U <= U, X <= X, Y <= Y, D1 <= D1, K1 <= K1, L1 <= L1, M1 <= 0*K, R1 <= K + R1] f5 ~> f5 [A <= A, B <= B, C <= C, D <= D, E <= E, L <= unknown, N <= N, U <= U, X <= X, Y <= Y, D1 <= D1, K1 <= K1, L1 <= L1, M1 <= 0*K, R1 <= K + R1] f5 ~> f5 [A <= A, B <= B, C <= C, D <= D, E <= E, L <= unknown, N <= N, U <= U, X <= X, Y <= Y, D1 <= D1, K1 <= K1, L1 <= L1, M1 <= 0*K, R1 <= K + R1] f5 ~> f5 [A <= A, B <= B, C <= C, D <= D, E <= E, L <= K1, N <= N, U <= U, X <= X, Y <= Y, D1 <= D1, K1 <= K1, L1 <= L1, M1 <= 0*K, R1 <= K + R1] + Applied Processor: AbstractFlow + Details: () * Step 10: Failure MAYBE + Considered Problem: Program: Domain: [tick,huge,K,A,B,C,D,E,L,N,U,X,Y,D1,K1,L1,M1,R1,0.0,0.1,0.2,0.3] f13 ~> f20 [C ~=> L,C ~=> N,D ~=> A,K ~=> E,huge ~=> B,huge ~=> C] f13 ~> f20 [C ~=> L,C ~=> N,D ~=> A,K ~=> E,huge ~=> B,huge ~=> C] f13 ~> f13 [B ~=> A,huge ~=> C] f20 ~> f11 [E ~=> X,L ~=> N,K ~=> Y] f20 ~> f11 [E ~=> X,L ~=> N,K ~=> Y] f20 ~> f20 [huge ~=> L,D ~+> D,E ~+> E,K ~+> D,K ~+> E] f20 ~> f20 [huge ~=> L,D ~+> D,E ~+> E,K ~+> D,K ~+> E] f20 ~> f20 [huge ~=> L,D ~+> D,E ~+> E,K ~+> D,K ~+> E] f20 ~> f20 [huge ~=> L,D ~+> D,E ~+> E,K ~+> D,K ~+> E] f20 ~> f20 [huge ~=> L,D ~+> D,E ~+> E,K ~+> D,K ~+> E] f20 ~> f20 [huge ~=> L,D ~+> D,E ~+> E,K ~+> D,K ~+> E] f20 ~> f20 [huge ~=> L,D ~+> D,E ~+> E,K ~+> D,K ~+> E] f20 ~> f20 [huge ~=> L,D ~+> D,E ~+> E,K ~+> D,K ~+> E] f11 ~> f11 [huge ~=> L,X ~+> X,Y ~+> Y,K ~+> X,K ~+> Y] f11 ~> f11 [huge ~=> L,X ~+> X,Y ~+> Y,K ~+> X,K ~+> Y] f11 ~> f11 [huge ~=> L,X ~+> X,Y ~+> Y,K ~+> X,K ~+> Y] f11 ~> f11 [huge ~=> L,X ~+> X,Y ~+> Y,K ~+> X,K ~+> Y] f11 ~> f11 [huge ~=> L,X ~+> X,Y ~+> Y,K ~+> X,K ~+> Y] f11 ~> f11 [huge ~=> L,X ~+> X,Y ~+> Y,K ~+> X,K ~+> Y] f11 ~> f11 [huge ~=> L,X ~+> X,Y ~+> Y,K ~+> X,K ~+> Y] f11 ~> f11 [huge ~=> L,X ~+> X,Y ~+> Y,K ~+> X,K ~+> Y] f5 ~> f5 [K1 ~=> L,K ~=> M1,R1 ~+> R1,K ~+> R1] f5 ~> f5 [K ~=> M1,huge ~=> L,R1 ~+> R1,K ~+> R1] f5 ~> f5 [K ~=> M1,huge ~=> L,R1 ~+> R1,K ~+> R1] f5 ~> f5 [K ~=> M1,huge ~=> L,R1 ~+> R1,K ~+> R1] f5 ~> f5 [K ~=> M1,huge ~=> L,R1 ~+> R1,K ~+> R1] f5 ~> f5 [K ~=> M1,huge ~=> L,R1 ~+> R1,K ~+> R1] f5 ~> f5 [K ~=> M1,huge ~=> L,R1 ~+> R1,K ~+> R1] f5 ~> f5 [K1 ~=> L,K ~=> M1,R1 ~+> R1,K ~+> R1] f5 ~> f22 [huge ~=> K1,huge ~=> M1] f21 ~> f13 [K ~=> A,huge ~=> B,huge ~=> C] f21 ~> f22 [K ~=> L,huge ~=> A,huge ~=> B,huge ~=> C,huge ~=> K1,huge ~=> M1,huge ~=> N] f11 ~> f5 [L ~=> K1,R1 ~=> L1,K ~=> M1,huge ~=> N,R1 ~+> Y,K ~+> Y] f11 ~> f5 [L ~=> K1,R1 ~=> L1,K ~=> M1,huge ~=> N,R1 ~+> Y,K ~+> Y] f22 ~> exitus616 [] f22 ~> exitus616 [] f22 ~> exitus616 [] f22 ~> exitus616 [] f22 ~> exitus616 [] f22 ~> exitus616 [] f22 ~> exitus616 [] f22 ~> exitus616 [] f22 ~> exitus616 [] + Loop: [A ~+> 0.0,B ~+> 0.0,K ~+> 0.0] f13 ~> f13 [B ~=> A,huge ~=> C] + Loop: [D ~=> 0.1] f20 ~> f20 [huge ~=> L,D ~+> D,E ~+> E,K ~+> D,K ~+> E] f20 ~> f20 [huge ~=> L,D ~+> D,E ~+> E,K ~+> D,K ~+> E] f20 ~> f20 [huge ~=> L,D ~+> D,E ~+> E,K ~+> D,K ~+> E] f20 ~> f20 [huge ~=> L,D ~+> D,E ~+> E,K ~+> D,K ~+> E] f20 ~> f20 [huge ~=> L,D ~+> D,E ~+> E,K ~+> D,K ~+> E] f20 ~> f20 [huge ~=> L,D ~+> D,E ~+> E,K ~+> D,K ~+> E] f20 ~> f20 [huge ~=> L,D ~+> D,E ~+> E,K ~+> D,K ~+> E] f20 ~> f20 [huge ~=> L,D ~+> D,E ~+> E,K ~+> D,K ~+> E] + Loop: [X ~=> 0.2] f11 ~> f11 [huge ~=> L,X ~+> X,Y ~+> Y,K ~+> X,K ~+> Y] f11 ~> f11 [huge ~=> L,X ~+> X,Y ~+> Y,K ~+> X,K ~+> Y] f11 ~> f11 [huge ~=> L,X ~+> X,Y ~+> Y,K ~+> X,K ~+> Y] f11 ~> f11 [huge ~=> L,X ~+> X,Y ~+> Y,K ~+> X,K ~+> Y] f11 ~> f11 [huge ~=> L,X ~+> X,Y ~+> Y,K ~+> X,K ~+> Y] f11 ~> f11 [huge ~=> L,X ~+> X,Y ~+> Y,K ~+> X,K ~+> Y] f11 ~> f11 [huge ~=> L,X ~+> X,Y ~+> Y,K ~+> X,K ~+> Y] f11 ~> f11 [huge ~=> L,X ~+> X,Y ~+> Y,K ~+> X,K ~+> Y] + Loop: [R1 ~=> 0.3] f5 ~> f5 [K ~=> M1,huge ~=> L,R1 ~+> R1,K ~+> R1] f5 ~> f5 [K1 ~=> L,K ~=> M1,R1 ~+> R1,K ~+> R1] f5 ~> f5 [K ~=> M1,huge ~=> L,R1 ~+> R1,K ~+> R1] f5 ~> f5 [K ~=> M1,huge ~=> L,R1 ~+> R1,K ~+> R1] f5 ~> f5 [K ~=> M1,huge ~=> L,R1 ~+> R1,K ~+> R1] f5 ~> f5 [K ~=> M1,huge ~=> L,R1 ~+> R1,K ~+> R1] f5 ~> f5 [K ~=> M1,huge ~=> L,R1 ~+> R1,K ~+> R1] f5 ~> f5 [K1 ~=> L,K ~=> M1,R1 ~+> R1,K ~+> R1] + Applied Processor: Lare + Details: Unknown bound. MAYBE