:- 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)))).