% COMMAND-LINE: --finite-model-find -i
% EXPECT: invalid
% EXPECT: valid
prin:TYPE;
form:TYPE;

signed:(prin,form)->BOOLEAN;
says:(prin,form)->BOOLEAN;

speaksfor:(prin,prin)->form;
signedE:BOOLEAN = FORALL(x:prin,y:form) : signed(x,y) => says(x,y);
saysE:BOOLEAN = FORALL(x,y:prin,z:form) : says(x,speaksfor(y,x)) AND says(y,z) => says(x,z); 

ASSERT(signedE);
ASSERT(saysE);

julie:prin;
dave:prin;
alice:prin;
openfile:form;

x2:BOOLEAN = signed(alice,openfile);
ASSERT(x2);
x3:BOOLEAN = signed(dave,speaksfor(alice,dave));
ASSERT(x3);

QUERY NOT says(dave,openfile); % this is invalid
QUERY says(dave,openfile); % this is valid