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