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