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