0.00/0.01	NO
0.00/0.01	; formula body / witness:
0.00/0.01	;     Σ+[2]((0 (<->* ∩ (NF[0] × NF[0])) 1 ∧ ¬ 0 = 1))
0.00/0.01	;     0 = f(a'())
0.00/0.01	;     1 = b()
0.00/0.01	; certificate:
0.00/0.01	(0
0.00/0.01	 (rr2-rel (inter (stepseq (0 0-))
0.00/0.01	   (product (normal-forms (0)) (normal-forms (0))))
0.00/0.01	  0
0.00/0.01	  1)
0.00/0.01	 (rr2-rel (inter (stepseq (0 0-))
0.00/0.01	   (product (normal-forms (0)) (normal-forms (0))))
0.00/0.01	  0
0.00/0.01	  1)
0.00/0.01	 (size 10 18 0))
0.00/0.01	(1 (rr2-rel (equality) 0 1) (rr2-rel (equality) 0 1) (size 1 7 0))
0.00/0.01	(2 (not 1) (not (rr2-rel (equality) 0 1)))
0.00/0.01	(3
0.00/0.01	 (and (0 2))
0.00/0.01	 (extend-sig 2
0.00/0.01	  (and ((rr2-rel (inter (stepseq (0 0-))
0.00/0.01	      (product (normal-forms (0)) (normal-forms (0))))
0.00/0.01	     0
0.00/0.01	     1)
0.00/0.01	    (not (rr2-rel (equality) 0 1)))))
0.00/0.01	 (size 8 12 0))
0.00/0.01	(4
0.00/0.01	 (exists 3)
0.00/0.01	 (exists (extend-sig 2
0.00/0.01	   (and ((rr2-rel (inter (stepseq (0 0-))
0.00/0.01	       (product (normal-forms (0)) (normal-forms (0))))
0.00/0.01	      0
0.00/0.01	      1)
0.00/0.01	     (not (rr2-rel (equality) 0 1)))))))
0.00/0.01	(5
0.00/0.01	 (exists 4)
0.00/0.01	 (exists (exists (extend-sig 2
0.00/0.01	    (and ((rr2-rel (inter (stepseq (0 0-))
0.00/0.01	        (product (normal-forms (0)) (normal-forms (0))))
0.00/0.01	       0
0.00/0.01	       1)
0.00/0.01	      (not (rr2-rel (equality) 0 1))))))))
0.00/0.01	(6
0.00/0.01	 (not 5)
0.00/0.01	 (not (exists (exists (extend-sig 2
0.00/0.01	     (and ((rr2-rel (inter (stepseq (0 0-))
0.00/0.01	         (product (normal-forms (0)) (normal-forms (0))))
0.00/0.01	        0
0.00/0.01	        1)
0.00/0.01	       (not (rr2-rel (equality) 0 1)))))))))
0.00/0.01	(7
0.00/0.01	 (nnf+ 6)
0.00/0.01	 (extend-sig 2
0.00/0.01	  (forall (forall (or ((not (rr2-rel (inter (stepseq (0 0-))
0.00/0.01	         (product (normal-forms (0)) (normal-forms (0))))
0.00/0.01	        0
0.00/0.01	        1))
0.00/0.01	      (rr2-rel (equality) 0 1)))))))
0.00/0.01	(empty 7)
0.00/0.01	EOF