(set-info :smt-lib-version 2.6) (set-logic QF_LIA) (set-info :category "crafted") (set-info :status unsat) (declare-fun p_0_0 () Int) (declare-fun p_0_1 () Int) (declare-fun p_0_2 () Int) (declare-fun p_0_3 () Int) (declare-fun p_0_4 () Int) (declare-fun p_0_5 () Int) (declare-fun p_0_6 () Int) (declare-fun p_0_7 () Int) (declare-fun p_0_8 () Int) (declare-fun p_0_9 () Int) (declare-fun p_0_10 () Int) (declare-fun p_0_11 () Int) (declare-fun p_0_12 () Int) (declare-fun p_0_13 () Int) (declare-fun p_0_14 () Int) (declare-fun p_0_15 () Int) (declare-fun p_1_0 () Int) (declare-fun p_1_1 () Int) (declare-fun p_1_2 () Int) (declare-fun p_1_3 () Int) (declare-fun p_1_4 () Int) (declare-fun p_1_5 () Int) (declare-fun p_1_6 () Int) (declare-fun p_1_7 () Int) (declare-fun p_1_8 () Int) (declare-fun p_1_9 () Int) (declare-fun p_1_10 () Int) (declare-fun p_1_11 () Int) (declare-fun p_1_12 () Int) (declare-fun p_1_13 () Int) (declare-fun p_1_14 () Int) (declare-fun p_1_15 () Int) (declare-fun p_2_0 () Int) (declare-fun p_2_1 () Int) (declare-fun p_2_2 () Int) (declare-fun p_2_3 () Int) (declare-fun p_2_4 () Int) (declare-fun p_2_5 () Int) (declare-fun p_2_6 () Int) (declare-fun p_2_7 () Int) (declare-fun p_2_8 () Int) (declare-fun p_2_9 () Int) (declare-fun p_2_10 () Int) (declare-fun p_2_11 () Int) (declare-fun p_2_12 () Int) (declare-fun p_2_13 () Int) (declare-fun p_2_14 () Int) (declare-fun p_2_15 () Int) (declare-fun p_3_0 () Int) (declare-fun p_3_1 () Int) (declare-fun p_3_2 () Int) (declare-fun p_3_3 () Int) (declare-fun p_3_4 () Int) (declare-fun p_3_5 () Int) (declare-fun p_3_6 () Int) (declare-fun p_3_7 () Int) (declare-fun p_3_8 () Int) (declare-fun p_3_9 () Int) (declare-fun p_3_10 () Int) (declare-fun p_3_11 () Int) (declare-fun p_3_12 () Int) (declare-fun p_3_13 () Int) (declare-fun p_3_14 () Int) (declare-fun p_3_15 () Int) (declare-fun p_4_0 () Int) (declare-fun p_4_1 () Int) (declare-fun p_4_2 () Int) (declare-fun p_4_3 () Int) (declare-fun p_4_4 () Int) (declare-fun p_4_5 () Int) (declare-fun p_4_6 () Int) (declare-fun p_4_7 () Int) (declare-fun p_4_8 () Int) (declare-fun p_4_9 () Int) (declare-fun p_4_10 () Int) (declare-fun p_4_11 () Int) (declare-fun p_4_12 () Int) (declare-fun p_4_13 () Int) (declare-fun p_4_14 () Int) (declare-fun p_4_15 () Int) (declare-fun p_5_0 () Int) (declare-fun p_5_1 () Int) (declare-fun p_5_2 () Int) (declare-fun p_5_3 () Int) (declare-fun p_5_4 () Int) (declare-fun p_5_5 () Int) (declare-fun p_5_6 () Int) (declare-fun p_5_7 () Int) (declare-fun p_5_8 () Int) (declare-fun p_5_9 () Int) (declare-fun p_5_10 () Int) (declare-fun p_5_11 () Int) (declare-fun p_5_12 () Int) (declare-fun p_5_13 () Int) (declare-fun p_5_14 () Int) (declare-fun p_5_15 () Int) (declare-fun p_6_0 () Int) (declare-fun p_6_1 () Int) (declare-fun p_6_2 () Int) (declare-fun p_6_3 () Int) (declare-fun p_6_4 () Int) (declare-fun p_6_5 () Int) (declare-fun p_6_6 () Int) (declare-fun p_6_7 () Int) (declare-fun p_6_8 () Int) (declare-fun p_6_9 () Int) (declare-fun p_6_10 () Int) (declare-fun p_6_11 () Int) (declare-fun p_6_12 () Int) (declare-fun p_6_13 () Int) (declare-fun p_6_14 () Int) (declare-fun p_6_15 () Int) (declare-fun p_7_0 () Int) (declare-fun p_7_1 () Int) (declare-fun p_7_2 () Int) (declare-fun p_7_3 () Int) (declare-fun p_7_4 () Int) (declare-fun p_7_5 () Int) (declare-fun p_7_6 () Int) (declare-fun p_7_7 () Int) (declare-fun p_7_8 () Int) (declare-fun p_7_9 () Int) (declare-fun p_7_10 () Int) (declare-fun p_7_11 () Int) (declare-fun p_7_12 () Int) (declare-fun p_7_13 () Int) (declare-fun p_7_14 () Int) (declare-fun p_7_15 () Int) (declare-fun p_8_0 () Int) (declare-fun p_8_1 () Int) (declare-fun p_8_2 () Int) (declare-fun p_8_3 () Int) (declare-fun p_8_4 () Int) (declare-fun p_8_5 () Int) (declare-fun p_8_6 () Int) (declare-fun p_8_7 () Int) (declare-fun p_8_8 () Int) (declare-fun p_8_9 () Int) (declare-fun p_8_10 () Int) (declare-fun p_8_11 () Int) (declare-fun p_8_12 () Int) (declare-fun p_8_13 () Int) (declare-fun p_8_14 () Int) (declare-fun p_8_15 () Int) (declare-fun p_9_0 () Int) (declare-fun p_9_1 () Int) (declare-fun p_9_2 () Int) (declare-fun p_9_3 () Int) (declare-fun p_9_4 () Int) (declare-fun p_9_5 () Int) (declare-fun p_9_6 () Int) (declare-fun p_9_7 () Int) (declare-fun p_9_8 () Int) (declare-fun p_9_9 () Int) (declare-fun p_9_10 () Int) (declare-fun p_9_11 () Int) (declare-fun p_9_12 () Int) (declare-fun p_9_13 () Int) (declare-fun p_9_14 () Int) (declare-fun p_9_15 () Int) (declare-fun p_10_0 () Int) (declare-fun p_10_1 () Int) (declare-fun p_10_2 () Int) (declare-fun p_10_3 () Int) (declare-fun p_10_4 () Int) (declare-fun p_10_5 () Int) (declare-fun p_10_6 () Int) (declare-fun p_10_7 () Int) (declare-fun p_10_8 () Int) (declare-fun p_10_9 () Int) (declare-fun p_10_10 () Int) (declare-fun p_10_11 () Int) (declare-fun p_10_12 () Int) (declare-fun p_10_13 () Int) (declare-fun p_10_14 () Int) (declare-fun p_10_15 () Int) (declare-fun p_11_0 () Int) (declare-fun p_11_1 () Int) (declare-fun p_11_2 () Int) (declare-fun p_11_3 () Int) (declare-fun p_11_4 () Int) (declare-fun p_11_5 () Int) (declare-fun p_11_6 () Int) (declare-fun p_11_7 () Int) (declare-fun p_11_8 () Int) (declare-fun p_11_9 () Int) (declare-fun p_11_10 () Int) (declare-fun p_11_11 () Int) (declare-fun p_11_12 () Int) (declare-fun p_11_13 () Int) (declare-fun p_11_14 () Int) (declare-fun p_11_15 () Int) (declare-fun p_12_0 () Int) (declare-fun p_12_1 () Int) (declare-fun p_12_2 () Int) (declare-fun p_12_3 () Int) (declare-fun p_12_4 () Int) (declare-fun p_12_5 () Int) (declare-fun p_12_6 () Int) (declare-fun p_12_7 () Int) (declare-fun p_12_8 () Int) (declare-fun p_12_9 () Int) (declare-fun p_12_10 () Int) (declare-fun p_12_11 () Int) (declare-fun p_12_12 () Int) (declare-fun p_12_13 () Int) (declare-fun p_12_14 () Int) (declare-fun p_12_15 () Int) (declare-fun p_13_0 () Int) (declare-fun p_13_1 () Int) (declare-fun p_13_2 () Int) (declare-fun p_13_3 () Int) (declare-fun p_13_4 () Int) (declare-fun p_13_5 () Int) (declare-fun p_13_6 () Int) (declare-fun p_13_7 () Int) (declare-fun p_13_8 () Int) (declare-fun p_13_9 () Int) (declare-fun p_13_10 () Int) (declare-fun p_13_11 () Int) (declare-fun p_13_12 () Int) (declare-fun p_13_13 () Int) (declare-fun p_13_14 () Int) (declare-fun p_13_15 () Int) (declare-fun p_14_0 () Int) (declare-fun p_14_1 () Int) (declare-fun p_14_2 () Int) (declare-fun p_14_3 () Int) (declare-fun p_14_4 () Int) (declare-fun p_14_5 () Int) (declare-fun p_14_6 () Int) (declare-fun p_14_7 () Int) (declare-fun p_14_8 () Int) (declare-fun p_14_9 () Int) (declare-fun p_14_10 () Int) (declare-fun p_14_11 () Int) (declare-fun p_14_12 () Int) (declare-fun p_14_13 () Int) (declare-fun p_14_14 () Int) (declare-fun p_14_15 () Int) (declare-fun p_15_0 () Int) (declare-fun p_15_1 () Int) (declare-fun p_15_2 () Int) (declare-fun p_15_3 () Int) (declare-fun p_15_4 () Int) (declare-fun p_15_5 () Int) (declare-fun p_15_6 () Int) (declare-fun p_15_7 () Int) (declare-fun p_15_8 () Int) (declare-fun p_15_9 () Int) (declare-fun p_15_10 () Int) (declare-fun p_15_11 () Int) (declare-fun p_15_12 () Int) (declare-fun p_15_13 () Int) (declare-fun p_15_14 () Int) (declare-fun p_15_15 () Int) (declare-fun p_16_0 () Int) (declare-fun p_16_1 () Int) (declare-fun p_16_2 () Int) (declare-fun p_16_3 () Int) (declare-fun p_16_4 () Int) (declare-fun p_16_5 () Int) (declare-fun p_16_6 () Int) (declare-fun p_16_7 () Int) (declare-fun p_16_8 () Int) (declare-fun p_16_9 () Int) (declare-fun p_16_10 () Int) (declare-fun p_16_11 () Int) (declare-fun p_16_12 () Int) (declare-fun p_16_13 () Int) (declare-fun p_16_14 () Int) (declare-fun p_16_15 () Int) (assert (>= p_0_0 0)) (assert (<= p_0_0 1)) (assert (>= p_0_1 0)) (assert (<= p_0_1 1)) (assert (>= p_0_2 0)) (assert (<= p_0_2 1)) (assert (>= p_0_3 0)) (assert (<= p_0_3 1)) (assert (>= p_0_4 0)) (assert (<= p_0_4 1)) (assert (>= p_0_5 0)) (assert (<= p_0_5 1)) (assert (>= p_0_6 0)) (assert (<= p_0_6 1)) (assert (>= p_0_7 0)) (assert (<= p_0_7 1)) (assert (>= p_0_8 0)) (assert (<= p_0_8 1)) (assert (>= p_0_9 0)) (assert (<= p_0_9 1)) (assert (>= p_0_10 0)) (assert (<= p_0_10 1)) (assert (>= p_0_11 0)) (assert (<= p_0_11 1)) (assert (>= p_0_12 0)) (assert (<= p_0_12 1)) (assert (>= p_0_13 0)) (assert (<= p_0_13 1)) (assert (>= p_0_14 0)) (assert (<= p_0_14 1)) (assert (>= p_0_15 0)) (assert (<= p_0_15 1)) (assert (>= p_1_0 0)) (assert (<= p_1_0 1)) (assert (>= p_1_1 0)) (assert (<= p_1_1 1)) (assert (>= p_1_2 0)) (assert (<= p_1_2 1)) (assert (>= p_1_3 0)) (assert (<= p_1_3 1)) (assert (>= p_1_4 0)) (assert (<= p_1_4 1)) (assert (>= p_1_5 0)) (assert (<= p_1_5 1)) (assert (>= p_1_6 0)) (assert (<= p_1_6 1)) (assert (>= p_1_7 0)) (assert (<= p_1_7 1)) (assert (>= p_1_8 0)) (assert (<= p_1_8 1)) (assert (>= p_1_9 0)) (assert (<= p_1_9 1)) (assert (>= p_1_10 0)) (assert (<= p_1_10 1)) (assert (>= p_1_11 0)) (assert (<= p_1_11 1)) (assert (>= p_1_12 0)) (assert (<= p_1_12 1)) (assert (>= p_1_13 0)) (assert (<= p_1_13 1)) (assert (>= p_1_14 0)) (assert (<= p_1_14 1)) (assert (>= p_1_15 0)) (assert (<= p_1_15 1)) (assert (>= p_2_0 0)) (assert (<= p_2_0 1)) (assert (>= p_2_1 0)) (assert (<= p_2_1 1)) (assert (>= p_2_2 0)) (assert (<= p_2_2 1)) (assert (>= p_2_3 0)) (assert (<= p_2_3 1)) (assert (>= p_2_4 0)) (assert (<= p_2_4 1)) (assert (>= p_2_5 0)) (assert (<= p_2_5 1)) (assert (>= p_2_6 0)) (assert (<= p_2_6 1)) (assert (>= p_2_7 0)) (assert (<= p_2_7 1)) (assert (>= p_2_8 0)) (assert (<= p_2_8 1)) (assert (>= p_2_9 0)) (assert (<= p_2_9 1)) (assert (>= p_2_10 0)) (assert (<= p_2_10 1)) (assert (>= p_2_11 0)) (assert (<= p_2_11 1)) (assert (>= p_2_12 0)) (assert (<= p_2_12 1)) (assert (>= p_2_13 0)) (assert (<= p_2_13 1)) (assert (>= p_2_14 0)) (assert (<= p_2_14 1)) (assert (>= p_2_15 0)) (assert (<= p_2_15 1)) (assert (>= p_3_0 0)) (assert (<= p_3_0 1)) (assert (>= p_3_1 0)) (assert (<= p_3_1 1)) (assert (>= p_3_2 0)) (assert (<= p_3_2 1)) (assert (>= p_3_3 0)) (assert (<= p_3_3 1)) (assert (>= p_3_4 0)) (assert (<= p_3_4 1)) (assert (>= p_3_5 0)) (assert (<= p_3_5 1)) (assert (>= p_3_6 0)) (assert (<= p_3_6 1)) (assert (>= p_3_7 0)) (assert (<= p_3_7 1)) (assert (>= p_3_8 0)) (assert (<= p_3_8 1)) (assert (>= p_3_9 0)) (assert (<= p_3_9 1)) (assert (>= p_3_10 0)) (assert (<= p_3_10 1)) (assert (>= p_3_11 0)) (assert (<= p_3_11 1)) (assert (>= p_3_12 0)) (assert (<= p_3_12 1)) (assert (>= p_3_13 0)) (assert (<= p_3_13 1)) (assert (>= p_3_14 0)) (assert (<= p_3_14 1)) (assert (>= p_3_15 0)) (assert (<= p_3_15 1)) (assert (>= p_4_0 0)) (assert (<= p_4_0 1)) (assert (>= p_4_1 0)) (assert (<= p_4_1 1)) (assert (>= p_4_2 0)) (assert (<= p_4_2 1)) (assert (>= p_4_3 0)) (assert (<= p_4_3 1)) (assert (>= p_4_4 0)) (assert (<= p_4_4 1)) (assert (>= p_4_5 0)) (assert (<= p_4_5 1)) (assert (>= p_4_6 0)) (assert (<= p_4_6 1)) (assert (>= p_4_7 0)) (assert (<= p_4_7 1)) (assert (>= p_4_8 0)) (assert (<= p_4_8 1)) (assert (>= p_4_9 0)) (assert (<= p_4_9 1)) (assert (>= p_4_10 0)) (assert (<= p_4_10 1)) (assert (>= p_4_11 0)) (assert (<= p_4_11 1)) (assert (>= p_4_12 0)) (assert (<= p_4_12 1)) (assert (>= p_4_13 0)) (assert (<= p_4_13 1)) (assert (>= p_4_14 0)) (assert (<= p_4_14 1)) (assert (>= p_4_15 0)) (assert (<= p_4_15 1)) (assert (>= p_5_0 0)) (assert (<= p_5_0 1)) (assert (>= p_5_1 0)) (assert (<= p_5_1 1)) (assert (>= p_5_2 0)) (assert (<= p_5_2 1)) (assert (>= p_5_3 0)) (assert (<= p_5_3 1)) (assert (>= p_5_4 0)) (assert (<= p_5_4 1)) (assert (>= p_5_5 0)) (assert (<= p_5_5 1)) (assert (>= p_5_6 0)) (assert (<= p_5_6 1)) (assert (>= p_5_7 0)) (assert (<= p_5_7 1)) (assert (>= p_5_8 0)) (assert (<= p_5_8 1)) (assert (>= p_5_9 0)) (assert (<= p_5_9 1)) (assert (>= p_5_10 0)) (assert (<= p_5_10 1)) (assert (>= p_5_11 0)) (assert (<= p_5_11 1)) (assert (>= p_5_12 0)) (assert (<= p_5_12 1)) (assert (>= p_5_13 0)) (assert (<= p_5_13 1)) (assert (>= p_5_14 0)) (assert (<= p_5_14 1)) (assert (>= p_5_15 0)) (assert (<= p_5_15 1)) (assert (>= p_6_0 0)) (assert (<= p_6_0 1)) (assert (>= p_6_1 0)) (assert (<= p_6_1 1)) (assert (>= p_6_2 0)) (assert (<= p_6_2 1)) (assert (>= p_6_3 0)) (assert (<= p_6_3 1)) (assert (>= p_6_4 0)) (assert (<= p_6_4 1)) (assert (>= p_6_5 0)) (assert (<= p_6_5 1)) (assert (>= p_6_6 0)) (assert (<= p_6_6 1)) (assert (>= p_6_7 0)) (assert (<= p_6_7 1)) (assert (>= p_6_8 0)) (assert (<= p_6_8 1)) (assert (>= p_6_9 0)) (assert (<= p_6_9 1)) (assert (>= p_6_10 0)) (assert (<= p_6_10 1)) (assert (>= p_6_11 0)) (assert (<= p_6_11 1)) (assert (>= p_6_12 0)) (assert (<= p_6_12 1)) (assert (>= p_6_13 0)) (assert (<= p_6_13 1)) (assert (>= p_6_14 0)) (assert (<= p_6_14 1)) (assert (>= p_6_15 0)) (assert (<= p_6_15 1)) (assert (>= p_7_0 0)) (assert (<= p_7_0 1)) (assert (>= p_7_1 0)) (assert (<= p_7_1 1)) (assert (>= p_7_2 0)) (assert (<= p_7_2 1)) (assert (>= p_7_3 0)) (assert (<= p_7_3 1)) (assert (>= p_7_4 0)) (assert (<= p_7_4 1)) (assert (>= p_7_5 0)) (assert (<= p_7_5 1)) (assert (>= p_7_6 0)) (assert (<= p_7_6 1)) (assert (>= p_7_7 0)) (assert (<= p_7_7 1)) (assert (>= p_7_8 0)) (assert (<= p_7_8 1)) (assert (>= p_7_9 0)) (assert (<= p_7_9 1)) (assert (>= p_7_10 0)) (assert (<= p_7_10 1)) (assert (>= p_7_11 0)) (assert (<= p_7_11 1)) (assert (>= p_7_12 0)) (assert (<= p_7_12 1)) (assert (>= p_7_13 0)) (assert (<= p_7_13 1)) (assert (>= p_7_14 0)) (assert (<= p_7_14 1)) (assert (>= p_7_15 0)) (assert (<= p_7_15 1)) (assert (>= p_8_0 0)) (assert (<= p_8_0 1)) (assert (>= p_8_1 0)) (assert (<= p_8_1 1)) (assert (>= p_8_2 0)) (assert (<= p_8_2 1)) (assert (>= p_8_3 0)) (assert (<= p_8_3 1)) (assert (>= p_8_4 0)) (assert (<= p_8_4 1)) (assert (>= p_8_5 0)) (assert (<= p_8_5 1)) (assert (>= p_8_6 0)) (assert (<= p_8_6 1)) (assert (>= p_8_7 0)) (assert (<= p_8_7 1)) (assert (>= p_8_8 0)) (assert (<= p_8_8 1)) (assert (>= p_8_9 0)) (assert (<= p_8_9 1)) (assert (>= p_8_10 0)) (assert (<= p_8_10 1)) (assert (>= p_8_11 0)) (assert (<= p_8_11 1)) (assert (>= p_8_12 0)) (assert (<= p_8_12 1)) (assert (>= p_8_13 0)) (assert (<= p_8_13 1)) (assert (>= p_8_14 0)) (assert (<= p_8_14 1)) (assert (>= p_8_15 0)) (assert (<= p_8_15 1)) (assert (>= p_9_0 0)) (assert (<= p_9_0 1)) (assert (>= p_9_1 0)) (assert (<= p_9_1 1)) (assert (>= p_9_2 0)) (assert (<= p_9_2 1)) (assert (>= p_9_3 0)) (assert (<= p_9_3 1)) (assert (>= p_9_4 0)) (assert (<= p_9_4 1)) (assert (>= p_9_5 0)) (assert (<= p_9_5 1)) (assert (>= p_9_6 0)) (assert (<= p_9_6 1)) (assert (>= p_9_7 0)) (assert (<= p_9_7 1)) (assert (>= p_9_8 0)) (assert (<= p_9_8 1)) (assert (>= p_9_9 0)) (assert (<= p_9_9 1)) (assert (>= p_9_10 0)) (assert (<= p_9_10 1)) (assert (>= p_9_11 0)) (assert (<= p_9_11 1)) (assert (>= p_9_12 0)) (assert (<= p_9_12 1)) (assert (>= p_9_13 0)) (assert (<= p_9_13 1)) (assert (>= p_9_14 0)) (assert (<= p_9_14 1)) (assert (>= p_9_15 0)) (assert (<= p_9_15 1)) (assert (>= p_10_0 0)) (assert (<= p_10_0 1)) (assert (>= p_10_1 0)) (assert (<= p_10_1 1)) (assert (>= p_10_2 0)) (assert (<= p_10_2 1)) (assert (>= p_10_3 0)) (assert (<= p_10_3 1)) (assert (>= p_10_4 0)) (assert (<= p_10_4 1)) (assert (>= p_10_5 0)) (assert (<= p_10_5 1)) (assert (>= p_10_6 0)) (assert (<= p_10_6 1)) (assert (>= p_10_7 0)) (assert (<= p_10_7 1)) (assert (>= p_10_8 0)) (assert (<= p_10_8 1)) (assert (>= p_10_9 0)) (assert (<= p_10_9 1)) (assert (>= p_10_10 0)) (assert (<= p_10_10 1)) (assert (>= p_10_11 0)) (assert (<= p_10_11 1)) (assert (>= p_10_12 0)) (assert (<= p_10_12 1)) (assert (>= p_10_13 0)) (assert (<= p_10_13 1)) (assert (>= p_10_14 0)) (assert (<= p_10_14 1)) (assert (>= p_10_15 0)) (assert (<= p_10_15 1)) (assert (>= p_11_0 0)) (assert (<= p_11_0 1)) (assert (>= p_11_1 0)) (assert (<= p_11_1 1)) (assert (>= p_11_2 0)) (assert (<= p_11_2 1)) (assert (>= p_11_3 0)) (assert (<= p_11_3 1)) (assert (>= p_11_4 0)) (assert (<= p_11_4 1)) (assert (>= p_11_5 0)) (assert (<= p_11_5 1)) (assert (>= p_11_6 0)) (assert (<= p_11_6 1)) (assert (>= p_11_7 0)) (assert (<= p_11_7 1)) (assert (>= p_11_8 0)) (assert (<= p_11_8 1)) (assert (>= p_11_9 0)) (assert (<= p_11_9 1)) (assert (>= p_11_10 0)) (assert (<= p_11_10 1)) (assert (>= p_11_11 0)) (assert (<= p_11_11 1)) (assert (>= p_11_12 0)) (assert (<= p_11_12 1)) (assert (>= p_11_13 0)) (assert (<= p_11_13 1)) (assert (>= p_11_14 0)) (assert (<= p_11_14 1)) (assert (>= p_11_15 0)) (assert (<= p_11_15 1)) (assert (>= p_12_0 0)) (assert (<= p_12_0 1)) (assert (>= p_12_1 0)) (assert (<= p_12_1 1)) (assert (>= p_12_2 0)) (assert (<= p_12_2 1)) (assert (>= p_12_3 0)) (assert (<= p_12_3 1)) (assert (>= p_12_4 0)) (assert (<= p_12_4 1)) (assert (>= p_12_5 0)) (assert (<= p_12_5 1)) (assert (>= p_12_6 0)) (assert (<= p_12_6 1)) (assert (>= p_12_7 0)) (assert (<= p_12_7 1)) (assert (>= p_12_8 0)) (assert (<= p_12_8 1)) (assert (>= p_12_9 0)) (assert (<= p_12_9 1)) (assert (>= p_12_10 0)) (assert (<= p_12_10 1)) (assert (>= p_12_11 0)) (assert (<= p_12_11 1)) (assert (>= p_12_12 0)) (assert (<= p_12_12 1)) (assert (>= p_12_13 0)) (assert (<= p_12_13 1)) (assert (>= p_12_14 0)) (assert (<= p_12_14 1)) (assert (>= p_12_15 0)) (assert (<= p_12_15 1)) (assert (>= p_13_0 0)) (assert (<= p_13_0 1)) (assert (>= p_13_1 0)) (assert (<= p_13_1 1)) (assert (>= p_13_2 0)) (assert (<= p_13_2 1)) (assert (>= p_13_3 0)) (assert (<= p_13_3 1)) (assert (>= p_13_4 0)) (assert (<= p_13_4 1)) (assert (>= p_13_5 0)) (assert (<= p_13_5 1)) (assert (>= p_13_6 0)) (assert (<= p_13_6 1)) (assert (>= p_13_7 0)) (assert (<= p_13_7 1)) (assert (>= p_13_8 0)) (assert (<= p_13_8 1)) (assert (>= p_13_9 0)) (assert (<= p_13_9 1)) (assert (>= p_13_10 0)) (assert (<= p_13_10 1)) (assert (>= p_13_11 0)) (assert (<= p_13_11 1)) (assert (>= p_13_12 0)) (assert (<= p_13_12 1)) (assert (>= p_13_13 0)) (assert (<= p_13_13 1)) (assert (>= p_13_14 0)) (assert (<= p_13_14 1)) (assert (>= p_13_15 0)) (assert (<= p_13_15 1)) (assert (>= p_14_0 0)) (assert (<= p_14_0 1)) (assert (>= p_14_1 0)) (assert (<= p_14_1 1)) (assert (>= p_14_2 0)) (assert (<= p_14_2 1)) (assert (>= p_14_3 0)) (assert (<= p_14_3 1)) (assert (>= p_14_4 0)) (assert (<= p_14_4 1)) (assert (>= p_14_5 0)) (assert (<= p_14_5 1)) (assert (>= p_14_6 0)) (assert (<= p_14_6 1)) (assert (>= p_14_7 0)) (assert (<= p_14_7 1)) (assert (>= p_14_8 0)) (assert (<= p_14_8 1)) (assert (>= p_14_9 0)) (assert (<= p_14_9 1)) (assert (>= p_14_10 0)) (assert (<= p_14_10 1)) (assert (>= p_14_11 0)) (assert (<= p_14_11 1)) (assert (>= p_14_12 0)) (assert (<= p_14_12 1)) (assert (>= p_14_13 0)) (assert (<= p_14_13 1)) (assert (>= p_14_14 0)) (assert (<= p_14_14 1)) (assert (>= p_14_15 0)) (assert (<= p_14_15 1)) (assert (>= p_15_0 0)) (assert (<= p_15_0 1)) (assert (>= p_15_1 0)) (assert (<= p_15_1 1)) (assert (>= p_15_2 0)) (assert (<= p_15_2 1)) (assert (>= p_15_3 0)) (assert (<= p_15_3 1)) (assert (>= p_15_4 0)) (assert (<= p_15_4 1)) (assert (>= p_15_5 0)) (assert (<= p_15_5 1)) (assert (>= p_15_6 0)) (assert (<= p_15_6 1)) (assert (>= p_15_7 0)) (assert (<= p_15_7 1)) (assert (>= p_15_8 0)) (assert (<= p_15_8 1)) (assert (>= p_15_9 0)) (assert (<= p_15_9 1)) (assert (>= p_15_10 0)) (assert (<= p_15_10 1)) (assert (>= p_15_11 0)) (assert (<= p_15_11 1)) (assert (>= p_15_12 0)) (assert (<= p_15_12 1)) (assert (>= p_15_13 0)) (assert (<= p_15_13 1)) (assert (>= p_15_14 0)) (assert (<= p_15_14 1)) (assert (>= p_15_15 0)) (assert (<= p_15_15 1)) (assert (>= p_16_0 0)) (assert (<= p_16_0 1)) (assert (>= p_16_1 0)) (assert (<= p_16_1 1)) (assert (>= p_16_2 0)) (assert (<= p_16_2 1)) (assert (>= p_16_3 0)) (assert (<= p_16_3 1)) (assert (>= p_16_4 0)) (assert (<= p_16_4 1)) (assert (>= p_16_5 0)) (assert (<= p_16_5 1)) (assert (>= p_16_6 0)) (assert (<= p_16_6 1)) (assert (>= p_16_7 0)) (assert (<= p_16_7 1)) (assert (>= p_16_8 0)) (assert (<= p_16_8 1)) (assert (>= p_16_9 0)) (assert (<= p_16_9 1)) (assert (>= p_16_10 0)) (assert (<= p_16_10 1)) (assert (>= p_16_11 0)) (assert (<= p_16_11 1)) (assert (>= p_16_12 0)) (assert (<= p_16_12 1)) (assert (>= p_16_13 0)) (assert (<= p_16_13 1)) (assert (>= p_16_14 0)) (assert (<= p_16_14 1)) (assert (>= p_16_15 0)) (assert (<= p_16_15 1)) (assert (>= (+ p_0_0 p_0_1 p_0_2 p_0_3 p_0_4 p_0_5 p_0_6 p_0_7 p_0_8 p_0_9 p_0_10 p_0_11 p_0_12 p_0_13 p_0_14 p_0_15) 1)) (assert (>= (+ p_1_0 p_1_1 p_1_2 p_1_3 p_1_4 p_1_5 p_1_6 p_1_7 p_1_8 p_1_9 p_1_10 p_1_11 p_1_12 p_1_13 p_1_14 p_1_15) 1)) (assert (>= (+ p_2_0 p_2_1 p_2_2 p_2_3 p_2_4 p_2_5 p_2_6 p_2_7 p_2_8 p_2_9 p_2_10 p_2_11 p_2_12 p_2_13 p_2_14 p_2_15) 1)) (assert (>= (+ p_3_0 p_3_1 p_3_2 p_3_3 p_3_4 p_3_5 p_3_6 p_3_7 p_3_8 p_3_9 p_3_10 p_3_11 p_3_12 p_3_13 p_3_14 p_3_15) 1)) (assert (>= (+ p_4_0 p_4_1 p_4_2 p_4_3 p_4_4 p_4_5 p_4_6 p_4_7 p_4_8 p_4_9 p_4_10 p_4_11 p_4_12 p_4_13 p_4_14 p_4_15) 1)) (assert (>= (+ p_5_0 p_5_1 p_5_2 p_5_3 p_5_4 p_5_5 p_5_6 p_5_7 p_5_8 p_5_9 p_5_10 p_5_11 p_5_12 p_5_13 p_5_14 p_5_15) 1)) (assert (>= (+ p_6_0 p_6_1 p_6_2 p_6_3 p_6_4 p_6_5 p_6_6 p_6_7 p_6_8 p_6_9 p_6_10 p_6_11 p_6_12 p_6_13 p_6_14 p_6_15) 1)) (assert (>= (+ p_7_0 p_7_1 p_7_2 p_7_3 p_7_4 p_7_5 p_7_6 p_7_7 p_7_8 p_7_9 p_7_10 p_7_11 p_7_12 p_7_13 p_7_14 p_7_15) 1)) (assert (>= (+ p_8_0 p_8_1 p_8_2 p_8_3 p_8_4 p_8_5 p_8_6 p_8_7 p_8_8 p_8_9 p_8_10 p_8_11 p_8_12 p_8_13 p_8_14 p_8_15) 1)) (assert (>= (+ p_9_0 p_9_1 p_9_2 p_9_3 p_9_4 p_9_5 p_9_6 p_9_7 p_9_8 p_9_9 p_9_10 p_9_11 p_9_12 p_9_13 p_9_14 p_9_15) 1)) (assert (>= (+ p_10_0 p_10_1 p_10_2 p_10_3 p_10_4 p_10_5 p_10_6 p_10_7 p_10_8 p_10_9 p_10_10 p_10_11 p_10_12 p_10_13 p_10_14 p_10_15) 1)) (assert (>= (+ p_11_0 p_11_1 p_11_2 p_11_3 p_11_4 p_11_5 p_11_6 p_11_7 p_11_8 p_11_9 p_11_10 p_11_11 p_11_12 p_11_13 p_11_14 p_11_15) 1)) (assert (>= (+ p_12_0 p_12_1 p_12_2 p_12_3 p_12_4 p_12_5 p_12_6 p_12_7 p_12_8 p_12_9 p_12_10 p_12_11 p_12_12 p_12_13 p_12_14 p_12_15) 1)) (assert (>= (+ p_13_0 p_13_1 p_13_2 p_13_3 p_13_4 p_13_5 p_13_6 p_13_7 p_13_8 p_13_9 p_13_10 p_13_11 p_13_12 p_13_13 p_13_14 p_13_15) 1)) (assert (>= (+ p_14_0 p_14_1 p_14_2 p_14_3 p_14_4 p_14_5 p_14_6 p_14_7 p_14_8 p_14_9 p_14_10 p_14_11 p_14_12 p_14_13 p_14_14 p_14_15) 1)) (assert (>= (+ p_15_0 p_15_1 p_15_2 p_15_3 p_15_4 p_15_5 p_15_6 p_15_7 p_15_8 p_15_9 p_15_10 p_15_11 p_15_12 p_15_13 p_15_14 p_15_15) 1)) (assert (>= (+ p_16_0 p_16_1 p_16_2 p_16_3 p_16_4 p_16_5 p_16_6 p_16_7 p_16_8 p_16_9 p_16_10 p_16_11 p_16_12 p_16_13 p_16_14 p_16_15) 1)) (assert (<= (+ p_0_0 p_1_0 p_2_0 p_3_0 p_4_0 p_5_0 p_6_0 p_7_0 p_8_0 p_9_0 p_10_0 p_11_0 p_12_0 p_13_0 p_14_0 p_15_0 p_16_0) 1)) (assert (<= (+ p_0_1 p_1_1 p_2_1 p_3_1 p_4_1 p_5_1 p_6_1 p_7_1 p_8_1 p_9_1 p_10_1 p_11_1 p_12_1 p_13_1 p_14_1 p_15_1 p_16_1) 1)) (assert (<= (+ p_0_2 p_1_2 p_2_2 p_3_2 p_4_2 p_5_2 p_6_2 p_7_2 p_8_2 p_9_2 p_10_2 p_11_2 p_12_2 p_13_2 p_14_2 p_15_2 p_16_2) 1)) (assert (<= (+ p_0_3 p_1_3 p_2_3 p_3_3 p_4_3 p_5_3 p_6_3 p_7_3 p_8_3 p_9_3 p_10_3 p_11_3 p_12_3 p_13_3 p_14_3 p_15_3 p_16_3) 1)) (assert (<= (+ p_0_4 p_1_4 p_2_4 p_3_4 p_4_4 p_5_4 p_6_4 p_7_4 p_8_4 p_9_4 p_10_4 p_11_4 p_12_4 p_13_4 p_14_4 p_15_4 p_16_4) 1)) (assert (<= (+ p_0_5 p_1_5 p_2_5 p_3_5 p_4_5 p_5_5 p_6_5 p_7_5 p_8_5 p_9_5 p_10_5 p_11_5 p_12_5 p_13_5 p_14_5 p_15_5 p_16_5) 1)) (assert (<= (+ p_0_6 p_1_6 p_2_6 p_3_6 p_4_6 p_5_6 p_6_6 p_7_6 p_8_6 p_9_6 p_10_6 p_11_6 p_12_6 p_13_6 p_14_6 p_15_6 p_16_6) 1)) (assert (<= (+ p_0_7 p_1_7 p_2_7 p_3_7 p_4_7 p_5_7 p_6_7 p_7_7 p_8_7 p_9_7 p_10_7 p_11_7 p_12_7 p_13_7 p_14_7 p_15_7 p_16_7) 1)) (assert (<= (+ p_0_8 p_1_8 p_2_8 p_3_8 p_4_8 p_5_8 p_6_8 p_7_8 p_8_8 p_9_8 p_10_8 p_11_8 p_12_8 p_13_8 p_14_8 p_15_8 p_16_8) 1)) (assert (<= (+ p_0_9 p_1_9 p_2_9 p_3_9 p_4_9 p_5_9 p_6_9 p_7_9 p_8_9 p_9_9 p_10_9 p_11_9 p_12_9 p_13_9 p_14_9 p_15_9 p_16_9) 1)) (assert (<= (+ p_0_10 p_1_10 p_2_10 p_3_10 p_4_10 p_5_10 p_6_10 p_7_10 p_8_10 p_9_10 p_10_10 p_11_10 p_12_10 p_13_10 p_14_10 p_15_10 p_16_10) 1)) (assert (<= (+ p_0_11 p_1_11 p_2_11 p_3_11 p_4_11 p_5_11 p_6_11 p_7_11 p_8_11 p_9_11 p_10_11 p_11_11 p_12_11 p_13_11 p_14_11 p_15_11 p_16_11) 1)) (assert (<= (+ p_0_12 p_1_12 p_2_12 p_3_12 p_4_12 p_5_12 p_6_12 p_7_12 p_8_12 p_9_12 p_10_12 p_11_12 p_12_12 p_13_12 p_14_12 p_15_12 p_16_12) 1)) (assert (<= (+ p_0_13 p_1_13 p_2_13 p_3_13 p_4_13 p_5_13 p_6_13 p_7_13 p_8_13 p_9_13 p_10_13 p_11_13 p_12_13 p_13_13 p_14_13 p_15_13 p_16_13) 1)) (assert (<= (+ p_0_14 p_1_14 p_2_14 p_3_14 p_4_14 p_5_14 p_6_14 p_7_14 p_8_14 p_9_14 p_10_14 p_11_14 p_12_14 p_13_14 p_14_14 p_15_14 p_16_14) 1)) (assert (<= (+ p_0_15 p_1_15 p_2_15 p_3_15 p_4_15 p_5_15 p_6_15 p_7_15 p_8_15 p_9_15 p_10_15 p_11_15 p_12_15 p_13_15 p_14_15 p_15_15 p_16_15) 1)) (check-sat) (exit)