formulas(goals).

% all a all x all b (  A(a,x,b) ->  B(a,x,b)).
% all a all x all b (  B(a,x,b) ->  C(a,x,b)).
% all a all x all b (  C(a,x,b) ->  D(a,x,b)).
  all a all x all b (  B(a,x,b) -> CS(a,x,b)).
% all a all x all b ( CS(a,x,b) ->  D(a,x,b)).

end_of_list.