MiniZinc-Auto-Tabling-Models/jp-encoding/instances/data800.dzn

len = 824;
stream = [
 130,
  187,
  130,
  177,
  130,
  197,
  129,
  65,
  147,
  250,
  130,
  204,
  150,
  218,
  130,
  170,
  140,
  169,
  130,
  166,
  130,
  200,
  130,
  173,
  130,
  200,
  130,
  233,
  130,
  198,
  129,
  65,
  146,
  78,
  130,
  197,
  130,
  224,
  139,
  67,
  150,
  161,
  130,
  240,
  136,
  171,
  130,
  233,
  130,
  170,
  130,
  193,
  130,
  196,
  129,
  65,
  130,
  177,
  130,
  204,
  150,
  229,
  130,
  204,
  139,
  223,
  143,
  138,
  130,
  214,
  130,
  205,
  145,
  171,
  130,
  212,
  130,
  221,
  130,
  240,
  130,
  181,
  130,
  200,
  130,
  162,
  142,
  150,
  130,
  201,
  130,
  200,
  130,
  193,
  130,
  196,
  130,
  181,
  130,
  220,
  130,
  193,
  130,
  189,
  130,
  204,
  130,
  197,
  130,
  160,
  130,
  233,
  129,
  66,
  10,
  84,
  104,
  101,
  32,
  113,
  117,
  105,
  99,
  107,
  32,
  98,
  114,
  111,
  119,
  110,
  32,
  102,
  111,
  120,
  32,
  106,
  117,
  109,
  112,
  115,
  32,
  111,
  118,
  101,
  114,
  32,
  116,
  104,
  101,
  32,
  108,
  97,
  122,
  121,
  32,
  100,
  111,
  103,
  10,
  130,
  187,
  130,
  234,
  130,
  170,
  129,
  65,
  130,
  177,
  130,
  204,
  146,
  106,
  130,
  204,
  130,
  217,
  130,
  169,
  130,
  201,
  130,
  205,
  146,
  78,
  130,
  224,
  130,
  162,
  130,
  200,
  130,
  162,
  129,
  66,
  10,
  178,
  191,
  184,
  206,
  164,
  171,
  164,
  200,
  177,
  190,
  164,
  166,
  164,
  200,
  161,
  162,
  164,
  179,
  164,
  206,
  198,
  243,
  187,
  176,
  199,
  175,
  161,
  162,
  181,
  254,
  197,
  212,
  164,
  203,
  164,
  207,
  161,
  162,
  195,
  207,
  191,
  204,
  164,
  200,
  164,
  171,
  196,
  212,
  201,
  247,
  164,
  200,
  164,
  171,
  178,
  208,
  187,
  246,
  164,
  200,
  164,
  171,
  241,
  192,
  241,
  188,
  164,
  200,
  164,
  171,
  177,
  190,
  164,
  166,
  186,
  210,
  164,
  172,
  164,
  196,
  164,
  197,
  164,
  164,
  164,
  198,
  181,
  175,
  164,
  195,
  164,
  191,
  161,
  163,
  10,
  151,
  133,
  144,
  182,
  150,
  229,
  130,
  170,
  129,
  65,
  142,
  233,
  144,
  157,
  145,
  229,
  152,
  72,
  130,
  201,
  130,
  160,
  130,
  233,
  136,
  200,
  143,
  227,
  130,
  205,
  129,
  65,
  130,
  177,
  130,
  204,
  146,
  106,
  130,
  204,
  130,
  217,
  130,
  169,
  130,
  201,
  130,
  224,
  129,
  65,
  137,
  74,
  130,
  226,
  130,
  221,
  130,
  240,
  130,
  183,
  130,
  233,
  142,
  115,
  143,
  151,
  138,
  125,
  130,
  226,
  157,
  134,
  137,
  71,
  150,
  88,
  142,
  113,
  130,
  170,
  129,
  65,
  130,
  224,
  130,
  164,
  147,
  241,
  142,
  79,
  144,
  108,
  130,
  205,
  130,
  160,
  130,
  232,
  130,
  187,
  130,
  164,
  130,
  200,
  130,
  224,
  130,
  204,
  130,
  197,
  130,
  160,
  130,
  233,
  129,
  66,
  10,
  227,
  129,
  157,
  227,
  130,
  140,
  227,
  129,
  140,
  227,
  128,
  129,
  227,
  129,
  147,
  227,
  129,
  174,
  231,
  148,
  183,
  227,
  129,
  174,
  227,
  129,
  187,
  227,
  129,
  139,
  227,
  129,
  171,
  227,
  129,
  175,
  232,
  170,
  176,
  227,
  130,
  130,
  227,
  129,
  132,
  227,
  129,
  170,
  227,
  129,
  132,
  227,
  128,
  130,
  10,
  144,
  101,
  143,
  247,
  130,
  232,
  130,
  204,
  150,
  179,
  147,
  83,
  150,
  67,
  130,
  197,
  143,
  172,
  139,
  159,
  130,
  204,
  142,
  158,
  130,
  169,
  130,
  231,
  145,
  185,
  130,
  206,
  130,
  169,
  130,
  232,
  130,
  181,
  130,
  196,
  130,
  162,
  130,
  233,
  129,
  66,
  10,
  229,
  136,
  165,
  230,
  174,
  181,
  230,
  183,
  177,
  227,
  129,
  132,
  231,
  144,
  134,
  231,
  148,
  177,
  227,
  129,
  167,
  227,
  130,
  130,
  227,
  129,
  170,
  227,
  129,
  132,
  227,
  128,
  130,
  10,
  142,
  227,
  146,
  142,
  130,
  226,
  129,
  91,
  130,
  162,
  129,
  66,
  130,
  198,
  154,
  146,
  130,
  181,
  130,
  189,
  130,
  169,
  130,
  231,
  130,
  197,
  130,
  160,
  130,
  233,
  129,
  66,
  143,
  172,
  142,
  103,
  130,
  201,
  149,
  137,
  130,
  212,
  130,
  179,
  130,
  193,
  130,
  196,
  139,
  65,
  130,
  193,
  130,
  196,
  151,
  136,
  130,
  189,
  142,
  158,
  129,
  65,
  130,
  168,
  130,
  226,
  130,
  182,
  130,
  170,
  145,
  229,
  130,
  171,
  130,
  200,
  138,
  225,
  130,
  240,
  130,
  181,
  130,
  196,
  147,
  241,
  138,
  75,
  130,
  174,
  130,
  231,
  130,
  162,
  130,
  169,
  130,
  231,
  148,
  242,
  130,
  209,
  141,
  126,
  130,
  232,
  130,
  196,
  141,
  152,
  130,
  240,
  148,
  178,
  130,
  169,
  130,
  183,
  147,
  122,
  130,
  170,
  130,
  160,
  130,
  233,
  130,
  169,
  130,
  198,
  137,
  93,
  130,
  193,
  130,
  189,
  130,
  169,
  130,
  231,
  129,
  65,
  130,
  177,
  130,
  204,
  142,
  159,
  130,
  205,
  148,
  178,
  130,
  169,
  130,
  179,
  130,
  184,
  130,
  201,
  148,
  242,
  130,
  241,
  130,
  197,
  140,
  169,
  130,
  185,
  130,
  220,
  130,
  183,
  130,
  198,
  147,
  154,
  130,
  166,
  130,
  189,
  129,
  66,
  10,
  137,
  189,
  140,
  204,
  130,
  169,
  130,
  198,
  137,
  93,
  130,
  164,
  130,
  198,
  129,
  65,
  130,
  177,
  130,
  204,
  147,
  241,
  142,
  79,
  148,
  78,
  129,
  65,
  139,
  158,
  147,
  115,
  130,
  201,
  130,
  205,
  129,
  65,
  146,
  110,
  144,
  107,
  130,
  198,
  130,
  169,
  146,
  210,
  149,
  151,
  130,
  198,
  130,
  169,
  137,
  206,
  142,
  150,
  130,
  198,
  130,
  169,
  233,
  95,
  233,
  91,
  130,
  198,
  130,
  169,
  137,
  93,
  130,
  164,
  141,
  208,
  130,
  170,
  130,
  194,
  130,
  195,
  130,
  162,
  130,
  196,
  139,
  78,
  130,
  193,
  130,
  189,
  129,
  66,
  10
];