Alloyでコンビネータ論理をやろうとしてうまく行かなかった話

Alloyになにか適当なパズルを解かせてみようと思って、最初に思いついたものが「SとKの組み合わせでIを作れ」だったので実装してみたが、Iを探す以前に、制約なしでもfactを満たす解が見つからない。何故だ？

abstract sig Bird{
	apply: Bird -> Bird
}

one sig K extends Bird{}

one sig S extends Bird{}

fact {
	all x, y: Bird | K.apply.x.apply.y = x
	all x, y, z: Bird {
		S.apply.x.apply.y.apply.z =
		x.apply.z.apply.(y.apply.z)
	}
}

run {} for 10 Bird

ありそうなのは「鳥の集合が有限だと解がない」かなと思うんだが。むむ。部分適用されたSコンビネータの今までの引数の状態を覚えておくのにそれぞれ鳥が必要になるから足りなくなるのか？