0.00/0.33 YES 0.00/0.34 Certificate: 0.00/0.34 (0 0.00/0.34 (rr2 (comp (inverse (step! (0))) (step! (0))) 0 1) 0.00/0.34 (rr2 (comp (inverse (step! (0))) (step! (0))) 0 1)) 0.00/0.34 (1 (rr2 (equality) 0 1) (rr2 (equality) 0 1)) 0.00/0.34 (2 (not 1) (not (rr2 (equality) 0 1))) 0.00/0.34 (3 0.00/0.34 (and (0 2)) 0.00/0.34 (and ((rr2 (comp (inverse (step! (0))) (step! (0))) 0 1) 0.00/0.34 (not (rr2 (equality) 0 1))))) 0.00/0.34 (4 0.00/0.34 (exists 3) 0.00/0.34 (exists (and ((rr2 (comp (inverse (step! (0))) (step! (0))) 0 1) 0.00/0.34 (not (rr2 (equality) 0 1)))))) 0.00/0.34 (5 0.00/0.34 (exists 4) 0.00/0.34 (exists (exists (and ((rr2 (comp (inverse (step! (0))) (step! (0))) 0 1) 0.00/0.34 (not (rr2 (equality) 0 1))))))) 0.00/0.34 (6 0.00/0.34 (not 5) 0.00/0.34 (not (exists (exists (and ((rr2 (comp (inverse (step! (0))) (step! (0))) 0 1) 0.00/0.34 (not (rr2 (equality) 0 1)))))))) 0.00/0.34 (7 0.00/0.34 (nnf 6) 0.00/0.34 (forall (forall (or ((not (rr2 (comp (inverse (step! (0))) (step! (0))) 0 1)) 0.00/0.34 (rr2 (equality) 0 1)))))) 0.00/0.34 (nonempty 7) 0.00/0.34 EOF