0.00/0.01 YES
0.00/0.01 ; certificate:
0.00/0.01 (0
0.00/0.01 (rr2-rel (compose (inverse (stepsnf (0))) (stepsnf (0))) 0 1)
0.00/0.01 (rr2-rel (compose (inverse (stepsnf (0))) (stepsnf (0))) 0 1)
0.00/0.01 (size 1 2 0))
0.00/0.01 (1 (rr2-rel (equality) 0 1) (rr2-rel (equality) 0 1) (size 1 5 0))
0.00/0.01 (2 (not 1) (not (rr2-rel (equality) 0 1)))
0.00/0.01 (3
0.00/0.01 (and (0 2))
0.00/0.01 (extend-sig 1
0.00/0.01 (and ((rr2-rel (compose (inverse (stepsnf (0))) (stepsnf (0))) 0 1)
0.00/0.01 (not (rr2-rel (equality) 0 1)))))
0.00/0.01 (size 0 0 0))
0.00/0.01 (4
0.00/0.01 (exists 3)
0.00/0.01 (exists (extend-sig 1
0.00/0.01 (and ((rr2-rel (compose (inverse (stepsnf (0))) (stepsnf (0))) 0 1)
0.00/0.01 (not (rr2-rel (equality) 0 1)))))))
0.00/0.01 (5
0.00/0.01 (exists 4)
0.00/0.01 (exists (exists (extend-sig 1
0.00/0.01 (and ((rr2-rel (compose (inverse (stepsnf (0))) (stepsnf (0))) 0 1)
0.00/0.01 (not (rr2-rel (equality) 0 1))))))))
0.00/0.01 (6
0.00/0.01 (not 5)
0.00/0.01 (not (exists (exists (extend-sig 1
0.00/0.01 (and ((rr2-rel (compose (inverse (stepsnf (0))) (stepsnf (0))) 0 1)
0.00/0.01 (not (rr2-rel (equality) 0 1)))))))))
0.00/0.01 (7
0.00/0.01 (nnf+ 6)
0.00/0.01 (extend-sig 1
0.00/0.01 (forall (forall (or ((not (rr2-rel (compose (inverse (stepsnf (0)))
0.00/0.01 (stepsnf (0)))
0.00/0.01 0
0.00/0.01 1))
0.00/0.01 (rr2-rel (equality) 0 1)))))))
0.00/0.01 (nonempty 7)
0.00/0.01 EOF