%[def] __def_4 pub(c).
%[def] __def_3 plus(a,b).
%[def] __def_1 crypt(plus(a,b),pub(c)).
%[def] __def_2 plus(crypt(a,pub(c)),crypt(b,pub(c))).
%[def] __def_6 b.
%[def] __def_9 crypt(b,pub(c)).
%[def] __def_7 c.
%[def] __def_8 crypt(a,pub(c)).
%[def] __def_5 a.
__def_4(pub(X)) :- __def_7(X).
eq(pair(X1,X2)) :- __def_2(X1), __def_1(X2).
eq(pair(X1,X2)) :- __def_2(X1), __def_2(X2).
eq(pair(X1,X2)) :- __def_6(X1), __def_6(X2).
eq(pair(X1,X2)) :- __def_1(X1), __def_2(X2).
eq(pair(X1,X2)) :- __def_5(X1), __def_5(X2).
eq(pair(X1,X2)) :- __def_7(X1), __def_7(X2).
eq(pair(X1,X2)) :- __def_1(X1), __def_1(X2).
__def_3(plus(X1,X2)) :- __def_5(X1), __def_6(X2).
__def_1(crypt(X1,X2)) :- __def_3(X1), __def_4(X2).
__def_2(plus(X1,X2)) :- __def_8(X1), __def_9(X2).
__def_6(b).
__def_9(crypt(X1,X2)) :- __def_6(X1), __def_4(X2).
__def_7(c).
__def_8(crypt(X1,X2)) :- __def_5(X1), __def_4(X2).
__def_5(a).
sig(zero).
sig(minus(X)) :- sig(X).
sig(crypt(X,Y)) :- sig(X), sig(Y).
sig(plus(X,Y)) :- sig(X), sig(Y).
sig(a).
sig(b).
sig(c).