Merge of the V7_3_new_exportation branch.

[helm.git] / helm / gTopLevel / esempi / decompose.cic

diff --git a/helm/gTopLevel/esempi/decompose.cic b/helm/gTopLevel/esempi/decompose.cic
new file mode 100644 (file)
index 0000000..1a06fcb
--- /dev/null
+++ b/helm/gTopLevel/esempi/decompose.cic
@@ -0,0 +1,8 @@
+!A:Prop.!B:Prop.!C:Prop.(and (sumbool A False) (and (or True B) (or B False))) -> True
+
+!A:Prop.!B:Prop.!C:Prop.(and (sumbool A C) (and (or A B) !D:Prop.(or B D))) -> True
+
+!A:Prop.!B:Prop.!C:Prop.(and (and A C) (and (and A B) (and B C))) -> True
+
+(and True True) -> True
+(and True False) -> True