__def_1(a). __def_2(b). __all(pair(X1,X2)) :- __def_2(X2), __all(X1). __all(pair(X1,X2)) :- __def_1(X2), __def_1(X1). __all(pair(X1,X2)) :- __def_1(X2), __def_2(X1). __all(pair(X1,X2)) :- __all(X2), eq(X1). __all(pair(X1,X2)) :- __all(X2), __all(X1). __all(pair(X1,X2)) :- eq(X2), __def_2(X1). __all(pair(X1,X2)) :- __def_2(X2), eq(X1). __all(pair(X1,X2)) :- eq(X2), __def_1(X1). __all(pair(X1,X2)) :- __all(X2), __def_1(X1). __all(pair(X1,X2)) :- eq(X2), eq(X1). eq(pair(X1,X2)) :- __def_2(X2), __def_1(X1). __all(pair(X1,X2)) :- __def_1(X2), eq(X1). __all(pair(X1,X2)) :- __all(X2), __def_2(X1). __all(pair(X1,X2)) :- __def_1(X2), __all(X1). __all(pair(X1,X2)) :- __def_2(X2), __def_2(X1). __all(pair(X1,X2)) :- eq(X2), __all(X1). __not_eq(X) :- __def_2(X). __not_eq(X) :- __def_1(X). __not_eq(X) :- __all(X). distinct (X,Y) :- sig(Y), sig(X), __not_eq(pair(X,Y)). __all(pair(X1,X2)) :- eq(X2), __all(X1). __all(pair(X1,X2)) :- __all(X2), __def_1(X1). __all(pair(X1,X2)) :- __def_1(X2), __def_2(X1). __all(pair(X1,X2)) :- __def_2(X2), __all(X1). __all(pair(X1,X2)) :- __def_1(X2), eq(X1). __all(pair(X1,X2)) :- __all(X2), __all(X1). __all(pair(X1,X2)) :- __def_1(X2), __all(X1). __all(pair(X1,X2)) :- __def_2(X2), eq(X1). __all(pair(X1,X2)) :- __all(X2), eq(X1). __all(pair(X1,X2)) :- eq(X2), eq(X1). __def_1(a). __def_2(b). __all(pair(X1,X2)) :- __def_1(X2), __def_1(X1). __all(pair(X1,X2)) :- eq(X2), __def_2(X1). __all(pair(X1,X2)) :- __all(X2), __def_2(X1). eq(pair(X1,X2)) :- __def_2(X2), __def_1(X1). __all(pair(X1,X2)) :- __def_2(X2), __def_2(X1). __all(pair(X1,X2)) :- eq(X2), __def_1(X1). distinct (X1,X2) :- __not_eq(pair(X1,X2)), sig(X2), sig(X1). __not_eq(X1) :- __def_1(X1). __not_eq(X1) :- __def_2(X1). __not_eq(X1) :- __all(X1). __all(pair(X1,X2)) :- __def_2(X2), __all(X1). [rename-resolve: __all(pair(X1,X2)) :- __def_2(X2), __all(X1). {X1=X1,X2=X2} ] __all(pair(X1,X2)) :- __def_1(X2), __def_1(X1). [rename-resolve: __all(pair(X1,X2)) :- __def_1(X2), __def_1(X1). {X1=X1,X2=X2} ] __all(pair(X1,X2)) :- __def_1(X2), __def_2(X1). [rename-resolve: __all(pair(X1,X2)) :- __def_1(X2), __def_2(X1). {X1=X1,X2=X2} ] __all(pair(X1,X2)) :- __all(X2), eq(X1). [rename-resolve: __all(pair(X1,X2)) :- __all(X2), eq(X1). {X1=X1,X2=X2} ] __all(pair(X1,X2)) :- __all(X2), __all(X1). [rename-resolve: __all(pair(X1,X2)) :- __all(X2), __all(X1). {X1=X1,X2=X2} ] __all(pair(X1,X2)) :- eq(X2), __def_2(X1). [rename-resolve: __all(pair(X1,X2)) :- eq(X2), __def_2(X1). {X1=X1,X2=X2} ] __all(pair(X1,X2)) :- __def_2(X2), eq(X1). [rename-resolve: __all(pair(X1,X2)) :- __def_2(X2), eq(X1). {X1=X1,X2=X2} ] __all(pair(X1,X2)) :- eq(X2), __def_1(X1). [rename-resolve: __all(pair(X1,X2)) :- eq(X2), __def_1(X1). {X1=X1,X2=X2} ] __all(pair(X1,X2)) :- __all(X2), __def_1(X1). [rename-resolve: __all(pair(X1,X2)) :- __all(X2), __def_1(X1). {X1=X1,X2=X2} ] __all(pair(X1,X2)) :- eq(X2), eq(X1). [rename-resolve: __all(pair(X1,X2)) :- eq(X2), eq(X1). {X1=X1,X2=X2} ] eq(pair(X1,X2)) :- __def_2(X2), __def_1(X1). [rename-resolve: eq(pair(X1,X2)) :- __def_2(X2), __def_1(X1). {X1=X1,X2=X2} ] __all(pair(X1,X2)) :- __def_1(X2), eq(X1). [rename-resolve: __all(pair(X1,X2)) :- __def_1(X2), eq(X1). {X1=X1,X2=X2} ] __all(pair(X1,X2)) :- __all(X2), __def_2(X1). [rename-resolve: __all(pair(X1,X2)) :- __all(X2), __def_2(X1). {X1=X1,X2=X2} ] __all(pair(X1,X2)) :- __def_1(X2), __all(X1). [rename-resolve: __all(pair(X1,X2)) :- __def_1(X2), __all(X1). {X1=X1,X2=X2} ] __all(pair(X1,X2)) :- __def_2(X2), __def_2(X1). [rename-resolve: __all(pair(X1,X2)) :- __def_2(X2), __def_2(X1). {X1=X1,X2=X2} ] __all(pair(X1,X2)) :- eq(X2), __all(X1). [rename-resolve: __all(pair(X1,X2)) :- eq(X2), __all(X1). {X1=X1,X2=X2} ] __not_eq(X) :- __def_2(X). [rename-resolve: __not_eq(X1) :- __def_2(X1). {X1=X} ] __not_eq(X) :- __def_1(X). [rename-resolve: __not_eq(X1) :- __def_1(X1). {X1=X} ] __not_eq(X) :- __all(X). [rename-resolve: __not_eq(X1) :- __all(X1). {X1=X} ] distinct (X,Y) :- sig(Y), sig(X), __not_eq(pair(X,Y)). [rename-resolve: distinct (X1,X2) :- __not_eq(pair(X1,X2)), sig(X2), sig(X1). {X2=Y,X1=X} ] __not_eq(pair(X1,X2)) :- __def_2(X2), __def_2(X1). [eps-resolve: __not_eq(X1) :- __all(X1). {X1=pair(X1,X2)} __all(pair(X1,X2)) :- __def_2(X2), __def_2(X1). ] __not_eq(pair(X1,X2)) :- eq(X2), __def_1(X1). [eps-resolve: __not_eq(X1) :- __all(X1). {X1=pair(X1,X2)} __all(pair(X1,X2)) :- eq(X2), __def_1(X1). ] __not_eq(pair(X1,X2)) :- eq(X2), eq(X1). [eps-resolve: __not_eq(X1) :- __all(X1). {X1=pair(X1,X2)} __all(pair(X1,X2)) :- eq(X2), eq(X1). ] __not_eq(pair(X1,X2)) :- eq(X2), __def_2(X1). [eps-resolve: __not_eq(X1) :- __all(X1). {X1=pair(X1,X2)} __all(pair(X1,X2)) :- eq(X2), __def_2(X1). ] __not_eq(pair(X1,X2)) :- __def_1(X2), __def_1(X1). [eps-resolve: __not_eq(X1) :- __all(X1). {X1=pair(X1,X2)} __all(pair(X1,X2)) :- __def_1(X2), __def_1(X1). ] __not_eq(pair(X1,X2)) :- __all(X2), __def_2(X1). [eps-resolve: __not_eq(X1) :- __all(X1). {X1=pair(X1,X2)} __all(pair(X1,X2)) :- __all(X2), __def_2(X1). ] __not_eq(pair(X1,X2)) :- __all(X2), __def_1(X1). [eps-resolve: __not_eq(X1) :- __all(X1). {X1=pair(X1,X2)} __all(pair(X1,X2)) :- __all(X2), __def_1(X1). ] __not_eq(pair(X1,X2)) :- __all(X2), eq(X1). [eps-resolve: __not_eq(X1) :- __all(X1). {X1=pair(X1,X2)} __all(pair(X1,X2)) :- __all(X2), eq(X1). ] __not_eq(pair(X1,X2)) :- __def_2(X2), eq(X1). [eps-resolve: __not_eq(X1) :- __all(X1). {X1=pair(X1,X2)} __all(pair(X1,X2)) :- __def_2(X2), eq(X1). ] __not_eq(pair(X1,X2)) :- __def_1(X2), __all(X1). [eps-resolve: __not_eq(X1) :- __all(X1). {X1=pair(X1,X2)} __all(pair(X1,X2)) :- __def_1(X2), __all(X1). ] __not_eq(pair(X1,X2)) :- __def_1(X2), __def_2(X1). [eps-resolve: __not_eq(X1) :- __all(X1). {X1=pair(X1,X2)} __all(pair(X1,X2)) :- __def_1(X2), __def_2(X1). ] __not_eq(pair(X1,X2)) :- __def_1(X2), eq(X1). [eps-resolve: __not_eq(X1) :- __all(X1). {X1=pair(X1,X2)} __all(pair(X1,X2)) :- __def_1(X2), eq(X1). ] __not_eq(pair(X1,X2)) :- __all(X2), __all(X1). [eps-resolve: __not_eq(X1) :- __all(X1). {X1=pair(X1,X2)} __all(pair(X1,X2)) :- __all(X2), __all(X1). ] __not_eq(pair(X1,X2)) :- eq(X2), __all(X1). [eps-resolve: __not_eq(X1) :- __all(X1). {X1=pair(X1,X2)} __all(pair(X1,X2)) :- eq(X2), __all(X1). ] __not_eq(pair(X1,X2)) :- __def_2(X2), __all(X1). [eps-resolve: __not_eq(X1) :- __all(X1). {X1=pair(X1,X2)} __all(pair(X1,X2)) :- __def_2(X2), __all(X1). ] __not_eq(b). [eps-resolve: __not_eq(X1) :- __def_2(X1). {X1=b} __def_2(b). ] __not_eq(a). [eps-resolve: __not_eq(X1) :- __def_1(X1). {X1=a} __def_1(a). ]