[traths@jk-005 LJT]$ eclipse
ECLiPSe Constraint Logic Programming System [kernel]
Copyright Imperial College London and ICL
Certain libraries copyright Parc Technologies Ltd
GMP library copyright Free Software Foundation
Version 5.7 #33, Sat Feb 14 00:16 2004
[eclipse 1]: nodbgcomp. % no debug instructions (slightly faster code)

Yes (0.00s cpu)
[eclipse 2]: [LJT].
LJT.pl     compiled traceable 17540 bytes in 0.00 seconds

Yes (0.00s cpu)

[eclipse 3]: prove((p v (~q & r) -> (p v ~q) & (p v r)) , Result).

Result = true
Yes (0.00s cpu)
[eclipse 4]: prove(((p -> q) <-> (q v ~ p) & ( ~ q v p)) , Result).

Result = false
Yes (0.00s cpu)
[eclipse 5]: halt.
[traths@jk-005 LJT]$