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