From: Mart Lubbers <mart@martlubbers.net>
Date: Sun, 29 Nov 2015 10:04:59 +0000 (+0100)
Subject: try for 3b
X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=84f47d6d66fda97c99ff0ec377b3754ebf33bf9b;p=ar1516.git

try for 3b
---

diff --git a/a2/src/3b.prv9 b/a2/src/3b.prv9
new file mode 100644
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
--- 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