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