The following problem was posed on an American radio program called Car Talk. Given a stone that weighs 40 pound and a balance scale, cut the stone into 4 pieces so that one can weigh any stone with an integral weight between 1 and 40 pounds.
Since there are only 2^4 - 1 = 16 non-empty subsets of the 4 pieces, we quickly deduce that we need to be able to put pieces on both sides of the balance to do this. Putting a piece weighing w pounds on the same side of the balance as the stone we are weighing is equivalent to placing a stone weighing -w pounds on the opposite side, we quickly see that the problem is to find natural numbers w1, ... , w4 such that for every weight w in 1..40, there exist numbers x1, ... , x4 in {-1,0,1} such that w = x1w1 + ... + x4w4.
It's easy to have TLC find the solution by having it evaluate an assumption that's a formula that quantifies the subformula
IF \A w \in 1..40 : w = x1w1 + ... + x4w4
THEN PrintT(<
over x1, ... , x4 and w1, ..., w4. As a more interesting problem, we here do it replacing 40 and 4 by constants W and N.