diff --git a/all.itarget b/all.itarget
index 0167f124..6eb81b74 100644
--- a/all.itarget
+++ b/all.itarget
@@ -9,6 +9,7 @@ src/while/while_prove.native
 src/while/while_abduce.native
 src/extended_while/extended_while_prove.native  
 src/temporal_ctl/temporal_ctl_prove.native
+src/temporal_ctl/temporal_ctl_prove.byte
 src/temporal_ltl/temporal_ltl_prove.native
 #src/cyclist.docdir/index.html
 src/seplog/sl.top
diff --git a/benchmarks/temporal/cyclic_list_nd.ctl b/benchmarks/temporal/cyclic_list_nd.ctl
new file mode 100644
index 00000000..641dc8ec
--- /dev/null
+++ b/benchmarks/temporal/cyclic_list_nd.ctl
@@ -0,0 +1,11 @@
+fields: next;
+precondition: List(x,x);
+property: AG(List(x,x));
+while x=x do
+if * then
+  x:=x.next
+else
+  y:=new();
+  y.next:=x
+fi
+od
\ No newline at end of file
diff --git a/benchmarks/temporal/fairness/test1.fctl b/benchmarks/temporal/fairness/test1.fctl
new file mode 100644
index 00000000..bcc29ef5
--- /dev/null
+++ b/benchmarks/temporal/fairness/test1.fctl
@@ -0,0 +1,7 @@
+fields: next;
+precondition:x=x;
+property: AF(final);
+while * do
+      skip	
+od;
+skip
\ No newline at end of file
diff --git a/benchmarks/temporal/fairness/test2.fctl b/benchmarks/temporal/fairness/test2.fctl
new file mode 100644
index 00000000..1ed030db
--- /dev/null
+++ b/benchmarks/temporal/fairness/test2.fctl
@@ -0,0 +1,7 @@
+fields: next;
+precondition:x=x;
+property: AF(final);
+while x=x do
+  skip 	
+od;
+skip
\ No newline at end of file
diff --git a/benchmarks/temporal/fairness/test3.fctl b/benchmarks/temporal/fairness/test3.fctl
new file mode 100644
index 00000000..cebe9fae
--- /dev/null
+++ b/benchmarks/temporal/fairness/test3.fctl
@@ -0,0 +1,10 @@
+fields: next;
+precondition:x->x';
+property: AF(emp);
+while x=x do
+  if * then
+     free(x)
+  else
+     skip
+  fi
+od
\ No newline at end of file
diff --git a/benchmarks/temporal/fairness/test4.fctl b/benchmarks/temporal/fairness/test4.fctl
new file mode 100644
index 00000000..5212964e
--- /dev/null
+++ b/benchmarks/temporal/fairness/test4.fctl
@@ -0,0 +1,12 @@
+fields: next;
+precondition:x->x';
+property: AF(emp);
+while x=x do
+  if * then
+     free(x)
+  else
+     while * do
+       skip
+     od
+  fi
+od
\ No newline at end of file
diff --git a/benchmarks/temporal/fairness/test5.fctl b/benchmarks/temporal/fairness/test5.fctl
new file mode 100644
index 00000000..038427db
--- /dev/null
+++ b/benchmarks/temporal/fairness/test5.fctl
@@ -0,0 +1,14 @@
+fields: next;
+precondition: tmp->x * ls(x,nil);
+property: AF(emp);
+while x=x do
+  if * then
+     while tmp!=nil do
+	free(tmp);
+	tmp:= x;
+	x:= x.next
+     od
+  else
+     skip
+  fi
+od
\ No newline at end of file
diff --git a/benchmarks/temporal/fairness/test6.fctl b/benchmarks/temporal/fairness/test6.fctl
new file mode 100644
index 00000000..fa1637d0
--- /dev/null
+++ b/benchmarks/temporal/fairness/test6.fctl
@@ -0,0 +1,16 @@
+fields: next;
+precondition: ls(x,nil);
+property: AF(emp);
+while x=x do
+  if * then
+     while x!=nil do
+       temp:=x.next;
+       free(x);
+       x:=temp
+     od
+  else
+    while * do
+       skip
+     od	
+  fi
+od
\ No newline at end of file
diff --git a/benchmarks/temporal/fairness/test7.fctl b/benchmarks/temporal/fairness/test7.fctl
new file mode 100644
index 00000000..bdf2afe5
--- /dev/null
+++ b/benchmarks/temporal/fairness/test7.fctl
@@ -0,0 +1,18 @@
+fields: next;
+precondition: ls(x,nil);
+property: AF(emp);
+while x=x do
+  if * then
+     while x!=nil do
+       temp:=x.next;
+       free(x);
+       x:=temp
+     od
+  else
+    while * do
+       y:=new();
+       y.next:=x;
+       x:=y
+     od	
+  fi
+od
\ No newline at end of file
diff --git a/benchmarks/temporal/fairness/test8.fctl b/benchmarks/temporal/fairness/test8.fctl
new file mode 100644
index 00000000..55eb5628
--- /dev/null
+++ b/benchmarks/temporal/fairness/test8.fctl
@@ -0,0 +1,19 @@
+fields: next;
+precondition: ls(x,nil);
+property: AG(AF(emp));
+while x=x do
+  if * then
+     while x!=nil do
+       temp:=x;
+       x:=x.next;
+       free(temp);
+       temp:=nil
+     od
+  else
+    while * do
+       y:=new();
+       y.next:=x;
+       x:=y
+     od	
+  fi
+od
\ No newline at end of file
diff --git a/benchmarks/temporal/gc/nd_af_ag_emp.ctl b/benchmarks/temporal/gc/nd_af_ag_emp.ctl
new file mode 100644
index 00000000..b38dea01
--- /dev/null
+++ b/benchmarks/temporal/gc/nd_af_ag_emp.ctl
@@ -0,0 +1,18 @@
+fields: next;
+precondition:ls(x,nil);
+property: AF(AG(emp));
+while x=x do
+    if * then
+        while x!=nil do
+            temp:=x.next;
+            free(x);
+            x:=temp
+        od
+    else
+        while * do
+	    y:=new();
+	    y.next:=x;
+	    x:=y
+	od
+    fi
+od
\ No newline at end of file
diff --git a/benchmarks/temporal/gc/nd_af_eg_emp.ctl b/benchmarks/temporal/gc/nd_af_eg_emp.ctl
index 3a382ac8..93007b4c 100644
--- a/benchmarks/temporal/gc/nd_af_eg_emp.ctl
+++ b/benchmarks/temporal/gc/nd_af_eg_emp.ctl
@@ -1,6 +1,6 @@
 fields: next;
 precondition:ls(x,nil);
-property: AG(EG(ls(x,nil)));
+property: AF(EG(emp));
 while x=x do
     if * then
         while x!=nil do
diff --git a/benchmarks/temporal/gc/nd_af_emp.ctl b/benchmarks/temporal/gc/nd_af_emp.ctl
new file mode 100644
index 00000000..76ff07a9
--- /dev/null
+++ b/benchmarks/temporal/gc/nd_af_emp.ctl
@@ -0,0 +1,18 @@
+fields: next;
+precondition:x!=nil * ls(x,nil);
+property: AF(emp);
+while x=x do
+    if * then
+        while x!=nil do
+            temp:=x.next;
+            free(x);
+            x:=temp
+        od
+    else
+        while * do
+	    y:=new();
+	    y.next:=x;
+	    x:=y
+	od
+    fi
+od
\ No newline at end of file
diff --git a/benchmarks/temporal/gc/nd_ag_af_emp.ctl b/benchmarks/temporal/gc/nd_ag_af_emp.ctl
new file mode 100644
index 00000000..87576673
--- /dev/null
+++ b/benchmarks/temporal/gc/nd_ag_af_emp.ctl
@@ -0,0 +1,18 @@
+fields: next;
+precondition:ls(x,nil);
+property: AG(AF(emp));
+while x=x do
+    if * then
+        while x!=nil do
+            temp:=x.next;
+            free(x);
+            x:=temp
+        od
+    else
+        while * do
+	    y:=new();
+	    y.next:=x;
+	    x:=y
+	od
+    fi
+od
\ No newline at end of file
diff --git a/benchmarks/temporal/gc/nd_ag_eg_ls.ctl b/benchmarks/temporal/gc/nd_ag_eg_ls.ctl
new file mode 100644
index 00000000..0cb9b979
--- /dev/null
+++ b/benchmarks/temporal/gc/nd_ag_eg_ls.ctl
@@ -0,0 +1,19 @@
+fields: next;
+precondition:ls(x,nil);
+property: AG(EG(ls(x,nil)));
+while x=x do
+    if * then
+        while x!=nil do
+            temp:=x;
+	    x:=x.next;
+            free(temp);
+	    temp:=nil
+        od
+    else
+        while * do
+	    y:=new();
+	    y.next:=x;
+	    x:=y
+	od
+    fi
+od
\ No newline at end of file
diff --git a/benchmarks/temporal/microbench/afagp_s.ctl b/benchmarks/temporal/microbench/afagp_s.ctl
index 905a32f3..53532a78 100644
--- a/benchmarks/temporal/microbench/afagp_s.ctl
+++ b/benchmarks/temporal/microbench/afagp_s.ctl
@@ -1,5 +1,5 @@
 fields: next;
-precondition: current=zero * x=zero * zero->one * one->two * two->three * three->four * four->five * FALSE->false' * TRUE->true' * break=FALSE;
+precondition: current=four * x=zero * zero->one * one->two * two->three * three->four * four->five * FALSE->false' * TRUE->true' * break=FALSE;
 property: AF(AG(x=one));
 while break=FALSE do
   if current=five then
diff --git a/benchmarks/temporal/microbench/afef_s.ctl b/benchmarks/temporal/microbench/afef_s.ctl
index 91fba7a9..e551d970 100644
--- a/benchmarks/temporal/microbench/afef_s.ctl
+++ b/benchmarks/temporal/microbench/afef_s.ctl
@@ -1,5 +1,5 @@
 fields: next;
-precondition: current=zero * x=zero * zero->one * one->two * two->three * three->four * four->five * FALSE->false' * TRUE->true' * break=FALSE;
+precondition: current=four * x=zero * zero->one * one->two * two->three * three->four * four->five * FALSE->false' * TRUE->true' * break=FALSE;
 property: AF(EF(x=one));
 while break=FALSE do
   if current=five then
@@ -9,7 +9,7 @@ while break=FALSE do
   fi
 od;
 break:=FALSE;
-current:=zero;
+current:=four;
 while break=FALSE do
   if current=five then
     break:=TRUE
diff --git a/benchmarks/temporal/microbench/afp_s.ctl b/benchmarks/temporal/microbench/afp_s.ctl
index a781a619..4c498875 100644
--- a/benchmarks/temporal/microbench/afp_s.ctl
+++ b/benchmarks/temporal/microbench/afp_s.ctl
@@ -1,14 +1,10 @@
 fields: next;
-precondition: n->one * one->zero * zero->nil * p=zero * current=n * FALSE->false' * TRUE->true';
-property: AF(p=one);
-while break=FALSE do
-  if current=zero then
-    break:=TRUE
+precondition: x=zero * zero->one * one->two * two->three * three->four * four->five;
+property: AF(x!=zero);
+while TRUE=TRUE do
+  if * then
+    x:=x.next
   else
-    current:=current.next
+    x:=zero
   fi
-od;
-p:=one;
-while TRUE=TRUE do
-  skip
-od
+od
\ No newline at end of file
diff --git a/benchmarks/temporal/microbench/afp_s_old.ctl b/benchmarks/temporal/microbench/afp_s_old.ctl
new file mode 100644
index 00000000..49ec0b07
--- /dev/null
+++ b/benchmarks/temporal/microbench/afp_s_old.ctl
@@ -0,0 +1,14 @@
+fields: next;
+precondition: n->one * one->zero * zero->nil * p=zero * current=n * FALSE->false' * TRUE->true';
+property: AF(p=one);
+while break=FALSE do
+  if current=zero then
+    break:=TRUE
+  else
+    current:=current.next
+  fi
+od;
+p:=one;
+while TRUE=TRUE do
+  skip
+od
\ No newline at end of file
diff --git a/benchmarks/temporal/microbench/agafp_s.ctl b/benchmarks/temporal/microbench/agafp_s.ctl
index 08af911a..8772b0aa 100644
--- a/benchmarks/temporal/microbench/agafp_s.ctl
+++ b/benchmarks/temporal/microbench/agafp_s.ctl
@@ -1,18 +1,18 @@
 fields: next;
-precondition: current=zero * x=zero * zero->one * one->two * two->three * three->four * four->five * FALSE->false' * TRUE->true';
-property: AG(AF(x=one));
-if * then
-   x:=one
-else
-  while break=FALSE do
-    if current=five then
-      break:=TRUE
-    else
-      current:=current.next
-    fi
-  od;
-  x:=one
-fi;
-while TRUE=TRUE do
+precondition: false!=true * break=false * x=one * zero->one * one->two * two->three * three->four * four->five;
+property: AG(AF(x!=zero));
+while break!=true do
+  if * then
+    x:=x.next
+  else
+    x:=zero
+  fi;
+  if x!=zero then
+    break:=true
+  else
+    skip
+  fi
+od;
+while break=break do
   skip
-od
+od
\ No newline at end of file
diff --git a/benchmarks/temporal/microbench/agafp_s_old.ctl b/benchmarks/temporal/microbench/agafp_s_old.ctl
new file mode 100644
index 00000000..44e211a2
--- /dev/null
+++ b/benchmarks/temporal/microbench/agafp_s_old.ctl
@@ -0,0 +1,18 @@
+fields: next;
+precondition: current=four * x=zero * zero->one * one->two * two->three * three->four * four->five * FALSE->false' * TRUE->true';
+property: AG(AF(x=one));
+if * then
+   x:=one
+else
+  while break=FALSE do
+    if current=five then
+      break:=TRUE
+    else
+      current:=current.next
+    fi
+  od;
+  x:=one
+fi;
+while TRUE=TRUE do
+  skip
+od
diff --git a/benchmarks/temporal/microbench/agef_s_heap.ctl b/benchmarks/temporal/microbench/agef_s_heap.ctl
index d4efe873..5440ff21 100644
--- a/benchmarks/temporal/microbench/agef_s_heap.ctl
+++ b/benchmarks/temporal/microbench/agef_s_heap.ctl
@@ -1,5 +1,5 @@
 fields: next;
-precondition: ls(x,nil);
+precondition: ls(y,x) * ls(x,nil);
 property: AG(EF(x=nil));
 while x!=nil do
 if * then
@@ -7,7 +7,11 @@ if * then
    x:=new();
    x.next:=temp
 else
-  x:=x.next
+  if x!=nil then
+    x:=x.next
+  else
+    skip
+  fi
 fi
 od;
 x:=nil;
diff --git a/benchmarks/temporal/microbench/ageg_s_heap_nd.ctl b/benchmarks/temporal/microbench/ageg_s_heap_nd.ctl
new file mode 100644
index 00000000..14ca3a32
--- /dev/null
+++ b/benchmarks/temporal/microbench/ageg_s_heap_nd.ctl
@@ -0,0 +1,13 @@
+fields: left,right;
+precondition: x!=nil * bt(x);
+property: AG(AF(x!=nil));
+while x=x do
+  if * then
+    temp:=new();
+    temp.left:=x;
+    temp.right:=nil;
+    x:=temp
+  else
+    x:=nil
+  fi
+od
\ No newline at end of file
diff --git a/benchmarks/temporal/microbench/agimpef_s.ctl b/benchmarks/temporal/microbench/agimpef_s.ctl
index 9a18acd8..51df2af4 100644
--- a/benchmarks/temporal/microbench/agimpef_s.ctl
+++ b/benchmarks/temporal/microbench/agimpef_s.ctl
@@ -1,5 +1,5 @@
 fields: next;
-precondition: current=zero * check=zero * p=zero * zero->one * one->two * two->three * three->four * four->five * FALSE->false' * TRUE->true' * break=FALSE;
+precondition: current=four * check=zero * p=zero * zero->one * one->two * two->three * three->four * four->five * FALSE->false' * TRUE->true' * break=FALSE;
 property: AG(\/(check=zero,EF(p=one)));
 check:=one;
 while break=FALSE do
diff --git a/benchmarks/temporal/microbench/agp_s_heap.ctl b/benchmarks/temporal/microbench/agp_s_heap.ctl
index 6ec4a573..eeabd6ce 100644
--- a/benchmarks/temporal/microbench/agp_s_heap.ctl
+++ b/benchmarks/temporal/microbench/agp_s_heap.ctl
@@ -1,17 +1,12 @@
 fields: next;
-precondition: x!=nil * ls(x,nil);
-property: AG(x!=nil);
+precondition: ls(y',x) * ls(x,nil);
+property: AG(ls(y',x) * ls(x,nil));
 while x=x do
-  if * then
-    temp:=new();
-    temp.next:=x;
-    x:=temp
-  else
-    temp:=new();
-    temp.next:=x;
-    x:=temp
-  fi
-od;
-while x=x do
-  skip
+    if x!= nil then
+      temp:=x;
+      x := x.next;
+      temp:=nil
+    else
+      skip
+    fi
 od
\ No newline at end of file
diff --git a/benchmarks/temporal/microbench/efp_s.ctl b/benchmarks/temporal/microbench/efp_s.ctl
index a1e3b20a..323b4814 100644
--- a/benchmarks/temporal/microbench/efp_s.ctl
+++ b/benchmarks/temporal/microbench/efp_s.ctl
@@ -1,5 +1,5 @@
 fields: next;
-precondition: x=one * zero->one * one->two * two->three * three->four * four->five * FALSE->false' * TRUE->true';
+precondition: x=four * zero->one * one->two * two->three * three->four * four->five * FALSE->false' * TRUE->true';
 property: EF(x=five);
 while TRUE=TRUE do
   if * then
diff --git a/benchmarks/temporal/microbench/egimpaf.ctl b/benchmarks/temporal/microbench/egimpaf.ctl
new file mode 100644
index 00000000..26e28f29
--- /dev/null
+++ b/benchmarks/temporal/microbench/egimpaf.ctl
@@ -0,0 +1,18 @@
+fields: next;
+precondition: current=four * check=zero * p=zero * zero->one * one->two * two->three * three->four * four->five * FALSE->false' * TRUE->true' * break=FALSE;
+property: EG(\/(x=zero,AF(p=one)));
+while TRUE=TRUE do
+  check:=zero.next;
+  if * then
+    while break=FALSE do
+      if current=five then
+        break:=TRUE
+      else
+	  current:=current.next
+      fi
+    od;
+    p:=one
+  else
+    p:=zero
+  fi
+od
\ No newline at end of file
diff --git a/benchmarks/temporal/microbench/egimpef_s.ctl b/benchmarks/temporal/microbench/egimpef_s.ctl
index 242ae2ca..aa0018b9 100644
--- a/benchmarks/temporal/microbench/egimpef_s.ctl
+++ b/benchmarks/temporal/microbench/egimpef_s.ctl
@@ -1,5 +1,5 @@
 fields: next;
-precondition: current=zero * check=zero * p=zero * zero->one * one->two * two->three * three->four * four->five * FALSE->false' * TRUE->true' * break=FALSE;
+precondition: current=four * check=zero * p=zero * zero->one * one->two * two->three * three->four * four->five * FALSE->false' * TRUE->true' * break=FALSE;
 property: EG(\/(x=zero,EF(p=one)));
 while TRUE=TRUE do
   check:=zero.next;
diff --git a/benchmarks/temporal/systems/acqrel_afag.ctl b/benchmarks/temporal/systems/acqrel_afag.ctl
new file mode 100644
index 00000000..90efb686
--- /dev/null
+++ b/benchmarks/temporal/systems/acqrel_afag.ctl
@@ -0,0 +1,29 @@
+fields: next;
+precondition: a=nil * r=nil * flag->f' * x->x' * three->two * two->one * one->nil;
+property: AF(AG(r=nil));
+while flag!=nil do
+    if * then
+	free(flag);
+        flag:=nil
+    else
+	skip
+    fi;
+    if flag!=nil then
+	x:=new();
+	x.next:=three;
+        a:=new();
+	free(a);
+	a:=nil;
+	while x=x do
+	    skip
+	od;
+	r:=new();
+	free(r);
+	r:=nil
+    else
+	skip
+    fi
+od;
+while flag=flag do
+    skip
+od
diff --git a/benchmarks/temporal/systems/acqrel_afeg.ctl b/benchmarks/temporal/systems/acqrel_afeg.ctl
new file mode 100644
index 00000000..77062232
--- /dev/null
+++ b/benchmarks/temporal/systems/acqrel_afeg.ctl
@@ -0,0 +1,29 @@
+fields: next;
+precondition: a=nil * r=nil * flag->f' * x->x' * three->two * two->one * one->nil;
+property: AF(EG(r=nil));
+while flag!=nil do
+    if * then
+	free(flag);
+        flag:=nil
+    else
+	skip
+    fi;
+    if flag!=nil then
+	x:=new();
+	x.next:=three;
+        a:=new();
+	free(a);
+	a:=nil;
+	while x!=nil do
+	    x:=x.next
+	od;
+	r:=new();
+	free(r);
+	r:=nil
+    else
+	skip
+    fi
+od;
+while flag=flag do
+    skip
+od
diff --git a/benchmarks/temporal/systems/acqrel_agaf.ctl b/benchmarks/temporal/systems/acqrel_agaf.ctl
index e2bdbf24..077cf0d5 100644
--- a/benchmarks/temporal/systems/acqrel_agaf.ctl
+++ b/benchmarks/temporal/systems/acqrel_agaf.ctl
@@ -10,7 +10,7 @@ while flag!=nil do
     fi;
     if flag!=nil then
 	x:=new();
-	x.next:=three;
+	x.next:=one;
         a:=new();
 	free(a);
 	a:=nil;
diff --git a/benchmarks/temporal/systems/acqrel_agef.ctl b/benchmarks/temporal/systems/acqrel_agef.ctl
index a4693629..7253cd85 100644
--- a/benchmarks/temporal/systems/acqrel_agef.ctl
+++ b/benchmarks/temporal/systems/acqrel_agef.ctl
@@ -1,5 +1,5 @@
 fields: next;
-precondition: a=nil * r=nil * flag->f' * x->x' * three->two * two->one * one->nil;
+precondition: temp=x * a=nil * r=nil * flag->f' * x->x' * three->two * two->one * one->nil;
 property: AG(\/(a=nil,EF(r!=nil)));
 while flag!=nil do
     if * then
@@ -10,12 +10,15 @@ while flag!=nil do
     fi;
     if flag!=nil then
 	x:=new();
-	x.next:=three;
+	x.next:=one;
         a:=new();
 	free(a);
 	a:=nil;
 	while x!=nil do
-	    x:=x.next
+	    temp:=x;
+	    x:=x.next;
+	    free(temp);
+	    temp:=nil
 	od;
 	r:=new();
 	free(r);
diff --git a/benchmarks/temporal/systems/heap_ar_af_nd.ctl b/benchmarks/temporal/systems/heap_ar_af_nd.ctl
new file mode 100644
index 00000000..698142ed
--- /dev/null
+++ b/benchmarks/temporal/systems/heap_ar_af_nd.ctl
@@ -0,0 +1,16 @@
+fields: next;
+precondition: a->zero * r->zero * ls(x,nil);
+property:AF(a->one * r->one * emp);
+while * do
+  if * do 
+    a.next:=one
+  else
+    skip
+  fi
+od
+while x!=nil do
+      temp:=x;
+      x:=x.next;
+      free(temp)
+od;
+r.next:=one
\ No newline at end of file
diff --git a/benchmarks/temporal/systems/heap_ar_nt_agaf.ctl b/benchmarks/temporal/systems/heap_ar_nt_agaf.ctl
index 28216796..e3489f49 100644
--- a/benchmarks/temporal/systems/heap_ar_nt_agaf.ctl
+++ b/benchmarks/temporal/systems/heap_ar_nt_agaf.ctl
@@ -1,8 +1,7 @@
 fields: next;
 precondition: flag=false * a->zero * r->zero * ls(x,nil);
-property:AG(\/(flag=false,AF(a->one * r->one * emp)));
+property:AG(AF(a->one * r->one * emp));
 while x=x do
-if * then
 flag:=true;
 a.next:=one;
 while x!=nil do
@@ -11,7 +10,4 @@ while x!=nil do
       free(temp)
 od;
 r.next:=one
-else
-flag:=false
-fi
 od
\ No newline at end of file
diff --git a/benchmarks/temporal/systems/heap_ar_nt_nd_af_simple.ctl b/benchmarks/temporal/systems/heap_ar_nt_nd_af_simple.ctl
new file mode 100644
index 00000000..7e60e9e4
--- /dev/null
+++ b/benchmarks/temporal/systems/heap_ar_nt_nd_af_simple.ctl
@@ -0,0 +1,14 @@
+fields: next;
+precondition: one!=zero * a->zero * r->zero;
+property:AF(a->one * r->one);
+while x=x do
+  if * then
+    a.next:=one;
+    while * do
+      skip
+    od;
+    r.next:=one
+  else
+    skip
+  fi
+od
\ No newline at end of file
diff --git a/benchmarks/temporal/systems/heap_ar_nt_nd_agaf.ctl b/benchmarks/temporal/systems/heap_ar_nt_nd_agaf.ctl
new file mode 100644
index 00000000..1a96ff9f
--- /dev/null
+++ b/benchmarks/temporal/systems/heap_ar_nt_nd_agaf.ctl
@@ -0,0 +1,17 @@
+fields: next;
+precondition: flag=false * a->zero * r->zero * ls(x,nil);
+property:AG(\/(flag=false,AF(a->one * r->one * emp)));
+while x=x do
+  if * then
+    flag:=true;
+    a.next:=one;
+    while x!=nil do
+      temp:=x;
+      x:=x.next;
+      free(temp)
+    od;
+    r.next:=one
+  else
+    flag:=false
+  fi
+od
\ No newline at end of file
diff --git a/benchmarks/temporal/systems/heap_ar_nt_nd_agaf_simple.ctl b/benchmarks/temporal/systems/heap_ar_nt_nd_agaf_simple.ctl
new file mode 100644
index 00000000..349a22d2
--- /dev/null
+++ b/benchmarks/temporal/systems/heap_ar_nt_nd_agaf_simple.ctl
@@ -0,0 +1,14 @@
+fields: next;
+precondition: one!=zero * a->zero * r->zero;
+property:AG(AF(a->one * r->one));
+while x=x do
+  if * then
+    a.next:=one;
+    while * do
+      skip
+    od;
+    r.next:=one
+  else
+    skip
+  fi
+od
\ No newline at end of file
diff --git a/benchmarks/temporal/systems/pgarch_afeg.ctl b/benchmarks/temporal/systems/pgarch_afeg.ctl
new file mode 100644
index 00000000..c3e0bd46
--- /dev/null
+++ b/benchmarks/temporal/systems/pgarch_afeg.ctl
@@ -0,0 +1,49 @@
+fields: next;
+precondition: wakend->nil * sigup->a' * flag->b';
+property: AF(EG(wakend=nil));
+while flag!=nil do
+      if sigup!=nil then
+	 free(sigup);
+      	 sigup:=nil;
+	 skip;
+	 if * then
+	    free(flag);
+	    flag:=nil
+	 else
+	    skip
+	 fi
+       else
+         skip
+       fi;
+       if flag!=nil then
+           if wakend!=nil then
+	       free(wakend);
+	       wakend:=nil;
+	       skip;
+	       skip
+	   else
+	       skip
+	   fi;
+	   if sigup!=nil then
+	       if * then
+		   wakend:=new();
+	           wakend.next:=nil
+	       else
+	           skip
+	       fi
+	   else
+	       skip
+	   fi;
+	   if * then
+	       free(flag);
+	       flag:=nil
+	   else
+	       skip
+	   fi
+       else
+           skip
+       fi
+od;
+while one=one do
+    skip
+od
diff --git a/benchmarks/temporal/systems/st88b_afag.ctl b/benchmarks/temporal/systems/st88b_afag.ctl
new file mode 100644
index 00000000..c7f90ba9
--- /dev/null
+++ b/benchmarks/temporal/systems/st88b_afag.ctl
@@ -0,0 +1,42 @@
+fields: next,prev;
+precondition: flag1->a' * flag2->b' * flag3->c' * three->nil,two * two->three,one * one->two,nil * WItemsNum->nil,nil;
+property: AF(AG(flag1->a' * three->nil,two * two->three,one * one->two,nil * WItemsNum->nil,nil));
+while flag1!=nil do
+    while flag2!=nil do
+	current:=WItemsNum.next;
+        if current=nil then
+	    free(flag2);
+	    flag2:=nil
+	else
+	    skip
+	fi;
+	if flag2!=nil then 
+	    if current=nil then
+	        WItemsNum.next:=two;
+		WItemsNum.prev:=nil
+	    else
+		nNum:=WItemsNum.next;
+		nnNum:=nNum.next;
+	        WItemsNum.next:=nnNum;
+		WItemsNum.prev:=nNum
+	    fi
+	else
+	    skip
+	fi
+    od;
+    while flag3!=nil do
+	current:=WItemsNum.next;
+	if current=nil then
+	    free(flag3);
+	    flag3:=nil
+	else
+	    pNum:=WItemsNum.prev;
+	    ppNum:=pNum.prev;
+            WItemsNum.next:=pNum;
+	    WItemsNum.prev:=ppNum
+	fi
+    od
+od;
+while WItemsNum=WItemsNum do
+    skip
+od
diff --git a/benchmarks/temporal/systems/st88b_afeg.ctl b/benchmarks/temporal/systems/st88b_afeg.ctl
new file mode 100644
index 00000000..98044402
--- /dev/null
+++ b/benchmarks/temporal/systems/st88b_afeg.ctl
@@ -0,0 +1,42 @@
+fields: next,prev;
+precondition: flag1->a' * flag2->b' * flag3->c' * three->nil,two * two->three,one * one->two,nil * WItemsNum->nil,nil;
+property: AF(EG(flag1->a' * three->nil,two * two->three,one * one->two,nil * WItemsNum->nil,nil));
+while flag1!=nil do
+    while flag2!=nil do
+	current:=WItemsNum.next;
+        if current=nil then
+	    free(flag2);
+	    flag2:=nil
+	else
+	    skip
+	fi;
+	if flag2!=nil then 
+	    if current=nil then
+	        WItemsNum.next:=two;
+		WItemsNum.prev:=nil
+	    else
+		nNum:=WItemsNum.next;
+		nnNum:=nNum.next;
+	        WItemsNum.next:=nnNum;
+		WItemsNum.prev:=nNum
+	    fi
+	else
+	    skip
+	fi
+    od;
+    while flag3!=nil do
+	current:=WItemsNum.next;
+	if current=nil then
+	    free(flag3);
+	    flag3:=nil
+	else
+	    pNum:=WItemsNum.prev;
+	    ppNum:=pNum.prev;
+            WItemsNum.next:=pNum;
+	    WItemsNum.prev:=ppNum
+	fi
+    od
+od;
+while WItemsNum=WItemsNum do
+    skip
+od
diff --git a/benchmarks/temporal/systems/st88b_efag.ctl b/benchmarks/temporal/systems/st88b_efag.ctl
index 297cbee8..69b9aa3e 100644
--- a/benchmarks/temporal/systems/st88b_efag.ctl
+++ b/benchmarks/temporal/systems/st88b_efag.ctl
@@ -1,6 +1,6 @@
 fields: next,prev;
-precondition: flag1->a' * flag2->b' * flag3->c' * three->nil,two * two->three,one * one->two,nil * WItemsNum->nil,nil;
-property: EF(AG(WItemsNum->nil,nil));
+precondition: WItemsNum!= nil *WItemsNum->nil,nil;
+property: EF(AG(WItemsNum!= nil *WItemsNum->nil,nil));
 current:=WItemsNum.next;
 while current=nil do
     skip
diff --git a/benchmarks/temporal/systems/st88b_efeg.ctl b/benchmarks/temporal/systems/st88b_efeg.ctl
index 0e01cbbf..ea1c14d2 100644
--- a/benchmarks/temporal/systems/st88b_efeg.ctl
+++ b/benchmarks/temporal/systems/st88b_efeg.ctl
@@ -1,6 +1,6 @@
 fields: next,prev;
 precondition: flag1->a' * flag2->b' * flag3->c' * three->nil,two * two->three,one * one->two,nil * WItemsNum->nil,nil;
-property: EF(EG(WItemsNum->nil,nil));
+property: EF(EG(flag1->a' * three->nil,two * two->three,one * one->two,nil * WItemsNum->nil,nil));
 while flag1!=nil do
     while flag2!=nil do
 	current:=WItemsNum.next;
diff --git a/src/generic/fair_soundcheck.ml b/src/generic/fair_soundcheck.ml
index eb7905c5..73452955 100644
--- a/src/generic/fair_soundcheck.ml
+++ b/src/generic/fair_soundcheck.ml
@@ -10,13 +10,13 @@ external set_fair_trace_pair : int -> int -> int -> int -> unit = "set_fair_trac
 external set_fair_progress_pair : int -> int -> int -> int -> unit = "set_fair_progress_pair" ;;
 external check_fair_soundness : unit -> bool = "check_fair_soundness" ;;
 external set_initial_fair_vertex : int -> unit = "set_initial_fair_vertex" ;;
-external set_fairness_constraint : int -> int -> unit = "set_fairness_constraint" ;;
+external set_fairness_constraint : int -> int -> int -> int -> unit = "set_fairness_constraint" ;;
   
 type fair_abstract_node =
-    bool * Util.Tags.t * ((int * Util.TagPairs.t * Util.TagPairs.t) list)
+    (int*int) option * Util.Tags.t * ((int * Util.TagPairs.t * Util.TagPairs.t) list)
 type t = fair_abstract_node Int.Map.t
 			    
-let is_fair (fair,tags,subg) = fair
+let is_fair (fair,tags,subg) = Option.is_some fair
 let get_tags (fair,tags,subg) = tags
 let get_subg ((fair,tags,subg):fair_abstract_node) : (int * Util.TagPairs.t * Util.TagPairs.t) list = subg
 
@@ -45,7 +45,7 @@ let fathers_grandchild prf idx n =
 
 let pp_proof_node fmt n =
   let aux fmt (fair, tags, subg) =
-    Format.printf "fair= %a, tags=%a " Format.pp_print_bool fair Tags.pp tags ; 
+    Format.printf "fair= %a, tags=%a " Format.pp_print_bool (Option.is_some fair) Tags.pp tags ; 
     if subg=[] then Format.pp_print_string fmt "leaf" else
     Blist.pp pp_semicolonsp 
       (fun fmt (i,tv,tp) ->
@@ -155,11 +155,11 @@ let check_proof p =
       | x::[] -> debug (fun () -> "Odd numbered list in fair constraint") ; [],[] (* TODO : handle this case appropriately *)
       | [] -> [],[]
     in
-    let create_pair (i,_,_) (j,_,_) = debug (fun () -> "Creating fairness constraint " ^ string_of_int i ^ " " ^ string_of_int j) ; set_fairness_constraint i j in
-    if fair then
+    let create_pair (i,_,_) (j,_,_) (c1,c2) = debug (fun () -> "Creating fairness constraint " ^ string_of_int i ^ " " ^ string_of_int j) ; set_fairness_constraint i j c1 c2 in
+    if Option.is_some fair then
       begin
 	let l1,l2 = separate l in
-	Blist.iter2 create_pair l1 l2
+	Blist.iter2 (fun li1 li2 -> create_pair li1 li2 (Option.get fair)) l1 l2
       end in
   let size = Int.Map.cardinal p in
   let log2size = 1 + int_of_float (ceil ((log (float_of_int size)) /. (log 2.0))) in
diff --git a/src/generic/proof.ml b/src/generic/proof.ml
index c28e3df6..b75cc4c7 100644
--- a/src/generic/proof.ml
+++ b/src/generic/proof.ml
@@ -85,13 +85,13 @@ module Make(Seq : Sigs.SEQUENT) =
       assert (Seq.equal_upto_tags seq (get_seq target prf));
       replace idx n prf
   
-     let add_inf ?(fair=false) idx descr subgoals prf =
+     let add_inf ?(fair_pair_fun=(fun _ -> None)) idx descr subgoals prf =
       let subidxs = Blist.range (fresh_idx prf) subgoals in
       let subnodes = 
         Blist.map2 (fun i (seq,_,_) -> (i, Node.mk_open seq)) subidxs subgoals in
       let subidxs_plus_tags = 
         Blist.map2 (fun i (_,vtts,ptts) -> (i,vtts,ptts)) subidxs subgoals in
-      let n = Node.mk_inf ~fair:fair (get_seq idx prf) descr subidxs_plus_tags in
+      let n = Node.mk_inf ~fair_pair_fun:fair_pair_fun (get_seq idx prf) descr subidxs_plus_tags in
       ensure_add idx n prf;
       let prf' = 
         Blist.foldl 
diff --git a/src/generic/proofnode.ml b/src/generic/proofnode.ml
index 01bf5422..f207962b 100644
--- a/src/generic/proofnode.ml
+++ b/src/generic/proofnode.ml
@@ -14,7 +14,7 @@ struct
   type proof_subnode =
     | OpenNode
     | AxiomNode
-    | InfNode of bool * (int * TagPairs.t * TagPairs.t) list
+    | InfNode of (int*int) option * (int * TagPairs.t * TagPairs.t) list
     | BackNode of int * TagPairs.t
   
   type t =
@@ -65,8 +65,10 @@ struct
     mk seq OpenNode "(Open)"
   let mk_axiom seq descr = 
     mk seq AxiomNode descr
-  let mk_inf ?(fair=false) seq descr subgoals = 
-    mk seq (InfNode(fair,subgoals)) descr
+  let mk_inf ?(fair_pair_fun=(fun _ -> None)) seq descr subgoals =
+    let fair_constraints = (fair_pair_fun seq) in
+    debug (fun () -> "Making inf node with fair constraints " ^ string_of_bool (Option.is_some fair_constraints));
+    mk seq (InfNode(fair_constraints,subgoals)) descr
   let mk_backlink seq descr child vtts = 
     mk seq (BackNode(child, vtts)) descr
   
@@ -80,11 +82,11 @@ struct
 
   let to_fair_abstract_node n = match n.node with
     | OpenNode | AxiomNode ->
-       Fair_soundcheck.mk_fair_abs_node false (Seq.tags n.seq) []
+       Fair_soundcheck.mk_fair_abs_node None (Seq.tags n.seq) []
     | InfNode(fair,subg) ->
        Fair_soundcheck.mk_fair_abs_node fair (Seq.tags n.seq) subg
     | BackNode(child, tv) ->
-       Fair_soundcheck.mk_fair_abs_node false (Seq.tags n.seq) [(child, tv, TagPairs.empty)]	
+       Fair_soundcheck.mk_fair_abs_node None (Seq.tags n.seq) [(child, tv, TagPairs.empty)]	
 			      
   let pp fmt n = match n.node with
     | OpenNode ->
@@ -95,14 +97,14 @@ struct
         Format.fprintf fmt "@[%a (%s) [%i] <pre=%a>@]" 
           Seq.pp n.seq n.descr i
           TagPairs.pp tps
-    | InfNode(f,p) -> (* TODO: print fair nodes? *) 
-       Format.fprintf fmt "@[%a (%s) [%a] - %s@]" 
+    | InfNode(f,p) ->
+       Format.fprintf fmt "@[%a (%s) [%a] %s@]" 
 		      Seq.pp n.seq
 		      n.descr
 		      (Blist.pp pp_commasp 
 				(fun fmt (i,pres,prog) -> 
 				 Format.fprintf fmt "%i" i)) p
-		      (string_of_bool f)
+		      (if Option.is_some f then "- fair (" ^ string_of_int (fst (Option.get f)) ^ "," ^ string_of_int(snd (Option.get f)) ^ ")" else "")
   (* Format.fprintf fmt "@[%i <%a/%a>@]" i TagPairs.pp pres TagPairs.pp prog)) p *)
   
   let justify = Latex.text "\n\\justifies\n\\thickness=0.1em\n"
diff --git a/src/generic/proofrule.ml b/src/generic/proofrule.ml
index d9b15870..3da6d10e 100644
--- a/src/generic/proofrule.ml
+++ b/src/generic/proofrule.ml
@@ -31,11 +31,11 @@ struct
     | None -> L.empty
     | Some descr -> L.singleton ([], Proof.add_axiom idx descr prf)  
   
-  let mk_infrule ?(fair=false) r_f idx prf =
+  let mk_infrule ?(fair_pair_fun=(fun _ -> None)) r_f idx prf =
     let seq = Proof.get_seq idx prf in
     let mk (l,d) = 
       debug (fun () -> "Found " ^ d ^ " app.") ;
-      Proof.add_inf ~fair:fair idx d l prf in
+      Proof.add_inf ~fair_pair_fun:fair_pair_fun idx d l prf in
     L.map mk (L.of_list (r_f seq))
 
   let mk_backrule ?(fair=false) greedy sel_f br_f srcidx prf =
diff --git a/src/generic/sigs.mli b/src/generic/sigs.mli
index fcaa145f..bd93579c 100644
--- a/src/generic/sigs.mli
+++ b/src/generic/sigs.mli
@@ -50,7 +50,7 @@ sig
       sequent [seq], description [descr], target index [target] and set of 
       valid tag transitions (as pairs) [vtts].*) 
   
-  val mk_inf : ?fair:bool -> seq_t -> string -> (int * Util.TagPairs.t * Util.TagPairs.t) list -> t
+  val mk_inf : ?fair_pair_fun:(seq_t -> (int*int) option) -> seq_t -> string -> (int * Util.TagPairs.t * Util.TagPairs.t) list -> t
   (** [mk_inf fair seq descr subgoals back] creates an inference node labelled by 
       sequent [seq], description [descr], a list of triples consisting of
       subgoal index, valid tag transitions and progressing tag transitions 
@@ -129,7 +129,7 @@ sig
   val add_axiom : int -> string -> t -> t
   val add_backlink : int -> string -> int -> Util.TagPairs.t -> t -> t
   val add_inf : 
-    ?fair:bool -> int -> string -> 
+    ?fair_pair_fun:(seq_t -> (int*int) option) -> int -> string -> 
     (seq_t * Util.TagPairs.t * Util.TagPairs.t) list -> t -> 
     (int list * t)
 
@@ -209,7 +209,7 @@ sig
   (** Rules are functions that break down a sequent to a choice of applications
       where each application is a list of premises, including tag information,
       and a description. *)
-  val mk_infrule : ?fair:bool -> infrule_f -> t
+  val mk_infrule : ?fair_pair_fun:(seq_t -> (int*int) option) -> infrule_f -> t
 	
   (** Backlink rules take:
       - a boolean [eager] 
diff --git a/src/soundness/fair_proof.c b/src/soundness/fair_proof.c
index 6886b35c..1d1f3216 100644
--- a/src/soundness/fair_proof.c
+++ b/src/soundness/fair_proof.c
@@ -20,12 +20,14 @@ Vertex FairProof::create_vertex() {
   return v;
 }
 //------------------------------------------------------------------
-void FairProof::set_fairness_constraint(const Vertex & v1, const Vertex & v2) {
+void FairProof::set_fairness_constraint(const Vertex & v1, const Vertex & v2, int c1, int c2) {
   assert( vertices.find(v1) != vertices.end() );
   assert( vertices.find(v2) != vertices.end() );
-  AcceptanceElem first_acc_elem = max_acc_elem++;
-  AcceptanceElem second_acc_elem = max_acc_elem++;
-  acc_set_map[v1].insert(first_acc_elem);
-  acc_set_map[v2].insert(second_acc_elem);
-  fairness_constraints.insert(FairnessConstraint(first_acc_elem, second_acc_elem));
+  /* AcceptanceElem first_acc_elem = max_acc_elem++; */
+  /* AcceptanceElem second_acc_elem = max_acc_elem++; */
+  max_acc_elem++;
+  max_acc_elem++; // TODO : we do not this anymore, we may use size of acc_set_map
+  acc_set_map[v1].insert(c1);
+  acc_set_map[v2].insert(c2);
+  fairness_constraints.insert(FairnessConstraint(c1, c2));
 }
diff --git a/src/soundness/fair_proof.hpp b/src/soundness/fair_proof.hpp
index d955eeda..3950db21 100644
--- a/src/soundness/fair_proof.hpp
+++ b/src/soundness/fair_proof.hpp
@@ -43,7 +43,7 @@ class FairProof : public Proof {
   Vertex create_vertex();
   const AcceptanceSet get_acc_set_of_vertex(const Vertex & v) const;
   AcceptanceElem get_max_acc_elem() const { return max_acc_elem; }
-  void set_fairness_constraint(const Vertex & v1, const Vertex & v2);
+  void set_fairness_constraint(const Vertex & v1, const Vertex & v2, const int c1, const int c2);
   virtual std::unordered_set<FairnessConstraint> get_fairness_constraints() const {return fairness_constraints; }
 };
 //==================================================================
diff --git a/src/soundness/fair_proof_aut.c b/src/soundness/fair_proof_aut.c
index bc6ecdda..8d0934f2 100644
--- a/src/soundness/fair_proof_aut.c
+++ b/src/soundness/fair_proof_aut.c
@@ -68,9 +68,11 @@ void FairProofAutomaton::set_acceptance_condition() {
     if(elem != fairness_constraints.begin()) acceptance_condition << " & ";
     acceptance_condition << "(Fin(" << (std::get< 0 >(*elem))
 			 << ") | Inf(" << (std::get< 1 >(*elem))
+			 << ")) & (Fin(" << (std::get< 1 >(*elem))
+			 << ") | Inf(" << (std::get< 0 >(*elem))
 			 << "))" << std::flush;
   }
-  std::cout << "Setting acceptance condition: \"" << acceptance_condition.str() << "\"\n" ;
+  /* std::cout << "Setting acceptance condition: \"" << acceptance_condition.str() << "\"\n" ; */
   if (acceptance_condition.str().empty()) {
     set_buchi();
   } else {
diff --git a/src/soundness/fair_soundness.c b/src/soundness/fair_soundness.c
index 2e78599b..190b2894 100644
--- a/src/soundness/fair_soundness.c
+++ b/src/soundness/fair_soundness.c
@@ -160,14 +160,16 @@ extern "C" void set_fair_progress_pair(value v1_, value v2_, value t1_, value t2
   CAMLreturn0;
 }
 
-extern "C" void set_fairness_constraint(value v1_, value v2_) {
-  CAMLparam2(v1_,v2_);
+extern "C" void set_fairness_constraint(value v1_, value v2_, value c1_, value c2_) {
+  CAMLparam4(v1_,v2_,c1_,c2_);
   int v1 = Int_val(v1_);
   int v2 = Int_val(v2_);
+  int c1 = Int_val(c1_);
+  int c2 = Int_val(c2_);
   assert(proof);
   assert( bdd_map.find(v1) != bdd_map.end() );
   assert( bdd_map.find(v2) != bdd_map.end() );
-  proof->set_fairness_constraint(bdd_map[v1], bdd_map[v2]);
+  proof->set_fairness_constraint(bdd_map[v1], bdd_map[v2], c1, c2);
   CAMLreturn0;
 }
 
@@ -176,11 +178,11 @@ extern "C" value check_fair_soundness() {
   CAMLlocal1(v_res);
   proof->set_acceptance_condition();
   spot::twa_graph_ptr proof_graph = copy(proof, spot::twa::prop_set::all());
-  custom_print(std::cout,proof_graph);
+  /* custom_print(std::cout,proof_graph); */
   spot::const_twa_ptr ta = std::make_shared<TraceAutomaton>(*proof);
   spot::twa_graph_ptr proof_cpy = copy(proof, spot::twa::prop_set::all());
   spot::twa_graph_ptr graph = copy(ta, spot::twa::prop_set::all());
-  custom_print(std::cout,graph);
+  /* custom_print(std::cout,graph); */
   spot::twa_graph_ptr det = to_generalized_buchi(dtwa_complement(tgba_determinize(graph, false, true, true, spot::check_stutter_invariance(graph).is_true())));
   spot::twa_graph_ptr proof_tgba = to_generalized_buchi(proof_cpy);
   spot::const_twa_ptr product = std::make_shared<spot::twa_product>(proof_tgba, det);
diff --git a/src/temporal_ctl/temporal_ctl_prove.ml b/src/temporal_ctl/temporal_ctl_prove.ml
index ac030511..3d1d9630 100644
--- a/src/temporal_ctl/temporal_ctl_prove.ml
+++ b/src/temporal_ctl/temporal_ctl_prove.ml
@@ -14,6 +14,8 @@ let () = F.speclist := !F.speclist @ [
       ": read inductive definitions from <file>, default is " ^ !defs_path);
     ("-P", Arg.Set_string prog_path, ": prove temporal property of program <file>");
     ("-F", Arg.Set Temporal_rules.use_fairness, ": restrict to fair execution paths");
+    ("-c", Arg.Set Temporal_rules.subcheck, ": check for subformulas");
+    ("-NC", Arg.Clear Temporal_rules.use_cut, ": check for subformulas");
     ("-IT", Arg.Set Sl_rules.use_invalidity_heuristic, 
      ": run invalidity heuristic during check, default is " ^ 
        (string_of_bool !Sl_rules.use_invalidity_heuristic));
diff --git a/src/temporal_ctl/temporal_program.ml b/src/temporal_ctl/temporal_program.ml
index 980d42f5..a01df5bb 100644
--- a/src/temporal_ctl/temporal_program.ml
+++ b/src/temporal_ctl/temporal_program.ml
@@ -448,7 +448,7 @@ module Seq =
     let tagset_one = Tags.singleton 1
     let tagpairs_one = TagPairs.mk tagset_one
     let tags (sf,cmd,tf) = Tags.union (Sl_form.tags sf) (Tl_form.tags tf)
-    let tag_pairs (sf,_,tf) = if !termination then TagPairs.union (Sl_form.tag_pairs sf) (TagPairs.mk (Tl_form.outermost_tag tf)) else (TagPairs.mk (Tl_form.outermost_tag tf))
+    let tag_pairs (sf,_,tf) = TagPairs.union (Sl_form.tag_pairs sf) (TagPairs.mk (Tl_form.outermost_tag tf))
     let sep_vars (sf,_,_) = Sl_form.vars sf
     let temp_vars (_,_,tf) = Tl_form.vars tf
     let vars (sf,_,tf) = Sl_term.Set.union (Sl_form.vars sf) (Tl_form.vars tf)
@@ -477,9 +477,7 @@ module Seq =
 								      
 										      
     let subsumed (sf,cmd,tf) (sf',cmd',tf') = 
-      Cmd.equal cmd cmd' &&
-	(if !termination then Sl_form.subsumed else Sl_form.subsumed_upto_tags) 
-          ~total:false  sf' sf
+      Cmd.equal cmd cmd' && Sl_form.subsumed ~total:false  sf' sf
     let subsumed_upto_tags (sf,cmd,tf) (sf',cmd',tf') = 
       Cmd.equal cmd cmd' &&
 	Sl_form.subsumed_upto_tags ~total:false sf' sf
diff --git a/src/temporal_ctl/temporal_rules.ml b/src/temporal_ctl/temporal_rules.ml
index 5e914556..807fcbc1 100644
--- a/src/temporal_ctl/temporal_rules.ml
+++ b/src/temporal_ctl/temporal_rules.ml
@@ -12,35 +12,40 @@ module Proof = Proof.Make(Temporal_program.Seq)
 let use_cut = ref true
 
 let use_fairness = ref false
-		  
+
+let subcheck = ref false
+		       
 let tagpairs s =
   Seq.tag_pairs s
 		
 (* following is for symex only *)
-let progpairs s = 
+let progpairs s =
   Seq.tag_pairs s
+(* let progpairs (sf,cmd,tf) = *)
+(*   (TagPairs.mk (Tl_form.outermost_tag tf)) *)
 
 let dest_sh_seq (sf,cmd,tf) = (Sl_form.dest sf, cmd, tf)
-				
+	
 (* axioms *)
 let subformula_axiom =
   Rule.mk_axiom 
-    (fun (sf,_,tf) ->
+    (fun (sf,c,tf) ->
      match Tl_form.is_atom tf with
      | true -> let tf_heap = Tl_form.dest_atom tf in
 	       let (_,_,ptos,inds) = Sl_heap.dest tf_heap in
-	       (Option.mk (Sl_ptos.is_empty ptos &&
-			     Sl_tpreds.is_empty inds &&
-			       not (Sl_heap.is_empty tf_heap) &&
-				 Sl_form.subsumed ~total:false [tf_heap] sf) "Sub-Check")
+	       let () = debug (fun () -> "Attempt subformula" ^ (Seq.to_string (sf,c,tf))) in
+	       (Option.mk ((Sl_ptos.is_empty ptos &&
+			      Sl_tpreds.is_empty inds &&
+				not (Sl_heap.is_empty tf_heap) || !subcheck) &&
+			     Sl_form.subsumed_upto_tags ~total:false [tf_heap] sf) "Sub-Check")
      | false -> None)
-
+    
 let ex_falso_axiom = 
   Rule.mk_axiom (fun (sf,_,_) -> Option.mk (Sl_form.inconsistent sf) "Ex Falso")
 
 let symex_check_axiom entails = 
   Rule.mk_axiom (fun (sf,_,tf) -> Option.mk (Tl_form.is_checkable tf && Option.is_some (entails sf (Tl_form.extract_checkable_slformula tf))) "Check")
-		
+
 let symex_empty_axiom =
   Rule.mk_axiom (fun (_,cmd,tf) -> Option.mk (Cmd.is_empty cmd && Tl_form.is_box tf) "Empty")
 
@@ -61,8 +66,8 @@ let simplify_seq_rl =
 
 let simplify = Rule.mk_infrule simplify_seq_rl  
     
-let wrap ?(fair=false) r =
-  Rule.mk_infrule ~fair:fair
+let wrap ?(fair_pair_fun=(fun _ -> None))  r =
+  Rule.mk_infrule ~fair_pair_fun:fair_pair_fun
     (Seqtactics.compose r (Seqtactics.attempt simplify_seq_rl))
 
 
@@ -82,25 +87,20 @@ let luf_rl seq defs =
     let (sf,cmd,tf) = dest_sh_seq seq in
     (* let (c,_,_) = if Cmd.is_ifelse cmd then Cmd.dest_ifelse cmd else let (c,cont) = Cmd.dest_while cmd in (c,cont,cont) in *)
     (* let cond_vars = Cond.vars c in *)
-    let t = if Cmd.is_load cmd then let (t,_,_) = Cmd.dest_load cmd in t else let (t,_,_) = Cmd.dest_store cmd in t in
-    let () = debug (fun _ -> "Term in cmd for luf: " ^ (Sl_term.to_string t)) in 
+    let t = if Cmd.is_load cmd then let (_,t,_) = Cmd.dest_load cmd in t else let (t,_,_) = Cmd.dest_store cmd in t in
+    let () = debug (fun _ -> "Term in cmd for luf: " ^ (Sl_term.to_string t)) in
     if (Blist.exists Option.is_some (Blist.map (fun var -> SH.find_lval var sf) [t])) then
-      let () = debug (fun _ -> "Already exists ") in 
+      let () = debug (fun _ -> "Already exists ") in
       []
     else
-      let () = debug (fun _ -> "Does NOT exists ") in 
-      let seq_vars = Seq.vars seq in
+      let () = debug (fun _ -> "Does NOT exists ") in
+    let seq_vars = Seq.vars seq in
     let left_unfold ((_, (ident, _)) as p) = 
       let l' = SH.del_ind sf p in
       let clauses = Sl_defs.unfold seq_vars l' p defs in
       let do_case (f', tagpairs) =
         let l' = Sl_heap.star l' f' in
-        ( 
-	  ([l'],cmd,tf), 
-	  (if !termination then tagpairs else Seq.tagpairs_one),
-	  (* Seq.tag_pairs ([l'],cmd,tf), *)
-	  (if !termination then tagpairs else TagPairs.empty)
-	) in
+        (([l'],cmd,tf), tagpairs, tagpairs) in
       Blist.map do_case clauses, ((Sl_predsym.to_string ident) ^ " L.Unf.") in
     Sl_tpreds.map_to_list 
       left_unfold (Sl_tpreds.filter (Sl_defs.is_defined defs) sf.SH.inds)
@@ -111,12 +111,8 @@ let luf defs = wrap (fun seq -> luf_rl seq defs)
 (* FOR SYMEX ONLY *)
 let fix_ts l = 
   Blist.map
-    (fun (g,d) ->
-     Blist.map
-       (fun s -> (s, tagpairs s, TagPairs.empty ))
-       g, d)
-    l 
-    
+    (fun (g,d) ->Blist.map (fun s -> (s, tagpairs s, TagPairs.empty )) g, d) l 
+
 let fix_tps l = 
   Blist.map 
     (fun (g,d) -> Blist.map (fun s -> (s, tagpairs s, progpairs s )) g, d) l 
@@ -127,12 +123,12 @@ let mk_symex f =
       if Tl_form.is_diamond tf then
 	let cont = Cmd.get_cont cmd in
 	let tf' = Tl_form.e_step tf in
-	fix_tps 
+	fix_ts 
 	  (Blist.map (fun (g,d) -> Blist.map (fun h' -> ([h'], cont, tf')) g, d) (f seq))
       else if Tl_form.is_box tf then
 	let cont = Cmd.get_cont cmd in
 	let tf' = Tl_form.a_step tf in
-	fix_tps 
+	fix_ts 
 	  (Blist.map (fun (g,d) -> Blist.map (fun h' -> ([h'], cont, tf')) g, d) (f seq))
       else
 	[]
@@ -214,25 +210,35 @@ let symex_skip_rule =
   mk_symex rl
 
 let symex_ifelse_fair_rule =
+  let fair_constraints seq =
+    try
+      let (sf,cmd,tf) = dest_sh_seq seq in
+      let (c,cmd1,cmd2) = Cmd.dest_ifelse cmd in
+      (* Get program labels for fairness constraint *)
+      let cmd_lbl_1 = Option.get (Cmd.get_lbl cmd1) in
+      let cmd_lbl_2 = Option.get (Cmd.get_lbl cmd2) in
+      debug (fun () -> "In constraint function. Shoud be some");
+      Some (cmd_lbl_1,cmd_lbl_2)
+    with WrongCmd -> debug (fun () -> "In constraint function. Failed. None"); None in 
   let rl seq =
     try
       let (sf,cmd,tf) = dest_sh_seq seq in
       let (c,cmd1,cmd2) = Cmd.dest_ifelse cmd in
       let cont = Cmd.get_cont cmd in
       let (sf',sf'') = Cond.fork sf c in 
-      if (Tl_form.is_box tf  && not (Cond.is_non_det c)) && !use_fairness then
+      if Tl_form.is_box tf  && (Cond.is_non_det c) && !use_fairness then
 	let tf' = Tl_form.a_step tf in
-	fix_tps 
+	fix_ts 
           [[ ([sf'], Cmd.mk_seq cmd1 cont, tf') ; ([sf''], Cmd.mk_seq cmd2 cont,tf') ], "If-F-[]"]
       else if (Cond.is_non_det c) && Tl_form.is_diamond tf && !use_fairness then
 	let tf' = Tl_form.e_step tf in
-	fix_tps 
+	fix_ts 
           [[ ([sf'], Cmd.mk_seq cmd1 cont, tf')], "If-<>1" ;
 	   [ ([sf''], Cmd.mk_seq cmd2 cont, tf')], "If-<>2"]
       else 
 	[]
     with Not_symheap | WrongCmd -> [] in
-  wrap ~fair:true rl
+  wrap ~fair_pair_fun:fair_constraints rl
        
 let symex_ifelse_rule =
   let rl seq =
@@ -243,14 +249,14 @@ let symex_ifelse_rule =
       let (sf',sf'') = Cond.fork sf c in
       if (Tl_form.is_box tf  && not (Cond.is_non_det c)) || (Tl_form.is_box tf && (not !use_fairness)) then
 	let tf' = Tl_form.a_step tf in
-	fix_tps 
+	fix_ts 
           [[ ([sf'], Cmd.mk_seq cmd1 cont, tf') ; ([sf''], Cmd.mk_seq cmd2 cont,tf') ], "If-[]"]
       else if Tl_form.is_box tf && !use_fairness then
 	[]
       else if Tl_form.is_diamond tf then
 	let tf' = Tl_form.e_step tf in
 	if (Cond.is_non_det c) && (not !use_fairness) then
-	  fix_tps 
+	  fix_ts 
             [[ ([sf'], Cmd.mk_seq cmd1 cont, tf')], 
              "If-<>1" ;
 	     [ ([sf''], Cmd.mk_seq cmd2 cont, tf')],
@@ -259,15 +265,26 @@ let symex_ifelse_rule =
 	else if (Cond.is_non_det c) && (!use_fairness) then
 	  []
 	else if Cond.validated_by sf c then
-	  fix_tps [[ ([sf'], Cmd.mk_seq cmd1 cont, tf')], "If-<>1"]
+	  fix_ts [[ ([sf'], Cmd.mk_seq cmd1 cont, tf')], "If-<>1"]
 	else
-	  fix_tps [[ ([sf''], Cmd.mk_seq cmd2 cont, tf')], "If-<>2"]
+	  fix_ts [[ ([sf''], Cmd.mk_seq cmd2 cont, tf')], "If-<>2"]
       else
 	[]
     with Not_symheap | WrongCmd -> [] in
-  wrap ~fair:false rl
+  wrap  rl
        
 let symex_while_fair_rule =
+  let fair_constraints seq =
+    try
+      let (sf,cmd,tf) = dest_sh_seq seq in
+      let (c,cmd') = Cmd.dest_while cmd in
+      let cont = Cmd.get_cont cmd in
+      (* Get program labels for fairness constraint *)
+      let cmd_lbl_1 = Option.get (Cmd.get_lbl cmd') in
+      let cmd_lbl_2 = Option.get (Cmd.get_lbl cont) in
+      debug (fun () -> "In constraint function. Shoud be some");
+      Some (cmd_lbl_1,cmd_lbl_2)
+    with WrongCmd -> debug (fun () -> "In constraint function. Failed. None"); None in 
   let rl seq =
     try
       let (sf,cmd,tf) = dest_sh_seq seq in
@@ -276,17 +293,17 @@ let symex_while_fair_rule =
       let (sf',sf'') = Cond.fork sf c in 
       if (Cond.is_non_det c) && Tl_form.is_box tf && !use_fairness then
 	let tf' = Tl_form.a_step tf in
-	fix_tps 
-	  [[ ([sf'], Cmd.mk_seq cmd' cmd, tf') ; ([sf''], cont, tf') ], "While-Fair-[]"]
+	fix_ts 
+	  [[ ([sf'], Cmd.mk_seq cmd' cmd, tf') ; ([sf''], cont, tf') ], "Wh-F-[]"]
       else if (Cond.is_non_det c) && Tl_form.is_diamond tf && !use_fairness then
 	let tf' = Tl_form.e_step tf in
-	fix_tps 
-          [[ ([sf'], Cmd.mk_seq cmd' cmd, tf')], "While-<>1" ;
-	   [ ([sf''], cont, tf')], "While-<>2"]
+	fix_ts 
+          [[ ([sf'], Cmd.mk_seq cmd' cmd, tf')], "Wh-<>1" ;
+	   [ ([sf''], cont, tf')], "Wh-<>2"]
       else
 	[]
     with Not_symheap | WrongCmd -> [] in
-  wrap ~fair:true rl
+  wrap ~fair_pair_fun:fair_constraints rl
        
 let symex_while_rule =
   let rl seq =
@@ -297,29 +314,29 @@ let symex_while_rule =
       let (sf',sf'') = Cond.fork sf c in 
       if (Tl_form.is_box tf && (not (Cond.is_non_det c))) || (Tl_form.is_box tf && (not !use_fairness)) then
 	let tf' = Tl_form.a_step tf in
-	fix_tps 
-	  [[ ([sf'], Cmd.mk_seq cmd' cmd, tf') ; ([sf''], cont, tf') ], "While-[]"]
+	fix_ts 
+	  [[ ([sf'], Cmd.mk_seq cmd' cmd, tf') ; ([sf''], cont, tf') ], "Wh-[]"]
       else if Tl_form.is_box tf && !use_fairness then
 	[]
       else if Tl_form.is_diamond tf then
 	let tf' = Tl_form.e_step tf in
 	if (Cond.is_non_det c) && (not !use_fairness) then
-	  fix_tps 
+	  fix_ts 
             [[ ([sf'], Cmd.mk_seq cmd' cmd, tf')], 
-             "While-<>1" ;
+             "Wh-<>1" ;
 	     [ ([sf''], cont, tf')],
-             "While-<>2"
+             "Wh-<>2"
             ]
 	else if (Cond.is_non_det c) && (!use_fairness) then
 	  []
 	else if Cond.validated_by sf c then
-	  fix_tps [[ ([sf'], Cmd.mk_seq cmd' cmd, tf')], "While-<>1"]
+	  fix_ts [[ ([sf'], Cmd.mk_seq cmd' cmd, tf')], "Wh-<>1"]
 	else
-	  fix_tps [[ ([sf''], cont, tf')], "While-<>2"]
+	  fix_ts [[ ([sf''], cont, tf')], "Wh-<>2"]
       else
 	[]
     with Not_symheap | WrongCmd -> [] in
-  wrap ~fair:false rl
+  wrap rl
 
 module Slprover = Prover.Make(Sl_seq)
 
@@ -366,7 +383,7 @@ let matches ((sf,cmd,tf) as seq) ((sf',cmd',tf') as seq') =
           ) in
       let res = 
 	Sl_term.backtrack 
-	  (Sl_heap.unify_partial ~tagpairs:true)
+	  (Sl_heap.classical_unify ~inverse:false ~tagpairs:true)
 	  ~sub_check
 	  ~cont 
 	  sf' sf in
@@ -390,7 +407,6 @@ let matches ((sf,cmd,tf) as seq) ((sf',cmd',tf') as seq') =
       		 else
       		   res in
       if Tl_form.is_ag tf && Tl_form.is_ag tf' then
-	(* let () = print_endline "After computer res with AG" in   *)
 	let (t1, _) = Tl_form.dest_ag tf in
 	let (t2, _) = Tl_form.dest_ag tf' in
 	assert (Tags.equal (Tags.singleton t1) (Tags.singleton t2));
@@ -428,7 +444,7 @@ let cut seq' seq =
     [ [(seq',
         TagPairs.union (TagPairs.mk (Tl_form.outermost_tag tf1)) (TagPairs.mk (Tags.inter (Seq.tags seq) (Seq.tags seq')))
 	(* TagPairs.mk (Tags.inter (Seq.tags seq) (Seq.tags seq')) *) (*Seq.tag_pairs seq*),
-       TagPairs.empty (* TagPairs.mk (Tags.inter (Seq.tags seq) (Seq.tags seq')) *) (*Seq.tag_pairs seq*))], "Cut" ]
+       TagPairs.empty (* TagPairs.mk (Tags.inter (Seq.tags seq) (Seq.tags seq')) *) (*Seq.tag_pairs seq*))], "Cons" ]
   else
     []
 
@@ -439,7 +455,7 @@ let unfold_ag_rule =
       if Tl_form.is_ag tf then
 	let (tf1,tf2) = Tl_form.unfold_ag tf in
 	fix_tps
-	  [[([sf],cmd,tf1); ([sf],cmd,tf2)], "UnfoldAG"]
+	  [[([sf],cmd,tf1); ([sf],cmd,tf2)], "AG"]
       else
 	[]
     with Not_symheap -> [] in
@@ -451,8 +467,8 @@ let unfold_eg_rule =
       let (sf,cmd,tf) = dest_sh_seq seq in
       if Tl_form.is_eg tf then
 	let (tf1,tf2) = Tl_form.unfold_eg tf in
-	fix_ts
-	  [[([sf],cmd,tf1) ; ([sf],cmd,tf2)], "UnfoldEG"]
+	fix_tps
+	  [[([sf],cmd,tf1) ; ([sf],cmd,tf2)], "EG"]
       else 
 	[]
     with Not_symheap -> [] in
@@ -464,9 +480,9 @@ let unfold_af_rule =
       let (sf,cmd,tf) = dest_sh_seq seq in
       if Tl_form.is_af tf then
 	let (tf1,tf2) = Tl_form.unfold_af tf in
-	fix_tps
-	  [[([sf],cmd,tf1)], "UnfoldAF" ;
-	   [([sf],cmd,tf2)], "UnfoldAF"]
+	fix_ts
+	  [[([sf],cmd,tf1)], "AF" ;
+	   [([sf],cmd,tf2)], "AF"]
       else
 	[]
     with Not_symheap -> [] in
@@ -478,9 +494,9 @@ let unfold_ef_rule =
       let (sf,cmd,tf) = dest_sh_seq seq in
       if Tl_form.is_ef tf then
 	let (tf1,tf2) = Tl_form.unfold_ef tf in
-	fix_tps
-	  [[([sf],cmd,tf1)], "UnfoldEF" ;
-	   [([sf],cmd,tf2)], "UnfoldEF"]
+	fix_ts
+	  [[([sf],cmd,tf1)], "EF" ;
+	   [([sf],cmd,tf2)], "EF"]
       else
 	[]
     with Not_symheap -> [] in
@@ -492,7 +508,7 @@ let disjunction_rule =
       let (sf,cmd,tf) = dest_sh_seq seq in
       if Tl_form.is_or tf then
 	let (tf1,tf2) = Tl_form.unfold_or tf in
-	fix_tps
+	fix_ts
 	  [[([sf],cmd,tf1)], "Disj1" ;
 	   [([sf],cmd,tf2)], "Disj2"]
       else 
@@ -506,7 +522,7 @@ let conjunction_rule =
       let (sf,cmd,tf) = dest_sh_seq seq in
       if Tl_form.is_and tf then
 	let (tf1,tf2) = Tl_form.unfold_and tf in
-	fix_tps
+	fix_ts
 	  [[([sf],cmd,tf1);([sf],cmd,tf2)], "Conj"]
       else 
 	[]
@@ -535,24 +551,25 @@ let dobackl idx prf =
       let subst_seq = Seq.subst theta targ_seq' in
       Rule.sequence [
           if Seq.equal src_seq subst_seq
-        then Rule.identity
-        else 
-	  if Seq.subsumed src_seq targ_seq then
-	    Rule.mk_infrule (frame subst_seq)
-	  else
-	    Rule.mk_infrule (cut subst_seq);
-	
-	if Sl_term.Map.for_all Sl_term.equal theta
-	then Rule.identity
-	else Rule.mk_infrule (subst_rule theta targ_seq');
-        
-        Rule.mk_backrule
-	  ~fair:!use_fairness
-          false 
-          (fun _ _ -> [targ_idx]) 
-          (fun (_,_,tf) s' -> 
-           [(if !termination then TagPairs.reflect tagpairs else TagPairs.mk (Tl_form.outermost_tag tf)
-	    (*TagPairs.empty *) (* Seq.tagpairs_one *)), "Backl"])
+          then Rule.identity
+          else 
+	    (* if Seq.subsumed src_seq targ_seq then *)
+	    (*   Rule.mk_infrule (frame subst_seq) *)
+	    (* else *)
+	      Rule.mk_infrule (cut subst_seq);
+	  
+	  if Sl_term.Map.for_all Sl_term.equal theta
+	  then Rule.identity
+	  else Rule.mk_infrule (subst_rule theta targ_seq');
+          
+          Rule.mk_backrule
+	    ~fair:!use_fairness
+            false 
+            (fun _ _ -> [targ_idx]) 
+            (fun (_,_,tf) s' -> 
+             [(*TagPairs.empty*)
+	     (TagPairs.reflect tagpairs)
+	    (*TagPairs.empty *) (* Seq.tagpairs_one *), "Backl"])
 	] in
   (* let () = print_endline "Attempting backlink with source seq:" in   *)
   (* let () = print_endline (Seq.to_string src_seq) in   *)
@@ -619,126 +636,6 @@ let generalise_while_rule =
     with Not_symheap | WrongCmd -> [] in
   Rule.mk_infrule rl 
 
-(* let matches_cut ((sf,cmd,tf) as seq) ((sf',cmd',tf') as seq') = *)
-(*   try *)
-(*     (\* let () = print_endline "At matches with seqs:" in   *\) *)
-(*     (\* let () = print_endline (Seq.to_string seq) in   *\) *)
-(*     (\* let () = print_endline (Seq.to_string seq') in   *\) *)
-(*     if not (Cmd.equal cmd cmd' && Tl_form.equal tf tf' *)
-(* 	    && (Tl_form.is_ag tf || Tl_form.is_eg tf) *)
-(* 	    && (Tl_form.is_ag tf' || Tl_form.is_eg tf')) then  *)
-(*       (\* let () = print_endline "Seqs are not equal" in   *\) *)
-(*       []  *)
-(*     else if Option.is_some (Slprover.idfs 1 11 !Sl_rules.axioms !Sl_rules.rules (sf, sf')) then *)
-(*          [TagPairs.mk (Tl_form.outermost_tag tf)] *)
-(*        else *)
-(* 	 [] *)
-(*   with Not_symheap -> [] *)
-
-			
-(* let new_backl_cut idx prf =  *)
-(*   let src_seq = Proof.get_seq idx prf in *)
-(*   let targets = Rule.all_nodes idx prf in *)
-(*   let apps =  *)
-(*     Blist.bind *)
-(*       (fun idx' ->  *)
-(*        Blist.map  *)
-(*          (fun res -> (idx',res)) *)
-(*          (matches_cut src_seq (Proof.get_seq idx' prf)) *)
-(*       )  *)
-(*       targets in *)
-(*   let f (targ_idx,tagpairs) = *)
-(*       let targ_seq = Proof.get_seq targ_idx prf in *)
-(*       (\* [targ_seq'] is as [targ_seq] but with the tags of [src_seq] *\) *)
-(*       let (sf_targ_seq,cmd_targ_seq,tf_targ_seq) = targ_seq in *)
-(*       let targ_seq' = (Sl_form.subst_tags tagpairs sf_targ_seq, cmd_targ_seq, tf_targ_seq) in  *)
-(*       (\* let subst_seq = Seq.subst theta targ_seq' in *\) *)
-(*       Rule.sequence [ *)
-(* 	  Rule.mk_infrule (fun seq -> [ [(targ_seq', TagPairs.mk (Tl_form.outermost_tag tf_targ_seq), *)
-(* 					  TagPairs.empty)], "Cut" ]); *)
-	  
-(*           Rule.mk_backrule  *)
-(*             false  *)
-(*             (fun _ _ -> [targ_idx])  *)
-(*             (fun s s' ->  *)
-(*              [(if !termination then TagPairs.reflect tagpairs else TagPairs.empty (\* Seq.tagpairs_one *\)), "Backl"]) *)
-(* 	] in *)
-(*   (\* let () = print_endline "Attempting backlink with source seq:" in   *\) *)
-(*   (\* let () = print_endline (Seq.to_string src_seq) in   *\) *)
-(*   let rule_list = (Blist.map f apps) in *)
-(*   (\* let () = print_endline "IS LIST EMPTY? " in *\) *)
-(*   (\* let () = print_endline (string_of_bool (Blist.is_empty rule_list)) in *\) *)
-(*   Rule.first rule_list idx prf *)
-		  
-(* let backlink_cut defs = *)
-(*   let rl s1 s2 = *)
-(*     (\* let () = incr step in *\) *)
-(*     let ((sf1,cmd1,tf1),(sf2,cmd2,tf2)) = (s1,s2) in *)
-(*     if not (Cmd.is_while cmd1) then [] else *)
-(*       let () = debug (fun () -> "CUTLINK3: trying: " ^ (Seq.to_string s2)) in *)
-(*       let () = debug (fun () -> "                  " ^ (Seq.to_string s1)) in *)
-(*       (\* let () = debug (fun () -> "CUTLINK3: step = " ^ (string_of_int !step)) in *\) *)
-(*       (\* if !step <> 22 then None else *\) *)
-(*       if not (Cmd.equal cmd1 cmd2) then [] else *)
-(* 	let olddebug = !Lib.do_debug in *)
-(* 	let () = Lib.do_debug := true in *)
-(* 	let () = Sl_rules.setup defs in *)
-(* 	let result = *)
-(* 	  Option.is_some (Slprover.idfs 1 11 !Sl_rules.axioms !Sl_rules.rules (sf1, sf2)) in *)
-(* 	let () = Lib.do_debug := olddebug in *)
-(* 	let () = debug (fun () -> "CUTLINK3: result: " ^ (string_of_bool result)) in *)
-(* 	if result then *)
-(* 	  [ ((TagPairs.mk (Tl_form.outermost_tag tf1)), "Cut/Backl") ] *)
-(* 	else [] in *)
-(*   Rule.sequence [ *)
-(*       Rule.mk_infrule ([[((sf2,cmd2,tf2), (TagPairs.mk (Tl_form.outermost_tag tf1)),TagPairs.empty)], "Cut" ]); *)
-(*       Rule.mk_backrule true Rule.all_nodes rl] *)
-(* (Blist.map (fun rl -> Rule.mk_backrule true Rule.all_nodes rl) rl) *)
-		   
-
-
-
-    (*     let targ_seq = Proof.get_seq targ_idx prf in *)
-	  (*     (\* [targ_seq'] is as [targ_seq] but with the tags of [src_seq] *\) *)
-	  (*     let (sf_targ_seq,cmd_targ_seq,tf_targ_seq) = targ_seq in *)
-	  (*     let targ_seq' = (Sl_form.subst_tags tagpairs sf_targ_seq, cmd_targ_seq, tf_targ_seq) in  *)
-	  (*     let subst_seq = Seq.subst theta targ_seq' in *)
-	  (*     Rule.sequence [ *)
-	  (* 	  if Seq.equal src_seq subst_seq *)
-	  (* 	  then Rule.identity *)
-	  (* 	  else Rule.mk_infrule (frame subst_seq); *)
-		  
-	  (* 	  if Sl_term.Map.for_all Sl_term.equal theta *)
-	  (* 	  then Rule.identity *)
-	  (* 	  else Rule.mk_infrule (subst_rule theta targ_seq'); *)
-		  
-	  (* 	  Rule.mk_backrule  *)
-	  (* 	    false  *)
-	  (* 	    (fun _ _ -> [targ_idx])  *)
-	  (* 	    (fun s s' ->  *)
-	  (* 	     [(TagPairs.reflect tagpairs), "Backl"]) *)
-	  (* 	] in *)
-	  (*   (\* let () = print_endline "Attempting backlink with source seq:" in   *\) *)
-	  (*   (\* let () = print_endline (Seq.to_string src_seq) in   *\) *)
-	  (*   let rule_list = (Blist.map f apps) in *)
-	  (*   (\* let () = print_endline "IS LIST EMPTY? " in *\) *)
-	  (*   (\* let () = print_endline (string_of_bool (Blist.is_empty rule_list)) in *\) *)
-	  (*   Rule.first rule_list idx prf *)
-	  (* else *)
-	  (*   Rule.identity *)
-		 
-
-  (*   if result then [ (Seq.tagpairs_one, "Cut/Backl") ] else [] in *)
-  (* Rule.mk_backrule true Rule.all_nodes rl *)
-		 
-
-
-  (* 	] in *)
-  (*     [ (Seq.tagpairs_one, "Cut/Backl") ]  *)
-  (*   else [] in *)
-  (* Rule.mk_backrule true Rule.all_nodes rl *)
-
-
 let axioms = 
   let entails f f' =
     let olddebug = !Lib.do_debug in
@@ -746,7 +643,6 @@ let axioms =
     let result = (Slprover.idfs 1 10 !Sl_rules.axioms !Sl_rules.rules (f, f')) in
     let () = Lib.do_debug := olddebug in
     result in
-    (* Slprover.idfs 1 10 !Sl_rules.axioms !Sl_rules.rules (f, f') in *)
   ref (Rule.first [symex_check_axiom entails; symex_empty_axiom; subformula_axiom])
       
 let rules = ref Rule.fail
@@ -790,19 +686,10 @@ let setup defs =
 	       simplify ;
 	       Rule.choice [
 		   dobackl;
-		   Rule.compose_pairwise unfold_gs [Rule.attempt !axioms; (Rule.first [symex;symex_empty_axiom])];
+		   Rule.compose_pairwise unfold_gs [Rule.attempt !axioms; (Rule.first [symex_fair;symex;symex_empty_axiom])];
 		   unfold_fs;
-		   (* Rule.choice  *)
-		   (*   (Blist.map  *)
-		   (* 	(fun c -> Rule.compose (fold c) dobackl)  *)
-		   (* 	(Sl_defs.to_list defs)); *)
-		   (* Rule.choice  *)
-		   (*   (Blist.map  *)
-		   (* 	(fun c -> Rule.compose (fold c) symex)  *)
-		   (* 	(Sl_defs.to_list defs));		    *)
-		   symex;
 		   symex_fair;
-		   (* new_backl_cut; *)
+		   symex;
 		   (Rule.compose (luf defs) (Rule.attempt ex_falso_axiom));
 		   disjunction_rule;
 		   conjunction_rule;