From: acondolu <andrea.condoluci@unibo.it>
Date: Wed, 12 Jul 2017 21:23:43 +0000 (+0200)
Subject: Added more problems with bombs, all working
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a784a4ebf67ebf00c94c6353a53a679fdf1bf163;p=fireball-separation.git

Added more problems with bombs, all working
---

diff --git a/ocaml/problems.ml b/ocaml/problems.ml
index b604231..3c098b9 100644
--- a/ocaml/problems.ml
+++ b/ocaml/problems.ml
@@ -338,10 +338,17 @@ let n3 () = magic_conv
 
 let o1 () = magic_conv None [] ["x a b"; "x (_. BOT) c"] ["*"];;
 let o2 () = magic_conv None [] ["x (y (_. BOT) a) c"; "x (y a PAC) d"] ["*"];;
+let o3 () = magic_conv
+ (Some"y (x a1 BOMB c) (x BOMB b1 d)")
+ [ "y (x a2 BOMB c) (x BOMB b1 d)";
+ "y (x a1 BOMB c) (x BOMB b2 d)";] [] ["*"];;
+let o4 () = magic_conv (Some"x BOMB a1 c")
+ [ "x y BOMB d"; "x BOMB a2 c" ] [] ["*"];;
 
-main [o1() ; o2() ];;
 
-(* main ([
+main [o1() ; o2(); o3(); o4();];;
+
+main ([
  p2 ; p4 ; p5 ; p6 ; p7 ; p8 ; p9 ; p10 ; p11 ; p12 ; p13 ;
  p14 ; p15 ; p16 ; p17 ; p18 ; p19 ; p20 ; p21 ; p22 ; p23 ;
  p24 ; p25 ; p26 ; p27 ; p28 ; p29 ; p30 ; p31 ; p32 ; p33 ;
@@ -363,4 +370,4 @@ main [o1() ; o2() ];;
  n1 ;
  n2 ;
  n3
-]));; *)
+]));;