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