c 1 _r c 2 _r_1 c 3 _r_2 c 4 _r_6 c 5 _r_1_3_4 c 6 _r_1_3_5 c 7 _r_2_32_33 c 8 _r_2_32_34 c 9 _r_2_32_35 c 10 _r_2_32_36 c 11 _r_6_14 c 12 _r_6_16 c 13 _r_6_17 c 14 _r_6_18 c 15 _r_6_14_19_20 c 16 _r_6_14_19_21 c 17 _r_6_14_19_22 c 18 _r_6_14_19_23 c 19 _r_6_16_24_25 c 20 _r_6_16_24_26 c 21 _r_6_16_24_27 c 22 _r_6_18_28_29 c 23 _r_6_18_28_30 c 24 _r_6_18_28_31 p cnf 24 35 1 0 -2 1 0 -1 2 0 -3 1 0 -1 3 0 -4 1 0 -1 4 0 -5 2 0 -6 2 0 -2 5 6 0 -7 3 0 -8 3 0 -9 3 0 -10 3 0 -3 7 8 9 10 0 -11 4 0 -12 4 0 -13 4 0 -4 13 0 -14 4 0 -15 11 0 -16 11 0 -17 11 0 -18 11 0 -11 15 16 17 18 0 -19 12 0 -20 12 0 -21 12 0 -12 19 20 21 0 -22 14 0 -23 14 0 -24 14 0 -14 22 23 24 0 5 -6 0 -12 -14 -10 0