ifThenTheory1
A theory with two solutions for a/1 (a(1) and a(2), in this order) and a single fact each for b/1 (b(1)) and c/1 (c(2)), used together with ifThenTheory2 (which lists a/1's facts in the opposite order) to check that ->/2 and ;/2 commit to the first solution of their condition.