% ----------------------------- % Theorem 3. Original version. % ----------------------------- assign(order,kbo). set(lex_order_vars). set(paramodulation). set(hyper_resolution). formulas(assumptions). x * (y * x) = y. x * y = y * x. e * e = e. x + e = x. e + y = y. % gL clauses z * x0 != z * y0 | w * x0 = w * y0 # label("gL"). (z * x0) * x1 != (z * y0) * y1 | (w * x0) * x1 = (w * y0) * y1 # label("gL"). x0 * (z * x1) != y0 * (z * y1) | x0 * (w * x1) = y0 * (w * y1) # label("gL"). (z * x0) + x1 != (z * y0) + y1 | (w * x0) + x1 = (w * y0) + y1 # label("gL"). x0 + (z * x1) != y0 + (z * y1) | x0 + (w * x1) = y0 + (w * y1) # label("gL"). x0 * z != y0 * z | x0 * w = y0 * w # label("gL"). (x0 * z) * x1 != (y0 * z) * y1 | (x0 * w) * x1 = (y0 * w) * y1 # label("gL"). x0 * (x1 * z) != y0 * (y1 * z) | x0 * (x1 * w) = y0 * (y1 * w) # label("gL"). (x0 * z) + x1 != (y0 * z) + y1 | (x0 * w) + x1 = (y0 * w) + y1 # label("gL"). x0 + (x1 * z) != y0 + (y1 * z) | x0 + (x1 * w) = y0 + (y1 * w) # label("gL"). z + x0 != z + y0 | w + x0 = w + y0 # label("gL"). (z + x0) * x1 != (z + y0) * y1 | (w + x0) * x1 = (w + y0) * y1 # label("gL"). x0 * (z + x1) != y0 * (z + y1) | x0 * (w + x1) = y0 * (w + y1) # label("gL"). (z + x0) + x1 != (z + y0) + y1 | (w + x0) + x1 = (w + y0) + y1 # label("gL"). x0 + (z + x1) != y0 + (z + y1) | x0 + (w + x1) = y0 + (w + y1) # label("gL"). x0 + z != y0 + z | x0 + w = y0 + w # label("gL"). (x0 + z) * x1 != (y0 + z) * y1 | (x0 + w) * x1 = (y0 + w) * y1 # label("gL"). x0 * (x1 + z) != y0 * (y1 + z) | x0 * (x1 + w) = y0 * (y1 + w) # label("gL"). (x0 + z) + x1 != (y0 + z) + y1 | (x0 + w) + x1 = (y0 + w) + y1 # label("gL"). x0 + (x1 + z) != y0 + (y1 + z) | x0 + (x1 + w) = y0 + (y1 + w) # label("gL"). % denial of all 4 goals (a * b) * e != a + b | a + (a * e) != e | a + b != b + a | a + (b + c) != (a + b) + c. end_of_list.