YES Termination proof succeeded Initially, performed program simplifications using lexicographic rank functions: * Removed transitions 121, 123, 124, 129 using the following rank functions: - Rank function 1: RF for loc. 87: -1+2*nDim_0-2*ni_0 RF for loc. 104: 2*nDim_0-2*ni_0 Bound for (chained) transitions 121, 129: 1 - Rank function 2: RF for loc. 87: 0 RF for loc. 104: 1 Bound for (chained) transitions 123: 1 Bound for (chained) transitions 124: 1 * Removed transitions 100, 102, 103, 112, 114, 115, 138, 139, 140, 141, 142, 151, 152, 153, 154, 155, 157 using the following rank functions: - Rank function 1: RF for loc. 69: 10*nN_0-10*ni_0 RF for loc. 70: -8+10*nN_0-10*ni_0 RF for loc. 71: -8+10*nN_0-10*ni_0 RF for loc. 72: -8+10*nN_0-10*ni_0 RF for loc. 73: -8+10*nN_0-10*ni_0 RF for loc. 74: -8+10*nN_0-10*ni_0 RF for loc. 75: -8+10*nN_0-10*ni_0 RF for loc. 96: 1+10*nN_0-10*ni_0 RF for loc. 100: -8+10*nN_0-10*ni_0 Bound for (chained) transitions 157: 10 - Rank function 2: RF for loc. 69: -2+10*nN_0-10*nj_0 RF for loc. 70: 2+10*nN_0-10*nj_0 RF for loc. 71: 10*nN_0-10*nj_0 RF for loc. 72: -7+10*nN_0-10*nj_0 RF for loc. 73: -6+10*nN_0-10*nj_0 RF for loc. 74: -5+10*nN_0-10*nj_0 RF for loc. 75: -4+10*nN_0-10*nj_0 RF for loc. 96: -1+10*nN_0-10*nj_0 RF for loc. 100: 1+10*nN_0-10*nj_0 Bound for (chained) transitions 155: 10 - Rank function 3: RF for loc. 69: -7 RF for loc. 70: -3 RF for loc. 71: -5 RF for loc. 72: -2 RF for loc. 73: -1 RF for loc. 74: 0 RF for loc. 75: 1 RF for loc. 96: -6 RF for loc. 100: -4 Bound for (chained) transitions 100, 154: -5 Bound for (chained) transitions 102: -6 Bound for (chained) transitions 103: -6 Bound for (chained) transitions 112: -3 Bound for (chained) transitions 114: -4 Bound for (chained) transitions 115: -4 Bound for (chained) transitions 138: -2 Bound for (chained) transitions 139: -1 Bound for (chained) transitions 140: 0 Bound for (chained) transitions 141: 0 Bound for (chained) transitions 142: 0 Bound for (chained) transitions 151: 1 Bound for (chained) transitions 152: 1 Bound for (chained) transitions 153: 1 * Removed transitions 176, 178, 179, 186, 188, 189, 194, 195, 196, 197, 198, 199, 200, 201, 210, 211, 212 using the following rank functions: - Rank function 1: RF for loc. 77: 10*nDim_0-10*nj_0 RF for loc. 78: -1+10*nDim_0-10*nj_0 RF for loc. 79: -1+10*nDim_0-10*nj_0 RF for loc. 80: -4+10*nDim_0-10*nj_0 RF for loc. 81: -5+10*nDim_0-10*nj_0 RF for loc. 82: -3+10*nDim_0-10*nj_0 RF for loc. 83: -2+10*nDim_0-10*nj_0 RF for loc. 120: 1+10*nDim_0-10*nj_0 RF for loc. 124: -1+10*nDim_0-10*nj_0 Bound for (chained) transitions 212: 10 - Rank function 2: RF for loc. 77: -5 RF for loc. 78: 1 RF for loc. 79: 1 RF for loc. 80: -2 RF for loc. 81: -3 RF for loc. 82: -1 RF for loc. 83: 0 RF for loc. 120: -4 RF for loc. 124: 1 Bound for (chained) transitions 176, 195: -3 Bound for (chained) transitions 178: -4 Bound for (chained) transitions 179: -4 Bound for (chained) transitions 196: -1 Bound for (chained) transitions 197: -1 Bound for (chained) transitions 198: -1 Bound for (chained) transitions 199: 0 Bound for (chained) transitions 200: 0 Bound for (chained) transitions 201: 0 Bound for (chained) transitions 211: 1 - Rank function 3: RF for loc. 78: 2+3*nDim_0-3*ni_0 RF for loc. 79: 3*nDim_0-3*ni_0 RF for loc. 80: 1 RF for loc. 81: 0 RF for loc. 124: 1+3*nDim_0-3*ni_0 Bound for (chained) transitions 194: 1 Bound for (chained) transitions 210: 3 - Rank function 4: RF for loc. 78: 1 RF for loc. 79: -1 RF for loc. 124: 0 Bound for (chained) transitions 186: 1 Bound for (chained) transitions 188: 0 Bound for (chained) transitions 189: 0 * Removed transitions 92, 93, 94, 95, 96, 97, 98, 99, 108, 109, 111, 143, 145, 146, 158, 160, 161 using the following rank functions: - Rank function 1: RF for loc. 60: -3+7*nDim_0-7*ni_0 RF for loc. 61: -4+7*nDim_0-7*ni_0 RF for loc. 63: -2+7*nDim_0-7*ni_0 RF for loc. 64: -1+7*nDim_0-7*ni_0 RF for loc. 65: 7*nDim_0-7*ni_0 RF for loc. 66: 7*nDim_0-7*ni_0 RF for loc. 67: 1+7*nDim_0-7*ni_0 RF for loc. 112: 2+7*nDim_0-7*ni_0 RF for loc. 116: 7*nDim_0-7*ni_0 Bound for (chained) transitions 111: 8 - Rank function 2: RF for loc. 60: -3+3*nDim_0-3*nj_0 RF for loc. 61: -4+3*nDim_0-3*nj_0+tmp___4_0 RF for loc. 63: -2+3*nDim_0-3*nj_0 RF for loc. 64: -1+3*nDim_0-3*nj_0 RF for loc. 65: 3*nDim_0-3*nj_0 RF for loc. 66: 2+3*nDim_0-3*nj_0 RF for loc. 67: -6+bSum_0+3*nDim_0-3*nj_0 RF for loc. 112: -5+bSum_0+3*nDim_0-3*nj_0 RF for loc. 116: 1+3*nDim_0-3*nj_0 Bound for (chained) transitions 108: 3 - Rank function 3: RF for loc. 60: -4 RF for loc. 61: -5 RF for loc. 63: -3 RF for loc. 64: -2 RF for loc. 65: -1 RF for loc. 66: 1 RF for loc. 67: -7 RF for loc. 112: -6 RF for loc. 116: 0 Bound for (chained) transitions 92: -4 Bound for (chained) transitions 93, 143: -5 Bound for (chained) transitions 94: -3 Bound for (chained) transitions 95: -3 Bound for (chained) transitions 96: -3 Bound for (chained) transitions 97: -2 Bound for (chained) transitions 98: -2 Bound for (chained) transitions 99: -2 Bound for (chained) transitions 109: -1 Bound for (chained) transitions 145: -6 Bound for (chained) transitions 146: -6 Bound for (chained) transitions 158: 1 Bound for (chained) transitions 160: 0 Bound for (chained) transitions 161: 0 * Removed transitions 120, 130, 132, 133 using the following rank functions: - Rank function 1: RF for loc. 84: -1+2*nDim_0-2*ni_0 RF for loc. 108: 2*nDim_0-2*ni_0 Bound for (chained) transitions 120, 130: 1 - Rank function 2: RF for loc. 84: 0 RF for loc. 108: 1 Bound for (chained) transitions 132: 1 Bound for (chained) transitions 133: 1 * Removed transitions 166, 167, 168, 169, 170, 171, 172, 173, 175, 213, 215, 216 using the following rank functions: - Rank function 1: RF for loc. 88: -7+8*nN_0-8*ni_0 RF for loc. 90: -6+8*nN_0-8*ni_0 RF for loc. 91: -6+8*nN_0-8*ni_0 RF for loc. 92: -5+8*nN_0-8*ni_0 RF for loc. 93: -1+8*nN_0-8*ni_0 RF for loc. 132: 8*nN_0-8*ni_0 Bound for (chained) transitions 175: 7 - Rank function 2: RF for loc. 88: -3 RF for loc. 90: -2 RF for loc. 91: -1 RF for loc. 92: 0 RF for loc. 93: -5 RF for loc. 132: -4 Bound for (chained) transitions 166, 213: -3 Bound for (chained) transitions 167: -2 Bound for (chained) transitions 168: -2 Bound for (chained) transitions 169: -1 Bound for (chained) transitions 170: -1 Bound for (chained) transitions 171: 0 Bound for (chained) transitions 172: 0 Bound for (chained) transitions 173: 0 Bound for (chained) transitions 215: -4 Bound for (chained) transitions 216: -4 * Removed transitions 185, 202, 204, 205 using the following rank functions: - Rank function 1: RF for loc. 94: -1+2*nN_0-2*ni_0 RF for loc. 128: 2*nN_0-2*ni_0 Bound for (chained) transitions 185, 202: 1 - Rank function 2: RF for loc. 94: -1 RF for loc. 128: 0 Bound for (chained) transitions 204: 0 Bound for (chained) transitions 205: 0 Errors: