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