[traths@jk-005 ileansep]$ 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]: [ileansep_ec5]. iso.pl compiled traceable 11324 bytes in 0.01 seconds ileansep_ec5.pl compiled traceable 11252 bytes in 0.02 seconds Yes (0.02s cpu) [eclipse 3]: prove((all X : p(X) , ex Y : q(Y) => ex Z : ( p(Z) ; ~q(Z) ))). 1 2 0.0 X = _114 Y = _103 Z = _87 Yes (0.00s cpu, solution 1, maybe more) ? [eclipse 4]: prove(((ex X: p(X) , ex Y: q(Y)) => all Z: (~p(Z) ; q(Z)))). 1 No (0.00s cpu) [eclipse 5]: halt. [traths@jk-005 ileansep]$