(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_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_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_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_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_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_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_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_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_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_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) (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_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_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_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_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_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_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_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_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_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_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_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) 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) 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) 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) 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) 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) 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) 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) 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) 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) 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) 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) 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) 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) 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) 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) 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) 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) 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) 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) 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) 1)) (check-sat) (exit)