    addb0: x260 <= 0
    addb1: x261 <= 0
    addb2: x262 <= 0
    addb3: x263 <= 0
    addb4: x264 <= 0
    addb5: x265 <= 0
    addb6: x266 <= 0
    addb7: x267 <= 0
    addb8: x268 <= 0
    addb9: x269 <= 0
    addb10: x270 <= 0
    addb11: x271 <= 0
    addb12: x272 <= 0
    addb13: x273 <= 0
    addb14: x274 <= 0
    addb15: x275 <= 0
    addb16: x276 <= 0
    addb17: x277 <= 0
    addb18: x278 <= 0
    addb19: x279 <= 0
    addb20: x280 <= 0
    addb21: x281 <= 0
    addb22: x282 <= 0
    addb23: x283 <= 0
    addb24: x284 <= 0
    addb25: x285 <= 0
    addb26: x286 <= 0
    addb27: x287 <= 0
    addb28: x288 <= 0
    addb29: x289 <= 0
    addb30: x290 <= 0
    addb31: x291 <= 0
    addb32: x292 <= 0
    addb33: x293 <= 0
    addb34: x294 <= 0
    addb35: x295 <= 0
    addb36: x296 <= 0
    addb37: x297 <= 0
    addb38: x298 <= 0
    addb39: x299 <= 0
    addb40: x300 <= 0
    addb41: x301 <= 0
    addb42: x302 <= 0
    addb43: x303 <= 0
    addb44: x304 <= 0
    addb45: x305 <= 0
    addb46: x306 <= 0
    addb47: x307 <= 0    
    addc0: x260 - x284 <= 0
    addc1: x260 - x288 <= 0
    addc2: x260 - x292 <= 0
    addc3: x260 - x296 <= 0
    addc4: x260 - x300 <= 0
    addc5: x260 - x304 <= 0
    addc6: x264 - x284 <= 0
    addc7: x264 - x288 <= 0
    addc8: x264 - x292 <= 0
    addc9: x264 - x296 <= 0
    addc10: x264 - x300 <= 0
    addc11: x264 - x304 <= 0
    addc12: x268 - x284 <= 0
    addc13: x268 - x288 <= 0
    addc14: x268 - x292 <= 0
    addc15: x268 - x296 <= 0
    addc16: x268 - x300 <= 0
    addc17: x268 - x304 <= 0
    addc18: x272 - x284 <= 0
    addc19: x272 - x288 <= 0
    addc20: x272 - x292 <= 0
    addc21: x272 - x296 <= 0
    addc22: x272 - x300 <= 0
    addc23: x272 - x304 <= 0
    addc24: x276 - x284 <= 0
    addc25: x276 - x288 <= 0
    addc26: x276 - x292 <= 0
    addc27: x276 - x296 <= 0
    addc28: x276 - x300 <= 0
    addc29: x276 - x304 <= 0
    addc30: x280 - x284 <= 0
    addc31: x280 - x288 <= 0
    addc32: x280 - x292 <= 0
    addc33: x280 - x296 <= 0
    addc34: x280 - x300 <= 0
    addc35: x280 - x304 <= 0
    addc36: x261 - x285 <= 0
    addc37: x261 - x289 <= 0
    addc38: x261 - x293 <= 0
    addc39: x261 - x297 <= 0
    addc40: x261 - x301 <= 0
    addc41: x261 - x305 <= 0
    addc42: x265 - x285 <= 0
    addc43: x265 - x289 <= 0
    addc44: x265 - x293 <= 0
    addc45: x265 - x297 <= 0
    addc46: x265 - x301 <= 0
    addc47: x265 - x305 <= 0
    addc48: x269 - x285 <= 0
    addc49: x269 - x289 <= 0
    addc50: x269 - x293 <= 0
    addc51: x269 - x297 <= 0
    addc52: x269 - x301 <= 0
    addc53: x269 - x305 <= 0
    addc54: x273 - x285 <= 0
    addc55: x273 - x289 <= 0
    addc56: x273 - x293 <= 0
    addc57: x273 - x297 <= 0
    addc58: x273 - x301 <= 0
    addc59: x273 - x305 <= 0
    addc60: x277 - x285 <= 0
    addc61: x277 - x289 <= 0
    addc62: x277 - x293 <= 0
    addc63: x277 - x297 <= 0
    addc64: x277 - x301 <= 0
    addc65: x277 - x305 <= 0
    addc66: x281 - x285 <= 0
    addc67: x281 - x289 <= 0
    addc68: x281 - x293 <= 0
    addc69: x281 - x297 <= 0
    addc70: x281 - x301 <= 0
    addc71: x281 - x305 <= 0
    addc72: x262 - x286 <= 0
    addc73: x262 - x290 <= 0
    addc74: x262 - x294 <= 0
    addc75: x262 - x298 <= 0
    addc76: x262 - x302 <= 0
    addc77: x262 - x306 <= 0
    addc78: x266 - x286 <= 0
    addc79: x266 - x290 <= 0
    addc80: x266 - x294 <= 0
    addc81: x266 - x298 <= 0
    addc82: x266 - x302 <= 0
    addc83: x266 - x306 <= 0
    addc84: x270 - x286 <= 0
    addc85: x270 - x290 <= 0
    addc86: x270 - x294 <= 0
    addc87: x270 - x298 <= 0
    addc88: x270 - x302 <= 0
    addc89: x270 - x306 <= 0
    addc90: x274 - x286 <= 0
    addc91: x274 - x290 <= 0
    addc92: x274 - x294 <= 0
    addc93: x274 - x298 <= 0
    addc94: x274 - x302 <= 0
    addc95: x274 - x306 <= 0
    addc96: x278 - x286 <= 0
    addc97: x278 - x290 <= 0
    addc98: x278 - x294 <= 0
    addc99: x278 - x298 <= 0
    addc100: x278 - x302 <= 0
    addc101: x278 - x306 <= 0
    addc102: x282 - x286 <= 0
    addc103: x282 - x290 <= 0
    addc104: x282 - x294 <= 0
    addc105: x282 - x298 <= 0
    addc106: x282 - x302 <= 0
    addc107: x282 - x306 <= 0
    addc108: x263 - x287 <= 0
    addc109: x263 - x291 <= 0
    addc110: x263 - x295 <= 0
    addc111: x263 - x299 <= 0
    addc112: x263 - x303 <= 0
    addc113: x263 - x307 <= 0
    addc114: x267 - x287 <= 0
    addc115: x267 - x291 <= 0
    addc116: x267 - x295 <= 0
    addc117: x267 - x299 <= 0
    addc118: x267 - x303 <= 0
    addc119: x267 - x307 <= 0
    addc120: x271 - x287 <= 0
    addc121: x271 - x291 <= 0
    addc122: x271 - x295 <= 0
    addc123: x271 - x299 <= 0
    addc124: x271 - x303 <= 0
    addc125: x271 - x307 <= 0
    addc126: x275 - x287 <= 0
    addc127: x275 - x291 <= 0
    addc128: x275 - x295 <= 0
    addc129: x275 - x299 <= 0
    addc130: x275 - x303 <= 0
    addc131: x275 - x307 <= 0
    addc132: x279 - x287 <= 0
    addc133: x279 - x291 <= 0
    addc134: x279 - x295 <= 0
    addc135: x279 - x299 <= 0
    addc136: x279 - x303 <= 0
    addc137: x279 - x307 <= 0
    addc138: x283 - x287 <= 0
    addc139: x283 - x291 <= 0
    addc140: x283 - x295 <= 0
    addc141: x283 - x299 <= 0
    addc142: x283 - x303 <= 0
    addc143: x283 - x307 <= 0
