Trying to load file: main.koat Initial Control flow graph problem: Start location: f0 0: f90 -> f93 : [ 1>=A ], cost: 1 1: f90 -> f93 : [ A>=3 ], cost: 1 20: f90 -> f113 : A'=2, T'=0, U'=0, V'=16, W'=32, X'=48, [ A==2 ], cost: 1 2: f93 -> f96 : [ 8>=A ], cost: 1 3: f93 -> f96 : [ A>=10 ], cost: 1 21: f93 -> f113 : A'=9, T'=0, U'=0, V'=16, W'=32, X'=48, [ A==9 ], cost: 1 16: f96 -> f100 : S'=1, [ 15>=A ], cost: 1 17: f96 -> f100 : S'=1, [ A>=17 ], cost: 1 22: f96 -> f113 : A'=16, T'=0, U'=0, V'=16, W'=32, X'=48, [ A==16 ], cost: 1 4: f0 -> f34 : B'=0, C'=free, D'=free_2, E'=free_3, F'=free_1, G'=free_2, [ B==0 ], cost: 1 5: f0 -> f29 : B'=0, C'=free_4, D'=free_6, E'=free_7, F'=free_5, G'=free_6, H'=1, Q'=2, [ 0>=1+B ], cost: 1 6: f0 -> f29 : B'=0, C'=free_8, D'=free_10, E'=free_11, F'=free_9, G'=free_10, H'=1, Q'=2, [ B>=1 ], cost: 1 8: f34 -> f41 : Q'=28, J'=56, [ 0>=1+free_13 ], cost: 1 9: f34 -> f41 : Q'=28, J'=56, [], cost: 1 31: f34 -> f182 : Q'=32, J'=64, [], cost: 1 80: f29 -> f34 : [ Q>=33 ], cost: 1 7: f29 -> f29 : H'=free_12, Q'=1+Q, [ 32>=Q ], cost: 1 10: f41 -> f59 : K'=F, L'=free_14, M'=32, N'=1, O'=1, [ 32>=free_14 && Q>=1 ], cost: 1 11: f41 -> f59 : K'=F, L'=free_15, M'=32, N'=0, O'=0, [ 32>=free_15 && Q>=1 ], cost: 1 12: f41 -> f59 : K'=F, L'=free_16, M'=32, O'=1, P'=1, [ free_16>=33 && Q>=1 ], cost: 1 13: f41 -> f59 : K'=F, L'=free_17, M'=32, O'=0, P'=0, [ free_17>=33 && Q>=1 ], cost: 1 79: f41 -> f81 : Q_1'=1, [ 0>=Q ], cost: 1 75: f59 -> f41 : Q'=-1+Q, J'=-1+J, U3'=O, V3'=F, W3'=free_108, X3'=32, Y3'=1, Z3'=1, A4'=1, [ 32>=free_108 ], cost: 1 76: f59 -> f41 : Q'=-1+Q, J'=-1+J, U3'=O, V3'=F, W3'=free_109, X3'=32, Y3'=0, Z3'=0, A4'=0, [ 32>=free_109 ], cost: 1 77: f59 -> f41 : Q'=-1+Q, J'=-1+J, U3'=O, V3'=F, W3'=free_110, X3'=32, Z3'=1, A4'=1, B4'=1, [ free_110>=33 ], cost: 1 78: f59 -> f41 : Q'=-1+Q, J'=-1+J, U3'=O, V3'=F, W3'=free_111, X3'=32, Z3'=0, A4'=0, B4'=0, [ free_111>=33 ], cost: 1 14: f81 -> f90 : A'=Q_1, R'=free_18, [ 0>=Q_1 && 16>=Q_1 ], cost: 1 15: f81 -> f90 : A'=Q_1, R'=free_19, [ 16>=Q_1 && Q_1>=2 ], cost: 1 19: f81 -> f113 : A'=1, Q_1'=1, R'=free_20, T'=0, U'=0, V'=16, W'=32, X'=48, [ Q_1==1 ], cost: 1 74: f81 -> f182 : Q'=32, J'=64, [ Q_1>=17 ], cost: 1 18: f100 -> f100 : S'=1+S, [ 2>=S ], cost: 1 73: f100 -> f113 : T'=0, U'=0, V'=16, W'=32, X'=48, [ S>=3 ], cost: 1 72: f113 -> f81 : Q_1'=1+Q_1, [ 0>=V ], cost: 1 23: f113 -> f132 : Y'=free_21, Z'=free_22, A1'=free_23, B1'=28, C1'=1, D1'=1, [ 28>=free_23 && V>=1 ], cost: 1 24: f113 -> f132 : Y'=free_24, Z'=free_25, A1'=free_26, B1'=28, C1'=0, D1'=0, [ 28>=free_26 && V>=1 ], cost: 1 25: f113 -> f132 : Y'=free_27, Z'=free_28, A1'=free_29, B1'=28, D1'=1, E1'=1, [ free_29>=29 && V>=1 ], cost: 1 26: f113 -> f132 : Y'=free_30, Z'=free_31, A1'=free_32, B1'=28, D1'=0, E1'=0, [ free_32>=29 && V>=1 ], cost: 1 27: f132 -> f150 : F1'=D1, G1'=free_33, H1'=free_34, Q1'=free_35, J1'=28, K1'=1, L1'=1, [ 28>=free_35 ], cost: 1 28: f132 -> f150 : F1'=D1, G1'=free_36, H1'=free_37, Q1'=free_38, J1'=28, K1'=0, L1'=0, [ 28>=free_38 ], cost: 1 29: f132 -> f150 : F1'=D1, G1'=free_39, H1'=free_40, Q1'=free_41, J1'=28, L1'=1, M1'=1, [ free_41>=29 ], cost: 1 30: f132 -> f150 : F1'=D1, G1'=free_42, H1'=free_43, Q1'=free_44, J1'=28, L1'=0, M1'=0, [ free_44>=29 ], cost: 1 68: f150 -> f113 : V'=-1+V, W'=-1+W, X'=-1+X, L3'=L1, M3'=free_96, N3'=free_97, O3'=free_98, P3'=28, Q3_1'=1, R3'=1, S3'=1, [ 28>=free_98 ], cost: 1 69: f150 -> f113 : V'=-1+V, W'=-1+W, X'=-1+X, L3'=L1, M3'=free_99, N3'=free_100, O3'=free_101, P3'=28, Q3_1'=0, R3'=0, S3'=0, [ 28>=free_101 ], cost: 1 70: f150 -> f113 : V'=-1+V, W'=-1+W, X'=-1+X, L3'=L1, M3'=free_102, N3'=free_103, O3'=free_104, P3'=28, R3'=1, S3'=1, T3'=1, [ free_104>=29 ], cost: 1 71: f150 -> f113 : V'=-1+V, W'=-1+W, X'=-1+X, L3'=L1, M3'=free_105, N3'=free_106, O3'=free_107, P3'=28, R3'=0, S3'=0, T3'=0, [ free_107>=29 ], cost: 1 32: f182 -> f200 : N1'=E, O1'=free_45, P1'=32, Q1_1'=1, R1'=1, [ 32>=free_45 && Q>=1 ], cost: 1 33: f182 -> f200 : N1'=E, O1'=free_46, P1'=32, Q1_1'=0, R1'=0, [ 32>=free_46 && Q>=1 ], cost: 1 34: f182 -> f200 : N1'=E, O1'=free_47, P1'=32, R1'=1, S1'=1, [ free_47>=33 && Q>=1 ], cost: 1 35: f182 -> f200 : N1'=E, O1'=free_48, P1'=32, R1'=0, S1'=0, [ free_48>=33 && Q>=1 ], cost: 1 67: f182 -> f222 : Q_1'=1, [ 0>=Q ], cost: 1 63: f200 -> f182 : Q'=-1+Q, J'=-1+J, D3'=R1, E3'=E, F3'=free_92, G3'=32, H3'=1, Q3'=1, J3'=1, [ 32>=free_92 ], cost: 1 64: f200 -> f182 : Q'=-1+Q, J'=-1+J, D3'=R1, E3'=E, F3'=free_93, G3'=32, H3'=0, Q3'=0, J3'=0, [ 32>=free_93 ], cost: 1 65: f200 -> f182 : Q'=-1+Q, J'=-1+J, D3'=R1, E3'=E, F3'=free_94, G3'=32, Q3'=1, J3'=1, K3'=1, [ free_94>=33 ], cost: 1 66: f200 -> f182 : Q'=-1+Q, J'=-1+J, D3'=R1, E3'=E, F3'=free_95, G3'=32, Q3'=0, J3'=0, K3'=0, [ free_95>=33 ], cost: 1 36: f222 -> f237 : G'=1, T1'=17-Q_1, U1'=free_49, V1'=free_50, W1'=16, X1'=32, Y1'=48, [ 16>=Q_1 && G==1 ], cost: 1 37: f222 -> f237 : T1'=Q_1, U1'=free_51, V1'=free_52, W1'=16, X1'=32, Y1'=48, [ 16>=Q_1 && 0>=G ], cost: 1 38: f222 -> f237 : T1'=Q_1, U1'=free_53, V1'=free_54, W1'=16, X1'=32, Y1'=48, [ 16>=Q_1 && G>=2 ], cost: 1 62: f222 -> f314 : Q'=32, J'=64, B3'=free_91, C3'=0, [ Q_1>=17 ], cost: 1 39: f237 -> f245 : Z1'=1, [ W1>=1 ], cost: 1 40: f237 -> f245 : Z1'=0, [ W1>=1 ], cost: 1 61: f237 -> f265 : W1'=1, Y1'=5, C2'=free_89, D2'=free_90, [ 0>=W1 ], cost: 1 41: f245 -> f250 : A2'=1, [], cost: 1 42: f245 -> f250 : A2'=0, [], cost: 1 43: f250 -> f237 : W1'=-1+W1, X1'=-1+X1, Y1'=-1+Y1, B2'=1, [], cost: 1 44: f250 -> f237 : W1'=-1+W1, X1'=-1+X1, Y1'=-1+Y1, B2'=0, [], cost: 1 45: f265 -> f265 : W1'=1+W1, Y1'=1+Y1, C2'=free_55, D2'=free_56, [ 4>=W1 ], cost: 1 60: f265 -> f276 : E2'=8, F2'=0, [ W1>=5 ], cost: 1 46: f276 -> f276 : W1'=free_57, E2'=-1+E2, F2'=free_59, G2'=free_61, H2'=free_58, Q2'=free_60, [ E2>=1 ], cost: 1 59: f276 -> f289 : W1'=32, [ 0>=E2 ], cost: 1 58: f289 -> f222 : Q_1'=1+Q_1, B3'=free_88, [ 0>=W1 ], cost: 1 47: f289 -> f289 : W1'=-1+W1, J2'=free_62, K2'=1, [ W1>=1 ], cost: 1 48: f289 -> f289 : W1'=-1+W1, J2'=free_63, K2'=0, [ W1>=1 ], cost: 1 49: f314 -> f333 : L2'=free_64, M2'=free_65, N2'=free_66, O2'=32, P2'=1, Q2_1'=1, [ 32>=free_66 && Q>=1 ], cost: 1 50: f314 -> f333 : L2'=free_67, M2'=free_68, N2'=free_69, O2'=32, P2'=0, Q2_1'=0, [ 32>=free_69 && Q>=1 ], cost: 1 51: f314 -> f333 : L2'=free_70, M2'=free_71, N2'=free_72, O2'=32, Q2_1'=1, R2'=1, [ free_72>=33 && Q>=1 ], cost: 1 52: f314 -> f333 : L2'=free_73, M2'=free_74, N2'=free_75, O2'=32, Q2_1'=0, R2'=0, [ free_75>=33 && Q>=1 ], cost: 1 57: f314 -> f358 : [ 0>=Q ], cost: 1 53: f333 -> f314 : Q'=-1+Q, J'=-1+J, S2'=Q2_1, T2'=free_76, U2'=free_77, V2'=free_78, W2'=32, X2'=1, Y2'=1, Z2'=1, [ 32>=free_78 ], cost: 1 54: f333 -> f314 : Q'=-1+Q, J'=-1+J, S2'=Q2_1, T2'=free_79, U2'=free_80, V2'=free_81, W2'=32, X2'=0, Y2'=0, Z2'=0, [ 32>=free_81 ], cost: 1 55: f333 -> f314 : Q'=-1+Q, J'=-1+J, S2'=Q2_1, T2'=free_82, U2'=free_83, V2'=free_84, W2'=32, Y2'=1, Z2'=1, A3'=1, [ free_84>=33 ], cost: 1 56: f333 -> f314 : Q'=-1+Q, J'=-1+J, S2'=Q2_1, T2'=free_85, U2'=free_86, V2'=free_87, W2'=32, Y2'=0, Z2'=0, A3'=0, [ free_87>=33 ], cost: 1 Removing duplicate transition: 8. Simplified the transitions: Start location: f0 0: f90 -> f93 : [ 1>=A ], cost: 1 1: f90 -> f93 : [ A>=3 ], cost: 1 20: f90 -> f113 : A'=2, T'=0, U'=0, V'=16, W'=32, X'=48, [ A==2 ], cost: 1 2: f93 -> f96 : [ 8>=A ], cost: 1 3: f93 -> f96 : [ A>=10 ], cost: 1 21: f93 -> f113 : A'=9, T'=0, U'=0, V'=16, W'=32, X'=48, [ A==9 ], cost: 1 16: f96 -> f100 : S'=1, [ 15>=A ], cost: 1 17: f96 -> f100 : S'=1, [ A>=17 ], cost: 1 22: f96 -> f113 : A'=16, T'=0, U'=0, V'=16, W'=32, X'=48, [ A==16 ], cost: 1 4: f0 -> f34 : B'=0, C'=free, D'=free_2, E'=free_3, F'=free_1, G'=free_2, [ B==0 ], cost: 1 5: f0 -> f29 : B'=0, C'=free_4, D'=free_6, E'=free_7, F'=free_5, G'=free_6, H'=1, Q'=2, [ 0>=1+B ], cost: 1 6: f0 -> f29 : B'=0, C'=free_8, D'=free_10, E'=free_11, F'=free_9, G'=free_10, H'=1, Q'=2, [ B>=1 ], cost: 1 9: f34 -> f41 : Q'=28, J'=56, [], cost: 1 31: f34 -> f182 : Q'=32, J'=64, [], cost: 1 80: f29 -> f34 : [ Q>=33 ], cost: 1 7: f29 -> f29 : H'=free_12, Q'=1+Q, [ 32>=Q ], cost: 1 10: f41 -> f59 : K'=F, L'=free_14, M'=32, N'=1, O'=1, [ 32>=free_14 && Q>=1 ], cost: 1 11: f41 -> f59 : K'=F, L'=free_15, M'=32, N'=0, O'=0, [ 32>=free_15 && Q>=1 ], cost: 1 12: f41 -> f59 : K'=F, L'=free_16, M'=32, O'=1, P'=1, [ free_16>=33 && Q>=1 ], cost: 1 13: f41 -> f59 : K'=F, L'=free_17, M'=32, O'=0, P'=0, [ free_17>=33 && Q>=1 ], cost: 1 79: f41 -> f81 : Q_1'=1, [ 0>=Q ], cost: 1 75: f59 -> f41 : Q'=-1+Q, J'=-1+J, U3'=O, V3'=F, W3'=free_108, X3'=32, Y3'=1, Z3'=1, A4'=1, [ 32>=free_108 ], cost: 1 76: f59 -> f41 : Q'=-1+Q, J'=-1+J, U3'=O, V3'=F, W3'=free_109, X3'=32, Y3'=0, Z3'=0, A4'=0, [ 32>=free_109 ], cost: 1 77: f59 -> f41 : Q'=-1+Q, J'=-1+J, U3'=O, V3'=F, W3'=free_110, X3'=32, Z3'=1, A4'=1, B4'=1, [ free_110>=33 ], cost: 1 78: f59 -> f41 : Q'=-1+Q, J'=-1+J, U3'=O, V3'=F, W3'=free_111, X3'=32, Z3'=0, A4'=0, B4'=0, [ free_111>=33 ], cost: 1 14: f81 -> f90 : A'=Q_1, R'=free_18, [ 0>=Q_1 ], cost: 1 15: f81 -> f90 : A'=Q_1, R'=free_19, [ 16>=Q_1 && Q_1>=2 ], cost: 1 19: f81 -> f113 : A'=1, Q_1'=1, R'=free_20, T'=0, U'=0, V'=16, W'=32, X'=48, [ Q_1==1 ], cost: 1 74: f81 -> f182 : Q'=32, J'=64, [ Q_1>=17 ], cost: 1 18: f100 -> f100 : S'=1+S, [ 2>=S ], cost: 1 73: f100 -> f113 : T'=0, U'=0, V'=16, W'=32, X'=48, [ S>=3 ], cost: 1 72: f113 -> f81 : Q_1'=1+Q_1, [ 0>=V ], cost: 1 23: f113 -> f132 : Y'=free_21, Z'=free_22, A1'=free_23, B1'=28, C1'=1, D1'=1, [ 28>=free_23 && V>=1 ], cost: 1 24: f113 -> f132 : Y'=free_24, Z'=free_25, A1'=free_26, B1'=28, C1'=0, D1'=0, [ 28>=free_26 && V>=1 ], cost: 1 25: f113 -> f132 : Y'=free_27, Z'=free_28, A1'=free_29, B1'=28, D1'=1, E1'=1, [ free_29>=29 && V>=1 ], cost: 1 26: f113 -> f132 : Y'=free_30, Z'=free_31, A1'=free_32, B1'=28, D1'=0, E1'=0, [ free_32>=29 && V>=1 ], cost: 1 27: f132 -> f150 : F1'=D1, G1'=free_33, H1'=free_34, Q1'=free_35, J1'=28, K1'=1, L1'=1, [ 28>=free_35 ], cost: 1 28: f132 -> f150 : F1'=D1, G1'=free_36, H1'=free_37, Q1'=free_38, J1'=28, K1'=0, L1'=0, [ 28>=free_38 ], cost: 1 29: f132 -> f150 : F1'=D1, G1'=free_39, H1'=free_40, Q1'=free_41, J1'=28, L1'=1, M1'=1, [ free_41>=29 ], cost: 1 30: f132 -> f150 : F1'=D1, G1'=free_42, H1'=free_43, Q1'=free_44, J1'=28, L1'=0, M1'=0, [ free_44>=29 ], cost: 1 68: f150 -> f113 : V'=-1+V, W'=-1+W, X'=-1+X, L3'=L1, M3'=free_96, N3'=free_97, O3'=free_98, P3'=28, Q3_1'=1, R3'=1, S3'=1, [ 28>=free_98 ], cost: 1 69: f150 -> f113 : V'=-1+V, W'=-1+W, X'=-1+X, L3'=L1, M3'=free_99, N3'=free_100, O3'=free_101, P3'=28, Q3_1'=0, R3'=0, S3'=0, [ 28>=free_101 ], cost: 1 70: f150 -> f113 : V'=-1+V, W'=-1+W, X'=-1+X, L3'=L1, M3'=free_102, N3'=free_103, O3'=free_104, P3'=28, R3'=1, S3'=1, T3'=1, [ free_104>=29 ], cost: 1 71: f150 -> f113 : V'=-1+V, W'=-1+W, X'=-1+X, L3'=L1, M3'=free_105, N3'=free_106, O3'=free_107, P3'=28, R3'=0, S3'=0, T3'=0, [ free_107>=29 ], cost: 1 32: f182 -> f200 : N1'=E, O1'=free_45, P1'=32, Q1_1'=1, R1'=1, [ 32>=free_45 && Q>=1 ], cost: 1 33: f182 -> f200 : N1'=E, O1'=free_46, P1'=32, Q1_1'=0, R1'=0, [ 32>=free_46 && Q>=1 ], cost: 1 34: f182 -> f200 : N1'=E, O1'=free_47, P1'=32, R1'=1, S1'=1, [ free_47>=33 && Q>=1 ], cost: 1 35: f182 -> f200 : N1'=E, O1'=free_48, P1'=32, R1'=0, S1'=0, [ free_48>=33 && Q>=1 ], cost: 1 67: f182 -> f222 : Q_1'=1, [ 0>=Q ], cost: 1 63: f200 -> f182 : Q'=-1+Q, J'=-1+J, D3'=R1, E3'=E, F3'=free_92, G3'=32, H3'=1, Q3'=1, J3'=1, [ 32>=free_92 ], cost: 1 64: f200 -> f182 : Q'=-1+Q, J'=-1+J, D3'=R1, E3'=E, F3'=free_93, G3'=32, H3'=0, Q3'=0, J3'=0, [ 32>=free_93 ], cost: 1 65: f200 -> f182 : Q'=-1+Q, J'=-1+J, D3'=R1, E3'=E, F3'=free_94, G3'=32, Q3'=1, J3'=1, K3'=1, [ free_94>=33 ], cost: 1 66: f200 -> f182 : Q'=-1+Q, J'=-1+J, D3'=R1, E3'=E, F3'=free_95, G3'=32, Q3'=0, J3'=0, K3'=0, [ free_95>=33 ], cost: 1 36: f222 -> f237 : G'=1, T1'=17-Q_1, U1'=free_49, V1'=free_50, W1'=16, X1'=32, Y1'=48, [ 16>=Q_1 && G==1 ], cost: 1 37: f222 -> f237 : T1'=Q_1, U1'=free_51, V1'=free_52, W1'=16, X1'=32, Y1'=48, [ 16>=Q_1 && 0>=G ], cost: 1 38: f222 -> f237 : T1'=Q_1, U1'=free_53, V1'=free_54, W1'=16, X1'=32, Y1'=48, [ 16>=Q_1 && G>=2 ], cost: 1 62: f222 -> f314 : Q'=32, J'=64, B3'=free_91, C3'=0, [ Q_1>=17 ], cost: 1 39: f237 -> f245 : Z1'=1, [ W1>=1 ], cost: 1 40: f237 -> f245 : Z1'=0, [ W1>=1 ], cost: 1 61: f237 -> f265 : W1'=1, Y1'=5, C2'=free_89, D2'=free_90, [ 0>=W1 ], cost: 1 41: f245 -> f250 : A2'=1, [], cost: 1 42: f245 -> f250 : A2'=0, [], cost: 1 43: f250 -> f237 : W1'=-1+W1, X1'=-1+X1, Y1'=-1+Y1, B2'=1, [], cost: 1 44: f250 -> f237 : W1'=-1+W1, X1'=-1+X1, Y1'=-1+Y1, B2'=0, [], cost: 1 45: f265 -> f265 : W1'=1+W1, Y1'=1+Y1, C2'=free_55, D2'=free_56, [ 4>=W1 ], cost: 1 60: f265 -> f276 : E2'=8, F2'=0, [ W1>=5 ], cost: 1 46: f276 -> f276 : W1'=free_57, E2'=-1+E2, F2'=free_59, G2'=free_61, H2'=free_58, Q2'=free_60, [ E2>=1 ], cost: 1 59: f276 -> f289 : W1'=32, [ 0>=E2 ], cost: 1 58: f289 -> f222 : Q_1'=1+Q_1, B3'=free_88, [ 0>=W1 ], cost: 1 47: f289 -> f289 : W1'=-1+W1, J2'=free_62, K2'=1, [ W1>=1 ], cost: 1 48: f289 -> f289 : W1'=-1+W1, J2'=free_63, K2'=0, [ W1>=1 ], cost: 1 49: f314 -> f333 : L2'=free_64, M2'=free_65, N2'=free_66, O2'=32, P2'=1, Q2_1'=1, [ 32>=free_66 && Q>=1 ], cost: 1 50: f314 -> f333 : L2'=free_67, M2'=free_68, N2'=free_69, O2'=32, P2'=0, Q2_1'=0, [ 32>=free_69 && Q>=1 ], cost: 1 51: f314 -> f333 : L2'=free_70, M2'=free_71, N2'=free_72, O2'=32, Q2_1'=1, R2'=1, [ free_72>=33 && Q>=1 ], cost: 1 52: f314 -> f333 : L2'=free_73, M2'=free_74, N2'=free_75, O2'=32, Q2_1'=0, R2'=0, [ free_75>=33 && Q>=1 ], cost: 1 53: f333 -> f314 : Q'=-1+Q, J'=-1+J, S2'=Q2_1, T2'=free_76, U2'=free_77, V2'=free_78, W2'=32, X2'=1, Y2'=1, Z2'=1, [ 32>=free_78 ], cost: 1 54: f333 -> f314 : Q'=-1+Q, J'=-1+J, S2'=Q2_1, T2'=free_79, U2'=free_80, V2'=free_81, W2'=32, X2'=0, Y2'=0, Z2'=0, [ 32>=free_81 ], cost: 1 55: f333 -> f314 : Q'=-1+Q, J'=-1+J, S2'=Q2_1, T2'=free_82, U2'=free_83, V2'=free_84, W2'=32, Y2'=1, Z2'=1, A3'=1, [ free_84>=33 ], cost: 1 56: f333 -> f314 : Q'=-1+Q, J'=-1+J, S2'=Q2_1, T2'=free_85, U2'=free_86, V2'=free_87, W2'=32, Y2'=0, Z2'=0, A3'=0, [ free_87>=33 ], cost: 1 Eliminating 1 self-loops for location f29 Self-Loop 7 has the metering function: 33-Q, resulting in the new transition 81. Removing the self-loops: 7. Eliminating 1 self-loops for location f100 Self-Loop 18 has the metering function: 3-S, resulting in the new transition 82. Removing the self-loops: 18. Eliminating 1 self-loops for location f265 Self-Loop 45 has the metering function: 5-W1, resulting in the new transition 83. Removing the self-loops: 45. Eliminating 1 self-loops for location f276 Self-Loop 46 has the metering function: E2, resulting in the new transition 84. Removing the self-loops: 46. Eliminating 2 self-loops for location f289 Self-Loop 47 has the metering function: W1, resulting in the new transition 85. Self-Loop 48 has the metering function: W1, resulting in the new transition 86. Removing the self-loops: 47 48. Removed all Self-loops using metering functions (where possible): Start location: f0 0: f90 -> f93 : [ 1>=A ], cost: 1 1: f90 -> f93 : [ A>=3 ], cost: 1 20: f90 -> f113 : A'=2, T'=0, U'=0, V'=16, W'=32, X'=48, [ A==2 ], cost: 1 2: f93 -> f96 : [ 8>=A ], cost: 1 3: f93 -> f96 : [ A>=10 ], cost: 1 21: f93 -> f113 : A'=9, T'=0, U'=0, V'=16, W'=32, X'=48, [ A==9 ], cost: 1 16: f96 -> f100 : S'=1, [ 15>=A ], cost: 1 17: f96 -> f100 : S'=1, [ A>=17 ], cost: 1 22: f96 -> f113 : A'=16, T'=0, U'=0, V'=16, W'=32, X'=48, [ A==16 ], cost: 1 4: f0 -> f34 : B'=0, C'=free, D'=free_2, E'=free_3, F'=free_1, G'=free_2, [ B==0 ], cost: 1 5: f0 -> f29 : B'=0, C'=free_4, D'=free_6, E'=free_7, F'=free_5, G'=free_6, H'=1, Q'=2, [ 0>=1+B ], cost: 1 6: f0 -> f29 : B'=0, C'=free_8, D'=free_10, E'=free_11, F'=free_9, G'=free_10, H'=1, Q'=2, [ B>=1 ], cost: 1 9: f34 -> f41 : Q'=28, J'=56, [], cost: 1 31: f34 -> f182 : Q'=32, J'=64, [], cost: 1 81: f29 -> [25] : H'=free_12, Q'=33, [ 32>=Q ], cost: 33-Q 10: f41 -> f59 : K'=F, L'=free_14, M'=32, N'=1, O'=1, [ 32>=free_14 && Q>=1 ], cost: 1 11: f41 -> f59 : K'=F, L'=free_15, M'=32, N'=0, O'=0, [ 32>=free_15 && Q>=1 ], cost: 1 12: f41 -> f59 : K'=F, L'=free_16, M'=32, O'=1, P'=1, [ free_16>=33 && Q>=1 ], cost: 1 13: f41 -> f59 : K'=F, L'=free_17, M'=32, O'=0, P'=0, [ free_17>=33 && Q>=1 ], cost: 1 79: f41 -> f81 : Q_1'=1, [ 0>=Q ], cost: 1 75: f59 -> f41 : Q'=-1+Q, J'=-1+J, U3'=O, V3'=F, W3'=free_108, X3'=32, Y3'=1, Z3'=1, A4'=1, [ 32>=free_108 ], cost: 1 76: f59 -> f41 : Q'=-1+Q, J'=-1+J, U3'=O, V3'=F, W3'=free_109, X3'=32, Y3'=0, Z3'=0, A4'=0, [ 32>=free_109 ], cost: 1 77: f59 -> f41 : Q'=-1+Q, J'=-1+J, U3'=O, V3'=F, W3'=free_110, X3'=32, Z3'=1, A4'=1, B4'=1, [ free_110>=33 ], cost: 1 78: f59 -> f41 : Q'=-1+Q, J'=-1+J, U3'=O, V3'=F, W3'=free_111, X3'=32, Z3'=0, A4'=0, B4'=0, [ free_111>=33 ], cost: 1 14: f81 -> f90 : A'=Q_1, R'=free_18, [ 0>=Q_1 ], cost: 1 15: f81 -> f90 : A'=Q_1, R'=free_19, [ 16>=Q_1 && Q_1>=2 ], cost: 1 19: f81 -> f113 : A'=1, Q_1'=1, R'=free_20, T'=0, U'=0, V'=16, W'=32, X'=48, [ Q_1==1 ], cost: 1 74: f81 -> f182 : Q'=32, J'=64, [ Q_1>=17 ], cost: 1 82: f100 -> [26] : S'=3, [ 2>=S ], cost: 3-S 72: f113 -> f81 : Q_1'=1+Q_1, [ 0>=V ], cost: 1 23: f113 -> f132 : Y'=free_21, Z'=free_22, A1'=free_23, B1'=28, C1'=1, D1'=1, [ 28>=free_23 && V>=1 ], cost: 1 24: f113 -> f132 : Y'=free_24, Z'=free_25, A1'=free_26, B1'=28, C1'=0, D1'=0, [ 28>=free_26 && V>=1 ], cost: 1 25: f113 -> f132 : Y'=free_27, Z'=free_28, A1'=free_29, B1'=28, D1'=1, E1'=1, [ free_29>=29 && V>=1 ], cost: 1 26: f113 -> f132 : Y'=free_30, Z'=free_31, A1'=free_32, B1'=28, D1'=0, E1'=0, [ free_32>=29 && V>=1 ], cost: 1 27: f132 -> f150 : F1'=D1, G1'=free_33, H1'=free_34, Q1'=free_35, J1'=28, K1'=1, L1'=1, [ 28>=free_35 ], cost: 1 28: f132 -> f150 : F1'=D1, G1'=free_36, H1'=free_37, Q1'=free_38, J1'=28, K1'=0, L1'=0, [ 28>=free_38 ], cost: 1 29: f132 -> f150 : F1'=D1, G1'=free_39, H1'=free_40, Q1'=free_41, J1'=28, L1'=1, M1'=1, [ free_41>=29 ], cost: 1 30: f132 -> f150 : F1'=D1, G1'=free_42, H1'=free_43, Q1'=free_44, J1'=28, L1'=0, M1'=0, [ free_44>=29 ], cost: 1 68: f150 -> f113 : V'=-1+V, W'=-1+W, X'=-1+X, L3'=L1, M3'=free_96, N3'=free_97, O3'=free_98, P3'=28, Q3_1'=1, R3'=1, S3'=1, [ 28>=free_98 ], cost: 1 69: f150 -> f113 : V'=-1+V, W'=-1+W, X'=-1+X, L3'=L1, M3'=free_99, N3'=free_100, O3'=free_101, P3'=28, Q3_1'=0, R3'=0, S3'=0, [ 28>=free_101 ], cost: 1 70: f150 -> f113 : V'=-1+V, W'=-1+W, X'=-1+X, L3'=L1, M3'=free_102, N3'=free_103, O3'=free_104, P3'=28, R3'=1, S3'=1, T3'=1, [ free_104>=29 ], cost: 1 71: f150 -> f113 : V'=-1+V, W'=-1+W, X'=-1+X, L3'=L1, M3'=free_105, N3'=free_106, O3'=free_107, P3'=28, R3'=0, S3'=0, T3'=0, [ free_107>=29 ], cost: 1 32: f182 -> f200 : N1'=E, O1'=free_45, P1'=32, Q1_1'=1, R1'=1, [ 32>=free_45 && Q>=1 ], cost: 1 33: f182 -> f200 : N1'=E, O1'=free_46, P1'=32, Q1_1'=0, R1'=0, [ 32>=free_46 && Q>=1 ], cost: 1 34: f182 -> f200 : N1'=E, O1'=free_47, P1'=32, R1'=1, S1'=1, [ free_47>=33 && Q>=1 ], cost: 1 35: f182 -> f200 : N1'=E, O1'=free_48, P1'=32, R1'=0, S1'=0, [ free_48>=33 && Q>=1 ], cost: 1 67: f182 -> f222 : Q_1'=1, [ 0>=Q ], cost: 1 63: f200 -> f182 : Q'=-1+Q, J'=-1+J, D3'=R1, E3'=E, F3'=free_92, G3'=32, H3'=1, Q3'=1, J3'=1, [ 32>=free_92 ], cost: 1 64: f200 -> f182 : Q'=-1+Q, J'=-1+J, D3'=R1, E3'=E, F3'=free_93, G3'=32, H3'=0, Q3'=0, J3'=0, [ 32>=free_93 ], cost: 1 65: f200 -> f182 : Q'=-1+Q, J'=-1+J, D3'=R1, E3'=E, F3'=free_94, G3'=32, Q3'=1, J3'=1, K3'=1, [ free_94>=33 ], cost: 1 66: f200 -> f182 : Q'=-1+Q, J'=-1+J, D3'=R1, E3'=E, F3'=free_95, G3'=32, Q3'=0, J3'=0, K3'=0, [ free_95>=33 ], cost: 1 36: f222 -> f237 : G'=1, T1'=17-Q_1, U1'=free_49, V1'=free_50, W1'=16, X1'=32, Y1'=48, [ 16>=Q_1 && G==1 ], cost: 1 37: f222 -> f237 : T1'=Q_1, U1'=free_51, V1'=free_52, W1'=16, X1'=32, Y1'=48, [ 16>=Q_1 && 0>=G ], cost: 1 38: f222 -> f237 : T1'=Q_1, U1'=free_53, V1'=free_54, W1'=16, X1'=32, Y1'=48, [ 16>=Q_1 && G>=2 ], cost: 1 62: f222 -> f314 : Q'=32, J'=64, B3'=free_91, C3'=0, [ Q_1>=17 ], cost: 1 39: f237 -> f245 : Z1'=1, [ W1>=1 ], cost: 1 40: f237 -> f245 : Z1'=0, [ W1>=1 ], cost: 1 61: f237 -> f265 : W1'=1, Y1'=5, C2'=free_89, D2'=free_90, [ 0>=W1 ], cost: 1 41: f245 -> f250 : A2'=1, [], cost: 1 42: f245 -> f250 : A2'=0, [], cost: 1 43: f250 -> f237 : W1'=-1+W1, X1'=-1+X1, Y1'=-1+Y1, B2'=1, [], cost: 1 44: f250 -> f237 : W1'=-1+W1, X1'=-1+X1, Y1'=-1+Y1, B2'=0, [], cost: 1 83: f265 -> [27] : W1'=5, Y1'=5+Y1-W1, C2'=free_55, D2'=free_56, [ 4>=W1 ], cost: 5-W1 84: f276 -> [28] : W1'=free_57, E2'=0, F2'=free_59, G2'=free_61, H2'=free_58, Q2'=free_60, [ E2>=1 ], cost: E2 85: f289 -> [29] : W1'=0, J2'=free_62, K2'=1, [ W1>=1 ], cost: W1 86: f289 -> [29] : W1'=0, J2'=free_63, K2'=0, [ W1>=1 ], cost: W1 49: f314 -> f333 : L2'=free_64, M2'=free_65, N2'=free_66, O2'=32, P2'=1, Q2_1'=1, [ 32>=free_66 && Q>=1 ], cost: 1 50: f314 -> f333 : L2'=free_67, M2'=free_68, N2'=free_69, O2'=32, P2'=0, Q2_1'=0, [ 32>=free_69 && Q>=1 ], cost: 1 51: f314 -> f333 : L2'=free_70, M2'=free_71, N2'=free_72, O2'=32, Q2_1'=1, R2'=1, [ free_72>=33 && Q>=1 ], cost: 1 52: f314 -> f333 : L2'=free_73, M2'=free_74, N2'=free_75, O2'=32, Q2_1'=0, R2'=0, [ free_75>=33 && Q>=1 ], cost: 1 53: f333 -> f314 : Q'=-1+Q, J'=-1+J, S2'=Q2_1, T2'=free_76, U2'=free_77, V2'=free_78, W2'=32, X2'=1, Y2'=1, Z2'=1, [ 32>=free_78 ], cost: 1 54: f333 -> f314 : Q'=-1+Q, J'=-1+J, S2'=Q2_1, T2'=free_79, U2'=free_80, V2'=free_81, W2'=32, X2'=0, Y2'=0, Z2'=0, [ 32>=free_81 ], cost: 1 55: f333 -> f314 : Q'=-1+Q, J'=-1+J, S2'=Q2_1, T2'=free_82, U2'=free_83, V2'=free_84, W2'=32, Y2'=1, Z2'=1, A3'=1, [ free_84>=33 ], cost: 1 56: f333 -> f314 : Q'=-1+Q, J'=-1+J, S2'=Q2_1, T2'=free_85, U2'=free_86, V2'=free_87, W2'=32, Y2'=0, Z2'=0, A3'=0, [ free_87>=33 ], cost: 1 80: [25] -> f34 : [ Q>=33 ], cost: 1 73: [26] -> f113 : T'=0, U'=0, V'=16, W'=32, X'=48, [ S>=3 ], cost: 1 60: [27] -> f276 : E2'=8, F2'=0, [ W1>=5 ], cost: 1 59: [28] -> f289 : W1'=32, [ 0>=E2 ], cost: 1 58: [29] -> f222 : Q_1'=1+Q_1, B3'=free_88, [ 0>=W1 ], cost: 1 Applied simple chaining: Start location: f0 0: f90 -> f93 : [ 1>=A ], cost: 1 1: f90 -> f93 : [ A>=3 ], cost: 1 20: f90 -> f113 : A'=2, T'=0, U'=0, V'=16, W'=32, X'=48, [ A==2 ], cost: 1 2: f93 -> f96 : [ 8>=A ], cost: 1 3: f93 -> f96 : [ A>=10 ], cost: 1 21: f93 -> f113 : A'=9, T'=0, U'=0, V'=16, W'=32, X'=48, [ A==9 ], cost: 1 16: f96 -> f100 : S'=1, [ 15>=A ], cost: 1 17: f96 -> f100 : S'=1, [ A>=17 ], cost: 1 22: f96 -> f113 : A'=16, T'=0, U'=0, V'=16, W'=32, X'=48, [ A==16 ], cost: 1 4: f0 -> f34 : B'=0, C'=free, D'=free_2, E'=free_3, F'=free_1, G'=free_2, [ B==0 ], cost: 1 5: f0 -> f29 : B'=0, C'=free_4, D'=free_6, E'=free_7, F'=free_5, G'=free_6, H'=1, Q'=2, [ 0>=1+B ], cost: 1 6: f0 -> f29 : B'=0, C'=free_8, D'=free_10, E'=free_11, F'=free_9, G'=free_10, H'=1, Q'=2, [ B>=1 ], cost: 1 9: f34 -> f41 : Q'=28, J'=56, [], cost: 1 31: f34 -> f182 : Q'=32, J'=64, [], cost: 1 81: f29 -> f34 : H'=free_12, Q'=33, [ 32>=Q && 33>=33 ], cost: 34-Q 10: f41 -> f59 : K'=F, L'=free_14, M'=32, N'=1, O'=1, [ 32>=free_14 && Q>=1 ], cost: 1 11: f41 -> f59 : K'=F, L'=free_15, M'=32, N'=0, O'=0, [ 32>=free_15 && Q>=1 ], cost: 1 12: f41 -> f59 : K'=F, L'=free_16, M'=32, O'=1, P'=1, [ free_16>=33 && Q>=1 ], cost: 1 13: f41 -> f59 : K'=F, L'=free_17, M'=32, O'=0, P'=0, [ free_17>=33 && Q>=1 ], cost: 1 79: f41 -> f81 : Q_1'=1, [ 0>=Q ], cost: 1 75: f59 -> f41 : Q'=-1+Q, J'=-1+J, U3'=O, V3'=F, W3'=free_108, X3'=32, Y3'=1, Z3'=1, A4'=1, [ 32>=free_108 ], cost: 1 76: f59 -> f41 : Q'=-1+Q, J'=-1+J, U3'=O, V3'=F, W3'=free_109, X3'=32, Y3'=0, Z3'=0, A4'=0, [ 32>=free_109 ], cost: 1 77: f59 -> f41 : Q'=-1+Q, J'=-1+J, U3'=O, V3'=F, W3'=free_110, X3'=32, Z3'=1, A4'=1, B4'=1, [ free_110>=33 ], cost: 1 78: f59 -> f41 : Q'=-1+Q, J'=-1+J, U3'=O, V3'=F, W3'=free_111, X3'=32, Z3'=0, A4'=0, B4'=0, [ free_111>=33 ], cost: 1 14: f81 -> f90 : A'=Q_1, R'=free_18, [ 0>=Q_1 ], cost: 1 15: f81 -> f90 : A'=Q_1, R'=free_19, [ 16>=Q_1 && Q_1>=2 ], cost: 1 19: f81 -> f113 : A'=1, Q_1'=1, R'=free_20, T'=0, U'=0, V'=16, W'=32, X'=48, [ Q_1==1 ], cost: 1 74: f81 -> f182 : Q'=32, J'=64, [ Q_1>=17 ], cost: 1 82: f100 -> f113 : S'=3, T'=0, U'=0, V'=16, W'=32, X'=48, [ 2>=S && 3>=3 ], cost: 4-S 72: f113 -> f81 : Q_1'=1+Q_1, [ 0>=V ], cost: 1 23: f113 -> f132 : Y'=free_21, Z'=free_22, A1'=free_23, B1'=28, C1'=1, D1'=1, [ 28>=free_23 && V>=1 ], cost: 1 24: f113 -> f132 : Y'=free_24, Z'=free_25, A1'=free_26, B1'=28, C1'=0, D1'=0, [ 28>=free_26 && V>=1 ], cost: 1 25: f113 -> f132 : Y'=free_27, Z'=free_28, A1'=free_29, B1'=28, D1'=1, E1'=1, [ free_29>=29 && V>=1 ], cost: 1 26: f113 -> f132 : Y'=free_30, Z'=free_31, A1'=free_32, B1'=28, D1'=0, E1'=0, [ free_32>=29 && V>=1 ], cost: 1 27: f132 -> f150 : F1'=D1, G1'=free_33, H1'=free_34, Q1'=free_35, J1'=28, K1'=1, L1'=1, [ 28>=free_35 ], cost: 1 28: f132 -> f150 : F1'=D1, G1'=free_36, H1'=free_37, Q1'=free_38, J1'=28, K1'=0, L1'=0, [ 28>=free_38 ], cost: 1 29: f132 -> f150 : F1'=D1, G1'=free_39, H1'=free_40, Q1'=free_41, J1'=28, L1'=1, M1'=1, [ free_41>=29 ], cost: 1 30: f132 -> f150 : F1'=D1, G1'=free_42, H1'=free_43, Q1'=free_44, J1'=28, L1'=0, M1'=0, [ free_44>=29 ], cost: 1 68: f150 -> f113 : V'=-1+V, W'=-1+W, X'=-1+X, L3'=L1, M3'=free_96, N3'=free_97, O3'=free_98, P3'=28, Q3_1'=1, R3'=1, S3'=1, [ 28>=free_98 ], cost: 1 69: f150 -> f113 : V'=-1+V, W'=-1+W, X'=-1+X, L3'=L1, M3'=free_99, N3'=free_100, O3'=free_101, P3'=28, Q3_1'=0, R3'=0, S3'=0, [ 28>=free_101 ], cost: 1 70: f150 -> f113 : V'=-1+V, W'=-1+W, X'=-1+X, L3'=L1, M3'=free_102, N3'=free_103, O3'=free_104, P3'=28, R3'=1, S3'=1, T3'=1, [ free_104>=29 ], cost: 1 71: f150 -> f113 : V'=-1+V, W'=-1+W, X'=-1+X, L3'=L1, M3'=free_105, N3'=free_106, O3'=free_107, P3'=28, R3'=0, S3'=0, T3'=0, [ free_107>=29 ], cost: 1 32: f182 -> f200 : N1'=E, O1'=free_45, P1'=32, Q1_1'=1, R1'=1, [ 32>=free_45 && Q>=1 ], cost: 1 33: f182 -> f200 : N1'=E, O1'=free_46, P1'=32, Q1_1'=0, R1'=0, [ 32>=free_46 && Q>=1 ], cost: 1 34: f182 -> f200 : N1'=E, O1'=free_47, P1'=32, R1'=1, S1'=1, [ free_47>=33 && Q>=1 ], cost: 1 35: f182 -> f200 : N1'=E, O1'=free_48, P1'=32, R1'=0, S1'=0, [ free_48>=33 && Q>=1 ], cost: 1 67: f182 -> f222 : Q_1'=1, [ 0>=Q ], cost: 1 63: f200 -> f182 : Q'=-1+Q, J'=-1+J, D3'=R1, E3'=E, F3'=free_92, G3'=32, H3'=1, Q3'=1, J3'=1, [ 32>=free_92 ], cost: 1 64: f200 -> f182 : Q'=-1+Q, J'=-1+J, D3'=R1, E3'=E, F3'=free_93, G3'=32, H3'=0, Q3'=0, J3'=0, [ 32>=free_93 ], cost: 1 65: f200 -> f182 : Q'=-1+Q, J'=-1+J, D3'=R1, E3'=E, F3'=free_94, G3'=32, Q3'=1, J3'=1, K3'=1, [ free_94>=33 ], cost: 1 66: f200 -> f182 : Q'=-1+Q, J'=-1+J, D3'=R1, E3'=E, F3'=free_95, G3'=32, Q3'=0, J3'=0, K3'=0, [ free_95>=33 ], cost: 1 36: f222 -> f237 : G'=1, T1'=17-Q_1, U1'=free_49, V1'=free_50, W1'=16, X1'=32, Y1'=48, [ 16>=Q_1 && G==1 ], cost: 1 37: f222 -> f237 : T1'=Q_1, U1'=free_51, V1'=free_52, W1'=16, X1'=32, Y1'=48, [ 16>=Q_1 && 0>=G ], cost: 1 38: f222 -> f237 : T1'=Q_1, U1'=free_53, V1'=free_54, W1'=16, X1'=32, Y1'=48, [ 16>=Q_1 && G>=2 ], cost: 1 62: f222 -> f314 : Q'=32, J'=64, B3'=free_91, C3'=0, [ Q_1>=17 ], cost: 1 39: f237 -> f245 : Z1'=1, [ W1>=1 ], cost: 1 40: f237 -> f245 : Z1'=0, [ W1>=1 ], cost: 1 61: f237 -> f289 : W1'=32, Y1'=9, C2'=free_55, D2'=free_56, E2'=0, F2'=free_59, G2'=free_61, H2'=free_58, Q2'=free_60, [ 0>=W1 && 4>=1 && 5>=5 && 8>=1 && 0>=0 ], cost: 15 41: f245 -> f250 : A2'=1, [], cost: 1 42: f245 -> f250 : A2'=0, [], cost: 1 43: f250 -> f237 : W1'=-1+W1, X1'=-1+X1, Y1'=-1+Y1, B2'=1, [], cost: 1 44: f250 -> f237 : W1'=-1+W1, X1'=-1+X1, Y1'=-1+Y1, B2'=0, [], cost: 1 85: f289 -> [29] : W1'=0, J2'=free_62, K2'=1, [ W1>=1 ], cost: W1 86: f289 -> [29] : W1'=0, J2'=free_63, K2'=0, [ W1>=1 ], cost: W1 49: f314 -> f333 : L2'=free_64, M2'=free_65, N2'=free_66, O2'=32, P2'=1, Q2_1'=1, [ 32>=free_66 && Q>=1 ], cost: 1 50: f314 -> f333 : L2'=free_67, M2'=free_68, N2'=free_69, O2'=32, P2'=0, Q2_1'=0, [ 32>=free_69 && Q>=1 ], cost: 1 51: f314 -> f333 : L2'=free_70, M2'=free_71, N2'=free_72, O2'=32, Q2_1'=1, R2'=1, [ free_72>=33 && Q>=1 ], cost: 1 52: f314 -> f333 : L2'=free_73, M2'=free_74, N2'=free_75, O2'=32, Q2_1'=0, R2'=0, [ free_75>=33 && Q>=1 ], cost: 1 53: f333 -> f314 : Q'=-1+Q, J'=-1+J, S2'=Q2_1, T2'=free_76, U2'=free_77, V2'=free_78, W2'=32, X2'=1, Y2'=1, Z2'=1, [ 32>=free_78 ], cost: 1 54: f333 -> f314 : Q'=-1+Q, J'=-1+J, S2'=Q2_1, T2'=free_79, U2'=free_80, V2'=free_81, W2'=32, X2'=0, Y2'=0, Z2'=0, [ 32>=free_81 ], cost: 1 55: f333 -> f314 : Q'=-1+Q, J'=-1+J, S2'=Q2_1, T2'=free_82, U2'=free_83, V2'=free_84, W2'=32, Y2'=1, Z2'=1, A3'=1, [ free_84>=33 ], cost: 1 56: f333 -> f314 : Q'=-1+Q, J'=-1+J, S2'=Q2_1, T2'=free_85, U2'=free_86, V2'=free_87, W2'=32, Y2'=0, Z2'=0, A3'=0, [ free_87>=33 ], cost: 1 58: [29] -> f222 : Q_1'=1+Q_1, B3'=free_88, [ 0>=W1 ], cost: 1 Applied chaining over branches and pruning: Start location: f0 108: f93 -> f100 : S'=1, [ 8>=A && 15>=A ], cost: 2 109: f93 -> f100 : S'=1, [ A>=10 && 15>=A ], cost: 2 110: f93 -> f100 : S'=1, [ A>=10 && A>=17 ], cost: 2 21: f93 -> f113 : A'=9, T'=0, U'=0, V'=16, W'=32, X'=48, [ A==9 ], cost: 1 111: f93 -> f113 : A'=16, T'=0, U'=0, V'=16, W'=32, X'=48, [ A>=10 && A==16 ], cost: 2 4: f0 -> f34 : B'=0, C'=free, D'=free_2, E'=free_3, F'=free_1, G'=free_2, [ B==0 ], cost: 1 87: f0 -> f34 : B'=0, C'=free_4, D'=free_6, E'=free_7, F'=free_5, G'=free_6, H'=free_12, Q'=33, [ 0>=1+B && 32>=2 && 33>=33 ], cost: 33 88: f0 -> f34 : B'=0, C'=free_8, D'=free_10, E'=free_11, F'=free_9, G'=free_10, H'=free_12, Q'=33, [ B>=1 && 32>=2 && 33>=33 ], cost: 33 9: f34 -> f41 : Q'=28, J'=56, [], cost: 1 31: f34 -> f182 : Q'=32, J'=64, [], cost: 1 89: f41 -> f41 : Q'=-1+Q, J'=-1+J, K'=F, L'=free_14, M'=32, N'=1, O'=1, U3'=1, V3'=F, W3'=free_108, X3'=32, Y3'=1, Z3'=1, A4'=1, [ 32>=free_14 && Q>=1 && 32>=free_108 ], cost: 2 90: f41 -> f41 : Q'=-1+Q, J'=-1+J, K'=F, L'=free_14, M'=32, N'=1, O'=1, U3'=1, V3'=F, W3'=free_109, X3'=32, Y3'=0, Z3'=0, A4'=0, [ 32>=free_14 && Q>=1 && 32>=free_109 ], cost: 2 92: f41 -> f41 : Q'=-1+Q, J'=-1+J, K'=F, L'=free_14, M'=32, N'=1, O'=1, U3'=1, V3'=F, W3'=free_111, X3'=32, Z3'=0, A4'=0, B4'=0, [ 32>=free_14 && Q>=1 && free_111>=33 ], cost: 2 96: f41 -> f41 : Q'=-1+Q, J'=-1+J, K'=F, L'=free_15, M'=32, N'=0, O'=0, U3'=0, V3'=F, W3'=free_111, X3'=32, Z3'=0, A4'=0, B4'=0, [ 32>=free_15 && Q>=1 && free_111>=33 ], cost: 2 98: f41 -> f41 : Q'=-1+Q, J'=-1+J, K'=F, L'=free_16, M'=32, O'=1, P'=1, U3'=1, V3'=F, W3'=free_109, X3'=32, Y3'=0, Z3'=0, A4'=0, [ free_16>=33 && Q>=1 && 32>=free_109 ], cost: 2 79: f41 -> f81 : Q_1'=1, [ 0>=Q ], cost: 1 105: f81 -> f93 : A'=Q_1, R'=free_18, [ 0>=Q_1 && 1>=Q_1 ], cost: 2 106: f81 -> f93 : A'=Q_1, R'=free_19, [ 16>=Q_1 && Q_1>=2 && Q_1>=3 ], cost: 2 19: f81 -> f113 : A'=1, Q_1'=1, R'=free_20, T'=0, U'=0, V'=16, W'=32, X'=48, [ Q_1==1 ], cost: 1 107: f81 -> f113 : A'=2, R'=free_19, T'=0, U'=0, V'=16, W'=32, X'=48, [ 16>=Q_1 && Q_1>=2 && Q_1==2 ], cost: 2 74: f81 -> f182 : Q'=32, J'=64, [ Q_1>=17 ], cost: 1 82: f100 -> f113 : S'=3, T'=0, U'=0, V'=16, W'=32, X'=48, [ 2>=S && 3>=3 ], cost: 4-S 72: f113 -> f81 : Q_1'=1+Q_1, [ 0>=V ], cost: 1 112: f113 -> f150 : Y'=free_21, Z'=free_22, A1'=free_23, B1'=28, C1'=1, D1'=1, F1'=1, G1'=free_33, H1'=free_34, Q1'=free_35, J1'=28, K1'=1, L1'=1, [ 28>=free_23 && V>=1 && 28>=free_35 ], cost: 2 113: f113 -> f150 : Y'=free_21, Z'=free_22, A1'=free_23, B1'=28, C1'=1, D1'=1, F1'=1, G1'=free_36, H1'=free_37, Q1'=free_38, J1'=28, K1'=0, L1'=0, [ 28>=free_23 && V>=1 && 28>=free_38 ], cost: 2 115: f113 -> f150 : Y'=free_21, Z'=free_22, A1'=free_23, B1'=28, C1'=1, D1'=1, F1'=1, G1'=free_42, H1'=free_43, Q1'=free_44, J1'=28, L1'=0, M1'=0, [ 28>=free_23 && V>=1 && free_44>=29 ], cost: 2 119: f113 -> f150 : Y'=free_24, Z'=free_25, A1'=free_26, B1'=28, C1'=0, D1'=0, F1'=0, G1'=free_42, H1'=free_43, Q1'=free_44, J1'=28, L1'=0, M1'=0, [ 28>=free_26 && V>=1 && free_44>=29 ], cost: 2 121: f113 -> f150 : Y'=free_27, Z'=free_28, A1'=free_29, B1'=28, D1'=1, E1'=1, F1'=1, G1'=free_36, H1'=free_37, Q1'=free_38, J1'=28, K1'=0, L1'=0, [ free_29>=29 && V>=1 && 28>=free_38 ], cost: 2 68: f150 -> f113 : V'=-1+V, W'=-1+W, X'=-1+X, L3'=L1, M3'=free_96, N3'=free_97, O3'=free_98, P3'=28, Q3_1'=1, R3'=1, S3'=1, [ 28>=free_98 ], cost: 1 69: f150 -> f113 : V'=-1+V, W'=-1+W, X'=-1+X, L3'=L1, M3'=free_99, N3'=free_100, O3'=free_101, P3'=28, Q3_1'=0, R3'=0, S3'=0, [ 28>=free_101 ], cost: 1 70: f150 -> f113 : V'=-1+V, W'=-1+W, X'=-1+X, L3'=L1, M3'=free_102, N3'=free_103, O3'=free_104, P3'=28, R3'=1, S3'=1, T3'=1, [ free_104>=29 ], cost: 1 71: f150 -> f113 : V'=-1+V, W'=-1+W, X'=-1+X, L3'=L1, M3'=free_105, N3'=free_106, O3'=free_107, P3'=28, R3'=0, S3'=0, T3'=0, [ free_107>=29 ], cost: 1 128: f182 -> f182 : Q'=-1+Q, J'=-1+J, N1'=E, O1'=free_45, P1'=32, Q1_1'=1, R1'=1, D3'=1, E3'=E, F3'=free_92, G3'=32, H3'=1, Q3'=1, J3'=1, [ 32>=free_45 && Q>=1 && 32>=free_92 ], cost: 2 129: f182 -> f182 : Q'=-1+Q, J'=-1+J, N1'=E, O1'=free_45, P1'=32, Q1_1'=1, R1'=1, D3'=1, E3'=E, F3'=free_93, G3'=32, H3'=0, Q3'=0, J3'=0, [ 32>=free_45 && Q>=1 && 32>=free_93 ], cost: 2 131: f182 -> f182 : Q'=-1+Q, J'=-1+J, N1'=E, O1'=free_45, P1'=32, Q1_1'=1, R1'=1, D3'=1, E3'=E, F3'=free_95, G3'=32, Q3'=0, J3'=0, K3'=0, [ 32>=free_45 && Q>=1 && free_95>=33 ], cost: 2 135: f182 -> f182 : Q'=-1+Q, J'=-1+J, N1'=E, O1'=free_46, P1'=32, Q1_1'=0, R1'=0, D3'=0, E3'=E, F3'=free_95, G3'=32, Q3'=0, J3'=0, K3'=0, [ 32>=free_46 && Q>=1 && free_95>=33 ], cost: 2 137: f182 -> f182 : Q'=-1+Q, J'=-1+J, N1'=E, O1'=free_47, P1'=32, R1'=1, S1'=1, D3'=1, E3'=E, F3'=free_93, G3'=32, H3'=0, Q3'=0, J3'=0, [ free_47>=33 && Q>=1 && 32>=free_93 ], cost: 2 67: f182 -> f222 : Q_1'=1, [ 0>=Q ], cost: 1 36: f222 -> f237 : G'=1, T1'=17-Q_1, U1'=free_49, V1'=free_50, W1'=16, X1'=32, Y1'=48, [ 16>=Q_1 && G==1 ], cost: 1 37: f222 -> f237 : T1'=Q_1, U1'=free_51, V1'=free_52, W1'=16, X1'=32, Y1'=48, [ 16>=Q_1 && 0>=G ], cost: 1 38: f222 -> f237 : T1'=Q_1, U1'=free_53, V1'=free_54, W1'=16, X1'=32, Y1'=48, [ 16>=Q_1 && G>=2 ], cost: 1 62: f222 -> f314 : Q'=32, J'=64, B3'=free_91, C3'=0, [ Q_1>=17 ], cost: 1 144: f237 -> f250 : Z1'=1, A2'=1, [ W1>=1 ], cost: 2 145: f237 -> f250 : Z1'=1, A2'=0, [ W1>=1 ], cost: 2 146: f237 -> f250 : Z1'=0, A2'=1, [ W1>=1 ], cost: 2 147: f237 -> f250 : Z1'=0, A2'=0, [ W1>=1 ], cost: 2 148: f237 -> [29] : W1'=0, Y1'=9, C2'=free_55, D2'=free_56, E2'=0, F2'=free_59, G2'=free_61, H2'=free_58, Q2'=free_60, J2'=free_62, K2'=1, [ 0>=W1 && 4>=1 && 5>=5 && 8>=1 && 0>=0 && 32>=1 ], cost: 47 149: f237 -> [29] : W1'=0, Y1'=9, C2'=free_55, D2'=free_56, E2'=0, F2'=free_59, G2'=free_61, H2'=free_58, Q2'=free_60, J2'=free_63, K2'=0, [ 0>=W1 && 4>=1 && 5>=5 && 8>=1 && 0>=0 && 32>=1 ], cost: 47 43: f250 -> f237 : W1'=-1+W1, X1'=-1+X1, Y1'=-1+Y1, B2'=1, [], cost: 1 44: f250 -> f237 : W1'=-1+W1, X1'=-1+X1, Y1'=-1+Y1, B2'=0, [], cost: 1 150: f314 -> f314 : Q'=-1+Q, J'=-1+J, L2'=free_64, M2'=free_65, N2'=free_66, O2'=32, P2'=1, Q2_1'=1, S2'=1, T2'=free_76, U2'=free_77, V2'=free_78, W2'=32, X2'=1, Y2'=1, Z2'=1, [ 32>=free_66 && Q>=1 && 32>=free_78 ], cost: 2 151: f314 -> f314 : Q'=-1+Q, J'=-1+J, L2'=free_64, M2'=free_65, N2'=free_66, O2'=32, P2'=1, Q2_1'=1, S2'=1, T2'=free_79, U2'=free_80, V2'=free_81, W2'=32, X2'=0, Y2'=0, Z2'=0, [ 32>=free_66 && Q>=1 && 32>=free_81 ], cost: 2 153: f314 -> f314 : Q'=-1+Q, J'=-1+J, L2'=free_64, M2'=free_65, N2'=free_66, O2'=32, P2'=1, Q2_1'=1, S2'=1, T2'=free_85, U2'=free_86, V2'=free_87, W2'=32, Y2'=0, Z2'=0, A3'=0, [ 32>=free_66 && Q>=1 && free_87>=33 ], cost: 2 157: f314 -> f314 : Q'=-1+Q, J'=-1+J, L2'=free_67, M2'=free_68, N2'=free_69, O2'=32, P2'=0, Q2_1'=0, S2'=0, T2'=free_85, U2'=free_86, V2'=free_87, W2'=32, Y2'=0, Z2'=0, A3'=0, [ 32>=free_69 && Q>=1 && free_87>=33 ], cost: 2 159: f314 -> f314 : Q'=-1+Q, J'=-1+J, L2'=free_70, M2'=free_71, N2'=free_72, O2'=32, Q2_1'=1, R2'=1, S2'=1, T2'=free_79, U2'=free_80, V2'=free_81, W2'=32, X2'=0, Y2'=0, Z2'=0, [ free_72>=33 && Q>=1 && 32>=free_81 ], cost: 2 58: [29] -> f222 : Q_1'=1+Q_1, B3'=free_88, [ 0>=W1 ], cost: 1 Eliminating 5 self-loops for location f41 Self-Loop 89 has the metering function: Q, resulting in the new transition 166. Self-Loop 90 has the metering function: Q, resulting in the new transition 167. Self-Loop 92 has the metering function: Q, resulting in the new transition 168. Self-Loop 96 has the metering function: Q, resulting in the new transition 169. Self-Loop 98 has the metering function: Q, resulting in the new transition 170. Removing the self-loops: 89 90 92 96 98. Eliminating 5 self-loops for location f182 Self-Loop 128 has the metering function: Q, resulting in the new transition 171. Self-Loop 129 has the metering function: Q, resulting in the new transition 172. Self-Loop 131 has the metering function: Q, resulting in the new transition 173. Self-Loop 135 has the metering function: Q, resulting in the new transition 174. Self-Loop 137 has the metering function: Q, resulting in the new transition 175. Removing the self-loops: 128 129 131 135 137. Eliminating 5 self-loops for location f314 Self-Loop 150 has the metering function: Q, resulting in the new transition 176. Self-Loop 151 has the metering function: Q, resulting in the new transition 177. Self-Loop 153 has the metering function: Q, resulting in the new transition 178. Self-Loop 157 has the metering function: Q, resulting in the new transition 179. Self-Loop 159 has the metering function: Q, resulting in the new transition 180. Removing the self-loops: 150 151 153 157 159. Removed all Self-loops using metering functions (where possible): Start location: f0 108: f93 -> f100 : S'=1, [ 8>=A && 15>=A ], cost: 2 109: f93 -> f100 : S'=1, [ A>=10 && 15>=A ], cost: 2 110: f93 -> f100 : S'=1, [ A>=10 && A>=17 ], cost: 2 21: f93 -> f113 : A'=9, T'=0, U'=0, V'=16, W'=32, X'=48, [ A==9 ], cost: 1 111: f93 -> f113 : A'=16, T'=0, U'=0, V'=16, W'=32, X'=48, [ A>=10 && A==16 ], cost: 2 4: f0 -> f34 : B'=0, C'=free, D'=free_2, E'=free_3, F'=free_1, G'=free_2, [ B==0 ], cost: 1 87: f0 -> f34 : B'=0, C'=free_4, D'=free_6, E'=free_7, F'=free_5, G'=free_6, H'=free_12, Q'=33, [ 0>=1+B && 32>=2 && 33>=33 ], cost: 33 88: f0 -> f34 : B'=0, C'=free_8, D'=free_10, E'=free_11, F'=free_9, G'=free_10, H'=free_12, Q'=33, [ B>=1 && 32>=2 && 33>=33 ], cost: 33 9: f34 -> f41 : Q'=28, J'=56, [], cost: 1 31: f34 -> f182 : Q'=32, J'=64, [], cost: 1 166: f41 -> [30] : Q'=0, J'=-Q+J, K'=F, L'=free_14, M'=32, N'=1, O'=1, U3'=1, V3'=F, W3'=free_108, X3'=32, Y3'=1, Z3'=1, A4'=1, [ 32>=free_14 && Q>=1 && 32>=free_108 ], cost: 2*Q 167: f41 -> [30] : Q'=0, J'=-Q+J, K'=F, L'=free_14, M'=32, N'=1, O'=1, U3'=1, V3'=F, W3'=free_109, X3'=32, Y3'=0, Z3'=0, A4'=0, [ 32>=free_14 && Q>=1 && 32>=free_109 ], cost: 2*Q 168: f41 -> [30] : Q'=0, J'=-Q+J, K'=F, L'=free_14, M'=32, N'=1, O'=1, U3'=1, V3'=F, W3'=free_111, X3'=32, Z3'=0, A4'=0, B4'=0, [ 32>=free_14 && Q>=1 && free_111>=33 ], cost: 2*Q 169: f41 -> [30] : Q'=0, J'=-Q+J, K'=F, L'=free_15, M'=32, N'=0, O'=0, U3'=0, V3'=F, W3'=free_111, X3'=32, Z3'=0, A4'=0, B4'=0, [ 32>=free_15 && Q>=1 && free_111>=33 ], cost: 2*Q 170: f41 -> [30] : Q'=0, J'=-Q+J, K'=F, L'=free_16, M'=32, O'=1, P'=1, U3'=1, V3'=F, W3'=free_109, X3'=32, Y3'=0, Z3'=0, A4'=0, [ free_16>=33 && Q>=1 && 32>=free_109 ], cost: 2*Q 105: f81 -> f93 : A'=Q_1, R'=free_18, [ 0>=Q_1 && 1>=Q_1 ], cost: 2 106: f81 -> f93 : A'=Q_1, R'=free_19, [ 16>=Q_1 && Q_1>=2 && Q_1>=3 ], cost: 2 19: f81 -> f113 : A'=1, Q_1'=1, R'=free_20, T'=0, U'=0, V'=16, W'=32, X'=48, [ Q_1==1 ], cost: 1 107: f81 -> f113 : A'=2, R'=free_19, T'=0, U'=0, V'=16, W'=32, X'=48, [ 16>=Q_1 && Q_1>=2 && Q_1==2 ], cost: 2 74: f81 -> f182 : Q'=32, J'=64, [ Q_1>=17 ], cost: 1 82: f100 -> f113 : S'=3, T'=0, U'=0, V'=16, W'=32, X'=48, [ 2>=S && 3>=3 ], cost: 4-S 72: f113 -> f81 : Q_1'=1+Q_1, [ 0>=V ], cost: 1 112: f113 -> f150 : Y'=free_21, Z'=free_22, A1'=free_23, B1'=28, C1'=1, D1'=1, F1'=1, G1'=free_33, H1'=free_34, Q1'=free_35, J1'=28, K1'=1, L1'=1, [ 28>=free_23 && V>=1 && 28>=free_35 ], cost: 2 113: f113 -> f150 : Y'=free_21, Z'=free_22, A1'=free_23, B1'=28, C1'=1, D1'=1, F1'=1, G1'=free_36, H1'=free_37, Q1'=free_38, J1'=28, K1'=0, L1'=0, [ 28>=free_23 && V>=1 && 28>=free_38 ], cost: 2 115: f113 -> f150 : Y'=free_21, Z'=free_22, A1'=free_23, B1'=28, C1'=1, D1'=1, F1'=1, G1'=free_42, H1'=free_43, Q1'=free_44, J1'=28, L1'=0, M1'=0, [ 28>=free_23 && V>=1 && free_44>=29 ], cost: 2 119: f113 -> f150 : Y'=free_24, Z'=free_25, A1'=free_26, B1'=28, C1'=0, D1'=0, F1'=0, G1'=free_42, H1'=free_43, Q1'=free_44, J1'=28, L1'=0, M1'=0, [ 28>=free_26 && V>=1 && free_44>=29 ], cost: 2 121: f113 -> f150 : Y'=free_27, Z'=free_28, A1'=free_29, B1'=28, D1'=1, E1'=1, F1'=1, G1'=free_36, H1'=free_37, Q1'=free_38, J1'=28, K1'=0, L1'=0, [ free_29>=29 && V>=1 && 28>=free_38 ], cost: 2 68: f150 -> f113 : V'=-1+V, W'=-1+W, X'=-1+X, L3'=L1, M3'=free_96, N3'=free_97, O3'=free_98, P3'=28, Q3_1'=1, R3'=1, S3'=1, [ 28>=free_98 ], cost: 1 69: f150 -> f113 : V'=-1+V, W'=-1+W, X'=-1+X, L3'=L1, M3'=free_99, N3'=free_100, O3'=free_101, P3'=28, Q3_1'=0, R3'=0, S3'=0, [ 28>=free_101 ], cost: 1 70: f150 -> f113 : V'=-1+V, W'=-1+W, X'=-1+X, L3'=L1, M3'=free_102, N3'=free_103, O3'=free_104, P3'=28, R3'=1, S3'=1, T3'=1, [ free_104>=29 ], cost: 1 71: f150 -> f113 : V'=-1+V, W'=-1+W, X'=-1+X, L3'=L1, M3'=free_105, N3'=free_106, O3'=free_107, P3'=28, R3'=0, S3'=0, T3'=0, [ free_107>=29 ], cost: 1 171: f182 -> [31] : Q'=0, J'=-Q+J, N1'=E, O1'=free_45, P1'=32, Q1_1'=1, R1'=1, D3'=1, E3'=E, F3'=free_92, G3'=32, H3'=1, Q3'=1, J3'=1, [ 32>=free_45 && Q>=1 && 32>=free_92 ], cost: 2*Q 172: f182 -> [31] : Q'=0, J'=-Q+J, N1'=E, O1'=free_45, P1'=32, Q1_1'=1, R1'=1, D3'=1, E3'=E, F3'=free_93, G3'=32, H3'=0, Q3'=0, J3'=0, [ 32>=free_45 && Q>=1 && 32>=free_93 ], cost: 2*Q 173: f182 -> [31] : Q'=0, J'=-Q+J, N1'=E, O1'=free_45, P1'=32, Q1_1'=1, R1'=1, D3'=1, E3'=E, F3'=free_95, G3'=32, Q3'=0, J3'=0, K3'=0, [ 32>=free_45 && Q>=1 && free_95>=33 ], cost: 2*Q 174: f182 -> [31] : Q'=0, J'=-Q+J, N1'=E, O1'=free_46, P1'=32, Q1_1'=0, R1'=0, D3'=0, E3'=E, F3'=free_95, G3'=32, Q3'=0, J3'=0, K3'=0, [ 32>=free_46 && Q>=1 && free_95>=33 ], cost: 2*Q 175: f182 -> [31] : Q'=0, J'=-Q+J, N1'=E, O1'=free_47, P1'=32, R1'=1, S1'=1, D3'=1, E3'=E, F3'=free_93, G3'=32, H3'=0, Q3'=0, J3'=0, [ free_47>=33 && Q>=1 && 32>=free_93 ], cost: 2*Q 36: f222 -> f237 : G'=1, T1'=17-Q_1, U1'=free_49, V1'=free_50, W1'=16, X1'=32, Y1'=48, [ 16>=Q_1 && G==1 ], cost: 1 37: f222 -> f237 : T1'=Q_1, U1'=free_51, V1'=free_52, W1'=16, X1'=32, Y1'=48, [ 16>=Q_1 && 0>=G ], cost: 1 38: f222 -> f237 : T1'=Q_1, U1'=free_53, V1'=free_54, W1'=16, X1'=32, Y1'=48, [ 16>=Q_1 && G>=2 ], cost: 1 62: f222 -> f314 : Q'=32, J'=64, B3'=free_91, C3'=0, [ Q_1>=17 ], cost: 1 144: f237 -> f250 : Z1'=1, A2'=1, [ W1>=1 ], cost: 2 145: f237 -> f250 : Z1'=1, A2'=0, [ W1>=1 ], cost: 2 146: f237 -> f250 : Z1'=0, A2'=1, [ W1>=1 ], cost: 2 147: f237 -> f250 : Z1'=0, A2'=0, [ W1>=1 ], cost: 2 148: f237 -> [29] : W1'=0, Y1'=9, C2'=free_55, D2'=free_56, E2'=0, F2'=free_59, G2'=free_61, H2'=free_58, Q2'=free_60, J2'=free_62, K2'=1, [ 0>=W1 && 4>=1 && 5>=5 && 8>=1 && 0>=0 && 32>=1 ], cost: 47 149: f237 -> [29] : W1'=0, Y1'=9, C2'=free_55, D2'=free_56, E2'=0, F2'=free_59, G2'=free_61, H2'=free_58, Q2'=free_60, J2'=free_63, K2'=0, [ 0>=W1 && 4>=1 && 5>=5 && 8>=1 && 0>=0 && 32>=1 ], cost: 47 43: f250 -> f237 : W1'=-1+W1, X1'=-1+X1, Y1'=-1+Y1, B2'=1, [], cost: 1 44: f250 -> f237 : W1'=-1+W1, X1'=-1+X1, Y1'=-1+Y1, B2'=0, [], cost: 1 176: f314 -> [32] : Q'=0, J'=-Q+J, L2'=free_64, M2'=free_65, N2'=free_66, O2'=32, P2'=1, Q2_1'=1, S2'=1, T2'=free_76, U2'=free_77, V2'=free_78, W2'=32, X2'=1, Y2'=1, Z2'=1, [ 32>=free_66 && Q>=1 && 32>=free_78 ], cost: 2*Q 177: f314 -> [32] : Q'=0, J'=-Q+J, L2'=free_64, M2'=free_65, N2'=free_66, O2'=32, P2'=1, Q2_1'=1, S2'=1, T2'=free_79, U2'=free_80, V2'=free_81, W2'=32, X2'=0, Y2'=0, Z2'=0, [ 32>=free_66 && Q>=1 && 32>=free_81 ], cost: 2*Q 178: f314 -> [32] : Q'=0, J'=-Q+J, L2'=free_64, M2'=free_65, N2'=free_66, O2'=32, P2'=1, Q2_1'=1, S2'=1, T2'=free_85, U2'=free_86, V2'=free_87, W2'=32, Y2'=0, Z2'=0, A3'=0, [ 32>=free_66 && Q>=1 && free_87>=33 ], cost: 2*Q 179: f314 -> [32] : Q'=0, J'=-Q+J, L2'=free_67, M2'=free_68, N2'=free_69, O2'=32, P2'=0, Q2_1'=0, S2'=0, T2'=free_85, U2'=free_86, V2'=free_87, W2'=32, Y2'=0, Z2'=0, A3'=0, [ 32>=free_69 && Q>=1 && free_87>=33 ], cost: 2*Q 180: f314 -> [32] : Q'=0, J'=-Q+J, L2'=free_70, M2'=free_71, N2'=free_72, O2'=32, Q2_1'=1, R2'=1, S2'=1, T2'=free_79, U2'=free_80, V2'=free_81, W2'=32, X2'=0, Y2'=0, Z2'=0, [ free_72>=33 && Q>=1 && 32>=free_81 ], cost: 2*Q 58: [29] -> f222 : Q_1'=1+Q_1, B3'=free_88, [ 0>=W1 ], cost: 1 79: [30] -> f81 : Q_1'=1, [ 0>=Q ], cost: 1 67: [31] -> f222 : Q_1'=1, [ 0>=Q ], cost: 1 Applied chaining over branches and pruning: Start location: f0 181: f0 -> f41 : B'=0, C'=free, D'=free_2, E'=free_3, F'=free_1, G'=free_2, Q'=28, J'=56, [ B==0 ], cost: 2 183: f0 -> f41 : B'=0, C'=free_4, D'=free_6, E'=free_7, F'=free_5, G'=free_6, H'=free_12, Q'=28, J'=56, [ 0>=1+B && 32>=2 && 33>=33 ], cost: 34 185: f0 -> f41 : B'=0, C'=free_8, D'=free_10, E'=free_11, F'=free_9, G'=free_10, H'=free_12, Q'=28, J'=56, [ B>=1 && 32>=2 && 33>=33 ], cost: 34 182: f0 -> f182 : B'=0, C'=free, D'=free_2, E'=free_3, F'=free_1, G'=free_2, Q'=32, J'=64, [ B==0 ], cost: 2 184: f0 -> f182 : B'=0, C'=free_4, D'=free_6, E'=free_7, F'=free_5, G'=free_6, H'=free_12, Q'=32, J'=64, [ 0>=1+B && 32>=2 && 33>=33 ], cost: 34 186: f0 -> f182 : B'=0, C'=free_8, D'=free_10, E'=free_11, F'=free_9, G'=free_10, H'=free_12, Q'=32, J'=64, [ B>=1 && 32>=2 && 33>=33 ], cost: 34 187: f41 -> f81 : Q'=0, J'=-Q+J, K'=F, L'=free_14, M'=32, N'=1, O'=1, Q_1'=1, U3'=1, V3'=F, W3'=free_108, X3'=32, Y3'=1, Z3'=1, A4'=1, [ 32>=free_14 && Q>=1 && 32>=free_108 && 0>=0 ], cost: 1+2*Q 188: f41 -> f81 : Q'=0, J'=-Q+J, K'=F, L'=free_14, M'=32, N'=1, O'=1, Q_1'=1, U3'=1, V3'=F, W3'=free_109, X3'=32, Y3'=0, Z3'=0, A4'=0, [ 32>=free_14 && Q>=1 && 32>=free_109 && 0>=0 ], cost: 1+2*Q 189: f41 -> f81 : Q'=0, J'=-Q+J, K'=F, L'=free_14, M'=32, N'=1, O'=1, Q_1'=1, U3'=1, V3'=F, W3'=free_111, X3'=32, Z3'=0, A4'=0, B4'=0, [ 32>=free_14 && Q>=1 && free_111>=33 && 0>=0 ], cost: 1+2*Q 190: f41 -> f81 : Q'=0, J'=-Q+J, K'=F, L'=free_15, M'=32, N'=0, O'=0, Q_1'=1, U3'=0, V3'=F, W3'=free_111, X3'=32, Z3'=0, A4'=0, B4'=0, [ 32>=free_15 && Q>=1 && free_111>=33 && 0>=0 ], cost: 1+2*Q 191: f41 -> f81 : Q'=0, J'=-Q+J, K'=F, L'=free_16, M'=32, O'=1, P'=1, Q_1'=1, U3'=1, V3'=F, W3'=free_109, X3'=32, Y3'=0, Z3'=0, A4'=0, [ free_16>=33 && Q>=1 && 32>=free_109 && 0>=0 ], cost: 1+2*Q 192: f81 -> f100 : A'=Q_1, R'=free_18, S'=1, [ 0>=Q_1 && 1>=Q_1 && 8>=Q_1 && 15>=Q_1 ], cost: 4 193: f81 -> f100 : A'=Q_1, R'=free_19, S'=1, [ 16>=Q_1 && Q_1>=2 && Q_1>=3 && 8>=Q_1 && 15>=Q_1 ], cost: 4 194: f81 -> f100 : A'=Q_1, R'=free_19, S'=1, [ 16>=Q_1 && Q_1>=2 && Q_1>=3 && Q_1>=10 && 15>=Q_1 ], cost: 4 19: f81 -> f113 : A'=1, Q_1'=1, R'=free_20, T'=0, U'=0, V'=16, W'=32, X'=48, [ Q_1==1 ], cost: 1 107: f81 -> f113 : A'=2, R'=free_19, T'=0, U'=0, V'=16, W'=32, X'=48, [ 16>=Q_1 && Q_1>=2 && Q_1==2 ], cost: 2 195: f81 -> f113 : A'=9, R'=free_19, T'=0, U'=0, V'=16, W'=32, X'=48, [ 16>=Q_1 && Q_1>=2 && Q_1>=3 && Q_1==9 ], cost: 3 196: f81 -> f113 : A'=16, R'=free_19, T'=0, U'=0, V'=16, W'=32, X'=48, [ 16>=Q_1 && Q_1>=2 && Q_1>=3 && Q_1>=10 && Q_1==16 ], cost: 4 74: f81 -> f182 : Q'=32, J'=64, [ Q_1>=17 ], cost: 1 82: f100 -> f113 : S'=3, T'=0, U'=0, V'=16, W'=32, X'=48, [ 2>=S && 3>=3 ], cost: 4-S 72: f113 -> f81 : Q_1'=1+Q_1, [ 0>=V ], cost: 1 197: f113 -> f113 : V'=-1+V, W'=-1+W, X'=-1+X, Y'=free_21, Z'=free_22, A1'=free_23, B1'=28, C1'=1, D1'=1, F1'=1, G1'=free_33, H1'=free_34, Q1'=free_35, J1'=28, K1'=1, L1'=1, L3'=1, M3'=free_96, N3'=free_97, O3'=free_98, P3'=28, Q3_1'=1, R3'=1, S3'=1, [ 28>=free_23 && V>=1 && 28>=free_35 && 28>=free_98 ], cost: 3 198: f113 -> f113 : V'=-1+V, W'=-1+W, X'=-1+X, Y'=free_21, Z'=free_22, A1'=free_23, B1'=28, C1'=1, D1'=1, F1'=1, G1'=free_33, H1'=free_34, Q1'=free_35, J1'=28, K1'=1, L1'=1, L3'=1, M3'=free_99, N3'=free_100, O3'=free_101, P3'=28, Q3_1'=0, R3'=0, S3'=0, [ 28>=free_23 && V>=1 && 28>=free_35 && 28>=free_101 ], cost: 3 200: f113 -> f113 : V'=-1+V, W'=-1+W, X'=-1+X, Y'=free_21, Z'=free_22, A1'=free_23, B1'=28, C1'=1, D1'=1, F1'=1, G1'=free_33, H1'=free_34, Q1'=free_35, J1'=28, K1'=1, L1'=1, L3'=1, M3'=free_105, N3'=free_106, O3'=free_107, P3'=28, R3'=0, S3'=0, T3'=0, [ 28>=free_23 && V>=1 && 28>=free_35 && free_107>=29 ], cost: 3 204: f113 -> f113 : V'=-1+V, W'=-1+W, X'=-1+X, Y'=free_21, Z'=free_22, A1'=free_23, B1'=28, C1'=1, D1'=1, F1'=1, G1'=free_36, H1'=free_37, Q1'=free_38, J1'=28, K1'=0, L1'=0, L3'=0, M3'=free_105, N3'=free_106, O3'=free_107, P3'=28, R3'=0, S3'=0, T3'=0, [ 28>=free_23 && V>=1 && 28>=free_38 && free_107>=29 ], cost: 3 207: f113 -> f113 : V'=-1+V, W'=-1+W, X'=-1+X, Y'=free_21, Z'=free_22, A1'=free_23, B1'=28, C1'=1, D1'=1, F1'=1, G1'=free_42, H1'=free_43, Q1'=free_44, J1'=28, L1'=0, M1'=0, L3'=0, M3'=free_102, N3'=free_103, O3'=free_104, P3'=28, R3'=1, S3'=1, T3'=1, [ 28>=free_23 && V>=1 && free_44>=29 && free_104>=29 ], cost: 3 217: f182 -> f222 : Q'=0, J'=-Q+J, Q_1'=1, N1'=E, O1'=free_45, P1'=32, Q1_1'=1, R1'=1, D3'=1, E3'=E, F3'=free_92, G3'=32, H3'=1, Q3'=1, J3'=1, [ 32>=free_45 && Q>=1 && 32>=free_92 && 0>=0 ], cost: 1+2*Q 218: f182 -> f222 : Q'=0, J'=-Q+J, Q_1'=1, N1'=E, O1'=free_45, P1'=32, Q1_1'=1, R1'=1, D3'=1, E3'=E, F3'=free_93, G3'=32, H3'=0, Q3'=0, J3'=0, [ 32>=free_45 && Q>=1 && 32>=free_93 && 0>=0 ], cost: 1+2*Q 219: f182 -> f222 : Q'=0, J'=-Q+J, Q_1'=1, N1'=E, O1'=free_45, P1'=32, Q1_1'=1, R1'=1, D3'=1, E3'=E, F3'=free_95, G3'=32, Q3'=0, J3'=0, K3'=0, [ 32>=free_45 && Q>=1 && free_95>=33 && 0>=0 ], cost: 1+2*Q 220: f182 -> f222 : Q'=0, J'=-Q+J, Q_1'=1, N1'=E, O1'=free_46, P1'=32, Q1_1'=0, R1'=0, D3'=0, E3'=E, F3'=free_95, G3'=32, Q3'=0, J3'=0, K3'=0, [ 32>=free_46 && Q>=1 && free_95>=33 && 0>=0 ], cost: 1+2*Q 221: f182 -> f222 : Q'=0, J'=-Q+J, Q_1'=1, N1'=E, O1'=free_47, P1'=32, R1'=1, S1'=1, D3'=1, E3'=E, F3'=free_93, G3'=32, H3'=0, Q3'=0, J3'=0, [ free_47>=33 && Q>=1 && 32>=free_93 && 0>=0 ], cost: 1+2*Q 36: f222 -> f237 : G'=1, T1'=17-Q_1, U1'=free_49, V1'=free_50, W1'=16, X1'=32, Y1'=48, [ 16>=Q_1 && G==1 ], cost: 1 37: f222 -> f237 : T1'=Q_1, U1'=free_51, V1'=free_52, W1'=16, X1'=32, Y1'=48, [ 16>=Q_1 && 0>=G ], cost: 1 38: f222 -> f237 : T1'=Q_1, U1'=free_53, V1'=free_54, W1'=16, X1'=32, Y1'=48, [ 16>=Q_1 && G>=2 ], cost: 1 235: f237 -> f222 : Q_1'=1+Q_1, W1'=0, Y1'=9, C2'=free_55, D2'=free_56, E2'=0, F2'=free_59, G2'=free_61, H2'=free_58, Q2'=free_60, J2'=free_62, K2'=1, B3'=free_88, [ 0>=W1 && 4>=1 && 5>=5 && 8>=1 && 0>=0 && 32>=1 && 0>=0 ], cost: 48 236: f237 -> f222 : Q_1'=1+Q_1, W1'=0, Y1'=9, C2'=free_55, D2'=free_56, E2'=0, F2'=free_59, G2'=free_61, H2'=free_58, Q2'=free_60, J2'=free_63, K2'=0, B3'=free_88, [ 0>=W1 && 4>=1 && 5>=5 && 8>=1 && 0>=0 && 32>=1 && 0>=0 ], cost: 48 227: f237 -> f237 : W1'=-1+W1, X1'=-1+X1, Y1'=-1+Y1, Z1'=1, A2'=1, B2'=1, [ W1>=1 ], cost: 3 228: f237 -> f237 : W1'=-1+W1, X1'=-1+X1, Y1'=-1+Y1, Z1'=1, A2'=1, B2'=0, [ W1>=1 ], cost: 3 230: f237 -> f237 : W1'=-1+W1, X1'=-1+X1, Y1'=-1+Y1, Z1'=1, A2'=0, B2'=0, [ W1>=1 ], cost: 3 231: f237 -> f237 : W1'=-1+W1, X1'=-1+X1, Y1'=-1+Y1, Z1'=0, A2'=1, B2'=1, [ W1>=1 ], cost: 3 232: f237 -> f237 : W1'=-1+W1, X1'=-1+X1, Y1'=-1+Y1, Z1'=0, A2'=1, B2'=0, [ W1>=1 ], cost: 3 Eliminating 5 self-loops for location f113 Self-Loop 197 has the metering function: V, resulting in the new transition 237. Self-Loop 198 has the metering function: V, resulting in the new transition 238. Self-Loop 200 has the metering function: V, resulting in the new transition 239. Self-Loop 204 has the metering function: V, resulting in the new transition 240. Self-Loop 207 has the metering function: V, resulting in the new transition 241. Removing the self-loops: 197 198 200 204 207. Eliminating 5 self-loops for location f237 Self-Loop 227 has the metering function: W1, resulting in the new transition 242. Self-Loop 228 has the metering function: W1, resulting in the new transition 243. Self-Loop 230 has the metering function: W1, resulting in the new transition 244. Self-Loop 231 has the metering function: W1, resulting in the new transition 245. Self-Loop 232 has the metering function: W1, resulting in the new transition 246. Removing the self-loops: 227 228 230 231 232. Removed all Self-loops using metering functions (where possible): Start location: f0 181: f0 -> f41 : B'=0, C'=free, D'=free_2, E'=free_3, F'=free_1, G'=free_2, Q'=28, J'=56, [ B==0 ], cost: 2 183: f0 -> f41 : B'=0, C'=free_4, D'=free_6, E'=free_7, F'=free_5, G'=free_6, H'=free_12, Q'=28, J'=56, [ 0>=1+B && 32>=2 && 33>=33 ], cost: 34 185: f0 -> f41 : B'=0, C'=free_8, D'=free_10, E'=free_11, F'=free_9, G'=free_10, H'=free_12, Q'=28, J'=56, [ B>=1 && 32>=2 && 33>=33 ], cost: 34 182: f0 -> f182 : B'=0, C'=free, D'=free_2, E'=free_3, F'=free_1, G'=free_2, Q'=32, J'=64, [ B==0 ], cost: 2 184: f0 -> f182 : B'=0, C'=free_4, D'=free_6, E'=free_7, F'=free_5, G'=free_6, H'=free_12, Q'=32, J'=64, [ 0>=1+B && 32>=2 && 33>=33 ], cost: 34 186: f0 -> f182 : B'=0, C'=free_8, D'=free_10, E'=free_11, F'=free_9, G'=free_10, H'=free_12, Q'=32, J'=64, [ B>=1 && 32>=2 && 33>=33 ], cost: 34 187: f41 -> f81 : Q'=0, J'=-Q+J, K'=F, L'=free_14, M'=32, N'=1, O'=1, Q_1'=1, U3'=1, V3'=F, W3'=free_108, X3'=32, Y3'=1, Z3'=1, A4'=1, [ 32>=free_14 && Q>=1 && 32>=free_108 && 0>=0 ], cost: 1+2*Q 188: f41 -> f81 : Q'=0, J'=-Q+J, K'=F, L'=free_14, M'=32, N'=1, O'=1, Q_1'=1, U3'=1, V3'=F, W3'=free_109, X3'=32, Y3'=0, Z3'=0, A4'=0, [ 32>=free_14 && Q>=1 && 32>=free_109 && 0>=0 ], cost: 1+2*Q 189: f41 -> f81 : Q'=0, J'=-Q+J, K'=F, L'=free_14, M'=32, N'=1, O'=1, Q_1'=1, U3'=1, V3'=F, W3'=free_111, X3'=32, Z3'=0, A4'=0, B4'=0, [ 32>=free_14 && Q>=1 && free_111>=33 && 0>=0 ], cost: 1+2*Q 190: f41 -> f81 : Q'=0, J'=-Q+J, K'=F, L'=free_15, M'=32, N'=0, O'=0, Q_1'=1, U3'=0, V3'=F, W3'=free_111, X3'=32, Z3'=0, A4'=0, B4'=0, [ 32>=free_15 && Q>=1 && free_111>=33 && 0>=0 ], cost: 1+2*Q 191: f41 -> f81 : Q'=0, J'=-Q+J, K'=F, L'=free_16, M'=32, O'=1, P'=1, Q_1'=1, U3'=1, V3'=F, W3'=free_109, X3'=32, Y3'=0, Z3'=0, A4'=0, [ free_16>=33 && Q>=1 && 32>=free_109 && 0>=0 ], cost: 1+2*Q 192: f81 -> f100 : A'=Q_1, R'=free_18, S'=1, [ 0>=Q_1 && 1>=Q_1 && 8>=Q_1 && 15>=Q_1 ], cost: 4 193: f81 -> f100 : A'=Q_1, R'=free_19, S'=1, [ 16>=Q_1 && Q_1>=2 && Q_1>=3 && 8>=Q_1 && 15>=Q_1 ], cost: 4 194: f81 -> f100 : A'=Q_1, R'=free_19, S'=1, [ 16>=Q_1 && Q_1>=2 && Q_1>=3 && Q_1>=10 && 15>=Q_1 ], cost: 4 19: f81 -> f113 : A'=1, Q_1'=1, R'=free_20, T'=0, U'=0, V'=16, W'=32, X'=48, [ Q_1==1 ], cost: 1 107: f81 -> f113 : A'=2, R'=free_19, T'=0, U'=0, V'=16, W'=32, X'=48, [ 16>=Q_1 && Q_1>=2 && Q_1==2 ], cost: 2 195: f81 -> f113 : A'=9, R'=free_19, T'=0, U'=0, V'=16, W'=32, X'=48, [ 16>=Q_1 && Q_1>=2 && Q_1>=3 && Q_1==9 ], cost: 3 196: f81 -> f113 : A'=16, R'=free_19, T'=0, U'=0, V'=16, W'=32, X'=48, [ 16>=Q_1 && Q_1>=2 && Q_1>=3 && Q_1>=10 && Q_1==16 ], cost: 4 74: f81 -> f182 : Q'=32, J'=64, [ Q_1>=17 ], cost: 1 82: f100 -> f113 : S'=3, T'=0, U'=0, V'=16, W'=32, X'=48, [ 2>=S && 3>=3 ], cost: 4-S 237: f113 -> [33] : V'=0, W'=-V+W, X'=X-V, Y'=free_21, Z'=free_22, A1'=free_23, B1'=28, C1'=1, D1'=1, F1'=1, G1'=free_33, H1'=free_34, Q1'=free_35, J1'=28, K1'=1, L1'=1, L3'=1, M3'=free_96, N3'=free_97, O3'=free_98, P3'=28, Q3_1'=1, R3'=1, S3'=1, [ 28>=free_23 && V>=1 && 28>=free_35 && 28>=free_98 ], cost: 3*V 238: f113 -> [33] : V'=0, W'=-V+W, X'=X-V, Y'=free_21, Z'=free_22, A1'=free_23, B1'=28, C1'=1, D1'=1, F1'=1, G1'=free_33, H1'=free_34, Q1'=free_35, J1'=28, K1'=1, L1'=1, L3'=1, M3'=free_99, N3'=free_100, O3'=free_101, P3'=28, Q3_1'=0, R3'=0, S3'=0, [ 28>=free_23 && V>=1 && 28>=free_35 && 28>=free_101 ], cost: 3*V 239: f113 -> [33] : V'=0, W'=-V+W, X'=X-V, Y'=free_21, Z'=free_22, A1'=free_23, B1'=28, C1'=1, D1'=1, F1'=1, G1'=free_33, H1'=free_34, Q1'=free_35, J1'=28, K1'=1, L1'=1, L3'=1, M3'=free_105, N3'=free_106, O3'=free_107, P3'=28, R3'=0, S3'=0, T3'=0, [ 28>=free_23 && V>=1 && 28>=free_35 && free_107>=29 ], cost: 3*V 240: f113 -> [33] : V'=0, W'=-V+W, X'=X-V, Y'=free_21, Z'=free_22, A1'=free_23, B1'=28, C1'=1, D1'=1, F1'=1, G1'=free_36, H1'=free_37, Q1'=free_38, J1'=28, K1'=0, L1'=0, L3'=0, M3'=free_105, N3'=free_106, O3'=free_107, P3'=28, R3'=0, S3'=0, T3'=0, [ 28>=free_23 && V>=1 && 28>=free_38 && free_107>=29 ], cost: 3*V 241: f113 -> [33] : V'=0, W'=-V+W, X'=X-V, Y'=free_21, Z'=free_22, A1'=free_23, B1'=28, C1'=1, D1'=1, F1'=1, G1'=free_42, H1'=free_43, Q1'=free_44, J1'=28, L1'=0, M1'=0, L3'=0, M3'=free_102, N3'=free_103, O3'=free_104, P3'=28, R3'=1, S3'=1, T3'=1, [ 28>=free_23 && V>=1 && free_44>=29 && free_104>=29 ], cost: 3*V 217: f182 -> f222 : Q'=0, J'=-Q+J, Q_1'=1, N1'=E, O1'=free_45, P1'=32, Q1_1'=1, R1'=1, D3'=1, E3'=E, F3'=free_92, G3'=32, H3'=1, Q3'=1, J3'=1, [ 32>=free_45 && Q>=1 && 32>=free_92 && 0>=0 ], cost: 1+2*Q 218: f182 -> f222 : Q'=0, J'=-Q+J, Q_1'=1, N1'=E, O1'=free_45, P1'=32, Q1_1'=1, R1'=1, D3'=1, E3'=E, F3'=free_93, G3'=32, H3'=0, Q3'=0, J3'=0, [ 32>=free_45 && Q>=1 && 32>=free_93 && 0>=0 ], cost: 1+2*Q 219: f182 -> f222 : Q'=0, J'=-Q+J, Q_1'=1, N1'=E, O1'=free_45, P1'=32, Q1_1'=1, R1'=1, D3'=1, E3'=E, F3'=free_95, G3'=32, Q3'=0, J3'=0, K3'=0, [ 32>=free_45 && Q>=1 && free_95>=33 && 0>=0 ], cost: 1+2*Q 220: f182 -> f222 : Q'=0, J'=-Q+J, Q_1'=1, N1'=E, O1'=free_46, P1'=32, Q1_1'=0, R1'=0, D3'=0, E3'=E, F3'=free_95, G3'=32, Q3'=0, J3'=0, K3'=0, [ 32>=free_46 && Q>=1 && free_95>=33 && 0>=0 ], cost: 1+2*Q 221: f182 -> f222 : Q'=0, J'=-Q+J, Q_1'=1, N1'=E, O1'=free_47, P1'=32, R1'=1, S1'=1, D3'=1, E3'=E, F3'=free_93, G3'=32, H3'=0, Q3'=0, J3'=0, [ free_47>=33 && Q>=1 && 32>=free_93 && 0>=0 ], cost: 1+2*Q 36: f222 -> f237 : G'=1, T1'=17-Q_1, U1'=free_49, V1'=free_50, W1'=16, X1'=32, Y1'=48, [ 16>=Q_1 && G==1 ], cost: 1 37: f222 -> f237 : T1'=Q_1, U1'=free_51, V1'=free_52, W1'=16, X1'=32, Y1'=48, [ 16>=Q_1 && 0>=G ], cost: 1 38: f222 -> f237 : T1'=Q_1, U1'=free_53, V1'=free_54, W1'=16, X1'=32, Y1'=48, [ 16>=Q_1 && G>=2 ], cost: 1 242: f237 -> [34] : W1'=0, X1'=X1-W1, Y1'=Y1-W1, Z1'=1, A2'=1, B2'=1, [ W1>=1 ], cost: 3*W1 243: f237 -> [34] : W1'=0, X1'=X1-W1, Y1'=Y1-W1, Z1'=1, A2'=1, B2'=0, [ W1>=1 ], cost: 3*W1 244: f237 -> [34] : W1'=0, X1'=X1-W1, Y1'=Y1-W1, Z1'=1, A2'=0, B2'=0, [ W1>=1 ], cost: 3*W1 245: f237 -> [34] : W1'=0, X1'=X1-W1, Y1'=Y1-W1, Z1'=0, A2'=1, B2'=1, [ W1>=1 ], cost: 3*W1 246: f237 -> [34] : W1'=0, X1'=X1-W1, Y1'=Y1-W1, Z1'=0, A2'=1, B2'=0, [ W1>=1 ], cost: 3*W1 72: [33] -> f81 : Q_1'=1+Q_1, [ 0>=V ], cost: 1 235: [34] -> f222 : Q_1'=1+Q_1, W1'=0, Y1'=9, C2'=free_55, D2'=free_56, E2'=0, F2'=free_59, G2'=free_61, H2'=free_58, Q2'=free_60, J2'=free_62, K2'=1, B3'=free_88, [ 0>=W1 && 4>=1 && 5>=5 && 8>=1 && 0>=0 && 32>=1 && 0>=0 ], cost: 48 236: [34] -> f222 : Q_1'=1+Q_1, W1'=0, Y1'=9, C2'=free_55, D2'=free_56, E2'=0, F2'=free_59, G2'=free_61, H2'=free_58, Q2'=free_60, J2'=free_63, K2'=0, B3'=free_88, [ 0>=W1 && 4>=1 && 5>=5 && 8>=1 && 0>=0 && 32>=1 && 0>=0 ], cost: 48 Applied chaining over branches and pruning: Start location: f0 247: f0 -> f81 : B'=0, C'=free, D'=free_2, E'=free_3, F'=free_1, G'=free_2, Q'=0, J'=28, K'=free_1, L'=free_14, M'=32, N'=1, O'=1, Q_1'=1, U3'=1, V3'=free_1, W3'=free_108, X3'=32, Y3'=1, Z3'=1, A4'=1, [ B==0 && 32>=free_14 && 28>=1 && 32>=free_108 && 0>=0 ], cost: 59 248: f0 -> f81 : B'=0, C'=free, D'=free_2, E'=free_3, F'=free_1, G'=free_2, Q'=0, J'=28, K'=free_1, L'=free_14, M'=32, N'=1, O'=1, Q_1'=1, U3'=1, V3'=free_1, W3'=free_109, X3'=32, Y3'=0, Z3'=0, A4'=0, [ B==0 && 32>=free_14 && 28>=1 && 32>=free_109 && 0>=0 ], cost: 59 250: f0 -> f81 : B'=0, C'=free, D'=free_2, E'=free_3, F'=free_1, G'=free_2, Q'=0, J'=28, K'=free_1, L'=free_15, M'=32, N'=0, O'=0, Q_1'=1, U3'=0, V3'=free_1, W3'=free_111, X3'=32, Z3'=0, A4'=0, B4'=0, [ B==0 && 32>=free_15 && 28>=1 && free_111>=33 && 0>=0 ], cost: 59 254: f0 -> f81 : B'=0, C'=free_4, D'=free_6, E'=free_7, F'=free_5, G'=free_6, H'=free_12, Q'=0, J'=28, K'=free_5, L'=free_14, M'=32, N'=1, O'=1, Q_1'=1, U3'=1, V3'=free_5, W3'=free_111, X3'=32, Z3'=0, A4'=0, B4'=0, [ 0>=1+B && 32>=2 && 33>=33 && 32>=free_14 && 28>=1 && free_111>=33 && 0>=0 ], cost: 91 255: f0 -> f81 : B'=0, C'=free_4, D'=free_6, E'=free_7, F'=free_5, G'=free_6, H'=free_12, Q'=0, J'=28, K'=free_5, L'=free_15, M'=32, N'=0, O'=0, Q_1'=1, U3'=0, V3'=free_5, W3'=free_111, X3'=32, Z3'=0, A4'=0, B4'=0, [ 0>=1+B && 32>=2 && 33>=33 && 32>=free_15 && 28>=1 && free_111>=33 && 0>=0 ], cost: 91 182: f0 -> f182 : B'=0, C'=free, D'=free_2, E'=free_3, F'=free_1, G'=free_2, Q'=32, J'=64, [ B==0 ], cost: 2 184: f0 -> f182 : B'=0, C'=free_4, D'=free_6, E'=free_7, F'=free_5, G'=free_6, H'=free_12, Q'=32, J'=64, [ 0>=1+B && 32>=2 && 33>=33 ], cost: 34 186: f0 -> f182 : B'=0, C'=free_8, D'=free_10, E'=free_11, F'=free_9, G'=free_10, H'=free_12, Q'=32, J'=64, [ B>=1 && 32>=2 && 33>=33 ], cost: 34 19: f81 -> f113 : A'=1, Q_1'=1, R'=free_20, T'=0, U'=0, V'=16, W'=32, X'=48, [ Q_1==1 ], cost: 1 107: f81 -> f113 : A'=2, R'=free_19, T'=0, U'=0, V'=16, W'=32, X'=48, [ 16>=Q_1 && Q_1>=2 && Q_1==2 ], cost: 2 195: f81 -> f113 : A'=9, R'=free_19, T'=0, U'=0, V'=16, W'=32, X'=48, [ 16>=Q_1 && Q_1>=2 && Q_1>=3 && Q_1==9 ], cost: 3 196: f81 -> f113 : A'=16, R'=free_19, T'=0, U'=0, V'=16, W'=32, X'=48, [ 16>=Q_1 && Q_1>=2 && Q_1>=3 && Q_1>=10 && Q_1==16 ], cost: 4 262: f81 -> f113 : A'=Q_1, R'=free_18, S'=3, T'=0, U'=0, V'=16, W'=32, X'=48, [ 0>=Q_1 && 1>=Q_1 && 8>=Q_1 && 15>=Q_1 && 2>=1 && 3>=3 ], cost: 7 74: f81 -> f182 : Q'=32, J'=64, [ Q_1>=17 ], cost: 1 265: f113 -> f81 : Q_1'=1+Q_1, V'=0, W'=-V+W, X'=X-V, Y'=free_21, Z'=free_22, A1'=free_23, B1'=28, C1'=1, D1'=1, F1'=1, G1'=free_33, H1'=free_34, Q1'=free_35, J1'=28, K1'=1, L1'=1, L3'=1, M3'=free_96, N3'=free_97, O3'=free_98, P3'=28, Q3_1'=1, R3'=1, S3'=1, [ 28>=free_23 && V>=1 && 28>=free_35 && 28>=free_98 && 0>=0 ], cost: 1+3*V 266: f113 -> f81 : Q_1'=1+Q_1, V'=0, W'=-V+W, X'=X-V, Y'=free_21, Z'=free_22, A1'=free_23, B1'=28, C1'=1, D1'=1, F1'=1, G1'=free_33, H1'=free_34, Q1'=free_35, J1'=28, K1'=1, L1'=1, L3'=1, M3'=free_99, N3'=free_100, O3'=free_101, P3'=28, Q3_1'=0, R3'=0, S3'=0, [ 28>=free_23 && V>=1 && 28>=free_35 && 28>=free_101 && 0>=0 ], cost: 1+3*V 267: f113 -> f81 : Q_1'=1+Q_1, V'=0, W'=-V+W, X'=X-V, Y'=free_21, Z'=free_22, A1'=free_23, B1'=28, C1'=1, D1'=1, F1'=1, G1'=free_33, H1'=free_34, Q1'=free_35, J1'=28, K1'=1, L1'=1, L3'=1, M3'=free_105, N3'=free_106, O3'=free_107, P3'=28, R3'=0, S3'=0, T3'=0, [ 28>=free_23 && V>=1 && 28>=free_35 && free_107>=29 && 0>=0 ], cost: 1+3*V 268: f113 -> f81 : Q_1'=1+Q_1, V'=0, W'=-V+W, X'=X-V, Y'=free_21, Z'=free_22, A1'=free_23, B1'=28, C1'=1, D1'=1, F1'=1, G1'=free_36, H1'=free_37, Q1'=free_38, J1'=28, K1'=0, L1'=0, L3'=0, M3'=free_105, N3'=free_106, O3'=free_107, P3'=28, R3'=0, S3'=0, T3'=0, [ 28>=free_23 && V>=1 && 28>=free_38 && free_107>=29 && 0>=0 ], cost: 1+3*V 269: f113 -> f81 : Q_1'=1+Q_1, V'=0, W'=-V+W, X'=X-V, Y'=free_21, Z'=free_22, A1'=free_23, B1'=28, C1'=1, D1'=1, F1'=1, G1'=free_42, H1'=free_43, Q1'=free_44, J1'=28, L1'=0, M1'=0, L3'=0, M3'=free_102, N3'=free_103, O3'=free_104, P3'=28, R3'=1, S3'=1, T3'=1, [ 28>=free_23 && V>=1 && free_44>=29 && free_104>=29 && 0>=0 ], cost: 1+3*V 217: f182 -> f222 : Q'=0, J'=-Q+J, Q_1'=1, N1'=E, O1'=free_45, P1'=32, Q1_1'=1, R1'=1, D3'=1, E3'=E, F3'=free_92, G3'=32, H3'=1, Q3'=1, J3'=1, [ 32>=free_45 && Q>=1 && 32>=free_92 && 0>=0 ], cost: 1+2*Q 218: f182 -> f222 : Q'=0, J'=-Q+J, Q_1'=1, N1'=E, O1'=free_45, P1'=32, Q1_1'=1, R1'=1, D3'=1, E3'=E, F3'=free_93, G3'=32, H3'=0, Q3'=0, J3'=0, [ 32>=free_45 && Q>=1 && 32>=free_93 && 0>=0 ], cost: 1+2*Q 219: f182 -> f222 : Q'=0, J'=-Q+J, Q_1'=1, N1'=E, O1'=free_45, P1'=32, Q1_1'=1, R1'=1, D3'=1, E3'=E, F3'=free_95, G3'=32, Q3'=0, J3'=0, K3'=0, [ 32>=free_45 && Q>=1 && free_95>=33 && 0>=0 ], cost: 1+2*Q 220: f182 -> f222 : Q'=0, J'=-Q+J, Q_1'=1, N1'=E, O1'=free_46, P1'=32, Q1_1'=0, R1'=0, D3'=0, E3'=E, F3'=free_95, G3'=32, Q3'=0, J3'=0, K3'=0, [ 32>=free_46 && Q>=1 && free_95>=33 && 0>=0 ], cost: 1+2*Q 221: f182 -> f222 : Q'=0, J'=-Q+J, Q_1'=1, N1'=E, O1'=free_47, P1'=32, R1'=1, S1'=1, D3'=1, E3'=E, F3'=free_93, G3'=32, H3'=0, Q3'=0, J3'=0, [ free_47>=33 && Q>=1 && 32>=free_93 && 0>=0 ], cost: 1+2*Q 270: f222 -> [34] : G'=1, T1'=17-Q_1, U1'=free_49, V1'=free_50, W1'=0, X1'=16, Y1'=32, Z1'=1, A2'=1, B2'=1, [ 16>=Q_1 && G==1 && 16>=1 ], cost: 49 271: f222 -> [34] : G'=1, T1'=17-Q_1, U1'=free_49, V1'=free_50, W1'=0, X1'=16, Y1'=32, Z1'=1, A2'=1, B2'=0, [ 16>=Q_1 && G==1 && 16>=1 ], cost: 49 273: f222 -> [34] : G'=1, T1'=17-Q_1, U1'=free_49, V1'=free_50, W1'=0, X1'=16, Y1'=32, Z1'=0, A2'=1, B2'=1, [ 16>=Q_1 && G==1 && 16>=1 ], cost: 49 277: f222 -> [34] : T1'=Q_1, U1'=free_51, V1'=free_52, W1'=0, X1'=16, Y1'=32, Z1'=1, A2'=0, B2'=0, [ 16>=Q_1 && 0>=G && 16>=1 ], cost: 49 278: f222 -> [34] : T1'=Q_1, U1'=free_51, V1'=free_52, W1'=0, X1'=16, Y1'=32, Z1'=0, A2'=1, B2'=1, [ 16>=Q_1 && 0>=G && 16>=1 ], cost: 49 235: [34] -> f222 : Q_1'=1+Q_1, W1'=0, Y1'=9, C2'=free_55, D2'=free_56, E2'=0, F2'=free_59, G2'=free_61, H2'=free_58, Q2'=free_60, J2'=free_62, K2'=1, B3'=free_88, [ 0>=W1 && 4>=1 && 5>=5 && 8>=1 && 0>=0 && 32>=1 && 0>=0 ], cost: 48 236: [34] -> f222 : Q_1'=1+Q_1, W1'=0, Y1'=9, C2'=free_55, D2'=free_56, E2'=0, F2'=free_59, G2'=free_61, H2'=free_58, Q2'=free_60, J2'=free_63, K2'=0, B3'=free_88, [ 0>=W1 && 4>=1 && 5>=5 && 8>=1 && 0>=0 && 32>=1 && 0>=0 ], cost: 48 Applied chaining over branches and pruning: Start location: f0 247: f0 -> f81 : B'=0, C'=free, D'=free_2, E'=free_3, F'=free_1, G'=free_2, Q'=0, J'=28, K'=free_1, L'=free_14, M'=32, N'=1, O'=1, Q_1'=1, U3'=1, V3'=free_1, W3'=free_108, X3'=32, Y3'=1, Z3'=1, A4'=1, [ B==0 && 32>=free_14 && 28>=1 && 32>=free_108 && 0>=0 ], cost: 59 248: f0 -> f81 : B'=0, C'=free, D'=free_2, E'=free_3, F'=free_1, G'=free_2, Q'=0, J'=28, K'=free_1, L'=free_14, M'=32, N'=1, O'=1, Q_1'=1, U3'=1, V3'=free_1, W3'=free_109, X3'=32, Y3'=0, Z3'=0, A4'=0, [ B==0 && 32>=free_14 && 28>=1 && 32>=free_109 && 0>=0 ], cost: 59 250: f0 -> f81 : B'=0, C'=free, D'=free_2, E'=free_3, F'=free_1, G'=free_2, Q'=0, J'=28, K'=free_1, L'=free_15, M'=32, N'=0, O'=0, Q_1'=1, U3'=0, V3'=free_1, W3'=free_111, X3'=32, Z3'=0, A4'=0, B4'=0, [ B==0 && 32>=free_15 && 28>=1 && free_111>=33 && 0>=0 ], cost: 59 254: f0 -> f81 : B'=0, C'=free_4, D'=free_6, E'=free_7, F'=free_5, G'=free_6, H'=free_12, Q'=0, J'=28, K'=free_5, L'=free_14, M'=32, N'=1, O'=1, Q_1'=1, U3'=1, V3'=free_5, W3'=free_111, X3'=32, Z3'=0, A4'=0, B4'=0, [ 0>=1+B && 32>=2 && 33>=33 && 32>=free_14 && 28>=1 && free_111>=33 && 0>=0 ], cost: 91 255: f0 -> f81 : B'=0, C'=free_4, D'=free_6, E'=free_7, F'=free_5, G'=free_6, H'=free_12, Q'=0, J'=28, K'=free_5, L'=free_15, M'=32, N'=0, O'=0, Q_1'=1, U3'=0, V3'=free_5, W3'=free_111, X3'=32, Z3'=0, A4'=0, B4'=0, [ 0>=1+B && 32>=2 && 33>=33 && 32>=free_15 && 28>=1 && free_111>=33 && 0>=0 ], cost: 91 182: f0 -> f182 : B'=0, C'=free, D'=free_2, E'=free_3, F'=free_1, G'=free_2, Q'=32, J'=64, [ B==0 ], cost: 2 184: f0 -> f182 : B'=0, C'=free_4, D'=free_6, E'=free_7, F'=free_5, G'=free_6, H'=free_12, Q'=32, J'=64, [ 0>=1+B && 32>=2 && 33>=33 ], cost: 34 186: f0 -> f182 : B'=0, C'=free_8, D'=free_10, E'=free_11, F'=free_9, G'=free_10, H'=free_12, Q'=32, J'=64, [ B>=1 && 32>=2 && 33>=33 ], cost: 34 285: f81 -> f81 : A'=1, Q_1'=2, R'=free_20, T'=0, U'=0, V'=0, W'=16, X'=32, Y'=free_21, Z'=free_22, A1'=free_23, B1'=28, C1'=1, D1'=1, F1'=1, G1'=free_33, H1'=free_34, Q1'=free_35, J1'=28, K1'=1, L1'=1, L3'=1, M3'=free_96, N3'=free_97, O3'=free_98, P3'=28, Q3_1'=1, R3'=1, S3'=1, [ Q_1==1 && 28>=free_23 && 16>=1 && 28>=free_35 && 28>=free_98 && 0>=0 ], cost: 50 286: f81 -> f81 : A'=1, Q_1'=2, R'=free_20, T'=0, U'=0, V'=0, W'=16, X'=32, Y'=free_21, Z'=free_22, A1'=free_23, B1'=28, C1'=1, D1'=1, F1'=1, G1'=free_33, H1'=free_34, Q1'=free_35, J1'=28, K1'=1, L1'=1, L3'=1, M3'=free_99, N3'=free_100, O3'=free_101, P3'=28, Q3_1'=0, R3'=0, S3'=0, [ Q_1==1 && 28>=free_23 && 16>=1 && 28>=free_35 && 28>=free_101 && 0>=0 ], cost: 50 288: f81 -> f81 : A'=1, Q_1'=2, R'=free_20, T'=0, U'=0, V'=0, W'=16, X'=32, Y'=free_21, Z'=free_22, A1'=free_23, B1'=28, C1'=1, D1'=1, F1'=1, G1'=free_36, H1'=free_37, Q1'=free_38, J1'=28, K1'=0, L1'=0, L3'=0, M3'=free_105, N3'=free_106, O3'=free_107, P3'=28, R3'=0, S3'=0, T3'=0, [ Q_1==1 && 28>=free_23 && 16>=1 && 28>=free_38 && free_107>=29 && 0>=0 ], cost: 50 292: f81 -> f81 : A'=2, Q_1'=1+Q_1, R'=free_19, T'=0, U'=0, V'=0, W'=16, X'=32, Y'=free_21, Z'=free_22, A1'=free_23, B1'=28, C1'=1, D1'=1, F1'=1, G1'=free_33, H1'=free_34, Q1'=free_35, J1'=28, K1'=1, L1'=1, L3'=1, M3'=free_105, N3'=free_106, O3'=free_107, P3'=28, R3'=0, S3'=0, T3'=0, [ 16>=Q_1 && Q_1>=2 && Q_1==2 && 28>=free_23 && 16>=1 && 28>=free_35 && free_107>=29 && 0>=0 ], cost: 51 297: f81 -> f81 : A'=9, Q_1'=1+Q_1, R'=free_19, T'=0, U'=0, V'=0, W'=16, X'=32, Y'=free_21, Z'=free_22, A1'=free_23, B1'=28, C1'=1, D1'=1, F1'=1, G1'=free_33, H1'=free_34, Q1'=free_35, J1'=28, K1'=1, L1'=1, L3'=1, M3'=free_105, N3'=free_106, O3'=free_107, P3'=28, R3'=0, S3'=0, T3'=0, [ 16>=Q_1 && Q_1>=2 && Q_1>=3 && Q_1==9 && 28>=free_23 && 16>=1 && 28>=free_35 && free_107>=29 && 0>=0 ], cost: 52 74: f81 -> f182 : Q'=32, J'=64, [ Q_1>=17 ], cost: 1 217: f182 -> f222 : Q'=0, J'=-Q+J, Q_1'=1, N1'=E, O1'=free_45, P1'=32, Q1_1'=1, R1'=1, D3'=1, E3'=E, F3'=free_92, G3'=32, H3'=1, Q3'=1, J3'=1, [ 32>=free_45 && Q>=1 && 32>=free_92 && 0>=0 ], cost: 1+2*Q 218: f182 -> f222 : Q'=0, J'=-Q+J, Q_1'=1, N1'=E, O1'=free_45, P1'=32, Q1_1'=1, R1'=1, D3'=1, E3'=E, F3'=free_93, G3'=32, H3'=0, Q3'=0, J3'=0, [ 32>=free_45 && Q>=1 && 32>=free_93 && 0>=0 ], cost: 1+2*Q 219: f182 -> f222 : Q'=0, J'=-Q+J, Q_1'=1, N1'=E, O1'=free_45, P1'=32, Q1_1'=1, R1'=1, D3'=1, E3'=E, F3'=free_95, G3'=32, Q3'=0, J3'=0, K3'=0, [ 32>=free_45 && Q>=1 && free_95>=33 && 0>=0 ], cost: 1+2*Q 220: f182 -> f222 : Q'=0, J'=-Q+J, Q_1'=1, N1'=E, O1'=free_46, P1'=32, Q1_1'=0, R1'=0, D3'=0, E3'=E, F3'=free_95, G3'=32, Q3'=0, J3'=0, K3'=0, [ 32>=free_46 && Q>=1 && free_95>=33 && 0>=0 ], cost: 1+2*Q 221: f182 -> f222 : Q'=0, J'=-Q+J, Q_1'=1, N1'=E, O1'=free_47, P1'=32, R1'=1, S1'=1, D3'=1, E3'=E, F3'=free_93, G3'=32, H3'=0, Q3'=0, J3'=0, [ free_47>=33 && Q>=1 && 32>=free_93 && 0>=0 ], cost: 1+2*Q 310: f222 -> f222 : G'=1, Q_1'=1+Q_1, T1'=17-Q_1, U1'=free_49, V1'=free_50, W1'=0, X1'=16, Y1'=9, Z1'=1, A2'=1, B2'=1, C2'=free_55, D2'=free_56, E2'=0, F2'=free_59, G2'=free_61, H2'=free_58, Q2'=free_60, J2'=free_62, K2'=1, B3'=free_88, [ 16>=Q_1 && G==1 && 16>=1 && 0>=0 && 4>=1 && 5>=5 && 8>=1 && 0>=0 && 32>=1 && 0>=0 ], cost: 97 311: f222 -> f222 : G'=1, Q_1'=1+Q_1, T1'=17-Q_1, U1'=free_49, V1'=free_50, W1'=0, X1'=16, Y1'=9, Z1'=1, A2'=1, B2'=1, C2'=free_55, D2'=free_56, E2'=0, F2'=free_59, G2'=free_61, H2'=free_58, Q2'=free_60, J2'=free_63, K2'=0, B3'=free_88, [ 16>=Q_1 && G==1 && 16>=1 && 0>=0 && 4>=1 && 5>=5 && 8>=1 && 0>=0 && 32>=1 && 0>=0 ], cost: 97 313: f222 -> f222 : G'=1, Q_1'=1+Q_1, T1'=17-Q_1, U1'=free_49, V1'=free_50, W1'=0, X1'=16, Y1'=9, Z1'=1, A2'=1, B2'=0, C2'=free_55, D2'=free_56, E2'=0, F2'=free_59, G2'=free_61, H2'=free_58, Q2'=free_60, J2'=free_63, K2'=0, B3'=free_88, [ 16>=Q_1 && G==1 && 16>=1 && 0>=0 && 4>=1 && 5>=5 && 8>=1 && 0>=0 && 32>=1 && 0>=0 ], cost: 97 314: f222 -> f222 : G'=1, Q_1'=1+Q_1, T1'=17-Q_1, U1'=free_49, V1'=free_50, W1'=0, X1'=16, Y1'=9, Z1'=0, A2'=1, B2'=1, C2'=free_55, D2'=free_56, E2'=0, F2'=free_59, G2'=free_61, H2'=free_58, Q2'=free_60, J2'=free_62, K2'=1, B3'=free_88, [ 16>=Q_1 && G==1 && 16>=1 && 0>=0 && 4>=1 && 5>=5 && 8>=1 && 0>=0 && 32>=1 && 0>=0 ], cost: 97 315: f222 -> f222 : G'=1, Q_1'=1+Q_1, T1'=17-Q_1, U1'=free_49, V1'=free_50, W1'=0, X1'=16, Y1'=9, Z1'=0, A2'=1, B2'=1, C2'=free_55, D2'=free_56, E2'=0, F2'=free_59, G2'=free_61, H2'=free_58, Q2'=free_60, J2'=free_63, K2'=0, B3'=free_88, [ 16>=Q_1 && G==1 && 16>=1 && 0>=0 && 4>=1 && 5>=5 && 8>=1 && 0>=0 && 32>=1 && 0>=0 ], cost: 97 Eliminating 5 self-loops for location f81 Self-Loop 285 has the metering function: 2-Q_1, resulting in the new transition 320. Self-Loop 286 has the metering function: 2-Q_1, resulting in the new transition 321. Self-Loop 288 has the metering function: 2-Q_1, resulting in the new transition 322. Self-Loop 292 has the metering function: 3-Q_1, resulting in the new transition 323. Self-Loop 297 has the metering function: 10-Q_1, resulting in the new transition 324. Found this metering function when nesting loops: meter, Found this metering function when nesting loops: meter_1, Found this metering function when nesting loops: meter_2, Found this metering function when nesting loops: meter_3, and nested parallel self-loops 285 (outer loop) and 323 (inner loop), obtaining the new transitions: 325. Found this metering function when nesting loops: meter_4, and nested parallel self-loops 286 (outer loop) and 323 (inner loop), obtaining the new transitions: 326. Found this metering function when nesting loops: meter_5, and nested parallel self-loops 288 (outer loop) and 323 (inner loop), obtaining the new transitions: 327. Removing the self-loops: 285 286 288 292 297. Eliminating 5 self-loops for location f222 Self-Loop 310 has the metering function: 17-Q_1, resulting in the new transition 328. Self-Loop 311 has the metering function: 17-Q_1, resulting in the new transition 329. Self-Loop 313 has the metering function: 17-Q_1, resulting in the new transition 330. Self-Loop 314 has the metering function: 17-Q_1, resulting in the new transition 331. Self-Loop 315 has the metering function: 17-Q_1, resulting in the new transition 332. Removing the self-loops: 310 311 313 314 315. Removed all Self-loops using metering functions (where possible): Start location: f0 247: f0 -> f81 : B'=0, C'=free, D'=free_2, E'=free_3, F'=free_1, G'=free_2, Q'=0, J'=28, K'=free_1, L'=free_14, M'=32, N'=1, O'=1, Q_1'=1, U3'=1, V3'=free_1, W3'=free_108, X3'=32, Y3'=1, Z3'=1, A4'=1, [ B==0 && 32>=free_14 && 28>=1 && 32>=free_108 && 0>=0 ], cost: 59 248: f0 -> f81 : B'=0, C'=free, D'=free_2, E'=free_3, F'=free_1, G'=free_2, Q'=0, J'=28, K'=free_1, L'=free_14, M'=32, N'=1, O'=1, Q_1'=1, U3'=1, V3'=free_1, W3'=free_109, X3'=32, Y3'=0, Z3'=0, A4'=0, [ B==0 && 32>=free_14 && 28>=1 && 32>=free_109 && 0>=0 ], cost: 59 250: f0 -> f81 : B'=0, C'=free, D'=free_2, E'=free_3, F'=free_1, G'=free_2, Q'=0, J'=28, K'=free_1, L'=free_15, M'=32, N'=0, O'=0, Q_1'=1, U3'=0, V3'=free_1, W3'=free_111, X3'=32, Z3'=0, A4'=0, B4'=0, [ B==0 && 32>=free_15 && 28>=1 && free_111>=33 && 0>=0 ], cost: 59 254: f0 -> f81 : B'=0, C'=free_4, D'=free_6, E'=free_7, F'=free_5, G'=free_6, H'=free_12, Q'=0, J'=28, K'=free_5, L'=free_14, M'=32, N'=1, O'=1, Q_1'=1, U3'=1, V3'=free_5, W3'=free_111, X3'=32, Z3'=0, A4'=0, B4'=0, [ 0>=1+B && 32>=2 && 33>=33 && 32>=free_14 && 28>=1 && free_111>=33 && 0>=0 ], cost: 91 255: f0 -> f81 : B'=0, C'=free_4, D'=free_6, E'=free_7, F'=free_5, G'=free_6, H'=free_12, Q'=0, J'=28, K'=free_5, L'=free_15, M'=32, N'=0, O'=0, Q_1'=1, U3'=0, V3'=free_5, W3'=free_111, X3'=32, Z3'=0, A4'=0, B4'=0, [ 0>=1+B && 32>=2 && 33>=33 && 32>=free_15 && 28>=1 && free_111>=33 && 0>=0 ], cost: 91 182: f0 -> f182 : B'=0, C'=free, D'=free_2, E'=free_3, F'=free_1, G'=free_2, Q'=32, J'=64, [ B==0 ], cost: 2 184: f0 -> f182 : B'=0, C'=free_4, D'=free_6, E'=free_7, F'=free_5, G'=free_6, H'=free_12, Q'=32, J'=64, [ 0>=1+B && 32>=2 && 33>=33 ], cost: 34 186: f0 -> f182 : B'=0, C'=free_8, D'=free_10, E'=free_11, F'=free_9, G'=free_10, H'=free_12, Q'=32, J'=64, [ B>=1 && 32>=2 && 33>=33 ], cost: 34 320: f81 -> [35] : A'=1, Q_1'=2, R'=free_20, T'=0, U'=0, V'=0, W'=16, X'=32, Y'=free_21, Z'=free_22, A1'=free_23, B1'=28, C1'=1, D1'=1, F1'=1, G1'=free_33, H1'=free_34, Q1'=free_35, J1'=28, K1'=1, L1'=1, L3'=1, M3'=free_96, N3'=free_97, O3'=free_98, P3'=28, Q3_1'=1, R3'=1, S3'=1, [ Q_1==1 && 28>=free_23 && 28>=free_35 && 28>=free_98 ], cost: 100-50*Q_1 321: f81 -> [35] : A'=1, Q_1'=2, R'=free_20, T'=0, U'=0, V'=0, W'=16, X'=32, Y'=free_21, Z'=free_22, A1'=free_23, B1'=28, C1'=1, D1'=1, F1'=1, G1'=free_33, H1'=free_34, Q1'=free_35, J1'=28, K1'=1, L1'=1, L3'=1, M3'=free_99, N3'=free_100, O3'=free_101, P3'=28, Q3_1'=0, R3'=0, S3'=0, [ Q_1==1 && 28>=free_23 && 28>=free_35 && 28>=free_101 ], cost: 100-50*Q_1 322: f81 -> [35] : A'=1, Q_1'=2, R'=free_20, T'=0, U'=0, V'=0, W'=16, X'=32, Y'=free_21, Z'=free_22, A1'=free_23, B1'=28, C1'=1, D1'=1, F1'=1, G1'=free_36, H1'=free_37, Q1'=free_38, J1'=28, K1'=0, L1'=0, L3'=0, M3'=free_105, N3'=free_106, O3'=free_107, P3'=28, R3'=0, S3'=0, T3'=0, [ Q_1==1 && 28>=free_23 && 28>=free_38 && free_107>=29 ], cost: 100-50*Q_1 323: f81 -> [35] : A'=2, Q_1'=3, R'=free_19, T'=0, U'=0, V'=0, W'=16, X'=32, Y'=free_21, Z'=free_22, A1'=free_23, B1'=28, C1'=1, D1'=1, F1'=1, G1'=free_33, H1'=free_34, Q1'=free_35, J1'=28, K1'=1, L1'=1, L3'=1, M3'=free_105, N3'=free_106, O3'=free_107, P3'=28, R3'=0, S3'=0, T3'=0, [ Q_1==2 && 28>=free_23 && 28>=free_35 && free_107>=29 ], cost: 153-51*Q_1 324: f81 -> [35] : A'=9, Q_1'=10, R'=free_19, T'=0, U'=0, V'=0, W'=16, X'=32, Y'=free_21, Z'=free_22, A1'=free_23, B1'=28, C1'=1, D1'=1, F1'=1, G1'=free_33, H1'=free_34, Q1'=free_35, J1'=28, K1'=1, L1'=1, L3'=1, M3'=free_105, N3'=free_106, O3'=free_107, P3'=28, R3'=0, S3'=0, T3'=0, [ Q_1==9 && 28>=free_23 && 28>=free_35 && free_107>=29 ], cost: 520-52*Q_1 325: f81 -> [35] : A'=2, Q_1'=3, R'=free_19, T'=0, U'=0, V'=0, W'=16, X'=32, Y'=free_21, Z'=free_22, A1'=free_23, B1'=28, C1'=1, D1'=1, F1'=1, G1'=free_33, H1'=free_34, Q1'=free_35, J1'=28, K1'=1, L1'=1, L3'=1, M3'=free_105, N3'=free_106, O3'=free_107, P3'=28, Q3_1'=1, R3'=0, S3'=0, T3'=0, [ Q_1==1 && 28>=free_23 && 28>=free_35 && 28>=free_98 && 2==2 && 28>=free_23 && 28>=free_35 && free_107>=29 && 2*meter_3==1-Q_1 ], cost: 101*meter_3 326: f81 -> [35] : A'=2, Q_1'=3, R'=free_19, T'=0, U'=0, V'=0, W'=16, X'=32, Y'=free_21, Z'=free_22, A1'=free_23, B1'=28, C1'=1, D1'=1, F1'=1, G1'=free_33, H1'=free_34, Q1'=free_35, J1'=28, K1'=1, L1'=1, L3'=1, M3'=free_105, N3'=free_106, O3'=free_107, P3'=28, Q3_1'=0, R3'=0, S3'=0, T3'=0, [ Q_1==1 && 28>=free_23 && 28>=free_35 && 28>=free_101 && 2==2 && 28>=free_23 && 28>=free_35 && free_107>=29 && 2*meter_4==1-Q_1 ], cost: 101*meter_4 327: f81 -> [35] : A'=2, Q_1'=3, R'=free_19, T'=0, U'=0, V'=0, W'=16, X'=32, Y'=free_21, Z'=free_22, A1'=free_23, B1'=28, C1'=1, D1'=1, F1'=1, G1'=free_33, H1'=free_34, Q1'=free_35, J1'=28, K1'=1, L1'=1, L3'=1, M3'=free_105, N3'=free_106, O3'=free_107, P3'=28, R3'=0, S3'=0, T3'=0, [ Q_1==1 && 28>=free_23 && 28>=free_38 && free_107>=29 && 2==2 && 28>=free_23 && 28>=free_35 && free_107>=29 && 2*meter_5==1-Q_1 ], cost: 101*meter_5 217: f182 -> f222 : Q'=0, J'=-Q+J, Q_1'=1, N1'=E, O1'=free_45, P1'=32, Q1_1'=1, R1'=1, D3'=1, E3'=E, F3'=free_92, G3'=32, H3'=1, Q3'=1, J3'=1, [ 32>=free_45 && Q>=1 && 32>=free_92 && 0>=0 ], cost: 1+2*Q 218: f182 -> f222 : Q'=0, J'=-Q+J, Q_1'=1, N1'=E, O1'=free_45, P1'=32, Q1_1'=1, R1'=1, D3'=1, E3'=E, F3'=free_93, G3'=32, H3'=0, Q3'=0, J3'=0, [ 32>=free_45 && Q>=1 && 32>=free_93 && 0>=0 ], cost: 1+2*Q 219: f182 -> f222 : Q'=0, J'=-Q+J, Q_1'=1, N1'=E, O1'=free_45, P1'=32, Q1_1'=1, R1'=1, D3'=1, E3'=E, F3'=free_95, G3'=32, Q3'=0, J3'=0, K3'=0, [ 32>=free_45 && Q>=1 && free_95>=33 && 0>=0 ], cost: 1+2*Q 220: f182 -> f222 : Q'=0, J'=-Q+J, Q_1'=1, N1'=E, O1'=free_46, P1'=32, Q1_1'=0, R1'=0, D3'=0, E3'=E, F3'=free_95, G3'=32, Q3'=0, J3'=0, K3'=0, [ 32>=free_46 && Q>=1 && free_95>=33 && 0>=0 ], cost: 1+2*Q 221: f182 -> f222 : Q'=0, J'=-Q+J, Q_1'=1, N1'=E, O1'=free_47, P1'=32, R1'=1, S1'=1, D3'=1, E3'=E, F3'=free_93, G3'=32, H3'=0, Q3'=0, J3'=0, [ free_47>=33 && Q>=1 && 32>=free_93 && 0>=0 ], cost: 1+2*Q 328: f222 -> [36] : G'=1, Q_1'=17, T1'=1, U1'=free_49, V1'=free_50, W1'=0, X1'=16, Y1'=9, Z1'=1, A2'=1, B2'=1, C2'=free_55, D2'=free_56, E2'=0, F2'=free_59, G2'=free_61, H2'=free_58, Q2'=free_60, J2'=free_62, K2'=1, B3'=free_88, [ 16>=Q_1 && G==1 ], cost: 1649-97*Q_1 329: f222 -> [36] : G'=1, Q_1'=17, T1'=1, U1'=free_49, V1'=free_50, W1'=0, X1'=16, Y1'=9, Z1'=1, A2'=1, B2'=1, C2'=free_55, D2'=free_56, E2'=0, F2'=free_59, G2'=free_61, H2'=free_58, Q2'=free_60, J2'=free_63, K2'=0, B3'=free_88, [ 16>=Q_1 && G==1 ], cost: 1649-97*Q_1 330: f222 -> [36] : G'=1, Q_1'=17, T1'=1, U1'=free_49, V1'=free_50, W1'=0, X1'=16, Y1'=9, Z1'=1, A2'=1, B2'=0, C2'=free_55, D2'=free_56, E2'=0, F2'=free_59, G2'=free_61, H2'=free_58, Q2'=free_60, J2'=free_63, K2'=0, B3'=free_88, [ 16>=Q_1 && G==1 ], cost: 1649-97*Q_1 331: f222 -> [36] : G'=1, Q_1'=17, T1'=1, U1'=free_49, V1'=free_50, W1'=0, X1'=16, Y1'=9, Z1'=0, A2'=1, B2'=1, C2'=free_55, D2'=free_56, E2'=0, F2'=free_59, G2'=free_61, H2'=free_58, Q2'=free_60, J2'=free_62, K2'=1, B3'=free_88, [ 16>=Q_1 && G==1 ], cost: 1649-97*Q_1 332: f222 -> [36] : G'=1, Q_1'=17, T1'=1, U1'=free_49, V1'=free_50, W1'=0, X1'=16, Y1'=9, Z1'=0, A2'=1, B2'=1, C2'=free_55, D2'=free_56, E2'=0, F2'=free_59, G2'=free_61, H2'=free_58, Q2'=free_60, J2'=free_63, K2'=0, B3'=free_88, [ 16>=Q_1 && G==1 ], cost: 1649-97*Q_1 74: [35] -> f182 : Q'=32, J'=64, [ Q_1>=17 ], cost: 1 Applied chaining over branches and pruning: Start location: f0 182: f0 -> f182 : B'=0, C'=free, D'=free_2, E'=free_3, F'=free_1, G'=free_2, Q'=32, J'=64, [ B==0 ], cost: 2 184: f0 -> f182 : B'=0, C'=free_4, D'=free_6, E'=free_7, F'=free_5, G'=free_6, H'=free_12, Q'=32, J'=64, [ 0>=1+B && 32>=2 && 33>=33 ], cost: 34 186: f0 -> f182 : B'=0, C'=free_8, D'=free_10, E'=free_11, F'=free_9, G'=free_10, H'=free_12, Q'=32, J'=64, [ B>=1 && 32>=2 && 33>=33 ], cost: 34 333: f0 -> [35] : A'=1, B'=0, C'=free, D'=free_2, E'=free_3, F'=free_1, G'=free_2, Q'=0, J'=28, K'=free_1, L'=free_14, M'=32, N'=1, O'=1, Q_1'=2, R'=free_20, T'=0, U'=0, V'=0, W'=16, X'=32, Y'=free_21, Z'=free_22, A1'=free_23, B1'=28, C1'=1, D1'=1, F1'=1, G1'=free_33, H1'=free_34, Q1'=free_35, J1'=28, K1'=1, L1'=1, L3'=1, M3'=free_96, N3'=free_97, O3'=free_98, P3'=28, Q3_1'=1, R3'=1, S3'=1, U3'=1, V3'=free_1, W3'=free_108, X3'=32, Y3'=1, Z3'=1, A4'=1, [ B==0 && 32>=free_14 && 28>=1 && 32>=free_108 && 0>=0 && 1==1 && 28>=free_23 && 28>=free_35 && 28>=free_98 ], cost: 109 334: f0 -> [35] : A'=1, B'=0, C'=free, D'=free_2, E'=free_3, F'=free_1, G'=free_2, Q'=0, J'=28, K'=free_1, L'=free_14, M'=32, N'=1, O'=1, Q_1'=2, R'=free_20, T'=0, U'=0, V'=0, W'=16, X'=32, Y'=free_21, Z'=free_22, A1'=free_23, B1'=28, C1'=1, D1'=1, F1'=1, G1'=free_33, H1'=free_34, Q1'=free_35, J1'=28, K1'=1, L1'=1, L3'=1, M3'=free_99, N3'=free_100, O3'=free_101, P3'=28, Q3_1'=0, R3'=0, S3'=0, U3'=1, V3'=free_1, W3'=free_108, X3'=32, Y3'=1, Z3'=1, A4'=1, [ B==0 && 32>=free_14 && 28>=1 && 32>=free_108 && 0>=0 && 1==1 && 28>=free_23 && 28>=free_35 && 28>=free_101 ], cost: 109 340: f0 -> [35] : A'=1, B'=0, C'=free, D'=free_2, E'=free_3, F'=free_1, G'=free_2, Q'=0, J'=28, K'=free_1, L'=free_14, M'=32, N'=1, O'=1, Q_1'=2, R'=free_20, T'=0, U'=0, V'=0, W'=16, X'=32, Y'=free_21, Z'=free_22, A1'=free_23, B1'=28, C1'=1, D1'=1, F1'=1, G1'=free_33, H1'=free_34, Q1'=free_35, J1'=28, K1'=1, L1'=1, L3'=1, M3'=free_99, N3'=free_100, O3'=free_101, P3'=28, Q3_1'=0, R3'=0, S3'=0, U3'=1, V3'=free_1, W3'=free_109, X3'=32, Y3'=0, Z3'=0, A4'=0, [ B==0 && 32>=free_14 && 28>=1 && 32>=free_109 && 0>=0 && 1==1 && 28>=free_23 && 28>=free_35 && 28>=free_101 ], cost: 109 347: f0 -> [35] : A'=1, B'=0, C'=free, D'=free_2, E'=free_3, F'=free_1, G'=free_2, Q'=0, J'=28, K'=free_1, L'=free_15, M'=32, N'=0, O'=0, Q_1'=2, R'=free_20, T'=0, U'=0, V'=0, W'=16, X'=32, Y'=free_21, Z'=free_22, A1'=free_23, B1'=28, C1'=1, D1'=1, F1'=1, G1'=free_36, H1'=free_37, Q1'=free_38, J1'=28, K1'=0, L1'=0, L3'=0, M3'=free_105, N3'=free_106, O3'=free_107, P3'=28, R3'=0, S3'=0, T3'=0, U3'=0, V3'=free_1, W3'=free_111, X3'=32, Z3'=0, A4'=0, B4'=0, [ B==0 && 32>=free_15 && 28>=1 && free_111>=33 && 0>=0 && 1==1 && 28>=free_23 && 28>=free_38 && free_107>=29 ], cost: 109 357: f0 -> [35] : A'=1, B'=0, C'=free_4, D'=free_6, E'=free_7, F'=free_5, G'=free_6, H'=free_12, Q'=0, J'=28, K'=free_5, L'=free_15, M'=32, N'=0, O'=0, Q_1'=2, R'=free_20, T'=0, U'=0, V'=0, W'=16, X'=32, Y'=free_21, Z'=free_22, A1'=free_23, B1'=28, C1'=1, D1'=1, F1'=1, G1'=free_33, H1'=free_34, Q1'=free_35, J1'=28, K1'=1, L1'=1, L3'=1, M3'=free_96, N3'=free_97, O3'=free_98, P3'=28, Q3_1'=1, R3'=1, S3'=1, U3'=0, V3'=free_5, W3'=free_111, X3'=32, Z3'=0, A4'=0, B4'=0, [ 0>=1+B && 32>=2 && 33>=33 && 32>=free_15 && 28>=1 && free_111>=33 && 0>=0 && 1==1 && 28>=free_23 && 28>=free_35 && 28>=free_98 ], cost: 141 363: f182 -> [36] : G'=1, Q'=0, J'=-Q+J, Q_1'=17, N1'=E, O1'=free_45, P1'=32, Q1_1'=1, R1'=1, T1'=1, U1'=free_49, V1'=free_50, W1'=0, X1'=16, Y1'=9, Z1'=1, A2'=1, B2'=1, C2'=free_55, D2'=free_56, E2'=0, F2'=free_59, G2'=free_61, H2'=free_58, Q2'=free_60, J2'=free_62, K2'=1, B3'=free_88, D3'=1, E3'=E, F3'=free_92, G3'=32, H3'=1, Q3'=1, J3'=1, [ 32>=free_45 && Q>=1 && 32>=free_92 && 0>=0 && 16>=1 && G==1 ], cost: 1553+2*Q 364: f182 -> [36] : G'=1, Q'=0, J'=-Q+J, Q_1'=17, N1'=E, O1'=free_45, P1'=32, Q1_1'=1, R1'=1, T1'=1, U1'=free_49, V1'=free_50, W1'=0, X1'=16, Y1'=9, Z1'=1, A2'=1, B2'=1, C2'=free_55, D2'=free_56, E2'=0, F2'=free_59, G2'=free_61, H2'=free_58, Q2'=free_60, J2'=free_63, K2'=0, B3'=free_88, D3'=1, E3'=E, F3'=free_92, G3'=32, H3'=1, Q3'=1, J3'=1, [ 32>=free_45 && Q>=1 && 32>=free_92 && 0>=0 && 16>=1 && G==1 ], cost: 1553+2*Q 366: f182 -> [36] : G'=1, Q'=0, J'=-Q+J, Q_1'=17, N1'=E, O1'=free_45, P1'=32, Q1_1'=1, R1'=1, T1'=1, U1'=free_49, V1'=free_50, W1'=0, X1'=16, Y1'=9, Z1'=0, A2'=1, B2'=1, C2'=free_55, D2'=free_56, E2'=0, F2'=free_59, G2'=free_61, H2'=free_58, Q2'=free_60, J2'=free_62, K2'=1, B3'=free_88, D3'=1, E3'=E, F3'=free_92, G3'=32, H3'=1, Q3'=1, J3'=1, [ 32>=free_45 && Q>=1 && 32>=free_92 && 0>=0 && 16>=1 && G==1 ], cost: 1553+2*Q 370: f182 -> [36] : G'=1, Q'=0, J'=-Q+J, Q_1'=17, N1'=E, O1'=free_45, P1'=32, Q1_1'=1, R1'=1, T1'=1, U1'=free_49, V1'=free_50, W1'=0, X1'=16, Y1'=9, Z1'=1, A2'=1, B2'=0, C2'=free_55, D2'=free_56, E2'=0, F2'=free_59, G2'=free_61, H2'=free_58, Q2'=free_60, J2'=free_63, K2'=0, B3'=free_88, D3'=1, E3'=E, F3'=free_93, G3'=32, H3'=0, Q3'=0, J3'=0, [ 32>=free_45 && Q>=1 && 32>=free_93 && 0>=0 && 16>=1 && G==1 ], cost: 1553+2*Q 375: f182 -> [36] : G'=1, Q'=0, J'=-Q+J, Q_1'=17, N1'=E, O1'=free_45, P1'=32, Q1_1'=1, R1'=1, T1'=1, U1'=free_49, V1'=free_50, W1'=0, X1'=16, Y1'=9, Z1'=1, A2'=1, B2'=0, C2'=free_55, D2'=free_56, E2'=0, F2'=free_59, G2'=free_61, H2'=free_58, Q2'=free_60, J2'=free_63, K2'=0, B3'=free_88, D3'=1, E3'=E, F3'=free_95, G3'=32, Q3'=0, J3'=0, K3'=0, [ 32>=free_45 && Q>=1 && free_95>=33 && 0>=0 && 16>=1 && G==1 ], cost: 1553+2*Q 74: [35] -> f182 : Q'=32, J'=64, [ Q_1>=17 ], cost: 1 Applied chaining over branches and pruning: Start location: f0 182: f0 -> f182 : B'=0, C'=free, D'=free_2, E'=free_3, F'=free_1, G'=free_2, Q'=32, J'=64, [ B==0 ], cost: 2 184: f0 -> f182 : B'=0, C'=free_4, D'=free_6, E'=free_7, F'=free_5, G'=free_6, H'=free_12, Q'=32, J'=64, [ 0>=1+B && 32>=2 && 33>=33 ], cost: 34 186: f0 -> f182 : B'=0, C'=free_8, D'=free_10, E'=free_11, F'=free_9, G'=free_10, H'=free_12, Q'=32, J'=64, [ B>=1 && 32>=2 && 33>=33 ], cost: 34 363: f182 -> [36] : G'=1, Q'=0, J'=-Q+J, Q_1'=17, N1'=E, O1'=free_45, P1'=32, Q1_1'=1, R1'=1, T1'=1, U1'=free_49, V1'=free_50, W1'=0, X1'=16, Y1'=9, Z1'=1, A2'=1, B2'=1, C2'=free_55, D2'=free_56, E2'=0, F2'=free_59, G2'=free_61, H2'=free_58, Q2'=free_60, J2'=free_62, K2'=1, B3'=free_88, D3'=1, E3'=E, F3'=free_92, G3'=32, H3'=1, Q3'=1, J3'=1, [ 32>=free_45 && Q>=1 && 32>=free_92 && 0>=0 && 16>=1 && G==1 ], cost: 1553+2*Q 364: f182 -> [36] : G'=1, Q'=0, J'=-Q+J, Q_1'=17, N1'=E, O1'=free_45, P1'=32, Q1_1'=1, R1'=1, T1'=1, U1'=free_49, V1'=free_50, W1'=0, X1'=16, Y1'=9, Z1'=1, A2'=1, B2'=1, C2'=free_55, D2'=free_56, E2'=0, F2'=free_59, G2'=free_61, H2'=free_58, Q2'=free_60, J2'=free_63, K2'=0, B3'=free_88, D3'=1, E3'=E, F3'=free_92, G3'=32, H3'=1, Q3'=1, J3'=1, [ 32>=free_45 && Q>=1 && 32>=free_92 && 0>=0 && 16>=1 && G==1 ], cost: 1553+2*Q 366: f182 -> [36] : G'=1, Q'=0, J'=-Q+J, Q_1'=17, N1'=E, O1'=free_45, P1'=32, Q1_1'=1, R1'=1, T1'=1, U1'=free_49, V1'=free_50, W1'=0, X1'=16, Y1'=9, Z1'=0, A2'=1, B2'=1, C2'=free_55, D2'=free_56, E2'=0, F2'=free_59, G2'=free_61, H2'=free_58, Q2'=free_60, J2'=free_62, K2'=1, B3'=free_88, D3'=1, E3'=E, F3'=free_92, G3'=32, H3'=1, Q3'=1, J3'=1, [ 32>=free_45 && Q>=1 && 32>=free_92 && 0>=0 && 16>=1 && G==1 ], cost: 1553+2*Q 370: f182 -> [36] : G'=1, Q'=0, J'=-Q+J, Q_1'=17, N1'=E, O1'=free_45, P1'=32, Q1_1'=1, R1'=1, T1'=1, U1'=free_49, V1'=free_50, W1'=0, X1'=16, Y1'=9, Z1'=1, A2'=1, B2'=0, C2'=free_55, D2'=free_56, E2'=0, F2'=free_59, G2'=free_61, H2'=free_58, Q2'=free_60, J2'=free_63, K2'=0, B3'=free_88, D3'=1, E3'=E, F3'=free_93, G3'=32, H3'=0, Q3'=0, J3'=0, [ 32>=free_45 && Q>=1 && 32>=free_93 && 0>=0 && 16>=1 && G==1 ], cost: 1553+2*Q 375: f182 -> [36] : G'=1, Q'=0, J'=-Q+J, Q_1'=17, N1'=E, O1'=free_45, P1'=32, Q1_1'=1, R1'=1, T1'=1, U1'=free_49, V1'=free_50, W1'=0, X1'=16, Y1'=9, Z1'=1, A2'=1, B2'=0, C2'=free_55, D2'=free_56, E2'=0, F2'=free_59, G2'=free_61, H2'=free_58, Q2'=free_60, J2'=free_63, K2'=0, B3'=free_88, D3'=1, E3'=E, F3'=free_95, G3'=32, Q3'=0, J3'=0, K3'=0, [ 32>=free_45 && Q>=1 && free_95>=33 && 0>=0 && 16>=1 && G==1 ], cost: 1553+2*Q Applied chaining over branches and pruning: Start location: f0 Final control flow graph problem, now checking costs for infinitely many models: Start location: f0 Computing complexity for remaining 0 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),?)