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
- 27 -1 37 0
- -19 -12 -8 0
- -28 -3 -14 0
- 8 -49 -16 0
- 31 5 -24 0
- 29 18 44 0
- -33 36 -40 0
- -4 22 -1 0
- 8 -3 -50 0
- -43 37 -6 0
- -23 -20 42 0
- 21 -23 47 0
- -48 3 -37 0
- -32 10 -44 0
- 13 16 12 0
- 16 32 34 0
- 22 -40 -44 0
- 33 -47 -46 0
- 11 26 -8 0
- -30 -19 46 0
- -5 2 37 0
- 9 -31 -46 0
- -44 -31 -41 0
- 37 11 45 0
- -45 37 20 0
- -39 -25 12 0
- -35 15 14 0
- 30 -43 -49 0
- 6 3 45 0
- -25 -11 49 0
- -20 35 -46 0
- 49 -46 44 0
- 20 -12 -48 0
- -3 -36 42 0
- 9 11 20 0
- 27 25 50 0
- -1 5 -7 0
- -49 36 -50 0
- -36 7 16 0
- 36 11 12 0
- 21 45 -41 0
- -32 17 1 0
- -27 10 3 0
- 6 41 14 0
- -22 4 -28 0
- -49 -30 39 0
- -37 32 -21 0
- 5 46 -41 0
- -14 -27 36 0
- 44 18 8 0
- 15 -50 -46 0
- -8 25 -27 0
- 10 16 41 0
- -46 37 -38 0
- -35 -8 2 0
- 8 -44 -2 0
- -49 -5 -15 0
- -21 43 12 0
- 39 3 -10 0
- -5 25 -46 0
- 5 -47 -49 0
- -6 -48 -4 0
- 2 24 -23 0
- -36 5 41 0
- -40 28 -32 0
- -33 -29 31 0
- 20 42 22 0
- -3 -25 26 0
- 24 45 4 0
- -9 46 -42 0
- 26 -49 -7 0
- -27 -25 2 0
- -3 23 27 0
- -41 34 -11 0
- -4 11 -25 0
- -22 -29 -43 0
- 8 12 -1 0
- -11 -15 -21 0
- 5 -33 15 0
- 44 -31 -28 0
- 12 47 -11 0
- -30 -32 8 0
- -29 -1 34 0
- -31 42 -8 0
- -12 1 -14 0
- -21 -30 37 0
- -27 -14 -42 0
- -4 23 32 0
- 12 -3 11 0
- 3 -9 -18 0
- -6 20 -16 0
- -2 28 13 0
- 24 16 30 0
- -24 -14 4 0
- 1 36 10 0
- 3 -8 -28 0
- -17 -2 7 0
- 37 19 -34 0
- 18 -48 -50 0
- -22 -32 19 0
- 40 3 -29 0
- 47 37 30 0
- 21 3 44 0
- -40 36 -15 0
- -23 29 -27 0
- -11 1 -28 0
- -18 14 35 0
- 22 -36 4 0
- -33 30 8 0
- -43 44 -19 0
- -44 4 23 0
- -50 35 5 0
- -19 -37 -9 0
- 17 -6 38 0
- 7 -18 -46 0
- -20 -44 2 0
- 13 26 8 0
- -23 -42 44 0
- -13 42 -25 0
- -3 -12 17 0
- -46 -7 -11 0
- -21 -12 -13 0
- -35 -2 26 0
- 48 -45 -43 0
- -23 -48 -11 0
- 6 -41 4 0
- 3 -9 -14 0
- 49 -21 -43 0
- 25 47 21 0
- -16 -41 13 0
- -24 36 -48 0
- -29 4 -44 0
- -33 -16 -1 0
- 2 -16 47 0
- -37 49 -6 0
- 6 49 21 0
- -39 -4 -25 0
- 13 28 -8 0
- -14 -5 10 0
- 14 45 31 0
- 19 -18 36 0
- -10 -46 32 0
- 5 19 -32 0
- -32 27 -44 0
- -15 -17 34 0
- -11 47 21 0
- -4 29 -9 0
- -10 -26 -18 0
- 22 25 17 0
- -4 30 36 0
- 40 -36 -12 0
- -23 36 -8 0
- -30 31 -4 0
- 37 43 -21 0
- 22 -11 -16 0
- -22 -37 26 0
- 13 -19 42 0
- 49 -29 43 0
- 49 13 7 0
- 5 -37 25 0
- -11 -16 8 0
- -42 -10 23 0
- -46 -28 -1 0
- 2 -28 40 0
- -23 3 -41 0
- -18 33 -1 0
- 31 -10 -8 0
- -25 -39 -15 0
- -3 -29 22 0
- -47 9 -21 0
- 23 -24 -26 0
- -21 -29 -2 0
- -15 -7 33 0
- -24 -36 37 0
- -14 25 -32 0
- 28 35 10 0
- -46 28 38 0
- 41 -20 27 0
- 32 23 45 0
- 42 31 48 0
- 11 -44 45 0
- 29 -41 -30 0
- 37 29 5 0
- 22 33 -26 0
- -40 43 -24 0
- -48 -26 -33 0
- 44 -25 20 0
- 8 -28 -36 0
- -15 -12 20 0
- 34 19 -14 0
- -47 -3 -5 0
- -8 39 25 0
- 34 -19 -43 0
- -6 45 -25 0
- -19 -42 -9 0
- 24 -50 -42 0
- -11 -33 -16 0
- -22 -12 23 0
- 45 36 49 0
- 15 40 13 0
- 11 -40 10 0
- 44 -4 -38 0
- 39 12 -43 0
- 17 47 -20 0
- -37 31 -30 0
- 10 15 -36 0
- 24 10 32 0
- -42 8 -35 0
- -18 36 -33 0
- 27 -38 -29 0
- -3 47 48 0
- -17 40 -24 0
- 22 -43 50 0
- 42 -45 4 0
- 23 9 -41 0
- -34 17 -25 0
- 46 22 -31 0
- 11 -41 24 0
- %
- 0
|