input = """
c generated by sgen
c see http://www.cs.qub.ac.uk/~i.spence/sgen
p cnf 77 164
-2 -3 -4 0
-1 -3 -4 0
-1 -2 -4 0
-1 -2 -3 0
-6 -7 -8 0
-5 -7 -8 0
-5 -6 -8 0
-5 -6 -7 0
-10 -11 -12 0
-9 -11 -12 0
-9 -10 -12 0
-9 -10 -11 0
-14 -15 -16 0
-13 -15 -16 0
-13 -14 -16 0
-13 -14 -15 0
-18 -19 -20 0
-17 -19 -20 0
-17 -18 -20 0
-17 -18 -19 0
-22 -23 -24 0
-21 -23 -24 0
-21 -22 -24 0
-21 -22 -23 0
-26 -27 -28 0
-25 -27 -28 0
-25 -26 -28 0
-25 -26 -27 0
-30 -31 -32 0
-29 -31 -32 0
-29 -30 -32 0
-29 -30 -31 0
-34 -35 -36 0
-33 -35 -36 0
-33 -34 -36 0
-33 -34 -35 0
-38 -39 -40 0
-37 -39 -40 0
-37 -38 -40 0
-37 -38 -39 0
-42 -43 -44 0
-41 -43 -44 0
-41 -42 -44 0
-41 -42 -43 0
-46 -47 -48 0
-45 -47 -48 0
-45 -46 -48 0
-45 -46 -47 0
-50 -51 -52 0
-49 -51 -52 0
-49 -50 -52 0
-49 -50 -51 0
-54 -55 -56 0
-53 -55 -56 0
-53 -54 -56 0
-53 -54 -55 0
-58 -59 -60 0
-57 -59 -60 0
-57 -58 -60 0
-57 -58 -59 0
-62 -63 -64 0
-61 -63 -64 0
-61 -62 -64 0
-61 -62 -63 0
-66 -67 -68 0
-65 -67 -68 0
-65 -66 -68 0
-65 -66 -67 0
-70 -71 -72 0
-69 -71 -72 0
-69 -70 -72 0
-69 -70 -71 0
-73 -74 -75 0
-73 -74 -76 0
-73 -74 -77 0
-73 -75 -76 0
-73 -75 -77 0
-73 -76 -77 0
-74 -75 -76 0
-74 -75 -77 0
-74 -76 -77 0
-75 -76 -77 0
5 35 2 0
30 35 2 0
30 5 2 0
30 5 35 0
72 27 59 0
38 27 59 0
38 72 59 0
38 72 27 0
36 45 62 0
29 45 62 0
29 36 62 0
29 36 45 0
11 3 71 0
22 3 71 0
22 11 71 0
22 11 3 0
32 37 68 0
43 37 68 0
43 32 68 0
43 32 37 0
51 55 39 0
33 55 39 0
33 51 39 0
33 51 55 0
77 41 63 0
49 41 63 0
49 77 63 0
49 77 41 0
56 31 69 0
19 31 69 0
19 56 69 0
19 56 31 0
23 8 40 0
74 8 40 0
74 23 40 0
74 23 8 0
18 34 73 0
66 34 73 0
66 18 73 0
66 18 34 0
48 54 65 0
1 54 65 0
1 48 65 0
1 48 54 0
28 47 75 0
10 47 75 0
10 28 75 0
10 28 47 0
46 20 13 0
21 20 13 0
21 46 13 0
21 46 20 0
4 60 76 0
16 60 76 0
16 4 76 0
16 4 60 0
61 12 6 0
57 12 6 0
57 61 6 0
57 61 12 0
70 42 14 0
7 42 14 0
7 70 14 0
7 70 42 0
24 67 25 0
50 67 25 0
50 24 25 0
50 24 67 0
26 64 15 0
53 64 15 0
53 26 15 0
53 26 64 0
44 17 52 0
44 17 58 0
44 17 9 0
44 52 58 0
44 52 9 0
44 58 9 0
17 52 58 0
17 52 9 0
17 58 9 0
52 58 9 0
"""

output = "UNSAT"
