0.00/0.15	NO
0.00/0.15	Certified
0.00/0.15	(0
0.00/0.15	 (rr2 (comp (step (0-)) (step! (0))) 1 0)
0.00/0.15	 (rr2 (comp (step (0-)) (step! (0))) 1 0))
0.00/0.15	(1 (rr2 (step* (0)) 1 0) (rr2 (step* (0)) 1 0))
0.00/0.15	(2 (not 1) (not (rr2 (step* (0)) 1 0)))
0.00/0.15	(3
0.00/0.15	 (and (0 2))
0.00/0.15	 (and ((rr2 (comp (step (0-)) (step! (0))) 1 0) (not (rr2 (step* (0)) 1 0)))))
0.00/0.15	(4
0.00/0.15	 (exists 3)
0.00/0.15	 (exists (and ((rr2 (comp (step (0-)) (step! (0))) 1 0)
0.00/0.15	    (not (rr2 (step* (0)) 1 0))))))
0.00/0.15	(5
0.00/0.15	 (exists 4)
0.00/0.15	 (exists (exists (and ((rr2 (comp (step (0-)) (step! (0))) 1 0)
0.00/0.15	     (not (rr2 (step* (0)) 1 0)))))))
0.00/0.15	(6
0.00/0.15	 (not 5)
0.00/0.15	 (not (exists (exists (and ((rr2 (comp (step (0-)) (step! (0))) 1 0)
0.00/0.15	      (not (rr2 (step* (0)) 1 0))))))))
0.00/0.15	(7
0.00/0.15	 (nnf 6)
0.00/0.15	 (forall (forall (or ((not (rr2 (comp (step (0-)) (step! (0))) 1 0))
0.00/0.15	     (rr2 (step* (0)) 1 0))))))
0.00/0.15	(empty 7)
0.00/0.15	EOF