123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229 |
- c This Formular is generated by mcnf
- c
- c horn? no
- c forced? no
- c mixed sat? no
- c clause length = 3
- c
- p cnf 50 218
- -5 -1 3 0
- -9 -43 20 0
- -23 48 37 0
- -14 -40 -42 0
- -31 -44 26 0
- -29 -1 22 0
- 46 38 -5 0
- 18 -40 39 0
- 14 -41 44 0
- 44 15 16 0
- 40 41 -13 0
- -23 -17 -29 0
- 18 1 35 0
- 10 18 -1 0
- -26 -16 50 0
- -3 25 15 0
- -8 41 -35 0
- 2 -24 14 0
- 17 45 25 0
- -45 33 9 0
- 39 -42 -23 0
- -10 35 37 0
- -23 -21 32 0
- -10 45 5 0
- 44 -8 5 0
- -23 -32 -13 0
- -41 -45 -24 0
- 36 -11 -13 0
- -27 -7 -35 0
- 2 -34 -6 0
- -27 8 31 0
- 29 42 -9 0
- 44 4 8 0
- -47 10 -31 0
- -29 34 -19 0
- -12 -50 28 0
- -36 31 -38 0
- -40 -31 11 0
- 4 -7 35 0
- 37 -18 47 0
- 32 -11 -7 0
- 30 24 -16 0
- 8 -45 -20 0
- 26 -42 -2 0
- 23 -32 4 0
- -26 -19 13 0
- -17 -9 -24 0
- -22 33 25 0
- -37 -27 -4 0
- -25 -9 29 0
- -30 -2 35 0
- 43 -1 -22 0
- 46 -5 -30 0
- 32 -7 -36 0
- 44 -2 -12 0
- -1 30 -13 0
- 36 -15 -48 0
- 49 -1 24 0
- -50 -27 11 0
- -18 41 -6 0
- 8 12 -14 0
- -47 -41 -42 0
- 38 42 -39 0
- -15 -9 12 0
- -30 -12 49 0
- -19 49 -21 0
- 10 15 17 0
- -39 46 1 0
- 12 -22 18 0
- -32 26 23 0
- 39 29 -12 0
- 36 20 44 0
- 11 -9 47 0
- -21 48 25 0
- 50 -3 48 0
- -35 -22 -37 0
- 25 -17 18 0
- -29 -46 16 0
- -10 -29 43 0
- 47 -2 12 0
- -3 -5 6 0
- -23 3 19 0
- 10 -50 -1 0
- -43 -49 10 0
- 50 44 -10 0
- -30 15 -48 0
- -37 36 5 0
- 36 -7 -11 0
- -3 -45 1 0
- -37 -35 19 0
- 26 11 -10 0
- 47 -9 -30 0
- 12 -21 -43 0
- 14 33 32 0
- -23 7 6 0
- 3 -30 -12 0
- -5 -36 -43 0
- 21 -48 -13 0
- -34 -11 31 0
- 21 -38 9 0
- -15 21 23 0
- 31 -45 -50 0
- -35 -30 26 0
- -47 -33 -15 0
- -30 2 33 0
- 49 28 44 0
- -28 -35 -48 0
- -5 -33 9 0
- -34 26 41 0
- 43 33 -23 0
- -48 -20 15 0
- -44 -19 2 0
- -21 -1 34 0
- -38 15 -39 0
- 50 -5 -24 0
- 9 27 15 0
- -41 11 24 0
- -43 24 21 0
- -39 41 -17 0
- -18 33 -42 0
- 50 37 1 0
- 14 15 -29 0
- 49 -41 19 0
- -13 34 37 0
- -7 20 47 0
- -34 -10 -44 0
- 39 45 -13 0
- -16 49 21 0
- -5 36 -47 0
- 6 -31 -18 0
- 9 -13 37 0
- 1 36 14 0
- 44 19 -13 0
- 28 -8 -21 0
- -24 4 26 0
- 19 14 17 0
- -23 -18 50 0
- 50 -25 22 0
- 48 -16 -32 0
- -13 14 -34 0
- 42 -23 4 0
- 22 -50 38 0
- -24 -36 -42 0
- 19 -46 -1 0
- 26 49 16 0
- 5 25 -8 0
- 34 -2 -15 0
- 27 23 24 0
- -41 -16 -49 0
- -23 5 -33 0
- -42 -22 11 0
- -27 17 14 0
- -24 48 19 0
- -11 50 -40 0
- 17 10 -12 0
- 13 -50 -17 0
- -39 -18 4 0
- 14 -38 -21 0
- 18 38 30 0
- 1 -39 11 0
- 45 -4 -11 0
- -44 18 -4 0
- 48 -21 33 0
- -48 46 -9 0
- -28 4 19 0
- 49 9 -14 0
- -46 12 9 0
- -44 7 36 0
- 47 -22 10 0
- 37 26 -16 0
- -15 11 39 0
- -20 15 -19 0
- -44 -9 34 0
- 43 -32 -30 0
- -14 -23 3 0
- -9 43 -27 0
- 4 39 -11 0
- -50 -10 34 0
- 42 -32 -49 0
- -48 -8 1 0
- -35 -28 -42 0
- 36 37 49 0
- -8 14 7 0
- 32 34 23 0
- -50 15 1 0
- 25 -28 -8 0
- -42 12 45 0
- -7 -29 -26 0
- -29 -14 -22 0
- -31 -45 -44 0
- 47 10 -22 0
- -1 8 9 0
- -13 14 -3 0
- 38 40 -46 0
- -37 -2 21 0
- -24 -30 -16 0
- 43 -35 -40 0
- -26 -43 10 0
- 10 -18 -11 0
- -33 13 3 0
- 17 -44 24 0
- 5 -12 -45 0
- 31 34 1 0
- 18 31 32 0
- 6 18 45 0
- -17 -27 -3 0
- -47 -42 -41 0
- -28 -16 33 0
- -4 10 -36 0
- -32 -33 42 0
- -8 19 -3 0
- -44 -49 24 0
- -17 25 23 0
- -3 -14 -11 0
- -35 22 8 0
- -26 19 -20 0
- -11 26 -34 0
- 12 46 13 0
- %
- 0
|