// $Id: Euler.cs,v 1.255 2005/03/06 19:47:08 amdus Exp $
// PxButton | build | \WINDOWS\Microsoft.NET\Framework\v1.1.4322\csc /debug /o /doc:Euler.xml *.cs |

using System;
using System.Collections;
using System.IO;
using System.Globalization;
using System.Net.Sockets;
using System.Text;

/// <summary>Euler proof mechanism</summary>
/// <author>Jos De Roo</author>

public class Euler {
  internal Euler subj = null;                   // RDF subject
  internal String verb = null;                  // RDF predicate as absoluteized verb
  internal Euler obj = null;                    // RDF object
  internal String cverb = null;                 // compact verb
  internal int varid = - 1;                     // variable id
  internal bool bound = false;                  // variable binding state
  internal bool vv = false;                     // variable verb state
  internal Euler refr = null;                   // to be dereferenced
  internal Euler premis = null;                 // to attach the premis
  internal Euler near = null;                   // to construct a conjunction
  internal Euler far;                           // to remember last clause
  internal long uid = 0;                        // unique id
  internal String src = null;                   // triple source
  internal int line  = -1;                      // triple source line
  internal EulerExt ext = null;                 // extensions
  
  internal const String E = "<http://eulersharp.sourceforge.net/2003/03swap/log-rules";
  internal const String EclashesWith = "<http://eulersharp.sourceforge.net/2003/03swap/log-rules#clashesWith>";
  internal const String Eevidence = "<http://eulersharp.sourceforge.net/2003/03swap/log-rules#evidence>";
  internal const String Ekb = "<http://eulersharp.sourceforge.net/2003/03swap/log-rules#kb>";
  internal const String Etrace = "trace";
  internal const String LOG = "<http://www.w3.org/2000/10/swap/log";
  internal const String LOGTruth = "<http://www.w3.org/2000/10/swap/log#Truth>";
  internal const String LOGconjunction = "<http://www.w3.org/2000/10/swap/log#conjunction>";
  internal const String LOGdefinitiveDocument = "<http://www.w3.org/2000/10/swap/log#definitiveDocument>";
  internal const String LOGdefinitiveService = "<http://www.w3.org/2000/10/swap/log#definitiveService>";
  internal const String LOGequalTo = "<http://www.w3.org/2000/10/swap/log#equalTo>";
  internal const String LOGforAll = "<http://www.w3.org/2000/10/swap/log#forAll>";
  internal const String LOGforSome = "<http://www.w3.org/2000/10/swap/log#forSome>";
  internal const String LOGimplies = "<http://www.w3.org/2000/10/swap/log#implies>";
  internal const String LOGincludes = "<http://www.w3.org/2000/10/swap/log#includes>";
  internal const String LOGkb = "<http://www.w3.org/2000/10/swap/log#kb>";
  internal const String LOGnotEqualTo = "<http://www.w3.org/2000/10/swap/log#notEqualTo>";
  internal const String LOGnotImplies = "<http://www.w3.org/2000/10/swap/log#notImplies>";
  internal const String LOGnotIncludes = "<http://www.w3.org/2000/10/swap/log#notIncludes>";
  internal const String LOGracine = "<http://www.w3.org/2000/10/swap/log#racine>";
  internal const String LOGsemantics = "<http://www.w3.org/2000/10/swap/log#semantics>";
  internal const String MATH = "<http://www.w3.org/2000/10/swap/math";
  internal const String MATHabsoluteValue = "<http://www.w3.org/2000/10/swap/math#absoluteValue>";
  internal const String MATHatan2 = "<http://www.w3.org/2000/10/swap/math#atan2>";
  internal const String MATHcos = "<http://www.w3.org/2000/10/swap/math#cos>";
  internal const String MATHcosh = "<http://www.w3.org/2000/10/swap/math#cosh>";
  internal const String MATHdegrees = "<http://www.w3.org/2000/10/swap/math#degrees>";
  internal const String MATHdifference = "<http://www.w3.org/2000/10/swap/math#difference>";
  internal const String MATHequalTo = "<http://www.w3.org/2000/10/swap/math#equalTo>";
  internal const String MATHexponentiation = "<http://www.w3.org/2000/10/swap/math#exponentiation>";
  internal const String MATHgreaterThan = "<http://www.w3.org/2000/10/swap/math#greaterThan>";
  internal const String MATHintegerQuotient = "<http://www.w3.org/2000/10/swap/math#integerQuotient>";
  internal const String MATHkb = "<http://www.w3.org/2000/10/swap/math#kb>";
  internal const String MATHlessThan = "<http://www.w3.org/2000/10/swap/math#lessThan>";
  internal const String MATHmemberCount = "<http://www.w3.org/2000/10/swap/math#memberCount>";
  internal const String MATHnegation = "<http://www.w3.org/2000/10/swap/math#negation>";
  internal const String MATHnotEqualTo = "<http://www.w3.org/2000/10/swap/math#notEqualTo>";
  internal const String MATHnotGreaterThan = "<http://www.w3.org/2000/10/swap/math#notGreaterThan>";
  internal const String MATHnotLessThan = "<http://www.w3.org/2000/10/swap/math#notLessThan>";
  internal const String MATHproduct = "<http://www.w3.org/2000/10/swap/math#product>";
  internal const String MATHproofCount = "<http://www.w3.org/2000/10/swap/math#proofCount>";
  internal const String MATHquotient = "<http://www.w3.org/2000/10/swap/math#quotient>";
  internal const String MATHremainder = "<http://www.w3.org/2000/10/swap/math#remainder>";
  internal const String MATHrounded = "<http://www.w3.org/2000/10/swap/math#rounded>";
  internal const String MATHsin = "<http://www.w3.org/2000/10/swap/math#sin>";
  internal const String MATHsinh = "<http://www.w3.org/2000/10/swap/math#sinh>";
  internal const String MATHsum = "<http://www.w3.org/2000/10/swap/math#sum>";
  internal const String MATHtan = "<http://www.w3.org/2000/10/swap/math#tan>";
  internal const String MATHtanh = "<http://www.w3.org/2000/10/swap/math#tanh>";
  internal const String OWL = "<http://www.w3.org/2002/07/owl";
  internal const String OWLClass = "<http://www.w3.org/2002/07/owl#Class>";
  internal const String OWLFunctionalProperty = "<http://www.w3.org/2002/07/owl#FunctionalProperty>";
  internal const String OWLInverseFunctionalProperty = "<http://www.w3.org/2002/07/owl#InverseFunctionalProperty>";
  internal const String OWLRestriction = "<http://www.w3.org/2002/07/owl#Restriction>";
  internal const String OWLSymmetricProperty = "<http://www.w3.org/2002/07/owl#SymmetricProperty>";
  internal const String OWLTransitiveProperty = "<http://www.w3.org/2002/07/owl#TransitiveProperty>";
  internal const String OWLThing = "<http://www.w3.org/2002/07/owl#Thing>";
  internal const String OWLallValuesFrom = "<http://www.w3.org/2002/07/owl#allValuesFrom>";
  internal const String OWLcardinality = "<http://www.w3.org/2002/07/owl#cardinality>";
  internal const String OWLcomplementOf = "<http://www.w3.org/2002/07/owl#complementOf>";
  internal const String OWLdifferentFrom = "<http://www.w3.org/2002/07/owl#differentFrom>";
  internal const String OWLequivalentClass = "<http://www.w3.org/2002/07/owl#equivalentClass>";
  internal const String OWLequivalentProperty = "<http://www.w3.org/2002/07/owl#equivalentProperty>";
  internal const String OWLhasValue = "<http://www.w3.org/2002/07/owl#hasValue>";
  internal const String OWLintersectionOf = "<http://www.w3.org/2002/07/owl#intersectionOf>";
  internal const String OWLinverseOf = "<http://www.w3.org/2002/07/owl#inverseOf>";
  internal const String OWLkb = "<http://www.w3.org/2002/07/owl#kb>";
  internal const String OWLmaxCardinality = "<http://www.w3.org/2002/07/owl#maxCardinality>";
  internal const String OWLminCardinality = "<http://www.w3.org/2002/07/owl#minCardinality>";
  internal const String OWLonProperty = "<http://www.w3.org/2002/07/owl#onProperty>";
  internal const String OWLoneOf = "<http://www.w3.org/2002/07/owl#oneOf>";
  internal const String OWLsameAs = "<http://www.w3.org/2002/07/owl#sameAs>";
  internal const String OWLsomeValuesFrom = "<http://www.w3.org/2002/07/owl#someValuesFrom>";
  internal const String OWLunionOf = "<http://www.w3.org/2002/07/owl#unionOf>";
  internal const String Q = "<http://www.w3.org/2004/ql";
  internal const String Qselect = "<http://www.w3.org/2004/ql#select>";
  internal const String Qsource = "<http://www.w3.org/2004/ql#source>";
  internal const String Qwhere = "<http://www.w3.org/2004/ql#where>";
  internal const String RDF = "<http://www.w3.org/1999/02/22-rdf-syntax-ns";
  internal const String RDFD = "<http://www.w3.org/2000/10/rdf-tests/rdfcore/datatypes";
  internal const String RDFList = "<http://www.w3.org/1999/02/22-rdf-syntax-ns#List>";
  internal const String RDFProperty = "<http://www.w3.org/1999/02/22-rdf-syntax-ns#Property>";
  internal const String RDFS = "<http://www.w3.org/2000/01/rdf-schema";
  internal const String RDFSClass = "<http://www.w3.org/2000/01/rdf-schema#Class>";
  internal const String RDFSContainerMembershipProperty = "<http://www.w3.org/2000/01/rdf-schema#ContainerMembershipProperty>";
  internal const String RDFSDatatype = "<http://www.w3.org/2000/01/rdf-schema#Datatype>";
  internal const String RDFSLiteral = "<http://www.w3.org/2000/01/rdf-schema#Literal>";
  internal const String RDFSResource = "<http://www.w3.org/2000/01/rdf-schema#Resource>";
  internal const String RDFSdomain = "<http://www.w3.org/2000/01/rdf-schema#domain>";
  internal const String RDFSmember = "<http://www.w3.org/2000/01/rdf-schema#member>";
  internal const String RDFSrange = "<http://www.w3.org/2000/01/rdf-schema#range>";
  internal const String RDFSsubClassOf = "<http://www.w3.org/2000/01/rdf-schema#subClassOf>";
  internal const String RDFSsubPropertyOf = "<http://www.w3.org/2000/01/rdf-schema#subPropertyOf>";
  internal const String RDFfirst = "<http://www.w3.org/1999/02/22-rdf-syntax-ns#first>";
  internal const String RDFnil = "<http://www.w3.org/1999/02/22-rdf-syntax-ns#nil>";
  internal const String RDFrest = "<http://www.w3.org/1999/02/22-rdf-syntax-ns#rest>";
  internal const String RDFtype = "<http://www.w3.org/1999/02/22-rdf-syntax-ns#type>";
  internal const String RDFXMLLiteral = "<http://www.w3.org/1999/02/22-rdf-syntax-ns#XMLLiteral>";
  internal const String STR = "<http://www.w3.org/2000/10/swap/string";
  internal const String STRconcatenation = "<http://www.w3.org/2000/10/swap/string#concatenation>";
  internal const String STRcontains = "<http://www.w3.org/2000/10/swap/string#contains>";
  internal const String STRcontainsIgnoringCase = "<http://www.w3.org/2000/10/swap/string#containsIgnoringCase>";
  internal const String STRendsWith = "<http://www.w3.org/2000/10/swap/string#endsWith>";
  internal const String STRequalIgnoringCase = "<http://www.w3.org/2000/10/swap/string#equalIgnoringCase>";
  internal const String STRgreaterThan = "<http://www.w3.org/2000/10/swap/string#greaterThan>";
  internal const String STRkb = "<http://www.w3.org/2000/10/swap/string#kb>";
  internal const String STRlessThan = "<http://www.w3.org/2000/10/swap/string#lessThan>";
  internal const String STRmatches = "<http://www.w3.org/2000/10/swap/string#matches>";
  internal const String STRnotEqualIgnoringCase = "<http://www.w3.org/2000/10/swap/string#notEqualIgnoringCase>";
  internal const String STRnotGreaterThan = "<http://www.w3.org/2000/10/swap/string#notGreaterThan>";
  internal const String STRnotLessThan = "<http://www.w3.org/2000/10/swap/string#notLessThan>";
  internal const String STRnotMatches = "<http://www.w3.org/2000/10/swap/string#notMatches>";
  internal const String STRstartsWith = "<http://www.w3.org/2000/10/swap/string#startsWith>";
  internal const String W3 = "<http://www.w3.org/";
  internal const String XSD = "<http://www.w3.org/2001/XMLSchema";
  internal const String XSDID = "<http://www.w3.org/2001/XMLSchema#ID>";
  internal const String XSDIDREF = "<http://www.w3.org/2001/XMLSchema#IDREF>";
  internal const String XSDNCName = "<http://www.w3.org/2001/XMLSchema#NCName>";
  internal const String XSDNMTOKEN = "<http://www.w3.org/2001/XMLSchema#NMTOKEN>";
  internal const String XSDName = "<http://www.w3.org/2001/XMLSchema#Name>";
  internal const String XSDanyURI = "<http://www.w3.org/2001/XMLSchema#anyURI>";
  internal const String XSDbase64Binary = "<http://www.w3.org/2001/XMLSchema#base64Binary>";
  internal const String XSDboolean = "<http://www.w3.org/2001/XMLSchema#boolean>";
  internal const String XSDbyte = "<http://www.w3.org/2001/XMLSchema#byte>";
  internal const String XSDdate = "<http://www.w3.org/2001/XMLSchema#date>";
  internal const String XSDdateTime = "<http://www.w3.org/2001/XMLSchema#dateTime>";
  internal const String XSDdecimal = "<http://www.w3.org/2001/XMLSchema#decimal>";
  internal const String XSDdouble = "<http://www.w3.org/2001/XMLSchema#double>";
  internal const String XSDduration = "<http://www.w3.org/2001/XMLSchema#duration>";
  internal const String XSDfloat = "<http://www.w3.org/2001/XMLSchema#float>";
  internal const String XSDgDay = "<http://www.w3.org/2001/XMLSchema#gDay>";
  internal const String XSDgMonth = "<http://www.w3.org/2001/XMLSchema#gMonth>";
  internal const String XSDgMonthDay = "<http://www.w3.org/2001/XMLSchema#gMonthDay>";
  internal const String XSDgYear = "<http://www.w3.org/2001/XMLSchema#gYear>";
  internal const String XSDgYearMonth = "<http://www.w3.org/2001/XMLSchema#gYearMonth>";
  internal const String XSDhexBinary = "<http://www.w3.org/2001/XMLSchema#hexBinary>";
  internal const String XSDint = "<http://www.w3.org/2001/XMLSchema#int>";
  internal const String XSDinteger = "<http://www.w3.org/2001/XMLSchema#integer>";
  internal const String XSDlanguage = "<http://www.w3.org/2001/XMLSchema#language>";
  internal const String XSDlong = "<http://www.w3.org/2001/XMLSchema#long>";
  internal const String XSDnegativeInteger = "<http://www.w3.org/2001/XMLSchema#negativeInteger>";
  internal const String XSDnonNegativeInteger = "<http://www.w3.org/2001/XMLSchema#nonNegativeInteger>";
  internal const String XSDnonPositiveInteger = "<http://www.w3.org/2001/XMLSchema#nonPositiveInteger>";
  internal const String XSDnormalizedString = "<http://www.w3.org/2001/XMLSchema#normalizedString>";
  internal const String XSDpositiveInteger = "<http://www.w3.org/2001/XMLSchema#positiveInteger>";
  internal const String XSDshort = "<http://www.w3.org/2001/XMLSchema#short>";
  internal const String XSDstring = "<http://www.w3.org/2001/XMLSchema#string>";
  internal const String XSDtime = "<http://www.w3.org/2001/XMLSchema#time>";
  internal const String XSDtoken = "<http://www.w3.org/2001/XMLSchema#token>";
  internal const String XSDunsignedByte = "<http://www.w3.org/2001/XMLSchema#unsignedByte>";
  internal const String XSDunsignedInt = "<http://www.w3.org/2001/XMLSchema#unsignedInt>";
  internal const String XSDunsignedLong = "<http://www.w3.org/2001/XMLSchema#unsignedLong>";
  internal const String XSDunsignedShort = "<http://www.w3.org/2001/XMLSchema#unsignedShort>";
  internal const String Xrcsid = "#rcsid";

  internal static long step = 1;
  internal static long doc = 1;
  internal static ArrayList docv = new ArrayList();
  internal static Hashtable conc = null;
  internal static Euler root = null;
  internal static long uidc = 1;
  internal static long triple = 0;

  /// <summary>constructs a proof engine</summary>

  public Euler() {
    far = this;
    uid = uidc++;
  }
  
  /// <summary>loads all facts and rules acquired from the RDF URI in that proof engine</summary>
  /// <param name="uri">of the RDF resource</param>

  public virtual void Load(String uri) {
    lock(this) {
      root = this;
      if (ext == null) ext = new EulerExt();
      if (ext.loaded == null) ext.loaded = new ArrayList();
      if (ext.loaded.Contains('<' + uri + '>')) return;
      String rk = fromWeb(uri);
      String u = ext.baseURI;
      if (!uri.StartsWith("data:")) ext.loaded.Add('<' + ext.baseURI + '>');
      if (!docv.Contains(ext.baseURI)) docv.Add(ext.baseURI);
      doc = docv.IndexOf(ext.baseURI);
      ArrayList vt = new ArrayList();
      Parser np = new Parser(rk, vt, this, u);
      StringBuilder gen = new StringBuilder("data:,");
      if (Outputter.log) Outputter.GetInstance().Log("Euler", "Load", "engine" + uid + " load " + uri, Outputter.LOGLEVEL.FINE);
      while (true) {
        far.near = np.Parse();
        if (far.near == null) break;
        while (far.near != null && far.near.verb != null) {
          if (far.near.verb.Equals(LOGforAll)) {
            if (far.near.subj.subj == null && far.near.subj.obj == null) {
              if (!vt.Contains(far.near.obj.verb)) vt.Add(far.near.obj.verb);
              far.near = far.near.near;
              continue;
            }
            else {
              Euler fn = far.near;
              ArrayList wt = new ArrayList();
              for (IEnumerator e = vt.GetEnumerator(); e.MoveNext(); wt.Add(e.Current));
              while (fn != null && fn.verb.Equals(LOGforAll)) {
                if (!wt.Contains(fn.obj.verb)) wt.Add(fn.obj.verb);
                fn = fn.near;
              }
              if (wt.Count > ext.varmax) ext.varmax = wt.Count;
              far.near.subj.near = fn;
              far.near = far.near.subj;
              far.near.forX(false, wt);
            }
          }
          far.near.forX(false, vt);
          rewrite(true, far.near, np);
          if (uid != -1 && far.near.verb.Equals(Qselect) && far.near.near.verb.Equals(Qwhere)) {
            far.near.obj.src = far.near.subj.verb;
            far.near.subj = far.near.near.obj;
            far.near.verb = LOGimplies;
            far.near.cverb = "=>";
            far.near.near = far.near.near.near;
          }
          if (far.near.verb.Equals(LOGimplies) && far.near.subj.cverb.Equals("{}")) far.near = far.near.obj;
          else if (far.near.verb.Equals(LOGimplies) || far.near.verb.Equals(LOGnotImplies)) {
            Euler fn = far.near.subj;
            while (fn != null) {
              if (fn.verb.Equals(LOGincludes) && fn.ToString().LastIndexOf('?') > fn.ToString().IndexOf("includes") &&
                  !far.near.subj.verb.Equals(LOGdefinitiveDocument) && !far.near.subj.verb.Equals(LOGdefinitiveService)) {
                rewrite(false,fn.obj, np);
                Euler oe = far.near.subj;
                far.near.subj = fn.obj.copy();
                Euler ne = far.near.subj;
                while (ne.near != null) ne = ne.near;
                ne.near = oe;
              }
              else if (fn.subj.subj != null && fn.verb != "vv" && fn.subj.verb != "^^") rewrite(true, fn.subj, np);
              else if (fn.obj.subj != null && fn.verb != "vv" && fn.obj.verb != "^^") rewrite(true, fn.obj, np);
              fn = fn.near;
            }
	    reorderPremis(far.near);
            rewrite(false, far.near.subj, np);
            far.near.obj.premis = far.near.subj;
            fn = far.near;
            while (fn.obj.near != null) {
              fn.near = np.parse(false, far.near.cverb);
              fn.near.subj = fn.subj;
              fn.near.obj = fn.obj.near;
              fn = fn.near;
            }
            fn = far.near.copy();
            fn.near = fn.subj;
            fn.subj = fn.obj;
            fn.obj = fn.near;
            far.near.obj.near = null;
          }
          else if (far.near.verb.Equals(OWLequivalentClass))
            gen.Append(far.near.subj).Append(' ').Append(RDFSsubClassOf).Append(' ').Append(far.near.obj).Append(". ")
               .Append(far.near.obj).Append(' ').Append(RDFSsubClassOf).Append(' ').Append(far.near.subj).Append(". ");
          else if (far.near.verb.Equals(OWLequivalentProperty))
            gen.Append(far.near.subj).Append(' ').Append(RDFSsubPropertyOf).Append(' ').Append(far.near.obj).Append(". ")
               .Append(far.near.obj).Append(' ').Append(RDFSsubPropertyOf).Append(' ').Append(far.near.subj).Append(". ");
          else if (far.near.verb.StartsWith(RDF + "#_"))
            gen.Append(far.near.verb).Append(' ').Append(RDFSsubPropertyOf).Append(' ').Append(RDFSmember).Append(". ");
          else if (far.near.verb.Equals(RDFtype) && far.near.obj.verb.Equals(RDFSClass))
            ext.ocl[far.near.subj.verb] = this;
          else if (far.near.verb.Equals(RDFtype) && far.near.obj.verb.Equals(OWLClass))
            ext.ocl[far.near.subj.verb] = this;
          else if (far.near.verb.Equals(LOGdefinitiveDocument) || far.near.verb.Equals(LOGdefinitiveService))
            ext.dds[far.near.subj.verb] = far.near.obj.verb;
          if (Outputter.log) Outputter.GetInstance().Log("Euler", "Load", "engine" + uid + " assert " + far.near, Outputter.LOGLEVEL.FINE);
          far = far.near;
          if (!ext.baseURI.StartsWith("_:")) triple++;
        }
      }
      String gener = gen.ToString();
      String ob = ext.baseURI;
      if (!ext.se && !gener.Equals("data:,")) Load(gener);
      ext.baseURI = ob;
      if (vt.Count > ext.varmax) ext.varmax = vt.Count;
    }
  }
  
  /// <summary>prepares that proof engine</summary>
  public virtual void Prepare() {
    lock(this) {
      bool ot = Configuration.GetInstance().Think;
      long os = step;
      long op = triple;
      long om = Configuration.GetInstance().Steps;
      if (Configuration.GetInstance().Steps != -1) Configuration.GetInstance().Steps = Configuration.GetInstance().Steps/20;
      Configuration.GetInstance().Think = true;
      if (Outputter.log) Outputter.GetInstance().Log("Euler", "Prepare", "engine" + uid + " prepare " + ext.baseURI, Outputter.LOGLEVEL.FINE);
      Proof("data:,?S " + OWLsameAs + " ?O. ");
      Configuration.GetInstance().Steps = om;
      triple = op;
      step = os;
      Configuration.GetInstance().Think = ot;
      syno(this);
    }
  }

  /// <summary>proofs a conjunction with that proof engine</summary>
  /// <param name="uri">of the RDF resource</param>
  /// <returns>proof</returns>

  public virtual String Proof(String uri) {
    lock(this) {
      root = this;
      if (ext == null) ext = new EulerExt();
      if (ext.loaded == null) ext.loaded = new ArrayList();
      String cj = fromWeb(uri);
      String u = ext.baseURI;
      ArrayList vt = new ArrayList();
      Parser np = new Parser(cj, vt, this, u);
      StringBuilder gen = new StringBuilder("data:,");
      Euler goal = new Euler();
      Euler g = goal;
      if (Outputter.log) Outputter.GetInstance().Log("Euler", "Proof", "engine" + uid + " proof " + uri, Outputter.LOGLEVEL.FINE);
      while (true) 
      {
        g.near = np.Parse();
        if (g.near == null) break;
        while (g.near != null && g.near.verb != null) {
          rewrite(true, g.near, np);
          if (g.near.subj.subj != null && g.near.verb != "vv" && g.near.subj.verb != "^^") rewrite(true, g.near.subj, np);
          if (g.near.obj.subj != null && g.near.verb != "vv" && g.near.obj.verb != "^^") rewrite(true, g.near.obj, np);
          if (g.near.verb.Equals(LOGimplies) && g.near.subj.cverb.Equals("{}")) g.near = g.near.obj;
          if (g.near.verb.Equals(Eevidence)) g.near = g.near.subj;
          if (g.near.verb.Equals(LOGforSome) || g.near.verb.Equals(LOGforAll) || g.near.obj.verb != null && g.near.obj.verb.Equals(LOGTruth)) {
            if (g.near.subj.subj == null && g.near.subj.obj == null) {
              if (g.near.obj != null && !vt.Contains(g.near.obj.verb)) vt.Add(g.near.obj.verb);
              g.near = g.near.near;
              continue;
            }
            else {
              Euler fn = g.near;
              ArrayList wt = new ArrayList();
              for (IEnumerator e = vt.GetEnumerator(); e.MoveNext(); wt.Add(e.Current));
              while (fn != null && (fn.verb.Equals(LOGforSome) || fn.verb.Equals(LOGforAll) || fn.obj.verb.Equals(LOGTruth))) {
                if ((fn.verb.Equals(LOGforSome) || fn.verb.Equals(LOGforAll)) && !wt.Contains(fn.obj.verb))
                  wt.Add(fn.obj.verb);
                fn = fn.near;
              }
              if (wt.Count > ext.varmax) ext.varmax = wt.Count;
              g.near = g.near.subj;
              Euler gn = g;
              while (gn.near != null) {
                gn.near.forX(false, wt);
                gn = gn.near;
              }
              gn.near = fn;
            }
            g = g.near;
          }
          else if (g.near.verb.EndsWith(Xrcsid + '>')) {
            g.near = g.near.near;
            continue;
          }
          else {
            g.near.getX(false, vt);
            g.near.forX(false, vt);
            if (vt.Count > ext.varmax) ext.varmax = vt.Count;
            if (Outputter.log) Outputter.GetInstance().Log("Euler", "Proof", "engine" + uid + " query " + g.near, Outputter.LOGLEVEL.FINE);
            g = g.near;
          }
          if (g.subj.varid != -1 &&  // @@ comprehension
              (g.verb.Equals(RDFtype) && g.obj.verb.Equals(RDFList) ||
               g.verb.Equals(RDFfirst) ||
               g.verb.Equals(RDFrest) ||
               g.verb.Equals(RDFtype) && g.obj.verb.Equals(OWLClass) ||
               g.verb.Equals(OWLintersectionOf) ||
               g.verb.Equals(OWLunionOf) ||
               g.verb.Equals(OWLcomplementOf) && (g.obj.varid != -1 || ext.ocl[g.obj.verb] != null) ||
               g.verb.Equals(OWLoneOf) ||
               g.verb.Equals(RDFtype) && g.obj.verb.Equals(OWLRestriction) ||
               g.verb.Equals(OWLonProperty) ||
               g.verb.Equals(OWLallValuesFrom) ||
               g.verb.Equals(OWLsomeValuesFrom) ||
               g.verb.Equals(OWLhasValue) ||
               g.verb.Equals(OWLminCardinality) ||
               g.verb.Equals(OWLmaxCardinality) ||
               g.verb.Equals(OWLcardinality))) {
            if (g.verb.Equals(RDFtype)) g.vv = true;
            gen.Append(g);
          }
        }
      }
      if (goal.near == null) goal.near = np.parse(false, "{}");
      if (Configuration.GetInstance().ProofExplanation) reorder(goal);
      syno(goal);
      String gener = gen.ToString();
      String ob = ext.baseURI;
      if (!ext.se && !gener.Equals("data:,")) Load(gener);
      ext.baseURI = ob;
      if (vt.Count > ext.varmax) ext.varmax = vt.Count;
      StringBuilder nsp = new StringBuilder(256);
      IEnumerator en = (IEnumerator) ext.ns.Keys.GetEnumerator();
      while (en.MoveNext()) {
        Object nsx = en.Current;
        nsp.Append("@prefix ").Append(nsx).Append(' ').Append(ext.ns[nsx]).Append(".\n");
      }
      nsp.Append('\n');
      int tab = 0;
      Euler[] vars = new Euler[ext.varmax];
      Euler lr = goal.near;
      Euler ts = null;
      Euler tsb = null;
      Euler ts1 = null;
      Euler ts2 = null;
      Stack stack = new Stack();
      bool not = false;
      long istep = step;
      long iuidc = uidc;
      StringBuilder proof = new StringBuilder(4096);
      int pn = 0;
      if (!(ext.baseURI.StartsWith("file:") && ext.baseURI.EndsWith("test.n3"))) {
        proof.Append("# Generated with http://www.agfa.com/w3c/euler/ version ").Append(Configuration.GetInstance().Version);
        proof.Append(" on ").Append(DateTime.UtcNow.ToString()).Append("\n");
        if (Configuration.GetInstance().ProofExplanation) {
          proof.Append("@prefix log: <http://www.w3.org/2000/10/swap/log#>.\n\n(");
          IEnumerator enu = (IEnumerator) ext.loaded.GetEnumerator();
          while (enu.MoveNext()) {
            if (proof[proof.Length - 1] != '(') proof.Append("\n ");
            proof.Append(enu.Current).Append("!log:semantics");
          }
          proof.Append(")!log:conjunction =>\n{\n");
          pn = proof.Length;
        }
        proof.Append(nsp);
      }
      int pns = proof.Length;
      proof.EnsureCapacity(proof.Length * 2);
      StringBuilder pp = new StringBuilder(4096);
      StringBuilder pc = new StringBuilder(4096);
      Hashtable pct = new Hashtable();
      Euler te = goal;
      while (te.near != null) {
        te.near = te.near.eval(false, vars, stack);
        te = te.near;
      }
      goal = goal.near;
      if (Outputter.log) Outputter.GetInstance().Log("Euler", "Proof", "engine" + uid + " [" + step + "]CALL: " + goal, Outputter.LOGLEVEL.FINER);
      long t = DateTime.Now.Ticks;
      while (true) {
        if (goal == null) {
          t = DateTime.Now.Ticks - t;
          if (!(ext.baseURI.StartsWith("file:") && ext.baseURI.EndsWith("test.n3"))) {
            if (proof.Length == pns) {
              if (Configuration.GetInstance().ProofExplanation) proof.Length = pn;
              proof.Append("# No proof found for ");
            }
            else proof.Append("# Proof found for ");
            proof.Append(u);
            proof.Append(" in ").Append(step-istep).Append(step-istep==1?" step":" steps");
            proof.Append(" (").Append((long)((step-istep)*10000000L/(t+100))).Append(" steps/sec)"); // @@ 100ns
            proof.Append(" using ").Append(ext.engine).Append(ext.engine==1?" engine":" engines");
            proof.Append(" (").Append(triple).Append(triple==1?" triple)":" triples)");
            if (!ext.baseURI.StartsWith("_:")) triple = 0;
            if (Configuration.GetInstance().ProofExplanation) proof.Append("\n}.\n");
          }
          conc = pct;
          return proof.ToString();
        }
        not = false;
        try {
          if (goal.varid != - 1 && goal.subj != null && goal.obj != null) {
            Euler gn = goal.eval(false, vars, stack);
            goal.verb = gn.verb;
            goal.cverb = gn.cverb;
          }
          if (goal.verb == null && goal.obj.subj == null) {
            if (goal.obj.verb == OWLsameAs) synon(goal.obj);
            tab--;
            if (pp[pp.Length - 2] == '.' && pp[pp.Length - 1] == ' ') pp[pp.Length - 2] = '}';
            else pp.Append("} ");
            pp.Append("=> {\n");
            for (int i = tab; i > 0; i--) pp.Append(' ');
            pp.Append(goal.obj).Append(" e:evidence ").Append(goal.obj.src).Append("}. ");
            if (tab == 0) {
              if (pct[goal.obj.ToString()+'\n'] == null) pc.Append(goal.obj).Append('\n');
              else not = true;
            }
          }
          else if (goal.verb == null && goal.obj.subj.deref().bound && goal.obj.obj.deref().bound) {
            if (goal.obj.verb == OWLsameAs) synon(goal.obj);
            tab--;
            if (pp[pp.Length - 2] == '.' && pp[pp.Length - 1] == ' ') pp[pp.Length - 2] = '}';
            else pp.Append("} ");
            pp.Append("=> {\n");
            for (int i = tab; i > 0; i--) pp.Append(' ');
            pp.Append("{").Append(goal.obj).Insert(pp.Length - 2, "} e:evidence ").Insert(pp.Length - 2, goal.obj.src);
            if (pp[pp.Length - 2] == '.' && pp[pp.Length - 1] == ' ') pp.Insert(pp.Length - 2, '}');
            else pp.Append("}. ");
            if (tab == 0) {
              if (pct[goal.obj.ToString()+'\n'] == null) pc.Append(goal.obj).Append('\n');
              else not = true;
            }
          }
          else if (goal.verb == "" && goal.subj.deref().bound && goal.subj.deref().getFirst() == null) {  // @@ single
            pp.Append('\n');
            for (int i = tab; i > 0; i--) pp.Append(' ');
            pp.Append(getLit(goal.subj)).Append(". ");
          }
          else if (goal.verb == Etrace) Console.Error.WriteLine("[" + step + "] " + goal);
          else if (!ext.se && goal.verb != null && BuiltinManager.GetInstance().IsBuiltin(goal.verb)) {
            not = BuiltinManager.GetInstance().ApplyBuiltin(this, goal, stack, tab, pp, pc);
          }
          else if ((goal.verb == RDFSsubClassOf || goal.verb == RDFSsubPropertyOf ||
                    goal.verb == OWLequivalentClass || goal.verb == OWLequivalentProperty ||
                    goal.verb == OWLsameAs) &&
                   goal.subj.deref().verb == goal.obj.deref().verb &&
                   goal.subj.deref().obj == null && goal.obj.deref().obj == null &&
                   (goal.subj.deref().bound || goal.verb != OWLsameAs && goal.subj.deref().verb.StartsWith("_:")) &&
                   (goal.obj.deref().bound || goal.verb != OWLsameAs && goal.obj.deref().verb.StartsWith("_:"))) {
            pp.Append('\n');
            for (int i = tab; i > 0; i--) pp.Append(' ');
            pp.Append('{').Append(goal).Insert(pp.Length - 2, "} e:evidence ").Insert(pp.Length - 2, OWLkb);
            if (tab == 0) pc.Append(goal).Append('\n');
          }
          else if (!ext.se && goal.verb != null && goal.verb == RDFtype &&
                   (goal.obj.deref().verb == RDFSResource ||
                    goal.obj.deref().verb == OWLThing ||
                    goal.obj.deref().verb == RDFSContainerMembershipProperty
                      && goal.subj.deref().verb.StartsWith(RDF + "#_") ||
                    goal.obj.deref().verb == RDFSLiteral
                      && (goal.subj.deref().verb.StartsWith("\"") ||
                          goal.subj.deref().verb == "^^" && goal.subj.deref().subj.deref().verb.StartsWith("\"") && !Datatype.Clash(goal.subj.deref().obj.verb, goal.subj.deref().subj.verb) ||
                          goal.subj.deref().isNumeral()) ||
                    goal.obj.deref().verb == XSDstring
                      && goal.subj.deref().verb.StartsWith("\"")
                      && goal.subj.deref().verb.EndsWith("\"") ||
                    goal.subj.deref().verb == "^^"
                      && goal.subj.deref().obj.verb == goal.obj.deref().verb
                      && !Datatype.Clash(goal.subj.deref().obj.verb, goal.subj.deref().subj.verb))) {
            pp.Append('\n');
            for (int i = tab; i > 0; i--) pp.Append(' ');
            pp.Append('{').Append(goal).Insert(pp.Length - 2, "} e:evidence ").Insert(pp.Length - 2, OWLkb);
            if (tab == 0) pc.Append(goal).Append('\n');
          }
          else {
            Euler gd = goal.deref();
            if (goal.varid != -1 && goal.subj == null && goal.obj == null) {
              Euler gn = goal.near;
              Euler gx = gd;
              while (gx.near != null) gx = gx.near;
              gx.near = gn;
              goal.near = gd.near;
            }
            bool b = Configuration.GetInstance().Steps == -1 || step-istep < Configuration.GetInstance().Steps*ext.engine;
            String d = null;
            if (goal.verb != null) d = (String)ext.dds[goal.verb];
            if (ts == null) {
              lr = this.near;
              while (lr != null) {
                ts = lr;
                if (b && !gd.vv && ts.verb == LOGimplies &&
                    (ts.obj.verb == gd.verb || !ts.obj.bound && gd.bound) &&
                    (d == null || d == ts.src)) {
                  ts = ts.obj;
                  break;
                }
                if (b && (d == null || d == ts.src) && gd.verb == "vv" &&
                    (ts.subj.obj == null || ts.subj.verb == "^^") &&
                    (ts.obj.obj == null || ts.obj.verb == "^^")) {
                  ts = ts.cvv();
                  break;
                }
                if (b && (d == null || d == ts.src) && ts.verb == gd.verb) {
                  if (gd.subj != null && gd.subj.verb == "vv" &&
                      gd.subj.subj != null) {
                    Euler er = ts.copy();
                    er.subj = ts.subj.cvv();
                    ts = er;
                  }
                  if (gd.obj != null && gd.obj.verb == "vv" &&
                      gd.obj.subj != null) {
                    Euler er = ts.copy();
                    er.obj = ts.obj.cvv();
                    ts = er;
                  }
                  break;
                }
                else lr = lr.near;
                ts = null;
              }
            }
            if (ts != null) {
              Euler n = lr.near;
              tsb = null;
              while (n != null) {
                tsb = n;
                if (b && !gd.vv && tsb.verb == LOGimplies &&
                    (tsb.obj.verb == gd.verb || !tsb.obj.bound && gd.bound) &&
                    (d == null || d == tsb.src)) {
                  tsb = tsb.obj;
                  break;
                }
                if (b && (d == null || d == tsb.src) && gd.verb == "vv" &&
                    (tsb.subj.obj == null || tsb.subj.verb == "^^") &&
                    (tsb.obj.obj == null || tsb.obj.verb == "^^")) {
                  tsb = tsb.cvv();
                  break;
                }
                if (b && (d == null || d == tsb.src) && tsb.verb == gd.verb) {
                  if (gd.subj != null && gd.subj.verb == "vv" &&
                      gd.subj.subj != null) {
                    Euler er = tsb.copy();
                    er.subj = tsb.subj.cvv();
                    tsb = er;
                  }
                  if (gd.obj != null && gd.obj.verb == "vv" &&
                      gd.obj.subj != null) {
                    Euler er = tsb.copy();
                    er.obj = tsb.obj.cvv();
                    tsb = er;
                  }
                  break;
                }
                else n = n.near;
                tsb = null;
              }
              if (tsb != null) {
                stack.push(goal, 0);
                stack.push(tsb, 0);
                stack.push(n, 0);
                stack.push(null, pp.Length);
                stack.push(null, pc.Length);
                stack.push(null, tab);
              }
              long hc = ts.uid;
              for (int i = 0; i < ext.varmax; i++) vars[i] = null;
              if (ts.eval(false, vars, stack).unify(goal, this, stack)) {
                if (ts.varid != -1) {
                  vars[ts.varid].verb = gd.verb;
                  vars[ts.varid].cverb = gd.cverb;
                  vars[ts.varid].varid = gd.varid;
                  vars[ts.varid].bound = true;
                  vars[ts.varid].vv = true;
                }
                Euler ep = goal.near;  // @@ euler paths
                while (ep != null) {
                  if (ep.verb == null && hc == ep.uid && ep.obj.unify(goal, this, null)) break;
                  ep = ep.near;
                }
                if (ep != null) {
                  if (Outputter.log) Outputter.GetInstance().Log("Euler", "Proof", "engine" + uid + " cycle " + ep, Outputter.LOGLEVEL.FINER);
                  not = true;
                }
                else {
                  String src = ts.src;
                  if (src == null && ext.baseURI.StartsWith("_:")) src = ext.baseURI;
                  else if (src == null && !ext.baseURI.StartsWith("_:")) src = '<' + ext.baseURI + '>';
                  else if (!src.StartsWith("_:") && src.IndexOf('#') == -1) src = src.Substring(0, src.Length - 1)+ "#_" + ts.line + '>';
                  goal.src = src;
                  ts = ts.premis;
                  if (ts != null) {
                    ts2 = new Euler();
                    ts1 = ts2;
                    while (ts != null) {
                      ts1.near = ts.eval(false, vars, stack);
                      ts1 = ts1.near;
                      ts = ts.near;
                    }
                    ts1.near = new Euler();
                    ts1 = ts1.near;
                    ts1.cverb = "[" + step + "]";
                    ts1.obj = goal;
                    ts1.bound = true;
                    ts1.uid = hc;
                    ts1.near = goal.near;
                    ts1.far = goal.far;
                    goal = ts2;
                    if (pp.Length > 1 && pp[pp.Length - 2] == '.' && pp[pp.Length - 1] == ' ') {
                      pp.Append('\n');
                      for (int i = tab; i > 0; i--) pp.Append(' ');
                    }
                    pp.Append('{');
                    tab++;
                  }
                  else {
                    if (goal.verb == OWLsameAs) synon(goal);
                    if (pp.Length > 1 && pp[pp.Length - 2] == '.' && pp[pp.Length - 1] == ' ') {
                      pp.Append('\n');
                      for (int i = tab; i > 0; i--) pp.Append(' ');
                    }
                    pp.Append('{').Append(goal).Insert(pp.Length - 2, "} e:evidence ").Insert(pp.Length - 2, src);
                    if (tab == 0) pc.Append(goal).Append('\n');
                  }
                }
              }
              else not = true;
            }
            else not = true;
          }
        }
        catch (FormatException) {
          not = true;
        }
        catch (Exception exc) {
          Console.Error.WriteLine(exc);
          not = true;
        }
        if (Outputter.log) {
          if (!not && goal.verb != null) Outputter.GetInstance().Log("Euler", "Proof", "engine" + uid + " [" + step + "]EXIT: " + goal, Outputter.LOGLEVEL.FINER);
          else if (!not && goal.cverb != null) Outputter.GetInstance().Log("Euler", "Proof", "engine" + uid + " " + goal.cverb + "EXIT: " + goal.obj, Outputter.LOGLEVEL.FINER);
          else if (not && goal.verb != null) Outputter.GetInstance().Log("Euler", "Proof", "engine" + uid + " [" + step + "]FAIL: " + goal, Outputter.LOGLEVEL.FINER);
          else if (not && goal.cverb != null) Outputter.GetInstance().Log("Euler", "Proof", "engine" + uid + " " + goal.cverb + "FAIL: " + goal.obj, Outputter.LOGLEVEL.FINER);
        }
        if (goal.verb != null) {
          step++;
          if (Outputter.log && step % 1000000 == 0) Outputter.GetInstance().Log("Euler", "Proof", "engine" + uid + " " + step + " steps for " + u, Outputter.LOGLEVEL.FINE);
        }
        goal = goal.near;
        if (Outputter.log && !not && goal != null && goal.verb != null)
           Outputter.GetInstance().Log("Euler", "Proof", "engine" + uid + " [" + step + "]CALL: " + goal, Outputter.LOGLEVEL.FINER);
        if (!not && goal == null) {
          if (!Configuration.GetInstance().ProofExplanation) proof.Append(pc).Append("\n");
          else proof.Append(pp).Append("\n\n");
          if (Outputter.log) Outputter.GetInstance().Log("Euler", "Proof", "engine" + uid + " continue", Outputter.LOGLEVEL.FINER);
          pct[pc.ToString()] = this;
        }
        if (not || Configuration.GetInstance().Think && goal == null) {
          goal = null;
          Euler b = null;
          while ((b = stack.pop()) != null) {
            if (b.bound) {
              b.bound = false;
              b.refr = null;
            }
            else {
              tab = b.varid;
              pc.Length = stack.pop().varid;
              pp.Length = stack.pop().varid;
              lr = stack.pop();
              ts = stack.pop();
              goal = stack.pop();
              if (Outputter.log) Outputter.GetInstance().Log("Euler", "Proof", "engine" + uid + " [" + step + "]REDO: " + goal, Outputter.LOGLEVEL.FINER);
              break;
            }
          }
        }
      }
    }
  }
  
  internal Euler eval(bool f, Euler[] v, Stack s) {
    if (refr != null && obj == null) return refr.eval(f, v, s);
    if (bound && varid == - 1 && obj == null) return this;
    if (varid != - 1 && v[varid] == null) v[varid] = new Euler();
    if (varid != -1 && v[varid] != null && v[varid].vv) {
      Euler t = new Euler();
      if (subj != null) t.subj = subj.eval(true, v, s);
      if (obj != null) t.obj = obj.eval(true, v, s);
      t.verb = v[varid].verb;
      t.cverb = v[varid].cverb;
      t.varid = v[varid].varid;
      t.bound = true;
      return t;
    }
    else if (obj != null) {
      Euler t = new Euler();
      if (subj != null) t.subj = subj.eval(true, v, s);
      if (obj != null) t.obj = obj.eval(true, v, s);
      t.verb = verb;
      t.cverb = cverb;
      t.varid = varid;
      if (v != null && !bound && varid != - 1) {
        if (v[varid] != t) t.refr = v[varid];
        t.bound = true;
        s.push(t, 0);
      }
      else t.bound = true;
      t.vv = vv;
      if (f && near != null) t.near = near.eval(true, v, s);
      else t.near = near;
      return t;
    }
    v[varid].verb = verb;
    v[varid].cverb = cverb;
    v[varid].varid = varid;
    return v[varid];
  }
  
  internal bool unify(Euler t, Euler r, Stack s) {
    if (t == null) return false;
    if (refr != null && obj == null) return refr.unify(t, r, s);
    if (t.refr != null && t.obj == null) return unify(t.refr, r, s);
    if (bound && t.bound) {
      if (obj != null && verb == "^^" && t.verb == "^^" && subj.bound && t.subj.bound &&
          (subj.unify(t.subj, r, s) && obj.unify(t.obj, r, s) || obj.unify(t.obj, r, s) || Datatype.IsNumeric(r.getType(this)) && Datatype.IsNumeric(r.getType(t))) ||
         (verb == "^^" && subj.bound && obj.bound && t.obj == null || obj == null && t.verb == "^^" && t.subj != null && t.subj.bound && t.obj != null && t.obj.bound) &&
          (r.getType(this) == r.getType(t) || Datatype.IsNumeric(r.getType(this)) && Datatype.IsNumeric(r.getType(t)) || Datatype.IsAlphaNumeric(r.getType(this)) && Datatype.IsAlphaNumeric(r.getType(t))))
        return Datatype.Compare(r.getType(this), r.getLit(this), r.getType(t), r.getLit(t)) == 0;
      if (varid == - 1 && verb != null && t.verb != null && deref().verb != t.deref().verb) return false;
      if (subj != null && !subj.unify(t.subj, r, s)) return false;
      if (obj != null && !obj.unify(t.obj, r, s)) return false;
      if (subj == null && near != null && !near.unify(t.near, r, s)) return false;
      return true;
    }
    if (bound) return t.unify(this, r, s);
    if (s != null) {   
      if (subj != null && !subj.unify(t.subj, r, s)) return false;
      if (obj != null && !obj.unify(t.obj, r, s)) return false;
      if (subj == null && near != null && !near.unify(t.near, r, s)) return false;
      if (t != deref()) deref().refr = t;
      bound = true;
      s.push(this, 0);
    }
    return true;
  }
  
  internal void rewrite(bool eu, Euler el, Parser np) {
    if (el.varid != -1) {
      Euler ex = el.subj.copy();
      el.subj = np.Parse("^^");
      el.subj.subj = ex;
      el.subj.obj = np.Parse(el.cverb);
      el.verb = el.cverb = "vv";
      el.varid = -1;
      el.bound = true;
    }
    if (np.u == null || np.u.StartsWith("_:engine_")) return;
    if (el.subj != null && el.subj.cverb == null)
      el.subj.verb = el.subj.cverb = (eu?"_:":"?v") + el.subj.uid + "_" + doc + "_";
    if (el.obj != null && el.obj.cverb == null)
      el.obj.verb = el.obj.cverb = (eu?"_:":"?v") + el.obj.uid + "_" + doc + "_";
    if (el.subj != null && el.subj.subj == null && el.subj.obj != null && el.subj.getFirst() == null) {
      Euler gr = el.subj.copy();
      Euler gv = np.parse(false, (eu?"_:":"?v") + gr.uid + "_" + doc + "_");
      el.subj = gv;
      Euler gl = gr;
      while (true) {
        gl.subj = gv;
        np.swap(gl);
        if (gl.near == null) break;
        gl = gl.near;
      }
      gl.near = el.near;
      el.near = gr;
      if (el.verb.Equals("")) {
        el.subj = gr.subj;
        el.verb = gr.verb;
        el.obj = gr.obj;
        el.cverb = gr.cverb;
        el.varid = gr.varid;
        el.bound = gr.bound;
        el.near = gr.near;
      }
    }
    if (el.obj != null && el.obj.subj == null && el.obj.obj != null) {
      Euler gr = el.obj.copy();
      Euler gv = np.parse(false, (eu?"_:":"?v") + gr.uid + "_" + doc + "_");
      el.obj = gv;
      Euler gl = gr;
      while (true) {
        gl.subj = gv;
        np.swap(gl);
        if (gl.near == null) break;
        gl = gl.near;
      }
      gl.near = el.near;
      el.near = gr;
    }
    if (el.subj != null && el.subj.verb.Equals("^") && el.subj.subj != null && el.subj.subj.getFirst() == null && !el.verb.Equals(LOGimplies) && !el.verb.Equals(LOGnotImplies)) {
      Euler gr = el.subj.copy();
      rewrite(eu, gr, np);
      Euler gv = np.parse(false, (eu?"_:":"?v") + gr.uid + "_" + doc + "_");
      el.subj = gv;
      Euler gl = gr;
      gl.verb = gl.obj.verb;
      gl.cverb = gl.obj.cverb;
      gl.varid = gl.obj.varid;
      gl.bound = gl.obj.bound;
      gl.obj = gl.subj.copy();
      gl.subj = gv;
      np.swap(gl);
      while (gl.near != null) gl = gl.near;
      gl.near = el.near;
      el.near = gr;
    }
    if (el.obj != null && el.obj.verb.Equals("^") && el.obj.obj != null && !el.verb.Equals(LOGimplies) && !el.verb.Equals(LOGnotImplies)) {
      Euler gr = el.obj.copy();
      rewrite(eu, gr, np);
      Euler gv = np.parse(false, (eu?"_:":"?v") + gr.uid + "_" + doc + "_");
      el.obj = gv;
      Euler gl = gr;
      gl.verb = gl.obj.verb;
      gl.cverb = gl.obj.cverb;
      gl.varid = gl.obj.varid;
      gl.bound = gl.obj.bound;
      gl.obj = gl.subj.copy();
      gl.subj = gv;
      np.swap(gl);
      while (gl.near != null) gl = gl.near;
      gl.near = el.near;
      el.near = gr;
    }
    if (el.subj != null && el.subj.verb.Equals("!") && el.subj.subj != null && el.subj.subj.getFirst() == null && !el.verb.Equals(LOGimplies) && !el.verb.Equals(LOGnotImplies)) {
      Euler gr = el.subj.copy();
      rewrite(eu, gr, np);
      Euler gv = np.parse(false, (eu?"_:":"?v") + gr.uid + "_" + doc + "_");
      el.subj = gv;
      Euler gl = gr;
      gl.verb = gl.obj.verb;
      gl.cverb = gl.obj.cverb;
      gl.varid = gl.obj.varid;
      gl.bound = gl.obj.bound;
      gl.obj = gv;
      np.swap(gl);
      while (gl.near != null) gl = gl.near;
      gl.near = el.near;
      el.near = gr;
    }
    if (el.obj != null && el.obj.verb.Equals("!") && el.obj.obj != null && !el.verb.Equals(LOGimplies) && !el.verb.Equals(LOGnotImplies)) {
      Euler gr = el.obj.copy();
      rewrite(eu, gr, np);
      Euler gv = np.parse(false, (eu?"_:":"?v") + gr.uid + "_" + doc + "_");
      el.obj = gv;
      Euler gl = gr;
      gl.verb = gl.obj.verb;
      gl.cverb = gl.obj.cverb;
      gl.varid = gl.obj.varid;
      gl.bound = gl.obj.bound;
      gl.obj = gv;
      np.swap(gl);
      while (gl.near != null) gl = gl.near;
      gl.near = el.near;
      el.near = gr;
    }
  }

  internal Euler copy() {
    Euler el = new Euler();
    if (subj != null) el.subj = subj.copy();
    el.verb = verb;
    if (obj != null) el.obj = obj.copy();
    el.cverb = cverb;
    el.varid = varid;
    el.bound = bound;
    if (refr != el) el.refr = refr;
    el.premis = premis;
    if (near != null) el.near = near.copy();
    el.far = far;
    el.src = src;
    el.line = line;
    return el;
  }
  
  internal Euler cvv() {
    Euler el = copy();
    el.subj = copy();
    el.subj.verb = el.subj.cverb = "^^";
    el.subj.obj.verb = verb;
    el.subj.obj.cverb = cverb;
    el.verb = el.cverb = "vv";
    return el;
  }

  internal void getX(bool f, ArrayList wt) {
    if (subj != null) subj.getX(true, wt);
    if (verb != null && (verb.StartsWith("_:") || verb.StartsWith("?")) && !wt.Contains(verb))
      wt.Add(verb);
    if (obj != null) obj.getX(true, wt);
    if (f && near != null) near.getX(f, wt);
  }
  
  internal void forX(bool f, ArrayList wt) {
    if (subj != null) subj.forX(true, wt);
    if (verb != null && wt.Count > 0 && wt.IndexOf(verb) != - 1) {
      if (!cverb.StartsWith("_:") && cverb.IndexOf('#') != -1) cverb = "?" + cverb.Substring(cverb.IndexOf('#') + 1, cverb.Length - cverb.IndexOf('#') - 2);
      else if (!cverb.StartsWith("_:") && cverb.IndexOf(':') != -1) cverb = "?" + cverb.Substring(cverb.IndexOf(':') + 1);
      varid = wt.IndexOf(verb);
      bound = false;
    }
    if (obj != null) obj.forX(true, wt);
    if (f && near != null) near.forX(f, wt);
  }
  
  internal void reorder(Euler er) {
    Euler el = er.near;
    Euler elc = null, elcp = null, elv = null, elvp = null;
    while (el != null) {
      if (el.varid != -1 || el.verb.Equals(RDFtype)) {
        if (elv == null) elvp = elv = el;
        else elvp = elvp.near = el;
      }
      else {
        if (elc == null) elcp = elc = el;
        else elcp = elcp.near = el;
      }
      el = el.near;
    }
    if (elvp != null) elvp.near = null;
    if (elcp != null) elcp.near = elv;
    if (elc != null) er.near = elc;
  }

  internal void reorderPremis(Euler er) {
    Euler el = er.subj;
    Euler elc = null, elcp = null, elv = null, elvp = null;
    while (el != null) {
      if (er.obj.subj != null && el.subj.verb.Equals(er.obj.subj.verb) && el.verb.Equals(er.obj.verb)) {
        if (elv == null) elvp = elv = el;
        else elvp = elvp.near = el;
      }
      else {
        if (elc == null) elcp = elc = el;
        else elcp = elcp.near = el;
      }
      el = el.near;
    }
    if (elvp != null) elvp.near = null;
    if (elcp != null) elcp.near = elv;
    if (elc != null) er.subj = elc;
  }

  internal void synon(Euler t) {
    if (t.subj.deref().verb.Equals("^^") || t.obj.deref().verb.Equals("^^")) return;
    bool w = !t.subj.deref().verb.StartsWith(W3);
    String s = w?t.subj.deref().verb:t.obj.deref().verb;
    String o = w?t.obj.deref().verb:t.subj.deref().verb;
    if (o == null || s == null) return;
    if (t.subj != null && t.obj != null && t.subj.subj == null &&
        t.subj.obj == null && t.obj.subj == null && t.obj.obj == null) {
      if (!s.Equals(o)) ext.syn[s] = o;
      for (IEnumerator e = (IEnumerator) ((Hashtable)ext.syn.Clone()).Keys.GetEnumerator(); e.MoveNext(); ) {
        String k = (String) e.Current;
        if (ext.syn[k] != null && ext.syn[k].Equals(s)) {
          if (!k.Equals(o)) ext.syn[k] = o;
          else ext.syn.Remove(k);
        }
      }
    }
    else if (t.subj != null && t.obj == null && t.subj.subj == null && t.subj.obj == null) ext.syn[s] = t;
    else if (t.subj == null && t.obj != null && t.obj.subj == null && t.obj.obj == null) ext.syn[o] = t;
  }
  
  internal void syno(Euler t) {
    for (Euler el = t; el != null; el = el.near) synt(el);
  }
  
  internal void synt(Euler t) {
    if (t.subj != null) syno(t.subj);
    if (t.verb != null) {
      Object o = this.ext.syn[t.verb];
      if (o != null) {
        if (o is String) t.verb = (String) o;
        else t.verb = o.ToString();
      }
    }
    if (t.obj != null) syno(t.obj);
  }
  
  internal Euler deref() {
    if (refr != null) return refr.deref();
    else return this;
  }
  
  /// <summary>string represention of this Euler object</summary>
  /// <returns>string</returns>

  public override String ToString() {
    if (refr != null && obj == null) return refr.ToString();
    if (subj == null && verb == null && obj == null) return "[]";
    String cv = deref().cverb;
    if (cv != null && cv.Equals("^^")) return subj + "^^" + obj;
    if (cv != null && cv.Equals("^")) return subj + "^" + obj;
    if (cv != null && cv.Equals("!")) return subj + "!" + obj;
    if (cv != null && cv.Equals("vv") && subj != null && subj.verb.Equals("^^") && subj.subj.bound)
      return subj.subj + " " + subj.obj + " " + obj + ". ";
    if (obj == null) {
      if (cv == null) return deref().verb;
      return cv;
    }
    Euler el = deref();
    Euler en = null;
    StringBuilder r = new StringBuilder(64);
    bool sv = subj != null && subj.refr == null && subj.subj == null &&
              subj.cverb != null && subj.cverb.Equals("[]") && subj.obj == null;
    bool ov = obj != null && obj.refr == null && obj.subj == null &&
              obj.cverb != null && obj.cverb.Equals("[]") && obj.obj == null;
    if (el.verb != null && el.verb.Equals(RDFfirst) && el.subj == null && el.obj != null) {
      r.Append('(');
      while (el != null && el.obj != null) {
        int i = r.Length;
        r.Append(el.obj.deref());
        if (r.Length > 1 && (r[r.Length - 2] == '.' && r[r.Length - 1] == ' ' || r[r.Length - 1] == ';')) {
          if (r[i] != ' ') {
            r.Insert(i, '{');
            r[r.Length - 2] = '}';
          }
          else {
            r.Insert(i, '[');
            r[r.Length - 1] = ']';
          }
        }
        en = el.near.obj.deref();
        if (en.verb.Equals(RDFnil)) break;
        else if (!en.verb.Equals(RDFfirst)) {
          r.Append("/ ");
          r.Append(en);
          break;
        }
        r.Append(' ');
        el = en;
      }
      r.Append(')');
      return r.ToString();
    }
    if (!sv && subj != null && subj.deref().subj != null && verb != null && subj.deref().verb != "!") {
      el = subj.deref();
      while (el != null && el.verb != null) {
        r.Append(el);
        el = el.near;
      }
    }
    else if (!sv && subj != null || !sv && subj != null && subj.deref().subj == null) {
      el = subj.deref();
      r.Append(el);
    }
    if (r.Length > 1 && (r[r.Length - 2] == '.' && r[r.Length - 1] == ' ' || r[r.Length - 1] == ';')) {
      if (r[0] != ' ') {
        r.Insert(0, '{');
        r[r.Length - 2] = '}';
      }
      else {
        r.Insert(0, '[');
        r[r.Length - 1] = ']';
      }
    }
    if (r.Length > 0 && r[r.Length - 1] != ' ') r.Append(' ');
    if (deref().cverb != null) r.Append(deref().cverb);
    else r.Append(cverb);
    r.Append(' ');
    int i2 = r.Length;
    if (!ov && obj != null && obj.deref().subj != null && verb != null && obj.deref().verb != "!") {
      el = obj.deref();
      while (el != null && el.verb != null) {
        r.Append(el);
        el = el.near;
      }
    }
    else if (!ov && obj != null || !ov && obj != null && obj.deref().subj == null) {
      el = obj.deref();
      r.Append(el);
    }
    if (r.Length > 1 && (r[r.Length - 2] == '.' && r[r.Length - 1] == ' ' || r[r.Length - 1] == ';')) {
      if (r[i2] != ' ') {
        r.Insert(i2, '{');
        r[r.Length - 2] = '}';
      }
      else {
        r.Insert(i2, '[');
        r[r.Length - 1] = ']';
      }
    }
    if (!sv && subj != null && r[r.Length - 1] == ' ') r.Insert(r.Length - 1, '.');
    else if (!sv && subj != null && r[r.Length - 1] != ' ') r.Append(". ");
    else {
      r.Append(';');
      el = near;
      while (el != null) {
        r.Append(' ').Append(el.deref().cverb).Append(' ');
        r.Append(el.obj);
        r.Append(';');
        el = el.near;
      }
      r.Insert(0, '[');
      r[r.Length - 1] = ']';
    }
    return r.ToString();
  }
  
  internal Euler getFirst() {
    Euler er = this;
    if (verb == "^^" || verb == "^" || verb == "!") er = subj;
    while (er != null) {
      if (er.verb == RDFfirst) return er.obj;
      else er = er.near;
    }
    return null;
  }

  internal Euler getRest() {
    Euler er = this;
    if (verb == "^^" || verb == "^" || verb == "!") er = subj;
    while (er != null) {
      if (er.verb == RDFrest) return er.obj;
      else er = er.near;
    }
    return null;
  }

  internal String getLit(Euler el) {
    String s = el.verb;
    if (s == "!" && el.obj != null && (el.obj.verb.StartsWith(MATH) || el.obj.verb.StartsWith(STR))) {
      Proof("data:," + el.subj + " " + el.obj + " ?X. ");
      if (obj != null) s = obj.cverb;
    }
    if (s == "^^") return getLit(el.subj.deref());
    if (s.StartsWith("\"\"\"")) return s.Substring(3, s.Length - 6);
    if (s.IndexOf('"') != -1) return s.Substring(s.IndexOf('"') + 1, s.LastIndexOf('"') - s.IndexOf('"') - 1);
    return s;
  }

  internal String getType(Euler el) {
    if (el.obj == null) {
      if (el.isNumeral()) return XSDdouble;
      else return XSDstring;
    }
    else return el.obj.deref().verb;
  }

  internal double mathCompare(Euler el) {
    Euler s = el.subj.deref();
    Euler o = el.obj.deref();
    if ((s.verb == "^^" || o.verb == "^^") &&
        (getType(s) == getType(o) || Datatype.IsNumeric(getType(s)) && Datatype.IsNumeric(getType(o))))
      return Datatype.Compare(getType(s), getLit(s), getType(o), getLit(o));
    else if (Datatype.IsNumeric(getType(s)) && Datatype.IsNumeric(getType(o)))
      return Double.Parse(getLit(s), NumberFormatInfo.InvariantInfo) - Double.Parse(getLit(o), NumberFormatInfo.InvariantInfo);
    else throw new FormatException();
  }

  internal String fromWeb(String uri) {
    StringBuilder sb = new StringBuilder();
    String rl = null;
    if (uri.StartsWith("data:")) {
      ext.baseURI = "_:engine_" + ext.engine;
      return uri.Substring(uri.IndexOf(',') + 1);
    }
    else if (uri.StartsWith("{")) {
      ext.baseURI = "_:engine_" + ext.engine;
      return uri.Substring(1, uri.Length - 2);
    }
    else if (uri.StartsWith("http:")) {
      try {
        if (!uri.StartsWith("http://localhost/euler.AskJena?fromWeb=")) ext.baseURI = uri;
        if (!Configuration.GetInstance().RunLocal || uri.StartsWith("http://localhost")) {
          Uri r = new Uri(uri);
          String p = r.PathAndQuery;
          String hp = Environment.GetEnvironmentVariable("http_proxy");
          if (hp != null && !hp.Equals("") && !hp.Equals("%http_proxy%") && !uri.StartsWith("http://localhost")) {
            r = new Uri(hp);
            p = uri;
          }
          TcpClient so = new TcpClient(r.Host, r.Port == - 1?80:r.Port);
          //so.NoDelay.Enabled = true;
          StreamWriter pw = new StreamWriter((Stream) so.GetStream());
          pw.WriteLine("GET " + p + " HTTP/1.0");
          pw.WriteLine("Host: " + r.Host);
          pw.WriteLine("");
          pw.Flush();
          StreamReader br = new StreamReader((Stream) so.GetStream());
          if ((rl = br.ReadLine()).IndexOf("200") == - 1) throw new SystemException(rl);
          while (!br.ReadLine().Equals(""));
          while ((rl = br.ReadLine()) != null) {
            sb.Append(rl);
            sb.Append('\n');
          }
          so.Close();
        }
        else {
          StreamReader br = new StreamReader(uri.Substring(6));
          while ((rl = br.ReadLine()) != null) {
            sb.Append(rl);
            sb.Append('\n');
          }
          br.Close();
        }
      }
      catch (Exception) {
        if (uri.StartsWith("http://localhost")) throw new SystemException(uri);
        if (ext.baseURI.EndsWith(".owl.n3") || ext.baseURI.EndsWith(".rss.n3")) ext.baseURI = ext.baseURI.Substring(0, ext.baseURI.Length - 3);
        if (ext.baseURI.EndsWith(".n3")) ext.baseURI = ext.baseURI.Substring(0, ext.baseURI.Length - 3) + ".rdf";
        if (uri.EndsWith(".owl.n3") || uri.EndsWith(".rss.n3")) uri = uri.Substring(0, uri.Length - 3);
        if (uri.EndsWith(".n3")) uri = uri.Substring(0, uri.Length - 3) + ".rdf";
        return fromWeb("http://localhost/euler.AskJena?fromWeb=" + (!Configuration.GetInstance().RunLocal?uri:uri.Substring(6)));
      }
    }
    else {
      if (uri.StartsWith("file:")) uri = uri.Substring(uri.IndexOf(':') + 1);
      if (uri.StartsWith("//")) uri = uri.Substring(1);
      if (uri.IndexOf('#') != - 1) uri = uri.Substring(0, uri.LastIndexOf('#'));
      try {
        String path = Directory.GetCurrentDirectory().Replace(Path.DirectorySeparatorChar, '/');
        path = path.Substring(path.IndexOf('/')) + "/";
        ext.baseURI = "file:/" + ((uri[0] == '/' || uri[1] ==':') ? "" : path) + uri;
        StreamReader br = new StreamReader(uri);
        while ((rl = br.ReadLine()) != null) {
          sb.Append(rl);
          sb.Append('\n');
        }
        br.Close();
      }
      catch (Exception) {
        if (ext.baseURI.EndsWith(".owl.n3") || ext.baseURI.EndsWith(".rss.n3")) ext.baseURI = ext.baseURI.Substring(0, ext.baseURI.Length - 3);
        if (ext.baseURI.EndsWith(".n3")) ext.baseURI = ext.baseURI.Substring(0, ext.baseURI.Length - 3) + ".rdf";
        if (uri.EndsWith(".owl.n3") || uri.EndsWith(".rss.n3")) uri = uri.Substring(0, uri.Length - 3);
        if (uri.EndsWith(".n3")) uri = uri.Substring(0, uri.Length - 3) + ".rdf";
        return fromWeb("http://localhost/euler.AskJena?fromWeb=" + uri);
      }
    }
    return sb.ToString();
  }
  
  internal String toURI(Euler el) {
    if (el.verb == "^^" || el.verb == "^" || el.verb == "!") el = el.subj.deref();
    if (el.obj != null) {
      StringBuilder sb = new StringBuilder("data:,");
      for (IEnumerator en = (IEnumerator) ext.ns.Keys.GetEnumerator(); en.MoveNext(); ) {
        Object nsx = en.Current;
        sb.Append("@prefix ").Append(nsx).Append(' ').Append(ext.ns[nsx]).Append(".\n");
      }
      for (Euler eu = el; eu != null; eu = eu.near) sb.Append(eu);
      return sb.ToString();
    }
    else if (el.verb.Equals("this")) return ext.baseURI;
    else if (el.verb.StartsWith(RDF)) return "http://www.agfa.com/w3c/euler/rdf-rules.n3";
    else if (el.verb.StartsWith(RDFS)) return "http://www.agfa.com/w3c/euler/rdfs-rules.n3";
    else if (el.verb.StartsWith(XSD)) return "http://www.agfa.com/w3c/euler/xsd-rules.n3";
    else if (el.verb.StartsWith(OWL)) return "http://www.agfa.com/w3c/euler/owl-rules.n3";
    else {
      String s = el.verb;
      if (s[0] == '<') s = s.Substring(1, s.Length - 2);
      if (s.IndexOf('#') != -1) s = s.Substring(0, s.IndexOf('#'));
      if (s.EndsWith(".rdf")) s = s.Substring(0, s.Length - 4) + ".n3";
      else if (!s.EndsWith(".n3") && !s.EndsWith(".nt") && !s.StartsWith("data:") && !s.StartsWith("{")) s = s + ".n3";
      return s;
    }
  }
  
  internal String nat(Euler el, double d) {
    if (el.getFirst() == null && getLit(el.deref()).IndexOf('.') != -1) return d.ToString(NumberFormatInfo.InvariantInfo);
    while (el.getFirst() != null) {
      if (getLit(el.getFirst().deref()).IndexOf('.') != -1) return d.ToString(NumberFormatInfo.InvariantInfo);
      el = el.getRest();
    }
    return ((int)d).ToString(NumberFormatInfo.InvariantInfo);
  }

  internal bool isNumeral() {
    try {
      Double.Parse(verb, NumberFormatInfo.InvariantInfo);
      return true;
    }
    catch (Exception) {
      return false;
    }
  }

  internal String now() {
    DateTime d = DateTime.UtcNow;
    StringBuilder sb = new StringBuilder();
    sb.Append(d.Year).Append('-')
      .Append(d.Month<10?"0":"").Append(d.Month).Append('-')
      .Append(d.Day<10?"0":"").Append(d.Day).Append('T')
      .Append(d.Hour<10?"0":"").Append(d.Hour).Append(':')
      .Append(d.Minute<10?"0":"").Append(d.Minute).Append(':')
      .Append(d.Second<10?"0":"").Append(d.Second).Append('Z');
    return sb.ToString();
  }

  internal String toHex(String s) {
    StringBuilder sb = new StringBuilder();
    for (int i = 0; i < s.Length; i++) sb.Append(Convert.ToString(s[i], 16));
    return sb.ToString();
  }

    /// <summary>Main method invoked via <code>Euler</code></summary>
    /// <param name="args">[--think] [--nope] [--step count] [--debug] [--trace] axiom ... [--filter|--query] lemma</param>

  [STAThread]
  public static void Main(string[] args) {
    if (args.Length == 0)
      Console.Error.WriteLine("Version: " + Configuration.GetInstance().Version + "\nUsage: Euler [--think] [--nope] [--step count] [--debug] [--trace] axiom ... [--filter|--query] lemma");
    else {
      try {
        //Configuration.GetInstance().Steps = 1;
        TextWriter outp = Console.Out;
        Euler e = new Euler();
        Parser np = new Parser();
        int n = args.Length - 1;
        if (args[n].StartsWith(">")) {
          outp = new StreamWriter(new FileStream(new FileInfo(args[n].Substring(1)).FullName, FileMode.Create));
          n--;
        }
        String c = e.toURI(np.Parse('<' + args[n] + '>'));
        for (int j = 0; j < n; j++) {
          if (args[j].EndsWith("-think")) Configuration.GetInstance().Think = true;
          else if (args[j].EndsWith("-nope")) Configuration.GetInstance().ProofExplanation = false;
          else if (args[j].EndsWith("-step")) Configuration.GetInstance().Steps = Int64.Parse(args[++j]);
          else if (args[j].EndsWith("-local")) Configuration.GetInstance().RunLocal = true;
          else if (args[j].EndsWith("-debug")) StdOutputter.GetInstance().setLogLevel(Outputter.LOGLEVEL.FINE);
          else if (args[j].EndsWith("-trace")) StdOutputter.GetInstance().setLogLevel(Outputter.LOGLEVEL.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] + '>')));
            StringBuilder sb = new StringBuilder("data:,");
            for (IEnumerator en = (IEnumerator) el.ext.ns.Keys.GetEnumerator(); en.MoveNext(); ) {
              Object nsx = en.Current;
              sb.Append("@prefix ").Append(nsx).Append(' ').Append(el.ext.ns[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] + '>')));
            StringBuilder sb = new StringBuilder("data:,");
            for (IEnumerator en = (IEnumerator) el.ext.ns.Keys.GetEnumerator(); en.MoveNext(); ) {
              Object nsx = en.Current;
              sb.Append("@prefix ").Append(nsx).Append(' ').Append(el.ext.ns[nsx]).Append(".\n");
            }
            while (el.near != null) {
              if (el.near.verb.Equals(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);
                    sb.Append(ee);
                  }
                  sb.Append("} => {_:").Append(el.near.uid).Append(' ').Append(Qselect).Append(" {");
                  e.rewrite(false, er, np);
                  sb.Append(er).Append("}}. ");
                }
                el = el.near;
              }
              else if (el.near.verb.Equals(Qselect) && el.near.near.verb.Equals(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);
                    sb.Append(ee);
                  }
                  sb.Append("} => {").Append(el.near.subj).Append(' ').Append(Qselect).Append(" {");
                  e.rewrite(false, er, np);
                  sb.Append(er).Append("}}. ");
                }
                el = el.near.near;
              }
              else el = el.near;
            }
            c = sb.ToString();
            e.Load(c);
          }
        }
        e.Prepare();
        String p = e.Proof(c);
        if (!Configuration.GetInstance().ProofExplanation) {
          Euler el = new Euler();
          el.uid = -1;
          el.Load("data:," + p);
          StringBuilder sb = new StringBuilder();
          for (IEnumerator enr = (IEnumerator) el.ext.ns.Keys.GetEnumerator(); enr.MoveNext(); ) {
            Object nsx = enr.Current;
            sb.Append("@prefix ").Append(nsx).Append(' ').Append(el.ext.ns[nsx]).Append(".\n");
          }
          sb.Append('\n');
          for (Euler eu = el; eu.near != null; eu = eu.near) {
            if (eu.near.verb.Equals(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.Equals("vv")) sb.Append(el.near).Append('\n');
            el = el.near;
          }
          p = sb.ToString();
        }
        outp.WriteLine(p);
        if (outp != Console.Out) outp.Close();
      }
      catch (Exception e) {
        Console.Error.WriteLine(e);
      }
    }
  }  
}