MAYBE * Step 1: ArgumentFilter MAYBE + Considered Problem: Rules: 0. f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f16(R1,P1,Q1,D,E,O1,S1,T1,U1,N1,Y1,0,Z1,A2,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,F2,C1,E2,B2,C2,D2,G2,I1,J1,M1,L1) [0 >= V1 && 0 >= W1 && 0 >= O1 && 0 >= X1] (1,1) 1. f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f1(2,O1,P1,D,E,O1,G,H,P1,P1,Q1,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,M1,R1) [O1 >= 2] (1,1) 2. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f1(1 + A,B,K,D,E,F,G,H,I,K,M1,L,M,N,O,O1,A,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) [-2 + F >= 0 && -4 + A + F >= 0 && -2 + A >= 0 && B >= 1 + A && A >= 0] (?,1) 3. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(D,O1,P1,D,0,M1,Q1,R1,S1,T1,U1,C,C,C,N1,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) [-2 + F >= 0 (?,1) && -4 + A + F >= 0 && -2 + A >= 0 && A >= B && A >= 0 && M1 >= 2 && C >= 1 && N1 >= M1 && D >= M1 && E = 0] 4. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f14(D,O1,P1,D,0,M1,Q1,R1,S1,T1,U1,C,C,C,N1,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) [-2 + F >= 0 (?,1) && -4 + A + F >= 0 && -2 + A >= 0 && A >= B && A >= 0 && M1 >= 2 && 0 >= 1 + C && N1 >= M1 && D >= M1 && E = 0] 5. f14(A,B,C,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) -> f14(A,B,C,-1 + D,1 + E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,S,T,U,V,W,N,Q1,1 + E,-1 + D,B1,C1,D1,E1,F1,G1,H1,I1[-2 + F >= 0 (?,1) ,J1,K1,L1) && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && D >= 0 && M1 >= 2 && R1 >= 1 && O1 >= 1 && Q1 >= 1] 6. f14(A,B,C,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) -> f14(A,B,C,-1 + D,1 + E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,S,T,U,V,W,N,Q1,1 + E,-1 + D,B1,C1,D1,E1,F1,G1,H1,I1[-2 + F >= 0 (?,1) ,J1,K1,L1) && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && D >= 0 && M1 >= 2 && R1 >= 1 && O1 >= 1 && 0 >= 1 + Q1] 7. f14(A,B,C,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) -> f14(A,B,C,-1 + D,1 + E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,S,T,U,V,W,N,Q1,1 + E,-1 + D,B1,C1,D1,E1,F1,G1,H1,I1[-2 + F >= 0 (?,1) ,J1,K1,L1) && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && D >= 0 && M1 >= 2 && R1 >= 1 && 0 >= 1 + O1 && Q1 >= 1] 8. f14(A,B,C,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) -> f14(A,B,C,-1 + D,1 + E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,S,T,U,V,W,N,Q1,1 + E,-1 + D,B1,C1,D1,E1,F1,G1,H1,I1[-2 + F >= 0 (?,1) ,J1,K1,L1) && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && D >= 0 && M1 >= 2 && R1 >= 1 && 0 >= 1 + O1 && 0 >= 1 + Q1] 9. f14(A,B,C,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) -> f14(A,B,C,-1 + D,1 + E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,S,T,U,V,W,N,Q1,1 + E,-1 + D,B1,C1,D1,E1,F1,G1,H1,I1[-2 + F >= 0 (?,1) ,J1,K1,L1) && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && D >= 0 && M1 >= 2 && 0 >= 1 + R1 && O1 >= 1 && Q1 >= 1] 10. f14(A,B,C,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) -> f14(A,B,C,-1 + D,1 + E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,S,T,U,V,W,N,Q1,1 + E,-1 + D,B1,C1,D1,E1,F1,G1,H1,I1[-2 + F >= 0 (?,1) ,J1,K1,L1) && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && D >= 0 && M1 >= 2 && 0 >= 1 + R1 && O1 >= 1 && 0 >= 1 + Q1] 11. f14(A,B,C,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) -> f14(A,B,C,-1 + D,1 + E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,S,T,U,V,W,N,Q1,1 + E,-1 + D,B1,C1,D1,E1,F1,G1,H1,I1[-2 + F >= 0 (?,1) ,J1,K1,L1) && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && D >= 0 && M1 >= 2 && 0 >= 1 + R1 && 0 >= 1 + O1 && Q1 >= 1] 12. f14(A,B,C,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) -> f14(A,B,C,-1 + D,1 + E,M1,G,H,I,J,K,O1,O1,N,O,P,Q,P1,S,T,U,V,W,N,Q1,1 + E,-1 + D,B1,C1,D1,E1,F1,G1,H1,I1[-2 + F >= 0 (?,1) ,J1,K1,L1) && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && D >= 0 && M1 >= 2 && 0 >= 1 + R1 && 0 >= 1 + O1 && 0 >= 1 + Q1] 13. f14(A,B,C,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) -> f8(A,B,C,D,1 + I1,M1,G,H,I,J,K,L,O1,P1,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,L,I1,0,L,0,L,L,I1,J1,K1,L1) [-2 + F >= 0 (?,1) && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && Q1 >= 2 && M1 >= 2 && D >= 0 && L >= 1 && N = 0] 14. f14(A,B,C,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) -> f8(A,B,C,D,1 + I1,M1,G,H,I,J,K,L,O1,P1,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,L,I1,0,L,0,L,L,I1,J1,K1,L1) [-2 + F >= 0 (?,1) && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && Q1 >= 2 && M1 >= 2 && D >= 0 && 0 >= 1 + L && N = 0] 15. f8(A,B,C,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) -> f8(A,B,C,D,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,P1,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,-1 + I1,-1 + I1,K1,L1) [-2 + F >= 0 (?,1) && -2 + D + F >= 0 && -2 + F + F1 >= 0 && -2 + F + -1*F1 >= 0 && -2 + D1 + F >= 0 && -2 + -1*D1 + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && 1 + C1 + -1*E >= 0 && -1 + E + -1*I1 >= 0 && -1 + -1*C1 + E >= 0 && A + -1*D >= 0 && D >= 0 && D + F1 >= 0 && D + -1*F1 >= 0 && D + D1 >= 0 && D + -1*D1 >= 0 && -2 + D + O >= 0 && -2 + A + D >= 0 && C1 + -1*I1 >= 0 && B1 + -1*H1 >= 0 && -1*B1 + H1 >= 0 && -1*F1 >= 0 && D1 + -1*F1 >= 0 && -1*D1 + -1*F1 >= 0 && -2 + -1*F1 + O >= 0 && -2 + A + -1*F1 >= 0 && F1 >= 0 && D1 + F1 >= 0 && -1*D1 + F1 >= 0 && -2 + F1 + O >= 0 && -2 + A + F1 >= 0 && -1*D1 >= 0 && -2 + -1*D1 + O >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + D1 + O >= 0 && -2 + A + D1 >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && B1 >= 1 + Q1 && I1 >= 0 && M1 >= 2 && Q1 >= 1 + O1 && 0 >= 1 + O1 && D1 = 0] 16. f8(A,B,C,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) -> f8(A,B,C,D,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,P1,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,-1 + I1,-1 + I1,K1,L1) [-2 + F >= 0 (?,1) && -2 + D + F >= 0 && -2 + F + F1 >= 0 && -2 + F + -1*F1 >= 0 && -2 + D1 + F >= 0 && -2 + -1*D1 + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && 1 + C1 + -1*E >= 0 && -1 + E + -1*I1 >= 0 && -1 + -1*C1 + E >= 0 && A + -1*D >= 0 && D >= 0 && D + F1 >= 0 && D + -1*F1 >= 0 && D + D1 >= 0 && D + -1*D1 >= 0 && -2 + D + O >= 0 && -2 + A + D >= 0 && C1 + -1*I1 >= 0 && B1 + -1*H1 >= 0 && -1*B1 + H1 >= 0 && -1*F1 >= 0 && D1 + -1*F1 >= 0 && -1*D1 + -1*F1 >= 0 && -2 + -1*F1 + O >= 0 && -2 + A + -1*F1 >= 0 && F1 >= 0 && D1 + F1 >= 0 && -1*D1 + F1 >= 0 && -2 + F1 + O >= 0 && -2 + A + F1 >= 0 && -1*D1 >= 0 && -2 + -1*D1 + O >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + D1 + O >= 0 && -2 + A + D1 >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && B1 >= 1 + Q1 && I1 >= 0 && M1 >= 2 && O1 >= 1 + Q1 && O1 >= 1 && D1 = 0] 17. f8(A,B,C,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) -> f8(A,B,C,D,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,P1,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,-1 + I1,-1 + I1,K1,L1) [-2 + F >= 0 (?,1) && -2 + D + F >= 0 && -2 + F + F1 >= 0 && -2 + F + -1*F1 >= 0 && -2 + D1 + F >= 0 && -2 + -1*D1 + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && 1 + C1 + -1*E >= 0 && -1 + E + -1*I1 >= 0 && -1 + -1*C1 + E >= 0 && A + -1*D >= 0 && D >= 0 && D + F1 >= 0 && D + -1*F1 >= 0 && D + D1 >= 0 && D + -1*D1 >= 0 && -2 + D + O >= 0 && -2 + A + D >= 0 && C1 + -1*I1 >= 0 && B1 + -1*H1 >= 0 && -1*B1 + H1 >= 0 && -1*F1 >= 0 && D1 + -1*F1 >= 0 && -1*D1 + -1*F1 >= 0 && -2 + -1*F1 + O >= 0 && -2 + A + -1*F1 >= 0 && F1 >= 0 && D1 + F1 >= 0 && -1*D1 + F1 >= 0 && -2 + F1 + O >= 0 && -2 + A + F1 >= 0 && -1*D1 >= 0 && -2 + -1*D1 + O >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + D1 + O >= 0 && -2 + A + D1 >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && B1 >= 1 + Q1 && I1 >= 0 && M1 >= 2 && O1 >= 1 + Q1 && 0 >= 1 + O1 && D1 = 0] 18. f8(A,B,C,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) -> f8(A,B,C,D,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,P1,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,-1 + I1,-1 + I1,K1,L1) [-2 + F >= 0 (?,1) && -2 + D + F >= 0 && -2 + F + F1 >= 0 && -2 + F + -1*F1 >= 0 && -2 + D1 + F >= 0 && -2 + -1*D1 + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && 1 + C1 + -1*E >= 0 && -1 + E + -1*I1 >= 0 && -1 + -1*C1 + E >= 0 && A + -1*D >= 0 && D >= 0 && D + F1 >= 0 && D + -1*F1 >= 0 && D + D1 >= 0 && D + -1*D1 >= 0 && -2 + D + O >= 0 && -2 + A + D >= 0 && C1 + -1*I1 >= 0 && B1 + -1*H1 >= 0 && -1*B1 + H1 >= 0 && -1*F1 >= 0 && D1 + -1*F1 >= 0 && -1*D1 + -1*F1 >= 0 && -2 + -1*F1 + O >= 0 && -2 + A + -1*F1 >= 0 && F1 >= 0 && D1 + F1 >= 0 && -1*D1 + F1 >= 0 && -2 + F1 + O >= 0 && -2 + A + F1 >= 0 && -1*D1 >= 0 && -2 + -1*D1 + O >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + D1 + O >= 0 && -2 + A + D1 >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && Q1 >= 1 + B1 && I1 >= 0 && M1 >= 2 && Q1 >= 1 + O1 && O1 >= 1 && D1 = 0] 19. f8(A,B,C,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) -> f8(A,B,C,D,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,P1,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,-1 + I1,-1 + I1,K1,L1) [-2 + F >= 0 (?,1) && -2 + D + F >= 0 && -2 + F + F1 >= 0 && -2 + F + -1*F1 >= 0 && -2 + D1 + F >= 0 && -2 + -1*D1 + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && 1 + C1 + -1*E >= 0 && -1 + E + -1*I1 >= 0 && -1 + -1*C1 + E >= 0 && A + -1*D >= 0 && D >= 0 && D + F1 >= 0 && D + -1*F1 >= 0 && D + D1 >= 0 && D + -1*D1 >= 0 && -2 + D + O >= 0 && -2 + A + D >= 0 && C1 + -1*I1 >= 0 && B1 + -1*H1 >= 0 && -1*B1 + H1 >= 0 && -1*F1 >= 0 && D1 + -1*F1 >= 0 && -1*D1 + -1*F1 >= 0 && -2 + -1*F1 + O >= 0 && -2 + A + -1*F1 >= 0 && F1 >= 0 && D1 + F1 >= 0 && -1*D1 + F1 >= 0 && -2 + F1 + O >= 0 && -2 + A + F1 >= 0 && -1*D1 >= 0 && -2 + -1*D1 + O >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + D1 + O >= 0 && -2 + A + D1 >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && Q1 >= 1 + B1 && I1 >= 0 && M1 >= 2 && Q1 >= 1 + O1 && 0 >= 1 + O1 && D1 = 0] 20. f8(A,B,C,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) -> f8(A,B,C,D,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,P1,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,-1 + I1,-1 + I1,K1,L1) [-2 + F >= 0 (?,1) && -2 + D + F >= 0 && -2 + F + F1 >= 0 && -2 + F + -1*F1 >= 0 && -2 + D1 + F >= 0 && -2 + -1*D1 + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && 1 + C1 + -1*E >= 0 && -1 + E + -1*I1 >= 0 && -1 + -1*C1 + E >= 0 && A + -1*D >= 0 && D >= 0 && D + F1 >= 0 && D + -1*F1 >= 0 && D + D1 >= 0 && D + -1*D1 >= 0 && -2 + D + O >= 0 && -2 + A + D >= 0 && C1 + -1*I1 >= 0 && B1 + -1*H1 >= 0 && -1*B1 + H1 >= 0 && -1*F1 >= 0 && D1 + -1*F1 >= 0 && -1*D1 + -1*F1 >= 0 && -2 + -1*F1 + O >= 0 && -2 + A + -1*F1 >= 0 && F1 >= 0 && D1 + F1 >= 0 && -1*D1 + F1 >= 0 && -2 + F1 + O >= 0 && -2 + A + F1 >= 0 && -1*D1 >= 0 && -2 + -1*D1 + O >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + D1 + O >= 0 && -2 + A + D1 >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && Q1 >= 1 + B1 && I1 >= 0 && M1 >= 2 && O1 >= 1 + Q1 && O1 >= 1 && D1 = 0] 21. f8(A,B,C,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) -> f8(A,B,C,D,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,P1,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,-1 + I1,-1 + I1,K1,L1) [-2 + F >= 0 (?,1) && -2 + D + F >= 0 && -2 + F + F1 >= 0 && -2 + F + -1*F1 >= 0 && -2 + D1 + F >= 0 && -2 + -1*D1 + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && 1 + C1 + -1*E >= 0 && -1 + E + -1*I1 >= 0 && -1 + -1*C1 + E >= 0 && A + -1*D >= 0 && D >= 0 && D + F1 >= 0 && D + -1*F1 >= 0 && D + D1 >= 0 && D + -1*D1 >= 0 && -2 + D + O >= 0 && -2 + A + D >= 0 && C1 + -1*I1 >= 0 && B1 + -1*H1 >= 0 && -1*B1 + H1 >= 0 && -1*F1 >= 0 && D1 + -1*F1 >= 0 && -1*D1 + -1*F1 >= 0 && -2 + -1*F1 + O >= 0 && -2 + A + -1*F1 >= 0 && F1 >= 0 && D1 + F1 >= 0 && -1*D1 + F1 >= 0 && -2 + F1 + O >= 0 && -2 + A + F1 >= 0 && -1*D1 >= 0 && -2 + -1*D1 + O >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + D1 + O >= 0 && -2 + A + D1 >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && Q1 >= 1 + B1 && I1 >= 0 && M1 >= 2 && O1 >= 1 + Q1 && 0 >= 1 + O1 && D1 = 0] 22. f8(A,B,C,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) -> f8(A,B,C,D,E,M1,G,H,I,J,K,O1,M,N,O,P,Q,P1,S,T,U,V,W,X,Y,Z,A1,B1,C1,0,O1,0,O1,B1,-1 + I1,-1 + I1,K1,L1) [-2 + F >= 0 (?,1) && -2 + D + F >= 0 && -2 + F + F1 >= 0 && -2 + F + -1*F1 >= 0 && -2 + D1 + F >= 0 && -2 + -1*D1 + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && 1 + C1 + -1*E >= 0 && -1 + E + -1*I1 >= 0 && -1 + -1*C1 + E >= 0 && A + -1*D >= 0 && D >= 0 && D + F1 >= 0 && D + -1*F1 >= 0 && D + D1 >= 0 && D + -1*D1 >= 0 && -2 + D + O >= 0 && -2 + A + D >= 0 && C1 + -1*I1 >= 0 && B1 + -1*H1 >= 0 && -1*B1 + H1 >= 0 && -1*F1 >= 0 && D1 + -1*F1 >= 0 && -1*D1 + -1*F1 >= 0 && -2 + -1*F1 + O >= 0 && -2 + A + -1*F1 >= 0 && F1 >= 0 && D1 + F1 >= 0 && -1*D1 + F1 >= 0 && -2 + F1 + O >= 0 && -2 + A + F1 >= 0 && -1*D1 >= 0 && -2 + -1*D1 + O >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + D1 + O >= 0 && -2 + A + D1 >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && B1 >= 1 + Q1 && I1 >= 0 && M1 >= 2 && Q1 >= 1 + O1 && O1 >= 1 && D1 = 0] 23. f8(A,B,C,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) -> f16(A,B,C,D,E,M1,G,O1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,T1,C1,S1,P1,Q1,R1,U1,I1,J1,K1,L1) [-2 + F >= 0 (?,1) && -2 + D + F >= 0 && -2 + F + F1 >= 0 && -2 + F + -1*F1 >= 0 && -2 + D1 + F >= 0 && -2 + -1*D1 + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && 1 + C1 + -1*E >= 0 && -1 + E + -1*I1 >= 0 && -1 + -1*C1 + E >= 0 && A + -1*D >= 0 && D >= 0 && D + F1 >= 0 && D + -1*F1 >= 0 && D + D1 >= 0 && D + -1*D1 >= 0 && -2 + D + O >= 0 && -2 + A + D >= 0 && C1 + -1*I1 >= 0 && B1 + -1*H1 >= 0 && -1*B1 + H1 >= 0 && -1*F1 >= 0 && D1 + -1*F1 >= 0 && -1*D1 + -1*F1 >= 0 && -2 + -1*F1 + O >= 0 && -2 + A + -1*F1 >= 0 && F1 >= 0 && D1 + F1 >= 0 && -1*D1 + F1 >= 0 && -2 + F1 + O >= 0 && -2 + A + F1 >= 0 && -1*D1 >= 0 && -2 + -1*D1 + O >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + D1 + O >= 0 && -2 + A + D1 >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && M1 >= 2 && I1 >= 0 && D1 = B1] Signature: {(f1,38);(f14,38);(f15,38);(f16,38);(f8,38)} Flow Graph: [0->{},1->{2,3,4},2->{2,3,4},3->{5,6,7,8,9,10,11,12,13,14},4->{5,6,7,8,9,10,11,12,13,14},5->{5,6,7,8,9,10 ,11,12,13,14},6->{5,6,7,8,9,10,11,12,13,14},7->{5,6,7,8,9,10,11,12,13,14},8->{5,6,7,8,9,10,11,12,13,14} ,9->{5,6,7,8,9,10,11,12,13,14},10->{5,6,7,8,9,10,11,12,13,14},11->{5,6,7,8,9,10,11,12,13,14},12->{5,6,7,8,9 ,10,11,12,13,14},13->{15,16,17,18,19,20,21,22,23},14->{15,16,17,18,19,20,21,22,23},15->{15,16,17,18,19,20,21 ,22,23},16->{15,16,17,18,19,20,21,22,23},17->{15,16,17,18,19,20,21,22,23},18->{15,16,17,18,19,20,21,22,23} ,19->{15,16,17,18,19,20,21,22,23},20->{15,16,17,18,19,20,21,22,23},21->{15,16,17,18,19,20,21,22,23},22->{15 ,16,17,18,19,20,21,22,23},23->{}] + Applied Processor: ArgumentFilter [6,7,8,9,10,12,15,16,17,18,19,20,21,22,23,24,25,26,30,32,35,36,37] + Details: We remove following argument positions: [6,7,8,9,10,12,15,16,17,18,19,20,21,22,23,24,25,26,30,32,35,36,37]. * Step 2: UnsatPaths MAYBE + Considered Problem: Rules: 0. f15(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f16(R1,P1,Q1,D,E,O1,0,A2,O,F2,C1,E2,C2,G2,I1) [0 >= V1 && 0 >= W1 && 0 >= O1 && 0 >= X1] (1,1) 1. f15(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f1(2,O1,P1,D,E,O1,L,N,O,B1,C1,D1,F1,H1,I1) [O1 >= 2] (1,1) 2. f1(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f1(1 + A,B,K,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) [-2 + F >= 0 && -4 + A + F >= 0 && -2 + A >= 0 && B >= 1 + A && A >= 0] (?,1) 3. f1(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f14(D,O1,P1,D,0,M1,C,C,N1,B1,C1,D1,F1,H1,I1) [-2 + F >= 0 (?,1) && -4 + A + F >= 0 && -2 + A >= 0 && A >= B && A >= 0 && M1 >= 2 && C >= 1 && N1 >= M1 && D >= M1 && E = 0] 4. f1(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f14(D,O1,P1,D,0,M1,C,C,N1,B1,C1,D1,F1,H1,I1) [-2 + F >= 0 (?,1) && -4 + A + F >= 0 && -2 + A >= 0 && A >= B && A >= 0 && M1 >= 2 && 0 >= 1 + C && N1 >= M1 && D >= M1 && E = 0] 5. f14(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f14(A,B,C,-1 + D,1 + E,M1,O1,N,O,B1,C1,D1,F1,H1,I1) [-2 + F >= 0 (?,1) && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && D >= 0 && M1 >= 2 && R1 >= 1 && O1 >= 1 && Q1 >= 1] 6. f14(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f14(A,B,C,-1 + D,1 + E,M1,O1,N,O,B1,C1,D1,F1,H1,I1) [-2 + F >= 0 (?,1) && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && D >= 0 && M1 >= 2 && R1 >= 1 && O1 >= 1 && 0 >= 1 + Q1] 7. f14(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f14(A,B,C,-1 + D,1 + E,M1,O1,N,O,B1,C1,D1,F1,H1,I1) [-2 + F >= 0 (?,1) && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && D >= 0 && M1 >= 2 && R1 >= 1 && 0 >= 1 + O1 && Q1 >= 1] 8. f14(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f14(A,B,C,-1 + D,1 + E,M1,O1,N,O,B1,C1,D1,F1,H1,I1) [-2 + F >= 0 (?,1) && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && D >= 0 && M1 >= 2 && R1 >= 1 && 0 >= 1 + O1 && 0 >= 1 + Q1] 9. f14(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f14(A,B,C,-1 + D,1 + E,M1,O1,N,O,B1,C1,D1,F1,H1,I1) [-2 + F >= 0 (?,1) && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && D >= 0 && M1 >= 2 && 0 >= 1 + R1 && O1 >= 1 && Q1 >= 1] 10. f14(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f14(A,B,C,-1 + D,1 + E,M1,O1,N,O,B1,C1,D1,F1,H1,I1) [-2 + F >= 0 (?,1) && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && D >= 0 && M1 >= 2 && 0 >= 1 + R1 && O1 >= 1 && 0 >= 1 + Q1] 11. f14(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f14(A,B,C,-1 + D,1 + E,M1,O1,N,O,B1,C1,D1,F1,H1,I1) [-2 + F >= 0 (?,1) && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && D >= 0 && M1 >= 2 && 0 >= 1 + R1 && 0 >= 1 + O1 && Q1 >= 1] 12. f14(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f14(A,B,C,-1 + D,1 + E,M1,O1,N,O,B1,C1,D1,F1,H1,I1) [-2 + F >= 0 (?,1) && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && D >= 0 && M1 >= 2 && 0 >= 1 + R1 && 0 >= 1 + O1 && 0 >= 1 + Q1] 13. f14(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f8(A,B,C,D,1 + I1,M1,L,P1,O,L,I1,0,0,L,I1) [-2 + F >= 0 (?,1) && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && Q1 >= 2 && M1 >= 2 && D >= 0 && L >= 1 && N = 0] 14. f14(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f8(A,B,C,D,1 + I1,M1,L,P1,O,L,I1,0,0,L,I1) [-2 + F >= 0 (?,1) && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && Q1 >= 2 && M1 >= 2 && D >= 0 && 0 >= 1 + L && N = 0] 15. f8(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f8(A,B,C,D,E,M1,O1,N,O,B1,C1,0,0,B1,-1 + I1) [-2 + F >= 0 (?,1) && -2 + D + F >= 0 && -2 + F + F1 >= 0 && -2 + F + -1*F1 >= 0 && -2 + D1 + F >= 0 && -2 + -1*D1 + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && 1 + C1 + -1*E >= 0 && -1 + E + -1*I1 >= 0 && -1 + -1*C1 + E >= 0 && A + -1*D >= 0 && D >= 0 && D + F1 >= 0 && D + -1*F1 >= 0 && D + D1 >= 0 && D + -1*D1 >= 0 && -2 + D + O >= 0 && -2 + A + D >= 0 && C1 + -1*I1 >= 0 && B1 + -1*H1 >= 0 && -1*B1 + H1 >= 0 && -1*F1 >= 0 && D1 + -1*F1 >= 0 && -1*D1 + -1*F1 >= 0 && -2 + -1*F1 + O >= 0 && -2 + A + -1*F1 >= 0 && F1 >= 0 && D1 + F1 >= 0 && -1*D1 + F1 >= 0 && -2 + F1 + O >= 0 && -2 + A + F1 >= 0 && -1*D1 >= 0 && -2 + -1*D1 + O >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + D1 + O >= 0 && -2 + A + D1 >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && B1 >= 1 + Q1 && I1 >= 0 && M1 >= 2 && Q1 >= 1 + O1 && 0 >= 1 + O1 && D1 = 0] 16. f8(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f8(A,B,C,D,E,M1,O1,N,O,B1,C1,0,0,B1,-1 + I1) [-2 + F >= 0 (?,1) && -2 + D + F >= 0 && -2 + F + F1 >= 0 && -2 + F + -1*F1 >= 0 && -2 + D1 + F >= 0 && -2 + -1*D1 + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && 1 + C1 + -1*E >= 0 && -1 + E + -1*I1 >= 0 && -1 + -1*C1 + E >= 0 && A + -1*D >= 0 && D >= 0 && D + F1 >= 0 && D + -1*F1 >= 0 && D + D1 >= 0 && D + -1*D1 >= 0 && -2 + D + O >= 0 && -2 + A + D >= 0 && C1 + -1*I1 >= 0 && B1 + -1*H1 >= 0 && -1*B1 + H1 >= 0 && -1*F1 >= 0 && D1 + -1*F1 >= 0 && -1*D1 + -1*F1 >= 0 && -2 + -1*F1 + O >= 0 && -2 + A + -1*F1 >= 0 && F1 >= 0 && D1 + F1 >= 0 && -1*D1 + F1 >= 0 && -2 + F1 + O >= 0 && -2 + A + F1 >= 0 && -1*D1 >= 0 && -2 + -1*D1 + O >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + D1 + O >= 0 && -2 + A + D1 >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && B1 >= 1 + Q1 && I1 >= 0 && M1 >= 2 && O1 >= 1 + Q1 && O1 >= 1 && D1 = 0] 17. f8(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f8(A,B,C,D,E,M1,O1,N,O,B1,C1,0,0,B1,-1 + I1) [-2 + F >= 0 (?,1) && -2 + D + F >= 0 && -2 + F + F1 >= 0 && -2 + F + -1*F1 >= 0 && -2 + D1 + F >= 0 && -2 + -1*D1 + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && 1 + C1 + -1*E >= 0 && -1 + E + -1*I1 >= 0 && -1 + -1*C1 + E >= 0 && A + -1*D >= 0 && D >= 0 && D + F1 >= 0 && D + -1*F1 >= 0 && D + D1 >= 0 && D + -1*D1 >= 0 && -2 + D + O >= 0 && -2 + A + D >= 0 && C1 + -1*I1 >= 0 && B1 + -1*H1 >= 0 && -1*B1 + H1 >= 0 && -1*F1 >= 0 && D1 + -1*F1 >= 0 && -1*D1 + -1*F1 >= 0 && -2 + -1*F1 + O >= 0 && -2 + A + -1*F1 >= 0 && F1 >= 0 && D1 + F1 >= 0 && -1*D1 + F1 >= 0 && -2 + F1 + O >= 0 && -2 + A + F1 >= 0 && -1*D1 >= 0 && -2 + -1*D1 + O >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + D1 + O >= 0 && -2 + A + D1 >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && B1 >= 1 + Q1 && I1 >= 0 && M1 >= 2 && O1 >= 1 + Q1 && 0 >= 1 + O1 && D1 = 0] 18. f8(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f8(A,B,C,D,E,M1,O1,N,O,B1,C1,0,0,B1,-1 + I1) [-2 + F >= 0 (?,1) && -2 + D + F >= 0 && -2 + F + F1 >= 0 && -2 + F + -1*F1 >= 0 && -2 + D1 + F >= 0 && -2 + -1*D1 + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && 1 + C1 + -1*E >= 0 && -1 + E + -1*I1 >= 0 && -1 + -1*C1 + E >= 0 && A + -1*D >= 0 && D >= 0 && D + F1 >= 0 && D + -1*F1 >= 0 && D + D1 >= 0 && D + -1*D1 >= 0 && -2 + D + O >= 0 && -2 + A + D >= 0 && C1 + -1*I1 >= 0 && B1 + -1*H1 >= 0 && -1*B1 + H1 >= 0 && -1*F1 >= 0 && D1 + -1*F1 >= 0 && -1*D1 + -1*F1 >= 0 && -2 + -1*F1 + O >= 0 && -2 + A + -1*F1 >= 0 && F1 >= 0 && D1 + F1 >= 0 && -1*D1 + F1 >= 0 && -2 + F1 + O >= 0 && -2 + A + F1 >= 0 && -1*D1 >= 0 && -2 + -1*D1 + O >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + D1 + O >= 0 && -2 + A + D1 >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && Q1 >= 1 + B1 && I1 >= 0 && M1 >= 2 && Q1 >= 1 + O1 && O1 >= 1 && D1 = 0] 19. f8(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f8(A,B,C,D,E,M1,O1,N,O,B1,C1,0,0,B1,-1 + I1) [-2 + F >= 0 (?,1) && -2 + D + F >= 0 && -2 + F + F1 >= 0 && -2 + F + -1*F1 >= 0 && -2 + D1 + F >= 0 && -2 + -1*D1 + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && 1 + C1 + -1*E >= 0 && -1 + E + -1*I1 >= 0 && -1 + -1*C1 + E >= 0 && A + -1*D >= 0 && D >= 0 && D + F1 >= 0 && D + -1*F1 >= 0 && D + D1 >= 0 && D + -1*D1 >= 0 && -2 + D + O >= 0 && -2 + A + D >= 0 && C1 + -1*I1 >= 0 && B1 + -1*H1 >= 0 && -1*B1 + H1 >= 0 && -1*F1 >= 0 && D1 + -1*F1 >= 0 && -1*D1 + -1*F1 >= 0 && -2 + -1*F1 + O >= 0 && -2 + A + -1*F1 >= 0 && F1 >= 0 && D1 + F1 >= 0 && -1*D1 + F1 >= 0 && -2 + F1 + O >= 0 && -2 + A + F1 >= 0 && -1*D1 >= 0 && -2 + -1*D1 + O >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + D1 + O >= 0 && -2 + A + D1 >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && Q1 >= 1 + B1 && I1 >= 0 && M1 >= 2 && Q1 >= 1 + O1 && 0 >= 1 + O1 && D1 = 0] 20. f8(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f8(A,B,C,D,E,M1,O1,N,O,B1,C1,0,0,B1,-1 + I1) [-2 + F >= 0 (?,1) && -2 + D + F >= 0 && -2 + F + F1 >= 0 && -2 + F + -1*F1 >= 0 && -2 + D1 + F >= 0 && -2 + -1*D1 + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && 1 + C1 + -1*E >= 0 && -1 + E + -1*I1 >= 0 && -1 + -1*C1 + E >= 0 && A + -1*D >= 0 && D >= 0 && D + F1 >= 0 && D + -1*F1 >= 0 && D + D1 >= 0 && D + -1*D1 >= 0 && -2 + D + O >= 0 && -2 + A + D >= 0 && C1 + -1*I1 >= 0 && B1 + -1*H1 >= 0 && -1*B1 + H1 >= 0 && -1*F1 >= 0 && D1 + -1*F1 >= 0 && -1*D1 + -1*F1 >= 0 && -2 + -1*F1 + O >= 0 && -2 + A + -1*F1 >= 0 && F1 >= 0 && D1 + F1 >= 0 && -1*D1 + F1 >= 0 && -2 + F1 + O >= 0 && -2 + A + F1 >= 0 && -1*D1 >= 0 && -2 + -1*D1 + O >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + D1 + O >= 0 && -2 + A + D1 >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && Q1 >= 1 + B1 && I1 >= 0 && M1 >= 2 && O1 >= 1 + Q1 && O1 >= 1 && D1 = 0] 21. f8(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f8(A,B,C,D,E,M1,O1,N,O,B1,C1,0,0,B1,-1 + I1) [-2 + F >= 0 (?,1) && -2 + D + F >= 0 && -2 + F + F1 >= 0 && -2 + F + -1*F1 >= 0 && -2 + D1 + F >= 0 && -2 + -1*D1 + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && 1 + C1 + -1*E >= 0 && -1 + E + -1*I1 >= 0 && -1 + -1*C1 + E >= 0 && A + -1*D >= 0 && D >= 0 && D + F1 >= 0 && D + -1*F1 >= 0 && D + D1 >= 0 && D + -1*D1 >= 0 && -2 + D + O >= 0 && -2 + A + D >= 0 && C1 + -1*I1 >= 0 && B1 + -1*H1 >= 0 && -1*B1 + H1 >= 0 && -1*F1 >= 0 && D1 + -1*F1 >= 0 && -1*D1 + -1*F1 >= 0 && -2 + -1*F1 + O >= 0 && -2 + A + -1*F1 >= 0 && F1 >= 0 && D1 + F1 >= 0 && -1*D1 + F1 >= 0 && -2 + F1 + O >= 0 && -2 + A + F1 >= 0 && -1*D1 >= 0 && -2 + -1*D1 + O >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + D1 + O >= 0 && -2 + A + D1 >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && Q1 >= 1 + B1 && I1 >= 0 && M1 >= 2 && O1 >= 1 + Q1 && 0 >= 1 + O1 && D1 = 0] 22. f8(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f8(A,B,C,D,E,M1,O1,N,O,B1,C1,0,0,B1,-1 + I1) [-2 + F >= 0 (?,1) && -2 + D + F >= 0 && -2 + F + F1 >= 0 && -2 + F + -1*F1 >= 0 && -2 + D1 + F >= 0 && -2 + -1*D1 + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && 1 + C1 + -1*E >= 0 && -1 + E + -1*I1 >= 0 && -1 + -1*C1 + E >= 0 && A + -1*D >= 0 && D >= 0 && D + F1 >= 0 && D + -1*F1 >= 0 && D + D1 >= 0 && D + -1*D1 >= 0 && -2 + D + O >= 0 && -2 + A + D >= 0 && C1 + -1*I1 >= 0 && B1 + -1*H1 >= 0 && -1*B1 + H1 >= 0 && -1*F1 >= 0 && D1 + -1*F1 >= 0 && -1*D1 + -1*F1 >= 0 && -2 + -1*F1 + O >= 0 && -2 + A + -1*F1 >= 0 && F1 >= 0 && D1 + F1 >= 0 && -1*D1 + F1 >= 0 && -2 + F1 + O >= 0 && -2 + A + F1 >= 0 && -1*D1 >= 0 && -2 + -1*D1 + O >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + D1 + O >= 0 && -2 + A + D1 >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && B1 >= 1 + Q1 && I1 >= 0 && M1 >= 2 && Q1 >= 1 + O1 && O1 >= 1 && D1 = 0] 23. f8(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f16(A,B,C,D,E,M1,L,N,O,T1,C1,S1,Q1,U1,I1) [-2 + F >= 0 (?,1) && -2 + D + F >= 0 && -2 + F + F1 >= 0 && -2 + F + -1*F1 >= 0 && -2 + D1 + F >= 0 && -2 + -1*D1 + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && 1 + C1 + -1*E >= 0 && -1 + E + -1*I1 >= 0 && -1 + -1*C1 + E >= 0 && A + -1*D >= 0 && D >= 0 && D + F1 >= 0 && D + -1*F1 >= 0 && D + D1 >= 0 && D + -1*D1 >= 0 && -2 + D + O >= 0 && -2 + A + D >= 0 && C1 + -1*I1 >= 0 && B1 + -1*H1 >= 0 && -1*B1 + H1 >= 0 && -1*F1 >= 0 && D1 + -1*F1 >= 0 && -1*D1 + -1*F1 >= 0 && -2 + -1*F1 + O >= 0 && -2 + A + -1*F1 >= 0 && F1 >= 0 && D1 + F1 >= 0 && -1*D1 + F1 >= 0 && -2 + F1 + O >= 0 && -2 + A + F1 >= 0 && -1*D1 >= 0 && -2 + -1*D1 + O >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + D1 + O >= 0 && -2 + A + D1 >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && M1 >= 2 && I1 >= 0 && D1 = B1] Signature: {(f1,38);(f14,38);(f15,38);(f16,38);(f8,38)} Flow Graph: [0->{},1->{2,3,4},2->{2,3,4},3->{5,6,7,8,9,10,11,12,13,14},4->{5,6,7,8,9,10,11,12,13,14},5->{5,6,7,8,9,10 ,11,12,13,14},6->{5,6,7,8,9,10,11,12,13,14},7->{5,6,7,8,9,10,11,12,13,14},8->{5,6,7,8,9,10,11,12,13,14} ,9->{5,6,7,8,9,10,11,12,13,14},10->{5,6,7,8,9,10,11,12,13,14},11->{5,6,7,8,9,10,11,12,13,14},12->{5,6,7,8,9 ,10,11,12,13,14},13->{15,16,17,18,19,20,21,22,23},14->{15,16,17,18,19,20,21,22,23},15->{15,16,17,18,19,20,21 ,22,23},16->{15,16,17,18,19,20,21,22,23},17->{15,16,17,18,19,20,21,22,23},18->{15,16,17,18,19,20,21,22,23} ,19->{15,16,17,18,19,20,21,22,23},20->{15,16,17,18,19,20,21,22,23},21->{15,16,17,18,19,20,21,22,23},22->{15 ,16,17,18,19,20,21,22,23},23->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(3,13) ,(3,14) ,(4,13) ,(4,14) ,(5,14) ,(6,14) ,(7,13) ,(8,13) ,(9,14) ,(10,14) ,(11,13) ,(12,13) ,(13,21) ,(13,23) ,(14,22) ,(14,23) ,(21,22) ,(21,23) ,(22,21) ,(22,23)] * Step 3: FromIts MAYBE + Considered Problem: Rules: 0. f15(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f16(R1,P1,Q1,D,E,O1,0,A2,O,F2,C1,E2,C2,G2,I1) [0 >= V1 && 0 >= W1 && 0 >= O1 && 0 >= X1] (1,1) 1. f15(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f1(2,O1,P1,D,E,O1,L,N,O,B1,C1,D1,F1,H1,I1) [O1 >= 2] (1,1) 2. f1(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f1(1 + A,B,K,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) [-2 + F >= 0 && -4 + A + F >= 0 && -2 + A >= 0 && B >= 1 + A && A >= 0] (?,1) 3. f1(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f14(D,O1,P1,D,0,M1,C,C,N1,B1,C1,D1,F1,H1,I1) [-2 + F >= 0 (?,1) && -4 + A + F >= 0 && -2 + A >= 0 && A >= B && A >= 0 && M1 >= 2 && C >= 1 && N1 >= M1 && D >= M1 && E = 0] 4. f1(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f14(D,O1,P1,D,0,M1,C,C,N1,B1,C1,D1,F1,H1,I1) [-2 + F >= 0 (?,1) && -4 + A + F >= 0 && -2 + A >= 0 && A >= B && A >= 0 && M1 >= 2 && 0 >= 1 + C && N1 >= M1 && D >= M1 && E = 0] 5. f14(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f14(A,B,C,-1 + D,1 + E,M1,O1,N,O,B1,C1,D1,F1,H1,I1) [-2 + F >= 0 (?,1) && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && D >= 0 && M1 >= 2 && R1 >= 1 && O1 >= 1 && Q1 >= 1] 6. f14(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f14(A,B,C,-1 + D,1 + E,M1,O1,N,O,B1,C1,D1,F1,H1,I1) [-2 + F >= 0 (?,1) && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && D >= 0 && M1 >= 2 && R1 >= 1 && O1 >= 1 && 0 >= 1 + Q1] 7. f14(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f14(A,B,C,-1 + D,1 + E,M1,O1,N,O,B1,C1,D1,F1,H1,I1) [-2 + F >= 0 (?,1) && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && D >= 0 && M1 >= 2 && R1 >= 1 && 0 >= 1 + O1 && Q1 >= 1] 8. f14(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f14(A,B,C,-1 + D,1 + E,M1,O1,N,O,B1,C1,D1,F1,H1,I1) [-2 + F >= 0 (?,1) && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && D >= 0 && M1 >= 2 && R1 >= 1 && 0 >= 1 + O1 && 0 >= 1 + Q1] 9. f14(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f14(A,B,C,-1 + D,1 + E,M1,O1,N,O,B1,C1,D1,F1,H1,I1) [-2 + F >= 0 (?,1) && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && D >= 0 && M1 >= 2 && 0 >= 1 + R1 && O1 >= 1 && Q1 >= 1] 10. f14(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f14(A,B,C,-1 + D,1 + E,M1,O1,N,O,B1,C1,D1,F1,H1,I1) [-2 + F >= 0 (?,1) && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && D >= 0 && M1 >= 2 && 0 >= 1 + R1 && O1 >= 1 && 0 >= 1 + Q1] 11. f14(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f14(A,B,C,-1 + D,1 + E,M1,O1,N,O,B1,C1,D1,F1,H1,I1) [-2 + F >= 0 (?,1) && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && D >= 0 && M1 >= 2 && 0 >= 1 + R1 && 0 >= 1 + O1 && Q1 >= 1] 12. f14(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f14(A,B,C,-1 + D,1 + E,M1,O1,N,O,B1,C1,D1,F1,H1,I1) [-2 + F >= 0 (?,1) && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && D >= 0 && M1 >= 2 && 0 >= 1 + R1 && 0 >= 1 + O1 && 0 >= 1 + Q1] 13. f14(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f8(A,B,C,D,1 + I1,M1,L,P1,O,L,I1,0,0,L,I1) [-2 + F >= 0 (?,1) && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && Q1 >= 2 && M1 >= 2 && D >= 0 && L >= 1 && N = 0] 14. f14(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f8(A,B,C,D,1 + I1,M1,L,P1,O,L,I1,0,0,L,I1) [-2 + F >= 0 (?,1) && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && Q1 >= 2 && M1 >= 2 && D >= 0 && 0 >= 1 + L && N = 0] 15. f8(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f8(A,B,C,D,E,M1,O1,N,O,B1,C1,0,0,B1,-1 + I1) [-2 + F >= 0 (?,1) && -2 + D + F >= 0 && -2 + F + F1 >= 0 && -2 + F + -1*F1 >= 0 && -2 + D1 + F >= 0 && -2 + -1*D1 + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && 1 + C1 + -1*E >= 0 && -1 + E + -1*I1 >= 0 && -1 + -1*C1 + E >= 0 && A + -1*D >= 0 && D >= 0 && D + F1 >= 0 && D + -1*F1 >= 0 && D + D1 >= 0 && D + -1*D1 >= 0 && -2 + D + O >= 0 && -2 + A + D >= 0 && C1 + -1*I1 >= 0 && B1 + -1*H1 >= 0 && -1*B1 + H1 >= 0 && -1*F1 >= 0 && D1 + -1*F1 >= 0 && -1*D1 + -1*F1 >= 0 && -2 + -1*F1 + O >= 0 && -2 + A + -1*F1 >= 0 && F1 >= 0 && D1 + F1 >= 0 && -1*D1 + F1 >= 0 && -2 + F1 + O >= 0 && -2 + A + F1 >= 0 && -1*D1 >= 0 && -2 + -1*D1 + O >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + D1 + O >= 0 && -2 + A + D1 >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && B1 >= 1 + Q1 && I1 >= 0 && M1 >= 2 && Q1 >= 1 + O1 && 0 >= 1 + O1 && D1 = 0] 16. f8(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f8(A,B,C,D,E,M1,O1,N,O,B1,C1,0,0,B1,-1 + I1) [-2 + F >= 0 (?,1) && -2 + D + F >= 0 && -2 + F + F1 >= 0 && -2 + F + -1*F1 >= 0 && -2 + D1 + F >= 0 && -2 + -1*D1 + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && 1 + C1 + -1*E >= 0 && -1 + E + -1*I1 >= 0 && -1 + -1*C1 + E >= 0 && A + -1*D >= 0 && D >= 0 && D + F1 >= 0 && D + -1*F1 >= 0 && D + D1 >= 0 && D + -1*D1 >= 0 && -2 + D + O >= 0 && -2 + A + D >= 0 && C1 + -1*I1 >= 0 && B1 + -1*H1 >= 0 && -1*B1 + H1 >= 0 && -1*F1 >= 0 && D1 + -1*F1 >= 0 && -1*D1 + -1*F1 >= 0 && -2 + -1*F1 + O >= 0 && -2 + A + -1*F1 >= 0 && F1 >= 0 && D1 + F1 >= 0 && -1*D1 + F1 >= 0 && -2 + F1 + O >= 0 && -2 + A + F1 >= 0 && -1*D1 >= 0 && -2 + -1*D1 + O >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + D1 + O >= 0 && -2 + A + D1 >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && B1 >= 1 + Q1 && I1 >= 0 && M1 >= 2 && O1 >= 1 + Q1 && O1 >= 1 && D1 = 0] 17. f8(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f8(A,B,C,D,E,M1,O1,N,O,B1,C1,0,0,B1,-1 + I1) [-2 + F >= 0 (?,1) && -2 + D + F >= 0 && -2 + F + F1 >= 0 && -2 + F + -1*F1 >= 0 && -2 + D1 + F >= 0 && -2 + -1*D1 + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && 1 + C1 + -1*E >= 0 && -1 + E + -1*I1 >= 0 && -1 + -1*C1 + E >= 0 && A + -1*D >= 0 && D >= 0 && D + F1 >= 0 && D + -1*F1 >= 0 && D + D1 >= 0 && D + -1*D1 >= 0 && -2 + D + O >= 0 && -2 + A + D >= 0 && C1 + -1*I1 >= 0 && B1 + -1*H1 >= 0 && -1*B1 + H1 >= 0 && -1*F1 >= 0 && D1 + -1*F1 >= 0 && -1*D1 + -1*F1 >= 0 && -2 + -1*F1 + O >= 0 && -2 + A + -1*F1 >= 0 && F1 >= 0 && D1 + F1 >= 0 && -1*D1 + F1 >= 0 && -2 + F1 + O >= 0 && -2 + A + F1 >= 0 && -1*D1 >= 0 && -2 + -1*D1 + O >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + D1 + O >= 0 && -2 + A + D1 >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && B1 >= 1 + Q1 && I1 >= 0 && M1 >= 2 && O1 >= 1 + Q1 && 0 >= 1 + O1 && D1 = 0] 18. f8(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f8(A,B,C,D,E,M1,O1,N,O,B1,C1,0,0,B1,-1 + I1) [-2 + F >= 0 (?,1) && -2 + D + F >= 0 && -2 + F + F1 >= 0 && -2 + F + -1*F1 >= 0 && -2 + D1 + F >= 0 && -2 + -1*D1 + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && 1 + C1 + -1*E >= 0 && -1 + E + -1*I1 >= 0 && -1 + -1*C1 + E >= 0 && A + -1*D >= 0 && D >= 0 && D + F1 >= 0 && D + -1*F1 >= 0 && D + D1 >= 0 && D + -1*D1 >= 0 && -2 + D + O >= 0 && -2 + A + D >= 0 && C1 + -1*I1 >= 0 && B1 + -1*H1 >= 0 && -1*B1 + H1 >= 0 && -1*F1 >= 0 && D1 + -1*F1 >= 0 && -1*D1 + -1*F1 >= 0 && -2 + -1*F1 + O >= 0 && -2 + A + -1*F1 >= 0 && F1 >= 0 && D1 + F1 >= 0 && -1*D1 + F1 >= 0 && -2 + F1 + O >= 0 && -2 + A + F1 >= 0 && -1*D1 >= 0 && -2 + -1*D1 + O >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + D1 + O >= 0 && -2 + A + D1 >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && Q1 >= 1 + B1 && I1 >= 0 && M1 >= 2 && Q1 >= 1 + O1 && O1 >= 1 && D1 = 0] 19. f8(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f8(A,B,C,D,E,M1,O1,N,O,B1,C1,0,0,B1,-1 + I1) [-2 + F >= 0 (?,1) && -2 + D + F >= 0 && -2 + F + F1 >= 0 && -2 + F + -1*F1 >= 0 && -2 + D1 + F >= 0 && -2 + -1*D1 + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && 1 + C1 + -1*E >= 0 && -1 + E + -1*I1 >= 0 && -1 + -1*C1 + E >= 0 && A + -1*D >= 0 && D >= 0 && D + F1 >= 0 && D + -1*F1 >= 0 && D + D1 >= 0 && D + -1*D1 >= 0 && -2 + D + O >= 0 && -2 + A + D >= 0 && C1 + -1*I1 >= 0 && B1 + -1*H1 >= 0 && -1*B1 + H1 >= 0 && -1*F1 >= 0 && D1 + -1*F1 >= 0 && -1*D1 + -1*F1 >= 0 && -2 + -1*F1 + O >= 0 && -2 + A + -1*F1 >= 0 && F1 >= 0 && D1 + F1 >= 0 && -1*D1 + F1 >= 0 && -2 + F1 + O >= 0 && -2 + A + F1 >= 0 && -1*D1 >= 0 && -2 + -1*D1 + O >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + D1 + O >= 0 && -2 + A + D1 >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && Q1 >= 1 + B1 && I1 >= 0 && M1 >= 2 && Q1 >= 1 + O1 && 0 >= 1 + O1 && D1 = 0] 20. f8(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f8(A,B,C,D,E,M1,O1,N,O,B1,C1,0,0,B1,-1 + I1) [-2 + F >= 0 (?,1) && -2 + D + F >= 0 && -2 + F + F1 >= 0 && -2 + F + -1*F1 >= 0 && -2 + D1 + F >= 0 && -2 + -1*D1 + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && 1 + C1 + -1*E >= 0 && -1 + E + -1*I1 >= 0 && -1 + -1*C1 + E >= 0 && A + -1*D >= 0 && D >= 0 && D + F1 >= 0 && D + -1*F1 >= 0 && D + D1 >= 0 && D + -1*D1 >= 0 && -2 + D + O >= 0 && -2 + A + D >= 0 && C1 + -1*I1 >= 0 && B1 + -1*H1 >= 0 && -1*B1 + H1 >= 0 && -1*F1 >= 0 && D1 + -1*F1 >= 0 && -1*D1 + -1*F1 >= 0 && -2 + -1*F1 + O >= 0 && -2 + A + -1*F1 >= 0 && F1 >= 0 && D1 + F1 >= 0 && -1*D1 + F1 >= 0 && -2 + F1 + O >= 0 && -2 + A + F1 >= 0 && -1*D1 >= 0 && -2 + -1*D1 + O >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + D1 + O >= 0 && -2 + A + D1 >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && Q1 >= 1 + B1 && I1 >= 0 && M1 >= 2 && O1 >= 1 + Q1 && O1 >= 1 && D1 = 0] 21. f8(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f8(A,B,C,D,E,M1,O1,N,O,B1,C1,0,0,B1,-1 + I1) [-2 + F >= 0 (?,1) && -2 + D + F >= 0 && -2 + F + F1 >= 0 && -2 + F + -1*F1 >= 0 && -2 + D1 + F >= 0 && -2 + -1*D1 + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && 1 + C1 + -1*E >= 0 && -1 + E + -1*I1 >= 0 && -1 + -1*C1 + E >= 0 && A + -1*D >= 0 && D >= 0 && D + F1 >= 0 && D + -1*F1 >= 0 && D + D1 >= 0 && D + -1*D1 >= 0 && -2 + D + O >= 0 && -2 + A + D >= 0 && C1 + -1*I1 >= 0 && B1 + -1*H1 >= 0 && -1*B1 + H1 >= 0 && -1*F1 >= 0 && D1 + -1*F1 >= 0 && -1*D1 + -1*F1 >= 0 && -2 + -1*F1 + O >= 0 && -2 + A + -1*F1 >= 0 && F1 >= 0 && D1 + F1 >= 0 && -1*D1 + F1 >= 0 && -2 + F1 + O >= 0 && -2 + A + F1 >= 0 && -1*D1 >= 0 && -2 + -1*D1 + O >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + D1 + O >= 0 && -2 + A + D1 >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && Q1 >= 1 + B1 && I1 >= 0 && M1 >= 2 && O1 >= 1 + Q1 && 0 >= 1 + O1 && D1 = 0] 22. f8(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f8(A,B,C,D,E,M1,O1,N,O,B1,C1,0,0,B1,-1 + I1) [-2 + F >= 0 (?,1) && -2 + D + F >= 0 && -2 + F + F1 >= 0 && -2 + F + -1*F1 >= 0 && -2 + D1 + F >= 0 && -2 + -1*D1 + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && 1 + C1 + -1*E >= 0 && -1 + E + -1*I1 >= 0 && -1 + -1*C1 + E >= 0 && A + -1*D >= 0 && D >= 0 && D + F1 >= 0 && D + -1*F1 >= 0 && D + D1 >= 0 && D + -1*D1 >= 0 && -2 + D + O >= 0 && -2 + A + D >= 0 && C1 + -1*I1 >= 0 && B1 + -1*H1 >= 0 && -1*B1 + H1 >= 0 && -1*F1 >= 0 && D1 + -1*F1 >= 0 && -1*D1 + -1*F1 >= 0 && -2 + -1*F1 + O >= 0 && -2 + A + -1*F1 >= 0 && F1 >= 0 && D1 + F1 >= 0 && -1*D1 + F1 >= 0 && -2 + F1 + O >= 0 && -2 + A + F1 >= 0 && -1*D1 >= 0 && -2 + -1*D1 + O >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + D1 + O >= 0 && -2 + A + D1 >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && B1 >= 1 + Q1 && I1 >= 0 && M1 >= 2 && Q1 >= 1 + O1 && O1 >= 1 && D1 = 0] 23. f8(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f16(A,B,C,D,E,M1,L,N,O,T1,C1,S1,Q1,U1,I1) [-2 + F >= 0 (?,1) && -2 + D + F >= 0 && -2 + F + F1 >= 0 && -2 + F + -1*F1 >= 0 && -2 + D1 + F >= 0 && -2 + -1*D1 + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && 1 + C1 + -1*E >= 0 && -1 + E + -1*I1 >= 0 && -1 + -1*C1 + E >= 0 && A + -1*D >= 0 && D >= 0 && D + F1 >= 0 && D + -1*F1 >= 0 && D + D1 >= 0 && D + -1*D1 >= 0 && -2 + D + O >= 0 && -2 + A + D >= 0 && C1 + -1*I1 >= 0 && B1 + -1*H1 >= 0 && -1*B1 + H1 >= 0 && -1*F1 >= 0 && D1 + -1*F1 >= 0 && -1*D1 + -1*F1 >= 0 && -2 + -1*F1 + O >= 0 && -2 + A + -1*F1 >= 0 && F1 >= 0 && D1 + F1 >= 0 && -1*D1 + F1 >= 0 && -2 + F1 + O >= 0 && -2 + A + F1 >= 0 && -1*D1 >= 0 && -2 + -1*D1 + O >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + D1 + O >= 0 && -2 + A + D1 >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && M1 >= 2 && I1 >= 0 && D1 = B1] Signature: {(f1,38);(f14,38);(f15,38);(f16,38);(f8,38)} Flow Graph: [0->{},1->{2,3,4},2->{2,3,4},3->{5,6,7,8,9,10,11,12},4->{5,6,7,8,9,10,11,12},5->{5,6,7,8,9,10,11,12,13} ,6->{5,6,7,8,9,10,11,12,13},7->{5,6,7,8,9,10,11,12,14},8->{5,6,7,8,9,10,11,12,14},9->{5,6,7,8,9,10,11,12,13} ,10->{5,6,7,8,9,10,11,12,13},11->{5,6,7,8,9,10,11,12,14},12->{5,6,7,8,9,10,11,12,14},13->{15,16,17,18,19,20 ,22},14->{15,16,17,18,19,20,21},15->{15,16,17,18,19,20,21,22,23},16->{15,16,17,18,19,20,21,22,23},17->{15,16 ,17,18,19,20,21,22,23},18->{15,16,17,18,19,20,21,22,23},19->{15,16,17,18,19,20,21,22,23},20->{15,16,17,18,19 ,20,21,22,23},21->{15,16,17,18,19,20,21},22->{15,16,17,18,19,20,22},23->{}] + Applied Processor: FromIts + Details: () * Step 4: AddSinks MAYBE + Considered Problem: Rules: f15(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f16(R1,P1,Q1,D,E,O1,0,A2,O,F2,C1,E2,C2,G2,I1) [0 >= V1 && 0 >= W1 && 0 >= O1 && 0 >= X1] f15(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f1(2,O1,P1,D,E,O1,L,N,O,B1,C1,D1,F1,H1,I1) [O1 >= 2] f1(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f1(1 + A,B,K,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) [-2 + F >= 0 && -4 + A + F >= 0 && -2 + A >= 0 && B >= 1 + A && A >= 0] f1(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f14(D,O1,P1,D,0,M1,C,C,N1,B1,C1,D1,F1,H1,I1) [-2 + F >= 0 && -4 + A + F >= 0 && -2 + A >= 0 && A >= B && A >= 0 && M1 >= 2 && C >= 1 && N1 >= M1 && D >= M1 && E = 0] f1(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f14(D,O1,P1,D,0,M1,C,C,N1,B1,C1,D1,F1,H1,I1) [-2 + F >= 0 && -4 + A + F >= 0 && -2 + A >= 0 && A >= B && A >= 0 && M1 >= 2 && 0 >= 1 + C && N1 >= M1 && D >= M1 && E = 0] f14(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f14(A,B,C,-1 + D,1 + E,M1,O1,N,O,B1,C1,D1,F1,H1,I1) [-2 + F >= 0 && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && D >= 0 && M1 >= 2 && R1 >= 1 && O1 >= 1 && Q1 >= 1] f14(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f14(A,B,C,-1 + D,1 + E,M1,O1,N,O,B1,C1,D1,F1,H1,I1) [-2 + F >= 0 && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && D >= 0 && M1 >= 2 && R1 >= 1 && O1 >= 1 && 0 >= 1 + Q1] f14(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f14(A,B,C,-1 + D,1 + E,M1,O1,N,O,B1,C1,D1,F1,H1,I1) [-2 + F >= 0 && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && D >= 0 && M1 >= 2 && R1 >= 1 && 0 >= 1 + O1 && Q1 >= 1] f14(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f14(A,B,C,-1 + D,1 + E,M1,O1,N,O,B1,C1,D1,F1,H1,I1) [-2 + F >= 0 && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && D >= 0 && M1 >= 2 && R1 >= 1 && 0 >= 1 + O1 && 0 >= 1 + Q1] f14(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f14(A,B,C,-1 + D,1 + E,M1,O1,N,O,B1,C1,D1,F1,H1,I1) [-2 + F >= 0 && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && D >= 0 && M1 >= 2 && 0 >= 1 + R1 && O1 >= 1 && Q1 >= 1] f14(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f14(A,B,C,-1 + D,1 + E,M1,O1,N,O,B1,C1,D1,F1,H1,I1) [-2 + F >= 0 && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && D >= 0 && M1 >= 2 && 0 >= 1 + R1 && O1 >= 1 && 0 >= 1 + Q1] f14(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f14(A,B,C,-1 + D,1 + E,M1,O1,N,O,B1,C1,D1,F1,H1,I1) [-2 + F >= 0 && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && D >= 0 && M1 >= 2 && 0 >= 1 + R1 && 0 >= 1 + O1 && Q1 >= 1] f14(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f14(A,B,C,-1 + D,1 + E,M1,O1,N,O,B1,C1,D1,F1,H1,I1) [-2 + F >= 0 && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && D >= 0 && M1 >= 2 && 0 >= 1 + R1 && 0 >= 1 + O1 && 0 >= 1 + Q1] f14(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f8(A,B,C,D,1 + I1,M1,L,P1,O,L,I1,0,0,L,I1) [-2 + F >= 0 && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && Q1 >= 2 && M1 >= 2 && D >= 0 && L >= 1 && N = 0] f14(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f8(A,B,C,D,1 + I1,M1,L,P1,O,L,I1,0,0,L,I1) [-2 + F >= 0 && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && Q1 >= 2 && M1 >= 2 && D >= 0 && 0 >= 1 + L && N = 0] f8(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f8(A,B,C,D,E,M1,O1,N,O,B1,C1,0,0,B1,-1 + I1) [-2 + F >= 0 && -2 + D + F >= 0 && -2 + F + F1 >= 0 && -2 + F + -1*F1 >= 0 && -2 + D1 + F >= 0 && -2 + -1*D1 + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && 1 + C1 + -1*E >= 0 && -1 + E + -1*I1 >= 0 && -1 + -1*C1 + E >= 0 && A + -1*D >= 0 && D >= 0 && D + F1 >= 0 && D + -1*F1 >= 0 && D + D1 >= 0 && D + -1*D1 >= 0 && -2 + D + O >= 0 && -2 + A + D >= 0 && C1 + -1*I1 >= 0 && B1 + -1*H1 >= 0 && -1*B1 + H1 >= 0 && -1*F1 >= 0 && D1 + -1*F1 >= 0 && -1*D1 + -1*F1 >= 0 && -2 + -1*F1 + O >= 0 && -2 + A + -1*F1 >= 0 && F1 >= 0 && D1 + F1 >= 0 && -1*D1 + F1 >= 0 && -2 + F1 + O >= 0 && -2 + A + F1 >= 0 && -1*D1 >= 0 && -2 + -1*D1 + O >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + D1 + O >= 0 && -2 + A + D1 >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && B1 >= 1 + Q1 && I1 >= 0 && M1 >= 2 && Q1 >= 1 + O1 && 0 >= 1 + O1 && D1 = 0] f8(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f8(A,B,C,D,E,M1,O1,N,O,B1,C1,0,0,B1,-1 + I1) [-2 + F >= 0 && -2 + D + F >= 0 && -2 + F + F1 >= 0 && -2 + F + -1*F1 >= 0 && -2 + D1 + F >= 0 && -2 + -1*D1 + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && 1 + C1 + -1*E >= 0 && -1 + E + -1*I1 >= 0 && -1 + -1*C1 + E >= 0 && A + -1*D >= 0 && D >= 0 && D + F1 >= 0 && D + -1*F1 >= 0 && D + D1 >= 0 && D + -1*D1 >= 0 && -2 + D + O >= 0 && -2 + A + D >= 0 && C1 + -1*I1 >= 0 && B1 + -1*H1 >= 0 && -1*B1 + H1 >= 0 && -1*F1 >= 0 && D1 + -1*F1 >= 0 && -1*D1 + -1*F1 >= 0 && -2 + -1*F1 + O >= 0 && -2 + A + -1*F1 >= 0 && F1 >= 0 && D1 + F1 >= 0 && -1*D1 + F1 >= 0 && -2 + F1 + O >= 0 && -2 + A + F1 >= 0 && -1*D1 >= 0 && -2 + -1*D1 + O >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + D1 + O >= 0 && -2 + A + D1 >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && B1 >= 1 + Q1 && I1 >= 0 && M1 >= 2 && O1 >= 1 + Q1 && O1 >= 1 && D1 = 0] f8(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f8(A,B,C,D,E,M1,O1,N,O,B1,C1,0,0,B1,-1 + I1) [-2 + F >= 0 && -2 + D + F >= 0 && -2 + F + F1 >= 0 && -2 + F + -1*F1 >= 0 && -2 + D1 + F >= 0 && -2 + -1*D1 + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && 1 + C1 + -1*E >= 0 && -1 + E + -1*I1 >= 0 && -1 + -1*C1 + E >= 0 && A + -1*D >= 0 && D >= 0 && D + F1 >= 0 && D + -1*F1 >= 0 && D + D1 >= 0 && D + -1*D1 >= 0 && -2 + D + O >= 0 && -2 + A + D >= 0 && C1 + -1*I1 >= 0 && B1 + -1*H1 >= 0 && -1*B1 + H1 >= 0 && -1*F1 >= 0 && D1 + -1*F1 >= 0 && -1*D1 + -1*F1 >= 0 && -2 + -1*F1 + O >= 0 && -2 + A + -1*F1 >= 0 && F1 >= 0 && D1 + F1 >= 0 && -1*D1 + F1 >= 0 && -2 + F1 + O >= 0 && -2 + A + F1 >= 0 && -1*D1 >= 0 && -2 + -1*D1 + O >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + D1 + O >= 0 && -2 + A + D1 >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && B1 >= 1 + Q1 && I1 >= 0 && M1 >= 2 && O1 >= 1 + Q1 && 0 >= 1 + O1 && D1 = 0] f8(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f8(A,B,C,D,E,M1,O1,N,O,B1,C1,0,0,B1,-1 + I1) [-2 + F >= 0 && -2 + D + F >= 0 && -2 + F + F1 >= 0 && -2 + F + -1*F1 >= 0 && -2 + D1 + F >= 0 && -2 + -1*D1 + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && 1 + C1 + -1*E >= 0 && -1 + E + -1*I1 >= 0 && -1 + -1*C1 + E >= 0 && A + -1*D >= 0 && D >= 0 && D + F1 >= 0 && D + -1*F1 >= 0 && D + D1 >= 0 && D + -1*D1 >= 0 && -2 + D + O >= 0 && -2 + A + D >= 0 && C1 + -1*I1 >= 0 && B1 + -1*H1 >= 0 && -1*B1 + H1 >= 0 && -1*F1 >= 0 && D1 + -1*F1 >= 0 && -1*D1 + -1*F1 >= 0 && -2 + -1*F1 + O >= 0 && -2 + A + -1*F1 >= 0 && F1 >= 0 && D1 + F1 >= 0 && -1*D1 + F1 >= 0 && -2 + F1 + O >= 0 && -2 + A + F1 >= 0 && -1*D1 >= 0 && -2 + -1*D1 + O >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + D1 + O >= 0 && -2 + A + D1 >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && Q1 >= 1 + B1 && I1 >= 0 && M1 >= 2 && Q1 >= 1 + O1 && O1 >= 1 && D1 = 0] f8(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f8(A,B,C,D,E,M1,O1,N,O,B1,C1,0,0,B1,-1 + I1) [-2 + F >= 0 && -2 + D + F >= 0 && -2 + F + F1 >= 0 && -2 + F + -1*F1 >= 0 && -2 + D1 + F >= 0 && -2 + -1*D1 + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && 1 + C1 + -1*E >= 0 && -1 + E + -1*I1 >= 0 && -1 + -1*C1 + E >= 0 && A + -1*D >= 0 && D >= 0 && D + F1 >= 0 && D + -1*F1 >= 0 && D + D1 >= 0 && D + -1*D1 >= 0 && -2 + D + O >= 0 && -2 + A + D >= 0 && C1 + -1*I1 >= 0 && B1 + -1*H1 >= 0 && -1*B1 + H1 >= 0 && -1*F1 >= 0 && D1 + -1*F1 >= 0 && -1*D1 + -1*F1 >= 0 && -2 + -1*F1 + O >= 0 && -2 + A + -1*F1 >= 0 && F1 >= 0 && D1 + F1 >= 0 && -1*D1 + F1 >= 0 && -2 + F1 + O >= 0 && -2 + A + F1 >= 0 && -1*D1 >= 0 && -2 + -1*D1 + O >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + D1 + O >= 0 && -2 + A + D1 >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && Q1 >= 1 + B1 && I1 >= 0 && M1 >= 2 && Q1 >= 1 + O1 && 0 >= 1 + O1 && D1 = 0] f8(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f8(A,B,C,D,E,M1,O1,N,O,B1,C1,0,0,B1,-1 + I1) [-2 + F >= 0 && -2 + D + F >= 0 && -2 + F + F1 >= 0 && -2 + F + -1*F1 >= 0 && -2 + D1 + F >= 0 && -2 + -1*D1 + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && 1 + C1 + -1*E >= 0 && -1 + E + -1*I1 >= 0 && -1 + -1*C1 + E >= 0 && A + -1*D >= 0 && D >= 0 && D + F1 >= 0 && D + -1*F1 >= 0 && D + D1 >= 0 && D + -1*D1 >= 0 && -2 + D + O >= 0 && -2 + A + D >= 0 && C1 + -1*I1 >= 0 && B1 + -1*H1 >= 0 && -1*B1 + H1 >= 0 && -1*F1 >= 0 && D1 + -1*F1 >= 0 && -1*D1 + -1*F1 >= 0 && -2 + -1*F1 + O >= 0 && -2 + A + -1*F1 >= 0 && F1 >= 0 && D1 + F1 >= 0 && -1*D1 + F1 >= 0 && -2 + F1 + O >= 0 && -2 + A + F1 >= 0 && -1*D1 >= 0 && -2 + -1*D1 + O >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + D1 + O >= 0 && -2 + A + D1 >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && Q1 >= 1 + B1 && I1 >= 0 && M1 >= 2 && O1 >= 1 + Q1 && O1 >= 1 && D1 = 0] f8(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f8(A,B,C,D,E,M1,O1,N,O,B1,C1,0,0,B1,-1 + I1) [-2 + F >= 0 && -2 + D + F >= 0 && -2 + F + F1 >= 0 && -2 + F + -1*F1 >= 0 && -2 + D1 + F >= 0 && -2 + -1*D1 + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && 1 + C1 + -1*E >= 0 && -1 + E + -1*I1 >= 0 && -1 + -1*C1 + E >= 0 && A + -1*D >= 0 && D >= 0 && D + F1 >= 0 && D + -1*F1 >= 0 && D + D1 >= 0 && D + -1*D1 >= 0 && -2 + D + O >= 0 && -2 + A + D >= 0 && C1 + -1*I1 >= 0 && B1 + -1*H1 >= 0 && -1*B1 + H1 >= 0 && -1*F1 >= 0 && D1 + -1*F1 >= 0 && -1*D1 + -1*F1 >= 0 && -2 + -1*F1 + O >= 0 && -2 + A + -1*F1 >= 0 && F1 >= 0 && D1 + F1 >= 0 && -1*D1 + F1 >= 0 && -2 + F1 + O >= 0 && -2 + A + F1 >= 0 && -1*D1 >= 0 && -2 + -1*D1 + O >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + D1 + O >= 0 && -2 + A + D1 >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && Q1 >= 1 + B1 && I1 >= 0 && M1 >= 2 && O1 >= 1 + Q1 && 0 >= 1 + O1 && D1 = 0] f8(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f8(A,B,C,D,E,M1,O1,N,O,B1,C1,0,0,B1,-1 + I1) [-2 + F >= 0 && -2 + D + F >= 0 && -2 + F + F1 >= 0 && -2 + F + -1*F1 >= 0 && -2 + D1 + F >= 0 && -2 + -1*D1 + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && 1 + C1 + -1*E >= 0 && -1 + E + -1*I1 >= 0 && -1 + -1*C1 + E >= 0 && A + -1*D >= 0 && D >= 0 && D + F1 >= 0 && D + -1*F1 >= 0 && D + D1 >= 0 && D + -1*D1 >= 0 && -2 + D + O >= 0 && -2 + A + D >= 0 && C1 + -1*I1 >= 0 && B1 + -1*H1 >= 0 && -1*B1 + H1 >= 0 && -1*F1 >= 0 && D1 + -1*F1 >= 0 && -1*D1 + -1*F1 >= 0 && -2 + -1*F1 + O >= 0 && -2 + A + -1*F1 >= 0 && F1 >= 0 && D1 + F1 >= 0 && -1*D1 + F1 >= 0 && -2 + F1 + O >= 0 && -2 + A + F1 >= 0 && -1*D1 >= 0 && -2 + -1*D1 + O >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + D1 + O >= 0 && -2 + A + D1 >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && B1 >= 1 + Q1 && I1 >= 0 && M1 >= 2 && Q1 >= 1 + O1 && O1 >= 1 && D1 = 0] f8(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f16(A,B,C,D,E,M1,L,N,O,T1,C1,S1,Q1,U1,I1) [-2 + F >= 0 && -2 + D + F >= 0 && -2 + F + F1 >= 0 && -2 + F + -1*F1 >= 0 && -2 + D1 + F >= 0 && -2 + -1*D1 + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && 1 + C1 + -1*E >= 0 && -1 + E + -1*I1 >= 0 && -1 + -1*C1 + E >= 0 && A + -1*D >= 0 && D >= 0 && D + F1 >= 0 && D + -1*F1 >= 0 && D + D1 >= 0 && D + -1*D1 >= 0 && -2 + D + O >= 0 && -2 + A + D >= 0 && C1 + -1*I1 >= 0 && B1 + -1*H1 >= 0 && -1*B1 + H1 >= 0 && -1*F1 >= 0 && D1 + -1*F1 >= 0 && -1*D1 + -1*F1 >= 0 && -2 + -1*F1 + O >= 0 && -2 + A + -1*F1 >= 0 && F1 >= 0 && D1 + F1 >= 0 && -1*D1 + F1 >= 0 && -2 + F1 + O >= 0 && -2 + A + F1 >= 0 && -1*D1 >= 0 && -2 + -1*D1 + O >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + D1 + O >= 0 && -2 + A + D1 >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && M1 >= 2 && I1 >= 0 && D1 = B1] Signature: {(f1,38);(f14,38);(f15,38);(f16,38);(f8,38)} Rule Graph: [0->{},1->{2,3,4},2->{2,3,4},3->{5,6,7,8,9,10,11,12},4->{5,6,7,8,9,10,11,12},5->{5,6,7,8,9,10,11,12,13} ,6->{5,6,7,8,9,10,11,12,13},7->{5,6,7,8,9,10,11,12,14},8->{5,6,7,8,9,10,11,12,14},9->{5,6,7,8,9,10,11,12,13} ,10->{5,6,7,8,9,10,11,12,13},11->{5,6,7,8,9,10,11,12,14},12->{5,6,7,8,9,10,11,12,14},13->{15,16,17,18,19,20 ,22},14->{15,16,17,18,19,20,21},15->{15,16,17,18,19,20,21,22,23},16->{15,16,17,18,19,20,21,22,23},17->{15,16 ,17,18,19,20,21,22,23},18->{15,16,17,18,19,20,21,22,23},19->{15,16,17,18,19,20,21,22,23},20->{15,16,17,18,19 ,20,21,22,23},21->{15,16,17,18,19,20,21},22->{15,16,17,18,19,20,22},23->{}] + Applied Processor: AddSinks + Details: () * Step 5: Decompose MAYBE + Considered Problem: Rules: f15(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f16(R1,P1,Q1,D,E,O1,0,A2,O,F2,C1,E2,C2,G2,I1) [0 >= V1 && 0 >= W1 && 0 >= O1 && 0 >= X1] f15(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f1(2,O1,P1,D,E,O1,L,N,O,B1,C1,D1,F1,H1,I1) [O1 >= 2] f1(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f1(1 + A,B,K,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) [-2 + F >= 0 && -4 + A + F >= 0 && -2 + A >= 0 && B >= 1 + A && A >= 0] f1(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f14(D,O1,P1,D,0,M1,C,C,N1,B1,C1,D1,F1,H1,I1) [-2 + F >= 0 && -4 + A + F >= 0 && -2 + A >= 0 && A >= B && A >= 0 && M1 >= 2 && C >= 1 && N1 >= M1 && D >= M1 && E = 0] f1(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f14(D,O1,P1,D,0,M1,C,C,N1,B1,C1,D1,F1,H1,I1) [-2 + F >= 0 && -4 + A + F >= 0 && -2 + A >= 0 && A >= B && A >= 0 && M1 >= 2 && 0 >= 1 + C && N1 >= M1 && D >= M1 && E = 0] f14(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f14(A,B,C,-1 + D,1 + E,M1,O1,N,O,B1,C1,D1,F1,H1,I1) [-2 + F >= 0 && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && D >= 0 && M1 >= 2 && R1 >= 1 && O1 >= 1 && Q1 >= 1] f14(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f14(A,B,C,-1 + D,1 + E,M1,O1,N,O,B1,C1,D1,F1,H1,I1) [-2 + F >= 0 && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && D >= 0 && M1 >= 2 && R1 >= 1 && O1 >= 1 && 0 >= 1 + Q1] f14(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f14(A,B,C,-1 + D,1 + E,M1,O1,N,O,B1,C1,D1,F1,H1,I1) [-2 + F >= 0 && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && D >= 0 && M1 >= 2 && R1 >= 1 && 0 >= 1 + O1 && Q1 >= 1] f14(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f14(A,B,C,-1 + D,1 + E,M1,O1,N,O,B1,C1,D1,F1,H1,I1) [-2 + F >= 0 && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && D >= 0 && M1 >= 2 && R1 >= 1 && 0 >= 1 + O1 && 0 >= 1 + Q1] f14(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f14(A,B,C,-1 + D,1 + E,M1,O1,N,O,B1,C1,D1,F1,H1,I1) [-2 + F >= 0 && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && D >= 0 && M1 >= 2 && 0 >= 1 + R1 && O1 >= 1 && Q1 >= 1] f14(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f14(A,B,C,-1 + D,1 + E,M1,O1,N,O,B1,C1,D1,F1,H1,I1) [-2 + F >= 0 && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && D >= 0 && M1 >= 2 && 0 >= 1 + R1 && O1 >= 1 && 0 >= 1 + Q1] f14(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f14(A,B,C,-1 + D,1 + E,M1,O1,N,O,B1,C1,D1,F1,H1,I1) [-2 + F >= 0 && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && D >= 0 && M1 >= 2 && 0 >= 1 + R1 && 0 >= 1 + O1 && Q1 >= 1] f14(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f14(A,B,C,-1 + D,1 + E,M1,O1,N,O,B1,C1,D1,F1,H1,I1) [-2 + F >= 0 && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && D >= 0 && M1 >= 2 && 0 >= 1 + R1 && 0 >= 1 + O1 && 0 >= 1 + Q1] f14(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f8(A,B,C,D,1 + I1,M1,L,P1,O,L,I1,0,0,L,I1) [-2 + F >= 0 && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && Q1 >= 2 && M1 >= 2 && D >= 0 && L >= 1 && N = 0] f14(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f8(A,B,C,D,1 + I1,M1,L,P1,O,L,I1,0,0,L,I1) [-2 + F >= 0 && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && Q1 >= 2 && M1 >= 2 && D >= 0 && 0 >= 1 + L && N = 0] f8(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f8(A,B,C,D,E,M1,O1,N,O,B1,C1,0,0,B1,-1 + I1) [-2 + F >= 0 && -2 + D + F >= 0 && -2 + F + F1 >= 0 && -2 + F + -1*F1 >= 0 && -2 + D1 + F >= 0 && -2 + -1*D1 + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && 1 + C1 + -1*E >= 0 && -1 + E + -1*I1 >= 0 && -1 + -1*C1 + E >= 0 && A + -1*D >= 0 && D >= 0 && D + F1 >= 0 && D + -1*F1 >= 0 && D + D1 >= 0 && D + -1*D1 >= 0 && -2 + D + O >= 0 && -2 + A + D >= 0 && C1 + -1*I1 >= 0 && B1 + -1*H1 >= 0 && -1*B1 + H1 >= 0 && -1*F1 >= 0 && D1 + -1*F1 >= 0 && -1*D1 + -1*F1 >= 0 && -2 + -1*F1 + O >= 0 && -2 + A + -1*F1 >= 0 && F1 >= 0 && D1 + F1 >= 0 && -1*D1 + F1 >= 0 && -2 + F1 + O >= 0 && -2 + A + F1 >= 0 && -1*D1 >= 0 && -2 + -1*D1 + O >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + D1 + O >= 0 && -2 + A + D1 >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && B1 >= 1 + Q1 && I1 >= 0 && M1 >= 2 && Q1 >= 1 + O1 && 0 >= 1 + O1 && D1 = 0] f8(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f8(A,B,C,D,E,M1,O1,N,O,B1,C1,0,0,B1,-1 + I1) [-2 + F >= 0 && -2 + D + F >= 0 && -2 + F + F1 >= 0 && -2 + F + -1*F1 >= 0 && -2 + D1 + F >= 0 && -2 + -1*D1 + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && 1 + C1 + -1*E >= 0 && -1 + E + -1*I1 >= 0 && -1 + -1*C1 + E >= 0 && A + -1*D >= 0 && D >= 0 && D + F1 >= 0 && D + -1*F1 >= 0 && D + D1 >= 0 && D + -1*D1 >= 0 && -2 + D + O >= 0 && -2 + A + D >= 0 && C1 + -1*I1 >= 0 && B1 + -1*H1 >= 0 && -1*B1 + H1 >= 0 && -1*F1 >= 0 && D1 + -1*F1 >= 0 && -1*D1 + -1*F1 >= 0 && -2 + -1*F1 + O >= 0 && -2 + A + -1*F1 >= 0 && F1 >= 0 && D1 + F1 >= 0 && -1*D1 + F1 >= 0 && -2 + F1 + O >= 0 && -2 + A + F1 >= 0 && -1*D1 >= 0 && -2 + -1*D1 + O >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + D1 + O >= 0 && -2 + A + D1 >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && B1 >= 1 + Q1 && I1 >= 0 && M1 >= 2 && O1 >= 1 + Q1 && O1 >= 1 && D1 = 0] f8(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f8(A,B,C,D,E,M1,O1,N,O,B1,C1,0,0,B1,-1 + I1) [-2 + F >= 0 && -2 + D + F >= 0 && -2 + F + F1 >= 0 && -2 + F + -1*F1 >= 0 && -2 + D1 + F >= 0 && -2 + -1*D1 + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && 1 + C1 + -1*E >= 0 && -1 + E + -1*I1 >= 0 && -1 + -1*C1 + E >= 0 && A + -1*D >= 0 && D >= 0 && D + F1 >= 0 && D + -1*F1 >= 0 && D + D1 >= 0 && D + -1*D1 >= 0 && -2 + D + O >= 0 && -2 + A + D >= 0 && C1 + -1*I1 >= 0 && B1 + -1*H1 >= 0 && -1*B1 + H1 >= 0 && -1*F1 >= 0 && D1 + -1*F1 >= 0 && -1*D1 + -1*F1 >= 0 && -2 + -1*F1 + O >= 0 && -2 + A + -1*F1 >= 0 && F1 >= 0 && D1 + F1 >= 0 && -1*D1 + F1 >= 0 && -2 + F1 + O >= 0 && -2 + A + F1 >= 0 && -1*D1 >= 0 && -2 + -1*D1 + O >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + D1 + O >= 0 && -2 + A + D1 >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && B1 >= 1 + Q1 && I1 >= 0 && M1 >= 2 && O1 >= 1 + Q1 && 0 >= 1 + O1 && D1 = 0] f8(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f8(A,B,C,D,E,M1,O1,N,O,B1,C1,0,0,B1,-1 + I1) [-2 + F >= 0 && -2 + D + F >= 0 && -2 + F + F1 >= 0 && -2 + F + -1*F1 >= 0 && -2 + D1 + F >= 0 && -2 + -1*D1 + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && 1 + C1 + -1*E >= 0 && -1 + E + -1*I1 >= 0 && -1 + -1*C1 + E >= 0 && A + -1*D >= 0 && D >= 0 && D + F1 >= 0 && D + -1*F1 >= 0 && D + D1 >= 0 && D + -1*D1 >= 0 && -2 + D + O >= 0 && -2 + A + D >= 0 && C1 + -1*I1 >= 0 && B1 + -1*H1 >= 0 && -1*B1 + H1 >= 0 && -1*F1 >= 0 && D1 + -1*F1 >= 0 && -1*D1 + -1*F1 >= 0 && -2 + -1*F1 + O >= 0 && -2 + A + -1*F1 >= 0 && F1 >= 0 && D1 + F1 >= 0 && -1*D1 + F1 >= 0 && -2 + F1 + O >= 0 && -2 + A + F1 >= 0 && -1*D1 >= 0 && -2 + -1*D1 + O >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + D1 + O >= 0 && -2 + A + D1 >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && Q1 >= 1 + B1 && I1 >= 0 && M1 >= 2 && Q1 >= 1 + O1 && O1 >= 1 && D1 = 0] f8(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f8(A,B,C,D,E,M1,O1,N,O,B1,C1,0,0,B1,-1 + I1) [-2 + F >= 0 && -2 + D + F >= 0 && -2 + F + F1 >= 0 && -2 + F + -1*F1 >= 0 && -2 + D1 + F >= 0 && -2 + -1*D1 + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && 1 + C1 + -1*E >= 0 && -1 + E + -1*I1 >= 0 && -1 + -1*C1 + E >= 0 && A + -1*D >= 0 && D >= 0 && D + F1 >= 0 && D + -1*F1 >= 0 && D + D1 >= 0 && D + -1*D1 >= 0 && -2 + D + O >= 0 && -2 + A + D >= 0 && C1 + -1*I1 >= 0 && B1 + -1*H1 >= 0 && -1*B1 + H1 >= 0 && -1*F1 >= 0 && D1 + -1*F1 >= 0 && -1*D1 + -1*F1 >= 0 && -2 + -1*F1 + O >= 0 && -2 + A + -1*F1 >= 0 && F1 >= 0 && D1 + F1 >= 0 && -1*D1 + F1 >= 0 && -2 + F1 + O >= 0 && -2 + A + F1 >= 0 && -1*D1 >= 0 && -2 + -1*D1 + O >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + D1 + O >= 0 && -2 + A + D1 >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && Q1 >= 1 + B1 && I1 >= 0 && M1 >= 2 && Q1 >= 1 + O1 && 0 >= 1 + O1 && D1 = 0] f8(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f8(A,B,C,D,E,M1,O1,N,O,B1,C1,0,0,B1,-1 + I1) [-2 + F >= 0 && -2 + D + F >= 0 && -2 + F + F1 >= 0 && -2 + F + -1*F1 >= 0 && -2 + D1 + F >= 0 && -2 + -1*D1 + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && 1 + C1 + -1*E >= 0 && -1 + E + -1*I1 >= 0 && -1 + -1*C1 + E >= 0 && A + -1*D >= 0 && D >= 0 && D + F1 >= 0 && D + -1*F1 >= 0 && D + D1 >= 0 && D + -1*D1 >= 0 && -2 + D + O >= 0 && -2 + A + D >= 0 && C1 + -1*I1 >= 0 && B1 + -1*H1 >= 0 && -1*B1 + H1 >= 0 && -1*F1 >= 0 && D1 + -1*F1 >= 0 && -1*D1 + -1*F1 >= 0 && -2 + -1*F1 + O >= 0 && -2 + A + -1*F1 >= 0 && F1 >= 0 && D1 + F1 >= 0 && -1*D1 + F1 >= 0 && -2 + F1 + O >= 0 && -2 + A + F1 >= 0 && -1*D1 >= 0 && -2 + -1*D1 + O >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + D1 + O >= 0 && -2 + A + D1 >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && Q1 >= 1 + B1 && I1 >= 0 && M1 >= 2 && O1 >= 1 + Q1 && O1 >= 1 && D1 = 0] f8(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f8(A,B,C,D,E,M1,O1,N,O,B1,C1,0,0,B1,-1 + I1) [-2 + F >= 0 && -2 + D + F >= 0 && -2 + F + F1 >= 0 && -2 + F + -1*F1 >= 0 && -2 + D1 + F >= 0 && -2 + -1*D1 + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && 1 + C1 + -1*E >= 0 && -1 + E + -1*I1 >= 0 && -1 + -1*C1 + E >= 0 && A + -1*D >= 0 && D >= 0 && D + F1 >= 0 && D + -1*F1 >= 0 && D + D1 >= 0 && D + -1*D1 >= 0 && -2 + D + O >= 0 && -2 + A + D >= 0 && C1 + -1*I1 >= 0 && B1 + -1*H1 >= 0 && -1*B1 + H1 >= 0 && -1*F1 >= 0 && D1 + -1*F1 >= 0 && -1*D1 + -1*F1 >= 0 && -2 + -1*F1 + O >= 0 && -2 + A + -1*F1 >= 0 && F1 >= 0 && D1 + F1 >= 0 && -1*D1 + F1 >= 0 && -2 + F1 + O >= 0 && -2 + A + F1 >= 0 && -1*D1 >= 0 && -2 + -1*D1 + O >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + D1 + O >= 0 && -2 + A + D1 >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && Q1 >= 1 + B1 && I1 >= 0 && M1 >= 2 && O1 >= 1 + Q1 && 0 >= 1 + O1 && D1 = 0] f8(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f8(A,B,C,D,E,M1,O1,N,O,B1,C1,0,0,B1,-1 + I1) [-2 + F >= 0 && -2 + D + F >= 0 && -2 + F + F1 >= 0 && -2 + F + -1*F1 >= 0 && -2 + D1 + F >= 0 && -2 + -1*D1 + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && 1 + C1 + -1*E >= 0 && -1 + E + -1*I1 >= 0 && -1 + -1*C1 + E >= 0 && A + -1*D >= 0 && D >= 0 && D + F1 >= 0 && D + -1*F1 >= 0 && D + D1 >= 0 && D + -1*D1 >= 0 && -2 + D + O >= 0 && -2 + A + D >= 0 && C1 + -1*I1 >= 0 && B1 + -1*H1 >= 0 && -1*B1 + H1 >= 0 && -1*F1 >= 0 && D1 + -1*F1 >= 0 && -1*D1 + -1*F1 >= 0 && -2 + -1*F1 + O >= 0 && -2 + A + -1*F1 >= 0 && F1 >= 0 && D1 + F1 >= 0 && -1*D1 + F1 >= 0 && -2 + F1 + O >= 0 && -2 + A + F1 >= 0 && -1*D1 >= 0 && -2 + -1*D1 + O >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + D1 + O >= 0 && -2 + A + D1 >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && B1 >= 1 + Q1 && I1 >= 0 && M1 >= 2 && Q1 >= 1 + O1 && O1 >= 1 && D1 = 0] f8(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f16(A,B,C,D,E,M1,L,N,O,T1,C1,S1,Q1,U1,I1) [-2 + F >= 0 && -2 + D + F >= 0 && -2 + F + F1 >= 0 && -2 + F + -1*F1 >= 0 && -2 + D1 + F >= 0 && -2 + -1*D1 + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && 1 + C1 + -1*E >= 0 && -1 + E + -1*I1 >= 0 && -1 + -1*C1 + E >= 0 && A + -1*D >= 0 && D >= 0 && D + F1 >= 0 && D + -1*F1 >= 0 && D + D1 >= 0 && D + -1*D1 >= 0 && -2 + D + O >= 0 && -2 + A + D >= 0 && C1 + -1*I1 >= 0 && B1 + -1*H1 >= 0 && -1*B1 + H1 >= 0 && -1*F1 >= 0 && D1 + -1*F1 >= 0 && -1*D1 + -1*F1 >= 0 && -2 + -1*F1 + O >= 0 && -2 + A + -1*F1 >= 0 && F1 >= 0 && D1 + F1 >= 0 && -1*D1 + F1 >= 0 && -2 + F1 + O >= 0 && -2 + A + F1 >= 0 && -1*D1 >= 0 && -2 + -1*D1 + O >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + D1 + O >= 0 && -2 + A + D1 >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && M1 >= 2 && I1 >= 0 && D1 = B1] f16(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> exitus616(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) True f16(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> exitus616(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) True f16(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> exitus616(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) True f16(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> exitus616(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) True f16(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> exitus616(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) True Signature: {(exitus616,15);(f1,38);(f14,38);(f15,38);(f16,38);(f8,38)} Rule Graph: [0->{28},1->{2,3,4},2->{2,3,4},3->{5,6,7,8,9,10,11,12},4->{5,6,7,8,9,10,11,12},5->{5,6,7,8,9,10,11,12,13} ,6->{5,6,7,8,9,10,11,12,13},7->{5,6,7,8,9,10,11,12,14},8->{5,6,7,8,9,10,11,12,14},9->{5,6,7,8,9,10,11,12,13} ,10->{5,6,7,8,9,10,11,12,13},11->{5,6,7,8,9,10,11,12,14},12->{5,6,7,8,9,10,11,12,14},13->{15,16,17,18,19,20 ,22},14->{15,16,17,18,19,20,21},15->{15,16,17,18,19,20,21,22,23},16->{15,16,17,18,19,20,21,22,23},17->{15,16 ,17,18,19,20,21,22,23},18->{15,16,17,18,19,20,21,22,23},19->{15,16,17,18,19,20,21,22,23},20->{15,16,17,18,19 ,20,21,22,23},21->{15,16,17,18,19,20,21},22->{15,16,17,18,19,20,22},23->{24,25,26,27}] + Applied Processor: Decompose Greedy + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28] | +- p:[2] c: [2] | +- p:[5,6,7,8,9,10,11,12] c: [5,6,7,8,9,10,11,12] | `- p:[15,16,17,18,19,20,21,22] c: [15,16,17,18,19,20,21,22] * Step 6: AbstractSize MAYBE + Considered Problem: (Rules: f15(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f16(R1,P1,Q1,D,E,O1,0,A2,O,F2,C1,E2,C2,G2,I1) [0 >= V1 && 0 >= W1 && 0 >= O1 && 0 >= X1] f15(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f1(2,O1,P1,D,E,O1,L,N,O,B1,C1,D1,F1,H1,I1) [O1 >= 2] f1(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f1(1 + A,B,K,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) [-2 + F >= 0 && -4 + A + F >= 0 && -2 + A >= 0 && B >= 1 + A && A >= 0] f1(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f14(D,O1,P1,D,0,M1,C,C,N1,B1,C1,D1,F1,H1,I1) [-2 + F >= 0 && -4 + A + F >= 0 && -2 + A >= 0 && A >= B && A >= 0 && M1 >= 2 && C >= 1 && N1 >= M1 && D >= M1 && E = 0] f1(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f14(D,O1,P1,D,0,M1,C,C,N1,B1,C1,D1,F1,H1,I1) [-2 + F >= 0 && -4 + A + F >= 0 && -2 + A >= 0 && A >= B && A >= 0 && M1 >= 2 && 0 >= 1 + C && N1 >= M1 && D >= M1 && E = 0] f14(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f14(A,B,C,-1 + D,1 + E,M1,O1,N,O,B1,C1,D1,F1,H1,I1) [-2 + F >= 0 && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && D >= 0 && M1 >= 2 && R1 >= 1 && O1 >= 1 && Q1 >= 1] f14(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f14(A,B,C,-1 + D,1 + E,M1,O1,N,O,B1,C1,D1,F1,H1,I1) [-2 + F >= 0 && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && D >= 0 && M1 >= 2 && R1 >= 1 && O1 >= 1 && 0 >= 1 + Q1] f14(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f14(A,B,C,-1 + D,1 + E,M1,O1,N,O,B1,C1,D1,F1,H1,I1) [-2 + F >= 0 && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && D >= 0 && M1 >= 2 && R1 >= 1 && 0 >= 1 + O1 && Q1 >= 1] f14(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f14(A,B,C,-1 + D,1 + E,M1,O1,N,O,B1,C1,D1,F1,H1,I1) [-2 + F >= 0 && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && D >= 0 && M1 >= 2 && R1 >= 1 && 0 >= 1 + O1 && 0 >= 1 + Q1] f14(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f14(A,B,C,-1 + D,1 + E,M1,O1,N,O,B1,C1,D1,F1,H1,I1) [-2 + F >= 0 && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && D >= 0 && M1 >= 2 && 0 >= 1 + R1 && O1 >= 1 && Q1 >= 1] f14(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f14(A,B,C,-1 + D,1 + E,M1,O1,N,O,B1,C1,D1,F1,H1,I1) [-2 + F >= 0 && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && D >= 0 && M1 >= 2 && 0 >= 1 + R1 && O1 >= 1 && 0 >= 1 + Q1] f14(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f14(A,B,C,-1 + D,1 + E,M1,O1,N,O,B1,C1,D1,F1,H1,I1) [-2 + F >= 0 && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && D >= 0 && M1 >= 2 && 0 >= 1 + R1 && 0 >= 1 + O1 && Q1 >= 1] f14(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f14(A,B,C,-1 + D,1 + E,M1,O1,N,O,B1,C1,D1,F1,H1,I1) [-2 + F >= 0 && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && D >= 0 && M1 >= 2 && 0 >= 1 + R1 && 0 >= 1 + O1 && 0 >= 1 + Q1] f14(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f8(A,B,C,D,1 + I1,M1,L,P1,O,L,I1,0,0,L,I1) [-2 + F >= 0 && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && Q1 >= 2 && M1 >= 2 && D >= 0 && L >= 1 && N = 0] f14(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f8(A,B,C,D,1 + I1,M1,L,P1,O,L,I1,0,0,L,I1) [-2 + F >= 0 && -2 + E + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && E >= 0 && -2 + D + E >= 0 && -2 + E + O >= 0 && -2 + A + E >= 0 && A + -1*D >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && Q1 >= 2 && M1 >= 2 && D >= 0 && 0 >= 1 + L && N = 0] f8(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f8(A,B,C,D,E,M1,O1,N,O,B1,C1,0,0,B1,-1 + I1) [-2 + F >= 0 && -2 + D + F >= 0 && -2 + F + F1 >= 0 && -2 + F + -1*F1 >= 0 && -2 + D1 + F >= 0 && -2 + -1*D1 + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && 1 + C1 + -1*E >= 0 && -1 + E + -1*I1 >= 0 && -1 + -1*C1 + E >= 0 && A + -1*D >= 0 && D >= 0 && D + F1 >= 0 && D + -1*F1 >= 0 && D + D1 >= 0 && D + -1*D1 >= 0 && -2 + D + O >= 0 && -2 + A + D >= 0 && C1 + -1*I1 >= 0 && B1 + -1*H1 >= 0 && -1*B1 + H1 >= 0 && -1*F1 >= 0 && D1 + -1*F1 >= 0 && -1*D1 + -1*F1 >= 0 && -2 + -1*F1 + O >= 0 && -2 + A + -1*F1 >= 0 && F1 >= 0 && D1 + F1 >= 0 && -1*D1 + F1 >= 0 && -2 + F1 + O >= 0 && -2 + A + F1 >= 0 && -1*D1 >= 0 && -2 + -1*D1 + O >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + D1 + O >= 0 && -2 + A + D1 >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && B1 >= 1 + Q1 && I1 >= 0 && M1 >= 2 && Q1 >= 1 + O1 && 0 >= 1 + O1 && D1 = 0] f8(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f8(A,B,C,D,E,M1,O1,N,O,B1,C1,0,0,B1,-1 + I1) [-2 + F >= 0 && -2 + D + F >= 0 && -2 + F + F1 >= 0 && -2 + F + -1*F1 >= 0 && -2 + D1 + F >= 0 && -2 + -1*D1 + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && 1 + C1 + -1*E >= 0 && -1 + E + -1*I1 >= 0 && -1 + -1*C1 + E >= 0 && A + -1*D >= 0 && D >= 0 && D + F1 >= 0 && D + -1*F1 >= 0 && D + D1 >= 0 && D + -1*D1 >= 0 && -2 + D + O >= 0 && -2 + A + D >= 0 && C1 + -1*I1 >= 0 && B1 + -1*H1 >= 0 && -1*B1 + H1 >= 0 && -1*F1 >= 0 && D1 + -1*F1 >= 0 && -1*D1 + -1*F1 >= 0 && -2 + -1*F1 + O >= 0 && -2 + A + -1*F1 >= 0 && F1 >= 0 && D1 + F1 >= 0 && -1*D1 + F1 >= 0 && -2 + F1 + O >= 0 && -2 + A + F1 >= 0 && -1*D1 >= 0 && -2 + -1*D1 + O >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + D1 + O >= 0 && -2 + A + D1 >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && B1 >= 1 + Q1 && I1 >= 0 && M1 >= 2 && O1 >= 1 + Q1 && O1 >= 1 && D1 = 0] f8(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f8(A,B,C,D,E,M1,O1,N,O,B1,C1,0,0,B1,-1 + I1) [-2 + F >= 0 && -2 + D + F >= 0 && -2 + F + F1 >= 0 && -2 + F + -1*F1 >= 0 && -2 + D1 + F >= 0 && -2 + -1*D1 + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && 1 + C1 + -1*E >= 0 && -1 + E + -1*I1 >= 0 && -1 + -1*C1 + E >= 0 && A + -1*D >= 0 && D >= 0 && D + F1 >= 0 && D + -1*F1 >= 0 && D + D1 >= 0 && D + -1*D1 >= 0 && -2 + D + O >= 0 && -2 + A + D >= 0 && C1 + -1*I1 >= 0 && B1 + -1*H1 >= 0 && -1*B1 + H1 >= 0 && -1*F1 >= 0 && D1 + -1*F1 >= 0 && -1*D1 + -1*F1 >= 0 && -2 + -1*F1 + O >= 0 && -2 + A + -1*F1 >= 0 && F1 >= 0 && D1 + F1 >= 0 && -1*D1 + F1 >= 0 && -2 + F1 + O >= 0 && -2 + A + F1 >= 0 && -1*D1 >= 0 && -2 + -1*D1 + O >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + D1 + O >= 0 && -2 + A + D1 >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && B1 >= 1 + Q1 && I1 >= 0 && M1 >= 2 && O1 >= 1 + Q1 && 0 >= 1 + O1 && D1 = 0] f8(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f8(A,B,C,D,E,M1,O1,N,O,B1,C1,0,0,B1,-1 + I1) [-2 + F >= 0 && -2 + D + F >= 0 && -2 + F + F1 >= 0 && -2 + F + -1*F1 >= 0 && -2 + D1 + F >= 0 && -2 + -1*D1 + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && 1 + C1 + -1*E >= 0 && -1 + E + -1*I1 >= 0 && -1 + -1*C1 + E >= 0 && A + -1*D >= 0 && D >= 0 && D + F1 >= 0 && D + -1*F1 >= 0 && D + D1 >= 0 && D + -1*D1 >= 0 && -2 + D + O >= 0 && -2 + A + D >= 0 && C1 + -1*I1 >= 0 && B1 + -1*H1 >= 0 && -1*B1 + H1 >= 0 && -1*F1 >= 0 && D1 + -1*F1 >= 0 && -1*D1 + -1*F1 >= 0 && -2 + -1*F1 + O >= 0 && -2 + A + -1*F1 >= 0 && F1 >= 0 && D1 + F1 >= 0 && -1*D1 + F1 >= 0 && -2 + F1 + O >= 0 && -2 + A + F1 >= 0 && -1*D1 >= 0 && -2 + -1*D1 + O >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + D1 + O >= 0 && -2 + A + D1 >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && Q1 >= 1 + B1 && I1 >= 0 && M1 >= 2 && Q1 >= 1 + O1 && O1 >= 1 && D1 = 0] f8(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f8(A,B,C,D,E,M1,O1,N,O,B1,C1,0,0,B1,-1 + I1) [-2 + F >= 0 && -2 + D + F >= 0 && -2 + F + F1 >= 0 && -2 + F + -1*F1 >= 0 && -2 + D1 + F >= 0 && -2 + -1*D1 + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && 1 + C1 + -1*E >= 0 && -1 + E + -1*I1 >= 0 && -1 + -1*C1 + E >= 0 && A + -1*D >= 0 && D >= 0 && D + F1 >= 0 && D + -1*F1 >= 0 && D + D1 >= 0 && D + -1*D1 >= 0 && -2 + D + O >= 0 && -2 + A + D >= 0 && C1 + -1*I1 >= 0 && B1 + -1*H1 >= 0 && -1*B1 + H1 >= 0 && -1*F1 >= 0 && D1 + -1*F1 >= 0 && -1*D1 + -1*F1 >= 0 && -2 + -1*F1 + O >= 0 && -2 + A + -1*F1 >= 0 && F1 >= 0 && D1 + F1 >= 0 && -1*D1 + F1 >= 0 && -2 + F1 + O >= 0 && -2 + A + F1 >= 0 && -1*D1 >= 0 && -2 + -1*D1 + O >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + D1 + O >= 0 && -2 + A + D1 >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && Q1 >= 1 + B1 && I1 >= 0 && M1 >= 2 && Q1 >= 1 + O1 && 0 >= 1 + O1 && D1 = 0] f8(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f8(A,B,C,D,E,M1,O1,N,O,B1,C1,0,0,B1,-1 + I1) [-2 + F >= 0 && -2 + D + F >= 0 && -2 + F + F1 >= 0 && -2 + F + -1*F1 >= 0 && -2 + D1 + F >= 0 && -2 + -1*D1 + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && 1 + C1 + -1*E >= 0 && -1 + E + -1*I1 >= 0 && -1 + -1*C1 + E >= 0 && A + -1*D >= 0 && D >= 0 && D + F1 >= 0 && D + -1*F1 >= 0 && D + D1 >= 0 && D + -1*D1 >= 0 && -2 + D + O >= 0 && -2 + A + D >= 0 && C1 + -1*I1 >= 0 && B1 + -1*H1 >= 0 && -1*B1 + H1 >= 0 && -1*F1 >= 0 && D1 + -1*F1 >= 0 && -1*D1 + -1*F1 >= 0 && -2 + -1*F1 + O >= 0 && -2 + A + -1*F1 >= 0 && F1 >= 0 && D1 + F1 >= 0 && -1*D1 + F1 >= 0 && -2 + F1 + O >= 0 && -2 + A + F1 >= 0 && -1*D1 >= 0 && -2 + -1*D1 + O >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + D1 + O >= 0 && -2 + A + D1 >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && Q1 >= 1 + B1 && I1 >= 0 && M1 >= 2 && O1 >= 1 + Q1 && O1 >= 1 && D1 = 0] f8(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f8(A,B,C,D,E,M1,O1,N,O,B1,C1,0,0,B1,-1 + I1) [-2 + F >= 0 && -2 + D + F >= 0 && -2 + F + F1 >= 0 && -2 + F + -1*F1 >= 0 && -2 + D1 + F >= 0 && -2 + -1*D1 + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && 1 + C1 + -1*E >= 0 && -1 + E + -1*I1 >= 0 && -1 + -1*C1 + E >= 0 && A + -1*D >= 0 && D >= 0 && D + F1 >= 0 && D + -1*F1 >= 0 && D + D1 >= 0 && D + -1*D1 >= 0 && -2 + D + O >= 0 && -2 + A + D >= 0 && C1 + -1*I1 >= 0 && B1 + -1*H1 >= 0 && -1*B1 + H1 >= 0 && -1*F1 >= 0 && D1 + -1*F1 >= 0 && -1*D1 + -1*F1 >= 0 && -2 + -1*F1 + O >= 0 && -2 + A + -1*F1 >= 0 && F1 >= 0 && D1 + F1 >= 0 && -1*D1 + F1 >= 0 && -2 + F1 + O >= 0 && -2 + A + F1 >= 0 && -1*D1 >= 0 && -2 + -1*D1 + O >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + D1 + O >= 0 && -2 + A + D1 >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && Q1 >= 1 + B1 && I1 >= 0 && M1 >= 2 && O1 >= 1 + Q1 && 0 >= 1 + O1 && D1 = 0] f8(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f8(A,B,C,D,E,M1,O1,N,O,B1,C1,0,0,B1,-1 + I1) [-2 + F >= 0 && -2 + D + F >= 0 && -2 + F + F1 >= 0 && -2 + F + -1*F1 >= 0 && -2 + D1 + F >= 0 && -2 + -1*D1 + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && 1 + C1 + -1*E >= 0 && -1 + E + -1*I1 >= 0 && -1 + -1*C1 + E >= 0 && A + -1*D >= 0 && D >= 0 && D + F1 >= 0 && D + -1*F1 >= 0 && D + D1 >= 0 && D + -1*D1 >= 0 && -2 + D + O >= 0 && -2 + A + D >= 0 && C1 + -1*I1 >= 0 && B1 + -1*H1 >= 0 && -1*B1 + H1 >= 0 && -1*F1 >= 0 && D1 + -1*F1 >= 0 && -1*D1 + -1*F1 >= 0 && -2 + -1*F1 + O >= 0 && -2 + A + -1*F1 >= 0 && F1 >= 0 && D1 + F1 >= 0 && -1*D1 + F1 >= 0 && -2 + F1 + O >= 0 && -2 + A + F1 >= 0 && -1*D1 >= 0 && -2 + -1*D1 + O >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + D1 + O >= 0 && -2 + A + D1 >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && B1 >= 1 + Q1 && I1 >= 0 && M1 >= 2 && Q1 >= 1 + O1 && O1 >= 1 && D1 = 0] f8(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> f16(A,B,C,D,E,M1,L,N,O,T1,C1,S1,Q1,U1,I1) [-2 + F >= 0 && -2 + D + F >= 0 && -2 + F + F1 >= 0 && -2 + F + -1*F1 >= 0 && -2 + D1 + F >= 0 && -2 + -1*D1 + F >= 0 && -4 + F + O >= 0 && -4 + A + F >= 0 && 1 + C1 + -1*E >= 0 && -1 + E + -1*I1 >= 0 && -1 + -1*C1 + E >= 0 && A + -1*D >= 0 && D >= 0 && D + F1 >= 0 && D + -1*F1 >= 0 && D + D1 >= 0 && D + -1*D1 >= 0 && -2 + D + O >= 0 && -2 + A + D >= 0 && C1 + -1*I1 >= 0 && B1 + -1*H1 >= 0 && -1*B1 + H1 >= 0 && -1*F1 >= 0 && D1 + -1*F1 >= 0 && -1*D1 + -1*F1 >= 0 && -2 + -1*F1 + O >= 0 && -2 + A + -1*F1 >= 0 && F1 >= 0 && D1 + F1 >= 0 && -1*D1 + F1 >= 0 && -2 + F1 + O >= 0 && -2 + A + F1 >= 0 && -1*D1 >= 0 && -2 + -1*D1 + O >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + D1 + O >= 0 && -2 + A + D1 >= 0 && -2 + O >= 0 && -4 + A + O >= 0 && -2 + A >= 0 && M1 >= 2 && I1 >= 0 && D1 = B1] f16(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> exitus616(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) True f16(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> exitus616(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) True f16(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> exitus616(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) True f16(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> exitus616(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) True f16(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) -> exitus616(A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1) True Signature: {(exitus616,15);(f1,38);(f14,38);(f15,38);(f16,38);(f8,38)} Rule Graph: [0->{28},1->{2,3,4},2->{2,3,4},3->{5,6,7,8,9,10,11,12},4->{5,6,7,8,9,10,11,12},5->{5,6,7,8,9,10,11,12,13} ,6->{5,6,7,8,9,10,11,12,13},7->{5,6,7,8,9,10,11,12,14},8->{5,6,7,8,9,10,11,12,14},9->{5,6,7,8,9,10,11,12,13} ,10->{5,6,7,8,9,10,11,12,13},11->{5,6,7,8,9,10,11,12,14},12->{5,6,7,8,9,10,11,12,14},13->{15,16,17,18,19,20 ,22},14->{15,16,17,18,19,20,21},15->{15,16,17,18,19,20,21,22,23},16->{15,16,17,18,19,20,21,22,23},17->{15,16 ,17,18,19,20,21,22,23},18->{15,16,17,18,19,20,21,22,23},19->{15,16,17,18,19,20,21,22,23},20->{15,16,17,18,19 ,20,21,22,23},21->{15,16,17,18,19,20,21},22->{15,16,17,18,19,20,22},23->{24,25,26,27}] ,We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28] | +- p:[2] c: [2] | +- p:[5,6,7,8,9,10,11,12] c: [5,6,7,8,9,10,11,12] | `- p:[15,16,17,18,19,20,21,22] c: [15,16,17,18,19,20,21,22]) + Applied Processor: AbstractSize Minimize + Details: () * Step 7: AbstractFlow MAYBE + Considered Problem: Program: Domain: [A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1,0.0,0.1,0.2] f15 ~> f16 [A <= unknown, B <= unknown, C <= unknown, D <= D, E <= E, F <= unknown, L <= 0*K, N <= unknown, O <= O, B1 <= unknown, C1 <= C1, D1 <= unknown, F1 <= unknown, H1 <= unknown, I1 <= I1] f15 ~> f1 [A <= 2*K, B <= unknown, C <= unknown, D <= D, E <= E, F <= unknown, L <= L, N <= N, O <= O, B1 <= B1, C1 <= C1, D1 <= D1, F1 <= F1, H1 <= H1, I1 <= I1] f1 ~> f1 [A <= B, B <= B, C <= unknown, D <= D, E <= E, F <= F, L <= L, N <= N, O <= O, B1 <= B1, C1 <= C1, D1 <= D1, F1 <= F1, H1 <= H1, I1 <= I1] f1 ~> f14 [A <= D, B <= unknown, C <= unknown, D <= D, E <= 0*K, F <= D, L <= C, N <= C, O <= unknown, B1 <= B1, C1 <= C1, D1 <= D1, F1 <= F1, H1 <= H1, I1 <= I1] f1 ~> f14 [A <= D, B <= unknown, C <= unknown, D <= D, E <= 0*K, F <= D, L <= C, N <= C, O <= unknown, B1 <= B1, C1 <= C1, D1 <= D1, F1 <= F1, H1 <= H1, I1 <= I1] f14 ~> f14 [A <= A, B <= B, C <= C, D <= A, E <= A + E, F <= unknown, L <= unknown, N <= N, O <= O, B1 <= B1, C1 <= C1, D1 <= D1, F1 <= F1, H1 <= H1, I1 <= I1] f14 ~> f14 [A <= A, B <= B, C <= C, D <= A, E <= A + E, F <= unknown, L <= unknown, N <= N, O <= O, B1 <= B1, C1 <= C1, D1 <= D1, F1 <= F1, H1 <= H1, I1 <= I1] f14 ~> f14 [A <= A, B <= B, C <= C, D <= A, E <= A + E, F <= unknown, L <= unknown, N <= N, O <= O, B1 <= B1, C1 <= C1, D1 <= D1, F1 <= F1, H1 <= H1, I1 <= I1] f14 ~> f14 [A <= A, B <= B, C <= C, D <= A, E <= A + E, F <= unknown, L <= unknown, N <= N, O <= O, B1 <= B1, C1 <= C1, D1 <= D1, F1 <= F1, H1 <= H1, I1 <= I1] f14 ~> f14 [A <= A, B <= B, C <= C, D <= A, E <= A + E, F <= unknown, L <= unknown, N <= N, O <= O, B1 <= B1, C1 <= C1, D1 <= D1, F1 <= F1, H1 <= H1, I1 <= I1] f14 ~> f14 [A <= A, B <= B, C <= C, D <= A, E <= A + E, F <= unknown, L <= unknown, N <= N, O <= O, B1 <= B1, C1 <= C1, D1 <= D1, F1 <= F1, H1 <= H1, I1 <= I1] f14 ~> f14 [A <= A, B <= B, C <= C, D <= A, E <= A + E, F <= unknown, L <= unknown, N <= N, O <= O, B1 <= B1, C1 <= C1, D1 <= D1, F1 <= F1, H1 <= H1, I1 <= I1] f14 ~> f14 [A <= A, B <= B, C <= C, D <= A, E <= A + E, F <= unknown, L <= unknown, N <= N, O <= O, B1 <= B1, C1 <= C1, D1 <= D1, F1 <= F1, H1 <= H1, I1 <= I1] f14 ~> f8 [A <= A, B <= B, C <= C, D <= D, E <= K + I1, F <= unknown, L <= L, N <= unknown, O <= O, B1 <= L, C1 <= I1, D1 <= 0*K, F1 <= 0*K, H1 <= L, I1 <= I1] f14 ~> f8 [A <= A, B <= B, C <= C, D <= D, E <= K + I1, F <= unknown, L <= L, N <= unknown, O <= O, B1 <= L, C1 <= I1, D1 <= 0*K, F1 <= 0*K, H1 <= L, I1 <= I1] f8 ~> f8 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= unknown, L <= unknown, N <= N, O <= O, B1 <= B1, C1 <= C1, D1 <= 0*K, F1 <= 0*K, H1 <= B1, I1 <= E] f8 ~> f8 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= unknown, L <= unknown, N <= N, O <= O, B1 <= B1, C1 <= C1, D1 <= 0*K, F1 <= 0*K, H1 <= B1, I1 <= E] f8 ~> f8 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= unknown, L <= unknown, N <= N, O <= O, B1 <= B1, C1 <= C1, D1 <= 0*K, F1 <= 0*K, H1 <= B1, I1 <= E] f8 ~> f8 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= unknown, L <= unknown, N <= N, O <= O, B1 <= B1, C1 <= C1, D1 <= 0*K, F1 <= 0*K, H1 <= B1, I1 <= E] f8 ~> f8 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= unknown, L <= unknown, N <= N, O <= O, B1 <= B1, C1 <= C1, D1 <= 0*K, F1 <= 0*K, H1 <= B1, I1 <= E] f8 ~> f8 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= unknown, L <= unknown, N <= N, O <= O, B1 <= B1, C1 <= C1, D1 <= 0*K, F1 <= 0*K, H1 <= B1, I1 <= E] f8 ~> f8 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= unknown, L <= H1, N <= N, O <= O, B1 <= B1, C1 <= C1, D1 <= 0*K, F1 <= 0*K, H1 <= B1, I1 <= E] f8 ~> f8 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= unknown, L <= H1, N <= N, O <= O, B1 <= B1, C1 <= C1, D1 <= 0*K, F1 <= 0*K, H1 <= B1, I1 <= E] f8 ~> f16 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= unknown, L <= L, N <= N, O <= O, B1 <= unknown, C1 <= C1, D1 <= unknown, F1 <= unknown, H1 <= unknown, I1 <= I1] f16 ~> exitus616 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, L <= L, N <= N, O <= O, B1 <= B1, C1 <= C1, D1 <= D1, F1 <= F1, H1 <= H1, I1 <= I1] f16 ~> exitus616 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, L <= L, N <= N, O <= O, B1 <= B1, C1 <= C1, D1 <= D1, F1 <= F1, H1 <= H1, I1 <= I1] f16 ~> exitus616 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, L <= L, N <= N, O <= O, B1 <= B1, C1 <= C1, D1 <= D1, F1 <= F1, H1 <= H1, I1 <= I1] f16 ~> exitus616 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, L <= L, N <= N, O <= O, B1 <= B1, C1 <= C1, D1 <= D1, F1 <= F1, H1 <= H1, I1 <= I1] f16 ~> exitus616 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, L <= L, N <= N, O <= O, B1 <= B1, C1 <= C1, D1 <= D1, F1 <= F1, H1 <= H1, I1 <= I1] + Loop: [0.0 <= K + A + B] f1 ~> f1 [A <= B, B <= B, C <= unknown, D <= D, E <= E, F <= F, L <= L, N <= N, O <= O, B1 <= B1, C1 <= C1, D1 <= D1, F1 <= F1, H1 <= H1, I1 <= I1] + Loop: [0.1 <= D] f14 ~> f14 [A <= A, B <= B, C <= C, D <= A, E <= A + E, F <= unknown, L <= unknown, N <= N, O <= O, B1 <= B1, C1 <= C1, D1 <= D1, F1 <= F1, H1 <= H1, I1 <= I1] f14 ~> f14 [A <= A, B <= B, C <= C, D <= A, E <= A + E, F <= unknown, L <= unknown, N <= N, O <= O, B1 <= B1, C1 <= C1, D1 <= D1, F1 <= F1, H1 <= H1, I1 <= I1] f14 ~> f14 [A <= A, B <= B, C <= C, D <= A, E <= A + E, F <= unknown, L <= unknown, N <= N, O <= O, B1 <= B1, C1 <= C1, D1 <= D1, F1 <= F1, H1 <= H1, I1 <= I1] f14 ~> f14 [A <= A, B <= B, C <= C, D <= A, E <= A + E, F <= unknown, L <= unknown, N <= N, O <= O, B1 <= B1, C1 <= C1, D1 <= D1, F1 <= F1, H1 <= H1, I1 <= I1] f14 ~> f14 [A <= A, B <= B, C <= C, D <= A, E <= A + E, F <= unknown, L <= unknown, N <= N, O <= O, B1 <= B1, C1 <= C1, D1 <= D1, F1 <= F1, H1 <= H1, I1 <= I1] f14 ~> f14 [A <= A, B <= B, C <= C, D <= A, E <= A + E, F <= unknown, L <= unknown, N <= N, O <= O, B1 <= B1, C1 <= C1, D1 <= D1, F1 <= F1, H1 <= H1, I1 <= I1] f14 ~> f14 [A <= A, B <= B, C <= C, D <= A, E <= A + E, F <= unknown, L <= unknown, N <= N, O <= O, B1 <= B1, C1 <= C1, D1 <= D1, F1 <= F1, H1 <= H1, I1 <= I1] f14 ~> f14 [A <= A, B <= B, C <= C, D <= A, E <= A + E, F <= unknown, L <= unknown, N <= N, O <= O, B1 <= B1, C1 <= C1, D1 <= D1, F1 <= F1, H1 <= H1, I1 <= I1] + Loop: [0.2 <= I1] f8 ~> f8 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= unknown, L <= unknown, N <= N, O <= O, B1 <= B1, C1 <= C1, D1 <= 0*K, F1 <= 0*K, H1 <= B1, I1 <= E] f8 ~> f8 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= unknown, L <= unknown, N <= N, O <= O, B1 <= B1, C1 <= C1, D1 <= 0*K, F1 <= 0*K, H1 <= B1, I1 <= E] f8 ~> f8 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= unknown, L <= unknown, N <= N, O <= O, B1 <= B1, C1 <= C1, D1 <= 0*K, F1 <= 0*K, H1 <= B1, I1 <= E] f8 ~> f8 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= unknown, L <= unknown, N <= N, O <= O, B1 <= B1, C1 <= C1, D1 <= 0*K, F1 <= 0*K, H1 <= B1, I1 <= E] f8 ~> f8 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= unknown, L <= unknown, N <= N, O <= O, B1 <= B1, C1 <= C1, D1 <= 0*K, F1 <= 0*K, H1 <= B1, I1 <= E] f8 ~> f8 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= unknown, L <= unknown, N <= N, O <= O, B1 <= B1, C1 <= C1, D1 <= 0*K, F1 <= 0*K, H1 <= B1, I1 <= E] f8 ~> f8 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= unknown, L <= H1, N <= N, O <= O, B1 <= B1, C1 <= C1, D1 <= 0*K, F1 <= 0*K, H1 <= B1, I1 <= E] f8 ~> f8 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= unknown, L <= H1, N <= N, O <= O, B1 <= B1, C1 <= C1, D1 <= 0*K, F1 <= 0*K, H1 <= B1, I1 <= E] + Applied Processor: AbstractFlow + Details: () * Step 8: Failure MAYBE + Considered Problem: Program: Domain: [tick,huge,K,A,B,C,D,E,F,L,N,O,B1,C1,D1,F1,H1,I1,0.0,0.1,0.2] f15 ~> f16 [K ~=> L ,huge ~=> A ,huge ~=> B ,huge ~=> B1 ,huge ~=> C ,huge ~=> D1 ,huge ~=> F ,huge ~=> F1 ,huge ~=> H1 ,huge ~=> N] f15 ~> f1 [K ~=> A,huge ~=> B,huge ~=> C,huge ~=> F] f1 ~> f1 [B ~=> A,huge ~=> C] f1 ~> f14 [C ~=> L,C ~=> N,D ~=> A,D ~=> F,K ~=> E,huge ~=> B,huge ~=> C,huge ~=> O] f1 ~> f14 [C ~=> L,C ~=> N,D ~=> A,D ~=> F,K ~=> E,huge ~=> B,huge ~=> C,huge ~=> O] f14 ~> f14 [A ~=> D,huge ~=> F,huge ~=> L,A ~+> E,E ~+> E] f14 ~> f14 [A ~=> D,huge ~=> F,huge ~=> L,A ~+> E,E ~+> E] f14 ~> f14 [A ~=> D,huge ~=> F,huge ~=> L,A ~+> E,E ~+> E] f14 ~> f14 [A ~=> D,huge ~=> F,huge ~=> L,A ~+> E,E ~+> E] f14 ~> f14 [A ~=> D,huge ~=> F,huge ~=> L,A ~+> E,E ~+> E] f14 ~> f14 [A ~=> D,huge ~=> F,huge ~=> L,A ~+> E,E ~+> E] f14 ~> f14 [A ~=> D,huge ~=> F,huge ~=> L,A ~+> E,E ~+> E] f14 ~> f14 [A ~=> D,huge ~=> F,huge ~=> L,A ~+> E,E ~+> E] f14 ~> f8 [I1 ~=> C1,L ~=> B1,L ~=> H1,K ~=> D1,K ~=> F1,huge ~=> F,huge ~=> N,I1 ~+> E,K ~+> E] f14 ~> f8 [I1 ~=> C1,L ~=> B1,L ~=> H1,K ~=> D1,K ~=> F1,huge ~=> F,huge ~=> N,I1 ~+> E,K ~+> E] f8 ~> f8 [B1 ~=> H1,E ~=> I1,K ~=> D1,K ~=> F1,huge ~=> F,huge ~=> L] f8 ~> f8 [B1 ~=> H1,E ~=> I1,K ~=> D1,K ~=> F1,huge ~=> F,huge ~=> L] f8 ~> f8 [B1 ~=> H1,E ~=> I1,K ~=> D1,K ~=> F1,huge ~=> F,huge ~=> L] f8 ~> f8 [B1 ~=> H1,E ~=> I1,K ~=> D1,K ~=> F1,huge ~=> F,huge ~=> L] f8 ~> f8 [B1 ~=> H1,E ~=> I1,K ~=> D1,K ~=> F1,huge ~=> F,huge ~=> L] f8 ~> f8 [B1 ~=> H1,E ~=> I1,K ~=> D1,K ~=> F1,huge ~=> F,huge ~=> L] f8 ~> f8 [B1 ~=> H1,E ~=> I1,H1 ~=> L,K ~=> D1,K ~=> F1,huge ~=> F] f8 ~> f8 [B1 ~=> H1,E ~=> I1,H1 ~=> L,K ~=> D1,K ~=> F1,huge ~=> F] f8 ~> f16 [huge ~=> B1,huge ~=> D1,huge ~=> F,huge ~=> F1,huge ~=> H1] f16 ~> exitus616 [] f16 ~> exitus616 [] f16 ~> exitus616 [] f16 ~> exitus616 [] f16 ~> exitus616 [] + Loop: [A ~+> 0.0,B ~+> 0.0,K ~+> 0.0] f1 ~> f1 [B ~=> A,huge ~=> C] + Loop: [D ~=> 0.1] f14 ~> f14 [A ~=> D,huge ~=> F,huge ~=> L,A ~+> E,E ~+> E] f14 ~> f14 [A ~=> D,huge ~=> F,huge ~=> L,A ~+> E,E ~+> E] f14 ~> f14 [A ~=> D,huge ~=> F,huge ~=> L,A ~+> E,E ~+> E] f14 ~> f14 [A ~=> D,huge ~=> F,huge ~=> L,A ~+> E,E ~+> E] f14 ~> f14 [A ~=> D,huge ~=> F,huge ~=> L,A ~+> E,E ~+> E] f14 ~> f14 [A ~=> D,huge ~=> F,huge ~=> L,A ~+> E,E ~+> E] f14 ~> f14 [A ~=> D,huge ~=> F,huge ~=> L,A ~+> E,E ~+> E] f14 ~> f14 [A ~=> D,huge ~=> F,huge ~=> L,A ~+> E,E ~+> E] + Loop: [I1 ~=> 0.2] f8 ~> f8 [B1 ~=> H1,E ~=> I1,K ~=> D1,K ~=> F1,huge ~=> F,huge ~=> L] f8 ~> f8 [B1 ~=> H1,E ~=> I1,K ~=> D1,K ~=> F1,huge ~=> F,huge ~=> L] f8 ~> f8 [B1 ~=> H1,E ~=> I1,K ~=> D1,K ~=> F1,huge ~=> F,huge ~=> L] f8 ~> f8 [B1 ~=> H1,E ~=> I1,K ~=> D1,K ~=> F1,huge ~=> F,huge ~=> L] f8 ~> f8 [B1 ~=> H1,E ~=> I1,K ~=> D1,K ~=> F1,huge ~=> F,huge ~=> L] f8 ~> f8 [B1 ~=> H1,E ~=> I1,K ~=> D1,K ~=> F1,huge ~=> F,huge ~=> L] f8 ~> f8 [B1 ~=> H1,E ~=> I1,H1 ~=> L,K ~=> D1,K ~=> F1,huge ~=> F] f8 ~> f8 [B1 ~=> H1,E ~=> I1,H1 ~=> L,K ~=> D1,K ~=> F1,huge ~=> F] + Applied Processor: Lare + Details: Unknown bound. MAYBE