Implement type scope handling

76 files changed, 1267 insertions, 537 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 7bfd4e09..fef8d621 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 4c4cd6a3..3c37bd02 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 dedb3ece..76127556 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 a6d502ef..467395cb 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 b2dc17a0..601c5a4c 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 73d9cdd1..c60c4d59 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 7880fdd6..030267ff 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 6a8836d4..ef7ffcdf 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/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 e0367170..219fec58 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 906c39f5..47712412 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 47a395a0..831f0df4 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/generator/.VampireLanguageGenerator.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/generator/.VampireLanguageGenerator.xtendbin
index 74f517cf..696d67c0 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 3c09270e..9bef3ff9 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 96e8559a..dd65afb4 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 e2c15b75..54c44c72 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
@@ -238,7 +238,7 @@ class Logic2VampireLanguageMapper {
         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("t", (instanceOf.range as ComplexTypeReference).referred.name)
                         it.terms += instanceOf.value.transformTerm(trace, variables)
                 ]
         }
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 60653a42..6f3b13ef 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
@@ -39,7 +39,7 @@ class Logic2VampireLanguageMapper_RelationMapper {
                         relationVar2VLS.put(variable, v)
 
                         val varTypeComply = createVLSFunction => [
-                                it.constant = support.toIDMultiple("type", (variable.range as ComplexTypeReference).referred.name)
+                                it.constant = support.toIDMultiple("t", (variable.range as ComplexTypeReference).referred.name)
                                 it.terms += createVLSVariable => [
                                         it.name = support.toIDMultiple("Var", variable.name)
                                 ]
@@ -47,7 +47,7 @@ class Logic2VampireLanguageMapper_RelationMapper {
                         relationVar2TypeDecComply.put(variable, varTypeComply)
                         
                         val varTypeRes = createVLSFunction => [
-                                it.constant = support.toIDMultiple("type", (variable.range as ComplexTypeReference).referred.name)
+                                it.constant = support.toIDMultiple("t", (variable.range as ComplexTypeReference).referred.name)
                                 it.terms += createVLSVariable => [
                                         it.name = support.toIDMultiple("Var", variable.name)
                                 ]
@@ -136,7 +136,7 @@ class Logic2VampireLanguageMapper_RelationMapper {
                         relationVar2VLS.add(v)
 
                         val varTypeComply = createVLSFunction => [
-                                it.constant = support.toIDMultiple("type", (r.parameters.get(i) as ComplexTypeReference).referred.name)
+                                it.constant = support.toIDMultiple("t", (r.parameters.get(i) as ComplexTypeReference).referred.name)
                                 it.terms += createVLSVariable => [
                                         it.name = support.toIDMultiple("Var", i.toString)
                                 ]
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend
index 84aa521d..4b7ea3d0 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend
@@ -18,7 +18,6 @@ class Logic2VampireLanguageMapper_ScopeMapper {
         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++) {

@@ -28,47 +27,37 @@ class Logic2VampireLanguageMapper_ScopeMapper {
                         ]

                         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

-                                                ]

-                                        ])

+                // TODO: specify for the max

+                if (config.typeScopes.minNewElements != 0) {

+                        // 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

+                        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.establishUniqueness(instances)

+                        ]

+                        trace.specification.formulas += uniqueness

+                }

         }

 }

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend
index e69f0d51..06ec585c 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
@@ -13,6 +13,8 @@ import java.util.HashMap
 import java.util.List
 import java.util.Map
 import org.eclipse.emf.common.util.EList
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSInequality
 
 class Logic2VampireLanguageMapper_Support {
         private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE
@@ -26,6 +28,7 @@ class Logic2VampireLanguageMapper_Support {
                 ids.split("\\s+").join("_")
         }
 
+        //TODO Make more general
         def protected VLSVariable duplicate(VLSVariable vrbl) {
                 return createVLSVariable => [it.name = vrbl.name]
         }
@@ -38,6 +41,25 @@ class Logic2VampireLanguageMapper_Support {
                         ]
                 ]
         }
+        
+        //TODO Make more general
+        def establishUniqueness(List<VLSConstant> terms) {
+                val List<VLSInequality> eqs = newArrayList
+                for (t1 : terms.subList(1, terms.length)){
+                        for (t2 : terms.subList(0, terms.indexOf(t1))){
+                                val eq = createVLSInequality => [
+                                        //TEMP
+                                        it.left = createVLSConstant => [it.name = t2.name]
+                                        it.right = createVLSConstant => [it.name = t1.name]
+                                        //TEMP
+                                ]
+                                eqs.add(eq)
+                        }                       
+                }
+                
+                return unfoldAnd(eqs)
+                
+        }
 
         // Support Functions
         // booleans
@@ -111,7 +133,7 @@ class Logic2VampireLanguageMapper_Support {
                 val typedefs = new ArrayList<VLSTerm>
                 for (variable : expression.quantifiedVariables) {
                         val eq = createVLSFunction => [
-                                it.constant = toIDMultiple("type", (variable.range as ComplexTypeReference).referred.name)
+                                it.constant = toIDMultiple("t", (variable.range as ComplexTypeReference).referred.name)
                                 it.terms += createVLSVariable => [
                                         it.name = toIDMultiple("Var", variable.name)
                                 ]
@@ -138,7 +160,7 @@ class Logic2VampireLanguageMapper_Support {
                 val typedefs = new ArrayList<VLSTerm>
                 for (variable : expression.quantifiedVariables) {
                         val eq = createVLSFunction => [
-                                it.constant = toIDMultiple("type", (variable.range as ComplexTypeReference).referred.name)
+                                it.constant = toIDMultiple("t", (variable.range as ComplexTypeReference).referred.name)
                                 it.terms += createVLSVariable => [
                                         it.name = toIDMultiple("Var", variable.name)
                                 ]
@@ -157,5 +179,7 @@ class Logic2VampireLanguageMapper_Support {
         def protected withAddition(Map<Variable, VLSVariable> map1, Map<Variable, VLSVariable> map2) {
                 new HashMap(map1) => [putAll(map2)]
         }
+        
+        
 
 }
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 eed10656..88e1e23a 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
@@ -89,27 +89,25 @@ class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Logic2Vamp
                 
                 // 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
-//              val List<VLSTerm> type2And = new ArrayList
-                for (type : types.filter[!isIsAbstract]) {
-                        for (type2 : types) {
+                for (t1 : types.filter[!isIsAbstract]) {
+                        for (t2 : types) {
                                 // possible improvement: check all supertypes and decide if negated or not based on negations/not negations of supertypes
-                                if (type == type2 || dfsSupertypeCheck(type, type2)) {
-                                        typeTrace.type2PossibleNot.put(type2, createVLSFunction => [
-                                                it.constant = type2.lookup(typeTrace.type2Predicate).constant
-                                                it.terms += createVLSVariable => [it.name = "A"]
+                                if (t1 == t2 || dfsSupertypeCheck(t1, t2)) {
+                                        typeTrace.type2PossibleNot.put(t2, createVLSFunction => [
+                                                it.constant = t2.lookup(typeTrace.type2Predicate).constant
+                                                it.terms += support.duplicate(variable)
                                         ])
                                 } else {
-                                        typeTrace.type2PossibleNot.put(type2, createVLSUnaryNegation => [
+                                        typeTrace.type2PossibleNot.put(t2, createVLSUnaryNegation => [
                                                 it.operand = createVLSFunction => [
-                                                        it.constant = type2.lookup(typeTrace.type2Predicate).constant
-                                                        it.terms += createVLSVariable => [it.name = "A"]
+                                                        it.constant = t2.lookup(typeTrace.type2Predicate).constant
+                                                        it.terms += support.duplicate(variable)
                                                 ]
                                         ])
                                 }
 //                              typeTrace.type2PossibleNot.put(type2, type2.lookup(typeTrace.type2Predicate))
                         }
-                        typeTrace.type2And.put(type, support.unfoldAnd(new ArrayList<VLSTerm>(typeTrace.type2PossibleNot.values)))
+                        typeTrace.type2And.put(t1, support.unfoldAnd(new ArrayList<VLSTerm>(typeTrace.type2PossibleNot.values)))
 //                      typeTrace.type2And.put(type, type.lookup(typeTrace.type2Predicate) )
                         typeTrace.type2PossibleNot.clear
                 }
@@ -123,7 +121,7 @@ class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Logic2Vamp
                         it.name = "hierarchyHandler"
                         it.fofRole = "axiom"
                         it.fofFormula = createVLSUniversalQuantifier => [
-                                it.variables += createVLSVariable => [it.name = "A"]
+                                it.variables += support.duplicate(variable)
                                 it.operand = createVLSEquivalent => [
                                         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/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 9a2a1b15..4a4eedf5 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 ce05b92c..55f0ac1e 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 379d0683..e91f89cc 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 76dd192f..154ff393 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 936ab9ca..5d6ad730 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 e0f442f5..7c787543 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 493ff288..34f3b285 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 13281767..f8d6cd3f 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 1a777880..7b2b11f8 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 e8658e7b..7e8336e2 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 aec1688a..a2229dba 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 e77b9866..d82649ff 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 100a52b8..030a0be9 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 231c1995..87203ed8 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 b67a307c..65689b0c 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 89c9637e..6643576f 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
@@ -273,7 +273,7 @@ public class Logic2VampireLanguageMapper {
     VLSFunction _createVLSFunction = this.factory.createVLSFunction();

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

       TypeReference _range = instanceOf.getRange();

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

+      it.setConstant(this.support.toIDMultiple("t", ((ComplexTypeReference) _range).getReferred().getName()));

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

       VLSTerm _transformTerm = this.transformTerm(instanceOf.getValue(), trace, variables);

       _terms.add(_transformTerm);

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 561402a7..bce50fcc 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
@@ -61,7 +61,7 @@ public class Logic2VampireLanguageMapper_RelationMapper {
         VLSFunction _createVLSFunction = this.factory.createVLSFunction();

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

           TypeReference _range = variable.getRange();

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

+          it.setConstant(this.support.toIDMultiple("t", ((ComplexTypeReference) _range).getReferred().getName()));

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

           VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable();

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

@@ -75,7 +75,7 @@ public class Logic2VampireLanguageMapper_RelationMapper {
         VLSFunction _createVLSFunction_1 = this.factory.createVLSFunction();

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

           TypeReference _range = variable.getRange();

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

+          it.setConstant(this.support.toIDMultiple("t", ((ComplexTypeReference) _range).getReferred().getName()));

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

           VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable();

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

@@ -215,7 +215,7 @@ public class Logic2VampireLanguageMapper_RelationMapper {
         VLSFunction _createVLSFunction = this.factory.createVLSFunction();

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

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

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

+          it.setConstant(this.support.toIDMultiple("t", ((ComplexTypeReference) _get).getReferred().getName()));

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

           VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable();

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

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java
index 86d8b648..8967839d 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java
@@ -51,42 +51,53 @@ public class Logic2VampireLanguageMapper_ScopeMapper {
         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());

+    if ((config.typeScopes.minNewElements != 0)) {

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

               };

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

             };

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

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

           };

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

         };

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

       };

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

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

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

+      _formulas.add(cstDec);

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

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

+        it.setName("typeUniqueness");

+        it.setFofRole("axiom");

+        it.setFofFormula(this.support.establishUniqueness(instances));

+      };

+      final VLSFofFormula uniqueness = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula_1, _function_2);

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

+      _formulas_1.add(uniqueness);

+    }

   }

   

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

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 b111732f..dfe624be 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
@@ -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.vampireLanguage.VLSAnd;

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

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

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

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

@@ -25,6 +26,7 @@ import java.util.List;
 import java.util.Map;

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

 import org.eclipse.xtend2.lib.StringConcatenation;

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

@@ -73,6 +75,36 @@ public class Logic2VampireLanguageMapper_Support {
     return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function);

   }

   

+  public VLSTerm establishUniqueness(final List<VLSConstant> terms) {

+    final List<VLSInequality> eqs = CollectionLiterals.<VLSInequality>newArrayList();

+    List<VLSConstant> _subList = terms.subList(1, ((Object[])Conversions.unwrapArray(terms, Object.class)).length);

+    for (final VLSConstant t1 : _subList) {

+      List<VLSConstant> _subList_1 = terms.subList(0, terms.indexOf(t1));

+      for (final VLSConstant t2 : _subList_1) {

+        {

+          VLSInequality _createVLSInequality = this.factory.createVLSInequality();

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

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

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

+              it_1.setName(t2.getName());

+            };

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

+            it.setLeft(_doubleArrow);

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

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

+              it_1.setName(t1.getName());

+            };

+            VLSConstant _doubleArrow_1 = ObjectExtensions.<VLSConstant>operator_doubleArrow(_createVLSConstant_1, _function_2);

+            it.setRight(_doubleArrow_1);

+          };

+          final VLSInequality eq = ObjectExtensions.<VLSInequality>operator_doubleArrow(_createVLSInequality, _function);

+          eqs.add(eq);

+        }

+      }

+    }

+    return this.unfoldAnd(eqs);

+  }

+  

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

     int _size = operands.size();

     boolean _equals = (_size == 1);

@@ -180,7 +212,7 @@ public class Logic2VampireLanguageMapper_Support {
           VLSFunction _createVLSFunction = this.factory.createVLSFunction();

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

             TypeReference _range = variable.getRange();

-            it.setConstant(this.toIDMultiple("type", ((ComplexTypeReference) _range).getReferred().getName()));

+            it.setConstant(this.toIDMultiple("t", ((ComplexTypeReference) _range).getReferred().getName()));

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

             VLSVariable _createVLSVariable = this.factory.createVLSVariable();

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

@@ -229,7 +261,7 @@ public class Logic2VampireLanguageMapper_Support {
           VLSFunction _createVLSFunction = this.factory.createVLSFunction();

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

             TypeReference _range = variable.getRange();

-            it.setConstant(this.toIDMultiple("type", ((ComplexTypeReference) _range).getReferred().getName()));

+            it.setConstant(this.toIDMultiple("t", ((ComplexTypeReference) _range).getReferred().getName()));

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

             VLSVariable _createVLSVariable = this.factory.createVLSVariable();

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

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 71e98871..1e845d94 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
@@ -115,47 +115,39 @@ public class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Log
       return Boolean.valueOf((!_isIsAbstract));

     };

     Iterable<Type> _filter_1 = IterableExtensions.<Type>filter(types, _function_1);

-    for (final Type type_2 : _filter_1) {

+    for (final Type t1 : _filter_1) {

       {

-        for (final Type type2 : types) {

-          if ((Objects.equal(type_2, type2) || this.dfsSupertypeCheck(type_2, type2))) {

+        for (final Type t2 : types) {

+          if ((Objects.equal(t1, t2) || this.dfsSupertypeCheck(t1, t2))) {

             VLSFunction _createVLSFunction = this.factory.createVLSFunction();

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

-              it.setConstant(CollectionsUtil.<Type, VLSFunction>lookup(type2, typeTrace.type2Predicate).getConstant());

+              it.setConstant(CollectionsUtil.<Type, VLSFunction>lookup(t2, typeTrace.type2Predicate).getConstant());

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

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

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

-                it_1.setName("A");

-              };

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

-              _terms.add(_doubleArrow);

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

+              _terms.add(_duplicate);

             };

             VLSFunction _doubleArrow = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_2);

-            typeTrace.type2PossibleNot.put(type2, _doubleArrow);

+            typeTrace.type2PossibleNot.put(t2, _doubleArrow);

           } else {

             VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation();

             final Procedure1<VLSUnaryNegation> _function_3 = (VLSUnaryNegation it) -> {

               VLSFunction _createVLSFunction_1 = this.factory.createVLSFunction();

               final Procedure1<VLSFunction> _function_4 = (VLSFunction it_1) -> {

-                it_1.setConstant(CollectionsUtil.<Type, VLSFunction>lookup(type2, typeTrace.type2Predicate).getConstant());

+                it_1.setConstant(CollectionsUtil.<Type, VLSFunction>lookup(t2, typeTrace.type2Predicate).getConstant());

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

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

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

-                  it_2.setName("A");

-                };

-                VLSVariable _doubleArrow_1 = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_1, _function_5);

-                _terms.add(_doubleArrow_1);

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

+                _terms.add(_duplicate);

               };

               VLSFunction _doubleArrow_1 = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction_1, _function_4);

               it.setOperand(_doubleArrow_1);

             };

             VLSUnaryNegation _doubleArrow_1 = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function_3);

-            typeTrace.type2PossibleNot.put(type2, _doubleArrow_1);

+            typeTrace.type2PossibleNot.put(t2, _doubleArrow_1);

           }

         }

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

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

-        typeTrace.type2And.put(type_2, this.support.unfoldAnd(_arrayList));

+        typeTrace.type2And.put(t1, this.support.unfoldAnd(_arrayList));

         typeTrace.type2PossibleNot.clear();

       }

     }

@@ -166,21 +158,17 @@ public class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Log
       VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();

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

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

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

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

-          it_2.setName("A");

-        };

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

-        _variables.add(_doubleArrow);

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

+        _variables.add(_duplicate);

         VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent();

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

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

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

         };

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

-        it_1.setOperand(_doubleArrow_1);

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

+        it_1.setOperand(_doubleArrow);

       };

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

       it.setFofFormula(_doubleArrow);

diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/.classpath b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/.classpath
index 1c96fe2f..3f0838b6 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/.classpath
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/.classpath
@@ -3,6 +3,7 @@
         <classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER/org.eclipse.jdt.internal.debug.ui.launcher.StandardVMType/JavaSE-1.8"/>

         <classpathentry kind="con" path="org.eclipse.pde.core.requiredPlugins"/>

         <classpathentry kind="src" path="src"/>

+        <classpathentry kind="src" path="src-gen"/>

         <classpathentry kind="src" path="xtend-gen"/>

         <classpathentry kind="output" path="bin"/>

 </classpath>

diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/.project b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/.project
index eb3347d0..87dc2baa 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/.project
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/.project
@@ -6,6 +6,11 @@
         </projects>

         <buildSpec>

                 <buildCommand>

+                        <name>org.eclipse.viatra.query.tooling.ui.projectbuilder</name>

+                        <arguments>

+                        </arguments>

+                </buildCommand>

+                <buildCommand>

                         <name>org.eclipse.xtext.ui.shared.xtextBuilder</name>

                         <arguments>

                         </arguments>

@@ -30,5 +35,6 @@
                 <nature>org.eclipse.pde.PluginNature</nature>

                 <nature>org.eclipse.jdt.core.javanature</nature>

                 <nature>org.eclipse.xtext.ui.shared.xtextNature</nature>

+                <nature>org.eclipse.viatra.query.projectnature</nature>

         </natures>

 </projectDescription>

diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/META-INF/MANIFEST.MF b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/META-INF/MANIFEST.MF
index fedee0e4..1995ee52 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/META-INF/MANIFEST.MF
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/META-INF/MANIFEST.MF
@@ -1,31 +1,36 @@
-Manifest-Version: 1.0

-Bundle-ManifestVersion: 2

-Bundle-Name: Test

-Bundle-SymbolicName: ca.mcgill.ecse.dslreasoner.vampire.test;singleton:=true

-Bundle-Version: 1.0.0.qualifier

-Automatic-Module-Name: ca.mcgill.ecse.dslreasoner.vampire.test

-Bundle-RequiredExecutionEnvironment: JavaSE-1.8

-Require-Bundle: com.google.guava,

- org.eclipse.xtext.xbase.lib,

- org.eclipse.xtend.lib,

- org.eclipse.xtend.lib.macro,

- ca.mcgill.ecse.dslreasoner.vampire.language;bundle-version="1.0.0",

- hu.bme.mit.inf.dslreasoner.logic.model;bundle-version="1.0.0",

- ca.mcgill.ecse.dslreasoner.vampire.reasoner;bundle-version="1.0.0",

- hu.bme.mit.inf.dslreasoner.ecore2logic;bundle-version="1.0.0",

- hu.bme.mit.inf.dslreasoner.viatra2logic;bundle-version="1.0.0",

- org.eclipse.emf.ecore.xmi;bundle-version="2.13.0",

- hu.bme.mit.inf.dlsreasoner.alloy.reasoner;bundle-version="1.0.0",

- hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage;bundle-version="1.0.0",

- hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner;bundle-version="1.0.0",

- hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatraquery;bundle-version="1.0.0",

- hu.bme.mit.inf.dslreasoner.logic2ecore;bundle-version="1.0.0",

- hu.bme.mit.inf.dslreasoner.visualisation;bundle-version="1.0.0",

- ModelGenExampleFAM_plugin;bundle-version="1.0.0",

- ModelGenExampleFAM_plugin.validation;bundle-version="0.0.1",

- hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph;bundle-version="1.0.0",

- hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.validation;bundle-version="0.0.1",

- org.eclipse.viatra.query.runtime;bundle-version="2.1.0",

- org.eclipse.collections;bundle-version="9.2.0",

- hu.bme.mit.inf.dslreasoner.application.FAMTest;bundle-version="1.0.0"

-

+Manifest-Version: 1.0
+Bundle-ManifestVersion: 2
+Bundle-Name: Test
+Bundle-SymbolicName: ca.mcgill.ecse.dslreasoner.vampire.test;singleton:=true
+Bundle-Version: 1.0.0.qualifier
+Export-Package: ca.mcgill.ecse.dslreasoner.vampire.queries
+Require-Bundle: org.eclipse.emf.ecore,
+  org.eclipse.viatra.query.runtime.rete,
+  org.eclipse.viatra.query.runtime.localsearch,
+  com.google.guava,
+  org.eclipse.xtext.xbase.lib,
+  org.eclipse.xtend.lib,
+  org.eclipse.xtend.lib.macro,
+  ca.mcgill.ecse.dslreasoner.vampire.language;bundle-version="1.0.0",
+  hu.bme.mit.inf.dslreasoner.logic.model;bundle-version="1.0.0",
+  ca.mcgill.ecse.dslreasoner.vampire.reasoner;bundle-version="1.0.0",
+  hu.bme.mit.inf.dslreasoner.ecore2logic;bundle-version="1.0.0",
+  hu.bme.mit.inf.dslreasoner.viatra2logic;bundle-version="1.0.0",
+  org.eclipse.emf.ecore.xmi;bundle-version="2.13.0",
+  hu.bme.mit.inf.dlsreasoner.alloy.reasoner;bundle-version="1.0.0",
+  hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage;bundle-version="1.0.0",
+  hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner;bundle-version="1.0.0",
+  hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatraquery;bundle-version="1.0.0",
+  hu.bme.mit.inf.dslreasoner.logic2ecore;bundle-version="1.0.0",
+  hu.bme.mit.inf.dslreasoner.visualisation;bundle-version="1.0.0",
+  ModelGenExampleFAM_plugin;bundle-version="1.0.0",
+  ModelGenExampleFAM_plugin.validation;bundle-version="0.0.1",
+  hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph;bundle-version="1.0.0",
+  hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.validation;bundle-version="0.0.1",
+  org.eclipse.viatra.query.runtime;bundle-version="2.1.0",
+  org.eclipse.collections;bundle-version="9.2.0",
+  hu.bme.mit.inf.dslreasoner.application.FAMTest;bundle-version="1.0.0",
+  ca.mcgill.ecse.dslreasoner.standalone.test;bundle-version="1.0.0"
+Bundle-RequiredExecutionEnvironment: JavaSE-1.8
+Import-Package: org.apache.log4j
+Automatic-Module-Name: ca.mcgill.ecse.dslreasoner.vampire.test
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/build.properties b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/build.properties
index 41eb6ade..efae4b07 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/build.properties
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/build.properties
@@ -1,4 +1,6 @@
-source.. = src/

-output.. = bin/

 bin.includes = META-INF/,\

                .

+source.. = src/,\

+           src-gen/,\

+           src-gen/

+output.. = bin/

diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/initialModels/FunctionalArchitectureModel.xmi b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/initialModels/FunctionalArchitectureModel.xmi
index 61256334..8500678c 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/initialModels/FunctionalArchitectureModel.xmi
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/initialModels/FunctionalArchitectureModel.xmi
@@ -7,4 +7,6 @@
     xsi:schemaLocation="http://www.inf.mit.bme.hu/viatrasolver/example/fam ../../ModelGenExampleFAM_plugin/model/FamMetamodel.ecore">

   <rootElements

       xsi:type="functionalarchitecture:Function"/>

+  <rootElements

+      xsi:type="functionalarchitecture:Function"/>

 </functionalarchitecture:FunctionalArchitectureModel>

diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/initialModels/FunctionalArchitectureModel2.xmi b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/initialModels/FunctionalArchitectureModel2.xmi
new file mode 100644
index 00000000..59935a2c
--- /dev/null
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/initialModels/FunctionalArchitectureModel2.xmi
@@ -0,0 +1,4 @@
+<?xml version="1.0" encoding="UTF-8"?>

+<functionalarchitecture:FunctionalArchitectureModel xmi:version="2.0" xmlns:xmi="http://www.omg.org/XMI"

+    xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:functionalarchitecture="http://www.inf.mit.bme.hu/viatrasolver/example/fam"

+    xsi:schemaLocation="http://www.inf.mit.bme.hu/viatrasolver/example/fam FamMetamodel.ecore"/>

diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/initialModels/yakindu/yakindu.ecore b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/initialModels/yakindu/yakindu.ecore
new file mode 100644
index 00000000..0c944db8
--- /dev/null
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/initialModels/yakindu/yakindu.ecore
@@ -0,0 +1,26 @@
+<?xml version="1.0" encoding="UTF-8"?>

+<ecore:EPackage xmi:version="2.0" xmlns:xmi="http://www.omg.org/XMI" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:ecore="http://www.eclipse.org/emf/2002/Ecore" name="yakindu" nsURI="YakinduMetamodel" nsPrefix="yakindu">

+  <eClassifiers xsi:type="ecore:EClass" name="Pseudostate" abstract="true" eSuperTypes="//Vertex"/>

+  <eClassifiers xsi:type="ecore:EClass" name="Vertex" abstract="true">

+    <eStructuralFeatures xsi:type="ecore:EReference" name="incomingTransitions" ordered="false" upperBound="-1" eType="//Transition" eOpposite="//Transition/target"/>

+    <eStructuralFeatures xsi:type="ecore:EReference" name="outgoingTransitions" ordered="false" upperBound="-1" eType="//Transition" containment="true" eOpposite="//Transition/source"/>

+  </eClassifiers>

+  <eClassifiers xsi:type="ecore:EClass" name="Region">

+    <eStructuralFeatures xsi:type="ecore:EReference" name="vertices" ordered="false" upperBound="-1" eType="//Vertex" containment="true"/>

+  </eClassifiers>

+  <eClassifiers xsi:type="ecore:EClass" name="Transition">

+    <eStructuralFeatures xsi:type="ecore:EReference" name="target" ordered="false" lowerBound="1" eType="//Vertex" eOpposite="//Vertex/incomingTransitions"/>

+    <eStructuralFeatures xsi:type="ecore:EReference" name="source" ordered="false" eType="//Vertex" eOpposite="//Vertex/outgoingTransitions"/>

+  </eClassifiers>

+  <eClassifiers xsi:type="ecore:EClass" name="Statechart" eSuperTypes="//CompositeElement"/>

+  <eClassifiers xsi:type="ecore:EClass" name="Entry" eSuperTypes="//Pseudostate"/>

+  <eClassifiers xsi:type="ecore:EClass" name="Synchronization" eSuperTypes="//Pseudostate"/>

+  <eClassifiers xsi:type="ecore:EClass" name="State" eSuperTypes="//RegularState //CompositeElement"/>

+  <eClassifiers xsi:type="ecore:EClass" name="RegularState" abstract="true" eSuperTypes="//Vertex"/>

+  <eClassifiers xsi:type="ecore:EClass" name="CompositeElement" abstract="true">

+    <eStructuralFeatures xsi:type="ecore:EReference" name="regions" upperBound="-1" eType="//Region" containment="true"/>

+  </eClassifiers>

+  <eClassifiers xsi:type="ecore:EClass" name="Choice" eSuperTypes="//Pseudostate"/>

+  <eClassifiers xsi:type="ecore:EClass" name="Exit" eSuperTypes="//Pseudostate"/>

+  <eClassifiers xsi:type="ecore:EClass" name="FinalState" eSuperTypes="//RegularState"/>

+</ecore:EPackage>

diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/Fam.logicproblem b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/Fam.logicproblem
index 5792ceed..a0b5d6ea 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/Fam.logicproblem
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/Fam.logicproblem
@@ -1,7 +1,7 @@
 <?xml version="1.0" encoding="ASCII"?>

 <language:LogicProblem xmi:version="2.0" xmlns:xmi="http://www.omg.org/XMI" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:ecore2logicannotations="http://www.bme.hu/mit/inf/dslreasoner/logic/model/language/ecore2logicannotation" xmlns:language="http://www.bme.hu/mit/inf/dslreasoner/logic/model/problem" xmlns:language_1="http://www.bme.hu/mit/inf/dslreasoner/logic/model/language" xmlns:viatra2logicannotations="http://www.bme.hu/mit/inf/dslreasoner/logic/model/language/viatra2logicannotation">

   <types xsi:type="language_1:TypeDeclaration" name="FunctionalElement class" subtypes="//@types.2" isAbstract="true"/>

-  <types xsi:type="language_1:TypeDeclaration" name="FunctionalArchitectureModel class" subtypes="//@types.10 //@types.11" isAbstract="true"/>

+  <types xsi:type="language_1:TypeDeclaration" name="FunctionalArchitectureModel class"/>

   <types xsi:type="language_1:TypeDeclaration" name="Function class" supertypes="//@types.0"/>

   <types xsi:type="language_1:TypeDeclaration" name="FAMTerminator class"/>

   <types xsi:type="language_1:TypeDeclaration" name="InformationLink class"/>

@@ -10,8 +10,6 @@
   <types xsi:type="language_1:TypeDeclaration" name="FunctionalOutput class" supertypes="//@types.8"/>

   <types xsi:type="language_1:TypeDeclaration" name="FunctionalData class" subtypes="//@types.6 //@types.7" isAbstract="true"/>

   <types xsi:type="language_1:TypeDefinition" name="FunctionType enum" elements="//@elements.0 //@elements.1 //@elements.2"/>

-  <types xsi:type="language_1:TypeDefinition" name="FunctionalArchitectureModel class DefinedPart" supertypes="//@types.1" elements="//@elements.3"/>

-  <types xsi:type="language_1:TypeDeclaration" name="FunctionalArchitectureModel class UndefinedPart" supertypes="//@types.1"/>

   <assertions name="upperMultiplicity interface FunctionalElement" annotations="//@annotations.0">

     <value xsi:type="language_1:Forall">

       <quantifiedVariables name="src">

@@ -496,7 +494,7 @@
       </expression>

     </value>

   </assertions>

-  <assertions name="errorpattern hu bme mit inf dslreasoner domains transima fam terminatorAndInformation" annotations="//@annotations.27">

+  <assertions name="errorpattern ca mcgill ecse dslreasoner vampire queries terminatorAndInformation" annotations="//@annotations.20">

     <value xsi:type="language_1:Forall">

       <quantifiedVariables name="p0">

         <range xsi:type="language_1:ComplexTypeReference" referred="//@types.3"/>

@@ -505,7 +503,7 @@
         <range xsi:type="language_1:ComplexTypeReference" referred="//@types.4"/>

       </quantifiedVariables>

       <expression xsi:type="language_1:Not">

-        <operand xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.22">

+        <operand xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15">

           <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@assertions.19/@value/@quantifiedVariables.0"/>

           <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@assertions.19/@value/@quantifiedVariables.1"/>

         </operand>

@@ -572,235 +570,7 @@
     <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/>

     <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.9"/>

   </relations>

-  <relations xsi:type="language_1:RelationDefinition" name="pattern hu bme mit inf dslreasoner domains transima fam hasRoot" annotations="//@annotations.19">

-    <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/>

-    <variables name="parameter F">

-      <range xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/>

-    </variables>

-    <value xsi:type="language_1:Or">

-      <operands xsi:type="language_1:Exists">

-        <quantifiedVariables name="variable Model">

-          <range xsi:type="language_1:ComplexTypeReference" referred="//@types.1"/>

-        </quantifiedVariables>

-        <expression xsi:type="language_1:And">

-          <operands xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.19">

-            <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15/@value/@operands.0/@quantifiedVariables.0"/>

-            <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15/@variables.0"/>

-          </operands>

-        </expression>

-      </operands>

-    </value>

-  </relations>

-  <relations xsi:type="language_1:RelationDefinition" name="pattern hu bme mit inf dslreasoner domains transima fam hasInt" annotations="//@annotations.20">

-    <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/>

-    <variables name="parameter F">

-      <range xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/>

-    </variables>

-    <value xsi:type="language_1:Or">

-      <operands xsi:type="language_1:Forall">

-        <quantifiedVariables name="variable Child">

-          <range xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/>

-        </quantifiedVariables>

-        <quantifiedVariables name="variable Model">

-          <range xsi:type="language_1:ComplexTypeReference" referred="//@types.1"/>

-        </quantifiedVariables>

-        <expression xsi:type="language_1:And">

-          <operands xsi:type="language_1:InstanceOf">

-            <value xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.16/@variables.0"/>

-            <range xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/>

-          </operands>

-          <operands xsi:type="language_1:Not">

-            <operand xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.21">

-              <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.16/@value/@operands.0/@quantifiedVariables.0"/>

-              <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.16/@variables.0"/>

-            </operand>

-          </operands>

-          <operands xsi:type="language_1:Not">

-            <operand xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.19">

-              <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.16/@value/@operands.0/@quantifiedVariables.1"/>

-              <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.16/@variables.0"/>

-            </operand>

-          </operands>

-        </expression>

-      </operands>

-    </value>

-  </relations>

-  <relations xsi:type="language_1:RelationDefinition" name="pattern hu bme mit inf dslreasoner domains transima fam hasLeaf" annotations="//@annotations.21">

-    <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/>

-    <variables name="parameter F">

-      <range xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/>

-    </variables>

-    <value xsi:type="language_1:Or">

-      <operands xsi:type="language_1:Exists">

-        <quantifiedVariables name="variable Par">

-          <range xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/>

-        </quantifiedVariables>

-        <quantifiedVariables name="variable Child">

-          <range xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/>

-        </quantifiedVariables>

-        <expression xsi:type="language_1:And">

-          <operands xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.21">

-            <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.17/@variables.0"/>

-            <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.17/@value/@operands.0/@quantifiedVariables.0"/>

-          </operands>

-          <operands xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.21">

-            <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.17/@value/@operands.0/@quantifiedVariables.1"/>

-            <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.17/@variables.0"/>

-          </operands>

-        </expression>

-      </operands>

-    </value>

-  </relations>

-  <relations xsi:type="language_1:RelationDefinition" name="pattern hu bme mit inf dslreasoner domains transima fam model" annotations="//@annotations.22">

-    <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.0"/>

-    <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.1"/>

-    <variables name="parameter This">

-      <range xsi:type="language_1:ComplexTypeReference" referred="//@types.0"/>

-    </variables>

-    <variables name="parameter Target">

-      <range xsi:type="language_1:ComplexTypeReference" referred="//@types.1"/>

-    </variables>

-    <value xsi:type="language_1:Or">

-      <operands xsi:type="language_1:And">

-        <operands xsi:type="language_1:InstanceOf">

-          <value xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.18/@variables.0"/>

-          <range xsi:type="language_1:ComplexTypeReference" referred="//@types.0"/>

-        </operands>

-        <operands xsi:type="language_1:InstanceOf">

-          <value xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.18/@variables.1"/>

-          <range xsi:type="language_1:ComplexTypeReference" referred="//@types.1"/>

-        </operands>

-      </operands>

-    </value>

-  </relations>

-  <relations xsi:type="language_1:RelationDefinition" name="pattern hu bme mit inf dslreasoner domains transima fam rootElements" annotations="//@annotations.23">

-    <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.1"/>

-    <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/>

-    <variables name="parameter Model">

-      <range xsi:type="language_1:ComplexTypeReference" referred="//@types.1"/>

-    </variables>

-    <variables name="parameter Root">

-      <range xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/>

-    </variables>

-    <value xsi:type="language_1:Or">

-      <operands xsi:type="language_1:And">

-        <operands xsi:type="language_1:InstanceOf">

-          <value xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.19/@variables.1"/>

-          <range xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/>

-        </operands>

-        <operands xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.3">

-          <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.19/@variables.0"/>

-          <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.19/@variables.1"/>

-        </operands>

-      </operands>

-    </value>

-  </relations>

-  <relations xsi:type="language_1:RelationDefinition" name="pattern hu bme mit inf dslreasoner domains transima fam type" annotations="//@annotations.24">

-    <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/>

-    <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.9"/>

-    <variables name="parameter This">

-      <range xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/>

-    </variables>

-    <variables name="parameter Target">

-      <range xsi:type="language_1:ComplexTypeReference" referred="//@types.9"/>

-    </variables>

-    <value xsi:type="language_1:Or">

-      <operands xsi:type="language_1:Exists">

-        <quantifiedVariables name="variable Model">

-          <range xsi:type="language_1:ComplexTypeReference" referred="//@types.1"/>

-        </quantifiedVariables>

-        <expression xsi:type="language_1:And">

-          <operands xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.19">

-            <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.20/@value/@operands.0/@quantifiedVariables.0"/>

-            <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.20/@variables.0"/>

-          </operands>

-          <operands xsi:type="language_1:Equals">

-            <leftOperand xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.20/@variables.1"/>

-            <rightOperand xsi:type="language_1:SymbolicValue" symbolicReference="//@elements.0"/>

-          </operands>

-        </expression>

-      </operands>

-      <operands xsi:type="language_1:Forall">

-        <quantifiedVariables name="variable Child">

-          <range xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/>

-        </quantifiedVariables>

-        <quantifiedVariables name="variable Model">

-          <range xsi:type="language_1:ComplexTypeReference" referred="//@types.1"/>

-        </quantifiedVariables>

-        <expression xsi:type="language_1:And">

-          <operands xsi:type="language_1:InstanceOf">

-            <value xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.20/@variables.0"/>

-            <range xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/>

-          </operands>

-          <operands xsi:type="language_1:Not">

-            <operand xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.21">

-              <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.20/@value/@operands.1/@quantifiedVariables.0"/>

-              <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.20/@variables.0"/>

-            </operand>

-          </operands>

-          <operands xsi:type="language_1:Not">

-            <operand xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.19">

-              <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.20/@value/@operands.1/@quantifiedVariables.1"/>

-              <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.20/@variables.0"/>

-            </operand>

-          </operands>

-          <operands xsi:type="language_1:Equals">

-            <leftOperand xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.20/@variables.1"/>

-            <rightOperand xsi:type="language_1:SymbolicValue" symbolicReference="//@elements.2"/>

-          </operands>

-        </expression>

-      </operands>

-      <operands xsi:type="language_1:Exists">

-        <quantifiedVariables name="variable Par">

-          <range xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/>

-        </quantifiedVariables>

-        <quantifiedVariables name="variable Child">

-          <range xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/>

-        </quantifiedVariables>

-        <expression xsi:type="language_1:And">

-          <operands xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.21">

-            <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.20/@variables.0"/>

-            <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.20/@value/@operands.2/@quantifiedVariables.0"/>

-          </operands>

-          <operands xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.21">

-            <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.20/@value/@operands.2/@quantifiedVariables.1"/>

-            <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.20/@variables.0"/>

-          </operands>

-          <operands xsi:type="language_1:Equals">

-            <leftOperand xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.20/@variables.1"/>

-            <rightOperand xsi:type="language_1:SymbolicValue" symbolicReference="//@elements.1"/>

-          </operands>

-        </expression>

-      </operands>

-    </value>

-  </relations>

-  <relations xsi:type="language_1:RelationDefinition" name="pattern hu bme mit inf dslreasoner domains transima fam parent" annotations="//@annotations.25">

-    <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/>

-    <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/>

-    <variables name="parameter Func">

-      <range xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/>

-    </variables>

-    <variables name="parameter Par">

-      <range xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/>

-    </variables>

-    <value xsi:type="language_1:Or">

-      <operands xsi:type="language_1:And">

-        <operands xsi:type="language_1:InstanceOf">

-          <value xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.21/@variables.0"/>

-          <range xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/>

-        </operands>

-        <operands xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.2">

-          <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.21/@variables.0"/>

-          <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.21/@variables.1"/>

-        </operands>

-        <operands xsi:type="language_1:InstanceOf">

-          <value xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.21/@variables.1"/>

-          <range xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/>

-        </operands>

-      </operands>

-    </value>

-  </relations>

-  <relations xsi:type="language_1:RelationDefinition" name="pattern hu bme mit inf dslreasoner domains transima fam terminatorAndInformation" annotations="//@annotations.26">

+  <relations xsi:type="language_1:RelationDefinition" name="pattern ca mcgill ecse dslreasoner vampire queries terminatorAndInformation" annotations="//@annotations.19">

     <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.3"/>

     <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.4"/>

     <variables name="parameter T">

@@ -816,12 +586,12 @@
         </quantifiedVariables>

         <expression xsi:type="language_1:And">

           <operands xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.11">

-            <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.22/@value/@operands.0/@quantifiedVariables.0"/>

-            <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.22/@variables.1"/>

+            <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15/@value/@operands.0/@quantifiedVariables.0"/>

+            <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15/@variables.1"/>

           </operands>

           <operands xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.12">

-            <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.22/@value/@operands.0/@quantifiedVariables.0"/>

-            <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.22/@variables.0"/>

+            <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15/@value/@operands.0/@quantifiedVariables.0"/>

+            <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15/@variables.0"/>

           </operands>

         </expression>

       </operands>

@@ -831,16 +601,12 @@
         </quantifiedVariables>

         <expression xsi:type="language_1:And">

           <operands xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.7">

-            <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.22/@variables.1"/>

-            <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.22/@value/@operands.1/@quantifiedVariables.0"/>

-          </operands>

-          <operands xsi:type="language_1:InstanceOf">

-            <value xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.22/@value/@operands.1/@quantifiedVariables.0"/>

-            <range xsi:type="language_1:ComplexTypeReference" referred="//@types.6"/>

+            <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15/@variables.1"/>

+            <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15/@value/@operands.1/@quantifiedVariables.0"/>

           </operands>

           <operands xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.12">

-            <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.22/@value/@operands.1/@quantifiedVariables.0"/>

-            <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.22/@variables.0"/>

+            <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15/@value/@operands.1/@quantifiedVariables.0"/>

+            <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15/@variables.0"/>

           </operands>

         </expression>

       </operands>

@@ -849,8 +615,7 @@
   <elements name="Root literal FunctionType" definedInType="//@types.9"/>

   <elements name="Intermediate literal FunctionType" definedInType="//@types.9"/>

   <elements name="Leaf literal FunctionType" definedInType="//@types.9"/>

-  <elements name="o 1" definedInType="//@types.10"/>

-  <containmentHierarchies typesOrderedInHierarchy="//@types.5 //@types.6 //@types.1 //@types.3 //@types.0 //@types.4 //@types.7 //@types.2 //@types.8 //@types.10 //@types.11" containmentRelations="//@relations.0 //@relations.3 //@relations.4 //@relations.8 //@relations.11 //@relations.12"/>

+  <containmentHierarchies typesOrderedInHierarchy="//@types.3 //@types.8 //@types.0 //@types.4 //@types.2 //@types.1 //@types.6 //@types.7 //@types.5" containmentRelations="//@relations.0 //@relations.3 //@relations.4 //@relations.8 //@relations.11 //@relations.12"/>

   <annotations xsi:type="ecore2logicannotations:UpperMultiplicityAssertion" target="//@assertions.0" relation="//@relations.0" upper="1"/>

   <annotations xsi:type="ecore2logicannotations:LowerMultiplicityAssertion" target="//@assertions.1" relation="//@relations.1" lower="1"/>

   <annotations xsi:type="ecore2logicannotations:UpperMultiplicityAssertion" target="//@assertions.2" relation="//@relations.1" upper="1"/>

@@ -870,13 +635,6 @@
   <annotations xsi:type="ecore2logicannotations:InverseRelationAssertion" target="//@assertions.16" inverseA="//@relations.8" inverseB="//@relations.13"/>

   <annotations xsi:type="ecore2logicannotations:LowerMultiplicityAssertion" target="//@assertions.17" relation="//@relations.14" lower="1"/>

   <annotations xsi:type="ecore2logicannotations:UpperMultiplicityAssertion" target="//@assertions.18" relation="//@relations.14" upper="1"/>

-  <annotations xsi:type="viatra2logicannotations:TransfomedViatraQuery" target="//@relations.15" patternFullyQualifiedName="hu.bme.mit.inf.dslreasoner.domains.transima.fam.hasRoot"/>

-  <annotations xsi:type="viatra2logicannotations:TransfomedViatraQuery" target="//@relations.16" patternFullyQualifiedName="hu.bme.mit.inf.dslreasoner.domains.transima.fam.hasInt"/>

-  <annotations xsi:type="viatra2logicannotations:TransfomedViatraQuery" target="//@relations.17" patternFullyQualifiedName="hu.bme.mit.inf.dslreasoner.domains.transima.fam.hasLeaf"/>

-  <annotations xsi:type="viatra2logicannotations:TransfomedViatraQuery" target="//@relations.18" patternFullyQualifiedName="hu.bme.mit.inf.dslreasoner.domains.transima.fam.model"/>

-  <annotations xsi:type="viatra2logicannotations:TransfomedViatraQuery" target="//@relations.19" patternFullyQualifiedName="hu.bme.mit.inf.dslreasoner.domains.transima.fam.rootElements"/>

-  <annotations xsi:type="viatra2logicannotations:TransfomedViatraQuery" target="//@relations.20" patternFullyQualifiedName="hu.bme.mit.inf.dslreasoner.domains.transima.fam.type"/>

-  <annotations xsi:type="viatra2logicannotations:TransfomedViatraQuery" target="//@relations.21" patternFullyQualifiedName="hu.bme.mit.inf.dslreasoner.domains.transima.fam.parent"/>

-  <annotations xsi:type="viatra2logicannotations:TransfomedViatraQuery" target="//@relations.22" patternFullyQualifiedName="hu.bme.mit.inf.dslreasoner.domains.transima.fam.terminatorAndInformation"/>

-  <annotations xsi:type="viatra2logicannotations:TransformedViatraWellformednessConstraint" target="//@assertions.19" query="//@annotations.26"/>

+  <annotations xsi:type="viatra2logicannotations:TransfomedViatraQuery" target="//@relations.15" patternFullyQualifiedName="ca.mcgill.ecse.dslreasoner.vampire.queries.terminatorAndInformation"/>

+  <annotations xsi:type="viatra2logicannotations:TransformedViatraWellformednessConstraint" target="//@assertions.19" query="//@annotations.19"/>

 </language:LogicProblem>

diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/vampireProblem.tptp b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/vampireProblem.tptp
index 242c404c..1f220d6f 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/vampireProblem.tptp
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/vampireProblem.tptp
@@ -1,55 +1,42 @@
 % This is an initial Test Comment

-fof ( typeDef_FunctionType_enum , axiom , ! [ A ] : ( type_FunctionType_enum ( A ) <=> ( A = "aRoot literal FunctionType" | ( A = "aIntermediate literal FunctionType" | A = "aLeaf literal FunctionType" ) ) ) ) .

-fof ( typeDef_FunctionalArchitectureModel_class_DefinedPart , axiom , ! [ A ] : ( type_FunctionalArchitectureModel_class_DefinedPart ( A ) <=> A = "ao 1" ) ) .

-fof ( hierarchyHandler , axiom , ! [ A ] : ( object ( A ) <=> ( ( type_FunctionType_enum ( A ) & ( ~ type_FunctionalData_class ( A ) & ( ~ type_Function_class ( A ) & ( ~ type_InformationLink_class ( A ) & ( ~ type_FunctionalOutput_class ( A ) & ( ~ type_FunctionalArchitectureModel_class ( A ) & ( ~ type_FunctionalElement_class ( A ) & ( ~ type_FunctionalArchitectureModel_class_DefinedPart ( A ) & ( ~ type_FAMTerminator_class ( A ) & ( ~ type_FunctionalArchitectureModel_class_UndefinedPart ( A ) & ( ~ type_FunctionalInput_class ( A ) & ~ type_FunctionalInterface_class ( A ) ) ) ) ) ) ) ) ) ) ) ) | ( ( ~ type_FunctionType_enum ( A ) & ( ~ type_FunctionalData_class ( A ) & ( type_Function_class ( A ) & ( ~ type_InformationLink_class ( A ) & ( ~ type_FunctionalOutput_class ( A ) & ( ~ type_FunctionalArchitectureModel_class ( A ) & ( type_FunctionalElement_class ( A ) & ( ~ type_FunctionalArchitectureModel_class_DefinedPart ( A ) & ( ~ type_FAMTerminator_class ( A ) & ( ~ type_FunctionalArchitectureModel_class_UndefinedPart ( A ) & ( ~ type_FunctionalInput_class ( A ) & ~ type_FunctionalInterface_class ( A ) ) ) ) ) ) ) ) ) ) ) ) | ( ( ~ type_FunctionType_enum ( A ) & ( ~ type_FunctionalData_class ( A ) & ( ~ type_Function_class ( A ) & ( type_InformationLink_class ( A ) & ( ~ type_FunctionalOutput_class ( A ) & ( ~ type_FunctionalArchitectureModel_class ( A ) & ( ~ type_FunctionalElement_class ( A ) & ( ~ type_FunctionalArchitectureModel_class_DefinedPart ( A ) & ( ~ type_FAMTerminator_class ( A ) & ( ~ type_FunctionalArchitectureModel_class_UndefinedPart ( A ) & ( ~ type_FunctionalInput_class ( A ) & ~ type_FunctionalInterface_class ( A ) ) ) ) ) ) ) ) ) ) ) ) | ( ( ~ type_FunctionType_enum ( A ) & ( type_FunctionalData_class ( A ) & ( ~ type_Function_class ( A ) & ( ~ type_InformationLink_class ( A ) & ( type_FunctionalOutput_class ( A ) & ( ~ type_FunctionalArchitectureModel_class ( A ) & ( ~ type_FunctionalElement_class ( A ) & ( ~ type_FunctionalArchitectureModel_class_DefinedPart ( A ) & ( ~ type_FAMTerminator_class ( A ) & ( ~ type_FunctionalArchitectureModel_class_UndefinedPart ( A ) & ( ~ type_FunctionalInput_class ( A ) & ~ type_FunctionalInterface_class ( A ) ) ) ) ) ) ) ) ) ) ) ) | ( ( ~ type_FunctionType_enum ( A ) & ( ~ type_FunctionalData_class ( A ) & ( ~ type_Function_class ( A ) & ( ~ type_InformationLink_class ( A ) & ( ~ type_FunctionalOutput_class ( A ) & ( type_FunctionalArchitectureModel_class ( A ) & ( ~ type_FunctionalElement_class ( A ) & ( type_FunctionalArchitectureModel_class_DefinedPart ( A ) & ( ~ type_FAMTerminator_class ( A ) & ( ~ type_FunctionalArchitectureModel_class_UndefinedPart ( A ) & ( ~ type_FunctionalInput_class ( A ) & ~ type_FunctionalInterface_class ( A ) ) ) ) ) ) ) ) ) ) ) ) | ( ( ~ type_FunctionType_enum ( A ) & ( ~ type_FunctionalData_class ( A ) & ( ~ type_Function_class ( A ) & ( ~ type_InformationLink_class ( A ) & ( ~ type_FunctionalOutput_class ( A ) & ( ~ type_FunctionalArchitectureModel_class ( A ) & ( ~ type_FunctionalElement_class ( A ) & ( ~ type_FunctionalArchitectureModel_class_DefinedPart ( A ) & ( type_FAMTerminator_class ( A ) & ( ~ type_FunctionalArchitectureModel_class_UndefinedPart ( A ) & ( ~ type_FunctionalInput_class ( A ) & ~ type_FunctionalInterface_class ( A ) ) ) ) ) ) ) ) ) ) ) ) | ( ( ~ type_FunctionType_enum ( A ) & ( ~ type_FunctionalData_class ( A ) & ( ~ type_Function_class ( A ) & ( ~ type_InformationLink_class ( A ) & ( ~ type_FunctionalOutput_class ( A ) & ( type_FunctionalArchitectureModel_class ( A ) & ( ~ type_FunctionalElement_class ( A ) & ( ~ type_FunctionalArchitectureModel_class_DefinedPart ( A ) & ( ~ type_FAMTerminator_class ( A ) & ( type_FunctionalArchitectureModel_class_UndefinedPart ( A ) & ( ~ type_FunctionalInput_class ( A ) & ~ type_FunctionalInterface_class ( A ) ) ) ) ) ) ) ) ) ) ) ) | ( ( ~ type_FunctionType_enum ( A ) & ( type_FunctionalData_class ( A ) & ( ~ type_Function_class ( A ) & ( ~ type_InformationLink_class ( A ) & ( ~ type_FunctionalOutput_class ( A ) & ( ~ type_FunctionalArchitectureModel_class ( A ) & ( ~ type_FunctionalElement_class ( A ) & ( ~ type_FunctionalArchitectureModel_class_DefinedPart ( A ) & ( ~ type_FAMTerminator_class ( A ) & ( ~ type_FunctionalArchitectureModel_class_UndefinedPart ( A ) & ( type_FunctionalInput_class ( A ) & ~ type_FunctionalInterface_class ( A ) ) ) ) ) ) ) ) ) ) ) ) | ( ~ type_FunctionType_enum ( A ) & ( ~ type_FunctionalData_class ( A ) & ( ~ type_Function_class ( A ) & ( ~ type_InformationLink_class ( A ) & ( ~ type_FunctionalOutput_class ( A ) & ( ~ type_FunctionalArchitectureModel_class ( A ) & ( ~ type_FunctionalElement_class ( A ) & ( ~ type_FunctionalArchitectureModel_class_DefinedPart ( A ) & ( ~ type_FAMTerminator_class ( A ) & ( ~ type_FunctionalArchitectureModel_class_UndefinedPart ( A ) & ( ~ type_FunctionalInput_class ( A ) & type_FunctionalInterface_class ( A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) .

-fof ( compliance_interface_reference_FunctionalElement , axiom , ! [ Var_0 , Var_1 ] : ( rel_interface_reference_FunctionalElement ( Var_0 , Var_1 ) => ( type_FunctionalElement_class ( Var_0 ) & type_FunctionalInterface_class ( Var_1 ) ) ) ) .

-fof ( compliance_model_reference_FunctionalElement , axiom , ! [ Var_0 , Var_1 ] : ( rel_model_reference_FunctionalElement ( Var_0 , Var_1 ) => ( type_FunctionalElement_class ( Var_0 ) & type_FunctionalArchitectureModel_class ( Var_1 ) ) ) ) .

-fof ( compliance_parent_reference_FunctionalElement , axiom , ! [ Var_0 , Var_1 ] : ( rel_parent_reference_FunctionalElement ( Var_0 , Var_1 ) => ( type_FunctionalElement_class ( Var_0 ) & type_Function_class ( Var_1 ) ) ) ) .

-fof ( compliance_rootElements_reference_FunctionalArchitectureModel , axiom , ! [ Var_0 , Var_1 ] : ( rel_rootElements_reference_FunctionalArchitectureModel ( Var_0 , Var_1 ) => ( type_FunctionalArchitectureModel_class ( Var_0 ) & type_FunctionalElement_class ( Var_1 ) ) ) ) .

-fof ( compliance_subElements_reference_Function , axiom , ! [ Var_0 , Var_1 ] : ( rel_subElements_reference_Function ( Var_0 , Var_1 ) => ( type_Function_class ( Var_0 ) & type_FunctionalElement_class ( Var_1 ) ) ) ) .

-fof ( compliance_data_reference_FAMTerminator , axiom , ! [ Var_0 , Var_1 ] : ( rel_data_reference_FAMTerminator ( Var_0 , Var_1 ) => ( type_FAMTerminator_class ( Var_0 ) & type_FunctionalData_class ( Var_1 ) ) ) ) .

-fof ( compliance_from_reference_InformationLink , axiom , ! [ Var_0 , Var_1 ] : ( rel_from_reference_InformationLink ( Var_0 , Var_1 ) => ( type_InformationLink_class ( Var_0 ) & type_FunctionalOutput_class ( Var_1 ) ) ) ) .

-fof ( compliance_to_reference_InformationLink , axiom , ! [ Var_0 , Var_1 ] : ( rel_to_reference_InformationLink ( Var_0 , Var_1 ) => ( type_InformationLink_class ( Var_0 ) & type_FunctionalInput_class ( Var_1 ) ) ) ) .

-fof ( compliance_data_reference_FunctionalInterface , axiom , ! [ Var_0 , Var_1 ] : ( rel_data_reference_FunctionalInterface ( Var_0 , Var_1 ) => ( type_FunctionalInterface_class ( Var_0 ) & type_FunctionalData_class ( Var_1 ) ) ) ) .

-fof ( compliance_element_reference_FunctionalInterface , axiom , ! [ Var_0 , Var_1 ] : ( rel_element_reference_FunctionalInterface ( Var_0 , Var_1 ) => ( type_FunctionalInterface_class ( Var_0 ) & type_FunctionalElement_class ( Var_1 ) ) ) ) .

-fof ( compliance_IncomingLinks_reference_FunctionalInput , axiom , ! [ Var_0 , Var_1 ] : ( rel_IncomingLinks_reference_FunctionalInput ( Var_0 , Var_1 ) => ( type_FunctionalInput_class ( Var_0 ) & type_InformationLink_class ( Var_1 ) ) ) ) .

-fof ( compliance_outgoingLinks_reference_FunctionalOutput , axiom , ! [ Var_0 , Var_1 ] : ( rel_outgoingLinks_reference_FunctionalOutput ( Var_0 , Var_1 ) => ( type_FunctionalOutput_class ( Var_0 ) & type_InformationLink_class ( Var_1 ) ) ) ) .

-fof ( compliance_terminator_reference_FunctionalData , axiom , ! [ Var_0 , Var_1 ] : ( rel_terminator_reference_FunctionalData ( Var_0 , Var_1 ) => ( type_FunctionalData_class ( Var_0 ) & type_FAMTerminator_class ( Var_1 ) ) ) ) .

-fof ( compliance_interface_reference_FunctionalData , axiom , ! [ Var_0 , Var_1 ] : ( rel_interface_reference_FunctionalData ( Var_0 , Var_1 ) => ( type_FunctionalData_class ( Var_0 ) & type_FunctionalInterface_class ( Var_1 ) ) ) ) .

-fof ( compliance_type_attribute_Function , axiom , ! [ Var_0 , Var_1 ] : ( rel_type_attribute_Function ( Var_0 , Var_1 ) => ( type_Function_class ( Var_0 ) & type_FunctionType_enum ( Var_1 ) ) ) ) .

-fof ( compliance_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_hasRoot , axiom , ! [ Var_parameter_F ] : ( rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_hasRoot ( Var_parameter_F ) => type_Function_class ( Var_parameter_F ) ) ) .

-fof ( relation_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_hasRoot , axiom , ! [ Var_parameter_F ] : ( type_Function_class ( Var_parameter_F ) => ( rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_hasRoot ( Var_parameter_F ) <=> ? [ Var_variable_Model ] : ( type_FunctionalArchitectureModel_class ( Var_variable_Model ) & rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_rootElements ( Var_variable_Model , Var_parameter_F ) ) ) ) ) .

-fof ( compliance_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_hasInt , axiom , ! [ Var_parameter_F ] : ( rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_hasInt ( Var_parameter_F ) => type_Function_class ( Var_parameter_F ) ) ) .

-fof ( relation_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_hasInt , axiom , ! [ Var_parameter_F ] : ( type_Function_class ( Var_parameter_F ) => ( rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_hasInt ( Var_parameter_F ) <=> ! [ Var_variable_Child , Var_variable_Model ] : ( ( type_Function_class ( Var_variable_Child ) & type_FunctionalArchitectureModel_class ( Var_variable_Model ) ) => ( type_Function_class ( Var_parameter_F ) & ( ~ rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_parent ( Var_variable_Child , Var_parameter_F ) & ~ rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_rootElements ( Var_variable_Model , Var_parameter_F ) ) ) ) ) ) ) .

-fof ( compliance_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_hasLeaf , axiom , ! [ Var_parameter_F ] : ( rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_hasLeaf ( Var_parameter_F ) => type_Function_class ( Var_parameter_F ) ) ) .

-fof ( relation_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_hasLeaf , axiom , ! [ Var_parameter_F ] : ( type_Function_class ( Var_parameter_F ) => ( rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_hasLeaf ( Var_parameter_F ) <=> ? [ Var_variable_Par , Var_variable_Child ] : ( type_Function_class ( Var_variable_Par ) & ( type_Function_class ( Var_variable_Child ) & ( rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_parent ( Var_parameter_F , Var_variable_Par ) & rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_parent ( Var_variable_Child , Var_parameter_F ) ) ) ) ) ) ) .

-fof ( compliance_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_model , axiom , ! [ Var_parameter_This , Var_parameter_Target ] : ( rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_model ( Var_parameter_This , Var_parameter_Target ) => ( type_FunctionalArchitectureModel_class ( Var_parameter_Target ) & type_FunctionalElement_class ( Var_parameter_This ) ) ) ) .

-fof ( relation_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_model , axiom , ! [ Var_parameter_This , Var_parameter_Target ] : ( ( type_FunctionalArchitectureModel_class ( Var_parameter_Target ) & type_FunctionalElement_class ( Var_parameter_This ) ) => ( rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_model ( Var_parameter_This , Var_parameter_Target ) <=> ( type_FunctionalElement_class ( Var_parameter_This ) & type_FunctionalArchitectureModel_class ( Var_parameter_Target ) ) ) ) ) .

-fof ( compliance_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_rootElements , axiom , ! [ Var_parameter_Model , Var_parameter_Root ] : ( rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_rootElements ( Var_parameter_Model , Var_parameter_Root ) => ( type_FunctionalArchitectureModel_class ( Var_parameter_Model ) & type_Function_class ( Var_parameter_Root ) ) ) ) .

-fof ( relation_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_rootElements , axiom , ! [ Var_parameter_Model , Var_parameter_Root ] : ( ( type_FunctionalArchitectureModel_class ( Var_parameter_Model ) & type_Function_class ( Var_parameter_Root ) ) => ( rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_rootElements ( Var_parameter_Model , Var_parameter_Root ) <=> ( type_Function_class ( Var_parameter_Root ) & rel_rootElements_reference_FunctionalArchitectureModel ( Var_parameter_Model , Var_parameter_Root ) ) ) ) ) .

-fof ( compliance_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_type , axiom , ! [ Var_parameter_This , Var_parameter_Target ] : ( rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_type ( Var_parameter_This , Var_parameter_Target ) => ( type_FunctionType_enum ( Var_parameter_Target ) & type_Function_class ( Var_parameter_This ) ) ) ) .

-fof ( relation_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_type , axiom , ! [ Var_parameter_This , Var_parameter_Target ] : ( ( type_FunctionType_enum ( Var_parameter_Target ) & type_Function_class ( Var_parameter_This ) ) => ( rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_type ( Var_parameter_This , Var_parameter_Target ) <=> ( ? [ Var_variable_Model ] : ( type_FunctionalArchitectureModel_class ( Var_variable_Model ) & ( rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_rootElements ( Var_variable_Model , Var_parameter_This ) & Var_parameter_Target = "aRoot literal FunctionType" ) ) | ( ! [ Var_variable_Child , Var_variable_Model ] : ( ( type_Function_class ( Var_variable_Child ) & type_FunctionalArchitectureModel_class ( Var_variable_Model ) ) => ( type_Function_class ( Var_parameter_This ) & ( ~ rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_parent ( Var_variable_Child , Var_parameter_This ) & ( ~ rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_rootElements ( Var_variable_Model , Var_parameter_This ) & Var_parameter_Target = "aLeaf literal FunctionType" ) ) ) ) | ? [ Var_variable_Par , Var_variable_Child ] : ( type_Function_class ( Var_variable_Par ) & ( type_Function_class ( Var_variable_Child ) & ( rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_parent ( Var_parameter_This , Var_variable_Par ) & ( rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_parent ( Var_variable_Child , Var_parameter_This ) & Var_parameter_Target = "aIntermediate literal FunctionType" ) ) ) ) ) ) ) ) ) .

-fof ( compliance_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_parent , axiom , ! [ Var_parameter_Func , Var_parameter_Par ] : ( rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_parent ( Var_parameter_Func , Var_parameter_Par ) => ( type_Function_class ( Var_parameter_Par ) & type_Function_class ( Var_parameter_Func ) ) ) ) .

-fof ( relation_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_parent , axiom , ! [ Var_parameter_Func , Var_parameter_Par ] : ( ( type_Function_class ( Var_parameter_Par ) & type_Function_class ( Var_parameter_Func ) ) => ( rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_parent ( Var_parameter_Func , Var_parameter_Par ) <=> ( type_Function_class ( Var_parameter_Func ) & ( rel_parent_reference_FunctionalElement ( Var_parameter_Func , Var_parameter_Par ) & type_Function_class ( Var_parameter_Par ) ) ) ) ) ) .

-fof ( compliance_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_terminatorAndInformation , axiom , ! [ Var_parameter_T , Var_parameter_I ] : ( rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_terminatorAndInformation ( Var_parameter_T , Var_parameter_I ) => ( type_FAMTerminator_class ( Var_parameter_T ) & type_InformationLink_class ( Var_parameter_I ) ) ) ) .

-fof ( relation_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_terminatorAndInformation , axiom , ! [ Var_parameter_T , Var_parameter_I ] : ( ( type_FAMTerminator_class ( Var_parameter_T ) & type_InformationLink_class ( Var_parameter_I ) ) => ( rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_terminatorAndInformation ( Var_parameter_T , Var_parameter_I ) <=> ( ? [ Var_variable_Out ] : ( type_FunctionalOutput_class ( Var_variable_Out ) & ( rel_outgoingLinks_reference_FunctionalOutput ( Var_variable_Out , Var_parameter_I ) & rel_terminator_reference_FunctionalData ( Var_variable_Out , Var_parameter_T ) ) ) | ? [ Var_variable_In ] : ( type_FunctionalInput_class ( Var_variable_In ) & ( rel_to_reference_InformationLink ( Var_parameter_I , Var_variable_In ) & ( type_FunctionalInput_class ( Var_variable_In ) & rel_terminator_reference_FunctionalData ( Var_variable_In , Var_parameter_T ) ) ) ) ) ) ) ) .

-fof ( upperMultiplicity_interface_FunctionalElement , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( type_FunctionalElement_class ( Var_src ) & ( type_FunctionalInterface_class ( Var_trg_1 ) & type_FunctionalInterface_class ( Var_trg_2 ) ) ) => ( ( rel_interface_reference_FunctionalElement ( Var_src , Var_trg_1 ) & rel_interface_reference_FunctionalElement ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) .

-fof ( lowerMultiplicity_model_FunctionalElement , axiom , ! [ Var_src ] : ( type_FunctionalElement_class ( Var_src ) => ? [ Var_trg_1 ] : ( type_FunctionalArchitectureModel_class ( Var_trg_1 ) & rel_model_reference_FunctionalElement ( Var_src , Var_trg_1 ) ) ) ) .

-fof ( upperMultiplicity_model_FunctionalElement , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( type_FunctionalElement_class ( Var_src ) & ( type_FunctionalArchitectureModel_class ( Var_trg_1 ) & type_FunctionalArchitectureModel_class ( Var_trg_2 ) ) ) => ( ( rel_model_reference_FunctionalElement ( Var_src , Var_trg_1 ) & rel_model_reference_FunctionalElement ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) .

-fof ( upperMultiplicity_parent_FunctionalElement , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( type_FunctionalElement_class ( Var_src ) & ( type_Function_class ( Var_trg_1 ) & type_Function_class ( Var_trg_2 ) ) ) => ( ( rel_parent_reference_FunctionalElement ( Var_src , Var_trg_1 ) & rel_parent_reference_FunctionalElement ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) .

-fof ( upperMultiplicity_data_FAMTerminator , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( type_FAMTerminator_class ( Var_src ) & ( type_FunctionalData_class ( Var_trg_1 ) & type_FunctionalData_class ( Var_trg_2 ) ) ) => ( ( rel_data_reference_FAMTerminator ( Var_src , Var_trg_1 ) & rel_data_reference_FAMTerminator ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) .

-fof ( upperMultiplicity_from_InformationLink , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( type_InformationLink_class ( Var_src ) & ( type_FunctionalOutput_class ( Var_trg_1 ) & type_FunctionalOutput_class ( Var_trg_2 ) ) ) => ( ( rel_from_reference_InformationLink ( Var_src , Var_trg_1 ) & rel_from_reference_InformationLink ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) .

-fof ( lowerMultiplicity_to_InformationLink , axiom , ! [ Var_src ] : ( type_InformationLink_class ( Var_src ) => ? [ Var_trg_1 ] : ( type_FunctionalInput_class ( Var_trg_1 ) & rel_to_reference_InformationLink ( Var_src , Var_trg_1 ) ) ) ) .

-fof ( upperMultiplicity_to_InformationLink , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( type_InformationLink_class ( Var_src ) & ( type_FunctionalInput_class ( Var_trg_1 ) & type_FunctionalInput_class ( Var_trg_2 ) ) ) => ( ( rel_to_reference_InformationLink ( Var_src , Var_trg_1 ) & rel_to_reference_InformationLink ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) .

-fof ( upperMultiplicity_element_FunctionalInterface , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( type_FunctionalInterface_class ( Var_src ) & ( type_FunctionalElement_class ( Var_trg_1 ) & type_FunctionalElement_class ( Var_trg_2 ) ) ) => ( ( rel_element_reference_FunctionalInterface ( Var_src , Var_trg_1 ) & rel_element_reference_FunctionalInterface ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) .

-fof ( upperMultiplicity_terminator_FunctionalData , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( type_FunctionalData_class ( Var_src ) & ( type_FAMTerminator_class ( Var_trg_1 ) & type_FAMTerminator_class ( Var_trg_2 ) ) ) => ( ( rel_terminator_reference_FunctionalData ( Var_src , Var_trg_1 ) & rel_terminator_reference_FunctionalData ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) .

-fof ( upperMultiplicity_interface_FunctionalData , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( type_FunctionalData_class ( Var_src ) & ( type_FunctionalInterface_class ( Var_trg_1 ) & type_FunctionalInterface_class ( Var_trg_2 ) ) ) => ( ( rel_interface_reference_FunctionalData ( Var_src , Var_trg_1 ) & rel_interface_reference_FunctionalData ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) .

-fof ( oppositeReference_interface_FunctionalElement , axiom , ! [ Var_src , Var_trg ] : ( ( type_FunctionalElement_class ( Var_src ) & type_FunctionalInterface_class ( Var_trg ) ) => ( rel_interface_reference_FunctionalElement ( Var_src , Var_trg ) <=> rel_element_reference_FunctionalInterface ( Var_trg , Var_src ) ) ) ) .

-fof ( oppositeReference_parent_FunctionalElement , axiom , ! [ Var_src , Var_trg ] : ( ( type_FunctionalElement_class ( Var_src ) & type_Function_class ( Var_trg ) ) => ( rel_parent_reference_FunctionalElement ( Var_src , Var_trg ) <=> rel_subElements_reference_Function ( Var_trg , Var_src ) ) ) ) .

-fof ( oppositeReference_data_FAMTerminator , axiom , ! [ Var_src , Var_trg ] : ( ( type_FAMTerminator_class ( Var_src ) & type_FunctionalData_class ( Var_trg ) ) => ( rel_data_reference_FAMTerminator ( Var_src , Var_trg ) <=> rel_terminator_reference_FunctionalData ( Var_trg , Var_src ) ) ) ) .

-fof ( oppositeReference_from_InformationLink , axiom , ! [ Var_src , Var_trg ] : ( ( type_InformationLink_class ( Var_src ) & type_FunctionalOutput_class ( Var_trg ) ) => ( rel_from_reference_InformationLink ( Var_src , Var_trg ) <=> rel_outgoingLinks_reference_FunctionalOutput ( Var_trg , Var_src ) ) ) ) .

-fof ( oppositeReference_to_InformationLink , axiom , ! [ Var_src , Var_trg ] : ( ( type_InformationLink_class ( Var_src ) & type_FunctionalInput_class ( Var_trg ) ) => ( rel_to_reference_InformationLink ( Var_src , Var_trg ) <=> rel_IncomingLinks_reference_FunctionalInput ( Var_trg , Var_src ) ) ) ) .

-fof ( oppositeReference_data_FunctionalInterface , axiom , ! [ Var_src , Var_trg ] : ( ( type_FunctionalInterface_class ( Var_src ) & type_FunctionalData_class ( Var_trg ) ) => ( rel_data_reference_FunctionalInterface ( Var_src , Var_trg ) <=> rel_interface_reference_FunctionalData ( Var_trg , Var_src ) ) ) ) .

-fof ( lowerMultiplicity_type_Function , axiom , ! [ Var_src ] : ( type_Function_class ( Var_src ) => ? [ Var_trg_1 ] : ( type_FunctionType_enum ( Var_trg_1 ) & rel_type_attribute_Function ( Var_src , Var_trg_1 ) ) ) ) .

-fof ( upperMultiplicity_type_Function , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( type_Function_class ( Var_src ) & ( type_FunctionType_enum ( Var_trg_1 ) & type_FunctionType_enum ( Var_trg_2 ) ) ) => ( ( rel_type_attribute_Function ( Var_src , Var_trg_1 ) & rel_type_attribute_Function ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) .

-fof ( errorpattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_terminatorAndInformation , axiom , ! [ Var_p0 , Var_p1 ] : ( ( type_FAMTerminator_class ( Var_p0 ) & type_InformationLink_class ( Var_p1 ) ) => ~ rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_terminatorAndInformation ( Var_p0 , Var_p1 ) ) ) .

+fof ( typeDef_FunctionType_enum , axiom , ! [ A ] : ( t_FunctionType_enum ( A ) <=> ( e_Root_literal_FunctionType_FunctionType_enum ( A ) | ( e_Intermediate_literal_FunctionType_FunctionType_enum ( A ) | e_Leaf_literal_FunctionType_FunctionType_enum ( A ) ) ) ) ) .

+fof ( hierarchyHandler , axiom , ! [ A ] : ( object ( A ) <=> ( ( t_InformationLink_class ( A ) & ( ~ t_FunctionType_enum ( A ) & ( ~ t_FunctionalData_class ( A ) & ( ~ t_FunctionalOutput_class ( A ) & ( ~ t_Function_class ( A ) & ( ~ t_FunctionalInput_class ( A ) & ( ~ t_FunctionalArchitectureModel_class ( A ) & ( ~ t_FunctionalElement_class ( A ) & ( ~ t_FunctionalInterface_class ( A ) & ~ t_FAMTerminator_class ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_InformationLink_class ( A ) & ( t_FunctionType_enum ( A ) & ( ~ t_FunctionalData_class ( A ) & ( ~ t_FunctionalOutput_class ( A ) & ( ~ t_Function_class ( A ) & ( ~ t_FunctionalInput_class ( A ) & ( ~ t_FunctionalArchitectureModel_class ( A ) & ( ~ t_FunctionalElement_class ( A ) & ( ~ t_FunctionalInterface_class ( A ) & ~ t_FAMTerminator_class ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_InformationLink_class ( A ) & ( ~ t_FunctionType_enum ( A ) & ( t_FunctionalData_class ( A ) & ( t_FunctionalOutput_class ( A ) & ( ~ t_Function_class ( A ) & ( ~ t_FunctionalInput_class ( A ) & ( ~ t_FunctionalArchitectureModel_class ( A ) & ( ~ t_FunctionalElement_class ( A ) & ( ~ t_FunctionalInterface_class ( A ) & ~ t_FAMTerminator_class ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_InformationLink_class ( A ) & ( ~ t_FunctionType_enum ( A ) & ( ~ t_FunctionalData_class ( A ) & ( ~ t_FunctionalOutput_class ( A ) & ( t_Function_class ( A ) & ( ~ t_FunctionalInput_class ( A ) & ( ~ t_FunctionalArchitectureModel_class ( A ) & ( t_FunctionalElement_class ( A ) & ( ~ t_FunctionalInterface_class ( A ) & ~ t_FAMTerminator_class ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_InformationLink_class ( A ) & ( ~ t_FunctionType_enum ( A ) & ( t_FunctionalData_class ( A ) & ( ~ t_FunctionalOutput_class ( A ) & ( ~ t_Function_class ( A ) & ( t_FunctionalInput_class ( A ) & ( ~ t_FunctionalArchitectureModel_class ( A ) & ( ~ t_FunctionalElement_class ( A ) & ( ~ t_FunctionalInterface_class ( A ) & ~ t_FAMTerminator_class ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_InformationLink_class ( A ) & ( ~ t_FunctionType_enum ( A ) & ( ~ t_FunctionalData_class ( A ) & ( ~ t_FunctionalOutput_class ( A ) & ( ~ t_Function_class ( A ) & ( ~ t_FunctionalInput_class ( A ) & ( t_FunctionalArchitectureModel_class ( A ) & ( ~ t_FunctionalElement_class ( A ) & ( ~ t_FunctionalInterface_class ( A ) & ~ t_FAMTerminator_class ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_InformationLink_class ( A ) & ( ~ t_FunctionType_enum ( A ) & ( ~ t_FunctionalData_class ( A ) & ( ~ t_FunctionalOutput_class ( A ) & ( ~ t_Function_class ( A ) & ( ~ t_FunctionalInput_class ( A ) & ( ~ t_FunctionalArchitectureModel_class ( A ) & ( ~ t_FunctionalElement_class ( A ) & ( t_FunctionalInterface_class ( A ) & ~ t_FAMTerminator_class ( A ) ) ) ) ) ) ) ) ) ) | ( ~ t_InformationLink_class ( A ) & ( ~ t_FunctionType_enum ( A ) & ( ~ t_FunctionalData_class ( A ) & ( ~ t_FunctionalOutput_class ( A ) & ( ~ t_Function_class ( A ) & ( ~ t_FunctionalInput_class ( A ) & ( ~ t_FunctionalArchitectureModel_class ( A ) & ( ~ t_FunctionalElement_class ( A ) & ( ~ t_FunctionalInterface_class ( A ) & t_FAMTerminator_class ( A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) .

+fof ( typeScope , axiom , ! [ A ] : ( object ( A ) <=> ( A = o1 | ( A = o2 | ( A = o3 | ( A = o4 | A = o5 ) ) ) ) ) ) .

+fof ( typeUniqueness , axiom , o1 != o2 & ( o1 != o3 & ( o2 != o3 & ( o1 != o4 & ( o2 != o4 & ( o3 != o4 & ( o1 != o5 & ( o2 != o5 & ( o3 != o5 & o4 != o5 ) ) ) ) ) ) ) ) ) .

+fof ( compliance_interface_reference_FunctionalElement , axiom , ! [ Var_0 , Var_1 ] : ( rel_interface_reference_FunctionalElement ( Var_0 , Var_1 ) => ( t_FunctionalElement_class ( Var_0 ) & t_FunctionalInterface_class ( Var_1 ) ) ) ) .

+fof ( compliance_model_reference_FunctionalElement , axiom , ! [ Var_0 , Var_1 ] : ( rel_model_reference_FunctionalElement ( Var_0 , Var_1 ) => ( t_FunctionalElement_class ( Var_0 ) & t_FunctionalArchitectureModel_class ( Var_1 ) ) ) ) .

+fof ( compliance_parent_reference_FunctionalElement , axiom , ! [ Var_0 , Var_1 ] : ( rel_parent_reference_FunctionalElement ( Var_0 , Var_1 ) => ( t_FunctionalElement_class ( Var_0 ) & t_Function_class ( Var_1 ) ) ) ) .

+fof ( compliance_rootElements_reference_FunctionalArchitectureModel , axiom , ! [ Var_0 , Var_1 ] : ( rel_rootElements_reference_FunctionalArchitectureModel ( Var_0 , Var_1 ) => ( t_FunctionalArchitectureModel_class ( Var_0 ) & t_FunctionalElement_class ( Var_1 ) ) ) ) .

+fof ( compliance_subElements_reference_Function , axiom , ! [ Var_0 , Var_1 ] : ( rel_subElements_reference_Function ( Var_0 , Var_1 ) => ( t_Function_class ( Var_0 ) & t_FunctionalElement_class ( Var_1 ) ) ) ) .

+fof ( compliance_data_reference_FAMTerminator , axiom , ! [ Var_0 , Var_1 ] : ( rel_data_reference_FAMTerminator ( Var_0 , Var_1 ) => ( t_FAMTerminator_class ( Var_0 ) & t_FunctionalData_class ( Var_1 ) ) ) ) .

+fof ( compliance_from_reference_InformationLink , axiom , ! [ Var_0 , Var_1 ] : ( rel_from_reference_InformationLink ( Var_0 , Var_1 ) => ( t_InformationLink_class ( Var_0 ) & t_FunctionalOutput_class ( Var_1 ) ) ) ) .

+fof ( compliance_to_reference_InformationLink , axiom , ! [ Var_0 , Var_1 ] : ( rel_to_reference_InformationLink ( Var_0 , Var_1 ) => ( t_InformationLink_class ( Var_0 ) & t_FunctionalInput_class ( Var_1 ) ) ) ) .

+fof ( compliance_data_reference_FunctionalInterface , axiom , ! [ Var_0 , Var_1 ] : ( rel_data_reference_FunctionalInterface ( Var_0 , Var_1 ) => ( t_FunctionalInterface_class ( Var_0 ) & t_FunctionalData_class ( Var_1 ) ) ) ) .

+fof ( compliance_element_reference_FunctionalInterface , axiom , ! [ Var_0 , Var_1 ] : ( rel_element_reference_FunctionalInterface ( Var_0 , Var_1 ) => ( t_FunctionalInterface_class ( Var_0 ) & t_FunctionalElement_class ( Var_1 ) ) ) ) .

+fof ( compliance_IncomingLinks_reference_FunctionalInput , axiom , ! [ Var_0 , Var_1 ] : ( rel_IncomingLinks_reference_FunctionalInput ( Var_0 , Var_1 ) => ( t_FunctionalInput_class ( Var_0 ) & t_InformationLink_class ( Var_1 ) ) ) ) .

+fof ( compliance_outgoingLinks_reference_FunctionalOutput , axiom , ! [ Var_0 , Var_1 ] : ( rel_outgoingLinks_reference_FunctionalOutput ( Var_0 , Var_1 ) => ( t_FunctionalOutput_class ( Var_0 ) & t_InformationLink_class ( Var_1 ) ) ) ) .

+fof ( compliance_terminator_reference_FunctionalData , axiom , ! [ Var_0 , Var_1 ] : ( rel_terminator_reference_FunctionalData ( Var_0 , Var_1 ) => ( t_FunctionalData_class ( Var_0 ) & t_FAMTerminator_class ( Var_1 ) ) ) ) .

+fof ( compliance_interface_reference_FunctionalData , axiom , ! [ Var_0 , Var_1 ] : ( rel_interface_reference_FunctionalData ( Var_0 , Var_1 ) => ( t_FunctionalData_class ( Var_0 ) & t_FunctionalInterface_class ( Var_1 ) ) ) ) .

+fof ( compliance_type_attribute_Function , axiom , ! [ Var_0 , Var_1 ] : ( rel_type_attribute_Function ( Var_0 , Var_1 ) => ( t_Function_class ( Var_0 ) & t_FunctionType_enum ( Var_1 ) ) ) ) .

+fof ( compliance_pattern_ca_mcgill_ecse_dslreasoner_vampire_queries_terminatorAndInformation , axiom , ! [ Var_parameter_T , Var_parameter_I ] : ( rel_pattern_ca_mcgill_ecse_dslreasoner_vampire_queries_terminatorAndInformation ( Var_parameter_T , Var_parameter_I ) => ( t_FAMTerminator_class ( Var_parameter_T ) & t_InformationLink_class ( Var_parameter_I ) ) ) ) .

+fof ( relation_pattern_ca_mcgill_ecse_dslreasoner_vampire_queries_terminatorAndInformation , axiom , ! [ Var_parameter_T , Var_parameter_I ] : ( ( t_FAMTerminator_class ( Var_parameter_T ) & t_InformationLink_class ( Var_parameter_I ) ) => ( rel_pattern_ca_mcgill_ecse_dslreasoner_vampire_queries_terminatorAndInformation ( Var_parameter_T , Var_parameter_I ) <=> ( ? [ Var_variable_Out ] : ( t_FunctionalOutput_class ( Var_variable_Out ) & ( rel_outgoingLinks_reference_FunctionalOutput ( Var_variable_Out , Var_parameter_I ) & rel_terminator_reference_FunctionalData ( Var_variable_Out , Var_parameter_T ) ) ) | ? [ Var_variable_In ] : ( t_FunctionalInput_class ( Var_variable_In ) & ( rel_to_reference_InformationLink ( Var_parameter_I , Var_variable_In ) & rel_terminator_reference_FunctionalData ( Var_variable_In , Var_parameter_T ) ) ) ) ) ) ) .

+fof ( upperMultiplicity_interface_FunctionalElement , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( t_FunctionalElement_class ( Var_src ) & ( t_FunctionalInterface_class ( Var_trg_1 ) & t_FunctionalInterface_class ( Var_trg_2 ) ) ) => ( ( rel_interface_reference_FunctionalElement ( Var_src , Var_trg_1 ) & rel_interface_reference_FunctionalElement ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) .

+fof ( lowerMultiplicity_model_FunctionalElement , axiom , ! [ Var_src ] : ( t_FunctionalElement_class ( Var_src ) => ? [ Var_trg_1 ] : ( t_FunctionalArchitectureModel_class ( Var_trg_1 ) & rel_model_reference_FunctionalElement ( Var_src , Var_trg_1 ) ) ) ) .

+fof ( upperMultiplicity_model_FunctionalElement , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( t_FunctionalElement_class ( Var_src ) & ( t_FunctionalArchitectureModel_class ( Var_trg_1 ) & t_FunctionalArchitectureModel_class ( Var_trg_2 ) ) ) => ( ( rel_model_reference_FunctionalElement ( Var_src , Var_trg_1 ) & rel_model_reference_FunctionalElement ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) .

+fof ( upperMultiplicity_parent_FunctionalElement , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( t_FunctionalElement_class ( Var_src ) & ( t_Function_class ( Var_trg_1 ) & t_Function_class ( Var_trg_2 ) ) ) => ( ( rel_parent_reference_FunctionalElement ( Var_src , Var_trg_1 ) & rel_parent_reference_FunctionalElement ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) .

+fof ( upperMultiplicity_data_FAMTerminator , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( t_FAMTerminator_class ( Var_src ) & ( t_FunctionalData_class ( Var_trg_1 ) & t_FunctionalData_class ( Var_trg_2 ) ) ) => ( ( rel_data_reference_FAMTerminator ( Var_src , Var_trg_1 ) & rel_data_reference_FAMTerminator ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) .

+fof ( upperMultiplicity_from_InformationLink , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( t_InformationLink_class ( Var_src ) & ( t_FunctionalOutput_class ( Var_trg_1 ) & t_FunctionalOutput_class ( Var_trg_2 ) ) ) => ( ( rel_from_reference_InformationLink ( Var_src , Var_trg_1 ) & rel_from_reference_InformationLink ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) .

+fof ( lowerMultiplicity_to_InformationLink , axiom , ! [ Var_src ] : ( t_InformationLink_class ( Var_src ) => ? [ Var_trg_1 ] : ( t_FunctionalInput_class ( Var_trg_1 ) & rel_to_reference_InformationLink ( Var_src , Var_trg_1 ) ) ) ) .

+fof ( upperMultiplicity_to_InformationLink , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( t_InformationLink_class ( Var_src ) & ( t_FunctionalInput_class ( Var_trg_1 ) & t_FunctionalInput_class ( Var_trg_2 ) ) ) => ( ( rel_to_reference_InformationLink ( Var_src , Var_trg_1 ) & rel_to_reference_InformationLink ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) .

+fof ( upperMultiplicity_element_FunctionalInterface , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( t_FunctionalInterface_class ( Var_src ) & ( t_FunctionalElement_class ( Var_trg_1 ) & t_FunctionalElement_class ( Var_trg_2 ) ) ) => ( ( rel_element_reference_FunctionalInterface ( Var_src , Var_trg_1 ) & rel_element_reference_FunctionalInterface ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) .

+fof ( upperMultiplicity_terminator_FunctionalData , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( t_FunctionalData_class ( Var_src ) & ( t_FAMTerminator_class ( Var_trg_1 ) & t_FAMTerminator_class ( Var_trg_2 ) ) ) => ( ( rel_terminator_reference_FunctionalData ( Var_src , Var_trg_1 ) & rel_terminator_reference_FunctionalData ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) .

+fof ( upperMultiplicity_interface_FunctionalData , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( t_FunctionalData_class ( Var_src ) & ( t_FunctionalInterface_class ( Var_trg_1 ) & t_FunctionalInterface_class ( Var_trg_2 ) ) ) => ( ( rel_interface_reference_FunctionalData ( Var_src , Var_trg_1 ) & rel_interface_reference_FunctionalData ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) .

+fof ( oppositeReference_interface_FunctionalElement , axiom , ! [ Var_src , Var_trg ] : ( ( t_FunctionalElement_class ( Var_src ) & t_FunctionalInterface_class ( Var_trg ) ) => ( rel_interface_reference_FunctionalElement ( Var_src , Var_trg ) <=> rel_element_reference_FunctionalInterface ( Var_trg , Var_src ) ) ) ) .

+fof ( oppositeReference_parent_FunctionalElement , axiom , ! [ Var_src , Var_trg ] : ( ( t_FunctionalElement_class ( Var_src ) & t_Function_class ( Var_trg ) ) => ( rel_parent_reference_FunctionalElement ( Var_src , Var_trg ) <=> rel_subElements_reference_Function ( Var_trg , Var_src ) ) ) ) .

+fof ( oppositeReference_data_FAMTerminator , axiom , ! [ Var_src , Var_trg ] : ( ( t_FAMTerminator_class ( Var_src ) & t_FunctionalData_class ( Var_trg ) ) => ( rel_data_reference_FAMTerminator ( Var_src , Var_trg ) <=> rel_terminator_reference_FunctionalData ( Var_trg , Var_src ) ) ) ) .

+fof ( oppositeReference_from_InformationLink , axiom , ! [ Var_src , Var_trg ] : ( ( t_InformationLink_class ( Var_src ) & t_FunctionalOutput_class ( Var_trg ) ) => ( rel_from_reference_InformationLink ( Var_src , Var_trg ) <=> rel_outgoingLinks_reference_FunctionalOutput ( Var_trg , Var_src ) ) ) ) .

+fof ( oppositeReference_to_InformationLink , axiom , ! [ Var_src , Var_trg ] : ( ( t_InformationLink_class ( Var_src ) & t_FunctionalInput_class ( Var_trg ) ) => ( rel_to_reference_InformationLink ( Var_src , Var_trg ) <=> rel_IncomingLinks_reference_FunctionalInput ( Var_trg , Var_src ) ) ) ) .

+fof ( oppositeReference_data_FunctionalInterface , axiom , ! [ Var_src , Var_trg ] : ( ( t_FunctionalInterface_class ( Var_src ) & t_FunctionalData_class ( Var_trg ) ) => ( rel_data_reference_FunctionalInterface ( Var_src , Var_trg ) <=> rel_interface_reference_FunctionalData ( Var_trg , Var_src ) ) ) ) .

+fof ( lowerMultiplicity_type_Function , axiom , ! [ Var_src ] : ( t_Function_class ( Var_src ) => ? [ Var_trg_1 ] : ( t_FunctionType_enum ( Var_trg_1 ) & rel_type_attribute_Function ( Var_src , Var_trg_1 ) ) ) ) .

+fof ( upperMultiplicity_type_Function , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( t_Function_class ( Var_src ) & ( t_FunctionType_enum ( Var_trg_1 ) & t_FunctionType_enum ( Var_trg_2 ) ) ) => ( ( rel_type_attribute_Function ( Var_src , Var_trg_1 ) & rel_type_attribute_Function ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) .

+fof ( errorpattern_ca_mcgill_ecse_dslreasoner_vampire_queries_terminatorAndInformation , axiom , ! [ Var_p0 , Var_p1 ] : ( ( t_FAMTerminator_class ( Var_p0 ) & t_InformationLink_class ( Var_p1 ) ) => ~ rel_pattern_ca_mcgill_ecse_dslreasoner_vampire_queries_terminatorAndInformation ( Var_p0 , Var_p1 ) ) ) .

diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/MedicalSystem/vampireProblem.tptp b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/MedicalSystem/vampireProblem.tptp
index aa088242..c23afb9a 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/MedicalSystem/vampireProblem.tptp
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/MedicalSystem/vampireProblem.tptp
@@ -1,6 +1,6 @@
 % This is an initial Test Comment

 fof ( typeDef_HealthSystem_class_DefinedPart , axiom , ! [ A ] : ( type_HealthSystem_class_DefinedPart ( A ) <=> A = "ao 1" ) ) .

-fof ( hierarchyHandler , axiom , ! [ A ] : ( object ( A ) <=> ( ( type_Allergy_class ( A ) & ( ~ type_Treatment_class ( A ) & ( ~ type_Medicine_class ( A ) & ( ~ type_HealthSystem_class_UndefinedPart ( A ) & ( ~ type_Symptom_class ( A ) & ( ~ type_ExaminationResult_class ( A ) & ( ~ type_Examination_class ( A ) & ( ~ type_Disease_class ( A ) & ( ~ type_MedicalRecord_class ( A ) & ( ~ type_Immunization_class ( A ) & ( ~ type_Patient_class ( A ) & ( ~ type_Injury_class ( A ) & ( ~ type_HealthSystem_class ( A ) & ( ~ type_HealthSystem_class_DefinedPart ( A ) & ( ~ type_Medication_class ( A ) & type_HealthProblem_class ( A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ( ( ~ type_Allergy_class ( A ) & ( ~ type_Treatment_class ( A ) & ( type_Medicine_class ( A ) & ( ~ type_HealthSystem_class_UndefinedPart ( A ) & ( ~ type_Symptom_class ( A ) & ( ~ type_ExaminationResult_class ( A ) & ( ~ type_Examination_class ( A ) & ( ~ type_Disease_class ( A ) & ( ~ type_MedicalRecord_class ( A ) & ( ~ type_Immunization_class ( A ) & ( ~ type_Patient_class ( A ) & ( ~ type_Injury_class ( A ) & ( ~ type_HealthSystem_class ( A ) & ( ~ type_HealthSystem_class_DefinedPart ( A ) & ( ~ type_Medication_class ( A ) & ~ type_HealthProblem_class ( A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ( ( ~ type_Allergy_class ( A ) & ( ~ type_Treatment_class ( A ) & ( ~ type_Medicine_class ( A ) & ( type_HealthSystem_class_UndefinedPart ( A ) & ( ~ type_Symptom_class ( A ) & ( ~ type_ExaminationResult_class ( A ) & ( ~ type_Examination_class ( A ) & ( ~ type_Disease_class ( A ) & ( ~ type_MedicalRecord_class ( A ) & ( ~ type_Immunization_class ( A ) & ( ~ type_Patient_class ( A ) & ( ~ type_Injury_class ( A ) & ( type_HealthSystem_class ( A ) & ( ~ type_HealthSystem_class_DefinedPart ( A ) & ( ~ type_Medication_class ( A ) & ~ type_HealthProblem_class ( A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ( ( ~ type_Allergy_class ( A ) & ( ~ type_Treatment_class ( A ) & ( ~ type_Medicine_class ( A ) & ( ~ type_HealthSystem_class_UndefinedPart ( A ) & ( type_Symptom_class ( A ) & ( ~ type_ExaminationResult_class ( A ) & ( ~ type_Examination_class ( A ) & ( ~ type_Disease_class ( A ) & ( ~ type_MedicalRecord_class ( A ) & ( ~ type_Immunization_class ( A ) & ( ~ type_Patient_class ( A ) & ( ~ type_Injury_class ( A ) & ( ~ type_HealthSystem_class ( A ) & ( ~ type_HealthSystem_class_DefinedPart ( A ) & ( ~ type_Medication_class ( A ) & ~ type_HealthProblem_class ( A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ( ( ~ type_Allergy_class ( A ) & ( ~ type_Treatment_class ( A ) & ( ~ type_Medicine_class ( A ) & ( ~ type_HealthSystem_class_UndefinedPart ( A ) & ( ~ type_Symptom_class ( A ) & ( type_ExaminationResult_class ( A ) & ( ~ type_Examination_class ( A ) & ( ~ type_Disease_class ( A ) & ( ~ type_MedicalRecord_class ( A ) & ( ~ type_Immunization_class ( A ) & ( ~ type_Patient_class ( A ) & ( ~ type_Injury_class ( A ) & ( ~ type_HealthSystem_class ( A ) & ( ~ type_HealthSystem_class_DefinedPart ( A ) & ( ~ type_Medication_class ( A ) & ~ type_HealthProblem_class ( A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ( ( ~ type_Allergy_class ( A ) & ( ~ type_Treatment_class ( A ) & ( ~ type_Medicine_class ( A ) & ( ~ type_HealthSystem_class_UndefinedPart ( A ) & ( ~ type_Symptom_class ( A ) & ( ~ type_ExaminationResult_class ( A ) & ( type_Examination_class ( A ) & ( ~ type_Disease_class ( A ) & ( ~ type_MedicalRecord_class ( A ) & ( ~ type_Immunization_class ( A ) & ( ~ type_Patient_class ( A ) & ( ~ type_Injury_class ( A ) & ( ~ type_HealthSystem_class ( A ) & ( ~ type_HealthSystem_class_DefinedPart ( A ) & ( ~ type_Medication_class ( A ) & ~ type_HealthProblem_class ( A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ( ( ~ type_Allergy_class ( A ) & ( ~ type_Treatment_class ( A ) & ( ~ type_Medicine_class ( A ) & ( ~ type_HealthSystem_class_UndefinedPart ( A ) & ( ~ type_Symptom_class ( A ) & ( ~ type_ExaminationResult_class ( A ) & ( ~ type_Examination_class ( A ) & ( type_Disease_class ( A ) & ( ~ type_MedicalRecord_class ( A ) & ( ~ type_Immunization_class ( A ) & ( ~ type_Patient_class ( A ) & ( ~ type_Injury_class ( A ) & ( ~ type_HealthSystem_class ( A ) & ( ~ type_HealthSystem_class_DefinedPart ( A ) & ( ~ type_Medication_class ( A ) & type_HealthProblem_class ( A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ( ( ~ type_Allergy_class ( A ) & ( ~ type_Treatment_class ( A ) & ( ~ type_Medicine_class ( A ) & ( ~ type_HealthSystem_class_UndefinedPart ( A ) & ( ~ type_Symptom_class ( A ) & ( ~ type_ExaminationResult_class ( A ) & ( ~ type_Examination_class ( A ) & ( ~ type_Disease_class ( A ) & ( type_MedicalRecord_class ( A ) & ( ~ type_Immunization_class ( A ) & ( ~ type_Patient_class ( A ) & ( ~ type_Injury_class ( A ) & ( ~ type_HealthSystem_class ( A ) & ( ~ type_HealthSystem_class_DefinedPart ( A ) & ( ~ type_Medication_class ( A ) & ~ type_HealthProblem_class ( A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ( ( ~ type_Allergy_class ( A ) & ( type_Treatment_class ( A ) & ( ~ type_Medicine_class ( A ) & ( ~ type_HealthSystem_class_UndefinedPart ( A ) & ( ~ type_Symptom_class ( A ) & ( ~ type_ExaminationResult_class ( A ) & ( ~ type_Examination_class ( A ) & ( ~ type_Disease_class ( A ) & ( ~ type_MedicalRecord_class ( A ) & ( type_Immunization_class ( A ) & ( ~ type_Patient_class ( A ) & ( ~ type_Injury_class ( A ) & ( ~ type_HealthSystem_class ( A ) & ( ~ type_HealthSystem_class_DefinedPart ( A ) & ( ~ type_Medication_class ( A ) & ~ type_HealthProblem_class ( A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ( ( ~ type_Allergy_class ( A ) & ( ~ type_Treatment_class ( A ) & ( ~ type_Medicine_class ( A ) & ( ~ type_HealthSystem_class_UndefinedPart ( A ) & ( ~ type_Symptom_class ( A ) & ( ~ type_ExaminationResult_class ( A ) & ( ~ type_Examination_class ( A ) & ( ~ type_Disease_class ( A ) & ( ~ type_MedicalRecord_class ( A ) & ( ~ type_Immunization_class ( A ) & ( type_Patient_class ( A ) & ( ~ type_Injury_class ( A ) & ( ~ type_HealthSystem_class ( A ) & ( ~ type_HealthSystem_class_DefinedPart ( A ) & ( ~ type_Medication_class ( A ) & ~ type_HealthProblem_class ( A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ( ( ~ type_Allergy_class ( A ) & ( ~ type_Treatment_class ( A ) & ( ~ type_Medicine_class ( A ) & ( ~ type_HealthSystem_class_UndefinedPart ( A ) & ( ~ type_Symptom_class ( A ) & ( ~ type_ExaminationResult_class ( A ) & ( ~ type_Examination_class ( A ) & ( ~ type_Disease_class ( A ) & ( ~ type_MedicalRecord_class ( A ) & ( ~ type_Immunization_class ( A ) & ( ~ type_Patient_class ( A ) & ( type_Injury_class ( A ) & ( ~ type_HealthSystem_class ( A ) & ( ~ type_HealthSystem_class_DefinedPart ( A ) & ( ~ type_Medication_class ( A ) & type_HealthProblem_class ( A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ( ( ~ type_Allergy_class ( A ) & ( ~ type_Treatment_class ( A ) & ( ~ type_Medicine_class ( A ) & ( ~ type_HealthSystem_class_UndefinedPart ( A ) & ( ~ type_Symptom_class ( A ) & ( ~ type_ExaminationResult_class ( A ) & ( ~ type_Examination_class ( A ) & ( ~ type_Disease_class ( A ) & ( ~ type_MedicalRecord_class ( A ) & ( ~ type_Immunization_class ( A ) & ( ~ type_Patient_class ( A ) & ( ~ type_Injury_class ( A ) & ( type_HealthSystem_class ( A ) & ( type_HealthSystem_class_DefinedPart ( A ) & ( ~ type_Medication_class ( A ) & ~ type_HealthProblem_class ( A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ( ~ type_Allergy_class ( A ) & ( type_Treatment_class ( A ) & ( ~ type_Medicine_class ( A ) & ( ~ type_HealthSystem_class_UndefinedPart ( A ) & ( ~ type_Symptom_class ( A ) & ( ~ type_ExaminationResult_class ( A ) & ( ~ type_Examination_class ( A ) & ( ~ type_Disease_class ( A ) & ( ~ type_MedicalRecord_class ( A ) & ( ~ type_Immunization_class ( A ) & ( ~ type_Patient_class ( A ) & ( ~ type_Injury_class ( A ) & ( ~ type_HealthSystem_class ( A ) & ( ~ type_HealthSystem_class_DefinedPart ( A ) & ( type_Medication_class ( A ) & ~ type_HealthProblem_class ( A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) .

+fof ( hierarchyHandler , axiom , ! [ A ] : ( object ( A ) <=> ( ( type_MedicalRecord_class ( A ) & ( ~ type_Medicine_class ( A ) & ( ~ type_ExaminationResult_class ( A ) & ( ~ type_HealthSystem_class_DefinedPart ( A ) & ( ~ type_Patient_class ( A ) & ( ~ type_HealthSystem_class_UndefinedPart ( A ) & ( ~ type_Immunization_class ( A ) & ( ~ type_Treatment_class ( A ) & ( ~ type_Disease_class ( A ) & ( ~ type_HealthSystem_class ( A ) & ( ~ type_Examination_class ( A ) & ( ~ type_Injury_class ( A ) & ( ~ type_Allergy_class ( A ) & ( ~ type_Symptom_class ( A ) & ( ~ type_HealthProblem_class ( A ) & ~ type_Medication_class ( A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ( ( ~ type_MedicalRecord_class ( A ) & ( type_Medicine_class ( A ) & ( ~ type_ExaminationResult_class ( A ) & ( ~ type_HealthSystem_class_DefinedPart ( A ) & ( ~ type_Patient_class ( A ) & ( ~ type_HealthSystem_class_UndefinedPart ( A ) & ( ~ type_Immunization_class ( A ) & ( ~ type_Treatment_class ( A ) & ( ~ type_Disease_class ( A ) & ( ~ type_HealthSystem_class ( A ) & ( ~ type_Examination_class ( A ) & ( ~ type_Injury_class ( A ) & ( ~ type_Allergy_class ( A ) & ( ~ type_Symptom_class ( A ) & ( ~ type_HealthProblem_class ( A ) & ~ type_Medication_class ( A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ( ( ~ type_MedicalRecord_class ( A ) & ( ~ type_Medicine_class ( A ) & ( type_ExaminationResult_class ( A ) & ( ~ type_HealthSystem_class_DefinedPart ( A ) & ( ~ type_Patient_class ( A ) & ( ~ type_HealthSystem_class_UndefinedPart ( A ) & ( ~ type_Immunization_class ( A ) & ( ~ type_Treatment_class ( A ) & ( ~ type_Disease_class ( A ) & ( ~ type_HealthSystem_class ( A ) & ( ~ type_Examination_class ( A ) & ( ~ type_Injury_class ( A ) & ( ~ type_Allergy_class ( A ) & ( ~ type_Symptom_class ( A ) & ( ~ type_HealthProblem_class ( A ) & ~ type_Medication_class ( A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ( ( ~ type_MedicalRecord_class ( A ) & ( ~ type_Medicine_class ( A ) & ( ~ type_ExaminationResult_class ( A ) & ( type_HealthSystem_class_DefinedPart ( A ) & ( ~ type_Patient_class ( A ) & ( ~ type_HealthSystem_class_UndefinedPart ( A ) & ( ~ type_Immunization_class ( A ) & ( ~ type_Treatment_class ( A ) & ( ~ type_Disease_class ( A ) & ( type_HealthSystem_class ( A ) & ( ~ type_Examination_class ( A ) & ( ~ type_Injury_class ( A ) & ( ~ type_Allergy_class ( A ) & ( ~ type_Symptom_class ( A ) & ( ~ type_HealthProblem_class ( A ) & ~ type_Medication_class ( A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ( ( ~ type_MedicalRecord_class ( A ) & ( ~ type_Medicine_class ( A ) & ( ~ type_ExaminationResult_class ( A ) & ( ~ type_HealthSystem_class_DefinedPart ( A ) & ( type_Patient_class ( A ) & ( ~ type_HealthSystem_class_UndefinedPart ( A ) & ( ~ type_Immunization_class ( A ) & ( ~ type_Treatment_class ( A ) & ( ~ type_Disease_class ( A ) & ( ~ type_HealthSystem_class ( A ) & ( ~ type_Examination_class ( A ) & ( ~ type_Injury_class ( A ) & ( ~ type_Allergy_class ( A ) & ( ~ type_Symptom_class ( A ) & ( ~ type_HealthProblem_class ( A ) & ~ type_Medication_class ( A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ( ( ~ type_MedicalRecord_class ( A ) & ( ~ type_Medicine_class ( A ) & ( ~ type_ExaminationResult_class ( A ) & ( ~ type_HealthSystem_class_DefinedPart ( A ) & ( ~ type_Patient_class ( A ) & ( type_HealthSystem_class_UndefinedPart ( A ) & ( ~ type_Immunization_class ( A ) & ( ~ type_Treatment_class ( A ) & ( ~ type_Disease_class ( A ) & ( type_HealthSystem_class ( A ) & ( ~ type_Examination_class ( A ) & ( ~ type_Injury_class ( A ) & ( ~ type_Allergy_class ( A ) & ( ~ type_Symptom_class ( A ) & ( ~ type_HealthProblem_class ( A ) & ~ type_Medication_class ( A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ( ( ~ type_MedicalRecord_class ( A ) & ( ~ type_Medicine_class ( A ) & ( ~ type_ExaminationResult_class ( A ) & ( ~ type_HealthSystem_class_DefinedPart ( A ) & ( ~ type_Patient_class ( A ) & ( ~ type_HealthSystem_class_UndefinedPart ( A ) & ( type_Immunization_class ( A ) & ( type_Treatment_class ( A ) & ( ~ type_Disease_class ( A ) & ( ~ type_HealthSystem_class ( A ) & ( ~ type_Examination_class ( A ) & ( ~ type_Injury_class ( A ) & ( ~ type_Allergy_class ( A ) & ( ~ type_Symptom_class ( A ) & ( ~ type_HealthProblem_class ( A ) & ~ type_Medication_class ( A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ( ( ~ type_MedicalRecord_class ( A ) & ( ~ type_Medicine_class ( A ) & ( ~ type_ExaminationResult_class ( A ) & ( ~ type_HealthSystem_class_DefinedPart ( A ) & ( ~ type_Patient_class ( A ) & ( ~ type_HealthSystem_class_UndefinedPart ( A ) & ( ~ type_Immunization_class ( A ) & ( ~ type_Treatment_class ( A ) & ( type_Disease_class ( A ) & ( ~ type_HealthSystem_class ( A ) & ( ~ type_Examination_class ( A ) & ( ~ type_Injury_class ( A ) & ( ~ type_Allergy_class ( A ) & ( ~ type_Symptom_class ( A ) & ( type_HealthProblem_class ( A ) & ~ type_Medication_class ( A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ( ( ~ type_MedicalRecord_class ( A ) & ( ~ type_Medicine_class ( A ) & ( ~ type_ExaminationResult_class ( A ) & ( ~ type_HealthSystem_class_DefinedPart ( A ) & ( ~ type_Patient_class ( A ) & ( ~ type_HealthSystem_class_UndefinedPart ( A ) & ( ~ type_Immunization_class ( A ) & ( ~ type_Treatment_class ( A ) & ( ~ type_Disease_class ( A ) & ( ~ type_HealthSystem_class ( A ) & ( type_Examination_class ( A ) & ( ~ type_Injury_class ( A ) & ( ~ type_Allergy_class ( A ) & ( ~ type_Symptom_class ( A ) & ( ~ type_HealthProblem_class ( A ) & ~ type_Medication_class ( A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ( ( ~ type_MedicalRecord_class ( A ) & ( ~ type_Medicine_class ( A ) & ( ~ type_ExaminationResult_class ( A ) & ( ~ type_HealthSystem_class_DefinedPart ( A ) & ( ~ type_Patient_class ( A ) & ( ~ type_HealthSystem_class_UndefinedPart ( A ) & ( ~ type_Immunization_class ( A ) & ( ~ type_Treatment_class ( A ) & ( ~ type_Disease_class ( A ) & ( ~ type_HealthSystem_class ( A ) & ( ~ type_Examination_class ( A ) & ( type_Injury_class ( A ) & ( ~ type_Allergy_class ( A ) & ( ~ type_Symptom_class ( A ) & ( type_HealthProblem_class ( A ) & ~ type_Medication_class ( A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ( ( ~ type_MedicalRecord_class ( A ) & ( ~ type_Medicine_class ( A ) & ( ~ type_ExaminationResult_class ( A ) & ( ~ type_HealthSystem_class_DefinedPart ( A ) & ( ~ type_Patient_class ( A ) & ( ~ type_HealthSystem_class_UndefinedPart ( A ) & ( ~ type_Immunization_class ( A ) & ( ~ type_Treatment_class ( A ) & ( ~ type_Disease_class ( A ) & ( ~ type_HealthSystem_class ( A ) & ( ~ type_Examination_class ( A ) & ( ~ type_Injury_class ( A ) & ( type_Allergy_class ( A ) & ( ~ type_Symptom_class ( A ) & ( type_HealthProblem_class ( A ) & ~ type_Medication_class ( A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ( ( ~ type_MedicalRecord_class ( A ) & ( ~ type_Medicine_class ( A ) & ( ~ type_ExaminationResult_class ( A ) & ( ~ type_HealthSystem_class_DefinedPart ( A ) & ( ~ type_Patient_class ( A ) & ( ~ type_HealthSystem_class_UndefinedPart ( A ) & ( ~ type_Immunization_class ( A ) & ( ~ type_Treatment_class ( A ) & ( ~ type_Disease_class ( A ) & ( ~ type_HealthSystem_class ( A ) & ( ~ type_Examination_class ( A ) & ( ~ type_Injury_class ( A ) & ( ~ type_Allergy_class ( A ) & ( type_Symptom_class ( A ) & ( ~ type_HealthProblem_class ( A ) & ~ type_Medication_class ( A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ( ~ type_MedicalRecord_class ( A ) & ( ~ type_Medicine_class ( A ) & ( ~ type_ExaminationResult_class ( A ) & ( ~ type_HealthSystem_class_DefinedPart ( A ) & ( ~ type_Patient_class ( A ) & ( ~ type_HealthSystem_class_UndefinedPart ( A ) & ( ~ type_Immunization_class ( A ) & ( type_Treatment_class ( A ) & ( ~ type_Disease_class ( A ) & ( ~ type_HealthSystem_class ( A ) & ( ~ type_Examination_class ( A ) & ( ~ type_Injury_class ( A ) & ( ~ type_Allergy_class ( A ) & ( ~ type_Symptom_class ( A ) & ( ~ type_HealthProblem_class ( A ) & type_Medication_class ( A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) .

 fof ( compliance_records_reference_Patient , axiom , ! [ Var_0 , Var_1 ] : ( rel_records_reference_Patient ( Var_0 , Var_1 ) => ( type_Patient_class ( Var_0 ) & type_MedicalRecord_class ( Var_1 ) ) ) ) .

 fof ( compliance_healthsystem_reference_Patient , axiom , ! [ Var_0 , Var_1 ] : ( rel_healthsystem_reference_Patient ( Var_0 , Var_1 ) => ( type_Patient_class ( Var_0 ) & type_HealthSystem_class ( Var_1 ) ) ) ) .

 fof ( compliance_patient_reference_HealthSystem , axiom , ! [ Var_0 , Var_1 ] : ( rel_patient_reference_HealthSystem ( Var_0 , Var_1 ) => ( type_HealthSystem_class ( Var_0 ) & type_Patient_class ( Var_1 ) ) ) ) .

@@ -35,8 +35,8 @@ fof ( compliance_pattern_ca_mcgill_dp19_queries_allergy , axiom , ! [ Var_parame
 fof ( relation_pattern_ca_mcgill_dp19_queries_allergy , axiom , ! [ Var_parameter_mr , Var_parameter_al ] : ( ( type_Allergy_class ( Var_parameter_al ) & type_MedicalRecord_class ( Var_parameter_mr ) ) => ( rel_pattern_ca_mcgill_dp19_queries_allergy ( Var_parameter_mr , Var_parameter_al ) <=> ( type_Allergy_class ( Var_parameter_al ) & rel_pattern_ca_mcgill_dp19_queries_healthProblems ( Var_parameter_mr , Var_parameter_al ) ) ) ) ) .

 fof ( compliance_pattern_ca_mcgill_dp19_queries_allergyWithoutSymptom , axiom , ! [ Var_parameter_mr ] : ( rel_pattern_ca_mcgill_dp19_queries_allergyWithoutSymptom ( Var_parameter_mr ) => type_MedicalRecord_class ( Var_parameter_mr ) ) ) .

 fof ( relation_pattern_ca_mcgill_dp19_queries_allergyWithoutSymptom , axiom , ! [ Var_parameter_mr ] : ( type_MedicalRecord_class ( Var_parameter_mr ) => ( rel_pattern_ca_mcgill_dp19_queries_allergyWithoutSymptom ( Var_parameter_mr ) <=> ? [ Var_variable_al ] : ( type_Allergy_class ( Var_variable_al ) & ! [ Var_variable_0 ] : ( type_Symptom_class ( Var_variable_0 ) => ( rel_pattern_ca_mcgill_dp19_queries_allergy ( Var_parameter_mr , Var_variable_al ) & ~ rel_pattern_ca_mcgill_dp19_queries_symptom ( Var_parameter_mr , Var_variable_0 ) ) ) ) ) ) ) .

-fof ( compliance_pattern_ca_mcgill_dp19_queries_recommended , axiom , ! [ Var_parameter_hp , Var_parameter_med ] : ( rel_pattern_ca_mcgill_dp19_queries_recommended ( Var_parameter_hp , Var_parameter_med ) => ( type_Medicine_class ( Var_parameter_med ) & type_HealthProblem_class ( Var_parameter_hp ) ) ) ) .

-fof ( relation_pattern_ca_mcgill_dp19_queries_recommended , axiom , ! [ Var_parameter_hp , Var_parameter_med ] : ( ( type_Medicine_class ( Var_parameter_med ) & type_HealthProblem_class ( Var_parameter_hp ) ) => ( rel_pattern_ca_mcgill_dp19_queries_recommended ( Var_parameter_hp , Var_parameter_med ) <=> ( rel_recommended_medicine_reference_HealthProblem ( Var_parameter_hp , Var_parameter_med ) & type_Medicine_class ( Var_parameter_med ) ) ) ) ) .

+fof ( compliance_pattern_ca_mcgill_dp19_queries_recommended , axiom , ! [ Var_parameter_hp , Var_parameter_med ] : ( rel_pattern_ca_mcgill_dp19_queries_recommended ( Var_parameter_hp , Var_parameter_med ) => ( type_HealthProblem_class ( Var_parameter_hp ) & type_Medicine_class ( Var_parameter_med ) ) ) ) .

+fof ( relation_pattern_ca_mcgill_dp19_queries_recommended , axiom , ! [ Var_parameter_hp , Var_parameter_med ] : ( ( type_HealthProblem_class ( Var_parameter_hp ) & type_Medicine_class ( Var_parameter_med ) ) => ( rel_pattern_ca_mcgill_dp19_queries_recommended ( Var_parameter_hp , Var_parameter_med ) <=> ( rel_recommended_medicine_reference_HealthProblem ( Var_parameter_hp , Var_parameter_med ) & type_Medicine_class ( Var_parameter_med ) ) ) ) ) .

 fof ( compliance_pattern_ca_mcgill_dp19_queries_prescribedMedicineNotRecommended , axiom , ! [ Var_parameter_mr , Var_parameter_med ] : ( rel_pattern_ca_mcgill_dp19_queries_prescribedMedicineNotRecommended ( Var_parameter_mr , Var_parameter_med ) => ( type_Medicine_class ( Var_parameter_med ) & type_MedicalRecord_class ( Var_parameter_mr ) ) ) ) .

 fof ( relation_pattern_ca_mcgill_dp19_queries_prescribedMedicineNotRecommended , axiom , ! [ Var_parameter_mr , Var_parameter_med ] : ( ( type_Medicine_class ( Var_parameter_med ) & type_MedicalRecord_class ( Var_parameter_mr ) ) => ( rel_pattern_ca_mcgill_dp19_queries_prescribedMedicineNotRecommended ( Var_parameter_mr , Var_parameter_med ) <=> ? [ Var_variable_hp , Var_variable_tr ] : ( type_HealthProblem_class ( Var_variable_hp ) & ( type_Treatment_class ( Var_variable_tr ) & ( rel_pattern_ca_mcgill_dp19_queries_healthProblems ( Var_parameter_mr , Var_variable_hp ) & ( rel_pattern_ca_mcgill_dp19_queries_treatment ( Var_parameter_mr , Var_variable_tr ) & ( rel_medicine_reference_Treatment ( Var_variable_tr , Var_parameter_med ) & ( type_Medicine_class ( Var_parameter_med ) & ~ rel_pattern_ca_mcgill_dp19_queries_recommended ( Var_variable_hp , Var_parameter_med ) ) ) ) ) ) ) ) ) ) .

 fof ( upperMultiplicity_healthsystem_Patient , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( type_Patient_class ( Var_src ) & ( type_HealthSystem_class ( Var_trg_1 ) & type_HealthSystem_class ( Var_trg_2 ) ) ) => ( ( rel_healthsystem_reference_Patient ( Var_src , Var_trg_1 ) & rel_healthsystem_reference_Patient ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) .

diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/VampireTest/vampireProblem.tptp b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/VampireTest/vampireProblem.tptp
index a4afb86e..4c368859 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/VampireTest/vampireProblem.tptp
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/VampireTest/vampireProblem.tptp
@@ -1 +1,7 @@
-% This is an initial Test Comment fof ( typeDef_oldRPS , axiom , ! [ A ] : ( type_oldRPS ( A ) <=> ( A = "aRock" | ( A = "aPaper" | A = "aScissor" ) ) ) ) . fof ( hierarchyHandler , axiom , ! [ A ] : ( object ( A ) <=> type_oldRPS ( A ) ) ) . fof ( compliance_beats2 , axiom , ! [ Var_0 , Var_1 ] : ( rel_beats2 ( Var_0 , Var_1 ) => ( type_oldRPS ( Var_0 ) & type_oldRPS ( Var_1 ) ) ) ) . fof ( assertion1 , axiom , ! [ Var_x ] : ( type_oldRPS ( Var_x ) => ? [ Var_y ] : ( type_oldRPS ( Var_y ) & ( rel_beats2 ( Var_x , Var_y ) & ( Var_x != Var_y & ~ rel_beats2 ( Var_y , Var_x ) ) ) ) ) ) .
\ No newline at end of file
+% This is an initial Test Comment

+fof ( typeDef_oldRPS , axiom , ! [ A ] : ( t_oldRPS ( A ) <=> ( e_Rock_oldRPS ( A ) | ( e_Paper_oldRPS ( A ) | e_Scissor_oldRPS ( A ) ) ) ) ) .

+fof ( hierarchyHandler , axiom , ! [ A ] : ( object ( A ) <=> t_oldRPS ( A ) ) ) .

+fof ( typeScope , axiom , ! [ A ] : ( object ( A ) <=> ( A = o1 | ( A = o2 | ( A = o3 | A = o4 ) ) ) ) ) .

+fof ( typeUniqueness , axiom , o1 != o2 & ( o1 != o3 & ( o2 != o3 & ( o1 != o4 & ( o2 != o4 & o3 != o4 ) ) ) ) ) .

+fof ( compliance_beats2 , axiom , ! [ Var_0 , Var_1 ] : ( rel_beats2 ( Var_0 , Var_1 ) => ( t_oldRPS ( Var_0 ) & t_oldRPS ( Var_1 ) ) ) ) .

+fof ( assertion1 , axiom , ! [ Var_x ] : ( t_oldRPS ( Var_x ) => ? [ Var_y ] : ( t_oldRPS ( Var_y ) & ( rel_beats2 ( Var_x , Var_y ) & ( Var_x != Var_y & ~ rel_beats2 ( Var_y , Var_x ) ) ) ) ) ) .

diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/plugin.xml b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/plugin.xml
index 2f4febdb..38efb459 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/plugin.xml
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/plugin.xml
@@ -1 +1,7 @@
-<?xml version="1.0" encoding="UTF-8"?><plugin/>

+<?xml version="1.0" encoding="UTF-8"?><plugin>

+  <extension id="ca.mcgill.ecse.dslreasoner.vampire.queries.FamPatterns" point="org.eclipse.viatra.query.runtime.queryspecification">

+    <group group="org.eclipse.viatra.query.runtime.extensibility.SingletonExtensionFactory:ca.mcgill.ecse.dslreasoner.vampire.queries.FamPatterns" id="ca.mcgill.ecse.dslreasoner.vampire.queries.FamPatterns">

+      <query-specification fqn="ca.mcgill.ecse.dslreasoner.vampire.queries.terminatorAndInformation"/>

+    </group>

+  </extension>

+</plugin>

diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src-gen/ca/mcgill/ecse/dslreasoner/vampire/queries/.gitignore b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src-gen/ca/mcgill/ecse/dslreasoner/vampire/queries/.gitignore
new file mode 100644
index 00000000..96fc598c
--- /dev/null
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src-gen/ca/mcgill/ecse/dslreasoner/vampire/queries/.gitignore
@@ -0,0 +1,50 @@
+/.EntryInRegion_M0.java._trace
+/.EntryInRegion_M1.java._trace
+/.EntryInRegion_M2.java._trace
+/.FamPatterns.java._trace
+/.MultipleEntryInRegion_M0.java._trace
+/.MultipleEntryInRegion_M1.java._trace
+/.MultipleEntryInRegion_M2.java._trace
+/.MultipleEntryInRegion_M3.java._trace
+/.MultipleEntryInRegion_M4.java._trace
+/.MultipleEntryInRegion_M5.java._trace
+/.NoEntryInRegion_M0.java._trace
+/.NoEntryInRegion_M1.java._trace
+/.NoEntryInRegion_M2.java._trace
+/.NoEntryInRegion_M3.java._trace
+/.NoEntryInRegion_M4.java._trace
+/.NoEntryInRegion_M5.java._trace
+/.TerminatorAndInformation.java._trace
+/.Transition_M0.java._trace
+/.Transition_M1.java._trace
+/.EntryInRegion.java._trace
+/.IncomingToEntry.java._trace
+/.MultipleEntryInRegion.java._trace
+/.MultipleTransitionFromEntry.java._trace
+/.NoEntryInRegion.java._trace
+/.NoOutgoingTransitionFromEntry.java._trace
+/.NoStateInRegion.java._trace
+/.OutgoingFromExit.java._trace
+/.OutgoingFromFinal.java._trace
+/.StateInRegion.java._trace
+/.Transition.java._trace
+/.Child.java._trace
+/.ChoiceHasNoIncoming.java._trace
+/.ChoiceHasNoOutgoing.java._trace
+/.HasMultipleIncomingTrainsition.java._trace
+/.HasMultipleOutgoingTrainsition.java._trace
+/.HasMultipleRegions.java._trace
+/.NotSynchronizingStates.java._trace
+/.SynchHasNoIncoming.java._trace
+/.SynchHasNoOutgoing.java._trace
+/.SynchThree.java._trace
+/.SynchronizedIncomingInSameRegion.java._trace
+/.SynchronizedRegionDoesNotHaveMultipleRegions.java._trace
+/.SynchronizedRegionsAreNotSiblings.java._trace
+/.TwoSynch.java._trace
+/.YakinduPatterns.java._trace
+/.Transition_M2.java._trace
+/.Transition_M3.java._trace
+/.IncomingToEntry_1.java._trace
+/.IncomingToEntry_M0.java._trace
+/.Transition_M4.java._trace
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src-gen/ca/mcgill/ecse/dslreasoner/vampire/queries/FamPatterns.java b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src-gen/ca/mcgill/ecse/dslreasoner/vampire/queries/FamPatterns.java
new file mode 100644
index 00000000..cf1378da
--- /dev/null
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src-gen/ca/mcgill/ecse/dslreasoner/vampire/queries/FamPatterns.java
@@ -0,0 +1,53 @@
+/**

+ * Generated from platform:/resource/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/queries/FamPatterns.vql

+ */

+package ca.mcgill.ecse.dslreasoner.vampire.queries;

+

+import ca.mcgill.ecse.dslreasoner.vampire.queries.TerminatorAndInformation;

+import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine;

+import org.eclipse.viatra.query.runtime.api.impl.BaseGeneratedPatternGroup;

+

+/**

+ * A pattern group formed of all public patterns defined in FamPatterns.vql.

+ * 

+ * <p>Use the static instance as any {@link interface org.eclipse.viatra.query.runtime.api.IQueryGroup}, to conveniently prepare

+ * a VIATRA Query engine for matching all patterns originally defined in file FamPatterns.vql,

+ * in order to achieve better performance than one-by-one on-demand matcher initialization.

+ * 

+ * <p> From package ca.mcgill.ecse.dslreasoner.vampire.queries, the group contains the definition of the following patterns: <ul>

+ * <li>terminatorAndInformation</li>

+ * </ul>

+ * 

+ * @see IQueryGroup

+ * 

+ */

+@SuppressWarnings("all")

+public final class FamPatterns extends BaseGeneratedPatternGroup {

+  /**

+   * Access the pattern group.

+   * 

+   * @return the singleton instance of the group

+   * @throws ViatraQueryRuntimeException if there was an error loading the generated code of pattern specifications

+   * 

+   */

+  public static FamPatterns instance() {

+    if (INSTANCE == null) {

+        INSTANCE = new FamPatterns();

+    }

+    return INSTANCE;

+  }

+  

+  private static FamPatterns INSTANCE;

+  

+  private FamPatterns() {

+    querySpecifications.add(TerminatorAndInformation.instance());

+  }

+  

+  public TerminatorAndInformation getTerminatorAndInformation() {

+    return TerminatorAndInformation.instance();

+  }

+  

+  public TerminatorAndInformation.Matcher getTerminatorAndInformation(final ViatraQueryEngine engine) {

+    return TerminatorAndInformation.Matcher.on(engine);

+  }

+}

diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src-gen/ca/mcgill/ecse/dslreasoner/vampire/queries/TerminatorAndInformation.java b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src-gen/ca/mcgill/ecse/dslreasoner/vampire/queries/TerminatorAndInformation.java
new file mode 100644
index 00000000..cb0708ad
--- /dev/null
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src-gen/ca/mcgill/ecse/dslreasoner/vampire/queries/TerminatorAndInformation.java
@@ -0,0 +1,747 @@
+/**

+ * Generated from platform:/resource/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/queries/FamPatterns.vql

+ */

+package ca.mcgill.ecse.dslreasoner.vampire.queries;

+

+import functionalarchitecture.FAMTerminator;

+import functionalarchitecture.InformationLink;

+import java.util.Arrays;

+import java.util.Collection;

+import java.util.LinkedHashSet;

+import java.util.List;

+import java.util.Objects;

+import java.util.Optional;

+import java.util.Set;

+import java.util.function.Consumer;

+import java.util.stream.Collectors;

+import java.util.stream.Stream;

+import org.apache.log4j.Logger;

+import org.eclipse.emf.ecore.EClass;

+import org.eclipse.viatra.query.runtime.api.IPatternMatch;

+import org.eclipse.viatra.query.runtime.api.IQuerySpecification;

+import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine;

+import org.eclipse.viatra.query.runtime.api.impl.BaseGeneratedEMFPQuery;

+import org.eclipse.viatra.query.runtime.api.impl.BaseGeneratedEMFQuerySpecification;

+import org.eclipse.viatra.query.runtime.api.impl.BaseMatcher;

+import org.eclipse.viatra.query.runtime.api.impl.BasePatternMatch;

+import org.eclipse.viatra.query.runtime.emf.types.EClassTransitiveInstancesKey;

+import org.eclipse.viatra.query.runtime.emf.types.EStructuralFeatureInstancesKey;

+import org.eclipse.viatra.query.runtime.matchers.backend.QueryEvaluationHint;

+import org.eclipse.viatra.query.runtime.matchers.psystem.PBody;

+import org.eclipse.viatra.query.runtime.matchers.psystem.PVariable;

+import org.eclipse.viatra.query.runtime.matchers.psystem.annotations.PAnnotation;

+import org.eclipse.viatra.query.runtime.matchers.psystem.annotations.ParameterReference;

+import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.Equality;

+import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.ExportedParameter;

+import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.TypeConstraint;

+import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PParameter;

+import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PParameterDirection;

+import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PVisibility;

+import org.eclipse.viatra.query.runtime.matchers.tuple.Tuple;

+import org.eclipse.viatra.query.runtime.matchers.tuple.Tuples;

+import org.eclipse.viatra.query.runtime.util.ViatraQueryLoggingUtil;

+

+/**

+ * A pattern-specific query specification that can instantiate Matcher in a type-safe way.

+ * 

+ * <p>Original source:

+ *         <code><pre>

+ *         {@literal @}Constraint(message="terminatorAndInformation", severity="error", key={T})

+ *         pattern terminatorAndInformation(T : FAMTerminator, I : InformationLink) = {

+ *              FunctionalOutput.outgoingLinks(Out,I);

+ *              FunctionalOutput.terminator(Out,T); 

+ *         } or {

+ *              InformationLink.to(I,In);

+ *              FunctionalInput.terminator(In,T);

+ *         }

+ * </pre></code>

+ * 

+ * @see Matcher

+ * @see Match

+ * 

+ */

+@SuppressWarnings("all")

+public final class TerminatorAndInformation extends BaseGeneratedEMFQuerySpecification<TerminatorAndInformation.Matcher> {

+  /**

+   * Pattern-specific match representation of the ca.mcgill.ecse.dslreasoner.vampire.queries.terminatorAndInformation pattern,

+   * to be used in conjunction with {@link Matcher}.

+   * 

+   * <p>Class fields correspond to parameters of the pattern. Fields with value null are considered unassigned.

+   * Each instance is a (possibly partial) substitution of pattern parameters,

+   * usable to represent a match of the pattern in the result of a query,

+   * or to specify the bound (fixed) input parameters when issuing a query.

+   * 

+   * @see Matcher

+   * 

+   */

+  public static abstract class Match extends BasePatternMatch {

+    private FAMTerminator fT;

+    

+    private InformationLink fI;

+    

+    private static List<String> parameterNames = makeImmutableList("T", "I");

+    

+    private Match(final FAMTerminator pT, final InformationLink pI) {

+      this.fT = pT;

+      this.fI = pI;

+    }

+    

+    @Override

+    public Object get(final String parameterName) {

+      if ("T".equals(parameterName)) return this.fT;

+      if ("I".equals(parameterName)) return this.fI;

+      return null;

+    }

+    

+    public FAMTerminator getT() {

+      return this.fT;

+    }

+    

+    public InformationLink getI() {

+      return this.fI;

+    }

+    

+    @Override

+    public boolean set(final String parameterName, final Object newValue) {

+      if (!isMutable()) throw new java.lang.UnsupportedOperationException();

+      if ("T".equals(parameterName) ) {

+          this.fT = (FAMTerminator) newValue;

+          return true;

+      }

+      if ("I".equals(parameterName) ) {

+          this.fI = (InformationLink) newValue;

+          return true;

+      }

+      return false;

+    }

+    

+    public void setT(final FAMTerminator pT) {

+      if (!isMutable()) throw new java.lang.UnsupportedOperationException();

+      this.fT = pT;

+    }

+    

+    public void setI(final InformationLink pI) {

+      if (!isMutable()) throw new java.lang.UnsupportedOperationException();

+      this.fI = pI;

+    }

+    

+    @Override

+    public String patternName() {

+      return "ca.mcgill.ecse.dslreasoner.vampire.queries.terminatorAndInformation";

+    }

+    

+    @Override

+    public List<String> parameterNames() {

+      return TerminatorAndInformation.Match.parameterNames;

+    }

+    

+    @Override

+    public Object[] toArray() {

+      return new Object[]{fT, fI};

+    }

+    

+    @Override

+    public TerminatorAndInformation.Match toImmutable() {

+      return isMutable() ? newMatch(fT, fI) : this;

+    }

+    

+    @Override

+    public String prettyPrint() {

+      StringBuilder result = new StringBuilder();

+      result.append("\"T\"=" + prettyPrintValue(fT) + ", ");

+      result.append("\"I\"=" + prettyPrintValue(fI));

+      return result.toString();

+    }

+    

+    @Override

+    public int hashCode() {

+      return Objects.hash(fT, fI);

+    }

+    

+    @Override

+    public boolean equals(final Object obj) {

+      if (this == obj)

+          return true;

+      if (obj == null) {

+          return false;

+      }

+      if ((obj instanceof TerminatorAndInformation.Match)) {

+          TerminatorAndInformation.Match other = (TerminatorAndInformation.Match) obj;

+          return Objects.equals(fT, other.fT) && Objects.equals(fI, other.fI);

+      } else {

+          // this should be infrequent

+          if (!(obj instanceof IPatternMatch)) {

+              return false;

+          }

+          IPatternMatch otherSig  = (IPatternMatch) obj;

+          return Objects.equals(specification(), otherSig.specification()) && Arrays.deepEquals(toArray(), otherSig.toArray());

+      }

+    }

+    

+    @Override

+    public TerminatorAndInformation specification() {

+      return TerminatorAndInformation.instance();

+    }

+    

+    /**

+     * Returns an empty, mutable match.

+     * Fields of the mutable match can be filled to create a partial match, usable as matcher input.

+     * 

+     * @return the empty match.

+     * 

+     */

+    public static TerminatorAndInformation.Match newEmptyMatch() {

+      return new Mutable(null, null);

+    }

+    

+    /**

+     * Returns a mutable (partial) match.

+     * Fields of the mutable match can be filled to create a partial match, usable as matcher input.

+     * 

+     * @param pT the fixed value of pattern parameter T, or null if not bound.

+     * @param pI the fixed value of pattern parameter I, or null if not bound.

+     * @return the new, mutable (partial) match object.

+     * 

+     */

+    public static TerminatorAndInformation.Match newMutableMatch(final FAMTerminator pT, final InformationLink pI) {

+      return new Mutable(pT, pI);

+    }

+    

+    /**

+     * Returns a new (partial) match.

+     * This can be used e.g. to call the matcher with a partial match.

+     * <p>The returned match will be immutable. Use {@link #newEmptyMatch()} to obtain a mutable match object.

+     * @param pT the fixed value of pattern parameter T, or null if not bound.

+     * @param pI the fixed value of pattern parameter I, or null if not bound.

+     * @return the (partial) match object.

+     * 

+     */

+    public static TerminatorAndInformation.Match newMatch(final FAMTerminator pT, final InformationLink pI) {

+      return new Immutable(pT, pI);

+    }

+    

+    private static final class Mutable extends TerminatorAndInformation.Match {

+      Mutable(final FAMTerminator pT, final InformationLink pI) {

+        super(pT, pI);

+      }

+      

+      @Override

+      public boolean isMutable() {

+        return true;

+      }

+    }

+    

+    private static final class Immutable extends TerminatorAndInformation.Match {

+      Immutable(final FAMTerminator pT, final InformationLink pI) {

+        super(pT, pI);

+      }

+      

+      @Override

+      public boolean isMutable() {

+        return false;

+      }

+    }

+  }

+  

+  /**

+   * Generated pattern matcher API of the ca.mcgill.ecse.dslreasoner.vampire.queries.terminatorAndInformation pattern,

+   * providing pattern-specific query methods.

+   * 

+   * <p>Use the pattern matcher on a given model via {@link #on(ViatraQueryEngine)},

+   * e.g. in conjunction with {@link ViatraQueryEngine#on(QueryScope)}.

+   * 

+   * <p>Matches of the pattern will be represented as {@link Match}.

+   * 

+   * <p>Original source:

+   * <code><pre>

+   * {@literal @}Constraint(message="terminatorAndInformation", severity="error", key={T})

+   * pattern terminatorAndInformation(T : FAMTerminator, I : InformationLink) = {

+   *    FunctionalOutput.outgoingLinks(Out,I);

+   *    FunctionalOutput.terminator(Out,T); 

+   * } or {

+   *    InformationLink.to(I,In);

+   *    FunctionalInput.terminator(In,T);

+   * }

+   * </pre></code>

+   * 

+   * @see Match

+   * @see TerminatorAndInformation

+   * 

+   */

+  public static class Matcher extends BaseMatcher<TerminatorAndInformation.Match> {

+    /**

+     * Initializes the pattern matcher within an existing VIATRA Query engine.

+     * If the pattern matcher is already constructed in the engine, only a light-weight reference is returned.

+     * 

+     * @param engine the existing VIATRA Query engine in which this matcher will be created.

+     * @throws ViatraQueryRuntimeException if an error occurs during pattern matcher creation

+     * 

+     */

+    public static TerminatorAndInformation.Matcher on(final ViatraQueryEngine engine) {

+      // check if matcher already exists

+      Matcher matcher = engine.getExistingMatcher(querySpecification());

+      if (matcher == null) {

+          matcher = (Matcher)engine.getMatcher(querySpecification());

+      }

+      return matcher;

+    }

+    

+    /**

+     * @throws ViatraQueryRuntimeException if an error occurs during pattern matcher creation

+     * @return an initialized matcher

+     * @noreference This method is for internal matcher initialization by the framework, do not call it manually.

+     * 

+     */

+    public static TerminatorAndInformation.Matcher create() {

+      return new Matcher();

+    }

+    

+    private final static int POSITION_T = 0;

+    

+    private final static int POSITION_I = 1;

+    

+    private final static Logger LOGGER = ViatraQueryLoggingUtil.getLogger(TerminatorAndInformation.Matcher.class);

+    

+    /**

+     * Initializes the pattern matcher within an existing VIATRA Query engine.

+     * If the pattern matcher is already constructed in the engine, only a light-weight reference is returned.

+     * 

+     * @param engine the existing VIATRA Query engine in which this matcher will be created.

+     * @throws ViatraQueryRuntimeException if an error occurs during pattern matcher creation

+     * 

+     */

+    private Matcher() {

+      super(querySpecification());

+    }

+    

+    /**

+     * Returns the set of all matches of the pattern that conform to the given fixed values of some parameters.

+     * @param pT the fixed value of pattern parameter T, or null if not bound.

+     * @param pI the fixed value of pattern parameter I, or null if not bound.

+     * @return matches represented as a Match object.

+     * 

+     */

+    public Collection<TerminatorAndInformation.Match> getAllMatches(final FAMTerminator pT, final InformationLink pI) {

+      return rawStreamAllMatches(new Object[]{pT, pI}).collect(Collectors.toSet());

+    }

+    

+    /**

+     * Returns a stream of all matches of the pattern that conform to the given fixed values of some parameters.

+     * </p>

+     * <strong>NOTE</strong>: It is important not to modify the source model while the stream is being processed.

+     * If the match set of the pattern changes during processing, the contents of the stream is <strong>undefined</strong>.

+     * In such cases, either rely on {@link #getAllMatches()} or collect the results of the stream in end-user code.

+     * @param pT the fixed value of pattern parameter T, or null if not bound.

+     * @param pI the fixed value of pattern parameter I, or null if not bound.

+     * @return a stream of matches represented as a Match object.

+     * 

+     */

+    public Stream<TerminatorAndInformation.Match> streamAllMatches(final FAMTerminator pT, final InformationLink pI) {

+      return rawStreamAllMatches(new Object[]{pT, pI});

+    }

+    

+    /**

+     * Returns an arbitrarily chosen match of the pattern that conforms to the given fixed values of some parameters.

+     * Neither determinism nor randomness of selection is guaranteed.

+     * @param pT the fixed value of pattern parameter T, or null if not bound.

+     * @param pI the fixed value of pattern parameter I, or null if not bound.

+     * @return a match represented as a Match object, or null if no match is found.

+     * 

+     */

+    public Optional<TerminatorAndInformation.Match> getOneArbitraryMatch(final FAMTerminator pT, final InformationLink pI) {

+      return rawGetOneArbitraryMatch(new Object[]{pT, pI});

+    }

+    

+    /**

+     * Indicates whether the given combination of specified pattern parameters constitute a valid pattern match,

+     * under any possible substitution of the unspecified parameters (if any).

+     * @param pT the fixed value of pattern parameter T, or null if not bound.

+     * @param pI the fixed value of pattern parameter I, or null if not bound.

+     * @return true if the input is a valid (partial) match of the pattern.

+     * 

+     */

+    public boolean hasMatch(final FAMTerminator pT, final InformationLink pI) {

+      return rawHasMatch(new Object[]{pT, pI});

+    }

+    

+    /**

+     * Returns the number of all matches of the pattern that conform to the given fixed values of some parameters.

+     * @param pT the fixed value of pattern parameter T, or null if not bound.

+     * @param pI the fixed value of pattern parameter I, or null if not bound.

+     * @return the number of pattern matches found.

+     * 

+     */

+    public int countMatches(final FAMTerminator pT, final InformationLink pI) {

+      return rawCountMatches(new Object[]{pT, pI});

+    }

+    

+    /**

+     * Executes the given processor on an arbitrarily chosen match of the pattern that conforms to the given fixed values of some parameters.

+     * Neither determinism nor randomness of selection is guaranteed.

+     * @param pT the fixed value of pattern parameter T, or null if not bound.

+     * @param pI the fixed value of pattern parameter I, or null if not bound.

+     * @param processor the action that will process the selected match.

+     * @return true if the pattern has at least one match with the given parameter values, false if the processor was not invoked

+     * 

+     */

+    public boolean forOneArbitraryMatch(final FAMTerminator pT, final InformationLink pI, final Consumer<? super TerminatorAndInformation.Match> processor) {

+      return rawForOneArbitraryMatch(new Object[]{pT, pI}, processor);

+    }

+    

+    /**

+     * Returns a new (partial) match.

+     * This can be used e.g. to call the matcher with a partial match.

+     * <p>The returned match will be immutable. Use {@link #newEmptyMatch()} to obtain a mutable match object.

+     * @param pT the fixed value of pattern parameter T, or null if not bound.

+     * @param pI the fixed value of pattern parameter I, or null if not bound.

+     * @return the (partial) match object.

+     * 

+     */

+    public TerminatorAndInformation.Match newMatch(final FAMTerminator pT, final InformationLink pI) {

+      return TerminatorAndInformation.Match.newMatch(pT, pI);

+    }

+    

+    /**

+     * Retrieve the set of values that occur in matches for T.

+     * @return the Set of all values or empty set if there are no matches

+     * 

+     */

+    protected Stream<FAMTerminator> rawStreamAllValuesOfT(final Object[] parameters) {

+      return rawStreamAllValues(POSITION_T, parameters).map(FAMTerminator.class::cast);

+    }

+    

+    /**

+     * Retrieve the set of values that occur in matches for T.

+     * @return the Set of all values or empty set if there are no matches

+     * 

+     */

+    public Set<FAMTerminator> getAllValuesOfT() {

+      return rawStreamAllValuesOfT(emptyArray()).collect(Collectors.toSet());

+    }

+    

+    /**

+     * Retrieve the set of values that occur in matches for T.

+     * @return the Set of all values or empty set if there are no matches

+     * 

+     */

+    public Stream<FAMTerminator> streamAllValuesOfT() {

+      return rawStreamAllValuesOfT(emptyArray());

+    }

+    

+    /**

+     * Retrieve the set of values that occur in matches for T.

+     * </p>

+     * <strong>NOTE</strong>: It is important not to modify the source model while the stream is being processed.

+     * If the match set of the pattern changes during processing, the contents of the stream is <strong>undefined</strong>.

+     * In such cases, either rely on {@link #getAllMatches()} or collect the results of the stream in end-user code.

+     *      

+     * @return the Stream of all values or empty set if there are no matches

+     * 

+     */

+    public Stream<FAMTerminator> streamAllValuesOfT(final TerminatorAndInformation.Match partialMatch) {

+      return rawStreamAllValuesOfT(partialMatch.toArray());

+    }

+    

+    /**

+     * Retrieve the set of values that occur in matches for T.

+     * </p>

+     * <strong>NOTE</strong>: It is important not to modify the source model while the stream is being processed.

+     * If the match set of the pattern changes during processing, the contents of the stream is <strong>undefined</strong>.

+     * In such cases, either rely on {@link #getAllMatches()} or collect the results of the stream in end-user code.

+     *      

+     * @return the Stream of all values or empty set if there are no matches

+     * 

+     */

+    public Stream<FAMTerminator> streamAllValuesOfT(final InformationLink pI) {

+      return rawStreamAllValuesOfT(new Object[]{null, pI});

+    }

+    

+    /**

+     * Retrieve the set of values that occur in matches for T.

+     * @return the Set of all values or empty set if there are no matches

+     * 

+     */

+    public Set<FAMTerminator> getAllValuesOfT(final TerminatorAndInformation.Match partialMatch) {

+      return rawStreamAllValuesOfT(partialMatch.toArray()).collect(Collectors.toSet());

+    }

+    

+    /**

+     * Retrieve the set of values that occur in matches for T.

+     * @return the Set of all values or empty set if there are no matches

+     * 

+     */

+    public Set<FAMTerminator> getAllValuesOfT(final InformationLink pI) {

+      return rawStreamAllValuesOfT(new Object[]{null, pI}).collect(Collectors.toSet());

+    }

+    

+    /**

+     * Retrieve the set of values that occur in matches for I.

+     * @return the Set of all values or empty set if there are no matches

+     * 

+     */

+    protected Stream<InformationLink> rawStreamAllValuesOfI(final Object[] parameters) {

+      return rawStreamAllValues(POSITION_I, parameters).map(InformationLink.class::cast);

+    }

+    

+    /**

+     * Retrieve the set of values that occur in matches for I.

+     * @return the Set of all values or empty set if there are no matches

+     * 

+     */

+    public Set<InformationLink> getAllValuesOfI() {

+      return rawStreamAllValuesOfI(emptyArray()).collect(Collectors.toSet());

+    }

+    

+    /**

+     * Retrieve the set of values that occur in matches for I.

+     * @return the Set of all values or empty set if there are no matches

+     * 

+     */

+    public Stream<InformationLink> streamAllValuesOfI() {

+      return rawStreamAllValuesOfI(emptyArray());

+    }

+    

+    /**

+     * Retrieve the set of values that occur in matches for I.

+     * </p>

+     * <strong>NOTE</strong>: It is important not to modify the source model while the stream is being processed.

+     * If the match set of the pattern changes during processing, the contents of the stream is <strong>undefined</strong>.

+     * In such cases, either rely on {@link #getAllMatches()} or collect the results of the stream in end-user code.

+     *      

+     * @return the Stream of all values or empty set if there are no matches

+     * 

+     */

+    public Stream<InformationLink> streamAllValuesOfI(final TerminatorAndInformation.Match partialMatch) {

+      return rawStreamAllValuesOfI(partialMatch.toArray());

+    }

+    

+    /**

+     * Retrieve the set of values that occur in matches for I.

+     * </p>

+     * <strong>NOTE</strong>: It is important not to modify the source model while the stream is being processed.

+     * If the match set of the pattern changes during processing, the contents of the stream is <strong>undefined</strong>.

+     * In such cases, either rely on {@link #getAllMatches()} or collect the results of the stream in end-user code.

+     *      

+     * @return the Stream of all values or empty set if there are no matches

+     * 

+     */

+    public Stream<InformationLink> streamAllValuesOfI(final FAMTerminator pT) {

+      return rawStreamAllValuesOfI(new Object[]{pT, null});

+    }

+    

+    /**

+     * Retrieve the set of values that occur in matches for I.

+     * @return the Set of all values or empty set if there are no matches

+     * 

+     */

+    public Set<InformationLink> getAllValuesOfI(final TerminatorAndInformation.Match partialMatch) {

+      return rawStreamAllValuesOfI(partialMatch.toArray()).collect(Collectors.toSet());

+    }

+    

+    /**

+     * Retrieve the set of values that occur in matches for I.

+     * @return the Set of all values or empty set if there are no matches

+     * 

+     */

+    public Set<InformationLink> getAllValuesOfI(final FAMTerminator pT) {

+      return rawStreamAllValuesOfI(new Object[]{pT, null}).collect(Collectors.toSet());

+    }

+    

+    @Override

+    protected TerminatorAndInformation.Match tupleToMatch(final Tuple t) {

+      try {

+          return TerminatorAndInformation.Match.newMatch((FAMTerminator) t.get(POSITION_T), (InformationLink) t.get(POSITION_I));

+      } catch(ClassCastException e) {

+          LOGGER.error("Element(s) in tuple not properly typed!",e);

+          return null;

+      }

+    }

+    

+    @Override

+    protected TerminatorAndInformation.Match arrayToMatch(final Object[] match) {

+      try {

+          return TerminatorAndInformation.Match.newMatch((FAMTerminator) match[POSITION_T], (InformationLink) match[POSITION_I]);

+      } catch(ClassCastException e) {

+          LOGGER.error("Element(s) in array not properly typed!",e);

+          return null;

+      }

+    }

+    

+    @Override

+    protected TerminatorAndInformation.Match arrayToMatchMutable(final Object[] match) {

+      try {

+          return TerminatorAndInformation.Match.newMutableMatch((FAMTerminator) match[POSITION_T], (InformationLink) match[POSITION_I]);

+      } catch(ClassCastException e) {

+          LOGGER.error("Element(s) in array not properly typed!",e);

+          return null;

+      }

+    }

+    

+    /**

+     * @return the singleton instance of the query specification of this pattern

+     * @throws ViatraQueryRuntimeException if the pattern definition could not be loaded

+     * 

+     */

+    public static IQuerySpecification<TerminatorAndInformation.Matcher> querySpecification() {

+      return TerminatorAndInformation.instance();

+    }

+  }

+  

+  private TerminatorAndInformation() {

+    super(GeneratedPQuery.INSTANCE);

+  }

+  

+  /**

+   * @return the singleton instance of the query specification

+   * @throws ViatraQueryRuntimeException if the pattern definition could not be loaded

+   * 

+   */

+  public static TerminatorAndInformation instance() {

+    try{

+        return LazyHolder.INSTANCE;

+    } catch (ExceptionInInitializerError err) {

+        throw processInitializerError(err);

+    }

+  }

+  

+  @Override

+  protected TerminatorAndInformation.Matcher instantiate(final ViatraQueryEngine engine) {

+    return TerminatorAndInformation.Matcher.on(engine);

+  }

+  

+  @Override

+  public TerminatorAndInformation.Matcher instantiate() {

+    return TerminatorAndInformation.Matcher.create();

+  }

+  

+  @Override

+  public TerminatorAndInformation.Match newEmptyMatch() {

+    return TerminatorAndInformation.Match.newEmptyMatch();

+  }

+  

+  @Override

+  public TerminatorAndInformation.Match newMatch(final Object... parameters) {

+    return TerminatorAndInformation.Match.newMatch((functionalarchitecture.FAMTerminator) parameters[0], (functionalarchitecture.InformationLink) parameters[1]);

+  }

+  

+  /**

+   * Inner class allowing the singleton instance of {@link JvmGenericType: ca.mcgill.ecse.dslreasoner.vampire.queries.TerminatorAndInformation (visibility: PUBLIC, simpleName: TerminatorAndInformation, identifier: ca.mcgill.ecse.dslreasoner.vampire.queries.TerminatorAndInformation, deprecated: <unset>) (abstract: false, static: false, final: true, packageName: ca.mcgill.ecse.dslreasoner.vampire.queries) (interface: false, strictFloatingPoint: false, anonymous: false)} to be created 

+   *     <b>not</b> at the class load time of the outer class, 

+   *     but rather at the first call to {@link JvmGenericType: ca.mcgill.ecse.dslreasoner.vampire.queries.TerminatorAndInformation (visibility: PUBLIC, simpleName: TerminatorAndInformation, identifier: ca.mcgill.ecse.dslreasoner.vampire.queries.TerminatorAndInformation, deprecated: <unset>) (abstract: false, static: false, final: true, packageName: ca.mcgill.ecse.dslreasoner.vampire.queries) (interface: false, strictFloatingPoint: false, anonymous: false)#instance()}.

+   * 

+   * <p> This workaround is required e.g. to support recursion.

+   * 

+   */

+  private static class LazyHolder {

+    private final static TerminatorAndInformation INSTANCE = new TerminatorAndInformation();

+    

+    /**

+     * Statically initializes the query specification <b>after</b> the field {@link #INSTANCE} is assigned.

+     * This initialization order is required to support indirect recursion.

+     * 

+     * <p> The static initializer is defined using a helper field to work around limitations of the code generator.

+     * 

+     */

+    private final static Object STATIC_INITIALIZER = ensureInitialized();

+    

+    public static Object ensureInitialized() {

+      INSTANCE.ensureInitializedInternal();

+      return null;

+    }

+  }

+  

+  private static class GeneratedPQuery extends BaseGeneratedEMFPQuery {

+    private final static TerminatorAndInformation.GeneratedPQuery INSTANCE = new GeneratedPQuery();

+    

+    private final PParameter parameter_T = new PParameter("T", "functionalarchitecture.FAMTerminator", new EClassTransitiveInstancesKey((EClass)getClassifierLiteralSafe("http://www.inf.mit.bme.hu/viatrasolver/example/fam", "FAMTerminator")), PParameterDirection.INOUT);

+    

+    private final PParameter parameter_I = new PParameter("I", "functionalarchitecture.InformationLink", new EClassTransitiveInstancesKey((EClass)getClassifierLiteralSafe("http://www.inf.mit.bme.hu/viatrasolver/example/fam", "InformationLink")), PParameterDirection.INOUT);

+    

+    private final List<PParameter> parameters = Arrays.asList(parameter_T, parameter_I);

+    

+    private GeneratedPQuery() {

+      super(PVisibility.PUBLIC);

+    }

+    

+    @Override

+    public String getFullyQualifiedName() {

+      return "ca.mcgill.ecse.dslreasoner.vampire.queries.terminatorAndInformation";

+    }

+    

+    @Override

+    public List<String> getParameterNames() {

+      return Arrays.asList("T","I");

+    }

+    

+    @Override

+    public List<PParameter> getParameters() {

+      return parameters;

+    }

+    

+    @Override

+    public Set<PBody> doGetContainedBodies() {

+      setEvaluationHints(new QueryEvaluationHint(null, QueryEvaluationHint.BackendRequirement.UNSPECIFIED));

+      Set<PBody> bodies = new LinkedHashSet<>();

+      {

+          PBody body = new PBody(this);

+          PVariable var_T = body.getOrCreateVariableByName("T");

+          PVariable var_I = body.getOrCreateVariableByName("I");

+          PVariable var_Out = body.getOrCreateVariableByName("Out");

+          new TypeConstraint(body, Tuples.flatTupleOf(var_T), new EClassTransitiveInstancesKey((EClass)getClassifierLiteral("http://www.inf.mit.bme.hu/viatrasolver/example/fam", "FAMTerminator")));

+          new TypeConstraint(body, Tuples.flatTupleOf(var_I), new EClassTransitiveInstancesKey((EClass)getClassifierLiteral("http://www.inf.mit.bme.hu/viatrasolver/example/fam", "InformationLink")));

+          body.setSymbolicParameters(Arrays.<ExportedParameter>asList(

+             new ExportedParameter(body, var_T, parameter_T),

+             new ExportedParameter(body, var_I, parameter_I)

+          ));

+          //    FunctionalOutput.outgoingLinks(Out,I)

+          new TypeConstraint(body, Tuples.flatTupleOf(var_Out), new EClassTransitiveInstancesKey((EClass)getClassifierLiteral("http://www.inf.mit.bme.hu/viatrasolver/example/fam", "FunctionalOutput")));

+          PVariable var__virtual_0_ = body.getOrCreateVariableByName(".virtual{0}");

+          new TypeConstraint(body, Tuples.flatTupleOf(var_Out, var__virtual_0_), new EStructuralFeatureInstancesKey(getFeatureLiteral("http://www.inf.mit.bme.hu/viatrasolver/example/fam", "FunctionalOutput", "outgoingLinks")));

+          new TypeConstraint(body, Tuples.flatTupleOf(var__virtual_0_), new EClassTransitiveInstancesKey((EClass)getClassifierLiteral("http://www.inf.mit.bme.hu/viatrasolver/example/fam", "InformationLink")));

+          new Equality(body, var__virtual_0_, var_I);

+          //    FunctionalOutput.terminator(Out,T)

+          new TypeConstraint(body, Tuples.flatTupleOf(var_Out), new EClassTransitiveInstancesKey((EClass)getClassifierLiteral("http://www.inf.mit.bme.hu/viatrasolver/example/fam", "FunctionalOutput")));

+          PVariable var__virtual_1_ = body.getOrCreateVariableByName(".virtual{1}");

+          new TypeConstraint(body, Tuples.flatTupleOf(var_Out, var__virtual_1_), new EStructuralFeatureInstancesKey(getFeatureLiteral("http://www.inf.mit.bme.hu/viatrasolver/example/fam", "FunctionalData", "terminator")));

+          new TypeConstraint(body, Tuples.flatTupleOf(var__virtual_1_), new EClassTransitiveInstancesKey((EClass)getClassifierLiteral("http://www.inf.mit.bme.hu/viatrasolver/example/fam", "FAMTerminator")));

+          new Equality(body, var__virtual_1_, var_T);

+          bodies.add(body);

+      }

+      {

+          PBody body = new PBody(this);

+          PVariable var_T = body.getOrCreateVariableByName("T");

+          PVariable var_I = body.getOrCreateVariableByName("I");

+          PVariable var_In = body.getOrCreateVariableByName("In");

+          new TypeConstraint(body, Tuples.flatTupleOf(var_T), new EClassTransitiveInstancesKey((EClass)getClassifierLiteral("http://www.inf.mit.bme.hu/viatrasolver/example/fam", "FAMTerminator")));

+          new TypeConstraint(body, Tuples.flatTupleOf(var_I), new EClassTransitiveInstancesKey((EClass)getClassifierLiteral("http://www.inf.mit.bme.hu/viatrasolver/example/fam", "InformationLink")));

+          body.setSymbolicParameters(Arrays.<ExportedParameter>asList(

+             new ExportedParameter(body, var_T, parameter_T),

+             new ExportedParameter(body, var_I, parameter_I)

+          ));

+          //    InformationLink.to(I,In)

+          new TypeConstraint(body, Tuples.flatTupleOf(var_I), new EClassTransitiveInstancesKey((EClass)getClassifierLiteral("http://www.inf.mit.bme.hu/viatrasolver/example/fam", "InformationLink")));

+          PVariable var__virtual_0_ = body.getOrCreateVariableByName(".virtual{0}");

+          new TypeConstraint(body, Tuples.flatTupleOf(var_I, var__virtual_0_), new EStructuralFeatureInstancesKey(getFeatureLiteral("http://www.inf.mit.bme.hu/viatrasolver/example/fam", "InformationLink", "to")));

+          new TypeConstraint(body, Tuples.flatTupleOf(var__virtual_0_), new EClassTransitiveInstancesKey((EClass)getClassifierLiteral("http://www.inf.mit.bme.hu/viatrasolver/example/fam", "FunctionalInput")));

+          new Equality(body, var__virtual_0_, var_In);

+          //    FunctionalInput.terminator(In,T)

+          new TypeConstraint(body, Tuples.flatTupleOf(var_In), new EClassTransitiveInstancesKey((EClass)getClassifierLiteral("http://www.inf.mit.bme.hu/viatrasolver/example/fam", "FunctionalInput")));

+          PVariable var__virtual_1_ = body.getOrCreateVariableByName(".virtual{1}");

+          new TypeConstraint(body, Tuples.flatTupleOf(var_In, var__virtual_1_), new EStructuralFeatureInstancesKey(getFeatureLiteral("http://www.inf.mit.bme.hu/viatrasolver/example/fam", "FunctionalData", "terminator")));

+          new TypeConstraint(body, Tuples.flatTupleOf(var__virtual_1_), new EClassTransitiveInstancesKey((EClass)getClassifierLiteral("http://www.inf.mit.bme.hu/viatrasolver/example/fam", "FAMTerminator")));

+          new Equality(body, var__virtual_1_, var_T);

+          bodies.add(body);

+      }

+      {

+          PAnnotation annotation = new PAnnotation("Constraint");

+          annotation.addAttribute("message", "terminatorAndInformation");

+          annotation.addAttribute("severity", "error");

+          annotation.addAttribute("key", Arrays.asList(new Object[] {

+                              new ParameterReference("T")

+                              }));

+          addAnnotation(annotation);

+      }

+      return bodies;

+    }

+  }

+}

diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/EcoreTest.xtend b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/EcoreTest.xtend
index 54114189..18b3badd 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/EcoreTest.xtend
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/EcoreTest.xtend
@@ -6,6 +6,7 @@ import functionalarchitecture.FunctionalarchitecturePackage
 import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic

 import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration

 import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor

+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.logicresult.LogicResult

 import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore

@@ -22,9 +23,6 @@ import org.eclipse.emf.ecore.EObject
 import org.eclipse.emf.ecore.EReference

 import org.eclipse.emf.ecore.resource.Resource

 import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl

-import hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.Patterns

-import java.util.LinkedHashMap

-import hu.bme.mit.inf.dslreasoner.viatra2logic.ViatraQuerySetDescriptor

 

 class EcoreTest {

         def static void main(String[] args) {

@@ -62,7 +60,7 @@ class EcoreTest {
                 reasoner = new VampireSolver

                 val vampireConfig = new VampireSolverConfiguration => [

                         //add configuration things, in config file first

-                        it.writeToFile = true

+                        it.documentationLevel = DocumentationLevel::FULL

                 ]

                 

                 solution = reasoner.solve(logicProblem, vampireConfig,  workspace)

diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.xtend b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.xtend
index 9ae00f8d..95bfd87a 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.xtend
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.xtend
@@ -1,8 +1,10 @@
 package ca.mcgill.ecse.dslreasoner.vampire.icse

 

+import ca.mcgill.ecse.dslreasoner.vampire.queries.FamPatterns

 import functionalarchitecture.FunctionalarchitecturePackage

-import hu.bme.mit.inf.dslreasoner.domains.transima.fam.FamPatterns

 import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace

+import java.util.LinkedList

+import org.eclipse.emf.ecore.EObject

 import org.eclipse.emf.ecore.resource.Resource

 import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl

 

@@ -21,12 +23,12 @@ class FAMTest {
                 println("Input and output workspaces are created")

 

                 val metamodel = GeneralTest.loadMetamodel(FunctionalarchitecturePackage.eINSTANCE)

-                val partialModel = GeneralTest.loadPartialModel(inputs, "FunctionalArchitectureModel.xmi")

+                val partialModel = GeneralTest.loadPartialModel(inputs, "FunctionalArchitectureModel2.xmi")

                 val queries = GeneralTest.loadQueries(metamodel, FamPatterns.instance)

 

                 println("DSL loaded")

                 

-                GeneralTest.createAndSolveProblem(metamodel, partialModel, queries, workspace)  

+                GeneralTest.createAndSolveProblem(metamodel, new LinkedList<EObject>, queries, workspace)       

         }

         

         

diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.xtend b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.xtend
index 2c53d181..8a60f486 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.xtend
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.xtend
@@ -26,56 +26,74 @@ import org.eclipse.emf.ecore.EReference
 import org.eclipse.emf.ecore.resource.Resource

 import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl

 import org.eclipse.viatra.query.runtime.api.IQueryGroup

+import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolver

+import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration

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

 

 class GeneralTest {

-        def static String createAndSolveProblem(EcoreMetamodelDescriptor metamodel, List<EObject> partialModel, ViatraQuerySetDescriptor queries, FileSystemWorkspace workspace) {

+        def static String createAndSolveProblem(EcoreMetamodelDescriptor metamodel, List<EObject> partialModel,

+                ViatraQuerySetDescriptor queries, FileSystemWorkspace workspace) {

                 val Ecore2Logic ecore2Logic = new Ecore2Logic

                 val Logic2Ecore logic2Ecore = new Logic2Ecore(ecore2Logic)

                 val Viatra2Logic viatra2Logic = new Viatra2Logic(ecore2Logic)

                 val InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic

-                

-                val modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel,new Ecore2LogicConfiguration())

-                var problem = instanceModel2Logic.transform(modelGenerationProblem,partialModel).output

-                problem = viatra2Logic.transformQueries(queries,modelGenerationProblem,new Viatra2LogicConfiguration).output

-                

+

+                val modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, new Ecore2LogicConfiguration())

+                var problem = instanceModel2Logic.transform(modelGenerationProblem, partialModel).output

+                problem = viatra2Logic.transformQueries(queries, modelGenerationProblem, new Viatra2LogicConfiguration).output

+

                 workspace.writeModel(problem, "Fam.logicproblem")

-                

+

                 println("Problem created")

-                

+

                 var LogicResult solution

                 var LogicReasoner reasoner

+                

                 //*

                 reasoner = new VampireSolver

                 val vampireConfig = new VampireSolverConfiguration => [

-                        //add configuration things, in config file first

-                        it.writeToFile = true

+                        // add configuration things, in config file first

+                        it.documentationLevel = DocumentationLevel::FULL

+                        it.typeScopes.minNewElements = 5

                 ]

+                solution = reasoner.solve(problem, vampireConfig, workspace)

                 

-                solution = reasoner.solve(problem, vampireConfig,       workspace)

+                /*/

                 

+                reasoner = new AlloySolver

+                val alloyConfig = new AlloySolverConfiguration => [

+                        it.typeScopes.maxNewElements = 7

+                        it.typeScopes.minNewElements = 3

+                        it.solutionScope.numberOfRequiredSolution = 1

+                        it.typeScopes.maxNewIntegers = 0

+                        it.documentationLevel = DocumentationLevel::NORMAL

+                ]

+                solution = reasoner.solve(problem, alloyConfig, workspace)

+                //*/

+

                 println("Problem solved")

         }

-        

+

         def static loadMetamodel(EPackage pckg) {

                 val List<EClass> classes = pckg.getEClassifiers.filter(EClass).toList

                 val List<EEnum> enums = pckg.getEClassifiers.filter(EEnum).toList

                 val List<EEnumLiteral> literals = enums.map[getELiterals].flatten.toList

                 val List<EReference> references = classes.map[getEReferences].flatten.toList

                 val List<EAttribute> attributes = classes.map[getEAttributes].flatten.toList

-                return new EcoreMetamodelDescriptor(classes,#{},false,enums,literals,references,attributes)

+                return new EcoreMetamodelDescriptor(classes, #{}, false, enums, literals, references, attributes)

         }

 

         def static loadPartialModel(ReasonerWorkspace inputs, String path) {

                 Resource.Factory.Registry.INSTANCE.getExtensionToFactoryMap().put("*", new XMIResourceFactoryImpl());

-                inputs.readModel(EObject,path).eResource.contents

+                inputs.readModel(EObject, path).eResource.contents

 //              inputs.readModel(EObject,"FamInstance.xmi").eResource.allContents.toList

         }

 

         def static loadQueries(EcoreMetamodelDescriptor metamodel, IQueryGroup i) {

                 val patterns = i.specifications.toList

-                val wfPatterns = patterns.filter[it.allAnnotations.exists[it.name== "Constraint"]].toSet

+                val wfPatterns = patterns.filter[it.allAnnotations.exists[it.name == "Constraint"]].toSet

                 val derivedFeatures = emptyMap

-                //NO DERIVED FEATURES

+                // NO DERIVED FEATURES

 //              val derivedFeatures = new LinkedHashMap

 //              derivedFeatures.put(i.type,metamodel.attributes.filter[it.name == "type"].head)

 //              derivedFeatures.put(i.model,metamodel.references.filter[it.name == "model"].head)

@@ -86,4 +104,4 @@ class GeneralTest {
                 )

                 return res

         }

-}
\ No newline at end of file
+}

diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.xtend b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.xtend
index e4f6f87a..eb3f4b14 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.xtend
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.xtend
@@ -1,11 +1,11 @@
 package ca.mcgill.ecse.dslreasoner.vampire.icse

 

 import functionalarchitecture.FunctionalarchitecturePackage

-import hu.bme.mit.inf.dslreasoner.domains.y

 import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace

 import org.eclipse.emf.ecore.resource.Resource

 import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl

 import hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.yakindumm.YakindummPackage

+import ca.mcgill.ecse.dslreasoner.standalone.test.yakindu.queries.YakinduPatterns

 

 class YakinduTest {

         def static void main(String[] args) {

@@ -23,11 +23,11 @@ class YakinduTest {
 

                 val metamodel = GeneralTest.loadMetamodel(YakindummPackage.eINSTANCE)

                 val partialModel = GeneralTest.loadPartialModel(inputs, "Yakindu.xmi")

-                val queries = GeneralTest.loadQueries(metamodel, 

+//              val queries = GeneralTest.loadQueries(metamodel, FamPa

 

                 println("DSL loaded")

                 

-                GeneralTest.createAndSolveProblem(metamodel, partialModel, queries, workspace)  

+//              GeneralTest.createAndSolveProblem(metamodel, partialModel, queries, workspace)  

         }

         

         

diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/queries/FamPatterns.vql b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/queries/FamPatterns.vql
index 013d0419..60679874 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/queries/FamPatterns.vql
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/queries/FamPatterns.vql
@@ -1,4 +1,4 @@
-package hu.bme.mit.inf.dslreasoner.domains.fam

+package ca.mcgill.ecse.dslreasoner.vampire.queries

 

 import epackage "http://www.inf.mit.bme.hu/viatrasolver/example/fam"

 

diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/test/MedicalSystem.xtend b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/test/MedicalSystem.xtend
index 15f9e1fe..40cb70a7 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/test/MedicalSystem.xtend
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/test/MedicalSystem.xtend
@@ -1,19 +1,17 @@
 package ca.mcgill.ecse.dslreasoner.vampire.test
 
 import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetup
+import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver
+import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration
 import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.Ecore2logicannotationsPackage
+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.logiclanguage.LogiclanguagePackage
 import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
 import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage
 import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult
-import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver
-import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration
-import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory
-import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel
 import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.Viatra2LogicAnnotationsPackage
 import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace
-import java.util.Collections
 import org.eclipse.emf.common.util.URI
 import org.eclipse.emf.ecore.resource.Resource
 import org.eclipse.emf.ecore.resource.impl.ResourceSetImpl
@@ -41,7 +39,7 @@ class MedicalSystem {
                 reasoner = new VampireSolver
                 val vampireConfig = new VampireSolverConfiguration => [
                         //add configuration things, in config file first
-                        it.writeToFile = true
+                it.documentationLevel = DocumentationLevel::FULL
                 ]
                 
                 solution = reasoner.solve(root, vampireConfig,  workspace)
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/test/VampireTest.xtend b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/test/VampireTest.xtend
index 4fc81ad8..bbb14f1f 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/test/VampireTest.xtend
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/test/VampireTest.xtend
@@ -1,23 +1,19 @@
 package ca.mcgill.ecse.dslreasoner.vampire.test

 

-

 import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetup

+import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver

+import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration

 import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.Ecore2logicannotationsPackage

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

 import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicProblemBuilder

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

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

 import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage

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

-import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver

-import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration

 import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.Viatra2LogicAnnotationsPackage

 import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace

-import java.util.Collections

-import org.eclipse.emf.common.util.URI

 import org.eclipse.emf.ecore.resource.Resource

-import org.eclipse.emf.ecore.resource.impl.ResourceSetImpl

 import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl

-import java.io.File

 

 class VampireTest {

         

@@ -65,7 +61,8 @@ class VampireTest {
                 reasoner = new VampireSolver

                 val vampireConfig = new VampireSolverConfiguration => [

                         //add configuration things, in config file first

-                        it.writeToFile = true

+                        it.documentationLevel = DocumentationLevel::FULL

+                        it.typeScopes.minNewElements = 4

                 ]

                 

                 solution = reasoner.solve(problem, vampireConfig,       workspace)

diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.EcoreTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.EcoreTest.xtendbin
index cf5c79b4..59a3bc01 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.EcoreTest.xtendbin
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.EcoreTest.xtendbin
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FAMTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FAMTest.xtendbin
index 33fae225..1406c597 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FAMTest.xtendbin
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FAMTest.xtendbin
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FileSystemTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FileSystemTest.xtendbin
index 56144b8f..20397ff3 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FileSystemTest.xtendbin
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FileSystemTest.xtendbin
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.GeneralTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.GeneralTest.xtendbin
index 29d89e94..ebca0881 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.GeneralTest.xtendbin
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.GeneralTest.xtendbin
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.YakinduTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.YakinduTest.xtendbin
index c0d35b2f..8fc60bab 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.YakinduTest.xtendbin
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.YakinduTest.xtendbin
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/EcoreTest.java b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/EcoreTest.java
index f3dc8572..820dd354 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/EcoreTest.java
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/EcoreTest.java
@@ -8,6 +8,7 @@ import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic;
 import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration;

 import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace;

 import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor;

+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.TracedOutput;

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

@@ -70,7 +71,7 @@ public class EcoreTest {
       reasoner = _vampireSolver;

       VampireSolverConfiguration _vampireSolverConfiguration = new VampireSolverConfiguration();

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

-        it.writeToFile = true;

+        it.documentationLevel = DocumentationLevel.FULL;

       };

       final VampireSolverConfiguration vampireConfig = ObjectExtensions.<VampireSolverConfiguration>operator_doubleArrow(_vampireSolverConfiguration, _function);

       solution = reasoner.solve(logicProblem, vampireConfig, workspace);

diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.java b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.java
index 92803b7f..dd061008 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.java
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.java
@@ -1,11 +1,12 @@
 package ca.mcgill.ecse.dslreasoner.vampire.icse;

 

 import ca.mcgill.ecse.dslreasoner.vampire.icse.GeneralTest;

+import ca.mcgill.ecse.dslreasoner.vampire.queries.FamPatterns;

 import functionalarchitecture.FunctionalarchitecturePackage;

-import hu.bme.mit.inf.dslreasoner.domains.transima.fam.FamPatterns;

 import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor;

 import hu.bme.mit.inf.dslreasoner.viatra2logic.ViatraQuerySetDescriptor;

 import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace;

+import java.util.LinkedList;

 import java.util.Map;

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

 import org.eclipse.emf.ecore.EObject;

@@ -30,9 +31,10 @@ public class FAMTest {
     map.put("logicproblem", _xMIResourceFactoryImpl);

     InputOutput.<String>println("Input and output workspaces are created");

     final EcoreMetamodelDescriptor metamodel = GeneralTest.loadMetamodel(FunctionalarchitecturePackage.eINSTANCE);

-    final EList<EObject> partialModel = GeneralTest.loadPartialModel(inputs, "FunctionalArchitectureModel.xmi");

+    final EList<EObject> partialModel = GeneralTest.loadPartialModel(inputs, "FunctionalArchitectureModel2.xmi");

     final ViatraQuerySetDescriptor queries = GeneralTest.loadQueries(metamodel, FamPatterns.instance());

     InputOutput.<String>println("DSL loaded");

-    GeneralTest.createAndSolveProblem(metamodel, partialModel, queries, workspace);

+    LinkedList<EObject> _linkedList = new LinkedList<EObject>();

+    GeneralTest.createAndSolveProblem(metamodel, _linkedList, queries, workspace);

   }

 }

diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.java b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.java
index 92cf666c..2401e710 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.java
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.java
@@ -8,6 +8,7 @@ import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic;
 import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration;

 import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace;

 import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor;

+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.TracedOutput;

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

@@ -69,7 +70,8 @@ public class GeneralTest {
         reasoner = _vampireSolver;

         VampireSolverConfiguration _vampireSolverConfiguration = new VampireSolverConfiguration();

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

-          it.writeToFile = true;

+          it.documentationLevel = DocumentationLevel.FULL;

+          it.typeScopes.minNewElements = 5;

         };

         final VampireSolverConfiguration vampireConfig = ObjectExtensions.<VampireSolverConfiguration>operator_doubleArrow(_vampireSolverConfiguration, _function);

         solution = reasoner.solve(problem, vampireConfig, workspace);

diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.java b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.java
index fa4ef6b9..bea4e8a6 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.java
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.java
@@ -1,10 +1,34 @@
 package ca.mcgill.ecse.dslreasoner.vampire.icse;

 

+import ca.mcgill.ecse.dslreasoner.vampire.icse.GeneralTest;

+import hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.yakindumm.YakindummPackage;

+import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor;

+import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace;

+import java.util.Map;

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

+import org.eclipse.emf.ecore.EObject;

+import org.eclipse.emf.ecore.resource.Resource;

+import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl;

+import org.eclipse.xtend2.lib.StringConcatenation;

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

+

 @SuppressWarnings("all")

 public class YakinduTest {

   public static void main(final String[] args) {

-    throw new Error("Unresolved compilation problems:"

-      + "\nmissing \')\' at \'GeneralTest\'"

-      + "\nType mismatch: cannot convert from String to IQueryGroup");

+    StringConcatenation _builder = new StringConcatenation();

+    _builder.append("initialModels/");

+    final FileSystemWorkspace inputs = new FileSystemWorkspace(_builder.toString(), "");

+    StringConcatenation _builder_1 = new StringConcatenation();

+    _builder_1.append("output/YakinduTest/");

+    final FileSystemWorkspace workspace = new FileSystemWorkspace(_builder_1.toString(), "");

+    workspace.initAndClear();

+    final Resource.Factory.Registry reg = Resource.Factory.Registry.INSTANCE;

+    final Map<String, Object> map = reg.getExtensionToFactoryMap();

+    XMIResourceFactoryImpl _xMIResourceFactoryImpl = new XMIResourceFactoryImpl();

+    map.put("logicproblem", _xMIResourceFactoryImpl);

+    InputOutput.<String>println("Input and output workspaces are created");

+    final EcoreMetamodelDescriptor metamodel = GeneralTest.loadMetamodel(YakindummPackage.eINSTANCE);

+    final EList<EObject> partialModel = GeneralTest.loadPartialModel(inputs, "Yakindu.xmi");

+    InputOutput.<String>println("DSL loaded");

   }

 }

diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.MedicalSystem.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.MedicalSystem.xtendbin
index fe447779..e9359697 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.MedicalSystem.xtendbin
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.MedicalSystem.xtendbin
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.SimpleRun.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.SimpleRun.xtendbin
index 8e57f5e7..78d32090 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.SimpleRun.xtendbin
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.SimpleRun.xtendbin
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbin
index 9d12dab4..1f7b3ee7 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbin
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbin
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.gitignore b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.gitignore
index 2760bac4..a16d5bbd 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.gitignore
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.gitignore
@@ -1,12 +1,2 @@
-/.VampireTest.java._trace
-/.SimpleRun.java._trace
-/.DslTest.java._trace
 /.MedicalSystem.java._trace
-/.DslTest.xtendbin
-/.MedicalSystem.xtendbin
-/.SimpleRun.xtendbin
-/.VampireTest.xtendbin
-/DslTest.java
-/MedicalSystem.java
-/VampireTest.java
-/.FAMTest.java._trace
+/.VampireTest.java._trace
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/MedicalSystem.java b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/MedicalSystem.java
index ece0a9bb..0b96a2f3 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/MedicalSystem.java
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/MedicalSystem.java
@@ -4,6 +4,7 @@ import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetup;
 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver;

 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration;

 import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.Ecore2logicannotationsPackage;

+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.logiclanguage.LogiclanguagePackage;

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

@@ -40,7 +41,7 @@ public class MedicalSystem {
       reasoner = _vampireSolver;

       VampireSolverConfiguration _vampireSolverConfiguration = new VampireSolverConfiguration();

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

-        it.writeToFile = true;

+        it.documentationLevel = DocumentationLevel.FULL;

       };

       final VampireSolverConfiguration vampireConfig = ObjectExtensions.<VampireSolverConfiguration>operator_doubleArrow(_vampireSolverConfiguration, _function);

       solution = reasoner.solve(root, vampireConfig, workspace);

diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/VampireTest.java b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/VampireTest.java
index 74f117f2..7228b48a 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/VampireTest.java
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/VampireTest.java
@@ -4,6 +4,7 @@ import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetup;
 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver;

 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration;

 import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.Ecore2logicannotationsPackage;

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

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

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

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

@@ -68,7 +69,8 @@ public class VampireTest {
       reasoner = _vampireSolver;

       VampireSolverConfiguration _vampireSolverConfiguration = new VampireSolverConfiguration();

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

-        it.writeToFile = true;

+        it.documentationLevel = DocumentationLevel.FULL;

+        it.typeScopes.minNewElements = 4;

       };

       final VampireSolverConfiguration vampireConfig = ObjectExtensions.<VampireSolverConfiguration>operator_doubleArrow(_vampireSolverConfiguration, _function);

       solution = reasoner.solve(problem, vampireConfig, workspace);