try for 3b

diff --git a/a2/src/3b.prv9 b/a2/src/3b.prv9
new file mode 100644 (file)
index 0000000..12c9aa4
--- /dev/null
+++ b/a2/src/3b.prv9
@@ -0,0 +1,6 @@
+formulas(assumptions).
+a(x, a(y, a(z, u))) -> a(y, a(z, a(x, u))).
+end_of_list.
+formulas(goals).
+a(b, a(c, a(d, a(e, a(f, a(b, g)))))). 
+end_of_list.

diff --git a/a2/src/path.sh b/a2/src/path.sh
index d7dfea0..3603923 100644 (file)
--- a/a2/src/path.sh
+++ b/a2/src/path.sh
@@ -1,2 +1,3 @@
 export PATH=$PATH:/home/mart/downloads/NuSMV-2.5.4/nusmv
 export PATH=$PATH:/home/mart/projects/NuSMV-2.6.0-Linux/bin
+export PATH=$PATH:/home/mart/projects/LADR-2009-11A/bin