[traths@jk-005 ft_prolog]$ 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]: :-[basic,flagops,unify,ip1,ip2,prop,ftprov,top].
basic.pl   compiled traceable 5716 bytes in 0.00 seconds
flagops.pl compiled traceable 3356 bytes in 0.00 seconds
unify.pl   compiled traceable 3448 bytes in 0.01 seconds
ip1.pl     compiled traceable 2276 bytes in 0.00 seconds
ip2.pl     compiled traceable 9280 bytes in 0.00 seconds
prop.pl    compiled traceable 6436 bytes in 0.00 seconds
ftprov.pl  compiled traceable 38116 bytes in 0.00 seconds
top.pl     compiled traceable 8376 bytes in 0.00 seconds

*** Warning: Singleton variables in clause 10 of sub/4: Term, Exp
... (lots of Warnings)


[eclipse 3]: f((a(x,p(x)) and e(y,q(y))) imp (e(z,(p(z) or neg q(z))))).
 1 
 0.0s
Yes (0.00s cpu, solution 1, maybe more) ?
[eclipse 4]: f(((e(x,p(x))) and (e(y,q(y)))) imp (a(z,(( neg p(z)) or q(z))))).
 1  
 2  
 3  
 4

^C
interruption: type a, b, c, e, or h for help : ? abort
Aborting execution ...
Abort
[eclipse 5]: pd(p or (neg q and r) imp ((p or neg q) and (p or r))). %pure propos. proving
0.0s
Yes (0.00s cpu)
[eclipse 6]: pd((p imp q) iff ((q or neg p) and (neg q or p))). %pure propos. proving

No (0.00s cpu)
[eclipse 7]: halt.
[traths@jk-005 ft_prolog]$