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