; First, define the necessary relations:

(define member class object1 rel object2)

;1. Tony, Mike, and John belong to the Alpine Club.
;   Although these are best represented in FOL as:
;
;   Belongs(alpineclub,tony),
;   Belongs(alpineclub,mike),
;   Belongs(alpineclub,john),
;
;   it's easier to represent them in SNePSUL just using member-class:

(describe (assert member (tony mike john) class alpineclub))

;2. Every member of the Alpine Club who is not a skier is a mountain climber.
;   In FOL (using LOTS of abbreviations):	Ax[Bax ^ ~Sx -> Mx]
;   But in SNePSUL:

(describe (assert forall $x
		  &ant (build member *x class alpineclub)
		  &ant (build min 0 max 0
			      arg (build member *x class skier))
		  cq (build member *x class mountain-climber)))	

;3. Mountain climbers do not like rain, and anyone who does not like
;   snow is not a skier.
;
;   We'll split this into its 2 conjuncts:
;
;   In FOL:	Ay[My -> ~Lry]
;   In SNePSUL:

(describe (assert forall $y
		  ant (build member *y class mountain-climber)
		  cq  (build min 0 max 0
			     arg (build object1 *y rel likes object2 rain))))

;   And the second conjunct:	
;   In FOL:	Az[~Lsz -> ~Sz]	
;   (note that we could have also used the contrapositive,
;    which would eliminate the negations)
;
;   In SNePSUL:

(describe (assert forall $z
		  ant (build min 0 max 0
			     arg (build object1 *z rel likes object2 snow))
		  cq  (build min 0 max 0
			     arg (build member *z class skier))))

;4. Mike dislikes whatever Tony likes, and likes whatever Tony dislikes. 
;   
;   Again, let's split this into 2 conjuncts:
;
;   In FOL:	Aw[Lwt -> -Lwm]
;   In SNePSUL:

(describe (assert forall $w
		  ant (build object1 tony rel likes object2 *w)
		  cq  (build min 0 max 0
			     arg (build object1 mike rel likes object2 *w))))

;   And the 2nd conjunct:
;
;   In FOL:	Av[~Lvt -> Lvm]
;   In SNePSUL:

(describe (assert forall $v
                  ant (build min 0 max 0
			     arg (build object1 tony rel likes object2 *v))
                  cq  (build object1 mike rel likes object2 *v)))

;* Is there a member of the Alpine Club who is a mountain climber but not
;  a skier?
;
;  In FOL:	Ex[Bax ^ Mx ^ ~Sx]

;  In SNePSUL, we could either ask for all 3 propositions:

(describe (deduce min 3 max 3
		  arg ( (build member $x class alpineclub)
			(build member *x class mountain-climber)
			(build min 0 max 0
			       arg (build member *x class skier)))))	

;  which, unfortunately, leaves Cassie speechless, which is the 
;  equivalent of her saying "I don't know".

;  We could also use the rarely used "deducewh" to find the individuals
;  (as opposed to the propositions about those individuals):

(describe (& (deducewh member $x class alpineclub)
	     (deducewh member *x class mountain-climber)
	     (deducewh min 0 max 0
		       arg (build member *x class skier))))

;  But that leaves her speechless, too.  The problem is that SNIP really
;  can't solve this kind of problem.

;  Exercise:  Use, in addition, the needed disjunction Lst v ~Lst,
;             and see what happens.