WORST_CASE(?,O(n^3)) * Step 1: LocalSizeboundsProc WORST_CASE(?,O(n^3)) + Considered Problem: Rules: 0. multiply(A,B,C,D,E) -> m6(A,B,C,D,E) True (1,1) 1. m0(A,B,C,D,E) -> m1(A,B,F,G,E) [A >= 1 && F >= 0 && A >= F && A >= G && G >= A && B >= F && F >= B] (?,1) 2. m2(A,B,C,D,E) -> m3(A,B,F,G,E) [F >= 0 && A >= G && G >= A && B >= F && F >= B] (?,1) 3. m4(A,B,C,D,E) -> m5(A,B,C,F,G) [B >= G && G >= B && C >= F && F >= C] (?,1) 4. m6(A,B,C,D,E) -> m7(A,B,C,D,E) True (?,1) 5. m5(A,B,C,D,E) -> n2(A,B,C,D,E) True (?,1) 6. m5(A,B,C,D,E) -> m9(D,E,C,D,E) True (?,1) 7. m3(A,B,C,D,E) -> n3(A,B,C,D,E) True (?,1) 8. m3(A,B,C,D,E) -> n0(C,D,C,D,E) True (?,1) 9. m1(A,B,C,D,E) -> n4(A,B,C,D,E) True (?,1) 10. m1(A,B,C,D,E) -> n1(C,D,C,D,E) True (?,1) 11. n20(A,B,C,D,E) -> m4(A,B,C,D,E) True (?,1) 12. n21(A,B,C,D,E) -> m2(A,0,C,D,E) True (?,1) 13. n2(A,B,C,D,E) -> c2(n20(A,B,F,D,E),n21(A,B,F,D,E)) [B >= F && 1 + C >= F && F >= 1 + C && B >= E && E >= B && 1 + D >= F && F >= 1 + D] (?,1) 14. n30(A,B,C,D,E) -> m2(A,B,C,D,E) True (?,1) 15. n31(A,B,C,D,E) -> m0(A,0,C,D,E) True (?,1) 16. n3(A,B,C,D,E) -> c2(n30(A,F,C,D,E),n31(A,F,C,D,E)) [F >= 1 && A >= F && 1 + C >= F && F >= 1 + C && 1 + B >= F && F >= 1 + B && A >= D && D >= A] (?,1) 17. m7(A,B,C,D,E) -> c2(m8(F,G,0,D,E),m4(F,G,0,D,E)) [B >= G && G >= B && A >= F && F >= A] (?,1) 18. n4(A,B,C,D,E) -> m0(A,F,C,D,E) [F >= 1 && A >= F && 1 + B >= F && F >= 1 + B && 1 + C >= F && F >= 1 + C && A >= D && D >= A] (?,1) Signature: {(m0,5) ;(m1,5) ;(m2,5) ;(m3,5) ;(m4,5) ;(m5,5) ;(m6,5) ;(m7,5) ;(m8,5) ;(m9,5) ;(multiply,5) ;(n0,5) ;(n1,5) ;(n2,5) ;(n20,5) ;(n21,5) ;(n3,5) ;(n30,5) ;(n31,5) ;(n4,5)} Flow Graph: [0->{4},1->{9,10},2->{7,8},3->{5,6},4->{17},5->{13},6->{},7->{16},8->{},9->{18},10->{},11->{3},12->{2} ,13->{11,12},14->{2},15->{1},16->{14,15},17->{3},18->{1}] + Applied Processor: LocalSizeboundsProc + Details: LocalSizebounds generated; rvgraph (< 0,0,A>, A, .= 0) (< 0,0,B>, B, .= 0) (< 0,0,C>, C, .= 0) (< 0,0,D>, D, .= 0) (< 0,0,E>, E, .= 0) (< 1,0,A>, A, .= 0) (< 1,0,B>, B, .= 0) (< 1,0,C>, B, .= 0) (< 1,0,D>, 1 + A, .+ 1) (< 1,0,E>, E, .= 0) (< 2,0,A>, A, .= 0) (< 2,0,B>, B, .= 0) (< 2,0,C>, B, .= 0) (< 2,0,D>, A, .= 0) (< 2,0,E>, E, .= 0) (< 3,0,A>, A, .= 0) (< 3,0,B>, B, .= 0) (< 3,0,C>, C, .= 0) (< 3,0,D>, C, .= 0) (< 3,0,E>, B, .= 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) (< 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) (< 6,0,A>, D, .= 0) (< 6,0,B>, E, .= 0) (< 6,0,C>, C, .= 0) (< 6,0,D>, D, .= 0) (< 6,0,E>, E, .= 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) (< 8,0,A>, C, .= 0) (< 8,0,B>, D, .= 0) (< 8,0,C>, C, .= 0) (< 8,0,D>, D, .= 0) (< 8,0,E>, E, .= 0) (< 9,0,A>, A, .= 0) (< 9,0,B>, B, .= 0) (< 9,0,C>, C, .= 0) (< 9,0,D>, D, .= 0) (< 9,0,E>, E, .= 0) (<10,0,A>, C, .= 0) (<10,0,B>, D, .= 0) (<10,0,C>, C, .= 0) (<10,0,D>, D, .= 0) (<10,0,E>, E, .= 0) (<11,0,A>, A, .= 0) (<11,0,B>, B, .= 0) (<11,0,C>, C, .= 0) (<11,0,D>, D, .= 0) (<11,0,E>, E, .= 0) (<12,0,A>, A, .= 0) (<12,0,B>, 0, .= 0) (<12,0,C>, C, .= 0) (<12,0,D>, D, .= 0) (<12,0,E>, E, .= 0) (<13,0,A>, A, .= 0) (<13,0,B>, B, .= 0) (<13,0,C>, 1 + B + C, .* 1) (<13,0,D>, D, .= 0) (<13,0,E>, E, .= 0) (<13,1,A>, A, .= 0) (<13,1,B>, B, .= 0) (<13,1,C>, 1 + B + C, .* 1) (<13,1,D>, D, .= 0) (<13,1,E>, E, .= 0) (<14,0,A>, A, .= 0) (<14,0,B>, B, .= 0) (<14,0,C>, C, .= 0) (<14,0,D>, D, .= 0) (<14,0,E>, E, .= 0) (<15,0,A>, A, .= 0) (<15,0,B>, 0, .= 0) (<15,0,C>, C, .= 0) (<15,0,D>, D, .= 0) (<15,0,E>, E, .= 0) (<16,0,A>, A, .= 0) (<16,0,B>, 1 + A, .+ 1) (<16,0,C>, C, .= 0) (<16,0,D>, D, .= 0) (<16,0,E>, E, .= 0) (<16,1,A>, A, .= 0) (<16,1,B>, 1 + A, .+ 1) (<16,1,C>, C, .= 0) (<16,1,D>, D, .= 0) (<16,1,E>, E, .= 0) (<17,0,A>, A, .= 0) (<17,0,B>, B, .= 0) (<17,0,C>, 0, .= 0) (<17,0,D>, D, .= 0) (<17,0,E>, E, .= 0) (<17,1,A>, A, .= 0) (<17,1,B>, B, .= 0) (<17,1,C>, 0, .= 0) (<17,1,D>, D, .= 0) (<17,1,E>, E, .= 0) (<18,0,A>, A, .= 0) (<18,0,B>, 1 + A, .+ 1) (<18,0,C>, C, .= 0) (<18,0,D>, D, .= 0) (<18,0,E>, E, .= 0) * Step 2: SizeboundsProc WORST_CASE(?,O(n^3)) + Considered Problem: Rules: 0. multiply(A,B,C,D,E) -> m6(A,B,C,D,E) True (1,1) 1. m0(A,B,C,D,E) -> m1(A,B,F,G,E) [A >= 1 && F >= 0 && A >= F && A >= G && G >= A && B >= F && F >= B] (?,1) 2. m2(A,B,C,D,E) -> m3(A,B,F,G,E) [F >= 0 && A >= G && G >= A && B >= F && F >= B] (?,1) 3. m4(A,B,C,D,E) -> m5(A,B,C,F,G) [B >= G && G >= B && C >= F && F >= C] (?,1) 4. m6(A,B,C,D,E) -> m7(A,B,C,D,E) True (?,1) 5. m5(A,B,C,D,E) -> n2(A,B,C,D,E) True (?,1) 6. m5(A,B,C,D,E) -> m9(D,E,C,D,E) True (?,1) 7. m3(A,B,C,D,E) -> n3(A,B,C,D,E) True (?,1) 8. m3(A,B,C,D,E) -> n0(C,D,C,D,E) True (?,1) 9. m1(A,B,C,D,E) -> n4(A,B,C,D,E) True (?,1) 10. m1(A,B,C,D,E) -> n1(C,D,C,D,E) True (?,1) 11. n20(A,B,C,D,E) -> m4(A,B,C,D,E) True (?,1) 12. n21(A,B,C,D,E) -> m2(A,0,C,D,E) True (?,1) 13. n2(A,B,C,D,E) -> c2(n20(A,B,F,D,E),n21(A,B,F,D,E)) [B >= F && 1 + C >= F && F >= 1 + C && B >= E && E >= B && 1 + D >= F && F >= 1 + D] (?,1) 14. n30(A,B,C,D,E) -> m2(A,B,C,D,E) True (?,1) 15. n31(A,B,C,D,E) -> m0(A,0,C,D,E) True (?,1) 16. n3(A,B,C,D,E) -> c2(n30(A,F,C,D,E),n31(A,F,C,D,E)) [F >= 1 && A >= F && 1 + C >= F && F >= 1 + C && 1 + B >= F && F >= 1 + B && A >= D && D >= A] (?,1) 17. m7(A,B,C,D,E) -> c2(m8(F,G,0,D,E),m4(F,G,0,D,E)) [B >= G && G >= B && A >= F && F >= A] (?,1) 18. n4(A,B,C,D,E) -> m0(A,F,C,D,E) [F >= 1 && A >= F && 1 + B >= F && F >= 1 + B && 1 + C >= F && F >= 1 + C && A >= D && D >= A] (?,1) Signature: {(m0,5) ;(m1,5) ;(m2,5) ;(m3,5) ;(m4,5) ;(m5,5) ;(m6,5) ;(m7,5) ;(m8,5) ;(m9,5) ;(multiply,5) ;(n0,5) ;(n1,5) ;(n2,5) ;(n20,5) ;(n21,5) ;(n3,5) ;(n30,5) ;(n31,5) ;(n4,5)} Flow Graph: [0->{4},1->{9,10},2->{7,8},3->{5,6},4->{17},5->{13},6->{},7->{16},8->{},9->{18},10->{},11->{3},12->{2} ,13->{11,12},14->{2},15->{1},16->{14,15},17->{3},18->{1}] Sizebounds: (< 0,0,A>, ?) (< 0,0,B>, ?) (< 0,0,C>, ?) (< 0,0,D>, ?) (< 0,0,E>, ?) (< 1,0,A>, ?) (< 1,0,B>, ?) (< 1,0,C>, ?) (< 1,0,D>, ?) (< 1,0,E>, ?) (< 2,0,A>, ?) (< 2,0,B>, ?) (< 2,0,C>, ?) (< 2,0,D>, ?) (< 2,0,E>, ?) (< 3,0,A>, ?) (< 3,0,B>, ?) (< 3,0,C>, ?) (< 3,0,D>, ?) (< 3,0,E>, ?) (< 4,0,A>, ?) (< 4,0,B>, ?) (< 4,0,C>, ?) (< 4,0,D>, ?) (< 4,0,E>, ?) (< 5,0,A>, ?) (< 5,0,B>, ?) (< 5,0,C>, ?) (< 5,0,D>, ?) (< 5,0,E>, ?) (< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, ?) (< 6,0,D>, ?) (< 6,0,E>, ?) (< 7,0,A>, ?) (< 7,0,B>, ?) (< 7,0,C>, ?) (< 7,0,D>, ?) (< 7,0,E>, ?) (< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, ?) (< 8,0,D>, ?) (< 8,0,E>, ?) (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, ?) (< 9,0,D>, ?) (< 9,0,E>, ?) (<10,0,A>, ?) (<10,0,B>, ?) (<10,0,C>, ?) (<10,0,D>, ?) (<10,0,E>, ?) (<11,0,A>, ?) (<11,0,B>, ?) (<11,0,C>, ?) (<11,0,D>, ?) (<11,0,E>, ?) (<12,0,A>, ?) (<12,0,B>, ?) (<12,0,C>, ?) (<12,0,D>, ?) (<12,0,E>, ?) (<13,0,A>, ?) (<13,0,B>, ?) (<13,0,C>, ?) (<13,0,D>, ?) (<13,0,E>, ?) (<13,1,A>, ?) (<13,1,B>, ?) (<13,1,C>, ?) (<13,1,D>, ?) (<13,1,E>, ?) (<14,0,A>, ?) (<14,0,B>, ?) (<14,0,C>, ?) (<14,0,D>, ?) (<14,0,E>, ?) (<15,0,A>, ?) (<15,0,B>, ?) (<15,0,C>, ?) (<15,0,D>, ?) (<15,0,E>, ?) (<16,0,A>, ?) (<16,0,B>, ?) (<16,0,C>, ?) (<16,0,D>, ?) (<16,0,E>, ?) (<16,1,A>, ?) (<16,1,B>, ?) (<16,1,C>, ?) (<16,1,D>, ?) (<16,1,E>, ?) (<17,0,A>, ?) (<17,0,B>, ?) (<17,0,C>, ?) (<17,0,D>, ?) (<17,0,E>, ?) (<17,1,A>, ?) (<17,1,B>, ?) (<17,1,C>, ?) (<17,1,D>, ?) (<17,1,E>, ?) (<18,0,A>, ?) (<18,0,B>, ?) (<18,0,C>, ?) (<18,0,D>, ?) (<18,0,E>, ?) + Applied Processor: SizeboundsProc + Details: Sizebounds computed: (< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D) (< 0,0,E>, E) (< 1,0,A>, A) (< 1,0,B>, 1 + A) (< 1,0,C>, 1 + A) (< 1,0,D>, 1 + A) (< 1,0,E>, B) (< 2,0,A>, A) (< 2,0,B>, 1 + A) (< 2,0,C>, 1 + A) (< 2,0,D>, A) (< 2,0,E>, B) (< 3,0,A>, A) (< 3,0,B>, B) (< 3,0,C>, ?) (< 3,0,D>, ?) (< 3,0,E>, B) (< 4,0,A>, A) (< 4,0,B>, B) (< 4,0,C>, C) (< 4,0,D>, D) (< 4,0,E>, E) (< 5,0,A>, A) (< 5,0,B>, B) (< 5,0,C>, ?) (< 5,0,D>, ?) (< 5,0,E>, B) (< 6,0,A>, ?) (< 6,0,B>, B) (< 6,0,C>, ?) (< 6,0,D>, ?) (< 6,0,E>, B) (< 7,0,A>, A) (< 7,0,B>, 1 + A) (< 7,0,C>, 1 + A) (< 7,0,D>, A) (< 7,0,E>, B) (< 8,0,A>, 1 + A) (< 8,0,B>, A) (< 8,0,C>, 1 + A) (< 8,0,D>, A) (< 8,0,E>, B) (< 9,0,A>, A) (< 9,0,B>, 1 + A) (< 9,0,C>, 1 + A) (< 9,0,D>, 1 + A) (< 9,0,E>, B) (<10,0,A>, 1 + A) (<10,0,B>, 1 + A) (<10,0,C>, 1 + A) (<10,0,D>, 1 + A) (<10,0,E>, B) (<11,0,A>, A) (<11,0,B>, B) (<11,0,C>, ?) (<11,0,D>, ?) (<11,0,E>, B) (<12,0,A>, A) (<12,0,B>, 0) (<12,0,C>, ?) (<12,0,D>, ?) (<12,0,E>, B) (<13,0,A>, A) (<13,0,B>, B) (<13,0,C>, ?) (<13,0,D>, ?) (<13,0,E>, B) (<13,1,A>, A) (<13,1,B>, B) (<13,1,C>, ?) (<13,1,D>, ?) (<13,1,E>, B) (<14,0,A>, A) (<14,0,B>, 1 + A) (<14,0,C>, 1 + A) (<14,0,D>, A) (<14,0,E>, B) (<15,0,A>, A) (<15,0,B>, 0) (<15,0,C>, 1 + A) (<15,0,D>, A) (<15,0,E>, B) (<16,0,A>, A) (<16,0,B>, 1 + A) (<16,0,C>, 1 + A) (<16,0,D>, A) (<16,0,E>, B) (<16,1,A>, A) (<16,1,B>, 1 + A) (<16,1,C>, 1 + A) (<16,1,D>, A) (<16,1,E>, B) (<17,0,A>, A) (<17,0,B>, B) (<17,0,C>, 0) (<17,0,D>, D) (<17,0,E>, E) (<17,1,A>, A) (<17,1,B>, B) (<17,1,C>, 0) (<17,1,D>, D) (<17,1,E>, E) (<18,0,A>, A) (<18,0,B>, 1 + A) (<18,0,C>, 1 + A) (<18,0,D>, 1 + A) (<18,0,E>, B) * Step 3: LeafRules WORST_CASE(?,O(n^3)) + Considered Problem: Rules: 0. multiply(A,B,C,D,E) -> m6(A,B,C,D,E) True (1,1) 1. m0(A,B,C,D,E) -> m1(A,B,F,G,E) [A >= 1 && F >= 0 && A >= F && A >= G && G >= A && B >= F && F >= B] (?,1) 2. m2(A,B,C,D,E) -> m3(A,B,F,G,E) [F >= 0 && A >= G && G >= A && B >= F && F >= B] (?,1) 3. m4(A,B,C,D,E) -> m5(A,B,C,F,G) [B >= G && G >= B && C >= F && F >= C] (?,1) 4. m6(A,B,C,D,E) -> m7(A,B,C,D,E) True (?,1) 5. m5(A,B,C,D,E) -> n2(A,B,C,D,E) True (?,1) 6. m5(A,B,C,D,E) -> m9(D,E,C,D,E) True (?,1) 7. m3(A,B,C,D,E) -> n3(A,B,C,D,E) True (?,1) 8. m3(A,B,C,D,E) -> n0(C,D,C,D,E) True (?,1) 9. m1(A,B,C,D,E) -> n4(A,B,C,D,E) True (?,1) 10. m1(A,B,C,D,E) -> n1(C,D,C,D,E) True (?,1) 11. n20(A,B,C,D,E) -> m4(A,B,C,D,E) True (?,1) 12. n21(A,B,C,D,E) -> m2(A,0,C,D,E) True (?,1) 13. n2(A,B,C,D,E) -> c2(n20(A,B,F,D,E),n21(A,B,F,D,E)) [B >= F && 1 + C >= F && F >= 1 + C && B >= E && E >= B && 1 + D >= F && F >= 1 + D] (?,1) 14. n30(A,B,C,D,E) -> m2(A,B,C,D,E) True (?,1) 15. n31(A,B,C,D,E) -> m0(A,0,C,D,E) True (?,1) 16. n3(A,B,C,D,E) -> c2(n30(A,F,C,D,E),n31(A,F,C,D,E)) [F >= 1 && A >= F && 1 + C >= F && F >= 1 + C && 1 + B >= F && F >= 1 + B && A >= D && D >= A] (?,1) 17. m7(A,B,C,D,E) -> c2(m8(F,G,0,D,E),m4(F,G,0,D,E)) [B >= G && G >= B && A >= F && F >= A] (?,1) 18. n4(A,B,C,D,E) -> m0(A,F,C,D,E) [F >= 1 && A >= F && 1 + B >= F && F >= 1 + B && 1 + C >= F && F >= 1 + C && A >= D && D >= A] (?,1) Signature: {(m0,5) ;(m1,5) ;(m2,5) ;(m3,5) ;(m4,5) ;(m5,5) ;(m6,5) ;(m7,5) ;(m8,5) ;(m9,5) ;(multiply,5) ;(n0,5) ;(n1,5) ;(n2,5) ;(n20,5) ;(n21,5) ;(n3,5) ;(n30,5) ;(n31,5) ;(n4,5)} Flow Graph: [0->{4},1->{9,10},2->{7,8},3->{5,6},4->{17},5->{13},6->{},7->{16},8->{},9->{18},10->{},11->{3},12->{2} ,13->{11,12},14->{2},15->{1},16->{14,15},17->{3},18->{1}] Sizebounds: (< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D) (< 0,0,E>, E) (< 1,0,A>, A) (< 1,0,B>, 1 + A) (< 1,0,C>, 1 + A) (< 1,0,D>, 1 + A) (< 1,0,E>, B) (< 2,0,A>, A) (< 2,0,B>, 1 + A) (< 2,0,C>, 1 + A) (< 2,0,D>, A) (< 2,0,E>, B) (< 3,0,A>, A) (< 3,0,B>, B) (< 3,0,C>, ?) (< 3,0,D>, ?) (< 3,0,E>, B) (< 4,0,A>, A) (< 4,0,B>, B) (< 4,0,C>, C) (< 4,0,D>, D) (< 4,0,E>, E) (< 5,0,A>, A) (< 5,0,B>, B) (< 5,0,C>, ?) (< 5,0,D>, ?) (< 5,0,E>, B) (< 6,0,A>, ?) (< 6,0,B>, B) (< 6,0,C>, ?) (< 6,0,D>, ?) (< 6,0,E>, B) (< 7,0,A>, A) (< 7,0,B>, 1 + A) (< 7,0,C>, 1 + A) (< 7,0,D>, A) (< 7,0,E>, B) (< 8,0,A>, 1 + A) (< 8,0,B>, A) (< 8,0,C>, 1 + A) (< 8,0,D>, A) (< 8,0,E>, B) (< 9,0,A>, A) (< 9,0,B>, 1 + A) (< 9,0,C>, 1 + A) (< 9,0,D>, 1 + A) (< 9,0,E>, B) (<10,0,A>, 1 + A) (<10,0,B>, 1 + A) (<10,0,C>, 1 + A) (<10,0,D>, 1 + A) (<10,0,E>, B) (<11,0,A>, A) (<11,0,B>, B) (<11,0,C>, ?) (<11,0,D>, ?) (<11,0,E>, B) (<12,0,A>, A) (<12,0,B>, 0) (<12,0,C>, ?) (<12,0,D>, ?) (<12,0,E>, B) (<13,0,A>, A) (<13,0,B>, B) (<13,0,C>, ?) (<13,0,D>, ?) (<13,0,E>, B) (<13,1,A>, A) (<13,1,B>, B) (<13,1,C>, ?) (<13,1,D>, ?) (<13,1,E>, B) (<14,0,A>, A) (<14,0,B>, 1 + A) (<14,0,C>, 1 + A) (<14,0,D>, A) (<14,0,E>, B) (<15,0,A>, A) (<15,0,B>, 0) (<15,0,C>, 1 + A) (<15,0,D>, A) (<15,0,E>, B) (<16,0,A>, A) (<16,0,B>, 1 + A) (<16,0,C>, 1 + A) (<16,0,D>, A) (<16,0,E>, B) (<16,1,A>, A) (<16,1,B>, 1 + A) (<16,1,C>, 1 + A) (<16,1,D>, A) (<16,1,E>, B) (<17,0,A>, A) (<17,0,B>, B) (<17,0,C>, 0) (<17,0,D>, D) (<17,0,E>, E) (<17,1,A>, A) (<17,1,B>, B) (<17,1,C>, 0) (<17,1,D>, D) (<17,1,E>, E) (<18,0,A>, A) (<18,0,B>, 1 + A) (<18,0,C>, 1 + A) (<18,0,D>, 1 + A) (<18,0,E>, B) + Applied Processor: LeafRules + Details: The following transitions are estimated by its predecessors and are removed [6,8,10] * Step 4: PolyRank WORST_CASE(?,O(n^3)) + Considered Problem: Rules: 0. multiply(A,B,C,D,E) -> m6(A,B,C,D,E) True (1,1) 1. m0(A,B,C,D,E) -> m1(A,B,F,G,E) [A >= 1 && F >= 0 && A >= F && A >= G && G >= A && B >= F && F >= B] (?,1) 2. m2(A,B,C,D,E) -> m3(A,B,F,G,E) [F >= 0 && A >= G && G >= A && B >= F && F >= B] (?,1) 3. m4(A,B,C,D,E) -> m5(A,B,C,F,G) [B >= G && G >= B && C >= F && F >= C] (?,1) 4. m6(A,B,C,D,E) -> m7(A,B,C,D,E) True (?,1) 5. m5(A,B,C,D,E) -> n2(A,B,C,D,E) True (?,1) 7. m3(A,B,C,D,E) -> n3(A,B,C,D,E) True (?,1) 9. m1(A,B,C,D,E) -> n4(A,B,C,D,E) True (?,1) 11. n20(A,B,C,D,E) -> m4(A,B,C,D,E) True (?,1) 12. n21(A,B,C,D,E) -> m2(A,0,C,D,E) True (?,1) 13. n2(A,B,C,D,E) -> c2(n20(A,B,F,D,E),n21(A,B,F,D,E)) [B >= F && 1 + C >= F && F >= 1 + C && B >= E && E >= B && 1 + D >= F && F >= 1 + D] (?,1) 14. n30(A,B,C,D,E) -> m2(A,B,C,D,E) True (?,1) 15. n31(A,B,C,D,E) -> m0(A,0,C,D,E) True (?,1) 16. n3(A,B,C,D,E) -> c2(n30(A,F,C,D,E),n31(A,F,C,D,E)) [F >= 1 && A >= F && 1 + C >= F && F >= 1 + C && 1 + B >= F && F >= 1 + B && A >= D && D >= A] (?,1) 17. m7(A,B,C,D,E) -> c2(m8(F,G,0,D,E),m4(F,G,0,D,E)) [B >= G && G >= B && A >= F && F >= A] (?,1) 18. n4(A,B,C,D,E) -> m0(A,F,C,D,E) [F >= 1 && A >= F && 1 + B >= F && F >= 1 + B && 1 + C >= F && F >= 1 + C && A >= D && D >= A] (?,1) Signature: {(m0,5) ;(m1,5) ;(m2,5) ;(m3,5) ;(m4,5) ;(m5,5) ;(m6,5) ;(m7,5) ;(m8,5) ;(m9,5) ;(multiply,5) ;(n0,5) ;(n1,5) ;(n2,5) ;(n20,5) ;(n21,5) ;(n3,5) ;(n30,5) ;(n31,5) ;(n4,5)} Flow Graph: [0->{4},1->{9},2->{7},3->{5},4->{17},5->{13},7->{16},9->{18},11->{3},12->{2},13->{11,12},14->{2},15->{1} ,16->{14,15},17->{3},18->{1}] Sizebounds: (< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D) (< 0,0,E>, E) (< 1,0,A>, A) (< 1,0,B>, 1 + A) (< 1,0,C>, 1 + A) (< 1,0,D>, 1 + A) (< 1,0,E>, B) (< 2,0,A>, A) (< 2,0,B>, 1 + A) (< 2,0,C>, 1 + A) (< 2,0,D>, A) (< 2,0,E>, B) (< 3,0,A>, A) (< 3,0,B>, B) (< 3,0,C>, ?) (< 3,0,D>, ?) (< 3,0,E>, B) (< 4,0,A>, A) (< 4,0,B>, B) (< 4,0,C>, C) (< 4,0,D>, D) (< 4,0,E>, E) (< 5,0,A>, A) (< 5,0,B>, B) (< 5,0,C>, ?) (< 5,0,D>, ?) (< 5,0,E>, B) (< 7,0,A>, A) (< 7,0,B>, 1 + A) (< 7,0,C>, 1 + A) (< 7,0,D>, A) (< 7,0,E>, B) (< 9,0,A>, A) (< 9,0,B>, 1 + A) (< 9,0,C>, 1 + A) (< 9,0,D>, 1 + A) (< 9,0,E>, B) (<11,0,A>, A) (<11,0,B>, B) (<11,0,C>, ?) (<11,0,D>, ?) (<11,0,E>, B) (<12,0,A>, A) (<12,0,B>, 0) (<12,0,C>, ?) (<12,0,D>, ?) (<12,0,E>, B) (<13,0,A>, A) (<13,0,B>, B) (<13,0,C>, ?) (<13,0,D>, ?) (<13,0,E>, B) (<13,1,A>, A) (<13,1,B>, B) (<13,1,C>, ?) (<13,1,D>, ?) (<13,1,E>, B) (<14,0,A>, A) (<14,0,B>, 1 + A) (<14,0,C>, 1 + A) (<14,0,D>, A) (<14,0,E>, B) (<15,0,A>, A) (<15,0,B>, 0) (<15,0,C>, 1 + A) (<15,0,D>, A) (<15,0,E>, B) (<16,0,A>, A) (<16,0,B>, 1 + A) (<16,0,C>, 1 + A) (<16,0,D>, A) (<16,0,E>, B) (<16,1,A>, A) (<16,1,B>, 1 + A) (<16,1,C>, 1 + A) (<16,1,D>, A) (<16,1,E>, B) (<17,0,A>, A) (<17,0,B>, B) (<17,0,C>, 0) (<17,0,D>, D) (<17,0,E>, E) (<17,1,A>, A) (<17,1,B>, B) (<17,1,C>, 0) (<17,1,D>, D) (<17,1,E>, E) (<18,0,A>, A) (<18,0,B>, 1 + A) (<18,0,C>, 1 + A) (<18,0,D>, 1 + A) (<18,0,E>, B) + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(m0) = 0 p(m1) = 0 p(m2) = 0 p(m3) = 0 p(m4) = 0 p(m5) = 0 p(m6) = 1 p(m7) = 1 p(m8) = 0 p(multiply) = 1 p(n2) = 0 p(n20) = 0 p(n21) = 0 p(n3) = 0 p(n30) = 0 p(n31) = 0 p(n4) = 0 The following rules are strictly oriented: [B >= G && G >= B && A >= F && F >= A] ==> m7(A,B,C,D,E) = 1 > 0 = c2(m8(F,G,0,D,E),m4(F,G,0,D,E)) The following rules are weakly oriented: True ==> multiply(A,B,C,D,E) = 1 >= 1 = m6(A,B,C,D,E) [A >= 1 && F >= 0 && A >= F && A >= G && G >= A && B >= F && F >= B] ==> m0(A,B,C,D,E) = 0 >= 0 = m1(A,B,F,G,E) [F >= 0 && A >= G && G >= A && B >= F && F >= B] ==> m2(A,B,C,D,E) = 0 >= 0 = m3(A,B,F,G,E) [B >= G && G >= B && C >= F && F >= C] ==> m4(A,B,C,D,E) = 0 >= 0 = m5(A,B,C,F,G) True ==> m6(A,B,C,D,E) = 1 >= 1 = m7(A,B,C,D,E) True ==> m5(A,B,C,D,E) = 0 >= 0 = n2(A,B,C,D,E) True ==> m3(A,B,C,D,E) = 0 >= 0 = n3(A,B,C,D,E) True ==> m1(A,B,C,D,E) = 0 >= 0 = n4(A,B,C,D,E) True ==> n20(A,B,C,D,E) = 0 >= 0 = m4(A,B,C,D,E) True ==> n21(A,B,C,D,E) = 0 >= 0 = m2(A,0,C,D,E) [B >= F && 1 + C >= F && F >= 1 + C && B >= E && E >= B && 1 + D >= F && F >= 1 + D] ==> n2(A,B,C,D,E) = 0 >= 0 = c2(n20(A,B,F,D,E),n21(A,B,F,D,E)) True ==> n30(A,B,C,D,E) = 0 >= 0 = m2(A,B,C,D,E) True ==> n31(A,B,C,D,E) = 0 >= 0 = m0(A,0,C,D,E) [F >= 1 && A >= F && 1 + C >= F && F >= 1 + C && 1 + B >= F && F >= 1 + B && A >= D && D >= A] ==> n3(A,B,C,D,E) = 0 >= 0 = c2(n30(A,F,C,D,E),n31(A,F,C,D,E)) [F >= 1 && A >= F && 1 + B >= F && F >= 1 + B && 1 + C >= F && F >= 1 + C && A >= D && D >= A] ==> n4(A,B,C,D,E) = 0 >= 0 = m0(A,F,C,D,E) * Step 5: KnowledgePropagation WORST_CASE(?,O(n^3)) + Considered Problem: Rules: 0. multiply(A,B,C,D,E) -> m6(A,B,C,D,E) True (1,1) 1. m0(A,B,C,D,E) -> m1(A,B,F,G,E) [A >= 1 && F >= 0 && A >= F && A >= G && G >= A && B >= F && F >= B] (?,1) 2. m2(A,B,C,D,E) -> m3(A,B,F,G,E) [F >= 0 && A >= G && G >= A && B >= F && F >= B] (?,1) 3. m4(A,B,C,D,E) -> m5(A,B,C,F,G) [B >= G && G >= B && C >= F && F >= C] (?,1) 4. m6(A,B,C,D,E) -> m7(A,B,C,D,E) True (?,1) 5. m5(A,B,C,D,E) -> n2(A,B,C,D,E) True (?,1) 7. m3(A,B,C,D,E) -> n3(A,B,C,D,E) True (?,1) 9. m1(A,B,C,D,E) -> n4(A,B,C,D,E) True (?,1) 11. n20(A,B,C,D,E) -> m4(A,B,C,D,E) True (?,1) 12. n21(A,B,C,D,E) -> m2(A,0,C,D,E) True (?,1) 13. n2(A,B,C,D,E) -> c2(n20(A,B,F,D,E),n21(A,B,F,D,E)) [B >= F && 1 + C >= F && F >= 1 + C && B >= E && E >= B && 1 + D >= F && F >= 1 + D] (?,1) 14. n30(A,B,C,D,E) -> m2(A,B,C,D,E) True (?,1) 15. n31(A,B,C,D,E) -> m0(A,0,C,D,E) True (?,1) 16. n3(A,B,C,D,E) -> c2(n30(A,F,C,D,E),n31(A,F,C,D,E)) [F >= 1 && A >= F && 1 + C >= F && F >= 1 + C && 1 + B >= F && F >= 1 + B && A >= D && D >= A] (?,1) 17. m7(A,B,C,D,E) -> c2(m8(F,G,0,D,E),m4(F,G,0,D,E)) [B >= G && G >= B && A >= F && F >= A] (1,1) 18. n4(A,B,C,D,E) -> m0(A,F,C,D,E) [F >= 1 && A >= F && 1 + B >= F && F >= 1 + B && 1 + C >= F && F >= 1 + C && A >= D && D >= A] (?,1) Signature: {(m0,5) ;(m1,5) ;(m2,5) ;(m3,5) ;(m4,5) ;(m5,5) ;(m6,5) ;(m7,5) ;(m8,5) ;(m9,5) ;(multiply,5) ;(n0,5) ;(n1,5) ;(n2,5) ;(n20,5) ;(n21,5) ;(n3,5) ;(n30,5) ;(n31,5) ;(n4,5)} Flow Graph: [0->{4},1->{9},2->{7},3->{5},4->{17},5->{13},7->{16},9->{18},11->{3},12->{2},13->{11,12},14->{2},15->{1} ,16->{14,15},17->{3},18->{1}] Sizebounds: (< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D) (< 0,0,E>, E) (< 1,0,A>, A) (< 1,0,B>, 1 + A) (< 1,0,C>, 1 + A) (< 1,0,D>, 1 + A) (< 1,0,E>, B) (< 2,0,A>, A) (< 2,0,B>, 1 + A) (< 2,0,C>, 1 + A) (< 2,0,D>, A) (< 2,0,E>, B) (< 3,0,A>, A) (< 3,0,B>, B) (< 3,0,C>, ?) (< 3,0,D>, ?) (< 3,0,E>, B) (< 4,0,A>, A) (< 4,0,B>, B) (< 4,0,C>, C) (< 4,0,D>, D) (< 4,0,E>, E) (< 5,0,A>, A) (< 5,0,B>, B) (< 5,0,C>, ?) (< 5,0,D>, ?) (< 5,0,E>, B) (< 7,0,A>, A) (< 7,0,B>, 1 + A) (< 7,0,C>, 1 + A) (< 7,0,D>, A) (< 7,0,E>, B) (< 9,0,A>, A) (< 9,0,B>, 1 + A) (< 9,0,C>, 1 + A) (< 9,0,D>, 1 + A) (< 9,0,E>, B) (<11,0,A>, A) (<11,0,B>, B) (<11,0,C>, ?) (<11,0,D>, ?) (<11,0,E>, B) (<12,0,A>, A) (<12,0,B>, 0) (<12,0,C>, ?) (<12,0,D>, ?) (<12,0,E>, B) (<13,0,A>, A) (<13,0,B>, B) (<13,0,C>, ?) (<13,0,D>, ?) (<13,0,E>, B) (<13,1,A>, A) (<13,1,B>, B) (<13,1,C>, ?) (<13,1,D>, ?) (<13,1,E>, B) (<14,0,A>, A) (<14,0,B>, 1 + A) (<14,0,C>, 1 + A) (<14,0,D>, A) (<14,0,E>, B) (<15,0,A>, A) (<15,0,B>, 0) (<15,0,C>, 1 + A) (<15,0,D>, A) (<15,0,E>, B) (<16,0,A>, A) (<16,0,B>, 1 + A) (<16,0,C>, 1 + A) (<16,0,D>, A) (<16,0,E>, B) (<16,1,A>, A) (<16,1,B>, 1 + A) (<16,1,C>, 1 + A) (<16,1,D>, A) (<16,1,E>, B) (<17,0,A>, A) (<17,0,B>, B) (<17,0,C>, 0) (<17,0,D>, D) (<17,0,E>, E) (<17,1,A>, A) (<17,1,B>, B) (<17,1,C>, 0) (<17,1,D>, D) (<17,1,E>, E) (<18,0,A>, A) (<18,0,B>, 1 + A) (<18,0,C>, 1 + A) (<18,0,D>, 1 + A) (<18,0,E>, B) + Applied Processor: KnowledgePropagation + Details: We propagate bounds from predecessors. * Step 6: ChainProcessor WORST_CASE(?,O(n^3)) + Considered Problem: Rules: 0. multiply(A,B,C,D,E) -> m6(A,B,C,D,E) True (1,1) 1. m0(A,B,C,D,E) -> m1(A,B,F,G,E) [A >= 1 && F >= 0 && A >= F && A >= G && G >= A && B >= F && F >= B] (?,1) 2. m2(A,B,C,D,E) -> m3(A,B,F,G,E) [F >= 0 && A >= G && G >= A && B >= F && F >= B] (?,1) 3. m4(A,B,C,D,E) -> m5(A,B,C,F,G) [B >= G && G >= B && C >= F && F >= C] (?,1) 4. m6(A,B,C,D,E) -> m7(A,B,C,D,E) True (1,1) 5. m5(A,B,C,D,E) -> n2(A,B,C,D,E) True (?,1) 7. m3(A,B,C,D,E) -> n3(A,B,C,D,E) True (?,1) 9. m1(A,B,C,D,E) -> n4(A,B,C,D,E) True (?,1) 11. n20(A,B,C,D,E) -> m4(A,B,C,D,E) True (?,1) 12. n21(A,B,C,D,E) -> m2(A,0,C,D,E) True (?,1) 13. n2(A,B,C,D,E) -> c2(n20(A,B,F,D,E),n21(A,B,F,D,E)) [B >= F && 1 + C >= F && F >= 1 + C && B >= E && E >= B && 1 + D >= F && F >= 1 + D] (?,1) 14. n30(A,B,C,D,E) -> m2(A,B,C,D,E) True (?,1) 15. n31(A,B,C,D,E) -> m0(A,0,C,D,E) True (?,1) 16. n3(A,B,C,D,E) -> c2(n30(A,F,C,D,E),n31(A,F,C,D,E)) [F >= 1 && A >= F && 1 + C >= F && F >= 1 + C && 1 + B >= F && F >= 1 + B && A >= D && D >= A] (?,1) 17. m7(A,B,C,D,E) -> c2(m8(F,G,0,D,E),m4(F,G,0,D,E)) [B >= G && G >= B && A >= F && F >= A] (1,1) 18. n4(A,B,C,D,E) -> m0(A,F,C,D,E) [F >= 1 && A >= F && 1 + B >= F && F >= 1 + B && 1 + C >= F && F >= 1 + C && A >= D && D >= A] (?,1) Signature: {(m0,5) ;(m1,5) ;(m2,5) ;(m3,5) ;(m4,5) ;(m5,5) ;(m6,5) ;(m7,5) ;(m8,5) ;(m9,5) ;(multiply,5) ;(n0,5) ;(n1,5) ;(n2,5) ;(n20,5) ;(n21,5) ;(n3,5) ;(n30,5) ;(n31,5) ;(n4,5)} Flow Graph: [0->{4},1->{9},2->{7},3->{5},4->{17},5->{13},7->{16},9->{18},11->{3},12->{2},13->{11,12},14->{2},15->{1} ,16->{14,15},17->{3},18->{1}] Sizebounds: (< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D) (< 0,0,E>, E) (< 1,0,A>, A) (< 1,0,B>, 1 + A) (< 1,0,C>, 1 + A) (< 1,0,D>, 1 + A) (< 1,0,E>, B) (< 2,0,A>, A) (< 2,0,B>, 1 + A) (< 2,0,C>, 1 + A) (< 2,0,D>, A) (< 2,0,E>, B) (< 3,0,A>, A) (< 3,0,B>, B) (< 3,0,C>, ?) (< 3,0,D>, ?) (< 3,0,E>, B) (< 4,0,A>, A) (< 4,0,B>, B) (< 4,0,C>, C) (< 4,0,D>, D) (< 4,0,E>, E) (< 5,0,A>, A) (< 5,0,B>, B) (< 5,0,C>, ?) (< 5,0,D>, ?) (< 5,0,E>, B) (< 7,0,A>, A) (< 7,0,B>, 1 + A) (< 7,0,C>, 1 + A) (< 7,0,D>, A) (< 7,0,E>, B) (< 9,0,A>, A) (< 9,0,B>, 1 + A) (< 9,0,C>, 1 + A) (< 9,0,D>, 1 + A) (< 9,0,E>, B) (<11,0,A>, A) (<11,0,B>, B) (<11,0,C>, ?) (<11,0,D>, ?) (<11,0,E>, B) (<12,0,A>, A) (<12,0,B>, 0) (<12,0,C>, ?) (<12,0,D>, ?) (<12,0,E>, B) (<13,0,A>, A) (<13,0,B>, B) (<13,0,C>, ?) (<13,0,D>, ?) (<13,0,E>, B) (<13,1,A>, A) (<13,1,B>, B) (<13,1,C>, ?) (<13,1,D>, ?) (<13,1,E>, B) (<14,0,A>, A) (<14,0,B>, 1 + A) (<14,0,C>, 1 + A) (<14,0,D>, A) (<14,0,E>, B) (<15,0,A>, A) (<15,0,B>, 0) (<15,0,C>, 1 + A) (<15,0,D>, A) (<15,0,E>, B) (<16,0,A>, A) (<16,0,B>, 1 + A) (<16,0,C>, 1 + A) (<16,0,D>, A) (<16,0,E>, B) (<16,1,A>, A) (<16,1,B>, 1 + A) (<16,1,C>, 1 + A) (<16,1,D>, A) (<16,1,E>, B) (<17,0,A>, A) (<17,0,B>, B) (<17,0,C>, 0) (<17,0,D>, D) (<17,0,E>, E) (<17,1,A>, A) (<17,1,B>, B) (<17,1,C>, 0) (<17,1,D>, D) (<17,1,E>, E) (<18,0,A>, A) (<18,0,B>, 1 + A) (<18,0,C>, 1 + A) (<18,0,D>, 1 + A) (<18,0,E>, B) + Applied Processor: ChainProcessor False [0,1,2,3,4,5,7,9,11,12,13,14,15,16,17,18] + Details: We chained rule 0 to obtain the rules [19] . * Step 7: UnreachableRules WORST_CASE(?,O(n^3)) + Considered Problem: Rules: 1. m0(A,B,C,D,E) -> m1(A,B,F,G,E) [A >= 1 && F >= 0 && A >= F && A >= G && G >= A && B >= F && F >= B] (?,1) 2. m2(A,B,C,D,E) -> m3(A,B,F,G,E) [F >= 0 && A >= G && G >= A && B >= F && F >= B] (?,1) 3. m4(A,B,C,D,E) -> m5(A,B,C,F,G) [B >= G && G >= B && C >= F && F >= C] (?,1) 4. m6(A,B,C,D,E) -> m7(A,B,C,D,E) True (1,1) 5. m5(A,B,C,D,E) -> n2(A,B,C,D,E) True (?,1) 7. m3(A,B,C,D,E) -> n3(A,B,C,D,E) True (?,1) 9. m1(A,B,C,D,E) -> n4(A,B,C,D,E) True (?,1) 11. n20(A,B,C,D,E) -> m4(A,B,C,D,E) True (?,1) 12. n21(A,B,C,D,E) -> m2(A,0,C,D,E) True (?,1) 13. n2(A,B,C,D,E) -> c2(n20(A,B,F,D,E),n21(A,B,F,D,E)) [B >= F && 1 + C >= F && F >= 1 + C && B >= E && E >= B && 1 + D >= F && F >= 1 + D] (?,1) 14. n30(A,B,C,D,E) -> m2(A,B,C,D,E) True (?,1) 15. n31(A,B,C,D,E) -> m0(A,0,C,D,E) True (?,1) 16. n3(A,B,C,D,E) -> c2(n30(A,F,C,D,E),n31(A,F,C,D,E)) [F >= 1 && A >= F && 1 + C >= F && F >= 1 + C && 1 + B >= F && F >= 1 + B && A >= D && D >= A] (?,1) 17. m7(A,B,C,D,E) -> c2(m8(F,G,0,D,E),m4(F,G,0,D,E)) [B >= G && G >= B && A >= F && F >= A] (1,1) 18. n4(A,B,C,D,E) -> m0(A,F,C,D,E) [F >= 1 && A >= F && 1 + B >= F && F >= 1 + B && 1 + C >= F && F >= 1 + C && A >= D && D >= A] (?,1) 19. multiply(A,B,C,D,E) -> m7(A,B,C,D,E) True (1,2) Signature: {(m0,5) ;(m1,5) ;(m2,5) ;(m3,5) ;(m4,5) ;(m5,5) ;(m6,5) ;(m7,5) ;(m8,5) ;(m9,5) ;(multiply,5) ;(n0,5) ;(n1,5) ;(n2,5) ;(n20,5) ;(n21,5) ;(n3,5) ;(n30,5) ;(n31,5) ;(n4,5)} Flow Graph: [1->{9},2->{7},3->{5},4->{17},5->{13},7->{16},9->{18},11->{3},12->{2},13->{11,12},14->{2},15->{1},16->{14 ,15},17->{3},18->{1},19->{17}] Sizebounds: (< 1,0,A>, A) (< 1,0,B>, 1 + A) (< 1,0,C>, 1 + A) (< 1,0,D>, 1 + A) (< 1,0,E>, B) (< 2,0,A>, A) (< 2,0,B>, 1 + A) (< 2,0,C>, 1 + A) (< 2,0,D>, A) (< 2,0,E>, B) (< 3,0,A>, A) (< 3,0,B>, B) (< 3,0,C>, ?) (< 3,0,D>, ?) (< 3,0,E>, B) (< 4,0,A>, A) (< 4,0,B>, B) (< 4,0,C>, C) (< 4,0,D>, D) (< 4,0,E>, E) (< 5,0,A>, A) (< 5,0,B>, B) (< 5,0,C>, ?) (< 5,0,D>, ?) (< 5,0,E>, B) (< 7,0,A>, A) (< 7,0,B>, 1 + A) (< 7,0,C>, 1 + A) (< 7,0,D>, A) (< 7,0,E>, B) (< 9,0,A>, A) (< 9,0,B>, 1 + A) (< 9,0,C>, 1 + A) (< 9,0,D>, 1 + A) (< 9,0,E>, B) (<11,0,A>, A) (<11,0,B>, B) (<11,0,C>, ?) (<11,0,D>, ?) (<11,0,E>, B) (<12,0,A>, A) (<12,0,B>, 0) (<12,0,C>, ?) (<12,0,D>, ?) (<12,0,E>, B) (<13,0,A>, A) (<13,0,B>, B) (<13,0,C>, ?) (<13,0,D>, ?) (<13,0,E>, B) (<13,1,A>, A) (<13,1,B>, B) (<13,1,C>, ?) (<13,1,D>, ?) (<13,1,E>, B) (<14,0,A>, A) (<14,0,B>, 1 + A) (<14,0,C>, 1 + A) (<14,0,D>, A) (<14,0,E>, B) (<15,0,A>, A) (<15,0,B>, 0) (<15,0,C>, 1 + A) (<15,0,D>, A) (<15,0,E>, B) (<16,0,A>, A) (<16,0,B>, 1 + A) (<16,0,C>, 1 + A) (<16,0,D>, A) (<16,0,E>, B) (<16,1,A>, A) (<16,1,B>, 1 + A) (<16,1,C>, 1 + A) (<16,1,D>, A) (<16,1,E>, B) (<17,0,A>, A) (<17,0,B>, B) (<17,0,C>, 0) (<17,0,D>, D) (<17,0,E>, E) (<17,1,A>, A) (<17,1,B>, B) (<17,1,C>, 0) (<17,1,D>, D) (<17,1,E>, E) (<18,0,A>, A) (<18,0,B>, 1 + A) (<18,0,C>, 1 + A) (<18,0,D>, 1 + A) (<18,0,E>, B) (<19,0,A>, A) (<19,0,B>, B) (<19,0,C>, C) (<19,0,D>, D) (<19,0,E>, E) + Applied Processor: UnreachableRules + Details: The following transitions are not reachable from the starting states and are removed: [4] * Step 8: ChainProcessor WORST_CASE(?,O(n^3)) + Considered Problem: Rules: 1. m0(A,B,C,D,E) -> m1(A,B,F,G,E) [A >= 1 && F >= 0 && A >= F && A >= G && G >= A && B >= F && F >= B] (?,1) 2. m2(A,B,C,D,E) -> m3(A,B,F,G,E) [F >= 0 && A >= G && G >= A && B >= F && F >= B] (?,1) 3. m4(A,B,C,D,E) -> m5(A,B,C,F,G) [B >= G && G >= B && C >= F && F >= C] (?,1) 5. m5(A,B,C,D,E) -> n2(A,B,C,D,E) True (?,1) 7. m3(A,B,C,D,E) -> n3(A,B,C,D,E) True (?,1) 9. m1(A,B,C,D,E) -> n4(A,B,C,D,E) True (?,1) 11. n20(A,B,C,D,E) -> m4(A,B,C,D,E) True (?,1) 12. n21(A,B,C,D,E) -> m2(A,0,C,D,E) True (?,1) 13. n2(A,B,C,D,E) -> c2(n20(A,B,F,D,E),n21(A,B,F,D,E)) [B >= F && 1 + C >= F && F >= 1 + C && B >= E && E >= B && 1 + D >= F && F >= 1 + D] (?,1) 14. n30(A,B,C,D,E) -> m2(A,B,C,D,E) True (?,1) 15. n31(A,B,C,D,E) -> m0(A,0,C,D,E) True (?,1) 16. n3(A,B,C,D,E) -> c2(n30(A,F,C,D,E),n31(A,F,C,D,E)) [F >= 1 && A >= F && 1 + C >= F && F >= 1 + C && 1 + B >= F && F >= 1 + B && A >= D && D >= A] (?,1) 17. m7(A,B,C,D,E) -> c2(m8(F,G,0,D,E),m4(F,G,0,D,E)) [B >= G && G >= B && A >= F && F >= A] (1,1) 18. n4(A,B,C,D,E) -> m0(A,F,C,D,E) [F >= 1 && A >= F && 1 + B >= F && F >= 1 + B && 1 + C >= F && F >= 1 + C && A >= D && D >= A] (?,1) 19. multiply(A,B,C,D,E) -> m7(A,B,C,D,E) True (1,2) Signature: {(m0,5) ;(m1,5) ;(m2,5) ;(m3,5) ;(m4,5) ;(m5,5) ;(m6,5) ;(m7,5) ;(m8,5) ;(m9,5) ;(multiply,5) ;(n0,5) ;(n1,5) ;(n2,5) ;(n20,5) ;(n21,5) ;(n3,5) ;(n30,5) ;(n31,5) ;(n4,5)} Flow Graph: [1->{9},2->{7},3->{5},5->{13},7->{16},9->{18},11->{3},12->{2},13->{11,12},14->{2},15->{1},16->{14,15} ,17->{3},18->{1},19->{17}] Sizebounds: (< 1,0,A>, A) (< 1,0,B>, 1 + A) (< 1,0,C>, 1 + A) (< 1,0,D>, 1 + A) (< 1,0,E>, B) (< 2,0,A>, A) (< 2,0,B>, 1 + A) (< 2,0,C>, 1 + A) (< 2,0,D>, A) (< 2,0,E>, B) (< 3,0,A>, A) (< 3,0,B>, B) (< 3,0,C>, ?) (< 3,0,D>, ?) (< 3,0,E>, B) (< 5,0,A>, A) (< 5,0,B>, B) (< 5,0,C>, ?) (< 5,0,D>, ?) (< 5,0,E>, B) (< 7,0,A>, A) (< 7,0,B>, 1 + A) (< 7,0,C>, 1 + A) (< 7,0,D>, A) (< 7,0,E>, B) (< 9,0,A>, A) (< 9,0,B>, 1 + A) (< 9,0,C>, 1 + A) (< 9,0,D>, 1 + A) (< 9,0,E>, B) (<11,0,A>, A) (<11,0,B>, B) (<11,0,C>, ?) (<11,0,D>, ?) (<11,0,E>, B) (<12,0,A>, A) (<12,0,B>, 0) (<12,0,C>, ?) (<12,0,D>, ?) (<12,0,E>, B) (<13,0,A>, A) (<13,0,B>, B) (<13,0,C>, ?) (<13,0,D>, ?) (<13,0,E>, B) (<13,1,A>, A) (<13,1,B>, B) (<13,1,C>, ?) (<13,1,D>, ?) (<13,1,E>, B) (<14,0,A>, A) (<14,0,B>, 1 + A) (<14,0,C>, 1 + A) (<14,0,D>, A) (<14,0,E>, B) (<15,0,A>, A) (<15,0,B>, 0) (<15,0,C>, 1 + A) (<15,0,D>, A) (<15,0,E>, B) (<16,0,A>, A) (<16,0,B>, 1 + A) (<16,0,C>, 1 + A) (<16,0,D>, A) (<16,0,E>, B) (<16,1,A>, A) (<16,1,B>, 1 + A) (<16,1,C>, 1 + A) (<16,1,D>, A) (<16,1,E>, B) (<17,0,A>, A) (<17,0,B>, B) (<17,0,C>, 0) (<17,0,D>, D) (<17,0,E>, E) (<17,1,A>, A) (<17,1,B>, B) (<17,1,C>, 0) (<17,1,D>, D) (<17,1,E>, E) (<18,0,A>, A) (<18,0,B>, 1 + A) (<18,0,C>, 1 + A) (<18,0,D>, 1 + A) (<18,0,E>, B) (<19,0,A>, A) (<19,0,B>, B) (<19,0,C>, C) (<19,0,D>, D) (<19,0,E>, E) + Applied Processor: ChainProcessor False [1,2,3,5,7,9,11,12,13,14,15,16,17,18,19] + Details: We chained rule 1 to obtain the rules [20] . * Step 9: UnreachableRules WORST_CASE(?,O(n^3)) + Considered Problem: Rules: 2. m2(A,B,C,D,E) -> m3(A,B,F,G,E) [F >= 0 && A >= G && G >= A && B >= F && F >= B] (?,1) 3. m4(A,B,C,D,E) -> m5(A,B,C,F,G) [B >= G && G >= B && C >= F && F >= C] (?,1) 5. m5(A,B,C,D,E) -> n2(A,B,C,D,E) True (?,1) 7. m3(A,B,C,D,E) -> n3(A,B,C,D,E) True (?,1) 9. m1(A,B,C,D,E) -> n4(A,B,C,D,E) True (?,1) 11. n20(A,B,C,D,E) -> m4(A,B,C,D,E) True (?,1) 12. n21(A,B,C,D,E) -> m2(A,0,C,D,E) True (?,1) 13. n2(A,B,C,D,E) -> c2(n20(A,B,F,D,E),n21(A,B,F,D,E)) [B >= F && 1 + C >= F && F >= 1 + C && B >= E && E >= B && 1 + D >= F && F >= 1 + D] (?,1) 14. n30(A,B,C,D,E) -> m2(A,B,C,D,E) True (?,1) 15. n31(A,B,C,D,E) -> m0(A,0,C,D,E) True (?,1) 16. n3(A,B,C,D,E) -> c2(n30(A,F,C,D,E),n31(A,F,C,D,E)) [F >= 1 && A >= F && 1 + C >= F && F >= 1 + C && 1 + B >= F && F >= 1 + B && A >= D && D >= A] (?,1) 17. m7(A,B,C,D,E) -> c2(m8(F,G,0,D,E),m4(F,G,0,D,E)) [B >= G && G >= B && A >= F && F >= A] (1,1) 18. n4(A,B,C,D,E) -> m0(A,F,C,D,E) [F >= 1 && A >= F && 1 + B >= F && F >= 1 + B && 1 + C >= F && F >= 1 + C && A >= D && D >= A] (?,1) 19. multiply(A,B,C,D,E) -> m7(A,B,C,D,E) True (1,2) 20. m0(A,B,C,D,E) -> n4(A,B,F,G,E) [A >= 1 && F >= 0 && A >= F && A >= G && G >= A && B >= F && F >= B] (?,2) Signature: {(m0,5) ;(m1,5) ;(m2,5) ;(m3,5) ;(m4,5) ;(m5,5) ;(m6,5) ;(m7,5) ;(m8,5) ;(m9,5) ;(multiply,5) ;(n0,5) ;(n1,5) ;(n2,5) ;(n20,5) ;(n21,5) ;(n3,5) ;(n30,5) ;(n31,5) ;(n4,5)} Flow Graph: [2->{7},3->{5},5->{13},7->{16},9->{18},11->{3},12->{2},13->{11,12},14->{2},15->{20},16->{14,15},17->{3} ,18->{20},19->{17},20->{18}] Sizebounds: (< 2,0,A>, A) (< 2,0,B>, 1 + A) (< 2,0,C>, 1 + A) (< 2,0,D>, A) (< 2,0,E>, B) (< 3,0,A>, A) (< 3,0,B>, B) (< 3,0,C>, ?) (< 3,0,D>, ?) (< 3,0,E>, B) (< 5,0,A>, A) (< 5,0,B>, B) (< 5,0,C>, ?) (< 5,0,D>, ?) (< 5,0,E>, B) (< 7,0,A>, A) (< 7,0,B>, 1 + A) (< 7,0,C>, 1 + A) (< 7,0,D>, A) (< 7,0,E>, B) (< 9,0,A>, A) (< 9,0,B>, 1 + A) (< 9,0,C>, 1 + A) (< 9,0,D>, 1 + A) (< 9,0,E>, B) (<11,0,A>, A) (<11,0,B>, B) (<11,0,C>, ?) (<11,0,D>, ?) (<11,0,E>, B) (<12,0,A>, A) (<12,0,B>, 0) (<12,0,C>, ?) (<12,0,D>, ?) (<12,0,E>, B) (<13,0,A>, A) (<13,0,B>, B) (<13,0,C>, ?) (<13,0,D>, ?) (<13,0,E>, B) (<13,1,A>, A) (<13,1,B>, B) (<13,1,C>, ?) (<13,1,D>, ?) (<13,1,E>, B) (<14,0,A>, A) (<14,0,B>, 1 + A) (<14,0,C>, 1 + A) (<14,0,D>, A) (<14,0,E>, B) (<15,0,A>, A) (<15,0,B>, 0) (<15,0,C>, 1 + A) (<15,0,D>, A) (<15,0,E>, B) (<16,0,A>, A) (<16,0,B>, 1 + A) (<16,0,C>, 1 + A) (<16,0,D>, A) (<16,0,E>, B) (<16,1,A>, A) (<16,1,B>, 1 + A) (<16,1,C>, 1 + A) (<16,1,D>, A) (<16,1,E>, B) (<17,0,A>, A) (<17,0,B>, B) (<17,0,C>, 0) (<17,0,D>, D) (<17,0,E>, E) (<17,1,A>, A) (<17,1,B>, B) (<17,1,C>, 0) (<17,1,D>, D) (<17,1,E>, E) (<18,0,A>, A) (<18,0,B>, 1 + A) (<18,0,C>, 1 + A) (<18,0,D>, 1 + A) (<18,0,E>, B) (<19,0,A>, A) (<19,0,B>, B) (<19,0,C>, C) (<19,0,D>, D) (<19,0,E>, E) (<20,0,A>, A) (<20,0,B>, 1 + A) (<20,0,C>, 1 + A) (<20,0,D>, 1 + A) (<20,0,E>, B) + Applied Processor: UnreachableRules + Details: The following transitions are not reachable from the starting states and are removed: [9] * Step 10: ChainProcessor WORST_CASE(?,O(n^3)) + Considered Problem: Rules: 2. m2(A,B,C,D,E) -> m3(A,B,F,G,E) [F >= 0 && A >= G && G >= A && B >= F && F >= B] (?,1) 3. m4(A,B,C,D,E) -> m5(A,B,C,F,G) [B >= G && G >= B && C >= F && F >= C] (?,1) 5. m5(A,B,C,D,E) -> n2(A,B,C,D,E) True (?,1) 7. m3(A,B,C,D,E) -> n3(A,B,C,D,E) True (?,1) 11. n20(A,B,C,D,E) -> m4(A,B,C,D,E) True (?,1) 12. n21(A,B,C,D,E) -> m2(A,0,C,D,E) True (?,1) 13. n2(A,B,C,D,E) -> c2(n20(A,B,F,D,E),n21(A,B,F,D,E)) [B >= F && 1 + C >= F && F >= 1 + C && B >= E && E >= B && 1 + D >= F && F >= 1 + D] (?,1) 14. n30(A,B,C,D,E) -> m2(A,B,C,D,E) True (?,1) 15. n31(A,B,C,D,E) -> m0(A,0,C,D,E) True (?,1) 16. n3(A,B,C,D,E) -> c2(n30(A,F,C,D,E),n31(A,F,C,D,E)) [F >= 1 && A >= F && 1 + C >= F && F >= 1 + C && 1 + B >= F && F >= 1 + B && A >= D && D >= A] (?,1) 17. m7(A,B,C,D,E) -> c2(m8(F,G,0,D,E),m4(F,G,0,D,E)) [B >= G && G >= B && A >= F && F >= A] (1,1) 18. n4(A,B,C,D,E) -> m0(A,F,C,D,E) [F >= 1 && A >= F && 1 + B >= F && F >= 1 + B && 1 + C >= F && F >= 1 + C && A >= D && D >= A] (?,1) 19. multiply(A,B,C,D,E) -> m7(A,B,C,D,E) True (1,2) 20. m0(A,B,C,D,E) -> n4(A,B,F,G,E) [A >= 1 && F >= 0 && A >= F && A >= G && G >= A && B >= F && F >= B] (?,2) Signature: {(m0,5) ;(m1,5) ;(m2,5) ;(m3,5) ;(m4,5) ;(m5,5) ;(m6,5) ;(m7,5) ;(m8,5) ;(m9,5) ;(multiply,5) ;(n0,5) ;(n1,5) ;(n2,5) ;(n20,5) ;(n21,5) ;(n3,5) ;(n30,5) ;(n31,5) ;(n4,5)} Flow Graph: [2->{7},3->{5},5->{13},7->{16},11->{3},12->{2},13->{11,12},14->{2},15->{20},16->{14,15},17->{3},18->{20} ,19->{17},20->{18}] Sizebounds: (< 2,0,A>, A) (< 2,0,B>, 1 + A) (< 2,0,C>, 1 + A) (< 2,0,D>, A) (< 2,0,E>, B) (< 3,0,A>, A) (< 3,0,B>, B) (< 3,0,C>, ?) (< 3,0,D>, ?) (< 3,0,E>, B) (< 5,0,A>, A) (< 5,0,B>, B) (< 5,0,C>, ?) (< 5,0,D>, ?) (< 5,0,E>, B) (< 7,0,A>, A) (< 7,0,B>, 1 + A) (< 7,0,C>, 1 + A) (< 7,0,D>, A) (< 7,0,E>, B) (<11,0,A>, A) (<11,0,B>, B) (<11,0,C>, ?) (<11,0,D>, ?) (<11,0,E>, B) (<12,0,A>, A) (<12,0,B>, 0) (<12,0,C>, ?) (<12,0,D>, ?) (<12,0,E>, B) (<13,0,A>, A) (<13,0,B>, B) (<13,0,C>, ?) (<13,0,D>, ?) (<13,0,E>, B) (<13,1,A>, A) (<13,1,B>, B) (<13,1,C>, ?) (<13,1,D>, ?) (<13,1,E>, B) (<14,0,A>, A) (<14,0,B>, 1 + A) (<14,0,C>, 1 + A) (<14,0,D>, A) (<14,0,E>, B) (<15,0,A>, A) (<15,0,B>, 0) (<15,0,C>, 1 + A) (<15,0,D>, A) (<15,0,E>, B) (<16,0,A>, A) (<16,0,B>, 1 + A) (<16,0,C>, 1 + A) (<16,0,D>, A) (<16,0,E>, B) (<16,1,A>, A) (<16,1,B>, 1 + A) (<16,1,C>, 1 + A) (<16,1,D>, A) (<16,1,E>, B) (<17,0,A>, A) (<17,0,B>, B) (<17,0,C>, 0) (<17,0,D>, D) (<17,0,E>, E) (<17,1,A>, A) (<17,1,B>, B) (<17,1,C>, 0) (<17,1,D>, D) (<17,1,E>, E) (<18,0,A>, A) (<18,0,B>, 1 + A) (<18,0,C>, 1 + A) (<18,0,D>, 1 + A) (<18,0,E>, B) (<19,0,A>, A) (<19,0,B>, B) (<19,0,C>, C) (<19,0,D>, D) (<19,0,E>, E) (<20,0,A>, A) (<20,0,B>, 1 + A) (<20,0,C>, 1 + A) (<20,0,D>, 1 + A) (<20,0,E>, B) + Applied Processor: ChainProcessor False [2,3,5,7,11,12,13,14,15,16,17,18,19,20] + Details: We chained rule 2 to obtain the rules [21] . * Step 11: UnreachableRules WORST_CASE(?,O(n^3)) + Considered Problem: Rules: 3. m4(A,B,C,D,E) -> m5(A,B,C,F,G) [B >= G && G >= B && C >= F && F >= C] (?,1) 5. m5(A,B,C,D,E) -> n2(A,B,C,D,E) True (?,1) 7. m3(A,B,C,D,E) -> n3(A,B,C,D,E) True (?,1) 11. n20(A,B,C,D,E) -> m4(A,B,C,D,E) True (?,1) 12. n21(A,B,C,D,E) -> m2(A,0,C,D,E) True (?,1) 13. n2(A,B,C,D,E) -> c2(n20(A,B,F,D,E),n21(A,B,F,D,E)) [B >= F && 1 + C >= F && F >= 1 + C && B >= E && E >= B && 1 + D >= F && F >= 1 + D] (?,1) 14. n30(A,B,C,D,E) -> m2(A,B,C,D,E) True (?,1) 15. n31(A,B,C,D,E) -> m0(A,0,C,D,E) True (?,1) 16. n3(A,B,C,D,E) -> c2(n30(A,F,C,D,E),n31(A,F,C,D,E)) [F >= 1 && A >= F && 1 + C >= F && F >= 1 + C && 1 + B >= F && F >= 1 + B && A >= D && D >= A] (?,1) 17. m7(A,B,C,D,E) -> c2(m8(F,G,0,D,E),m4(F,G,0,D,E)) [B >= G && G >= B && A >= F && F >= A] (1,1) 18. n4(A,B,C,D,E) -> m0(A,F,C,D,E) [F >= 1 && A >= F && 1 + B >= F && F >= 1 + B && 1 + C >= F && F >= 1 + C && A >= D && D >= A] (?,1) 19. multiply(A,B,C,D,E) -> m7(A,B,C,D,E) True (1,2) 20. m0(A,B,C,D,E) -> n4(A,B,F,G,E) [A >= 1 && F >= 0 && A >= F && A >= G && G >= A && B >= F && F >= B] (?,2) 21. m2(A,B,C,D,E) -> n3(A,B,F,G,E) [F >= 0 && A >= G && G >= A && B >= F && F >= B] (?,2) Signature: {(m0,5) ;(m1,5) ;(m2,5) ;(m3,5) ;(m4,5) ;(m5,5) ;(m6,5) ;(m7,5) ;(m8,5) ;(m9,5) ;(multiply,5) ;(n0,5) ;(n1,5) ;(n2,5) ;(n20,5) ;(n21,5) ;(n3,5) ;(n30,5) ;(n31,5) ;(n4,5)} Flow Graph: [3->{5},5->{13},7->{16},11->{3},12->{21},13->{11,12},14->{21},15->{20},16->{14,15},17->{3},18->{20} ,19->{17},20->{18},21->{16}] Sizebounds: (< 3,0,A>, A) (< 3,0,B>, B) (< 3,0,C>, ?) (< 3,0,D>, ?) (< 3,0,E>, B) (< 5,0,A>, A) (< 5,0,B>, B) (< 5,0,C>, ?) (< 5,0,D>, ?) (< 5,0,E>, B) (< 7,0,A>, A) (< 7,0,B>, 1 + A) (< 7,0,C>, 1 + A) (< 7,0,D>, A) (< 7,0,E>, B) (<11,0,A>, A) (<11,0,B>, B) (<11,0,C>, ?) (<11,0,D>, ?) (<11,0,E>, B) (<12,0,A>, A) (<12,0,B>, 0) (<12,0,C>, ?) (<12,0,D>, ?) (<12,0,E>, B) (<13,0,A>, A) (<13,0,B>, B) (<13,0,C>, ?) (<13,0,D>, ?) (<13,0,E>, B) (<13,1,A>, A) (<13,1,B>, B) (<13,1,C>, ?) (<13,1,D>, ?) (<13,1,E>, B) (<14,0,A>, A) (<14,0,B>, 1 + A) (<14,0,C>, 1 + A) (<14,0,D>, A) (<14,0,E>, B) (<15,0,A>, A) (<15,0,B>, 0) (<15,0,C>, 1 + A) (<15,0,D>, A) (<15,0,E>, B) (<16,0,A>, A) (<16,0,B>, 1 + A) (<16,0,C>, 1 + A) (<16,0,D>, A) (<16,0,E>, B) (<16,1,A>, A) (<16,1,B>, 1 + A) (<16,1,C>, 1 + A) (<16,1,D>, A) (<16,1,E>, B) (<17,0,A>, A) (<17,0,B>, B) (<17,0,C>, 0) (<17,0,D>, D) (<17,0,E>, E) (<17,1,A>, A) (<17,1,B>, B) (<17,1,C>, 0) (<17,1,D>, D) (<17,1,E>, E) (<18,0,A>, A) (<18,0,B>, 1 + A) (<18,0,C>, 1 + A) (<18,0,D>, 1 + A) (<18,0,E>, B) (<19,0,A>, A) (<19,0,B>, B) (<19,0,C>, C) (<19,0,D>, D) (<19,0,E>, E) (<20,0,A>, A) (<20,0,B>, 1 + A) (<20,0,C>, 1 + A) (<20,0,D>, 1 + A) (<20,0,E>, B) (<21,0,A>, A) (<21,0,B>, 1 + A) (<21,0,C>, 1 + A) (<21,0,D>, A) (<21,0,E>, B) + Applied Processor: UnreachableRules + Details: The following transitions are not reachable from the starting states and are removed: [7] * Step 12: ChainProcessor WORST_CASE(?,O(n^3)) + Considered Problem: Rules: 3. m4(A,B,C,D,E) -> m5(A,B,C,F,G) [B >= G && G >= B && C >= F && F >= C] (?,1) 5. m5(A,B,C,D,E) -> n2(A,B,C,D,E) True (?,1) 11. n20(A,B,C,D,E) -> m4(A,B,C,D,E) True (?,1) 12. n21(A,B,C,D,E) -> m2(A,0,C,D,E) True (?,1) 13. n2(A,B,C,D,E) -> c2(n20(A,B,F,D,E),n21(A,B,F,D,E)) [B >= F && 1 + C >= F && F >= 1 + C && B >= E && E >= B && 1 + D >= F && F >= 1 + D] (?,1) 14. n30(A,B,C,D,E) -> m2(A,B,C,D,E) True (?,1) 15. n31(A,B,C,D,E) -> m0(A,0,C,D,E) True (?,1) 16. n3(A,B,C,D,E) -> c2(n30(A,F,C,D,E),n31(A,F,C,D,E)) [F >= 1 && A >= F && 1 + C >= F && F >= 1 + C && 1 + B >= F && F >= 1 + B && A >= D && D >= A] (?,1) 17. m7(A,B,C,D,E) -> c2(m8(F,G,0,D,E),m4(F,G,0,D,E)) [B >= G && G >= B && A >= F && F >= A] (1,1) 18. n4(A,B,C,D,E) -> m0(A,F,C,D,E) [F >= 1 && A >= F && 1 + B >= F && F >= 1 + B && 1 + C >= F && F >= 1 + C && A >= D && D >= A] (?,1) 19. multiply(A,B,C,D,E) -> m7(A,B,C,D,E) True (1,2) 20. m0(A,B,C,D,E) -> n4(A,B,F,G,E) [A >= 1 && F >= 0 && A >= F && A >= G && G >= A && B >= F && F >= B] (?,2) 21. m2(A,B,C,D,E) -> n3(A,B,F,G,E) [F >= 0 && A >= G && G >= A && B >= F && F >= B] (?,2) Signature: {(m0,5) ;(m1,5) ;(m2,5) ;(m3,5) ;(m4,5) ;(m5,5) ;(m6,5) ;(m7,5) ;(m8,5) ;(m9,5) ;(multiply,5) ;(n0,5) ;(n1,5) ;(n2,5) ;(n20,5) ;(n21,5) ;(n3,5) ;(n30,5) ;(n31,5) ;(n4,5)} Flow Graph: [3->{5},5->{13},11->{3},12->{21},13->{11,12},14->{21},15->{20},16->{14,15},17->{3},18->{20},19->{17} ,20->{18},21->{16}] Sizebounds: (< 3,0,A>, A) (< 3,0,B>, B) (< 3,0,C>, ?) (< 3,0,D>, ?) (< 3,0,E>, B) (< 5,0,A>, A) (< 5,0,B>, B) (< 5,0,C>, ?) (< 5,0,D>, ?) (< 5,0,E>, B) (<11,0,A>, A) (<11,0,B>, B) (<11,0,C>, ?) (<11,0,D>, ?) (<11,0,E>, B) (<12,0,A>, A) (<12,0,B>, 0) (<12,0,C>, ?) (<12,0,D>, ?) (<12,0,E>, B) (<13,0,A>, A) (<13,0,B>, B) (<13,0,C>, ?) (<13,0,D>, ?) (<13,0,E>, B) (<13,1,A>, A) (<13,1,B>, B) (<13,1,C>, ?) (<13,1,D>, ?) (<13,1,E>, B) (<14,0,A>, A) (<14,0,B>, 1 + A) (<14,0,C>, 1 + A) (<14,0,D>, A) (<14,0,E>, B) (<15,0,A>, A) (<15,0,B>, 0) (<15,0,C>, 1 + A) (<15,0,D>, A) (<15,0,E>, B) (<16,0,A>, A) (<16,0,B>, 1 + A) (<16,0,C>, 1 + A) (<16,0,D>, A) (<16,0,E>, B) (<16,1,A>, A) (<16,1,B>, 1 + A) (<16,1,C>, 1 + A) (<16,1,D>, A) (<16,1,E>, B) (<17,0,A>, A) (<17,0,B>, B) (<17,0,C>, 0) (<17,0,D>, D) (<17,0,E>, E) (<17,1,A>, A) (<17,1,B>, B) (<17,1,C>, 0) (<17,1,D>, D) (<17,1,E>, E) (<18,0,A>, A) (<18,0,B>, 1 + A) (<18,0,C>, 1 + A) (<18,0,D>, 1 + A) (<18,0,E>, B) (<19,0,A>, A) (<19,0,B>, B) (<19,0,C>, C) (<19,0,D>, D) (<19,0,E>, E) (<20,0,A>, A) (<20,0,B>, 1 + A) (<20,0,C>, 1 + A) (<20,0,D>, 1 + A) (<20,0,E>, B) (<21,0,A>, A) (<21,0,B>, 1 + A) (<21,0,C>, 1 + A) (<21,0,D>, A) (<21,0,E>, B) + Applied Processor: ChainProcessor False [3,5,11,12,13,14,15,16,17,18,19,20,21] + Details: We chained rule 3 to obtain the rules [22] . * Step 13: UnreachableRules WORST_CASE(?,O(n^3)) + Considered Problem: Rules: 5. m5(A,B,C,D,E) -> n2(A,B,C,D,E) True (?,1) 11. n20(A,B,C,D,E) -> m4(A,B,C,D,E) True (?,1) 12. n21(A,B,C,D,E) -> m2(A,0,C,D,E) True (?,1) 13. n2(A,B,C,D,E) -> c2(n20(A,B,F,D,E),n21(A,B,F,D,E)) [B >= F && 1 + C >= F && F >= 1 + C && B >= E && E >= B && 1 + D >= F && F >= 1 + D] (?,1) 14. n30(A,B,C,D,E) -> m2(A,B,C,D,E) True (?,1) 15. n31(A,B,C,D,E) -> m0(A,0,C,D,E) True (?,1) 16. n3(A,B,C,D,E) -> c2(n30(A,F,C,D,E),n31(A,F,C,D,E)) [F >= 1 && A >= F && 1 + C >= F && F >= 1 + C && 1 + B >= F && F >= 1 + B && A >= D && D >= A] (?,1) 17. m7(A,B,C,D,E) -> c2(m8(F,G,0,D,E),m4(F,G,0,D,E)) [B >= G && G >= B && A >= F && F >= A] (1,1) 18. n4(A,B,C,D,E) -> m0(A,F,C,D,E) [F >= 1 && A >= F && 1 + B >= F && F >= 1 + B && 1 + C >= F && F >= 1 + C && A >= D && D >= A] (?,1) 19. multiply(A,B,C,D,E) -> m7(A,B,C,D,E) True (1,2) 20. m0(A,B,C,D,E) -> n4(A,B,F,G,E) [A >= 1 && F >= 0 && A >= F && A >= G && G >= A && B >= F && F >= B] (?,2) 21. m2(A,B,C,D,E) -> n3(A,B,F,G,E) [F >= 0 && A >= G && G >= A && B >= F && F >= B] (?,2) 22. m4(A,B,C,D,E) -> n2(A,B,C,F,G) [B >= G && G >= B && C >= F && F >= C] (?,2) Signature: {(m0,5) ;(m1,5) ;(m2,5) ;(m3,5) ;(m4,5) ;(m5,5) ;(m6,5) ;(m7,5) ;(m8,5) ;(m9,5) ;(multiply,5) ;(n0,5) ;(n1,5) ;(n2,5) ;(n20,5) ;(n21,5) ;(n3,5) ;(n30,5) ;(n31,5) ;(n4,5)} Flow Graph: [5->{13},11->{22},12->{21},13->{11,12},14->{21},15->{20},16->{14,15},17->{22},18->{20},19->{17},20->{18} ,21->{16},22->{13}] Sizebounds: (< 5,0,A>, A) (< 5,0,B>, B) (< 5,0,C>, ?) (< 5,0,D>, ?) (< 5,0,E>, B) (<11,0,A>, A) (<11,0,B>, B) (<11,0,C>, ?) (<11,0,D>, ?) (<11,0,E>, B) (<12,0,A>, A) (<12,0,B>, 0) (<12,0,C>, ?) (<12,0,D>, ?) (<12,0,E>, B) (<13,0,A>, A) (<13,0,B>, B) (<13,0,C>, ?) (<13,0,D>, ?) (<13,0,E>, B) (<13,1,A>, A) (<13,1,B>, B) (<13,1,C>, ?) (<13,1,D>, ?) (<13,1,E>, B) (<14,0,A>, A) (<14,0,B>, 1 + A) (<14,0,C>, 1 + A) (<14,0,D>, A) (<14,0,E>, B) (<15,0,A>, A) (<15,0,B>, 0) (<15,0,C>, 1 + A) (<15,0,D>, A) (<15,0,E>, B) (<16,0,A>, A) (<16,0,B>, 1 + A) (<16,0,C>, 1 + A) (<16,0,D>, A) (<16,0,E>, B) (<16,1,A>, A) (<16,1,B>, 1 + A) (<16,1,C>, 1 + A) (<16,1,D>, A) (<16,1,E>, B) (<17,0,A>, A) (<17,0,B>, B) (<17,0,C>, 0) (<17,0,D>, D) (<17,0,E>, E) (<17,1,A>, A) (<17,1,B>, B) (<17,1,C>, 0) (<17,1,D>, D) (<17,1,E>, E) (<18,0,A>, A) (<18,0,B>, 1 + A) (<18,0,C>, 1 + A) (<18,0,D>, 1 + A) (<18,0,E>, B) (<19,0,A>, A) (<19,0,B>, B) (<19,0,C>, C) (<19,0,D>, D) (<19,0,E>, E) (<20,0,A>, A) (<20,0,B>, 1 + A) (<20,0,C>, 1 + A) (<20,0,D>, 1 + A) (<20,0,E>, B) (<21,0,A>, A) (<21,0,B>, 1 + A) (<21,0,C>, 1 + A) (<21,0,D>, A) (<21,0,E>, B) (<22,0,A>, A) (<22,0,B>, B) (<22,0,C>, ?) (<22,0,D>, ?) (<22,0,E>, B) + Applied Processor: UnreachableRules + Details: The following transitions are not reachable from the starting states and are removed: [5] * Step 14: ChainProcessor WORST_CASE(?,O(n^3)) + Considered Problem: Rules: 11. n20(A,B,C,D,E) -> m4(A,B,C,D,E) True (?,1) 12. n21(A,B,C,D,E) -> m2(A,0,C,D,E) True (?,1) 13. n2(A,B,C,D,E) -> c2(n20(A,B,F,D,E),n21(A,B,F,D,E)) [B >= F && 1 + C >= F && F >= 1 + C && B >= E && E >= B && 1 + D >= F && F >= 1 + D] (?,1) 14. n30(A,B,C,D,E) -> m2(A,B,C,D,E) True (?,1) 15. n31(A,B,C,D,E) -> m0(A,0,C,D,E) True (?,1) 16. n3(A,B,C,D,E) -> c2(n30(A,F,C,D,E),n31(A,F,C,D,E)) [F >= 1 && A >= F && 1 + C >= F && F >= 1 + C && 1 + B >= F && F >= 1 + B && A >= D && D >= A] (?,1) 17. m7(A,B,C,D,E) -> c2(m8(F,G,0,D,E),m4(F,G,0,D,E)) [B >= G && G >= B && A >= F && F >= A] (1,1) 18. n4(A,B,C,D,E) -> m0(A,F,C,D,E) [F >= 1 && A >= F && 1 + B >= F && F >= 1 + B && 1 + C >= F && F >= 1 + C && A >= D && D >= A] (?,1) 19. multiply(A,B,C,D,E) -> m7(A,B,C,D,E) True (1,2) 20. m0(A,B,C,D,E) -> n4(A,B,F,G,E) [A >= 1 && F >= 0 && A >= F && A >= G && G >= A && B >= F && F >= B] (?,2) 21. m2(A,B,C,D,E) -> n3(A,B,F,G,E) [F >= 0 && A >= G && G >= A && B >= F && F >= B] (?,2) 22. m4(A,B,C,D,E) -> n2(A,B,C,F,G) [B >= G && G >= B && C >= F && F >= C] (?,2) Signature: {(m0,5) ;(m1,5) ;(m2,5) ;(m3,5) ;(m4,5) ;(m5,5) ;(m6,5) ;(m7,5) ;(m8,5) ;(m9,5) ;(multiply,5) ;(n0,5) ;(n1,5) ;(n2,5) ;(n20,5) ;(n21,5) ;(n3,5) ;(n30,5) ;(n31,5) ;(n4,5)} Flow Graph: [11->{22},12->{21},13->{11,12},14->{21},15->{20},16->{14,15},17->{22},18->{20},19->{17},20->{18},21->{16} ,22->{13}] Sizebounds: (<11,0,A>, A) (<11,0,B>, B) (<11,0,C>, ?) (<11,0,D>, ?) (<11,0,E>, B) (<12,0,A>, A) (<12,0,B>, 0) (<12,0,C>, ?) (<12,0,D>, ?) (<12,0,E>, B) (<13,0,A>, A) (<13,0,B>, B) (<13,0,C>, ?) (<13,0,D>, ?) (<13,0,E>, B) (<13,1,A>, A) (<13,1,B>, B) (<13,1,C>, ?) (<13,1,D>, ?) (<13,1,E>, B) (<14,0,A>, A) (<14,0,B>, 1 + A) (<14,0,C>, 1 + A) (<14,0,D>, A) (<14,0,E>, B) (<15,0,A>, A) (<15,0,B>, 0) (<15,0,C>, 1 + A) (<15,0,D>, A) (<15,0,E>, B) (<16,0,A>, A) (<16,0,B>, 1 + A) (<16,0,C>, 1 + A) (<16,0,D>, A) (<16,0,E>, B) (<16,1,A>, A) (<16,1,B>, 1 + A) (<16,1,C>, 1 + A) (<16,1,D>, A) (<16,1,E>, B) (<17,0,A>, A) (<17,0,B>, B) (<17,0,C>, 0) (<17,0,D>, D) (<17,0,E>, E) (<17,1,A>, A) (<17,1,B>, B) (<17,1,C>, 0) (<17,1,D>, D) (<17,1,E>, E) (<18,0,A>, A) (<18,0,B>, 1 + A) (<18,0,C>, 1 + A) (<18,0,D>, 1 + A) (<18,0,E>, B) (<19,0,A>, A) (<19,0,B>, B) (<19,0,C>, C) (<19,0,D>, D) (<19,0,E>, E) (<20,0,A>, A) (<20,0,B>, 1 + A) (<20,0,C>, 1 + A) (<20,0,D>, 1 + A) (<20,0,E>, B) (<21,0,A>, A) (<21,0,B>, 1 + A) (<21,0,C>, 1 + A) (<21,0,D>, A) (<21,0,E>, B) (<22,0,A>, A) (<22,0,B>, B) (<22,0,C>, ?) (<22,0,D>, ?) (<22,0,E>, B) + Applied Processor: ChainProcessor False [11,12,13,14,15,16,17,18,19,20,21,22] + Details: We chained rule 11 to obtain the rules [23] . * Step 15: ChainProcessor WORST_CASE(?,O(n^3)) + Considered Problem: Rules: 12. n21(A,B,C,D,E) -> m2(A,0,C,D,E) True (?,1) 13. n2(A,B,C,D,E) -> c2(n20(A,B,F,D,E),n21(A,B,F,D,E)) [B >= F && 1 + C >= F && F >= 1 + C && B >= E && E >= B && 1 + D >= F && F >= 1 + D] (?,1) 14. n30(A,B,C,D,E) -> m2(A,B,C,D,E) True (?,1) 15. n31(A,B,C,D,E) -> m0(A,0,C,D,E) True (?,1) 16. n3(A,B,C,D,E) -> c2(n30(A,F,C,D,E),n31(A,F,C,D,E)) [F >= 1 && A >= F && 1 + C >= F && F >= 1 + C && 1 + B >= F && F >= 1 + B && A >= D && D >= A] (?,1) 17. m7(A,B,C,D,E) -> c2(m8(F,G,0,D,E),m4(F,G,0,D,E)) [B >= G && G >= B && A >= F && F >= A] (1,1) 18. n4(A,B,C,D,E) -> m0(A,F,C,D,E) [F >= 1 && A >= F && 1 + B >= F && F >= 1 + B && 1 + C >= F && F >= 1 + C && A >= D && D >= A] (?,1) 19. multiply(A,B,C,D,E) -> m7(A,B,C,D,E) True (1,2) 20. m0(A,B,C,D,E) -> n4(A,B,F,G,E) [A >= 1 && F >= 0 && A >= F && A >= G && G >= A && B >= F && F >= B] (?,2) 21. m2(A,B,C,D,E) -> n3(A,B,F,G,E) [F >= 0 && A >= G && G >= A && B >= F && F >= B] (?,2) 22. m4(A,B,C,D,E) -> n2(A,B,C,F,G) [B >= G && G >= B && C >= F && F >= C] (?,2) 23. n20(A,B,C,D,E) -> n2(A,B,C,F$,G$) [B >= G$ && G$ >= B && C >= F$ && F$ >= C] (?,3) Signature: {(m0,5) ;(m1,5) ;(m2,5) ;(m3,5) ;(m4,5) ;(m5,5) ;(m6,5) ;(m7,5) ;(m8,5) ;(m9,5) ;(multiply,5) ;(n0,5) ;(n1,5) ;(n2,5) ;(n20,5) ;(n21,5) ;(n3,5) ;(n30,5) ;(n31,5) ;(n4,5)} Flow Graph: [12->{21},13->{12,23},14->{21},15->{20},16->{14,15},17->{22},18->{20},19->{17},20->{18},21->{16},22->{13} ,23->{13}] Sizebounds: (<12,0,A>, A) (<12,0,B>, 0) (<12,0,C>, ?) (<12,0,D>, ?) (<12,0,E>, B) (<13,0,A>, A) (<13,0,B>, B) (<13,0,C>, ?) (<13,0,D>, ?) (<13,0,E>, B) (<13,1,A>, A) (<13,1,B>, B) (<13,1,C>, ?) (<13,1,D>, ?) (<13,1,E>, B) (<14,0,A>, A) (<14,0,B>, 1 + A) (<14,0,C>, 1 + A) (<14,0,D>, A) (<14,0,E>, B) (<15,0,A>, A) (<15,0,B>, 0) (<15,0,C>, 1 + A) (<15,0,D>, A) (<15,0,E>, B) (<16,0,A>, A) (<16,0,B>, 1 + A) (<16,0,C>, 1 + A) (<16,0,D>, A) (<16,0,E>, B) (<16,1,A>, A) (<16,1,B>, 1 + A) (<16,1,C>, 1 + A) (<16,1,D>, A) (<16,1,E>, B) (<17,0,A>, A) (<17,0,B>, B) (<17,0,C>, 0) (<17,0,D>, D) (<17,0,E>, E) (<17,1,A>, A) (<17,1,B>, B) (<17,1,C>, 0) (<17,1,D>, D) (<17,1,E>, E) (<18,0,A>, A) (<18,0,B>, 1 + A) (<18,0,C>, 1 + A) (<18,0,D>, 1 + A) (<18,0,E>, B) (<19,0,A>, A) (<19,0,B>, B) (<19,0,C>, C) (<19,0,D>, D) (<19,0,E>, E) (<20,0,A>, A) (<20,0,B>, 1 + A) (<20,0,C>, 1 + A) (<20,0,D>, 1 + A) (<20,0,E>, B) (<21,0,A>, A) (<21,0,B>, 1 + A) (<21,0,C>, 1 + A) (<21,0,D>, A) (<21,0,E>, B) (<22,0,A>, A) (<22,0,B>, B) (<22,0,C>, ?) (<22,0,D>, ?) (<22,0,E>, B) (<23,0,A>, A) (<23,0,B>, B) (<23,0,C>, ?) (<23,0,D>, ?) (<23,0,E>, B) + Applied Processor: ChainProcessor False [12,13,14,15,16,17,18,19,20,21,22,23] + Details: We chained rule 12 to obtain the rules [24] . * Step 16: ChainProcessor WORST_CASE(?,O(n^3)) + Considered Problem: Rules: 13. n2(A,B,C,D,E) -> c2(n20(A,B,F,D,E),n21(A,B,F,D,E)) [B >= F && 1 + C >= F && F >= 1 + C && B >= E && E >= B && 1 + D >= F && F >= 1 + D] (?,1) 14. n30(A,B,C,D,E) -> m2(A,B,C,D,E) True (?,1) 15. n31(A,B,C,D,E) -> m0(A,0,C,D,E) True (?,1) 16. n3(A,B,C,D,E) -> c2(n30(A,F,C,D,E),n31(A,F,C,D,E)) [F >= 1 && A >= F && 1 + C >= F && F >= 1 + C && 1 + B >= F && F >= 1 + B && A >= D && D >= A] (?,1) 17. m7(A,B,C,D,E) -> c2(m8(F,G,0,D,E),m4(F,G,0,D,E)) [B >= G && G >= B && A >= F && F >= A] (1,1) 18. n4(A,B,C,D,E) -> m0(A,F,C,D,E) [F >= 1 && A >= F && 1 + B >= F && F >= 1 + B && 1 + C >= F && F >= 1 + C && A >= D && D >= A] (?,1) 19. multiply(A,B,C,D,E) -> m7(A,B,C,D,E) True (1,2) 20. m0(A,B,C,D,E) -> n4(A,B,F,G,E) [A >= 1 && F >= 0 && A >= F && A >= G && G >= A && B >= F && F >= B] (?,2) 21. m2(A,B,C,D,E) -> n3(A,B,F,G,E) [F >= 0 && A >= G && G >= A && B >= F && F >= B] (?,2) 22. m4(A,B,C,D,E) -> n2(A,B,C,F,G) [B >= G && G >= B && C >= F && F >= C] (?,2) 23. n20(A,B,C,D,E) -> n2(A,B,C,F$,G$) [B >= G$ && G$ >= B && C >= F$ && F$ >= C] (?,3) 24. n21(A,B,C,D,E) -> n3(A,0,F$,G$,E) [F$ >= 0 && A >= G$ && G$ >= A && 0 >= F$ && F$ >= 0] (?,3) Signature: {(m0,5) ;(m1,5) ;(m2,5) ;(m3,5) ;(m4,5) ;(m5,5) ;(m6,5) ;(m7,5) ;(m8,5) ;(m9,5) ;(multiply,5) ;(n0,5) ;(n1,5) ;(n2,5) ;(n20,5) ;(n21,5) ;(n3,5) ;(n30,5) ;(n31,5) ;(n4,5)} Flow Graph: [13->{23,24},14->{21},15->{20},16->{14,15},17->{22},18->{20},19->{17},20->{18},21->{16},22->{13},23->{13} ,24->{16}] Sizebounds: (<13,0,A>, A) (<13,0,B>, B) (<13,0,C>, ?) (<13,0,D>, ?) (<13,0,E>, B) (<13,1,A>, A) (<13,1,B>, B) (<13,1,C>, ?) (<13,1,D>, ?) (<13,1,E>, B) (<14,0,A>, A) (<14,0,B>, 1 + A) (<14,0,C>, 1 + A) (<14,0,D>, A) (<14,0,E>, B) (<15,0,A>, A) (<15,0,B>, 0) (<15,0,C>, 1 + A) (<15,0,D>, A) (<15,0,E>, B) (<16,0,A>, A) (<16,0,B>, 1 + A) (<16,0,C>, 1 + A) (<16,0,D>, A) (<16,0,E>, B) (<16,1,A>, A) (<16,1,B>, 1 + A) (<16,1,C>, 1 + A) (<16,1,D>, A) (<16,1,E>, B) (<17,0,A>, A) (<17,0,B>, B) (<17,0,C>, 0) (<17,0,D>, D) (<17,0,E>, E) (<17,1,A>, A) (<17,1,B>, B) (<17,1,C>, 0) (<17,1,D>, D) (<17,1,E>, E) (<18,0,A>, A) (<18,0,B>, 1 + A) (<18,0,C>, 1 + A) (<18,0,D>, 1 + A) (<18,0,E>, B) (<19,0,A>, A) (<19,0,B>, B) (<19,0,C>, C) (<19,0,D>, D) (<19,0,E>, E) (<20,0,A>, A) (<20,0,B>, 1 + A) (<20,0,C>, 1 + A) (<20,0,D>, 1 + A) (<20,0,E>, B) (<21,0,A>, A) (<21,0,B>, 1 + A) (<21,0,C>, 1 + A) (<21,0,D>, A) (<21,0,E>, B) (<22,0,A>, A) (<22,0,B>, B) (<22,0,C>, ?) (<22,0,D>, ?) (<22,0,E>, B) (<23,0,A>, A) (<23,0,B>, B) (<23,0,C>, ?) (<23,0,D>, ?) (<23,0,E>, B) (<24,0,A>, A) (<24,0,B>, 1 + A) (<24,0,C>, 1 + A) (<24,0,D>, A) (<24,0,E>, B) + Applied Processor: ChainProcessor False [13,14,15,16,17,18,19,20,21,22,23,24] + Details: We chained rule 13 to obtain the rules [25] . * Step 17: UnreachableRules WORST_CASE(?,O(n^3)) + Considered Problem: Rules: 14. n30(A,B,C,D,E) -> m2(A,B,C,D,E) True (?,1) 15. n31(A,B,C,D,E) -> m0(A,0,C,D,E) True (?,1) 16. n3(A,B,C,D,E) -> c2(n30(A,F,C,D,E),n31(A,F,C,D,E)) [F >= 1 && A >= F && 1 + C >= F && F >= 1 + C && 1 + B >= F && F >= 1 + B && A >= D && D >= A] (?,1) 17. m7(A,B,C,D,E) -> c2(m8(F,G,0,D,E),m4(F,G,0,D,E)) [B >= G && G >= B && A >= F && F >= A] (1,1) 18. n4(A,B,C,D,E) -> m0(A,F,C,D,E) [F >= 1 && A >= F && 1 + B >= F && F >= 1 + B && 1 + C >= F && F >= 1 + C && A >= D && D >= A] (?,1) 19. multiply(A,B,C,D,E) -> m7(A,B,C,D,E) True (1,2) 20. m0(A,B,C,D,E) -> n4(A,B,F,G,E) [A >= 1 && F >= 0 && A >= F && A >= G && G >= A && B >= F && F >= B] (?,2) 21. m2(A,B,C,D,E) -> n3(A,B,F,G,E) [F >= 0 && A >= G && G >= A && B >= F && F >= B] (?,2) 22. m4(A,B,C,D,E) -> n2(A,B,C,F,G) [B >= G && G >= B && C >= F && F >= C] (?,2) 23. n20(A,B,C,D,E) -> n2(A,B,C,F$,G$) [B >= G$ && G$ >= B && C >= F$ && F$ >= C] (?,3) 24. n21(A,B,C,D,E) -> n3(A,0,F$,G$,E) [F$ >= 0 && A >= G$ && G$ >= A && 0 >= F$ && F$ >= 0] (?,3) 25. n2(A,B,C,D,E) -> c2(n2(A,B,F,F$$,G$$),n21(A,B,F,D,E)) [B >= F (?,4) && 1 + C >= F && F >= 1 + C && B >= E && E >= B && 1 + D >= F && F >= 1 + D && B >= G$$ && G$$ >= B && F >= F$$ && F$$ >= F] Signature: {(m0,5) ;(m1,5) ;(m2,5) ;(m3,5) ;(m4,5) ;(m5,5) ;(m6,5) ;(m7,5) ;(m8,5) ;(m9,5) ;(multiply,5) ;(n0,5) ;(n1,5) ;(n2,5) ;(n20,5) ;(n21,5) ;(n3,5) ;(n30,5) ;(n31,5) ;(n4,5)} Flow Graph: [14->{21},15->{20},16->{14,15},17->{22},18->{20},19->{17},20->{18},21->{16},22->{25},23->{25},24->{16} ,25->{24,25}] Sizebounds: (<14,0,A>, A) (<14,0,B>, 1 + A) (<14,0,C>, 1 + A) (<14,0,D>, A) (<14,0,E>, B) (<15,0,A>, A) (<15,0,B>, 0) (<15,0,C>, 1 + A) (<15,0,D>, A) (<15,0,E>, B) (<16,0,A>, A) (<16,0,B>, 1 + A) (<16,0,C>, 1 + A) (<16,0,D>, A) (<16,0,E>, B) (<16,1,A>, A) (<16,1,B>, 1 + A) (<16,1,C>, 1 + A) (<16,1,D>, A) (<16,1,E>, B) (<17,0,A>, A) (<17,0,B>, B) (<17,0,C>, 0) (<17,0,D>, D) (<17,0,E>, E) (<17,1,A>, A) (<17,1,B>, B) (<17,1,C>, 0) (<17,1,D>, D) (<17,1,E>, E) (<18,0,A>, A) (<18,0,B>, 1 + A) (<18,0,C>, 1 + A) (<18,0,D>, 1 + A) (<18,0,E>, B) (<19,0,A>, A) (<19,0,B>, B) (<19,0,C>, C) (<19,0,D>, D) (<19,0,E>, E) (<20,0,A>, A) (<20,0,B>, 1 + A) (<20,0,C>, 1 + A) (<20,0,D>, 1 + A) (<20,0,E>, B) (<21,0,A>, A) (<21,0,B>, 1 + A) (<21,0,C>, 1 + A) (<21,0,D>, A) (<21,0,E>, B) (<22,0,A>, A) (<22,0,B>, B) (<22,0,C>, ?) (<22,0,D>, ?) (<22,0,E>, B) (<23,0,A>, A) (<23,0,B>, B) (<23,0,C>, ?) (<23,0,D>, ?) (<23,0,E>, B) (<24,0,A>, A) (<24,0,B>, 1 + A) (<24,0,C>, 1 + A) (<24,0,D>, A) (<24,0,E>, B) (<25,0,A>, A) (<25,0,B>, B) (<25,0,C>, ?) (<25,0,D>, ?) (<25,0,E>, B) + Applied Processor: UnreachableRules + Details: The following transitions are not reachable from the starting states and are removed: [23] * Step 18: ChainProcessor WORST_CASE(?,O(n^3)) + Considered Problem: Rules: 14. n30(A,B,C,D,E) -> m2(A,B,C,D,E) True (?,1) 15. n31(A,B,C,D,E) -> m0(A,0,C,D,E) True (?,1) 16. n3(A,B,C,D,E) -> c2(n30(A,F,C,D,E),n31(A,F,C,D,E)) [F >= 1 && A >= F && 1 + C >= F && F >= 1 + C && 1 + B >= F && F >= 1 + B && A >= D && D >= A] (?,1) 17. m7(A,B,C,D,E) -> c2(m8(F,G,0,D,E),m4(F,G,0,D,E)) [B >= G && G >= B && A >= F && F >= A] (1,1) 18. n4(A,B,C,D,E) -> m0(A,F,C,D,E) [F >= 1 && A >= F && 1 + B >= F && F >= 1 + B && 1 + C >= F && F >= 1 + C && A >= D && D >= A] (?,1) 19. multiply(A,B,C,D,E) -> m7(A,B,C,D,E) True (1,2) 20. m0(A,B,C,D,E) -> n4(A,B,F,G,E) [A >= 1 && F >= 0 && A >= F && A >= G && G >= A && B >= F && F >= B] (?,2) 21. m2(A,B,C,D,E) -> n3(A,B,F,G,E) [F >= 0 && A >= G && G >= A && B >= F && F >= B] (?,2) 22. m4(A,B,C,D,E) -> n2(A,B,C,F,G) [B >= G && G >= B && C >= F && F >= C] (?,2) 24. n21(A,B,C,D,E) -> n3(A,0,F$,G$,E) [F$ >= 0 && A >= G$ && G$ >= A && 0 >= F$ && F$ >= 0] (?,3) 25. n2(A,B,C,D,E) -> c2(n2(A,B,F,F$$,G$$),n21(A,B,F,D,E)) [B >= F (?,4) && 1 + C >= F && F >= 1 + C && B >= E && E >= B && 1 + D >= F && F >= 1 + D && B >= G$$ && G$$ >= B && F >= F$$ && F$$ >= F] Signature: {(m0,5) ;(m1,5) ;(m2,5) ;(m3,5) ;(m4,5) ;(m5,5) ;(m6,5) ;(m7,5) ;(m8,5) ;(m9,5) ;(multiply,5) ;(n0,5) ;(n1,5) ;(n2,5) ;(n20,5) ;(n21,5) ;(n3,5) ;(n30,5) ;(n31,5) ;(n4,5)} Flow Graph: [14->{21},15->{20},16->{14,15},17->{22},18->{20},19->{17},20->{18},21->{16},22->{25},24->{16},25->{24,25}] Sizebounds: (<14,0,A>, A) (<14,0,B>, 1 + A) (<14,0,C>, 1 + A) (<14,0,D>, A) (<14,0,E>, B) (<15,0,A>, A) (<15,0,B>, 0) (<15,0,C>, 1 + A) (<15,0,D>, A) (<15,0,E>, B) (<16,0,A>, A) (<16,0,B>, 1 + A) (<16,0,C>, 1 + A) (<16,0,D>, A) (<16,0,E>, B) (<16,1,A>, A) (<16,1,B>, 1 + A) (<16,1,C>, 1 + A) (<16,1,D>, A) (<16,1,E>, B) (<17,0,A>, A) (<17,0,B>, B) (<17,0,C>, 0) (<17,0,D>, D) (<17,0,E>, E) (<17,1,A>, A) (<17,1,B>, B) (<17,1,C>, 0) (<17,1,D>, D) (<17,1,E>, E) (<18,0,A>, A) (<18,0,B>, 1 + A) (<18,0,C>, 1 + A) (<18,0,D>, 1 + A) (<18,0,E>, B) (<19,0,A>, A) (<19,0,B>, B) (<19,0,C>, C) (<19,0,D>, D) (<19,0,E>, E) (<20,0,A>, A) (<20,0,B>, 1 + A) (<20,0,C>, 1 + A) (<20,0,D>, 1 + A) (<20,0,E>, B) (<21,0,A>, A) (<21,0,B>, 1 + A) (<21,0,C>, 1 + A) (<21,0,D>, A) (<21,0,E>, B) (<22,0,A>, A) (<22,0,B>, B) (<22,0,C>, ?) (<22,0,D>, ?) (<22,0,E>, B) (<24,0,A>, A) (<24,0,B>, 1 + A) (<24,0,C>, 1 + A) (<24,0,D>, A) (<24,0,E>, B) (<25,0,A>, A) (<25,0,B>, B) (<25,0,C>, ?) (<25,0,D>, ?) (<25,0,E>, B) + Applied Processor: ChainProcessor False [14,15,16,17,18,19,20,21,22,24,25] + Details: We chained rule 14 to obtain the rules [26] . * Step 19: UnreachableRules WORST_CASE(?,O(n^3)) + Considered Problem: Rules: 15. n31(A,B,C,D,E) -> m0(A,0,C,D,E) True (?,1) 16. n3(A,B,C,D,E) -> c2(n30(A,F,C,D,E),n31(A,F,C,D,E)) [F >= 1 && A >= F && 1 + C >= F && F >= 1 + C && 1 + B >= F && F >= 1 + B && A >= D && D >= A] (?,1) 17. m7(A,B,C,D,E) -> c2(m8(F,G,0,D,E),m4(F,G,0,D,E)) [B >= G && G >= B && A >= F && F >= A] (1,1) 18. n4(A,B,C,D,E) -> m0(A,F,C,D,E) [F >= 1 && A >= F && 1 + B >= F && F >= 1 + B && 1 + C >= F && F >= 1 + C && A >= D && D >= A] (?,1) 19. multiply(A,B,C,D,E) -> m7(A,B,C,D,E) True (1,2) 20. m0(A,B,C,D,E) -> n4(A,B,F,G,E) [A >= 1 && F >= 0 && A >= F && A >= G && G >= A && B >= F && F >= B] (?,2) 21. m2(A,B,C,D,E) -> n3(A,B,F,G,E) [F >= 0 && A >= G && G >= A && B >= F && F >= B] (?,2) 22. m4(A,B,C,D,E) -> n2(A,B,C,F,G) [B >= G && G >= B && C >= F && F >= C] (?,2) 24. n21(A,B,C,D,E) -> n3(A,0,F$,G$,E) [F$ >= 0 && A >= G$ && G$ >= A && 0 >= F$ && F$ >= 0] (?,3) 25. n2(A,B,C,D,E) -> c2(n2(A,B,F,F$$,G$$),n21(A,B,F,D,E)) [B >= F (?,4) && 1 + C >= F && F >= 1 + C && B >= E && E >= B && 1 + D >= F && F >= 1 + D && B >= G$$ && G$$ >= B && F >= F$$ && F$$ >= F] 26. n30(A,B,C,D,E) -> n3(A,B,F$,G$,E) [F$ >= 0 && A >= G$ && G$ >= A && B >= F$ && F$ >= B] (?,3) Signature: {(m0,5) ;(m1,5) ;(m2,5) ;(m3,5) ;(m4,5) ;(m5,5) ;(m6,5) ;(m7,5) ;(m8,5) ;(m9,5) ;(multiply,5) ;(n0,5) ;(n1,5) ;(n2,5) ;(n20,5) ;(n21,5) ;(n3,5) ;(n30,5) ;(n31,5) ;(n4,5)} Flow Graph: [15->{20},16->{15,26},17->{22},18->{20},19->{17},20->{18},21->{16},22->{25},24->{16},25->{24,25},26->{16}] Sizebounds: (<15,0,A>, A) (<15,0,B>, 0) (<15,0,C>, 1 + A) (<15,0,D>, A) (<15,0,E>, B) (<16,0,A>, A) (<16,0,B>, 1 + A) (<16,0,C>, 1 + A) (<16,0,D>, A) (<16,0,E>, B) (<16,1,A>, A) (<16,1,B>, 1 + A) (<16,1,C>, 1 + A) (<16,1,D>, A) (<16,1,E>, B) (<17,0,A>, A) (<17,0,B>, B) (<17,0,C>, 0) (<17,0,D>, D) (<17,0,E>, E) (<17,1,A>, A) (<17,1,B>, B) (<17,1,C>, 0) (<17,1,D>, D) (<17,1,E>, E) (<18,0,A>, A) (<18,0,B>, 1 + A) (<18,0,C>, 1 + A) (<18,0,D>, 1 + A) (<18,0,E>, B) (<19,0,A>, A) (<19,0,B>, B) (<19,0,C>, C) (<19,0,D>, D) (<19,0,E>, E) (<20,0,A>, A) (<20,0,B>, 1 + A) (<20,0,C>, 1 + A) (<20,0,D>, 1 + A) (<20,0,E>, B) (<21,0,A>, A) (<21,0,B>, 1 + A) (<21,0,C>, 1 + A) (<21,0,D>, A) (<21,0,E>, B) (<22,0,A>, A) (<22,0,B>, B) (<22,0,C>, ?) (<22,0,D>, ?) (<22,0,E>, B) (<24,0,A>, A) (<24,0,B>, 1 + A) (<24,0,C>, 1 + A) (<24,0,D>, A) (<24,0,E>, B) (<25,0,A>, A) (<25,0,B>, B) (<25,0,C>, ?) (<25,0,D>, ?) (<25,0,E>, B) (<26,0,A>, A) (<26,0,B>, 1 + A) (<26,0,C>, 1 + A) (<26,0,D>, A) (<26,0,E>, B) + Applied Processor: UnreachableRules + Details: The following transitions are not reachable from the starting states and are removed: [21] * Step 20: ChainProcessor WORST_CASE(?,O(n^3)) + Considered Problem: Rules: 15. n31(A,B,C,D,E) -> m0(A,0,C,D,E) True (?,1) 16. n3(A,B,C,D,E) -> c2(n30(A,F,C,D,E),n31(A,F,C,D,E)) [F >= 1 && A >= F && 1 + C >= F && F >= 1 + C && 1 + B >= F && F >= 1 + B && A >= D && D >= A] (?,1) 17. m7(A,B,C,D,E) -> c2(m8(F,G,0,D,E),m4(F,G,0,D,E)) [B >= G && G >= B && A >= F && F >= A] (1,1) 18. n4(A,B,C,D,E) -> m0(A,F,C,D,E) [F >= 1 && A >= F && 1 + B >= F && F >= 1 + B && 1 + C >= F && F >= 1 + C && A >= D && D >= A] (?,1) 19. multiply(A,B,C,D,E) -> m7(A,B,C,D,E) True (1,2) 20. m0(A,B,C,D,E) -> n4(A,B,F,G,E) [A >= 1 && F >= 0 && A >= F && A >= G && G >= A && B >= F && F >= B] (?,2) 22. m4(A,B,C,D,E) -> n2(A,B,C,F,G) [B >= G && G >= B && C >= F && F >= C] (?,2) 24. n21(A,B,C,D,E) -> n3(A,0,F$,G$,E) [F$ >= 0 && A >= G$ && G$ >= A && 0 >= F$ && F$ >= 0] (?,3) 25. n2(A,B,C,D,E) -> c2(n2(A,B,F,F$$,G$$),n21(A,B,F,D,E)) [B >= F (?,4) && 1 + C >= F && F >= 1 + C && B >= E && E >= B && 1 + D >= F && F >= 1 + D && B >= G$$ && G$$ >= B && F >= F$$ && F$$ >= F] 26. n30(A,B,C,D,E) -> n3(A,B,F$,G$,E) [F$ >= 0 && A >= G$ && G$ >= A && B >= F$ && F$ >= B] (?,3) Signature: {(m0,5) ;(m1,5) ;(m2,5) ;(m3,5) ;(m4,5) ;(m5,5) ;(m6,5) ;(m7,5) ;(m8,5) ;(m9,5) ;(multiply,5) ;(n0,5) ;(n1,5) ;(n2,5) ;(n20,5) ;(n21,5) ;(n3,5) ;(n30,5) ;(n31,5) ;(n4,5)} Flow Graph: [15->{20},16->{15,26},17->{22},18->{20},19->{17},20->{18},22->{25},24->{16},25->{24,25},26->{16}] Sizebounds: (<15,0,A>, A) (<15,0,B>, 0) (<15,0,C>, 1 + A) (<15,0,D>, A) (<15,0,E>, B) (<16,0,A>, A) (<16,0,B>, 1 + A) (<16,0,C>, 1 + A) (<16,0,D>, A) (<16,0,E>, B) (<16,1,A>, A) (<16,1,B>, 1 + A) (<16,1,C>, 1 + A) (<16,1,D>, A) (<16,1,E>, B) (<17,0,A>, A) (<17,0,B>, B) (<17,0,C>, 0) (<17,0,D>, D) (<17,0,E>, E) (<17,1,A>, A) (<17,1,B>, B) (<17,1,C>, 0) (<17,1,D>, D) (<17,1,E>, E) (<18,0,A>, A) (<18,0,B>, 1 + A) (<18,0,C>, 1 + A) (<18,0,D>, 1 + A) (<18,0,E>, B) (<19,0,A>, A) (<19,0,B>, B) (<19,0,C>, C) (<19,0,D>, D) (<19,0,E>, E) (<20,0,A>, A) (<20,0,B>, 1 + A) (<20,0,C>, 1 + A) (<20,0,D>, 1 + A) (<20,0,E>, B) (<22,0,A>, A) (<22,0,B>, B) (<22,0,C>, ?) (<22,0,D>, ?) (<22,0,E>, B) (<24,0,A>, A) (<24,0,B>, 1 + A) (<24,0,C>, 1 + A) (<24,0,D>, A) (<24,0,E>, B) (<25,0,A>, A) (<25,0,B>, B) (<25,0,C>, ?) (<25,0,D>, ?) (<25,0,E>, B) (<26,0,A>, A) (<26,0,B>, 1 + A) (<26,0,C>, 1 + A) (<26,0,D>, A) (<26,0,E>, B) + Applied Processor: ChainProcessor False [15,16,17,18,19,20,22,24,25,26] + Details: We chained rule 15 to obtain the rules [27] . * Step 21: ChainProcessor WORST_CASE(?,O(n^3)) + Considered Problem: Rules: 16. n3(A,B,C,D,E) -> c2(n30(A,F,C,D,E),n31(A,F,C,D,E)) [F >= 1 && A >= F && 1 + C >= F && F >= 1 + C && 1 + B >= F && F >= 1 + B && A >= D && D >= A] (?,1) 17. m7(A,B,C,D,E) -> c2(m8(F,G,0,D,E),m4(F,G,0,D,E)) [B >= G && G >= B && A >= F && F >= A] (1,1) 18. n4(A,B,C,D,E) -> m0(A,F,C,D,E) [F >= 1 && A >= F && 1 + B >= F && F >= 1 + B && 1 + C >= F && F >= 1 + C && A >= D && D >= A] (?,1) 19. multiply(A,B,C,D,E) -> m7(A,B,C,D,E) True (1,2) 20. m0(A,B,C,D,E) -> n4(A,B,F,G,E) [A >= 1 && F >= 0 && A >= F && A >= G && G >= A && B >= F && F >= B] (?,2) 22. m4(A,B,C,D,E) -> n2(A,B,C,F,G) [B >= G && G >= B && C >= F && F >= C] (?,2) 24. n21(A,B,C,D,E) -> n3(A,0,F$,G$,E) [F$ >= 0 && A >= G$ && G$ >= A && 0 >= F$ && F$ >= 0] (?,3) 25. n2(A,B,C,D,E) -> c2(n2(A,B,F,F$$,G$$),n21(A,B,F,D,E)) [B >= F (?,4) && 1 + C >= F && F >= 1 + C && B >= E && E >= B && 1 + D >= F && F >= 1 + D && B >= G$$ && G$$ >= B && F >= F$$ && F$$ >= F] 26. n30(A,B,C,D,E) -> n3(A,B,F$,G$,E) [F$ >= 0 && A >= G$ && G$ >= A && B >= F$ && F$ >= B] (?,3) 27. n31(A,B,C,D,E) -> n4(A,0,F$,G$,E) [A >= 1 && F$ >= 0 && A >= F$ && A >= G$ && G$ >= A && 0 >= F$ && F$ >= 0] (?,3) Signature: {(m0,5) ;(m1,5) ;(m2,5) ;(m3,5) ;(m4,5) ;(m5,5) ;(m6,5) ;(m7,5) ;(m8,5) ;(m9,5) ;(multiply,5) ;(n0,5) ;(n1,5) ;(n2,5) ;(n20,5) ;(n21,5) ;(n3,5) ;(n30,5) ;(n31,5) ;(n4,5)} Flow Graph: [16->{26,27},17->{22},18->{20},19->{17},20->{18},22->{25},24->{16},25->{24,25},26->{16},27->{18}] Sizebounds: (<16,0,A>, A) (<16,0,B>, 1 + A) (<16,0,C>, 1 + A) (<16,0,D>, A) (<16,0,E>, B) (<16,1,A>, A) (<16,1,B>, 1 + A) (<16,1,C>, 1 + A) (<16,1,D>, A) (<16,1,E>, B) (<17,0,A>, A) (<17,0,B>, B) (<17,0,C>, 0) (<17,0,D>, D) (<17,0,E>, E) (<17,1,A>, A) (<17,1,B>, B) (<17,1,C>, 0) (<17,1,D>, D) (<17,1,E>, E) (<18,0,A>, A) (<18,0,B>, 1 + A) (<18,0,C>, 1 + A) (<18,0,D>, 1 + A) (<18,0,E>, B) (<19,0,A>, A) (<19,0,B>, B) (<19,0,C>, C) (<19,0,D>, D) (<19,0,E>, E) (<20,0,A>, A) (<20,0,B>, 1 + A) (<20,0,C>, 1 + A) (<20,0,D>, 1 + A) (<20,0,E>, B) (<22,0,A>, A) (<22,0,B>, B) (<22,0,C>, ?) (<22,0,D>, ?) (<22,0,E>, B) (<24,0,A>, A) (<24,0,B>, 1 + A) (<24,0,C>, 1 + A) (<24,0,D>, A) (<24,0,E>, B) (<25,0,A>, A) (<25,0,B>, B) (<25,0,C>, ?) (<25,0,D>, ?) (<25,0,E>, B) (<26,0,A>, A) (<26,0,B>, 1 + A) (<26,0,C>, 1 + A) (<26,0,D>, A) (<26,0,E>, B) (<27,0,A>, A) (<27,0,B>, 1 + A) (<27,0,C>, 1 + A) (<27,0,D>, 1 + A) (<27,0,E>, B) + Applied Processor: ChainProcessor False [16,17,18,19,20,22,24,25,26,27] + Details: We chained rule 16 to obtain the rules [28] . * Step 22: UnreachableRules WORST_CASE(?,O(n^3)) + Considered Problem: Rules: 17. m7(A,B,C,D,E) -> c2(m8(F,G,0,D,E),m4(F,G,0,D,E)) [B >= G && G >= B && A >= F && F >= A] (1,1) 18. n4(A,B,C,D,E) -> m0(A,F,C,D,E) [F >= 1 && A >= F && 1 + B >= F && F >= 1 + B && 1 + C >= F && F >= 1 + C && A >= D && D >= A] (?,1) 19. multiply(A,B,C,D,E) -> m7(A,B,C,D,E) True (1,2) 20. m0(A,B,C,D,E) -> n4(A,B,F,G,E) [A >= 1 && F >= 0 && A >= F && A >= G && G >= A && B >= F && F >= B] (?,2) 22. m4(A,B,C,D,E) -> n2(A,B,C,F,G) [B >= G && G >= B && C >= F && F >= C] (?,2) 24. n21(A,B,C,D,E) -> n3(A,0,F$,G$,E) [F$ >= 0 && A >= G$ && G$ >= A && 0 >= F$ && F$ >= 0] (?,3) 25. n2(A,B,C,D,E) -> c2(n2(A,B,F,F$$,G$$),n21(A,B,F,D,E)) [B >= F (?,4) && 1 + C >= F && F >= 1 + C && B >= E && E >= B && 1 + D >= F && F >= 1 + D && B >= G$$ && G$$ >= B && F >= F$$ && F$$ >= F] 26. n30(A,B,C,D,E) -> n3(A,B,F$,G$,E) [F$ >= 0 && A >= G$ && G$ >= A && B >= F$ && F$ >= B] (?,3) 27. n31(A,B,C,D,E) -> n4(A,0,F$,G$,E) [A >= 1 && F$ >= 0 && A >= F$ && A >= G$ && G$ >= A && 0 >= F$ && F$ >= 0] (?,3) 28. n3(A,B,C,D,E) -> c2(n3(A,F,F$$,G$$,E),n31(A,F,C,D,E)) [F >= 1 (?,4) && A >= F && 1 + C >= F && F >= 1 + C && 1 + B >= F && F >= 1 + B && A >= D && D >= A && F$$ >= 0 && A >= G$$ && G$$ >= A && F >= F$$ && F$$ >= F] Signature: {(m0,5) ;(m1,5) ;(m2,5) ;(m3,5) ;(m4,5) ;(m5,5) ;(m6,5) ;(m7,5) ;(m8,5) ;(m9,5) ;(multiply,5) ;(n0,5) ;(n1,5) ;(n2,5) ;(n20,5) ;(n21,5) ;(n3,5) ;(n30,5) ;(n31,5) ;(n4,5)} Flow Graph: [17->{22},18->{20},19->{17},20->{18},22->{25},24->{28},25->{24,25},26->{28},27->{18},28->{27,28}] Sizebounds: (<17,0,A>, A) (<17,0,B>, B) (<17,0,C>, 0) (<17,0,D>, D) (<17,0,E>, E) (<17,1,A>, A) (<17,1,B>, B) (<17,1,C>, 0) (<17,1,D>, D) (<17,1,E>, E) (<18,0,A>, A) (<18,0,B>, 1 + A) (<18,0,C>, 1 + A) (<18,0,D>, 1 + A) (<18,0,E>, B) (<19,0,A>, A) (<19,0,B>, B) (<19,0,C>, C) (<19,0,D>, D) (<19,0,E>, E) (<20,0,A>, A) (<20,0,B>, 1 + A) (<20,0,C>, 1 + A) (<20,0,D>, 1 + A) (<20,0,E>, B) (<22,0,A>, A) (<22,0,B>, B) (<22,0,C>, ?) (<22,0,D>, ?) (<22,0,E>, B) (<24,0,A>, A) (<24,0,B>, 1 + A) (<24,0,C>, 1 + A) (<24,0,D>, A) (<24,0,E>, B) (<25,0,A>, A) (<25,0,B>, B) (<25,0,C>, ?) (<25,0,D>, ?) (<25,0,E>, B) (<26,0,A>, A) (<26,0,B>, 1 + A) (<26,0,C>, 1 + A) (<26,0,D>, A) (<26,0,E>, B) (<27,0,A>, A) (<27,0,B>, 1 + A) (<27,0,C>, 1 + A) (<27,0,D>, 1 + A) (<27,0,E>, B) (<28,0,A>, A) (<28,0,B>, 1 + A) (<28,0,C>, 1 + A) (<28,0,D>, A) (<28,0,E>, B) + Applied Processor: UnreachableRules + Details: The following transitions are not reachable from the starting states and are removed: [26] * Step 23: ChainProcessor WORST_CASE(?,O(n^3)) + Considered Problem: Rules: 17. m7(A,B,C,D,E) -> c2(m8(F,G,0,D,E),m4(F,G,0,D,E)) [B >= G && G >= B && A >= F && F >= A] (1,1) 18. n4(A,B,C,D,E) -> m0(A,F,C,D,E) [F >= 1 && A >= F && 1 + B >= F && F >= 1 + B && 1 + C >= F && F >= 1 + C && A >= D && D >= A] (?,1) 19. multiply(A,B,C,D,E) -> m7(A,B,C,D,E) True (1,2) 20. m0(A,B,C,D,E) -> n4(A,B,F,G,E) [A >= 1 && F >= 0 && A >= F && A >= G && G >= A && B >= F && F >= B] (?,2) 22. m4(A,B,C,D,E) -> n2(A,B,C,F,G) [B >= G && G >= B && C >= F && F >= C] (?,2) 24. n21(A,B,C,D,E) -> n3(A,0,F$,G$,E) [F$ >= 0 && A >= G$ && G$ >= A && 0 >= F$ && F$ >= 0] (?,3) 25. n2(A,B,C,D,E) -> c2(n2(A,B,F,F$$,G$$),n21(A,B,F,D,E)) [B >= F (?,4) && 1 + C >= F && F >= 1 + C && B >= E && E >= B && 1 + D >= F && F >= 1 + D && B >= G$$ && G$$ >= B && F >= F$$ && F$$ >= F] 27. n31(A,B,C,D,E) -> n4(A,0,F$,G$,E) [A >= 1 && F$ >= 0 && A >= F$ && A >= G$ && G$ >= A && 0 >= F$ && F$ >= 0] (?,3) 28. n3(A,B,C,D,E) -> c2(n3(A,F,F$$,G$$,E),n31(A,F,C,D,E)) [F >= 1 (?,4) && A >= F && 1 + C >= F && F >= 1 + C && 1 + B >= F && F >= 1 + B && A >= D && D >= A && F$$ >= 0 && A >= G$$ && G$$ >= A && F >= F$$ && F$$ >= F] Signature: {(m0,5) ;(m1,5) ;(m2,5) ;(m3,5) ;(m4,5) ;(m5,5) ;(m6,5) ;(m7,5) ;(m8,5) ;(m9,5) ;(multiply,5) ;(n0,5) ;(n1,5) ;(n2,5) ;(n20,5) ;(n21,5) ;(n3,5) ;(n30,5) ;(n31,5) ;(n4,5)} Flow Graph: [17->{22},18->{20},19->{17},20->{18},22->{25},24->{28},25->{24,25},27->{18},28->{27,28}] Sizebounds: (<17,0,A>, A) (<17,0,B>, B) (<17,0,C>, 0) (<17,0,D>, D) (<17,0,E>, E) (<17,1,A>, A) (<17,1,B>, B) (<17,1,C>, 0) (<17,1,D>, D) (<17,1,E>, E) (<18,0,A>, A) (<18,0,B>, 1 + A) (<18,0,C>, 1 + A) (<18,0,D>, 1 + A) (<18,0,E>, B) (<19,0,A>, A) (<19,0,B>, B) (<19,0,C>, C) (<19,0,D>, D) (<19,0,E>, E) (<20,0,A>, A) (<20,0,B>, 1 + A) (<20,0,C>, 1 + A) (<20,0,D>, 1 + A) (<20,0,E>, B) (<22,0,A>, A) (<22,0,B>, B) (<22,0,C>, ?) (<22,0,D>, ?) (<22,0,E>, B) (<24,0,A>, A) (<24,0,B>, 1 + A) (<24,0,C>, 1 + A) (<24,0,D>, A) (<24,0,E>, B) (<25,0,A>, A) (<25,0,B>, B) (<25,0,C>, ?) (<25,0,D>, ?) (<25,0,E>, B) (<27,0,A>, A) (<27,0,B>, 1 + A) (<27,0,C>, 1 + A) (<27,0,D>, 1 + A) (<27,0,E>, B) (<28,0,A>, A) (<28,0,B>, 1 + A) (<28,0,C>, 1 + A) (<28,0,D>, A) (<28,0,E>, B) + Applied Processor: ChainProcessor False [17,18,19,20,22,24,25,27,28] + Details: We chained rule 17 to obtain the rules [29] . * Step 24: UnreachableRules WORST_CASE(?,O(n^3)) + Considered Problem: Rules: 18. n4(A,B,C,D,E) -> m0(A,F,C,D,E) [F >= 1 && A >= F && 1 + B >= F && F >= 1 + B && 1 + C >= F && F >= 1 + C && A >= D && D >= A] (?,1) 19. multiply(A,B,C,D,E) -> m7(A,B,C,D,E) True (1,2) 20. m0(A,B,C,D,E) -> n4(A,B,F,G,E) [A >= 1 && F >= 0 && A >= F && A >= G && G >= A && B >= F && F >= B] (?,2) 22. m4(A,B,C,D,E) -> n2(A,B,C,F,G) [B >= G && G >= B && C >= F && F >= C] (?,2) 24. n21(A,B,C,D,E) -> n3(A,0,F$,G$,E) [F$ >= 0 && A >= G$ && G$ >= A && 0 >= F$ && F$ >= 0] (?,3) 25. n2(A,B,C,D,E) -> c2(n2(A,B,F,F$$,G$$),n21(A,B,F,D,E)) [B >= F (?,4) && 1 + C >= F && F >= 1 + C && B >= E && E >= B && 1 + D >= F && F >= 1 + D && B >= G$$ && G$$ >= B && F >= F$$ && F$$ >= F] 27. n31(A,B,C,D,E) -> n4(A,0,F$,G$,E) [A >= 1 && F$ >= 0 && A >= F$ && A >= G$ && G$ >= A && 0 >= F$ && F$ >= 0] (?,3) 28. n3(A,B,C,D,E) -> c2(n3(A,F,F$$,G$$,E),n31(A,F,C,D,E)) [F >= 1 (?,4) && A >= F && 1 + C >= F && F >= 1 + C && 1 + B >= F && F >= 1 + B && A >= D && D >= A && F$$ >= 0 && A >= G$$ && G$$ >= A && F >= F$$ && F$$ >= F] 29. m7(A,B,C,D,E) -> c2(m8(F,G,0,D,E),n2(F,G,0,F$,G$)) [B >= G && G >= B && A >= F && F >= A && G >= G$ && G$ >= G && 0 >= F$ && F$ >= 0] (1,3) Signature: {(m0,5) ;(m1,5) ;(m2,5) ;(m3,5) ;(m4,5) ;(m5,5) ;(m6,5) ;(m7,5) ;(m8,5) ;(m9,5) ;(multiply,5) ;(n0,5) ;(n1,5) ;(n2,5) ;(n20,5) ;(n21,5) ;(n3,5) ;(n30,5) ;(n31,5) ;(n4,5)} Flow Graph: [18->{20},19->{29},20->{18},22->{25},24->{28},25->{24,25},27->{18},28->{27,28},29->{25}] Sizebounds: (<18,0,A>, A) (<18,0,B>, 1 + A) (<18,0,C>, 1 + A) (<18,0,D>, 1 + A) (<18,0,E>, B) (<19,0,A>, A) (<19,0,B>, B) (<19,0,C>, C) (<19,0,D>, D) (<19,0,E>, E) (<20,0,A>, A) (<20,0,B>, 1 + A) (<20,0,C>, 1 + A) (<20,0,D>, 1 + A) (<20,0,E>, B) (<22,0,A>, A) (<22,0,B>, B) (<22,0,C>, ?) (<22,0,D>, ?) (<22,0,E>, B) (<24,0,A>, A) (<24,0,B>, 1 + A) (<24,0,C>, 1 + A) (<24,0,D>, A) (<24,0,E>, B) (<25,0,A>, A) (<25,0,B>, B) (<25,0,C>, ?) (<25,0,D>, ?) (<25,0,E>, B) (<27,0,A>, A) (<27,0,B>, 1 + A) (<27,0,C>, 1 + A) (<27,0,D>, 1 + A) (<27,0,E>, B) (<28,0,A>, A) (<28,0,B>, 1 + A) (<28,0,C>, 1 + A) (<28,0,D>, A) (<28,0,E>, B) (<29,0,A>, A) (<29,0,B>, B) (<29,0,C>, ?) (<29,0,D>, ?) (<29,0,E>, B) + Applied Processor: UnreachableRules + Details: The following transitions are not reachable from the starting states and are removed: [22] * Step 25: ChainProcessor WORST_CASE(?,O(n^3)) + Considered Problem: Rules: 18. n4(A,B,C,D,E) -> m0(A,F,C,D,E) [F >= 1 && A >= F && 1 + B >= F && F >= 1 + B && 1 + C >= F && F >= 1 + C && A >= D && D >= A] (?,1) 19. multiply(A,B,C,D,E) -> m7(A,B,C,D,E) True (1,2) 20. m0(A,B,C,D,E) -> n4(A,B,F,G,E) [A >= 1 && F >= 0 && A >= F && A >= G && G >= A && B >= F && F >= B] (?,2) 24. n21(A,B,C,D,E) -> n3(A,0,F$,G$,E) [F$ >= 0 && A >= G$ && G$ >= A && 0 >= F$ && F$ >= 0] (?,3) 25. n2(A,B,C,D,E) -> c2(n2(A,B,F,F$$,G$$),n21(A,B,F,D,E)) [B >= F (?,4) && 1 + C >= F && F >= 1 + C && B >= E && E >= B && 1 + D >= F && F >= 1 + D && B >= G$$ && G$$ >= B && F >= F$$ && F$$ >= F] 27. n31(A,B,C,D,E) -> n4(A,0,F$,G$,E) [A >= 1 && F$ >= 0 && A >= F$ && A >= G$ && G$ >= A && 0 >= F$ && F$ >= 0] (?,3) 28. n3(A,B,C,D,E) -> c2(n3(A,F,F$$,G$$,E),n31(A,F,C,D,E)) [F >= 1 (?,4) && A >= F && 1 + C >= F && F >= 1 + C && 1 + B >= F && F >= 1 + B && A >= D && D >= A && F$$ >= 0 && A >= G$$ && G$$ >= A && F >= F$$ && F$$ >= F] 29. m7(A,B,C,D,E) -> c2(m8(F,G,0,D,E),n2(F,G,0,F$,G$)) [B >= G && G >= B && A >= F && F >= A && G >= G$ && G$ >= G && 0 >= F$ && F$ >= 0] (1,3) Signature: {(m0,5) ;(m1,5) ;(m2,5) ;(m3,5) ;(m4,5) ;(m5,5) ;(m6,5) ;(m7,5) ;(m8,5) ;(m9,5) ;(multiply,5) ;(n0,5) ;(n1,5) ;(n2,5) ;(n20,5) ;(n21,5) ;(n3,5) ;(n30,5) ;(n31,5) ;(n4,5)} Flow Graph: [18->{20},19->{29},20->{18},24->{28},25->{24,25},27->{18},28->{27,28},29->{25}] Sizebounds: (<18,0,A>, A) (<18,0,B>, 1 + A) (<18,0,C>, 1 + A) (<18,0,D>, 1 + A) (<18,0,E>, B) (<19,0,A>, A) (<19,0,B>, B) (<19,0,C>, C) (<19,0,D>, D) (<19,0,E>, E) (<20,0,A>, A) (<20,0,B>, 1 + A) (<20,0,C>, 1 + A) (<20,0,D>, 1 + A) (<20,0,E>, B) (<24,0,A>, A) (<24,0,B>, 1 + A) (<24,0,C>, 1 + A) (<24,0,D>, A) (<24,0,E>, B) (<25,0,A>, A) (<25,0,B>, B) (<25,0,C>, ?) (<25,0,D>, ?) (<25,0,E>, B) (<27,0,A>, A) (<27,0,B>, 1 + A) (<27,0,C>, 1 + A) (<27,0,D>, 1 + A) (<27,0,E>, B) (<28,0,A>, A) (<28,0,B>, 1 + A) (<28,0,C>, 1 + A) (<28,0,D>, A) (<28,0,E>, B) (<29,0,A>, A) (<29,0,B>, B) (<29,0,C>, ?) (<29,0,D>, ?) (<29,0,E>, B) + Applied Processor: ChainProcessor False [18,19,20,24,25,27,28,29] + Details: We chained rule 18 to obtain the rules [30] . * Step 26: UnreachableRules WORST_CASE(?,O(n^3)) + Considered Problem: Rules: 19. multiply(A,B,C,D,E) -> m7(A,B,C,D,E) True (1,2) 20. m0(A,B,C,D,E) -> n4(A,B,F,G,E) [A >= 1 && F >= 0 && A >= F && A >= G && G >= A && B >= F && F >= B] (?,2) 24. n21(A,B,C,D,E) -> n3(A,0,F$,G$,E) [F$ >= 0 && A >= G$ && G$ >= A && 0 >= F$ && F$ >= 0] (?,3) 25. n2(A,B,C,D,E) -> c2(n2(A,B,F,F$$,G$$),n21(A,B,F,D,E)) [B >= F (?,4) && 1 + C >= F && F >= 1 + C && B >= E && E >= B && 1 + D >= F && F >= 1 + D && B >= G$$ && G$$ >= B && F >= F$$ && F$$ >= F] 27. n31(A,B,C,D,E) -> n4(A,0,F$,G$,E) [A >= 1 && F$ >= 0 && A >= F$ && A >= G$ && G$ >= A && 0 >= F$ && F$ >= 0] (?,3) 28. n3(A,B,C,D,E) -> c2(n3(A,F,F$$,G$$,E),n31(A,F,C,D,E)) [F >= 1 (?,4) && A >= F && 1 + C >= F && F >= 1 + C && 1 + B >= F && F >= 1 + B && A >= D && D >= A && F$$ >= 0 && A >= G$$ && G$$ >= A && F >= F$$ && F$$ >= F] 29. m7(A,B,C,D,E) -> c2(m8(F,G,0,D,E),n2(F,G,0,F$,G$)) [B >= G && G >= B && A >= F && F >= A && G >= G$ && G$ >= G && 0 >= F$ && F$ >= 0] (1,3) 30. n4(A,B,C,D,E) -> n4(A,F,F$,G$,E) [F >= 1 (?,3) && A >= F && 1 + B >= F && F >= 1 + B && 1 + C >= F && F >= 1 + C && A >= D && D >= A && A >= 1 && F$ >= 0 && A >= F$ && A >= G$ && G$ >= A && F >= F$ && F$ >= F] Signature: {(m0,5) ;(m1,5) ;(m2,5) ;(m3,5) ;(m4,5) ;(m5,5) ;(m6,5) ;(m7,5) ;(m8,5) ;(m9,5) ;(multiply,5) ;(n0,5) ;(n1,5) ;(n2,5) ;(n20,5) ;(n21,5) ;(n3,5) ;(n30,5) ;(n31,5) ;(n4,5)} Flow Graph: [19->{29},20->{30},24->{28},25->{24,25},27->{30},28->{27,28},29->{25},30->{30}] Sizebounds: (<19,0,A>, A) (<19,0,B>, B) (<19,0,C>, C) (<19,0,D>, D) (<19,0,E>, E) (<20,0,A>, A) (<20,0,B>, 1 + A) (<20,0,C>, 1 + A) (<20,0,D>, 1 + A) (<20,0,E>, B) (<24,0,A>, A) (<24,0,B>, 1 + A) (<24,0,C>, 1 + A) (<24,0,D>, A) (<24,0,E>, B) (<25,0,A>, A) (<25,0,B>, B) (<25,0,C>, ?) (<25,0,D>, ?) (<25,0,E>, B) (<27,0,A>, A) (<27,0,B>, 1 + A) (<27,0,C>, 1 + A) (<27,0,D>, 1 + A) (<27,0,E>, B) (<28,0,A>, A) (<28,0,B>, 1 + A) (<28,0,C>, 1 + A) (<28,0,D>, A) (<28,0,E>, B) (<29,0,A>, A) (<29,0,B>, B) (<29,0,C>, ?) (<29,0,D>, ?) (<29,0,E>, B) (<30,0,A>, A) (<30,0,B>, 1 + A) (<30,0,C>, 1 + A) (<30,0,D>, 1 + A) (<30,0,E>, B) + Applied Processor: UnreachableRules + Details: The following transitions are not reachable from the starting states and are removed: [20] * Step 27: ChainProcessor WORST_CASE(?,O(n^3)) + Considered Problem: Rules: 19. multiply(A,B,C,D,E) -> m7(A,B,C,D,E) True (1,2) 24. n21(A,B,C,D,E) -> n3(A,0,F$,G$,E) [F$ >= 0 && A >= G$ && G$ >= A && 0 >= F$ && F$ >= 0] (?,3) 25. n2(A,B,C,D,E) -> c2(n2(A,B,F,F$$,G$$),n21(A,B,F,D,E)) [B >= F (?,4) && 1 + C >= F && F >= 1 + C && B >= E && E >= B && 1 + D >= F && F >= 1 + D && B >= G$$ && G$$ >= B && F >= F$$ && F$$ >= F] 27. n31(A,B,C,D,E) -> n4(A,0,F$,G$,E) [A >= 1 && F$ >= 0 && A >= F$ && A >= G$ && G$ >= A && 0 >= F$ && F$ >= 0] (?,3) 28. n3(A,B,C,D,E) -> c2(n3(A,F,F$$,G$$,E),n31(A,F,C,D,E)) [F >= 1 (?,4) && A >= F && 1 + C >= F && F >= 1 + C && 1 + B >= F && F >= 1 + B && A >= D && D >= A && F$$ >= 0 && A >= G$$ && G$$ >= A && F >= F$$ && F$$ >= F] 29. m7(A,B,C,D,E) -> c2(m8(F,G,0,D,E),n2(F,G,0,F$,G$)) [B >= G && G >= B && A >= F && F >= A && G >= G$ && G$ >= G && 0 >= F$ && F$ >= 0] (1,3) 30. n4(A,B,C,D,E) -> n4(A,F,F$,G$,E) [F >= 1 (?,3) && A >= F && 1 + B >= F && F >= 1 + B && 1 + C >= F && F >= 1 + C && A >= D && D >= A && A >= 1 && F$ >= 0 && A >= F$ && A >= G$ && G$ >= A && F >= F$ && F$ >= F] Signature: {(m0,5) ;(m1,5) ;(m2,5) ;(m3,5) ;(m4,5) ;(m5,5) ;(m6,5) ;(m7,5) ;(m8,5) ;(m9,5) ;(multiply,5) ;(n0,5) ;(n1,5) ;(n2,5) ;(n20,5) ;(n21,5) ;(n3,5) ;(n30,5) ;(n31,5) ;(n4,5)} Flow Graph: [19->{29},24->{28},25->{24,25},27->{30},28->{27,28},29->{25},30->{30}] Sizebounds: (<19,0,A>, A) (<19,0,B>, B) (<19,0,C>, C) (<19,0,D>, D) (<19,0,E>, E) (<24,0,A>, A) (<24,0,B>, 1 + A) (<24,0,C>, 1 + A) (<24,0,D>, A) (<24,0,E>, B) (<25,0,A>, A) (<25,0,B>, B) (<25,0,C>, ?) (<25,0,D>, ?) (<25,0,E>, B) (<27,0,A>, A) (<27,0,B>, 1 + A) (<27,0,C>, 1 + A) (<27,0,D>, 1 + A) (<27,0,E>, B) (<28,0,A>, A) (<28,0,B>, 1 + A) (<28,0,C>, 1 + A) (<28,0,D>, A) (<28,0,E>, B) (<29,0,A>, A) (<29,0,B>, B) (<29,0,C>, ?) (<29,0,D>, ?) (<29,0,E>, B) (<30,0,A>, A) (<30,0,B>, 1 + A) (<30,0,C>, 1 + A) (<30,0,D>, 1 + A) (<30,0,E>, B) + Applied Processor: ChainProcessor False [19,24,25,27,28,29,30] + Details: We chained rule 25 to obtain the rules [31] . * Step 28: UnreachableRules WORST_CASE(?,O(n^3)) + Considered Problem: Rules: 19. multiply(A,B,C,D,E) -> m7(A,B,C,D,E) True (1,2) 24. n21(A,B,C,D,E) -> n3(A,0,F$,G$,E) [F$ >= 0 && A >= G$ && G$ >= A && 0 >= F$ && F$ >= 0] (?,3) 27. n31(A,B,C,D,E) -> n4(A,0,F$,G$,E) [A >= 1 && F$ >= 0 && A >= F$ && A >= G$ && G$ >= A && 0 >= F$ && F$ >= 0] (?,3) 28. n3(A,B,C,D,E) -> c2(n3(A,F,F$$,G$$,E),n31(A,F,C,D,E)) [F >= 1 (?,4) && A >= F && 1 + C >= F && F >= 1 + C && 1 + B >= F && F >= 1 + B && A >= D && D >= A && F$$ >= 0 && A >= G$$ && G$$ >= A && F >= F$$ && F$$ >= F] 29. m7(A,B,C,D,E) -> c2(m8(F,G,0,D,E),n2(F,G,0,F$,G$)) [B >= G && G >= B && A >= F && F >= A && G >= G$ && G$ >= G && 0 >= F$ && F$ >= 0] (1,3) 30. n4(A,B,C,D,E) -> n4(A,F,F$,G$,E) [F >= 1 (?,3) && A >= F && 1 + B >= F && F >= 1 + B && 1 + C >= F && F >= 1 + C && A >= D && D >= A && A >= 1 && F$ >= 0 && A >= F$ && A >= G$ && G$ >= A && F >= F$ && F$ >= F] 31. n2(A,B,C,D,E) -> c2(n2(A,B,F,F$$,G$$),n3(A,0,F$$$,G$$$,G$$)) [B >= F (?,7) && 1 + C >= F && F >= 1 + C && B >= E && E >= B && 1 + D >= F && F >= 1 + D && B >= G$$ && G$$ >= B && F >= F$$ && F$$ >= F && F$$$ >= 0 && A >= G$$$ && G$$$ >= A && 0 >= F$$$ && F$$$ >= 0] Signature: {(m0,5) ;(m1,5) ;(m2,5) ;(m3,5) ;(m4,5) ;(m5,5) ;(m6,5) ;(m7,5) ;(m8,5) ;(m9,5) ;(multiply,5) ;(n0,5) ;(n1,5) ;(n2,5) ;(n20,5) ;(n21,5) ;(n3,5) ;(n30,5) ;(n31,5) ;(n4,5)} Flow Graph: [19->{29},24->{28},27->{30},28->{27,28},29->{31},30->{30},31->{28,31}] Sizebounds: (<19,0,A>, A) (<19,0,B>, B) (<19,0,C>, C) (<19,0,D>, D) (<19,0,E>, E) (<24,0,A>, A) (<24,0,B>, 1 + A) (<24,0,C>, 1 + A) (<24,0,D>, A) (<24,0,E>, B) (<27,0,A>, A) (<27,0,B>, 1 + A) (<27,0,C>, 1 + A) (<27,0,D>, 1 + A) (<27,0,E>, B) (<28,0,A>, A) (<28,0,B>, 1 + A) (<28,0,C>, 1 + A) (<28,0,D>, A) (<28,0,E>, B) (<29,0,A>, A) (<29,0,B>, B) (<29,0,C>, ?) (<29,0,D>, ?) (<29,0,E>, B) (<30,0,A>, A) (<30,0,B>, 1 + A) (<30,0,C>, 1 + A) (<30,0,D>, 1 + A) (<30,0,E>, B) (<31,0,A>, A) (<31,0,B>, 1 + A) (<31,0,C>, 1 + A) (<31,0,D>, A) (<31,0,E>, B) + Applied Processor: UnreachableRules + Details: The following transitions are not reachable from the starting states and are removed: [24] * Step 29: ChainProcessor WORST_CASE(?,O(n^3)) + Considered Problem: Rules: 19. multiply(A,B,C,D,E) -> m7(A,B,C,D,E) True (1,2) 27. n31(A,B,C,D,E) -> n4(A,0,F$,G$,E) [A >= 1 && F$ >= 0 && A >= F$ && A >= G$ && G$ >= A && 0 >= F$ && F$ >= 0] (?,3) 28. n3(A,B,C,D,E) -> c2(n3(A,F,F$$,G$$,E),n31(A,F,C,D,E)) [F >= 1 (?,4) && A >= F && 1 + C >= F && F >= 1 + C && 1 + B >= F && F >= 1 + B && A >= D && D >= A && F$$ >= 0 && A >= G$$ && G$$ >= A && F >= F$$ && F$$ >= F] 29. m7(A,B,C,D,E) -> c2(m8(F,G,0,D,E),n2(F,G,0,F$,G$)) [B >= G && G >= B && A >= F && F >= A && G >= G$ && G$ >= G && 0 >= F$ && F$ >= 0] (1,3) 30. n4(A,B,C,D,E) -> n4(A,F,F$,G$,E) [F >= 1 (?,3) && A >= F && 1 + B >= F && F >= 1 + B && 1 + C >= F && F >= 1 + C && A >= D && D >= A && A >= 1 && F$ >= 0 && A >= F$ && A >= G$ && G$ >= A && F >= F$ && F$ >= F] 31. n2(A,B,C,D,E) -> c2(n2(A,B,F,F$$,G$$),n3(A,0,F$$$,G$$$,G$$)) [B >= F (?,7) && 1 + C >= F && F >= 1 + C && B >= E && E >= B && 1 + D >= F && F >= 1 + D && B >= G$$ && G$$ >= B && F >= F$$ && F$$ >= F && F$$$ >= 0 && A >= G$$$ && G$$$ >= A && 0 >= F$$$ && F$$$ >= 0] Signature: {(m0,5) ;(m1,5) ;(m2,5) ;(m3,5) ;(m4,5) ;(m5,5) ;(m6,5) ;(m7,5) ;(m8,5) ;(m9,5) ;(multiply,5) ;(n0,5) ;(n1,5) ;(n2,5) ;(n20,5) ;(n21,5) ;(n3,5) ;(n30,5) ;(n31,5) ;(n4,5)} Flow Graph: [19->{29},27->{30},28->{27,28},29->{31},30->{30},31->{28,31}] Sizebounds: (<19,0,A>, A) (<19,0,B>, B) (<19,0,C>, C) (<19,0,D>, D) (<19,0,E>, E) (<27,0,A>, A) (<27,0,B>, 1 + A) (<27,0,C>, 1 + A) (<27,0,D>, 1 + A) (<27,0,E>, B) (<28,0,A>, A) (<28,0,B>, 1 + A) (<28,0,C>, 1 + A) (<28,0,D>, A) (<28,0,E>, B) (<29,0,A>, A) (<29,0,B>, B) (<29,0,C>, ?) (<29,0,D>, ?) (<29,0,E>, B) (<30,0,A>, A) (<30,0,B>, 1 + A) (<30,0,C>, 1 + A) (<30,0,D>, 1 + A) (<30,0,E>, B) (<31,0,A>, A) (<31,0,B>, 1 + A) (<31,0,C>, 1 + A) (<31,0,D>, A) (<31,0,E>, B) + Applied Processor: ChainProcessor False [19,27,28,29,30,31] + Details: We chained rule 28 to obtain the rules [32] . * Step 30: UnreachableRules WORST_CASE(?,O(n^3)) + Considered Problem: Rules: 19. multiply(A,B,C,D,E) -> m7(A,B,C,D,E) True (1,2) 27. n31(A,B,C,D,E) -> n4(A,0,F$,G$,E) [A >= 1 && F$ >= 0 && A >= F$ && A >= G$ && G$ >= A && 0 >= F$ && F$ >= 0] (?,3) 29. m7(A,B,C,D,E) -> c2(m8(F,G,0,D,E),n2(F,G,0,F$,G$)) [B >= G && G >= B && A >= F && F >= A && G >= G$ && G$ >= G && 0 >= F$ && F$ >= 0] (1,3) 30. n4(A,B,C,D,E) -> n4(A,F,F$,G$,E) [F >= 1 (?,3) && A >= F && 1 + B >= F && F >= 1 + B && 1 + C >= F && F >= 1 + C && A >= D && D >= A && A >= 1 && F$ >= 0 && A >= F$ && A >= G$ && G$ >= A && F >= F$ && F$ >= F] 31. n2(A,B,C,D,E) -> c2(n2(A,B,F,F$$,G$$),n3(A,0,F$$$,G$$$,G$$)) [B >= F (?,7) && 1 + C >= F && F >= 1 + C && B >= E && E >= B && 1 + D >= F && F >= 1 + D && B >= G$$ && G$$ >= B && F >= F$$ && F$$ >= F && F$$$ >= 0 && A >= G$$$ && G$$$ >= A && 0 >= F$$$ && F$$$ >= 0] 32. n3(A,B,C,D,E) -> c2(n3(A,F,F$$,G$$,E),n4(A,0,F$$$,G$$$,E)) [F >= 1 (?,7) && A >= F && 1 + C >= F && F >= 1 + C && 1 + B >= F && F >= 1 + B && A >= D && D >= A && F$$ >= 0 && A >= G$$ && G$$ >= A && F >= F$$ && F$$ >= F && A >= 1 && F$$$ >= 0 && A >= F$$$ && A >= G$$$ && G$$$ >= A && 0 >= F$$$ && F$$$ >= 0] Signature: {(m0,5) ;(m1,5) ;(m2,5) ;(m3,5) ;(m4,5) ;(m5,5) ;(m6,5) ;(m7,5) ;(m8,5) ;(m9,5) ;(multiply,5) ;(n0,5) ;(n1,5) ;(n2,5) ;(n20,5) ;(n21,5) ;(n3,5) ;(n30,5) ;(n31,5) ;(n4,5)} Flow Graph: [19->{29},27->{30},29->{31},30->{30},31->{31,32},32->{30,32}] Sizebounds: (<19,0,A>, A) (<19,0,B>, B) (<19,0,C>, C) (<19,0,D>, D) (<19,0,E>, E) (<27,0,A>, A) (<27,0,B>, 1 + A) (<27,0,C>, 1 + A) (<27,0,D>, 1 + A) (<27,0,E>, B) (<29,0,A>, A) (<29,0,B>, B) (<29,0,C>, ?) (<29,0,D>, ?) (<29,0,E>, B) (<30,0,A>, A) (<30,0,B>, 1 + A) (<30,0,C>, 1 + A) (<30,0,D>, 1 + A) (<30,0,E>, B) (<31,0,A>, A) (<31,0,B>, 1 + A) (<31,0,C>, 1 + A) (<31,0,D>, A) (<31,0,E>, B) (<32,0,A>, A) (<32,0,B>, 1 + A) (<32,0,C>, 1 + A) (<32,0,D>, 1 + A) (<32,0,E>, B) + Applied Processor: UnreachableRules + Details: The following transitions are not reachable from the starting states and are removed: [27] * Step 31: LocalSizeboundsProc WORST_CASE(?,O(n^3)) + Considered Problem: Rules: 19. multiply(A,B,C,D,E) -> m7(A,B,C,D,E) True (1,2) 29. m7(A,B,C,D,E) -> c2(m8(F,G,0,D,E),n2(F,G,0,F$,G$)) [B >= G && G >= B && A >= F && F >= A && G >= G$ && G$ >= G && 0 >= F$ && F$ >= 0] (1,3) 30. n4(A,B,C,D,E) -> n4(A,F,F$,G$,E) [F >= 1 (?,3) && A >= F && 1 + B >= F && F >= 1 + B && 1 + C >= F && F >= 1 + C && A >= D && D >= A && A >= 1 && F$ >= 0 && A >= F$ && A >= G$ && G$ >= A && F >= F$ && F$ >= F] 31. n2(A,B,C,D,E) -> c2(n2(A,B,F,F$$,G$$),n3(A,0,F$$$,G$$$,G$$)) [B >= F (?,7) && 1 + C >= F && F >= 1 + C && B >= E && E >= B && 1 + D >= F && F >= 1 + D && B >= G$$ && G$$ >= B && F >= F$$ && F$$ >= F && F$$$ >= 0 && A >= G$$$ && G$$$ >= A && 0 >= F$$$ && F$$$ >= 0] 32. n3(A,B,C,D,E) -> c2(n3(A,F,F$$,G$$,E),n4(A,0,F$$$,G$$$,E)) [F >= 1 (?,7) && A >= F && 1 + C >= F && F >= 1 + C && 1 + B >= F && F >= 1 + B && A >= D && D >= A && F$$ >= 0 && A >= G$$ && G$$ >= A && F >= F$$ && F$$ >= F && A >= 1 && F$$$ >= 0 && A >= F$$$ && A >= G$$$ && G$$$ >= A && 0 >= F$$$ && F$$$ >= 0] Signature: {(m0,5) ;(m1,5) ;(m2,5) ;(m3,5) ;(m4,5) ;(m5,5) ;(m6,5) ;(m7,5) ;(m8,5) ;(m9,5) ;(multiply,5) ;(n0,5) ;(n1,5) ;(n2,5) ;(n20,5) ;(n21,5) ;(n3,5) ;(n30,5) ;(n31,5) ;(n4,5)} Flow Graph: [19->{29},29->{31},30->{30},31->{31,32},32->{30,32}] Sizebounds: (<19,0,A>, A) (<19,0,B>, B) (<19,0,C>, C) (<19,0,D>, D) (<19,0,E>, E) (<29,0,A>, A) (<29,0,B>, B) (<29,0,C>, ?) (<29,0,D>, ?) (<29,0,E>, B) (<30,0,A>, A) (<30,0,B>, 1 + A) (<30,0,C>, 1 + A) (<30,0,D>, 1 + A) (<30,0,E>, B) (<31,0,A>, A) (<31,0,B>, 1 + A) (<31,0,C>, 1 + A) (<31,0,D>, A) (<31,0,E>, B) (<32,0,A>, A) (<32,0,B>, 1 + A) (<32,0,C>, 1 + A) (<32,0,D>, 1 + A) (<32,0,E>, B) + Applied Processor: LocalSizeboundsProc + Details: LocalSizebounds generated; rvgraph (<19,0,A>, A, .= 0) (<19,0,B>, B, .= 0) (<19,0,C>, C, .= 0) (<19,0,D>, D, .= 0) (<19,0,E>, E, .= 0) (<29,0,A>, A, .= 0) (<29,0,B>, B, .= 0) (<29,0,C>, 0, .= 0) (<29,0,D>, D, .= 0) (<29,0,E>, E, .= 0) (<29,1,A>, A, .= 0) (<29,1,B>, B, .= 0) (<29,1,C>, 0, .= 0) (<29,1,D>, 0, .= 0) (<29,1,E>, B, .= 0) (<30,0,A>, A, .= 0) (<30,0,B>, 1 + B, .+ 1) (<30,0,C>, A, .= 0) (<30,0,D>, 1 + A, .+ 1) (<30,0,E>, E, .= 0) (<31,0,A>, A, .= 0) (<31,0,B>, B, .= 0) (<31,0,C>, 1 + B + C, .* 1) (<31,0,D>, 1 + B + C, .* 1) (<31,0,E>, B, .= 0) (<31,1,A>, A, .= 0) (<31,1,B>, 0, .= 0) (<31,1,C>, 0, .= 0) (<31,1,D>, A, .= 0) (<31,1,E>, B, .= 0) (<32,0,A>, A, .= 0) (<32,0,B>, 1 + B, .+ 1) (<32,0,C>, 1 + B, .+ 1) (<32,0,D>, 1 + A, .+ 1) (<32,0,E>, E, .= 0) (<32,1,A>, A, .= 0) (<32,1,B>, 0, .= 0) (<32,1,C>, 0, .= 0) (<32,1,D>, 1 + A, .+ 1) (<32,1,E>, E, .= 0) * Step 32: SizeboundsProc WORST_CASE(?,O(n^3)) + Considered Problem: Rules: 19. multiply(A,B,C,D,E) -> m7(A,B,C,D,E) True (1,2) 29. m7(A,B,C,D,E) -> c2(m8(F,G,0,D,E),n2(F,G,0,F$,G$)) [B >= G && G >= B && A >= F && F >= A && G >= G$ && G$ >= G && 0 >= F$ && F$ >= 0] (1,3) 30. n4(A,B,C,D,E) -> n4(A,F,F$,G$,E) [F >= 1 (?,3) && A >= F && 1 + B >= F && F >= 1 + B && 1 + C >= F && F >= 1 + C && A >= D && D >= A && A >= 1 && F$ >= 0 && A >= F$ && A >= G$ && G$ >= A && F >= F$ && F$ >= F] 31. n2(A,B,C,D,E) -> c2(n2(A,B,F,F$$,G$$),n3(A,0,F$$$,G$$$,G$$)) [B >= F (?,7) && 1 + C >= F && F >= 1 + C && B >= E && E >= B && 1 + D >= F && F >= 1 + D && B >= G$$ && G$$ >= B && F >= F$$ && F$$ >= F && F$$$ >= 0 && A >= G$$$ && G$$$ >= A && 0 >= F$$$ && F$$$ >= 0] 32. n3(A,B,C,D,E) -> c2(n3(A,F,F$$,G$$,E),n4(A,0,F$$$,G$$$,E)) [F >= 1 (?,7) && A >= F && 1 + C >= F && F >= 1 + C && 1 + B >= F && F >= 1 + B && A >= D && D >= A && F$$ >= 0 && A >= G$$ && G$$ >= A && F >= F$$ && F$$ >= F && A >= 1 && F$$$ >= 0 && A >= F$$$ && A >= G$$$ && G$$$ >= A && 0 >= F$$$ && F$$$ >= 0] Signature: {(m0,5) ;(m1,5) ;(m2,5) ;(m3,5) ;(m4,5) ;(m5,5) ;(m6,5) ;(m7,5) ;(m8,5) ;(m9,5) ;(multiply,5) ;(n0,5) ;(n1,5) ;(n2,5) ;(n20,5) ;(n21,5) ;(n3,5) ;(n30,5) ;(n31,5) ;(n4,5)} Flow Graph: [19->{29},29->{31},30->{30},31->{31,32},32->{30,32}] Sizebounds: (<19,0,A>, ?) (<19,0,B>, ?) (<19,0,C>, ?) (<19,0,D>, ?) (<19,0,E>, ?) (<29,0,A>, ?) (<29,0,B>, ?) (<29,0,C>, ?) (<29,0,D>, ?) (<29,0,E>, ?) (<29,1,A>, ?) (<29,1,B>, ?) (<29,1,C>, ?) (<29,1,D>, ?) (<29,1,E>, ?) (<30,0,A>, ?) (<30,0,B>, ?) (<30,0,C>, ?) (<30,0,D>, ?) (<30,0,E>, ?) (<31,0,A>, ?) (<31,0,B>, ?) (<31,0,C>, ?) (<31,0,D>, ?) (<31,0,E>, ?) (<31,1,A>, ?) (<31,1,B>, ?) (<31,1,C>, ?) (<31,1,D>, ?) (<31,1,E>, ?) (<32,0,A>, ?) (<32,0,B>, ?) (<32,0,C>, ?) (<32,0,D>, ?) (<32,0,E>, ?) (<32,1,A>, ?) (<32,1,B>, ?) (<32,1,C>, ?) (<32,1,D>, ?) (<32,1,E>, ?) + Applied Processor: SizeboundsProc + Details: Sizebounds computed: (<19,0,A>, A) (<19,0,B>, B) (<19,0,C>, C) (<19,0,D>, D) (<19,0,E>, E) (<29,0,A>, A) (<29,0,B>, B) (<29,0,C>, 0) (<29,0,D>, D) (<29,0,E>, E) (<29,1,A>, A) (<29,1,B>, B) (<29,1,C>, 0) (<29,1,D>, 0) (<29,1,E>, B) (<30,0,A>, A) (<30,0,B>, 1) (<30,0,C>, A) (<30,0,D>, 1 + A) (<30,0,E>, B) (<31,0,A>, A) (<31,0,B>, B) (<31,0,C>, ?) (<31,0,D>, ?) (<31,0,E>, B) (<31,1,A>, A) (<31,1,B>, 0) (<31,1,C>, 0) (<31,1,D>, A) (<31,1,E>, B) (<32,0,A>, A) (<32,0,B>, ?) (<32,0,C>, ?) (<32,0,D>, 1 + A) (<32,0,E>, B) (<32,1,A>, A) (<32,1,B>, 0) (<32,1,C>, 0) (<32,1,D>, 1 + A) (<32,1,E>, B) * Step 33: LocationConstraintsProc WORST_CASE(?,O(n^3)) + Considered Problem: Rules: 19. multiply(A,B,C,D,E) -> m7(A,B,C,D,E) True (1,2) 29. m7(A,B,C,D,E) -> c2(m8(F,G,0,D,E),n2(F,G,0,F$,G$)) [B >= G && G >= B && A >= F && F >= A && G >= G$ && G$ >= G && 0 >= F$ && F$ >= 0] (1,3) 30. n4(A,B,C,D,E) -> n4(A,F,F$,G$,E) [F >= 1 (?,3) && A >= F && 1 + B >= F && F >= 1 + B && 1 + C >= F && F >= 1 + C && A >= D && D >= A && A >= 1 && F$ >= 0 && A >= F$ && A >= G$ && G$ >= A && F >= F$ && F$ >= F] 31. n2(A,B,C,D,E) -> c2(n2(A,B,F,F$$,G$$),n3(A,0,F$$$,G$$$,G$$)) [B >= F (?,7) && 1 + C >= F && F >= 1 + C && B >= E && E >= B && 1 + D >= F && F >= 1 + D && B >= G$$ && G$$ >= B && F >= F$$ && F$$ >= F && F$$$ >= 0 && A >= G$$$ && G$$$ >= A && 0 >= F$$$ && F$$$ >= 0] 32. n3(A,B,C,D,E) -> c2(n3(A,F,F$$,G$$,E),n4(A,0,F$$$,G$$$,E)) [F >= 1 (?,7) && A >= F && 1 + C >= F && F >= 1 + C && 1 + B >= F && F >= 1 + B && A >= D && D >= A && F$$ >= 0 && A >= G$$ && G$$ >= A && F >= F$$ && F$$ >= F && A >= 1 && F$$$ >= 0 && A >= F$$$ && A >= G$$$ && G$$$ >= A && 0 >= F$$$ && F$$$ >= 0] Signature: {(m0,5) ;(m1,5) ;(m2,5) ;(m3,5) ;(m4,5) ;(m5,5) ;(m6,5) ;(m7,5) ;(m8,5) ;(m9,5) ;(multiply,5) ;(n0,5) ;(n1,5) ;(n2,5) ;(n20,5) ;(n21,5) ;(n3,5) ;(n30,5) ;(n31,5) ;(n4,5)} Flow Graph: [19->{29},29->{31},30->{30},31->{31,32},32->{30,32}] Sizebounds: (<19,0,A>, A) (<19,0,B>, B) (<19,0,C>, C) (<19,0,D>, D) (<19,0,E>, E) (<29,0,A>, A) (<29,0,B>, B) (<29,0,C>, 0) (<29,0,D>, D) (<29,0,E>, E) (<29,1,A>, A) (<29,1,B>, B) (<29,1,C>, 0) (<29,1,D>, 0) (<29,1,E>, B) (<30,0,A>, A) (<30,0,B>, 1) (<30,0,C>, A) (<30,0,D>, 1 + A) (<30,0,E>, B) (<31,0,A>, A) (<31,0,B>, B) (<31,0,C>, ?) (<31,0,D>, ?) (<31,0,E>, B) (<31,1,A>, A) (<31,1,B>, 0) (<31,1,C>, 0) (<31,1,D>, A) (<31,1,E>, B) (<32,0,A>, A) (<32,0,B>, ?) (<32,0,C>, ?) (<32,0,D>, 1 + A) (<32,0,E>, B) (<32,1,A>, A) (<32,1,B>, 0) (<32,1,C>, 0) (<32,1,D>, 1 + A) (<32,1,E>, B) + Applied Processor: LocationConstraintsProc + Details: We computed the location constraints 19 : True 29 : True 30 : True 31 : True 32 : True . * Step 34: LoopRecurrenceProcessor WORST_CASE(?,O(n^3)) + Considered Problem: Rules: 19. multiply(A,B,C,D,E) -> m7(A,B,C,D,E) True (1,2) 29. m7(A,B,C,D,E) -> c2(m8(F,G,0,D,E),n2(F,G,0,F$,G$)) [B >= G && G >= B && A >= F && F >= A && G >= G$ && G$ >= G && 0 >= F$ && F$ >= 0] (1,3) 30. n4(A,B,C,D,E) -> n4(A,F,F$,G$,E) [F >= 1 (?,3) && A >= F && 1 + B >= F && F >= 1 + B && 1 + C >= F && F >= 1 + C && A >= D && D >= A && A >= 1 && F$ >= 0 && A >= F$ && A >= G$ && G$ >= A && F >= F$ && F$ >= F] 31. n2(A,B,C,D,E) -> c2(n2(A,B,F,F$$,G$$),n3(A,0,F$$$,G$$$,G$$)) [B >= F (?,7) && 1 + C >= F && F >= 1 + C && B >= E && E >= B && 1 + D >= F && F >= 1 + D && B >= G$$ && G$$ >= B && F >= F$$ && F$$ >= F && F$$$ >= 0 && A >= G$$$ && G$$$ >= A && 0 >= F$$$ && F$$$ >= 0] 32. n3(A,B,C,D,E) -> c2(n3(A,F,F$$,G$$,E),n4(A,0,F$$$,G$$$,E)) [F >= 1 (?,7) && A >= F && 1 + C >= F && F >= 1 + C && 1 + B >= F && F >= 1 + B && A >= D && D >= A && F$$ >= 0 && A >= G$$ && G$$ >= A && F >= F$$ && F$$ >= F && A >= 1 && F$$$ >= 0 && A >= F$$$ && A >= G$$$ && G$$$ >= A && 0 >= F$$$ && F$$$ >= 0] Signature: {(m0,5) ;(m1,5) ;(m2,5) ;(m3,5) ;(m4,5) ;(m5,5) ;(m6,5) ;(m7,5) ;(m8,5) ;(m9,5) ;(multiply,5) ;(n0,5) ;(n1,5) ;(n2,5) ;(n20,5) ;(n21,5) ;(n3,5) ;(n30,5) ;(n31,5) ;(n4,5)} Flow Graph: [19->{29},29->{31},30->{30},31->{31,32},32->{30,32}] Sizebounds: (<19,0,A>, A) (<19,0,B>, B) (<19,0,C>, C) (<19,0,D>, D) (<19,0,E>, E) (<29,0,A>, A) (<29,0,B>, B) (<29,0,C>, 0) (<29,0,D>, D) (<29,0,E>, E) (<29,1,A>, A) (<29,1,B>, B) (<29,1,C>, 0) (<29,1,D>, 0) (<29,1,E>, B) (<30,0,A>, A) (<30,0,B>, 1) (<30,0,C>, A) (<30,0,D>, 1 + A) (<30,0,E>, B) (<31,0,A>, A) (<31,0,B>, B) (<31,0,C>, ?) (<31,0,D>, ?) (<31,0,E>, B) (<31,1,A>, A) (<31,1,B>, 0) (<31,1,C>, 0) (<31,1,D>, A) (<31,1,E>, B) (<32,0,A>, A) (<32,0,B>, ?) (<32,0,C>, ?) (<32,0,D>, 1 + A) (<32,0,E>, B) (<32,1,A>, A) (<32,1,B>, 0) (<32,1,C>, 0) (<32,1,D>, 1 + A) (<32,1,E>, B) + Applied Processor: LoopRecurrenceProcessor [31] + Details: Applying the recurrence pattern linear * f to the expression B-C yields the solution 2*A*B + -2*A*C + 2*A^2*B + -2*A^2*C + B + -1*C . * Step 35: LoopRecurrenceProcessor WORST_CASE(?,O(n^3)) + Considered Problem: Rules: 19. multiply(A,B,C,D,E) -> m7(A,B,C,D,E) True (1,2) 29. m7(A,B,C,D,E) -> c2(m8(F,G,0,D,E),n2(F,G,0,F$,G$)) [B >= G && G >= B && A >= F && F >= A && G >= G$ && G$ >= G && 0 >= F$ && F$ >= 0] (1,3) 30. n4(A,B,C,D,E) -> n4(A,F,F$,G$,E) [F >= 1 (2*A*B + 2*A^2*B + B,3) && A >= F && 1 + B >= F && F >= 1 + B && 1 + C >= F && F >= 1 + C && A >= D && D >= A && A >= 1 && F$ >= 0 && A >= F$ && A >= G$ && G$ >= A && F >= F$ && F$ >= F] 31. n2(A,B,C,D,E) -> c2(n2(A,B,F,F$$,G$$),n3(A,0,F$$$,G$$$,G$$)) [B >= F (2*A*B + 2*A^2*B + B,7) && 1 + C >= F && F >= 1 + C && B >= E && E >= B && 1 + D >= F && F >= 1 + D && B >= G$$ && G$$ >= B && F >= F$$ && F$$ >= F && F$$$ >= 0 && A >= G$$$ && G$$$ >= A && 0 >= F$$$ && F$$$ >= 0] 32. n3(A,B,C,D,E) -> c2(n3(A,F,F$$,G$$,E),n4(A,0,F$$$,G$$$,E)) [F >= 1 (2*A*B + 2*A^2*B + B,7) && A >= F && 1 + C >= F && F >= 1 + C && 1 + B >= F && F >= 1 + B && A >= D && D >= A && F$$ >= 0 && A >= G$$ && G$$ >= A && F >= F$$ && F$$ >= F && A >= 1 && F$$$ >= 0 && A >= F$$$ && A >= G$$$ && G$$$ >= A && 0 >= F$$$ && F$$$ >= 0] Signature: {(m0,5) ;(m1,5) ;(m2,5) ;(m3,5) ;(m4,5) ;(m5,5) ;(m6,5) ;(m7,5) ;(m8,5) ;(m9,5) ;(multiply,5) ;(n0,5) ;(n1,5) ;(n2,5) ;(n20,5) ;(n21,5) ;(n3,5) ;(n30,5) ;(n31,5) ;(n4,5)} Flow Graph: [19->{29},29->{31},30->{30},31->{31,32},32->{30,32}] Sizebounds: (<19,0,A>, A) (<19,0,B>, B) (<19,0,C>, C) (<19,0,D>, D) (<19,0,E>, E) (<29,0,A>, A) (<29,0,B>, B) (<29,0,C>, 0) (<29,0,D>, D) (<29,0,E>, E) (<29,1,A>, A) (<29,1,B>, B) (<29,1,C>, 0) (<29,1,D>, 0) (<29,1,E>, B) (<30,0,A>, A) (<30,0,B>, 1) (<30,0,C>, A) (<30,0,D>, 1 + A) (<30,0,E>, B) (<31,0,A>, A) (<31,0,B>, B) (<31,0,C>, ?) (<31,0,D>, ?) (<31,0,E>, B) (<31,1,A>, A) (<31,1,B>, 0) (<31,1,C>, 0) (<31,1,D>, A) (<31,1,E>, B) (<32,0,A>, A) (<32,0,B>, ?) (<32,0,C>, ?) (<32,0,D>, 1 + A) (<32,0,E>, B) (<32,1,A>, A) (<32,1,B>, 0) (<32,1,C>, 0) (<32,1,D>, 1 + A) (<32,1,E>, B) + Applied Processor: LoopRecurrenceProcessor [32] + Details: Applying the recurrence pattern linear * f to the expression A-B yields the solution A + -1*A*B + A^2 + -1*B . * Step 36: LoopRecurrenceProcessor WORST_CASE(?,O(n^3)) + Considered Problem: Rules: 19. multiply(A,B,C,D,E) -> m7(A,B,C,D,E) True (1,2) 29. m7(A,B,C,D,E) -> c2(m8(F,G,0,D,E),n2(F,G,0,F$,G$)) [B >= G && G >= B && A >= F && F >= A && G >= G$ && G$ >= G && 0 >= F$ && F$ >= 0] (1,3) 30. n4(A,B,C,D,E) -> n4(A,F,F$,G$,E) [F >= 1 (2*A*B + 2*A^2*B + B,3) && A >= F && 1 + B >= F && F >= 1 + B && 1 + C >= F && F >= 1 + C && A >= D && D >= A && A >= 1 && F$ >= 0 && A >= F$ && A >= G$ && G$ >= A && F >= F$ && F$ >= F] 31. n2(A,B,C,D,E) -> c2(n2(A,B,F,F$$,G$$),n3(A,0,F$$$,G$$$,G$$)) [B >= F (2*A*B + 2*A^2*B + B,7) && 1 + C >= F && F >= 1 + C && B >= E && E >= B && 1 + D >= F && F >= 1 + D && B >= G$$ && G$$ >= B && F >= F$$ && F$$ >= F && F$$$ >= 0 && A >= G$$$ && G$$$ >= A && 0 >= F$$$ && F$$$ >= 0] 32. n3(A,B,C,D,E) -> c2(n3(A,F,F$$,G$$,E),n4(A,0,F$$$,G$$$,E)) [F >= 1 (2*A*B + 2*A^2*B + B,7) && A >= F && 1 + C >= F && F >= 1 + C && 1 + B >= F && F >= 1 + B && A >= D && D >= A && F$$ >= 0 && A >= G$$ && G$$ >= A && F >= F$$ && F$$ >= F && A >= 1 && F$$$ >= 0 && A >= F$$$ && A >= G$$$ && G$$$ >= A && 0 >= F$$$ && F$$$ >= 0] Signature: {(m0,5) ;(m1,5) ;(m2,5) ;(m3,5) ;(m4,5) ;(m5,5) ;(m6,5) ;(m7,5) ;(m8,5) ;(m9,5) ;(multiply,5) ;(n0,5) ;(n1,5) ;(n2,5) ;(n20,5) ;(n21,5) ;(n3,5) ;(n30,5) ;(n31,5) ;(n4,5)} Flow Graph: [19->{29},29->{31},30->{30},31->{31,32},32->{30,32}] Sizebounds: (<19,0,A>, A) (<19,0,B>, B) (<19,0,C>, C) (<19,0,D>, D) (<19,0,E>, E) (<29,0,A>, A) (<29,0,B>, B) (<29,0,C>, 0) (<29,0,D>, D) (<29,0,E>, E) (<29,1,A>, A) (<29,1,B>, B) (<29,1,C>, 0) (<29,1,D>, 0) (<29,1,E>, B) (<30,0,A>, A) (<30,0,B>, 1) (<30,0,C>, A) (<30,0,D>, 1 + A) (<30,0,E>, B) (<31,0,A>, A) (<31,0,B>, B) (<31,0,C>, ?) (<31,0,D>, ?) (<31,0,E>, B) (<31,1,A>, A) (<31,1,B>, 0) (<31,1,C>, 0) (<31,1,D>, A) (<31,1,E>, B) (<32,0,A>, A) (<32,0,B>, ?) (<32,0,C>, ?) (<32,0,D>, 1 + A) (<32,0,E>, B) (<32,1,A>, A) (<32,1,B>, 0) (<32,1,C>, 0) (<32,1,D>, 1 + A) (<32,1,E>, B) + Applied Processor: LoopRecurrenceProcessor [30] + Details: Applying the recurrence pattern linear * f to the expression A-B yields the solution A + -1*B . * Step 37: UnsatPaths WORST_CASE(?,O(n^3)) + Considered Problem: Rules: 19. multiply(A,B,C,D,E) -> m7(A,B,C,D,E) True (1,2) 29. m7(A,B,C,D,E) -> c2(m8(F,G,0,D,E),n2(F,G,0,F$,G$)) [B >= G && G >= B && A >= F && F >= A && G >= G$ && G$ >= G && 0 >= F$ && F$ >= 0] (1,3) 30. n4(A,B,C,D,E) -> n4(A,F,F$,G$,E) [F >= 1 (2*A*B + 2*A^2*B + B,3) && A >= F && 1 + B >= F && F >= 1 + B && 1 + C >= F && F >= 1 + C && A >= D && D >= A && A >= 1 && F$ >= 0 && A >= F$ && A >= G$ && G$ >= A && F >= F$ && F$ >= F] 31. n2(A,B,C,D,E) -> c2(n2(A,B,F,F$$,G$$),n3(A,0,F$$$,G$$$,G$$)) [B >= F (2*A*B + 2*A^2*B + B,7) && 1 + C >= F && F >= 1 + C && B >= E && E >= B && 1 + D >= F && F >= 1 + D && B >= G$$ && G$$ >= B && F >= F$$ && F$$ >= F && F$$$ >= 0 && A >= G$$$ && G$$$ >= A && 0 >= F$$$ && F$$$ >= 0] 32. n3(A,B,C,D,E) -> c2(n3(A,F,F$$,G$$,E),n4(A,0,F$$$,G$$$,E)) [F >= 1 (2*A*B + 2*A^2*B + B,7) && A >= F && 1 + C >= F && F >= 1 + C && 1 + B >= F && F >= 1 + B && A >= D && D >= A && F$$ >= 0 && A >= G$$ && G$$ >= A && F >= F$$ && F$$ >= F && A >= 1 && F$$$ >= 0 && A >= F$$$ && A >= G$$$ && G$$$ >= A && 0 >= F$$$ && F$$$ >= 0] Signature: {(m0,5) ;(m1,5) ;(m2,5) ;(m3,5) ;(m4,5) ;(m5,5) ;(m6,5) ;(m7,5) ;(m8,5) ;(m9,5) ;(multiply,5) ;(n0,5) ;(n1,5) ;(n2,5) ;(n20,5) ;(n21,5) ;(n3,5) ;(n30,5) ;(n31,5) ;(n4,5)} Flow Graph: [19->{29},29->{31},30->{30},31->{31,32},32->{30,32}] Sizebounds: (<19,0,A>, A) (<19,0,B>, B) (<19,0,C>, C) (<19,0,D>, D) (<19,0,E>, E) (<29,0,A>, A) (<29,0,B>, B) (<29,0,C>, 0) (<29,0,D>, D) (<29,0,E>, E) (<29,1,A>, A) (<29,1,B>, B) (<29,1,C>, 0) (<29,1,D>, 0) (<29,1,E>, B) (<30,0,A>, A) (<30,0,B>, 1) (<30,0,C>, A) (<30,0,D>, 1 + A) (<30,0,E>, B) (<31,0,A>, A) (<31,0,B>, B) (<31,0,C>, ?) (<31,0,D>, ?) (<31,0,E>, B) (<31,1,A>, A) (<31,1,B>, 0) (<31,1,C>, 0) (<31,1,D>, A) (<31,1,E>, B) (<32,0,A>, A) (<32,0,B>, ?) (<32,0,C>, ?) (<32,0,D>, 1 + A) (<32,0,E>, B) (<32,1,A>, A) (<32,1,B>, 0) (<32,1,C>, 0) (<32,1,D>, 1 + A) (<32,1,E>, B) + Applied Processor: UnsatPaths + Details: The problem is already solved. WORST_CASE(?,O(n^3))