VAMPIRE: Implement wf constraint handling

38 files changed, 305 insertions, 175 deletions

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 a0d8ad91..0aefc3c7 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 7f0974a6..f93445d1 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/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 e814f9af..4266e495 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 acbea6c4..ff67b75e 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 2b006891..67f6087a 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 4c2a01e7..ebd73974 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 f712428d..cdb3137a 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 db6e5d42..62560a49 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/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 4fc67b22..fe1c852f 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
@@ -23,9 +23,9 @@ class VampireLanguageFormatter extends AbstractFormatter2 {
                 for (VLSComment vLSComment : vampireModel.getComments()) {

                         vLSComment.format;

                 }

-//              for (VLSFofFormula vLSFofFormula : vampireModel.getFormulas()) {

-//                      vLSFofFormula.format;

-//              }

+                for (VLSFofFormula vLSFofFormula : vampireModel.getFormulas()) {

+                        vLSFofFormula.format;

+                }

         }

 

 //      def dispatch void format(VLSInclude vLSInclude, extension IFormattableDocument document) {

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 bc9ce4bc..a60c74b4 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 322bb058..63c46199 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 2bd5f5f8..b3a43b5a 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 0daa6fa5..48b973e7 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
@@ -29,6 +29,10 @@ public class VampireLanguageFormatter extends AbstractFormatter2 {
     for (final VLSComment vLSComment : _comments) {

       document.<VLSComment>format(vLSComment);

     }

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

+    for (final VLSFofFormula vLSFofFormula : _formulas) {

+      document.<VLSFofFormula>format(vLSFofFormula);

+    }

   }

   

   protected void _format(final VLSFofFormula formula, @Extension 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 c332270d..f3d705a1 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 60bd0c88..9e2e4cb2 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 fe1d6bf2..0ace8e93 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/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 a2449fc0..14926280 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
@@ -1,5 +1,10 @@
 package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder
 
+import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel
 import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.And
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Assertion
@@ -21,18 +26,14 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.InstanceOf
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntLiteral
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Not
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Or
-import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealLiteral
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.impl.RelationDefinitionImpl
 import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
-import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration
-import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm
-import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable
-import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory
-import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel
 import java.util.Collections
 import java.util.HashMap
 import java.util.List
@@ -40,7 +41,7 @@ import java.util.Map
 import org.eclipse.xtend.lib.annotations.Accessors
 
 import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
-import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.impl.RelationDeclarationImpl
 
 class Logic2VampireLanguageMapper {
         private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE
@@ -81,7 +82,8 @@ class Logic2VampireLanguageMapper {
                 
                 // RELATION MAPPER
                 trace.relationDefinitions = problem.collectRelationDefinitions
-                problem.relations.forEach[this.relationMapper.transformRelation(it, trace)]
+//              println(problem.relations.filter[class == RelationDefinitionImpl])
+                problem.relations.forEach[this.relationMapper.transformRelation(it, trace, new Logic2VampireLanguageMapper)]
                 
                 // CONTAINMENT MAPPER
                 containmentMapper.transformContainment(config,problem.containmentHierarchies, trace)
@@ -140,7 +142,7 @@ class Logic2VampireLanguageMapper {
         // ////////////
         def protected transformAssertion(Assertion assertion, Logic2VampireLanguageMapperTrace trace) {
                 val res = createVLSFofFormula => [
-                        it.name = support.toID(assertion.name)
+                        it.name = support.toID("assertion_" + assertion.name)
                         // below is temporary solution
                         it.fofRole = "axiom"
                         it.fofFormula = assertion.value.transformTerm(trace, Collections.EMPTY_MAP)
@@ -378,8 +380,18 @@ class Logic2VampireLanguageMapper {
 //                                              it.referredDefinition = relation.lookup(trace.relationDefinition2Predicate)
 //                                              it.params += parameterSubstitutions.map[p|p.transformTerm(trace, variables)]
 //                                      ]
+//              println(relation.name)
+//              if(relation.class == RelationDefinitionImpl) {
+//                      println("(" + (relation as RelationDefinition).getDefines + ")")
+//              }
                 return createVLSFunction => [
-                        it.constant = (relation as RelationDeclaration).lookup(trace.rel2Predicate).constant
+                        if (relation.class == RelationDeclarationImpl) {
+                                                        it.constant = (relation as RelationDeclaration).lookup(trace.rel2Predicate).constant
+                        }
+                        else {
+                                it.constant = (relation as RelationDefinition).lookup(trace.relDef2Predicate).constant
+                        }
+                        
                         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/Logic2VampireLanguageMapperTrace.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.xtend
index 6b383b12..13778dee 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.xtend
@@ -47,6 +47,8 @@ class Logic2VampireLanguageMapperTrace {
         public var Map<RelationDeclaration, RelationDefinition> relationDefinitions
         public var Map<RelationDeclaration, VLSFunction> rel2Predicate = new HashMap
         public var Map<VLSFunction, RelationDeclaration> predicate2Relation = new HashMap
+        public var Map<RelationDefinition, VLSFunction> relDef2Predicate = new HashMap
+        public var Map<VLSFunction, RelationDefinition> predicate2RelDef = new HashMap
         
         
 //NOT NEEDED    //public var VLSFunction constantDec
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_AssertionMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_AssertionMapper.xtend
new file mode 100644
index 00000000..cf218270
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_AssertionMapper.xtend
@@ -0,0 +1,5 @@
+package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder
+
+class Logic2VampireLanguageMapper_AssertionMapper {
+        
+}
\ 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_RelationMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend
index 18e97020..181c59ca 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend
@@ -1,14 +1,12 @@
 package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder
 
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction
+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.RelationDeclaration
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition
 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.VLSFofFormula
-import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory
 import java.util.ArrayList
 import java.util.HashMap
 import java.util.List
@@ -25,7 +23,7 @@ class Logic2VampireLanguageMapper_RelationMapper {
                 this.base = base
         }
 
-        def dispatch public void transformRelation(RelationDeclaration r, Logic2VampireLanguageMapperTrace trace) {
+        def dispatch public void transformRelation(RelationDeclaration r, Logic2VampireLanguageMapperTrace trace, Logic2VampireLanguageMapper mapper) {
 
                 // 1. store all variables in support wrt their name
                 // 1.1 if variable has type, creating list of type declarations
@@ -81,91 +79,79 @@ class Logic2VampireLanguageMapper_RelationMapper {
                 trace.specification.formulas += comply
         }
 
-        def dispatch public void transformRelation(RelationDefinition reldef, Logic2VampireLanguageMapperTrace trace) {
-
-//              // 1. store all variables in support wrt their name
-//              // 1.1 if variable has type, creating list of type declarations
-////            val VLSVariable variable = createVLSVariable => [it.name = "A"]
-//              val Map<Variable, VLSVariable> relationVar2VLS = new HashMap
-//              val Map<Variable, VLSFunction> relationVar2TypeDecComply = new HashMap
-//              val Map<Variable, VLSFunction> relationVar2TypeDecRes = new HashMap
-//              val typedefs = new ArrayList<VLSTerm>
-//
-//              for (variable : reldef.variables) {
-//                      val v = createVLSVariable => [
-//                              it.name = support.toIDMultiple("V", variable.name)
-//                      ]
-//                      relationVar2VLS.put(variable, v)
-//
-//                      val varTypeComply = createVLSFunction => [
-//                              it.constant = support.toIDMultiple("t", (variable.range as ComplexTypeReference).referred.name)
-//                              it.terms += support.duplicate(v)
-//                      ]
-//                      relationVar2TypeDecComply.put(variable, varTypeComply)
-//                      relationVar2TypeDecRes.put(variable, support.duplicate(varTypeComply))
-//              }
-//              val nameArray = reldef.name.split(" ")
-//              val comply = createVLSFofFormula => [
-//                      it.name = support.toIDMultiple("compliance", nameArray.get(nameArray.length - 2),
-//                              nameArray.get(nameArray.length - 1))
-//                      it.fofRole = "axiom"
-//                      it.fofFormula = createVLSUniversalQuantifier => [
-//                              for (variable : reldef.variables) {
-//                                      it.variables += support.duplicate(variable.lookup(relationVar2VLS))
-//
-//                              }
-//                              it.operand = createVLSImplies => [
-//                                      it.left = createVLSFunction => [
-//                                              it.constant = support.toIDMultiple("rel", reldef.name)
-//                                              for (variable : reldef.variables) {
-//                                                      val v = createVLSVariable => [
-//                                                              it.name = variable.lookup(relationVar2VLS).name
-//                                                      ]
-//                                                      it.terms += v
-//                                              }
-//                                      ]
-//                                      it.right = support.unfoldAnd(new ArrayList<VLSTerm>(relationVar2TypeDecComply.values))
-//                              ]
-//                      ]
-//              ]
-//
-//              val res = createVLSFofFormula => [
-//                      it.name = support.toIDMultiple("relation", nameArray.get(nameArray.length - 2),
-//                              nameArray.get(nameArray.length - 1))
-//                      it.fofRole = "axiom"
-//                      it.fofFormula = createVLSUniversalQuantifier => [
-//                              for (variable : reldef.variables) {
-//                                      val v = createVLSVariable => [
-//                                              it.name = variable.lookup(relationVar2VLS).name
-//                                      ]
-//                                      it.variables += v
-//
-//                              }
-//                              it.operand = createVLSImplies => [
-//                                      it.left = support.unfoldAnd(new ArrayList<VLSTerm>(relationVar2TypeDecRes.values))
-//                                      it.right = createVLSEquivalent => [
-//                                              it.left = createVLSFunction => [
-//                                                      it.constant = support.toIDMultiple("rel", reldef.name)
-//                                                      for (variable : reldef.variables) {
-//                                                              val v = createVLSVariable => [
-//                                                                      it.name = variable.lookup(relationVar2VLS).name
-//                                                              ]
-//                                                              it.terms += v
-//
-//                                                      }
-//                                              ]
-//                                              it.right = base.transformTerm(reldef.value, trace, relationVar2VLS)
-//                                      ]
-//
-//                              ]
-//
-//                      ]
-//
-//              ]
-//
-//              // trace.relationDefinition2Predicate.put(r,res)
-//              trace.specification.formulas += comply;
-//              trace.specification.formulas += res;
+        def dispatch public void transformRelation(RelationDefinition r, Logic2VampireLanguageMapperTrace trace, Logic2VampireLanguageMapper mapper) {
+                
+//              println("XXXXXXXXXXXXXXXXX")
+
+// 1. store all variables in support wrt their name
+                // 1.1 if variable has type, creating list of type declarations
+                val Map<Variable, VLSVariable> relVar2VLS = new HashMap
+                val List<VLSVariable> vars = newArrayList
+                val List<VLSFunction> relVar2TypeDecComply = new ArrayList
+                for (i : 0 ..< r.parameters.length) {
+
+                        val v = createVLSVariable => [
+                                it.name = support.toIDMultiple("V", i.toString)
+                        ]
+                        relVar2VLS.put(r.variables.get(i), v)
+                        vars.add(v)
+
+                        val relType = (r.parameters.get(i) as ComplexTypeReference).referred
+                        val varTypeComply = support.duplicate(relType.lookup(trace.type2Predicate), v)
+                        relVar2TypeDecComply.add(varTypeComply)
+
+                }
+
+                //deciding name of relation
+                val nameArray = r.name.split(" ")
+                var relNameVar = ""
+                if (nameArray.length == 3) {
+                        relNameVar = support.toIDMultiple(nameArray.get(0), nameArray.get(2))
+                }
+                else {
+                        relNameVar = r.name
+                }
+                val relName = relNameVar
+                
+                //define logic for pattern
+//              val map = new HashMap
+//              map.put(r.variables.get(0), createVLSVariable)
+                val definition = mapper.transformTerm(r.value, trace, relVar2VLS)
+                
+                
+                
+                
+                //get entire contents of and
+                val compliance = support.unfoldAnd(relVar2TypeDecComply)
+                val compDefn = createVLSAnd=> [
+                        it.left = compliance
+                        it.right = definition
+                ]
+                
+                val relDef = createVLSFofFormula=> [
+                        
+                        it.name = support.toID(relName)
+                        it.fofRole = "axiom"
+                        it.fofFormula = createVLSUniversalQuantifier => [
+                                for (v : vars) {
+                                        it.variables += support.duplicate(v)
+                                }
+                                it.operand = createVLSImplies => [
+                                        val rel = createVLSFunction => [
+                                                it.constant = support.toIDMultiple("r", relName)
+                                                for (v : vars) {
+                                                        it.terms += support.duplicate(v)
+                                                }
+                                        ]
+                                        trace.relDef2Predicate.put(r, rel)
+                                        trace.predicate2RelDef.put(rel, r)
+                                        it.left = support.duplicate(rel)
+                                        it.right = compDefn
+                                ]
+                        ]
+                ]
+
+                trace.specification.formulas += relDef
 
         }
 
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation.xtend
index 5df47bbc..ef77b6ca 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation.xtend
@@ -24,26 +24,28 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.impl.RelationDeclarationImpl
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.impl.TypeDeclarationImpl
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.impl.TypeDefinitionImpl
 import java.util.Arrays
 import java.util.HashMap
 import java.util.List
 import java.util.Map
-import java.util.Set
 
 import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
-import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.impl.TypeDefinitionImpl
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition
+import java.util.concurrent.TimeUnit
 
 class VampireModelInterpretation implements LogicModelInterpretation {
         protected val extension LogiclanguageFactory factory = LogiclanguageFactory.eINSTANCE
 
         protected val Logic2VampireLanguageMapperTrace forwardTrace;
 
-        //These three maps capture all the information found in the Vampire output
+        // These three maps capture all the information found in the Vampire output
         private val Map<String, DefinedElement> name2DefinedElement = new HashMap
         private val Map<TypeDeclaration, List<DefinedElement>> type2DefinedElement = new HashMap
-        private val Map<RelationDeclaration, List<String[]>> rel2Inst = new HashMap
-        //end
+        private val Map<RelationDeclaration, List<String[]>> relDec2Inst = new HashMap
+        private val Map<RelationDefinition, List<String[]>> relDef2Inst = new HashMap
 
+        // end
         public new(VampireModel model, Logic2VampireLanguageMapperTrace trace) {
                 this.forwardTrace = trace
 
@@ -77,6 +79,7 @@ class VampireModelInterpretation implements LogicModelInterpretation {
 //              println()
 //              println(trace.type2Predicate)
                 // Fill keys of map
+                println(trace.type2Predicate.keySet)
                 val allTypeDecls = trace.type2Predicate.keySet.filter[class == TypeDeclarationImpl]
                 val allTypeFunctions = trace.predicate2Type
                 println(trace.type2Predicate.keySet.filter[class == TypeDefinitionImpl])
@@ -86,52 +89,64 @@ class VampireModelInterpretation implements LogicModelInterpretation {
                 }
 
                 // USE THE DECLARE_<TYPE_NAME> FORMULAS TO SEE WHAT THE TYPES ARE
-                val typeFormulas = model.tfformulas.filter[name.length > 12 && name.substring(0, 12) == "predicate_t_"]
+                val typeFormulas = model.tfformulas.filter [
+                        name.length > 12 && (name.substring(0, 12) == "predicate_t_" || name.substring(0, 12) == "predicate_e_")
+                ]
                 // ^this way, we ignore the "object" type
-                //TODO potentially need to handle the enums in this case as well
+                // TODO potentially need to handle the enums in this case as well
                 for (formula : typeFormulas) {
                         // get associated type
                         val associatedTypeName = (formula as VLSTffFormula).name.substring(10)
-                        val associatedFunction = allTypeFunctions.keySet.filter[constant == associatedTypeName].
-                                get(0) as VLSFunction
-                        val associatedTypeAll = associatedFunction.lookup(allTypeFunctions)
+                        print(associatedTypeName)
+                        val associatedFunctions = allTypeFunctions.keySet.filter[constant == associatedTypeName]
+                        if (associatedFunctions.length > 0) {
+                                val associatedFunction = associatedFunctions.get(0) as VLSFunction
+                                val associatedTypeAll = associatedFunction.lookup(allTypeFunctions)
 //                      val associatedTypeDeclFormula = model.tfformulas.filter[name == ("declare_t_" + associatedTypeName)].get(0) as VLSTffFormula
 //                      val associatedTypeDefn = associatedTypeDeclFormula.fofFormula as VLSOtherDeclaration
 //                      val associatedTypeFct = associatedTypeDefn.name as VLSConstant
-                        if (associatedTypeAll.class == TypeDeclarationImpl) {
-                                val associatedType = associatedTypeAll as TypeDeclaration
+                                if (associatedTypeAll.class == TypeDeclarationImpl) {
+                                        val associatedType = associatedTypeAll as TypeDeclaration
+
+                                        // get definedElements
+                                        var andFormulaTerm = formula.fofFormula
+                                        end = false
+                                        val List<DefinedElement> instances = newArrayList
+                                        while (!end) {
+                                                if (andFormulaTerm.class == VLSAndImpl) {
+                                                        val andFormula = andFormulaTerm as VLSAnd
+                                                        val andRight = andFormula.right
+                                                        addIfNotNeg(andRight, instances)
+                                                        andFormulaTerm = andFormula.left
+                                                } else {
+                                                        addIfNotNeg(andFormulaTerm as VLSTerm, instances)
+                                                        end = true
+                                                }
 
-                                // get definedElements
-                                var andFormulaTerm = formula.fofFormula
-                                end = false
-                                val List<DefinedElement> instances = newArrayList
-                                while (!end) {
-                                        if (andFormulaTerm.class == VLSAndImpl) {
-                                                val andFormula = andFormulaTerm as VLSAnd
-                                                val andRight = andFormula.right
-                                                addIfNotNeg(andRight, instances)
-                                                andFormulaTerm = andFormula.left
-                                        } else {
-                                                addIfNotNeg(andFormulaTerm as VLSTerm, instances)
-                                                end = true
                                         }
-
-                                }
-                                for (elem : instances) {
-                                        associatedType.lookup(type2DefinedElement).add(elem)
+                                        for (elem : instances) {
+                                                associatedType.lookup(type2DefinedElement).add(elem)
+                                        }
                                 }
                         }
+
                 }
-                
+
                 printMap()
-                
+
                 // 3. get relations
                 // Fill keys of map
-                val allRelDecls = trace.rel2Predicate.keySet.filter[class == RelationDeclarationImpl]
-                val allRelFunctions = trace.predicate2Relation
+                val allRelDecls = trace.rel2Predicate.keySet
+                val allRelDefns = trace.relDef2Predicate.keySet
+                val allRelDeclFunctions = trace.predicate2Relation
+                val allRelDefnFunctions = trace.predicate2RelDef
 
                 for (rel : allRelDecls) {
-                        rel2Inst.put(rel as RelationDeclaration, newArrayList)
+                        relDec2Inst.put(rel as RelationDeclaration, newArrayList)
+                }
+
+                for (rel : allRelDefns) {
+                        relDef2Inst.put(rel as RelationDefinition, newArrayList)
                 }
 
                 // USE THE DECLARE_<RELATION_NAME> FORMULAS TO SEE WHAT THE RELATIONS ARE
@@ -140,34 +155,40 @@ class VampireModelInterpretation implements LogicModelInterpretation {
                 for (formula : relFormulas) {
                         // get associated type
                         val associatedRelName = (formula as VLSTffFormula).name.substring(10)
-                        val associatedRelFunction = allRelFunctions.keySet.filter[constant == associatedRelName].
-                                get(0) as VLSFunction
-                        val associatedRel = associatedRelFunction.lookup(allRelFunctions) as RelationDeclaration
-
-                        // get definedElements
-                        var andFormulaTerm = formula.fofFormula
-                        end = false
-                        val List<String[]> instances = newArrayList
-                        while (!end) {
-                                if (andFormulaTerm.class == VLSAndImpl) {
-                                        val andFormula = andFormulaTerm as VLSAnd
-                                        val andRight = andFormula.right
-                                        addRelIfNotNeg(andRight, instances)
-                                        andFormulaTerm = andFormula.left
-                                } else {
-                                        addRelIfNotNeg(andFormulaTerm as VLSTerm, instances)
-                                        end = true
+
+                        // TRY FOR DECLARATION
+                        val associatedRelFunctionList = allRelDeclFunctions.keySet.filter[constant == associatedRelName]
+                        if (associatedRelFunctionList.isEmpty) {
+                                // THEN IT IS NOT A DECLARATION
+                        } else {
+                                val associatedRelFunction = associatedRelFunctionList.get(0) as VLSFunction // ASSUMING ONLY 1 SATISFIES QUERY
+                                val associatedRel = associatedRelFunction.lookup(allRelDeclFunctions) as RelationDeclaration
+
+                                // get definedElements
+                                var andFormulaTerm = formula.fofFormula
+                                end = false
+                                val List<String[]> instances = newArrayList
+                                while (!end) {
+                                        if (andFormulaTerm.class == VLSAndImpl) {
+                                                val andFormula = andFormulaTerm as VLSAnd
+                                                val andRight = andFormula.right
+                                                addRelIfNotNeg(andRight, instances)
+                                                andFormulaTerm = andFormula.left
+                                        } else {
+                                                addRelIfNotNeg(andFormulaTerm as VLSTerm, instances)
+                                                end = true
+                                        }
+
+                                }
+                                for (elem : instances) {
+                                        associatedRel.lookup(relDec2Inst).add(elem)
                                 }
 
                         }
-                        for (elem : instances) {
-                                associatedRel.lookup(rel2Inst).add(elem)
-                        }
 
                 }
 
 //              printMap2()
-
         }
 
         def printMap() {
@@ -182,12 +203,12 @@ class VampireModelInterpretation implements LogicModelInterpretation {
                 }
                 println()
         }
-        
+
         def printMap2() {
                 println("------------------")
-                for (key : rel2Inst.keySet) {
+                for (key : relDec2Inst.keySet) {
                         println(key.name + "==>")
-                        for (elem : key.lookup(rel2Inst)) {
+                        for (elem : key.lookup(relDec2Inst)) {
                                 print("[" + elem.get(0) + "-" + elem.get(1) + "], ")
                         }
                         println()
@@ -203,7 +224,7 @@ class VampireModelInterpretation implements LogicModelInterpretation {
                         list.add(defnElem)
                 }
         }
-        
+
         def private addRelIfNotNeg(VLSTerm term, List<String[]> list) {
                 if (term.class != VLSUnaryNegationImpl) {
                         val nodeName1 = ((term as VLSFunction).terms.get(0) as VLSFunctionAsTerm).functor
@@ -232,14 +253,19 @@ class VampireModelInterpretation implements LogicModelInterpretation {
         }
 
         override getInterpretation(RelationDeclaration relation, Object[] parameterSubstitution) {
+                print("-- " + relation.name)
                 val node1 = (parameterSubstitution.get(0) as DefinedElement).name
                 val node2 = (parameterSubstitution.get(1) as DefinedElement).name
-                val realRelations = relation.lookup(rel2Inst)
-                for (real : realRelations){
-                        if(real.contains(node1) && real.contains(node2)){
+                val realRelations = relation.lookup(relDec2Inst)
+                for (real : realRelations) {
+                        if (real.contains(node1) && real.contains(node2)) {
+                                println("  true")
+                                TimeUnit.SECONDS.sleep(1)
                                 return true
                         }
                 }
+                println("  false")
+                TimeUnit.SECONDS.sleep(1)
                 return false
         }
 
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 a1d6f783..972af7b4 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 6ac0457b..071db3ce 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/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 f5991439..b1e3b95d 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 0d6c8b61..31cc2f43 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 659d4637..552bcd6c 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_ContainmentMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin
index 927327e1..680bcfe1 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.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 d8fc0296..9cc64d7c 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
index bc3caa3b..803b5fed 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin
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 299c4e0c..0083e90f 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 da8c1d26..7e8b1703 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/.Vampire2LogicMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin
index adc3fff4..081757ca 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 2ab5b32f..3471f95b 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 41af19ec..1c707ca6 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 2b46d5c2..d8e3808c 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/Logic2VampireLanguageMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java
index 58da7ccd..f8a65187 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
@@ -21,6 +21,7 @@ import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUnaryNegation;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable;

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

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

+import com.google.common.base.Objects;

 import com.google.common.collect.Iterables;

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

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

@@ -52,6 +53,7 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term;
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type;

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

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

+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.impl.RelationDeclarationImpl;

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

 import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil;

 import java.util.Arrays;

@@ -117,7 +119,8 @@ public class Logic2VampireLanguageMapper {
     }

     trace.relationDefinitions = this.collectRelationDefinitions(problem);

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

-      this.relationMapper.transformRelation(it, trace);

+      Logic2VampireLanguageMapper _logic2VampireLanguageMapper = new Logic2VampireLanguageMapper();

+      this.relationMapper.transformRelation(it, trace, _logic2VampireLanguageMapper);

     };

     problem.getRelations().forEach(_function_3);

     this.containmentMapper.transformContainment(config, problem.getContainmentHierarchies(), trace);

@@ -169,7 +172,9 @@ public class Logic2VampireLanguageMapper {
     {

       VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula();

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

-        it.setName(this.support.toID(assertion.getName()));

+        String _name = assertion.getName();

+        String _plus = ("assertion_" + _name);

+        it.setName(this.support.toID(_plus));

         it.setFofRole("axiom");

         it.setFofFormula(this.transformTerm(assertion.getValue(), trace, Collections.EMPTY_MAP));

       };

@@ -346,7 +351,13 @@ public class Logic2VampireLanguageMapper {
   protected VLSTerm _transformSymbolicReference(final Relation relation, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {

     VLSFunction _createVLSFunction = this.factory.createVLSFunction();

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

-      it.setConstant(CollectionsUtil.<RelationDeclaration, VLSFunction>lookup(((RelationDeclaration) relation), trace.rel2Predicate).getConstant());

+      Class<? extends Relation> _class = relation.getClass();

+      boolean _equals = Objects.equal(_class, RelationDeclarationImpl.class);

+      if (_equals) {

+        it.setConstant(CollectionsUtil.<RelationDeclaration, VLSFunction>lookup(((RelationDeclaration) relation), trace.rel2Predicate).getConstant());

+      } else {

+        it.setConstant(CollectionsUtil.<RelationDefinition, VLSFunction>lookup(((RelationDefinition) relation), trace.relDef2Predicate).getConstant());

+      }

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

       final Function1<Term, VLSTerm> _function_1 = (Term p) -> {

         return this.transformTerm(p, trace, variables);

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java
index 4e77d45d..22df456b 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java
@@ -55,6 +55,10 @@ public class Logic2VampireLanguageMapperTrace {
   

   public Map<VLSFunction, RelationDeclaration> predicate2Relation = new HashMap<VLSFunction, RelationDeclaration>();

   

+  public Map<RelationDefinition, VLSFunction> relDef2Predicate = new HashMap<RelationDefinition, VLSFunction>();

+  

+  public Map<VLSFunction, RelationDefinition> predicate2RelDef = new HashMap<VLSFunction, RelationDefinition>();

+  

   public final Map<Variable, VLSVariable> relationVar2VLS = new HashMap<Variable, VLSVariable>();

   

   public final Map<Variable, VLSFunction> relationVar2TypeDec = new HashMap<Variable, VLSFunction>();

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java
index 143d3db5..c175c72a 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java
@@ -3,6 +3,7 @@ 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.VLSAnd;

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

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

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

@@ -17,11 +18,15 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration;
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition;

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

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

+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable;

 import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil;

 import java.util.ArrayList;

 import java.util.Arrays;

+import java.util.HashMap;

 import java.util.List;

+import java.util.Map;

 import org.eclipse.emf.common.util.EList;

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

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

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

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

@@ -41,7 +46,7 @@ public class Logic2VampireLanguageMapper_RelationMapper {
     this.base = base;

   }

   

-  public void _transformRelation(final RelationDeclaration r, final Logic2VampireLanguageMapperTrace trace) {

+  public void _transformRelation(final RelationDeclaration r, final Logic2VampireLanguageMapperTrace trace, final Logic2VampireLanguageMapper mapper) {

     final List<VLSVariable> relVar2VLS = new ArrayList<VLSVariable>();

     final List<VLSFunction> relVar2TypeDecComply = new ArrayList<VLSFunction>();

     int _length = ((Object[])Conversions.unwrapArray(r.getParameters(), Object.class)).length;

@@ -109,19 +114,94 @@ public class Logic2VampireLanguageMapper_RelationMapper {
     _formulas.add(comply);

   }

   

-  public void _transformRelation(final RelationDefinition reldef, final Logic2VampireLanguageMapperTrace trace) {

+  public void _transformRelation(final RelationDefinition r, final Logic2VampireLanguageMapperTrace trace, final Logic2VampireLanguageMapper mapper) {

+    final Map<Variable, VLSVariable> relVar2VLS = new HashMap<Variable, VLSVariable>();

+    final List<VLSVariable> vars = CollectionLiterals.<VLSVariable>newArrayList();

+    final List<VLSFunction> relVar2TypeDecComply = new ArrayList<VLSFunction>();

+    int _length = ((Object[])Conversions.unwrapArray(r.getParameters(), Object.class)).length;

+    ExclusiveRange _doubleDotLessThan = new ExclusiveRange(0, _length, true);

+    for (final Integer i : _doubleDotLessThan) {

+      {

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

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

+          it.setName(this.support.toIDMultiple("V", i.toString()));

+        };

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

+        relVar2VLS.put(r.getVariables().get((i).intValue()), v);

+        vars.add(v);

+        TypeReference _get = r.getParameters().get((i).intValue());

+        final Type relType = ((ComplexTypeReference) _get).getReferred();

+        final VLSFunction varTypeComply = this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(relType, trace.type2Predicate), v);

+        relVar2TypeDecComply.add(varTypeComply);

+      }

+    }

+    final String[] nameArray = r.getName().split(" ");

+    String relNameVar = "";

+    int _length_1 = nameArray.length;

+    boolean _equals = (_length_1 == 3);

+    if (_equals) {

+      relNameVar = this.support.toIDMultiple(nameArray[0], nameArray[2]);

+    } else {

+      relNameVar = r.getName();

+    }

+    final String relName = relNameVar;

+    final VLSTerm definition = mapper.transformTerm(r.getValue(), trace, relVar2VLS);

+    final VLSTerm compliance = this.support.unfoldAnd(relVar2TypeDecComply);

+    VLSAnd _createVLSAnd = this.factory.createVLSAnd();

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

+      it.setLeft(compliance);

+      it.setRight(definition);

+    };

+    final VLSAnd compDefn = ObjectExtensions.<VLSAnd>operator_doubleArrow(_createVLSAnd, _function);

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

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

+      it.setName(this.support.toID(relName));

+      it.setFofRole("axiom");

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

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

+        for (final VLSVariable v : vars) {

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

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

+          _variables.add(_duplicate);

+        }

+        VLSImplies _createVLSImplies = this.factory.createVLSImplies();

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

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

+          final Procedure1<VLSFunction> _function_4 = (VLSFunction it_3) -> {

+            it_3.setConstant(this.support.toIDMultiple("r", relName));

+            for (final VLSVariable v_1 : vars) {

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

+              VLSVariable _duplicate_1 = this.support.duplicate(v_1);

+              _terms.add(_duplicate_1);

+            }

+          };

+          final VLSFunction rel = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_4);

+          trace.relDef2Predicate.put(r, rel);

+          trace.predicate2RelDef.put(rel, r);

+          it_2.setLeft(this.support.duplicate(rel));

+          it_2.setRight(compDefn);

+        };

+        VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_3);

+        it_1.setOperand(_doubleArrow);

+      };

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

+      it.setFofFormula(_doubleArrow);

+    };

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

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

+    _formulas.add(relDef);

   }

   

-  public void transformRelation(final Relation r, final Logic2VampireLanguageMapperTrace trace) {

+  public void transformRelation(final Relation r, final Logic2VampireLanguageMapperTrace trace, final Logic2VampireLanguageMapper mapper) {

     if (r instanceof RelationDeclaration) {

-      _transformRelation((RelationDeclaration)r, trace);

+      _transformRelation((RelationDeclaration)r, trace, mapper);

       return;

     } else if (r instanceof RelationDefinition) {

-      _transformRelation((RelationDefinition)r, trace);

+      _transformRelation((RelationDefinition)r, trace, mapper);

       return;

     } else {

       throw new IllegalArgumentException("Unhandled parameter types: " +

-        Arrays.<Object>asList(r, trace).toString());

+        Arrays.<Object>asList(r, trace, mapper).toString());

     }

   }

 }