2.88/2.90	NO
2.88/2.90	Certified
2.88/2.90	(0
2.88/2.90	 (rr2 (comp (inverse (step* (1))) (step* (0))) 0 1)
2.88/2.90	 (rr2 (comp (inverse (step* (1))) (step* (0))) 0 1))
2.88/2.90	(1
2.88/2.90	 (rr2 (comp (step* (0)) (inverse (step* (1)))) 0 1)
2.88/2.90	 (rr2 (comp (step* (0)) (inverse (step* (1)))) 0 1))
2.88/2.90	(2 (not 1) (not (rr2 (comp (step* (0)) (inverse (step* (1)))) 0 1)))
2.88/2.90	(3
2.88/2.90	 (and (0 2))
2.88/2.90	 (and ((rr2 (comp (inverse (step* (1))) (step* (0))) 0 1)
2.88/2.90	   (not (rr2 (comp (step* (0)) (inverse (step* (1)))) 0 1)))))
2.88/2.90	(4
2.88/2.90	 (exists 3)
2.88/2.90	 (exists (and ((rr2 (comp (inverse (step* (1))) (step* (0))) 0 1)
2.88/2.90	    (not (rr2 (comp (step* (0)) (inverse (step* (1)))) 0 1))))))
2.88/2.90	(5
2.88/2.90	 (exists 4)
2.88/2.90	 (exists (exists (and ((rr2 (comp (inverse (step* (1))) (step* (0))) 0 1)
2.88/2.90	     (not (rr2 (comp (step* (0)) (inverse (step* (1)))) 0 1)))))))
2.88/2.90	(6
2.88/2.90	 (not 5)
2.88/2.90	 (not (exists (exists (and ((rr2 (comp (inverse (step* (1))) (step* (0))) 0 1)
2.88/2.90	      (not (rr2 (comp (step* (0)) (inverse (step* (1)))) 0 1))))))))
2.88/2.90	(7
2.88/2.90	 (nnf 6)
2.88/2.90	 (forall (forall (or ((not (rr2 (comp (inverse (step* (1))) (step* (0))) 0 1))
2.88/2.90	     (rr2 (comp (step* (0)) (inverse (step* (1)))) 0 1))))))
2.88/2.90	(empty 7)
2.88/2.90	EOF