% problem-set/puzzles/carroll/lizard.ver1.clauses  
% created : 07/19/88
% revised : 07/19/88 

% description:
%
% This run solves "The Animals Puzzle" by using UR-resolution,
% hyper-resolution, and binary resolution.     
%
%                   		The Animals
%
%  (1)  All cunning savage animals are destructive.
%  (2)  No fat lazy animals climb trees.
%  (3)  All poisonous animals with claws wriggle.
%  (4)  No lizards are destructive unless they climb trees.
%  (5)  All animals, that have claws but no scales, are fat.
%  (6)  All grinning animals, that are dreaded, have claws.
%  (7)  No active destructive animal is fat.
%  (8)  All animals with scales, that are dreaded, are poisonous.
%  (9)  All grinning animals with claws are cunning.
%  (10) No savage lizard is viewed without dread.
%  (11) A savage lizard is an object of dread.
%       Deduce everything you can about these animals.
%                         -Lewis Carroll, Symbolic Logic, p.408

% representation:
%
                  

-CUNNING(x) | -SAVAGE(x) | DESTRUCTIVE(x).
-FAT(x) | -LAZY(x) | -CLIMB_TREES(x).
-POISONOUS(x) | -HAS_CLAWS(x) | WRIGGLES(x).
-CLIMB_TREES(x) | -LIZARD(x) | DESTRUCTIVE(x).
CLIMB_TREES(x) | -LIZARD(x) | -DESTRUCTIVE(x).
-HAS_CLAWS(x) | HAS_SCALES(x) | FAT(x).
-GRINNING(x) | -DREADED(x) | HAS_CLAWS(x).
-ACTIVE(x) | -DESTRUCTIVE(x) | -FAT(x). 
-HAS_SCALES(x) | -DREADED(x) | POISONOUS(x).
-GRINNING(x) | -HAS_CLAWS(x) | CUNNING(x).
-SAVAGE(x) | -LIZARD(x) | DREADED(x).