# A puzzle by Lewis Carroll :
# 
#  From the premises
# 
#  All who neither dance on tight ropes nor eat penny-buns are old.
#  Pigs, that are liable to giddiness, are treated with respect.
#  A wise balloonist takes an umbrella with him.
#  No one ought to lunch in public who looks ridiculous and eats penny-buns.
#  Young creatures, who go up in balloons, are liable to giddiness.
#  Fat creatures, who look ridiculous, may lunch in
#      public, provided that they do not dance on tight ropes.
#  No wise creatures dance on tight ropes, if liable to giddiness.
#  A pig looks ridiculous carrying an umbrella.
#  All who do not dance on tight ropes and who are treated
#      with respect are fat.
# 
# Show that "no wise young pigs go up in balloons."

#  First specify the desired variable ordering. DDcal can later reorder
var = dance*eats*old*pig*giddy*respect*wise*balloon*umbrella*ridic*\
      public*young*fat

#  All who neither dance on tight ropes nor eat penny-buns are old.
A1 = (dance' * eats') => old

#  Pigs, that are liable to giddiness, are treated with respect.
A2 = (pig * giddy) => respect

#  A wise balloonist takes an umbrella with him.
A3 = (wise * balloon) => umbrella

#  No one ought to lunch in public who looks ridiculous and eats penny-buns.
A4 = (ridic * eats) => public'

#  Young creatures, who go up in balloons, are liable to giddiness.
A5 = (young * balloon) => giddy

#  Fat creatures, who look ridiculous, may lunch in
#      public, provided that they do not dance on tight ropes.
A6 = (fat * ridic * dance') => public

#  No wise creatures dance on tight ropes, if liable to giddiness.
A7 = (wise * giddy) => dance'

#  A pig looks ridiculous carrying an umbrella.
A8 = (pig * umbrella) => ridic

#  All who do not dance on tight ropes and who are treated
#      with respect are fat.
A9 = (dance' * respect) => fat

# Show that "no wise young pigs go up in balloons."
proofGoal = wise * young * pig => balloon'

# Negate proof-goal and add it in
contra1 = A1 * A2 * A3 * A4 * A5 * A6 * A7 * A8 * A9 * \
           proofGoal'

# Unfortunately contra1 did not emerge to be false. Why? Forgot this!
frame = (young == old')

# Add this frame condition. Now we get "false". Thus proved by contradiction.

contra = contra1 * frame	   
[contra1 frame contra]