Begin handing of scope and fix type definitions.

65 files changed, 607 insertions, 870 deletions

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/src-gen/ca/mcgill/ecse/dslreasoner/ide/contentassist/antlr/VampireLanguageParser.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/src-gen/ca/mcgill/ecse/dslreasoner/ide/contentassist/antlr/VampireLanguageParser.java
index 831cde0b..9004026e 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/src-gen/ca/mcgill/ecse/dslreasoner/ide/contentassist/antlr/VampireLanguageParser.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/src-gen/ca/mcgill/ecse/dslreasoner/ide/contentassist/antlr/VampireLanguageParser.java
@@ -54,8 +54,6 @@ public class VampireLanguageParser extends AbstractContentAssistParser {
                                         put(grammarAccess.getVLSIncludeAccess().getGroup_2_2(), "rule__VLSInclude__Group_2_2__0");

                                         put(grammarAccess.getVLSCommentAccess().getGroup(), "rule__VLSComment__Group__0");

                                         put(grammarAccess.getVLSSatisfiableAccess().getGroup(), "rule__VLSSatisfiable__Group__0");

-                                        put(grammarAccess.getVLSTryingAccess().getGroup(), "rule__VLSTrying__Group__0");

-                                        put(grammarAccess.getVLSFiniteModelAccess().getGroup(), "rule__VLSFiniteModel__Group__0");

                                         put(grammarAccess.getVLSFofFormulaAccess().getGroup(), "rule__VLSFofFormula__Group__0");

                                         put(grammarAccess.getVLSFofFormulaAccess().getGroup_7(), "rule__VLSFofFormula__Group_7__0");

                                         put(grammarAccess.getVLSTffFormulaAccess().getGroup(), "rule__VLSTffFormula__Group__0");

@@ -111,7 +109,6 @@ public class VampireLanguageParser extends AbstractContentAssistParser {
                                         put(grammarAccess.getVLSIncludeAccess().getNamesAssignment_2_2_1(), "rule__VLSInclude__NamesAssignment_2_2_1");

                                         put(grammarAccess.getVLSNameAccess().getNameAssignment(), "rule__VLSName__NameAssignment");

                                         put(grammarAccess.getVLSCommentAccess().getCommentAssignment_1(), "rule__VLSComment__CommentAssignment_1");

-                                        put(grammarAccess.getVLSTryingAccess().getNameAssignment_2(), "rule__VLSTrying__NameAssignment_2");

                                         put(grammarAccess.getVLSFofFormulaAccess().getNameAssignment_2(), "rule__VLSFofFormula__NameAssignment_2");

                                         put(grammarAccess.getVLSFofFormulaAccess().getFofRoleAssignment_4(), "rule__VLSFofFormula__FofRoleAssignment_4");

                                         put(grammarAccess.getVLSFofFormulaAccess().getFofFormulaAssignment_6(), "rule__VLSFofFormula__FofFormulaAssignment_6");

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeModule.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeModule.xtendbin
index edf76642..7bfd4e09 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeModule.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeModule.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeSetup.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeSetup.xtendbin
index acb28f52..4c4cd6a3 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeSetup.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeSetup.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/src-gen/ca/mcgill/ecse/dslreasoner/ui/contentassist/AbstractVampireLanguageProposalProvider.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/src-gen/ca/mcgill/ecse/dslreasoner/ui/contentassist/AbstractVampireLanguageProposalProvider.java
index 90b81dcb..aead1baf 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/src-gen/ca/mcgill/ecse/dslreasoner/ui/contentassist/AbstractVampireLanguageProposalProvider.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/src-gen/ca/mcgill/ecse/dslreasoner/ui/contentassist/AbstractVampireLanguageProposalProvider.java
@@ -48,9 +48,6 @@ public abstract class AbstractVampireLanguageProposalProvider extends TerminalsP
         public void completeVLSComment_Comment(EObject model, Assignment assignment, ContentAssistContext context, ICompletionProposalAcceptor acceptor) {

                 completeRuleCall(((RuleCall)assignment.getTerminal()), context, acceptor);

         }

-        public void completeVLSTrying_Name(EObject model, Assignment assignment, ContentAssistContext context, ICompletionProposalAcceptor acceptor) {

-                completeRuleCall(((RuleCall)assignment.getTerminal()), context, acceptor);

-        }

         public void completeVLSFofFormula_Name(EObject model, Assignment assignment, ContentAssistContext context, ICompletionProposalAcceptor acceptor) {

                 completeRuleCall(((RuleCall)((Alternatives)assignment.getTerminal()).getElements().get(0)), context, acceptor);

                 completeRuleCall(((RuleCall)((Alternatives)assignment.getTerminal()).getElements().get(1)), context, acceptor);

@@ -219,12 +216,6 @@ public abstract class AbstractVampireLanguageProposalProvider extends TerminalsP
         public void complete_VLSSatisfiable(EObject model, RuleCall ruleCall, ContentAssistContext context, ICompletionProposalAcceptor acceptor) {

                 // subclasses may override

         }

-        public void complete_VLSTrying(EObject model, RuleCall ruleCall, ContentAssistContext context, ICompletionProposalAcceptor acceptor) {

-                // subclasses may override

-        }

-        public void complete_VLSFiniteModel(EObject model, RuleCall ruleCall, ContentAssistContext context, ICompletionProposalAcceptor acceptor) {

-                // subclasses may override

-        }

         public void complete_VLSFofFormula(EObject model, RuleCall ruleCall, ContentAssistContext context, ICompletionProposalAcceptor acceptor) {

                 // subclasses may override

         }

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/.VampireLanguageUiModule.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/.VampireLanguageUiModule.xtendbin
index 050d1635..dedb3ece 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/.VampireLanguageUiModule.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/.VampireLanguageUiModule.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/contentassist/.VampireLanguageProposalProvider.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/contentassist/.VampireLanguageProposalProvider.xtendbin
index ad8d105e..a6d502ef 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/contentassist/.VampireLanguageProposalProvider.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/contentassist/.VampireLanguageProposalProvider.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageDescriptionLabelProvider.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageDescriptionLabelProvider.xtendbin
index 070441a8..b2dc17a0 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageDescriptionLabelProvider.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageDescriptionLabelProvider.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageLabelProvider.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageLabelProvider.xtendbin
index c453602a..73d9cdd1 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageLabelProvider.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageLabelProvider.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/outline/.VampireLanguageOutlineTreeProvider.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/outline/.VampireLanguageOutlineTreeProvider.xtendbin
index 396972da..7880fdd6 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/outline/.VampireLanguageOutlineTreeProvider.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/outline/.VampireLanguageOutlineTreeProvider.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/quickfix/.VampireLanguageQuickfixProvider.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/quickfix/.VampireLanguageQuickfixProvider.xtendbin
index f0fe0710..6a8836d4 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/quickfix/.VampireLanguageQuickfixProvider.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/quickfix/.VampireLanguageQuickfixProvider.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/model/generated/VampireLanguage.ecore b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/model/generated/VampireLanguage.ecore
index fcfb84c7..ff954f57 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/model/generated/VampireLanguage.ecore
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/model/generated/VampireLanguage.ecore
@@ -27,10 +27,6 @@
   </eClassifiers>

   <eClassifiers xsi:type="ecore:EClass" name="VLSConfirmations"/>

   <eClassifiers xsi:type="ecore:EClass" name="VLSSatisfiable" eSuperTypes="#//VLSConfirmations"/>

-  <eClassifiers xsi:type="ecore:EClass" name="VLSTrying">

-    <eStructuralFeatures xsi:type="ecore:EAttribute" name="name" eType="ecore:EDataType http://www.eclipse.org/emf/2002/Ecore#//EString"/>

-  </eClassifiers>

-  <eClassifiers xsi:type="ecore:EClass" name="VLSFiniteModel"/>

   <eClassifiers xsi:type="ecore:EClass" name="VLSFofFormula">

     <eStructuralFeatures xsi:type="ecore:EAttribute" name="name" eType="ecore:EDataType http://www.eclipse.org/emf/2002/Ecore#//EString"/>

     <eStructuralFeatures xsi:type="ecore:EAttribute" name="fofRole" eType="ecore:EDataType http://www.eclipse.org/emf/2002/Ecore#//EString"/>

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/model/generated/VampireLanguage.genmodel b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/model/generated/VampireLanguage.genmodel
index ce5d9184..655f282b 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/model/generated/VampireLanguage.genmodel
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/model/generated/VampireLanguage.genmodel
@@ -25,10 +25,6 @@
     </genClasses>

     <genClasses ecoreClass="VampireLanguage.ecore#//VLSConfirmations"/>

     <genClasses ecoreClass="VampireLanguage.ecore#//VLSSatisfiable"/>

-    <genClasses ecoreClass="VampireLanguage.ecore#//VLSTrying">

-      <genFeatures createChild="false" ecoreFeature="ecore:EAttribute VampireLanguage.ecore#//VLSTrying/name"/>

-    </genClasses>

-    <genClasses ecoreClass="VampireLanguage.ecore#//VLSFiniteModel"/>

     <genClasses ecoreClass="VampireLanguage.ecore#//VLSFofFormula">

       <genFeatures createChild="false" ecoreFeature="ecore:EAttribute VampireLanguage.ecore#//VLSFofFormula/name"/>

       <genFeatures createChild="false" ecoreFeature="ecore:EAttribute VampireLanguage.ecore#//VLSFofFormula/fofRole"/>

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/VampireLanguage.xtextbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/VampireLanguage.xtextbin
index ddc983a6..337977f1 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/VampireLanguage.xtextbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/VampireLanguage.xtextbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/serializer/VampireLanguageSemanticSequencer.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/serializer/VampireLanguageSemanticSequencer.java
index d763a193..890341db 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/serializer/VampireLanguageSemanticSequencer.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/serializer/VampireLanguageSemanticSequencer.java
@@ -14,7 +14,6 @@ import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquality;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquivalent;

 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSExistentialQuantifier;

 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFalse;

-import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFiniteModel;

 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula;

 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction;

 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunctionFof;

@@ -33,7 +32,6 @@ import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSRevImplies;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSSatisfiable;

 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTffFormula;

 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTrue;

-import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTrying;

 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUnaryNegation;

 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier;

 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable;

@@ -103,9 +101,6 @@ public class VampireLanguageSemanticSequencer extends AbstractDelegatingSemantic
                         case VampireLanguagePackage.VLS_FALSE:

                                 sequence_VLSAtomicConstant(context, (VLSFalse) semanticObject); 

                                 return; 

-                        case VampireLanguagePackage.VLS_FINITE_MODEL:

-                                sequence_VLSFiniteModel(context, (VLSFiniteModel) semanticObject); 

-                                return; 

                         case VampireLanguagePackage.VLS_FOF_FORMULA:

                                 sequence_VLSFofFormula(context, (VLSFofFormula) semanticObject); 

                                 return; 

@@ -160,9 +155,6 @@ public class VampireLanguageSemanticSequencer extends AbstractDelegatingSemantic
                         case VampireLanguagePackage.VLS_TRUE:

                                 sequence_VLSAtomicConstant(context, (VLSTrue) semanticObject); 

                                 return; 

-                        case VampireLanguagePackage.VLS_TRYING:

-                                sequence_VLSTrying(context, (VLSTrying) semanticObject); 

-                                return; 

                         case VampireLanguagePackage.VLS_UNARY_NEGATION:

                                 sequence_VLSUnaryNegation(context, (VLSUnaryNegation) semanticObject); 

                                 return; 

@@ -782,18 +774,6 @@ public class VampireLanguageSemanticSequencer extends AbstractDelegatingSemantic
         

         /**

          * Contexts:

-         *     VLSFiniteModel returns VLSFiniteModel

-         *

-         * Constraint:

-         *     {VLSFiniteModel}

-         */

-        protected void sequence_VLSFiniteModel(ISerializationContext context, VLSFiniteModel semanticObject) {

-                genericSequencer.createSequence(context, semanticObject);

-        }

-        

-        

-        /**

-         * Contexts:

          *     VLSFofFormula returns VLSFofFormula

          *

          * Constraint:

@@ -868,24 +848,6 @@ public class VampireLanguageSemanticSequencer extends AbstractDelegatingSemantic
         

         /**

          * Contexts:

-         *     VLSTrying returns VLSTrying

-         *

-         * Constraint:

-         *     name=LITERAL

-         */

-        protected void sequence_VLSTrying(ISerializationContext context, VLSTrying semanticObject) {

-                if (errorAcceptor != null) {

-                        if (transientValues.isValueTransient(semanticObject, VampireLanguagePackage.Literals.VLS_TRYING__NAME) == ValueTransient.YES)

-                                errorAcceptor.accept(diagnosticProvider.createFeatureValueMissing(semanticObject, VampireLanguagePackage.Literals.VLS_TRYING__NAME));

-                }

-                SequenceFeeder feeder = createSequencerFeeder(context, semanticObject);

-                feeder.accept(grammarAccess.getVLSTryingAccess().getNameLITERALTerminalRuleCall_2_0(), semanticObject.getName());

-                feeder.finish();

-        }

-        

-        

-        /**

-         * Contexts:

          *     VLSTerm returns VLSAssignment

          *     VLSBinary returns VLSAssignment

          *     VLSBinary.VLSEquivalent_1_0_0_0_0 returns VLSAssignment

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/services/VampireLanguageGrammarAccess.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/services/VampireLanguageGrammarAccess.java
index 64ba160f..c5bd8be2 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/services/VampireLanguageGrammarAccess.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/services/VampireLanguageGrammarAccess.java
@@ -234,64 +234,6 @@ public class VampireLanguageGrammarAccess extends AbstractGrammarElementFinder {
                 //'Satisfiable!'

                 public Keyword getSatisfiableKeyword_1() { return cSatisfiableKeyword_1; }

         }

-        public class VLSTryingElements extends AbstractParserRuleElementFinder {

-                private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSTrying");

-                private final Group cGroup = (Group)rule.eContents().get(1);

-                private final Keyword cTRYINGKeyword_0 = (Keyword)cGroup.eContents().get(0);

-                private final Keyword cLeftSquareBracketKeyword_1 = (Keyword)cGroup.eContents().get(1);

-                private final Assignment cNameAssignment_2 = (Assignment)cGroup.eContents().get(2);

-                private final RuleCall cNameLITERALTerminalRuleCall_2_0 = (RuleCall)cNameAssignment_2.eContents().get(0);

-                private final Keyword cRightSquareBracketKeyword_3 = (Keyword)cGroup.eContents().get(3);

-                

-                //VLSTrying:

-                //      'TRYING' '[' name=LITERAL ']';

-                @Override public ParserRule getRule() { return rule; }

-                

-                //'TRYING' '[' name=LITERAL ']'

-                public Group getGroup() { return cGroup; }

-                

-                //'TRYING'

-                public Keyword getTRYINGKeyword_0() { return cTRYINGKeyword_0; }

-                

-                //'['

-                public Keyword getLeftSquareBracketKeyword_1() { return cLeftSquareBracketKeyword_1; }

-                

-                //name=LITERAL

-                public Assignment getNameAssignment_2() { return cNameAssignment_2; }

-                

-                //LITERAL

-                public RuleCall getNameLITERALTerminalRuleCall_2_0() { return cNameLITERALTerminalRuleCall_2_0; }

-                

-                //']'

-                public Keyword getRightSquareBracketKeyword_3() { return cRightSquareBracketKeyword_3; }

-        }

-        public class VLSFiniteModelElements extends AbstractParserRuleElementFinder {

-                private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSFiniteModel");

-                private final Group cGroup = (Group)rule.eContents().get(1);

-                private final Action cVLSFiniteModelAction_0 = (Action)cGroup.eContents().get(0);

-                private final Keyword cFiniteKeyword_1 = (Keyword)cGroup.eContents().get(1);

-                private final Keyword cModelKeyword_2 = (Keyword)cGroup.eContents().get(2);

-                private final Keyword cFoundKeyword_3 = (Keyword)cGroup.eContents().get(3);

-                

-                //VLSFiniteModel:

-                //      {VLSFiniteModel} 'Finite' 'Model' 'Found!';

-                @Override public ParserRule getRule() { return rule; }

-                

-                //{VLSFiniteModel} 'Finite' 'Model' 'Found!'

-                public Group getGroup() { return cGroup; }

-                

-                //{VLSFiniteModel}

-                public Action getVLSFiniteModelAction_0() { return cVLSFiniteModelAction_0; }

-                

-                //'Finite'

-                public Keyword getFiniteKeyword_1() { return cFiniteKeyword_1; }

-                

-                //'Model'

-                public Keyword getModelKeyword_2() { return cModelKeyword_2; }

-                

-                //'Found!'

-                public Keyword getFoundKeyword_3() { return cFoundKeyword_3; }

-        }

         public class VLSFofFormulaElements extends AbstractParserRuleElementFinder {

                 private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSFofFormula");

                 private final Group cGroup = (Group)rule.eContents().get(1);

@@ -315,6 +257,13 @@ public class VampireLanguageGrammarAccess extends AbstractGrammarElementFinder {
                 private final Keyword cRightParenthesisKeyword_8 = (Keyword)cGroup.eContents().get(8);

                 private final Keyword cFullStopKeyword_9 = (Keyword)cGroup.eContents().get(9);

                 

+                ////VLSTrying:

+                ////    'TRYING' '[' name = LITERAL ']'

+                ////;

+                ////

+                ////VLSFiniteModel:

+                ////    {VLSFiniteModel} 'Finite' 'Model' 'Found!'

+                ////;

                 //// <FOF formulas>

                 //VLSFofFormula:

                 //      'fof' '(' name=(LOWER_WORD_ID | SIGNED_LITERAL | SINGLE_QUOTE) ',' fofRole=VLSRole ',' fofFormula=VLSTerm (','

@@ -1633,8 +1582,6 @@ public class VampireLanguageGrammarAccess extends AbstractGrammarElementFinder {
         private final VLSCommentElements pVLSComment;

         private final VLSConfirmationsElements pVLSConfirmations;

         private final VLSSatisfiableElements pVLSSatisfiable;

-        private final VLSTryingElements pVLSTrying;

-        private final VLSFiniteModelElements pVLSFiniteModel;

         private final VLSFofFormulaElements pVLSFofFormula;

         private final VLSTffFormulaElements pVLSTffFormula;

         private final VLSRoleElements pVLSRole;

@@ -1688,8 +1635,6 @@ public class VampireLanguageGrammarAccess extends AbstractGrammarElementFinder {
                 this.pVLSComment = new VLSCommentElements();

                 this.pVLSConfirmations = new VLSConfirmationsElements();

                 this.pVLSSatisfiable = new VLSSatisfiableElements();

-                this.pVLSTrying = new VLSTryingElements();

-                this.pVLSFiniteModel = new VLSFiniteModelElements();

                 this.pVLSFofFormula = new VLSFofFormulaElements();

                 this.pVLSTffFormula = new VLSTffFormulaElements();

                 this.pVLSRole = new VLSRoleElements();

@@ -1922,26 +1867,13 @@ public class VampireLanguageGrammarAccess extends AbstractGrammarElementFinder {
                 return getVLSSatisfiableAccess().getRule();

         }

         

-        //VLSTrying:

-        //      'TRYING' '[' name=LITERAL ']';

-        public VLSTryingElements getVLSTryingAccess() {

-                return pVLSTrying;

-        }

-        

-        public ParserRule getVLSTryingRule() {

-                return getVLSTryingAccess().getRule();

-        }

-        

-        //VLSFiniteModel:

-        //      {VLSFiniteModel} 'Finite' 'Model' 'Found!';

-        public VLSFiniteModelElements getVLSFiniteModelAccess() {

-                return pVLSFiniteModel;

-        }

-        

-        public ParserRule getVLSFiniteModelRule() {

-                return getVLSFiniteModelAccess().getRule();

-        }

-        

+        ////VLSTrying:

+        ////    'TRYING' '[' name = LITERAL ']'

+        ////;

+        ////

+        ////VLSFiniteModel:

+        ////    {VLSFiniteModel} 'Finite' 'Model' 'Found!'

+        ////;

         //// <FOF formulas>

         //VLSFofFormula:

         //      'fof' '(' name=(LOWER_WORD_ID | SIGNED_LITERAL | SINGLE_QUOTE) ',' fofRole=VLSRole ',' fofFormula=VLSTerm (','

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/VampireLanguageFactory.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/VampireLanguageFactory.java
index a89885ee..84b65a59 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/VampireLanguageFactory.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/VampireLanguageFactory.java
@@ -78,24 +78,6 @@ public interface VampireLanguageFactory extends EFactory
   VLSSatisfiable createVLSSatisfiable();

 

   /**

-   * Returns a new object of class '<em>VLS Trying</em>'.

-   * <!-- begin-user-doc -->

-   * <!-- end-user-doc -->

-   * @return a new object of class '<em>VLS Trying</em>'.

-   * @generated

-   */

-  VLSTrying createVLSTrying();

-

-  /**

-   * Returns a new object of class '<em>VLS Finite Model</em>'.

-   * <!-- begin-user-doc -->

-   * <!-- end-user-doc -->

-   * @return a new object of class '<em>VLS Finite Model</em>'.

-   * @generated

-   */

-  VLSFiniteModel createVLSFiniteModel();

-

-  /**

    * Returns a new object of class '<em>VLS Fof Formula</em>'.

    * <!-- begin-user-doc -->

    * <!-- end-user-doc -->

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/VampireLanguagePackage.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/VampireLanguagePackage.java
index a9334a48..e7df5378 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/VampireLanguagePackage.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/VampireLanguagePackage.java
@@ -253,53 +253,6 @@ public interface VampireLanguagePackage extends EPackage
   int VLS_SATISFIABLE_FEATURE_COUNT = VLS_CONFIRMATIONS_FEATURE_COUNT + 0;

 

   /**

-   * The meta object id for the '{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSTryingImpl <em>VLS Trying</em>}' class.

-   * <!-- begin-user-doc -->

-   * <!-- end-user-doc -->

-   * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSTryingImpl

-   * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSTrying()

-   * @generated

-   */

-  int VLS_TRYING = 6;

-

-  /**

-   * The feature id for the '<em><b>Name</b></em>' attribute.

-   * <!-- begin-user-doc -->

-   * <!-- end-user-doc -->

-   * @generated

-   * @ordered

-   */

-  int VLS_TRYING__NAME = 0;

-

-  /**

-   * The number of structural features of the '<em>VLS Trying</em>' class.

-   * <!-- begin-user-doc -->

-   * <!-- end-user-doc -->

-   * @generated

-   * @ordered

-   */

-  int VLS_TRYING_FEATURE_COUNT = 1;

-

-  /**

-   * The meta object id for the '{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSFiniteModelImpl <em>VLS Finite Model</em>}' class.

-   * <!-- begin-user-doc -->

-   * <!-- end-user-doc -->

-   * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSFiniteModelImpl

-   * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSFiniteModel()

-   * @generated

-   */

-  int VLS_FINITE_MODEL = 7;

-

-  /**

-   * The number of structural features of the '<em>VLS Finite Model</em>' class.

-   * <!-- begin-user-doc -->

-   * <!-- end-user-doc -->

-   * @generated

-   * @ordered

-   */

-  int VLS_FINITE_MODEL_FEATURE_COUNT = 0;

-

-  /**

    * The meta object id for the '{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSFofFormulaImpl <em>VLS Fof Formula</em>}' class.

    * <!-- begin-user-doc -->

    * <!-- end-user-doc -->

@@ -307,7 +260,7 @@ public interface VampireLanguagePackage extends EPackage
    * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSFofFormula()

    * @generated

    */

-  int VLS_FOF_FORMULA = 8;

+  int VLS_FOF_FORMULA = 6;

 

   /**

    * The feature id for the '<em><b>Name</b></em>' attribute.

@@ -362,7 +315,7 @@ public interface VampireLanguagePackage extends EPackage
    * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSTffFormula()

    * @generated

    */

-  int VLS_TFF_FORMULA = 9;

+  int VLS_TFF_FORMULA = 7;

 

   /**

    * The feature id for the '<em><b>Name</b></em>' attribute.

@@ -417,7 +370,7 @@ public interface VampireLanguagePackage extends EPackage
    * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSAnnotation()

    * @generated

    */

-  int VLS_ANNOTATION = 10;

+  int VLS_ANNOTATION = 8;

 

   /**

    * The feature id for the '<em><b>Name</b></em>' attribute.

@@ -463,7 +416,7 @@ public interface VampireLanguagePackage extends EPackage
    * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSTerm()

    * @generated

    */

-  int VLS_TERM = 11;

+  int VLS_TERM = 9;

 

   /**

    * The number of structural features of the '<em>VLS Term</em>' class.

@@ -482,7 +435,7 @@ public interface VampireLanguagePackage extends EPackage
    * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSVariable()

    * @generated

    */

-  int VLS_VARIABLE = 12;

+  int VLS_VARIABLE = 10;

 

   /**

    * The feature id for the '<em><b>Name</b></em>' attribute.

@@ -510,7 +463,7 @@ public interface VampireLanguagePackage extends EPackage
    * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSFunctionFof()

    * @generated

    */

-  int VLS_FUNCTION_FOF = 13;

+  int VLS_FUNCTION_FOF = 11;

 

   /**

    * The feature id for the '<em><b>Functor</b></em>' attribute.

@@ -547,7 +500,7 @@ public interface VampireLanguagePackage extends EPackage
    * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSDefinedTerm()

    * @generated

    */

-  int VLS_DEFINED_TERM = 14;

+  int VLS_DEFINED_TERM = 12;

 

   /**

    * The feature id for the '<em><b>Value</b></em>' attribute.

@@ -575,7 +528,7 @@ public interface VampireLanguagePackage extends EPackage
    * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSEquivalent()

    * @generated

    */

-  int VLS_EQUIVALENT = 15;

+  int VLS_EQUIVALENT = 13;

 

   /**

    * The feature id for the '<em><b>Left</b></em>' containment reference.

@@ -612,7 +565,7 @@ public interface VampireLanguagePackage extends EPackage
    * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSImplies()

    * @generated

    */

-  int VLS_IMPLIES = 16;

+  int VLS_IMPLIES = 14;

 

   /**

    * The feature id for the '<em><b>Left</b></em>' containment reference.

@@ -649,7 +602,7 @@ public interface VampireLanguagePackage extends EPackage
    * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSRevImplies()

    * @generated

    */

-  int VLS_REV_IMPLIES = 17;

+  int VLS_REV_IMPLIES = 15;

 

   /**

    * The feature id for the '<em><b>Left</b></em>' containment reference.

@@ -686,7 +639,7 @@ public interface VampireLanguagePackage extends EPackage
    * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSXnor()

    * @generated

    */

-  int VLS_XNOR = 18;

+  int VLS_XNOR = 16;

 

   /**

    * The feature id for the '<em><b>Left</b></em>' containment reference.

@@ -723,7 +676,7 @@ public interface VampireLanguagePackage extends EPackage
    * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSNor()

    * @generated

    */

-  int VLS_NOR = 19;

+  int VLS_NOR = 17;

 

   /**

    * The feature id for the '<em><b>Left</b></em>' containment reference.

@@ -760,7 +713,7 @@ public interface VampireLanguagePackage extends EPackage
    * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSNand()

    * @generated

    */

-  int VLS_NAND = 20;

+  int VLS_NAND = 18;

 

   /**

    * The feature id for the '<em><b>Left</b></em>' containment reference.

@@ -797,7 +750,7 @@ public interface VampireLanguagePackage extends EPackage
    * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSAnd()

    * @generated

    */

-  int VLS_AND = 21;

+  int VLS_AND = 19;

 

   /**

    * The feature id for the '<em><b>Left</b></em>' containment reference.

@@ -834,7 +787,7 @@ public interface VampireLanguagePackage extends EPackage
    * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSOr()

    * @generated

    */

-  int VLS_OR = 22;

+  int VLS_OR = 20;

 

   /**

    * The feature id for the '<em><b>Left</b></em>' containment reference.

@@ -871,7 +824,7 @@ public interface VampireLanguagePackage extends EPackage
    * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSUniversalQuantifier()

    * @generated

    */

-  int VLS_UNIVERSAL_QUANTIFIER = 23;

+  int VLS_UNIVERSAL_QUANTIFIER = 21;

 

   /**

    * The feature id for the '<em><b>Variables</b></em>' containment reference list.

@@ -908,7 +861,7 @@ public interface VampireLanguagePackage extends EPackage
    * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSExistentialQuantifier()

    * @generated

    */

-  int VLS_EXISTENTIAL_QUANTIFIER = 24;

+  int VLS_EXISTENTIAL_QUANTIFIER = 22;

 

   /**

    * The feature id for the '<em><b>Variables</b></em>' containment reference list.

@@ -945,7 +898,7 @@ public interface VampireLanguagePackage extends EPackage
    * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSUnaryNegation()

    * @generated

    */

-  int VLS_UNARY_NEGATION = 25;

+  int VLS_UNARY_NEGATION = 23;

 

   /**

    * The feature id for the '<em><b>Operand</b></em>' containment reference.

@@ -973,7 +926,7 @@ public interface VampireLanguagePackage extends EPackage
    * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSInequality()

    * @generated

    */

-  int VLS_INEQUALITY = 26;

+  int VLS_INEQUALITY = 24;

 

   /**

    * The feature id for the '<em><b>Left</b></em>' containment reference.

@@ -1010,7 +963,7 @@ public interface VampireLanguagePackage extends EPackage
    * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSEquality()

    * @generated

    */

-  int VLS_EQUALITY = 27;

+  int VLS_EQUALITY = 25;

 

   /**

    * The feature id for the '<em><b>Left</b></em>' containment reference.

@@ -1047,7 +1000,7 @@ public interface VampireLanguagePackage extends EPackage
    * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSAssignment()

    * @generated

    */

-  int VLS_ASSIGNMENT = 28;

+  int VLS_ASSIGNMENT = 26;

 

   /**

    * The feature id for the '<em><b>Left</b></em>' containment reference.

@@ -1084,7 +1037,7 @@ public interface VampireLanguagePackage extends EPackage
    * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSConstant()

    * @generated

    */

-  int VLS_CONSTANT = 29;

+  int VLS_CONSTANT = 27;

 

   /**

    * The feature id for the '<em><b>Name</b></em>' attribute.

@@ -1112,7 +1065,7 @@ public interface VampireLanguagePackage extends EPackage
    * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSTrue()

    * @generated

    */

-  int VLS_TRUE = 30;

+  int VLS_TRUE = 28;

 

   /**

    * The number of structural features of the '<em>VLS True</em>' class.

@@ -1131,7 +1084,7 @@ public interface VampireLanguagePackage extends EPackage
    * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSFalse()

    * @generated

    */

-  int VLS_FALSE = 31;

+  int VLS_FALSE = 29;

 

   /**

    * The number of structural features of the '<em>VLS False</em>' class.

@@ -1150,7 +1103,7 @@ public interface VampireLanguagePackage extends EPackage
    * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSFunction()

    * @generated

    */

-  int VLS_FUNCTION = 32;

+  int VLS_FUNCTION = 30;

 

   /**

    * The feature id for the '<em><b>Constant</b></em>' attribute.

@@ -1187,7 +1140,7 @@ public interface VampireLanguagePackage extends EPackage
    * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSLess()

    * @generated

    */

-  int VLS_LESS = 33;

+  int VLS_LESS = 31;

 

   /**

    * The feature id for the '<em><b>Name</b></em>' attribute.

@@ -1224,7 +1177,7 @@ public interface VampireLanguagePackage extends EPackage
    * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSInt()

    * @generated

    */

-  int VLS_INT = 34;

+  int VLS_INT = 32;

 

   /**

    * The feature id for the '<em><b>Value</b></em>' attribute.

@@ -1252,7 +1205,7 @@ public interface VampireLanguagePackage extends EPackage
    * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSReal()

    * @generated

    */

-  int VLS_REAL = 35;

+  int VLS_REAL = 33;

 

   /**

    * The feature id for the '<em><b>Value</b></em>' attribute.

@@ -1280,7 +1233,7 @@ public interface VampireLanguagePackage extends EPackage
    * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSRational()

    * @generated

    */

-  int VLS_RATIONAL = 36;

+  int VLS_RATIONAL = 34;

 

   /**

    * The feature id for the '<em><b>Value</b></em>' attribute.

@@ -1308,7 +1261,7 @@ public interface VampireLanguagePackage extends EPackage
    * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSDoubleQuote()

    * @generated

    */

-  int VLS_DOUBLE_QUOTE = 37;

+  int VLS_DOUBLE_QUOTE = 35;

 

   /**

    * The feature id for the '<em><b>Value</b></em>' attribute.

@@ -1489,37 +1442,6 @@ public interface VampireLanguagePackage extends EPackage
   EClass getVLSSatisfiable();

 

   /**

-   * Returns the meta object for class '{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTrying <em>VLS Trying</em>}'.

-   * <!-- begin-user-doc -->

-   * <!-- end-user-doc -->

-   * @return the meta object for class '<em>VLS Trying</em>'.

-   * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTrying

-   * @generated

-   */

-  EClass getVLSTrying();

-

-  /**

-   * Returns the meta object for the attribute '{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTrying#getName <em>Name</em>}'.

-   * <!-- begin-user-doc -->

-   * <!-- end-user-doc -->

-   * @return the meta object for the attribute '<em>Name</em>'.

-   * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTrying#getName()

-   * @see #getVLSTrying()

-   * @generated

-   */

-  EAttribute getVLSTrying_Name();

-

-  /**

-   * Returns the meta object for class '{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFiniteModel <em>VLS Finite Model</em>}'.

-   * <!-- begin-user-doc -->

-   * <!-- end-user-doc -->

-   * @return the meta object for class '<em>VLS Finite Model</em>'.

-   * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFiniteModel

-   * @generated

-   */

-  EClass getVLSFiniteModel();

-

-  /**

    * Returns the meta object for class '{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula <em>VLS Fof Formula</em>}'.

    * <!-- begin-user-doc -->

    * <!-- end-user-doc -->

@@ -2492,34 +2414,6 @@ public interface VampireLanguagePackage extends EPackage
     EClass VLS_SATISFIABLE = eINSTANCE.getVLSSatisfiable();

 

     /**

-     * The meta object literal for the '{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSTryingImpl <em>VLS Trying</em>}' class.

-     * <!-- begin-user-doc -->

-     * <!-- end-user-doc -->

-     * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSTryingImpl

-     * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSTrying()

-     * @generated

-     */

-    EClass VLS_TRYING = eINSTANCE.getVLSTrying();

-

-    /**

-     * The meta object literal for the '<em><b>Name</b></em>' attribute feature.

-     * <!-- begin-user-doc -->

-     * <!-- end-user-doc -->

-     * @generated

-     */

-    EAttribute VLS_TRYING__NAME = eINSTANCE.getVLSTrying_Name();

-

-    /**

-     * The meta object literal for the '{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSFiniteModelImpl <em>VLS Finite Model</em>}' class.

-     * <!-- begin-user-doc -->

-     * <!-- end-user-doc -->

-     * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSFiniteModelImpl

-     * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSFiniteModel()

-     * @generated

-     */

-    EClass VLS_FINITE_MODEL = eINSTANCE.getVLSFiniteModel();

-

-    /**

      * The meta object literal for the '{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSFofFormulaImpl <em>VLS Fof Formula</em>}' class.

      * <!-- begin-user-doc -->

      * <!-- end-user-doc -->

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VampireLanguageFactoryImpl.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VampireLanguageFactoryImpl.java
index cd4a7a01..c3c74fe9 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VampireLanguageFactoryImpl.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VampireLanguageFactoryImpl.java
@@ -71,8 +71,6 @@ public class VampireLanguageFactoryImpl extends EFactoryImpl implements VampireL
       case VampireLanguagePackage.VLS_COMMENT: return createVLSComment();

       case VampireLanguagePackage.VLS_CONFIRMATIONS: return createVLSConfirmations();

       case VampireLanguagePackage.VLS_SATISFIABLE: return createVLSSatisfiable();

-      case VampireLanguagePackage.VLS_TRYING: return createVLSTrying();

-      case VampireLanguagePackage.VLS_FINITE_MODEL: return createVLSFiniteModel();

       case VampireLanguagePackage.VLS_FOF_FORMULA: return createVLSFofFormula();

       case VampireLanguagePackage.VLS_TFF_FORMULA: return createVLSTffFormula();

       case VampireLanguagePackage.VLS_ANNOTATION: return createVLSAnnotation();

@@ -179,28 +177,6 @@ public class VampireLanguageFactoryImpl extends EFactoryImpl implements VampireL
    * <!-- end-user-doc -->

    * @generated

    */

-  public VLSTrying createVLSTrying()

-  {

-    VLSTryingImpl vlsTrying = new VLSTryingImpl();

-    return vlsTrying;

-  }

-

-  /**

-   * <!-- begin-user-doc -->

-   * <!-- end-user-doc -->

-   * @generated

-   */

-  public VLSFiniteModel createVLSFiniteModel()

-  {

-    VLSFiniteModelImpl vlsFiniteModel = new VLSFiniteModelImpl();

-    return vlsFiniteModel;

-  }

-

-  /**

-   * <!-- begin-user-doc -->

-   * <!-- end-user-doc -->

-   * @generated

-   */

   public VLSFofFormula createVLSFofFormula()

   {

     VLSFofFormulaImpl vlsFofFormula = new VLSFofFormulaImpl();

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VampireLanguagePackageImpl.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VampireLanguagePackageImpl.java
index ff71ff74..2b131272 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VampireLanguagePackageImpl.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VampireLanguagePackageImpl.java
@@ -15,7 +15,6 @@ import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquality;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquivalent;

 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSExistentialQuantifier;

 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFalse;

-import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFiniteModel;

 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula;

 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction;

 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunctionFof;

@@ -35,7 +34,6 @@ import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSSatisfiable;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm;

 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTffFormula;

 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTrue;

-import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTrying;

 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUnaryNegation;

 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier;

 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable;

@@ -106,20 +104,6 @@ public class VampireLanguagePackageImpl extends EPackageImpl implements VampireL
    * <!-- end-user-doc -->

    * @generated

    */

-  private EClass vlsTryingEClass = null;

-

-  /**

-   * <!-- begin-user-doc -->

-   * <!-- end-user-doc -->

-   * @generated

-   */

-  private EClass vlsFiniteModelEClass = null;

-

-  /**

-   * <!-- begin-user-doc -->

-   * <!-- end-user-doc -->

-   * @generated

-   */

   private EClass vlsFofFormulaEClass = null;

 

   /**

@@ -543,36 +527,6 @@ public class VampireLanguagePackageImpl extends EPackageImpl implements VampireL
    * <!-- end-user-doc -->

    * @generated

    */

-  public EClass getVLSTrying()

-  {

-    return vlsTryingEClass;

-  }

-

-  /**

-   * <!-- begin-user-doc -->

-   * <!-- end-user-doc -->

-   * @generated

-   */

-  public EAttribute getVLSTrying_Name()

-  {

-    return (EAttribute)vlsTryingEClass.getEStructuralFeatures().get(0);

-  }

-

-  /**

-   * <!-- begin-user-doc -->

-   * <!-- end-user-doc -->

-   * @generated

-   */

-  public EClass getVLSFiniteModel()

-  {

-    return vlsFiniteModelEClass;

-  }

-

-  /**

-   * <!-- begin-user-doc -->

-   * <!-- end-user-doc -->

-   * @generated

-   */

   public EClass getVLSFofFormula()

   {

     return vlsFofFormulaEClass;

@@ -1389,11 +1343,6 @@ public class VampireLanguagePackageImpl extends EPackageImpl implements VampireL
 

     vlsSatisfiableEClass = createEClass(VLS_SATISFIABLE);

 

-    vlsTryingEClass = createEClass(VLS_TRYING);

-    createEAttribute(vlsTryingEClass, VLS_TRYING__NAME);

-

-    vlsFiniteModelEClass = createEClass(VLS_FINITE_MODEL);

-

     vlsFofFormulaEClass = createEClass(VLS_FOF_FORMULA);

     createEAttribute(vlsFofFormulaEClass, VLS_FOF_FORMULA__NAME);

     createEAttribute(vlsFofFormulaEClass, VLS_FOF_FORMULA__FOF_ROLE);

@@ -1581,11 +1530,6 @@ public class VampireLanguagePackageImpl extends EPackageImpl implements VampireL
 

     initEClass(vlsSatisfiableEClass, VLSSatisfiable.class, "VLSSatisfiable", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);

 

-    initEClass(vlsTryingEClass, VLSTrying.class, "VLSTrying", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);

-    initEAttribute(getVLSTrying_Name(), ecorePackage.getEString(), "name", null, 0, 1, VLSTrying.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, !IS_UNSETTABLE, !IS_ID, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);

-

-    initEClass(vlsFiniteModelEClass, VLSFiniteModel.class, "VLSFiniteModel", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);

-

     initEClass(vlsFofFormulaEClass, VLSFofFormula.class, "VLSFofFormula", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);

     initEAttribute(getVLSFofFormula_Name(), ecorePackage.getEString(), "name", null, 0, 1, VLSFofFormula.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, !IS_UNSETTABLE, !IS_ID, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);

     initEAttribute(getVLSFofFormula_FofRole(), ecorePackage.getEString(), "fofRole", null, 0, 1, VLSFofFormula.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, !IS_UNSETTABLE, !IS_ID, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/util/VampireLanguageAdapterFactory.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/util/VampireLanguageAdapterFactory.java
index 90781f47..41e073ca 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/util/VampireLanguageAdapterFactory.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/util/VampireLanguageAdapterFactory.java
@@ -106,16 +106,6 @@ public class VampireLanguageAdapterFactory extends AdapterFactoryImpl
         return createVLSSatisfiableAdapter();

       }

       @Override

-      public Adapter caseVLSTrying(VLSTrying object)

-      {

-        return createVLSTryingAdapter();

-      }

-      @Override

-      public Adapter caseVLSFiniteModel(VLSFiniteModel object)

-      {

-        return createVLSFiniteModelAdapter();

-      }

-      @Override

       public Adapter caseVLSFofFormula(VLSFofFormula object)

       {

         return createVLSFofFormulaAdapter();

@@ -378,36 +368,6 @@ public class VampireLanguageAdapterFactory extends AdapterFactoryImpl
   }

 

   /**

-   * Creates a new adapter for an object of class '{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTrying <em>VLS Trying</em>}'.

-   * <!-- begin-user-doc -->

-   * This default implementation returns null so that we can easily ignore cases;

-   * it's useful to ignore a case when inheritance will catch all the cases anyway.

-   * <!-- end-user-doc -->

-   * @return the new adapter.

-   * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTrying

-   * @generated

-   */

-  public Adapter createVLSTryingAdapter()

-  {

-    return null;

-  }

-

-  /**

-   * Creates a new adapter for an object of class '{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFiniteModel <em>VLS Finite Model</em>}'.

-   * <!-- begin-user-doc -->

-   * This default implementation returns null so that we can easily ignore cases;

-   * it's useful to ignore a case when inheritance will catch all the cases anyway.

-   * <!-- end-user-doc -->

-   * @return the new adapter.

-   * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFiniteModel

-   * @generated

-   */

-  public Adapter createVLSFiniteModelAdapter()

-  {

-    return null;

-  }

-

-  /**

    * Creates a new adapter for an object of class '{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula <em>VLS Fof Formula</em>}'.

    * <!-- begin-user-doc -->

    * This default implementation returns null so that we can easily ignore cases;

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/util/VampireLanguageSwitch.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/util/VampireLanguageSwitch.java
index eddb3b4c..24ad4238 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/util/VampireLanguageSwitch.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/util/VampireLanguageSwitch.java
@@ -116,20 +116,6 @@ public class VampireLanguageSwitch<T> extends Switch<T>
         if (result == null) result = defaultCase(theEObject);

         return result;

       }

-      case VampireLanguagePackage.VLS_TRYING:

-      {

-        VLSTrying vlsTrying = (VLSTrying)theEObject;

-        T result = caseVLSTrying(vlsTrying);

-        if (result == null) result = defaultCase(theEObject);

-        return result;

-      }

-      case VampireLanguagePackage.VLS_FINITE_MODEL:

-      {

-        VLSFiniteModel vlsFiniteModel = (VLSFiniteModel)theEObject;

-        T result = caseVLSFiniteModel(vlsFiniteModel);

-        if (result == null) result = defaultCase(theEObject);

-        return result;

-      }

       case VampireLanguagePackage.VLS_FOF_FORMULA:

       {

         VLSFofFormula vlsFofFormula = (VLSFofFormula)theEObject;

@@ -471,38 +457,6 @@ public class VampireLanguageSwitch<T> extends Switch<T>
   }

 

   /**

-   * Returns the result of interpreting the object as an instance of '<em>VLS Trying</em>'.

-   * <!-- begin-user-doc -->

-   * This implementation returns null;

-   * returning a non-null result will terminate the switch.

-   * <!-- end-user-doc -->

-   * @param object the target of the switch.

-   * @return the result of interpreting the object as an instance of '<em>VLS Trying</em>'.

-   * @see #doSwitch(org.eclipse.emf.ecore.EObject) doSwitch(EObject)

-   * @generated

-   */

-  public T caseVLSTrying(VLSTrying object)

-  {

-    return null;

-  }

-

-  /**

-   * Returns the result of interpreting the object as an instance of '<em>VLS Finite Model</em>'.

-   * <!-- begin-user-doc -->

-   * This implementation returns null;

-   * returning a non-null result will terminate the switch.

-   * <!-- end-user-doc -->

-   * @param object the target of the switch.

-   * @return the result of interpreting the object as an instance of '<em>VLS Finite Model</em>'.

-   * @see #doSwitch(org.eclipse.emf.ecore.EObject) doSwitch(EObject)

-   * @generated

-   */

-  public T caseVLSFiniteModel(VLSFiniteModel object)

-  {

-    return null;

-  }

-

-  /**

    * Returns the result of interpreting the object as an instance of '<em>VLS Fof Formula</em>'.

    * <!-- begin-user-doc -->

    * This implementation returns null;

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/VampireLanguage.xtext b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/VampireLanguage.xtext
index a76107c4..2b5958ca 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/VampireLanguage.xtext
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/VampireLanguage.xtext
@@ -85,13 +85,13 @@ VLSSatisfiable:
         {VLSSatisfiable} 'Satisfiable!'

 ;

 

-VLSTrying:

-        'TRYING' '[' name = LITERAL ']'

-;

-

-VLSFiniteModel:

-        {VLSFiniteModel} 'Finite' 'Model' 'Found!'

-;

+//VLSTrying:

+//      'TRYING' '[' name = LITERAL ']'

+//;

+//

+//VLSFiniteModel:

+//      {VLSFiniteModel} 'Finite' 'Model' 'Found!'

+//;

 

 // <FOF formulas>

 VLSFofFormula:

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/formatting2/VampireLanguageFormatter.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/formatting2/VampireLanguageFormatter.xtend
index 4398d659..f943daad 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/formatting2/VampireLanguageFormatter.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/formatting2/VampireLanguageFormatter.xtend
@@ -38,11 +38,11 @@ class VampireLanguageFormatter extends AbstractFormatter2 {
         }

         

         def dispatch void format(VLSFofFormula formula, extension IFormattableDocument document){

-//              formula.append[newLine]

+                formula.append[newLine]

         }

         

         def dispatch void format(VLSComment comment, extension IFormattableDocument document){

-//              comment.append[newLine]

+                comment.append[newLine]

         }

         // TODO: implement for VLSFofFormula, VLSAnnotation, VLSAnd, VLSOr, VLSUniversalQuantifier, VLSExistentialQuantifier, VLSUnaryNegation, VLSFunction, VLSLess, VLSFunctionFof, VLSEquivalent, VLSImplies, VLSRevImplies, VLSXnor, VLSNor, VLSNand, VLSInequality, VLSEquality, VLSAssignment

 }

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageRuntimeModule.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageRuntimeModule.xtendbin
index 0f621faf..e0367170 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageRuntimeModule.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageRuntimeModule.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageStandaloneSetup.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageStandaloneSetup.xtendbin
index c7c7a12c..906c39f5 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageStandaloneSetup.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageStandaloneSetup.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/formatting2/.VampireLanguageFormatter.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/formatting2/.VampireLanguageFormatter.xtendbin
index c21238ee..47a395a0 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/formatting2/.VampireLanguageFormatter.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/formatting2/.VampireLanguageFormatter.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/formatting2/VampireLanguageFormatter.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/formatting2/VampireLanguageFormatter.java
index c439bbdb..73a032e7 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/formatting2/VampireLanguageFormatter.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/formatting2/VampireLanguageFormatter.java
@@ -15,8 +15,10 @@ import org.eclipse.emf.common.util.EList;
 import org.eclipse.emf.ecore.EObject;

 import org.eclipse.xtext.formatting2.AbstractFormatter2;

 import org.eclipse.xtext.formatting2.IFormattableDocument;

+import org.eclipse.xtext.formatting2.IHiddenRegionFormatter;

 import org.eclipse.xtext.resource.XtextResource;

 import org.eclipse.xtext.xbase.lib.Extension;

+import org.eclipse.xtext.xbase.lib.Procedures.Procedure1;

 

 @SuppressWarnings("all")

 public class VampireLanguageFormatter extends AbstractFormatter2 {

@@ -47,9 +49,17 @@ public class VampireLanguageFormatter extends AbstractFormatter2 {
   }

   

   protected void _format(final VLSFofFormula formula, @Extension final IFormattableDocument document) {

+    final Procedure1<IHiddenRegionFormatter> _function = (IHiddenRegionFormatter it) -> {

+      it.newLine();

+    };

+    document.<VLSFofFormula>append(formula, _function);

   }

   

   protected void _format(final VLSComment comment, @Extension final IFormattableDocument document) {

+    final Procedure1<IHiddenRegionFormatter> _function = (IHiddenRegionFormatter it) -> {

+      it.newLine();

+    };

+    document.<VLSComment>append(comment, _function);

   }

   

   public void format(final Object comment, final IFormattableDocument document) {

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/generator/.VampireLanguageGenerator.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/generator/.VampireLanguageGenerator.xtendbin
index 763ffecc..74f517cf 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/generator/.VampireLanguageGenerator.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/generator/.VampireLanguageGenerator.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/scoping/.VampireLanguageScopeProvider.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/scoping/.VampireLanguageScopeProvider.xtendbin
index 7aa1da64..3c09270e 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/scoping/.VampireLanguageScopeProvider.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/scoping/.VampireLanguageScopeProvider.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/validation/.VampireLanguageValidator.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/validation/.VampireLanguageValidator.xtendbin
index 7b46ca82..96e8559a 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/validation/.VampireLanguageValidator.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/validation/.VampireLanguageValidator.xtendbin
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 41eb6ade..aed85a48 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,4 +1,5 @@
-source.. = src/

-output.. = bin/

 bin.includes = META-INF/,\

                .

+source.. = src/,\

+           src-gen/

+output.. = bin/

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireAnalyzerConfiguration.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireAnalyzerConfiguration.xtend
index 27e00ccf..618980a3 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireAnalyzerConfiguration.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireAnalyzerConfiguration.xtend
@@ -4,10 +4,9 @@ import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration
 
 class VampireSolverConfiguration extends LogicSolverConfiguration {
         
-        public var int symmetry = 0 // by default
+        //public var int symmetry = 0 // by default
         //choose needed backend solver
 //      public var VampireBackendSolver solver = VampireBackendSolver.SAT4J
-        public var boolean writeToFile = false
 }
 
 
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend
index cbe53bff..ee802a99 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend
@@ -7,6 +7,7 @@ import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguage
 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Vampire2LogicMapper
 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireHandler
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage
+import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel
 import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner
 import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasonerException
 import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration
@@ -14,80 +15,81 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
 import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult
 import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace
 
-class VampireSolver extends LogicReasoner{
-        
+class VampireSolver extends LogicReasoner {
+
         new() {
                 VampireLanguagePackage.eINSTANCE.eClass
                 val x = new VampireLanguageStandaloneSetupGenerated
                 VampireLanguageStandaloneSetup::doSetup()
         }
-        
-         val Logic2VampireLanguageMapper forwardMapper = new Logic2VampireLanguageMapper(new Logic2VampireLanguageMapper_TypeMapper_FilteredTypes)
-         val Vampire2LogicMapper backwardMapper = new Vampire2LogicMapper
-         val VampireHandler handler = new VampireHandler
-         
-         
-         val fileName = "vampireProblem.tptp"
-         
-         override solve(LogicProblem problem, LogicSolverConfiguration config, ReasonerWorkspace workspace) throws LogicReasonerException {
+
+        val Logic2VampireLanguageMapper forwardMapper = new Logic2VampireLanguageMapper(
+                new Logic2VampireLanguageMapper_TypeMapper_FilteredTypes)
+        val Vampire2LogicMapper backwardMapper = new Vampire2LogicMapper
+        val VampireHandler handler = new VampireHandler
+
+        val fileName = "vampireProblem.tptp"
+
+        override solve(LogicProblem problem, LogicSolverConfiguration config,
+                ReasonerWorkspace workspace) throws LogicReasonerException {
                 val vampireConfig = config.asConfig
-                
+
                 // Start: Logic -> Vampire mapping
                 val transformationStart = System.currentTimeMillis
-                //TODO
-                val result = forwardMapper.transformProblem(problem,vampireConfig)
+                // TODO
+                val result = forwardMapper.transformProblem(problem, vampireConfig)
                 val vampireProblem = result.output
                 val forwardTrace = result.trace
-                
+
                 var String fileURI = null;
                 var String vampireCode = null;
-                vampireCode = workspace.writeModelToString(vampireProblem,fileName)
-                if(vampireConfig.writeToFile) {
-                        fileURI = workspace.writeModel(vampireProblem,fileName).toFileString
+                vampireCode = workspace.writeModelToString(vampireProblem, fileName)
+
+                val writeFile = (
+                        vampireConfig.documentationLevel === DocumentationLevel::NORMAL ||
+                        vampireConfig.documentationLevel === DocumentationLevel::FULL)
+                if (writeFile) {
+                        fileURI = workspace.writeModel(vampireProblem, fileName).toFileString
                 }
-                
-                //Result as String
 
-                                
+                // Result as String
                 val transformationTime = System.currentTimeMillis - transformationStart
                 // Finish: Logic -> Vampire mapping
-                
-                                
                 /*        
-                // Start: Solving Alloy problem
-                val solverStart = System.currentTimeMillis
-                //Calling Solver (Currently Manually)
-                val result2 = handler.callSolver(vampireProblem,workspace,vampireConfig,vampireCode)
-//              val result2 = null
-                //TODO
-                //Backwards Mapper
-                val logicResult = backwardMapper.transformOutput(problem,config.solutionScope.numberOfRequiredSolution,result2,forwardTrace,transformationTime)
-                
-                val solverFinish = System.currentTimeMillis-solverStart
-                // Finish: Solving Alloy problem
-                                
-                if(vampireConfig.writeToFile) workspace.deactivateModel(fileName)
-                
-                return logicResult
-                
-                /*/
+                 * // Start: Solving Alloy problem
+                 * val solverStart = System.currentTimeMillis
+                 * //Calling Solver (Currently Manually)
+                 * val result2 = handler.callSolver(vampireProblem,workspace,vampireConfig,vampireCode)
+                 * //           val result2 = null
+                 * //TODO
+                 * //Backwards Mapper
+                 * val logicResult = backwardMapper.transformOutput(problem,config.solutionScope.numberOfRequiredSolution,result2,forwardTrace,transformationTime)
+                 * 
+                 * val solverFinish = System.currentTimeMillis-solverStart
+                 * // Finish: Solving Alloy problem
+                 *              
+                 * if(vampireConfig.writeToFile) workspace.deactivateModel(fileName)
+                 * 
+                 * return logicResult
+                 * 
+                 /*/
                 return null // for now
-                //*/
+                // */
         }
-        
-        def asConfig(LogicSolverConfiguration configuration){
-                if(configuration instanceof VampireSolverConfiguration) {
+
+        def asConfig(LogicSolverConfiguration configuration) {
+                if (configuration instanceof VampireSolverConfiguration) {
                         return configuration
                 } else {
-                        throw new IllegalArgumentException('''The configuration have to be an «VampireSolverConfiguration.simpleName»!''')    
+                        throw new IllegalArgumentException('''The configuration have to be an «VampireSolverConfiguration.simpleName»!''')
                 }
         }
-        
+
 //      /*
 //       * not for now
 //       * 
         override getInterpretations(ModelResult modelResult) {
-                //val answers = (modelResult.representation as MonitoredAlloySolution).aswers.map[key]
+                // val answers = (modelResult.representation as MonitoredAlloySolution).aswers.map[key]
 //              val sols = modelResult.representation// as List<A4Solution>
 //              //val res = answers.map 
 //              sols.map[
@@ -98,7 +100,6 @@ class VampireSolver extends LogicReasoner{
 //                              modelResult.trace as Logic2AlloyLanguageMapperTrace
 //                      )
 //              ]
-        }       
+        }
 //      */
-        
-}
\ No newline at end of file
+}
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend
index cd48a032..e2c15b75 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend
@@ -48,6 +48,8 @@ class Logic2VampireLanguageMapper {
                 this)
         @Accessors(PUBLIC_GETTER) private val Logic2VampireLanguageMapper_RelationMapper relationMapper = new Logic2VampireLanguageMapper_RelationMapper(
                 this)
+        @Accessors(PUBLIC_GETTER) private val Logic2VampireLanguageMapper_ScopeMapper scopeMapper = new Logic2VampireLanguageMapper_ScopeMapper(
+                this)
         @Accessors(PUBLIC_GETTER) private val Logic2VampireLanguageMapper_TypeMapper typeMapper
 
         public new(Logic2VampireLanguageMapper_TypeMapper typeMapper) {
@@ -72,11 +74,15 @@ class Logic2VampireLanguageMapper {
 //                      it.incQueryEngine = viatraQueryEngine.on(new EMFScope(problem))
                 ]
 
-                // call mappers
+                // TYPE MAPPER
                 if (!problem.types.isEmpty) {
                         typeMapper.transformTypes(problem.types, problem.elements, this, trace)
                 }
 
+                // SCOPE MAPPER
+                scopeMapper.transformScope(config, trace)
+                
+                
                 trace.constantDefinitions = problem.collectConstantDefinitions
                 trace.relationDefinitions = problem.collectRelationDefinitions
 
@@ -204,8 +210,9 @@ class Logic2VampireLanguageMapper {
                 ]
         }
 
-        def dispatch protected VLSTerm transformTerm(Distinct distinct, Logic2VampireLanguageMapperTrace trace, Map<Variable, VLSVariable> variables) {
-                support.unfoldDistinctTerms(this,distinct.operands,trace,variables) }
+        def dispatch protected VLSTerm transformTerm(Distinct distinct, Logic2VampireLanguageMapperTrace trace,
+                Map<Variable, VLSVariable> variables) { support.unfoldDistinctTerms(this, distinct.operands, trace, variables) }
+
 //      
 //              def dispatch protected ALSTerm transformTerm(Plus plus, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) {
 //              createALSFunctionCall => [it.params += plus.leftOperand.transformTerm(trace,variables) it.params += plus.rightOperand.transformTerm(trace,variables) it.referredNumericOperator = ALSNumericOperator.PLUS] }
@@ -228,12 +235,14 @@ class Logic2VampireLanguageMapper {
                 support.createExistentiallyQuantifiedExpression(this, exists, trace, variables)
         }
 
-        def dispatch protected VLSTerm transformTerm(InstanceOf instanceOf, Logic2VampireLanguageMapperTrace trace, Map<Variable, VLSVariable> variables) {
+        def dispatch protected VLSTerm transformTerm(InstanceOf instanceOf, Logic2VampireLanguageMapperTrace trace,
+                Map<Variable, VLSVariable> variables) {
                 return createVLSFunction => [
-                        it.constant = support.toIDMultiple("type", (instanceOf.range as ComplexTypeReference).referred.name )
+                        it.constant = support.toIDMultiple("type", (instanceOf.range as ComplexTypeReference).referred.name)
                         it.terms += instanceOf.value.transformTerm(trace, variables)
                 ]
         }
+
 //      
 //      def dispatch protected ALSTerm transformTerm(TransitiveClosure tc, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) {
 //              return this.relationMapper.transformTransitiveRelationReference(
@@ -253,50 +262,49 @@ class Logic2VampireLanguageMapper {
         def dispatch protected VLSTerm transformSymbolicReference(DefinedElement referred,
                 List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace,
                 Map<Variable, VLSVariable> variables) {
-                        typeMapper.transformReference(referred, trace)
-                }
+                typeMapper.transformReference(referred, trace)
+        }
 
-                def dispatch protected VLSTerm transformSymbolicReference(ConstantDeclaration constant,
-                        List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace,
-                        Map<Variable, VLSVariable> variables) {
-                                // might need to make sure that only declared csts get transformed. see for Alloy
-                                val res = createVLSConstant => [
-                                        // ask if necessary VLSConstantDeclaration and not just directly strng
-                                        it.name = support.toID(constant.name)
-                                ]
-                                // no postprocessing cuz booleans are accepted
-                                return res
-                        }
-
-                        // NOT NEEDED FOR NOW
-                        // TODO
-                        def dispatch protected VLSTerm transformSymbolicReference(ConstantDefinition constant,
-                                List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace,
-                                Map<Variable, VLSVariable> variables) {
+        def dispatch protected VLSTerm transformSymbolicReference(ConstantDeclaration constant,
+                List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace,
+                Map<Variable, VLSVariable> variables) {
+                // might need to make sure that only declared csts get transformed. see for Alloy
+                val res = createVLSConstant => [
+                        // ask if necessary VLSConstantDeclaration and not just directly strng
+                        it.name = support.toID(constant.name)
+                ]
+                // no postprocessing cuz booleans are accepted
+                return res
+        }
+
+        // NOT NEEDED FOR NOW
+        // TODO
+        def dispatch protected VLSTerm transformSymbolicReference(ConstantDefinition constant,
+                List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace,
+                Map<Variable, VLSVariable> variables) {
 //              val res = createVLSFunctionCall => [
 //                      it.referredDefinition = constant.lookup(trace.constantDefinition2Function)
 //              ]
 //              return support.postprocessResultOfSymbolicReference(constant.type,res,trace)
-                                }
+        }
 
-                                def dispatch protected VLSTerm transformSymbolicReference(Variable variable,
-                                        List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace,
-                                        Map<Variable, VLSVariable> variables) {
+        def dispatch protected VLSTerm transformSymbolicReference(Variable variable, List<Term> parameterSubstitutions,
+                Logic2VampireLanguageMapperTrace trace, Map<Variable, VLSVariable> variables) {
 
-                                        // cannot treat variable as function (constant) because of name ID not being the same
-                                        // below does not work
-                                        val res = createVLSVariable => [
+                // cannot treat variable as function (constant) because of name ID not being the same
+                // below does not work
+                val res = createVLSVariable => [
 //                                              it.name = support.toIDMultiple("Var", variable.lookup(variables).name)
-                                                it.name = support.toID(variable.lookup(variables).name)
-                                        ]
-                                        // no need for potprocessing cuz booleans are supported
-                                        return res
-                                }
-
-                                // TODO
-                                def dispatch protected VLSTerm transformSymbolicReference(FunctionDeclaration function,
-                                        List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace,
-                                        Map<Variable, VLSVariable> variables) {
+                        it.name = support.toID(variable.lookup(variables).name)
+                ]
+                // no need for potprocessing cuz booleans are supported
+                return res
+        }
+
+        // TODO
+        def dispatch protected VLSTerm transformSymbolicReference(FunctionDeclaration function,
+                List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace,
+                Map<Variable, VLSVariable> variables) {
 //              if(trace.functionDefinitions.containsKey(function)) {
 //                      return this.transformSymbolicReference(function.lookup(trace.functionDefinitions),parameterSubstitutions,trace,variables)
 //              } else {
@@ -316,71 +324,68 @@ class Logic2VampireLanguageMapper {
 //                              return support.postprocessResultOfSymbolicReference(function.range,res,trace)
 //                      }
 //              }
-                                }
+        }
 
-                                // TODO
-                                def dispatch protected VLSTerm transformSymbolicReference(FunctionDefinition function,
-                                        List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace,
-                                        Map<Variable, VLSVariable> variables) {
+        // TODO
+        def dispatch protected VLSTerm transformSymbolicReference(FunctionDefinition function,
+                List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace,
+                Map<Variable, VLSVariable> variables) {
 //              val result = createVLSFunctionCall => [
 //                      it.referredDefinition = function.lookup(trace.functionDefinition2Function)
 //                      it.params += parameterSubstitutions.map[it.transformTerm(trace,variables)]
 //              ]
 //              return support.postprocessResultOfSymbolicReference(function.range,result,trace)
-                                }
-
-                                // TODO
-                                /*
-                                def dispatch protected VLSTerm transformSymbolicReference(Relation relation,
-                                        List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace,
-                                        Map<Variable, VLSVariable> variables) {
-                                        if (trace.relationDefinitions.containsKey(relation)) {
-                                                this.transformSymbolicReference(relation.lookup(trace.relationDefinitions),
-                                                        parameterSubstitutions, trace, variables)
-                                        }
-                                        else {
-//                                              if (relationMapper.transformToHostedField(relation, trace)) {
-//                                                      val VLSRelation = relation.lookup(trace.relationDeclaration2Field)
-//                                                      // R(a,b) =>
-//                                                      // b in a.R
-//                                                      return createVLSSubset => [
-//                                                              it.leftOperand = parameterSubstitutions.get(1).transformTerm(trace, variables)
-//                                                              it.rightOperand = createVLSJoin => [
-//                                                                      it.leftOperand = parameterSubstitutions.get(0).transformTerm(trace, variables)
-//                                                                      it.rightOperand = createVLSReference => [it.referred = VLSRelation]
-//                                                              ]
-//                                                      ]
-//                                              } else {
-//                                                      val target = createVLSJoin => [
-//                                                              leftOperand = createVLSReference => [referred = trace.logicLanguage]
-//                                                              rightOperand = createVLSReference => [
-//                                                                      referred = relation.lookup(trace.relationDeclaration2Global)
-//                                                              ]
-//                                                      ]
-//                                                      val source = support.unfoldTermDirectProduct(this, parameterSubstitutions, trace, variables)
-//
-//                                                      return createVLSSubset => [
-//                                                              leftOperand = source
-//                                                              rightOperand = target
-//                                                      ]
-//                                              }
-                                        }
-                                }
-                                */
-
-                                // TODO
-                                def dispatch protected VLSTerm transformSymbolicReference(Relation relation,
-                                        List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace,
-                                        Map<Variable, VLSVariable> variables) {
+        }
+
+        // TODO
+        /*
+         * def dispatch protected VLSTerm transformSymbolicReference(Relation relation,
+         *      List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace,
+         *      Map<Variable, VLSVariable> variables) {
+         *      if (trace.relationDefinitions.containsKey(relation)) {
+         *              this.transformSymbolicReference(relation.lookup(trace.relationDefinitions),
+         *                      parameterSubstitutions, trace, variables)
+         *      }
+         *      else {
+         * //                                           if (relationMapper.transformToHostedField(relation, trace)) {
+         * //                                                   val VLSRelation = relation.lookup(trace.relationDeclaration2Field)
+         * //                                                   // R(a,b) =>
+         * //                                                   // b in a.R
+         * //                                                   return createVLSSubset => [
+         * //                                                           it.leftOperand = parameterSubstitutions.get(1).transformTerm(trace, variables)
+         * //                                                           it.rightOperand = createVLSJoin => [
+         * //                                                                   it.leftOperand = parameterSubstitutions.get(0).transformTerm(trace, variables)
+         * //                                                                   it.rightOperand = createVLSReference => [it.referred = VLSRelation]
+         * //                                                           ]
+         * //                                                   ]
+         * //                                           } else {
+         * //                                                   val target = createVLSJoin => [
+         * //                                                           leftOperand = createVLSReference => [referred = trace.logicLanguage]
+         * //                                                           rightOperand = createVLSReference => [
+         * //                                                                   referred = relation.lookup(trace.relationDeclaration2Global)
+         * //                                                           ]
+         * //                                                   ]
+         * //                                                   val source = support.unfoldTermDirectProduct(this, parameterSubstitutions, trace, variables)
+         * //
+         * //                                                   return createVLSSubset => [
+         * //                                                           leftOperand = source
+         * //                                                           rightOperand = target
+         * //                                                   ]
+         * //                                           }
+         *      }
+         * }
+         */
+        // TODO
+        def dispatch protected VLSTerm transformSymbolicReference(Relation relation, List<Term> parameterSubstitutions,
+                Logic2VampireLanguageMapperTrace trace, Map<Variable, VLSVariable> variables) {
 //                                       createVLSFunction => [
 //                                              it.referredDefinition = relation.lookup(trace.relationDefinition2Predicate)
 //                                              it.params += parameterSubstitutions.map[p|p.transformTerm(trace, variables)]
 //                                      ]
-                                        return createVLSFunction => [
-                                                it.constant = support.toIDMultiple("rel", relation.name)
-                                                it.terms += parameterSubstitutions.map[p | p.transformTerm(trace,variables)]
-                                        ]
-                                }
-
-                        }
-                        
\ No newline at end of file
+                return createVLSFunction => [
+                        it.constant = support.toIDMultiple("rel", relation.name)
+                        it.terms += parameterSubstitutions.map[p|p.transformTerm(trace, variables)]
+                ]
+        }
+
+}
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
new file mode 100644
index 00000000..84aa521d
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend
@@ -0,0 +1,74 @@
+package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder

+

+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant

+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

+

+class Logic2VampireLanguageMapper_ScopeMapper {

+        private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE

+        private val Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support

+        val Logic2VampireLanguageMapper base

+

+        public new(Logic2VampireLanguageMapper base) {

+                this.base = base

+        }

+

+        def dispatch public void transformScope(LogicSolverConfiguration config, Logic2VampireLanguageMapperTrace trace) {

+                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

+                for (var i = 0; i < config.typeScopes.minNewElements; i++) {

+                        val num = i + 1

+                        val cst = createVLSConstant => [

+                                it.name = "o" + num

+                        ]

+                        instances.add(cst)

+                }

+                

+                

+                // TODO: specify for the max

+

+

+                // 2. Create initial fof formula to specify the number of elems

+                val cstDec = createVLSFofFormula => [

+                        it.name = "typeScope"

+                        it.fofRole = "axiom"

+                        it.fofFormula = createVLSUniversalQuantifier => [

+                                it.variables += support.duplicate(variable)

+                                // check below

+                                it.operand = createVLSEquivalent => [

+                                        it.left = support.topLevelTypeFunc

+                                        it.right = support.unfoldOr(instances.map [ i |

+                                                createVLSEquality => [

+                                                        it.left = createVLSVariable => [it.name = variable.name]

+                                                        it.right = i

+                                                ]

+                                        ])

+                                ]

+                        ]

+                ]

+                trace.specification.formulas += cstDec

+

+

+                // TODO: specify for scope per type

+

+

+

+                // 3. Specify uniqueness of elements

+                val uniqueness = createVLSFofFormula => [

+                        it.name = "typeUniqueness"

+                        it.fofRole = "axiom"

+                        it.fofFormula = support.unfoldOr(instances.map [ i |

+                                createVLSEquality => [

+                                        it.left = createVLSVariable => [it.name = variable.name]

+                                        it.right = i

+                                ]

+                        ])

+                ]

+                trace.specification.formulas += cstDec

+        }

+}

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 ab92b42f..e69f0d51 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
@@ -1,17 +1,18 @@
 package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder
 
-import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.QuantifiedExpression
-import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.QuantifiedExpression
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable
 import java.util.ArrayList
 import java.util.HashMap
 import java.util.List
 import java.util.Map
-import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference
 import org.eclipse.emf.common.util.EList
-import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term
 
 class Logic2VampireLanguageMapper_Support {
         private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE
@@ -25,6 +26,19 @@ class Logic2VampireLanguageMapper_Support {
                 ids.split("\\s+").join("_")
         }
 
+        def protected VLSVariable duplicate(VLSVariable vrbl) {
+                return createVLSVariable => [it.name = vrbl.name]
+        }
+
+        def protected VLSFunction topLevelTypeFunc() {
+                return createVLSFunction => [
+                        it.constant = "object"
+                        it.terms += createVLSVariable => [
+                                it.name = "A"
+                        ]
+                ]
+        }
+
         // Support Functions
         // booleans
         // AND and OR
@@ -41,7 +55,6 @@ class Logic2VampireLanguageMapper_Support {
         }
 
         def protected VLSTerm unfoldOr(List<? extends VLSTerm> operands) {
-
 //              if(operands.size == 0) {basically return true}
                 /*else*/ if (operands.size == 1) {
                         return operands.head
@@ -56,20 +69,21 @@ class Logic2VampireLanguageMapper_Support {
 
         def protected VLSTerm unfoldDistinctTerms(Logic2VampireLanguageMapper m, EList<Term> operands,
                 Logic2VampireLanguageMapperTrace trace, Map<Variable, VLSVariable> variables) {
-                        if(operands.size == 1) { return m.transformTerm(operands.head,trace,variables) }
-                else if(operands.size > 1) {
-                        val notEquals = new ArrayList<VLSTerm>(operands.size*operands.size/2)
-                        for(i:0..<operands.size) {
-                                for(j: i+1..<operands.size) {
-                                        notEquals+=createVLSInequality=>[
-                                                it.left= m.transformTerm(operands.get(i),trace,variables)
-                                                it.right = m.transformTerm(operands.get(j),trace,variables)
+                if (operands.size == 1) {
+                        return m.transformTerm(operands.head, trace, variables)
+                } else if (operands.size > 1) {
+                        val notEquals = new ArrayList<VLSTerm>(operands.size * operands.size / 2)
+                        for (i : 0 ..< operands.size) {
+                                for (j : i + 1 ..< operands.size) {
+                                        notEquals += createVLSInequality => [
+                                                it.left = m.transformTerm(operands.get(i), trace, variables)
+                                                it.right = m.transformTerm(operands.get(j), trace, variables)
                                         ]
                                 }
                         }
                         return notEquals.unfoldAnd
-                 }
-                else throw new UnsupportedOperationException('''Logic operator with 0 operands!''')
+                } else
+                        throw new UnsupportedOperationException('''Logic operator with 0 operands!''')
         }
 
         // Symbolic
@@ -105,7 +119,6 @@ class Logic2VampireLanguageMapper_Support {
                         ]
                         typedefs.add(eq)
                 }
-                
 
                 createVLSUniversalQuantifier => [
                         it.variables += variableMap.values
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.xtend
index a0f0edda..aba47edb 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.xtend
@@ -1,20 +1,17 @@
 package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder
 
-import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
-import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
-import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquality
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm
-import java.util.ArrayList
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
 import java.util.HashMap
-import java.util.List
 import java.util.Map
 
 class Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes implements Logic2VampireLanguageMapper_TypeMapperTrace{
         
 //      public var VLSFofFormula objectSuperClass
         public val Map<Type, VLSFunction> type2Predicate = new HashMap;
-        public val Map<DefinedElement, VLSEquality> definedElement2Declaration = new HashMap //Not Yet Used
+        public val Map<DefinedElement, VLSFunction> element2Predicate = new HashMap
         public val Map<Type, VLSTerm> type2PossibleNot = new HashMap
         public val Map<Type, VLSTerm> type2And = new HashMap
 
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtend
index 41e2137c..eed10656 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtend
@@ -11,6 +11,8 @@ import java.util.ArrayList
 import java.util.Collection
 
 import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
+import java.util.List
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction
 
 class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Logic2VampireLanguageMapper_TypeMapper {
         private val Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support
@@ -25,50 +27,66 @@ class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Logic2Vamp
                 val typeTrace = new Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes
                 trace.typeMapperTrace = typeTrace
 
-                val VLSVariable variable = createVLSVariable => [it.name = "A"] // did not work
-                // 1. store predicates for declarations in trace
+                // The variable
+                val VLSVariable variable = createVLSVariable => [it.name = "A"]
+
+                // 1. Each type (class) is a predicate with a single variable as input
                 for (type : types) {
                         val typePred = createVLSFunction => [
-                                it.constant = support.toIDMultiple("type", type.name)
-                                it.terms += createVLSVariable => [it.name = variable.name]
+                                it.constant = support.toIDMultiple("t", type.name)
+                                it.terms += support.duplicate(variable)
                         ]
                         typeTrace.type2Predicate.put(type, typePred)
                 }
 
-                // 2. Map each type definition to fof formula
+                // 2. Map each ENUM type definition to fof formula
                 for (type : types.filter(TypeDefinition)) {
+                        val List<VLSFunction> orElems = newArrayList
+                        for (e : type.elements) {
+                                val enumElemPred = createVLSFunction => [
+                                        it.constant = support.toIDMultiple("e", e.name, type.name)
+                                        it.terms += support.duplicate(variable)
+                                ]
+                                typeTrace.element2Predicate.put(e, enumElemPred)
+                                orElems.add(enumElemPred)
+                        }
 
                         val res = createVLSFofFormula => [
                                 it.name = support.toIDMultiple("typeDef", type.name)
                                 // below is temporary solution
                                 it.fofRole = "axiom"
                                 it.fofFormula = createVLSUniversalQuantifier => [
-                                        it.variables += createVLSVariable => [it.name = variable.name]
+                                        it.variables += support.duplicate(variable)
                                         it.operand = createVLSEquivalent => [
-                                                it.left = createVLSFunction => [
-                                                        it.constant = type.lookup(typeTrace.type2Predicate).constant
-                                                        it.terms += createVLSVariable => [it.name = "A"]
-                                                ]
-
-                                                type.lookup(typeTrace.type2Predicate)
-                                                it.right = support.unfoldOr(type.elements.map [ e |
-                                                        createVLSEquality => [
-                                                                it.left = createVLSVariable => [it.name = variable.name]
+//                                              it.left = createVLSFunction => [
+//                                                      it.constant = type.lookup(typeTrace.type2Predicate).constant
+//                                                      it.terms += createVLSVariable => [it.name = "A"]
+//                                              ]
+                                                it.left = type.lookup(typeTrace.type2Predicate)
+
+                                                it.right = support.unfoldOr(orElems)
+
+                                        // TEMPPPPPPP
+//                                              it.right = support.unfoldOr(type.elements.map [e |
+//                                                      
+//                                                      createVLSEquality => [
+//                                                              it.left = support.duplicate(variable)
 //                                                              it.right = createVLSDoubleQuote => [
-//                                                                      it.value = "\"" + e.name + "\""
+//                                                                      it.value = "\"a" + e.name + "\""
 //                                                              ]
-                                                                it.right = createVLSDoubleQuote => [
-                                                                        it.value = "\"a" + e.name + "\""
-                                                                ]
-                                                        ]
-                                                ])
+//                                                      ]
+//                                              ])
+                                        // END TEMPPPPP
                                         ]
                                 ]
 
                         ]
                         trace.specification.formulas += res
                 }
-                // 2.5. Currently allowing duplicate types. Not problematic cuz strings are by def unique
+                
+                //HIERARCHY HANDLER
+                
+                
                 // 3. For each non-abstract type, create an and sequence containing all typedeclaration predicates
                 // and store in a map
 //              val List<VLSTerm> type2PossibleNot = new ArrayList
@@ -97,19 +115,17 @@ class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Logic2Vamp
                 }
 
                 // 5. create fof function that is an or with all the elements in map
-                // Do this only if there are more than 1 type
+                
+                
+                
+                
                 val hierarch = createVLSFofFormula => [
                         it.name = "hierarchyHandler"
                         it.fofRole = "axiom"
                         it.fofFormula = createVLSUniversalQuantifier => [
                                 it.variables += createVLSVariable => [it.name = "A"]
                                 it.operand = createVLSEquivalent => [
-                                        it.left = createVLSFunction => [
-                                                it.constant = "object"
-                                                it.terms += createVLSVariable => [
-                                                        it.name = "A"
-                                                ]
-                                        ]
+                                        it.left = support.topLevelTypeFunc
                                         it.right = support.unfoldOr(new ArrayList<VLSTerm>(typeTrace.type2And.values))
                                 ]
                         ]
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.xtend
index 5cb0198e..9c9e65b4 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.xtend
@@ -4,63 +4,64 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
 import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultFactory

 

 class Vampire2LogicMapper {

-        val extension LogicresultFactory resultFactory = LogicresultFactory.eINSTANCE

-        

-        public def transformOutput(LogicProblem problem, int requiredNumberOfSolution, VampireSolutionModel vampireSolution, Logic2VampireLanguageMapperTrace trace, long transformationTime) {

-                val models = vampireSolution.aswers.map[it.key].toList

-                

-                if(!monitoredAlloySolution.finishedBeforeTimeout) {

-                        return createInsuficientResourcesResult => [

-                                it.problem = problem

-                                it.representation += models

-                                it.trace = trace

-                                it.statistics = transformStatistics(monitoredAlloySolution,transformationTime)

-                        ]

-                } else {

-                        if(models.last.satisfiable || requiredNumberOfSolution == -1) {

-                                return createModelResult => [

-                                        it.problem = problem

-                                        it.representation += models

-                                        it.trace = trace

-                                        it.statistics = transformStatistics(monitoredAlloySolution,transformationTime)

-                                ]

-                        } else {

-                                return createInconsistencyResult => [

-                                        it.problem = problem

-                                        it.representation += models

-                                        it.trace = trace

-                                        it.statistics = transformStatistics(monitoredAlloySolution,transformationTime)

-                                ]

-                        }

-                }

-        }

-        

-        def transformStatistics(MonitoredAlloySolution solution, long transformationTime) {

-                createStatistics => [

-                        it.transformationTime = transformationTime as int

-                        for(solutionIndex : 0..<solution.aswers.size) {

-                                val solutionTime = solution.aswers.get(solutionIndex).value

-                                 it.entries+= createIntStatisticEntry => [

-                                        it.name = '''Answer«solutionIndex»Time'''

-                                        it.value = solutionTime.intValue

-                                ]

-                        }

-                        it.entries+= createIntStatisticEntry => [

-                                it.name = "Alloy2KodKodTransformationTime"

-                                it.value = solution.kodkodTime as int

-                        ]

-                        it.entries+= createIntStatisticEntry => [

-                                it.name = "Alloy2KodKodTransformationTime"

-                                it.value = solution.kodkodTime as int

-                        ]

-                        it.entries+= createStringStatisticEntry => [

-                                it.name = "warnings"

-                                it.value = '''[«FOR warning : solution.warnings SEPARATOR ","»«warning»«ENDFOR»]'''

-                        ]

-                ]

-        }

-        

-        def sum(Iterable<Long> ints) {

-                ints.reduce[p1, p2|p1+p2]

-        }

 }

+//      val extension LogicresultFactory resultFactory = LogicresultFactory.eINSTANCE

+//      

+//      public def transformOutput(LogicProblem problem, int requiredNumberOfSolution, VampireSolutionModel vampireSolution, Logic2VampireLanguageMapperTrace trace, long transformationTime) {

+//              val models = vampireSolution.aswers.map[it.key].toList

+//              

+//              if(!monitoredAlloySolution.finishedBeforeTimeout) {

+//                      return createInsuficientResourcesResult => [

+//                              it.problem = problem

+//                              it.representation += models

+//                              it.trace = trace

+//                              it.statistics = transformStatistics(monitoredAlloySolution,transformationTime)

+//                      ]

+//              } else {

+//                      if(models.last.satisfiable || requiredNumberOfSolution == -1) {

+//                              return createModelResult => [

+//                                      it.problem = problem

+//                                      it.representation += models

+//                                      it.trace = trace

+//                                      it.statistics = transformStatistics(monitoredAlloySolution,transformationTime)

+//                              ]

+//                      } else {

+//                              return createInconsistencyResult => [

+//                                      it.problem = problem

+//                                      it.representation += models

+//                                      it.trace = trace

+//                                      it.statistics = transformStatistics(monitoredAlloySolution,transformationTime)

+//                              ]

+//                      }

+//              }

+//      }

+//      

+//      def transformStatistics(MonitoredAlloySolution solution, long transformationTime) {

+//              createStatistics => [

+//                      it.transformationTime = transformationTime as int

+//                      for(solutionIndex : 0..<solution.aswers.size) {

+//                              val solutionTime = solution.aswers.get(solutionIndex).value

+//                               it.entries+= createIntStatisticEntry => [

+//                                      it.name = '''Answer«solutionIndex»Time'''

+//                                      it.value = solutionTime.intValue

+//                              ]

+//                      }

+//                      it.entries+= createIntStatisticEntry => [

+//                              it.name = "Alloy2KodKodTransformationTime"

+//                              it.value = solution.kodkodTime as int

+//                      ]

+//                      it.entries+= createIntStatisticEntry => [

+//                              it.name = "Alloy2KodKodTransformationTime"

+//                              it.value = solution.kodkodTime as int

+//                      ]

+//                      it.entries+= createStringStatisticEntry => [

+//                              it.name = "warnings"

+//                              it.value = '''[«FOR warning : solution.warnings SEPARATOR ","»«warning»«ENDFOR»]'''

+//                      ]

+//              ]

+//      }

+//      

+//      def sum(Iterable<Long> ints) {

+//              ints.reduce[p1, p2|p1+p2]

+//      }

+//}

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 462a940b..9a2a1b15 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
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 d8b8ca61..ce05b92c 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
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.java
index e1a1ca6e..1846ba2e 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.java
@@ -10,6 +10,7 @@ import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Vampire2LogicMapper;
 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireHandler;

 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage;

 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel;

+import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel;

 import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicModelInterpretation;

 import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner;

 import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasonerException;

@@ -30,7 +31,8 @@ public class VampireSolver extends LogicReasoner {
     VampireLanguageStandaloneSetup.doSetup();

   }

   

-  private final Logic2VampireLanguageMapper forwardMapper = new Logic2VampireLanguageMapper(new Logic2VampireLanguageMapper_TypeMapper_FilteredTypes());

+  private final Logic2VampireLanguageMapper forwardMapper = new Logic2VampireLanguageMapper(

+    new Logic2VampireLanguageMapper_TypeMapper_FilteredTypes());

   

   private final Vampire2LogicMapper backwardMapper = new Vampire2LogicMapper();

   

@@ -48,7 +50,9 @@ public class VampireSolver extends LogicReasoner {
     String fileURI = null;

     String vampireCode = null;

     vampireCode = workspace.writeModelToString(vampireProblem, this.fileName);

-    if (vampireConfig.writeToFile) {

+    final boolean writeFile = ((vampireConfig.documentationLevel == DocumentationLevel.NORMAL) || 

+      (vampireConfig.documentationLevel == DocumentationLevel.FULL));

+    if (writeFile) {

       fileURI = workspace.writeModel(vampireProblem, this.fileName).toFileString();

     }

     long _currentTimeMillis = System.currentTimeMillis();

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolverConfiguration.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolverConfiguration.java
index d392016e..1f6b3d42 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolverConfiguration.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolverConfiguration.java
@@ -4,7 +4,4 @@ import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration;
 

 @SuppressWarnings("all")

 public class VampireSolverConfiguration extends LogicSolverConfiguration {

-  public int symmetry = 0;

-  

-  public boolean writeToFile = false;

 }

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 d248b361..379d0683 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
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 d747e8ab..76dd192f 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
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 4dc095c0..936ab9ca 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
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 9a948c6f..e0f442f5 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
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
new file mode 100644
index 00000000..493ff288
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin
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 4ef4809b..13281767 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
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 0f4acafe..1a777880 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
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.xtendbin
index 7d6865bb..e8658e7b 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtendbin
index 6db26bf7..aec1688a 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtendbin
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 8c96afa7..e77b9866 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
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 2427721d..100a52b8 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
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 d2c93ab4..231c1995 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
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 28c5d0f7..b67a307c 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
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.gitignore b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.gitignore
index 3d29fb07..ec8107e8 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.gitignore
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.gitignore
@@ -37,3 +37,4 @@
 /.VampireSolverException.java._trace
 /.VampireSolutionModel.java._trace
 /.VampireCallerWithTimeout.java._trace
+/.Logic2VampireLanguageMapper_ScopeMapper.java._trace
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java
index a1d80e58..89c9637e 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java
@@ -4,6 +4,7 @@ import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration;
 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace;

 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_ConstantMapper;

 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_RelationMapper;

+import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_ScopeMapper;

 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support;

 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_TypeMapper;

 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSComment;

@@ -84,6 +85,9 @@ public class Logic2VampireLanguageMapper {
   private final Logic2VampireLanguageMapper_RelationMapper relationMapper = new Logic2VampireLanguageMapper_RelationMapper(this);

   

   @Accessors(AccessorType.PUBLIC_GETTER)

+  private final Logic2VampireLanguageMapper_ScopeMapper scopeMapper = new Logic2VampireLanguageMapper_ScopeMapper(this);

+  

+  @Accessors(AccessorType.PUBLIC_GETTER)

   private final Logic2VampireLanguageMapper_TypeMapper typeMapper;

   

   public Logic2VampireLanguageMapper(final Logic2VampireLanguageMapper_TypeMapper typeMapper) {

@@ -112,6 +116,7 @@ public class Logic2VampireLanguageMapper {
     if (_not) {

       this.typeMapper.transformTypes(problem.getTypes(), problem.getElements(), this, trace);

     }

+    this.scopeMapper.transformScope(config, trace);

     trace.constantDefinitions = this.collectConstantDefinitions(problem);

     trace.relationDefinitions = this.collectRelationDefinitions(problem);

     final Consumer<Relation> _function_3 = (Relation it) -> {

@@ -316,13 +321,13 @@ public class Logic2VampireLanguageMapper {
   

   /**

    * def dispatch protected VLSTerm transformSymbolicReference(Relation relation,

-   * List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace,

-   * Map<Variable, VLSVariable> variables) {

-   * if (trace.relationDefinitions.containsKey(relation)) {

-   * this.transformSymbolicReference(relation.lookup(trace.relationDefinitions),

-   * parameterSubstitutions, trace, variables)

-   * }

-   * else {

+   *    List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace,

+   *    Map<Variable, VLSVariable> variables) {

+   *    if (trace.relationDefinitions.containsKey(relation)) {

+   *            this.transformSymbolicReference(relation.lookup(trace.relationDefinitions),

+   *                    parameterSubstitutions, trace, variables)

+   *    }

+   *    else {

    * //                                         if (relationMapper.transformToHostedField(relation, trace)) {

    * //                                                 val VLSRelation = relation.lookup(trace.relationDeclaration2Field)

    * //                                                 // R(a,b) =>

@@ -348,7 +353,7 @@ public class Logic2VampireLanguageMapper {
    * //                                                         rightOperand = target

    * //                                                 ]

    * //                                         }

-   * }

+   *    }

    * }

    */

   protected VLSTerm _transformSymbolicReference(final Relation relation, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {

@@ -436,6 +441,11 @@ public class Logic2VampireLanguageMapper {
   }

   

   @Pure

+  public Logic2VampireLanguageMapper_ScopeMapper getScopeMapper() {

+    return this.scopeMapper;

+  }

+  

+  @Pure

   public Logic2VampireLanguageMapper_TypeMapper getTypeMapper() {

     return this.typeMapper;

   }

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
new file mode 100644
index 00000000..86d8b648
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java
@@ -0,0 +1,96 @@
+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.VLSEquality;

+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquivalent;

+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula;

+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 org.eclipse.emf.common.util.EList;

+import org.eclipse.xtext.xbase.lib.CollectionLiterals;

+import org.eclipse.xtext.xbase.lib.Extension;

+import org.eclipse.xtext.xbase.lib.Functions.Function1;

+import org.eclipse.xtext.xbase.lib.ListExtensions;

+import org.eclipse.xtext.xbase.lib.ObjectExtensions;

+import org.eclipse.xtext.xbase.lib.Procedures.Procedure1;

+

+@SuppressWarnings("all")

+public class Logic2VampireLanguageMapper_ScopeMapper {

+  @Extension

+  private final VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE;

+  

+  private final Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support();

+  

+  private final Logic2VampireLanguageMapper base;

+  

+  public Logic2VampireLanguageMapper_ScopeMapper(final Logic2VampireLanguageMapper base) {

+    this.base = base;

+  }

+  

+  public void _transformScope(final LogicSolverConfiguration config, final Logic2VampireLanguageMapperTrace trace) {

+    VLSVariable _createVLSVariable = this.factory.createVLSVariable();

+    final Procedure1<VLSVariable> _function = (VLSVariable it) -> {

+      it.setName("A");

+    };

+    final VLSVariable variable = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function);

+    final List<VLSConstant> instances = CollectionLiterals.<VLSConstant>newArrayList();

+    for (int i = 0; (i < config.typeScopes.minNewElements); i++) {

+      {

+        final int num = (i + 1);

+        VLSConstant _createVLSConstant = this.factory.createVLSConstant();

+        final Procedure1<VLSConstant> _function_1 = (VLSConstant it) -> {

+          it.setName(("o" + Integer.valueOf(num)));

+        };

+        final VLSConstant cst = ObjectExtensions.<VLSConstant>operator_doubleArrow(_createVLSConstant, _function_1);

+        instances.add(cst);

+      }

+    }

+    VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula();

+    final Procedure1<VLSFofFormula> _function_1 = (VLSFofFormula it) -> {

+      it.setName("typeScope");

+      it.setFofRole("axiom");

+      VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();

+      final Procedure1<VLSUniversalQuantifier> _function_2 = (VLSUniversalQuantifier it_1) -> {

+        EList<VLSVariable> _variables = it_1.getVariables();

+        VLSVariable _duplicate = this.support.duplicate(variable);

+        _variables.add(_duplicate);

+        VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent();

+        final Procedure1<VLSEquivalent> _function_3 = (VLSEquivalent it_2) -> {

+          it_2.setLeft(this.support.topLevelTypeFunc());

+          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();

+              final Procedure1<VLSVariable> _function_6 = (VLSVariable it_4) -> {

+                it_4.setName(variable.getName());

+              };

+              VLSVariable _doubleArrow = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_1, _function_6);

+              it_3.setLeft(_doubleArrow);

+              it_3.setRight(i);

+            };

+            return ObjectExtensions.<VLSEquality>operator_doubleArrow(_createVLSEquality, _function_5);

+          };

+          it_2.setRight(this.support.unfoldOr(ListExtensions.<VLSConstant, VLSEquality>map(instances, _function_4)));

+        };

+        VLSEquivalent _doubleArrow = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_3);

+        it_1.setOperand(_doubleArrow);

+      };

+      VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_2);

+      it.setFofFormula(_doubleArrow);

+    };

+    final VLSFofFormula cstDec = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_1);

+    EList<VLSFofFormula> _formulas = trace.specification.getFormulas();

+    _formulas.add(cstDec);

+  }

+  

+  public void transformScope(final LogicSolverConfiguration config, final Logic2VampireLanguageMapperTrace trace) {

+    _transformScope(config, trace);

+    return;

+  }

+}

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 e1be7df5..b111732f 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
@@ -50,6 +50,29 @@ public class Logic2VampireLanguageMapper_Support {
     return IterableExtensions.join(((Iterable<?>)Conversions.doWrapArray(ids.split("\\s+"))), "_");

   }

   

+  protected VLSVariable duplicate(final VLSVariable vrbl) {

+    VLSVariable _createVLSVariable = this.factory.createVLSVariable();

+    final Procedure1<VLSVariable> _function = (VLSVariable it) -> {

+      it.setName(vrbl.getName());

+    };

+    return ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function);

+  }

+  

+  protected VLSFunction topLevelTypeFunc() {

+    VLSFunction _createVLSFunction = this.factory.createVLSFunction();

+    final Procedure1<VLSFunction> _function = (VLSFunction it) -> {

+      it.setConstant("object");

+      EList<VLSTerm> _terms = it.getTerms();

+      VLSVariable _createVLSVariable = this.factory.createVLSVariable();

+      final Procedure1<VLSVariable> _function_1 = (VLSVariable it_1) -> {

+        it_1.setName("A");

+      };

+      VLSVariable _doubleArrow = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_1);

+      _terms.add(_doubleArrow);

+    };

+    return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function);

+  }

+  

   protected VLSTerm unfoldAnd(final List<? extends VLSTerm> operands) {

     int _size = operands.size();

     boolean _equals = (_size == 1);

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.java
index d674ac71..f7c6cb70 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.java
@@ -1,7 +1,6 @@
 package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder;

 

 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_TypeMapperTrace;

-import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquality;

 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction;

 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm;

 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement;

@@ -13,7 +12,7 @@ import java.util.Map;
 public class Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes implements Logic2VampireLanguageMapper_TypeMapperTrace {

   public final Map<Type, VLSFunction> type2Predicate = new HashMap<Type, VLSFunction>();

   

-  public final Map<DefinedElement, VLSEquality> definedElement2Declaration = new HashMap<DefinedElement, VLSEquality>();

+  public final Map<DefinedElement, VLSFunction> element2Predicate = new HashMap<DefinedElement, VLSFunction>();

   

   public final Map<Type, VLSTerm> type2PossibleNot = new HashMap<Type, VLSTerm>();

   

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.java
index 0f5e4e7a..71e98871 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.java
@@ -7,7 +7,6 @@ import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguage
 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes;

 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireModelInterpretation_TypeInterpretation;

 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSDoubleQuote;

-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.VLSFunction;

@@ -27,10 +26,10 @@ import java.util.ArrayList;
 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.Extension;

 import org.eclipse.xtext.xbase.lib.Functions.Function1;

 import org.eclipse.xtext.xbase.lib.IterableExtensions;

-import org.eclipse.xtext.xbase.lib.ListExtensions;

 import org.eclipse.xtext.xbase.lib.ObjectExtensions;

 import org.eclipse.xtext.xbase.lib.Procedures.Procedure1;

 

@@ -58,14 +57,10 @@ public class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Log
       {

         VLSFunction _createVLSFunction = this.factory.createVLSFunction();

         final Procedure1<VLSFunction> _function_1 = (VLSFunction it) -> {

-          it.setConstant(this.support.toIDMultiple("type", type.getName()));

+          it.setConstant(this.support.toIDMultiple("t", type.getName()));

           EList<VLSTerm> _terms = it.getTerms();

-          VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable();

-          final Procedure1<VLSVariable> _function_2 = (VLSVariable it_1) -> {

-            it_1.setName(variable.getName());

-          };

-          VLSVariable _doubleArrow = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_1, _function_2);

-          _terms.add(_doubleArrow);

+          VLSVariable _duplicate = this.support.duplicate(variable);

+          _terms.add(_duplicate);

         };

         final VLSFunction typePred = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_1);

         typeTrace.type2Predicate.put(type, typePred);

@@ -74,6 +69,22 @@ public class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Log
     Iterable<TypeDefinition> _filter = Iterables.<TypeDefinition>filter(types, TypeDefinition.class);

     for (final TypeDefinition type_1 : _filter) {

       {

+        final List<VLSFunction> orElems = CollectionLiterals.<VLSFunction>newArrayList();

+        EList<DefinedElement> _elements = type_1.getElements();

+        for (final DefinedElement e : _elements) {

+          {

+            VLSFunction _createVLSFunction = this.factory.createVLSFunction();

+            final Procedure1<VLSFunction> _function_1 = (VLSFunction it) -> {

+              it.setConstant(this.support.toIDMultiple("e", e.getName(), type_1.getName()));

+              EList<VLSTerm> _terms = it.getTerms();

+              VLSVariable _duplicate = this.support.duplicate(variable);

+              _terms.add(_duplicate);

+            };

+            final VLSFunction enumElemPred = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_1);

+            typeTrace.element2Predicate.put(e, enumElemPred);

+            orElems.add(enumElemPred);

+          }

+        }

         VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula();

         final Procedure1<VLSFofFormula> _function_1 = (VLSFofFormula it) -> {

           it.setName(this.support.toIDMultiple("typeDef", type_1.getName()));

@@ -81,53 +92,15 @@ public class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Log
           VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();

           final Procedure1<VLSUniversalQuantifier> _function_2 = (VLSUniversalQuantifier it_1) -> {

             EList<VLSVariable> _variables = it_1.getVariables();

-            VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable();

-            final Procedure1<VLSVariable> _function_3 = (VLSVariable it_2) -> {

-              it_2.setName(variable.getName());

-            };

-            VLSVariable _doubleArrow = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_1, _function_3);

-            _variables.add(_doubleArrow);

+            VLSVariable _duplicate = this.support.duplicate(variable);

+            _variables.add(_duplicate);

             VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent();

-            final Procedure1<VLSEquivalent> _function_4 = (VLSEquivalent it_2) -> {

-              VLSFunction _createVLSFunction = this.factory.createVLSFunction();

-              final Procedure1<VLSFunction> _function_5 = (VLSFunction it_3) -> {

-                it_3.setConstant(CollectionsUtil.<TypeDefinition, VLSFunction>lookup(type_1, typeTrace.type2Predicate).getConstant());

-                EList<VLSTerm> _terms = it_3.getTerms();

-                VLSVariable _createVLSVariable_2 = this.factory.createVLSVariable();

-                final Procedure1<VLSVariable> _function_6 = (VLSVariable it_4) -> {

-                  it_4.setName("A");

-                };

-                VLSVariable _doubleArrow_1 = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_2, _function_6);

-                _terms.add(_doubleArrow_1);

-              };

-              VLSFunction _doubleArrow_1 = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_5);

-              it_2.setLeft(_doubleArrow_1);

-              CollectionsUtil.<TypeDefinition, VLSFunction>lookup(type_1, typeTrace.type2Predicate);

-              final Function1<DefinedElement, VLSEquality> _function_6 = (DefinedElement e) -> {

-                VLSEquality _createVLSEquality = this.factory.createVLSEquality();

-                final Procedure1<VLSEquality> _function_7 = (VLSEquality it_3) -> {

-                  VLSVariable _createVLSVariable_2 = this.factory.createVLSVariable();

-                  final Procedure1<VLSVariable> _function_8 = (VLSVariable it_4) -> {

-                    it_4.setName(variable.getName());

-                  };

-                  VLSVariable _doubleArrow_2 = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_2, _function_8);

-                  it_3.setLeft(_doubleArrow_2);

-                  VLSDoubleQuote _createVLSDoubleQuote = this.factory.createVLSDoubleQuote();

-                  final Procedure1<VLSDoubleQuote> _function_9 = (VLSDoubleQuote it_4) -> {

-                    String _name = e.getName();

-                    String _plus = ("\"a" + _name);

-                    String _plus_1 = (_plus + "\"");

-                    it_4.setValue(_plus_1);

-                  };

-                  VLSDoubleQuote _doubleArrow_3 = ObjectExtensions.<VLSDoubleQuote>operator_doubleArrow(_createVLSDoubleQuote, _function_9);

-                  it_3.setRight(_doubleArrow_3);

-                };

-                return ObjectExtensions.<VLSEquality>operator_doubleArrow(_createVLSEquality, _function_7);

-              };

-              it_2.setRight(this.support.unfoldOr(ListExtensions.<DefinedElement, VLSEquality>map(type_1.getElements(), _function_6)));

+            final Procedure1<VLSEquivalent> _function_3 = (VLSEquivalent it_2) -> {

+              it_2.setLeft(CollectionsUtil.<TypeDefinition, VLSFunction>lookup(type_1, typeTrace.type2Predicate));

+              it_2.setRight(this.support.unfoldOr(orElems));

             };

-            VLSEquivalent _doubleArrow_1 = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_4);

-            it_1.setOperand(_doubleArrow_1);

+            VLSEquivalent _doubleArrow = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_3);

+            it_1.setOperand(_doubleArrow);

           };

           VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_2);

           it.setFofFormula(_doubleArrow);

@@ -201,19 +174,7 @@ public class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Log
         _variables.add(_doubleArrow);

         VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent();

         final Procedure1<VLSEquivalent> _function_5 = (VLSEquivalent it_2) -> {

-          VLSFunction _createVLSFunction = this.factory.createVLSFunction();

-          final Procedure1<VLSFunction> _function_6 = (VLSFunction it_3) -> {

-            it_3.setConstant("object");

-            EList<VLSTerm> _terms = it_3.getTerms();

-            VLSVariable _createVLSVariable_2 = this.factory.createVLSVariable();

-            final Procedure1<VLSVariable> _function_7 = (VLSVariable it_4) -> {

-              it_4.setName("A");

-            };

-            VLSVariable _doubleArrow_1 = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_2, _function_7);

-            _terms.add(_doubleArrow_1);

-          };

-          VLSFunction _doubleArrow_1 = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_6);

-          it_2.setLeft(_doubleArrow_1);

+          it_2.setLeft(this.support.topLevelTypeFunc());

           Collection<VLSTerm> _values = typeTrace.type2And.values();

           ArrayList<VLSTerm> _arrayList = new ArrayList<VLSTerm>(_values);

           it_2.setRight(this.support.unfoldOr(_arrayList));

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.java
index f4380894..f4b5a1d2 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.java
@@ -1,59 +1,5 @@
 package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder;

 

-import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace;

-import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireSolutionModel;

-import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem;

-import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult;

-import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultFactory;

-import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.Statistics;

-import org.eclipse.xtext.xbase.lib.Extension;

-import org.eclipse.xtext.xbase.lib.Functions.Function2;

-import org.eclipse.xtext.xbase.lib.IterableExtensions;

-

 @SuppressWarnings("all")

 public class Vampire2LogicMapper {

-  @Extension

-  private final LogicresultFactory resultFactory = LogicresultFactory.eINSTANCE;

-  

-  public LogicResult transformOutput(final LogicProblem problem, final int requiredNumberOfSolution, final VampireSolutionModel vampireSolution, final Logic2VampireLanguageMapperTrace trace, final long transformationTime) {

-    throw new Error("Unresolved compilation problems:"

-      + "\nThe method or field aswers is undefined for the type VampireSolutionModel"

-      + "\nThe method or field key is undefined for the type Object"

-      + "\nThe method or field monitoredAlloySolution is undefined"

-      + "\nThe method or field monitoredAlloySolution is undefined"

-      + "\nThe method or field monitoredAlloySolution is undefined"

-      + "\nThe method or field monitoredAlloySolution is undefined"

-      + "\nThe method transformStatistics(MonitoredAlloySolution, long) from the type Vampire2LogicMapper refers to the missing type MonitoredAlloySolution"

-      + "\nThe method transformStatistics(MonitoredAlloySolution, long) from the type Vampire2LogicMapper refers to the missing type MonitoredAlloySolution"

-      + "\nThe method transformStatistics(MonitoredAlloySolution, long) from the type Vampire2LogicMapper refers to the missing type MonitoredAlloySolution"

-      + "\nmap cannot be resolved"

-      + "\ntoList cannot be resolved"

-      + "\nfinishedBeforeTimeout cannot be resolved"

-      + "\n! cannot be resolved"

-      + "\nlast cannot be resolved"

-      + "\nsatisfiable cannot be resolved"

-      + "\n|| cannot be resolved");

-  }

-  

-  public Statistics transformStatistics(final /* MonitoredAlloySolution */Object solution, final long transformationTime) {

-    throw new Error("Unresolved compilation problems:"

-      + "\nCannot cast from Object to int"

-      + "\nCannot cast from Object to int"

-      + "\naswers cannot be resolved"

-      + "\nsize cannot be resolved"

-      + "\naswers cannot be resolved"

-      + "\nget cannot be resolved"

-      + "\nvalue cannot be resolved"

-      + "\nintValue cannot be resolved"

-      + "\nkodkodTime cannot be resolved"

-      + "\nkodkodTime cannot be resolved"

-      + "\nwarnings cannot be resolved");

-  }

-  

-  public Long sum(final Iterable<Long> ints) {

-    final Function2<Long, Long, Long> _function = (Long p1, Long p2) -> {

-      return Long.valueOf(((p1).longValue() + (p2).longValue()));

-    };

-    return IterableExtensions.<Long>reduce(ints, _function);

-  }

 }

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireSolutionModel.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireSolutionModel.java
index c665b9a6..3c43c4ea 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireSolutionModel.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireSolutionModel.java
@@ -10,8 +10,7 @@ public class VampireSolutionModel {
   @Override

   @Pure

   public int hashCode() {

-    int result = 1;

-    return result;

+    return 1;

   }

   

   @Override

diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/initialModels/FAM/FamPatterns.vql b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/queries/FamPatterns.vql
index 013d0419..013d0419 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/initialModels/FAM/FamPatterns.vql
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/queries/FamPatterns.vql