fork download
copy 
  1. process.stdin.resume();
  2. process.stdin.setEncoding('utf8');
  3.  
  4. const puzzle = {
  5.     "width": 9,
  6.     "height": 9,
  7.     "blackCount": 33
  8. };
  9.  
  10. const size = puzzle.width * puzzle.height;
  11. const vars = (name, id) => `${name}_${id}`
  12. const v = {};
  13.  
  14. const define = (type, name, size, domain) => {
  15.     v[name] = (id) => name + `_` + id;
  16.     if (typeof domain === 'string') {
  17.         let tmp2 = '' + domain;
  18.         domain = () => tmp2;
  19.     }
  20.     return range(size).map(id => `(${type} ${v[name](id)} ${domain(id)})`)
  21. };
  22.  
  23. /* formula */
  24. const formula = (sign, ...arr) => `(${sign} ${arr.join(' ')})`
  25. const f = {};
  26. const signs = {
  27.     if: 'if',
  28.     eq: '=',
  29.     ne: '!=',
  30.     and: '&&',
  31.     or: '||',
  32.     gt: '>',
  33.     lt: '<',
  34.     le: '<=',
  35.     ge: '>=',
  36.     imp: '=>',
  37.     plus: '+'
  38. };
  39. Object.keys(signs).forEach((name) => { f[name] = (...arr) => formula(signs[name], ...arr); });
  40.  
  41. const range = (size) => [...Array(size).keys()];
  42. const maxAreaNumber = size
  43. const maxAreaSize = 8;
  44.  
  45. const checkFourDirections = (x, y, func) => [
  46.     x !== puzzle.width - 1 ? func(1) : null,
  47.     x !== 0 ? func(-1) : null,
  48.     y !== puzzle.height - 1 ? func(puzzle.width) : null,
  49.     y !== 0 ? func(-puzzle.width) : null,
  50. ].filter(e => e != null);
  51.  
  52. const checkRightBottom = (x, y, func) => [
  53.     x !== puzzle.width - 1 ? func(1) : null,
  54.     y !== puzzle.height - 1 ? func(puzzle.width) : null,
  55. ].filter(e => e != null);
  56.  
  57. /**
  58.  * 根の条件
  59.  * @param {} id 
  60.  */
  61. const rootConstraints = (id) => {
  62.     const isRoot = f.eq(v.r(id), 1);
  63.     return f.imp(isRoot, f.and(
  64.         f.eq(v.z(id), 0),
  65.         f.eq(v.x(id), 1),
  66.     ))
  67. }
  68.  
  69. /* 連結条件 */
  70. const connectConstraints = (id) => {
  71.     const x = id % puzzle.width;
  72.     const y = id / puzzle.width | 0;
  73.     /**
  74.      * 親マスについての条件
  75.      * エリア番号が1,
  76.      * エリア内番号が小さい,
  77.      * な隣接するマスが存在
  78.      */
  79.     const connection = (diff) => f.and(
  80.         f.eq(v.x(id + diff), 1),
  81.         f.gt(v.z(id), v.z(id + diff)),
  82.     );
  83.  
  84.     /* 根じゃなければ隣接するどこかが親 */
  85.     const isNotRoot = f.eq(v.r(id), 0);
  86.     return f.imp(f.and(isNotRoot, f.eq(v.x(id), 1)), f.or(...checkFourDirections(x, y, connection)));
  87. }
  88.  
  89. /**
  90.  * 横方向の連続同色数条件
  91.  * @param {} id 
  92.  */
  93. const rowCount = (id) => {
  94.     const x = id % puzzle.width;
  95.     const y = id / puzzle.width | 0;
  96.     if (x == 0) { return f.eq(v.row(id), 0) }
  97.  
  98.     return f.or(
  99.         f.and(
  100.             f.eq(v.x(id - 1), v.x(id)),
  101.             f.eq(v.row(id), f.plus(v.row(id - 1), 1))
  102.         ),
  103.         f.and(
  104.             f.ne(v.x(id - 1), v.x(id)),
  105.             f.eq(v.row(id), 0)
  106.         )
  107.     );
  108. }
  109.  
  110. /**
  111.  * 縦方向の連続同色数条件
  112.  * @param {} id 
  113.  */
  114. const colCount = (id) => {
  115.     const x = id % puzzle.width;
  116.     const y = id / puzzle.width | 0;
  117.     if (y == 0) { return f.eq(v.col(id), 0) }
  118.  
  119.     return f.or(
  120.         f.and(
  121.             f.eq(v.x(id - puzzle.width), v.x(id)),
  122.             f.eq(v.col(id), f.plus(v.col(id - puzzle.width), 1))
  123.         ),
  124.         f.and(
  125.             f.ne(v.x(id - puzzle.width), v.x(id)),
  126.             f.eq(v.col(id), 0)
  127.         )
  128.     );
  129. }
  130.  
  131. const defines = []
  132.     .concat(define('int', 'z', size, `0 ${size}`)) // エリア内番号
  133.     .concat(define('int', 'r', size, `0 1`)) // is root
  134.     .concat(define('int', 'x', size, `0 1`)) // 色
  135.     .concat(define('int', 'col', size, `0 2`)) // 縦方向同色連続数
  136.     .concat(define('int', 'row', size, `0 2`)) // 横方向同色連続数
  137.  
  138. const lines = defines
  139.     .concat(range(size).map(rootConstraints))
  140.     .concat(range(size).map(connectConstraints))
  141.     .concat(range(size).map(rowCount))
  142.     .concat(range(size).map(colCount))
  143.     .concat(f.eq(f.plus(...range(size).map(id => v.r(id))), 1))
  144.     .concat(f.le(f.plus(...range(size).map(id => v.x(id))), puzzle.blackCount));
  145.  
  146. console.log(lines.filter(e => e != null).join('\n'));
Success #stdin #stdout 0.12s 32256KB
comments (?)
stdin
copy 
Standard input is empty
stdout
copy 
(int z_0 0 81)
(int z_1 0 81)
(int z_2 0 81)
(int z_3 0 81)
(int z_4 0 81)
(int z_5 0 81)
(int z_6 0 81)
(int z_7 0 81)
(int z_8 0 81)
(int z_9 0 81)
(int z_10 0 81)
(int z_11 0 81)
(int z_12 0 81)
(int z_13 0 81)
(int z_14 0 81)
(int z_15 0 81)
(int z_16 0 81)
(int z_17 0 81)
(int z_18 0 81)
(int z_19 0 81)
(int z_20 0 81)
(int z_21 0 81)
(int z_22 0 81)
(int z_23 0 81)
(int z_24 0 81)
(int z_25 0 81)
(int z_26 0 81)
(int z_27 0 81)
(int z_28 0 81)
(int z_29 0 81)
(int z_30 0 81)
(int z_31 0 81)
(int z_32 0 81)
(int z_33 0 81)
(int z_34 0 81)
(int z_35 0 81)
(int z_36 0 81)
(int z_37 0 81)
(int z_38 0 81)
(int z_39 0 81)
(int z_40 0 81)
(int z_41 0 81)
(int z_42 0 81)
(int z_43 0 81)
(int z_44 0 81)
(int z_45 0 81)
(int z_46 0 81)
(int z_47 0 81)
(int z_48 0 81)
(int z_49 0 81)
(int z_50 0 81)
(int z_51 0 81)
(int z_52 0 81)
(int z_53 0 81)
(int z_54 0 81)
(int z_55 0 81)
(int z_56 0 81)
(int z_57 0 81)
(int z_58 0 81)
(int z_59 0 81)
(int z_60 0 81)
(int z_61 0 81)
(int z_62 0 81)
(int z_63 0 81)
(int z_64 0 81)
(int z_65 0 81)
(int z_66 0 81)
(int z_67 0 81)
(int z_68 0 81)
(int z_69 0 81)
(int z_70 0 81)
(int z_71 0 81)
(int z_72 0 81)
(int z_73 0 81)
(int z_74 0 81)
(int z_75 0 81)
(int z_76 0 81)
(int z_77 0 81)
(int z_78 0 81)
(int z_79 0 81)
(int z_80 0 81)
(int r_0 0 1)
(int r_1 0 1)
(int r_2 0 1)
(int r_3 0 1)
(int r_4 0 1)
(int r_5 0 1)
(int r_6 0 1)
(int r_7 0 1)
(int r_8 0 1)
(int r_9 0 1)
(int r_10 0 1)
(int r_11 0 1)
(int r_12 0 1)
(int r_13 0 1)
(int r_14 0 1)
(int r_15 0 1)
(int r_16 0 1)
(int r_17 0 1)
(int r_18 0 1)
(int r_19 0 1)
(int r_20 0 1)
(int r_21 0 1)
(int r_22 0 1)
(int r_23 0 1)
(int r_24 0 1)
(int r_25 0 1)
(int r_26 0 1)
(int r_27 0 1)
(int r_28 0 1)
(int r_29 0 1)
(int r_30 0 1)
(int r_31 0 1)
(int r_32 0 1)
(int r_33 0 1)
(int r_34 0 1)
(int r_35 0 1)
(int r_36 0 1)
(int r_37 0 1)
(int r_38 0 1)
(int r_39 0 1)
(int r_40 0 1)
(int r_41 0 1)
(int r_42 0 1)
(int r_43 0 1)
(int r_44 0 1)
(int r_45 0 1)
(int r_46 0 1)
(int r_47 0 1)
(int r_48 0 1)
(int r_49 0 1)
(int r_50 0 1)
(int r_51 0 1)
(int r_52 0 1)
(int r_53 0 1)
(int r_54 0 1)
(int r_55 0 1)
(int r_56 0 1)
(int r_57 0 1)
(int r_58 0 1)
(int r_59 0 1)
(int r_60 0 1)
(int r_61 0 1)
(int r_62 0 1)
(int r_63 0 1)
(int r_64 0 1)
(int r_65 0 1)
(int r_66 0 1)
(int r_67 0 1)
(int r_68 0 1)
(int r_69 0 1)
(int r_70 0 1)
(int r_71 0 1)
(int r_72 0 1)
(int r_73 0 1)
(int r_74 0 1)
(int r_75 0 1)
(int r_76 0 1)
(int r_77 0 1)
(int r_78 0 1)
(int r_79 0 1)
(int r_80 0 1)
(int x_0 0 1)
(int x_1 0 1)
(int x_2 0 1)
(int x_3 0 1)
(int x_4 0 1)
(int x_5 0 1)
(int x_6 0 1)
(int x_7 0 1)
(int x_8 0 1)
(int x_9 0 1)
(int x_10 0 1)
(int x_11 0 1)
(int x_12 0 1)
(int x_13 0 1)
(int x_14 0 1)
(int x_15 0 1)
(int x_16 0 1)
(int x_17 0 1)
(int x_18 0 1)
(int x_19 0 1)
(int x_20 0 1)
(int x_21 0 1)
(int x_22 0 1)
(int x_23 0 1)
(int x_24 0 1)
(int x_25 0 1)
(int x_26 0 1)
(int x_27 0 1)
(int x_28 0 1)
(int x_29 0 1)
(int x_30 0 1)
(int x_31 0 1)
(int x_32 0 1)
(int x_33 0 1)
(int x_34 0 1)
(int x_35 0 1)
(int x_36 0 1)
(int x_37 0 1)
(int x_38 0 1)
(int x_39 0 1)
(int x_40 0 1)
(int x_41 0 1)
(int x_42 0 1)
(int x_43 0 1)
(int x_44 0 1)
(int x_45 0 1)
(int x_46 0 1)
(int x_47 0 1)
(int x_48 0 1)
(int x_49 0 1)
(int x_50 0 1)
(int x_51 0 1)
(int x_52 0 1)
(int x_53 0 1)
(int x_54 0 1)
(int x_55 0 1)
(int x_56 0 1)
(int x_57 0 1)
(int x_58 0 1)
(int x_59 0 1)
(int x_60 0 1)
(int x_61 0 1)
(int x_62 0 1)
(int x_63 0 1)
(int x_64 0 1)
(int x_65 0 1)
(int x_66 0 1)
(int x_67 0 1)
(int x_68 0 1)
(int x_69 0 1)
(int x_70 0 1)
(int x_71 0 1)
(int x_72 0 1)
(int x_73 0 1)
(int x_74 0 1)
(int x_75 0 1)
(int x_76 0 1)
(int x_77 0 1)
(int x_78 0 1)
(int x_79 0 1)
(int x_80 0 1)
(int col_0 0 2)
(int col_1 0 2)
(int col_2 0 2)
(int col_3 0 2)
(int col_4 0 2)
(int col_5 0 2)
(int col_6 0 2)
(int col_7 0 2)
(int col_8 0 2)
(int col_9 0 2)
(int col_10 0 2)
(int col_11 0 2)
(int col_12 0 2)
(int col_13 0 2)
(int col_14 0 2)
(int col_15 0 2)
(int col_16 0 2)
(int col_17 0 2)
(int col_18 0 2)
(int col_19 0 2)
(int col_20 0 2)
(int col_21 0 2)
(int col_22 0 2)
(int col_23 0 2)
(int col_24 0 2)
(int col_25 0 2)
(int col_26 0 2)
(int col_27 0 2)
(int col_28 0 2)
(int col_29 0 2)
(int col_30 0 2)
(int col_31 0 2)
(int col_32 0 2)
(int col_33 0 2)
(int col_34 0 2)
(int col_35 0 2)
(int col_36 0 2)
(int col_37 0 2)
(int col_38 0 2)
(int col_39 0 2)
(int col_40 0 2)
(int col_41 0 2)
(int col_42 0 2)
(int col_43 0 2)
(int col_44 0 2)
(int col_45 0 2)
(int col_46 0 2)
(int col_47 0 2)
(int col_48 0 2)
(int col_49 0 2)
(int col_50 0 2)
(int col_51 0 2)
(int col_52 0 2)
(int col_53 0 2)
(int col_54 0 2)
(int col_55 0 2)
(int col_56 0 2)
(int col_57 0 2)
(int col_58 0 2)
(int col_59 0 2)
(int col_60 0 2)
(int col_61 0 2)
(int col_62 0 2)
(int col_63 0 2)
(int col_64 0 2)
(int col_65 0 2)
(int col_66 0 2)
(int col_67 0 2)
(int col_68 0 2)
(int col_69 0 2)
(int col_70 0 2)
(int col_71 0 2)
(int col_72 0 2)
(int col_73 0 2)
(int col_74 0 2)
(int col_75 0 2)
(int col_76 0 2)
(int col_77 0 2)
(int col_78 0 2)
(int col_79 0 2)
(int col_80 0 2)
(int row_0 0 2)
(int row_1 0 2)
(int row_2 0 2)
(int row_3 0 2)
(int row_4 0 2)
(int row_5 0 2)
(int row_6 0 2)
(int row_7 0 2)
(int row_8 0 2)
(int row_9 0 2)
(int row_10 0 2)
(int row_11 0 2)
(int row_12 0 2)
(int row_13 0 2)
(int row_14 0 2)
(int row_15 0 2)
(int row_16 0 2)
(int row_17 0 2)
(int row_18 0 2)
(int row_19 0 2)
(int row_20 0 2)
(int row_21 0 2)
(int row_22 0 2)
(int row_23 0 2)
(int row_24 0 2)
(int row_25 0 2)
(int row_26 0 2)
(int row_27 0 2)
(int row_28 0 2)
(int row_29 0 2)
(int row_30 0 2)
(int row_31 0 2)
(int row_32 0 2)
(int row_33 0 2)
(int row_34 0 2)
(int row_35 0 2)
(int row_36 0 2)
(int row_37 0 2)
(int row_38 0 2)
(int row_39 0 2)
(int row_40 0 2)
(int row_41 0 2)
(int row_42 0 2)
(int row_43 0 2)
(int row_44 0 2)
(int row_45 0 2)
(int row_46 0 2)
(int row_47 0 2)
(int row_48 0 2)
(int row_49 0 2)
(int row_50 0 2)
(int row_51 0 2)
(int row_52 0 2)
(int row_53 0 2)
(int row_54 0 2)
(int row_55 0 2)
(int row_56 0 2)
(int row_57 0 2)
(int row_58 0 2)
(int row_59 0 2)
(int row_60 0 2)
(int row_61 0 2)
(int row_62 0 2)
(int row_63 0 2)
(int row_64 0 2)
(int row_65 0 2)
(int row_66 0 2)
(int row_67 0 2)
(int row_68 0 2)
(int row_69 0 2)
(int row_70 0 2)
(int row_71 0 2)
(int row_72 0 2)
(int row_73 0 2)
(int row_74 0 2)
(int row_75 0 2)
(int row_76 0 2)
(int row_77 0 2)
(int row_78 0 2)
(int row_79 0 2)
(int row_80 0 2)
(=> (= r_0 1) (&& (= z_0 0) (= x_0 1)))
(=> (= r_1 1) (&& (= z_1 0) (= x_1 1)))
(=> (= r_2 1) (&& (= z_2 0) (= x_2 1)))
(=> (= r_3 1) (&& (= z_3 0) (= x_3 1)))
(=> (= r_4 1) (&& (= z_4 0) (= x_4 1)))
(=> (= r_5 1) (&& (= z_5 0) (= x_5 1)))
(=> (= r_6 1) (&& (= z_6 0) (= x_6 1)))
(=> (= r_7 1) (&& (= z_7 0) (= x_7 1)))
(=> (= r_8 1) (&& (= z_8 0) (= x_8 1)))
(=> (= r_9 1) (&& (= z_9 0) (= x_9 1)))
(=> (= r_10 1) (&& (= z_10 0) (= x_10 1)))
(=> (= r_11 1) (&& (= z_11 0) (= x_11 1)))
(=> (= r_12 1) (&& (= z_12 0) (= x_12 1)))
(=> (= r_13 1) (&& (= z_13 0) (= x_13 1)))
(=> (= r_14 1) (&& (= z_14 0) (= x_14 1)))
(=> (= r_15 1) (&& (= z_15 0) (= x_15 1)))
(=> (= r_16 1) (&& (= z_16 0) (= x_16 1)))
(=> (= r_17 1) (&& (= z_17 0) (= x_17 1)))
(=> (= r_18 1) (&& (= z_18 0) (= x_18 1)))
(=> (= r_19 1) (&& (= z_19 0) (= x_19 1)))
(=> (= r_20 1) (&& (= z_20 0) (= x_20 1)))
(=> (= r_21 1) (&& (= z_21 0) (= x_21 1)))
(=> (= r_22 1) (&& (= z_22 0) (= x_22 1)))
(=> (= r_23 1) (&& (= z_23 0) (= x_23 1)))
(=> (= r_24 1) (&& (= z_24 0) (= x_24 1)))
(=> (= r_25 1) (&& (= z_25 0) (= x_25 1)))
(=> (= r_26 1) (&& (= z_26 0) (= x_26 1)))
(=> (= r_27 1) (&& (= z_27 0) (= x_27 1)))
(=> (= r_28 1) (&& (= z_28 0) (= x_28 1)))
(=> (= r_29 1) (&& (= z_29 0) (= x_29 1)))
(=> (= r_30 1) (&& (= z_30 0) (= x_30 1)))
(=> (= r_31 1) (&& (= z_31 0) (= x_31 1)))
(=> (= r_32 1) (&& (= z_32 0) (= x_32 1)))
(=> (= r_33 1) (&& (= z_33 0) (= x_33 1)))
(=> (= r_34 1) (&& (= z_34 0) (= x_34 1)))
(=> (= r_35 1) (&& (= z_35 0) (= x_35 1)))
(=> (= r_36 1) (&& (= z_36 0) (= x_36 1)))
(=> (= r_37 1) (&& (= z_37 0) (= x_37 1)))
(=> (= r_38 1) (&& (= z_38 0) (= x_38 1)))
(=> (= r_39 1) (&& (= z_39 0) (= x_39 1)))
(=> (= r_40 1) (&& (= z_40 0) (= x_40 1)))
(=> (= r_41 1) (&& (= z_41 0) (= x_41 1)))
(=> (= r_42 1) (&& (= z_42 0) (= x_42 1)))
(=> (= r_43 1) (&& (= z_43 0) (= x_43 1)))
(=> (= r_44 1) (&& (= z_44 0) (= x_44 1)))
(=> (= r_45 1) (&& (= z_45 0) (= x_45 1)))
(=> (= r_46 1) (&& (= z_46 0) (= x_46 1)))
(=> (= r_47 1) (&& (= z_47 0) (= x_47 1)))
(=> (= r_48 1) (&& (= z_48 0) (= x_48 1)))
(=> (= r_49 1) (&& (= z_49 0) (= x_49 1)))
(=> (= r_50 1) (&& (= z_50 0) (= x_50 1)))
(=> (= r_51 1) (&& (= z_51 0) (= x_51 1)))
(=> (= r_52 1) (&& (= z_52 0) (= x_52 1)))
(=> (= r_53 1) (&& (= z_53 0) (= x_53 1)))
(=> (= r_54 1) (&& (= z_54 0) (= x_54 1)))
(=> (= r_55 1) (&& (= z_55 0) (= x_55 1)))
(=> (= r_56 1) (&& (= z_56 0) (= x_56 1)))
(=> (= r_57 1) (&& (= z_57 0) (= x_57 1)))
(=> (= r_58 1) (&& (= z_58 0) (= x_58 1)))
(=> (= r_59 1) (&& (= z_59 0) (= x_59 1)))
(=> (= r_60 1) (&& (= z_60 0) (= x_60 1)))
(=> (= r_61 1) (&& (= z_61 0) (= x_61 1)))
(=> (= r_62 1) (&& (= z_62 0) (= x_62 1)))
(=> (= r_63 1) (&& (= z_63 0) (= x_63 1)))
(=> (= r_64 1) (&& (= z_64 0) (= x_64 1)))
(=> (= r_65 1) (&& (= z_65 0) (= x_65 1)))
(=> (= r_66 1) (&& (= z_66 0) (= x_66 1)))
(=> (= r_67 1) (&& (= z_67 0) (= x_67 1)))
(=> (= r_68 1) (&& (= z_68 0) (= x_68 1)))
(=> (= r_69 1) (&& (= z_69 0) (= x_69 1)))
(=> (= r_70 1) (&& (= z_70 0) (= x_70 1)))
(=> (= r_71 1) (&& (= z_71 0) (= x_71 1)))
(=> (= r_72 1) (&& (= z_72 0) (= x_72 1)))
(=> (= r_73 1) (&& (= z_73 0) (= x_73 1)))
(=> (= r_74 1) (&& (= z_74 0) (= x_74 1)))
(=> (= r_75 1) (&& (= z_75 0) (= x_75 1)))
(=> (= r_76 1) (&& (= z_76 0) (= x_76 1)))
(=> (= r_77 1) (&& (= z_77 0) (= x_77 1)))
(=> (= r_78 1) (&& (= z_78 0) (= x_78 1)))
(=> (= r_79 1) (&& (= z_79 0) (= x_79 1)))
(=> (= r_80 1) (&& (= z_80 0) (= x_80 1)))
(=> (&& (= r_0 0) (= x_0 1)) (|| (&& (= x_1 1) (> z_0 z_1)) (&& (= x_9 1) (> z_0 z_9))))
(=> (&& (= r_1 0) (= x_1 1)) (|| (&& (= x_2 1) (> z_1 z_2)) (&& (= x_0 1) (> z_1 z_0)) (&& (= x_10 1) (> z_1 z_10))))
(=> (&& (= r_2 0) (= x_2 1)) (|| (&& (= x_3 1) (> z_2 z_3)) (&& (= x_1 1) (> z_2 z_1)) (&& (= x_11 1) (> z_2 z_11))))
(=> (&& (= r_3 0) (= x_3 1)) (|| (&& (= x_4 1) (> z_3 z_4)) (&& (= x_2 1) (> z_3 z_2)) (&& (= x_12 1) (> z_3 z_12))))
(=> (&& (= r_4 0) (= x_4 1)) (|| (&& (= x_5 1) (> z_4 z_5)) (&& (= x_3 1) (> z_4 z_3)) (&& (= x_13 1) (> z_4 z_13))))
(=> (&& (= r_5 0) (= x_5 1)) (|| (&& (= x_6 1) (> z_5 z_6)) (&& (= x_4 1) (> z_5 z_4)) (&& (= x_14 1) (> z_5 z_14))))
(=> (&& (= r_6 0) (= x_6 1)) (|| (&& (= x_7 1) (> z_6 z_7)) (&& (= x_5 1) (> z_6 z_5)) (&& (= x_15 1) (> z_6 z_15))))
(=> (&& (= r_7 0) (= x_7 1)) (|| (&& (= x_8 1) (> z_7 z_8)) (&& (= x_6 1) (> z_7 z_6)) (&& (= x_16 1) (> z_7 z_16))))
(=> (&& (= r_8 0) (= x_8 1)) (|| (&& (= x_7 1) (> z_8 z_7)) (&& (= x_17 1) (> z_8 z_17))))
(=> (&& (= r_9 0) (= x_9 1)) (|| (&& (= x_10 1) (> z_9 z_10)) (&& (= x_18 1) (> z_9 z_18)) (&& (= x_0 1) (> z_9 z_0))))
(=> (&& (= r_10 0) (= x_10 1)) (|| (&& (= x_11 1) (> z_10 z_11)) (&& (= x_9 1) (> z_10 z_9)) (&& (= x_19 1) (> z_10 z_19)) (&& (= x_1 1) (> z_10 z_1))))
(=> (&& (= r_11 0) (= x_11 1)) (|| (&& (= x_12 1) (> z_11 z_12)) (&& (= x_10 1) (> z_11 z_10)) (&& (= x_20 1) (> z_11 z_20)) (&& (= x_2 1) (> z_11 z_2))))
(=> (&& (= r_12 0) (= x_12 1)) (|| (&& (= x_13 1) (> z_12 z_13)) (&& (= x_11 1) (> z_12 z_11)) (&& (= x_21 1) (> z_12 z_21)) (&& (= x_3 1) (> z_12 z_3))))
(=> (&& (= r_13 0) (= x_13 1)) (|| (&& (= x_14 1) (> z_13 z_14)) (&& (= x_12 1) (> z_13 z_12)) (&& (= x_22 1) (> z_13 z_22)) (&& (= x_4 1) (> z_13 z_4))))
(=> (&& (= r_14 0) (= x_14 1)) (|| (&& (= x_15 1) (> z_14 z_15)) (&& (= x_13 1) (> z_14 z_13)) (&& (= x_23 1) (> z_14 z_23)) (&& (= x_5 1) (> z_14 z_5))))
(=> (&& (= r_15 0) (= x_15 1)) (|| (&& (= x_16 1) (> z_15 z_16)) (&& (= x_14 1) (> z_15 z_14)) (&& (= x_24 1) (> z_15 z_24)) (&& (= x_6 1) (> z_15 z_6))))
(=> (&& (= r_16 0) (= x_16 1)) (|| (&& (= x_17 1) (> z_16 z_17)) (&& (= x_15 1) (> z_16 z_15)) (&& (= x_25 1) (> z_16 z_25)) (&& (= x_7 1) (> z_16 z_7))))
(=> (&& (= r_17 0) (= x_17 1)) (|| (&& (= x_16 1) (> z_17 z_16)) (&& (= x_26 1) (> z_17 z_26)) (&& (= x_8 1) (> z_17 z_8))))
(=> (&& (= r_18 0) (= x_18 1)) (|| (&& (= x_19 1) (> z_18 z_19)) (&& (= x_27 1) (> z_18 z_27)) (&& (= x_9 1) (> z_18 z_9))))
(=> (&& (= r_19 0) (= x_19 1)) (|| (&& (= x_20 1) (> z_19 z_20)) (&& (= x_18 1) (> z_19 z_18)) (&& (= x_28 1) (> z_19 z_28)) (&& (= x_10 1) (> z_19 z_10))))
(=> (&& (= r_20 0) (= x_20 1)) (|| (&& (= x_21 1) (> z_20 z_21)) (&& (= x_19 1) (> z_20 z_19)) (&& (= x_29 1) (> z_20 z_29)) (&& (= x_11 1) (> z_20 z_11))))
(=> (&& (= r_21 0) (= x_21 1)) (|| (&& (= x_22 1) (> z_21 z_22)) (&& (= x_20 1) (> z_21 z_20)) (&& (= x_30 1) (> z_21 z_30)) (&& (= x_12 1) (> z_21 z_12))))
(=> (&& (= r_22 0) (= x_22 1)) (|| (&& (= x_23 1) (> z_22 z_23)) (&& (= x_21 1) (> z_22 z_21)) (&& (= x_31 1) (> z_22 z_31)) (&& (= x_13 1) (> z_22 z_13))))
(=> (&& (= r_23 0) (= x_23 1)) (|| (&& (= x_24 1) (> z_23 z_24)) (&& (= x_22 1) (> z_23 z_22)) (&& (= x_32 1) (> z_23 z_32)) (&& (= x_14 1) (> z_23 z_14))))
(=> (&& (= r_24 0) (= x_24 1)) (|| (&& (= x_25 1) (> z_24 z_25)) (&& (= x_23 1) (> z_24 z_23)) (&& (= x_33 1) (> z_24 z_33)) (&& (= x_15 1) (> z_24 z_15))))
(=> (&& (= r_25 0) (= x_25 1)) (|| (&& (= x_26 1) (> z_25 z_26)) (&& (= x_24 1) (> z_25 z_24)) (&& (= x_34 1) (> z_25 z_34)) (&& (= x_16 1) (> z_25 z_16))))
(=> (&& (= r_26 0) (= x_26 1)) (|| (&& (= x_25 1) (> z_26 z_25)) (&& (= x_35 1) (> z_26 z_35)) (&& (= x_17 1) (> z_26 z_17))))
(=> (&& (= r_27 0) (= x_27 1)) (|| (&& (= x_28 1) (> z_27 z_28)) (&& (= x_36 1) (> z_27 z_36)) (&& (= x_18 1) (> z_27 z_18))))
(=> (&& (= r_28 0) (= x_28 1)) (|| (&& (= x_29 1) (> z_28 z_29)) (&& (= x_27 1) (> z_28 z_27)) (&& (= x_37 1) (> z_28 z_37)) (&& (= x_19 1) (> z_28 z_19))))
(=> (&& (= r_29 0) (= x_29 1)) (|| (&& (= x_30 1) (> z_29 z_30)) (&& (= x_28 1) (> z_29 z_28)) (&& (= x_38 1) (> z_29 z_38)) (&& (= x_20 1) (> z_29 z_20))))
(=> (&& (= r_30 0) (= x_30 1)) (|| (&& (= x_31 1) (> z_30 z_31)) (&& (= x_29 1) (> z_30 z_29)) (&& (= x_39 1) (> z_30 z_39)) (&& (= x_21 1) (> z_30 z_21))))
(=> (&& (= r_31 0) (= x_31 1)) (|| (&& (= x_32 1) (> z_31 z_32)) (&& (= x_30 1) (> z_31 z_30)) (&& (= x_40 1) (> z_31 z_40)) (&& (= x_22 1) (> z_31 z_22))))
(=> (&& (= r_32 0) (= x_32 1)) (|| (&& (= x_33 1) (> z_32 z_33)) (&& (= x_31 1) (> z_32 z_31)) (&& (= x_41 1) (> z_32 z_41)) (&& (= x_23 1) (> z_32 z_23))))
(=> (&& (= r_33 0) (= x_33 1)) (|| (&& (= x_34 1) (> z_33 z_34)) (&& (= x_32 1) (> z_33 z_32)) (&& (= x_42 1) (> z_33 z_42)) (&& (= x_24 1) (> z_33 z_24))))
(=> (&& (= r_34 0) (= x_34 1)) (|| (&& (= x_35 1) (> z_34 z_35)) (&& (= x_33 1) (> z_34 z_33)) (&& (= x_43 1) (> z_34 z_43)) (&& (= x_25 1) (> z_34 z_25))))
(=> (&& (= r_35 0) (= x_35 1)) (|| (&& (= x_34 1) (> z_35 z_34)) (&& (= x_44 1) (> z_35 z_44)) (&& (= x_26 1) (> z_35 z_26))))
(=> (&& (= r_36 0) (= x_36 1)) (|| (&& (= x_37 1) (> z_36 z_37)) (&& (= x_45 1) (> z_36 z_45)) (&& (= x_27 1) (> z_36 z_27))))
(=> (&& (= r_37 0) (= x_37 1)) (|| (&& (= x_38 1) (> z_37 z_38)) (&& (= x_36 1) (> z_37 z_36)) (&& (= x_46 1) (> z_37 z_46)) (&& (= x_28 1) (> z_37 z_28))))
(=> (&& (= r_38 0) (= x_38 1)) (|| (&& (= x_39 1) (> z_38 z_39)) (&& (= x_37 1) (> z_38 z_37)) (&& (= x_47 1) (> z_38 z_47)) (&& (= x_29 1) (> z_38 z_29))))
(=> (&& (= r_39 0) (= x_39 1)) (|| (&& (= x_40 1) (> z_39 z_40)) (&& (= x_38 1) (> z_39 z_38)) (&& (= x_48 1) (> z_39 z_48)) (&& (= x_30 1) (> z_39 z_30))))
(=> (&& (= r_40 0) (= x_40 1)) (|| (&& (= x_41 1) (> z_40 z_41)) (&& (= x_39 1) (> z_40 z_39)) (&& (= x_49 1) (> z_40 z_49)) (&& (= x_31 1) (> z_40 z_31))))
(=> (&& (= r_41 0) (= x_41 1)) (|| (&& (= x_42 1) (> z_41 z_42)) (&& (= x_40 1) (> z_41 z_40)) (&& (= x_50 1) (> z_41 z_50)) (&& (= x_32 1) (> z_41 z_32))))
(=> (&& (= r_42 0) (= x_42 1)) (|| (&& (= x_43 1) (> z_42 z_43)) (&& (= x_41 1) (> z_42 z_41)) (&& (= x_51 1) (> z_42 z_51)) (&& (= x_33 1) (> z_42 z_33))))
(=> (&& (= r_43 0) (= x_43 1)) (|| (&& (= x_44 1) (> z_43 z_44)) (&& (= x_42 1) (> z_43 z_42)) (&& (= x_52 1) (> z_43 z_52)) (&& (= x_34 1) (> z_43 z_34))))
(=> (&& (= r_44 0) (= x_44 1)) (|| (&& (= x_43 1) (> z_44 z_43)) (&& (= x_53 1) (> z_44 z_53)) (&& (= x_35 1) (> z_44 z_35))))
(=> (&& (= r_45 0) (= x_45 1)) (|| (&& (= x_46 1) (> z_45 z_46)) (&& (= x_54 1) (> z_45 z_54)) (&& (= x_36 1) (> z_45 z_36))))
(=> (&& (= r_46 0) (= x_46 1)) (|| (&& (= x_47 1) (> z_46 z_47)) (&& (= x_45 1) (> z_46 z_45)) (&& (= x_55 1) (> z_46 z_55)) (&& (= x_37 1) (> z_46 z_37))))
(=> (&& (= r_47 0) (= x_47 1)) (|| (&& (= x_48 1) (> z_47 z_48)) (&& (= x_46 1) (> z_47 z_46)) (&& (= x_56 1) (> z_47 z_56)) (&& (= x_38 1) (> z_47 z_38))))
(=> (&& (= r_48 0) (= x_48 1)) (|| (&& (= x_49 1) (> z_48 z_49)) (&& (= x_47 1) (> z_48 z_47)) (&& (= x_57 1) (> z_48 z_57)) (&& (= x_39 1) (> z_48 z_39))))
(=> (&& (= r_49 0) (= x_49 1)) (|| (&& (= x_50 1) (> z_49 z_50)) (&& (= x_48 1) (> z_49 z_48)) (&& (= x_58 1) (> z_49 z_58)) (&& (= x_40 1) (> z_49 z_40))))
(=> (&& (= r_50 0) (= x_50 1)) (|| (&& (= x_51 1) (> z_50 z_51)) (&& (= x_49 1) (> z_50 z_49)) (&& (= x_59 1) (> z_50 z_59)) (&& (= x_41 1) (> z_50 z_41))))
(=> (&& (= r_51 0) (= x_51 1)) (|| (&& (= x_52 1) (> z_51 z_52)) (&& (= x_50 1) (> z_51 z_50)) (&& (= x_60 1) (> z_51 z_60)) (&& (= x_42 1) (> z_51 z_42))))
(=> (&& (= r_52 0) (= x_52 1)) (|| (&& (= x_53 1) (> z_52 z_53)) (&& (= x_51 1) (> z_52 z_51)) (&& (= x_61 1) (> z_52 z_61)) (&& (= x_43 1) (> z_52 z_43))))
(=> (&& (= r_53 0) (= x_53 1)) (|| (&& (= x_52 1) (> z_53 z_52)) (&& (= x_62 1) (> z_53 z_62)) (&& (= x_44 1) (> z_53 z_44))))
(=> (&& (= r_54 0) (= x_54 1)) (|| (&& (= x_55 1) (> z_54 z_55)) (&& (= x_63 1) (> z_54 z_63)) (&& (= x_45 1) (> z_54 z_45))))
(=> (&& (= r_55 0) (= x_55 1)) (|| (&& (= x_56 1) (> z_55 z_56)) (&& (= x_54 1) (> z_55 z_54)) (&& (= x_64 1) (> z_55 z_64)) (&& (= x_46 1) (> z_55 z_46))))
(=> (&& (= r_56 0) (= x_56 1)) (|| (&& (= x_57 1) (> z_56 z_57)) (&& (= x_55 1) (> z_56 z_55)) (&& (= x_65 1) (> z_56 z_65)) (&& (= x_47 1) (> z_56 z_47))))
(=> (&& (= r_57 0) (= x_57 1)) (|| (&& (= x_58 1) (> z_57 z_58)) (&& (= x_56 1) (> z_57 z_56)) (&& (= x_66 1) (> z_57 z_66)) (&& (= x_48 1) (> z_57 z_48))))
(=> (&& (= r_58 0) (= x_58 1)) (|| (&& (= x_59 1) (> z_58 z_59)) (&& (= x_57 1) (> z_58 z_57)) (&& (= x_67 1) (> z_58 z_67)) (&& (= x_49 1) (> z_58 z_49))))
(=> (&& (= r_59 0) (= x_59 1)) (|| (&& (= x_60 1) (> z_59 z_60)) (&& (= x_58 1) (> z_59 z_58)) (&& (= x_68 1) (> z_59 z_68)) (&& (= x_50 1) (> z_59 z_50))))
(=> (&& (= r_60 0) (= x_60 1)) (|| (&& (= x_61 1) (> z_60 z_61)) (&& (= x_59 1) (> z_60 z_59)) (&& (= x_69 1) (> z_60 z_69)) (&& (= x_51 1) (> z_60 z_51))))
(=> (&& (= r_61 0) (= x_61 1)) (|| (&& (= x_62 1) (> z_61 z_62)) (&& (= x_60 1) (> z_61 z_60)) (&& (= x_70 1) (> z_61 z_70)) (&& (= x_52 1) (> z_61 z_52))))
(=> (&& (= r_62 0) (= x_62 1)) (|| (&& (= x_61 1) (> z_62 z_61)) (&& (= x_71 1) (> z_62 z_71)) (&& (= x_53 1) (> z_62 z_53))))
(=> (&& (= r_63 0) (= x_63 1)) (|| (&& (= x_64 1) (> z_63 z_64)) (&& (= x_72 1) (> z_63 z_72)) (&& (= x_54 1) (> z_63 z_54))))
(=> (&& (= r_64 0) (= x_64 1)) (|| (&& (= x_65 1) (> z_64 z_65)) (&& (= x_63 1) (> z_64 z_63)) (&& (= x_73 1) (> z_64 z_73)) (&& (= x_55 1) (> z_64 z_55))))
(=> (&& (= r_65 0) (= x_65 1)) (|| (&& (= x_66 1) (> z_65 z_66)) (&& (= x_64 1) (> z_65 z_64)) (&& (= x_74 1) (> z_65 z_74)) (&& (= x_56 1) (> z_65 z_56))))
(=> (&& (= r_66 0) (= x_66 1)) (|| (&& (= x_67 1) (> z_66 z_67)) (&& (= x_65 1) (> z_66 z_65)) (&& (= x_75 1) (> z_66 z_75)) (&& (= x_57 1) (> z_66 z_57))))
(=> (&& (= r_67 0) (= x_67 1)) (|| (&& (= x_68 1) (> z_67 z_68)) (&& (= x_66 1) (> z_67 z_66)) (&& (= x_76 1) (> z_67 z_76)) (&& (= x_58 1) (> z_67 z_58))))
(=> (&& (= r_68 0) (= x_68 1)) (|| (&& (= x_69 1) (> z_68 z_69)) (&& (= x_67 1) (> z_68 z_67)) (&& (= x_77 1) (> z_68 z_77)) (&& (= x_59 1) (> z_68 z_59))))
(=> (&& (= r_69 0) (= x_69 1)) (|| (&& (= x_70 1) (> z_69 z_70)) (&& (= x_68 1) (> z_69 z_68)) (&& (= x_78 1) (> z_69 z_78)) (&& (= x_60 1) (> z_69 z_60))))
(=> (&& (= r_70 0) (= x_70 1)) (|| (&& (= x_71 1) (> z_70 z_71)) (&& (= x_69 1) (> z_70 z_69)) (&& (= x_79 1) (> z_70 z_79)) (&& (= x_61 1) (> z_70 z_61))))
(=> (&& (= r_71 0) (= x_71 1)) (|| (&& (= x_70 1) (> z_71 z_70)) (&& (= x_80 1) (> z_71 z_80)) (&& (= x_62 1) (> z_71 z_62))))
(=> (&& (= r_72 0) (= x_72 1)) (|| (&& (= x_73 1) (> z_72 z_73)) (&& (= x_63 1) (> z_72 z_63))))
(=> (&& (= r_73 0) (= x_73 1)) (|| (&& (= x_74 1) (> z_73 z_74)) (&& (= x_72 1) (> z_73 z_72)) (&& (= x_64 1) (> z_73 z_64))))
(=> (&& (= r_74 0) (= x_74 1)) (|| (&& (= x_75 1) (> z_74 z_75)) (&& (= x_73 1) (> z_74 z_73)) (&& (= x_65 1) (> z_74 z_65))))
(=> (&& (= r_75 0) (= x_75 1)) (|| (&& (= x_76 1) (> z_75 z_76)) (&& (= x_74 1) (> z_75 z_74)) (&& (= x_66 1) (> z_75 z_66))))
(=> (&& (= r_76 0) (= x_76 1)) (|| (&& (= x_77 1) (> z_76 z_77)) (&& (= x_75 1) (> z_76 z_75)) (&& (= x_67 1) (> z_76 z_67))))
(=> (&& (= r_77 0) (= x_77 1)) (|| (&& (= x_78 1) (> z_77 z_78)) (&& (= x_76 1) (> z_77 z_76)) (&& (= x_68 1) (> z_77 z_68))))
(=> (&& (= r_78 0) (= x_78 1)) (|| (&& (= x_79 1) (> z_78 z_79)) (&& (= x_77 1) (> z_78 z_77)) (&& (= x_69 1) (> z_78 z_69))))
(=> (&& (= r_79 0) (= x_79 1)) (|| (&& (= x_80 1) (> z_79 z_80)) (&& (= x_78 1) (> z_79 z_78)) (&& (= x_70 1) (> z_79 z_70))))
(=> (&& (= r_80 0) (= x_80 1)) (|| (&& (= x_79 1) (> z_80 z_79)) (&& (= x_71 1) (> z_80 z_71))))
(= row_0 0)
(|| (&& (= x_0 x_1) (= row_1 (+ row_0 1))) (&& (!= x_0 x_1) (= row_1 0)))
(|| (&& (= x_1 x_2) (= row_2 (+ row_1 1))) (&& (!= x_1 x_2) (= row_2 0)))
(|| (&& (= x_2 x_3) (= row_3 (+ row_2 1))) (&& (!= x_2 x_3) (= row_3 0)))
(|| (&& (= x_3 x_4) (= row_4 (+ row_3 1))) (&& (!= x_3 x_4) (= row_4 0)))
(|| (&& (= x_4 x_5) (= row_5 (+ row_4 1))) (&& (!= x_4 x_5) (= row_5 0)))
(|| (&& (= x_5 x_6) (= row_6 (+ row_5 1))) (&& (!= x_5 x_6) (= row_6 0)))
(|| (&& (= x_6 x_7) (= row_7 (+ row_6 1))) (&& (!= x_6 x_7) (= row_7 0)))
(|| (&& (= x_7 x_8) (= row_8 (+ row_7 1))) (&& (!= x_7 x_8) (= row_8 0)))
(= row_9 0)
(|| (&& (= x_9 x_10) (= row_10 (+ row_9 1))) (&& (!= x_9 x_10) (= row_10 0)))
(|| (&& (= x_10 x_11) (= row_11 (+ row_10 1))) (&& (!= x_10 x_11) (= row_11 0)))
(|| (&& (= x_11 x_12) (= row_12 (+ row_11 1))) (&& (!= x_11 x_12) (= row_12 0)))
(|| (&& (= x_12 x_13) (= row_13 (+ row_12 1))) (&& (!= x_12 x_13) (= row_13 0)))
(|| (&& (= x_13 x_14) (= row_14 (+ row_13 1))) (&& (!= x_13 x_14) (= row_14 0)))
(|| (&& (= x_14 x_15) (= row_15 (+ row_14 1))) (&& (!= x_14 x_15) (= row_15 0)))
(|| (&& (= x_15 x_16) (= row_16 (+ row_15 1))) (&& (!= x_15 x_16) (= row_16 0)))
(|| (&& (= x_16 x_17) (= row_17 (+ row_16 1))) (&& (!= x_16 x_17) (= row_17 0)))
(= row_18 0)
(|| (&& (= x_18 x_19) (= row_19 (+ row_18 1))) (&& (!= x_18 x_19) (= row_19 0)))
(|| (&& (= x_19 x_20) (= row_20 (+ row_19 1))) (&& (!= x_19 x_20) (= row_20 0)))
(|| (&& (= x_20 x_21) (= row_21 (+ row_20 1))) (&& (!= x_20 x_21) (= row_21 0)))
(|| (&& (= x_21 x_22) (= row_22 (+ row_21 1))) (&& (!= x_21 x_22) (= row_22 0)))
(|| (&& (= x_22 x_23) (= row_23 (+ row_22 1))) (&& (!= x_22 x_23) (= row_23 0)))
(|| (&& (= x_23 x_24) (= row_24 (+ row_23 1))) (&& (!= x_23 x_24) (= row_24 0)))
(|| (&& (= x_24 x_25) (= row_25 (+ row_24 1))) (&& (!= x_24 x_25) (= row_25 0)))
(|| (&& (= x_25 x_26) (= row_26 (+ row_25 1))) (&& (!= x_25 x_26) (= row_26 0)))
(= row_27 0)
(|| (&& (= x_27 x_28) (= row_28 (+ row_27 1))) (&& (!= x_27 x_28) (= row_28 0)))
(|| (&& (= x_28 x_29) (= row_29 (+ row_28 1))) (&& (!= x_28 x_29) (= row_29 0)))
(|| (&& (= x_29 x_30) (= row_30 (+ row_29 1))) (&& (!= x_29 x_30) (= row_30 0)))
(|| (&& (= x_30 x_31) (= row_31 (+ row_30 1))) (&& (!= x_30 x_31) (= row_31 0)))
(|| (&& (= x_31 x_32) (= row_32 (+ row_31 1))) (&& (!= x_31 x_32) (= row_32 0)))
(|| (&& (= x_32 x_33) (= row_33 (+ row_32 1))) (&& (!= x_32 x_33) (= row_33 0)))
(|| (&& (= x_33 x_34) (= row_34 (+ row_33 1))) (&& (!= x_33 x_34) (= row_34 0)))
(|| (&& (= x_34 x_35) (= row_35 (+ row_34 1))) (&& (!= x_34 x_35) (= row_35 0)))
(= row_36 0)
(|| (&& (= x_36 x_37) (= row_37 (+ row_36 1))) (&& (!= x_36 x_37) (= row_37 0)))
(|| (&& (= x_37 x_38) (= row_38 (+ row_37 1))) (&& (!= x_37 x_38) (= row_38 0)))
(|| (&& (= x_38 x_39) (= row_39 (+ row_38 1))) (&& (!= x_38 x_39) (= row_39 0)))
(|| (&& (= x_39 x_40) (= row_40 (+ row_39 1))) (&& (!= x_39 x_40) (= row_40 0)))
(|| (&& (= x_40 x_41) (= row_41 (+ row_40 1))) (&& (!= x_40 x_41) (= row_41 0)))
(|| (&& (= x_41 x_42) (= row_42 (+ row_41 1))) (&& (!= x_41 x_42) (= row_42 0)))
(|| (&& (= x_42 x_43) (= row_43 (+ row_42 1))) (&& (!= x_42 x_43) (= row_43 0)))
(|| (&& (= x_43 x_44) (= row_44 (+ row_43 1))) (&& (!= x_43 x_44) (= row_44 0)))
(= row_45 0)
(|| (&& (= x_45 x_46) (= row_46 (+ row_45 1))) (&& (!= x_45 x_46) (= row_46 0)))
(|| (&& (= x_46 x_47) (= row_47 (+ row_46 1))) (&& (!= x_46 x_47) (= row_47 0)))
(|| (&& (= x_47 x_48) (= row_48 (+ row_47 1))) (&& (!= x_47 x_48) (= row_48 0)))
(|| (&& (= x_48 x_49) (= row_49 (+ row_48 1))) (&& (!= x_48 x_49) (= row_49 0)))
(|| (&& (= x_49 x_50) (= row_50 (+ row_49 1))) (&& (!= x_49 x_50) (= row_50 0)))
(|| (&& (= x_50 x_51) (= row_51 (+ row_50 1))) (&& (!= x_50 x_51) (= row_51 0)))
(|| (&& (= x_51 x_52) (= row_52 (+ row_51 1))) (&& (!= x_51 x_52) (= row_52 0)))
(|| (&& (= x_52 x_53) (= row_53 (+ row_52 1))) (&& (!= x_52 x_53) (= row_53 0)))
(= row_54 0)
(|| (&& (= x_54 x_55) (= row_55 (+ row_54 1))) (&& (!= x_54 x_55) (= row_55 0)))
(|| (&& (= x_55 x_56) (= row_56 (+ row_55 1))) (&& (!= x_55 x_56) (= row_56 0)))
(|| (&& (= x_56 x_57) (= row_57 (+ row_56 1))) (&& (!= x_56 x_57) (= row_57 0)))
(|| (&& (= x_57 x_58) (= row_58 (+ row_57 1))) (&& (!= x_57 x_58) (= row_58 0)))
(|| (&& (= x_58 x_59) (= row_59 (+ row_58 1))) (&& (!= x_58 x_59) (= row_59 0)))
(|| (&& (= x_59 x_60) (= row_60 (+ row_59 1))) (&& (!= x_59 x_60) (= row_60 0)))
(|| (&& (= x_60 x_61) (= row_61 (+ row_60 1))) (&& (!= x_60 x_61) (= row_61 0)))
(|| (&& (= x_61 x_62) (= row_62 (+ row_61 1))) (&& (!= x_61 x_62) (= row_62 0)))
(= row_63 0)
(|| (&& (= x_63 x_64) (= row_64 (+ row_63 1))) (&& (!= x_63 x_64) (= row_64 0)))
(|| (&& (= x_64 x_65) (= row_65 (+ row_64 1))) (&& (!= x_64 x_65) (= row_65 0)))
(|| (&& (= x_65 x_66) (= row_66 (+ row_65 1))) (&& (!= x_65 x_66) (= row_66 0)))
(|| (&& (= x_66 x_67) (= row_67 (+ row_66 1))) (&& (!= x_66 x_67) (= row_67 0)))
(|| (&& (= x_67 x_68) (= row_68 (+ row_67 1))) (&& (!= x_67 x_68) (= row_68 0)))
(|| (&& (= x_68 x_69) (= row_69 (+ row_68 1))) (&& (!= x_68 x_69) (= row_69 0)))
(|| (&& (= x_69 x_70) (= row_70 (+ row_69 1))) (&& (!= x_69 x_70) (= row_70 0)))
(|| (&& (= x_70 x_71) (= row_71 (+ row_70 1))) (&& (!= x_70 x_71) (= row_71 0)))
(= row_72 0)
(|| (&& (= x_72 x_73) (= row_73 (+ row_72 1))) (&& (!= x_72 x_73) (= row_73 0)))
(|| (&& (= x_73 x_74) (= row_74 (+ row_73 1))) (&& (!= x_73 x_74) (= row_74 0)))
(|| (&& (= x_74 x_75) (= row_75 (+ row_74 1))) (&& (!= x_74 x_75) (= row_75 0)))
(|| (&& (= x_75 x_76) (= row_76 (+ row_75 1))) (&& (!= x_75 x_76) (= row_76 0)))
(|| (&& (= x_76 x_77) (= row_77 (+ row_76 1))) (&& (!= x_76 x_77) (= row_77 0)))
(|| (&& (= x_77 x_78) (= row_78 (+ row_77 1))) (&& (!= x_77 x_78) (= row_78 0)))
(|| (&& (= x_78 x_79) (= row_79 (+ row_78 1))) (&& (!= x_78 x_79) (= row_79 0)))
(|| (&& (= x_79 x_80) (= row_80 (+ row_79 1))) (&& (!= x_79 x_80) (= row_80 0)))
(= col_0 0)
(= col_1 0)
(= col_2 0)
(= col_3 0)
(= col_4 0)
(= col_5 0)
(= col_6 0)
(= col_7 0)
(= col_8 0)
(|| (&& (= x_0 x_9) (= col_9 (+ col_0 1))) (&& (!= x_0 x_9) (= col_9 0)))
(|| (&& (= x_1 x_10) (= col_10 (+ col_1 1))) (&& (!= x_1 x_10) (= col_10 0)))
(|| (&& (= x_2 x_11) (= col_11 (+ col_2 1))) (&& (!= x_2 x_11) (= col_11 0)))
(|| (&& (= x_3 x_12) (= col_12 (+ col_3 1))) (&& (!= x_3 x_12) (= col_12 0)))
(|| (&& (= x_4 x_13) (= col_13 (+ col_4 1))) (&& (!= x_4 x_13) (= col_13 0)))
(|| (&& (= x_5 x_14) (= col_14 (+ col_5 1))) (&& (!= x_5 x_14) (= col_14 0)))
(|| (&& (= x_6 x_15) (= col_15 (+ col_6 1))) (&& (!= x_6 x_15) (= col_15 0)))
(|| (&& (= x_7 x_16) (= col_16 (+ col_7 1))) (&& (!= x_7 x_16) (= col_16 0)))
(|| (&& (= x_8 x_17) (= col_17 (+ col_8 1))) (&& (!= x_8 x_17) (= col_17 0)))
(|| (&& (= x_9 x_18) (= col_18 (+ col_9 1))) (&& (!= x_9 x_18) (= col_18 0)))
(|| (&& (= x_10 x_19) (= col_19 (+ col_10 1))) (&& (!= x_10 x_19) (= col_19 0)))
(|| (&& (= x_11 x_20) (= col_20 (+ col_11 1))) (&& (!= x_11 x_20) (= col_20 0)))
(|| (&& (= x_12 x_21) (= col_21 (+ col_12 1))) (&& (!= x_12 x_21) (= col_21 0)))
(|| (&& (= x_13 x_22) (= col_22 (+ col_13 1))) (&& (!= x_13 x_22) (= col_22 0)))
(|| (&& (= x_14 x_23) (= col_23 (+ col_14 1))) (&& (!= x_14 x_23) (= col_23 0)))
(|| (&& (= x_15 x_24) (= col_24 (+ col_15 1))) (&& (!= x_15 x_24) (= col_24 0)))
(|| (&& (= x_16 x_25) (= col_25 (+ col_16 1))) (&& (!= x_16 x_25) (= col_25 0)))
(|| (&& (= x_17 x_26) (= col_26 (+ col_17 1))) (&& (!= x_17 x_26) (= col_26 0)))
(|| (&& (= x_18 x_27) (= col_27 (+ col_18 1))) (&& (!= x_18 x_27) (= col_27 0)))
(|| (&& (= x_19 x_28) (= col_28 (+ col_19 1))) (&& (!= x_19 x_28) (= col_28 0)))
(|| (&& (= x_20 x_29) (= col_29 (+ col_20 1))) (&& (!= x_20 x_29) (= col_29 0)))
(|| (&& (= x_21 x_30) (= col_30 (+ col_21 1))) (&& (!= x_21 x_30) (= col_30 0)))
(|| (&& (= x_22 x_31) (= col_31 (+ col_22 1))) (&& (!= x_22 x_31) (= col_31 0)))
(|| (&& (= x_23 x_32) (= col_32 (+ col_23 1))) (&& (!= x_23 x_32) (= col_32 0)))
(|| (&& (= x_24 x_33) (= col_33 (+ col_24 1))) (&& (!= x_24 x_33) (= col_33 0)))
(|| (&& (= x_25 x_34) (= col_34 (+ col_25 1))) (&& (!= x_25 x_34) (= col_34 0)))
(|| (&& (= x_26 x_35) (= col_35 (+ col_26 1))) (&& (!= x_26 x_35) (= col_35 0)))
(|| (&& (= x_27 x_36) (= col_36 (+ col_27 1))) (&& (!= x_27 x_36) (= col_36 0)))
(|| (&& (= x_28 x_37) (= col_37 (+ col_28 1))) (&& (!= x_28 x_37) (= col_37 0)))
(|| (&& (= x_29 x_38) (= col_38 (+ col_29 1))) (&& (!= x_29 x_38) (= col_38 0)))
(|| (&& (= x_30 x_39) (= col_39 (+ col_30 1))) (&& (!= x_30 x_39) (= col_39 0)))
(|| (&& (= x_31 x_40) (= col_40 (+ col_31 1))) (&& (!= x_31 x_40) (= col_40 0)))
(|| (&& (= x_32 x_41) (= col_41 (+ col_32 1))) (&& (!= x_32 x_41) (= col_41 0)))
(|| (&& (= x_33 x_42) (= col_42 (+ col_33 1))) (&& (!= x_33 x_42) (= col_42 0)))
(|| (&& (= x_34 x_43) (= col_43 (+ col_34 1))) (&& (!= x_34 x_43) (= col_43 0)))
(|| (&& (= x_35 x_44) (= col_44 (+ col_35 1))) (&& (!= x_35 x_44) (= col_44 0)))
(|| (&& (= x_36 x_45) (= col_45 (+ col_36 1))) (&& (!= x_36 x_45) (= col_45 0)))
(|| (&& (= x_37 x_46) (= col_46 (+ col_37 1))) (&& (!= x_37 x_46) (= col_46 0)))
(|| (&& (= x_38 x_47) (= col_47 (+ col_38 1))) (&& (!= x_38 x_47) (= col_47 0)))
(|| (&& (= x_39 x_48) (= col_48 (+ col_39 1))) (&& (!= x_39 x_48) (= col_48 0)))
(|| (&& (= x_40 x_49) (= col_49 (+ col_40 1))) (&& (!= x_40 x_49) (= col_49 0)))
(|| (&& (= x_41 x_50) (= col_50 (+ col_41 1))) (&& (!= x_41 x_50) (= col_50 0)))
(|| (&& (= x_42 x_51) (= col_51 (+ col_42 1))) (&& (!= x_42 x_51) (= col_51 0)))
(|| (&& (= x_43 x_52) (= col_52 (+ col_43 1))) (&& (!= x_43 x_52) (= col_52 0)))
(|| (&& (= x_44 x_53) (= col_53 (+ col_44 1))) (&& (!= x_44 x_53) (= col_53 0)))
(|| (&& (= x_45 x_54) (= col_54 (+ col_45 1))) (&& (!= x_45 x_54) (= col_54 0)))
(|| (&& (= x_46 x_55) (= col_55 (+ col_46 1))) (&& (!= x_46 x_55) (= col_55 0)))
(|| (&& (= x_47 x_56) (= col_56 (+ col_47 1))) (&& (!= x_47 x_56) (= col_56 0)))
(|| (&& (= x_48 x_57) (= col_57 (+ col_48 1))) (&& (!= x_48 x_57) (= col_57 0)))
(|| (&& (= x_49 x_58) (= col_58 (+ col_49 1))) (&& (!= x_49 x_58) (= col_58 0)))
(|| (&& (= x_50 x_59) (= col_59 (+ col_50 1))) (&& (!= x_50 x_59) (= col_59 0)))
(|| (&& (= x_51 x_60) (= col_60 (+ col_51 1))) (&& (!= x_51 x_60) (= col_60 0)))
(|| (&& (= x_52 x_61) (= col_61 (+ col_52 1))) (&& (!= x_52 x_61) (= col_61 0)))
(|| (&& (= x_53 x_62) (= col_62 (+ col_53 1))) (&& (!= x_53 x_62) (= col_62 0)))
(|| (&& (= x_54 x_63) (= col_63 (+ col_54 1))) (&& (!= x_54 x_63) (= col_63 0)))
(|| (&& (= x_55 x_64) (= col_64 (+ col_55 1))) (&& (!= x_55 x_64) (= col_64 0)))
(|| (&& (= x_56 x_65) (= col_65 (+ col_56 1))) (&& (!= x_56 x_65) (= col_65 0)))
(|| (&& (= x_57 x_66) (= col_66 (+ col_57 1))) (&& (!= x_57 x_66) (= col_66 0)))
(|| (&& (= x_58 x_67) (= col_67 (+ col_58 1))) (&& (!= x_58 x_67) (= col_67 0)))
(|| (&& (= x_59 x_68) (= col_68 (+ col_59 1))) (&& (!= x_59 x_68) (= col_68 0)))
(|| (&& (= x_60 x_69) (= col_69 (+ col_60 1))) (&& (!= x_60 x_69) (= col_69 0)))
(|| (&& (= x_61 x_70) (= col_70 (+ col_61 1))) (&& (!= x_61 x_70) (= col_70 0)))
(|| (&& (= x_62 x_71) (= col_71 (+ col_62 1))) (&& (!= x_62 x_71) (= col_71 0)))
(|| (&& (= x_63 x_72) (= col_72 (+ col_63 1))) (&& (!= x_63 x_72) (= col_72 0)))
(|| (&& (= x_64 x_73) (= col_73 (+ col_64 1))) (&& (!= x_64 x_73) (= col_73 0)))
(|| (&& (= x_65 x_74) (= col_74 (+ col_65 1))) (&& (!= x_65 x_74) (= col_74 0)))
(|| (&& (= x_66 x_75) (= col_75 (+ col_66 1))) (&& (!= x_66 x_75) (= col_75 0)))
(|| (&& (= x_67 x_76) (= col_76 (+ col_67 1))) (&& (!= x_67 x_76) (= col_76 0)))
(|| (&& (= x_68 x_77) (= col_77 (+ col_68 1))) (&& (!= x_68 x_77) (= col_77 0)))
(|| (&& (= x_69 x_78) (= col_78 (+ col_69 1))) (&& (!= x_69 x_78) (= col_78 0)))
(|| (&& (= x_70 x_79) (= col_79 (+ col_70 1))) (&& (!= x_70 x_79) (= col_79 0)))
(|| (&& (= x_71 x_80) (= col_80 (+ col_71 1))) (&& (!= x_71 x_80) (= col_80 0)))
(= (+ r_0 r_1 r_2 r_3 r_4 r_5 r_6 r_7 r_8 r_9 r_10 r_11 r_12 r_13 r_14 r_15 r_16 r_17 r_18 r_19 r_20 r_21 r_22 r_23 r_24 r_25 r_26 r_27 r_28 r_29 r_30 r_31 r_32 r_33 r_34 r_35 r_36 r_37 r_38 r_39 r_40 r_41 r_42 r_43 r_44 r_45 r_46 r_47 r_48 r_49 r_50 r_51 r_52 r_53 r_54 r_55 r_56 r_57 r_58 r_59 r_60 r_61 r_62 r_63 r_64 r_65 r_66 r_67 r_68 r_69 r_70 r_71 r_72 r_73 r_74 r_75 r_76 r_77 r_78 r_79 r_80) 1)
(<= (+ x_0 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) 33)
https://ideone.com/EWZZXN
language:
Node.js (node 11.12.0)
created:
4 years ago
visibility:
public

Share or Embed source code

Discover > Sphere Engine API

The brand new service which powers Ideone!

Discover > IDE Widget

Widget for compiling and running the source code in a web browser!