1.59/1.67	YES
1.59/1.67	Certified
1.59/1.67	(0 (rr2 (product (nf (0)) (nf (0))) 0 1) (rr2 (product (nf (0)) (nf (0))) 0 1))
1.59/1.67	(1 (rr2 (equality) 0 1) (rr2 (equality) 0 1))
1.59/1.67	(2 (not 1) (not (rr2 (equality) 0 1)))
1.59/1.67	(3
1.59/1.67	 (and (0 2))
1.59/1.67	 (and ((rr2 (product (nf (0)) (nf (0))) 0 1) (not (rr2 (equality) 0 1)))))
1.59/1.67	(4 (rr2 (step* (0 0-)) 0 1) (rr2 (step* (0 0-)) 0 1))
1.59/1.67	(5
1.59/1.67	 (and (3 4))
1.59/1.67	 (and ((and ((rr2 (product (nf (0)) (nf (0))) 0 1) (not (rr2 (equality) 0 1))))
1.59/1.67	   (rr2 (step* (0 0-)) 0 1))))
1.59/1.67	(6
1.59/1.67	 (exists 5)
1.59/1.67	 (exists (and ((and ((rr2 (product (nf (0)) (nf (0))) 0 1)
1.59/1.67	      (not (rr2 (equality) 0 1))))
1.59/1.67	    (rr2 (step* (0 0-)) 0 1)))))
1.59/1.67	(7
1.59/1.67	 (exists 6)
1.59/1.67	 (exists (exists (and ((and ((rr2 (product (nf (0)) (nf (0))) 0 1)
1.59/1.67	       (not (rr2 (equality) 0 1))))
1.59/1.67	     (rr2 (step* (0 0-)) 0 1))))))
1.59/1.67	(8
1.59/1.67	 (not 7)
1.59/1.67	 (not (exists (exists (and ((and ((rr2 (product (nf (0)) (nf (0))) 0 1)
1.59/1.67	        (not (rr2 (equality) 0 1))))
1.59/1.67	      (rr2 (step* (0 0-)) 0 1)))))))
1.59/1.67	(9
1.59/1.67	 (nnf 8)
1.59/1.67	 (forall (forall (or ((not (and ((rr2 (product (nf (0)) (nf (0))) 0 1)
1.59/1.67	        (not (rr2 (equality) 0 1)))))
1.59/1.67	     (not (rr2 (step* (0 0-)) 0 1)))))))
1.59/1.67	(nonempty 9)
1.59/1.67	EOF