:- op(10, fx, v). to_hs(f) :- write('R_False'). to_hs(t) :- write('R_True'). to_hs(v(N)) :- write('(Var '), write(N), write(')'). to_hs(n(X)) :- write('(Not '), to_hs(X), write(')'). to_hs(a(X,Y)) :- to_hs('And', X, Y). to_hs(o(X,Y)) :- to_hs('Or', X, Y). to_hs(i(X,Y)) :- to_hs('Imp', X, Y). to_hs(e(X,Y)) :- to_hs('Eqv', X, Y). to_hs(F, X, Y) :- put(40 /* ( */), write(F), put(32 /* */), to_hs(X), put(32 /* */), to_hs(Y), put(41 /* ) */). tc_to_hs :- tc(N, X), write('tc '), write(N), write(' = '), to_hs(X), nl, nl, fail ; true. tc(1, v 1). tc(2, o(v 1,v 1)). tc(3, e(i(v 1,v 2),o(n(v 1),v 2))). tc(5, a(a(a(e(v 13,o(a(f,v 1),o(a(f,v 5),a(v 1,v 5)))),e(v 9,e(e(f,n(v 1)), n(v 5)))),a(a(e(v 14,o(a(v 13,v 2),o(a(v 13,v 6),a(v 2,v 6)))),e(v 10, e(e(v 13,n(v 2)),n(v 6)))),a(a(e(v 15,o(a(v 14,v 3),o(a(v 14,v 7),a(v 3, v 7)))),e(v 11,e(e(v 14,n(v 3)),n(v 7)))),a(e(v 16,o(a(v 15,v 4), o(a(v 15,v 8),a(v 4,v 8)))),e(v 12,e(e(v 15,n(v 4)),n(v 8))))))), a(a(a(e(v 17,o(a(n(f),a(v 1,v 5)),a(f,o(v 1,v 5)))),e(v 9,o(a(f,a(v 1, v 5)),o(a(f,a(n(v 1),n(v 5))),o(a(n(f),a(v 1,n(v 5))),a(n(f),a(n(v 1), v 5))))))),a(a(e(v 18,o(a(n(v 17),a(v 2,v 6)),a(v 17,o(v 2,v 6)))), e(v 10,o(a(v 17,a(v 2,v 6)),o(a(v 17,a(n(v 2),n(v 6))),o(a(n(v 17),a(v 2, n(v 6))),a(n(v 17),a(n(v 2),v 6))))))),a(a(e(v 19,o(a(n(v 18),a(v 3, v 7)),a(v 18,o(v 3,v 7)))),e(v 11,o(a(v 18,a(v 3,v 7)),o(a(v 18,a(n(v 3), n(v 7))),o(a(n(v 18),a(v 3,n(v 7))),a(n(v 18),a(n(v 3),v 7))))))), a(e(v 20,o(a(n(v 19),a(v 4,v 8)),a(v 19,o(v 4,v 8)))),e(v 12,o(a(v 19, a(v 4,v 8)),o(a(v 19,a(n(v 4),n(v 8))),o(a(n(v 19),a(v 4,n(v 8))), a(n(v 19),a(n(v 4),v 8)))))))))),e(v 16,v 20)))). tc(6, a(a(a(e(v 13,o(a(f,t),o(a(f,v 5),a(t,v 5)))), e(v 9,e(e(f,n(t)),n(v 5)))),a(a(e(v 14,o(a(v 13,f),o(a(v 13,v 6),a(f, v 6)))),e(v 10,e(e(v 13,n(f)),n(v 6)))),a(a(e(v 15,o(a(v 14,f), o(a(v 14,v 7),a(f,v 7)))),e(v 11,e(e(v 14,n(f)),n(v 7)))),a(e(v 16, o(a(v 15,t),o(a(v 15,v 8),a(t,v 8)))),e(v 12,e(e(v 15,n(t)), n(v 8))))))),a(a(a(e(v 17,o(a(n(f),a(t,v 5)),a(f,o(t,v 5)))),e(v 9, o(a(f,a(t,v 5)),o(a(f,a(n(t),n(v 5))),o(a(n(f),a(t,n(v 5))), a(n(f),a(n(t),v 5))))))),a(a(e(v 18,o(a(n(v 17),a(f,v 6)),a(v 17,o(f, v 6)))),e(v 10,o(a(v 17,a(f,v 6)),o(a(v 17,a(n(f),n(v 6))),o(a(n(v 17), a(f,n(v 6))),a(n(v 17),a(n(f),v 6))))))),a(a(e(v 19,o(a(n(v 18),a(f, v 7)),a(v 18,o(f,v 7)))),e(v 11,o(a(v 18,a(f,v 7)),o(a(v 18,a(n(f), n(v 7))),o(a(n(v 18),a(f,n(v 7))),a(n(v 18),a(n(f),v 7))))))),a(e(v 20, o(a(n(v 19),a(t,v 8)),a(v 19,o(t,v 8)))),e(v 12,o(a(v 19,a(t,v 8)), o(a(v 19,a(n(t),n(v 8))),o(a(n(v 19),a(t,n(v 8))),a(n(v 19),a(n(t), v 8)))))))))),e(v 16,v 20)))).