Prop8: shows that ac is not a decision procedure Prop9: shows w>x>y>z>w fails