Timings for the original version of the video shop, using the SAL encoding for
functions with both extended domain and extended codomain types.  These examples 
were run as per Michael Schleucher's request (for comparison) to have:

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

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

TITLE : TYPE = {filmA, filmB, filmC, filmD, TITLE__B};  %% four films and bottom.

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

counter-theorem 1 : "nothing ever gets rented"

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

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

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

Refuted in 3 steps: addMember(black), addMember(grey), addMember(brown)
Time ~4.37 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 ~5.10 secs

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

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

Refuted in 1 step: addTitle(filmA, 3)
Time ~4.40 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 ~9.03 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 ~6.52 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 ~10.83 secs