MAYBE * Step 1: TrivialSCCs MAYBE + Considered Problem: Rules: 0. f9(A,B,C,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) -> f10(T1,B,1,S1,E,F,G,H,I,J,K,L,0,N,O,P,R1,Y1,B2,A2,U,V,Z1,C2,D2,Z,A1,Q1,M1,O1,P1,E2,N1,H1,I1,U1,K1,L1) [S = 0] (1,1) 1. f9(A,B,C,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) -> f10(T1,B,M1,0,E,F,G,H,I,J,K,L,0,N,O,P,R1,Y1,B2,A2,U,V,Z1,C2,D2,Z,A1,N1,O1,P1,Q1,E2,S1,H1,I1,U1,K1,L1) [0 >= V1 && 0 >= W1 && 0 >= M1 && 0 >= X1] (1,1) 2. f9(A,B,C,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,B,M1,D,E,F,G,H,I,J,K,L,M,N,O,P,M1,P1,Q1,P1,U,V,P1,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,O1,N1,2) [M1 >= 2] (1,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) -> f16(G,0,M1,R,E,F,G,H,I,J,K,L,R,N,O,P,O1,P1,S1,N1,U,V,Q1,T1,U1,R1,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) [2 + -1*L1 >= 0 (?,1) && -1*L1 + Q >= 0 && A + -1*L1 >= 0 && -2 + L1 >= 0 && -4 + L1 + Q >= 0 && -4 + A + L1 >= 0 && -2 + Q >= 0 && -4 + A + Q >= 0 && -1*A + Q >= 0 && -2 + A >= 0 && A >= Q && A >= 0 && M1 >= 2 && R1 >= M1 && G >= M1 && B = 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) -> f1(1 + A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,S,M1,S,O1,A,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) [2 + -1*L1 >= 0 (?,1) && -1*L1 + Q >= 0 && A + -1*L1 >= 0 && -2 + L1 >= 0 && -4 + L1 + Q >= 0 && -4 + A + L1 >= 0 && -2 + Q >= 0 && -4 + A + Q >= 0 && -1*A + Q >= 0 && -2 + A >= 0 && Q >= 1 + A && A >= 0] 5. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,1 + H1,M1,D,E,F,G,H,I,J,K,L,0,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,H1,0,D,0,D,D,D,H1,I1,J1,K1,L1) [A + -1*G >= 0 (?,1) && -2 + B + G >= 0 && 2 + -1*L1 >= 0 && C + -1*L1 >= 0 && -1*L1 + Z >= 0 && 2 + B + -1*L1 >= 0 && A + -1*L1 >= 0 && -2 + L1 >= 0 && -4 + C + L1 >= 0 && -4 + L1 + Z >= 0 && -2 + B + L1 >= 0 && -4 + A + L1 >= 0 && -2 + C >= 0 && -4 + C + Z >= 0 && -2 + B + C >= 0 && -4 + A + C >= 0 && -2 + Z >= 0 && -2 + B + Z >= 0 && -4 + A + Z >= 0 && B >= 0 && -2 + A + B >= 0 && -2 + A >= 0 && O1 >= 2 && M1 >= 2 && G >= 0 && M = 0] 6. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f16(A,1 + B,M1,O1,P1,F,-1 + G,H,I,J,K,M,M,Q1,1 + B,-1 + G,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1[A + -1*G >= 0 (?,1) ,J1,K1,L1) && -2 + B + G >= 0 && 2 + -1*L1 >= 0 && C + -1*L1 >= 0 && -1*L1 + Z >= 0 && 2 + B + -1*L1 >= 0 && A + -1*L1 >= 0 && -2 + L1 >= 0 && -4 + C + L1 >= 0 && -4 + L1 + Z >= 0 && -2 + B + L1 >= 0 && -4 + A + L1 >= 0 && -2 + C >= 0 && -4 + C + Z >= 0 && -2 + B + C >= 0 && -4 + A + C >= 0 && -2 + Z >= 0 && -2 + B + Z >= 0 && -4 + A + Z >= 0 && B >= 0 && -2 + A + B >= 0 && -2 + A >= 0 && G >= 0 && M1 >= 2] 7. 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) -> f10(A,B,M1,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,T1,Z,A1,N1,O1,P1,Q1,U1,S1,H1,I1,J1,K1,L1) [A + -1*G >= 0 (?,1) && G >= 0 && -2 + G + L1 >= 0 && 2 + G + -1*L1 >= 0 && D1 + G >= 0 && -1*D1 + G >= 0 && -2 + C + G >= 0 && B1 + G >= 0 && -1*B1 + G >= 0 && -2 + G + Z >= 0 && G + M >= 0 && G + -1*M >= 0 && -2 + A + G >= 0 && 2 + -1*L1 >= 0 && 2 + D1 + -1*L1 >= 0 && 2 + -1*D1 + -1*L1 >= 0 && C + -1*L1 >= 0 && 2 + B1 + -1*L1 >= 0 && 2 + -1*B1 + -1*L1 >= 0 && -1*L1 + Z >= 0 && 2 + -1*L1 + M >= 0 && 2 + -1*L1 + -1*M >= 0 && A + -1*L1 >= 0 && -2 + L1 >= 0 && -2 + D1 + L1 >= 0 && -2 + -1*D1 + L1 >= 0 && -4 + C + L1 >= 0 && -2 + B1 + L1 >= 0 && -2 + -1*B1 + L1 >= 0 && -4 + L1 + Z >= 0 && -2 + L1 + M >= 0 && -2 + L1 + -1*M >= 0 && -4 + A + L1 >= 0 && A1 + -1*H1 >= 0 && -1 + B + -1*H1 >= 0 && F1 + -1*G1 >= 0 && -1*F1 + G1 >= 0 && -1*D1 >= 0 && -2 + C + -1*D1 >= 0 && B1 + -1*D1 >= 0 && -1*B1 + -1*D1 >= 0 && -2 + -1*D1 + Z >= 0 && -1*D1 + M >= 0 && -1*D1 + -1*M >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + C + D1 >= 0 && B1 + D1 >= 0 && -1*B1 + D1 >= 0 && -2 + D1 + Z >= 0 && D1 + M >= 0 && D1 + -1*M >= 0 && -2 + A + D1 >= 0 && -2 + C >= 0 && -2 + B1 + C >= 0 && -2 + -1*B1 + C >= 0 && -4 + C + Z >= 0 && -2 + C + M >= 0 && -2 + C + -1*M >= 0 && -4 + A + C >= 0 && -1*B1 >= 0 && -2 + -1*B1 + Z >= 0 && -1*B1 + M >= 0 && -1*B1 + -1*M >= 0 && -2 + A + -1*B1 >= 0 && B1 >= 0 && -2 + B1 + Z >= 0 && B1 + M >= 0 && B1 + -1*M >= 0 && -2 + A + B1 >= 0 && -1 + -1*A1 + B >= 0 && 1 + A1 + -1*B >= 0 && -2 + Z >= 0 && -2 + M + Z >= 0 && -2 + -1*M + Z >= 0 && -4 + A + Z >= 0 && -1*M >= 0 && -2 + A + -1*M >= 0 && M >= 0 && -2 + A + M >= 0 && -2 + A >= 0 && M1 >= 2 && H1 >= 0 && B1 = G1] 8. 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,M1,O1,P1,F,G,H,I,J,K,L,0,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,0,O1,0,O1,G1,G1,-1 + H1,-1 + H1,J1,K1,L1) [A + -1*G >= 0 (?,1) && G >= 0 && -2 + G + L1 >= 0 && 2 + G + -1*L1 >= 0 && D1 + G >= 0 && -1*D1 + G >= 0 && -2 + C + G >= 0 && B1 + G >= 0 && -1*B1 + G >= 0 && -2 + G + Z >= 0 && G + M >= 0 && G + -1*M >= 0 && -2 + A + G >= 0 && 2 + -1*L1 >= 0 && 2 + D1 + -1*L1 >= 0 && 2 + -1*D1 + -1*L1 >= 0 && C + -1*L1 >= 0 && 2 + B1 + -1*L1 >= 0 && 2 + -1*B1 + -1*L1 >= 0 && -1*L1 + Z >= 0 && 2 + -1*L1 + M >= 0 && 2 + -1*L1 + -1*M >= 0 && A + -1*L1 >= 0 && -2 + L1 >= 0 && -2 + D1 + L1 >= 0 && -2 + -1*D1 + L1 >= 0 && -4 + C + L1 >= 0 && -2 + B1 + L1 >= 0 && -2 + -1*B1 + L1 >= 0 && -4 + L1 + Z >= 0 && -2 + L1 + M >= 0 && -2 + L1 + -1*M >= 0 && -4 + A + L1 >= 0 && A1 + -1*H1 >= 0 && -1 + B + -1*H1 >= 0 && F1 + -1*G1 >= 0 && -1*F1 + G1 >= 0 && -1*D1 >= 0 && -2 + C + -1*D1 >= 0 && B1 + -1*D1 >= 0 && -1*B1 + -1*D1 >= 0 && -2 + -1*D1 + Z >= 0 && -1*D1 + M >= 0 && -1*D1 + -1*M >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + C + D1 >= 0 && B1 + D1 >= 0 && -1*B1 + D1 >= 0 && -2 + D1 + Z >= 0 && D1 + M >= 0 && D1 + -1*M >= 0 && -2 + A + D1 >= 0 && -2 + C >= 0 && -2 + B1 + C >= 0 && -2 + -1*B1 + C >= 0 && -4 + C + Z >= 0 && -2 + C + M >= 0 && -2 + C + -1*M >= 0 && -4 + A + C >= 0 && -1*B1 >= 0 && -2 + -1*B1 + Z >= 0 && -1*B1 + M >= 0 && -1*B1 + -1*M >= 0 && -2 + A + -1*B1 >= 0 && B1 >= 0 && -2 + B1 + Z >= 0 && B1 + M >= 0 && B1 + -1*M >= 0 && -2 + A + B1 >= 0 && -1 + -1*A1 + B >= 0 && 1 + A1 + -1*B >= 0 && -2 + Z >= 0 && -2 + M + Z >= 0 && -2 + -1*M + Z >= 0 && -4 + A + Z >= 0 && -1*M >= 0 && -2 + A + -1*M >= 0 && M >= 0 && -2 + A + M >= 0 && -2 + A >= 0 && M1 >= 2 && H1 >= 0 && B1 = 0] Signature: {(f1,38);(f10,38);(f16,38);(f8,38);(f9,38)} Flow Graph: [0->{},1->{},2->{3,4},3->{5,6},4->{3,4},5->{7,8},6->{5,6},7->{},8->{7,8}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: PolyRank MAYBE + Considered Problem: Rules: 0. f9(A,B,C,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) -> f10(T1,B,1,S1,E,F,G,H,I,J,K,L,0,N,O,P,R1,Y1,B2,A2,U,V,Z1,C2,D2,Z,A1,Q1,M1,O1,P1,E2,N1,H1,I1,U1,K1,L1) [S = 0] (1,1) 1. f9(A,B,C,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) -> f10(T1,B,M1,0,E,F,G,H,I,J,K,L,0,N,O,P,R1,Y1,B2,A2,U,V,Z1,C2,D2,Z,A1,N1,O1,P1,Q1,E2,S1,H1,I1,U1,K1,L1) [0 >= V1 && 0 >= W1 && 0 >= M1 && 0 >= X1] (1,1) 2. f9(A,B,C,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,B,M1,D,E,F,G,H,I,J,K,L,M,N,O,P,M1,P1,Q1,P1,U,V,P1,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,O1,N1,2) [M1 >= 2] (1,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) -> f16(G,0,M1,R,E,F,G,H,I,J,K,L,R,N,O,P,O1,P1,S1,N1,U,V,Q1,T1,U1,R1,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) [2 + -1*L1 >= 0 (1,1) && -1*L1 + Q >= 0 && A + -1*L1 >= 0 && -2 + L1 >= 0 && -4 + L1 + Q >= 0 && -4 + A + L1 >= 0 && -2 + Q >= 0 && -4 + A + Q >= 0 && -1*A + Q >= 0 && -2 + A >= 0 && A >= Q && A >= 0 && M1 >= 2 && R1 >= M1 && G >= M1 && B = 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) -> f1(1 + A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,S,M1,S,O1,A,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) [2 + -1*L1 >= 0 (?,1) && -1*L1 + Q >= 0 && A + -1*L1 >= 0 && -2 + L1 >= 0 && -4 + L1 + Q >= 0 && -4 + A + L1 >= 0 && -2 + Q >= 0 && -4 + A + Q >= 0 && -1*A + Q >= 0 && -2 + A >= 0 && Q >= 1 + A && A >= 0] 5. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,1 + H1,M1,D,E,F,G,H,I,J,K,L,0,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,H1,0,D,0,D,D,D,H1,I1,J1,K1,L1) [A + -1*G >= 0 (1,1) && -2 + B + G >= 0 && 2 + -1*L1 >= 0 && C + -1*L1 >= 0 && -1*L1 + Z >= 0 && 2 + B + -1*L1 >= 0 && A + -1*L1 >= 0 && -2 + L1 >= 0 && -4 + C + L1 >= 0 && -4 + L1 + Z >= 0 && -2 + B + L1 >= 0 && -4 + A + L1 >= 0 && -2 + C >= 0 && -4 + C + Z >= 0 && -2 + B + C >= 0 && -4 + A + C >= 0 && -2 + Z >= 0 && -2 + B + Z >= 0 && -4 + A + Z >= 0 && B >= 0 && -2 + A + B >= 0 && -2 + A >= 0 && O1 >= 2 && M1 >= 2 && G >= 0 && M = 0] 6. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f16(A,1 + B,M1,O1,P1,F,-1 + G,H,I,J,K,M,M,Q1,1 + B,-1 + G,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1[A + -1*G >= 0 (?,1) ,J1,K1,L1) && -2 + B + G >= 0 && 2 + -1*L1 >= 0 && C + -1*L1 >= 0 && -1*L1 + Z >= 0 && 2 + B + -1*L1 >= 0 && A + -1*L1 >= 0 && -2 + L1 >= 0 && -4 + C + L1 >= 0 && -4 + L1 + Z >= 0 && -2 + B + L1 >= 0 && -4 + A + L1 >= 0 && -2 + C >= 0 && -4 + C + Z >= 0 && -2 + B + C >= 0 && -4 + A + C >= 0 && -2 + Z >= 0 && -2 + B + Z >= 0 && -4 + A + Z >= 0 && B >= 0 && -2 + A + B >= 0 && -2 + A >= 0 && G >= 0 && M1 >= 2] 7. 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) -> f10(A,B,M1,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,T1,Z,A1,N1,O1,P1,Q1,U1,S1,H1,I1,J1,K1,L1) [A + -1*G >= 0 (1,1) && G >= 0 && -2 + G + L1 >= 0 && 2 + G + -1*L1 >= 0 && D1 + G >= 0 && -1*D1 + G >= 0 && -2 + C + G >= 0 && B1 + G >= 0 && -1*B1 + G >= 0 && -2 + G + Z >= 0 && G + M >= 0 && G + -1*M >= 0 && -2 + A + G >= 0 && 2 + -1*L1 >= 0 && 2 + D1 + -1*L1 >= 0 && 2 + -1*D1 + -1*L1 >= 0 && C + -1*L1 >= 0 && 2 + B1 + -1*L1 >= 0 && 2 + -1*B1 + -1*L1 >= 0 && -1*L1 + Z >= 0 && 2 + -1*L1 + M >= 0 && 2 + -1*L1 + -1*M >= 0 && A + -1*L1 >= 0 && -2 + L1 >= 0 && -2 + D1 + L1 >= 0 && -2 + -1*D1 + L1 >= 0 && -4 + C + L1 >= 0 && -2 + B1 + L1 >= 0 && -2 + -1*B1 + L1 >= 0 && -4 + L1 + Z >= 0 && -2 + L1 + M >= 0 && -2 + L1 + -1*M >= 0 && -4 + A + L1 >= 0 && A1 + -1*H1 >= 0 && -1 + B + -1*H1 >= 0 && F1 + -1*G1 >= 0 && -1*F1 + G1 >= 0 && -1*D1 >= 0 && -2 + C + -1*D1 >= 0 && B1 + -1*D1 >= 0 && -1*B1 + -1*D1 >= 0 && -2 + -1*D1 + Z >= 0 && -1*D1 + M >= 0 && -1*D1 + -1*M >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + C + D1 >= 0 && B1 + D1 >= 0 && -1*B1 + D1 >= 0 && -2 + D1 + Z >= 0 && D1 + M >= 0 && D1 + -1*M >= 0 && -2 + A + D1 >= 0 && -2 + C >= 0 && -2 + B1 + C >= 0 && -2 + -1*B1 + C >= 0 && -4 + C + Z >= 0 && -2 + C + M >= 0 && -2 + C + -1*M >= 0 && -4 + A + C >= 0 && -1*B1 >= 0 && -2 + -1*B1 + Z >= 0 && -1*B1 + M >= 0 && -1*B1 + -1*M >= 0 && -2 + A + -1*B1 >= 0 && B1 >= 0 && -2 + B1 + Z >= 0 && B1 + M >= 0 && B1 + -1*M >= 0 && -2 + A + B1 >= 0 && -1 + -1*A1 + B >= 0 && 1 + A1 + -1*B >= 0 && -2 + Z >= 0 && -2 + M + Z >= 0 && -2 + -1*M + Z >= 0 && -4 + A + Z >= 0 && -1*M >= 0 && -2 + A + -1*M >= 0 && M >= 0 && -2 + A + M >= 0 && -2 + A >= 0 && M1 >= 2 && H1 >= 0 && B1 = G1] 8. 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,M1,O1,P1,F,G,H,I,J,K,L,0,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,0,O1,0,O1,G1,G1,-1 + H1,-1 + H1,J1,K1,L1) [A + -1*G >= 0 (?,1) && G >= 0 && -2 + G + L1 >= 0 && 2 + G + -1*L1 >= 0 && D1 + G >= 0 && -1*D1 + G >= 0 && -2 + C + G >= 0 && B1 + G >= 0 && -1*B1 + G >= 0 && -2 + G + Z >= 0 && G + M >= 0 && G + -1*M >= 0 && -2 + A + G >= 0 && 2 + -1*L1 >= 0 && 2 + D1 + -1*L1 >= 0 && 2 + -1*D1 + -1*L1 >= 0 && C + -1*L1 >= 0 && 2 + B1 + -1*L1 >= 0 && 2 + -1*B1 + -1*L1 >= 0 && -1*L1 + Z >= 0 && 2 + -1*L1 + M >= 0 && 2 + -1*L1 + -1*M >= 0 && A + -1*L1 >= 0 && -2 + L1 >= 0 && -2 + D1 + L1 >= 0 && -2 + -1*D1 + L1 >= 0 && -4 + C + L1 >= 0 && -2 + B1 + L1 >= 0 && -2 + -1*B1 + L1 >= 0 && -4 + L1 + Z >= 0 && -2 + L1 + M >= 0 && -2 + L1 + -1*M >= 0 && -4 + A + L1 >= 0 && A1 + -1*H1 >= 0 && -1 + B + -1*H1 >= 0 && F1 + -1*G1 >= 0 && -1*F1 + G1 >= 0 && -1*D1 >= 0 && -2 + C + -1*D1 >= 0 && B1 + -1*D1 >= 0 && -1*B1 + -1*D1 >= 0 && -2 + -1*D1 + Z >= 0 && -1*D1 + M >= 0 && -1*D1 + -1*M >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + C + D1 >= 0 && B1 + D1 >= 0 && -1*B1 + D1 >= 0 && -2 + D1 + Z >= 0 && D1 + M >= 0 && D1 + -1*M >= 0 && -2 + A + D1 >= 0 && -2 + C >= 0 && -2 + B1 + C >= 0 && -2 + -1*B1 + C >= 0 && -4 + C + Z >= 0 && -2 + C + M >= 0 && -2 + C + -1*M >= 0 && -4 + A + C >= 0 && -1*B1 >= 0 && -2 + -1*B1 + Z >= 0 && -1*B1 + M >= 0 && -1*B1 + -1*M >= 0 && -2 + A + -1*B1 >= 0 && B1 >= 0 && -2 + B1 + Z >= 0 && B1 + M >= 0 && B1 + -1*M >= 0 && -2 + A + B1 >= 0 && -1 + -1*A1 + B >= 0 && 1 + A1 + -1*B >= 0 && -2 + Z >= 0 && -2 + M + Z >= 0 && -2 + -1*M + Z >= 0 && -4 + A + Z >= 0 && -1*M >= 0 && -2 + A + -1*M >= 0 && M >= 0 && -2 + A + M >= 0 && -2 + A >= 0 && M1 >= 2 && H1 >= 0 && B1 = 0] Signature: {(f1,38);(f10,38);(f16,38);(f8,38);(f9,38)} Flow Graph: [0->{},1->{},2->{3,4},3->{5,6},4->{3,4},5->{7,8},6->{5,6},7->{},8->{7,8}] + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(f1) = 1 + x34 p(f10) = 1 + x34 p(f16) = 1 + x34 p(f8) = 1 + x34 p(f9) = 1 + x34 Following rules are strictly oriented: [A + -1*G >= 0 ==> && G >= 0 && -2 + G + L1 >= 0 && 2 + G + -1*L1 >= 0 && D1 + G >= 0 && -1*D1 + G >= 0 && -2 + C + G >= 0 && B1 + G >= 0 && -1*B1 + G >= 0 && -2 + G + Z >= 0 && G + M >= 0 && G + -1*M >= 0 && -2 + A + G >= 0 && 2 + -1*L1 >= 0 && 2 + D1 + -1*L1 >= 0 && 2 + -1*D1 + -1*L1 >= 0 && C + -1*L1 >= 0 && 2 + B1 + -1*L1 >= 0 && 2 + -1*B1 + -1*L1 >= 0 && -1*L1 + Z >= 0 && 2 + -1*L1 + M >= 0 && 2 + -1*L1 + -1*M >= 0 && A + -1*L1 >= 0 && -2 + L1 >= 0 && -2 + D1 + L1 >= 0 && -2 + -1*D1 + L1 >= 0 && -4 + C + L1 >= 0 && -2 + B1 + L1 >= 0 && -2 + -1*B1 + L1 >= 0 && -4 + L1 + Z >= 0 && -2 + L1 + M >= 0 && -2 + L1 + -1*M >= 0 && -4 + A + L1 >= 0 && A1 + -1*H1 >= 0 && -1 + B + -1*H1 >= 0 && F1 + -1*G1 >= 0 && -1*F1 + G1 >= 0 && -1*D1 >= 0 && -2 + C + -1*D1 >= 0 && B1 + -1*D1 >= 0 && -1*B1 + -1*D1 >= 0 && -2 + -1*D1 + Z >= 0 && -1*D1 + M >= 0 && -1*D1 + -1*M >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + C + D1 >= 0 && B1 + D1 >= 0 && -1*B1 + D1 >= 0 && -2 + D1 + Z >= 0 && D1 + M >= 0 && D1 + -1*M >= 0 && -2 + A + D1 >= 0 && -2 + C >= 0 && -2 + B1 + C >= 0 && -2 + -1*B1 + C >= 0 && -4 + C + Z >= 0 && -2 + C + M >= 0 && -2 + C + -1*M >= 0 && -4 + A + C >= 0 && -1*B1 >= 0 && -2 + -1*B1 + Z >= 0 && -1*B1 + M >= 0 && -1*B1 + -1*M >= 0 && -2 + A + -1*B1 >= 0 && B1 >= 0 && -2 + B1 + Z >= 0 && B1 + M >= 0 && B1 + -1*M >= 0 && -2 + A + B1 >= 0 && -1 + -1*A1 + B >= 0 && 1 + A1 + -1*B >= 0 && -2 + Z >= 0 && -2 + M + Z >= 0 && -2 + -1*M + Z >= 0 && -4 + A + Z >= 0 && -1*M >= 0 && -2 + A + -1*M >= 0 && M >= 0 && -2 + A + M >= 0 && -2 + A >= 0 && M1 >= 2 && H1 >= 0 && B1 = 0] 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) = 1 + H1 > H1 = f8(A,B,M1,O1,P1,F,G,H,I,J,K,L,0,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,0,O1,0,O1,G1,G1,-1 + H1,-1 + H1,J1,K1,L1) Following rules are weakly oriented: [S = 0] ==> f9(A,B,C,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) = 1 + H1 >= 1 + H1 = f10(T1,B,1,S1,E,F,G,H,I,J,K,L,0,N,O,P,R1,Y1,B2,A2,U,V,Z1,C2,D2,Z,A1,Q1,M1,O1,P1,E2,N1,H1,I1,U1,K1,L1) [0 >= V1 && 0 >= W1 && 0 >= M1 && 0 >= X1] ==> f9(A,B,C,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) = 1 + H1 >= 1 + H1 = f10(T1,B,M1,0,E,F,G,H,I,J,K,L,0,N,O,P,R1,Y1,B2,A2,U,V,Z1,C2,D2,Z,A1,N1,O1,P1,Q1,E2,S1,H1,I1,U1,K1,L1) [M1 >= 2] ==> f9(A,B,C,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) = 1 + H1 >= 1 + H1 = f1(2,B,M1,D,E,F,G,H,I,J,K,L,M,N,O,P,M1,P1,Q1,P1,U,V,P1,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,O1,N1,2) [2 + -1*L1 >= 0 ==> && -1*L1 + Q >= 0 && A + -1*L1 >= 0 && -2 + L1 >= 0 && -4 + L1 + Q >= 0 && -4 + A + L1 >= 0 && -2 + Q >= 0 && -4 + A + Q >= 0 && -1*A + Q >= 0 && -2 + A >= 0 && A >= Q && A >= 0 && M1 >= 2 && R1 >= M1 && G >= M1 && B = 0] 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) = 1 + H1 >= 1 + H1 = f16(G,0,M1,R,E,F,G,H,I,J,K,L,R,N,O,P,O1,P1,S1,N1,U,V,Q1,T1,U1,R1,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) [2 + -1*L1 >= 0 ==> && -1*L1 + Q >= 0 && A + -1*L1 >= 0 && -2 + L1 >= 0 && -4 + L1 + Q >= 0 && -4 + A + L1 >= 0 && -2 + Q >= 0 && -4 + A + Q >= 0 && -1*A + Q >= 0 && -2 + A >= 0 && Q >= 1 + A && A >= 0] 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) = 1 + H1 >= 1 + H1 = f1(1 + A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,S,M1,S,O1,A,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) [A + -1*G >= 0 ==> && -2 + B + G >= 0 && 2 + -1*L1 >= 0 && C + -1*L1 >= 0 && -1*L1 + Z >= 0 && 2 + B + -1*L1 >= 0 && A + -1*L1 >= 0 && -2 + L1 >= 0 && -4 + C + L1 >= 0 && -4 + L1 + Z >= 0 && -2 + B + L1 >= 0 && -4 + A + L1 >= 0 && -2 + C >= 0 && -4 + C + Z >= 0 && -2 + B + C >= 0 && -4 + A + C >= 0 && -2 + Z >= 0 && -2 + B + Z >= 0 && -4 + A + Z >= 0 && B >= 0 && -2 + A + B >= 0 && -2 + A >= 0 && O1 >= 2 && M1 >= 2 && G >= 0 && M = 0] f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) = 1 + H1 >= 1 + H1 = f8(A,1 + H1,M1,D,E,F,G,H,I,J,K,L,0,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,H1,0,D,0,D,D,D,H1,I1,J1,K1,L1) [A + -1*G >= 0 ==> && -2 + B + G >= 0 && 2 + -1*L1 >= 0 && C + -1*L1 >= 0 && -1*L1 + Z >= 0 && 2 + B + -1*L1 >= 0 && A + -1*L1 >= 0 && -2 + L1 >= 0 && -4 + C + L1 >= 0 && -4 + L1 + Z >= 0 && -2 + B + L1 >= 0 && -4 + A + L1 >= 0 && -2 + C >= 0 && -4 + C + Z >= 0 && -2 + B + C >= 0 && -4 + A + C >= 0 && -2 + Z >= 0 && -2 + B + Z >= 0 && -4 + A + Z >= 0 && B >= 0 && -2 + A + B >= 0 && -2 + A >= 0 && G >= 0 && M1 >= 2] f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) = 1 + H1 >= 1 + H1 = f16(A,1 + B,M1,O1,P1,F,-1 + G,H,I,J,K,M,M,Q1,1 + B,-1 + G,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1 ,K1,L1) [A + -1*G >= 0 ==> && G >= 0 && -2 + G + L1 >= 0 && 2 + G + -1*L1 >= 0 && D1 + G >= 0 && -1*D1 + G >= 0 && -2 + C + G >= 0 && B1 + G >= 0 && -1*B1 + G >= 0 && -2 + G + Z >= 0 && G + M >= 0 && G + -1*M >= 0 && -2 + A + G >= 0 && 2 + -1*L1 >= 0 && 2 + D1 + -1*L1 >= 0 && 2 + -1*D1 + -1*L1 >= 0 && C + -1*L1 >= 0 && 2 + B1 + -1*L1 >= 0 && 2 + -1*B1 + -1*L1 >= 0 && -1*L1 + Z >= 0 && 2 + -1*L1 + M >= 0 && 2 + -1*L1 + -1*M >= 0 && A + -1*L1 >= 0 && -2 + L1 >= 0 && -2 + D1 + L1 >= 0 && -2 + -1*D1 + L1 >= 0 && -4 + C + L1 >= 0 && -2 + B1 + L1 >= 0 && -2 + -1*B1 + L1 >= 0 && -4 + L1 + Z >= 0 && -2 + L1 + M >= 0 && -2 + L1 + -1*M >= 0 && -4 + A + L1 >= 0 && A1 + -1*H1 >= 0 && -1 + B + -1*H1 >= 0 && F1 + -1*G1 >= 0 && -1*F1 + G1 >= 0 && -1*D1 >= 0 && -2 + C + -1*D1 >= 0 && B1 + -1*D1 >= 0 && -1*B1 + -1*D1 >= 0 && -2 + -1*D1 + Z >= 0 && -1*D1 + M >= 0 && -1*D1 + -1*M >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + C + D1 >= 0 && B1 + D1 >= 0 && -1*B1 + D1 >= 0 && -2 + D1 + Z >= 0 && D1 + M >= 0 && D1 + -1*M >= 0 && -2 + A + D1 >= 0 && -2 + C >= 0 && -2 + B1 + C >= 0 && -2 + -1*B1 + C >= 0 && -4 + C + Z >= 0 && -2 + C + M >= 0 && -2 + C + -1*M >= 0 && -4 + A + C >= 0 && -1*B1 >= 0 && -2 + -1*B1 + Z >= 0 && -1*B1 + M >= 0 && -1*B1 + -1*M >= 0 && -2 + A + -1*B1 >= 0 && B1 >= 0 && -2 + B1 + Z >= 0 && B1 + M >= 0 && B1 + -1*M >= 0 && -2 + A + B1 >= 0 && -1 + -1*A1 + B >= 0 && 1 + A1 + -1*B >= 0 && -2 + Z >= 0 && -2 + M + Z >= 0 && -2 + -1*M + Z >= 0 && -4 + A + Z >= 0 && -1*M >= 0 && -2 + A + -1*M >= 0 && M >= 0 && -2 + A + M >= 0 && -2 + A >= 0 && M1 >= 2 && H1 >= 0 && B1 = G1] 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) = 1 + H1 >= 1 + H1 = f10(A,B,M1,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,T1,Z,A1,N1,O1,P1,Q1,U1,S1,H1,I1,J1,K1,L1) * Step 3: PolyRank MAYBE + Considered Problem: Rules: 0. f9(A,B,C,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) -> f10(T1,B,1,S1,E,F,G,H,I,J,K,L,0,N,O,P,R1,Y1,B2,A2,U,V,Z1,C2,D2,Z,A1,Q1,M1,O1,P1,E2,N1,H1,I1,U1,K1,L1) [S = 0] (1,1) 1. f9(A,B,C,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) -> f10(T1,B,M1,0,E,F,G,H,I,J,K,L,0,N,O,P,R1,Y1,B2,A2,U,V,Z1,C2,D2,Z,A1,N1,O1,P1,Q1,E2,S1,H1,I1,U1,K1,L1) [0 >= V1 && 0 >= W1 && 0 >= M1 && 0 >= X1] (1,1) 2. f9(A,B,C,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,B,M1,D,E,F,G,H,I,J,K,L,M,N,O,P,M1,P1,Q1,P1,U,V,P1,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,O1,N1,2) [M1 >= 2] (1,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) -> f16(G,0,M1,R,E,F,G,H,I,J,K,L,R,N,O,P,O1,P1,S1,N1,U,V,Q1,T1,U1,R1,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) [2 + -1*L1 >= 0 (1,1) && -1*L1 + Q >= 0 && A + -1*L1 >= 0 && -2 + L1 >= 0 && -4 + L1 + Q >= 0 && -4 + A + L1 >= 0 && -2 + Q >= 0 && -4 + A + Q >= 0 && -1*A + Q >= 0 && -2 + A >= 0 && A >= Q && A >= 0 && M1 >= 2 && R1 >= M1 && G >= M1 && B = 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) -> f1(1 + A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,S,M1,S,O1,A,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) [2 + -1*L1 >= 0 (?,1) && -1*L1 + Q >= 0 && A + -1*L1 >= 0 && -2 + L1 >= 0 && -4 + L1 + Q >= 0 && -4 + A + L1 >= 0 && -2 + Q >= 0 && -4 + A + Q >= 0 && -1*A + Q >= 0 && -2 + A >= 0 && Q >= 1 + A && A >= 0] 5. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,1 + H1,M1,D,E,F,G,H,I,J,K,L,0,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,H1,0,D,0,D,D,D,H1,I1,J1,K1,L1) [A + -1*G >= 0 (1,1) && -2 + B + G >= 0 && 2 + -1*L1 >= 0 && C + -1*L1 >= 0 && -1*L1 + Z >= 0 && 2 + B + -1*L1 >= 0 && A + -1*L1 >= 0 && -2 + L1 >= 0 && -4 + C + L1 >= 0 && -4 + L1 + Z >= 0 && -2 + B + L1 >= 0 && -4 + A + L1 >= 0 && -2 + C >= 0 && -4 + C + Z >= 0 && -2 + B + C >= 0 && -4 + A + C >= 0 && -2 + Z >= 0 && -2 + B + Z >= 0 && -4 + A + Z >= 0 && B >= 0 && -2 + A + B >= 0 && -2 + A >= 0 && O1 >= 2 && M1 >= 2 && G >= 0 && M = 0] 6. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f16(A,1 + B,M1,O1,P1,F,-1 + G,H,I,J,K,M,M,Q1,1 + B,-1 + G,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1[A + -1*G >= 0 (?,1) ,J1,K1,L1) && -2 + B + G >= 0 && 2 + -1*L1 >= 0 && C + -1*L1 >= 0 && -1*L1 + Z >= 0 && 2 + B + -1*L1 >= 0 && A + -1*L1 >= 0 && -2 + L1 >= 0 && -4 + C + L1 >= 0 && -4 + L1 + Z >= 0 && -2 + B + L1 >= 0 && -4 + A + L1 >= 0 && -2 + C >= 0 && -4 + C + Z >= 0 && -2 + B + C >= 0 && -4 + A + C >= 0 && -2 + Z >= 0 && -2 + B + Z >= 0 && -4 + A + Z >= 0 && B >= 0 && -2 + A + B >= 0 && -2 + A >= 0 && G >= 0 && M1 >= 2] 7. 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) -> f10(A,B,M1,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,T1,Z,A1,N1,O1,P1,Q1,U1,S1,H1,I1,J1,K1,L1) [A + -1*G >= 0 (1,1) && G >= 0 && -2 + G + L1 >= 0 && 2 + G + -1*L1 >= 0 && D1 + G >= 0 && -1*D1 + G >= 0 && -2 + C + G >= 0 && B1 + G >= 0 && -1*B1 + G >= 0 && -2 + G + Z >= 0 && G + M >= 0 && G + -1*M >= 0 && -2 + A + G >= 0 && 2 + -1*L1 >= 0 && 2 + D1 + -1*L1 >= 0 && 2 + -1*D1 + -1*L1 >= 0 && C + -1*L1 >= 0 && 2 + B1 + -1*L1 >= 0 && 2 + -1*B1 + -1*L1 >= 0 && -1*L1 + Z >= 0 && 2 + -1*L1 + M >= 0 && 2 + -1*L1 + -1*M >= 0 && A + -1*L1 >= 0 && -2 + L1 >= 0 && -2 + D1 + L1 >= 0 && -2 + -1*D1 + L1 >= 0 && -4 + C + L1 >= 0 && -2 + B1 + L1 >= 0 && -2 + -1*B1 + L1 >= 0 && -4 + L1 + Z >= 0 && -2 + L1 + M >= 0 && -2 + L1 + -1*M >= 0 && -4 + A + L1 >= 0 && A1 + -1*H1 >= 0 && -1 + B + -1*H1 >= 0 && F1 + -1*G1 >= 0 && -1*F1 + G1 >= 0 && -1*D1 >= 0 && -2 + C + -1*D1 >= 0 && B1 + -1*D1 >= 0 && -1*B1 + -1*D1 >= 0 && -2 + -1*D1 + Z >= 0 && -1*D1 + M >= 0 && -1*D1 + -1*M >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + C + D1 >= 0 && B1 + D1 >= 0 && -1*B1 + D1 >= 0 && -2 + D1 + Z >= 0 && D1 + M >= 0 && D1 + -1*M >= 0 && -2 + A + D1 >= 0 && -2 + C >= 0 && -2 + B1 + C >= 0 && -2 + -1*B1 + C >= 0 && -4 + C + Z >= 0 && -2 + C + M >= 0 && -2 + C + -1*M >= 0 && -4 + A + C >= 0 && -1*B1 >= 0 && -2 + -1*B1 + Z >= 0 && -1*B1 + M >= 0 && -1*B1 + -1*M >= 0 && -2 + A + -1*B1 >= 0 && B1 >= 0 && -2 + B1 + Z >= 0 && B1 + M >= 0 && B1 + -1*M >= 0 && -2 + A + B1 >= 0 && -1 + -1*A1 + B >= 0 && 1 + A1 + -1*B >= 0 && -2 + Z >= 0 && -2 + M + Z >= 0 && -2 + -1*M + Z >= 0 && -4 + A + Z >= 0 && -1*M >= 0 && -2 + A + -1*M >= 0 && M >= 0 && -2 + A + M >= 0 && -2 + A >= 0 && M1 >= 2 && H1 >= 0 && B1 = G1] 8. 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,M1,O1,P1,F,G,H,I,J,K,L,0,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,0,O1,0,O1,G1,G1,-1 + H1,-1 + H1,J1,K1,L1) [A + -1*G >= 0 (1 + H1,1) && G >= 0 && -2 + G + L1 >= 0 && 2 + G + -1*L1 >= 0 && D1 + G >= 0 && -1*D1 + G >= 0 && -2 + C + G >= 0 && B1 + G >= 0 && -1*B1 + G >= 0 && -2 + G + Z >= 0 && G + M >= 0 && G + -1*M >= 0 && -2 + A + G >= 0 && 2 + -1*L1 >= 0 && 2 + D1 + -1*L1 >= 0 && 2 + -1*D1 + -1*L1 >= 0 && C + -1*L1 >= 0 && 2 + B1 + -1*L1 >= 0 && 2 + -1*B1 + -1*L1 >= 0 && -1*L1 + Z >= 0 && 2 + -1*L1 + M >= 0 && 2 + -1*L1 + -1*M >= 0 && A + -1*L1 >= 0 && -2 + L1 >= 0 && -2 + D1 + L1 >= 0 && -2 + -1*D1 + L1 >= 0 && -4 + C + L1 >= 0 && -2 + B1 + L1 >= 0 && -2 + -1*B1 + L1 >= 0 && -4 + L1 + Z >= 0 && -2 + L1 + M >= 0 && -2 + L1 + -1*M >= 0 && -4 + A + L1 >= 0 && A1 + -1*H1 >= 0 && -1 + B + -1*H1 >= 0 && F1 + -1*G1 >= 0 && -1*F1 + G1 >= 0 && -1*D1 >= 0 && -2 + C + -1*D1 >= 0 && B1 + -1*D1 >= 0 && -1*B1 + -1*D1 >= 0 && -2 + -1*D1 + Z >= 0 && -1*D1 + M >= 0 && -1*D1 + -1*M >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + C + D1 >= 0 && B1 + D1 >= 0 && -1*B1 + D1 >= 0 && -2 + D1 + Z >= 0 && D1 + M >= 0 && D1 + -1*M >= 0 && -2 + A + D1 >= 0 && -2 + C >= 0 && -2 + B1 + C >= 0 && -2 + -1*B1 + C >= 0 && -4 + C + Z >= 0 && -2 + C + M >= 0 && -2 + C + -1*M >= 0 && -4 + A + C >= 0 && -1*B1 >= 0 && -2 + -1*B1 + Z >= 0 && -1*B1 + M >= 0 && -1*B1 + -1*M >= 0 && -2 + A + -1*B1 >= 0 && B1 >= 0 && -2 + B1 + Z >= 0 && B1 + M >= 0 && B1 + -1*M >= 0 && -2 + A + B1 >= 0 && -1 + -1*A1 + B >= 0 && 1 + A1 + -1*B >= 0 && -2 + Z >= 0 && -2 + M + Z >= 0 && -2 + -1*M + Z >= 0 && -4 + A + Z >= 0 && -1*M >= 0 && -2 + A + -1*M >= 0 && M >= 0 && -2 + A + M >= 0 && -2 + A >= 0 && M1 >= 2 && H1 >= 0 && B1 = 0] Signature: {(f1,38);(f10,38);(f16,38);(f8,38);(f9,38)} Flow Graph: [0->{},1->{},2->{3,4},3->{5,6},4->{3,4},5->{7,8},6->{5,6},7->{},8->{7,8}] + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(f1) = 1 + x7 p(f10) = x7 p(f16) = 1 + x7 p(f8) = x7 p(f9) = 1 + x7 Following rules are strictly oriented: [A + -1*G >= 0 ==> && -2 + B + G >= 0 && 2 + -1*L1 >= 0 && C + -1*L1 >= 0 && -1*L1 + Z >= 0 && 2 + B + -1*L1 >= 0 && A + -1*L1 >= 0 && -2 + L1 >= 0 && -4 + C + L1 >= 0 && -4 + L1 + Z >= 0 && -2 + B + L1 >= 0 && -4 + A + L1 >= 0 && -2 + C >= 0 && -4 + C + Z >= 0 && -2 + B + C >= 0 && -4 + A + C >= 0 && -2 + Z >= 0 && -2 + B + Z >= 0 && -4 + A + Z >= 0 && B >= 0 && -2 + A + B >= 0 && -2 + A >= 0 && O1 >= 2 && M1 >= 2 && G >= 0 && M = 0] f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) = 1 + G > G = f8(A,1 + H1,M1,D,E,F,G,H,I,J,K,L,0,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,H1,0,D,0,D,D,D,H1,I1,J1,K1,L1) [A + -1*G >= 0 ==> && -2 + B + G >= 0 && 2 + -1*L1 >= 0 && C + -1*L1 >= 0 && -1*L1 + Z >= 0 && 2 + B + -1*L1 >= 0 && A + -1*L1 >= 0 && -2 + L1 >= 0 && -4 + C + L1 >= 0 && -4 + L1 + Z >= 0 && -2 + B + L1 >= 0 && -4 + A + L1 >= 0 && -2 + C >= 0 && -4 + C + Z >= 0 && -2 + B + C >= 0 && -4 + A + C >= 0 && -2 + Z >= 0 && -2 + B + Z >= 0 && -4 + A + Z >= 0 && B >= 0 && -2 + A + B >= 0 && -2 + A >= 0 && G >= 0 && M1 >= 2] f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) = 1 + G > G = f16(A,1 + B,M1,O1,P1,F,-1 + G,H,I,J,K,M,M,Q1,1 + B,-1 + G,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1 ,K1,L1) Following rules are weakly oriented: [S = 0] ==> f9(A,B,C,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) = 1 + G >= G = f10(T1,B,1,S1,E,F,G,H,I,J,K,L,0,N,O,P,R1,Y1,B2,A2,U,V,Z1,C2,D2,Z,A1,Q1,M1,O1,P1,E2,N1,H1,I1,U1,K1,L1) [0 >= V1 && 0 >= W1 && 0 >= M1 && 0 >= X1] ==> f9(A,B,C,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) = 1 + G >= G = f10(T1,B,M1,0,E,F,G,H,I,J,K,L,0,N,O,P,R1,Y1,B2,A2,U,V,Z1,C2,D2,Z,A1,N1,O1,P1,Q1,E2,S1,H1,I1,U1,K1,L1) [M1 >= 2] ==> f9(A,B,C,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) = 1 + G >= 1 + G = f1(2,B,M1,D,E,F,G,H,I,J,K,L,M,N,O,P,M1,P1,Q1,P1,U,V,P1,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,O1,N1,2) [2 + -1*L1 >= 0 ==> && -1*L1 + Q >= 0 && A + -1*L1 >= 0 && -2 + L1 >= 0 && -4 + L1 + Q >= 0 && -4 + A + L1 >= 0 && -2 + Q >= 0 && -4 + A + Q >= 0 && -1*A + Q >= 0 && -2 + A >= 0 && A >= Q && A >= 0 && M1 >= 2 && R1 >= M1 && G >= M1 && B = 0] 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) = 1 + G >= 1 + G = f16(G,0,M1,R,E,F,G,H,I,J,K,L,R,N,O,P,O1,P1,S1,N1,U,V,Q1,T1,U1,R1,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) [2 + -1*L1 >= 0 ==> && -1*L1 + Q >= 0 && A + -1*L1 >= 0 && -2 + L1 >= 0 && -4 + L1 + Q >= 0 && -4 + A + L1 >= 0 && -2 + Q >= 0 && -4 + A + Q >= 0 && -1*A + Q >= 0 && -2 + A >= 0 && Q >= 1 + A && A >= 0] 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) = 1 + G >= 1 + G = f1(1 + A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,S,M1,S,O1,A,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) [A + -1*G >= 0 ==> && G >= 0 && -2 + G + L1 >= 0 && 2 + G + -1*L1 >= 0 && D1 + G >= 0 && -1*D1 + G >= 0 && -2 + C + G >= 0 && B1 + G >= 0 && -1*B1 + G >= 0 && -2 + G + Z >= 0 && G + M >= 0 && G + -1*M >= 0 && -2 + A + G >= 0 && 2 + -1*L1 >= 0 && 2 + D1 + -1*L1 >= 0 && 2 + -1*D1 + -1*L1 >= 0 && C + -1*L1 >= 0 && 2 + B1 + -1*L1 >= 0 && 2 + -1*B1 + -1*L1 >= 0 && -1*L1 + Z >= 0 && 2 + -1*L1 + M >= 0 && 2 + -1*L1 + -1*M >= 0 && A + -1*L1 >= 0 && -2 + L1 >= 0 && -2 + D1 + L1 >= 0 && -2 + -1*D1 + L1 >= 0 && -4 + C + L1 >= 0 && -2 + B1 + L1 >= 0 && -2 + -1*B1 + L1 >= 0 && -4 + L1 + Z >= 0 && -2 + L1 + M >= 0 && -2 + L1 + -1*M >= 0 && -4 + A + L1 >= 0 && A1 + -1*H1 >= 0 && -1 + B + -1*H1 >= 0 && F1 + -1*G1 >= 0 && -1*F1 + G1 >= 0 && -1*D1 >= 0 && -2 + C + -1*D1 >= 0 && B1 + -1*D1 >= 0 && -1*B1 + -1*D1 >= 0 && -2 + -1*D1 + Z >= 0 && -1*D1 + M >= 0 && -1*D1 + -1*M >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + C + D1 >= 0 && B1 + D1 >= 0 && -1*B1 + D1 >= 0 && -2 + D1 + Z >= 0 && D1 + M >= 0 && D1 + -1*M >= 0 && -2 + A + D1 >= 0 && -2 + C >= 0 && -2 + B1 + C >= 0 && -2 + -1*B1 + C >= 0 && -4 + C + Z >= 0 && -2 + C + M >= 0 && -2 + C + -1*M >= 0 && -4 + A + C >= 0 && -1*B1 >= 0 && -2 + -1*B1 + Z >= 0 && -1*B1 + M >= 0 && -1*B1 + -1*M >= 0 && -2 + A + -1*B1 >= 0 && B1 >= 0 && -2 + B1 + Z >= 0 && B1 + M >= 0 && B1 + -1*M >= 0 && -2 + A + B1 >= 0 && -1 + -1*A1 + B >= 0 && 1 + A1 + -1*B >= 0 && -2 + Z >= 0 && -2 + M + Z >= 0 && -2 + -1*M + Z >= 0 && -4 + A + Z >= 0 && -1*M >= 0 && -2 + A + -1*M >= 0 && M >= 0 && -2 + A + M >= 0 && -2 + A >= 0 && M1 >= 2 && H1 >= 0 && B1 = G1] 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) = G >= G = f10(A,B,M1,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,T1,Z,A1,N1,O1,P1,Q1,U1,S1,H1,I1,J1,K1,L1) [A + -1*G >= 0 ==> && G >= 0 && -2 + G + L1 >= 0 && 2 + G + -1*L1 >= 0 && D1 + G >= 0 && -1*D1 + G >= 0 && -2 + C + G >= 0 && B1 + G >= 0 && -1*B1 + G >= 0 && -2 + G + Z >= 0 && G + M >= 0 && G + -1*M >= 0 && -2 + A + G >= 0 && 2 + -1*L1 >= 0 && 2 + D1 + -1*L1 >= 0 && 2 + -1*D1 + -1*L1 >= 0 && C + -1*L1 >= 0 && 2 + B1 + -1*L1 >= 0 && 2 + -1*B1 + -1*L1 >= 0 && -1*L1 + Z >= 0 && 2 + -1*L1 + M >= 0 && 2 + -1*L1 + -1*M >= 0 && A + -1*L1 >= 0 && -2 + L1 >= 0 && -2 + D1 + L1 >= 0 && -2 + -1*D1 + L1 >= 0 && -4 + C + L1 >= 0 && -2 + B1 + L1 >= 0 && -2 + -1*B1 + L1 >= 0 && -4 + L1 + Z >= 0 && -2 + L1 + M >= 0 && -2 + L1 + -1*M >= 0 && -4 + A + L1 >= 0 && A1 + -1*H1 >= 0 && -1 + B + -1*H1 >= 0 && F1 + -1*G1 >= 0 && -1*F1 + G1 >= 0 && -1*D1 >= 0 && -2 + C + -1*D1 >= 0 && B1 + -1*D1 >= 0 && -1*B1 + -1*D1 >= 0 && -2 + -1*D1 + Z >= 0 && -1*D1 + M >= 0 && -1*D1 + -1*M >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + C + D1 >= 0 && B1 + D1 >= 0 && -1*B1 + D1 >= 0 && -2 + D1 + Z >= 0 && D1 + M >= 0 && D1 + -1*M >= 0 && -2 + A + D1 >= 0 && -2 + C >= 0 && -2 + B1 + C >= 0 && -2 + -1*B1 + C >= 0 && -4 + C + Z >= 0 && -2 + C + M >= 0 && -2 + C + -1*M >= 0 && -4 + A + C >= 0 && -1*B1 >= 0 && -2 + -1*B1 + Z >= 0 && -1*B1 + M >= 0 && -1*B1 + -1*M >= 0 && -2 + A + -1*B1 >= 0 && B1 >= 0 && -2 + B1 + Z >= 0 && B1 + M >= 0 && B1 + -1*M >= 0 && -2 + A + B1 >= 0 && -1 + -1*A1 + B >= 0 && 1 + A1 + -1*B >= 0 && -2 + Z >= 0 && -2 + M + Z >= 0 && -2 + -1*M + Z >= 0 && -4 + A + Z >= 0 && -1*M >= 0 && -2 + A + -1*M >= 0 && M >= 0 && -2 + A + M >= 0 && -2 + A >= 0 && M1 >= 2 && H1 >= 0 && B1 = 0] 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) = G >= G = f8(A,B,M1,O1,P1,F,G,H,I,J,K,L,0,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,0,O1,0,O1,G1,G1,-1 + H1,-1 + H1,J1,K1,L1) * Step 4: Failure MAYBE + Considered Problem: Rules: 0. f9(A,B,C,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) -> f10(T1,B,1,S1,E,F,G,H,I,J,K,L,0,N,O,P,R1,Y1,B2,A2,U,V,Z1,C2,D2,Z,A1,Q1,M1,O1,P1,E2,N1,H1,I1,U1,K1,L1) [S = 0] (1,1) 1. f9(A,B,C,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) -> f10(T1,B,M1,0,E,F,G,H,I,J,K,L,0,N,O,P,R1,Y1,B2,A2,U,V,Z1,C2,D2,Z,A1,N1,O1,P1,Q1,E2,S1,H1,I1,U1,K1,L1) [0 >= V1 && 0 >= W1 && 0 >= M1 && 0 >= X1] (1,1) 2. f9(A,B,C,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,B,M1,D,E,F,G,H,I,J,K,L,M,N,O,P,M1,P1,Q1,P1,U,V,P1,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,O1,N1,2) [M1 >= 2] (1,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) -> f16(G,0,M1,R,E,F,G,H,I,J,K,L,R,N,O,P,O1,P1,S1,N1,U,V,Q1,T1,U1,R1,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) [2 + -1*L1 >= 0 (1,1) && -1*L1 + Q >= 0 && A + -1*L1 >= 0 && -2 + L1 >= 0 && -4 + L1 + Q >= 0 && -4 + A + L1 >= 0 && -2 + Q >= 0 && -4 + A + Q >= 0 && -1*A + Q >= 0 && -2 + A >= 0 && A >= Q && A >= 0 && M1 >= 2 && R1 >= M1 && G >= M1 && B = 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) -> f1(1 + A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,S,M1,S,O1,A,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) [2 + -1*L1 >= 0 (?,1) && -1*L1 + Q >= 0 && A + -1*L1 >= 0 && -2 + L1 >= 0 && -4 + L1 + Q >= 0 && -4 + A + L1 >= 0 && -2 + Q >= 0 && -4 + A + Q >= 0 && -1*A + Q >= 0 && -2 + A >= 0 && Q >= 1 + A && A >= 0] 5. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f8(A,1 + H1,M1,D,E,F,G,H,I,J,K,L,0,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,H1,0,D,0,D,D,D,H1,I1,J1,K1,L1) [A + -1*G >= 0 (1,1) && -2 + B + G >= 0 && 2 + -1*L1 >= 0 && C + -1*L1 >= 0 && -1*L1 + Z >= 0 && 2 + B + -1*L1 >= 0 && A + -1*L1 >= 0 && -2 + L1 >= 0 && -4 + C + L1 >= 0 && -4 + L1 + Z >= 0 && -2 + B + L1 >= 0 && -4 + A + L1 >= 0 && -2 + C >= 0 && -4 + C + Z >= 0 && -2 + B + C >= 0 && -4 + A + C >= 0 && -2 + Z >= 0 && -2 + B + Z >= 0 && -4 + A + Z >= 0 && B >= 0 && -2 + A + B >= 0 && -2 + A >= 0 && O1 >= 2 && M1 >= 2 && G >= 0 && M = 0] 6. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1) -> f16(A,1 + B,M1,O1,P1,F,-1 + G,H,I,J,K,M,M,Q1,1 + B,-1 + G,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1[A + -1*G >= 0 (1 + G,1) ,J1,K1,L1) && -2 + B + G >= 0 && 2 + -1*L1 >= 0 && C + -1*L1 >= 0 && -1*L1 + Z >= 0 && 2 + B + -1*L1 >= 0 && A + -1*L1 >= 0 && -2 + L1 >= 0 && -4 + C + L1 >= 0 && -4 + L1 + Z >= 0 && -2 + B + L1 >= 0 && -4 + A + L1 >= 0 && -2 + C >= 0 && -4 + C + Z >= 0 && -2 + B + C >= 0 && -4 + A + C >= 0 && -2 + Z >= 0 && -2 + B + Z >= 0 && -4 + A + Z >= 0 && B >= 0 && -2 + A + B >= 0 && -2 + A >= 0 && G >= 0 && M1 >= 2] 7. 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) -> f10(A,B,M1,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,T1,Z,A1,N1,O1,P1,Q1,U1,S1,H1,I1,J1,K1,L1) [A + -1*G >= 0 (1,1) && G >= 0 && -2 + G + L1 >= 0 && 2 + G + -1*L1 >= 0 && D1 + G >= 0 && -1*D1 + G >= 0 && -2 + C + G >= 0 && B1 + G >= 0 && -1*B1 + G >= 0 && -2 + G + Z >= 0 && G + M >= 0 && G + -1*M >= 0 && -2 + A + G >= 0 && 2 + -1*L1 >= 0 && 2 + D1 + -1*L1 >= 0 && 2 + -1*D1 + -1*L1 >= 0 && C + -1*L1 >= 0 && 2 + B1 + -1*L1 >= 0 && 2 + -1*B1 + -1*L1 >= 0 && -1*L1 + Z >= 0 && 2 + -1*L1 + M >= 0 && 2 + -1*L1 + -1*M >= 0 && A + -1*L1 >= 0 && -2 + L1 >= 0 && -2 + D1 + L1 >= 0 && -2 + -1*D1 + L1 >= 0 && -4 + C + L1 >= 0 && -2 + B1 + L1 >= 0 && -2 + -1*B1 + L1 >= 0 && -4 + L1 + Z >= 0 && -2 + L1 + M >= 0 && -2 + L1 + -1*M >= 0 && -4 + A + L1 >= 0 && A1 + -1*H1 >= 0 && -1 + B + -1*H1 >= 0 && F1 + -1*G1 >= 0 && -1*F1 + G1 >= 0 && -1*D1 >= 0 && -2 + C + -1*D1 >= 0 && B1 + -1*D1 >= 0 && -1*B1 + -1*D1 >= 0 && -2 + -1*D1 + Z >= 0 && -1*D1 + M >= 0 && -1*D1 + -1*M >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + C + D1 >= 0 && B1 + D1 >= 0 && -1*B1 + D1 >= 0 && -2 + D1 + Z >= 0 && D1 + M >= 0 && D1 + -1*M >= 0 && -2 + A + D1 >= 0 && -2 + C >= 0 && -2 + B1 + C >= 0 && -2 + -1*B1 + C >= 0 && -4 + C + Z >= 0 && -2 + C + M >= 0 && -2 + C + -1*M >= 0 && -4 + A + C >= 0 && -1*B1 >= 0 && -2 + -1*B1 + Z >= 0 && -1*B1 + M >= 0 && -1*B1 + -1*M >= 0 && -2 + A + -1*B1 >= 0 && B1 >= 0 && -2 + B1 + Z >= 0 && B1 + M >= 0 && B1 + -1*M >= 0 && -2 + A + B1 >= 0 && -1 + -1*A1 + B >= 0 && 1 + A1 + -1*B >= 0 && -2 + Z >= 0 && -2 + M + Z >= 0 && -2 + -1*M + Z >= 0 && -4 + A + Z >= 0 && -1*M >= 0 && -2 + A + -1*M >= 0 && M >= 0 && -2 + A + M >= 0 && -2 + A >= 0 && M1 >= 2 && H1 >= 0 && B1 = G1] 8. 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,M1,O1,P1,F,G,H,I,J,K,L,0,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,0,O1,0,O1,G1,G1,-1 + H1,-1 + H1,J1,K1,L1) [A + -1*G >= 0 (1 + H1,1) && G >= 0 && -2 + G + L1 >= 0 && 2 + G + -1*L1 >= 0 && D1 + G >= 0 && -1*D1 + G >= 0 && -2 + C + G >= 0 && B1 + G >= 0 && -1*B1 + G >= 0 && -2 + G + Z >= 0 && G + M >= 0 && G + -1*M >= 0 && -2 + A + G >= 0 && 2 + -1*L1 >= 0 && 2 + D1 + -1*L1 >= 0 && 2 + -1*D1 + -1*L1 >= 0 && C + -1*L1 >= 0 && 2 + B1 + -1*L1 >= 0 && 2 + -1*B1 + -1*L1 >= 0 && -1*L1 + Z >= 0 && 2 + -1*L1 + M >= 0 && 2 + -1*L1 + -1*M >= 0 && A + -1*L1 >= 0 && -2 + L1 >= 0 && -2 + D1 + L1 >= 0 && -2 + -1*D1 + L1 >= 0 && -4 + C + L1 >= 0 && -2 + B1 + L1 >= 0 && -2 + -1*B1 + L1 >= 0 && -4 + L1 + Z >= 0 && -2 + L1 + M >= 0 && -2 + L1 + -1*M >= 0 && -4 + A + L1 >= 0 && A1 + -1*H1 >= 0 && -1 + B + -1*H1 >= 0 && F1 + -1*G1 >= 0 && -1*F1 + G1 >= 0 && -1*D1 >= 0 && -2 + C + -1*D1 >= 0 && B1 + -1*D1 >= 0 && -1*B1 + -1*D1 >= 0 && -2 + -1*D1 + Z >= 0 && -1*D1 + M >= 0 && -1*D1 + -1*M >= 0 && -2 + A + -1*D1 >= 0 && D1 >= 0 && -2 + C + D1 >= 0 && B1 + D1 >= 0 && -1*B1 + D1 >= 0 && -2 + D1 + Z >= 0 && D1 + M >= 0 && D1 + -1*M >= 0 && -2 + A + D1 >= 0 && -2 + C >= 0 && -2 + B1 + C >= 0 && -2 + -1*B1 + C >= 0 && -4 + C + Z >= 0 && -2 + C + M >= 0 && -2 + C + -1*M >= 0 && -4 + A + C >= 0 && -1*B1 >= 0 && -2 + -1*B1 + Z >= 0 && -1*B1 + M >= 0 && -1*B1 + -1*M >= 0 && -2 + A + -1*B1 >= 0 && B1 >= 0 && -2 + B1 + Z >= 0 && B1 + M >= 0 && B1 + -1*M >= 0 && -2 + A + B1 >= 0 && -1 + -1*A1 + B >= 0 && 1 + A1 + -1*B >= 0 && -2 + Z >= 0 && -2 + M + Z >= 0 && -2 + -1*M + Z >= 0 && -4 + A + Z >= 0 && -1*M >= 0 && -2 + A + -1*M >= 0 && M >= 0 && -2 + A + M >= 0 && -2 + A >= 0 && M1 >= 2 && H1 >= 0 && B1 = 0] Signature: {(f1,38);(f10,38);(f16,38);(f8,38);(f9,38)} Flow Graph: [0->{},1->{},2->{3,4},3->{5,6},4->{3,4},5->{7,8},6->{5,6},7->{},8->{7,8}] + Applied Processor: Failing "Open problems left." + Details: Open problems left. MAYBE