【演習問題９：含意論理``単一公理'' (TPTP/LCL038-1)】

true-->is_a_theorem(implies(implies(implies(A,B),C),
                            implies(implies(C,A),implies(D,A)))).

is_a_theorem(implies(A,B)),is_a_theorem(A)-->is_a_theorem(B).

is_a_theorem(implies(implies(a,b),
                     implies(implies(b,c),implies(a,c))))
    -->false.