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