Trying to load file: main.koat Initial Control flow graph problem: Start location: f0 0: f47 -> f51 : [ A>=1 ], cost: 1 23: f47 -> f51 : [ B>=1 && 0>=A ], cost: 1 22: f47 -> f45 : Q_1'=2, [ 0>=B && 0>=A ], cost: 1 1: f51 -> f45 : [ 0>=B ], cost: 1 24: f51 -> f45 : Q_1'=3, [ B>=1 ], cost: 1 27: f45 -> f58 : Q'=free_10, P'=0, [ free_10>=0 && P>=1 && 1>=free_10 ], cost: 1 28: f45 -> f58 : Q'=free_11, P'=1, [ free_11>=0 && 0>=P && 1>=free_11 ], cost: 1 2: f0 -> f10 : C'=free, D'=free_1, E'=0, F'=1, G'=0, [ free>=1 && free_1>=0 ], cost: 1 3: f10 -> f14 : H'=1, [ C>=1+G && 0>=G ], cost: 1 4: f10 -> f14 : H'=0, [ C>=1+G && G>=1 ], cost: 1 35: f10 -> f79 : [ G>=C ], cost: 1 8: f14 -> f22 : J'=free_5, K'=1, L'=M, [ 1+G>=C && 1>=free_5 && free_5>=0 ], cost: 1 9: f14 -> f22 : J'=free_6, K'=0, L'=M, [ C>=2+G && 1>=free_6 && free_6>=0 ], cost: 1 33: f62 -> f10 : G'=1+G, Q'=1, M'=0, [ M>=1 && Q==1 ], cost: 1 34: f62 -> f10 : G'=1+G, Q'=1, M'=1, [ 0>=M && Q==1 ], cost: 1 5: f62 -> f22 : J'=free_2, [ free_2>=0 && 0>=Q && 1>=free_2 ], cost: 1 6: f62 -> f22 : J'=free_3, [ free_3>=0 && Q>=2 && 1>=free_3 ], cost: 1 10: f22 -> f26 : E'=1+E, [ J>=1 && 0>=D && 0>=E ], cost: 1 11: f22 -> f26 : E'=1+E, [ J>=1 && 0>=D && E==1 ], cost: 1 12: f22 -> f26 : D'=free_7, E'=0, F'=1+F, [ E>=2 && 0>=D && free_7>=0 ], cost: 1 13: f22 -> f26 : D'=-1+D, [ D>=1 ], cost: 1 7: f26 -> f22 : J'=free_4, [ 0>=J && 1>=free_4 && free_4>=0 ], cost: 1 14: f26 -> f41 : A'=H, B'=K, N'=1, O'=L, [ N>=1 && J>=1 ], cost: 1 15: f26 -> f41 : A'=H, B'=K, N'=1, O'=L, P'=L, [ 0>=N && J>=1 ], cost: 1 18: f41 -> f47 : A'=0, P'=O, [ A==0 && O==P ], cost: 1 16: f41 -> f43 : P'=O, [ 0>=1+A && O==P ], cost: 1 17: f41 -> f43 : P'=O, [ A>=1 && O==P ], cost: 1 25: f41 -> f58 : Q'=free_8, [ free_8>=0 && O>=1+P && 1>=free_8 ], cost: 1 26: f41 -> f58 : Q'=free_9, [ free_9>=0 && P>=1+O && 1>=free_9 ], cost: 1 20: f43 -> f47 : [ 0>=1+B ], cost: 1 21: f43 -> f47 : [ B>=1 ], cost: 1 19: f43 -> f45 : B'=0, Q_1'=1, [ B==0 ], cost: 1 29: f58 -> f62 : E'=1+E, [ 0>=E && 0>=D && Q>=1 ], cost: 1 30: f58 -> f62 : E'=1+E, [ 0>=D && Q>=1 && E==1 ], cost: 1 31: f58 -> f62 : D'=free_12, E'=0, F'=1+F, [ E>=2 && 0>=D && free_12>=0 ], cost: 1 32: f58 -> f62 : D'=-1+D, [ D>=1 ], cost: 1 Simplified the transitions: Start location: f0 0: f47 -> f51 : [ A>=1 ], cost: 1 23: f47 -> f51 : [ B>=1 && 0>=A ], cost: 1 22: f47 -> f45 : Q_1'=2, [ 0>=B && 0>=A ], cost: 1 1: f51 -> f45 : [ 0>=B ], cost: 1 24: f51 -> f45 : Q_1'=3, [ B>=1 ], cost: 1 27: f45 -> f58 : Q'=free_10, P'=0, [ free_10>=0 && P>=1 && 1>=free_10 ], cost: 1 28: f45 -> f58 : Q'=free_11, P'=1, [ free_11>=0 && 0>=P && 1>=free_11 ], cost: 1 2: f0 -> f10 : C'=free, D'=free_1, E'=0, F'=1, G'=0, [ free>=1 && free_1>=0 ], cost: 1 3: f10 -> f14 : H'=1, [ C>=1+G && 0>=G ], cost: 1 4: f10 -> f14 : H'=0, [ C>=1+G && G>=1 ], cost: 1 8: f14 -> f22 : J'=free_5, K'=1, L'=M, [ 1+G>=C && 1>=free_5 && free_5>=0 ], cost: 1 9: f14 -> f22 : J'=free_6, K'=0, L'=M, [ C>=2+G && 1>=free_6 && free_6>=0 ], cost: 1 33: f62 -> f10 : G'=1+G, Q'=1, M'=0, [ M>=1 && Q==1 ], cost: 1 34: f62 -> f10 : G'=1+G, Q'=1, M'=1, [ 0>=M && Q==1 ], cost: 1 5: f62 -> f22 : J'=free_2, [ free_2>=0 && 0>=Q && 1>=free_2 ], cost: 1 6: f62 -> f22 : J'=free_3, [ free_3>=0 && Q>=2 && 1>=free_3 ], cost: 1 10: f22 -> f26 : E'=1+E, [ J>=1 && 0>=D && 0>=E ], cost: 1 11: f22 -> f26 : E'=1+E, [ J>=1 && 0>=D && E==1 ], cost: 1 12: f22 -> f26 : D'=free_7, E'=0, F'=1+F, [ E>=2 && 0>=D && free_7>=0 ], cost: 1 13: f22 -> f26 : D'=-1+D, [ D>=1 ], cost: 1 7: f26 -> f22 : J'=free_4, [ 0>=J && 1>=free_4 && free_4>=0 ], cost: 1 14: f26 -> f41 : A'=H, B'=K, N'=1, O'=L, [ N>=1 && J>=1 ], cost: 1 15: f26 -> f41 : A'=H, B'=K, N'=1, O'=L, P'=L, [ 0>=N && J>=1 ], cost: 1 18: f41 -> f47 : A'=0, P'=O, [ A==0 && O==P ], cost: 1 16: f41 -> f43 : P'=O, [ 0>=1+A && O==P ], cost: 1 17: f41 -> f43 : P'=O, [ A>=1 && O==P ], cost: 1 25: f41 -> f58 : Q'=free_8, [ free_8>=0 && O>=1+P && 1>=free_8 ], cost: 1 26: f41 -> f58 : Q'=free_9, [ free_9>=0 && P>=1+O && 1>=free_9 ], cost: 1 20: f43 -> f47 : [ 0>=1+B ], cost: 1 21: f43 -> f47 : [ B>=1 ], cost: 1 19: f43 -> f45 : B'=0, Q_1'=1, [ B==0 ], cost: 1 29: f58 -> f62 : E'=1+E, [ 0>=E && 0>=D && Q>=1 ], cost: 1 30: f58 -> f62 : E'=1+E, [ 0>=D && Q>=1 && E==1 ], cost: 1 31: f58 -> f62 : D'=free_12, E'=0, F'=1+F, [ E>=2 && 0>=D && free_12>=0 ], cost: 1 32: f58 -> f62 : D'=-1+D, [ D>=1 ], cost: 1 Applied chaining over branches and pruning: Start location: f0 22: f47 -> f45 : Q_1'=2, [ 0>=B && 0>=A ], cost: 1 56: f47 -> f45 : [ A>=1 && 0>=B ], cost: 2 57: f47 -> f45 : Q_1'=3, [ A>=1 && B>=1 ], cost: 2 58: f47 -> f45 : Q_1'=3, [ B>=1 && 0>=A && B>=1 ], cost: 2 27: f45 -> f58 : Q'=free_10, P'=0, [ free_10>=0 && P>=1 && 1>=free_10 ], cost: 1 28: f45 -> f58 : Q'=free_11, P'=1, [ free_11>=0 && 0>=P && 1>=free_11 ], cost: 1 2: f0 -> f10 : C'=free, D'=free_1, E'=0, F'=1, G'=0, [ free>=1 && free_1>=0 ], cost: 1 36: f10 -> f22 : H'=1, J'=free_5, K'=1, L'=M, [ C>=1+G && 0>=G && 1+G>=C && 1>=free_5 && free_5>=0 ], cost: 2 37: f10 -> f22 : H'=1, J'=free_6, K'=0, L'=M, [ C>=1+G && 0>=G && C>=2+G && 1>=free_6 && free_6>=0 ], cost: 2 38: f10 -> f22 : H'=0, J'=free_5, K'=1, L'=M, [ C>=1+G && G>=1 && 1+G>=C && 1>=free_5 && free_5>=0 ], cost: 2 39: f10 -> f22 : H'=0, J'=free_6, K'=0, L'=M, [ C>=1+G && G>=1 && C>=2+G && 1>=free_6 && free_6>=0 ], cost: 2 44: f22 -> f22 : D'=free_7, E'=0, F'=1+F, J'=free_4, [ E>=2 && 0>=D && free_7>=0 && 0>=J && 1>=free_4 && free_4>=0 ], cost: 2 47: f22 -> f22 : D'=-1+D, J'=free_4, [ D>=1 && 0>=J && 1>=free_4 && free_4>=0 ], cost: 2 40: f22 -> f41 : A'=H, B'=K, E'=1+E, N'=1, O'=L, [ J>=1 && 0>=D && 0>=E && N>=1 && J>=1 ], cost: 2 41: f22 -> f41 : A'=H, B'=K, E'=1+E, N'=1, O'=L, P'=L, [ J>=1 && 0>=D && 0>=E && 0>=N && J>=1 ], cost: 2 43: f22 -> f41 : A'=H, B'=K, E'=1+E, N'=1, O'=L, P'=L, [ J>=1 && 0>=D && E==1 && 0>=N && J>=1 ], cost: 2 45: f22 -> f41 : A'=H, B'=K, D'=free_7, E'=0, F'=1+F, N'=1, O'=L, [ E>=2 && 0>=D && free_7>=0 && N>=1 && J>=1 ], cost: 2 46: f22 -> f41 : A'=H, B'=K, D'=free_7, E'=0, F'=1+F, N'=1, O'=L, P'=L, [ E>=2 && 0>=D && free_7>=0 && 0>=N && J>=1 ], cost: 2 18: f41 -> f47 : A'=0, P'=O, [ A==0 && O==P ], cost: 1 50: f41 -> f47 : P'=O, [ 0>=1+A && O==P && 0>=1+B ], cost: 2 51: f41 -> f47 : P'=O, [ 0>=1+A && O==P && B>=1 ], cost: 2 53: f41 -> f47 : P'=O, [ A>=1 && O==P && 0>=1+B ], cost: 2 54: f41 -> f47 : P'=O, [ A>=1 && O==P && B>=1 ], cost: 2 52: f41 -> f45 : B'=0, P'=O, Q_1'=1, [ 0>=1+A && O==P && B==0 ], cost: 2 55: f41 -> f45 : B'=0, P'=O, Q_1'=1, [ A>=1 && O==P && B==0 ], cost: 2 25: f41 -> f58 : Q'=free_8, [ free_8>=0 && O>=1+P && 1>=free_8 ], cost: 1 26: f41 -> f58 : Q'=free_9, [ free_9>=0 && P>=1+O && 1>=free_9 ], cost: 1 59: f58 -> f10 : E'=1+E, G'=1+G, Q'=1, M'=0, [ 0>=E && 0>=D && Q>=1 && M>=1 && Q==1 ], cost: 2 60: f58 -> f10 : E'=1+E, G'=1+G, Q'=1, M'=1, [ 0>=E && 0>=D && Q>=1 && 0>=M && Q==1 ], cost: 2 63: f58 -> f10 : E'=1+E, G'=1+G, Q'=1, M'=1, [ 0>=D && Q>=1 && E==1 && 0>=M && Q==1 ], cost: 2 65: f58 -> f10 : D'=free_12, E'=0, F'=1+F, G'=1+G, Q'=1, M'=0, [ E>=2 && 0>=D && free_12>=0 && M>=1 && Q==1 ], cost: 2 66: f58 -> f10 : D'=free_12, E'=0, F'=1+F, G'=1+G, Q'=1, M'=1, [ E>=2 && 0>=D && free_12>=0 && 0>=M && Q==1 ], cost: 2 61: f58 -> f22 : E'=1+E, J'=free_3, [ 0>=E && 0>=D && Q>=1 && free_3>=0 && Q>=2 && 1>=free_3 ], cost: 2 64: f58 -> f22 : E'=1+E, J'=free_3, [ 0>=D && Q>=1 && E==1 && free_3>=0 && Q>=2 && 1>=free_3 ], cost: 2 67: f58 -> f22 : D'=free_12, E'=0, F'=1+F, J'=free_2, [ E>=2 && 0>=D && free_12>=0 && free_2>=0 && 0>=Q && 1>=free_2 ], cost: 2 68: f58 -> f22 : D'=free_12, E'=0, F'=1+F, J'=free_3, [ E>=2 && 0>=D && free_12>=0 && free_3>=0 && Q>=2 && 1>=free_3 ], cost: 2 72: f58 -> f22 : D'=-1+D, J'=free_3, [ D>=1 && free_3>=0 && Q>=2 && 1>=free_3 ], cost: 2 Eliminating 2 self-loops for location f22 Self-Loop 47 has the metering function: D, resulting in the new transition 74. Removing the self-loops: 44 47. Adding an epsilon transition (to model nonexecution of the loops): 75. Removed all Self-loops using metering functions (where possible): Start location: f0 22: f47 -> f45 : Q_1'=2, [ 0>=B && 0>=A ], cost: 1 56: f47 -> f45 : [ A>=1 && 0>=B ], cost: 2 57: f47 -> f45 : Q_1'=3, [ A>=1 && B>=1 ], cost: 2 58: f47 -> f45 : Q_1'=3, [ B>=1 && 0>=A && B>=1 ], cost: 2 27: f45 -> f58 : Q'=free_10, P'=0, [ free_10>=0 && P>=1 && 1>=free_10 ], cost: 1 28: f45 -> f58 : Q'=free_11, P'=1, [ free_11>=0 && 0>=P && 1>=free_11 ], cost: 1 2: f0 -> f10 : C'=free, D'=free_1, E'=0, F'=1, G'=0, [ free>=1 && free_1>=0 ], cost: 1 36: f10 -> f22 : H'=1, J'=free_5, K'=1, L'=M, [ C>=1+G && 0>=G && 1+G>=C && 1>=free_5 && free_5>=0 ], cost: 2 37: f10 -> f22 : H'=1, J'=free_6, K'=0, L'=M, [ C>=1+G && 0>=G && C>=2+G && 1>=free_6 && free_6>=0 ], cost: 2 38: f10 -> f22 : H'=0, J'=free_5, K'=1, L'=M, [ C>=1+G && G>=1 && 1+G>=C && 1>=free_5 && free_5>=0 ], cost: 2 39: f10 -> f22 : H'=0, J'=free_6, K'=0, L'=M, [ C>=1+G && G>=1 && C>=2+G && 1>=free_6 && free_6>=0 ], cost: 2 73: f22 -> [13] : D'=free_7, E'=0, F'=1+F, J'=free_4, [ E>=2 && 0>=D && free_7>=0 && 0>=J && 1>=free_4 && free_4>=0 ], cost: 2 74: f22 -> [13] : D'=0, J'=0, [ D>=1 && 0>=J && 1>=0 && 0>=0 ], cost: 2*D 75: f22 -> [13] : [], cost: 0 18: f41 -> f47 : A'=0, P'=O, [ A==0 && O==P ], cost: 1 50: f41 -> f47 : P'=O, [ 0>=1+A && O==P && 0>=1+B ], cost: 2 51: f41 -> f47 : P'=O, [ 0>=1+A && O==P && B>=1 ], cost: 2 53: f41 -> f47 : P'=O, [ A>=1 && O==P && 0>=1+B ], cost: 2 54: f41 -> f47 : P'=O, [ A>=1 && O==P && B>=1 ], cost: 2 52: f41 -> f45 : B'=0, P'=O, Q_1'=1, [ 0>=1+A && O==P && B==0 ], cost: 2 55: f41 -> f45 : B'=0, P'=O, Q_1'=1, [ A>=1 && O==P && B==0 ], cost: 2 25: f41 -> f58 : Q'=free_8, [ free_8>=0 && O>=1+P && 1>=free_8 ], cost: 1 26: f41 -> f58 : Q'=free_9, [ free_9>=0 && P>=1+O && 1>=free_9 ], cost: 1 59: f58 -> f10 : E'=1+E, G'=1+G, Q'=1, M'=0, [ 0>=E && 0>=D && Q>=1 && M>=1 && Q==1 ], cost: 2 60: f58 -> f10 : E'=1+E, G'=1+G, Q'=1, M'=1, [ 0>=E && 0>=D && Q>=1 && 0>=M && Q==1 ], cost: 2 63: f58 -> f10 : E'=1+E, G'=1+G, Q'=1, M'=1, [ 0>=D && Q>=1 && E==1 && 0>=M && Q==1 ], cost: 2 65: f58 -> f10 : D'=free_12, E'=0, F'=1+F, G'=1+G, Q'=1, M'=0, [ E>=2 && 0>=D && free_12>=0 && M>=1 && Q==1 ], cost: 2 66: f58 -> f10 : D'=free_12, E'=0, F'=1+F, G'=1+G, Q'=1, M'=1, [ E>=2 && 0>=D && free_12>=0 && 0>=M && Q==1 ], cost: 2 61: f58 -> f22 : E'=1+E, J'=free_3, [ 0>=E && 0>=D && Q>=1 && free_3>=0 && Q>=2 && 1>=free_3 ], cost: 2 64: f58 -> f22 : E'=1+E, J'=free_3, [ 0>=D && Q>=1 && E==1 && free_3>=0 && Q>=2 && 1>=free_3 ], cost: 2 67: f58 -> f22 : D'=free_12, E'=0, F'=1+F, J'=free_2, [ E>=2 && 0>=D && free_12>=0 && free_2>=0 && 0>=Q && 1>=free_2 ], cost: 2 68: f58 -> f22 : D'=free_12, E'=0, F'=1+F, J'=free_3, [ E>=2 && 0>=D && free_12>=0 && free_3>=0 && Q>=2 && 1>=free_3 ], cost: 2 72: f58 -> f22 : D'=-1+D, J'=free_3, [ D>=1 && free_3>=0 && Q>=2 && 1>=free_3 ], cost: 2 40: [13] -> f41 : A'=H, B'=K, E'=1+E, N'=1, O'=L, [ J>=1 && 0>=D && 0>=E && N>=1 && J>=1 ], cost: 2 41: [13] -> f41 : A'=H, B'=K, E'=1+E, N'=1, O'=L, P'=L, [ J>=1 && 0>=D && 0>=E && 0>=N && J>=1 ], cost: 2 43: [13] -> f41 : A'=H, B'=K, E'=1+E, N'=1, O'=L, P'=L, [ J>=1 && 0>=D && E==1 && 0>=N && J>=1 ], cost: 2 45: [13] -> f41 : A'=H, B'=K, D'=free_7, E'=0, F'=1+F, N'=1, O'=L, [ E>=2 && 0>=D && free_7>=0 && N>=1 && J>=1 ], cost: 2 46: [13] -> f41 : A'=H, B'=K, D'=free_7, E'=0, F'=1+F, N'=1, O'=L, P'=L, [ E>=2 && 0>=D && free_7>=0 && 0>=N && J>=1 ], cost: 2 Applied chaining over branches and pruning: Start location: f0 27: f45 -> f58 : Q'=free_10, P'=0, [ free_10>=0 && P>=1 && 1>=free_10 ], cost: 1 28: f45 -> f58 : Q'=free_11, P'=1, [ free_11>=0 && 0>=P && 1>=free_11 ], cost: 1 2: f0 -> f10 : C'=free, D'=free_1, E'=0, F'=1, G'=0, [ free>=1 && free_1>=0 ], cost: 1 36: f10 -> f22 : H'=1, J'=free_5, K'=1, L'=M, [ C>=1+G && 0>=G && 1+G>=C && 1>=free_5 && free_5>=0 ], cost: 2 37: f10 -> f22 : H'=1, J'=free_6, K'=0, L'=M, [ C>=1+G && 0>=G && C>=2+G && 1>=free_6 && free_6>=0 ], cost: 2 38: f10 -> f22 : H'=0, J'=free_5, K'=1, L'=M, [ C>=1+G && G>=1 && 1+G>=C && 1>=free_5 && free_5>=0 ], cost: 2 39: f10 -> f22 : H'=0, J'=free_6, K'=0, L'=M, [ C>=1+G && G>=1 && C>=2+G && 1>=free_6 && free_6>=0 ], cost: 2 76: f22 -> f41 : A'=H, B'=K, D'=free_7, E'=1, F'=1+F, J'=free_4, N'=1, O'=L, [ E>=2 && 0>=D && free_7>=0 && 0>=J && 1>=free_4 && free_4>=0 && free_4>=1 && 0>=free_7 && 0>=0 && N>=1 && free_4>=1 ], cost: 4 77: f22 -> f41 : A'=H, B'=K, D'=free_7, E'=1, F'=1+F, J'=free_4, N'=1, O'=L, P'=L, [ E>=2 && 0>=D && free_7>=0 && 0>=J && 1>=free_4 && free_4>=0 && free_4>=1 && 0>=free_7 && 0>=0 && 0>=N && free_4>=1 ], cost: 4 83: f22 -> f41 : A'=H, B'=K, E'=1+E, N'=1, O'=L, [ J>=1 && 0>=D && 0>=E && N>=1 && J>=1 ], cost: 2 84: f22 -> f41 : A'=H, B'=K, E'=1+E, N'=1, O'=L, P'=L, [ J>=1 && 0>=D && 0>=E && 0>=N && J>=1 ], cost: 2 85: f22 -> f41 : A'=H, B'=K, E'=1+E, N'=1, O'=L, P'=L, [ J>=1 && 0>=D && E==1 && 0>=N && J>=1 ], cost: 2 78: f22 -> [14] : D'=0, J'=0, [ D>=1 && 0>=J && 1>=0 && 0>=0 ], cost: 2*D 79: f22 -> [15] : D'=0, J'=0, [ D>=1 && 0>=J && 1>=0 && 0>=0 ], cost: 2*D 80: f22 -> [16] : D'=0, J'=0, [ D>=1 && 0>=J && 1>=0 && 0>=0 ], cost: 2*D 81: f22 -> [17] : D'=0, J'=0, [ D>=1 && 0>=J && 1>=0 && 0>=0 ], cost: 2*D 82: f22 -> [18] : D'=0, J'=0, [ D>=1 && 0>=J && 1>=0 && 0>=0 ], cost: 2*D 52: f41 -> f45 : B'=0, P'=O, Q_1'=1, [ 0>=1+A && O==P && B==0 ], cost: 2 55: f41 -> f45 : B'=0, P'=O, Q_1'=1, [ A>=1 && O==P && B==0 ], cost: 2 89: f41 -> f45 : A'=0, P'=O, Q_1'=3, [ A==0 && O==P && B>=1 && 0>=0 && B>=1 ], cost: 3 90: f41 -> f45 : P'=O, Q_1'=2, [ 0>=1+A && O==P && 0>=1+B && 0>=B && 0>=A ], cost: 3 91: f41 -> f45 : P'=O, Q_1'=3, [ 0>=1+A && O==P && B>=1 && B>=1 && 0>=A && B>=1 ], cost: 4 25: f41 -> f58 : Q'=free_8, [ free_8>=0 && O>=1+P && 1>=free_8 ], cost: 1 26: f41 -> f58 : Q'=free_9, [ free_9>=0 && P>=1+O && 1>=free_9 ], cost: 1 59: f58 -> f10 : E'=1+E, G'=1+G, Q'=1, M'=0, [ 0>=E && 0>=D && Q>=1 && M>=1 && Q==1 ], cost: 2 60: f58 -> f10 : E'=1+E, G'=1+G, Q'=1, M'=1, [ 0>=E && 0>=D && Q>=1 && 0>=M && Q==1 ], cost: 2 63: f58 -> f10 : E'=1+E, G'=1+G, Q'=1, M'=1, [ 0>=D && Q>=1 && E==1 && 0>=M && Q==1 ], cost: 2 65: f58 -> f10 : D'=free_12, E'=0, F'=1+F, G'=1+G, Q'=1, M'=0, [ E>=2 && 0>=D && free_12>=0 && M>=1 && Q==1 ], cost: 2 66: f58 -> f10 : D'=free_12, E'=0, F'=1+F, G'=1+G, Q'=1, M'=1, [ E>=2 && 0>=D && free_12>=0 && 0>=M && Q==1 ], cost: 2 61: f58 -> f22 : E'=1+E, J'=free_3, [ 0>=E && 0>=D && Q>=1 && free_3>=0 && Q>=2 && 1>=free_3 ], cost: 2 64: f58 -> f22 : E'=1+E, J'=free_3, [ 0>=D && Q>=1 && E==1 && free_3>=0 && Q>=2 && 1>=free_3 ], cost: 2 67: f58 -> f22 : D'=free_12, E'=0, F'=1+F, J'=free_2, [ E>=2 && 0>=D && free_12>=0 && free_2>=0 && 0>=Q && 1>=free_2 ], cost: 2 68: f58 -> f22 : D'=free_12, E'=0, F'=1+F, J'=free_3, [ E>=2 && 0>=D && free_12>=0 && free_3>=0 && Q>=2 && 1>=free_3 ], cost: 2 72: f58 -> f22 : D'=-1+D, J'=free_3, [ D>=1 && free_3>=0 && Q>=2 && 1>=free_3 ], cost: 2 Applied chaining over branches and pruning: Start location: f0 27: f45 -> f58 : Q'=free_10, P'=0, [ free_10>=0 && P>=1 && 1>=free_10 ], cost: 1 28: f45 -> f58 : Q'=free_11, P'=1, [ free_11>=0 && 0>=P && 1>=free_11 ], cost: 1 2: f0 -> f10 : C'=free, D'=free_1, E'=0, F'=1, G'=0, [ free>=1 && free_1>=0 ], cost: 1 36: f10 -> f22 : H'=1, J'=free_5, K'=1, L'=M, [ C>=1+G && 0>=G && 1+G>=C && 1>=free_5 && free_5>=0 ], cost: 2 37: f10 -> f22 : H'=1, J'=free_6, K'=0, L'=M, [ C>=1+G && 0>=G && C>=2+G && 1>=free_6 && free_6>=0 ], cost: 2 38: f10 -> f22 : H'=0, J'=free_5, K'=1, L'=M, [ C>=1+G && G>=1 && 1+G>=C && 1>=free_5 && free_5>=0 ], cost: 2 39: f10 -> f22 : H'=0, J'=free_6, K'=0, L'=M, [ C>=1+G && G>=1 && C>=2+G && 1>=free_6 && free_6>=0 ], cost: 2 94: f22 -> f45 : A'=H, B'=0, D'=free_7, E'=1, F'=1+F, J'=free_4, N'=1, O'=L, P'=L, Q_1'=1, [ E>=2 && 0>=D && free_7>=0 && 0>=J && 1>=free_4 && free_4>=0 && free_4>=1 && 0>=free_7 && 0>=0 && N>=1 && free_4>=1 && 0>=1+H && L==P && K==0 ], cost: 6 95: f22 -> f45 : A'=H, B'=0, D'=free_7, E'=1, F'=1+F, J'=free_4, N'=1, O'=L, P'=L, Q_1'=1, [ E>=2 && 0>=D && free_7>=0 && 0>=J && 1>=free_4 && free_4>=0 && free_4>=1 && 0>=free_7 && 0>=0 && N>=1 && free_4>=1 && H>=1 && L==P && K==0 ], cost: 6 97: f22 -> f45 : A'=H, B'=K, D'=free_7, E'=1, F'=1+F, J'=free_4, N'=1, O'=L, P'=L, Q_1'=2, [ E>=2 && 0>=D && free_7>=0 && 0>=J && 1>=free_4 && free_4>=0 && free_4>=1 && 0>=free_7 && 0>=0 && N>=1 && free_4>=1 && 0>=1+H && L==P && 0>=1+K && 0>=K && 0>=H ], cost: 7 103: f22 -> f45 : A'=0, B'=K, D'=free_7, E'=1, F'=1+F, J'=free_4, N'=1, O'=L, P'=L, Q_1'=3, [ E>=2 && 0>=D && free_7>=0 && 0>=J && 1>=free_4 && free_4>=0 && free_4>=1 && 0>=free_7 && 0>=0 && 0>=N && free_4>=1 && H==0 && L==L && K>=1 && 0>=0 && K>=1 ], cost: 7 108: f22 -> f45 : A'=0, B'=K, E'=1+E, N'=1, O'=L, P'=L, Q_1'=3, [ J>=1 && 0>=D && 0>=E && N>=1 && J>=1 && H==0 && L==P && K>=1 && 0>=0 && K>=1 ], cost: 5 99: f22 -> f58 : A'=H, B'=K, D'=free_7, E'=1, F'=1+F, Q'=free_8, J'=free_4, N'=1, O'=L, [ E>=2 && 0>=D && free_7>=0 && 0>=J && 1>=free_4 && free_4>=0 && free_4>=1 && 0>=free_7 && 0>=0 && N>=1 && free_4>=1 && free_8>=0 && L>=1+P && 1>=free_8 ], cost: 5 100: f22 -> f58 : A'=H, B'=K, D'=free_7, E'=1, F'=1+F, Q'=free_9, J'=free_4, N'=1, O'=L, [ E>=2 && 0>=D && free_7>=0 && 0>=J && 1>=free_4 && free_4>=0 && free_4>=1 && 0>=free_7 && 0>=0 && N>=1 && free_4>=1 && free_9>=0 && P>=1+L && 1>=free_9 ], cost: 5 111: f22 -> f58 : A'=H, B'=K, E'=1+E, Q'=free_8, N'=1, O'=L, [ J>=1 && 0>=D && 0>=E && N>=1 && J>=1 && free_8>=0 && L>=1+P && 1>=free_8 ], cost: 3 112: f22 -> f58 : A'=H, B'=K, E'=1+E, Q'=free_9, N'=1, O'=L, [ J>=1 && 0>=D && 0>=E && N>=1 && J>=1 && free_9>=0 && P>=1+L && 1>=free_9 ], cost: 3 78: f22 -> [14] : D'=0, J'=0, [ D>=1 && 0>=J && 1>=0 && 0>=0 ], cost: 2*D 79: f22 -> [15] : D'=0, J'=0, [ D>=1 && 0>=J && 1>=0 && 0>=0 ], cost: 2*D 80: f22 -> [16] : D'=0, J'=0, [ D>=1 && 0>=J && 1>=0 && 0>=0 ], cost: 2*D 81: f22 -> [17] : D'=0, J'=0, [ D>=1 && 0>=J && 1>=0 && 0>=0 ], cost: 2*D 82: f22 -> [18] : D'=0, J'=0, [ D>=1 && 0>=J && 1>=0 && 0>=0 ], cost: 2*D 59: f58 -> f10 : E'=1+E, G'=1+G, Q'=1, M'=0, [ 0>=E && 0>=D && Q>=1 && M>=1 && Q==1 ], cost: 2 60: f58 -> f10 : E'=1+E, G'=1+G, Q'=1, M'=1, [ 0>=E && 0>=D && Q>=1 && 0>=M && Q==1 ], cost: 2 63: f58 -> f10 : E'=1+E, G'=1+G, Q'=1, M'=1, [ 0>=D && Q>=1 && E==1 && 0>=M && Q==1 ], cost: 2 65: f58 -> f10 : D'=free_12, E'=0, F'=1+F, G'=1+G, Q'=1, M'=0, [ E>=2 && 0>=D && free_12>=0 && M>=1 && Q==1 ], cost: 2 66: f58 -> f10 : D'=free_12, E'=0, F'=1+F, G'=1+G, Q'=1, M'=1, [ E>=2 && 0>=D && free_12>=0 && 0>=M && Q==1 ], cost: 2 61: f58 -> f22 : E'=1+E, J'=free_3, [ 0>=E && 0>=D && Q>=1 && free_3>=0 && Q>=2 && 1>=free_3 ], cost: 2 64: f58 -> f22 : E'=1+E, J'=free_3, [ 0>=D && Q>=1 && E==1 && free_3>=0 && Q>=2 && 1>=free_3 ], cost: 2 67: f58 -> f22 : D'=free_12, E'=0, F'=1+F, J'=free_2, [ E>=2 && 0>=D && free_12>=0 && free_2>=0 && 0>=Q && 1>=free_2 ], cost: 2 68: f58 -> f22 : D'=free_12, E'=0, F'=1+F, J'=free_3, [ E>=2 && 0>=D && free_12>=0 && free_3>=0 && Q>=2 && 1>=free_3 ], cost: 2 72: f58 -> f22 : D'=-1+D, J'=free_3, [ D>=1 && free_3>=0 && Q>=2 && 1>=free_3 ], cost: 2 Applied chaining over branches and pruning: Start location: f0 2: f0 -> f10 : C'=free, D'=free_1, E'=0, F'=1, G'=0, [ free>=1 && free_1>=0 ], cost: 1 36: f10 -> f22 : H'=1, J'=free_5, K'=1, L'=M, [ C>=1+G && 0>=G && 1+G>=C && 1>=free_5 && free_5>=0 ], cost: 2 37: f10 -> f22 : H'=1, J'=free_6, K'=0, L'=M, [ C>=1+G && 0>=G && C>=2+G && 1>=free_6 && free_6>=0 ], cost: 2 38: f10 -> f22 : H'=0, J'=free_5, K'=1, L'=M, [ C>=1+G && G>=1 && 1+G>=C && 1>=free_5 && free_5>=0 ], cost: 2 39: f10 -> f22 : H'=0, J'=free_6, K'=0, L'=M, [ C>=1+G && G>=1 && C>=2+G && 1>=free_6 && free_6>=0 ], cost: 2 99: f22 -> f58 : A'=H, B'=K, D'=free_7, E'=1, F'=1+F, Q'=free_8, J'=free_4, N'=1, O'=L, [ E>=2 && 0>=D && free_7>=0 && 0>=J && 1>=free_4 && free_4>=0 && free_4>=1 && 0>=free_7 && 0>=0 && N>=1 && free_4>=1 && free_8>=0 && L>=1+P && 1>=free_8 ], cost: 5 100: f22 -> f58 : A'=H, B'=K, D'=free_7, E'=1, F'=1+F, Q'=free_9, J'=free_4, N'=1, O'=L, [ E>=2 && 0>=D && free_7>=0 && 0>=J && 1>=free_4 && free_4>=0 && free_4>=1 && 0>=free_7 && 0>=0 && N>=1 && free_4>=1 && free_9>=0 && P>=1+L && 1>=free_9 ], cost: 5 112: f22 -> f58 : A'=H, B'=K, E'=1+E, Q'=free_9, N'=1, O'=L, [ J>=1 && 0>=D && 0>=E && N>=1 && J>=1 && free_9>=0 && P>=1+L && 1>=free_9 ], cost: 3 125: f22 -> f58 : A'=H, B'=0, D'=free_7, E'=1, F'=1+F, Q'=free_10, J'=free_4, N'=1, O'=L, P'=0, Q_1'=1, [ E>=2 && 0>=D && free_7>=0 && 0>=J && 1>=free_4 && free_4>=0 && free_4>=1 && 0>=free_7 && 0>=0 && N>=1 && free_4>=1 && H>=1 && L==P && K==0 && free_10>=0 && L>=1 && 1>=free_10 ], cost: 7 126: f22 -> f58 : A'=H, B'=0, D'=free_7, E'=1, F'=1+F, Q'=free_11, J'=free_4, N'=1, O'=L, P'=1, Q_1'=1, [ E>=2 && 0>=D && free_7>=0 && 0>=J && 1>=free_4 && free_4>=0 && free_4>=1 && 0>=free_7 && 0>=0 && N>=1 && free_4>=1 && H>=1 && L==P && K==0 && free_11>=0 && 0>=L && 1>=free_11 ], cost: 7 78: f22 -> [14] : D'=0, J'=0, [ D>=1 && 0>=J && 1>=0 && 0>=0 ], cost: 2*D 79: f22 -> [15] : D'=0, J'=0, [ D>=1 && 0>=J && 1>=0 && 0>=0 ], cost: 2*D 80: f22 -> [16] : D'=0, J'=0, [ D>=1 && 0>=J && 1>=0 && 0>=0 ], cost: 2*D 81: f22 -> [17] : D'=0, J'=0, [ D>=1 && 0>=J && 1>=0 && 0>=0 ], cost: 2*D 82: f22 -> [18] : D'=0, J'=0, [ D>=1 && 0>=J && 1>=0 && 0>=0 ], cost: 2*D 59: f58 -> f10 : E'=1+E, G'=1+G, Q'=1, M'=0, [ 0>=E && 0>=D && Q>=1 && M>=1 && Q==1 ], cost: 2 60: f58 -> f10 : E'=1+E, G'=1+G, Q'=1, M'=1, [ 0>=E && 0>=D && Q>=1 && 0>=M && Q==1 ], cost: 2 63: f58 -> f10 : E'=1+E, G'=1+G, Q'=1, M'=1, [ 0>=D && Q>=1 && E==1 && 0>=M && Q==1 ], cost: 2 65: f58 -> f10 : D'=free_12, E'=0, F'=1+F, G'=1+G, Q'=1, M'=0, [ E>=2 && 0>=D && free_12>=0 && M>=1 && Q==1 ], cost: 2 66: f58 -> f10 : D'=free_12, E'=0, F'=1+F, G'=1+G, Q'=1, M'=1, [ E>=2 && 0>=D && free_12>=0 && 0>=M && Q==1 ], cost: 2 61: f58 -> f22 : E'=1+E, J'=free_3, [ 0>=E && 0>=D && Q>=1 && free_3>=0 && Q>=2 && 1>=free_3 ], cost: 2 64: f58 -> f22 : E'=1+E, J'=free_3, [ 0>=D && Q>=1 && E==1 && free_3>=0 && Q>=2 && 1>=free_3 ], cost: 2 67: f58 -> f22 : D'=free_12, E'=0, F'=1+F, J'=free_2, [ E>=2 && 0>=D && free_12>=0 && free_2>=0 && 0>=Q && 1>=free_2 ], cost: 2 68: f58 -> f22 : D'=free_12, E'=0, F'=1+F, J'=free_3, [ E>=2 && 0>=D && free_12>=0 && free_3>=0 && Q>=2 && 1>=free_3 ], cost: 2 72: f58 -> f22 : D'=-1+D, J'=free_3, [ D>=1 && free_3>=0 && Q>=2 && 1>=free_3 ], cost: 2 Applied chaining over branches and pruning: Start location: f0 2: f0 -> f10 : C'=free, D'=free_1, E'=0, F'=1, G'=0, [ free>=1 && free_1>=0 ], cost: 1 36: f10 -> f22 : H'=1, J'=free_5, K'=1, L'=M, [ C>=1+G && 0>=G && 1+G>=C && 1>=free_5 && free_5>=0 ], cost: 2 37: f10 -> f22 : H'=1, J'=free_6, K'=0, L'=M, [ C>=1+G && 0>=G && C>=2+G && 1>=free_6 && free_6>=0 ], cost: 2 38: f10 -> f22 : H'=0, J'=free_5, K'=1, L'=M, [ C>=1+G && G>=1 && 1+G>=C && 1>=free_5 && free_5>=0 ], cost: 2 39: f10 -> f22 : H'=0, J'=free_6, K'=0, L'=M, [ C>=1+G && G>=1 && C>=2+G && 1>=free_6 && free_6>=0 ], cost: 2 133: f22 -> f10 : A'=H, B'=K, D'=free_7, E'=2, F'=1+F, G'=1+G, Q'=1, J'=free_4, M'=1, N'=1, O'=L, [ E>=2 && 0>=D && free_7>=0 && 0>=J && 1>=free_4 && free_4>=0 && free_4>=1 && 0>=free_7 && 0>=0 && N>=1 && free_4>=1 && free_8>=0 && L>=1+P && 1>=free_8 && 0>=free_7 && free_8>=1 && 1==1 && 0>=M && free_8==1 ], cost: 7 134: f22 -> f10 : A'=H, B'=K, D'=free_7, E'=2, F'=1+F, G'=1+G, Q'=1, J'=free_4, M'=1, N'=1, O'=L, [ E>=2 && 0>=D && free_7>=0 && 0>=J && 1>=free_4 && free_4>=0 && free_4>=1 && 0>=free_7 && 0>=0 && N>=1 && free_4>=1 && free_9>=0 && P>=1+L && 1>=free_9 && 0>=free_7 && free_9>=1 && 1==1 && 0>=M && free_9==1 ], cost: 7 135: f22 -> f10 : A'=H, B'=K, E'=2+E, G'=1+G, Q'=1, M'=0, N'=1, O'=L, [ J>=1 && 0>=D && 0>=E && N>=1 && J>=1 && free_9>=0 && P>=1+L && 1>=free_9 && 0>=1+E && 0>=D && free_9>=1 && M>=1 && free_9==1 ], cost: 5 136: f22 -> f10 : A'=H, B'=K, E'=2+E, G'=1+G, Q'=1, M'=1, N'=1, O'=L, [ J>=1 && 0>=D && 0>=E && N>=1 && J>=1 && free_9>=0 && P>=1+L && 1>=free_9 && 0>=1+E && 0>=D && free_9>=1 && 0>=M && free_9==1 ], cost: 5 137: f22 -> f10 : A'=H, B'=K, E'=2+E, G'=1+G, Q'=1, M'=1, N'=1, O'=L, [ J>=1 && 0>=D && 0>=E && N>=1 && J>=1 && free_9>=0 && P>=1+L && 1>=free_9 && 0>=D && free_9>=1 && 1+E==1 && 0>=M && free_9==1 ], cost: 5 78: f22 -> [14] : D'=0, J'=0, [ D>=1 && 0>=J && 1>=0 && 0>=0 ], cost: 2*D 79: f22 -> [15] : D'=0, J'=0, [ D>=1 && 0>=J && 1>=0 && 0>=0 ], cost: 2*D 80: f22 -> [16] : D'=0, J'=0, [ D>=1 && 0>=J && 1>=0 && 0>=0 ], cost: 2*D 81: f22 -> [17] : D'=0, J'=0, [ D>=1 && 0>=J && 1>=0 && 0>=0 ], cost: 2*D 82: f22 -> [18] : D'=0, J'=0, [ D>=1 && 0>=J && 1>=0 && 0>=0 ], cost: 2*D Applied chaining over branches and pruning: Start location: f0 2: f0 -> f10 : C'=free, D'=free_1, E'=0, F'=1, G'=0, [ free>=1 && free_1>=0 ], cost: 1 140: f10 -> f10 : A'=1, B'=1, D'=free_7, E'=2, F'=1+F, G'=1+G, H'=1, Q'=1, J'=free_4, K'=1, L'=M, M'=1, N'=1, O'=M, [ C>=1+G && 0>=G && 1+G>=C && 1>=free_5 && free_5>=0 && E>=2 && 0>=D && free_7>=0 && 0>=free_5 && 1>=free_4 && free_4>=0 && free_4>=1 && 0>=free_7 && 0>=0 && N>=1 && free_4>=1 && free_8>=0 && M>=1+P && 1>=free_8 && 0>=free_7 && free_8>=1 && 1==1 && 0>=M && free_8==1 ], cost: 9 141: f10 -> f10 : A'=1, B'=1, D'=free_7, E'=2, F'=1+F, G'=1+G, H'=1, Q'=1, J'=free_4, K'=1, L'=M, M'=1, N'=1, O'=M, [ C>=1+G && 0>=G && 1+G>=C && 1>=free_5 && free_5>=0 && E>=2 && 0>=D && free_7>=0 && 0>=free_5 && 1>=free_4 && free_4>=0 && free_4>=1 && 0>=free_7 && 0>=0 && N>=1 && free_4>=1 && free_9>=0 && P>=1+M && 1>=free_9 && 0>=free_7 && free_9>=1 && 1==1 && 0>=M && free_9==1 ], cost: 9 143: f10 -> f10 : A'=1, B'=1, E'=2+E, G'=1+G, H'=1, Q'=1, J'=free_5, K'=1, L'=M, M'=1, N'=1, O'=M, [ C>=1+G && 0>=G && 1+G>=C && 1>=free_5 && free_5>=0 && free_5>=1 && 0>=D && 0>=E && N>=1 && free_5>=1 && free_9>=0 && P>=1+M && 1>=free_9 && 0>=1+E && 0>=D && free_9>=1 && 0>=M && free_9==1 ], cost: 7 152: f10 -> f10 : A'=1, B'=0, E'=2+E, G'=1+G, H'=1, Q'=1, J'=free_6, K'=0, L'=M, M'=0, N'=1, O'=M, [ C>=1+G && 0>=G && C>=2+G && 1>=free_6 && free_6>=0 && free_6>=1 && 0>=D && 0>=E && N>=1 && free_6>=1 && free_9>=0 && P>=1+M && 1>=free_9 && 0>=1+E && 0>=D && free_9>=1 && M>=1 && free_9==1 ], cost: 7 160: f10 -> f10 : A'=0, B'=1, D'=free_7, E'=2, F'=1+F, G'=1+G, H'=0, Q'=1, J'=free_4, K'=1, L'=M, M'=1, N'=1, O'=M, [ C>=1+G && G>=1 && 1+G>=C && 1>=free_5 && free_5>=0 && E>=2 && 0>=D && free_7>=0 && 0>=free_5 && 1>=free_4 && free_4>=0 && free_4>=1 && 0>=free_7 && 0>=0 && N>=1 && free_4>=1 && free_8>=0 && M>=1+P && 1>=free_8 && 0>=free_7 && free_8>=1 && 1==1 && 0>=M && free_8==1 ], cost: 9 145: f10 -> [14] : D'=0, H'=1, J'=0, K'=1, L'=M, [ C>=1+G && 0>=G && 1+G>=C && 1>=free_5 && free_5>=0 && D>=1 && 0>=free_5 && 1>=0 && 0>=0 ], cost: 2+2*D 155: f10 -> [14] : D'=0, H'=1, J'=0, K'=0, L'=M, [ C>=1+G && 0>=G && C>=2+G && 1>=free_6 && free_6>=0 && D>=1 && 0>=free_6 && 1>=0 && 0>=0 ], cost: 2+2*D 165: f10 -> [14] : D'=0, H'=0, J'=0, K'=1, L'=M, [ C>=1+G && G>=1 && 1+G>=C && 1>=free_5 && free_5>=0 && D>=1 && 0>=free_5 && 1>=0 && 0>=0 ], cost: 2+2*D 175: f10 -> [14] : D'=0, H'=0, J'=0, K'=0, L'=M, [ C>=1+G && G>=1 && C>=2+G && 1>=free_6 && free_6>=0 && D>=1 && 0>=free_6 && 1>=0 && 0>=0 ], cost: 2+2*D 146: f10 -> [15] : D'=0, H'=1, J'=0, K'=1, L'=M, [ C>=1+G && 0>=G && 1+G>=C && 1>=free_5 && free_5>=0 && D>=1 && 0>=free_5 && 1>=0 && 0>=0 ], cost: 2+2*D 156: f10 -> [15] : D'=0, H'=1, J'=0, K'=0, L'=M, [ C>=1+G && 0>=G && C>=2+G && 1>=free_6 && free_6>=0 && D>=1 && 0>=free_6 && 1>=0 && 0>=0 ], cost: 2+2*D 166: f10 -> [15] : D'=0, H'=0, J'=0, K'=1, L'=M, [ C>=1+G && G>=1 && 1+G>=C && 1>=free_5 && free_5>=0 && D>=1 && 0>=free_5 && 1>=0 && 0>=0 ], cost: 2+2*D 176: f10 -> [15] : D'=0, H'=0, J'=0, K'=0, L'=M, [ C>=1+G && G>=1 && C>=2+G && 1>=free_6 && free_6>=0 && D>=1 && 0>=free_6 && 1>=0 && 0>=0 ], cost: 2+2*D 147: f10 -> [16] : D'=0, H'=1, J'=0, K'=1, L'=M, [ C>=1+G && 0>=G && 1+G>=C && 1>=free_5 && free_5>=0 && D>=1 && 0>=free_5 && 1>=0 && 0>=0 ], cost: 2+2*D 157: f10 -> [16] : D'=0, H'=1, J'=0, K'=0, L'=M, [ C>=1+G && 0>=G && C>=2+G && 1>=free_6 && free_6>=0 && D>=1 && 0>=free_6 && 1>=0 && 0>=0 ], cost: 2+2*D 167: f10 -> [16] : D'=0, H'=0, J'=0, K'=1, L'=M, [ C>=1+G && G>=1 && 1+G>=C && 1>=free_5 && free_5>=0 && D>=1 && 0>=free_5 && 1>=0 && 0>=0 ], cost: 2+2*D 177: f10 -> [16] : D'=0, H'=0, J'=0, K'=0, L'=M, [ C>=1+G && G>=1 && C>=2+G && 1>=free_6 && free_6>=0 && D>=1 && 0>=free_6 && 1>=0 && 0>=0 ], cost: 2+2*D 148: f10 -> [17] : D'=0, H'=1, J'=0, K'=1, L'=M, [ C>=1+G && 0>=G && 1+G>=C && 1>=free_5 && free_5>=0 && D>=1 && 0>=free_5 && 1>=0 && 0>=0 ], cost: 2+2*D 158: f10 -> [17] : D'=0, H'=1, J'=0, K'=0, L'=M, [ C>=1+G && 0>=G && C>=2+G && 1>=free_6 && free_6>=0 && D>=1 && 0>=free_6 && 1>=0 && 0>=0 ], cost: 2+2*D 168: f10 -> [17] : D'=0, H'=0, J'=0, K'=1, L'=M, [ C>=1+G && G>=1 && 1+G>=C && 1>=free_5 && free_5>=0 && D>=1 && 0>=free_5 && 1>=0 && 0>=0 ], cost: 2+2*D 178: f10 -> [17] : D'=0, H'=0, J'=0, K'=0, L'=M, [ C>=1+G && G>=1 && C>=2+G && 1>=free_6 && free_6>=0 && D>=1 && 0>=free_6 && 1>=0 && 0>=0 ], cost: 2+2*D 149: f10 -> [18] : D'=0, H'=1, J'=0, K'=1, L'=M, [ C>=1+G && 0>=G && 1+G>=C && 1>=free_5 && free_5>=0 && D>=1 && 0>=free_5 && 1>=0 && 0>=0 ], cost: 2+2*D 159: f10 -> [18] : D'=0, H'=1, J'=0, K'=0, L'=M, [ C>=1+G && 0>=G && C>=2+G && 1>=free_6 && free_6>=0 && D>=1 && 0>=free_6 && 1>=0 && 0>=0 ], cost: 2+2*D 169: f10 -> [18] : D'=0, H'=0, J'=0, K'=1, L'=M, [ C>=1+G && G>=1 && 1+G>=C && 1>=free_5 && free_5>=0 && D>=1 && 0>=free_5 && 1>=0 && 0>=0 ], cost: 2+2*D 179: f10 -> [18] : D'=0, H'=0, J'=0, K'=0, L'=M, [ C>=1+G && G>=1 && C>=2+G && 1>=free_6 && free_6>=0 && D>=1 && 0>=free_6 && 1>=0 && 0>=0 ], cost: 2+2*D Eliminating 5 self-loops for location f10 Self-Loop 140 has the metering function: -1+C-G, resulting in the new transition 180. Self-Loop 141 has the metering function: -1+C-G, resulting in the new transition 181. Self-Loop 143 has the metering function: -1+C-G, resulting in the new transition 182. Self-Loop 160 has the metering function: -1+C-G, resulting in the new transition 186. Found this metering function when nesting loops: -2+C-G, Removing the self-loops: 140 141 143 152 160 183 184. Adding an epsilon transition (to model nonexecution of the loops): 187. Removed all Self-loops using metering functions (where possible): Start location: f0 2: f0 -> f10 : C'=free, D'=free_1, E'=0, F'=1, G'=0, [ free>=1 && free_1>=0 ], cost: 1 180: f10 -> [19] : A'=1, B'=1, D'=0, E'=2, F'=-1+F+C-G, G'=-1+C, H'=1, Q'=1, J'=1, K'=1, L'=1, M'=1, N'=1, O'=1, [ 1-C+G==0 && 0>=G && E>=2 && 0>=D && N>=1 && M>=1+P && 0>=M ], cost: -9+9*C-9*G 181: f10 -> [19] : A'=1, B'=1, D'=0, E'=2, F'=-1+F+C-G, G'=-1+C, H'=1, Q'=1, J'=1, K'=1, L'=1, M'=1, N'=1, O'=1, [ 1-C+G==0 && 0>=G && E>=2 && 0>=D && N>=1 && P>=1+M && 0>=M ], cost: -9+9*C-9*G 182: f10 -> [19] : A'=1, B'=1, E'=-2+E+2*C-2*G, G'=-1+C, H'=1, Q'=1, J'=1, K'=1, L'=1, M'=1, N'=1, O'=1, [ 1-C+G==0 && 0>=G && 0>=D && N>=1 && P>=1+M && 0>=1+E && 0>=M ], cost: -7+7*C-7*G 185: f10 -> [19] : A'=1, B'=0, E'=2+E, G'=1+G, H'=1, Q'=1, J'=1, K'=0, L'=M, M'=0, N'=1, O'=M, [ 0>=G && C>=2+G && 0>=D && N>=1 && P>=1+M && 0>=1+E && M>=1 ], cost: 7 186: f10 -> [19] : A'=0, B'=1, D'=0, E'=2, F'=-1+F+C-G, G'=-1+C, H'=0, Q'=1, J'=1, K'=1, L'=1, M'=1, N'=1, O'=1, [ 1-C+G==0 && G>=1 && E>=2 && 0>=D && N>=1 && M>=1+P && 0>=M ], cost: -9+9*C-9*G 187: f10 -> [19] : [], cost: 0 145: [19] -> [14] : D'=0, H'=1, J'=0, K'=1, L'=M, [ C>=1+G && 0>=G && 1+G>=C && 1>=free_5 && free_5>=0 && D>=1 && 0>=free_5 && 1>=0 && 0>=0 ], cost: 2+2*D 155: [19] -> [14] : D'=0, H'=1, J'=0, K'=0, L'=M, [ C>=1+G && 0>=G && C>=2+G && 1>=free_6 && free_6>=0 && D>=1 && 0>=free_6 && 1>=0 && 0>=0 ], cost: 2+2*D 165: [19] -> [14] : D'=0, H'=0, J'=0, K'=1, L'=M, [ C>=1+G && G>=1 && 1+G>=C && 1>=free_5 && free_5>=0 && D>=1 && 0>=free_5 && 1>=0 && 0>=0 ], cost: 2+2*D 175: [19] -> [14] : D'=0, H'=0, J'=0, K'=0, L'=M, [ C>=1+G && G>=1 && C>=2+G && 1>=free_6 && free_6>=0 && D>=1 && 0>=free_6 && 1>=0 && 0>=0 ], cost: 2+2*D 146: [19] -> [15] : D'=0, H'=1, J'=0, K'=1, L'=M, [ C>=1+G && 0>=G && 1+G>=C && 1>=free_5 && free_5>=0 && D>=1 && 0>=free_5 && 1>=0 && 0>=0 ], cost: 2+2*D 156: [19] -> [15] : D'=0, H'=1, J'=0, K'=0, L'=M, [ C>=1+G && 0>=G && C>=2+G && 1>=free_6 && free_6>=0 && D>=1 && 0>=free_6 && 1>=0 && 0>=0 ], cost: 2+2*D 166: [19] -> [15] : D'=0, H'=0, J'=0, K'=1, L'=M, [ C>=1+G && G>=1 && 1+G>=C && 1>=free_5 && free_5>=0 && D>=1 && 0>=free_5 && 1>=0 && 0>=0 ], cost: 2+2*D 176: [19] -> [15] : D'=0, H'=0, J'=0, K'=0, L'=M, [ C>=1+G && G>=1 && C>=2+G && 1>=free_6 && free_6>=0 && D>=1 && 0>=free_6 && 1>=0 && 0>=0 ], cost: 2+2*D 147: [19] -> [16] : D'=0, H'=1, J'=0, K'=1, L'=M, [ C>=1+G && 0>=G && 1+G>=C && 1>=free_5 && free_5>=0 && D>=1 && 0>=free_5 && 1>=0 && 0>=0 ], cost: 2+2*D 157: [19] -> [16] : D'=0, H'=1, J'=0, K'=0, L'=M, [ C>=1+G && 0>=G && C>=2+G && 1>=free_6 && free_6>=0 && D>=1 && 0>=free_6 && 1>=0 && 0>=0 ], cost: 2+2*D 167: [19] -> [16] : D'=0, H'=0, J'=0, K'=1, L'=M, [ C>=1+G && G>=1 && 1+G>=C && 1>=free_5 && free_5>=0 && D>=1 && 0>=free_5 && 1>=0 && 0>=0 ], cost: 2+2*D 177: [19] -> [16] : D'=0, H'=0, J'=0, K'=0, L'=M, [ C>=1+G && G>=1 && C>=2+G && 1>=free_6 && free_6>=0 && D>=1 && 0>=free_6 && 1>=0 && 0>=0 ], cost: 2+2*D 148: [19] -> [17] : D'=0, H'=1, J'=0, K'=1, L'=M, [ C>=1+G && 0>=G && 1+G>=C && 1>=free_5 && free_5>=0 && D>=1 && 0>=free_5 && 1>=0 && 0>=0 ], cost: 2+2*D 158: [19] -> [17] : D'=0, H'=1, J'=0, K'=0, L'=M, [ C>=1+G && 0>=G && C>=2+G && 1>=free_6 && free_6>=0 && D>=1 && 0>=free_6 && 1>=0 && 0>=0 ], cost: 2+2*D 168: [19] -> [17] : D'=0, H'=0, J'=0, K'=1, L'=M, [ C>=1+G && G>=1 && 1+G>=C && 1>=free_5 && free_5>=0 && D>=1 && 0>=free_5 && 1>=0 && 0>=0 ], cost: 2+2*D 178: [19] -> [17] : D'=0, H'=0, J'=0, K'=0, L'=M, [ C>=1+G && G>=1 && C>=2+G && 1>=free_6 && free_6>=0 && D>=1 && 0>=free_6 && 1>=0 && 0>=0 ], cost: 2+2*D 149: [19] -> [18] : D'=0, H'=1, J'=0, K'=1, L'=M, [ C>=1+G && 0>=G && 1+G>=C && 1>=free_5 && free_5>=0 && D>=1 && 0>=free_5 && 1>=0 && 0>=0 ], cost: 2+2*D 159: [19] -> [18] : D'=0, H'=1, J'=0, K'=0, L'=M, [ C>=1+G && 0>=G && C>=2+G && 1>=free_6 && free_6>=0 && D>=1 && 0>=free_6 && 1>=0 && 0>=0 ], cost: 2+2*D 169: [19] -> [18] : D'=0, H'=0, J'=0, K'=1, L'=M, [ C>=1+G && G>=1 && 1+G>=C && 1>=free_5 && free_5>=0 && D>=1 && 0>=free_5 && 1>=0 && 0>=0 ], cost: 2+2*D 179: [19] -> [18] : D'=0, H'=0, J'=0, K'=0, L'=M, [ C>=1+G && G>=1 && C>=2+G && 1>=free_6 && free_6>=0 && D>=1 && 0>=free_6 && 1>=0 && 0>=0 ], cost: 2+2*D Applied chaining over branches and pruning: Start location: f0 188: f0 -> [19] : C'=free, D'=free_1, E'=0, F'=1, G'=0, [ free>=1 && free_1>=0 ], cost: 1 145: [19] -> [14] : D'=0, H'=1, J'=0, K'=1, L'=M, [ C>=1+G && 0>=G && 1+G>=C && 1>=free_5 && free_5>=0 && D>=1 && 0>=free_5 && 1>=0 && 0>=0 ], cost: 2+2*D 155: [19] -> [14] : D'=0, H'=1, J'=0, K'=0, L'=M, [ C>=1+G && 0>=G && C>=2+G && 1>=free_6 && free_6>=0 && D>=1 && 0>=free_6 && 1>=0 && 0>=0 ], cost: 2+2*D 165: [19] -> [14] : D'=0, H'=0, J'=0, K'=1, L'=M, [ C>=1+G && G>=1 && 1+G>=C && 1>=free_5 && free_5>=0 && D>=1 && 0>=free_5 && 1>=0 && 0>=0 ], cost: 2+2*D 175: [19] -> [14] : D'=0, H'=0, J'=0, K'=0, L'=M, [ C>=1+G && G>=1 && C>=2+G && 1>=free_6 && free_6>=0 && D>=1 && 0>=free_6 && 1>=0 && 0>=0 ], cost: 2+2*D 146: [19] -> [15] : D'=0, H'=1, J'=0, K'=1, L'=M, [ C>=1+G && 0>=G && 1+G>=C && 1>=free_5 && free_5>=0 && D>=1 && 0>=free_5 && 1>=0 && 0>=0 ], cost: 2+2*D 156: [19] -> [15] : D'=0, H'=1, J'=0, K'=0, L'=M, [ C>=1+G && 0>=G && C>=2+G && 1>=free_6 && free_6>=0 && D>=1 && 0>=free_6 && 1>=0 && 0>=0 ], cost: 2+2*D 166: [19] -> [15] : D'=0, H'=0, J'=0, K'=1, L'=M, [ C>=1+G && G>=1 && 1+G>=C && 1>=free_5 && free_5>=0 && D>=1 && 0>=free_5 && 1>=0 && 0>=0 ], cost: 2+2*D 176: [19] -> [15] : D'=0, H'=0, J'=0, K'=0, L'=M, [ C>=1+G && G>=1 && C>=2+G && 1>=free_6 && free_6>=0 && D>=1 && 0>=free_6 && 1>=0 && 0>=0 ], cost: 2+2*D 147: [19] -> [16] : D'=0, H'=1, J'=0, K'=1, L'=M, [ C>=1+G && 0>=G && 1+G>=C && 1>=free_5 && free_5>=0 && D>=1 && 0>=free_5 && 1>=0 && 0>=0 ], cost: 2+2*D 157: [19] -> [16] : D'=0, H'=1, J'=0, K'=0, L'=M, [ C>=1+G && 0>=G && C>=2+G && 1>=free_6 && free_6>=0 && D>=1 && 0>=free_6 && 1>=0 && 0>=0 ], cost: 2+2*D 167: [19] -> [16] : D'=0, H'=0, J'=0, K'=1, L'=M, [ C>=1+G && G>=1 && 1+G>=C && 1>=free_5 && free_5>=0 && D>=1 && 0>=free_5 && 1>=0 && 0>=0 ], cost: 2+2*D 177: [19] -> [16] : D'=0, H'=0, J'=0, K'=0, L'=M, [ C>=1+G && G>=1 && C>=2+G && 1>=free_6 && free_6>=0 && D>=1 && 0>=free_6 && 1>=0 && 0>=0 ], cost: 2+2*D 148: [19] -> [17] : D'=0, H'=1, J'=0, K'=1, L'=M, [ C>=1+G && 0>=G && 1+G>=C && 1>=free_5 && free_5>=0 && D>=1 && 0>=free_5 && 1>=0 && 0>=0 ], cost: 2+2*D 158: [19] -> [17] : D'=0, H'=1, J'=0, K'=0, L'=M, [ C>=1+G && 0>=G && C>=2+G && 1>=free_6 && free_6>=0 && D>=1 && 0>=free_6 && 1>=0 && 0>=0 ], cost: 2+2*D 168: [19] -> [17] : D'=0, H'=0, J'=0, K'=1, L'=M, [ C>=1+G && G>=1 && 1+G>=C && 1>=free_5 && free_5>=0 && D>=1 && 0>=free_5 && 1>=0 && 0>=0 ], cost: 2+2*D 178: [19] -> [17] : D'=0, H'=0, J'=0, K'=0, L'=M, [ C>=1+G && G>=1 && C>=2+G && 1>=free_6 && free_6>=0 && D>=1 && 0>=free_6 && 1>=0 && 0>=0 ], cost: 2+2*D 149: [19] -> [18] : D'=0, H'=1, J'=0, K'=1, L'=M, [ C>=1+G && 0>=G && 1+G>=C && 1>=free_5 && free_5>=0 && D>=1 && 0>=free_5 && 1>=0 && 0>=0 ], cost: 2+2*D 159: [19] -> [18] : D'=0, H'=1, J'=0, K'=0, L'=M, [ C>=1+G && 0>=G && C>=2+G && 1>=free_6 && free_6>=0 && D>=1 && 0>=free_6 && 1>=0 && 0>=0 ], cost: 2+2*D 169: [19] -> [18] : D'=0, H'=0, J'=0, K'=1, L'=M, [ C>=1+G && G>=1 && 1+G>=C && 1>=free_5 && free_5>=0 && D>=1 && 0>=free_5 && 1>=0 && 0>=0 ], cost: 2+2*D 179: [19] -> [18] : D'=0, H'=0, J'=0, K'=0, L'=M, [ C>=1+G && G>=1 && C>=2+G && 1>=free_6 && free_6>=0 && D>=1 && 0>=free_6 && 1>=0 && 0>=0 ], cost: 2+2*D Applied chaining over branches and pruning: Start location: f0 189: f0 -> [14] : C'=free, D'=0, E'=0, F'=1, G'=0, H'=1, J'=0, K'=1, L'=M, [ free>=1 && free_1>=0 && free>=1 && 0>=0 && 1>=free && 1>=free_5 && free_5>=0 && free_1>=1 && 0>=free_5 && 1>=0 && 0>=0 ], cost: 3+2*free_1 190: f0 -> [14] : C'=free, D'=0, E'=0, F'=1, G'=0, H'=1, J'=0, K'=0, L'=M, [ free>=1 && free_1>=0 && free>=1 && 0>=0 && free>=2 && 1>=free_6 && free_6>=0 && free_1>=1 && 0>=free_6 && 1>=0 && 0>=0 ], cost: 3+2*free_1 191: f0 -> [15] : C'=free, D'=0, E'=0, F'=1, G'=0, H'=1, J'=0, K'=1, L'=M, [ free>=1 && free_1>=0 && free>=1 && 0>=0 && 1>=free && 1>=free_5 && free_5>=0 && free_1>=1 && 0>=free_5 && 1>=0 && 0>=0 ], cost: 3+2*free_1 192: f0 -> [15] : C'=free, D'=0, E'=0, F'=1, G'=0, H'=1, J'=0, K'=0, L'=M, [ free>=1 && free_1>=0 && free>=1 && 0>=0 && free>=2 && 1>=free_6 && free_6>=0 && free_1>=1 && 0>=free_6 && 1>=0 && 0>=0 ], cost: 3+2*free_1 193: f0 -> [16] : C'=free, D'=0, E'=0, F'=1, G'=0, H'=1, J'=0, K'=1, L'=M, [ free>=1 && free_1>=0 && free>=1 && 0>=0 && 1>=free && 1>=free_5 && free_5>=0 && free_1>=1 && 0>=free_5 && 1>=0 && 0>=0 ], cost: 3+2*free_1 194: f0 -> [16] : C'=free, D'=0, E'=0, F'=1, G'=0, H'=1, J'=0, K'=0, L'=M, [ free>=1 && free_1>=0 && free>=1 && 0>=0 && free>=2 && 1>=free_6 && free_6>=0 && free_1>=1 && 0>=free_6 && 1>=0 && 0>=0 ], cost: 3+2*free_1 195: f0 -> [17] : C'=free, D'=0, E'=0, F'=1, G'=0, H'=1, J'=0, K'=1, L'=M, [ free>=1 && free_1>=0 && free>=1 && 0>=0 && 1>=free && 1>=free_5 && free_5>=0 && free_1>=1 && 0>=free_5 && 1>=0 && 0>=0 ], cost: 3+2*free_1 196: f0 -> [17] : C'=free, D'=0, E'=0, F'=1, G'=0, H'=1, J'=0, K'=0, L'=M, [ free>=1 && free_1>=0 && free>=1 && 0>=0 && free>=2 && 1>=free_6 && free_6>=0 && free_1>=1 && 0>=free_6 && 1>=0 && 0>=0 ], cost: 3+2*free_1 197: f0 -> [18] : C'=free, D'=0, E'=0, F'=1, G'=0, H'=1, J'=0, K'=1, L'=M, [ free>=1 && free_1>=0 && free>=1 && 0>=0 && 1>=free && 1>=free_5 && free_5>=0 && free_1>=1 && 0>=free_5 && 1>=0 && 0>=0 ], cost: 3+2*free_1 198: f0 -> [18] : C'=free, D'=0, E'=0, F'=1, G'=0, H'=1, J'=0, K'=0, L'=M, [ free>=1 && free_1>=0 && free>=1 && 0>=0 && free>=2 && 1>=free_6 && free_6>=0 && free_1>=1 && 0>=free_6 && 1>=0 && 0>=0 ], cost: 3+2*free_1 Final control flow graph problem, now checking costs for infinitely many models: Start location: f0 189: f0 -> [14] : C'=free, D'=0, E'=0, F'=1, G'=0, H'=1, J'=0, K'=1, L'=M, [ free>=1 && free_1>=0 && free>=1 && 0>=0 && 1>=free && 1>=free_5 && free_5>=0 && free_1>=1 && 0>=free_5 && 1>=0 && 0>=0 ], cost: 3+2*free_1 190: f0 -> [14] : C'=free, D'=0, E'=0, F'=1, G'=0, H'=1, J'=0, K'=0, L'=M, [ free>=1 && free_1>=0 && free>=1 && 0>=0 && free>=2 && 1>=free_6 && free_6>=0 && free_1>=1 && 0>=free_6 && 1>=0 && 0>=0 ], cost: 3+2*free_1 191: f0 -> [15] : C'=free, D'=0, E'=0, F'=1, G'=0, H'=1, J'=0, K'=1, L'=M, [ free>=1 && free_1>=0 && free>=1 && 0>=0 && 1>=free && 1>=free_5 && free_5>=0 && free_1>=1 && 0>=free_5 && 1>=0 && 0>=0 ], cost: 3+2*free_1 192: f0 -> [15] : C'=free, D'=0, E'=0, F'=1, G'=0, H'=1, J'=0, K'=0, L'=M, [ free>=1 && free_1>=0 && free>=1 && 0>=0 && free>=2 && 1>=free_6 && free_6>=0 && free_1>=1 && 0>=free_6 && 1>=0 && 0>=0 ], cost: 3+2*free_1 193: f0 -> [16] : C'=free, D'=0, E'=0, F'=1, G'=0, H'=1, J'=0, K'=1, L'=M, [ free>=1 && free_1>=0 && free>=1 && 0>=0 && 1>=free && 1>=free_5 && free_5>=0 && free_1>=1 && 0>=free_5 && 1>=0 && 0>=0 ], cost: 3+2*free_1 194: f0 -> [16] : C'=free, D'=0, E'=0, F'=1, G'=0, H'=1, J'=0, K'=0, L'=M, [ free>=1 && free_1>=0 && free>=1 && 0>=0 && free>=2 && 1>=free_6 && free_6>=0 && free_1>=1 && 0>=free_6 && 1>=0 && 0>=0 ], cost: 3+2*free_1 195: f0 -> [17] : C'=free, D'=0, E'=0, F'=1, G'=0, H'=1, J'=0, K'=1, L'=M, [ free>=1 && free_1>=0 && free>=1 && 0>=0 && 1>=free && 1>=free_5 && free_5>=0 && free_1>=1 && 0>=free_5 && 1>=0 && 0>=0 ], cost: 3+2*free_1 196: f0 -> [17] : C'=free, D'=0, E'=0, F'=1, G'=0, H'=1, J'=0, K'=0, L'=M, [ free>=1 && free_1>=0 && free>=1 && 0>=0 && free>=2 && 1>=free_6 && free_6>=0 && free_1>=1 && 0>=free_6 && 1>=0 && 0>=0 ], cost: 3+2*free_1 197: f0 -> [18] : C'=free, D'=0, E'=0, F'=1, G'=0, H'=1, J'=0, K'=1, L'=M, [ free>=1 && free_1>=0 && free>=1 && 0>=0 && 1>=free && 1>=free_5 && free_5>=0 && free_1>=1 && 0>=free_5 && 1>=0 && 0>=0 ], cost: 3+2*free_1 198: f0 -> [18] : C'=free, D'=0, E'=0, F'=1, G'=0, H'=1, J'=0, K'=0, L'=M, [ free>=1 && free_1>=0 && free>=1 && 0>=0 && free>=2 && 1>=free_6 && free_6>=0 && free_1>=1 && 0>=free_6 && 1>=0 && 0>=0 ], cost: 3+2*free_1 Computing complexity for remaining 10 transitions. The final runtime is determined by this resulting transition: Final Guard: Final Cost: 1 Obtained the following complexity w.r.t. the length of the input n: Complexity class: const Complexity value: 0 WORST_CASE(Omega(1),?)