============================== NewAuto =============================== NewAuto (32) version April-2007, April 2007. Process 32200 was started by ??? on pengy, Mon May 21 11:37:16 2007 The command was "/nfs/faculty/veroff/PROVER/LADR/provers.src/newauto -f newauto.in3". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file newauto.in3 lex([1,A,B,C,D,\,/,*,i]). assign(order,kbo). set(lex_order_vars). clear(auto_denials). assign(sos_limit,75000). assign(max_megs,950). clear(print_given). formulas(sos). 1 * x = x. x * 1 = x. x * (x \ y) = y. x \ (x * y) = y. (x * y) / y = x. (x / y) * y = x. ((x * y) / x) * (x * z) = x * (y * z) # label(LCC). (z * x) * (x \ (y * x)) = (z * y) * x # label(RCC). end_of_list. formulas(sos). A * (B * ((D * C) \ (C * D))) != (A * B) * ((D * C) \ (C * D)) # label("orig"). end_of_list. formulas(extra_assumptions). x * (y * ((z * z) \ (z * z))) = (x * y) * ((z * z) \ (z * z)) # label("DC"). x * (z * ((w * z) \ (z * w))) = (x * z) * ((w * z) \ (z * w)) # label("BC"). x * (y * ((y * z) \ (z * y))) = (x * y) * ((y * z) \ (z * y)) # label("DB"). w * (y * ((w * z) \ (z * w))) = (w * y) * ((w * z) \ (z * w)) # label("AD"). x * (y * ((w * x) \ (x * w))) = (x * y) * ((w * x) \ (x * w)) # label("CA"). x * (x * ((w * z) \ (z * w))) = (x * x) * ((w * z) \ (z * w)) # label("BA"). i(x) = x \ 1. i(x) = 1 / x. x * i(x) = 1. i(x) * x = 1. y * i(x * y) = i(x). i(y * x) * y = i(x). y * ((x * y) \ 1) = x \ 1. (1 / (y * x)) * y = 1 / x. end_of_list. formulas(hints). x * (y * ((w * z) \ (z * w))) = (x * y) * ((w * z) \ (z * w)) # label("orig"). end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: ============================== end of process non-clausal formulas === *********************************************** AUTO SKETCHES ITERATION 1 *********************************************** Starting a search with 14 assumptions: formulas(assumptions_active). x * (y * ((z * z) \ (z * z))) = (x * y) * ((z * z) \ (z * z)) # label("DC"). [assumption]. x * (y * ((z * y) \ (y * z))) = (x * y) * ((z * y) \ (y * z)) # label("BC"). [assumption]. x * (y * ((y * z) \ (z * y))) = (x * y) * ((y * z) \ (z * y)) # label("DB"). [assumption]. x * (y * ((x * z) \ (z * x))) = (x * y) * ((x * z) \ (z * x)) # label("AD"). [assumption]. x * (y * ((z * x) \ (x * z))) = (x * y) * ((z * x) \ (x * z)) # label("CA"). [assumption]. x * (x * ((y * z) \ (z * y))) = (x * x) * ((y * z) \ (z * y)) # label("BA"). [assumption]. i(x) = x \ 1. [assumption]. i(x) = 1 / x. [assumption]. x * i(x) = 1. [assumption]. i(x) * x = 1. [assumption]. x * i(y * x) = i(y). [assumption]. i(x * y) * x = i(y). [assumption]. x * ((y * x) \ 1) = y \ 1. [assumption]. (1 / (x * y)) * x = 1 / y. [assumption]. end_of_list. Child search process 32201 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). 1 * x = x. [assumption]. x * 1 = x. [assumption]. x * (x \ y) = y. [assumption]. x \ (x * y) = y. [assumption]. (x * y) / y = x. [assumption]. (x / y) * y = x. [assumption]. ((x * y) / x) * (x * z) = x * (y * z) # label(LCC). [assumption]. (x * y) * (y \ (z * y)) = (x * z) * y # label(RCC). [assumption]. A * (B * ((D * C) \ (C * D))) != (A * B) * ((D * C) \ (C * D)) # label("orig"). [assumption]. x * (y * ((z * z) \ (z * z))) = (x * y) * ((z * z) \ (z * z)) # label("DC"). [assumption]. x * (y * ((z * y) \ (y * z))) = (x * y) * ((z * y) \ (y * z)) # label("BC"). [assumption]. x * (y * ((y * z) \ (z * y))) = (x * y) * ((y * z) \ (z * y)) # label("DB"). [assumption]. x * (y * ((x * z) \ (z * x))) = (x * y) * ((x * z) \ (z * x)) # label("AD"). [assumption]. x * (y * ((z * x) \ (x * z))) = (x * y) * ((z * x) \ (x * z)) # label("CA"). [assumption]. x * (x * ((y * z) \ (z * y))) = (x * x) * ((y * z) \ (z * y)) # label("BA"). [assumption]. i(x) = x \ 1. [assumption]. i(x) = 1 / x. [assumption]. x * i(x) = 1. [assumption]. i(x) * x = 1. [assumption]. x * i(y * x) = i(y). [assumption]. i(x * y) * x = i(y). [assumption]. x * ((y * x) \ 1) = y \ 1. [assumption]. (1 / (x * y)) * x = 1 / y. [assumption]. end_of_list. formulas(demodulators). end_of_list. % 1 hints input. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Term ordering decisions: Function symbol KB weights: 1=1. A=1. B=1. C=1. D=1. \=1. /=1. *=1. i=1. Relation symbol precedence: lex([ = ]). Function symbol precedence: lex([ 1, A, B, C, D, \, /, *, i ]). Skipping inverse_order, because there is a lex command. Skipping unfold_eq, becaure there is a lex command. Auto_inference settings: % set(paramodulation). % (positive equality literals) % set(paramodulation) -> set(back_demod). Auto_process settings: (no changes). ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). end_of_list. formulas(sos). 1 1 * x = x. [assumption]. 2 x * 1 = x. [assumption]. 3 x * (x \ y) = y. [assumption]. 4 x \ (x * y) = y. [assumption]. 5 (x * y) / y = x. [assumption]. 6 (x / y) * y = x. [assumption]. 7 ((x * y) / x) * (x * z) = x * (y * z) # label(LCC). [assumption]. 8 (x * y) * (y \ (z * y)) = (x * z) * y # label(RCC). [assumption]. 10 (A * B) * ((D * C) \ (C * D)) != A * (B * ((D * C) \ (C * D))). [copy(9),flip(a)]. 12 (x * y) * ((z * z) \ (z * z)) = x * (y * ((z * z) \ (z * z))). [copy(11),flip(a)]. 14 (x * y) * ((z * y) \ (y * z)) = x * (y * ((z * y) \ (y * z))). [copy(13),flip(a)]. 16 (x * y) * ((y * z) \ (z * y)) = x * (y * ((y * z) \ (z * y))). [copy(15),flip(a)]. 18 (x * y) * ((x * z) \ (z * x)) = x * (y * ((x * z) \ (z * x))). [copy(17),flip(a)]. 20 (x * y) * ((z * x) \ (x * z)) = x * (y * ((z * x) \ (x * z))). [copy(19),flip(a)]. 22 (x * x) * ((y * z) \ (z * y)) = x * (x * ((y * z) \ (z * y))). [copy(21),flip(a)]. 24 x \ 1 = i(x). [copy(23),flip(a)]. 26 1 / x = i(x). [copy(25),flip(a)]. 27 x * i(x) = 1. [assumption]. 28 i(x) * x = 1. [assumption]. 29 x * i(y * x) = i(y). [assumption]. 30 i(x * y) * x = i(y). [assumption]. end_of_list. formulas(demodulators). 1 1 * x = x. [assumption]. 2 x * 1 = x. [assumption]. 3 x * (x \ y) = y. [assumption]. 4 x \ (x * y) = y. [assumption]. 5 (x * y) / y = x. [assumption]. 6 (x / y) * y = x. [assumption]. 7 ((x * y) / x) * (x * z) = x * (y * z) # label(LCC). [assumption]. 8 (x * y) * (y \ (z * y)) = (x * z) * y # label(RCC). [assumption]. 12 (x * y) * ((z * z) \ (z * z)) = x * (y * ((z * z) \ (z * z))). [copy(11),flip(a)]. 14 (x * y) * ((z * y) \ (y * z)) = x * (y * ((z * y) \ (y * z))). [copy(13),flip(a)]. 16 (x * y) * ((y * z) \ (z * y)) = x * (y * ((y * z) \ (z * y))). [copy(15),flip(a)]. 18 (x * y) * ((x * z) \ (z * x)) = x * (y * ((x * z) \ (z * x))). [copy(17),flip(a)]. 20 (x * y) * ((z * x) \ (x * z)) = x * (y * ((z * x) \ (x * z))). [copy(19),flip(a)]. 22 (x * x) * ((y * z) \ (z * y)) = x * (x * ((y * z) \ (z * y))). [copy(21),flip(a)]. 24 x \ 1 = i(x). [copy(23),flip(a)]. 26 1 / x = i(x). [copy(25),flip(a)]. 27 x * i(x) = 1. [assumption]. 28 i(x) * x = 1. [assumption]. 29 x * i(y * x) = i(y). [assumption]. 30 i(x * y) * x = i(y). [assumption]. end_of_list. % 1 hints processed (0 are redundant). ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. NOTE: Back_subsumption disabled, ratio of kept to back_subsumed is 113 (0.00 of 37.23 sec). Low Water (keep, True_semantics): wt=98 Low Water (keep, True_semantics): wt=95 Low Water (keep, True_semantics): wt=91 Low Water (keep, True_semantics): wt=83 Low Water (keep, True_semantics): wt=79 Low Water (keep, True_semantics): wt=75 Low Water (keep, True_semantics): wt=73 Low Water (keep, True_semantics): wt=71 Low Water (keep, True_semantics): wt=67 Low Water (keep, True_semantics): wt=65 Low Water (keep, True_semantics): wt=63 Low Water (keep, True_semantics): wt=61 Low Water (keep, True_semantics): wt=59 Low Water (keep, True_semantics): wt=57 Low Water (keep, True_semantics): wt=55 Low Water (keep, True_semantics): wt=54 Low Water (keep, True_semantics): wt=52 Low Water (keep, True_semantics): wt=51 Low Water (keep, True_semantics): wt=49 Low Water (keep, True_semantics): wt=47 Low Water (keep, True_semantics): wt=45 Low Water (keep, True_semantics): wt=44 Low Water (keep, True_semantics): wt=43 Low Water (keep, True_semantics): wt=41 Low Water (keep, True_semantics): wt=40 Low Water (keep, True_semantics): wt=39 Low Water (keep, True_semantics): wt=38 Low Water (keep, True_semantics): wt=37 Low Water (keep, True_semantics): wt=36 Low Water (keep, True_semantics): wt=35 Low Water (keep, True_semantics): wt=34 Low Water (keep, True_semantics): wt=33 Low Water (keep, True_semantics): wt=32 Low Water (keep, True_semantics): wt=31 Low Water (keep, True_semantics): wt=30 Low Water (keep, True_semantics): wt=29 Low Water (keep, True_semantics): wt=28 Low Water (keep, True_semantics): wt=27 Low Water (keep, True_semantics): wt=26 Low Water (keep, True_semantics): wt=25 Low Water (keep, True_semantics): wt=24 Low Water (keep, True_semantics): wt=23 Demod_limit (see stdout) Demod_limit: (x \ ((((x * x) * y) / (x * (x * (x * (x * (x * x)))))) * i(x))) \ (i(x) \ x) = (y / ((((x * (x * (x * x))) * x) * x) * x)) \ x. [para(24031(a,1),153140(a,2,2)),rewrite(7291(4),817(2),7291(5),7291(3),7291(6),7291(4),817(2),7291(10),817(8),7291(11),7291(9),7291(12),7291(10),817(8),144944(13),198556(13),78742(12),818(11),817(10),45623(13),78742(12),818(11),818(10),818(9),817(8),144944(14),78742(13),145300(12),198556(14),78742(13),145300(12),35847(6),62344(12),219325(8),1732(5),1732(6),950(5),1732(7),3501(6),854(4),78742(6),145300(5),817(4),45623(5),3501(10),1732(8),3501(7),81924(5),3501(5),78742(7),818(6),817(5),219325(7),1732(4),1732(5),1732(6),78742(10),157879(9),817(4),112848(6),817(8),48367(9),1732(6),4803(5),1732(7),3501(6),191016(6),854(5),1732(8),3501(7),1732(5),78742(7),145300(6),145300(5),817(4),45623(5),174552(6),3932(6),950(5),1732(11),3501(10),1732(8),3501(7),1732(5),78742(7),145300(6),145300(5),4803(5),3501(6),191016(6),854(5),78742(10),199982(9),1732(5),1732(6),145300(7),817(4),220895(7),817(5),78742(9),81924(8),3932(6),3932(7),45625(6),854(4),3501(5),3501(8),81924(6),3501(6),191016(6),854(5),78742(8),145300(7),817(4),107510(7),3932(4),3501(6),854(4),78742(6),145300(5),817(4),45623(5),107510(14),3932(11),3501(10),1732(8),3501(7),1732(5),174552(4),3932(4),950(3),78742(7),145300(6),817(2),107510(6),3932(3),3501(5),854(3),78742(5),145300(4),817(2),220895(4),817(2),78742(10),199982(9),161379(5),1732(3),3501(5),854(3),78742(5),145300(4),817(3),45623(4),1732(6),174552(5),3932(5),950(4),199982(7),854(3),1732(4),48467(5),817(2),75888(4),42662(3),1744(5),168014(4),817(3),48367(4),78742(7),202372(6),145300(4),145300(3),817(2),45623(3),174552(4),3932(4),950(3),78742(6),145300(5),817(2),228602(5),145300(3),4803(3),78742(9),199982(8),1732(4),1732(5),950(4),145300(6),817(2),107510(6),3932(3),3501(5),854(3),78742(5),145300(4),817(2),220895(4),817(2),78742(8),145300(7),817(2),228602(7),81924(5),3932(3),3932(4),45625(3),3501(5),854(3),78742(5),145300(4),817(2),241706(4),854(3),3932(4),3501(3),3501(13),1732(11),3501(10),1732(8),3501(7),1732(5),78541(4),17481(4),1732(3),78742(7),157879(6),817(2),42662(3),817(5),17481(6),4803(3),1732(5),3501(4),191016(4),854(3),78742(10),199982(9),1732(5),3501(4),1732(6),78541(5),17481(5),1732(4),145300(7),817(2),107510(7),3932(4),3501(6),854(4),78742(6),145300(5),817(2),220895(5),817(3),78742(9),145300(8),817(2),228602(8),81924(6),3932(4),3932(5),45625(4),854(2),3501(3),3501(6),81924(4),3501(4),191016(4),854(3),78742(6),145300(5),817(2),107510(5),3932(2),3501(4),854(2),78742(4),145300(3),817(2),45623(3),78742(13),199982(12),1732(8),3501(7),1732(5),78541(4),78742(7),81924(6),3932(4),3932(5),45625(4),3501(6),854(4),78742(6),145300(5),817(3),241706(5),854(4),3932(5),3501(4),1732(9),3501(8),1732(6),78541(5),17481(5),1732(4),78742(8),157879(7),817(3),42662(4),817(6),17481(7),4803(4),1732(6),3501(5),191016(5),854(4),199982(10),1732(6),3501(5),1732(3),78742(5),145300(4),4803(4),1732(7),3501(6),1732(4),78742(6),42569(5),817(3),42662(4),176563(5),2615(4),199982(8),818(6),818(5),818(4),818(3),191016(8),4480(6),818(5),35847(4),1732(7),1744(6),4480(5),818(4),818(3),78742(10),141549(9),176563(5),2615(4),141549(7),42606(5),817(2),112861(4),817(2),145582(5),17481(4),1732(3),78742(7),157879(6),817(2),42662(3),817(5),17481(6),4803(3),1732(5),3501(4),191016(4),854(3),78742(9),199982(8),1732(4),1732(5),2615(4),145300(6),817(2),228602(6),818(4),818(3),78742(8),145300(7),817(2),219221(7),42663(5),42662(3),142967(5),1744(3),1732(6),3501(5),854(3),78742(5),145300(4),817(2),228602(4),78742(12),199982(11),1732(7),3501(6),142967(6),1744(4),1732(8),3501(7),1732(5),2615(4),78742(7),145300(6),817(3),241706(6),854(5),3932(6),3501(5),191016(5),854(4),199982(9),1732(5),3501(4),1732(6),78541(5),17481(5),1732(4),145300(7),817(2),107510(7),3932(4),3501(6),854(4),78742(6),145300(5),817(2),220895(5),817(3),78742(9),145300(8),817(2),228602(8),81924(6),3932(4),3932(5),45625(4),854(2),3501(3),3501(6),81924(4),3501(4),191016(4),854(3),78742(6),145300(5),817(2),107510(5),3932(2),3501(4),854(2),78742(4),145300(3),817(2),45623(3),78742(11),199982(10),1732(6),174552(5),3932(5),950(4),1732(7),3501(6),1732(4),78742(6),145300(5),145300(4),4803(4),3501(5),191016(5),854(4),199982(8),1732(4),1732(5),2615(4),145300(6),817(2),228602(6),818(4),818(3),78742(8),145300(7),817(2),219221(7),42663(5),42662(3),142967(5),1744(3),1732(6),3501(5),854(3),78742(5),145300(4),817(2),228602(4),78742(10),199982(9),1732(5),4803(4),1732(6),3501(5),191016(5),854(4),199982(7),1732(3),1732(4),145300(5),817(2),220895(5),817(3),78742(7),81924(6),3932(4),3932(5),45625(4),854(2),3501(3),3501(6),81924(4),3501(4),191016(4),854(3),78742(6),145300(5),817(2),107510(5),3932(2),3501(4),854(2),78742(4),145300(3),817(2),45623(3),78742(9),199982(8),81924(4),3501(4),81924(5),3501(5),191016(5),854(4),199982(6),818(4),818(3),191016(6),168014(4),817(3),48367(4),1732(5),1744(4),4480(3),78742(8),145300(7),817(2),107510(7),3932(4),4803(3),3501(6),1732(4),4480(3),78742(6),157731(5),145300(3),817(2),45623(3),78742(5),854(4),3932(3),3932(4),45625(3),3709(21),106281(20),818(18),817(17),818(19),818(18),818(17),817(16),233886(22),203(14),594(14),1732(12),3501(11),1732(9),3501(8),1732(6),3501(5),854(3),78742(5),145300(4),817(2),241706(4),854(3),3932(4),3501(3),78742(8),145603(7),4803(4),145300(5),817(2),228602(5),818(3),78742(7),212581(6),3932(3),78742(5),145300(4),145300(3),4803(3),3501(4),191016(4),854(3),3501(6),1732(4),3501(3),78742(6),854(5),3932(4),3932(5),45625(4),1744(3),78742(11),199982(10),1732(6),45625(5),1732(3),45625(4),1732(7),3501(6),854(4),78742(6),145300(5),817(3),241706(5),854(4),3932(5),3501(4),145300(8),817(2),107510(8),3932(5),78541(4),17481(4),1732(3),3501(7),1732(5),45625(4),854(2),3501(3),78742(7),145300(6),817(2),45623(6),78742(5),818(4),817(3),219325(5),1732(2),1732(3),1732(4),78742(10),199982(9),854(5),1732(6),45625(5),854(3),3501(4),145603(7),4803(4),145300(5),817(2),228602(5),818(3),78742(7),212581(6),3932(3),78742(5),145300(4),145300(3),4803(3),3501(4),191016(4),854(3),3501(6),1732(4),3501(3),78742(6),854(5),3932(4),3932(5),45625(4),1744(3),78742(9),199982(8),854(4),1732(5),3501(4),145300(6),817(2),45623(6),78742(5),818(4),817(3),219325(5),1732(2),1732(3),1732(4),78742(8),157879(7),817(2),112848(4),817(6),48367(7),1732(4),4803(3),1732(5),3501(4),191016(4),854(3),1732(6),3501(5),1732(3),78742(5),145300(4),145300(3),817(2),45623(3),174552(4),3932(4),950(3),845(14),3501(12),1732(10),3501(9),1732(7),3501(6),1732(4),45625(3),78742(6),42606(5),817(2),112861(4),817(2),145582(5),17481(4),1732(3),78742(9),199982(8),854(4),1732(5),45625(4),143122(6),35847(4),191016(6),4480(4),818(3),1732(5),176563(4),2615(3),78742(8),141549(7),42606(5),817(2),112861(4),817(2),145582(5),17481(4),1732(3),78742(7),157879(6),817(2),42662(3),817(5),17481(6),4803(3),1732(5),3501(4),191016(4),854(3),78742(12),199982(11),1732(7),3501(6),1732(4),78742(6),145300(5),145300(4),817(3),45623(4),174552(5),3932(5),950(4),1732(8),3501(7),1732(5),45625(4),78742(7),42606(6),817(3),112861(5),817(3),145582(6),17481(5),1732(4),199982(9),1732(5),1732(6),24623(5),145300(7),817(2),45623(7),78742(6),818(5),818(4),818(3),817(2),78742(9),145300(8),78742(11),145300(10),35847(4),62344(10),219325(6),1732(3),1732(4),950(3),1732(5),3501(4),854(2),78742(4),145300(3),817(2),45623(3),3501(8),1732(6),3501(5),81924(3),3501(3),78742(5),818(4),817(3),219325(5),1732(2),1732(3),1732(4),78742(8),157879(7),817(2),112848(4),817(6),48367(7),1732(4),4803(3),1732(5),3501(4),191016(4),854(3),1732(6),3501(5),1732(3),78742(5),145300(4),145300(3),817(2),45623(3),174552(4),3932(4),950(3),1732(9),3501(8),1732(6),3501(5),1732(3),78742(5),145300(4),145300(3),4803(3),3501(4),191016(4),854(3),78742(8),199982(7),1732(3),1732(4),145300(5),817(2),220895(5),817(3),78742(7),81924(6),3932(4),3932(5),45625(4),854(2),3501(3),3501(6),81924(4),3501(4),191016(4),854(3),78742(6),145300(5),817(2),107510(5),3932(2),3501(4),854(2),78742(4),145300(3),817(2),45623(3),4297(18),818(17),818(16),818(15),817(14),233886(18),203(12),594(12),1732(10),3501(9),1732(7),3501(6),1732(4),78541(3),78742(6),81924(5),3932(3),3932(4),45625(3),3501(5),854(3),78742(5),145300(4),817(2),241706(4),854(3),3932(4),3501(3),78742(9),145300(8),817(2),107510(8),3932(5),78541(4),17481(4),1732(3),3501(7),1732(5),45625(4),854(2),3501(3),78742(7),145300(6),817(2),45623(6),78742(5),818(4),817(3),219325(5),1732(2),1732(3),1732(4),845(12),3501(10),1732(8),3501(7),1732(5),24623(4),78742(7),223955(6),178688(5),3932(6),145582(5),17481(4),1732(3),78742(10),199982(9),1732(5),1732(6),24623(5),145300(7),817(2),45623(7),78742(6),818(5),818(4),818(3),817(2),78742(9),145300(8),4297(14),818(13),817(12),233886(14),203(10))]. Demod_limit (steps=0, size=45). The most recent kept clause is 250329. From here on, a short message will be printed for each 100 times the limit is hit. -------- Proof 1 -------- ============================== PROOF ================================= % Proof 1 at 1044.07 (+ 4.26) seconds. % Length of proof is 2505. % Level of proof is 76. % Maximum clause weight is 49. % Given clauses 3809. 1 1 * x = x. [assumption]. 2 x * 1 = x. [assumption]. 3 x * (x \ y) = y. [assumption]. 4 x \ (x * y) = y. [assumption]. 5 (x * y) / y = x. [assumption]. 6 (x / y) * y = x. [assumption]. 7 ((x * y) / x) * (x * z) = x * (y * z) # label(LCC). [assumption]. 8 (x * y) * (y \ (z * y)) = (x * z) * y # label(RCC). [assumption]. 9 A * (B * ((D * C) \ (C * D))) != (A * B) * ((D * C) \ (C * D)) # label("orig"). [assumption]. 10 (A * B) * ((D * C) \ (C * D)) != A * (B * ((D * C) \ (C * D))). [copy(9),flip(a)]. 13 x * (y * ((z * y) \ (y * z))) = (x * y) * ((z * y) \ (y * z)) # label("BC"). [assumption]. 14 (x * y) * ((z * y) \ (y * z)) = x * (y * ((z * y) \ (y * z))). [copy(13),flip(a)]. 15 x * (y * ((y * z) \ (z * y))) = (x * y) * ((y * z) \ (z * y)) # label("DB"). [assumption]. 16 (x * y) * ((y * z) \ (z * y)) = x * (y * ((y * z) \ (z * y))). [copy(15),flip(a)]. 17 x * (y * ((x * z) \ (z * x))) = (x * y) * ((x * z) \ (z * x)) # label("AD"). [assumption]. 18 (x * y) * ((x * z) \ (z * x)) = x * (y * ((x * z) \ (z * x))). [copy(17),flip(a)]. 19 x * (y * ((z * x) \ (x * z))) = (x * y) * ((z * x) \ (x * z)) # label("CA"). [assumption]. 20 (x * y) * ((z * x) \ (x * z)) = x * (y * ((z * x) \ (x * z))). [copy(19),flip(a)]. 21 x * (x * ((y * z) \ (z * y))) = (x * x) * ((y * z) \ (z * y)) # label("BA"). [assumption]. 22 (x * x) * ((y * z) \ (z * y)) = x * (x * ((y * z) \ (z * y))). [copy(21),flip(a)]. 23 i(x) = x \ 1. [assumption]. 24 x \ 1 = i(x). [copy(23),flip(a)]. 25 i(x) = 1 / x. [assumption]. 26 1 / x = i(x). [copy(25),flip(a)]. 27 x * i(x) = 1. [assumption]. 28 i(x) * x = 1. [assumption]. 29 x * i(y * x) = i(y). [assumption]. 33 1 \ x = x. [para(3(a,1),1(a,1)),flip(a)]. 34 x \ x = 1. [para(2(a,1),4(a,1,2))]. 35 x / x = 1. [para(1(a,1),5(a,1,1))]. 36 x / 1 = x. [para(2(a,1),5(a,1,1))]. 37 x / (y \ x) = y. [para(3(a,1),5(a,1,1))]. 38 (x / y) \ x = y. [para(6(a,1),4(a,1,2))]. 39 (x / y) * (y * z) = y * ((y \ x) * z). [para(3(a,1),7(a,1,1,1))]. 40 ((x * y) / x) * z = x * (y * (x \ z)). [para(3(a,1),7(a,1,2))]. 41 ((x * y) / x) \ (x * (y * z)) = x * z. [para(7(a,1),4(a,1,2))]. 42 (x * (y * z)) / (x * z) = (x * y) / x. [para(7(a,1),5(a,1,1))]. 46 x * ((y \ x) \ (z * (y \ x))) = (y * z) * (y \ x). [para(3(a,1),8(a,1,1))]. 47 (x * (y \ z)) * ((y \ z) \ z) = (x * y) * (y \ z). [para(3(a,1),8(a,1,2,2))]. 48 (x * y) \ ((x * z) * y) = y \ (z * y). [para(8(a,1),4(a,1,2))]. 49 ((x * y) * z) / (z \ (y * z)) = x * z. [para(8(a,1),5(a,1,1))]. 50 ((x / y) * z) * y = x * (y \ (z * y)). [para(6(a,1),8(a,1,1)),flip(a)]. 51 (x * (y / z)) * z = (x * z) * (z \ y). [para(6(a,1),8(a,1,2,2)),flip(a)]. 53 (x * (y \ (z * y))) * ((y \ (z * y)) \ ((u * z) * y)) = (x * (u * y)) * (y \ (z * y)). [para(8(a,1),8(a,1,2,2))]. 54 x * (y * ((x * y) \ (y * x))) = y * x. [para(14(a,1),3(a,1))]. 60 x * ((x \ y) * ((z * x) \ (x * z))) = y * ((z * x) \ (x * z)). [para(6(a,1),14(a,1,1)),rewrite(39(10)),flip(a)]. 76 x * ((x \ y) * ((x * z) \ (z * x))) = y * ((x * z) \ (z * x)). [para(6(a,1),16(a,1,1)),rewrite(39(10)),flip(a)]. 95 (x * y) \ (x * (y * ((x * z) \ (z * x)))) = (x * z) \ (z * x). [para(18(a,1),4(a,1,2))]. 96 (x * (y * ((x * z) \ (z * x)))) / ((x * z) \ (z * x)) = x * y. [para(18(a,1),5(a,1,1))]. 97 x * ((x \ y) * (((y / x) * z) \ (z * (y / x)))) = y * (((y / x) * z) \ (z * (y / x))). [para(6(a,1),18(a,1,1)),rewrite(39(14)),flip(a)]. 124 x * ((x \ y) * ((z * (y / x)) \ ((y / x) * z))) = y * ((z * (y / x)) \ ((y / x) * z)). [para(6(a,1),20(a,1,1)),rewrite(39(14)),flip(a)]. 156 (x * (x * ((y * z) \ (z * y)))) / ((y * z) \ (z * y)) = x * x. [para(22(a,1),5(a,1,1))]. 187 i(1) = 1. [para(27(a,1),1(a,1)),flip(a)]. 188 i(i(x)) = x. [para(27(a,1),5(a,1,1)),rewrite(26(3))]. 189 i(x) \ (y * i(x)) = (x * y) * i(x). [para(27(a,1),8(a,1,1)),rewrite(1(6))]. 190 (x * i(y)) * y = (x * y) * i(y). [para(27(a,1),8(a,1,2,2)),rewrite(24(5),188(4))]. 191 (x * i(x * y)) * (i(x * y) \ i(x)) = 1. [para(27(a,1),8(a,2)),rewrite(29(8))]. 196 (i(x) * y) * x = x \ (y * x). [para(28(a,1),8(a,1,1)),rewrite(1(4)),flip(a)]. 201 (x \ y) * i(y) = i(x). [para(3(a,1),29(a,1,2,1))]. 202 i(x * y) = y \ i(x). [para(29(a,1),4(a,1,2)),flip(a)]. 203 i(x / y) = y * i(x). [para(6(a,1),29(a,1,2,1)),flip(a)]. 204 (x \ (y * x)) * (x \ (y \ i(z))) = x \ i(z). [para(8(a,1),29(a,1,2,1)),rewrite(202(5),202(4),202(8))]. 210 (x \ i(y)) * y = i(x). [para(29(a,1),29(a,1,2,1)),rewrite(202(2),188(4))]. 211 (x * y) * (y \ i(x)) = 1. [back_rewrite(191),rewrite(202(2),202(5),47(8))]. 212 (x \ y) \ i(x) = i(y). [para(201(a,1),4(a,1,2))]. 214 i(x) * ((y * z) * i(y)) = ((x \ y) * z) * i(y). [para(201(a,1),8(a,1,1)),rewrite(189(5))]. 215 (x * i(y)) * (i(y) \ i(z)) = (x * (z \ y)) * i(y). [para(201(a,1),8(a,1,2,2))]. 216 (x \ y) * (i(y) * ((z * i(y)) \ (i(y) * z))) = i(x) * ((z * i(y)) \ (i(y) * z)). [para(201(a,1),14(a,1,1)),flip(a)]. 219 (x \ y) * (i(y) * ((i(y) * z) \ (z * i(y)))) = i(x) * ((i(y) * z) \ (z * i(y))). [para(201(a,1),16(a,1,1)),flip(a)]. 233 (x * ((y * z) \ (z * y))) \ i(y) = ((y * z) \ (z * y)) \ (x \ i(y)). [para(18(a,1),202(a,1,1)),rewrite(202(6),202(11))]. 238 (x \ (y * z)) * (z \ i(y)) = i(x). [para(202(a,1),201(a,1,2))]. 240 x * ((x \ y) * (x \ z)) = (y / x) * z. [para(3(a,1),39(a,1,2)),flip(a)]. 241 (x / y) \ (y * ((y \ x) * z)) = y * z. [para(39(a,1),4(a,1,2))]. 242 x * ((x \ (y * x)) * z) = y * (x * z). [para(5(a,1),39(a,1,1)),flip(a)]. 243 (x / y) * (((x / y) \ z) * y) = (z / (x / y)) * x. [para(6(a,1),39(a,1,2)),flip(a)]. 246 (x * y) * (((x * y) \ z) * (y \ (u * y))) = (z / (x * y)) * ((x * u) * y). [para(8(a,1),39(a,1,2)),flip(a)]. 266 i(x) * (x * y) = x * (i(x) * y). [para(24(a,1),39(a,2,2,1)),rewrite(26(2))]. 269 (x \ y) * (((x \ y) \ y) * z) = x * ((x \ y) * z). [para(37(a,1),39(a,1,1)),flip(a)]. 270 (x \ y) * (((x \ y) \ z) * i(y)) = (z / (x \ y)) * i(x). [para(201(a,1),39(a,1,2)),flip(a)]. 271 ((x \ y) * z) \ i(x) = (x * z) \ (x * i(y)). [para(39(a,1),202(a,1,1)),rewrite(202(4),203(7))]. 273 (x * i(y)) * (y / x) = 1. [para(203(a,1),28(a,1,1))]. 274 i(x) \ i(y) = x / y. [para(203(a,1),188(a,1,1)),rewrite(202(3))]. 275 (x \ (y / z)) * (z * i(y)) = i(x). [para(203(a,1),201(a,1,2))]. 276 (x * (y \ z)) * i(z) = (x * i(z)) * (z / y). [back_rewrite(215),rewrite(274(5)),flip(a)]. 277 i(x) / y = x \ i(y). [para(210(a,1),5(a,1,1))]. 278 ((x \ i(y)) * z) * y = i(x) * (y \ (z * y)). [para(210(a,1),8(a,1,1)),flip(a)]. 279 (x * (y \ i(z))) * z = (x * z) * (z \ i(y)). [para(210(a,1),8(a,1,2,2)),flip(a)]. 297 (x \ i(y)) * (((x \ i(y)) \ z) * y) = (z / (x \ i(y))) * i(x). [para(210(a,1),39(a,1,2)),flip(a)]. 298 (x \ (y * i(z))) * (z / y) = i(x). [para(203(a,1),210(a,1,1,2))]. 299 (i(x) \ y) \ x = i(y). [para(188(a,1),212(a,1,2))]. 300 i(x \ y) = i(y) * x. [para(212(a,1),201(a,1,1)),rewrite(188(3)),flip(a)]. 301 ((x * y) \ z) \ (y \ i(x)) = i(z). [para(202(a,1),212(a,1,2))]. 303 ((x / y) \ z) \ (y * i(x)) = i(z). [para(203(a,1),212(a,1,2))]. 304 i(x) * (x / y) = i(y). [para(274(a,1),3(a,1,2))]. 305 x / i(y) = i(x) \ y. [para(188(a,1),274(a,1,2)),flip(a)]. 306 (x \ i(y)) \ i(z) = (y * x) / z. [para(202(a,1),274(a,1,1))]. 307 i(x) \ (y \ i(z)) = x / (z * y). [para(202(a,1),274(a,1,2))]. 308 (x \ y) * (i(y) * z) = i(y) * ((y / x) * z). [para(274(a,1),39(a,2,2,1)),rewrite(305(3),188(2))]. 309 (x * i(y)) \ i(z) = (y / x) / z. [para(203(a,1),274(a,1,1))]. 310 i(x) \ (y * i(z)) = x / (z / y). [para(203(a,1),274(a,1,2))]. 315 i(x) * ((x / y) * ((i(x) * z) \ (z * i(x)))) = i(y) * ((i(x) * z) \ (z * i(x))). [back_rewrite(219),rewrite(308(9))]. 316 i(x) * ((x / y) * ((z * i(x)) \ (i(x) * z))) = i(y) * ((z * i(x)) \ (i(x) * z)). [back_rewrite(216),rewrite(308(9))]. 317 (x * y) * i(x) = x / (x / y). [back_rewrite(189),rewrite(310(4)),flip(a)]. 318 ((x \ y) * z) * i(y) = i(x) * (y / (y / z)). [back_rewrite(214),rewrite(317(4)),flip(a)]. 319 x * (y * i(x)) = (x * y) / x. [para(40(a,1),2(a,1)),rewrite(24(2))]. 320 x * (y * (x \ (((x * y) / x) \ z))) = z. [para(40(a,1),3(a,1))]. 321 (x * (y * (x \ z))) / z = (x * y) / x. [para(40(a,1),5(a,1,1))]. 322 x * ((x \ y) * ((y / x) \ z)) = (y / (y / x)) * z. [para(6(a,1),40(a,1,1,1)),rewrite(39(8)),flip(a)]. 327 (x * y) * ((z * (u * (z \ y))) \ (y * ((z * u) / z))) = x * (y * ((z * (u * (z \ y))) \ (y * ((z * u) / z)))). [para(40(a,1),14(a,1,2,1)),rewrite(40(12))]. 344 x * (i(x) * (x \ y)) = i(x) * y. [para(27(a,1),40(a,1,1,1)),rewrite(26(2)),flip(a)]. 347 (x * (y \ z)) \ i(y) = z \ (y * (x \ i(y))). [para(40(a,1),202(a,1,1)),rewrite(202(4),203(7),202(6))]. 350 (x \ i(y)) * (y * ((x \ i(y)) \ z)) = (x \ (y * x)) * z. [para(210(a,1),40(a,1,1,1)),rewrite(277(4),300(3),188(2)),flip(a)]. 352 ((x \ y) \ y) * i(z) = i(y) * (x * (y / z)). [para(274(a,1),40(a,2,2,2)),rewrite(305(4),202(3),188(2))]. 362 (x \ i(y)) / z = (y * x) \ i(z). [para(202(a,1),277(a,1,1))]. 363 (x \ i(y)) * (y * z) = y * ((y \ i(x)) * z). [para(277(a,1),39(a,1,1))]. 364 (x * i(y)) / z = (y / x) \ i(z). [para(203(a,1),277(a,1,1))]. 365 x * ((x \ i(y)) * ((y \ i(x)) \ z)) = (y \ (x * y)) * z. [back_rewrite(350),rewrite(363(7))]. 368 ((x \ i(y)) \ z) \ (y * x) = i(z). [para(202(a,1),299(a,1,1,1))]. 369 ((x * i(y)) \ z) \ (y / x) = i(z). [para(203(a,1),299(a,1,1,1))]. 370 (i(x) * y) * (y \ x) = 1. [para(300(a,1),28(a,1,1))]. 372 (x \ (i(y) * z)) * (z \ y) = i(x). [para(300(a,1),210(a,1,1,2))]. 374 (i(x) * y) \ i(z) = (y \ x) / z. [para(300(a,1),274(a,1,1))]. 375 i(x) \ (i(y) * z) = x / (z \ y). [para(300(a,1),274(a,1,2))]. 376 (i(x) * y) / z = (y \ x) \ i(z). [para(300(a,1),277(a,1,1))]. 377 ((i(x) * y) \ z) \ (y \ x) = i(z). [para(300(a,1),299(a,1,1,1))]. 384 (x * (y / z)) * ((y / z) \ i(z)) = (x * i(y)) * (y / z). [para(304(a,1),8(a,1,2,2))]. 387 (x * i(y)) * ((y / (y / z)) / z) = x * (i(y) * ((y / (y / z)) / z)). [para(304(a,1),14(a,1,2,2)),rewrite(309(7),304(13),309(12))]. 397 (x \ i(y)) * ((y * x) / z) = i(z). [para(202(a,1),304(a,1,1))]. 401 (i(x) * y) * ((y \ x) / z) = i(z). [para(300(a,1),304(a,1,1))]. 402 ((x * y) / x) \ (x * z) = x * (y \ z). [para(3(a,1),41(a,1,2,2))]. 403 (x / (x / y)) \ (y * ((y \ x) * z)) = (x / y) * z. [para(6(a,1),41(a,1,1,1)),rewrite(39(5))]. 412 ((x * y) / x) \ x = x * i(y). [para(27(a,1),41(a,1,2,2)),rewrite(2(4))]. 420 (x * y) \ (x * (z \ i(x))) = (z * y) \ i(x). [para(41(a,1),212(a,1,1)),rewrite(203(4),202(3),202(8))]. 423 (x \ y) \ (i(y) * ((y / x) * z)) = i(y) * z. [para(304(a,1),41(a,1,1,1)),rewrite(305(3),188(2))]. 426 x / (y \ i(z)) = i(x) \ (z * y). [para(202(a,1),305(a,1,2))]. 427 x / (y * i(z)) = i(x) \ (z / y). [para(203(a,1),305(a,1,2))]. 428 i(x) * (y * (i(x) \ z)) = ((y \ x) \ x) * z. [para(305(a,1),40(a,1,1)),rewrite(202(3),188(2)),flip(a)]. 429 x / (i(y) * z) = i(x) \ (z \ y). [para(300(a,1),305(a,1,2))]. 430 (x \ i(y)) * (((x \ i(y)) \ z) * y) = (i(z) \ (y * x)) * i(x). [back_rewrite(297),rewrite(426(10))]. 431 (x \ i(y)) \ (z * (x \ i(y))) = ((y * x) * z) * (x \ i(y)). [para(211(a,1),8(a,1,1)),rewrite(1(8))]. 432 (x * (y \ i(z))) * (z * y) = (x * (z * y)) * (y \ i(z)). [para(211(a,1),8(a,1,2,2)),rewrite(24(7),300(6),188(5))]. 446 ((x / y) * z) * (z \ (y * i(x))) = 1. [para(203(a,1),211(a,1,2,2))]. 458 (x * (y * i(z))) * ((z / y) / x) = 1. [para(203(a,1),273(a,1,1,2))]. 463 (x * (i(y) * z)) * (z \ y) = (x * (z \ y)) * (i(y) * z). [para(370(a,1),8(a,1,2,2)),rewrite(24(5),300(4)),flip(a)]. 471 ((x \ i(y)) * z) * (z \ (y * x)) = 1. [para(202(a,1),370(a,1,1,1))]. 476 (x * y) / (x * (z \ y)) = (x * z) / x. [para(3(a,1),42(a,1,1,2))]. 477 (x * (y / z)) / x = (x * y) / (x * z). [para(6(a,1),42(a,1,1,2)),flip(a)]. 480 (x * ((x \ y) * z)) / ((y / x) * z) = y / (y / x). [para(6(a,1),42(a,2,1)),rewrite(39(3))]. 482 ((x * y) * (z * (y \ (u * y)))) / ((x * u) * y) = ((x * y) * z) / (x * y). [para(8(a,1),42(a,1,2))]. 493 i(x) \ (y / x) = (x * y) / x. [para(27(a,1),42(a,1,1,2)),rewrite(2(2),427(3))]. 494 (x / y) \ i(y) = y / (y * x). [para(28(a,1),42(a,1,1,2)),rewrite(2(2),364(5)),flip(a)]. 495 i(x) * (y * x) = (y \ x) \ x. [para(28(a,1),42(a,1,2)),rewrite(36(5),305(7),202(6),188(5))]. 496 (x * (y \ z)) / x = (y / x) \ (z / x). [para(201(a,1),42(a,1,1,2)),rewrite(427(5),202(3),274(3)),flip(a)]. 497 ((x * i(y)) \ (i(y) * z)) \ z = ((z \ y) * x) / (z \ y). [para(201(a,1),42(a,1,2)),rewrite(305(6),202(5),300(4))]. 503 ((x * y) \ (y * z)) \ z = (x \ (y * z)) \ (y * z). [para(210(a,1),42(a,1,2)),rewrite(305(6),202(5),300(4),188(3),426(10),202(8),300(7),188(6))]. 506 (x * (y * (z * (y \ u)))) / (x * u) = (x * (y * z)) / (x * y). [para(40(a,1),42(a,1,1,2)),rewrite(477(10))]. 509 ((x * (y / z)) \ y) \ z = (x \ y) \ y. [para(304(a,1),42(a,1,2)),rewrite(305(6),202(5),188(4),305(8),202(7),188(6))]. 511 ((x * y) \ z) \ (y \ z) = (x \ z) \ z. [para(305(a,1),42(a,2)),rewrite(429(6),202(4),188(3),202(7),188(6))]. 513 (x * y) * (z * (y \ i(x))) = ((x * y) * z) / (x * y). [para(211(a,1),42(a,1,2)),rewrite(36(7))]. 517 (i(x) * y) * (z * (y \ x)) = (z \ (y \ x)) \ (y \ x). [para(370(a,1),42(a,1,2)),rewrite(36(7),429(11),202(9),202(8),188(7))]. 519 (x * (y / z)) * (z / (z * y)) = (x * i(y)) * (y / z). [back_rewrite(384),rewrite(494(5))]. 520 (x \ (i(y) * z)) \ (i(y) * z) = ((z \ y) * x) / (z \ y). [back_rewrite(497),rewrite(503(6))]. 522 (i(x) * y) \ (x \ (y * x)) = x. [para(196(a,1),4(a,1,2))]. 523 (x \ (y * x)) / x = i(x) * y. [para(196(a,1),5(a,1,1))]. 524 (x \ (y * x)) * (x \ (z * x)) = ((i(x) * y) * z) * x. [para(196(a,1),8(a,1,1))]. 525 (x * y) * (y \ (y \ (z * y))) = (x * (i(y) * z)) * y. [para(196(a,1),8(a,1,2,2))]. 554 (x \ i(y)) * x = x \ (y \ x). [para(196(a,1),202(a,1,1)),rewrite(300(3),202(2),202(6),188(5))]. 556 (i(x) * y) * (((i(x) * y) \ z) * x) = (i(z) \ (y \ x)) * (x \ (y * x)). [para(196(a,1),39(a,1,2)),rewrite(429(3)),flip(a)]. 558 x \ ((x / y) * x) = i(y) * x. [para(304(a,1),196(a,1,1)),flip(a)]. 566 x / (x / (x \ y)) = y * i(x). [para(3(a,1),317(a,1,1)),flip(a)]. 567 (x * y) \ (x / (x / y)) = i(x). [para(317(a,1),4(a,1,2))]. 570 (x / y) / ((x / y) / y) = (x * y) / x. [para(6(a,1),317(a,1,1)),rewrite(203(2),319(3)),flip(a)]. 571 (x / (x / y)) * (x / (x / z)) = ((x * y) * z) * i(x). [para(317(a,1),8(a,1,1)),rewrite(310(6))]. 593 (x \ y) / ((i(y) * x) \ y) = (i(y) \ x) \ x. [para(201(a,1),317(a,1,1)),rewrite(300(3),495(4),305(7),300(6)),flip(a)]. 594 (x / y) * i(x) = x / (x * y). [para(317(a,1),202(a,1,1)),rewrite(203(3),202(6),307(7))]. 595 ((x * y) * z) * (y \ i(x)) = (x * y) / ((x * y) / z). [para(202(a,1),317(a,1,2))]. 597 (x * ((x \ y) * z)) * (x * i(y)) = (y / x) / ((y / x) / (x * z)). [para(39(a,1),317(a,1,1)),rewrite(203(5))]. 599 (x * y) \ (x * (x * y)) = (x \ y) \ y. [para(210(a,1),317(a,1,1)),rewrite(300(4),188(3),495(3),362(7),426(8),300(5),188(4)),flip(a)]. 602 ((x \ y) * z) * (i(y) * x) = (x \ y) / ((x \ y) / z). [para(300(a,1),317(a,1,2))]. 606 (x \ (y * x)) * (y \ x) = (y \ x) \ (x * (y \ x)). [para(196(a,1),317(a,1,1)),rewrite(202(5),188(4),376(9),426(10),202(7),188(6))]. 608 (x \ i(y)) \ (z * (x \ i(y))) = (y * x) / ((y * x) / z). [back_rewrite(431),rewrite(595(11))]. 610 x \ ((x * y) / x) = y * i(x). [para(319(a,1),4(a,1,2))]. 629 i(x) * ((x / y) * (i(x) * y)) = y \ (i(x) * y). [para(201(a,1),319(a,2,1)),rewrite(300(4),308(6),277(9),300(8))]. 630 x * (y \ i(x)) = (x / y) / x. [para(319(a,1),202(a,1,1)),rewrite(203(3),202(2),309(7))]. 634 (x / y) * (z * (y * i(x))) = ((x / y) * z) / (x / y). [para(203(a,1),319(a,1,2,2))]. 641 ((x \ y) \ y) * ((x * y) \ y) = 1. [para(319(a,1),370(a,1,1)),rewrite(305(4),202(3),188(2),188(4))]. 644 ((x \ y) \ y) * y = y \ ((x * y) * y). [para(319(a,1),196(a,1,1)),rewrite(305(4),202(3),188(2),188(5))]. 646 x * (x / (x / y)) = (x * (x * y)) / x. [para(196(a,1),319(a,1,2)),rewrite(310(4),188(5))]. 647 x * (y * (x \ i(x))) = x / (i(x) \ (x / y)). [para(319(a,1),317(a,1,1)),rewrite(40(4),427(7))]. 651 (x * y) \ ((x / z) / x) = (z * y) \ i(x). [back_rewrite(420),rewrite(630(4))]. 657 (x * (y \ z)) \ i(y) = z \ ((y / x) / y). [back_rewrite(347),rewrite(630(7))]. 664 x * (i(y) * x) = (y / x) \ x. [para(3(a,1),412(a,1,1,1)),rewrite(300(4)),flip(a)]. 665 (x / (x / y)) \ (x / y) = (x / y) * i(y). [para(6(a,1),412(a,1,1,1))]. 672 i(x) \ x = x * x. [para(27(a,1),412(a,1,1,1)),rewrite(26(2),188(4))]. 673 i(x) * i(x) = x \ i(x). [para(28(a,1),412(a,1,1,1)),rewrite(305(3),187(2),33(2)),flip(a)]. 674 x / (i(x) \ y) = (x / y) / x. [para(412(a,1),201(a,1,1)),rewrite(317(4),305(2),203(6),202(5),630(6))]. 675 (x \ (i(y) * x)) \ (x \ y) = (x \ y) * y. [para(201(a,1),412(a,1,1,1)),rewrite(277(3),300(2),188(8))]. 678 ((x * y) / (x * z)) \ x = x * (z * i(y)). [para(203(a,1),412(a,2,2)),rewrite(477(3))]. 679 i(x) * (y \ x) = x \ (i(y) * x). [para(412(a,1),210(a,1,1)),rewrite(196(4),305(7),202(6),188(5),300(6)),flip(a)]. 683 ((x / y) \ (z / y)) \ y = y * (i(z) * x). [para(300(a,1),412(a,2,2)),rewrite(496(3))]. 684 i(x) * (y * i(x)) = (y \ x) \ i(x). [para(304(a,1),412(a,1,1,1)),rewrite(305(3),188(2),203(6)),flip(a)]. 687 (x * i(y)) * (x * i(y)) = (y / x) \ (x * i(y)). [para(273(a,1),412(a,1,1,1)),rewrite(427(4),187(2),33(3),203(8)),flip(a)]. 692 x * (y * (x \ i(x))) = (x / (x / y)) / x. [back_rewrite(647),rewrite(674(8))]. 693 (x * x) * (x \ y) = y * ((x \ y) \ y). [para(3(a,1),46(a,1,2,2)),flip(a)]. 694 (x \ y) \ (z * (x \ y)) = y \ ((x * z) * (x \ y)). [para(46(a,1),4(a,1,2)),flip(a)]. 703 ((x / y) \ y) * (y \ x) = x * (i(x) * y). [para(28(a,1),46(a,1,2,2)),rewrite(24(3),300(2),300(5),664(6)),flip(a)]. 713 i(x) \ ((y * z) * (y \ i(x))) = (x * y) / ((x * y) / z). [back_rewrite(608),rewrite(694(6))]. 714 (x \ (y * x)) * (y \ x) = x \ ((y * x) * (y \ x)). [back_rewrite(606),rewrite(694(8))]. 727 x / (x * x) = i(x). [para(672(a,1),37(a,1,2))]. 731 i(x) * (y * (x * x)) = x \ ((y * x) * x). [para(672(a,1),40(a,2,2,2)),rewrite(305(4),202(3),188(2),644(3)),flip(a)]. 733 (i(x) * y) \ (y \ x) = (y \ x) * (y \ x). [para(300(a,1),672(a,1,1))]. 736 (x \ i(x)) * (x / (x / y)) = (i(x) * y) * i(x). [para(673(a,1),8(a,1,1)),rewrite(310(6))]. 740 (x \ i(y)) * (x \ i(y)) = (y * x) \ (x \ i(y)). [para(202(a,1),673(a,1,1)),rewrite(202(4),202(8))]. 783 (x * (y * i(z))) * ((y * i(z)) \ y) = (x * ((y * z) / y)) * (y * i(z)). [para(412(a,1),47(a,1,1,2)),rewrite(412(6),412(13))]. 786 (x * (y * x)) / x = i(x) \ y. [para(5(a,1),493(a,1,2)),flip(a)]. 794 (x / y) / ((y * x) / y) = i(y). [para(493(a,1),37(a,1,2))]. 795 ((x \ y) * y) / (x \ y) = (i(y) * x) \ x. [para(37(a,1),493(a,1,2)),rewrite(300(2)),flip(a)]. 796 x \ (i(y) \ x) = (y \ x) \ x. [para(188(a,1),493(a,1,1)),rewrite(305(2),305(7),202(6),188(5))]. 800 (x * i(y)) \ (z / (y / x)) = ((y / x) * z) / (y / x). [para(203(a,1),493(a,1,1))]. 808 ((x * y) / x) / x = x / (x * (x / y)). [para(319(a,1),493(a,2,1)),rewrite(364(4),307(5)),flip(a)]. 809 ((x * x) * x) / (x * x) = x. [para(727(a,1),493(a,1,2)),rewrite(202(2),212(4),188(2)),flip(a)]. 817 (x * x) * x = x * (x * x). [para(809(a,1),6(a,1,1)),flip(a)]. 818 (x * x) * (x * y) = x * ((x * x) * y). [para(809(a,1),39(a,1,1)),rewrite(817(7),599(8),34(5),33(6)),flip(a)]. 825 (x * x) \ i(x) = x \ (x \ i(x)). [para(817(a,1),202(a,1,1)),rewrite(202(3),202(5))]. 828 x * ((x \ y) * ((x \ y) * (x \ y))) = (((y / x) * y) / x) * y. [para(817(a,1),40(a,2,2)),rewrite(240(4)),flip(a)]. 832 (x * (y * (y * y))) / (x * y) = (x * (y * y)) / x. [para(817(a,1),42(a,1,1,2))]. 836 (x / y) * (y / (y * x)) = i(y). [para(494(a,1),3(a,1,2))]. 837 x / (x * (y * x)) = y \ i(x). [para(5(a,1),494(a,1,1)),flip(a)]. 845 x \ (x / (x / y)) = y / x. [para(494(a,1),37(a,1,2)),rewrite(277(4),203(3),317(3))]. 846 (x \ y) / ((x \ y) * y) = x \ (i(y) * x). [para(37(a,1),494(a,1,1)),rewrite(300(2)),flip(a)]. 847 (i(x) \ y) \ y = y \ (x \ y). [para(188(a,1),494(a,1,2)),rewrite(305(2),429(7),188(5))]. 849 (x / (y * z)) \ (z \ i(y)) = (y * z) / ((y * z) * x). [para(202(a,1),494(a,1,2))]. 850 (x / y) * ((y / (y * x)) * z) = i(x) * ((x / y) * z). [para(494(a,1),39(a,2,2,1)),rewrite(277(3),203(2),4(3)),flip(a)]. 854 x * (y / x) = x / (x / y). [para(494(a,1),300(a,1,1)),rewrite(203(3),317(3),188(4)),flip(a)]. 855 (x / (y \ z)) \ (i(z) * y) = (y \ z) / ((y \ z) * x). [para(300(a,1),494(a,1,2))]. 859 (x * x) / (x * y) = x / ((x * y) / x). [para(319(a,1),494(a,2,2)),rewrite(364(3),306(5),477(3))]. 862 (x \ y) / ((i(y) * x) \ y) = x \ (y \ x). [back_rewrite(593),rewrite(847(8))]. 877 (x * y) \ (z * y) = y \ ((x \ z) * y). [para(3(a,1),48(a,1,2,1))]. 890 (x \ ((y * z) \ (z * y))) \ ((y * z) \ (z * y)) = (z * y) \ (((y * z) * x) * ((y * z) \ (z * y))). [para(22(a,1),48(a,1,2)),rewrite(599(10),694(16))]. 891 x \ (i(y) * x) = (y * x) \ x. [para(27(a,1),48(a,1,2,1)),rewrite(1(3)),flip(a)]. 892 (i(x) * y) \ y = y \ (x * y). [para(28(a,1),48(a,1,2,1)),rewrite(1(4))]. 895 (x \ (y \ i(z))) * (z * x) = x \ (y \ x). [para(48(a,1),300(a,1,1)),rewrite(300(3),202(2),554(3),202(5),202(4)),flip(a)]. 897 x \ ((y \ i(z)) * x) = ((z * y) * x) \ x. [para(211(a,1),48(a,1,2,1)),rewrite(1(4)),flip(a)]. 910 (x \ y) / ((x \ y) * y) = (y * x) \ x. [back_rewrite(846),rewrite(891(7))]. 916 i(x) * (y \ x) = (y * x) \ x. [back_rewrite(679),rewrite(891(6))]. 917 ((x * y) \ y) \ (y \ x) = (y \ x) * x. [back_rewrite(675),rewrite(891(3))]. 918 i(x) * ((x / y) * (i(x) * y)) = (x * y) \ y. [back_rewrite(629),rewrite(891(9))]. 923 ((x \ y) * y) / (x \ y) = x \ (y * x). [back_rewrite(795),rewrite(892(7))]. 924 (x * y) \ ((x * y) / x) = y / (x * y). [para(5(a,1),845(a,1,2,2))]. 925 (x / (x / y)) / (y / x) = x. [para(845(a,1),37(a,1,2))]. 926 (x \ y) / y = y \ (y / x). [para(37(a,1),845(a,1,2,2)),flip(a)]. 928 i(x) \ (x \ (y * x)) = i(y) \ x. [para(277(a,1),845(a,1,2,2)),rewrite(426(5),188(3),305(6))]. 929 x \ ((x / y) / x) = y \ i(x). [para(277(a,1),845(a,2)),rewrite(305(2),674(3))]. 930 x / (x \ (y \ x)) = i(y) \ x. [para(845(a,1),305(a,2)),rewrite(277(3),426(4),188(2),300(3),202(2),554(3),305(5))]. 939 (x \ y) / (y \ (y / x)) = (x \ y) * x. [para(37(a,1),854(a,1,2)),rewrite(926(5)),flip(a)]. 940 (x / y) * (y / (y / z)) = y * ((y \ x) * (z / y)). [para(854(a,1),39(a,1,2))]. 941 ((x / (x / y)) / x) * z = x * ((y / x) * (x \ z)). [para(854(a,1),40(a,1,1,1))]. 946 x \ ((i(y) \ x) * x) = (x \ (y * x)) * x. [para(854(a,1),196(a,1,1)),rewrite(277(3),426(4),188(2),305(5)),flip(a)]. 947 x / (x * (x / y)) = x / (x / (y / x)). [para(854(a,1),317(a,1,1)),rewrite(594(4))]. 948 ((x / (x / y)) / x) \ x = x * (x * i(y)). [para(854(a,1),412(a,1,1,1)),rewrite(203(6))]. 950 ((x * y) / x) / x = x / (x / (y / x)). [back_rewrite(808),rewrite(947(6))]. 951 ((x * y) / x) / (y / (x * y)) = x * y. [para(5(a,1),925(a,1,1,2))]. 954 ((x * (y * z)) / ((x * y) / x)) / ((x * z) / (x * (y * z))) = x * (y * z). [para(42(a,1),925(a,1,1,2))]. 961 (x \ (x / y)) * x = y \ x. [para(926(a,1),6(a,1,1))]. 962 (x \ (x / y)) \ (y \ x) = x. [para(926(a,1),38(a,1,1))]. 963 (x \ (x / y)) * (x * z) = x * ((x \ (y \ x)) * z). [para(926(a,1),39(a,1,1))]. 964 (x * y) * i(y) = y * (i(y) * x). [para(926(a,1),203(a,1,1)),rewrite(300(3),203(2),190(3),300(5))]. 966 (x * i(y)) \ x = i(x) \ (x \ y). [para(274(a,1),926(a,1,1)),rewrite(305(3),203(2),305(7),188(6))]. 967 x / (y * x) = (x * y) \ x. [para(277(a,1),926(a,2,2)),rewrite(305(4),300(3),188(2),307(6)),flip(a)]. 971 i(x) \ (x \ (x / y)) = x * i(y). [para(926(a,1),493(a,1,2)),rewrite(496(7),35(6),24(7),203(6))]. 984 (x * i(y)) * y = y * (i(y) * x). [back_rewrite(190),rewrite(964(6))]. 986 (x * (y * i(z))) * (i(y) \ (y \ z)) = (x * ((y * z) / y)) * (y * i(z)). [back_rewrite(783),rewrite(966(6))]. 987 ((x * y) / x) / ((y * x) \ y) = x * y. [back_rewrite(951),rewrite(967(4))]. 988 (x * y) \ ((x * y) / x) = (y * x) \ y. [back_rewrite(924),rewrite(967(6))]. 990 (x * y) / (y \ (z * y)) = (x / z) * y. [para(6(a,1),49(a,1,1,1))]. 1008 x / (x \ (y * x)) = i(y) * x. [para(28(a,1),49(a,1,1,1)),rewrite(1(2))]. 1009 (x \ (x / y)) \ x = y * x. [para(28(a,1),49(a,1,2,2)),rewrite(984(3),24(5),305(5),202(4),374(4),926(2))]. 1010 (x \ y) \ ((z \ x) \ x) = (y \ z) * x. [para(201(a,1),49(a,1,1,1)),rewrite(891(5),376(5),300(4),495(4))]. 1018 (((x * y) * y) * z) * (z \ (y \ i(x))) = ((x * y) * z) / (x * z). [para(49(a,1),317(a,2,2)),rewrite(8(5),202(6),202(5))]. 1027 ((x * y) * (y \ z)) / (((y \ z) \ z) \ z) = x * ((y \ z) \ z). [para(47(a,1),49(a,1,1)),rewrite(3(9))]. 1042 (x * (y \ (y / z))) * y = (x * y) * (y \ (z \ y)). [para(961(a,1),8(a,1,2,2)),flip(a)]. 1055 (x \ y) * x = (y \ x) \ x. [para(37(a,1),961(a,1,1,2))]. 1057 x * ((x \ (y \ x)) * ((x \ (x / y)) \ z)) = ((x \ y) \ y) * z. [para(961(a,1),40(a,1,1,1)),rewrite(939(4),1055(2),963(10)),flip(a)]. 1070 x \ ((i(y) \ x) * x) = ((y * x) \ x) \ x. [back_rewrite(946),rewrite(1055(7))]. 1071 (x \ y) / (y \ (y / x)) = (y \ x) \ x. [back_rewrite(939),rewrite(1055(6))]. 1086 ((x * y) \ x) \ (y \ (x * y)) = x * y. [para(5(a,1),962(a,1,1,2))]. 1088 (i(x) \ (x \ y)) \ (y / x) = i(x). [para(274(a,1),962(a,1,2)),rewrite(305(4),188(3))]. 1091 (x / y) \ (x / (x * y)) = i(x). [para(494(a,1),962(a,1,2)),rewrite(277(4),203(3),4(4),274(3))]. 1093 ((x \ y) \ (y \ (y / x))) \ (y \ (x \ y)) = x \ y. [para(926(a,1),962(a,1,1,2))]. 1094 ((x \ y) \ y) \ (y \ x) = x \ (x / y). [para(3(a,1),967(a,1,2)),rewrite(926(2),1055(4)),flip(a)]. 1095 (x / y) / (y / (y / x)) = x \ (x / y). [para(6(a,1),967(a,2,1)),rewrite(854(3))]. 1099 ((x * y) \ (y * x)) / (x * (z * ((x * y) \ (y * x)))) = (((x * y) \ (y * x)) * (x * z)) \ ((x * y) \ (y * x)). [para(18(a,1),967(a,1,2))]. 1104 ((x * y) \ x) * ((y * x) * z) = (y * x) * (((y * x) \ x) * z). [para(967(a,1),39(a,1,1))]. 1106 ((x / y) / x) \ x = i(x) \ y. [para(210(a,1),967(a,1,2)),rewrite(305(2),630(5)),flip(a)]. 1108 ((x * y) * x) \ x = x \ i(y). [para(967(a,1),304(a,1,2)),rewrite(916(4),202(5))]. 1112 (x * (i(x) * y)) \ i(x) = x \ (x / (x * y)). [para(317(a,1),967(a,1,2)),rewrite(277(4),203(3),594(3),266(6)),flip(a)]. 1117 (x \ i(y)) \ ((x * y) \ x) = ((y * x) * x) / (y * x). [para(967(a,1),493(a,1,2)),rewrite(202(2))]. 1120 (x * y) * ((y * x) \ y) = (x * y) / x. [para(967(a,1),854(a,1,2)),rewrite(5(7))]. 1124 x * (x * i(y)) = i(x) \ (x / y). [back_rewrite(948),rewrite(1106(4)),flip(a)]. 1131 (x \ (x / y)) * (y * x) = x. [para(1009(a,1),3(a,1,2))]. 1132 ((x * y) \ x) \ (x * y) = y * (x * y). [para(5(a,1),1009(a,1,1,2))]. 1133 (x * y) \ x = x \ (x / y). [para(1009(a,1),37(a,1,2)),rewrite(967(2))]. 1134 (x \ y) * y = (y \ x) \ y. [para(37(a,1),1009(a,1,1,2)),flip(a)]. 1137 (x * y) \ (y * (i(y) * x)) = i(y). [para(1009(a,1),212(a,1,1)),rewrite(300(4),203(3),984(4))]. 1140 (x \ (i(x) \ y)) \ x = i(y) * x. [para(305(a,1),1009(a,1,1,2))]. 1146 (x / y) * x = (y / x) \ x. [para(845(a,1),1009(a,1,1)),flip(a)]. 1147 x * ((x \ y) * (y / x)) = (x / y) \ (x / (x / y)). [para(925(a,1),1009(a,1,1,2)),rewrite(38(3),940(8)),flip(a)]. 1150 (x \ (x \ (x / y))) \ x = (y * x) * x. [para(967(a,1),1009(a,1,1,2)),rewrite(1133(2))]. 1151 (x \ (x / y)) \ (x * y) = y * (x * y). [back_rewrite(1132),rewrite(1133(2))]. 1153 (x * y) * (y \ (y / x)) = (x * y) / x. [back_rewrite(1120),rewrite(1133(3))]. 1155 (x \ i(y)) \ (x \ (x / y)) = ((y * x) * x) / (y * x). [back_rewrite(1117),rewrite(1133(4))]. 1160 (x \ (x / y)) * ((y * x) * z) = (y * x) * (((y * x) \ x) * z). [back_rewrite(1104),rewrite(1133(2))]. 1163 ((x * y) \ (y * x)) / (x * (z * ((x * y) \ (y * x)))) = ((x * y) \ (y * x)) \ (((x * y) \ (y * x)) / (x * z)). [back_rewrite(1099),rewrite(1133(18))]. 1167 (x \ (x / y)) \ (y \ (x * y)) = x * y. [back_rewrite(1086),rewrite(1133(2))]. 1169 (x * y) \ ((x * y) / x) = y \ (y / x). [back_rewrite(988),rewrite(1133(6))]. 1170 ((x * y) / x) / (y \ (y / x)) = x * y. [back_rewrite(987),rewrite(1133(4))]. 1171 x / (y * x) = x \ (x / y). [back_rewrite(967),rewrite(1133(4))]. 1172 i(x) \ (x \ y) = x \ (i(x) \ y). [back_rewrite(966),rewrite(1133(3),305(2)),flip(a)]. 1173 x \ ((x \ i(y)) \ x) = ((y * x) \ x) \ x. [back_rewrite(1070),rewrite(1134(3))]. 1174 ((x \ y) \ x) / (y \ x) = y \ (x * y). [back_rewrite(923),rewrite(1134(2))]. 1175 ((x * y) \ y) \ (y \ x) = (x \ y) \ x. [back_rewrite(917),rewrite(1134(6))]. 1176 (x \ y) / ((y \ x) \ y) = (y * x) \ x. [back_rewrite(910),rewrite(1134(3))]. 1179 (x \ (y \ x)) \ x = x \ ((y * x) * x). [back_rewrite(644),rewrite(1134(3))]. 1181 x * ((x \ y) * ((x \ y) * (x \ y))) = (((x / y) \ y) / x) * y. [back_rewrite(828),rewrite(1146(8))]. 1182 x \ ((y / x) \ x) = i(y) * x. [back_rewrite(558),rewrite(1146(2))]. 1188 (x \ (i(x) \ y)) \ (y / x) = i(x). [back_rewrite(1088),rewrite(1172(3))]. 1189 (x * (y * i(z))) * (y \ (i(y) \ z)) = (x * ((y * z) / y)) * (y * i(z)). [back_rewrite(986),rewrite(1172(6))]. 1191 x \ (i(x) \ (x / y)) = x * i(y). [back_rewrite(971),rewrite(1172(4))]. 1192 x \ (i(x) \ (y * x)) = i(y) \ x. [back_rewrite(928),rewrite(1172(4))]. 1194 ((x / y) * z) \ (x * (y \ (z * y))) = y. [para(50(a,1),4(a,1,2))]. 1195 (x * (y \ (z * y))) / y = (x / y) * z. [para(50(a,1),5(a,1,1))]. 1196 (x * (y \ (z * y))) * (y \ (u * y)) = (((x / y) * z) * u) * y. [para(50(a,1),8(a,1,1))]. 1218 (x \ (y * x)) \ i(z) = x \ (y \ (x * i(z))). [para(50(a,1),202(a,1,1)),rewrite(202(4),202(7),203(6))]. 1220 (x * ((x \ y) * z)) * x = y * (x \ ((x * z) * x)). [para(39(a,1),50(a,1,1))]. 1223 (x * (y * (x \ z))) * x = (x * y) * (x \ (z * x)). [para(40(a,1),50(a,1,1))]. 1240 (x * ((y \ x) \ x)) * x = y * (x * x). [para(817(a,1),50(a,2,2,2)),rewrite(39(3),1055(2),4(7))]. 1247 x * ((x \ (y \ x)) * y) = y \ (x * y). [para(4(a,1),1055(a,2,1)),rewrite(1133(2),963(4))]. 1254 (x \ (x / y)) \ (x / y) = y / (y / x). [para(38(a,1),1055(a,1,1)),rewrite(854(2)),flip(a)]. 1255 (x / (y \ z)) * ((z \ y) \ y) = (y \ z) * (((y \ z) \ x) * y). [para(1055(a,1),39(a,1,2))]. 1256 (x \ (i(x) \ y)) \ (x \ y) = (x * y) \ y. [para(212(a,1),1055(a,1,1)),rewrite(916(3),1172(5)),flip(a)]. 1258 (((x \ y) \ y) / (y \ x)) * z = (y \ x) * (y * ((y \ x) \ z)). [para(1055(a,1),40(a,1,1,1))]. 1260 (x \ (i(x) \ y)) \ (i(x) \ y) = y \ (x * y). [para(299(a,1),1055(a,1,1)),rewrite(916(4),892(3)),flip(a)]. 1265 (x \ y) * ((y / x) \ x) = ((y \ x) \ x) / (x \ y). [para(1055(a,1),319(a,2,1)),rewrite(300(3),664(4))]. 1268 x * (i(x) * y) = x \ (i(x) \ y). [para(412(a,1),1055(a,2,1)),rewrite(610(3),984(3),1133(6),305(5))]. 1270 (x / (x * y)) \ i(x) = (x / (x / y)) / x. [para(493(a,1),1055(a,1,1)),rewrite(40(4),692(4),494(6)),flip(a)]. 1271 (x / (x * y)) * (y / x) = ((x * y) / x) \ (y / x). [para(493(a,1),1055(a,2,1)),rewrite(494(3))]. 1274 (x * y) \ (y \ (i(y) \ x)) = i(y). [back_rewrite(1137),rewrite(1268(4))]. 1278 x \ (x / (x * y)) = i(y) * i(x). [back_rewrite(1112),rewrite(1268(3),212(5),300(3)),flip(a)]. 1282 (x * i(y)) * y = y \ (i(y) \ x). [back_rewrite(984),rewrite(1268(6))]. 1289 (x * y) * i(y) = y \ (i(y) \ x). [back_rewrite(964),rewrite(1268(6))]. 1291 ((x / y) \ y) * (y \ x) = x \ (i(x) \ y). [back_rewrite(703),rewrite(1268(7))]. 1313 x \ (x \ (i(x) \ y)) = i(x) * y. [back_rewrite(344),rewrite(1268(4),1172(3))]. 1314 i(x) * (x * y) = x \ (i(x) \ y). [back_rewrite(266),rewrite(1268(6))]. 1321 (x \ (x / y)) * (y * (x * y)) = x * y. [para(5(a,1),1131(a,1,1,2)),rewrite(1133(2))]. 1323 ((x \ (x / y)) * z) * (y * x) = x * ((y * x) \ (z * (y * x))). [para(1131(a,1),8(a,1,1)),flip(a)]. 1348 (x * y) / (x * (z * y)) = (y / x) \ ((y / z) / x). [para(1131(a,1),42(a,1,1,2)),rewrite(496(8))]. 1357 (x / (x \ (x / y))) \ (x \ (x / y)) = (x \ (x / y)) * (x \ i(y)). [para(1131(a,1),412(a,1,1,1)),rewrite(202(10))]. 1360 ((x / y) \ ((x / y) / y)) * (y / (y / x)) = x / y. [para(854(a,1),1131(a,1,2))]. 1366 ((x * (y * z)) / ((x * y) / x)) / ((z / x) \ ((z / y) / x)) = x * (y * z). [back_rewrite(954),rewrite(1348(9))]. 1370 (x * y) * (x \ (x / y)) = x. [para(1133(a,1),3(a,1,2))]. 1371 x \ (x / (x \ y)) = y \ x. [para(3(a,1),1133(a,1,1)),flip(a)]. 1372 (x / y) \ ((x / y) / y) = x \ (x / y). [para(6(a,1),1133(a,1,1)),flip(a)]. 1375 (x * (y * ((x * z) \ (z * x)))) \ (x * y) = (x * y) \ ((x * y) / ((x * z) \ (z * x))). [para(18(a,1),1133(a,1,1))]. 1377 (x * (x * ((y * z) \ (z * y)))) \ (x * x) = (x * x) \ ((x * x) / ((y * z) \ (z * y))). [para(22(a,1),1133(a,1,1))]. 1378 x / (x \ (x / y)) = x * y. [para(1133(a,1),37(a,1,2))]. 1382 (x \ (x / y)) \ (y \ i(x)) = i(x). [para(1133(a,1),212(a,1,1)),rewrite(202(4))]. 1390 x \ (x / (y / x)) = x / y. [para(854(a,1),1133(a,1,1)),rewrite(38(3)),flip(a)]. 1391 (x \ (x / y)) / x = i(y) * i(x). [para(1133(a,1),926(a,1,1)),rewrite(1278(6))]. 1393 (i(x) * i(y)) \ (y \ (y / x)) = y. [para(1133(a,1),962(a,1,2)),rewrite(1278(3))]. 1395 (x \ y) \ ((x \ y) / x) = y \ (y / x). [para(1055(a,1),1133(a,1,1)),rewrite(1094(4)),flip(a)]. 1397 (x \ (x / y)) * (y / (y / x)) = x / y. [back_rewrite(1360),rewrite(1372(4))]. 1399 (x \ (x / y)) * (x \ i(y)) = (x * y) \ (x \ (x / y)). [back_rewrite(1357),rewrite(1378(3)),flip(a)]. 1406 (x \ y) \ ((y \ x) \ y) = y. [para(1134(a,1),4(a,1,2))]. 1423 i(x) * (x \ y) = x \ (i(x) * y). [para(1134(a,1),202(a,1,1)),rewrite(300(3),300(5))]. 1425 (x \ (i(x) \ y)) * (x \ y) = i(y) \ (x \ y). [para(212(a,1),1134(a,2,1)),rewrite(1172(3))]. 1426 (x / y) * i(y) = (y / x) \ i(y). [para(274(a,1),1134(a,1,1)),rewrite(274(6))]. 1427 (x \ y) * (y * ((x \ y) \ z)) = (x \ (y * x)) * z. [para(1134(a,1),40(a,1,1,1)),rewrite(1174(4)),flip(a)]. 1434 (x \ (y * x)) \ x = x \ ((x \ y) \ x). [para(1134(a,1),196(a,2,2)),rewrite(916(3),1134(3))]. 1437 (x \ y) * (y \ (i(y) \ x)) = x \ (y * x). [para(1134(a,1),319(a,2,1)),rewrite(300(3),1268(4),1174(9))]. 1438 (x \ (y * x)) \ (x \ y) = i(x). [para(1134(a,1),412(a,1,1,1)),rewrite(1174(4),201(7))]. 1439 (x * i(y)) * x = (y * i(x)) \ x. [para(412(a,1),1134(a,1,1)),rewrite(610(6))]. 1442 x * (y * (x \ (y / x))) = (x / (x * y)) \ (y / x). [para(493(a,1),1134(a,1,1)),rewrite(40(4),494(7))]. 1444 (x / (x / y)) \ (x / y) = (y / x) \ i(y). [back_rewrite(665),rewrite(1426(7))]. 1445 (x * (y / z)) \ ((x * z) * (z \ y)) = z. [para(51(a,1),4(a,1,2))]. 1446 ((x * y) * (y \ z)) / y = x * (z / y). [para(51(a,1),5(a,1,1))]. 1466 (x \ i(y)) \ (x * y) = (y * x) * (x * y). [para(22(a,1),51(a,2)),rewrite(854(5),1146(7),1106(7),202(2),3(10))]. 1468 (x \ y) \ (x \ i(z)) = x \ ((y / x) \ i(z)). [para(51(a,1),202(a,1,1)),rewrite(202(4),202(3),202(7))]. 1490 (x * x) * (x \ y) = i(x) \ y. [para(854(a,1),51(a,1,1)),rewrite(1146(3),1106(3)),flip(a)]. 1495 ((x * y) * (y \ z)) \ (x * (z / y)) = (x * (z / y)) \ ((x * (z / y)) / y). [para(51(a,1),1133(a,1,1))]. 1499 x * ((y \ x) \ x) = i(y) \ x. [back_rewrite(693),rewrite(1490(3)),flip(a)]. 1500 (x \ i(y)) \ x = y * (x * x). [back_rewrite(1240),rewrite(1499(3),1134(3))]. 1501 ((x * y) \ y) \ y = y \ (x * (y * y)). [back_rewrite(1173),rewrite(1500(3)),flip(a)]. 1502 (x / y) \ ((y / x) \ x) = x. [para(1146(a,1),4(a,1,2))]. 1503 (x \ (x / y)) \ (y * x) = y * (y * x). [para(5(a,1),1146(a,1,1)),rewrite(1171(4)),flip(a)]. 1505 (x * y) * (i(z) * y) = (x * (y / z)) * y. [para(1146(a,1),8(a,1,2,2)),rewrite(1182(4))]. 1520 (x \ (x / y)) * (y \ x) = y \ (y \ x). [para(37(a,1),1146(a,2,1)),rewrite(926(2))]. 1521 i(x) * (y / x) = x \ (y * i(x)). [para(1146(a,1),202(a,1,1)),rewrite(300(3),203(5))]. 1523 (x / (x * y)) \ (x * y) = x * (y * y). [para(1146(a,1),39(a,1)),rewrite(4(6))]. 1525 (((x / y) \ y) / (y / x)) * z = (y / x) * (y * ((y / x) \ z)). [para(1146(a,1),40(a,1,1,1))]. 1527 (i(x) \ y) * x = (y \ i(x)) \ x. [para(277(a,1),1146(a,2,1)),rewrite(305(2))]. 1528 ((x / y) \ y) * (y \ (x * i(y))) = 1. [para(1146(a,1),211(a,1,1)),rewrite(203(4))]. 1536 (x / y) * ((x * y) / x) = ((y / x) \ x) / (x / y). [para(1146(a,1),319(a,2,1)),rewrite(203(3),319(4))]. 1541 ((x / y) \ y) * x = y * (x \ (y * x)). [para(1146(a,1),50(a,1,1))]. 1542 ((x / y) \ y) \ (y / x) = (y / x) \ ((y / x) / y). [para(1146(a,1),1133(a,1,1))]. 1548 x \ (i(x) \ (x * y)) = i(x) \ y. [para(210(a,1),1171(a,1,2)),rewrite(305(2),426(5)),flip(a)]. 1549 (x / y) \ ((y * i(x)) \ x) = y \ (i(y) \ x). [para(304(a,1),1171(a,1,2)),rewrite(305(3),203(2),1133(3),305(2),305(7),203(6)),flip(a)]. 1550 (x * i(y)) \ ((y / x) \ i(y)) = (y / x) \ ((y / x) / y). [para(319(a,1),1171(a,1,2)),rewrite(364(5),203(4),202(3),630(4),364(9)),flip(a)]. 1554 x / ((y * x) * (x \ z)) = x \ (x / (y * (z / x))). [para(51(a,1),1171(a,1,2))]. 1556 ((x * y) * y) * (x \ (x / y)) = x * y. [para(5(a,1),1370(a,1,2,2)),rewrite(1133(4))]. 1582 (x * i(y)) * (x \ (i(x) \ y)) = x. [para(305(a,1),1370(a,1,2,2))]. 1587 (x * y) / ((x * y) / (x \ (x / y))) = (x / y) / x. [para(1370(a,1),317(a,1,1)),rewrite(202(2),630(3)),flip(a)]. 1588 (x * y) * (x \ (i(x) \ y)) = x * (y * y). [para(1370(a,1),412(a,1,1,1)),rewrite(1523(4),300(6),203(5),1282(6)),flip(a)]. 1595 ((x \ y) \ y) * (x \ (x / y)) = y \ x. [para(1055(a,1),1370(a,1,1)),rewrite(1395(6))]. 1599 ((x / y) \ y) * ((y / x) \ ((y / x) / y)) = y / x. [para(1146(a,1),1370(a,1,1))]. 1602 x * (y \ x) = x / (x \ y). [para(1371(a,1),3(a,1,2))]. 1603 (x / (x \ y)) / (y \ x) = x. [para(1371(a,1),37(a,1,2))]. 1605 (x \ y) * i(x) = (y \ x) \ i(x). [para(1371(a,1),212(a,1,1)),rewrite(203(6)),flip(a)]. 1609 (x / (x \ y)) \ ((x / (x \ y)) / x) = (y \ x) / (x / (x \ y)). [para(1371(a,1),926(a,1,1)),flip(a)]. 1610 (x \ (x / y)) \ (i(y) * i(x)) = (y \ x) \ (x \ (x / y)). [para(962(a,1),1371(a,1,2,2)),rewrite(1391(5))]. 1611 (x \ y) / ((x \ y) / x) = (y \ x) \ (x / (x \ y)). [para(1371(a,1),1055(a,2,1)),rewrite(38(3),854(4))]. 1665 (x * (y \ (z * y))) * (y \ ((y \ z) \ y)) = (x * (i(z) * y)) * (y \ (z * y)). [para(28(a,1),53(a,1,2,2,1)),rewrite(1(7),1434(6))]. 1727 (x * y) / (x \ (x / y)) = (x * y) * y. [para(5(a,1),1378(a,1,2,2)),rewrite(1133(3))]. 1729 (x * y) * (((x * y) \ y) * z) = (y * x) * ((y \ (y / x)) * z). [para(1378(a,1),39(a,1,1)),rewrite(1009(10),1160(10)),flip(a)]. 1732 x * (x / y) = x / (y / x). [para(845(a,1),1378(a,1,2)),flip(a)]. 1733 (x / (x / y)) \ (i(x) \ y) = x. [para(1378(a,1),925(a,1,1,2)),rewrite(1391(5),427(6),203(3),317(3),305(4))]. 1734 (x / (x / y)) * (y / x) = (x / (x / y)) / (x / y). [para(925(a,1),1378(a,1,2,2)),rewrite(38(5)),flip(a)]. 1736 (i(x) * i(y)) \ y = (y * x) * y. [para(1378(a,1),1146(a,1,1)),rewrite(1391(5)),flip(a)]. 1737 (i(x) * i(y)) * (y \ (y / x)) = (y * x) \ (y \ (y / x)). [para(1378(a,1),1146(a,2,1)),rewrite(1391(3))]. 1739 (x * y) / ((x * y) * y) = (x / y) / x. [back_rewrite(1587),rewrite(1727(5))]. 1744 (x * (x * y)) / x = x / ((x / y) / x). [back_rewrite(646),rewrite(1732(3)),flip(a)]. 1747 (x / (y / x)) / (x / y) = x. [para(1390(a,1),37(a,1,2))]. 1748 x / (y * (x * x)) = x \ i(y). [para(1390(a,1),305(a,2)),rewrite(305(3),277(4),300(3),300(5),202(4),188(3),1134(3),1500(3),277(5))]. 1753 (x / y) \ (x / (y / x)) = (y * x) / y. [para(1390(a,1),1055(a,2,1)),rewrite(38(3),854(4),570(4)),flip(a)]. 1760 (x * i(y)) \ ((y * i(x)) \ x) = x. [para(412(a,1),1406(a,1,1)),rewrite(610(5))]. 1764 ((x \ y) \ x) \ (y \ (x * y)) = x \ y. [para(1406(a,1),926(a,1,1)),rewrite(37(3),1174(7)),flip(a)]. 1773 (x \ (x / y)) \ (y \ (y \ x)) = y \ x. [para(37(a,1),1502(a,1,2,1)),rewrite(926(2))]. 1775 (i(x) \ y) \ ((y \ i(x)) \ x) = x. [para(277(a,1),1502(a,1,2,1)),rewrite(305(2))]. 1784 x * ((y * x) \ (x * y)) = y \ (x * y). [para(54(a,1),4(a,1,2)),flip(a)]. 1846 (x \ (y * x)) \ (i(x) * y) = y \ (y / x). [para(54(a,1),1171(a,1,2)),rewrite(1784(4),926(4),5(3),1133(2),1784(6),1784(8),523(7)),flip(a)]. 1935 (x / y) * (y / (y \ z)) = y * ((y \ x) * (z \ y)). [para(1602(a,1),39(a,1,2))]. 1936 x \ (x \ (x / y)) = i(x) * i(y). [para(212(a,1),1602(a,1,2)),rewrite(1172(7),277(8),300(7),300(6),1282(7),274(6)),flip(a)]. 1944 (x \ y) \ (y / (y \ x)) = y \ ((x * y) * (x \ y)). [para(1602(a,1),196(a,2,2)),rewrite(300(2),196(3),714(4)),flip(a)]. 1945 (x / (x \ y)) / x = x * i(y). [para(1602(a,1),319(a,2,1)),rewrite(201(3)),flip(a)]. 1946 x * (y * (x \ (y * i(x)))) = ((x / y) / x) \ (y / x). [para(412(a,1),1602(a,2,2)),rewrite(610(5),40(5),427(10),203(8),202(7),630(8))]. 1948 (x \ y) * ((x \ (x \ y)) \ x) = (x * y) * (y \ x). [para(1602(a,1),47(a,1,1)),rewrite(1255(5),1134(4))]. 1949 (x / y) * ((y * x) / y) = (x / y) / (y / (y * x)). [para(493(a,1),1602(a,1,2)),rewrite(494(8))]. 1950 i(x) \ (i(y) \ x) = x * (y * x). [para(1009(a,1),1602(a,1,2)),rewrite(1936(5),427(6),305(5)),flip(a)]. 1953 (x \ y) / (y / (y \ x)) = (x \ y) \ (y \ (y / x)). [para(1602(a,1),1171(a,1,2)),rewrite(926(7))]. 1955 (x / (y / x)) * (x / y) = (x / (y / x)) / (y / x). [para(1390(a,1),1602(a,1,2)),rewrite(38(9))]. 1965 (i(x) * i(y)) \ x = (y * x) * x. [back_rewrite(1150),rewrite(1936(3))]. 1967 (x \ y) / ((x \ y) / x) = x \ ((y * x) * (y \ x)). [back_rewrite(1611),rewrite(1944(8))]. 1970 (x / (x \ y)) \ (x * i(y)) = (y \ x) \ (x \ (x / y)). [back_rewrite(1609),rewrite(1945(5),1953(9))]. 1976 (x \ (y * i(x))) / (y / x) = i(x). [para(274(a,1),1603(a,1,1,2)),rewrite(277(3),203(2),274(6))]. 1995 (x * y) / (y \ (y / x)) = (x * y) * x. [para(5(a,1),1732(a,1,2)),rewrite(1171(5)),flip(a)]. 2000 (x \ y) * (y \ (y / x)) = (x \ y) / x. [para(37(a,1),1732(a,2,2)),rewrite(926(3))]. 2002 ((x / (y / x)) / x) * z = x * ((x / y) * (x \ z)). [para(1732(a,1),40(a,1,1,1))]. 2004 x * (i(x) \ y) = i(x) \ (x * y). [para(277(a,1),1732(a,2,2)),rewrite(305(2),426(6))]. 2005 x \ (i(x) * i(y)) = (x * x) \ i(y). [para(1732(a,1),300(a,2)),rewrite(277(2),1500(3),202(3),305(6),277(7),300(6)),flip(a)]. 2006 (x / (y / x)) * ((x / y) \ i(x)) = 1. [para(1732(a,1),211(a,1,1))]. 2011 ((x * x) \ i(y)) * x = x \ (x \ (y \ x)). [para(1732(a,1),196(a,1,1)),rewrite(305(3),277(4),300(3),2005(4),277(6),1055(7),847(7))]. 2013 (x / (y / x)) / x = x / ((x * y) / x). [para(1732(a,1),319(a,2,1)),rewrite(594(3),1732(3)),flip(a)]. 2014 (x / (x / y)) / (y \ (y / x)) = i(x) \ y. [para(925(a,1),1732(a,1,2)),rewrite(1146(3),1106(3),1095(8)),flip(a)]. 2016 ((x / y) \ ((x / y) / x)) * (x / (y / x)) = x / y. [para(1732(a,1),1131(a,1,2))]. 2017 (x / (y / x)) * y = (x * y) * (y \ x). [para(1732(a,1),51(a,1,1))]. 2018 (x / y) / (x / (y / x)) = (x / y) \ ((x / y) / x). [para(1732(a,1),1171(a,1,2))]. 2019 i(x) \ (i(x) \ y) = x * (x * y). [para(1378(a,1),1732(a,1,2)),rewrite(1391(5),427(6),305(5)),flip(a)]. 2026 (x / ((x * y) / x)) * z = x * ((x / y) * (x \ z)). [back_rewrite(2002),rewrite(2013(3))]. 2028 ((x \ y) / x) / (y \ (y / x)) = x \ y. [para(37(a,1),1747(a,1,1,2)),rewrite(926(4))]. 2031 (x * (y * y)) \ (x * y) = i(y). [para(277(a,1),1747(a,1,1)),rewrite(305(2),300(3),2005(4),277(5),426(6),300(4),188(2))]. 2038 (i(x) \ y) / x = x / (x / y). [para(925(a,1),1747(a,1,2)),rewrite(1095(6),2014(5))]. 2039 ((x * y) / x) / (y / (x / y)) = x / y. [para(1747(a,1),926(a,2,2)),rewrite(1753(4),38(8))]. 2060 i(x) * ((i(x) \ y) * (i(z) \ ((z * x) \ x))) = y * (i(z) \ ((z * x) \ x)). [para(201(a,1),60(a,1,2,2,1)),rewrite(916(7),201(12),916(13))]. 2062 (x / y) * (z \ (y * z)) = x * ((z * y) \ (y * z)). [para(60(a,1),39(a,2)),rewrite(1784(5))]. 2101 (x * y) * (((x * y) \ z) * ((y \ (x * y)) \ x)) = z * ((y \ (x * y)) \ x). [para(1370(a,1),60(a,1,2,2,2)),rewrite(963(7),1247(7),963(12),1247(12),1370(14))]. 2120 (x \ (x \ y)) \ (x \ y) = y \ (x * y). [para(3(a,1),495(a,1,2)),rewrite(300(2),196(3)),flip(a)]. 2122 ((x \ y) \ y) / (x * y) = i(y). [para(495(a,1),5(a,1,1))]. 2123 ((x / y) \ y) \ y = i(y) * x. [para(6(a,1),495(a,1,2)),flip(a)]. 2141 (x * y) \ (((y * x) * ((y \ i(x)) * (y * x))) * ((y * x) \ (x * y))) = (y \ i(x)) * (y * x). [para(495(a,1),22(a,2)),rewrite(300(4),202(2),300(8),202(6),22(13),471(12),2(6),300(8),202(6),890(16)),flip(a)]. 2147 i(x) * (y * (z * (y \ x))) = (((y * z) / y) \ x) \ x. [para(40(a,1),495(a,1,2))]. 2152 (x \ (y * i(x))) \ (y * i(x)) = ((y / x) \ x) / (x / y). [para(319(a,1),495(a,1,2)),rewrite(202(3),274(3),1536(4)),flip(a)]. 2154 (x * i(y)) * (x \ (y * i(x))) = ((x * y) / x) \ (y / x). [para(493(a,1),495(a,2,1)),rewrite(203(2),1521(5))]. 2155 (x * (y * y)) \ y = y \ ((x * y) \ y). [para(495(a,1),494(a,2,2)),rewrite(305(3),202(2),1500(3),188(4),277(7),300(6),916(6))]. 2160 i(x) * (y * (x \ (z * x))) = (((y / x) * z) \ x) \ x. [para(50(a,1),495(a,1,2))]. 2162 (x * (x * y)) \ (x * y) = y \ (x \ y). [para(1131(a,1),495(a,1,2)),rewrite(202(2),1055(3),847(3),1503(6)),flip(a)]. 2163 i(x) * ((y * x) * (x \ z)) = ((y * (z / x)) \ x) \ x. [para(51(a,1),495(a,1,2))]. 2164 (x * y) / ((x \ y) \ y) = (x * y) \ (x * (y * y)). [para(495(a,1),1171(a,1,2)),rewrite(305(8),202(7),1500(8))]. 2180 (x / (x \ y)) \ (x / y) = i(x). [para(201(a,1),522(a,1,2,2)),rewrite(188(2),1602(2),274(5))]. 2190 ((x \ y) \ y) \ (y \ ((x * y) * y)) = y. [para(319(a,1),522(a,1,1)),rewrite(305(4),202(3),188(2),188(4))]. 2198 (x \ (x / y)) * (y \ (x * y)) = y \ (y \ (x * y)). [para(522(a,1),1055(a,2,1)),rewrite(1846(5))]. 2199 (x \ (i(x) * y)) \ (x \ ((y \ x) \ x)) = x. [para(1055(a,1),522(a,1,2,2)),rewrite(1423(3))]. 2202 ((x * y) \ y) \ (y \ ((y \ x) \ y)) = y. [para(1134(a,1),522(a,1,2,2)),rewrite(916(3))]. 2217 ((x \ y) \ y) / (x \ y) = (i(y) * x) * x. [para(3(a,1),523(a,1,1,2)),rewrite(300(6))]. 2218 x \ (y * i(x)) = (x \ y) / x. [para(6(a,1),523(a,1,1,2)),rewrite(1521(5)),flip(a)]. 2224 (x * i(y)) \ y = y / (y \ x). [para(201(a,1),523(a,1,1,2)),rewrite(274(3),305(3),203(2),188(5),1602(5))]. 2229 (x / (x * y)) / (y / x) = (x * i(y)) * i(y). [para(304(a,1),523(a,1,1,2)),rewrite(494(3),203(6))]. 2230 (x \ y) \ (i(y) * x) = ((y \ x) / y) * x. [para(370(a,1),523(a,1,1,2)),rewrite(24(3),300(2),376(4),300(3),300(6),1505(9),1521(7),2218(7))]. 2231 (x \ (x \ (y * x))) / x = i(x) * (i(x) * y). [para(196(a,1),523(a,1,1,2))]. 2235 (x \ (y * x)) * (i(y) * x) = (x \ (y \ x)) \ (y \ x). [para(523(a,1),854(a,2,2)),rewrite(1008(5),429(10),300(8),202(7),1055(8),847(8))]. 2245 (i(x) * y) * (x \ (y * x)) = (i(y) * x) \ (x \ (y * x)). [para(523(a,1),1146(a,1,1)),rewrite(1008(8))]. 2246 (i(x) * y) * y = (i(y) * x) \ y. [para(523(a,1),1146(a,2,1)),rewrite(1008(3))]. 2248 (x \ (i(x) \ y)) * (x * y) = (y * x) * y. [para(1370(a,1),523(a,1,1,2)),rewrite(1009(3),1995(4),300(5),203(4),1282(5)),flip(a)]. 2253 i(x) \ (y \ x) = (y / x) \ x. [para(523(a,1),1732(a,2,2)),rewrite(1008(3),664(3),429(5)),flip(a)]. 2259 (x * i(y)) * ((x \ y) / x) = ((x * y) / x) \ (y / x). [back_rewrite(2154),rewrite(2218(5))]. 2260 ((x \ y) / x) \ (y * i(x)) = ((y / x) \ x) / (x / y). [back_rewrite(2152),rewrite(2218(3))]. 2262 ((x \ y) / x) / (y / x) = i(x). [back_rewrite(1976),rewrite(2218(3))]. 2263 x * (y * ((x \ y) / x)) = ((x / y) / x) \ (y / x). [back_rewrite(1946),rewrite(2218(3))]. 2265 ((x / y) \ y) * ((y \ x) / y) = 1. [back_rewrite(1528),rewrite(2218(5))]. 2266 i(x) * (y / x) = (x \ y) / x. [back_rewrite(1521),rewrite(2218(6))]. 2269 (x * i(y)) \ (x / (x \ y)) = x. [back_rewrite(1760),rewrite(2224(5))]. 2270 i(x) \ (y * x) = (x * y) * x. [back_rewrite(1736),rewrite(2224(4),426(3))]. 2271 (x / y) \ (x / (x \ y)) = y \ (i(y) \ x). [back_rewrite(1549),rewrite(2224(4))]. 2272 (x * i(y)) * x = x / (x \ y). [back_rewrite(1439),rewrite(2224(6))]. 2274 ((x \ y) \ y) / (x \ y) = (i(x) * y) \ x. [back_rewrite(2217),rewrite(2246(7))]. 2278 (x \ i(y)) \ y = y * (x * y). [back_rewrite(1950),rewrite(2253(4),277(2))]. 2280 (x \ (i(x) \ y)) * (x \ y) = (x / y) \ y. [back_rewrite(1425),rewrite(2253(8))]. 2284 x \ ((x * y) * x) = i(y) \ x. [back_rewrite(1192),rewrite(2270(3))]. 2285 (i(x) \ y) \ (x * (y * x)) = x. [back_rewrite(1775),rewrite(2278(5))]. 2286 (i(x) \ y) * x = x * (y * x). [back_rewrite(1527),rewrite(2278(6))]. 2289 (x * ((x \ y) * z)) * x = y * (i(z) \ x). [back_rewrite(1220),rewrite(2284(7))]. 2291 (x * i(y)) * (y / (y \ x)) = y. [para(566(a,1),6(a,1,1))]. 2296 (x / (x \ y)) / (((x \ y) / x) \ x) = (y * i(x)) \ ((y \ x) \ i(x)). [para(566(a,1),494(a,1,1)),rewrite(203(5),1605(5),1146(11)),flip(a)]. 2297 (x / y) / ((x / y) / (y / (y * x))) = y \ (y / x). [para(494(a,1),566(a,1,2,2)),rewrite(203(9),1314(10),274(9))]. 2299 (x / (x \ y)) * (y * i(x)) = ((y \ x) \ i(x)) \ (y / x). [para(566(a,1),854(a,1,2)),rewrite(1945(10),427(10),203(8),1605(8))]. 2456 (x * (y * x)) \ (x * y) = i(x). [para(1171(a,1),567(a,1,2,2)),rewrite(1378(5))]. 2484 (x * x) * ((y / (y * z)) \ i(z)) = x * (x * ((y / (y * z)) \ i(z))). [para(594(a,1),22(a,1,2,1)),rewrite(304(6),594(9),304(11))]. 2491 (x / y) * (i(x) * ((x / y) \ z)) = ((x / (x * y)) / (x / y)) * z. [para(594(a,1),40(a,1,1,1)),flip(a)]. 2500 ((x / y) \ y) \ (x \ y) = (x \ y) \ (y \ (x \ y)). [para(196(a,1),594(a,2,2)),rewrite(376(3),202(6),188(5),1055(5),2253(3),376(9),300(8),202(7),1055(8),847(8))]. 2502 (x * (y * x)) * (y \ i(x)) = (x * y) / (x / (x / y)). [para(317(a,1),594(a,2,2)),rewrite(305(3),202(2),2278(3),202(4))]. 2503 (x / y) * ((y \ x) \ i(x)) = (x / (x * y)) / (x / y). [para(594(a,1),319(a,2,1)),rewrite(203(4),684(5))]. 2507 ((x / y) \ y) / (y / x) = (y / x) / (y / (y * x)). [para(594(a,1),494(a,2,2)),rewrite(277(3),203(2),2218(3),203(4),2260(5))]. 2513 (x / y) / (y \ (i(y) \ x)) = x / (x * y). [para(594(a,1),1378(a,2)),rewrite(305(5),203(4),2224(5),2271(5))]. 2521 ((x \ y) \ i(y)) \ (x / y) = (y / x) / (y / (y * x)). [para(594(a,1),594(a,2,2)),rewrite(305(3),203(2),2224(3),203(4),2299(5))]. 2527 ((x / y) / (x / (x * y))) * z = (x / y) * (x * ((x / y) \ z)). [back_rewrite(1525),rewrite(2507(4))]. 2530 (x \ y) \ i(y) = y \ (x / y). [para(3(a,1),610(a,1,2,1)),rewrite(1605(5)),flip(a)]. 2531 (x / y) \ (x / (x / y)) = i(y) \ (y / x). [para(6(a,1),610(a,1,2,1)),rewrite(203(6),1124(7))]. 2537 (x \ y) \ ((y * x) \ x) = i(y) * (i(y) * x). [para(201(a,1),610(a,1,2,1)),rewrite(277(4),300(3),891(4),300(7))]. 2545 (x * i(y)) * i(y) = (x / y) / y. [para(319(a,1),610(a,1,2,1)),rewrite(950(3),845(4)),flip(a)]. 2550 (x \ y) \ (x \ (y * x)) = y \ (i(y) \ x). [para(1134(a,1),610(a,1,2,1)),rewrite(1174(5),300(6),1268(7))]. 2561 (x / y) / (x / (x * y)) = (x \ (y / x)) \ (y / x). [back_rewrite(2521),rewrite(2530(3)),flip(a)]. 2562 (x / y) * (x \ (y / x)) = (x / (x * y)) / (x / y). [back_rewrite(2503),rewrite(2530(4))]. 2569 (x / (x \ y)) / (((x \ y) / x) \ x) = (y * i(x)) \ (x \ (y / x)). [back_rewrite(2296),rewrite(2530(11))]. 2576 (x \ y) * i(x) = x \ (y / x). [back_rewrite(1605),rewrite(2530(6))]. 2577 i(x) * (y * i(x)) = x \ (y / x). [back_rewrite(684),rewrite(2530(7))]. 2578 x * ((x \ y) * (y / x)) = i(y) \ (y / x). [back_rewrite(1147),rewrite(2531(8))]. 2580 (x / (x * y)) / (y / x) = (x / y) / y. [back_rewrite(2229),rewrite(2545(8))]. 2586 ((x \ (y / x)) \ (y / x)) * z = (x / y) * (x * ((x / y) \ z)). [back_rewrite(2527),rewrite(2561(4))]. 2602 (x * y) * (z \ (y \ i(x))) = ((x * y) / z) / (x * y). [para(202(a,1),630(a,1,2,2))]. 2605 (x / y) * (z \ (y * i(x))) = ((x / y) / z) / (x / y). [para(203(a,1),630(a,1,2,2))]. 2611 (x \ i(y)) \ ((y / x) / y) = (y * x) / ((y * x) / y). [para(630(a,1),196(a,2,2)),rewrite(300(3),188(2),595(5)),flip(a)]. 2612 (x / (x / y)) \ i(x) = (x / (x * y)) / x. [para(630(a,1),317(a,1,1)),rewrite(1426(4),426(7),674(8))]. 2621 ((x / y) / x) * (i(x) \ y) = x. [para(630(a,1),1370(a,1,1)),rewrite(426(5),1548(6))]. 2625 (x \ (y * x)) * (x \ (x \ (y \ x))) = (y \ x) \ (x \ (y \ x)). [para(523(a,1),630(a,2,1)),rewrite(300(5),202(4),1055(5),847(5),376(11),300(10),202(9),1055(10),847(10))]. 2782 (x \ y) * ((x * y) \ y) = x \ (x \ y). [para(37(a,1),664(a,2,1)),rewrite(916(4))]. 2783 x * ((y \ i(z)) * x) = ((z * y) / x) \ x. [para(202(a,1),664(a,1,2,1))]. 2786 x * ((y * i(z)) * x) = ((z / y) / x) \ x. [para(203(a,1),664(a,1,2,1))]. 2795 (x * y) * ((x \ y) \ y) = x * (x * y). [para(319(a,1),664(a,1,2)),rewrite(188(2),305(5),202(4),188(3),188(6),1171(6),188(8),1503(8))]. 2796 (i(x) \ y) * (y \ (x * y)) = x * (x * y). [para(854(a,1),664(a,1,2)),rewrite(305(2),277(5),426(6),188(4),305(7),37(8),305(8),2019(9))]. 2798 (x \ (x / y)) \ (i(x) * y) = (x / y) \ y. [para(664(a,1),1009(a,2)),rewrite(5(5),1133(4),277(3),1172(4),274(3))]. 2808 ((x * y) \ y) \ (i(x) * y) = ((x \ y) \ y) / (y \ x). [para(664(a,1),495(a,1,2)),rewrite(202(3),188(2),1265(4),891(7)),flip(a)]. 2811 (x / (x \ y)) * (i(y) * x) = (y * i(x)) \ (x / (x \ y)). [para(566(a,1),664(a,2,1)),rewrite(304(6),300(4))]. 2821 (x \ i(y)) * (x * y) = (y * x) \ (x * y). [back_rewrite(2141),rewrite(2783(7),1291(10),202(4),1466(6),4(6)),flip(a)]. 2849 (i(x) \ y) * ((x / y) / x) = (i(x) \ y) / (x / (x / y)). [para(674(a,1),854(a,1,2)),rewrite(2038(10))]. 2852 (x \ (x / y)) / (y \ x) = y \ (x \ y). [para(926(a,1),674(a,2,1)),rewrite(300(3),862(5)),flip(a)]. 2861 (x \ (y * x)) / (x \ ((y * x) * x)) = (y \ x) \ (x \ (y \ x)). [para(523(a,1),674(a,2,1)),rewrite(300(5),202(4),1055(5),847(5),1179(5),376(11),300(10),202(9),1055(10),847(10))]. 2868 (i(x) \ y) * (x * z) = x * ((y * x) * z). [para(786(a,1),39(a,1,1)),rewrite(4(7))]. 2869 x * ((y * x) * (x \ z)) = (i(x) \ y) * z. [para(786(a,1),40(a,1,1)),flip(a)]. 2876 (x * (y * y)) / y = i(x) \ y. [para(845(a,1),786(a,2)),rewrite(277(3),426(4),188(2),1055(3),1501(3),3(4),305(5))]. 2877 (x * (y * x)) / (i(x) \ y) = (x * y) / (x / (x / y)). [para(786(a,1),854(a,2,2)),rewrite(837(5),2502(5)),flip(a)]. 2880 (x * (y * (x \ (z * x)))) / x = i(x) \ ((y / x) * z). [para(50(a,1),786(a,1,1,2))]. 2888 (x \ (y \ x)) / x = x \ i(y). [para(1390(a,1),786(a,2)),rewrite(305(3),277(4),300(3),2005(4),2011(4),3(4),277(5))]. 2909 (i(x) \ y) / ((x \ y) \ y) = y. [para(188(a,1),794(a,2)),rewrite(305(2),305(6),202(5),188(4))]. 2911 x * (y * (x \ ((((x * y) / x) \ (y / x)) * z))) = x \ (i(x) \ (y * (x \ z))). [para(794(a,1),39(a,1,1)),rewrite(40(4),1314(5),40(13)),flip(a)]. 2935 (x * y) \ (x * (y * y)) = x \ (i(x) \ y). [para(1378(a,1),794(a,1,1)),rewrite(1055(4),38(3),1071(5),2164(4),300(7),203(6),1282(7))]. 2945 ((x / y) / (y / (y * x))) \ (y \ (i(y) \ x)) = y * i(x). [para(794(a,1),567(a,1,2,2)),rewrite(1949(4),305(7),203(6),1133(7),305(6),203(10))]. 3000 x \ ((y \ i(z)) \ x) = ((z * y) \ x) \ x. [para(202(a,1),796(a,1,2,1))]. 3001 (x \ (i(x) \ y)) * (x * z) = x * (((y \ x) \ x) * z). [para(796(a,1),39(a,2,2,1)),rewrite(926(3),305(2))]. 3003 x \ ((i(y) * z) \ x) = ((z \ y) \ x) \ x. [para(300(a,1),796(a,1,2,1))]. 3005 (x \ (y / x)) \ (y / x) = (y / x) \ ((x * y) / x). [para(493(a,1),796(a,1,2)),flip(a)]. 3006 ((x * y) / x) \ (y / x) = (y / x) \ (x \ (y / x)). [para(493(a,1),796(a,2,1)),rewrite(188(3)),flip(a)]. 3007 (x \ (y * x)) \ (i(y) \ x) = (y * x) \ (x * (y * x)). [para(845(a,1),796(a,1,2)),rewrite(277(3),426(4),188(2),305(4),277(8),426(9),188(7),277(11),426(12),188(10),2120(11))]. 3022 (((x \ y) \ y) \ x) * y = ((x \ y) \ y) \ (x * y). [para(610(a,1),796(a,1,2)),rewrite(305(4),202(3),188(2),188(4),305(8),202(7),188(6),305(11),202(10),188(9),1010(10)),flip(a)]. 3025 x * (((y \ x) \ x) * y) = (y * x) * y. [back_rewrite(2248),rewrite(3001(5))]. 3030 ((x / y) \ ((y * x) / y)) * z = (y / x) * (y * ((y / x) \ z)). [back_rewrite(2586),rewrite(3005(4))]. 3034 (x / y) / (x / (x * y)) = (y / x) \ ((x * y) / x). [back_rewrite(2561),rewrite(3005(8))]. 3037 x * (y * (x \ (((y / x) \ (x \ (y / x))) * z))) = x \ (i(x) \ (y * (x \ z))). [back_rewrite(2911),rewrite(3006(4))]. 3038 (x * i(y)) * ((x \ y) / x) = (y / x) \ (x \ (y / x)). [back_rewrite(2259),rewrite(3006(9))]. 3040 (x / (x * y)) * (y / x) = (y / x) \ (x \ (y / x)). [back_rewrite(1271),rewrite(3006(8))]. 3045 ((x \ y) / x) * (x / y) = i(x). [para(3(a,1),836(a,1,2,2))]. 3061 (i(x) \ y) * (y \ (x \ y)) = y. [para(188(a,1),836(a,2)),rewrite(305(2),429(6),188(4))]. 3085 (x / (x * y)) \ ((x / y) / y) = x / y. [para(836(a,1),1171(a,1,2)),rewrite(305(4),203(3),317(3),38(3),2580(7)),flip(a)]. 3087 (x * y) * (y \ (x \ y)) = x \ (i(x) \ y). [para(1378(a,1),836(a,1,1)),rewrite(1055(6),38(5),2852(5),300(7),203(6),1282(7))]. 3091 ((x / (x / y)) / x) / (x / (x * y)) = (x / (x / y)) / (x / y). [para(836(a,1),523(a,1,1,2)),rewrite(1270(4),203(9),317(9),1734(10))]. 3111 (x * (y * x)) * ((i(x) * i(y)) * z) = (y \ i(x)) * ((x * (y * x)) * z). [para(837(a,1),39(a,1,1)),rewrite(1133(11),1171(10),1936(11)),flip(a)]. 3117 (x \ (y \ i(x))) \ x = (x * (y * x)) * x. [para(837(a,1),1009(a,1,1,2))]. 3122 x / ((i(x) \ y) * z) = (y * (z / x)) \ i(x). [para(51(a,1),837(a,1,2,2)),rewrite(2869(4))]. 3124 x / (x \ (y \ i(x))) = x * (x * (y * x)). [para(837(a,1),1378(a,1,2,2))]. 3133 (i(x) \ y) * ((y \ (x \ y)) * z) = i(x) * ((i(x) \ y) * z). [para(847(a,1),39(a,2,2,1)),rewrite(37(3)),flip(a)]. 3136 ((i(x) * y) \ z) \ z = z \ ((y \ x) \ z). [para(300(a,1),847(a,1,1,1))]. 3137 (x * (y \ (z \ y))) * (y \ ((z * y) * y)) = (x * (i(z) \ y)) * (y \ (z \ y)). [para(847(a,1),47(a,1,1,2)),rewrite(847(6),1179(6),847(13))]. 3138 (x * (i(y) \ z)) * (z \ (y \ z)) = (x * i(y)) * (i(y) \ z). [para(847(a,1),47(a,1,2))]. 3141 (x \ i(y)) \ (x \ (y \ x)) = x. [para(847(a,1),962(a,1,2)),rewrite(37(3))]. 3150 ((x * y) * y) \ y = y \ (y \ (x \ y)). [para(847(a,1),847(a,2,2)),rewrite(300(3),1965(4))]. 3151 (x * (y \ (z \ y))) * (y \ ((z * y) * y)) = (x * i(z)) * (i(z) \ y). [back_rewrite(3137),rewrite(3138(13))]. 3241 (x * y) * ((z * y) \ y) = (x * i(z)) * y. [para(891(a,1),8(a,1,2))]. 3242 ((x * y) \ y) * (y \ x) = i(y). [para(891(a,1),201(a,1,1)),rewrite(202(5),188(4))]. 3246 (x * (y * (x \ z))) \ z = z \ (((x / y) / x) * z). [para(40(a,1),891(a,2,1)),rewrite(203(3),202(2),630(3)),flip(a)]. 3248 (x / (y / x)) \ (x / y) = y / (y * x). [para(304(a,1),891(a,1,2)),rewrite(494(3),1732(4)),flip(a)]. 3251 ((x * y) / x) \ (y * i(x)) = (y * i(x)) \ (x \ (y / x)). [para(319(a,1),891(a,2,1)),rewrite(2577(6)),flip(a)]. 3254 (x / (x / y)) \ (y / x) = (y / x) \ ((x \ y) / x). [para(854(a,1),891(a,2,1)),rewrite(2266(4)),flip(a)]. 3257 ((x \ y) \ y) / (y \ x) = (y \ (x \ y)) \ (x \ y). [para(891(a,1),1055(a,2,1)),rewrite(892(3),2235(5),2808(9)),flip(a)]. 3260 ((x \ y) \ x) \ x = x \ (x \ (y * x)). [para(1134(a,1),891(a,2,1)),rewrite(300(2),196(3)),flip(a)]. 3265 ((x \ y) \ y) \ (x * y) = (x * y) \ (y * (x * y)). [para(495(a,1),891(a,2,1)),rewrite(188(3)),flip(a)]. 3292 ((x \ (y \ x)) \ (y \ x)) * z = (x \ y) * (x * ((x \ y) \ z)). [back_rewrite(1258),rewrite(3257(4))]. 3296 (((x \ y) \ y) \ x) * y = (x * y) \ (y * (x * y)). [back_rewrite(3022),rewrite(3265(8))]. 3312 (i(x) \ y) \ ((y * x) * y) = (x * y) \ (y * (x * y)). [para(854(a,1),892(a,1,1)),rewrite(277(3),426(4),188(2),305(4),3007(5),305(6),305(8),1602(9),426(9),2270(9)),flip(a)]. 3316 (x * (y \ (i(y) \ z))) * (i(z) * y) = (x * (i(z) * y)) * (y \ (z * y)). [para(892(a,1),51(a,2,2)),rewrite(1171(3),305(2))]. 3319 (x \ y) \ (x \ (y * y)) = y. [para(892(a,1),566(a,1,2,2)),rewrite(990(7),277(4),376(6),202(5),300(4),188(3),202(7),188(6),3(6))]. 3321 (x \ (y \ i(x))) \ (i(y) * i(x)) = (i(y) * i(x)) \ (x / (x * y)). [para(664(a,1),892(a,1,1)),rewrite(305(2),2530(4),277(2),319(14),364(13),494(13))]. 3326 (x \ y) \ x = y \ (x * x). [para(3319(a,1),3(a,1,2)),rewrite(1134(2))]. 3328 (x \ (y * y)) / y = x \ y. [para(3319(a,1),37(a,1,2))]. 3332 (x \ i(x)) * y = x \ (i(x) * y). [para(3319(a,1),212(a,1,1)),rewrite(300(2),300(6),202(5)),flip(a)]. 3333 (x / y) \ (x / (y * y)) = i(y). [para(274(a,1),3319(a,1,1)),rewrite(673(5),307(5))]. 3343 (x \ (y * y)) \ ((x \ (y * y)) / (x \ y)) = y / (x \ (y * y)). [para(3319(a,1),926(a,1,1)),flip(a)]. 3346 (((x * x) \ ((x * x) / y)) \ x) \ (y * (x * x)) = x. [para(1009(a,1),3319(a,1,2))]. 3351 (x \ (y * y)) \ (x \ y) = (x \ y) \ (y \ (y / x)). [para(3319(a,1),1371(a,1,2,2)),rewrite(926(3)),flip(a)]. 3371 (x \ (y * y)) \ y = y \ (y \ (x * y)). [back_rewrite(3260),rewrite(3326(2))]. 3377 (x \ i(y)) \ (y * y) = (y * (x * y)) * y. [back_rewrite(3117),rewrite(3326(4))]. 3397 ((x * y) \ y) \ (y \ (x \ (y * y))) = y. [back_rewrite(2202),rewrite(3326(4))]. 3402 (x * y) * (y \ x) = x * x. [back_rewrite(1948),rewrite(3326(4),3(5)),flip(a)]. 3409 (x \ (y * y)) \ (x \ (y * x)) = y \ x. [back_rewrite(1764),rewrite(3326(2))]. 3413 (x * (y \ (z * y))) * (y \ (z \ (y * y))) = (x * (i(z) * y)) * (y \ (z * y)). [back_rewrite(1665),rewrite(3326(5))]. 3420 i(x) \ (y * y) = x * (y * y). [back_rewrite(1500),rewrite(3326(3))]. 3431 (x \ y) \ (y * y) = y \ ((x * y) * y). [back_rewrite(1179),rewrite(3326(3))]. 3433 (x \ y) / (x \ (y * y)) = (y * x) \ x. [back_rewrite(1176),rewrite(3326(3))]. 3434 ((x * y) \ y) \ (y \ x) = y \ (x * x). [back_rewrite(1175),rewrite(3326(6))]. 3435 (x \ (y * y)) / (x \ y) = x \ (y * x). [back_rewrite(1174),rewrite(3326(2))]. 3437 (i(x) \ y) \ (x * x) = i(y) * x. [back_rewrite(1140),rewrite(3326(4))]. 3438 (x \ y) * y = x \ (y * y). [back_rewrite(1134),rewrite(3326(4))]. 3439 (x / y) \ (x * x) = y * x. [back_rewrite(1009),rewrite(3326(3))]. 3445 (i(x) * y) * i(x) = (x \ y) / x. [back_rewrite(736),rewrite(3332(5),304(4),203(2),2218(3)),flip(a)]. 3449 (x / (y / x)) * y = x * x. [back_rewrite(2017),rewrite(3402(6))]. 3451 x / (y \ (x * x)) = x \ y. [back_rewrite(3343),rewrite(3435(6),3409(5)),flip(a)]. 3456 (x \ y) * (y \ (x * x)) = x. [para(3326(a,1),3(a,1,2))]. 3457 (x * y) \ (x * x) = y \ x. [para(4(a,1),3326(a,1,1)),flip(a)]. 3460 (x \ (y \ i(y))) * y = i(x) * i(y). [para(3326(a,1),210(a,1,1)),rewrite(673(3),300(7))]. 3462 (x / y) \ i(x) = y / (x * x). [para(274(a,1),3326(a,1,1)),rewrite(673(7),307(7))]. 3465 (x \ (i(x) * y)) * (y \ (x * x)) = 1. [para(3326(a,1),370(a,1,2)),rewrite(1423(3))]. 3467 (x * (y \ (z * z))) * (z \ (z \ (y * z))) = (x * (z \ y)) * (y \ (z * z)). [para(3326(a,1),47(a,1,1,2)),rewrite(3326(5),3371(6),3326(11))]. 3471 (x \ (y * y)) * (y \ x) = x \ (y * x). [para(3326(a,1),1055(a,1,1)),rewrite(2120(8))]. 3475 x * (y \ (x * x)) = x / (x \ (x \ y)). [para(3326(a,1),1602(a,1,2))]. 3478 (x \ (y * x)) \ (((x \ y) / x) * y) = x \ (i(x) * y). [para(522(a,1),3326(a,1,1)),rewrite(1505(10),2266(8)),flip(a)]. 3488 (x * x) \ ((x * x) / ((y * z) \ (z * y))) = x \ (x / ((y * z) \ (z * y))). [back_rewrite(1377),rewrite(3457(7),1133(5)),flip(a)]. 3493 (x / (x * y)) / x = (x / y) / (x * x). [back_rewrite(2612),rewrite(3462(4)),flip(a)]. 3497 (x / (y / x)) * (y / (x * x)) = 1. [back_rewrite(2006),rewrite(3462(5))]. 3498 (x * i(y)) \ (x / (y * y)) = (y / x) \ ((y / x) / y). [back_rewrite(1550),rewrite(3462(5))]. 3499 (x / (x / y)) \ (x / y) = x / (y * y). [back_rewrite(1444),rewrite(3462(7))]. 3500 (x / y) * i(y) = x / (y * y). [back_rewrite(1426),rewrite(3462(6))]. 3501 (x / (x / y)) / x = (x * y) / (x * x). [back_rewrite(1270),rewrite(3462(4)),flip(a)]. 3510 ((x * y) / (x * x)) / (x / (x * y)) = (x / (x / y)) / (x / y). [back_rewrite(3091),rewrite(3501(3))]. 3521 ((x * y) / (x * x)) * z = x * ((y / x) * (x \ z)). [back_rewrite(941),rewrite(3501(3))]. 3618 x * ((x \ (y \ (x * x))) * z) = (y \ x) * (x * z). [para(3328(a,1),39(a,1,1)),flip(a)]. 3622 ((x * x) * y) \ x = y \ i(x). [para(3328(a,1),305(a,1)),rewrite(673(5),300(6),300(5),188(4)),flip(a)]. 3624 (((x * x) * y) / (x * x)) \ x = (y / (x * x)) \ i(x). [para(412(a,1),3328(a,1,1)),rewrite(364(4)),flip(a)]. 3626 (x \ (y * x)) / (y \ x) = x \ (y * y). [para(3328(a,1),925(a,1,1,2)),rewrite(3435(4),3451(5))]. 3645 (x \ y) / ((x / y) \ y) = i(y). [para(3328(a,1),794(a,1,1)),rewrite(3475(4),1945(5),300(3),664(4))]. 3646 (x \ y) * (y \ (x / y)) = i(y). [para(3328(a,1),836(a,1,1)),rewrite(3475(4),566(5),2576(4))]. 3654 ((x * y) * x) * y = (x * y) * (x * y). [para(4(a,1),3402(a,1,2))]. 3656 (x / y) * (x / y) = x * (y \ (x / y)). [para(6(a,1),3402(a,1,1)),flip(a)]. 3675 i(x) * ((x / y) \ y) = (x \ y) * (x \ y). [para(201(a,1),3402(a,1,1)),rewrite(2253(4))]. 3676 x \ (x / (y * y)) = y \ i(y). [para(3402(a,1),202(a,1,1)),rewrite(202(2),202(5),1468(6),3462(5)),flip(a)]. 3679 i(x) * (y \ (x \ i(y))) = (y * x) \ (x \ i(y)). [para(210(a,1),3402(a,1,1)),rewrite(740(10))]. 3681 (i(x) * i(y)) * (y / x) = x \ i(x). [para(274(a,1),3402(a,1,2)),rewrite(673(8))]. 3692 (x / ((x * y) / x)) \ (x * y) = (x / (x / y)) * y. [para(3402(a,1),412(a,1,1,1)),rewrite(859(3),300(8),1505(9),854(7))]. 3699 ((x \ y) / x) * y = (x \ y) * (x \ y). [para(962(a,1),3402(a,1,2)),rewrite(2000(4))]. 3703 (x \ (x / y)) * (x \ (x / y)) = x * ((y * x) \ (x \ (x / y))). [para(1131(a,1),3402(a,1,1)),flip(a)]. 3705 (x * (x * y)) * (x \ (x / y)) = x * x. [para(1133(a,1),3402(a,1,2))]. 3709 (x * y) * (x * y) = x * (y * (x * y)). [para(1370(a,1),3402(a,1,1)),rewrite(1151(4)),flip(a)]. 3712 (((x / y) \ y) * (y / x)) * y = ((x / y) \ y) * ((x / y) \ y). [para(1502(a,1),3402(a,1,2))]. 3725 (x * y) \ (x / ((x * y) / x)) = (y \ x) * (y \ i(x)). [para(3402(a,1),610(a,1,2,1)),rewrite(859(4),202(8))]. 3733 (x * (y * y)) * ((x \ y) \ y) = (i(x) \ y) * (i(x) \ y). [para(796(a,1),3402(a,1,2)),rewrite(3438(3),3420(3))]. 3737 ((x * y) * x) * (x \ (y \ x)) = x * x. [para(847(a,1),3402(a,1,2)),rewrite(1602(3),426(3),2270(3))]. 3758 (x \ (y * x)) \ ((x \ y) * (x \ y)) = x \ (i(x) * y). [back_rewrite(3478),rewrite(3699(5))]. 3761 (x \ y) \ (i(y) * x) = (y \ x) * (y \ x). [back_rewrite(2230),rewrite(3699(7))]. 3771 ((x * y) * x) * y = x * (y * (x * y)). [back_rewrite(3654),rewrite(3709(6))]. 3788 (x / y) \ (y * i(x)) = y * (x \ (y / x)). [back_rewrite(687),rewrite(3709(5),2577(4)),flip(a)]. 3797 i(x) \ (y * (x \ (y / x))) = (x / (x * y)) \ (y / x). [para(493(a,1),3438(a,1,1)),rewrite(40(4),1442(4),3656(8)),flip(a)]. 3798 (x * x) \ ((x * x) / y) = i(y). [para(1133(a,1),3438(a,2)),rewrite(3622(3),210(3)),flip(a)]. 3799 (x / y) \ (((y / x) \ x) * ((y / x) \ x)) = x / (x \ (y / x)). [para(1502(a,1),3438(a,1,1)),rewrite(1602(3)),flip(a)]. 3805 (x \ (y * y)) \ (y * y) = (y * y) \ (x * (y * y)). [para(892(a,1),3438(a,2)),rewrite(2155(4),892(3),1055(4),3326(3),877(3),3438(2),3326(4))]. 3808 x \ (x / ((y * z) \ (z * y))) = (z * y) \ (y * z). [back_rewrite(3488),rewrite(3798(7),300(4),202(2),2821(4)),flip(a)]. 3809 (i(x) \ y) \ (x * (y * y)) = y. [back_rewrite(3346),rewrite(3798(4))]. 3821 (x * (y * ((x * z) \ (z * x)))) \ (x * y) = (z * x) \ (x * z). [back_rewrite(1375),rewrite(3808(14))]. 3833 (x * y) \ (x * i(y)) = y \ i(y). [para(3439(a,1),212(a,1,1)),rewrite(203(3),202(6))]. 3839 (x * y) / (y * y) = x * i(y). [para(3439(a,1),926(a,1,1)),rewrite(3798(8),203(5))]. 3840 (x * i(y)) \ (x * y) = y * y. [para(3439(a,1),962(a,1,2)),rewrite(3798(5),203(2))]. 3841 ((x * x) \ (x / y)) \ (x / y) = (y * x) * (x / y). [para(3439(a,1),1055(a,1,1)),flip(a)]. 3852 (x * i(y)) \ (y * y) = ((y \ x) / y) \ y. [para(566(a,1),3439(a,1,1)),rewrite(1146(7))]. 3854 ((x / y) / x) \ (x * x) = x * (y * x). [para(674(a,1),3439(a,1,1)),rewrite(2286(7))]. 3909 x * ((x \ y) * ((x / (z / x)) \ ((z / x) \ x))) = y * ((x / (z / x)) \ ((z / x) \ x)). [para(1146(a,1),76(a,1,2,2,2)),rewrite(1732(3),1732(10),1146(12))]. 3932 (x * x) / y = x / (y / x). [para(3449(a,1),5(a,1,1))]. 3959 (x * x) * (y / x) = x / (x / (x * y)). [para(3449(a,1),50(a,1,1)),rewrite(1732(6),1753(7),854(6))]. 3963 x \ (x / (y / (x / y))) = x / (y * y). [para(3449(a,1),1171(a,1,2)),flip(a)]. 3966 ((x / (y / x)) \ y) \ y = i(y) * (x * x). [para(3449(a,1),495(a,1,2)),flip(a)]. 3969 ((x \ (y / x)) \ (x / y)) * x = x * ((x \ y) \ (x / (x \ y))). [para(566(a,1),3449(a,1,1,2)),rewrite(427(5),203(3),2576(3),3656(10))]. 3986 x \ ((y / (x / y)) \ x) = (y * y) \ x. [para(3449(a,1),891(a,2,1)),rewrite(203(3),3500(3),1146(3),3932(2))]. 3987 i(x) * (y * y) = x \ (y * y). [para(3449(a,1),892(a,2,2)),rewrite(203(3),3500(3),1146(3),3932(2),3966(4))]. 3993 (x * x) \ (x / (y / x)) = i(y). [back_rewrite(3798),rewrite(3932(3))]. 4001 x \ ((x * x) * y) = i(x) \ y. [para(3451(a,1),277(a,1)),rewrite(673(5),300(6),300(5),188(4)),flip(a)]. 4007 i(x) * (i(x) * y) = x \ (x \ y). [para(3451(a,1),926(a,2,2)),rewrite(3371(3),2231(4))]. 4013 x / (x \ (y * (x * x))) = (y * x) \ x. [para(891(a,1),3451(a,2)),rewrite(877(4),3438(3),3420(3))]. 4017 (x \ y) \ ((y * x) \ x) = y \ (y \ x). [back_rewrite(2537),rewrite(4007(8))]. 4029 (x / y) * (y / (x * x)) = i(x). [para(274(a,1),3456(a,1,1)),rewrite(673(5),307(5))]. 4042 (x \ (x \ (y * x))) / (y \ (x * x)) = (x \ (i(x) * y)) * (x \ y). [para(3456(a,1),523(a,1,1,2)),rewrite(3371(3),300(9),202(8),3332(9))]. 4074 (x \ y) / (y * y) = x \ i(y). [para(3457(a,1),926(a,1,1)),rewrite(3932(7),3993(8),202(5))]. 4075 (x \ i(y)) \ (x \ y) = y * y. [para(3457(a,1),962(a,1,2)),rewrite(3932(4),3993(5),202(2))]. 4077 ((x * x) \ (x * y)) \ (x * y) = (y \ x) * (x * y). [para(3457(a,1),1055(a,1,1)),flip(a)]. 4090 (x * x) \ (y \ x) = x \ ((y * x) \ x). [para(3457(a,1),847(a,2,2)),rewrite(202(2),3377(4),877(5),1133(3),1171(2),1936(3),196(4),891(3)),flip(a)]. 4094 (x * x) \ (x * (y * (x * y))) = (y \ x) \ (x * y). [para(3457(a,1),3326(a,1,1)),rewrite(3709(7)),flip(a)]. 4283 (x / (y / x)) * (y * z) = y * ((y \ (x * x)) * z). [para(3932(a,1),39(a,1,1))]. 4284 x * (y \ i(y)) = x / (y * y). [para(3932(a,1),203(a,1,1)),rewrite(203(3),3500(3),202(4)),flip(a)]. 4286 (x \ i(x)) \ y = i(x) \ (x * y). [para(277(a,1),3932(a,2,2)),rewrite(305(3),202(2),426(6))]. 4288 (x * y) / (((x * y) * y) / (x * y)) = ((x * y) * x) / (x * y). [para(3932(a,1),42(a,1))]. 4290 ((x * x) * y) / (x * x) = x / (x / ((x * y) / x)). [para(3932(a,1),317(a,2,2)),rewrite(202(4),4284(5),3932(8),2013(7))]. 4291 x * (y / (x / y)) = x / (x / (y * y)). [para(3932(a,1),854(a,1,2))]. 4293 (x / (x / (y * y))) / (y / (x / y)) = x. [para(3932(a,1),925(a,1,2))]. 4296 (x * (y * (x * y))) / y = (x * y) * x. [para(1171(a,1),3932(a,2,2)),rewrite(3709(3),1995(8))]. 4297 i(x) \ (x * y) = (x * x) * y. [para(3932(a,1),1378(a,1,2,2)),rewrite(3993(5),305(3),202(2),4286(3))]. 4298 (x \ (x / y)) / (x * y) = (y * y) \ i(x). [para(1378(a,1),3932(a,2,2)),rewrite(3703(5),496(6),5(2),1391(3),2005(4)),flip(a)]. 4299 (x * x) * i(y) = x / (y / x). [para(3932(a,1),1390(a,1,2)),rewrite(3993(6),203(3),3932(5))]. 4332 (x / (y * y)) \ i(y) = y / ((y * x) / y). [back_rewrite(3624),rewrite(4290(4),38(5)),flip(a)]. 4341 (x \ i(x)) \ y = (x * x) * y. [back_rewrite(4286),rewrite(4297(6))]. 4352 x * (i(x) \ y) = (x * x) * y. [back_rewrite(2004),rewrite(4297(6))]. 4365 ((x * y) \ y) / (x \ y) = i(y). [para(916(a,1),5(a,1,1))]. 4387 (x \ i(y)) * (z \ (y * x)) = (z * (y * x)) \ (y * x). [para(202(a,1),916(a,1,1))]. 4388 i(x) * ((i(x) \ y) * (z \ x)) = (i(y) \ x) * ((z * x) \ x). [para(916(a,1),39(a,1,2)),rewrite(305(2)),flip(a)]. 4389 (x * i(y)) * (z \ (y / x)) = (z * (y / x)) \ (y / x). [para(203(a,1),916(a,1,1))]. 4394 (x * i(y)) \ (y \ (x / y)) = (y / x) * ((y \ x) / y). [para(319(a,1),916(a,2,1)),rewrite(202(3),274(3),2218(4),3251(9)),flip(a)]. 4396 (x / y) / ((y / x) \ x) = (y / x) \ (x \ (y / x)). [para(845(a,1),916(a,1,2)),rewrite(203(3),594(3),3040(4),1732(7),3248(10),1146(7)),flip(a)]. 4400 (x / (y * y)) * (y / x) = (x / y) / x. [para(1390(a,1),916(a,1,2)),rewrite(203(3),3500(3),1732(7),3248(10),6(7))]. 4435 ((x \ y) / x) \ (x \ ((x \ y) / x)) = (x / y) * ((x \ y) / x). [back_rewrite(2569),rewrite(4396(6),4394(11))]. 4439 (x * y) \ (x / (x * y)) = y \ (y \ i(x)). [para(5(a,1),929(a,1,2,1)),rewrite(202(6))]. 4442 (x * i(y)) \ ((y / x) / y) = (x / y) \ (y / (y * x)). [para(925(a,1),929(a,1,2,1)),rewrite(2531(6),203(2),203(9),594(9))]. 4445 (i(x) \ y) / (x / (x / y)) = (x * y) / ((x * y) / x). [para(929(a,1),1055(a,2,1)),rewrite(1106(3),2849(5),2611(10))]. 4454 (x / y) / (x * x) = x / ((x * x) * y). [para(929(a,1),566(a,1,2,2)),rewrite(426(3),4297(3),3500(7)),flip(a)]. 4455 (x \ y) / (x * x) = x \ (y / (x * x)). [para(566(a,1),929(a,1,2,1)),rewrite(364(3),3462(3),3462(7)),flip(a)]. 4466 (x \ i(y)) * ((y / x) / y) = y \ ((y / x) * (x \ i(y))). [para(929(a,1),3438(a,1,1)),rewrite(3656(10),929(9))]. 4480 (x / (x * y)) / x = x / ((x * x) * y). [back_rewrite(3493),rewrite(4454(6))]. 4504 (x * i(y)) \ ((x / y) \ y) = ((y \ x) / y) \ (x \ y). [para(1502(a,1),930(a,1,2,2)),rewrite(2123(5),429(5),300(3),2266(3),203(6)),flip(a)]. 4506 ((x * y) * x) / (i(y) \ x) = x. [para(930(a,1),1747(a,1,2)),rewrite(2888(3),426(3),2270(3))]. 4517 x / (x \ (y \ (x * x))) = x \ (y * x). [para(3326(a,1),930(a,1,2,2)),rewrite(300(6),892(7))]. 4518 x / (x \ (i(x) * y)) = ((x \ y) / x) \ x. [para(3439(a,1),930(a,1,2,2)),rewrite(877(4),1055(3),3932(5),2888(4),300(2),203(6),3852(8))]. 4520 x / (x \ (x \ i(y))) = (x * (y * x)) * x. [para(3457(a,1),930(a,1,2,2)),rewrite(4090(4),3932(5),2888(4),202(2),202(6),3377(8))]. 4688 (x / y) / (y / (y * x)) = x / (y / x). [para(304(a,1),1008(a,1,2,2)),rewrite(494(4),188(6),1732(6))]. 4697 x / (x \ ((y * x) * (x \ z))) = ((z / x) \ i(y)) * x. [para(51(a,1),1008(a,1,2,2)),rewrite(202(8))]. 4703 (x \ (y * x)) * (x \ ((y \ x) \ x)) = (i(y) * x) \ (x \ (y * x)). [para(1008(a,1),664(a,2,1)),rewrite(1423(6),495(5))]. 4707 (x / (x * y)) / ((x * y) / (x * x)) = (x * i(y)) * (x / (x * y)). [para(836(a,1),1008(a,1,2,2)),rewrite(3462(6),203(8))]. 4709 x / (x \ (y * y)) = (y / (x / y)) \ x. [para(3449(a,1),1008(a,1,2,2)),rewrite(203(6),3500(6),1146(6),3932(5))]. 4712 (x \ (y \ x)) \ (x \ y) = (i(y) * x) \ y. [para(1008(a,1),3932(a,2,2)),rewrite(524(5),2246(3),5(5),429(8),300(6),202(5),1055(6),847(6)),flip(a)]. 4715 (x / (y / x)) \ (y \ (i(y) \ x)) = y * i(x). [back_rewrite(2945),rewrite(4688(4))]. 4716 (x / y) \ ((x / y) / x) = y \ (y / x). [back_rewrite(2297),rewrite(4688(5),2018(4))]. 4723 (x * i(y)) \ (x / (y * y)) = x \ (x / y). [back_rewrite(3498),rewrite(4716(9))]. 4731 (x / y) / (x / (y / x)) = y \ (y / x). [back_rewrite(2018),rewrite(4716(8))]. 4732 (x \ (x / y)) * (y / (x / y)) = y / x. [back_rewrite(2016),rewrite(4716(4))]. 4734 ((x / y) \ y) * (x \ (x / y)) = y / x. [back_rewrite(1599),rewrite(4716(6))]. 4736 ((x / y) \ y) \ (y / x) = x \ (x / y). [back_rewrite(1542),rewrite(4716(8))]. 4780 (x \ y) \ (x \ (y / x)) = i(x). [para(3451(a,1),1091(a,1,1)),rewrite(3475(4),566(5),2576(4))]. 4786 (x * i(y)) * (x / (x * y)) = (y * i(x)) \ (x / (x * y)). [para(1091(a,1),930(a,1,2,2)),rewrite(3462(6),4707(6),203(7))]. 4791 x / (x * (y \ (x / y))) = (x / (x * y)) \ (y / x). [para(925(a,1),1106(a,1,1,1)),rewrite(3499(6),3656(3),203(7),594(7))]. 4793 (x * i(y)) \ (y / (y \ x)) = (y \ (x / y)) \ (x \ y). [para(1603(a,1),1106(a,1,1,1)),rewrite(566(3),203(8),2576(8))]. 4797 i(x) \ (x / (x \ y)) = (y / (x * x)) \ x. [para(566(a,1),1106(a,1,1,1)),rewrite(364(3),3462(3)),flip(a)]. 4799 (x * x) * (y * x) = x * ((x * y) * x). [para(837(a,1),1106(a,1,1,1)),rewrite(362(3),2278(4),4297(7)),flip(a)]. 4801 (i(x) \ y) \ ((x / y) / x) = x \ ((x / y) * (y \ i(x))). [para(1106(a,1),3326(a,1,1)),rewrite(3656(10),929(9))]. 4803 ((x * x) * y) / x = x / (x / (x * y)). [para(1106(a,1),3328(a,1,1)),rewrite(202(2),4341(3),3932(5),4454(7),3959(6),38(8))]. 4809 (x / (x \ y)) * (i(y) * x) = (x \ (y / x)) \ (y \ x). [back_rewrite(2811),rewrite(4793(10))]. 4816 ((x * y) * x) * (x \ i(y)) = x. [para(1108(a,1),3(a,1,2))]. 4825 ((x * ((x \ y) * z)) * (y / x)) \ (y / x) = (y / x) \ (z \ i(x)). [para(39(a,1),1108(a,1,1,1)),rewrite(202(10))]. 4834 ((x * (y \ (z * y))) * ((x / y) * z)) \ ((x / y) * z) = ((x / y) * z) \ i(y). [para(50(a,1),1108(a,1,1,1))]. 4947 (x \ y) \ (x \ (x \ y)) = (x * y) \ y. [para(37(a,1),1182(a,1,2,1)),rewrite(916(7))]. 4961 (i(x) * i(y)) \ (y / (y * x)) = (y * x) / ((y * x) / y). [para(1182(a,1),796(a,1,2)),rewrite(305(2),2530(4),277(2),3321(7),305(8),2530(10),277(8),305(12),2530(14),277(12),2120(14),630(11),2611(11))]. 4970 x \ (i(x) * y) = (x * x) \ y. [para(3932(a,1),1182(a,1,2,1)),rewrite(3986(4),202(4),3332(5)),flip(a)]. 4989 x / ((x * x) \ y) = ((x \ y) / x) \ x. [back_rewrite(4518),rewrite(4970(3))]. 4996 (x \ (x \ (y * x))) / (y \ (x * x)) = ((x * x) \ y) * (x \ y). [back_rewrite(4042),rewrite(4970(9))]. 5002 (x \ (y * x)) \ ((x \ y) * (x \ y)) = (x * x) \ y. [back_rewrite(3758),rewrite(4970(9))]. 5011 ((x * x) \ y) * (y \ (x * x)) = 1. [back_rewrite(3465),rewrite(4970(3))]. 5014 (x \ i(x)) * y = (x * x) \ y. [back_rewrite(3332),rewrite(4970(6))]. 5020 ((x * x) \ y) \ (x \ ((y \ x) \ x)) = x. [back_rewrite(2199),rewrite(4970(3))]. 5023 i(x) * (x \ y) = (x * x) \ y. [back_rewrite(1423),rewrite(4970(6))]. 5063 (x \ y) * (x \ (y \ x)) = (y \ x) \ (x \ (y \ x)). [para(1438(a,1),566(a,1,2,2)),rewrite(305(6),300(5),202(4),1055(5),847(5),3326(5),3431(5),2861(6),300(8),202(7),1055(8),847(8)),flip(a)]. 5072 i(x) \ ((x * x) \ y) = x \ y. [para(1438(a,1),3319(a,1,1)),rewrite(5002(7))]. 5075 ((x * x) \ y) / (x \ y) = i(x). [para(1438(a,1),3328(a,2)),rewrite(5002(6))]. 5100 (x * x) \ (i(x) \ y) = x \ y. [para(1490(a,1),4(a,1,2))]. 5101 (i(x) \ y) / (x \ y) = x * x. [para(1490(a,1),5(a,1,1))]. 5121 (x * (y \ (x / y))) * ((x / y) \ z) = (y * i(x)) \ z. [para(203(a,1),1490(a,2,1)),rewrite(3656(3))]. 5122 (x * x) \ (x / y) = x \ i(y). [para(274(a,1),1490(a,1,2)),rewrite(673(3),5014(4),188(5))]. 5128 (i(x) \ y) / (x * x) = x / (x / (y / x)). [para(1490(a,1),317(a,1,1)),rewrite(202(4),4284(5),3932(8),3932(9),2013(8),3(6))]. 5129 x / ((x \ y) / x) = ((y / x) / x) \ x. [para(1490(a,1),412(a,1,1,1)),rewrite(5128(4),3439(5),1146(3),300(6),4799(7),2272(6),1732(6)),flip(a)]. 5139 (x * x) * (y \ x) = (y / (x * x)) \ x. [para(1371(a,1),1490(a,1,2)),rewrite(4797(7))]. 5141 (x * (y \ (x / y))) * x = ((x \ y) / x) \ (y \ x). [para(1502(a,1),1490(a,1,2)),rewrite(3656(3),203(6),4504(9))]. 5144 ((x \ y) * (x \ y)) * x = (y \ x) \ (x \ (y * x)). [para(522(a,1),1490(a,1,2)),rewrite(3709(5),664(4),3675(4),202(7),188(6))]. 5152 (x * x) * (y * i(x)) = x / ((x / y) / x). [para(610(a,1),1490(a,1,2)),rewrite(493(8),1744(7))]. 5182 (x * x) * (y \ i(x)) = x / ((x * y) / x). [para(929(a,1),1490(a,1,2)),rewrite(493(8),1732(6),2013(7))]. 5189 (x * i(y)) \ (y / (y * x)) = y / (y / (x \ (y / x))). [para(1091(a,1),1490(a,1,2)),rewrite(3656(3),317(5),203(6)),flip(a)]. 5195 x \ (i(x) \ ((i(y) * x) \ y)) = (i(y) * x) \ y. [para(1438(a,1),1490(a,1,2)),rewrite(524(5),2246(3),1289(6),300(9),202(8),1055(9),847(9),4712(10))]. 5200 (x \ i(y)) \ (x / y) = (y * x) * (x / y). [back_rewrite(3841),rewrite(5122(3))]. 5217 (x * i(y)) * (x / (x * y)) = x / (x / (y \ (x / y))). [back_rewrite(4786),rewrite(5189(10))]. 5234 (x / (x / y)) / ((x * y) / (x * x)) = (i(x) \ y) * (x / (x * y)). [para(1733(a,1),566(a,1,2,2)),rewrite(3501(5),203(11),594(11))]. 5248 (x / (x * y)) \ (i(x) \ y) = (x * y) * y. [para(1733(a,1),930(a,1,2,2)),rewrite(299(5),305(4),300(3),1965(4),203(5),594(5)),flip(a)]. 5364 (x * (y * y)) * (y \ i(x)) = (x * (y * y)) / (i(x) \ y). [para(1748(a,1),854(a,1,2)),rewrite(2876(10))]. 5373 (x * (y * x)) * x = x * (y * (x * x)). [para(1748(a,1),1378(a,1,2,2)),rewrite(4520(4))]. 5376 (x * (y * y)) * (i(x) \ y) = ((y * y) \ i(x)) \ (x * y). [para(1748(a,1),1732(a,2,2)),rewrite(2876(5),426(10),202(8))]. 5379 x / (x * (y * (x * x))) = x \ (y \ i(x)). [para(1748(a,1),594(a,1,1)),rewrite(2576(4),277(2)),flip(a)]. 5388 (x * (y * y)) \ i(y) = y \ ((x * y) \ i(y)). [para(1748(a,1),929(a,1,2,1)),rewrite(362(3)),flip(a)]. 5396 (x \ i(y)) \ (y * y) = y * (x * (y * y)). [back_rewrite(3377),rewrite(5373(7))]. 5406 ((x / y) / y) / (x / y) = x / (x * y). [para(38(a,1),1945(a,1,1,2)),rewrite(594(7))]. 5407 (x * i(y)) * (x * z) = x * ((y \ x) * z). [para(1945(a,1),39(a,1,1)),rewrite(1371(7))]. 5410 ((x * y) * y) / (x * y) = x / (x / y). [para(196(a,1),1945(a,2)),rewrite(188(2),188(3),1133(3),1727(4),188(4),310(8))]. 5417 (x \ y) \ (y \ (y / x)) = x \ (x / y). [para(1945(a,1),1133(a,2,2)),rewrite(1146(3),4736(6),1395(4),1970(7)),flip(a)]. 5423 (x / y) * ((x \ y) / x) = ((x / y) / x) / (x / y). [para(1502(a,1),1945(a,1,1,2)),rewrite(300(8),2266(8)),flip(a)]. 5425 ((x / y) / x) / (x / y) = (y / x) \ ((x \ y) / x). [para(1945(a,1),594(a,1,1)),rewrite(203(5),2576(5),4389(5),854(2),3254(4),1146(9),4396(10),4435(10),5423(8)),flip(a)]. 5427 (x / (x \ y)) / ((y / x) \ (x * x)) = (y / x) \ (x \ (y / x)). [para(1945(a,1),674(a,2,1)),rewrite(203(5),2576(5),3326(5),364(11),203(10),2576(10))]. 5428 (x \ y) * ((y * y) \ x) = x \ (y \ x). [para(3319(a,1),1945(a,1,1,2)),rewrite(926(2),2852(4),300(6),202(5),5014(6)),flip(a)]. 5442 (x \ ((y * x) * x)) / (x \ (y * x)) = (x \ (y \ x)) \ (y \ x). [para(1438(a,1),1945(a,1,1,2)),rewrite(305(4),300(3),202(2),1055(3),847(3),3326(3),3431(3),300(10),2235(11))]. 5446 ((x * y) * x) / (x * y) = (x * y) / (x / (x / y)). [back_rewrite(4288),rewrite(5410(5)),flip(a)]. 5448 (x \ i(y)) \ (x \ (x / y)) = y / (y / x). [back_rewrite(1155),rewrite(5410(9))]. 5461 (x \ (y * y)) \ (x \ y) = x \ (x / y). [back_rewrite(3351),rewrite(5417(8))]. 5464 (x \ y) / (y / (y \ x)) = x \ (x / y). [back_rewrite(1953),rewrite(5417(8))]. 5466 (x \ (x / y)) \ (i(y) * i(x)) = y \ (y / x). [back_rewrite(1610),rewrite(5417(10))]. 5468 (x \ (x / y)) \ (y \ (x \ y)) = x \ y. [back_rewrite(1093),rewrite(5417(4))]. 5471 ((x \ y) / x) \ (x \ ((x \ y) / x)) = (y / x) \ ((x \ y) / x). [back_rewrite(4435),rewrite(5423(10),5425(10))]. 5483 (x / (y * y)) \ (x * i(y)) = y. [para(188(a,1),2031(a,2)),rewrite(673(3),4284(3))]. 5501 (x \ (i(x) \ y)) \ (x * (y * y)) = y \ ((x * y) * y). [para(2031(a,1),1055(a,1,1)),rewrite(731(4),2935(7)),flip(a)]. 5532 ((x * x) \ i(y)) \ (y * x) = (x \ i(y)) \ (x * (y * x)). [para(2031(a,1),930(a,1,2,2)),rewrite(426(5),202(2),202(8)),flip(a)]. 5540 (x * (y * y)) * (i(x) \ y) = (y \ i(x)) \ (y * (x * y)). [back_rewrite(5376),rewrite(5532(10))]. 5690 (i(x) * i(y)) * (y * (y * x)) = (y \ x) \ x. [para(2122(a,1),1131(a,1,1,2)),rewrite(2530(4),926(2),1936(3),2795(7))]. 5691 (x * y) / ((y * x) * y) = i(y). [para(1133(a,1),2122(a,1,1,1)),rewrite(3326(3),3439(3))]. 5725 (i(x) \ y) * (i(x) \ y) = x * (y * (x * y)). [para(2122(a,1),3449(a,1,1,2)),rewrite(305(3),202(2),3326(3),3420(3),3733(5),3709(8))]. 5751 (x * ((y / z) \ z)) * (i(z) * y) = (x * (y / z)) * ((y / z) \ z). [para(2123(a,1),47(a,1,2))]. 5752 (x \ (y / x)) \ (i(x) * y) = x. [para(2123(a,1),962(a,1,2)),rewrite(37(3))]. 5766 (x / y) * (x * x) = ((x \ y) / x) \ x. [para(2123(a,1),1490(a,1,2)),rewrite(5751(8),1055(4),3005(4),3030(7),1502(5),300(6),2266(6))]. 5794 (x / (x \ y)) \ ((y / x) \ (x * x)) = y \ (i(y) \ x). [para(2180(a,1),1371(a,1,2,2)),rewrite(305(6),203(5),2576(5),3326(5),2271(10))]. 5798 (x / (x * y)) / (x / y) = (y / x) \ (x \ (y / x)). [para(2180(a,1),566(a,1,2,2)),rewrite(305(6),203(5),2576(5),3326(5),5427(6),203(8),2576(8),2562(8)),flip(a)]. 5801 ((x \ (y / x)) \ (x / y)) \ (x / y) = y / (x * x). [para(2180(a,1),847(a,2,2)),rewrite(203(3),2576(3),3462(9))]. 5803 ((x * x) \ y) \ i(x) = y \ x. [para(892(a,1),2180(a,1,1,2)),rewrite(990(5),277(2),5014(3),5(5),202(7),188(6))]. 5804 (x / y) \ (x * ((x \ y) \ (x / (x \ y)))) = (y / (x * x)) \ x. [para(2180(a,1),3326(a,1,1)),rewrite(4797(4),3656(9)),flip(a)]. 5825 (x / y) * (x \ (y / x)) = (y / x) \ (x \ (y / x)). [back_rewrite(2562),rewrite(5798(8))]. 5827 (x / y) * (i(x) * ((x / y) \ z)) = ((y / x) \ (x \ (y / x))) * z. [back_rewrite(2491),rewrite(5798(10))]. 5829 (x / (y * y)) * (y * z) = y * (((y \ x) / y) * z). [para(2218(a,1),39(a,2,2,1)),rewrite(364(3),3462(3))]. 5837 (x / y) \ (y \ (y / x)) = (y / x) / x. [para(494(a,1),2218(a,2,1)),rewrite(203(4),1314(5),274(4),2580(8))]. 5845 (((x / y) / y) \ y) / (y / (y \ x)) = y. [para(2218(a,1),1603(a,1,1,2)),rewrite(5129(3),2224(6))]. 5849 (x \ (y \ x)) / (i(y) \ x) = (i(y) \ x) \ (x \ (x / y)). [para(847(a,1),2218(a,2,1)),rewrite(300(5),1268(6),274(5)),flip(a)]. 5858 (x \ y) * (x \ i(y)) = (x \ y) / (y * x). [para(3457(a,1),2218(a,2,1)),rewrite(202(4),5182(5),3725(5))]. 5883 (x * y) \ (x / ((x * y) / x)) = (y \ x) / (x * y). [back_rewrite(3725),rewrite(5858(9))]. 5970 ((x * y) / x) \ (x / y) = (x / y) / y. [para(38(a,1),2224(a,2,2)),rewrite(203(2),319(3))]. 5973 (x * (y * i(z))) \ (z / y) = (z / y) / ((z / y) \ x). [para(203(a,1),2224(a,1,1,2))]. 5976 (x * (i(y) * z)) \ (z \ y) = (z \ y) / ((z \ y) \ x). [para(300(a,1),2224(a,1,1,2))]. 5984 ((x * i(y)) * (i(y) \ z)) \ y = y / (y \ (x * (i(z) \ y))). [para(51(a,1),2224(a,1,1)),rewrite(305(8))]. 5992 (x \ y) / (y \ (x * x)) = ((y / x) \ x) \ (x \ y). [para(3326(a,1),2224(a,2,2)),rewrite(300(2),664(3)),flip(a)]. 5993 (x \ (y \ i(y))) \ y = y * (y * (x * y)). [para(3438(a,1),2224(a,1,1)),rewrite(673(3),3124(8))]. 5994 (x / ((x / y) / x)) \ (x / y) = (x / y) / (y * x). [para(3439(a,1),2224(a,2,2)),rewrite(203(3),5152(4))]. 5997 (x / (x / y)) * y = (x * y) / (y \ x). [para(3457(a,1),2224(a,2,2)),rewrite(202(3),5182(4),3692(5))]. 6005 (x * i(y)) \ (y / (x / y)) = (y \ (x / y)) \ (y / x). [para(2224(a,1),2218(a,2,1)),rewrite(202(5),274(5),1732(4),427(10),203(8),2576(8))]. 6020 (x / ((x * y) / x)) \ (x * y) = (x * y) / (y \ x). [back_rewrite(3692),rewrite(5997(8))]. 6025 (x \ i(y)) \ (z \ (y * x)) = (z / (y * x)) \ (y * x). [para(202(a,1),2253(a,1,1))]. 6028 (i(x) * y) \ (z \ (y \ x)) = (z / (y \ x)) \ (y \ x). [para(300(a,1),2253(a,1,1))]. 6029 ((x \ y) / x) * ((y / x) \ x) = 1. [para(2253(a,1),370(a,1,2)),rewrite(300(2),3445(4))]. 6030 (x * ((y / z) \ z)) * ((y \ z) \ (z \ (y \ z))) = (x * i(z)) * ((y / z) \ z). [para(2253(a,1),47(a,1,1,2)),rewrite(2253(6),2500(7),2253(13))]. 6035 (x * x) \ (y / x) = x \ ((x \ y) / x). [para(2253(a,1),1602(a,2,2)),rewrite(2530(4),5023(4),277(7),300(6),2266(6))]. 6043 (x \ (y \ x)) \ (y \ x) = (y \ x) \ ((y / x) \ x). [para(2253(a,1),796(a,1,2)),flip(a)]. 6044 (i(x) * i(y)) \ ((y \ x) \ x) = y * (y * x). [para(796(a,1),2253(a,1,2)),rewrite(300(3),37(9),2019(10))]. 6052 ((x * x) * y) * x = x * ((x * y) * x). [para(3439(a,1),2253(a,1,2)),rewrite(202(2),4341(4),4799(3),4454(6),3439(8)),flip(a)]. 6059 ((x \ y) / x) \ (i(y) * x) = (y / x) \ ((y / x) \ x). [para(1182(a,1),2253(a,1,2)),rewrite(300(3),2266(3),37(8))]. 6062 (x \ ((x \ y) / x)) \ ((x * x) \ y) = x. [para(2253(a,1),2180(a,1,1,2)),rewrite(277(4),300(3),2266(3),277(6),300(5),4970(6),188(8))]. 6068 (x \ ((y * x) * x)) / (x \ (y * x)) = (y \ x) \ ((y / x) \ x). [back_rewrite(5442),rewrite(6043(10))]. 6072 ((x \ y) \ ((x / y) \ y)) * z = (y \ x) * (y * ((y \ x) \ z)). [back_rewrite(3292),rewrite(6043(4))]. 6129 (x / y) * ((y \ x) / y) = (y / x) \ ((y \ x) / y). [para(2262(a,1),3439(a,1,1)),rewrite(3656(6),3797(7),3(2)),flip(a)]. 6187 (x / (y / x)) \ (y / x) = (x / y) \ ((x \ y) / x). [para(2266(a,1),664(a,1,2)),rewrite(6129(4)),flip(a)]. 6191 (i(x) \ y) \ (y \ (y / x)) = (x * y) \ i(x). [para(847(a,1),2266(a,2,1)),rewrite(300(3),37(6),2545(5),277(2),362(3),5849(8)),flip(a)]. 6196 (x * i(y)) * (y / ((y / x) / y)) = (x * y) / (y / x). [para(3439(a,1),2266(a,2,1)),rewrite(203(2),3932(5))]. 6232 (x \ (y \ x)) / (i(y) \ x) = (y * x) \ i(y). [back_rewrite(5849),rewrite(6191(10))]. 6264 (x \ (y * x)) \ y = (y * x) \ (x * y). [para(28(a,1),95(a,1,2,2)),rewrite(300(4),202(2),2821(4),1784(4),2(4))]. 6294 ((x * y) \ (y * x)) * (x * z) = ((y * x) \ (x * y)) \ (x * z). [para(95(a,1),1055(a,1,1)),rewrite(3821(12))]. 6310 x * (y * ((z * x) \ (x * z))) = (x * y) / ((x * z) \ (z * x)). [para(95(a,1),1602(a,2,2)),rewrite(3821(8),20(5))]. 6373 (x / (y * z)) * (z * y) = x * ((y * z) \ (z * y)). [back_rewrite(2101),rewrite(6264(6),240(8),6264(7))]. 6509 i(x) * ((y * i(z)) \ (i(z) * y)) = x \ ((z / y) * (i(z) * y)). [back_rewrite(316),rewrite(6310(9),304(3),277(7),300(6),202(3),274(3)),flip(a)]. 6639 (x \ (y \ x)) \ (y \ (y / x)) = x \ y. [para(3319(a,1),2269(a,1,2,2)),rewrite(300(4),202(3),5014(4),5428(4),926(4))]. 6650 ((x \ y) / x) \ (y \ x) = (y / x) \ (x / (x \ y)). [para(2269(a,1),1490(a,1,2)),rewrite(3709(5),2577(4),5141(4),202(7),274(7))]. 6662 (x * (y \ (x / y))) * x = (y / x) \ (x / (x \ y)). [back_rewrite(5141),rewrite(6650(8))]. 6673 (x * (y * ((x * z) \ (z * x)))) * (x * y) = (((z * x) \ (x * z)) / (x * y)) \ (x * y). [para(18(a,1),2270(a,2,1)),rewrite(202(2),6294(7),6025(8)),flip(a)]. 6677 (x \ i(y)) \ (z * (y * x)) = ((y * x) * z) * (y * x). [para(202(a,1),2270(a,1,1))]. 6681 (x * i(y)) \ (z * (y / x)) = ((y / x) * z) * (y / x). [para(203(a,1),2270(a,1,1))]. 6686 (x / (x * y)) * (x / y) = (x / y) / y. [para(304(a,1),2270(a,1,2)),rewrite(203(2),309(4),594(5)),flip(a)]. 6697 ((x / y) \ y) * (y / x) = (y \ (x / y)) \ (y / x). [para(1146(a,1),2270(a,2,1)),rewrite(203(2),1732(4),6005(5)),flip(a)]. 6699 ((x * y) * y) * (x * y) = (x * y) * ((y * x) * y). [para(2270(a,1),1602(a,1,2)),rewrite(426(9),202(6),6677(9)),flip(a)]. 6737 (x * (y * y)) * (i(x) \ y) = (x * y) * ((y * x) * y). [back_rewrite(5540),rewrite(6677(10),6699(9))]. 6746 ((x / y) \ y) * ((x / y) \ y) = y * ((y \ x) \ (y / (y \ x))). [back_rewrite(3712),rewrite(6697(4),3969(5)),flip(a)]. 6751 x / (x \ (y / x)) = (y / (x * x)) \ x. [back_rewrite(3799),rewrite(6746(6),5804(7)),flip(a)]. 6758 ((x * y) / (y \ x)) * i(x) = (x / (x / y)) / (x / y). [para(2272(a,1),8(a,1)),rewrite(310(4),310(6),38(5),310(8),5997(7)),flip(a)]. 6770 (x * (y * i(z))) * x = x / (x \ (z / y)). [para(203(a,1),2272(a,1,1,2))]. 6786 x / (x \ (y / (x \ z))) = z * (y \ x). [para(2272(a,1),50(a,2,2,2)),rewrite(39(4),6770(5),1371(7))]. 6807 (x \ (y / x)) * (x \ y) = ((y / x) \ x) \ (x \ y). [para(3326(a,1),2272(a,2,2)),rewrite(2576(3),5992(8))]. 6811 (x / (x \ y)) * i(y) = x * (y \ (x / y)). [para(2272(a,1),3402(a,1,1)),rewrite(4(5),3709(9),2577(8))]. 6882 ((x * x) * y) * ((y \ i(x)) * z) = (y \ i(x)) * ((x * (y * x)) * z). [para(2278(a,1),39(a,2,2,1)),rewrite(426(3),4297(3))]. 6894 x \ ((x / y) * (y \ i(x))) = y \ (y \ i(x)). [para(630(a,1),2278(a,2,2)),rewrite(300(3),188(2),4(2),4466(8)),flip(a)]. 6904 x / (x \ (x \ y)) = (y / x) \ (x * x). [para(3438(a,1),2278(a,2,2)),rewrite(2530(3),3326(3),3475(6)),flip(a)]. 6924 (i(x) \ y) \ ((x / y) / x) = y \ (y \ i(x)). [back_rewrite(4801),rewrite(6894(10))]. 7009 (x * (y * ((x * z) \ (z * x)))) / (((x * z) \ (z * x)) \ (((x * z) \ (z * x)) / (x * y))) = (((z * x) \ (x * z)) / (x * y)) \ (x * y). [para(96(a,1),1732(a,1,2)),rewrite(6673(7),1163(21)),flip(a)]. 7010 x * (y * ((x * z) \ (z * x))) = (x * y) / ((z * x) \ (x * z)). [para(96(a,1),1747(a,1,2)),rewrite(1163(14),7009(15),926(9),1390(9)),flip(a)]. 7206 i(x) * ((i(y) * z) \ (z * i(y))) = x \ ((z \ y) * (z * i(y))). [back_rewrite(315),rewrite(7010(9),304(3),277(7),300(6),202(3),188(2)),flip(a)]. 7214 (x * y) * ((x * z) \ (z * x)) = (x * y) / ((z * x) \ (x * z)). [back_rewrite(18),rewrite(7010(10))]. 7248 (i(x) \ y) * (y \ (x \ i(y))) = i(y). [para(2284(a,1),201(a,1,1)),rewrite(202(5),202(4))]. 7249 x * ((i(y) \ x) * z) = (x * y) * (x * z). [para(2284(a,1),39(a,2,2,1)),rewrite(5(3)),flip(a)]. 7271 (x * y) \ (y * (x * y)) = y \ (((y \ x) \ x) * y). [para(2284(a,1),796(a,2,1)),rewrite(2270(6),877(6),599(4),3312(9)),flip(a)]. 7276 (x * y) \ (x * ((x * x) * y)) = y \ ((x * x) * y). [para(3402(a,1),2284(a,1,2,1)),rewrite(818(4),300(7),877(9),672(7))]. 7291 (x * (x * y)) * x = x * (x * (y * x)). [para(2284(a,1),1490(a,1,2)),rewrite(5139(4),277(3),202(2),5993(4),2270(7)),flip(a)]. 7315 (i(x) \ y) \ ((y * x) * y) = y \ (((y \ x) \ x) * y). [back_rewrite(3312),rewrite(7271(9))]. 7316 (((x \ y) \ y) \ x) * y = y \ (((y \ x) \ x) * y). [back_rewrite(3296),rewrite(7271(8))]. 7318 (x \ (y * x)) \ (i(y) \ x) = x \ (((x \ y) \ y) * x). [back_rewrite(3007),rewrite(7271(9))]. 7557 x * ((x \ y) * (z * (x \ y))) = y * ((z / x) * y). [para(2286(a,1),40(a,2,2)),rewrite(300(2),496(5),5(3),2286(4)),flip(a)]. 7560 (x * (y * (z * y))) / (x * y) = (y \ i(x)) \ (z / x). [para(2286(a,1),42(a,1,1,2)),rewrite(496(9),277(7))]. 7564 (i(x) \ y) * (x / (x * y)) = (x * y) / (x / (x / y)). [para(2286(a,1),319(a,2,1)),rewrite(300(5),319(6),364(5),494(5),2877(10))]. 7597 (x \ (y * (x * x))) * (x \ y) = (x \ y) * (i(x) \ y). [para(1490(a,1),2286(a,2,2)),rewrite(300(2),877(4),3438(3),3420(3))]. 7606 ((x * y) * x) * x = x * ((y * x) * x). [para(2218(a,1),2286(a,1,1)),rewrite(305(4),300(3),2224(4),426(3),2270(3),188(5))]. 7615 (((x / y) \ y) / x) * y = y * ((x \ y) * (x \ y)). [back_rewrite(1181),rewrite(7557(6),3699(3)),flip(a)]. 7616 (x * y) * (y / x) = (x * (y * y)) / x. [back_rewrite(832),rewrite(7560(5),5200(4))]. 7618 (x / (x / y)) / ((x * y) / (x * x)) = (x * y) / (x / (x / y)). [back_rewrite(5234),rewrite(7564(11))]. 7648 (x \ (y * x)) * (i(x) * i(y)) = y \ (y / x). [para(962(a,1),2291(a,1,2,2)),rewrite(300(4),203(3),1282(4),1437(5),1391(5))]. 7668 x * ((x * x) \ y) = i(x) * y. [para(892(a,1),2291(a,1,2,2)),rewrite(202(3),188(2),3(2),990(5),277(2),5014(3))]. 7707 (i(x) * y) \ (y * i(x)) = (y \ x) * (y * i(x)). [para(1(a,1),97(a,2)),rewrite(24(2),26(3),26(5),7206(7),3(6),26(6),26(8)),flip(a)]. 7893 (x \ (y \ z)) \ (i(z) * y) = (y \ z) \ (x / (y \ z)). [para(300(a,1),2530(a,1,2))]. 7904 x * ((y \ x) * (y \ x)) = (x \ (y / x)) \ (y \ x). [para(2530(a,1),3326(a,1,1)),rewrite(3420(9)),flip(a)]. 7928 (((x / y) \ y) / x) * y = (y \ (x / y)) \ (x \ y). [back_rewrite(7615),rewrite(7904(8))]. 7958 (x \ (y / x)) \ (x \ y) = y \ (i(y) \ x). [para(2576(a,1),1133(a,1,1)),rewrite(305(8),300(7),892(8),2550(8))]. 8054 (x / y) * (y \ i(x)) = x * (y \ (y \ i(x))). [para(2621(a,1),3402(a,1,1)),rewrite(6924(5),3656(9),929(8)),flip(a)]. 8059 (x * (x * y)) * (i(y) * i(x)) = x. [para(1182(a,1),2621(a,1,2)),rewrite(305(2),2530(4),277(2),3124(4),1744(4),1171(2),1391(3),427(4),305(3),2019(4))]. 8284 x * ((x \ (y * (x * x))) * z) = (i(y) \ x) * (x * z). [para(2876(a,1),39(a,1,1)),flip(a)]. 8289 (x * (y * y)) * (y \ (z * y)) = ((i(x) \ y) * z) * y. [para(2876(a,1),50(a,1,1,1)),flip(a)]. 8304 (x \ (x \ y)) / ((x * y) \ y) = x \ y. [para(929(a,1),2876(a,2)),rewrite(277(2),305(4),300(3),188(2),277(4),305(6),300(5),188(4),7904(6),5(2),4017(4),277(4),305(6),300(5),188(4),188(7))]. 8332 (x \ (y * y)) \ (i(y) * x) = ((y * y) \ x) * (y \ x). [para(3319(a,1),2888(a,1,1,2)),rewrite(3371(3),4996(6),300(8)),flip(a)]. 8340 (x / (x * y)) \ (y * i(x)) = (x / (x / y)) / (x / y). [para(1091(a,1),2888(a,1,1,2)),rewrite(3462(4),3510(6),203(8)),flip(a)]. 8346 ((x * x) \ y) / x = x \ ((x \ y) / x). [para(2123(a,1),2888(a,1,1,2)),rewrite(4970(3),300(6),2266(6))]. 8392 ((x \ y) \ y) * ((x \ y) \ y) = (y \ x) * (i(x) \ y). [para(2909(a,1),3449(a,1,1,2)),rewrite(926(3),37(2)),flip(a)]. 8419 (((x \ y) / x) * z) / ((x \ y) / x) = ((z * (x / y)) \ ((y / x) \ x)) \ x. [para(3045(a,1),42(a,1,2)),rewrite(305(7),202(6),203(5),300(4),664(5)),flip(a)]. 8808 ((x * (x * ((y * z) \ (z * y)))) \ ((y * z) \ (z * y))) * (((y * z) \ (z * y)) \ (x * x)) = (z * y) \ (y * z). [para(22(a,1),3242(a,1,1,1)),rewrite(300(19),202(17),2821(19))]. 8818 ((x * x) \ y) * (y \ x) = i(x). [para(3242(a,1),196(a,2,2)),rewrite(300(2),3241(5),673(3),5014(3),212(7))]. 8824 (x \ (y \ (x * x))) * (x \ y) = i(x) * ((x \ y) \ y). [para(3242(a,1),47(a,1,1)),rewrite(3438(7),877(7),3438(6)),flip(a)]. 8835 (x \ (y \ x)) * (y \ (y / x)) = x \ i(y). [para(1133(a,1),3242(a,1,2)),rewrite(2162(4),202(7))]. 8839 (x / (y * y)) * y = x * i(y). [para(1502(a,1),3242(a,1,2)),rewrite(6697(4),5801(6),203(5))]. 8846 ((x * y) \ y) \ (y \ ((x \ y) \ y)) = (y \ x) * ((x \ y) \ y). [para(3242(a,1),610(a,1,2,1)),rewrite(277(6),300(5),495(5),300(10),495(10))]. 8919 (x \ (x / y)) \ (x / (y * (x * (y * x)))) = x \ i(y). [para(1171(a,1),3333(a,1,1)),rewrite(3709(5),202(9))]. 8952 x * (y * (x \ (x / y))) = y \ (i(y) \ x). [para(3333(a,1),2272(a,2,2)),rewrite(203(4),4299(4),854(4),570(4),40(4),305(7),203(6),1133(7),305(6))]. 8956 (x / ((x * y) / x)) / (y / (x * x)) = (y / (x * x)) \ (x * i(y)). [para(3333(a,1),2888(a,1,1,2)),rewrite(4332(4),203(10))]. 9100 (x \ i(y)) \ (z * z) = (y * x) * (z * z). [para(202(a,1),3420(a,1,1))]. 9102 (x * i(y)) \ (z * z) = (y / x) * (z * z). [para(203(a,1),3420(a,1,1))]. 9106 (i(x) * y) \ (z * z) = (y \ x) * (z * z). [para(300(a,1),3420(a,1,1))]. 9109 x * ((y * y) \ (z * (y * y))) = (z \ (y / (x / y))) \ (y * y). [para(50(a,1),3420(a,2)),rewrite(202(4),203(3),4299(3)),flip(a)]. 9110 (x * (y * y)) / x = x / (x / (y * y)). [para(3420(a,1),1055(a,1,1)),rewrite(317(4),306(8)),flip(a)]. 9113 (x / (y * y)) / x = x / (x * (y * y)). [para(3420(a,1),674(a,1,2)),flip(a)]. 9130 (x * y) * (x * x) = x * (y * (x * x)). [back_rewrite(5396),rewrite(9100(4))]. 9137 (x * y) * (y / x) = x / (x / (y * y)). [back_rewrite(7616),rewrite(9110(6))]. 9164 x / (y * (x * (y * x))) = y \ (x \ i(y)). [para(5(a,1),3462(a,1,1)),rewrite(202(2),3709(6)),flip(a)]. 9169 ((x \ y) / z) \ (i(y) * x) = z / ((x \ y) * (x \ y)). [para(300(a,1),3462(a,1,2))]. 9172 (x / y) / (y * (i(x) \ (x / y))) = i(x) * i(y). [para(925(a,1),3462(a,1,1)),rewrite(203(3),594(3),1278(3),3656(9),2531(8)),flip(a)]. 9173 x / ((y \ x) * (y \ x)) = (x / y) \ y. [para(926(a,1),3462(a,1,1)),rewrite(300(4),2798(5)),flip(a)]. 9188 (x * y) / ((y \ x) * (i(x) \ y)) = x \ y. [para(2122(a,1),3462(a,1,1)),rewrite(300(4),916(4),2253(4),5(2),8392(7)),flip(a)]. 9199 (x \ (x / y)) \ (y \ (x \ i(y))) = x \ i(y). [back_rewrite(8919),rewrite(9164(6))]. 9204 x / ((x \ y) * (x \ y)) = (y / x) \ ((y / x) \ x). [back_rewrite(6059),rewrite(9169(5))]. 9210 (x / (y * y)) * (y / (y / z)) = ((x / y) * z) * i(y). [para(3500(a,1),8(a,1,1)),rewrite(310(6))]. 9217 (x / (y \ z)) * (i(z) * y) = x / ((y \ z) * (y \ z)). [para(300(a,1),3500(a,1,2))]. 9226 (x * y) \ (x \ (x / y)) = y \ (x \ i(y)). [para(1171(a,1),3500(a,1,1)),rewrite(202(4),1399(5),3709(7),9164(8))]. 9253 (x \ (y / x)) / x = x \ (y / (x * x)). [para(3500(a,1),2218(a,1,2)),flip(a)]. 9267 (x \ (y / x)) \ (y \ x) = (y / x) \ ((y / x) \ x). [back_rewrite(4809),rewrite(9217(5),9204(4)),flip(a)]. 9276 (i(x) * i(y)) * (y \ (y / x)) = x \ (y \ i(x)). [back_rewrite(1737),rewrite(9226(10))]. 9288 (((x / y) \ y) / x) * y = (x / y) \ ((x / y) \ y). [back_rewrite(7928),rewrite(9267(8))]. 9304 i(x) * ((x * x) * y) = x * y. [para(3622(a,1),300(a,1,1)),rewrite(300(3),188(2)),flip(a)]. 9309 (x / (y * y)) / y = (x / y) / (y * y). [para(1732(a,1),3622(a,1,1)),rewrite(3932(4),38(5),3932(5),3462(7))]. 9535 (i(x) * y) * (x \ (y / x)) = (x / (x \ y)) \ (y / x). [para(3646(a,1),1008(a,1,2,2)),rewrite(212(6),203(4),427(5),300(3),203(2),2272(3),300(6)),flip(a)]. 9607 (x * (y * y)) / (y \ ((x * y) \ y)) = (i(y) * i(x)) \ (x * (y * y)). [para(3809(a,1),930(a,1,2,2)),rewrite(2155(5),300(9))]. 9610 (i(x) * i(y)) \ (y * (x * x)) = (y * (x * (y * x))) * x. [para(3809(a,1),1490(a,1,2)),rewrite(5725(5),300(7)),flip(a)]. 9623 (x * (y * y)) / (y \ ((x * y) \ y)) = (x * (y * (x * y))) * y. [back_rewrite(9607),rewrite(9610(12))]. 9625 (x * i(y)) \ (i(y) * x) = y * ((y * x) \ x). [para(1(a,1),124(a,2)),rewrite(24(2),26(3),26(5),1784(7),891(3),26(5),26(7)),flip(a)]. 9630 i(x) \ ((x * y) \ y) = x * ((x * y) \ y). [para(24(a,1),124(a,1,2,1)),rewrite(26(3),26(5),9625(6),1314(5),3(6),26(7),26(9),9625(10),1(9))]. 9652 i(x) * ((x / y) * (x * ((x * z) \ z))) = i(y) * (x * ((x * z) \ z)). [para(494(a,1),124(a,1,2,1)),rewrite(277(6),203(5),4(6),277(8),203(7),4(8),9625(8),850(8),277(11),203(10),4(11),277(13),203(12),4(13),9625(13))]. 9750 i(x) * (y * ((y * z) \ z)) = x \ ((y / z) * (i(y) * z)). [back_rewrite(6509),rewrite(9625(6))]. 9768 i(x) * ((i(x) \ y) * (z * ((z * x) \ x))) = y * (z * ((z * x) \ x)). [back_rewrite(2060),rewrite(9630(7),9630(12))]. 9775 i(x) * ((x / y) * (x * ((x * z) \ z))) = y \ ((x / z) * (i(x) * z)). [back_rewrite(9652),rewrite(9750(12))]. 9793 (x * (y \ (z * y))) / (y * y) = ((x / y) * z) * i(y). [para(50(a,1),3839(a,1,1))]. 9797 x * ((x \ y) \ y) = (y / x) \ (x * y). [para(3839(a,1),1146(a,1,1)),rewrite(5407(4),1055(2),3932(6),5(5))]. 9799 (x / y) \ (((x \ y) / x) \ x) = x * x. [para(3839(a,1),1502(a,1,2,1)),rewrite(3932(3),5(2),9102(5),5766(4))]. 9809 (x * y) / (y \ x) = x / ((y \ x) / y). [para(3402(a,1),3839(a,1,1)),rewrite(3932(5),3932(4),37(3),300(6),1505(7),854(5),5997(6)),flip(a)]. 9826 (x * i(y)) \ (y \ i(x)) = y / ((x * y) * x). [para(3839(a,1),3462(a,1,1)),rewrite(202(4),3709(9),3932(10),4296(9))]. 9833 (x / (x / y)) / (x / y) = x / (x * ((y \ x) / y)). [back_rewrite(6758),rewrite(9809(3),594(5)),flip(a)]. 9835 (x / ((x * y) / x)) \ (x * y) = x / ((y \ x) / y). [back_rewrite(6020),rewrite(9809(8))]. 9836 (x / (x / y)) * y = x / ((y \ x) / y). [back_rewrite(5997),rewrite(9809(6))]. 9857 (x / (x * y)) \ (y * i(x)) = x / (x * ((y \ x) / y)). [back_rewrite(8340),rewrite(9833(9))]. 9861 (x / (x / y)) * (y / x) = x / (x * ((y \ x) / y)). [back_rewrite(1734),rewrite(9833(8))]. 9862 (x \ y) * (x \ y) = ((y / x) \ x) \ y. [para(3(a,1),3840(a,1,2)),rewrite(300(2),664(3)),flip(a)]. 9886 (x / (x * y)) \ ((y / x) \ x) = x * x. [para(1146(a,1),3840(a,1,2)),rewrite(594(3))]. 9887 (i(x) \ y) \ (x / y) = y \ i(y). [para(1370(a,1),3840(a,1,2)),rewrite(300(4),203(3),1282(4),1588(5),1133(3),3676(3),9862(7),1106(5)),flip(a)]. 9890 ((x * x) \ i(y)) \ ((y \ x) \ x) = y * (x * (y * x)). [para(495(a,1),3840(a,1,2)),rewrite(202(3),5023(4),3709(9))]. 9894 ((x / y) \ y) \ x = y \ ((y / x) \ x). [para(664(a,1),3840(a,1,2)),rewrite(202(3),188(2),3(2),3709(8),664(7),3675(7),9862(6)),flip(a)]. 9896 (i(x) \ (x / y)) \ i(y) = y * (x \ (x \ i(y))). [para(836(a,1),3840(a,1,2)),rewrite(203(4),317(4),940(4),2578(4),3656(10),4439(9))]. 9906 (x * (y \ (x / y))) * (y * y) = (y / x) \ (x * y). [para(3840(a,1),1490(a,1,2)),rewrite(3709(5),2577(4),202(8),274(8))]. 9927 (x * (x * y)) \ y = (x * y) \ (x \ y). [para(3061(a,1),3840(a,1,2)),rewrite(300(5),300(4),196(5),2796(5),9862(8),926(5),3326(6),3439(6))]. 9947 x / (y \ ((y / x) \ x)) = (x / y) \ y. [back_rewrite(9173),rewrite(9862(3),9894(3))]. 9959 (x \ y) * (i(y) \ x) = (y \ (y \ x)) \ x. [back_rewrite(8392),rewrite(9862(5),37(2)),flip(a)]. 9998 (x \ ((x / y) \ y)) \ y = (x \ y) \ (y \ (x * y)). [back_rewrite(5144),rewrite(9862(3),9894(3),1055(4),9894(3))]. 10014 (x \ y) \ (i(y) * x) = y \ ((y / x) \ x). [back_rewrite(3761),rewrite(9862(7),9894(7))]. 10021 ((x \ y) / x) * y = x \ ((x / y) \ y). [back_rewrite(3699),rewrite(9862(6),9894(6))]. 10022 i(x) * ((x / y) \ y) = x \ ((x / y) \ y). [back_rewrite(3675),rewrite(9862(7),9894(7))]. 10030 (i(x) * y) \ (y \ x) = y \ ((y / x) \ x). [back_rewrite(733),rewrite(9862(7),9894(7))]. 10039 (x \ y) * (x \ y) = x \ ((x / y) \ y). [back_rewrite(9862),rewrite(9894(6))]. 10050 ((x * ((y * z) \ (z * y))) \ (x \ ((y * z) \ (z * y)))) * (((y * z) \ (z * y)) \ (x * x)) = (z * y) \ (y * z). [back_rewrite(8808),rewrite(9927(9))]. 10064 (x * y) / ((x \ (x \ y)) \ y) = x \ y. [back_rewrite(9188),rewrite(9959(5))]. 10082 (x * i(y)) * (z * z) = (y / x) \ (z * z). [para(203(a,1),3987(a,1,1))]. 10085 ((x * x) \ y) \ y = y \ ((x * x) * y). [para(3987(a,1),196(a,1,1)),rewrite(1055(3))]. 10087 ((x * x) * y) \ y = y \ ((x * x) \ y). [para(3987(a,1),494(a,2,2)),rewrite(305(3),202(2),4341(3),188(4),277(7),300(6),202(5),5014(6))]. 10132 (x \ y) * (y * x) = x \ ((y * y) * x). [back_rewrite(4077),rewrite(10085(5),818(4),7276(5)),flip(a)]. 10165 i(x) \ ((y * z) \ (z * y)) = x * ((y * z) \ (z * y)). [para(22(a,1),4001(a,1,2)),rewrite(4(6)),flip(a)]. 11020 ((x * (y / (z * z))) \ (y * i(z))) \ z = ((z / y) * x) / (z / y). [para(4029(a,1),42(a,1,2)),rewrite(305(7),202(6),203(5))]. 11024 (x / (y * y)) \ (y * i(x)) = (y / (x / y)) / (x / y). [para(4029(a,1),523(a,1,1,2)),rewrite(4332(4),8956(6),203(8),4299(8),1955(9))]. 11068 (x / ((x * y) / x)) / (y / (x * x)) = (x / (y / x)) / (y / x). [back_rewrite(8956),rewrite(11024(11))]. 11070 (x * x) * ((x \ ((y * x) \ x)) * z) = (y \ i(x)) * ((x * x) * z). [para(4074(a,1),39(a,1,1)),rewrite(4090(9)),flip(a)]. 11082 (x \ i(y)) * (x \ y) = (y * x) \ (x \ y). [para(4074(a,1),1146(a,1,1)),rewrite(3932(7),926(6),1378(7))]. 11085 (x * y) \ (x * (y * (x * x))) = x * x. [para(4074(a,1),1502(a,1,2,1)),rewrite(3932(3),926(2),1378(3),9100(5),9130(4))]. 11087 x / (x \ (y * (y * x))) = y \ (y \ x). [para(522(a,1),4074(a,1,1)),rewrite(10039(5),1171(2),1503(4),300(9),202(8),1055(9),847(9),6028(9),37(6))]. 11105 x / (x \ (y \ (y \ x))) = y * (y * x). [para(3141(a,1),4074(a,1,1)),rewrite(10039(5),37(2),300(9),300(8),196(9),6025(9),1171(6),1503(8))]. 11125 (x * x) \ (x * y) = i(x) * y. [para(4075(a,1),212(a,1,1)),rewrite(300(4),188(3),300(5))]. 11126 (x / y) \ (i(x) \ y) = y * y. [para(274(a,1),4075(a,1,1))]. 11139 (x \ (x \ y)) \ y = y \ (x * (x * y)). [para(522(a,1),4075(a,1,2)),rewrite(300(5),202(4),1055(5),847(5),6028(5),37(2),10039(8),1171(5),1503(7))]. 11140 i(x) \ (i(y) \ (y / x)) = x * (i(y) \ (y / x)). [para(567(a,1),4075(a,1,2)),rewrite(203(4),594(4),4439(4),11139(5),1124(4),3656(10),2531(9))]. 11143 i(x) \ (y * (x * y)) = x * (y * (x * y)). [para(796(a,1),4075(a,1,2)),rewrite(300(3),4970(4),9890(6),10039(8),277(6),2278(7)),flip(a)]. 11151 (x * i(y)) \ (x \ i(y)) = y * (x \ (x \ i(y))). [para(929(a,1),4075(a,1,2)),rewrite(203(3),203(2),319(3),610(3),3656(10),929(9),8054(9))]. 11161 (x * y) \ (x \ i(x)) = y \ (x \ (x \ i(x))). [para(4075(a,1),2224(a,2,2)),rewrite(300(4),188(3),10132(3),1468(6),5(3),825(3),362(8),202(7)),flip(a)]. 11163 (x * (x * x)) * y = x * ((x * x) * y). [para(4075(a,1),2266(a,2,1)),rewrite(300(3),188(2),426(5),300(3),877(5),672(3),8(5),426(7),202(5),4341(7),818(6))]. 11175 (x * y) \ (x \ y) = y \ (x \ (x \ y)). [para(3141(a,1),4075(a,1,2)),rewrite(300(5),300(4),196(5),6025(5),1171(2),1503(4),9927(3),10039(8),37(5))]. 11183 i(x) * (y * (x * y)) = (y \ x) \ (x * y). [back_rewrite(4094),rewrite(11125(5))]. 11200 (x * y) / (y \ (x * (x * y))) = x \ y. [back_rewrite(10064),rewrite(11139(4))]. 11230 i(x) \ (y \ (y \ i(x))) = x * (y \ (y \ i(x))). [back_rewrite(11151),rewrite(11175(5))]. 11234 (((x * y) \ (y * x)) \ (z \ (z \ ((x * y) \ (y * x))))) * (((x * y) \ (y * x)) \ (z * z)) = (y * x) \ (x * y). [back_rewrite(10050),rewrite(11175(9))]. 11237 (x * (x * y)) \ y = y \ (x \ (x \ y)). [back_rewrite(9927),rewrite(11175(6))]. 11242 x * (y * (z \ (y / z))) = x / (z * (y \ (z / y))). [para(203(a,1),4284(a,1,2,2)),rewrite(3788(4),3656(7))]. 11243 (x / (x * (y * y))) * z = x * ((y * y) \ (x \ z)). [para(4284(a,1),40(a,1,1,1)),rewrite(9113(3),5014(8))]. 11246 x * (y \ ((y / z) \ z)) = x / (z \ ((z / y) \ y)). [para(300(a,1),4284(a,1,2,2)),rewrite(10014(4),10039(7))]. 11251 ((x / y) / (z * z)) * y = x * (y \ ((z * z) \ y)). [para(4284(a,1),50(a,1,1)),rewrite(5014(7))]. 11571 (x * (y * (x * y))) * (y \ (z * y)) = (y \ i(x)) \ ((x * z) * y). [para(8(a,1),4297(a,1,2)),rewrite(202(2),3709(8)),flip(a)]. 11574 (x \ i(y)) \ ((y * x) * z) = (y * (x * (y * x))) * z. [para(202(a,1),4297(a,1,1)),rewrite(3709(8))]. 11581 (i(x) * y) \ ((y \ x) * z) = (y \ ((y / x) \ x)) * z. [para(300(a,1),4297(a,1,1)),rewrite(10039(8))]. 11588 (i(x) * y) \ ((x \ y) \ y) = (x \ y) \ (y \ (x * y)). [para(1055(a,1),4297(a,1,2)),rewrite(300(2),10039(8),1055(9),9894(8),9998(9))]. 11604 (i(x) * y) \ (y \ (x / y)) = y \ (((y / x) \ x) / y). [para(2576(a,1),4297(a,1,2)),rewrite(300(2),10039(8),2576(10))]. 11634 (x / (y / x)) * (y / (y / z)) = ((x * x) * z) * i(y). [para(4299(a,1),8(a,1,1)),rewrite(310(6))]. 11636 (x * x) * (y \ i(z)) = x / ((z * y) / x). [para(202(a,1),4299(a,1,2))]. 11641 (x * x) * (i(y) * z) = x / ((z \ y) / x). [para(300(a,1),4299(a,1,2))]. 11690 x * (x * ((y / (y * z)) \ i(z))) = x / ((z * (y / (y * z))) / x). [back_rewrite(2484),rewrite(11636(6)),flip(a)]. 11704 (x * (y * y)) * ((y * y) \ z) = (y * y) \ (((y * y) * x) * z). [para(4341(a,1),39(a,2,2,1)),rewrite(426(3),3420(3),5014(5),5014(11))]. 11705 (x * (y \ (x / y))) * z = (y * (x \ (y / x))) \ z. [para(203(a,1),4341(a,1,1,2)),rewrite(3788(4),3656(7)),flip(a)]. 11706 ((x * x) \ (y * (x * x))) * z = (x * x) \ (y * ((x * x) * z)). [para(4341(a,1),40(a,2,2,2)),rewrite(5014(3),426(5),300(3),3987(3),3805(4),5014(11))]. 11708 (x \ ((x / y) \ y)) * z = (y \ ((y / x) \ x)) \ z. [para(300(a,1),4341(a,1,1,2)),rewrite(10014(4),10039(7)),flip(a)]. 11732 (x \ (y / x)) \ y = (y / x) \ (x * y). [back_rewrite(9906),rewrite(11705(5),3457(5))]. 11736 (x * (y \ (x / y))) \ y = (x / y) \ (y / (y \ x)). [back_rewrite(6662),rewrite(11705(4))]. 11740 (x * (y \ (x / y))) \ ((y / x) \ z) = (x * i(y)) \ z. [back_rewrite(5121),rewrite(11705(6))]. 11750 (i(x) * y) \ ((y \ x) * z) = (x \ ((x / y) \ y)) \ z. [back_rewrite(11581),rewrite(11708(9))]. 11833 (x \ (x \ ((y * z) \ (z * y)))) / ((y * z) \ (z * y)) = x \ i(x). [para(673(a,1),156(a,2)),rewrite(4007(7))]. 11882 (x * y) \ (y \ i(x)) = y \ (x \ (y \ i(x))). [para(916(a,1),156(a,1,1,2)),rewrite(202(2),4387(8),3150(7),11833(11),202(3),202(6),202(8),10039(9),305(6),2530(8),277(6))]. 11961 i(x) * (y \ (x \ i(y))) = x \ (y \ (x \ i(y))). [back_rewrite(3679),rewrite(11882(9))]. 12044 (x \ y) * ((y \ x) \ x) = (y \ x) \ ((y \ x) \ x). [para(4365(a,1),929(a,1,2,1)),rewrite(277(6),300(5),495(5),8846(6),300(8),495(8))]. 12064 (i(x) \ y) * ((y \ (((y \ x) \ x) * y)) * z) = (y * x) * (y * z). [para(4506(a,1),39(a,1,1)),rewrite(7249(4),7315(10)),flip(a)]. 12142 (x / (x \ y)) \ (y / x) = x \ (((x / y) \ y) / x). [para(4780(a,1),930(a,1,2,2)),rewrite(212(6),203(4),427(5),300(3),203(2),2272(3),300(6),11604(9))]. 12147 (x \ (y * x)) / (x \ y) = x \ ((y * x) * (y \ x)). [para(4780(a,1),1945(a,1,1,2)),rewrite(305(3),300(2),892(3),300(8),203(7),2272(8),854(8),1967(8))]. 12166 (i(x) * y) * (x \ (y / x)) = x \ (((x / y) \ y) / x). [back_rewrite(9535),rewrite(12142(9))]. 12171 (x \ y) \ ((x / y) \ y) = y \ (x / ((y \ x) / y)). [back_rewrite(6068),rewrite(12147(6),3241(5),317(3),9836(3)),flip(a)]. 12206 (x \ (y / ((x \ y) / x))) * z = (x \ y) * (x * ((x \ y) \ z)). [back_rewrite(6072),rewrite(12171(4))]. 12213 (x \ (y \ x)) \ (y \ x) = x \ (y / ((x \ y) / x)). [back_rewrite(6043),rewrite(12171(8))]. 12495 (x * y) / (x * (y \ i(z))) = (x * ((y * z) * y)) / x. [para(4816(a,1),42(a,1,1,2))]. 12572 (x / y) \ ((y * i(x)) * z) = (x * (y \ (x / y))) \ z. [para(203(a,1),4970(a,1,2,1)),rewrite(3656(8))]. 12574 (x \ y) \ ((i(y) * x) * z) = (x \ ((x / y) \ y)) \ z. [para(300(a,1),4970(a,1,2,1)),rewrite(10039(8))]. 12579 (x * x) \ (y * (x * x)) = x \ (x \ ((y * x) * x)). [para(796(a,1),4970(a,2)),rewrite(3420(4),731(4),3805(8)),flip(a)]. 12591 (x * x) \ (x \ y) = x \ ((x * x) \ y). [para(4352(a,1),4970(a,1,2)),rewrite(673(3),5014(3),188(6)),flip(a)]. 12597 (x \ (x \ ((y * x) * x))) * z = (x * x) \ (y * ((x * x) * z)). [back_rewrite(11706),rewrite(12579(4))]. 12598 x * (y \ (y \ ((z * y) * y))) = (z \ (y / (x / y))) \ (y * y). [back_rewrite(9109),rewrite(12579(4))]. 12623 ((x * x) \ y) * (y \ (z * y)) = ((x * x) \ z) * y. [para(5014(a,1),8(a,1,1)),rewrite(5014(8))]. 12660 (x * i(y)) * ((y / x) \ z) = (y * (x \ (y / x))) \ z. [para(203(a,1),5023(a,1,1)),rewrite(3656(8))]. 12666 x / (x / (y \ (x / y))) = (y / x) \ ((x / y) / x). [para(494(a,1),5023(a,1,2)),rewrite(203(2),5217(5),3656(7),657(9))]. 12669 (i(x) * y) * ((y * y) \ x) = (y * x) \ x. [para(5023(a,1),495(a,1,2)),rewrite(300(2),1172(8),1256(10))]. 12676 (x \ y) * (x \ (y * x)) = (y \ x) \ (x \ (y * x)). [para(892(a,1),5023(a,1,2)),rewrite(202(3),188(2),3709(9),664(8),10022(8),9998(8))]. 12722 (x * i(y)) \ (y / (y * x)) = (x / y) \ ((y / x) / y). [back_rewrite(5189),rewrite(12666(9))]. 12999 ((x \ y) \ y) * ((y * y) \ z) = i(y) * (x * (y \ z)). [para(5072(a,1),40(a,2,2,2)),rewrite(305(4),202(3),188(2))]. 13007 ((x * x) \ y) * (x \ y) = ((x * x) \ y) / (y \ x). [para(5072(a,1),1602(a,1,2)),rewrite(5803(10))]. 13017 ((x * x) \ y) / ((x \ y) \ y) = x \ ((x * x) \ y). [para(5072(a,1),930(a,1,2,2)),rewrite(511(6),188(7))]. 13030 (x \ (y * y)) \ (i(y) * x) = ((y * y) \ x) / (x \ y). [back_rewrite(8332),rewrite(13007(9))]. 13052 (x \ y) * (y \ (x * y)) = x \ (i(x) \ y). [para(5075(a,1),664(a,2,1)),rewrite(300(4),3987(4),3471(5),1172(7))]. 13062 (x \ y) \ (x \ (i(x) \ y)) = y \ (x * y). [para(5075(a,1),1182(a,1,2,1)),rewrite(1172(4),300(8),3987(8),3471(9))]. 13078 (x \ y) * (x * x) = x \ (y * (x * x)). [para(5100(a,1),1055(a,1,1)),rewrite(3437(7),877(7),3438(6),3420(6))]. 13081 (i(x) * i(y)) \ (y \ x) = (i(y) \ x) * (y \ x). [para(5100(a,1),1602(a,1,2)),rewrite(3437(10),429(9),300(7)),flip(a)]. 13092 (x \ y) * (i(x) \ y) = (y \ x) \ (x * y). [para(5100(a,1),3438(a,1,1)),rewrite(10039(10),277(8),2278(9),11143(9),11125(9),11183(8))]. 13093 (x * (y \ (x / y))) \ (((x \ y) / x) \ x) = y * x. [para(3439(a,1),5100(a,2)),rewrite(3656(3),203(5),9102(7),5766(6))]. 13172 (x \ (y * (x * x))) * (x \ y) = (y \ x) \ (x * y). [back_rewrite(7597),rewrite(13092(9))]. 13176 x * (y \ (x / y)) = (x / (x \ y)) / y. [para(38(a,1),5101(a,1,2)