[traths@jk-005 ft]$ ft ft An intuitionistic theorem prover Version 1.23 Swedish Institute of Computer Science 1989 >set forever 1. % contraction deepening >Ax p(x) & Ey q(y) -> Ez (p(z) | ~q(z)). 1 1 1 yes 0 >Ex p(x) & Ey q(Y) -> Az (~p(z) | q(z)). 1 2 3 4 5 6 6 8 9 ^C Aborted time used 10 >(p -> q) <-> (q | ~p) & (~q | p). no 0 >quit. [traths@jk-005 ft]$