:

diff --git a/Robust/src/Benchmarks/SingleTM/Intruder/extractLines b/Robust/src/Benchmarks/SingleTM/Intruder/extractLines
new file mode 100755 (executable)
index 0000000..c75e572
--- /dev/null
+++ b/Robust/src/Benchmarks/SingleTM/Intruder/extractLines
@@ -0,0 +1,3 @@
+#!/bin/sh
+lines=$(grep -n "#" $1 | cut -d: -f1 | sed '1q')
+sed '/^#/d' $1 > ttt$1