From: acondolu Date: Sat, 15 Jul 2017 13:05:59 +0000 (+0200) Subject: Added problems encoded from 3-colorability of graphs X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b67b37f44b44a1bfe844e765d9ea45d16734c32b;p=fireball-separation.git Added problems encoded from 3-colorability of graphs --- diff --git a/ocaml/problems/3col b/ocaml/problems/3col new file mode 100644 index 0000000..df0045e --- /dev/null +++ b/ocaml/problems/3col @@ -0,0 +1,25 @@ + +$! 3col: 0<>1 +C x (_.x y BOMB BOMB y y y b) (_.x BOMB y BOMB y y y b) (_.x BOMB BOMB y y y y b) BOMB BOMB BOMB a +C x y y y (_.x BOMB y y y BOMB BOMB b) (_.x y BOMB y BOMB y BOMB b) (_.x y y BOMB BOMB BOMB y b) a +D x y y y y y y a +C x z z z BOMB BOMB BOMB BOMB +C x y y y z z z BOMB + +$? 3col: 0<>1 1<>1 +C x (_.x y BOMB BOMB y y y b) (_.x BOMB y BOMB y y y b) (_.x BOMB BOMB y y y y b) BOMB BOMB BOMB a +C x y y y (_.x BOMB y y BOMB BOMB BOMB b) (_.x y BOMB y BOMB BOMB BOMB b) (_.x y y BOMB BOMB BOMB BOMB b) a +D x y y y y y y a +C x z z z BOMB BOMB BOMB BOMB +C x y y y z z z BOMB + +$? 3col: 0<>1<>2 0<>3 1<>3 2<>3 +C x (_.x y BOMB BOMB y y y y y y y y y b) (_.x BOMB y BOMB y y y y y y y y y b) (_.x BOMB BOMB y y y y y y y y y y b) BOMB BOMB BOMB BOMB BOMB BOMB BOMB BOMB BOMB a +C x y y y (_.x BOMB y y y BOMB BOMB y y y y y y b) (_.x y BOMB y BOMB y BOMB y y y y y y b) (_.x y y BOMB BOMB BOMB y y y y y y y b) BOMB BOMB BOMB BOMB BOMB BOMB a +C x y y y y y y (_.x BOMB y y BOMB y y y BOMB BOMB y y y b) (_.x y BOMB y y BOMB y BOMB y BOMB y y y b) (_.x y y BOMB y y BOMB BOMB BOMB y y y y b) BOMB BOMB BOMB a +C x y y y y y y y y y (_.x BOMB y y BOMB y y BOMB y y y BOMB BOMB b) (_.x y BOMB y y BOMB y y BOMB y BOMB y BOMB b) (_.x y y BOMB y y BOMB y y BOMB BOMB BOMB y b) a +D x y y y y y y y y y y y y a +C x z z z BOMB BOMB BOMB BOMB BOMB BOMB BOMB BOMB BOMB BOMB +C x y y y z z z BOMB BOMB BOMB BOMB BOMB BOMB BOMB +C x y y y y y y z z z BOMB BOMB BOMB BOMB +C x y y y y y y y y y z z z BOMB