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
   x + y = y + x.

end_of_list.

formulas(goals).

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

end_of_list.

formulas(hints).

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

end_of_list.
