:- module(ring_conn, [step/1, lemma/1]).
:- discontiguous(step/1).
:- discontiguous(lemma/1).
:- style_check(-singleton).
step(add(rule(1, (X1 + X2) = (X2 + X1)))).
step(add(rule(2, ((X1 + X2) + X3) = (X1 + (X2 + X3))))).
step(add(rule(3, (0 + X1) = X1))).
step(add(rule(4, (X1 + -X1) = 0))).
step(add(rule(5, ((X1 * X2) * X3) = (X1 * (X2 * X3))))).
step(add(rule(6, ((X1 * X2) + (X1 * X3)) = (X1 * (X2 + X3))))).
step(add(rule(7, ((X1 * X3) + (X2 * X3)) = ((X1 + X2) * X3)))).
step(add(rule(8, (X1 * (X1 * X1)) = X1))).
step(add(rule(9, -0 = 0))).
step(add(rule(10, (X1 + 0) = X1))).
step(add(rule(11, (X1 + (-X1 + X2)) = X2))).
step(add(rule(12, -(-X1) = X1))).
step(add(rule(13, (X1 + (X2 + X3)) = (X3 + (X1 + X2))))).
step(add(rule(14, (X1 + (X2 + X3)) = (X2 + (X1 + X3))))).
step(add(rule(15, ((X1 + X1) * X2) = (X1 * (X2 + X2))))).
step(add(rule(16, (X2 + (X1 + -X2)) = X1))).
step(add(rule(17, (0 * (X1 + X1)) = (0 * X1)))).
step(add(rule(18, (X1 * (X1 * (X1 * X2))) = (X1 * X2)))).
step(hard((X1 + (X2 + X3)) = (X3 + (X2 + X1)))).
step(hard((X1 + (X2 + X3)) = (X1 + (X3 + X2)))).
step(add(rule(19, (X1 + (X2 + -(X1 + X2))) = 0))).
step(add(rule(20, (X1 + -(-X2 + X1)) = X2))).
step(add(rule(21, (X1 * ((X1 * X1) + X2)) = (X1 + (X1 * X2))))).
step(add(rule(22, (X1 + (X1 * 0)) = X1))).
step(add(rule(23, (X1 * 0) = 0))).
step(add(rule(24, (X1 * (X2 + (X1 * X1))) = (X1 + (X1 * X2))))).
step(add(rule(25, (X2 + -(X1 + X2)) = -X1))).
step(add(rule(26, ((X1 + X1) * (X1 * X1)) = (X1 + X1)))).
step(hard(0 = (X1 + (X2 + -(X2 + X1))))).
step(add(rule(27, (X2 + -(X2 + -X1)) = X1))).
step(add(rule(28, -(-X1 + -X2) = (X2 + X1)))).
step(add(rule(29, (X1 * (0 * X2)) = (0 * X2)))).
step(add(rule(30, (X1 + (X2 * (X1 * X1))) = ((X1 + X2) * (X1 * X1))))).
step(add(rule(31, (X2 + -(X2 + X1)) = -X1))).
step(hard((-X1 + (X2 + (X3 + X1))) = (X3 + X2))).
step(add(rule(32, (X3 + (X2 + (-X3 + X1))) = (X1 + X2)))).
step(add(rule(33, (X3 + (X1 + (X2 + -X3))) = (X1 + X2)))).
step(add(rule(34, -(X1 + -X2) = (X2 + -X1)))).
step(add(rule(35, (-X1 + -X2) = -(X2 + X1)))).
step(add(rule(36, (X1 + (X1 * -(X1 * X1))) = 0))).
step(add(rule(37, (-X1 * -(-X1 * -X1)) = X1))).
step(add(rule(38, (-X1 * (-X1 * X1)) = X1))).
step(add(rule(39, (X1 * -(X1 * X1)) = -X1))).
step(hard((X1 + (X2 + (X3 + X4))) = (X2 + (X3 + (X4 + X1))))).
step(hard((X1 + (X2 + (X3 + X4))) = (X3 + (X2 + (X4 + X1))))).
step(hard((X1 + (X2 + (X3 + X4))) = (X3 + (X4 + (X1 + X2))))).
step(hard((X1 + (X2 + (X3 + X4))) = (X4 + (X3 + (X1 + X2))))).
step(hard((X1 + (X2 + (X3 + X4))) = (X3 + (X1 + (X2 + X4))))).
step(hard((X1 + (X2 + (X3 + X4))) = (X4 + (X2 + (X3 + X1))))).
step(hard((X1 + (X2 + (X3 + X4))) = (X2 + (X4 + (X1 + X3))))).
step(add(rule(40, ((X1 + X1) * (X2 * X3)) = (X1 * ((X2 + X2) * X3))))).
step(add(rule(41, (X1 * (X1 * (X1 + X1))) = (X1 + X1)))).
step(add(rule(42, (X1 * (X2 * (X3 + X3))) = (X1 * ((X2 + X2) * X3))))).
step(add(rule(43, (X1 + (X1 * (X1 * X2))) = (X1 * (X1 * (X1 + X2)))))).
step(add(rule(44, (X1 + (X1 * (X2 * X1))) = (X1 * ((X1 + X2) * X1))))).
step(add(rule(45, (X1 + (0 * X1)) = X1))).
step(add(rule(46, (0 * X1) = 0))).
step(add(rule(47, (X2 + (X3 + (-(X2 + X3) + X1))) = X1))).
step(hard((X1 + (X2 + (-(X2 + X1) + X3))) = X3)).
step(add(rule(48, (X1 * (X1 * -X1)) = -X1))).
step(add(rule(49, -(-X1 + X2) = (X1 + -X2)))).
step(add(rule(50, ((X1 * X2) + ((X1 * X3) + X4)) = ((X1 * (X2 + X3)) + X4)))).
step(add(rule(51, ((X1 * X2) + ((X3 * X2) + X4)) = (((X1 + X3) * X2) + X4)))).
step(add(rule(52, ((X1 * (X2 * X4)) + (X3 * X4)) = (((X1 * X2) + X3) * X4)))).
step(add(rule(53, (((X1 * X1) + X2) * X1) = (X1 + (X2 * X1))))).
step(add(rule(54, (X1 + (-(X1 * X1) * X1)) = 0))).
step(add(rule(55, (-(X1 * X1) * X1) = -X1))).
step(add(rule(56, ((X1 + (X1 * X2)) * X3) = (X1 * (X3 + (X2 * X3)))))).
step(add(rule(57, ((X2 + (X1 * X1)) * X1) = (X1 + (X2 * X1))))).
step(add(rule(58, ((X1 * X4) + (X2 * (X3 * X4))) = ((X1 + (X2 * X3)) * X4)))).
step(add(rule(59, (X1 * (X2 * (X1 * (X2 * (X1 * X2))))) = (X1 * X2)))).
step(add(rule(60, (X1 * ((X1 * (X1 * X2)) + X3)) = (X1 * (X2 + X3))))).
step(add(rule(61, (X1 * (X2 + (X1 * (X1 * X3)))) = (X1 * (X2 + X3))))).
step(add(rule(62, (X1 * (X2 + X2)) = (X1 * (X1 * ((X1 + X1) * X2)))))).
step(add(rule(63, (X1 * (X1 * (X1 + (X1 * X2)))) = (X1 + (X1 * X2))))).
step(add(rule(64, (X1 + (X1 * (-(X1 * X1) + X2))) = (X1 * X2)))).
step(add(rule(65, ((X1 + X1) * (X2 * X3)) = (X1 * (X2 * (X3 + X3)))))).
step(add(rule(66, (-(X1 * X3) + (X1 * (X2 + X3))) = (X1 * X2)))).
step(add(rule(67, -(X1 * -X2) = (X1 * X2)))).
step(add(rule(68, -(X1 * X2) = (X1 * -X2)))).
step(add(rule(69, (X1 * (X2 * (-X2 * -X2))) = (X1 * X2)))).
step(add(rule(70, (-X1 * (X1 * -X1)) = X1))).
step(add(rule(71, (X1 * (-X1 * -X1)) = X1))).
step(add(rule(72, (-X1 * (X1 * X1)) = -X1))).
step(add(rule(73, (X1 * (-X1 * X1)) = -X1))).
step(add(rule(74, ((X2 * -X3) + ((X1 + X2) * X3)) = (X1 * X3)))).
step(add(rule(75, (-X1 * -X2) = (X1 * X2)))).
step(add(rule(76, (-X1 * X2) = (X1 * -X2)))).
step(add(rule(77, (X2 + (X3 + (X1 + -(X2 + X3)))) = X1))).
step(hard(X1 = (X2 + (X3 + (-(X3 + X2) + X1))))).
step(add(rule(78, ((X1 + (X1 * X1)) * (X1 * X1)) = (X1 + (X1 * X1))))).
step(add(rule(79, (X1 + (X1 * ((X1 + X1) * -X1))) = -X1))).
step(add(rule(80, ((X1 * X2) + (X3 + (X1 * X4))) = (X3 + (X1 * (X4 + X2)))))).
step(add(rule(81, ((X1 * X2) + (X3 + (X4 * X2))) = (X3 + ((X4 + X1) * X2))))).
step(add(rule(82, ((X1 + X2) * (X3 + X3)) = ((X1 + (X2 + (X1 + X2))) * X3)))).
step(add(rule(83, ((X1 + (X1 + X2)) * X3) = ((X1 * (X3 + X3)) + (X2 * X3))))).
step(add(rule(84, ((X1 + (X1 + X1)) * X2) = (X1 * (X2 + (X2 + X2)))))).
step(add(rule(85, ((X1 + (X2 + X2)) * X3) = ((X1 * X3) + (X2 * (X3 + X3)))))).
step(hard(((X1 + X2) * (X3 + X3)) = ((X2 + (X1 + (X2 + X1))) * X3))).
step(add(rule(86, ((X1 + X1) * (X2 + X3)) = (X1 * (X2 + (X3 + (X2 + X3))))))).
step(add(rule(87, (X1 * (X2 + (X2 + X3))) = (((X1 + X1) * X2) + (X1 * X3))))).
step(add(rule(88, (X1 * (X2 + (X3 + X3))) = ((X1 * X2) + ((X1 + X1) * X3))))).
step(add(rule(89, (X1 + (X1 * (X2 + X2))) = (X1 + ((X1 + X1) * X2))))).
step(add(rule(90, (X1 * -(X2 + X2)) = ((X1 + X1) * -X2)))).
step(hard(((X1 + X1) * (X2 + X3)) = (X1 * (X3 + (X2 + (X3 + X2)))))).
step(add(rule(91, (X1 * (((X1 * X1) + X2) * X3)) = ((X1 + (X1 * X2)) * X3)))).
step(add(rule(92, (X1 * (X3 + ((X1 * X1) + X2))) = (X1 + (X1 * (X2 + X3)))))).
step(add(rule(93, (X1 * (X2 + (X3 + (X1 * X1)))) = (X1 + (X1 * (X2 + X3)))))).
step(add(rule(94, (X1 * ((X2 + (X1 * X1)) * X3)) = ((X1 + (X1 * X2)) * X3)))).
step(add(rule(95, (X1 + (-(X2 + X1) + X3)) = (-X2 + X3)))).
step(add(rule(96, (X3 + -(X1 + (X2 + X3))) = -(X1 + X2)))).
step(add(rule(97, (X1 + (X2 + -(X3 + X1))) = (X2 + -X3)))).
step(add(rule(98, (((X1 * X1) + X2) * (X1 * X3)) = ((X1 + (X2 * X1)) * X3)))).
step(add(rule(99, ((X1 + (X2 * X3)) * (X3 * X3)) = (((X1 * X3) + X2) * X3)))).
step(add(rule(100, ((X1 + (X2 * X2)) * (X2 * X3)) = ((X2 + (X1 * X2)) * X3)))).
step(add(rule(101, (X1 * (X1 * -(X1 + X1))) = -(X1 + X1)))).
step(add(rule(102, (X1 * (X1 * ((X1 + X1) * X2))) = ((X1 + X1) * X2)))).
step(add(rule(103, ((X1 + (X1 + X1)) * (X1 * X1)) = (X1 + (X1 + X1))))).
step(add(rule(104, ((X1 + (X1 * (X2 * X2))) * X2) = (X1 * (X2 + X2))))).
step(add(rule(105, (((X1 * (X2 * X2)) + X3) * X2) = ((X1 + X3) * X2)))).
step(add(rule(106, (X1 + (X1 * (X2 + (X1 * -X1)))) = (X1 * X2)))).
step(add(rule(107, (X1 + (((X1 * -X1) + X2) * X1)) = (X2 * X1)))).
step(add(rule(108, (X1 + ((X2 + (X1 * -X1)) * X1)) = (X2 * X1)))).
step(add(rule(109, (X1 + ((-X2 + (X1 * X1)) * -X1)) = (X2 * X1)))).
step(add(rule(110, ((X3 * -X2) + ((X3 + X1) * X2)) = (X1 * X2)))).
step(hard(X1 = (X2 + (X3 + (X1 + -(X3 + X2)))))).
step(add(rule(111, ((X3 * X2) + ((X1 + X3) * -X2)) = (X1 * -X2)))).
step(add(rule(112, ((X1 + (X1 + (X1 + X1))) * X2) = (X1 * (X2 + (X2 + (X2 + X2))))))).
step(add(rule(113, ((X1 * X3) + (X2 * (X1 * (X1 * X3)))) = ((X1 + X2) * (X1 * (X1 * X3)))))).
step(add(rule(114, (X1 * ((X1 + X1) * ((X1 + X1) * (X2 + X2)))) = ((X1 + X1) * X2)))).
step(add(rule(115, (((X1 + X2) * (X1 * X1)) + X3) = (X1 + ((X2 * (X1 * X1)) + X3))))).
step(interreduce).
step(delete(rule(11, (X1 + (-X1 + X2)) = X2))).
step(delete(rule(13, (X1 + (X2 + X3)) = (X3 + (X1 + X2))))).
step(delete(rule(17, (0 * (X1 + X1)) = (0 * X1)))).
step(delete(rule(19, (X1 + (X2 + -(X1 + X2))) = 0))).
step(delete(rule(20, (X1 + -(-X2 + X1)) = X2))).
step(delete(rule(21, (X1 * ((X1 * X1) + X2)) = (X1 + (X1 * X2))))).
step(delete(rule(22, (X1 + (X1 * 0)) = X1))).
step(delete(rule(25, (X2 + -(X1 + X2)) = -X1))).
step(delete(rule(26, ((X1 + X1) * (X1 * X1)) = (X1 + X1)))).
step(delete(rule(27, (X2 + -(X2 + -X1)) = X1))).
step(delete(rule(28, -(-X1 + -X2) = (X2 + X1)))).
step(delete(rule(29, (X1 * (0 * X2)) = (0 * X2)))).
step(delete(rule(36, (X1 + (X1 * -(X1 * X1))) = 0))).
step(delete(rule(37, (-X1 * -(-X1 * -X1)) = X1))).
step(delete(rule(38, (-X1 * (-X1 * X1)) = X1))).
step(delete(rule(39, (X1 * -(X1 * X1)) = -X1))).
step(delete(rule(45, (X1 + (0 * X1)) = X1))).
step(delete(rule(47, (X2 + (X3 + (-(X2 + X3) + X1))) = X1))).
step(delete(rule(50, ((X1 * X2) + ((X1 * X3) + X4)) = ((X1 * (X2 + X3)) + X4)))).
step(delete(rule(51, ((X1 * X2) + ((X3 * X2) + X4)) = (((X1 + X3) * X2) + X4)))).
step(delete(rule(53, (((X1 * X1) + X2) * X1) = (X1 + (X2 * X1))))).
step(delete(rule(54, (X1 + (-(X1 * X1) * X1)) = 0))).
step(delete(rule(55, (-(X1 * X1) * X1) = -X1))).
step(delete(rule(60, (X1 * ((X1 * (X1 * X2)) + X3)) = (X1 * (X2 + X3))))).
step(delete(rule(62, (X1 * (X2 + X2)) = (X1 * (X1 * ((X1 + X1) * X2)))))).
step(delete(rule(64, (X1 + (X1 * (-(X1 * X1) + X2))) = (X1 * X2)))).
step(delete(rule(66, (-(X1 * X3) + (X1 * (X2 + X3))) = (X1 * X2)))).
step(delete(rule(67, -(X1 * -X2) = (X1 * X2)))).
step(delete(rule(69, (X1 * (X2 * (-X2 * -X2))) = (X1 * X2)))).
step(delete(rule(70, (-X1 * (X1 * -X1)) = X1))).
step(delete(rule(71, (X1 * (-X1 * -X1)) = X1))).
step(delete(rule(72, (-X1 * (X1 * X1)) = -X1))).
step(delete(rule(73, (X1 * (-X1 * X1)) = -X1))).
step(delete(rule(74, ((X2 * -X3) + ((X1 + X2) * X3)) = (X1 * X3)))).
step(delete(rule(75, (-X1 * -X2) = (X1 * X2)))).
step(delete(rule(77, (X2 + (X3 + (X1 + -(X2 + X3)))) = X1))).
step(delete(rule(78, ((X1 + (X1 * X1)) * (X1 * X1)) = (X1 + (X1 * X1))))).
step(delete(rule(79, (X1 + (X1 * ((X1 + X1) * -X1))) = -X1))).
step(delete(rule(91, (X1 * (((X1 * X1) + X2) * X3)) = ((X1 + (X1 * X2)) * X3)))).
step(delete(rule(95, (X1 + (-(X2 + X1) + X3)) = (-X2 + X3)))).
step(delete(rule(98, (((X1 * X1) + X2) * (X1 * X3)) = ((X1 + (X2 * X1)) * X3)))).
step(delete(rule(107, (X1 + (((X1 * -X1) + X2) * X1)) = (X2 * X1)))).
step(add(rule(116, (X1 + (X2 * (X3 * (X1 * X1)))) = ((X1 + (X2 * X3)) * (X1 * X1))))).
step(add(rule(117, (X1 + (X2 + (X3 * (X1 * X1)))) = (X2 + ((X1 + X3) * (X1 * X1)))))).
step(add(rule(118, (X1 * (X1 * (X1 + (X1 + X1)))) = (X1 + (X1 + X1))))).
step(add(rule(119, ((X1 + (X2 + X2)) * (X1 * X1)) = (X1 + (X2 * (X1 * (X1 + X1))))))).
step(add(rule(120, (X1 + (X1 * (X2 * (X3 * X1)))) = (X1 * (((X2 * X3) + X1) * X1))))).
step(add(rule(121, ((X2 * -X3) + (X1 * X3)) = ((X1 + -X2) * X3)))).
step(add(rule(122, (X1 + (-(X1 + X2) + X3)) = (-X2 + X3)))).
step(add(rule(123, (X1 + (X2 + -(X1 + X3))) = (X2 + -X3)))).
step(add(rule(124, (X3 + -(X1 + (X3 + X2))) = -(X1 + X2)))).
step(add(rule(125, (X1 * (X1 * (X2 + (X1 * X3)))) = (X1 * ((X1 * X2) + X3))))).
step(add(rule(126, ((X3 + (X3 + (X2 + X2))) * X4) = ((X3 + X2) * (X4 + X4))))).
step(hard(((X1 + X2) * (X3 + X3)) = ((X1 + (X2 + (X2 + X1))) * X3))).
step(hard(((X1 + X2) * (X3 + X3)) = ((X2 + (X1 + (X1 + X2))) * X3))).
step(hard(((X1 * (X2 + X2)) + (X3 * X2)) = ((X1 + (X3 + X1)) * X2))).
step(add(rule(127, ((X1 + (X1 + X2)) * X3) = ((X2 * X3) + (X1 * (X3 + X3)))))).
step(hard(((X1 + (X1 + X2)) * X3) = ((X2 + (X1 + X1)) * X3))).
step(hard(((X1 * X2) + (X3 * (X2 + X2))) = ((X3 + (X1 + X3)) * X2))).
step(hard(((X1 + (X2 + X2)) * X3) = ((X2 * (X3 + X3)) + (X1 * X3)))).
step(add(rule(128, (X1 * (X4 + (X4 + (X3 + X3)))) = ((X1 + X1) * (X4 + X3))))).
step(hard(((X1 + X1) * (X2 + X3)) = (X1 * (X2 + (X3 + (X3 + X2)))))).
step(hard(((X1 + X1) * (X2 + X3)) = (X1 * (X3 + (X2 + (X2 + X3)))))).
step(hard((((X1 + X1) * X2) + (X1 * X3)) = (X1 * (X2 + (X3 + X2))))).
step(add(rule(129, (X1 * (X2 + (X2 + X3))) = ((X1 * X3) + ((X1 + X1) * X2))))).
step(hard((X1 * (X2 + (X2 + X3))) = (X1 * (X3 + (X2 + X2))))).
step(hard(((X1 * X2) + ((X1 + X1) * X3)) = (X1 * (X3 + (X2 + X3))))).
step(hard((X1 * (X2 + (X3 + X3))) = (((X1 + X1) * X3) + (X1 * X2)))).
step(add(rule(130, (X1 * ((X1 * (X1 * X2)) + (X3 + X3))) = ((X1 * X2) + ((X1 + X1) * X3))))).
step(add(rule(131, (((X3 * X2) + X1) * (X2 * X2)) = (((X1 * X2) + X3) * X2)))).
step(add(rule(132, (X2 + (-X2 + (X1 * -X2))) = (X1 * -X2)))).
step(add(rule(133, (X1 * ((X1 + X1) * (X1 + (X1 + (X1 + X1))))) = (X1 + X1)))).
step(add(rule(134, (X4 + (X2 + (X3 + (-X4 + X1)))) = (X1 + (X2 + X3))))).
step(add(rule(135, -(X1 + (-X2 + X3)) = (X2 + -(X3 + X1))))).
step(add(rule(136, (X4 + (X1 + (X2 + (X3 + -X4)))) = (X1 + (X2 + X3))))).
step(add(rule(137, -(X1 + (X2 + -X3)) = (X3 + -(X1 + X2))))).
step(add(rule(138, (-X1 + (-X2 + X3)) = (-(X2 + X1) + X3)))).
step(add(rule(139, (-X1 + (X2 + -X3)) = (X2 + -(X3 + X1))))).
step(add(rule(140, -(X3 + (X1 * -X2)) = ((X1 * X2) + -X3)))).
step(add(rule(141, ((X2 * -X3) + -X1) = -(X1 + (X2 * X3))))).
step(add(rule(142, (-X3 + (X1 * -X2)) = -((X1 * X2) + X3)))).
step(add(rule(143, ((X1 + -X2) * -X3) = ((X2 + -X1) * X3)))).
step(add(rule(144, ((X2 + (X1 * (X3 * X3))) * X3) = ((X1 + X2) * X3)))).
step(add(rule(145, ((X1 + X1) * (X1 + (X1 + (X1 + X1)))) = (X1 * (X1 + X1))))).
step(add(rule(146, (X1 + (X1 * ((X1 * -X1) + X2))) = (X1 * X2)))).
step(add(rule(147, (X2 + (-X2 + (X1 * X2))) = (X1 * X2)))).
step(add(rule(148, ((X1 * (X2 + X2)) + ((X1 + X1) * X3)) = ((X1 + X1) * (X2 + X3))))).
step(add(rule(149, (((X1 + X1) * X2) + (X1 * (X3 + X3))) = ((X1 + X1) * (X2 + X3))))).
step(add(rule(150, (X1 + (X1 + ((X1 + X1) * X2))) = ((X1 + X1) * (X2 + (X1 * X1)))))).
step(add(rule(151, (((X1 + X1) * X3) + (X2 * (X3 + X3))) = ((X1 + X2) * (X3 + X3))))).
step(add(rule(152, ((X1 * (X3 + X3)) + ((X2 + X2) * X3)) = ((X1 + X2) * (X3 + X3))))).
step(add(rule(153, (((X1 + X1) * -X2) + X3) = ((X1 * -(X2 + X2)) + X3)))).
step(add(rule(154, ((X1 * (X2 + X2)) + X3) = (((X1 + X1) * X2) + X3)))).
step(add(rule(155, (X1 + ((X2 + X2) * X3)) = (X1 + (X2 * (X3 + X3)))))).
step(add(rule(156, (X1 + ((X1 + (X1 * X1)) * -X1)) = (X1 * -X1)))).
step(add(rule(157, (X2 + ((X1 + (X2 * X2)) * -X2)) = (X1 * -X2)))).
step(add(rule(158, ((((X2 * -X2) + X1) * -X2) + X3) = (X2 + (X3 + (X1 * -X2)))))).
step(add(rule(159, ((X3 * X2) + ((X3 + X1) * -X2)) = (X1 * -X2)))).
step(add(rule(160, (((? * X2) + ((? * X2) + ((X3 + ?) * -(X2 + X2)))) * X4) = (X3 * (X2 * -(X4 + X4)))))).
step(add(rule(161, (((X1 * X2) + ((X1 * X2) + ((X3 + X1) * -(X2 + X2)))) * X4) = (((? * X2) + ((? * X2) + ((X3 + ?) * -(X2 + X2)))) * X4)))).
step(interreduce).
step(delete(rule(63, (X1 * (X1 * (X1 + (X1 * X2)))) = (X1 + (X1 * X2))))).
step(delete(rule(82, ((X1 + X2) * (X3 + X3)) = ((X1 + (X2 + (X1 + X2))) * X3)))).
step(delete(rule(85, ((X1 + (X2 + X2)) * X3) = ((X1 * X3) + (X2 * (X3 + X3)))))).
step(delete(rule(86, ((X1 + X1) * (X2 + X3)) = (X1 * (X2 + (X3 + (X2 + X3))))))).
step(delete(rule(88, (X1 * (X2 + (X3 + X3))) = ((X1 * X2) + ((X1 + X1) * X3))))).
step(delete(rule(89, (X1 + (X1 * (X2 + X2))) = (X1 + ((X1 + X1) * X2))))).
step(delete(rule(96, (X3 + -(X1 + (X2 + X3))) = -(X1 + X2)))).
step(delete(rule(104, ((X1 + (X1 * (X2 * X2))) * X2) = (X1 * (X2 + X2))))).
step(delete(rule(105, (((X1 * (X2 * X2)) + X3) * X2) = ((X1 + X3) * X2)))).
step(delete(rule(109, (X1 + ((-X2 + (X1 * X1)) * -X1)) = (X2 * X1)))).
step(delete(rule(110, ((X3 * -X2) + ((X3 + X1) * X2)) = (X1 * X2)))).
step(delete(rule(111, ((X3 * X2) + ((X1 + X3) * -X2)) = (X1 * -X2)))).
step(delete(rule(122, (X1 + (-(X1 + X2) + X3)) = (-X2 + X3)))).
step(delete(rule(132, (X2 + (-X2 + (X1 * -X2))) = (X1 * -X2)))).
step(delete(rule(133, (X1 * ((X1 + X1) * (X1 + (X1 + (X1 + X1))))) = (X1 + X1)))).
step(delete(rule(134, (X4 + (X2 + (X3 + (-X4 + X1)))) = (X1 + (X2 + X3))))).
step(delete(rule(135, -(X1 + (-X2 + X3)) = (X2 + -(X3 + X1))))).
step(delete(rule(138, (-X1 + (-X2 + X3)) = (-(X2 + X1) + X3)))).
step(delete(rule(156, (X1 + ((X1 + (X1 * X1)) * -X1)) = (X1 * -X1)))).
step(delete(rule(160, (((? * X2) + ((? * X2) + ((X3 + ?) * -(X2 + X2)))) * X4) = (X3 * (X2 * -(X4 + X4)))))).
step(add(rule(162, (((? * X2) + ((? * X2) + ((? + X3) * -(X2 + X2)))) * X4) = (X3 * (X2 * -(X4 + X4)))))).
step(delete(rule(161, (((X1 * X2) + ((X1 * X2) + ((X3 + X1) * -(X2 + X2)))) * X4) = (((? * X2) + ((? * X2) + ((X3 + ?) * -(X2 + X2)))) * X4)))).
step(add(rule(163, (((X1 * X2) + ((X1 * X2) + ((X3 + X1) * -(X2 + X2)))) * X4) = (((? * X2) + ((? * X2) + ((? + X3) * -(X2 + X2)))) * X4)))).
step(add(rule(164, (X1 * (X2 * ((X3 + X3) * X4))) = ((X1 + X1) * (X2 * (X3 * X4)))))).
step(add(rule(165, (X1 * (X2 * ((X3 + X3) * X4))) = (X1 * ((X2 + X2) * (X3 * X4)))))).
step(add(rule(166, ((X1 + X1) * (X2 * ((X2 + X2) * (X2 + X2)))) = (X1 * (X2 + X2))))).
step(add(rule(167, (X1 * (X2 * (X3 * (X4 + X4)))) = (X1 * (X2 * ((X3 + X3) * X4)))))).
step(add(rule(168, (X1 * (((X2 + X2) * X3) + X4)) = (X1 * ((X2 * (X3 + X3)) + X4))))).
step(add(rule(169, (X1 * (X2 + ((X3 + X3) * X4))) = (X1 * (X2 + (X3 * (X4 + X4))))))).
step(add(rule(170, ((X1 * (X1 * (X1 + X2))) + X3) = (X1 + ((X1 * (X1 * X2)) + X3))))).
step(add(rule(171, (X1 + (X2 + (X1 * (X1 * X3)))) = (X2 + (X1 * (X1 * (X1 + X3))))))).
step(add(rule(172, (X1 * (X1 * (X1 + (X2 + X2)))) = (X1 + (X1 * ((X1 + X1) * X2)))))).
step(add(rule(173, ((X1 * ((X1 + X2) * X1)) + X3) = (X1 + ((X1 * (X2 * X1)) + X3))))).
step(add(rule(174, (X1 + (X2 + (X1 * (X3 * X1)))) = (X2 + (X1 * ((X1 + X3) * X1)))))).
step(add(rule(175, (X1 * ((X1 + (X2 + X2)) * X1)) = (X1 + (X1 * (X2 * (X1 + X1))))))).
step(add(rule(176, ((((X1 + X1) * X2) + X3) * X4) = (((X1 * (X2 + X2)) + X3) * X4)))).
step(add(rule(177, ((X1 + (X1 * X2)) * (X3 * X4)) = (X1 * ((X3 + (X2 * X3)) * X4))))).
step(add(rule(178, (X1 * (X2 * (X3 + (X4 * X3)))) = (X1 * ((X2 + (X2 * X4)) * X3))))).
step(add(rule(179, (X1 * (X2 + ((X3 + X3) * X2))) = ((X1 + ((X1 + X1) * X3)) * X2)))).
step(add(rule(180, (X1 * (X2 + (X1 * (X3 * X2)))) = (X1 * (X1 * ((X1 + X3) * X2)))))).
step(add(rule(181, (X1 * (X2 + (X3 * (X1 * X2)))) = (X1 * ((X1 + X3) * (X1 * X2)))))).
step(add(rule(182, ((X1 + (X1 * (X2 * X3))) * X4) = (X1 * (X4 + (X2 * (X3 * X4))))))).
step(add(rule(183, ((X1 + (X1 * (X2 + X2))) * X3) = (X1 * (X3 + (X2 * (X3 + X3))))))).
step(add(rule(184, ((X1 + ((X2 + X2) * X3)) * X4) = ((X1 + (X2 * (X3 + X3))) * X4)))).
step(add(rule(185, (X1 * -(X2 + (X1 * X1))) = -(X1 + (X1 * X2))))).
step(add(rule(186, ((X1 + (X2 * X2)) * -X2) = -(X2 + (X1 * X2))))).
step(add(rule(187, ((X2 * X1) + -(X1 + (X2 * X1))) = -X1))).
step(add(rule(188, ((X1 * X3) + (X2 * -X3)) = ((X1 + -X2) * X3)))).
step(add(rule(189, ((X1 * X2) + (X3 * (X2 + X4))) = ((X3 * X4) + ((X1 + X3) * X2))))).
step(hard(((X1 + (X3 + X1)) * X2) = ((X3 + (X1 + X1)) * X2))).
step(hard(((X1 + (X3 + X1)) * X2) = ((X1 + (X1 + X3)) * X2))).
step(add(rule(190, (X1 + (X1 * ((X1 * X2) + X3))) = (X1 * (X3 + (X1 * (X1 + X2))))))).
step(add(rule(191, (X1 + (X1 * ((X2 * X1) + X3))) = (X1 * (X3 + ((X1 + X2) * X1)))))).
step(hard(((X1 + (X1 + X2)) * (X2 * X2)) = (X2 + (X1 * (X2 * (X2 + X2)))))).
step(hard((X1 + (X1 * (X2 * (X1 + X1)))) = (X1 * ((X2 + (X2 + X1)) * X1)))).
step(hard((X1 + (X1 * ((X1 + X1) * X2))) = (X1 * (X1 * (X2 + (X2 + X1)))))).
step(add(rule(192, (X1 * ((X2 * X3) + ((X2 * X3) + X4))) = (X1 * (((X2 + X2) * X3) + X4))))).
step(add(rule(193, (X1 * (X2 + (X2 + (X3 * X2)))) = ((X1 + (X1 + (X1 * X3))) * X2)))).
step(add(rule(194, (X1 + (X1 + (X1 * (X2 + X2)))) = ((X1 + X1) * ((X1 * X1) + X2))))).
step(add(rule(195, (X1 + (X1 * (X2 + (X1 * X3)))) = (X1 * (X2 + (X1 * (X3 + X1))))))).
step(add(rule(196, (X1 + (X1 * (X2 + (X3 * X1)))) = (X1 * (X2 + ((X3 + X1) * X1)))))).
step(add(rule(197, ((X1 + (X2 + (X1 * X1))) * (X1 * X1)) = (X1 + ((X1 + (X2 * X1)) * X1))))).
step(add(rule(198, ((X1 + (X2 * -X2)) * -X2) = (X2 + (X1 * -X2))))).
step(add(rule(199, (((X2 + X1) * (X1 * X1)) + X3) = (X1 + ((X2 * (X1 * X1)) + X3))))).
step(add(rule(200, (X1 + (((X2 * X1) + X3) * X1)) = ((((X1 + X2) * X1) + X3) * X1)))).
step(add(rule(201, (X1 + ((X2 + X3) * (X2 * X2))) = (X2 + ((X3 * (X2 * X2)) + X1))))).
step(add(rule(202, ((X1 + ((X1 * X1) + X2)) * (X1 * X1)) = ((X1 + ((X2 + X1) * X1)) * X1)))).
step(add(rule(203, (X1 + (X2 + (X3 * (X1 * X1)))) = (X2 + ((X3 + X1) * (X1 * X1)))))).
step(add(rule(204, (X1 + ((X2 + (X3 * X1)) * X1)) = ((X2 + ((X1 + X3) * X1)) * X1)))).
step(hard((X1 + (X2 * (X1 * (X1 + X1)))) = ((X2 + (X1 + X2)) * (X1 * X1)))).
step(add(rule(205, ((X1 + X1) * (X2 + (X2 + X2))) = ((X1 + (X1 + X1)) * (X2 + X2))))).
step(add(rule(206, (X1 * (X2 + (X2 + (X1 * (X1 + X1))))) = ((X1 + X1) * (X2 + (X1 * X1)))))).
step(simplify_queue).
step(interreduce).
step(delete(rule(106, (X1 + (X1 * (X2 + (X1 * -X1)))) = (X1 * X2)))).
step(delete(rule(117, (X1 + (X2 + (X3 * (X1 * X1)))) = (X2 + ((X1 + X3) * (X1 * X1)))))).
step(delete(rule(121, ((X2 * -X3) + (X1 * X3)) = ((X1 + -X2) * X3)))).
step(delete(rule(146, (X1 + (X1 * ((X1 * -X1) + X2))) = (X1 * X2)))).
step(delete(rule(157, (X2 + ((X1 + (X2 * X2)) * -X2)) = (X1 * -X2)))).
step(delete(rule(158, ((((X2 * -X2) + X1) * -X2) + X3) = (X2 + (X3 + (X1 * -X2)))))).
step(delete(rule(159, ((X3 * X2) + ((X3 + X1) * -X2)) = (X1 * -X2)))).
step(delete(rule(190, (X1 + (X1 * ((X1 * X2) + X3))) = (X1 * (X3 + (X1 * (X1 + X2))))))).
step(delete(rule(191, (X1 + (X1 * ((X2 * X1) + X3))) = (X1 * (X3 + ((X1 + X2) * X1)))))).
step(delete(rule(197, ((X1 + (X2 + (X1 * X1))) * (X1 * X1)) = (X1 + ((X1 + (X2 * X1)) * X1))))).
step(add(rule(207, ((X1 + (X2 + (X1 * X1))) * (X1 * X1)) = ((X1 + ((X1 + X2) * X1)) * X1)))).
step(delete(rule(200, (X1 + (((X2 * X1) + X3) * X1)) = ((((X1 + X2) * X1) + X3) * X1)))).
step(delete(rule(202, ((X1 + ((X1 * X1) + X2)) * (X1 * X1)) = ((X1 + ((X2 + X1) * X1)) * X1)))).
step(hard(((X1 + X3) * (X2 + X2)) = ((X3 + X1) * (X2 + X2)))).
step(hard(((X1 + X1) * (X2 + X3)) = ((X1 + X1) * (X3 + X2)))).
step(add(rule(208, (X2 + (X2 + (X1 * (X2 * (X2 + X2))))) = ((X1 + X2) * (X2 * (X2 + X2)))))).
step(add(rule(209, (X1 * ((X1 + X1) * (X1 + X1))) = (X1 + (X1 + (X1 + X1)))))).
step(add(rule(210, (X3 + (X4 + (X2 + (-(X3 + X4) + X1)))) = (X1 + X2)))).
step(add(rule(211, (X3 + (X4 + (X1 + (X2 + -(X3 + X4))))) = (X1 + X2)))).
step(add(rule(212, (X1 * ((X1 * (X1 + X1)) + X2)) = (X1 + (X1 + (X1 * X2)))))).
step(add(rule(213, (X1 * (X2 + (X1 * (X1 + X1)))) = (X1 + (X1 + (X1 * X2)))))).
step(add(rule(214, ((X2 + (X3 + (X1 * X1))) * X1) = (X1 + ((X2 + X3) * X1))))).
step(add(rule(215, (X2 + (X2 + (X1 * (X2 + X2)))) = ((X1 + (X2 * X2)) * (X2 + X2))))).
step(add(rule(216, ((X1 + X1) * (X2 + X2)) = (X1 * ((X1 + X1) * ((X1 + X1) * X2)))))).
step(add(rule(217, ((X1 + X1) * ((X1 + X1) * (X2 + X2))) = (X1 * ((X1 + X1) * X2))))).
step(add(rule(218, (X1 * (X1 * ((X1 * X3) + X2))) = (X1 * ((X1 * X2) + X3))))).
step(hard(((X1 + X2) * (X3 + X3)) = ((X1 + (X2 + (X1 + X2))) * X3))).
step(hard(((X1 + (X1 + (X2 + X2))) * X3) = ((X2 + X1) * (X3 + X3)))).
step(hard(((X1 + X1) * (X2 + X3)) = (X1 * (X2 + (X3 + (X2 + X3)))))).
step(hard((X1 * (X2 + (X2 + (X3 + X3)))) = ((X1 + X1) * (X3 + X2)))).
step(add(rule(219, ((X1 + (X2 * (X2 + X2))) * X2) = (X2 + (X2 + (X1 * X2)))))).
step(add(rule(220, -(X2 + (-X1 + X3)) = (X1 + -(X2 + X3))))).
step(add(rule(221, -((X1 * -X2) + X3) = ((X1 * X2) + -X3)))).
step(add(rule(222, ((? + (-? + X2)) * (X3 + X3)) = ((X2 + X2) * X3)))).
step(add(rule(223, ((X1 + (-X1 + X2)) * (X3 + X3)) = ((? + (-? + X2)) * (X3 + X3))))).
step(add(rule(224, ((X1 + X1) * (? + (-? + X3))) = (X1 * (X3 + X3))))).
step(add(rule(225, ((X1 + X1) * (X2 + (-X2 + X3))) = ((X1 + X1) * (? + (-? + X3)))))).
step(add(rule(226, ((-X1 + X2) * -X3) = ((X1 + -X2) * X3)))).
step(add(rule(227, ((X1 * X2) + -(X3 + (X1 * X2))) = -X3))).
step(add(rule(228, (((X1 + X1) * X2) + X3) = (X3 + (X1 * (X2 + X2)))))).
step(add(rule(229, ((X1 * (X2 + X2)) + X3) = (X3 + ((X1 + X1) * X2))))).
step(add(rule(230, (X1 * (X2 * (X1 * (X2 * (X1 * (X2 * X3)))))) = (X1 * (X2 * X3))))).
step(add(rule(231, ((X1 * (X2 * X3)) + ((X4 * X3) + X5)) = ((((X1 * X2) + X4) * X3) + X5)))).
step(add(rule(232, ((X1 * (X2 * (X3 * X5))) + (X4 * X5)) = (((X1 * (X2 * X3)) + X4) * X5)))).
step(add(rule(233, ((X1 * (X2 * X5)) + (X3 * (X4 * X5))) = (((X1 * X2) + (X3 * X4)) * X5)))).
step(add(rule(234, ((X1 * (X2 * X3)) + (X4 + (X5 * X3))) = (X4 + (((X1 * X2) + X5) * X3))))).
step(add(rule(235, ((((X1 + X1) * X2) + X3) * X4) = ((X1 * (X2 * (X4 + X4))) + (X3 * X4))))).
step(add(rule(236, ((X1 + ((X1 + X1) * X2)) * X3) = (X1 * (X3 + (X2 * (X3 + X3))))))).
step(add(rule(237, (((X1 * (X2 + X2)) + X3) * X4) = ((X1 * (X2 * (X4 + X4))) + (X3 * X4))))).
step(add(rule(238, (((X1 * X2) + (X3 + X3)) * X4) = ((X1 * (X2 * X4)) + (X3 * (X4 + X4)))))).
step(add(rule(239, (((X1 * X1) + (X2 + X2)) * X1) = (X1 + (X2 * (X1 + X1)))))).
step(add(rule(240, ((X1 + X1) * ((X2 + (X1 * X1)) * X3)) = ((X1 + X1) * (X3 + (X2 * X3)))))).
step(add(rule(241, ((X2 + ((X1 * X1) + X2)) * X1) = (X1 + (X2 * (X1 + X1)))))).
step(add(rule(242, (((X1 * X2) + X3) * (X2 * (X2 * X4))) = ((X1 + (X3 * X2)) * (X2 * X4))))).
step(add(rule(243, ((X1 + (X1 * (X2 * -X2))) * (X2 * X3)) = 0))).
step(add(rule(244, (X1 * (X2 + (X2 * (X1 * -X1)))) = 0))).
step(add(rule(245, ((X1 + (X1 * (X2 * -X2))) * (X2 + X2)) = 0))).
step(add(rule(246, (X1 * ((X2 + (X2 * (X1 * -X1))) * X3)) = 0))).
step(add(rule(247, ((X1 + (X1 * (X2 * -X2))) * -X2) = 0))).
step(add(rule(248, (X1 * -(X2 + (X2 * (X1 * -X1)))) = 0))).
step(add(rule(249, (X1 * (-X2 + (X2 * (X1 * X1)))) = 0))).
step(add(rule(250, ((X1 * X2) + ((X3 * (X4 * X2)) + X5)) = (((X1 + (X3 * X4)) * X2) + X5)))).
step(add(rule(251, ((X1 * X5) + (X2 * (X3 * (X4 * X5)))) = ((X1 + (X2 * (X3 * X4))) * X5)))).
step(add(rule(252, ((X1 * X2) + (X3 + (X4 * (X5 * X2)))) = (X3 + ((X1 + (X4 * X5)) * X2))))).
step(add(rule(253, (X1 + ((X2 + (X1 * X3)) * X1)) = ((X2 + (X1 * (X1 + X3))) * X1)))).
step(add(rule(254, ((X1 + (X1 + (X2 * X3))) * X4) = ((X1 * (X4 + X4)) + (X2 * (X3 * X4)))))).
step(add(rule(255, ((X1 + ((X2 + X2) * X3)) * X4) = ((X1 * X4) + (X2 * (X3 * (X4 + X4))))))).
step(add(rule(256, ((X1 + (X2 * (X3 + X3))) * X4) = ((X1 * X4) + (X2 * (X3 * (X4 + X4))))))).
step(add(rule(257, ((X1 + (X2 * X3)) * (X3 * (X3 * X4))) = (((X1 * X3) + X2) * (X3 * X4))))).
step(add(rule(258, (X1 * ((X2 * (X1 * (X2 * (X1 * X2)))) + X3)) = (X1 * (X2 + X3))))).
step(add(rule(259, (X1 * (X2 + (X3 * (X1 * (X3 * (X1 * X3)))))) = (X1 * (X2 + X3))))).
step(add(rule(260, (X2 + ((X1 + X2) * (X2 * -X2))) = (X1 * (X2 * -X2))))).
step(add(rule(261, (X1 * (X2 * -(X3 + X3))) = (X1 * ((X2 + X2) * -X3))))).
step(add(rule(262, (X1 * (X2 + (X3 * X2))) = (X1 * (X1 * ((X1 + (X1 * X3)) * X2)))))).
step(add(rule(263, (X1 * (X2 + (X3 + (X1 * (X1 * X4))))) = (X1 * (X2 + (X3 + X4)))))).
step(add(rule(264, (X1 * ((X2 + (X1 * (X1 * X3))) * X4)) = (X1 * ((X2 + X3) * X4))))).
step(add(rule(265, (X1 * (X2 + (X3 + X3))) = (X1 * (X2 + (X1 * ((X1 + X1) * X3))))))).
step(add(rule(266, (X1 * (X2 + (X1 * (X1 + (X1 * X3))))) = (X1 + (X1 * (X2 + X3)))))).
step(add(rule(267, (X1 * (X2 * -(X3 + X3))) = ((X1 + X1) * (X2 * -X3))))).
step(add(rule(268, ((X1 + (X1 * X2)) * -X3) = (X1 * -(X3 + (X2 * X3)))))).
step(add(rule(269, (X1 + (X2 * (X1 * -X1))) = ((X1 + -X2) * (X1 * X1))))).
step(add(rule(270, ((X1 + X1) * (X1 + X1)) = (X1 * -(X1 + X1))))).
step(add(rule(271, ((X1 + X1) * -(X1 + X1)) = (X1 * (X1 + X1))))).
step(add(rule(272, (X1 + (X1 + (X1 + X1))) = -(X1 + X1)))).
step(add(rule(273, -(X1 + (X1 + X1)) = (X1 + (X1 + X1))))).
step(add(rule(274, (-X1 + (X2 * (X1 * X1))) = ((-X1 + X2) * (X1 * X1))))).
step(add(rule(275, -(X1 + (X1 * (X2 * -X1))) = (X1 * ((X2 + -X1) * X1))))).
step(add(rule(276, (X1 + (X1 * (X2 * -X1))) = (X1 * ((X1 + -X2) * X1))))).
step(add(rule(277, ((X1 + (X1 * -X2)) * X3) = (X1 * (X3 + (X2 * -X3)))))).
step(add(rule(278, (X1 * (X2 + (X2 + X2))) = ((X1 + (X1 + X1)) * -X2)))).
step(add(rule(279, ((X1 + X1) * (X2 + (X2 + X2))) = 0))).
step(interreduce).
step(delete(rule(108, (X1 + ((X2 + (X1 * -X1)) * X1)) = (X2 * X1)))).
step(delete(rule(112, ((X1 + (X1 + (X1 + X1))) * X2) = (X1 * (X2 + (X2 + (X2 + X2))))))).
step(delete(rule(113, ((X1 * X3) + (X2 * (X1 * (X1 * X3)))) = ((X1 + X2) * (X1 * (X1 * X3)))))).
step(delete(rule(114, (X1 * ((X1 + X1) * ((X1 + X1) * (X2 + X2)))) = ((X1 + X1) * X2)))).
step(delete(rule(145, ((X1 + X1) * (X1 + (X1 + (X1 + X1)))) = (X1 * (X1 + X1))))).
step(delete(rule(154, ((X1 * (X2 + X2)) + X3) = (((X1 + X1) * X2) + X3)))).
step(delete(rule(166, ((X1 + X1) * (X2 * ((X2 + X2) * (X2 + X2)))) = (X1 * (X2 + X2))))).
step(add(rule(280, ((X1 + X1) * -(X2 + X2)) = (X1 * (X2 + X2))))).
step(delete(rule(187, ((X2 * X1) + -(X1 + (X2 * X1))) = -X1))).
step(delete(rule(205, ((X1 + X1) * (X2 + (X2 + X2))) = ((X1 + (X1 + X1)) * (X2 + X2))))).
step(add(rule(281, ((X1 + (X1 + X1)) * (X2 + X2)) = 0))).
step(delete(rule(209, (X1 * ((X1 + X1) * (X1 + X1))) = (X1 + (X1 + (X1 + X1)))))).
step(delete(rule(210, (X3 + (X4 + (X2 + (-(X3 + X4) + X1)))) = (X1 + X2)))).
step(delete(rule(212, (X1 * ((X1 * (X1 + X1)) + X2)) = (X1 + (X1 + (X1 * X2)))))).
step(delete(rule(231, ((X1 * (X2 * X3)) + ((X4 * X3) + X5)) = ((((X1 * X2) + X4) * X3) + X5)))).
step(delete(rule(242, (((X1 * X2) + X3) * (X2 * (X2 * X4))) = ((X1 + (X3 * X2)) * (X2 * X4))))).
step(delete(rule(247, ((X1 + (X1 * (X2 * -X2))) * -X2) = 0))).
step(delete(rule(250, ((X1 * X2) + ((X3 * (X4 * X2)) + X5)) = (((X1 + (X3 * X4)) * X2) + X5)))).
step(delete(rule(258, (X1 * ((X2 * (X1 * (X2 * (X1 * X2)))) + X3)) = (X1 * (X2 + X3))))).
step(delete(rule(260, (X2 + ((X1 + X2) * (X2 * -X2))) = (X1 * (X2 * -X2))))).
step(delete(rule(271, ((X1 + X1) * -(X1 + X1)) = (X1 * (X1 + X1))))).
step(delete(rule(275, -(X1 + (X1 * (X2 * -X1))) = (X1 * ((X2 + -X1) * X1))))).
step(add(rule(282, ((X1 + (X1 + X1)) * -(X2 + X2)) = 0))).
step(add(rule(283, ((X1 + X1) * (X2 + X2)) = (X1 * -(X2 + X2))))).
step(add(rule(284, ((X1 + (X1 + X1)) * ((X2 + X2) * X3)) = 0))).
step(add(rule(285, ((X1 + (X1 + X1)) * (X2 * (X3 + X3))) = 0))).
step(add(rule(286, ((X1 + X1) * ((X2 + (X2 + X2)) * X3)) = 0))).
step(add(rule(287, (((X1 + X1) * X2) + (((X1 + X1) * X2) + (((X1 + X1) * X2) + X3))) = X3))).
step(add(rule(288, (((X1 + (X1 + X1)) * X2) + (((X1 + (X1 + X1)) * X2) + X3)) = X3))).
step(add(rule(289, ((X1 + X1) * (X2 + (X2 * (X1 * (X1 + X1))))) = 0))).
step(add(rule(290, ((X1 + (X1 * (X2 * (X2 + X2)))) * (X2 + X2)) = 0))).
step(add(rule(291, ((X1 + X1) * (X2 * (X3 + (X3 + X3)))) = 0))).
step(add(rule(292, (X1 * (X2 + (X2 + X3))) = (X1 * ((X1 * ((X1 + X1) * X2)) + X3))))).
step(add(rule(293, ((X1 + (X1 + X1)) * (X1 * ((X1 + X1) * X2))) = 0))).
step(add(rule(294, ((X1 + (X1 + X1)) * (X1 * -(X1 + X1))) = 0))).
step(add(rule(295, (X1 * (-X2 + (-X2 + X3))) = (X1 * (-(X2 + X2) + X3))))).
step(add(rule(296, (X1 * (X1 * ((X1 + (X1 * X2)) * X3))) = ((X1 + (X1 * X2)) * X3)))).
step(add(rule(297, (((X1 * (X2 * (X3 * X3))) + X4) * X3) = (((X1 * X2) + X4) * X3)))).
step(add(rule(298, (((X1 * (X2 * (X2 + X2))) + X3) * X2) = ((X1 + (X1 + X3)) * X2)))).
step(add(rule(299, (X1 * (-(X2 + X2) + X3)) = (X1 * (X3 + -(X2 + X2)))))).
step(add(rule(300, ((X1 * -(X2 + X2)) + X3) = (X3 + ((X1 + X1) * -X2))))).
step(add(rule(301, (X1 + ((X2 + X2) * -X3)) = (X1 + (X2 * -(X3 + X3)))))).
step(add(rule(302, -(X3 + ((X1 + X1) * X2)) = -(X3 + (X1 * (X2 + X2)))))).
step(add(rule(303, (((X1 + X1) * -X2) + X3) = (X3 + (X1 * -(X2 + X2)))))).
step(add(rule(304, (((X1 * (X2 * X2)) + X3) * (X2 * X4)) = ((X1 + X3) * (X2 * X4))))).
step(add(rule(305, ((X1 + (X2 * (X3 * X3))) * (X3 * X4)) = ((X1 + X2) * (X3 * X4))))).
step(add(rule(306, (X1 * ((X1 * -X1) + X2)) = (-X1 + (X1 * X2))))).
step(add(rule(307, (X1 + (-X1 + (X1 * X2))) = (X1 * X2)))).
step(add(rule(308, (X1 * (X2 + (X1 * -X1))) = (-X1 + (X1 * X2))))).
step(add(rule(309, (X1 * (X2 * (X3 * (X4 + X4)))) = ((X1 + X1) * (X2 * (X3 * X4)))))).
step(add(rule(310, (X1 * (X2 * (X3 * (X4 + X4)))) = (X1 * ((X2 + X2) * (X3 * X4)))))).
step(add(rule(311, ((X1 + X1) * (X2 * (X3 + X3))) = (X1 * (X2 * -(X3 + X3)))))).
step(add(rule(312, ((X1 + X1) * ((X2 + X2) * X3)) = (X1 * (X2 * -(X3 + X3)))))).
step(add(rule(313, ((X1 * (X2 + X2)) + ((X3 + -X1) * X2)) = ((X1 + X3) * X2)))).
step(add(rule(314, ((X1 * (X2 + X2)) + ((-X1 + X3) * X2)) = ((X3 + X1) * X2)))).
step(add(rule(315, ((X1 + (X1 + X1)) * (X2 * X3)) = (X1 * ((X2 + (X2 + X2)) * X3))))).
step(add(rule(316, (X1 * (X2 * (X3 + (X3 + X3)))) = (X1 * ((X2 + (X2 + X2)) * X3))))).
step(add(rule(317, (((X1 + X1) * X2) + (X1 * (X3 + -X2))) = (X1 * (X2 + X3))))).
step(add(rule(318, (((X1 + X1) * X2) + (X1 * (-X2 + X3))) = (X1 * (X3 + X2))))).
step(add(rule(319, (X1 * (X2 + (X2 * (X1 * X1)))) = ((X1 + X1) * X2)))).
step(add(rule(320, (X1 + (X1 * (X2 + ((X1 * -X1) + X3)))) = (X1 * (X3 + X2))))).
step(hard(((X1 + (X1 + (X2 + X2))) * X3) = ((X1 + (X2 + (X1 + X2))) * X3))).
step(hard((X1 * (X2 + (X2 + (X3 + X3)))) = (X1 * (X2 + (X3 + (X2 + X3)))))).
step(add(rule(321, (X1 * (((X2 + X2) * X3) + X4)) = (X1 * (X4 + ((X2 + X2) * X3)))))).
step(add(rule(322, (X1 * (((X2 + X2) * X3) + X4)) = (X1 * (X4 + (X2 * (X3 + X3))))))).
step(add(rule(323, (X1 * ((X2 * (X3 + X3)) + X4)) = (X1 * (X4 + ((X2 + X2) * X3)))))).
step(add(rule(324, (X1 + (X1 * (X2 * (X3 + X3)))) = (X1 + (X1 * ((X2 + X2) * X3)))))).
step(hard((X1 * (X2 * (X3 + (X4 + X4)))) = (X1 * (X2 * (X4 + (X4 + X3)))))).
step(hard((X1 * ((X2 + (X4 + X4)) * X3)) = (X1 * ((X4 + (X4 + X2)) * X3)))).
step(add(rule(325, ((X1 * (X1 * (X2 + X1))) + X3) = (X1 + ((X1 * (X1 * X2)) + X3))))).
step(add(rule(326, (X1 + (X2 * (X2 * (X2 + X3)))) = (X2 + ((X2 * (X2 * X3)) + X1))))).
step(add(rule(327, (X1 + (X2 + (X1 * (X1 * X3)))) = (X2 + (X1 * (X1 * (X3 + X1))))))).
step(hard((X1 + (X1 * ((X1 + X1) * X2))) = (X1 * (X1 * (X2 + (X1 + X2)))))).
step(add(rule(328, ((X1 * ((X2 + X1) * X1)) + X3) = (X1 + ((X1 * (X2 * X1)) + X3))))).
step(add(rule(329, (X1 + (X2 * ((X2 + X3) * X2))) = (X2 + ((X2 * (X3 * X2)) + X1))))).
step(add(rule(330, (X1 + (X2 + (X1 * (X3 * X1)))) = (X2 + (X1 * ((X3 + X1) * X1)))))).
step(hard((X1 + (X1 * (X2 * (X1 + X1)))) = (X1 * ((X2 + (X1 + X2)) * X1)))).
step(add(rule(331, (((X1 * (X2 + X2)) + X3) * X4) = ((X3 + ((X1 + X1) * X2)) * X4)))).
step(add(rule(332, ((((X1 + X1) * X2) + X3) * X4) = ((X3 + (X1 * (X2 + X2))) * X4)))).
step(add(rule(333, ((X1 + (X1 * X2)) * (X2 * X3)) = (X1 * (X2 * (X3 + (X2 * X3))))))).
step(add(rule(334, ((X1 + X1) * (X2 + (X1 * ((X1 + X1) * X2)))) = 0))).
step(add(rule(335, (X1 * (X1 * ((X1 + X2) * X2))) = (X1 * ((X2 + X1) * (X2 * X2)))))).
step(add(rule(336, (X1 * (X2 + (X1 * (X3 * X2)))) = (X1 * (X1 * ((X3 + X1) * X2)))))).
step(add(rule(337, (X1 * ((X1 + X2) * (X1 * X2))) = (X1 * (X2 * ((X2 + X1) * X2)))))).
step(add(rule(338, (X1 * (X2 + (X3 * (X1 * X2)))) = (X1 * ((X3 + X1) * (X1 * X2)))))).
step(add(rule(339, (X1 * -(X2 + (X1 * (X1 * -X2)))) = 0))).
step(add(rule(340, ((X1 + (X1 * (X2 * X3))) * X3) = (X1 * ((X3 + X2) * (X3 * X3)))))).
step(add(rule(341, ((X1 + (X1 * (X2 * -X2))) * X2) = 0))).
step(add(rule(342, ((X1 + (X1 * (X2 * -X2))) * -X2) = 0))).
step(add(rule(343, ((X1 + (X1 * (X2 * X3))) * X2) = (X1 * (X2 * ((X2 + X3) * X2)))))).
step(add(rule(344, (X1 * -((X1 * X1) + X2)) = -(X1 + (X1 * X2))))).
step(add(rule(345, (((X1 * X1) + X2) * -X1) = -(X1 + (X2 * X1))))).
step(add(rule(346, ((X1 * X2) + ((X3 + X1) * X4)) = ((X1 * (X4 + X2)) + (X3 * X4))))).
step(hard((X1 * (X2 + (X3 + X2))) = (X1 * (X3 + (X2 + X2))))).
step(hard((X1 * (X2 + (X3 + X2))) = (X1 * (X2 + (X2 + X3))))).
step(add(rule(347, ((X1 * -X2) + ((X3 + X1) * X2)) = (X3 * X2)))).
step(add(rule(348, ((X1 * X2) + ((X3 + X1) * X4)) = ((X3 * X4) + (X1 * (X2 + X4)))))).
step(add(rule(349, (X1 * (X2 + -(X3 + X2))) = (X1 * -X3)))).
step(add(rule(350, ((X1 + -(X3 + X1)) * X2) = (X3 * -X2)))).
step(add(rule(351, (((X1 * X2) + (X4 + X1)) * X3) = ((X4 + (X1 + (X1 * X2))) * X3)))).
step(interreduce).
step(delete(rule(103, ((X1 + (X1 + X1)) * (X1 * X1)) = (X1 + (X1 + X1))))).
step(delete(rule(153, (((X1 + X1) * -X2) + X3) = ((X1 * -(X2 + X2)) + X3)))).
step(delete(rule(168, (X1 * (((X2 + X2) * X3) + X4)) = (X1 * ((X2 * (X3 + X3)) + X4))))).
step(delete(rule(171, (X1 + (X2 + (X1 * (X1 * X3)))) = (X2 + (X1 * (X1 * (X1 + X3))))))).
step(delete(rule(174, (X1 + (X2 + (X1 * (X3 * X1)))) = (X2 + (X1 * ((X1 + X3) * X1)))))).
step(delete(rule(180, (X1 * (X2 + (X1 * (X3 * X2)))) = (X1 * (X1 * ((X1 + X3) * X2)))))).
step(delete(rule(181, (X1 * (X2 + (X3 * (X1 * X2)))) = (X1 * ((X1 + X3) * (X1 * X2)))))).
step(delete(rule(189, ((X1 * X2) + (X3 * (X2 + X4))) = ((X3 * X4) + ((X1 + X3) * X2))))).
step(delete(rule(216, ((X1 + X1) * (X2 + X2)) = (X1 * ((X1 + X1) * ((X1 + X1) * X2)))))).
step(add(rule(352, (X1 * -(X2 + X2)) = (X1 * ((X1 + X1) * ((X1 + X1) * X2)))))).
step(delete(rule(217, ((X1 + X1) * ((X1 + X1) * (X2 + X2))) = (X1 * ((X1 + X1) * X2))))).
step(delete(rule(262, (X1 * (X2 + (X3 * X2))) = (X1 * (X1 * ((X1 + (X1 * X3)) * X2)))))).
step(delete(rule(270, ((X1 + X1) * (X1 + X1)) = (X1 * -(X1 + X1))))).
step(delete(rule(288, (((X1 + (X1 + X1)) * X2) + (((X1 + (X1 + X1)) * X2) + X3)) = X3))).
step(delete(rule(293, ((X1 + (X1 + X1)) * (X1 * ((X1 + X1) * X2))) = 0))).
step(delete(rule(294, ((X1 + (X1 + X1)) * (X1 * -(X1 + X1))) = 0))).
step(delete(rule(304, (((X1 * (X2 * X2)) + X3) * (X2 * X4)) = ((X1 + X3) * (X2 * X4))))).
step(delete(rule(306, (X1 * ((X1 * -X1) + X2)) = (-X1 + (X1 * X2))))).
step(delete(rule(341, ((X1 + (X1 * (X2 * -X2))) * X2) = 0))).
step(add(rule(353, (X1 * ((X1 + X1) * ((X1 + X1) * X2))) = ((X1 + X1) * -X2)))).
step(add(rule(354, (X1 + (X1 + (X1 * (X2 + X2)))) = ((X1 + X1) * (X2 + (X1 * X1)))))).
step(add(rule(355, (X1 + (X1 * ((X1 * X3) + X2))) = (X1 * (X2 + (X1 * (X3 + X1))))))).
step(add(rule(356, (X1 * (X2 + (X1 * (X2 + X1)))) = (X1 + ((X1 + (X1 * X1)) * X2))))).
step(add(rule(357, (X1 + (X1 * ((X3 * X1) + X2))) = (X1 * (X2 + ((X3 + X1) * X1)))))).
step(add(rule(358, (((X1 * -X1) + X2) * -X1) = (X1 + (X2 * -X1))))).
step(add(rule(359, ((X1 + (X2 * -X2)) * X2) = (-X2 + (X1 * X2))))).
step(hard((X1 + ((X2 * (X1 * X1)) + X3)) = (X3 + ((X2 + X1) * (X1 * X1))))).
step(add(rule(360, (X1 + ((X2 + X3) * (X2 * X2))) = (X2 + (X1 + (X3 * (X2 * X2))))))).
step(hard((X1 + ((X2 + X3) * (X3 * X3))) = (X1 + ((X3 + X2) * (X3 * X3))))).
step(add(rule(361, (X2 + (((X3 * X2) + X1) * X2)) = ((X1 + ((X2 + X3) * X2)) * X2)))).
step(add(rule(362, ((X1 + ((X2 + X1) * X2)) * X2) = (X2 + (X1 * (X2 + (X2 * X2))))))).
step(add(rule(363, ((X1 + ((X1 * X1) + X2)) * (X1 * X1)) = ((X1 + ((X1 + X2) * X1)) * X1)))).
step(add(rule(364, ((X2 + (X1 + (X1 * X1))) * (X1 * X1)) = ((X1 + ((X1 + X2) * X1)) * X1)))).
step(add(rule(365, ((X1 + (X1 * X3)) * (X2 + X2)) = ((X1 + X1) * (X2 + (X3 * X2)))))).
step(add(rule(366, (X2 + (((X2 * X3) + X1) * X2)) = ((X1 + (X2 * (X2 + X3))) * X2)))).
step(add(rule(367, ((X1 + (X1 + (X1 + X2))) * (X3 + X3)) = (X2 * (X3 + X3))))).
step(add(rule(368, ((X1 + ((X2 * X2) + X3)) * (X2 * X2)) = ((X2 + ((X1 + X3) * X2)) * X2)))).
step(add(rule(369, (X1 * ((X2 * (X3 + X3)) + X4)) = (X1 * (((X2 + X2) * X3) + X4))))).
step(hard((X1 + X2) = (X3 + (X4 + (X1 + (X2 + -(X4 + X3))))))).
step(add(rule(370, ((X3 + ((X1 * X1) + X2)) * X1) = (X1 + ((X2 + X3) * X1))))).
step(add(rule(371, (((X1 * (X1 + X1)) + X2) * X1) = (X1 + (X1 + (X2 * X1)))))).
step(add(rule(372, (X1 * (X2 + (X3 + (X3 * (X1 * -X1))))) = (X1 * X2)))).
step(add(rule(373, ((X1 + X1) * ((X2 + X2) * -X3)) = (X1 * ((X2 + X2) * X3))))).
step(add(rule(374, ((X1 + X1) * (-(X2 + X2) + X3)) = ((X1 + X1) * (X2 + X3))))).
step(add(rule(375, ((X1 + X1) * (X2 + -(X3 + X3))) = ((X1 + X1) * (X2 + X3))))).
step(add(rule(376, ((X1 + X1) * (X2 * -(X3 + X3))) = (X1 * (X2 * (X3 + X3)))))).
step(add(rule(377, ((X1 + (X1 * (X2 * (X2 + X2)))) * ((X2 + X2) * X3)) = 0))).
step(add(rule(378, ((X1 + (X1 + X1)) * (X2 + (X3 + (X2 + X3)))) = 0))).
step(add(rule(379, ((X1 + (X1 + X1)) * (X2 + (X2 + (X3 + X3)))) = 0))).
step(add(rule(380, (X1 * (-X2 + (X1 * ((X1 + X1) * X2)))) = (X1 * X2)))).
step(add(rule(381, ((X1 + (X1 + X1)) * -X2) = ((X1 + (X1 + X1)) * X2)))).
step(add(rule(382, ((-X1 + (X1 * (X2 * (X2 + X2)))) * X2) = (X1 * X2)))).
step(add(rule(383, (X1 * ((X1 * (X1 + X1)) + X2)) = (X1 + (X1 + (X1 * X2)))))).
step(hard((((X1 * X1) + (X2 + X1)) * X1) = (X1 + ((X2 + X1) * X1)))).
step(hard(((X1 + (-X1 + (X3 + X1))) * X2) = ((X3 + X1) * X2))).
step(add(rule(384, (X2 + (-(X2 + (X3 * X2)) + ((X1 + (X3 + (X1 * X3))) * X2))) = (X1 * (X2 + (X3 * X2)))))).
step(add(rule(385, (X2 + (X2 + (X2 + (X2 + (X2 + (X2 + ((X1 + (X1 + X1)) * X2))))))) = (X1 * (X2 + (X2 + X2)))))).
step(add(rule(386, ((X2 * -X3) + ((X2 + (X2 + (X1 * X2))) * X3)) = ((X2 + (X1 * X2)) * X3)))).
step(add(rule(387, (((X1 + X1) * X2) + X3) = (? + (? + (X3 + (-(? + ?) + (X1 * (X2 + X2))))))))).
step(add(rule(388, (X4 + (X5 + (X3 + (-(X4 + X5) + (X1 * (X2 + X2)))))) = (? + (? + (X3 + (-(? + ?) + (X1 * (X2 + X2))))))))).
step(add(rule(389, (((X1 + X1) * X2) + X3) = ((X1 * (X2 + X2)) + X3)))).
step(add(rule(390, ((X1 * (X2 + X2)) + X3) = (? + (? + (X3 + (-(? + ?) + ((X1 + X1) * X2)))))))).
step(add(rule(391, (X4 + (X5 + (X3 + (-(X4 + X5) + ((X1 + X1) * X2))))) = (? + (? + (X3 + (-(? + ?) + ((X1 + X1) * X2)))))))).
step(add(rule(392, (X1 * (X2 * (X3 + (X3 * (X1 * -X1))))) = 0))).
step(add(rule(393, (X1 * (X2 * (X3 + (X1 * (X1 * -X3))))) = 0))).
step(add(rule(394, ((X1 + (X1 + X1)) * (X2 * -(X3 + X3))) = 0))).
step(add(rule(395, ((X1 + (X1 * (X2 * (X2 + X2)))) * -(X2 + X2)) = 0))).
step(add(rule(396, ((X3 * -X2) + ((X3 + X1) * X2)) = (X1 * X2)))).
step(add(rule(397, ((X1 + X1) * ((X1 + X1) * X2)) = (X1 * ((X1 + X1) * -X2))))).
step(add(rule(398, ((X1 + X1) * (X2 + (X2 * (X1 * -X1)))) = 0))).
step(add(rule(399, (X1 * (X2 * (X3 + (X1 * (X2 * (X1 * X2)))))) = (X1 * (X2 + (X2 * X3)))))).
step(add(rule(400, (X1 + (X2 + (X3 * ((X1 + X2) * (X1 + X2))))) = ((X1 + (X2 + X3)) * ((X1 + X2) * (X1 + X2)))))).
step(add(rule(401, ((X1 + (X2 + (X1 + X2))) * ((X1 + X2) * (X1 + X2))) = (X1 + (X2 + (X1 + X2)))))).
step(add(rule(402, ((X1 * X2) + (X3 * (X1 * (X2 * (X1 * X2))))) = (((X1 * X2) + X3) * (X1 * (X2 * (X1 * X2))))))).
step(add(rule(403, (X1 * ((X1 + (X2 * X1)) * (X2 * (X1 * X2)))) = (X1 * (X2 + (X1 * (X2 * (X1 * X2)))))))).
step(add(rule(404, ((X1 + (X1 * (X2 * -X2))) * (X3 * X2)) = 0))).
step(add(rule(405, (X1 * (X3 * (X3 * (X2 * X3)))) = (X1 * (X2 * X3))))).
step(add(rule(406, ((X3 * X4) + (X1 * (X2 * (X3 * (X3 * X4))))) = (((X1 * X2) + X3) * (X3 * (X3 * X4)))))).
step(add(rule(407, ((X2 + -X1) * (X3 + X3)) = ((X2 + (-(X1 + X1) + X2)) * X3)))).
step(add(rule(408, ((X1 + X1) * (X3 + -X2)) = (X1 * (X3 + (-(X2 + X2) + X3)))))).
step(add(rule(409, ((X1 + (((X2 * -X2) + X1) * (X2 * -X2))) * (X2 * -X2)) = (X2 * -X2)))).
step(add(rule(410, (X1 * (X2 + (X1 * ((X1 + X1) * -X2)))) = (X1 * -X2)))).
step(add(rule(411, ((X1 + (X1 + X2)) * -(X3 + X3)) = ((X1 + -X2) * (X3 + X3))))).
step(add(rule(412, ((X1 + X1) * ((X2 + X2) * X3)) = (X1 * ((X2 + X2) * -X3))))).
step(add(rule(413, ((X1 + X1) * (X2 + (X2 + X3))) = ((X1 + X1) * (X3 + -X2))))).
step(add(rule(414, ((X1 + X1) * (X2 + (X1 * ((X1 + X1) * X3)))) = ((X1 + X1) * (X2 + -X3))))).
step(add(rule(415, ((X2 + (X2 * (X3 * -X3))) * X3) = 0))).
step(add(rule(416, ((X2 + (X2 + X1)) * (X3 + X3)) = ((X1 + -X2) * (X3 + X3))))).
step(add(rule(417, ((X1 + X1) * (X2 + (X3 + X3))) = ((X1 + X1) * (X2 + -X3))))).
step(add(rule(418, ((X1 + (X2 * -(X2 + X2))) * X2) = ((X1 * X2) + -(X2 + X2))))).
step(add(rule(419, ((X1 + (X2 * (X2 * -X1))) * -X2) = 0))).
step(add(rule(420, (X1 * (X1 * (X2 * X1))) = (X2 * X1)))).
step(add(rule(421, (X2 * (X2 * (X1 * -X2))) = (X1 * -X2)))).
step(add(rule(422, ((X1 + (X2 * (X2 * -X1))) * X2) = 0))).
step(add(rule(423, ((X1 + X2) * ((X3 + X3) * X4)) = ((X1 + (X2 + (X1 + X2))) * (X3 * X4))))).
step(add(rule(424, ((X1 + (X2 + (X1 + X2))) * (X3 + (X3 + X3))) = 0))).
step(add(rule(425, ((X1 + X2) * ((X3 + X3) * X4)) = ((X1 + (X1 + (X2 + X2))) * (X3 * X4))))).
step(hard(((X1 + X2) * ((X3 + X3) * X4)) = ((X2 + X1) * (X3 * (X4 + X4))))).
step(add(rule(426, ((X1 + -(X2 + X2)) * (X3 + X3)) = ((X1 + X2) * (X3 + X3))))).
step(add(rule(427, (X1 * ((X2 + X2) * (X3 + (X2 * X2)))) = ((X1 + X1) * (X2 + (X2 * X3)))))).
step(add(rule(428, ((X1 + X1) * ((X2 + X3) * X4)) = (X1 * ((X2 + (X3 + (X2 + X3))) * X4))))).
step(add(rule(429, (X1 * (((X2 + X2) * X3) + X4)) = (((X1 + X1) * (X2 * X3)) + (X1 * X4))))).
step(add(rule(430, (X1 + ((X1 + X1) * (X2 * X3))) = (X1 + (X1 * ((X2 + X2) * X3)))))).
step(add(rule(431, (X1 * (X2 + ((X3 + X3) * X4))) = ((X1 * X2) + ((X1 + X1) * (X3 * X4)))))).
step(add(rule(432, (X1 * (X2 + (X1 * -(X1 + X1)))) = ((X1 * X2) + -(X1 + X1))))).
step(add(rule(433, ((X1 + X1) * ((X2 + X3) * X4)) = (X1 * ((X2 + (X2 + (X3 + X3))) * X4))))).
step(hard(((X1 + X1) * ((X2 + X3) * X4)) = (X1 * ((X3 + X2) * (X4 + X4))))).
step(add(rule(434, (X1 * ((X2 + X2) * (X3 + X4))) = (X1 * (X2 * (X3 + (X4 + (X3 + X4)))))))).
step(add(rule(435, (X1 * ((X2 + X2) * (X3 + X4))) = (X1 * (X2 * (X3 + (X3 + (X4 + X4)))))))).
step(hard((X1 * ((X2 + X2) * (X3 + X4))) = (X1 * ((X2 + X2) * (X4 + X3))))).
step(add(rule(436, (X1 * ((X2 + X3) * (X4 + X4))) = (X1 * ((X2 + (X3 + (X2 + X3))) * X4))))).
step(add(rule(437, (X1 * ((X2 + X3) * (X4 + X4))) = (X1 * ((X2 + (X2 + (X3 + X3))) * X4))))).
step(interreduce).
step(delete(rule(194, (X1 + (X1 + (X1 * (X2 + X2)))) = ((X1 + X1) * ((X1 * X1) + X2))))).
step(delete(rule(207, ((X1 + (X2 + (X1 * X1))) * (X1 * X1)) = ((X1 + ((X1 + X2) * X1)) * X1)))).
step(delete(rule(240, ((X1 + X1) * ((X2 + (X1 * X1)) * X3)) = ((X1 + X1) * (X3 + (X2 * X3)))))).
step(delete(rule(241, ((X2 + ((X1 * X1) + X2)) * X1) = (X1 + (X2 * (X1 + X1)))))).
step(delete(rule(245, ((X1 + (X1 * (X2 * -X2))) * (X2 + X2)) = 0))).
step(delete(rule(278, (X1 * (X2 + (X2 + X2))) = ((X1 + (X1 + X1)) * -X2)))).
step(delete(rule(279, ((X1 + X1) * (X2 + (X2 + X2))) = 0))).
step(delete(rule(281, ((X1 + (X1 + X1)) * (X2 + X2)) = 0))).
step(delete(rule(282, ((X1 + (X1 + X1)) * -(X2 + X2)) = 0))).
step(delete(rule(290, ((X1 + (X1 * (X2 * (X2 + X2)))) * (X2 + X2)) = 0))).
step(delete(rule(312, ((X1 + X1) * ((X2 + X2) * X3)) = (X1 * (X2 * -(X3 + X3)))))).
step(delete(rule(334, ((X1 + X1) * (X2 + (X1 * ((X1 + X1) * X2)))) = 0))).
step(delete(rule(352, (X1 * -(X2 + X2)) = (X1 * ((X1 + X1) * ((X1 + X1) * X2)))))).
step(delete(rule(353, (X1 * ((X1 + X1) * ((X1 + X1) * X2))) = ((X1 + X1) * -X2)))).
step(delete(rule(363, ((X1 + ((X1 * X1) + X2)) * (X1 * X1)) = ((X1 + ((X1 + X2) * X1)) * X1)))).
step(delete(rule(367, ((X1 + (X1 + (X1 + X2))) * (X3 + X3)) = (X2 * (X3 + X3))))).
step(delete(rule(373, ((X1 + X1) * ((X2 + X2) * -X3)) = (X1 * ((X2 + X2) * X3))))).
step(delete(rule(374, ((X1 + X1) * (-(X2 + X2) + X3)) = ((X1 + X1) * (X2 + X3))))).
step(delete(rule(378, ((X1 + (X1 + X1)) * (X2 + (X3 + (X2 + X3)))) = 0))).
step(delete(rule(386, ((X2 * -X3) + ((X2 + (X2 + (X1 * X2))) * X3)) = ((X2 + (X1 * X2)) * X3)))).
step(delete(rule(397, ((X1 + X1) * ((X1 + X1) * X2)) = (X1 * ((X1 + X1) * -X2))))).
step(delete(rule(401, ((X1 + (X2 + (X1 + X2))) * ((X1 + X2) * (X1 + X2))) = (X1 + (X2 + (X1 + X2)))))).
step(add(rule(438, ((X1 + X2) * ((X1 + X2) * (X1 + (X1 + (X2 + X2))))) = (X1 + (X2 + (X1 + X2)))))).
step(delete(rule(404, ((X1 + (X1 * (X2 * -X2))) * (X3 * X2)) = 0))).
step(delete(rule(405, (X1 * (X3 * (X3 * (X2 * X3)))) = (X1 * (X2 * X3))))).
step(delete(rule(413, ((X1 + X1) * (X2 + (X2 + X3))) = ((X1 + X1) * (X3 + -X2))))).
step(delete(rule(423, ((X1 + X2) * ((X3 + X3) * X4)) = ((X1 + (X2 + (X1 + X2))) * (X3 * X4))))).
step(delete(rule(428, ((X1 + X1) * ((X2 + X3) * X4)) = (X1 * ((X2 + (X3 + (X2 + X3))) * X4))))).
step(delete(rule(434, (X1 * ((X2 + X2) * (X3 + X4))) = (X1 * (X2 * (X3 + (X4 + (X3 + X4)))))))).
step(delete(rule(436, (X1 * ((X2 + X3) * (X4 + X4))) = (X1 * ((X2 + (X3 + (X2 + X3))) * X4))))).
step(hard((X1 * ((X2 + X3) * (X4 + X4))) = (X1 * ((X3 + X2) * (X4 + X4))))).
step(add(rule(439, ((X1 * X2) + (X3 * -(X2 + X2))) = ((X1 + -(X3 + X3)) * X2)))).
step(add(rule(440, ((X1 + (X2 + X2)) * X3) = ((X1 * X3) + (X2 * (X3 + X3)))))).
step(hard((((X1 + X1) * X2) + (X1 * -(X2 + X2))) = 0)).
step(add(rule(441, ((X1 + X2) * (X3 + (X4 * X3))) = ((X1 + (X2 + ((X1 + X2) * X4))) * X3)))).
step(add(rule(442, ((X1 + ((X1 * X2) + X3)) * X4) = ((X1 * (X4 + (X2 * X4))) + (X3 * X4))))).
step(add(rule(443, ((X1 + (X2 + (X2 * X3))) * X4) = ((X1 * X4) + (X2 * (X4 + (X3 * X4))))))).
step(add(rule(444, ((X1 + X1) * (X2 + (X3 * X2))) = ((X1 + (X1 + (X1 * (X3 + X3)))) * X2)))).
step(add(rule(445, (X1 * (X2 + ((X3 + (X1 * X1)) * X2))) = ((X1 + (X1 + (X1 * X3))) * X2)))).
step(add(rule(446, ((X1 + (X1 * X2)) * (X3 + X4)) = (X1 * (X3 + (X4 + (X2 * (X3 + X4)))))))).
step(add(rule(447, (X1 * (X2 + ((X3 * X2) + X4))) = (((X1 + (X1 * X3)) * X2) + (X1 * X4))))).
step(add(rule(448, (X1 * (-X2 + (X3 * X2))) = ((-X1 + (X1 * X3)) * X2)))).
step(add(rule(449, (X1 + (X1 * (X2 + (X3 * X2)))) = (X1 + ((X1 + (X1 * X3)) * X2))))).
step(add(rule(450, (X1 * ((X2 * X3) + ((X2 * -X3) + X4))) = (X1 * X4)))).
step(add(rule(451, (X1 * (X2 * (X3 * (X1 * X1)))) = (X1 * (X2 * X3))))).
step(add(rule(452, (X1 * (X2 * (X1 * X1))) = (X1 * X2)))).
step(add(rule(453, (X1 * (X2 * (X1 * -X1))) = (X1 * -X2)))).
step(add(rule(454, (X1 * (X2 + (X3 * (X1 * X1)))) = (X1 * (X2 + X3))))).
step(add(rule(455, (X1 * (X2 * (X1 * (X1 + X1)))) = ((X1 + X1) * X2)))).
step(add(rule(456, (X1 * ((X1 + (X2 * X1)) * X1)) = (X1 + (X1 * X2))))).
step(add(rule(457, (X1 * (X2 * (X1 * X2))) = (X1 * (X2 * (X2 * X1)))))).
step(add(rule(458, ((X1 + (X2 * X1)) * X1) = (X1 * (X1 + (X1 * X2)))))).
step(add(rule(459, (X1 * (X2 + (X3 + (X4 * X3)))) = ((X1 * X2) + ((X1 + (X1 * X4)) * X3))))).
step(add(rule(460, (X1 * (X2 + (X3 + X3))) = ((X1 * X2) + ((X1 + X1) * X3))))).
step(add(rule(461, (X1 * ((X1 * X1) + (X2 + X2))) = (X1 + ((X1 + X1) * X2))))).
step(add(rule(462, ((X1 + (X2 + X1)) * (X3 + X3)) = ((X2 + -X1) * (X3 + X3))))).
step(add(rule(463, ((X2 + (X1 + X1)) * (X3 + X3)) = ((X2 + -X1) * (X3 + X3))))).
step(add(rule(464, ((X1 + X1) * (X3 + (X2 * X3))) = (X1 * (X3 + (X3 + ((X2 + X2) * X3))))))).
step(add(rule(465, (X1 * -(X2 + (X1 * (X1 * X3)))) = (X1 * -(X2 + X3))))).
step(add(rule(466, ((X3 * X5) + (X1 + (X2 + (X3 * X4)))) = (X1 + (X2 + (X3 * (X4 + X5))))))).
step(add(rule(467, (X1 + (X2 * (X3 + (X4 + X4)))) = (((X2 + X2) * X4) + (X1 + (X2 * X3)))))).
step(add(rule(468, (X1 + (X2 * (X3 + (X3 + X3)))) = (X1 + ((X2 + (X2 + X2)) * X3))))).
step(add(rule(469, (X1 + (X2 * (X3 + (X3 + X4)))) = ((X2 * X4) + (X1 + ((X2 + X2) * X3)))))).
step(add(rule(470, (X1 + (X2 + (X2 * (X3 + X3)))) = (X2 + (X1 + ((X2 + X2) * X3)))))).
step(hard((X1 * (X2 + (X3 + (X3 + X4)))) = (X1 * (X4 + (X3 + (X3 + X2)))))).
step(add(rule(471, ((X2 * X3) + ((X1 + X2) * (X1 * X1))) = (X1 + (X2 * ((X1 * X1) + X3)))))).
step(add(rule(472, ((X4 * X5) + (X1 + (X2 + (X3 * X5)))) = (X1 + (X2 + ((X3 + X4) * X5)))))).
step(add(rule(473, (X1 + ((X2 + (X3 + X3)) * X4)) = ((X3 * (X4 + X4)) + (X1 + (X2 * X4)))))).
step(add(rule(474, ((X1 + X1) * (X2 + (X3 + X2))) = ((X1 + X1) * (X3 + -X2))))).
step(add(rule(475, (X1 + ((X2 + (X2 + X3)) * X4)) = ((X3 * X4) + (X1 + (X2 * (X4 + X4))))))).
step(hard(((X1 + (X3 + (X3 + X4))) * X2) = ((X4 + (X3 + (X3 + X1))) * X2))).
step(add(rule(476, ((X1 + (X1 + X2)) * (X3 * X4)) = (((X1 * (X3 + X3)) + (X2 * X3)) * X4)))).
step(add(rule(477, (X1 * ((X2 * (X3 + X3)) + (X4 * X3))) = (X1 * ((X2 + (X2 + X4)) * X3))))).
step(add(rule(478, ((X1 * (X2 + X2)) + ((X3 + X4) * X2)) = ((X1 + (X3 + (X1 + X4))) * X2)))).
step(hard(((X1 + (X2 + (X1 + X3))) * X4) = ((X1 + (X1 + (X2 + X3))) * X4))).
step(add(rule(479, ((X1 * (X2 + X2)) + ((X3 * X2) + X4)) = (((X1 + (X1 + X3)) * X2) + X4)))).
step(hard(((X1 + (X1 + (X2 + X4))) * X3) = ((X2 + (X4 + (X1 + X1))) * X3))).
step(add(rule(480, (((X1 * X2) + ((X1 * X2) + X3)) * X4) = ((X1 * (X2 * (X4 + X4))) + (X3 * X4))))).
step(add(rule(481, (((X1 * X2) + ((X1 * X2) + X3)) * X4) = (((X1 * (X2 + X2)) + X3) * X4)))).
step(add(rule(482, ((X1 * (X2 + X2)) + (X3 + (X4 * X2))) = (X3 + ((X1 + (X1 + X4)) * X2))))).
step(hard((X1 + ((X2 + (X2 + X3)) * X4)) = (X1 + ((X3 + (X2 + X2)) * X4)))).
step(hard(((X1 + (X3 + (X3 + X4))) * X2) = ((X3 + (X3 + (X1 + X4))) * X2))).
step(add(rule(483, ((X1 * (X2 + X2)) + ((X3 + X4) * X2)) = ((X4 + (X1 + (X1 + X3))) * X2)))).
step(add(rule(484, ((-? + (X2 + (X2 + ?))) * X3) = (X2 * (X3 + X3))))).
step(add(rule(485, ((-X1 + (X2 + (X2 + X1))) * X3) = ((-? + (X2 + (X2 + ?))) * X3)))).
step(hard(((X1 + (X2 + (X2 + X3))) * X4) = ((X2 + (X2 + (X3 + X1))) * X4))).
step(hard(((X1 + (X2 + (X2 + X3))) * X4) = ((X2 + (X3 + (X2 + X1))) * X4))).
step(add(rule(486, (X1 * (((X2 + X2) * X3) + (X2 * X4))) = (X1 * (X2 * (X3 + (X3 + X4))))))).
step(add(rule(487, (X1 * ((X2 + (X2 + X3)) * X4)) = ((((X1 + X1) * X2) + (X1 * X3)) * X4)))).
step(add(rule(488, ((X1 + (X1 + X1)) * (X2 * X3)) = (X1 * (X2 * (X3 + (X3 + X3))))))).
step(add(rule(489, (((X1 + X1) * X2) + (X1 * (X3 + X4))) = (X1 * (X2 + (X3 + (X2 + X4))))))).
step(hard((X1 * (X2 + (X3 + (X2 + X4)))) = (X1 * (X2 + (X2 + (X3 + X4)))))).
step(add(rule(490, (((X1 + X1) * X2) + ((X1 * X3) + X4)) = ((X1 * (X2 + (X2 + X3))) + X4)))).
step(hard((X1 * (X2 + (X2 + (X3 + X4)))) = (X1 * (X3 + (X4 + (X2 + X2)))))).
step(add(rule(491, ((X1 * (X2 + X2)) + ((X1 * -(X2 + X2)) + X3)) = X3))).
step(add(rule(492, (((X1 + X1) * X2) + (X3 + (X1 * X4))) = (X3 + (X1 * (X2 + (X2 + X4))))))).
step(hard((X1 + (X2 * (X3 + (X3 + X4)))) = (X1 + (X2 * (X4 + (X3 + X3)))))).
step(hard((X1 * (X2 + (X3 + (X3 + X4)))) = (X1 * (X3 + (X3 + (X2 + X4)))))).
step(add(rule(493, (X1 * (X2 + (X2 + ((X3 + X3) * X4)))) = ((X1 + X1) * (X2 + (X3 * X4)))))).
step(add(rule(494, (X1 * (X2 + X2)) = ((X1 + X1) * (X2 + (? + (? + ?))))))).
step(add(rule(495, ((X1 + X1) * (X2 + (X3 + (X3 + X3)))) = ((X1 + X1) * (X2 + (? + (? + ?))))))).
step(add(rule(496, ((X1 + X1) * (X2 + -X3)) = (X1 * (X2 + (X2 + -(X3 + X3))))))).
step(add(rule(497, (X1 * (X1 * (X2 + (X2 + (X1 * X3))))) = (X1 * (((X1 + X1) * X2) + X3))))).
step(add(rule(498, (((X1 + X1) * X2) + (X1 * (X3 + X4))) = (X1 * (X4 + (X2 + (X2 + X3))))))).
step(add(rule(499, (X1 * (-? + (X3 + (X3 + ?)))) = ((X1 + X1) * X3)))).
step(add(rule(500, (X1 * (-X2 + (X3 + (X3 + X2)))) = (X1 * (-? + (X3 + (X3 + ?))))))).
step(hard((X1 * (X2 + (X3 + (X3 + X4)))) = (X1 * (X3 + (X3 + (X4 + X2)))))).
step(hard((X1 * (X2 + (X3 + (X3 + X4)))) = (X1 * (X3 + (X4 + (X3 + X2)))))).
step(add(rule(501, (X1 * (X3 + (X4 + ((X1 * X1) + X2)))) = (X1 + (X1 * (X2 + (X3 + X4))))))).
step(add(rule(502, (X1 * ((X2 + ((X1 * X1) + X3)) * X4)) = ((X1 + (X1 * (X3 + X2))) * X4)))).
step(add(rule(503, (X1 * (X2 + (X3 + (X4 + (X1 * X1))))) = (X1 + (X1 * (X2 + (X3 + X4))))))).
step(add(rule(504, (X1 * ((X2 + (X3 + (X1 * X1))) * X4)) = ((X1 + (X1 * (X2 + X3))) * X4)))).
step(hard(((X1 + (X1 * (X2 + X3))) * X4) = ((X1 + (X1 * (X3 + X2))) * X4))).
step(add(rule(505, ((X1 + (X1 * X2)) * ((X2 + (X1 * X1)) * (X2 + (X1 * X1)))) = (X1 + (X1 * X2))))).
step(interreduce).
step(delete(rule(162, (((? * X2) + ((? * X2) + ((? + X3) * -(X2 + X2)))) * X4) = (X3 * (X2 * -(X4 + X4)))))).
step(delete(rule(163, (((X1 * X2) + ((X1 * X2) + ((X3 + X1) * -(X2 + X2)))) * X4) = (((? * X2) + ((? * X2) + ((? + X3) * -(X2 + X2)))) * X4)))).
step(delete(rule(249, (X1 * (-X2 + (X2 * (X1 * X1)))) = 0))).
step(delete(rule(287, (((X1 + X1) * X2) + (((X1 + X1) * X2) + (((X1 + X1) * X2) + X3))) = X3))).
step(delete(rule(319, (X1 * (X2 + (X2 * (X1 * X1)))) = ((X1 + X1) * X2)))).
step(delete(rule(339, (X1 * -(X2 + (X1 * (X1 * -X2)))) = 0))).
step(delete(rule(364, ((X2 + (X1 + (X1 * X1))) * (X1 * X1)) = ((X1 + ((X1 + X2) * X1)) * X1)))).
step(add(rule(506, ((X2 + (X1 + (X1 * X1))) * (X1 * X1)) = (X1 * (X1 + (X1 * (X1 + X2))))))).
step(delete(rule(368, ((X1 + ((X2 * X2) + X3)) * (X2 * X2)) = ((X2 + ((X1 + X3) * X2)) * X2)))).
step(add(rule(507, ((X1 + ((X2 * X2) + X3)) * (X2 * X2)) = (X2 * (X2 + (X2 * (X1 + X3))))))).
step(delete(rule(408, ((X1 + X1) * (X3 + -X2)) = (X1 * (X3 + (-(X2 + X2) + X3)))))).
step(delete(rule(416, ((X2 + (X2 + X1)) * (X3 + X3)) = ((X1 + -X2) * (X3 + X3))))).
step(delete(rule(456, (X1 * ((X1 + (X2 * X1)) * X1)) = (X1 + (X1 * X2))))).
step(delete(rule(464, ((X1 + X1) * (X3 + (X2 * X3))) = (X1 * (X3 + (X3 + ((X2 + X2) * X3))))))).
step(delete(rule(467, (X1 + (X2 * (X3 + (X4 + X4)))) = (((X2 + X2) * X4) + (X1 + (X2 * X3)))))).
step(delete(rule(473, (X1 + ((X2 + (X3 + X3)) * X4)) = ((X3 * (X4 + X4)) + (X1 + (X2 * X4)))))).
step(delete(rule(480, (((X1 * X2) + ((X1 * X2) + X3)) * X4) = ((X1 * (X2 * (X4 + X4))) + (X3 * X4))))).
step(delete(rule(484, ((-? + (X2 + (X2 + ?))) * X3) = (X2 * (X3 + X3))))).
step(add(rule(508, ((? + (-? + (X2 + X2))) * X3) = (X2 * (X3 + X3))))).
step(delete(rule(485, ((-X1 + (X2 + (X2 + X1))) * X3) = ((-? + (X2 + (X2 + ?))) * X3)))).
step(add(rule(509, ((-X1 + (X2 + (X2 + X1))) * X3) = ((? + (-? + (X2 + X2))) * X3)))).
step(delete(rule(494, (X1 * (X2 + X2)) = ((X1 + X1) * (X2 + (? + (? + ?))))))).
step(add(rule(510, (X1 * (X2 + X2)) = ((X1 + X1) * (? + (? + (? + X2))))))).
step(delete(rule(495, ((X1 + X1) * (X2 + (X3 + (X3 + X3)))) = ((X1 + X1) * (X2 + (? + (? + ?))))))).
step(add(rule(511, ((X1 + X1) * (X2 + (X3 + (X3 + X3)))) = ((X1 + X1) * (? + (? + (? + X2))))))).
step(delete(rule(499, (X1 * (-? + (X3 + (X3 + ?)))) = ((X1 + X1) * X3)))).
step(add(rule(512, (X1 * (? + (-? + (X3 + X3)))) = ((X1 + X1) * X3)))).
step(delete(rule(500, (X1 * (-X2 + (X3 + (X3 + X2)))) = (X1 * (-? + (X3 + (X3 + ?))))))).
step(add(rule(513, (X1 * (-X2 + (X3 + (X3 + X2)))) = (X1 * (? + (-? + (X3 + X3))))))).
step(delete(rule(501, (X1 * (X3 + (X4 + ((X1 * X1) + X2)))) = (X1 + (X1 * (X2 + (X3 + X4))))))).
step(add(rule(514, ((X1 + (X3 * -X1)) * X1) = (X1 * (X1 + (X1 * -X3)))))).
step(add(rule(515, (X1 * (X1 * -X2)) = (X2 * (X1 * -X1))))).
step(add(rule(516, (X1 * (X2 * X2)) = (X2 * (X2 * X1))))).
step(add(rule(517, (X1 * (X1 * X2)) = (X1 * (X2 * X1))))).
step(add(rule(518, (X1 * X2) = (X2 * X1)))).

lemma((X1 + 0) = X1).
lemma((X1 + (-X1 + X2)) = X2).
lemma(-(-X1) = X1).
lemma((X1 + (X2 + X3)) = (X2 + (X1 + X3))).
lemma((X2 + (X1 + -X2)) = X1).
lemma((X1 * (X1 * (X1 * X2))) = (X1 * X2)).
lemma((X1 + (X2 + -(X1 + X2))) = 0).
lemma((X1 * ((X1 * X1) + X2)) = (X1 + (X1 * X2))).
lemma((X1 * 0) = 0).
lemma((X1 * (X2 + (X1 * X1))) = (X1 + (X1 * X2))).
lemma((X2 + -(X1 + X2)) = -X1).
lemma((X1 + (X2 * (X1 * X1))) = ((X1 + X2) * (X1 * X1))).
lemma((X2 + -(X2 + X1)) = -X1).
lemma(-(X1 + -X2) = (X2 + -X1)).
lemma((X1 + (X1 * (X2 * X1))) = (X1 * ((X1 + X2) * X1))).
lemma((0 * X1) = 0).
lemma(((X1 * (X2 * X4)) + (X3 * X4)) = (((X1 * X2) + X3) * X4)).
lemma((X1 * (X3 + (X2 * X3))) = ((X1 + (X1 * X2)) * X3)).
lemma(((X1 + (X1 * X2)) * X3) = (X1 * (X3 + (X2 * X3)))).
lemma(((X1 * X4) + (X2 * (X3 * X4))) = ((X1 + (X2 * X3)) * X4)).
lemma(-(X1 * X2) = (X1 * -X2)).
lemma((-X1 * X2) = (X1 * -X2)).
lemma((X1 * ((X2 + (X1 * X1)) * X3)) = ((X1 + (X1 * X2)) * X3)).
lemma(((X1 + (X2 * X3)) * (X3 * X3)) = (((X1 * X3) + X2) * X3)).
lemma((((X3 * X2) + X1) * (X2 * X2)) = (((X1 * X2) + X3) * X2)).
lemma(((X1 + -X2) * -X3) = ((X2 + -X1) * X3)).
lemma(((X1 + (X1 * X2)) * (X3 * X4)) = (X1 * ((X3 + (X2 * X3)) * X4))).
lemma(((X1 * X2) + (X3 * (X2 + X4))) = ((X3 * X4) + ((X1 + X3) * X2))).
lemma(((X1 + (X1 * (X2 * -X2))) * (X2 * X3)) = 0).
lemma((X1 * ((X2 + (X1 * (X1 * X3))) * X4)) = (X1 * ((X2 + X3) * X4))).
lemma(((X1 + (X2 * (X3 * X3))) * (X3 * X4)) = ((X1 + X2) * (X3 * X4))).
lemma((X1 * (X1 * (X2 * X1))) = (X2 * X1)).
lemma((X1 * (X2 * (X3 * (X1 * X1)))) = (X1 * (X2 * X3))).