26 files changed, 225 insertions, 67 deletions
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/.project b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/.project
index 2221f39c..e73fac6d 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/.project
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/.project
@@ -6,6 +6,11 @@
        </projects>
        <buildSpec>
                <buildCommand>
+                        <name>org.eclipse.viatra.query.tooling.ui.projectbuilder</name>
+                        <arguments>
+                        </arguments>
+                </buildCommand>
+                <buildCommand>
                        <name>org.eclipse.xtext.ui.shared.xtextBuilder</name>
                        <arguments>
                        </arguments>
@@ -30,5 +35,6 @@
                <nature>org.eclipse.pde.PluginNature</nature>
                <nature>org.eclipse.jdt.core.javanature</nature>
                <nature>org.eclipse.xtext.ui.shared.xtextNature</nature>
+                <nature>org.eclipse.viatra.query.projectnature</nature>
        </natures>
 </projectDescription>
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/META-INF/MANIFEST.MF b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/META-INF/MANIFEST.MF
index 63d39592..6ed29084 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/META-INF/MANIFEST.MF
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/META-INF/MANIFEST.MF
@@ -6,12 +6,17 @@ Bundle-Version: 1.0.0.qualifier
 Export-Package: ca.mcgill.ecse.dslreasoner.vampire.reasoner,
  ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder,
  ca.mcgill.ecse.dslreasoner.vampire.reasoner.queries
-Require-Bundle: org.eclipse.xtend.lib,
+Require-Bundle: org.eclipse.emf.ecore,
+  org.eclipse.viatra.query.runtime.rete,
+  org.eclipse.viatra.query.runtime.localsearch,
+  org.eclipse.xtext.xbase.lib,
+  org.eclipse.xtend.lib,
  hu.bme.mit.inf.dslreasoner.logic.model;bundle-version="1.0.0",
  hu.bme.mit.inf.dslreasoner.ecore2logic;bundle-version="1.0.0",
  ca.mcgill.ecse.dslreasoner.vampire.language;bundle-version="1.0.0",
  org.eclipse.viatra.query.runtime;bundle-version="2.1.0",
  org.eclipse.viatra.query.runtime.base.itc;bundle-version="2.1.0",
  org.apache.log4j;bundle-version="1.2.15"
-Automatic-Module-Name: ca.mcgill.ecse.dslreasoner.vampire.reasoner
 Bundle-RequiredExecutionEnvironment: JavaSE-1.8
+Import-Package: org.apache.log4j
+Automatic-Module-Name: ca.mcgill.ecse.dslreasoner.vampire.reasoner
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/build.properties b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/build.properties
index aed85a48..efae4b07 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/build.properties
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/build.properties
@@ -1,5 +1,6 @@
 bin.includes = META-INF/,\
               .
 source.. = src/,\
+           src-gen/,\
           src-gen/
 output.. = bin/
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/queries/ca/mcgill/ecse/dslreasoner/vampire/reasoner/queries/vampireQueries.vql b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/queries/ca/mcgill/ecse/dslreasoner/vampire/reasoner/queries/vampireQueries.vql
index 2db380e4..be5a7c1f 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/queries/ca/mcgill/ecse/dslreasoner/vampire/reasoner/queries/vampireQueries.vql
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/queries/ca/mcgill/ecse/dslreasoner/vampire/reasoner/queries/vampireQueries.vql
@@ -48,8 +48,8 @@ pattern VLSInequality(term: VLSInequality){
        VLSInequality(term);
 }
-pattern VLSFunctionFof(term: VLSFunctionFof){
+pattern VLSFunctionFof(term: VLSFunctionAsTerm){
-        VLSFunctionFof(term);
+        VLSFunctionAsTerm(term);
 }
 //pattern VLSFofTerm(term: VLSFofTerm){
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/queries/VLSFunctionFof.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/queries/VLSFunctionFof.java
index 5a88b0b4..0e82d459 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/queries/VLSFunctionFof.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/queries/VLSFunctionFof.java
@@ -3,6 +3,7 @@
 */
 package ca.mcgill.ecse.dslreasoner.vampire.reasoner.queries;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunctionAsTerm;
 import java.util.Arrays;
 import java.util.Collection;
 import java.util.LinkedHashSet;
@@ -40,8 +41,8 @@ import org.eclipse.viatra.query.runtime.util.ViatraQueryLoggingUtil;
 * 
 * <p>Original source:
 *         <code><pre>
- *         pattern VLSFunctionFof(term: VLSFunctionFof){
+ *         pattern VLSFunctionFof(term: VLSFunctionAsTerm){
- *              VLSFunctionFof(term);
+ *              VLSFunctionAsTerm(term);
 *         }
 * </pre></code>
 * 
@@ -64,11 +65,11 @@ public final class VLSFunctionFof extends BaseGeneratedEMFQuerySpecification<VLS
   * 
   */
  public static abstract class Match extends BasePatternMatch {
-    private ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunctionFof fTerm;
+    private VLSFunctionAsTerm fTerm;
    
    private static List<String> parameterNames = makeImmutableList("term");
    
-    private Match(final ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunctionFof pTerm) {
+    private Match(final VLSFunctionAsTerm pTerm) {
      this.fTerm = pTerm;
    }
    
@@ -78,7 +79,7 @@ public final class VLSFunctionFof extends BaseGeneratedEMFQuerySpecification<VLS
      return null;
    }
    
-    public ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunctionFof getTerm() {
+    public VLSFunctionAsTerm getTerm() {
      return this.fTerm;
    }
    
@@ -86,13 +87,13 @@ public final class VLSFunctionFof extends BaseGeneratedEMFQuerySpecification<VLS
    public boolean set(final String parameterName, final Object newValue) {
      if (!isMutable()) throw new java.lang.UnsupportedOperationException();
      if ("term".equals(parameterName) ) {
-          this.fTerm = (ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunctionFof) newValue;
+          this.fTerm = (VLSFunctionAsTerm) newValue;
          return true;
      }
      return false;
    }
    
-    public void setTerm(final ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunctionFof pTerm) {
+    public void setTerm(final VLSFunctionAsTerm pTerm) {
      if (!isMutable()) throw new java.lang.UnsupportedOperationException();
      this.fTerm = pTerm;
    }
@@ -173,7 +174,7 @@ public final class VLSFunctionFof extends BaseGeneratedEMFQuerySpecification<VLS
     * @return the new, mutable (partial) match object.
     * 
     */
-    public static VLSFunctionFof.Match newMutableMatch(final ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunctionFof pTerm) {
+    public static VLSFunctionFof.Match newMutableMatch(final VLSFunctionAsTerm pTerm) {
      return new Mutable(pTerm);
    }
    
@@ -185,12 +186,12 @@ public final class VLSFunctionFof extends BaseGeneratedEMFQuerySpecification<VLS
     * @return the (partial) match object.
     * 
     */
-    public static VLSFunctionFof.Match newMatch(final ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunctionFof pTerm) {
+    public static VLSFunctionFof.Match newMatch(final VLSFunctionAsTerm pTerm) {
      return new Immutable(pTerm);
    }
    
    private static final class Mutable extends VLSFunctionFof.Match {
-      Mutable(final ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunctionFof pTerm) {
+      Mutable(final VLSFunctionAsTerm pTerm) {
        super(pTerm);
      }
      
@@ -201,7 +202,7 @@ public final class VLSFunctionFof extends BaseGeneratedEMFQuerySpecification<VLS
    }
    
    private static final class Immutable extends VLSFunctionFof.Match {
-      Immutable(final ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunctionFof pTerm) {
+      Immutable(final VLSFunctionAsTerm pTerm) {
        super(pTerm);
      }
      
@@ -223,8 +224,8 @@ public final class VLSFunctionFof extends BaseGeneratedEMFQuerySpecification<VLS
   * 
   * <p>Original source:
   * <code><pre>
-   * pattern VLSFunctionFof(term: VLSFunctionFof){
+   * pattern VLSFunctionFof(term: VLSFunctionAsTerm){
-   *    VLSFunctionFof(term);
+   *    VLSFunctionAsTerm(term);
   * }
   * </pre></code>
   * 
@@ -282,7 +283,7 @@ public final class VLSFunctionFof extends BaseGeneratedEMFQuerySpecification<VLS
     * @return matches represented as a Match object.
     * 
     */
-    public Collection<VLSFunctionFof.Match> getAllMatches(final ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunctionFof pTerm) {
+    public Collection<VLSFunctionFof.Match> getAllMatches(final VLSFunctionAsTerm pTerm) {
      return rawStreamAllMatches(new Object[]{pTerm}).collect(Collectors.toSet());
    }
    
@@ -296,7 +297,7 @@ public final class VLSFunctionFof extends BaseGeneratedEMFQuerySpecification<VLS
     * @return a stream of matches represented as a Match object.
     * 
     */
-    public Stream<VLSFunctionFof.Match> streamAllMatches(final ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunctionFof pTerm) {
+    public Stream<VLSFunctionFof.Match> streamAllMatches(final VLSFunctionAsTerm pTerm) {
      return rawStreamAllMatches(new Object[]{pTerm});
    }
    
@@ -307,7 +308,7 @@ public final class VLSFunctionFof extends BaseGeneratedEMFQuerySpecification<VLS
     * @return a match represented as a Match object, or null if no match is found.
     * 
     */
-    public Optional<VLSFunctionFof.Match> getOneArbitraryMatch(final ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunctionFof pTerm) {
+    public Optional<VLSFunctionFof.Match> getOneArbitraryMatch(final VLSFunctionAsTerm pTerm) {
      return rawGetOneArbitraryMatch(new Object[]{pTerm});
    }
    
@@ -318,7 +319,7 @@ public final class VLSFunctionFof extends BaseGeneratedEMFQuerySpecification<VLS
     * @return true if the input is a valid (partial) match of the pattern.
     * 
     */
-    public boolean hasMatch(final ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunctionFof pTerm) {
+    public boolean hasMatch(final VLSFunctionAsTerm pTerm) {
      return rawHasMatch(new Object[]{pTerm});
    }
    
@@ -328,7 +329,7 @@ public final class VLSFunctionFof extends BaseGeneratedEMFQuerySpecification<VLS
     * @return the number of pattern matches found.
     * 
     */
-    public int countMatches(final ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunctionFof pTerm) {
+    public int countMatches(final VLSFunctionAsTerm pTerm) {
      return rawCountMatches(new Object[]{pTerm});
    }
    
@@ -340,7 +341,7 @@ public final class VLSFunctionFof extends BaseGeneratedEMFQuerySpecification<VLS
     * @return true if the pattern has at least one match with the given parameter values, false if the processor was not invoked
     * 
     */
-    public boolean forOneArbitraryMatch(final ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunctionFof pTerm, final Consumer<? super VLSFunctionFof.Match> processor) {
+    public boolean forOneArbitraryMatch(final VLSFunctionAsTerm pTerm, final Consumer<? super VLSFunctionFof.Match> processor) {
      return rawForOneArbitraryMatch(new Object[]{pTerm}, processor);
    }
    
@@ -352,7 +353,7 @@ public final class VLSFunctionFof extends BaseGeneratedEMFQuerySpecification<VLS
     * @return the (partial) match object.
     * 
     */
-    public VLSFunctionFof.Match newMatch(final ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunctionFof pTerm) {
+    public VLSFunctionFof.Match newMatch(final VLSFunctionAsTerm pTerm) {
      return VLSFunctionFof.Match.newMatch(pTerm);
    }
    
@@ -361,8 +362,8 @@ public final class VLSFunctionFof extends BaseGeneratedEMFQuerySpecification<VLS
     * @return the Set of all values or empty set if there are no matches
     * 
     */
-    protected Stream<ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunctionFof> rawStreamAllValuesOfterm(final Object[] parameters) {
+    protected Stream<VLSFunctionAsTerm> rawStreamAllValuesOfterm(final Object[] parameters) {
-      return rawStreamAllValues(POSITION_TERM, parameters).map(ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunctionFof.class::cast);
+      return rawStreamAllValues(POSITION_TERM, parameters).map(VLSFunctionAsTerm.class::cast);
    }
    
    /**
@@ -370,7 +371,7 @@ public final class VLSFunctionFof extends BaseGeneratedEMFQuerySpecification<VLS
     * @return the Set of all values or empty set if there are no matches
     * 
     */
-    public Set<ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunctionFof> getAllValuesOfterm() {
+    public Set<VLSFunctionAsTerm> getAllValuesOfterm() {
      return rawStreamAllValuesOfterm(emptyArray()).collect(Collectors.toSet());
    }
    
@@ -379,14 +380,14 @@ public final class VLSFunctionFof extends BaseGeneratedEMFQuerySpecification<VLS
     * @return the Set of all values or empty set if there are no matches
     * 
     */
-    public Stream<ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunctionFof> streamAllValuesOfterm() {
+    public Stream<VLSFunctionAsTerm> streamAllValuesOfterm() {
      return rawStreamAllValuesOfterm(emptyArray());
    }
    
    @Override
    protected VLSFunctionFof.Match tupleToMatch(final Tuple t) {
      try {
-          return VLSFunctionFof.Match.newMatch((ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunctionFof) t.get(POSITION_TERM));
+          return VLSFunctionFof.Match.newMatch((VLSFunctionAsTerm) t.get(POSITION_TERM));
      } catch(ClassCastException e) {
          LOGGER.error("Element(s) in tuple not properly typed!",e);
          return null;
@@ -396,7 +397,7 @@ public final class VLSFunctionFof extends BaseGeneratedEMFQuerySpecification<VLS
    @Override
    protected VLSFunctionFof.Match arrayToMatch(final Object[] match) {
      try {
-          return VLSFunctionFof.Match.newMatch((ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunctionFof) match[POSITION_TERM]);
+          return VLSFunctionFof.Match.newMatch((VLSFunctionAsTerm) match[POSITION_TERM]);
      } catch(ClassCastException e) {
          LOGGER.error("Element(s) in array not properly typed!",e);
          return null;
@@ -406,7 +407,7 @@ public final class VLSFunctionFof extends BaseGeneratedEMFQuerySpecification<VLS
    @Override
    protected VLSFunctionFof.Match arrayToMatchMutable(final Object[] match) {
      try {
-          return VLSFunctionFof.Match.newMutableMatch((ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunctionFof) match[POSITION_TERM]);
+          return VLSFunctionFof.Match.newMutableMatch((VLSFunctionAsTerm) match[POSITION_TERM]);
      } catch(ClassCastException e) {
          LOGGER.error("Element(s) in array not properly typed!",e);
          return null;
@@ -457,7 +458,7 @@ public final class VLSFunctionFof extends BaseGeneratedEMFQuerySpecification<VLS
  
  @Override
  public VLSFunctionFof.Match newMatch(final Object... parameters) {
-    return VLSFunctionFof.Match.newMatch((ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunctionFof) parameters[0]);
+    return VLSFunctionFof.Match.newMatch((ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunctionAsTerm) parameters[0]);
  }
  
  /**
@@ -489,7 +490,7 @@ public final class VLSFunctionFof extends BaseGeneratedEMFQuerySpecification<VLS
  private static class GeneratedPQuery extends BaseGeneratedEMFPQuery {
    private final static VLSFunctionFof.GeneratedPQuery INSTANCE = new GeneratedPQuery();
    
-    private final PParameter parameter_term = new PParameter("term", "ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunctionFof", new EClassTransitiveInstancesKey((EClass)getClassifierLiteralSafe("http://www.mcgill.ca/ecse/dslreasoner/VampireLanguage", "VLSFunctionFof")), PParameterDirection.INOUT);
+    private final PParameter parameter_term = new PParameter("term", "ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunctionAsTerm", new EClassTransitiveInstancesKey((EClass)getClassifierLiteralSafe("http://www.mcgill.ca/ecse/dslreasoner/VampireLanguage", "VLSFunctionAsTerm")), PParameterDirection.INOUT);
    
    private final List<PParameter> parameters = Arrays.asList(parameter_term);
    
@@ -519,12 +520,12 @@ public final class VLSFunctionFof extends BaseGeneratedEMFQuerySpecification<VLS
      {
          PBody body = new PBody(this);
          PVariable var_term = body.getOrCreateVariableByName("term");
-          new TypeConstraint(body, Tuples.flatTupleOf(var_term), new EClassTransitiveInstancesKey((EClass)getClassifierLiteral("http://www.mcgill.ca/ecse/dslreasoner/VampireLanguage", "VLSFunctionFof")));
+          new TypeConstraint(body, Tuples.flatTupleOf(var_term), new EClassTransitiveInstancesKey((EClass)getClassifierLiteral("http://www.mcgill.ca/ecse/dslreasoner/VampireLanguage", "VLSFunctionAsTerm")));
          body.setSymbolicParameters(Arrays.<ExportedParameter>asList(
             new ExportedParameter(body, var_term, parameter_term)
          ));
-          //    VLSFunctionFof(term)
+          //    VLSFunctionAsTerm(term)
-          new TypeConstraint(body, Tuples.flatTupleOf(var_term), new EClassTransitiveInstancesKey((EClass)getClassifierLiteral("http://www.mcgill.ca/ecse/dslreasoner/VampireLanguage", "VLSFunctionFof")));
+          new TypeConstraint(body, Tuples.flatTupleOf(var_term), new EClassTransitiveInstancesKey((EClass)getClassifierLiteral("http://www.mcgill.ca/ecse/dslreasoner/VampireLanguage", "VLSFunctionAsTerm")));
          bodies.add(body);
      }
      return bodies;
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.xtend
index 3c672f4b..22bd4ab5 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.xtend
@@ -1,5 +1,6 @@
 package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm
@@ -13,6 +14,7 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable
 import java.util.HashMap
+import java.util.List
 import java.util.Map
 interface Logic2VampireLanguageMapper_TypeMapperTrace {}
@@ -32,6 +34,9 @@ class Logic2VampireLanguageMapperTrace {
        public val Map<DefinedElement, VLSFunction> element2Predicate = new HashMap
        public val Map<Type, VLSTerm> type2PossibleNot = new HashMap
        public val Map<Type, VLSTerm> type2And = new HashMap
+        //Uniqueness
+        public val List<VLSConstant> uniqueInstances = newArrayList
+        
        
        public var Map<ConstantDeclaration, ConstantDefinition> constantDefinitions
        public var Map<RelationDeclaration, RelationDefinition> relationDefinitions
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend
index 4b7ea3d0..e5dfbf08 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend
@@ -19,13 +19,14 @@ class Logic2VampireLanguageMapper_ScopeMapper {
                val VLSVariable variable = createVLSVariable => [it.name = "A"]
                // 1. make a list of constants equaling the min number of specified objects
-                val List<VLSConstant> instances = newArrayList
+                val localInstances = newArrayList
                for (var i = 0; i < config.typeScopes.minNewElements; i++) {
                        val num = i + 1
                        val cst = createVLSConstant => [
                                it.name = "o" + num
                        ]
-                        instances.add(cst)
+                        trace.uniqueInstances.add(cst)
+                        localInstances.add(cst)
                }
                // TODO: specify for the max
@@ -37,14 +38,14 @@ class Logic2VampireLanguageMapper_ScopeMapper {
                                it.fofFormula = createVLSUniversalQuantifier => [
                                        it.variables += support.duplicate(variable)
                                        // check below
-                                        it.operand = createVLSEquivalent => [
+                                        it.operand = createVLSImplies => [
-                                                it.left = support.topLevelTypeFunc
+                                                it.left = support.unfoldOr(localInstances.map [ i |
-                                                it.right = support.unfoldOr(instances.map [ i |
                                                        createVLSEquality => [
                                                                it.left = createVLSVariable => [it.name = variable.name]
                                                                it.right = i
                                                        ]
                                                ])
+                                                it.right = support.topLevelTypeFunc
                                        ]
                                ]
                        ]
@@ -55,7 +56,7 @@ class Logic2VampireLanguageMapper_ScopeMapper {
                        val uniqueness = createVLSFofFormula => [
                                it.name = "typeUniqueness"
                                it.fofRole = "axiom"
-                                it.fofFormula = support.establishUniqueness(instances)
+                                it.fofFormula = support.establishUniqueness(trace.uniqueInstances)
                        ]
                        trace.specification.formulas += uniqueness
                }
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend
index d3595a73..021cb0ea 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend
@@ -2,6 +2,7 @@ package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunctionAsTerm
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSInequality
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable
@@ -36,6 +37,14 @@ class Logic2VampireLanguageMapper_Support {
        def protected VLSVariable duplicate(VLSVariable term) {
                return createVLSVariable => [it.name = term.name]
        }
+        
+        def protected VLSFunctionAsTerm duplicate(VLSFunctionAsTerm term) {
+                return createVLSFunctionAsTerm => [it.functor = term.functor]
+        }
+        
+        def protected VLSConstant duplicate(VLSConstant term) {
+                return createVLSConstant => [it.name = term.name]
+        }
        def protected VLSFunction duplicate(VLSFunction term) {
                return createVLSFunction => [
@@ -52,6 +61,19 @@ class Logic2VampireLanguageMapper_Support {
                        it.terms += duplicate(v)
                ]
        }
+        
+        def protected VLSFunction duplicate(VLSFunction term, VLSFunctionAsTerm v) {
+                return createVLSFunction => [
+                        it.constant = term.constant
+                        it.terms += duplicate(v)
+                ]
+        }
+        
+        def protected VLSConstant toConstant(VLSFunctionAsTerm term) {
+                return createVLSConstant => [
+                        it.name = term.functor
+                ]
+        }
        def protected VLSFunction topLevelTypeFunc() {
                return createVLSFunction => [
@@ -61,6 +83,13 @@ class Logic2VampireLanguageMapper_Support {
                        ]
                ]
        }
+        
+        def protected VLSFunction topLevelTypeFunc(VLSFunctionAsTerm v) {
+                return createVLSFunction => [
+                        it.constant = "object"
+                        it.terms += duplicate(v)
+                ]
+        }
        // TODO Make more general
        def establishUniqueness(List<VLSConstant> terms) {
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend
index bc0b3e23..f2a7b3f2 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend
@@ -14,8 +14,9 @@ import java.util.Collection
 import java.util.List
 import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
+import java.util.Collections
-class Logic2VampireLanguageMapper_TypeMapper  {
+class Logic2VampireLanguageMapper_TypeMapper {
        private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE
        private val Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support
        val Logic2VampireLanguageMapper base
@@ -25,8 +26,9 @@ class Logic2VampireLanguageMapper_TypeMapper  {
                this.base = base
        }
-        def protected transformTypes(Collection<Type> types, Collection<DefinedElement> elements, Logic2VampireLanguageMapper mapper, Logic2VampireLanguageMapperTrace trace) {
+        def protected transformTypes(Collection<Type> types, Collection<DefinedElement> elements,
-                
+                Logic2VampireLanguageMapper mapper, Logic2VampireLanguageMapperTrace trace) {
 //              val typeTrace = new Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes
 //              trace.typeMapperTrace = typeTrace
                val VLSVariable variable = createVLSVariable => [it.name = "A"]
@@ -86,14 +88,38 @@ class Logic2VampireLanguageMapper_TypeMapper  {
                        ]
                        trace.specification.formulas += res
+                        // Create objects for the enum elements
+                        val List<VLSFunction> enumScopeElems = newArrayList
+                        for (var i = 0; i < type.elements.length; i++) {
+                                val num = i + 1
+                                val cstTerm = createVLSFunctionAsTerm => [
+                                        it.functor = "eo" + num
+                                ]
+                                val cst = support.toConstant(cstTerm)
+                                trace.uniqueInstances.add(cst)
+                                val fct = support.duplicate(type.elements.get(i).lookup(trace.element2Predicate), cstTerm)
+                                enumScopeElems.add(fct)
+//                              enumScopeElems.add(support.topLevelTypeFunc(cstTerm))
+                        }
+                        
+                        
+                        
+                        val enumScope = createVLSFofFormula => [
+                                it.name = support.toIDMultiple("enumScope", type.name.split(" ").get(0))
+                                // below is temporary solution
+                                it.fofRole = "axiom"                    
+                                it.fofFormula = support.unfoldAnd(enumScopeElems)
+                        ]
+                        
+                        trace.specification.formulas += enumScope
                }
-                
-                //HIERARCHY HANDLER
+                // HIERARCHY HANDLER
-                
-                
                // 3. For each non-abstract type, create an and sequence containing all typedeclaration predicates
                // and store in a map
-                for (t1 : types.filter[!isIsAbstract]) {
+//              println(types.filter[!isIsAbstract])
+                for (t1 : types.filter[!isIsAbstract].filter(TypeDeclaration)) {
                        for (t2 : types) {
                                // possible improvement: check all supertypes and decide if negated or not based on negations/not negations of supertypes
                                if (t1 == t2 || support.dfsSupertypeCheck(t1, t2)) {
@@ -121,7 +147,9 @@ class Logic2VampireLanguageMapper_TypeMapper  {
                                it.operand = createVLSEquivalent => [
                                        it.left = support.topLevelTypeFunc
 //                                      it.right = support.unfoldOr(new ArrayList<VLSTerm>(typeTrace.type2And.values))
-                                        it.right = support.unfoldOr(new ArrayList<VLSTerm>(trace.type2And.values))
+                                        val reversedList = new ArrayList<VLSTerm>(trace.type2And.values)
+//                                      Collections.reverse(reversedList)
+                                        it.right = support.unfoldOr(reversedList)
                                ]
                        ]
                ]
@@ -130,7 +158,7 @@ class Logic2VampireLanguageMapper_TypeMapper  {
        }
-        //below are from previous interface
+        // below are from previous interface
        def protected transformTypeReference(Type referred, Logic2VampireLanguageMapper mapper,
                Logic2VampireLanguageMapperTrace trace) {
                throw new UnsupportedOperationException("TODO: auto-generated method stub")
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin
index e0766c08..3f204913 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin
Binary files differ
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin
index c38c96ad..10983f27 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin
Binary files differ
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin
index 2c091b47..00ebca4b 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin
Binary files differ
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin
index b05fd2c1..9641858d 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin
Binary files differ
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin
index 7f6519eb..2b51fe5d 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin
Binary files differ
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin
index d30eebe5..75482abc 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin
Binary files differ
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin
index 921b79bd..c394f878 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin
Binary files differ
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin
index 6b8d1dc0..1ec5da80 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin
Binary files differ
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin
index 83e57283..e85b5240 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin
Binary files differ
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin
index 5a0087bc..c000d128 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin
Binary files differ
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin
index 7d090297..5eb63977 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin
Binary files differ
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin
index c8ab54c2..501dbfb4 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin
Binary files differ
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin
index 3306fa73..621c888a 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin
Binary files differ
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java
index 2b491209..24df5fcd 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java
@@ -1,6 +1,7 @@
 package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder;
 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_TypeMapperTrace;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm;
@@ -14,7 +15,9 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition;
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type;
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable;
 import java.util.HashMap;
+import java.util.List;
 import java.util.Map;
+import org.eclipse.xtext.xbase.lib.CollectionLiterals;
 @SuppressWarnings("all")
 public class Logic2VampireLanguageMapperTrace {
@@ -34,6 +37,8 @@ public class Logic2VampireLanguageMapperTrace {
  
  public final Map<Type, VLSTerm> type2And = new HashMap<Type, VLSTerm>();
  
+  public final List<VLSConstant> uniqueInstances = CollectionLiterals.<VLSConstant>newArrayList();
+  
  public Map<ConstantDeclaration, ConstantDefinition> constantDefinitions;
  
  public Map<RelationDeclaration, RelationDefinition> relationDefinitions;
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java
index 8967839d..15ba78c9 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java
@@ -5,13 +5,14 @@ import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguage
 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquality;
-import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquivalent;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory;
 import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration;
-import java.util.List;
+import java.util.ArrayList;
 import org.eclipse.emf.common.util.EList;
 import org.eclipse.xtext.xbase.lib.CollectionLiterals;
 import org.eclipse.xtext.xbase.lib.Extension;
@@ -39,7 +40,7 @@ public class Logic2VampireLanguageMapper_ScopeMapper {
      it.setName("A");
    };
    final VLSVariable variable = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function);
-    final List<VLSConstant> instances = CollectionLiterals.<VLSConstant>newArrayList();
+    final ArrayList<VLSTerm> localInstances = CollectionLiterals.<VLSTerm>newArrayList();
    for (int i = 0; (i < config.typeScopes.minNewElements); i++) {
      {
        final int num = (i + 1);
@@ -48,7 +49,8 @@ public class Logic2VampireLanguageMapper_ScopeMapper {
          it.setName(("o" + Integer.valueOf(num)));
        };
        final VLSConstant cst = ObjectExtensions.<VLSConstant>operator_doubleArrow(_createVLSConstant, _function_1);
-        instances.add(cst);
+        trace.uniqueInstances.add(cst);
+        localInstances.add(cst);
      }
    }
    if ((config.typeScopes.minNewElements != 0)) {
@@ -61,10 +63,9 @@ public class Logic2VampireLanguageMapper_ScopeMapper {
          EList<VLSVariable> _variables = it_1.getVariables();
          VLSVariable _duplicate = this.support.duplicate(variable);
          _variables.add(_duplicate);
-          VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent();
+          VLSImplies _createVLSImplies = this.factory.createVLSImplies();
-          final Procedure1<VLSEquivalent> _function_3 = (VLSEquivalent it_2) -> {
+          final Procedure1<VLSImplies> _function_3 = (VLSImplies it_2) -> {
-            it_2.setLeft(this.support.topLevelTypeFunc());
+            final Function1<VLSTerm, VLSEquality> _function_4 = (VLSTerm i) -> {
-            final Function1<VLSConstant, VLSEquality> _function_4 = (VLSConstant i) -> {
              VLSEquality _createVLSEquality = this.factory.createVLSEquality();
              final Procedure1<VLSEquality> _function_5 = (VLSEquality it_3) -> {
                VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable();
@@ -77,9 +78,10 @@ public class Logic2VampireLanguageMapper_ScopeMapper {
              };
              return ObjectExtensions.<VLSEquality>operator_doubleArrow(_createVLSEquality, _function_5);
            };
-            it_2.setRight(this.support.unfoldOr(ListExtensions.<VLSConstant, VLSEquality>map(instances, _function_4)));
+            it_2.setLeft(this.support.unfoldOr(ListExtensions.<VLSTerm, VLSEquality>map(localInstances, _function_4)));
+            it_2.setRight(this.support.topLevelTypeFunc());
          };
-          VLSEquivalent _doubleArrow = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_3);
+          VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_3);
          it_1.setOperand(_doubleArrow);
        };
        VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_2);
@@ -92,7 +94,7 @@ public class Logic2VampireLanguageMapper_ScopeMapper {
      final Procedure1<VLSFofFormula> _function_2 = (VLSFofFormula it) -> {
        it.setName("typeUniqueness");
        it.setFofRole("axiom");
-        it.setFofFormula(this.support.establishUniqueness(instances));
+        it.setFofFormula(this.support.establishUniqueness(trace.uniqueInstances));
      };
      final VLSFofFormula uniqueness = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula_1, _function_2);
      EList<VLSFofFormula> _formulas_1 = trace.specification.getFormulas();
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java
index 72ca44e9..e2ff7a0e 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java
@@ -6,6 +6,7 @@ import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSAnd;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSExistentialQuantifier;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunctionAsTerm;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSInequality;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSOr;
@@ -62,6 +63,22 @@ public class Logic2VampireLanguageMapper_Support {
    return ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function);
  }
  
+  protected VLSFunctionAsTerm duplicate(final VLSFunctionAsTerm term) {
+    VLSFunctionAsTerm _createVLSFunctionAsTerm = this.factory.createVLSFunctionAsTerm();
+    final Procedure1<VLSFunctionAsTerm> _function = (VLSFunctionAsTerm it) -> {
+      it.setFunctor(term.getFunctor());
+    };
+    return ObjectExtensions.<VLSFunctionAsTerm>operator_doubleArrow(_createVLSFunctionAsTerm, _function);
+  }
+  
+  protected VLSConstant duplicate(final VLSConstant term) {
+    VLSConstant _createVLSConstant = this.factory.createVLSConstant();
+    final Procedure1<VLSConstant> _function = (VLSConstant it) -> {
+      it.setName(term.getName());
+    };
+    return ObjectExtensions.<VLSConstant>operator_doubleArrow(_createVLSConstant, _function);
+  }
+  
  protected VLSFunction duplicate(final VLSFunction term) {
    VLSFunction _createVLSFunction = this.factory.createVLSFunction();
    final Procedure1<VLSFunction> _function = (VLSFunction it) -> {
@@ -87,6 +104,25 @@ public class Logic2VampireLanguageMapper_Support {
    return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function);
  }
  
+  protected VLSFunction duplicate(final VLSFunction term, final VLSFunctionAsTerm v) {
+    VLSFunction _createVLSFunction = this.factory.createVLSFunction();
+    final Procedure1<VLSFunction> _function = (VLSFunction it) -> {
+      it.setConstant(term.getConstant());
+      EList<VLSTerm> _terms = it.getTerms();
+      VLSFunctionAsTerm _duplicate = this.duplicate(v);
+      _terms.add(_duplicate);
+    };
+    return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function);
+  }
+  
+  protected VLSConstant toConstant(final VLSFunctionAsTerm term) {
+    VLSConstant _createVLSConstant = this.factory.createVLSConstant();
+    final Procedure1<VLSConstant> _function = (VLSConstant it) -> {
+      it.setName(term.getFunctor());
+    };
+    return ObjectExtensions.<VLSConstant>operator_doubleArrow(_createVLSConstant, _function);
+  }
+  
  protected VLSFunction topLevelTypeFunc() {
    VLSFunction _createVLSFunction = this.factory.createVLSFunction();
    final Procedure1<VLSFunction> _function = (VLSFunction it) -> {
@@ -102,6 +138,17 @@ public class Logic2VampireLanguageMapper_Support {
    return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function);
  }
  
+  protected VLSFunction topLevelTypeFunc(final VLSFunctionAsTerm v) {
+    VLSFunction _createVLSFunction = this.factory.createVLSFunction();
+    final Procedure1<VLSFunction> _function = (VLSFunction it) -> {
+      it.setConstant("object");
+      EList<VLSTerm> _terms = it.getTerms();
+      VLSFunctionAsTerm _duplicate = this.duplicate(v);
+      _terms.add(_duplicate);
+    };
+    return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function);
+  }
+  
  public VLSTerm establishUniqueness(final List<VLSConstant> terms) {
    final List<VLSInequality> eqs = CollectionLiterals.<VLSInequality>newArrayList();
    List<VLSConstant> _subList = terms.subList(1, ((Object[])Conversions.unwrapArray(terms, Object.class)).length);
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java
index d3dddcfc..f776371b 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java
@@ -3,10 +3,12 @@ package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder;
 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper;
 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace;
 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSDoubleQuote;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquivalent;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunctionAsTerm;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUnaryNegation;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier;
@@ -16,6 +18,7 @@ import com.google.common.base.Objects;
 import com.google.common.collect.Iterables;
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement;
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type;
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration;
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition;
 import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage;
 import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil;
@@ -24,6 +27,7 @@ import java.util.Collection;
 import java.util.List;
 import org.eclipse.emf.common.util.EList;
 import org.eclipse.xtext.xbase.lib.CollectionLiterals;
+import org.eclipse.xtext.xbase.lib.Conversions;
 import org.eclipse.xtext.xbase.lib.Extension;
 import org.eclipse.xtext.xbase.lib.Functions.Function1;
 import org.eclipse.xtext.xbase.lib.IterableExtensions;
@@ -107,14 +111,38 @@ public class Logic2VampireLanguageMapper_TypeMapper {
          final VLSFofFormula res = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_1);
          EList<VLSFofFormula> _formulas = trace.specification.getFormulas();
          _formulas.add(res);
+          final List<VLSFunction> enumScopeElems = CollectionLiterals.<VLSFunction>newArrayList();
+          for (int i = 0; (i < ((Object[])Conversions.unwrapArray(type_1.getElements(), Object.class)).length); i++) {
+            {
+              final int num = (i + 1);
+              VLSFunctionAsTerm _createVLSFunctionAsTerm = this.factory.createVLSFunctionAsTerm();
+              final Procedure1<VLSFunctionAsTerm> _function_2 = (VLSFunctionAsTerm it) -> {
+                it.setFunctor(("eo" + Integer.valueOf(num)));
+              };
+              final VLSFunctionAsTerm cstTerm = ObjectExtensions.<VLSFunctionAsTerm>operator_doubleArrow(_createVLSFunctionAsTerm, _function_2);
+              final VLSConstant cst = this.support.toConstant(cstTerm);
+              trace.uniqueInstances.add(cst);
+              final VLSFunction fct = this.support.duplicate(CollectionsUtil.<DefinedElement, VLSFunction>lookup(type_1.getElements().get(i), trace.element2Predicate), cstTerm);
+              enumScopeElems.add(fct);
+            }
+          }
+          VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula();
+          final Procedure1<VLSFofFormula> _function_2 = (VLSFofFormula it) -> {
+            it.setName(this.support.toIDMultiple("enumScope", type_1.getName().split(" ")[0]));
+            it.setFofRole("axiom");
+            it.setFofFormula(this.support.unfoldAnd(enumScopeElems));
+          };
+          final VLSFofFormula enumScope = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula_1, _function_2);
+          EList<VLSFofFormula> _formulas_1 = trace.specification.getFormulas();
+          _formulas_1.add(enumScope);
        }
      }
      final Function1<Type, Boolean> _function_1 = (Type it) -> {
        boolean _isIsAbstract = it.isIsAbstract();
        return Boolean.valueOf((!_isIsAbstract));
      };
-      Iterable<Type> _filter_1 = IterableExtensions.<Type>filter(types, _function_1);
+      Iterable<TypeDeclaration> _filter_1 = Iterables.<TypeDeclaration>filter(IterableExtensions.<Type>filter(types, _function_1), TypeDeclaration.class);
-      for (final Type t1 : _filter_1) {
+      for (final TypeDeclaration t1 : _filter_1) {
        {
          for (final Type t2 : types) {
            if ((Objects.equal(t1, t2) || this.support.dfsSupertypeCheck(t1, t2))) {
@@ -147,8 +175,8 @@ public class Logic2VampireLanguageMapper_TypeMapper {
          final Procedure1<VLSEquivalent> _function_4 = (VLSEquivalent it_2) -> {
            it_2.setLeft(this.support.topLevelTypeFunc());
            Collection<VLSTerm> _values = trace.type2And.values();
-            ArrayList<VLSTerm> _arrayList = new ArrayList<VLSTerm>(_values);
+            final ArrayList<VLSTerm> reversedList = new ArrayList<VLSTerm>(_values);
-            it_2.setRight(this.support.unfoldOr(_arrayList));
+            it_2.setRight(this.support.unfoldOr(reversedList));
          };
          VLSEquivalent _doubleArrow = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_4);
          it_1.setOperand(_doubleArrow);