diff --git a/benchmarks/README.md b/benchmarks/README.md
index d31bae7e9a261dc2974e69c869bab959ec9fe0df..f28d8f02cfaea5a8a30b00bccd5ae57b1b87d040 100644
--- a/benchmarks/README.md
+++ b/benchmarks/README.md
@@ -8,10 +8,11 @@ imitator models were borrowed from the
 
 ```
 .
-├── analysis.ipynb    # Python notebook to generate the plots
+├── analysis.ipynb    # Python notebook to generate the plots (analysis.py)
 ├── benchmarks.sh     # Bash script to run the benchmarks
 ├── images            # Folder containing the plots of the benchmark results
 ├── models            # Folder containing the models of the benchmark
+├── requirements.txt  # File containing the python requirements
 └── results.csv       # CSV file with the benchmarks results
 ```
 
@@ -20,3 +21,8 @@ imitator models were borrowed from the
 The script `benchmarks.sh` allows to run the benchmarks for a specific model.
 Before running it, please set the variables `imitator` and `maude` with the
 absolute path of IMITATOR and Maude binaries, respectively.
+
+```
+λ> ./benchmarks.sh
+Usage: ./benchmarks.sh -m MODEL -t TIMEOUT
+```
diff --git a/benchmarks/benchmarks.sh b/benchmarks/benchmarks.sh
index e9009523169f9f66b3e24656d9f4d44f581fcb9d..801a8508d883e278a4759aacb5cd01af451ccb1d 100755
--- a/benchmarks/benchmarks.sh
+++ b/benchmarks/benchmarks.sh
@@ -109,11 +109,36 @@ function run_benchmark {
   sed -zi 's/^\n//g' ${location_file}
 }
 
-# Timeout in seconds (3 minutes)
-timeout="5m"
+# Print a help message.
+function usage() {
+  echo "Usage: $0 -m MODEL -t TIMEOUT" 1>&2
+}
+
+# Exit with error.
+exit_abnormal() {
+  usage
+  exit 1
+}
+
+# -----------------------------------------------------------------------------
+# MAIN
+# -----------------------------------------------------------------------------
+
+TIMEOUT=""
+MODEL=""
+
+while [[ "$#" -gt 0 ]]; do
+  case "$1" in
+    -m|--model) MODEL="$2"; shift ;;
+    -t|--timeout) TIMEOUT="$2"; shift ;;
+    *) exit_abnormal ;;
+  esac
+  shift
+done
 
-# model
-model="coffee"
+if [ "$MODEL" = "" ] || [ "$TIMEOUT" = "" ]; then
+  exit_abnormal
+fi
 
 # run benchmark
-run_benchmark "${model}" "${timeout}"
\ No newline at end of file
+run_benchmark "${MODEL}" "${TIMEOUT}"
\ No newline at end of file
diff --git a/benchmarks/models/tgc.collapsing.maude b/benchmarks/models/tgc.collapsing.maude
index 63a0c1ff702a0db3496189d5778c055be925f7d2..90c31762999ade14817562900f26aed355c48d99 100644
--- a/benchmarks/models/tgc.collapsing.maude
+++ b/benchmarks/models/tgc.collapsing.maude
@@ -8,7 +8,7 @@ mod MODEL is
     vars x y z : Real .
     vars a b c d e f : Real .
 
-    ops Train0Gate0Controller0 Train1Gate0Controller1 Train1Gate1Controller2 Train1Gate2Controller2 Train2Gate2Controller2 Train3Gate2Controller2 Train0Gate2Controller3 Train0Gate3Controller0 Train1Gate3Controller1 Train2Gate3Controller1 Train3Gate3Controller1 Train3Gate0Controller1 Train3Gate1Controller2 Train0Gate1Controller3 Train2Gate0Controller1 Train2Gate1Controller2 : -> Location .
+    ops Train0Gate0Controller0 Train1Gate0Controller1 Train1Gate1Controller2 Train1Gate2Controller2 Train2Gate2Controller2 Train3Gate2Controller2 Train0Gate2Controller3 Train0Gate3Controller0 Train1Gate3Controller1 Train2Gate3Controller1 Train2Gate0Controller1 Train2Gate1Controller2 Train3Gate1Controller2 Train0Gate1Controller3 Train3Gate0Controller1 Train3Gate3Controller1 : -> Location .
 
     op <_;_;_;_> <_;_;_;_;_;_> : Location Real Real Real Real Real Real Real Real Real -> NState .
     op [_;_;_;_] <_;_;_;_;_;_> : Location Real Real Real Real Real Real Real Real Real -> DState .
@@ -36,23 +36,25 @@ mod MODEL is
     crl [Train0Gate2Controller3-Train0Gate3Controller0] : < Train0Gate2Controller3 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train0Gate3Controller0 ; x ; 0/1 ; z ] < a ; b ; c ; d ; e ; f > if (e < z and z < f) = true .
     crl [tick-Train0Gate2Controller3] : [ Train0Gate2Controller3 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > => < Train0Gate2Controller3 ; x + T ; y + T ; z + T > < a ; b ; c ; d ; e ; f > if (T >= 0/1) = true [nonexec] .
 
-    crl [Train0Gate3Controller0-Train0Gate0Controller0] : < Train0Gate3Controller0 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train0Gate0Controller0 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > if (c < y and y < d) = true .
     rl [Train0Gate3Controller0-Train1Gate3Controller1] : < Train0Gate3Controller0 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train1Gate3Controller1 ; 0/1 ; y ; 0/1 ] < a ; b ; c ; d ; e ; f > .
+    crl [Train0Gate3Controller0-Train0Gate0Controller0] : < Train0Gate3Controller0 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train0Gate0Controller0 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > if (c < y and y < d) = true .
     crl [tick-Train0Gate3Controller0] : [ Train0Gate3Controller0 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > => < Train0Gate3Controller0 ; x + T ; y + T ; z + T > < a ; b ; c ; d ; e ; f > if (T >= 0/1) = true [nonexec] .
 
-    crl [Train1Gate3Controller1-Train1Gate0Controller1] : < Train1Gate3Controller1 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train1Gate0Controller1 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > if (c < y and y < d) = true .
     crl [Train1Gate3Controller1-Train2Gate3Controller1] : < Train1Gate3Controller1 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train2Gate3Controller1 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > if (x > a) = true .
+    crl [Train1Gate3Controller1-Train1Gate0Controller1] : < Train1Gate3Controller1 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train1Gate0Controller1 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > if (c < y and y < d) = true .
     crl [tick-Train1Gate3Controller1] : [ Train1Gate3Controller1 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > => < Train1Gate3Controller1 ; x + T ; y + T ; z + T > < a ; b ; c ; d ; e ; f > if (T >= 0/1) = true [nonexec] .
 
-    crl [Train2Gate3Controller1-Train2Gate0Controller1] : < Train2Gate3Controller1 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train2Gate0Controller1 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > if (c < y and y < d) = true .
     rl [Train2Gate3Controller1-Train3Gate3Controller1] : < Train2Gate3Controller1 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train3Gate3Controller1 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > .
+    crl [Train2Gate3Controller1-Train2Gate0Controller1] : < Train2Gate3Controller1 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train2Gate0Controller1 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > if (c < y and y < d) = true .
     crl [tick-Train2Gate3Controller1] : [ Train2Gate3Controller1 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > => < Train2Gate3Controller1 ; x + T ; y + T ; z + T > < a ; b ; c ; d ; e ; f > if (T >= 0/1) = true [nonexec] .
 
-    crl [Train3Gate3Controller1-Train3Gate0Controller1] : < Train3Gate3Controller1 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train3Gate0Controller1 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > if (c < y and y < d) = true .
-    crl [tick-Train3Gate3Controller1] : [ Train3Gate3Controller1 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > => < Train3Gate3Controller1 ; x + T ; y + T ; z + T > < a ; b ; c ; d ; e ; f > if (T >= 0/1) = true [nonexec] .
+    rl [Train2Gate0Controller1-Train3Gate0Controller1] : < Train2Gate0Controller1 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train3Gate0Controller1 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > .
+    crl [Train2Gate0Controller1-Train2Gate1Controller2] : < Train2Gate0Controller1 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train2Gate1Controller2 ; x ; 0/1 ; z ] < a ; b ; c ; d ; e ; f > if (e < z and z < f) = true .
+    crl [tick-Train2Gate0Controller1] : [ Train2Gate0Controller1 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > => < Train2Gate0Controller1 ; x + T ; y + T ; z + T > < a ; b ; c ; d ; e ; f > if (T >= 0/1) = true [nonexec] .
 
-    crl [Train3Gate0Controller1-Train3Gate1Controller2] : < Train3Gate0Controller1 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train3Gate1Controller2 ; x ; 0/1 ; z ] < a ; b ; c ; d ; e ; f > if (e < z and z < f) = true .
-    crl [tick-Train3Gate0Controller1] : [ Train3Gate0Controller1 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > => < Train3Gate0Controller1 ; x + T ; y + T ; z + T > < a ; b ; c ; d ; e ; f > if (T >= 0/1) = true [nonexec] .
+    rl [Train2Gate1Controller2-Train3Gate1Controller2] : < Train2Gate1Controller2 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train3Gate1Controller2 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > .
+    crl [Train2Gate1Controller2-Train2Gate2Controller2] : < Train2Gate1Controller2 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train2Gate2Controller2 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > if (c < y and y < d) = true .
+    crl [tick-Train2Gate1Controller2] : [ Train2Gate1Controller2 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > => < Train2Gate1Controller2 ; x + T ; y + T ; z + T > < a ; b ; c ; d ; e ; f > if (T >= 0/1) = true [nonexec] .
 
     crl [Train3Gate1Controller2-Train0Gate1Controller3] : < Train3Gate1Controller2 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train0Gate1Controller3 ; x ; y ; 0/1 ] < a ; b ; c ; d ; e ; f > if (x < b) = true .
     crl [Train3Gate1Controller2-Train3Gate2Controller2] : < Train3Gate1Controller2 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train3Gate2Controller2 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > if (c < y and y < d) = true .
@@ -61,13 +63,11 @@ mod MODEL is
     crl [Train0Gate1Controller3-Train0Gate2Controller3] : < Train0Gate1Controller3 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train0Gate2Controller3 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > if (c < y and y < d) = true .
     crl [tick-Train0Gate1Controller3] : [ Train0Gate1Controller3 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > => < Train0Gate1Controller3 ; x + T ; y + T ; z + T > < a ; b ; c ; d ; e ; f > if (T >= 0/1) = true [nonexec] .
 
-    rl [Train2Gate0Controller1-Train3Gate0Controller1] : < Train2Gate0Controller1 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train3Gate0Controller1 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > .
-    crl [Train2Gate0Controller1-Train2Gate1Controller2] : < Train2Gate0Controller1 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train2Gate1Controller2 ; x ; 0/1 ; z ] < a ; b ; c ; d ; e ; f > if (e < z and z < f) = true .
-    crl [tick-Train2Gate0Controller1] : [ Train2Gate0Controller1 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > => < Train2Gate0Controller1 ; x + T ; y + T ; z + T > < a ; b ; c ; d ; e ; f > if (T >= 0/1) = true [nonexec] .
+    crl [Train3Gate0Controller1-Train3Gate1Controller2] : < Train3Gate0Controller1 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train3Gate1Controller2 ; x ; 0/1 ; z ] < a ; b ; c ; d ; e ; f > if (e < z and z < f) = true .
+    crl [tick-Train3Gate0Controller1] : [ Train3Gate0Controller1 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > => < Train3Gate0Controller1 ; x + T ; y + T ; z + T > < a ; b ; c ; d ; e ; f > if (T >= 0/1) = true [nonexec] .
 
-    crl [Train2Gate1Controller2-Train2Gate2Controller2] : < Train2Gate1Controller2 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train2Gate2Controller2 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > if (c < y and y < d) = true .
-    rl [Train2Gate1Controller2-Train3Gate1Controller2] : < Train2Gate1Controller2 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train3Gate1Controller2 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > .
-    crl [tick-Train2Gate1Controller2] : [ Train2Gate1Controller2 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > => < Train2Gate1Controller2 ; x + T ; y + T ; z + T > < a ; b ; c ; d ; e ; f > if (T >= 0/1) = true [nonexec] .
+    crl [Train3Gate3Controller1-Train3Gate0Controller1] : < Train3Gate3Controller1 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train3Gate0Controller1 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > if (c < y and y < d) = true .
+    crl [tick-Train3Gate3Controller1] : [ Train3Gate3Controller1 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > => < Train3Gate3Controller1 ; x + T ; y + T ; z + T > < a ; b ; c ; d ; e ; f > if (T >= 0/1) = true [nonexec] .
 
 
     var l : Location .
@@ -78,7 +78,7 @@ endm
 
 load meta-pta .
 
-red reachability (<replace>, (< Train0Gate0Controller0 ; x:Real ; y:Real ; z:Real > < a:Real ; b:Real ; c:Real ; d:Real ; e:Real ; f:Real > | ( x:Real === y:Real and x:Real === z:Real and x:Real >= 0/1 and y:Real >= 0/1 and z:Real >= 0/1 and a:Real >= 0/1 and b:Real >= 0/1 and c:Real >= 0/1 and d:Real >= 0/1 and e:Real >= 0/1 and f:Real >= 0/1 ) )) .
+red reachability (<replace>, ( < Train0Gate0Controller0 ; x:Real ; y:Real ; z:Real > < a:Real ; b:Real ; c:Real ; d:Real ; e:Real ; f:Real > | ( x:Real === y:Real and x:Real === z:Real and x:Real >= 0/1 and y:Real >= 0/1 and z:Real >= 0/1 and a:Real >= 0/1 and b:Real >= 0/1 and c:Real >= 0/1 and d:Real >= 0/1 and e:Real >= 0/1 and f:Real >= 0/1 ) )) .
 
 quit .
 
diff --git a/benchmarks/models/tgc.imi.full b/benchmarks/models/tgc.imi.full
index 3e42ac82aec58bc8d303364d2d6cf357e0d8d62b..2dfd94b0e9abdc44cce4a6b33008c53a14648763 100644
--- a/benchmarks/models/tgc.imi.full
+++ b/benchmarks/models/tgc.imi.full
@@ -5,7 +5,7 @@ var
 (************************************************************)
   automaton tgc
 (************************************************************)
-synclabs: up, inn, exit, raise, approach, down, out, lower;
+synclabs: inn, up, approach, down, exit, out, lower, raise;
 
 loc Train0Gate0Controller0: invariant True
   when True sync approach do {x:=0, z:=0} goto Train1Gate0Controller1;
@@ -35,8 +35,8 @@ accepting loc Train0Gate3Controller0: invariant True
   when True sync approach do {x:=0, z:=0} goto Train1Gate3Controller1;
 
 accepting loc Train1Gate3Controller1: invariant True
-  when c<y&y<d sync up do {} goto Train1Gate0Controller1;
   when x>a sync inn do {} goto Train2Gate3Controller1;
+  when c<y&y<d sync up do {} goto Train1Gate0Controller1;
 
 accepting loc Train2Gate3Controller1: invariant True
   when c<y&y<d sync up do {} goto Train2Gate0Controller1;
@@ -49,8 +49,8 @@ loc Train3Gate0Controller1: invariant True
   when e<z&z<f sync lower do {y:=0} goto Train3Gate1Controller2;
 
 loc Train3Gate1Controller2: invariant True
-  when x<b sync exit do {z:=0} goto Train0Gate1Controller3;
   when c<y&y<d sync down do {} goto Train3Gate2Controller2;
+  when x<b sync exit do {z:=0} goto Train0Gate1Controller3;
 
 loc Train0Gate1Controller3: invariant True
   when c<y&y<d sync down do {} goto Train0Gate2Controller3;
diff --git a/benchmarks/models/tgc.no-collapsing.maude b/benchmarks/models/tgc.no-collapsing.maude
new file mode 100644
index 0000000000000000000000000000000000000000..3a5123402e25ed1f094f9fced676b51ec4dc89cf
--- /dev/null
+++ b/benchmarks/models/tgc.no-collapsing.maude
@@ -0,0 +1,79 @@
+load smt .
+
+mod MODEL is
+    protecting REAL .
+
+    sorts State Location .
+
+    var T : Real .
+    vars x y z : Real .
+    vars a b c d e f : Real .
+
+    ops Train0Gate0Controller0 Train1Gate0Controller1 Train1Gate1Controller2 Train1Gate2Controller2 Train2Gate2Controller2 Train3Gate2Controller2 Train0Gate2Controller3 Train0Gate3Controller0 Train1Gate3Controller1 Train2Gate3Controller1 Train3Gate3Controller1 Train3Gate0Controller1 Train3Gate1Controller2 Train0Gate1Controller3 Train2Gate0Controller1 Train2Gate1Controller2 : -> Location .
+
+    op <_;_;_;_> <_;_;_;_;_;_> : Location Real Real Real Real Real Real Real Real Real -> State .
+    op [_;_;_;_] <_;_;_;_;_;_> : Location Real Real Real Real Real Real Real Real Real -> State .
+
+    rl [Train0Gate0Controller0-Train1Gate0Controller1] : < Train0Gate0Controller0 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train1Gate0Controller1 ; 0/1 ; y ; 0/1 ] < a ; b ; c ; d ; e ; f > .
+    crl [tick-Train0Gate0Controller0] : [ Train0Gate0Controller0 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > => < Train0Gate0Controller0 ; x + T ; y + T ; z + T > < a ; b ; c ; d ; e ; f > if (T >= 0/1) = true [nonexec] .
+
+    crl [Train1Gate0Controller1-Train2Gate0Controller1] : < Train1Gate0Controller1 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train2Gate0Controller1 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > if (x > a) = true .
+    crl [Train1Gate0Controller1-Train1Gate1Controller2] : < Train1Gate0Controller1 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train1Gate1Controller2 ; x ; 0/1 ; z ] < a ; b ; c ; d ; e ; f > if (e < z and z < f) = true .
+    crl [tick-Train1Gate0Controller1] : [ Train1Gate0Controller1 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > => < Train1Gate0Controller1 ; x + T ; y + T ; z + T > < a ; b ; c ; d ; e ; f > if (T >= 0/1) = true [nonexec] .
+
+    crl [Train1Gate1Controller2-Train2Gate1Controller2] : < Train1Gate1Controller2 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train2Gate1Controller2 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > if (x > a) = true .
+    crl [Train1Gate1Controller2-Train1Gate2Controller2] : < Train1Gate1Controller2 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train1Gate2Controller2 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > if (c < y and y < d) = true .
+    crl [tick-Train1Gate1Controller2] : [ Train1Gate1Controller2 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > => < Train1Gate1Controller2 ; x + T ; y + T ; z + T > < a ; b ; c ; d ; e ; f > if (T >= 0/1) = true [nonexec] .
+
+    crl [Train1Gate2Controller2-Train2Gate2Controller2] : < Train1Gate2Controller2 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train2Gate2Controller2 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > if (x > a) = true .
+    crl [tick-Train1Gate2Controller2] : [ Train1Gate2Controller2 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > => < Train1Gate2Controller2 ; x + T ; y + T ; z + T > < a ; b ; c ; d ; e ; f > if (T >= 0/1) = true [nonexec] .
+
+    rl [Train2Gate2Controller2-Train3Gate2Controller2] : < Train2Gate2Controller2 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train3Gate2Controller2 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > .
+    crl [tick-Train2Gate2Controller2] : [ Train2Gate2Controller2 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > => < Train2Gate2Controller2 ; x + T ; y + T ; z + T > < a ; b ; c ; d ; e ; f > if (T >= 0/1) = true [nonexec] .
+
+    crl [Train3Gate2Controller2-Train0Gate2Controller3] : < Train3Gate2Controller2 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train0Gate2Controller3 ; x ; y ; 0/1 ] < a ; b ; c ; d ; e ; f > if (x < b) = true .
+    crl [tick-Train3Gate2Controller2] : [ Train3Gate2Controller2 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > => < Train3Gate2Controller2 ; x + T ; y + T ; z + T > < a ; b ; c ; d ; e ; f > if (T >= 0/1) = true [nonexec] .
+
+    crl [Train0Gate2Controller3-Train0Gate3Controller0] : < Train0Gate2Controller3 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train0Gate3Controller0 ; x ; 0/1 ; z ] < a ; b ; c ; d ; e ; f > if (e < z and z < f) = true .
+    crl [tick-Train0Gate2Controller3] : [ Train0Gate2Controller3 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > => < Train0Gate2Controller3 ; x + T ; y + T ; z + T > < a ; b ; c ; d ; e ; f > if (T >= 0/1) = true [nonexec] .
+
+    crl [Train0Gate3Controller0-Train0Gate0Controller0] : < Train0Gate3Controller0 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train0Gate0Controller0 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > if (c < y and y < d) = true .
+    rl [Train0Gate3Controller0-Train1Gate3Controller1] : < Train0Gate3Controller0 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train1Gate3Controller1 ; 0/1 ; y ; 0/1 ] < a ; b ; c ; d ; e ; f > .
+    crl [tick-Train0Gate3Controller0] : [ Train0Gate3Controller0 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > => < Train0Gate3Controller0 ; x + T ; y + T ; z + T > < a ; b ; c ; d ; e ; f > if (T >= 0/1) = true [nonexec] .
+
+    crl [Train1Gate3Controller1-Train2Gate3Controller1] : < Train1Gate3Controller1 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train2Gate3Controller1 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > if (x > a) = true .
+    crl [Train1Gate3Controller1-Train1Gate0Controller1] : < Train1Gate3Controller1 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train1Gate0Controller1 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > if (c < y and y < d) = true .
+    crl [tick-Train1Gate3Controller1] : [ Train1Gate3Controller1 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > => < Train1Gate3Controller1 ; x + T ; y + T ; z + T > < a ; b ; c ; d ; e ; f > if (T >= 0/1) = true [nonexec] .
+
+    crl [Train2Gate3Controller1-Train2Gate0Controller1] : < Train2Gate3Controller1 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train2Gate0Controller1 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > if (c < y and y < d) = true .
+    rl [Train2Gate3Controller1-Train3Gate3Controller1] : < Train2Gate3Controller1 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train3Gate3Controller1 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > .
+    crl [tick-Train2Gate3Controller1] : [ Train2Gate3Controller1 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > => < Train2Gate3Controller1 ; x + T ; y + T ; z + T > < a ; b ; c ; d ; e ; f > if (T >= 0/1) = true [nonexec] .
+
+    crl [Train3Gate3Controller1-Train3Gate0Controller1] : < Train3Gate3Controller1 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train3Gate0Controller1 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > if (c < y and y < d) = true .
+    crl [tick-Train3Gate3Controller1] : [ Train3Gate3Controller1 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > => < Train3Gate3Controller1 ; x + T ; y + T ; z + T > < a ; b ; c ; d ; e ; f > if (T >= 0/1) = true [nonexec] .
+
+    crl [Train3Gate0Controller1-Train3Gate1Controller2] : < Train3Gate0Controller1 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train3Gate1Controller2 ; x ; 0/1 ; z ] < a ; b ; c ; d ; e ; f > if (e < z and z < f) = true .
+    crl [tick-Train3Gate0Controller1] : [ Train3Gate0Controller1 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > => < Train3Gate0Controller1 ; x + T ; y + T ; z + T > < a ; b ; c ; d ; e ; f > if (T >= 0/1) = true [nonexec] .
+
+    crl [Train3Gate1Controller2-Train3Gate2Controller2] : < Train3Gate1Controller2 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train3Gate2Controller2 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > if (c < y and y < d) = true .
+    crl [Train3Gate1Controller2-Train0Gate1Controller3] : < Train3Gate1Controller2 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train0Gate1Controller3 ; x ; y ; 0/1 ] < a ; b ; c ; d ; e ; f > if (x < b) = true .
+    crl [tick-Train3Gate1Controller2] : [ Train3Gate1Controller2 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > => < Train3Gate1Controller2 ; x + T ; y + T ; z + T > < a ; b ; c ; d ; e ; f > if (T >= 0/1) = true [nonexec] .
+
+    crl [Train0Gate1Controller3-Train0Gate2Controller3] : < Train0Gate1Controller3 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train0Gate2Controller3 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > if (c < y and y < d) = true .
+    crl [tick-Train0Gate1Controller3] : [ Train0Gate1Controller3 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > => < Train0Gate1Controller3 ; x + T ; y + T ; z + T > < a ; b ; c ; d ; e ; f > if (T >= 0/1) = true [nonexec] .
+
+    rl [Train2Gate0Controller1-Train3Gate0Controller1] : < Train2Gate0Controller1 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train3Gate0Controller1 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > .
+    crl [Train2Gate0Controller1-Train2Gate1Controller2] : < Train2Gate0Controller1 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train2Gate1Controller2 ; x ; 0/1 ; z ] < a ; b ; c ; d ; e ; f > if (e < z and z < f) = true .
+    crl [tick-Train2Gate0Controller1] : [ Train2Gate0Controller1 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > => < Train2Gate0Controller1 ; x + T ; y + T ; z + T > < a ; b ; c ; d ; e ; f > if (T >= 0/1) = true [nonexec] .
+
+    crl [Train2Gate1Controller2-Train2Gate2Controller2] : < Train2Gate1Controller2 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train2Gate2Controller2 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > if (c < y and y < d) = true .
+    rl [Train2Gate1Controller2-Train3Gate1Controller2] : < Train2Gate1Controller2 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train3Gate1Controller2 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > .
+    crl [tick-Train2Gate1Controller2] : [ Train2Gate1Controller2 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > => < Train2Gate1Controller2 ; x + T ; y + T ; z + T > < a ; b ; c ; d ; e ; f > if (T >= 0/1) = true [nonexec] .
+
+endm
+
+smt-search [1] < Train0Gate0Controller0 ; x ; y ; z > < a ; b ; c ; d ; e ; f > =>* < <replace> ; x':Real ; y':Real ; z':Real > < a ; b ; c ; d ; e ; f > such that ( x === y and x === z and x >= 0/1 and y >= 0/1 and z >= 0/1 and a >= 0/1 and b >= 0/1 and c >= 0/1 and d >= 0/1 and e >= 0/1 and f >= 0/1 ) = true .
+
+quit .
+
+eof
\ No newline at end of file