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