1654 lines
113 KiB
MiniZinc
1654 lines
113 KiB
MiniZinc
predicate fzn_all_different_int(array [int] of var int: x);
|
|
predicate count(array [int] of var int: x, var int: y, var int: c);
|
|
predicate fixed_fzn_cumulative(array [int] of var int: s, array [int] of int: d, array [int] of int: r, int: b);
|
|
predicate global_cardinality(array [int] of var int: x, array [int] of int: cover, array [int] of var int: counts);
|
|
predicate maximum_int(var int: m, array [int] of var int: x);
|
|
predicate minimum_int(var int: m, array [int] of var int: x);
|
|
predicate sliding_sum(int: low, int: up, int: seq, array [int] of var int: vs);
|
|
predicate sort(array [int] of var int: x, array [int] of var int: y);
|
|
predicate table_bool(array [int] of var bool: x, array [int, int] of bool: t);
|
|
predicate table_int(array [int] of var int: x, array [int, int] of int: t);
|
|
predicate var_fzn_cumulative(array [int] of var int: s, array [int] of int: d, array [int] of int: r, var int: b);
|
|
array [1..144] of int: puzzle = [0, 0, 134, 2, 4, 0, 0, 0, 0, 0, 0, 0, 136, 0, 0, 1, 0, 5, 6, 10, 115, 106, 0, 0, 139, 0, 0, 124, 0, 122, 117, 0, 0, 107, 0, 0, 0, 131, 126, 0, 123, 0, 0, 12, 0, 0, 0, 103, 0, 0, 144, 0, 0, 0, 0, 0, 14, 0, 99, 101, 0, 0, 129, 0, 23, 21, 0, 16, 65, 97, 96, 0, 30, 29, 25, 0, 0, 19, 0, 0, 0, 66, 94, 0, 32, 0, 0, 27, 57, 59, 60, 0, 0, 0, 0, 92, 0, 40, 42, 0, 56, 58, 0, 0, 72, 0, 0, 0, 0, 39, 0, 0, 0, 0, 78, 73, 71, 85, 69, 0, 35, 0, 0, 46, 53, 0, 0, 0, 80, 84, 0, 0, 36, 0, 45, 0, 0, 52, 51, 0, 0, 0, 0, 88];
|
|
array [1..4048] of int: valid_connections2 = [1, 1, 1, 2, 1, 1, 2, 1, 1, 1, 2, 2, 1, 2, 1, 1, 1, 2, 1, 3, 1, 2, 2, 1, 1, 2, 2, 2, 1, 2, 2, 3, 1, 3, 1, 2, 1, 3, 1, 4, 1, 3, 2, 2, 1, 3, 2, 3, 1, 3, 2, 4, 1, 4, 1, 3, 1, 4, 1, 5, 1, 4, 2, 3, 1, 4, 2, 4, 1, 4, 2, 5, 1, 5, 1, 4, 1, 5, 1, 6, 1, 5, 2, 4, 1, 5, 2, 5, 1, 5, 2, 6, 1, 6, 1, 5, 1, 6, 1, 7, 1, 6, 2, 5, 1, 6, 2, 6, 1, 6, 2, 7, 1, 7, 1, 6, 1, 7, 1, 8, 1, 7, 2, 6, 1, 7, 2, 7, 1, 7, 2, 8, 1, 8, 1, 7, 1, 8, 1, 9, 1, 8, 2, 7, 1, 8, 2, 8, 1, 8, 2, 9, 1, 9, 1, 8, 1, 9, 1, 10, 1, 9, 2, 8, 1, 9, 2, 9, 1, 9, 2, 10, 1, 10, 1, 9, 1, 10, 1, 11, 1, 10, 2, 9, 1, 10, 2, 10, 1, 10, 2, 11, 1, 11, 1, 10, 1, 11, 1, 12, 1, 11, 2, 10, 1, 11, 2, 11, 1, 11, 2, 12, 1, 12, 1, 11, 1, 12, 2, 11, 1, 12, 2, 12, 2, 1, 1, 1, 2, 1, 1, 2, 2, 1, 2, 2, 2, 1, 3, 1, 2, 1, 3, 2, 2, 2, 1, 1, 2, 2, 1, 2, 2, 2, 1, 3, 2, 2, 2, 1, 2, 2, 2, 3, 2, 2, 3, 1, 2, 2, 3, 2, 2, 2, 3, 3, 2, 3, 1, 2, 2, 3, 1, 3, 2, 3, 1, 4, 2, 3, 2, 2, 2, 3, 2, 4, 2, 3, 3, 2, 2, 3, 3, 3, 2, 3, 3, 4, 2, 4, 1, 3, 2, 4, 1, 4, 2, 4, 1, 5, 2, 4, 2, 3, 2, 4, 2, 5, 2, 4, 3, 3, 2, 4, 3, 4, 2, 4, 3, 5, 2, 5, 1, 4, 2, 5, 1, 5, 2, 5, 1, 6, 2, 5, 2, 4, 2, 5, 2, 6, 2, 5, 3, 4, 2, 5, 3, 5, 2, 5, 3, 6, 2, 6, 1, 5, 2, 6, 1, 6, 2, 6, 1, 7, 2, 6, 2, 5, 2, 6, 2, 7, 2, 6, 3, 5, 2, 6, 3, 6, 2, 6, 3, 7, 2, 7, 1, 6, 2, 7, 1, 7, 2, 7, 1, 8, 2, 7, 2, 6, 2, 7, 2, 8, 2, 7, 3, 6, 2, 7, 3, 7, 2, 7, 3, 8, 2, 8, 1, 7, 2, 8, 1, 8, 2, 8, 1, 9, 2, 8, 2, 7, 2, 8, 2, 9, 2, 8, 3, 7, 2, 8, 3, 8, 2, 8, 3, 9, 2, 9, 1, 8, 2, 9, 1, 9, 2, 9, 1, 10, 2, 9, 2, 8, 2, 9, 2, 10, 2, 9, 3, 8, 2, 9, 3, 9, 2, 9, 3, 10, 2, 10, 1, 9, 2, 10, 1, 10, 2, 10, 1, 11, 2, 10, 2, 9, 2, 10, 2, 11, 2, 10, 3, 9, 2, 10, 3, 10, 2, 10, 3, 11, 2, 11, 1, 10, 2, 11, 1, 11, 2, 11, 1, 12, 2, 11, 2, 10, 2, 11, 2, 12, 2, 11, 3, 10, 2, 11, 3, 11, 2, 11, 3, 12, 2, 12, 1, 11, 2, 12, 1, 12, 2, 12, 2, 11, 2, 12, 3, 11, 2, 12, 3, 12, 3, 1, 2, 1, 3, 1, 2, 2, 3, 1, 3, 2, 3, 1, 4, 1, 3, 1, 4, 2, 3, 2, 2, 1, 3, 2, 2, 2, 3, 2, 2, 3, 3, 2, 3, 1, 3, 2, 3, 3, 3, 2, 4, 1, 3, 2, 4, 2, 3, 2, 4, 3, 3, 3, 2, 2, 3, 3, 2, 3, 3, 3, 2, 4, 3, 3, 3, 2, 3, 3, 3, 4, 3, 3, 4, 2, 3, 3, 4, 3, 3, 3, 4, 4, 3, 4, 2, 3, 3, 4, 2, 4, 3, 4, 2, 5, 3, 4, 3, 3, 3, 4, 3, 5, 3, 4, 4, 3, 3, 4, 4, 4, 3, 4, 4, 5, 3, 5, 2, 4, 3, 5, 2, 5, 3, 5, 2, 6, 3, 5, 3, 4, 3, 5, 3, 6, 3, 5, 4, 4, 3, 5, 4, 5, 3, 5, 4, 6, 3, 6, 2, 5, 3, 6, 2, 6, 3, 6, 2, 7, 3, 6, 3, 5, 3, 6, 3, 7, 3, 6, 4, 5, 3, 6, 4, 6, 3, 6, 4, 7, 3, 7, 2, 6, 3, 7, 2, 7, 3, 7, 2, 8, 3, 7, 3, 6, 3, 7, 3, 8, 3, 7, 4, 6, 3, 7, 4, 7, 3, 7, 4, 8, 3, 8, 2, 7, 3, 8, 2, 8, 3, 8, 2, 9, 3, 8, 3, 7, 3, 8, 3, 9, 3, 8, 4, 7, 3, 8, 4, 8, 3, 8, 4, 9, 3, 9, 2, 8, 3, 9, 2, 9, 3, 9, 2, 10, 3, 9, 3, 8, 3, 9, 3, 10, 3, 9, 4, 8, 3, 9, 4, 9, 3, 9, 4, 10, 3, 10, 2, 9, 3, 10, 2, 10, 3, 10, 2, 11, 3, 10, 3, 9, 3, 10, 3, 11, 3, 10, 4, 9, 3, 10, 4, 10, 3, 10, 4, 11, 3, 11, 2, 10, 3, 11, 2, 11, 3, 11, 2, 12, 3, 11, 3, 10, 3, 11, 3, 12, 3, 11, 4, 10, 3, 11, 4, 11, 3, 11, 4, 12, 3, 12, 2, 11, 3, 12, 2, 12, 3, 12, 3, 11, 3, 12, 4, 11, 3, 12, 4, 12, 4, 1, 3, 1, 4, 1, 3, 2, 4, 1, 4, 2, 4, 1, 5, 1, 4, 1, 5, 2, 4, 2, 3, 1, 4, 2, 3, 2, 4, 2, 3, 3, 4, 2, 4, 1, 4, 2, 4, 3, 4, 2, 5, 1, 4, 2, 5, 2, 4, 2, 5, 3, 4, 3, 3, 2, 4, 3, 3, 3, 4, 3, 3, 4, 4, 3, 4, 2, 4, 3, 4, 4, 4, 3, 5, 2, 4, 3, 5, 3, 4, 3, 5, 4, 4, 4, 3, 3, 4, 4, 3, 4, 4, 4, 3, 5, 4, 4, 4, 3, 4, 4, 4, 5, 4, 4, 5, 3, 4, 4, 5, 4, 4, 4, 5, 5, 4, 5, 3, 4, 4, 5, 3, 5, 4, 5, 3, 6, 4, 5, 4, 4, 4, 5, 4, 6, 4, 5, 5, 4, 4, 5, 5, 5, 4, 5, 5, 6, 4, 6, 3, 5, 4, 6, 3, 6, 4, 6, 3, 7, 4, 6, 4, 5, 4, 6, 4, 7, 4, 6, 5, 5, 4, 6, 5, 6, 4, 6, 5, 7, 4, 7, 3, 6, 4, 7, 3, 7, 4, 7, 3, 8, 4, 7, 4, 6, 4, 7, 4, 8, 4, 7, 5, 6, 4, 7, 5, 7, 4, 7, 5, 8, 4, 8, 3, 7, 4, 8, 3, 8, 4, 8, 3, 9, 4, 8, 4, 7, 4, 8, 4, 9, 4, 8, 5, 7, 4, 8, 5, 8, 4, 8, 5, 9, 4, 9, 3, 8, 4, 9, 3, 9, 4, 9, 3, 10, 4, 9, 4, 8, 4, 9, 4, 10, 4, 9, 5, 8, 4, 9, 5, 9, 4, 9, 5, 10, 4, 10, 3, 9, 4, 10, 3, 10, 4, 10, 3, 11, 4, 10, 4, 9, 4, 10, 4, 11, 4, 10, 5, 9, 4, 10, 5, 10, 4, 10, 5, 11, 4, 11, 3, 10, 4, 11, 3, 11, 4, 11, 3, 12, 4, 11, 4, 10, 4, 11, 4, 12, 4, 11, 5, 10, 4, 11, 5, 11, 4, 11, 5, 12, 4, 12, 3, 11, 4, 12, 3, 12, 4, 12, 4, 11, 4, 12, 5, 11, 4, 12, 5, 12, 5, 1, 4, 1, 5, 1, 4, 2, 5, 1, 5, 2, 5, 1, 6, 1, 5, 1, 6, 2, 5, 2, 4, 1, 5, 2, 4, 2, 5, 2, 4, 3, 5, 2, 5, 1, 5, 2, 5, 3, 5, 2, 6, 1, 5, 2, 6, 2, 5, 2, 6, 3, 5, 3, 4, 2, 5, 3, 4, 3, 5, 3, 4, 4, 5, 3, 5, 2, 5, 3, 5, 4, 5, 3, 6, 2, 5, 3, 6, 3, 5, 3, 6, 4, 5, 4, 4, 3, 5, 4, 4, 4, 5, 4, 4, 5, 5, 4, 5, 3, 5, 4, 5, 5, 5, 4, 6, 3, 5, 4, 6, 4, 5, 4, 6, 5, 5, 5, 4, 4, 5, 5, 4, 5, 5, 5, 4, 6, 5, 5, 5, 4, 5, 5, 5, 6, 5, 5, 6, 4, 5, 5, 6, 5, 5, 5, 6, 6, 5, 6, 4, 5, 5, 6, 4, 6, 5, 6, 4, 7, 5, 6, 5, 5, 5, 6, 5, 7, 5, 6, 6, 5, 5, 6, 6, 6, 5, 6, 6, 7, 5, 7, 4, 6, 5, 7, 4, 7, 5, 7, 4, 8, 5, 7, 5, 6, 5, 7, 5, 8, 5, 7, 6, 6, 5, 7, 6, 7, 5, 7, 6, 8, 5, 8, 4, 7, 5, 8, 4, 8, 5, 8, 4, 9, 5, 8, 5, 7, 5, 8, 5, 9, 5, 8, 6, 7, 5, 8, 6, 8, 5, 8, 6, 9, 5, 9, 4, 8, 5, 9, 4, 9, 5, 9, 4, 10, 5, 9, 5, 8, 5, 9, 5, 10, 5, 9, 6, 8, 5, 9, 6, 9, 5, 9, 6, 10, 5, 10, 4, 9, 5, 10, 4, 10, 5, 10, 4, 11, 5, 10, 5, 9, 5, 10, 5, 11, 5, 10, 6, 9, 5, 10, 6, 10, 5, 10, 6, 11, 5, 11, 4, 10, 5, 11, 4, 11, 5, 11, 4, 12, 5, 11, 5, 10, 5, 11, 5, 12, 5, 11, 6, 10, 5, 11, 6, 11, 5, 11, 6, 12, 5, 12, 4, 11, 5, 12, 4, 12, 5, 12, 5, 11, 5, 12, 6, 11, 5, 12, 6, 12, 6, 1, 5, 1, 6, 1, 5, 2, 6, 1, 6, 2, 6, 1, 7, 1, 6, 1, 7, 2, 6, 2, 5, 1, 6, 2, 5, 2, 6, 2, 5, 3, 6, 2, 6, 1, 6, 2, 6, 3, 6, 2, 7, 1, 6, 2, 7, 2, 6, 2, 7, 3, 6, 3, 5, 2, 6, 3, 5, 3, 6, 3, 5, 4, 6, 3, 6, 2, 6, 3, 6, 4, 6, 3, 7, 2, 6, 3, 7, 3, 6, 3, 7, 4, 6, 4, 5, 3, 6, 4, 5, 4, 6, 4, 5, 5, 6, 4, 6, 3, 6, 4, 6, 5, 6, 4, 7, 3, 6, 4, 7, 4, 6, 4, 7, 5, 6, 5, 5, 4, 6, 5, 5, 5, 6, 5, 5, 6, 6, 5, 6, 4, 6, 5, 6, 6, 6, 5, 7, 4, 6, 5, 7, 5, 6, 5, 7, 6, 6, 6, 5, 5, 6, 6, 5, 6, 6, 6, 5, 7, 6, 6, 6, 5, 6, 6, 6, 7, 6, 6, 7, 5, 6, 6, 7, 6, 6, 6, 7, 7, 6, 7, 5, 6, 6, 7, 5, 7, 6, 7, 5, 8, 6, 7, 6, 6, 6, 7, 6, 8, 6, 7, 7, 6, 6, 7, 7, 7, 6, 7, 7, 8, 6, 8, 5, 7, 6, 8, 5, 8, 6, 8, 5, 9, 6, 8, 6, 7, 6, 8, 6, 9, 6, 8, 7, 7, 6, 8, 7, 8, 6, 8, 7, 9, 6, 9, 5, 8, 6, 9, 5, 9, 6, 9, 5, 10, 6, 9, 6, 8, 6, 9, 6, 10, 6, 9, 7, 8, 6, 9, 7, 9, 6, 9, 7, 10, 6, 10, 5, 9, 6, 10, 5, 10, 6, 10, 5, 11, 6, 10, 6, 9, 6, 10, 6, 11, 6, 10, 7, 9, 6, 10, 7, 10, 6, 10, 7, 11, 6, 11, 5, 10, 6, 11, 5, 11, 6, 11, 5, 12, 6, 11, 6, 10, 6, 11, 6, 12, 6, 11, 7, 10, 6, 11, 7, 11, 6, 11, 7, 12, 6, 12, 5, 11, 6, 12, 5, 12, 6, 12, 6, 11, 6, 12, 7, 11, 6, 12, 7, 12, 7, 1, 6, 1, 7, 1, 6, 2, 7, 1, 7, 2, 7, 1, 8, 1, 7, 1, 8, 2, 7, 2, 6, 1, 7, 2, 6, 2, 7, 2, 6, 3, 7, 2, 7, 1, 7, 2, 7, 3, 7, 2, 8, 1, 7, 2, 8, 2, 7, 2, 8, 3, 7, 3, 6, 2, 7, 3, 6, 3, 7, 3, 6, 4, 7, 3, 7, 2, 7, 3, 7, 4, 7, 3, 8, 2, 7, 3, 8, 3, 7, 3, 8, 4, 7, 4, 6, 3, 7, 4, 6, 4, 7, 4, 6, 5, 7, 4, 7, 3, 7, 4, 7, 5, 7, 4, 8, 3, 7, 4, 8, 4, 7, 4, 8, 5, 7, 5, 6, 4, 7, 5, 6, 5, 7, 5, 6, 6, 7, 5, 7, 4, 7, 5, 7, 6, 7, 5, 8, 4, 7, 5, 8, 5, 7, 5, 8, 6, 7, 6, 6, 5, 7, 6, 6, 6, 7, 6, 6, 7, 7, 6, 7, 5, 7, 6, 7, 7, 7, 6, 8, 5, 7, 6, 8, 6, 7, 6, 8, 7, 7, 7, 6, 6, 7, 7, 6, 7, 7, 7, 6, 8, 7, 7, 7, 6, 7, 7, 7, 8, 7, 7, 8, 6, 7, 7, 8, 7, 7, 7, 8, 8, 7, 8, 6, 7, 7, 8, 6, 8, 7, 8, 6, 9, 7, 8, 7, 7, 7, 8, 7, 9, 7, 8, 8, 7, 7, 8, 8, 8, 7, 8, 8, 9, 7, 9, 6, 8, 7, 9, 6, 9, 7, 9, 6, 10, 7, 9, 7, 8, 7, 9, 7, 10, 7, 9, 8, 8, 7, 9, 8, 9, 7, 9, 8, 10, 7, 10, 6, 9, 7, 10, 6, 10, 7, 10, 6, 11, 7, 10, 7, 9, 7, 10, 7, 11, 7, 10, 8, 9, 7, 10, 8, 10, 7, 10, 8, 11, 7, 11, 6, 10, 7, 11, 6, 11, 7, 11, 6, 12, 7, 11, 7, 10, 7, 11, 7, 12, 7, 11, 8, 10, 7, 11, 8, 11, 7, 11, 8, 12, 7, 12, 6, 11, 7, 12, 6, 12, 7, 12, 7, 11, 7, 12, 8, 11, 7, 12, 8, 12, 8, 1, 7, 1, 8, 1, 7, 2, 8, 1, 8, 2, 8, 1, 9, 1, 8, 1, 9, 2, 8, 2, 7, 1, 8, 2, 7, 2, 8, 2, 7, 3, 8, 2, 8, 1, 8, 2, 8, 3, 8, 2, 9, 1, 8, 2, 9, 2, 8, 2, 9, 3, 8, 3, 7, 2, 8, 3, 7, 3, 8, 3, 7, 4, 8, 3, 8, 2, 8, 3, 8, 4, 8, 3, 9, 2, 8, 3, 9, 3, 8, 3, 9, 4, 8, 4, 7, 3, 8, 4, 7, 4, 8, 4, 7, 5, 8, 4, 8, 3, 8, 4, 8, 5, 8, 4, 9, 3, 8, 4, 9, 4, 8, 4, 9, 5, 8, 5, 7, 4, 8, 5, 7, 5, 8, 5, 7, 6, 8, 5, 8, 4, 8, 5, 8, 6, 8, 5, 9, 4, 8, 5, 9, 5, 8, 5, 9, 6, 8, 6, 7, 5, 8, 6, 7, 6, 8, 6, 7, 7, 8, 6, 8, 5, 8, 6, 8, 7, 8, 6, 9, 5, 8, 6, 9, 6, 8, 6, 9, 7, 8, 7, 7, 6, 8, 7, 7, 7, 8, 7, 7, 8, 8, 7, 8, 6, 8, 7, 8, 8, 8, 7, 9, 6, 8, 7, 9, 7, 8, 7, 9, 8, 8, 8, 7, 7, 8, 8, 7, 8, 8, 8, 7, 9, 8, 8, 8, 7, 8, 8, 8, 9, 8, 8, 9, 7, 8, 8, 9, 8, 8, 8, 9, 9, 8, 9, 7, 8, 8, 9, 7, 9, 8, 9, 7, 10, 8, 9, 8, 8, 8, 9, 8, 10, 8, 9, 9, 8, 8, 9, 9, 9, 8, 9, 9, 10, 8, 10, 7, 9, 8, 10, 7, 10, 8, 10, 7, 11, 8, 10, 8, 9, 8, 10, 8, 11, 8, 10, 9, 9, 8, 10, 9, 10, 8, 10, 9, 11, 8, 11, 7, 10, 8, 11, 7, 11, 8, 11, 7, 12, 8, 11, 8, 10, 8, 11, 8, 12, 8, 11, 9, 10, 8, 11, 9, 11, 8, 11, 9, 12, 8, 12, 7, 11, 8, 12, 7, 12, 8, 12, 8, 11, 8, 12, 9, 11, 8, 12, 9, 12, 9, 1, 8, 1, 9, 1, 8, 2, 9, 1, 9, 2, 9, 1, 10, 1, 9, 1, 10, 2, 9, 2, 8, 1, 9, 2, 8, 2, 9, 2, 8, 3, 9, 2, 9, 1, 9, 2, 9, 3, 9, 2, 10, 1, 9, 2, 10, 2, 9, 2, 10, 3, 9, 3, 8, 2, 9, 3, 8, 3, 9, 3, 8, 4, 9, 3, 9, 2, 9, 3, 9, 4, 9, 3, 10, 2, 9, 3, 10, 3, 9, 3, 10, 4, 9, 4, 8, 3, 9, 4, 8, 4, 9, 4, 8, 5, 9, 4, 9, 3, 9, 4, 9, 5, 9, 4, 10, 3, 9, 4, 10, 4, 9, 4, 10, 5, 9, 5, 8, 4, 9, 5, 8, 5, 9, 5, 8, 6, 9, 5, 9, 4, 9, 5, 9, 6, 9, 5, 10, 4, 9, 5, 10, 5, 9, 5, 10, 6, 9, 6, 8, 5, 9, 6, 8, 6, 9, 6, 8, 7, 9, 6, 9, 5, 9, 6, 9, 7, 9, 6, 10, 5, 9, 6, 10, 6, 9, 6, 10, 7, 9, 7, 8, 6, 9, 7, 8, 7, 9, 7, 8, 8, 9, 7, 9, 6, 9, 7, 9, 8, 9, 7, 10, 6, 9, 7, 10, 7, 9, 7, 10, 8, 9, 8, 8, 7, 9, 8, 8, 8, 9, 8, 8, 9, 9, 8, 9, 7, 9, 8, 9, 9, 9, 8, 10, 7, 9, 8, 10, 8, 9, 8, 10, 9, 9, 9, 8, 8, 9, 9, 8, 9, 9, 9, 8, 10, 9, 9, 9, 8, 9, 9, 9, 10, 9, 9, 10, 8, 9, 9, 10, 9, 9, 9, 10, 10, 9, 10, 8, 9, 9, 10, 8, 10, 9, 10, 8, 11, 9, 10, 9, 9, 9, 10, 9, 11, 9, 10, 10, 9, 9, 10, 10, 10, 9, 10, 10, 11, 9, 11, 8, 10, 9, 11, 8, 11, 9, 11, 8, 12, 9, 11, 9, 10, 9, 11, 9, 12, 9, 11, 10, 10, 9, 11, 10, 11, 9, 11, 10, 12, 9, 12, 8, 11, 9, 12, 8, 12, 9, 12, 9, 11, 9, 12, 10, 11, 9, 12, 10, 12, 10, 1, 9, 1, 10, 1, 9, 2, 10, 1, 10, 2, 10, 1, 11, 1, 10, 1, 11, 2, 10, 2, 9, 1, 10, 2, 9, 2, 10, 2, 9, 3, 10, 2, 10, 1, 10, 2, 10, 3, 10, 2, 11, 1, 10, 2, 11, 2, 10, 2, 11, 3, 10, 3, 9, 2, 10, 3, 9, 3, 10, 3, 9, 4, 10, 3, 10, 2, 10, 3, 10, 4, 10, 3, 11, 2, 10, 3, 11, 3, 10, 3, 11, 4, 10, 4, 9, 3, 10, 4, 9, 4, 10, 4, 9, 5, 10, 4, 10, 3, 10, 4, 10, 5, 10, 4, 11, 3, 10, 4, 11, 4, 10, 4, 11, 5, 10, 5, 9, 4, 10, 5, 9, 5, 10, 5, 9, 6, 10, 5, 10, 4, 10, 5, 10, 6, 10, 5, 11, 4, 10, 5, 11, 5, 10, 5, 11, 6, 10, 6, 9, 5, 10, 6, 9, 6, 10, 6, 9, 7, 10, 6, 10, 5, 10, 6, 10, 7, 10, 6, 11, 5, 10, 6, 11, 6, 10, 6, 11, 7, 10, 7, 9, 6, 10, 7, 9, 7, 10, 7, 9, 8, 10, 7, 10, 6, 10, 7, 10, 8, 10, 7, 11, 6, 10, 7, 11, 7, 10, 7, 11, 8, 10, 8, 9, 7, 10, 8, 9, 8, 10, 8, 9, 9, 10, 8, 10, 7, 10, 8, 10, 9, 10, 8, 11, 7, 10, 8, 11, 8, 10, 8, 11, 9, 10, 9, 9, 8, 10, 9, 9, 9, 10, 9, 9, 10, 10, 9, 10, 8, 10, 9, 10, 10, 10, 9, 11, 8, 10, 9, 11, 9, 10, 9, 11, 10, 10, 10, 9, 9, 10, 10, 9, 10, 10, 10, 9, 11, 10, 10, 10, 9, 10, 10, 10, 11, 10, 10, 11, 9, 10, 10, 11, 10, 10, 10, 11, 11, 10, 11, 9, 10, 10, 11, 9, 11, 10, 11, 9, 12, 10, 11, 10, 10, 10, 11, 10, 12, 10, 11, 11, 10, 10, 11, 11, 11, 10, 11, 11, 12, 10, 12, 9, 11, 10, 12, 9, 12, 10, 12, 10, 11, 10, 12, 11, 11, 10, 12, 11, 12, 11, 1, 10, 1, 11, 1, 10, 2, 11, 1, 11, 2, 11, 1, 12, 1, 11, 1, 12, 2, 11, 2, 10, 1, 11, 2, 10, 2, 11, 2, 10, 3, 11, 2, 11, 1, 11, 2, 11, 3, 11, 2, 12, 1, 11, 2, 12, 2, 11, 2, 12, 3, 11, 3, 10, 2, 11, 3, 10, 3, 11, 3, 10, 4, 11, 3, 11, 2, 11, 3, 11, 4, 11, 3, 12, 2, 11, 3, 12, 3, 11, 3, 12, 4, 11, 4, 10, 3, 11, 4, 10, 4, 11, 4, 10, 5, 11, 4, 11, 3, 11, 4, 11, 5, 11, 4, 12, 3, 11, 4, 12, 4, 11, 4, 12, 5, 11, 5, 10, 4, 11, 5, 10, 5, 11, 5, 10, 6, 11, 5, 11, 4, 11, 5, 11, 6, 11, 5, 12, 4, 11, 5, 12, 5, 11, 5, 12, 6, 11, 6, 10, 5, 11, 6, 10, 6, 11, 6, 10, 7, 11, 6, 11, 5, 11, 6, 11, 7, 11, 6, 12, 5, 11, 6, 12, 6, 11, 6, 12, 7, 11, 7, 10, 6, 11, 7, 10, 7, 11, 7, 10, 8, 11, 7, 11, 6, 11, 7, 11, 8, 11, 7, 12, 6, 11, 7, 12, 7, 11, 7, 12, 8, 11, 8, 10, 7, 11, 8, 10, 8, 11, 8, 10, 9, 11, 8, 11, 7, 11, 8, 11, 9, 11, 8, 12, 7, 11, 8, 12, 8, 11, 8, 12, 9, 11, 9, 10, 8, 11, 9, 10, 9, 11, 9, 10, 10, 11, 9, 11, 8, 11, 9, 11, 10, 11, 9, 12, 8, 11, 9, 12, 9, 11, 9, 12, 10, 11, 10, 10, 9, 11, 10, 10, 10, 11, 10, 10, 11, 11, 10, 11, 9, 11, 10, 11, 11, 11, 10, 12, 9, 11, 10, 12, 10, 11, 10, 12, 11, 11, 11, 10, 10, 11, 11, 10, 11, 11, 11, 10, 12, 11, 11, 11, 10, 11, 11, 11, 12, 11, 11, 12, 10, 11, 11, 12, 11, 11, 11, 12, 12, 11, 12, 10, 11, 11, 12, 10, 12, 11, 12, 11, 11, 11, 12, 12, 11, 11, 12, 12, 12, 12, 1, 11, 1, 12, 1, 11, 2, 12, 1, 12, 2, 12, 2, 11, 1, 12, 2, 11, 2, 12, 2, 11, 3, 12, 2, 12, 1, 12, 2, 12, 3, 12, 3, 11, 2, 12, 3, 11, 3, 12, 3, 11, 4, 12, 3, 12, 2, 12, 3, 12, 4, 12, 4, 11, 3, 12, 4, 11, 4, 12, 4, 11, 5, 12, 4, 12, 3, 12, 4, 12, 5, 12, 5, 11, 4, 12, 5, 11, 5, 12, 5, 11, 6, 12, 5, 12, 4, 12, 5, 12, 6, 12, 6, 11, 5, 12, 6, 11, 6, 12, 6, 11, 7, 12, 6, 12, 5, 12, 6, 12, 7, 12, 7, 11, 6, 12, 7, 11, 7, 12, 7, 11, 8, 12, 7, 12, 6, 12, 7, 12, 8, 12, 8, 11, 7, 12, 8, 11, 8, 12, 8, 11, 9, 12, 8, 12, 7, 12, 8, 12, 9, 12, 9, 11, 8, 12, 9, 11, 9, 12, 9, 11, 10, 12, 9, 12, 8, 12, 9, 12, 10, 12, 10, 11, 9, 12, 10, 11, 10, 12, 10, 11, 11, 12, 10, 12, 9, 12, 10, 12, 11, 12, 11, 11, 10, 12, 11, 11, 11, 12, 11, 11, 12, 12, 11, 12, 10, 12, 11, 12, 12, 12, 12, 11, 11, 12, 12, 11, 12, 12, 12, 12, 11];
|
|
var 1..144: INT____00005 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00007 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00013 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00015 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00021 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00023 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00029 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00031 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00037 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00039 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00045 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00047 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00053 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00055 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00061 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00063 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00069 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00071 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00077 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00079 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00085 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00087 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00093 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00095 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00101 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00103 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00109 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00111 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00117 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00119 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00125 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00127 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00133 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00135 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00141 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00143 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00149 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00151 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00157 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00159 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00165 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00167 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00173 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00175 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00181 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00183 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00189 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00191 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00197 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00199 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00205 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00207 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00213 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00215 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00221 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00223 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00229 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00231 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00237 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00239 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00245 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00247 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00253 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00255 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00261 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00263 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00269 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00271 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00277 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00279 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00285 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00287 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00293 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00295 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00301 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00303 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00309 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00311 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00317 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00319 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00325 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00327 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00333 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00335 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00341 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00343 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00349 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00351 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00357 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00359 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00365 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00367 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00373 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00375 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00381 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00383 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00389 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00391 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00397 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00399 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00405 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00407 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00413 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00415 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00421 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00423 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00429 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00431 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00437 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00439 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00445 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00447 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00453 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00455 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00461 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00463 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00469 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00471 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00477 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00479 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00485 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00487 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00493 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00495 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00501 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00503 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00509 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00511 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00517 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00519 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00525 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00527 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00533 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00535 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00541 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00543 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00549 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00551 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00557 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00559 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00565 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00567 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00573 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00575 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00581 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00583 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00589 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00591 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00597 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00599 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00605 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00607 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00613 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00615 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00621 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00623 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00629 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00631 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00637 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00639 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00645 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00647 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00653 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00655 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00661 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00663 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00669 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00671 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00677 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00679 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00685 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00687 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00693 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00695 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00701 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00703 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00709 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00711 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00717 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00719 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00725 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00727 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00733 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00735 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00741 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00743 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00749 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00751 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00757 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00759 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00765 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00767 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00773 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00775 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00781 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00783 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00789 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00791 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00797 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00799 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00805 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00807 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00813 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00815 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00821 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00823 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00829 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00831 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00837 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00839 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00845 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00847 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00853 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00855 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00861 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00863 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00869 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00871 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00877 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00879 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00885 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00887 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00893 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00895 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00901 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00903 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00909 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00911 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00917 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00919 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00925 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00927 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00933 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00935 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00941 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00943 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00949 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00951 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00957 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00959 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00965 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00967 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00973 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00975 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00981 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00983 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00989 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00991 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00997 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____00999 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____01005 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____01007 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____01013 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____01015 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____01021 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____01023 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____01029 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____01031 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____01037 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____01039 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____01045 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____01047 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____01053 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____01055 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____01061 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____01063 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____01069 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____01071 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____01077 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____01079 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____01085 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____01087 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____01093 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____01095 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____01101 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____01103 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____01109 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____01111 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____01117 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____01119 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____01125 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____01127 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____01133 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____01135 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____01141 :: is_defined_var :: var_is_introduced;
|
|
var 1..144: INT____01143 :: is_defined_var :: var_is_introduced;
|
|
var 1..12: i1____00001;
|
|
var 1..12: i1____00009;
|
|
var 1..12: i1____00017;
|
|
var 1..12: i1____00025;
|
|
var 1..12: i1____00033;
|
|
var 1..12: i1____00041;
|
|
var 1..12: i1____00049;
|
|
var 1..12: i1____00057;
|
|
var 1..12: i1____00065;
|
|
var 1..12: i1____00073;
|
|
var 1..12: i1____00081;
|
|
var 1..12: i1____00089;
|
|
var 1..12: i1____00097;
|
|
var 1..12: i1____00105;
|
|
var 1..12: i1____00113;
|
|
var 1..12: i1____00121;
|
|
var 1..12: i1____00129;
|
|
var 1..12: i1____00137;
|
|
var 1..12: i1____00145;
|
|
var 1..12: i1____00153;
|
|
var 1..12: i1____00161;
|
|
var 1..12: i1____00169;
|
|
var 1..12: i1____00177;
|
|
var 1..12: i1____00185;
|
|
var 1..12: i1____00193;
|
|
var 1..12: i1____00201;
|
|
var 1..12: i1____00209;
|
|
var 1..12: i1____00217;
|
|
var 1..12: i1____00225;
|
|
var 1..12: i1____00233;
|
|
var 1..12: i1____00241;
|
|
var 1..12: i1____00249;
|
|
var 1..12: i1____00257;
|
|
var 1..12: i1____00265;
|
|
var 1..12: i1____00273;
|
|
var 1..12: i1____00281;
|
|
var 1..12: i1____00289;
|
|
var 1..12: i1____00297;
|
|
var 1..12: i1____00305;
|
|
var 1..12: i1____00313;
|
|
var 1..12: i1____00321;
|
|
var 1..12: i1____00329;
|
|
var 1..12: i1____00337;
|
|
var 1..12: i1____00345;
|
|
var 1..12: i1____00353;
|
|
var 1..12: i1____00361;
|
|
var 1..12: i1____00369;
|
|
var 1..12: i1____00377;
|
|
var 1..12: i1____00385;
|
|
var 1..12: i1____00393;
|
|
var 1..12: i1____00401;
|
|
var 1..12: i1____00409;
|
|
var 1..12: i1____00417;
|
|
var 1..12: i1____00425;
|
|
var 1..12: i1____00433;
|
|
var 1..12: i1____00441;
|
|
var 1..12: i1____00449;
|
|
var 1..12: i1____00457;
|
|
var 1..12: i1____00465;
|
|
var 1..12: i1____00473;
|
|
var 1..12: i1____00481;
|
|
var 1..12: i1____00489;
|
|
var 1..12: i1____00497;
|
|
var 1..12: i1____00505;
|
|
var 1..12: i1____00513;
|
|
var 1..12: i1____00521;
|
|
var 1..12: i1____00529;
|
|
var 1..12: i1____00537;
|
|
var 1..12: i1____00545;
|
|
var 1..12: i1____00553;
|
|
var 1..12: i1____00561;
|
|
var 1..12: i1____00569;
|
|
var 1..12: i1____00577;
|
|
var 1..12: i1____00585;
|
|
var 1..12: i1____00593;
|
|
var 1..12: i1____00601;
|
|
var 1..12: i1____00609;
|
|
var 1..12: i1____00617;
|
|
var 1..12: i1____00625;
|
|
var 1..12: i1____00633;
|
|
var 1..12: i1____00641;
|
|
var 1..12: i1____00649;
|
|
var 1..12: i1____00657;
|
|
var 1..12: i1____00665;
|
|
var 1..12: i1____00673;
|
|
var 1..12: i1____00681;
|
|
var 1..12: i1____00689;
|
|
var 1..12: i1____00697;
|
|
var 1..12: i1____00705;
|
|
var 1..12: i1____00713;
|
|
var 1..12: i1____00721;
|
|
var 1..12: i1____00729;
|
|
var 1..12: i1____00737;
|
|
var 1..12: i1____00745;
|
|
var 1..12: i1____00753;
|
|
var 1..12: i1____00761;
|
|
var 1..12: i1____00769;
|
|
var 1..12: i1____00777;
|
|
var 1..12: i1____00785;
|
|
var 1..12: i1____00793;
|
|
var 1..12: i1____00801;
|
|
var 1..12: i1____00809;
|
|
var 1..12: i1____00817;
|
|
var 1..12: i1____00825;
|
|
var 1..12: i1____00833;
|
|
var 1..12: i1____00841;
|
|
var 1..12: i1____00849;
|
|
var 1..12: i1____00857;
|
|
var 1..12: i1____00865;
|
|
var 1..12: i1____00873;
|
|
var 1..12: i1____00881;
|
|
var 1..12: i1____00889;
|
|
var 1..12: i1____00897;
|
|
var 1..12: i1____00905;
|
|
var 1..12: i1____00913;
|
|
var 1..12: i1____00921;
|
|
var 1..12: i1____00929;
|
|
var 1..12: i1____00937;
|
|
var 1..12: i1____00945;
|
|
var 1..12: i1____00953;
|
|
var 1..12: i1____00961;
|
|
var 1..12: i1____00969;
|
|
var 1..12: i1____00977;
|
|
var 1..12: i1____00985;
|
|
var 1..12: i1____00993;
|
|
var 1..12: i1____01001;
|
|
var 1..12: i1____01009;
|
|
var 1..12: i1____01017;
|
|
var 1..12: i1____01025;
|
|
var 1..12: i1____01033;
|
|
var 1..12: i1____01041;
|
|
var 1..12: i1____01049;
|
|
var 1..12: i1____01057;
|
|
var 1..12: i1____01065;
|
|
var 1..12: i1____01073;
|
|
var 1..12: i1____01081;
|
|
var 1..12: i1____01089;
|
|
var 1..12: i1____01097;
|
|
var 1..12: i1____01105;
|
|
var 1..12: i1____01113;
|
|
var 1..12: i1____01121;
|
|
var 1..12: i1____01129;
|
|
var 1..12: i1____01137;
|
|
var 1..12: i2____00003;
|
|
var 1..12: i2____00011;
|
|
var 1..12: i2____00019;
|
|
var 1..12: i2____00027;
|
|
var 1..12: i2____00035;
|
|
var 1..12: i2____00043;
|
|
var 1..12: i2____00051;
|
|
var 1..12: i2____00059;
|
|
var 1..12: i2____00067;
|
|
var 1..12: i2____00075;
|
|
var 1..12: i2____00083;
|
|
var 1..12: i2____00091;
|
|
var 1..12: i2____00099;
|
|
var 1..12: i2____00107;
|
|
var 1..12: i2____00115;
|
|
var 1..12: i2____00123;
|
|
var 1..12: i2____00131;
|
|
var 1..12: i2____00139;
|
|
var 1..12: i2____00147;
|
|
var 1..12: i2____00155;
|
|
var 1..12: i2____00163;
|
|
var 1..12: i2____00171;
|
|
var 1..12: i2____00179;
|
|
var 1..12: i2____00187;
|
|
var 1..12: i2____00195;
|
|
var 1..12: i2____00203;
|
|
var 1..12: i2____00211;
|
|
var 1..12: i2____00219;
|
|
var 1..12: i2____00227;
|
|
var 1..12: i2____00235;
|
|
var 1..12: i2____00243;
|
|
var 1..12: i2____00251;
|
|
var 1..12: i2____00259;
|
|
var 1..12: i2____00267;
|
|
var 1..12: i2____00275;
|
|
var 1..12: i2____00283;
|
|
var 1..12: i2____00291;
|
|
var 1..12: i2____00299;
|
|
var 1..12: i2____00307;
|
|
var 1..12: i2____00315;
|
|
var 1..12: i2____00323;
|
|
var 1..12: i2____00331;
|
|
var 1..12: i2____00339;
|
|
var 1..12: i2____00347;
|
|
var 1..12: i2____00355;
|
|
var 1..12: i2____00363;
|
|
var 1..12: i2____00371;
|
|
var 1..12: i2____00379;
|
|
var 1..12: i2____00387;
|
|
var 1..12: i2____00395;
|
|
var 1..12: i2____00403;
|
|
var 1..12: i2____00411;
|
|
var 1..12: i2____00419;
|
|
var 1..12: i2____00427;
|
|
var 1..12: i2____00435;
|
|
var 1..12: i2____00443;
|
|
var 1..12: i2____00451;
|
|
var 1..12: i2____00459;
|
|
var 1..12: i2____00467;
|
|
var 1..12: i2____00475;
|
|
var 1..12: i2____00483;
|
|
var 1..12: i2____00491;
|
|
var 1..12: i2____00499;
|
|
var 1..12: i2____00507;
|
|
var 1..12: i2____00515;
|
|
var 1..12: i2____00523;
|
|
var 1..12: i2____00531;
|
|
var 1..12: i2____00539;
|
|
var 1..12: i2____00547;
|
|
var 1..12: i2____00555;
|
|
var 1..12: i2____00563;
|
|
var 1..12: i2____00571;
|
|
var 1..12: i2____00579;
|
|
var 1..12: i2____00587;
|
|
var 1..12: i2____00595;
|
|
var 1..12: i2____00603;
|
|
var 1..12: i2____00611;
|
|
var 1..12: i2____00619;
|
|
var 1..12: i2____00627;
|
|
var 1..12: i2____00635;
|
|
var 1..12: i2____00643;
|
|
var 1..12: i2____00651;
|
|
var 1..12: i2____00659;
|
|
var 1..12: i2____00667;
|
|
var 1..12: i2____00675;
|
|
var 1..12: i2____00683;
|
|
var 1..12: i2____00691;
|
|
var 1..12: i2____00699;
|
|
var 1..12: i2____00707;
|
|
var 1..12: i2____00715;
|
|
var 1..12: i2____00723;
|
|
var 1..12: i2____00731;
|
|
var 1..12: i2____00739;
|
|
var 1..12: i2____00747;
|
|
var 1..12: i2____00755;
|
|
var 1..12: i2____00763;
|
|
var 1..12: i2____00771;
|
|
var 1..12: i2____00779;
|
|
var 1..12: i2____00787;
|
|
var 1..12: i2____00795;
|
|
var 1..12: i2____00803;
|
|
var 1..12: i2____00811;
|
|
var 1..12: i2____00819;
|
|
var 1..12: i2____00827;
|
|
var 1..12: i2____00835;
|
|
var 1..12: i2____00843;
|
|
var 1..12: i2____00851;
|
|
var 1..12: i2____00859;
|
|
var 1..12: i2____00867;
|
|
var 1..12: i2____00875;
|
|
var 1..12: i2____00883;
|
|
var 1..12: i2____00891;
|
|
var 1..12: i2____00899;
|
|
var 1..12: i2____00907;
|
|
var 1..12: i2____00915;
|
|
var 1..12: i2____00923;
|
|
var 1..12: i2____00931;
|
|
var 1..12: i2____00939;
|
|
var 1..12: i2____00947;
|
|
var 1..12: i2____00955;
|
|
var 1..12: i2____00963;
|
|
var 1..12: i2____00971;
|
|
var 1..12: i2____00979;
|
|
var 1..12: i2____00987;
|
|
var 1..12: i2____00995;
|
|
var 1..12: i2____01003;
|
|
var 1..12: i2____01011;
|
|
var 1..12: i2____01019;
|
|
var 1..12: i2____01027;
|
|
var 1..12: i2____01035;
|
|
var 1..12: i2____01043;
|
|
var 1..12: i2____01051;
|
|
var 1..12: i2____01059;
|
|
var 1..12: i2____01067;
|
|
var 1..12: i2____01075;
|
|
var 1..12: i2____01083;
|
|
var 1..12: i2____01091;
|
|
var 1..12: i2____01099;
|
|
var 1..12: i2____01107;
|
|
var 1..12: i2____01115;
|
|
var 1..12: i2____01123;
|
|
var 1..12: i2____01131;
|
|
var 1..12: i2____01139;
|
|
var 1..12: j1____00002;
|
|
var 1..12: j1____00010;
|
|
var 1..12: j1____00018;
|
|
var 1..12: j1____00026;
|
|
var 1..12: j1____00034;
|
|
var 1..12: j1____00042;
|
|
var 1..12: j1____00050;
|
|
var 1..12: j1____00058;
|
|
var 1..12: j1____00066;
|
|
var 1..12: j1____00074;
|
|
var 1..12: j1____00082;
|
|
var 1..12: j1____00090;
|
|
var 1..12: j1____00098;
|
|
var 1..12: j1____00106;
|
|
var 1..12: j1____00114;
|
|
var 1..12: j1____00122;
|
|
var 1..12: j1____00130;
|
|
var 1..12: j1____00138;
|
|
var 1..12: j1____00146;
|
|
var 1..12: j1____00154;
|
|
var 1..12: j1____00162;
|
|
var 1..12: j1____00170;
|
|
var 1..12: j1____00178;
|
|
var 1..12: j1____00186;
|
|
var 1..12: j1____00194;
|
|
var 1..12: j1____00202;
|
|
var 1..12: j1____00210;
|
|
var 1..12: j1____00218;
|
|
var 1..12: j1____00226;
|
|
var 1..12: j1____00234;
|
|
var 1..12: j1____00242;
|
|
var 1..12: j1____00250;
|
|
var 1..12: j1____00258;
|
|
var 1..12: j1____00266;
|
|
var 1..12: j1____00274;
|
|
var 1..12: j1____00282;
|
|
var 1..12: j1____00290;
|
|
var 1..12: j1____00298;
|
|
var 1..12: j1____00306;
|
|
var 1..12: j1____00314;
|
|
var 1..12: j1____00322;
|
|
var 1..12: j1____00330;
|
|
var 1..12: j1____00338;
|
|
var 1..12: j1____00346;
|
|
var 1..12: j1____00354;
|
|
var 1..12: j1____00362;
|
|
var 1..12: j1____00370;
|
|
var 1..12: j1____00378;
|
|
var 1..12: j1____00386;
|
|
var 1..12: j1____00394;
|
|
var 1..12: j1____00402;
|
|
var 1..12: j1____00410;
|
|
var 1..12: j1____00418;
|
|
var 1..12: j1____00426;
|
|
var 1..12: j1____00434;
|
|
var 1..12: j1____00442;
|
|
var 1..12: j1____00450;
|
|
var 1..12: j1____00458;
|
|
var 1..12: j1____00466;
|
|
var 1..12: j1____00474;
|
|
var 1..12: j1____00482;
|
|
var 1..12: j1____00490;
|
|
var 1..12: j1____00498;
|
|
var 1..12: j1____00506;
|
|
var 1..12: j1____00514;
|
|
var 1..12: j1____00522;
|
|
var 1..12: j1____00530;
|
|
var 1..12: j1____00538;
|
|
var 1..12: j1____00546;
|
|
var 1..12: j1____00554;
|
|
var 1..12: j1____00562;
|
|
var 1..12: j1____00570;
|
|
var 1..12: j1____00578;
|
|
var 1..12: j1____00586;
|
|
var 1..12: j1____00594;
|
|
var 1..12: j1____00602;
|
|
var 1..12: j1____00610;
|
|
var 1..12: j1____00618;
|
|
var 1..12: j1____00626;
|
|
var 1..12: j1____00634;
|
|
var 1..12: j1____00642;
|
|
var 1..12: j1____00650;
|
|
var 1..12: j1____00658;
|
|
var 1..12: j1____00666;
|
|
var 1..12: j1____00674;
|
|
var 1..12: j1____00682;
|
|
var 1..12: j1____00690;
|
|
var 1..12: j1____00698;
|
|
var 1..12: j1____00706;
|
|
var 1..12: j1____00714;
|
|
var 1..12: j1____00722;
|
|
var 1..12: j1____00730;
|
|
var 1..12: j1____00738;
|
|
var 1..12: j1____00746;
|
|
var 1..12: j1____00754;
|
|
var 1..12: j1____00762;
|
|
var 1..12: j1____00770;
|
|
var 1..12: j1____00778;
|
|
var 1..12: j1____00786;
|
|
var 1..12: j1____00794;
|
|
var 1..12: j1____00802;
|
|
var 1..12: j1____00810;
|
|
var 1..12: j1____00818;
|
|
var 1..12: j1____00826;
|
|
var 1..12: j1____00834;
|
|
var 1..12: j1____00842;
|
|
var 1..12: j1____00850;
|
|
var 1..12: j1____00858;
|
|
var 1..12: j1____00866;
|
|
var 1..12: j1____00874;
|
|
var 1..12: j1____00882;
|
|
var 1..12: j1____00890;
|
|
var 1..12: j1____00898;
|
|
var 1..12: j1____00906;
|
|
var 1..12: j1____00914;
|
|
var 1..12: j1____00922;
|
|
var 1..12: j1____00930;
|
|
var 1..12: j1____00938;
|
|
var 1..12: j1____00946;
|
|
var 1..12: j1____00954;
|
|
var 1..12: j1____00962;
|
|
var 1..12: j1____00970;
|
|
var 1..12: j1____00978;
|
|
var 1..12: j1____00986;
|
|
var 1..12: j1____00994;
|
|
var 1..12: j1____01002;
|
|
var 1..12: j1____01010;
|
|
var 1..12: j1____01018;
|
|
var 1..12: j1____01026;
|
|
var 1..12: j1____01034;
|
|
var 1..12: j1____01042;
|
|
var 1..12: j1____01050;
|
|
var 1..12: j1____01058;
|
|
var 1..12: j1____01066;
|
|
var 1..12: j1____01074;
|
|
var 1..12: j1____01082;
|
|
var 1..12: j1____01090;
|
|
var 1..12: j1____01098;
|
|
var 1..12: j1____01106;
|
|
var 1..12: j1____01114;
|
|
var 1..12: j1____01122;
|
|
var 1..12: j1____01130;
|
|
var 1..12: j1____01138;
|
|
var 1..12: j2____00004;
|
|
var 1..12: j2____00012;
|
|
var 1..12: j2____00020;
|
|
var 1..12: j2____00028;
|
|
var 1..12: j2____00036;
|
|
var 1..12: j2____00044;
|
|
var 1..12: j2____00052;
|
|
var 1..12: j2____00060;
|
|
var 1..12: j2____00068;
|
|
var 1..12: j2____00076;
|
|
var 1..12: j2____00084;
|
|
var 1..12: j2____00092;
|
|
var 1..12: j2____00100;
|
|
var 1..12: j2____00108;
|
|
var 1..12: j2____00116;
|
|
var 1..12: j2____00124;
|
|
var 1..12: j2____00132;
|
|
var 1..12: j2____00140;
|
|
var 1..12: j2____00148;
|
|
var 1..12: j2____00156;
|
|
var 1..12: j2____00164;
|
|
var 1..12: j2____00172;
|
|
var 1..12: j2____00180;
|
|
var 1..12: j2____00188;
|
|
var 1..12: j2____00196;
|
|
var 1..12: j2____00204;
|
|
var 1..12: j2____00212;
|
|
var 1..12: j2____00220;
|
|
var 1..12: j2____00228;
|
|
var 1..12: j2____00236;
|
|
var 1..12: j2____00244;
|
|
var 1..12: j2____00252;
|
|
var 1..12: j2____00260;
|
|
var 1..12: j2____00268;
|
|
var 1..12: j2____00276;
|
|
var 1..12: j2____00284;
|
|
var 1..12: j2____00292;
|
|
var 1..12: j2____00300;
|
|
var 1..12: j2____00308;
|
|
var 1..12: j2____00316;
|
|
var 1..12: j2____00324;
|
|
var 1..12: j2____00332;
|
|
var 1..12: j2____00340;
|
|
var 1..12: j2____00348;
|
|
var 1..12: j2____00356;
|
|
var 1..12: j2____00364;
|
|
var 1..12: j2____00372;
|
|
var 1..12: j2____00380;
|
|
var 1..12: j2____00388;
|
|
var 1..12: j2____00396;
|
|
var 1..12: j2____00404;
|
|
var 1..12: j2____00412;
|
|
var 1..12: j2____00420;
|
|
var 1..12: j2____00428;
|
|
var 1..12: j2____00436;
|
|
var 1..12: j2____00444;
|
|
var 1..12: j2____00452;
|
|
var 1..12: j2____00460;
|
|
var 1..12: j2____00468;
|
|
var 1..12: j2____00476;
|
|
var 1..12: j2____00484;
|
|
var 1..12: j2____00492;
|
|
var 1..12: j2____00500;
|
|
var 1..12: j2____00508;
|
|
var 1..12: j2____00516;
|
|
var 1..12: j2____00524;
|
|
var 1..12: j2____00532;
|
|
var 1..12: j2____00540;
|
|
var 1..12: j2____00548;
|
|
var 1..12: j2____00556;
|
|
var 1..12: j2____00564;
|
|
var 1..12: j2____00572;
|
|
var 1..12: j2____00580;
|
|
var 1..12: j2____00588;
|
|
var 1..12: j2____00596;
|
|
var 1..12: j2____00604;
|
|
var 1..12: j2____00612;
|
|
var 1..12: j2____00620;
|
|
var 1..12: j2____00628;
|
|
var 1..12: j2____00636;
|
|
var 1..12: j2____00644;
|
|
var 1..12: j2____00652;
|
|
var 1..12: j2____00660;
|
|
var 1..12: j2____00668;
|
|
var 1..12: j2____00676;
|
|
var 1..12: j2____00684;
|
|
var 1..12: j2____00692;
|
|
var 1..12: j2____00700;
|
|
var 1..12: j2____00708;
|
|
var 1..12: j2____00716;
|
|
var 1..12: j2____00724;
|
|
var 1..12: j2____00732;
|
|
var 1..12: j2____00740;
|
|
var 1..12: j2____00748;
|
|
var 1..12: j2____00756;
|
|
var 1..12: j2____00764;
|
|
var 1..12: j2____00772;
|
|
var 1..12: j2____00780;
|
|
var 1..12: j2____00788;
|
|
var 1..12: j2____00796;
|
|
var 1..12: j2____00804;
|
|
var 1..12: j2____00812;
|
|
var 1..12: j2____00820;
|
|
var 1..12: j2____00828;
|
|
var 1..12: j2____00836;
|
|
var 1..12: j2____00844;
|
|
var 1..12: j2____00852;
|
|
var 1..12: j2____00860;
|
|
var 1..12: j2____00868;
|
|
var 1..12: j2____00876;
|
|
var 1..12: j2____00884;
|
|
var 1..12: j2____00892;
|
|
var 1..12: j2____00900;
|
|
var 1..12: j2____00908;
|
|
var 1..12: j2____00916;
|
|
var 1..12: j2____00924;
|
|
var 1..12: j2____00932;
|
|
var 1..12: j2____00940;
|
|
var 1..12: j2____00948;
|
|
var 1..12: j2____00956;
|
|
var 1..12: j2____00964;
|
|
var 1..12: j2____00972;
|
|
var 1..12: j2____00980;
|
|
var 1..12: j2____00988;
|
|
var 1..12: j2____00996;
|
|
var 1..12: j2____01004;
|
|
var 1..12: j2____01012;
|
|
var 1..12: j2____01020;
|
|
var 1..12: j2____01028;
|
|
var 1..12: j2____01036;
|
|
var 1..12: j2____01044;
|
|
var 1..12: j2____01052;
|
|
var 1..12: j2____01060;
|
|
var 1..12: j2____01068;
|
|
var 1..12: j2____01076;
|
|
var 1..12: j2____01084;
|
|
var 1..12: j2____01092;
|
|
var 1..12: j2____01100;
|
|
var 1..12: j2____01108;
|
|
var 1..12: j2____01116;
|
|
var 1..12: j2____01124;
|
|
var 1..12: j2____01132;
|
|
var 1..12: j2____01140;
|
|
array [1..144] of var 1..144: x :: output_array([1..12, 1..12]);
|
|
constraint fzn_all_different_int([x[1], x[2], x[3], x[4], x[5], x[6], x[7], x[8], x[9], x[10], x[11], x[12], x[13], x[14], x[15], x[16], x[17], x[18], x[19], x[20], x[21], x[22], x[23], x[24], x[25], x[26], x[27], x[28], x[29], x[30], x[31], x[32], x[33], x[34], x[35], x[36], x[37], x[38], x[39], x[40], x[41], x[42], x[43], x[44], x[45], x[46], x[47], x[48], x[49], x[50], x[51], x[52], x[53], x[54], x[55], x[56], x[57], x[58], x[59], x[60], x[61], x[62], x[63], x[64], x[65], x[66], x[67], x[68], x[69], x[70], x[71], x[72], x[73], x[74], x[75], x[76], x[77], x[78], x[79], x[80], x[81], x[82], x[83], x[84], x[85], x[86], x[87], x[88], x[89], x[90], x[91], x[92], x[93], x[94], x[95], x[96], x[97], x[98], x[99], x[100], x[101], x[102], x[103], x[104], x[105], x[106], x[107], x[108], x[109], x[110], x[111], x[112], x[113], x[114], x[115], x[116], x[117], x[118], x[119], x[120], x[121], x[122], x[123], x[124], x[125], x[126], x[127], x[128], x[129], x[130], x[131], x[132], x[133], x[134], x[135], x[136], x[137], x[138], x[139], x[140], x[141], x[142], x[143], x[144]]);
|
|
constraint array_var_int_element(INT____00005, x, 1);
|
|
constraint array_var_int_element(INT____00007, x, 2);
|
|
constraint array_var_int_element(INT____00013, x, 2);
|
|
constraint array_var_int_element(INT____00015, x, 3);
|
|
constraint array_var_int_element(INT____00021, x, 3);
|
|
constraint array_var_int_element(INT____00023, x, 4);
|
|
constraint array_var_int_element(INT____00029, x, 4);
|
|
constraint array_var_int_element(INT____00031, x, 5);
|
|
constraint array_var_int_element(INT____00037, x, 5);
|
|
constraint array_var_int_element(INT____00039, x, 6);
|
|
constraint array_var_int_element(INT____00045, x, 6);
|
|
constraint array_var_int_element(INT____00047, x, 7);
|
|
constraint array_var_int_element(INT____00053, x, 7);
|
|
constraint array_var_int_element(INT____00055, x, 8);
|
|
constraint array_var_int_element(INT____00061, x, 8);
|
|
constraint array_var_int_element(INT____00063, x, 9);
|
|
constraint array_var_int_element(INT____00069, x, 9);
|
|
constraint array_var_int_element(INT____00071, x, 10);
|
|
constraint array_var_int_element(INT____00077, x, 10);
|
|
constraint array_var_int_element(INT____00079, x, 11);
|
|
constraint array_var_int_element(INT____00085, x, 11);
|
|
constraint array_var_int_element(INT____00087, x, 12);
|
|
constraint array_var_int_element(INT____00093, x, 12);
|
|
constraint array_var_int_element(INT____00095, x, 13);
|
|
constraint array_var_int_element(INT____00101, x, 13);
|
|
constraint array_var_int_element(INT____00103, x, 14);
|
|
constraint array_var_int_element(INT____00109, x, 14);
|
|
constraint array_var_int_element(INT____00111, x, 15);
|
|
constraint array_var_int_element(INT____00117, x, 15);
|
|
constraint array_var_int_element(INT____00119, x, 16);
|
|
constraint array_var_int_element(INT____00125, x, 16);
|
|
constraint array_var_int_element(INT____00127, x, 17);
|
|
constraint array_var_int_element(INT____00133, x, 17);
|
|
constraint array_var_int_element(INT____00135, x, 18);
|
|
constraint array_var_int_element(INT____00141, x, 18);
|
|
constraint array_var_int_element(INT____00143, x, 19);
|
|
constraint array_var_int_element(INT____00149, x, 19);
|
|
constraint array_var_int_element(INT____00151, x, 20);
|
|
constraint array_var_int_element(INT____00157, x, 20);
|
|
constraint array_var_int_element(INT____00159, x, 21);
|
|
constraint array_var_int_element(INT____00165, x, 21);
|
|
constraint array_var_int_element(INT____00167, x, 22);
|
|
constraint array_var_int_element(INT____00173, x, 22);
|
|
constraint array_var_int_element(INT____00175, x, 23);
|
|
constraint array_var_int_element(INT____00181, x, 23);
|
|
constraint array_var_int_element(INT____00183, x, 24);
|
|
constraint array_var_int_element(INT____00189, x, 24);
|
|
constraint array_var_int_element(INT____00191, x, 25);
|
|
constraint array_var_int_element(INT____00197, x, 25);
|
|
constraint array_var_int_element(INT____00199, x, 26);
|
|
constraint array_var_int_element(INT____00205, x, 26);
|
|
constraint array_var_int_element(INT____00207, x, 27);
|
|
constraint array_var_int_element(INT____00213, x, 27);
|
|
constraint array_var_int_element(INT____00215, x, 28);
|
|
constraint array_var_int_element(INT____00221, x, 28);
|
|
constraint array_var_int_element(INT____00223, x, 29);
|
|
constraint array_var_int_element(INT____00229, x, 29);
|
|
constraint array_var_int_element(INT____00231, x, 30);
|
|
constraint array_var_int_element(INT____00237, x, 30);
|
|
constraint array_var_int_element(INT____00239, x, 31);
|
|
constraint array_var_int_element(INT____00245, x, 31);
|
|
constraint array_var_int_element(INT____00247, x, 32);
|
|
constraint array_var_int_element(INT____00253, x, 32);
|
|
constraint array_var_int_element(INT____00255, x, 33);
|
|
constraint array_var_int_element(INT____00261, x, 33);
|
|
constraint array_var_int_element(INT____00263, x, 34);
|
|
constraint array_var_int_element(INT____00269, x, 34);
|
|
constraint array_var_int_element(INT____00271, x, 35);
|
|
constraint array_var_int_element(INT____00277, x, 35);
|
|
constraint array_var_int_element(INT____00279, x, 36);
|
|
constraint array_var_int_element(INT____00285, x, 36);
|
|
constraint array_var_int_element(INT____00287, x, 37);
|
|
constraint array_var_int_element(INT____00293, x, 37);
|
|
constraint array_var_int_element(INT____00295, x, 38);
|
|
constraint array_var_int_element(INT____00301, x, 38);
|
|
constraint array_var_int_element(INT____00303, x, 39);
|
|
constraint array_var_int_element(INT____00309, x, 39);
|
|
constraint array_var_int_element(INT____00311, x, 40);
|
|
constraint array_var_int_element(INT____00317, x, 40);
|
|
constraint array_var_int_element(INT____00319, x, 41);
|
|
constraint array_var_int_element(INT____00325, x, 41);
|
|
constraint array_var_int_element(INT____00327, x, 42);
|
|
constraint array_var_int_element(INT____00333, x, 42);
|
|
constraint array_var_int_element(INT____00335, x, 43);
|
|
constraint array_var_int_element(INT____00341, x, 43);
|
|
constraint array_var_int_element(INT____00343, x, 44);
|
|
constraint array_var_int_element(INT____00349, x, 44);
|
|
constraint array_var_int_element(INT____00351, x, 45);
|
|
constraint array_var_int_element(INT____00357, x, 45);
|
|
constraint array_var_int_element(INT____00359, x, 46);
|
|
constraint array_var_int_element(INT____00365, x, 46);
|
|
constraint array_var_int_element(INT____00367, x, 47);
|
|
constraint array_var_int_element(INT____00373, x, 47);
|
|
constraint array_var_int_element(INT____00375, x, 48);
|
|
constraint array_var_int_element(INT____00381, x, 48);
|
|
constraint array_var_int_element(INT____00383, x, 49);
|
|
constraint array_var_int_element(INT____00389, x, 49);
|
|
constraint array_var_int_element(INT____00391, x, 50);
|
|
constraint array_var_int_element(INT____00397, x, 50);
|
|
constraint array_var_int_element(INT____00399, x, 51);
|
|
constraint array_var_int_element(INT____00405, x, 51);
|
|
constraint array_var_int_element(INT____00407, x, 52);
|
|
constraint array_var_int_element(INT____00413, x, 52);
|
|
constraint array_var_int_element(INT____00415, x, 53);
|
|
constraint array_var_int_element(INT____00421, x, 53);
|
|
constraint array_var_int_element(INT____00423, x, 54);
|
|
constraint array_var_int_element(INT____00429, x, 54);
|
|
constraint array_var_int_element(INT____00431, x, 55);
|
|
constraint array_var_int_element(INT____00437, x, 55);
|
|
constraint array_var_int_element(INT____00439, x, 56);
|
|
constraint array_var_int_element(INT____00445, x, 56);
|
|
constraint array_var_int_element(INT____00447, x, 57);
|
|
constraint array_var_int_element(INT____00453, x, 57);
|
|
constraint array_var_int_element(INT____00455, x, 58);
|
|
constraint array_var_int_element(INT____00461, x, 58);
|
|
constraint array_var_int_element(INT____00463, x, 59);
|
|
constraint array_var_int_element(INT____00469, x, 59);
|
|
constraint array_var_int_element(INT____00471, x, 60);
|
|
constraint array_var_int_element(INT____00477, x, 60);
|
|
constraint array_var_int_element(INT____00479, x, 61);
|
|
constraint array_var_int_element(INT____00485, x, 61);
|
|
constraint array_var_int_element(INT____00487, x, 62);
|
|
constraint array_var_int_element(INT____00493, x, 62);
|
|
constraint array_var_int_element(INT____00495, x, 63);
|
|
constraint array_var_int_element(INT____00501, x, 63);
|
|
constraint array_var_int_element(INT____00503, x, 64);
|
|
constraint array_var_int_element(INT____00509, x, 64);
|
|
constraint array_var_int_element(INT____00511, x, 65);
|
|
constraint array_var_int_element(INT____00517, x, 65);
|
|
constraint array_var_int_element(INT____00519, x, 66);
|
|
constraint array_var_int_element(INT____00525, x, 66);
|
|
constraint array_var_int_element(INT____00527, x, 67);
|
|
constraint array_var_int_element(INT____00533, x, 67);
|
|
constraint array_var_int_element(INT____00535, x, 68);
|
|
constraint array_var_int_element(INT____00541, x, 68);
|
|
constraint array_var_int_element(INT____00543, x, 69);
|
|
constraint array_var_int_element(INT____00549, x, 69);
|
|
constraint array_var_int_element(INT____00551, x, 70);
|
|
constraint array_var_int_element(INT____00557, x, 70);
|
|
constraint array_var_int_element(INT____00559, x, 71);
|
|
constraint array_var_int_element(INT____00565, x, 71);
|
|
constraint array_var_int_element(INT____00567, x, 72);
|
|
constraint array_var_int_element(INT____00573, x, 72);
|
|
constraint array_var_int_element(INT____00575, x, 73);
|
|
constraint array_var_int_element(INT____00581, x, 73);
|
|
constraint array_var_int_element(INT____00583, x, 74);
|
|
constraint array_var_int_element(INT____00589, x, 74);
|
|
constraint array_var_int_element(INT____00591, x, 75);
|
|
constraint array_var_int_element(INT____00597, x, 75);
|
|
constraint array_var_int_element(INT____00599, x, 76);
|
|
constraint array_var_int_element(INT____00605, x, 76);
|
|
constraint array_var_int_element(INT____00607, x, 77);
|
|
constraint array_var_int_element(INT____00613, x, 77);
|
|
constraint array_var_int_element(INT____00615, x, 78);
|
|
constraint array_var_int_element(INT____00621, x, 78);
|
|
constraint array_var_int_element(INT____00623, x, 79);
|
|
constraint array_var_int_element(INT____00629, x, 79);
|
|
constraint array_var_int_element(INT____00631, x, 80);
|
|
constraint array_var_int_element(INT____00637, x, 80);
|
|
constraint array_var_int_element(INT____00639, x, 81);
|
|
constraint array_var_int_element(INT____00645, x, 81);
|
|
constraint array_var_int_element(INT____00647, x, 82);
|
|
constraint array_var_int_element(INT____00653, x, 82);
|
|
constraint array_var_int_element(INT____00655, x, 83);
|
|
constraint array_var_int_element(INT____00661, x, 83);
|
|
constraint array_var_int_element(INT____00663, x, 84);
|
|
constraint array_var_int_element(INT____00669, x, 84);
|
|
constraint array_var_int_element(INT____00671, x, 85);
|
|
constraint array_var_int_element(INT____00677, x, 85);
|
|
constraint array_var_int_element(INT____00679, x, 86);
|
|
constraint array_var_int_element(INT____00685, x, 86);
|
|
constraint array_var_int_element(INT____00687, x, 87);
|
|
constraint array_var_int_element(INT____00693, x, 87);
|
|
constraint array_var_int_element(INT____00695, x, 88);
|
|
constraint array_var_int_element(INT____00701, x, 88);
|
|
constraint array_var_int_element(INT____00703, x, 89);
|
|
constraint array_var_int_element(INT____00709, x, 89);
|
|
constraint array_var_int_element(INT____00711, x, 90);
|
|
constraint array_var_int_element(INT____00717, x, 90);
|
|
constraint array_var_int_element(INT____00719, x, 91);
|
|
constraint array_var_int_element(INT____00725, x, 91);
|
|
constraint array_var_int_element(INT____00727, x, 92);
|
|
constraint array_var_int_element(INT____00733, x, 92);
|
|
constraint array_var_int_element(INT____00735, x, 93);
|
|
constraint array_var_int_element(INT____00741, x, 93);
|
|
constraint array_var_int_element(INT____00743, x, 94);
|
|
constraint array_var_int_element(INT____00749, x, 94);
|
|
constraint array_var_int_element(INT____00751, x, 95);
|
|
constraint array_var_int_element(INT____00757, x, 95);
|
|
constraint array_var_int_element(INT____00759, x, 96);
|
|
constraint array_var_int_element(INT____00765, x, 96);
|
|
constraint array_var_int_element(INT____00767, x, 97);
|
|
constraint array_var_int_element(INT____00773, x, 97);
|
|
constraint array_var_int_element(INT____00775, x, 98);
|
|
constraint array_var_int_element(INT____00781, x, 98);
|
|
constraint array_var_int_element(INT____00783, x, 99);
|
|
constraint array_var_int_element(INT____00789, x, 99);
|
|
constraint array_var_int_element(INT____00791, x, 100);
|
|
constraint array_var_int_element(INT____00797, x, 100);
|
|
constraint array_var_int_element(INT____00799, x, 101);
|
|
constraint array_var_int_element(INT____00805, x, 101);
|
|
constraint array_var_int_element(INT____00807, x, 102);
|
|
constraint array_var_int_element(INT____00813, x, 102);
|
|
constraint array_var_int_element(INT____00815, x, 103);
|
|
constraint array_var_int_element(INT____00821, x, 103);
|
|
constraint array_var_int_element(INT____00823, x, 104);
|
|
constraint array_var_int_element(INT____00829, x, 104);
|
|
constraint array_var_int_element(INT____00831, x, 105);
|
|
constraint array_var_int_element(INT____00837, x, 105);
|
|
constraint array_var_int_element(INT____00839, x, 106);
|
|
constraint array_var_int_element(INT____00845, x, 106);
|
|
constraint array_var_int_element(INT____00847, x, 107);
|
|
constraint array_var_int_element(INT____00853, x, 107);
|
|
constraint array_var_int_element(INT____00855, x, 108);
|
|
constraint array_var_int_element(INT____00861, x, 108);
|
|
constraint array_var_int_element(INT____00863, x, 109);
|
|
constraint array_var_int_element(INT____00869, x, 109);
|
|
constraint array_var_int_element(INT____00871, x, 110);
|
|
constraint array_var_int_element(INT____00877, x, 110);
|
|
constraint array_var_int_element(INT____00879, x, 111);
|
|
constraint array_var_int_element(INT____00885, x, 111);
|
|
constraint array_var_int_element(INT____00887, x, 112);
|
|
constraint array_var_int_element(INT____00893, x, 112);
|
|
constraint array_var_int_element(INT____00895, x, 113);
|
|
constraint array_var_int_element(INT____00901, x, 113);
|
|
constraint array_var_int_element(INT____00903, x, 114);
|
|
constraint array_var_int_element(INT____00909, x, 114);
|
|
constraint array_var_int_element(INT____00911, x, 115);
|
|
constraint array_var_int_element(INT____00917, x, 115);
|
|
constraint array_var_int_element(INT____00919, x, 116);
|
|
constraint array_var_int_element(INT____00925, x, 116);
|
|
constraint array_var_int_element(INT____00927, x, 117);
|
|
constraint array_var_int_element(INT____00933, x, 117);
|
|
constraint array_var_int_element(INT____00935, x, 118);
|
|
constraint array_var_int_element(INT____00941, x, 118);
|
|
constraint array_var_int_element(INT____00943, x, 119);
|
|
constraint array_var_int_element(INT____00949, x, 119);
|
|
constraint array_var_int_element(INT____00951, x, 120);
|
|
constraint array_var_int_element(INT____00957, x, 120);
|
|
constraint array_var_int_element(INT____00959, x, 121);
|
|
constraint array_var_int_element(INT____00965, x, 121);
|
|
constraint array_var_int_element(INT____00967, x, 122);
|
|
constraint array_var_int_element(INT____00973, x, 122);
|
|
constraint array_var_int_element(INT____00975, x, 123);
|
|
constraint array_var_int_element(INT____00981, x, 123);
|
|
constraint array_var_int_element(INT____00983, x, 124);
|
|
constraint array_var_int_element(INT____00989, x, 124);
|
|
constraint array_var_int_element(INT____00991, x, 125);
|
|
constraint array_var_int_element(INT____00997, x, 125);
|
|
constraint array_var_int_element(INT____00999, x, 126);
|
|
constraint array_var_int_element(INT____01005, x, 126);
|
|
constraint array_var_int_element(INT____01007, x, 127);
|
|
constraint array_var_int_element(INT____01013, x, 127);
|
|
constraint array_var_int_element(INT____01015, x, 128);
|
|
constraint array_var_int_element(INT____01021, x, 128);
|
|
constraint array_var_int_element(INT____01023, x, 129);
|
|
constraint array_var_int_element(INT____01029, x, 129);
|
|
constraint array_var_int_element(INT____01031, x, 130);
|
|
constraint array_var_int_element(INT____01037, x, 130);
|
|
constraint array_var_int_element(INT____01039, x, 131);
|
|
constraint array_var_int_element(INT____01045, x, 131);
|
|
constraint array_var_int_element(INT____01047, x, 132);
|
|
constraint array_var_int_element(INT____01053, x, 132);
|
|
constraint array_var_int_element(INT____01055, x, 133);
|
|
constraint array_var_int_element(INT____01061, x, 133);
|
|
constraint array_var_int_element(INT____01063, x, 134);
|
|
constraint array_var_int_element(INT____01069, x, 134);
|
|
constraint array_var_int_element(INT____01071, x, 135);
|
|
constraint array_var_int_element(INT____01077, x, 135);
|
|
constraint array_var_int_element(INT____01079, x, 136);
|
|
constraint array_var_int_element(INT____01085, x, 136);
|
|
constraint array_var_int_element(INT____01087, x, 137);
|
|
constraint array_var_int_element(INT____01093, x, 137);
|
|
constraint array_var_int_element(INT____01095, x, 138);
|
|
constraint array_var_int_element(INT____01101, x, 138);
|
|
constraint array_var_int_element(INT____01103, x, 139);
|
|
constraint array_var_int_element(INT____01109, x, 139);
|
|
constraint array_var_int_element(INT____01111, x, 140);
|
|
constraint array_var_int_element(INT____01117, x, 140);
|
|
constraint array_var_int_element(INT____01119, x, 141);
|
|
constraint array_var_int_element(INT____01125, x, 141);
|
|
constraint array_var_int_element(INT____01127, x, 142);
|
|
constraint array_var_int_element(INT____01133, x, 142);
|
|
constraint array_var_int_element(INT____01135, x, 143);
|
|
constraint array_var_int_element(INT____01141, x, 143);
|
|
constraint array_var_int_element(INT____01143, x, 144);
|
|
constraint int_eq_reif(x[3], 134, true);
|
|
constraint int_eq_reif(x[4], 2, true);
|
|
constraint int_eq_reif(x[5], 4, true);
|
|
constraint int_eq_reif(x[13], 136, true);
|
|
constraint int_eq_reif(x[16], 1, true);
|
|
constraint int_eq_reif(x[18], 5, true);
|
|
constraint int_eq_reif(x[19], 6, true);
|
|
constraint int_eq_reif(x[20], 10, true);
|
|
constraint int_eq_reif(x[21], 115, true);
|
|
constraint int_eq_reif(x[22], 106, true);
|
|
constraint int_eq_reif(x[25], 139, true);
|
|
constraint int_eq_reif(x[28], 124, true);
|
|
constraint int_eq_reif(x[30], 122, true);
|
|
constraint int_eq_reif(x[31], 117, true);
|
|
constraint int_eq_reif(x[34], 107, true);
|
|
constraint int_eq_reif(x[38], 131, true);
|
|
constraint int_eq_reif(x[39], 126, true);
|
|
constraint int_eq_reif(x[41], 123, true);
|
|
constraint int_eq_reif(x[44], 12, true);
|
|
constraint int_eq_reif(x[48], 103, true);
|
|
constraint int_eq_reif(x[51], 144, true);
|
|
constraint int_eq_reif(x[57], 14, true);
|
|
constraint int_eq_reif(x[59], 99, true);
|
|
constraint int_eq_reif(x[60], 101, true);
|
|
constraint int_eq_reif(x[63], 129, true);
|
|
constraint int_eq_reif(x[65], 23, true);
|
|
constraint int_eq_reif(x[66], 21, true);
|
|
constraint int_eq_reif(x[68], 16, true);
|
|
constraint int_eq_reif(x[69], 65, true);
|
|
constraint int_eq_reif(x[70], 97, true);
|
|
constraint int_eq_reif(x[71], 96, true);
|
|
constraint int_eq_reif(x[73], 30, true);
|
|
constraint int_eq_reif(x[74], 29, true);
|
|
constraint int_eq_reif(x[75], 25, true);
|
|
constraint int_eq_reif(x[78], 19, true);
|
|
constraint int_eq_reif(x[82], 66, true);
|
|
constraint int_eq_reif(x[83], 94, true);
|
|
constraint int_eq_reif(x[85], 32, true);
|
|
constraint int_eq_reif(x[88], 27, true);
|
|
constraint int_eq_reif(x[89], 57, true);
|
|
constraint int_eq_reif(x[90], 59, true);
|
|
constraint int_eq_reif(x[91], 60, true);
|
|
constraint int_eq_reif(x[96], 92, true);
|
|
constraint int_eq_reif(x[98], 40, true);
|
|
constraint int_eq_reif(x[99], 42, true);
|
|
constraint int_eq_reif(x[101], 56, true);
|
|
constraint int_eq_reif(x[102], 58, true);
|
|
constraint int_eq_reif(x[105], 72, true);
|
|
constraint int_eq_reif(x[110], 39, true);
|
|
constraint int_eq_reif(x[115], 78, true);
|
|
constraint int_eq_reif(x[116], 73, true);
|
|
constraint int_eq_reif(x[117], 71, true);
|
|
constraint int_eq_reif(x[118], 85, true);
|
|
constraint int_eq_reif(x[119], 69, true);
|
|
constraint int_eq_reif(x[121], 35, true);
|
|
constraint int_eq_reif(x[124], 46, true);
|
|
constraint int_eq_reif(x[125], 53, true);
|
|
constraint int_eq_reif(x[129], 80, true);
|
|
constraint int_eq_reif(x[130], 84, true);
|
|
constraint int_eq_reif(x[133], 36, true);
|
|
constraint int_eq_reif(x[135], 45, true);
|
|
constraint int_eq_reif(x[138], 52, true);
|
|
constraint int_eq_reif(x[139], 51, true);
|
|
constraint int_eq_reif(x[144], 88, true);
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00005, i1____00001, j1____00002], 12) :: defines_var(INT____00005) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00007, i2____00003, j2____00004], 12) :: defines_var(INT____00007) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00013, i1____00009, j1____00010], 12) :: defines_var(INT____00013) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00015, i2____00011, j2____00012], 12) :: defines_var(INT____00015) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00021, i1____00017, j1____00018], 12) :: defines_var(INT____00021) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00023, i2____00019, j2____00020], 12) :: defines_var(INT____00023) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00029, i1____00025, j1____00026], 12) :: defines_var(INT____00029) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00031, i2____00027, j2____00028], 12) :: defines_var(INT____00031) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00037, i1____00033, j1____00034], 12) :: defines_var(INT____00037) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00039, i2____00035, j2____00036], 12) :: defines_var(INT____00039) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00045, i1____00041, j1____00042], 12) :: defines_var(INT____00045) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00047, i2____00043, j2____00044], 12) :: defines_var(INT____00047) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00053, i1____00049, j1____00050], 12) :: defines_var(INT____00053) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00055, i2____00051, j2____00052], 12) :: defines_var(INT____00055) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00061, i1____00057, j1____00058], 12) :: defines_var(INT____00061) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00063, i2____00059, j2____00060], 12) :: defines_var(INT____00063) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00069, i1____00065, j1____00066], 12) :: defines_var(INT____00069) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00071, i2____00067, j2____00068], 12) :: defines_var(INT____00071) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00077, i1____00073, j1____00074], 12) :: defines_var(INT____00077) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00079, i2____00075, j2____00076], 12) :: defines_var(INT____00079) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00085, i1____00081, j1____00082], 12) :: defines_var(INT____00085) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00087, i2____00083, j2____00084], 12) :: defines_var(INT____00087) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00093, i1____00089, j1____00090], 12) :: defines_var(INT____00093) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00095, i2____00091, j2____00092], 12) :: defines_var(INT____00095) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00101, i1____00097, j1____00098], 12) :: defines_var(INT____00101) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00103, i2____00099, j2____00100], 12) :: defines_var(INT____00103) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00109, i1____00105, j1____00106], 12) :: defines_var(INT____00109) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00111, i2____00107, j2____00108], 12) :: defines_var(INT____00111) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00117, i1____00113, j1____00114], 12) :: defines_var(INT____00117) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00119, i2____00115, j2____00116], 12) :: defines_var(INT____00119) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00125, i1____00121, j1____00122], 12) :: defines_var(INT____00125) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00127, i2____00123, j2____00124], 12) :: defines_var(INT____00127) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00133, i1____00129, j1____00130], 12) :: defines_var(INT____00133) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00135, i2____00131, j2____00132], 12) :: defines_var(INT____00135) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00141, i1____00137, j1____00138], 12) :: defines_var(INT____00141) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00143, i2____00139, j2____00140], 12) :: defines_var(INT____00143) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00149, i1____00145, j1____00146], 12) :: defines_var(INT____00149) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00151, i2____00147, j2____00148], 12) :: defines_var(INT____00151) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00157, i1____00153, j1____00154], 12) :: defines_var(INT____00157) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00159, i2____00155, j2____00156], 12) :: defines_var(INT____00159) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00165, i1____00161, j1____00162], 12) :: defines_var(INT____00165) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00167, i2____00163, j2____00164], 12) :: defines_var(INT____00167) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00173, i1____00169, j1____00170], 12) :: defines_var(INT____00173) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00175, i2____00171, j2____00172], 12) :: defines_var(INT____00175) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00181, i1____00177, j1____00178], 12) :: defines_var(INT____00181) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00183, i2____00179, j2____00180], 12) :: defines_var(INT____00183) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00189, i1____00185, j1____00186], 12) :: defines_var(INT____00189) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00191, i2____00187, j2____00188], 12) :: defines_var(INT____00191) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00197, i1____00193, j1____00194], 12) :: defines_var(INT____00197) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00199, i2____00195, j2____00196], 12) :: defines_var(INT____00199) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00205, i1____00201, j1____00202], 12) :: defines_var(INT____00205) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00207, i2____00203, j2____00204], 12) :: defines_var(INT____00207) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00213, i1____00209, j1____00210], 12) :: defines_var(INT____00213) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00215, i2____00211, j2____00212], 12) :: defines_var(INT____00215) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00221, i1____00217, j1____00218], 12) :: defines_var(INT____00221) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00223, i2____00219, j2____00220], 12) :: defines_var(INT____00223) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00229, i1____00225, j1____00226], 12) :: defines_var(INT____00229) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00231, i2____00227, j2____00228], 12) :: defines_var(INT____00231) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00237, i1____00233, j1____00234], 12) :: defines_var(INT____00237) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00239, i2____00235, j2____00236], 12) :: defines_var(INT____00239) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00245, i1____00241, j1____00242], 12) :: defines_var(INT____00245) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00247, i2____00243, j2____00244], 12) :: defines_var(INT____00247) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00253, i1____00249, j1____00250], 12) :: defines_var(INT____00253) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00255, i2____00251, j2____00252], 12) :: defines_var(INT____00255) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00261, i1____00257, j1____00258], 12) :: defines_var(INT____00261) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00263, i2____00259, j2____00260], 12) :: defines_var(INT____00263) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00269, i1____00265, j1____00266], 12) :: defines_var(INT____00269) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00271, i2____00267, j2____00268], 12) :: defines_var(INT____00271) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00277, i1____00273, j1____00274], 12) :: defines_var(INT____00277) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00279, i2____00275, j2____00276], 12) :: defines_var(INT____00279) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00285, i1____00281, j1____00282], 12) :: defines_var(INT____00285) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00287, i2____00283, j2____00284], 12) :: defines_var(INT____00287) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00293, i1____00289, j1____00290], 12) :: defines_var(INT____00293) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00295, i2____00291, j2____00292], 12) :: defines_var(INT____00295) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00301, i1____00297, j1____00298], 12) :: defines_var(INT____00301) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00303, i2____00299, j2____00300], 12) :: defines_var(INT____00303) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00309, i1____00305, j1____00306], 12) :: defines_var(INT____00309) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00311, i2____00307, j2____00308], 12) :: defines_var(INT____00311) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00317, i1____00313, j1____00314], 12) :: defines_var(INT____00317) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00319, i2____00315, j2____00316], 12) :: defines_var(INT____00319) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00325, i1____00321, j1____00322], 12) :: defines_var(INT____00325) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00327, i2____00323, j2____00324], 12) :: defines_var(INT____00327) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00333, i1____00329, j1____00330], 12) :: defines_var(INT____00333) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00335, i2____00331, j2____00332], 12) :: defines_var(INT____00335) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00341, i1____00337, j1____00338], 12) :: defines_var(INT____00341) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00343, i2____00339, j2____00340], 12) :: defines_var(INT____00343) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00349, i1____00345, j1____00346], 12) :: defines_var(INT____00349) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00351, i2____00347, j2____00348], 12) :: defines_var(INT____00351) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00357, i1____00353, j1____00354], 12) :: defines_var(INT____00357) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00359, i2____00355, j2____00356], 12) :: defines_var(INT____00359) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00365, i1____00361, j1____00362], 12) :: defines_var(INT____00365) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00367, i2____00363, j2____00364], 12) :: defines_var(INT____00367) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00373, i1____00369, j1____00370], 12) :: defines_var(INT____00373) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00375, i2____00371, j2____00372], 12) :: defines_var(INT____00375) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00381, i1____00377, j1____00378], 12) :: defines_var(INT____00381) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00383, i2____00379, j2____00380], 12) :: defines_var(INT____00383) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00389, i1____00385, j1____00386], 12) :: defines_var(INT____00389) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00391, i2____00387, j2____00388], 12) :: defines_var(INT____00391) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00397, i1____00393, j1____00394], 12) :: defines_var(INT____00397) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00399, i2____00395, j2____00396], 12) :: defines_var(INT____00399) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00405, i1____00401, j1____00402], 12) :: defines_var(INT____00405) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00407, i2____00403, j2____00404], 12) :: defines_var(INT____00407) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00413, i1____00409, j1____00410], 12) :: defines_var(INT____00413) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00415, i2____00411, j2____00412], 12) :: defines_var(INT____00415) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00421, i1____00417, j1____00418], 12) :: defines_var(INT____00421) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00423, i2____00419, j2____00420], 12) :: defines_var(INT____00423) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00429, i1____00425, j1____00426], 12) :: defines_var(INT____00429) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00431, i2____00427, j2____00428], 12) :: defines_var(INT____00431) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00437, i1____00433, j1____00434], 12) :: defines_var(INT____00437) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00439, i2____00435, j2____00436], 12) :: defines_var(INT____00439) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00445, i1____00441, j1____00442], 12) :: defines_var(INT____00445) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00447, i2____00443, j2____00444], 12) :: defines_var(INT____00447) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00453, i1____00449, j1____00450], 12) :: defines_var(INT____00453) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00455, i2____00451, j2____00452], 12) :: defines_var(INT____00455) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00461, i1____00457, j1____00458], 12) :: defines_var(INT____00461) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00463, i2____00459, j2____00460], 12) :: defines_var(INT____00463) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00469, i1____00465, j1____00466], 12) :: defines_var(INT____00469) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00471, i2____00467, j2____00468], 12) :: defines_var(INT____00471) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00477, i1____00473, j1____00474], 12) :: defines_var(INT____00477) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00479, i2____00475, j2____00476], 12) :: defines_var(INT____00479) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00485, i1____00481, j1____00482], 12) :: defines_var(INT____00485) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00487, i2____00483, j2____00484], 12) :: defines_var(INT____00487) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00493, i1____00489, j1____00490], 12) :: defines_var(INT____00493) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00495, i2____00491, j2____00492], 12) :: defines_var(INT____00495) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00501, i1____00497, j1____00498], 12) :: defines_var(INT____00501) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00503, i2____00499, j2____00500], 12) :: defines_var(INT____00503) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00509, i1____00505, j1____00506], 12) :: defines_var(INT____00509) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00511, i2____00507, j2____00508], 12) :: defines_var(INT____00511) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00517, i1____00513, j1____00514], 12) :: defines_var(INT____00517) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00519, i2____00515, j2____00516], 12) :: defines_var(INT____00519) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00525, i1____00521, j1____00522], 12) :: defines_var(INT____00525) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00527, i2____00523, j2____00524], 12) :: defines_var(INT____00527) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00533, i1____00529, j1____00530], 12) :: defines_var(INT____00533) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00535, i2____00531, j2____00532], 12) :: defines_var(INT____00535) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00541, i1____00537, j1____00538], 12) :: defines_var(INT____00541) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00543, i2____00539, j2____00540], 12) :: defines_var(INT____00543) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00549, i1____00545, j1____00546], 12) :: defines_var(INT____00549) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00551, i2____00547, j2____00548], 12) :: defines_var(INT____00551) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00557, i1____00553, j1____00554], 12) :: defines_var(INT____00557) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00559, i2____00555, j2____00556], 12) :: defines_var(INT____00559) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00565, i1____00561, j1____00562], 12) :: defines_var(INT____00565) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00567, i2____00563, j2____00564], 12) :: defines_var(INT____00567) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00573, i1____00569, j1____00570], 12) :: defines_var(INT____00573) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00575, i2____00571, j2____00572], 12) :: defines_var(INT____00575) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00581, i1____00577, j1____00578], 12) :: defines_var(INT____00581) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00583, i2____00579, j2____00580], 12) :: defines_var(INT____00583) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00589, i1____00585, j1____00586], 12) :: defines_var(INT____00589) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00591, i2____00587, j2____00588], 12) :: defines_var(INT____00591) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00597, i1____00593, j1____00594], 12) :: defines_var(INT____00597) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00599, i2____00595, j2____00596], 12) :: defines_var(INT____00599) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00605, i1____00601, j1____00602], 12) :: defines_var(INT____00605) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00607, i2____00603, j2____00604], 12) :: defines_var(INT____00607) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00613, i1____00609, j1____00610], 12) :: defines_var(INT____00613) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00615, i2____00611, j2____00612], 12) :: defines_var(INT____00615) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00621, i1____00617, j1____00618], 12) :: defines_var(INT____00621) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00623, i2____00619, j2____00620], 12) :: defines_var(INT____00623) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00629, i1____00625, j1____00626], 12) :: defines_var(INT____00629) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00631, i2____00627, j2____00628], 12) :: defines_var(INT____00631) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00637, i1____00633, j1____00634], 12) :: defines_var(INT____00637) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00639, i2____00635, j2____00636], 12) :: defines_var(INT____00639) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00645, i1____00641, j1____00642], 12) :: defines_var(INT____00645) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00647, i2____00643, j2____00644], 12) :: defines_var(INT____00647) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00653, i1____00649, j1____00650], 12) :: defines_var(INT____00653) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00655, i2____00651, j2____00652], 12) :: defines_var(INT____00655) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00661, i1____00657, j1____00658], 12) :: defines_var(INT____00661) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00663, i2____00659, j2____00660], 12) :: defines_var(INT____00663) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00669, i1____00665, j1____00666], 12) :: defines_var(INT____00669) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00671, i2____00667, j2____00668], 12) :: defines_var(INT____00671) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00677, i1____00673, j1____00674], 12) :: defines_var(INT____00677) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00679, i2____00675, j2____00676], 12) :: defines_var(INT____00679) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00685, i1____00681, j1____00682], 12) :: defines_var(INT____00685) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00687, i2____00683, j2____00684], 12) :: defines_var(INT____00687) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00693, i1____00689, j1____00690], 12) :: defines_var(INT____00693) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00695, i2____00691, j2____00692], 12) :: defines_var(INT____00695) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00701, i1____00697, j1____00698], 12) :: defines_var(INT____00701) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00703, i2____00699, j2____00700], 12) :: defines_var(INT____00703) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00709, i1____00705, j1____00706], 12) :: defines_var(INT____00709) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00711, i2____00707, j2____00708], 12) :: defines_var(INT____00711) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00717, i1____00713, j1____00714], 12) :: defines_var(INT____00717) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00719, i2____00715, j2____00716], 12) :: defines_var(INT____00719) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00725, i1____00721, j1____00722], 12) :: defines_var(INT____00725) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00727, i2____00723, j2____00724], 12) :: defines_var(INT____00727) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00733, i1____00729, j1____00730], 12) :: defines_var(INT____00733) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00735, i2____00731, j2____00732], 12) :: defines_var(INT____00735) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00741, i1____00737, j1____00738], 12) :: defines_var(INT____00741) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00743, i2____00739, j2____00740], 12) :: defines_var(INT____00743) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00749, i1____00745, j1____00746], 12) :: defines_var(INT____00749) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00751, i2____00747, j2____00748], 12) :: defines_var(INT____00751) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00757, i1____00753, j1____00754], 12) :: defines_var(INT____00757) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00759, i2____00755, j2____00756], 12) :: defines_var(INT____00759) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00765, i1____00761, j1____00762], 12) :: defines_var(INT____00765) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00767, i2____00763, j2____00764], 12) :: defines_var(INT____00767) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00773, i1____00769, j1____00770], 12) :: defines_var(INT____00773) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00775, i2____00771, j2____00772], 12) :: defines_var(INT____00775) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00781, i1____00777, j1____00778], 12) :: defines_var(INT____00781) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00783, i2____00779, j2____00780], 12) :: defines_var(INT____00783) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00789, i1____00785, j1____00786], 12) :: defines_var(INT____00789) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00791, i2____00787, j2____00788], 12) :: defines_var(INT____00791) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00797, i1____00793, j1____00794], 12) :: defines_var(INT____00797) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00799, i2____00795, j2____00796], 12) :: defines_var(INT____00799) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00805, i1____00801, j1____00802], 12) :: defines_var(INT____00805) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00807, i2____00803, j2____00804], 12) :: defines_var(INT____00807) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00813, i1____00809, j1____00810], 12) :: defines_var(INT____00813) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00815, i2____00811, j2____00812], 12) :: defines_var(INT____00815) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00821, i1____00817, j1____00818], 12) :: defines_var(INT____00821) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00823, i2____00819, j2____00820], 12) :: defines_var(INT____00823) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00829, i1____00825, j1____00826], 12) :: defines_var(INT____00829) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00831, i2____00827, j2____00828], 12) :: defines_var(INT____00831) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00837, i1____00833, j1____00834], 12) :: defines_var(INT____00837) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00839, i2____00835, j2____00836], 12) :: defines_var(INT____00839) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00845, i1____00841, j1____00842], 12) :: defines_var(INT____00845) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00847, i2____00843, j2____00844], 12) :: defines_var(INT____00847) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00853, i1____00849, j1____00850], 12) :: defines_var(INT____00853) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00855, i2____00851, j2____00852], 12) :: defines_var(INT____00855) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00861, i1____00857, j1____00858], 12) :: defines_var(INT____00861) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00863, i2____00859, j2____00860], 12) :: defines_var(INT____00863) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00869, i1____00865, j1____00866], 12) :: defines_var(INT____00869) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00871, i2____00867, j2____00868], 12) :: defines_var(INT____00871) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00877, i1____00873, j1____00874], 12) :: defines_var(INT____00877) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00879, i2____00875, j2____00876], 12) :: defines_var(INT____00879) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00885, i1____00881, j1____00882], 12) :: defines_var(INT____00885) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00887, i2____00883, j2____00884], 12) :: defines_var(INT____00887) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00893, i1____00889, j1____00890], 12) :: defines_var(INT____00893) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00895, i2____00891, j2____00892], 12) :: defines_var(INT____00895) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00901, i1____00897, j1____00898], 12) :: defines_var(INT____00901) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00903, i2____00899, j2____00900], 12) :: defines_var(INT____00903) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00909, i1____00905, j1____00906], 12) :: defines_var(INT____00909) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00911, i2____00907, j2____00908], 12) :: defines_var(INT____00911) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00917, i1____00913, j1____00914], 12) :: defines_var(INT____00917) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00919, i2____00915, j2____00916], 12) :: defines_var(INT____00919) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00925, i1____00921, j1____00922], 12) :: defines_var(INT____00925) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00927, i2____00923, j2____00924], 12) :: defines_var(INT____00927) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00933, i1____00929, j1____00930], 12) :: defines_var(INT____00933) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00935, i2____00931, j2____00932], 12) :: defines_var(INT____00935) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00941, i1____00937, j1____00938], 12) :: defines_var(INT____00941) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00943, i2____00939, j2____00940], 12) :: defines_var(INT____00943) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00949, i1____00945, j1____00946], 12) :: defines_var(INT____00949) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00951, i2____00947, j2____00948], 12) :: defines_var(INT____00951) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00957, i1____00953, j1____00954], 12) :: defines_var(INT____00957) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00959, i2____00955, j2____00956], 12) :: defines_var(INT____00959) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00965, i1____00961, j1____00962], 12) :: defines_var(INT____00965) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00967, i2____00963, j2____00964], 12) :: defines_var(INT____00967) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00973, i1____00969, j1____00970], 12) :: defines_var(INT____00973) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00975, i2____00971, j2____00972], 12) :: defines_var(INT____00975) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00981, i1____00977, j1____00978], 12) :: defines_var(INT____00981) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00983, i2____00979, j2____00980], 12) :: defines_var(INT____00983) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00989, i1____00985, j1____00986], 12) :: defines_var(INT____00989) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00991, i2____00987, j2____00988], 12) :: defines_var(INT____00991) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00997, i1____00993, j1____00994], 12) :: defines_var(INT____00997) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____00999, i2____00995, j2____00996], 12) :: defines_var(INT____00999) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____01005, i1____01001, j1____01002], 12) :: defines_var(INT____01005) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____01007, i2____01003, j2____01004], 12) :: defines_var(INT____01007) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____01013, i1____01009, j1____01010], 12) :: defines_var(INT____01013) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____01015, i2____01011, j2____01012], 12) :: defines_var(INT____01015) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____01021, i1____01017, j1____01018], 12) :: defines_var(INT____01021) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____01023, i2____01019, j2____01020], 12) :: defines_var(INT____01023) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____01029, i1____01025, j1____01026], 12) :: defines_var(INT____01029) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____01031, i2____01027, j2____01028], 12) :: defines_var(INT____01031) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____01037, i1____01033, j1____01034], 12) :: defines_var(INT____01037) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____01039, i2____01035, j2____01036], 12) :: defines_var(INT____01039) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____01045, i1____01041, j1____01042], 12) :: defines_var(INT____01045) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____01047, i2____01043, j2____01044], 12) :: defines_var(INT____01047) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____01053, i1____01049, j1____01050], 12) :: defines_var(INT____01053) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____01055, i2____01051, j2____01052], 12) :: defines_var(INT____01055) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____01061, i1____01057, j1____01058], 12) :: defines_var(INT____01061) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____01063, i2____01059, j2____01060], 12) :: defines_var(INT____01063) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____01069, i1____01065, j1____01066], 12) :: defines_var(INT____01069) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____01071, i2____01067, j2____01068], 12) :: defines_var(INT____01071) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____01077, i1____01073, j1____01074], 12) :: defines_var(INT____01077) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____01079, i2____01075, j2____01076], 12) :: defines_var(INT____01079) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____01085, i1____01081, j1____01082], 12) :: defines_var(INT____01085) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____01087, i2____01083, j2____01084], 12) :: defines_var(INT____01087) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____01093, i1____01089, j1____01090], 12) :: defines_var(INT____01093) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____01095, i2____01091, j2____01092], 12) :: defines_var(INT____01095) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____01101, i1____01097, j1____01098], 12) :: defines_var(INT____01101) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____01103, i2____01099, j2____01100], 12) :: defines_var(INT____01103) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____01109, i1____01105, j1____01106], 12) :: defines_var(INT____01109) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____01111, i2____01107, j2____01108], 12) :: defines_var(INT____01111) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____01117, i1____01113, j1____01114], 12) :: defines_var(INT____01117) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____01119, i2____01115, j2____01116], 12) :: defines_var(INT____01119) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____01125, i1____01121, j1____01122], 12) :: defines_var(INT____01125) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____01127, i2____01123, j2____01124], 12) :: defines_var(INT____01127) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____01133, i1____01129, j1____01130], 12) :: defines_var(INT____01133) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____01135, i2____01131, j2____01132], 12) :: defines_var(INT____01135) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____01141, i1____01137, j1____01138], 12) :: defines_var(INT____01141) :: domain;
|
|
constraint int_lin_eq([-1, 12, 1], [INT____01143, i2____01139, j2____01140], 12) :: defines_var(INT____01143) :: domain;
|
|
constraint table_int([i1____00001, j1____00002, i2____00003, j2____00004], valid_connections2);
|
|
constraint table_int([i1____00009, j1____00010, i2____00011, j2____00012], valid_connections2);
|
|
constraint table_int([i1____00017, j1____00018, i2____00019, j2____00020], valid_connections2);
|
|
constraint table_int([i1____00025, j1____00026, i2____00027, j2____00028], valid_connections2);
|
|
constraint table_int([i1____00033, j1____00034, i2____00035, j2____00036], valid_connections2);
|
|
constraint table_int([i1____00041, j1____00042, i2____00043, j2____00044], valid_connections2);
|
|
constraint table_int([i1____00049, j1____00050, i2____00051, j2____00052], valid_connections2);
|
|
constraint table_int([i1____00057, j1____00058, i2____00059, j2____00060], valid_connections2);
|
|
constraint table_int([i1____00065, j1____00066, i2____00067, j2____00068], valid_connections2);
|
|
constraint table_int([i1____00073, j1____00074, i2____00075, j2____00076], valid_connections2);
|
|
constraint table_int([i1____00081, j1____00082, i2____00083, j2____00084], valid_connections2);
|
|
constraint table_int([i1____00089, j1____00090, i2____00091, j2____00092], valid_connections2);
|
|
constraint table_int([i1____00097, j1____00098, i2____00099, j2____00100], valid_connections2);
|
|
constraint table_int([i1____00105, j1____00106, i2____00107, j2____00108], valid_connections2);
|
|
constraint table_int([i1____00113, j1____00114, i2____00115, j2____00116], valid_connections2);
|
|
constraint table_int([i1____00121, j1____00122, i2____00123, j2____00124], valid_connections2);
|
|
constraint table_int([i1____00129, j1____00130, i2____00131, j2____00132], valid_connections2);
|
|
constraint table_int([i1____00137, j1____00138, i2____00139, j2____00140], valid_connections2);
|
|
constraint table_int([i1____00145, j1____00146, i2____00147, j2____00148], valid_connections2);
|
|
constraint table_int([i1____00153, j1____00154, i2____00155, j2____00156], valid_connections2);
|
|
constraint table_int([i1____00161, j1____00162, i2____00163, j2____00164], valid_connections2);
|
|
constraint table_int([i1____00169, j1____00170, i2____00171, j2____00172], valid_connections2);
|
|
constraint table_int([i1____00177, j1____00178, i2____00179, j2____00180], valid_connections2);
|
|
constraint table_int([i1____00185, j1____00186, i2____00187, j2____00188], valid_connections2);
|
|
constraint table_int([i1____00193, j1____00194, i2____00195, j2____00196], valid_connections2);
|
|
constraint table_int([i1____00201, j1____00202, i2____00203, j2____00204], valid_connections2);
|
|
constraint table_int([i1____00209, j1____00210, i2____00211, j2____00212], valid_connections2);
|
|
constraint table_int([i1____00217, j1____00218, i2____00219, j2____00220], valid_connections2);
|
|
constraint table_int([i1____00225, j1____00226, i2____00227, j2____00228], valid_connections2);
|
|
constraint table_int([i1____00233, j1____00234, i2____00235, j2____00236], valid_connections2);
|
|
constraint table_int([i1____00241, j1____00242, i2____00243, j2____00244], valid_connections2);
|
|
constraint table_int([i1____00249, j1____00250, i2____00251, j2____00252], valid_connections2);
|
|
constraint table_int([i1____00257, j1____00258, i2____00259, j2____00260], valid_connections2);
|
|
constraint table_int([i1____00265, j1____00266, i2____00267, j2____00268], valid_connections2);
|
|
constraint table_int([i1____00273, j1____00274, i2____00275, j2____00276], valid_connections2);
|
|
constraint table_int([i1____00281, j1____00282, i2____00283, j2____00284], valid_connections2);
|
|
constraint table_int([i1____00289, j1____00290, i2____00291, j2____00292], valid_connections2);
|
|
constraint table_int([i1____00297, j1____00298, i2____00299, j2____00300], valid_connections2);
|
|
constraint table_int([i1____00305, j1____00306, i2____00307, j2____00308], valid_connections2);
|
|
constraint table_int([i1____00313, j1____00314, i2____00315, j2____00316], valid_connections2);
|
|
constraint table_int([i1____00321, j1____00322, i2____00323, j2____00324], valid_connections2);
|
|
constraint table_int([i1____00329, j1____00330, i2____00331, j2____00332], valid_connections2);
|
|
constraint table_int([i1____00337, j1____00338, i2____00339, j2____00340], valid_connections2);
|
|
constraint table_int([i1____00345, j1____00346, i2____00347, j2____00348], valid_connections2);
|
|
constraint table_int([i1____00353, j1____00354, i2____00355, j2____00356], valid_connections2);
|
|
constraint table_int([i1____00361, j1____00362, i2____00363, j2____00364], valid_connections2);
|
|
constraint table_int([i1____00369, j1____00370, i2____00371, j2____00372], valid_connections2);
|
|
constraint table_int([i1____00377, j1____00378, i2____00379, j2____00380], valid_connections2);
|
|
constraint table_int([i1____00385, j1____00386, i2____00387, j2____00388], valid_connections2);
|
|
constraint table_int([i1____00393, j1____00394, i2____00395, j2____00396], valid_connections2);
|
|
constraint table_int([i1____00401, j1____00402, i2____00403, j2____00404], valid_connections2);
|
|
constraint table_int([i1____00409, j1____00410, i2____00411, j2____00412], valid_connections2);
|
|
constraint table_int([i1____00417, j1____00418, i2____00419, j2____00420], valid_connections2);
|
|
constraint table_int([i1____00425, j1____00426, i2____00427, j2____00428], valid_connections2);
|
|
constraint table_int([i1____00433, j1____00434, i2____00435, j2____00436], valid_connections2);
|
|
constraint table_int([i1____00441, j1____00442, i2____00443, j2____00444], valid_connections2);
|
|
constraint table_int([i1____00449, j1____00450, i2____00451, j2____00452], valid_connections2);
|
|
constraint table_int([i1____00457, j1____00458, i2____00459, j2____00460], valid_connections2);
|
|
constraint table_int([i1____00465, j1____00466, i2____00467, j2____00468], valid_connections2);
|
|
constraint table_int([i1____00473, j1____00474, i2____00475, j2____00476], valid_connections2);
|
|
constraint table_int([i1____00481, j1____00482, i2____00483, j2____00484], valid_connections2);
|
|
constraint table_int([i1____00489, j1____00490, i2____00491, j2____00492], valid_connections2);
|
|
constraint table_int([i1____00497, j1____00498, i2____00499, j2____00500], valid_connections2);
|
|
constraint table_int([i1____00505, j1____00506, i2____00507, j2____00508], valid_connections2);
|
|
constraint table_int([i1____00513, j1____00514, i2____00515, j2____00516], valid_connections2);
|
|
constraint table_int([i1____00521, j1____00522, i2____00523, j2____00524], valid_connections2);
|
|
constraint table_int([i1____00529, j1____00530, i2____00531, j2____00532], valid_connections2);
|
|
constraint table_int([i1____00537, j1____00538, i2____00539, j2____00540], valid_connections2);
|
|
constraint table_int([i1____00545, j1____00546, i2____00547, j2____00548], valid_connections2);
|
|
constraint table_int([i1____00553, j1____00554, i2____00555, j2____00556], valid_connections2);
|
|
constraint table_int([i1____00561, j1____00562, i2____00563, j2____00564], valid_connections2);
|
|
constraint table_int([i1____00569, j1____00570, i2____00571, j2____00572], valid_connections2);
|
|
constraint table_int([i1____00577, j1____00578, i2____00579, j2____00580], valid_connections2);
|
|
constraint table_int([i1____00585, j1____00586, i2____00587, j2____00588], valid_connections2);
|
|
constraint table_int([i1____00593, j1____00594, i2____00595, j2____00596], valid_connections2);
|
|
constraint table_int([i1____00601, j1____00602, i2____00603, j2____00604], valid_connections2);
|
|
constraint table_int([i1____00609, j1____00610, i2____00611, j2____00612], valid_connections2);
|
|
constraint table_int([i1____00617, j1____00618, i2____00619, j2____00620], valid_connections2);
|
|
constraint table_int([i1____00625, j1____00626, i2____00627, j2____00628], valid_connections2);
|
|
constraint table_int([i1____00633, j1____00634, i2____00635, j2____00636], valid_connections2);
|
|
constraint table_int([i1____00641, j1____00642, i2____00643, j2____00644], valid_connections2);
|
|
constraint table_int([i1____00649, j1____00650, i2____00651, j2____00652], valid_connections2);
|
|
constraint table_int([i1____00657, j1____00658, i2____00659, j2____00660], valid_connections2);
|
|
constraint table_int([i1____00665, j1____00666, i2____00667, j2____00668], valid_connections2);
|
|
constraint table_int([i1____00673, j1____00674, i2____00675, j2____00676], valid_connections2);
|
|
constraint table_int([i1____00681, j1____00682, i2____00683, j2____00684], valid_connections2);
|
|
constraint table_int([i1____00689, j1____00690, i2____00691, j2____00692], valid_connections2);
|
|
constraint table_int([i1____00697, j1____00698, i2____00699, j2____00700], valid_connections2);
|
|
constraint table_int([i1____00705, j1____00706, i2____00707, j2____00708], valid_connections2);
|
|
constraint table_int([i1____00713, j1____00714, i2____00715, j2____00716], valid_connections2);
|
|
constraint table_int([i1____00721, j1____00722, i2____00723, j2____00724], valid_connections2);
|
|
constraint table_int([i1____00729, j1____00730, i2____00731, j2____00732], valid_connections2);
|
|
constraint table_int([i1____00737, j1____00738, i2____00739, j2____00740], valid_connections2);
|
|
constraint table_int([i1____00745, j1____00746, i2____00747, j2____00748], valid_connections2);
|
|
constraint table_int([i1____00753, j1____00754, i2____00755, j2____00756], valid_connections2);
|
|
constraint table_int([i1____00761, j1____00762, i2____00763, j2____00764], valid_connections2);
|
|
constraint table_int([i1____00769, j1____00770, i2____00771, j2____00772], valid_connections2);
|
|
constraint table_int([i1____00777, j1____00778, i2____00779, j2____00780], valid_connections2);
|
|
constraint table_int([i1____00785, j1____00786, i2____00787, j2____00788], valid_connections2);
|
|
constraint table_int([i1____00793, j1____00794, i2____00795, j2____00796], valid_connections2);
|
|
constraint table_int([i1____00801, j1____00802, i2____00803, j2____00804], valid_connections2);
|
|
constraint table_int([i1____00809, j1____00810, i2____00811, j2____00812], valid_connections2);
|
|
constraint table_int([i1____00817, j1____00818, i2____00819, j2____00820], valid_connections2);
|
|
constraint table_int([i1____00825, j1____00826, i2____00827, j2____00828], valid_connections2);
|
|
constraint table_int([i1____00833, j1____00834, i2____00835, j2____00836], valid_connections2);
|
|
constraint table_int([i1____00841, j1____00842, i2____00843, j2____00844], valid_connections2);
|
|
constraint table_int([i1____00849, j1____00850, i2____00851, j2____00852], valid_connections2);
|
|
constraint table_int([i1____00857, j1____00858, i2____00859, j2____00860], valid_connections2);
|
|
constraint table_int([i1____00865, j1____00866, i2____00867, j2____00868], valid_connections2);
|
|
constraint table_int([i1____00873, j1____00874, i2____00875, j2____00876], valid_connections2);
|
|
constraint table_int([i1____00881, j1____00882, i2____00883, j2____00884], valid_connections2);
|
|
constraint table_int([i1____00889, j1____00890, i2____00891, j2____00892], valid_connections2);
|
|
constraint table_int([i1____00897, j1____00898, i2____00899, j2____00900], valid_connections2);
|
|
constraint table_int([i1____00905, j1____00906, i2____00907, j2____00908], valid_connections2);
|
|
constraint table_int([i1____00913, j1____00914, i2____00915, j2____00916], valid_connections2);
|
|
constraint table_int([i1____00921, j1____00922, i2____00923, j2____00924], valid_connections2);
|
|
constraint table_int([i1____00929, j1____00930, i2____00931, j2____00932], valid_connections2);
|
|
constraint table_int([i1____00937, j1____00938, i2____00939, j2____00940], valid_connections2);
|
|
constraint table_int([i1____00945, j1____00946, i2____00947, j2____00948], valid_connections2);
|
|
constraint table_int([i1____00953, j1____00954, i2____00955, j2____00956], valid_connections2);
|
|
constraint table_int([i1____00961, j1____00962, i2____00963, j2____00964], valid_connections2);
|
|
constraint table_int([i1____00969, j1____00970, i2____00971, j2____00972], valid_connections2);
|
|
constraint table_int([i1____00977, j1____00978, i2____00979, j2____00980], valid_connections2);
|
|
constraint table_int([i1____00985, j1____00986, i2____00987, j2____00988], valid_connections2);
|
|
constraint table_int([i1____00993, j1____00994, i2____00995, j2____00996], valid_connections2);
|
|
constraint table_int([i1____01001, j1____01002, i2____01003, j2____01004], valid_connections2);
|
|
constraint table_int([i1____01009, j1____01010, i2____01011, j2____01012], valid_connections2);
|
|
constraint table_int([i1____01017, j1____01018, i2____01019, j2____01020], valid_connections2);
|
|
constraint table_int([i1____01025, j1____01026, i2____01027, j2____01028], valid_connections2);
|
|
constraint table_int([i1____01033, j1____01034, i2____01035, j2____01036], valid_connections2);
|
|
constraint table_int([i1____01041, j1____01042, i2____01043, j2____01044], valid_connections2);
|
|
constraint table_int([i1____01049, j1____01050, i2____01051, j2____01052], valid_connections2);
|
|
constraint table_int([i1____01057, j1____01058, i2____01059, j2____01060], valid_connections2);
|
|
constraint table_int([i1____01065, j1____01066, i2____01067, j2____01068], valid_connections2);
|
|
constraint table_int([i1____01073, j1____01074, i2____01075, j2____01076], valid_connections2);
|
|
constraint table_int([i1____01081, j1____01082, i2____01083, j2____01084], valid_connections2);
|
|
constraint table_int([i1____01089, j1____01090, i2____01091, j2____01092], valid_connections2);
|
|
constraint table_int([i1____01097, j1____01098, i2____01099, j2____01100], valid_connections2);
|
|
constraint table_int([i1____01105, j1____01106, i2____01107, j2____01108], valid_connections2);
|
|
constraint table_int([i1____01113, j1____01114, i2____01115, j2____01116], valid_connections2);
|
|
constraint table_int([i1____01121, j1____01122, i2____01123, j2____01124], valid_connections2);
|
|
constraint table_int([i1____01129, j1____01130, i2____01131, j2____01132], valid_connections2);
|
|
constraint table_int([i1____01137, j1____01138, i2____01139, j2____01140], valid_connections2);
|
|
solve :: int_search([x[1], x[2], x[3], x[4], x[5], x[6], x[7], x[8], x[9], x[10], x[11], x[12], x[13], x[14], x[15], x[16], x[17], x[18], x[19], x[20], x[21], x[22], x[23], x[24], x[25], x[26], x[27], x[28], x[29], x[30], x[31], x[32], x[33], x[34], x[35], x[36], x[37], x[38], x[39], x[40], x[41], x[42], x[43], x[44], x[45], x[46], x[47], x[48], x[49], x[50], x[51], x[52], x[53], x[54], x[55], x[56], x[57], x[58], x[59], x[60], x[61], x[62], x[63], x[64], x[65], x[66], x[67], x[68], x[69], x[70], x[71], x[72], x[73], x[74], x[75], x[76], x[77], x[78], x[79], x[80], x[81], x[82], x[83], x[84], x[85], x[86], x[87], x[88], x[89], x[90], x[91], x[92], x[93], x[94], x[95], x[96], x[97], x[98], x[99], x[100], x[101], x[102], x[103], x[104], x[105], x[106], x[107], x[108], x[109], x[110], x[111], x[112], x[113], x[114], x[115], x[116], x[117], x[118], x[119], x[120], x[121], x[122], x[123], x[124], x[125], x[126], x[127], x[128], x[129], x[130], x[131], x[132], x[133], x[134], x[135], x[136], x[137], x[138], x[139], x[140], x[141], x[142], x[143], x[144]], max_regret, indomain_min, complete) satisfy;
|