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