【演習問題８：``ヘンキンの問題'' (TPTP/HEN001-5)】

dom(A),dom(B)-->equal(divide(divide(A,B),A),zero).
dom(A),dom(B),dom(C)
    -->equal(divide(divide(divide(A,B),divide(C,B)),
                    divide(divide(A,C),B)),
             zero).

dom(A)-->equal(divide(zero,A),zero).
equal(divide(A,B),zero),equal(divide(B,A),zero)-->equal(A,B).
dom(A)-->equal(divide(A,identity),zero).

equal(divide(a,identity),zero)-->false.

dom(A)-->equal(A,A).
equal(A,B)-->equal(B,A).
equal(A,B),equal(B,C)-->equal(A,C).

equal(A,B),dom(C)-->equal(divide(A,C),divide(B,C)).
equal(A,B),dom(C)-->equal(divide(C,A),divide(C,B)).

true-->dom(zero),dom(identity),dom(a).
dom(A),dom(B)-->dom(divide(A,B)).