diff --git a/.github/scripts/linux-setup.sh b/.github/scripts/linux-setup.sh
new file mode 100755
index 00000000..f5da2497
--- /dev/null
+++ b/.github/scripts/linux-setup.sh
@@ -0,0 +1,81 @@
+# This script downloads all necessary dependencies to run the CI on Linux.
+# It can also be run locally, as long as you have the following dependencies:
+#  - python 3.1x
+#  - java
+#  - C & C++ compiler (aliased to cc and cpp commands respectively)
+#  - wget
+#  - tar
+#
+# The script takes the following positional command line parameters:
+#  1. Path to this script directory from the current working directory
+#  2. Path to the desired dependencies directory
+#  3. Boolean true/false; whether to initialize a python virtual env
+
+main() {
+  # Validate command line parameters
+  if [ $# -ne 3 ]; then
+    echo "Usage: $0 <script dir path> <desired dependency dir path> <bool: use python venv>"
+    exit 1
+  fi
+  SCRIPT_DIR="$1"
+  DEPS_DIR="$2"
+  USE_VENV=$3
+  # Print out tool version information
+  java --version
+  python --version
+  pip --version
+  cc --version
+  cpp --version
+  # Install python packages
+  if $USE_VENV; then
+    python -m venv .
+    source bin/activate
+    pip install -r "$SCRIPT_DIR/requirements.txt"
+    deactivate
+  else
+    pip install -r "$SCRIPT_DIR/requirements.txt"
+  fi
+  # Put all dependencies in their own directory to ensure they aren't included implicitly
+  mkdir -p "$DEPS_DIR"
+  # Get tree-sitter-tlaplus
+  wget -nv https://github.com/tlaplus-community/tree-sitter-tlaplus/archive/main.tar.gz -O /tmp/tree-sitter-tlaplus.tar.gz
+  tar -xzf /tmp/tree-sitter-tlaplus.tar.gz --directory "$DEPS_DIR"
+  mv "$DEPS_DIR/tree-sitter-tlaplus-main" "$DEPS_DIR/tree-sitter-tlaplus"
+  # Get TLA⁺ tools
+  mkdir -p "$DEPS_DIR/tools"
+  wget -nv http://nightly.tlapl.us/dist/tla2tools.jar -P "$DEPS_DIR/tools"
+  # Get TLA⁺ community modules
+  mkdir -p "$DEPS_DIR/community"
+  wget -nv https://github.com/tlaplus/CommunityModules/releases/latest/download/CommunityModules-deps.jar \
+        -O "$DEPS_DIR/community/modules.jar"
+  # Get TLAPS modules
+  wget -nv https://github.com/tlaplus/tlapm/archive/main.tar.gz -O /tmp/tlapm.tar.gz
+  tar -xzf /tmp/tlapm.tar.gz --directory "$DEPS_DIR"
+  mv "$DEPS_DIR/tlapm-main" "$DEPS_DIR/tlapm"
+  # Install TLAPS
+  kernel=$(uname -s)
+  if [ "$kernel" == "Linux" ]; then
+    TLAPM_BIN_TYPE=x86_64-linux-gnu
+  elif [ "$kernel" == "Darwin" ]; then
+    TLAPM_BIN_TYPE=i386-darwin
+  else
+    echo "Unknown OS: $kernel"
+    exit 1
+  fi
+  TLAPM_BIN="tlaps-1.5.0-$TLAPM_BIN_TYPE-inst.bin"
+  wget -nv "https://github.com/tlaplus/tlapm/releases/latest/download/$TLAPM_BIN" -O /tmp/tlapm-installer.bin
+  chmod +x /tmp/tlapm-installer.bin
+  # Workaround for https://github.com/tlaplus/tlapm/issues/88
+  set +e
+  for ((attempt = 1; attempt <= 5; attempt++)); do
+    rm -rf "$DEPS_DIR/tlapm-install"
+    /tmp/tlapm-installer.bin -d "$DEPS_DIR/tlapm-install"
+    if [ $? -eq 0 ]; then
+      exit 0
+    fi
+  done
+  exit 1
+}
+
+main "$@"
+
diff --git a/.github/scripts/parse_modules.py b/.github/scripts/parse_modules.py
index 7fd69c06..bc76ee17 100644
--- a/.github/scripts/parse_modules.py
+++ b/.github/scripts/parse_modules.py
@@ -16,9 +16,11 @@
 parser.add_argument('--community_modules_jar_path', help='Path to the CommunityModules-deps.jar file', required=True)
 parser.add_argument('--manifest_path', help='Path to the tlaplus/examples manifest.json file', required=True)
 parser.add_argument('--skip', nargs='+', help='Space-separated list of .tla modules to skip parsing', required=False, default=[])
+parser.add_argument('--only', nargs='+', help='If provided, only parse models in this space-separated list', required=False, default=[])
+parser.add_argument('--verbose', help='Set logging output level to debug', action='store_true')
 args = parser.parse_args()
 
-logging.basicConfig(level=logging.INFO)
+logging.basicConfig(level = logging.DEBUG if args.verbose else logging.INFO)
 
 tools_jar_path = normpath(args.tools_jar_path)
 tlaps_modules = normpath(args.tlapm_lib_path)
@@ -26,6 +28,7 @@
 manifest_path = normpath(args.manifest_path)
 examples_root = dirname(manifest_path)
 skip_modules = [normpath(path) for path in args.skip]
+only_modules = [normpath(path) for path in args.only]
 
 def parse_module(path):
     """
@@ -33,7 +36,7 @@ def parse_module(path):
     """
     logging.info(path)
     # Jar paths must go first
-    search_paths = pathsep.join([tools_jar_path, community_modules, dirname(path), tlaps_modules])
+    search_paths = pathsep.join([tools_jar_path, dirname(path), community_modules, tlaps_modules])
     sany = subprocess.run([
         'java',
         '-cp', search_paths,
@@ -41,10 +44,13 @@ def parse_module(path):
         '-error-codes',
         path
     ], capture_output=True)
-    if sany.returncode != 0:
-        logging.error(sany.stdout.decode('utf-8'))
+    output = ' '.join(sany.args) + '\n' + sany.stdout.decode('utf-8')
+    if 0 == sany.returncode:
+        logging.debug(output)
+        return True
+    else:
+        logging.error(output)
         return False
-    return True
 
 manifest = tla_utils.load_json(manifest_path)
 
@@ -54,13 +60,14 @@ def parse_module(path):
     for spec in manifest['specifications']
     for module in spec['modules']
         if normpath(module['path']) not in skip_modules
+        and (only_modules == [] or normpath(module['path']) in only_modules)
 ]
 
 for path in skip_modules:
     logging.info(f'Skipping {path}')
 
 # Parse specs in parallel
-thread_count = cpu_count()
+thread_count = cpu_count() if not args.verbose else 1
 logging.info(f'Parsing using {thread_count} threads')
 with ThreadPoolExecutor(thread_count) as executor:
     results = executor.map(parse_module, modules)
diff --git a/.github/scripts/windows-setup.sh b/.github/scripts/windows-setup.sh
new file mode 100755
index 00000000..405d4dff
--- /dev/null
+++ b/.github/scripts/windows-setup.sh
@@ -0,0 +1,56 @@
+# This script downloads all necessary dependencies to run the CI on Windows.
+# It can also be run locally, as long as you have the following dependencies:
+#  - python 3.1x
+#  - java
+#  - curl
+#  - 7-zip
+#
+# The script takes the following positional command line parameters:
+#  1. Path to this script directory from the current working directory
+#  2. Path to the desired dependencies directory
+#  3. Boolean true/false; whether to initialize a python virtual env
+
+main() {
+  # Validate command line parameters
+  if [ $# -ne 3 ]; then
+    echo "Usage: $0 <script dir path> <desired dependency dir path> <bool: use python venv>"
+    exit 1
+  fi
+  SCRIPT_DIR="$1"
+  DEPS_DIR="$2"
+  USE_VENV=$3
+  # Print out tool version information
+  java --version
+  python --version
+  pip --version
+  # Install python packages
+  if $USE_VENV; then
+    python -m venv .
+    pwsh Scripts/Activate.ps1
+    pip install -r "$SCRIPT_DIR/requirements.txt"
+    deactivate
+  else
+    pip install -r "$SCRIPT_DIR/requirements.txt"
+  fi
+  # Put all dependencies in their own directory to ensure they aren't included implicitly
+  mkdir -p "$DEPS_DIR"
+  # Get tree-sitter-tlaplus
+  curl -L https://github.com/tlaplus-community/tree-sitter-tlaplus/archive/main.zip --output tree-sitter-tlaplus.zip
+  7z x tree-sitter-tlaplus.zip
+  mv tree-sitter-tlaplus-main "$DEPS_DIR/tree-sitter-tlaplus"
+  rm tree-sitter-tlaplus.zip
+  # Get TLA⁺ tools
+  mkdir -p "$DEPS_DIR/tools"
+  curl http://nightly.tlapl.us/dist/tla2tools.jar --output "$DEPS_DIR/tools/tla2tools.jar"
+  # Get TLA⁺ community modules
+  mkdir -p "$DEPS_DIR/community"
+  curl -L https://github.com/tlaplus/CommunityModules/releases/latest/download/CommunityModules-deps.jar --output "$DEPS_DIR/community/modules.jar"
+  # Get TLAPS modules
+  curl -L https://github.com/tlaplus/tlapm/archive/main.zip --output tlapm.zip
+  7z x tlapm.zip
+  mv tlapm-main "$DEPS_DIR/tlapm"
+  rm tlapm.zip
+}
+
+main "$@"
+
diff --git a/.github/workflows/CI.yml b/.github/workflows/CI.yml
index e5e58a80..bfa62a00 100644
--- a/.github/workflows/CI.yml
+++ b/.github/workflows/CI.yml
@@ -18,11 +18,11 @@ jobs:
         include:
         - { os: windows-latest }
         - { os: ubuntu-latest }
-        - { os: macos-latest }
+        - { os: macos-14 }
       fail-fast: false
     env:
       SCRIPT_DIR: .github/scripts
-      TLAPS_VERSION: 202210041448
+      DEPS_DIR: deps
     defaults:
       run:
         shell: bash
@@ -32,93 +32,18 @@ jobs:
       - name: Install python
         uses: actions/setup-python@v5
         with:
-          python-version: '3.11'
+          python-version: '3.12'
       - name: Install Java
         uses: actions/setup-java@v4
         with:
           distribution: adopt
           java-version: 17
-      - name: Download TLA⁺ dependencies
+      - name: Download TLA⁺ dependencies (Windows)
         if: matrix.os == 'windows-latest'
-        run: |
-          # Print out tool version information
-          java --version
-          python --version
-          pip --version
-          # Install python packages
-          pip install -r $SCRIPT_DIR/requirements.txt
-          # Put all dependencies in their own directory to ensure they aren't included implicitly
-          mkdir deps
-          # Get tree-sitter-tlaplus
-          curl -LO https://github.com/tlaplus-community/tree-sitter-tlaplus/archive/main.zip
-          7z x main.zip
-          rm main.zip
-          mv tree-sitter-tlaplus-main deps/tree-sitter-tlaplus
-          # Get TLA⁺ tools
-          mkdir deps/tools
-          curl -LO http://nightly.tlapl.us/dist/tla2tools.jar
-          mv tla2tools.jar deps/tools/tla2tools.jar
-          # Get TLA⁺ community modules
-          mkdir deps/community
-          curl -LO https://github.com/tlaplus/CommunityModules/releases/latest/download/CommunityModules-deps.jar
-          mv CommunityModules-deps.jar deps/community/modules.jar
-          # Get TLAPS modules
-          curl -LO https://github.com/tlaplus/tlapm/archive/refs/tags/$TLAPS_VERSION.zip
-          7z x $TLAPS_VERSION.zip
-          rm $TLAPS_VERSION.zip
-          mv tlapm-$TLAPS_VERSION deps/tlapm
-      - name: Download TLA⁺ dependencies
+        run: $SCRIPT_DIR/windows-setup.sh $SCRIPT_DIR $DEPS_DIR false
+      - name: Download TLA⁺ dependencies (Linux & macOS)
         if: matrix.os != 'windows-latest'
-        run: |
-          # Print out tool version information
-          java --version
-          python --version
-          pip --version
-          cc --version
-          cpp --version
-          # Install python packages
-          pip install -r $SCRIPT_DIR/requirements.txt
-          # Put all dependencies in their own directory to ensure they aren't included implicitly
-          mkdir deps
-          # Get tree-sitter-tlaplus
-          wget -nv https://github.com/tlaplus-community/tree-sitter-tlaplus/archive/main.tar.gz
-          tar -xf main.tar.gz
-          rm main.tar.gz
-          mv tree-sitter-tlaplus-main deps/tree-sitter-tlaplus
-          # Get TLA⁺ tools
-          mkdir deps/tools
-          wget -nv http://nightly.tlapl.us/dist/tla2tools.jar -O deps/tools/tla2tools.jar
-          # Get TLA⁺ community modules
-          mkdir deps/community
-          wget -nv https://github.com/tlaplus/CommunityModules/releases/latest/download/CommunityModules-deps.jar \
-                -O deps/community/modules.jar
-          # Get TLAPS modules
-          wget -nv https://github.com/tlaplus/tlapm/archive/refs/tags/$TLAPS_VERSION.tar.gz
-          tar -xf $TLAPS_VERSION.tar.gz
-          rm $TLAPS_VERSION.tar.gz
-          mv tlapm-$TLAPS_VERSION deps/tlapm
-          # Install TLAPS
-          if [[ "${{ runner.os }}" == "Linux" ]]; then
-            TLAPM_BIN_TYPE=x86_64-linux-gnu
-          elif [[ "${{ runner.os }}" == "macOS" ]]; then
-            TLAPM_BIN_TYPE=i386-darwin
-          else
-            echo "Unknown OS"
-            exit 1
-          fi
-          TLAPM_BIN="tlaps-1.5.0-$TLAPM_BIN_TYPE-inst.bin"
-          wget -nv https://github.com/tlaplus/tlapm/releases/download/$TLAPS_VERSION/$TLAPM_BIN
-          chmod +x $TLAPM_BIN
-          # Workaround for https://github.com/tlaplus/tlapm/issues/88
-          set +e
-          for ((attempt = 1; attempt <= 5; attempt++)); do
-            rm -rf deps/tlapm-install
-            ./$TLAPM_BIN -d deps/tlapm-install
-            if [ $? -eq 0 ]; then
-              exit 0
-            fi
-          done
-          exit 1
+        run: $SCRIPT_DIR/linux-setup.sh $SCRIPT_DIR $DEPS_DIR false
       - name: Check manifest.json format
         run: |
           python $SCRIPT_DIR/check_manifest_schema.py \
@@ -133,7 +58,7 @@ jobs:
         run: |
           python $SCRIPT_DIR/check_manifest_features.py \
             --manifest_path manifest.json               \
-            --ts_path deps/tree-sitter-tlaplus
+            --ts_path $DEPS_DIR/tree-sitter-tlaplus
       - name: Check README spec table
         run: |
           python $SCRIPT_DIR/check_markdown_table.py  \
@@ -141,17 +66,17 @@ jobs:
             --readme_path README.md
       - name: Parse all modules
         run: |
-          python $SCRIPT_DIR/parse_modules.py                       \
-            --tools_jar_path deps/tools/tla2tools.jar               \
-            --tlapm_lib_path deps/tlapm/library                     \
-            --community_modules_jar_path deps/community/modules.jar \
+          python $SCRIPT_DIR/parse_modules.py                            \
+            --tools_jar_path $DEPS_DIR/tools/tla2tools.jar               \
+            --tlapm_lib_path $DEPS_DIR/tlapm/library                     \
+            --community_modules_jar_path $DEPS_DIR/community/modules.jar \
             --manifest_path manifest.json
       - name: Check small models
         run: |
-          python $SCRIPT_DIR/check_small_models.py                  \
-            --tools_jar_path deps/tools/tla2tools.jar               \
-            --tlapm_lib_path deps/tlapm/library                     \
-            --community_modules_jar_path deps/community/modules.jar \
+          python $SCRIPT_DIR/check_small_models.py                       \
+            --tools_jar_path $DEPS_DIR/tools/tla2tools.jar               \
+            --tlapm_lib_path $DEPS_DIR/tlapm/library                     \
+            --community_modules_jar_path $DEPS_DIR/community/modules.jar \
             --manifest_path manifest.json
       - name: Smoke-test large models
         run: |
@@ -163,11 +88,11 @@ jobs:
           if [[ "${{ runner.os }}" == "Windows" ]]; then
             SKIP+=("specifications/ewd426/SimTokenRing.cfg")
           fi
-          python $SCRIPT_DIR/smoke_test_large_models.py             \
-            --tools_jar_path deps/tools/tla2tools.jar               \
-            --tlapm_lib_path deps/tlapm/library                     \
-            --community_modules_jar_path deps/community/modules.jar \
-            --manifest_path manifest.json                           \
+          python $SCRIPT_DIR/smoke_test_large_models.py                  \
+            --tools_jar_path $DEPS_DIR/tools/tla2tools.jar               \
+            --tlapm_lib_path $DEPS_DIR/tlapm/library                     \
+            --community_modules_jar_path $DEPS_DIR/community/modules.jar \
+            --manifest_path manifest.json                                \
             --skip "${SKIP[@]}"
       - name: Check proofs
         if: matrix.os != 'windows-latest'
@@ -188,16 +113,16 @@ jobs:
             specifications/MisraReachability/ReachabilityProofs.tla
             specifications/byzpaxos/BPConProof.tla # Takes about 30 minutes
           )
-          python $SCRIPT_DIR/check_proofs.py  \
-            --tlapm_path deps/tlapm-install   \
-            --manifest_path manifest.json     \
+          python $SCRIPT_DIR/check_proofs.py       \
+            --tlapm_path $DEPS_DIR/tlapm-install   \
+            --manifest_path manifest.json          \
             --skip "${SKIP[@]}"
       - name: Smoke-test manifest generation script
         run: |
-          rm -r deps/tree-sitter-tlaplus/build
+          rm -r $DEPS_DIR/tree-sitter-tlaplus/build
           python $SCRIPT_DIR/generate_manifest.py \
             --manifest_path manifest.json         \
             --ci_ignore_path .ciignore            \
-            --ts_path deps/tree-sitter-tlaplus
+            --ts_path $DEPS_DIR/tree-sitter-tlaplus
           git diff -a
 
diff --git a/README.md b/README.md
index 653ddff1..b3bd0a5e 100644
--- a/README.md
+++ b/README.md
@@ -16,7 +16,6 @@ All specs in this repository are subject to CI validation to ensure quality.
 
 ## Examples Included Here
 Here is a list of specs included in this repository, with links to the relevant directory and flags for various features:
-<<<<<<< HEAD
 | Name                                                                                                | Author(s)                                           | Beginner | TLAPS Proof | PlusCal | TLC Model | Apalache |
 | --------------------------------------------------------------------------------------------------- | --------------------------------------------------- | :------: | :---------: | :-----: | :-------: | :------: |
 | [Teaching Concurrency](specifications/TeachingConcurrency)                                          | Leslie Lamport                                      |    ✔     |      ✔      |    ✔    |     ✔     |          |
diff --git a/manifest.json b/manifest.json
index e953ce0d..5e54c820 100644
--- a/manifest.json
+++ b/manifest.json
@@ -4220,6 +4220,15 @@
             }
           ]
         },
+        {
+          "path": "specifications/ewd998/TLAPS.tla",
+          "communityDependencies": [],
+          "tlaLanguageVersion": 2,
+          "features": [
+            "proof"
+          ],
+          "models": []
+        },
         {
           "path": "specifications/ewd998/Utils.tla",
           "communityDependencies": [
@@ -4683,4 +4692,4 @@
       ]
     }
   ]
-}
+}
\ No newline at end of file
diff --git a/specifications/ewd998/.gitignore b/specifications/ewd998/.gitignore
deleted file mode 100644
index 620eaaea..00000000
--- a/specifications/ewd998/.gitignore
+++ /dev/null
@@ -1,15 +0,0 @@
-EWD998.toolbox/EWD998___Model_1_SnapShot_*.launch
-EWD998.toolbox/Model_1*/
-EWD998Chan.toolbox/EWD998Chan___Model_1_SnapShot_*.launch
-EWD998Chan.toolbox/Model_1*/
-_apalache-out
-EWD998_*/
-FiniteSetsExt.tla
-FiniteSetTheorems.tla
-Folds.tla
-Functions.tla
-FunctionTheorems.tla
-NaturalsInduction.tla
-SequencesExt.tla
-TLAPS.tla
-WellFoundedInduction.tla
diff --git a/specifications/ewd998/TLAPS.tla b/specifications/ewd998/TLAPS.tla
new file mode 100644
index 00000000..e83bb97d
--- /dev/null
+++ b/specifications/ewd998/TLAPS.tla
@@ -0,0 +1,468 @@
+------------------------------- MODULE TLAPS --------------------------------
+
+(* Backend pragmas. *)
+
+
+(***************************************************************************)
+(* Each of these pragmas can be cited with a BY or a USE.  The pragma that *)
+(* is added to the context of an obligation most recently is the one whose *)
+(* effects are triggered.                                                  *)
+(***************************************************************************)
+
+(***************************************************************************)
+(* The following pragmas should be used only as a last resource.  They are *)
+(* dependent upon the particular backend provers, and are unlikely to have *)
+(* any effect if the set of backend provers changes.  Moreover, they are   *)
+(* meaningless to a reader of the proof.                                   *)
+(***************************************************************************)
+
+
+(**************************************************************************)
+(* Backend pragma: use the SMT solver for arithmetic.                     *)
+(*                                                                        *)
+(* This method exists under this name for historical reasons.             *)
+(**************************************************************************)
+
+SimpleArithmetic == TRUE (*{ by (prover:"smt3") }*)
+
+
+(**************************************************************************)
+(* Backend pragma: SMT solver                                             *)
+(*                                                                        *)
+(* This method translates the proof obligation to SMTLIB2. The supported  *)
+(* fragment includes first-order logic, set theory, functions and         *)
+(* records.                                                               *)
+(* SMT calls the smt-solver with the default timeout of 5 seconds         *)
+(* while SMTT(n) calls the smt-solver with a timeout of n seconds.        *)
+(**************************************************************************)
+
+SMT == TRUE (*{ by (prover:"smt3") }*)
+SMTT(X) == TRUE (*{ by (prover:"smt3"; timeout:@) }*)
+
+
+(**************************************************************************)
+(* Backend pragma: CVC4 SMT solver                                        *)
+(*                                                                        *)
+(* These methods translate the proof obligation to SMTLIB2 and call CVC4. *)
+(**************************************************************************)
+
+(* The CVC3* methods are here for backward compatibility. They call CVC4. *)
+CVC3 == TRUE (*{ by (prover: "cvc33") }*)
+CVC3T(X) == TRUE (*{ by (prover:"cvc33"; timeout:@) }*)
+
+CVC4 == TRUE (*{ by (prover: "cvc33") }*)
+CVC4T(X) == TRUE (*{ by (prover:"cvc33"; timeout:@) }*)
+
+
+(**************************************************************************)
+(* Backend pragma: Yices SMT solver                                       *)
+(*                                                                        *)
+(* This method translates the proof obligation to Yices native language.  *)
+(**************************************************************************)
+
+Yices == TRUE (*{ by (prover: "yices3") }*)
+YicesT(X) == TRUE (*{ by (prover:"yices3"; timeout:@) }*)
+
+(**************************************************************************)
+(* Backend pragma: veriT SMT solver                                       *)
+(*                                                                        *)
+(* This method translates the proof obligation to SMTLIB2 and calls veriT.*)
+(**************************************************************************)
+
+veriT == TRUE (*{ by (prover: "verit") }*)
+veriTT(X) == TRUE (*{ by (prover:"verit"; timeout:@) }*)
+
+(**************************************************************************)
+(* Backend pragma: Z3 SMT solver                                          *)
+(*                                                                        *)
+(* This method translates the proof obligation to SMTLIB2 and calls Z3.   *)
+(* Z3 is used by default but you can also explicitly call it.             *)
+(**************************************************************************)
+
+Z3 == TRUE (*{ by (prover: "z33") }*)
+Z3T(X) == TRUE (*{ by (prover:"z33"; timeout:@) }*)
+
+(**************************************************************************)
+(* Backend pragma: SPASS superposition prover                             *)
+(*                                                                        *)
+(* This method translates the proof obligation to the DFG format language *)
+(* supported by the ATP SPASS. The translation is based on the SMT one.   *)
+(**************************************************************************)
+
+Spass == TRUE (*{ by (prover: "spass") }*)
+SpassT(X) == TRUE (*{ by (prover:"spass"; timeout:@) }*)
+
+(**************************************************************************)
+(* Backend pragma: The PTL propositional linear time temporal logic       *)
+(* prover.  It currently is the LS4 backend.                              *)
+(*                                                                        *)
+(* This method translates the negetation of the proof obligation to       *)
+(* Seperated Normal Form (TRP++ format) and checks for unsatisfiability   *)
+(**************************************************************************)
+
+LS4 == TRUE (*{ by (prover: "ls4") }*)
+LS4T(X) == TRUE (*{ by (prover: "ls4"; timeout:@) }*)
+PTL == TRUE (*{ by (prover: "ls4") }*)
+
+(**************************************************************************)
+(* Backend pragma: Zenon with different timeouts (default is 10 seconds)  *)
+(*                                                                        *)
+(**************************************************************************)
+
+Zenon == TRUE (*{ by (prover:"zenon") }*)
+ZenonT(X) == TRUE (*{ by (prover:"zenon"; timeout:@) }*)
+
+(********************************************************************)
+(* Backend pragma: Isabelle with different timeouts and tactics     *)
+(*  (default is 30 seconds/auto)                                    *)
+(********************************************************************)
+
+Isa == TRUE (*{ by (prover:"isabelle") }*)
+IsaT(X) ==  TRUE (*{ by (prover:"isabelle"; timeout:@) }*)
+IsaM(X) ==  TRUE (*{ by (prover:"isabelle"; tactic:@) }*)
+IsaMT(X,Y) ==  TRUE (*{ by (prover:"isabelle"; tactic:@; timeout:@) }*)
+
+(***************************************************************************)
+(* The following theorem expresses the (useful implication of the) law of  *)
+(* set extensionality, which can be written as                             *)
+(*                                                                         *)
+(*    THEOREM  \A S, T : (S = T) <=> (\A x : (x \in S) <=> (x \in T))      *)
+(*                                                                         *)
+(* Theorem SetExtensionality is sometimes required by the SMT backend for  *)
+(* reasoning about sets. It is usually counterproductive to include        *)
+(* theorem SetExtensionality in a BY clause for the Zenon or Isabelle      *)
+(* backends. Instead, use the pragma IsaWithSetExtensionality to instruct  *)
+(* the Isabelle backend to use the rule of set extensionality.             *)
+(***************************************************************************)
+IsaWithSetExtensionality == TRUE
+           (*{ by (prover:"isabelle"; tactic:"(auto intro: setEqualI)")}*)
+
+THEOREM SetExtensionality == \A S,T : (\A x : x \in S <=> x \in T) => S = T
+OBVIOUS
+
+(***************************************************************************)
+(* The following theorem is needed to deduce NotInSetS \notin SetS from    *)
+(* the definition                                                          *)
+(*                                                                         *)
+(*   NotInSetS == CHOOSE v : v \notin SetS                                 *)
+(***************************************************************************)
+THEOREM NoSetContainsEverything == \A S : \E x : x \notin S
+OBVIOUS (*{by (isabelle "(auto intro: inIrrefl)")}*)
+-----------------------------------------------------------------------------
+
+
+
+(********************************************************************)
+(********************************************************************)
+(********************************************************************)
+
+
+(********************************************************************)
+(* Old versions of Zenon and Isabelle pragmas below                 *)
+(* (kept for compatibility)                                         *)
+(********************************************************************)
+
+
+(**************************************************************************)
+(* Backend pragma: Zenon with different timeouts (default is 10 seconds)  *)
+(*                                                                        *)
+(**************************************************************************)
+
+SlowZenon == TRUE (*{ by (prover:"zenon"; timeout:20) }*)
+SlowerZenon == TRUE (*{ by (prover:"zenon"; timeout:40) }*)
+VerySlowZenon == TRUE (*{ by (prover:"zenon"; timeout:80) }*)
+SlowestZenon == TRUE (*{ by (prover:"zenon"; timeout:160) }*)
+
+
+
+(********************************************************************)
+(* Backend pragma: Isabelle's automatic search ("auto")             *)
+(*                                                                  *)
+(* This pragma bypasses Zenon. It is useful in situations involving *)
+(* essentially simplification and equational reasoning.             *)
+(* Default imeout for all isabelle tactics is 30 seconds.           *)
+(********************************************************************)
+Auto == TRUE (*{ by (prover:"isabelle"; tactic:"auto") }*)
+SlowAuto == TRUE (*{ by (prover:"isabelle"; tactic:"auto"; timeout:120) }*)
+SlowerAuto == TRUE (*{ by (prover:"isabelle"; tactic:"auto"; timeout:480) }*)
+SlowestAuto == TRUE (*{ by (prover:"isabelle"; tactic:"auto"; timeout:960) }*)
+
+(********************************************************************)
+(* Backend pragma: Isabelle's "force" tactic                        *)
+(*                                                                  *)
+(* This pragma bypasses Zenon. It is useful in situations involving *)
+(* quantifier reasoning.                                            *)
+(********************************************************************)
+Force == TRUE (*{ by (prover:"isabelle"; tactic:"force") }*)
+SlowForce == TRUE (*{ by (prover:"isabelle"; tactic:"force"; timeout:120) }*)
+SlowerForce == TRUE (*{ by (prover:"isabelle"; tactic:"force"; timeout:480) }*)
+SlowestForce == TRUE (*{ by (prover:"isabelle"; tactic:"force"; timeout:960) }*)
+
+(***********************************************************************)
+(* Backend pragma: Isabelle's "simplification" tactics                 *)
+(*                                                                     *)
+(* These tactics simplify the goal before running one of the automated *)
+(* tactics. They are often necessary for obligations involving record  *)
+(* or tuple projections. Use the SimplfyAndSolve tactic unless you're  *)
+(* sure you can get away with just Simplification                      *)
+(***********************************************************************)
+SimplifyAndSolve        == TRUE
+    (*{ by (prover:"isabelle"; tactic:"clarsimp auto?") }*)
+SlowSimplifyAndSolve    == TRUE
+    (*{ by (prover:"isabelle"; tactic:"clarsimp auto?"; timeout:120) }*)
+SlowerSimplifyAndSolve  == TRUE
+    (*{ by (prover:"isabelle"; tactic:"clarsimp auto?"; timeout:480) }*)
+SlowestSimplifyAndSolve == TRUE
+    (*{ by (prover:"isabelle"; tactic:"clarsimp auto?"; timeout:960) }*)
+
+Simplification == TRUE (*{ by (prover:"isabelle"; tactic:"clarsimp") }*)
+SlowSimplification == TRUE
+    (*{ by (prover:"isabelle"; tactic:"clarsimp"; timeout:120) }*)
+SlowerSimplification  == TRUE
+    (*{ by (prover:"isabelle"; tactic:"clarsimp"; timeout:480) }*)
+SlowestSimplification == TRUE
+    (*{ by (prover:"isabelle"; tactic:"clarsimp"; timeout:960) }*)
+
+(**************************************************************************)
+(* Backend pragma: Isabelle's tableau prover ("blast")                    *)
+(*                                                                        *)
+(* This pragma bypasses Zenon and uses Isabelle's built-in theorem        *)
+(* prover, Blast. It is almost never better than Zenon by itself, but     *)
+(* becomes very useful in combination with the Auto pragma above. The     *)
+(* AutoBlast pragma first attempts Auto and then uses Blast to prove what *)
+(* Auto could not prove. (There is currently no way to use Zenon on the   *)
+(* results left over from Auto.)                                          *)
+(**************************************************************************)
+Blast == TRUE (*{ by (prover:"isabelle"; tactic:"blast") }*)
+SlowBlast == TRUE (*{ by (prover:"isabelle"; tactic:"blast"; timeout:120) }*)
+SlowerBlast == TRUE (*{ by (prover:"isabelle"; tactic:"blast"; timeout:480) }*)
+SlowestBlast == TRUE (*{ by (prover:"isabelle"; tactic:"blast"; timeout:960) }*)
+
+AutoBlast == TRUE (*{ by (prover:"isabelle"; tactic:"auto, blast") }*)
+
+
+(**************************************************************************)
+(* Backend pragmas: multi-back-ends                                       *)
+(*                                                                        *)
+(* These pragmas just run a bunch of back-ends one after the other in the *)
+(* hope that one will succeed. This saves time and effort for the user at *)
+(* the expense of computation time.                                       *)
+(**************************************************************************)
+
+(* CVC3 goes first because it's bundled with TLAPS, then the other SMT
+   solvers are unlikely to succeed if CVC3 fails, so we run zenon and
+   Isabelle before them. *)
+AllProvers == TRUE (*{
+    by (prover:"cvc33")
+    by (prover:"zenon")
+    by (prover:"isabelle"; tactic:"auto")
+    by (prover:"spass")
+    by (prover:"smt3")
+    by (prover:"yices3")
+    by (prover:"verit")
+    by (prover:"z33")
+    by (prover:"isabelle"; tactic:"force")
+    by (prover:"isabelle"; tactic:"(auto intro: setEqualI)")
+    by (prover:"isabelle"; tactic:"clarsimp auto?")
+    by (prover:"isabelle"; tactic:"clarsimp")
+    by (prover:"isabelle"; tactic:"auto, blast")
+  }*)
+AllProversT(X) == TRUE (*{
+    by (prover:"cvc33"; timeout:@)
+    by (prover:"zenon"; timeout:@)
+    by (prover:"isabelle"; tactic:"auto"; timeout:@)
+    by (prover:"spass"; timeout:@)
+    by (prover:"smt3"; timeout:@)
+    by (prover:"yices3"; timeout:@)
+    by (prover:"verit"; timeout:@)
+    by (prover:"z33"; timeout:@)
+    by (prover:"isabelle"; tactic:"force"; timeout:@)
+    by (prover:"isabelle"; tactic:"(auto intro: setEqualI)"; timeout:@)
+    by (prover:"isabelle"; tactic:"clarsimp auto?"; timeout:@)
+    by (prover:"isabelle"; tactic:"clarsimp"; timeout:@)
+    by (prover:"isabelle"; tactic:"auto, blast"; timeout:@)
+  }*)
+
+AllSMT == TRUE (*{
+    by (prover:"cvc33")
+    by (prover:"smt3")
+    by (prover:"yices3")
+    by (prover:"verit")
+    by (prover:"z33")
+  }*)
+AllSMTT(X) == TRUE (*{
+    by (prover:"cvc33"; timeout:@)
+    by (prover:"smt3"; timeout:@)
+    by (prover:"yices3"; timeout:@)
+    by (prover:"verit"; timeout:@)
+    by (prover:"z33"; timeout:@)
+  }*)
+
+AllIsa == TRUE (*{
+    by (prover:"isabelle"; tactic:"auto")
+    by (prover:"isabelle"; tactic:"force")
+    by (prover:"isabelle"; tactic:"(auto intro: setEqualI)")
+    by (prover:"isabelle"; tactic:"clarsimp auto?")
+    by (prover:"isabelle"; tactic:"clarsimp")
+    by (prover:"isabelle"; tactic:"auto, blast")
+  }*)
+AllIsaT(X) == TRUE (*{
+    by (prover:"isabelle"; tactic:"auto"; timeout:@)
+    by (prover:"isabelle"; tactic:"force"; timeout:@)
+    by (prover:"isabelle"; tactic:"(auto intro: setEqualI)"; timeout:@)
+    by (prover:"isabelle"; tactic:"clarsimp auto?"; timeout:@)
+    by (prover:"isabelle"; tactic:"clarsimp"; timeout:@)
+    by (prover:"isabelle"; tactic:"auto, blast"; timeout:@)
+  }*)
+
+
+(**************************************************************************)
+(* The pragma ExpandEnabled invokes expansion of the operator ENABLED.    *)
+(*                                                                        *)
+(* The pragma ExpandCdot invokes expansion of the operator \cdot.         *)
+(*                                                                        *)
+(* The pragma AutoUSE invokes automated expansion of definitions,         *)
+(* for both of ExpandEnabled and ExpandCdot, when each is present.        *)
+(*                                                                        *)
+(* The pragma Lambdify invokes expansion of the operators                 *)
+(* ENABLED and \cdot to an intermediate form with bound VARIABLES,        *)
+(* which is a form before introducing rigid quantifiers.                  *)
+(* The pragma Lambdify is sound for occurrences of ENABLED and \cdot      *)
+(* that are not nested.                                                   *)
+(*                                                                        *)
+(* The pragma ENABLEDaxioms invokes axioms about the operator ENABLED.    *)
+(*                                                                        *)
+(* The pragma ENABLEDrules invokes two proof rules about the operator     *)
+(* ENABLED.                                                               *)
+(*                                                                        *)
+(* The pragma LevelComparison allows proofs that change only the levels   *)
+(* of declared operators, or rename declared operators.                   *)
+(**************************************************************************)
+ExpandENABLED == TRUE  (*{ by (prover:"expandenabled") }*)
+ExpandCdot == TRUE  (*{ by (prover:"expandcdot") }*)
+AutoUSE == TRUE  (*{ by (prover:"autouse") }*)
+Lambdify == TRUE  (*{ by (prover:"lambdify") }*)
+ENABLEDaxioms == TRUE  (*{ by (prover:"enabledaxioms") }*)
+ENABLEDrewrites == TRUE  (*{ by (prover:"enabledrewrites") }*)
+ENABLEDrules == TRUE  (*{ by (prover:"enabledrules") }*)
+LevelComparison == TRUE  (*{ by (prover:"levelcomparison") }*)
+
+(* The operators EnabledWrapper and CdotWrapper occur in an intermediate  *)
+(* representation within TLAPM.                                           *)
+EnabledWrapper(Op(_)) == FALSE
+CdotWrapper(Op(_)) == FALSE
+
+(***************************************************************************)
+(* The following may be used in a `BY ONLY ThmName` for unit testing the   *)
+(* triviality checks in TLAPM.                                             *)
+(***************************************************************************)
+Trivial == TRUE  (*{ by (prover:"trivial") }*)
+
+
+=============================================================================
+
+The material below is obsolete: the TLA proof rules below are superseded by
+the PTL decision procedure, and their formulation is unsound for the semantics
+of temporal reasoning that TLAPS adopts.
+
+----------------------------------------------------------------------------
+(***************************************************************************)
+(*                           TEMPORAL LOGIC                                *)
+(*                                                                         *)
+(* The following rules are intended to be used when TLAPS handles temporal *)
+(* logic.  They will not work now.  Moreover when temporal reasoning is    *)
+(* implemented, these rules may be changed or omitted, and additional      *)
+(* rules will probably be added.  However, they are included mainly so     *)
+(* their names will be defined, preventing the use of identifiers that are *)
+(* likely to produce name clashes with future versions of this module.     *)
+(***************************************************************************)
+
+
+(***************************************************************************)
+(* The following proof rules (and their names) are from the paper "The     *)
+(* Temporal Logic of Actions".                                             *)
+(***************************************************************************)
+THEOREM RuleTLA1 == ASSUME STATE P, STATE f,
+                           P /\ (f' = f) => P'
+                    PROVE  []P <=> P /\ [][P => P']_f
+
+THEOREM RuleTLA2 == ASSUME STATE P, STATE Q, STATE f, STATE g,
+                           ACTION A, ACTION B,
+                           P /\ [A]_f => Q /\ [B]_g
+                    PROVE  []P /\ [][A]_f => []Q /\ [][B]_g
+
+THEOREM RuleINV1 == ASSUME STATE I, STATE F,  ACTION N,
+                           I /\ [N]_F => I'
+                    PROVE  I /\ [][N]_F => []I
+
+THEOREM RuleINV2 == ASSUME STATE I, STATE f, ACTION N
+                    PROVE  []I => ([][N]_f <=> [][N /\ I /\ I']_f)
+
+THEOREM RuleWF1 == ASSUME STATE P, STATE Q, STATE f, ACTION N, ACTION A,
+                          P /\ [N]_f => (P' \/ Q'),
+                          P /\ <<N /\ A>>_f => Q',
+                          P => ENABLED <<A>>_f
+                   PROVE  [][N]_f /\ WF_f(A) => (P ~> Q)
+
+THEOREM RuleSF1 == ASSUME STATE P, STATE Q, STATE f,
+                          ACTION N, ACTION A, TEMPORAL F,
+                          P /\ [N]_f => (P' \/ Q'),
+                          P /\ <<N /\ A>>_f => Q',
+                          []P /\ [][N]_f /\ []F => <> ENABLED <<A>>_f
+                   PROVE  [][N]_f /\ SF_f(A) /\ []F => (P ~> Q)
+
+(***************************************************************************)
+(* The rules WF2 and SF2 in "The Temporal Logic of Actions" are obtained   *)
+(* from the following two rules by the following substitutions: `.         *)
+(*                                                                         *)
+(*          ___        ___         _______________                         *)
+(*      M <- M ,   g <- g ,  EM <- ENABLED <<M>>_g       .'                *)
+(***************************************************************************)
+THEOREM RuleWF2 == ASSUME STATE P, STATE f, STATE g, STATE EM,
+                          ACTION A, ACTION B, ACTION N, ACTION M,
+                          TEMPORAL F,
+                          <<N /\ B>>_f => <<M>>_g,
+                          P /\ P' /\ <<N /\ A>>_f /\ EM => B,
+                          P /\ EM => ENABLED A,
+                          [][N /\ ~B]_f /\ WF_f(A) /\ []F /\ <>[]EM => <>[]P
+                   PROVE  [][N]_f /\ WF_f(A) /\ []F => []<><<M>>_g \/ []<>(~EM)
+
+THEOREM RuleSF2 == ASSUME STATE P, STATE f, STATE g, STATE EM,
+                          ACTION A, ACTION B, ACTION N, ACTION M,
+                          TEMPORAL F,
+                          <<N /\ B>>_f => <<M>>_g,
+                          P /\ P' /\ <<N /\ A>>_f /\ EM => B,
+                          P /\ EM => ENABLED A,
+                          [][N /\ ~B]_f /\ SF_f(A) /\ []F /\ []<>EM => <>[]P
+                   PROVE  [][N]_f /\ SF_f(A) /\ []F => []<><<M>>_g \/ <>[](~EM)
+
+
+(***************************************************************************)
+(* The following rule is a special case of the general temporal logic      *)
+(* proof rule STL4 from the paper "The Temporal Logic of Actions".  The    *)
+(* general rule is for arbitrary temporal formulas F and G, but it cannot  *)
+(* yet be handled by TLAPS.                                                *)
+(***************************************************************************)
+THEOREM RuleInvImplication ==
+  ASSUME STATE F, STATE G,
+         F => G
+  PROVE  []F => []G
+PROOF OMITTED
+
+(***************************************************************************)
+(* The following rule is a special case of rule TLA2 from the paper "The   *)
+(* Temporal Logic of Actions".                                             *)
+(***************************************************************************)
+THEOREM RuleStepSimulation ==
+  ASSUME STATE I, STATE f, STATE g,
+         ACTION M, ACTION N,
+         I /\ I' /\ [M]_f => [N]_g
+  PROVE  []I /\ [][M]_f => [][N]_g
+PROOF OMITTED
+
+(***************************************************************************)
+(* The following may be used to invoke a decision procedure for            *)
+(* propositional temporal logic.                                           *)
+(***************************************************************************)
+PropositionalTemporalLogic == TRUE
+=============================================================================