0.00/0.00	NO
0.00/0.00	formula body / witness:
0.00/0.00	    Σ+[0]((0 ((->*[1])⁻ o ->*) 1 ∧ ¬ 0 (->* o (->*[1])⁻) 1))
0.00/0.00	    0 = a()
0.00/0.00	    1 = h(b(),a())
0.00/0.00	Certificate:
0.00/0.01	(0
0.00/0.01	 (rr2 (comp (inverse (step* (1))) (step* (0))) 0 1)
0.00/0.01	 (rr2 (comp (inverse (step* (1))) (step* (0))) 0 1))
0.00/0.01	(1
0.00/0.01	 (rr2 (comp (step* (0)) (inverse (step* (1)))) 0 1)
0.00/0.01	 (rr2 (comp (step* (0)) (inverse (step* (1)))) 0 1))
0.00/0.01	(2 (not 1) (not (rr2 (comp (step* (0)) (inverse (step* (1)))) 0 1)))
0.00/0.01	(3
0.00/0.01	 (and (0 2))
0.00/0.01	 (and ((rr2 (comp (inverse (step* (1))) (step* (0))) 0 1)
0.00/0.01	   (not (rr2 (comp (step* (0)) (inverse (step* (1)))) 0 1)))))
0.00/0.01	(4
0.00/0.01	 (exists 3)
0.00/0.01	 (exists (and ((rr2 (comp (inverse (step* (1))) (step* (0))) 0 1)
0.00/0.01	    (not (rr2 (comp (step* (0)) (inverse (step* (1)))) 0 1))))))
0.00/0.01	(5
0.00/0.01	 (exists 4)
0.00/0.01	 (exists (exists (and ((rr2 (comp (inverse (step* (1))) (step* (0))) 0 1)
0.00/0.01	     (not (rr2 (comp (step* (0)) (inverse (step* (1)))) 0 1)))))))
0.00/0.01	(6
0.00/0.01	 (not 5)
0.00/0.01	 (not (exists (exists (and ((rr2 (comp (inverse (step* (1))) (step* (0))) 0 1)
0.00/0.01	      (not (rr2 (comp (step* (0)) (inverse (step* (1)))) 0 1))))))))
0.00/0.01	(7
0.00/0.01	 (nnf 6)
0.00/0.01	 (forall (forall (or ((not (rr2 (comp (inverse (step* (1))) (step* (0))) 0 1))
0.00/0.01	     (rr2 (comp (step* (0)) (inverse (step* (1)))) 0 1))))))
0.00/0.01	(empty 7)
0.00/0.01	EOF