0.00/0.11	YES
0.00/0.11	; certificate:
0.00/0.11	(0
0.00/0.11	 (rr2-rel (compose (step (0-)) (stepseq (0))) 0 1)
0.00/0.11	 (rr2-rel (compose (step (0-)) (stepseq (0))) 0 1)
0.00/0.11	 (size 44 210 0))
0.00/0.11	(1
0.00/0.11	 (rr2-rel (compose (stepseq (0)) (stepseq (0-))) 0 1)
0.00/0.11	 (rr2-rel (compose (stepseq (0)) (stepseq (0-))) 0 1)
0.00/0.11	 (size 106 2091 0))
0.00/0.11	(2 (not 1) (not (rr2-rel (compose (stepseq (0)) (stepseq (0-))) 0 1)))
0.00/0.11	(3
0.00/0.11	 (and (0 2))
0.00/0.11	 (and ((rr2-rel (compose (step (0-)) (stepseq (0))) 0 1)
0.00/0.11	   (not (rr2-rel (compose (stepseq (0)) (stepseq (0-))) 0 1)))))
0.00/0.11	(4
0.00/0.11	 (exists 3)
0.00/0.11	 (exists (and ((rr2-rel (compose (step (0-)) (stepseq (0))) 0 1)
0.00/0.11	    (not (rr2-rel (compose (stepseq (0)) (stepseq (0-))) 0 1))))))
0.00/0.11	(5
0.00/0.11	 (exists 4)
0.00/0.11	 (exists (exists (and ((rr2-rel (compose (step (0-)) (stepseq (0))) 0 1)
0.00/0.11	     (not (rr2-rel (compose (stepseq (0)) (stepseq (0-))) 0 1)))))))
0.00/0.11	(6
0.00/0.11	 (not 5)
0.00/0.11	 (not (exists (exists (and ((rr2-rel (compose (step (0-)) (stepseq (0))) 0 1)
0.00/0.11	      (not (rr2-rel (compose (stepseq (0)) (stepseq (0-))) 0 1))))))))
0.00/0.11	(7
0.00/0.11	 (nnf+ 6)
0.00/0.11	 (forall (forall (or ((not (rr2-rel (compose (step (0-)) (stepseq (0))) 0 1))
0.00/0.11	     (rr2-rel (compose (stepseq (0)) (stepseq (0-))) 0 1))))))
0.00/0.11	(nonempty 7)
0.00/0.11	EOF