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