% Steamroller

precedence( [w,f,b,s,g,c,i,j,t,ff,0,answer] ).
first_predicate_precedence( [wolf,fox,bird,snail,grain,plant,caterpillar,eats,<,ani] ).

%predicates( [eats,<,ani,wolf,fox,bird,snail,grain,plant,caterpillar] ).


%  w,f,b,s,g,c == constants of type wolf, ..., caterpillar
%  moreover we have eats, < (smaller), ani

axiom(  [ [], [wolf(w)] ] ).			% there are some of each of them
axiom(  [ [], [fox(f)] ] ).			% (except plants)
axiom(  [ [], [bird(b)] ] ).
axiom(  [ [], [snail(s)] ] ).
axiom(  [ [], [grain(g)] ] ).
axiom(  [ [], [caterpillar(c)] ] ).

axiom(  [ [wolf(X)], [ani(X)] ]).	  	% all these ones are animals
axiom(  [ [fox(X)], [ani(X)] ]).
axiom(  [ [bird(X)], [ani(X)] ]).
axiom(  [ [snail(X)], [ani(X)] ]).
axiom(  [ [caterpillar(X)], [ani(X)] ]).
axiom(  [ [grain(X)], [plant(X)] ] ).		% grains are plants

axiom(  [ [caterpillar(X), bird(Y)], [<(X,Y)] ]). % caterp. are smaller than birds
axiom(  [ [snail(X), bird(Y)], [<(X,Y)] ]).	% snails are smaller than birds
axiom(  [ [bird(X), fox(Y)], [<(X,Y)] ]).	% birds  are smaller than foxes
axiom(  [ [fox(X), wolf(Y)], [<(X,Y)] ]).   	% foxes are smaller than wolves

axiom(  [ [wolf(X), fox(Y), eats(X,Y)], [] ]).	% wolves do not eat foxes
axiom(  [ [wolf(X), grain(Y), eats(X,Y)], [] ]). % wolves do not eat grains
axiom(  [ [bird(X), snail(Y), eats(X,Y)], [] ]). % birds  do not eat snails
axiom(  [ [bird(X), caterpillar(Y)], [eats(X,Y)] ] ). % birds do eat caterpillars

% every animal X	eats all plants Y
%	 or else	eats all smaller plant eating animals Z:
%
axiom(  [ [ani(X), ani(Z), <(Z,X), plant(Y), plant(W), eats(Z,W)],
	 [eats(X,Y), eats(X,Z)] ]).

axiom(  [ [caterpillar(X)], [plant(i(X))] ]).	% caterpillars eat some plants 
axiom(  [ [caterpillar(X)], [eats(X,i(X))] ]).	%      plants
axiom(  [ [snail(X)], [plant(j(X))] ]).		% snails eat some
axiom(  [ [snail(X)], [eats(X,j(X))] ]).	%      plants


% Theorem: 		There is some animal that eats a grain eating animal.
% negated theorem:	There is no   animal that eats a grain eating animal,
% i.e. there are no animals X and Y and a grain Z s.t. X eats Y and Y eats Z:

axiom( [ [ani(X), ani(Y), grain(Z), eats(Y,Z), eats(X,Y)], [answer(X)] ]).


%ani(X), eats(X,s) -> [].



/* adding that < is a partial order makes the proof 30% faster  */
% doesn't terminate with answer predicate
%<(X,Y),<(Y,Z) -> <(X,Z).
%<(X,X) -> [].