3.54/3.59	YES
3.54/3.59	Certified
3.54/3.59	(0
3.54/3.59	 (rr2 (comp (inverse (step! (0))) (step! (0))) 0 1)
3.54/3.59	 (rr2 (comp (inverse (step! (0))) (step! (0))) 0 1))
3.54/3.59	(1 (rr2 (equality) 0 1) (rr2 (equality) 0 1))
3.54/3.59	(2 (not 1) (not (rr2 (equality) 0 1)))
3.54/3.59	(3
3.54/3.59	 (and (0 2))
3.54/3.59	 (and ((rr2 (comp (inverse (step! (0))) (step! (0))) 0 1)
3.54/3.59	   (not (rr2 (equality) 0 1)))))
3.54/3.59	(4
3.54/3.59	 (exists 3)
3.54/3.59	 (exists (and ((rr2 (comp (inverse (step! (0))) (step! (0))) 0 1)
3.54/3.59	    (not (rr2 (equality) 0 1))))))
3.54/3.59	(5
3.54/3.59	 (exists 4)
3.54/3.59	 (exists (exists (and ((rr2 (comp (inverse (step! (0))) (step! (0))) 0 1)
3.54/3.59	     (not (rr2 (equality) 0 1)))))))
3.54/3.59	(6
3.54/3.59	 (not 5)
3.54/3.59	 (not (exists (exists (and ((rr2 (comp (inverse (step! (0))) (step! (0))) 0 1)
3.54/3.59	      (not (rr2 (equality) 0 1))))))))
3.54/3.59	(7
3.54/3.59	 (nnf 6)
3.54/3.59	 (forall (forall (or ((not (rr2 (comp (inverse (step! (0))) (step! (0))) 0 1))
3.54/3.59	     (rr2 (equality) 0 1))))))
3.54/3.59	(nonempty 7)
3.54/3.59	EOF