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