http://cstheory.blogoverflow.com/2012/02/something-you-should-know-about-quantifier-elimination-part-ii/ のアルゴリズムを実装したらどうもうまく動かないで随分長い時間悩んでしまったが、どうも説明が間違っていたようだ。
このzmodの定義だと、例えば、{ax^2 + bx + c, 2ax+b} から始めると、
(ax^2 + bx + c) zmod (2ax+b) = abx + 2ac
(ax^2 + bx + c) zmod (abx + 2ac) = (ab^2 - 2a^2c)x + abc
(ax^2 + bx + c) zmod ((ab^2 - 2a^2c)x + abc) = (ab^3 - 3a^2bc)x + (ab^2c - 2a^2c^2)
となるので多項式の集合が収束しない(多分)。
さらに元ネタの https://math.umons.ac.be/preprints/src/Ozturk020411.pdf を見てみたら、違う定義を使っていて、こっちだと収束するのは明らか……