WORST_CASE(?,O(n^2)) * Step 1: RestrictVarsProcessor WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 0. f0(A,B,C,D) -> f4(0,B,C,D) True (1,1) 1. f4(A,B,C,D) -> f8(1 + A,B,0,D) [B >= 1 + A] (?,1) 2. f8(A,B,C,D) -> f16(A,B,C,0) [B >= 1 + A] (?,1) 3. f8(A,B,C,D) -> f16(A,B,C,D) [A >= B] (?,1) 4. f8(A,B,C,D) -> f8(1 + A,B,1 + C,E) [B >= 1 + A && 0 >= 1 + E] (?,1) 5. f8(A,B,C,D) -> f8(1 + A,B,1 + C,E) [B >= 1 + A && E >= 1] (?,1) 6. f16(A,B,C,D) -> f4(A,B,C,D) [0 >= C] (?,1) 7. f16(A,B,C,D) -> f4(-1 + A,B,C,D) [C >= 1] (?,1) 8. f4(A,B,C,D) -> f20(A,B,C,D) [A >= B] (?,1) Signature: {(f0,4);(f16,4);(f20,4);(f4,4);(f8,4)} Flow Graph: [0->{1,8},1->{2,3,4,5},2->{6,7},3->{6,7},4->{2,3,4,5},5->{2,3,4,5},6->{1,8},7->{1,8},8->{}] + Applied Processor: RestrictVarsProcessor + Details: We removed the arguments [D] . * Step 2: LocalSizeboundsProc WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 0. f0(A,B,C) -> f4(0,B,C) True (1,1) 1. f4(A,B,C) -> f8(1 + A,B,0) [B >= 1 + A] (?,1) 2. f8(A,B,C) -> f16(A,B,C) [B >= 1 + A] (?,1) 3. f8(A,B,C) -> f16(A,B,C) [A >= B] (?,1) 4. f8(A,B,C) -> f8(1 + A,B,1 + C) [B >= 1 + A && 0 >= 1 + E] (?,1) 5. f8(A,B,C) -> f8(1 + A,B,1 + C) [B >= 1 + A && E >= 1] (?,1) 6. f16(A,B,C) -> f4(A,B,C) [0 >= C] (?,1) 7. f16(A,B,C) -> f4(-1 + A,B,C) [C >= 1] (?,1) 8. f4(A,B,C) -> f20(A,B,C) [A >= B] (?,1) Signature: {(f0,3);(f16,3);(f20,3);(f4,3);(f8,3)} Flow Graph: [0->{1,8},1->{2,3,4,5},2->{6,7},3->{6,7},4->{2,3,4,5},5->{2,3,4,5},6->{1,8},7->{1,8},8->{}] + Applied Processor: LocalSizeboundsProc + Details: LocalSizebounds generated; rvgraph (<0,0,A>, 0, .= 0) (<0,0,B>, B, .= 0) (<0,0,C>, C, .= 0) (<1,0,A>, 1 + A, .+ 1) (<1,0,B>, B, .= 0) (<1,0,C>, 0, .= 0) (<2,0,A>, A, .= 0) (<2,0,B>, B, .= 0) (<2,0,C>, C, .= 0) (<3,0,A>, A, .= 0) (<3,0,B>, B, .= 0) (<3,0,C>, C, .= 0) (<4,0,A>, 1 + A, .+ 1) (<4,0,B>, B, .= 0) (<4,0,C>, 1 + C, .+ 1) (<5,0,A>, 1 + A, .+ 1) (<5,0,B>, B, .= 0) (<5,0,C>, 1 + C, .+ 1) (<6,0,A>, A, .= 0) (<6,0,B>, B, .= 0) (<6,0,C>, C, .= 0) (<7,0,A>, 1 + A, .+ 1) (<7,0,B>, B, .= 0) (<7,0,C>, C, .= 0) (<8,0,A>, A, .= 0) (<8,0,B>, B, .= 0) (<8,0,C>, C, .= 0) * Step 3: SizeboundsProc WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 0. f0(A,B,C) -> f4(0,B,C) True (1,1) 1. f4(A,B,C) -> f8(1 + A,B,0) [B >= 1 + A] (?,1) 2. f8(A,B,C) -> f16(A,B,C) [B >= 1 + A] (?,1) 3. f8(A,B,C) -> f16(A,B,C) [A >= B] (?,1) 4. f8(A,B,C) -> f8(1 + A,B,1 + C) [B >= 1 + A && 0 >= 1 + E] (?,1) 5. f8(A,B,C) -> f8(1 + A,B,1 + C) [B >= 1 + A && E >= 1] (?,1) 6. f16(A,B,C) -> f4(A,B,C) [0 >= C] (?,1) 7. f16(A,B,C) -> f4(-1 + A,B,C) [C >= 1] (?,1) 8. f4(A,B,C) -> f20(A,B,C) [A >= B] (?,1) Signature: {(f0,3);(f16,3);(f20,3);(f4,3);(f8,3)} Flow Graph: [0->{1,8},1->{2,3,4,5},2->{6,7},3->{6,7},4->{2,3,4,5},5->{2,3,4,5},6->{1,8},7->{1,8},8->{}] Sizebounds: (<0,0,A>, ?) (<0,0,B>, ?) (<0,0,C>, ?) (<1,0,A>, ?) (<1,0,B>, ?) (<1,0,C>, ?) (<2,0,A>, ?) (<2,0,B>, ?) (<2,0,C>, ?) (<3,0,A>, ?) (<3,0,B>, ?) (<3,0,C>, ?) (<4,0,A>, ?) (<4,0,B>, ?) (<4,0,C>, ?) (<5,0,A>, ?) (<5,0,B>, ?) (<5,0,C>, ?) (<6,0,A>, ?) (<6,0,B>, ?) (<6,0,C>, ?) (<7,0,A>, ?) (<7,0,B>, ?) (<7,0,C>, ?) (<8,0,A>, ?) (<8,0,B>, ?) (<8,0,C>, ?) + Applied Processor: SizeboundsProc + Details: Sizebounds computed: (<0,0,A>, 0) (<0,0,B>, B) (<0,0,C>, C) (<1,0,A>, B) (<1,0,B>, B) (<1,0,C>, 0) (<2,0,A>, B) (<2,0,B>, B) (<2,0,C>, ?) (<3,0,A>, B) (<3,0,B>, B) (<3,0,C>, ?) (<4,0,A>, B) (<4,0,B>, B) (<4,0,C>, ?) (<5,0,A>, B) (<5,0,B>, B) (<5,0,C>, ?) (<6,0,A>, B) (<6,0,B>, B) (<6,0,C>, ?) (<7,0,A>, B) (<7,0,B>, B) (<7,0,C>, ?) (<8,0,A>, B) (<8,0,B>, B) (<8,0,C>, ?) * Step 4: LeafRules WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 0. f0(A,B,C) -> f4(0,B,C) True (1,1) 1. f4(A,B,C) -> f8(1 + A,B,0) [B >= 1 + A] (?,1) 2. f8(A,B,C) -> f16(A,B,C) [B >= 1 + A] (?,1) 3. f8(A,B,C) -> f16(A,B,C) [A >= B] (?,1) 4. f8(A,B,C) -> f8(1 + A,B,1 + C) [B >= 1 + A && 0 >= 1 + E] (?,1) 5. f8(A,B,C) -> f8(1 + A,B,1 + C) [B >= 1 + A && E >= 1] (?,1) 6. f16(A,B,C) -> f4(A,B,C) [0 >= C] (?,1) 7. f16(A,B,C) -> f4(-1 + A,B,C) [C >= 1] (?,1) 8. f4(A,B,C) -> f20(A,B,C) [A >= B] (?,1) Signature: {(f0,3);(f16,3);(f20,3);(f4,3);(f8,3)} Flow Graph: [0->{1,8},1->{2,3,4,5},2->{6,7},3->{6,7},4->{2,3,4,5},5->{2,3,4,5},6->{1,8},7->{1,8},8->{}] Sizebounds: (<0,0,A>, 0) (<0,0,B>, B) (<0,0,C>, C) (<1,0,A>, B) (<1,0,B>, B) (<1,0,C>, 0) (<2,0,A>, B) (<2,0,B>, B) (<2,0,C>, ?) (<3,0,A>, B) (<3,0,B>, B) (<3,0,C>, ?) (<4,0,A>, B) (<4,0,B>, B) (<4,0,C>, ?) (<5,0,A>, B) (<5,0,B>, B) (<5,0,C>, ?) (<6,0,A>, B) (<6,0,B>, B) (<6,0,C>, ?) (<7,0,A>, B) (<7,0,B>, B) (<7,0,C>, ?) (<8,0,A>, B) (<8,0,B>, B) (<8,0,C>, ?) + Applied Processor: LeafRules + Details: The following transitions are estimated by its predecessors and are removed [8] * Step 5: PolyRank WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 0. f0(A,B,C) -> f4(0,B,C) True (1,1) 1. f4(A,B,C) -> f8(1 + A,B,0) [B >= 1 + A] (?,1) 2. f8(A,B,C) -> f16(A,B,C) [B >= 1 + A] (?,1) 3. f8(A,B,C) -> f16(A,B,C) [A >= B] (?,1) 4. f8(A,B,C) -> f8(1 + A,B,1 + C) [B >= 1 + A && 0 >= 1 + E] (?,1) 5. f8(A,B,C) -> f8(1 + A,B,1 + C) [B >= 1 + A && E >= 1] (?,1) 6. f16(A,B,C) -> f4(A,B,C) [0 >= C] (?,1) 7. f16(A,B,C) -> f4(-1 + A,B,C) [C >= 1] (?,1) Signature: {(f0,3);(f16,3);(f20,3);(f4,3);(f8,3)} Flow Graph: [0->{1},1->{2,3,4,5},2->{6,7},3->{6,7},4->{2,3,4,5},5->{2,3,4,5},6->{1},7->{1}] Sizebounds: (<0,0,A>, 0) (<0,0,B>, B) (<0,0,C>, C) (<1,0,A>, B) (<1,0,B>, B) (<1,0,C>, 0) (<2,0,A>, B) (<2,0,B>, B) (<2,0,C>, ?) (<3,0,A>, B) (<3,0,B>, B) (<3,0,C>, ?) (<4,0,A>, B) (<4,0,B>, B) (<4,0,C>, ?) (<5,0,A>, B) (<5,0,B>, B) (<5,0,C>, ?) (<6,0,A>, B) (<6,0,B>, B) (<6,0,C>, ?) (<7,0,A>, B) (<7,0,B>, B) (<7,0,C>, ?) + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(f0) = x2 p(f16) = 1 + -1*x1 + x2 p(f4) = -1*x1 + x2 p(f8) = 1 + -1*x1 + x2 The following rules are strictly oriented: [B >= 1 + A && 0 >= 1 + E] ==> f8(A,B,C) = 1 + -1*A + B > -1*A + B = f8(1 + A,B,1 + C) [B >= 1 + A && E >= 1] ==> f8(A,B,C) = 1 + -1*A + B > -1*A + B = f8(1 + A,B,1 + C) The following rules are weakly oriented: True ==> f0(A,B,C) = B >= B = f4(0,B,C) [B >= 1 + A] ==> f4(A,B,C) = -1*A + B >= -1*A + B = f8(1 + A,B,0) [B >= 1 + A] ==> f8(A,B,C) = 1 + -1*A + B >= 1 + -1*A + B = f16(A,B,C) [A >= B] ==> f8(A,B,C) = 1 + -1*A + B >= 1 + -1*A + B = f16(A,B,C) [0 >= C] ==> f16(A,B,C) = 1 + -1*A + B >= -1*A + B = f4(A,B,C) [C >= 1] ==> f16(A,B,C) = 1 + -1*A + B >= 1 + -1*A + B = f4(-1 + A,B,C) * Step 6: ChainProcessor WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 0. f0(A,B,C) -> f4(0,B,C) True (1,1) 1. f4(A,B,C) -> f8(1 + A,B,0) [B >= 1 + A] (?,1) 2. f8(A,B,C) -> f16(A,B,C) [B >= 1 + A] (?,1) 3. f8(A,B,C) -> f16(A,B,C) [A >= B] (?,1) 4. f8(A,B,C) -> f8(1 + A,B,1 + C) [B >= 1 + A && 0 >= 1 + E] (B,1) 5. f8(A,B,C) -> f8(1 + A,B,1 + C) [B >= 1 + A && E >= 1] (B,1) 6. f16(A,B,C) -> f4(A,B,C) [0 >= C] (?,1) 7. f16(A,B,C) -> f4(-1 + A,B,C) [C >= 1] (?,1) Signature: {(f0,3);(f16,3);(f20,3);(f4,3);(f8,3)} Flow Graph: [0->{1},1->{2,3,4,5},2->{6,7},3->{6,7},4->{2,3,4,5},5->{2,3,4,5},6->{1},7->{1}] Sizebounds: (<0,0,A>, 0) (<0,0,B>, B) (<0,0,C>, C) (<1,0,A>, B) (<1,0,B>, B) (<1,0,C>, 0) (<2,0,A>, B) (<2,0,B>, B) (<2,0,C>, ?) (<3,0,A>, B) (<3,0,B>, B) (<3,0,C>, ?) (<4,0,A>, B) (<4,0,B>, B) (<4,0,C>, ?) (<5,0,A>, B) (<5,0,B>, B) (<5,0,C>, ?) (<6,0,A>, B) (<6,0,B>, B) (<6,0,C>, ?) (<7,0,A>, B) (<7,0,B>, B) (<7,0,C>, ?) + Applied Processor: ChainProcessor False [0,1,2,3,4,5,6,7] + Details: We chained rule 0 to obtain the rules [8] . * Step 7: ChainProcessor WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 1. f4(A,B,C) -> f8(1 + A,B,0) [B >= 1 + A] (?,1) 2. f8(A,B,C) -> f16(A,B,C) [B >= 1 + A] (?,1) 3. f8(A,B,C) -> f16(A,B,C) [A >= B] (?,1) 4. f8(A,B,C) -> f8(1 + A,B,1 + C) [B >= 1 + A && 0 >= 1 + E] (B,1) 5. f8(A,B,C) -> f8(1 + A,B,1 + C) [B >= 1 + A && E >= 1] (B,1) 6. f16(A,B,C) -> f4(A,B,C) [0 >= C] (?,1) 7. f16(A,B,C) -> f4(-1 + A,B,C) [C >= 1] (?,1) 8. f0(A,B,C) -> f8(1,B,0) [B >= 1] (1,2) Signature: {(f0,3);(f16,3);(f20,3);(f4,3);(f8,3)} Flow Graph: [1->{2,3,4,5},2->{6,7},3->{6,7},4->{2,3,4,5},5->{2,3,4,5},6->{1},7->{1},8->{2,3,4,5}] Sizebounds: (<1,0,A>, B) (<1,0,B>, B) (<1,0,C>, 0) (<2,0,A>, B) (<2,0,B>, B) (<2,0,C>, ?) (<3,0,A>, B) (<3,0,B>, B) (<3,0,C>, ?) (<4,0,A>, B) (<4,0,B>, B) (<4,0,C>, ?) (<5,0,A>, B) (<5,0,B>, B) (<5,0,C>, ?) (<6,0,A>, B) (<6,0,B>, B) (<6,0,C>, ?) (<7,0,A>, B) (<7,0,B>, B) (<7,0,C>, ?) (<8,0,A>, B) (<8,0,B>, B) (<8,0,C>, 0) + Applied Processor: ChainProcessor False [1,2,3,4,5,6,7,8] + Details: We chained rule 2 to obtain the rules [9,10] . * Step 8: ChainProcessor WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 1. f4(A,B,C) -> f8(1 + A,B,0) [B >= 1 + A] (?,1) 3. f8(A,B,C) -> f16(A,B,C) [A >= B] (?,1) 4. f8(A,B,C) -> f8(1 + A,B,1 + C) [B >= 1 + A && 0 >= 1 + E] (B,1) 5. f8(A,B,C) -> f8(1 + A,B,1 + C) [B >= 1 + A && E >= 1] (B,1) 6. f16(A,B,C) -> f4(A,B,C) [0 >= C] (?,1) 7. f16(A,B,C) -> f4(-1 + A,B,C) [C >= 1] (?,1) 8. f0(A,B,C) -> f8(1,B,0) [B >= 1] (1,2) 9. f8(A,B,C) -> f4(A,B,C) [B >= 1 + A && 0 >= C] (?,2) 10. f8(A,B,C) -> f4(-1 + A,B,C) [B >= 1 + A && C >= 1] (?,2) Signature: {(f0,3);(f16,3);(f20,3);(f4,3);(f8,3)} Flow Graph: [1->{3,4,5,9,10},3->{6,7},4->{3,4,5,9,10},5->{3,4,5,9,10},6->{1},7->{1},8->{3,4,5,9,10},9->{1},10->{1}] Sizebounds: (< 1,0,A>, B) (< 1,0,B>, B) (< 1,0,C>, 0) (< 3,0,A>, B) (< 3,0,B>, B) (< 3,0,C>, ?) (< 4,0,A>, B) (< 4,0,B>, B) (< 4,0,C>, ?) (< 5,0,A>, B) (< 5,0,B>, B) (< 5,0,C>, ?) (< 6,0,A>, B) (< 6,0,B>, B) (< 6,0,C>, ?) (< 7,0,A>, B) (< 7,0,B>, B) (< 7,0,C>, ?) (< 8,0,A>, B) (< 8,0,B>, B) (< 8,0,C>, 0) (< 9,0,A>, B) (< 9,0,B>, B) (< 9,0,C>, ?) (<10,0,A>, B) (<10,0,B>, B) (<10,0,C>, ?) + Applied Processor: ChainProcessor False [1,3,4,5,6,7,8,9,10] + Details: We chained rule 3 to obtain the rules [11,12] . * Step 9: UnreachableRules WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 1. f4(A,B,C) -> f8(1 + A,B,0) [B >= 1 + A] (?,1) 4. f8(A,B,C) -> f8(1 + A,B,1 + C) [B >= 1 + A && 0 >= 1 + E] (B,1) 5. f8(A,B,C) -> f8(1 + A,B,1 + C) [B >= 1 + A && E >= 1] (B,1) 6. f16(A,B,C) -> f4(A,B,C) [0 >= C] (?,1) 7. f16(A,B,C) -> f4(-1 + A,B,C) [C >= 1] (?,1) 8. f0(A,B,C) -> f8(1,B,0) [B >= 1] (1,2) 9. f8(A,B,C) -> f4(A,B,C) [B >= 1 + A && 0 >= C] (?,2) 10. f8(A,B,C) -> f4(-1 + A,B,C) [B >= 1 + A && C >= 1] (?,2) 11. f8(A,B,C) -> f4(A,B,C) [A >= B && 0 >= C] (?,2) 12. f8(A,B,C) -> f4(-1 + A,B,C) [A >= B && C >= 1] (?,2) Signature: {(f0,3);(f16,3);(f20,3);(f4,3);(f8,3)} Flow Graph: [1->{4,5,9,10,11,12},4->{4,5,9,10,11,12},5->{4,5,9,10,11,12},6->{1},7->{1},8->{4,5,9,10,11,12},9->{1} ,10->{1},11->{1},12->{1}] Sizebounds: (< 1,0,A>, B) (< 1,0,B>, B) (< 1,0,C>, 0) (< 4,0,A>, B) (< 4,0,B>, B) (< 4,0,C>, ?) (< 5,0,A>, B) (< 5,0,B>, B) (< 5,0,C>, ?) (< 6,0,A>, B) (< 6,0,B>, B) (< 6,0,C>, ?) (< 7,0,A>, B) (< 7,0,B>, B) (< 7,0,C>, ?) (< 8,0,A>, B) (< 8,0,B>, B) (< 8,0,C>, 0) (< 9,0,A>, B) (< 9,0,B>, B) (< 9,0,C>, ?) (<10,0,A>, B) (<10,0,B>, B) (<10,0,C>, ?) (<11,0,A>, B) (<11,0,B>, B) (<11,0,C>, ?) (<12,0,A>, B) (<12,0,B>, B) (<12,0,C>, ?) + Applied Processor: UnreachableRules + Details: The following transitions are not reachable from the starting states and are removed: [6,7] * Step 10: ChainProcessor WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 1. f4(A,B,C) -> f8(1 + A,B,0) [B >= 1 + A] (?,1) 4. f8(A,B,C) -> f8(1 + A,B,1 + C) [B >= 1 + A && 0 >= 1 + E] (B,1) 5. f8(A,B,C) -> f8(1 + A,B,1 + C) [B >= 1 + A && E >= 1] (B,1) 8. f0(A,B,C) -> f8(1,B,0) [B >= 1] (1,2) 9. f8(A,B,C) -> f4(A,B,C) [B >= 1 + A && 0 >= C] (?,2) 10. f8(A,B,C) -> f4(-1 + A,B,C) [B >= 1 + A && C >= 1] (?,2) 11. f8(A,B,C) -> f4(A,B,C) [A >= B && 0 >= C] (?,2) 12. f8(A,B,C) -> f4(-1 + A,B,C) [A >= B && C >= 1] (?,2) Signature: {(f0,3);(f16,3);(f20,3);(f4,3);(f8,3)} Flow Graph: [1->{4,5,9,10,11,12},4->{4,5,9,10,11,12},5->{4,5,9,10,11,12},8->{4,5,9,10,11,12},9->{1},10->{1},11->{1} ,12->{1}] Sizebounds: (< 1,0,A>, B) (< 1,0,B>, B) (< 1,0,C>, 0) (< 4,0,A>, B) (< 4,0,B>, B) (< 4,0,C>, ?) (< 5,0,A>, B) (< 5,0,B>, B) (< 5,0,C>, ?) (< 8,0,A>, B) (< 8,0,B>, B) (< 8,0,C>, 0) (< 9,0,A>, B) (< 9,0,B>, B) (< 9,0,C>, ?) (<10,0,A>, B) (<10,0,B>, B) (<10,0,C>, ?) (<11,0,A>, B) (<11,0,B>, B) (<11,0,C>, ?) (<12,0,A>, B) (<12,0,B>, B) (<12,0,C>, ?) + Applied Processor: ChainProcessor False [1,4,5,8,9,10,11,12] + Details: We chained rule 9 to obtain the rules [13] . * Step 11: ChainProcessor WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 1. f4(A,B,C) -> f8(1 + A,B,0) [B >= 1 + A] (?,1) 4. f8(A,B,C) -> f8(1 + A,B,1 + C) [B >= 1 + A && 0 >= 1 + E] (B,1) 5. f8(A,B,C) -> f8(1 + A,B,1 + C) [B >= 1 + A && E >= 1] (B,1) 8. f0(A,B,C) -> f8(1,B,0) [B >= 1] (1,2) 10. f8(A,B,C) -> f4(-1 + A,B,C) [B >= 1 + A && C >= 1] (?,2) 11. f8(A,B,C) -> f4(A,B,C) [A >= B && 0 >= C] (?,2) 12. f8(A,B,C) -> f4(-1 + A,B,C) [A >= B && C >= 1] (?,2) 13. f8(A,B,C) -> f8(1 + A,B,0) [B >= 1 + A && 0 >= C && B >= 1 + A] (?,3) Signature: {(f0,3);(f16,3);(f20,3);(f4,3);(f8,3)} Flow Graph: [1->{4,5,10,11,12,13},4->{4,5,10,11,12,13},5->{4,5,10,11,12,13},8->{4,5,10,11,12,13},10->{1},11->{1} ,12->{1},13->{4,5,10,11,12,13}] Sizebounds: (< 1,0,A>, B) (< 1,0,B>, B) (< 1,0,C>, 0) (< 4,0,A>, B) (< 4,0,B>, B) (< 4,0,C>, ?) (< 5,0,A>, B) (< 5,0,B>, B) (< 5,0,C>, ?) (< 8,0,A>, B) (< 8,0,B>, B) (< 8,0,C>, 0) (<10,0,A>, B) (<10,0,B>, B) (<10,0,C>, ?) (<11,0,A>, B) (<11,0,B>, B) (<11,0,C>, ?) (<12,0,A>, B) (<12,0,B>, B) (<12,0,C>, ?) (<13,0,A>, B) (<13,0,B>, B) (<13,0,C>, 0) + Applied Processor: ChainProcessor False [1,4,5,8,10,11,12,13] + Details: We chained rule 10 to obtain the rules [14] . * Step 12: ChainProcessor WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 1. f4(A,B,C) -> f8(1 + A,B,0) [B >= 1 + A] (?,1) 4. f8(A,B,C) -> f8(1 + A,B,1 + C) [B >= 1 + A && 0 >= 1 + E] (B,1) 5. f8(A,B,C) -> f8(1 + A,B,1 + C) [B >= 1 + A && E >= 1] (B,1) 8. f0(A,B,C) -> f8(1,B,0) [B >= 1] (1,2) 11. f8(A,B,C) -> f4(A,B,C) [A >= B && 0 >= C] (?,2) 12. f8(A,B,C) -> f4(-1 + A,B,C) [A >= B && C >= 1] (?,2) 13. f8(A,B,C) -> f8(1 + A,B,0) [B >= 1 + A && 0 >= C && B >= 1 + A] (?,3) 14. f8(A,B,C) -> f8(A,B,0) [B >= 1 + A && C >= 1 && B >= A] (?,3) Signature: {(f0,3);(f16,3);(f20,3);(f4,3);(f8,3)} Flow Graph: [1->{4,5,11,12,13,14},4->{4,5,11,12,13,14},5->{4,5,11,12,13,14},8->{4,5,11,12,13,14},11->{1},12->{1} ,13->{4,5,11,12,13,14},14->{4,5,11,12,13,14}] Sizebounds: (< 1,0,A>, B) (< 1,0,B>, B) (< 1,0,C>, 0) (< 4,0,A>, B) (< 4,0,B>, B) (< 4,0,C>, ?) (< 5,0,A>, B) (< 5,0,B>, B) (< 5,0,C>, ?) (< 8,0,A>, B) (< 8,0,B>, B) (< 8,0,C>, 0) (<11,0,A>, B) (<11,0,B>, B) (<11,0,C>, ?) (<12,0,A>, B) (<12,0,B>, B) (<12,0,C>, ?) (<13,0,A>, B) (<13,0,B>, B) (<13,0,C>, 0) (<14,0,A>, B) (<14,0,B>, B) (<14,0,C>, 0) + Applied Processor: ChainProcessor False [1,4,5,8,11,12,13,14] + Details: We chained rule 11 to obtain the rules [15] . * Step 13: ChainProcessor WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 1. f4(A,B,C) -> f8(1 + A,B,0) [B >= 1 + A] (?,1) 4. f8(A,B,C) -> f8(1 + A,B,1 + C) [B >= 1 + A && 0 >= 1 + E] (B,1) 5. f8(A,B,C) -> f8(1 + A,B,1 + C) [B >= 1 + A && E >= 1] (B,1) 8. f0(A,B,C) -> f8(1,B,0) [B >= 1] (1,2) 12. f8(A,B,C) -> f4(-1 + A,B,C) [A >= B && C >= 1] (?,2) 13. f8(A,B,C) -> f8(1 + A,B,0) [B >= 1 + A && 0 >= C && B >= 1 + A] (?,3) 14. f8(A,B,C) -> f8(A,B,0) [B >= 1 + A && C >= 1 && B >= A] (?,3) 15. f8(A,B,C) -> f8(1 + A,B,0) [A >= B && 0 >= C && B >= 1 + A] (?,3) Signature: {(f0,3);(f16,3);(f20,3);(f4,3);(f8,3)} Flow Graph: [1->{4,5,12,13,14,15},4->{4,5,12,13,14,15},5->{4,5,12,13,14,15},8->{4,5,12,13,14,15},12->{1},13->{4,5,12 ,13,14,15},14->{4,5,12,13,14,15},15->{4,5,12,13,14,15}] Sizebounds: (< 1,0,A>, B) (< 1,0,B>, B) (< 1,0,C>, 0) (< 4,0,A>, B) (< 4,0,B>, B) (< 4,0,C>, ?) (< 5,0,A>, B) (< 5,0,B>, B) (< 5,0,C>, ?) (< 8,0,A>, B) (< 8,0,B>, B) (< 8,0,C>, 0) (<12,0,A>, B) (<12,0,B>, B) (<12,0,C>, ?) (<13,0,A>, B) (<13,0,B>, B) (<13,0,C>, 0) (<14,0,A>, B) (<14,0,B>, B) (<14,0,C>, 0) (<15,0,A>, B) (<15,0,B>, B) (<15,0,C>, 0) + Applied Processor: ChainProcessor False [1,4,5,8,12,13,14,15] + Details: We chained rule 12 to obtain the rules [16] . * Step 14: UnreachableRules WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 1. f4(A,B,C) -> f8(1 + A,B,0) [B >= 1 + A] (?,1) 4. f8(A,B,C) -> f8(1 + A,B,1 + C) [B >= 1 + A && 0 >= 1 + E] (B,1) 5. f8(A,B,C) -> f8(1 + A,B,1 + C) [B >= 1 + A && E >= 1] (B,1) 8. f0(A,B,C) -> f8(1,B,0) [B >= 1] (1,2) 13. f8(A,B,C) -> f8(1 + A,B,0) [B >= 1 + A && 0 >= C && B >= 1 + A] (?,3) 14. f8(A,B,C) -> f8(A,B,0) [B >= 1 + A && C >= 1 && B >= A] (?,3) 15. f8(A,B,C) -> f8(1 + A,B,0) [A >= B && 0 >= C && B >= 1 + A] (?,3) 16. f8(A,B,C) -> f8(A,B,0) [A >= B && C >= 1 && B >= A] (?,3) Signature: {(f0,3);(f16,3);(f20,3);(f4,3);(f8,3)} Flow Graph: [1->{4,5,13,14,15,16},4->{4,5,13,14,15,16},5->{4,5,13,14,15,16},8->{4,5,13,14,15,16},13->{4,5,13,14,15,16} ,14->{4,5,13,14,15,16},15->{4,5,13,14,15,16},16->{4,5,13,14,15,16}] Sizebounds: (< 1,0,A>, B) (< 1,0,B>, B) (< 1,0,C>, 0) (< 4,0,A>, B) (< 4,0,B>, B) (< 4,0,C>, ?) (< 5,0,A>, B) (< 5,0,B>, B) (< 5,0,C>, ?) (< 8,0,A>, B) (< 8,0,B>, B) (< 8,0,C>, 0) (<13,0,A>, B) (<13,0,B>, B) (<13,0,C>, 0) (<14,0,A>, B) (<14,0,B>, B) (<14,0,C>, 0) (<15,0,A>, B) (<15,0,B>, B) (<15,0,C>, 0) (<16,0,A>, B) (<16,0,B>, B) (<16,0,C>, 0) + Applied Processor: UnreachableRules + Details: The following transitions are not reachable from the starting states and are removed: [1] * Step 15: UnsatPaths WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 4. f8(A,B,C) -> f8(1 + A,B,1 + C) [B >= 1 + A && 0 >= 1 + E] (B,1) 5. f8(A,B,C) -> f8(1 + A,B,1 + C) [B >= 1 + A && E >= 1] (B,1) 8. f0(A,B,C) -> f8(1,B,0) [B >= 1] (1,2) 13. f8(A,B,C) -> f8(1 + A,B,0) [B >= 1 + A && 0 >= C && B >= 1 + A] (?,3) 14. f8(A,B,C) -> f8(A,B,0) [B >= 1 + A && C >= 1 && B >= A] (?,3) 15. f8(A,B,C) -> f8(1 + A,B,0) [A >= B && 0 >= C && B >= 1 + A] (?,3) 16. f8(A,B,C) -> f8(A,B,0) [A >= B && C >= 1 && B >= A] (?,3) Signature: {(f0,3);(f16,3);(f20,3);(f4,3);(f8,3)} Flow Graph: [4->{4,5,13,14,15,16},5->{4,5,13,14,15,16},8->{4,5,13,14,15,16},13->{4,5,13,14,15,16},14->{4,5,13,14,15 ,16},15->{4,5,13,14,15,16},16->{4,5,13,14,15,16}] Sizebounds: (< 4,0,A>, B) (< 4,0,B>, B) (< 4,0,C>, ?) (< 5,0,A>, B) (< 5,0,B>, B) (< 5,0,C>, ?) (< 8,0,A>, B) (< 8,0,B>, B) (< 8,0,C>, 0) (<13,0,A>, B) (<13,0,B>, B) (<13,0,C>, 0) (<14,0,A>, B) (<14,0,B>, B) (<14,0,C>, 0) (<15,0,A>, B) (<15,0,B>, B) (<15,0,C>, 0) (<16,0,A>, B) (<16,0,B>, B) (<16,0,C>, 0) + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(4,15) ,(5,15) ,(8,14) ,(8,15) ,(8,16) ,(13,14) ,(13,15) ,(13,16) ,(14,14) ,(14,15) ,(14,16) ,(15,4) ,(15,5) ,(15,13) ,(15,14) ,(15,15) ,(15,16) ,(16,4) ,(16,5) ,(16,13) ,(16,14) ,(16,15) ,(16,16)] * Step 16: UnreachableRules WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 4. f8(A,B,C) -> f8(1 + A,B,1 + C) [B >= 1 + A && 0 >= 1 + E] (B,1) 5. f8(A,B,C) -> f8(1 + A,B,1 + C) [B >= 1 + A && E >= 1] (B,1) 8. f0(A,B,C) -> f8(1,B,0) [B >= 1] (1,2) 13. f8(A,B,C) -> f8(1 + A,B,0) [B >= 1 + A && 0 >= C && B >= 1 + A] (?,3) 14. f8(A,B,C) -> f8(A,B,0) [B >= 1 + A && C >= 1 && B >= A] (?,3) 15. f8(A,B,C) -> f8(1 + A,B,0) [A >= B && 0 >= C && B >= 1 + A] (?,3) 16. f8(A,B,C) -> f8(A,B,0) [A >= B && C >= 1 && B >= A] (?,3) Signature: {(f0,3);(f16,3);(f20,3);(f4,3);(f8,3)} Flow Graph: [4->{4,5,13,14,16},5->{4,5,13,14,16},8->{4,5,13},13->{4,5,13},14->{4,5,13},15->{},16->{}] Sizebounds: (< 4,0,A>, B) (< 4,0,B>, B) (< 4,0,C>, ?) (< 5,0,A>, B) (< 5,0,B>, B) (< 5,0,C>, ?) (< 8,0,A>, B) (< 8,0,B>, B) (< 8,0,C>, 0) (<13,0,A>, B) (<13,0,B>, B) (<13,0,C>, 0) (<14,0,A>, B) (<14,0,B>, B) (<14,0,C>, 0) (<15,0,A>, B) (<15,0,B>, B) (<15,0,C>, 0) (<16,0,A>, B) (<16,0,B>, B) (<16,0,C>, 0) + Applied Processor: UnreachableRules + Details: The following transitions are not reachable from the starting states and are removed: [15] * Step 17: LeafRules WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 4. f8(A,B,C) -> f8(1 + A,B,1 + C) [B >= 1 + A && 0 >= 1 + E] (B,1) 5. f8(A,B,C) -> f8(1 + A,B,1 + C) [B >= 1 + A && E >= 1] (B,1) 8. f0(A,B,C) -> f8(1,B,0) [B >= 1] (1,2) 13. f8(A,B,C) -> f8(1 + A,B,0) [B >= 1 + A && 0 >= C && B >= 1 + A] (?,3) 14. f8(A,B,C) -> f8(A,B,0) [B >= 1 + A && C >= 1 && B >= A] (?,3) 16. f8(A,B,C) -> f8(A,B,0) [A >= B && C >= 1 && B >= A] (?,3) Signature: {(f0,3);(f16,3);(f20,3);(f4,3);(f8,3)} Flow Graph: [4->{4,5,13,14,16},5->{4,5,13,14,16},8->{4,5,13},13->{4,5,13},14->{4,5,13},16->{}] Sizebounds: (< 4,0,A>, B) (< 4,0,B>, B) (< 4,0,C>, ?) (< 5,0,A>, B) (< 5,0,B>, B) (< 5,0,C>, ?) (< 8,0,A>, B) (< 8,0,B>, B) (< 8,0,C>, 0) (<13,0,A>, B) (<13,0,B>, B) (<13,0,C>, 0) (<14,0,A>, B) (<14,0,B>, B) (<14,0,C>, 0) (<16,0,A>, B) (<16,0,B>, B) (<16,0,C>, 0) + Applied Processor: LeafRules + Details: The following transitions are estimated by its predecessors and are removed [16] * Step 18: LocalSizeboundsProc WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 4. f8(A,B,C) -> f8(1 + A,B,1 + C) [B >= 1 + A && 0 >= 1 + E] (B,1) 5. f8(A,B,C) -> f8(1 + A,B,1 + C) [B >= 1 + A && E >= 1] (B,1) 8. f0(A,B,C) -> f8(1,B,0) [B >= 1] (1,2) 13. f8(A,B,C) -> f8(1 + A,B,0) [B >= 1 + A && 0 >= C && B >= 1 + A] (?,3) 14. f8(A,B,C) -> f8(A,B,0) [B >= 1 + A && C >= 1 && B >= A] (?,3) Signature: {(f0,3);(f16,3);(f20,3);(f4,3);(f8,3)} Flow Graph: [4->{4,5,13,14},5->{4,5,13,14},8->{4,5,13},13->{4,5,13},14->{4,5,13}] Sizebounds: (< 4,0,A>, B) (< 4,0,B>, B) (< 4,0,C>, ?) (< 5,0,A>, B) (< 5,0,B>, B) (< 5,0,C>, ?) (< 8,0,A>, B) (< 8,0,B>, B) (< 8,0,C>, 0) (<13,0,A>, B) (<13,0,B>, B) (<13,0,C>, 0) (<14,0,A>, B) (<14,0,B>, B) (<14,0,C>, 0) + Applied Processor: LocalSizeboundsProc + Details: LocalSizebounds generated; rvgraph (< 4,0,A>, 1 + A, .+ 1) (< 4,0,B>, B, .= 0) (< 4,0,C>, 1 + C, .+ 1) (< 5,0,A>, 1 + A, .+ 1) (< 5,0,B>, B, .= 0) (< 5,0,C>, 1 + C, .+ 1) (< 8,0,A>, 1, .= 1) (< 8,0,B>, B, .= 0) (< 8,0,C>, 0, .= 0) (<13,0,A>, 1 + A, .+ 1) (<13,0,B>, B, .= 0) (<13,0,C>, 0, .= 0) (<14,0,A>, A, .= 0) (<14,0,B>, B, .= 0) (<14,0,C>, 0, .= 0) * Step 19: SizeboundsProc WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 4. f8(A,B,C) -> f8(1 + A,B,1 + C) [B >= 1 + A && 0 >= 1 + E] (B,1) 5. f8(A,B,C) -> f8(1 + A,B,1 + C) [B >= 1 + A && E >= 1] (B,1) 8. f0(A,B,C) -> f8(1,B,0) [B >= 1] (1,2) 13. f8(A,B,C) -> f8(1 + A,B,0) [B >= 1 + A && 0 >= C && B >= 1 + A] (?,3) 14. f8(A,B,C) -> f8(A,B,0) [B >= 1 + A && C >= 1 && B >= A] (?,3) Signature: {(f0,3);(f16,3);(f20,3);(f4,3);(f8,3)} Flow Graph: [4->{4,5,13,14},5->{4,5,13,14},8->{4,5,13},13->{4,5,13},14->{4,5,13}] Sizebounds: (< 4,0,A>, ?) (< 4,0,B>, ?) (< 4,0,C>, ?) (< 5,0,A>, ?) (< 5,0,B>, ?) (< 5,0,C>, ?) (< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, ?) (<13,0,A>, ?) (<13,0,B>, ?) (<13,0,C>, ?) (<14,0,A>, ?) (<14,0,B>, ?) (<14,0,C>, ?) + Applied Processor: SizeboundsProc + Details: Sizebounds computed: (< 4,0,A>, B) (< 4,0,B>, B) (< 4,0,C>, 2*B) (< 5,0,A>, B) (< 5,0,B>, B) (< 5,0,C>, 2*B) (< 8,0,A>, 1) (< 8,0,B>, B) (< 8,0,C>, 0) (<13,0,A>, B) (<13,0,B>, B) (<13,0,C>, 0) (<14,0,A>, B) (<14,0,B>, B) (<14,0,C>, 0) * Step 20: LocationConstraintsProc WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 4. f8(A,B,C) -> f8(1 + A,B,1 + C) [B >= 1 + A && 0 >= 1 + E] (B,1) 5. f8(A,B,C) -> f8(1 + A,B,1 + C) [B >= 1 + A && E >= 1] (B,1) 8. f0(A,B,C) -> f8(1,B,0) [B >= 1] (1,2) 13. f8(A,B,C) -> f8(1 + A,B,0) [B >= 1 + A && 0 >= C && B >= 1 + A] (?,3) 14. f8(A,B,C) -> f8(A,B,0) [B >= 1 + A && C >= 1 && B >= A] (?,3) Signature: {(f0,3);(f16,3);(f20,3);(f4,3);(f8,3)} Flow Graph: [4->{4,5,13,14},5->{4,5,13,14},8->{4,5,13},13->{4,5,13},14->{4,5,13}] Sizebounds: (< 4,0,A>, B) (< 4,0,B>, B) (< 4,0,C>, 2*B) (< 5,0,A>, B) (< 5,0,B>, B) (< 5,0,C>, 2*B) (< 8,0,A>, 1) (< 8,0,B>, B) (< 8,0,C>, 0) (<13,0,A>, B) (<13,0,B>, B) (<13,0,C>, 0) (<14,0,A>, B) (<14,0,B>, B) (<14,0,C>, 0) + Applied Processor: LocationConstraintsProc + Details: We computed the location constraints 4 : [B >= A] 5 : [B >= A] 8 : True 13 : [B >= A] 14 : [B >= A] . * Step 21: PolyRank WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 4. f8(A,B,C) -> f8(1 + A,B,1 + C) [B >= 1 + A && 0 >= 1 + E] (B,1) 5. f8(A,B,C) -> f8(1 + A,B,1 + C) [B >= 1 + A && E >= 1] (B,1) 8. f0(A,B,C) -> f8(1,B,0) [B >= 1] (1,2) 13. f8(A,B,C) -> f8(1 + A,B,0) [B >= 1 + A && 0 >= C && B >= 1 + A] (?,3) 14. f8(A,B,C) -> f8(A,B,0) [B >= 1 + A && C >= 1 && B >= A] (?,3) Signature: {(f0,3);(f16,3);(f20,3);(f4,3);(f8,3)} Flow Graph: [4->{4,5,13,14},5->{4,5,13,14},8->{4,5,13},13->{4,5,13},14->{4,5,13}] Sizebounds: (< 4,0,A>, B) (< 4,0,B>, B) (< 4,0,C>, 2*B) (< 5,0,A>, B) (< 5,0,B>, B) (< 5,0,C>, 2*B) (< 8,0,A>, 1) (< 8,0,B>, B) (< 8,0,C>, 0) (<13,0,A>, B) (<13,0,B>, B) (<13,0,C>, 0) (<14,0,A>, B) (<14,0,B>, B) (<14,0,C>, 0) + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(f0) = x2 p(f8) = -1*x1 + x2 The following rules are strictly oriented: [B >= 1 + A && 0 >= 1 + E] ==> f8(A,B,C) = -1*A + B > -1 + -1*A + B = f8(1 + A,B,1 + C) [B >= 1 + A && E >= 1] ==> f8(A,B,C) = -1*A + B > -1 + -1*A + B = f8(1 + A,B,1 + C) [B >= 1] ==> f0(A,B,C) = B > -1 + B = f8(1,B,0) [B >= 1 + A && 0 >= C && B >= 1 + A] ==> f8(A,B,C) = -1*A + B > -1 + -1*A + B = f8(1 + A,B,0) The following rules are weakly oriented: [B >= 1 + A && C >= 1 && B >= A] ==> f8(A,B,C) = -1*A + B >= -1*A + B = f8(A,B,0) * Step 22: PolyRank WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 4. f8(A,B,C) -> f8(1 + A,B,1 + C) [B >= 1 + A && 0 >= 1 + E] (B,1) 5. f8(A,B,C) -> f8(1 + A,B,1 + C) [B >= 1 + A && E >= 1] (B,1) 8. f0(A,B,C) -> f8(1,B,0) [B >= 1] (1,2) 13. f8(A,B,C) -> f8(1 + A,B,0) [B >= 1 + A && 0 >= C && B >= 1 + A] (B,3) 14. f8(A,B,C) -> f8(A,B,0) [B >= 1 + A && C >= 1 && B >= A] (?,3) Signature: {(f0,3);(f16,3);(f20,3);(f4,3);(f8,3)} Flow Graph: [4->{4,5,13,14},5->{4,5,13,14},8->{4,5,13},13->{4,5,13},14->{4,5,13}] Sizebounds: (< 4,0,A>, B) (< 4,0,B>, B) (< 4,0,C>, 2*B) (< 5,0,A>, B) (< 5,0,B>, B) (< 5,0,C>, 2*B) (< 8,0,A>, 1) (< 8,0,B>, B) (< 8,0,C>, 0) (<13,0,A>, B) (<13,0,B>, B) (<13,0,C>, 0) (<14,0,A>, B) (<14,0,B>, B) (<14,0,C>, 0) + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [4,5,14], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(f8) = -1*x1 + x2 + x3 The following rules are strictly oriented: [B >= 1 + A && C >= 1 && B >= A] ==> f8(A,B,C) = -1*A + B + C > -1*A + B = f8(A,B,0) The following rules are weakly oriented: [B >= 1 + A && 0 >= 1 + E] ==> f8(A,B,C) = -1*A + B + C >= -1*A + B + C = f8(1 + A,B,1 + C) [B >= 1 + A && E >= 1] ==> f8(A,B,C) = -1*A + B + C >= -1*A + B + C = f8(1 + A,B,1 + C) We use the following global sizebounds: (< 4,0,A>, B) (< 4,0,B>, B) (< 4,0,C>, 2*B) (< 5,0,A>, B) (< 5,0,B>, B) (< 5,0,C>, 2*B) (< 8,0,A>, 1) (< 8,0,B>, B) (< 8,0,C>, 0) (<13,0,A>, B) (<13,0,B>, B) (<13,0,C>, 0) (<14,0,A>, B) (<14,0,B>, B) (<14,0,C>, 0) * Step 23: KnowledgePropagation WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 4. f8(A,B,C) -> f8(1 + A,B,1 + C) [B >= 1 + A && 0 >= 1 + E] (B,1) 5. f8(A,B,C) -> f8(1 + A,B,1 + C) [B >= 1 + A && E >= 1] (B,1) 8. f0(A,B,C) -> f8(1,B,0) [B >= 1] (1,2) 13. f8(A,B,C) -> f8(1 + A,B,0) [B >= 1 + A && 0 >= C && B >= 1 + A] (B,3) 14. f8(A,B,C) -> f8(A,B,0) [B >= 1 + A && C >= 1 && B >= A] (1 + B + 2*B^2,3) Signature: {(f0,3);(f16,3);(f20,3);(f4,3);(f8,3)} Flow Graph: [4->{4,5,13,14},5->{4,5,13,14},8->{4,5,13},13->{4,5,13},14->{4,5,13}] Sizebounds: (< 4,0,A>, B) (< 4,0,B>, B) (< 4,0,C>, 2*B) (< 5,0,A>, B) (< 5,0,B>, B) (< 5,0,C>, 2*B) (< 8,0,A>, 1) (< 8,0,B>, B) (< 8,0,C>, 0) (<13,0,A>, B) (<13,0,B>, B) (<13,0,C>, 0) (<14,0,A>, B) (<14,0,B>, B) (<14,0,C>, 0) + Applied Processor: KnowledgePropagation + Details: The problem is already solved. WORST_CASE(?,O(n^2))