helm/gTopLevel/esempi/decompose.cic

   1 !A:Prop.!B:Prop.!C:Prop.(and (or A C) (and (or A B) (or B C))) -> True
   2
   3 !A:Prop.!B:Prop.!C:Prop.(and (sumbool A C) (and (or A B) !D:Prop.(or B D))) -> True
   4
   5 !A:Prop.!B:Prop.!C:Prop.(and (and A C) (and (and A B) (and B C))) -> True