implement http requests for the TPTP server

52 files changed, 387 insertions, 228 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 ef511dca..1eaefbda 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 c9ed86f5..05c29aff 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 e24f55b7..12f063b1 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 af221451..88a713db 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 1f1241ce..31d3dbf6 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 e89f2182..ca30b3d0 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 9c0c7969..0d75d237 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 fe289357..a8d38a91 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 6cb28d31..0192cd3c 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 7e8ae1ab..07f4c611 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 81de0171..01c9f74f 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 c5672cca..b4bd4155 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 2b96a53a..5dd72d15 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 5faad94e..db384a64 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/VampireAnalyzerConfiguration.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireAnalyzerConfiguration.xtend
index b223dbe5..4e9737cb 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireAnalyzerConfiguration.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireAnalyzerConfiguration.xtend
@@ -8,6 +8,7 @@ class VampireSolverConfiguration extends LogicSolverConfiguration {
         public var boolean uniquenessDuplicates = false
         public var int iteration = -1
         public var BackendSolver solver = BackendSolver::VAMP
+        public var genModel = true
         //choose needed backend solver
 //      public var VampireBackendSolver solver = VampireBackendSolver.SAT4J
 }
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend
index 3281a196..85b81a8c 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend
@@ -31,29 +31,32 @@ class VampireSolver extends LogicReasoner {
         val Vampire2LogicMapper backwardMapper = new Vampire2LogicMapper
         val VampireHandler handler = new VampireHandler
 
-        var fileName = "problem.tptp"
+//      var fileName = "problem.tptp"
 
-        def solve(LogicProblem problem, LogicSolverConfiguration config, ReasonerWorkspace workspace, String location) {
-                fileName = location + fileName
-                solve(problem, config, workspace)
-        }
+//      def solve(LogicProblem problem, LogicSolverConfiguration config, ReasonerWorkspace workspace, String location) {
+//              fileName = location + fileName
+//              solve(problem, config, workspace)
+//      }
 
         override solve(LogicProblem problem, LogicSolverConfiguration config,
                 ReasonerWorkspace workspace) throws LogicReasonerException {
                 val vampireConfig = config.asConfig
+                var fileName = "problem_" + vampireConfig.typeScopes.minNewElements + "-" + vampireConfig.typeScopes.maxNewElements + ".tptp"
 
                 // Start: Logic -> Vampire mapping
                 val transformationStart = System.currentTimeMillis
                 // TODO
                 val result = forwardMapper.transformProblem(problem, vampireConfig)
                 val transformationTime = System.currentTimeMillis - transformationStart
-                
+
                 val vampireProblem = result.output
                 val forwardTrace = result.trace
 
                 var String fileURI = null;
                 var String vampireCode = null;
                 vampireCode = workspace.writeModelToString(vampireProblem, fileName)
+                
+                
 
                 val writeFile = (
                         vampireConfig.documentationLevel === DocumentationLevel::NORMAL ||
@@ -61,35 +64,33 @@ class VampireSolver extends LogicReasoner {
                 if (writeFile) {
                         fileURI = workspace.writeModel(vampireProblem, fileName).toFileString
                 }
-                
-                
-                
+
 //              Resource.Factory.Registry.INSTANCE.getExtensionToFactoryMap().put("tptp", new VampireLanguageFactoryImpl)
 ////            val Resource resource = Resource.
 ////            Resource.getResource(wsURI+"problem.tptp") as Resource
 ////            resource
 //              val model = workspace.readModel(VampireModel, "problem.tptp").eResource.contents
 //              println(model)
-                
-
-                // Result as String
-                
                 // Finish: Logic -> Vampire mapping
-                
-                // Start: Solving .tptp problem
-                val MonitoredVampireSolution vampSol = handler.callSolver(vampireProblem, workspace, vampireConfig)
-                // Finish: Solving .tptp problem
-                
-                // Start: Vampire -> Logic mapping
-                val backTransformationStart = System.currentTimeMillis
-                // Backwards Mapper
-                val logicResult = backwardMapper.transformOutput(problem,vampireConfig.solutionScope.numberOfRequiredSolution,vampSol,forwardTrace,transformationTime)
+                if (vampireConfig.genModel) {
 
-                val backTransformationTime = System.currentTimeMillis - backTransformationStart
-                // Finish: Vampire -> Logic Mapping
-                
+                        // Start: Solving .tptp problem
+                        val MonitoredVampireSolution vampSol = handler.callSolver(vampireProblem, workspace, vampireConfig)
+                        // Finish: Solving .tptp problem
+                        // Start: Vampire -> Logic mapping
+                        val backTransformationStart = System.currentTimeMillis
+                        // Backwards Mapper
+                        val logicResult = backwardMapper.transformOutput(problem,
+                                vampireConfig.solutionScope.numberOfRequiredSolution, vampSol, forwardTrace, transformationTime)
+
+                        val backTransformationTime = System.currentTimeMillis - backTransformationStart
+                        // Finish: Vampire -> Logic Mapping
 //              print(vampSol.generatedModel.tfformulas.size)
-                return logicResult //currently only a ModelResult
+                        return logicResult // currently only a ModelResult
+                }
+                
+                return backwardMapper.transformOutput(problem,
+                                vampireConfig.solutionScope.numberOfRequiredSolution, new MonitoredVampireSolution(-1, null), forwardTrace, transformationTime)
         }
 
         def asConfig(LogicSolverConfiguration configuration) {
@@ -105,9 +106,9 @@ class VampireSolver extends LogicReasoner {
 //       * 
         override getInterpretations(ModelResult modelResult) {
 //               val answers = (modelResult.representation as MonitoredAlloySolution).aswers.map[key]
-                val sols = modelResult.representation// as List<A4Solution>
-                //val res = answers.map 
-                sols.map[
+                val sols = modelResult.representation // as List<A4Solution>
+                // val res = answers.map 
+                sols.map [
                         new VampireModelInterpretation(
 //                              forwardMapper.typeMapper.typeInterpreter,
                                 it as VampireModel,
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 df3cfd82..39862c65 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
@@ -25,8 +25,7 @@ class Logic2VampireLanguageMapper_ScopeMapper {
 

         def dispatch public void transformScope(List<Type> types, VampireSolverConfiguration config,

                 Logic2VampireLanguageMapperTrace trace) {

-                val ABSOLUTE_MIN = 0

-                val ABSOLUTE_MAX = Integer.MAX_VALUE

+                

 

 //              TODO HANDLE ERRORS RELATED TO MAX > MIN

 //              TODO HANDLE ERROR RELATED TO SUM(MIN TYPES)+1(for root) > MAX OBJECTS

@@ -40,6 +39,8 @@ class Logic2VampireLanguageMapper_ScopeMapper {
                 // Number of defined non-abstract elements that are not enum elements

                 // Equals the number of elements in te initial model

                 var elemsInIM = trace.definedElement2String.size

+                val ABSOLUTE_MIN = 0

+                val ABSOLUTE_MAX = -1-elemsInIM

 //              var elemsInIM = 0

 //              

 //              for(t : types.filter(TypeDefinition).filter[!isIsAbstract]) {

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.xtend
index c1eb3382..47eae807 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.xtend
@@ -52,8 +52,10 @@ class VampireHandler {
 

                 val CMD = "cmd /c "

                 val TEMPNAME = "TEMP.tptp"

-                val SOLNNAME = "solution" + configuration.solver.toString + "_" + configuration.typeScopes.maxNewElements +

-                        "_" + configuration.iteration + ".tptp"

+//              val SOLNNAME = "solution" + configuration.solver.toString + "_" + configuration.typeScopes.maxNewElements +

+//                      "_" + configuration.iteration + ".tptp"

+                val SOLNNAME = "solution" + "_" + configuration.typeScopes.maxNewElements + "_" + configuration.iteration +

+                        ".tptp"

                 val PATH = "C:/cygwin64/bin"

 

                 val wsURI = workspace.workspaceURI

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 85f3773c..e50e6812 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 77dc060f..e4925e24 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.java
index c3e185f5..432b14c3 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.java
@@ -24,7 +24,6 @@ import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace;
 import java.util.List;

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

 import org.eclipse.xtend2.lib.StringConcatenation;

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

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

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

 

@@ -42,24 +41,10 @@ public class VampireSolver extends LogicReasoner {
   

   private final VampireHandler handler = new VampireHandler();

   

-  private String fileName = "problem.tptp";

-  

-  public LogicResult solve(final LogicProblem problem, final LogicSolverConfiguration config, final ReasonerWorkspace workspace, final String location) {

-    try {

-      LogicResult _xblockexpression = null;

-      {

-        this.fileName = (location + this.fileName);

-        _xblockexpression = this.solve(problem, config, workspace);

-      }

-      return _xblockexpression;

-    } catch (Throwable _e) {

-      throw Exceptions.sneakyThrow(_e);

-    }

-  }

-  

   @Override

   public LogicResult solve(final LogicProblem problem, final LogicSolverConfiguration config, final ReasonerWorkspace workspace) throws LogicReasonerException {

     final VampireSolverConfiguration vampireConfig = this.asConfig(config);

+    String fileName = (((("problem_" + Integer.valueOf(vampireConfig.typeScopes.minNewElements)) + "-") + Integer.valueOf(vampireConfig.typeScopes.maxNewElements)) + ".tptp");

     final long transformationStart = System.currentTimeMillis();

     final TracedOutput<VampireModel, Logic2VampireLanguageMapperTrace> result = this.forwardMapper.transformProblem(problem, vampireConfig);

     long _currentTimeMillis = System.currentTimeMillis();

@@ -68,18 +53,24 @@ public class VampireSolver extends LogicReasoner {
     final Logic2VampireLanguageMapperTrace forwardTrace = result.getTrace();

     String fileURI = null;

     String vampireCode = null;

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

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

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

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

     if (writeFile) {

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

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

+    }

+    if (vampireConfig.genModel) {

+      final MonitoredVampireSolution vampSol = this.handler.callSolver(vampireProblem, workspace, vampireConfig);

+      final long backTransformationStart = System.currentTimeMillis();

+      final ModelResult logicResult = this.backwardMapper.transformOutput(problem, 

+        vampireConfig.solutionScope.numberOfRequiredSolution, vampSol, forwardTrace, transformationTime);

+      long _currentTimeMillis_1 = System.currentTimeMillis();

+      final long backTransformationTime = (_currentTimeMillis_1 - backTransformationStart);

+      return logicResult;

     }

-    final MonitoredVampireSolution vampSol = this.handler.callSolver(vampireProblem, workspace, vampireConfig);

-    final long backTransformationStart = System.currentTimeMillis();

-    final ModelResult logicResult = this.backwardMapper.transformOutput(problem, vampireConfig.solutionScope.numberOfRequiredSolution, vampSol, forwardTrace, transformationTime);

-    long _currentTimeMillis_1 = System.currentTimeMillis();

-    final long backTransformationTime = (_currentTimeMillis_1 - backTransformationStart);

-    return logicResult;

+    MonitoredVampireSolution _monitoredVampireSolution = new MonitoredVampireSolution((-1), null);

+    return this.backwardMapper.transformOutput(problem, 

+      vampireConfig.solutionScope.numberOfRequiredSolution, _monitoredVampireSolution, forwardTrace, transformationTime);

   }

   

   public VampireSolverConfiguration asConfig(final LogicSolverConfiguration configuration) {

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolverConfiguration.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolverConfiguration.java
index 7bb17b59..dd66e910 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolverConfiguration.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolverConfiguration.java
@@ -12,4 +12,6 @@ public class VampireSolverConfiguration extends LogicSolverConfiguration {
   public int iteration = (-1);

   

   public BackendSolver solver = BackendSolver.VAMP;

+  

+  public boolean genModel = true;

 }

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 eb1685d1..8d2ec6ab 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 3ddf9cfc..515b4b3c 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 66f9d9e8..46ad8c79 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin
index bafcfab6..169aedc2 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin
index a4af882f..699ce6e2 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 08f9fd96..799515d4 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 dc25e3be..2a112ae7 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 37b0c7a5..7f32e055 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin
index 6d562aa8..a2dd469b 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 5ed9ac3b..98c355ab 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 111053a4..246c08c8 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 f33599f9..9e55bac4 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_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 6da75271..bc39a068 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
@@ -53,9 +53,9 @@ public class Logic2VampireLanguageMapper_ScopeMapper {
   }

   

   public void _transformScope(final List<Type> types, final VampireSolverConfiguration config, final Logic2VampireLanguageMapperTrace trace) {

-    final int ABSOLUTE_MIN = 0;

-    final int ABSOLUTE_MAX = Integer.MAX_VALUE;

     int elemsInIM = trace.definedElement2String.size();

+    final int ABSOLUTE_MIN = 0;

+    final int ABSOLUTE_MAX = ((-1) - elemsInIM);

     final int GLOBAL_MIN = (config.typeScopes.minNewElements - elemsInIM);

     final int GLOBAL_MAX = (config.typeScopes.maxNewElements - elemsInIM);

     final ArrayList<VLSConstant> localInstances = CollectionLiterals.<VLSConstant>newArrayList();

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.java
index 7906c5fb..fcbdfde7 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.java
@@ -30,19 +30,13 @@ public class VampireHandler {
       final String CVC4LOC = (CVC4DIR + CVC4NAME);

       final String CMD = "cmd /c ";

       final String TEMPNAME = "TEMP.tptp";

-      String _string = configuration.solver.toString();

-      String _plus = ("solution" + _string);

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

-      String _plus_2 = (_plus_1 + Integer.valueOf(configuration.typeScopes.maxNewElements));

-      String _plus_3 = (_plus_2 + 

-        "_");

-      String _plus_4 = (_plus_3 + Integer.valueOf(configuration.iteration));

-      final String SOLNNAME = (_plus_4 + ".tptp");

+      final String SOLNNAME = ((((("solution" + "_") + Integer.valueOf(configuration.typeScopes.maxNewElements)) + "_") + Integer.valueOf(configuration.iteration)) + 

+        ".tptp");

       final String PATH = "C:/cygwin64/bin";

       final URI wsURI = workspace.getWorkspaceURI();

       final String tempLoc = (wsURI + TEMPNAME);

-      String _plus_5 = (wsURI + SOLNNAME);

-      final String solnLoc = (_plus_5 + " ");

+      String _plus = (wsURI + SOLNNAME);

+      final String solnLoc = (_plus + " ");

       String tempURI = workspace.writeModel(problem, TEMPNAME).toFileString();

       long startTime = (-((long) 1));

       long solverTime = (-((long) 1));

diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/.classpath b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/.classpath
index 3f0838b6..7618afdf 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/.classpath
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/.classpath
@@ -5,5 +5,11 @@
         <classpathentry kind="src" path="src"/>

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

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

+        <classpathentry kind="lib" path="InputLPs/unirest-java-1.4.9.jar"/>

+        <classpathentry kind="lib" path="InputLPs/annotations-13.0.jar"/>

+        <classpathentry kind="lib" path="InputLPs/kotlin-stdlib-1.3.50.jar"/>

+        <classpathentry kind="lib" path="InputLPs/kotlin-stdlib-common-1.3.50.jar"/>

+        <classpathentry kind="lib" path="InputLPs/okhttp-4.2.0.jar"/>

+        <classpathentry kind="lib" path="InputLPs/okio-2.2.2.jar"/>

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

 </classpath>

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 0af80e6c..dead7622 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
@@ -6,48 +6,44 @@ Bundle-Version: 1.0.0.qualifier
 Bundle-ClassPath: .
 Bundle-Vendor: %providerName
 Bundle-Localization: plugin
-Export-Package: ca.mcgill.ecse.dslreasoner.vamipre.yakindumm,
- ca.mcgill.ecse.dslreasoner.vamipre.yakindumm.impl,
- ca.mcgill.ecse.dslreasoner.vamipre.yakindumm.util,
- ca.mcgill.ecse.dslreasoner.vampire.queries,
- ca.mcgill.ecse.dslreasoner.vampire.yakindumm,
- ca.mcgill.ecse.dslreasoner.vampire.yakindumm.impl,
- ca.mcgill.ecse.dslreasoner.vampire.yakindumm.util,
- yakindumm,
- yakindumm.impl,
- yakindumm.util,
- yakindumm.yakindumm,
- yakindumm.yakindumm.impl,
- yakindumm.yakindumm.util
+Export-Package: ca.mcgill.ecse.dslreasoner.vampire.queries,
+  ca.mcgill.ecse.dslreasoner.vampire.yakindumm,
+  ca.mcgill.ecse.dslreasoner.vampire.yakindumm.impl,
+  ca.mcgill.ecse.dslreasoner.vampire.yakindumm.util
 Require-Bundle: org.eclipse.viatra.addon.querybasedfeatures.runtime,
- org.eclipse.core.runtime,
- org.eclipse.emf.ecore;visibility:=reexport,
- 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"
+  org.eclipse.core.runtime,
+  org.eclipse.emf.ecore;visibility:=reexport,
+  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",
+  org.apache.httpcomponents.httpcore;bundle-version="4.4.6",
+  org.apache.httpcomponents.httpclient;bundle-version="4.5.2",
+  org.apache.httpcomponents.httpclient.source;bundle-version="4.5.2",
+  org.apache.httpcomponents.httpclient.win;bundle-version="4.5.2",
+  org.apache.httpcomponents.httpcore.source;bundle-version="4.4.6"
 Import-Package: org.apache.log4j
 Automatic-Module-Name: ca.mcgill.ecse.dslreasoner.vampire.test
 Bundle-ActivationPolicy: lazy
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FileSystemTest.xtend b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FileSystemTest.xtend
index 2495ab77..5289371f 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FileSystemTest.xtend
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FileSystemTest.xtend
@@ -86,7 +86,7 @@ class FileSystemTest {
                         it.uniquenessDuplicates = false

                 ]

 

-                var LogicResult solution = reasoner.solve(problem, vampireConfig, workspace, "FS")

+                var LogicResult solution = reasoner.solve(problem, vampireConfig, 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 89375801..5225fb89 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
@@ -9,6 +9,11 @@ import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace
 import java.util.HashMap

 import java.util.List

 import java.util.Map

+import okhttp3.MediaType

+import okhttp3.OkHttpClient

+import okhttp3.Request

+import okhttp3.RequestBody

+import okhttp3.Response

 import org.eclipse.emf.ecore.EAttribute

 import org.eclipse.emf.ecore.EClass

 import org.eclipse.emf.ecore.EEnum

@@ -20,15 +25,77 @@ import org.eclipse.emf.ecore.resource.Resource
 import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl

 import org.eclipse.viatra.query.runtime.api.IQueryGroup

 

-class GeneralTest {     

-        def static Map<Type, Integer> getTypeMap(Map<Class, Integer> classMap, EcoreMetamodelDescriptor metamodel, Ecore2Logic e2l, Ecore2Logic_Trace trace) {

+class GeneralTest {

+        val static USER_AGENT = "Mozilla/5.0 (Windows NT 10.0 Win64 x64) AppleWebKit/537.36 (KHTML, like Gecko) Chrome/77.0.3865.90 Safari/537.36"

+

+        def static void main(String[] args) {

+                val form = makeForm("fof (a, axiom, ! [A] : a(A) ) .", "Z3---4.4.1", "run_z3_tptp -proof -model -t:20 -file:%s", 300)

+                

+//              val x =sendPost("------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"ProblemSource\"\r\n\r\nFORMULAE\r\n------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"FORMULAEProblem\"\r\n\r\n\r\ntester

+//

+//\r\n------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"QuietFlag\"\r\n\r\n-q3\r\n------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"SubmitButton\"\r\n\r\nRunSelectedSystems\r\n

+//

+//------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"System___Paradox---4.0\"\r\n\r\nParadox---4.0\r\n------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"Command___Paradox---4.0\"\r\n\r\nparadox --no-progress --time %d --tstp --model %s\r\n------WebKitFormBoundaryBdFiQ5zEvTbBl4DA--")

+                val x = sendPost(form)

+                print(x.toString)

+        }

+        

+        def static makeForm(String formula, String solver, String cmd, int time) {

+                return header + addSpec(formula) + addOptions + addSolver(solver, cmd.replace("%d", time.toString)) + addEnd

+        }

+

+        def static sendPost(String formData ) throws Exception {

+

+                val OkHttpClient client = new OkHttpClient()

+

+                val MediaType mediaType = MediaType.parse(

+                        "multipart/form-data boundary=----WebKitFormBoundaryBdFiQ5zEvTbBl4DA")

+                val RequestBody body = RequestBody.create(mediaType, formData)          

+                val Request request = new Request.Builder().url("http://www.tptp.org/cgi-bin/SystemOnTPTPFormReply").post(body).

+                        addHeader("Connection", "keep-alive").addHeader("Cache-Control", "max-age=0").addHeader("Origin",

+                                "http://tptp.cs.miami.edu").addHeader("Upgrade-Insecure-Requests", "1").addHeader("Content-Type",

+                                "multipart/form-data boundary=----WebKitFormBoundaryBdFiQ5zEvTbBl4DA").addHeader("User-Agent",

+                                "Mozilla/5.0 (Windows NT 10.0 Win64 x64) AppleWebKit/537.36 (KHTML, like Gecko) Chrome/77.0.3865.90 Safari/537.36").

+                        addHeader("Accept",

+                                "text/html,application/xhtml+xml,application/xmlq=0.9,image/webp,image/apng,*/*q=0.8,application/signed-exchangev=b3").

+                        addHeader("Referer", "http://tptp.cs.miami.edu/cgi-bin/SystemOnTPTP").addHeader("Accept-Encoding",

+                                "gzip, deflate").addHeader("Accept-Language", "en-US,enq=0.9").addHeader("Postman-Token",

+                                "639ff59f-ab5c-4d9f-9da5-ac8bb64be466,ecb71882-f4d8-4126-8a97-4edb07d4055c").addHeader("Host",

+                                "www.tptp.org").addHeader("Content-Length", "44667").addHeader("cache-control", "no-cache").build()

+

+                val Response response = client.newCall(request).execute()

+//              TimeUnit.SECONDS.sleep(5)

+//              return newArrayList( response.body.string.split("\n"))

+return response.body.string

+

+        // case 1: 

+        }

+        def static getHeader() {

+                return "------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"ProblemSource\"\r\n\r\nFORMULAE\r\n------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"FORMULAEProblem\"\r\n\r\n\r\n"

+        }

+        def static addSpec(String spec) {

+                return spec.replace("\n", "\r\n")

+        }

+        def static addOptions() {

+                return "\r\n------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"QuietFlag\"\r\n\r\n-q3\r\n------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"SubmitButton\"\r\n\r\nRunSelectedSystems\r\n"

+        }

+        def static addSolver(String ID, String cmd) {

+                return "------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"System___" + ID + "\"\r\n\r\n" + ID + "\r\n------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"Command___" + ID + "\"\r\n\r\n" + cmd + "\r\n"

+        }

+        def static addEnd() {

+                return "------WebKitFormBoundaryBdFiQ5zEvTbBl4DA--"

+        }

+

+        def static Map<Type, Integer> getTypeMap(Map<Class, Integer> classMap, EcoreMetamodelDescriptor metamodel,

+                Ecore2Logic e2l, Ecore2Logic_Trace trace) {

                 val typeMap = new HashMap<Type, Integer>

                 val listMap = metamodel.classes.toMap[s|s.name]

-                

+

                 for (Class  elem : classMap.keySet) {

                         typeMap.put(e2l.TypeofEClass(

-                        trace, listMap.get(elem.simpleName)

-                ), classMap.get(elem))

+                                trace,

+                                listMap.get(elem.simpleName)

+                        ), classMap.get(elem))

                 }

                 return typeMap

         }

@@ -43,7 +110,7 @@ class GeneralTest {
         }

 

         def static loadPartialModel(ReasonerWorkspace inputs, String path) {

-                Resource.Factory.Registry.INSTANCE.getExtensionToFactoryMap().put("*", new XMIResourceFactoryImpl());

+                Resource.Factory.Registry.INSTANCE.getExtensionToFactoryMap().put("*", new XMIResourceFactoryImpl())

                 inputs.readModel(EObject, path).eResource.contents

 //              inputs.readModel(EObject,"FamInstance.xmi").eResource.allContents.toList

         }

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 28e3e685..c35b200e 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
@@ -3,13 +3,14 @@ package ca.mcgill.ecse.dslreasoner.vampire.icse
 import ca.mcgill.ecse.dslreasoner.vampire.queries.Patterns

 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver

 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration

+import ca.mcgill.ecse.dslreasoner.vampire.yakindumm.CompositeElement

+import ca.mcgill.ecse.dslreasoner.vampire.yakindumm.Region

+import ca.mcgill.ecse.dslreasoner.vampire.yakindumm.Transition

 import ca.mcgill.ecse.dslreasoner.vampire.yakindumm.YakindummPackage

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

 import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic

 import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration

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

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

-import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult

 import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore

 import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic

 import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2LogicConfiguration

@@ -17,8 +18,8 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.Insta
 import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace

 import java.io.PrintWriter

 import java.text.SimpleDateFormat

-import java.time.LocalDate

 import java.util.Date

+import java.util.HashMap

 import org.eclipse.emf.ecore.resource.Resource

 import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl

 

@@ -54,16 +55,18 @@ class YakinduTest {
 //              val queries = null

                 println("DSL loaded")

 

-                var MAX = 80

-                var START = 79

+                var SZ_TOP = 10

+                var SZ_BOT = 126

                 var INC = 1

-                var REPS = 3

+                var REPS = 1

+                

+                val RANGE = 3

 

-                val EXACT = 130

+                val EXACT = 10

                 if (EXACT != -1) {

-                        MAX = EXACT

-                        START = EXACT

-                        INC = 5

+                        SZ_TOP = EXACT

+                        SZ_BOT = EXACT

+                        INC = 1

                         REPS = 1

                 }

 

@@ -77,8 +80,8 @@ class YakinduTest {
                 var transformationTimes = newArrayList

                 var modelFound = true

                 var LogicResult solution = null

-                for (var i = START; i <= MAX; i += INC) {

-                        val num = (i - START) / INC

+                for (var i = SZ_BOT; i <= SZ_TOP; i += INC) {

+                        val num = (i - SZ_BOT) / INC

                         print("Generation " + num + ": SIZE=" + i + " Attempt: ")

                         writer.append(i + ",")

                         solverTimes.clear

@@ -106,17 +109,16 @@ class YakinduTest {
 

                                 // /////////////////////////////////////////////////////

                                 // Minimum Scope

-//                      val classMapMin = new HashMap<Class, Integer>

-//                      classMapMin.put(Region, 1)

-//                      classMapMin.put(Transition, 2)

-//                      classMapMin.put(CompositeElement, 3)

-//                      val typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, modelGenerationProblem.trace)

+                        val classMapMin = new HashMap<Class, Integer>

+                        classMapMin.put(Region, 1)

+                        classMapMin.put(Transition, 2)

+                        classMapMin.put(CompositeElement, 3)

+                        val typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, modelGenerationProblem.trace)

                                 // Maximum Scope

-//                      val classMapMax = new HashMap<Class, Integer>

-//                      classMapMax.put(Region, 5)

-//                      classMapMax.put(Transition, 2)

-//                      classMapMax.put(Synchronization, 4)

-//                      val typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, modelGenerationProblem.trace)

+                        val classMapMax = new HashMap<Class, Integer>

+                        classMapMax.put(Region, 5)

+                        classMapMax.put(Transition, 2)

+                        val typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, modelGenerationProblem.trace)

                                 // Define Config File           

                                 val size = i

                                 val inc = INC

@@ -126,18 +128,18 @@ class YakinduTest {
                                         it.documentationLevel = DocumentationLevel::FULL

                                         it.iteration = iter

                                         it.runtimeLimit = 60

-                                        it.typeScopes.maxNewElements = size

-                                        it.typeScopes.minNewElements = size - 5

-

-//                      if(typeMapMin.size != 0) it.typeScopes.minNewElementsByType = typeMapMin

-//                      if(typeMapMin.size != 0) it.typeScopes.maxNewElementsByType = typeMapMax

+                                        it.typeScopes.maxNewElements = -1

+                                        it.typeScopes.minNewElements = size

+                                        it.genModel = false

+                        if(typeMapMin.size != 0) it.typeScopes.minNewElementsByType = typeMapMin

+                        if(typeMapMin.size != 0) it.typeScopes.maxNewElementsByType = typeMapMax

                                         it.contCycleLevel = 5

                                         it.uniquenessDuplicates = false

                                 ]

 

                                 solution = reasoner.solve(problem, vampireConfig, workspace)

 //                              print((solution as ModelResult).representation.get(0))

-                                val soln = ((solution as ModelResult).representation.get(0) as VampireModel)

+//                              val soln = ((solution as ModelResult).representation.get(0) as VampireModel)

 //                              println(soln.confirmations)

 //                              println((solution as ModelResult).representation)

 //                              modelFound = !soln.confirmations.filter [

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 084503b5..93d27b4d 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 2315cd50..bc2bae6f 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 a3386941..5687258f 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 dee6f742..de68a908 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 f54cd3a0..16a3cd03 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/FileSystemTest.java b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/FileSystemTest.java
index 7579bd98..8c7923be 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/FileSystemTest.java
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/FileSystemTest.java
@@ -25,6 +25,7 @@ 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.Exceptions;

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

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

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

@@ -32,70 +33,74 @@ import org.eclipse.xtext.xbase.lib.Procedures.Procedure1;
 @SuppressWarnings("all")

 public class FileSystemTest {

   public static void main(final String[] args) {

-    final Ecore2Logic ecore2Logic = new Ecore2Logic();

-    final Viatra2Logic viatra2Logic = new Viatra2Logic(ecore2Logic);

-    final InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic();

-    StringConcatenation _builder = new StringConcatenation();

-    _builder.append("initialModels/");

-    final FileSystemWorkspace inputs = new FileSystemWorkspace(_builder.toString(), "");

-    StringConcatenation _builder_1 = new StringConcatenation();

-    _builder_1.append("output/FileSystemTest/");

-    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(filesystemPackage.eINSTANCE);

-    final EList<EObject> partialModel = GeneralTest.loadPartialModel(inputs, "fs/filesystemInstance.xmi");

-    InputOutput.<String>println("DSL loaded");

-    Ecore2LogicConfiguration _ecore2LogicConfiguration = new Ecore2LogicConfiguration();

-    final TracedOutput<LogicProblem, Ecore2Logic_Trace> modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, _ecore2LogicConfiguration);

-    LogicProblem problem = modelGenerationProblem.getOutput();

-    problem = instanceModel2Logic.transform(modelGenerationProblem, partialModel).getOutput();

-    workspace.writeModel(problem, "FileSystem.logicproblem");

-    InputOutput.<String>println("Problem created");

-    long startTime = System.currentTimeMillis();

-    VampireSolver reasoner = null;

-    VampireSolver _vampireSolver = new VampireSolver();

-    reasoner = _vampireSolver;

-    final HashMap<Class, Integer> classMapMin = new HashMap<Class, Integer>();

-    classMapMin.put(Dir.class, Integer.valueOf(10));

-    classMapMin.put(File.class, Integer.valueOf(5));

-    final Map<Type, Integer> typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, modelGenerationProblem.getTrace());

-    final HashMap<Class, Integer> classMapMax = new HashMap<Class, Integer>();

-    classMapMax.put(File.class, Integer.valueOf(15));

-    classMapMax.put(Dir.class, Integer.valueOf(15));

-    final Map<Type, Integer> typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, modelGenerationProblem.getTrace());

-    VampireSolverConfiguration _vampireSolverConfiguration = new VampireSolverConfiguration();

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

-      it.documentationLevel = DocumentationLevel.FULL;

-      it.typeScopes.minNewElements = 10;

-      it.typeScopes.maxNewElements = 25;

-      int _size = typeMapMin.size();

-      boolean _notEquals = (_size != 0);

-      if (_notEquals) {

-        it.typeScopes.minNewElementsByType = typeMapMin;

-      }

-      int _size_1 = typeMapMin.size();

-      boolean _notEquals_1 = (_size_1 != 0);

-      if (_notEquals_1) {

-        it.typeScopes.maxNewElementsByType = typeMapMax;

-      }

-      it.contCycleLevel = 5;

-      it.uniquenessDuplicates = false;

-    };

-    final VampireSolverConfiguration vampireConfig = ObjectExtensions.<VampireSolverConfiguration>operator_doubleArrow(_vampireSolverConfiguration, _function);

-    LogicResult solution = reasoner.solve(problem, vampireConfig, workspace, "FS");

-    long _currentTimeMillis = System.currentTimeMillis();

-    long _minus = (_currentTimeMillis - startTime);

-    long totalTimeMin = (_minus / 60000);

-    long _currentTimeMillis_1 = System.currentTimeMillis();

-    long _minus_1 = (_currentTimeMillis_1 - startTime);

-    long _divide = (_minus_1 / 1000);

-    long totalTimeSec = (_divide % 60);

-    InputOutput.<String>println("Problem solved");

-    InputOutput.<String>println(((("Time was: " + Long.valueOf(totalTimeMin)) + ":") + Long.valueOf(totalTimeSec)));

+    try {

+      final Ecore2Logic ecore2Logic = new Ecore2Logic();

+      final Viatra2Logic viatra2Logic = new Viatra2Logic(ecore2Logic);

+      final InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic();

+      StringConcatenation _builder = new StringConcatenation();

+      _builder.append("initialModels/");

+      final FileSystemWorkspace inputs = new FileSystemWorkspace(_builder.toString(), "");

+      StringConcatenation _builder_1 = new StringConcatenation();

+      _builder_1.append("output/FileSystemTest/");

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

+      final EList<EObject> partialModel = GeneralTest.loadPartialModel(inputs, "fs/filesystemInstance.xmi");

+      InputOutput.<String>println("DSL loaded");

+      Ecore2LogicConfiguration _ecore2LogicConfiguration = new Ecore2LogicConfiguration();

+      final TracedOutput<LogicProblem, Ecore2Logic_Trace> modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, _ecore2LogicConfiguration);

+      LogicProblem problem = modelGenerationProblem.getOutput();

+      problem = instanceModel2Logic.transform(modelGenerationProblem, partialModel).getOutput();

+      workspace.writeModel(problem, "FileSystem.logicproblem");

+      InputOutput.<String>println("Problem created");

+      long startTime = System.currentTimeMillis();

+      VampireSolver reasoner = null;

+      VampireSolver _vampireSolver = new VampireSolver();

+      reasoner = _vampireSolver;

+      final HashMap<Class, Integer> classMapMin = new HashMap<Class, Integer>();

+      classMapMin.put(Dir.class, Integer.valueOf(10));

+      classMapMin.put(File.class, Integer.valueOf(5));

+      final Map<Type, Integer> typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, modelGenerationProblem.getTrace());

+      final HashMap<Class, Integer> classMapMax = new HashMap<Class, Integer>();

+      classMapMax.put(File.class, Integer.valueOf(15));

+      classMapMax.put(Dir.class, Integer.valueOf(15));

+      final Map<Type, Integer> typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, modelGenerationProblem.getTrace());

+      VampireSolverConfiguration _vampireSolverConfiguration = new VampireSolverConfiguration();

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

+        it.documentationLevel = DocumentationLevel.FULL;

+        it.typeScopes.minNewElements = 10;

+        it.typeScopes.maxNewElements = 25;

+        int _size = typeMapMin.size();

+        boolean _notEquals = (_size != 0);

+        if (_notEquals) {

+          it.typeScopes.minNewElementsByType = typeMapMin;

+        }

+        int _size_1 = typeMapMin.size();

+        boolean _notEquals_1 = (_size_1 != 0);

+        if (_notEquals_1) {

+          it.typeScopes.maxNewElementsByType = typeMapMax;

+        }

+        it.contCycleLevel = 5;

+        it.uniquenessDuplicates = false;

+      };

+      final VampireSolverConfiguration vampireConfig = ObjectExtensions.<VampireSolverConfiguration>operator_doubleArrow(_vampireSolverConfiguration, _function);

+      LogicResult solution = reasoner.solve(problem, vampireConfig, workspace);

+      long _currentTimeMillis = System.currentTimeMillis();

+      long _minus = (_currentTimeMillis - startTime);

+      long totalTimeMin = (_minus / 60000);

+      long _currentTimeMillis_1 = System.currentTimeMillis();

+      long _minus_1 = (_currentTimeMillis_1 - startTime);

+      long _divide = (_minus_1 / 1000);

+      long totalTimeSec = (_divide % 60);

+      InputOutput.<String>println("Problem solved");

+      InputOutput.<String>println(((("Time was: " + Long.valueOf(totalTimeMin)) + ":") + Long.valueOf(totalTimeSec)));

+    } catch (Throwable _e) {

+      throw Exceptions.sneakyThrow(_e);

+    }

   }

 }

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 0bb8f76e..ce057092 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
@@ -13,6 +13,11 @@ import java.util.HashMap;
 import java.util.List;

 import java.util.Map;

 import java.util.Set;

+import okhttp3.MediaType;

+import okhttp3.OkHttpClient;

+import okhttp3.Request;

+import okhttp3.RequestBody;

+import okhttp3.Response;

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

 import org.eclipse.emf.ecore.EAttribute;

 import org.eclipse.emf.ecore.EClass;

@@ -28,12 +33,75 @@ import org.eclipse.viatra.query.runtime.api.IQueryGroup;
 import org.eclipse.viatra.query.runtime.api.IQuerySpecification;

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

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

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

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

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

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

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

 

 @SuppressWarnings("all")

 public class GeneralTest {

+  private final static String USER_AGENT = "Mozilla/5.0 (Windows NT 10.0 Win64 x64) AppleWebKit/537.36 (KHTML, like Gecko) Chrome/77.0.3865.90 Safari/537.36";

+  

+  public static void main(final String[] args) {

+    try {

+      final String form = GeneralTest.makeForm("fof (a, axiom, ! [A] : a(A) ) .", "Z3---4.4.1", "run_z3_tptp -proof -model -t:20 -file:%s", 300);

+      final String x = GeneralTest.sendPost(form);

+      InputOutput.<String>print(x.toString());

+    } catch (Throwable _e) {

+      throw Exceptions.sneakyThrow(_e);

+    }

+  }

+  

+  public static String makeForm(final String formula, final String solver, final String cmd, final int time) {

+    String _header = GeneralTest.getHeader();

+    String _addSpec = GeneralTest.addSpec(formula);

+    String _plus = (_header + _addSpec);

+    String _addOptions = GeneralTest.addOptions();

+    String _plus_1 = (_plus + _addOptions);

+    String _addSolver = GeneralTest.addSolver(solver, cmd.replace("%d", Integer.valueOf(time).toString()));

+    String _plus_2 = (_plus_1 + _addSolver);

+    String _addEnd = GeneralTest.addEnd();

+    return (_plus_2 + _addEnd);

+  }

+  

+  public static String sendPost(final String formData) throws Exception {

+    final OkHttpClient client = new OkHttpClient();

+    final MediaType mediaType = MediaType.parse(

+      "multipart/form-data boundary=----WebKitFormBoundaryBdFiQ5zEvTbBl4DA");

+    final RequestBody body = RequestBody.create(mediaType, formData);

+    final Request request = new Request.Builder().url("http://www.tptp.org/cgi-bin/SystemOnTPTPFormReply").post(body).addHeader("Connection", "keep-alive").addHeader("Cache-Control", "max-age=0").addHeader("Origin", 

+      "http://tptp.cs.miami.edu").addHeader("Upgrade-Insecure-Requests", "1").addHeader("Content-Type", 

+      "multipart/form-data boundary=----WebKitFormBoundaryBdFiQ5zEvTbBl4DA").addHeader("User-Agent", 

+      "Mozilla/5.0 (Windows NT 10.0 Win64 x64) AppleWebKit/537.36 (KHTML, like Gecko) Chrome/77.0.3865.90 Safari/537.36").addHeader("Accept", 

+      "text/html,application/xhtml+xml,application/xmlq=0.9,image/webp,image/apng,*/*q=0.8,application/signed-exchangev=b3").addHeader("Referer", "http://tptp.cs.miami.edu/cgi-bin/SystemOnTPTP").addHeader("Accept-Encoding", 

+      "gzip, deflate").addHeader("Accept-Language", "en-US,enq=0.9").addHeader("Postman-Token", 

+      "639ff59f-ab5c-4d9f-9da5-ac8bb64be466,ecb71882-f4d8-4126-8a97-4edb07d4055c").addHeader("Host", 

+      "www.tptp.org").addHeader("Content-Length", "44667").addHeader("cache-control", "no-cache").build();

+    final Response response = client.newCall(request).execute();

+    return response.body().string();

+  }

+  

+  public static String getHeader() {

+    return "------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"ProblemSource\"\r\n\r\nFORMULAE\r\n------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"FORMULAEProblem\"\r\n\r\n\r\n";

+  }

+  

+  public static String addSpec(final String spec) {

+    return spec.replace("\n", "\r\n");

+  }

+  

+  public static String addOptions() {

+    return "\r\n------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"QuietFlag\"\r\n\r\n-q3\r\n------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"SubmitButton\"\r\n\r\nRunSelectedSystems\r\n";

+  }

+  

+  public static String addSolver(final String ID, final String cmd) {

+    return (((((((("------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"System___" + ID) + "\"\r\n\r\n") + ID) + "\r\n------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"Command___") + ID) + "\"\r\n\r\n") + cmd) + "\r\n");

+  }

+  

+  public static String addEnd() {

+    return "------WebKitFormBoundaryBdFiQ5zEvTbBl4DA--";

+  }

+  

   public static Map<Type, Integer> getTypeMap(final Map<Class, Integer> classMap, final EcoreMetamodelDescriptor metamodel, final Ecore2Logic e2l, final Ecore2Logic_Trace trace) {

     final HashMap<Type, Integer> typeMap = new HashMap<Type, Integer>();

     final Function1<EClass, String> _function = (EClass s) -> {

@@ -43,7 +111,8 @@ public class GeneralTest {
     Set<Class> _keySet = classMap.keySet();

     for (final Class elem : _keySet) {

       typeMap.put(

-        e2l.TypeofEClass(trace, listMap.get(elem.getSimpleName())), classMap.get(elem));

+        e2l.TypeofEClass(trace, 

+          listMap.get(elem.getSimpleName())), classMap.get(elem));

     }

     return typeMap;

   }

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 b18ede4f..3a8f3fb4 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
@@ -4,17 +4,19 @@ import ca.mcgill.ecse.dslreasoner.vampire.icse.GeneralTest;
 import ca.mcgill.ecse.dslreasoner.vampire.queries.Patterns;

 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver;

 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration;

+import ca.mcgill.ecse.dslreasoner.vampire.yakindumm.CompositeElement;

+import ca.mcgill.ecse.dslreasoner.vampire.yakindumm.Region;

+import ca.mcgill.ecse.dslreasoner.vampire.yakindumm.Transition;

 import ca.mcgill.ecse.dslreasoner.vampire.yakindumm.YakindummPackage;

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

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

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

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

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

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

 import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore;

 import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic;

 import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2LogicConfiguration;

@@ -26,6 +28,7 @@ import java.io.PrintWriter;
 import java.text.SimpleDateFormat;

 import java.util.ArrayList;

 import java.util.Date;

+import java.util.HashMap;

 import java.util.Map;

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

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

@@ -72,15 +75,16 @@ public class YakinduTest {
       final EList<EObject> partialModel = GeneralTest.loadPartialModel(inputs, "yakindu/Yakindu.xmi");

       final ViatraQuerySetDescriptor queries = GeneralTest.loadQueries(metamodel, Patterns.instance());

       InputOutput.<String>println("DSL loaded");

-      int MAX = 80;

-      int START = 79;

+      int SZ_TOP = 10;

+      int SZ_BOT = 126;

       int INC = 1;

-      int REPS = 3;

-      final int EXACT = 130;

+      int REPS = 1;

+      final int RANGE = 3;

+      final int EXACT = 10;

       if ((EXACT != (-1))) {

-        MAX = EXACT;

-        START = EXACT;

-        INC = 5;

+        SZ_TOP = EXACT;

+        SZ_BOT = EXACT;

+        INC = 1;

         REPS = 1;

       }

       URI _workspaceURI = workspace.getWorkspaceURI();

@@ -96,11 +100,11 @@ public class YakinduTest {
       boolean modelFound = true;

       LogicResult solution = null;

       {

-        int i = START;

-        boolean _while = (i <= MAX);

+        int i = SZ_BOT;

+        boolean _while = (i <= SZ_TOP);

         while (_while) {

           {

-            final int num = ((i - START) / INC);

+            final int num = ((i - SZ_BOT) / INC);

             InputOutput.<String>print((((("Generation " + Integer.valueOf(num)) + ": SIZE=") + Integer.valueOf(i)) + " Attempt: "));

             String _plus_3 = (Integer.valueOf(i) + ",");

             writer.append(_plus_3);

@@ -121,6 +125,15 @@ public class YakinduTest {
                 VampireSolver reasoner = null;

                 VampireSolver _vampireSolver = new VampireSolver();

                 reasoner = _vampireSolver;

+                final HashMap<Class, Integer> classMapMin = new HashMap<Class, Integer>();

+                classMapMin.put(Region.class, Integer.valueOf(1));

+                classMapMin.put(Transition.class, Integer.valueOf(2));

+                classMapMin.put(CompositeElement.class, Integer.valueOf(3));

+                final Map<Type, Integer> typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, modelGenerationProblem.getTrace());

+                final HashMap<Class, Integer> classMapMax = new HashMap<Class, Integer>();

+                classMapMax.put(Region.class, Integer.valueOf(5));

+                classMapMax.put(Transition.class, Integer.valueOf(2));

+                final Map<Type, Integer> typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, modelGenerationProblem.getTrace());

                 final int size = i;

                 final int inc = INC;

                 final int iter = j;

@@ -129,15 +142,24 @@ public class YakinduTest {
                   it.documentationLevel = DocumentationLevel.FULL;

                   it.iteration = iter;

                   it.runtimeLimit = 60;

-                  it.typeScopes.maxNewElements = size;

-                  it.typeScopes.minNewElements = (size - 5);

+                  it.typeScopes.maxNewElements = (-1);

+                  it.typeScopes.minNewElements = size;

+                  it.genModel = false;

+                  int _size = typeMapMin.size();

+                  boolean _notEquals = (_size != 0);

+                  if (_notEquals) {

+                    it.typeScopes.minNewElementsByType = typeMapMin;

+                  }

+                  int _size_1 = typeMapMin.size();

+                  boolean _notEquals_1 = (_size_1 != 0);

+                  if (_notEquals_1) {

+                    it.typeScopes.maxNewElementsByType = typeMapMax;

+                  }

                   it.contCycleLevel = 5;

                   it.uniquenessDuplicates = false;

                 };

                 final VampireSolverConfiguration vampireConfig = ObjectExtensions.<VampireSolverConfiguration>operator_doubleArrow(_vampireSolverConfiguration, _function);

                 solution = reasoner.solve(problem, vampireConfig, workspace);

-                Object _get = ((ModelResult) solution).getRepresentation().get(0);

-                final VampireModel soln = ((VampireModel) _get);

                 int _transformationTime = solution.getStatistics().getTransformationTime();

                 final double tTime = (_transformationTime / 1000.0);

                 int _solverTime = solution.getStatistics().getSolverTime();

@@ -163,7 +185,7 @@ public class YakinduTest {
           }

           int _i = i;

           i = (_i + INC);

-          _while = (i <= MAX);

+          _while = (i <= SZ_TOP);

         }

       }

       writer.close();

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 e77449e7..96f343fa 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 97f29b0c..1ca8223d 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 0e320f18..5d6a9ee2 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