c Standarized MaxSat Instance
c{
c "sha1sum": "eeb92fe463d17ee335d449e6209f52dc6585ff07",
c "nvars": 81,
c "ncls": 162,
c "nhards": 81,
c "nhard_len_stats":
c { "min": 3, "max": 5, "ave": 4.56,
c "stddev": 0.59 },
c "nsofts": 81,
c "nsoft_len_stats":
c { "min": 1, "max": 1, "ave": 1.00,
c "stddev": 0.00 },
c "nsoft_wts": 1,
c "soft_wt_stats":
c { "min": 1, "max": 1, "ave": 1.00,
c "stddev": 0.00 }
c}
c------------------------------------------------------------
c SUBTRACT 0
p wcnf 81 162 82
1 -1 0
1 -2 0
1 -3 0
1 -4 0
1 -5 0
1 -6 0
1 -7 0
1 -8 0
1 -9 0
1 -10 0
1 -11 0
1 -12 0
1 -13 0
1 -14 0
1 -15 0
1 -16 0
1 -17 0
1 -18 0
1 -19 0
1 -20 0
1 -21 0
1 -22 0
1 -23 0
1 -24 0
1 -25 0
1 -26 0
1 -27 0
1 -28 0
1 -29 0
1 -30 0
1 -31 0
1 -32 0
1 -33 0
1 -34 0
1 -35 0
1 -36 0
1 -37 0
1 -38 0
1 -39 0
1 -40 0
1 -41 0
1 -42 0
1 -43 0
1 -44 0
1 -45 0
1 -46 0
1 -47 0
1 -48 0
1 -49 0
1 -50 0
1 -51 0
1 -52 0
1 -53 0
1 -54 0
1 -55 0
1 -56 0
1 -57 0
1 -58 0
1 -59 0
1 -60 0
1 -61 0
1 -62 0
1 -63 0
1 -64 0
1 -65 0
1 -66 0
1 -67 0
1 -68 0
1 -69 0
1 -70 0
1 -71 0
1 -72 0
1 -73 0
1 -74 0
1 -75 0
1 -76 0
1 -77 0
1 -78 0
1 -79 0
1 -80 0
1 -81 0
82 1 2 10 0
82 1 10 11 19 0
82 10 19 20 28 0
82 19 28 29 37 0
82 28 37 38 46 0
82 37 46 47 55 0
82 46 55 56 64 0
82 55 64 65 73 0
82 64 73 74 0
82 1 2 3 11 0
82 2 10 11 12 20 0
82 11 19 20 21 29 0
82 20 28 29 30 38 0
82 29 37 38 39 47 0
82 38 46 47 48 56 0
82 47 55 56 57 65 0
82 56 64 65 66 74 0
82 65 73 74 75 0
82 2 3 4 12 0
82 3 11 12 13 21 0
82 12 20 21 22 30 0
82 21 29 30 31 39 0
82 30 38 39 40 48 0
82 39 47 48 49 57 0
82 48 56 57 58 66 0
82 57 65 66 67 75 0
82 66 74 75 76 0
82 3 4 5 13 0
82 4 12 13 14 22 0
82 13 21 22 23 31 0
82 22 30 31 32 40 0
82 31 39 40 41 49 0
82 40 48 49 50 58 0
82 49 57 58 59 67 0
82 58 66 67 68 76 0
82 67 75 76 77 0
82 4 5 6 14 0
82 5 13 14 15 23 0
82 14 22 23 24 32 0
82 23 31 32 33 41 0
82 32 40 41 42 50 0
82 41 49 50 51 59 0
82 50 58 59 60 68 0
82 59 67 68 69 77 0
82 68 76 77 78 0
82 5 6 7 15 0
82 6 14 15 16 24 0
82 15 23 24 25 33 0
82 24 32 33 34 42 0
82 33 41 42 43 51 0
82 42 50 51 52 60 0
82 51 59 60 61 69 0
82 60 68 69 70 78 0
82 69 77 78 79 0
82 6 7 8 16 0
82 7 15 16 17 25 0
82 16 24 25 26 34 0
82 25 33 34 35 43 0
82 34 42 43 44 52 0
82 43 51 52 53 61 0
82 52 60 61 62 70 0
82 61 69 70 71 79 0
82 70 78 79 80 0
82 7 8 9 17 0
82 8 16 17 18 26 0
82 17 25 26 27 35 0
82 26 34 35 36 44 0
82 35 43 44 45 53 0
82 44 52 53 54 62 0
82 53 61 62 63 71 0
82 62 70 71 72 80 0
82 71 79 80 81 0
82 8 9 18 0
82 9 17 18 27 0
82 18 26 27 36 0
82 27 35 36 45 0
82 36 44 45 54 0
82 45 53 54 63 0
82 54 62 63 72 0
82 63 71 72 81 0
82 72 80 81 0