Attached is a much larger example of a lookup table. This is the same size as one used for proprietary purposes, but with the proprietary information replaced with non-properietary numbers that have similar relationships. The purpose of the lookup table is to calculate an efficiency value that is between 0 and 1. The theory generates 3 TCCs, the last of which (LookupTable_2_D_TCC3) is the important one, namely that the result is indeed between 0 and 1. If I attempt the proof strategy (skeep)(skeep)(skeep)(grind), I get the following error:
Error: `(#<Judgement posrat_div_posrat_is_posrat>)' is not of the
expected type `array'
[condition type: type-error]
Note that I do not get this error if I just try (grind). This uses the patch previously sent to me by Sam Owre (patch-20141114.lisp), although I do not know if it is related to that patch, or whether the problem would exist without it. While it takes a long time to process with the patch, without it, the time required is so long that I have not attempted to ascertain whether it would actually complete.