package euler;

import euler.output.ILogger;
import euler.output.Outputter;
import euler.output.StdOutputter;
import java.io.ByteArrayOutputStream;
import java.io.File;
import java.io.FileOutputStream;
import java.io.InputStream;
import java.io.OutputStreamWriter;
import java.io.PrintStream;
import java.io.PrintWriter;
import java.util.Enumeration;
import java.util.Date;
import java.util.Hashtable;
import java.util.Vector;

public class EulerRunner {
	/**
	 * Main method invoked via <code>java euler.EulerRunner</code>
	 * 
	 * @param args
	 *            command line arguments
	 */
	public static void main(String[] args) {
		if (args.length == 0 || args[0].endsWith("-help")) {
			System.err.println("Version: " + Configuration.getInstance().getVersion() + "\n" +
					"Usage: euler <options> [--rules|--trules] uris --query|--tquery uri\n" + "options:\n" +
					"--prolog          translate to prolog\n" +
					"--prolog-bchain   translate to prolog backchain-only\n" +
					"--sem             translate to SEM\n" +
					"--sql             translate to SQL\n" +
					"--pass            pass-thru the N3\n" +
					"--json            translate to JSON\n" +
					"--prover9         translate to prover9\n" +
					"--nope            no proof explanation\n" +
					"--nobe            no belief explanation\n" +
					"--nefq            no ex falso quodlibet\n" +
					"--quiet           shorter explanation\n" +
					"--quick           optimized runtime\n" +
					"--think           give all solutions\n" +
					"--step count      maximum number of reasoning steps\n" +
					"--debug           output debug info via stderr\n" +
					"--trace           output trace info via stderr\n" +
					"--test            output test run\n" +
					"--test-as         output test run as service\n" +
					"--profile         enable profiling\n" +
					"--help            show help");
		} else {
			try {
				PrintStream out = System.out;
				out.println(doProof(args));
				if (out != System.out)
					out.close();
			} catch (Throwable t) {
				t.printStackTrace();
			}
		}
	}

	public static synchronized String doProof(String[] args) {
		try {
			Euler.runner++;
			Euler.z = null;
			Euler e = new Euler();
			Parser np = new Parser();
			int n = args.length - 1;
			String c = e.toURI(np.parse('<' + args[n] + '>'));
			for (int j = 0; j < n; j++) {
				if (args[j].endsWith("-think"))
					Configuration.getInstance().setThink(true);
				else if (args[j].endsWith("-nope"))
					Configuration.getInstance().setProofExplanation(false);
				else if (args[j].endsWith("-step"))
					Configuration.getInstance().setSteps(Long.parseLong(args[++j]));
				else if (args[j].endsWith("-local"))
					Configuration.getInstance().setRunLocal(true);
				else if (args[j].endsWith("-debug"))
					StdOutputter.getInstance().setLogLevel(ILogger.FINE);
				else if (args[j].endsWith("-trace"))
					StdOutputter.getInstance().setLogLevel(ILogger.FINER);
				else if (!args[j].startsWith("-"))
					e.load(e.toURI(np.parse('<' + args[j] + '>')));
				else if (args[j].endsWith("-graph")) {
					Euler el = new Euler();
					el.load(e.toURI(np.parse('<' + args[++j] + '>')));
					StringBuffer sb = new StringBuffer("data:,");
					for (Enumeration en = el.ext.ns.keys(); en.hasMoreElements();) {
						Object nsx = en.nextElement();
						sb.append("@prefix ").append(nsx).append(' ').append(el.ext.ns.get(nsx)).append(".\n");
					}
					String s = el.ext.baseURI;
					while (el.near != null) {
						sb.append('{').append(el.near).append("} q:source <").append(s).append(">.\n");
						el = el.near;
					}
					e.load(sb.toString());
				} else if (args[j].endsWith("-filter") || args[j].endsWith("-query")) {
					Euler el = new Euler();
					el.uid = -1;
					el.load(e.toURI(np.parse('<' + args[++j] + '>')));
					StringBuffer sb = new StringBuffer("data:,");
					for (Enumeration en = el.ext.ns.keys(); en.hasMoreElements();) {
						Object nsx = en.nextElement();
						sb.append("@prefix ").append(nsx).append(' ').append(el.ext.ns.get(nsx)).append(".\n");
					}
					while (el.near != null) {
						if (el.near.verb == Euler.LOGimplies) {
							for (Euler er = el.near.obj; er != null; er = er.near) {
								sb.append('{');
								for (Euler ee = el.near.subj; ee != null; ee = ee.near) {
									e.rewrite(false, ee, np);
									bnp(ee);
									sb.append(ee);
								}
								sb.append(sfg(el.near.subj, er));
								sb.append("} => {_:").append(el.near.uid).append(' ').append(Euler.Qselect).append(" {");
								e.rewrite(false, er, np);
								bnc(er);
								sb.append(er).append("}}. ");
							}
							el = el.near;
						} else if (el.near.verb == Euler.Qselect && el.near.near.verb == Euler.Qwhere) {
							for (Euler er = el.near.obj; er != null; er = er.near) {
								sb.append('{');
								for (Euler ee = el.near.near.obj; ee != null; ee = ee.near) {
									e.rewrite(false, ee, np);
									bnp(ee);
									sb.append(ee);
								}
								sb.append(sfg(el.near.near.obj, er));
								sb.append("} => {").append(el.near.subj).append(' ').append(Euler.Qselect).append(" {");
								e.rewrite(false, er, np);
								bnc(er);
								sb.append(er).append("}}. \n");
							}
							el = el.near.near;
						} else if (el.near.verb.equals("WHERE")) {
							if (!el.near.obj.verb.equals("")) {
								Euler et = new Euler();
								et.subj = el.near.obj;
								el.near.obj = et;
							}
							for (Euler er = el.near.subj; er != null; er = er.near) {
								for (Euler ev = el.near.obj; ev != null; ev = ev.near) {
									sb.append('{');
									for (Euler ee = ev.subj; ee != null; ee = ee.near) {
										e.rewrite(false, ee, np);
										bnp(ee);
										sb.append(ee);
									}
									sb.append(sfg(ev.subj, er));
									sb.append("} => {_:e").append(el.near.subj.uid).append(' ').append(Euler.Qselect).append(" {");
									e.rewrite(false, er, np);
									bnc(er);
									sb.append(er).append("}}. \n");
								}
							}
							el = el.near;
						} else
							el = el.near;
					}
					c = sb.toString();
					e.load(c);
					e.ext.loaded.addElement('<' + e.toURI(np.parse('<' + args[j] + '>')) + '>');
				} else if (args[j].endsWith("-prolog") || args[j].endsWith("-pterm")) {
					Euler.prolog = true;
					boolean pterm = args[j].endsWith("-pterm");
					boolean tas = false;
					boolean think = false;
					boolean nope = false;
					boolean profile = false;
					Euler el = new Euler();
					el.uid = -1;
					int jq = j;
					StringBuffer sa = new StringBuffer("feed(fpath([");
					while (j < n) {
						j++;
						if (args[j].endsWith("-test-as"))
							tas = true;
						else if (args[j].endsWith("-think"))
							think = true;
						else if (args[j].endsWith("-nope"))
							nope = true;
						else if (args[j].endsWith("-profile"))
							profile = true;
						else if (args[j].endsWith("-query") || args[j].endsWith("-filter")) {
							j++;
							jq = j;
							if (sa.charAt(sa.length() - 1) != '[')
								sa.append(',');
							sa.append("fpath('<").append(el.testURI(args[j])).append(">','log:semantics')");
							Euler ell = new Euler();
							ell.uid = -1;
							ell.ext = new EulerExt();
							ell.ext.kc = true;
							ell.load(e.toURI(np.parse('<' + args[j] + '>')));
							StringBuffer sb = new StringBuffer("data:,");
							for (Enumeration en = ell.ext.ns.keys(); en.hasMoreElements();) {
								Object nsx = en.nextElement();
								sb.append("@prefix ").append(nsx).append(' ').append(ell.ext.ns.get(nsx)).append(".\n");
							}
							Hashtable ens = ell.ext.ns;
							while (ell.near != null) {
								if (ell.near.verb == Euler.LOGimplies) {
									for (Euler elr = ell.near.obj; elr != null; elr = elr.near) {
										sb.append('{');
										for (Euler ee = ell.near.subj; ee != null; ee = ee.near) {
											e.rewrite(false, ee, np);
											bnp(ee);
											sb.append(ee);
										}
										sb.append(sfg(ell.near.subj, elr)).append("} case {").append(elr).append("}. ");
									}
									ell = ell.near;
								} else if (ell.near.verb == Euler.Qselect && ell.near.near.verb == Euler.Qwhere) {
									for (Euler elr = ell.near.obj; elr != null; elr = elr.near) {
										sb.append('{');
										for (Euler ee = ell.near.near.obj; ee != null; ee = ee.near) {
											e.rewrite(false, ee, np);
											bnp(ee);
											sb.append(ee);
										}
										sb.append(sfg(ell.near.near.obj, elr)).append("} case {").append(elr).append("}. ");
									}
									ell = ell.near.near;
								} else if (ell.near.verb.equals("WHERE")) {
									if (!ell.near.obj.verb.equals("")) {
										Euler et = new Euler();
										et.subj = ell.near.obj;
										ell.near.obj = et;
									}
									for (Euler ev = ell.near.obj; ev != null; ev = ev.near) {
										sb.append('{');
										for (Euler ee = ev.subj; ee != null; ee = ee.near) {
											e.rewrite(false, ee, np);
											bnp(ee);
											sb.append(ee);
										}
										sb.append(sfg(ev.subj, ell.near.subj)).append("} case {").append(ell.near.subj).append(
												"}. ");
									}
									ell = ell.near;
								} else
									ell = ell.near;
							}
							el.load(sb.toString());
						} else if (args[j].startsWith("-"))
							;
						else {
							if (sa.charAt(sa.length() - 1) != '[')
								sa.append(',');
							sa.append("fpath('<").append(el.testURI(args[j])).append(">','log:semantics')");
							el.load(e.toURI(np.parse('<' + args[j] + '>')));
						}
					}
					if (pterm)
						return el.near != null ? el.near.toPrologString(true, true, false) + "." : "";
					StringBuffer sb = new StringBuffer();
					for (Enumeration enr = el.ext.ns.keys(); enr.hasMoreElements();) {
						String nsx = (String) enr.nextElement();
						String nsy = (String) el.ext.ns.get(nsx);
						sb.append("pfx('").append(nsx).append("','").append(nsy).append("').\n");
					}
					sb.append('\n');
					StringBuffer rb = new StringBuffer();
					Hashtable dp = new Hashtable();
					while (el.near != null) {
						if (el.near.verb == Euler.LOGimplies) {
							Euler te = el.near.near;
							el.near.near = null;
							Euler ve = el.near.copy();
							el.near.near = te;
							Vector vt = new Vector();
							StringBuffer vb = new StringBuffer("@forAll ");
							StringBuffer vb2 = new StringBuffer();
							getVars(false, ve, vt, vb, vb2);
							vb.append(". ");
							if (vb.length() == 10)
								vb = new StringBuffer();
							boolean begin = true;
							rb.append("'log:implies'(lf((");
							for (Euler er = el.near.subj; er != null; er = er.near) {
								dpp(dp, er);
								if (!begin)
									rb.append(", ");
								if (er.verb.equals(Euler.Efindall) || er.verb.equals(Euler.LOGnotIncludes))
									er.src = "e" + er.uid;
								else
									er.src = "_";
								rb.append(er.toPrologString(false, false, false));
								begin = false;
							}
							if (el.near.obj.cverb.charAt(0) == '?') {
								if (!begin)
									rb.append(", ");
								if (nope)
									el.near.src = "_";
								rb.append("atom(").append(el.toPrologString(el.near.obj.cverb)).append("), _U").append(
										el.near.obj.uid).append("=..[").append(el.toPrologString(el.near.obj.cverb)).append(',')
										.append(el.near.obj.subj.toPrologString(true, true, false)).append(',').append(
												el.near.obj.obj.toPrologString(true, true, false)).append(",'").append(el.near.src)
										.append("']");
							}
							rb.append(", instrument('" + vb + ve + "'," + vt + ')');
							rb.append(")), lf((");
							for (Euler er = el.near.obj; er != null; er = er.near) {
								dpp(dp, er);
								if (er.verb.equals(Euler.LOGimplies)) {
									for (Euler erp = er.subj; erp != null; erp = erp.near)
										dpp(dp, erp);									
								}
								if (el.near.obj.cverb.charAt(0) == '?')
									rb.append("_U" + el.near.obj.uid);
								else {
									er.src = nope ? "_" : "'" + er.src + "'";
									rb.append(er.toPrologString(false, false, false));
								}
								begin = false;
							}
							rb.append(")),_).\n");
						} else if (el.near.verb == "case") {
							Euler te = el.near.near;
							el.near.near = null;
							Euler ve = el.near.copy();
							el.near.near = te;
							Vector vt = new Vector();
							StringBuffer vb = new StringBuffer("@forAll ");
							StringBuffer vb2 = new StringBuffer();
							getVars(false, ve, vt, vb, vb2);
							vb.append(". ");
							if (vb.length() == 10)
								vb = new StringBuffer();
							boolean begin = true;
							rb.append("'log:implies'(lf((");
							for (Euler er = el.near.subj; er != null; er = er.near) {
								dpp(dp, er);
								if (!begin)
									rb.append(", ");
								if (er.verb.equals(Euler.Efindall) || er.verb.equals(Euler.LOGnotIncludes))
									er.src = "e" + er.uid;
								else
									er.src = "_";
								rb.append(er.toPrologString(false, false, false));
								begin = false;
							}
							if (el.near.obj.cverb.charAt(0) == '?') {
								if (!begin)
									rb.append(", ");
								if (nope)
									el.near.src = "_";
								rb.append("atom(").append(el.toPrologString(el.near.obj.cverb)).append("), _U").append(
										el.near.obj.uid).append("=..[").append(el.toPrologString(el.near.obj.cverb)).append(',')
										.append(el.near.obj.subj.toPrologString(true, true, false)).append(',').append(
												el.near.obj.obj.toPrologString(true, true, false)).append(",'").append(el.near.src)
										.append("']");
							}
							ve.cverb = "=>";
							rb.append(", instrument('" + vb + ve + "'," + vt + ')');
							rb.append(")), lf(case(");
							for (Euler er = el.near.obj; er != null; er = er.near) {
								dpp(dp, er);
								if (el.near.obj.cverb.charAt(0) == '?')
									rb.append("_U" + el.near.obj.uid);
								else {
									er.src = nope ? "_" : "'<" + args[jq] + ">'";
									rb.append(er.toPrologString(false, false, false));
								}
								begin = false;
							}
							rb.append(")),_).\n");
						} else {
							dpp(dp, el.near);
							if (el.near.verb == Euler.RDFSdomain)
								dpp(dp, el.near.subj);
							if (el.near.verb == Euler.RDFSrange)
								dpp(dp, el.near.subj);
							if (el.near.verb == Euler.RDFSsubPropertyOf) {
								dpp(dp, el.near.subj);
								dpp(dp, el.near.obj);
							}
							if (el.near.verb == Euler.OWLinverseOf) {
								dpp(dp, el.near.subj);
								dpp(dp, el.near.obj);
							}
							if (el.near.verb == Euler.OWLonProperty)
								dpp(dp, el.near.obj);
							if (el.near.verb == Euler.RDFtype && el.near.obj.verb == Euler.OWLDatatypeProperty)
								dpp(dp, el.near.subj);
							if (el.near.verb == Euler.RDFtype && el.near.obj.verb == Euler.OWLObjectProperty)
								dpp(dp, el.near.subj);
							if (el.near.verb == Euler.RDFtype && el.near.obj.verb == Euler.OWLSymmetricProperty)
								dpp(dp, el.near.subj);
							if (el.near.verb == Euler.RDFtype && el.near.obj.verb == Euler.OWLTransitiveProperty)
								dpp(dp, el.near.subj);
							el.near.src = nope ? "_" : "'" + el.near.src + "'";
							rb.append(el.near.toPrologString(false, false, false)).append(".\n");
						}
						el = el.near;
					}
					sb.append(sa).append("],'log:conjunction'),").append(Euler.runner).append(").\n");
					if (nope)
						sb.append("flag('e:nope').\n");
					else
						sb.append("flag('e:pe').\n");
					if (Codd.port != 80)
						sb.append("flag(port(").append(Codd.port).append(")).\n");
					if (profile)
						sb.append("flag(profile).\n");
					sb.append('\n');
					sb.append(":- style_check(-discontiguous).\n");
					sb.append(":- style_check(-singleton).\n");
					sb.append('\n');
					for (Enumeration enr = dp.keys(); enr.hasMoreElements();)
						sb.append(":- dynamic(").append(enr.nextElement()).append("/3).\n");
					sb.append('\n');
					if (think) {
						for (Enumeration enr = dp.keys(); enr.hasMoreElements();)
							sb.append("'rdf:type'(").append(enr.nextElement()).append(",'rdf:Property',_).\n");
						sb.append('\n');
					}
					String th = sb.append(rb).toString();
					Euler.prolog = false;
					if (tas)
						return new Euler().fromWeb("http://localhost:" + Codd.port + "/.euler5s+data:," + Codd.urlEncode(th));						
					else
						return th;
				} else if (args[j].endsWith("-prolog-bchain")) {
					Euler.prolog = true;
					Euler.prologBChain = true;
					boolean tas = false;
					boolean think = false;
					boolean nope = false;
					boolean nobe = false;
					boolean nefq = false;
					boolean profile = false;
					Euler el = new Euler();
					el.uid = -1;
					StringBuffer sa = new StringBuffer("feed(fpath([");
					while (j < n) {
						j++;
						if (args[j].endsWith("-test-as"))
							tas = true;
						else if (args[j].endsWith("-think"))
							think = true;
						else if (args[j].endsWith("-nope"))
							nope = true;
						else if (args[j].endsWith("-nobe")) {
							nope = true;
							nobe = true;
						}
						else if (args[j].endsWith("-nefq"))
							nefq = true;
						else if (args[j].endsWith("-profile"))
							profile = true;
						else if (args[j].endsWith("-query") || args[j].endsWith("-filter")) {
							j++;
							if (sa.charAt(sa.length() - 1) != '[')
								sa.append(',');
							sa.append("fpath('<").append(el.testURI(args[j])).append(">','log:semantics')");
							Euler ell = new Euler();
							ell.uid = -1;
							ell.ext = new EulerExt();
							ell.ext.kc = true;
							ell.load(e.toURI(np.parse('<' + args[j] + '>')));
							StringBuffer sb = new StringBuffer("data:,");
							for (Enumeration en = ell.ext.ns.keys(); en.hasMoreElements();) {
								Object nsx = en.nextElement();
								sb.append("@prefix ").append(nsx).append(' ').append(ell.ext.ns.get(nsx)).append(".\n");
							}
							Hashtable ens = ell.ext.ns;
							while (ell.near != null) {
								if (ell.near.verb == Euler.LOGimplies) {
									ell.near.cverb = "case";
									sb.append(ell.near);
								} else
									sb.append("{_: e:true 1} case {").append(ell.near).append("}. ");
								ell = ell.near;
							}
							el.load(sb.toString());
						} else if (args[j].startsWith("-"))
							;
						else {
							if (sa.charAt(sa.length() - 1) != '[')
								sa.append(',');
							sa.append("fpath('<").append(el.testURI(args[j])).append(">','log:semantics')");
							el.load(e.toURI(np.parse('<' + args[j] + '>')));
						}
					}
					StringBuffer sb = new StringBuffer();
					for (Enumeration enr = el.ext.ns.keys(); enr.hasMoreElements();) {
						String nsx = (String) enr.nextElement();
						String nsy = (String) el.ext.ns.get(nsx);
						sb.append("pfx('").append(nsx).append("','").append(nsy).append("').\n");
					}
					sb.append('\n');
					StringBuffer rb = new StringBuffer();
					Hashtable dp = new Hashtable();
					while (el.near != null) {
						boolean begin = true;
						boolean etrue = false;
						if (el.near.verb == Euler.LOGimplies) {
							rb.append("rule(");
							if (el.near.obj.cverb.charAt(0) == '?') {
								rb.append("vv([").append(el.near.obj.toPrologBChainString(el.near.obj.cverb)).append(',')
										.append(el.near.obj.subj.toPrologBChainString(true, true)).append(",")
										.append(el.near.obj.obj.toPrologBChainString(true, true)).append(",'")
										.append(el.near.obj.src).append("'])");
							} else {
								dpp(dp, el.near.obj);
								el.near.obj.src = "'" + el.near.obj.src + "'";
								rb.append(el.near.obj.toPrologBChainString(false, false));
							}
							rb.append(",(");
							for (Euler er = el.near.subj; er != null; er = er.near) {
								dpp(dp, er);
								if (!begin)
									rb.append(',');
								er.src = "_";
								if (er.verb == Euler.Etrue) {
									er.subj.cverb = "_:";
									etrue = true;
								}
								rb.append(er.toPrologBChainString(false, false));
								begin = false;
							}
							if (!etrue)
								rb.append(",'e:true'(_,1,_)");
							rb.append(")).\n");
							if (el.near.obj.verb == Euler.Eboolean && nefq) {
								rb.append("rule(");
								begin = true;
								if (el.near.obj.obj.cverb.equals("e:T"))
									el.near.obj.obj.cverb = "e:F";
								else if (el.near.obj.obj.cverb.equals("e:F"))
									el.near.obj.obj.cverb = "e:T";
								rb.append(el.near.obj.toPrologBChainString(false, false));
								rb.append(",(");
								for (Euler er = el.near.subj; er != null; er = er.near) {
									if (!begin)
										rb.append(',');
									if (er.verb == Euler.Etrue)
										rb.append("'math:difference'([1.0,").append(er.obj.toPrologBChainString(false, false))
												.append("],_U").append(er.obj.uid).append(",_),'e:true'(_,_U").append(er.obj.uid)
												.append(",_)");
									else
										rb.append(er.toPrologBChainString(false, false));
									begin = false;
								}
								if (!etrue)
									rb.append(",'e:true'(_,0,_)");
								rb.append(")).\n");
							}
						} else if (el.near.verb == "case") {
							dpp(dp, el.near.obj);
							rb.append("goal(");
							el.near.obj.src = "_";
							if (el.near.obj.verb == Euler.Eboolean)
								el.near.obj.obj = np.parse("?B" + el.near.obj.uid);
							rb.append(el.near.obj.toPrologBChainString(false, false));
							rb.append(",(");
							for (Euler er = el.near.subj; er != null; er = er.near) {
								dpp(dp, er);
								if (!begin)
									rb.append(',');
								er.src = "_";
								rb.append(er.toPrologBChainString(false, false));
								begin = false;
							}
							rb.append(")).\n");
						} else {
							dpp(dp, el.near);
							if (el.near.verb == Euler.RDFSdomain)
								dpp(dp, el.near.subj);
							if (el.near.verb == Euler.RDFSrange)
								dpp(dp, el.near.subj);
							if (el.near.verb == Euler.RDFSsubPropertyOf) {
								dpp(dp, el.near.subj);
								dpp(dp, el.near.obj);
							}
							if (el.near.verb == Euler.OWLinverseOf) {
								dpp(dp, el.near.subj);
								dpp(dp, el.near.obj);
							}
							if (el.near.verb == Euler.OWLonProperty)
								dpp(dp, el.near.obj);
							if (el.near.verb == Euler.RDFtype && el.near.obj.verb == Euler.OWLDatatypeProperty)
								dpp(dp, el.near.subj);
							if (el.near.verb == Euler.RDFtype && el.near.obj.verb == Euler.OWLObjectProperty)
								dpp(dp, el.near.subj);
							if (el.near.verb == Euler.RDFtype && el.near.obj.verb == Euler.OWLSymmetricProperty)
								dpp(dp, el.near.subj);
							if (el.near.verb == Euler.RDFtype && el.near.obj.verb == Euler.OWLTransitiveProperty)
								dpp(dp, el.near.subj);
							el.near.src = "'" + el.near.src + "'";
							rb.append(nobe ? "" : "rule(").append(el.near.toPrologBChainString(false, false)).append(
									nobe ? ".\n" : ",('e:true'(_,1,_))).\n");
							if (el.near.verb == Euler.Eboolean && nefq) {
								rb.append("rule(");
								if (el.near.obj.cverb.equals("e:T"))
									el.near.obj.cverb = "e:F";
								else if (el.near.obj.cverb.equals("e:F"))
									el.near.obj.cverb = "e:T";
								rb.append(el.near.toPrologBChainString(false, false)).append(",('e:true'(_,0,_))).\n");
							}
						}
						el = el.near;
					}
					sb.append(sa).append("],'log:conjunction'),").append(Euler.runner).append(").\n");
					sb.append("flag('e:bchain').\n");
					if (nope)
						sb.append("flag('e:nope').\n");
					else
						sb.append("flag('e:pe').\n");
					if (nobe)
						sb.append("flag('e:nobe').\n");
					else
						sb.append("flag('e:be').\n");
					if (Codd.port != 80)
						sb.append("flag(port(").append(Codd.port).append(")).\n");
					if (profile)
						sb.append("flag(profile).\n");
					sb.append('\n');
					sb.append(":- style_check(-discontiguous).\n");
					sb.append(":- style_check(-singleton).\n");
					sb.append('\n');
					for (Enumeration enr = dp.keys(); enr.hasMoreElements();)
						sb.append(":- dynamic(").append(enr.nextElement()).append("/3).\n");
					sb.append('\n');
					if (think) {
						for (Enumeration enr = dp.keys(); enr.hasMoreElements();)
							sb.append("'rdf:type'(").append(enr.nextElement()).append(",'rdf:Property',_).\n");
						sb.append('\n');
					}
					String th = sb.append(rb).toString();
					Euler.prolog = false;
					Euler.prologBChain = false;
					if (tas)
						return new Euler().fromWeb("http://localhost:" + Codd.port + "/.euler5s+data:," + Codd.urlEncode(th));						
					else
						return th;
				} else if (args[j].endsWith("-sem") || args[j].endsWith("-semterm") || args[j].endsWith("-semquery")) {
					Euler.sem = true;
					boolean semterm = args[j].endsWith("-semterm");
					boolean semquery = args[j].endsWith("-semquery");
					boolean test = false;
					boolean tas = false;
					boolean nope = false;
					boolean nobranch = false;
					boolean quiet = false;
					boolean quick = false;
					boolean think = false;
					boolean tquery = false;
					boolean answer = false;
					String scope = "";
					String marker = "e:rules";
					Euler el = new Euler();
					Euler.doc = 1;
					Euler.docv = new Vector();
					Euler.uidc = 1;
					el.uid = -1;
					int jq = j;
					long step = 500000;
					while (j < n) {
						j++;
						if (args[j].endsWith("-test"))
							test = true;
						else if (args[j].endsWith("-test-as"))
							tas = true;
						else if (args[j].endsWith("-nope"))
							nope = true;
						else if (args[j].endsWith("-no-branch"))
							nobranch = true;
						else if (args[j].endsWith("-quiet"))
							quiet = true;
						else if (args[j].endsWith("-quick"))
							quick = true;
						else if (args[j].endsWith("-think"))
							think = true;
						else if (args[j].endsWith("-step"))
							step = Long.parseLong(args[++j]);
						else if (args[j].endsWith("-rules"))
							el.load("data:,_: e:marker e:rules.");
						else if (args[j].endsWith("-trules"))
							el.load("data:,_: e:marker e:trules.");
						else if (args[j].endsWith("-query") || args[j].endsWith("-filter"))
							el.load("data:,_: e:marker e:query.");
						else if (args[j].endsWith("-tquery")) {
							tquery = true;
							el.load("data:,_: e:marker e:tquery.");
						}
						else if (args[j].endsWith("-pass"))
							el.load("data:,_: e:marker e:query. {?S ?P ?O} => {?S ?P ?O}.");
						else if (args[j].startsWith("-"))
							;
						else {
							el.load(e.toURI(np.parse('<' + args[j] + '>')));
							if (!args[j-1].endsWith("-query") && !args[j-1].endsWith("-filter") && !args[j-1].endsWith("-tquery"))
								scope = scope + (scope.equals("")?"":",") + np.parse("'<" + args[j] + ">'");
							else
								answer = false;
							el.load("data:,_: e:marker e:rules.");
						}
					}
					if (semterm)
						return el.near != null ? el.near.toSemString(true, true, false) + "." : "";
					StringBuffer rb = new StringBuffer();
					Hashtable dp = new Hashtable();
					if (!semquery) {
						for (Enumeration enr = el.ext.ns.keys(); enr.hasMoreElements();) {
							String nsx = (String) enr.nextElement();
							String nsy = (String) el.ext.ns.get(nsx);
							rb.append("pfx('").append(nsx).append("','").append(nsy).append("').\n");
						}
						rb.append('\n');
					}
					while (el.near != null) {
						StringBuffer cb = new StringBuffer();
						if (marker.equals("e:trules")) {
							dp.put("'e:conditional'", new Object());
							cb.append("'e:conditional'([");
						}
						if (marker.equals("e:tquery"))
							cb.append("'e:biconditional'([");
						if (el.near.cverb.equals("e:marker")) {
							marker = el.near.obj.cverb;
							if (marker.equals("e:query") || marker.equals("e:tquery"))
								answer = true;
							else if (answer && (marker.equals("e:rules") || marker.equals("e:trules"))) {
								rb.append("[] := answer(_) => goal.\n");
								answer = false;
							}
						}
						else if (el.near.verb == Euler.LOGimplies) {
							boolean begin = true;
							if (marker.equals("e:trules") || marker.equals("e:tquery")) 
								cb.append(el.near.obj.toSemString(true, true, false));
							Euler te = el.near.near;
							el.near.near = null;
							Euler ve = el.near.subj.copy();
							if (marker.equals("e:trules") || marker.equals("e:tquery")) 
								ve = el.near.copy();
							el.near.near = te;
							Vector vt = new Vector();
							StringBuffer vb = new StringBuffer("@forAll ");
							StringBuffer vb2 = new StringBuffer();
							getVars(true, ve, vt, vb, vb2);
							if (marker.equals("e:tquery")) {
								if (vb.charAt(vb.length() - 1) != ' ')
									vb.append(',');
								vb.append("var:TQUERY");
								if (vb2.length() != 0)
									vb2.append(',');
								vb2.append("_TQUERY");
							}
							vb.append(". ");
							if (vb.length() == 10)
								vb = new StringBuffer();
							rb.append("[").append(el.toSemString(el.near.src, false));
							if (vb2.length() != 0)
								rb.append(",").append(vb2);
							rb.append("] := ");
							int rbl = rb.length();
							for (Euler er = el.near.subj; er != null; er = er.near) {
								dpp(dp, er);
								if (er.cverb.equals("e:findall"))
									dpp(dp, er.obj.getRest().getFirst());
								if ((marker.equals("e:trules") || marker.equals("e:tquery")) && er.cverb.equals("e:boolean")) 
									cb.append(',').append(er.toSemString(false, true, false));
								else if (marker.equals("e:trules") && er.cverb.equals("e:true")) 
									cb.append("],").append(er.obj.toSemString(false, false, false)).append(')');
								else {
									if (!begin)
										rb.append(", ");
									rb.append(er.toSemString(false, false, false));
									begin = false;
								}
							}
							//if (el.near.obj.cverb.charAt(0) == '?' && el.near.obj.subj != null && el.near.obj.obj != null) {
							//	if (!begin)
							//		rb.append(", ");
							//	rb.append("atom(").append(el.toSemString(el.near.obj.cverb, false)).append("), _U").append(
							//			el.near.obj.uid).append(" =.. [").append(el.toSemString(el.near.obj.cverb, false)).append(',')
							//			.append(el.near.obj.subj.toSemString(true, true, false)).append(',').append(
							//					el.near.obj.obj.toSemString(true, true, false))
							//			.append("]");
							//}
							if (marker.equals("e:trules")) {
								if (rb.length() == rbl)
									rb.append("true");
								if (cb.indexOf("]") == -1)
									cb.append("],1.0)");
								rb.append(" => ").append(cb);
							}
							else if (marker.equals("e:tquery")) {
								cb.append("],_TQUERY)");
								if (rb.charAt(rb.length()-1) != ' ') rb.append(", ");
								rb.append(cb).append(" => ").append("answer(").append(cb).append(')');
							}
							else {
								rb.append(" => ");
								if (marker.equals("e:query")) rb.append("answer((");
								if (el.near.obj.verb.equals("{}")
										|| el.near.obj.verb.equals("\"false\"^^xsd:boolean")
										|| el.near.obj.cverb.equals("^^")
										&& el.near.obj.subj.verb.equals("\"false\"")
										&& el.near.obj.obj.verb.equals(Euler.XSDboolean))
									rb.append("false");
								else {
									begin = true;
									for (Euler er = el.near.obj; er != null; er = er.near) {
										dpp(dp, er);
										if (er.verb.equals(Euler.LOGimplies)) {
											for (Euler erp = er.subj; erp != null; erp = erp.near)
												dpp(dp, erp);									
										}
										if (!begin)
											rb.append(", ");
										if (el.near.obj.cverb.charAt(0) == '?' && el.near.obj.subj != null && el.near.obj.obj != null)
											//rb.append("_U" + el.near.obj.uid);
											rb.append("varpred(").append(el.near.obj.subj.toSemString(true, true, false)).append(',')
												.append(el.near.obj.toSemString(el.near.obj.cverb, false)).append(',')
												.append(el.near.obj.obj.toSemString(true, true, false)).append(')');
										else
											rb.append(er.toSemString(false, false, false));
										begin = false;
									}
								}
								if (marker.equals("e:query")) {
									rb.append("))");
									if (semquery)
										return rb.toString();
								}
							}
							rb.append(".\n");
						} else {
							dpp(dp, el.near);
							if (el.near.verb == Euler.RDFSdomain)
								dpp(dp, el.near.subj);
							if (el.near.verb == Euler.RDFSrange)
								dpp(dp, el.near.subj);
							if (el.near.verb == Euler.RDFSsubPropertyOf) {
								dpp(dp, el.near.subj);
								dpp(dp, el.near.obj);
							}
							if (el.near.verb == Euler.OWLinverseOf) {
								dpp(dp, el.near.subj);
								dpp(dp, el.near.obj);
							}
							if (el.near.verb == Euler.OWLonProperty)
								dpp(dp, el.near.obj);
							if (el.near.verb == Euler.RDFtype && el.near.obj.verb == Euler.OWLDatatypeProperty)
								dpp(dp, el.near.subj);
							if (el.near.verb == Euler.RDFtype && el.near.obj.verb == Euler.OWLObjectProperty)
								dpp(dp, el.near.subj);
							if (el.near.verb == Euler.RDFtype && el.near.obj.verb == Euler.OWLSymmetricProperty)
								dpp(dp, el.near.subj);
							if (el.near.verb == Euler.RDFtype && el.near.obj.verb == Euler.OWLTransitiveProperty)
								dpp(dp, el.near.subj);
							if (marker.equals("e:trules")) {
								cb.append(el.near.toSemString(false, true, false)).append("],1.0)");
								rb.append("[").append(el.toSemString(el.near.src, false)).append("] := true => ").append(cb).append(".\n");
								rb.append(el.near.toSemString(false, false, false)).append(".\n");
							} else if (marker.equals("e:tquery")) {
								cb.append(el.near.toSemString(false, true, false)).append("],_TQUERY)");
								rb.append("[").append(el.toSemString(el.near.src, false)).append("] := ").append(cb).append(" => answer(").append(cb).append(").\n");
							} else
								rb.append(el.near.toSemString(false, false, true)).append(". steps([").append(el.toSemString(el.near.src, false)).append("],true,")
									.append(el.near.toSemString(false, false, true)).append(",([").append(el.toSemString(el.near.src, false)).append("] := true => ")
									.append(el.near.toSemString(false, false, true)).append(")).\n");
						}
						el = el.near;
					}
					if (answer) {
						rb.append("[] := answer(_) => goal.\n");
						answer = false;
					}
					StringBuffer sb = new StringBuffer();
					sb.append(":- op(1200,xfx,':=').\n");
					sb.append(":- op(1199,xfx,'=>').\n");
					sb.append('\n');
					if (tas) {
						sb.append(":- style_check(-discontiguous).\n");
						sb.append(":- style_check(-singleton).\n");
						sb.append('\n');
						sb.append(":- dynamic(answer/1).\n");
						for (Enumeration enr = dp.keys(); enr.hasMoreElements();)
							sb.append(":- dynamic(").append(enr.nextElement()).append("/2).\n");
						sb.append('\n');
					}
					if (Codd.port != 80)
						sb.append("flag(port(").append(Codd.port).append(")).\n");
					if (nope)
						sb.append("flag(nope).\n");
					if (nobranch)
						sb.append("flag('no-branch').\n");
					if (quiet)
						sb.append("flag(quiet).\n");
					if (quick)
						sb.append("flag(quick).\n");
					if (think)
						sb.append("flag(think).\n");
					if (tquery)
						sb.append("flag(tquery).\n");
					sb.append("flag(step(").append(step).append(")).\n");
					sb.append("flag(scope([").append(scope).append("])).\n");
					sb.append('\n');
					if (tas && !Euler.semgen.equals("")) {
						sb.append(Euler.semgen).append('\n');
						Euler.semgen = "";
					}
					sb.append(rb);
					String th = sb.toString();
					Euler.sem = false;
					/*if (test) {
						ByteArrayOutputStream baos = new ByteArrayOutputStream();
						PrintWriter pw = new PrintWriter(baos);
						jPrologAPI api = new jPrologAPI(Codd.nativeToAscii(Euler.euler + th), null, pw, null, null);
						Hashtable result = api.query("main.", new Hashtable());
						while (result != null)
							result = api.retry();
						pw.flush();
						return baos.toString();
					} else*/ if (tas)
						return new Euler().fromWeb("http://localhost:" + Codd.port + "/.sem+data:," + Codd.urlEncode(th));						
					else
						return th;
				} else if (args[j].endsWith("-semi")) {
					boolean test = false;
					boolean tas = false;
					boolean nope = false;
					String th = null;
					while (j < n) {
						j++;
						if (args[j].endsWith("-test"))
							test = true;
						else if (args[j].endsWith("-test-as"))
							tas = true;
						else if (args[j].endsWith("-nope"))
							nope = true;
						else if (args[j].startsWith("-"))
							;
						else
							th = new Euler().fromWeb(args[j]);
					}
					if (nope)
						th = th + "flag(nope).\n";
					/*if (test) {
						ByteArrayOutputStream baos = new ByteArrayOutputStream();
						PrintWriter pw = new PrintWriter(baos);
						jPrologAPI api = new jPrologAPI(Codd.nativeToAscii(Euler.euler + th), null, pw, null, null);
						Hashtable result = api.query("main.", new Hashtable());
						while (result != null)
							result = api.retry();
						pw.flush();
						return baos.toString();
					} else*/ if (tas)
						return new Euler().fromWeb("http://localhost:" + Codd.port + "/.sem+data:," + Codd.urlEncode(th));						
					else
						return th;
				} else if (args[j].endsWith("-sql")) {
					Euler el = new Euler();
					Euler.doc = 1;
					Euler.docv = new Vector();
					Euler.uidc = 1;
					el.uid = -1;
					while (j < n) {
						j++;
						if (args[j].endsWith("-query") || args[j].endsWith("-filter"))
							j++;
						else if (args[j].startsWith("-"))
							;
						else
							el.load(e.toURI(np.parse('<' + args[j] + '>')));
					}
					System.out.println("BEGIN TRANSACTION;");
					System.out.println("CREATE TABLE pfx(prefix varchar(8192), namespace varchar(8192));");
					System.out.println("CREATE TABLE rdf(subject varchar(8192), predicate varchar(8192), object varchar(8192), source varchar(8192));");
					System.out.println();
					for (Enumeration enr = el.ext.ns.keys(); enr.hasMoreElements();) {
						String nsx = (String) enr.nextElement();
						String nsy = (String) el.ext.ns.get(nsx);
						System.out.println("INSERT INTO pfx VALUES('" + nsx + "','" + nsy + "');");
					}
					System.out.println();
					while (el.near != null) {
						System.out.println("INSERT INTO rdf VALUES('" + el.near.subj.toN3String().replace("'", "''") + "','" +
							el.near.cverb + "','" + el.near.obj.toN3String().replace("'", "''") + "','" + el.near.src + "');");
						el = el.near;
					}
					System.out.println();
					System.out.println("CREATE INDEX subject_index ON rdf (subject);");
					System.out.println("CREATE INDEX object_index ON rdf (object);");
					System.out.println("COMMIT;");
					return "";
				} else if (args[j].endsWith("-pass")) {
					boolean why = false;
					boolean once = false;
					boolean debug = false;
					boolean tas = false;
					Euler.doc = 1;
					Euler.docv = new Vector();
					Euler.uidc = 1;
					while (j < n) {
						j++;
						if (args[j].endsWith("-test-as"))
							tas = true;
						else if (args[j].endsWith("-why"))
							why = true;
						else if (args[j].endsWith("-once"))
							once = true;
						else if (args[j].endsWith("-debug"))
							debug = true;
						else if (args[j].endsWith("-trules")) {
							Euler el = new Euler();
							el.uid = -1;
							el.load(e.toURI(np.parse('<' + args[++j] + '>')));
							StringBuffer rb = new StringBuffer();
							Hashtable dp = new Hashtable();
							for (Enumeration enr = el.ext.ns.keys(); enr.hasMoreElements();) {
								String nsx = (String) enr.nextElement();
								String nsy = (String) el.ext.ns.get(nsx);
								rb.append("@prefix ").append(nsx).append(" ").append(nsy).append(".\n");
							}
							rb.append('\n');
							while (el.near != null) {
								StringBuffer cb = new StringBuffer();
								cb.append('(');
								if (el.near.verb == Euler.LOGimplies) {
									boolean begin = true;
									cb.append('{').append(el.near.obj).append('}');
									int rbl = rb.length();
									for (Euler er = el.near.subj; er != null; er = er.near) {
										if (er.cverb.equals("e:boolean")) 
											cb.append(" {").append(er).append('}');
										else if (er.cverb.equals("e:true")) 
											cb.append(") e:conditional ").append(er.obj);
										else {
											if (begin)
												rb.append('{');
											rb.append(er);
											begin = false;
										}
									}
									if (cb.indexOf(")") == -1)
										cb.append(") e:conditional 1.0");
									if (rb.length() == rbl)
										rb.append(cb);
									else
										rb.append("} => {").append(cb).append('}');
									rb.append(".\n");
								} else
									rb.append(el.near).append("\n");
								el = el.near;
							}
							return rb.toString();
						}
						else if (args[j].endsWith("-query") || args[j].endsWith("-filter")) {
							Euler el = new Euler();
							el.uid = -1;
							el.load(e.toURI(np.parse('<' + args[++j] + '>')));
							StringBuffer sb = new StringBuffer("data:,");
							for (Enumeration en = el.ext.ns.keys(); en.hasMoreElements();) {
								Object nsx = en.nextElement();
								sb.append("@prefix ").append(nsx).append(' ').append(el.ext.ns.get(nsx)).append(".\n");
							}
							Hashtable ens = el.ext.ns;
							while (el.near != null) {
								if (el.near.verb == Euler.LOGimplies) {
									for (Euler er = el.near.obj; er != null; er = er.near) {
										sb.append('{');
										for (Euler ee = el.near.subj; ee != null; ee = ee.near) {
											e.rewrite(false, ee, np);
											bnp(ee);
											sb.append(ee);
										}
										sb.append(sfg(el.near.subj, er));
										e.rewrite(false, er, np);
										bnc(er);
										sb.append("} => {(").append(er).insert(sb.length() - 2, ")}").append("{(").append(er)
												.insert(sb.length() - 2, ")} => []");
									}
									el = el.near;
								} else if (el.near.verb == Euler.Qselect && el.near.near.verb == Euler.Qwhere) {
									for (Euler er = el.near.obj; er != null; er = er.near) {
										sb.append('{');
										for (Euler ee = el.near.near.obj; ee != null; ee = ee.near) {
											e.rewrite(false, ee, np);
											bnp(ee);
											sb.append(ee);
										}
										sb.append(sfg(el.near.near.obj, er));
										e.rewrite(false, er, np);
										bnc(er);
										sb.append("} => {(").append(er).insert(sb.length() - 2, ")}").append("{(").append(er)
												.insert(sb.length() - 2, ")} => []");
									}
									el = el.near.near;
								} else if (el.near.verb.equals("WHERE")) {
									if (!el.near.obj.verb.equals("")) {
										Euler et = new Euler();
										et.subj = el.near.obj;
										el.near.obj = et;
									}
									for (Euler er = el.near.subj; er != null; er = er.near) {
										for (Euler ev = el.near.obj; ev != null; ev = ev.near) {
											sb.append('{');
											for (Euler ee = ev.subj; ee != null; ee = ee.near) {
												e.rewrite(false, ee, np);
												bnp(ee);
												sb.append(ee);
											}
											sb.append(sfg(ev.subj, er));
											e.rewrite(false, er, np);
											bnc(er);
											if (er.toString().endsWith(". "))
												sb.append("} => {(").append(er).insert(sb.length() - 2, ")}").append("{(").append(
														er).insert(sb.length() - 2, ")} => []");
											else
												sb.append("} => {(").append(er).append(")}. ").append("{(").append(er).append(
														")} => []. ");
										}
									}
									el = el.near;
								} else
									el = el.near;
							}
							e.load(sb.toString());
						} else if (args[j].startsWith("-"))
							;
						else
							e.load(e.toURI(np.parse('<' + args[j] + '>')));
					}
					StringBuffer sb = new StringBuffer();
					for (Enumeration en = e.ext.ns.keys(); en.hasMoreElements();) {
						Object nsx = en.nextElement();
						sb.append("@prefix ").append(nsx).append(' ').append(e.ext.ns.get(nsx)).append(".\n");
					}
					sb.append('\n');
					while (e.near != null) {
						sb.append(e.near).setCharAt(sb.length() - 1, '\n');
						e = e.near;
					}
					String th = sb.toString();
					if (tas)
						return new Euler().fromWeb("http://localhost:" + Codd.port + "/.euler3+" + (why ? "--why+" : "")
								+ (once ? "--once+" : "") + (debug ? "--debug+" : "") + "data:," + Codd.urlEncode(th));
					else
						return th;
				} else if (args[j].endsWith("-json")) {
					boolean tas = false;
					Euler el = new Euler();
					el.uid = -1;
					while (j < n) {
						j++;
						if (args[j].endsWith("-test-as"))
							tas = true;
						else if (args[j].endsWith("-query") || args[j].endsWith("-filter")) {
							Euler ell = new Euler();
							ell.uid = -1;
							ell.ext = new EulerExt();
							ell.ext.kc = true;
							ell.load(e.toURI(np.parse('<' + args[++j] + '>')));
							StringBuffer sb = new StringBuffer("data:,");
							for (Enumeration en = ell.ext.ns.keys(); en.hasMoreElements();) {
								Object nsx = en.nextElement();
								sb.append("@prefix ").append(nsx).append(' ').append(ell.ext.ns.get(nsx)).append(".\n");
							}
							Hashtable ens = ell.ext.ns;
							while (ell.near != null) {
								if (ell.near.verb == Euler.LOGimplies) {
									sb.append('{');
									for (Euler ee = ell.near.subj; ee != null; ee = ee.near) {
										e.rewrite(false, ee, np);
										bnp(ee);
										sb.append(ee);
									}
									sb.append(sfg(ell.near.subj, ell.near.obj)).append("} => {}. ");
									ell = ell.near;
								} else if (ell.near.verb == Euler.Qselect && ell.near.near.verb == Euler.Qwhere) {
									sb.append('{');
									for (Euler ee = ell.near.near.obj; ee != null; ee = ee.near) {
										e.rewrite(false, ee, np);
										bnp(ee);
										sb.append(ee);
									}
									sb.append(sfg(ell.near.near.obj, ell.near.obj)).append("} => {}. ");
									ell = ell.near.near;
								} else if (ell.near.verb.equals("WHERE")) {
									if (!ell.near.obj.verb.equals("")) {
										Euler et = new Euler();
										et.subj = ell.near.obj;
										ell.near.obj = et;
									}
									for (Euler ev = ell.near.obj; ev != null; ev = ev.near) {
										sb.append('{');
										for (Euler ee = ev.subj; ee != null; ee = ee.near) {
											e.rewrite(false, ee, np);
											bnp(ee);
											sb.append(ee);
										}
										sb.append(sfg(ev.subj, ell.near.subj)).append("} => {}. ");
									}
									ell = ell.near;
								} else
									ell = ell.near;
							}
							el.load(sb.toString());
						} else if (args[j].startsWith("-"))
							;
						else
							el.load(e.toURI(np.parse('<' + args[j] + '>')));
					}
					StringBuffer sb = new StringBuffer();
					sb.append("{\n  \"GND\":{\n    ");
					for (Enumeration enr = el.ext.ns.keys(); enr.hasMoreElements();) {
						Object nsx = enr.nextElement();
						String nsy = (String) el.ext.ns.get(nsx);
						if (sb.charAt(sb.length() - 1) != ' ')
							sb.append(",\n    ");
						sb.append("\"").append(nsx).append("\":\"").append(nsy.substring(1, nsy.length() - 1)).append("\"");
					}
					sb.append("\n  }");
					Hashtable cases = new Hashtable();
					while (el.near != null) {
						if (el.near.verb == Euler.LOGimplies) {
							String hk = el.near.obj.cverb;
							if (hk.equals("{}"))
								hk = "";
							StringBuffer rb = (StringBuffer) cases.get(hk);
							if (rb == null)
								rb = new StringBuffer();
							if (rb.length() > 0)
								rb.append(",\n    ");
							rb.append("{head:").append(el.near.obj.toJsonString(false, false)).append(", body:[").append(
									el.near.subj.toJsonString(true, false)).append("]}");
							cases.put(hk, rb);
						} else {
							String hk = el.near.cverb;
							StringBuffer rb = (StringBuffer) cases.get(hk);
							if (rb == null)
								rb = new StringBuffer();
							if (rb.length() > 0)
								rb.append(",\n    ");
							rb.append("{head:").append(el.near.toJsonString(false, false)).append(", body:[]}");
							cases.put(hk, rb);
						}
						el = el.near;
					}
					for (Enumeration enr = cases.keys(); enr.hasMoreElements();) {
						Object v = enr.nextElement();
						if (sb.charAt(sb.length() - 1) != ' ')
							sb.append(",\n  ");
						sb.append('"').append(v).append("\":[\n    ").append(cases.get(v)).append("\n  ]");
					}
					sb.append("\n}");
					String th = sb.toString();
					if (tas) {
						String t = "http://localhost:" + Codd.port + "/.euler4+data:," + Codd.urlEncode(th);						
						return new Euler().fromWeb("http://localhost:" + Codd.port + "/.json+" + Codd.urlEncode(t));						
					} else
						return th;
				} else if (args[j].endsWith("-prover9")) {
					Euler el = new Euler();
					el.uid = -9;
					while (j < n)
						el.load(e.toURI(np.parse('<' + args[++j] + '>')));
					StringBuffer sb = new StringBuffer();
					sb.append("set(auto).\n");
					int eh = sb.length();
					sb.append("clauses(sos).\n\n");
					for (Enumeration enr = el.ext.ns.keys(); enr.hasMoreElements();) {
						Object nsx = enr.nextElement();
						String nsy = (String) el.ext.ns.get(nsx);
						sb.append("qname(\"").append(nsx).append("\") = iri(\"").append(nsy.substring(1, nsy.length() - 1)).append(
								"\").\n");
					}
					sb.append('\n');
					while (el.near != null) {
						if (el.near.verb == Euler.LOGimplies) {
							boolean begin = true;
							if (el.near.subj.cverb != "{}") {
								for (Euler er = el.near.subj; er != null; er = er.near) {
									if (!begin)
										sb.append(" | ");
									if (er.verb == Euler.LOGimplies) {
										sb.append(" ");
										sb.append(er.subj.toProver9String());
									} else {
										sb.append("- ");
										sb.append(er.toProver9String());
									}
									begin = false;
								}
							}
							if (el.near.obj.cverb != "{}") {
								for (Euler er = el.near.obj; er != null; er = er.near) {
									if (!begin)
										sb.append(" | ");
									sb.append(er.toProver9String());
									begin = false;
								}
							}
							sb.append(".\n");
						} else {
							sb.append(el.near.toProver9String()).append(".\n");
							if (el.near.verb == Euler.Ehint)
								sb.insert(eh, el.getLit(el.near.obj));
						}
						el = el.near;
					}
					sb.append("end_of_list.\n");
					if (Outputter.log)
						Outputter.getInstance().log("EulerRunner", "-prover9", sb.toString(), ILogger.FINE);
					File f = new File(System.getProperty("java.io.tmpdir"), "prover9.in");
					PrintStream ps = new PrintStream(new FileOutputStream(f), true);
					ps.print(sb);
					ps.close();
					Process rp = new Process("prover9 -f " + f, null);
					rp.start();
					long steps = Configuration.getInstance().getSteps();
					if (steps == -1) {
						while (rp.isRunning())
							Thread.sleep(100);
					} else {
						while (rp.isRunning() && steps > 0) {
							Thread.sleep(100);
							steps = steps - 100;
						}
						if (steps <= 0) {
							rp.stop();
							return "# No proof found: timeout";
						}
					}
					return "[] = \"\"\"Euler-" + Configuration.getInstance().getVersion() + " " + new Date().toGMTString() + "\n"
							+ rp.getOutput() + "\"\"\".";
				}
				else if (args[j].startsWith("-"))
					;
			}
			e.prepare();
			String p = e.proof(c);
			if (!Configuration.getInstance().getProofExplanation()) {
				Euler el = new Euler();
				el.uid = -1;
				el.load("data:," + p);
				StringBuffer sb = new StringBuffer();
				for (Enumeration enr = el.ext.ns.keys(); enr.hasMoreElements();) {
					Object nsx = enr.nextElement();
					sb.append("@prefix ").append(nsx).append(' ').append(el.ext.ns.get(nsx)).append(".\n");
				}
				sb.append('\n');
				for (Euler eu = el; eu.near != null; eu = eu.near) {
					if (eu.near.verb == Euler.Qselect) {
						Euler en = eu.near.near;
						eu.near = eu.near.obj;
						eu.near.near = en;
					}
				}
				while (el.near != null) {
					Euler eu = el.near.near;
					while (eu != null) {
						if (eu.unify(el.near, e, null))
							break;
						eu = eu.near;
					}
					if (eu == null && el.near.cverb != "vv")
						sb.append(el.near).append('\n');
					el = el.near;
				}
				p = sb.toString();
			}
			Configuration.getInstance().setThink(false);
			Configuration.getInstance().setProofExplanation(true);
			Configuration.getInstance().setSteps(-1);
			Configuration.getInstance().setRunLocal(false);
			return p;
		} catch (Throwable t) {
			t.printStackTrace();
			return null;
		}
	}

	static void getVars(boolean f, Euler er, Vector vt, StringBuffer vb, StringBuffer vb2) {
		if (er.subj != null)
			getVars(true, er.subj, vt, vb, vb2);
		if (er.obj != null)
			getVars(true, er.obj, vt, vb, vb2);
		if (er.cverb != null && er.cverb.length() > 1 && er.cverb.charAt(0) == '?') {
			String vs = "'\"http://localhost/var#" + er.cverb.substring(1) + "\"'";
			if (!vt.contains(vs)) {
				vt.addElement(vs);
				vt.addElement("_" + er.cverb.substring(1));
				if (vb.charAt(vb.length() - 1) != ' ')
					vb.append(',');
				vb.append("var:" + er.cverb.substring(1));
				if (vb2.length() != 0)
					vb2.append(',');
				vb2.append("_" + er.cverb.substring(1));
			}
			er.cverb = "var:" + er.cverb.substring(1);
		}
		if (f && er.near != null)
			getVars(true, er.near, vt, vb, vb2);
	}

	static void dpp(Hashtable dp, Euler er) {
		if (er.cverb.length() > 0 && er.cverb.charAt(0) != '?' && !er.cverb.equals("=") && !er.cverb.equals("=>") && !er.cverb.equals("!")
				&& !er.cverb.startsWith("log:") && !er.cverb.startsWith("math:") && !er.cverb.startsWith("list:")
				&& !er.cverb.startsWith("str:") && !er.cverb.startsWith("fn:") && !er.cverb.startsWith("time:") && !er.cverb.startsWith("e:")
				&& !er.cverb.equals("rdf:first") && !er.cverb.equals("rdf:rest") && !er.cverb.equals("fl:pi")
				|| er.cverb.equals("list:notIn") || er.cverb.equals("list:subListOf") || er.cverb.equals("list:hasLenght")
				|| er.cverb.equals("e:columns") || er.cverb.equals("e:depends") || er.cverb.equals("e:bayesian")
				|| er.cverb.equals("e:boolean") || er.cverb.equals("e:conditional")
				|| er.cverb.equals("e:possibleModel") || er.cverb.equals("e:falseModel") || er.cverb.equals("e:counterModel")
				|| er.cverb.equals("e:because") || er.cverb.equals("e:integrityConstraint") || er.cverb.equals("e:selected")
				|| er.cverb.equals("e:triple") || er.cverb.equals("e:ancestors") || er.cverb.equals("e:decendents")
				|| er.cverb.equals("e:falseAncestors") || er.cverb.equals("e:falseDecendents") || er.cverb.equals("e:consistentGives"))
			dp.put(er.toPrologString(er.cverb), new Object());
		if (er.verb == Euler.Eoptional) {
			for (Euler el = er.obj; el != null; el = el.near) dpp(dp, el);
		}
	}

	static void bnp(Euler el) {
		if (el.subj != null) {
			if (el.verb.equals(Euler.LOGimplies)) {
				for (Euler ej = el.subj; ej != null; ej = ej.near) bnp(ej);
			}
			else bnp(el.subj);
		}
		if (el.cverb.startsWith("_:"))
			el.cverb = "?P" + el.cverb.substring(2);
		if (el.obj != null)
			bnp(el.obj);
	}

	static void bnc(Euler el) {
		if (el.subj != null) {
			if (el.verb.equals(Euler.LOGimplies)) {
				for (Euler ej = el.subj; ej != null; ej = ej.near) bnc(ej);
			}
			else bnc(el.subj);
		}
		if (el.cverb.startsWith("_:"))
			el.cverb = "?C" + el.cverb.substring(2);
		if (el.obj != null)
			bnc(el.obj);
	}

	static String sfg(Euler ev, Euler er) {
		StringBuffer sb = new StringBuffer();
		Vector wt = new Vector();
		ev.getX(true, wt);
		if (er.subj != null && er.subj.cverb != null && er.subj.cverb.startsWith("_:")) {
			sb.append("?C").append(er.subj.cverb.substring(2)).append(" e:tuple (");
			for (Enumeration e = wt.elements(); e.hasMoreElements();) {
				String ne = (String) e.nextElement();
				if (ne.startsWith("?"))
					sb.append(ne).append(' ');
			}
			sb.append("). ");
		}
		if (er.obj != null && er.obj.cverb != null && er.obj.cverb.startsWith("_:")) {
			sb.append("?C").append(er.obj.cverb.substring(2)).append(" e:tuple (");
			for (Enumeration e = wt.elements(); e.hasMoreElements();) {
				String ne = (String) e.nextElement();
				if (ne.startsWith("?"))
					sb.append(ne).append(' ');
			}
			sb.append("). ");
		}
		return (sb.toString());
	}
}