Skip to content

Instantly share code, notes, and snippets.

@gdeest

gdeest/condition.c

Created December 9, 2015 09:06
Show Gist options
  • Save gdeest/7a5375ec52495468fc8a to your computer and use it in GitHub Desktop.
Save gdeest/7a5375ec52495468fc8a to your computer and use it in GitHub Desktop.
Download ZIP
Raw
condition.c
t_idx >= x0_idx + 2 * x1_idx || (x0_idx + x1_idx + 1 >= t_idx && 2 * x0_idx + x1_idx + 2 >= t_idx && x0_idx + 2 * x1_idx + 2 >= t_idx) || (x1_idx >= x0_idx && t_idx >= 2 * x0_idx + x1_idx && x0_idx + 2 * x1_idx + 2 >= t_idx) || (2 * x0_idx + x1_idx >= t_idx + 1 && t_idx >= x0_idx + x1_idx + 1 && x0_idx + 2 * x1_idx >= t_idx + 1 && 384 * x0_idx + 192 * x1_idx + 3 >= 192 * t_idx + N0 && 192 * t_idx + N1 >= 192 * x0_idx + 384 * x1_idx + 4) || (2 * x0_idx + x1_idx >= t_idx + 1 && t_idx >= x0_idx + x1_idx + 1 && x0_idx + 2 * x1_idx >= t_idx + 1 && 192 * t_idx + N0 >= 384 * x0_idx + 192 * x1_idx + 4 && 384 * x0_idx + 192 * x1_idx + 192 >= 192 * t_idx + N0 && 192 * t_idx + N1 >= 192 * x0_idx + 384 * x1_idx + 4) || (t_idx >= x1_idx + 2 && t_idx >= 2 * x0_idx + x1_idx + 1 && 2 * x0_idx + x1_idx + 2 >= t_idx && x0_idx + 2 * x1_idx >= t_idx + 1 && N0 <= 6 && 96 * t_idx + N1 >= 288 * x1_idx + 289) || (t_idx >= x0_idx + 1 && 3 * x0_idx >= t_idx + 1 && t_idx >= x0_idx + 2 * x1_idx && 96 * t_idx + N0 >= 288 * x0_idx + 5 && 384 * x0_idx + 192 * x1_idx + 192 >= 192 * t_idx + N0 && N1 >= 7) || (t_idx >= x0_idx + 1 && 3 * x0_idx >= t_idx + 1 && t_idx >= x0_idx + 2 * x1_idx && x0_idx + 2 * x1_idx + 1 >= t_idx && 288 * x0_idx + 4 >= 96 * t_idx + N0 && N1 >= 7) || (t_idx >= x1_idx + 2 && t_idx >= 2 * x0_idx + x1_idx + 1 && x0_idx + 2 * x1_idx >= t_idx + 1 && N0 <= 6 && 96 * t_idx + N1 >= 288 * x1_idx + 6 && 288 * x1_idx + 288 >= 96 * t_idx + N1 && 576 * x0_idx + N1 + 557 >= 192 * t_idx) || (t_idx >= x1_idx + 2 && t_idx >= 2 * x0_idx + x1_idx + 1 && 2 * x0_idx + x1_idx + 2 >= t_idx && t_idx >= x0_idx + 2 * x1_idx && x0_idx + 2 * x1_idx + 1 >= t_idx && N0 <= 6 && 96 * t_idx + N1 >= 288 * x1_idx + 289) || (2 * x0_idx + x1_idx >= t_idx + 1 && x0_idx + 2 * x1_idx >= t_idx + 1 && 192 * t_idx + N0 >= 384 * x0_idx + 192 * x1_idx + 193 && 192 * t_idx >= 192 * x1_idx + N0 + 192 && 576 * x0_idx + N1 + 569 >= 192 * t_idx + 2 * N0 && 126 * t_idx + N1 + 3 * ((6 * t_idx + 7 * N0 + N1 + 2) / 9) >= 384 * x1_idx + 3 * N0 + 4 && 192 * x1_idx + 5 * N0 + 2 >= 60 * t_idx + 6 * ((6 * t_idx + 7 * N0 + N1 + 2) / 9)) || (2 * x0_idx + x1_idx >= t_idx + 1 && t_idx >= x0_idx + x1_idx + 1 && x0_idx + 2 * x1_idx >= t_idx + 1 && 192 * x0_idx + N1 >= 192 * x1_idx + N0 + 1 && 192 * x0_idx + 384 * x1_idx + 3 >= 192 * t_idx + N1 && 3 * floord(-192 * x0_idx + 192 * x1_idx + N0 + 2, 3) >= N1 && 192 * t_idx + 6 * floord(-192 * x0_idx + 192 * x1_idx + N0 + 2, 3) + 180 >= 576 * x1_idx + N0) || (2 * x0_idx + x1_idx >= t_idx + 1 && t_idx >= x0_idx + x1_idx + 1 && x0_idx + 2 * x1_idx >= t_idx + 1 && 192 * x0_idx + 384 * x1_idx + 3 >= 192 * t_idx + N1 && 192 * t_idx + N1 + 185 >= 192 * x0_idx + 384 * x1_idx && 192 * x0_idx + N1 >= ((N1 + 2) % 3) + 192 * x1_idx + N0 + 1) || (t_idx >= x0_idx + 1 && 3 * x0_idx >= t_idx + 1 && t_idx >= x0_idx + 2 * x1_idx && x0_idx + 2 * x1_idx + 1 >= t_idx && 192 * t_idx + N0 >= 384 * x0_idx + 192 * x1_idx + 193 && 192 * x0_idx + 189 >= N0 && 192 * x1_idx + N0 + 191 >= 192 * t_idx && N1 >= 7 && N0 + N1 + 2 >= 192 * t_idx) || (x0_idx >= 0 && x1_idx >= 0 && t_idx >= x0_idx + x1_idx && 2 * x0_idx + x1_idx + 2 >= t_idx && x0_idx + 2 * x1_idx + 2 >= t_idx && 192 * t_idx + 180 >= N1 && 192 * t_idx + 186 >= 192 * x0_idx + N1 && 192 * x1_idx + 189 >= N1 && 192 * x0_idx + 384 * x1_idx + 570 >= 192 * t_idx + N1) || (t_idx >= x1_idx + 2 && t_idx >= 2 * x0_idx + x1_idx + 1 && t_idx >= x0_idx + 2 * x1_idx && x0_idx + 2 * x1_idx + 1 >= t_idx && N0 <= 6 && N1 >= 7 && 96 * t_idx + N1 >= 288 * x1_idx + 6 && 288 * x1_idx + 288 >= 96 * t_idx + N1 && 576 * x0_idx + N1 + 557 >= 192 * t_idx) || (2 * x0_idx + x1_idx >= t_idx + 1 && x0_idx + 2 * x1_idx >= t_idx + 1 && 192 * t_idx + N0 >= 384 * x0_idx + 192 * x1_idx + 193 && 192 * t_idx >= 192 * x1_idx + N0 + 192 && 576 * x1_idx + N0 + 4 >= 192 * t_idx + 2 * N1 && 384 * x0_idx + 3 * floord(2 * N0 + 2 * N1 + 1, 3) + 375 >= 384 * x1_idx + 4 * N0 && ((2 * N0 + 2 * N1 + 1) % 3) + 3 * ((-((2 * N0 + 2 * N1 + 1) % 3) + 4 * N0 + 2 * N1 + 4) / 6) >= 2 * N0 + N1 + 2) || (2 * x0_idx + x1_idx >= t_idx + 1 && t_idx >= x0_idx + x1_idx + 1 && x0_idx + 2 * x1_idx >= t_idx + 1 && 192 * x1_idx + N0 >= 192 * x0_idx + N1 && 192 * x0_idx + 384 * x1_idx + 3 >= 192 * t_idx + N1 && 192 * t_idx + 2 * N1 + 184 >= 576 * x1_idx + N0 && ((2 * N0 + 2 * N1 + 1) % 3) + 3 * ((-((2 * N0 + 2 * N1 + 1) % 3) + 4 * N0 + 2 * N1 + 4) / 6) >= 2 * N0 + N1 + 2) || (t_idx >= x1_idx + 2 && t_idx >= 2 * x0_idx + x1_idx + 1 && x0_idx + 2 * x1_idx >= t_idx + 1 && 96 * t_idx + N1 >= 288 * x1_idx + 289 && 576 * x1_idx + N0 + 571 >= 192 * t_idx + 2 * N1 && 2 * (2 * N0 % 3) >= ((6 * t_idx + 7 * N0 + N1 + 2) % 9) + 1 && 576 * x0_idx + N1 + 569 >= 2 * (2 * N0 % 3) + 192 * t_idx + 2 * N0) || (2 * x0_idx + x1_idx >= t_idx + 1 && x0_idx + 2 * x1_idx >= t_idx + 1 && 192 * t_idx + N0 >= 384 * x0_idx + 192 * x1_idx + 193 && 192 * t_idx >= 192 * x1_idx + N0 + 192 && 576 * x1_idx + N0 + 4 >= 192 * t_idx + 2 * N1 && 384 * x0_idx + 3 * floord(2 * N0 + 2 * N1 + 1, 3) + 375 >= 384 * x1_idx + 4 * N0 && ((-((2 * N0 + 2 * N1 + 1) % 3) + 4 * N0 + 2 * N1 + 4) % 6) + 2 * N0 + 2 * N1 >= ((2 * N0 + 2 * N1 + 1) % 3) + 3 * ((2 * N0 + 2 * N1 + 1) / 3) + 2) || (2 * x0_idx + x1_idx >= t_idx + 1 && x0_idx + 2 * x1_idx >= t_idx + 1 && 192 * t_idx + N0 >= 384 * x0_idx + 192 * x1_idx + 193 && 192 * t_idx >= 192 * x1_idx + N0 + 192 && 576 * x1_idx + N0 + 571 >= 192 * t_idx + 2 * N1 && 60 * t_idx + 6 * floord(6 * t_idx + 7 * N0 + N1 + 2, 9) >= 192 * x1_idx + 5 * N0 + 3 && 2 * (2 * N0 % 3) >= ((6 * t_idx + 7 * N0 + N1 + 2) % 9) + 1 && 576 * x0_idx + N1 + 569 >= 2 * (2 * N0 % 3) + 192 * t_idx + 2 * N0) || (2 * x0_idx + x1_idx >= t_idx + 1 && t_idx >= x0_idx + x1_idx + 1 && x0_idx + 2 * x1_idx >= t_idx + 1 && 192 * x1_idx + N0 >= 192 * x0_idx + N1 && 192 * x0_idx + 384 * x1_idx + 3 >= 192 * t_idx + N1 && 192 * t_idx + N1 + 3 * floord(2 * N0 + 3 * floord(2 * N0 + 2 * N1 + 1, 3) + 3, 6) + 182 >= 576 * x1_idx + 3 * N0 && ((-((2 * N0 + 2 * N1 + 1) % 3) + 4 * N0 + 2 * N1 + 4) % 6) + 2 * N0 + 2 * N1 >= ((2 * N0 + 2 * N1 + 1) % 3) + 3 * ((2 * N0 + 2 * N1 + 1) / 3) + 2) || (t_idx >= x1_idx + 2 && t_idx >= 2 * x0_idx + x1_idx + 1 && x0_idx + 2 * x1_idx >= t_idx + 1 && N0 >= 7 && 288 * x1_idx + 288 >= 96 * t_idx + N1 && 60 * t_idx + 6 * floord(6 * t_idx + 7 * N0 + N1 + 2, 9) >= 192 * x1_idx + 5 * N0 + 3 && ((6 * t_idx + 7 * N0 + N1 + 2) % 9) + 2 * ((N0 - 1) % 3) <= 3 && 2 * ((N0 - 1) % 3) + 576 * x0_idx + N1 + 565 >= 192 * t_idx + 2 * N0) || (t_idx >= x1_idx + 2 && t_idx >= 2 * x0_idx + x1_idx + 1 && x0_idx + 2 * x1_idx >= t_idx + 1 && 96 * t_idx + N1 >= 288 * x1_idx + 289 && 576 * x0_idx + N1 + 569 >= 192 * t_idx + 2 * N0 && 576 * x1_idx + N0 + 571 >= 192 * t_idx + 2 * N1 && (6 * t_idx + 7 * N0 + N1 + 2) % 9 >= 2 * (2 * N0 % 3)) || (t_idx >= x1_idx + 2 && t_idx >= 2 * x0_idx + x1_idx + 1 && t_idx >= x0_idx + 2 * x1_idx && x0_idx + 2 * x1_idx + 1 >= t_idx && 96 * t_idx + N1 >= 288 * x1_idx + 289 && 576 * x1_idx + N0 + 571 >= 192 * t_idx + 2 * N1 && 2 * (2 * N0 % 3) >= ((6 * t_idx + 7 * N0 + N1 + 2) % 9) + 1 && 576 * x0_idx + N1 + 569 >= 2 * (2 * N0 % 3) + 192 * t_idx + 2 * N0) || (2 * x0_idx + x1_idx >= t_idx + 1 && x0_idx + 2 * x1_idx >= t_idx + 1 && 192 * t_idx + N0 >= 384 * x0_idx + 192 * x1_idx + 193 && 192 * t_idx >= 192 * x1_idx + N0 + 192 && 576 * x0_idx + N1 + 569 >= 192 * t_idx + 2 * N0 && 192 * t_idx + 2 * N1 >= 576 * x1_idx + N0 + 5 && 384 * x1_idx + 3 * N0 + 3 >= 126 * t_idx + N1 + 3 * ((6 * t_idx + 7 * N0 + N1 + 2) / 9) && 66 * t_idx + 2 * N0 + N1 >= ((N1 + 2) % 3) + 192 * x1_idx + 3 * ((6 * t_idx + 7 * N0 + N1 + 2) / 9) + 1) || (2 * x0_idx + x1_idx >= t_idx + 1 && x0_idx + 2 * x1_idx >= t_idx + 1 && 192 * t_idx + N0 >= 384 * x0_idx + 192 * x1_idx + 193 && 192 * t_idx >= 192 * x1_idx + N0 + 192 && 576 * x0_idx + N1 + 569 >= 192 * t_idx + 2 * N0 && 576 * x1_idx + N0 + 571 >= 192 * t_idx + 2 * N1 && 60 * t_idx + 6 * ((6 * t_idx + 7 * N0 + N1 + 2) / 9) >= 192 * x1_idx + 5 * N0 + 3 && (6 * t_idx + 7 * N0 + N1 + 2) % 9 >= 2 * (2 * N0 % 3)) || (2 * x0_idx + x1_idx >= t_idx + 1 && x0_idx + 2 * x1_idx >= t_idx + 1 && 192 * t_idx + N0 >= 384 * x0_idx + 192 * x1_idx + 193 && 192 * t_idx >= 192 * x1_idx + N0 + 192 && 384 * x0_idx + 192 * x1_idx + 570 >= 192 * t_idx + N0 && 192 * t_idx + 2 * N1 >= 576 * x1_idx + N0 + 572 && 96 * t_idx + 7 * N0 + N1 >= 2 * (2 * N0 % 3) + 288 * x1_idx + 9 * (5 * N0 / 6) + 286) || (t_idx >= x1_idx + 2 && t_idx >= 2 * x0_idx + x1_idx + 1 && x0_idx + 2 * x1_idx >= t_idx + 1 && N0 >= 7 && 288 * x1_idx + 288 >= 96 * t_idx + N1 && 576 * x0_idx + N1 + 569 >= 192 * t_idx + 2 * N0 && 60 * t_idx + 6 * ((6 * t_idx + 7 * N0 + N1 + 2) / 9) >= 192 * x1_idx + 5 * N0 + 3 && ((6 * t_idx + 7 * N0 + N1 + 2) % 9) + 2 * ((N0 - 1) % 3) >= 4) || (t_idx >= x1_idx + 2 && t_idx >= 2 * x0_idx + x1_idx + 1 && x0_idx + 2 * x1_idx >= t_idx + 1 && N0 >= 7 && 384 * x0_idx + 192 * x1_idx + 570 >= 192 * t_idx + N0 && 192 * t_idx + 2 * N1 >= 576 * x1_idx + N0 + 572 && 2 * ((N0 - 1) % 3) + 96 * t_idx + 7 * N0 + N1 >= 288 * x1_idx + 9 * (5 * N0 / 6) + 290) || (t_idx >= x1_idx + 2 && t_idx >= 2 * x0_idx + x1_idx + 1 && t_idx >= x0_idx + 2 * x1_idx && x0_idx + 2 * x1_idx + 1 >= t_idx && 96 * t_idx + N1 >= 288 * x1_idx + 289 && 576 * x0_idx + N1 + 569 >= 192 * t_idx + 2 * N0 && 576 * x1_idx + N0 + 571 >= 192 * t_idx + 2 * N1 && (6 * t_idx + 7 * N0 + N1 + 2) % 9 >= 2 * (2 * N0 % 3)) || (3 * x0_idx >= t_idx + 1 && t_idx >= x0_idx + 2 * x1_idx && x0_idx + 2 * x1_idx + 1 >= t_idx && 192 * t_idx + N0 >= 384 * x0_idx + 192 * x1_idx + 193 && 192 * t_idx >= 192 * x1_idx + N0 + 192 && 576 * x1_idx + N0 + 571 >= 192 * t_idx + 2 * N1 && 60 * t_idx + 6 * floord(6 * t_idx + 7 * N0 + N1 + 2, 9) >= 192 * x1_idx + 5 * N0 + 3 && N1 >= ((6 * t_idx + 7 * N0 + N1 + 2) % 9) + 7 && 2 * (2 * N0 % 3) >= ((6 * t_idx + 7 * N0 + N1 + 2) % 9) + 1 && 576 * x0_idx + N1 + 569 >= 2 * (2 * N0 % 3) + 192 * t_idx + 2 * N0) || (3 * x0_idx >= t_idx + 1 && t_idx >= x0_idx + 2 * x1_idx && x0_idx + 2 * x1_idx + 1 >= t_idx && 192 * t_idx + N0 >= 384 * x0_idx + 192 * x1_idx + 193 && 192 * t_idx >= 192 * x1_idx + N0 + 192 && 384 * x0_idx + 192 * x1_idx + 570 >= 192 * t_idx + N0 && 192 * t_idx + 2 * N1 >= 576 * x1_idx + N0 + 572 && 96 * t_idx + 7 * N0 + N1 >= 2 * (2 * N0 % 3) + 288 * x1_idx + 9 * (5 * N0 / 6) + 286) || (t_idx >= x1_idx + 2 && t_idx >= 2 * x0_idx + x1_idx + 1 && t_idx >= x0_idx + 2 * x1_idx && x0_idx + 2 * x1_idx + 1 >= t_idx && N0 >= 7 && 288 * x1_idx + 288 >= 96 * t_idx + N1 && 60 * t_idx + 6 * floord(6 * t_idx + 7 * N0 + N1 + 2, 9) >= 192 * x1_idx + 5 * N0 + 3 && 9 * floord(6 * t_idx + 7 * N0 + N1 + 2, 9) >= 6 * t_idx + 7 * N0 + 9 && ((6 * t_idx + 7 * N0 + N1 + 2) % 9) + 2 * ((N0 - 1) % 3) <= 3 && 2 * ((N0 - 1) % 3) + 576 * x0_idx + N1 + 565 >= 192 * t_idx + 2 * N0) || (t_idx >= x1_idx + 2 && t_idx >= 2 * x0_idx + x1_idx + 1 && t_idx >= x0_idx + 2 * x1_idx && x0_idx + 2 * x1_idx + 1 >= t_idx && N0 >= 7 && 384 * x0_idx + 192 * x1_idx + 570 >= 192 * t_idx + N0 && 192 * t_idx + 2 * N1 >= 576 * x1_idx + N0 + 572 && 2 * ((N0 - 1) % 3) + 96 * t_idx + 7 * N0 + N1 >= 288 * x1_idx + 9 * (5 * N0 / 6) + 290) || (3 * x0_idx >= t_idx + 1 && t_idx >= x0_idx + 2 * x1_idx && x0_idx + 2 * x1_idx + 1 >= t_idx && 192 * t_idx + N0 >= 384 * x0_idx + 192 * x1_idx + 193 && 192 * t_idx >= 192 * x1_idx + N0 + 192 && 576 * x0_idx + N1 + 569 >= 192 * t_idx + 2 * N0 && 576 * x1_idx + N0 + 571 >= 192 * t_idx + 2 * N1 && 60 * t_idx + 6 * ((6 * t_idx + 7 * N0 + N1 + 2) / 9) >= 192 * x1_idx + 5 * N0 + 3 && N1 >= ((6 * t_idx + 7 * N0 + N1 + 2) % 9) + 7 && (6 * t_idx + 7 * N0 + N1 + 2) % 9 >= 2 * (2 * N0 % 3)) || (t_idx >= x1_idx + 2 && t_idx >= 2 * x0_idx + x1_idx + 1 && t_idx >= x0_idx + 2 * x1_idx && x0_idx + 2 * x1_idx + 1 >= t_idx && N0 >= 7 && 288 * x1_idx + 288 >= 96 * t_idx + N1 && 576 * x0_idx + N1 + 569 >= 192 * t_idx + 2 * N0 && 60 * t_idx + 6 * floord(6 * t_idx + 7 * N0 + N1 + 2, 9) >= 192 * x1_idx + 5 * N0 + 3 && 9 * floord(6 * t_idx + 7 * N0 + N1 + 2, 9) >= 6 * t_idx + 7 * N0 + 9 && ((6 * t_idx + 7 * N0 + N1 + 2) % 9) + 2 * ((N0 - 1) % 3) >= 4) || (x0_idx >= 1 && t_idx >= x0_idx + 1 && x0_idx + x1_idx == t_idx && 192 * x0_idx >= N0 && 192 * x0_idx + N1 >= 192 * t_idx + 1) || (x0_idx >= 1 && t_idx >= 3 * x0_idx + 1 && 2 * x0_idx + x1_idx == t_idx && N0 <= 6 && 576 * x0_idx + N1 >= 192 * t_idx + 10) || (t_idx >= x0_idx + 2 && 3 * x0_idx >= t_idx && x0_idx + 2 * x1_idx + 2 == t_idx && 288 * x0_idx + 18 >= 96 * t_idx + N0 && N1 >= 7) || (x0_idx >= 1 && t_idx >= x0_idx + 1 && x0_idx + x1_idx == t_idx && N0 >= 192 * x0_idx + 1 && 192 * x0_idx + 186 >= N0 && 192 * x0_idx + N1 >= 192 * t_idx + 1) || (x0_idx >= 1 && t_idx >= 3 * x0_idx + 1 && 2 * x0_idx + x1_idx == t_idx && N0 >= 7 && 192 * t_idx + 9 >= 576 * x0_idx + N1 && 1152 * x0_idx + 2 * N1 >= 384 * t_idx + N0 + 5) || (x0_idx >= 1 && t_idx >= 3 * x0_idx + 1 && 2 * x0_idx + x1_idx == t_idx && N0 <= 6 && 576 * x0_idx + N1 >= 192 * t_idx + 6 && 192 * t_idx + 9 >= 576 * x0_idx + N1) || (x0_idx >= 1 && t_idx >= 3 * x0_idx + 1 && 2 * x0_idx + x1_idx == t_idx && N0 <= 6 && 192 * t_idx + 5 >= 576 * x0_idx + N1 && 576 * x0_idx + N1 + 89 >= 192 * t_idx) || (x0_idx >= 1 && t_idx >= 3 * x0_idx + 1 && 2 * x0_idx + x1_idx == t_idx && N0 >= 7 && N0 <= 192 && 576 * x0_idx + N1 >= 192 * t_idx + 10) || (t_idx >= x0_idx + 3 && x0_idx >= 2 && x0_idx + x1_idx + 1 == t_idx && N0 >= 192 * x0_idx + 1 && 192 * x0_idx + 189 >= N0 && N0 + N1 + 2 >= 192 * t_idx) || (x0_idx >= 1 && t_idx >= 3 * x0_idx + 3 && 2 * x0_idx + x1_idx + 1 == t_idx && N0 <= 6 && 192 * t_idx >= 576 * x0_idx + N1 + 283 && 576 * x0_idx + N1 + 374 >= 192 * t_idx) || (t_idx >= x0_idx + 2 && 3 * x0_idx >= t_idx && x0_idx + 2 * x1_idx + 2 == t_idx && 96 * t_idx + N0 >= 288 * x0_idx + 19 && 288 * x0_idx + 2 * N1 + 4 >= 96 * t_idx + N0 && 144 * x0_idx + 7 * N0 + 8 >= 48 * t_idx + 9 * (5 * N0 / 6)) || (x0_idx >= 1 && t_idx >= x0_idx + 1 && x0_idx + x1_idx == t_idx && 384 * x0_idx + N1 >= 192 * t_idx + N0 + 1 && 192 * t_idx >= 192 * x0_idx + N1 && 192 * t_idx + N0 + 2 >= 384 * x0_idx + 3 * floord(N1 + 2, 3) && 576 * x0_idx + 6 * floord(N1 + 2, 3) + 180 >= 384 * t_idx + N0) || (x0_idx >= 1 && t_idx >= x0_idx + 1 && x0_idx + x1_idx == t_idx && 192 * t_idx >= 192 * x0_idx + N1 && 192 * x0_idx + N1 + 185 >= 192 * t_idx && 384 * x0_idx + N1 >= ((N1 + 2) % 3) + 192 * t_idx + N0 + 1) || (3 * x0_idx >= t_idx + 1 && x0_idx + 2 * x1_idx == t_idx && 96 * t_idx + N0 >= 288 * x0_idx + 193 && 96 * t_idx + 96 * x0_idx >= N0 + 192 && 576 * x0_idx + N1 + 569 >= 192 * t_idx + 2 * N0 && 192 * x0_idx + N1 + 3 * ((6 * t_idx + 7 * N0 + N1 + 2) / 9) >= 66 * t_idx + 3 * N0 + 4 && 36 * t_idx + 5 * N0 + 2 >= 96 * x0_idx + 6 * ((6 * t_idx + 7 * N0 + N1 + 2) / 9)) || (t_idx >= 3 * x0_idx + 1 && 2 * x0_idx + x1_idx == t_idx && N0 >= 193 && 384 * x0_idx >= N0 + 192 && 576 * x0_idx + N1 + 569 >= 192 * t_idx + 2 * N0 && 768 * x0_idx + N1 + 3 * ((6 * t_idx + 7 * N0 + N1 + 2) / 9) >= 258 * t_idx + 3 * N0 + 4 && 132 * t_idx + 5 * N0 + 2 >= 384 * x0_idx + 6 * ((6 * t_idx + 7 * N0 + N1 + 2) / 9)) || (t_idx >= x0_idx + 3 && x0_idx >= 2 && x0_idx + x1_idx + 1 == t_idx && N0 >= 192 * x0_idx + 1 && 192 * t_idx >= N0 + N1 + 3 && 192 * x0_idx + 6 * floord(6 * t_idx + 7 * N0 + N1 + 2, 9) + 189 >= 132 * t_idx + 5 * N0) || (t_idx >= x0_idx + 3 && x0_idx >= 2 && x0_idx + x1_idx + 1 == t_idx && N0 >= 192 * x0_idx + 1 && 192 * t_idx >= N0 + N1 + 3 && 384 * x0_idx + N1 + 3 * floord(6 * t_idx + 7 * N0 + N1 + 2, 9) + 380 >= 258 * t_idx + 3 * N0 && 132 * t_idx + 5 * N0 >= 192 * x0_idx + 6 * ((6 * t_idx + 7 * N0 + N1 + 2) / 9) + 190) || (2 * x0_idx >= 1 && t_idx >= 3 * x0_idx + 3 && 2 * x0_idx + x1_idx + 1 == t_idx && N0 >= 7 && 576 * x0_idx + N1 + 569 >= 192 * t_idx + 2 * N0 && 768 * x0_idx + N1 + 3 * ((6 * t_idx + 7 * N0 + N1 + 2) / 9) + 380 >= 258 * t_idx + 3 * N0 && 132 * t_idx + 5 * N0 >= 384 * x0_idx + 6 * ((6 * t_idx + 7 * N0 + N1 + 2) / 9) + 190) || (t_idx >= x0_idx + 2 && 3 * x0_idx >= t_idx && x0_idx + 2 * x1_idx + 2 == t_idx && N1 >= 7 && 576 * x0_idx + N1 + 569 >= 192 * t_idx + 2 * N0 && 96 * t_idx + N0 >= 288 * x0_idx + 2 * N1 + 5 && ((6 * t_idx + 7 * N0 + N1 + 2) % 9) + 6 >= N1) || (3 * x0_idx >= t_idx + 1 && x0_idx + 2 * x1_idx == t_idx && 96 * t_idx + N0 >= 288 * x0_idx + 193 && 96 * t_idx + 96 * x0_idx >= N0 + 192 && 576 * x0_idx + N1 + 569 >= 192 * t_idx + 2 * N0 && 288 * x0_idx + 2 * N1 >= 96 * t_idx + N0 + 5 && 66 * t_idx + 3 * N0 + 3 >= 192 * x0_idx + N1 + 3 * ((6 * t_idx + 7 * N0 + N1 + 2) / 9) && 36 * t_idx + 5 * N0 >= 96 * x0_idx + 6 * ((6 * t_idx + 7 * N0 + N1 + 2) / 9)) || (t_idx >= x0_idx + 3 && x0_idx >= 2 && x0_idx + x1_idx + 1 == t_idx && N0 >= 192 * x0_idx + 1 && 192 * t_idx >= N0 + N1 + 3 && 576 * x0_idx + 2 * N1 + 571 >= 384 * t_idx + N0 && 258 * t_idx + 3 * N0 >= 384 * x0_idx + N1 + 3 * ((6 * t_idx + 7 * N0 + N1 + 2) / 9) + 381 && 132 * t_idx + 5 * N0 >= 192 * x0_idx + 6 * ((6 * t_idx + 7 * N0 + N1 + 2) / 9) + 192) || (x0_idx + 2 >= t_idx && 3 * x0_idx >= t_idx + 1 && x0_idx + x1_idx + 1 == t_idx && N0 >= 192 * x0_idx + 1 && N1 >= 7 && 192 * t_idx >= N0 + N1 + 3 && 192 * x0_idx + 6 * ((6 * t_idx + 7 * N0 + N1 + 2) / 9) + 189 >= 132 * t_idx + 5 * N0) || (3 * x0_idx >= t_idx + 1 && x0_idx + 2 * x1_idx + 1 == t_idx && 96 * t_idx + N0 >= 288 * x0_idx + 97 && 96 * t_idx + 96 * x0_idx >= N0 + 96 && N1 >= 7 && 576 * x0_idx + N1 + 569 >= 192 * t_idx + 2 * N0 && 96 * x0_idx + 6 * ((6 * t_idx + 7 * N0 + N1 + 2) / 9) + 93 >= 36 * t_idx + 5 * N0 && ((6 * t_idx + 7 * N0 + N1 + 2) % 9) + 6 >= N1) || (x0_idx >= 1 && t_idx >= 3 * x0_idx + 3 && 2 * x0_idx + x1_idx + 1 == t_idx && N0 >= 7 && 576 * x0_idx + N1 + 569 >= 192 * t_idx + 2 * N0 && 1152 * x0_idx + 2 * N1 + 571 >= 384 * t_idx + N0 && 258 * t_idx + 3 * N0 >= 768 * x0_idx + N1 + 3 * ((6 * t_idx + 7 * N0 + N1 + 2) / 9) + 381 && 132 * t_idx + 5 * N0 >= 384 * x0_idx + 6 * ((6 * t_idx + 7 * N0 + N1 + 2) / 9) + 192) || (x0_idx >= 1 && t_idx >= x0_idx + 1 && x0_idx + x1_idx == t_idx && 192 * t_idx + N0 >= 384 * x0_idx + N1 && 192 * t_idx >= 192 * x0_idx + N1 && 576 * x0_idx + 2 * N1 + 184 >= 384 * t_idx + N0 && ((2 * N0 + 2 * N1 + 1) % 3) + 3 * ((-((2 * N0 + 2 * N1 + 1) % 3) + 4 * N0 + 2 * N1 + 4) / 6) >= 2 * N0 + N1 + 2) || (t_idx >= x0_idx + 3 && x0_idx >= 2 && x0_idx + x1_idx + 1 == t_idx && N0 >= 192 * x0_idx + 1 && 384 * t_idx + N0 >= 576 * x0_idx + 2 * N1 + 572 && 768 * x0_idx + 3 * floord(2 * N0 + 2 * N1 + 1, 3) + 759 >= 384 * t_idx + 4 * N0 && ((2 * N0 + 2 * N1 + 1) % 3) + 3 * ((-((2 * N0 + 2 * N1 + 1) % 3) + 4 * N0 + 2 * N1 + 4) / 6) >= 2 * N0 + N1 + 2) || (x0_idx >= 1 && t_idx >= 3 * x0_idx + 3 && 2 * x0_idx + x1_idx + 1 == t_idx && N0 >= 7 && 192 * t_idx >= 576 * x0_idx + N1 + 283 && 1152 * x0_idx + 3 * floord(2 * N0 + 2 * N1 + 1, 3) + 759 >= 384 * t_idx + 4 * N0 && ((2 * N0 + 2 * N1 + 1) % 3) + 3 * ((-((2 * N0 + 2 * N1 + 1) % 3) + 4 * N0 + 2 * N1 + 4) / 6) >= 2 * N0 + N1 + 2) || (x0_idx >= 1 && t_idx >= 3 * x0_idx + 3 && 2 * x0_idx + x1_idx + 1 == t_idx && 576 * x0_idx + N1 + 282 >= 192 * t_idx && 384 * t_idx + N0 >= 1152 * x0_idx + 2 * N1 + 572 && 1152 * x0_idx + 2 * N1 + 760 >= ((2 * N0 + 2 * N1 + 1) % 3) + 384 * t_idx + 2 * N0 && ((2 * N0 + 2 * N1 + 1) % 3) + 3 * ((-((2 * N0 + 2 * N1 + 1) % 3) + 4 * N0 + 2 * N1 + 4) / 6) >= 2 * N0 + N1 + 2) || (t_idx >= x0_idx + 2 && 3 * x0_idx >= t_idx && x0_idx + 2 * x1_idx + 2 == t_idx && 96 * t_idx + N0 >= 288 * x0_idx + 2 * N1 + 5 && 9 * floord(6 * t_idx + 7 * N0 + N1 + 2, 9) >= 6 * t_idx + 7 * N0 + 9 && 2 * (2 * N0 % 3) >= ((6 * t_idx + 7 * N0 + N1 + 2) % 9) + 1 && 576 * x0_idx + N1 + 569 >= 2 * (2 * N0 % 3) + 192 * t_idx + 2 * N0) || (x0_idx >= 1 && t_idx >= x0_idx + 1 && x0_idx + x1_idx == t_idx && 192 * t_idx + N0 >= 384 * x0_idx + N1 && 192 * t_idx >= 192 * x0_idx + N1 && 576 * x0_idx + N1 + 3 * floord(2 * N0 + 3 * floord(2 * N0 + 2 * N1 + 1, 3) + 3, 6) + 182 >= 384 * t_idx + 3 * N0 && ((-((2 * N0 + 2 * N1 + 1) % 3) + 4 * N0 + 2 * N1 + 4) % 6) + 2 * N0 + 2 * N1 >= ((2 * N0 + 2 * N1 + 1) % 3) + 3 * ((2 * N0 + 2 * N1 + 1) / 3) + 2) || (3 * x0_idx >= t_idx + 1 && x0_idx + 2 * x1_idx == t_idx && 96 * t_idx + N0 >= 288 * x0_idx + 193 && 96 * t_idx + 96 * x0_idx >= N0 + 192 && 96 * t_idx + N0 + 4 >= 288 * x0_idx + 2 * N1 && 3 * floord(2 * N0 + 2 * N1 + 1, 3) >= 2 * N0 + 15 && 576 * x0_idx + 2 * N1 + 376 >= ((2 * N0 + 2 * N1 + 1) % 3) + 192 * t_idx + 2 * N0 && ((2 * N0 + 2 * N1 + 1) % 3) + 3 * ((-((2 * N0 + 2 * N1 + 1) % 3) + 4 * N0 + 2 * N1 + 4) / 6) >= 2 * N0 + N1 + 2) || (x0_idx >= 1 && t_idx >= 3 * x0_idx + 1 && 2 * x0_idx + x1_idx == t_idx && N0 >= 7 && 192 * t_idx + 5 >= 576 * x0_idx + N1 && 1152 * x0_idx + N1 + 3 * floord(2 * N0 + 3 * floord(2 * N0 + 2 * N1 + 1, 3) + 3, 6) + 182 >= 384 * t_idx + 3 * N0 && ((-((2 * N0 + 2 * N1 + 1) % 3) + 4 * N0 + 2 * N1 + 4) % 6) + 2 * N0 + 2 * N1 >= ((2 * N0 + 2 * N1 + 1) % 3) + 3 * ((2 * N0 + 2 * N1 + 1) / 3) + 2) || (x0_idx >= 1 && t_idx >= 3 * x0_idx + 1 && 2 * x0_idx + x1_idx == t_idx && N0 >= 7 && 192 * t_idx + 5 >= 576 * x0_idx + N1 && 1152 * x0_idx + 2 * N1 + 184 >= 384 * t_idx + N0 && 1152 * x0_idx + 2 * N1 + 376 >= ((2 * N0 + 2 * N1 + 1) % 3) + 384 * t_idx + 2 * N0 && ((2 * N0 + 2 * N1 + 1) % 3) + 3 * ((-((2 * N0 + 2 * N1 + 1) % 3) + 4 * N0 + 2 * N1 + 4) / 6) >= 2 * N0 + N1 + 2) || (x0_idx >= 1 && t_idx >= 3 * x0_idx + 1 && 2 * x0_idx + x1_idx == t_idx && 576 * x0_idx + N1 >= 192 * t_idx + 6 && 192 * t_idx + 9 >= 576 * x0_idx + N1 && 384 * t_idx + N0 + 4 >= 1152 * x0_idx + 2 * N1 && 1152 * x0_idx + 2 * N1 + 376 >= ((2 * N0 + 2 * N1 + 1) % 3) + 384 * t_idx + 2 * N0 && ((2 * N0 + 2 * N1 + 1) % 3) + 3 * ((-((2 * N0 + 2 * N1 + 1) % 3) + 4 * N0 + 2 * N1 + 4) / 6) >= 2 * N0 + N1 + 2) || (t_idx >= 3 * x0_idx + 1 && 2 * x0_idx + x1_idx == t_idx && N0 >= 193 && 384 * x0_idx >= N0 + 192 && 576 * x0_idx + N1 >= 192 * t_idx + 10 && 384 * t_idx + N0 + 4 >= 1152 * x0_idx + 2 * N1 && 1152 * x0_idx + 2 * N1 + 376 >= ((2 * N0 + 2 * N1 + 1) % 3) + 384 * t_idx + 2 * N0 && ((2 * N0 + 2 * N1 + 1) % 3) + 3 * ((-((2 * N0 + 2 * N1 + 1) % 3) + 4 * N0 + 2 * N1 + 4) / 6) >= 2 * N0 + N1 + 2) || (t_idx >= 3 * x0_idx + 1 && 2 * x0_idx + x1_idx == t_idx && N0 >= 193 && 384 * x0_idx >= N0 + 192 && 384 * t_idx + N0 + 571 >= 1152 * x0_idx + 2 * N1 && 384 * x0_idx + 6 * floord(6 * t_idx + 7 * N0 + N1 + 2, 9) >= 132 * t_idx + 5 * N0 + 3 && ((6 * t_idx + 7 * N0 + N1 + 2) % 9) + 2 * ((N0 - 1) % 3) <= 3 && 2 * ((N0 - 1) % 3) + 576 * x0_idx + N1 + 565 >= 192 * t_idx + 2 * N0) || (t_idx >= x0_idx + 3 && x0_idx >= 2 && x0_idx + x1_idx + 1 == t_idx && N0 >= 192 * x0_idx + 1 && 384 * t_idx + N0 >= 576 * x0_idx + 2 * N1 + 572 && 768 * x0_idx + 3 * floord(2 * N0 + 2 * N1 + 1, 3) + 759 >= 384 * t_idx + 4 * N0 && ((-((2 * N0 + 2 * N1 + 1) % 3) + 4 * N0 + 2 * N1 + 4) % 6) + 2 * N0 + 2 * N1 >= ((2 * N0 + 2 * N1 + 1) % 3) + 3 * ((2 * N0 + 2 * N1 + 1) / 3) + 2) || (x0_idx >= 1 && t_idx >= 3 * x0_idx + 3 && 2 * x0_idx + x1_idx + 1 == t_idx && N0 >= 7 && 192 * t_idx >= 576 * x0_idx + N1 + 283 && 1152 * x0_idx + 3 * floord(2 * N0 + 2 * N1 + 1, 3) + 759 >= 384 * t_idx + 4 * N0 && ((-((2 * N0 + 2 * N1 + 1) % 3) + 4 * N0 + 2 * N1 + 4) % 6) + 2 * N0 + 2 * N1 >= ((2 * N0 + 2 * N1 + 1) % 3) + 3 * ((2 * N0 + 2 * N1 + 1) / 3) + 2) || (x0_idx >= 1 && t_idx >= 3 * x0_idx + 3 && 2 * x0_idx + x1_idx + 1 == t_idx && 576 * x0_idx + N1 + 282 >= 192 * t_idx && 384 * t_idx + N0 >= 1152 * x0_idx + 2 * N1 + 572 && 1152 * x0_idx + 2 * N1 + 760 >= ((2 * N0 + 2 * N1 + 1) % 3) + 384 * t_idx + 2 * N0 && ((-((2 * N0 + 2 * N1 + 1) % 3) + 4 * N0 + 2 * N1 + 4) % 6) + 2 * N0 + 2 * N1 >= ((2 * N0 + 2 * N1 + 1) % 3) + 3 * ((2 * N0 + 2 * N1 + 1) / 3) + 2) || (t_idx >= x0_idx + 2 && 3 * x0_idx >= t_idx && x0_idx + 2 * x1_idx + 2 == t_idx && 576 * x0_idx + N1 + 569 >= 192 * t_idx + 2 * N0 && 96 * t_idx + N0 >= 288 * x0_idx + 2 * N1 + 5 && 9 * floord(6 * t_idx + 7 * N0 + N1 + 2, 9) >= 6 * t_idx + 7 * N0 + 9 && (6 * t_idx + 7 * N0 + N1 + 2) % 9 >= 2 * (2 * N0 % 3)) || (3 * x0_idx >= t_idx + 1 && x0_idx + 2 * x1_idx == t_idx && 96 * t_idx + N0 >= 288 * x0_idx + 193 && 96 * t_idx + 96 * x0_idx >= N0 + 192 && 96 * t_idx + N0 + 4 >= 288 * x0_idx + 2 * N1 && 3 * floord(2 * N0 + 2 * N1 + 1, 3) >= 2 * N0 + 15 && 576 * x0_idx + 2 * N1 + 376 >= ((2 * N0 + 2 * N1 + 1) % 3) + 192 * t_idx + 2 * N0 && ((-((2 * N0 + 2 * N1 + 1) % 3) + 4 * N0 + 2 * N1 + 4) % 6) + 2 * N0 + 2 * N1 >= ((2 * N0 + 2 * N1 + 1) % 3) + 3 * ((2 * N0 + 2 * N1 + 1) / 3) + 2) || (x0_idx >= 1 && t_idx >= 3 * x0_idx + 1 && 2 * x0_idx + x1_idx == t_idx && 576 * x0_idx + N1 >= 192 * t_idx + 6 && 192 * t_idx + 9 >= 576 * x0_idx + N1 && 384 * t_idx + N0 + 4 >= 1152 * x0_idx + 2 * N1 && 1152 * x0_idx + 2 * N1 + 376 >= ((2 * N0 + 2 * N1 + 1) % 3) + 384 * t_idx + 2 * N0 && ((-((2 * N0 + 2 * N1 + 1) % 3) + 4 * N0 + 2 * N1 + 4) % 6) + 2 * N0 + 2 * N1 >= ((2 * N0 + 2 * N1 + 1) % 3) + 3 * ((2 * N0 + 2 * N1 + 1) / 3) + 2) || (t_idx >= 3 * x0_idx + 1 && 2 * x0_idx + x1_idx == t_idx && N0 >= 193 && 384 * x0_idx >= N0 + 192 && 576 * x0_idx + N1 >= 192 * t_idx + 10 && 384 * t_idx + N0 + 4 >= 1152 * x0_idx + 2 * N1 && 1152 * x0_idx + 2 * N1 + 376 >= ((2 * N0 + 2 * N1 + 1) % 3) + 384 * t_idx + 2 * N0 && ((-((2 * N0 + 2 * N1 + 1) % 3) + 4 * N0 + 2 * N1 + 4) % 6) + 2 * N0 + 2 * N1 >= ((2 * N0 + 2 * N1 + 1) % 3) + 3 * ((2 * N0 + 2 * N1 + 1) / 3) + 2) || (t_idx >= 3 * x0_idx + 1 && 2 * x0_idx + x1_idx == t_idx && N0 >= 193 && 384 * x0_idx >= N0 + 192 && 576 * x0_idx + N1 + 569 >= 192 * t_idx + 2 * N0 && 1152 * x0_idx + 2 * N1 >= 384 * t_idx + N0 + 5 && 258 * t_idx + 3 * N0 + 3 >= 768 * x0_idx + N1 + 3 * ((6 * t_idx + 7 * N0 + N1 + 2) / 9) && 384 * x0_idx + 2 * N0 + N1 >= ((N1 + 2) % 3) + 126 * t_idx + 3 * ((6 * t_idx + 7 * N0 + N1 + 2) / 9) + 1) || (t_idx >= 3 * x0_idx + 1 && 2 * x0_idx + x1_idx == t_idx && N0 >= 193 && 384 * x0_idx >= N0 + 192 && 576 * x0_idx + N1 + 569 >= 192 * t_idx + 2 * N0 && 384 * t_idx + N0 + 571 >= 1152 * x0_idx + 2 * N1 && 384 * x0_idx + 6 * ((6 * t_idx + 7 * N0 + N1 + 2) / 9) >= 132 * t_idx + 5 * N0 + 3 && ((6 * t_idx + 7 * N0 + N1 + 2) % 9) + 2 * ((N0 - 1) % 3) >= 4) || (t_idx >= 3 * x0_idx + 1 && 2 * x0_idx + x1_idx == t_idx && N0 >= 193 && 384 * x0_idx >= N0 + 192 && N0 <= 570 && 1152 * x0_idx + 2 * N1 >= 384 * t_idx + N0 + 572 && 2 * ((N0 - 1) % 3) + 576 * x0_idx + 7 * N0 + N1 >= 192 * t_idx + 9 * (5 * N0 / 6) + 290) || (t_idx >= x0_idx + 2 && 3 * x0_idx >= t_idx && x0_idx + 2 * x1_idx + 2 == t_idx && 96 * t_idx + N0 >= 288 * x0_idx + 19 && 288 * x0_idx + 378 >= 96 * t_idx + N0 && 288 * x0_idx + 2 * N1 + 4 >= 96 * t_idx + N0 && 48 * t_idx + 9 * (5 * N0 / 6) >= 144 * x0_idx + 7 * N0 + 9 && 144 * x0_idx + 7 * N0 + N1 + 2 >= 2 * (2 * N0 % 3) + 48 * t_idx + 9 * (5 * N0 / 6)) || (t_idx >= 1 && x0_idx == 0 && x1_idx == t_idx && N0 <= 6 && N1 >= 192 * t_idx + 1) || (t_idx >= 3 && 3 * x0_idx == t_idx && 3 * x1_idx == t_idx && N0 <= 6 && N1 >= 10) || (t_idx >= 1 && x0_idx == t_idx && x1_idx == 0 && 192 * t_idx >= N0 && N1 >= 7) || (t_idx >= 3 && x0_idx == 0 && x1_idx + 1 == t_idx && N0 <= 6 && N1 + 8 >= 192 * t_idx) || (t_idx >= 2 && 3 * x0_idx + 2 == t_idx && 3 * x1_idx + 2 == t_idx && N0 <= 6 && N1 >= 97) || (2 * t_idx >= 7 && 3 * x0_idx + 2 == t_idx && 3 * x1_idx == t_idx + 1 && N0 <= 6 && N1 >= 10 && N1 <= 101) || (t_idx >= 1 && x0_idx == 0 && x1_idx == t_idx && N0 <= 6 && 192 * t_idx >= N1 && N1 + 89 >= 192 * t_idx) || (t_idx >= 1 && x0_idx == 0 && x1_idx == t_idx && N0 >= 7 && N0 <= 186 && N1 >= 192 * t_idx + 1) || (t_idx >= 3 && 3 * x0_idx == t_idx && 3 * x1_idx == t_idx && N0 <= 6 && N1 >= 7 && N1 <= 9) || (t_idx >= 3 && 3 * x0_idx == t_idx && 3 * x1_idx == t_idx && N0 >= 7 && N0 <= 192 && N1 >= 10) || (t_idx >= 1 && x0_idx == t_idx && x1_idx == 0 && N0 >= 192 * t_idx + 1 && 192 * t_idx + 180 >= N0 && N1 >= 7) || (t_idx >= 3 && x0_idx == 0 && x1_idx + 1 == t_idx && N0 <= 6 && 192 * t_idx >= N1 + 9 && N1 + 282 >= 192 * t_idx) || (t_idx >= 3 && x0_idx == 0 && x1_idx + 1 == t_idx && N0 <= 6 && 192 * t_idx >= N1 + 283 && N1 + 374 >= 192 * t_idx) || (t_idx >= 3 && x0_idx == 0 && x1_idx + 1 == t_idx && N0 >= 7 && N0 <= 189 && N1 + 8 >= 192 * t_idx) || (t_idx >= 3 && x0_idx == 0 && x1_idx + 1 == t_idx && N0 <= 189 && 192 * t_idx >= N1 + 9 && N0 + N1 + 1 >= 192 * t_idx) || (t_idx >= 1 && t_idx <= 2 && x0_idx == 0 && x1_idx + 1 == t_idx && N0 <= 6 && N1 + 8 >= 192 * t_idx) || (t_idx >= 4 && x0_idx == 1 && x1_idx + 2 == t_idx && N0 >= 193 && N0 <= 381 && N0 + N1 + 2 >= 192 * t_idx) || (t_idx >= 2 && 3 * x0_idx + 2 == t_idx && 3 * x1_idx + 2 == t_idx && N0 <= 6 && N1 >= 7 && N1 <= 96) || (t_idx >= 3 && 3 * x0_idx == t_idx && 3 * x1_idx == t_idx && N0 >= 7 && N1 >= 7 && N1 <= 9 && 2 * N1 >= N0 + 5) || (t_idx >= 1 && t_idx <= 2 && x0_idx == 0 && x1_idx + 1 == t_idx && N0 >= 7 && N0 <= 189 && N1 + 8 >= 192 * t_idx) || (t_idx <= 2 && x0_idx == 0 && x1_idx + 1 == t_idx && N0 <= 6 && 192 * t_idx >= N1 + 9 && N1 >= 7 && N1 + 282 >= 192 * t_idx) || (t_idx <= 2 && x0_idx == 0 && x1_idx + 1 == t_idx && N0 <= 189 && 192 * t_idx >= N1 + 9 && N1 >= 7 && N0 + N1 + 1 >= 192 * t_idx) || (2 * x0_idx + x1_idx >= t_idx + 1 && x0_idx + 2 * x1_idx >= t_idx + 1 && 192 * t_idx + N0 >= 384 * x0_idx + 192 * x1_idx + 193 && 192 * t_idx >= 192 * x1_idx + N0 + 192 && 384 * x0_idx + 192 * x1_idx + 567 >= 192 * t_idx + N0 && 192 * t_idx + 2 * N1 == 576 * x1_idx + N0 + 572 && (192 * t_idx - 576 * x1_idx - N0 - 572) % 6 == 0) || (t_idx >= x1_idx + 2 && t_idx >= 2 * x0_idx + x1_idx + 1 && x0_idx + 2 * x1_idx >= t_idx + 1 && N0 >= 7 && 384 * x0_idx + 192 * x1_idx + 567 >= 192 * t_idx + N0 && 192 * t_idx + 2 * N1 == 576 * x1_idx + N0 + 572 && (192 * t_idx - 576 * x1_idx - N0 - 572) % 6 == 0) || (2 * x0_idx + x1_idx >= t_idx + 1 && x0_idx + 2 * x1_idx >= t_idx + 1 && 192 * t_idx + N0 >= 384 * x0_idx + 192 * x1_idx + 193 && 192 * t_idx >= 192 * x1_idx + N0 + 192 && 384 * x0_idx + 192 * x1_idx + 377 >= 192 * t_idx + N0 && 192 * t_idx + 2 * N1 == 576 * x1_idx + N0 + 5 && (192 * t_idx - 576 * x1_idx - N0 - 5) % 6 == 0) || (3 * x0_idx >= t_idx + 1 && t_idx >= x0_idx + 2 * x1_idx && x0_idx + 2 * x1_idx + 1 >= t_idx && 192 * t_idx + N0 >= 384 * x0_idx + 192 * x1_idx + 193 && 192 * t_idx >= 192 * x1_idx + N0 + 192 && 384 * x0_idx + 192 * x1_idx + 567 >= 192 * t_idx + N0 && 192 * t_idx + 2 * N1 == 576 * x1_idx + N0 + 572 && (192 * t_idx - 576 * x1_idx - N0 - 572) % 6 == 0) || (t_idx >= x1_idx + 2 && t_idx >= 2 * x0_idx + x1_idx + 1 && t_idx >= x0_idx + 2 * x1_idx && x0_idx + 2 * x1_idx + 1 >= t_idx && N0 >= 7 && 384 * x0_idx + 192 * x1_idx + 567 >= 192 * t_idx + N0 && 192 * t_idx + 2 * N1 == 576 * x1_idx + N0 + 572 && (192 * t_idx - 576 * x1_idx - N0 - 572) % 6 == 0) || (3 * x0_idx >= t_idx + 1 && x0_idx + 2 * x1_idx == t_idx && 96 * t_idx + N0 >= 288 * x0_idx + 193 && 96 * t_idx + 96 * x0_idx >= N0 + 192 && N1 == 7 && (2 * N0 + 15) % 3 >= 1 && 576 * x0_idx + 390 >= ((2 * N0 + 15) % 3) + 192 * t_idx + 2 * N0) || (2 * t_idx >= 7 && 3 * x0_idx + 2 == t_idx && 3 * x1_idx == t_idx + 1 && N0 >= 7 && N1 + 185 >= 2 * N0 && N1 + 3 * floord(6 * t_idx + 7 * N0 + N1 + 2, 9) >= 2 * t_idx + 3 * N0 + 132 && 4 * t_idx + 5 * N0 + 66 >= 6 * ((6 * t_idx + 7 * N0 + N1 + 2) / 9)) || (2 * t_idx >= 7 && x0_idx + 2 == t_idx && x1_idx == 1 && N0 + 383 >= 192 * t_idx && 192 * t_idx >= N0 + N1 + 3 && 126 * t_idx + N1 + 3 * floord(6 * t_idx + 7 * N0 + N1 + 2, 9) >= 3 * N0 + 388 && 5 * N0 + 194 >= 60 * t_idx + 6 * ((6 * t_idx + 7 * N0 + N1 + 2) / 9)) || (3 * x0_idx == t_idx && 3 * x1_idx == t_idx && N0 >= 193 && 128 * t_idx >= N0 + 192 && N1 + 569 >= 2 * N0 && N1 + 3 * ((6 * t_idx + 7 * N0 + N1 + 2) / 9) >= 2 * t_idx + 3 * N0 + 4 && 4 * t_idx + 5 * N0 + 2 >= 6 * ((6 * t_idx + 7 * N0 + N1 + 2) / 9)) || (t_idx >= 3 && x0_idx == 0 && x1_idx + 1 == t_idx && N0 >= 7 && 192 * t_idx >= N0 + N1 + 2 && 6 * floord(6 * t_idx + 7 * N0 + N1 + 2, 9) + 189 >= 132 * t_idx + 5 * N0) || (t_idx >= 3 && x0_idx == 0 && x1_idx + 1 == t_idx && N0 >= 7 && 192 * t_idx >= N0 + N1 + 2 && N1 + 3 * floord(6 * t_idx + 7 * N0 + N1 + 2, 9) + 380 >= 258 * t_idx + 3 * N0 && 132 * t_idx + 5 * N0 >= 6 * ((6 * t_idx + 7 * N0 + N1 + 2) / 9) + 190) || (t_idx >= 4 && x0_idx == 1 && x1_idx + 2 == t_idx && N0 >= 193 && 192 * t_idx >= N0 + N1 + 3 && 6 * floord(6 * t_idx + 7 * N0 + N1 + 2, 9) + 381 >= 132 * t_idx + 5 * N0) || (t_idx >= 4 && x0_idx == 1 && x1_idx + 2 == t_idx && N0 >= 193 && 192 * t_idx >= N0 + N1 + 3 && N1 + 3 * floord(6 * t_idx + 7 * N0 + N1 + 2, 9) + 764 >= 258 * t_idx + 3 * N0 && 132 * t_idx + 5 * N0 >= 6 * ((6 * t_idx + 7 * N0 + N1 + 2) / 9) + 382) || (t_idx >= 2 && 3 * x0_idx + 2 == t_idx && 3 * x1_idx + 2 == t_idx && N0 >= 7 && N1 >= 7 && N1 + 185 >= 2 * N0 && ((6 * t_idx + 7 * N0 + N1 + 2) % 9) + 6 >= N1) || (2 * x0_idx + x1_idx >= t_idx + 1 && x0_idx + 2 * x1_idx >= t_idx + 1 && 192 * t_idx + N0 >= 384 * x0_idx + 192 * x1_idx + 193 && 192 * t_idx >= 192 * x1_idx + N0 + 192 && 192 * x0_idx + N1 + 186 >= 192 * x1_idx + N0 && 576 * x1_idx + N0 + 4 >= 192 * t_idx + 2 * N1 && (N0 - 1) % 3 == 0 && N1 % 3 == 0) || (2 * x0_idx + x1_idx >= t_idx + 1 && t_idx >= x0_idx + x1_idx + 1 && x0_idx + 2 * x1_idx >= t_idx + 1 && 192 * x1_idx + N0 >= 192 * x0_idx + N1 && 192 * x0_idx + 384 * x1_idx + 3 >= 192 * t_idx + N1 && 192 * t_idx + 2 * N1 + 180 >= 576 * x1_idx + N0 && (N0 - 1) % 3 == 0 && N1 % 3 == 0) || (t_idx >= 3 && 3 * x0_idx == t_idx && 3 * x1_idx == t_idx && N0 + 4 >= 2 * N1 && 3 * floord(2 * N0 + 18, 3) + 1 >= 2 * N0 + 2 * N1 && 2 * N0 + 2 * N1 + 1 >= 3 * floord(2 * N0 + 18, 3) && ((2 * N0 + 18) % 3) + 2 * N0 <= 393) || (t_idx <= 2 && x0_idx == 0 && x1_idx + 1 == t_idx && N0 >= 7 && N1 >= 7 && 192 * t_idx >= N0 + N1 + 2 && 6 * ((6 * t_idx + 7 * N0 + N1 + 2) / 9) + 189 >= 132 * t_idx + 5 * N0) || (2 * t_idx >= 5 && 3 * x0_idx + 1 == t_idx && 3 * x1_idx + 1 == t_idx && N0 >= 7 && N1 >= 7 && N1 + 377 >= 2 * N0 && 6 * ((6 * t_idx + 7 * N0 + N1 + 2) / 9) + 61 >= 4 * t_idx + 5 * N0 && ((6 * t_idx + 7 * N0 + N1 + 2) % 9) + 6 >= N1) || (t_idx >= 4 && 3 * x0_idx + 2 == t_idx && 3 * x1_idx == t_idx + 1 && N1 >= 102 && N0 + 196 >= 2 * N1 && ((N0 - 2 * N1 + 196) % 3) + 2 * N1 >= 2 * N0 + 10 && 3 * ((((N0 - 2 * N1 + 196) % 3) + 4 * N0 + 2 * N1 + 2) / 6) >= ((N0 - 2 * N1 + 196) % 3) + 2 * N0 + N1) || (t_idx >= 4 && 3 * x0_idx + 2 == t_idx && 3 * x1_idx == t_idx + 1 && N0 >= 7 && N1 <= 101 && 3 * floord(2 * N0 + 2 * N1 + 1, 3) >= 4 * N0 + 9 && ((2 * N0 + 2 * N1 + 1) % 3) + 3 * ((-((2 * N0 + 2 * N1 + 1) % 3) + 4 * N0 + 2 * N1 + 4) / 6) >= 2 * N0 + N1 + 2) || (t_idx >= 1 && x0_idx == 0 && x1_idx == t_idx && N0 >= 7 && 192 * t_idx >= N1 && 2 * N1 + 184 >= 384 * t_idx + N0 && ((2 * N0 + 2 * N1 + 1) % 3) + 3 * ((-((2 * N0 + 2 * N1 + 1) % 3) + 4 * N0 + 2 * N1 + 4) / 6) >= 2 * N0 + N1 + 2) || (t_idx >= 3 && x0_idx == 0 && x1_idx + 1 == t_idx && N0 >= 7 && 192 * t_idx >= N1 + 283 && 3 * floord(2 * N0 + 2 * N1 + 1, 3) + 759 >= 384 * t_idx + 4 * N0 && ((2 * N0 + 2 * N1 + 1) % 3) + 3 * ((-((2 * N0 + 2 * N1 + 1) % 3) + 4 * N0 + 2 * N1 + 4) / 6) >= 2 * N0 + N1 + 2) || (t_idx >= 3 && x0_idx == 0 && x1_idx + 1 == t_idx && N1 + 282 >= 192 * t_idx && 384 * t_idx + N0 >= 2 * N1 + 572 && 2 * N1 + 760 >= ((2 * N0 + 2 * N1 + 1) % 3) + 384 * t_idx + 2 * N0 && ((2 * N0 + 2 * N1 + 1) % 3) + 3 * ((-((2 * N0 + 2 * N1 + 1) % 3) + 4 * N0 + 2 * N1 + 4) / 6) >= 2 * N0 + N1 + 2) || (t_idx >= 2 && 3 * x0_idx + 2 == t_idx && 3 * x1_idx + 2 == t_idx && N1 >= 97 && N0 + 187 >= 2 * N1 && 2 * (2 * N0 % 3) >= ((6 * t_idx + 7 * N0 + N1 + 2) % 9) + 1 && N1 + 185 >= 2 * (2 * N0 % 3) + 2 * N0) || (t_idx >= 4 && 3 * x0_idx + 2 == t_idx && 3 * x1_idx == t_idx + 1 && N1 >= 102 && N0 + 196 >= 2 * N1 && ((N0 - 2 * N1 + 196) % 3) + 2 * N1 >= 2 * N0 + 10 && ((N0 - 2 * N1 + 196) % 3) + ((((N0 - 2 * N1 + 196) % 3) + 4 * N0 + 2 * N1 + 2) % 6) + 2 * N0 + 2 * N1 >= 3 * ((2 * N0 + 2 * N1 + 1) / 3) + 4) || (t_idx >= 4 && 3 * x0_idx + 2 == t_idx && 3 * x1_idx == t_idx + 1 && N0 >= 7 && N1 <= 101 && 3 * floord(2 * N0 + 2 * N1 + 1, 3) >= 4 * N0 + 9 && ((-((2 * N0 + 2 * N1 + 1) % 3) + 4 * N0 + 2 * N1 + 4) % 6) + 2 * N0 + 2 * N1 >= ((2 * N0 + 2 * N1 + 1) % 3) + 3 * ((2 * N0 + 2 * N1 + 1) / 3) + 2) || (t_idx >= 4 && x0_idx + 2 == t_idx && x1_idx == 1 && N0 + 383 >= 192 * t_idx && N0 + 580 >= 192 * t_idx + 2 * N1 && 384 * t_idx + 3 * floord(2 * N0 + 2 * N1 + 1, 3) >= 4 * N0 + 777 && 2 * N1 >= ((2 * N0 + 2 * N1 + 1) % 3) + 14 && ((2 * N0 + 2 * N1 + 1) % 3) + 3 * ((-((2 * N0 + 2 * N1 + 1) % 3) + 4 * N0 + 2 * N1 + 4) / 6) >= 2 * N0 + N1 + 2) || (t_idx >= 1 && x0_idx == 0 && x1_idx == t_idx && N0 >= 7 && 192 * t_idx >= N1 && N1 + 3 * floord(2 * N0 + 3 * floord(2 * N0 + 2 * N1 + 1, 3) + 3, 6) + 182 >= 384 * t_idx + 3 * N0 && ((-((2 * N0 + 2 * N1 + 1) % 3) + 4 * N0 + 2 * N1 + 4) % 6) + 2 * N0 + 2 * N1 >= ((2 * N0 + 2 * N1 + 1) % 3) + 3 * ((2 * N0 + 2 * N1 + 1) / 3) + 2) || (3 * x0_idx == t_idx && 3 * x1_idx == t_idx && N0 >= 193 && 128 * t_idx >= N0 + 192 && N1 >= 10 && N0 + 4 >= 2 * N1 && ((N0 - 2 * N1 + 4) % 3) + 2 * N1 + 374 >= 2 * N0 && 3 * ((((N0 - 2 * N1 + 4) % 3) + 4 * N0 + 2 * N1 + 2) / 6) >= ((N0 - 2 * N1 + 4) % 3) + 2 * N0 + N1) || (3 * x0_idx == t_idx && 3 * x1_idx == t_idx && N0 >= 193 && 128 * t_idx >= N0 + 192 && N0 + 571 >= 2 * N1 && 6 * floord(6 * t_idx + 7 * N0 + N1 + 2, 9) >= 4 * t_idx + 5 * N0 + 3 && ((6 * t_idx + 7 * N0 + N1 + 2) % 9) + 2 * ((N0 - 1) % 3) <= 3 && 2 * ((N0 - 1) % 3) + N1 + 565 >= 2 * N0) || (t_idx >= 3 && 3 * x0_idx == t_idx && 3 * x1_idx == t_idx && N1 <= 9 && N0 + 4 >= 2 * N1 && ((N0 - 2 * N1 + 4) % 3) + 2 * N1 >= 16 && ((N0 - 2 * N1 + 4) % 3) + 2 * N1 + 374 >= 2 * N0 && 3 * ((((N0 - 2 * N1 + 4) % 3) + 4 * N0 + 2 * N1 + 2) / 6) >= ((N0 - 2 * N1 + 4) % 3) + 2 * N0 + N1) || (t_idx >= 3 && x0_idx == 0 && x1_idx + 1 == t_idx && N0 >= 7 && 192 * t_idx >= N1 + 283 && 3 * floord(2 * N0 + 2 * N1 + 1, 3) + 759 >= 384 * t_idx + 4 * N0 && ((-((2 * N0 + 2 * N1 + 1) % 3) + 4 * N0 + 2 * N1 + 4) % 6) + 2 * N0 + 2 * N1 >= ((2 * N0 + 2 * N1 + 1) % 3) + 3 * ((2 * N0 + 2 * N1 + 1) / 3) + 2) || (t_idx >= 3 && x0_idx == 0 && x1_idx + 1 == t_idx && N1 + 282 >= 192 * t_idx && 384 * t_idx + N0 >= 2 * N1 + 572 && 2 * N1 + 760 >= ((2 * N0 + 2 * N1 + 1) % 3) + 384 * t_idx + 2 * N0 && ((-((2 * N0 + 2 * N1 + 1) % 3) + 4 * N0 + 2 * N1 + 4) % 6) + 2 * N0 + 2 * N1 >= ((2 * N0 + 2 * N1 + 1) % 3) + 3 * ((2 * N0 + 2 * N1 + 1) / 3) + 2) || (t_idx >= 4 && x0_idx == 1 && x1_idx + 2 == t_idx && N0 >= 193 && N1 + 566 >= 192 * t_idx && 384 * t_idx + N0 >= 2 * N1 + 1148 && 2 * N1 + 1528 >= ((2 * N0 + 2 * N1 + 1) % 3) + 384 * t_idx + 2 * N0 && ((2 * N0 + 2 * N1 + 1) % 3) + 3 * ((-((2 * N0 + 2 * N1 + 1) % 3) + 4 * N0 + 2 * N1 + 4) / 6) >= 2 * N0 + N1 + 2) || (t_idx >= 2 && 3 * x0_idx + 2 == t_idx && 3 * x1_idx + 2 == t_idx && N0 >= 7 && N1 <= 96 && 9 * floord(6 * t_idx + 7 * N0 + N1 + 2, 9) >= 6 * t_idx + 7 * N0 + 9 && ((6 * t_idx + 7 * N0 + N1 + 2) % 9) + 2 * ((N0 - 1) % 3) <= 3 && 2 * ((N0 - 1) % 3) + N1 + 181 >= 2 * N0) || (t_idx >= 2 && 3 * x0_idx + 2 == t_idx && 3 * x1_idx + 2 == t_idx && N1 >= 97 && N1 + 185 >= 2 * N0 && N0 + 187 >= 2 * N1 && (6 * t_idx + 7 * N0 + N1 + 2) % 9 >= 2 * (2 * N0 % 3)) || (2 * t_idx >= 7 && x0_idx + 2 == t_idx && x1_idx == 1 && N0 + 383 >= 192 * t_idx && 192 * t_idx >= N0 + N1 + 3 && 192 * t_idx + 2 * N1 >= N0 + 581 && 3 * N0 + 387 >= 126 * t_idx + N1 + 3 * ((6 * t_idx + 7 * N0 + N1 + 2) / 9) && 66 * t_idx + 2 * N0 + N1 >= ((N1 + 2) % 3) + 3 * ((6 * t_idx + 7 * N0 + N1 + 2) / 9) + 193) || (t_idx >= 4 && x0_idx + 2 == t_idx && x1_idx == 1 && N0 + 383 >= 192 * t_idx && N0 + 580 >= 192 * t_idx + 2 * N1 && 384 * t_idx + 3 * floord(2 * N0 + 2 * N1 + 1, 3) >= 4 * N0 + 777 && 2 * N1 >= ((2 * N0 + 2 * N1 + 1) % 3) + 14 && ((-((2 * N0 + 2 * N1 + 1) % 3) + 4 * N0 + 2 * N1 + 4) % 6) + 2 * N0 + 2 * N1 >= ((2 * N0 + 2 * N1 + 1) % 3) + 3 * ((2 * N0 + 2 * N1 + 1) / 3) + 2) || (3 * x0_idx == t_idx && 3 * x1_idx == t_idx && N0 >= 193 && 128 * t_idx >= N0 + 192 && N1 >= 10 && N0 + 4 >= 2 * N1 && ((N0 - 2 * N1 + 4) % 3) + 2 * N1 + 374 >= 2 * N0 && ((N0 - 2 * N1 + 4) % 3) + ((((N0 - 2 * N1 + 4) % 3) + 4 * N0 + 2 * N1 + 2) % 6) + 2 * N0 + 2 * N1 >= 3 * ((2 * N0 + 2 * N1 + 1) / 3) + 4) || (3 * x0_idx == t_idx && 3 * x1_idx == t_idx && N0 >= 193 && 128 * t_idx >= N0 + 192 && N1 + 569 >= 2 * N0 && N0 + 571 >= 2 * N1 && 6 * ((6 * t_idx + 7 * N0 + N1 + 2) / 9) >= 4 * t_idx + 5 * N0 + 3 && ((6 * t_idx + 7 * N0 + N1 + 2) % 9) + 2 * ((N0 - 1) % 3) >= 4) || (3 * x0_idx == t_idx && 3 * x1_idx == t_idx && N0 >= 193 && 128 * t_idx >= N0 + 192 && N0 <= 570 && 2 * N1 >= N0 + 572 && 2 * ((N0 - 1) % 3) + 7 * N0 + N1 >= 9 * (5 * N0 / 6) + 290) || (t_idx >= 3 && x0_idx == 0 && x1_idx + 1 == t_idx && N0 >= 7 && 192 * t_idx >= N0 + N1 + 2 && 2 * N1 + 571 >= 384 * t_idx + N0 && 258 * t_idx + 3 * N0 >= N1 + 3 * ((6 * t_idx + 7 * N0 + N1 + 2) / 9) + 381 && 2 * N0 + N1 + 191 >= ((N1 + 2) % 3) + 126 * t_idx + 3 * ((6 * t_idx + 7 * N0 + N1 + 2) / 9)) || (t_idx >= 4 && x0_idx == 1 && x1_idx + 2 == t_idx && N0 >= 193 && N1 + 566 >= 192 * t_idx && 384 * t_idx + N0 >= 2 * N1 + 1148 && 2 * N1 + 1528 >= ((2 * N0 + 2 * N1 + 1) % 3) + 384 * t_idx + 2 * N0 && ((-((2 * N0 + 2 * N1 + 1) % 3) + 4 * N0 + 2 * N1 + 4) % 6) + 2 * N0 + 2 * N1 >= ((2 * N0 + 2 * N1 + 1) % 3) + 3 * ((2 * N0 + 2 * N1 + 1) / 3) + 2) || (t_idx >= 4 && x0_idx == 1 && x1_idx + 2 == t_idx && N0 >= 193 && 192 * t_idx >= N0 + N1 + 3 && 2 * N1 + 1147 >= 384 * t_idx + N0 && 258 * t_idx + 3 * N0 >= N1 + 3 * ((6 * t_idx + 7 * N0 + N1 + 2) / 9) + 765 && 2 * N0 + N1 + 383 >= ((N1 + 2) % 3) + 126 * t_idx + 3 * ((6 * t_idx + 7 * N0 + N1 + 2) / 9)) || (t_idx >= 2 && 3 * x0_idx + 2 == t_idx && 3 * x1_idx + 2 == t_idx && N0 >= 7 && N1 <= 96 && N1 + 185 >= 2 * N0 && 9 * floord(6 * t_idx + 7 * N0 + N1 + 2, 9) >= 6 * t_idx + 7 * N0 + 9 && ((6 * t_idx + 7 * N0 + N1 + 2) % 9) + 2 * ((N0 - 1) % 3) >= 4) || (t_idx >= 2 && 3 * x0_idx + 2 == t_idx && 3 * x1_idx + 2 == t_idx && N0 >= 7 && N0 <= 186 && 2 * N1 >= N0 + 188 && 2 * ((N0 - 1) % 3) + 7 * N0 + N1 >= 9 * (5 * N0 / 6) + 98) || (t_idx >= x0_idx + 2 && 3 * x0_idx >= t_idx + 1 && x0_idx + 2 * x1_idx + 1 == t_idx && 96 * t_idx + N0 == 288 * x0_idx + 284 && N1 == 7) || (t_idx == 0 && x0_idx == 0 && x1_idx == 0 && N0 <= 6 && N1 >= 7) || (t_idx == 3 && x0_idx == 1 && x1_idx == 1 && N0 >= 193 && N0 <= 381 && N0 + N1 >= 574) || (t_idx == 2 && x0_idx == 0 && x1_idx == 1 && N0 <= 6 && N1 >= 10 && N1 <= 101) || (t_idx == 0 && x0_idx == 0 && x1_idx == 0 && N0 >= 7 && N0 <= 180 && N1 >= 7) || (t_idx >= 3 * x0_idx + 1 && 2 * x0_idx + x1_idx == t_idx && N0 >= 193 && 384 * x0_idx >= N0 + 192 && N0 <= 567 && 1152 * x0_idx + 2 * N1 == 384 * t_idx + N0 + 572 && (-384 * t_idx + 1152 * x0_idx - N0 - 572) % 6 == 0) || (t_idx >= 3 * x0_idx + 1 && 2 * x0_idx + x1_idx == t_idx && N0 >= 193 && 384 * x0_idx >= N0 + 192 && N0 <= 377 && 1152 * x0_idx + 2 * N1 == 384 * t_idx + N0 + 5 && (-384 * t_idx + 1152 * x0_idx - N0 - 5) % 6 == 0) || (3 * x0_idx >= t_idx + 1 && x0_idx + 2 * x1_idx == t_idx && 96 * t_idx + N0 >= 288 * x0_idx + 193 && 96 * t_idx + 96 * x0_idx >= N0 + 192 && 288 * x0_idx + 377 >= 96 * t_idx + N0 && 288 * x0_idx + 2 * N1 == 96 * t_idx + N0 + 5 && (-96 * t_idx + 288 * x0_idx - N0 - 5) % 6 == 0) || (t_idx >= x0_idx + 2 && 3 * x0_idx >= t_idx && x0_idx + 2 * x1_idx + 2 == t_idx && 96 * t_idx + N0 >= 288 * x0_idx + 24 && 288 * x0_idx + 375 >= 96 * t_idx + N0 && 288 * x0_idx + 2 * N1 + 4 == 96 * t_idx + N0 && (-96 * t_idx + 288 * x0_idx - N0 + 4) % 6 == 0) || (t_idx >= x0_idx + 3 && x0_idx >= 2 && x0_idx + x1_idx + 1 == t_idx && N0 >= 192 * x0_idx + 1 && 192 * x0_idx + 185 >= N0 && 576 * x0_idx + 2 * N1 + 571 == 384 * t_idx + N0 && (-384 * t_idx + 576 * x0_idx - N0 + 571) % 6 == 0) || (x0_idx >= 1 && t_idx >= 3 * x0_idx + 3 && 2 * x0_idx + x1_idx + 1 == t_idx && N0 >= 7 && N0 <= 185 && 1152 * x0_idx + 2 * N1 + 571 == 384 * t_idx + N0 && (-384 * t_idx + 1152 * x0_idx - N0 + 571) % 6 == 0) || (t_idx >= 4 && x0_idx + 2 == t_idx && x1_idx == 1 && N0 + 383 >= 192 * t_idx && N1 == 7 && 384 * t_idx >= ((2 * N0 + 15) % 3) + 2 * N0 + 762 && (2 * N0 + 15) % 3 >= 1) || (t_idx >= 3 && 3 * x0_idx == t_idx && 3 * x1_idx == t_idx && N0 >= 10 && N1 == 7 && (N0 - 1) % 3 <= 1 && ((N0 - 1) % 3) + 388 >= 2 * N0) || (t_idx == 3 && x0_idx == 1 && x1_idx == 1 && N0 >= 193 && N0 + N1 <= 573 && 6 * floord(7 * N0 + N1 + 20, 9) >= 5 * N0 + 15) || (t_idx == 3 && x0_idx == 1 && x1_idx == 1 && N0 >= 193 && N0 + N1 <= 573 && N1 + 3 * floord(7 * N0 + N1 + 20, 9) >= 3 * N0 + 10 && 5 * N0 + 14 >= 6 * ((7 * N0 + N1 + 20) / 9)) || (t_idx == 2 && x0_idx == 0 && x1_idx == 1 && N0 >= 7 && N0 + N1 <= 382 && N1 + 3 * floord(7 * N0 + N1 + 14, 9) >= 3 * N0 + 136 && 5 * N0 + 74 >= 6 * ((7 * N0 + N1 + 14) / 9)) || (x0_idx >= 1 && t_idx >= x0_idx + 1 && x0_idx + x1_idx == t_idx && 192 * t_idx + N0 >= 384 * x0_idx + N1 && 192 * t_idx >= 192 * x0_idx + N1 && 576 * x0_idx + 2 * N1 + 180 >= 384 * t_idx + N0 && (N0 - 1) % 3 == 0 && N1 % 3 == 0) || (3 * x0_idx >= t_idx + 1 && x0_idx + 2 * x1_idx == t_idx && 96 * t_idx + N0 >= 288 * x0_idx + 193 && 96 * t_idx + 96 * x0_idx >= N0 + 192 && 288 * x0_idx + N1 + 186 >= 96 * t_idx + N0 && 96 * t_idx + N0 + 4 >= 288 * x0_idx + 2 * N1 && (N0 - 1) % 3 == 0 && N1 % 3 == 0) || (x0_idx >= 1 && t_idx >= 3 * x0_idx + 1 && 2 * x0_idx + x1_idx == t_idx && N0 >= 7 && 192 * t_idx + 5 >= 576 * x0_idx + N1 && 1152 * x0_idx + 2 * N1 + 180 >= 384 * t_idx + N0 && (N0 - 1) % 3 == 0 && N1 % 3 == 0) || (t_idx >= x0_idx + 3 && x0_idx >= 2 && x0_idx + x1_idx + 1 == t_idx && N0 >= 192 * x0_idx + 1 && 384 * x0_idx + N1 + 378 >= 192 * t_idx + N0 && 384 * t_idx + N0 >= 576 * x0_idx + 2 * N1 + 572 && (N0 - 1) % 3 == 0 && N1 % 3 == 0) || (x0_idx >= 1 && t_idx >= 3 * x0_idx + 3 && 2 * x0_idx + x1_idx + 1 == t_idx && N0 >= 7 && 192 * t_idx >= 576 * x0_idx + N1 + 283 && 576 * x0_idx + N1 + 378 >= 192 * t_idx + N0 && (N0 - 1) % 3 == 0 && N1 % 3 == 0) || (x0_idx >= 1 && t_idx >= 3 * x0_idx + 3 && 2 * x0_idx + x1_idx + 1 == t_idx && 576 * x0_idx + N1 + 282 >= 192 * t_idx && 576 * x0_idx + N1 + 378 >= 192 * t_idx + N0 && 384 * t_idx + N0 >= 1152 * x0_idx + 2 * N1 + 572 && (N0 - 1) % 3 == 0 && N1 % 3 == 0) || (t_idx == 2 && x0_idx == 0 && x1_idx == 1 && N1 >= 102 && N0 + 196 >= 2 * N1 && ((N0 - 2 * N1 + 196) % 3) + 2 * N1 >= 2 * N0 + 10 && 3 * ((((N0 - 2 * N1 + 196) % 3) + 4 * N0 + 2 * N1 + 2) / 6) >= ((N0 - 2 * N1 + 196) % 3) + 2 * N0 + N1) || (t_idx == 2 && x0_idx == 0 && x1_idx == 1 && N0 >= 7 && N1 <= 101 && 3 * floord(2 * N0 + 2 * N1 + 1, 3) >= 4 * N0 + 9 && ((2 * N0 + 2 * N1 + 1) % 3) + 3 * ((-((2 * N0 + 2 * N1 + 1) % 3) + 4 * N0 + 2 * N1 + 4) / 6) >= 2 * N0 + N1 + 2) || (x0_idx >= 1 && t_idx >= 3 * x0_idx + 1 && 2 * x0_idx + x1_idx == t_idx && 576 * x0_idx + N1 >= 192 * t_idx + 6 && 192 * t_idx + 9 >= 576 * x0_idx + N1 && 576 * x0_idx + N1 + 186 >= 192 * t_idx + N0 && 384 * t_idx + N0 + 4 >= 1152 * x0_idx + 2 * N1 && (N0 - 1) % 3 == 0 && N1 % 3 == 0) || (t_idx >= 3 * x0_idx + 1 && 2 * x0_idx + x1_idx == t_idx && N0 >= 193 && 384 * x0_idx >= N0 + 192 && 576 * x0_idx + N1 >= 192 * t_idx + 10 && 576 * x0_idx + N1 + 186 >= 192 * t_idx + N0 && 384 * t_idx + N0 + 4 >= 1152 * x0_idx + 2 * N1 && (N0 - 1) % 3 == 0 && N1 % 3 == 0) || (t_idx >= 4 && 3 * x0_idx + 2 == t_idx && 3 * x1_idx == t_idx + 1 && N0 >= 7 && N1 + 185 >= 2 * N0 && 2 * N1 >= N0 + 197 && 2 * t_idx + 3 * N0 + 131 >= N1 + 3 * ((6 * t_idx + 7 * N0 + N1 + 2) / 9) && 4 * t_idx + 5 * N0 + 64 >= 6 * ((6 * t_idx + 7 * N0 + N1 + 2) / 9) && N1 + 3 * ((6 * t_idx + 7 * N0 + N1 + 2) / 9) == ((N1 + 2) % 3) + 2 * t_idx + 3 * N0 + 129) || (3 * x0_idx == t_idx && 3 * x1_idx == t_idx && N0 >= 193 && 128 * t_idx >= N0 + 192 && N1 + 569 >= 2 * N0 && 2 * N1 >= N0 + 5 && 2 * t_idx + 3 * N0 + 3 >= N1 + 3 * ((6 * t_idx + 7 * N0 + N1 + 2) / 9) && 4 * t_idx + 5 * N0 >= 6 * ((6 * t_idx + 7 * N0 + N1 + 2) / 9) && N1 + 3 * ((6 * t_idx + 7 * N0 + N1 + 2) / 9) == ((N1 + 2) % 3) + 2 * t_idx + 3 * N0 + 1) || (t_idx == 3 && x0_idx == 1 && x1_idx == 1 && N0 >= 193 && N1 >= 10 && N0 + 4 >= 2 * N1 && ((N0 - 2 * N1 + 4) % 3) + 2 * N1 + 374 >= 2 * N0 && 3 * ((((N0 - 2 * N1 + 4) % 3) + 4 * N0 + 2 * N1 + 2) / 6) >= ((N0 - 2 * N1 + 4) % 3) + 2 * N0 + N1) || (t_idx == 2 && x0_idx == 0 && x1_idx == 1 && N1 >= 102 && N0 + 196 >= 2 * N1 && ((N0 - 2 * N1 + 196) % 3) + 2 * N1 >= 2 * N0 + 10 && ((N0 - 2 * N1 + 196) % 3) + ((((N0 - 2 * N1 + 196) % 3) + 4 * N0 + 2 * N1 + 2) % 6) + 2 * N0 + 2 * N1 >= 3 * ((2 * N0 + 2 * N1 + 1) / 3) + 4) || (t_idx == 2 && x0_idx == 0 && x1_idx == 1 && N0 >= 7 && N1 <= 101 && 3 * floord(2 * N0 + 2 * N1 + 1, 3) >= 4 * N0 + 9 && ((-((2 * N0 + 2 * N1 + 1) % 3) + 4 * N0 + 2 * N1 + 4) % 6) + 2 * N0 + 2 * N1 >= ((2 * N0 + 2 * N1 + 1) % 3) + 3 * ((2 * N0 + 2 * N1 + 1) / 3) + 2) || (t_idx == 3 && x0_idx == 1 && x1_idx == 1 && N0 >= 193 && N1 >= 10 && N0 + 4 >= 2 * N1 && ((N0 - 2 * N1 + 4) % 3) + 2 * N1 + 374 >= 2 * N0 && ((N0 - 2 * N1 + 4) % 3) + ((((N0 - 2 * N1 + 4) % 3) + 4 * N0 + 2 * N1 + 2) % 6) + 2 * N0 + 2 * N1 >= 3 * ((2 * N0 + 2 * N1 + 1) / 3) + 4) || (t_idx == 3 && x0_idx == 1 && x1_idx == 1 && N0 >= 193 && N0 + N1 <= 573 && 2 * N1 >= N0 + 5 && 3 * N0 + 9 >= N1 + 3 * ((7 * N0 + N1 + 20) / 9) && 2 * N0 + N1 + 5 >= ((N1 + 2) % 3) + 3 * ((7 * N0 + N1 + 20) / 9)) || (t_idx == 2 && x0_idx == 0 && x1_idx == 1 && N0 >= 7 && N0 + N1 <= 382 && 2 * N1 >= N0 + 197 && 3 * N0 + 135 >= N1 + 3 * ((7 * N0 + N1 + 14) / 9) && 2 * N0 + N1 >= ((N1 + 2) % 3) + 3 * ((7 * N0 + N1 + 14) / 9) + 61) || (t_idx >= 3 && 3 * x0_idx + 1 == t_idx && 3 * x1_idx + 1 == t_idx && N0 == 188 && N1 == 7) || (t_idx >= 4 && x0_idx + 2 == t_idx && x1_idx == 1 && 192 * t_idx >= N0 + 199 && N0 + 383 >= 192 * t_idx && 192 * t_idx + 2 * N1 == N0 + 581 && (192 * t_idx - N0 - 581) % 6 == 0) || (3 * x0_idx == t_idx && 3 * x1_idx == t_idx && N0 >= 193 && 128 * t_idx >= N0 + 192 && N0 <= 567 && 2 * N1 == N0 + 572 && (N0 + 572) % 6 == 0) || (t_idx >= 4 && 3 * x0_idx + 2 == t_idx && 3 * x1_idx == t_idx + 1 && N0 >= 7 && N0 <= 185 && 2 * N1 == N0 + 197 && (N0 + 197) % 6 == 0) || (t_idx >= 2 && 3 * x0_idx + 2 == t_idx && 3 * x1_idx + 2 == t_idx && N0 >= 7 && N0 <= 183 && 2 * N1 == N0 + 188 && (N0 + 188) % 6 == 0) || (3 * x0_idx == t_idx && 3 * x1_idx == t_idx && N0 >= 193 && 128 * t_idx >= N0 + 192 && N0 <= 377 && 2 * N1 == N0 + 5 && (N0 + 5) % 6 == 0) || (t_idx >= 3 && 3 * x0_idx == t_idx && 3 * x1_idx == t_idx && N0 >= 14 && N0 <= 195 && N1 == 9 && (N0 - 1) % 3 == 0) || (t_idx >= 3 && x0_idx == 0 && x1_idx + 1 == t_idx && N0 >= 7 && N0 <= 185 && 2 * N1 + 571 == 384 * t_idx + N0 && (384 * t_idx + N0 - 571) % 6 == 0) || (t_idx >= 4 && x0_idx == 1 && x1_idx + 2 == t_idx && N0 >= 193 && N0 <= 377 && 2 * N1 + 1147 == 384 * t_idx + N0 && (384 * t_idx + N0 - 1147) % 6 == 0) || (t_idx >= 4 && 3 * x0_idx + 2 == t_idx && 3 * x1_idx == t_idx + 1 && N0 >= 7 && N1 >= N0 + 6 && N1 <= 101 && (N0 - 1) % 3 == 0 && N1 % 3 == 0) || (t_idx >= 4 && 3 * x0_idx + 2 == t_idx && 3 * x1_idx == t_idx + 1 && N1 >= 102 && N1 >= N0 + 6 && N0 + 196 >= 2 * N1 && (N0 - 1) % 3 == 0 && N1 % 3 == 0) || (t_idx >= 4 && x0_idx + 2 == t_idx && x1_idx == 1 && N0 + 383 >= 192 * t_idx && 192 * t_idx + N1 >= N0 + 390 && N0 + 580 >= 192 * t_idx + 2 * N1 && (N0 - 1) % 3 == 0 && N1 % 3 == 0) || (t_idx >= 1 && x0_idx == 0 && x1_idx == t_idx && N0 >= 7 && 192 * t_idx >= N1 && 2 * N1 + 180 >= 384 * t_idx + N0 && (N0 - 1) % 3 == 0 && N1 % 3 == 0) || (t_idx >= 3 && x0_idx == 0 && x1_idx + 1 == t_idx && N0 >= 7 && 192 * t_idx >= N1 + 283 && N1 + 378 >= 192 * t_idx + N0 && (N0 - 1) % 3 == 0 && N1 % 3 == 0) || (t_idx >= 3 && x0_idx == 0 && x1_idx + 1 == t_idx && N1 + 282 >= 192 * t_idx && N1 + 378 >= 192 * t_idx + N0 && 384 * t_idx + N0 >= 2 * N1 + 572 && (N0 - 1) % 3 == 0 && N1 % 3 == 0) || (3 * x0_idx == t_idx && 3 * x1_idx == t_idx && N0 >= 193 && 128 * t_idx >= N0 + 192 && N1 >= 10 && N1 + 186 >= N0 && N0 + 4 >= 2 * N1 && (N0 - 1) % 3 == 0 && N1 % 3 == 0) || (t_idx >= 4 && x0_idx == 1 && x1_idx + 2 == t_idx && N0 >= 193 && N1 + 566 >= 192 * t_idx && N1 + 762 >= 192 * t_idx + N0 && 384 * t_idx + N0 >= 2 * N1 + 1148 && (N0 - 1) % 3 == 0 && N1 % 3 == 0) || (t_idx == 2 && x0_idx == 0 && x1_idx == 1 && N0 >= 7 && N0 <= 185 && 2 * N1 == N0 + 197 && (N0 + 197) % 6 == 0) || (t_idx == 3 && x0_idx == 1 && x1_idx == 1 && N0 >= 193 && N0 <= 377 && 2 * N1 == N0 + 5 && (N0 + 5) % 6 == 0) || (t_idx == 2 && x0_idx == 0 && x1_idx == 1 && N0 >= 7 && N1 >= N0 + 6 && N1 <= 101 && (N0 - 1) % 3 == 0 && N1 % 3 == 0) || (t_idx == 2 && x0_idx == 0 && x1_idx == 1 && N1 >= 102 && N1 >= N0 + 6 && N0 + 196 >= 2 * N1 && (N0 - 1) % 3 == 0 && N1 % 3 == 0) || (t_idx == 3 && x0_idx == 1 && x1_idx == 1 && N0 >= 193 && N1 >= 10 && N1 + 186 >= N0 && N0 + 4 >= 2 * N1 && (N0 - 1) % 3 == 0 && N1 % 3 == 0) || (t_idx >= 3 * x0_idx && 2 * x0_idx + x1_idx >= t_idx + 1 && T >= 5 && 192 * t_idx + 190 >= 192 * x0_idx + 192 * x1_idx + T && 192 * t_idx + N0 + 185 >= 384 * x0_idx + 192 * x1_idx && 192 * t_idx + N1 + 185 >= 192 * x0_idx + 384 * x1_idx) || (t_idx >= 3 * x0_idx && 2 * x0_idx + x1_idx >= t_idx + 1 && t_idx >= x0_idx + x1_idx && T <= 4 && 192 * t_idx + N0 + 185 >= 384 * x0_idx + 192 * x1_idx && 192 * t_idx + N1 + 185 >= 192 * x0_idx + 384 * x1_idx) || (3 * x0_idx >= t_idx + 1 && T >= 5 && 96 * t_idx >= 96 * x0_idx + T + 1 && 192 * x1_idx + N0 >= 192 * x0_idx + 8 && 288 * x0_idx + 5 >= 96 * t_idx + N0 && 192 * t_idx + N0 + 185 >= 384 * x0_idx + 192 * x1_idx && N1 >= 7) || (3 * x0_idx >= t_idx + 1 && t_idx >= x0_idx + x1_idx && x0_idx + 2 * x1_idx >= t_idx + 1 && T <= 4 && 96 * t_idx + N0 >= 288 * x0_idx + 6 && 192 * t_idx + N0 + 185 >= 384 * x0_idx + 192 * x1_idx && 192 * t_idx + N1 + 185 >= 192 * x0_idx + 384 * x1_idx) || (t_idx >= x0_idx + 1 && 3 * x0_idx >= t_idx + 1 && t_idx >= x0_idx + 2 * x1_idx && x0_idx + 2 * x1_idx + 1 >= t_idx && T <= 4 && 96 * t_idx + N0 >= 288 * x0_idx + 6 && N1 >= 7) || (t_idx >= x0_idx + 1 && 3 * x0_idx >= t_idx + 1 && T <= 4 && 192 * x1_idx + N0 >= 192 * x0_idx + 8 && 288 * x0_idx + 5 >= 96 * t_idx + N0 && 192 * t_idx + N0 + 185 >= 384 * x0_idx + 192 * x1_idx && N1 >= 7) || (3 * x0_idx >= t_idx + 1 && t_idx >= x0_idx + 2 * x1_idx && x0_idx + 2 * x1_idx + 1 >= t_idx && T >= 5 && 96 * t_idx >= 96 * x0_idx + T + 1 && 96 * t_idx + N0 >= 288 * x0_idx + 6 && N1 >= 7) || (x0_idx >= 1 && t_idx >= 2 * x0_idx + x1_idx + 1 && 2 * x0_idx + x1_idx + 2 >= t_idx && 3 * x1_idx + 2 >= t_idx && T <= 4 && N0 >= 7 && 576 * x0_idx + N1 >= 192 * t_idx + 10) || (x0_idx >= 1 && 2 * x0_idx + x1_idx + 2 >= t_idx && 3 * x1_idx + 2 >= t_idx && 96 * t_idx >= 96 * x1_idx + T + 96 && T + 1 >= 192 * x0_idx && N0 >= 7 && 3 * T + N1 >= 192 * t_idx + 4) || (x0_idx >= 1 && 2 * x0_idx + x1_idx + 2 >= t_idx && 3 * x1_idx + 2 >= t_idx && T + 1 >= 192 * x0_idx && N0 >= 7 && 96 * t_idx + N1 >= 288 * x1_idx + 290 && 192 * t_idx + 3 >= 3 * T + N1) || (x0_idx >= 1 && 2 * x0_idx + x1_idx + 2 >= t_idx && 3 * x1_idx + 2 >= t_idx && T <= 4 && N0 >= 7 && 96 * t_idx + N1 >= 288 * x1_idx + 290 && 192 * t_idx + 9 >= 576 * x0_idx + N1) || (T >= 5 && 96 * x0_idx + T >= 96 * t_idx && 192 * x1_idx + N0 >= 192 * x0_idx + 8 && N0 >= 7 && 192 * x0_idx + 4 >= T + N0 && 192 * t_idx + N0 + 185 >= 384 * x0_idx + 192 * x1_idx && N1 >= 7) || (T >= 5 && 192 * x1_idx >= T + 3 && 192 * x0_idx >= T + 2 && 96 * x0_idx + T >= 96 * t_idx && 192 * t_idx + 190 >= 192 * x0_idx + 192 * x1_idx + T && T + N0 >= 192 * x0_idx + 5 && N1 >= 7) || (2 * x0_idx + x1_idx + 2 >= t_idx && 3 * x1_idx + 2 >= t_idx && T >= 5 && 192 * x0_idx >= T + 2 && N0 >= 7 && 96 * t_idx + N1 >= 288 * x1_idx + 290 && 192 * t_idx + 9 >= 576 * x0_idx + N1) || (t_idx >= 2 * x0_idx + x1_idx + 1 && 2 * x0_idx + x1_idx + 2 >= t_idx && 3 * x1_idx + 2 >= t_idx && T >= 5 && 192 * x0_idx >= T + 2 && N0 >= 7 && 576 * x0_idx + N1 >= 192 * t_idx + 10) || (T >= 5 && 192 * x0_idx >= T + 2 && N0 >= 7 && N1 >= 7 && 288 * x1_idx + 5 >= 96 * t_idx + N1 && 192 * t_idx + 9 >= 576 * x0_idx + N1 && 96 * t_idx + N1 + 89 >= 288 * x1_idx && 192 * x0_idx + N1 + 182 >= 192 * x1_idx) || (T >= 5 && 192 * x0_idx >= T + 2 && N0 >= 7 && N1 >= 7 && 96 * t_idx + N1 >= 288 * x1_idx + 6 && 192 * t_idx + 9 >= 576 * x0_idx + N1 && 288 * x1_idx + 289 >= 96 * t_idx + N1 && 576 * x0_idx + N1 + 557 >= 192 * t_idx) || (3 * x0_idx >= t_idx + 1 && T >= 5 && 96 * t_idx >= 96 * x0_idx + T + 1 && 288 * x0_idx + 5 >= 96 * t_idx + N0 && 192 * x0_idx + 7 >= 192 * x1_idx + N0 && 96 * t_idx + N0 + 89 >= 288 * x0_idx && 192 * x1_idx + N0 + 182 >= 192 * x0_idx && N1 >= 7) || (3 * x0_idx >= t_idx + 1 && x0_idx + 2 * x1_idx >= t_idx + 1 && T >= 5 && 96 * t_idx >= 96 * x0_idx + T + 1 && 192 * t_idx + 190 >= 192 * x0_idx + 192 * x1_idx + T && 96 * t_idx + N0 >= 288 * x0_idx + 6 && 192 * t_idx + N0 + 185 >= 384 * x0_idx + 192 * x1_idx && 192 * t_idx + N1 + 185 >= 192 * x0_idx + 384 * x1_idx) || (t_idx >= x0_idx + 1 && 3 * x0_idx >= t_idx + 1 && T <= 4 && 288 * x0_idx + 5 >= 96 * t_idx + N0 && 192 * x0_idx + 7 >= 192 * x1_idx + N0 && 96 * t_idx + N0 + 89 >= 288 * x0_idx && 192 * x1_idx + N0 + 182 >= 192 * x0_idx && N1 >= 7) || (x0_idx >= 1 && 64 * t_idx >= T + 2 && 96 * x1_idx + T >= 96 * t_idx && T + 1 >= 192 * x0_idx && 96 * t_idx + 94 >= 96 * x1_idx + T && 192 * x0_idx + 187 >= T && N0 >= 7 && T + N1 >= 192 * x1_idx + 5) || (x0_idx >= 1 && T + 1 >= 192 * x0_idx && N0 >= 7 && N1 >= 7 && 192 * t_idx + 3 >= 3 * T + N1 && 288 * x1_idx + 5 >= 96 * t_idx + N1 && 96 * t_idx + N1 + 89 >= 288 * x1_idx && 192 * x0_idx + N1 + 182 >= 192 * x1_idx) || (x0_idx >= 1 && T + 1 >= 192 * x0_idx && N0 >= 7 && N1 >= 7 && 96 * t_idx + N1 >= 288 * x1_idx + 6 && 192 * t_idx + 3 >= 3 * T + N1 && 288 * x1_idx + 289 >= 96 * t_idx + N1 && 576 * x0_idx + N1 + 557 >= 192 * t_idx) || (x0_idx >= 1 && 64 * t_idx >= T + 2 && T + 1 >= 192 * x0_idx && N0 >= 7 && 3 * T + N1 >= 192 * t_idx + 4 && 192 * x1_idx + 4 >= T + N1 && 96 * t_idx + N1 + 89 >= 288 * x1_idx && 192 * x0_idx + N1 + 182 >= 192 * x1_idx) || (x0_idx >= 1 && T <= 4 && N0 >= 7 && N1 >= 7 && 288 * x1_idx + 5 >= 96 * t_idx + N1 && 192 * t_idx + 9 >= 576 * x0_idx + N1 && 96 * t_idx + N1 + 89 >= 288 * x1_idx && 192 * x0_idx + N1 + 182 >= 192 * x1_idx) || (x0_idx >= 1 && T <= 4 && N0 >= 7 && N1 >= 7 && 96 * t_idx + N1 >= 288 * x1_idx + 6 && 192 * t_idx + 9 >= 576 * x0_idx + N1 && 288 * x1_idx + 289 >= 96 * t_idx + N1 && 576 * x0_idx + N1 + 557 >= 192 * t_idx) || (x0_idx >= 1 && 64 * t_idx >= T + 2 && 96 * t_idx >= 96 * x1_idx + T + 1 && T + 1 >= 192 * x0_idx && 96 * x1_idx + T + 95 >= 96 * t_idx && 192 * x0_idx + 187 >= T && N0 >= 7 && 3 * T + N1 >= 192 * t_idx + 4) || (T >= 5 && 96 * x0_idx + T >= 96 * t_idx && N0 >= 7 && 192 * x0_idx + 4 >= T + N0 && 192 * x0_idx + 7 >= 192 * x1_idx + N0 && 96 * t_idx + N0 + 89 >= 288 * x0_idx && 192 * x1_idx + N0 + 182 >= 192 * x0_idx && N1 >= 7) || (T >= 5 && 192 * x0_idx >= T + 2 && 96 * x0_idx + T >= 96 * t_idx && T + 2 >= 192 * x1_idx && 96 * t_idx + 94 >= 96 * x0_idx + T && 192 * x1_idx + 187 >= T && T + N0 >= 192 * x0_idx + 5 && N1 >= 7) || (x0_idx >= 1 && t_idx >= 3 * x0_idx && 2 * x0_idx + x1_idx == t_idx && T <= 4 && N0 >= 7 && 576 * x0_idx + N1 >= 192 * t_idx + 10) || (t_idx >= 3 * x0_idx && 2 * x0_idx + x1_idx == t_idx && T >= 5 && 192 * x0_idx >= T + 2 && N0 >= 7 && 576 * x0_idx + N1 >= 192 * t_idx + 10) || (3 * x0_idx >= t_idx + 1 && x0_idx + 2 * x1_idx + 2 == t_idx && T >= 5 && 96 * t_idx >= 96 * x0_idx + T + 5 && 96 * t_idx + N0 >= 288 * x0_idx + 19 && N1 >= 7) || (t_idx >= x0_idx + 2 && 3 * x0_idx >= t_idx + 1 && x0_idx + 2 * x1_idx + 2 == t_idx && T <= 4 && 96 * t_idx + N0 >= 288 * x0_idx + 19 && N1 >= 7) || (x0_idx >= 1 && x1_idx == x0_idx + 1 && T + 1 >= 64 * t_idx && N0 >= 7 && 96 * t_idx + N1 >= 288 * x0_idx + 199 && N1 >= 10 && 192 * x0_idx + 196 >= T + N1) || (x0_idx >= 1 && x1_idx == x0_idx + 1 && 96 * t_idx >= 96 * x0_idx + T + 2 && T + 1 >= 64 * t_idx && 192 * x0_idx + 187 >= T && N0 >= 7 && T + N1 >= 192 * x0_idx + 197) || (x0_idx == 0 && T >= 5 && N0 >= 7 && N1 >= 7 && 192 * t_idx + 3 >= 3 * T + N1 && 288 * x1_idx + 5 >= 96 * t_idx + N1 && 96 * t_idx + N1 + 89 >= 288 * x1_idx && N1 + 182 >= 192 * x1_idx) || (x0_idx == 0 && T >= 5 && N0 >= 7 && N1 >= 7 && 96 * t_idx + N1 >= 288 * x1_idx + 6 && 192 * t_idx + 3 >= 3 * T + N1 && 288 * x1_idx + 289 >= 96 * t_idx + N1 && N1 + 557 >= 192 * t_idx) || (x0_idx == 0 && T >= 5 && 64 * t_idx >= T + 2 && N0 >= 7 && 3 * T + N1 >= 192 * t_idx + 4 && 192 * x1_idx + 4 >= T + N1 && 96 * t_idx + N1 + 89 >= 288 * x1_idx && N1 + 182 >= 192 * x1_idx) || (x0_idx == 0 && T >= 5 && 64 * t_idx >= T + 2 && 96 * x1_idx + T >= 96 * t_idx && 96 * t_idx + 94 >= 96 * x1_idx + T && T <= 187 && N0 >= 7 && T + N1 >= 192 * x1_idx + 5) || (x0_idx == 0 && T <= 4 && N0 >= 7 && 192 * t_idx >= N1 + 9 && N1 >= 7 && 288 * x1_idx + 5 >= 96 * t_idx + N1 && 96 * t_idx + N1 + 89 >= 288 * x1_idx && N1 + 182 >= 192 * x1_idx) || (x0_idx == 0 && T <= 4 && N0 >= 7 && 192 * t_idx >= N1 + 9 && N1 >= 7 && 96 * t_idx + N1 >= 288 * x1_idx + 6 && 288 * x1_idx + 289 >= 96 * t_idx + N1 && N1 + 557 >= 192 * t_idx) || (x0_idx == 0 && T >= 5 && 64 * t_idx >= T + 2 && 96 * t_idx >= 96 * x1_idx + T + 1 && 96 * x1_idx + T + 95 >= 96 * t_idx && T <= 187 && N0 >= 7 && 3 * T + N1 >= 192 * t_idx + 4) || (x0_idx >= 1 && x1_idx == x0_idx && T + 1 >= 64 * t_idx && T + 1 >= 192 * x0_idx && 192 * x0_idx + 187 >= T && N1 >= 7 && N0 >= ((2 * T + 1) % 3) + 7 && 192 * t_idx + 186 >= 2 * ((2 * T + 1) % 3) + 3 * T) || (x0_idx >= 1 && x1_idx == x0_idx && T + 1 >= 64 * t_idx && T + 1 >= 192 * x0_idx && 192 * x0_idx + 187 >= T && N0 >= 7 && N1 >= 7 && ((2 * T + 1) % 3) + 6 >= N0 && 192 * t_idx + 2 * N0 + 172 >= 3 * ((2 * T + 1) % 3) + 3 * T) || (t_idx >= 1 && x0_idx == 0 && x1_idx == t_idx && T <= 4 && N0 >= 7 && N1 + 8 >= 192 * t_idx) || (t_idx >= 1 && x0_idx == t_idx && x1_idx == 0 && T <= 4 && N0 >= 192 * t_idx + 1 && N1 >= 7) || (t_idx >= 1 && x0_idx == 0 && x1_idx + 1 == t_idx && T <= 4 && N0 >= 7 && N1 + 8 >= 192 * t_idx) || (t_idx >= 2 && x0_idx == 0 && x1_idx + 2 == t_idx && T <= 4 && N0 >= 7 && N1 + 8 >= 192 * t_idx) || (3 * x0_idx == t_idx && 3 * x1_idx + 3 == t_idx && T >= 5 && 64 * t_idx >= T + 5 && N0 >= 19 && N1 >= 10) || (t_idx >= 3 && 3 * x0_idx == t_idx && 3 * x1_idx + 3 == t_idx && T <= 4 && N0 >= 19 && N1 >= 10) || (t_idx >= 1 && x0_idx == t_idx && x1_idx == 0 && T <= 4 && 192 * t_idx >= N0 && N0 + 89 >= 192 * t_idx && N1 >= 7) || (t_idx >= 2 && x0_idx == 0 && x1_idx + 2 == t_idx && T >= 5 && N0 >= 7 && 192 * t_idx + 3 >= 3 * T + N1 && N1 + 286 >= 192 * t_idx) || (t_idx >= 2 && x0_idx == 0 && x1_idx + 2 == t_idx && T <= 4 && N0 >= 7 && 192 * t_idx >= N1 + 9 && N1 + 286 >= 192 * t_idx) || (t_idx >= 2 && x0_idx == 0 && x1_idx + 2 == t_idx && T >= 5 && T <= 96 && N0 >= 7 && 3 * T + N1 >= 192 * t_idx + 4) || (3 * x0_idx == t_idx && 3 * x1_idx + 3 == t_idx && T >= 5 && 64 * t_idx >= T + 5 && N0 >= 19 && N1 >= 7 && N1 <= 9) || (t_idx >= 3 && 3 * x0_idx == t_idx && 3 * x1_idx + 3 == t_idx && T <= 4 && N0 >= 19 && N1 >= 7 && N1 <= 9) || (x0_idx == 0 && x1_idx == 1 && T >= 5 && T + 1 >= 64 * t_idx && N0 >= 7 && 96 * t_idx + N1 >= 199 && N1 >= 10 && T + N1 <= 196) || (x0_idx == 0 && x1_idx == 1 && T >= 5 && 96 * t_idx >= T + 2 && T + 1 >= 64 * t_idx && T <= 187 && N0 >= 7 && T + N1 >= 197) || (x0_idx == 0 && x1_idx == 0 && T >= 5 && T + 1 >= 64 * t_idx && T <= 187 && N1 >= 7 && ((T - 2) % 3) + N0 >= 9 && 2 * ((T - 2) % 3) + 192 * t_idx + 182 >= 3 * T) || (x0_idx == 0 && x1_idx == 0 && T >= 5 && T + 1 >= 64 * t_idx && T <= 187 && N0 >= 7 && N1 >= 7 && ((T - 2) % 3) + N0 <= 8 && 3 * ((T - 2) % 3) + 192 * t_idx + 2 * N0 + 166 >= 3 * T) || (t_idx == 0 && x0_idx == 0 && x1_idx == 0 && T <= 4 && N0 >= 7 && N1 >= 7)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment