Trying to load file: main.koat Initial Control flow graph problem: Start location: f0 0: f0 -> f1 : [], cost: 1 1: f1 -> f2 : C'=1+B, [ A>=1+B ], cost: 1 2: f1 -> f2 : C'=-1+B, [ B>=1+A ], cost: 1 3: f1 -> f2 : A'=B, C'=B, [ B==A ], cost: 1 4: f2 -> f3 : E'=1+D, [ B>=1+D ], cost: 1 5: f2 -> f3 : E'=-1+D, [ D>=1+B ], cost: 1 6: f2 -> f3 : D'=B, E'=B, [ B==D ], cost: 1 7: f3 -> f4 : G'=1+F, [ 2>=F+D ], cost: 1 8: f3 -> f4 : G'=-1+F, [ F+D>=4 ], cost: 1 9: f3 -> f4 : F'=3-D, G'=3-D, [ F+D==3 ], cost: 1 10: f4 -> f5 : Q'=1+H, [ 2>=H+F ], cost: 1 11: f4 -> f5 : Q'=-1+H, [ H+F>=4 ], cost: 1 12: f4 -> f5 : H'=3-F, Q'=3-F, [ H+F==3 ], cost: 1 13: f5 -> f6 : K'=1+J, [ H>=1+J ], cost: 1 14: f5 -> f6 : K'=-1+J, [ J>=1+H ], cost: 1 15: f5 -> f6 : J'=H, K'=H, [ H==J ], cost: 1 16: f6 -> f7 : N'=1+L, [ 0>=1+L && M>=1+L ], cost: 1 17: f6 -> f7 : N'=-1+L, [ L>=1 ], cost: 1 18: f6 -> f7 : N'=-1+L, [ L>=1+M ], cost: 1 19: f6 -> f7 : L'=0, N'=0, [ M>=0 && L==0 ], cost: 1 20: f6 -> f7 : M'=L, N'=L, [ 0>=1+M && L==M ], cost: 1 21: f7 -> f8 : P'=1+O, [ L>=1+O ], cost: 1 22: f7 -> f8 : P'=-1+O, [ O>=1+L ], cost: 1 23: f7 -> f8 : O'=L, P'=L, [ L==O ], cost: 1 24: f8 -> f9 : R'=1+Q_1, [ O+J>=1+2*Q_1 ], cost: 1 25: f8 -> f9 : R'=-1+Q_1, [ 2*Q_1>=2+O+J ], cost: 1 26: f8 -> f9 : R'=Q_1, [ 2*Q_1>=O+J && 1+O+J>=2*Q_1 ], cost: 1 27: f9 -> f10 : T'=1+S, [ L>=1+S ], cost: 1 28: f9 -> f10 : T'=-1+S, [ S>=1+L ], cost: 1 29: f9 -> f10 : S'=L, T'=L, [ L==S ], cost: 1 30: f10 -> f11 : V'=1+U, [ 2>=U+S ], cost: 1 31: f10 -> f11 : V'=-1+U, [ U+S>=4 ], cost: 1 32: f10 -> f11 : U'=3-S, V'=3-S, [ U+S==3 ], cost: 1 33: f11 -> f12 : X'=1+A, [ 1+W>=2*A ], cost: 1 34: f11 -> f12 : X'=-1+A, [ 2*A>=4+W ], cost: 1 35: f11 -> f12 : X'=A, [ 2*A>=2+W && 3+W>=2*A ], cost: 1 36: f12 -> f13 : Z'=1+M, [ 1+Y>=2*M ], cost: 1 37: f12 -> f13 : Z'=-1+M, [ 2*M>=4+Y ], cost: 1 38: f12 -> f13 : Z'=M, [ 3+Y>=2*M && 2*M>=2+Y ], cost: 1 39: f13 -> f14 : C1'=1+B1, [ A1>=1+B1 ], cost: 1 40: f13 -> f14 : C1'=-1+B1, [ B1>=1+A1 ], cost: 1 41: f13 -> f14 : A1'=B1, C1'=B1, [ B1==A1 ], cost: 1 42: f14 -> f15 : E1'=1+D1, [ B1>=1+D1 ], cost: 1 43: f14 -> f15 : E1'=-1+D1, [ D1>=1+B1 ], cost: 1 44: f14 -> f15 : D1'=B1, E1'=B1, [ B1==D1 ], cost: 1 45: f15 -> f16 : G1'=1+F1, [ 2>=F1+D1 ], cost: 1 46: f15 -> f16 : G1'=-1+F1, [ F1+D1>=4 ], cost: 1 47: f15 -> f16 : F1'=3-D1, G1'=3-D1, [ F1+D1==3 ], cost: 1 48: f16 -> f17 : Q1'=1+H1, [ 2>=H1+F1 ], cost: 1 49: f16 -> f17 : Q1'=-1+H1, [ H1+F1>=4 ], cost: 1 50: f16 -> f17 : H1'=3-F1, Q1'=3-F1, [ H1+F1==3 ], cost: 1 51: f17 -> f18 : K1'=1+J1, [ H1>=1+J1 ], cost: 1 52: f17 -> f18 : K1'=-1+J1, [ J1>=1+H1 ], cost: 1 53: f17 -> f18 : J1'=H1, K1'=H1, [ H1==J1 ], cost: 1 54: f18 -> f19 : N1'=1+L1, [ 1>=L1 && M1>=1+L1 ], cost: 1 55: f18 -> f19 : N1'=-1+L1, [ L1>=3 ], cost: 1 56: f18 -> f19 : N1'=-1+L1, [ L1>=1+M1 ], cost: 1 57: f18 -> f19 : L1'=2, N1'=2, [ M1>=2 && L1==2 ], cost: 1 58: f18 -> f19 : M1'=L1, N1'=L1, [ 1>=M1 && L1==M1 ], cost: 1 59: f19 -> f20 : P1'=1+O1, [ L1>=1+O1 ], cost: 1 60: f19 -> f20 : P1'=-1+O1, [ O1>=1+L1 ], cost: 1 61: f19 -> f20 : O1'=L1, P1'=L1, [ L1==O1 ], cost: 1 62: f20 -> f21 : Q1_1'=1+Y, [ O1+J1>=1+2*Y ], cost: 1 63: f20 -> f21 : Q1_1'=-1+Y, [ 2*Y>=2+O1+J1 ], cost: 1 64: f20 -> f21 : Q1_1'=Y, [ 2*Y>=O1+J1 && 1+O1+J1>=2*Y ], cost: 1 65: f21 -> f22 : S1'=1+R1, [ L1>=1+R1 ], cost: 1 66: f21 -> f22 : S1'=-1+R1, [ R1>=1+L1 ], cost: 1 67: f21 -> f22 : R1'=L1, S1'=L1, [ L1==R1 ], cost: 1 68: f22 -> f23 : T1'=1+W, [ 2>=R1+W ], cost: 1 69: f22 -> f23 : T1'=-1+W, [ R1+W>=4 ], cost: 1 70: f22 -> f23 : W'=3-R1, T1'=3-R1, [ R1+W==3 ], cost: 1 71: f23 -> f24 : V1'=1+A1, [ U+U1>=2+2*A1 ], cost: 1 72: f23 -> f24 : V1'=-1+A1, [ 2*A1>=1+U+U1 ], cost: 1 73: f23 -> f24 : V1'=A1, [ 1+2*A1>=U+U1 && U+U1>=2*A1 ], cost: 1 74: f24 -> f25 : X1'=1+M1, [ Q_1+W1>=1+2*M1 ], cost: 1 75: f24 -> f25 : X1'=-1+M1, [ 2*M1>=2+Q_1+W1 ], cost: 1 76: f24 -> f25 : X1'=M1, [ 1+Q_1+W1>=2*M1 && 2*M1>=Q_1+W1 ], cost: 1 77: f25 -> f26 : A2'=1+Z1, [ Y1>=1+Z1 ], cost: 1 78: f25 -> f26 : A2'=-1+Z1, [ Z1>=1+Y1 ], cost: 1 79: f25 -> f26 : Y1'=Z1, A2'=Z1, [ Z1==Y1 ], cost: 1 80: f26 -> f27 : C2'=1+B2, [ Z1>=1+B2 ], cost: 1 81: f26 -> f27 : C2'=-1+B2, [ B2>=1+Z1 ], cost: 1 82: f26 -> f27 : B2'=Z1, C2'=Z1, [ Z1==B2 ], cost: 1 83: f27 -> f28 : E2'=1+D2, [ 2>=D2+B2 ], cost: 1 84: f27 -> f28 : E2'=-1+D2, [ D2+B2>=4 ], cost: 1 85: f27 -> f28 : D2'=3-B2, E2'=3-B2, [ D2+B2==3 ], cost: 1 86: f28 -> f29 : G2'=1+F2, [ 2>=D2+F2 ], cost: 1 87: f28 -> f29 : G2'=-1+F2, [ D2+F2>=4 ], cost: 1 88: f28 -> f29 : F2'=3-D2, G2'=3-D2, [ D2+F2==3 ], cost: 1 89: f29 -> f30 : Q2'=1+H2, [ F2>=1+H2 ], cost: 1 90: f29 -> f30 : Q2'=-1+H2, [ H2>=1+F2 ], cost: 1 91: f29 -> f30 : H2'=F2, Q2'=F2, [ F2==H2 ], cost: 1 92: f30 -> f31 : L2'=1+J2, [ 2>=J2 && K2>=1+J2 ], cost: 1 93: f30 -> f31 : L2'=-1+J2, [ J2>=4 ], cost: 1 94: f30 -> f31 : L2'=-1+J2, [ J2>=1+K2 ], cost: 1 95: f30 -> f31 : J2'=3, L2'=3, [ K2>=3 && J2==3 ], cost: 1 96: f30 -> f31 : K2'=J2, L2'=J2, [ 2>=K2 && J2==K2 ], cost: 1 97: f31 -> f32 : N2'=1+M2, [ J2>=1+M2 ], cost: 1 98: f31 -> f32 : N2'=-1+M2, [ M2>=1+J2 ], cost: 1 99: f31 -> f32 : M2'=J2, N2'=J2, [ J2==M2 ], cost: 1 100: f32 -> f33 : O2'=1+W1, [ M2+H2>=1+2*W1 ], cost: 1 101: f32 -> f33 : O2'=-1+W1, [ 2*W1>=2+M2+H2 ], cost: 1 102: f32 -> f33 : O2'=W1, [ 2*W1>=M2+H2 && 1+M2+H2>=2*W1 ], cost: 1 103: f33 -> f34 : Q2_1'=1+P2, [ J2>=1+P2 ], cost: 1 104: f33 -> f34 : Q2_1'=-1+P2, [ P2>=1+J2 ], cost: 1 105: f33 -> f34 : P2'=J2, Q2_1'=J2, [ J2==P2 ], cost: 1 106: f34 -> f35 : R2'=1+U1, [ 2>=P2+U1 ], cost: 1 107: f34 -> f35 : R2'=-1+U1, [ P2+U1>=4 ], cost: 1 108: f34 -> f35 : U1'=3-P2, R2'=3-P2, [ P2+U1==3 ], cost: 1 109: f35 -> f36 : T2'=1+Y1, [ S2+W>=2+2*Y1 ], cost: 1 110: f35 -> f36 : T2'=-1+Y1, [ 2*Y1>=1+S2+W ], cost: 1 111: f35 -> f36 : T2'=Y1, [ 1+2*Y1>=S2+W && S2+W>=2*Y1 ], cost: 1 112: f36 -> f37 : V2'=1+K2, [ Y+U2>=1+2*K2 ], cost: 1 113: f36 -> f37 : V2'=-1+K2, [ 2*K2>=2+Y+U2 ], cost: 1 114: f36 -> f37 : V2'=K2, [ 1+Y+U2>=2*K2 && 2*K2>=Y+U2 ], cost: 1 115: f37 -> f38 : Y2'=1+X2, [ W2>=1+X2 ], cost: 1 116: f37 -> f38 : Y2'=-1+X2, [ X2>=1+W2 ], cost: 1 117: f37 -> f38 : W2'=X2, Y2'=X2, [ X2==W2 ], cost: 1 118: f38 -> f39 : A3'=1+Z2, [ X2>=1+Z2 ], cost: 1 119: f38 -> f39 : A3'=-1+Z2, [ Z2>=1+X2 ], cost: 1 120: f38 -> f39 : Z2'=X2, A3'=X2, [ X2==Z2 ], cost: 1 121: f39 -> f40 : C3'=1+B3, [ 2>=Z2+B3 ], cost: 1 122: f39 -> f40 : C3'=-1+B3, [ Z2+B3>=4 ], cost: 1 123: f39 -> f40 : B3'=3-Z2, C3'=3-Z2, [ Z2+B3==3 ], cost: 1 124: f40 -> f41 : E3'=1+D3, [ 2>=D3+B3 ], cost: 1 125: f40 -> f41 : E3'=-1+D3, [ D3+B3>=4 ], cost: 1 126: f40 -> f41 : D3'=3-B3, E3'=3-B3, [ D3+B3==3 ], cost: 1 127: f41 -> f42 : G3'=1+F3, [ D3>=1+F3 ], cost: 1 128: f41 -> f42 : G3'=-1+F3, [ F3>=1+D3 ], cost: 1 129: f41 -> f42 : F3'=D3, G3'=D3, [ D3==F3 ], cost: 1 130: f42 -> f43 : J3'=1+H3, [ 2>=H3 && Q3>=1+H3 ], cost: 1 131: f42 -> f43 : J3'=-1+H3, [ H3>=4 ], cost: 1 132: f42 -> f43 : J3'=-1+H3, [ H3>=1+Q3 ], cost: 1 133: f42 -> f43 : H3'=3, J3'=3, [ Q3>=3 && H3==3 ], cost: 1 134: f42 -> f43 : Q3'=H3, J3'=H3, [ 2>=Q3 && H3==Q3 ], cost: 1 135: f43 -> f44 : L3'=1+K3, [ H3>=1+K3 ], cost: 1 136: f43 -> f44 : L3'=-1+K3, [ K3>=1+H3 ], cost: 1 137: f43 -> f44 : K3'=H3, L3'=H3, [ H3==K3 ], cost: 1 138: f44 -> f45 : M3'=1+U2, [ F3+K3>=1+2*U2 ], cost: 1 139: f44 -> f45 : M3'=-1+U2, [ 2*U2>=2+F3+K3 ], cost: 1 140: f44 -> f45 : M3'=U2, [ 2*U2>=F3+K3 && 1+F3+K3>=2*U2 ], cost: 1 141: f45 -> f46 : O3'=1+N3, [ H3>=1+N3 ], cost: 1 142: f45 -> f46 : O3'=-1+N3, [ N3>=1+H3 ], cost: 1 143: f45 -> f46 : N3'=H3, O3'=H3, [ H3==N3 ], cost: 1 144: f46 -> f47 : P3'=1+S2, [ 2>=S2+N3 ], cost: 1 145: f46 -> f47 : P3'=-1+S2, [ S2+N3>=4 ], cost: 1 146: f46 -> f47 : S2'=3-N3, P3'=3-N3, [ S2+N3==3 ], cost: 1 147: f47 -> f48 : R3'=1+W2, [ U1+Q3_1>=2+2*W2 ], cost: 1 148: f47 -> f48 : R3'=-1+W2, [ 2*W2>=1+U1+Q3_1 ], cost: 1 149: f47 -> f48 : R3'=W2, [ 1+2*W2>=U1+Q3_1 && U1+Q3_1>=2*W2 ], cost: 1 150: f48 -> f49 : T3'=1+Q3, [ S3+W1>=1+2*Q3 ], cost: 1 151: f48 -> f49 : T3'=-1+Q3, [ 2*Q3>=2+S3+W1 ], cost: 1 152: f48 -> f49 : T3'=Q3, [ 1+S3+W1>=2*Q3 && 2*Q3>=S3+W1 ], cost: 1 153: f49 -> f50 : W3'=1+V3, [ U3>=1+V3 ], cost: 1 154: f49 -> f50 : W3'=-1+V3, [ V3>=1+U3 ], cost: 1 155: f49 -> f50 : U3'=V3, W3'=V3, [ V3==U3 ], cost: 1 156: f50 -> f51 : Y3'=1+X3, [ V3>=1+X3 ], cost: 1 157: f50 -> f51 : Y3'=-1+X3, [ X3>=1+V3 ], cost: 1 158: f50 -> f51 : X3'=V3, Y3'=V3, [ V3==X3 ], cost: 1 159: f51 -> f52 : A4'=1+Z3, [ 2>=Z3+X3 ], cost: 1 160: f51 -> f52 : A4'=-1+Z3, [ Z3+X3>=4 ], cost: 1 161: f51 -> f52 : Z3'=3-X3, A4'=3-X3, [ Z3+X3==3 ], cost: 1 162: f52 -> f53 : C4'=1+B4, [ 2>=Z3+B4 ], cost: 1 163: f52 -> f53 : C4'=-1+B4, [ Z3+B4>=4 ], cost: 1 164: f52 -> f53 : B4'=3-Z3, C4'=3-Z3, [ Z3+B4==3 ], cost: 1 165: f53 -> f54 : E4'=1+D4, [ B4>=1+D4 ], cost: 1 166: f53 -> f54 : E4'=-1+D4, [ D4>=1+B4 ], cost: 1 167: f53 -> f54 : D4'=B4, E4'=B4, [ B4==D4 ], cost: 1 168: f54 -> f55 : H4'=1+F4, [ 2>=F4 && G4>=1+F4 ], cost: 1 169: f54 -> f55 : H4'=-1+F4, [ F4>=4 ], cost: 1 170: f54 -> f55 : H4'=-1+F4, [ F4>=1+G4 ], cost: 1 171: f54 -> f55 : F4'=3, H4'=3, [ G4>=3 && F4==3 ], cost: 1 172: f54 -> f55 : G4'=F4, H4'=F4, [ 2>=G4 && F4==G4 ], cost: 1 173: f55 -> f56 : J4'=1+Q4, [ F4>=1+Q4 ], cost: 1 174: f55 -> f56 : J4'=-1+Q4, [ Q4>=1+F4 ], cost: 1 175: f55 -> f56 : Q4'=F4, J4'=F4, [ F4==Q4 ], cost: 1 176: f56 -> f57 : K4'=1+S3, [ Q4+D4>=1+2*S3 ], cost: 1 177: f56 -> f57 : K4'=-1+S3, [ 2*S3>=2+Q4+D4 ], cost: 1 178: f56 -> f57 : K4'=S3, [ 2*S3>=Q4+D4 && 1+Q4+D4>=2*S3 ], cost: 1 179: f57 -> f58 : M4'=1+L4, [ F4>=1+L4 ], cost: 1 180: f57 -> f58 : M4'=-1+L4, [ L4>=1+F4 ], cost: 1 181: f57 -> f58 : L4'=F4, M4'=F4, [ F4==L4 ], cost: 1 182: f58 -> f59 : N4'=1+Q3_1, [ 2>=L4+Q3_1 ], cost: 1 183: f58 -> f59 : N4'=-1+Q3_1, [ L4+Q3_1>=4 ], cost: 1 184: f58 -> f59 : Q3_1'=3-L4, N4'=3-L4, [ L4+Q3_1==3 ], cost: 1 185: f59 -> f60 : O4'=1+U3, [ S2>=2+2*U3 ], cost: 1 186: f59 -> f60 : O4'=-1+U3, [ 2*U3>=1+S2 ], cost: 1 187: f59 -> f60 : O4'=U3, [ 1+2*U3>=S2 && S2>=2*U3 ], cost: 1 188: f60 -> f1 : A'=X, B'=C, D'=E, F'=G, H'=Q, J'=K, L'=N, M'=Z, O'=P, Q_1'=R, S'=T, U'=V, W'=T1, Y'=Q1_1, A1'=V1, B1'=C1, D1'=E1, F1'=G1, H1'=Q1, J1'=K1, L1'=N1, M1'=X1, O1'=P1, R1'=S1, U1'=R2, W1'=O2, Y1'=T2, Z1'=A2, B2'=C2, D2'=E2, F2'=G2, H2'=Q2, J2'=L2, K2'=V2, M2'=N2, P2'=Q2_1, S2'=P3, U2'=M3, W2'=R3, X2'=Y2, Z2'=A3, B3'=C3, D3'=E3, F3'=G3, H3'=J3, Q3'=T3, K3'=L3, N3'=O3, Q3_1'=N4, S3'=K4, U3'=O4, V3'=W3, X3'=Y3, Z3'=A4, B4'=C4, D4'=E4, F4'=H4, G4'=1+G4, Q4'=J4, L4'=M4, P4'=1+G4, [ 1+U2>=2*G4 ], cost: 1 189: f60 -> f1 : A'=X, B'=C, D'=E, F'=G, H'=Q, J'=K, L'=N, M'=Z, O'=P, Q_1'=R, S'=T, U'=V, W'=T1, Y'=Q1_1, A1'=V1, B1'=C1, D1'=E1, F1'=G1, H1'=Q1, J1'=K1, L1'=N1, M1'=X1, O1'=P1, R1'=S1, U1'=R2, W1'=O2, Y1'=T2, Z1'=A2, B2'=C2, D2'=E2, F2'=G2, H2'=Q2, J2'=L2, K2'=V2, M2'=N2, P2'=Q2_1, S2'=P3, U2'=M3, W2'=R3, X2'=Y2, Z2'=A3, B3'=C3, D3'=E3, F3'=G3, H3'=J3, Q3'=T3, K3'=L3, N3'=O3, Q3_1'=N4, S3'=K4, U3'=O4, V3'=W3, X3'=Y3, Z3'=A4, B4'=C4, D4'=E4, F4'=H4, G4'=-1+G4, Q4'=J4, L4'=M4, P4'=-1+G4, [ 2*G4>=4+U2 ], cost: 1 190: f60 -> f1 : A'=X, B'=C, D'=E, F'=G, H'=Q, J'=K, L'=N, M'=Z, O'=P, Q_1'=R, S'=T, U'=V, W'=T1, Y'=Q1_1, A1'=V1, B1'=C1, D1'=E1, F1'=G1, H1'=Q1, J1'=K1, L1'=N1, M1'=X1, O1'=P1, R1'=S1, U1'=R2, W1'=O2, Y1'=T2, Z1'=A2, B2'=C2, D2'=E2, F2'=G2, H2'=Q2, J2'=L2, K2'=V2, M2'=N2, P2'=Q2_1, S2'=P3, U2'=M3, W2'=R3, X2'=Y2, Z2'=A3, B3'=C3, D3'=E3, F3'=G3, H3'=J3, Q3'=T3, K3'=L3, N3'=O3, Q3_1'=N4, S3'=K4, U3'=O4, V3'=W3, X3'=Y3, Z3'=A4, B4'=C4, D4'=E4, F4'=H4, Q4'=J4, L4'=M4, P4'=G4, [ 2*G4>=2+U2 && 3+U2>=2*G4 ], cost: 1 Applied chaining over branches and pruning: Start location: f0 0: f0 -> f1 : [], cost: 1 191: f1 -> f3 : C'=1+B, E'=1+D, [ A>=1+B && B>=1+D ], cost: 2 192: f1 -> f3 : C'=1+B, E'=-1+D, [ A>=1+B && D>=1+B ], cost: 2 194: f1 -> f3 : C'=-1+B, E'=1+D, [ B>=1+A && B>=1+D ], cost: 2 195: f1 -> f3 : C'=-1+B, E'=-1+D, [ B>=1+A && D>=1+B ], cost: 2 197: f1 -> f3 : A'=B, C'=B, E'=1+D, [ B==A && B>=1+D ], cost: 2 200: f3 -> f5 : G'=1+F, Q'=1+H, [ 2>=F+D && 2>=H+F ], cost: 2 201: f3 -> f5 : G'=1+F, Q'=-1+H, [ 2>=F+D && H+F>=4 ], cost: 2 203: f3 -> f5 : G'=-1+F, Q'=1+H, [ F+D>=4 && 2>=H+F ], cost: 2 204: f3 -> f5 : G'=-1+F, Q'=-1+H, [ F+D>=4 && H+F>=4 ], cost: 2 206: f3 -> f5 : F'=3-D, G'=3-D, Q'=1+H, [ F+D==3 && 2>=3+H-D ], cost: 2 209: f5 -> f7 : K'=1+J, N'=1+L, [ H>=1+J && 0>=1+L && M>=1+L ], cost: 2 210: f5 -> f7 : K'=1+J, N'=-1+L, [ H>=1+J && L>=1 ], cost: 2 212: f5 -> f7 : K'=1+J, L'=0, N'=0, [ H>=1+J && M>=0 && L==0 ], cost: 2 216: f5 -> f7 : K'=-1+J, N'=-1+L, [ J>=1+H && L>=1+M ], cost: 2 217: f5 -> f7 : K'=-1+J, L'=0, N'=0, [ J>=1+H && M>=0 && L==0 ], cost: 2 224: f7 -> f9 : P'=1+O, R'=1+Q_1, [ L>=1+O && O+J>=1+2*Q_1 ], cost: 2 225: f7 -> f9 : P'=1+O, R'=-1+Q_1, [ L>=1+O && 2*Q_1>=2+O+J ], cost: 2 227: f7 -> f9 : P'=-1+O, R'=1+Q_1, [ O>=1+L && O+J>=1+2*Q_1 ], cost: 2 228: f7 -> f9 : P'=-1+O, R'=-1+Q_1, [ O>=1+L && 2*Q_1>=2+O+J ], cost: 2 230: f7 -> f9 : O'=L, P'=L, R'=1+Q_1, [ L==O && L+J>=1+2*Q_1 ], cost: 2 233: f9 -> f11 : T'=1+S, V'=1+U, [ L>=1+S && 2>=U+S ], cost: 2 234: f9 -> f11 : T'=1+S, V'=-1+U, [ L>=1+S && U+S>=4 ], cost: 2 236: f9 -> f11 : T'=-1+S, V'=1+U, [ S>=1+L && 2>=U+S ], cost: 2 237: f9 -> f11 : T'=-1+S, V'=-1+U, [ S>=1+L && U+S>=4 ], cost: 2 239: f9 -> f11 : S'=L, T'=L, V'=1+U, [ L==S && 2>=U+L ], cost: 2 242: f11 -> f13 : X'=1+A, Z'=1+M, [ 1+W>=2*A && 1+Y>=2*M ], cost: 2 243: f11 -> f13 : X'=1+A, Z'=-1+M, [ 1+W>=2*A && 2*M>=4+Y ], cost: 2 245: f11 -> f13 : X'=-1+A, Z'=1+M, [ 2*A>=4+W && 1+Y>=2*M ], cost: 2 246: f11 -> f13 : X'=-1+A, Z'=-1+M, [ 2*A>=4+W && 2*M>=4+Y ], cost: 2 248: f11 -> f13 : X'=A, Z'=1+M, [ 2*A>=2+W && 3+W>=2*A && 1+Y>=2*M ], cost: 2 251: f13 -> f15 : C1'=1+B1, E1'=1+D1, [ A1>=1+B1 && B1>=1+D1 ], cost: 2 252: f13 -> f15 : C1'=1+B1, E1'=-1+D1, [ A1>=1+B1 && D1>=1+B1 ], cost: 2 254: f13 -> f15 : C1'=-1+B1, E1'=1+D1, [ B1>=1+A1 && B1>=1+D1 ], cost: 2 255: f13 -> f15 : C1'=-1+B1, E1'=-1+D1, [ B1>=1+A1 && D1>=1+B1 ], cost: 2 257: f13 -> f15 : A1'=B1, C1'=B1, E1'=1+D1, [ B1==A1 && B1>=1+D1 ], cost: 2 260: f15 -> f17 : G1'=1+F1, Q1'=1+H1, [ 2>=F1+D1 && 2>=H1+F1 ], cost: 2 261: f15 -> f17 : G1'=1+F1, Q1'=-1+H1, [ 2>=F1+D1 && H1+F1>=4 ], cost: 2 263: f15 -> f17 : G1'=-1+F1, Q1'=1+H1, [ F1+D1>=4 && 2>=H1+F1 ], cost: 2 264: f15 -> f17 : G1'=-1+F1, Q1'=-1+H1, [ F1+D1>=4 && H1+F1>=4 ], cost: 2 266: f15 -> f17 : F1'=3-D1, G1'=3-D1, Q1'=1+H1, [ F1+D1==3 && 2>=3+H1-D1 ], cost: 2 269: f17 -> f19 : K1'=1+J1, N1'=1+L1, [ H1>=1+J1 && 1>=L1 && M1>=1+L1 ], cost: 2 270: f17 -> f19 : K1'=1+J1, N1'=-1+L1, [ H1>=1+J1 && L1>=3 ], cost: 2 272: f17 -> f19 : K1'=1+J1, L1'=2, N1'=2, [ H1>=1+J1 && M1>=2 && L1==2 ], cost: 2 276: f17 -> f19 : K1'=-1+J1, N1'=-1+L1, [ J1>=1+H1 && L1>=1+M1 ], cost: 2 277: f17 -> f19 : K1'=-1+J1, L1'=2, N1'=2, [ J1>=1+H1 && M1>=2 && L1==2 ], cost: 2 284: f19 -> f21 : P1'=1+O1, Q1_1'=1+Y, [ L1>=1+O1 && O1+J1>=1+2*Y ], cost: 2 285: f19 -> f21 : P1'=1+O1, Q1_1'=-1+Y, [ L1>=1+O1 && 2*Y>=2+O1+J1 ], cost: 2 287: f19 -> f21 : P1'=-1+O1, Q1_1'=1+Y, [ O1>=1+L1 && O1+J1>=1+2*Y ], cost: 2 288: f19 -> f21 : P1'=-1+O1, Q1_1'=-1+Y, [ O1>=1+L1 && 2*Y>=2+O1+J1 ], cost: 2 290: f19 -> f21 : O1'=L1, P1'=L1, Q1_1'=1+Y, [ L1==O1 && L1+J1>=1+2*Y ], cost: 2 293: f21 -> f23 : S1'=1+R1, T1'=1+W, [ L1>=1+R1 && 2>=R1+W ], cost: 2 294: f21 -> f23 : S1'=1+R1, T1'=-1+W, [ L1>=1+R1 && R1+W>=4 ], cost: 2 296: f21 -> f23 : S1'=-1+R1, T1'=1+W, [ R1>=1+L1 && 2>=R1+W ], cost: 2 297: f21 -> f23 : S1'=-1+R1, T1'=-1+W, [ R1>=1+L1 && R1+W>=4 ], cost: 2 299: f21 -> f23 : R1'=L1, S1'=L1, T1'=1+W, [ L1==R1 && 2>=L1+W ], cost: 2 302: f23 -> f25 : V1'=1+A1, X1'=1+M1, [ U+U1>=2+2*A1 && Q_1+W1>=1+2*M1 ], cost: 2 303: f23 -> f25 : V1'=1+A1, X1'=-1+M1, [ U+U1>=2+2*A1 && 2*M1>=2+Q_1+W1 ], cost: 2 305: f23 -> f25 : V1'=-1+A1, X1'=1+M1, [ 2*A1>=1+U+U1 && Q_1+W1>=1+2*M1 ], cost: 2 306: f23 -> f25 : V1'=-1+A1, X1'=-1+M1, [ 2*A1>=1+U+U1 && 2*M1>=2+Q_1+W1 ], cost: 2 308: f23 -> f25 : V1'=A1, X1'=1+M1, [ 1+2*A1>=U+U1 && U+U1>=2*A1 && Q_1+W1>=1+2*M1 ], cost: 2 311: f25 -> f27 : A2'=1+Z1, C2'=1+B2, [ Y1>=1+Z1 && Z1>=1+B2 ], cost: 2 312: f25 -> f27 : A2'=1+Z1, C2'=-1+B2, [ Y1>=1+Z1 && B2>=1+Z1 ], cost: 2 314: f25 -> f27 : A2'=-1+Z1, C2'=1+B2, [ Z1>=1+Y1 && Z1>=1+B2 ], cost: 2 315: f25 -> f27 : A2'=-1+Z1, C2'=-1+B2, [ Z1>=1+Y1 && B2>=1+Z1 ], cost: 2 317: f25 -> f27 : Y1'=Z1, A2'=Z1, C2'=1+B2, [ Z1==Y1 && Z1>=1+B2 ], cost: 2 320: f27 -> f29 : E2'=1+D2, G2'=1+F2, [ 2>=D2+B2 && 2>=D2+F2 ], cost: 2 321: f27 -> f29 : E2'=1+D2, G2'=-1+F2, [ 2>=D2+B2 && D2+F2>=4 ], cost: 2 323: f27 -> f29 : E2'=-1+D2, G2'=1+F2, [ D2+B2>=4 && 2>=D2+F2 ], cost: 2 324: f27 -> f29 : E2'=-1+D2, G2'=-1+F2, [ D2+B2>=4 && D2+F2>=4 ], cost: 2 326: f27 -> f29 : D2'=3-B2, E2'=3-B2, G2'=1+F2, [ D2+B2==3 && 2>=3-B2+F2 ], cost: 2 329: f29 -> f31 : Q2'=1+H2, L2'=1+J2, [ F2>=1+H2 && 2>=J2 && K2>=1+J2 ], cost: 2 330: f29 -> f31 : Q2'=1+H2, L2'=-1+J2, [ F2>=1+H2 && J2>=4 ], cost: 2 332: f29 -> f31 : Q2'=1+H2, J2'=3, L2'=3, [ F2>=1+H2 && K2>=3 && J2==3 ], cost: 2 336: f29 -> f31 : Q2'=-1+H2, L2'=-1+J2, [ H2>=1+F2 && J2>=1+K2 ], cost: 2 337: f29 -> f31 : Q2'=-1+H2, J2'=3, L2'=3, [ H2>=1+F2 && K2>=3 && J2==3 ], cost: 2 344: f31 -> f33 : N2'=1+M2, O2'=1+W1, [ J2>=1+M2 && M2+H2>=1+2*W1 ], cost: 2 345: f31 -> f33 : N2'=1+M2, O2'=-1+W1, [ J2>=1+M2 && 2*W1>=2+M2+H2 ], cost: 2 347: f31 -> f33 : N2'=-1+M2, O2'=1+W1, [ M2>=1+J2 && M2+H2>=1+2*W1 ], cost: 2 348: f31 -> f33 : N2'=-1+M2, O2'=-1+W1, [ M2>=1+J2 && 2*W1>=2+M2+H2 ], cost: 2 350: f31 -> f33 : M2'=J2, N2'=J2, O2'=1+W1, [ J2==M2 && J2+H2>=1+2*W1 ], cost: 2 353: f33 -> f35 : Q2_1'=1+P2, R2'=1+U1, [ J2>=1+P2 && 2>=P2+U1 ], cost: 2 354: f33 -> f35 : Q2_1'=1+P2, R2'=-1+U1, [ J2>=1+P2 && P2+U1>=4 ], cost: 2 356: f33 -> f35 : Q2_1'=-1+P2, R2'=1+U1, [ P2>=1+J2 && 2>=P2+U1 ], cost: 2 357: f33 -> f35 : Q2_1'=-1+P2, R2'=-1+U1, [ P2>=1+J2 && P2+U1>=4 ], cost: 2 359: f33 -> f35 : P2'=J2, Q2_1'=J2, R2'=1+U1, [ J2==P2 && 2>=J2+U1 ], cost: 2 362: f35 -> f37 : T2'=1+Y1, V2'=1+K2, [ S2+W>=2+2*Y1 && Y+U2>=1+2*K2 ], cost: 2 363: f35 -> f37 : T2'=1+Y1, V2'=-1+K2, [ S2+W>=2+2*Y1 && 2*K2>=2+Y+U2 ], cost: 2 365: f35 -> f37 : T2'=-1+Y1, V2'=1+K2, [ 2*Y1>=1+S2+W && Y+U2>=1+2*K2 ], cost: 2 366: f35 -> f37 : T2'=-1+Y1, V2'=-1+K2, [ 2*Y1>=1+S2+W && 2*K2>=2+Y+U2 ], cost: 2 368: f35 -> f37 : T2'=Y1, V2'=1+K2, [ 1+2*Y1>=S2+W && S2+W>=2*Y1 && Y+U2>=1+2*K2 ], cost: 2 371: f37 -> f39 : Y2'=1+X2, A3'=1+Z2, [ W2>=1+X2 && X2>=1+Z2 ], cost: 2 372: f37 -> f39 : Y2'=1+X2, A3'=-1+Z2, [ W2>=1+X2 && Z2>=1+X2 ], cost: 2 374: f37 -> f39 : Y2'=-1+X2, A3'=1+Z2, [ X2>=1+W2 && X2>=1+Z2 ], cost: 2 375: f37 -> f39 : Y2'=-1+X2, A3'=-1+Z2, [ X2>=1+W2 && Z2>=1+X2 ], cost: 2 377: f37 -> f39 : W2'=X2, Y2'=X2, A3'=1+Z2, [ X2==W2 && X2>=1+Z2 ], cost: 2 380: f39 -> f41 : C3'=1+B3, E3'=1+D3, [ 2>=Z2+B3 && 2>=D3+B3 ], cost: 2 381: f39 -> f41 : C3'=1+B3, E3'=-1+D3, [ 2>=Z2+B3 && D3+B3>=4 ], cost: 2 383: f39 -> f41 : C3'=-1+B3, E3'=1+D3, [ Z2+B3>=4 && 2>=D3+B3 ], cost: 2 384: f39 -> f41 : C3'=-1+B3, E3'=-1+D3, [ Z2+B3>=4 && D3+B3>=4 ], cost: 2 386: f39 -> f41 : B3'=3-Z2, C3'=3-Z2, E3'=1+D3, [ Z2+B3==3 && 2>=3-Z2+D3 ], cost: 2 389: f41 -> f43 : G3'=1+F3, J3'=1+H3, [ D3>=1+F3 && 2>=H3 && Q3>=1+H3 ], cost: 2 390: f41 -> f43 : G3'=1+F3, J3'=-1+H3, [ D3>=1+F3 && H3>=4 ], cost: 2 392: f41 -> f43 : G3'=1+F3, H3'=3, J3'=3, [ D3>=1+F3 && Q3>=3 && H3==3 ], cost: 2 396: f41 -> f43 : G3'=-1+F3, J3'=-1+H3, [ F3>=1+D3 && H3>=1+Q3 ], cost: 2 397: f41 -> f43 : G3'=-1+F3, H3'=3, J3'=3, [ F3>=1+D3 && Q3>=3 && H3==3 ], cost: 2 404: f43 -> f45 : L3'=1+K3, M3'=1+U2, [ H3>=1+K3 && F3+K3>=1+2*U2 ], cost: 2 405: f43 -> f45 : L3'=1+K3, M3'=-1+U2, [ H3>=1+K3 && 2*U2>=2+F3+K3 ], cost: 2 407: f43 -> f45 : L3'=-1+K3, M3'=1+U2, [ K3>=1+H3 && F3+K3>=1+2*U2 ], cost: 2 408: f43 -> f45 : L3'=-1+K3, M3'=-1+U2, [ K3>=1+H3 && 2*U2>=2+F3+K3 ], cost: 2 410: f43 -> f45 : K3'=H3, L3'=H3, M3'=1+U2, [ H3==K3 && F3+H3>=1+2*U2 ], cost: 2 413: f45 -> f47 : O3'=1+N3, P3'=1+S2, [ H3>=1+N3 && 2>=S2+N3 ], cost: 2 414: f45 -> f47 : O3'=1+N3, P3'=-1+S2, [ H3>=1+N3 && S2+N3>=4 ], cost: 2 416: f45 -> f47 : O3'=-1+N3, P3'=1+S2, [ N3>=1+H3 && 2>=S2+N3 ], cost: 2 417: f45 -> f47 : O3'=-1+N3, P3'=-1+S2, [ N3>=1+H3 && S2+N3>=4 ], cost: 2 419: f45 -> f47 : N3'=H3, O3'=H3, P3'=1+S2, [ H3==N3 && 2>=S2+H3 ], cost: 2 422: f47 -> f49 : R3'=1+W2, T3'=1+Q3, [ U1+Q3_1>=2+2*W2 && S3+W1>=1+2*Q3 ], cost: 2 423: f47 -> f49 : R3'=1+W2, T3'=-1+Q3, [ U1+Q3_1>=2+2*W2 && 2*Q3>=2+S3+W1 ], cost: 2 425: f47 -> f49 : R3'=-1+W2, T3'=1+Q3, [ 2*W2>=1+U1+Q3_1 && S3+W1>=1+2*Q3 ], cost: 2 426: f47 -> f49 : R3'=-1+W2, T3'=-1+Q3, [ 2*W2>=1+U1+Q3_1 && 2*Q3>=2+S3+W1 ], cost: 2 428: f47 -> f49 : R3'=W2, T3'=1+Q3, [ 1+2*W2>=U1+Q3_1 && U1+Q3_1>=2*W2 && S3+W1>=1+2*Q3 ], cost: 2 431: f49 -> f51 : W3'=1+V3, Y3'=1+X3, [ U3>=1+V3 && V3>=1+X3 ], cost: 2 432: f49 -> f51 : W3'=1+V3, Y3'=-1+X3, [ U3>=1+V3 && X3>=1+V3 ], cost: 2 434: f49 -> f51 : W3'=-1+V3, Y3'=1+X3, [ V3>=1+U3 && V3>=1+X3 ], cost: 2 435: f49 -> f51 : W3'=-1+V3, Y3'=-1+X3, [ V3>=1+U3 && X3>=1+V3 ], cost: 2 437: f49 -> f51 : U3'=V3, W3'=V3, Y3'=1+X3, [ V3==U3 && V3>=1+X3 ], cost: 2 440: f51 -> f53 : A4'=1+Z3, C4'=1+B4, [ 2>=Z3+X3 && 2>=Z3+B4 ], cost: 2 441: f51 -> f53 : A4'=1+Z3, C4'=-1+B4, [ 2>=Z3+X3 && Z3+B4>=4 ], cost: 2 443: f51 -> f53 : A4'=-1+Z3, C4'=1+B4, [ Z3+X3>=4 && 2>=Z3+B4 ], cost: 2 444: f51 -> f53 : A4'=-1+Z3, C4'=-1+B4, [ Z3+X3>=4 && Z3+B4>=4 ], cost: 2 446: f51 -> f53 : Z3'=3-X3, A4'=3-X3, C4'=1+B4, [ Z3+X3==3 && 2>=3-X3+B4 ], cost: 2 449: f53 -> f55 : E4'=1+D4, H4'=1+F4, [ B4>=1+D4 && 2>=F4 && G4>=1+F4 ], cost: 2 450: f53 -> f55 : E4'=1+D4, H4'=-1+F4, [ B4>=1+D4 && F4>=4 ], cost: 2 452: f53 -> f55 : E4'=1+D4, F4'=3, H4'=3, [ B4>=1+D4 && G4>=3 && F4==3 ], cost: 2 456: f53 -> f55 : E4'=-1+D4, H4'=-1+F4, [ D4>=1+B4 && F4>=1+G4 ], cost: 2 457: f53 -> f55 : E4'=-1+D4, F4'=3, H4'=3, [ D4>=1+B4 && G4>=3 && F4==3 ], cost: 2 464: f55 -> f57 : J4'=1+Q4, K4'=1+S3, [ F4>=1+Q4 && Q4+D4>=1+2*S3 ], cost: 2 465: f55 -> f57 : J4'=1+Q4, K4'=-1+S3, [ F4>=1+Q4 && 2*S3>=2+Q4+D4 ], cost: 2 467: f55 -> f57 : J4'=-1+Q4, K4'=1+S3, [ Q4>=1+F4 && Q4+D4>=1+2*S3 ], cost: 2 468: f55 -> f57 : J4'=-1+Q4, K4'=-1+S3, [ Q4>=1+F4 && 2*S3>=2+Q4+D4 ], cost: 2 470: f55 -> f57 : Q4'=F4, J4'=F4, K4'=1+S3, [ F4==Q4 && F4+D4>=1+2*S3 ], cost: 2 473: f57 -> f59 : M4'=1+L4, N4'=1+Q3_1, [ F4>=1+L4 && 2>=L4+Q3_1 ], cost: 2 474: f57 -> f59 : M4'=1+L4, N4'=-1+Q3_1, [ F4>=1+L4 && L4+Q3_1>=4 ], cost: 2 476: f57 -> f59 : M4'=-1+L4, N4'=1+Q3_1, [ L4>=1+F4 && 2>=L4+Q3_1 ], cost: 2 477: f57 -> f59 : M4'=-1+L4, N4'=-1+Q3_1, [ L4>=1+F4 && L4+Q3_1>=4 ], cost: 2 479: f57 -> f59 : L4'=F4, M4'=F4, N4'=1+Q3_1, [ F4==L4 && 2>=F4+Q3_1 ], cost: 2 482: f59 -> f1 : A'=X, B'=C, D'=E, F'=G, H'=Q, J'=K, L'=N, M'=Z, O'=P, Q_1'=R, S'=T, U'=V, W'=T1, Y'=Q1_1, A1'=V1, B1'=C1, D1'=E1, F1'=G1, H1'=Q1, J1'=K1, L1'=N1, M1'=X1, O1'=P1, R1'=S1, U1'=R2, W1'=O2, Y1'=T2, Z1'=A2, B2'=C2, D2'=E2, F2'=G2, H2'=Q2, J2'=L2, K2'=V2, M2'=N2, P2'=Q2_1, S2'=P3, U2'=M3, W2'=R3, X2'=Y2, Z2'=A3, B3'=C3, D3'=E3, F3'=G3, H3'=J3, Q3'=T3, K3'=L3, N3'=O3, Q3_1'=N4, S3'=K4, U3'=1+U3, V3'=W3, X3'=Y3, Z3'=A4, B4'=C4, D4'=E4, F4'=H4, G4'=1+G4, Q4'=J4, L4'=M4, O4'=1+U3, P4'=1+G4, [ S2>=2+2*U3 && 1+U2>=2*G4 ], cost: 2 483: f59 -> f1 : A'=X, B'=C, D'=E, F'=G, H'=Q, J'=K, L'=N, M'=Z, O'=P, Q_1'=R, S'=T, U'=V, W'=T1, Y'=Q1_1, A1'=V1, B1'=C1, D1'=E1, F1'=G1, H1'=Q1, J1'=K1, L1'=N1, M1'=X1, O1'=P1, R1'=S1, U1'=R2, W1'=O2, Y1'=T2, Z1'=A2, B2'=C2, D2'=E2, F2'=G2, H2'=Q2, J2'=L2, K2'=V2, M2'=N2, P2'=Q2_1, S2'=P3, U2'=M3, W2'=R3, X2'=Y2, Z2'=A3, B3'=C3, D3'=E3, F3'=G3, H3'=J3, Q3'=T3, K3'=L3, N3'=O3, Q3_1'=N4, S3'=K4, U3'=1+U3, V3'=W3, X3'=Y3, Z3'=A4, B4'=C4, D4'=E4, F4'=H4, G4'=-1+G4, Q4'=J4, L4'=M4, O4'=1+U3, P4'=-1+G4, [ S2>=2+2*U3 && 2*G4>=4+U2 ], cost: 2 485: f59 -> f1 : A'=X, B'=C, D'=E, F'=G, H'=Q, J'=K, L'=N, M'=Z, O'=P, Q_1'=R, S'=T, U'=V, W'=T1, Y'=Q1_1, A1'=V1, B1'=C1, D1'=E1, F1'=G1, H1'=Q1, J1'=K1, L1'=N1, M1'=X1, O1'=P1, R1'=S1, U1'=R2, W1'=O2, Y1'=T2, Z1'=A2, B2'=C2, D2'=E2, F2'=G2, H2'=Q2, J2'=L2, K2'=V2, M2'=N2, P2'=Q2_1, S2'=P3, U2'=M3, W2'=R3, X2'=Y2, Z2'=A3, B3'=C3, D3'=E3, F3'=G3, H3'=J3, Q3'=T3, K3'=L3, N3'=O3, Q3_1'=N4, S3'=K4, U3'=-1+U3, V3'=W3, X3'=Y3, Z3'=A4, B4'=C4, D4'=E4, F4'=H4, G4'=1+G4, Q4'=J4, L4'=M4, O4'=-1+U3, P4'=1+G4, [ 2*U3>=1+S2 && 1+U2>=2*G4 ], cost: 2 486: f59 -> f1 : A'=X, B'=C, D'=E, F'=G, H'=Q, J'=K, L'=N, M'=Z, O'=P, Q_1'=R, S'=T, U'=V, W'=T1, Y'=Q1_1, A1'=V1, B1'=C1, D1'=E1, F1'=G1, H1'=Q1, J1'=K1, L1'=N1, M1'=X1, O1'=P1, R1'=S1, U1'=R2, W1'=O2, Y1'=T2, Z1'=A2, B2'=C2, D2'=E2, F2'=G2, H2'=Q2, J2'=L2, K2'=V2, M2'=N2, P2'=Q2_1, S2'=P3, U2'=M3, W2'=R3, X2'=Y2, Z2'=A3, B3'=C3, D3'=E3, F3'=G3, H3'=J3, Q3'=T3, K3'=L3, N3'=O3, Q3_1'=N4, S3'=K4, U3'=-1+U3, V3'=W3, X3'=Y3, Z3'=A4, B4'=C4, D4'=E4, F4'=H4, G4'=-1+G4, Q4'=J4, L4'=M4, O4'=-1+U3, P4'=-1+G4, [ 2*U3>=1+S2 && 2*G4>=4+U2 ], cost: 2 488: f59 -> f1 : A'=X, B'=C, D'=E, F'=G, H'=Q, J'=K, L'=N, M'=Z, O'=P, Q_1'=R, S'=T, U'=V, W'=T1, Y'=Q1_1, A1'=V1, B1'=C1, D1'=E1, F1'=G1, H1'=Q1, J1'=K1, L1'=N1, M1'=X1, O1'=P1, R1'=S1, U1'=R2, W1'=O2, Y1'=T2, Z1'=A2, B2'=C2, D2'=E2, F2'=G2, H2'=Q2, J2'=L2, K2'=V2, M2'=N2, P2'=Q2_1, S2'=P3, U2'=M3, W2'=R3, X2'=Y2, Z2'=A3, B3'=C3, D3'=E3, F3'=G3, H3'=J3, Q3'=T3, K3'=L3, N3'=O3, Q3_1'=N4, S3'=K4, U3'=U3, V3'=W3, X3'=Y3, Z3'=A4, B4'=C4, D4'=E4, F4'=H4, G4'=1+G4, Q4'=J4, L4'=M4, O4'=U3, P4'=1+G4, [ 1+2*U3>=S2 && S2>=2*U3 && 1+U2>=2*G4 ], cost: 2 Applied chaining over branches and pruning: Start location: f0 0: f0 -> f1 : [], cost: 1 491: f1 -> f5 : C'=1+B, E'=1+D, G'=1+F, Q'=1+H, [ A>=1+B && B>=1+D && 2>=F+D && 2>=H+F ], cost: 4 492: f1 -> f5 : C'=1+B, E'=1+D, G'=1+F, Q'=-1+H, [ A>=1+B && B>=1+D && 2>=F+D && H+F>=4 ], cost: 4 494: f1 -> f5 : C'=1+B, E'=1+D, G'=-1+F, Q'=-1+H, [ A>=1+B && B>=1+D && F+D>=4 && H+F>=4 ], cost: 4 498: f1 -> f5 : C'=1+B, E'=-1+D, G'=-1+F, Q'=1+H, [ A>=1+B && D>=1+B && F+D>=4 && 2>=H+F ], cost: 4 503: f1 -> f5 : C'=-1+B, E'=1+D, G'=-1+F, Q'=1+H, [ B>=1+A && B>=1+D && F+D>=4 && 2>=H+F ], cost: 4 516: f5 -> f9 : K'=1+J, N'=1+L, P'=1+O, R'=1+Q_1, [ H>=1+J && 0>=1+L && M>=1+L && L>=1+O && O+J>=1+2*Q_1 ], cost: 4 517: f5 -> f9 : K'=1+J, N'=1+L, P'=1+O, R'=-1+Q_1, [ H>=1+J && 0>=1+L && M>=1+L && L>=1+O && 2*Q_1>=2+O+J ], cost: 4 519: f5 -> f9 : K'=1+J, N'=1+L, P'=-1+O, R'=-1+Q_1, [ H>=1+J && 0>=1+L && M>=1+L && O>=1+L && 2*Q_1>=2+O+J ], cost: 4 523: f5 -> f9 : K'=1+J, N'=-1+L, P'=-1+O, R'=1+Q_1, [ H>=1+J && L>=1 && O>=1+L && O+J>=1+2*Q_1 ], cost: 4 528: f5 -> f9 : K'=1+J, L'=0, N'=0, P'=-1+O, R'=1+Q_1, [ H>=1+J && M>=0 && L==0 && O>=1 && O+J>=1+2*Q_1 ], cost: 4 541: f9 -> f13 : T'=1+S, V'=1+U, X'=1+A, Z'=1+M, [ L>=1+S && 2>=U+S && 1+W>=2*A && 1+Y>=2*M ], cost: 4 542: f9 -> f13 : T'=1+S, V'=1+U, X'=1+A, Z'=-1+M, [ L>=1+S && 2>=U+S && 1+W>=2*A && 2*M>=4+Y ], cost: 4 544: f9 -> f13 : T'=1+S, V'=1+U, X'=-1+A, Z'=-1+M, [ L>=1+S && 2>=U+S && 2*A>=4+W && 2*M>=4+Y ], cost: 4 548: f9 -> f13 : T'=1+S, V'=-1+U, X'=-1+A, Z'=1+M, [ L>=1+S && U+S>=4 && 2*A>=4+W && 1+Y>=2*M ], cost: 4 553: f9 -> f13 : T'=-1+S, V'=1+U, X'=-1+A, Z'=1+M, [ S>=1+L && 2>=U+S && 2*A>=4+W && 1+Y>=2*M ], cost: 4 566: f13 -> f17 : C1'=1+B1, E1'=1+D1, G1'=1+F1, Q1'=1+H1, [ A1>=1+B1 && B1>=1+D1 && 2>=F1+D1 && 2>=H1+F1 ], cost: 4 567: f13 -> f17 : C1'=1+B1, E1'=1+D1, G1'=1+F1, Q1'=-1+H1, [ A1>=1+B1 && B1>=1+D1 && 2>=F1+D1 && H1+F1>=4 ], cost: 4 569: f13 -> f17 : C1'=1+B1, E1'=1+D1, G1'=-1+F1, Q1'=-1+H1, [ A1>=1+B1 && B1>=1+D1 && F1+D1>=4 && H1+F1>=4 ], cost: 4 573: f13 -> f17 : C1'=1+B1, E1'=-1+D1, G1'=-1+F1, Q1'=1+H1, [ A1>=1+B1 && D1>=1+B1 && F1+D1>=4 && 2>=H1+F1 ], cost: 4 578: f13 -> f17 : C1'=-1+B1, E1'=1+D1, G1'=-1+F1, Q1'=1+H1, [ B1>=1+A1 && B1>=1+D1 && F1+D1>=4 && 2>=H1+F1 ], cost: 4 591: f17 -> f21 : K1'=1+J1, N1'=1+L1, P1'=1+O1, Q1_1'=1+Y, [ H1>=1+J1 && 1>=L1 && M1>=1+L1 && L1>=1+O1 && O1+J1>=1+2*Y ], cost: 4 592: f17 -> f21 : K1'=1+J1, N1'=1+L1, P1'=1+O1, Q1_1'=-1+Y, [ H1>=1+J1 && 1>=L1 && M1>=1+L1 && L1>=1+O1 && 2*Y>=2+O1+J1 ], cost: 4 594: f17 -> f21 : K1'=1+J1, N1'=1+L1, P1'=-1+O1, Q1_1'=-1+Y, [ H1>=1+J1 && 1>=L1 && M1>=1+L1 && O1>=1+L1 && 2*Y>=2+O1+J1 ], cost: 4 598: f17 -> f21 : K1'=1+J1, N1'=-1+L1, P1'=-1+O1, Q1_1'=1+Y, [ H1>=1+J1 && L1>=3 && O1>=1+L1 && O1+J1>=1+2*Y ], cost: 4 603: f17 -> f21 : K1'=1+J1, L1'=2, N1'=2, P1'=-1+O1, Q1_1'=1+Y, [ H1>=1+J1 && M1>=2 && L1==2 && O1>=3 && O1+J1>=1+2*Y ], cost: 4 616: f21 -> f25 : S1'=1+R1, T1'=1+W, V1'=1+A1, X1'=1+M1, [ L1>=1+R1 && 2>=R1+W && U+U1>=2+2*A1 && Q_1+W1>=1+2*M1 ], cost: 4 617: f21 -> f25 : S1'=1+R1, T1'=1+W, V1'=1+A1, X1'=-1+M1, [ L1>=1+R1 && 2>=R1+W && U+U1>=2+2*A1 && 2*M1>=2+Q_1+W1 ], cost: 4 619: f21 -> f25 : S1'=1+R1, T1'=1+W, V1'=-1+A1, X1'=-1+M1, [ L1>=1+R1 && 2>=R1+W && 2*A1>=1+U+U1 && 2*M1>=2+Q_1+W1 ], cost: 4 623: f21 -> f25 : S1'=1+R1, T1'=-1+W, V1'=-1+A1, X1'=1+M1, [ L1>=1+R1 && R1+W>=4 && 2*A1>=1+U+U1 && Q_1+W1>=1+2*M1 ], cost: 4 628: f21 -> f25 : S1'=-1+R1, T1'=1+W, V1'=-1+A1, X1'=1+M1, [ R1>=1+L1 && 2>=R1+W && 2*A1>=1+U+U1 && Q_1+W1>=1+2*M1 ], cost: 4 641: f25 -> f29 : A2'=1+Z1, C2'=1+B2, E2'=1+D2, G2'=1+F2, [ Y1>=1+Z1 && Z1>=1+B2 && 2>=D2+B2 && 2>=D2+F2 ], cost: 4 642: f25 -> f29 : A2'=1+Z1, C2'=1+B2, E2'=1+D2, G2'=-1+F2, [ Y1>=1+Z1 && Z1>=1+B2 && 2>=D2+B2 && D2+F2>=4 ], cost: 4 644: f25 -> f29 : A2'=1+Z1, C2'=1+B2, E2'=-1+D2, G2'=-1+F2, [ Y1>=1+Z1 && Z1>=1+B2 && D2+B2>=4 && D2+F2>=4 ], cost: 4 648: f25 -> f29 : A2'=1+Z1, C2'=-1+B2, E2'=-1+D2, G2'=1+F2, [ Y1>=1+Z1 && B2>=1+Z1 && D2+B2>=4 && 2>=D2+F2 ], cost: 4 653: f25 -> f29 : A2'=-1+Z1, C2'=1+B2, E2'=-1+D2, G2'=1+F2, [ Z1>=1+Y1 && Z1>=1+B2 && D2+B2>=4 && 2>=D2+F2 ], cost: 4 666: f29 -> f33 : Q2'=1+H2, L2'=1+J2, N2'=1+M2, O2'=1+W1, [ F2>=1+H2 && 2>=J2 && K2>=1+J2 && J2>=1+M2 && M2+H2>=1+2*W1 ], cost: 4 667: f29 -> f33 : Q2'=1+H2, L2'=1+J2, N2'=1+M2, O2'=-1+W1, [ F2>=1+H2 && 2>=J2 && K2>=1+J2 && J2>=1+M2 && 2*W1>=2+M2+H2 ], cost: 4 669: f29 -> f33 : Q2'=1+H2, L2'=1+J2, N2'=-1+M2, O2'=-1+W1, [ F2>=1+H2 && 2>=J2 && K2>=1+J2 && M2>=1+J2 && 2*W1>=2+M2+H2 ], cost: 4 673: f29 -> f33 : Q2'=1+H2, L2'=-1+J2, N2'=-1+M2, O2'=1+W1, [ F2>=1+H2 && J2>=4 && M2>=1+J2 && M2+H2>=1+2*W1 ], cost: 4 678: f29 -> f33 : Q2'=1+H2, J2'=3, L2'=3, N2'=-1+M2, O2'=1+W1, [ F2>=1+H2 && K2>=3 && J2==3 && M2>=4 && M2+H2>=1+2*W1 ], cost: 4 691: f33 -> f37 : Q2_1'=1+P2, R2'=1+U1, T2'=1+Y1, V2'=1+K2, [ J2>=1+P2 && 2>=P2+U1 && S2+W>=2+2*Y1 && Y+U2>=1+2*K2 ], cost: 4 692: f33 -> f37 : Q2_1'=1+P2, R2'=1+U1, T2'=1+Y1, V2'=-1+K2, [ J2>=1+P2 && 2>=P2+U1 && S2+W>=2+2*Y1 && 2*K2>=2+Y+U2 ], cost: 4 694: f33 -> f37 : Q2_1'=1+P2, R2'=1+U1, T2'=-1+Y1, V2'=-1+K2, [ J2>=1+P2 && 2>=P2+U1 && 2*Y1>=1+S2+W && 2*K2>=2+Y+U2 ], cost: 4 698: f33 -> f37 : Q2_1'=1+P2, R2'=-1+U1, T2'=-1+Y1, V2'=1+K2, [ J2>=1+P2 && P2+U1>=4 && 2*Y1>=1+S2+W && Y+U2>=1+2*K2 ], cost: 4 703: f33 -> f37 : Q2_1'=-1+P2, R2'=1+U1, T2'=-1+Y1, V2'=1+K2, [ P2>=1+J2 && 2>=P2+U1 && 2*Y1>=1+S2+W && Y+U2>=1+2*K2 ], cost: 4 716: f37 -> f41 : Y2'=1+X2, A3'=1+Z2, C3'=1+B3, E3'=1+D3, [ W2>=1+X2 && X2>=1+Z2 && 2>=Z2+B3 && 2>=D3+B3 ], cost: 4 717: f37 -> f41 : Y2'=1+X2, A3'=1+Z2, C3'=1+B3, E3'=-1+D3, [ W2>=1+X2 && X2>=1+Z2 && 2>=Z2+B3 && D3+B3>=4 ], cost: 4 719: f37 -> f41 : Y2'=1+X2, A3'=1+Z2, C3'=-1+B3, E3'=-1+D3, [ W2>=1+X2 && X2>=1+Z2 && Z2+B3>=4 && D3+B3>=4 ], cost: 4 723: f37 -> f41 : Y2'=1+X2, A3'=-1+Z2, C3'=-1+B3, E3'=1+D3, [ W2>=1+X2 && Z2>=1+X2 && Z2+B3>=4 && 2>=D3+B3 ], cost: 4 728: f37 -> f41 : Y2'=-1+X2, A3'=1+Z2, C3'=-1+B3, E3'=1+D3, [ X2>=1+W2 && X2>=1+Z2 && Z2+B3>=4 && 2>=D3+B3 ], cost: 4 741: f41 -> f45 : G3'=1+F3, J3'=1+H3, L3'=1+K3, M3'=1+U2, [ D3>=1+F3 && 2>=H3 && Q3>=1+H3 && H3>=1+K3 && F3+K3>=1+2*U2 ], cost: 4 742: f41 -> f45 : G3'=1+F3, J3'=1+H3, L3'=1+K3, M3'=-1+U2, [ D3>=1+F3 && 2>=H3 && Q3>=1+H3 && H3>=1+K3 && 2*U2>=2+F3+K3 ], cost: 4 744: f41 -> f45 : G3'=1+F3, J3'=1+H3, L3'=-1+K3, M3'=-1+U2, [ D3>=1+F3 && 2>=H3 && Q3>=1+H3 && K3>=1+H3 && 2*U2>=2+F3+K3 ], cost: 4 748: f41 -> f45 : G3'=1+F3, J3'=-1+H3, L3'=-1+K3, M3'=1+U2, [ D3>=1+F3 && H3>=4 && K3>=1+H3 && F3+K3>=1+2*U2 ], cost: 4 753: f41 -> f45 : G3'=1+F3, H3'=3, J3'=3, L3'=-1+K3, M3'=1+U2, [ D3>=1+F3 && Q3>=3 && H3==3 && K3>=4 && F3+K3>=1+2*U2 ], cost: 4 766: f45 -> f49 : O3'=1+N3, P3'=1+S2, R3'=1+W2, T3'=1+Q3, [ H3>=1+N3 && 2>=S2+N3 && U1+Q3_1>=2+2*W2 && S3+W1>=1+2*Q3 ], cost: 4 767: f45 -> f49 : O3'=1+N3, P3'=1+S2, R3'=1+W2, T3'=-1+Q3, [ H3>=1+N3 && 2>=S2+N3 && U1+Q3_1>=2+2*W2 && 2*Q3>=2+S3+W1 ], cost: 4 769: f45 -> f49 : O3'=1+N3, P3'=1+S2, R3'=-1+W2, T3'=-1+Q3, [ H3>=1+N3 && 2>=S2+N3 && 2*W2>=1+U1+Q3_1 && 2*Q3>=2+S3+W1 ], cost: 4 773: f45 -> f49 : O3'=1+N3, P3'=-1+S2, R3'=-1+W2, T3'=1+Q3, [ H3>=1+N3 && S2+N3>=4 && 2*W2>=1+U1+Q3_1 && S3+W1>=1+2*Q3 ], cost: 4 778: f45 -> f49 : O3'=-1+N3, P3'=1+S2, R3'=-1+W2, T3'=1+Q3, [ N3>=1+H3 && 2>=S2+N3 && 2*W2>=1+U1+Q3_1 && S3+W1>=1+2*Q3 ], cost: 4 791: f49 -> f53 : W3'=1+V3, Y3'=1+X3, A4'=1+Z3, C4'=1+B4, [ U3>=1+V3 && V3>=1+X3 && 2>=Z3+X3 && 2>=Z3+B4 ], cost: 4 792: f49 -> f53 : W3'=1+V3, Y3'=1+X3, A4'=1+Z3, C4'=-1+B4, [ U3>=1+V3 && V3>=1+X3 && 2>=Z3+X3 && Z3+B4>=4 ], cost: 4 794: f49 -> f53 : W3'=1+V3, Y3'=1+X3, A4'=-1+Z3, C4'=-1+B4, [ U3>=1+V3 && V3>=1+X3 && Z3+X3>=4 && Z3+B4>=4 ], cost: 4 798: f49 -> f53 : W3'=1+V3, Y3'=-1+X3, A4'=-1+Z3, C4'=1+B4, [ U3>=1+V3 && X3>=1+V3 && Z3+X3>=4 && 2>=Z3+B4 ], cost: 4 803: f49 -> f53 : W3'=-1+V3, Y3'=1+X3, A4'=-1+Z3, C4'=1+B4, [ V3>=1+U3 && V3>=1+X3 && Z3+X3>=4 && 2>=Z3+B4 ], cost: 4 816: f53 -> f57 : E4'=1+D4, H4'=1+F4, J4'=1+Q4, K4'=1+S3, [ B4>=1+D4 && 2>=F4 && G4>=1+F4 && F4>=1+Q4 && Q4+D4>=1+2*S3 ], cost: 4 817: f53 -> f57 : E4'=1+D4, H4'=1+F4, J4'=1+Q4, K4'=-1+S3, [ B4>=1+D4 && 2>=F4 && G4>=1+F4 && F4>=1+Q4 && 2*S3>=2+Q4+D4 ], cost: 4 819: f53 -> f57 : E4'=1+D4, H4'=1+F4, J4'=-1+Q4, K4'=-1+S3, [ B4>=1+D4 && 2>=F4 && G4>=1+F4 && Q4>=1+F4 && 2*S3>=2+Q4+D4 ], cost: 4 823: f53 -> f57 : E4'=1+D4, H4'=-1+F4, J4'=-1+Q4, K4'=1+S3, [ B4>=1+D4 && F4>=4 && Q4>=1+F4 && Q4+D4>=1+2*S3 ], cost: 4 828: f53 -> f57 : E4'=1+D4, F4'=3, H4'=3, J4'=-1+Q4, K4'=1+S3, [ B4>=1+D4 && G4>=3 && F4==3 && Q4>=4 && Q4+D4>=1+2*S3 ], cost: 4 841: f57 -> f1 : A'=X, B'=C, D'=E, F'=G, H'=Q, J'=K, L'=N, M'=Z, O'=P, Q_1'=R, S'=T, U'=V, W'=T1, Y'=Q1_1, A1'=V1, B1'=C1, D1'=E1, F1'=G1, H1'=Q1, J1'=K1, L1'=N1, M1'=X1, O1'=P1, R1'=S1, U1'=R2, W1'=O2, Y1'=T2, Z1'=A2, B2'=C2, D2'=E2, F2'=G2, H2'=Q2, J2'=L2, K2'=V2, M2'=N2, P2'=Q2_1, S2'=P3, U2'=M3, W2'=R3, X2'=Y2, Z2'=A3, B3'=C3, D3'=E3, F3'=G3, H3'=J3, Q3'=T3, K3'=L3, N3'=O3, Q3_1'=1+Q3_1, S3'=K4, U3'=1+U3, V3'=W3, X3'=Y3, Z3'=A4, B4'=C4, D4'=E4, F4'=H4, G4'=1+G4, Q4'=J4, L4'=1+L4, M4'=1+L4, N4'=1+Q3_1, O4'=1+U3, P4'=1+G4, [ F4>=1+L4 && 2>=L4+Q3_1 && S2>=2+2*U3 && 1+U2>=2*G4 ], cost: 4 842: f57 -> f1 : A'=X, B'=C, D'=E, F'=G, H'=Q, J'=K, L'=N, M'=Z, O'=P, Q_1'=R, S'=T, U'=V, W'=T1, Y'=Q1_1, A1'=V1, B1'=C1, D1'=E1, F1'=G1, H1'=Q1, J1'=K1, L1'=N1, M1'=X1, O1'=P1, R1'=S1, U1'=R2, W1'=O2, Y1'=T2, Z1'=A2, B2'=C2, D2'=E2, F2'=G2, H2'=Q2, J2'=L2, K2'=V2, M2'=N2, P2'=Q2_1, S2'=P3, U2'=M3, W2'=R3, X2'=Y2, Z2'=A3, B3'=C3, D3'=E3, F3'=G3, H3'=J3, Q3'=T3, K3'=L3, N3'=O3, Q3_1'=1+Q3_1, S3'=K4, U3'=1+U3, V3'=W3, X3'=Y3, Z3'=A4, B4'=C4, D4'=E4, F4'=H4, G4'=-1+G4, Q4'=J4, L4'=1+L4, M4'=1+L4, N4'=1+Q3_1, O4'=1+U3, P4'=-1+G4, [ F4>=1+L4 && 2>=L4+Q3_1 && S2>=2+2*U3 && 2*G4>=4+U2 ], cost: 4 844: f57 -> f1 : A'=X, B'=C, D'=E, F'=G, H'=Q, J'=K, L'=N, M'=Z, O'=P, Q_1'=R, S'=T, U'=V, W'=T1, Y'=Q1_1, A1'=V1, B1'=C1, D1'=E1, F1'=G1, H1'=Q1, J1'=K1, L1'=N1, M1'=X1, O1'=P1, R1'=S1, U1'=R2, W1'=O2, Y1'=T2, Z1'=A2, B2'=C2, D2'=E2, F2'=G2, H2'=Q2, J2'=L2, K2'=V2, M2'=N2, P2'=Q2_1, S2'=P3, U2'=M3, W2'=R3, X2'=Y2, Z2'=A3, B3'=C3, D3'=E3, F3'=G3, H3'=J3, Q3'=T3, K3'=L3, N3'=O3, Q3_1'=1+Q3_1, S3'=K4, U3'=-1+U3, V3'=W3, X3'=Y3, Z3'=A4, B4'=C4, D4'=E4, F4'=H4, G4'=-1+G4, Q4'=J4, L4'=1+L4, M4'=1+L4, N4'=1+Q3_1, O4'=-1+U3, P4'=-1+G4, [ F4>=1+L4 && 2>=L4+Q3_1 && 2*U3>=1+S2 && 2*G4>=4+U2 ], cost: 4 848: f57 -> f1 : A'=X, B'=C, D'=E, F'=G, H'=Q, J'=K, L'=N, M'=Z, O'=P, Q_1'=R, S'=T, U'=V, W'=T1, Y'=Q1_1, A1'=V1, B1'=C1, D1'=E1, F1'=G1, H1'=Q1, J1'=K1, L1'=N1, M1'=X1, O1'=P1, R1'=S1, U1'=R2, W1'=O2, Y1'=T2, Z1'=A2, B2'=C2, D2'=E2, F2'=G2, H2'=Q2, J2'=L2, K2'=V2, M2'=N2, P2'=Q2_1, S2'=P3, U2'=M3, W2'=R3, X2'=Y2, Z2'=A3, B3'=C3, D3'=E3, F3'=G3, H3'=J3, Q3'=T3, K3'=L3, N3'=O3, Q3_1'=-1+Q3_1, S3'=K4, U3'=-1+U3, V3'=W3, X3'=Y3, Z3'=A4, B4'=C4, D4'=E4, F4'=H4, G4'=1+G4, Q4'=J4, L4'=1+L4, M4'=1+L4, N4'=-1+Q3_1, O4'=-1+U3, P4'=1+G4, [ F4>=1+L4 && L4+Q3_1>=4 && 2*U3>=1+S2 && 1+U2>=2*G4 ], cost: 4 853: f57 -> f1 : A'=X, B'=C, D'=E, F'=G, H'=Q, J'=K, L'=N, M'=Z, O'=P, Q_1'=R, S'=T, U'=V, W'=T1, Y'=Q1_1, A1'=V1, B1'=C1, D1'=E1, F1'=G1, H1'=Q1, J1'=K1, L1'=N1, M1'=X1, O1'=P1, R1'=S1, U1'=R2, W1'=O2, Y1'=T2, Z1'=A2, B2'=C2, D2'=E2, F2'=G2, H2'=Q2, J2'=L2, K2'=V2, M2'=N2, P2'=Q2_1, S2'=P3, U2'=M3, W2'=R3, X2'=Y2, Z2'=A3, B3'=C3, D3'=E3, F3'=G3, H3'=J3, Q3'=T3, K3'=L3, N3'=O3, Q3_1'=1+Q3_1, S3'=K4, U3'=-1+U3, V3'=W3, X3'=Y3, Z3'=A4, B4'=C4, D4'=E4, F4'=H4, G4'=1+G4, Q4'=J4, L4'=-1+L4, M4'=-1+L4, N4'=1+Q3_1, O4'=-1+U3, P4'=1+G4, [ L4>=1+F4 && 2>=L4+Q3_1 && 2*U3>=1+S2 && 1+U2>=2*G4 ], cost: 4 Applied chaining over branches and pruning: Start location: f0 0: f0 -> f1 : [], cost: 1 866: f1 -> f9 : C'=1+B, E'=1+D, G'=1+F, Q'=1+H, K'=1+J, N'=1+L, P'=1+O, R'=1+Q_1, [ A>=1+B && B>=1+D && 2>=F+D && 2>=H+F && H>=1+J && 0>=1+L && M>=1+L && L>=1+O && O+J>=1+2*Q_1 ], cost: 8 867: f1 -> f9 : C'=1+B, E'=1+D, G'=1+F, Q'=1+H, K'=1+J, N'=1+L, P'=1+O, R'=-1+Q_1, [ A>=1+B && B>=1+D && 2>=F+D && 2>=H+F && H>=1+J && 0>=1+L && M>=1+L && L>=1+O && 2*Q_1>=2+O+J ], cost: 8 869: f1 -> f9 : C'=1+B, E'=1+D, G'=1+F, Q'=1+H, K'=1+J, N'=-1+L, P'=-1+O, R'=1+Q_1, [ A>=1+B && B>=1+D && 2>=F+D && 2>=H+F && H>=1+J && L>=1 && O>=1+L && O+J>=1+2*Q_1 ], cost: 8 873: f1 -> f9 : C'=1+B, E'=1+D, G'=1+F, Q'=-1+H, K'=1+J, N'=1+L, P'=-1+O, R'=-1+Q_1, [ A>=1+B && B>=1+D && 2>=F+D && H+F>=4 && H>=1+J && 0>=1+L && M>=1+L && O>=1+L && 2*Q_1>=2+O+J ], cost: 8 878: f1 -> f9 : C'=1+B, E'=1+D, G'=-1+F, Q'=-1+H, K'=1+J, N'=1+L, P'=-1+O, R'=-1+Q_1, [ A>=1+B && B>=1+D && F+D>=4 && H+F>=4 && H>=1+J && 0>=1+L && M>=1+L && O>=1+L && 2*Q_1>=2+O+J ], cost: 8 891: f9 -> f17 : T'=1+S, V'=1+U, X'=1+A, Z'=1+M, C1'=1+B1, E1'=1+D1, G1'=1+F1, Q1'=1+H1, [ L>=1+S && 2>=U+S && 1+W>=2*A && 1+Y>=2*M && A1>=1+B1 && B1>=1+D1 && 2>=F1+D1 && 2>=H1+F1 ], cost: 8 892: f9 -> f17 : T'=1+S, V'=1+U, X'=1+A, Z'=1+M, C1'=1+B1, E1'=1+D1, G1'=1+F1, Q1'=-1+H1, [ L>=1+S && 2>=U+S && 1+W>=2*A && 1+Y>=2*M && A1>=1+B1 && B1>=1+D1 && 2>=F1+D1 && H1+F1>=4 ], cost: 8 894: f9 -> f17 : T'=1+S, V'=1+U, X'=1+A, Z'=1+M, C1'=1+B1, E1'=-1+D1, G1'=-1+F1, Q1'=1+H1, [ L>=1+S && 2>=U+S && 1+W>=2*A && 1+Y>=2*M && A1>=1+B1 && D1>=1+B1 && F1+D1>=4 && 2>=H1+F1 ], cost: 8 898: f9 -> f17 : T'=1+S, V'=1+U, X'=1+A, Z'=-1+M, C1'=1+B1, E1'=1+D1, G1'=-1+F1, Q1'=-1+H1, [ L>=1+S && 2>=U+S && 1+W>=2*A && 2*M>=4+Y && A1>=1+B1 && B1>=1+D1 && F1+D1>=4 && H1+F1>=4 ], cost: 8 903: f9 -> f17 : T'=1+S, V'=1+U, X'=-1+A, Z'=-1+M, C1'=1+B1, E1'=1+D1, G1'=-1+F1, Q1'=-1+H1, [ L>=1+S && 2>=U+S && 2*A>=4+W && 2*M>=4+Y && A1>=1+B1 && B1>=1+D1 && F1+D1>=4 && H1+F1>=4 ], cost: 8 916: f17 -> f25 : K1'=1+J1, N1'=1+L1, P1'=1+O1, Q1_1'=1+Y, S1'=1+R1, T1'=1+W, V1'=1+A1, X1'=1+M1, [ H1>=1+J1 && 1>=L1 && M1>=1+L1 && L1>=1+O1 && O1+J1>=1+2*Y && L1>=1+R1 && 2>=R1+W && U+U1>=2+2*A1 && Q_1+W1>=1+2*M1 ], cost: 8 917: f17 -> f25 : K1'=1+J1, N1'=1+L1, P1'=1+O1, Q1_1'=1+Y, S1'=1+R1, T1'=1+W, V1'=1+A1, X1'=-1+M1, [ H1>=1+J1 && 1>=L1 && M1>=1+L1 && L1>=1+O1 && O1+J1>=1+2*Y && L1>=1+R1 && 2>=R1+W && U+U1>=2+2*A1 && 2*M1>=2+Q_1+W1 ], cost: 8 919: f17 -> f25 : K1'=1+J1, N1'=1+L1, P1'=1+O1, Q1_1'=1+Y, S1'=1+R1, T1'=-1+W, V1'=-1+A1, X1'=1+M1, [ H1>=1+J1 && 1>=L1 && M1>=1+L1 && L1>=1+O1 && O1+J1>=1+2*Y && L1>=1+R1 && R1+W>=4 && 2*A1>=1+U+U1 && Q_1+W1>=1+2*M1 ], cost: 8 923: f17 -> f25 : K1'=1+J1, N1'=1+L1, P1'=1+O1, Q1_1'=-1+Y, S1'=1+R1, T1'=1+W, V1'=-1+A1, X1'=-1+M1, [ H1>=1+J1 && 1>=L1 && M1>=1+L1 && L1>=1+O1 && 2*Y>=2+O1+J1 && L1>=1+R1 && 2>=R1+W && 2*A1>=1+U+U1 && 2*M1>=2+Q_1+W1 ], cost: 8 928: f17 -> f25 : K1'=1+J1, N1'=1+L1, P1'=-1+O1, Q1_1'=-1+Y, S1'=1+R1, T1'=1+W, V1'=-1+A1, X1'=-1+M1, [ H1>=1+J1 && 1>=L1 && M1>=1+L1 && O1>=1+L1 && 2*Y>=2+O1+J1 && L1>=1+R1 && 2>=R1+W && 2*A1>=1+U+U1 && 2*M1>=2+Q_1+W1 ], cost: 8 941: f25 -> f33 : A2'=1+Z1, C2'=1+B2, E2'=1+D2, G2'=1+F2, Q2'=1+H2, L2'=1+J2, N2'=1+M2, O2'=1+W1, [ Y1>=1+Z1 && Z1>=1+B2 && 2>=D2+B2 && 2>=D2+F2 && F2>=1+H2 && 2>=J2 && K2>=1+J2 && J2>=1+M2 && M2+H2>=1+2*W1 ], cost: 8 942: f25 -> f33 : A2'=1+Z1, C2'=1+B2, E2'=1+D2, G2'=1+F2, Q2'=1+H2, L2'=1+J2, N2'=1+M2, O2'=-1+W1, [ Y1>=1+Z1 && Z1>=1+B2 && 2>=D2+B2 && 2>=D2+F2 && F2>=1+H2 && 2>=J2 && K2>=1+J2 && J2>=1+M2 && 2*W1>=2+M2+H2 ], cost: 8 944: f25 -> f33 : A2'=1+Z1, C2'=1+B2, E2'=1+D2, G2'=1+F2, Q2'=1+H2, L2'=-1+J2, N2'=-1+M2, O2'=1+W1, [ Y1>=1+Z1 && Z1>=1+B2 && 2>=D2+B2 && 2>=D2+F2 && F2>=1+H2 && J2>=4 && M2>=1+J2 && M2+H2>=1+2*W1 ], cost: 8 948: f25 -> f33 : A2'=1+Z1, C2'=1+B2, E2'=1+D2, G2'=-1+F2, Q2'=1+H2, L2'=1+J2, N2'=-1+M2, O2'=-1+W1, [ Y1>=1+Z1 && Z1>=1+B2 && 2>=D2+B2 && D2+F2>=4 && F2>=1+H2 && 2>=J2 && K2>=1+J2 && M2>=1+J2 && 2*W1>=2+M2+H2 ], cost: 8 953: f25 -> f33 : A2'=1+Z1, C2'=1+B2, E2'=-1+D2, G2'=-1+F2, Q2'=1+H2, L2'=1+J2, N2'=-1+M2, O2'=-1+W1, [ Y1>=1+Z1 && Z1>=1+B2 && D2+B2>=4 && D2+F2>=4 && F2>=1+H2 && 2>=J2 && K2>=1+J2 && M2>=1+J2 && 2*W1>=2+M2+H2 ], cost: 8 966: f33 -> f41 : Q2_1'=1+P2, R2'=1+U1, T2'=1+Y1, V2'=1+K2, Y2'=1+X2, A3'=1+Z2, C3'=1+B3, E3'=1+D3, [ J2>=1+P2 && 2>=P2+U1 && S2+W>=2+2*Y1 && Y+U2>=1+2*K2 && W2>=1+X2 && X2>=1+Z2 && 2>=Z2+B3 && 2>=D3+B3 ], cost: 8 967: f33 -> f41 : Q2_1'=1+P2, R2'=1+U1, T2'=1+Y1, V2'=1+K2, Y2'=1+X2, A3'=1+Z2, C3'=1+B3, E3'=-1+D3, [ J2>=1+P2 && 2>=P2+U1 && S2+W>=2+2*Y1 && Y+U2>=1+2*K2 && W2>=1+X2 && X2>=1+Z2 && 2>=Z2+B3 && D3+B3>=4 ], cost: 8 969: f33 -> f41 : Q2_1'=1+P2, R2'=1+U1, T2'=1+Y1, V2'=1+K2, Y2'=1+X2, A3'=-1+Z2, C3'=-1+B3, E3'=1+D3, [ J2>=1+P2 && 2>=P2+U1 && S2+W>=2+2*Y1 && Y+U2>=1+2*K2 && W2>=1+X2 && Z2>=1+X2 && Z2+B3>=4 && 2>=D3+B3 ], cost: 8 973: f33 -> f41 : Q2_1'=1+P2, R2'=1+U1, T2'=1+Y1, V2'=-1+K2, Y2'=1+X2, A3'=1+Z2, C3'=-1+B3, E3'=-1+D3, [ J2>=1+P2 && 2>=P2+U1 && S2+W>=2+2*Y1 && 2*K2>=2+Y+U2 && W2>=1+X2 && X2>=1+Z2 && Z2+B3>=4 && D3+B3>=4 ], cost: 8 978: f33 -> f41 : Q2_1'=1+P2, R2'=1+U1, T2'=-1+Y1, V2'=-1+K2, Y2'=1+X2, A3'=1+Z2, C3'=-1+B3, E3'=-1+D3, [ J2>=1+P2 && 2>=P2+U1 && 2*Y1>=1+S2+W && 2*K2>=2+Y+U2 && W2>=1+X2 && X2>=1+Z2 && Z2+B3>=4 && D3+B3>=4 ], cost: 8 991: f41 -> f49 : G3'=1+F3, J3'=1+H3, L3'=1+K3, M3'=1+U2, O3'=1+N3, P3'=1+S2, R3'=1+W2, T3'=1+Q3, [ D3>=1+F3 && 2>=H3 && Q3>=1+H3 && H3>=1+K3 && F3+K3>=1+2*U2 && H3>=1+N3 && 2>=S2+N3 && U1+Q3_1>=2+2*W2 && S3+W1>=1+2*Q3 ], cost: 8 992: f41 -> f49 : G3'=1+F3, J3'=1+H3, L3'=1+K3, M3'=1+U2, O3'=1+N3, P3'=1+S2, R3'=1+W2, T3'=-1+Q3, [ D3>=1+F3 && 2>=H3 && Q3>=1+H3 && H3>=1+K3 && F3+K3>=1+2*U2 && H3>=1+N3 && 2>=S2+N3 && U1+Q3_1>=2+2*W2 && 2*Q3>=2+S3+W1 ], cost: 8 994: f41 -> f49 : G3'=1+F3, J3'=1+H3, L3'=1+K3, M3'=1+U2, O3'=1+N3, P3'=-1+S2, R3'=-1+W2, T3'=1+Q3, [ D3>=1+F3 && 2>=H3 && Q3>=1+H3 && H3>=1+K3 && F3+K3>=1+2*U2 && H3>=1+N3 && S2+N3>=4 && 2*W2>=1+U1+Q3_1 && S3+W1>=1+2*Q3 ], cost: 8 998: f41 -> f49 : G3'=1+F3, J3'=1+H3, L3'=1+K3, M3'=-1+U2, O3'=1+N3, P3'=1+S2, R3'=-1+W2, T3'=-1+Q3, [ D3>=1+F3 && 2>=H3 && Q3>=1+H3 && H3>=1+K3 && 2*U2>=2+F3+K3 && H3>=1+N3 && 2>=S2+N3 && 2*W2>=1+U1+Q3_1 && 2*Q3>=2+S3+W1 ], cost: 8 1003: f41 -> f49 : G3'=1+F3, J3'=1+H3, L3'=-1+K3, M3'=-1+U2, O3'=1+N3, P3'=1+S2, R3'=-1+W2, T3'=-1+Q3, [ D3>=1+F3 && 2>=H3 && Q3>=1+H3 && K3>=1+H3 && 2*U2>=2+F3+K3 && H3>=1+N3 && 2>=S2+N3 && 2*W2>=1+U1+Q3_1 && 2*Q3>=2+S3+W1 ], cost: 8 1016: f49 -> f57 : W3'=1+V3, Y3'=1+X3, A4'=1+Z3, C4'=1+B4, E4'=1+D4, H4'=1+F4, J4'=1+Q4, K4'=1+S3, [ U3>=1+V3 && V3>=1+X3 && 2>=Z3+X3 && 2>=Z3+B4 && B4>=1+D4 && 2>=F4 && G4>=1+F4 && F4>=1+Q4 && Q4+D4>=1+2*S3 ], cost: 8 1017: f49 -> f57 : W3'=1+V3, Y3'=1+X3, A4'=1+Z3, C4'=1+B4, E4'=1+D4, H4'=1+F4, J4'=1+Q4, K4'=-1+S3, [ U3>=1+V3 && V3>=1+X3 && 2>=Z3+X3 && 2>=Z3+B4 && B4>=1+D4 && 2>=F4 && G4>=1+F4 && F4>=1+Q4 && 2*S3>=2+Q4+D4 ], cost: 8 1019: f49 -> f57 : W3'=1+V3, Y3'=1+X3, A4'=1+Z3, C4'=1+B4, E4'=1+D4, H4'=-1+F4, J4'=-1+Q4, K4'=1+S3, [ U3>=1+V3 && V3>=1+X3 && 2>=Z3+X3 && 2>=Z3+B4 && B4>=1+D4 && F4>=4 && Q4>=1+F4 && Q4+D4>=1+2*S3 ], cost: 8 1023: f49 -> f57 : W3'=1+V3, Y3'=1+X3, A4'=1+Z3, C4'=-1+B4, E4'=1+D4, H4'=1+F4, J4'=-1+Q4, K4'=-1+S3, [ U3>=1+V3 && V3>=1+X3 && 2>=Z3+X3 && Z3+B4>=4 && B4>=1+D4 && 2>=F4 && G4>=1+F4 && Q4>=1+F4 && 2*S3>=2+Q4+D4 ], cost: 8 1028: f49 -> f57 : W3'=1+V3, Y3'=1+X3, A4'=-1+Z3, C4'=-1+B4, E4'=1+D4, H4'=1+F4, J4'=-1+Q4, K4'=-1+S3, [ U3>=1+V3 && V3>=1+X3 && Z3+X3>=4 && Z3+B4>=4 && B4>=1+D4 && 2>=F4 && G4>=1+F4 && Q4>=1+F4 && 2*S3>=2+Q4+D4 ], cost: 8 841: f57 -> f1 : A'=X, B'=C, D'=E, F'=G, H'=Q, J'=K, L'=N, M'=Z, O'=P, Q_1'=R, S'=T, U'=V, W'=T1, Y'=Q1_1, A1'=V1, B1'=C1, D1'=E1, F1'=G1, H1'=Q1, J1'=K1, L1'=N1, M1'=X1, O1'=P1, R1'=S1, U1'=R2, W1'=O2, Y1'=T2, Z1'=A2, B2'=C2, D2'=E2, F2'=G2, H2'=Q2, J2'=L2, K2'=V2, M2'=N2, P2'=Q2_1, S2'=P3, U2'=M3, W2'=R3, X2'=Y2, Z2'=A3, B3'=C3, D3'=E3, F3'=G3, H3'=J3, Q3'=T3, K3'=L3, N3'=O3, Q3_1'=1+Q3_1, S3'=K4, U3'=1+U3, V3'=W3, X3'=Y3, Z3'=A4, B4'=C4, D4'=E4, F4'=H4, G4'=1+G4, Q4'=J4, L4'=1+L4, M4'=1+L4, N4'=1+Q3_1, O4'=1+U3, P4'=1+G4, [ F4>=1+L4 && 2>=L4+Q3_1 && S2>=2+2*U3 && 1+U2>=2*G4 ], cost: 4 842: f57 -> f1 : A'=X, B'=C, D'=E, F'=G, H'=Q, J'=K, L'=N, M'=Z, O'=P, Q_1'=R, S'=T, U'=V, W'=T1, Y'=Q1_1, A1'=V1, B1'=C1, D1'=E1, F1'=G1, H1'=Q1, J1'=K1, L1'=N1, M1'=X1, O1'=P1, R1'=S1, U1'=R2, W1'=O2, Y1'=T2, Z1'=A2, B2'=C2, D2'=E2, F2'=G2, H2'=Q2, J2'=L2, K2'=V2, M2'=N2, P2'=Q2_1, S2'=P3, U2'=M3, W2'=R3, X2'=Y2, Z2'=A3, B3'=C3, D3'=E3, F3'=G3, H3'=J3, Q3'=T3, K3'=L3, N3'=O3, Q3_1'=1+Q3_1, S3'=K4, U3'=1+U3, V3'=W3, X3'=Y3, Z3'=A4, B4'=C4, D4'=E4, F4'=H4, G4'=-1+G4, Q4'=J4, L4'=1+L4, M4'=1+L4, N4'=1+Q3_1, O4'=1+U3, P4'=-1+G4, [ F4>=1+L4 && 2>=L4+Q3_1 && S2>=2+2*U3 && 2*G4>=4+U2 ], cost: 4 844: f57 -> f1 : A'=X, B'=C, D'=E, F'=G, H'=Q, J'=K, L'=N, M'=Z, O'=P, Q_1'=R, S'=T, U'=V, W'=T1, Y'=Q1_1, A1'=V1, B1'=C1, D1'=E1, F1'=G1, H1'=Q1, J1'=K1, L1'=N1, M1'=X1, O1'=P1, R1'=S1, U1'=R2, W1'=O2, Y1'=T2, Z1'=A2, B2'=C2, D2'=E2, F2'=G2, H2'=Q2, J2'=L2, K2'=V2, M2'=N2, P2'=Q2_1, S2'=P3, U2'=M3, W2'=R3, X2'=Y2, Z2'=A3, B3'=C3, D3'=E3, F3'=G3, H3'=J3, Q3'=T3, K3'=L3, N3'=O3, Q3_1'=1+Q3_1, S3'=K4, U3'=-1+U3, V3'=W3, X3'=Y3, Z3'=A4, B4'=C4, D4'=E4, F4'=H4, G4'=-1+G4, Q4'=J4, L4'=1+L4, M4'=1+L4, N4'=1+Q3_1, O4'=-1+U3, P4'=-1+G4, [ F4>=1+L4 && 2>=L4+Q3_1 && 2*U3>=1+S2 && 2*G4>=4+U2 ], cost: 4 848: f57 -> f1 : A'=X, B'=C, D'=E, F'=G, H'=Q, J'=K, L'=N, M'=Z, O'=P, Q_1'=R, S'=T, U'=V, W'=T1, Y'=Q1_1, A1'=V1, B1'=C1, D1'=E1, F1'=G1, H1'=Q1, J1'=K1, L1'=N1, M1'=X1, O1'=P1, R1'=S1, U1'=R2, W1'=O2, Y1'=T2, Z1'=A2, B2'=C2, D2'=E2, F2'=G2, H2'=Q2, J2'=L2, K2'=V2, M2'=N2, P2'=Q2_1, S2'=P3, U2'=M3, W2'=R3, X2'=Y2, Z2'=A3, B3'=C3, D3'=E3, F3'=G3, H3'=J3, Q3'=T3, K3'=L3, N3'=O3, Q3_1'=-1+Q3_1, S3'=K4, U3'=-1+U3, V3'=W3, X3'=Y3, Z3'=A4, B4'=C4, D4'=E4, F4'=H4, G4'=1+G4, Q4'=J4, L4'=1+L4, M4'=1+L4, N4'=-1+Q3_1, O4'=-1+U3, P4'=1+G4, [ F4>=1+L4 && L4+Q3_1>=4 && 2*U3>=1+S2 && 1+U2>=2*G4 ], cost: 4 853: f57 -> f1 : A'=X, B'=C, D'=E, F'=G, H'=Q, J'=K, L'=N, M'=Z, O'=P, Q_1'=R, S'=T, U'=V, W'=T1, Y'=Q1_1, A1'=V1, B1'=C1, D1'=E1, F1'=G1, H1'=Q1, J1'=K1, L1'=N1, M1'=X1, O1'=P1, R1'=S1, U1'=R2, W1'=O2, Y1'=T2, Z1'=A2, B2'=C2, D2'=E2, F2'=G2, H2'=Q2, J2'=L2, K2'=V2, M2'=N2, P2'=Q2_1, S2'=P3, U2'=M3, W2'=R3, X2'=Y2, Z2'=A3, B3'=C3, D3'=E3, F3'=G3, H3'=J3, Q3'=T3, K3'=L3, N3'=O3, Q3_1'=1+Q3_1, S3'=K4, U3'=-1+U3, V3'=W3, X3'=Y3, Z3'=A4, B4'=C4, D4'=E4, F4'=H4, G4'=1+G4, Q4'=J4, L4'=-1+L4, M4'=-1+L4, N4'=1+Q3_1, O4'=-1+U3, P4'=1+G4, [ L4>=1+F4 && 2>=L4+Q3_1 && 2*U3>=1+S2 && 1+U2>=2*G4 ], cost: 4 Applied chaining over branches and pruning: Start location: f0 0: f0 -> f1 : [], cost: 1 1041: f1 -> f17 : C'=1+B, E'=1+D, G'=1+F, Q'=1+H, K'=1+J, N'=1+L, P'=1+O, R'=1+Q_1, T'=1+S, V'=1+U, X'=1+A, Z'=1+M, C1'=1+B1, E1'=1+D1, G1'=1+F1, Q1'=1+H1, [ A>=1+B && B>=1+D && 2>=F+D && 2>=H+F && H>=1+J && 0>=1+L && M>=1+L && L>=1+O && O+J>=1+2*Q_1 && L>=1+S && 2>=U+S && 1+W>=2*A && 1+Y>=2*M && A1>=1+B1 && B1>=1+D1 && 2>=F1+D1 && 2>=H1+F1 ], cost: 16 1042: f1 -> f17 : C'=1+B, E'=1+D, G'=1+F, Q'=1+H, K'=1+J, N'=1+L, P'=1+O, R'=1+Q_1, T'=1+S, V'=1+U, X'=1+A, Z'=1+M, C1'=1+B1, E1'=1+D1, G1'=1+F1, Q1'=-1+H1, [ A>=1+B && B>=1+D && 2>=F+D && 2>=H+F && H>=1+J && 0>=1+L && M>=1+L && L>=1+O && O+J>=1+2*Q_1 && L>=1+S && 2>=U+S && 1+W>=2*A && 1+Y>=2*M && A1>=1+B1 && B1>=1+D1 && 2>=F1+D1 && H1+F1>=4 ], cost: 16 1044: f1 -> f17 : C'=1+B, E'=1+D, G'=1+F, Q'=1+H, K'=1+J, N'=1+L, P'=1+O, R'=1+Q_1, T'=1+S, V'=1+U, X'=1+A, Z'=-1+M, C1'=1+B1, E1'=1+D1, G1'=-1+F1, Q1'=-1+H1, [ A>=1+B && B>=1+D && 2>=F+D && 2>=H+F && H>=1+J && 0>=1+L && M>=1+L && L>=1+O && O+J>=1+2*Q_1 && L>=1+S && 2>=U+S && 1+W>=2*A && 2*M>=4+Y && A1>=1+B1 && B1>=1+D1 && F1+D1>=4 && H1+F1>=4 ], cost: 16 1048: f1 -> f17 : C'=1+B, E'=1+D, G'=1+F, Q'=1+H, K'=1+J, N'=1+L, P'=1+O, R'=-1+Q_1, T'=1+S, V'=1+U, X'=1+A, Z'=1+M, C1'=1+B1, E1'=-1+D1, G1'=-1+F1, Q1'=1+H1, [ A>=1+B && B>=1+D && 2>=F+D && 2>=H+F && H>=1+J && 0>=1+L && M>=1+L && L>=1+O && 2*Q_1>=2+O+J && L>=1+S && 2>=U+S && 1+W>=2*A && 1+Y>=2*M && A1>=1+B1 && D1>=1+B1 && F1+D1>=4 && 2>=H1+F1 ], cost: 16 1053: f1 -> f17 : C'=1+B, E'=1+D, G'=1+F, Q'=1+H, K'=1+J, N'=-1+L, P'=-1+O, R'=1+Q_1, T'=1+S, V'=1+U, X'=1+A, Z'=1+M, C1'=1+B1, E1'=-1+D1, G1'=-1+F1, Q1'=1+H1, [ A>=1+B && B>=1+D && 2>=F+D && 2>=H+F && H>=1+J && L>=1 && O>=1+L && O+J>=1+2*Q_1 && L>=1+S && 2>=U+S && 1+W>=2*A && 1+Y>=2*M && A1>=1+B1 && D1>=1+B1 && F1+D1>=4 && 2>=H1+F1 ], cost: 16 1066: f17 -> f33 : K1'=1+J1, N1'=1+L1, P1'=1+O1, Q1_1'=1+Y, S1'=1+R1, T1'=1+W, V1'=1+A1, X1'=1+M1, A2'=1+Z1, C2'=1+B2, E2'=1+D2, G2'=1+F2, Q2'=1+H2, L2'=1+J2, N2'=1+M2, O2'=1+W1, [ H1>=1+J1 && 1>=L1 && M1>=1+L1 && L1>=1+O1 && O1+J1>=1+2*Y && L1>=1+R1 && 2>=R1+W && U+U1>=2+2*A1 && Q_1+W1>=1+2*M1 && Y1>=1+Z1 && Z1>=1+B2 && 2>=D2+B2 && 2>=D2+F2 && F2>=1+H2 && 2>=J2 && K2>=1+J2 && J2>=1+M2 && M2+H2>=1+2*W1 ], cost: 16 1067: f17 -> f33 : K1'=1+J1, N1'=1+L1, P1'=1+O1, Q1_1'=1+Y, S1'=1+R1, T1'=1+W, V1'=1+A1, X1'=1+M1, A2'=1+Z1, C2'=1+B2, E2'=1+D2, G2'=1+F2, Q2'=1+H2, L2'=1+J2, N2'=1+M2, O2'=-1+W1, [ H1>=1+J1 && 1>=L1 && M1>=1+L1 && L1>=1+O1 && O1+J1>=1+2*Y && L1>=1+R1 && 2>=R1+W && U+U1>=2+2*A1 && Q_1+W1>=1+2*M1 && Y1>=1+Z1 && Z1>=1+B2 && 2>=D2+B2 && 2>=D2+F2 && F2>=1+H2 && 2>=J2 && K2>=1+J2 && J2>=1+M2 && 2*W1>=2+M2+H2 ], cost: 16 1069: f17 -> f33 : K1'=1+J1, N1'=1+L1, P1'=1+O1, Q1_1'=1+Y, S1'=1+R1, T1'=1+W, V1'=1+A1, X1'=1+M1, A2'=1+Z1, C2'=1+B2, E2'=1+D2, G2'=-1+F2, Q2'=1+H2, L2'=1+J2, N2'=-1+M2, O2'=-1+W1, [ H1>=1+J1 && 1>=L1 && M1>=1+L1 && L1>=1+O1 && O1+J1>=1+2*Y && L1>=1+R1 && 2>=R1+W && U+U1>=2+2*A1 && Q_1+W1>=1+2*M1 && Y1>=1+Z1 && Z1>=1+B2 && 2>=D2+B2 && D2+F2>=4 && F2>=1+H2 && 2>=J2 && K2>=1+J2 && M2>=1+J2 && 2*W1>=2+M2+H2 ], cost: 16 1073: f17 -> f33 : K1'=1+J1, N1'=1+L1, P1'=1+O1, Q1_1'=1+Y, S1'=1+R1, T1'=1+W, V1'=1+A1, X1'=-1+M1, A2'=1+Z1, C2'=1+B2, E2'=1+D2, G2'=1+F2, Q2'=1+H2, L2'=-1+J2, N2'=-1+M2, O2'=1+W1, [ H1>=1+J1 && 1>=L1 && M1>=1+L1 && L1>=1+O1 && O1+J1>=1+2*Y && L1>=1+R1 && 2>=R1+W && U+U1>=2+2*A1 && 2*M1>=2+Q_1+W1 && Y1>=1+Z1 && Z1>=1+B2 && 2>=D2+B2 && 2>=D2+F2 && F2>=1+H2 && J2>=4 && M2>=1+J2 && M2+H2>=1+2*W1 ], cost: 16 1078: f17 -> f33 : K1'=1+J1, N1'=1+L1, P1'=1+O1, Q1_1'=1+Y, S1'=1+R1, T1'=-1+W, V1'=-1+A1, X1'=1+M1, A2'=1+Z1, C2'=1+B2, E2'=1+D2, G2'=1+F2, Q2'=1+H2, L2'=-1+J2, N2'=-1+M2, O2'=1+W1, [ H1>=1+J1 && 1>=L1 && M1>=1+L1 && L1>=1+O1 && O1+J1>=1+2*Y && L1>=1+R1 && R1+W>=4 && 2*A1>=1+U+U1 && Q_1+W1>=1+2*M1 && Y1>=1+Z1 && Z1>=1+B2 && 2>=D2+B2 && 2>=D2+F2 && F2>=1+H2 && J2>=4 && M2>=1+J2 && M2+H2>=1+2*W1 ], cost: 16 1091: f33 -> f49 : Q2_1'=1+P2, R2'=1+U1, T2'=1+Y1, V2'=1+K2, Y2'=1+X2, A3'=1+Z2, C3'=1+B3, E3'=1+D3, G3'=1+F3, J3'=1+H3, L3'=1+K3, M3'=1+U2, O3'=1+N3, P3'=1+S2, R3'=1+W2, T3'=1+Q3, [ J2>=1+P2 && 2>=P2+U1 && S2+W>=2+2*Y1 && Y+U2>=1+2*K2 && W2>=1+X2 && X2>=1+Z2 && 2>=Z2+B3 && 2>=D3+B3 && D3>=1+F3 && 2>=H3 && Q3>=1+H3 && H3>=1+K3 && F3+K3>=1+2*U2 && H3>=1+N3 && 2>=S2+N3 && U1+Q3_1>=2+2*W2 && S3+W1>=1+2*Q3 ], cost: 16 1092: f33 -> f49 : Q2_1'=1+P2, R2'=1+U1, T2'=1+Y1, V2'=1+K2, Y2'=1+X2, A3'=1+Z2, C3'=1+B3, E3'=1+D3, G3'=1+F3, J3'=1+H3, L3'=1+K3, M3'=1+U2, O3'=1+N3, P3'=1+S2, R3'=1+W2, T3'=-1+Q3, [ J2>=1+P2 && 2>=P2+U1 && S2+W>=2+2*Y1 && Y+U2>=1+2*K2 && W2>=1+X2 && X2>=1+Z2 && 2>=Z2+B3 && 2>=D3+B3 && D3>=1+F3 && 2>=H3 && Q3>=1+H3 && H3>=1+K3 && F3+K3>=1+2*U2 && H3>=1+N3 && 2>=S2+N3 && U1+Q3_1>=2+2*W2 && 2*Q3>=2+S3+W1 ], cost: 16 1094: f33 -> f49 : Q2_1'=1+P2, R2'=1+U1, T2'=1+Y1, V2'=1+K2, Y2'=1+X2, A3'=1+Z2, C3'=1+B3, E3'=1+D3, G3'=1+F3, J3'=1+H3, L3'=1+K3, M3'=-1+U2, O3'=1+N3, P3'=1+S2, R3'=-1+W2, T3'=-1+Q3, [ J2>=1+P2 && 2>=P2+U1 && S2+W>=2+2*Y1 && Y+U2>=1+2*K2 && W2>=1+X2 && X2>=1+Z2 && 2>=Z2+B3 && 2>=D3+B3 && D3>=1+F3 && 2>=H3 && Q3>=1+H3 && H3>=1+K3 && 2*U2>=2+F3+K3 && H3>=1+N3 && 2>=S2+N3 && 2*W2>=1+U1+Q3_1 && 2*Q3>=2+S3+W1 ], cost: 16 1098: f33 -> f49 : Q2_1'=1+P2, R2'=1+U1, T2'=1+Y1, V2'=1+K2, Y2'=1+X2, A3'=1+Z2, C3'=1+B3, E3'=-1+D3, G3'=1+F3, J3'=1+H3, L3'=1+K3, M3'=1+U2, O3'=1+N3, P3'=-1+S2, R3'=-1+W2, T3'=1+Q3, [ J2>=1+P2 && 2>=P2+U1 && S2+W>=2+2*Y1 && Y+U2>=1+2*K2 && W2>=1+X2 && X2>=1+Z2 && 2>=Z2+B3 && D3+B3>=4 && D3>=1+F3 && 2>=H3 && Q3>=1+H3 && H3>=1+K3 && F3+K3>=1+2*U2 && H3>=1+N3 && S2+N3>=4 && 2*W2>=1+U1+Q3_1 && S3+W1>=1+2*Q3 ], cost: 16 1103: f33 -> f49 : Q2_1'=1+P2, R2'=1+U1, T2'=1+Y1, V2'=1+K2, Y2'=1+X2, A3'=-1+Z2, C3'=-1+B3, E3'=1+D3, G3'=1+F3, J3'=1+H3, L3'=1+K3, M3'=1+U2, O3'=1+N3, P3'=-1+S2, R3'=-1+W2, T3'=1+Q3, [ J2>=1+P2 && 2>=P2+U1 && S2+W>=2+2*Y1 && Y+U2>=1+2*K2 && W2>=1+X2 && Z2>=1+X2 && Z2+B3>=4 && 2>=D3+B3 && D3>=1+F3 && 2>=H3 && Q3>=1+H3 && H3>=1+K3 && F3+K3>=1+2*U2 && H3>=1+N3 && S2+N3>=4 && 2*W2>=1+U1+Q3_1 && S3+W1>=1+2*Q3 ], cost: 16 1116: f49 -> f1 : A'=X, B'=C, D'=E, F'=G, H'=Q, J'=K, L'=N, M'=Z, O'=P, Q_1'=R, S'=T, U'=V, W'=T1, Y'=Q1_1, A1'=V1, B1'=C1, D1'=E1, F1'=G1, H1'=Q1, J1'=K1, L1'=N1, M1'=X1, O1'=P1, R1'=S1, U1'=R2, W1'=O2, Y1'=T2, Z1'=A2, B2'=C2, D2'=E2, F2'=G2, H2'=Q2, J2'=L2, K2'=V2, M2'=N2, P2'=Q2_1, S2'=P3, U2'=M3, W2'=R3, X2'=Y2, Z2'=A3, B3'=C3, D3'=E3, F3'=G3, H3'=J3, Q3'=T3, K3'=L3, N3'=O3, Q3_1'=1+Q3_1, S3'=1+S3, U3'=1+U3, V3'=1+V3, W3'=1+V3, X3'=1+X3, Y3'=1+X3, Z3'=1+Z3, A4'=1+Z3, B4'=1+B4, C4'=1+B4, D4'=1+D4, E4'=1+D4, F4'=1+F4, G4'=1+G4, H4'=1+F4, Q4'=1+Q4, J4'=1+Q4, K4'=1+S3, L4'=1+L4, M4'=1+L4, N4'=1+Q3_1, O4'=1+U3, P4'=1+G4, [ U3>=1+V3 && V3>=1+X3 && 2>=Z3+X3 && 2>=Z3+B4 && B4>=1+D4 && 2>=F4 && G4>=1+F4 && F4>=1+Q4 && Q4+D4>=1+2*S3 && F4>=1+L4 && 2>=L4+Q3_1 && S2>=2+2*U3 && 1+U2>=2*G4 ], cost: 12 1117: f49 -> f1 : A'=X, B'=C, D'=E, F'=G, H'=Q, J'=K, L'=N, M'=Z, O'=P, Q_1'=R, S'=T, U'=V, W'=T1, Y'=Q1_1, A1'=V1, B1'=C1, D1'=E1, F1'=G1, H1'=Q1, J1'=K1, L1'=N1, M1'=X1, O1'=P1, R1'=S1, U1'=R2, W1'=O2, Y1'=T2, Z1'=A2, B2'=C2, D2'=E2, F2'=G2, H2'=Q2, J2'=L2, K2'=V2, M2'=N2, P2'=Q2_1, S2'=P3, U2'=M3, W2'=R3, X2'=Y2, Z2'=A3, B3'=C3, D3'=E3, F3'=G3, H3'=J3, Q3'=T3, K3'=L3, N3'=O3, Q3_1'=1+Q3_1, S3'=1+S3, U3'=1+U3, V3'=1+V3, W3'=1+V3, X3'=1+X3, Y3'=1+X3, Z3'=1+Z3, A4'=1+Z3, B4'=1+B4, C4'=1+B4, D4'=1+D4, E4'=1+D4, F4'=1+F4, G4'=-1+G4, H4'=1+F4, Q4'=1+Q4, J4'=1+Q4, K4'=1+S3, L4'=1+L4, M4'=1+L4, N4'=1+Q3_1, O4'=1+U3, P4'=-1+G4, [ U3>=1+V3 && V3>=1+X3 && 2>=Z3+X3 && 2>=Z3+B4 && B4>=1+D4 && 2>=F4 && G4>=1+F4 && F4>=1+Q4 && Q4+D4>=1+2*S3 && F4>=1+L4 && 2>=L4+Q3_1 && S2>=2+2*U3 && 2*G4>=4+U2 ], cost: 12 1119: f49 -> f1 : A'=X, B'=C, D'=E, F'=G, H'=Q, J'=K, L'=N, M'=Z, O'=P, Q_1'=R, S'=T, U'=V, W'=T1, Y'=Q1_1, A1'=V1, B1'=C1, D1'=E1, F1'=G1, H1'=Q1, J1'=K1, L1'=N1, M1'=X1, O1'=P1, R1'=S1, U1'=R2, W1'=O2, Y1'=T2, Z1'=A2, B2'=C2, D2'=E2, F2'=G2, H2'=Q2, J2'=L2, K2'=V2, M2'=N2, P2'=Q2_1, S2'=P3, U2'=M3, W2'=R3, X2'=Y2, Z2'=A3, B3'=C3, D3'=E3, F3'=G3, H3'=J3, Q3'=T3, K3'=L3, N3'=O3, Q3_1'=-1+Q3_1, S3'=1+S3, U3'=-1+U3, V3'=1+V3, W3'=1+V3, X3'=1+X3, Y3'=1+X3, Z3'=1+Z3, A4'=1+Z3, B4'=1+B4, C4'=1+B4, D4'=1+D4, E4'=1+D4, F4'=1+F4, G4'=1+G4, H4'=1+F4, Q4'=1+Q4, J4'=1+Q4, K4'=1+S3, L4'=1+L4, M4'=1+L4, N4'=-1+Q3_1, O4'=-1+U3, P4'=1+G4, [ U3>=1+V3 && V3>=1+X3 && 2>=Z3+X3 && 2>=Z3+B4 && B4>=1+D4 && 2>=F4 && G4>=1+F4 && F4>=1+Q4 && Q4+D4>=1+2*S3 && F4>=1+L4 && L4+Q3_1>=4 && 2*U3>=1+S2 && 1+U2>=2*G4 ], cost: 12 1123: f49 -> f1 : A'=X, B'=C, D'=E, F'=G, H'=Q, J'=K, L'=N, M'=Z, O'=P, Q_1'=R, S'=T, U'=V, W'=T1, Y'=Q1_1, A1'=V1, B1'=C1, D1'=E1, F1'=G1, H1'=Q1, J1'=K1, L1'=N1, M1'=X1, O1'=P1, R1'=S1, U1'=R2, W1'=O2, Y1'=T2, Z1'=A2, B2'=C2, D2'=E2, F2'=G2, H2'=Q2, J2'=L2, K2'=V2, M2'=N2, P2'=Q2_1, S2'=P3, U2'=M3, W2'=R3, X2'=Y2, Z2'=A3, B3'=C3, D3'=E3, F3'=G3, H3'=J3, Q3'=T3, K3'=L3, N3'=O3, Q3_1'=1+Q3_1, S3'=-1+S3, U3'=-1+U3, V3'=1+V3, W3'=1+V3, X3'=1+X3, Y3'=1+X3, Z3'=1+Z3, A4'=1+Z3, B4'=1+B4, C4'=1+B4, D4'=1+D4, E4'=1+D4, F4'=1+F4, G4'=-1+G4, H4'=1+F4, Q4'=1+Q4, J4'=1+Q4, K4'=-1+S3, L4'=1+L4, M4'=1+L4, N4'=1+Q3_1, O4'=-1+U3, P4'=-1+G4, [ U3>=1+V3 && V3>=1+X3 && 2>=Z3+X3 && 2>=Z3+B4 && B4>=1+D4 && 2>=F4 && G4>=1+F4 && F4>=1+Q4 && 2*S3>=2+Q4+D4 && F4>=1+L4 && 2>=L4+Q3_1 && 2*U3>=1+S2 && 2*G4>=4+U2 ], cost: 12 1128: f49 -> f1 : A'=X, B'=C, D'=E, F'=G, H'=Q, J'=K, L'=N, M'=Z, O'=P, Q_1'=R, S'=T, U'=V, W'=T1, Y'=Q1_1, A1'=V1, B1'=C1, D1'=E1, F1'=G1, H1'=Q1, J1'=K1, L1'=N1, M1'=X1, O1'=P1, R1'=S1, U1'=R2, W1'=O2, Y1'=T2, Z1'=A2, B2'=C2, D2'=E2, F2'=G2, H2'=Q2, J2'=L2, K2'=V2, M2'=N2, P2'=Q2_1, S2'=P3, U2'=M3, W2'=R3, X2'=Y2, Z2'=A3, B3'=C3, D3'=E3, F3'=G3, H3'=J3, Q3'=T3, K3'=L3, N3'=O3, Q3_1'=1+Q3_1, S3'=1+S3, U3'=-1+U3, V3'=1+V3, W3'=1+V3, X3'=1+X3, Y3'=1+X3, Z3'=1+Z3, A4'=1+Z3, B4'=1+B4, C4'=1+B4, D4'=1+D4, E4'=1+D4, F4'=-1+F4, G4'=-1+G4, H4'=-1+F4, Q4'=-1+Q4, J4'=-1+Q4, K4'=1+S3, L4'=1+L4, M4'=1+L4, N4'=1+Q3_1, O4'=-1+U3, P4'=-1+G4, [ U3>=1+V3 && V3>=1+X3 && 2>=Z3+X3 && 2>=Z3+B4 && B4>=1+D4 && F4>=4 && Q4>=1+F4 && Q4+D4>=1+2*S3 && F4>=1+L4 && 2>=L4+Q3_1 && 2*U3>=1+S2 && 2*G4>=4+U2 ], cost: 12 Applied chaining over branches and pruning: Start location: f0 0: f0 -> f1 : [], cost: 1 1141: f1 -> f33 : C'=1+B, E'=1+D, G'=1+F, Q'=1+H, K'=1+J, N'=1+L, P'=1+O, R'=1+Q_1, T'=1+S, V'=1+U, X'=1+A, Z'=1+M, C1'=1+B1, E1'=1+D1, G1'=1+F1, Q1'=1+H1, K1'=1+J1, N1'=1+L1, P1'=1+O1, Q1_1'=1+Y, S1'=1+R1, T1'=1+W, V1'=1+A1, X1'=1+M1, A2'=1+Z1, C2'=1+B2, E2'=1+D2, G2'=1+F2, Q2'=1+H2, L2'=1+J2, N2'=1+M2, O2'=1+W1, [ A>=1+B && B>=1+D && 2>=F+D && 2>=H+F && H>=1+J && 0>=1+L && M>=1+L && L>=1+O && O+J>=1+2*Q_1 && L>=1+S && 2>=U+S && 1+W>=2*A && 1+Y>=2*M && A1>=1+B1 && B1>=1+D1 && 2>=F1+D1 && 2>=H1+F1 && H1>=1+J1 && 1>=L1 && M1>=1+L1 && L1>=1+O1 && O1+J1>=1+2*Y && L1>=1+R1 && 2>=R1+W && U+U1>=2+2*A1 && Q_1+W1>=1+2*M1 && Y1>=1+Z1 && Z1>=1+B2 && 2>=D2+B2 && 2>=D2+F2 && F2>=1+H2 && 2>=J2 && K2>=1+J2 && J2>=1+M2 && M2+H2>=1+2*W1 ], cost: 32 1142: f1 -> f33 : C'=1+B, E'=1+D, G'=1+F, Q'=1+H, K'=1+J, N'=1+L, P'=1+O, R'=1+Q_1, T'=1+S, V'=1+U, X'=1+A, Z'=1+M, C1'=1+B1, E1'=1+D1, G1'=1+F1, Q1'=1+H1, K1'=1+J1, N1'=1+L1, P1'=1+O1, Q1_1'=1+Y, S1'=1+R1, T1'=1+W, V1'=1+A1, X1'=1+M1, A2'=1+Z1, C2'=1+B2, E2'=1+D2, G2'=1+F2, Q2'=1+H2, L2'=1+J2, N2'=1+M2, O2'=-1+W1, [ A>=1+B && B>=1+D && 2>=F+D && 2>=H+F && H>=1+J && 0>=1+L && M>=1+L && L>=1+O && O+J>=1+2*Q_1 && L>=1+S && 2>=U+S && 1+W>=2*A && 1+Y>=2*M && A1>=1+B1 && B1>=1+D1 && 2>=F1+D1 && 2>=H1+F1 && H1>=1+J1 && 1>=L1 && M1>=1+L1 && L1>=1+O1 && O1+J1>=1+2*Y && L1>=1+R1 && 2>=R1+W && U+U1>=2+2*A1 && Q_1+W1>=1+2*M1 && Y1>=1+Z1 && Z1>=1+B2 && 2>=D2+B2 && 2>=D2+F2 && F2>=1+H2 && 2>=J2 && K2>=1+J2 && J2>=1+M2 && 2*W1>=2+M2+H2 ], cost: 32 1144: f1 -> f33 : C'=1+B, E'=1+D, G'=1+F, Q'=1+H, K'=1+J, N'=1+L, P'=1+O, R'=1+Q_1, T'=1+S, V'=1+U, X'=1+A, Z'=1+M, C1'=1+B1, E1'=1+D1, G1'=1+F1, Q1'=1+H1, K1'=1+J1, N1'=1+L1, P1'=1+O1, Q1_1'=1+Y, S1'=1+R1, T1'=1+W, V1'=1+A1, X1'=-1+M1, A2'=1+Z1, C2'=1+B2, E2'=1+D2, G2'=1+F2, Q2'=1+H2, L2'=-1+J2, N2'=-1+M2, O2'=1+W1, [ A>=1+B && B>=1+D && 2>=F+D && 2>=H+F && H>=1+J && 0>=1+L && M>=1+L && L>=1+O && O+J>=1+2*Q_1 && L>=1+S && 2>=U+S && 1+W>=2*A && 1+Y>=2*M && A1>=1+B1 && B1>=1+D1 && 2>=F1+D1 && 2>=H1+F1 && H1>=1+J1 && 1>=L1 && M1>=1+L1 && L1>=1+O1 && O1+J1>=1+2*Y && L1>=1+R1 && 2>=R1+W && U+U1>=2+2*A1 && 2*M1>=2+Q_1+W1 && Y1>=1+Z1 && Z1>=1+B2 && 2>=D2+B2 && 2>=D2+F2 && F2>=1+H2 && J2>=4 && M2>=1+J2 && M2+H2>=1+2*W1 ], cost: 32 1148: f1 -> f33 : C'=1+B, E'=1+D, G'=1+F, Q'=1+H, K'=1+J, N'=1+L, P'=1+O, R'=1+Q_1, T'=1+S, V'=1+U, X'=1+A, Z'=1+M, C1'=1+B1, E1'=1+D1, G1'=1+F1, Q1'=-1+H1, K1'=1+J1, N1'=1+L1, P1'=1+O1, Q1_1'=1+Y, S1'=1+R1, T1'=1+W, V1'=1+A1, X1'=1+M1, A2'=1+Z1, C2'=1+B2, E2'=1+D2, G2'=-1+F2, Q2'=1+H2, L2'=1+J2, N2'=-1+M2, O2'=-1+W1, [ A>=1+B && B>=1+D && 2>=F+D && 2>=H+F && H>=1+J && 0>=1+L && M>=1+L && L>=1+O && O+J>=1+2*Q_1 && L>=1+S && 2>=U+S && 1+W>=2*A && 1+Y>=2*M && A1>=1+B1 && B1>=1+D1 && 2>=F1+D1 && H1+F1>=4 && H1>=1+J1 && 1>=L1 && M1>=1+L1 && L1>=1+O1 && O1+J1>=1+2*Y && L1>=1+R1 && 2>=R1+W && U+U1>=2+2*A1 && Q_1+W1>=1+2*M1 && Y1>=1+Z1 && Z1>=1+B2 && 2>=D2+B2 && D2+F2>=4 && F2>=1+H2 && 2>=J2 && K2>=1+J2 && M2>=1+J2 && 2*W1>=2+M2+H2 ], cost: 32 1153: f1 -> f33 : C'=1+B, E'=1+D, G'=1+F, Q'=1+H, K'=1+J, N'=1+L, P'=1+O, R'=1+Q_1, T'=1+S, V'=1+U, X'=1+A, Z'=-1+M, C1'=1+B1, E1'=1+D1, G1'=-1+F1, Q1'=-1+H1, K1'=1+J1, N1'=1+L1, P1'=1+O1, Q1_1'=1+Y, S1'=1+R1, T1'=1+W, V1'=1+A1, X1'=1+M1, A2'=1+Z1, C2'=1+B2, E2'=1+D2, G2'=-1+F2, Q2'=1+H2, L2'=1+J2, N2'=-1+M2, O2'=-1+W1, [ A>=1+B && B>=1+D && 2>=F+D && 2>=H+F && H>=1+J && 0>=1+L && M>=1+L && L>=1+O && O+J>=1+2*Q_1 && L>=1+S && 2>=U+S && 1+W>=2*A && 2*M>=4+Y && A1>=1+B1 && B1>=1+D1 && F1+D1>=4 && H1+F1>=4 && H1>=1+J1 && 1>=L1 && M1>=1+L1 && L1>=1+O1 && O1+J1>=1+2*Y && L1>=1+R1 && 2>=R1+W && U+U1>=2+2*A1 && Q_1+W1>=1+2*M1 && Y1>=1+Z1 && Z1>=1+B2 && 2>=D2+B2 && D2+F2>=4 && F2>=1+H2 && 2>=J2 && K2>=1+J2 && M2>=1+J2 && 2*W1>=2+M2+H2 ], cost: 32 1166: f33 -> f1 : A'=X, B'=C, D'=E, F'=G, H'=Q, J'=K, L'=N, M'=Z, O'=P, Q_1'=R, S'=T, U'=V, W'=T1, Y'=Q1_1, A1'=V1, B1'=C1, D1'=E1, F1'=G1, H1'=Q1, J1'=K1, L1'=N1, M1'=X1, O1'=P1, R1'=S1, U1'=1+U1, W1'=O2, Y1'=1+Y1, Z1'=A2, B2'=C2, D2'=E2, F2'=G2, H2'=Q2, J2'=L2, K2'=1+K2, M2'=N2, P2'=1+P2, Q2_1'=1+P2, R2'=1+U1, S2'=1+S2, T2'=1+Y1, U2'=1+U2, V2'=1+K2, W2'=1+W2, X2'=1+X2, Y2'=1+X2, Z2'=1+Z2, A3'=1+Z2, B3'=1+B3, C3'=1+B3, D3'=1+D3, E3'=1+D3, F3'=1+F3, G3'=1+F3, H3'=1+H3, Q3'=1+Q3, J3'=1+H3, K3'=1+K3, L3'=1+K3, M3'=1+U2, N3'=1+N3, O3'=1+N3, P3'=1+S2, Q3_1'=1+Q3_1, R3'=1+W2, S3'=1+S3, T3'=1+Q3, U3'=1+U3, V3'=1+V3, W3'=1+V3, X3'=1+X3, Y3'=1+X3, Z3'=1+Z3, A4'=1+Z3, B4'=1+B4, C4'=1+B4, D4'=1+D4, E4'=1+D4, F4'=1+F4, G4'=1+G4, H4'=1+F4, Q4'=1+Q4, J4'=1+Q4, K4'=1+S3, L4'=1+L4, M4'=1+L4, N4'=1+Q3_1, O4'=1+U3, P4'=1+G4, [ J2>=1+P2 && 2>=P2+U1 && S2+W>=2+2*Y1 && Y+U2>=1+2*K2 && W2>=1+X2 && X2>=1+Z2 && 2>=Z2+B3 && 2>=D3+B3 && D3>=1+F3 && 2>=H3 && Q3>=1+H3 && H3>=1+K3 && F3+K3>=1+2*U2 && H3>=1+N3 && 2>=S2+N3 && U1+Q3_1>=2+2*W2 && S3+W1>=1+2*Q3 && U3>=1+V3 && V3>=1+X3 && 2>=Z3+X3 && 2>=Z3+B4 && B4>=1+D4 && 2>=F4 && G4>=1+F4 && F4>=1+Q4 && Q4+D4>=1+2*S3 && F4>=1+L4 && 2>=L4+Q3_1 && S2>=2+2*U3 && 1+U2>=2*G4 ], cost: 28 1167: f33 -> f1 : A'=X, B'=C, D'=E, F'=G, H'=Q, J'=K, L'=N, M'=Z, O'=P, Q_1'=R, S'=T, U'=V, W'=T1, Y'=Q1_1, A1'=V1, B1'=C1, D1'=E1, F1'=G1, H1'=Q1, J1'=K1, L1'=N1, M1'=X1, O1'=P1, R1'=S1, U1'=1+U1, W1'=O2, Y1'=1+Y1, Z1'=A2, B2'=C2, D2'=E2, F2'=G2, H2'=Q2, J2'=L2, K2'=1+K2, M2'=N2, P2'=1+P2, Q2_1'=1+P2, R2'=1+U1, S2'=1+S2, T2'=1+Y1, U2'=1+U2, V2'=1+K2, W2'=1+W2, X2'=1+X2, Y2'=1+X2, Z2'=1+Z2, A3'=1+Z2, B3'=1+B3, C3'=1+B3, D3'=1+D3, E3'=1+D3, F3'=1+F3, G3'=1+F3, H3'=1+H3, Q3'=1+Q3, J3'=1+H3, K3'=1+K3, L3'=1+K3, M3'=1+U2, N3'=1+N3, O3'=1+N3, P3'=1+S2, Q3_1'=1+Q3_1, R3'=1+W2, S3'=1+S3, T3'=1+Q3, U3'=1+U3, V3'=1+V3, W3'=1+V3, X3'=1+X3, Y3'=1+X3, Z3'=1+Z3, A4'=1+Z3, B4'=1+B4, C4'=1+B4, D4'=1+D4, E4'=1+D4, F4'=1+F4, G4'=-1+G4, H4'=1+F4, Q4'=1+Q4, J4'=1+Q4, K4'=1+S3, L4'=1+L4, M4'=1+L4, N4'=1+Q3_1, O4'=1+U3, P4'=-1+G4, [ J2>=1+P2 && 2>=P2+U1 && S2+W>=2+2*Y1 && Y+U2>=1+2*K2 && W2>=1+X2 && X2>=1+Z2 && 2>=Z2+B3 && 2>=D3+B3 && D3>=1+F3 && 2>=H3 && Q3>=1+H3 && H3>=1+K3 && F3+K3>=1+2*U2 && H3>=1+N3 && 2>=S2+N3 && U1+Q3_1>=2+2*W2 && S3+W1>=1+2*Q3 && U3>=1+V3 && V3>=1+X3 && 2>=Z3+X3 && 2>=Z3+B4 && B4>=1+D4 && 2>=F4 && G4>=1+F4 && F4>=1+Q4 && Q4+D4>=1+2*S3 && F4>=1+L4 && 2>=L4+Q3_1 && S2>=2+2*U3 && 2*G4>=4+U2 ], cost: 28 1169: f33 -> f1 : A'=X, B'=C, D'=E, F'=G, H'=Q, J'=K, L'=N, M'=Z, O'=P, Q_1'=R, S'=T, U'=V, W'=T1, Y'=Q1_1, A1'=V1, B1'=C1, D1'=E1, F1'=G1, H1'=Q1, J1'=K1, L1'=N1, M1'=X1, O1'=P1, R1'=S1, U1'=1+U1, W1'=O2, Y1'=1+Y1, Z1'=A2, B2'=C2, D2'=E2, F2'=G2, H2'=Q2, J2'=L2, K2'=1+K2, M2'=N2, P2'=1+P2, Q2_1'=1+P2, R2'=1+U1, S2'=1+S2, T2'=1+Y1, U2'=1+U2, V2'=1+K2, W2'=1+W2, X2'=1+X2, Y2'=1+X2, Z2'=1+Z2, A3'=1+Z2, B3'=1+B3, C3'=1+B3, D3'=1+D3, E3'=1+D3, F3'=1+F3, G3'=1+F3, H3'=1+H3, Q3'=1+Q3, J3'=1+H3, K3'=1+K3, L3'=1+K3, M3'=1+U2, N3'=1+N3, O3'=1+N3, P3'=1+S2, Q3_1'=1+Q3_1, R3'=1+W2, S3'=-1+S3, T3'=1+Q3, U3'=-1+U3, V3'=1+V3, W3'=1+V3, X3'=1+X3, Y3'=1+X3, Z3'=1+Z3, A4'=1+Z3, B4'=1+B4, C4'=1+B4, D4'=1+D4, E4'=1+D4, F4'=1+F4, G4'=-1+G4, H4'=1+F4, Q4'=1+Q4, J4'=1+Q4, K4'=-1+S3, L4'=1+L4, M4'=1+L4, N4'=1+Q3_1, O4'=-1+U3, P4'=-1+G4, [ J2>=1+P2 && 2>=P2+U1 && S2+W>=2+2*Y1 && Y+U2>=1+2*K2 && W2>=1+X2 && X2>=1+Z2 && 2>=Z2+B3 && 2>=D3+B3 && D3>=1+F3 && 2>=H3 && Q3>=1+H3 && H3>=1+K3 && F3+K3>=1+2*U2 && H3>=1+N3 && 2>=S2+N3 && U1+Q3_1>=2+2*W2 && S3+W1>=1+2*Q3 && U3>=1+V3 && V3>=1+X3 && 2>=Z3+X3 && 2>=Z3+B4 && B4>=1+D4 && 2>=F4 && G4>=1+F4 && F4>=1+Q4 && 2*S3>=2+Q4+D4 && F4>=1+L4 && 2>=L4+Q3_1 && 2*U3>=1+S2 && 2*G4>=4+U2 ], cost: 28 1173: f33 -> f1 : A'=X, B'=C, D'=E, F'=G, H'=Q, J'=K, L'=N, M'=Z, O'=P, Q_1'=R, S'=T, U'=V, W'=T1, Y'=Q1_1, A1'=V1, B1'=C1, D1'=E1, F1'=G1, H1'=Q1, J1'=K1, L1'=N1, M1'=X1, O1'=P1, R1'=S1, U1'=1+U1, W1'=O2, Y1'=1+Y1, Z1'=A2, B2'=C2, D2'=E2, F2'=G2, H2'=Q2, J2'=L2, K2'=1+K2, M2'=N2, P2'=1+P2, Q2_1'=1+P2, R2'=1+U1, S2'=1+S2, T2'=1+Y1, U2'=1+U2, V2'=1+K2, W2'=1+W2, X2'=1+X2, Y2'=1+X2, Z2'=1+Z2, A3'=1+Z2, B3'=1+B3, C3'=1+B3, D3'=1+D3, E3'=1+D3, F3'=1+F3, G3'=1+F3, H3'=1+H3, Q3'=-1+Q3, J3'=1+H3, K3'=1+K3, L3'=1+K3, M3'=1+U2, N3'=1+N3, O3'=1+N3, P3'=1+S2, Q3_1'=-1+Q3_1, R3'=1+W2, S3'=1+S3, T3'=-1+Q3, U3'=-1+U3, V3'=1+V3, W3'=1+V3, X3'=1+X3, Y3'=1+X3, Z3'=1+Z3, A4'=1+Z3, B4'=1+B4, C4'=1+B4, D4'=1+D4, E4'=1+D4, F4'=1+F4, G4'=1+G4, H4'=1+F4, Q4'=1+Q4, J4'=1+Q4, K4'=1+S3, L4'=1+L4, M4'=1+L4, N4'=-1+Q3_1, O4'=-1+U3, P4'=1+G4, [ J2>=1+P2 && 2>=P2+U1 && S2+W>=2+2*Y1 && Y+U2>=1+2*K2 && W2>=1+X2 && X2>=1+Z2 && 2>=Z2+B3 && 2>=D3+B3 && D3>=1+F3 && 2>=H3 && Q3>=1+H3 && H3>=1+K3 && F3+K3>=1+2*U2 && H3>=1+N3 && 2>=S2+N3 && U1+Q3_1>=2+2*W2 && 2*Q3>=2+S3+W1 && U3>=1+V3 && V3>=1+X3 && 2>=Z3+X3 && 2>=Z3+B4 && B4>=1+D4 && 2>=F4 && G4>=1+F4 && F4>=1+Q4 && Q4+D4>=1+2*S3 && F4>=1+L4 && L4+Q3_1>=4 && 2*U3>=1+S2 && 1+U2>=2*G4 ], cost: 28 1178: f33 -> f1 : A'=X, B'=C, D'=E, F'=G, H'=Q, J'=K, L'=N, M'=Z, O'=P, Q_1'=R, S'=T, U'=V, W'=T1, Y'=Q1_1, A1'=V1, B1'=C1, D1'=E1, F1'=G1, H1'=Q1, J1'=K1, L1'=N1, M1'=X1, O1'=P1, R1'=S1, U1'=1+U1, W1'=O2, Y1'=1+Y1, Z1'=A2, B2'=C2, D2'=E2, F2'=G2, H2'=Q2, J2'=L2, K2'=1+K2, M2'=N2, P2'=1+P2, Q2_1'=1+P2, R2'=1+U1, S2'=1+S2, T2'=1+Y1, U2'=-1+U2, V2'=1+K2, W2'=-1+W2, X2'=1+X2, Y2'=1+X2, Z2'=1+Z2, A3'=1+Z2, B3'=1+B3, C3'=1+B3, D3'=1+D3, E3'=1+D3, F3'=1+F3, G3'=1+F3, H3'=1+H3, Q3'=-1+Q3, J3'=1+H3, K3'=1+K3, L3'=1+K3, M3'=-1+U2, N3'=1+N3, O3'=1+N3, P3'=1+S2, Q3_1'=-1+Q3_1, R3'=-1+W2, S3'=1+S3, T3'=-1+Q3, U3'=-1+U3, V3'=1+V3, W3'=1+V3, X3'=1+X3, Y3'=1+X3, Z3'=1+Z3, A4'=1+Z3, B4'=1+B4, C4'=1+B4, D4'=1+D4, E4'=1+D4, F4'=1+F4, G4'=1+G4, H4'=1+F4, Q4'=1+Q4, J4'=1+Q4, K4'=1+S3, L4'=1+L4, M4'=1+L4, N4'=-1+Q3_1, O4'=-1+U3, P4'=1+G4, [ J2>=1+P2 && 2>=P2+U1 && S2+W>=2+2*Y1 && Y+U2>=1+2*K2 && W2>=1+X2 && X2>=1+Z2 && 2>=Z2+B3 && 2>=D3+B3 && D3>=1+F3 && 2>=H3 && Q3>=1+H3 && H3>=1+K3 && 2*U2>=2+F3+K3 && H3>=1+N3 && 2>=S2+N3 && 2*W2>=1+U1+Q3_1 && 2*Q3>=2+S3+W1 && U3>=1+V3 && V3>=1+X3 && 2>=Z3+X3 && 2>=Z3+B4 && B4>=1+D4 && 2>=F4 && G4>=1+F4 && F4>=1+Q4 && Q4+D4>=1+2*S3 && F4>=1+L4 && L4+Q3_1>=4 && 2*U3>=1+S2 && 1+U2>=2*G4 ], cost: 28 Applied chaining over branches and pruning: Start location: f0 0: f0 -> f1 : [], cost: 1 1191: f1 -> f1 : A'=1+A, B'=1+B, C'=1+B, D'=1+D, E'=1+D, F'=1+F, G'=1+F, H'=1+H, Q'=1+H, J'=1+J, K'=1+J, L'=1+L, M'=1+M, N'=1+L, O'=1+O, P'=1+O, Q_1'=1+Q_1, R'=1+Q_1, S'=1+S, T'=1+S, U'=1+U, V'=1+U, W'=1+W, X'=1+A, Y'=1+Y, Z'=1+M, A1'=1+A1, B1'=1+B1, C1'=1+B1, D1'=1+D1, E1'=1+D1, F1'=1+F1, G1'=1+F1, H1'=1+H1, Q1'=1+H1, J1'=1+J1, K1'=1+J1, L1'=1+L1, M1'=1+M1, N1'=1+L1, O1'=1+O1, P1'=1+O1, Q1_1'=1+Y, R1'=1+R1, S1'=1+R1, T1'=1+W, U1'=1+U1, V1'=1+A1, W1'=1+W1, X1'=1+M1, Y1'=1+Y1, Z1'=1+Z1, A2'=1+Z1, B2'=1+B2, C2'=1+B2, D2'=1+D2, E2'=1+D2, F2'=1+F2, G2'=1+F2, H2'=1+H2, Q2'=1+H2, J2'=1+J2, K2'=1+K2, L2'=1+J2, M2'=1+M2, N2'=1+M2, O2'=1+W1, P2'=1+P2, Q2_1'=1+P2, R2'=1+U1, S2'=1+S2, T2'=1+Y1, U2'=1+U2, V2'=1+K2, W2'=1+W2, X2'=1+X2, Y2'=1+X2, Z2'=1+Z2, A3'=1+Z2, B3'=1+B3, C3'=1+B3, D3'=1+D3, E3'=1+D3, F3'=1+F3, G3'=1+F3, H3'=1+H3, Q3'=1+Q3, J3'=1+H3, K3'=1+K3, L3'=1+K3, M3'=1+U2, N3'=1+N3, O3'=1+N3, P3'=1+S2, Q3_1'=1+Q3_1, R3'=1+W2, S3'=1+S3, T3'=1+Q3, U3'=1+U3, V3'=1+V3, W3'=1+V3, X3'=1+X3, Y3'=1+X3, Z3'=1+Z3, A4'=1+Z3, B4'=1+B4, C4'=1+B4, D4'=1+D4, E4'=1+D4, F4'=1+F4, G4'=1+G4, H4'=1+F4, Q4'=1+Q4, J4'=1+Q4, K4'=1+S3, L4'=1+L4, M4'=1+L4, N4'=1+Q3_1, O4'=1+U3, P4'=1+G4, [ A>=1+B && B>=1+D && 2>=F+D && 2>=H+F && H>=1+J && 0>=1+L && M>=1+L && L>=1+O && O+J>=1+2*Q_1 && L>=1+S && 2>=U+S && 1+W>=2*A && 1+Y>=2*M && A1>=1+B1 && B1>=1+D1 && 2>=F1+D1 && 2>=H1+F1 && H1>=1+J1 && 1>=L1 && M1>=1+L1 && L1>=1+O1 && O1+J1>=1+2*Y && L1>=1+R1 && 2>=R1+W && U+U1>=2+2*A1 && Q_1+W1>=1+2*M1 && Y1>=1+Z1 && Z1>=1+B2 && 2>=D2+B2 && 2>=D2+F2 && F2>=1+H2 && 2>=J2 && K2>=1+J2 && J2>=1+M2 && M2+H2>=1+2*W1 && J2>=1+P2 && 2>=P2+U1 && S2+W>=2+2*Y1 && Y+U2>=1+2*K2 && W2>=1+X2 && X2>=1+Z2 && 2>=Z2+B3 && 2>=D3+B3 && D3>=1+F3 && 2>=H3 && Q3>=1+H3 && H3>=1+K3 && F3+K3>=1+2*U2 && H3>=1+N3 && 2>=S2+N3 && U1+Q3_1>=2+2*W2 && S3+W1>=1+2*Q3 && U3>=1+V3 && V3>=1+X3 && 2>=Z3+X3 && 2>=Z3+B4 && B4>=1+D4 && 2>=F4 && G4>=1+F4 && F4>=1+Q4 && Q4+D4>=1+2*S3 && F4>=1+L4 && 2>=L4+Q3_1 && S2>=2+2*U3 && 1+U2>=2*G4 ], cost: 60 1192: f1 -> f1 : A'=1+A, B'=1+B, C'=1+B, D'=1+D, E'=1+D, F'=1+F, G'=1+F, H'=1+H, Q'=1+H, J'=1+J, K'=1+J, L'=1+L, M'=1+M, N'=1+L, O'=1+O, P'=1+O, Q_1'=1+Q_1, R'=1+Q_1, S'=1+S, T'=1+S, U'=1+U, V'=1+U, W'=1+W, X'=1+A, Y'=1+Y, Z'=1+M, A1'=1+A1, B1'=1+B1, C1'=1+B1, D1'=1+D1, E1'=1+D1, F1'=1+F1, G1'=1+F1, H1'=1+H1, Q1'=1+H1, J1'=1+J1, K1'=1+J1, L1'=1+L1, M1'=1+M1, N1'=1+L1, O1'=1+O1, P1'=1+O1, Q1_1'=1+Y, R1'=1+R1, S1'=1+R1, T1'=1+W, U1'=1+U1, V1'=1+A1, W1'=1+W1, X1'=1+M1, Y1'=1+Y1, Z1'=1+Z1, A2'=1+Z1, B2'=1+B2, C2'=1+B2, D2'=1+D2, E2'=1+D2, F2'=1+F2, G2'=1+F2, H2'=1+H2, Q2'=1+H2, J2'=1+J2, K2'=1+K2, L2'=1+J2, M2'=1+M2, N2'=1+M2, O2'=1+W1, P2'=1+P2, Q2_1'=1+P2, R2'=1+U1, S2'=1+S2, T2'=1+Y1, U2'=1+U2, V2'=1+K2, W2'=1+W2, X2'=1+X2, Y2'=1+X2, Z2'=1+Z2, A3'=1+Z2, B3'=1+B3, C3'=1+B3, D3'=1+D3, E3'=1+D3, F3'=1+F3, G3'=1+F3, H3'=1+H3, Q3'=1+Q3, J3'=1+H3, K3'=1+K3, L3'=1+K3, M3'=1+U2, N3'=1+N3, O3'=1+N3, P3'=1+S2, Q3_1'=1+Q3_1, R3'=1+W2, S3'=1+S3, T3'=1+Q3, U3'=1+U3, V3'=1+V3, W3'=1+V3, X3'=1+X3, Y3'=1+X3, Z3'=1+Z3, A4'=1+Z3, B4'=1+B4, C4'=1+B4, D4'=1+D4, E4'=1+D4, F4'=1+F4, G4'=-1+G4, H4'=1+F4, Q4'=1+Q4, J4'=1+Q4, K4'=1+S3, L4'=1+L4, M4'=1+L4, N4'=1+Q3_1, O4'=1+U3, P4'=-1+G4, [ A>=1+B && B>=1+D && 2>=F+D && 2>=H+F && H>=1+J && 0>=1+L && M>=1+L && L>=1+O && O+J>=1+2*Q_1 && L>=1+S && 2>=U+S && 1+W>=2*A && 1+Y>=2*M && A1>=1+B1 && B1>=1+D1 && 2>=F1+D1 && 2>=H1+F1 && H1>=1+J1 && 1>=L1 && M1>=1+L1 && L1>=1+O1 && O1+J1>=1+2*Y && L1>=1+R1 && 2>=R1+W && U+U1>=2+2*A1 && Q_1+W1>=1+2*M1 && Y1>=1+Z1 && Z1>=1+B2 && 2>=D2+B2 && 2>=D2+F2 && F2>=1+H2 && 2>=J2 && K2>=1+J2 && J2>=1+M2 && M2+H2>=1+2*W1 && J2>=1+P2 && 2>=P2+U1 && S2+W>=2+2*Y1 && Y+U2>=1+2*K2 && W2>=1+X2 && X2>=1+Z2 && 2>=Z2+B3 && 2>=D3+B3 && D3>=1+F3 && 2>=H3 && Q3>=1+H3 && H3>=1+K3 && F3+K3>=1+2*U2 && H3>=1+N3 && 2>=S2+N3 && U1+Q3_1>=2+2*W2 && S3+W1>=1+2*Q3 && U3>=1+V3 && V3>=1+X3 && 2>=Z3+X3 && 2>=Z3+B4 && B4>=1+D4 && 2>=F4 && G4>=1+F4 && F4>=1+Q4 && Q4+D4>=1+2*S3 && F4>=1+L4 && 2>=L4+Q3_1 && S2>=2+2*U3 && 2*G4>=4+U2 ], cost: 60 1194: f1 -> f1 : A'=1+A, B'=1+B, C'=1+B, D'=1+D, E'=1+D, F'=1+F, G'=1+F, H'=1+H, Q'=1+H, J'=1+J, K'=1+J, L'=1+L, M'=1+M, N'=1+L, O'=1+O, P'=1+O, Q_1'=1+Q_1, R'=1+Q_1, S'=1+S, T'=1+S, U'=1+U, V'=1+U, W'=1+W, X'=1+A, Y'=1+Y, Z'=1+M, A1'=1+A1, B1'=1+B1, C1'=1+B1, D1'=1+D1, E1'=1+D1, F1'=1+F1, G1'=1+F1, H1'=1+H1, Q1'=1+H1, J1'=1+J1, K1'=1+J1, L1'=1+L1, M1'=1+M1, N1'=1+L1, O1'=1+O1, P1'=1+O1, Q1_1'=1+Y, R1'=1+R1, S1'=1+R1, T1'=1+W, U1'=1+U1, V1'=1+A1, W1'=1+W1, X1'=1+M1, Y1'=1+Y1, Z1'=1+Z1, A2'=1+Z1, B2'=1+B2, C2'=1+B2, D2'=1+D2, E2'=1+D2, F2'=1+F2, G2'=1+F2, H2'=1+H2, Q2'=1+H2, J2'=1+J2, K2'=1+K2, L2'=1+J2, M2'=1+M2, N2'=1+M2, O2'=1+W1, P2'=1+P2, Q2_1'=1+P2, R2'=1+U1, S2'=1+S2, T2'=1+Y1, U2'=1+U2, V2'=1+K2, W2'=1+W2, X2'=1+X2, Y2'=1+X2, Z2'=1+Z2, A3'=1+Z2, B3'=1+B3, C3'=1+B3, D3'=1+D3, E3'=1+D3, F3'=1+F3, G3'=1+F3, H3'=1+H3, Q3'=-1+Q3, J3'=1+H3, K3'=1+K3, L3'=1+K3, M3'=1+U2, N3'=1+N3, O3'=1+N3, P3'=1+S2, Q3_1'=-1+Q3_1, R3'=1+W2, S3'=1+S3, T3'=-1+Q3, U3'=-1+U3, V3'=1+V3, W3'=1+V3, X3'=1+X3, Y3'=1+X3, Z3'=1+Z3, A4'=1+Z3, B4'=1+B4, C4'=1+B4, D4'=1+D4, E4'=1+D4, F4'=1+F4, G4'=1+G4, H4'=1+F4, Q4'=1+Q4, J4'=1+Q4, K4'=1+S3, L4'=1+L4, M4'=1+L4, N4'=-1+Q3_1, O4'=-1+U3, P4'=1+G4, [ A>=1+B && B>=1+D && 2>=F+D && 2>=H+F && H>=1+J && 0>=1+L && M>=1+L && L>=1+O && O+J>=1+2*Q_1 && L>=1+S && 2>=U+S && 1+W>=2*A && 1+Y>=2*M && A1>=1+B1 && B1>=1+D1 && 2>=F1+D1 && 2>=H1+F1 && H1>=1+J1 && 1>=L1 && M1>=1+L1 && L1>=1+O1 && O1+J1>=1+2*Y && L1>=1+R1 && 2>=R1+W && U+U1>=2+2*A1 && Q_1+W1>=1+2*M1 && Y1>=1+Z1 && Z1>=1+B2 && 2>=D2+B2 && 2>=D2+F2 && F2>=1+H2 && 2>=J2 && K2>=1+J2 && J2>=1+M2 && M2+H2>=1+2*W1 && J2>=1+P2 && 2>=P2+U1 && S2+W>=2+2*Y1 && Y+U2>=1+2*K2 && W2>=1+X2 && X2>=1+Z2 && 2>=Z2+B3 && 2>=D3+B3 && D3>=1+F3 && 2>=H3 && Q3>=1+H3 && H3>=1+K3 && F3+K3>=1+2*U2 && H3>=1+N3 && 2>=S2+N3 && U1+Q3_1>=2+2*W2 && 2*Q3>=2+S3+W1 && U3>=1+V3 && V3>=1+X3 && 2>=Z3+X3 && 2>=Z3+B4 && B4>=1+D4 && 2>=F4 && G4>=1+F4 && F4>=1+Q4 && Q4+D4>=1+2*S3 && F4>=1+L4 && L4+Q3_1>=4 && 2*U3>=1+S2 && 1+U2>=2*G4 ], cost: 60 1198: f1 -> f1 : A'=1+A, B'=1+B, C'=1+B, D'=1+D, E'=1+D, F'=1+F, G'=1+F, H'=1+H, Q'=1+H, J'=1+J, K'=1+J, L'=1+L, M'=1+M, N'=1+L, O'=1+O, P'=1+O, Q_1'=1+Q_1, R'=1+Q_1, S'=1+S, T'=1+S, U'=1+U, V'=1+U, W'=1+W, X'=1+A, Y'=1+Y, Z'=1+M, A1'=1+A1, B1'=1+B1, C1'=1+B1, D1'=1+D1, E1'=1+D1, F1'=1+F1, G1'=1+F1, H1'=1+H1, Q1'=1+H1, J1'=1+J1, K1'=1+J1, L1'=1+L1, M1'=1+M1, N1'=1+L1, O1'=1+O1, P1'=1+O1, Q1_1'=1+Y, R1'=1+R1, S1'=1+R1, T1'=1+W, U1'=1+U1, V1'=1+A1, W1'=-1+W1, X1'=1+M1, Y1'=1+Y1, Z1'=1+Z1, A2'=1+Z1, B2'=1+B2, C2'=1+B2, D2'=1+D2, E2'=1+D2, F2'=1+F2, G2'=1+F2, H2'=1+H2, Q2'=1+H2, J2'=1+J2, K2'=1+K2, L2'=1+J2, M2'=1+M2, N2'=1+M2, O2'=-1+W1, P2'=1+P2, Q2_1'=1+P2, R2'=1+U1, S2'=1+S2, T2'=1+Y1, U2'=1+U2, V2'=1+K2, W2'=1+W2, X2'=1+X2, Y2'=1+X2, Z2'=1+Z2, A3'=1+Z2, B3'=1+B3, C3'=1+B3, D3'=1+D3, E3'=1+D3, F3'=1+F3, G3'=1+F3, H3'=1+H3, Q3'=1+Q3, J3'=1+H3, K3'=1+K3, L3'=1+K3, M3'=1+U2, N3'=1+N3, O3'=1+N3, P3'=1+S2, Q3_1'=1+Q3_1, R3'=1+W2, S3'=-1+S3, T3'=1+Q3, U3'=-1+U3, V3'=1+V3, W3'=1+V3, X3'=1+X3, Y3'=1+X3, Z3'=1+Z3, A4'=1+Z3, B4'=1+B4, C4'=1+B4, D4'=1+D4, E4'=1+D4, F4'=1+F4, G4'=-1+G4, H4'=1+F4, Q4'=1+Q4, J4'=1+Q4, K4'=-1+S3, L4'=1+L4, M4'=1+L4, N4'=1+Q3_1, O4'=-1+U3, P4'=-1+G4, [ A>=1+B && B>=1+D && 2>=F+D && 2>=H+F && H>=1+J && 0>=1+L && M>=1+L && L>=1+O && O+J>=1+2*Q_1 && L>=1+S && 2>=U+S && 1+W>=2*A && 1+Y>=2*M && A1>=1+B1 && B1>=1+D1 && 2>=F1+D1 && 2>=H1+F1 && H1>=1+J1 && 1>=L1 && M1>=1+L1 && L1>=1+O1 && O1+J1>=1+2*Y && L1>=1+R1 && 2>=R1+W && U+U1>=2+2*A1 && Q_1+W1>=1+2*M1 && Y1>=1+Z1 && Z1>=1+B2 && 2>=D2+B2 && 2>=D2+F2 && F2>=1+H2 && 2>=J2 && K2>=1+J2 && J2>=1+M2 && 2*W1>=2+M2+H2 && J2>=1+P2 && 2>=P2+U1 && S2+W>=2+2*Y1 && Y+U2>=1+2*K2 && W2>=1+X2 && X2>=1+Z2 && 2>=Z2+B3 && 2>=D3+B3 && D3>=1+F3 && 2>=H3 && Q3>=1+H3 && H3>=1+K3 && F3+K3>=1+2*U2 && H3>=1+N3 && 2>=S2+N3 && U1+Q3_1>=2+2*W2 && S3+W1>=1+2*Q3 && U3>=1+V3 && V3>=1+X3 && 2>=Z3+X3 && 2>=Z3+B4 && B4>=1+D4 && 2>=F4 && G4>=1+F4 && F4>=1+Q4 && 2*S3>=2+Q4+D4 && F4>=1+L4 && 2>=L4+Q3_1 && 2*U3>=1+S2 && 2*G4>=4+U2 ], cost: 60 1203: f1 -> f1 : A'=1+A, B'=1+B, C'=1+B, D'=1+D, E'=1+D, F'=1+F, G'=1+F, H'=1+H, Q'=1+H, J'=1+J, K'=1+J, L'=1+L, M'=1+M, N'=1+L, O'=1+O, P'=1+O, Q_1'=1+Q_1, R'=1+Q_1, S'=1+S, T'=1+S, U'=1+U, V'=1+U, W'=1+W, X'=1+A, Y'=1+Y, Z'=1+M, A1'=1+A1, B1'=1+B1, C1'=1+B1, D1'=1+D1, E1'=1+D1, F1'=1+F1, G1'=1+F1, H1'=1+H1, Q1'=1+H1, J1'=1+J1, K1'=1+J1, L1'=1+L1, M1'=-1+M1, N1'=1+L1, O1'=1+O1, P1'=1+O1, Q1_1'=1+Y, R1'=1+R1, S1'=1+R1, T1'=1+W, U1'=1+U1, V1'=1+A1, W1'=1+W1, X1'=-1+M1, Y1'=1+Y1, Z1'=1+Z1, A2'=1+Z1, B2'=1+B2, C2'=1+B2, D2'=1+D2, E2'=1+D2, F2'=1+F2, G2'=1+F2, H2'=1+H2, Q2'=1+H2, J2'=-1+J2, K2'=1+K2, L2'=-1+J2, M2'=-1+M2, N2'=-1+M2, O2'=1+W1, P2'=1+P2, Q2_1'=1+P2, R2'=1+U1, S2'=1+S2, T2'=1+Y1, U2'=1+U2, V2'=1+K2, W2'=1+W2, X2'=1+X2, Y2'=1+X2, Z2'=1+Z2, A3'=1+Z2, B3'=1+B3, C3'=1+B3, D3'=1+D3, E3'=1+D3, F3'=1+F3, G3'=1+F3, H3'=1+H3, Q3'=1+Q3, J3'=1+H3, K3'=1+K3, L3'=1+K3, M3'=1+U2, N3'=1+N3, O3'=1+N3, P3'=1+S2, Q3_1'=1+Q3_1, R3'=1+W2, S3'=-1+S3, T3'=1+Q3, U3'=-1+U3, V3'=1+V3, W3'=1+V3, X3'=1+X3, Y3'=1+X3, Z3'=1+Z3, A4'=1+Z3, B4'=1+B4, C4'=1+B4, D4'=1+D4, E4'=1+D4, F4'=1+F4, G4'=-1+G4, H4'=1+F4, Q4'=1+Q4, J4'=1+Q4, K4'=-1+S3, L4'=1+L4, M4'=1+L4, N4'=1+Q3_1, O4'=-1+U3, P4'=-1+G4, [ A>=1+B && B>=1+D && 2>=F+D && 2>=H+F && H>=1+J && 0>=1+L && M>=1+L && L>=1+O && O+J>=1+2*Q_1 && L>=1+S && 2>=U+S && 1+W>=2*A && 1+Y>=2*M && A1>=1+B1 && B1>=1+D1 && 2>=F1+D1 && 2>=H1+F1 && H1>=1+J1 && 1>=L1 && M1>=1+L1 && L1>=1+O1 && O1+J1>=1+2*Y && L1>=1+R1 && 2>=R1+W && U+U1>=2+2*A1 && 2*M1>=2+Q_1+W1 && Y1>=1+Z1 && Z1>=1+B2 && 2>=D2+B2 && 2>=D2+F2 && F2>=1+H2 && J2>=4 && M2>=1+J2 && M2+H2>=1+2*W1 && J2>=1+P2 && 2>=P2+U1 && S2+W>=2+2*Y1 && Y+U2>=1+2*K2 && W2>=1+X2 && X2>=1+Z2 && 2>=Z2+B3 && 2>=D3+B3 && D3>=1+F3 && 2>=H3 && Q3>=1+H3 && H3>=1+K3 && F3+K3>=1+2*U2 && H3>=1+N3 && 2>=S2+N3 && U1+Q3_1>=2+2*W2 && S3+W1>=1+2*Q3 && U3>=1+V3 && V3>=1+X3 && 2>=Z3+X3 && 2>=Z3+B4 && B4>=1+D4 && 2>=F4 && G4>=1+F4 && F4>=1+Q4 && 2*S3>=2+Q4+D4 && F4>=1+L4 && 2>=L4+Q3_1 && 2*U3>=1+S2 && 2*G4>=4+U2 ], cost: 60 Eliminating 5 self-loops for location f1 Removing the self-loops: 1191 1192 1194 1198 1203. Adding an epsilon transition (to model nonexecution of the loops): 1221. Removed all Self-loops using metering functions (where possible): Start location: f0 0: f0 -> f1 : [], cost: 1 1216: f1 -> [61] : A'=1+A, B'=1+B, C'=1+B, D'=1+D, E'=1+D, F'=1+F, G'=1+F, H'=1+H, Q'=1+H, J'=1+J, K'=1+J, L'=1+L, M'=1+M, N'=1+L, O'=1+O, P'=1+O, Q_1'=1+Q_1, R'=1+Q_1, S'=1+S, T'=1+S, U'=1+U, V'=1+U, W'=1+W, X'=1+A, Y'=1+Y, Z'=1+M, A1'=1+A1, B1'=1+B1, C1'=1+B1, D1'=1+D1, E1'=1+D1, F1'=1+F1, G1'=1+F1, H1'=1+H1, Q1'=1+H1, J1'=1+J1, K1'=1+J1, L1'=1+L1, M1'=1+M1, N1'=1+L1, O1'=1+O1, P1'=1+O1, Q1_1'=1+Y, R1'=1+R1, S1'=1+R1, T1'=1+W, U1'=1+U1, V1'=1+A1, W1'=1+W1, X1'=1+M1, Y1'=1+Y1, Z1'=1+Z1, A2'=1+Z1, B2'=1+B2, C2'=1+B2, D2'=1+D2, E2'=1+D2, F2'=1+F2, G2'=1+F2, H2'=1+H2, Q2'=1+H2, J2'=1+J2, K2'=1+K2, L2'=1+J2, M2'=1+M2, N2'=1+M2, O2'=1+W1, P2'=1+P2, Q2_1'=1+P2, R2'=1+U1, S2'=1+S2, T2'=1+Y1, U2'=1+U2, V2'=1+K2, W2'=1+W2, X2'=1+X2, Y2'=1+X2, Z2'=1+Z2, A3'=1+Z2, B3'=1+B3, C3'=1+B3, D3'=1+D3, E3'=1+D3, F3'=1+F3, G3'=1+F3, H3'=1+H3, Q3'=1+Q3, J3'=1+H3, K3'=1+K3, L3'=1+K3, M3'=1+U2, N3'=1+N3, O3'=1+N3, P3'=1+S2, Q3_1'=1+Q3_1, R3'=1+W2, S3'=1+S3, T3'=1+Q3, U3'=1+U3, V3'=1+V3, W3'=1+V3, X3'=1+X3, Y3'=1+X3, Z3'=1+Z3, A4'=1+Z3, B4'=1+B4, C4'=1+B4, D4'=1+D4, E4'=1+D4, F4'=1+F4, G4'=1+G4, H4'=1+F4, Q4'=1+Q4, J4'=1+Q4, K4'=1+S3, L4'=1+L4, M4'=1+L4, N4'=1+Q3_1, O4'=1+U3, P4'=1+G4, [ A>=1+B && B>=1+D && 2>=F+D && 2>=H+F && H>=1+J && 0>=1+L && M>=1+L && L>=1+O && O+J>=1+2*Q_1 && L>=1+S && 2>=U+S && 1+W>=2*A && 1+Y>=2*M && A1>=1+B1 && B1>=1+D1 && 2>=F1+D1 && 2>=H1+F1 && H1>=1+J1 && 1>=L1 && M1>=1+L1 && L1>=1+O1 && O1+J1>=1+2*Y && L1>=1+R1 && 2>=R1+W && U+U1>=2+2*A1 && Q_1+W1>=1+2*M1 && Y1>=1+Z1 && Z1>=1+B2 && 2>=D2+B2 && 2>=D2+F2 && F2>=1+H2 && 2>=J2 && K2>=1+J2 && J2>=1+M2 && M2+H2>=1+2*W1 && J2>=1+P2 && 2>=P2+U1 && S2+W>=2+2*Y1 && Y+U2>=1+2*K2 && W2>=1+X2 && X2>=1+Z2 && 2>=Z2+B3 && 2>=D3+B3 && D3>=1+F3 && 2>=H3 && Q3>=1+H3 && H3>=1+K3 && F3+K3>=1+2*U2 && H3>=1+N3 && 2>=S2+N3 && U1+Q3_1>=2+2*W2 && S3+W1>=1+2*Q3 && U3>=1+V3 && V3>=1+X3 && 2>=Z3+X3 && 2>=Z3+B4 && B4>=1+D4 && 2>=F4 && G4>=1+F4 && F4>=1+Q4 && Q4+D4>=1+2*S3 && F4>=1+L4 && 2>=L4+Q3_1 && S2>=2+2*U3 && 1+U2>=2*G4 ], cost: 60 1217: f1 -> [61] : A'=1+A, B'=1+B, C'=1+B, D'=1+D, E'=1+D, F'=1+F, G'=1+F, H'=1+H, Q'=1+H, J'=1+J, K'=1+J, L'=1+L, M'=1+M, N'=1+L, O'=1+O, P'=1+O, Q_1'=1+Q_1, R'=1+Q_1, S'=1+S, T'=1+S, U'=1+U, V'=1+U, W'=1+W, X'=1+A, Y'=1+Y, Z'=1+M, A1'=1+A1, B1'=1+B1, C1'=1+B1, D1'=1+D1, E1'=1+D1, F1'=1+F1, G1'=1+F1, H1'=1+H1, Q1'=1+H1, J1'=1+J1, K1'=1+J1, L1'=1+L1, M1'=1+M1, N1'=1+L1, O1'=1+O1, P1'=1+O1, Q1_1'=1+Y, R1'=1+R1, S1'=1+R1, T1'=1+W, U1'=1+U1, V1'=1+A1, W1'=1+W1, X1'=1+M1, Y1'=1+Y1, Z1'=1+Z1, A2'=1+Z1, B2'=1+B2, C2'=1+B2, D2'=1+D2, E2'=1+D2, F2'=1+F2, G2'=1+F2, H2'=1+H2, Q2'=1+H2, J2'=1+J2, K2'=1+K2, L2'=1+J2, M2'=1+M2, N2'=1+M2, O2'=1+W1, P2'=1+P2, Q2_1'=1+P2, R2'=1+U1, S2'=1+S2, T2'=1+Y1, U2'=1+U2, V2'=1+K2, W2'=1+W2, X2'=1+X2, Y2'=1+X2, Z2'=1+Z2, A3'=1+Z2, B3'=1+B3, C3'=1+B3, D3'=1+D3, E3'=1+D3, F3'=1+F3, G3'=1+F3, H3'=1+H3, Q3'=1+Q3, J3'=1+H3, K3'=1+K3, L3'=1+K3, M3'=1+U2, N3'=1+N3, O3'=1+N3, P3'=1+S2, Q3_1'=1+Q3_1, R3'=1+W2, S3'=1+S3, T3'=1+Q3, U3'=1+U3, V3'=1+V3, W3'=1+V3, X3'=1+X3, Y3'=1+X3, Z3'=1+Z3, A4'=1+Z3, B4'=1+B4, C4'=1+B4, D4'=1+D4, E4'=1+D4, F4'=1+F4, G4'=-1+G4, H4'=1+F4, Q4'=1+Q4, J4'=1+Q4, K4'=1+S3, L4'=1+L4, M4'=1+L4, N4'=1+Q3_1, O4'=1+U3, P4'=-1+G4, [ A>=1+B && B>=1+D && 2>=F+D && 2>=H+F && H>=1+J && 0>=1+L && M>=1+L && L>=1+O && O+J>=1+2*Q_1 && L>=1+S && 2>=U+S && 1+W>=2*A && 1+Y>=2*M && A1>=1+B1 && B1>=1+D1 && 2>=F1+D1 && 2>=H1+F1 && H1>=1+J1 && 1>=L1 && M1>=1+L1 && L1>=1+O1 && O1+J1>=1+2*Y && L1>=1+R1 && 2>=R1+W && U+U1>=2+2*A1 && Q_1+W1>=1+2*M1 && Y1>=1+Z1 && Z1>=1+B2 && 2>=D2+B2 && 2>=D2+F2 && F2>=1+H2 && 2>=J2 && K2>=1+J2 && J2>=1+M2 && M2+H2>=1+2*W1 && J2>=1+P2 && 2>=P2+U1 && S2+W>=2+2*Y1 && Y+U2>=1+2*K2 && W2>=1+X2 && X2>=1+Z2 && 2>=Z2+B3 && 2>=D3+B3 && D3>=1+F3 && 2>=H3 && Q3>=1+H3 && H3>=1+K3 && F3+K3>=1+2*U2 && H3>=1+N3 && 2>=S2+N3 && U1+Q3_1>=2+2*W2 && S3+W1>=1+2*Q3 && U3>=1+V3 && V3>=1+X3 && 2>=Z3+X3 && 2>=Z3+B4 && B4>=1+D4 && 2>=F4 && G4>=1+F4 && F4>=1+Q4 && Q4+D4>=1+2*S3 && F4>=1+L4 && 2>=L4+Q3_1 && S2>=2+2*U3 && 2*G4>=4+U2 ], cost: 60 1218: f1 -> [61] : A'=1+A, B'=1+B, C'=1+B, D'=1+D, E'=1+D, F'=1+F, G'=1+F, H'=1+H, Q'=1+H, J'=1+J, K'=1+J, L'=1+L, M'=1+M, N'=1+L, O'=1+O, P'=1+O, Q_1'=1+Q_1, R'=1+Q_1, S'=1+S, T'=1+S, U'=1+U, V'=1+U, W'=1+W, X'=1+A, Y'=1+Y, Z'=1+M, A1'=1+A1, B1'=1+B1, C1'=1+B1, D1'=1+D1, E1'=1+D1, F1'=1+F1, G1'=1+F1, H1'=1+H1, Q1'=1+H1, J1'=1+J1, K1'=1+J1, L1'=1+L1, M1'=1+M1, N1'=1+L1, O1'=1+O1, P1'=1+O1, Q1_1'=1+Y, R1'=1+R1, S1'=1+R1, T1'=1+W, U1'=1+U1, V1'=1+A1, W1'=1+W1, X1'=1+M1, Y1'=1+Y1, Z1'=1+Z1, A2'=1+Z1, B2'=1+B2, C2'=1+B2, D2'=1+D2, E2'=1+D2, F2'=1+F2, G2'=1+F2, H2'=1+H2, Q2'=1+H2, J2'=1+J2, K2'=1+K2, L2'=1+J2, M2'=1+M2, N2'=1+M2, O2'=1+W1, P2'=1+P2, Q2_1'=1+P2, R2'=1+U1, S2'=1+S2, T2'=1+Y1, U2'=1+U2, V2'=1+K2, W2'=1+W2, X2'=1+X2, Y2'=1+X2, Z2'=1+Z2, A3'=1+Z2, B3'=1+B3, C3'=1+B3, D3'=1+D3, E3'=1+D3, F3'=1+F3, G3'=1+F3, H3'=1+H3, Q3'=-1+Q3, J3'=1+H3, K3'=1+K3, L3'=1+K3, M3'=1+U2, N3'=1+N3, O3'=1+N3, P3'=1+S2, Q3_1'=-1+Q3_1, R3'=1+W2, S3'=1+S3, T3'=-1+Q3, U3'=-1+U3, V3'=1+V3, W3'=1+V3, X3'=1+X3, Y3'=1+X3, Z3'=1+Z3, A4'=1+Z3, B4'=1+B4, C4'=1+B4, D4'=1+D4, E4'=1+D4, F4'=1+F4, G4'=1+G4, H4'=1+F4, Q4'=1+Q4, J4'=1+Q4, K4'=1+S3, L4'=1+L4, M4'=1+L4, N4'=-1+Q3_1, O4'=-1+U3, P4'=1+G4, [ A>=1+B && B>=1+D && 2>=F+D && 2>=H+F && H>=1+J && 0>=1+L && M>=1+L && L>=1+O && O+J>=1+2*Q_1 && L>=1+S && 2>=U+S && 1+W>=2*A && 1+Y>=2*M && A1>=1+B1 && B1>=1+D1 && 2>=F1+D1 && 2>=H1+F1 && H1>=1+J1 && 1>=L1 && M1>=1+L1 && L1>=1+O1 && O1+J1>=1+2*Y && L1>=1+R1 && 2>=R1+W && U+U1>=2+2*A1 && Q_1+W1>=1+2*M1 && Y1>=1+Z1 && Z1>=1+B2 && 2>=D2+B2 && 2>=D2+F2 && F2>=1+H2 && 2>=J2 && K2>=1+J2 && J2>=1+M2 && M2+H2>=1+2*W1 && J2>=1+P2 && 2>=P2+U1 && S2+W>=2+2*Y1 && Y+U2>=1+2*K2 && W2>=1+X2 && X2>=1+Z2 && 2>=Z2+B3 && 2>=D3+B3 && D3>=1+F3 && 2>=H3 && Q3>=1+H3 && H3>=1+K3 && F3+K3>=1+2*U2 && H3>=1+N3 && 2>=S2+N3 && U1+Q3_1>=2+2*W2 && 2*Q3>=2+S3+W1 && U3>=1+V3 && V3>=1+X3 && 2>=Z3+X3 && 2>=Z3+B4 && B4>=1+D4 && 2>=F4 && G4>=1+F4 && F4>=1+Q4 && Q4+D4>=1+2*S3 && F4>=1+L4 && L4+Q3_1>=4 && 2*U3>=1+S2 && 1+U2>=2*G4 ], cost: 60 1219: f1 -> [61] : A'=1+A, B'=1+B, C'=1+B, D'=1+D, E'=1+D, F'=1+F, G'=1+F, H'=1+H, Q'=1+H, J'=1+J, K'=1+J, L'=1+L, M'=1+M, N'=1+L, O'=1+O, P'=1+O, Q_1'=1+Q_1, R'=1+Q_1, S'=1+S, T'=1+S, U'=1+U, V'=1+U, W'=1+W, X'=1+A, Y'=1+Y, Z'=1+M, A1'=1+A1, B1'=1+B1, C1'=1+B1, D1'=1+D1, E1'=1+D1, F1'=1+F1, G1'=1+F1, H1'=1+H1, Q1'=1+H1, J1'=1+J1, K1'=1+J1, L1'=1+L1, M1'=1+M1, N1'=1+L1, O1'=1+O1, P1'=1+O1, Q1_1'=1+Y, R1'=1+R1, S1'=1+R1, T1'=1+W, U1'=1+U1, V1'=1+A1, W1'=-1+W1, X1'=1+M1, Y1'=1+Y1, Z1'=1+Z1, A2'=1+Z1, B2'=1+B2, C2'=1+B2, D2'=1+D2, E2'=1+D2, F2'=1+F2, G2'=1+F2, H2'=1+H2, Q2'=1+H2, J2'=1+J2, K2'=1+K2, L2'=1+J2, M2'=1+M2, N2'=1+M2, O2'=-1+W1, P2'=1+P2, Q2_1'=1+P2, R2'=1+U1, S2'=1+S2, T2'=1+Y1, U2'=1+U2, V2'=1+K2, W2'=1+W2, X2'=1+X2, Y2'=1+X2, Z2'=1+Z2, A3'=1+Z2, B3'=1+B3, C3'=1+B3, D3'=1+D3, E3'=1+D3, F3'=1+F3, G3'=1+F3, H3'=1+H3, Q3'=1+Q3, J3'=1+H3, K3'=1+K3, L3'=1+K3, M3'=1+U2, N3'=1+N3, O3'=1+N3, P3'=1+S2, Q3_1'=1+Q3_1, R3'=1+W2, S3'=-1+S3, T3'=1+Q3, U3'=-1+U3, V3'=1+V3, W3'=1+V3, X3'=1+X3, Y3'=1+X3, Z3'=1+Z3, A4'=1+Z3, B4'=1+B4, C4'=1+B4, D4'=1+D4, E4'=1+D4, F4'=1+F4, G4'=-1+G4, H4'=1+F4, Q4'=1+Q4, J4'=1+Q4, K4'=-1+S3, L4'=1+L4, M4'=1+L4, N4'=1+Q3_1, O4'=-1+U3, P4'=-1+G4, [ A>=1+B && B>=1+D && 2>=F+D && 2>=H+F && H>=1+J && 0>=1+L && M>=1+L && L>=1+O && O+J>=1+2*Q_1 && L>=1+S && 2>=U+S && 1+W>=2*A && 1+Y>=2*M && A1>=1+B1 && B1>=1+D1 && 2>=F1+D1 && 2>=H1+F1 && H1>=1+J1 && 1>=L1 && M1>=1+L1 && L1>=1+O1 && O1+J1>=1+2*Y && L1>=1+R1 && 2>=R1+W && U+U1>=2+2*A1 && Q_1+W1>=1+2*M1 && Y1>=1+Z1 && Z1>=1+B2 && 2>=D2+B2 && 2>=D2+F2 && F2>=1+H2 && 2>=J2 && K2>=1+J2 && J2>=1+M2 && 2*W1>=2+M2+H2 && J2>=1+P2 && 2>=P2+U1 && S2+W>=2+2*Y1 && Y+U2>=1+2*K2 && W2>=1+X2 && X2>=1+Z2 && 2>=Z2+B3 && 2>=D3+B3 && D3>=1+F3 && 2>=H3 && Q3>=1+H3 && H3>=1+K3 && F3+K3>=1+2*U2 && H3>=1+N3 && 2>=S2+N3 && U1+Q3_1>=2+2*W2 && S3+W1>=1+2*Q3 && U3>=1+V3 && V3>=1+X3 && 2>=Z3+X3 && 2>=Z3+B4 && B4>=1+D4 && 2>=F4 && G4>=1+F4 && F4>=1+Q4 && 2*S3>=2+Q4+D4 && F4>=1+L4 && 2>=L4+Q3_1 && 2*U3>=1+S2 && 2*G4>=4+U2 ], cost: 60 1220: f1 -> [61] : A'=1+A, B'=1+B, C'=1+B, D'=1+D, E'=1+D, F'=1+F, G'=1+F, H'=1+H, Q'=1+H, J'=1+J, K'=1+J, L'=1+L, M'=1+M, N'=1+L, O'=1+O, P'=1+O, Q_1'=1+Q_1, R'=1+Q_1, S'=1+S, T'=1+S, U'=1+U, V'=1+U, W'=1+W, X'=1+A, Y'=1+Y, Z'=1+M, A1'=1+A1, B1'=1+B1, C1'=1+B1, D1'=1+D1, E1'=1+D1, F1'=1+F1, G1'=1+F1, H1'=1+H1, Q1'=1+H1, J1'=1+J1, K1'=1+J1, L1'=1+L1, M1'=-1+M1, N1'=1+L1, O1'=1+O1, P1'=1+O1, Q1_1'=1+Y, R1'=1+R1, S1'=1+R1, T1'=1+W, U1'=1+U1, V1'=1+A1, W1'=1+W1, X1'=-1+M1, Y1'=1+Y1, Z1'=1+Z1, A2'=1+Z1, B2'=1+B2, C2'=1+B2, D2'=1+D2, E2'=1+D2, F2'=1+F2, G2'=1+F2, H2'=1+H2, Q2'=1+H2, J2'=-1+J2, K2'=1+K2, L2'=-1+J2, M2'=-1+M2, N2'=-1+M2, O2'=1+W1, P2'=1+P2, Q2_1'=1+P2, R2'=1+U1, S2'=1+S2, T2'=1+Y1, U2'=1+U2, V2'=1+K2, W2'=1+W2, X2'=1+X2, Y2'=1+X2, Z2'=1+Z2, A3'=1+Z2, B3'=1+B3, C3'=1+B3, D3'=1+D3, E3'=1+D3, F3'=1+F3, G3'=1+F3, H3'=1+H3, Q3'=1+Q3, J3'=1+H3, K3'=1+K3, L3'=1+K3, M3'=1+U2, N3'=1+N3, O3'=1+N3, P3'=1+S2, Q3_1'=1+Q3_1, R3'=1+W2, S3'=-1+S3, T3'=1+Q3, U3'=-1+U3, V3'=1+V3, W3'=1+V3, X3'=1+X3, Y3'=1+X3, Z3'=1+Z3, A4'=1+Z3, B4'=1+B4, C4'=1+B4, D4'=1+D4, E4'=1+D4, F4'=1+F4, G4'=-1+G4, H4'=1+F4, Q4'=1+Q4, J4'=1+Q4, K4'=-1+S3, L4'=1+L4, M4'=1+L4, N4'=1+Q3_1, O4'=-1+U3, P4'=-1+G4, [ A>=1+B && B>=1+D && 2>=F+D && 2>=H+F && H>=1+J && 0>=1+L && M>=1+L && L>=1+O && O+J>=1+2*Q_1 && L>=1+S && 2>=U+S && 1+W>=2*A && 1+Y>=2*M && A1>=1+B1 && B1>=1+D1 && 2>=F1+D1 && 2>=H1+F1 && H1>=1+J1 && 1>=L1 && M1>=1+L1 && L1>=1+O1 && O1+J1>=1+2*Y && L1>=1+R1 && 2>=R1+W && U+U1>=2+2*A1 && 2*M1>=2+Q_1+W1 && Y1>=1+Z1 && Z1>=1+B2 && 2>=D2+B2 && 2>=D2+F2 && F2>=1+H2 && J2>=4 && M2>=1+J2 && M2+H2>=1+2*W1 && J2>=1+P2 && 2>=P2+U1 && S2+W>=2+2*Y1 && Y+U2>=1+2*K2 && W2>=1+X2 && X2>=1+Z2 && 2>=Z2+B3 && 2>=D3+B3 && D3>=1+F3 && 2>=H3 && Q3>=1+H3 && H3>=1+K3 && F3+K3>=1+2*U2 && H3>=1+N3 && 2>=S2+N3 && U1+Q3_1>=2+2*W2 && S3+W1>=1+2*Q3 && U3>=1+V3 && V3>=1+X3 && 2>=Z3+X3 && 2>=Z3+B4 && B4>=1+D4 && 2>=F4 && G4>=1+F4 && F4>=1+Q4 && 2*S3>=2+Q4+D4 && F4>=1+L4 && 2>=L4+Q3_1 && 2*U3>=1+S2 && 2*G4>=4+U2 ], cost: 60 1221: f1 -> [61] : [], cost: 0 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),?)