__exactly_____def__7(c).
__exactly_____def__5(a).
__bot(plus(X1,X2)) :- __exactly_____def__4(X1), __exactly_____def__2(X2).
__bot(plus(X1,X2)) :- __exactly_eq(X1), __exactly_____def__8(X2).
__exactly_sig(plus(X1,X2)) :- __exactly_____def__5(X1), __exactly_____def__5(X2).
__bot(plus(X1,X2)) :- __exactly_sig(X1), __exactly_____def__2(X2).
__bot(plus(X1,X2)) :- __bot(X1), __exactly_____def__6(X2).
__bot(plus(X1,X2)) :- __exactly_eq(X1), __exactly_____def__1(X2).
__exactly_sig(plus(X1,X2)) :- __exactly_____def__6(X1), __exactly_____def__5(X2).
__bot(plus(X1,X2)) :- __exactly_____def__1(X1), __exactly_____def__7(X2).
__exactly_sig(plus(X1,X2)) :- __exactly_sig(X1), __exactly_sig(X2).
__bot(plus(X1,X2)) :- __exactly_____def__1(X1), __exactly_____def__3(X2).
__bot(plus(X1,X2)) :- __exactly_____def__1(X1), __exactly_sig(X2).
__exactly_____def__3(plus(X1,X2)) :- __exactly_____def__5(X1), __exactly_____def__6(X2).
__bot(plus(X1,X2)) :- __exactly_sig(X1), __bot(X2).
__bot(plus(X1,X2)) :- __bot(X1), __exactly_____def__4(X2).
__bot(plus(X1,X2)) :- __exactly_eq(X1), __exactly_eq(X2).
__bot(plus(X1,X2)) :- __bot(X1), __exactly_sig(X2).
__bot(plus(X1,X2)) :- __exactly_____def__7(X1), __exactly_____def__2(X2).
__bot(plus(X1,X2)) :- __exactly_____def__5(X1), __exactly_____def__9(X2).
__bot(plus(X1,X2)) :- __exactly_____def__1(X1), __exactly_____def__8(X2).
__bot(plus(X1,X2)) :- __exactly_____def__1(X1), __exactly_eq(X2).
__exactly_sig(plus(X1,X2)) :- __exactly_____def__5(X1), __exactly_sig(X2).
__bot(plus(X1,X2)) :- __bot(X1), __exactly_eq(X2).
__bot(plus(X1,X2)) :- __exactly_eq(X1), __exactly_____def__6(X2).
__bot(plus(X1,X2)) :- __exactly_sig(X1), __exactly_____def__9(X2).
__bot(plus(X1,X2)) :- __exactly_____def__4(X1), __exactly_____def__9(X2).
__exactly_sig(plus(X1,X2)) :- __exactly_____def__3(X1), __exactly_____def__5(X2).
__bot(plus(X1,X2)) :- __exactly_sig(X1), __exactly_____def__1(X2).
__bot(plus(X1,X2)) :- __exactly_____def__5(X1), __bot(X2).
__bot(plus(X1,X2)) :- __exactly_____def__7(X1), __exactly_____def__1(X2).
__exactly_sig(plus(X1,X2)) :- __exactly_sig(X1), __exactly_____def__5(X2).
__bot(plus(X1,X2)) :- __exactly_____def__4(X1), __bot(X2).
__bot(plus(X1,X2)) :- __exactly_eq(X1), __exactly_sig(X2).
__bot(plus(X1,X2)) :- __exactly_eq(X1), __exactly_____def__4(X2).
__bot(plus(X1,X2)) :- __bot(X1), __exactly_____def__8(X2).
__bot(plus(X1,X2)) :- __exactly_____def__4(X1), __exactly_____def__4(X2).
__bot(plus(X1,X2)) :- __exactly_sig(X1), __exactly_eq(X2).
__exactly_sig(plus(X1,X2)) :- __exactly_____def__5(X1), __exactly_____def__3(X2).
__bot(plus(X1,X2)) :- __exactly_____def__7(X1), __bot(X2).
__bot(plus(X1,X2)) :- __exactly_____def__5(X1), __exactly_eq(X2).
__bot(plus(X1,X2)) :- __exactly_____def__4(X1), __exactly_sig(X2).
__exactly_sig(plus(X1,X2)) :- __exactly_____def__6(X1), __exactly_____def__6(X2).
__bot(plus(X1,X2)) :- __exactly_____def__5(X1), __exactly_____def__2(X2).
__bot(plus(X1,X2)) :- __exactly_____def__1(X1), __exactly_____def__5(X2).
__bot(plus(X1,X2)) :- __exactly_____def__1(X1), __bot(X2).
__bot(plus(X1,X2)) :- __exactly_____def__7(X1), __exactly_____def__4(X2).
__bot(plus(X1,X2)) :- __exactly_sig(X1), __exactly_____def__8(X2).
__bot(plus(X1,X2)) :- __bot(X1), __bot(X2).
__bot(plus(X1,X2)) :- __exactly_eq(X1), __exactly_____def__2(X2).
__bot(plus(X1,X2)) :- __exactly_____def__1(X1), __exactly_____def__6(X2).
__bot(plus(X1,X2)) :- __exactly_____def__4(X1), __exactly_____def__7(X2).
__bot(plus(X1,X2)) :- __exactly_____def__1(X1), __exactly_____def__9(X2).
__bot(plus(X1,X2)) :- __bot(X1), __exactly_____def__7(X2).
__bot(plus(X1,X2)) :- __exactly_____def__7(X1), __exactly_eq(X2).
__bot(plus(X1,X2)) :- __exactly_sig(X1), __exactly_____def__4(X2).
__bot(plus(X1,X2)) :- __bot(X1), __exactly_____def__9(X2).
__bot(plus(X1,X2)) :- __bot(X1), __exactly_____def__2(X2).
__bot(plus(X1,X2)) :- __exactly_____def__1(X1), __exactly_____def__4(X2).
__bot(plus(X1,X2)) :- __exactly_____def__7(X1), __exactly_____def__8(X2).
__bot(plus(X1,X2)) :- __exactly_____def__5(X1), __exactly_____def__1(X2).
__bot(plus(X1,X2)) :- __exactly_eq(X1), __bot(X2).
__exactly_sig(plus(X1,X2)) :- __exactly_____def__3(X1), __exactly_____def__3(X2).
__bot(plus(X1,X2)) :- __exactly_____def__4(X1), __exactly_____def__1(X2).
__bot(plus(X1,X2)) :- __exactly_____def__5(X1), __exactly_____def__4(X2).
__bot(plus(X1,X2)) :- __exactly_____def__7(X1), __exactly_____def__9(X2).
__bot(plus(X1,X2)) :- __exactly_____def__4(X1), __exactly_____def__8(X2).
__bot(plus(X1,X2)) :- __exactly_eq(X1), __exactly_____def__3(X2).
__bot(plus(X1,X2)) :- __exactly_____def__4(X1), __exactly_____def__5(X2).
__bot(plus(X1,X2)) :- __exactly_____def__4(X1), __exactly_eq(X2).
__bot(plus(X1,X2)) :- __exactly_eq(X1), __exactly_____def__5(X2).
__exactly_sig(plus(X1,X2)) :- __exactly_____def__7(X1), __exactly_____def__7(X2).
__bot(plus(X1,X2)) :- __exactly_eq(X1), __exactly_____def__9(X2).
__bot(plus(X1,X2)) :- __exactly_____def__5(X1), __exactly_____def__8(X2).
__bot(plus(X1,X2)) :- __exactly_eq(X1), __exactly_____def__7(X2).
__bot(plus(X1,X2)) :- __exactly_____def__9(X1), __exactly_____def__8(X2).
__bot(plus(X1,X2)) :- __exactly_____def__9(X1), __exactly_____def__2(X2).
__bot(plus(X1,X2)) :- __exactly_____def__3(X1), __exactly_____def__2(X2).
__bot(plus(X1,X2)) :- __exactly_____def__8(X1), __exactly_____def__4(X2).
__exactly_sig(plus(X1,X2)) :- __exactly_sig(X1), __exactly_____def__3(X2).
__exactly_sig(plus(X1,X2)) :- __exactly_____def__3(X1), __exactly_____def__7(X2).
__bot(plus(X1,X2)) :- __exactly_____def__2(X1), __exactly_eq(X2).
__bot(plus(X1,X2)) :- __exactly_____def__8(X1), __exactly_____def__5(X2).
__bot(plus(X1,X2)) :- __exactly_____def__1(X1), __exactly_____def__1(X2).
__bot(plus(X1,X2)) :- __bot(X1), __exactly_____def__1(X2).
__bot(plus(X1,X2)) :- __exactly_____def__3(X1), __exactly_____def__1(X2).
__bot(plus(X1,X2)) :- __exactly_____def__2(X1), __exactly_____def__7(X2).
__exactly_sig(plus(X1,X2)) :- __exactly_____def__7(X1), __exactly_____def__3(X2).
__bot(plus(X1,X2)) :- __exactly_____def__8(X1), __exactly_sig(X2).
__exactly_sig(plus(X1,X2)) :- __exactly_____def__7(X1), __exactly_____def__5(X2).
__bot(plus(X1,X2)) :- __exactly_____def__8(X1), __exactly_____def__1(X2).
__exactly_sig(plus(X1,X2)) :- __exactly_____def__7(X1), __exactly_____def__6(X2).
__bot(plus(X1,X2)) :- __exactly_____def__8(X1), __exactly_____def__6(X2).
__bot(plus(X1,X2)) :- __exactly_____def__6(X1), __exactly_____def__4(X2).
__bot(plus(X1,X2)) :- __exactly_____def__2(X1), __exactly_sig(X2).
__bot(plus(X1,X2)) :- __exactly_____def__8(X1), __exactly_eq(X2).
__bot(plus(X1,X2)) :- __exactly_____def__8(X1), __exactly_____def__2(X2).
__bot(plus(X1,X2)) :- __exactly_____def__3(X1), __exactly_____def__4(X2).
__bot(plus(X1,X2)) :- __exactly_____def__3(X1), __exactly_____def__9(X2).
__exactly_sig(plus(X1,X2)) :- __exactly_sig(X1), __exactly_____def__7(X2).
__bot(plus(X1,X2)) :- __exactly_____def__9(X1), __exactly_____def__9(X2).
__exactly_sig(plus(X1,X2)) :- __exactly_____def__6(X1), __exactly_____def__7(X2).
__bot(plus(X1,X2)) :- __exactly_____def__2(X1), __exactly_____def__3(X2).
__bot(plus(X1,X2)) :- __exactly_____def__3(X1), __bot(X2).
__bot(plus(X1,X2)) :- __exactly_____def__9(X1), __exactly_____def__3(X2).
__bot(plus(X1,X2)) :- __exactly_____def__8(X1), __exactly_____def__7(X2).
__bot(plus(X1,X2)) :- __exactly_____def__9(X1), __bot(X2).
__bot(plus(X1,X2)) :- __exactly_____def__4(X1), __exactly_____def__6(X2).
__bot(plus(X1,X2)) :- __exactly_____def__2(X1), __exactly_____def__4(X2).
__bot(plus(X1,X2)) :- __exactly_____def__9(X1), __exactly_____def__5(X2).
__bot(plus(X1,X2)) :- __exactly_____def__9(X1), __exactly_____def__7(X2).
__bot(plus(X1,X2)) :- __exactly_____def__2(X1), __exactly_____def__1(X2).
__bot(plus(X1,X2)) :- __exactly_____def__6(X1), __exactly_____def__8(X2).
__bot(plus(X1,X2)) :- __exactly_____def__2(X1), __exactly_____def__5(X2).
__exactly_sig(plus(X1,X2)) :- __exactly_sig(X1), __exactly_____def__6(X2).
__bot(plus(X1,X2)) :- __exactly_____def__8(X1), __bot(X2).
__bot(plus(X1,X2)) :- __exactly_____def__9(X1), __exactly_sig(X2).
__bot(plus(X1,X2)) :- __exactly_____def__8(X1), __exactly_____def__8(X2).
__bot(plus(X1,X2)) :- __exactly_____def__6(X1), __bot(X2).
__exactly_____def__2(plus(X1,X2)) :- __exactly_____def__8(X1), __exactly_____def__9(X2).
__bot(plus(X1,X2)) :- __exactly_____def__9(X1), __exactly_____def__6(X2).
__bot(plus(X1,X2)) :- __exactly_____def__9(X1), __exactly_____def__1(X2).
__bot(plus(X1,X2)) :- __exactly_____def__4(X1), __exactly_____def__3(X2).
__exactly_sig(plus(X1,X2)) :- __exactly_____def__7(X1), __exactly_sig(X2).
__bot(plus(X1,X2)) :- __exactly_____def__6(X1), __exactly_____def__2(X2).
__bot(plus(X1,X2)) :- __exactly_____def__6(X1), __exactly_____def__1(X2).
__exactly_sig(plus(X1,X2)) :- __exactly_____def__6(X1), __exactly_sig(X2).
__bot(plus(X1,X2)) :- __exactly_____def__1(X1), __exactly_____def__2(X2).
__bot(plus(X1,X2)) :- __exactly_____def__6(X1), __exactly_eq(X2).
__bot(plus(X1,X2)) :- __exactly_____def__2(X1), __exactly_____def__9(X2).
__bot(plus(X1,X2)) :- __exactly_____def__8(X1), __exactly_____def__3(X2).
__bot(plus(X1,X2)) :- __exactly_____def__3(X1), __exactly_____def__8(X2).
__exactly_sig(plus(X1,X2)) :- __exactly_____def__6(X1), __exactly_____def__3(X2).
__bot(plus(X1,X2)) :- __bot(X1), __exactly_____def__3(X2).
__exactly_sig(plus(X1,X2)) :- __exactly_____def__3(X1), __exactly_sig(X2).
__bot(plus(X1,X2)) :- __exactly_____def__2(X1), __exactly_____def__2(X2).
__exactly_sig(plus(X1,X2)) :- __exactly_____def__3(X1), __exactly_____def__6(X2).
__bot(plus(X1,X2)) :- __exactly_____def__2(X1), __exactly_____def__8(X2).
__bot(plus(X1,X2)) :- __bot(X1), __exactly_____def__5(X2).
__exactly_sig(plus(X1,X2)) :- __exactly_____def__5(X1), __exactly_____def__7(X2).
__bot(plus(X1,X2)) :- __exactly_____def__9(X1), __exactly_____def__4(X2).
__bot(plus(X1,X2)) :- __exactly_____def__2(X1), __bot(X2).
__bot(plus(X1,X2)) :- __exactly_____def__3(X1), __exactly_eq(X2).
__bot(plus(X1,X2)) :- __exactly_____def__9(X1), __exactly_eq(X2).
__bot(plus(X1,X2)) :- __exactly_____def__6(X1), __exactly_____def__9(X2).
__bot(plus(X1,X2)) :- __exactly_____def__2(X1), __exactly_____def__6(X2).
__exactly_____def__6(b).
__bot(minus(X1)) :- __exactly_eq(X1).
__exactly_sig(minus(X1)) :- __exactly_sig(X1).
__bot(minus(X1)) :- __bot(X1).
__bot(minus(X1)) :- __exactly_____def__9(X1).
__bot(minus(X1)) :- __exactly_____def__2(X1).
__exactly_sig(minus(X1)) :- __exactly_____def__6(X1).
__bot(minus(X1)) :- __exactly_____def__8(X1).
__bot(minus(X1)) :- __exactly_____def__4(X1).
__exactly_sig(minus(X1)) :- __exactly_____def__7(X1).
__bot(minus(X1)) :- __exactly_____def__1(X1).
__exactly_sig(minus(X1)) :- __exactly_____def__5(X1).
__exactly_sig(minus(X1)) :- __exactly_____def__3(X1).
__bot(pub(X1)) :- __exactly_eq(X1).
__bot(pub(X1)) :- __exactly_sig(X1).
__bot(pub(X1)) :- __bot(X1).
__bot(pub(X1)) :- __exactly_____def__9(X1).
__bot(pub(X1)) :- __exactly_____def__2(X1).
__bot(pub(X1)) :- __exactly_____def__6(X1).
__bot(pub(X1)) :- __exactly_____def__8(X1).
__bot(pub(X1)) :- __exactly_____def__4(X1).
__exactly_____def__4(pub(X1)) :- __exactly_____def__7(X1).
__bot(pub(X1)) :- __exactly_____def__1(X1).
__bot(pub(X1)) :- __exactly_____def__5(X1).
__bot(pub(X1)) :- __exactly_____def__3(X1).
__exactly_sig(zero).
__bot(pair(X1,X2)) :- __exactly_____def__4(X1), __exactly_____def__2(X2).
__bot(pair(X1,X2)) :- __exactly_eq(X1), __exactly_____def__8(X2).
__exactly_eq(pair(X1,X2)) :- __exactly_____def__5(X1), __exactly_____def__5(X2).
__bot(pair(X1,X2)) :- __exactly_sig(X1), __exactly_____def__2(X2).
__bot(pair(X1,X2)) :- __bot(X1), __exactly_____def__6(X2).
__bot(pair(X1,X2)) :- __exactly_eq(X1), __exactly_____def__1(X2).
__bot(pair(X1,X2)) :- __exactly_____def__6(X1), __exactly_____def__5(X2).
__bot(pair(X1,X2)) :- __exactly_____def__1(X1), __exactly_____def__7(X2).
__bot(pair(X1,X2)) :- __exactly_sig(X1), __exactly_sig(X2).
__bot(pair(X1,X2)) :- __exactly_____def__1(X1), __exactly_____def__3(X2).
__bot(pair(X1,X2)) :- __exactly_____def__1(X1), __exactly_sig(X2).
__bot(pair(X1,X2)) :- __exactly_____def__5(X1), __exactly_____def__6(X2).
__bot(pair(X1,X2)) :- __exactly_sig(X1), __bot(X2).
__bot(pair(X1,X2)) :- __bot(X1), __exactly_____def__4(X2).
__bot(pair(X1,X2)) :- __exactly_eq(X1), __exactly_eq(X2).
__bot(pair(X1,X2)) :- __bot(X1), __exactly_sig(X2).
__bot(pair(X1,X2)) :- __exactly_____def__7(X1), __exactly_____def__2(X2).
__bot(pair(X1,X2)) :- __exactly_____def__5(X1), __exactly_____def__9(X2).
__bot(pair(X1,X2)) :- __exactly_____def__1(X1), __exactly_____def__8(X2).
__bot(pair(X1,X2)) :- __exactly_____def__1(X1), __exactly_eq(X2).
__bot(pair(X1,X2)) :- __exactly_____def__5(X1), __exactly_sig(X2).
__bot(pair(X1,X2)) :- __bot(X1), __exactly_eq(X2).
__bot(pair(X1,X2)) :- __exactly_eq(X1), __exactly_____def__6(X2).
__bot(pair(X1,X2)) :- __exactly_sig(X1), __exactly_____def__9(X2).
__bot(pair(X1,X2)) :- __exactly_____def__4(X1), __exactly_____def__9(X2).
__bot(pair(X1,X2)) :- __exactly_____def__3(X1), __exactly_____def__5(X2).
__bot(pair(X1,X2)) :- __exactly_sig(X1), __exactly_____def__1(X2).
__bot(pair(X1,X2)) :- __exactly_____def__5(X1), __bot(X2).
__bot(pair(X1,X2)) :- __exactly_____def__7(X1), __exactly_____def__1(X2).
__bot(pair(X1,X2)) :- __exactly_sig(X1), __exactly_____def__5(X2).
__bot(pair(X1,X2)) :- __exactly_____def__4(X1), __bot(X2).
__bot(pair(X1,X2)) :- __exactly_eq(X1), __exactly_sig(X2).
__bot(pair(X1,X2)) :- __exactly_eq(X1), __exactly_____def__4(X2).
__bot(pair(X1,X2)) :- __bot(X1), __exactly_____def__8(X2).
__bot(pair(X1,X2)) :- __exactly_____def__4(X1), __exactly_____def__4(X2).
__bot(pair(X1,X2)) :- __exactly_sig(X1), __exactly_eq(X2).
__bot(pair(X1,X2)) :- __exactly_____def__5(X1), __exactly_____def__3(X2).
__bot(pair(X1,X2)) :- __exactly_____def__7(X1), __bot(X2).
__bot(pair(X1,X2)) :- __exactly_____def__5(X1), __exactly_eq(X2).
__bot(pair(X1,X2)) :- __exactly_____def__4(X1), __exactly_sig(X2).
__exactly_eq(pair(X1,X2)) :- __exactly_____def__6(X1), __exactly_____def__6(X2).
__bot(pair(X1,X2)) :- __exactly_____def__5(X1), __exactly_____def__2(X2).
__bot(pair(X1,X2)) :- __exactly_____def__1(X1), __exactly_____def__5(X2).
__bot(pair(X1,X2)) :- __exactly_____def__1(X1), __bot(X2).
__bot(pair(X1,X2)) :- __exactly_____def__7(X1), __exactly_____def__4(X2).
__bot(pair(X1,X2)) :- __exactly_sig(X1), __exactly_____def__8(X2).
__bot(pair(X1,X2)) :- __bot(X1), __bot(X2).
__bot(pair(X1,X2)) :- __exactly_eq(X1), __exactly_____def__2(X2).
__bot(pair(X1,X2)) :- __exactly_____def__1(X1), __exactly_____def__6(X2).
__bot(pair(X1,X2)) :- __exactly_____def__4(X1), __exactly_____def__7(X2).
__bot(pair(X1,X2)) :- __exactly_____def__1(X1), __exactly_____def__9(X2).
__bot(pair(X1,X2)) :- __bot(X1), __exactly_____def__7(X2).
__bot(pair(X1,X2)) :- __exactly_____def__7(X1), __exactly_eq(X2).
__bot(pair(X1,X2)) :- __exactly_sig(X1), __exactly_____def__4(X2).
__bot(pair(X1,X2)) :- __bot(X1), __exactly_____def__9(X2).
__bot(pair(X1,X2)) :- __bot(X1), __exactly_____def__2(X2).
__bot(pair(X1,X2)) :- __exactly_____def__1(X1), __exactly_____def__4(X2).
__bot(pair(X1,X2)) :- __exactly_____def__7(X1), __exactly_____def__8(X2).
__bot(pair(X1,X2)) :- __exactly_____def__5(X1), __exactly_____def__1(X2).
__bot(pair(X1,X2)) :- __exactly_eq(X1), __bot(X2).
__bot(pair(X1,X2)) :- __exactly_____def__3(X1), __exactly_____def__3(X2).
__bot(pair(X1,X2)) :- __exactly_____def__4(X1), __exactly_____def__1(X2).
__bot(pair(X1,X2)) :- __exactly_____def__5(X1), __exactly_____def__4(X2).
__bot(pair(X1,X2)) :- __exactly_____def__7(X1), __exactly_____def__9(X2).
__bot(pair(X1,X2)) :- __exactly_____def__4(X1), __exactly_____def__8(X2).
__bot(pair(X1,X2)) :- __exactly_eq(X1), __exactly_____def__3(X2).
__bot(pair(X1,X2)) :- __exactly_____def__4(X1), __exactly_____def__5(X2).
__bot(pair(X1,X2)) :- __exactly_____def__4(X1), __exactly_eq(X2).
__bot(pair(X1,X2)) :- __exactly_eq(X1), __exactly_____def__5(X2).
__exactly_eq(pair(X1,X2)) :- __exactly_____def__7(X1), __exactly_____def__7(X2).
__bot(pair(X1,X2)) :- __exactly_eq(X1), __exactly_____def__9(X2).
__bot(pair(X1,X2)) :- __exactly_____def__5(X1), __exactly_____def__8(X2).
__bot(pair(X1,X2)) :- __exactly_eq(X1), __exactly_____def__7(X2).
__bot(pair(X1,X2)) :- __exactly_____def__9(X1), __exactly_____def__8(X2).
__bot(pair(X1,X2)) :- __exactly_____def__9(X1), __exactly_____def__2(X2).
__bot(pair(X1,X2)) :- __exactly_____def__3(X1), __exactly_____def__2(X2).
__bot(pair(X1,X2)) :- __exactly_____def__8(X1), __exactly_____def__4(X2).
__bot(pair(X1,X2)) :- __exactly_sig(X1), __exactly_____def__3(X2).
__bot(pair(X1,X2)) :- __exactly_____def__3(X1), __exactly_____def__7(X2).
__bot(pair(X1,X2)) :- __exactly_____def__2(X1), __exactly_eq(X2).
__bot(pair(X1,X2)) :- __exactly_____def__8(X1), __exactly_____def__5(X2).
__exactly_eq(pair(X1,X2)) :- __exactly_____def__1(X1), __exactly_____def__1(X2).
__bot(pair(X1,X2)) :- __bot(X1), __exactly_____def__1(X2).
__bot(pair(X1,X2)) :- __exactly_____def__3(X1), __exactly_____def__1(X2).
__bot(pair(X1,X2)) :- __exactly_____def__2(X1), __exactly_____def__7(X2).
__bot(pair(X1,X2)) :- __exactly_____def__7(X1), __exactly_____def__3(X2).
__bot(pair(X1,X2)) :- __exactly_____def__8(X1), __exactly_sig(X2).
__bot(pair(X1,X2)) :- __exactly_____def__7(X1), __exactly_____def__5(X2).
__bot(pair(X1,X2)) :- __exactly_____def__8(X1), __exactly_____def__1(X2).
__bot(pair(X1,X2)) :- __exactly_____def__7(X1), __exactly_____def__6(X2).
__bot(pair(X1,X2)) :- __exactly_____def__8(X1), __exactly_____def__6(X2).
__bot(pair(X1,X2)) :- __exactly_____def__6(X1), __exactly_____def__4(X2).
__bot(pair(X1,X2)) :- __exactly_____def__2(X1), __exactly_sig(X2).
__bot(pair(X1,X2)) :- __exactly_____def__8(X1), __exactly_eq(X2).
__bot(pair(X1,X2)) :- __exactly_____def__8(X1), __exactly_____def__2(X2).
__bot(pair(X1,X2)) :- __exactly_____def__3(X1), __exactly_____def__4(X2).
__bot(pair(X1,X2)) :- __exactly_____def__3(X1), __exactly_____def__9(X2).
__bot(pair(X1,X2)) :- __exactly_sig(X1), __exactly_____def__7(X2).
__bot(pair(X1,X2)) :- __exactly_____def__9(X1), __exactly_____def__9(X2).
__bot(pair(X1,X2)) :- __exactly_____def__6(X1), __exactly_____def__7(X2).
__bot(pair(X1,X2)) :- __exactly_____def__2(X1), __exactly_____def__3(X2).
__bot(pair(X1,X2)) :- __exactly_____def__3(X1), __bot(X2).
__bot(pair(X1,X2)) :- __exactly_____def__9(X1), __exactly_____def__3(X2).
__bot(pair(X1,X2)) :- __exactly_____def__8(X1), __exactly_____def__7(X2).
__bot(pair(X1,X2)) :- __exactly_____def__9(X1), __bot(X2).
__bot(pair(X1,X2)) :- __exactly_____def__4(X1), __exactly_____def__6(X2).
__bot(pair(X1,X2)) :- __exactly_____def__2(X1), __exactly_____def__4(X2).
__bot(pair(X1,X2)) :- __exactly_____def__9(X1), __exactly_____def__5(X2).
__bot(pair(X1,X2)) :- __exactly_____def__9(X1), __exactly_____def__7(X2).
__exactly_eq(pair(X1,X2)) :- __exactly_____def__2(X1), __exactly_____def__1(X2).
__bot(pair(X1,X2)) :- __exactly_____def__6(X1), __exactly_____def__8(X2).
__bot(pair(X1,X2)) :- __exactly_____def__2(X1), __exactly_____def__5(X2).
__bot(pair(X1,X2)) :- __exactly_sig(X1), __exactly_____def__6(X2).
__bot(pair(X1,X2)) :- __exactly_____def__8(X1), __bot(X2).
__bot(pair(X1,X2)) :- __exactly_____def__9(X1), __exactly_sig(X2).
__bot(pair(X1,X2)) :- __exactly_____def__8(X1), __exactly_____def__8(X2).
__bot(pair(X1,X2)) :- __exactly_____def__6(X1), __bot(X2).
__bot(pair(X1,X2)) :- __exactly_____def__8(X1), __exactly_____def__9(X2).
__bot(pair(X1,X2)) :- __exactly_____def__9(X1), __exactly_____def__6(X2).
__bot(pair(X1,X2)) :- __exactly_____def__9(X1), __exactly_____def__1(X2).
__bot(pair(X1,X2)) :- __exactly_____def__4(X1), __exactly_____def__3(X2).
__bot(pair(X1,X2)) :- __exactly_____def__7(X1), __exactly_sig(X2).
__bot(pair(X1,X2)) :- __exactly_____def__6(X1), __exactly_____def__2(X2).
__bot(pair(X1,X2)) :- __exactly_____def__6(X1), __exactly_____def__1(X2).
__bot(pair(X1,X2)) :- __exactly_____def__6(X1), __exactly_sig(X2).
__exactly_eq(pair(X1,X2)) :- __exactly_____def__1(X1), __exactly_____def__2(X2).
__bot(pair(X1,X2)) :- __exactly_____def__6(X1), __exactly_eq(X2).
__bot(pair(X1,X2)) :- __exactly_____def__2(X1), __exactly_____def__9(X2).
__bot(pair(X1,X2)) :- __exactly_____def__8(X1), __exactly_____def__3(X2).
__bot(pair(X1,X2)) :- __exactly_____def__3(X1), __exactly_____def__8(X2).
__bot(pair(X1,X2)) :- __exactly_____def__6(X1), __exactly_____def__3(X2).
__bot(pair(X1,X2)) :- __bot(X1), __exactly_____def__3(X2).
__bot(pair(X1,X2)) :- __exactly_____def__3(X1), __exactly_sig(X2).
__exactly_eq(pair(X1,X2)) :- __exactly_____def__2(X1), __exactly_____def__2(X2).
__bot(pair(X1,X2)) :- __exactly_____def__3(X1), __exactly_____def__6(X2).
__bot(pair(X1,X2)) :- __exactly_____def__2(X1), __exactly_____def__8(X2).
__bot(pair(X1,X2)) :- __bot(X1), __exactly_____def__5(X2).
__bot(pair(X1,X2)) :- __exactly_____def__5(X1), __exactly_____def__7(X2).
__bot(pair(X1,X2)) :- __exactly_____def__9(X1), __exactly_____def__4(X2).
__bot(pair(X1,X2)) :- __exactly_____def__2(X1), __bot(X2).
__bot(pair(X1,X2)) :- __exactly_____def__3(X1), __exactly_eq(X2).
__bot(pair(X1,X2)) :- __exactly_____def__9(X1), __exactly_eq(X2).
__bot(pair(X1,X2)) :- __exactly_____def__6(X1), __exactly_____def__9(X2).
__bot(pair(X1,X2)) :- __exactly_____def__2(X1), __exactly_____def__6(X2).
__bot(crypt(X1,X2)) :- __exactly_____def__4(X1), __exactly_____def__2(X2).
__bot(crypt(X1,X2)) :- __exactly_eq(X1), __exactly_____def__8(X2).
__exactly_sig(crypt(X1,X2)) :- __exactly_____def__5(X1), __exactly_____def__5(X2).
__bot(crypt(X1,X2)) :- __exactly_sig(X1), __exactly_____def__2(X2).
__bot(crypt(X1,X2)) :- __bot(X1), __exactly_____def__6(X2).
__bot(crypt(X1,X2)) :- __exactly_eq(X1), __exactly_____def__1(X2).
__exactly_sig(crypt(X1,X2)) :- __exactly_____def__6(X1), __exactly_____def__5(X2).
__bot(crypt(X1,X2)) :- __exactly_____def__1(X1), __exactly_____def__7(X2).
__exactly_sig(crypt(X1,X2)) :- __exactly_sig(X1), __exactly_sig(X2).
__bot(crypt(X1,X2)) :- __exactly_____def__1(X1), __exactly_____def__3(X2).
__bot(crypt(X1,X2)) :- __exactly_____def__1(X1), __exactly_sig(X2).
__exactly_sig(crypt(X1,X2)) :- __exactly_____def__5(X1), __exactly_____def__6(X2).
__bot(crypt(X1,X2)) :- __exactly_sig(X1), __bot(X2).
__bot(crypt(X1,X2)) :- __bot(X1), __exactly_____def__4(X2).
__bot(crypt(X1,X2)) :- __exactly_eq(X1), __exactly_eq(X2).
__bot(crypt(X1,X2)) :- __bot(X1), __exactly_sig(X2).
__bot(crypt(X1,X2)) :- __exactly_____def__7(X1), __exactly_____def__2(X2).
__bot(crypt(X1,X2)) :- __exactly_____def__5(X1), __exactly_____def__9(X2).
__bot(crypt(X1,X2)) :- __exactly_____def__1(X1), __exactly_____def__8(X2).
__bot(crypt(X1,X2)) :- __exactly_____def__1(X1), __exactly_eq(X2).
__exactly_sig(crypt(X1,X2)) :- __exactly_____def__5(X1), __exactly_sig(X2).
__bot(crypt(X1,X2)) :- __bot(X1), __exactly_eq(X2).
__bot(crypt(X1,X2)) :- __exactly_eq(X1), __exactly_____def__6(X2).
__bot(crypt(X1,X2)) :- __exactly_sig(X1), __exactly_____def__9(X2).
__bot(crypt(X1,X2)) :- __exactly_____def__4(X1), __exactly_____def__9(X2).
__exactly_sig(crypt(X1,X2)) :- __exactly_____def__3(X1), __exactly_____def__5(X2).
__bot(crypt(X1,X2)) :- __exactly_sig(X1), __exactly_____def__1(X2).
__bot(crypt(X1,X2)) :- __exactly_____def__5(X1), __bot(X2).
__bot(crypt(X1,X2)) :- __exactly_____def__7(X1), __exactly_____def__1(X2).
__exactly_sig(crypt(X1,X2)) :- __exactly_sig(X1), __exactly_____def__5(X2).
__bot(crypt(X1,X2)) :- __exactly_____def__4(X1), __bot(X2).
__bot(crypt(X1,X2)) :- __exactly_eq(X1), __exactly_sig(X2).
__bot(crypt(X1,X2)) :- __exactly_eq(X1), __exactly_____def__4(X2).
__bot(crypt(X1,X2)) :- __bot(X1), __exactly_____def__8(X2).
__bot(crypt(X1,X2)) :- __exactly_____def__4(X1), __exactly_____def__4(X2).
__bot(crypt(X1,X2)) :- __exactly_sig(X1), __exactly_eq(X2).
__exactly_sig(crypt(X1,X2)) :- __exactly_____def__5(X1), __exactly_____def__3(X2).
__bot(crypt(X1,X2)) :- __exactly_____def__7(X1), __bot(X2).
__bot(crypt(X1,X2)) :- __exactly_____def__5(X1), __exactly_eq(X2).
__bot(crypt(X1,X2)) :- __exactly_____def__4(X1), __exactly_sig(X2).
__exactly_sig(crypt(X1,X2)) :- __exactly_____def__6(X1), __exactly_____def__6(X2).
__bot(crypt(X1,X2)) :- __exactly_____def__5(X1), __exactly_____def__2(X2).
__bot(crypt(X1,X2)) :- __exactly_____def__1(X1), __exactly_____def__5(X2).
__bot(crypt(X1,X2)) :- __exactly_____def__1(X1), __bot(X2).
__bot(crypt(X1,X2)) :- __exactly_____def__7(X1), __exactly_____def__4(X2).
__bot(crypt(X1,X2)) :- __exactly_sig(X1), __exactly_____def__8(X2).
__bot(crypt(X1,X2)) :- __bot(X1), __bot(X2).
__bot(crypt(X1,X2)) :- __exactly_eq(X1), __exactly_____def__2(X2).
__bot(crypt(X1,X2)) :- __exactly_____def__1(X1), __exactly_____def__6(X2).
__bot(crypt(X1,X2)) :- __exactly_____def__4(X1), __exactly_____def__7(X2).
__bot(crypt(X1,X2)) :- __exactly_____def__1(X1), __exactly_____def__9(X2).
__bot(crypt(X1,X2)) :- __bot(X1), __exactly_____def__7(X2).
__bot(crypt(X1,X2)) :- __exactly_____def__7(X1), __exactly_eq(X2).
__bot(crypt(X1,X2)) :- __exactly_sig(X1), __exactly_____def__4(X2).
__bot(crypt(X1,X2)) :- __bot(X1), __exactly_____def__9(X2).
__bot(crypt(X1,X2)) :- __bot(X1), __exactly_____def__2(X2).
__bot(crypt(X1,X2)) :- __exactly_____def__1(X1), __exactly_____def__4(X2).
__bot(crypt(X1,X2)) :- __exactly_____def__7(X1), __exactly_____def__8(X2).
__bot(crypt(X1,X2)) :- __exactly_____def__5(X1), __exactly_____def__1(X2).
__bot(crypt(X1,X2)) :- __exactly_eq(X1), __bot(X2).
__exactly_sig(crypt(X1,X2)) :- __exactly_____def__3(X1), __exactly_____def__3(X2).
__bot(crypt(X1,X2)) :- __exactly_____def__4(X1), __exactly_____def__1(X2).
__exactly_____def__8(crypt(X1,X2)) :- __exactly_____def__5(X1), __exactly_____def__4(X2).
__bot(crypt(X1,X2)) :- __exactly_____def__7(X1), __exactly_____def__9(X2).
__bot(crypt(X1,X2)) :- __exactly_____def__4(X1), __exactly_____def__8(X2).
__bot(crypt(X1,X2)) :- __exactly_eq(X1), __exactly_____def__3(X2).
__bot(crypt(X1,X2)) :- __exactly_____def__4(X1), __exactly_____def__5(X2).
__bot(crypt(X1,X2)) :- __exactly_____def__4(X1), __exactly_eq(X2).
__bot(crypt(X1,X2)) :- __exactly_eq(X1), __exactly_____def__5(X2).
__exactly_sig(crypt(X1,X2)) :- __exactly_____def__7(X1), __exactly_____def__7(X2).
__bot(crypt(X1,X2)) :- __exactly_eq(X1), __exactly_____def__9(X2).
__bot(crypt(X1,X2)) :- __exactly_____def__5(X1), __exactly_____def__8(X2).
__bot(crypt(X1,X2)) :- __exactly_eq(X1), __exactly_____def__7(X2).
__bot(crypt(X1,X2)) :- __exactly_____def__9(X1), __exactly_____def__8(X2).
__bot(crypt(X1,X2)) :- __exactly_____def__9(X1), __exactly_____def__2(X2).
__bot(crypt(X1,X2)) :- __exactly_____def__3(X1), __exactly_____def__2(X2).
__bot(crypt(X1,X2)) :- __exactly_____def__8(X1), __exactly_____def__4(X2).
__exactly_sig(crypt(X1,X2)) :- __exactly_sig(X1), __exactly_____def__3(X2).
__exactly_sig(crypt(X1,X2)) :- __exactly_____def__3(X1), __exactly_____def__7(X2).
__bot(crypt(X1,X2)) :- __exactly_____def__2(X1), __exactly_eq(X2).
__bot(crypt(X1,X2)) :- __exactly_____def__8(X1), __exactly_____def__5(X2).
__bot(crypt(X1,X2)) :- __exactly_____def__1(X1), __exactly_____def__1(X2).
__bot(crypt(X1,X2)) :- __bot(X1), __exactly_____def__1(X2).
__bot(crypt(X1,X2)) :- __exactly_____def__3(X1), __exactly_____def__1(X2).
__bot(crypt(X1,X2)) :- __exactly_____def__2(X1), __exactly_____def__7(X2).
__exactly_sig(crypt(X1,X2)) :- __exactly_____def__7(X1), __exactly_____def__3(X2).
__bot(crypt(X1,X2)) :- __exactly_____def__8(X1), __exactly_sig(X2).
__exactly_sig(crypt(X1,X2)) :- __exactly_____def__7(X1), __exactly_____def__5(X2).
__bot(crypt(X1,X2)) :- __exactly_____def__8(X1), __exactly_____def__1(X2).
__exactly_sig(crypt(X1,X2)) :- __exactly_____def__7(X1), __exactly_____def__6(X2).
__bot(crypt(X1,X2)) :- __exactly_____def__8(X1), __exactly_____def__6(X2).
__exactly_____def__9(crypt(X1,X2)) :- __exactly_____def__6(X1), __exactly_____def__4(X2).
__bot(crypt(X1,X2)) :- __exactly_____def__2(X1), __exactly_sig(X2).
__bot(crypt(X1,X2)) :- __exactly_____def__8(X1), __exactly_eq(X2).
__bot(crypt(X1,X2)) :- __exactly_____def__8(X1), __exactly_____def__2(X2).
__exactly_____def__1(crypt(X1,X2)) :- __exactly_____def__3(X1), __exactly_____def__4(X2).
__bot(crypt(X1,X2)) :- __exactly_____def__3(X1), __exactly_____def__9(X2).
__exactly_sig(crypt(X1,X2)) :- __exactly_sig(X1), __exactly_____def__7(X2).
__bot(crypt(X1,X2)) :- __exactly_____def__9(X1), __exactly_____def__9(X2).
__exactly_sig(crypt(X1,X2)) :- __exactly_____def__6(X1), __exactly_____def__7(X2).
__bot(crypt(X1,X2)) :- __exactly_____def__2(X1), __exactly_____def__3(X2).
__bot(crypt(X1,X2)) :- __exactly_____def__3(X1), __bot(X2).
__bot(crypt(X1,X2)) :- __exactly_____def__9(X1), __exactly_____def__3(X2).
__bot(crypt(X1,X2)) :- __exactly_____def__8(X1), __exactly_____def__7(X2).
__bot(crypt(X1,X2)) :- __exactly_____def__9(X1), __bot(X2).
__bot(crypt(X1,X2)) :- __exactly_____def__4(X1), __exactly_____def__6(X2).
__bot(crypt(X1,X2)) :- __exactly_____def__2(X1), __exactly_____def__4(X2).
__bot(crypt(X1,X2)) :- __exactly_____def__9(X1), __exactly_____def__5(X2).
__bot(crypt(X1,X2)) :- __exactly_____def__9(X1), __exactly_____def__7(X2).
__bot(crypt(X1,X2)) :- __exactly_____def__2(X1), __exactly_____def__1(X2).
__bot(crypt(X1,X2)) :- __exactly_____def__6(X1), __exactly_____def__8(X2).
__bot(crypt(X1,X2)) :- __exactly_____def__2(X1), __exactly_____def__5(X2).
__exactly_sig(crypt(X1,X2)) :- __exactly_sig(X1), __exactly_____def__6(X2).
__bot(crypt(X1,X2)) :- __exactly_____def__8(X1), __bot(X2).
__bot(crypt(X1,X2)) :- __exactly_____def__9(X1), __exactly_sig(X2).
__bot(crypt(X1,X2)) :- __exactly_____def__8(X1), __exactly_____def__8(X2).
__bot(crypt(X1,X2)) :- __exactly_____def__6(X1), __bot(X2).
__bot(crypt(X1,X2)) :- __exactly_____def__8(X1), __exactly_____def__9(X2).
__bot(crypt(X1,X2)) :- __exactly_____def__9(X1), __exactly_____def__6(X2).
__bot(crypt(X1,X2)) :- __exactly_____def__9(X1), __exactly_____def__1(X2).
__bot(crypt(X1,X2)) :- __exactly_____def__4(X1), __exactly_____def__3(X2).
__exactly_sig(crypt(X1,X2)) :- __exactly_____def__7(X1), __exactly_sig(X2).
__bot(crypt(X1,X2)) :- __exactly_____def__6(X1), __exactly_____def__2(X2).
__bot(crypt(X1,X2)) :- __exactly_____def__6(X1), __exactly_____def__1(X2).
__exactly_sig(crypt(X1,X2)) :- __exactly_____def__6(X1), __exactly_sig(X2).
__bot(crypt(X1,X2)) :- __exactly_____def__1(X1), __exactly_____def__2(X2).
__bot(crypt(X1,X2)) :- __exactly_____def__6(X1), __exactly_eq(X2).
__bot(crypt(X1,X2)) :- __exactly_____def__2(X1), __exactly_____def__9(X2).
__bot(crypt(X1,X2)) :- __exactly_____def__8(X1), __exactly_____def__3(X2).
__bot(crypt(X1,X2)) :- __exactly_____def__3(X1), __exactly_____def__8(X2).
__exactly_sig(crypt(X1,X2)) :- __exactly_____def__6(X1), __exactly_____def__3(X2).
__bot(crypt(X1,X2)) :- __bot(X1), __exactly_____def__3(X2).
__exactly_sig(crypt(X1,X2)) :- __exactly_____def__3(X1), __exactly_sig(X2).
__bot(crypt(X1,X2)) :- __exactly_____def__2(X1), __exactly_____def__2(X2).
__exactly_sig(crypt(X1,X2)) :- __exactly_____def__3(X1), __exactly_____def__6(X2).
__bot(crypt(X1,X2)) :- __exactly_____def__2(X1), __exactly_____def__8(X2).
__bot(crypt(X1,X2)) :- __bot(X1), __exactly_____def__5(X2).
__exactly_sig(crypt(X1,X2)) :- __exactly_____def__5(X1), __exactly_____def__7(X2).
__bot(crypt(X1,X2)) :- __exactly_____def__9(X1), __exactly_____def__4(X2).
__bot(crypt(X1,X2)) :- __exactly_____def__2(X1), __bot(X2).
__bot(crypt(X1,X2)) :- __exactly_____def__3(X1), __exactly_eq(X2).
__bot(crypt(X1,X2)) :- __exactly_____def__9(X1), __exactly_eq(X2).
__bot(crypt(X1,X2)) :- __exactly_____def__6(X1), __exactly_____def__9(X2).
__bot(crypt(X1,X2)) :- __exactly_____def__2(X1), __exactly_____def__6(X2).
% Definitions.
sig(X) :- __exactly_sig(X).
sig(X) :- __exactly_____def__3(X).
sig(X) :- __exactly_____def__6(X).
sig(X) :- __exactly_____def__7(X).
sig(X) :- __exactly_____def__5(X).
%[def] __def_5(a).
__def_5(X) :- __exactly_____def__5(X).
%[def] __def_9(crypt(b,pub(c))).
__def_9(X) :- __exactly_____def__9(X).
%[def] __def_7(c).
__def_7(X) :- __exactly_____def__7(X).
%[def] __def_4(pub(c)).
__def_4(X) :- __exactly_____def__4(X).
%[def] __def_6(b).
__def_6(X) :- __exactly_____def__6(X).
eq(X) :- __exactly_eq(X).
%[def] __def_8(crypt(a,pub(c))).
__def_8(X) :- __exactly_____def__8(X).
%[def] __def_2(plus(crypt(a,pub(c)),crypt(b,pub(c)))).
__def_2(X) :- __exactly_____def__2(X).
%[def] __def_1(crypt(plus(a,b),pub(c))).
__def_1(X) :- __exactly_____def__1(X).
%[def] __def_3(plus(a,b)).
__def_3(X) :- __exactly_____def__3(X).
% Negated predicates.
__not_eq(X) :- __exactly_sig(X).
__not_eq(X) :- __exactly_____def__3(X).
__not_eq(X) :- __exactly_____def__2(X).
__not_eq(X) :- __exactly_____def__9(X).
__not_eq(X) :- __exactly_____def__6(X).
__not_eq(X) :- __exactly_____def__8(X).
__not_eq(X) :- __exactly_____def__7(X).
__not_eq(X) :- __exactly_____def__5(X).
__not_eq(X) :- __exactly_____def__4(X).
__not_eq(X) :- __exactly_____def__1(X).
__not_eq(X) :- __bot(X).
distinct(X,Y) :- __not_eq(pair(X,Y)), sig(X), sig(Y).