Timings for the revised encoding of the video shop example, after eliminating
the need for extended domains in function-types.  For this example, we see an
order of magnitude improvement over the previous times:

NAT : TYPE = [0..5];  %% legal range 0..4; 5 is bottom.

PERSON : TYPE = {black, brown, grey};  %% three people

TITLE : TYPE = {filmA, filmB, filmC, filmD};  %% four films (no bottom).

================

counter-theorem 1 : "nothing ever gets rented"

Refuted in 3 steps: addMember(black), AddTitle(filmA, 3), rentVideo(black, filmA)
Time ~0.48 secs

================

counter-theorem 2 : "there are never 3 members of the store"

Refuted in 3 steps: addMember(black), addMember(grey), addMember(brown)
Time ~0.47 secs

================

counter-theorem 3 : "3 copies are never rented at once"

Refuted in 8 steps: addMember(black), addMember(brown), addTitle(filmA, 3), 
	rentVideo(brown, filmA), rentVideo(black, filmA), addMember(grey),
	rentVideo(grey, filmA), copiesOut(filmA)
Time ~0.67 secs

================

counter-theorem 4 : "there are never 3 copies of any title"

Refuted in 1 step: addTitle(filmA, 3)
Time ~0.46 secs

================

normal theorem 5 : "there are never more rented videos than the stock level"

Refuted in 4 steps: addMember(black), addTitle(filmD, 4), rentVideo(black, filmD),
		addTitle(filmD, 0)
		%% Reveals a specification error - can reset the number of films 
		%% in stock after renting
Time ~0.59 secs

================

counter-theorem 6 : "it is never the case that every person rents a copy of every 
		video and the stock level of each video is at least 3"

Refuted in 19 steps: Basically, every member in {black, grey, brown} joins; 
		filmsA, B, C and D are respectively stocked 3, 3, 4, 4 times;
		and twelve rentVideo actions occur with unique person-film pairs.
Time ~3.40 secs

================

counter-theorem 7 : "it is never the case that every person rents a copy of every 
		video and the stock level of each video greater or equal to the 
		number of rented copies".

Refuted in 19 steps: Like the above.
Time ~3.58 secs