Trying to load file: main.koat Initial Control flow graph problem: Start location: f2 0: f69 -> f71 : [ 0>=1+free ], cost: 1 1: f69 -> f71 : [ free_1>=1 ], cost: 1 12: f69 -> f71 : [], cost: 1 16: f71 -> f23 : D'=1+A, [ A==D ], cost: 1 13: f71 -> f74 : Q'=free_9, [ A>=1+D ], cost: 1 14: f71 -> f74 : Q'=free_10, [ D>=1+A ], cost: 1 2: f2 -> f5 : [], cost: 1 3: f5 -> f9 : C'=0, [ A>=B ], cost: 1 30: f5 -> f23 : [ B>=1+A ], cost: 1 27: f9 -> f5 : B'=1+B, [ 0>=1+C && D>=1+A ], cost: 1 28: f9 -> f5 : B'=1+B, [ C>=1 && D>=1+A ], cost: 1 29: f9 -> f5 : B'=1+B, C'=0, [ D>=1+A && C==0 ], cost: 1 4: f9 -> f9 : D'=1+D, E'=free_2, F'=free_2, [ C>=free_2 && A>=D ], cost: 1 5: f9 -> f9 : C'=free_3, D'=1+D, E'=free_3, F'=free_3, [ free_3>=1+C && A>=D ], cost: 1 6: f23 -> f26 : [ A>=D ], cost: 1 26: f23 -> f1 : [ D>=1+A ], cost: 1 7: f26 -> f30 : G'=free_4, [ D>=1+B ], cost: 1 25: f26 -> f40 : C'=0, [ B>=D ], cost: 1 24: f30 -> f26 : B'=1+B, [ H>=B ], cost: 1 8: f30 -> f30 : G'=free_5, H'=1+H, [ B>=1+H ], cost: 1 23: f40 -> f69 : K'=D, [ B>=1+A && D==K ], cost: 1 9: f40 -> f44 : G'=free_6, [ A>=B ], cost: 1 21: f40 -> f59 : [ B>=1+A && K>=1+D ], cost: 1 22: f40 -> f59 : [ B>=1+A && D>=1+K ], cost: 1 19: f44 -> f40 : B'=1+B, Q'=free_12, J'=free_11, [ C>=1+free_12 && H>=D ], cost: 1 20: f44 -> f40 : B'=1+B, C'=free_13, Q'=free_13, J'=free_14, K'=B, [ free_13>=C && H>=D ], cost: 1 10: f44 -> f44 : G'=free_7, H'=1+H, [ D>=1+H ], cost: 1 18: f59 -> f69 : [ H>=1+A ], cost: 1 11: f59 -> f59 : H'=1+H, Q'=free_8, [ A>=H ], cost: 1 17: f74 -> f23 : D'=1+D, [ B>=1+A ], cost: 1 15: f74 -> f74 : B'=1+B, [ A>=B ], cost: 1 Removing duplicate transition: 0. Removing duplicate transition: 1. Simplified the transitions: Start location: f2 12: f69 -> f71 : [], cost: 1 16: f71 -> f23 : D'=1+A, [ A==D ], cost: 1 13: f71 -> f74 : Q'=free_9, [ A>=1+D ], cost: 1 14: f71 -> f74 : Q'=free_10, [ D>=1+A ], cost: 1 2: f2 -> f5 : [], cost: 1 3: f5 -> f9 : C'=0, [ A>=B ], cost: 1 30: f5 -> f23 : [ B>=1+A ], cost: 1 27: f9 -> f5 : B'=1+B, [ 0>=1+C && D>=1+A ], cost: 1 28: f9 -> f5 : B'=1+B, [ C>=1 && D>=1+A ], cost: 1 29: f9 -> f5 : B'=1+B, C'=0, [ D>=1+A && C==0 ], cost: 1 4: f9 -> f9 : D'=1+D, E'=free_2, F'=free_2, [ C>=free_2 && A>=D ], cost: 1 5: f9 -> f9 : C'=free_3, D'=1+D, E'=free_3, F'=free_3, [ free_3>=1+C && A>=D ], cost: 1 6: f23 -> f26 : [ A>=D ], cost: 1 7: f26 -> f30 : G'=free_4, [ D>=1+B ], cost: 1 25: f26 -> f40 : C'=0, [ B>=D ], cost: 1 24: f30 -> f26 : B'=1+B, [ H>=B ], cost: 1 8: f30 -> f30 : G'=free_5, H'=1+H, [ B>=1+H ], cost: 1 23: f40 -> f69 : K'=D, [ B>=1+A && D==K ], cost: 1 9: f40 -> f44 : G'=free_6, [ A>=B ], cost: 1 21: f40 -> f59 : [ B>=1+A && K>=1+D ], cost: 1 22: f40 -> f59 : [ B>=1+A && D>=1+K ], cost: 1 19: f44 -> f40 : B'=1+B, Q'=free_12, J'=free_11, [ C>=1+free_12 && H>=D ], cost: 1 20: f44 -> f40 : B'=1+B, C'=free_13, Q'=free_13, J'=free_14, K'=B, [ free_13>=C && H>=D ], cost: 1 10: f44 -> f44 : G'=free_7, H'=1+H, [ D>=1+H ], cost: 1 18: f59 -> f69 : [ H>=1+A ], cost: 1 11: f59 -> f59 : H'=1+H, Q'=free_8, [ A>=H ], cost: 1 17: f74 -> f23 : D'=1+D, [ B>=1+A ], cost: 1 15: f74 -> f74 : B'=1+B, [ A>=B ], cost: 1 Eliminating 2 self-loops for location f9 Self-Loop 4 has the metering function: 1-D+A, resulting in the new transition 31. Self-Loop 5 has the metering function: 1-D+A, resulting in the new transition 32. Removing the self-loops: 4 5. Eliminating 1 self-loops for location f30 Self-Loop 8 has the metering function: -H+B, resulting in the new transition 33. Removing the self-loops: 8. Eliminating 1 self-loops for location f44 Self-Loop 10 has the metering function: -H+D, resulting in the new transition 34. Removing the self-loops: 10. Eliminating 1 self-loops for location f59 Self-Loop 11 has the metering function: 1-H+A, resulting in the new transition 35. Removing the self-loops: 11. Eliminating 1 self-loops for location f74 Self-Loop 15 has the metering function: 1-B+A, resulting in the new transition 36. Removing the self-loops: 15. Removed all Self-loops using metering functions (where possible): Start location: f2 12: f69 -> f71 : [], cost: 1 16: f71 -> f23 : D'=1+A, [ A==D ], cost: 1 13: f71 -> f74 : Q'=free_9, [ A>=1+D ], cost: 1 14: f71 -> f74 : Q'=free_10, [ D>=1+A ], cost: 1 2: f2 -> f5 : [], cost: 1 3: f5 -> f9 : C'=0, [ A>=B ], cost: 1 30: f5 -> f23 : [ B>=1+A ], cost: 1 31: f9 -> [13] : D'=1+A, E'=free_2, F'=free_2, [ C>=free_2 && A>=D ], cost: 1-D+A 32: f9 -> [13] : C'=1+C-D+A, D'=1+A, E'=1+C-D+A, F'=1+C-D+A, [ 1+C>=1+C && A>=D ], cost: 1-D+A 6: f23 -> f26 : [ A>=D ], cost: 1 7: f26 -> f30 : G'=free_4, [ D>=1+B ], cost: 1 25: f26 -> f40 : C'=0, [ B>=D ], cost: 1 33: f30 -> [14] : G'=free_5, H'=B, [ B>=1+H ], cost: -H+B 23: f40 -> f69 : K'=D, [ B>=1+A && D==K ], cost: 1 9: f40 -> f44 : G'=free_6, [ A>=B ], cost: 1 21: f40 -> f59 : [ B>=1+A && K>=1+D ], cost: 1 22: f40 -> f59 : [ B>=1+A && D>=1+K ], cost: 1 34: f44 -> [15] : G'=free_7, H'=D, [ D>=1+H ], cost: -H+D 35: f59 -> [16] : H'=1+A, Q'=free_8, [ A>=H ], cost: 1-H+A 36: f74 -> [17] : B'=1+A, [ A>=B ], cost: 1-B+A 27: [13] -> f5 : B'=1+B, [ 0>=1+C && D>=1+A ], cost: 1 28: [13] -> f5 : B'=1+B, [ C>=1 && D>=1+A ], cost: 1 29: [13] -> f5 : B'=1+B, C'=0, [ D>=1+A && C==0 ], cost: 1 24: [14] -> f26 : B'=1+B, [ H>=B ], cost: 1 19: [15] -> f40 : B'=1+B, Q'=free_12, J'=free_11, [ C>=1+free_12 && H>=D ], cost: 1 20: [15] -> f40 : B'=1+B, C'=free_13, Q'=free_13, J'=free_14, K'=B, [ free_13>=C && H>=D ], cost: 1 18: [16] -> f69 : [ H>=1+A ], cost: 1 17: [17] -> f23 : D'=1+D, [ B>=1+A ], cost: 1 Applied simple chaining: Start location: f2 12: f69 -> f71 : [], cost: 1 16: f71 -> f23 : D'=1+A, [ A==D ], cost: 1 13: f71 -> f74 : Q'=free_9, [ A>=1+D ], cost: 1 14: f71 -> f74 : Q'=free_10, [ D>=1+A ], cost: 1 2: f2 -> f5 : [], cost: 1 3: f5 -> f9 : C'=0, [ A>=B ], cost: 1 30: f5 -> f23 : [ B>=1+A ], cost: 1 31: f9 -> [13] : D'=1+A, E'=free_2, F'=free_2, [ C>=free_2 && A>=D ], cost: 1-D+A 32: f9 -> [13] : C'=1+C-D+A, D'=1+A, E'=1+C-D+A, F'=1+C-D+A, [ 1+C>=1+C && A>=D ], cost: 1-D+A 6: f23 -> f26 : [ A>=D ], cost: 1 7: f26 -> f26 : B'=1+B, G'=free_5, H'=B, [ D>=1+B && B>=1+H && B>=B ], cost: 2-H+B 25: f26 -> f40 : C'=0, [ B>=D ], cost: 1 23: f40 -> f69 : K'=D, [ B>=1+A && D==K ], cost: 1 21: f40 -> f59 : [ B>=1+A && K>=1+D ], cost: 1 22: f40 -> f59 : [ B>=1+A && D>=1+K ], cost: 1 9: f40 -> [15] : G'=free_7, H'=D, [ A>=B && D>=1+H ], cost: 1-H+D 35: f59 -> f69 : H'=1+A, Q'=free_8, [ A>=H && 1+A>=1+A ], cost: 2-H+A 36: f74 -> f23 : B'=1+A, D'=1+D, [ A>=B && 1+A>=1+A ], cost: 2-B+A 27: [13] -> f5 : B'=1+B, [ 0>=1+C && D>=1+A ], cost: 1 28: [13] -> f5 : B'=1+B, [ C>=1 && D>=1+A ], cost: 1 29: [13] -> f5 : B'=1+B, C'=0, [ D>=1+A && C==0 ], cost: 1 19: [15] -> f40 : B'=1+B, Q'=free_12, J'=free_11, [ C>=1+free_12 && H>=D ], cost: 1 20: [15] -> f40 : B'=1+B, C'=free_13, Q'=free_13, J'=free_14, K'=B, [ free_13>=C && H>=D ], cost: 1 Eliminating 1 self-loops for location f26 Self-Loop 7 has the metering function: -B+D, resulting in the new transition 37. Removing the self-loops: 7. Removed all Self-loops using metering functions (where possible): Start location: f2 12: f69 -> f71 : [], cost: 1 16: f71 -> f23 : D'=1+A, [ A==D ], cost: 1 13: f71 -> f74 : Q'=free_9, [ A>=1+D ], cost: 1 14: f71 -> f74 : Q'=free_10, [ D>=1+A ], cost: 1 2: f2 -> f5 : [], cost: 1 3: f5 -> f9 : C'=0, [ A>=B ], cost: 1 30: f5 -> f23 : [ B>=1+A ], cost: 1 31: f9 -> [13] : D'=1+A, E'=free_2, F'=free_2, [ C>=free_2 && A>=D ], cost: 1-D+A 32: f9 -> [13] : C'=1+C-D+A, D'=1+A, E'=1+C-D+A, F'=1+C-D+A, [ 1+C>=1+C && A>=D ], cost: 1-D+A 6: f23 -> f26 : [ A>=D ], cost: 1 37: f26 -> [18] : B'=D, G'=free_5, H'=-1+D, [ D>=1+B && B>=1+H ], cost: -3*B+3*D 23: f40 -> f69 : K'=D, [ B>=1+A && D==K ], cost: 1 21: f40 -> f59 : [ B>=1+A && K>=1+D ], cost: 1 22: f40 -> f59 : [ B>=1+A && D>=1+K ], cost: 1 9: f40 -> [15] : G'=free_7, H'=D, [ A>=B && D>=1+H ], cost: 1-H+D 35: f59 -> f69 : H'=1+A, Q'=free_8, [ A>=H && 1+A>=1+A ], cost: 2-H+A 36: f74 -> f23 : B'=1+A, D'=1+D, [ A>=B && 1+A>=1+A ], cost: 2-B+A 27: [13] -> f5 : B'=1+B, [ 0>=1+C && D>=1+A ], cost: 1 28: [13] -> f5 : B'=1+B, [ C>=1 && D>=1+A ], cost: 1 29: [13] -> f5 : B'=1+B, C'=0, [ D>=1+A && C==0 ], cost: 1 19: [15] -> f40 : B'=1+B, Q'=free_12, J'=free_11, [ C>=1+free_12 && H>=D ], cost: 1 20: [15] -> f40 : B'=1+B, C'=free_13, Q'=free_13, J'=free_14, K'=B, [ free_13>=C && H>=D ], cost: 1 25: [18] -> f40 : C'=0, [ B>=D ], cost: 1 Applied simple chaining: Start location: f2 12: f69 -> f71 : [], cost: 1 16: f71 -> f23 : D'=1+A, [ A==D ], cost: 1 13: f71 -> f74 : Q'=free_9, [ A>=1+D ], cost: 1 14: f71 -> f74 : Q'=free_10, [ D>=1+A ], cost: 1 2: f2 -> f5 : [], cost: 1 3: f5 -> f9 : C'=0, [ A>=B ], cost: 1 30: f5 -> f23 : [ B>=1+A ], cost: 1 31: f9 -> [13] : D'=1+A, E'=free_2, F'=free_2, [ C>=free_2 && A>=D ], cost: 1-D+A 32: f9 -> [13] : C'=1+C-D+A, D'=1+A, E'=1+C-D+A, F'=1+C-D+A, [ 1+C>=1+C && A>=D ], cost: 1-D+A 6: f23 -> f40 : B'=D, C'=0, G'=free_5, H'=-1+D, [ A>=D && D>=1+B && B>=1+H && D>=D ], cost: 2-3*B+3*D 23: f40 -> f69 : K'=D, [ B>=1+A && D==K ], cost: 1 21: f40 -> f59 : [ B>=1+A && K>=1+D ], cost: 1 22: f40 -> f59 : [ B>=1+A && D>=1+K ], cost: 1 9: f40 -> [15] : G'=free_7, H'=D, [ A>=B && D>=1+H ], cost: 1-H+D 35: f59 -> f69 : H'=1+A, Q'=free_8, [ A>=H && 1+A>=1+A ], cost: 2-H+A 36: f74 -> f23 : B'=1+A, D'=1+D, [ A>=B && 1+A>=1+A ], cost: 2-B+A 27: [13] -> f5 : B'=1+B, [ 0>=1+C && D>=1+A ], cost: 1 28: [13] -> f5 : B'=1+B, [ C>=1 && D>=1+A ], cost: 1 29: [13] -> f5 : B'=1+B, C'=0, [ D>=1+A && C==0 ], cost: 1 19: [15] -> f40 : B'=1+B, Q'=free_12, J'=free_11, [ C>=1+free_12 && H>=D ], cost: 1 20: [15] -> f40 : B'=1+B, C'=free_13, Q'=free_13, J'=free_14, K'=B, [ free_13>=C && H>=D ], cost: 1 Applied chaining over branches and pruning: Start location: f2 44: f69 -> f23 : D'=1+A, [ A==D ], cost: 2 45: f69 -> f74 : Q'=free_9, [ A>=1+D ], cost: 2 46: f69 -> f74 : Q'=free_10, [ D>=1+A ], cost: 2 2: f2 -> f5 : [], cost: 1 30: f5 -> f23 : [ B>=1+A ], cost: 1 38: f5 -> [13] : C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D ], cost: 2-D+A 39: f5 -> [13] : C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && 1>=1 && A>=D ], cost: 2-D+A 6: f23 -> f40 : B'=D, C'=0, G'=free_5, H'=-1+D, [ A>=D && D>=1+B && B>=1+H && D>=D ], cost: 2-3*B+3*D 23: f40 -> f69 : K'=D, [ B>=1+A && D==K ], cost: 1 40: f40 -> f69 : H'=1+A, Q'=free_8, [ B>=1+A && K>=1+D && A>=H && 1+A>=1+A ], cost: 3-H+A 41: f40 -> f69 : H'=1+A, Q'=free_8, [ B>=1+A && D>=1+K && A>=H && 1+A>=1+A ], cost: 3-H+A 42: f40 -> f40 : B'=1+B, G'=free_7, H'=D, Q'=free_12, J'=free_11, [ A>=B && D>=1+H && C>=1+free_12 && D>=D ], cost: 2-H+D 43: f40 -> f40 : B'=1+B, C'=free_13, G'=free_7, H'=D, Q'=free_13, J'=free_14, K'=B, [ A>=B && D>=1+H && free_13>=C && D>=D ], cost: 2-H+D 36: f74 -> f23 : B'=1+A, D'=1+D, [ A>=B && 1+A>=1+A ], cost: 2-B+A 27: [13] -> f5 : B'=1+B, [ 0>=1+C && D>=1+A ], cost: 1 28: [13] -> f5 : B'=1+B, [ C>=1 && D>=1+A ], cost: 1 29: [13] -> f5 : B'=1+B, C'=0, [ D>=1+A && C==0 ], cost: 1 Eliminating 2 self-loops for location f40 Removing the self-loops: 42 43. Adding an epsilon transition (to model nonexecution of the loops): 49. Removed all Self-loops using metering functions (where possible): Start location: f2 44: f69 -> f23 : D'=1+A, [ A==D ], cost: 2 45: f69 -> f74 : Q'=free_9, [ A>=1+D ], cost: 2 46: f69 -> f74 : Q'=free_10, [ D>=1+A ], cost: 2 2: f2 -> f5 : [], cost: 1 30: f5 -> f23 : [ B>=1+A ], cost: 1 38: f5 -> [13] : C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D ], cost: 2-D+A 39: f5 -> [13] : C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && 1>=1 && A>=D ], cost: 2-D+A 6: f23 -> f40 : B'=D, C'=0, G'=free_5, H'=-1+D, [ A>=D && D>=1+B && B>=1+H && D>=D ], cost: 2-3*B+3*D 47: f40 -> [19] : B'=1+B, G'=free_7, H'=D, Q'=free_12, J'=free_11, [ A>=B && D>=1+H && C>=1+free_12 ], cost: 2-H+D 48: f40 -> [19] : B'=1+B, C'=free_13, G'=free_7, H'=D, Q'=free_13, J'=free_14, K'=B, [ A>=B && D>=1+H && free_13>=C ], cost: 2-H+D 49: f40 -> [19] : [], cost: 0 36: f74 -> f23 : B'=1+A, D'=1+D, [ A>=B && 1+A>=1+A ], cost: 2-B+A 27: [13] -> f5 : B'=1+B, [ 0>=1+C && D>=1+A ], cost: 1 28: [13] -> f5 : B'=1+B, [ C>=1 && D>=1+A ], cost: 1 29: [13] -> f5 : B'=1+B, C'=0, [ D>=1+A && C==0 ], cost: 1 23: [19] -> f69 : K'=D, [ B>=1+A && D==K ], cost: 1 40: [19] -> f69 : H'=1+A, Q'=free_8, [ B>=1+A && K>=1+D && A>=H && 1+A>=1+A ], cost: 3-H+A 41: [19] -> f69 : H'=1+A, Q'=free_8, [ B>=1+A && D>=1+K && A>=H && 1+A>=1+A ], cost: 3-H+A Applied chaining over branches and pruning: Start location: f2 2: f2 -> f5 : [], cost: 1 52: f5 -> f5 : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+A>=1+A && 0==0 ], cost: 3-D+A 54: f5 -> f5 : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && 1>=1 && A>=D && 1-D+A>=1 && 1+A>=1+A ], cost: 3-D+A 30: f5 -> f23 : [ B>=1+A ], cost: 1 50: f5 -> [20] : C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D ], cost: 2-D+A 51: f5 -> [21] : C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D ], cost: 2-D+A 53: f5 -> [22] : C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && 1>=1 && A>=D ], cost: 2-D+A 55: f5 -> [23] : C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && 1>=1 && A>=D ], cost: 2-D+A 56: f23 -> [19] : B'=1+D, C'=0, G'=free_7, H'=D, Q'=free_12, J'=free_11, [ A>=D && D>=1+B && B>=1+H && D>=D && A>=D && D>=D && 0>=1+free_12 ], cost: 5-3*B+3*D 57: f23 -> [19] : B'=1+D, C'=free_13, G'=free_7, H'=D, Q'=free_13, J'=free_14, K'=D, [ A>=D && D>=1+B && B>=1+H && D>=D && A>=D && D>=D && free_13>=0 ], cost: 5-3*B+3*D 58: f23 -> [19] : B'=D, C'=0, G'=free_5, H'=-1+D, [ A>=D && D>=1+B && B>=1+H && D>=D ], cost: 2-3*B+3*D 36: f74 -> f23 : B'=1+A, D'=1+D, [ A>=B && 1+A>=1+A ], cost: 2-B+A 59: [19] -> f23 : D'=1+A, K'=D, [ B>=1+A && D==K && A==D ], cost: 3 62: [19] -> f23 : D'=1+A, H'=1+A, Q'=free_8, [ B>=1+A && K>=1+D && A>=H && 1+A>=1+A && A==D ], cost: 5-H+A 65: [19] -> f23 : D'=1+A, H'=1+A, Q'=free_8, [ B>=1+A && D>=1+K && A>=H && 1+A>=1+A && A==D ], cost: 5-H+A 60: [19] -> f74 : Q'=free_9, K'=D, [ B>=1+A && D==K && A>=1+D ], cost: 3 63: [19] -> f74 : H'=1+A, Q'=free_9, [ B>=1+A && K>=1+D && A>=H && 1+A>=1+A && A>=1+D ], cost: 5-H+A 64: [19] -> f74 : H'=1+A, Q'=free_10, [ B>=1+A && K>=1+D && A>=H && 1+A>=1+A && D>=1+A ], cost: 5-H+A 66: [19] -> f74 : H'=1+A, Q'=free_9, [ B>=1+A && D>=1+K && A>=H && 1+A>=1+A && A>=1+D ], cost: 5-H+A 67: [19] -> f74 : H'=1+A, Q'=free_10, [ B>=1+A && D>=1+K && A>=H && 1+A>=1+A && D>=1+A ], cost: 5-H+A Eliminating 2 self-loops for location f5 Removing the self-loops: 52 54. Adding an epsilon transition (to model nonexecution of the loops): 70. Removed all Self-loops using metering functions (where possible): Start location: f2 2: f2 -> f5 : [], cost: 1 68: f5 -> [24] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D ], cost: 3-D+A 69: f5 -> [24] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D ], cost: 3-D+A 70: f5 -> [24] : [], cost: 0 56: f23 -> [19] : B'=1+D, C'=0, G'=free_7, H'=D, Q'=free_12, J'=free_11, [ A>=D && D>=1+B && B>=1+H && D>=D && A>=D && D>=D && 0>=1+free_12 ], cost: 5-3*B+3*D 57: f23 -> [19] : B'=1+D, C'=free_13, G'=free_7, H'=D, Q'=free_13, J'=free_14, K'=D, [ A>=D && D>=1+B && B>=1+H && D>=D && A>=D && D>=D && free_13>=0 ], cost: 5-3*B+3*D 58: f23 -> [19] : B'=D, C'=0, G'=free_5, H'=-1+D, [ A>=D && D>=1+B && B>=1+H && D>=D ], cost: 2-3*B+3*D 36: f74 -> f23 : B'=1+A, D'=1+D, [ A>=B && 1+A>=1+A ], cost: 2-B+A 59: [19] -> f23 : D'=1+A, K'=D, [ B>=1+A && D==K && A==D ], cost: 3 62: [19] -> f23 : D'=1+A, H'=1+A, Q'=free_8, [ B>=1+A && K>=1+D && A>=H && 1+A>=1+A && A==D ], cost: 5-H+A 65: [19] -> f23 : D'=1+A, H'=1+A, Q'=free_8, [ B>=1+A && D>=1+K && A>=H && 1+A>=1+A && A==D ], cost: 5-H+A 60: [19] -> f74 : Q'=free_9, K'=D, [ B>=1+A && D==K && A>=1+D ], cost: 3 63: [19] -> f74 : H'=1+A, Q'=free_9, [ B>=1+A && K>=1+D && A>=H && 1+A>=1+A && A>=1+D ], cost: 5-H+A 64: [19] -> f74 : H'=1+A, Q'=free_10, [ B>=1+A && K>=1+D && A>=H && 1+A>=1+A && D>=1+A ], cost: 5-H+A 66: [19] -> f74 : H'=1+A, Q'=free_9, [ B>=1+A && D>=1+K && A>=H && 1+A>=1+A && A>=1+D ], cost: 5-H+A 67: [19] -> f74 : H'=1+A, Q'=free_10, [ B>=1+A && D>=1+K && A>=H && 1+A>=1+A && D>=1+A ], cost: 5-H+A 30: [24] -> f23 : [ B>=1+A ], cost: 1 50: [24] -> [20] : C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D ], cost: 2-D+A 51: [24] -> [21] : C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D ], cost: 2-D+A 53: [24] -> [22] : C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && 1>=1 && A>=D ], cost: 2-D+A 55: [24] -> [23] : C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && 1>=1 && A>=D ], cost: 2-D+A Applied chaining over branches and pruning: Start location: f2 71: f2 -> [24] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D ], cost: 4-D+A 72: f2 -> [24] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D ], cost: 4-D+A 73: f2 -> [24] : [], cost: 1 74: f23 -> f23 : B'=1+D, C'=0, D'=1+A, G'=free_7, H'=D, Q'=free_12, J'=free_11, K'=D, [ A>=D && D>=1+B && B>=1+H && D>=D && A>=D && D>=D && 0>=1+free_12 && 1+D>=1+A && D==K && A==D ], cost: 8-3*B+3*D 75: f23 -> f23 : B'=1+D, C'=0, D'=1+A, G'=free_7, H'=1+A, Q'=free_8, J'=free_11, [ A>=D && D>=1+B && B>=1+H && D>=D && A>=D && D>=D && 0>=1+free_12 && 1+D>=1+A && K>=1+D && A>=D && 1+A>=1+A && A==D ], cost: 10-3*B+2*D+A 76: f23 -> f23 : B'=1+D, C'=0, D'=1+A, G'=free_7, H'=1+A, Q'=free_8, J'=free_11, [ A>=D && D>=1+B && B>=1+H && D>=D && A>=D && D>=D && 0>=1+free_12 && 1+D>=1+A && D>=1+K && A>=D && 1+A>=1+A && A==D ], cost: 10-3*B+2*D+A 82: f23 -> f23 : B'=1+D, C'=free_13, D'=1+A, G'=free_7, H'=D, Q'=free_13, J'=free_14, K'=D, [ A>=D && D>=1+B && B>=1+H && D>=D && A>=D && D>=D && free_13>=0 && 1+D>=1+A && D==D && A==D ], cost: 8-3*B+3*D 77: f23 -> [25] : B'=1+D, C'=0, G'=free_7, H'=D, Q'=free_12, J'=free_11, [ A>=D && D>=1+B && B>=1+H && D>=D && A>=D && D>=D && 0>=1+free_12 ], cost: 5-3*B+3*D 78: f23 -> [26] : B'=1+D, C'=0, G'=free_7, H'=D, Q'=free_12, J'=free_11, [ A>=D && D>=1+B && B>=1+H && D>=D && A>=D && D>=D && 0>=1+free_12 ], cost: 5-3*B+3*D 79: f23 -> [27] : B'=1+D, C'=0, G'=free_7, H'=D, Q'=free_12, J'=free_11, [ A>=D && D>=1+B && B>=1+H && D>=D && A>=D && D>=D && 0>=1+free_12 ], cost: 5-3*B+3*D 80: f23 -> [28] : B'=1+D, C'=0, G'=free_7, H'=D, Q'=free_12, J'=free_11, [ A>=D && D>=1+B && B>=1+H && D>=D && A>=D && D>=D && 0>=1+free_12 ], cost: 5-3*B+3*D 81: f23 -> [29] : B'=1+D, C'=0, G'=free_7, H'=D, Q'=free_12, J'=free_11, [ A>=D && D>=1+B && B>=1+H && D>=D && A>=D && D>=D && 0>=1+free_12 ], cost: 5-3*B+3*D 83: f23 -> [30] : B'=1+D, C'=free_13, G'=free_7, H'=D, Q'=free_13, J'=free_14, K'=D, [ A>=D && D>=1+B && B>=1+H && D>=D && A>=D && D>=D && free_13>=0 ], cost: 5-3*B+3*D 84: f23 -> [31] : B'=1+D, C'=free_13, G'=free_7, H'=D, Q'=free_13, J'=free_14, K'=D, [ A>=D && D>=1+B && B>=1+H && D>=D && A>=D && D>=D && free_13>=0 ], cost: 5-3*B+3*D 85: f23 -> [32] : B'=1+D, C'=free_13, G'=free_7, H'=D, Q'=free_13, J'=free_14, K'=D, [ A>=D && D>=1+B && B>=1+H && D>=D && A>=D && D>=D && free_13>=0 ], cost: 5-3*B+3*D 86: f23 -> [33] : B'=1+D, C'=free_13, G'=free_7, H'=D, Q'=free_13, J'=free_14, K'=D, [ A>=D && D>=1+B && B>=1+H && D>=D && A>=D && D>=D && free_13>=0 ], cost: 5-3*B+3*D 87: f23 -> [34] : B'=1+D, C'=free_13, G'=free_7, H'=D, Q'=free_13, J'=free_14, K'=D, [ A>=D && D>=1+B && B>=1+H && D>=D && A>=D && D>=D && free_13>=0 ], cost: 5-3*B+3*D 88: f23 -> [35] : B'=1+D, C'=free_13, G'=free_7, H'=D, Q'=free_13, J'=free_14, K'=D, [ A>=D && D>=1+B && B>=1+H && D>=D && A>=D && D>=D && free_13>=0 ], cost: 5-3*B+3*D 89: f23 -> [36] : B'=1+D, C'=free_13, G'=free_7, H'=D, Q'=free_13, J'=free_14, K'=D, [ A>=D && D>=1+B && B>=1+H && D>=D && A>=D && D>=D && free_13>=0 ], cost: 5-3*B+3*D 90: f23 -> [37] : B'=D, C'=0, G'=free_5, H'=-1+D, [ A>=D && D>=1+B && B>=1+H && D>=D ], cost: 2-3*B+3*D 91: f23 -> [38] : B'=D, C'=0, G'=free_5, H'=-1+D, [ A>=D && D>=1+B && B>=1+H && D>=D ], cost: 2-3*B+3*D 92: f23 -> [39] : B'=D, C'=0, G'=free_5, H'=-1+D, [ A>=D && D>=1+B && B>=1+H && D>=D ], cost: 2-3*B+3*D 93: f23 -> [40] : B'=D, C'=0, G'=free_5, H'=-1+D, [ A>=D && D>=1+B && B>=1+H && D>=D ], cost: 2-3*B+3*D 94: f23 -> [41] : B'=D, C'=0, G'=free_5, H'=-1+D, [ A>=D && D>=1+B && B>=1+H && D>=D ], cost: 2-3*B+3*D 95: f23 -> [42] : B'=D, C'=0, G'=free_5, H'=-1+D, [ A>=D && D>=1+B && B>=1+H && D>=D ], cost: 2-3*B+3*D 96: f23 -> [43] : B'=D, C'=0, G'=free_5, H'=-1+D, [ A>=D && D>=1+B && B>=1+H && D>=D ], cost: 2-3*B+3*D 97: f23 -> [44] : B'=D, C'=0, G'=free_5, H'=-1+D, [ A>=D && D>=1+B && B>=1+H && D>=D ], cost: 2-3*B+3*D 30: [24] -> f23 : [ B>=1+A ], cost: 1 50: [24] -> [20] : C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D ], cost: 2-D+A 51: [24] -> [21] : C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D ], cost: 2-D+A 53: [24] -> [22] : C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && 1>=1 && A>=D ], cost: 2-D+A 55: [24] -> [23] : C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && 1>=1 && A>=D ], cost: 2-D+A Eliminating 4 self-loops for location f23 Self-Loop 74 has the metering function: meter, resulting in the new transition 98. Self-Loop 75 has the metering function: -D+A, resulting in the new transition 99. Self-Loop 76 has the metering function: -D+A, resulting in the new transition 100. Self-Loop 82 has the metering function: -D+A, resulting in the new transition 101. Removing the self-loops: 74 75 76 82. Removed all Self-loops using metering functions (where possible): Start location: f2 71: f2 -> [24] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D ], cost: 4-D+A 72: f2 -> [24] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D ], cost: 4-D+A 73: f2 -> [24] : [], cost: 1 98: f23 -> [45] : B'=2+A, C'=0, D'=1+A, G'=free_7, H'=1+A, Q'=free_12, J'=free_11, K'=1+A, [ D>=1+B && B>=1+H && 0>=1+free_12 && D==K && A==D && 2*meter==K-2*D+A ], cost: 5*meter 99: f23 -> [45] : B'=2+A, C'=0, D'=1+A, G'=free_7, H'=1+A, Q'=free_8, J'=free_11, [ D>=1+B && B>=1+H && K>=1+D && A==D ], cost: -6*D+6*A 100: f23 -> [45] : B'=2+A, C'=0, D'=1+A, G'=free_7, H'=1+A, Q'=free_8, J'=free_11, [ D>=1+B && B>=1+H && D>=1+K && A==D ], cost: -6*D+6*A 101: f23 -> [45] : B'=2+A, C'=free_13, D'=1+A, G'=free_7, H'=1+A, Q'=free_13, J'=free_14, K'=1+A, [ D>=1+B && B>=1+H && free_13>=0 && A==D ], cost: -5*D+5*A 30: [24] -> f23 : [ B>=1+A ], cost: 1 50: [24] -> [20] : C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D ], cost: 2-D+A 51: [24] -> [21] : C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D ], cost: 2-D+A 53: [24] -> [22] : C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && 1>=1 && A>=D ], cost: 2-D+A 55: [24] -> [23] : C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && 1>=1 && A>=D ], cost: 2-D+A 77: [45] -> [25] : B'=1+D, C'=0, G'=free_7, H'=D, Q'=free_12, J'=free_11, [ A>=D && D>=1+B && B>=1+H && D>=D && A>=D && D>=D && 0>=1+free_12 ], cost: 5-3*B+3*D 78: [45] -> [26] : B'=1+D, C'=0, G'=free_7, H'=D, Q'=free_12, J'=free_11, [ A>=D && D>=1+B && B>=1+H && D>=D && A>=D && D>=D && 0>=1+free_12 ], cost: 5-3*B+3*D 79: [45] -> [27] : B'=1+D, C'=0, G'=free_7, H'=D, Q'=free_12, J'=free_11, [ A>=D && D>=1+B && B>=1+H && D>=D && A>=D && D>=D && 0>=1+free_12 ], cost: 5-3*B+3*D 80: [45] -> [28] : B'=1+D, C'=0, G'=free_7, H'=D, Q'=free_12, J'=free_11, [ A>=D && D>=1+B && B>=1+H && D>=D && A>=D && D>=D && 0>=1+free_12 ], cost: 5-3*B+3*D 81: [45] -> [29] : B'=1+D, C'=0, G'=free_7, H'=D, Q'=free_12, J'=free_11, [ A>=D && D>=1+B && B>=1+H && D>=D && A>=D && D>=D && 0>=1+free_12 ], cost: 5-3*B+3*D 83: [45] -> [30] : B'=1+D, C'=free_13, G'=free_7, H'=D, Q'=free_13, J'=free_14, K'=D, [ A>=D && D>=1+B && B>=1+H && D>=D && A>=D && D>=D && free_13>=0 ], cost: 5-3*B+3*D 84: [45] -> [31] : B'=1+D, C'=free_13, G'=free_7, H'=D, Q'=free_13, J'=free_14, K'=D, [ A>=D && D>=1+B && B>=1+H && D>=D && A>=D && D>=D && free_13>=0 ], cost: 5-3*B+3*D 85: [45] -> [32] : B'=1+D, C'=free_13, G'=free_7, H'=D, Q'=free_13, J'=free_14, K'=D, [ A>=D && D>=1+B && B>=1+H && D>=D && A>=D && D>=D && free_13>=0 ], cost: 5-3*B+3*D 86: [45] -> [33] : B'=1+D, C'=free_13, G'=free_7, H'=D, Q'=free_13, J'=free_14, K'=D, [ A>=D && D>=1+B && B>=1+H && D>=D && A>=D && D>=D && free_13>=0 ], cost: 5-3*B+3*D 87: [45] -> [34] : B'=1+D, C'=free_13, G'=free_7, H'=D, Q'=free_13, J'=free_14, K'=D, [ A>=D && D>=1+B && B>=1+H && D>=D && A>=D && D>=D && free_13>=0 ], cost: 5-3*B+3*D 88: [45] -> [35] : B'=1+D, C'=free_13, G'=free_7, H'=D, Q'=free_13, J'=free_14, K'=D, [ A>=D && D>=1+B && B>=1+H && D>=D && A>=D && D>=D && free_13>=0 ], cost: 5-3*B+3*D 89: [45] -> [36] : B'=1+D, C'=free_13, G'=free_7, H'=D, Q'=free_13, J'=free_14, K'=D, [ A>=D && D>=1+B && B>=1+H && D>=D && A>=D && D>=D && free_13>=0 ], cost: 5-3*B+3*D 90: [45] -> [37] : B'=D, C'=0, G'=free_5, H'=-1+D, [ A>=D && D>=1+B && B>=1+H && D>=D ], cost: 2-3*B+3*D 91: [45] -> [38] : B'=D, C'=0, G'=free_5, H'=-1+D, [ A>=D && D>=1+B && B>=1+H && D>=D ], cost: 2-3*B+3*D 92: [45] -> [39] : B'=D, C'=0, G'=free_5, H'=-1+D, [ A>=D && D>=1+B && B>=1+H && D>=D ], cost: 2-3*B+3*D 93: [45] -> [40] : B'=D, C'=0, G'=free_5, H'=-1+D, [ A>=D && D>=1+B && B>=1+H && D>=D ], cost: 2-3*B+3*D 94: [45] -> [41] : B'=D, C'=0, G'=free_5, H'=-1+D, [ A>=D && D>=1+B && B>=1+H && D>=D ], cost: 2-3*B+3*D 95: [45] -> [42] : B'=D, C'=0, G'=free_5, H'=-1+D, [ A>=D && D>=1+B && B>=1+H && D>=D ], cost: 2-3*B+3*D 96: [45] -> [43] : B'=D, C'=0, G'=free_5, H'=-1+D, [ A>=D && D>=1+B && B>=1+H && D>=D ], cost: 2-3*B+3*D 97: [45] -> [44] : B'=D, C'=0, G'=free_5, H'=-1+D, [ A>=D && D>=1+B && B>=1+H && D>=D ], cost: 2-3*B+3*D Applied chaining over branches and pruning: Start location: f2 102: f2 -> f23 : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 107: f2 -> f23 : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 112: f2 -> f23 : [ B>=1+A ], cost: 2 113: f2 -> [20] : C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D ], cost: 3-D+A 114: f2 -> [21] : C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D ], cost: 3-D+A 115: f2 -> [22] : C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && 1>=1 && A>=D ], cost: 3-D+A 116: f2 -> [23] : C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && 1>=1 && A>=D ], cost: 3-D+A 103: f2 -> [46] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D ], cost: 4-D+A 104: f2 -> [47] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D ], cost: 4-D+A 105: f2 -> [48] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D ], cost: 4-D+A 106: f2 -> [49] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D ], cost: 4-D+A 108: f2 -> [50] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D ], cost: 4-D+A 109: f2 -> [51] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D ], cost: 4-D+A 110: f2 -> [52] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D ], cost: 4-D+A 111: f2 -> [53] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D ], cost: 4-D+A 117: f23 -> [54] : B'=2+A, C'=0, D'=1+A, G'=free_7, H'=1+A, Q'=free_12, J'=free_11, K'=1+A, [ D>=1+B && B>=1+H && 0>=1+free_12 && D==K && A==D && 2*meter==K-2*D+A ], cost: 5*meter 118: f23 -> [55] : B'=2+A, C'=0, D'=1+A, G'=free_7, H'=1+A, Q'=free_12, J'=free_11, K'=1+A, [ D>=1+B && B>=1+H && 0>=1+free_12 && D==K && A==D && 2*meter==K-2*D+A ], cost: 5*meter 119: f23 -> [56] : B'=2+A, C'=0, D'=1+A, G'=free_7, H'=1+A, Q'=free_12, J'=free_11, K'=1+A, [ D>=1+B && B>=1+H && 0>=1+free_12 && D==K && A==D && 2*meter==K-2*D+A ], cost: 5*meter 120: f23 -> [57] : B'=2+A, C'=0, D'=1+A, G'=free_7, H'=1+A, Q'=free_12, J'=free_11, K'=1+A, [ D>=1+B && B>=1+H && 0>=1+free_12 && D==K && A==D && 2*meter==K-2*D+A ], cost: 5*meter 121: f23 -> [58] : B'=2+A, C'=0, D'=1+A, G'=free_7, H'=1+A, Q'=free_12, J'=free_11, K'=1+A, [ D>=1+B && B>=1+H && 0>=1+free_12 && D==K && A==D && 2*meter==K-2*D+A ], cost: 5*meter 122: f23 -> [59] : B'=2+A, C'=0, D'=1+A, G'=free_7, H'=1+A, Q'=free_12, J'=free_11, K'=1+A, [ D>=1+B && B>=1+H && 0>=1+free_12 && D==K && A==D && 2*meter==K-2*D+A ], cost: 5*meter 123: f23 -> [60] : B'=2+A, C'=0, D'=1+A, G'=free_7, H'=1+A, Q'=free_12, J'=free_11, K'=1+A, [ D>=1+B && B>=1+H && 0>=1+free_12 && D==K && A==D && 2*meter==K-2*D+A ], cost: 5*meter 124: f23 -> [61] : B'=2+A, C'=0, D'=1+A, G'=free_7, H'=1+A, Q'=free_12, J'=free_11, K'=1+A, [ D>=1+B && B>=1+H && 0>=1+free_12 && D==K && A==D && 2*meter==K-2*D+A ], cost: 5*meter 125: f23 -> [62] : B'=2+A, C'=0, D'=1+A, G'=free_7, H'=1+A, Q'=free_12, J'=free_11, K'=1+A, [ D>=1+B && B>=1+H && 0>=1+free_12 && D==K && A==D && 2*meter==K-2*D+A ], cost: 5*meter 126: f23 -> [63] : B'=2+A, C'=0, D'=1+A, G'=free_7, H'=1+A, Q'=free_12, J'=free_11, K'=1+A, [ D>=1+B && B>=1+H && 0>=1+free_12 && D==K && A==D && 2*meter==K-2*D+A ], cost: 5*meter 127: f23 -> [64] : B'=2+A, C'=0, D'=1+A, G'=free_7, H'=1+A, Q'=free_12, J'=free_11, K'=1+A, [ D>=1+B && B>=1+H && 0>=1+free_12 && D==K && A==D && 2*meter==K-2*D+A ], cost: 5*meter 128: f23 -> [65] : B'=2+A, C'=0, D'=1+A, G'=free_7, H'=1+A, Q'=free_12, J'=free_11, K'=1+A, [ D>=1+B && B>=1+H && 0>=1+free_12 && D==K && A==D && 2*meter==K-2*D+A ], cost: 5*meter 129: f23 -> [66] : B'=2+A, C'=0, D'=1+A, G'=free_7, H'=1+A, Q'=free_12, J'=free_11, K'=1+A, [ D>=1+B && B>=1+H && 0>=1+free_12 && D==K && A==D && 2*meter==K-2*D+A ], cost: 5*meter 130: f23 -> [67] : B'=2+A, C'=0, D'=1+A, G'=free_7, H'=1+A, Q'=free_12, J'=free_11, K'=1+A, [ D>=1+B && B>=1+H && 0>=1+free_12 && D==K && A==D && 2*meter==K-2*D+A ], cost: 5*meter 131: f23 -> [68] : B'=2+A, C'=0, D'=1+A, G'=free_7, H'=1+A, Q'=free_12, J'=free_11, K'=1+A, [ D>=1+B && B>=1+H && 0>=1+free_12 && D==K && A==D && 2*meter==K-2*D+A ], cost: 5*meter 132: f23 -> [69] : B'=2+A, C'=0, D'=1+A, G'=free_7, H'=1+A, Q'=free_12, J'=free_11, K'=1+A, [ D>=1+B && B>=1+H && 0>=1+free_12 && D==K && A==D && 2*meter==K-2*D+A ], cost: 5*meter 133: f23 -> [70] : B'=2+A, C'=0, D'=1+A, G'=free_7, H'=1+A, Q'=free_12, J'=free_11, K'=1+A, [ D>=1+B && B>=1+H && 0>=1+free_12 && D==K && A==D && 2*meter==K-2*D+A ], cost: 5*meter 134: f23 -> [71] : B'=2+A, C'=0, D'=1+A, G'=free_7, H'=1+A, Q'=free_12, J'=free_11, K'=1+A, [ D>=1+B && B>=1+H && 0>=1+free_12 && D==K && A==D && 2*meter==K-2*D+A ], cost: 5*meter 135: f23 -> [72] : B'=2+A, C'=0, D'=1+A, G'=free_7, H'=1+A, Q'=free_12, J'=free_11, K'=1+A, [ D>=1+B && B>=1+H && 0>=1+free_12 && D==K && A==D && 2*meter==K-2*D+A ], cost: 5*meter 136: f23 -> [73] : B'=2+A, C'=0, D'=1+A, G'=free_7, H'=1+A, Q'=free_12, J'=free_11, K'=1+A, [ D>=1+B && B>=1+H && 0>=1+free_12 && D==K && A==D && 2*meter==K-2*D+A ], cost: 5*meter 137: f23 -> [74] : B'=2+A, C'=0, D'=1+A, G'=free_7, H'=1+A, Q'=free_8, J'=free_11, [ D>=1+B && B>=1+H && K>=1+D && A==D ], cost: -6*D+6*A 138: f23 -> [75] : B'=2+A, C'=0, D'=1+A, G'=free_7, H'=1+A, Q'=free_8, J'=free_11, [ D>=1+B && B>=1+H && K>=1+D && A==D ], cost: -6*D+6*A 139: f23 -> [76] : B'=2+A, C'=0, D'=1+A, G'=free_7, H'=1+A, Q'=free_8, J'=free_11, [ D>=1+B && B>=1+H && K>=1+D && A==D ], cost: -6*D+6*A 140: f23 -> [77] : B'=2+A, C'=0, D'=1+A, G'=free_7, H'=1+A, Q'=free_8, J'=free_11, [ D>=1+B && B>=1+H && K>=1+D && A==D ], cost: -6*D+6*A 141: f23 -> [78] : B'=2+A, C'=0, D'=1+A, G'=free_7, H'=1+A, Q'=free_8, J'=free_11, [ D>=1+B && B>=1+H && K>=1+D && A==D ], cost: -6*D+6*A 142: f23 -> [79] : B'=2+A, C'=0, D'=1+A, G'=free_7, H'=1+A, Q'=free_8, J'=free_11, [ D>=1+B && B>=1+H && K>=1+D && A==D ], cost: -6*D+6*A 143: f23 -> [80] : B'=2+A, C'=0, D'=1+A, G'=free_7, H'=1+A, Q'=free_8, J'=free_11, [ D>=1+B && B>=1+H && K>=1+D && A==D ], cost: -6*D+6*A 144: f23 -> [81] : B'=2+A, C'=0, D'=1+A, G'=free_7, H'=1+A, Q'=free_8, J'=free_11, [ D>=1+B && B>=1+H && K>=1+D && A==D ], cost: -6*D+6*A 145: f23 -> [82] : B'=2+A, C'=0, D'=1+A, G'=free_7, H'=1+A, Q'=free_8, J'=free_11, [ D>=1+B && B>=1+H && K>=1+D && A==D ], cost: -6*D+6*A 146: f23 -> [83] : B'=2+A, C'=0, D'=1+A, G'=free_7, H'=1+A, Q'=free_8, J'=free_11, [ D>=1+B && B>=1+H && K>=1+D && A==D ], cost: -6*D+6*A 147: f23 -> [84] : B'=2+A, C'=0, D'=1+A, G'=free_7, H'=1+A, Q'=free_8, J'=free_11, [ D>=1+B && B>=1+H && K>=1+D && A==D ], cost: -6*D+6*A 148: f23 -> [85] : B'=2+A, C'=0, D'=1+A, G'=free_7, H'=1+A, Q'=free_8, J'=free_11, [ D>=1+B && B>=1+H && K>=1+D && A==D ], cost: -6*D+6*A 149: f23 -> [86] : B'=2+A, C'=0, D'=1+A, G'=free_7, H'=1+A, Q'=free_8, J'=free_11, [ D>=1+B && B>=1+H && K>=1+D && A==D ], cost: -6*D+6*A 150: f23 -> [87] : B'=2+A, C'=0, D'=1+A, G'=free_7, H'=1+A, Q'=free_8, J'=free_11, [ D>=1+B && B>=1+H && K>=1+D && A==D ], cost: -6*D+6*A 151: f23 -> [88] : B'=2+A, C'=0, D'=1+A, G'=free_7, H'=1+A, Q'=free_8, J'=free_11, [ D>=1+B && B>=1+H && K>=1+D && A==D ], cost: -6*D+6*A 152: f23 -> [89] : B'=2+A, C'=0, D'=1+A, G'=free_7, H'=1+A, Q'=free_8, J'=free_11, [ D>=1+B && B>=1+H && K>=1+D && A==D ], cost: -6*D+6*A 153: f23 -> [90] : B'=2+A, C'=0, D'=1+A, G'=free_7, H'=1+A, Q'=free_8, J'=free_11, [ D>=1+B && B>=1+H && K>=1+D && A==D ], cost: -6*D+6*A 154: f23 -> [91] : B'=2+A, C'=0, D'=1+A, G'=free_7, H'=1+A, Q'=free_8, J'=free_11, [ D>=1+B && B>=1+H && K>=1+D && A==D ], cost: -6*D+6*A 155: f23 -> [92] : B'=2+A, C'=0, D'=1+A, G'=free_7, H'=1+A, Q'=free_8, J'=free_11, [ D>=1+B && B>=1+H && K>=1+D && A==D ], cost: -6*D+6*A 156: f23 -> [93] : B'=2+A, C'=0, D'=1+A, G'=free_7, H'=1+A, Q'=free_8, J'=free_11, [ D>=1+B && B>=1+H && K>=1+D && A==D ], cost: -6*D+6*A 157: f23 -> [94] : B'=2+A, C'=0, D'=1+A, G'=free_7, H'=1+A, Q'=free_8, J'=free_11, [ D>=1+B && B>=1+H && D>=1+K && A==D ], cost: -6*D+6*A 158: f23 -> [95] : B'=2+A, C'=0, D'=1+A, G'=free_7, H'=1+A, Q'=free_8, J'=free_11, [ D>=1+B && B>=1+H && D>=1+K && A==D ], cost: -6*D+6*A 159: f23 -> [96] : B'=2+A, C'=0, D'=1+A, G'=free_7, H'=1+A, Q'=free_8, J'=free_11, [ D>=1+B && B>=1+H && D>=1+K && A==D ], cost: -6*D+6*A 160: f23 -> [97] : B'=2+A, C'=0, D'=1+A, G'=free_7, H'=1+A, Q'=free_8, J'=free_11, [ D>=1+B && B>=1+H && D>=1+K && A==D ], cost: -6*D+6*A 161: f23 -> [98] : B'=2+A, C'=0, D'=1+A, G'=free_7, H'=1+A, Q'=free_8, J'=free_11, [ D>=1+B && B>=1+H && D>=1+K && A==D ], cost: -6*D+6*A 162: f23 -> [99] : B'=2+A, C'=0, D'=1+A, G'=free_7, H'=1+A, Q'=free_8, J'=free_11, [ D>=1+B && B>=1+H && D>=1+K && A==D ], cost: -6*D+6*A 163: f23 -> [100] : B'=2+A, C'=0, D'=1+A, G'=free_7, H'=1+A, Q'=free_8, J'=free_11, [ D>=1+B && B>=1+H && D>=1+K && A==D ], cost: -6*D+6*A 164: f23 -> [101] : B'=2+A, C'=0, D'=1+A, G'=free_7, H'=1+A, Q'=free_8, J'=free_11, [ D>=1+B && B>=1+H && D>=1+K && A==D ], cost: -6*D+6*A 165: f23 -> [102] : B'=2+A, C'=0, D'=1+A, G'=free_7, H'=1+A, Q'=free_8, J'=free_11, [ D>=1+B && B>=1+H && D>=1+K && A==D ], cost: -6*D+6*A 166: f23 -> [103] : B'=2+A, C'=0, D'=1+A, G'=free_7, H'=1+A, Q'=free_8, J'=free_11, [ D>=1+B && B>=1+H && D>=1+K && A==D ], cost: -6*D+6*A 167: f23 -> [104] : B'=2+A, C'=0, D'=1+A, G'=free_7, H'=1+A, Q'=free_8, J'=free_11, [ D>=1+B && B>=1+H && D>=1+K && A==D ], cost: -6*D+6*A 168: f23 -> [105] : B'=2+A, C'=0, D'=1+A, G'=free_7, H'=1+A, Q'=free_8, J'=free_11, [ D>=1+B && B>=1+H && D>=1+K && A==D ], cost: -6*D+6*A 169: f23 -> [106] : B'=2+A, C'=0, D'=1+A, G'=free_7, H'=1+A, Q'=free_8, J'=free_11, [ D>=1+B && B>=1+H && D>=1+K && A==D ], cost: -6*D+6*A 170: f23 -> [107] : B'=2+A, C'=0, D'=1+A, G'=free_7, H'=1+A, Q'=free_8, J'=free_11, [ D>=1+B && B>=1+H && D>=1+K && A==D ], cost: -6*D+6*A 171: f23 -> [108] : B'=2+A, C'=0, D'=1+A, G'=free_7, H'=1+A, Q'=free_8, J'=free_11, [ D>=1+B && B>=1+H && D>=1+K && A==D ], cost: -6*D+6*A 172: f23 -> [109] : B'=2+A, C'=0, D'=1+A, G'=free_7, H'=1+A, Q'=free_8, J'=free_11, [ D>=1+B && B>=1+H && D>=1+K && A==D ], cost: -6*D+6*A 173: f23 -> [110] : B'=2+A, C'=0, D'=1+A, G'=free_7, H'=1+A, Q'=free_8, J'=free_11, [ D>=1+B && B>=1+H && D>=1+K && A==D ], cost: -6*D+6*A 174: f23 -> [111] : B'=2+A, C'=0, D'=1+A, G'=free_7, H'=1+A, Q'=free_8, J'=free_11, [ D>=1+B && B>=1+H && D>=1+K && A==D ], cost: -6*D+6*A 175: f23 -> [112] : B'=2+A, C'=0, D'=1+A, G'=free_7, H'=1+A, Q'=free_8, J'=free_11, [ D>=1+B && B>=1+H && D>=1+K && A==D ], cost: -6*D+6*A 176: f23 -> [113] : B'=2+A, C'=0, D'=1+A, G'=free_7, H'=1+A, Q'=free_8, J'=free_11, [ D>=1+B && B>=1+H && D>=1+K && A==D ], cost: -6*D+6*A 177: f23 -> [114] : B'=2+A, C'=free_13, D'=1+A, G'=free_7, H'=1+A, Q'=free_13, J'=free_14, K'=1+A, [ D>=1+B && B>=1+H && free_13>=0 && A==D ], cost: -5*D+5*A 178: f23 -> [115] : B'=2+A, C'=free_13, D'=1+A, G'=free_7, H'=1+A, Q'=free_13, J'=free_14, K'=1+A, [ D>=1+B && B>=1+H && free_13>=0 && A==D ], cost: -5*D+5*A 179: f23 -> [116] : B'=2+A, C'=free_13, D'=1+A, G'=free_7, H'=1+A, Q'=free_13, J'=free_14, K'=1+A, [ D>=1+B && B>=1+H && free_13>=0 && A==D ], cost: -5*D+5*A 180: f23 -> [117] : B'=2+A, C'=free_13, D'=1+A, G'=free_7, H'=1+A, Q'=free_13, J'=free_14, K'=1+A, [ D>=1+B && B>=1+H && free_13>=0 && A==D ], cost: -5*D+5*A 181: f23 -> [118] : B'=2+A, C'=free_13, D'=1+A, G'=free_7, H'=1+A, Q'=free_13, J'=free_14, K'=1+A, [ D>=1+B && B>=1+H && free_13>=0 && A==D ], cost: -5*D+5*A 182: f23 -> [119] : B'=2+A, C'=free_13, D'=1+A, G'=free_7, H'=1+A, Q'=free_13, J'=free_14, K'=1+A, [ D>=1+B && B>=1+H && free_13>=0 && A==D ], cost: -5*D+5*A 183: f23 -> [120] : B'=2+A, C'=free_13, D'=1+A, G'=free_7, H'=1+A, Q'=free_13, J'=free_14, K'=1+A, [ D>=1+B && B>=1+H && free_13>=0 && A==D ], cost: -5*D+5*A 184: f23 -> [121] : B'=2+A, C'=free_13, D'=1+A, G'=free_7, H'=1+A, Q'=free_13, J'=free_14, K'=1+A, [ D>=1+B && B>=1+H && free_13>=0 && A==D ], cost: -5*D+5*A 185: f23 -> [122] : B'=2+A, C'=free_13, D'=1+A, G'=free_7, H'=1+A, Q'=free_13, J'=free_14, K'=1+A, [ D>=1+B && B>=1+H && free_13>=0 && A==D ], cost: -5*D+5*A 186: f23 -> [123] : B'=2+A, C'=free_13, D'=1+A, G'=free_7, H'=1+A, Q'=free_13, J'=free_14, K'=1+A, [ D>=1+B && B>=1+H && free_13>=0 && A==D ], cost: -5*D+5*A 187: f23 -> [124] : B'=2+A, C'=free_13, D'=1+A, G'=free_7, H'=1+A, Q'=free_13, J'=free_14, K'=1+A, [ D>=1+B && B>=1+H && free_13>=0 && A==D ], cost: -5*D+5*A 188: f23 -> [125] : B'=2+A, C'=free_13, D'=1+A, G'=free_7, H'=1+A, Q'=free_13, J'=free_14, K'=1+A, [ D>=1+B && B>=1+H && free_13>=0 && A==D ], cost: -5*D+5*A 189: f23 -> [126] : B'=2+A, C'=free_13, D'=1+A, G'=free_7, H'=1+A, Q'=free_13, J'=free_14, K'=1+A, [ D>=1+B && B>=1+H && free_13>=0 && A==D ], cost: -5*D+5*A 190: f23 -> [127] : B'=2+A, C'=free_13, D'=1+A, G'=free_7, H'=1+A, Q'=free_13, J'=free_14, K'=1+A, [ D>=1+B && B>=1+H && free_13>=0 && A==D ], cost: -5*D+5*A 191: f23 -> [128] : B'=2+A, C'=free_13, D'=1+A, G'=free_7, H'=1+A, Q'=free_13, J'=free_14, K'=1+A, [ D>=1+B && B>=1+H && free_13>=0 && A==D ], cost: -5*D+5*A 192: f23 -> [129] : B'=2+A, C'=free_13, D'=1+A, G'=free_7, H'=1+A, Q'=free_13, J'=free_14, K'=1+A, [ D>=1+B && B>=1+H && free_13>=0 && A==D ], cost: -5*D+5*A 193: f23 -> [130] : B'=2+A, C'=free_13, D'=1+A, G'=free_7, H'=1+A, Q'=free_13, J'=free_14, K'=1+A, [ D>=1+B && B>=1+H && free_13>=0 && A==D ], cost: -5*D+5*A 194: f23 -> [131] : B'=2+A, C'=free_13, D'=1+A, G'=free_7, H'=1+A, Q'=free_13, J'=free_14, K'=1+A, [ D>=1+B && B>=1+H && free_13>=0 && A==D ], cost: -5*D+5*A 195: f23 -> [132] : B'=2+A, C'=free_13, D'=1+A, G'=free_7, H'=1+A, Q'=free_13, J'=free_14, K'=1+A, [ D>=1+B && B>=1+H && free_13>=0 && A==D ], cost: -5*D+5*A 196: f23 -> [133] : B'=2+A, C'=free_13, D'=1+A, G'=free_7, H'=1+A, Q'=free_13, J'=free_14, K'=1+A, [ D>=1+B && B>=1+H && free_13>=0 && A==D ], cost: -5*D+5*A Applied chaining over branches and pruning: Start location: f2 113: f2 -> [20] : C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D ], cost: 3-D+A 114: f2 -> [21] : C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D ], cost: 3-D+A 115: f2 -> [22] : C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && 1>=1 && A>=D ], cost: 3-D+A 116: f2 -> [23] : C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && 1>=1 && A>=D ], cost: 3-D+A 103: f2 -> [46] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D ], cost: 4-D+A 104: f2 -> [47] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D ], cost: 4-D+A 105: f2 -> [48] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D ], cost: 4-D+A 106: f2 -> [49] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D ], cost: 4-D+A 108: f2 -> [50] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D ], cost: 4-D+A 109: f2 -> [51] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D ], cost: 4-D+A 110: f2 -> [52] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D ], cost: 4-D+A 111: f2 -> [53] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D ], cost: 4-D+A 197: f2 -> [134] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 198: f2 -> [135] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 199: f2 -> [136] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 200: f2 -> [137] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 201: f2 -> [138] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 202: f2 -> [139] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 203: f2 -> [140] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 204: f2 -> [141] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 205: f2 -> [142] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 206: f2 -> [143] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 207: f2 -> [144] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 208: f2 -> [145] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 209: f2 -> [146] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 210: f2 -> [147] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 211: f2 -> [148] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 212: f2 -> [149] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 213: f2 -> [150] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 214: f2 -> [151] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 215: f2 -> [152] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 216: f2 -> [153] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 217: f2 -> [154] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 218: f2 -> [155] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 219: f2 -> [156] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 220: f2 -> [157] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 221: f2 -> [158] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 222: f2 -> [159] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 223: f2 -> [160] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 224: f2 -> [161] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 225: f2 -> [162] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 226: f2 -> [163] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 227: f2 -> [164] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 228: f2 -> [165] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 229: f2 -> [166] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 230: f2 -> [167] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 231: f2 -> [168] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 232: f2 -> [169] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 233: f2 -> [170] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 234: f2 -> [171] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 235: f2 -> [172] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 236: f2 -> [173] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 237: f2 -> [174] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 238: f2 -> [175] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 239: f2 -> [176] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 240: f2 -> [177] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 241: f2 -> [178] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 242: f2 -> [179] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 243: f2 -> [180] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 244: f2 -> [181] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 245: f2 -> [182] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 246: f2 -> [183] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 247: f2 -> [184] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 248: f2 -> [185] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 249: f2 -> [186] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 250: f2 -> [187] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 251: f2 -> [188] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 252: f2 -> [189] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 253: f2 -> [190] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 254: f2 -> [191] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 255: f2 -> [192] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 256: f2 -> [193] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 257: f2 -> [194] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 258: f2 -> [195] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 259: f2 -> [196] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 260: f2 -> [197] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 261: f2 -> [198] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 262: f2 -> [199] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 263: f2 -> [200] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 264: f2 -> [201] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 265: f2 -> [202] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 266: f2 -> [203] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 267: f2 -> [204] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 268: f2 -> [205] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 269: f2 -> [206] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 270: f2 -> [207] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 271: f2 -> [208] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 272: f2 -> [209] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 273: f2 -> [210] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 274: f2 -> [211] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 275: f2 -> [212] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 276: f2 -> [213] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 277: f2 -> [214] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 278: f2 -> [215] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 279: f2 -> [216] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 280: f2 -> [217] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 281: f2 -> [218] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 282: f2 -> [219] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 283: f2 -> [220] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 284: f2 -> [221] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 285: f2 -> [222] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 286: f2 -> [223] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 287: f2 -> [224] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 288: f2 -> [225] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 289: f2 -> [226] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 290: f2 -> [227] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 291: f2 -> [228] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 292: f2 -> [229] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 293: f2 -> [230] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 294: f2 -> [231] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 295: f2 -> [232] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 296: f2 -> [233] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 297: f2 -> [234] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 298: f2 -> [235] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 299: f2 -> [236] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 300: f2 -> [237] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 301: f2 -> [238] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 302: f2 -> [239] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 303: f2 -> [240] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 304: f2 -> [241] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 305: f2 -> [242] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 306: f2 -> [243] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 307: f2 -> [244] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 308: f2 -> [245] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 309: f2 -> [246] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 310: f2 -> [247] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 311: f2 -> [248] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 312: f2 -> [249] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 313: f2 -> [250] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 314: f2 -> [251] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 315: f2 -> [252] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 316: f2 -> [253] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 317: f2 -> [254] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 318: f2 -> [255] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 319: f2 -> [256] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 320: f2 -> [257] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 321: f2 -> [258] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 322: f2 -> [259] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 323: f2 -> [260] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 324: f2 -> [261] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 325: f2 -> [262] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 326: f2 -> [263] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 327: f2 -> [264] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 328: f2 -> [265] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 329: f2 -> [266] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 330: f2 -> [267] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 331: f2 -> [268] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 332: f2 -> [269] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 333: f2 -> [270] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 334: f2 -> [271] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 335: f2 -> [272] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 336: f2 -> [273] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 337: f2 -> [274] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 338: f2 -> [275] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 339: f2 -> [276] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 340: f2 -> [277] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 341: f2 -> [278] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 342: f2 -> [279] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 343: f2 -> [280] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 344: f2 -> [281] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 345: f2 -> [282] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 346: f2 -> [283] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 347: f2 -> [284] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 348: f2 -> [285] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 349: f2 -> [286] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 350: f2 -> [287] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 351: f2 -> [288] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 352: f2 -> [289] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 353: f2 -> [290] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 354: f2 -> [291] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 355: f2 -> [292] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 356: f2 -> [293] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A Final control flow graph problem, now checking costs for infinitely many models: Start location: f2 113: f2 -> [20] : C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D ], cost: 3-D+A 114: f2 -> [21] : C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D ], cost: 3-D+A 115: f2 -> [22] : C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && 1>=1 && A>=D ], cost: 3-D+A 116: f2 -> [23] : C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && 1>=1 && A>=D ], cost: 3-D+A 103: f2 -> [46] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D ], cost: 4-D+A 104: f2 -> [47] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D ], cost: 4-D+A 105: f2 -> [48] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D ], cost: 4-D+A 106: f2 -> [49] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D ], cost: 4-D+A 108: f2 -> [50] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D ], cost: 4-D+A 109: f2 -> [51] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D ], cost: 4-D+A 110: f2 -> [52] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D ], cost: 4-D+A 111: f2 -> [53] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D ], cost: 4-D+A 197: f2 -> [134] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 198: f2 -> [135] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 199: f2 -> [136] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 200: f2 -> [137] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 201: f2 -> [138] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 202: f2 -> [139] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 203: f2 -> [140] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 204: f2 -> [141] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 205: f2 -> [142] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 206: f2 -> [143] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 207: f2 -> [144] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 208: f2 -> [145] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 209: f2 -> [146] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 210: f2 -> [147] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 211: f2 -> [148] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 212: f2 -> [149] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 213: f2 -> [150] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 214: f2 -> [151] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 215: f2 -> [152] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 216: f2 -> [153] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 217: f2 -> [154] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 218: f2 -> [155] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 219: f2 -> [156] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 220: f2 -> [157] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 221: f2 -> [158] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 222: f2 -> [159] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 223: f2 -> [160] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 224: f2 -> [161] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 225: f2 -> [162] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 226: f2 -> [163] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 227: f2 -> [164] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 228: f2 -> [165] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 229: f2 -> [166] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 230: f2 -> [167] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 231: f2 -> [168] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 232: f2 -> [169] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 233: f2 -> [170] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 234: f2 -> [171] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 235: f2 -> [172] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 236: f2 -> [173] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 237: f2 -> [174] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 238: f2 -> [175] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 239: f2 -> [176] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 240: f2 -> [177] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 241: f2 -> [178] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 242: f2 -> [179] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 243: f2 -> [180] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 244: f2 -> [181] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 245: f2 -> [182] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 246: f2 -> [183] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 247: f2 -> [184] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 248: f2 -> [185] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 249: f2 -> [186] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 250: f2 -> [187] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 251: f2 -> [188] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 252: f2 -> [189] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 253: f2 -> [190] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 254: f2 -> [191] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 255: f2 -> [192] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 256: f2 -> [193] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 257: f2 -> [194] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 258: f2 -> [195] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 259: f2 -> [196] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 260: f2 -> [197] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 261: f2 -> [198] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 262: f2 -> [199] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 263: f2 -> [200] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 264: f2 -> [201] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 265: f2 -> [202] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 266: f2 -> [203] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 267: f2 -> [204] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 268: f2 -> [205] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 269: f2 -> [206] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 270: f2 -> [207] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 271: f2 -> [208] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 272: f2 -> [209] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 273: f2 -> [210] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 274: f2 -> [211] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 275: f2 -> [212] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 276: f2 -> [213] : B'=1+B, C'=0, D'=1+A, E'=free_2, F'=free_2, [ A>=B && 0>=free_2 && A>=D && 1+B>=1+A ], cost: 5-D+A 277: f2 -> [214] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 278: f2 -> [215] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 279: f2 -> [216] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 280: f2 -> [217] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 281: f2 -> [218] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 282: f2 -> [219] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 283: f2 -> [220] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 284: f2 -> [221] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 285: f2 -> [222] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 286: f2 -> [223] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 287: f2 -> [224] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 288: f2 -> [225] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 289: f2 -> [226] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 290: f2 -> [227] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 291: f2 -> [228] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 292: f2 -> [229] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 293: f2 -> [230] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 294: f2 -> [231] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 295: f2 -> [232] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 296: f2 -> [233] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 297: f2 -> [234] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 298: f2 -> [235] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 299: f2 -> [236] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 300: f2 -> [237] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 301: f2 -> [238] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 302: f2 -> [239] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 303: f2 -> [240] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 304: f2 -> [241] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 305: f2 -> [242] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 306: f2 -> [243] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 307: f2 -> [244] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 308: f2 -> [245] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 309: f2 -> [246] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 310: f2 -> [247] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 311: f2 -> [248] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 312: f2 -> [249] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 313: f2 -> [250] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 314: f2 -> [251] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 315: f2 -> [252] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 316: f2 -> [253] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 317: f2 -> [254] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 318: f2 -> [255] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 319: f2 -> [256] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 320: f2 -> [257] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 321: f2 -> [258] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 322: f2 -> [259] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 323: f2 -> [260] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 324: f2 -> [261] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 325: f2 -> [262] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 326: f2 -> [263] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 327: f2 -> [264] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 328: f2 -> [265] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 329: f2 -> [266] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 330: f2 -> [267] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 331: f2 -> [268] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 332: f2 -> [269] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 333: f2 -> [270] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 334: f2 -> [271] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 335: f2 -> [272] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 336: f2 -> [273] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 337: f2 -> [274] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 338: f2 -> [275] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 339: f2 -> [276] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 340: f2 -> [277] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 341: f2 -> [278] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 342: f2 -> [279] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 343: f2 -> [280] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 344: f2 -> [281] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 345: f2 -> [282] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 346: f2 -> [283] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 347: f2 -> [284] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 348: f2 -> [285] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 349: f2 -> [286] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 350: f2 -> [287] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 351: f2 -> [288] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 352: f2 -> [289] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 353: f2 -> [290] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 354: f2 -> [291] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 355: f2 -> [292] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A 356: f2 -> [293] : B'=1+B, C'=1-D+A, D'=1+A, E'=1-D+A, F'=1-D+A, [ A>=B && A>=D && 1+B>=1+A ], cost: 5-D+A Computing complexity for remaining 172 transitions. Found configuration with infinitely models for cost: 3-D+A and guard: A>=B && 0>=free_2 && A>=D: B: Pos, free_2: Neg, D: Pos, A: Pos, where: A > B A > D Found new complexity n^1, because: Found infinity configuration. The final runtime is determined by this resulting transition: Final Guard: A>=B && 0>=free_2 && A>=D Final Cost: 3-D+A Obtained the following complexity w.r.t. the length of the input n: Complexity class: n^1 Complexity value: 1 WORST_CASE(Omega(n^1),?)