またimpliesに引っかかった

RubyKaigiに行くので今から(am 6:00)寝るわけにも行かず取りあえず水島さんところで見つけた次の問題をやってみた。
http://d.hatena.ne.jp/kmizushima/20090629/1246212207

sig Person { pet : one Pet , tabacco : one Tabacco }
sig Pet { }
sig Tabacco { }

one sig Japanese extends Person { }
one sig American extends Person { }

fact { Japanese + American = Person }

// 異なる2人は異なるペットとタバコ
fact { all p1 : Person | all p2 : Person | p1 != p2 => p1.pet != p2.pet and p1.tabacco != p2.tabacco }

one sig Dog extends Pet { }
one sig Bird extends Pet { }

fact { Dog + Bird = Pet }

one sig SevenStar extends Tabacco { }
one sig MildSeven extends Tabacco { }

fact { SevenStar + MildSeven = Tabacco }

fact { one p : Person | p.tabacco = SevenStar => p.pet = Bird } // (6) セブンスターを吸う家主は鳥を飼っています。
// fact { one p : Person | p.tabacco = SevenStar and p.pet = Bird }

pred show() { }

run show for 1

最初これにしてno instanceになるのでなんだコレは！！みたいな感じだったんですけれども、ハイ。悲しいなー。
(4パターン書き出してfactを見て行くと分かります。)

一応意図としては、「ある人がセブンスターを吸う"ならば"その人は鳥を飼っている。そしてそういう人は１人しか居ない。」という事を意図して書いたのですが、まぁハイ。

これとかでアウトですね。(oneじゃないので)

なんか絶対こういうところハマるよなぁとか。