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