% Length of proof is 189.
% Level of proof is 38.
% Maximum clause weight is
79.
% Given clauses 233.
1 (x * y) / y = x # label(non_clause) # label(goal). [goal].
2 (x / y) * y = x. [assumption].
3 x * (x \ y) = y. [assumption].
4 x * ((y * z) * x) = (x *
y) * (z * x). [assumption].
5 (x * y) * (z * x) = x *
((y * z) * x). [copy(4),flip(a)].
6 (c1 * c2) / c2 !=
c1. [deny(1)].
7 (x / y) * ((y * z) * (x
/ y)) = x * (z * (x / y)). [para(2(a,1),5(a,1,1)),flip(a)].
8 x * ((y * (z / x)) * x)
= (x * y) * z. [para(2(a,1),5(a,1,2)),flip(a)].
9 x * (((x \ y) * z) * x)
= y * (z * x). [para(3(a,1),5(a,1,1)),flip(a)].
10 (x \ y) * ((z * x) * (x
\ y)) = ((x \ y) * z) * y. [para(3(a,1),5(a,1,2)),flip(a)].
14 (x / y) * (z * (x / y))
= x * ((y \ z) * (x / y)). [para(3(a,1),7(a,1,2,1))].
22 (x * (y / (z / x))) * z
= x * (y * x). [para(2(a,1),8(a,1,2,1)),flip(a)].
23 x * ((((y * (z / x)) *
x) * u) * x) = ((x * y) * z) * (u * x).
[para(8(a,1),5(a,1,1)),flip(a)].
24 ((x * (y / z)) * z) *
((u * z) * ((x * (y / z)) * z)) = (((x * (y / z)) * z) * u) * ((z * x) *
y). [para(8(a,1),5(a,1,2)),flip(a)].
26 x * (((y \ x) \ z) * y)
= y * (z * y). [para(3(a,1),9(a,1,2,1)),flip(a)].
27 x * (((((x \ y) * z) *
x) * u) * x) = (y * (z * x)) * (u * x).
[para(9(a,1),5(a,1,1)),flip(a)].
29 x * (((y * (z / (u \
x))) * (u \ x)) * u) = u * ((((u \ x) * y) * z) * u). [para(8(a,1),9(a,1,2,1)),flip(a)].
30 x * (((((y \ x) \ z) *
u) * (y \ x)) * y) = y * ((z * (u * (y \ x))) * y). [para(9(a,1),9(a,1,2,1)),flip(a)].
35 x * ((x \ y) * (z * (x
\ y))) = y * ((z / (x / (x \ y))) * x).
[para(22(a,1),9(a,1,2))].
36 x * (((((y \ x) \ z) *
y) * u) * x) = (y * (z * y)) * (u * x).
[para(26(a,1),5(a,1,1)),flip(a)].
38 x * ((y * ((x \ (x *
y)) \ z)) * x) = x * (z * x). [para(26(a,1),5(a,1)),flip(a)].
40 ((x \ y) * (z / x)) * y
= (x \ y) * (z * (x \ y)). [para(2(a,1),10(a,1,2,1)),flip(a)].
46 x * ((((x \ y) * z) *
y) * x) = y * (((z * x) * (x \ y)) * x).
[para(10(a,1),9(a,1,2,1))].
51 x * ((y \ (z / (x /
y))) * (x / y)) = (x / y) * z. [para(2(a,1),14(a,1,2)),flip(a)].
124 x * ((x \ x) * (y * (x
\ x))) = x * y. [para(40(a,1),8(a,1,2)),rewrite([3(7)])].
135 x * (y / (x \ x)) = x
* ((x \ x) * y). [para(2(a,1),124(a,1,2,2)),flip(a)].
136 x * ((x \ x) * x) = x
* x. [para(3(a,1),124(a,1,2,2))].
139 x * (((x \ x) * y) *
z) = x * (y * (z / (x \ x))). [para(8(a,1),124(a,1,2))].
142 x * (((x \ x) \ y) *
z) = x * (y * (z * (x \ x))). [para(9(a,1),124(a,1,2)),flip(a)].
145 x * (((x \ x) \ (x \
x)) \ y) = x * y. [para(26(a,1),124(a,1,2)),rewrite([124(5)]),flip(a)].
147 x * (y * (x / (x \
x))) = x * (y * x). [para(10(a,1),124(a,1,2)),rewrite([139(4)])].
150 x * (y * (((x \ x) \
((x \ x) * y)) \ z)) = x * z. [para(38(a,1),124(a,1,2)),rewrite([124(5)]),flip(a)].
153 x * ((((x \ x) * x) *
y) * x) = x * ((x * y) * x). [para(136(a,1),5(a,1,1)),rewrite([5(3)]),flip(a)].
161 x * ((x \ x) \ (x \
x)) = x * ((x \ x) * (x \ x)). [para(136(a,1),124(a,1,2)),flip(a)].
164 (x \ x) * ((x * ((x \
x) * y)) * (x \ x)) = ((x \ x) * x) * y.
[para(135(a,1),8(a,1,2,1))].
219 x * (((((x \ x) \ (x \
x)) \ y) * z) * x) = x * ((y * z) * x).
[para(145(a,1),5(a,1,1)),rewrite([5(3)]),flip(a)].
227 x * ((y / (x / (x \
x))) * x) = x * y. [para(2(a,1),147(a,1,2)),flip(a)].
258 (x / (x \ x)) * y = x
* y. [para(51(a,1),147(a,1)),rewrite([142(10),3(8),227(8)])].
300 x * ((y * (z / (x / (x
\ x)))) * x) = (x * y) * z. [para(258(a,1),8(a,1)),rewrite([147(8),258(9)])].
311 x * (y / (y \ y)) = x
* y. [para(258(a,1),124(a,1,2,2)),rewrite([124(5)]),flip(a)].
333 (x / (y / (y \ y))) *
y = x. [para(311(a,1),2(a,1))].
374 x * (y * ((z * (x \
x)) / (x \ x))) = x * (y * z). [para(5(a,1),139(a,1,2)),rewrite([124(6)]),flip(a)].
422 x * (((((y \ x) \ (y \
x)) \ z) * u) * y) = x * ((z * (u * ((y \ x) \ (y \ x)))) * y). [para(142(a,1),9(a,1,2,1)),rewrite([9(9)]),flip(a)].
439 x * ((y * (z * ((x \
x) \ (x \ x)))) * x) = x * ((y * z) * x).
[back_rewrite(219),rewrite([422(7)])].
501 x * ((x * (((x \ x) *
x) \ y)) * x) = x * (y * x). [para(3(a,1),153(a,1,2,1)),flip(a)].
504 x * (((x * y) * (x \
x)) * x) = x * ((x * (y * (x \ x))) * x).
[para(5(a,1),153(a,1,2,1)),rewrite([139(7),311(6)])].
554 x * ((((x \ x) \ (x \
x)) * y) * x) = x * ((((x \ x) * (x \ x)) * y) * x). [para(161(a,1),5(a,1,1)),rewrite([5(6)]),flip(a)].
592 ((x * y) * z) * ((((y
* (z / x)) * x) \ u) * x) = x * (u * x).
[para(3(a,1),23(a,1,2,1)),flip(a)].
904 x * ((x \ x) * ((((x \
x) \ (x \ x)) * (x \ x)) \ y)) = x * y.
[para(501(a,1),124(a,1,2)),rewrite([124(5)]),flip(a)].
964 (x * (y * z)) * (((((z
\ x) * y) * z) \ u) * z) = z * (u * z). [para(3(a,1),27(a,1,2,1)),flip(a)].
1089 x * (((y / (z \ x)) /
(z / (z \ x))) * z) = z * ((z \ x) * y).
[para(2(a,1),35(a,1,2,2)),flip(a)].
1112 x * (((y * z) / (z /
(z \ x))) * z) = z * (((z \ x) * y) * x).
[para(10(a,1),35(a,1,2)),flip(a)].
1627 x * ((((x \ x) * ((x
\ y) * z)) * x) * x) = (y * (z * x)) * ((x \ x) * x). [para(46(a,2),27(a,1))].
1665 x * (((y * x) * (x \
x)) * x) = x * ((y * x) * x). [para(46(a,2),36(a,1)), rewrite([3(4),5(8)]),flip(a)].
1692 x * ((y * (z / ((x \
x) \ (x \ x)))) * ((x \ x) \ (x \ x))) = x * ((((x \ x) \ (x \ x)) * y) *
z). [para(29(a,1),124(a,1,2)),rewrite([124(10)]),flip(a)].
1693 x * ((x * (y * ((x \
x) / (x \ x)))) * x) = x * ((x * y) * x).
[para(135(a,1),29(a,1,2,1,1)),rewrite([504(7),139(5),153(12)])].
1699 x * ((((x \ x) * y) *
x) * x) = x * ((y * x) * x). [para(311(a,1),29(a,1,2,1,1)),rewrite([1665(5)]),flip(a)].
1724 (x * (y * z)) * ((z \
z) * z) = z * ((((z \ x) * y) * z) * z).
[back_rewrite(1627),rewrite([1699(7)]),flip(a)].
1729 x * ((y * (x \ x)) *
x) = x * (y * x). [para(2(a,1),1665(a,1,2,1,1)),rewrite([2(6)])].
1763 x * ((y / (x \ x)) *
x) = x * (y * x). [para(2(a,1),1729(a,1,2,1)),flip(a)].
1768 x * ((y \ y) * y) = y
* ((y \ x) * y). [para(1729(a,1),9(a,1)),flip(a)].
1779 x * (y * ((x \ x) \
(x \ x))) = x * y. [para(1729(a,1),124(a,1,2)),rewrite([124(5)]),flip(a)].
1794 ((x \ x) * x) * (x \
x) = (x \ x) * x. [para(161(a,1),1729(a,1,2,1)),rewrite([164(8),3(7)])].
1811 (x \ x) * (((y * x) *
(x \ (x \ x))) * x) = (x \ x) * (y * x).
[para(1729(a,1),46(a,1)),rewrite([9(5)]),flip(a)].
1813 x * ((((x \ x) * y) *
z) * x) = x * ((y * (z / (x \ x))) * x).
[para(1729(a,1),29(a,1)),flip(a)].
1815 x * ((((x \ x) \ (x \
x)) * y) * z) = x * (y * (z / ((x \ x) \ (x \ x)))). [back_rewrite(1692),rewrite([1779(10)]),flip(a)].
1818 x * (y * (x / ((x \
x) \ (x \ x)))) = x * (y * x). [back_rewrite(554),rewrite([1815(6),1813(12),139(12),311(11),1763(10)])].
1860 x * ((x \ (x * y)) *
x) = x * (y * x). [para(1768(a,1),5(a,1)),rewrite([1729(8)])].
1867 (x * ((y \ y) * y)) *
z = (y * ((y \ x) * y)) * z. [para(1768(a,1),8(a,2,1)),rewrite([8(6)])].
1869 x * ((y * ((y \ (x \
z)) * y)) * x) = z * (((y \ y) * y) * x).
[para(1768(a,1),9(a,1,2,1))].
1871 x * (y * ((z \ z) *
z)) = x * (z * ((z \ y) * z)). [para(1768(a,1),9(a,2,2)),rewrite([9(10)])].
1903 x * (y * (((x \ x) \
(x \ x)) * (x \ x))) = x * ((x \ x) \ y).
[para(1768(a,2),124(a,1,2))].
1940 (x \ x) * (((x \ x) \
x) * (x \ x)) = x. [para(1768(a,1),142(a,1)),rewrite([124(12),3(8)])].
1983 ((x \ x) * x) * (x *
((x \ (((x \ x) * x) * (((((x \ x) * x) \ ((x \ x) * x)) * ((x \ x) * x)) \
y))) * x)) = ((x \ x) * x) * (y * ((x \ x) * x)). [para(1768(a,1),501(a,1,2))].
2064 x * ((((x \ x) \ y) *
z) * x) = x * ((y * (z * (x \ x))) * x).
[para(30(a,1),22(a,2)),rewrite([22(9),1729(7)])].
2070 x * ((((x \ x) \ (x \
x)) \ y) * z) = x * (y * (z * ((x \ x) \ (x \ x)))). [para(30(a,1),124(a,1,2)),rewrite([124(10),1779(16)]),flip(a)].
2149 ((x \ x) * (x \ x)) *
x = (x \ x) * ((x \ x) * x). [para(1794(a,1),5(a,2,2)),rewrite([3(5)])].
2155 x * ((x \ x) * ((x \
x) * x)) = x * x. [para(1794(a,1),124(a,1,2,2)),rewrite([136(8)])].
2405 x * ((x \ x) \ ((x \
x) * y)) = x * y. [para(1860(a,1),124(a,1,2)),rewrite([124(5)]),flip(a)].
2450 x * (((y * (x \ x)) *
x) * x) = x * ((y * x) * x). [para(1729(a,1),1860(a,1,2,1,2)),rewrite([1860(5)]),flip(a)].
2454 x * ((y * ((x \ x) \
(x \ x))) * x) = x * (y * x). [para(1779(a,1),1860(a,1,2,1,2)),rewrite([1860(4)]),flip(a)].
2473 x * ((x \ x) * (x \
x)) = x. [para(1940(a,1),1860(a,1,2,1,2)),rewrite([1940(6),9(8)]),flip(a)].
2490 x * ((x \ x) \ (x \
x)) = x. [back_rewrite(161),rewrite([2473(8)])].
2643 (x \ x) * (((x \ x) \
(x \ x)) * x) = (x \ x) * x. [para(2490(a,1),124(a,1,2,2))].
2725 x * ((x \ x) \ ((x \
x) \ (x \ x))) = x. [para(2155(a,1),2405(a,1,2,2)),rewrite([2405(6),3(2),1903(10)]),flip(a)].
2905 x * ((y * ((x \ x) *
(x \ x))) * x) = x * (y * x). [para(2725(a,1),38(a,1,2,1,2,1,2)),rewrite([2064(10),2064(10),9(8)])].
3138 x * ((y / (x / ((x \
x) \ (x \ x)))) * x) = x * y. [para(2(a,1),1818(a,1,2)),flip(a)].
3149 (x / ((x \ x) \ (x \
x))) * y = x * y. [para(1818(a,1),51(a,1)),rewrite([2070(11),2490(9),3138(7)]),flip(a)].
3196 x * (y / ((y \ y) \
(y \ y))) = x * y. [para(3149(a,1),124(a,1,2,2)),rewrite([124(5)]),flip(a)].
4274 x * ((y \ y) * ((y \
y) * y)) = y * ((y \ x) * y). [para(2149(a,1),9(a,2,2)),rewrite([2905(7)]),flip(a)].
4293 ((x \ x) * x) * ((y *
(x \ x)) * ((x \ x) * x)) = x * ((x \ (((x \ x) * x) * y)) * x). [para(2149(a,1),24(a,2,2)),rewrite([311(4),1794(4),311(8),1794(8),311(12),1794(12),4274(16)])].
4376 x * (((y \ y) \ (y \
y)) * y) = y * ((y \ x) * y). [para(2454(a,1),9(a,1)),flip(a)].
4426 x * ((x \ (x \ x)) *
x) = (x \ x) * x. [back_rewrite(2643),rewrite([4376(6)])].
4623 (x \ x) * ((x \ x) *
x) = (x \ x) * x. [para(4426(a,1),1768(a,2))].
4625 x * ((x \ ((x \ x) *
x)) * x) = (x \ x) * (x * x). [para(4426(a,1),1860(a,1,2,1,2)),rewrite([9(10)])].
4677 ((x \ x) * (x \ x)) *
x = (x \ x) * x. [back_rewrite(2149),rewrite([4623(8)])].
5532 x * ((((y \ y) \ (y \
y)) * y) * z) = x * (((y \ y) * y) * z).
[para(4376(a,1),9(a,1,2,1)),rewrite([1869(6)]),flip(a)].
5589 x * (y * ((y \ ((((y
\ y) * y) \ ((y \ y) * y)) \ (((y \ y) * y) \ ((y \ y) * y)))) * y)) = ((y \ y)
* y) * ((((y \ y) * y) \ x) * ((y \ y) * y)). [para(1768(a,1),4376(a,1,2))].
5607 x * (y * (z * ((z \
((((z \ z) \ (z \ z)) * z) \ (((z \ z) \ (z \ z)) * z))) * z))) = x * (((z \ z)
* z) * (z * ((z \ ((((z \ z) \ (z \ z)) * z) \ y)) * z))). [para(4376(a,1),1871(a,1,2,2)),rewrite([4376(28),5532(28)])].
5680 ((x \ x) * x) * ((x \
x) * x) = (x \ x) * (x * x). [para(4625(a,1),1768(a,2))].
5690 (x * ((y \ y) * y)) *
(((y * ((y \ x) * y)) \ (((y * ((y \ x) * y)) \ (y * ((y \ x) * y))) * (y * ((y
\ x) * y)))) * (y * ((y \ x) * y))) = ((y * ((y \ x) * y)) \ (y * ((y \ x) * y)))
* ((y * ((y \ x) * y)) * (y * ((y \ x) * y))). [para(4625(a,1),1867(a,2))].
5997 ((x \ x) * x) * ((((x
\ x) * x) * y) * ((x \ x) * x)) = ((x \ x) * (x * x)) * (y * ((x \ x) *
x)). [para(5680(a,1),5(a,1,1)),flip(a)].
5998 (((x \ x) * x) * y) *
((x \ x) * (x * x)) = ((x \ x) * x) * (y * (x * x)). [para(5680(a,1),5(a,1,2)),rewrite([1724(15),2450(15),9(13)])].
5999 ((x \ x) * x) * x =
(x \ x) * (x * x). [para(5680(a,1),8(a,2)),rewrite([135(6),4623(5),136(4),10(5)])].
6031 (((x * ((x \ y) * x))
\ (x * ((x \ y) * x))) * (y * ((x \ x) * x))) * (((x * ((x \ y) * x)) \ (x *
((x \ y) * x))) * (x * ((x \ y) * x))) = ((x * ((x \ y) * x)) \ (x * ((x \ y) *
x))) * ((x * ((x \ y) * x)) * (x * ((x \ y) * x))). [para(1871(a,2),5680(a,1,1))].
6047 ((x \ x) * (x * x)) *
(y * ((x \ x) * x)) = ((x \ x) * x) * (x * (y * x)). [para(5999(a,1),5(a,1,1)),rewrite([5(13),1729(13)])].
6050 (x \ y) * (((x \ x) *
(x * x)) * (x \ y)) = ((x \ y) * ((x \ x) * x)) * y. [para(5999(a,1),10(a,1,2,1))].
6068 ((x \ x) * x) * (x *
((y / (((x \ x) * x) / (((x \ x) * x) \ ((x \ x) * x)))) * x)) = ((x \ x) * (x
* x)) * y. [para(5999(a,1),300(a,2,1)),rewrite([5(15),1729(15)])].
6074 x * (y * ((((x \ x) \
(x \ x)) * ((x \ x) * (x \ x))) / (x \ x))) = x * ((x \ x) \ y). [para(5999(a,1),374(a,1,2,2,1)),rewrite([1903(18)])].
6092 (((x * ((y \ y) * y))
\ (x * ((y \ y) * y))) * (x * ((y \ y) * y))) * (y * ((y \ x) * y)) = ((x * ((y
\ y) * y)) \ (x * ((y \ y) * y))) * ((x * ((y \ y) * y)) * (x * ((y \ y) *
y))). [para(5999(a,1),1871(a,1)),flip(a)].
6093 (((x * ((x \ y) * x))
\ (x * ((x \ y) * x))) * (x * ((x \ y) * x))) * (y * ((x \ x) * x)) = ((x * ((x
\ y) * x)) \ (x * ((x \ y) * x))) * ((x * ((x \ y) * x)) * (x * ((x \ y) *
x))). [para(5999(a,1),1871(a,2))].
6095 (((x * ((x \ y) * x))
\ (x * ((x \ y) * x))) * (y * ((x \ x) * x))) * (x * ((x \ y) * x)) = ((x * ((x
\ y) * x)) \ (x * ((x \ y) * x))) * ((x * ((x \ y) * x)) * (x * ((x \ y) *
x))). [para(1871(a,2),5999(a,1,1))].
6114 ((x \ x) * x) * ((((x
\ x) * x) * y) * ((x \ x) * x)) = ((x \ x) * x) * (x * (y * x)). [back_rewrite(5997),rewrite([6047(16)])].
6717 ((x \ x) * x) * ((x \
x) \ y) = (x \ x) * ((x * y) * (x \ x)).
[para(3(a,1),164(a,1,2,1,2)),flip(a)].
6741 ((x \ x) * x) * (((x
\ x) \ ((x \ x) * (x \ x))) \ y) = (x \ x) * ((x * y) * (x \ x)). [para(150(a,1),164(a,1,2,1)),flip(a)].
6788 (((x \ x) \ (x \ x))
* (x \ x)) * x = ((x \ x) \ (x \ x)) * ((x \ x) * x). [para(4376(a,1),164(a,1,2,1)),rewrite([4426(7),6717(9),3(6),3(6)]),flip(a)].
8388 x * ((y * ((z \ z) \
(z \ z))) * z) = x * (y * z). [para(439(a,1),9(a,1)), rewrite([9(4)]),flip(a)].
8704 (x / ((y * ((z \ z) \
(z \ z))) * z)) * (y * z) = x. [para(8388(a,1),2(a,1))].
8705 x * ((y / ((z \ z) \
(z \ z))) * z) = x * (y * z). [para(2(a,1),8388(a,1,2,1)),flip(a)].
9080 (x / ((y / ((z \ z) \
(z \ z))) * z)) * (y * z) = x. [para(8705(a,1),2(a,1))].
9533 (x / (((y / z) / ((z
\ z) \ (z \ z))) * z)) * y = x. [para(2(a,1),9080(a,1,2))].
9978 (((x \ x) * x) * y) *
((((((x \ x) * x) * (y / (x \ x))) * (x \ x)) \ z) * (x \ x)) = (x \ x) * (z * (x
\ x)). [para(4623(a,1),592(a,1,1,1))].
9979 (((x \ x) * x) * y) *
((((x * (y / ((x \ x) * (x \ x)))) * ((x \ x) * (x \ x))) \ z) * ((x \ x) * (x
\ x))) = ((x \ x) * (x \ x)) * (z * ((x \ x) * (x \ x))). [para(4677(a,1),592(a,1,1,1))].
10807 ((x \ x) * x) *
((((x \ x) \ (x \ x)) * (x \ x)) \ y) = (x \ x) * ((x * y) * (x \ x)). [para(904(a,1),164(a,1,2,1)),flip(a)].
12240 ((x \ x) * x) * (x *
((x \ (((x \ x) * x) * y)) * x)) = ((x \ x) * x) * (x * (y * x)). [para(1768(a,1),1693(a,2,2)),rewrite([1693(21),6114(9)]),flip(a)].
12303 ((x \ x) * x) * (x *
((((((x \ x) * x) \ ((x \ x) * x)) * ((x \ x) * x)) \ y) * x)) = ((x \ x) * x)
* (y * ((x \ x) * x)). [back_rewrite(1983),rewrite([12240(18)])].
14244 (x \ x) * ((y * (x \
(x \ x))) * x) = (x \ x) * y. [para(2(a,1),1811(a,1,2,1,1)),rewrite([2(9)])].
14299 (x \ x) * ((x \ (x \
x)) * x) = x \ x. [para(14244(a,1),139(a,1)),rewrite([3(5),3196(9)]),flip(a)].
14305 (x \ x) * ((y / (z /
(z \ (x \ x)))) * z) = z * ((z \ (x \ x)) * (y * (z \ (x \ x)))). [para(35(a,2),14244(a,2)),rewrite([14244(11)])].
14337 (x \ x) * (y / ((((x
\ (x \ x)) / z) / ((z \ z) \ (z \ z))) * z)) = (x \ x) * (y * x). [para(9533(a,1),14244(a,1,2,1)),flip(a)].
14351 (x \ x) * ((((x \ (x
\ x)) * x) * y) * (x \ x)) = (x \ x) * (y * (x \ x)). [para(14299(a,1),5(a,1,1)),flip(a)].
14352 ((x \ (x \ x)) * x)
* ((y * (x \ x)) * ((x \ (x \ x)) * x)) = (((x \ (x \ x)) * x) * y) * (x \
x). [para(14299(a,1),5(a,1,2)),flip(a)].
14353 (x \ x) * (x * x) =
x * x. [para(14299(a,1),9(a,1,2,1)),rewrite([136(3),9(6)]),flip(a)].
14369 ((x \ x) * (x \ (x \
x))) * x = (x \ x) * (x \ x). [para(14299(a,1),1860(a,1,2,1,2)),rewrite([136(7),10(10)]),flip(a)].
14371 (x \ x) * x =
x. [para(14299(a,1),2405(a,1,2,2)),rewrite([2490(4),4426(4)]),flip(a)].
14384 (x / (((y \ y) *
((((y \ (y \ y)) * y) \ ((y \ (y \ y)) * y)) \ (((y \ (y \ y)) * y) \ ((y \ (y
\ y)) * y)))) * ((y \ (y \ y)) * y))) * (y \ y) = x. [para(14299(a,1),8704(a,1,2))].
14397 ((x \ (x \ x)) * x)
* ((((((x \ (x \ x)) * x) \ y) * (x \ x)) * ((x \ (x \ x)) * x)) * ((x \ (x \
x)) * x)) = (y * (x \ x)) * ((x \ (x \ x)) * x). [para(
14299(a,1),1724(a,1,1,2)),rewrite([14371(13)]),flip(a)].
14464 (((x * ((x \ y) *
x)) \ (x * ((x \ y) * x))) * (y * x)) * (x * ((x \ y) * x)) = (x * ((x \ y) *
x)) * (x * ((x \ y) * x)). [back_rewrite(6095),rewrite([14371(9),14353(28)])].
14466 (x * ((x \ y) * x))
* (x * ((x \ y) * x)) = x * ((((x \ y) * x) * y) * x). [back_rewrite(6093),rewrite([14371(11),14371(5),5(5),14353(20)]),flip(a)].
14467 (x * y) * (y * ((y \
x) * y)) = (x * y) * (x * y). [back_rewrite(6092),rewrite([14371(2),14371(3),14371(5),14371(5),14371(7),14371(8),14371(10),14371(11),14353(12)])].
14471 x * ((x \ x) \ y) =
x * (y * (x \ x)). [back_rewrite(6074),rewrite([14353(7),374(7)]),flip(a)].
14474 (x * x) * y = x * (x
* y). [back_rewrite(6068),rewrite([14371(2),14371(2),14371(2),14371(2),333(4),14353(5)]),flip(a)].
14485 ((x \ y) * x) * y =
(x \ y) * (x * y). [back_rewrite(6050),rewrite([14353(4),14474(4),3(3),14371(6)]),flip(a)].
14491 ((x * ((x \ y) * x))
\ (x * ((x \ y) * x))) * (y * ((x * y) * x)) = y * ((x * y) * x). [back_rewrite(6031),rewrite([14371(9),14371(20),14464(13),14466(7)
, 14485(3),9(5),14466(17),14485(13),9(15)]),flip(a)].
14504 x * ((y * x) * x) =
x * (y * (x * x)). [back_rewrite(5998),rewrite([14371(2),14353(4),5(3),14371(5)])].
14509 (x * y) * (x * y) =
x * ((y * x) * y). [back_rewrite(5690),rewrite([14371(2),14371(15),14371(12),14467(5),14466(17),14485(13),9(15),14491(14)])].
15027 x * (x * ((x \ y) *
x)) = x * (y * x). [back_rewrite(12303),rewrite([14371(2),14371(2),14371(2),14371(3),14371(2),14371(6),14371(6)])].
15201 (x \ x) * ((x * y) *
(x \ x)) = x * (y * (x \ x)). [back_rewrite(10807),rewrite([14371(2),14371(5),14471(3)]),flip(a)].
15275 (x * y) * ((((x * (y
/ ((x \ x) * (x \ x)))) * ((x \ x) * (x \ x))) \ z) * ((x \ x) * (x \ x))) = (x
\ x) * ((x \ x) * (z * ((x \ x) * (x \ x)))). [back_rewrite(9979),rewrite([14371(2),14474(24)])].
15276 (x * y) * ((((x *
((x \ x) * y)) * (x \ x)) \ z) * (x \ x)) = (x \ x) * (z * (x \ x)). [back_rewrite(9978),rewrite([14371(2),14371(3),135(4)])].
15619 ((x \ x) \ (x \ x))
* x = x. [back_rewrite(6788),rewrite([14371(5),14371(2),14371(5)]),flip(a)].
15636 x * (((x \ x) \ ((x
\ x) * (x \ x))) \ y) = x * (y * (x \ x)). [back_rewrite(6741),rewrite([14371(2),15201(12)])].
15726 x * (y * ((y \ z) *
y)) = x * (z * y). [back_rewrite(5607),rewrite([15619(4),15619(4),4426(4),14371(2),14371(4),15619(6),15027(7)]),flip(a)].
15728 x * ((x \ y) * x) =
y * x. [back_rewrite(5589),rewrite([14371(2),14371(2),14371(3),14371(3),15726(7),15619(4),14371(3),14371(3),14371(4)]),flip(a)].
15836 (x * y) * x = x * (y
* x). [back_rewrite(4293),rewrite([14371(2),14371(4),1729(4),14371(4),15728(6)]),flip(a)].
16316 (x * (y \ y)) * ((y
\ (y \ y)) * y) = x * (y \ y). [back_rewrite(14397),rewrite([14504(18),14509(16),3(14),14371(13),9(14),14299(5)]),flip(a)].
16933 (((x \ (x \ x)) * x)
* y) * (x \ x) = ((x \ (x \ x)) * x) * (y * (x \ x)). [back_rewrite(14352),rewrite([16316(9)]),flip(a)].
17017 (x \ x) * (((x \ (x
\ x)) * x) * (y * (x \ x))) = (x \ x) * (y * (x \ x)). [back_rewrite(14351),rewrite([16933(7)])].
17568 x * (x * ((x * x) \
y)) = y. [para(14474(a,1),3(a,1))].
17924 (x \ x) * (y * (x \
x)) = x * ((x \ y) * (x \ x)). [para(15619(a,1),964(a,1,2,1,1,1)),rewrite([3(3),14371(2),3(2)]),flip(a)].
17947 (x \ x) * (((x \ (x
\ x)) * x) * (y * (x \ x))) = x * ((x \ y) * (x \ x)). [back_rewrite(17017),rewrite([17924(12)])].
17963 (x * y) * ((((x *
((x \ x) * y)) * (x \ x)) \ z) * (x \ x)) = x * ((x \ z) * (x \ x)). [back_rewrite(15276),rewrite([17924(14)])].
18297 (x \ y) * ((x * (z *
x)) * (x \ y)) = ((x \ y) * (x * z)) * y.
[para(15836(a,1),10(a,1,2,1))].
18452 (x \ x) * (x \ x) =
x \ x. [para(14299(a,1),15836(a,1,1)),rewrite([14485(9),3(8),14299(8)])].
18510 x * (y * (x \ x)) =
x * y. [back_rewrite(15636),rewrite([18452(4),145(5)]),flip(a)].
18511 (x \ x) * y =
y. [back_rewrite(15275),rewrite([18452(4),135(4),18452(7),18452(10),17963(10),18510(4),3(2),18452(5),17924(5),18510(5),3(3)]),flip(a)].
18514 (x \ (x \ x)) * x =
x \ x. [back_rewrite(14369),rewrite([18511(4),18511(6)])].
18570 x * (y \ y) =
x. [back_rewrite(17947),rewrite([18514(4),18511(5),18511(4),18510(6),3(4)])].
18709 x / (y \ y) =
x. [back_rewrite(14384),rewrite([18514(4),18514(5),18514(7),18514(8),18570(9),18514(4),18570(3),18570(4)])].
18716 x / (y \ (y \ y)) =
x * y. [back_rewrite(14337),rewrite([18709(8),2(5),18511(5),18511(6)])].
18723 x * ((x \ (y \ y)) *
(z * (x \ (y \ y)))) = (z / (x / (x \ (y \ y)))) * x. [back_rewrite(14305),rewrite([18511(7)]),flip(a)].
19368 ((x * y) / (y / (y \
(z \ z)))) * y = y * ((y \ (z \ z)) * x).
[para(18511(a,1),1112(a,1)),rewrite([18570(11)])].
19371 (x \ (y \ y)) * (z *
(x \ (y \ y))) = (x \ (y \ y)) * (z / x).
[para(18570(a,1),40(a,1)),flip(a)].
19384 x \ x = y \ y. [para(18570(a,1),18511(a,1))].
19385 (x / (y / (y \ (z \
z)))) * y = y * ((y \ (z \ z)) * (x / y)). [back_rewrite(18723),rewrite([19371(6)]),flip(a)].
19387 x * ((x \ (y \ y)) *
((z * x) / x)) = x * ((x \ (y \ y)) * z).
[back_rewrite(19368),rewrite([19385(6)])].
19881 (x \ (x \ x)) * (x *
y) = y. [para(18514(a,1),8(a,2,1)),rewrite([18716(5),18297(8),18570(6),18511(6)])].
20062 ((x * y) / (y * y))
* y = y * ((y \ (y \ y)) * x). [para(18716(a,1),1089(a,1,2,1,1)),rewrite([18716(5),18511(6)])].
20065 x / (y \ (z \ z)) =
x * y. [para(19384(a,1),18716(a,1,2,2))].
21256 x * ((x \ (y \ y)) *
(z / x)) = (z / (x * x)) * x. [back_rewrite(19385),rewrite([20065(3)]),flip(a)].
21302 x * ((x \ (y \ y)) *
z) = x * ((x \ (x \ x)) * z). [back_rewrite(19387),rewrite([21256(6),20062(4)]),flip(a)].
21414 (x \ (x \ x)) * y =
x \ y. [para(3(a,1),19881(a,1,2))].
21433 x \ (x \ x) = x \ (x
/ x). [para(19881(a,1),40(a,2)),rewrite([21414(4),18570(4)]),flip(a)].
21558 (x \ (x / x)) * y =
x * ((x * x) \ y). [para(17568(a,1),19881(a,1,2)),rewrite([21433(2)])].
21563 x * ((x \ (y \ y)) *
z) = z. [back_rewrite(21302),rewrite([21433(6),21558(7),17568(8)])].
21572 ((x * y) / (y * y))
* y = x. [back_rewrite(20062),rewrite([21433(6),21558(7),17568(8)])].
22783 (x / (y * y)) * y =
x / y. [back_rewrite(21256),rewrite([21563(5)]),flip(a)].
23209 (x * y) / y =
x. [back_rewrite(21572),rewrite([22783(4)])].
23210 $F. [resolve(23209,a,6,a)].
==============================
end of proof ==========================
%
Length of proof is 169.
%
Level of proof is 34.
%
Maximum clause weight is 79.
%
Given clauses 233.
1
x \ (x * y) = y # label(non_clause) #
label(goal). [goal].
2
(x / y) * y = x. [assumption].
3
x * (x \ y) = y. [assumption].
4
x * ((y * z) * x) = (x * y) * (z * x).
[assumption].
5
(x * y) * (z * x) = x * ((y * z) * x).
[copy(4),flip(a)].
6
c1 \ (c1 * c2) != c2. [deny(1)].
7
(x / y) * ((y * z) * (x / y)) = x * (z * (x / y)). [para(2(a,1),5(a,1,1)),flip(a)].
8
x * ((y * (z / x)) * x) = (x * y) * z.
[para(2(a,1),5(a,1,2)),flip(a)].
9
x * (((x \ y) * z) * x) = y * (z * x).
[para(3(a,1),5(a,1,1)),flip(a)].
10
(x \ y) * ((z * x) * (x \ y)) = ((x \ y) * z) * y. [para(3(a,1),5(a,1,2)),flip(a)].
14
(x / y) * (z * (x / y)) = x * ((y \ z) * (x / y)). [para(3(a,1),7(a,1,2,1))].
22
(x * (y / (z / x))) * z = x * (y * x).
[para(2(a,1),8(a,1,2,1)),flip(a)].
23
x * ((((y * (z / x)) * x) * u) * x) = ((x * y) * z) * (u * x). [para(8(a,1),5(a,1,1)),flip(a)].
24
((x * (y / z)) * z) * ((u * z) * ((x * (y / z)) * z)) = (((x * (y / z)) * z) *
u) * ((z * x) * y). [para(8(a,1),5(a,1,2)),flip(a)].
26
x * (((y \ x) \ z) * y) = y * (z * y).
[para(3(a,1),9(a,1,2,1)),flip(a)].
27
x * (((((x \ y) * z) * x) * u) * x) = (y * (z * x)) * (u * x). [para(9(a,1),5(a,1,1)),flip(a)].
29
x * (((y * (z / (u \ x))) * (u \ x)) * u) = u * ((((u \ x) * y) * z) * u). [para(8(a,1),9(a,1,2,1)),flip(a)].
30
x * (((((y \ x) \ z) * u) * (y \ x)) * y) = y * ((z * (u * (y \ x))) * y). [para(9(a,1),9(a,1,2,1)),flip(a)].
36
x * (((((y \ x) \ z) * y) * u) * x) = (y * (z * y)) * (u * x). [para(26(a,1),5(a,1,1)),flip(a)].
38
x * ((y * ((x \ (x * y)) \ z)) * x) = x * (z * x). [para(26(a,1),5(a,1)),flip(a)].
40
((x \ y) * (z / x)) * y = (x \ y) * (z * (x \ y)). [para(2(a,1),10(a,1,2,1)),flip(a)].
46
x * ((((x \ y) * z) * y) * x) = y * (((z * x) * (x \ y)) * x). [para(10(a,1),9(a,1,2,1))].
51
x * ((y \ (z / (x / y))) * (x / y)) = (x / y) * z. [para(2(a,1),14(a,1,2)),flip(a)].
124
x * ((x \ x) * (y * (x \ x))) = x * y.
[para(40(a,1),8(a,1,2)),rewrite([3(7)])].
135
x * (y / (x \ x)) = x * ((x \ x) * y).
[para(2(a,1),124(a,1,2,2)),flip(a)].
136
x * ((x \ x) * x) = x * x. [para(3(a,1),124(a,1,2,2))].
139
x * (((x \ x) * y) * z) = x * (y * (z / (x \ x))). [para(8(a,1),124(a,1,2))].
142
x * (((x \ x) \ y) * z) = x * (y * (z * (x \ x))). [para(9(a,1),124(a,1,2)),flip(a)].
145
x * (((x \ x) \ (x \ x)) \ y) = x * y.
[para(26(a,1),124(a,1,2)),rewrite([124(5)]),flip(a)].
147
x * (y * (x / (x \ x))) = x * (y * x).
[para(10(a,1),124(a,1,2)),rewrite([139(4)])].
150
x * (y * (((x \ x) \ ((x \ x) * y)) \ z)) = x * z. [para(38(a,1),124(a,1,2)),rewrite([124(5)]),flip(a)].
153
x * ((((x \ x) * x) * y) * x) = x * ((x * y) * x). [para(136(a,1),5(a,1,1)),rewrite([5(3)]),flip(a)].
161
x * ((x \ x) \ (x \ x)) = x * ((x \ x) * (x \ x)). [para(136(a,1),124(a,1,2)),flip(a)].
164
(x \ x) * ((x * ((x \ x) * y)) * (x \ x)) = ((x \ x) * x) * y. [para(135(a,1),8(a,1,2,1))].
219
x * (((((x \ x) \ (x \ x)) \ y) * z) * x) = x * ((y * z) * x). [para(145(a,1),5(a,1,1)),rewrite([5(3)]),flip(a)].
227
x * ((y / (x / (x \ x))) * x) = x * y.
[para(2(a,1),147(a,1,2)),flip(a)].
258
(x / (x \ x)) * y = x * y. [para(51(a,1),147(a,1)),rewrite([142(10),3(8),227(8)])].
300
x * ((y * (z / (x / (x \ x)))) * x) = (x * y) * z. [para(258(a,1),8(a,1)),rewrite([147(8),258(9)])].
311
x * (y / (y \ y)) = x * y. [para(258(a,1),124(a,1,2,2)),rewrite([124(5)]),flip(a)].
333
(x / (y / (y \ y))) * y = x. [para(311(a,1),2(a,1))].
374
x * (y * ((z * (x \ x)) / (x \ x))) = x * (y * z). [para(5(a,1),139(a,1,2)),rewrite([124(6)]),flip(a)].
422
x * (((((y \ x) \ (y \ x)) \ z) * u) * y) = x * ((z * (u * ((y \ x) \ (y \
x)))) * y). [para(142(a,1),9(a,1,2,1)),rewrite([9(9)]),flip(a)].
439
x * ((y * (z * ((x \ x) \ (x \ x)))) * x) = x * ((y * z) * x). [back_rewrite(219),rewrite([422(7)])].
501
x * ((x * (((x \ x) * x) \ y)) * x) = x * (y * x). [para(3(a,1),153(a,1,2,1)),flip(a)].
504
x * (((x * y) * (x \ x)) * x) = x * ((x * (y * (x \ x))) * x). [para(5(a,1),153(a,1,2,1)),rewrite([139(7),311(6)])].
554
x * ((((x \ x) \ (x \ x)) * y) * x) = x * ((((x \ x) * (x \ x)) * y) * x). [para(161(a,1),5(a,1,1)),rewrite([5(6)]),flip(a)].
592
((x * y) * z) * ((((y * (z / x)) * x) \ u) * x) = x * (u * x). [para(3(a,1),23(a,1,2,1)),flip(a)].
904
x * ((x \ x) * ((((x \ x) \ (x \ x)) * (x \ x)) \ y)) = x * y. [para(501(a,1),124(a,1,2)),rewrite([124(5)]),flip(a)].
964
(x * (y * z)) * (((((z \ x) * y) * z) \ u) * z) = z * (u * z). [para(3(a,1),27(a,1,2,1)),flip(a)].
1627
x * ((((x \ x) * ((x \ y) * z)) * x) * x) = (y * (z * x)) * ((x \ x) * x). [para(46(a,2),27(a,1))].
1665
x * (((y * x) * (x \ x)) * x) = x * ((y * x) * x). [para(46(a,2),36(a,1)),rewrite([3(4),5(8)]),flip(a)].
1692
x * ((y * (z / ((x \ x) \ (x \ x)))) * ((x \ x) \ (x \ x))) = x * ((((x \ x) \
(x \ x)) * y) * z). [para(29(a,1),124(a,1,2)),rewrite([124(10)]),flip(a)].
1693
x * ((x * (y * ((x \ x) / (x \ x)))) * x) = x * ((x * y) * x). [para(135(a,1),29(a,1,2,1,1)),rewrite([504(7),139(5),153(12)])].
1699
x * ((((x \ x) * y) * x) * x) = x * ((y * x) * x). [para(311(a,1),29(a,1,2,1,1)),rewrite([1665(5)]),flip(a)].
1724
(x * (y * z)) * ((z \ z) * z) = z * ((((z \ x) * y) * z) * z). [back_rewrite(1627),rewrite([1699(7)]),flip(a)].
1729
x * ((y * (x \ x)) * x) = x * (y * x).
[para(2(a,1),1665(a,1,2,1,1)),rewrite([2(6)])].
1763
x * ((y / (x \ x)) * x) = x * (y * x).
[para(2(a,1),1729(a,1,2,1)),flip(a)].
1768
x * ((y \ y) * y) = y * ((y \ x) * y).
[para(1729(a,1),9(a,1)),flip(a)].
1779
x * (y * ((x \ x) \ (x \ x))) = x * y.
[para(1729(a,1),124(a,1,2)),rewrite([124(5)]),flip(a)].
1794
((x \ x) * x) * (x \ x) = (x \ x) * x.
[para(161(a,1),1729(a,1,2,1)),rewrite([164(8),3(7)])].
1811
(x \ x) * (((y * x) * (x \ (x \ x))) * x) = (x \ x) * (y * x). [para(1729(a,1),46(a,1)),rewrite([9(5)]),flip(a)].
1813
x * ((((x \ x) * y) * z) * x) = x * ((y * (z / (x \ x))) * x). [para(1729(a,1),29(a,1)),flip(a)].
1815
x * ((((x \ x) \ (x \ x)) * y) * z) = x * (y * (z / ((x \ x) \ (x \ x)))). [back_rewrite(1692),rewrite([1779(10)]),flip(a)].
1818
x * (y * (x / ((x \ x) \ (x \ x)))) = x * (y * x). [back_rewrite(554),rewrite([1815(6),1813(12),139(12),311(11),1763(10)])].
1860
x * ((x \ (x * y)) * x) = x * (y * x).
[para(1768(a,1),5(a,1)),rewrite([1729(8)])].
1867
(x * ((y \ y) * y)) * z = (y * ((y \ x) * y)) * z. [para(1768(a,1),8(a,2,1)),rewrite([8(6)])].
1869
x * ((y * ((y \ (x \ z)) * y)) * x) = z * (((y \ y) * y) * x). [para(1768(a,1),9(a,1,2,1))].
1871
x * (y * ((z \ z) * z)) = x * (z * ((z \ y) * z)). [para(1768(a,1),9(a,2,2)),rewrite([9(10)])].
1903
x * (y * (((x \ x) \ (x \ x)) * (x \ x))) = x * ((x \ x) \ y). [para(1768(a,2),124(a,1,2))].
1940
(x \ x) * (((x \ x) \ x) * (x \ x)) = x.
[para(1768(a,1),142(a,1)),rewrite([124(12),3(8)])].
1983
((x \ x) * x) * (x * ((x \ (((x \ x) * x) * (((((x \ x) * x) \ ((x \ x) * x)) *
((x \ x) * x)) \ y))) * x)) = ((x \ x) * x) * (y * ((x \ x) * x)). [para(1768(a,1),501(a,1,2))].
2064
x * ((((x \ x) \ y) * z) * x) = x * ((y * (z * (x \ x))) * x). [para(30(a,1),22(a,2)),rewrite([22(9),1729(7)])].
2070
x * ((((x \ x) \ (x \ x)) \ y) * z) = x * (y * (z * ((x \ x) \ (x \ x)))). [para(30(a,1),124(a,1,2)),rewrite([124(10),1779(16)]),flip(a)].
2149
((x \ x) * (x \ x)) * x = (x \ x) * ((x \ x) * x). [para(1794(a,1),5(a,2,2)),rewrite([3(5)])].
2155
x * ((x \ x) * ((x \ x) * x)) = x * x.
[para(1794(a,1),124(a,1,2,2)),rewrite([136(8)])].
2405
x * ((x \ x) \ ((x \ x) * y)) = x * y.
[para(1860(a,1),124(a,1,2)),rewrite([124(5)]),flip(a)].
2450
x * (((y * (x \ x)) * x) * x) = x * ((y * x) * x). [para(1729(a,1),1860(a,1,2,1,2)),rewrite([1860(5)]),flip(a)].
2454
x * ((y * ((x \ x) \ (x \ x))) * x) = x * (y * x). [para(1779(a,1),1860(a,1,2,1,2)),rewrite([1860(4)]),flip(a)].
2473
x * ((x \ x) * (x \ x)) = x. [para(1940(a,1),1860(a,1,2,1,2)),rewrite([1940(6),9(8)]),flip(a)].
2490
x * ((x \ x) \ (x \ x)) = x. [back_rewrite(161),rewrite([2473(8)])].
2643
(x \ x) * (((x \ x) \ (x \ x)) * x) = (x \ x) * x. [para(2490(a,1),124(a,1,2,2))].
2725
x * ((x \ x) \ ((x \ x) \ (x \ x))) = x.
[para(2155(a,1),2405(a,1,2,2)),rewrite([2405(6),3(2),1903(10)]),flip(a)].
2905
x * ((y * ((x \ x) * (x \ x))) * x) = x * (y * x). [para(2725(a,1),38(a,1,2,1,2,1,2)),rewrite([2064(10),2064(10),9(8)])].
3138
x * ((y / (x / ((x \ x) \ (x \ x)))) * x) = x * y. [para(2(a,1),1818(a,1,2)),flip(a)].
3149
(x / ((x \ x) \ (x \ x))) * y = x * y.
[para(1818(a,1),51(a,1)),rewrite([2070(11),2490(9),3138(7)]),flip(a)].
3196
x * (y / ((y \ y) \ (y \ y))) = x * y.
[para(3149(a,1),124(a,1,2,2)),rewrite([124(5)]),flip(a)].
4274
x * ((y \ y) * ((y \ y) * y)) = y * ((y \ x) * y). [para(2149(a,1),9(a,2,2)),rewrite([2905(7)]),flip(a)].
4293
((x \ x) * x) * ((y * (x \ x)) * ((x \ x) * x)) = x * ((x \ (((x \ x) * x) * y))
* x). [para(2149(a,1),24(a,2,2)),rewrite([311(4),1794(4),311(8),1794(8),311(12),1794(12),4274(16)])].
4376
x * (((y \ y) \ (y \ y)) * y) = y * ((y \ x) * y). [para(2454(a,1),9(a,1)),flip(a)].
4426
x * ((x \ (x \ x)) * x) = (x \ x) * x.
[back_rewrite(2643),rewrite([4376(6)])].
4623
(x \ x) * ((x \ x) * x) = (x \ x) * x.
[para(4426(a,1),1768(a,2))].
4625
x * ((x \ ((x \ x) * x)) * x) = (x \ x) * (x * x). [para(4426(a,1),1860(a,1,2,1,2)),rewrite([9(10)])].
4677
((x \ x) * (x \ x)) * x = (x \ x) * x.
[back_rewrite(2149),rewrite([4623(8)])].
5532
x * ((((y \ y) \ (y \ y)) * y) * z) = x * (((y \ y) * y) * z). [para(4376(a,1),9(a,1,2,1)),rewrite([1869(6)]),flip(a)].
5589
x * (y * ((y \ ((((y \ y) * y) \ ((y \ y) * y)) \ (((y \ y) * y) \ ((y \ y) * y))))
* y)) = ((y \ y) * y) * ((((y \ y) * y) \ x) * ((y \ y) * y)). [para(1768(a,1),4376(a,1,2))].
5607
x * (y * (z * ((z \ ((((z \ z) \ (z \ z)) * z) \ (((z \ z) \ (z \ z)) * z))) *
z))) = x * (((z \ z) * z) * (z * ((z \ ((((z \ z) \ (z \ z)) * z) \ y)) *
z))). [para(4376(a,1),1871(a,1,2,2)),rewrite([4376(28),5532(28)])].
5680
((x \ x) * x) * ((x \ x) * x) = (x \ x) * (x * x). [para(4625(a,1),1768(a,2))].
5690
(x * ((y \ y) * y)) * (((y * ((y \ x) * y)) \ (((y * ((y \ x) * y)) \ (y * ((y
\ x) * y))) * (y * ((y \ x) * y)))) * (y * ((y \ x) * y))) = ((y * ((y \ x) *
y)) \ (y * ((y \ x) * y))) * ((y * ((y \ x) * y)) * (y * ((y \ x) * y))). [para(4625(a,1),1867(a,2))].
5997
((x \ x) * x) * ((((x \ x) * x) * y) * ((x \ x) * x)) = ((x \ x) * (x * x)) *
(y * ((x \ x) * x)). [para(5680(a,1),5(a,1,1)),flip(a)].
5998
(((x \ x) * x) * y) * ((x \ x) * (x * x)) = ((x \ x) * x) * (y * (x * x)). [para(5680(a,1),5(a,1,2)),rewrite([1724(15),2450(15),9(13)])].
5999
((x \ x) * x) * x = (x \ x) * (x * x).
[para(5680(a,1),8(a,2)),rewrite([135(6),4623(5),136(4),10(5)])].
6031
(((x * ((x \ y) * x)) \ (x * ((x \ y) * x))) * (y * ((x \ x) * x))) * (((x * ((x
\ y) * x)) \ (x * ((x \ y) * x))) * (x * ((x \ y) * x))) = ((x * ((x \ y) * x))
\ (x * ((x \ y) * x))) * ((x * ((x \ y) * x)) * (x * ((x \ y) * x))). [para(1871(a,2),5680(a,1,1))].
6047
((x \ x) * (x * x)) * (y * ((x \ x) * x)) = ((x \ x) * x) * (x * (y * x)). [para(5999(a,1),5(a,1,1)),rewrite([5(13),1729(13)])].
6050
(x \ y) * (((x \ x) * (x * x)) * (x \ y)) = ((x \ y) * ((x \ x) * x)) * y. [para(5999(a,1),10(a,1,2,1))].
6068
((x \ x) * x) * (x * ((y / (((x \ x) * x) / (((x \ x) * x) \ ((x \ x) * x)))) *
x)) = ((x \ x) * (x * x)) * y. [para(5999(a,1),300(a,2,1)),rewrite([5(15),1729(15)])].
6074
x * (y * ((((x \ x) \ (x \ x)) * ((x \ x) * (x \ x))) / (x \ x))) = x * ((x \ x)
\ y). [para(5999(a,1),374(a,1,2,2,1)),rewrite([1903(18)])].
6092
(((x * ((y \ y) * y)) \ (x * ((y \ y) * y))) * (x * ((y \ y) * y))) * (y * ((y
\ x) * y)) = ((x * ((y \ y) * y)) \ (x * ((y \ y) * y))) * ((x * ((y \ y) * y))
* (x * ((y \ y) * y))). [para(5999(a,1),1871(a,1)),flip(a)].
6093
(((x * ((x \ y) * x)) \ (x * ((x \ y) * x))) * (x * ((x \ y) * x))) * (y * ((x
\ x) * x)) = ((x * ((x \ y) * x)) \ (x * ((x \ y) * x))) * ((x * ((x \ y) * x))
* (x * ((x \ y) * x))). [para(5999(a,1),1871(a,2))].
6095
(((x * ((x \ y) * x)) \ (x * ((x \ y) * x))) * (y * ((x \ x) * x))) * (x * ((x
\ y) * x)) = ((x * ((x \ y) * x)) \ (x * ((x \ y) * x))) * ((x * ((x \ y) * x))
* (x * ((x \ y) * x))). [para(1871(a,2),5999(a,1,1))].
6114
((x \ x) * x) * ((((x \ x) * x) * y) * ((x \ x) * x)) = ((x \ x) * x) * (x * (y
* x)). [back_rewrite(5997),rewrite([6047(16)])].
6717
((x \ x) * x) * ((x \ x) \ y) = (x \ x) * ((x * y) * (x \ x)). [para(3(a,1),164(a,1,2,1,2)),flip(a)].
6741
((x \ x) * x) * (((x \ x) \ ((x \ x) * (x \ x))) \ y) = (x \ x) * ((x * y) * (x
\ x)). [para(150(a,1),164(a,1,2,1)),flip(a)].
6788
(((x \ x) \ (x \ x)) * (x \ x)) * x = ((x \ x) \ (x \ x)) * ((x \ x) * x). [para(4376(a,1),164(a,1,2,1)),rewrite([4426(7),6717(9),3(6),3(6)]),flip(a)].
8388
x * ((y * ((z \ z) \ (z \ z))) * z) = x * (y * z). [para(439(a,1),9(a,1)),rewrite([9(4)]),flip(a)].
8704
(x / ((y * ((z \ z) \ (z \ z))) * z)) * (y * z) = x. [para(8388(a,1),2(a,1))].
8705
x * ((y / ((z \ z) \ (z \ z))) * z) = x * (y * z). [para(2(a,1),8388(a,1,2,1)),flip(a)].
9080
(x / ((y / ((z \ z) \ (z \ z))) * z)) * (y * z) = x. [para(8705(a,1),2(a,1))].
9533
(x / (((y / z) / ((z \ z) \ (z \ z))) * z)) * y = x. [para(2(a,1),9080(a,1,2))].
9978
(((x \ x) * x) * y) * ((((((x \ x) * x) * (y / (x \ x))) * (x \ x)) \ z) * (x \
x)) = (x \ x) * (z * (x \ x)). [para(4623(a,1),592(a,1,1,1))].
9979
(((x \ x) * x) * y) * ((((x * (y / ((x \ x) * (x \ x)))) * ((x \ x) * (x \ x)))
\ z) * ((x \ x) * (x \ x))) = ((x \ x) * (x \ x)) * (z * ((x \ x) * (x \
x))). [para(4677(a,1),592(a,1,1,1))].
10807
((x \ x) * x) * ((((x \ x) \ (x \ x)) * (x \ x)) \ y) = (x \ x) * ((x * y) * (x
\ x)). [para(904(a,1),164(a,1,2,1)),flip(a)].
12240
((x \ x) * x) * (x * ((x \ (((x \ x) * x) * y)) * x)) = ((x \ x) * x) * (x * (y
* x)). [para(1768(a,1),1693(a,2,2)),rewrite([1693(21),6114(9)]),flip(a)].
12303
((x \ x) * x) * (x * ((((((x \ x) * x) \ ((x \ x) * x)) * ((x \ x) * x)) \ y) *
x)) = ((x \ x) * x) * (y * ((x \ x) * x)). [back_rewrite(1983),rewrite([12240(18)])].
14244
(x \ x) * ((y * (x \ (x \ x))) * x) = (x \ x) * y. [para(2(a,1),1811(a,1,2,1,1)),rewrite([2(9)])].
14299
(x \ x) * ((x \ (x \ x)) * x) = x \ x.
[para(14244(a,1),139(a,1)),rewrite([3(5),3196(9)]),flip(a)].
14337
(x \ x) * (y / ((((x \ (x \ x)) / z) / ((z \ z) \ (z \ z))) * z)) = (x \ x) *
(y * x). [para(9533(a,1),14244(a,1,2,1)),flip(a)].
14351
(x \ x) * ((((x \ (x \ x)) * x) * y) * (x \ x)) = (x \ x) * (y * (x \ x)). [para(14299(a,1),5(a,1,1)),flip(a)].
14352
((x \ (x \ x)) * x) * ((y * (x \ x)) * ((x \ (x \ x)) * x)) = (((x \ (x \ x)) *
x) * y) * (x \ x). [para(14299(a,1),5(a,1,2)),flip(a)].
14353
(x \ x) * (x * x) = x * x. [para(14299(a,1),9(a,1,2,1)),rewrite([136(3),9(6)]),flip(a)].
14369
((x \ x) * (x \ (x \ x))) * x = (x \ x) * (x \ x). [para(14299(a,1),1860(a,1,2,1,2)),rewrite([136(7),10(10)]),flip(a)].
14371
(x \ x) * x = x. [para(14299(a,1),2405(a,1,2,2)),rewrite([2490(4),4426(4)]),flip(a)].
14384
(x / (((y \ y) * ((((y \ (y \ y)) * y) \ ((y \ (y \ y)) * y)) \ (((y \ (y \ y))
* y) \ ((y \ (y \ y)) * y)))) * ((y \ (y \ y)) * y))) * (y \ y) = x. [para(14299(a,1),8704(a,1,2))].
14397
((x \ (x \ x)) * x) * ((((((x \ (x \ x)) * x) \ y) * (x \ x)) * ((x \ (x \ x))
* x)) * ((x \ (x \ x)) * x)) = (y * (x \ x)) * ((x \ (x \ x)) * x). [para(14299(a,1),1724(a,1,1,2)),rewrite([14371(13)]),flip(a)].
14464
(((x * ((x \ y) * x)) \ (x * ((x \ y) * x))) * (y * x)) * (x * ((x \ y) * x)) =
(x * ((x \ y) * x)) * (x * ((x \ y) * x)). [back_rewrite(6095),rewrite([14371(9),14353(28)])].
14466
(x * ((x \ y) * x)) * (x * ((x \ y) * x)) = x * ((((x \ y) * x) * y) * x). [back_rewrite(6093),rewrite([14371(11),14371(5),5(5),14353(20)]),flip(a)].
14467
(x * y) * (y * ((y \ x) * y)) = (x * y) * (x * y). [back_rewrite(6092),rewrite([14371(2),14371(3),14371(5),14371(5),14371(7),14371(8),14371(10),14371(11),14353(12)])].
14471
x * ((x \ x) \ y) = x * (y * (x \ x)).
[back_rewrite(6074),rewrite([14353(7),374(7)]),flip(a)].
14474
(x * x) * y = x * (x * y). [back_rewrite(6068),rewrite([14371(2),14371(2),14371(2),14371(2),333(4),14353(5)]),flip(a)].
14485
((x \ y) * x) * y = (x \ y) * (x * y).
[back_rewrite(6050),rewrite([14353(4),14474(4),3(3),14371(6)]),flip(a)].
14491
((x * ((x \ y) * x)) \ (x * ((x \ y) * x))) * (y * ((x * y) * x)) = y * ((x *
y) * x). [back_rewrite(6031),rewrite([14371(9),14371(20),14464(13),14466(7),14485(3),9(5),14466(17),14485(13),9(15)]),flip(a)].
14504
x * ((y * x) * x) = x * (y * (x * x)).
[back_rewrite(5998),rewrite([14371(2),14353(4),5(3),14371(5)])].
14509
(x * y) * (x * y) = x * ((y * x) * y).
[back_rewrite(5690),rewrite([14371(2),14371(15),14371(12),14467(5),14466(17),14485(13),9(15),14491(14)])].
15027
x * (x * ((x \ y) * x)) = x * (y * x).
[back_rewrite(12303),rewrite([14371(2),14371(2),14371(2),14371(3),14371(2),14371(6),14371(6)])].
15201
(x \ x) * ((x * y) * (x \ x)) = x * (y * (x \ x)). [back_rewrite(10807),rewrite([14371(2),14371(5),14471(3)]),flip(a)].
15275
(x * y) * ((((x * (y / ((x \ x) * (x \ x)))) * ((x \ x) * (x \ x))) \ z) * ((x
\ x) * (x \ x))) = (x \ x) * ((x \ x) * (z * ((x \ x) * (x \ x)))). [back_rewrite(9979),rewrite([14371(2),14474(24)])].
15276
(x * y) * ((((x * ((x \ x) * y)) * (x \ x)) \ z) * (x \ x)) = (x \ x) * (z * (x
\ x)). [back_rewrite(9978),rewrite([14371(2),14371(3),135(4)])].
15619
((x \ x) \ (x \ x)) * x = x. [back_rewrite(6788),rewrite([14371(5),14371(2),14371(5)]),flip(a)].
15636
x * (((x \ x) \ ((x \ x) * (x \ x))) \ y) = x * (y * (x \ x)). [back_rewrite(6741),rewrite([14371(2),15201(12)])].
15726
x * (y * ((y \ z) * y)) = x * (z * y).
[back_rewrite(5607),rewrite([15619(4),15619(4),4426(4),14371(2),14371(4),15619(6),15027(7)]),flip(a)].
15728
x * ((x \ y) * x) = y * x. [back_rewrite(5589),rewrite([14371(2),14371(2),14371(3),14371(3),15726(7),15619(4),14371(3),14371(3),14371(4)]),flip(a)].
15836
(x * y) * x = x * (y * x). [back_rewrite(4293),rewrite([14371(2),14371(4),1729(4),14371(4),15728(6)]),flip(a)].
16316
(x * (y \ y)) * ((y \ (y \ y)) * y) = x * (y \ y). [back_rewrite(14397),rewrite([14504(18),14509(16),3(14),14371(13),9(14),14299(5)]),flip(a)].
16933
(((x \ (x \ x)) * x) * y) * (x \ x) = ((x \ (x \ x)) * x) * (y * (x \ x)). [back_rewrite(14352),rewrite([16316(9)]),flip(a)].
17017
(x \ x) * (((x \ (x \ x)) * x) * (y * (x \ x))) = (x \ x) * (y * (x \ x)). [back_rewrite(14351),rewrite([16933(7)])].
17924
(x \ x) * (y * (x \ x)) = x * ((x \ y) * (x \ x)). [para(15619(a,1),964(a,1,2,1,1,1)),rewrite([3(3),14371(2),3(2)]),flip(a)].
17947
(x \ x) * (((x \ (x \ x)) * x) * (y * (x \ x))) = x * ((x \ y) * (x \ x)). [back_rewrite(17017),rewrite([17924(12)])].
17963
(x * y) * ((((x * ((x \ x) * y)) * (x \ x)) \ z) * (x \ x)) = x * ((x \ z) * (x
\ x)). [back_rewrite(15276),rewrite([17924(14)])].
18297
(x \ y) * ((x * (z * x)) * (x \ y)) = ((x \ y) * (x * z)) * y. [para(15836(a,1),10(a,1,2,1))].
18452
(x \ x) * (x \ x) = x \ x. [para(14299(a,1),15836(a,1,1)),rewrite([14485(9),3(8),14299(8)])].
18510
x * (y * (x \ x)) = x * y. [back_rewrite(15636),rewrite([18452(4),145(5)]),flip(a)].
18511
(x \ x) * y = y. [back_rewrite(15275),rewrite([18452(4),135(4),18452(7),18452(10),17963(10),18510(4),3(2),18452(5),17924(5),18510(5),3(3)]),flip(a)].
18514
(x \ (x \ x)) * x = x \ x. [back_rewrite(14369),rewrite([18511(4),18511(6)])].
18570
x * (y \ y) = x. [back_rewrite(17947),rewrite([18514(4),18511(5),18511(4),18510(6),3(4)])].
18709
x / (y \ y) = x. [back_rewrite(14384),rewrite([18514(4),18514(5),18514(7),18514(8),18570(9),18514(4),18570(3),18570(4)])].
18716
x / (y \ (y \ y)) = x * y. [back_rewrite(14337),rewrite([18709(8),2(5),18511(5),18511(6)])].
19881
(x \ (x \ x)) * (x * y) = y. [para(18514(a,1),8(a,2,1)),rewrite([18716(5),18297(8),18570(6),18511(6)])].
21414
(x \ (x \ x)) * y = x \ y. [para(3(a,1),19881(a,1,2))].
21423
x \ (x * y) = y. [para(19881(a,1),9(a,2)),rewrite([9(6),21414(4)])].
21424
$F. [resolve(21423,a,6,a)].
==============================
end of proof ==========================
%
Length of proof is 92.
%
Level of proof is 29.
%
Maximum clause weight is 39.
%
Given clauses 193.
1
(x * y) / y = x # label(non_clause) #
label(goal). [goal].
2
(x / y) * y = x. [assumption].
3
x * (x \ y) = y. [assumption].
4
x * (y * (x * z)) = ((x * y) * x) * z.
[assumption].
5
((x * y) * x) * z = x * (y * (x * z)).
[copy(4),flip(a)].
6
(c1 * c2) / c2 != c1. [deny(1)].
7
(x / y) * (y * ((x / y) * z)) = (x * (x / y)) * z. [para(2(a,1),5(a,1,1,1)),flip(a)].
9
x * ((x \ y) * (x * z)) = (y * x) * z.
[para(3(a,1),5(a,1,1,1)),flip(a)].
12
(x * (x / y)) * y = (x / y) * (y * x).
[para(2(a,1),7(a,1,2,2)),flip(a)].
14
(x / y) * ((y * ((x / y) * z)) * ((x / y) * u)) = (((x * (x / y)) * z) * (x /
y)) * u. [para(7(a,1),5(a,1,1,1)),flip(a)].
16
(x * (x / y)) * (y * ((x / y) * z)) = (x / y) * (y * ((x * (x / y)) * z)). [para(7(a,1),7(a,1,2,2)),flip(a)].
24
(x * y) * (y \ z) = y * ((y \ x) * z).
[para(3(a,1),9(a,1,2,2)),flip(a)].
35
((x / x) * (x * x)) * y = x * ((x / x) * (x * y)). [para(12(a,1),5(a,1,1))].
40
x * ((x \ (y / x)) * z) = y * (x \ z).
[para(2(a,1),24(a,1,1)),flip(a)].
41
(x \ y) * (((x \ y) \ x) * z) = y * ((x \ y) \ z). [para(3(a,1),24(a,1,1)),flip(a)].
81
x * (y \ ((y \ (x / y)) \ z)) = y * z.
[para(3(a,1),40(a,1,2)),flip(a)].
84
x * (y \ (y * z)) = x * z. [para(40(a,1),5(a,2)),rewrite([3(3),2(2)]),flip(a)].
92
(x / (y \ (y * z))) * z = x. [para(84(a,1),2(a,1))].
163
(x \ (x / x)) \ y = x * y. [para(81(a,1),3(a,1)),flip(a)].
172
(x \ (x / x)) * (x * y) = y. [para(163(a,1),3(a,1,2))].
194
(x \ (x / x)) * y = x \ y. [para(3(a,1),172(a,1,2))].
200
x \ ((y * x) * z) = (x \ y) * (x * z).
[para(9(a,1),172(a,1,2)),rewrite([194(5)])].
203
(x * y) \ (y * ((y \ x) * z)) = y \ z.
[para(24(a,1),172(a,1,2)),rewrite([194(9)])].
204
x \ (y * (x \ z)) = (x \ (y / x)) * z.
[para(40(a,1),172(a,1,2)),rewrite([194(5)])].
205
x \ (x * y) = y. [para(172(a,1),84(a,2)),rewrite([84(6),194(4)])].
206
(x / y) \ x = y. [para(92(a,1),172(a,1,2)),rewrite([205(2),205(3),205(4),194(6)])].
260
(x \ y) * (x * ((y * x) \ z)) = x \ z.
[para(3(a,1),200(a,1,2)),flip(a)].
288
(x * y) \ (y * z) = y \ ((y \ x) \ z).
[para(3(a,1),203(a,1,2,2))].
310
(x \ ((y * x) / x)) * z = (x \ y) * z.
[para(24(a,1),204(a,1,2)),rewrite([205(4)]),flip(a)].
341
(x \ y) \ (x \ z) = x * ((y * x) \ z).
[para(260(a,1),205(a,1,2))].
349
x \ ((x \ (y / x)) \ z) = y \ (x * z).
[para(2(a,1),288(a,1,1)),flip(a)].
352
(x * (y * (x * z))) \ (z * u) = z \ ((z \ ((x * y) * x)) \ u). [para(5(a,1),288(a,1,1))].
449
(x \ y) * (((x \ ((y * x) / x)) \ z) * ((x \ y) * u)) = (z * (x \ ((y * x) / x)))
* u. [para(310(a,1),9(a,1,2,2)),rewrite([310(11)])].
493
(x \ (y / x)) \ z = x * (y \ (x * z)).
[para(349(a,1),3(a,1,2)),flip(a)].
505
(x * (y \ ((z * y) / y))) * u = (x * (y \ z)) * u. [back_rewrite(449),rewrite([493(5),288(4),3(5),9(7)]),flip(a)].
647
(x * ((x / x) * (x * (x / x)))) * y = (x / x) * ((x * x) * ((x / x) * y)). [para(35(a,1),5(a,1,1))].
680
(x \ x) * (x * y) = (x / x) * (x * y).
[para(41(a,1),194(a,1)),rewrite([493(4),205(3),493(6),205(5),200(6)]),flip(a)].
697
(x \ x) * y = (x / x) * y. [para(3(a,1),680(a,1,2)),rewrite([3(5)])].
700
x * ((x / x) * (x * y)) = (x * x) * y.
[para(680(a,1),5(a,2,2)),rewrite([3(2)]),flip(a)].
701
(x * (x / x)) * y = x * y. [para(680(a,1),5(a,2)),rewrite([697(2),2(2),3(2),697(4),7(6)]),flip(a)].
712
(x / x) * (x * ((x * x) \ y)) = x \ y.
[para(680(a,1),260(a,1))].
748
(x / x) * ((x * x) * ((x / x) * y)) = ((x * x) * (x / x)) * y. [back_rewrite(647),rewrite([700(5)]),flip(a)].
756
(x / x) * ((x \ x) \ y) = y. [para(697(a,1),3(a,1))].
759
(x / x) * (((x \ x) \ y) * ((x / x) * z)) = (y * (x \ x)) * z. [para(697(a,1),9(a,1,2,2)),rewrite([697(7)])].
776
(x \ ((x \ x) \ x)) * y = ((x * x) / (x * x)) * y. [para(288(a,1),697(a,1,1))].
777
(x \ (y \ y)) * z = (x \ (y / y)) * z.
[para(697(a,1),310(a,1,1,2,1)),rewrite([310(5)]),flip(a)].
778
((x \ y) / (x \ y)) * z = (x * ((y * x) \ y)) * z. [para(341(a,1),697(a,1,1)),flip(a)].
812
x * ((x * (x / x)) \ y) = y. [para(701(a,1),3(a,1))].
820
(x / x) * (x * y) = x * ((x / x) \ y).
[para(701(a,1),24(a,1)),rewrite([206(6)]),flip(a)].
832
(x / x) \ (x * y) = x * ((x / x) * y).
[para(701(a,1),200(a,1,2)),rewrite([206(5)])].
853
x * ((x / x) \ ((x * x) \ y)) = x \ y.
[back_rewrite(712),rewrite([820(5)])].
854
x * (x * ((x / x) \ y)) = (x * x) * y.
[back_rewrite(700),rewrite([820(3)])].
857
(x * (y \ y)) * z = (x * (y / y)) * z.
[para(756(a,1),5(a,1,1,1)),rewrite([759(10)]),flip(a)].
862
(x \ x) \ y = (x / x) \ y. [para(756(a,1),205(a,1,2)),flip(a)].
864
(x / x) * ((x * x) * y) = x * (x * y).
[para(756(a,1),16(a,1,2,2)),rewrite([701(4),862(7),24(8),206(6),820(6),854(7)]),flip(a)].
872
((x * x) / (x * x)) * y = (x / x) * y.
[back_rewrite(776),rewrite([862(2),206(2),697(2)]),flip(a)].
879
((x * x) * (x / x)) * y = x * (x * ((x / x) * y)). [back_rewrite(748),rewrite([864(6)]),flip(a)].
891
x * ((x / x) \ (x \ y)) = (x / x) * y.
[para(288(a,1),812(a,1,2)),rewrite([206(3)])].
904
(x / x) * ((y * (x \ x)) \ z) = (x / x) * ((y * (x / x)) \ z). [para(862(a,1),341(a,1,1)),rewrite([862(4),341(5),697(10)]),flip(a)].
905
(x / x) \ (x \ y) = x * ((x * x) \ y).
[para(862(a,1),341(a,1))].
906
((x \ y) / (x \ y)) \ z = (x * ((y * x) \ y)) \ z. [para(341(a,1),862(a,1,1)),flip(a)].
910
x * (x * ((x * x) \ y)) = (x / x) * y.
[back_rewrite(891),rewrite([905(3)])].
1012
((x / x) / (x / x)) * y = (x * ((x * x) \ x)) * y. [para(777(a,1),697(a,1)),rewrite([862(3),697(4),778(8)])].
1055
(x * ((x * x) \ x)) * ((x / x) * y) = (x / x) * ((x * ((x * x) \ x)) \ y). [para(697(a,1),820(a,1,2)),rewrite([778(6),906(11),697(12)])].
1200
(x / x) * ((x * ((x * x) \ x)) \ (((x / x) * (x \ x)) \ y)) = (x / x) \ y. [para(853(a,1),697(a,1)),rewrite([862(2),697(9),906(11)]),flip(a)].
1211
(x * x) * x = x * (x * x). [para(206(a,1),854(a,1,2,2)),flip(a)].
1231
x * (x * (x * ((x / x) * y))) = (x * x) * (x * y). [para(832(a,1),854(a,1,2,2))].
1314
((x * y) * (y / y)) * z = (y * ((y \ x) * y)) * z. [para(24(a,1),857(a,1,1)),flip(a)].
1329
(x * ((y * y) / (y * y))) * z = (x * (y / y)) * z. [para(288(a,1),857(a,1,1,2)),rewrite([862(2),206(2),857(3)]),flip(a)].
1352
x * (x * ((x / x) * y)) = (x * x) * y.
[back_rewrite(879),rewrite([1314(4),697(2),2(2)]),flip(a)].
1354
(x * x) * (x * y) = x * ((x * x) * y).
[back_rewrite(1231),rewrite([1352(4)]),flip(a)].
1377
(x * ((x * x) \ x)) * (((x / x) * (x / x)) * y) = (x / x) * ((x / x) * y). [para(697(a,1),864(a,1,2,1)),rewrite([857(7),778(8),697(11),697(12)])].
1397
((x / x) * (x / x)) * y = (x / x) * y.
[para(194(a,1),872(a,1,1,1)),rewrite([194(8),778(8),194(3),862(4),905(4),910(5),778(10),2(6),3(7)])].
1418
(x / x) * ((((x * x) / (x * x)) / ((x * x) / (x * x))) \ y) = (x * ((x / x) * ((x
* x) \ x))) * ((x / x) * y). [para(872(a,1),820(a,1,2)),rewrite([1012(10),1354(4),1211(3),352(6),1211(3),205(4),24(5),697(4),872(20)]),flip(a)].
1425
((x * ((x * x) \ x)) * (x / x)) * y = (x / x) * y. [para(872(a,1),854(a,1,2)),rewrite([1418(13),872(12),14(10),701(5),872(13),1329(12),1397(10)])].
1433
(x / x) * ((x * ((x * x) \ x)) \ y) = (x / x) * ((x / x) * y). [back_rewrite(1377),rewrite([1397(7),1055(6)])].
1440
(x * ((x * x) \ x)) * y = (x / x) \ y.
[back_rewrite(1200),rewrite([1433(10),904(7),910(8),1012(4)])].
1442
(x / x) \ y = (x / x) * y. [back_rewrite(1425),rewrite([1440(5),697(4),1012(4),1440(4)])].
1543
(x \ x) \ y = (x / x) * y. [back_rewrite(862),rewrite([1442(4)])].
1546
(x / x) * (x * y) = x * ((x / x) * y).
[back_rewrite(820),rewrite([1442(5)])].
7018
((x * y) / y) * z = x * z. [para(3(a,1),505(a,1,1)),rewrite([3(5)])].
7224
x * (((x * y) / y) \ z) = z. [para(7018(a,1),3(a,1))].
7242
((x \ y) / y) * z = x \ z. [para(194(a,1),7018(a,1,1,1)),rewrite([194(6)])].
7448
((x * y) / y) \ z = x \ z. [para(7224(a,1),205(a,1,2)),flip(a)].
7452
(x \ (x / ((x * y) / y))) * z = x \ z.
[para(7224(a,1),204(a,1,2)),rewrite([7448(3),7448(7)]),flip(a)].
7880
(x / y) \ z = (y / x) * z. [para(206(a,1),7242(a,1,1,1)),flip(a)].
9580
x * (((x / ((x * y) / y)) * x) \ z) = z.
[para(7452(a,1),205(a,1,2)),rewrite([341(6)])].
9594
x \ ((x \ (y \ (y / ((y * z) / z)))) \ u) = (y \ x) \ (x * u). [para(7452(a,1),288(a,1,1)),flip(a)].
9627
(x / ((x * y) / y)) * z = (x / x) * z.
[para(7452(a,1),910(a,1,2,2,1)),rewrite([7452(15),9594(11),1543(7),1546(7),7452(8),205(4),778(12),9580(11)]),flip(a)].
12426
(x / x) * ((x * y) / y) = x. [para(9627(a,1),2(a,1))].
12623
(x * y) / y = x. [para(12426(a,1),205(a,1,2)),rewrite([7880(2),2(2)]),flip(a)].
12624
$F. [resolve(12623,a,6,a)].
==============================
end of proof ==========================
%
Length of proof is 16.
%
Level of proof is 10.
%
Maximum clause weight is 15.
%
Given clauses 21.
1
x \ (x * y) = y # label(non_clause) #
label(goal). [goal].
2
(x / y) * y = x. [assumption].
3
x * (x \ y) = y. [assumption].
4
x * (y * (x * z)) = ((x * y) * x) * z.
[assumption].
5
((x * y) * x) * z = x * (y * (x * z)).
[copy(4),flip(a)].
6
c1 \ (c1 * c2) != c2. [deny(1)].
9
x * ((x \ y) * (x * z)) = (y * x) * z.
[para(3(a,1),5(a,1,1,1)),flip(a)].
24
(x * y) * (y \ z) = y * ((y \ x) * z). [para(3(a,1),9(a,1,2,2)),flip(a)].
40
x * ((x \ (y / x)) * z) = y * (x \ z).
[para(2(a,1),24(a,1,1)),flip(a)].
81
x * (y \ ((y \ (x / y)) \ z)) = y * z.
[para(3(a,1),40(a,1,2)),flip(a)].
84
x * (y \ (y * z)) = x * z. [para(40(a,1),5(a,2)),rewrite([3(3),2(2)]),flip(a)].
163
(x \ (x / x)) \ y = x * y. [para(81(a,1),3(a,1)),flip(a)].
172
(x \ (x / x)) * (x * y) = y. [para(163(a,1),3(a,1,2))].
194
(x \ (x / x)) * y = x \ y. [para(3(a,1),172(a,1,2))].
205
x \ (x * y) = y. [para(172(a,1),84(a,2)),rewrite([84(6),194(4)])].
206
$F. [resolve(205,a,6,a)].
==============================
end of proof ==========================
The proofs for (B) are dual to the proofs for (A), and
the proofs for (D) are dual to the proofs for (C). Thus, we have shown that divisible
groupoids satisfying any one of (A), (B), (C), or (D)
are, in fact, quasigroups. Thus, by KunenŐs result, they are Moufang
loops.