(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_0_16 () Int)
(declare-fun p_0_17 () Int)
(declare-fun p_0_18 () Int)
(declare-fun p_0_19 () 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_1_16 () Int)
(declare-fun p_1_17 () Int)
(declare-fun p_1_18 () Int)
(declare-fun p_1_19 () 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_2_16 () Int)
(declare-fun p_2_17 () Int)
(declare-fun p_2_18 () Int)
(declare-fun p_2_19 () 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_3_16 () Int)
(declare-fun p_3_17 () Int)
(declare-fun p_3_18 () Int)
(declare-fun p_3_19 () 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_4_16 () Int)
(declare-fun p_4_17 () Int)
(declare-fun p_4_18 () Int)
(declare-fun p_4_19 () 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_5_16 () Int)
(declare-fun p_5_17 () Int)
(declare-fun p_5_18 () Int)
(declare-fun p_5_19 () 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_6_16 () Int)
(declare-fun p_6_17 () Int)
(declare-fun p_6_18 () Int)
(declare-fun p_6_19 () 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_7_16 () Int)
(declare-fun p_7_17 () Int)
(declare-fun p_7_18 () Int)
(declare-fun p_7_19 () 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_8_16 () Int)
(declare-fun p_8_17 () Int)
(declare-fun p_8_18 () Int)
(declare-fun p_8_19 () 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_9_16 () Int)
(declare-fun p_9_17 () Int)
(declare-fun p_9_18 () Int)
(declare-fun p_9_19 () 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_10_16 () Int)
(declare-fun p_10_17 () Int)
(declare-fun p_10_18 () Int)
(declare-fun p_10_19 () 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_11_16 () Int)
(declare-fun p_11_17 () Int)
(declare-fun p_11_18 () Int)
(declare-fun p_11_19 () 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_12_16 () Int)
(declare-fun p_12_17 () Int)
(declare-fun p_12_18 () Int)
(declare-fun p_12_19 () 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_13_16 () Int)
(declare-fun p_13_17 () Int)
(declare-fun p_13_18 () Int)
(declare-fun p_13_19 () 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_14_16 () Int)
(declare-fun p_14_17 () Int)
(declare-fun p_14_18 () Int)
(declare-fun p_14_19 () 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_15_16 () Int)
(declare-fun p_15_17 () Int)
(declare-fun p_15_18 () Int)
(declare-fun p_15_19 () 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)
(declare-fun p_16_16 () Int)
(declare-fun p_16_17 () Int)
(declare-fun p_16_18 () Int)
(declare-fun p_16_19 () Int)
(declare-fun p_17_0 () Int)
(declare-fun p_17_1 () Int)
(declare-fun p_17_2 () Int)
(declare-fun p_17_3 () Int)
(declare-fun p_17_4 () Int)
(declare-fun p_17_5 () Int)
(declare-fun p_17_6 () Int)
(declare-fun p_17_7 () Int)
(declare-fun p_17_8 () Int)
(declare-fun p_17_9 () Int)
(declare-fun p_17_10 () Int)
(declare-fun p_17_11 () Int)
(declare-fun p_17_12 () Int)
(declare-fun p_17_13 () Int)
(declare-fun p_17_14 () Int)
(declare-fun p_17_15 () Int)
(declare-fun p_17_16 () Int)
(declare-fun p_17_17 () Int)
(declare-fun p_17_18 () Int)
(declare-fun p_17_19 () Int)
(declare-fun p_18_0 () Int)
(declare-fun p_18_1 () Int)
(declare-fun p_18_2 () Int)
(declare-fun p_18_3 () Int)
(declare-fun p_18_4 () Int)
(declare-fun p_18_5 () Int)
(declare-fun p_18_6 () Int)
(declare-fun p_18_7 () Int)
(declare-fun p_18_8 () Int)
(declare-fun p_18_9 () Int)
(declare-fun p_18_10 () Int)
(declare-fun p_18_11 () Int)
(declare-fun p_18_12 () Int)
(declare-fun p_18_13 () Int)
(declare-fun p_18_14 () Int)
(declare-fun p_18_15 () Int)
(declare-fun p_18_16 () Int)
(declare-fun p_18_17 () Int)
(declare-fun p_18_18 () Int)
(declare-fun p_18_19 () Int)
(declare-fun p_19_0 () Int)
(declare-fun p_19_1 () Int)
(declare-fun p_19_2 () Int)
(declare-fun p_19_3 () Int)
(declare-fun p_19_4 () Int)
(declare-fun p_19_5 () Int)
(declare-fun p_19_6 () Int)
(declare-fun p_19_7 () Int)
(declare-fun p_19_8 () Int)
(declare-fun p_19_9 () Int)
(declare-fun p_19_10 () Int)
(declare-fun p_19_11 () Int)
(declare-fun p_19_12 () Int)
(declare-fun p_19_13 () Int)
(declare-fun p_19_14 () Int)
(declare-fun p_19_15 () Int)
(declare-fun p_19_16 () Int)
(declare-fun p_19_17 () Int)
(declare-fun p_19_18 () Int)
(declare-fun p_19_19 () Int)
(declare-fun p_20_0 () Int)
(declare-fun p_20_1 () Int)
(declare-fun p_20_2 () Int)
(declare-fun p_20_3 () Int)
(declare-fun p_20_4 () Int)
(declare-fun p_20_5 () Int)
(declare-fun p_20_6 () Int)
(declare-fun p_20_7 () Int)
(declare-fun p_20_8 () Int)
(declare-fun p_20_9 () Int)
(declare-fun p_20_10 () Int)
(declare-fun p_20_11 () Int)
(declare-fun p_20_12 () Int)
(declare-fun p_20_13 () Int)
(declare-fun p_20_14 () Int)
(declare-fun p_20_15 () Int)
(declare-fun p_20_16 () Int)
(declare-fun p_20_17 () Int)
(declare-fun p_20_18 () Int)
(declare-fun p_20_19 () 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_0_16 0))
(assert (<= p_0_16 1))
(assert (>= p_0_17 0))
(assert (<= p_0_17 1))
(assert (>= p_0_18 0))
(assert (<= p_0_18 1))
(assert (>= p_0_19 0))
(assert (<= p_0_19 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_1_16 0))
(assert (<= p_1_16 1))
(assert (>= p_1_17 0))
(assert (<= p_1_17 1))
(assert (>= p_1_18 0))
(assert (<= p_1_18 1))
(assert (>= p_1_19 0))
(assert (<= p_1_19 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_2_16 0))
(assert (<= p_2_16 1))
(assert (>= p_2_17 0))
(assert (<= p_2_17 1))
(assert (>= p_2_18 0))
(assert (<= p_2_18 1))
(assert (>= p_2_19 0))
(assert (<= p_2_19 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_3_16 0))
(assert (<= p_3_16 1))
(assert (>= p_3_17 0))
(assert (<= p_3_17 1))
(assert (>= p_3_18 0))
(assert (<= p_3_18 1))
(assert (>= p_3_19 0))
(assert (<= p_3_19 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_4_16 0))
(assert (<= p_4_16 1))
(assert (>= p_4_17 0))
(assert (<= p_4_17 1))
(assert (>= p_4_18 0))
(assert (<= p_4_18 1))
(assert (>= p_4_19 0))
(assert (<= p_4_19 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_5_16 0))
(assert (<= p_5_16 1))
(assert (>= p_5_17 0))
(assert (<= p_5_17 1))
(assert (>= p_5_18 0))
(assert (<= p_5_18 1))
(assert (>= p_5_19 0))
(assert (<= p_5_19 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_6_16 0))
(assert (<= p_6_16 1))
(assert (>= p_6_17 0))
(assert (<= p_6_17 1))
(assert (>= p_6_18 0))
(assert (<= p_6_18 1))
(assert (>= p_6_19 0))
(assert (<= p_6_19 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_7_16 0))
(assert (<= p_7_16 1))
(assert (>= p_7_17 0))
(assert (<= p_7_17 1))
(assert (>= p_7_18 0))
(assert (<= p_7_18 1))
(assert (>= p_7_19 0))
(assert (<= p_7_19 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_8_16 0))
(assert (<= p_8_16 1))
(assert (>= p_8_17 0))
(assert (<= p_8_17 1))
(assert (>= p_8_18 0))
(assert (<= p_8_18 1))
(assert (>= p_8_19 0))
(assert (<= p_8_19 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_9_16 0))
(assert (<= p_9_16 1))
(assert (>= p_9_17 0))
(assert (<= p_9_17 1))
(assert (>= p_9_18 0))
(assert (<= p_9_18 1))
(assert (>= p_9_19 0))
(assert (<= p_9_19 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_10_16 0))
(assert (<= p_10_16 1))
(assert (>= p_10_17 0))
(assert (<= p_10_17 1))
(assert (>= p_10_18 0))
(assert (<= p_10_18 1))
(assert (>= p_10_19 0))
(assert (<= p_10_19 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_11_16 0))
(assert (<= p_11_16 1))
(assert (>= p_11_17 0))
(assert (<= p_11_17 1))
(assert (>= p_11_18 0))
(assert (<= p_11_18 1))
(assert (>= p_11_19 0))
(assert (<= p_11_19 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_12_16 0))
(assert (<= p_12_16 1))
(assert (>= p_12_17 0))
(assert (<= p_12_17 1))
(assert (>= p_12_18 0))
(assert (<= p_12_18 1))
(assert (>= p_12_19 0))
(assert (<= p_12_19 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_13_16 0))
(assert (<= p_13_16 1))
(assert (>= p_13_17 0))
(assert (<= p_13_17 1))
(assert (>= p_13_18 0))
(assert (<= p_13_18 1))
(assert (>= p_13_19 0))
(assert (<= p_13_19 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_14_16 0))
(assert (<= p_14_16 1))
(assert (>= p_14_17 0))
(assert (<= p_14_17 1))
(assert (>= p_14_18 0))
(assert (<= p_14_18 1))
(assert (>= p_14_19 0))
(assert (<= p_14_19 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_15_16 0))
(assert (<= p_15_16 1))
(assert (>= p_15_17 0))
(assert (<= p_15_17 1))
(assert (>= p_15_18 0))
(assert (<= p_15_18 1))
(assert (>= p_15_19 0))
(assert (<= p_15_19 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_16_16 0))
(assert (<= p_16_16 1))
(assert (>= p_16_17 0))
(assert (<= p_16_17 1))
(assert (>= p_16_18 0))
(assert (<= p_16_18 1))
(assert (>= p_16_19 0))
(assert (<= p_16_19 1))
(assert (>= p_17_0 0))
(assert (<= p_17_0 1))
(assert (>= p_17_1 0))
(assert (<= p_17_1 1))
(assert (>= p_17_2 0))
(assert (<= p_17_2 1))
(assert (>= p_17_3 0))
(assert (<= p_17_3 1))
(assert (>= p_17_4 0))
(assert (<= p_17_4 1))
(assert (>= p_17_5 0))
(assert (<= p_17_5 1))
(assert (>= p_17_6 0))
(assert (<= p_17_6 1))
(assert (>= p_17_7 0))
(assert (<= p_17_7 1))
(assert (>= p_17_8 0))
(assert (<= p_17_8 1))
(assert (>= p_17_9 0))
(assert (<= p_17_9 1))
(assert (>= p_17_10 0))
(assert (<= p_17_10 1))
(assert (>= p_17_11 0))
(assert (<= p_17_11 1))
(assert (>= p_17_12 0))
(assert (<= p_17_12 1))
(assert (>= p_17_13 0))
(assert (<= p_17_13 1))
(assert (>= p_17_14 0))
(assert (<= p_17_14 1))
(assert (>= p_17_15 0))
(assert (<= p_17_15 1))
(assert (>= p_17_16 0))
(assert (<= p_17_16 1))
(assert (>= p_17_17 0))
(assert (<= p_17_17 1))
(assert (>= p_17_18 0))
(assert (<= p_17_18 1))
(assert (>= p_17_19 0))
(assert (<= p_17_19 1))
(assert (>= p_18_0 0))
(assert (<= p_18_0 1))
(assert (>= p_18_1 0))
(assert (<= p_18_1 1))
(assert (>= p_18_2 0))
(assert (<= p_18_2 1))
(assert (>= p_18_3 0))
(assert (<= p_18_3 1))
(assert (>= p_18_4 0))
(assert (<= p_18_4 1))
(assert (>= p_18_5 0))
(assert (<= p_18_5 1))
(assert (>= p_18_6 0))
(assert (<= p_18_6 1))
(assert (>= p_18_7 0))
(assert (<= p_18_7 1))
(assert (>= p_18_8 0))
(assert (<= p_18_8 1))
(assert (>= p_18_9 0))
(assert (<= p_18_9 1))
(assert (>= p_18_10 0))
(assert (<= p_18_10 1))
(assert (>= p_18_11 0))
(assert (<= p_18_11 1))
(assert (>= p_18_12 0))
(assert (<= p_18_12 1))
(assert (>= p_18_13 0))
(assert (<= p_18_13 1))
(assert (>= p_18_14 0))
(assert (<= p_18_14 1))
(assert (>= p_18_15 0))
(assert (<= p_18_15 1))
(assert (>= p_18_16 0))
(assert (<= p_18_16 1))
(assert (>= p_18_17 0))
(assert (<= p_18_17 1))
(assert (>= p_18_18 0))
(assert (<= p_18_18 1))
(assert (>= p_18_19 0))
(assert (<= p_18_19 1))
(assert (>= p_19_0 0))
(assert (<= p_19_0 1))
(assert (>= p_19_1 0))
(assert (<= p_19_1 1))
(assert (>= p_19_2 0))
(assert (<= p_19_2 1))
(assert (>= p_19_3 0))
(assert (<= p_19_3 1))
(assert (>= p_19_4 0))
(assert (<= p_19_4 1))
(assert (>= p_19_5 0))
(assert (<= p_19_5 1))
(assert (>= p_19_6 0))
(assert (<= p_19_6 1))
(assert (>= p_19_7 0))
(assert (<= p_19_7 1))
(assert (>= p_19_8 0))
(assert (<= p_19_8 1))
(assert (>= p_19_9 0))
(assert (<= p_19_9 1))
(assert (>= p_19_10 0))
(assert (<= p_19_10 1))
(assert (>= p_19_11 0))
(assert (<= p_19_11 1))
(assert (>= p_19_12 0))
(assert (<= p_19_12 1))
(assert (>= p_19_13 0))
(assert (<= p_19_13 1))
(assert (>= p_19_14 0))
(assert (<= p_19_14 1))
(assert (>= p_19_15 0))
(assert (<= p_19_15 1))
(assert (>= p_19_16 0))
(assert (<= p_19_16 1))
(assert (>= p_19_17 0))
(assert (<= p_19_17 1))
(assert (>= p_19_18 0))
(assert (<= p_19_18 1))
(assert (>= p_19_19 0))
(assert (<= p_19_19 1))
(assert (>= p_20_0 0))
(assert (<= p_20_0 1))
(assert (>= p_20_1 0))
(assert (<= p_20_1 1))
(assert (>= p_20_2 0))
(assert (<= p_20_2 1))
(assert (>= p_20_3 0))
(assert (<= p_20_3 1))
(assert (>= p_20_4 0))
(assert (<= p_20_4 1))
(assert (>= p_20_5 0))
(assert (<= p_20_5 1))
(assert (>= p_20_6 0))
(assert (<= p_20_6 1))
(assert (>= p_20_7 0))
(assert (<= p_20_7 1))
(assert (>= p_20_8 0))
(assert (<= p_20_8 1))
(assert (>= p_20_9 0))
(assert (<= p_20_9 1))
(assert (>= p_20_10 0))
(assert (<= p_20_10 1))
(assert (>= p_20_11 0))
(assert (<= p_20_11 1))
(assert (>= p_20_12 0))
(assert (<= p_20_12 1))
(assert (>= p_20_13 0))
(assert (<= p_20_13 1))
(assert (>= p_20_14 0))
(assert (<= p_20_14 1))
(assert (>= p_20_15 0))
(assert (<= p_20_15 1))
(assert (>= p_20_16 0))
(assert (<= p_20_16 1))
(assert (>= p_20_17 0))
(assert (<= p_20_17 1))
(assert (>= p_20_18 0))
(assert (<= p_20_18 1))
(assert (>= p_20_19 0))
(assert (<= p_20_19 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 p_0_16 p_0_17 p_0_18 p_0_19) 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 p_1_16 p_1_17 p_1_18 p_1_19) 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 p_2_16 p_2_17 p_2_18 p_2_19) 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 p_3_16 p_3_17 p_3_18 p_3_19) 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 p_4_16 p_4_17 p_4_18 p_4_19) 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 p_5_16 p_5_17 p_5_18 p_5_19) 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 p_6_16 p_6_17 p_6_18 p_6_19) 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 p_7_16 p_7_17 p_7_18 p_7_19) 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 p_8_16 p_8_17 p_8_18 p_8_19) 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 p_9_16 p_9_17 p_9_18 p_9_19) 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 p_10_16 p_10_17 p_10_18 p_10_19) 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 p_11_16 p_11_17 p_11_18 p_11_19) 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 p_12_16 p_12_17 p_12_18 p_12_19) 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 p_13_16 p_13_17 p_13_18 p_13_19) 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 p_14_16 p_14_17 p_14_18 p_14_19) 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 p_15_16 p_15_17 p_15_18 p_15_19) 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 p_16_16 p_16_17 p_16_18 p_16_19) 1))
(assert (>= (+ p_17_0 p_17_1 p_17_2 p_17_3 p_17_4 p_17_5 p_17_6 p_17_7 p_17_8 p_17_9 p_17_10 p_17_11 p_17_12 p_17_13 p_17_14 p_17_15 p_17_16 p_17_17 p_17_18 p_17_19) 1))
(assert (>= (+ p_18_0 p_18_1 p_18_2 p_18_3 p_18_4 p_18_5 p_18_6 p_18_7 p_18_8 p_18_9 p_18_10 p_18_11 p_18_12 p_18_13 p_18_14 p_18_15 p_18_16 p_18_17 p_18_18 p_18_19) 1))
(assert (>= (+ p_19_0 p_19_1 p_19_2 p_19_3 p_19_4 p_19_5 p_19_6 p_19_7 p_19_8 p_19_9 p_19_10 p_19_11 p_19_12 p_19_13 p_19_14 p_19_15 p_19_16 p_19_17 p_19_18 p_19_19) 1))
(assert (>= (+ p_20_0 p_20_1 p_20_2 p_20_3 p_20_4 p_20_5 p_20_6 p_20_7 p_20_8 p_20_9 p_20_10 p_20_11 p_20_12 p_20_13 p_20_14 p_20_15 p_20_16 p_20_17 p_20_18 p_20_19) 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 p_17_0 p_18_0 p_19_0 p_20_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 p_17_1 p_18_1 p_19_1 p_20_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 p_17_2 p_18_2 p_19_2 p_20_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 p_17_3 p_18_3 p_19_3 p_20_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 p_17_4 p_18_4 p_19_4 p_20_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 p_17_5 p_18_5 p_19_5 p_20_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 p_17_6 p_18_6 p_19_6 p_20_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 p_17_7 p_18_7 p_19_7 p_20_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 p_17_8 p_18_8 p_19_8 p_20_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 p_17_9 p_18_9 p_19_9 p_20_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 p_17_10 p_18_10 p_19_10 p_20_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 p_17_11 p_18_11 p_19_11 p_20_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 p_17_12 p_18_12 p_19_12 p_20_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 p_17_13 p_18_13 p_19_13 p_20_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 p_17_14 p_18_14 p_19_14 p_20_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 p_17_15 p_18_15 p_19_15 p_20_15) 1))
(assert (<= (+ p_0_16 p_1_16 p_2_16 p_3_16 p_4_16 p_5_16 p_6_16 p_7_16 p_8_16 p_9_16 p_10_16 p_11_16 p_12_16 p_13_16 p_14_16 p_15_16 p_16_16 p_17_16 p_18_16 p_19_16 p_20_16) 1))
(assert (<= (+ p_0_17 p_1_17 p_2_17 p_3_17 p_4_17 p_5_17 p_6_17 p_7_17 p_8_17 p_9_17 p_10_17 p_11_17 p_12_17 p_13_17 p_14_17 p_15_17 p_16_17 p_17_17 p_18_17 p_19_17 p_20_17) 1))
(assert (<= (+ p_0_18 p_1_18 p_2_18 p_3_18 p_4_18 p_5_18 p_6_18 p_7_18 p_8_18 p_9_18 p_10_18 p_11_18 p_12_18 p_13_18 p_14_18 p_15_18 p_16_18 p_17_18 p_18_18 p_19_18 p_20_18) 1))
(assert (<= (+ p_0_19 p_1_19 p_2_19 p_3_19 p_4_19 p_5_19 p_6_19 p_7_19 p_8_19 p_9_19 p_10_19 p_11_19 p_12_19 p_13_19 p_14_19 p_15_19 p_16_19 p_17_19 p_18_19 p_19_19 p_20_19) 1))
(check-sat)
(exit)