1.28/1.34	YES
1.28/1.34	Certified
1.28/1.34	(0
1.28/1.34	 (rr2 (comp (inverse (step* (1))) (step* (0))) 0 1)
1.28/1.34	 (rr2 (comp (inverse (step* (1))) (step* (0))) 0 1))
1.28/1.34	(1
1.28/1.34	 (rr2 (comp (step* (0)) (inverse (step* (1)))) 0 1)
1.28/1.34	 (rr2 (comp (step* (0)) (inverse (step* (1)))) 0 1))
1.28/1.34	(2 (not 1) (not (rr2 (comp (step* (0)) (inverse (step* (1)))) 0 1)))
1.28/1.34	(3
1.28/1.34	 (and (0 2))
1.28/1.34	 (and ((rr2 (comp (inverse (step* (1))) (step* (0))) 0 1)
1.28/1.34	   (not (rr2 (comp (step* (0)) (inverse (step* (1)))) 0 1)))))
1.28/1.34	(4
1.28/1.34	 (exists 3)
1.28/1.34	 (exists (and ((rr2 (comp (inverse (step* (1))) (step* (0))) 0 1)
1.28/1.34	    (not (rr2 (comp (step* (0)) (inverse (step* (1)))) 0 1))))))
1.28/1.34	(5
1.28/1.34	 (exists 4)
1.28/1.34	 (exists (exists (and ((rr2 (comp (inverse (step* (1))) (step* (0))) 0 1)
1.28/1.34	     (not (rr2 (comp (step* (0)) (inverse (step* (1)))) 0 1)))))))
1.28/1.34	(6
1.28/1.34	 (not 5)
1.28/1.34	 (not (exists (exists (and ((rr2 (comp (inverse (step* (1))) (step* (0))) 0 1)
1.28/1.34	      (not (rr2 (comp (step* (0)) (inverse (step* (1)))) 0 1))))))))
1.28/1.34	(7
1.28/1.34	 (nnf 6)
1.28/1.34	 (forall (forall (or ((not (rr2 (comp (inverse (step* (1))) (step* (0))) 0 1))
1.28/1.34	     (rr2 (comp (step* (0)) (inverse (step* (1)))) 0 1))))))
1.28/1.34	(nonempty 7)
1.28/1.35	EOF