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

lemma((X1 + 0) = X1).
lemma((X1 + (-X1 + X2)) = X2).
lemma(-(-X1) = X1).
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 * -(-X1 * -X1)) = X1).
lemma((X1 + (X1 * (X1 * X2))) = (X1 * (X1 * (X1 + X2)))).
lemma((0 * X1) = 0).
lemma(((X1 * (X2 * X4)) + (X3 * X4)) = (((X1 * X2) + X3) * X4)).
lemma(((X1 * X4) + (X2 * (X3 * X4))) = ((X1 + (X2 * X3)) * X4)).
lemma((X1 * (X2 * (X1 * (X2 * (X1 * X2))))) = (X1 * X2)).
lemma(-(X1 * X2) = (X1 * -X2)).
lemma((-X1 * X2) = (X1 * -X2)).
lemma(((X1 + (X1 * (X2 * -X2))) * (X2 * X3)) = 0).
lemma(((X1 + (((X1 * -X2) + X3) * X2)) * X2) = (X3 * (X2 * X2))).
lemma((X1 * (X1 * (X2 * X1))) = (X2 * X1)).
lemma((X1 * (X2 * (X1 * X1))) = (X1 * X2)).
lemma((X1 * (X2 * (X3 * X3))) = (X3 * (X3 * (X1 * X2)))).