diff --git a/.idea/workspace.xml b/.idea/workspace.xml
index 652ad034..b1b4b216 100644
--- a/.idea/workspace.xml
+++ b/.idea/workspace.xml
@@ -1,9 +1,19 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <project version="4">
   <component name="ChangeListManager">
-    <list default="true" id="75bffae6-a1ba-4ac5-852b-b5d05ec617f4" name="Default" comment="" />
-    <ignored path="$PROJECT_DIR$/out/" />
-    <option name="EXCLUDED_CONVERTED_TO_IGNORED" value="true" />
+    <list default="true" id="25289ec0-0955-483c-84aa-fe847d55afb0" name="Default" comment="">
+      <change beforePath="$PROJECT_DIR$/.idea/workspace.xml" beforeDir="false" />
+      <change beforePath="$PROJECT_DIR$/examples/kodkod/examples/tptp/ALG195.java" beforeDir="false" afterPath="$PROJECT_DIR$/examples/kodkod/examples/tptp/ALG195.java" afterDir="false" />
+      <change beforePath="$PROJECT_DIR$/examples/kodkod/examples/tptp/ALG195_1.java" beforeDir="false" afterPath="$PROJECT_DIR$/examples/kodkod/examples/tptp/ALG195_1.java" afterDir="false" />
+      <change beforePath="$PROJECT_DIR$/examples/kodkod/examples/tptp/ALG212.java" beforeDir="false" afterPath="$PROJECT_DIR$/examples/kodkod/examples/tptp/ALG212.java" afterDir="false" />
+      <change beforePath="$PROJECT_DIR$/examples/kodkod/examples/tptp/COM008.java" beforeDir="false" afterPath="$PROJECT_DIR$/examples/kodkod/examples/tptp/COM008.java" afterDir="false" />
+      <change beforePath="$PROJECT_DIR$/examples/kodkod/examples/tptp/GEO091.java" beforeDir="false" afterPath="$PROJECT_DIR$/examples/kodkod/examples/tptp/GEO091.java" afterDir="false" />
+      <change beforePath="$PROJECT_DIR$/examples/kodkod/examples/tptp/GEO092.java" beforeDir="false" afterPath="$PROJECT_DIR$/examples/kodkod/examples/tptp/GEO092.java" afterDir="false" />
+      <change beforePath="$PROJECT_DIR$/examples/kodkod/examples/tptp/GEO158.java" beforeDir="false" afterPath="$PROJECT_DIR$/examples/kodkod/examples/tptp/GEO158.java" afterDir="false" />
+      <change beforePath="$PROJECT_DIR$/examples/kodkod/examples/tptp/GEO159.java" beforeDir="false" afterPath="$PROJECT_DIR$/examples/kodkod/examples/tptp/GEO159.java" afterDir="false" />
+      <change beforePath="$PROJECT_DIR$/examples/kodkod/examples/tptp/GRA013_026.java" beforeDir="false" afterPath="$PROJECT_DIR$/examples/kodkod/examples/tptp/GRA013_026.java" afterDir="false" />
+      <change beforePath="$PROJECT_DIR$/examples/kodkod/examples/tptp/LAT258.java" beforeDir="false" afterPath="$PROJECT_DIR$/examples/kodkod/examples/tptp/LAT258.java" afterDir="false" />
+    </list>
     <option name="TRACKING_ENABLED" value="true" />
     <option name="SHOW_DIALOG" value="false" />
     <option name="HIGHLIGHT_CONFLICTS" value="true" />
@@ -12,252 +22,96 @@
   </component>
   <component name="FileEditorManager">
     <leaf SIDE_TABS_SIZE_LIMIT_KEY="300">
-      <file leaf-file-name="GEO115.java" pinned="false" current-in-tab="false">
-        <entry file="file://$PROJECT_DIR$/examples/kodkod/examples/tptp/GEO115.java">
-          <provider selected="true" editor-type-id="text-editor">
-            <state relative-caret-position="1037">
-              <caret line="71" column="57" lean-forward="false" selection-start-line="71" selection-start-column="50" selection-end-line="71" selection-end-column="57" />
-              <folding />
-            </state>
-          </provider>
-        </entry>
-      </file>
-      <file leaf-file-name="COM008.java" pinned="false" current-in-tab="false">
-        <entry file="file://$PROJECT_DIR$/examples/kodkod/examples/tptp/COM008.java">
-          <provider selected="true" editor-type-id="text-editor">
-            <state relative-caret-position="153">
-              <caret line="26" column="19" lean-forward="false" selection-start-line="26" selection-start-column="19" selection-end-line="26" selection-end-column="19" />
-              <folding />
-            </state>
-          </provider>
-        </entry>
-      </file>
-      <file leaf-file-name="GEO091.java" pinned="false" current-in-tab="false">
-        <entry file="file://$PROJECT_DIR$/examples/kodkod/examples/tptp/GEO091.java">
-          <provider selected="true" editor-type-id="text-editor">
-            <state relative-caret-position="153">
-              <caret line="14" column="13" lean-forward="false" selection-start-line="14" selection-start-column="13" selection-end-line="14" selection-end-column="13" />
-              <folding />
-            </state>
-          </provider>
-        </entry>
-      </file>
-      <file leaf-file-name="SocialGolfer.java" pinned="false" current-in-tab="false">
-        <entry file="file://$PROJECT_DIR$/examples/kodkod/examples/csp/SocialGolfer.java">
-          <provider selected="true" editor-type-id="text-editor">
-            <state relative-caret-position="136">
-              <caret line="44" column="3" lean-forward="false" selection-start-line="44" selection-start-column="3" selection-end-line="44" selection-end-column="3" />
-              <folding />
-            </state>
-          </provider>
-        </entry>
-      </file>
-      <file leaf-file-name="MagicSeries.java" pinned="false" current-in-tab="false">
-        <entry file="file://$PROJECT_DIR$/examples/kodkod/examples/csp/MagicSeries.java">
-          <provider selected="true" editor-type-id="text-editor">
-            <state relative-caret-position="1836">
-              <caret line="144" column="9" lean-forward="false" selection-start-line="144" selection-start-column="9" selection-end-line="144" selection-end-column="9" />
-              <folding />
-            </state>
-          </provider>
-        </entry>
-      </file>
-      <file leaf-file-name="Z3Solver.java" pinned="false" current-in-tab="true">
-        <entry file="file://$PROJECT_DIR$/src/kodkod/engine/satlab/Z3Solver.java">
-          <provider selected="true" editor-type-id="text-editor">
-            <state relative-caret-position="17">
-              <caret line="71" column="5" lean-forward="false" selection-start-line="71" selection-start-column="5" selection-end-line="71" selection-end-column="5" />
-              <folding />
-            </state>
-          </provider>
-        </entry>
-      </file>
-      <file leaf-file-name="Evaluator.java" pinned="false" current-in-tab="false">
-        <entry file="file://$PROJECT_DIR$/src/kodkod/engine/Evaluator.java">
-          <provider selected="true" editor-type-id="text-editor">
-            <state relative-caret-position="1700">
-              <caret line="130" column="37" lean-forward="false" selection-start-line="130" selection-start-column="37" selection-end-line="130" selection-end-column="37" />
-              <folding />
-            </state>
-          </provider>
-        </entry>
-      </file>
-      <file leaf-file-name="Translator.java" pinned="false" current-in-tab="false">
-        <entry file="file://$PROJECT_DIR$/src/kodkod/engine/fol2sat/Translator.java">
-          <provider selected="true" editor-type-id="text-editor">
-            <state relative-caret-position="1003">
-              <caret line="113" column="22" lean-forward="false" selection-start-line="113" selection-start-column="22" selection-end-line="113" selection-end-column="22" />
-              <folding />
-            </state>
-          </provider>
-        </entry>
-      </file>
-      <file leaf-file-name="LeafInterpreter.java" pinned="false" current-in-tab="false">
-        <entry file="file://$PROJECT_DIR$/src/kodkod/engine/fol2sat/LeafInterpreter.java">
+      <file leaf-file-name="LAT258.java" pinned="false" current-in-tab="true">
+        <entry file="file://$PROJECT_DIR$/examples/kodkod/examples/tptp/LAT258.java">
           <provider selected="true" editor-type-id="text-editor">
-            <state relative-caret-position="3638">
-              <caret line="258" column="0" lean-forward="false" selection-start-line="258" selection-start-column="0" selection-end-line="258" selection-end-column="0" />
-              <folding />
-            </state>
-          </provider>
-        </entry>
-      </file>
-      <file leaf-file-name="Viktor.java" pinned="false" current-in-tab="false">
-        <entry file="file://$PROJECT_DIR$/examples/kodkod/examples/alloy/Viktor.java">
-          <provider selected="true" editor-type-id="text-editor">
-            <state relative-caret-position="2295">
-              <caret line="161" column="39" lean-forward="false" selection-start-line="161" selection-start-column="39" selection-end-line="161" selection-end-column="39" />
-              <folding />
+            <state relative-caret-position="120">
+              <caret line="28" column="3" selection-start-line="28" selection-start-column="3" selection-end-line="28" selection-end-column="3" />
+              <folding>
+                <element signature="e#9211#9219#0" expanded="true" />
+              </folding>
             </state>
           </provider>
         </entry>
       </file>
     </leaf>
   </component>
-  <component name="FindInProjectRecents">
-    <findStrings>
-      <find>solver</find>
-    </findStrings>
-  </component>
   <component name="Git.Settings">
-    <option name="UPDATE_TYPE" value="REBASE" />
     <option name="RECENT_GIT_ROOT_PATH" value="$PROJECT_DIR$" />
   </component>
-  <component name="GradleLocalSettings">
-    <option name="externalProjectsViewState">
-      <projects_view />
-    </option>
-  </component>
-  <component name="IdeDocumentHistory">
-    <option name="CHANGED_PATHS">
-      <list>
-        <option value="$PROJECT_DIR$/examples/kodkod/examples/alloy/Viktor.java" />
-        <option value="$PROJECT_DIR$/examples/kodkod/examples/tptp/TOP020.java" />
-        <option value="$PROJECT_DIR$/examples/kodkod/examples/csp/MagicSeries.java" />
-        <option value="$PROJECT_DIR$/src/kodkod/engine/satlab/Z3Solver.java" />
-      </list>
-    </option>
-  </component>
-  <component name="ProjectFrameBounds" extendedState="6">
-    <option name="x" value="64" />
-    <option name="y" value="-11" />
-    <option name="width" value="1857" />
-    <option name="height" value="1092" />
-  </component>
+  <component name="ProjectLevelVcsManager" settingsEditedManually="true" />
   <component name="ProjectView">
-    <navigator currentView="ProjectPane" proportions="" version="1">
-      <flattenPackages />
-      <showMembers />
-      <showModules />
-      <showLibraryContents />
-      <hideEmptyPackages />
-      <abbreviatePackageNames />
-      <autoscrollToSource />
-      <autoscrollFromSource />
-      <sortByType />
-      <manualOrder />
+    <navigator proportions="" version="1">
       <foldersAlwaysOnTop value="true" />
     </navigator>
     <panes>
-      <pane id="ProjectPane">
+      <pane id="AndroidView" />
+      <pane id="PackagesPane">
         <subPane>
           <expand>
             <path>
-              <item name="kodkod" type="b2602c69:ProjectViewProjectNode" />
-              <item name="kodkod" type="462c0819:PsiDirectoryNode" />
-            </path>
-            <path>
-              <item name="kodkod" type="b2602c69:ProjectViewProjectNode" />
-              <item name="kodkod" type="462c0819:PsiDirectoryNode" />
-              <item name="examples" type="462c0819:PsiDirectoryNode" />
-            </path>
-            <path>
-              <item name="kodkod" type="b2602c69:ProjectViewProjectNode" />
-              <item name="kodkod" type="462c0819:PsiDirectoryNode" />
-              <item name="examples" type="462c0819:PsiDirectoryNode" />
-              <item name="examples" type="462c0819:PsiDirectoryNode" />
+              <item name="kodkodz" type="58d84e3e:PackageViewProjectNode" />
+              <item name="kodkod" type="616d4139:PackageViewModuleNode" />
             </path>
+          </expand>
+          <select />
+        </subPane>
+      </pane>
+      <pane id="ProjectPane">
+        <subPane>
+          <expand>
             <path>
-              <item name="kodkod" type="b2602c69:ProjectViewProjectNode" />
-              <item name="kodkod" type="462c0819:PsiDirectoryNode" />
-              <item name="examples" type="462c0819:PsiDirectoryNode" />
-              <item name="examples" type="462c0819:PsiDirectoryNode" />
-              <item name="alloy" type="462c0819:PsiDirectoryNode" />
+              <item name="kodkodz" type="b2602c69:ProjectViewProjectNode" />
+              <item name="kodkodz" type="462c0819:PsiDirectoryNode" />
             </path>
             <path>
-              <item name="kodkod" type="b2602c69:ProjectViewProjectNode" />
-              <item name="kodkod" type="462c0819:PsiDirectoryNode" />
-              <item name="examples" type="462c0819:PsiDirectoryNode" />
+              <item name="kodkodz" type="b2602c69:ProjectViewProjectNode" />
+              <item name="kodkodz" type="462c0819:PsiDirectoryNode" />
               <item name="examples" type="462c0819:PsiDirectoryNode" />
-              <item name="alloyinecore" type="462c0819:PsiDirectoryNode" />
             </path>
             <path>
-              <item name="kodkod" type="b2602c69:ProjectViewProjectNode" />
-              <item name="kodkod" type="462c0819:PsiDirectoryNode" />
+              <item name="kodkodz" type="b2602c69:ProjectViewProjectNode" />
+              <item name="kodkodz" type="462c0819:PsiDirectoryNode" />
               <item name="examples" type="462c0819:PsiDirectoryNode" />
               <item name="examples" type="462c0819:PsiDirectoryNode" />
-              <item name="bmc" type="462c0819:PsiDirectoryNode" />
             </path>
             <path>
-              <item name="kodkod" type="b2602c69:ProjectViewProjectNode" />
-              <item name="kodkod" type="462c0819:PsiDirectoryNode" />
+              <item name="kodkodz" type="b2602c69:ProjectViewProjectNode" />
+              <item name="kodkodz" type="462c0819:PsiDirectoryNode" />
               <item name="examples" type="462c0819:PsiDirectoryNode" />
               <item name="examples" type="462c0819:PsiDirectoryNode" />
               <item name="csp" type="462c0819:PsiDirectoryNode" />
             </path>
             <path>
-              <item name="kodkod" type="b2602c69:ProjectViewProjectNode" />
-              <item name="kodkod" type="462c0819:PsiDirectoryNode" />
+              <item name="kodkodz" type="b2602c69:ProjectViewProjectNode" />
+              <item name="kodkodz" type="462c0819:PsiDirectoryNode" />
               <item name="examples" type="462c0819:PsiDirectoryNode" />
               <item name="examples" type="462c0819:PsiDirectoryNode" />
-              <item name="sudoku" type="462c0819:PsiDirectoryNode" />
+              <item name="tptp" type="462c0819:PsiDirectoryNode" />
             </path>
             <path>
-              <item name="kodkod" type="b2602c69:ProjectViewProjectNode" />
-              <item name="kodkod" type="462c0819:PsiDirectoryNode" />
+              <item name="kodkodz" type="b2602c69:ProjectViewProjectNode" />
+              <item name="kodkodz" type="462c0819:PsiDirectoryNode" />
               <item name="examples" type="462c0819:PsiDirectoryNode" />
               <item name="examples" type="462c0819:PsiDirectoryNode" />
-              <item name="tptp" type="462c0819:PsiDirectoryNode" />
-            </path>
-            <path>
-              <item name="kodkod" type="b2602c69:ProjectViewProjectNode" />
-              <item name="kodkod" type="462c0819:PsiDirectoryNode" />
-              <item name="src" type="462c0819:PsiDirectoryNode" />
-            </path>
-            <path>
-              <item name="kodkod" type="b2602c69:ProjectViewProjectNode" />
-              <item name="kodkod" type="462c0819:PsiDirectoryNode" />
-              <item name="src" type="462c0819:PsiDirectoryNode" />
-              <item name="kodkod" type="462c0819:PsiDirectoryNode" />
+              <item name="xpose" type="462c0819:PsiDirectoryNode" />
             </path>
             <path>
-              <item name="kodkod" type="b2602c69:ProjectViewProjectNode" />
-              <item name="kodkod" type="462c0819:PsiDirectoryNode" />
-              <item name="src" type="462c0819:PsiDirectoryNode" />
-              <item name="kodkod" type="462c0819:PsiDirectoryNode" />
-              <item name="engine" type="462c0819:PsiDirectoryNode" />
+              <item name="kodkodz" type="b2602c69:ProjectViewProjectNode" />
+              <item name="Scratches and Consoles" type="1a2a3e82:ScratchProjectViewPane$MyProjectNode" />
             </path>
             <path>
-              <item name="kodkod" type="b2602c69:ProjectViewProjectNode" />
-              <item name="kodkod" type="462c0819:PsiDirectoryNode" />
-              <item name="src" type="462c0819:PsiDirectoryNode" />
-              <item name="kodkod" type="462c0819:PsiDirectoryNode" />
-              <item name="engine" type="462c0819:PsiDirectoryNode" />
-              <item name="satlab" type="462c0819:PsiDirectoryNode" />
+              <item name="kodkodz" type="b2602c69:ProjectViewProjectNode" />
+              <item name="Scratches and Consoles" type="1a2a3e82:ScratchProjectViewPane$MyProjectNode" />
+              <item name="Scratches" type="d62648e6:ScratchProjectViewPane$MyRootNode" />
             </path>
           </expand>
           <select />
         </subPane>
       </pane>
       <pane id="Scope" />
-      <pane id="Scratches" />
-      <pane id="AndroidView" />
-      <pane id="PackagesPane" />
     </panes>
   </component>
-  <component name="PropertiesComponent">
-    <property name="last_opened_file_path" value="$PROJECT_DIR$" />
-  </component>
   <component name="RunDashboard">
     <option name="ruleStates">
       <list>
@@ -270,107 +124,11 @@
       </list>
     </option>
   </component>
-  <component name="RunManager" selected="Application.MagicSeries">
-    <configuration name="GEO115" type="Application" factoryName="Application" temporary="true" nameIsGenerated="true">
-      <extension name="coverage" enabled="false" merge="false" sample_coverage="true" runner="idea">
-        <pattern>
-          <option name="PATTERN" value="kodkod.examples.tptp.*" />
-          <option name="ENABLED" value="true" />
-        </pattern>
-      </extension>
-      <option name="MAIN_CLASS_NAME" value="kodkod.examples.tptp.GEO115" />
-      <option name="VM_PARAMETERS" />
-      <option name="PROGRAM_PARAMETERS" />
-      <option name="WORKING_DIRECTORY" value="$PROJECT_DIR$" />
-      <option name="ALTERNATIVE_JRE_PATH_ENABLED" value="false" />
-      <option name="ALTERNATIVE_JRE_PATH" />
-      <option name="ENABLE_SWING_INSPECTOR" value="false" />
-      <option name="ENV_VARIABLES" />
-      <option name="PASS_PARENT_ENVS" value="true" />
-      <module name="kodkod" />
-      <envs />
-    </configuration>
-    <configuration name="MagicSeries" type="Application" factoryName="Application" temporary="true" nameIsGenerated="true">
-      <extension name="coverage" enabled="false" merge="false" sample_coverage="true" runner="idea">
-        <pattern>
-          <option name="PATTERN" value="kodkod.examples.csp.*" />
-          <option name="ENABLED" value="true" />
-        </pattern>
-      </extension>
-      <option name="MAIN_CLASS_NAME" value="kodkod.examples.csp.MagicSeries" />
-      <option name="VM_PARAMETERS" value="" />
-      <option name="PROGRAM_PARAMETERS" value="70" />
-      <option name="WORKING_DIRECTORY" value="file://$PROJECT_DIR$" />
-      <option name="ALTERNATIVE_JRE_PATH_ENABLED" value="false" />
-      <option name="ALTERNATIVE_JRE_PATH" />
-      <option name="ENABLE_SWING_INSPECTOR" value="false" />
-      <option name="ENV_VARIABLES" />
-      <option name="PASS_PARENT_ENVS" value="true" />
-      <module name="kodkod" />
-      <envs />
-    </configuration>
-    <configuration name="NQueens" type="Application" factoryName="Application" temporary="true" nameIsGenerated="true">
-      <extension name="coverage" enabled="false" merge="false" sample_coverage="true" runner="idea">
-        <pattern>
-          <option name="PATTERN" value="kodkod.examples.csp.*" />
-          <option name="ENABLED" value="true" />
-        </pattern>
-      </extension>
-      <option name="MAIN_CLASS_NAME" value="kodkod.examples.csp.NQueens" />
-      <option name="VM_PARAMETERS" value="-Xms5120m -Xss4096m" />
-      <option name="PROGRAM_PARAMETERS" value="8 int" />
-      <option name="WORKING_DIRECTORY" value="file://$PROJECT_DIR$" />
-      <option name="ALTERNATIVE_JRE_PATH_ENABLED" value="false" />
-      <option name="ALTERNATIVE_JRE_PATH" />
-      <option name="ENABLE_SWING_INSPECTOR" value="false" />
-      <option name="ENV_VARIABLES" />
-      <option name="PASS_PARENT_ENVS" value="true" />
-      <module name="kodkod" />
-      <envs />
-    </configuration>
-    <configuration name="Viktor" type="Application" factoryName="Application" temporary="true" nameIsGenerated="true">
-      <extension name="coverage" enabled="false" merge="false" sample_coverage="true" runner="idea">
-        <pattern>
-          <option name="PATTERN" value="kodkod.examples.alloy.*" />
-          <option name="ENABLED" value="true" />
-        </pattern>
-      </extension>
-      <option name="MAIN_CLASS_NAME" value="kodkod.examples.alloy.Viktor" />
-      <option name="VM_PARAMETERS" />
-      <option name="PROGRAM_PARAMETERS" />
-      <option name="WORKING_DIRECTORY" value="$PROJECT_DIR$" />
-      <option name="ALTERNATIVE_JRE_PATH_ENABLED" value="false" />
-      <option name="ALTERNATIVE_JRE_PATH" />
-      <option name="ENABLE_SWING_INSPECTOR" value="false" />
-      <option name="ENV_VARIABLES" />
-      <option name="PASS_PARENT_ENVS" value="true" />
-      <module name="kodkod" />
-      <envs />
-    </configuration>
-    <configuration default="true" type="Applet" factoryName="Applet">
-      <option name="HTML_USED" value="false" />
-      <option name="WIDTH" value="400" />
-      <option name="HEIGHT" value="300" />
-      <option name="POLICY_FILE" value="$APPLICATION_HOME_DIR$/bin/appletviewer.policy" />
-      <module />
-    </configuration>
+  <component name="RunManager">
     <configuration default="true" type="Application" factoryName="Application">
-      <extension name="coverage" enabled="false" merge="false" sample_coverage="true" runner="idea" />
-      <option name="MAIN_CLASS_NAME" />
-      <option name="VM_PARAMETERS" />
-      <option name="PROGRAM_PARAMETERS" />
       <option name="WORKING_DIRECTORY" value="$PROJECT_DIR$" />
-      <option name="ALTERNATIVE_JRE_PATH_ENABLED" value="false" />
-      <option name="ALTERNATIVE_JRE_PATH" />
-      <option name="ENABLE_SWING_INSPECTOR" value="false" />
-      <option name="ENV_VARIABLES" />
-      <option name="PASS_PARENT_ENVS" value="true" />
-      <module name="" />
-      <envs />
     </configuration>
     <configuration default="true" type="JUnit" factoryName="JUnit">
-      <extension name="coverage" enabled="false" merge="false" sample_coverage="true" runner="idea" />
-      <module name="" />
       <option name="ALTERNATIVE_JRE_PATH_ENABLED" value="false" />
       <option name="ALTERNATIVE_JRE_PATH" />
       <option name="PACKAGE_NAME" />
@@ -379,31 +137,14 @@
       <option name="TEST_OBJECT" value="class" />
       <option name="VM_PARAMETERS" value="-ea" />
       <option name="PARAMETERS" />
-      <option name="WORKING_DIRECTORY" value="$MODULE_DIR$" />
-      <option name="ENV_VARIABLES" />
+      <option name="WORKING_DIRECTORY" value="%MODULE_WORKING_DIR%" />
       <option name="PASS_PARENT_ENVS" value="true" />
       <option name="TEST_SEARCH_SCOPE">
         <value defaultName="singleModule" />
       </option>
-      <envs />
       <patterns />
     </configuration>
-    <configuration default="true" type="#org.jetbrains.idea.devkit.run.PluginConfigurationType" factoryName="Plugin">
-      <module name="" />
-      <option name="VM_PARAMETERS" value="-Xmx512m -Xms256m -XX:MaxPermSize=250m -ea" />
-      <option name="PROGRAM_PARAMETERS" />
-      <predefined_log_file id="idea.log" enabled="true" />
-    </configuration>
-    <configuration default="true" type="Remote" factoryName="Remote">
-      <option name="USE_SOCKET_TRANSPORT" value="true" />
-      <option name="SERVER_MODE" value="false" />
-      <option name="SHMEM_ADDRESS" value="javadebug" />
-      <option name="HOST" value="localhost" />
-      <option name="PORT" value="5005" />
-    </configuration>
     <configuration default="true" type="TestNG" factoryName="TestNG">
-      <extension name="coverage" enabled="false" merge="false" sample_coverage="true" runner="idea" />
-      <module name="" />
       <option name="ALTERNATIVE_JRE_PATH_ENABLED" value="false" />
       <option name="ALTERNATIVE_JRE_PATH" />
       <option name="SUITE_NAME" />
@@ -414,454 +155,463 @@
       <option name="TEST_OBJECT" value="CLASS" />
       <option name="VM_PARAMETERS" value="-ea" />
       <option name="PARAMETERS" />
-      <option name="WORKING_DIRECTORY" value="$MODULE_DIR$" />
+      <option name="WORKING_DIRECTORY" value="%MODULE_WORKING_DIR%" />
       <option name="OUTPUT_DIRECTORY" />
-      <option name="ANNOTATION_TYPE" />
-      <option name="ENV_VARIABLES" />
       <option name="PASS_PARENT_ENVS" value="true" />
       <option name="TEST_SEARCH_SCOPE">
         <value defaultName="singleModule" />
       </option>
       <option name="USE_DEFAULT_REPORTERS" value="false" />
       <option name="PROPERTIES_FILE" />
-      <envs />
       <properties />
       <listeners />
     </configuration>
-    <list size="4">
-      <item index="0" class="java.lang.String" itemvalue="Application.NQueens" />
-      <item index="1" class="java.lang.String" itemvalue="Application.Viktor" />
-      <item index="2" class="java.lang.String" itemvalue="Application.GEO115" />
-      <item index="3" class="java.lang.String" itemvalue="Application.MagicSeries" />
-    </list>
-    <recent_temporary>
-      <list size="4">
-        <item index="0" class="java.lang.String" itemvalue="Application.MagicSeries" />
-        <item index="1" class="java.lang.String" itemvalue="Application.GEO115" />
-        <item index="2" class="java.lang.String" itemvalue="Application.Viktor" />
-        <item index="3" class="java.lang.String" itemvalue="Application.NQueens" />
-      </list>
-    </recent_temporary>
   </component>
-  <component name="ShelveChangesManager" show_recycled="false">
-    <option name="remove_strategy" value="false" />
+  <component name="SvnConfiguration">
+    <configuration />
   </component>
   <component name="TaskManager">
     <task active="true" id="Default" summary="Default task">
-      <changelist id="75bffae6-a1ba-4ac5-852b-b5d05ec617f4" name="Default" comment="" />
-      <created>1531387795749</created>
+      <changelist id="cdf86ea0-63a3-4a3f-88f0-c05ab74326c3" name="Default" comment="" />
+      <created>1527187479827</created>
       <option name="number" value="Default" />
       <option name="presentableId" value="Default" />
-      <updated>1531387795749</updated>
+      <updated>1527187479827</updated>
+    </task>
+    <task id="LOCAL-00001" summary="Upperbounds of Binary Relations are simplified.">
+      <created>1527634297491</created>
+      <option name="number" value="00001" />
+      <option name="presentableId" value="LOCAL-00001" />
+      <option name="project" value="LOCAL" />
+      <updated>1527634297491</updated>
+    </task>
+    <task id="LOCAL-00002" summary="The Theory of List example is simplified.">
+      <created>1527635219402</created>
+      <option name="number" value="00002" />
+      <option name="presentableId" value="LOCAL-00002" />
+      <option name="project" value="LOCAL" />
+      <updated>1527635219402</updated>
+    </task>
+    <task id="LOCAL-00003" summary="The Theory of List example is simplified.">
+      <created>1527667563201</created>
+      <option name="number" value="00003" />
+      <option name="presentableId" value="LOCAL-00003" />
+      <option name="project" value="LOCAL" />
+      <updated>1527667563201</updated>
+    </task>
+    <task id="LOCAL-00004" summary="The line to comment to get a SAT answer is showned.">
+      <created>1528118183300</created>
+      <option name="number" value="00004" />
+      <option name="presentableId" value="LOCAL-00004" />
+      <option name="project" value="LOCAL" />
+      <updated>1528118183300</updated>
     </task>
     <servers />
   </component>
   <component name="ToolWindowManager">
-    <frame x="56" y="-11" width="1865" height="1092" extended-state="6" />
+    <frame x="0" y="26" width="1920" height="1053" extended-state="6" />
+    <editor active="true" />
     <layout>
-      <window_info id="Palette" active="false" anchor="right" auto_hide="false" internal_type="DOCKED" type="DOCKED" visible="false" show_stripe_button="true" weight="0.33" sideWeight="0.5" order="3" side_tool="false" content_ui="tabs" />
-      <window_info id="TODO" active="false" anchor="bottom" auto_hide="false" internal_type="DOCKED" type="DOCKED" visible="false" show_stripe_button="true" weight="0.33" sideWeight="0.5" order="6" side_tool="false" content_ui="tabs" />
-      <window_info id="Tool Output" active="false" anchor="bottom" auto_hide="false" internal_type="DOCKED" type="DOCKED" visible="false" show_stripe_button="true" weight="0.33" sideWeight="0.5" order="7" side_tool="false" content_ui="tabs" />
-      <window_info id="Palette&#9;" active="false" anchor="right" auto_hide="false" internal_type="DOCKED" type="DOCKED" visible="false" show_stripe_button="true" weight="0.33" sideWeight="0.5" order="3" side_tool="false" content_ui="tabs" />
-      <window_info id="Image Layers" active="false" anchor="left" auto_hide="false" internal_type="DOCKED" type="DOCKED" visible="false" show_stripe_button="true" weight="0.33" sideWeight="0.5" order="2" side_tool="false" content_ui="tabs" />
-      <window_info id="Capture Analysis" active="false" anchor="right" auto_hide="false" internal_type="DOCKED" type="DOCKED" visible="false" show_stripe_button="true" weight="0.33" sideWeight="0.5" order="3" side_tool="false" content_ui="tabs" />
-      <window_info id="Event Log" active="false" anchor="bottom" auto_hide="false" internal_type="DOCKED" type="DOCKED" visible="false" show_stripe_button="true" weight="0.33" sideWeight="0.5" order="7" side_tool="true" content_ui="tabs" />
-      <window_info id="Maven Projects" active="false" anchor="right" auto_hide="false" internal_type="DOCKED" type="DOCKED" visible="false" show_stripe_button="true" weight="0.33" sideWeight="0.5" order="3" side_tool="false" content_ui="tabs" />
-      <window_info id="Run" active="false" anchor="bottom" auto_hide="false" internal_type="DOCKED" type="DOCKED" visible="false" show_stripe_button="true" weight="0.6548387" sideWeight="0.5" order="2" side_tool="false" content_ui="tabs" />
-      <window_info id="Version Control" active="false" anchor="bottom" auto_hide="false" internal_type="DOCKED" type="DOCKED" visible="false" show_stripe_button="true" weight="0.33" sideWeight="0.5" order="7" side_tool="false" content_ui="tabs" />
-      <window_info id="Terminal" active="false" anchor="bottom" auto_hide="false" internal_type="DOCKED" type="DOCKED" visible="false" show_stripe_button="true" weight="0.33" sideWeight="0.5" order="7" side_tool="false" content_ui="tabs" />
-      <window_info id="Capture Tool" active="false" anchor="left" auto_hide="false" internal_type="DOCKED" type="DOCKED" visible="false" show_stripe_button="true" weight="0.33" sideWeight="0.5" order="2" side_tool="false" content_ui="tabs" />
-      <window_info id="Designer" active="false" anchor="left" auto_hide="false" internal_type="DOCKED" type="DOCKED" visible="false" show_stripe_button="true" weight="0.33" sideWeight="0.5" order="2" side_tool="false" content_ui="tabs" />
-      <window_info id="Project" active="false" anchor="left" auto_hide="false" internal_type="DOCKED" type="DOCKED" visible="true" show_stripe_button="true" weight="0.255366" sideWeight="0.5" order="0" side_tool="false" content_ui="combo" />
-      <window_info id="ANTLR Preview" active="false" anchor="bottom" auto_hide="false" internal_type="DOCKED" type="DOCKED" visible="false" show_stripe_button="true" weight="0.33" sideWeight="0.5" order="7" side_tool="false" content_ui="tabs" />
-      <window_info id="Structure" active="false" anchor="left" auto_hide="false" internal_type="DOCKED" type="DOCKED" visible="false" show_stripe_button="true" weight="0.24986242" sideWeight="0.5" order="1" side_tool="false" content_ui="tabs" />
-      <window_info id="Ant Build" active="false" anchor="right" auto_hide="false" internal_type="DOCKED" type="DOCKED" visible="false" show_stripe_button="true" weight="0.25" sideWeight="0.5" order="1" side_tool="false" content_ui="tabs" />
-      <window_info id="UI Designer" active="false" anchor="left" auto_hide="false" internal_type="DOCKED" type="DOCKED" visible="false" show_stripe_button="true" weight="0.33" sideWeight="0.5" order="2" side_tool="false" content_ui="tabs" />
-      <window_info id="Theme Preview" active="false" anchor="right" auto_hide="false" internal_type="DOCKED" type="DOCKED" visible="false" show_stripe_button="true" weight="0.33" sideWeight="0.5" order="3" side_tool="false" content_ui="tabs" />
-      <window_info id="Debug" active="false" anchor="bottom" auto_hide="false" internal_type="DOCKED" type="DOCKED" visible="false" show_stripe_button="true" weight="0.4" sideWeight="0.5" order="3" side_tool="false" content_ui="tabs" />
-      <window_info id="Favorites" active="false" anchor="left" auto_hide="false" internal_type="DOCKED" type="DOCKED" visible="false" show_stripe_button="true" weight="0.33" sideWeight="0.5" order="2" side_tool="true" content_ui="tabs" />
-      <window_info id="Cvs" active="false" anchor="bottom" auto_hide="false" internal_type="DOCKED" type="DOCKED" visible="false" show_stripe_button="true" weight="0.25" sideWeight="0.5" order="4" side_tool="false" content_ui="tabs" />
-      <window_info id="Message" active="false" anchor="bottom" auto_hide="false" internal_type="DOCKED" type="DOCKED" visible="false" show_stripe_button="true" weight="0.33" sideWeight="0.5" order="0" side_tool="false" content_ui="tabs" />
-      <window_info id="Commander" active="false" anchor="right" auto_hide="false" internal_type="DOCKED" type="DOCKED" visible="false" show_stripe_button="true" weight="0.4" sideWeight="0.5" order="0" side_tool="false" content_ui="tabs" />
-      <window_info id="Hierarchy" active="false" anchor="right" auto_hide="false" internal_type="DOCKED" type="DOCKED" visible="false" show_stripe_button="true" weight="0.25" sideWeight="0.5" order="2" side_tool="false" content_ui="combo" />
-      <window_info id="Messages" active="false" anchor="bottom" auto_hide="false" internal_type="DOCKED" type="DOCKED" visible="false" show_stripe_button="true" weight="0.33" sideWeight="0.5" order="7" side_tool="false" content_ui="tabs" />
-      <window_info id="Inspection" active="false" anchor="bottom" auto_hide="false" internal_type="DOCKED" type="DOCKED" visible="false" show_stripe_button="true" weight="0.4" sideWeight="0.5" order="5" side_tool="false" content_ui="tabs" />
-      <window_info id="Find" active="false" anchor="bottom" auto_hide="false" internal_type="DOCKED" type="DOCKED" visible="false" show_stripe_button="true" weight="0.33" sideWeight="0.5" order="1" side_tool="false" content_ui="tabs" />
+      <window_info anchor="right" id="Palette" order="3" />
+      <window_info anchor="bottom" id="TODO" order="6" />
+      <window_info anchor="right" id="Palette&#9;" order="7" />
+      <window_info id="Image Layers" order="2" />
+      <window_info anchor="right" id="Capture Analysis" order="4" />
+      <window_info anchor="bottom" id="Event Log" order="7" sideWeight="0.5063291" side_tool="true" weight="0.7542194" />
+      <window_info anchor="right" id="Maven Projects" order="6" />
+      <window_info active="true" anchor="bottom" id="Version Control" order="10" visible="true" weight="0.3263041" />
+      <window_info anchor="bottom" id="Run" order="2" sideWeight="0.49367088" weight="0.25949368" />
+      <window_info anchor="bottom" id="Terminal" order="8" weight="0.32903227" />
+      <window_info id="Capture Tool" order="6" />
+      <window_info id="Designer" order="3" />
+      <window_info content_ui="combo" id="Project" order="0" visible="true" weight="0.13340448" />
+      <window_info id="Structure" order="1" side_tool="true" weight="0.24986242" />
+      <window_info anchor="right" id="Ant Build" order="1" weight="0.25" />
+      <window_info id="UI Designer" order="4" />
+      <window_info anchor="right" id="Theme Preview" order="5" />
+      <window_info id="Favorites" order="5" side_tool="true" />
+      <window_info anchor="bottom" id="Debug" order="3" weight="0.4" />
+      <window_info anchor="right" content_ui="combo" id="Hierarchy" order="2" weight="0.25" />
+      <window_info anchor="bottom" id="Inspection" order="5" weight="0.4" />
+      <window_info anchor="bottom" id="Tool Output" order="11" />
+      <window_info anchor="right" id="Commander" order="0" weight="0.4" />
+      <window_info anchor="bottom" id="ANTLR Preview" order="9" />
+      <window_info anchor="bottom" id="Message" order="0" />
+      <window_info anchor="bottom" id="Cvs" order="4" weight="0.25" />
+      <window_info anchor="bottom" id="Find" order="1" weight="0.32911393" />
+      <window_info anchor="bottom" id="Messages" order="12" weight="0.3273495" />
     </layout>
   </component>
   <component name="VcsContentAnnotationSettings">
     <option name="myLimit" value="2678400000" />
   </component>
-  <component name="XDebuggerManager">
-    <breakpoint-manager />
-    <watches-manager />
+  <component name="VcsManagerConfiguration">
+    <ignored-roots>
+      <path value="$USER_HOME$" />
+    </ignored-roots>
+    <MESSAGE value="Upperbounds of Binary Relations are simplified." />
+    <MESSAGE value="The Theory of List example is simplified." />
+    <MESSAGE value="The line to comment to get a SAT answer is showned." />
+    <option name="LAST_COMMIT_MESSAGE" value="The line to comment to get a SAT answer is showned." />
   </component>
   <component name="editorHistoryManager">
-    <entry file="file://$PROJECT_DIR$/examples/kodkod/examples/tptp/GEO115.java">
+    <entry file="file://$PROJECT_DIR$/examples/kodkod/examples/alloy/DNACuts.java">
       <provider selected="true" editor-type-id="text-editor">
-        <state relative-caret-position="1037">
-          <caret line="71" column="57" lean-forward="false" selection-start-line="71" selection-start-column="50" selection-end-line="71" selection-end-column="57" />
-          <folding />
+        <state relative-caret-position="630">
+          <caret line="90" column="24" selection-start-line="90" selection-start-column="24" selection-end-line="90" selection-end-column="24" />
         </state>
       </provider>
     </entry>
-    <entry file="file://$PROJECT_DIR$/examples/kodkod/examples/tptp/COM008.java">
+    <entry file="file://$PROJECT_DIR$/examples/kodkod/examples/alloy/FileSystem.java">
       <provider selected="true" editor-type-id="text-editor">
-        <state relative-caret-position="153">
-          <caret line="26" column="19" lean-forward="false" selection-start-line="26" selection-start-column="19" selection-end-line="26" selection-end-column="19" />
-          <folding />
+        <state relative-caret-position="630">
+          <caret line="44" column="1" lean-forward="true" selection-start-line="26" selection-end-line="44" selection-end-column="1" />
         </state>
       </provider>
     </entry>
-    <entry file="file://$PROJECT_DIR$/examples/kodkod/examples/tptp/GEO091.java">
+    <entry file="file://$PROJECT_DIR$/examples/kodkod/examples/alloy/GroupScheduling.java">
       <provider selected="true" editor-type-id="text-editor">
-        <state relative-caret-position="153">
-          <caret line="14" column="13" lean-forward="false" selection-start-line="14" selection-start-column="13" selection-end-line="14" selection-end-column="13" />
-          <folding />
+        <state relative-caret-position="435">
+          <caret line="67" column="1" lean-forward="true" selection-start-line="49" selection-end-line="67" selection-end-column="1" />
         </state>
       </provider>
     </entry>
-    <entry file="file://$PROJECT_DIR$/examples/kodkod/examples/csp/SocialGolfer.java">
+    <entry file="file://$PROJECT_DIR$/examples/kodkod/examples/alloy/Handshake.java">
       <provider selected="true" editor-type-id="text-editor">
-        <state relative-caret-position="136">
-          <caret line="44" column="3" lean-forward="true" selection-start-line="44" selection-start-column="3" selection-end-line="44" selection-end-column="3" />
-          <folding />
+        <state relative-caret-position="600">
+          <caret line="41" column="1" lean-forward="true" selection-start-line="23" selection-end-line="41" selection-end-column="1" />
         </state>
       </provider>
     </entry>
-    <entry file="file://$PROJECT_DIR$/examples/kodkod/examples/csp/MagicSeries.java">
+    <entry file="file://$PROJECT_DIR$/examples/kodkod/examples/alloy/Hotel.java">
       <provider selected="true" editor-type-id="text-editor">
-        <state relative-caret-position="1836">
-          <caret line="144" column="9" lean-forward="true" selection-start-line="144" selection-start-column="9" selection-end-line="144" selection-end-column="9" />
-          <folding />
+        <state relative-caret-position="150">
+          <caret line="50" selection-start-line="50" selection-end-line="68" selection-end-column="1" />
         </state>
       </provider>
     </entry>
-    <entry file="file://$PROJECT_DIR$/src/kodkod/engine/Evaluator.java">
+    <entry file="file://$PROJECT_DIR$/examples/kodkod/examples/alloy/Lists.java">
       <provider selected="true" editor-type-id="text-editor">
-        <state relative-caret-position="1700">
-          <caret line="130" column="37" lean-forward="false" selection-start-line="130" selection-start-column="37" selection-end-line="130" selection-end-column="37" />
-          <folding />
+        <state relative-caret-position="90">
+          <caret line="26" selection-start-line="26" selection-end-line="44" selection-end-column="1" />
         </state>
       </provider>
     </entry>
-    <entry file="file://$PROJECT_DIR$/src/kodkod/engine/fol2sat/Translator.java">
+    <entry file="file://$PROJECT_DIR$/examples/kodkod/examples/alloy/Netconfig.java">
       <provider selected="true" editor-type-id="text-editor">
-        <state relative-caret-position="1003">
-          <caret line="113" column="22" lean-forward="false" selection-start-line="113" selection-start-column="22" selection-end-line="113" selection-end-column="22" />
-          <folding />
+        <state relative-caret-position="615">
+          <caret line="103" column="1" lean-forward="true" selection-start-line="85" selection-end-line="103" selection-end-column="1" />
         </state>
       </provider>
     </entry>
-    <entry file="file://$PROJECT_DIR$/src/kodkod/engine/fol2sat/LeafInterpreter.java">
+    <entry file="file://$PROJECT_DIR$/examples/kodkod/examples/alloy/Pigeonhole.java">
       <provider selected="true" editor-type-id="text-editor">
-        <state relative-caret-position="3638">
-          <caret line="258" column="0" lean-forward="false" selection-start-line="258" selection-start-column="0" selection-end-line="258" selection-end-column="0" />
-          <folding />
+        <state relative-caret-position="420">
+          <caret line="41" column="30" lean-forward="true" selection-start-line="41" selection-start-column="30" selection-end-line="41" selection-end-column="30" />
         </state>
       </provider>
     </entry>
-    <entry file="file://$PROJECT_DIR$/examples/kodkod/examples/alloy/Viktor.java">
+    <entry file="file://$PROJECT_DIR$/examples/kodkod/examples/alloy/RingElection.java">
       <provider selected="true" editor-type-id="text-editor">
-        <state relative-caret-position="2295">
-          <caret line="161" column="39" lean-forward="false" selection-start-line="161" selection-start-column="39" selection-end-line="161" selection-end-column="39" />
-          <folding />
+        <state relative-caret-position="705">
+          <caret line="88" column="1" lean-forward="true" selection-start-line="70" selection-end-line="88" selection-end-column="1" />
         </state>
       </provider>
     </entry>
-    <entry file="file://$PROJECT_DIR$/src/kodkod/engine/satlab/Z3Solver.java">
+    <entry file="file://$PROJECT_DIR$/examples/kodkod/examples/alloy/Toughnut.java">
       <provider selected="true" editor-type-id="text-editor">
-        <state relative-caret-position="935">
-          <caret line="71" column="5" lean-forward="false" selection-start-line="71" selection-start-column="5" selection-end-line="71" selection-end-column="5" />
-          <folding />
+        <state relative-caret-position="570">
+          <caret line="52" column="26" lean-forward="true" selection-start-line="52" selection-start-column="26" selection-end-line="52" selection-end-column="26" />
         </state>
       </provider>
     </entry>
-    <entry file="file://$PROJECT_DIR$/examples/kodkod/examples/tptp/GEO115.java">
+    <entry file="file://$PROJECT_DIR$/examples/kodkod/examples/alloy/ToyFilesystem.java">
       <provider selected="true" editor-type-id="text-editor">
-        <state relative-caret-position="1037">
-          <caret line="71" column="57" lean-forward="false" selection-start-line="71" selection-start-column="50" selection-end-line="71" selection-end-column="57" />
-          <folding />
+        <state relative-caret-position="165">
+          <caret line="44" column="15" lean-forward="true" selection-start-line="44" selection-start-column="15" selection-end-line="44" selection-end-column="15" />
         </state>
       </provider>
     </entry>
-    <entry file="file://$PROJECT_DIR$/examples/kodkod/examples/tptp/COM008.java">
+    <entry file="file://$PROJECT_DIR$/examples/kodkod/examples/alloy/ToyLists.java">
       <provider selected="true" editor-type-id="text-editor">
-        <state relative-caret-position="442">
-          <caret line="26" column="19" lean-forward="false" selection-start-line="26" selection-start-column="19" selection-end-line="26" selection-end-column="19" />
-          <folding />
+        <state relative-caret-position="405">
+          <caret line="63" column="1" lean-forward="true" selection-start-line="45" selection-end-line="63" selection-end-column="1" />
         </state>
       </provider>
     </entry>
-    <entry file="file://$PROJECT_DIR$/examples/kodkod/examples/tptp/GEO091.java">
+    <entry file="file://$PROJECT_DIR$/examples/kodkod/examples/alloy/Trees.java">
       <provider selected="true" editor-type-id="text-editor">
-        <state relative-caret-position="153">
-          <caret line="14" column="13" lean-forward="false" selection-start-line="14" selection-start-column="13" selection-end-line="14" selection-end-column="13" />
-          <folding />
+        <state relative-caret-position="165">
+          <caret line="30" selection-start-line="30" selection-end-line="48" selection-end-column="1" />
         </state>
       </provider>
     </entry>
-    <entry file="file://$PROJECT_DIR$/examples/kodkod/examples/csp/SocialGolfer.java">
+    <entry file="file://$PROJECT_DIR$/examples/kodkod/examples/alloyinecore/RequirementsModel.java">
       <provider selected="true" editor-type-id="text-editor">
-        <state relative-caret-position="748">
-          <caret line="44" column="19" lean-forward="false" selection-start-line="44" selection-start-column="19" selection-end-line="44" selection-end-column="19" />
-          <folding />
+        <state relative-caret-position="540">
+          <caret line="36" column="1" lean-forward="true" selection-start-line="18" selection-end-line="36" selection-end-column="1" />
         </state>
       </provider>
     </entry>
-    <entry file="file://$PROJECT_DIR$/examples/kodkod/examples/csp/MagicSeries.java">
+    <entry file="file://$PROJECT_DIR$/examples/kodkod/examples/alloyinecore/SimplifiedTheoryOfList.java">
       <provider selected="true" editor-type-id="text-editor">
-        <state relative-caret-position="1853">
-          <caret line="144" column="47" lean-forward="false" selection-start-line="144" selection-start-column="47" selection-end-line="144" selection-end-column="47" />
-          <folding />
+        <state relative-caret-position="555">
+          <caret line="37" column="1" lean-forward="true" selection-start-line="19" selection-end-line="37" selection-end-column="1" />
         </state>
       </provider>
     </entry>
-    <entry file="file://$PROJECT_DIR$/src/kodkod/engine/Evaluator.java">
+    <entry file="file://$PROJECT_DIR$/examples/kodkod/examples/bmc/List.java">
       <provider selected="true" editor-type-id="text-editor">
-        <state relative-caret-position="1700">
-          <caret line="130" column="37" lean-forward="false" selection-start-line="130" selection-start-column="37" selection-end-line="130" selection-end-column="37" />
-          <folding />
+        <state relative-caret-position="225">
+          <caret line="36" column="12" selection-start-line="36" selection-start-column="12" selection-end-line="36" selection-end-column="12" />
         </state>
       </provider>
     </entry>
-    <entry file="file://$PROJECT_DIR$/src/kodkod/engine/fol2sat/Translator.java">
+    <entry file="file://$PROJECT_DIR$/examples/kodkod/examples/bmc/ListCheck.java">
       <provider selected="true" editor-type-id="text-editor">
-        <state relative-caret-position="1003">
-          <caret line="113" column="22" lean-forward="false" selection-start-line="113" selection-start-column="22" selection-end-line="113" selection-end-column="22" />
-          <folding />
+        <state relative-caret-position="165">
+          <caret line="36" column="13" selection-start-line="36" selection-start-column="13" selection-end-line="36" selection-end-column="13" />
         </state>
       </provider>
     </entry>
-    <entry file="file://$PROJECT_DIR$/src/kodkod/engine/fol2sat/LeafInterpreter.java">
+    <entry file="file://$PROJECT_DIR$/examples/kodkod/examples/bmc/ListRepair.java">
       <provider selected="true" editor-type-id="text-editor">
-        <state relative-caret-position="3638">
-          <caret line="258" column="0" lean-forward="false" selection-start-line="258" selection-start-column="0" selection-end-line="258" selection-end-column="0" />
-          <folding />
+        <state relative-caret-position="330">
+          <caret line="51" selection-start-line="51" selection-end-line="51" />
         </state>
       </provider>
     </entry>
-    <entry file="file://$PROJECT_DIR$/examples/kodkod/examples/alloy/Viktor.java">
+    <entry file="file://$PROJECT_DIR$/examples/kodkod/examples/bmc/ListViz.java">
       <provider selected="true" editor-type-id="text-editor">
-        <state relative-caret-position="2295">
-          <caret line="161" column="39" lean-forward="false" selection-start-line="161" selection-start-column="39" selection-end-line="161" selection-end-column="39" />
-          <folding />
+        <state relative-caret-position="15">
+          <caret line="47" column="6" selection-start-line="47" selection-start-column="6" selection-end-line="47" selection-end-column="6" />
         </state>
       </provider>
     </entry>
-    <entry file="file://$PROJECT_DIR$/src/kodkod/engine/satlab/Z3Solver.java">
+    <entry file="file://$PROJECT_DIR$/examples/kodkod/examples/bmc/ListSynth.java">
       <provider selected="true" editor-type-id="text-editor">
-        <state relative-caret-position="1207">
-          <caret line="71" column="5" lean-forward="true" selection-start-line="71" selection-start-column="5" selection-end-line="71" selection-end-column="5" />
-          <folding />
+        <state relative-caret-position="165">
+          <caret line="43" column="13" selection-start-line="43" selection-start-column="13" selection-end-line="43" selection-end-column="13" />
         </state>
       </provider>
     </entry>
-    <entry file="file://$PROJECT_DIR$/examples/kodkod/examples/tptp/GEO115.java">
+    <entry file="file://$PROJECT_DIR$/examples/kodkod/examples/bmc/ListEncoding.java">
       <provider selected="true" editor-type-id="text-editor">
-        <state relative-caret-position="1037">
-          <caret line="71" column="57" lean-forward="false" selection-start-line="71" selection-start-column="50" selection-end-line="71" selection-end-column="57" />
-          <folding />
+        <state relative-caret-position="180">
+          <caret line="42" column="15" selection-start-line="42" selection-start-column="15" selection-end-line="42" selection-end-column="15" />
         </state>
       </provider>
     </entry>
-    <entry file="file://$PROJECT_DIR$/examples/kodkod/examples/tptp/COM008.java">
+    <entry file="file://$PROJECT_DIR$/examples/kodkod/examples/bmc/ListDebug.java">
       <provider selected="true" editor-type-id="text-editor">
-        <state relative-caret-position="442">
-          <caret line="26" column="19" lean-forward="false" selection-start-line="26" selection-start-column="19" selection-end-line="26" selection-end-column="19" />
-          <folding />
+        <state relative-caret-position="165">
+          <caret line="46" column="13" selection-start-line="46" selection-start-column="13" selection-end-line="46" selection-end-column="13" />
         </state>
       </provider>
     </entry>
-    <entry file="file://$PROJECT_DIR$/examples/kodkod/examples/csp/SocialGolfer.java">
+    <entry file="file://$PROJECT_DIR$/examples/kodkod/examples/alloyinecore/TheoryOfList.java">
       <provider selected="true" editor-type-id="text-editor">
-        <state relative-caret-position="153">
-          <caret line="44" column="19" lean-forward="false" selection-start-line="44" selection-start-column="19" selection-end-line="44" selection-end-column="19" />
-          <folding />
+        <state relative-caret-position="105">
+          <caret line="19" column="17" selection-start-line="19" selection-start-column="17" selection-end-line="19" selection-end-column="17" />
         </state>
       </provider>
     </entry>
-    <entry file="file://$PROJECT_DIR$/examples/kodkod/examples/csp/MagicSeries.java">
+    <entry file="file://$PROJECT_DIR$/examples/kodkod/examples/csp/Graph.java">
       <provider selected="true" editor-type-id="text-editor">
-        <state relative-caret-position="1853">
-          <caret line="144" column="47" lean-forward="true" selection-start-line="144" selection-start-column="47" selection-end-line="144" selection-end-column="47" />
-          <folding />
+        <state relative-caret-position="194">
+          <caret line="42" column="19" selection-start-line="42" selection-start-column="19" selection-end-line="42" selection-end-column="19" />
         </state>
       </provider>
     </entry>
-    <entry file="file://$PROJECT_DIR$/src/kodkod/engine/Evaluator.java">
+    <entry file="file://$PROJECT_DIR$/examples/kodkod/examples/csp/BlockedNQueens2.java">
       <provider selected="true" editor-type-id="text-editor">
-        <state relative-caret-position="1700">
-          <caret line="130" column="37" lean-forward="false" selection-start-line="130" selection-start-column="37" selection-end-line="130" selection-end-column="37" />
-          <folding />
+        <state relative-caret-position="240">
+          <caret line="64" column="28" lean-forward="true" selection-start-line="64" selection-start-column="28" selection-end-line="64" selection-end-column="28" />
         </state>
       </provider>
     </entry>
-    <entry file="file://$PROJECT_DIR$/src/kodkod/engine/fol2sat/Translator.java">
+    <entry file="file://$PROJECT_DIR$/examples/kodkod/examples/csp/GraphColoring2.java">
       <provider selected="true" editor-type-id="text-editor">
-        <state relative-caret-position="1003">
-          <caret line="113" column="22" lean-forward="false" selection-start-line="113" selection-start-column="22" selection-end-line="113" selection-end-column="22" />
-          <folding />
+        <state relative-caret-position="255">
+          <caret line="31" column="27" lean-forward="true" selection-start-line="31" selection-start-column="27" selection-end-line="31" selection-end-column="27" />
         </state>
       </provider>
     </entry>
-    <entry file="file://$PROJECT_DIR$/src/kodkod/engine/fol2sat/LeafInterpreter.java">
+    <entry file="file://$PROJECT_DIR$/examples/kodkod/examples/csp/GraphColoring.java">
       <provider selected="true" editor-type-id="text-editor">
-        <state relative-caret-position="4386">
-          <caret line="258" column="0" lean-forward="false" selection-start-line="258" selection-start-column="0" selection-end-line="258" selection-end-column="0" />
-          <folding />
+        <state relative-caret-position="330">
+          <caret line="66" column="1" lean-forward="true" selection-start-line="48" selection-end-line="66" selection-end-column="1" />
         </state>
       </provider>
     </entry>
-    <entry file="file://$PROJECT_DIR$/examples/kodkod/examples/alloy/Viktor.java">
+    <entry file="file://$PROJECT_DIR$/examples/kodkod/examples/csp/HamiltonianCycle2.java">
       <provider selected="true" editor-type-id="text-editor">
-        <state relative-caret-position="2295">
-          <caret line="161" column="39" lean-forward="true" selection-start-line="161" selection-start-column="39" selection-end-line="161" selection-end-column="39" />
-          <folding />
+        <state relative-caret-position="165">
+          <caret line="48" column="19" selection-start-line="48" selection-start-column="19" selection-end-line="48" selection-end-column="19" />
         </state>
       </provider>
     </entry>
-    <entry file="file://$PROJECT_DIR$/src/kodkod/engine/satlab/Z3Solver.java">
+    <entry file="file://$PROJECT_DIR$/examples/kodkod/examples/csp/HamiltonianCycle.java">
       <provider selected="true" editor-type-id="text-editor">
-        <state relative-caret-position="1071">
-          <caret line="63" column="54" lean-forward="true" selection-start-line="63" selection-start-column="54" selection-end-line="63" selection-end-column="54" />
-          <folding />
+        <state relative-caret-position="435">
+          <caret line="61" column="1" lean-forward="true" selection-start-line="43" selection-end-line="61" selection-end-column="1" />
         </state>
       </provider>
     </entry>
-    <entry file="file://$PROJECT_DIR$/examples/kodkod/examples/csp/HamiltonianCycle.java">
+    <entry file="file://$PROJECT_DIR$/examples/kodkod/examples/csp/LatinSquare.java">
       <provider selected="true" editor-type-id="text-editor">
-        <state relative-caret-position="-1077">
-          <caret line="42" column="19" lean-forward="false" selection-start-line="42" selection-start-column="19" selection-end-line="42" selection-end-column="19" />
+        <state relative-caret-position="405">
+          <caret line="44" column="1" lean-forward="true" selection-start-line="26" selection-end-line="44" selection-end-column="1" />
         </state>
       </provider>
     </entry>
-    <entry file="file://$PROJECT_DIR$/examples/kodkod/examples/alloy/Trees.java">
+    <entry file="file://$PROJECT_DIR$/examples/kodkod/examples/csp/MagicSeries.java">
       <provider selected="true" editor-type-id="text-editor">
-        <state relative-caret-position="2482">
-          <caret line="168" column="27" lean-forward="true" selection-start-line="168" selection-start-column="27" selection-end-line="168" selection-end-column="27" />
+        <state relative-caret-position="405">
+          <caret line="63" column="1" lean-forward="true" selection-start-line="45" selection-end-line="63" selection-end-column="1" />
         </state>
       </provider>
     </entry>
     <entry file="file://$PROJECT_DIR$/examples/kodkod/examples/csp/NQueens.java">
       <provider selected="true" editor-type-id="text-editor">
-        <state relative-caret-position="2873">
-          <caret line="227" column="21" lean-forward="true" selection-start-line="227" selection-start-column="21" selection-end-line="227" selection-end-column="21" />
+        <state relative-caret-position="90">
+          <caret line="408" column="4" lean-forward="true" selection-start-line="408" selection-start-column="4" selection-end-line="426" selection-end-column="5" />
         </state>
       </provider>
     </entry>
-    <entry file="file://$PROJECT_DIR$/examples/kodkod/examples/tptp/NUM374.java">
+    <entry file="file://$PROJECT_DIR$/examples/kodkod/examples/sudoku/Sudoku.java">
       <provider selected="true" editor-type-id="text-editor">
-        <state relative-caret-position="-3916">
-          <caret line="51" column="21" lean-forward="false" selection-start-line="51" selection-start-column="21" selection-end-line="51" selection-end-column="21" />
+        <state relative-caret-position="165">
+          <caret line="58" column="19" selection-start-line="58" selection-start-column="19" selection-end-line="58" selection-end-column="19" />
         </state>
       </provider>
     </entry>
-    <entry file="file://$PROJECT_DIR$/examples/kodkod/examples/tptp/NUM378.java">
+    <entry file="file://$PROJECT_DIR$/examples/kodkod/examples/sudoku/SudokuDatabase.java">
       <provider selected="true" editor-type-id="text-editor">
-        <state relative-caret-position="-2284">
-          <caret line="28" column="19" lean-forward="false" selection-start-line="28" selection-start-column="19" selection-end-line="28" selection-end-column="19" />
+        <state relative-caret-position="-330">
+          <caret line="54" column="19" selection-start-line="54" selection-start-column="19" selection-end-line="54" selection-end-column="19" />
         </state>
       </provider>
     </entry>
-    <entry file="file://$PROJECT_DIR$/examples/kodkod/examples/tptp/ALG212.java">
+    <entry file="file://$PROJECT_DIR$/examples/kodkod/examples/sudoku/SudokuParser.java">
+      <provider selected="true" editor-type-id="text-editor">
+        <state relative-caret-position="135">
+          <caret line="36" column="19" selection-start-line="36" selection-start-column="19" selection-end-line="36" selection-end-column="19" />
+        </state>
+      </provider>
+    </entry>
+    <entry file="file://$PROJECT_DIR$/examples/kodkod/examples/csp/BlockedNQueens.java">
       <provider selected="true" editor-type-id="text-editor">
-        <state relative-caret-position="300">
-          <caret line="173" column="42" lean-forward="false" selection-start-line="173" selection-start-column="42" selection-end-line="173" selection-end-column="42" />
+        <state relative-caret-position="225">
+          <caret line="63" column="28" lean-forward="true" selection-start-line="63" selection-start-column="28" selection-end-line="63" selection-end-column="28" />
         </state>
       </provider>
     </entry>
     <entry file="file://$PROJECT_DIR$/examples/kodkod/examples/alloy/Viktor.java">
       <provider selected="true" editor-type-id="text-editor">
-        <state relative-caret-position="2295">
-          <caret line="161" column="39" lean-forward="false" selection-start-line="161" selection-start-column="39" selection-end-line="161" selection-end-column="39" />
-          <folding />
+        <state relative-caret-position="-2467">
+          <caret line="32" column="19" selection-start-line="32" selection-start-column="19" selection-end-line="32" selection-end-column="19" />
         </state>
       </provider>
     </entry>
-    <entry file="file://$PROJECT_DIR$/examples/kodkod/examples/tptp/GEO115.java">
+    <entry file="file://$PROJECT_DIR$/examples/kodkod/examples/csp/SocialGolfer.java">
       <provider selected="true" editor-type-id="text-editor">
-        <state relative-caret-position="1037">
-          <caret line="71" column="57" lean-forward="false" selection-start-line="71" selection-start-column="50" selection-end-line="71" selection-end-column="57" />
-          <folding />
+        <state relative-caret-position="135">
+          <caret line="45" selection-start-line="45" selection-end-line="63" selection-end-column="1" />
         </state>
       </provider>
     </entry>
-    <entry file="file://$PROJECT_DIR$/examples/kodkod/examples/tptp/COM008.java">
+    <entry file="file://$PROJECT_DIR$/examples/kodkod/examples/tptp/ALG195_1.java">
       <provider selected="true" editor-type-id="text-editor">
-        <state relative-caret-position="153">
-          <caret line="26" column="19" lean-forward="false" selection-start-line="26" selection-start-column="19" selection-end-line="26" selection-end-column="19" />
-          <folding />
+        <state relative-caret-position="390">
+          <caret line="45" column="24" selection-start-line="45" selection-start-column="24" selection-end-line="45" selection-end-column="24" />
         </state>
       </provider>
     </entry>
-    <entry file="file://$PROJECT_DIR$/examples/kodkod/examples/csp/SocialGolfer.java">
+    <entry file="file://$PROJECT_DIR$/examples/kodkod/examples/tptp/ALG197.java">
       <provider selected="true" editor-type-id="text-editor">
-        <state relative-caret-position="136">
-          <caret line="44" column="3" lean-forward="false" selection-start-line="44" selection-start-column="3" selection-end-line="44" selection-end-column="3" />
-          <folding />
+        <state relative-caret-position="135">
+          <caret line="23" column="19" selection-start-line="23" selection-start-column="19" selection-end-line="23" selection-end-column="19" />
         </state>
       </provider>
     </entry>
-    <entry file="file://$PROJECT_DIR$/examples/kodkod/examples/tptp/TOP020.java">
+    <entry file="file://$PROJECT_DIR$/examples/kodkod/examples/tptp/ALG195.java">
       <provider selected="true" editor-type-id="text-editor">
-        <state relative-caret-position="232">
-          <caret line="319" column="57" lean-forward="false" selection-start-line="319" selection-start-column="50" selection-end-line="319" selection-end-column="57" />
+        <state relative-caret-position="135">
+          <caret line="22" selection-start-line="22" selection-end-line="40" selection-end-column="1" />
         </state>
       </provider>
     </entry>
-    <entry file="file://$PROJECT_DIR$/src/kodkod/engine/fol2sat/FOL2BoolTranslator.java">
+    <entry file="file://$PROJECT_DIR$/examples/kodkod/examples/tptp/Quasigroups7.java">
       <provider selected="true" editor-type-id="text-editor">
-        <state relative-caret-position="199">
-          <caret line="309" column="0" lean-forward="false" selection-start-line="309" selection-start-column="0" selection-end-line="309" selection-end-column="0" />
+        <state relative-caret-position="15">
+          <caret line="190" column="35" selection-start-line="190" selection-start-column="31" selection-end-line="190" selection-end-column="35" />
         </state>
       </provider>
     </entry>
-    <entry file="file://$PROJECT_DIR$/src/kodkod/engine/fol2sat/LeafInterpreter.java">
+    <entry file="file://$PROJECT_DIR$/examples/kodkod/examples/tptp/ALG212.java">
       <provider selected="true" editor-type-id="text-editor">
-        <state relative-caret-position="3638">
-          <caret line="258" column="0" lean-forward="false" selection-start-line="258" selection-start-column="0" selection-end-line="258" selection-end-column="0" />
-          <folding />
+        <state relative-caret-position="105">
+          <caret line="23" selection-start-line="23" selection-end-line="42" selection-end-column="1" />
         </state>
       </provider>
     </entry>
-    <entry file="file://$PROJECT_DIR$/src/kodkod/engine/Evaluator.java">
+    <entry file="file://$PROJECT_DIR$/examples/kodkod/examples/tptp/COM008.java">
       <provider selected="true" editor-type-id="text-editor">
-        <state relative-caret-position="1700">
-          <caret line="130" column="37" lean-forward="false" selection-start-line="130" selection-start-column="37" selection-end-line="130" selection-end-column="37" />
-          <folding />
+        <state relative-caret-position="135">
+          <caret line="27" selection-start-line="27" selection-end-line="45" selection-end-column="1" />
         </state>
       </provider>
     </entry>
-    <entry file="file://$PROJECT_DIR$/src/kodkod/engine/fol2sat/Translator.java">
+    <entry file="file://$PROJECT_DIR$/examples/kodkod/examples/tptp/GEO091.java">
       <provider selected="true" editor-type-id="text-editor">
-        <state relative-caret-position="1003">
-          <caret line="113" column="22" lean-forward="false" selection-start-line="113" selection-start-column="22" selection-end-line="113" selection-end-column="22" />
-          <folding />
+        <state relative-caret-position="390">
+          <caret line="32" column="24" selection-start-line="32" selection-start-column="24" selection-end-line="32" selection-end-column="24" />
         </state>
       </provider>
     </entry>
-    <entry file="file://$PROJECT_DIR$/examples/kodkod/examples/csp/MagicSeries.java">
+    <entry file="file://$PROJECT_DIR$/examples/kodkod/examples/tptp/GEO092.java">
       <provider selected="true" editor-type-id="text-editor">
-        <state relative-caret-position="1836">
-          <caret line="144" column="9" lean-forward="false" selection-start-line="144" selection-start-column="9" selection-end-line="144" selection-end-column="9" />
-          <folding />
+        <state relative-caret-position="405">
+          <caret line="36" column="24" selection-start-line="36" selection-start-column="24" selection-end-line="36" selection-end-column="24" />
         </state>
       </provider>
     </entry>
-    <entry file="file://$PROJECT_DIR$/src/kodkod/engine/satlab/Z3Solver.java">
+    <entry file="file://$PROJECT_DIR$/examples/kodkod/examples/tptp/GEO158.java">
       <provider selected="true" editor-type-id="text-editor">
-        <state relative-caret-position="17">
-          <caret line="71" column="5" lean-forward="false" selection-start-line="71" selection-start-column="5" selection-end-line="71" selection-end-column="5" />
-          <folding />
+        <state relative-caret-position="135">
+          <caret line="23" selection-start-line="23" selection-end-line="41" selection-end-column="1" />
         </state>
       </provider>
     </entry>
-    <entry file="file://$PROJECT_DIR$/examples/kodkod/examples/tptp/GEO091.java">
+    <entry file="file://$PROJECT_DIR$/examples/kodkod/examples/tptp/GEO115.java">
+      <provider selected="true" editor-type-id="text-editor">
+        <state relative-caret-position="135">
+          <caret line="17" column="19" selection-start-line="17" selection-start-column="19" selection-end-line="17" selection-end-column="19" />
+        </state>
+      </provider>
+    </entry>
+    <entry file="file://$PROJECT_DIR$/examples/kodkod/examples/tptp/GEO159.java">
+      <provider selected="true" editor-type-id="text-editor">
+        <state relative-caret-position="135">
+          <caret line="20" lean-forward="true" selection-start-line="20" selection-end-line="38" selection-end-column="1" />
+        </state>
+      </provider>
+    </entry>
+    <entry file="file://$PROJECT_DIR$/examples/kodkod/examples/tptp/GRA013_026.java">
+      <provider selected="true" editor-type-id="text-editor">
+        <state relative-caret-position="135">
+          <caret line="30" selection-start-line="30" selection-end-line="48" selection-end-column="1" />
+        </state>
+      </provider>
+    </entry>
+    <entry file="file://$PROJECT_DIR$/examples/kodkod/examples/tptp/LAT258.java">
       <provider selected="true" editor-type-id="text-editor">
-        <state relative-caret-position="153">
-          <caret line="14" column="13" lean-forward="false" selection-start-line="14" selection-start-column="13" selection-end-line="14" selection-end-column="13" />
-          <folding />
+        <state relative-caret-position="120">
+          <caret line="28" column="3" selection-start-line="28" selection-start-column="3" selection-end-line="28" selection-end-column="3" />
+          <folding>
+            <element signature="e#9211#9219#0" expanded="true" />
+          </folding>
         </state>
       </provider>
     </entry>
diff --git a/examples/kodkod/examples/tptp/ALG195.java b/examples/kodkod/examples/tptp/ALG195.java
index 93bafe19..745bd2fc 100644
--- a/examples/kodkod/examples/tptp/ALG195.java
+++ b/examples/kodkod/examples/tptp/ALG195.java
@@ -10,6 +10,7 @@
 import kodkod.engine.Solution;
 import kodkod.engine.Solver;
 import kodkod.engine.satlab.SATFactory;
+import kodkod.examples.ExampleMetadata;
 import kodkod.instance.Bounds;
 import kodkod.instance.Tuple;
 import kodkod.instance.TupleFactory;
@@ -19,6 +20,25 @@
  * A KK encoding of ALG195+1.p from http://www.cs.miami.edu/~tptp/
  * @author Emina Torlak
  */
+@ExampleMetadata(
+		Name = "ALG195",
+		Note = "",
+		IsCheck = true,
+		PartialModel = true,
+		BinaryRelations = 7,
+		TernaryRelations = 2,
+		NaryRelations = 0,
+		HierarchicalTypes = 0,
+		NestedRelationalJoins = 49,
+		TransitiveClosure = 0,
+		NestedQuantifiers = 0,
+		SetCardinality = 0,
+		Additions = 0,
+		Subtractions = 0,
+		Comparison = 17,
+		OrderedRelations = 0,
+		Constraints = 38
+)
 public final class ALG195 extends Quasigroups7 {
 
 	/**
diff --git a/examples/kodkod/examples/tptp/ALG195_1.java b/examples/kodkod/examples/tptp/ALG195_1.java
index ce5a12f7..a072ed69 100644
--- a/examples/kodkod/examples/tptp/ALG195_1.java
+++ b/examples/kodkod/examples/tptp/ALG195_1.java
@@ -14,6 +14,7 @@
 import kodkod.engine.Solution;
 import kodkod.engine.Solver;
 import kodkod.engine.satlab.SATFactory;
+import kodkod.examples.ExampleMetadata;
 import kodkod.instance.Bounds;
 import kodkod.instance.Instance;
 import kodkod.instance.Tuple;
@@ -25,6 +26,25 @@
  * @author emina
  *
  */
+@ExampleMetadata(
+		Name = "ALG195_1",
+		Note = "",
+		IsCheck = true,
+		PartialModel = true,
+		BinaryRelations = 7,
+		TernaryRelations = 2,
+		NaryRelations = 0,
+		HierarchicalTypes = 0,
+		NestedRelationalJoins = 80,
+		TransitiveClosure = 0,
+		NestedQuantifiers = 0,
+		SetCardinality = 0,
+		Additions = 0,
+		Subtractions = 0,
+		Comparison = 20,
+		OrderedRelations = 0,
+		Constraints = 25
+)
 public final class ALG195_1 {
 	final Relation[] e1, e2, h;
 	final Relation op1, op2, s1, s2;
diff --git a/examples/kodkod/examples/tptp/ALG212.java b/examples/kodkod/examples/tptp/ALG212.java
index 4d90703c..f3d40035 100644
--- a/examples/kodkod/examples/tptp/ALG212.java
+++ b/examples/kodkod/examples/tptp/ALG212.java
@@ -14,6 +14,7 @@
 import kodkod.engine.Solution;
 import kodkod.engine.Solver;
 import kodkod.engine.satlab.SATFactory;
+import kodkod.examples.ExampleMetadata;
 import kodkod.instance.Bounds;
 import kodkod.instance.Universe;
 
@@ -21,6 +22,25 @@
  * A KK encoding of ALG212+1.p from http://www.cs.miami.edu/~tptp/
  * @author Emina Torlak
  */
+@ExampleMetadata(
+		Name = "ALG212",
+		Note = "",
+		IsCheck = true,
+		PartialModel = false,
+		BinaryRelations = 0,
+		TernaryRelations = 0,
+		NaryRelations = 1,
+		HierarchicalTypes = 0,
+		NestedRelationalJoins = 16,
+		TransitiveClosure = 0,
+		NestedQuantifiers = 0,
+		SetCardinality = 0,
+		Additions = 0,
+		Subtractions = 0,
+		Comparison = 5,
+		OrderedRelations = 0,
+		Constraints = 6
+)
 public final class ALG212 {
 	private final Relation f;
 	
diff --git a/examples/kodkod/examples/tptp/COM008.java b/examples/kodkod/examples/tptp/COM008.java
index 75dbd3bb..3f3afd77 100644
--- a/examples/kodkod/examples/tptp/COM008.java
+++ b/examples/kodkod/examples/tptp/COM008.java
@@ -15,6 +15,7 @@
 import kodkod.engine.Solution;
 import kodkod.engine.Solver;
 import kodkod.engine.satlab.SATFactory;
+import kodkod.examples.ExampleMetadata;
 import kodkod.instance.Bounds;
 import kodkod.instance.TupleFactory;
 import kodkod.instance.TupleSet;
@@ -24,6 +25,25 @@
  * 
  * @author Emina Torlak
  */
+@ExampleMetadata(
+		Name = "COM008",
+		Note = "",
+		IsCheck = true,
+		PartialModel = false,
+		BinaryRelations = 3,
+		TernaryRelations = 0,
+		NaryRelations = 0,
+		HierarchicalTypes = 0,
+		NestedRelationalJoins = 0,
+		TransitiveClosure = 0,
+		NestedQuantifiers = 0,
+		SetCardinality = 0,
+		Additions = 0,
+		Subtractions = 0,
+		Comparison = 1,
+		OrderedRelations = 0,
+		Constraints = 14
+)
 public final class COM008 {
 	private final Relation equalish, rewrite, trr;
 	private final Relation a, b, c, goal;
diff --git a/examples/kodkod/examples/tptp/GEO091.java b/examples/kodkod/examples/tptp/GEO091.java
index fde31adf..93426abf 100644
--- a/examples/kodkod/examples/tptp/GEO091.java
+++ b/examples/kodkod/examples/tptp/GEO091.java
@@ -5,6 +5,7 @@
 import kodkod.engine.Solution;
 import kodkod.engine.Solver;
 import kodkod.engine.satlab.SATFactory;
+import kodkod.examples.ExampleMetadata;
 import kodkod.instance.Bounds;
 
 /**
@@ -12,6 +13,25 @@
  * 
  * @author Emina Torlak
  */
+@ExampleMetadata(
+		Name = "GEO091",
+		Note = "",
+		IsCheck = true,
+		PartialModel = false,
+		BinaryRelations = 4,
+		TernaryRelations = 2,
+		NaryRelations = 0,
+		HierarchicalTypes = 0,
+		NestedRelationalJoins = 4,
+		TransitiveClosure = 0,
+		NestedQuantifiers = 0,
+		SetCardinality = 0,
+		Additions = 0,
+		Subtractions = 0,
+		Comparison = 9,
+		OrderedRelations = 0,
+		Constraints = 39
+)
 public class GEO091 extends GEO158 {
 
 	/**
diff --git a/examples/kodkod/examples/tptp/GEO092.java b/examples/kodkod/examples/tptp/GEO092.java
index b7f891c7..af6f3410 100644
--- a/examples/kodkod/examples/tptp/GEO092.java
+++ b/examples/kodkod/examples/tptp/GEO092.java
@@ -9,6 +9,7 @@
 import kodkod.engine.Solution;
 import kodkod.engine.Solver;
 import kodkod.engine.satlab.SATFactory;
+import kodkod.examples.ExampleMetadata;
 import kodkod.instance.Bounds;
 
 /**
@@ -16,6 +17,25 @@
  * 
  * @author Emina Torlak
  */
+@ExampleMetadata(
+		Name = "GEO092",
+		Note = "",
+		IsCheck = true,
+		PartialModel = false,
+		BinaryRelations = 4,
+		TernaryRelations = 2,
+		NaryRelations = 0,
+		HierarchicalTypes = 0,
+		NestedRelationalJoins = 4,
+		TransitiveClosure = 0,
+		NestedQuantifiers = 0,
+		SetCardinality = 0,
+		Additions = 0,
+		Subtractions = 0,
+		Comparison = 8,
+		OrderedRelations = 0,
+		Constraints = 39
+)
 public class GEO092 extends GEO158 {
 
 	/**
diff --git a/examples/kodkod/examples/tptp/GEO158.java b/examples/kodkod/examples/tptp/GEO158.java
index ccf8a04b..8ed4cdb8 100644
--- a/examples/kodkod/examples/tptp/GEO158.java
+++ b/examples/kodkod/examples/tptp/GEO158.java
@@ -10,6 +10,7 @@
 import kodkod.engine.Solution;
 import kodkod.engine.Solver;
 import kodkod.engine.satlab.SATFactory;
+import kodkod.examples.ExampleMetadata;
 import kodkod.instance.Bounds;
 import kodkod.instance.TupleFactory;
 import kodkod.instance.TupleSet;
@@ -20,6 +21,25 @@
  * 
  * @author Emina Torlak
  */
+@ExampleMetadata(
+		Name = "GEO158",
+		Note = "",
+		IsCheck = true,
+		PartialModel = false,
+		BinaryRelations = 4,
+		TernaryRelations = 2,
+		NaryRelations = 0,
+		HierarchicalTypes = 0,
+		NestedRelationalJoins = 4,
+		TransitiveClosure = 0,
+		NestedQuantifiers = 0,
+		SetCardinality = 0,
+		Additions = 0,
+		Subtractions = 0,
+		Comparison = 8,
+		OrderedRelations = 0,
+		Constraints = 37
+)
 public class GEO158 {
 	final Relation partOf, incident, sum, endPoint, innerPoint, meet, closed, open;
 	final Relation curve, point;
@@ -27,7 +47,7 @@ public class GEO158 {
 	 * part_of		:	C -> C
 	 * incident_c	: 	P -> C
 	 * sum			:	C -> C -> one C     	 
-	 * end_point		:	P -> C
+	 * end_point	:	P -> C
 	 * inner_point	:	P -> C
 	 * meet			: 	P -> C -> C
 	 * closed		:	C
diff --git a/examples/kodkod/examples/tptp/GEO159.java b/examples/kodkod/examples/tptp/GEO159.java
index c476cdcd..70544e99 100644
--- a/examples/kodkod/examples/tptp/GEO159.java
+++ b/examples/kodkod/examples/tptp/GEO159.java
@@ -10,6 +10,7 @@
 import kodkod.engine.Solution;
 import kodkod.engine.Solver;
 import kodkod.engine.satlab.SATFactory;
+import kodkod.examples.ExampleMetadata;
 import kodkod.instance.Bounds;
 import kodkod.instance.TupleSet;
 
@@ -17,6 +18,25 @@
  * The  GEO159+1 problem from http://www.cs.miami.edu/~tptp/
  * @author Emina Torlak
  */
+@ExampleMetadata(
+		Name = "GEO159",
+		Note = "",
+		IsCheck = true,
+		PartialModel = false,
+		BinaryRelations = 4,
+		TernaryRelations = 2,
+		NaryRelations = 1,
+		HierarchicalTypes = 0,
+		NestedRelationalJoins = 4,
+		TransitiveClosure = 0,
+		NestedQuantifiers = 0,
+		SetCardinality = 0,
+		Additions = 0,
+		Subtractions = 0,
+		Comparison = 9,
+		OrderedRelations = 0,
+		Constraints = 39
+)
 public class GEO159 extends GEO158 {
 	final Relation between;
 	/*
diff --git a/examples/kodkod/examples/tptp/GRA013_026.java b/examples/kodkod/examples/tptp/GRA013_026.java
index 18a13b20..bc5d32c0 100644
--- a/examples/kodkod/examples/tptp/GRA013_026.java
+++ b/examples/kodkod/examples/tptp/GRA013_026.java
@@ -17,6 +17,7 @@
 import kodkod.engine.fol2sat.HigherOrderDeclException;
 import kodkod.engine.fol2sat.UnboundLeafException;
 import kodkod.engine.satlab.SATFactory;
+import kodkod.examples.ExampleMetadata;
 import kodkod.instance.Bounds;
 import kodkod.instance.TupleFactory;
 import kodkod.instance.TupleSet;
@@ -27,6 +28,25 @@
  * A KK encoding of GRA019+1.p through GRA026+1.p from http://www.cs.miami.edu/~tptp/
  * @author Emina Torlak
  */
+@ExampleMetadata(
+		Name = "GRA013_026",
+		Note = "",
+		IsCheck = true,
+		PartialModel = true,
+		BinaryRelations = 3,
+		TernaryRelations = 0,
+		NaryRelations = 0,
+		HierarchicalTypes = 0,
+		NestedRelationalJoins = 0,
+		TransitiveClosure = 0,
+		NestedQuantifiers = 0,
+		SetCardinality = 0,
+		Additions = 0,
+		Subtractions = 0,
+		Comparison = 0,
+		OrderedRelations = 0,
+		Constraints = 5
+)
 public final class GRA013_026 {
 	private final Relation red, green, lessThan,goal,node;
 	private final int graphSize, cliqueSize;
diff --git a/examples/kodkod/examples/tptp/LAT258.java b/examples/kodkod/examples/tptp/LAT258.java
index eb7a5d2c..1584257e 100644
--- a/examples/kodkod/examples/tptp/LAT258.java
+++ b/examples/kodkod/examples/tptp/LAT258.java
@@ -17,6 +17,7 @@
 import kodkod.engine.fol2sat.HigherOrderDeclException;
 import kodkod.engine.fol2sat.UnboundLeafException;
 import kodkod.engine.satlab.SATFactory;
+import kodkod.examples.ExampleMetadata;
 import kodkod.instance.Bounds;
 import kodkod.instance.TupleFactory;
 import kodkod.instance.TupleSet;
@@ -26,6 +27,25 @@
  * A KK encoding of LAT258+1.p from http://www.cs.miami.edu/~tptp/
  * @author Emina Torlak
  */
+@ExampleMetadata(
+		Name = "LAT258",
+		Note = "",
+		IsCheck = true,
+		PartialModel = false,
+		BinaryRelations = 1,
+		TernaryRelations = 2,
+		NaryRelations = 0,
+		HierarchicalTypes = 0,
+		NestedRelationalJoins = 10,
+		TransitiveClosure = 0,
+		NestedQuantifiers = 0,
+		SetCardinality = 0,
+		Additions = 0,
+		Subtractions = 0,
+		Comparison = 0,
+		OrderedRelations = 0,
+		Constraints = 21
+)
 public final class LAT258 {
 	private final Relation goal, p, t, u, v, w, x, y, z;
 	private final Relation lessThan, meet, join;