% Drinker Paradox, after translation FOL -> GL, is trivial
% d(X) for X is drunk, notd(X) for the complement

fof(d_cons,axiom, ! [A]:((d(A) & notd(A)) => ((goal)))).
fof(neg_phi,axiom, ! [A]:(((d(A) & neg_psi)))).
fof(neg_psi_ax,axiom, ((neg_psi) => (? [A] : (notd(A))))).
fof(goal_to_be_proved,conjecture,goal).