% GMV algebras:  Prove all 15 goals

op(500, infix, "V").   % join
op(500, infix, "^").   % meet
op(500,infix,"@").     % Graetzer-Lakser-Plonka star

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

clear(cac_redundancy).

set(para_from_small).

clear(back_demod).
set(restrict_denials).

assign(max_weight,  5).

formulas(assumptions).

   (x ^ y) ^ z = x ^ (y ^ z)               # label("Associativity-^").
   (x V y) V z = x V (y V z)               # label("Associativity-V").
   x ^ x = x                               # label("Idempotence-^").
   x V x = x                               # label("Idempotence-V").
   x ^ y = y ^ x                           # label("Commutativity-^").
   x V y = y V x                           # label("Commutativity-V").
   (x ^ y) V x = x                         # label("Absorption a").
   (x V y) ^ x = x                         # label("Absorption b").
   
   (x * ((x \ z) ^ y)) V z = z             # label("Residual a").
   ((y ^ (z / x)) * x) V z = z             # label("Residual b").
   (x \ ((x * y) V z)) ^ y = y             # label("Residual c").
   (((y * x) V z) / x) ^ y = y             # label("Residual d").
   
   (x * y) * z = x * (y * z)               # label("Associativity-* (fusion)").
   1 * x = x                               # label("Left monoid unit").
   x * 1 = x                               # label("Right monoid unit").
   
   x V y = x / ((x V y) \ x)               # label("GMV a").
   x V y = (x / (x V y)) \ x               # label("GMV b").
   
   x @ y = (x * (x \ 1)) * ((y \ 1) \ 1)   # label("Definition-@").

end_of_list.

formulas(goals).

   x @ x = x                               # label("Goal 1").
   (x @ y) @ z = x @ z                     # label("Goal 2").
   x @ (y @ z) = x @ z                     # label("Goal 3").
  
   (x ^ y) @ (z ^ u) = (x @ z) ^ (y @ u)   # label("Goal 4").
   (x V y) @ (z V u) = (x @ z) V (y @ u)   # label("Goal 5").
   (x \ y) @ (z \ u) = (x @ z) \ (y @ u)   # label("Goal 6").
   (x / y) @ (z / u) = (x @ z) / (y @ u)   # label("Goal 7").
  
   (x * (x \ 1)) @ 1 = x * (x \ 1)         # label("Goal 8").
   1 @ (x * (x \ 1)) = 1                   # label("Goal 9").
   (x \ 1) @ 1 = 1                         # label("Goal 10").
   1 @ (x \ 1) = x \ 1                     # label("Goal 11").
  
   (x / (y \ x)) @ (x V y) = x V y         # label("Goal 12").
   ((x / y) \ x) @ (x V y) = x V y         # label("Goal 13").
   (x V y) @ (x / (y \ x)) = x / (y \ x)   # label("Goal 14").
   (x V y) @ ((x / y) \ x) = (x / y) \ x   # label("Goal 15").

end_of_list.

%
% Hints extracted from previously found proofs.
%

formulas(hints).

(x ^ y) ^ z = x ^ (y ^ z).
(x V y) V z = x V (y V z).
x ^ x = x.
x V x = x.
x ^ y = y ^ x.
x V y = y V x.
(x ^ y) V x = x.
(x V y) ^ x = x.
(x * ((x \ y) ^ z)) V y = y.
((x ^ (y / z)) * z) V y = y.
(x \ ((x * y) V z)) ^ y = y.
(((x * y) V z) / y) ^ x = x.
(x * y) * z = x * (y * z).
1 * x = x.
x * 1 = x.
x V y = (x / (x V y)) \ x.
(x / (x V y)) \ x = x V y.
x @ y = (x * (x \ 1)) * ((y \ 1) \ 1).
(x * (x \ 1)) * ((y \ 1) \ 1) = x @ y.
1 @ (c25 * (c25 \ 1)) != 1 # answer("Goal 9") # label("Goal 9").
x V (y V z) = y V (z V x).
x V (y V z) = z V (x V y).
(x ^ y) V y = y.
x = x V (x ^ y).
x V (x ^ y) = x.
x = x ^ (x V y).
x ^ (x V y) = x.
(x V y) ^ y = y.
(x * (y ^ (x \ z))) V z = z.
x = x V (y * ((y \ x) ^ z)).
x V (y * ((y \ x) ^ z)) = x.
x = x V ((y ^ (x / z)) * z).
x V ((y ^ (x / z)) * z) = x.
x = x ^ (y \ ((y * x) V z)).
x ^ (y \ ((y * x) V z)) = x.
(x \ (y V (x * z))) ^ z = z.
x = x ^ (((x * y) V z) / y).
x ^ (((x * y) V z) / y) = x.
((x V (y * z)) / z) ^ y = y.
(x / (x V x)) \ x = x.
((x ^ y) / x) \ (x ^ y) = (x ^ y) V x.
(1 \ 1) * ((x \ 1) \ 1) = 1 @ x.
x = x V (y ^ x).
x V (y ^ x) = x.
x V ((x ^ y) ^ z) = x.
x ^ (y V x) = x.
x ^ (y V (z V x)) = x.
(x / x) \ x = x.
x V (y ^ (x ^ z)) = x.
x ^ (y V (x V z)) = x.
x V y = (y ^ z) V (x V y).
(x ^ y) V (z V x) = z V x.
x = x V (y * (z ^ (y \ x))).
x V (y * (z ^ (y \ x))) = x.
x V (y * (y \ x)) = x.
x V (1 \ x) = x.
x ^ (y * (y \ x)) = y * (y \ x).
x ^ (1 \ x) = 1 \ x.
x V ((y ^ (z ^ (x / u))) * u) = x.
x V ((x / y) * y) = x.
x V (x / 1) = x.
x ^ ((x / y) * y) = (x / y) * y.
x ^ (x / 1) = x / 1.
x ^ (y \ (y * x)) = x.
x ^ (y \ (z V (y * x))) = x.
1 ^ (x \ (x V y)) = 1.
x ^ ((y * z) \ (y * (z * x))) = x.
x ^ (1 \ x) = x.
1 ^ (x \ x) = 1.
x V (y \ (y * x)) = y \ (y * x).
(x \ (x * y)) V y = x \ (x * y).
x = 1 \ x.
1 \ x = x.
(x ^ 1) ^ (y \ y) = x ^ 1.
1 V (x \ x) = x \ x.
1 ^ ((x ^ y) \ y) = 1.
1 ^ (x V (y \ y)) = 1.
1 ^ ((x \ x) V y) = 1.
x ^ ((x * y) / y) = x.
x ^ ((y V (x * z)) / z) = x.
x ^ (y / (z ^ (x \ y))) = x.
(x * y) ^ ((x * (y * z)) / z) = x * y.
1 ^ (x / x) = 1.
x ^ (x / 1) = x.
x V ((x * y) / y) = (x * y) / y.
(x ^ 1) ^ (y / y) = x ^ 1.
1 V (x / x) = x / x.
(x / x) V 1 = x / x.
x = x / 1.
x / 1 = x.
(x / (y \ x)) ^ y = y.
x = x ^ (y / (x \ y)).
x ^ (y / (x \ y)) = x.
x ^ ((y * z) \ (u V (y * (z * x)))) = x.
x ^ ((y / x) \ y) = x.
x V (x * (y ^ 1)) = x.
x V (x * (1 ^ y)) = x.
1 ^ (x \ (y / (z ^ (x \ y)))) = 1.
x V ((y ^ 1) * x) = x.
x V ((1 ^ y) * x) = x.
1 * ((x \ 1) \ 1) = 1 @ x.
1 @ x = (x \ 1) \ 1.
(x \ 1) \ 1 = 1 @ x.
x V (y * (z * (z \ (y \ x)))) = x.
x V ((y * (y \ 1)) * x) = x.
x V (y * ((y \ 1) * x)) = x.
(x \ y) ^ ((x \ 1) * y) = (x \ 1) * y.
x V ((y ^ z) * (z \ x)) = x.
x V (y * ((y V z) \ x)) = x.
x V ((1 V y) \ x) = x.
(x \ y) ^ ((x V z) \ y) = (x V z) \ y.
x V ((y / y) \ x) = x.
x V (((x ^ y) / z) * z) = x.
x V (y ^ ((x / z) * z)) = x.
x V (x * ((1 / y) * y)) = x.
x V (((1 / y) * y) * x) = x.
x ^ (((y ^ z) / x) \ y) = x.
x V ((1 / y) * (y * x)) = x.
x ^ ((y / x) \ (y V z)) = x.
(1 / x) ^ (y / (x * y)) = 1 / x.
(x / y) ^ ((x V z) / y) = x / y.
x ^ (y V (z \ (z * x))) = x.
1 ^ (x \ (x * (y \ y))) = 1.
x ^ ((y / y) * x) = x.
x = (x / x) * x.
(x / x) * x = x.
x ^ ((x * (y \ y)) / 1) = x.
x ^ (x * (y \ y)) = x.
x = x * (x \ x).
x * (x \ x) = x.
(x \ x) ^ ((y * x) \ (y * x)) = x \ x.
x ^ (y \ (y * (z V x))) = x.
x ^ ((x * (y V z)) / z) = x.
x ^ (x * (y V 1)) = x.
x V (x / (y V 1)) = x.
x V (x / (y / y)) = x.
x ^ (x / (y / y)) = x / (y / y).
x ^ ((((x * y) * z) / z) / y) = x.
x ^ (((x * (y * z)) / z) / y) = x.
x ^ (((x * y) / y) / (y / y)) = x.
(x / x) ^ ((x / x) / (x / x)) = x / x.
((x ^ y) / x) \ (x ^ y) = x.
(1 ^ x) \ (1 ^ x) = 1.
((1 / x) * x) \ (1 ^ ((1 / x) * x)) = 1.
x ^ ((y * (1 / x)) \ y) = x.
(x \ (y \ z)) ^ ((y * x) \ z) = x \ (y \ z).
1 ^ ((x * (1 / y)) \ (x / y)) = 1.
(x / y) V ((x * (1 / y)) * 1) = x / y.
((x \ 1) * y) V (x \ y) = x \ y.
x ^ ((y \ 1) \ (y \ x)) = x.
(x \ 1) ^ ((x \ y) / y) = x \ 1.
(x \ y) V ((x V z) \ y) = x \ y.
x / x = (x / x) / (x / x).
(x / x) / (x / x) = x / x.
(x / x) \ (x / x) = x / x.
((1 / x) * x) \ ((1 / x) * x) = 1.
(x \ x) ^ 1 = x \ x.
1 V (x \ x) = 1.
1 = x \ x.
x \ x = 1.
(x \ x) \ y = y.
x ^ ((x \ 1) \ 1) = x.
(x \ 1) ^ (1 / x) = x \ 1.
1 V ((x V y) \ x) = x \ x.
1 = x / x.
x / x = 1.
(x / (x V y)) ^ 1 = x / (x V y).
1 V ((x \ 1) * x) = 1.
(1 / x) ^ (x \ 1) = x \ 1.
1 V ((x ^ (y \ 1)) * y) = 1.
1 V ((x V y) \ x) = 1.
1 V ((x V y) \ (y ^ z)) = 1.
x ^ ((y ^ (x \ 1)) \ 1) = x.
(1 / x) ^ (x \ 1) = 1 / x.
1 / x = x \ 1.
x \ 1 = 1 / x.
x V ((y / (y V z)) * x) = x.
x V (((y ^ z) / y) * x) = x.
1 V ((x ^ y) / x) = 1.
1 V (1 \ (((x ^ y) / x) ^ z)) = 1.
1 V (((x ^ y) / x) ^ z) = 1.
1 V (x ^ ((y ^ z) / y)) = 1.
1 V (x ^ (((y / z) * z) / y)) = 1.
1 V ((x / (y * x)) * y) = 1.
(1 / x) ^ (y / (x * y)) = y / (x * y).
(x / y) V (x * (1 / y)) = x / y.
(x / y) V (x * (y \ 1)) = x / y.
(x \ 1) ^ (y \ (y / x)) = x \ 1.
x / (y * x) = 1 / y.
x \ 1 = y / (x * y).
x / (y * x) = y \ 1.
((x * y) \ 1) ^ (y \ (x \ 1)) = (x * y) \ 1.
(x * y) \ 1 = (y \ (x \ 1)) ^ ((x * y) \ 1).
(x \ (y \ 1)) ^ ((y * x) \ 1) = (y * x) \ 1.
(x * y) \ 1 = y \ (x \ 1).
((x * (x \ 1)) \ 1) \ y = y.
1 = 1 @ (x * (x \ 1)).
1 @ (x * (x \ 1)) = 1.
(c24 * (c24 \ 1)) @ 1 != c24 * (c24 \ 1) # answer("Goal 8") # label("Goal 8").
x * y = x * (y * 1).
x * (y * 1) = x * y.
x @ y = x * ((x \ 1) * ((y \ 1) \ 1)).
x * ((x \ 1) * ((y \ 1) \ 1)) = x @ y.
x * (y * (z \ z)) = x * y.
x * ((x \ 1) * 1) = x @ 1.
x * (x \ 1) = x @ 1.
(x * y) @ 1 = x * (y * ((x * y) \ 1)).
x * (y * ((x * y) \ 1)) = (x * y) @ 1.
x * (y * ((z * (z \ 1)) \ 1)) = x * y.
x * (x \ 1) = (x * (x \ 1)) @ 1.
(x * (x \ 1)) @ 1 = x * (x \ 1).
1 @ (c27 \ 1) != c27 \ 1 # answer("Goal 11") # label("Goal 11").
(x V y) V (y ^ z) = x V y.
x V (y * (z * ((y * z) \ x))) = x.
x ^ (y / ((x \ y) ^ z)) = x.
(x \ y) ^ (z * ((x * z) \ y)) = z * ((x * z) \ y).
x V (x * (y * (y \ 1))) = x.
x ^ (y / (((x \ y) / z) * z)) = x.
(x \ 1) ^ ((y * x) \ y) = x \ 1.
1 V (x \ (x ^ y)) = 1.
1 V ((x \ (x ^ y)) ^ z) = 1 V (x \ (x ^ y)).
1 / (x \ 1) = 1 @ x.
x ^ ((1 / y) \ (y \ x)) = x.
(1 / x) ^ ((x \ y) / y) = 1 / x.
x ^ (((x \ y) / y) \ 1) = x.
(((x \ y) / y) * x) V 1 = 1.
(1 / x) ^ ((x \ y) / y) = (x \ y) / y.
(x \ y) / y = 1 / x.
x \ 1 = (x \ y) / y.
(x \ y) / y = x \ 1.
1 V ((x \ (x ^ y)) ^ z) = 1.
1 V (x * ((y * x) \ (y ^ z))) = 1.
1 V (x * ((y * x) \ y)) = 1.
(x \ 1) ^ ((y * x) \ y) = (y * x) \ y.
(x * y) \ x = y \ 1.
(x \ 1) / y = (y * x) \ 1.
(x * y) \ 1 = (y \ 1) / x.
(x \ 1) / y = x \ (y \ 1).
x \ (y \ 1) = (x \ 1) / y.
x \ ((x \ 1) \ 1) = 1.
1 / ((x \ 1) \ 1) = x \ 1.
x \ 1 = 1 @ (x \ 1).
1 @ (x \ 1) = x \ 1.
c5 @ (c6 @ c7) != c5 @ c7 # answer("Goal 3") # label("Goal 3").
x * ((x \ 1) * (1 @ y)) = x @ y.
(x @ 1) * y = x * ((x \ 1) * y).
x * ((x \ 1) * y) = (x @ 1) * y.
(x @ 1) * (1 @ y) = x @ y.
(x * (x \ 1)) \ 1 = 1.
(x @ 1) \ 1 = 1.
((x @ 1) * y) \ 1 = y \ 1.
x \ (1 @ x) = 1.
1 / (1 @ x) = x \ 1.
(1 @ x) \ 1 = x \ 1.
((x @ 1) * (1 @ y)) \ 1 = y \ 1.
(x @ y) \ 1 = y \ 1.
(x \ 1) \ 1 = 1 @ (y @ x).
x * ((x \ 1) * (1 @ (y @ z))) = x @ z.
x @ y = x @ (z @ y).
x @ (y @ z) = x @ z.
x V y = x / ((x V y) \ x).
x / ((x V y) \ x) = x V y.
(c26 \ 1) @ 1 != 1 # answer("Goal 10") # label("Goal 10").
x / ((x V y) \ x) = y V x.
(x ^ y) / (x \ (x ^ y)) = (x ^ y) V x.
(x / (x V y)) \ x = y V x.
x V (((x / y) ^ z) * y) = x.
x ^ ((y ^ (z / x)) \ z) = x.
1 ^ ((x V y) \ (x V (y V z))) = 1.
1 ^ ((x ^ y) \ x) = 1.
1 V ((x ^ y) \ x) = (x ^ y) \ x.
1 ^ ((x V y) / x) = 1.
1 ^ (x / (x ^ y)) = 1.
x / ((y V x) \ x) = y V x.
(x / (y V x)) \ x = y V x.
x ^ (((y / x) ^ z) \ y) = x.
((x / y) \ x) V y = (x / y) \ x.
x ^ ((y ^ 1) \ x) = x.
x V ((y ^ 1) \ x) = (y ^ 1) \ x.
x ^ ((y * (y \ (z / x))) \ z) = x.
(((1 V x) \ y) / y) \ ((1 V x) \ y) = y V ((1 V x) \ y).
x ^ ((1 V y) * x) = x.
x ^ (x / (y V 1)) = x / (y V 1).
(x / (y V 1)) / (x \ (x / (y V 1))) = x V (x / (y V 1)).
1 ^ ((x V 1) \ (x V ((y ^ z) \ y))) = 1.
x ^ ((y / (x V z)) \ y) = x.
x V ((x / (y V z)) * y) = x.
(x / y) ^ (x / (y V z)) = x / (y V z).
(x ^ y) / (x \ (x ^ y)) = x.
(x ^ y) / (y \ (y ^ x)) = y.
(x ^ y) / (y \ (x ^ y)) = y.
x / ((x * (y V 1)) \ (x ^ (x * (y V 1)))) = x * (y V 1).
((x ^ y) / y) \ (y ^ x) = y.
((x ^ y) / y) \ (x ^ y) = y.
(x / ((1 V y) * x)) \ (x ^ ((1 V y) * x)) = (1 V y) * x.
1 ^ ((x \ y) / ((x V z) \ y)) = 1.
1 ^ ((x V 1) \ ((x ^ 1) \ x)) = 1.
(x V 1) ^ (((x ^ 1) \ x) / 1) = x V 1.
1 ^ (x / (x V y)) = x / (x V y).
(x \ (x / y)) ^ (1 / y) = 1 / y.
(x V 1) ^ ((x ^ 1) \ x) = x V 1.
(x ^ 1) ^ (x / (x V 1)) = x ^ 1.
x ^ 1 = x ^ (1 ^ (x / (x V 1))).
x ^ (1 ^ (x / (x V 1))) = x ^ 1.
x ^ (x / (x V 1)) = x ^ 1.
x ^ 1 = x / (x V 1).
x / (x V 1) = x ^ 1.
x / (1 V x) = x ^ 1.
(x \ y) V (z * ((x * z) \ y)) = x \ y.
(x \ (y \ z)) ^ ((y * x) \ z) = (y * x) \ z.
x ^ ((y \ (y / x)) \ 1) = x.
(x \ (x / y)) ^ (1 / y) = x \ (x / y).
x \ (x / y) = 1 / y.
x \ 1 = y \ (y / x).
x \ (x / y) = y \ 1.
x \ (x ^ 1) = (x V 1) \ 1.
(x V 1) \ 1 = x \ (x ^ 1).
(x * y) \ z = y \ (x \ z).
(((1 V x) \ y) / y) \ ((1 V x) \ y) = y.
((1 V x) \ 1) \ ((1 V x) \ y) = y.
(x / (y V 1)) / (x \ (x / (y V 1))) = x.
(x / (1 V y)) / (x \ (x / (y V 1))) = x.
(x / (1 V y)) / ((y V 1) \ 1) = x.
x / ((x * (y V 1)) \ x) = x * (y V 1).
x / ((y V 1) \ 1) = x * (y V 1).
1 ^ ((x \ 1) * (x V 1)) = 1.
(x / (1 V y)) * (y V 1) = x.
1 ^ ((x \ 1) * (1 V x)) = 1.
(x ^ 1) * (x V 1) = x.
x * y = (x ^ 1) * ((x V 1) * y).
(x ^ 1) * ((x V 1) * y) = x * y.
1 = ((x \ 1) * (1 V x)) ^ 1.
((x \ 1) * (1 V x)) ^ 1 = 1.
(x / ((1 V y) * x)) \ x = (1 V y) * x.
((1 V x) \ 1) \ y = (1 V x) * y.
(1 V x) * ((1 V x) \ y) = y.
(1 V x) * ((x V 1) \ y) = y.
(x V 1) * ((x V 1) \ y) = y.
(x V 1) * (x \ (x ^ 1)) = 1.
(x ^ 1) * 1 = x * (x \ (x ^ 1)).
x * (x \ (x ^ 1)) = (x ^ 1) * 1.
x * (x \ (x ^ 1)) = x ^ 1.
((x \ 1) * (1 V x)) * (((x \ 1) * (1 V x)) \ 1) = ((x \ 1) * (1 V x)) ^ 1.
((x \ 1) * (1 V x)) * ((1 V x) \ ((x \ 1) \ 1)) = ((x \ 1) * (1 V x)) ^ 1.
((x \ 1) * (1 V x)) ^ 1 = (x \ 1) * ((1 V x) * ((1 V x) \ ((x \ 1) \ 1))).
(x \ 1) * ((1 V x) * ((1 V x) \ ((x \ 1) \ 1))) = ((x \ 1) * (1 V x)) ^ 1.
(x \ 1) * ((x \ 1) \ 1) = ((x \ 1) * (1 V x)) ^ 1.
(x \ 1) * ((x \ 1) \ 1) = 1.
1 = (x \ 1) @ 1.
(x \ 1) @ 1 = 1.
c1 @ c1 != c1 # answer("Goal 1") # label("Goal 1").
x * 1 = x @ x.
x @ x = x * 1.
x @ x = x # label("Goal 1").
(c2 @ c3) @ c4 != c2 @ c4 # answer("Goal 2") # label("Goal 2").
(x @ y) * z = (x @ 1) * ((1 @ y) * z).
(x @ 1) * ((1 @ y) * z) = (x @ y) * z.
((x \ 1) \ 1) \ 1 = x \ 1.
(x @ y) * (y \ 1) = (x @ y) @ 1.
((x \ 1) \ 1) * (x \ 1) = 1.
(1 @ x) * (x \ 1) = 1.
x * ((1 @ y) * (y \ 1)) = x.
x @ 1 = (x @ y) * (y \ 1).
(x @ y) * (y \ 1) = x @ 1.
x @ 1 = (x @ y) @ 1.
(x @ y) @ 1 = x @ 1.
(x @ 1) * (1 @ y) = (x @ z) @ y.
(x @ y) @ z = (x @ 1) * (1 @ z).
(x @ y) @ z = x @ z # label("Goal 2").
(c16 \ c17) @ (c18 \ c19) != (c16 @ c18) \ (c17 @ c19) # answer("Goal 6").
(c16 @ c18) \ (c17 @ c19) != (c16 \ c17) @ (c18 \ c19) # answer("Goal 6").
x / ((y V x) \ x) = x V y.
x V y = (z ^ y) V (x V y).
(x ^ y) V (z V y) = z V y.
(x \ (x V y)) V 1 = x \ (x V y).
1 ^ (x \ (y \ (z V (y * x)))) = 1.
x V (y / (x \ y)) = y / (x \ y).
x V (y * (z * (u ^ ((y * z) \ x)))) = x.
1 ^ (x \ ((y / x) \ y)) = 1.
((x * (x \ y)) / (y V (x * (x \ y)))) \ (x * (x \ y)) = y.
1 V (x \ ((y / x) \ y)) = x \ ((y / x) \ y).
x V (y * ((z V y) \ x)) = x.
x V ((y V 1) \ x) = x.
x ^ ((y V 1) \ x) = (y V 1) \ x.
x V (((y / z) * z) * (y \ x)) = x.
x V ((((x / y) / z) * z) * y) = x.
x ^ ((y V 1) * x) = x.
x V ((y V 1) * x) = (y V 1) * x.
x ^ ((x * y) / (z * (z \ y))) = x.
1 ^ (((x V y) \ z) \ (x \ z)) = 1.
x V ((y / z) * (z * (y \ x))) = x.
x V (((x / y) / z) * (z * y)) = x.
1 / (((x ^ y) \ y) \ (1 ^ ((x ^ y) \ y))) = (x ^ y) \ y.
(1 @ x) V (y @ x) = 1 @ x.
(x @ y) ^ (1 @ y) = x @ y.
x ^ (y / (z * (u ^ ((x * z) \ y)))) = x.
x ^ (((y ^ (z / (u * x))) * u) \ z) = x.
1 ^ ((x V y) \ x) = (x V y) \ x.
x ^ (1 @ x) = x.
(1 @ x) V x = 1 @ x.
x V (y V (1 @ x)) = y V (1 @ x).
x ^ (1 @ (y V x)) = x.
1 ^ (1 @ (x \ (x V y))) = 1.
1 ^ (1 @ ((x ^ y) \ y)) = 1.
(1 / x) \ 1 = 1 @ x.
x V (x * (y * (1 / y))) = x.
1 @ (x V 1) = x V 1.
1 @ x = 1 / (1 / x).
1 / (1 / x) = 1 @ x.
(1 / x) ^ ((y * x) \ y) = 1 / x.
x V (((y V z) \ y) * x) = x.
1 V ((x ^ y) / y) = 1.
1 ^ ((x * y) \ (x / (1 / y))) = 1.
x ^ ((x / (1 / y)) / (y * 1)) = x.
x ^ ((x / (1 / y)) / y) = x.
x ^ ((x / (1 @ y)) / (y \ 1)) = x.
x V ((x / (1 @ y)) / (y \ 1)) = (x / (1 @ y)) / (y \ 1).
(x \ y) ^ ((z * x) \ (z * y)) = x \ y.
x ^ ((x / y) / (y \ 1)) = x.
1 V ((x \ 1) / (y \ (y / x))) = 1.
x / ((y \ 1) * x) = 1 @ y.
(x @ y) ^ (z / ((y \ 1) * z)) = x @ y.
((x \ 1) * y) ^ ((z @ x) \ y) = (x \ 1) * y.
((x \ y) / y) \ 1 = 1 @ x.
(x \ (y \ 1)) \ 1 = 1 @ (y * x).
((x \ 1) * y) \ 1 = y \ (1 @ x).
x * (y * (y \ (x \ 1))) = (x * y) @ 1.
(x \ (1 @ y)) \ 1 = 1 @ ((y \ 1) * x).
((x \ 1) * y) * (y \ (1 @ x)) = ((x \ 1) * y) @ 1.
((x \ 1) / y) \ 1 = 1 @ (y * x).
(x \ 1) / (y \ 1) = x \ (1 @ y).
(x \ 1) \ (y \ 1) = (1 @ x) / y.
1 V (x \ ((y \ (y / x)) \ 1)) = 1.
1 ^ (((x V y) \ (1 @ x)) \ 1) = 1.
1 @ (1 / x) = x \ 1.
(x @ 1) * (y \ 1) = x @ (y \ 1).
1 @ ((x * y) \ x) = y \ 1.
x \ 1 = 1 / (y @ x).
1 / (x @ y) = y \ 1.
(x \ (y \ 1)) \ 1 = 1 @ ((z @ y) * x).
(x @ y) * (z * (z \ (y \ 1))) = ((x @ y) * z) @ 1.
(x @ y) \ (z \ 1) = (y \ 1) / z.
1 @ (x @ y) = 1 @ y.
(x * y) \ 1 = (z @ y) \ (x \ 1).
(x @ y) \ (z \ 1) = (z * y) \ 1.
x \ (y \ 1) = (z @ x) \ (y \ 1).
(x @ y) \ (z \ 1) = y \ (z \ 1).
(x @ 1) \ (y \ 1) = y \ 1.
(x @ y) \ (1 @ z) = ((z \ 1) * y) \ 1.
x * ((y @ 1) * (x \ 1)) = (x * (y @ 1)) @ 1.
x \ (x / (y \ 1)) = 1 @ y.
1 @ (x \ (x / y)) = y \ 1.
(x \ 1) / (y / x) = y \ 1.
(x \ y) \ (x \ 1) = y \ 1.
(x \ (y \ 1)) \ (x \ 1) = 1 @ y.
(x \ 1) / (y \ 1) = (y \ x) \ 1.
x \ ((y / x) \ 1) = y \ 1.
(x \ 1) \ (y \ 1) = (y / x) \ 1.
x \ (1 @ y) = (y \ x) \ 1.
(x \ y) \ 1 = y \ (1 @ x).
x \ (1 @ (x * y)) = (y \ 1) \ 1.
(x \ (1 @ y)) \ 1 = 1 @ (y \ x).
((x V 1) \ y) \ 1 = y \ (x V 1).
(x \ 1) \ (1 @ y) = 1 @ (x * y).
(x \ 1) \ (y \ 1) = 1 @ (x / y).
(x / y) \ 1 = (1 @ y) / x.
(1 @ x) / y = 1 / (y / x).
(1 @ x) / (y \ x) = 1 @ y.
x \ ((1 @ x) / y) = y \ 1.
(x \ 1) / (y \ (x \ 1)) = 1 @ y.
x \ (1 @ (x * y)) = 1 @ y.
1 @ (x \ y) = 1 @ ((x \ 1) * y).
1 @ ((x \ 1) * y) = 1 @ (x \ y).
1 ^ ((1 @ x) \ (x V 1)) = 1.
(x V 1) V ((1 @ x) * 1) = x V 1.
1 @ (x / y) = (1 @ x) / y.
(1 @ x) / y = 1 @ (x / y).
1 @ (x / y) = (y / x) \ 1.
(x / y) \ 1 = 1 @ (y / x).
1 @ (x / y) = 1 / (y / x).
1 / (x / y) = 1 @ (y / x).
1 @ (x / (y \ x)) = 1 @ y.
x \ (1 @ (x / y)) = y \ 1.
((x / y) \ z) / z = 1 @ (y / x).
1 / (1 / x) = 1 @ ((x * y) / y).
1 @ ((x * y) / y) = 1 / (1 / x).
(x \ 1) \ 1 = 1 @ ((y / x) \ y).
1 @ ((x / y) \ x) = (y \ 1) \ 1.
(x \ 1) / (y \ 1) = 1 @ (x \ y).
(x \ 1) \ (1 @ (x \ y)) = 1 @ y.
(x V 1) V (1 @ x) = x V 1.
x V 1 = x V (1 V (1 @ x)).
x V (1 V (1 @ x)) = x V 1.
x V 1 = 1 V (1 @ x).
1 V (1 @ x) = x V 1.
1 V (1 @ x) = (y @ x) V 1.
(x @ y) V 1 = 1 V (1 @ y).
(x @ y) V 1 = y V 1.
x V 1 = 1 V (y @ x).
1 V (x @ y) = y V 1.
1 V (x @ y) = 1 V y.
(x V y) / y = 1 @ ((x V y) / y).
1 @ ((x V y) / y) = (x V y) / y.
1 @ ((x * y) / y) = 1 @ x.
1 @ ((x / y) \ x) = 1 @ y.
1 @ (x \ y) = x \ (1 @ y).
x \ (1 @ y) = 1 @ (x \ y).
1 @ (x \ y) = (y \ x) \ 1.
(x \ y) \ 1 = 1 @ (y \ x).
(1 @ x) / (1 @ ((y V (1 @ x)) \ x)) = (1 @ x) V y.
x \ (1 @ y) = 1 @ (x \ (z @ y)).
1 @ (x \ (y @ z)) = x \ (1 @ z).
1 @ (x \ (x * y)) = 1 @ y.
1 @ (x \ y) = 1 / (y \ x).
1 / (x \ y) = 1 @ (y \ x).
1 V (x \ (1 @ ((y / x) \ y))) = 1.
1 @ x = 1 @ (y * (y \ x)).
1 @ (x * (x \ y)) = 1 @ y.
1 @ (x \ (y @ z)) = 1 @ (x \ z).
1 V (1 @ (x \ ((y / x) \ y))) = 1.
1 = 1 V (x \ ((y / x) \ y)).
1 V (x \ ((y / x) \ y)) = 1.
1 = x \ ((y / x) \ y).
x \ ((y / x) \ y) = 1.
1 @ ((x @ y) * z) = 1 @ (y * z).
(x @ y) \ (1 @ (y * z)) = 1 @ z.
x @ (1 @ y) = x @ (z / (y \ z)).
x @ (y / (z \ y)) = x @ (1 @ z).
x @ (1 @ (y \ z)) = x @ ((y \ 1) * z).
x @ ((y \ 1) * z) = x @ (1 @ (y \ z)).
x @ (1 @ y) = x @ ((y * z) / z).
x @ ((y * z) / z) = x @ (1 @ y).
x @ (1 @ y) = x @ ((z / y) \ z).
x @ ((y / z) \ y) = x @ (1 @ z).
x @ (1 @ y) = x @ (z \ (z * y)).
x @ (y \ (y * z)) = x @ (1 @ z).
x @ (1 @ y) = x @ (z * (z \ y)).
x @ (y * (y \ z)) = x @ (1 @ z).
x @ (1 @ (y \ z)) = x @ (y \ (u @ z)).
x @ (y \ (z @ u)) = x @ (1 @ (y \ u)).
x @ (1 @ (y * z)) = x @ ((u @ y) * z).
x @ (y / (z \ y)) = x @ z.
x @ ((y * z) / z) = x @ y.
x @ ((y / z) \ y) = x @ z.
x @ (y \ (y * z)) = x @ z.
x @ (y * (y \ z)) = x @ z.
x @ (y * (1 / z)) = x @ (y / z).
x @ (y * (z \ 1)) = x @ (y / z).
x @ (y * (z * (1 / u))) = x @ ((y * z) / u).
x @ (y * (z \ 1)) = x @ (y / (u @ z)).
x @ (y / (z @ u)) = x @ (y * (u \ 1)).
x @ (y * (1 @ (z \ u))) = x @ (y / (u \ z)).
(x @ y) \ (1 @ z) = y \ (1 @ z).
x \ (1 @ y) = 1 @ ((z @ x) \ y).
1 @ ((x @ y) \ z) = y \ (1 @ z).
1 @ ((x @ y) \ z) = 1 @ (y \ z).
(x \ (y @ z)) \ 1 = 1 @ (z \ x).
x @ ((y \ 1) * z) = x @ (y \ z).
x @ ((1 / y) * z) = x @ (y \ z).
x @ ((y \ 1) * z) = x @ ((u @ y) \ z).
x @ ((y @ z) \ u) = x @ ((z \ 1) * u).
x @ (((y / z) \ 1) * y) = x @ z.
x @ ((1 @ (y / z)) * z) = x @ y.
x @ ((1 @ y) * z) = x @ (y * z).
x @ ((y / z) * z) = x @ y.
x @ (y \ (z @ u)) = x @ (y \ u).
x @ ((y @ z) * u) = x @ (z * u).
x @ (y / (z @ u)) = x @ (y / u).
(1 @ x) / (y @ z) = 1 @ (x / z).
(1 @ x) / (y @ (z \ x)) = 1 @ z.
x @ ((y @ z) \ u) = x @ (z \ u).
(x @ 1) \ y = (x \ 1) \ (x \ y).
(x \ 1) \ (x \ y) = (x @ 1) \ y.
(x @ y) \ z = (1 @ y) \ ((x @ 1) \ z).
(1 @ x) \ ((y @ 1) \ z) = (y @ x) \ z.
x * (y @ (x \ 1)) = (x * (y @ 1)) @ 1.
(x * (y @ 1)) @ 1 = x * (y @ (x \ 1)).
(x * (y @ 1)) @ 1 = x * (y @ (1 / x)).
(x * (y @ (1 / x))) * (1 @ z) = (x * (y @ 1)) @ z.
x @ (y * (1 @ (y \ z))) = x @ z.
x @ (y * (1 @ z)) = x @ (y * z).
x @ (y * (1 @ z)) = x @ (y * (u @ z)).
x @ (y * (z @ u)) = x @ (y * u).
((x \ 1) * x) * 1 = ((x \ 1) * x) @ 1.
((x \ 1) * x) @ 1 = (x \ 1) * x.
(1 @ x) V y = 1 @ (y V (1 @ x)).
1 @ (x V (1 @ y)) = (1 @ y) V x.
1 @ (x \ (x * (1 @ y))) = (1 @ y) V (x \ (x * (1 @ y))).
(1 @ x) V (y \ (y * (1 @ x))) = 1 @ (y \ (y * (1 @ x))).
(x * (y @ 1)) @ z = x * ((y @ (1 / x)) * (1 @ z)).
x * ((y @ (1 / x)) * (1 @ z)) = (x * (y @ 1)) @ z.
((x * (x \ y)) / y) \ (x * (x \ y)) = y.
x / (y * (y \ x)) = 1 @ (x / (y * (y \ x))).
1 @ (x / (y * (y \ x))) = x / (y * (y \ x)).
1 / (((x ^ y) \ y) \ 1) = (x ^ y) \ y.
(x ^ y) \ y = 1 @ ((x ^ y) \ y).
1 @ ((x ^ y) \ y) = (x ^ y) \ y.
1 @ (x \ (x * (1 @ y))) = x \ (x * (1 @ y)).
x \ (x * (1 @ y)) = 1 @ (1 @ y).
x \ (x * (1 @ y)) = 1 @ y.
(x @ 1) \ (x @ y) = 1 @ y.
(1 @ x) \ (1 @ y) = (z @ x) \ (z @ y).
(x @ y) \ (x @ (y * z)) = 1 @ z.
(x @ y) \ (x @ z) = 1 @ (y \ z).
(x \ 1) * (1 @ x) = 1.
x @ (y * (y \ x)) = x.
(x \ 1) * y = ((x \ 1) * y) @ (x \ y).
((x \ 1) * y) @ (x \ y) = (x \ 1) * y.
(x @ y) * z = ((x @ y) * z) @ (y * z).
((x @ y) * z) @ (y * z) = (x @ y) * z.
x / (y @ z) = (x / (y @ z)) @ (x / z).
(x / (y @ z)) @ (x / z) = x / (y @ z).
(x @ y) \ z = ((x @ y) \ z) @ (y \ z).
((x @ y) \ z) @ (y \ z) = (x @ y) \ z.
x \ (x @ (x * y)) = 1 @ y.
x \ (x @ y) = 1 @ (x \ y).
(x @ y) \ x = 1 @ (y \ x).
x V (((x / (1 @ y)) / (y \ 1)) * 1) = x.
((1 @ x) \ y) ^ (1 \ ((x \ 1) * y)) = (1 @ x) \ y.
x @ (y * z) = x @ (y * (u * (u \ z))).
x @ (y * (z * (z \ u))) = x @ (y * u).
x \ (x @ y) = 1 @ (x \ (z @ y)).
1 ^ ((x @ (y ^ x)) \ x) = 1.
(x \ (y @ z)) \ 1 = (x @ z) \ x.
x \ (x @ y) = (y @ x) \ y.
(x @ y) \ x = y \ (y @ x).
1 ^ ((x @ (x ^ y)) \ x) = 1.
(x @ 1) \ y = (z \ 1) \ ((x @ z) \ y).
(x \ 1) \ ((y @ x) \ z) = (y @ 1) \ z.
x V ((x @ (x ^ y)) * 1) = x.
x V (x @ (x ^ y)) = x.
x V (x @ ((y V 1) \ x)) = x.
1 @ (x / (x @ ((y V 1) \ x))) = (x V (x @ ((y V 1) \ x))) / (x @ ((y V 1) \ x)).
(x V (x @ ((y V 1) \ x))) / (x @ ((y V 1) \ x)) = 1 @ (x / (x @ ((y V 1) \ x))).
(x \ (x @ y)) * ((x \ (z @ y)) \ 1) = 1 @ 1.
(x @ y) \ (z @ u) = ((x @ y) \ (z @ u)) @ (y \ u).
((x @ y) \ (z @ u)) @ (y \ u) = (x @ y) \ (z @ u).
x V ((x / (1 @ y)) / (y \ 1)) = x.
x = (x / (1 @ y)) / (y \ 1).
(x / (1 @ y)) / (y \ 1) = x.
x @ (y * (z * (1 / u))) = x @ (y * (z / u)).
(x \ (x @ y)) * ((x @ y) \ x) = 1 @ 1.
(x \ (x @ y)) * ((x @ y) \ x) = 1.
x V (((x @ y) / (x \ (x @ y))) * 1) = x.
x V ((x @ y) / (x \ (x @ y))) = x.
x = (x @ y) / (x \ (x @ y)).
(x @ y) / (x \ (x @ y)) = x.
(x @ (x * y)) / (1 @ y) = x.
x @ (y * (z / u)) = x @ ((y * z) / u).
x @ ((y * z) / u) = x @ (y * (z / u)).
((1 @ x) \ y) ^ ((x \ 1) * y) = (1 @ x) \ y.
(1 @ x) \ y = ((x \ 1) * y) ^ ((1 @ x) \ y).
((x \ 1) * y) ^ ((1 @ x) \ y) = (1 @ x) \ y.
(1 @ x) \ y = (x \ 1) * y.
(x V 1) \ y = ((x V 1) \ 1) * y.
((x V 1) \ 1) * y = (x V 1) \ y.
(x \ 1) \ y = ((x \ 1) \ 1) * y.
((x \ 1) \ 1) * y = (x \ 1) \ y.
(1 @ (x / y)) \ z = (1 @ (y / x)) * z.
(x \ 1) * (1 @ (x * y)) = 1 @ y.
(x \ (x @ y)) \ z = ((x \ (u @ y)) \ 1) * z # label(flip_matches_hint).
((x V 1) \ y) * z = ((x V 1) \ 1) * (y * z).
((x V 1) \ 1) * (y * z) = ((x V 1) \ y) * z.
(1 @ x) * y = (x \ 1) \ y.
(x \ 1) \ y = (1 @ x) * y.
((x \ 1) * y) \ z = y \ ((1 @ x) * z).
(1 @ x) * (x \ y) = (x @ 1) \ y.
(1 @ x) * ((y @ x) \ z) = (y @ 1) \ z.
x * (1 @ y) = x @ (x * y).
x @ (x * y) = x * (1 @ y).
x * (1 @ (x \ y)) = x @ y.
(x * (1 @ y)) @ z = x @ z.
(x * (1 @ y)) / (1 @ y) = x.
(x * y) * (y \ 1) = (x * y) @ x.
(x * y) @ x = (x * y) * (y \ 1).
x * (y \ 1) = x @ (x / y).
x @ (x / y) = x * (y \ 1).
(x ^ y) * ((x ^ y) \ y) = (x ^ y) @ y.
x * ((y @ x) \ y) = x @ y.
x / (y \ 1) = x * (1 @ y).
(x @ y) * z = x * (((y @ x) \ y) * z).
x * (((y @ x) \ y) * z) = (x @ y) * z.
(x @ y) * ((z @ (x @ y)) \ z) = x @ z.
x ^ ((x / y) * (1 @ y)) = x.
(x / (y \ 1)) @ z = x @ z.
x ^ ((x / y) * (1 @ ((z / y) \ z))) = x.
(x / (1 @ y)) @ z = x @ z.
x @ (x / y) = x / (1 @ y).
x / (1 @ y) = x @ (x / y).
x / (1 @ y) = x * (y \ 1).
(x * y) @ x = x * (y * (y \ 1)).
(x * y) @ x = x * (y @ 1).
(x @ y) * (z @ 1) = ((x @ y) * z) @ y.
((x @ y) * z) @ y = (x @ y) * (z @ 1).
(x * (y @ 1)) @ z = (x * y) @ z.
(x / (y * (y \ x))) \ z = (1 @ ((y * (y \ x)) / x)) * z.
(1 @ ((x * (x \ y)) / y)) * z = (y / (x * (x \ y))) \ z.
(x @ y) * (z * (((u @ z) \ u) * ((z @ u) \ (y \ 1)))) = ((x @ y) * (z @ u)) @ 1.
(x @ y) * ((z @ y) \ z) = x @ z.
(x @ y) * (1 @ (y \ z)) = x @ z.
(x @ y) * (y \ (y @ z)) = x @ z.
(x @ y) * (1 @ z) = x @ (y * z).
(x @ y) \ z = (u \ (u @ y)) \ ((x @ u) \ z).
(x \ (x @ y)) \ ((z @ x) \ u) = (z @ y) \ u.
x * (y @ ((1 / x) * z)) = (x * (y @ 1)) @ z.
x ^ ((x / y) @ x) = x.
x ^ ((x V y) @ x) = x.
x ^ (((y V 1) * x) @ x) = x.
(x \ (x @ y)) \ z = ((x @ y) \ x) * z.
((x V 1) \ y) * z = (x V 1) \ (y * z).
(x V 1) \ (y * z) = ((x V 1) \ y) * z.
(x @ y) \ z = ((u @ y) \ u) * ((x @ u) \ z).
((x @ y) \ x) * ((z @ x) \ u) = (z @ y) \ u.
x * (y @ (x \ z)) = (x * (y @ 1)) @ z.
(x * (y @ 1)) @ z = x * (y @ (x \ z)).
x * (y @ (x \ z)) = (x * y) @ z.
(1 @ (x * ((x \ y) / y))) * z = (y / (x * (x \ y))) \ z.
(1 @ (x * (x \ 1))) * y = (z / (x * (x \ z))) \ y.
(x / (y * (y \ x))) \ z = (1 @ (y * (y \ 1))) * z.
(x / (y * (y \ x))) \ z = 1 * z.
(x / (y * (y \ x))) \ z = z.
x / (y * (y \ x)) = 1.
x / ((y ^ x) @ x) = 1.
(x V y) / (y @ (x V y)) = 1.
x / ((((y V z) \ y) * x) @ (x V (((y V z) \ y) * x))) = 1.
x / ((((y V z) \ y) * x) @ x) = 1.
x / (x @ ((y V 1) \ x)) = 1 @ (x / (x @ ((y V 1) \ x))).
1 @ (x / (x @ ((y V 1) \ x))) = x / (x @ ((y V 1) \ x)).
x / (x @ ((y V 1) \ x)) = 1 @ (x * (((y V 1) \ x) \ 1)).
x / (x @ ((y V 1) \ x)) = 1 @ (x * (x \ (y V 1))).
x / (x @ ((y V 1) \ x)) = 1 @ (y V 1).
x / (x @ ((y V 1) \ x)) = y V 1.
x ^ ((y V 1) * (x @ ((y V 1) \ x))) = (x / (x @ ((y V 1) \ x))) * (x @ ((y V 1) \ x)).
(x / (x @ ((y V 1) \ x))) * (x @ ((y V 1) \ x)) = x ^ ((y V 1) * (x @ ((y V 1) \ x))).
(x @ y) * (z * ((z @ z) \ (y \ 1))) = ((x @ y) * (z @ u)) @ 1.
((x @ y) * (z @ u)) @ 1 = (x @ y) * (z * ((z @ z) \ (y \ 1))).
((x @ y) * (z @ u)) @ 1 = (x @ y) * (z * (z \ (y \ 1))).
((x @ y) * (z @ u)) @ 1 = ((x @ y) * z) @ 1.
(x * (y @ z)) @ 1 = ((x @ x) * y) @ 1.
((x @ x) * y) @ 1 = (x * (y @ z)) @ 1.
(x * y) @ 1 = (x * (y @ z)) @ 1.
(x * (y @ z)) @ 1 = (x * y) @ 1.
((x * y) @ 1) @ z = (x * (y @ u)) @ z.
(x * (y @ z)) @ u = (x * y) @ u.
(x / (x @ ((y V 1) \ x))) * (x @ ((y V 1) \ x)) = x ^ (((y V 1) * x) @ x).
(x V 1) * (y @ ((x V 1) \ y)) = y ^ (((x V 1) * y) @ y).
x ^ (((y V 1) * x) @ x) = (y V 1) * (x @ ((y V 1) \ x)).
x ^ (((y V 1) * x) @ x) = ((y V 1) * x) @ x.
((x V 1) * y) @ y = y.
x @ y = ((z V 1) * x) @ y.
((x V 1) * y) @ z = y @ z.
x @ y = ((z V 1) \ x) @ y.
((x V 1) \ y) @ z = y @ z.
(((x V 1) \ y) * z) @ u = (y * z) @ u.
x / ((y * x) @ x) = 1.
x V (1 * ((y * x) @ x)) = x.
((x * y) @ y) \ (1 \ y) = 1.
x V ((y * x) @ x) = x.
x V ((y @ x) * (x @ 1)) = x.
((x * y) @ y) \ y = 1.
(1 @ ((x * y) @ y)) * 1 = (((x * y) @ y) @ 1) \ y.
(((x * y) @ y) @ 1) \ y = (1 @ ((x * y) @ y)) * 1.
(((x * y) @ y) @ 1) \ y = (1 @ y) * 1.
(((x * y) @ y) @ 1) \ y = 1 @ y.
((x * y) @ 1) \ y = 1 @ y.
((x \ 1) * x) \ x = 1 @ x.
1 @ x = x \ ((1 @ x) * x).
x \ ((1 @ x) * x) = 1 @ x.
x V (((1 @ x) * x) / (1 @ x)) = ((1 @ x) * x) / (x \ ((1 @ x) * x)).
((1 @ x) * x) / (x \ ((1 @ x) * x)) = x V (((1 @ x) * x) / (1 @ x)).
((1 @ x) * x) / (x \ ((1 @ x) * x)) = x V (((1 @ x) * x) * (x \ 1)).
((1 @ x) * x) / (x \ ((1 @ x) * x)) = x V ((1 @ x) * (x * (x \ 1))).
((1 @ x) * x) / (x \ ((1 @ x) * x)) = x V ((1 @ x) * (x @ 1)).
((1 @ x) * x) / (x \ ((1 @ x) * x)) = x.
((1 @ x) * x) / (1 @ x) = x.
x = ((1 @ x) * x) * (x \ 1).
((1 @ x) * x) * (x \ 1) = x.
x = (1 @ x) * (x * (x \ 1)).
(1 @ x) * (x * (x \ 1)) = x.
(1 @ x) * (x @ 1) = x.
(1 @ x) * ((y @ x) @ 1) = y @ x.
(1 @ x) * (y @ 1) = y @ x.
((1 @ x) * (y @ 1)) @ z = y @ z.
x @ y = ((1 @ z) * x) @ y.
((1 @ x) * y) @ z = y @ z.
((x \ 1) * y) @ z = y @ z.
x @ (y * x) = (1 @ y) * x.
((x @ 1) \ y) @ z = (x \ y) @ z.
((x @ 1) \ y) @ z = ((x @ u) \ y) @ z.
x @ (y \ x) = (y \ 1) * x.
(1 @ (x / y)) * y = y @ x.
((x @ y) \ z) @ u = (x \ z) @ u.
(x \ (y @ z)) @ (u \ z) = (x @ u) \ (y @ z).
(((x \ 1) * y) \ z) @ u = (y \ z) @ u.
(x \ ((1 @ y) * z)) @ u = (x \ z) @ u.
(x \ (y @ z)) @ u = (x \ y) @ u.
(x @ y) \ (z @ u) = (x \ z) @ (y \ u) # label("Goal 6").
(c8 ^ c9) @ (c10 ^ c11) != (c8 @ c10) ^ (c9 @ c11) # answer("Goal 4") # label("Goal 4").
x ^ (y ^ z) = y ^ (z ^ x).
x ^ (y ^ z) = z ^ (x ^ y).
(x ^ y) ^ z = x ^ (z ^ y).
(x V y) V z = x V (z V y).
x ^ y = y ^ (x ^ (y V z)).
x ^ (y ^ (x V z)) = y ^ x.
1 V (x \ (x V y)) = x \ (x V y).
x ^ (x * (1 V y)) = x.
x ^ (x * (y \ (y V z))) = x.
1 / ((x \ (x V y)) \ (1 ^ (x \ (x V y)))) = x \ (x V y).
(x \ 1) * ((1 @ x) * (1 @ y)) = (x \ 1) @ y.
(1 @ x) ^ (y @ x) = y @ x.
x V (1 @ x) = 1 @ x.
x ^ y = x ^ (y ^ (1 @ x)).
x ^ (y ^ (1 @ x)) = x ^ y.
(1 @ x) V y = x V (y V (1 @ x)).
x V (y V (1 @ x)) = (1 @ x) V y.
x ^ (1 @ (x V y)) = x.
x V (1 @ (x V y)) = 1 @ (x V y).
1 V (x \ (y ^ x)) = 1.
1 = (x \ (y ^ x)) V 1.
(x \ (y ^ x)) V 1 = 1.
1 V ((x ^ (y V z)) \ (x ^ y)) = 1.
x V ((y @ 1) * x) = x.
x ^ ((y @ 1) * x) = (y @ 1) * x.
1 ^ ((x ^ y) \ (y ^ (1 @ x))) = 1.
1 V ((x ^ (((y @ 1) * x) V z)) \ ((y @ 1) * x)) = 1.
1 ^ (x \ ((x V y) ^ (1 @ x))) = 1.
1 ^ ((x ^ y) \ (x ^ (1 @ (x ^ y)))) = 1.
((x @ y) \ z) \ 1 = z \ (1 @ y).
((x @ y) \ y) \ 1 = 1.
((x @ y) \ y) * 1 = ((x @ y) \ y) @ 1.
1 V (x @ (y \ (z ^ y))) = 1.
((x @ y) \ y) @ 1 = (x @ y) \ y.
1 V (x @ (y * z)) = ((u @ y) * z) V 1.
((x @ y) * z) V 1 = 1 V (u @ (y * z)).
1 V (x @ (y \ (z ^ (u @ y)))) = 1.
1 = (x \ (y ^ (z @ x))) V 1.
(x \ (y ^ (z @ x))) V 1 = 1.
1 ^ (x \ (y ^ (z @ x))) = x \ (y ^ (z @ x)).
((x @ y) * z) V 1 = 1 V (y * z).
1 V (x * y) = 1 V ((z @ x) * y).
1 V ((x @ y) * z) = 1 V (y * z).
(x ^ y) \ (x ^ (1 @ (x ^ y))) = 1.
1 V ((x ^ (y V ((z @ 1) * x))) \ ((z @ 1) * x)) = 1.
1 @ (x V (1 @ y)) = x V (1 @ y).
1 / ((x \ (x V y)) \ 1) = x \ (x V y).
x \ (x V y) = 1 @ (x \ (x V y)).
1 @ (x \ (x V y)) = x \ (x V y).
1 * x = (y \ 1) * ((1 @ y) * x).
(x \ 1) * ((1 @ x) * y) = 1 * y.
x V ((x @ y) * (z ^ (1 @ (y \ x)))) = x.
(x V y) V ((x V y) @ x) = x V y.
x ^ (x @ (x ^ y)) = x @ (x ^ y).
(x \ 1) * ((1 @ x) * y) = y.
1 @ x = (y \ 1) @ x.
(x \ 1) @ y = 1 @ y.
(1 @ x) @ y = 1 @ y.
(x V (1 @ y)) @ z = 1 @ z.
x V y = x V (y V ((x V y) @ x)).
x V (y V ((x V y) @ x)) = x V y.
(x @ (x ^ y)) \ (x ^ (1 @ (x ^ (x @ (x ^ y))))) = 1.
x V ((1 @ y) V (1 @ x)) = x V (1 @ y).
1 V ((x \ 1) * y) = 1 V (x \ y).
1 V ((1 / x) * y) = 1 V (x \ y).
x V (1 @ y) = (1 @ y) V (1 @ x).
(1 @ x) V (1 @ y) = y V (1 @ x).
x V (1 @ y) = (1 @ x) V (1 @ y).
(1 @ x) V (1 @ y) = x V (1 @ y).
x V (1 @ y) = y V (1 @ x).
(x V y) V (1 @ x) = 1 @ (x V y).
x V (1 @ y) = (z @ y) V (1 @ x).
(x @ y) V (1 @ z) = z V (1 @ y).
1 @ (x V y) = x V (y V (1 @ x)).
x V (y V (1 @ x)) = 1 @ (x V y).
1 @ (x V y) = y V (1 @ x).
1 @ (x V y) = x V (1 @ y).
x @ (y V (1 @ z)) = x @ (z V y).
x @ (y V (1 @ z)) = x @ (y V z).
x @ (y V (1 @ z)) = x @ (y V (u @ z)).
x @ (y V (z @ u)) = x @ (u V y).
x @ (y V (z @ u)) = x @ (y V u).
x @ ((y @ z) V u) = x @ (z V u).
(x V (y @ z)) @ (x V z) = x V (y @ z).
x * (x \ (x V y)) = x @ (x V y).
(x V y) V (x @ (x V y)) = x V y.
x ^ (x @ (x V y)) = x.
x V (x @ (x V y)) = x @ (x V y).
x V (y V (x @ (x V z))) = y V (x @ (x V z)).
x V y = x V (y V (x @ (x V y))).
x V (y V (x @ (x V y))) = x V y.
x V ((y ^ x) @ x) = x.
x V ((x ^ y) @ x) = x.
x V (y @ (y V x)) = y V x.
x V (y @ ((y @ z) V x)) = (y @ z) V x.
x V (y @ (x V (y @ z))) = (y @ z) V x.
x V (y @ (x V z)) = (y @ z) V x.
x V (y @ (x V z)) = x V (y @ z).
x V (x @ y) = x @ (x V y).
x @ (x V y) = x V (x @ y).
(x V (x @ y)) @ z = x @ z.
((x @ y) V ((x @ y) @ z)) @ u = x @ u.
((x @ y) V (x @ z)) @ u = x @ u.
x @ ((x @ y) V z) = (x @ y) V (x @ z).
(x @ y) V (x @ z) = x @ (y V z).
(x @ y) ^ (x @ (y V z)) = x @ y.
(x @ (y ^ z)) ^ (x @ z) = x @ (y ^ z).
x @ (y ^ z) = (x @ z) ^ (x @ (y ^ z)).
(x @ y) ^ (x @ (z ^ y)) = x @ (z ^ y).
(x @ (x ^ y)) \ (x ^ (1 @ (x @ (x ^ y)))) = 1.
(x @ (x ^ y)) \ (x ^ (1 @ (x ^ y))) = 1.
x @ (y \ x) = (1 / y) * x.
1 V (((1 / x) * y) * z) = 1 V ((x \ y) * z).
(x \ y) @ 1 = (x @ y) \ y.
(x @ y) \ y = (x \ y) @ 1.
1 V ((1 / x) * (y * z)) = 1 V ((x \ y) * z).
x \ (y @ z) = (x \ y) @ (x \ z).
(x \ y) @ (x \ z) = x \ (y @ z).
(x \ y) @ 1 = x \ (y @ x).
x \ (y @ x) = (x \ y) @ 1.
1 V ((x \ (y @ z)) * u) = 1 V ((x \ z) * u).
1 V ((x \ y) * z) = 1 V (x \ (y * z)).
1 V (x \ (y * z)) = 1 V ((x \ y) * z).
1 V (((x ^ (y V ((z @ 1) * x))) \ (z @ 1)) * x) = 1.
1 = 1 V (((x ^ (y V ((z @ 1) * x))) \ 1) * x).
1 V (((x ^ (y V ((z @ 1) * x))) \ 1) * x) = 1.
1 = 1 V ((x ^ (y V ((z @ 1) * x))) \ x).
1 V ((x ^ (y V ((z @ 1) * x))) \ x) = 1.
1 = (x ^ (y V ((z @ 1) * x))) \ x.
(x ^ (y V ((z @ 1) * x))) \ x = 1.
((x ^ (1 @ (1 \ y))) ^ y) \ (x ^ (1 @ (1 \ y))) = 1.
((x ^ (1 @ y)) ^ y) \ (x ^ (1 @ (1 \ y))) = 1.
(x ^ (y ^ (1 @ x))) \ (y ^ (1 @ (1 \ x))) = 1.
(x ^ y) \ (y ^ (1 @ (1 \ x))) = 1.
(x ^ y) \ (y ^ (1 @ x)) = 1.
x * ((y ^ z) \ (z ^ (1 @ y))) = x.
x @ (y ^ z) = x @ (z ^ (1 @ y)).
x @ (y ^ (1 @ z)) = x @ (z ^ y).
x @ (y ^ (1 @ z)) = x @ (y ^ z).
x @ (y ^ (1 @ z)) = x @ ((u @ z) ^ y).
x @ ((y @ z) ^ u) = x @ (u ^ (1 @ z)).
x @ ((y @ z) ^ u) = x @ (z ^ u).
x @ ((y @ z) ^ u) = x @ (u ^ z).
x @ (y ^ (z @ u)) = x @ (u ^ y).
x @ (y ^ (z @ u)) = x @ (y ^ u).
(x ^ (y @ z)) @ (z ^ x) = x ^ (y @ z).
(x ^ (y @ z)) @ (x ^ z) = x ^ (y @ z).
(x @ (y ^ z)) \ (y ^ (u @ z)) = (x \ (y ^ (u @ z))) @ 1.
(1 @ (x ^ y)) ^ (x ^ (z @ y)) = (x ^ (z @ y)) @ (x ^ y).
x ^ ((y @ z) ^ (1 @ (x ^ z))) = (x ^ (y @ z)) @ (x ^ z).
x ^ (1 @ (x ^ y)) = (x ^ (1 @ y)) @ (x ^ y).
(x ^ (1 @ y)) @ (x ^ y) = x ^ (1 @ (x ^ y)).
x ^ (1 @ (x ^ y)) = x ^ (1 @ y).
(x @ (x ^ y)) \ (x ^ (1 @ y)) = 1.
1 = (x \ (x ^ (1 @ y))) @ 1.
(x \ (x ^ (1 @ y))) @ 1 = 1.
x \ ((x ^ (1 @ y)) @ x) = 1.
((x ^ (1 @ y)) @ x) V (x * 1) = (x ^ (1 @ y)) @ x.
((x ^ (1 @ y)) @ x) V x = (x ^ (1 @ y)) @ x.
(x ^ (1 @ y)) @ x = x V ((x ^ (1 @ y)) @ x).
x V ((x ^ (1 @ y)) @ x) = (x ^ (1 @ y)) @ x.
(x ^ (1 @ y)) @ x = x.
x @ y = (x ^ (1 @ z)) @ y.
(x ^ (1 @ y)) @ z = x @ z.
x @ (y ^ x) = x ^ (1 @ y).
x ^ (1 @ y) = x @ (y ^ x).
(x @ y) ^ (1 @ z) = x @ (z ^ (x @ y)).
(x @ y) ^ (1 @ z) = x @ (y ^ z).
(x @ y) ^ (1 @ z) = x @ (z ^ y).
x ^ (y @ (z ^ x)) = x ^ (y @ z).
x ^ ((y @ x) ^ (1 @ z)) = x ^ (y @ z).
(x ^ (y @ x)) ^ (1 @ z) = x ^ (y @ z).
(x ^ (y @ z)) @ u = (x ^ (y @ x)) @ u.
(x ^ y) @ z = (x ^ (y @ x)) @ z.
(x ^ (y @ x)) @ z = (x ^ y) @ z.
(x ^ (y @ x)) @ (x ^ z) = x ^ (y @ z).
x ^ (y @ z) = (x ^ y) @ (x ^ z).
(x ^ y) @ (x ^ z) = x ^ (y @ z).
(x ^ (y @ z)) @ u = (x ^ y) @ u.
(x ^ (y @ z)) @ u = (y ^ x) @ u.
((x @ y) ^ z) @ u = (x ^ z) @ u.
((x @ y) ^ z) @ ((u @ w) ^ v5) = (x ^ z) @ (w ^ v5).
(x ^ y) @ (z ^ u) = (x @ z) ^ (y @ u) # label("Goal 4").
(c12 V c13) @ (c14 V c15) != (c12 @ c14) V (c13 @ c15) # answer("Goal 5") # label("Goal 5").
(x V y) V z = y V (x V z).
x V (y V z) = y V (x V z).
x ^ ((1 ^ y) \ x) = x.
1 V (x @ 1) = 1.
1 ^ (x @ 1) = x @ 1.
x ^ ((y @ 1) \ x) = x.
x V (y @ x) = x V (y @ (x ^ z)).
x V (y @ (x ^ z)) = x V (y @ x).
x V (y V (y @ x)) = y V x.
x V y = x V (y V (x @ y)).
x V (y V (x @ y)) = x V y.
x V ((y @ z) V (x @ z)) = x V (y @ z).
(x \ y) @ (z \ y) = (x @ z) \ y.
(x \ y) @ y = (x @ 1) \ y.
(x @ 1) \ y = (x \ y) @ y.
x ^ ((y \ x) @ x) = x.
(x @ y) ^ ((z \ (x @ y)) @ y) = x @ y.
(x @ y) ^ ((z \ x) @ y) = x @ y.
(x @ y) ^ ((x V z) @ y) = x @ y.
(x @ y) ^ ((z V x) @ y) = x @ y.
(x @ y) V ((x V z) @ y) = (x V z) @ y.
(x @ y) V ((z V x) @ y) = (z V x) @ y.
(x V y) V ((x V y) @ z) = (x V y) V (x @ z).
(x @ y) V ((z V (x @ u)) @ y) = (z V (x @ u)) @ y.
(x V y) V (x @ z) = x V (y V ((x V y) @ z)).
x V (y V ((x V y) @ z)) = (x V y) V (x @ z).
((x V y) V (x @ z)) @ u = (x V y) @ u.
(x V (y V (x @ z))) @ u = (x V y) @ u.
(x V ((y @ (x ^ z)) V (x @ u))) @ w = (x V (y @ x)) @ w.
x V (y V ((x V y) @ z)) = x V (y V (x @ z)).
(x V (y @ z)) V ((x V (y @ z)) @ u) = (x V (y @ z)) V (y @ u).
(x V (y @ z)) V (y @ u) = x V ((y @ z) V ((x V (y @ z)) @ u)).
x V ((y @ z) V ((x V (y @ z)) @ u)) = (x V (y @ z)) V (y @ u).
(x V (y @ z)) V (y @ u) = x V ((y @ z) V (x @ u)).
x V ((y @ z) V (x @ u)) = x V ((y @ z) V (y @ u)).
x V ((y @ z) V (y @ u)) = x V ((y @ z) V (x @ u)).
x V (y @ (z V u)) = x V ((y @ z) V (x @ u)).
x V ((y @ z) V (x @ u)) = x V (y @ (z V u)).
(x V (y @ ((x ^ z) V u))) @ w = (x V (y @ x)) @ w.
(x V (y @ z)) @ u = (x V (y @ x)) @ u.
(x V (y @ z)) @ u = (x V (y @ w)) @ u.
(x V (y @ z)) @ (x V u) = x V (y @ u).
(x V y) @ z = (y V (x @ u)) @ z.
(x V (y @ z)) @ u = (y V x) @ u.
((x @ y) V z) @ u = (x V z) @ u.
(x V y) @ (x V z) = x V (y @ z).
(x @ y) V (z @ u) = ((x @ y) V z) @ (y V u).
((x @ y) V z) @ (y V u) = (x @ y) V (z @ u).
(x @ y) V (z @ u) = (x V z) @ (y V u).
(x V y) @ (z V u) = (x @ z) V (y @ u).
(c34 V c35) @ ((c34 / c35) \ c34) != (c34 / c35) \ c34 # answer("Goal 15").
1 ^ (x \ (y V x)) = 1.
1 ^ ((x * (x \ y)) \ y) = 1.
x V ((y / x) \ y) = (y / x) \ y.
1 V ((x * (x \ y)) \ y) = (x * (x \ y)) \ y.
(x * y) ^ ((z V (x * (y * u))) / u) = x * y.
x V (y / (z ^ (x \ y))) = y / (z ^ (x \ y)).
x ^ (y / (z * (z \ (x \ y)))) = x.
x V (y * (((y \ x) / z) * z)) = x.
x V (((y ^ x) / z) * z) = x.
x ^ (((y ^ z) / x) \ z) = x.
(x \ y) V ((x \ 1) * y) = x \ y.
x ^ ((y / x) \ (1 @ y)) = x.
x ^ ((y \ 1) \ (1 @ (y \ x))) = x.
x / ((y / (z ^ (x \ y))) \ x) = x V (y / (z ^ (x \ y))).
(x * y) \ x = 1 / y.
1 / (x @ y) = 1 / y.
x \ (1 / y) = 1 / (y * x).
x \ (1 / y) = 1 / ((z @ y) * x).
1 / ((x @ y) * z) = z \ (1 / y).
1 / ((x @ y) * z) = 1 / (y * z).
x ^ (1 @ (y * (y \ x))) = x.
1 / ((x @ (y \ z)) * u) = u \ (1 @ (z \ y)).
x @ (y / (1 / z)) = x @ (y * z).
x @ (y * (y \ (z * (1 / u)))) = x @ (z / u).
1 = 1 V (x \ (y ^ (z @ x))).
1 V (x \ (y ^ (z @ x))) = 1.
1 V ((x * (x \ y)) \ y) = 1.
1 = (x * (x \ y)) \ y.
(x * (x \ y)) \ y = 1.
x ^ ((y \ (z / x)) \ (y \ z)) = x.
1 / ((x @ (y \ z)) * u) = 1 @ (u \ (z \ y)).
x @ (y * (z \ u)) = x @ (y / (u \ z)).
x @ (y / (z \ u)) = x @ (y * (u \ z)).
1 @ (x \ (y \ z)) = 1 / ((z \ y) * x).
1 / ((x \ y) * z) = 1 @ (z \ (y \ x)).
x @ (y / (1 / ((z \ u) * w))) = x @ (y / (w \ (u \ z))).
x / ((y / (z ^ (x \ y))) \ x) = y / (z ^ (x \ y)).
(x \ (y / z)) / (((x \ y) / z) \ (x \ (y / z))) = (x \ y) / (z ^ ((x \ (y / z)) \ (x \ y))).
x @ (y / (z \ (u \ w))) = x @ (y * ((w \ u) * z)).
x @ (y / ((z * u) \ w)) = x @ (y * ((w \ z) * u)).
x @ (y * ((z \ u) * w)) = x @ (y * (z \ (u * w))).
x @ (y * (z \ (u * w))) = x @ (y * ((z \ u) * w)).
x @ (y * ((y \ z) * (1 / u))) = x @ (z / u).
x @ (y @ x) = x.
(x / y) \ x = ((x / y) \ x) @ y.
((x / y) \ x) @ y = (x / y) \ x.
x \ (x @ (x V y)) = x \ (x V y).
x V (((y / x) \ y) @ x) = (y / x) \ y.
((1 @ x) * y) / y = 1 @ x.
x @ (y * ((y \ z) / u)) = x @ (z / u).
(x * ((x \ y) / z)) @ (y / z) = x * ((x \ y) / z).
(1 @ x) \ ((1 @ x) * y) = y.
x @ (x V (y @ z)) = x V (x @ z).
x \ (x V (x @ y)) = x \ (x V y).
x * (x \ (x V y)) = x V (x @ y).
x \ (x V (x @ y)) = x \ (x V (z @ y)).
x \ (x V (y @ z)) = x \ (x V (x @ z)).
(x V (x @ y)) \ (x V y) = 1.
x \ (x V (y @ z)) = x \ (x V z).
(x V y) \ (x V (y V (z @ u))) = (x V y) \ ((x V y) V u).
((x * ((x \ y) / z)) V (x * ((x \ y) / z))) \ ((x * ((x \ y) / z)) V (y / z)) = 1.
(x V y) \ (x V (y V (z @ u))) = (x V y) \ (x V (y V u)).
(x V y) \ (x V ((z / y) \ z)) = (x V y) \ (x V (y V y)).
(x V y) \ (x V (y V y)) = (x V y) \ (x V ((z / y) \ z)).
(x V y) \ (x V y) = (x V y) \ (x V ((z / y) \ z)).
(x V y) \ (x V ((z / y) \ z)) = (x V y) \ (x V y).
(x V y) \ (x V ((z / y) \ z)) = 1.
(x * ((x \ y) / z)) \ ((x * ((x \ y) / z)) V (y / z)) = 1.
(x * ((x \ y) / z)) \ ((y / z) V (x * ((x \ y) / z))) = 1.
1 = ((x \ y) / z) \ (x \ ((y / z) V (x * ((x \ y) / z)))).
((x \ y) / z) \ (x \ ((y / z) V (x * ((x \ y) / z)))) = 1.
(1 @ x) \ x = x @ 1.
(x \ y) V (y @ (x \ y)) = x \ y.
x / (x @ (y \ x)) = 1 @ y.
(x @ y) / x = 1 @ (y / x).
x / (x @ y) = 1 @ (x / y).
((x @ y) / x) \ (y / x) = (y / x) @ 1.
(x @ y) V ((1 @ (x / y)) \ x) = (x / (x @ y)) \ x.
(x @ y) / x = y / (y @ x).
(x @ (y / z)) \ y = (x \ y) @ z.
(x @ y) V ((1 \ x) @ y) = (x / (x @ y)) \ x.
(x @ y) V (x @ y) = (x / (x @ y)) \ x.
(x / (x @ y)) \ x = x @ y.
((x @ y) / x) \ y = y @ x.
x @ (x ^ y) = x ^ (1 @ y).
x ^ (1 @ y) = x @ (x ^ y).
x ^ (y @ (x ^ z)) = x ^ (y @ z).
x ^ (x @ y) = x @ (x ^ y).
x @ (x ^ y) = x ^ (x @ y).
x ^ (1 @ y) = x ^ (x @ y).
x ^ (y ^ (y @ x)) = x ^ y.
x ^ ((x @ y) ^ y) = y ^ x.
x ^ (y ^ (x @ y)) = y ^ x.
x ^ (y ^ (x @ y)) = x ^ y.
(x ^ y) ^ (x @ y) = x ^ y.
(x ^ y) V (x @ y) = x @ y.
(x ^ y) V (y @ x) = y @ x.
(x * y) V (((z V (x * (y * u))) / u) @ (x * y)) = ((z V (x * (y * u))) / u) @ (x * y).
(x V y) @ z = (x V (y @ x)) @ z.
(x V (y @ x)) @ z = (x V y) @ z.
(x V y) @ (x V x) = x V (y @ x).
(x V y) @ x = x V (y @ x).
(x V y) @ y = y V (x @ y).
(x V (y \ x)) @ (y \ x) = y \ x.
(x \ y) @ z = (y V (x \ y)) @ z.
(x V (y \ x)) @ z = (y \ x) @ z.
(x V y) @ (z V x) = x V (y @ z).
x V ((y \ x) @ z) = (y \ x) @ (x V z).
(x \ y) @ (y V z) = y V ((x \ y) @ z).
(x V y) \ (x V ((z \ x) @ y)) = ((x V y) \ (z \ x)) @ 1.
(x @ y) V (z @ x) = x V (z @ y).
x V (y @ z) = (y @ x) V (x @ z).
(x @ y) V (y @ z) = y V (x @ z).
(x V y) \ (x V ((x / y) \ x)) = ((x V y) \ ((x / y) \ x)) @ 1.
((x V y) \ ((x / y) \ x)) @ 1 = 1.
((x V y) @ ((x / y) \ x)) \ ((x / y) \ x) = 1.
((x V y) @ y) \ ((x / y) \ x) = 1.
(x V (y @ x)) \ ((y / x) \ y) = 1.
(x / y) ^ (x / ((y V (x @ y)) * 1)) = x / y.
(x / y) ^ (x / (y V (x @ y))) = x / y.
x / y = x / (y V (x @ y)).
x / (y V (x @ y)) = x / y.
x / ((y @ z) V (x @ z)) = x / (y @ z).
x / (x V (y @ x)) = x / (y @ x).
(x / (y @ x)) \ x = x V (y @ x).
((x @ y) / (y @ (x @ y))) \ (x @ y) = y V (x @ (x @ y)).
((x @ y) / y) \ (x @ y) = y V (x @ (x @ y)).
(x * ((x \ y) / z)) V ((y / z) @ (x * ((x \ y) / z))) = ((y V (x * (((x \ y) / z) * z))) / z) @ (x * ((x \ y) / z)).
((x V (y * (((y \ x) / z) * z))) / z) @ (y * ((y \ x) / z)) = (y * ((y \ x) / z)) V ((x / z) @ (y * ((y \ x) / z))).
(x \ (y / z)) / (((x \ y) / z) \ (x \ (y / z))) = (x \ y) / z.
((x V (y * (((y \ x) / z) * z))) / z) @ (y * ((y \ x) / z)) = (y * ((y \ x) / z)) V ((x / z) @ (x / z)).
((x V (y * (((y \ x) / z) * z))) / z) @ (y * ((y \ x) / z)) = (y * ((y \ x) / z)) V (x / z).
((x V (y * (((y \ x) / z) * z))) / z) @ (y * ((y \ x) / z)) = (x / z) V (y * ((y \ x) / z)).
(x / y) @ (z * ((z \ x) / y)) = (x / y) V (z * ((z \ x) / y)).
(x / y) V (z * ((z \ x) / y)) = (x / y) @ (x / y).
(x / y) V (z * ((z \ x) / y)) = x / y.
((x \ y) / z) \ (x \ (y / z)) = 1.
(x \ (y / z)) / 1 = (x \ y) / z.
(x \ y) / z = x \ (y / z).
x \ (y / z) = (x \ y) / z.
(((x @ y) / x) \ y) / x = (y / x) @ 1.
(x @ y) / y = (x / y) @ 1.
x V (((y / x) @ 1) \ (y @ x)) = ((y @ x) / x) \ (y @ x).
x V (((y / x) \ y) @ (1 \ x)) = ((y @ x) / x) \ (y @ x).
x V (((y / x) \ y) @ x) = ((y @ x) / x) \ (y @ x).
((x @ y) / y) \ (x @ y) = y V (((x / y) \ x) @ y).
((x @ y) / y) \ (x @ y) = (x / y) \ x.
(x / y) \ x = y V (x @ (x @ y)).
x V (y @ (y @ x)) = (y / x) \ y.
x V (y @ x) = (y / x) \ y.
(x V y) @ y = (x / y) \ x.
(x / y) \ x = (x V y) @ y.
(x V y) @ ((z / y) \ z) = (x / y) \ x.
(x / y) \ x = (x V y) @ ((z / y) \ z).
((c30 / c31) \ c30) @ (c30 V c31) != c30 V c31 # answer("Goal 13").
(x @ y) @ x = x.
((x / y) \ x) @ (x V y) = x V y # label("Goal 13").
(c32 V c33) @ (c32 / (c33 \ c32)) != c32 / (c33 \ c32) # answer("Goal 14").
x V y = y V (x V (y ^ z)).
x V (y V (x ^ z)) = y V x.
(x * (x \ y)) / ((y V (x * (x \ y))) \ (x * (x \ y))) = y.
x = (1 @ x) ^ x.
(1 @ x) ^ x = x.
x ^ (1 @ ((y / x) \ y)) = x.
(x @ y) \ (1 @ y) = 1.
1 @ ((x @ y) \ y) = 1.
1 ^ ((x @ y) \ y) = (x @ y) \ y.
(x * (x \ y)) / (y \ (x * (x \ y))) = y.
(x \ (x / y)) @ 1 = 1.
(x \ (y V x)) @ 1 = 1.
((x V (y ^ z)) \ (x V y)) @ 1 = 1.
x ^ ((y @ (y / x)) \ y) = x.
(x @ (x / y)) ^ (x / y) = x @ (x / y).
1 ^ ((x @ (x / y)) \ (x / y)) = 1.
((x V (y ^ z)) \ (x V z)) @ 1 = 1.
1 = (x @ (x / y)) \ (x / y).
(x @ (x / y)) \ (x / y) = 1.
((x V (y @ (y / z))) \ (x V (y / z))) @ 1 = 1.
(1 @ (x / y)) * 1 = (x @ 1) \ (x / y).
(x @ 1) \ (x / y) = (1 @ (x / y)) * 1.
(x @ 1) \ (x / y) = 1 @ (x / y).
((x @ 1) * (1 @ (x / y))) / ((x / y) \ ((x @ 1) * ((x @ 1) \ (x / y)))) = x / y.
(x @ (x / y)) / ((x / y) \ ((x @ 1) * ((x @ 1) \ (x / y)))) = x / y.
(x @ (x / y)) / ((x / y) \ ((x @ 1) * (1 @ (x / y)))) = x / y.
(x @ (x / y)) / ((x / y) \ (x @ (x / y))) = x / y.
(x @ (x / y)) / (((x / y) \ x) @ 1) = x / y.
(((x V y) @ z) \ u) @ w = ((y V (x @ v5)) \ u) @ w.
((x V (y @ z)) \ u) @ w = (((y V x) @ v5) \ u) @ w.
(x V y) @ z = (x @ z) V (y @ z).
(x @ y) V (z @ y) = (x V z) @ y.
(x @ y) / (((x V z) @ y) \ (x @ y)) = (x @ y) V (z @ y).
((x V (y @ z)) \ u) @ w = ((y V x) \ u) @ w.
((x V y) \ (y V (x / z))) @ 1 = 1.
((x V y) \ (x / (y \ x))) @ 1 = 1.
((x V y) @ (x / (y \ x))) \ (x / (y \ x)) = 1.
((x V y) @ y) \ (x / (y \ x)) = 1.
(x V (y @ x)) \ (y / (x \ y)) = 1.
(x \ y) ^ (((x V (y @ x)) * 1) \ y) = x \ y.
(x \ y) ^ ((x V (y @ x)) \ y) = x \ y.
x \ y = (x V (y @ x)) \ y.
(x V (y @ x)) \ y = x \ y.
(x \ y) @ z = ((y V x) \ y) @ z.
((x V y) \ x) @ z = (y \ x) @ z.
(x @ y) / (((x V z) \ x) @ (y \ y)) = (x @ y) V (z @ y).
(x @ y) / (((x V z) \ x) @ (y \ y)) = (x V z) @ y.
(x @ y) / (((x V z) \ x) @ 1) = (x V z) @ y.
(x @ y) / ((z \ x) @ 1) = (x V z) @ y.
x / ((y V x) @ z) = x / (y @ z).
(x @ y) / ((x V z) @ u) = (x @ y) / (z @ u).
((x / y) \ x) @ z = (x V y) @ z.
(x @ (x / y)) / ((x V y) @ 1) = x / y.
x / y = (x @ (x / y)) / (y @ 1).
(x @ (x / y)) / (y @ 1) = x / y.
x / (y \ x) = (x V y) @ (x / (y \ x)).
(x V y) @ (x / (y \ x)) = x / (y \ x).
(c28 / (c29 \ c28)) @ (c28 V c29) != c28 V c29 # answer("Goal 12") # label("Goal 12").
(x / y) V (x @ (x / y)) = x / y.
(x / y) @ z = ((x / y) V x) @ z.
((x / y) V x) @ z = (x / y) @ z.
(x V (x / y)) @ z = (x / y) @ z.
(x @ y) / (((x / z) \ x) @ 1) = (x / z) @ y.
(x @ y) / ((x V z) @ 1) = (x / z) @ y.
(x / y) @ z = (x @ z) / (y @ 1).
(x @ y) / (z @ 1) = (x / z) @ y.
(x / (y \ x)) @ z = (x V y) @ z.
(x / (y \ x)) @ (x V y) = x V y # label("Goal 12").
(c20 / c21) @ (c22 / c23) != (c20 @ c22) / (c21 @ c23) # answer("Goal 7").
(c20 @ c22) / (c21 @ c23) != (c20 / c21) @ (c22 / c23) # answer("Goal 7").
(1 / x) / y = 1 / (y * x).
(1 @ x) / y = 1 @ ((z @ x) / y).
1 @ ((x @ y) / z) = (1 @ y) / z.
x @ ((1 @ y) / z) = x @ (y / z).
x @ ((1 @ y) / z) = x @ ((u @ y) / z).
x @ ((y @ z) / u) = x @ (z / u).
x @ (y / z) = x @ ((u * (u \ y)) / z).
x @ ((y * (y \ z)) / u) = x @ (z / u).
x @ ((y * (1 / z)) / u) = x @ ((y / z) / u).
(x @ y) / z = ((x @ y) / z) @ (y / z).
((x @ y) / z) @ (y / z) = (x @ y) / z.
(x @ y) / (z @ u) = ((x @ y) / (z @ u)) @ (y / u).
((x @ y) / (z @ u)) @ (y / u) = (x @ y) / (z @ u).
x @ (y * ((1 / z) / u)) = x @ ((y / z) / u).
x @ (y * (1 / (z * u))) = x @ ((y / u) / z).
x @ ((y / z) / u) = x @ (y / (u * z)).
(((x / y) / ((x / y) @ z)) \ x) / y = (x / y) @ z.
((1 @ ((x / y) / z)) \ x) / y = (x / y) @ z.
((1 @ (x / (y * z))) \ x) / z = (x / z) @ y.
((1 \ x) @ (y * z)) / z = (x / z) @ y.
(x @ (y * z)) / z = (x / z) @ y.
(x @ y) / z = (x / z) @ (y / z).
(x / y) @ (z / y) = (x @ z) / y.
((x @ y) / z) @ u = (x / z) @ u.
(x / y) @ z = (x / (y @ 1)) @ z.
(x / (y @ 1)) @ z = (x / y) @ z.
(x / (y @ 1)) @ z = (x / (y @ u)) @ z.
(x / (y @ z)) @ u = (x / y) @ u.
((x @ y) / z) @ (y / u) = (x @ y) / (z @ u).
(x @ y) / (z @ u) = (x / z) @ (y / u) # label("Goal 7").

end_of_list.
