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