VAMPIRE: complete testing setup

51 files changed, 723 insertions, 384 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 1eaefbda..8225ed58 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 05c29aff..5d455790 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 12f063b1..db1a37c4 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 88a713db..32d2213b 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 31d3dbf6..24c6eca6 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 ca30b3d0..422fad02 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 0d75d237..d6bf1d6f 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 a8d38a91..d341af67 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 0192cd3c..2f552529 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 07f4c611..f73dadba 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 01c9f74f..0b18e8e6 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 b4bd4155..8dac584b 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 5dd72d15..ee3df0a3 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 db384a64..96ae5822 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/.classpath b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/.classpath
index 2a126610..f6de9681 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/.classpath
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/.classpath
@@ -6,5 +6,11 @@
         <classpathentry kind="src" path="xtend-gen"/>

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

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

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

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

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

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

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

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

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

 </classpath>

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 4e9737cb..4c2f1952 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
@@ -2,21 +2,29 @@ package ca.mcgill.ecse.dslreasoner.vampire.reasoner
 
 import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration
 
-class VampireSolverConfiguration extends LogicSolverConfiguration {
+class VampireSolverConfiguration
+ extends LogicSolverConfiguration {
         
         public var int contCycleLevel = 0
         public var boolean uniquenessDuplicates = false
         public var int iteration = -1
-        public var BackendSolver solver = BackendSolver::VAMP
+        public var BackendSolver solver = BackendSolver::VAMPIRE
         public var genModel = true
+        public var server = false
         //choose needed backend solver
 //      public var VampireBackendSolver solver = VampireBackendSolver.SAT4J
 }
 
 
 enum BackendSolver {
-        VAMP,
-        CVC4
+        CVC4,
+        DARWINFM,
+        EDARWIN,
+        GEOIII,
+        IPROVER,
+        PARADOX,
+        VAMPIRE,
+        Z3
         //add needed things
 }
 
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 85b81a8c..31aa091c 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
@@ -4,18 +4,20 @@ import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetup
 import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetupGenerated
 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper
 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace
+import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support
 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.MonitoredVampireSolution
 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Vampire2LogicMapper
 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireHandler
 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireModelInterpretation
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel
-import ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSFiniteModelImpl
 import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel
 import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner
 import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasonerException
 import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration
 import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
+import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultFactory
 import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult
 import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace
 
@@ -30,18 +32,20 @@ class VampireSolver extends LogicReasoner {
         val Logic2VampireLanguageMapper forwardMapper = new Logic2VampireLanguageMapper
         val Vampire2LogicMapper backwardMapper = new Vampire2LogicMapper
         val VampireHandler handler = new VampireHandler
+        val Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support
+        val extension LogicresultFactory resultFactory = LogicresultFactory.eINSTANCE
+        private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE
 
 //      var fileName = "problem.tptp"
-
 //      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"
+                var fileName = "problem_" + vampireConfig.typeScopes.minNewElements + "-" +
+                        vampireConfig.typeScopes.maxNewElements + ".tptp"
 
                 // Start: Logic -> Vampire mapping
                 val transformationStart = System.currentTimeMillis
@@ -55,8 +59,6 @@ class VampireSolver extends LogicReasoner {
                 var String fileURI = null;
                 var String vampireCode = null;
                 vampireCode = workspace.writeModelToString(vampireProblem, fileName)
-                
-                
 
                 val writeFile = (
                         vampireConfig.documentationLevel === DocumentationLevel::NORMAL ||
@@ -73,24 +75,94 @@ class VampireSolver extends LogicReasoner {
 //              println(model)
                 // Finish: Logic -> Vampire mapping
                 if (vampireConfig.genModel) {
-
-                        // 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
+                        if (vampireConfig.server) {
+                                val form = support.makeForm(vampireCode, vampireConfig.solver, vampireConfig.runtimeLimit)
+                                var response = newArrayList
+                                var ind = 0
+                                var done = false
+                                print(" ")
+                                while (!done) {
+                                        print("(x)")
+                                        done = false
+                                        response = support.sendPost(form)
+
+                                        var responseFound = false
+                                        ind = 0
+                                        while (!responseFound) {
+                                                var line = response.get(ind)
+                                                if (line.length >= 5 && line.substring(0, 5) == "ERROR") {
+                                                        done = false
+                                                        responseFound = true
+                                                } else {
+                                                        if (line == "</PRE>") {
+                                                                done = true
+                                                                responseFound = true
+                                                        }
+                                                }
+                                                ind++
+                                        }
+                                }
+                                val satRaw = response.get(ind - 3)
+                                val modRaw = response.get(ind - 2)
+
+                                val sat = newArrayList(satRaw.split(" "))
+                                val mod = newArrayList(modRaw.split(" "))
+
+                                val satOut = sat.get(1)
+                                val modOut = mod.get(1)
+                                val satTime = sat.get(2)
+                                val modTime = mod.get(2)
+
+                                println()
+                                println(sat)
+                                println(mod)
+
+                                return createModelResult => [
+                                        it.problem = null
+                                        it.representation += createVampireModel => []
+                                        it.trace = trace
+                                        it.statistics = createStatistics => [
+                                                it.transformationTime = transformationTime as int
+                                                it.entries += createStringStatisticEntry => [
+                                                        it.name = "satOut"
+                                                        it.value = satOut
+                                                ]
+                                                it.entries += createRealStatisticEntry => [
+                                                        it.name = "satTime"
+                                                        it.value = Double.parseDouble(satTime)
+                                                ]
+                                                it.entries += createStringStatisticEntry => [
+                                                        it.name = "modOut"
+                                                        it.value = modOut
+                                                ]
+                                                it.entries += createRealStatisticEntry => [
+                                                        it.name = "modTime"
+                                                        it.value = Double.parseDouble(modTime)
+                                                ]
+
+                                        ]
+                                ]
+
+//                              return newArrayList(line1, line2)
+                        } else {
+
+                                // 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)
+                return backwardMapper.transformOutput(problem, vampireConfig.solutionScope.numberOfRequiredSolution,
+                        new MonitoredVampireSolution(-1, null), forwardTrace, transformationTime)
         }
 
         def asConfig(LogicSolverConfiguration configuration) {
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 39862c65..a9516cc4 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
@@ -40,7 +40,7 @@ class Logic2VampireLanguageMapper_ScopeMapper {
                 // Equals the number of elements in te initial model

                 var elemsInIM = trace.definedElement2String.size

                 val ABSOLUTE_MIN = 0

-                val ABSOLUTE_MAX = -1-elemsInIM

+                val ABSOLUTE_MAX = Integer.MAX_VALUE-elemsInIM

 //              var elemsInIM = 0

 //              

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

@@ -60,7 +60,7 @@ class Logic2VampireLanguageMapper_ScopeMapper {
 

                 // Handling Minimum_General

                 if (GLOBAL_MIN != ABSOLUTE_MIN) {

-                        getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, !consistant)

+                        getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, consistant)//may make not consistent here 

                         if (consistant) {

                                 for (i : trace.uniqueInstances) {

                                         localInstances.add(support.duplicate(i))

@@ -73,7 +73,7 @@ class Logic2VampireLanguageMapper_ScopeMapper {
 

                 // Handling Maximum_General

                 if (GLOBAL_MAX != ABSOLUTE_MAX) {

-                        getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, consistant)

+                        getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, !consistant)

                         if (consistant) {

                                 makeFofFormula(trace.uniqueInstances as ArrayList, trace, false, null)

                         } else {

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 680213ab..7b1c7d9a 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend
@@ -1,5 +1,6 @@
 package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder
 
+import ca.mcgill.ecse.dslreasoner.vampire.reasoner.BackendSolver
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunctionAsTerm
@@ -16,6 +17,12 @@ import java.util.ArrayList
 import java.util.HashMap
 import java.util.List
 import java.util.Map
+import java.util.concurrent.TimeUnit
+import okhttp3.MediaType
+import okhttp3.OkHttpClient
+import okhttp3.Request
+import okhttp3.RequestBody
+import okhttp3.Response
 import org.eclipse.emf.common.util.EList
 
 import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
@@ -77,13 +84,13 @@ class Logic2VampireLanguageMapper_Support {
                         it.terms += duplicate(v)
                 ]
         }
-        
+
         def protected List<VLSVariable> duplicate(List<VLSVariable> vars) {
-                        var newList = newArrayList
-                        for (v : vars) {
-                                newList.add(duplicate(v))
-                        }
-                        return newList
+                var newList = newArrayList
+                for (v : vars) {
+                        newList.add(duplicate(v))
+                }
+                return newList
         }
 
         def protected VLSConstant toConstant(VLSFunctionAsTerm term) {
@@ -117,7 +124,7 @@ class Logic2VampireLanguageMapper_Support {
 
 // TODO Make more general
         def establishUniqueness(List<VLSConstant> terms, VLSConstant t2) {
-                
+
 //              OLD
 //              val List<VLSInequality> eqs = newArrayList
 //              for (t1 : terms.subList(1, terms.length)) {
@@ -133,7 +140,6 @@ class Logic2VampireLanguageMapper_Support {
 //              }
 //              return unfoldAnd(eqs)
 //              END OLD
-
                 val List<VLSInequality> eqs = newArrayList
                 for (t1 : terms) {
                         if (t1 != t2) {
@@ -257,7 +263,8 @@ class Logic2VampireLanguageMapper_Support {
                         }
                 }
         }
-        //TODO rewrite such that it uses "listSubTypes"
+
+        // TODO rewrite such that it uses "listSubTypes"
         def protected boolean dfsSubtypeCheck(Type type, Type type2) {
                 // There is surely a better way to do this
                 if (type.subtypes.isEmpty)
@@ -284,4 +291,74 @@ class Logic2VampireLanguageMapper_Support {
                 new HashMap(map1) => [putAll(map2)]
         }
 
+        // SERVERS
+        def makeForm(String formula, BackendSolver solver, int time) {
+                return header + formula + addOptions + addSolver(solver, time) + addEnd
+        }
+
+        def getSolverSpecs(BackendSolver solver) {
+                switch (solver) {
+                        case BackendSolver::CVC4: return newArrayList("CVC4---SAT-1.7", "do_CVC4 %s %d SAT")
+                        case BackendSolver::DARWINFM: return newArrayList("DarwinFM---1.4.5", "darwin -fd true -ppp true -pl 0 -to %d -pmtptp true %s")
+                        case BackendSolver::EDARWIN: return newArrayList("E-Darwin---1.5", "e-darwin -pev \"TPTP\" -pmd true -if tptp -pl 2 -pc false -ps false %s")
+                        case BackendSolver::GEOIII: return newArrayList("Geo-III---2018C", "geo -tptp_input -nonempty -include /home/tptp/TPTP -inputfile %s")
+                        case BackendSolver::IPROVER: return newArrayList("iProver---SAT-3.0", "iproveropt_run_sat.sh %d %s")
+                        case BackendSolver::PARADOX: return newArrayList("Paradox---4.0", "paradox --no-progress --time %d --tstp --model %s")
+                        case BackendSolver::VAMPIRE: return newArrayList("Vampire---SAT-4.4", "vampire --mode casc_sat -t %d %s")
+                        case BackendSolver::Z3: return newArrayList("Z3---4.4.1", "run_z3_tptp -proof -model -t:20 -file:%s")
+                }
+        }
+
+        def 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 addSpec(String spec) {
+                return spec.replace("\n", "\\r\\n")
+        }
+
+        def 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 addSolver(BackendSolver solver, int time) {
+                val solverSpecs = getSolverSpecs(solver)
+                val ID = solverSpecs.get(0)
+                val cmd = solverSpecs.get(1)
+
+                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.replace("%d", time.toString) + "\r\n"
+        }
+
+        def addEnd() {
+                return "------WebKitFormBoundaryBdFiQ5zEvTbBl4DA--"
+        }
+
+        def sendPost(String formData) throws Exception {
+
+                val OkHttpClient client = new OkHttpClient.Builder().connectTimeout(350, TimeUnit.SECONDS).readTimeout(350, TimeUnit.SECONDS).build()
+
+                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: 
+        }
+
 }
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 47eae807..6d301442 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
@@ -70,7 +70,7 @@ class VampireHandler {
                 var long startTime = -1 as long

                 var long solverTime = -1 as long

                 var Process p = null

-                if (configuration.solver == BackendSolver::VAMP) {

+                if (configuration.solver == BackendSolver::VAMPIRE) {

 

                         var OPTION = " --mode casc_sat "

                         if (configuration.runtimeLimit != -1) {

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 e50e6812..b26c1ded 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 e4925e24..fb8f872d 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 432b14c3..3e3bd688 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
@@ -5,12 +5,15 @@ import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetupGenerated;
 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

@@ -19,13 +22,25 @@ import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration;
 import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput;

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

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

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

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

+import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.RealStatisticEntry;

+import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.StatisticEntry;

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

+import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.StringStatisticEntry;

 import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace;

+import java.util.ArrayList;

 import java.util.List;

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

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

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

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

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

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

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

 

 @SuppressWarnings("all")

 public class VampireSolver extends LogicReasoner {

@@ -41,36 +56,142 @@ public class VampireSolver extends LogicReasoner {
   

   private final VampireHandler handler = new VampireHandler();

   

+  private final Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support();

+  

+  @Extension

+  private final LogicresultFactory resultFactory = LogicresultFactory.eINSTANCE;

+  

+  @Extension

+  private final VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE;

+  

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

-    final long transformationTime = (_currentTimeMillis - transformationStart);

-    final VampireModel vampireProblem = result.getOutput();

-    final Logic2VampireLanguageMapperTrace forwardTrace = result.getTrace();

-    String fileURI = null;

-    String vampireCode = null;

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

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

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

-    if (writeFile) {

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

+    try {

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

+      final long transformationTime = (_currentTimeMillis - transformationStart);

+      final VampireModel vampireProblem = result.getOutput();

+      final Logic2VampireLanguageMapperTrace forwardTrace = result.getTrace();

+      String fileURI = null;

+      String vampireCode = null;

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

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

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

+      if (writeFile) {

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

+      }

+      if (vampireConfig.genModel) {

+        if (vampireConfig.server) {

+          final String form = this.support.makeForm(vampireCode, vampireConfig.solver, vampireConfig.runtimeLimit);

+          ArrayList<String> response = CollectionLiterals.<String>newArrayList();

+          int ind = 0;

+          boolean done = false;

+          InputOutput.<String>print(" ");

+          while ((!done)) {

+            {

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

+              done = false;

+              response = this.support.sendPost(form);

+              boolean responseFound = false;

+              ind = 0;

+              while ((!responseFound)) {

+                {

+                  String line = response.get(ind);

+                  if (((line.length() >= 5) && Objects.equal(line.substring(0, 5), "ERROR"))) {

+                    done = false;

+                    responseFound = true;

+                  } else {

+                    boolean _equals = Objects.equal(line, "</PRE>");

+                    if (_equals) {

+                      done = true;

+                      responseFound = true;

+                    }

+                  }

+                  ind++;

+                }

+              }

+            }

+          }

+          final String satRaw = response.get((ind - 3));

+          final String modRaw = response.get((ind - 2));

+          final ArrayList<String> sat = CollectionLiterals.<String>newArrayList(satRaw.split(" "));

+          final ArrayList<String> mod = CollectionLiterals.<String>newArrayList(modRaw.split(" "));

+          final String satOut = sat.get(1);

+          final String modOut = mod.get(1);

+          final String satTime = sat.get(2);

+          final String modTime = mod.get(2);

+          InputOutput.println();

+          InputOutput.<ArrayList<String>>println(sat);

+          InputOutput.<ArrayList<String>>println(mod);

+          ModelResult _createModelResult = this.resultFactory.createModelResult();

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

+            it.setProblem(null);

+            EList<Object> _representation = it.getRepresentation();

+            VampireModel _createVampireModel = this.factory.createVampireModel();

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

+            };

+            VampireModel _doubleArrow = ObjectExtensions.<VampireModel>operator_doubleArrow(_createVampireModel, _function_1);

+            _representation.add(_doubleArrow);

+            it.setTrace(it.getTrace());

+            Statistics _createStatistics = this.resultFactory.createStatistics();

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

+              it_1.setTransformationTime(((int) transformationTime));

+              EList<StatisticEntry> _entries = it_1.getEntries();

+              StringStatisticEntry _createStringStatisticEntry = this.resultFactory.createStringStatisticEntry();

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

+                it_2.setName("satOut");

+                it_2.setValue(satOut);

+              };

+              StringStatisticEntry _doubleArrow_1 = ObjectExtensions.<StringStatisticEntry>operator_doubleArrow(_createStringStatisticEntry, _function_3);

+              _entries.add(_doubleArrow_1);

+              EList<StatisticEntry> _entries_1 = it_1.getEntries();

+              RealStatisticEntry _createRealStatisticEntry = this.resultFactory.createRealStatisticEntry();

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

+                it_2.setName("satTime");

+                it_2.setValue(Double.parseDouble(satTime));

+              };

+              RealStatisticEntry _doubleArrow_2 = ObjectExtensions.<RealStatisticEntry>operator_doubleArrow(_createRealStatisticEntry, _function_4);

+              _entries_1.add(_doubleArrow_2);

+              EList<StatisticEntry> _entries_2 = it_1.getEntries();

+              StringStatisticEntry _createStringStatisticEntry_1 = this.resultFactory.createStringStatisticEntry();

+              final Procedure1<StringStatisticEntry> _function_5 = (StringStatisticEntry it_2) -> {

+                it_2.setName("modOut");

+                it_2.setValue(modOut);

+              };

+              StringStatisticEntry _doubleArrow_3 = ObjectExtensions.<StringStatisticEntry>operator_doubleArrow(_createStringStatisticEntry_1, _function_5);

+              _entries_2.add(_doubleArrow_3);

+              EList<StatisticEntry> _entries_3 = it_1.getEntries();

+              RealStatisticEntry _createRealStatisticEntry_1 = this.resultFactory.createRealStatisticEntry();

+              final Procedure1<RealStatisticEntry> _function_6 = (RealStatisticEntry it_2) -> {

+                it_2.setName("modTime");

+                it_2.setValue(Double.parseDouble(modTime));

+              };

+              RealStatisticEntry _doubleArrow_4 = ObjectExtensions.<RealStatisticEntry>operator_doubleArrow(_createRealStatisticEntry_1, _function_6);

+              _entries_3.add(_doubleArrow_4);

+            };

+            Statistics _doubleArrow_1 = ObjectExtensions.<Statistics>operator_doubleArrow(_createStatistics, _function_2);

+            it.setStatistics(_doubleArrow_1);

+          };

+          return ObjectExtensions.<ModelResult>operator_doubleArrow(_createModelResult, _function);

+        } else {

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

+    } catch (Throwable _e) {

+      throw Exceptions.sneakyThrow(_e);

     }

-    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 dd66e910..c094872e 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
@@ -11,7 +11,9 @@ public class VampireSolverConfiguration extends LogicSolverConfiguration {
   

   public int iteration = (-1);

   

-  public BackendSolver solver = BackendSolver.VAMP;

+  public BackendSolver solver = BackendSolver.VAMPIRE;

   

   public boolean genModel = true;

+  

+  public boolean server = false;

 }

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin
index 8d2ec6ab..8b7f031e 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 515b4b3c..1b6e8f80 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 46ad8c79..f523f1af 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 169aedc2..30ba1843 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 699ce6e2..174c7362 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 799515d4..affa3754 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 2a112ae7..6c7c7522 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 7f32e055..5be67889 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 a2dd469b..192c9d1a 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 98c355ab..0495ab53 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 246c08c8..c438f1e5 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 9e55bac4..5fb9b455 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 bc39a068..c09d929e 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
@@ -55,13 +55,13 @@ public class Logic2VampireLanguageMapper_ScopeMapper {
   public void _transformScope(final List<Type> types, final VampireSolverConfiguration config, final Logic2VampireLanguageMapperTrace trace) {

     int elemsInIM = trace.definedElement2String.size();

     final int ABSOLUTE_MIN = 0;

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

+    final int ABSOLUTE_MAX = (Integer.MAX_VALUE - elemsInIM);

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

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

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

     final boolean consistant = (GLOBAL_MAX > GLOBAL_MIN);

     if ((GLOBAL_MIN != ABSOLUTE_MIN)) {

-      this.getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, (!consistant));

+      this.getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, consistant);

       if (consistant) {

         for (final VLSConstant i : trace.uniqueInstances) {

           localInstances.add(this.support.duplicate(i));

@@ -72,7 +72,7 @@ public class Logic2VampireLanguageMapper_ScopeMapper {
       }

     }

     if ((GLOBAL_MAX != ABSOLUTE_MAX)) {

-      this.getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, consistant);

+      this.getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, (!consistant));

       if (consistant) {

         this.makeFofFormula(((ArrayList) trace.uniqueInstances), trace, false, null);

       } else {

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 dae0df6e..1255b25c 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
@@ -1,5 +1,6 @@
 package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder;

 

+import ca.mcgill.ecse.dslreasoner.vampire.reasoner.BackendSolver;

 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;

@@ -29,6 +30,12 @@ import java.util.Collection;
 import java.util.HashMap;

 import java.util.List;

 import java.util.Map;

+import java.util.concurrent.TimeUnit;

+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.xtend2.lib.StringConcatenation;

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

@@ -421,4 +428,85 @@ public class Logic2VampireLanguageMapper_Support {
     };

     return ObjectExtensions.<HashMap<Variable, VLSVariable>>operator_doubleArrow(_hashMap, _function);

   }

+  

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

+    String _header = this.getHeader();

+    String _plus = (_header + formula);

+    String _addOptions = this.addOptions();

+    String _plus_1 = (_plus + _addOptions);

+    String _addSolver = this.addSolver(solver, time);

+    String _plus_2 = (_plus_1 + _addSolver);

+    String _addEnd = this.addEnd();

+    return (_plus_2 + _addEnd);

+  }

+  

+  public ArrayList<String> getSolverSpecs(final BackendSolver solver) {

+    if (solver != null) {

+      switch (solver) {

+        case CVC4:

+          return CollectionLiterals.<String>newArrayList("CVC4---SAT-1.7", "do_CVC4 %s %d SAT");

+        case DARWINFM:

+          return CollectionLiterals.<String>newArrayList("DarwinFM---1.4.5", "darwin -fd true -ppp true -pl 0 -to %d -pmtptp true %s");

+        case EDARWIN:

+          return CollectionLiterals.<String>newArrayList("E-Darwin---1.5", "e-darwin -pev \"TPTP\" -pmd true -if tptp -pl 2 -pc false -ps false %s");

+        case GEOIII:

+          return CollectionLiterals.<String>newArrayList("Geo-III---2018C", "geo -tptp_input -nonempty -include /home/tptp/TPTP -inputfile %s");

+        case IPROVER:

+          return CollectionLiterals.<String>newArrayList("iProver---SAT-3.0", "iproveropt_run_sat.sh %d %s");

+        case PARADOX:

+          return CollectionLiterals.<String>newArrayList("Paradox---4.0", "paradox --no-progress --time %d --tstp --model %s");

+        case VAMPIRE:

+          return CollectionLiterals.<String>newArrayList("Vampire---SAT-4.4", "vampire --mode casc_sat -t %d %s");

+        case Z3:

+          return CollectionLiterals.<String>newArrayList("Z3---4.4.1", "run_z3_tptp -proof -model -t:20 -file:%s");

+        default:

+          break;

+      }

+    }

+    return null;

+  }

+  

+  public 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 String addSpec(final String spec) {

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

+  }

+  

+  public 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 String addSolver(final BackendSolver solver, final int time) {

+    final ArrayList<String> solverSpecs = this.getSolverSpecs(solver);

+    final String ID = solverSpecs.get(0);

+    final String cmd = solverSpecs.get(1);

+    String _replace = cmd.replace("%d", Integer.valueOf(time).toString());

+    String _plus = ((((((("------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") + _replace);

+    return (_plus + "\r\n");

+  }

+  

+  public String addEnd() {

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

+  }

+  

+  public ArrayList<String> sendPost(final String formData) throws Exception {

+    final OkHttpClient client = new OkHttpClient.Builder().connectTimeout(350, TimeUnit.SECONDS).readTimeout(350, TimeUnit.SECONDS).build();

+    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 CollectionLiterals.<String>newArrayList(response.body().string().split("\n"));

+  }

 }

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 fcbdfde7..e32530cb 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
@@ -41,7 +41,7 @@ public class VampireHandler {
       long startTime = (-((long) 1));

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

       Process p = null;

-      boolean _equals = Objects.equal(configuration.solver, BackendSolver.VAMP);

+      boolean _equals = Objects.equal(configuration.solver, BackendSolver.VAMPIRE);

       if (_equals) {

         String OPTION = " --mode casc_sat ";

         if ((configuration.runtimeLimit != (-1))) {

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 5225fb89..26ed10e3 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,65 +26,6 @@ import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl
 import org.eclipse.viatra.query.runtime.api.IQueryGroup

 

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

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 c35b200e..9121367b 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,6 +1,7 @@
 package ca.mcgill.ecse.dslreasoner.vampire.icse

 

 import ca.mcgill.ecse.dslreasoner.vampire.queries.Patterns

+import ca.mcgill.ecse.dslreasoner.vampire.reasoner.BackendSolver

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

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

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

@@ -11,6 +12,8 @@ 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.RealStatisticEntry

+import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.StringStatisticEntry

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

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

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

@@ -32,10 +35,11 @@ class YakinduTest {
 

                 // Workspace setup

                 val Date date = new Date(System.currentTimeMillis)

-                val SimpleDateFormat format = new SimpleDateFormat("MMdd-HHmmss");

+                val SimpleDateFormat format = new SimpleDateFormat("dd-HHmm");

                 val formattedDate = format.format(date)

 

                 val inputs = new FileSystemWorkspace('''initialModels/''', "")

+                val dataWorkspace = new FileSystemWorkspace('''output/YakinduTest/''', "")

                 val workspace = new FileSystemWorkspace('''output/YakinduTest/''' + formattedDate + '''/''', "")

                 workspace.initAndClear

 

@@ -55,89 +59,120 @@ class YakinduTest {
 //              val queries = null

                 println("DSL loaded")

 

-                var SZ_TOP = 10

-                var SZ_BOT = 126

-                var INC = 1

+                var SZ_TOP = 30

+                var SZ_BOT = 5

+                var INC = 5

                 var REPS = 1

-                

-                val RANGE = 3

 

-                val EXACT = 10

+                val RUNTIME = 20

+

+                val EXACT = -1

                 if (EXACT != -1) {

                         SZ_TOP = EXACT

                         SZ_BOT = EXACT

                         INC = 1

-                        REPS = 1

+                        REPS = 10

                 }

+                val BACKENDSOLVERS = newArrayList(

+//                      BackendSolver::CVC4

+//                      , 

+//                      BackendSolver::DARWINFM

+//                      , 

+//                      BackendSolver::EDARWIN

+//                      ,                       

+//                      BackendSolver::GEOIII

+//                      , 

+                        BackendSolver::IPROVER

+//                      , 

+//                      BackendSolver::PARADOX

+//                      , 

+//                      BackendSolver::VAMPIRE

+//                      ,

+//                      BackendSolver::Z3

+                        )

+                

 

-                var writer = new PrintWriter(workspace.workspaceURI + "//_yakinduStats.csv")

-                writer.append("size,")

-                for (var x = 0; x < REPS; x++) {

-                        writer.append("tTransf" + x + "," + "tSolv" + x + ",")

+                var str = ""

+

+                for (solver : BACKENDSOLVERS) {

+                        str += solver.name.substring(0, 1)

                 }

-                writer.append("medSolv,medTransf\n")

+

+                var writer = new PrintWriter(

+                        dataWorkspace.workspaceURI + "//_stats" + formattedDate + "-" + str + SZ_BOT + "to" + SZ_TOP + "by" + INC +

+                                "x" + REPS + ".csv")

+                writer.append("solver,size,transTime,sat?,satTime,model?,modelTime\n")

                 var solverTimes = newArrayList

                 var transformationTimes = newArrayList

-                var modelFound = true

                 var LogicResult solution = null

-                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

-                        transformationTimes.clear

-                        modelFound = true

-                        for (var j = 0; j < REPS; j++) {

 

-                                print(j)

+                for (BESOLVER : BACKENDSOLVERS) {

 

-                                val modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, new Ecore2LogicConfiguration())

-                                var modelExtensionProblem = instanceModel2Logic.transform(modelGenerationProblem, partialModel)

-                                var validModelExtensionProblem = viatra2Logic.transformQueries(queries, modelExtensionProblem,

-                                        new Viatra2LogicConfiguration)

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

+                                val num = (i - SZ_BOT) / INC

+                                println()

+                                println("SOLVER: " + BESOLVER.name + ", SIZE=" + i)

+                                println()

 

-                                var problem = modelGenerationProblem.output

-                                workspace.writeModel(problem, "Yakindu.logicproblem")

+                                solverTimes.clear

+                                transformationTimes.clear

+                                for (var j = 0; j < REPS; j++) {

 

+                                        print("<<Run number " + j + ">> :")

+

+                                        val modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel,

+                                                new Ecore2LogicConfiguration())

+                                        var modelExtensionProblem = instanceModel2Logic.transform(modelGenerationProblem, partialModel)

+                                        var validModelExtensionProblem = viatra2Logic.transformQueries(queries, modelExtensionProblem,

+                                                new Viatra2LogicConfiguration)

+

+                                        var problem = modelGenerationProblem.output

+//                              workspace.writeModel(problem, "Yakindu.logicproblem")

 //                               println("Problem created")

 //                               Start Time

-                                var startTime = System.currentTimeMillis

-

-                                var VampireSolver reasoner

-                                // *

-                                reasoner = new VampireSolver

-

-                                // /////////////////////////////////////////////////////

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

-                                // Maximum Scope

-                        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

-                                val iter = j

-                                val vampireConfig = new VampireSolverConfiguration => [

-                                        // add configuration things, in config file first

-                                        it.documentationLevel = DocumentationLevel::FULL

-                                        it.iteration = iter

-                                        it.runtimeLimit = 60

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

+                                        var startTime = System.currentTimeMillis

+

+                                        var VampireSolver reasoner

+                                        // *

+                                        reasoner = new VampireSolver

+

+                                        // /////////////////////////////////////////////////////

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

+                                        // Maximum Scope

+                                        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

+                                        val iter = j

+                                        val vampireConfig = new VampireSolverConfiguration => [

+                                                // add configuration things, in config file first

+                                                it.documentationLevel = DocumentationLevel::FULL

+                                                it.iteration = iter

+                                                it.runtimeLimit = RUNTIME

+//                                      it.typeScopes.maxNewElements = size

+                                                it.typeScopes.minNewElements = size

+

+                                                it.genModel = true

+                                                it.server = true

+                                                it.solver = BESOLVER

+

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

 //                              println(soln.confirmations)

@@ -145,20 +180,35 @@ class YakinduTest {
 //                              modelFound = !soln.confirmations.filter [

 //                                      class == VLSFiniteModelImpl

 //                              ].isEmpty

-//

-//                              if (modelFound) {

-                                val tTime = solution.statistics.transformationTime / 1000.0

-                                val sTime = solution.statistics.solverTime / 1000.0

-                                writer.append(tTime + "," + sTime + ",")

-                                print("(" + tTime + "/" + sTime + "s)..")

-                                solverTimes.add(sTime)

-                                transformationTimes.add(tTime)

+//      ADD TO CSV

+                                        writer.append(vampireConfig.solver.name + ",")

+                                        writer.append(size + ",")

+                                        writer.append(solution.statistics.transformationTime / 1000.0 + ",")

+

+                                        val satOut = (solution.statistics.entries.filter[name == "satOut"].get(0) as StringStatisticEntry).

+                                                value

+                                        val satTime = (solution.statistics.entries.filter[name == "satTime"].get(0) as RealStatisticEntry).

+                                                value

+                                        val modOut = (solution.statistics.entries.filter[name == "modOut"].get(0) as StringStatisticEntry).

+                                                value

+                                        val modTime = (solution.statistics.entries.filter[name == "modTime"].get(0) as RealStatisticEntry).

+                                                value

+

+                                        writer.append(satOut + ",")

+                                        writer.append(satTime + ",")

+                                        writer.append(modOut + ",")

+                                        writer.append(modTime + ",")

+                                        writer.append("\n")

+

+//                              print("(" + tTime + "/" + sTime + "s)..")

+//                              solverTimes.add(sTime)

+//                              transformationTimes.add(tTime)

 //                              } else {

 //                                      writer.append("MNF" + ",")

 ////                                    print("MNF")

 //                              }

-                        // println("Problem solved")

-                        // visualisation, see 

+                                // println("Problem solved")

+                                // visualisation, see 

 //                              var interpretations = reasoner.getInterpretations(solution as ModelResult)

 //                       for (interpretation : interpretations) {

 //                       val model = logic2Ecore.transformInterpretation(interpretation, modelGenerationProblem.trace)

@@ -168,15 +218,15 @@ class YakinduTest {
 //                       var totalTimeSec = ((System.currentTimeMillis - startTime) / 1000) % 60

 //                       println("Problem solved")

 //                       println("Time was: " + totalTimeMin + ":" + totalTimeSec)

+                                }

+//                      println()

+//                      var solverMed = solverTimes.sort.get(REPS / 2)

+//                      var transformationMed = transformationTimes.sort.get(REPS / 2)

+//                      writer.append(solverMed.toString + "," + transformationMed.toString)

                         }

-                        println()

-                        var solverMed = solverTimes.sort.get(REPS / 2)

-                        var transformationMed = transformationTimes.sort.get(REPS / 2)

-                        writer.append(solverMed.toString + "," + transformationMed.toString)

-                        writer.append("\n")

+

                 }

                 writer.close

-

         }

 

 }

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 93d27b4d..5dc01040 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 bc2bae6f..e96cf904 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 5687258f..688908b9 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 de68a908..0d18615c 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 16a3cd03..cf52d6a6 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/GeneralTest.java b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.java
index ce057092..bdea5746 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,11 +13,6 @@ 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;

@@ -33,75 +28,12 @@ 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) -> {

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 3a8f3fb4..1837b768 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
@@ -2,12 +2,14 @@ package ca.mcgill.ecse.dslreasoner.vampire.icse;
 

 import ca.mcgill.ecse.dslreasoner.vampire.icse.GeneralTest;

 import ca.mcgill.ecse.dslreasoner.vampire.queries.Patterns;

+import ca.mcgill.ecse.dslreasoner.vampire.reasoner.BackendSolver;

 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 com.google.common.base.Objects;

 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;

@@ -17,6 +19,9 @@ 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.RealStatisticEntry;

+import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.StatisticEntry;

+import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.StringStatisticEntry;

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

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

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

@@ -37,7 +42,9 @@ 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.CollectionLiterals;

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

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

@@ -53,17 +60,20 @@ public class YakinduTest {
       final InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic();

       long _currentTimeMillis = System.currentTimeMillis();

       final Date date = new Date(_currentTimeMillis);

-      final SimpleDateFormat format = new SimpleDateFormat("MMdd-HHmmss");

+      final SimpleDateFormat format = new SimpleDateFormat("dd-HHmm");

       final String formattedDate = format.format(date);

       StringConcatenation _builder = new StringConcatenation();

       _builder.append("initialModels/");

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

       StringConcatenation _builder_1 = new StringConcatenation();

       _builder_1.append("output/YakinduTest/");

-      String _plus = (_builder_1.toString() + formattedDate);

+      final FileSystemWorkspace dataWorkspace = new FileSystemWorkspace(_builder_1.toString(), "");

       StringConcatenation _builder_2 = new StringConcatenation();

-      _builder_2.append("/");

-      String _plus_1 = (_plus + _builder_2);

+      _builder_2.append("output/YakinduTest/");

+      String _plus = (_builder_2.toString() + formattedDate);

+      StringConcatenation _builder_3 = new StringConcatenation();

+      _builder_3.append("/");

+      String _plus_1 = (_plus + _builder_3);

       final FileSystemWorkspace workspace = new FileSystemWorkspace(_plus_1, "");

       workspace.initAndClear();

       final Resource.Factory.Registry reg = Resource.Factory.Registry.INSTANCE;

@@ -75,117 +85,149 @@ 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 SZ_TOP = 10;

-      int SZ_BOT = 126;

-      int INC = 1;

+      int SZ_TOP = 30;

+      int SZ_BOT = 5;

+      int INC = 5;

       int REPS = 1;

-      final int RANGE = 3;

-      final int EXACT = 10;

+      final int RUNTIME = 20;

+      final int EXACT = (-1);

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

         SZ_TOP = EXACT;

         SZ_BOT = EXACT;

         INC = 1;

-        REPS = 1;

+        REPS = 10;

       }

-      URI _workspaceURI = workspace.getWorkspaceURI();

-      String _plus_2 = (_workspaceURI + "//_yakinduStats.csv");

-      PrintWriter writer = new PrintWriter(_plus_2);

-      writer.append("size,");

-      for (int x = 0; (x < REPS); x++) {

-        writer.append(((((("tTransf" + Integer.valueOf(x)) + ",") + "tSolv") + Integer.valueOf(x)) + ","));

+      final ArrayList<BackendSolver> BACKENDSOLVERS = CollectionLiterals.<BackendSolver>newArrayList(

+        BackendSolver.IPROVER);

+      String str = "";

+      for (final BackendSolver solver : BACKENDSOLVERS) {

+        String _str = str;

+        String _substring = solver.name().substring(0, 1);

+        str = (_str + _substring);

       }

-      writer.append("medSolv,medTransf\n");

-      ArrayList<Double> solverTimes = CollectionLiterals.<Double>newArrayList();

-      ArrayList<Double> transformationTimes = CollectionLiterals.<Double>newArrayList();

-      boolean modelFound = true;

+      URI _workspaceURI = dataWorkspace.getWorkspaceURI();

+      String _plus_2 = (_workspaceURI + "//_stats");

+      String _plus_3 = (_plus_2 + formattedDate);

+      String _plus_4 = (_plus_3 + "-");

+      String _plus_5 = (_plus_4 + str);

+      String _plus_6 = (_plus_5 + Integer.valueOf(SZ_BOT));

+      String _plus_7 = (_plus_6 + "to");

+      String _plus_8 = (_plus_7 + Integer.valueOf(SZ_TOP));

+      String _plus_9 = (_plus_8 + "by");

+      String _plus_10 = (_plus_9 + Integer.valueOf(INC));

+      String _plus_11 = (_plus_10 + 

+        "x");

+      String _plus_12 = (_plus_11 + Integer.valueOf(REPS));

+      String _plus_13 = (_plus_12 + ".csv");

+      PrintWriter writer = new PrintWriter(_plus_13);

+      writer.append("solver,size,transTime,sat?,satTime,model?,modelTime\n");

+      ArrayList<Object> solverTimes = CollectionLiterals.<Object>newArrayList();

+      ArrayList<Object> transformationTimes = CollectionLiterals.<Object>newArrayList();

       LogicResult solution = null;

-      {

-        int i = SZ_BOT;

-        boolean _while = (i <= SZ_TOP);

-        while (_while) {

-          {

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

-            solverTimes.clear();

-            transformationTimes.clear();

-            modelFound = true;

-            for (int j = 0; (j < REPS); j++) {

-              {

-                InputOutput.<Integer>print(Integer.valueOf(j));

-                Ecore2LogicConfiguration _ecore2LogicConfiguration = new Ecore2LogicConfiguration();

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

-                TracedOutput<LogicProblem, Ecore2Logic_Trace> modelExtensionProblem = instanceModel2Logic.transform(modelGenerationProblem, partialModel);

-                Viatra2LogicConfiguration _viatra2LogicConfiguration = new Viatra2LogicConfiguration();

-                TracedOutput<LogicProblem, Viatra2LogicTrace> validModelExtensionProblem = viatra2Logic.transformQueries(queries, modelExtensionProblem, _viatra2LogicConfiguration);

-                LogicProblem problem = modelGenerationProblem.getOutput();

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

-                long startTime = System.currentTimeMillis();

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

-                VampireSolverConfiguration _vampireSolverConfiguration = new VampireSolverConfiguration();

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

-                  it.documentationLevel = DocumentationLevel.FULL;

-                  it.iteration = iter;

-                  it.runtimeLimit = 60;

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

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

-                final double tTime = (_transformationTime / 1000.0);

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

-                final double sTime = (_solverTime / 1000.0);

-                String _plus_4 = (Double.valueOf(tTime) + ",");

-                String _plus_5 = (_plus_4 + Double.valueOf(sTime));

-                String _plus_6 = (_plus_5 + ",");

-                writer.append(_plus_6);

-                InputOutput.<String>print((((("(" + Double.valueOf(tTime)) + "/") + Double.valueOf(sTime)) + "s).."));

-                solverTimes.add(Double.valueOf(sTime));

-                transformationTimes.add(Double.valueOf(tTime));

+      for (final BackendSolver BESOLVER : BACKENDSOLVERS) {

+        {

+          int i = SZ_BOT;

+          boolean _while = (i <= SZ_TOP);

+          while (_while) {

+            {

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

+              InputOutput.println();

+              String _name = BESOLVER.name();

+              String _plus_14 = ("SOLVER: " + _name);

+              String _plus_15 = (_plus_14 + ", SIZE=");

+              String _plus_16 = (_plus_15 + Integer.valueOf(i));

+              InputOutput.<String>println(_plus_16);

+              InputOutput.println();

+              solverTimes.clear();

+              transformationTimes.clear();

+              for (int j = 0; (j < REPS); j++) {

+                {

+                  InputOutput.<String>print((("<<Run number " + Integer.valueOf(j)) + ">> :"));

+                  Ecore2LogicConfiguration _ecore2LogicConfiguration = new Ecore2LogicConfiguration();

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

+                  TracedOutput<LogicProblem, Ecore2Logic_Trace> modelExtensionProblem = instanceModel2Logic.transform(modelGenerationProblem, partialModel);

+                  Viatra2LogicConfiguration _viatra2LogicConfiguration = new Viatra2LogicConfiguration();

+                  TracedOutput<LogicProblem, Viatra2LogicTrace> validModelExtensionProblem = viatra2Logic.transformQueries(queries, modelExtensionProblem, _viatra2LogicConfiguration);

+                  LogicProblem problem = modelGenerationProblem.getOutput();

+                  long startTime = System.currentTimeMillis();

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

+                  VampireSolverConfiguration _vampireSolverConfiguration = new VampireSolverConfiguration();

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

+                    it.documentationLevel = DocumentationLevel.FULL;

+                    it.iteration = iter;

+                    it.runtimeLimit = RUNTIME;

+                    it.typeScopes.minNewElements = size;

+                    it.genModel = true;

+                    it.server = true;

+                    it.solver = BESOLVER;

+                    it.contCycleLevel = 5;

+                    it.uniquenessDuplicates = false;

+                  };

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

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

+                  String _name_1 = vampireConfig.solver.name();

+                  String _plus_17 = (_name_1 + ",");

+                  writer.append(_plus_17);

+                  String _plus_18 = (Integer.valueOf(size) + ",");

+                  writer.append(_plus_18);

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

+                  double _divide = (_transformationTime / 1000.0);

+                  String _plus_19 = (Double.valueOf(_divide) + ",");

+                  writer.append(_plus_19);

+                  final Function1<StatisticEntry, Boolean> _function_1 = (StatisticEntry it) -> {

+                    String _name_2 = it.getName();

+                    return Boolean.valueOf(Objects.equal(_name_2, "satOut"));

+                  };

+                  StatisticEntry _get = ((StatisticEntry[])Conversions.unwrapArray(IterableExtensions.<StatisticEntry>filter(solution.getStatistics().getEntries(), _function_1), StatisticEntry.class))[0];

+                  final String satOut = ((StringStatisticEntry) _get).getValue();

+                  final Function1<StatisticEntry, Boolean> _function_2 = (StatisticEntry it) -> {

+                    String _name_2 = it.getName();

+                    return Boolean.valueOf(Objects.equal(_name_2, "satTime"));

+                  };

+                  StatisticEntry _get_1 = ((StatisticEntry[])Conversions.unwrapArray(IterableExtensions.<StatisticEntry>filter(solution.getStatistics().getEntries(), _function_2), StatisticEntry.class))[0];

+                  final double satTime = ((RealStatisticEntry) _get_1).getValue();

+                  final Function1<StatisticEntry, Boolean> _function_3 = (StatisticEntry it) -> {

+                    String _name_2 = it.getName();

+                    return Boolean.valueOf(Objects.equal(_name_2, "modOut"));

+                  };

+                  StatisticEntry _get_2 = ((StatisticEntry[])Conversions.unwrapArray(IterableExtensions.<StatisticEntry>filter(solution.getStatistics().getEntries(), _function_3), StatisticEntry.class))[0];

+                  final String modOut = ((StringStatisticEntry) _get_2).getValue();

+                  final Function1<StatisticEntry, Boolean> _function_4 = (StatisticEntry it) -> {

+                    String _name_2 = it.getName();

+                    return Boolean.valueOf(Objects.equal(_name_2, "modTime"));

+                  };

+                  StatisticEntry _get_3 = ((StatisticEntry[])Conversions.unwrapArray(IterableExtensions.<StatisticEntry>filter(solution.getStatistics().getEntries(), _function_4), StatisticEntry.class))[0];

+                  final double modTime = ((RealStatisticEntry) _get_3).getValue();

+                  writer.append((satOut + ","));

+                  String _plus_20 = (Double.valueOf(satTime) + ",");

+                  writer.append(_plus_20);

+                  writer.append((modOut + ","));

+                  String _plus_21 = (Double.valueOf(modTime) + ",");

+                  writer.append(_plus_21);

+                  writer.append("\n");

+                }

               }

             }

-            InputOutput.println();

-            Double solverMed = IterableExtensions.<Double>sort(solverTimes).get((REPS / 2));

-            Double transformationMed = IterableExtensions.<Double>sort(transformationTimes).get((REPS / 2));

-            String _string = solverMed.toString();

-            String _plus_4 = (_string + ",");

-            String _string_1 = transformationMed.toString();

-            String _plus_5 = (_plus_4 + _string_1);

-            writer.append(_plus_5);

-            writer.append("\n");

+            int _i = i;

+            i = (_i + INC);

+            _while = (i <= SZ_TOP);

           }

-          int _i = i;

-          i = (_i + INC);

-          _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 96f343fa..b596dc1f 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 1ca8223d..e1434d74 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 5d6a9ee2..50068d97 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