0.00/0.09	YES
0.00/0.09	; certificate:
0.00/0.09	(0
0.00/0.09	 (rr2-rel (inter (stepseq (0 0-)) (product (terms) (normal-forms (0)))) 0 1)
0.00/0.09	 (rr2-rel (inter (stepseq (0 0-)) (product (terms) (normal-forms (0)))) 0 1)
0.00/0.09	 (size 8 30 0))
0.00/0.09	(1 (rr2-rel (stepseq (0)) 0 1) (rr2-rel (stepseq (0)) 0 1) (size 3 14 0))
0.00/0.09	(2 (not 1) (not (rr2-rel (stepseq (0)) 0 1)))
0.00/0.09	(3
0.00/0.09	 (and (0 2))
0.00/0.09	 (extend-sig 1
0.00/0.09	  (and ((rr2-rel (inter (stepseq (0 0-)) (product (terms) (normal-forms (0))))
0.00/0.09	     0
0.00/0.09	     1)
0.00/0.09	    (not (rr2-rel (stepseq (0)) 0 1)))))
0.00/0.09	 (size 0 0 0))
0.00/0.09	(4
0.00/0.09	 (exists 3)
0.00/0.09	 (exists (extend-sig 1
0.00/0.09	   (and ((rr2-rel (inter (stepseq (0 0-)) (product (terms) (normal-forms (0))))
0.00/0.09	      0
0.00/0.09	      1)
0.00/0.09	     (not (rr2-rel (stepseq (0)) 0 1)))))))
0.00/0.09	(5
0.00/0.09	 (exists 4)
0.00/0.09	 (exists (exists (extend-sig 1
0.00/0.09	    (and ((rr2-rel (inter (stepseq (0 0-)) (product (terms) (normal-forms (0))))
0.00/0.09	       0
0.00/0.09	       1)
0.00/0.09	      (not (rr2-rel (stepseq (0)) 0 1))))))))
0.00/0.09	(6
0.00/0.09	 (not 5)
0.00/0.09	 (not (exists (exists (extend-sig 1
0.00/0.09	     (and ((rr2-rel (inter (stepseq (0 0-))
0.00/0.09	         (product (terms) (normal-forms (0))))
0.00/0.09	        0
0.00/0.09	        1)
0.00/0.09	       (not (rr2-rel (stepseq (0)) 0 1)))))))))
0.00/0.09	(7
0.00/0.09	 (nnf+ 6)
0.00/0.09	 (extend-sig 1
0.00/0.09	  (forall (forall (or ((not (rr2-rel (inter (stepseq (0 0-))
0.00/0.09	         (product (terms) (normal-forms (0))))
0.00/0.09	        0
0.00/0.09	        1))
0.00/0.09	      (rr2-rel (stepseq (0)) 0 1)))))))
0.00/0.09	(nonempty 7)
0.00/0.09	EOF