c 1 v1 c 2 v2 c 3 v3 c 4 v4 c 5 v5 c 6 v6 c 7 v7 c 8 v8 c 9 v9 c 10 v10 c 11 v11 c 12 v12 c 13 v13 c 14 v14 c 15 v15 c 16 v16 c 17 v17 c 18 v18 c 19 v19 c 20 v20 c 21 v21 c 22 v22 c 23 v23 c 24 v24 c 25 v25 c 26 v26 c 27 v27 c 28 v28 c 29 v29 c 30 v30 c 31 v31 c 32 v32 c 33 v33 c 34 v34 c 35 v35 c 36 v36 c 37 v37 c 38 v38 p cnf 38 167 -7 4 0 -7 1 3 0 -8 5 0 -8 1 3 0 -9 4 0 -9 1 3 0 -11 4 0 -11 10 0 -11 1 3 0 -12 5 0 -12 10 0 -12 1 3 0 -13 5 0 -13 10 0 -13 1 3 0 -14 5 0 -14 10 0 -14 1 3 0 -15 4 0 -17 1 0 -17 4 5 0 -17 10 0 -18 3 0 -18 4 5 0 -18 10 0 -19 1 0 -19 4 5 0 -19 10 0 -20 3 0 -20 4 5 0 -20 10 0 -21 1 0 -21 4 5 0 -21 10 0 -22 3 0 -22 4 5 0 -22 10 0 -23 4 0 -25 1 0 -25 17 18 19 20 21 22 0 -26 3 0 -26 17 18 19 20 21 22 0 -27 17 18 19 20 21 22 0 -29 1 0 -29 4 5 0 -30 3 0 -30 4 5 0 -32 1 3 0 -32 4 5 0 -34 32 0 -34 17 18 19 20 21 22 0 -35 29 30 0 -35 32 0 -36 1 0 -36 32 0 -36 17 18 19 20 21 22 0 -37 3 0 -37 29 30 0 -37 32 0 -16 -4 0 -16 -10 1 -5 0 -16 -10 -3 -5 0 -16 -10 1 -6 0 -16 -10 -3 -6 0 -24 -4 0 -24 -10 1 -5 0 -24 -10 -3 -5 0 -24 -10 1 -6 0 -24 -10 -3 -6 0 -28 -17 0 -28 -18 0 -28 -19 0 -28 -20 0 -28 -21 0 -28 -22 0 -38 -17 -32 0 -38 -18 -32 0 -38 -19 -32 0 -38 -20 -32 0 -38 -21 -32 0 -38 -22 -32 0 -38 -29 -32 0 -38 -30 -32 0 1 2 3 0 -1 -2 0 -1 -3 0 -2 -3 0 4 5 6 0 -4 -5 0 -4 -6 0 -5 -6 0 7 8 9 10 0 -7 -8 0 -7 -9 0 -7 -10 0 -8 -9 0 -8 -10 0 -9 -10 0 11 12 13 14 15 16 0 -11 -12 0 -11 -13 0 -11 -14 0 -11 -15 0 -11 -16 0 -12 -13 0 -12 -14 0 -12 -15 0 -12 -16 0 -13 -14 0 -13 -15 0 -13 -16 0 -14 -15 0 -14 -16 0 -15 -16 0 17 18 19 20 21 22 23 24 0 -17 -18 0 -17 -19 0 -17 -20 0 -17 -21 0 -17 -22 0 -17 -23 0 -17 -24 0 -18 -19 0 -18 -20 0 -18 -21 0 -18 -22 0 -18 -23 0 -18 -24 0 -19 -20 0 -19 -21 0 -19 -22 0 -19 -23 0 -19 -24 0 -20 -21 0 -20 -22 0 -20 -23 0 -20 -24 0 -21 -22 0 -21 -23 0 -21 -24 0 -22 -23 0 -22 -24 0 -23 -24 0 25 26 27 28 0 -25 -26 0 -25 -27 0 -25 -28 0 -26 -27 0 -26 -28 0 -27 -28 0 29 30 31 0 -29 -30 0 -29 -31 0 -30 -31 0 32 33 0 -32 -33 0 34 35 36 37 38 0 -34 -35 0 -34 -36 0 -34 -37 0 -34 -38 0 -35 -36 0 -35 -37 0 -35 -38 0 -36 -37 0 -36 -38 0 -37 -38 0