WORST_CASE(?,O(n^1)) * Step 1: RestrictVarsProcessor WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. f16(A,B,C,D,E,F,G,H,I,J) -> f19(A,0,C,D,E,F,G,H,I,J) [19 >= A] (?,1) 1. f33(A,B,C,D,E,F,G,H,I,J) -> f36(A,B,C,0,E,F,G,H,I,J) [19 >= C] (?,1) 2. f52(A,B,C,D,E,F,G,H,I,J) -> f55(A,B,C,D,E,0,G,H,I,J) [19 >= E] (?,1) 3. f55(A,B,C,D,E,F,G,H,I,J) -> f59(A,B,C,D,E,F,0,H,I,J) [19 >= F] (?,1) 4. f59(A,B,C,D,E,F,G,H,I,J) -> f59(A,B,C,D,E,F,1 + G,H,I,J) [19 >= G] (?,1) 5. f59(A,B,C,D,E,F,G,H,I,J) -> f55(A,B,C,D,E,1 + F,G,H,I,J) [G >= 20] (?,1) 6. f55(A,B,C,D,E,F,G,H,I,J) -> f52(A,B,C,D,1 + E,F,G,H,I,J) [F >= 20] (?,1) 7. f52(A,B,C,D,E,F,G,H,I,J) -> f73(A,B,C,D,E,F,G,H,I,J) [E >= 20] (?,1) 8. f36(A,B,C,D,E,F,G,H,I,J) -> f36(A,B,C,1 + D,E,F,G,K,K,J) [19 >= D] (?,1) 9. f36(A,B,C,D,E,F,G,H,I,J) -> f33(A,B,1 + C,D,E,F,G,H,I,J) [D >= 20] (?,1) 10. f33(A,B,C,D,E,F,G,H,I,J) -> f52(A,B,C,D,0,F,G,H,I,J) [C >= 20] (?,1) 11. f19(A,B,C,D,E,F,G,H,I,J) -> f19(A,1 + B,C,D,E,F,G,K,I,K) [19 >= B] (?,1) 12. f19(A,B,C,D,E,F,G,H,I,J) -> f16(1 + A,B,C,D,E,F,G,H,I,J) [B >= 20] (?,1) 13. f16(A,B,C,D,E,F,G,H,I,J) -> f33(A,B,0,D,E,F,G,H,I,J) [A >= 20] (?,1) 14. f0(A,B,C,D,E,F,G,H,I,J) -> f16(0,B,C,D,E,F,G,0,I,J) True (1,1) Signature: {(f0,10);(f16,10);(f19,10);(f33,10);(f36,10);(f52,10);(f55,10);(f59,10);(f73,10)} Flow Graph: [0->{11,12},1->{8,9},2->{3,6},3->{4,5},4->{4,5},5->{3,6},6->{2,7},7->{},8->{8,9},9->{1,10},10->{2,7} ,11->{11,12},12->{0,13},13->{1,10},14->{0,13}] + Applied Processor: RestrictVarsProcessor + Details: We removed the arguments [H,I,J] . * Step 2: LocalSizeboundsProc WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. f16(A,B,C,D,E,F,G) -> f19(A,0,C,D,E,F,G) [19 >= A] (?,1) 1. f33(A,B,C,D,E,F,G) -> f36(A,B,C,0,E,F,G) [19 >= C] (?,1) 2. f52(A,B,C,D,E,F,G) -> f55(A,B,C,D,E,0,G) [19 >= E] (?,1) 3. f55(A,B,C,D,E,F,G) -> f59(A,B,C,D,E,F,0) [19 >= F] (?,1) 4. f59(A,B,C,D,E,F,G) -> f59(A,B,C,D,E,F,1 + G) [19 >= G] (?,1) 5. f59(A,B,C,D,E,F,G) -> f55(A,B,C,D,E,1 + F,G) [G >= 20] (?,1) 6. f55(A,B,C,D,E,F,G) -> f52(A,B,C,D,1 + E,F,G) [F >= 20] (?,1) 7. f52(A,B,C,D,E,F,G) -> f73(A,B,C,D,E,F,G) [E >= 20] (?,1) 8. f36(A,B,C,D,E,F,G) -> f36(A,B,C,1 + D,E,F,G) [19 >= D] (?,1) 9. f36(A,B,C,D,E,F,G) -> f33(A,B,1 + C,D,E,F,G) [D >= 20] (?,1) 10. f33(A,B,C,D,E,F,G) -> f52(A,B,C,D,0,F,G) [C >= 20] (?,1) 11. f19(A,B,C,D,E,F,G) -> f19(A,1 + B,C,D,E,F,G) [19 >= B] (?,1) 12. f19(A,B,C,D,E,F,G) -> f16(1 + A,B,C,D,E,F,G) [B >= 20] (?,1) 13. f16(A,B,C,D,E,F,G) -> f33(A,B,0,D,E,F,G) [A >= 20] (?,1) 14. f0(A,B,C,D,E,F,G) -> f16(0,B,C,D,E,F,G) True (1,1) Signature: {(f0,7);(f16,7);(f19,7);(f33,7);(f36,7);(f52,7);(f55,7);(f59,7);(f73,7)} Flow Graph: [0->{11,12},1->{8,9},2->{3,6},3->{4,5},4->{4,5},5->{3,6},6->{2,7},7->{},8->{8,9},9->{1,10},10->{2,7} ,11->{11,12},12->{0,13},13->{1,10},14->{0,13}] + Applied Processor: LocalSizeboundsProc + Details: LocalSizebounds generated; rvgraph (< 0,0,A>, A, .= 0) (< 0,0,B>, 0, .= 0) (< 0,0,C>, C, .= 0) (< 0,0,D>, D, .= 0) (< 0,0,E>, E, .= 0) (< 0,0,F>, F, .= 0) (< 0,0,G>, G, .= 0) (< 1,0,A>, A, .= 0) (< 1,0,B>, B, .= 0) (< 1,0,C>, C, .= 0) (< 1,0,D>, 0, .= 0) (< 1,0,E>, E, .= 0) (< 1,0,F>, F, .= 0) (< 1,0,G>, G, .= 0) (< 2,0,A>, A, .= 0) (< 2,0,B>, B, .= 0) (< 2,0,C>, C, .= 0) (< 2,0,D>, D, .= 0) (< 2,0,E>, E, .= 0) (< 2,0,F>, 0, .= 0) (< 2,0,G>, G, .= 0) (< 3,0,A>, A, .= 0) (< 3,0,B>, B, .= 0) (< 3,0,C>, C, .= 0) (< 3,0,D>, D, .= 0) (< 3,0,E>, E, .= 0) (< 3,0,F>, F, .= 0) (< 3,0,G>, 0, .= 0) (< 4,0,A>, A, .= 0) (< 4,0,B>, B, .= 0) (< 4,0,C>, C, .= 0) (< 4,0,D>, D, .= 0) (< 4,0,E>, E, .= 0) (< 4,0,F>, F, .= 0) (< 4,0,G>, 1 + G, .+ 1) (< 5,0,A>, A, .= 0) (< 5,0,B>, B, .= 0) (< 5,0,C>, C, .= 0) (< 5,0,D>, D, .= 0) (< 5,0,E>, E, .= 0) (< 5,0,F>, 1 + F, .+ 1) (< 5,0,G>, G, .= 0) (< 6,0,A>, A, .= 0) (< 6,0,B>, B, .= 0) (< 6,0,C>, C, .= 0) (< 6,0,D>, D, .= 0) (< 6,0,E>, 1 + E, .+ 1) (< 6,0,F>, F, .= 0) (< 6,0,G>, G, .= 0) (< 7,0,A>, A, .= 0) (< 7,0,B>, B, .= 0) (< 7,0,C>, C, .= 0) (< 7,0,D>, D, .= 0) (< 7,0,E>, E, .= 0) (< 7,0,F>, F, .= 0) (< 7,0,G>, G, .= 0) (< 8,0,A>, A, .= 0) (< 8,0,B>, B, .= 0) (< 8,0,C>, C, .= 0) (< 8,0,D>, 1 + D, .+ 1) (< 8,0,E>, E, .= 0) (< 8,0,F>, F, .= 0) (< 8,0,G>, G, .= 0) (< 9,0,A>, A, .= 0) (< 9,0,B>, B, .= 0) (< 9,0,C>, 1 + C, .+ 1) (< 9,0,D>, D, .= 0) (< 9,0,E>, E, .= 0) (< 9,0,F>, F, .= 0) (< 9,0,G>, G, .= 0) (<10,0,A>, A, .= 0) (<10,0,B>, B, .= 0) (<10,0,C>, C, .= 0) (<10,0,D>, D, .= 0) (<10,0,E>, 0, .= 0) (<10,0,F>, F, .= 0) (<10,0,G>, G, .= 0) (<11,0,A>, A, .= 0) (<11,0,B>, 1 + B, .+ 1) (<11,0,C>, C, .= 0) (<11,0,D>, D, .= 0) (<11,0,E>, E, .= 0) (<11,0,F>, F, .= 0) (<11,0,G>, G, .= 0) (<12,0,A>, 1 + A, .+ 1) (<12,0,B>, B, .= 0) (<12,0,C>, C, .= 0) (<12,0,D>, D, .= 0) (<12,0,E>, E, .= 0) (<12,0,F>, F, .= 0) (<12,0,G>, G, .= 0) (<13,0,A>, A, .= 0) (<13,0,B>, B, .= 0) (<13,0,C>, 0, .= 0) (<13,0,D>, D, .= 0) (<13,0,E>, E, .= 0) (<13,0,F>, F, .= 0) (<13,0,G>, G, .= 0) (<14,0,A>, 0, .= 0) (<14,0,B>, B, .= 0) (<14,0,C>, C, .= 0) (<14,0,D>, D, .= 0) (<14,0,E>, E, .= 0) (<14,0,F>, F, .= 0) (<14,0,G>, G, .= 0) * Step 3: SizeboundsProc WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. f16(A,B,C,D,E,F,G) -> f19(A,0,C,D,E,F,G) [19 >= A] (?,1) 1. f33(A,B,C,D,E,F,G) -> f36(A,B,C,0,E,F,G) [19 >= C] (?,1) 2. f52(A,B,C,D,E,F,G) -> f55(A,B,C,D,E,0,G) [19 >= E] (?,1) 3. f55(A,B,C,D,E,F,G) -> f59(A,B,C,D,E,F,0) [19 >= F] (?,1) 4. f59(A,B,C,D,E,F,G) -> f59(A,B,C,D,E,F,1 + G) [19 >= G] (?,1) 5. f59(A,B,C,D,E,F,G) -> f55(A,B,C,D,E,1 + F,G) [G >= 20] (?,1) 6. f55(A,B,C,D,E,F,G) -> f52(A,B,C,D,1 + E,F,G) [F >= 20] (?,1) 7. f52(A,B,C,D,E,F,G) -> f73(A,B,C,D,E,F,G) [E >= 20] (?,1) 8. f36(A,B,C,D,E,F,G) -> f36(A,B,C,1 + D,E,F,G) [19 >= D] (?,1) 9. f36(A,B,C,D,E,F,G) -> f33(A,B,1 + C,D,E,F,G) [D >= 20] (?,1) 10. f33(A,B,C,D,E,F,G) -> f52(A,B,C,D,0,F,G) [C >= 20] (?,1) 11. f19(A,B,C,D,E,F,G) -> f19(A,1 + B,C,D,E,F,G) [19 >= B] (?,1) 12. f19(A,B,C,D,E,F,G) -> f16(1 + A,B,C,D,E,F,G) [B >= 20] (?,1) 13. f16(A,B,C,D,E,F,G) -> f33(A,B,0,D,E,F,G) [A >= 20] (?,1) 14. f0(A,B,C,D,E,F,G) -> f16(0,B,C,D,E,F,G) True (1,1) Signature: {(f0,7);(f16,7);(f19,7);(f33,7);(f36,7);(f52,7);(f55,7);(f59,7);(f73,7)} Flow Graph: [0->{11,12},1->{8,9},2->{3,6},3->{4,5},4->{4,5},5->{3,6},6->{2,7},7->{},8->{8,9},9->{1,10},10->{2,7} ,11->{11,12},12->{0,13},13->{1,10},14->{0,13}] Sizebounds: (< 0,0,A>, ?) (< 0,0,B>, ?) (< 0,0,C>, ?) (< 0,0,D>, ?) (< 0,0,E>, ?) (< 0,0,F>, ?) (< 0,0,G>, ?) (< 1,0,A>, ?) (< 1,0,B>, ?) (< 1,0,C>, ?) (< 1,0,D>, ?) (< 1,0,E>, ?) (< 1,0,F>, ?) (< 1,0,G>, ?) (< 2,0,A>, ?) (< 2,0,B>, ?) (< 2,0,C>, ?) (< 2,0,D>, ?) (< 2,0,E>, ?) (< 2,0,F>, ?) (< 2,0,G>, ?) (< 3,0,A>, ?) (< 3,0,B>, ?) (< 3,0,C>, ?) (< 3,0,D>, ?) (< 3,0,E>, ?) (< 3,0,F>, ?) (< 3,0,G>, ?) (< 4,0,A>, ?) (< 4,0,B>, ?) (< 4,0,C>, ?) (< 4,0,D>, ?) (< 4,0,E>, ?) (< 4,0,F>, ?) (< 4,0,G>, ?) (< 5,0,A>, ?) (< 5,0,B>, ?) (< 5,0,C>, ?) (< 5,0,D>, ?) (< 5,0,E>, ?) (< 5,0,F>, ?) (< 5,0,G>, ?) (< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, ?) (< 6,0,D>, ?) (< 6,0,E>, ?) (< 6,0,F>, ?) (< 6,0,G>, ?) (< 7,0,A>, ?) (< 7,0,B>, ?) (< 7,0,C>, ?) (< 7,0,D>, ?) (< 7,0,E>, ?) (< 7,0,F>, ?) (< 7,0,G>, ?) (< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, ?) (< 8,0,D>, ?) (< 8,0,E>, ?) (< 8,0,F>, ?) (< 8,0,G>, ?) (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, ?) (< 9,0,D>, ?) (< 9,0,E>, ?) (< 9,0,F>, ?) (< 9,0,G>, ?) (<10,0,A>, ?) (<10,0,B>, ?) (<10,0,C>, ?) (<10,0,D>, ?) (<10,0,E>, ?) (<10,0,F>, ?) (<10,0,G>, ?) (<11,0,A>, ?) (<11,0,B>, ?) (<11,0,C>, ?) (<11,0,D>, ?) (<11,0,E>, ?) (<11,0,F>, ?) (<11,0,G>, ?) (<12,0,A>, ?) (<12,0,B>, ?) (<12,0,C>, ?) (<12,0,D>, ?) (<12,0,E>, ?) (<12,0,F>, ?) (<12,0,G>, ?) (<13,0,A>, ?) (<13,0,B>, ?) (<13,0,C>, ?) (<13,0,D>, ?) (<13,0,E>, ?) (<13,0,F>, ?) (<13,0,G>, ?) (<14,0,A>, ?) (<14,0,B>, ?) (<14,0,C>, ?) (<14,0,D>, ?) (<14,0,E>, ?) (<14,0,F>, ?) (<14,0,G>, ?) + Applied Processor: SizeboundsProc + Details: Sizebounds computed: (< 0,0,A>, 19) (< 0,0,B>, 0) (< 0,0,C>, C) (< 0,0,D>, D) (< 0,0,E>, E) (< 0,0,F>, F) (< 0,0,G>, G) (< 1,0,A>, ?) (< 1,0,B>, ?) (< 1,0,C>, 19) (< 1,0,D>, 0) (< 1,0,E>, E) (< 1,0,F>, F) (< 1,0,G>, G) (< 2,0,A>, ?) (< 2,0,B>, ?) (< 2,0,C>, ?) (< 2,0,D>, ?) (< 2,0,E>, 19) (< 2,0,F>, 0) (< 2,0,G>, ?) (< 3,0,A>, ?) (< 3,0,B>, ?) (< 3,0,C>, ?) (< 3,0,D>, ?) (< 3,0,E>, ?) (< 3,0,F>, 19) (< 3,0,G>, 0) (< 4,0,A>, ?) (< 4,0,B>, ?) (< 4,0,C>, ?) (< 4,0,D>, ?) (< 4,0,E>, ?) (< 4,0,F>, 19) (< 4,0,G>, 20) (< 5,0,A>, ?) (< 5,0,B>, ?) (< 5,0,C>, ?) (< 5,0,D>, ?) (< 5,0,E>, ?) (< 5,0,F>, 19) (< 5,0,G>, 20) (< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, ?) (< 6,0,D>, ?) (< 6,0,E>, ?) (< 6,0,F>, 19) (< 6,0,G>, ?) (< 7,0,A>, ?) (< 7,0,B>, ?) (< 7,0,C>, ?) (< 7,0,D>, ?) (< 7,0,E>, ?) (< 7,0,F>, 19 + F) (< 7,0,G>, ?) (< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, 19) (< 8,0,D>, 20) (< 8,0,E>, E) (< 8,0,F>, F) (< 8,0,G>, G) (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, 19) (< 9,0,D>, 20) (< 9,0,E>, E) (< 9,0,F>, F) (< 9,0,G>, G) (<10,0,A>, ?) (<10,0,B>, ?) (<10,0,C>, 19) (<10,0,D>, 20 + D) (<10,0,E>, 0) (<10,0,F>, F) (<10,0,G>, G) (<11,0,A>, 19) (<11,0,B>, 20) (<11,0,C>, C) (<11,0,D>, D) (<11,0,E>, E) (<11,0,F>, F) (<11,0,G>, G) (<12,0,A>, 19) (<12,0,B>, 20) (<12,0,C>, C) (<12,0,D>, D) (<12,0,E>, E) (<12,0,F>, F) (<12,0,G>, G) (<13,0,A>, 19) (<13,0,B>, 20 + B) (<13,0,C>, 0) (<13,0,D>, D) (<13,0,E>, E) (<13,0,F>, F) (<13,0,G>, G) (<14,0,A>, 0) (<14,0,B>, B) (<14,0,C>, C) (<14,0,D>, D) (<14,0,E>, E) (<14,0,F>, F) (<14,0,G>, G) * Step 4: UnsatPaths WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. f16(A,B,C,D,E,F,G) -> f19(A,0,C,D,E,F,G) [19 >= A] (?,1) 1. f33(A,B,C,D,E,F,G) -> f36(A,B,C,0,E,F,G) [19 >= C] (?,1) 2. f52(A,B,C,D,E,F,G) -> f55(A,B,C,D,E,0,G) [19 >= E] (?,1) 3. f55(A,B,C,D,E,F,G) -> f59(A,B,C,D,E,F,0) [19 >= F] (?,1) 4. f59(A,B,C,D,E,F,G) -> f59(A,B,C,D,E,F,1 + G) [19 >= G] (?,1) 5. f59(A,B,C,D,E,F,G) -> f55(A,B,C,D,E,1 + F,G) [G >= 20] (?,1) 6. f55(A,B,C,D,E,F,G) -> f52(A,B,C,D,1 + E,F,G) [F >= 20] (?,1) 7. f52(A,B,C,D,E,F,G) -> f73(A,B,C,D,E,F,G) [E >= 20] (?,1) 8. f36(A,B,C,D,E,F,G) -> f36(A,B,C,1 + D,E,F,G) [19 >= D] (?,1) 9. f36(A,B,C,D,E,F,G) -> f33(A,B,1 + C,D,E,F,G) [D >= 20] (?,1) 10. f33(A,B,C,D,E,F,G) -> f52(A,B,C,D,0,F,G) [C >= 20] (?,1) 11. f19(A,B,C,D,E,F,G) -> f19(A,1 + B,C,D,E,F,G) [19 >= B] (?,1) 12. f19(A,B,C,D,E,F,G) -> f16(1 + A,B,C,D,E,F,G) [B >= 20] (?,1) 13. f16(A,B,C,D,E,F,G) -> f33(A,B,0,D,E,F,G) [A >= 20] (?,1) 14. f0(A,B,C,D,E,F,G) -> f16(0,B,C,D,E,F,G) True (1,1) Signature: {(f0,7);(f16,7);(f19,7);(f33,7);(f36,7);(f52,7);(f55,7);(f59,7);(f73,7)} Flow Graph: [0->{11,12},1->{8,9},2->{3,6},3->{4,5},4->{4,5},5->{3,6},6->{2,7},7->{},8->{8,9},9->{1,10},10->{2,7} ,11->{11,12},12->{0,13},13->{1,10},14->{0,13}] Sizebounds: (< 0,0,A>, 19) (< 0,0,B>, 0) (< 0,0,C>, C) (< 0,0,D>, D) (< 0,0,E>, E) (< 0,0,F>, F) (< 0,0,G>, G) (< 1,0,A>, ?) (< 1,0,B>, ?) (< 1,0,C>, 19) (< 1,0,D>, 0) (< 1,0,E>, E) (< 1,0,F>, F) (< 1,0,G>, G) (< 2,0,A>, ?) (< 2,0,B>, ?) (< 2,0,C>, ?) (< 2,0,D>, ?) (< 2,0,E>, 19) (< 2,0,F>, 0) (< 2,0,G>, ?) (< 3,0,A>, ?) (< 3,0,B>, ?) (< 3,0,C>, ?) (< 3,0,D>, ?) (< 3,0,E>, ?) (< 3,0,F>, 19) (< 3,0,G>, 0) (< 4,0,A>, ?) (< 4,0,B>, ?) (< 4,0,C>, ?) (< 4,0,D>, ?) (< 4,0,E>, ?) (< 4,0,F>, 19) (< 4,0,G>, 20) (< 5,0,A>, ?) (< 5,0,B>, ?) (< 5,0,C>, ?) (< 5,0,D>, ?) (< 5,0,E>, ?) (< 5,0,F>, 19) (< 5,0,G>, 20) (< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, ?) (< 6,0,D>, ?) (< 6,0,E>, ?) (< 6,0,F>, 19) (< 6,0,G>, ?) (< 7,0,A>, ?) (< 7,0,B>, ?) (< 7,0,C>, ?) (< 7,0,D>, ?) (< 7,0,E>, ?) (< 7,0,F>, 19 + F) (< 7,0,G>, ?) (< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, 19) (< 8,0,D>, 20) (< 8,0,E>, E) (< 8,0,F>, F) (< 8,0,G>, G) (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, 19) (< 9,0,D>, 20) (< 9,0,E>, E) (< 9,0,F>, F) (< 9,0,G>, G) (<10,0,A>, ?) (<10,0,B>, ?) (<10,0,C>, 19) (<10,0,D>, 20 + D) (<10,0,E>, 0) (<10,0,F>, F) (<10,0,G>, G) (<11,0,A>, 19) (<11,0,B>, 20) (<11,0,C>, C) (<11,0,D>, D) (<11,0,E>, E) (<11,0,F>, F) (<11,0,G>, G) (<12,0,A>, 19) (<12,0,B>, 20) (<12,0,C>, C) (<12,0,D>, D) (<12,0,E>, E) (<12,0,F>, F) (<12,0,G>, G) (<13,0,A>, 19) (<13,0,B>, 20 + B) (<13,0,C>, 0) (<13,0,D>, D) (<13,0,E>, E) (<13,0,F>, F) (<13,0,G>, G) (<14,0,A>, 0) (<14,0,B>, B) (<14,0,C>, C) (<14,0,D>, D) (<14,0,E>, E) (<14,0,F>, F) (<14,0,G>, G) + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(0,12),(1,9),(2,6),(3,5),(10,7),(13,10),(14,13)] * Step 5: LeafRules WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. f16(A,B,C,D,E,F,G) -> f19(A,0,C,D,E,F,G) [19 >= A] (?,1) 1. f33(A,B,C,D,E,F,G) -> f36(A,B,C,0,E,F,G) [19 >= C] (?,1) 2. f52(A,B,C,D,E,F,G) -> f55(A,B,C,D,E,0,G) [19 >= E] (?,1) 3. f55(A,B,C,D,E,F,G) -> f59(A,B,C,D,E,F,0) [19 >= F] (?,1) 4. f59(A,B,C,D,E,F,G) -> f59(A,B,C,D,E,F,1 + G) [19 >= G] (?,1) 5. f59(A,B,C,D,E,F,G) -> f55(A,B,C,D,E,1 + F,G) [G >= 20] (?,1) 6. f55(A,B,C,D,E,F,G) -> f52(A,B,C,D,1 + E,F,G) [F >= 20] (?,1) 7. f52(A,B,C,D,E,F,G) -> f73(A,B,C,D,E,F,G) [E >= 20] (?,1) 8. f36(A,B,C,D,E,F,G) -> f36(A,B,C,1 + D,E,F,G) [19 >= D] (?,1) 9. f36(A,B,C,D,E,F,G) -> f33(A,B,1 + C,D,E,F,G) [D >= 20] (?,1) 10. f33(A,B,C,D,E,F,G) -> f52(A,B,C,D,0,F,G) [C >= 20] (?,1) 11. f19(A,B,C,D,E,F,G) -> f19(A,1 + B,C,D,E,F,G) [19 >= B] (?,1) 12. f19(A,B,C,D,E,F,G) -> f16(1 + A,B,C,D,E,F,G) [B >= 20] (?,1) 13. f16(A,B,C,D,E,F,G) -> f33(A,B,0,D,E,F,G) [A >= 20] (?,1) 14. f0(A,B,C,D,E,F,G) -> f16(0,B,C,D,E,F,G) True (1,1) Signature: {(f0,7);(f16,7);(f19,7);(f33,7);(f36,7);(f52,7);(f55,7);(f59,7);(f73,7)} Flow Graph: [0->{11},1->{8},2->{3},3->{4},4->{4,5},5->{3,6},6->{2,7},7->{},8->{8,9},9->{1,10},10->{2},11->{11,12} ,12->{0,13},13->{1},14->{0}] Sizebounds: (< 0,0,A>, 19) (< 0,0,B>, 0) (< 0,0,C>, C) (< 0,0,D>, D) (< 0,0,E>, E) (< 0,0,F>, F) (< 0,0,G>, G) (< 1,0,A>, ?) (< 1,0,B>, ?) (< 1,0,C>, 19) (< 1,0,D>, 0) (< 1,0,E>, E) (< 1,0,F>, F) (< 1,0,G>, G) (< 2,0,A>, ?) (< 2,0,B>, ?) (< 2,0,C>, ?) (< 2,0,D>, ?) (< 2,0,E>, 19) (< 2,0,F>, 0) (< 2,0,G>, ?) (< 3,0,A>, ?) (< 3,0,B>, ?) (< 3,0,C>, ?) (< 3,0,D>, ?) (< 3,0,E>, ?) (< 3,0,F>, 19) (< 3,0,G>, 0) (< 4,0,A>, ?) (< 4,0,B>, ?) (< 4,0,C>, ?) (< 4,0,D>, ?) (< 4,0,E>, ?) (< 4,0,F>, 19) (< 4,0,G>, 20) (< 5,0,A>, ?) (< 5,0,B>, ?) (< 5,0,C>, ?) (< 5,0,D>, ?) (< 5,0,E>, ?) (< 5,0,F>, 19) (< 5,0,G>, 20) (< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, ?) (< 6,0,D>, ?) (< 6,0,E>, ?) (< 6,0,F>, 19) (< 6,0,G>, ?) (< 7,0,A>, ?) (< 7,0,B>, ?) (< 7,0,C>, ?) (< 7,0,D>, ?) (< 7,0,E>, ?) (< 7,0,F>, 19 + F) (< 7,0,G>, ?) (< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, 19) (< 8,0,D>, 20) (< 8,0,E>, E) (< 8,0,F>, F) (< 8,0,G>, G) (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, 19) (< 9,0,D>, 20) (< 9,0,E>, E) (< 9,0,F>, F) (< 9,0,G>, G) (<10,0,A>, ?) (<10,0,B>, ?) (<10,0,C>, 19) (<10,0,D>, 20 + D) (<10,0,E>, 0) (<10,0,F>, F) (<10,0,G>, G) (<11,0,A>, 19) (<11,0,B>, 20) (<11,0,C>, C) (<11,0,D>, D) (<11,0,E>, E) (<11,0,F>, F) (<11,0,G>, G) (<12,0,A>, 19) (<12,0,B>, 20) (<12,0,C>, C) (<12,0,D>, D) (<12,0,E>, E) (<12,0,F>, F) (<12,0,G>, G) (<13,0,A>, 19) (<13,0,B>, 20 + B) (<13,0,C>, 0) (<13,0,D>, D) (<13,0,E>, E) (<13,0,F>, F) (<13,0,G>, G) (<14,0,A>, 0) (<14,0,B>, B) (<14,0,C>, C) (<14,0,D>, D) (<14,0,E>, E) (<14,0,F>, F) (<14,0,G>, G) + Applied Processor: LeafRules + Details: The following transitions are estimated by its predecessors and are removed [7] * Step 6: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. f16(A,B,C,D,E,F,G) -> f19(A,0,C,D,E,F,G) [19 >= A] (?,1) 1. f33(A,B,C,D,E,F,G) -> f36(A,B,C,0,E,F,G) [19 >= C] (?,1) 2. f52(A,B,C,D,E,F,G) -> f55(A,B,C,D,E,0,G) [19 >= E] (?,1) 3. f55(A,B,C,D,E,F,G) -> f59(A,B,C,D,E,F,0) [19 >= F] (?,1) 4. f59(A,B,C,D,E,F,G) -> f59(A,B,C,D,E,F,1 + G) [19 >= G] (?,1) 5. f59(A,B,C,D,E,F,G) -> f55(A,B,C,D,E,1 + F,G) [G >= 20] (?,1) 6. f55(A,B,C,D,E,F,G) -> f52(A,B,C,D,1 + E,F,G) [F >= 20] (?,1) 8. f36(A,B,C,D,E,F,G) -> f36(A,B,C,1 + D,E,F,G) [19 >= D] (?,1) 9. f36(A,B,C,D,E,F,G) -> f33(A,B,1 + C,D,E,F,G) [D >= 20] (?,1) 10. f33(A,B,C,D,E,F,G) -> f52(A,B,C,D,0,F,G) [C >= 20] (?,1) 11. f19(A,B,C,D,E,F,G) -> f19(A,1 + B,C,D,E,F,G) [19 >= B] (?,1) 12. f19(A,B,C,D,E,F,G) -> f16(1 + A,B,C,D,E,F,G) [B >= 20] (?,1) 13. f16(A,B,C,D,E,F,G) -> f33(A,B,0,D,E,F,G) [A >= 20] (?,1) 14. f0(A,B,C,D,E,F,G) -> f16(0,B,C,D,E,F,G) True (1,1) Signature: {(f0,7);(f16,7);(f19,7);(f33,7);(f36,7);(f52,7);(f55,7);(f59,7);(f73,7)} Flow Graph: [0->{11},1->{8},2->{3},3->{4},4->{4,5},5->{3,6},6->{2},8->{8,9},9->{1,10},10->{2},11->{11,12},12->{0,13} ,13->{1},14->{0}] Sizebounds: (< 0,0,A>, 19) (< 0,0,B>, 0) (< 0,0,C>, C) (< 0,0,D>, D) (< 0,0,E>, E) (< 0,0,F>, F) (< 0,0,G>, G) (< 1,0,A>, ?) (< 1,0,B>, ?) (< 1,0,C>, 19) (< 1,0,D>, 0) (< 1,0,E>, E) (< 1,0,F>, F) (< 1,0,G>, G) (< 2,0,A>, ?) (< 2,0,B>, ?) (< 2,0,C>, ?) (< 2,0,D>, ?) (< 2,0,E>, 19) (< 2,0,F>, 0) (< 2,0,G>, ?) (< 3,0,A>, ?) (< 3,0,B>, ?) (< 3,0,C>, ?) (< 3,0,D>, ?) (< 3,0,E>, ?) (< 3,0,F>, 19) (< 3,0,G>, 0) (< 4,0,A>, ?) (< 4,0,B>, ?) (< 4,0,C>, ?) (< 4,0,D>, ?) (< 4,0,E>, ?) (< 4,0,F>, 19) (< 4,0,G>, 20) (< 5,0,A>, ?) (< 5,0,B>, ?) (< 5,0,C>, ?) (< 5,0,D>, ?) (< 5,0,E>, ?) (< 5,0,F>, 19) (< 5,0,G>, 20) (< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, ?) (< 6,0,D>, ?) (< 6,0,E>, ?) (< 6,0,F>, 19) (< 6,0,G>, ?) (< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, 19) (< 8,0,D>, 20) (< 8,0,E>, E) (< 8,0,F>, F) (< 8,0,G>, G) (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, 19) (< 9,0,D>, 20) (< 9,0,E>, E) (< 9,0,F>, F) (< 9,0,G>, G) (<10,0,A>, ?) (<10,0,B>, ?) (<10,0,C>, 19) (<10,0,D>, 20 + D) (<10,0,E>, 0) (<10,0,F>, F) (<10,0,G>, G) (<11,0,A>, 19) (<11,0,B>, 20) (<11,0,C>, C) (<11,0,D>, D) (<11,0,E>, E) (<11,0,F>, F) (<11,0,G>, G) (<12,0,A>, 19) (<12,0,B>, 20) (<12,0,C>, C) (<12,0,D>, D) (<12,0,E>, E) (<12,0,F>, F) (<12,0,G>, G) (<13,0,A>, 19) (<13,0,B>, 20 + B) (<13,0,C>, 0) (<13,0,D>, D) (<13,0,E>, E) (<13,0,F>, F) (<13,0,G>, G) (<14,0,A>, 0) (<14,0,B>, B) (<14,0,C>, C) (<14,0,D>, D) (<14,0,E>, E) (<14,0,F>, F) (<14,0,G>, G) + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(f0) = 1 p(f16) = 1 p(f19) = 1 p(f33) = 0 p(f36) = 0 p(f52) = 0 p(f55) = 0 p(f59) = 0 The following rules are strictly oriented: [A >= 20] ==> f16(A,B,C,D,E,F,G) = 1 > 0 = f33(A,B,0,D,E,F,G) The following rules are weakly oriented: [19 >= A] ==> f16(A,B,C,D,E,F,G) = 1 >= 1 = f19(A,0,C,D,E,F,G) [19 >= C] ==> f33(A,B,C,D,E,F,G) = 0 >= 0 = f36(A,B,C,0,E,F,G) [19 >= E] ==> f52(A,B,C,D,E,F,G) = 0 >= 0 = f55(A,B,C,D,E,0,G) [19 >= F] ==> f55(A,B,C,D,E,F,G) = 0 >= 0 = f59(A,B,C,D,E,F,0) [19 >= G] ==> f59(A,B,C,D,E,F,G) = 0 >= 0 = f59(A,B,C,D,E,F,1 + G) [G >= 20] ==> f59(A,B,C,D,E,F,G) = 0 >= 0 = f55(A,B,C,D,E,1 + F,G) [F >= 20] ==> f55(A,B,C,D,E,F,G) = 0 >= 0 = f52(A,B,C,D,1 + E,F,G) [19 >= D] ==> f36(A,B,C,D,E,F,G) = 0 >= 0 = f36(A,B,C,1 + D,E,F,G) [D >= 20] ==> f36(A,B,C,D,E,F,G) = 0 >= 0 = f33(A,B,1 + C,D,E,F,G) [C >= 20] ==> f33(A,B,C,D,E,F,G) = 0 >= 0 = f52(A,B,C,D,0,F,G) [19 >= B] ==> f19(A,B,C,D,E,F,G) = 1 >= 1 = f19(A,1 + B,C,D,E,F,G) [B >= 20] ==> f19(A,B,C,D,E,F,G) = 1 >= 1 = f16(1 + A,B,C,D,E,F,G) True ==> f0(A,B,C,D,E,F,G) = 1 >= 1 = f16(0,B,C,D,E,F,G) * Step 7: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. f16(A,B,C,D,E,F,G) -> f19(A,0,C,D,E,F,G) [19 >= A] (?,1) 1. f33(A,B,C,D,E,F,G) -> f36(A,B,C,0,E,F,G) [19 >= C] (?,1) 2. f52(A,B,C,D,E,F,G) -> f55(A,B,C,D,E,0,G) [19 >= E] (?,1) 3. f55(A,B,C,D,E,F,G) -> f59(A,B,C,D,E,F,0) [19 >= F] (?,1) 4. f59(A,B,C,D,E,F,G) -> f59(A,B,C,D,E,F,1 + G) [19 >= G] (?,1) 5. f59(A,B,C,D,E,F,G) -> f55(A,B,C,D,E,1 + F,G) [G >= 20] (?,1) 6. f55(A,B,C,D,E,F,G) -> f52(A,B,C,D,1 + E,F,G) [F >= 20] (?,1) 8. f36(A,B,C,D,E,F,G) -> f36(A,B,C,1 + D,E,F,G) [19 >= D] (?,1) 9. f36(A,B,C,D,E,F,G) -> f33(A,B,1 + C,D,E,F,G) [D >= 20] (?,1) 10. f33(A,B,C,D,E,F,G) -> f52(A,B,C,D,0,F,G) [C >= 20] (?,1) 11. f19(A,B,C,D,E,F,G) -> f19(A,1 + B,C,D,E,F,G) [19 >= B] (?,1) 12. f19(A,B,C,D,E,F,G) -> f16(1 + A,B,C,D,E,F,G) [B >= 20] (?,1) 13. f16(A,B,C,D,E,F,G) -> f33(A,B,0,D,E,F,G) [A >= 20] (1,1) 14. f0(A,B,C,D,E,F,G) -> f16(0,B,C,D,E,F,G) True (1,1) Signature: {(f0,7);(f16,7);(f19,7);(f33,7);(f36,7);(f52,7);(f55,7);(f59,7);(f73,7)} Flow Graph: [0->{11},1->{8},2->{3},3->{4},4->{4,5},5->{3,6},6->{2},8->{8,9},9->{1,10},10->{2},11->{11,12},12->{0,13} ,13->{1},14->{0}] Sizebounds: (< 0,0,A>, 19) (< 0,0,B>, 0) (< 0,0,C>, C) (< 0,0,D>, D) (< 0,0,E>, E) (< 0,0,F>, F) (< 0,0,G>, G) (< 1,0,A>, ?) (< 1,0,B>, ?) (< 1,0,C>, 19) (< 1,0,D>, 0) (< 1,0,E>, E) (< 1,0,F>, F) (< 1,0,G>, G) (< 2,0,A>, ?) (< 2,0,B>, ?) (< 2,0,C>, ?) (< 2,0,D>, ?) (< 2,0,E>, 19) (< 2,0,F>, 0) (< 2,0,G>, ?) (< 3,0,A>, ?) (< 3,0,B>, ?) (< 3,0,C>, ?) (< 3,0,D>, ?) (< 3,0,E>, ?) (< 3,0,F>, 19) (< 3,0,G>, 0) (< 4,0,A>, ?) (< 4,0,B>, ?) (< 4,0,C>, ?) (< 4,0,D>, ?) (< 4,0,E>, ?) (< 4,0,F>, 19) (< 4,0,G>, 20) (< 5,0,A>, ?) (< 5,0,B>, ?) (< 5,0,C>, ?) (< 5,0,D>, ?) (< 5,0,E>, ?) (< 5,0,F>, 19) (< 5,0,G>, 20) (< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, ?) (< 6,0,D>, ?) (< 6,0,E>, ?) (< 6,0,F>, 19) (< 6,0,G>, ?) (< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, 19) (< 8,0,D>, 20) (< 8,0,E>, E) (< 8,0,F>, F) (< 8,0,G>, G) (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, 19) (< 9,0,D>, 20) (< 9,0,E>, E) (< 9,0,F>, F) (< 9,0,G>, G) (<10,0,A>, ?) (<10,0,B>, ?) (<10,0,C>, 19) (<10,0,D>, 20 + D) (<10,0,E>, 0) (<10,0,F>, F) (<10,0,G>, G) (<11,0,A>, 19) (<11,0,B>, 20) (<11,0,C>, C) (<11,0,D>, D) (<11,0,E>, E) (<11,0,F>, F) (<11,0,G>, G) (<12,0,A>, 19) (<12,0,B>, 20) (<12,0,C>, C) (<12,0,D>, D) (<12,0,E>, E) (<12,0,F>, F) (<12,0,G>, G) (<13,0,A>, 19) (<13,0,B>, 20 + B) (<13,0,C>, 0) (<13,0,D>, D) (<13,0,E>, E) (<13,0,F>, F) (<13,0,G>, G) (<14,0,A>, 0) (<14,0,B>, B) (<14,0,C>, C) (<14,0,D>, D) (<14,0,E>, E) (<14,0,F>, F) (<14,0,G>, G) + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(f0) = 1 p(f16) = 1 p(f19) = 1 p(f33) = 1 p(f36) = 1 p(f52) = 0 p(f55) = 0 p(f59) = 0 The following rules are strictly oriented: [C >= 20] ==> f33(A,B,C,D,E,F,G) = 1 > 0 = f52(A,B,C,D,0,F,G) The following rules are weakly oriented: [19 >= A] ==> f16(A,B,C,D,E,F,G) = 1 >= 1 = f19(A,0,C,D,E,F,G) [19 >= C] ==> f33(A,B,C,D,E,F,G) = 1 >= 1 = f36(A,B,C,0,E,F,G) [19 >= E] ==> f52(A,B,C,D,E,F,G) = 0 >= 0 = f55(A,B,C,D,E,0,G) [19 >= F] ==> f55(A,B,C,D,E,F,G) = 0 >= 0 = f59(A,B,C,D,E,F,0) [19 >= G] ==> f59(A,B,C,D,E,F,G) = 0 >= 0 = f59(A,B,C,D,E,F,1 + G) [G >= 20] ==> f59(A,B,C,D,E,F,G) = 0 >= 0 = f55(A,B,C,D,E,1 + F,G) [F >= 20] ==> f55(A,B,C,D,E,F,G) = 0 >= 0 = f52(A,B,C,D,1 + E,F,G) [19 >= D] ==> f36(A,B,C,D,E,F,G) = 1 >= 1 = f36(A,B,C,1 + D,E,F,G) [D >= 20] ==> f36(A,B,C,D,E,F,G) = 1 >= 1 = f33(A,B,1 + C,D,E,F,G) [19 >= B] ==> f19(A,B,C,D,E,F,G) = 1 >= 1 = f19(A,1 + B,C,D,E,F,G) [B >= 20] ==> f19(A,B,C,D,E,F,G) = 1 >= 1 = f16(1 + A,B,C,D,E,F,G) [A >= 20] ==> f16(A,B,C,D,E,F,G) = 1 >= 1 = f33(A,B,0,D,E,F,G) True ==> f0(A,B,C,D,E,F,G) = 1 >= 1 = f16(0,B,C,D,E,F,G) * Step 8: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. f16(A,B,C,D,E,F,G) -> f19(A,0,C,D,E,F,G) [19 >= A] (?,1) 1. f33(A,B,C,D,E,F,G) -> f36(A,B,C,0,E,F,G) [19 >= C] (?,1) 2. f52(A,B,C,D,E,F,G) -> f55(A,B,C,D,E,0,G) [19 >= E] (?,1) 3. f55(A,B,C,D,E,F,G) -> f59(A,B,C,D,E,F,0) [19 >= F] (?,1) 4. f59(A,B,C,D,E,F,G) -> f59(A,B,C,D,E,F,1 + G) [19 >= G] (?,1) 5. f59(A,B,C,D,E,F,G) -> f55(A,B,C,D,E,1 + F,G) [G >= 20] (?,1) 6. f55(A,B,C,D,E,F,G) -> f52(A,B,C,D,1 + E,F,G) [F >= 20] (?,1) 8. f36(A,B,C,D,E,F,G) -> f36(A,B,C,1 + D,E,F,G) [19 >= D] (?,1) 9. f36(A,B,C,D,E,F,G) -> f33(A,B,1 + C,D,E,F,G) [D >= 20] (?,1) 10. f33(A,B,C,D,E,F,G) -> f52(A,B,C,D,0,F,G) [C >= 20] (1,1) 11. f19(A,B,C,D,E,F,G) -> f19(A,1 + B,C,D,E,F,G) [19 >= B] (?,1) 12. f19(A,B,C,D,E,F,G) -> f16(1 + A,B,C,D,E,F,G) [B >= 20] (?,1) 13. f16(A,B,C,D,E,F,G) -> f33(A,B,0,D,E,F,G) [A >= 20] (1,1) 14. f0(A,B,C,D,E,F,G) -> f16(0,B,C,D,E,F,G) True (1,1) Signature: {(f0,7);(f16,7);(f19,7);(f33,7);(f36,7);(f52,7);(f55,7);(f59,7);(f73,7)} Flow Graph: [0->{11},1->{8},2->{3},3->{4},4->{4,5},5->{3,6},6->{2},8->{8,9},9->{1,10},10->{2},11->{11,12},12->{0,13} ,13->{1},14->{0}] Sizebounds: (< 0,0,A>, 19) (< 0,0,B>, 0) (< 0,0,C>, C) (< 0,0,D>, D) (< 0,0,E>, E) (< 0,0,F>, F) (< 0,0,G>, G) (< 1,0,A>, ?) (< 1,0,B>, ?) (< 1,0,C>, 19) (< 1,0,D>, 0) (< 1,0,E>, E) (< 1,0,F>, F) (< 1,0,G>, G) (< 2,0,A>, ?) (< 2,0,B>, ?) (< 2,0,C>, ?) (< 2,0,D>, ?) (< 2,0,E>, 19) (< 2,0,F>, 0) (< 2,0,G>, ?) (< 3,0,A>, ?) (< 3,0,B>, ?) (< 3,0,C>, ?) (< 3,0,D>, ?) (< 3,0,E>, ?) (< 3,0,F>, 19) (< 3,0,G>, 0) (< 4,0,A>, ?) (< 4,0,B>, ?) (< 4,0,C>, ?) (< 4,0,D>, ?) (< 4,0,E>, ?) (< 4,0,F>, 19) (< 4,0,G>, 20) (< 5,0,A>, ?) (< 5,0,B>, ?) (< 5,0,C>, ?) (< 5,0,D>, ?) (< 5,0,E>, ?) (< 5,0,F>, 19) (< 5,0,G>, 20) (< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, ?) (< 6,0,D>, ?) (< 6,0,E>, ?) (< 6,0,F>, 19) (< 6,0,G>, ?) (< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, 19) (< 8,0,D>, 20) (< 8,0,E>, E) (< 8,0,F>, F) (< 8,0,G>, G) (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, 19) (< 9,0,D>, 20) (< 9,0,E>, E) (< 9,0,F>, F) (< 9,0,G>, G) (<10,0,A>, ?) (<10,0,B>, ?) (<10,0,C>, 19) (<10,0,D>, 20 + D) (<10,0,E>, 0) (<10,0,F>, F) (<10,0,G>, G) (<11,0,A>, 19) (<11,0,B>, 20) (<11,0,C>, C) (<11,0,D>, D) (<11,0,E>, E) (<11,0,F>, F) (<11,0,G>, G) (<12,0,A>, 19) (<12,0,B>, 20) (<12,0,C>, C) (<12,0,D>, D) (<12,0,E>, E) (<12,0,F>, F) (<12,0,G>, G) (<13,0,A>, 19) (<13,0,B>, 20 + B) (<13,0,C>, 0) (<13,0,D>, D) (<13,0,E>, E) (<13,0,F>, F) (<13,0,G>, G) (<14,0,A>, 0) (<14,0,B>, B) (<14,0,C>, C) (<14,0,D>, D) (<14,0,E>, E) (<14,0,F>, F) (<14,0,G>, G) + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(f0) = 20 p(f16) = 20 p(f19) = 20 p(f33) = 20 p(f36) = 20 p(f52) = 20 + -1*x5 p(f55) = 19 + -1*x5 p(f59) = 19 + -1*x5 The following rules are strictly oriented: [19 >= E] ==> f52(A,B,C,D,E,F,G) = 20 + -1*E > 19 + -1*E = f55(A,B,C,D,E,0,G) The following rules are weakly oriented: [19 >= A] ==> f16(A,B,C,D,E,F,G) = 20 >= 20 = f19(A,0,C,D,E,F,G) [19 >= C] ==> f33(A,B,C,D,E,F,G) = 20 >= 20 = f36(A,B,C,0,E,F,G) [19 >= F] ==> f55(A,B,C,D,E,F,G) = 19 + -1*E >= 19 + -1*E = f59(A,B,C,D,E,F,0) [19 >= G] ==> f59(A,B,C,D,E,F,G) = 19 + -1*E >= 19 + -1*E = f59(A,B,C,D,E,F,1 + G) [G >= 20] ==> f59(A,B,C,D,E,F,G) = 19 + -1*E >= 19 + -1*E = f55(A,B,C,D,E,1 + F,G) [F >= 20] ==> f55(A,B,C,D,E,F,G) = 19 + -1*E >= 19 + -1*E = f52(A,B,C,D,1 + E,F,G) [19 >= D] ==> f36(A,B,C,D,E,F,G) = 20 >= 20 = f36(A,B,C,1 + D,E,F,G) [D >= 20] ==> f36(A,B,C,D,E,F,G) = 20 >= 20 = f33(A,B,1 + C,D,E,F,G) [C >= 20] ==> f33(A,B,C,D,E,F,G) = 20 >= 20 = f52(A,B,C,D,0,F,G) [19 >= B] ==> f19(A,B,C,D,E,F,G) = 20 >= 20 = f19(A,1 + B,C,D,E,F,G) [B >= 20] ==> f19(A,B,C,D,E,F,G) = 20 >= 20 = f16(1 + A,B,C,D,E,F,G) [A >= 20] ==> f16(A,B,C,D,E,F,G) = 20 >= 20 = f33(A,B,0,D,E,F,G) True ==> f0(A,B,C,D,E,F,G) = 20 >= 20 = f16(0,B,C,D,E,F,G) * Step 9: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. f16(A,B,C,D,E,F,G) -> f19(A,0,C,D,E,F,G) [19 >= A] (?,1) 1. f33(A,B,C,D,E,F,G) -> f36(A,B,C,0,E,F,G) [19 >= C] (?,1) 2. f52(A,B,C,D,E,F,G) -> f55(A,B,C,D,E,0,G) [19 >= E] (20,1) 3. f55(A,B,C,D,E,F,G) -> f59(A,B,C,D,E,F,0) [19 >= F] (?,1) 4. f59(A,B,C,D,E,F,G) -> f59(A,B,C,D,E,F,1 + G) [19 >= G] (?,1) 5. f59(A,B,C,D,E,F,G) -> f55(A,B,C,D,E,1 + F,G) [G >= 20] (?,1) 6. f55(A,B,C,D,E,F,G) -> f52(A,B,C,D,1 + E,F,G) [F >= 20] (?,1) 8. f36(A,B,C,D,E,F,G) -> f36(A,B,C,1 + D,E,F,G) [19 >= D] (?,1) 9. f36(A,B,C,D,E,F,G) -> f33(A,B,1 + C,D,E,F,G) [D >= 20] (?,1) 10. f33(A,B,C,D,E,F,G) -> f52(A,B,C,D,0,F,G) [C >= 20] (1,1) 11. f19(A,B,C,D,E,F,G) -> f19(A,1 + B,C,D,E,F,G) [19 >= B] (?,1) 12. f19(A,B,C,D,E,F,G) -> f16(1 + A,B,C,D,E,F,G) [B >= 20] (?,1) 13. f16(A,B,C,D,E,F,G) -> f33(A,B,0,D,E,F,G) [A >= 20] (1,1) 14. f0(A,B,C,D,E,F,G) -> f16(0,B,C,D,E,F,G) True (1,1) Signature: {(f0,7);(f16,7);(f19,7);(f33,7);(f36,7);(f52,7);(f55,7);(f59,7);(f73,7)} Flow Graph: [0->{11},1->{8},2->{3},3->{4},4->{4,5},5->{3,6},6->{2},8->{8,9},9->{1,10},10->{2},11->{11,12},12->{0,13} ,13->{1},14->{0}] Sizebounds: (< 0,0,A>, 19) (< 0,0,B>, 0) (< 0,0,C>, C) (< 0,0,D>, D) (< 0,0,E>, E) (< 0,0,F>, F) (< 0,0,G>, G) (< 1,0,A>, ?) (< 1,0,B>, ?) (< 1,0,C>, 19) (< 1,0,D>, 0) (< 1,0,E>, E) (< 1,0,F>, F) (< 1,0,G>, G) (< 2,0,A>, ?) (< 2,0,B>, ?) (< 2,0,C>, ?) (< 2,0,D>, ?) (< 2,0,E>, 19) (< 2,0,F>, 0) (< 2,0,G>, ?) (< 3,0,A>, ?) (< 3,0,B>, ?) (< 3,0,C>, ?) (< 3,0,D>, ?) (< 3,0,E>, ?) (< 3,0,F>, 19) (< 3,0,G>, 0) (< 4,0,A>, ?) (< 4,0,B>, ?) (< 4,0,C>, ?) (< 4,0,D>, ?) (< 4,0,E>, ?) (< 4,0,F>, 19) (< 4,0,G>, 20) (< 5,0,A>, ?) (< 5,0,B>, ?) (< 5,0,C>, ?) (< 5,0,D>, ?) (< 5,0,E>, ?) (< 5,0,F>, 19) (< 5,0,G>, 20) (< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, ?) (< 6,0,D>, ?) (< 6,0,E>, ?) (< 6,0,F>, 19) (< 6,0,G>, ?) (< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, 19) (< 8,0,D>, 20) (< 8,0,E>, E) (< 8,0,F>, F) (< 8,0,G>, G) (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, 19) (< 9,0,D>, 20) (< 9,0,E>, E) (< 9,0,F>, F) (< 9,0,G>, G) (<10,0,A>, ?) (<10,0,B>, ?) (<10,0,C>, 19) (<10,0,D>, 20 + D) (<10,0,E>, 0) (<10,0,F>, F) (<10,0,G>, G) (<11,0,A>, 19) (<11,0,B>, 20) (<11,0,C>, C) (<11,0,D>, D) (<11,0,E>, E) (<11,0,F>, F) (<11,0,G>, G) (<12,0,A>, 19) (<12,0,B>, 20) (<12,0,C>, C) (<12,0,D>, D) (<12,0,E>, E) (<12,0,F>, F) (<12,0,G>, G) (<13,0,A>, 19) (<13,0,B>, 20 + B) (<13,0,C>, 0) (<13,0,D>, D) (<13,0,E>, E) (<13,0,F>, F) (<13,0,G>, G) (<14,0,A>, 0) (<14,0,B>, B) (<14,0,C>, C) (<14,0,D>, D) (<14,0,E>, E) (<14,0,F>, F) (<14,0,G>, G) + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(f0) = 20 p(f16) = 20 + -1*x1 p(f19) = 19 + -1*x1 p(f33) = 1 + -1*x1 p(f36) = 1 + -1*x1 p(f52) = 1 + -1*x1 p(f55) = 1 + -1*x1 p(f59) = 1 + -1*x1 The following rules are strictly oriented: [19 >= A] ==> f16(A,B,C,D,E,F,G) = 20 + -1*A > 19 + -1*A = f19(A,0,C,D,E,F,G) The following rules are weakly oriented: [19 >= C] ==> f33(A,B,C,D,E,F,G) = 1 + -1*A >= 1 + -1*A = f36(A,B,C,0,E,F,G) [19 >= E] ==> f52(A,B,C,D,E,F,G) = 1 + -1*A >= 1 + -1*A = f55(A,B,C,D,E,0,G) [19 >= F] ==> f55(A,B,C,D,E,F,G) = 1 + -1*A >= 1 + -1*A = f59(A,B,C,D,E,F,0) [19 >= G] ==> f59(A,B,C,D,E,F,G) = 1 + -1*A >= 1 + -1*A = f59(A,B,C,D,E,F,1 + G) [G >= 20] ==> f59(A,B,C,D,E,F,G) = 1 + -1*A >= 1 + -1*A = f55(A,B,C,D,E,1 + F,G) [F >= 20] ==> f55(A,B,C,D,E,F,G) = 1 + -1*A >= 1 + -1*A = f52(A,B,C,D,1 + E,F,G) [19 >= D] ==> f36(A,B,C,D,E,F,G) = 1 + -1*A >= 1 + -1*A = f36(A,B,C,1 + D,E,F,G) [D >= 20] ==> f36(A,B,C,D,E,F,G) = 1 + -1*A >= 1 + -1*A = f33(A,B,1 + C,D,E,F,G) [C >= 20] ==> f33(A,B,C,D,E,F,G) = 1 + -1*A >= 1 + -1*A = f52(A,B,C,D,0,F,G) [19 >= B] ==> f19(A,B,C,D,E,F,G) = 19 + -1*A >= 19 + -1*A = f19(A,1 + B,C,D,E,F,G) [B >= 20] ==> f19(A,B,C,D,E,F,G) = 19 + -1*A >= 19 + -1*A = f16(1 + A,B,C,D,E,F,G) [A >= 20] ==> f16(A,B,C,D,E,F,G) = 20 + -1*A >= 1 + -1*A = f33(A,B,0,D,E,F,G) True ==> f0(A,B,C,D,E,F,G) = 20 >= 20 = f16(0,B,C,D,E,F,G) * Step 10: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. f16(A,B,C,D,E,F,G) -> f19(A,0,C,D,E,F,G) [19 >= A] (20,1) 1. f33(A,B,C,D,E,F,G) -> f36(A,B,C,0,E,F,G) [19 >= C] (?,1) 2. f52(A,B,C,D,E,F,G) -> f55(A,B,C,D,E,0,G) [19 >= E] (20,1) 3. f55(A,B,C,D,E,F,G) -> f59(A,B,C,D,E,F,0) [19 >= F] (?,1) 4. f59(A,B,C,D,E,F,G) -> f59(A,B,C,D,E,F,1 + G) [19 >= G] (?,1) 5. f59(A,B,C,D,E,F,G) -> f55(A,B,C,D,E,1 + F,G) [G >= 20] (?,1) 6. f55(A,B,C,D,E,F,G) -> f52(A,B,C,D,1 + E,F,G) [F >= 20] (?,1) 8. f36(A,B,C,D,E,F,G) -> f36(A,B,C,1 + D,E,F,G) [19 >= D] (?,1) 9. f36(A,B,C,D,E,F,G) -> f33(A,B,1 + C,D,E,F,G) [D >= 20] (?,1) 10. f33(A,B,C,D,E,F,G) -> f52(A,B,C,D,0,F,G) [C >= 20] (1,1) 11. f19(A,B,C,D,E,F,G) -> f19(A,1 + B,C,D,E,F,G) [19 >= B] (?,1) 12. f19(A,B,C,D,E,F,G) -> f16(1 + A,B,C,D,E,F,G) [B >= 20] (?,1) 13. f16(A,B,C,D,E,F,G) -> f33(A,B,0,D,E,F,G) [A >= 20] (1,1) 14. f0(A,B,C,D,E,F,G) -> f16(0,B,C,D,E,F,G) True (1,1) Signature: {(f0,7);(f16,7);(f19,7);(f33,7);(f36,7);(f52,7);(f55,7);(f59,7);(f73,7)} Flow Graph: [0->{11},1->{8},2->{3},3->{4},4->{4,5},5->{3,6},6->{2},8->{8,9},9->{1,10},10->{2},11->{11,12},12->{0,13} ,13->{1},14->{0}] Sizebounds: (< 0,0,A>, 19) (< 0,0,B>, 0) (< 0,0,C>, C) (< 0,0,D>, D) (< 0,0,E>, E) (< 0,0,F>, F) (< 0,0,G>, G) (< 1,0,A>, ?) (< 1,0,B>, ?) (< 1,0,C>, 19) (< 1,0,D>, 0) (< 1,0,E>, E) (< 1,0,F>, F) (< 1,0,G>, G) (< 2,0,A>, ?) (< 2,0,B>, ?) (< 2,0,C>, ?) (< 2,0,D>, ?) (< 2,0,E>, 19) (< 2,0,F>, 0) (< 2,0,G>, ?) (< 3,0,A>, ?) (< 3,0,B>, ?) (< 3,0,C>, ?) (< 3,0,D>, ?) (< 3,0,E>, ?) (< 3,0,F>, 19) (< 3,0,G>, 0) (< 4,0,A>, ?) (< 4,0,B>, ?) (< 4,0,C>, ?) (< 4,0,D>, ?) (< 4,0,E>, ?) (< 4,0,F>, 19) (< 4,0,G>, 20) (< 5,0,A>, ?) (< 5,0,B>, ?) (< 5,0,C>, ?) (< 5,0,D>, ?) (< 5,0,E>, ?) (< 5,0,F>, 19) (< 5,0,G>, 20) (< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, ?) (< 6,0,D>, ?) (< 6,0,E>, ?) (< 6,0,F>, 19) (< 6,0,G>, ?) (< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, 19) (< 8,0,D>, 20) (< 8,0,E>, E) (< 8,0,F>, F) (< 8,0,G>, G) (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, 19) (< 9,0,D>, 20) (< 9,0,E>, E) (< 9,0,F>, F) (< 9,0,G>, G) (<10,0,A>, ?) (<10,0,B>, ?) (<10,0,C>, 19) (<10,0,D>, 20 + D) (<10,0,E>, 0) (<10,0,F>, F) (<10,0,G>, G) (<11,0,A>, 19) (<11,0,B>, 20) (<11,0,C>, C) (<11,0,D>, D) (<11,0,E>, E) (<11,0,F>, F) (<11,0,G>, G) (<12,0,A>, 19) (<12,0,B>, 20) (<12,0,C>, C) (<12,0,D>, D) (<12,0,E>, E) (<12,0,F>, F) (<12,0,G>, G) (<13,0,A>, 19) (<13,0,B>, 20 + B) (<13,0,C>, 0) (<13,0,D>, D) (<13,0,E>, E) (<13,0,F>, F) (<13,0,G>, G) (<14,0,A>, 0) (<14,0,B>, B) (<14,0,C>, C) (<14,0,D>, D) (<14,0,E>, E) (<14,0,F>, F) (<14,0,G>, G) + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(f0) = 20 p(f16) = 20 p(f19) = 20 p(f33) = 20 + -1*x3 p(f36) = 19 + -1*x3 p(f52) = 20 + -1*x3 p(f55) = 20 + -1*x3 p(f59) = 20 + -1*x3 The following rules are strictly oriented: [19 >= C] ==> f33(A,B,C,D,E,F,G) = 20 + -1*C > 19 + -1*C = f36(A,B,C,0,E,F,G) The following rules are weakly oriented: [19 >= A] ==> f16(A,B,C,D,E,F,G) = 20 >= 20 = f19(A,0,C,D,E,F,G) [19 >= E] ==> f52(A,B,C,D,E,F,G) = 20 + -1*C >= 20 + -1*C = f55(A,B,C,D,E,0,G) [19 >= F] ==> f55(A,B,C,D,E,F,G) = 20 + -1*C >= 20 + -1*C = f59(A,B,C,D,E,F,0) [19 >= G] ==> f59(A,B,C,D,E,F,G) = 20 + -1*C >= 20 + -1*C = f59(A,B,C,D,E,F,1 + G) [G >= 20] ==> f59(A,B,C,D,E,F,G) = 20 + -1*C >= 20 + -1*C = f55(A,B,C,D,E,1 + F,G) [F >= 20] ==> f55(A,B,C,D,E,F,G) = 20 + -1*C >= 20 + -1*C = f52(A,B,C,D,1 + E,F,G) [19 >= D] ==> f36(A,B,C,D,E,F,G) = 19 + -1*C >= 19 + -1*C = f36(A,B,C,1 + D,E,F,G) [D >= 20] ==> f36(A,B,C,D,E,F,G) = 19 + -1*C >= 19 + -1*C = f33(A,B,1 + C,D,E,F,G) [C >= 20] ==> f33(A,B,C,D,E,F,G) = 20 + -1*C >= 20 + -1*C = f52(A,B,C,D,0,F,G) [19 >= B] ==> f19(A,B,C,D,E,F,G) = 20 >= 20 = f19(A,1 + B,C,D,E,F,G) [B >= 20] ==> f19(A,B,C,D,E,F,G) = 20 >= 20 = f16(1 + A,B,C,D,E,F,G) [A >= 20] ==> f16(A,B,C,D,E,F,G) = 20 >= 20 = f33(A,B,0,D,E,F,G) True ==> f0(A,B,C,D,E,F,G) = 20 >= 20 = f16(0,B,C,D,E,F,G) * Step 11: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. f16(A,B,C,D,E,F,G) -> f19(A,0,C,D,E,F,G) [19 >= A] (20,1) 1. f33(A,B,C,D,E,F,G) -> f36(A,B,C,0,E,F,G) [19 >= C] (20,1) 2. f52(A,B,C,D,E,F,G) -> f55(A,B,C,D,E,0,G) [19 >= E] (20,1) 3. f55(A,B,C,D,E,F,G) -> f59(A,B,C,D,E,F,0) [19 >= F] (?,1) 4. f59(A,B,C,D,E,F,G) -> f59(A,B,C,D,E,F,1 + G) [19 >= G] (?,1) 5. f59(A,B,C,D,E,F,G) -> f55(A,B,C,D,E,1 + F,G) [G >= 20] (?,1) 6. f55(A,B,C,D,E,F,G) -> f52(A,B,C,D,1 + E,F,G) [F >= 20] (?,1) 8. f36(A,B,C,D,E,F,G) -> f36(A,B,C,1 + D,E,F,G) [19 >= D] (?,1) 9. f36(A,B,C,D,E,F,G) -> f33(A,B,1 + C,D,E,F,G) [D >= 20] (?,1) 10. f33(A,B,C,D,E,F,G) -> f52(A,B,C,D,0,F,G) [C >= 20] (1,1) 11. f19(A,B,C,D,E,F,G) -> f19(A,1 + B,C,D,E,F,G) [19 >= B] (?,1) 12. f19(A,B,C,D,E,F,G) -> f16(1 + A,B,C,D,E,F,G) [B >= 20] (?,1) 13. f16(A,B,C,D,E,F,G) -> f33(A,B,0,D,E,F,G) [A >= 20] (1,1) 14. f0(A,B,C,D,E,F,G) -> f16(0,B,C,D,E,F,G) True (1,1) Signature: {(f0,7);(f16,7);(f19,7);(f33,7);(f36,7);(f52,7);(f55,7);(f59,7);(f73,7)} Flow Graph: [0->{11},1->{8},2->{3},3->{4},4->{4,5},5->{3,6},6->{2},8->{8,9},9->{1,10},10->{2},11->{11,12},12->{0,13} ,13->{1},14->{0}] Sizebounds: (< 0,0,A>, 19) (< 0,0,B>, 0) (< 0,0,C>, C) (< 0,0,D>, D) (< 0,0,E>, E) (< 0,0,F>, F) (< 0,0,G>, G) (< 1,0,A>, ?) (< 1,0,B>, ?) (< 1,0,C>, 19) (< 1,0,D>, 0) (< 1,0,E>, E) (< 1,0,F>, F) (< 1,0,G>, G) (< 2,0,A>, ?) (< 2,0,B>, ?) (< 2,0,C>, ?) (< 2,0,D>, ?) (< 2,0,E>, 19) (< 2,0,F>, 0) (< 2,0,G>, ?) (< 3,0,A>, ?) (< 3,0,B>, ?) (< 3,0,C>, ?) (< 3,0,D>, ?) (< 3,0,E>, ?) (< 3,0,F>, 19) (< 3,0,G>, 0) (< 4,0,A>, ?) (< 4,0,B>, ?) (< 4,0,C>, ?) (< 4,0,D>, ?) (< 4,0,E>, ?) (< 4,0,F>, 19) (< 4,0,G>, 20) (< 5,0,A>, ?) (< 5,0,B>, ?) (< 5,0,C>, ?) (< 5,0,D>, ?) (< 5,0,E>, ?) (< 5,0,F>, 19) (< 5,0,G>, 20) (< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, ?) (< 6,0,D>, ?) (< 6,0,E>, ?) (< 6,0,F>, 19) (< 6,0,G>, ?) (< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, 19) (< 8,0,D>, 20) (< 8,0,E>, E) (< 8,0,F>, F) (< 8,0,G>, G) (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, 19) (< 9,0,D>, 20) (< 9,0,E>, E) (< 9,0,F>, F) (< 9,0,G>, G) (<10,0,A>, ?) (<10,0,B>, ?) (<10,0,C>, 19) (<10,0,D>, 20 + D) (<10,0,E>, 0) (<10,0,F>, F) (<10,0,G>, G) (<11,0,A>, 19) (<11,0,B>, 20) (<11,0,C>, C) (<11,0,D>, D) (<11,0,E>, E) (<11,0,F>, F) (<11,0,G>, G) (<12,0,A>, 19) (<12,0,B>, 20) (<12,0,C>, C) (<12,0,D>, D) (<12,0,E>, E) (<12,0,F>, F) (<12,0,G>, G) (<13,0,A>, 19) (<13,0,B>, 20 + B) (<13,0,C>, 0) (<13,0,D>, D) (<13,0,E>, E) (<13,0,F>, F) (<13,0,G>, G) (<14,0,A>, 0) (<14,0,B>, B) (<14,0,C>, C) (<14,0,D>, D) (<14,0,E>, E) (<14,0,F>, F) (<14,0,G>, G) + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [11], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(f19) = 20 + -1*x2 The following rules are strictly oriented: [19 >= B] ==> f19(A,B,C,D,E,F,G) = 20 + -1*B > 19 + -1*B = f19(A,1 + B,C,D,E,F,G) The following rules are weakly oriented: We use the following global sizebounds: (< 0,0,A>, 19) (< 0,0,B>, 0) (< 0,0,C>, C) (< 0,0,D>, D) (< 0,0,E>, E) (< 0,0,F>, F) (< 0,0,G>, G) (< 1,0,A>, ?) (< 1,0,B>, ?) (< 1,0,C>, 19) (< 1,0,D>, 0) (< 1,0,E>, E) (< 1,0,F>, F) (< 1,0,G>, G) (< 2,0,A>, ?) (< 2,0,B>, ?) (< 2,0,C>, ?) (< 2,0,D>, ?) (< 2,0,E>, 19) (< 2,0,F>, 0) (< 2,0,G>, ?) (< 3,0,A>, ?) (< 3,0,B>, ?) (< 3,0,C>, ?) (< 3,0,D>, ?) (< 3,0,E>, ?) (< 3,0,F>, 19) (< 3,0,G>, 0) (< 4,0,A>, ?) (< 4,0,B>, ?) (< 4,0,C>, ?) (< 4,0,D>, ?) (< 4,0,E>, ?) (< 4,0,F>, 19) (< 4,0,G>, 20) (< 5,0,A>, ?) (< 5,0,B>, ?) (< 5,0,C>, ?) (< 5,0,D>, ?) (< 5,0,E>, ?) (< 5,0,F>, 19) (< 5,0,G>, 20) (< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, ?) (< 6,0,D>, ?) (< 6,0,E>, ?) (< 6,0,F>, 19) (< 6,0,G>, ?) (< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, 19) (< 8,0,D>, 20) (< 8,0,E>, E) (< 8,0,F>, F) (< 8,0,G>, G) (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, 19) (< 9,0,D>, 20) (< 9,0,E>, E) (< 9,0,F>, F) (< 9,0,G>, G) (<10,0,A>, ?) (<10,0,B>, ?) (<10,0,C>, 19) (<10,0,D>, 20 + D) (<10,0,E>, 0) (<10,0,F>, F) (<10,0,G>, G) (<11,0,A>, 19) (<11,0,B>, 20) (<11,0,C>, C) (<11,0,D>, D) (<11,0,E>, E) (<11,0,F>, F) (<11,0,G>, G) (<12,0,A>, 19) (<12,0,B>, 20) (<12,0,C>, C) (<12,0,D>, D) (<12,0,E>, E) (<12,0,F>, F) (<12,0,G>, G) (<13,0,A>, 19) (<13,0,B>, 20 + B) (<13,0,C>, 0) (<13,0,D>, D) (<13,0,E>, E) (<13,0,F>, F) (<13,0,G>, G) (<14,0,A>, 0) (<14,0,B>, B) (<14,0,C>, C) (<14,0,D>, D) (<14,0,E>, E) (<14,0,F>, F) (<14,0,G>, G) * Step 12: KnowledgePropagation WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. f16(A,B,C,D,E,F,G) -> f19(A,0,C,D,E,F,G) [19 >= A] (20,1) 1. f33(A,B,C,D,E,F,G) -> f36(A,B,C,0,E,F,G) [19 >= C] (20,1) 2. f52(A,B,C,D,E,F,G) -> f55(A,B,C,D,E,0,G) [19 >= E] (20,1) 3. f55(A,B,C,D,E,F,G) -> f59(A,B,C,D,E,F,0) [19 >= F] (?,1) 4. f59(A,B,C,D,E,F,G) -> f59(A,B,C,D,E,F,1 + G) [19 >= G] (?,1) 5. f59(A,B,C,D,E,F,G) -> f55(A,B,C,D,E,1 + F,G) [G >= 20] (?,1) 6. f55(A,B,C,D,E,F,G) -> f52(A,B,C,D,1 + E,F,G) [F >= 20] (?,1) 8. f36(A,B,C,D,E,F,G) -> f36(A,B,C,1 + D,E,F,G) [19 >= D] (?,1) 9. f36(A,B,C,D,E,F,G) -> f33(A,B,1 + C,D,E,F,G) [D >= 20] (?,1) 10. f33(A,B,C,D,E,F,G) -> f52(A,B,C,D,0,F,G) [C >= 20] (1,1) 11. f19(A,B,C,D,E,F,G) -> f19(A,1 + B,C,D,E,F,G) [19 >= B] (400,1) 12. f19(A,B,C,D,E,F,G) -> f16(1 + A,B,C,D,E,F,G) [B >= 20] (?,1) 13. f16(A,B,C,D,E,F,G) -> f33(A,B,0,D,E,F,G) [A >= 20] (1,1) 14. f0(A,B,C,D,E,F,G) -> f16(0,B,C,D,E,F,G) True (1,1) Signature: {(f0,7);(f16,7);(f19,7);(f33,7);(f36,7);(f52,7);(f55,7);(f59,7);(f73,7)} Flow Graph: [0->{11},1->{8},2->{3},3->{4},4->{4,5},5->{3,6},6->{2},8->{8,9},9->{1,10},10->{2},11->{11,12},12->{0,13} ,13->{1},14->{0}] Sizebounds: (< 0,0,A>, 19) (< 0,0,B>, 0) (< 0,0,C>, C) (< 0,0,D>, D) (< 0,0,E>, E) (< 0,0,F>, F) (< 0,0,G>, G) (< 1,0,A>, ?) (< 1,0,B>, ?) (< 1,0,C>, 19) (< 1,0,D>, 0) (< 1,0,E>, E) (< 1,0,F>, F) (< 1,0,G>, G) (< 2,0,A>, ?) (< 2,0,B>, ?) (< 2,0,C>, ?) (< 2,0,D>, ?) (< 2,0,E>, 19) (< 2,0,F>, 0) (< 2,0,G>, ?) (< 3,0,A>, ?) (< 3,0,B>, ?) (< 3,0,C>, ?) (< 3,0,D>, ?) (< 3,0,E>, ?) (< 3,0,F>, 19) (< 3,0,G>, 0) (< 4,0,A>, ?) (< 4,0,B>, ?) (< 4,0,C>, ?) (< 4,0,D>, ?) (< 4,0,E>, ?) (< 4,0,F>, 19) (< 4,0,G>, 20) (< 5,0,A>, ?) (< 5,0,B>, ?) (< 5,0,C>, ?) (< 5,0,D>, ?) (< 5,0,E>, ?) (< 5,0,F>, 19) (< 5,0,G>, 20) (< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, ?) (< 6,0,D>, ?) (< 6,0,E>, ?) (< 6,0,F>, 19) (< 6,0,G>, ?) (< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, 19) (< 8,0,D>, 20) (< 8,0,E>, E) (< 8,0,F>, F) (< 8,0,G>, G) (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, 19) (< 9,0,D>, 20) (< 9,0,E>, E) (< 9,0,F>, F) (< 9,0,G>, G) (<10,0,A>, ?) (<10,0,B>, ?) (<10,0,C>, 19) (<10,0,D>, 20 + D) (<10,0,E>, 0) (<10,0,F>, F) (<10,0,G>, G) (<11,0,A>, 19) (<11,0,B>, 20) (<11,0,C>, C) (<11,0,D>, D) (<11,0,E>, E) (<11,0,F>, F) (<11,0,G>, G) (<12,0,A>, 19) (<12,0,B>, 20) (<12,0,C>, C) (<12,0,D>, D) (<12,0,E>, E) (<12,0,F>, F) (<12,0,G>, G) (<13,0,A>, 19) (<13,0,B>, 20 + B) (<13,0,C>, 0) (<13,0,D>, D) (<13,0,E>, E) (<13,0,F>, F) (<13,0,G>, G) (<14,0,A>, 0) (<14,0,B>, B) (<14,0,C>, C) (<14,0,D>, D) (<14,0,E>, E) (<14,0,F>, F) (<14,0,G>, G) + Applied Processor: KnowledgePropagation + Details: We propagate bounds from predecessors. * Step 13: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. f16(A,B,C,D,E,F,G) -> f19(A,0,C,D,E,F,G) [19 >= A] (20,1) 1. f33(A,B,C,D,E,F,G) -> f36(A,B,C,0,E,F,G) [19 >= C] (20,1) 2. f52(A,B,C,D,E,F,G) -> f55(A,B,C,D,E,0,G) [19 >= E] (20,1) 3. f55(A,B,C,D,E,F,G) -> f59(A,B,C,D,E,F,0) [19 >= F] (?,1) 4. f59(A,B,C,D,E,F,G) -> f59(A,B,C,D,E,F,1 + G) [19 >= G] (?,1) 5. f59(A,B,C,D,E,F,G) -> f55(A,B,C,D,E,1 + F,G) [G >= 20] (?,1) 6. f55(A,B,C,D,E,F,G) -> f52(A,B,C,D,1 + E,F,G) [F >= 20] (?,1) 8. f36(A,B,C,D,E,F,G) -> f36(A,B,C,1 + D,E,F,G) [19 >= D] (?,1) 9. f36(A,B,C,D,E,F,G) -> f33(A,B,1 + C,D,E,F,G) [D >= 20] (?,1) 10. f33(A,B,C,D,E,F,G) -> f52(A,B,C,D,0,F,G) [C >= 20] (1,1) 11. f19(A,B,C,D,E,F,G) -> f19(A,1 + B,C,D,E,F,G) [19 >= B] (400,1) 12. f19(A,B,C,D,E,F,G) -> f16(1 + A,B,C,D,E,F,G) [B >= 20] (400,1) 13. f16(A,B,C,D,E,F,G) -> f33(A,B,0,D,E,F,G) [A >= 20] (1,1) 14. f0(A,B,C,D,E,F,G) -> f16(0,B,C,D,E,F,G) True (1,1) Signature: {(f0,7);(f16,7);(f19,7);(f33,7);(f36,7);(f52,7);(f55,7);(f59,7);(f73,7)} Flow Graph: [0->{11},1->{8},2->{3},3->{4},4->{4,5},5->{3,6},6->{2},8->{8,9},9->{1,10},10->{2},11->{11,12},12->{0,13} ,13->{1},14->{0}] Sizebounds: (< 0,0,A>, 19) (< 0,0,B>, 0) (< 0,0,C>, C) (< 0,0,D>, D) (< 0,0,E>, E) (< 0,0,F>, F) (< 0,0,G>, G) (< 1,0,A>, ?) (< 1,0,B>, ?) (< 1,0,C>, 19) (< 1,0,D>, 0) (< 1,0,E>, E) (< 1,0,F>, F) (< 1,0,G>, G) (< 2,0,A>, ?) (< 2,0,B>, ?) (< 2,0,C>, ?) (< 2,0,D>, ?) (< 2,0,E>, 19) (< 2,0,F>, 0) (< 2,0,G>, ?) (< 3,0,A>, ?) (< 3,0,B>, ?) (< 3,0,C>, ?) (< 3,0,D>, ?) (< 3,0,E>, ?) (< 3,0,F>, 19) (< 3,0,G>, 0) (< 4,0,A>, ?) (< 4,0,B>, ?) (< 4,0,C>, ?) (< 4,0,D>, ?) (< 4,0,E>, ?) (< 4,0,F>, 19) (< 4,0,G>, 20) (< 5,0,A>, ?) (< 5,0,B>, ?) (< 5,0,C>, ?) (< 5,0,D>, ?) (< 5,0,E>, ?) (< 5,0,F>, 19) (< 5,0,G>, 20) (< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, ?) (< 6,0,D>, ?) (< 6,0,E>, ?) (< 6,0,F>, 19) (< 6,0,G>, ?) (< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, 19) (< 8,0,D>, 20) (< 8,0,E>, E) (< 8,0,F>, F) (< 8,0,G>, G) (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, 19) (< 9,0,D>, 20) (< 9,0,E>, E) (< 9,0,F>, F) (< 9,0,G>, G) (<10,0,A>, ?) (<10,0,B>, ?) (<10,0,C>, 19) (<10,0,D>, 20 + D) (<10,0,E>, 0) (<10,0,F>, F) (<10,0,G>, G) (<11,0,A>, 19) (<11,0,B>, 20) (<11,0,C>, C) (<11,0,D>, D) (<11,0,E>, E) (<11,0,F>, F) (<11,0,G>, G) (<12,0,A>, 19) (<12,0,B>, 20) (<12,0,C>, C) (<12,0,D>, D) (<12,0,E>, E) (<12,0,F>, F) (<12,0,G>, G) (<13,0,A>, 19) (<13,0,B>, 20 + B) (<13,0,C>, 0) (<13,0,D>, D) (<13,0,E>, E) (<13,0,F>, F) (<13,0,G>, G) (<14,0,A>, 0) (<14,0,B>, B) (<14,0,C>, C) (<14,0,D>, D) (<14,0,E>, E) (<14,0,F>, F) (<14,0,G>, G) + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [8], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(f36) = 20 + -1*x4 The following rules are strictly oriented: [19 >= D] ==> f36(A,B,C,D,E,F,G) = 20 + -1*D > 19 + -1*D = f36(A,B,C,1 + D,E,F,G) The following rules are weakly oriented: We use the following global sizebounds: (< 0,0,A>, 19) (< 0,0,B>, 0) (< 0,0,C>, C) (< 0,0,D>, D) (< 0,0,E>, E) (< 0,0,F>, F) (< 0,0,G>, G) (< 1,0,A>, ?) (< 1,0,B>, ?) (< 1,0,C>, 19) (< 1,0,D>, 0) (< 1,0,E>, E) (< 1,0,F>, F) (< 1,0,G>, G) (< 2,0,A>, ?) (< 2,0,B>, ?) (< 2,0,C>, ?) (< 2,0,D>, ?) (< 2,0,E>, 19) (< 2,0,F>, 0) (< 2,0,G>, ?) (< 3,0,A>, ?) (< 3,0,B>, ?) (< 3,0,C>, ?) (< 3,0,D>, ?) (< 3,0,E>, ?) (< 3,0,F>, 19) (< 3,0,G>, 0) (< 4,0,A>, ?) (< 4,0,B>, ?) (< 4,0,C>, ?) (< 4,0,D>, ?) (< 4,0,E>, ?) (< 4,0,F>, 19) (< 4,0,G>, 20) (< 5,0,A>, ?) (< 5,0,B>, ?) (< 5,0,C>, ?) (< 5,0,D>, ?) (< 5,0,E>, ?) (< 5,0,F>, 19) (< 5,0,G>, 20) (< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, ?) (< 6,0,D>, ?) (< 6,0,E>, ?) (< 6,0,F>, 19) (< 6,0,G>, ?) (< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, 19) (< 8,0,D>, 20) (< 8,0,E>, E) (< 8,0,F>, F) (< 8,0,G>, G) (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, 19) (< 9,0,D>, 20) (< 9,0,E>, E) (< 9,0,F>, F) (< 9,0,G>, G) (<10,0,A>, ?) (<10,0,B>, ?) (<10,0,C>, 19) (<10,0,D>, 20 + D) (<10,0,E>, 0) (<10,0,F>, F) (<10,0,G>, G) (<11,0,A>, 19) (<11,0,B>, 20) (<11,0,C>, C) (<11,0,D>, D) (<11,0,E>, E) (<11,0,F>, F) (<11,0,G>, G) (<12,0,A>, 19) (<12,0,B>, 20) (<12,0,C>, C) (<12,0,D>, D) (<12,0,E>, E) (<12,0,F>, F) (<12,0,G>, G) (<13,0,A>, 19) (<13,0,B>, 20 + B) (<13,0,C>, 0) (<13,0,D>, D) (<13,0,E>, E) (<13,0,F>, F) (<13,0,G>, G) (<14,0,A>, 0) (<14,0,B>, B) (<14,0,C>, C) (<14,0,D>, D) (<14,0,E>, E) (<14,0,F>, F) (<14,0,G>, G) * Step 14: KnowledgePropagation WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. f16(A,B,C,D,E,F,G) -> f19(A,0,C,D,E,F,G) [19 >= A] (20,1) 1. f33(A,B,C,D,E,F,G) -> f36(A,B,C,0,E,F,G) [19 >= C] (20,1) 2. f52(A,B,C,D,E,F,G) -> f55(A,B,C,D,E,0,G) [19 >= E] (20,1) 3. f55(A,B,C,D,E,F,G) -> f59(A,B,C,D,E,F,0) [19 >= F] (?,1) 4. f59(A,B,C,D,E,F,G) -> f59(A,B,C,D,E,F,1 + G) [19 >= G] (?,1) 5. f59(A,B,C,D,E,F,G) -> f55(A,B,C,D,E,1 + F,G) [G >= 20] (?,1) 6. f55(A,B,C,D,E,F,G) -> f52(A,B,C,D,1 + E,F,G) [F >= 20] (?,1) 8. f36(A,B,C,D,E,F,G) -> f36(A,B,C,1 + D,E,F,G) [19 >= D] (400,1) 9. f36(A,B,C,D,E,F,G) -> f33(A,B,1 + C,D,E,F,G) [D >= 20] (?,1) 10. f33(A,B,C,D,E,F,G) -> f52(A,B,C,D,0,F,G) [C >= 20] (1,1) 11. f19(A,B,C,D,E,F,G) -> f19(A,1 + B,C,D,E,F,G) [19 >= B] (400,1) 12. f19(A,B,C,D,E,F,G) -> f16(1 + A,B,C,D,E,F,G) [B >= 20] (400,1) 13. f16(A,B,C,D,E,F,G) -> f33(A,B,0,D,E,F,G) [A >= 20] (1,1) 14. f0(A,B,C,D,E,F,G) -> f16(0,B,C,D,E,F,G) True (1,1) Signature: {(f0,7);(f16,7);(f19,7);(f33,7);(f36,7);(f52,7);(f55,7);(f59,7);(f73,7)} Flow Graph: [0->{11},1->{8},2->{3},3->{4},4->{4,5},5->{3,6},6->{2},8->{8,9},9->{1,10},10->{2},11->{11,12},12->{0,13} ,13->{1},14->{0}] Sizebounds: (< 0,0,A>, 19) (< 0,0,B>, 0) (< 0,0,C>, C) (< 0,0,D>, D) (< 0,0,E>, E) (< 0,0,F>, F) (< 0,0,G>, G) (< 1,0,A>, ?) (< 1,0,B>, ?) (< 1,0,C>, 19) (< 1,0,D>, 0) (< 1,0,E>, E) (< 1,0,F>, F) (< 1,0,G>, G) (< 2,0,A>, ?) (< 2,0,B>, ?) (< 2,0,C>, ?) (< 2,0,D>, ?) (< 2,0,E>, 19) (< 2,0,F>, 0) (< 2,0,G>, ?) (< 3,0,A>, ?) (< 3,0,B>, ?) (< 3,0,C>, ?) (< 3,0,D>, ?) (< 3,0,E>, ?) (< 3,0,F>, 19) (< 3,0,G>, 0) (< 4,0,A>, ?) (< 4,0,B>, ?) (< 4,0,C>, ?) (< 4,0,D>, ?) (< 4,0,E>, ?) (< 4,0,F>, 19) (< 4,0,G>, 20) (< 5,0,A>, ?) (< 5,0,B>, ?) (< 5,0,C>, ?) (< 5,0,D>, ?) (< 5,0,E>, ?) (< 5,0,F>, 19) (< 5,0,G>, 20) (< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, ?) (< 6,0,D>, ?) (< 6,0,E>, ?) (< 6,0,F>, 19) (< 6,0,G>, ?) (< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, 19) (< 8,0,D>, 20) (< 8,0,E>, E) (< 8,0,F>, F) (< 8,0,G>, G) (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, 19) (< 9,0,D>, 20) (< 9,0,E>, E) (< 9,0,F>, F) (< 9,0,G>, G) (<10,0,A>, ?) (<10,0,B>, ?) (<10,0,C>, 19) (<10,0,D>, 20 + D) (<10,0,E>, 0) (<10,0,F>, F) (<10,0,G>, G) (<11,0,A>, 19) (<11,0,B>, 20) (<11,0,C>, C) (<11,0,D>, D) (<11,0,E>, E) (<11,0,F>, F) (<11,0,G>, G) (<12,0,A>, 19) (<12,0,B>, 20) (<12,0,C>, C) (<12,0,D>, D) (<12,0,E>, E) (<12,0,F>, F) (<12,0,G>, G) (<13,0,A>, 19) (<13,0,B>, 20 + B) (<13,0,C>, 0) (<13,0,D>, D) (<13,0,E>, E) (<13,0,F>, F) (<13,0,G>, G) (<14,0,A>, 0) (<14,0,B>, B) (<14,0,C>, C) (<14,0,D>, D) (<14,0,E>, E) (<14,0,F>, F) (<14,0,G>, G) + Applied Processor: KnowledgePropagation + Details: We propagate bounds from predecessors. * Step 15: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. f16(A,B,C,D,E,F,G) -> f19(A,0,C,D,E,F,G) [19 >= A] (20,1) 1. f33(A,B,C,D,E,F,G) -> f36(A,B,C,0,E,F,G) [19 >= C] (20,1) 2. f52(A,B,C,D,E,F,G) -> f55(A,B,C,D,E,0,G) [19 >= E] (20,1) 3. f55(A,B,C,D,E,F,G) -> f59(A,B,C,D,E,F,0) [19 >= F] (?,1) 4. f59(A,B,C,D,E,F,G) -> f59(A,B,C,D,E,F,1 + G) [19 >= G] (?,1) 5. f59(A,B,C,D,E,F,G) -> f55(A,B,C,D,E,1 + F,G) [G >= 20] (?,1) 6. f55(A,B,C,D,E,F,G) -> f52(A,B,C,D,1 + E,F,G) [F >= 20] (?,1) 8. f36(A,B,C,D,E,F,G) -> f36(A,B,C,1 + D,E,F,G) [19 >= D] (400,1) 9. f36(A,B,C,D,E,F,G) -> f33(A,B,1 + C,D,E,F,G) [D >= 20] (400,1) 10. f33(A,B,C,D,E,F,G) -> f52(A,B,C,D,0,F,G) [C >= 20] (1,1) 11. f19(A,B,C,D,E,F,G) -> f19(A,1 + B,C,D,E,F,G) [19 >= B] (400,1) 12. f19(A,B,C,D,E,F,G) -> f16(1 + A,B,C,D,E,F,G) [B >= 20] (400,1) 13. f16(A,B,C,D,E,F,G) -> f33(A,B,0,D,E,F,G) [A >= 20] (1,1) 14. f0(A,B,C,D,E,F,G) -> f16(0,B,C,D,E,F,G) True (1,1) Signature: {(f0,7);(f16,7);(f19,7);(f33,7);(f36,7);(f52,7);(f55,7);(f59,7);(f73,7)} Flow Graph: [0->{11},1->{8},2->{3},3->{4},4->{4,5},5->{3,6},6->{2},8->{8,9},9->{1,10},10->{2},11->{11,12},12->{0,13} ,13->{1},14->{0}] Sizebounds: (< 0,0,A>, 19) (< 0,0,B>, 0) (< 0,0,C>, C) (< 0,0,D>, D) (< 0,0,E>, E) (< 0,0,F>, F) (< 0,0,G>, G) (< 1,0,A>, ?) (< 1,0,B>, ?) (< 1,0,C>, 19) (< 1,0,D>, 0) (< 1,0,E>, E) (< 1,0,F>, F) (< 1,0,G>, G) (< 2,0,A>, ?) (< 2,0,B>, ?) (< 2,0,C>, ?) (< 2,0,D>, ?) (< 2,0,E>, 19) (< 2,0,F>, 0) (< 2,0,G>, ?) (< 3,0,A>, ?) (< 3,0,B>, ?) (< 3,0,C>, ?) (< 3,0,D>, ?) (< 3,0,E>, ?) (< 3,0,F>, 19) (< 3,0,G>, 0) (< 4,0,A>, ?) (< 4,0,B>, ?) (< 4,0,C>, ?) (< 4,0,D>, ?) (< 4,0,E>, ?) (< 4,0,F>, 19) (< 4,0,G>, 20) (< 5,0,A>, ?) (< 5,0,B>, ?) (< 5,0,C>, ?) (< 5,0,D>, ?) (< 5,0,E>, ?) (< 5,0,F>, 19) (< 5,0,G>, 20) (< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, ?) (< 6,0,D>, ?) (< 6,0,E>, ?) (< 6,0,F>, 19) (< 6,0,G>, ?) (< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, 19) (< 8,0,D>, 20) (< 8,0,E>, E) (< 8,0,F>, F) (< 8,0,G>, G) (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, 19) (< 9,0,D>, 20) (< 9,0,E>, E) (< 9,0,F>, F) (< 9,0,G>, G) (<10,0,A>, ?) (<10,0,B>, ?) (<10,0,C>, 19) (<10,0,D>, 20 + D) (<10,0,E>, 0) (<10,0,F>, F) (<10,0,G>, G) (<11,0,A>, 19) (<11,0,B>, 20) (<11,0,C>, C) (<11,0,D>, D) (<11,0,E>, E) (<11,0,F>, F) (<11,0,G>, G) (<12,0,A>, 19) (<12,0,B>, 20) (<12,0,C>, C) (<12,0,D>, D) (<12,0,E>, E) (<12,0,F>, F) (<12,0,G>, G) (<13,0,A>, 19) (<13,0,B>, 20 + B) (<13,0,C>, 0) (<13,0,D>, D) (<13,0,E>, E) (<13,0,F>, F) (<13,0,G>, G) (<14,0,A>, 0) (<14,0,B>, B) (<14,0,C>, C) (<14,0,D>, D) (<14,0,E>, E) (<14,0,F>, F) (<14,0,G>, G) + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [5,4,3], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(f55) = 20 + -1*x6 p(f59) = 19 + -1*x6 The following rules are strictly oriented: [19 >= F] ==> f55(A,B,C,D,E,F,G) = 20 + -1*F > 19 + -1*F = f59(A,B,C,D,E,F,0) The following rules are weakly oriented: [19 >= G] ==> f59(A,B,C,D,E,F,G) = 19 + -1*F >= 19 + -1*F = f59(A,B,C,D,E,F,1 + G) [G >= 20] ==> f59(A,B,C,D,E,F,G) = 19 + -1*F >= 19 + -1*F = f55(A,B,C,D,E,1 + F,G) We use the following global sizebounds: (< 0,0,A>, 19) (< 0,0,B>, 0) (< 0,0,C>, C) (< 0,0,D>, D) (< 0,0,E>, E) (< 0,0,F>, F) (< 0,0,G>, G) (< 1,0,A>, ?) (< 1,0,B>, ?) (< 1,0,C>, 19) (< 1,0,D>, 0) (< 1,0,E>, E) (< 1,0,F>, F) (< 1,0,G>, G) (< 2,0,A>, ?) (< 2,0,B>, ?) (< 2,0,C>, ?) (< 2,0,D>, ?) (< 2,0,E>, 19) (< 2,0,F>, 0) (< 2,0,G>, ?) (< 3,0,A>, ?) (< 3,0,B>, ?) (< 3,0,C>, ?) (< 3,0,D>, ?) (< 3,0,E>, ?) (< 3,0,F>, 19) (< 3,0,G>, 0) (< 4,0,A>, ?) (< 4,0,B>, ?) (< 4,0,C>, ?) (< 4,0,D>, ?) (< 4,0,E>, ?) (< 4,0,F>, 19) (< 4,0,G>, 20) (< 5,0,A>, ?) (< 5,0,B>, ?) (< 5,0,C>, ?) (< 5,0,D>, ?) (< 5,0,E>, ?) (< 5,0,F>, 19) (< 5,0,G>, 20) (< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, ?) (< 6,0,D>, ?) (< 6,0,E>, ?) (< 6,0,F>, 19) (< 6,0,G>, ?) (< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, 19) (< 8,0,D>, 20) (< 8,0,E>, E) (< 8,0,F>, F) (< 8,0,G>, G) (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, 19) (< 9,0,D>, 20) (< 9,0,E>, E) (< 9,0,F>, F) (< 9,0,G>, G) (<10,0,A>, ?) (<10,0,B>, ?) (<10,0,C>, 19) (<10,0,D>, 20 + D) (<10,0,E>, 0) (<10,0,F>, F) (<10,0,G>, G) (<11,0,A>, 19) (<11,0,B>, 20) (<11,0,C>, C) (<11,0,D>, D) (<11,0,E>, E) (<11,0,F>, F) (<11,0,G>, G) (<12,0,A>, 19) (<12,0,B>, 20) (<12,0,C>, C) (<12,0,D>, D) (<12,0,E>, E) (<12,0,F>, F) (<12,0,G>, G) (<13,0,A>, 19) (<13,0,B>, 20 + B) (<13,0,C>, 0) (<13,0,D>, D) (<13,0,E>, E) (<13,0,F>, F) (<13,0,G>, G) (<14,0,A>, 0) (<14,0,B>, B) (<14,0,C>, C) (<14,0,D>, D) (<14,0,E>, E) (<14,0,F>, F) (<14,0,G>, G) * Step 16: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. f16(A,B,C,D,E,F,G) -> f19(A,0,C,D,E,F,G) [19 >= A] (20,1) 1. f33(A,B,C,D,E,F,G) -> f36(A,B,C,0,E,F,G) [19 >= C] (20,1) 2. f52(A,B,C,D,E,F,G) -> f55(A,B,C,D,E,0,G) [19 >= E] (20,1) 3. f55(A,B,C,D,E,F,G) -> f59(A,B,C,D,E,F,0) [19 >= F] (400,1) 4. f59(A,B,C,D,E,F,G) -> f59(A,B,C,D,E,F,1 + G) [19 >= G] (?,1) 5. f59(A,B,C,D,E,F,G) -> f55(A,B,C,D,E,1 + F,G) [G >= 20] (?,1) 6. f55(A,B,C,D,E,F,G) -> f52(A,B,C,D,1 + E,F,G) [F >= 20] (?,1) 8. f36(A,B,C,D,E,F,G) -> f36(A,B,C,1 + D,E,F,G) [19 >= D] (400,1) 9. f36(A,B,C,D,E,F,G) -> f33(A,B,1 + C,D,E,F,G) [D >= 20] (400,1) 10. f33(A,B,C,D,E,F,G) -> f52(A,B,C,D,0,F,G) [C >= 20] (1,1) 11. f19(A,B,C,D,E,F,G) -> f19(A,1 + B,C,D,E,F,G) [19 >= B] (400,1) 12. f19(A,B,C,D,E,F,G) -> f16(1 + A,B,C,D,E,F,G) [B >= 20] (400,1) 13. f16(A,B,C,D,E,F,G) -> f33(A,B,0,D,E,F,G) [A >= 20] (1,1) 14. f0(A,B,C,D,E,F,G) -> f16(0,B,C,D,E,F,G) True (1,1) Signature: {(f0,7);(f16,7);(f19,7);(f33,7);(f36,7);(f52,7);(f55,7);(f59,7);(f73,7)} Flow Graph: [0->{11},1->{8},2->{3},3->{4},4->{4,5},5->{3,6},6->{2},8->{8,9},9->{1,10},10->{2},11->{11,12},12->{0,13} ,13->{1},14->{0}] Sizebounds: (< 0,0,A>, 19) (< 0,0,B>, 0) (< 0,0,C>, C) (< 0,0,D>, D) (< 0,0,E>, E) (< 0,0,F>, F) (< 0,0,G>, G) (< 1,0,A>, ?) (< 1,0,B>, ?) (< 1,0,C>, 19) (< 1,0,D>, 0) (< 1,0,E>, E) (< 1,0,F>, F) (< 1,0,G>, G) (< 2,0,A>, ?) (< 2,0,B>, ?) (< 2,0,C>, ?) (< 2,0,D>, ?) (< 2,0,E>, 19) (< 2,0,F>, 0) (< 2,0,G>, ?) (< 3,0,A>, ?) (< 3,0,B>, ?) (< 3,0,C>, ?) (< 3,0,D>, ?) (< 3,0,E>, ?) (< 3,0,F>, 19) (< 3,0,G>, 0) (< 4,0,A>, ?) (< 4,0,B>, ?) (< 4,0,C>, ?) (< 4,0,D>, ?) (< 4,0,E>, ?) (< 4,0,F>, 19) (< 4,0,G>, 20) (< 5,0,A>, ?) (< 5,0,B>, ?) (< 5,0,C>, ?) (< 5,0,D>, ?) (< 5,0,E>, ?) (< 5,0,F>, 19) (< 5,0,G>, 20) (< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, ?) (< 6,0,D>, ?) (< 6,0,E>, ?) (< 6,0,F>, 19) (< 6,0,G>, ?) (< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, 19) (< 8,0,D>, 20) (< 8,0,E>, E) (< 8,0,F>, F) (< 8,0,G>, G) (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, 19) (< 9,0,D>, 20) (< 9,0,E>, E) (< 9,0,F>, F) (< 9,0,G>, G) (<10,0,A>, ?) (<10,0,B>, ?) (<10,0,C>, 19) (<10,0,D>, 20 + D) (<10,0,E>, 0) (<10,0,F>, F) (<10,0,G>, G) (<11,0,A>, 19) (<11,0,B>, 20) (<11,0,C>, C) (<11,0,D>, D) (<11,0,E>, E) (<11,0,F>, F) (<11,0,G>, G) (<12,0,A>, 19) (<12,0,B>, 20) (<12,0,C>, C) (<12,0,D>, D) (<12,0,E>, E) (<12,0,F>, F) (<12,0,G>, G) (<13,0,A>, 19) (<13,0,B>, 20 + B) (<13,0,C>, 0) (<13,0,D>, D) (<13,0,E>, E) (<13,0,F>, F) (<13,0,G>, G) (<14,0,A>, 0) (<14,0,B>, B) (<14,0,C>, C) (<14,0,D>, D) (<14,0,E>, E) (<14,0,F>, F) (<14,0,G>, G) + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [6,5,4,3], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(f52) = 0 p(f55) = 1 p(f59) = 1 The following rules are strictly oriented: [F >= 20] ==> f55(A,B,C,D,E,F,G) = 1 > 0 = f52(A,B,C,D,1 + E,F,G) The following rules are weakly oriented: [19 >= F] ==> f55(A,B,C,D,E,F,G) = 1 >= 1 = f59(A,B,C,D,E,F,0) [19 >= G] ==> f59(A,B,C,D,E,F,G) = 1 >= 1 = f59(A,B,C,D,E,F,1 + G) [G >= 20] ==> f59(A,B,C,D,E,F,G) = 1 >= 1 = f55(A,B,C,D,E,1 + F,G) We use the following global sizebounds: (< 0,0,A>, 19) (< 0,0,B>, 0) (< 0,0,C>, C) (< 0,0,D>, D) (< 0,0,E>, E) (< 0,0,F>, F) (< 0,0,G>, G) (< 1,0,A>, ?) (< 1,0,B>, ?) (< 1,0,C>, 19) (< 1,0,D>, 0) (< 1,0,E>, E) (< 1,0,F>, F) (< 1,0,G>, G) (< 2,0,A>, ?) (< 2,0,B>, ?) (< 2,0,C>, ?) (< 2,0,D>, ?) (< 2,0,E>, 19) (< 2,0,F>, 0) (< 2,0,G>, ?) (< 3,0,A>, ?) (< 3,0,B>, ?) (< 3,0,C>, ?) (< 3,0,D>, ?) (< 3,0,E>, ?) (< 3,0,F>, 19) (< 3,0,G>, 0) (< 4,0,A>, ?) (< 4,0,B>, ?) (< 4,0,C>, ?) (< 4,0,D>, ?) (< 4,0,E>, ?) (< 4,0,F>, 19) (< 4,0,G>, 20) (< 5,0,A>, ?) (< 5,0,B>, ?) (< 5,0,C>, ?) (< 5,0,D>, ?) (< 5,0,E>, ?) (< 5,0,F>, 19) (< 5,0,G>, 20) (< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, ?) (< 6,0,D>, ?) (< 6,0,E>, ?) (< 6,0,F>, 19) (< 6,0,G>, ?) (< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, 19) (< 8,0,D>, 20) (< 8,0,E>, E) (< 8,0,F>, F) (< 8,0,G>, G) (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, 19) (< 9,0,D>, 20) (< 9,0,E>, E) (< 9,0,F>, F) (< 9,0,G>, G) (<10,0,A>, ?) (<10,0,B>, ?) (<10,0,C>, 19) (<10,0,D>, 20 + D) (<10,0,E>, 0) (<10,0,F>, F) (<10,0,G>, G) (<11,0,A>, 19) (<11,0,B>, 20) (<11,0,C>, C) (<11,0,D>, D) (<11,0,E>, E) (<11,0,F>, F) (<11,0,G>, G) (<12,0,A>, 19) (<12,0,B>, 20) (<12,0,C>, C) (<12,0,D>, D) (<12,0,E>, E) (<12,0,F>, F) (<12,0,G>, G) (<13,0,A>, 19) (<13,0,B>, 20 + B) (<13,0,C>, 0) (<13,0,D>, D) (<13,0,E>, E) (<13,0,F>, F) (<13,0,G>, G) (<14,0,A>, 0) (<14,0,B>, B) (<14,0,C>, C) (<14,0,D>, D) (<14,0,E>, E) (<14,0,F>, F) (<14,0,G>, G) * Step 17: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. f16(A,B,C,D,E,F,G) -> f19(A,0,C,D,E,F,G) [19 >= A] (20,1) 1. f33(A,B,C,D,E,F,G) -> f36(A,B,C,0,E,F,G) [19 >= C] (20,1) 2. f52(A,B,C,D,E,F,G) -> f55(A,B,C,D,E,0,G) [19 >= E] (20,1) 3. f55(A,B,C,D,E,F,G) -> f59(A,B,C,D,E,F,0) [19 >= F] (400,1) 4. f59(A,B,C,D,E,F,G) -> f59(A,B,C,D,E,F,1 + G) [19 >= G] (?,1) 5. f59(A,B,C,D,E,F,G) -> f55(A,B,C,D,E,1 + F,G) [G >= 20] (?,1) 6. f55(A,B,C,D,E,F,G) -> f52(A,B,C,D,1 + E,F,G) [F >= 20] (20,1) 8. f36(A,B,C,D,E,F,G) -> f36(A,B,C,1 + D,E,F,G) [19 >= D] (400,1) 9. f36(A,B,C,D,E,F,G) -> f33(A,B,1 + C,D,E,F,G) [D >= 20] (400,1) 10. f33(A,B,C,D,E,F,G) -> f52(A,B,C,D,0,F,G) [C >= 20] (1,1) 11. f19(A,B,C,D,E,F,G) -> f19(A,1 + B,C,D,E,F,G) [19 >= B] (400,1) 12. f19(A,B,C,D,E,F,G) -> f16(1 + A,B,C,D,E,F,G) [B >= 20] (400,1) 13. f16(A,B,C,D,E,F,G) -> f33(A,B,0,D,E,F,G) [A >= 20] (1,1) 14. f0(A,B,C,D,E,F,G) -> f16(0,B,C,D,E,F,G) True (1,1) Signature: {(f0,7);(f16,7);(f19,7);(f33,7);(f36,7);(f52,7);(f55,7);(f59,7);(f73,7)} Flow Graph: [0->{11},1->{8},2->{3},3->{4},4->{4,5},5->{3,6},6->{2},8->{8,9},9->{1,10},10->{2},11->{11,12},12->{0,13} ,13->{1},14->{0}] Sizebounds: (< 0,0,A>, 19) (< 0,0,B>, 0) (< 0,0,C>, C) (< 0,0,D>, D) (< 0,0,E>, E) (< 0,0,F>, F) (< 0,0,G>, G) (< 1,0,A>, ?) (< 1,0,B>, ?) (< 1,0,C>, 19) (< 1,0,D>, 0) (< 1,0,E>, E) (< 1,0,F>, F) (< 1,0,G>, G) (< 2,0,A>, ?) (< 2,0,B>, ?) (< 2,0,C>, ?) (< 2,0,D>, ?) (< 2,0,E>, 19) (< 2,0,F>, 0) (< 2,0,G>, ?) (< 3,0,A>, ?) (< 3,0,B>, ?) (< 3,0,C>, ?) (< 3,0,D>, ?) (< 3,0,E>, ?) (< 3,0,F>, 19) (< 3,0,G>, 0) (< 4,0,A>, ?) (< 4,0,B>, ?) (< 4,0,C>, ?) (< 4,0,D>, ?) (< 4,0,E>, ?) (< 4,0,F>, 19) (< 4,0,G>, 20) (< 5,0,A>, ?) (< 5,0,B>, ?) (< 5,0,C>, ?) (< 5,0,D>, ?) (< 5,0,E>, ?) (< 5,0,F>, 19) (< 5,0,G>, 20) (< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, ?) (< 6,0,D>, ?) (< 6,0,E>, ?) (< 6,0,F>, 19) (< 6,0,G>, ?) (< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, 19) (< 8,0,D>, 20) (< 8,0,E>, E) (< 8,0,F>, F) (< 8,0,G>, G) (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, 19) (< 9,0,D>, 20) (< 9,0,E>, E) (< 9,0,F>, F) (< 9,0,G>, G) (<10,0,A>, ?) (<10,0,B>, ?) (<10,0,C>, 19) (<10,0,D>, 20 + D) (<10,0,E>, 0) (<10,0,F>, F) (<10,0,G>, G) (<11,0,A>, 19) (<11,0,B>, 20) (<11,0,C>, C) (<11,0,D>, D) (<11,0,E>, E) (<11,0,F>, F) (<11,0,G>, G) (<12,0,A>, 19) (<12,0,B>, 20) (<12,0,C>, C) (<12,0,D>, D) (<12,0,E>, E) (<12,0,F>, F) (<12,0,G>, G) (<13,0,A>, 19) (<13,0,B>, 20 + B) (<13,0,C>, 0) (<13,0,D>, D) (<13,0,E>, E) (<13,0,F>, F) (<13,0,G>, G) (<14,0,A>, 0) (<14,0,B>, B) (<14,0,C>, C) (<14,0,D>, D) (<14,0,E>, E) (<14,0,F>, F) (<14,0,G>, G) + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [2,6,5,4], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(f52) = 0 p(f55) = 0 p(f59) = 1 The following rules are strictly oriented: [G >= 20] ==> f59(A,B,C,D,E,F,G) = 1 > 0 = f55(A,B,C,D,E,1 + F,G) The following rules are weakly oriented: [19 >= E] ==> f52(A,B,C,D,E,F,G) = 0 >= 0 = f55(A,B,C,D,E,0,G) [19 >= G] ==> f59(A,B,C,D,E,F,G) = 1 >= 1 = f59(A,B,C,D,E,F,1 + G) [F >= 20] ==> f55(A,B,C,D,E,F,G) = 0 >= 0 = f52(A,B,C,D,1 + E,F,G) We use the following global sizebounds: (< 0,0,A>, 19) (< 0,0,B>, 0) (< 0,0,C>, C) (< 0,0,D>, D) (< 0,0,E>, E) (< 0,0,F>, F) (< 0,0,G>, G) (< 1,0,A>, ?) (< 1,0,B>, ?) (< 1,0,C>, 19) (< 1,0,D>, 0) (< 1,0,E>, E) (< 1,0,F>, F) (< 1,0,G>, G) (< 2,0,A>, ?) (< 2,0,B>, ?) (< 2,0,C>, ?) (< 2,0,D>, ?) (< 2,0,E>, 19) (< 2,0,F>, 0) (< 2,0,G>, ?) (< 3,0,A>, ?) (< 3,0,B>, ?) (< 3,0,C>, ?) (< 3,0,D>, ?) (< 3,0,E>, ?) (< 3,0,F>, 19) (< 3,0,G>, 0) (< 4,0,A>, ?) (< 4,0,B>, ?) (< 4,0,C>, ?) (< 4,0,D>, ?) (< 4,0,E>, ?) (< 4,0,F>, 19) (< 4,0,G>, 20) (< 5,0,A>, ?) (< 5,0,B>, ?) (< 5,0,C>, ?) (< 5,0,D>, ?) (< 5,0,E>, ?) (< 5,0,F>, 19) (< 5,0,G>, 20) (< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, ?) (< 6,0,D>, ?) (< 6,0,E>, ?) (< 6,0,F>, 19) (< 6,0,G>, ?) (< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, 19) (< 8,0,D>, 20) (< 8,0,E>, E) (< 8,0,F>, F) (< 8,0,G>, G) (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, 19) (< 9,0,D>, 20) (< 9,0,E>, E) (< 9,0,F>, F) (< 9,0,G>, G) (<10,0,A>, ?) (<10,0,B>, ?) (<10,0,C>, 19) (<10,0,D>, 20 + D) (<10,0,E>, 0) (<10,0,F>, F) (<10,0,G>, G) (<11,0,A>, 19) (<11,0,B>, 20) (<11,0,C>, C) (<11,0,D>, D) (<11,0,E>, E) (<11,0,F>, F) (<11,0,G>, G) (<12,0,A>, 19) (<12,0,B>, 20) (<12,0,C>, C) (<12,0,D>, D) (<12,0,E>, E) (<12,0,F>, F) (<12,0,G>, G) (<13,0,A>, 19) (<13,0,B>, 20 + B) (<13,0,C>, 0) (<13,0,D>, D) (<13,0,E>, E) (<13,0,F>, F) (<13,0,G>, G) (<14,0,A>, 0) (<14,0,B>, B) (<14,0,C>, C) (<14,0,D>, D) (<14,0,E>, E) (<14,0,F>, F) (<14,0,G>, G) * Step 18: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. f16(A,B,C,D,E,F,G) -> f19(A,0,C,D,E,F,G) [19 >= A] (20,1) 1. f33(A,B,C,D,E,F,G) -> f36(A,B,C,0,E,F,G) [19 >= C] (20,1) 2. f52(A,B,C,D,E,F,G) -> f55(A,B,C,D,E,0,G) [19 >= E] (20,1) 3. f55(A,B,C,D,E,F,G) -> f59(A,B,C,D,E,F,0) [19 >= F] (400,1) 4. f59(A,B,C,D,E,F,G) -> f59(A,B,C,D,E,F,1 + G) [19 >= G] (?,1) 5. f59(A,B,C,D,E,F,G) -> f55(A,B,C,D,E,1 + F,G) [G >= 20] (400,1) 6. f55(A,B,C,D,E,F,G) -> f52(A,B,C,D,1 + E,F,G) [F >= 20] (20,1) 8. f36(A,B,C,D,E,F,G) -> f36(A,B,C,1 + D,E,F,G) [19 >= D] (400,1) 9. f36(A,B,C,D,E,F,G) -> f33(A,B,1 + C,D,E,F,G) [D >= 20] (400,1) 10. f33(A,B,C,D,E,F,G) -> f52(A,B,C,D,0,F,G) [C >= 20] (1,1) 11. f19(A,B,C,D,E,F,G) -> f19(A,1 + B,C,D,E,F,G) [19 >= B] (400,1) 12. f19(A,B,C,D,E,F,G) -> f16(1 + A,B,C,D,E,F,G) [B >= 20] (400,1) 13. f16(A,B,C,D,E,F,G) -> f33(A,B,0,D,E,F,G) [A >= 20] (1,1) 14. f0(A,B,C,D,E,F,G) -> f16(0,B,C,D,E,F,G) True (1,1) Signature: {(f0,7);(f16,7);(f19,7);(f33,7);(f36,7);(f52,7);(f55,7);(f59,7);(f73,7)} Flow Graph: [0->{11},1->{8},2->{3},3->{4},4->{4,5},5->{3,6},6->{2},8->{8,9},9->{1,10},10->{2},11->{11,12},12->{0,13} ,13->{1},14->{0}] Sizebounds: (< 0,0,A>, 19) (< 0,0,B>, 0) (< 0,0,C>, C) (< 0,0,D>, D) (< 0,0,E>, E) (< 0,0,F>, F) (< 0,0,G>, G) (< 1,0,A>, ?) (< 1,0,B>, ?) (< 1,0,C>, 19) (< 1,0,D>, 0) (< 1,0,E>, E) (< 1,0,F>, F) (< 1,0,G>, G) (< 2,0,A>, ?) (< 2,0,B>, ?) (< 2,0,C>, ?) (< 2,0,D>, ?) (< 2,0,E>, 19) (< 2,0,F>, 0) (< 2,0,G>, ?) (< 3,0,A>, ?) (< 3,0,B>, ?) (< 3,0,C>, ?) (< 3,0,D>, ?) (< 3,0,E>, ?) (< 3,0,F>, 19) (< 3,0,G>, 0) (< 4,0,A>, ?) (< 4,0,B>, ?) (< 4,0,C>, ?) (< 4,0,D>, ?) (< 4,0,E>, ?) (< 4,0,F>, 19) (< 4,0,G>, 20) (< 5,0,A>, ?) (< 5,0,B>, ?) (< 5,0,C>, ?) (< 5,0,D>, ?) (< 5,0,E>, ?) (< 5,0,F>, 19) (< 5,0,G>, 20) (< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, ?) (< 6,0,D>, ?) (< 6,0,E>, ?) (< 6,0,F>, 19) (< 6,0,G>, ?) (< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, 19) (< 8,0,D>, 20) (< 8,0,E>, E) (< 8,0,F>, F) (< 8,0,G>, G) (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, 19) (< 9,0,D>, 20) (< 9,0,E>, E) (< 9,0,F>, F) (< 9,0,G>, G) (<10,0,A>, ?) (<10,0,B>, ?) (<10,0,C>, 19) (<10,0,D>, 20 + D) (<10,0,E>, 0) (<10,0,F>, F) (<10,0,G>, G) (<11,0,A>, 19) (<11,0,B>, 20) (<11,0,C>, C) (<11,0,D>, D) (<11,0,E>, E) (<11,0,F>, F) (<11,0,G>, G) (<12,0,A>, 19) (<12,0,B>, 20) (<12,0,C>, C) (<12,0,D>, D) (<12,0,E>, E) (<12,0,F>, F) (<12,0,G>, G) (<13,0,A>, 19) (<13,0,B>, 20 + B) (<13,0,C>, 0) (<13,0,D>, D) (<13,0,E>, E) (<13,0,F>, F) (<13,0,G>, G) (<14,0,A>, 0) (<14,0,B>, B) (<14,0,C>, C) (<14,0,D>, D) (<14,0,E>, E) (<14,0,F>, F) (<14,0,G>, G) + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [2,6,5,4], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(f52) = -1*x7 p(f55) = -1*x7 p(f59) = 20 + -1*x7 The following rules are strictly oriented: [19 >= G] ==> f59(A,B,C,D,E,F,G) = 20 + -1*G > 19 + -1*G = f59(A,B,C,D,E,F,1 + G) The following rules are weakly oriented: [19 >= E] ==> f52(A,B,C,D,E,F,G) = -1*G >= -1*G = f55(A,B,C,D,E,0,G) [G >= 20] ==> f59(A,B,C,D,E,F,G) = 20 + -1*G >= -1*G = f55(A,B,C,D,E,1 + F,G) [F >= 20] ==> f55(A,B,C,D,E,F,G) = -1*G >= -1*G = f52(A,B,C,D,1 + E,F,G) We use the following global sizebounds: (< 0,0,A>, 19) (< 0,0,B>, 0) (< 0,0,C>, C) (< 0,0,D>, D) (< 0,0,E>, E) (< 0,0,F>, F) (< 0,0,G>, G) (< 1,0,A>, ?) (< 1,0,B>, ?) (< 1,0,C>, 19) (< 1,0,D>, 0) (< 1,0,E>, E) (< 1,0,F>, F) (< 1,0,G>, G) (< 2,0,A>, ?) (< 2,0,B>, ?) (< 2,0,C>, ?) (< 2,0,D>, ?) (< 2,0,E>, 19) (< 2,0,F>, 0) (< 2,0,G>, ?) (< 3,0,A>, ?) (< 3,0,B>, ?) (< 3,0,C>, ?) (< 3,0,D>, ?) (< 3,0,E>, ?) (< 3,0,F>, 19) (< 3,0,G>, 0) (< 4,0,A>, ?) (< 4,0,B>, ?) (< 4,0,C>, ?) (< 4,0,D>, ?) (< 4,0,E>, ?) (< 4,0,F>, 19) (< 4,0,G>, 20) (< 5,0,A>, ?) (< 5,0,B>, ?) (< 5,0,C>, ?) (< 5,0,D>, ?) (< 5,0,E>, ?) (< 5,0,F>, 19) (< 5,0,G>, 20) (< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, ?) (< 6,0,D>, ?) (< 6,0,E>, ?) (< 6,0,F>, 19) (< 6,0,G>, ?) (< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, 19) (< 8,0,D>, 20) (< 8,0,E>, E) (< 8,0,F>, F) (< 8,0,G>, G) (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, 19) (< 9,0,D>, 20) (< 9,0,E>, E) (< 9,0,F>, F) (< 9,0,G>, G) (<10,0,A>, ?) (<10,0,B>, ?) (<10,0,C>, 19) (<10,0,D>, 20 + D) (<10,0,E>, 0) (<10,0,F>, F) (<10,0,G>, G) (<11,0,A>, 19) (<11,0,B>, 20) (<11,0,C>, C) (<11,0,D>, D) (<11,0,E>, E) (<11,0,F>, F) (<11,0,G>, G) (<12,0,A>, 19) (<12,0,B>, 20) (<12,0,C>, C) (<12,0,D>, D) (<12,0,E>, E) (<12,0,F>, F) (<12,0,G>, G) (<13,0,A>, 19) (<13,0,B>, 20 + B) (<13,0,C>, 0) (<13,0,D>, D) (<13,0,E>, E) (<13,0,F>, F) (<13,0,G>, G) (<14,0,A>, 0) (<14,0,B>, B) (<14,0,C>, C) (<14,0,D>, D) (<14,0,E>, E) (<14,0,F>, F) (<14,0,G>, G) * Step 19: KnowledgePropagation WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. f16(A,B,C,D,E,F,G) -> f19(A,0,C,D,E,F,G) [19 >= A] (20,1) 1. f33(A,B,C,D,E,F,G) -> f36(A,B,C,0,E,F,G) [19 >= C] (20,1) 2. f52(A,B,C,D,E,F,G) -> f55(A,B,C,D,E,0,G) [19 >= E] (20,1) 3. f55(A,B,C,D,E,F,G) -> f59(A,B,C,D,E,F,0) [19 >= F] (400,1) 4. f59(A,B,C,D,E,F,G) -> f59(A,B,C,D,E,F,1 + G) [19 >= G] (8000 + G,1) 5. f59(A,B,C,D,E,F,G) -> f55(A,B,C,D,E,1 + F,G) [G >= 20] (400,1) 6. f55(A,B,C,D,E,F,G) -> f52(A,B,C,D,1 + E,F,G) [F >= 20] (20,1) 8. f36(A,B,C,D,E,F,G) -> f36(A,B,C,1 + D,E,F,G) [19 >= D] (400,1) 9. f36(A,B,C,D,E,F,G) -> f33(A,B,1 + C,D,E,F,G) [D >= 20] (400,1) 10. f33(A,B,C,D,E,F,G) -> f52(A,B,C,D,0,F,G) [C >= 20] (1,1) 11. f19(A,B,C,D,E,F,G) -> f19(A,1 + B,C,D,E,F,G) [19 >= B] (400,1) 12. f19(A,B,C,D,E,F,G) -> f16(1 + A,B,C,D,E,F,G) [B >= 20] (400,1) 13. f16(A,B,C,D,E,F,G) -> f33(A,B,0,D,E,F,G) [A >= 20] (1,1) 14. f0(A,B,C,D,E,F,G) -> f16(0,B,C,D,E,F,G) True (1,1) Signature: {(f0,7);(f16,7);(f19,7);(f33,7);(f36,7);(f52,7);(f55,7);(f59,7);(f73,7)} Flow Graph: [0->{11},1->{8},2->{3},3->{4},4->{4,5},5->{3,6},6->{2},8->{8,9},9->{1,10},10->{2},11->{11,12},12->{0,13} ,13->{1},14->{0}] Sizebounds: (< 0,0,A>, 19) (< 0,0,B>, 0) (< 0,0,C>, C) (< 0,0,D>, D) (< 0,0,E>, E) (< 0,0,F>, F) (< 0,0,G>, G) (< 1,0,A>, ?) (< 1,0,B>, ?) (< 1,0,C>, 19) (< 1,0,D>, 0) (< 1,0,E>, E) (< 1,0,F>, F) (< 1,0,G>, G) (< 2,0,A>, ?) (< 2,0,B>, ?) (< 2,0,C>, ?) (< 2,0,D>, ?) (< 2,0,E>, 19) (< 2,0,F>, 0) (< 2,0,G>, ?) (< 3,0,A>, ?) (< 3,0,B>, ?) (< 3,0,C>, ?) (< 3,0,D>, ?) (< 3,0,E>, ?) (< 3,0,F>, 19) (< 3,0,G>, 0) (< 4,0,A>, ?) (< 4,0,B>, ?) (< 4,0,C>, ?) (< 4,0,D>, ?) (< 4,0,E>, ?) (< 4,0,F>, 19) (< 4,0,G>, 20) (< 5,0,A>, ?) (< 5,0,B>, ?) (< 5,0,C>, ?) (< 5,0,D>, ?) (< 5,0,E>, ?) (< 5,0,F>, 19) (< 5,0,G>, 20) (< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, ?) (< 6,0,D>, ?) (< 6,0,E>, ?) (< 6,0,F>, 19) (< 6,0,G>, ?) (< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, 19) (< 8,0,D>, 20) (< 8,0,E>, E) (< 8,0,F>, F) (< 8,0,G>, G) (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, 19) (< 9,0,D>, 20) (< 9,0,E>, E) (< 9,0,F>, F) (< 9,0,G>, G) (<10,0,A>, ?) (<10,0,B>, ?) (<10,0,C>, 19) (<10,0,D>, 20 + D) (<10,0,E>, 0) (<10,0,F>, F) (<10,0,G>, G) (<11,0,A>, 19) (<11,0,B>, 20) (<11,0,C>, C) (<11,0,D>, D) (<11,0,E>, E) (<11,0,F>, F) (<11,0,G>, G) (<12,0,A>, 19) (<12,0,B>, 20) (<12,0,C>, C) (<12,0,D>, D) (<12,0,E>, E) (<12,0,F>, F) (<12,0,G>, G) (<13,0,A>, 19) (<13,0,B>, 20 + B) (<13,0,C>, 0) (<13,0,D>, D) (<13,0,E>, E) (<13,0,F>, F) (<13,0,G>, G) (<14,0,A>, 0) (<14,0,B>, B) (<14,0,C>, C) (<14,0,D>, D) (<14,0,E>, E) (<14,0,F>, F) (<14,0,G>, G) + Applied Processor: KnowledgePropagation + Details: The problem is already solved. WORST_CASE(?,O(n^1))