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