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