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