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