refactored examples

29 files changed, 646 insertions, 83 deletions

diff --git a/.gitignore b/.gitignore
index 9fa256b..fd38b1c 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,6 +1,5 @@
 /inpla
-*/__pycache__
-/vnncomp2025_benchmarks/
+/__pycache__/
 /examples/fashion_mnist/FashionMNIST/raw
 /examples/fashion_mnist/fashion_mnist_a.onnx
 /examples/fashion_mnist/fashion_mnist_a.onnx.data
@@ -15,3 +14,10 @@
 /examples/xor/xor_b.onnx.data
 /examples/fashion_mnist/FashionMNIST/raw
 /notes.norg
+/examples/ACASXU/script_argmax.fish
+/examples/ACASXU/script_epsilon.fish
+/examples/ACASXU/script_strict.fish
+/examples/iris/iris_b.onnx
+/examples/iris/iris_b.onnx.data
+/examples/iris/iris_a.onnx.data
+/examples/iris/iris_a.onnx
diff --git a/examples/ACASXU/ACASXU_argmax.vnnlib b/examples/ACASXU/ACASXU_argmax.vnnlib
new file mode 100644
index 0000000..3009eef
--- /dev/null
+++ b/examples/ACASXU/ACASXU_argmax.vnnlib
@@ -0,0 +1,94 @@
+; Argmax Equivalence for ACASXU
+
+; Constant declaration
+(declare-const X_0 Real)
+(declare-const X_1 Real)
+(declare-const X_2 Real)
+(declare-const X_3 Real)
+(declare-const X_4 Real)
+(declare-const Y_0 Real)
+(declare-const Y_1 Real)
+(declare-const Y_2 Real)
+(declare-const Y_3 Real)
+(declare-const Y_4 Real)
+(declare-const Y_5 Real)
+(declare-const Y_6 Real)
+(declare-const Y_7 Real)
+(declare-const Y_8 Real)
+(declare-const Y_9 Real)
+
+; Bounded inputs: X must be within [0, 1]
+(assert (>= X_0 0.0))
+(assert (<= X_0 1.0))
+(assert (>= X_1 0.0))
+(assert (<= X_1 1.0))
+(assert (>= X_2 0.0))
+(assert (<= X_2 1.0))
+(assert (>= X_3 0.0))
+(assert (<= X_3 1.0))
+(assert (>= X_4 0.0))
+(assert (<= X_4 1.0))
+
+; Violation of argmax equivalence
+(assert (or
+  (and 
+    (> Y_0 Y_1)
+    (> Y_0 Y_2)
+    (> Y_0 Y_3)
+    (> Y_0 Y_4)
+    (or
+      (> Y_6 Y_5)
+      (> Y_7 Y_5)
+      (> Y_8 Y_5)
+      (> Y_9 Y_5)
+    )
+  )
+  (and 
+    (> Y_1 Y_0)
+    (> Y_1 Y_2)
+    (> Y_1 Y_3)
+    (> Y_1 Y_4)
+    (or
+      (> Y_5 Y_6)
+      (> Y_7 Y_6)
+      (> Y_8 Y_6)
+      (> Y_9 Y_6)
+    )
+  )
+  (and 
+    (> Y_2 Y_0)
+    (> Y_2 Y_1)
+    (> Y_2 Y_3)
+    (> Y_2 Y_4)
+    (or
+      (> Y_5 Y_7)
+      (> Y_6 Y_7)
+      (> Y_8 Y_7)
+      (> Y_9 Y_7)
+    )
+  )
+  (and 
+    (> Y_3 Y_0)
+    (> Y_3 Y_1)
+    (> Y_3 Y_2)
+    (> Y_3 Y_4)
+    (or
+      (> Y_5 Y_8)
+      (> Y_6 Y_8)
+      (> Y_7 Y_8)
+      (> Y_9 Y_8)
+    )
+  )
+  (and 
+    (> Y_4 Y_0)
+    (> Y_4 Y_1)
+    (> Y_4 Y_2)
+    (> Y_4 Y_3)
+    (or
+      (> Y_5 Y_9)
+      (> Y_6 Y_9)
+      (> Y_7 Y_9)
+      (> Y_8 Y_9)
+    )
+  )
+))
diff --git a/examples/ACASXU/ACASXU_epsilon.vnnlib b/examples/ACASXU/ACASXU_epsilon.vnnlib
new file mode 100644
index 0000000..0ca04f8
--- /dev/null
+++ b/examples/ACASXU/ACASXU_epsilon.vnnlib
@@ -0,0 +1,40 @@
+; Strict Equivalence for ACASXU
+
+; Constant declaration
+(declare-const X_0 Real)
+(declare-const X_1 Real)
+(declare-const X_2 Real)
+(declare-const X_3 Real)
+(declare-const X_4 Real)
+(declare-const Y_0 Real)
+(declare-const Y_1 Real)
+(declare-const Y_2 Real)
+(declare-const Y_3 Real)
+(declare-const Y_4 Real)
+(declare-const Y_5 Real)
+(declare-const Y_6 Real)
+(declare-const Y_7 Real)
+(declare-const Y_8 Real)
+(declare-const Y_9 Real)
+
+; Bounded inputs: X must be within [0, 1]
+(assert (>= X_0 0.0))
+(assert (<= X_0 1.0))
+(assert (>= X_1 0.0))
+(assert (<= X_1 1.0))
+(assert (>= X_2 0.0))
+(assert (<= X_2 1.0))
+(assert (>= X_3 0.0))
+(assert (<= X_3 1.0))
+(assert (>= X_4 0.0))
+(assert (<= X_4 1.0))
+
+; Violation of epsilon equivalence (epsilon = 0.1)
+(define-fun absolute ((x Real)) Real (if (>= x 0) x (- x)))
+(assert (or
+	(> (absolute (- Y_0 Y_5)) 0.1)
+	(> (absolute (- Y_1 Y_6)) 0.1)
+	(> (absolute (- Y_2 Y_7)) 0.1)
+	(> (absolute (- Y_3 Y_8)) 0.1)
+	(> (absolute (- Y_4 Y_9)) 0.1)
+))
diff --git a/examples/ACASXU/ACASXU_run2a_1_1_batch_2000.onnx b/examples/ACASXU/ACASXU_run2a_1_1_batch_2000.onnx
new file mode 100644
index 0000000..107622f
--- /dev/null
+++ b/examples/ACASXU/ACASXU_run2a_1_1_batch_2000.onnx
diff --git a/examples/ACASXU/ACASXU_strict.vnnlib b/examples/ACASXU/ACASXU_strict.vnnlib
new file mode 100644
index 0000000..1e5b8e2
--- /dev/null
+++ b/examples/ACASXU/ACASXU_strict.vnnlib
@@ -0,0 +1,39 @@
+; Strict Equivalence for ACASXU
+
+; Constant declaration
+(declare-const X_0 Real)
+(declare-const X_1 Real)
+(declare-const X_2 Real)
+(declare-const X_3 Real)
+(declare-const X_4 Real)
+(declare-const Y_0 Real)
+(declare-const Y_1 Real)
+(declare-const Y_2 Real)
+(declare-const Y_3 Real)
+(declare-const Y_4 Real)
+(declare-const Y_5 Real)
+(declare-const Y_6 Real)
+(declare-const Y_7 Real)
+(declare-const Y_8 Real)
+(declare-const Y_9 Real)
+
+; Bounded inputs: X must be within [0, 1]
+(assert (>= X_0 0.0))
+(assert (<= X_0 1.0))
+(assert (>= X_1 0.0))
+(assert (<= X_1 1.0))
+(assert (>= X_2 0.0))
+(assert (<= X_2 1.0))
+(assert (>= X_3 0.0))
+(assert (<= X_3 1.0))
+(assert (>= X_4 0.0))
+(assert (<= X_4 1.0))
+
+; Violation of strict equivalence
+(assert (or
+	(not (= Y_0 Y_5))
+	(not (= Y_1 Y_6))
+	(not (= Y_2 Y_7))
+	(not (= Y_3 Y_8))
+	(not (= Y_4 Y_9))
+))
diff --git a/examples/double_integrator/double_integrator_argmax.vnnlib b/examples/double_integrator/double_integrator_argmax.vnnlib
new file mode 100644
index 0000000..f0a72e9
--- /dev/null
+++ b/examples/double_integrator/double_integrator_argmax.vnnlib
@@ -0,0 +1,27 @@
+; Argmax Equivalence for Double Integrator
+
+; Constant declaration
+(declare-const X_0 Real)
+(declare-const X_1 Real)
+(declare-const Y_0 Real)
+(declare-const Y_1 Real)
+(declare-const Y_2 Real)
+(declare-const Y_3 Real)
+
+; Bounded inputs: X must be within [0, 1]
+(assert (>= X_0 0.0))
+(assert (<= X_0 1.0))
+(assert (>= X_1 0.0))
+(assert (<= X_1 1.0))
+
+; Violation of argmax equivalence
+(assert (or
+  (and 
+    (> Y_0 Y_1)
+		(> Y_3 Y_2)
+  )
+  (and 
+    (> Y_1 Y_0)
+		(> Y_2 Y_3)
+  )
+))
diff --git a/examples/double_integrator/double_integrator_epsilon.vnnlib b/examples/double_integrator/double_integrator_epsilon.vnnlib
new file mode 100644
index 0000000..3af9079
--- /dev/null
+++ b/examples/double_integrator/double_integrator_epsilon.vnnlib
@@ -0,0 +1,22 @@
+; Strict Equivalence for Double Integrator
+
+; Constant declaration
+(declare-const X_0 Real)
+(declare-const X_1 Real)
+(declare-const Y_0 Real)
+(declare-const Y_1 Real)
+(declare-const Y_2 Real)
+(declare-const Y_3 Real)
+
+; Bounded inputs: X must be within [0, 1]
+(assert (>= X_0 0.0))
+(assert (<= X_0 1.0))
+(assert (>= X_1 0.0))
+(assert (<= X_1 1.0))
+
+; Violation of epsilon equivalence (epsilon = 0.1)
+(define-fun absolute ((x Real)) Real (if (>= x 0) x (- x)))
+(assert (or
+	(> (absolute (- Y_0 Y_2)) 0.1)
+	(> (absolute (- Y_1 Y_3)) 0.1)
+))
diff --git a/examples/double_integrator/double_integrator_finetune_inv.onnx b/examples/double_integrator/double_integrator_finetune_inv.onnx
new file mode 100644
index 0000000..8a7797b
--- /dev/null
+++ b/examples/double_integrator/double_integrator_finetune_inv.onnx
diff --git a/examples/double_integrator/double_integrator_strict.vnnlib b/examples/double_integrator/double_integrator_strict.vnnlib
new file mode 100644
index 0000000..d3c8c3e
--- /dev/null
+++ b/examples/double_integrator/double_integrator_strict.vnnlib
@@ -0,0 +1,21 @@
+; Strict Equivalence for Double Integrator
+
+; Constant declaration
+(declare-const X_0 Real)
+(declare-const X_1 Real)
+(declare-const Y_0 Real)
+(declare-const Y_1 Real)
+(declare-const Y_2 Real)
+(declare-const Y_3 Real)
+
+; Bounded inputs: X must be within [0, 1]
+(assert (>= X_0 0.0))
+(assert (<= X_0 1.0))
+(assert (>= X_1 0.0))
+(assert (<= X_1 1.0))
+
+; Violation of strict equivalence
+(assert (or
+	(not (= Y_0 Y_2))
+	(not (= Y_1 Y_3))
+))
diff --git a/examples/fashion_mnist/fashion_mnist.py b/examples/fashion_mnist/fashion_mnist.py
index 3514448..680f4eb 100644
--- a/examples/fashion_mnist/fashion_mnist.py
+++ b/examples/fashion_mnist/fashion_mnist.py
@@ -23,7 +23,7 @@ def train_model(name: str, dim):
     loss_fn = nn.CrossEntropyLoss()
     optimizer = torch.optim.Adam(net.parameters(), lr=1e-4)
 
-    print(f"Training {name}...")
+    print(f"Training {name} ({dim} neurons)...")
     for epoch in range(10):
         global loss
         for data in trainloader:
diff --git a/examples/iris/iris.py b/examples/iris/iris.py
new file mode 100644
index 0000000..db631c0
--- /dev/null
+++ b/examples/iris/iris.py
@@ -0,0 +1,63 @@
+import torch
+import torch.nn as nn
+from sklearn.datasets import load_iris
+from sklearn.preprocessing import StandardScaler
+from torch.utils.data import DataLoader, TensorDataset
+
+class Iris_MLP(nn.Module):
+    def __init__(self, hidden_dim):
+        super().__init__()
+        self.layers = nn.Sequential(
+            nn.Linear(4, hidden_dim),
+            nn.ReLU(),
+            nn.Linear(hidden_dim, 3),
+        )
+    def forward(self, x):
+        return self.layers(x)
+
+iris = load_iris()
+scaler = StandardScaler()
+X = scaler.fit_transform(iris.data).astype('float32') # pyright: ignore
+y = iris.target.astype('int64') # pyright: ignore
+
+dataset = TensorDataset(torch.from_numpy(X), torch.from_numpy(y))
+trainloader = DataLoader(dataset, batch_size=16, shuffle=True)
+
+def train_model(name: str, dim):
+    net = Iris_MLP(hidden_dim=dim)
+    loss_fn = nn.CrossEntropyLoss()
+    optimizer = torch.optim.Adam(net.parameters(), lr=1e-2)
+
+    print(f"Training {name} ({dim} neurons)...")
+    for epoch in range(200):
+        global loss
+        for data in trainloader:
+            inputs, targets = data
+            optimizer.zero_grad()
+            outputs = net(inputs)
+            loss = loss_fn(outputs, targets)
+            loss.backward()
+            optimizer.step()
+        if (epoch + 1) % 100 == 0:
+            print(f"  Epoch {epoch+1}, Loss: {loss.item():.4f}")
+    return net
+
+if __name__ == "__main__":
+    torch_net_a = train_model("Network A", 10).eval()
+    torch_net_b = Iris_MLP(hidden_dim=20).eval()
+
+    with torch.no_grad():
+        torch_net_b.layers[0].weight[:10].copy_(torch_net_a.layers[0].weight) # pyright: ignore
+        torch_net_b.layers[0].bias[:10].copy_(torch_net_a.layers[0].bias) # pyright: ignore
+        torch_net_b.layers[0].weight[10:].copy_(torch_net_a.layers[0].weight) # pyright: ignore
+        torch_net_b.layers[0].bias[10:].copy_(torch_net_a.layers[0].bias) # pyright: ignore
+
+        half_weights = torch_net_a.layers[2].weight / 2.0 # pyright: ignore
+        
+        torch_net_b.layers[2].weight[:, :10].copy_(half_weights) # pyright: ignore
+        torch_net_b.layers[2].weight[:, 10:].copy_(half_weights) # pyright: ignore
+        
+        torch_net_b.layers[2].bias.copy_(torch_net_a.layers[2].bias) # pyright: ignore
+
+    torch.onnx.export(torch_net_a, (torch.randn(1, 4),), "iris_a.onnx")
+    torch.onnx.export(torch_net_b, (torch.randn(1, 4),), "iris_b.onnx")
diff --git a/examples/iris/iris_argmax.vnnlib b/examples/iris/iris_argmax.vnnlib
new file mode 100644
index 0000000..ec72109
--- /dev/null
+++ b/examples/iris/iris_argmax.vnnlib
@@ -0,0 +1,51 @@
+; Argmax Equivalence for Iris
+
+; Constant declaration
+(declare-const X_0 Real)
+(declare-const X_1 Real)
+(declare-const X_2 Real)
+(declare-const X_3 Real)
+(declare-const Y_0 Real)
+(declare-const Y_1 Real)
+(declare-const Y_2 Real)
+(declare-const Y_3 Real)
+(declare-const Y_4 Real)
+(declare-const Y_5 Real)
+
+; Bounded inputs: X must be within [0, 1]
+(assert (>= X_0 0.0))
+(assert (<= X_0 1.0))
+(assert (>= X_1 0.0))
+(assert (<= X_1 1.0))
+(assert (>= X_2 0.0))
+(assert (<= X_2 1.0))
+(assert (>= X_3 0.0))
+(assert (<= X_3 1.0))
+
+; Violation of argmax equivalence
+(assert (or
+  (and 
+    (> Y_0 Y_1)
+    (> Y_0 Y_2)
+    (or
+      (> Y_4 Y_3)
+      (> Y_5 Y_3)
+    )
+  )
+  (and 
+    (> Y_1 Y_0)
+    (> Y_1 Y_2)
+    (or
+      (> Y_3 Y_4)
+      (> Y_5 Y_4)
+    )
+  )
+  (and 
+    (> Y_2 Y_0)
+    (> Y_2 Y_1)
+    (or
+      (> Y_3 Y_5)
+      (> Y_4 Y_5)
+    )
+  )
+))
diff --git a/examples/iris/iris_epsilon.vnnlib b/examples/iris/iris_epsilon.vnnlib
new file mode 100644
index 0000000..9c8e825
--- /dev/null
+++ b/examples/iris/iris_epsilon.vnnlib
@@ -0,0 +1,31 @@
+; Strict Equivalence for Iris
+
+; Constant declaration
+(declare-const X_0 Real)
+(declare-const X_1 Real)
+(declare-const X_2 Real)
+(declare-const X_3 Real)
+(declare-const Y_0 Real)
+(declare-const Y_1 Real)
+(declare-const Y_2 Real)
+(declare-const Y_3 Real)
+(declare-const Y_4 Real)
+(declare-const Y_5 Real)
+
+; Bounded inputs: X must be within [0, 1]
+(assert (>= X_0 0.0))
+(assert (<= X_0 1.0))
+(assert (>= X_1 0.0))
+(assert (<= X_1 1.0))
+(assert (>= X_2 0.0))
+(assert (<= X_2 1.0))
+(assert (>= X_3 0.0))
+(assert (<= X_3 1.0))
+
+; Violation of epsilon equivalence (epsilon = 0.1)
+(define-fun absolute ((x Real)) Real (if (>= x 0) x (- x)))
+(assert (or
+	(> (absolute (- Y_0 Y_3)) 0.1)
+	(> (absolute (- Y_1 Y_4)) 0.1)
+	(> (absolute (- Y_2 Y_5)) 0.1)
+))
diff --git a/examples/iris/iris_strict.vnnlib b/examples/iris/iris_strict.vnnlib
new file mode 100644
index 0000000..78d01fe
--- /dev/null
+++ b/examples/iris/iris_strict.vnnlib
@@ -0,0 +1,30 @@
+; Strict Equivalence for Iris
+
+; Constant declaration
+(declare-const X_0 Real)
+(declare-const X_1 Real)
+(declare-const X_2 Real)
+(declare-const X_3 Real)
+(declare-const Y_0 Real)
+(declare-const Y_1 Real)
+(declare-const Y_2 Real)
+(declare-const Y_3 Real)
+(declare-const Y_4 Real)
+(declare-const Y_5 Real)
+
+; Bounded inputs: X must be within [0, 1]
+(assert (>= X_0 0.0))
+(assert (<= X_0 1.0))
+(assert (>= X_1 0.0))
+(assert (<= X_1 1.0))
+(assert (>= X_2 0.0))
+(assert (<= X_2 1.0))
+(assert (>= X_3 0.0))
+(assert (<= X_3 1.0))
+
+; Violation of strict equivalence
+(assert (or
+	(not (= Y_0 Y_3))
+	(not (= Y_1 Y_4))
+	(not (= Y_2 Y_5))
+))
diff --git a/examples/pendulum/pendulum_argmax.vnnlib b/examples/pendulum/pendulum_argmax.vnnlib
new file mode 100644
index 0000000..c11dc0b
--- /dev/null
+++ b/examples/pendulum/pendulum_argmax.vnnlib
@@ -0,0 +1,27 @@
+; Argmax Equivalence for Pendulum
+
+; Constant declaration
+(declare-const X_0 Real)
+(declare-const X_1 Real)
+(declare-const Y_0 Real)
+(declare-const Y_1 Real)
+(declare-const Y_2 Real)
+(declare-const Y_3 Real)
+
+; Bounded inputs: X must be within [0, 1]
+(assert (>= X_0 0.0))
+(assert (<= X_0 1.0))
+(assert (>= X_1 0.0))
+(assert (<= X_1 1.0))
+
+; Violation of argmax equivalence
+(assert (or
+  (and 
+    (> Y_0 Y_1)
+		(> Y_3 Y_2)
+  )
+  (and 
+    (> Y_1 Y_0)
+		(> Y_2 Y_3)
+  )
+))
diff --git a/examples/pendulum/pendulum_epsilon.vnnlib b/examples/pendulum/pendulum_epsilon.vnnlib
new file mode 100644
index 0000000..a192029
--- /dev/null
+++ b/examples/pendulum/pendulum_epsilon.vnnlib
@@ -0,0 +1,22 @@
+; Strict Equivalence for Pendulum
+
+; Constant declaration
+(declare-const X_0 Real)
+(declare-const X_1 Real)
+(declare-const Y_0 Real)
+(declare-const Y_1 Real)
+(declare-const Y_2 Real)
+(declare-const Y_3 Real)
+
+; Bounded inputs: X must be within [0, 1]
+(assert (>= X_0 0.0))
+(assert (<= X_0 1.0))
+(assert (>= X_1 0.0))
+(assert (<= X_1 1.0))
+
+; Violation of epsilon equivalence (epsilon = 0.1)
+(define-fun absolute ((x Real)) Real (if (>= x 0) x (- x)))
+(assert (or
+	(> (absolute (- Y_0 Y_2)) 0.1)
+	(> (absolute (- Y_1 Y_3)) 0.1)
+))
diff --git a/examples/pendulum/pendulum_finetune_con.onnx b/examples/pendulum/pendulum_finetune_con.onnx
new file mode 100644
index 0000000..59c38ab
--- /dev/null
+++ b/examples/pendulum/pendulum_finetune_con.onnx
diff --git a/examples/pendulum/pendulum_strict.vnnlib b/examples/pendulum/pendulum_strict.vnnlib
new file mode 100644
index 0000000..d1c1167
--- /dev/null
+++ b/examples/pendulum/pendulum_strict.vnnlib
@@ -0,0 +1,21 @@
+; Strict Equivalence for Pendulum
+
+; Constant declaration
+(declare-const X_0 Real)
+(declare-const X_1 Real)
+(declare-const Y_0 Real)
+(declare-const Y_1 Real)
+(declare-const Y_2 Real)
+(declare-const Y_3 Real)
+
+; Bounded inputs: X must be within [0, 1]
+(assert (>= X_0 0.0))
+(assert (<= X_0 1.0))
+(assert (>= X_1 0.0))
+(assert (<= X_1 1.0))
+
+; Violation of strict equivalence
+(assert (or
+	(not (= Y_0 Y_2))
+	(not (= Y_1 Y_3))
+))
diff --git a/examples/tll/tllBench_n=2_N=M=8_m=1_instance_0_0.onnx b/examples/tll/tllBench_n=2_N=M=8_m=1_instance_0_0.onnx
new file mode 100644
index 0000000..a6632fb
--- /dev/null
+++ b/examples/tll/tllBench_n=2_N=M=8_m=1_instance_0_0.onnx
diff --git a/examples/tll/tllBench_n=2_N=M=8_m=1_instance_0_2.onnx b/examples/tll/tllBench_n=2_N=M=8_m=1_instance_0_2.onnx
new file mode 100644
index 0000000..b650a13
--- /dev/null
+++ b/examples/tll/tllBench_n=2_N=M=8_m=1_instance_0_2.onnx
diff --git a/examples/tll/tll_argmax.vnnlib b/examples/tll/tll_argmax.vnnlib
new file mode 100644
index 0000000..c084e52
--- /dev/null
+++ b/examples/tll/tll_argmax.vnnlib
@@ -0,0 +1,16 @@
+; Argmax Equivalence for TLL
+
+; Constant declaration
+(declare-const X_0 Real)
+(declare-const X_1 Real)
+(declare-const Y_0 Real)
+(declare-const Y_1 Real)
+
+; Bounded inputs: X must be within [0, 1]
+(assert (>= X_0 0.0))
+(assert (<= X_0 1.0))
+(assert (>= X_1 0.0))
+(assert (<= X_1 1.0))
+
+; Violation of argmax equivalence
+(assert (and (> Y_0 0.5) (< Y_1 0.5)))
diff --git a/examples/tll/tll_epsilon.vnnlib b/examples/tll/tll_epsilon.vnnlib
new file mode 100644
index 0000000..8e0902d
--- /dev/null
+++ b/examples/tll/tll_epsilon.vnnlib
@@ -0,0 +1,17 @@
+; Strict Equivalence for TLL
+
+; Constant declaration
+(declare-const X_0 Real)
+(declare-const X_1 Real)
+(declare-const Y_0 Real)
+(declare-const Y_1 Real)
+
+; Bounded inputs: X must be within [0, 1]
+(assert (>= X_0 0.0))
+(assert (<= X_0 1.0))
+(assert (>= X_1 0.0))
+(assert (<= X_1 1.0))
+
+; Violation of epsilon equivalence (epsilon = 0.1)
+(define-fun absolute ((x Real)) Real (if (>= x 0) x (- x)))
+(assert (> (absolute (- Y_0 Y_1)) 0.1))
diff --git a/examples/tll/tll_strict.vnnlib b/examples/tll/tll_strict.vnnlib
new file mode 100644
index 0000000..0079b1e
--- /dev/null
+++ b/examples/tll/tll_strict.vnnlib
@@ -0,0 +1,16 @@
+; Strict Equivalence for TLL
+
+; Constant declaration
+(declare-const X_0 Real)
+(declare-const X_1 Real)
+(declare-const Y_0 Real)
+(declare-const Y_1 Real)
+
+; Bounded inputs: X must be within [0, 1]
+(assert (>= X_0 0.0))
+(assert (<= X_0 1.0))
+(assert (>= X_1 0.0))
+(assert (<= X_1 1.0))
+
+; Violation of strict equivalence
+(assert (not (= Y_0 Y_1)))
diff --git a/examples/verify.py b/examples/verify.py
new file mode 100644
index 0000000..046ec0b
--- /dev/null
+++ b/examples/verify.py
@@ -0,0 +1,86 @@
+import sys, os
+sys.path.append(os.path.dirname(os.path.dirname(os.path.abspath(__file__))))
+
+import z3
+import nneq
+
+def check_property(onnx_a, onnx_b, vnnlib):
+    solver = nneq.Solver()
+
+    print(f"--- Checking {vnnlib} ---")
+
+    solver.load_onnx(onnx_a)
+    solver.load_onnx(onnx_b)
+    solver.load_vnnlib(vnnlib)
+
+    result = solver.check()
+
+    if result == z3.unsat:
+        print("VERIFIED (UNSAT): The networks are equivalent under this property.")
+    elif result == z3.sat:
+        print("FAILED (SAT): The networks are NOT equivalent.")
+        print("Counter-example input:")
+        print(solver.model())
+        # m = solver.model()
+        # sorted_symbols = sorted([s for s in m.decls() if s.name().startswith("X_")], key=lambda s: s.name())
+        # for s in sorted_symbols:
+            # print(f"  {s.name()} = {m[s]}")
+    else:
+        print("UNKNOWN")
+    print("")
+
+if __name__ == "__main__":
+    if len(sys.argv) <= 1:
+        print("Net not provided")
+        print("Available Nets: 'xor', 'fashion_mnist', 'iris', 'acasxu', 'tll', 'pendulum', 'double_integrator'")
+    else:
+        match sys.argv[1]:
+            case "xor":
+                net_a = "./examples/xor/xor_a.onnx"
+                net_b = "./examples/xor/xor_b.onnx"
+                strict = "./examples/xor/xor_strict.vnnlib"
+                epsilon = "./examples/xor/xor_epsilon.vnnlib"
+                argmax = "./examples/xor/xor_argmax.vnnlib"
+            case "fashion_mnist":
+                net_a = "./examples/fashion_mnist/fashion_mnist_a.onnx"
+                net_b = "./examples/fashion_mnist/fashion_mnist_b.onnx"
+                strict = "./examples/fashion_mnist/fashion_mnist_strict.vnnlib"
+                epsilon = "./examples/fashion_mnist/fashion_mnist_epsilon.vnnlib"
+                argmax = "./examples/fashion_mnist/fashion_mnist_argmax.vnnlib"
+            case "iris":
+                net_a = "./examples/iris/iris_a.onnx"
+                net_b = "./examples/iris/iris_b.onnx"
+                strict = "./examples/iris/iris_strict.vnnlib"
+                epsilon = "./examples/iris/iris_epsilon.vnnlib"
+                argmax = "./examples/iris/iris_argmax.vnnlib"
+            case "acasxu":
+                net_a = "./examples/ACASXU/ACASXU_run2a_1_1_batch_2000.onnx"
+                net_b = "./examples/ACASXU/ACASXU_run2a_1_1_batch_2000.onnx"
+                strict = "./examples/ACASXU/ACASXU_strict.vnnlib"
+                epsilon = "./examples/ACASXU/ACASXU_epsilon.vnnlib"
+                argmax = "./examples/ACASXU/ACASXU_argmax.vnnlib"
+            case "tll":
+                net_a = "./examples/tll/tllBench_n=2_N=M=8_m=1_instance_0_0.onnx"
+                net_b = "./examples/tll/tllBench_n=2_N=M=8_m=1_instance_0_2.onnx"
+                strict = "./examples/tll/tll_strict.vnnlib"
+                epsilon = "./examples/tll/tll_epsilon.vnnlib"
+                argmax = "./examples/tll/tll_argmax.vnnlib"
+            case "pendulum":
+                net_a = "./examples/pendulum/pendulum_finetune_con.onnx"
+                net_b = "./examples/pendulum/pendulum_finetune_con.onnx"
+                strict = "./examples/pendulum/pendulum_strict.vnnlib"
+                epsilon = "./examples/pendulum/pendulum_epsilon.vnnlib"
+                argmax = "./examples/pendulum/pendulum_argmax.vnnlib"
+            case "double_integrator":
+                net_a = "./examples/double_integrator/double_integrator_finetune_inv.onnx"
+                net_b = "./examples/double_integrator/double_integrator_finetune_inv.onnx"
+                strict = "./examples/double_integrator/double_integrator_strict.vnnlib"
+                epsilon = "./examples/double_integrator/double_integrator_epsilon.vnnlib"
+                argmax = "./examples/double_integrator/double_integrator_argmax.vnnlib"
+            case _:
+                print("Available Nets: 'xor', 'fashion_mnist', 'iris', 'acasxu', 'tll', 'pendulum', 'double_integrator'")
+                sys.exit()
+
+        check_property(net_a, net_b, strict)
+        check_property(net_a, net_b, epsilon)
+        check_property(net_a, net_b, argmax)
diff --git a/examples/verify_fashion_mnist.py b/examples/verify_fashion_mnist.py
deleted file mode 100644
index 91ca1ae..0000000
--- a/examples/verify_fashion_mnist.py
+++ /dev/null
@@ -1,35 +0,0 @@
-import sys, os
-sys.path.append(os.path.dirname(os.path.dirname(os.path.abspath(__file__))))
-
-import z3
-import nneq
-
-def check_property(onnx_a, onnx_b, vnnlib):
-    solver = nneq.Solver()
-    
-    print(f"--- Checking {vnnlib} ---")
-    
-    solver.load_onnx(onnx_a)
-    solver.load_onnx(onnx_b)
-    solver.load_vnnlib(vnnlib)
-    
-    result = solver.check()
-    
-    if result == z3.unsat:
-        print("VERIFIED (UNSAT): The networks are equivalent under this property.")
-    elif result == z3.sat:
-        print("FAILED (SAT): The networks are NOT equivalent.")
-        print("Counter-example input:")
-        print(solver.model())
-        # m = solver.model()
-        # sorted_symbols = sorted([s for s in m.decls() if s.name().startswith("X_")], key=lambda s: s.name())
-        # for s in sorted_symbols:
-            # print(f"  {s.name()} = {m[s]}")
-    else:
-        print("UNKNOWN")
-    print("")
-
-if __name__ == "__main__":
-    check_property("./examples/fashion_mnist/fashion_mnist_a.onnx", "./examples/fashion_mnist/fashion_mnist_b.onnx", "./examples/fashion_mnist/fashion_mnist_strict.vnnlib")
-    check_property("./examples/fashion_mnist/fashion_mnist_a.onnx", "./examples/fashion_mnist/fashion_mnist_b.onnx", "./examples/fashion_mnist/fashion_mnist_epsilon.vnnlib")
-    check_property("./examples/fashion_mnist/fashion_mnist_a.onnx", "./examples/fashion_mnist/fashion_mnist_b.onnx", "./examples/fashion_mnist/fashion_mnist_argmax.vnnlib")
diff --git a/examples/verify_xor.py b/examples/verify_xor.py
deleted file mode 100644
index a9f5e23..0000000
--- a/examples/verify_xor.py
+++ /dev/null
@@ -1,35 +0,0 @@
-import sys, os
-sys.path.append(os.path.dirname(os.path.dirname(os.path.abspath(__file__))))
-
-import z3
-import nneq
-
-def check_property(onnx_a, onnx_b, vnnlib):
-    solver = nneq.Solver()
-    
-    print(f"--- Checking {vnnlib} ---")
-    
-    solver.load_onnx(onnx_a)
-    solver.load_onnx(onnx_b)
-    solver.load_vnnlib(vnnlib)
-    
-    result = solver.check()
-    
-    if result == z3.unsat:
-        print("VERIFIED (UNSAT): The networks are equivalent under this property.")
-    elif result == z3.sat:
-        print("FAILED (SAT): The networks are NOT equivalent.")
-        print("Counter-example input:")
-        print(solver.model())
-        # m = solver.model()
-        # sorted_symbols = sorted([s for s in m.decls() if s.name().startswith("X_")], key=lambda s: s.name())
-        # for s in sorted_symbols:
-            # print(f"  {s.name()} = {m[s]}")
-    else:
-        print("UNKNOWN")
-    print("")
-
-if __name__ == "__main__":
-    check_property("./examples/xor/xor_a.onnx", "./examples/xor/xor_b.onnx", "./examples/xor/xor_strict.vnnlib")
-    check_property("./examples/xor/xor_a.onnx", "./examples/xor/xor_b.onnx", "./examples/xor/xor_epsilon.vnnlib")
-    check_property("./examples/xor/xor_a.onnx", "./examples/xor/xor_b.onnx", "./examples/xor/xor_argmax.vnnlib")
diff --git a/examples/xor/xor_argmax.vnnlib b/examples/xor/xor_argmax.vnnlib
index d38bc31..d21119b 100644
--- a/examples/xor/xor_argmax.vnnlib
+++ b/examples/xor/xor_argmax.vnnlib
@@ -11,4 +11,4 @@
 (assert (or (= X_1 0) (= X_1 1)))
 
 ; Violation of argmax equivalence
-(assert (not (= (> Y_0 0.5) (> Y_1 0.5))))
+(assert (and (> Y_0 0.5) (< Y_1 0.5)))
diff --git a/proof.md b/proof.md
index a376bb9..1290159 100644
--- a/proof.md
+++ b/proof.md
@@ -38,13 +38,15 @@ By grouping the operations we get:
 ![Y = alpha * A * B + beta * C](https://latex.codecogs.com/svg.image?Y=\alpha\cdot&space;A\cdot&space;B&plus;\beta\cdot&space;C&space;)
 
 ### Flatten
-Just identity mapping.
+Just identity mapping because the wires are always Flatten.
+![out_i ~ in_i](https://latex.codecogs.com/svg.image?out_i\sim&space;in_i)
 
 ### MatMul
-Equal to Gemm with ![alpha=1](https://latex.codecogs.com/svg.image?\inline&space;\alpha=1) and ![beta=0](https://latex.codecogs.com/svg.image?\inline&space;\beta=0).
+Equal to Gemm with ![alpha=1](https://latex.codecogs.com/svg.image?\inline&space;\alpha=1), ![beta=0](https://latex.codecogs.com/svg.image?\inline&space;\beta=0) and ![C=0](https://latex.codecogs.com/svg.image?\inline&space;&space;C=0).
 
 ### Reshape
-Just identity mapping.
+Just identity mapping because the wires always Flatten.
+![out_i ~ iin_i](https://latex.codecogs.com/svg.image?out_i\sim&space;in_i)
 
 ### Add
 ONNX Add node is defined as:
@@ -553,8 +555,8 @@ Otherwise, there exists an active pair ![A](https://latex.codecogs.com/svg.image
 By the [Soundness of Interaction Rules](#soundness-of-interaction-rules), the mathematical definition is preserved after any reduction step,
 it follows that ![[IN_{n+1}] = [IN_n]](https://latex.codecogs.com/svg.image?\inline&space;[\mathrm{IN_{n&plus;1}}]=[\mathrm{IN_n}]). By the inductive hypothesis, ![[IN_{n+1}] = [NN]](https://latex.codecogs.com/svg.image?\inline&space;[\mathrm{IN_{n&plus;1}}]=[\mathrm{NN}]).
 
-  By the principle of mathematical induction, the Interaction Net remains semantically equivalent to the original 
-  Neural Network at every step of the reduction process.
+By the principle of mathematical induction, the Interaction Net remains semantically equivalent to the original 
+Neural Network at every step of the reduction process.
 
 Since Interaction Nets are confluent, the reduced mathematical expression is unique regardless
 of order in which rules are applied.
diff --git a/proof.norg b/proof.norg
index 36851a9..7bd9e25 100644
--- a/proof.norg
+++ b/proof.norg
@@ -48,13 +48,15 @@ version: 1.1.1
 		$Y = alpha * A * B + beta * C$
 
 *** Flatten
-		Just identity mapping.
+		Just identity mapping because the wires are always Flatten.
+		$o_i ~ i_i$
 
 *** MatMul
-		Equal to Gemm with $alpha=1$ and $beta=0$.
+		Equal to Gemm with $alpha=1$, $beta=0$ and $C=0$.
 
 *** Reshape
-		Just identity mapping.
+		Just identity mapping because the wires always Flatten.
+		$o_i ~ i_i$
 
 *** Add
 		ONNX Add node is defined as:
@@ -491,7 +493,7 @@ version: 1.1.1
 		 $IF false THEN k ELSE 0 = 0 => 0 = 0$
 		 $$
 
-** Soundness of Reduction 
+** Soundness of Reduction
 	 Let $IN_0$ be the Interaction Net translated from a Neural Network $NN$. Let $IN_n$ be the state of the net
 	 after $n$ reduction steps. Then $\forall n \in N$, $[IN_n] = [NN]$.