0.00/0.12	NO
0.00/0.12	formula body / witness:
0.00/0.12	    Σ+[2](((0 (NF[0] × NF[0]) 1 ∧ ¬ 0 = 1) ∧ 0 <->* 1))
0.00/0.12	    0 = f(_00(),b())
0.00/0.12	    1 = f(_01(),b())
0.00/0.12	Certificate:
0.11/0.12	(0 (rr2 (product (nf (0)) (nf (0))) 0 1) (rr2 (product (nf (0)) (nf (0))) 0 1))
0.11/0.12	(1 (rr2 (equality) 0 1) (rr2 (equality) 0 1))
0.11/0.12	(2 (not 1) (not (rr2 (equality) 0 1)))
0.11/0.12	(3
0.11/0.12	 (and (0 2))
0.11/0.12	 (and ((rr2 (product (nf (0)) (nf (0))) 0 1) (not (rr2 (equality) 0 1)))))
0.11/0.12	(4 (rr2 (step* (0 0-)) 0 1) (rr2 (step* (0 0-)) 0 1))
0.11/0.12	(5
0.11/0.12	 (and (3 4))
0.11/0.12	 (and ((and ((rr2 (product (nf (0)) (nf (0))) 0 1) (not (rr2 (equality) 0 1))))
0.11/0.12	   (rr2 (step* (0 0-)) 0 1))))
0.11/0.12	(6
0.11/0.12	 (exists 5)
0.11/0.12	 (exists (and ((and ((rr2 (product (nf (0)) (nf (0))) 0 1)
0.11/0.12	      (not (rr2 (equality) 0 1))))
0.11/0.12	    (rr2 (step* (0 0-)) 0 1)))))
0.11/0.12	(7
0.11/0.12	 (exists 6)
0.11/0.12	 (exists (exists (and ((and ((rr2 (product (nf (0)) (nf (0))) 0 1)
0.11/0.12	       (not (rr2 (equality) 0 1))))
0.11/0.12	     (rr2 (step* (0 0-)) 0 1))))))
0.11/0.12	(8
0.11/0.12	 (not 7)
0.11/0.12	 (not (exists (exists (and ((and ((rr2 (product (nf (0)) (nf (0))) 0 1)
0.11/0.12	        (not (rr2 (equality) 0 1))))
0.11/0.12	      (rr2 (step* (0 0-)) 0 1)))))))
0.11/0.12	(9
0.11/0.12	 (nnf 8)
0.11/0.12	 (forall (forall (or ((not (and ((rr2 (product (nf (0)) (nf (0))) 0 1)
0.11/0.12	        (not (rr2 (equality) 0 1)))))
0.11/0.12	     (not (rr2 (step* (0 0-)) 0 1)))))))
0.11/0.12	(empty 9)
0.11/0.12	EOF