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