/* This circuit is a miter between
 * x1 = a OR (a' AND b); and
 * y1 = a OR b
 * Miter should be infeasible
 * GB(J + J0) = {1}
 * but GB(J) is not equal to 1, 
 * solution in the closure, outside of F2
 */



ring r = 2, (a, b, c, x1, y1, t), lp;

// c = a' AND n
poly f1 = (1 - a)*b + c;
// x1 = a OR C
poly f2 = a*c + a + c + x1;
// y1 = a OR b
poly f3 = a*b + a + b + y1;
// the miter polynomial
poly f4 = t*(x1 - y1) + 1;

ideal J = f1, f2, f3, f4;

ideal J0 = a^2-a, b^2-b, c^2-c, x1^2 - x1, y1^2 - y1, t^2-t;

printf("GB of J:");
groebner(J);

printf("GB of J + J0:");
groebner(J + J0);