assign(order,kbo).
set(lex_order_vars).

set(para_units_only).

clear(back_demod).
set(restrict_denials).

formulas(assumptions).

   % neardomain axioms

   % additive Bruck loop
   x + 0 = x. 0 + x = x.
   -x + (x + y) = y.
   (x + (y + x)) + z = x + (y + (x + z)).
   -(x + y) = -x + -y.

   % multiplicative group
   (x * y) * z = x * (y * z).
   1 * x = x. x * 1 = x.
   x != 0 -> x' * x = 1.
   x != 0 -> x * x' = 1.
   x != 0 -> x'' = x.
   x != 0 & y != 0 -> (x * y)' = y' * x'.

   % compatibility
   0 * x = 0.
   x * (y + z) = (x * y) + (x * z).
   1 != 0. 1' = 1.
   -1 != 0. (-1)' = -1.

   % special automorphism
   -(x + y) + (x + (y + z)) = d(x,y) * z.

   % -----------------
   % extra assumptions
   % -----------------

   % suffices
   d(x,y) = 1 # label("nearfield").

end_of_list.

formulas(goals).

   x + y = y + x # label("commutativity of +").

end_of_list.

formulas(hints).

-x + x = 0.
--x + y = x + y.
-(x * y) + (x * (y + z)) = x * z.
0 = -0.
-0 = 0.
--x + 0 = x.
x + 0 = --x.
--x = x + 0.
x + (-x + y) = y.
x + -x = 0.
x + -(x + y) = -y.
(x + y) + (d(x,y) * z) = x + (y + z).
-(x * y) + (x * y) = x * 0.
-(x * y) + (x * 0) = x * -y.
x * 0 = 0.
x * -0 = 0.
-(x * y) + 0 = x * -y.
x * -y = -(x * y).
-(x * y) = x * -y.
-(0 * x) = 0.
(x + y) + (1 * z) = x + (y + z).
(x + y) + z = x + (y + z).
0 + (0 + x) = x.
-(x * 0) = 0.
0 + (0 * x) = 0.
0 + (x * 0) = 0.
(x + 0) + 0 = x.
0 + 0 = 0 * x.
0 * x = 0 + 0.
0 + 0 = x * 0.
x * 0 = 0 + 0.
x = x + (0 + 0).
x + (0 + 0) = x.
x + (0 * y) = x.
x + (y * 0) = x.
-x + x = y * 0.
x * 0 = -y + y.
x + (-y + y) = x.
(x + -y) + y = x.
-x + (y + x) = y.

end_of_list.
