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