YES
Certificate:
(0 (rr2 (product (nf (0)) (nf (0))) 0 1) (rr2 (product (nf (0)) (nf (0))) 0 1))
(1 (rr2 (equality) 0 1) (rr2 (equality) 0 1))
(2 (not 1) (not (rr2 (equality) 0 1)))
(3
 (and (0 2))
 (and ((rr2 (product (nf (0)) (nf (0))) 0 1) (not (rr2 (equality) 0 1)))))
(4 (rr2 (step* (0 0-)) 0 1) (rr2 (step* (0 0-)) 0 1))
(5
 (and (3 4))
 (and ((and ((rr2 (product (nf (0)) (nf (0))) 0 1) (not (rr2 (equality) 0 1))))
   (rr2 (step* (0 0-)) 0 1))))
(6
 (exists 5)
 (exists (and ((and ((rr2 (product (nf (0)) (nf (0))) 0 1)
      (not (rr2 (equality) 0 1))))
    (rr2 (step* (0 0-)) 0 1)))))
(7
 (exists 6)
 (exists (exists (and ((and ((rr2 (product (nf (0)) (nf (0))) 0 1)
       (not (rr2 (equality) 0 1))))
     (rr2 (step* (0 0-)) 0 1))))))
(8
 (not 7)
 (not (exists (exists (and ((and ((rr2 (product (nf (0)) (nf (0))) 0 1)
        (not (rr2 (equality) 0 1))))
      (rr2 (step* (0 0-)) 0 1)))))))
(9
 (nnf 8)
 (forall (forall (or ((not (and ((rr2 (product (nf (0)) (nf (0))) 0 1)
        (not (rr2 (equality) 0 1)))))
     (not (rr2 (step* (0 0-)) 0 1)))))))
(nonempty 9)