Index: /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/Main.java
===================================================================
--- /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/Main.java	(revision 56)
+++ /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/Main.java	(revision 57)
@@ -1,5 +1,5 @@
 package de.uni_hildesheim.sse.trans;
 
-import org.apache.commons.cli.HelpFormatter;
+import java.io.File;
 
 import de.uni_hildesheim.sse.trans.cli.Arguments;
@@ -23,9 +23,10 @@
         
         if (arguments.isHelp()) {
-            HelpFormatter formatter = new HelpFormatter();
-            formatter.printHelp("ModelTranslator", ArgumentsParser.OPTIONS);
+            ArgumentsParser.printHelp();
         } else {
-            ModelTranslator.translate(arguments.getInputFile(), arguments.getOutputFile(), InputType.MODEL,
-                OutputType.IVML, arguments.getComment(), arguments.getVersion());
+            File destFile = arguments.getOutputFile();
+            OutputType resultType = destFile.getName().endsWith(".ivml") ? OutputType.IVML : OutputType.DIMCAS;
+            ModelTranslator.translate(arguments.getInputFile(), destFile, InputType.MODEL,
+                resultType, arguments.getComment(), arguments.getVersion());
         }
     }
Index: /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/ModelTranslator.java
===================================================================
--- /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/ModelTranslator.java	(revision 56)
+++ /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/ModelTranslator.java	(revision 57)
@@ -7,4 +7,6 @@
 
 import de.uni_hildesheim.sse.model.varModel.Project;
+import de.uni_hildesheim.sse.trans.convert.CNFConverter;
+import de.uni_hildesheim.sse.trans.convert.MaxTermConverter;
 import de.uni_hildesheim.sse.trans.in.IModelReader;
 import de.uni_hildesheim.sse.trans.in.InputType;
@@ -77,4 +79,7 @@
                 }
                 break;
+            case DIMCAS:
+                CNFConverter.convert(model, new MaxTermConverter());
+                break;
             default:
                 LOGGER.debug("Not supported input model specified.");
Index: /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/cli/ArgumentsParser.java
===================================================================
--- /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/cli/ArgumentsParser.java	(revision 56)
+++ /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/cli/ArgumentsParser.java	(revision 57)
@@ -6,4 +6,5 @@
 import org.apache.commons.cli.CommandLine;
 import org.apache.commons.cli.CommandLineParser;
+import org.apache.commons.cli.HelpFormatter;
 import org.apache.commons.cli.Option;
 import org.apache.commons.cli.OptionBuilder;
@@ -24,5 +25,5 @@
 public class ArgumentsParser {
 
-    public static final Options OPTIONS = new Options();
+    private static final Options OPTIONS = new Options();
     
     private static final String CMD_IN = "in";
@@ -105,3 +106,11 @@
         return arguments;
     }
+    
+    /**
+     * Prints out the command line options.
+     */
+    public static void printHelp() {
+        HelpFormatter formatter = new HelpFormatter();
+        formatter.printHelp("ModelTranslator", OPTIONS);
+    }
 }
Index: /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/convert/CNFConverter.java
===================================================================
--- /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/convert/CNFConverter.java	(revision 56)
+++ /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/convert/CNFConverter.java	(revision 57)
@@ -44,8 +44,5 @@
                 project.add(constraint);
             } else {
-                List<Constraint> cnfConstraints = converter.convert(constraint);
-                for (Constraint cnfConstraint : cnfConstraints) {
-                    project.add(cnfConstraint);
-                }
+                converter.convert(constraint);
             }
         }
Index: /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/convert/ICNFConvertStrategy.java
===================================================================
--- /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/convert/ICNFConvertStrategy.java	(revision 56)
+++ /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/convert/ICNFConvertStrategy.java	(revision 57)
@@ -1,5 +1,3 @@
 package de.uni_hildesheim.sse.trans.convert;
-
-import java.util.List;
 
 import de.uni_hildesheim.sse.model.varModel.Constraint;
@@ -14,7 +12,7 @@
     /**
      * Converts boolean formula into a CNF formula, which may consists of multiple disjunction terms.
+     * These constraints should be added to {@link Constraint#getTopLevelParent()}.
      * @param constraint The boolean constraint, which shall be converted.
-     * @return A list of constraints expressing the same formula.
      */
-    public List<Constraint> convert(Constraint constraint);
+    public void convert(Constraint constraint);
 }
Index: /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/convert/MaxTermConverter.java
===================================================================
--- /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/convert/MaxTermConverter.java	(revision 57)
+++ /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/convert/MaxTermConverter.java	(revision 57)
@@ -0,0 +1,49 @@
+package de.uni_hildesheim.sse.trans.convert;
+
+import java.util.Set;
+
+import de.uni_hildesheim.sse.model.cst.CSTSemanticException;
+import de.uni_hildesheim.sse.model.cst.ConstraintSyntaxTree;
+import de.uni_hildesheim.sse.model.varModel.AbstractVariable;
+import de.uni_hildesheim.sse.model.varModel.Constraint;
+import de.uni_hildesheim.sse.model.varModel.Project;
+import de.uni_hildesheim.sse.model.varModel.filter.DeclrationInConstraintFinder;
+import de.uni_hildesheim.sse.trans.Bundle;
+import de.uni_hildesheim.sse.utils.logger.EASyLoggerFactory;
+import de.uni_hildesheim.sse.utils.logger.EASyLoggerFactory.EASyLogger;
+
+/**
+ * Converts a boolean formula in a list of disjunction terms by means of
+ * <a href="http://de.wikipedia.org/wiki/Konjunktive_Normalform#Beispiel_f.C3.BCr_die_Bildung">max terms</a>.
+ * @author El-Sharkawy
+ *
+ */
+public class MaxTermConverter implements ICNFConvertStrategy {
+    private static final EASyLogger LOGGER = EASyLoggerFactory.INSTANCE.getLogger(MaxTermConverter.class, Bundle.ID);
+
+    private Project project;
+    
+    @Override
+    public void convert(Constraint constraint) {
+        project = (Project) constraint.getTopLevelParent();
+        ConstraintSyntaxTree originalConstraint = constraint.getConsSyntax();
+        DeclrationInConstraintFinder finder = new DeclrationInConstraintFinder(originalConstraint);
+        Set<AbstractVariable> declarations = finder.getDeclarations();
+        System.out.println(declarations.size());
+    }
+
+    /**
+     * Adds the given constraint to the project.
+     * @param cst The constraint to add.
+     */
+    private void addConstraint(ConstraintSyntaxTree cst) {
+        Constraint constraint = new Constraint(project);
+        try {
+            constraint.setConsSyntax(cst);
+        } catch (CSTSemanticException e) {
+            LOGGER.exception(e);
+        }
+        
+        project.add(constraint);
+    }
+}