;; ----- Otter 3.0.4, August 1995 -----
;; The job was started by mccune on gyro, Thu Oct 12 22:29:00 1995
;;
;;;;  -> x=x.
;;;; x*y=u, x*z=u -> y=z.
;;;; y*x=u, z*x=u -> y=z.
;;;;  -> (x*y)*z=x*y*z.
;;;;  -> x*y*z*y*x=y*x*z*x*y.
;;;;  -> b*b0=a*a0.
;;;;  -> d*b0=c*a0.
;;;;  -> b*d0=a*c0.
;;;; d*d0=c*c0 -> .
;;
;; ----> UNIT CONFLICT at 25288.37 sec ----> 18265 [binary,18263.1,1.1]  -> .
;;
(
(1 (input) ((not (= (* (d) (d0)) (* (c) (c0))))))
(2 (input) ((= v0 v0)))
(3 (input) ((not (= (* v0 v1) v2)) (not (= (* v0 v3) v2)) (= v1 v3)))
(4 (input) ((= (* (* v0 v1) v2) (* v0 (* v1 v2)))))
(5 (input) ((= (* v0 (* v1 (* v2 (* v1 v0)))) (* v1 (* v0 (* v2 (* v0 v1)))))))
(6 (input) ((= (* (b) (b0)) (* (a) (a0)))))
(7 (input) ((= (* (d) (b0)) (* (c) (a0)))))
(8 (input) ((= (* (b) (d0)) (* (a) (c0)))))
(9 (instantiate 4 ((v0 . (b))(v1 . (b0))(v2 . v66))) ((= (* (* (b) (b0)) v66) (* (b) (* (b0) v66)))))
(10 (paramod 6 (1 1) 9 (1 1 1)) ((= (* (* (a) (a0)) v66) (* (b) (* (b0) v66)))))
(11 (instantiate 4 ((v0 . (a))(v1 . (a0))(v2 . v66))) ((= (* (* (a) (a0)) v66) (* (a) (* (a0) v66)))))
(12 (paramod 11 (1 1) 10 (1 1)) ((= (* (a) (* (a0) v66)) (* (b) (* (b0) v66)))))
(13 (flip 12 (1)) ((= (* (b) (* (b0) v66)) (* (a) (* (a0) v66)))))
(14 (instantiate 13 ((v66 . v0))) ((= (* (b) (* (b0) v0)) (* (a) (* (a0) v0)))))
(15 (instantiate 4 ((v0 . (d))(v1 . (b0))(v2 . v66))) ((= (* (* (d) (b0)) v66) (* (d) (* (b0) v66)))))
(16 (paramod 7 (1 1) 15 (1 1 1)) ((= (* (* (c) (a0)) v66) (* (d) (* (b0) v66)))))
(17 (instantiate 4 ((v0 . (c))(v1 . (a0))(v2 . v66))) ((= (* (* (c) (a0)) v66) (* (c) (* (a0) v66)))))
(18 (paramod 17 (1 1) 16 (1 1)) ((= (* (c) (* (a0) v66)) (* (d) (* (b0) v66)))))
(19 (flip 18 (1)) ((= (* (d) (* (b0) v66)) (* (c) (* (a0) v66)))))
(20 (instantiate 19 ((v66 . v0))) ((= (* (d) (* (b0) v0)) (* (c) (* (a0) v0)))))
(21 (instantiate 5 ((v0 . (b0))(v1 . (d))(v2 . v66))) ((= (* (b0) (* (d) (* v66 (* (d) (b0))))) (* (d) (* (b0) (* v66 (* (b0) (d))))))))
(22 (paramod 7 (1 1) 21 (1 1 2 2 2)) ((= (* (b0) (* (d) (* v66 (* (c) (a0))))) (* (d) (* (b0) (* v66 (* (b0) (d))))))))
(23 (instantiate 20 ((v0 . (* v66 (* (b0) (d)))))) ((= (* (d) (* (b0) (* v66 (* (b0) (d))))) (* (c) (* (a0) (* v66 (* (b0) (d))))))))
(24 (paramod 23 (1 1) 22 (1 2)) ((= (* (b0) (* (d) (* v66 (* (c) (a0))))) (* (c) (* (a0) (* v66 (* (b0) (d))))))))
(25 (instantiate 24 ((v66 . v0))) ((= (* (b0) (* (d) (* v0 (* (c) (a0))))) (* (c) (* (a0) (* v0 (* (b0) (d))))))))
(26 (instantiate 5 ((v0 . (b0))(v1 . (b))(v2 . v66))) ((= (* (b0) (* (b) (* v66 (* (b) (b0))))) (* (b) (* (b0) (* v66 (* (b0) (b))))))))
(27 (paramod 6 (1 1) 26 (1 1 2 2 2)) ((= (* (b0) (* (b) (* v66 (* (a) (a0))))) (* (b) (* (b0) (* v66 (* (b0) (b))))))))
(28 (instantiate 14 ((v0 . (* v66 (* (b0) (b)))))) ((= (* (b) (* (b0) (* v66 (* (b0) (b))))) (* (a) (* (a0) (* v66 (* (b0) (b))))))))
(29 (paramod 28 (1 1) 27 (1 2)) ((= (* (b0) (* (b) (* v66 (* (a) (a0))))) (* (a) (* (a0) (* v66 (* (b0) (b))))))))
(30 (instantiate 29 ((v66 . v0))) ((= (* (b0) (* (b) (* v0 (* (a) (a0))))) (* (a) (* (a0) (* v0 (* (b0) (b))))))))
(31 (instantiate 4 ((v2 . (* v65 v64)))) ((= (* (* v0 v1) (* v65 v64)) (* v0 (* v1 (* v65 v64))))))
(32 (instantiate 5 ((v0 . v64)(v1 . v65)(v2 . (* v0 v1)))) ((= (* v64 (* v65 (* (* v0 v1) (* v65 v64)))) (* v65 (* v64 (* (* v0 v1) (* v64 v65)))))))
(33 (paramod 31 (1 1) 32 (1 1 2 2)) ((= (* v64 (* v65 (* v0 (* v1 (* v65 v64))))) (* v65 (* v64 (* (* v0 v1) (* v64 v65)))))))
(34 (instantiate 4 ((v0 . v0)(v1 . v1)(v2 . (* v64 v65)))) ((= (* (* v0 v1) (* v64 v65)) (* v0 (* v1 (* v64 v65))))))
(35 (paramod 34 (1 1) 33 (1 2 2 2)) ((= (* v64 (* v65 (* v0 (* v1 (* v65 v64))))) (* v65 (* v64 (* v0 (* v1 (* v64 v65))))))))
(36 (instantiate 35 ((v0 . v2)(v1 . v3)(v64 . v0)(v65 . v1))) ((= (* v0 (* v1 (* v2 (* v3 (* v1 v0))))) (* v1 (* v0 (* v2 (* v3 (* v0 v1))))))))
(37 (instantiate 5 ((v0 . v64))) ((= (* v64 (* v1 (* v2 (* v1 v64)))) (* v1 (* v64 (* v2 (* v64 v1)))))))
(38 (instantiate 4 ((v0 . v64)(v1 . (* v1 (* v2 (* v1 v64))))(v2 . v66))) ((= (* (* v64 (* v1 (* v2 (* v1 v64)))) v66) (* v64 (* (* v1 (* v2 (* v1 v64))) v66)))))
(39 (paramod 37 (1 1) 38 (1 1 1)) ((= (* (* v1 (* v64 (* v2 (* v64 v1)))) v66) (* v64 (* (* v1 (* v2 (* v1 v64))) v66)))))
(40 (instantiate 4 ((v0 . v1)(v1 . (* v64 (* v2 (* v64 v1))))(v2 . v66))) ((= (* (* v1 (* v64 (* v2 (* v64 v1)))) v66) (* v1 (* (* v64 (* v2 (* v64 v1))) v66)))))
(41 (paramod 40 (1 1) 39 (1 1)) ((= (* v1 (* (* v64 (* v2 (* v64 v1))) v66)) (* v64 (* (* v1 (* v2 (* v1 v64))) v66)))))
(42 (instantiate 4 ((v0 . v64)(v1 . (* v2 (* v64 v1)))(v2 . v66))) ((= (* (* v64 (* v2 (* v64 v1))) v66) (* v64 (* (* v2 (* v64 v1)) v66)))))
(43 (paramod 42 (1 1) 41 (1 1 2)) ((= (* v1 (* v64 (* (* v2 (* v64 v1)) v66))) (* v64 (* (* v1 (* v2 (* v1 v64))) v66)))))
(44 (instantiate 4 ((v0 . v2)(v1 . (* v64 v1))(v2 . v66))) ((= (* (* v2 (* v64 v1)) v66) (* v2 (* (* v64 v1) v66)))))
(45 (paramod 44 (1 1) 43 (1 1 2 2)) ((= (* v1 (* v64 (* v2 (* (* v64 v1) v66)))) (* v64 (* (* v1 (* v2 (* v1 v64))) v66)))))
(46 (instantiate 4 ((v0 . v64)(v1 . v1)(v2 . v66))) ((= (* (* v64 v1) v66) (* v64 (* v1 v66)))))
(47 (paramod 46 (1 1) 45 (1 1 2 2 2)) ((= (* v1 (* v64 (* v2 (* v64 (* v1 v66))))) (* v64 (* (* v1 (* v2 (* v1 v64))) v66)))))
(48 (instantiate 4 ((v0 . v1)(v1 . (* v2 (* v1 v64)))(v2 . v66))) ((= (* (* v1 (* v2 (* v1 v64))) v66) (* v1 (* (* v2 (* v1 v64)) v66)))))
(49 (paramod 48 (1 1) 47 (1 2 2)) ((= (* v1 (* v64 (* v2 (* v64 (* v1 v66))))) (* v64 (* v1 (* (* v2 (* v1 v64)) v66))))))
(50 (instantiate 4 ((v0 . v2)(v1 . (* v1 v64))(v2 . v66))) ((= (* (* v2 (* v1 v64)) v66) (* v2 (* (* v1 v64) v66)))))
(51 (paramod 50 (1 1) 49 (1 2 2 2)) ((= (* v1 (* v64 (* v2 (* v64 (* v1 v66))))) (* v64 (* v1 (* v2 (* (* v1 v64) v66)))))))
(52 (instantiate 4 ((v0 . v1)(v1 . v64)(v2 . v66))) ((= (* (* v1 v64) v66) (* v1 (* v64 v66)))))
(53 (paramod 52 (1 1) 51 (1 2 2 2 2)) ((= (* v1 (* v64 (* v2 (* v64 (* v1 v66))))) (* v64 (* v1 (* v2 (* v1 (* v64 v66))))))))
(54 (instantiate 53 ((v1 . v0)(v64 . v1)(v66 . v3))) ((= (* v0 (* v1 (* v2 (* v1 (* v0 v3))))) (* v1 (* v0 (* v2 (* v0 (* v1 v3))))))))
(55 (instantiate 5 ((v0 . (d0))(v1 . (b))(v2 . v66))) ((= (* (d0) (* (b) (* v66 (* (b) (d0))))) (* (b) (* (d0) (* v66 (* (d0) (b))))))))
(56 (paramod 8 (1 1) 55 (1 1 2 2 2)) ((= (* (d0) (* (b) (* v66 (* (a) (c0))))) (* (b) (* (d0) (* v66 (* (d0) (b))))))))
(57 (instantiate 56 ((v66 . v0))) ((= (* (d0) (* (b) (* v0 (* (a) (c0))))) (* (b) (* (d0) (* v0 (* (d0) (b))))))))
(58 (instantiate 4 ((v0 . (b))(v1 . (d0))(v2 . v66))) ((= (* (* (b) (d0)) v66) (* (b) (* (d0) v66)))))
(59 (paramod 8 (1 1) 58 (1 1 1)) ((= (* (* (a) (c0)) v66) (* (b) (* (d0) v66)))))
(60 (instantiate 4 ((v0 . (a))(v1 . (c0))(v2 . v66))) ((= (* (* (a) (c0)) v66) (* (a) (* (c0) v66)))))
(61 (paramod 60 (1 1) 59 (1 1)) ((= (* (a) (* (c0) v66)) (* (b) (* (d0) v66)))))
(62 (flip 61 (1)) ((= (* (b) (* (d0) v66)) (* (a) (* (c0) v66)))))
(63 (instantiate 62 ((v66 . v0))) ((= (* (b) (* (d0) v0)) (* (a) (* (c0) v0)))))
(64 (instantiate 63 ((v0 . (* v0 (* (d0) (b)))))) ((= (* (b) (* (d0) (* v0 (* (d0) (b))))) (* (a) (* (c0) (* v0 (* (d0) (b))))))))
(65 (paramod 64 (1 1) 57 (1 2)) ((= (* (d0) (* (b) (* v0 (* (a) (c0))))) (* (a) (* (c0) (* v0 (* (d0) (b))))))))
(66 (flip 65 (1)) ((= (* (a) (* (c0) (* v0 (* (d0) (b))))) (* (d0) (* (b) (* v0 (* (a) (c0))))))))
(67 (instantiate 5 ((v0 . (b0)))) ((= (* (b0) (* v1 (* v2 (* v1 (b0))))) (* v1 (* (b0) (* v2 (* (b0) v1)))))))
(68 (instantiate 14 ((v0 . (* v1 (* v2 (* v1 (b0))))))) ((= (* (b) (* (b0) (* v1 (* v2 (* v1 (b0)))))) (* (a) (* (a0) (* v1 (* v2 (* v1 (b0)))))))))
(69 (paramod 67 (1 1) 68 (1 1 2)) ((= (* (b) (* v1 (* (b0) (* v2 (* (b0) v1))))) (* (a) (* (a0) (* v1 (* v2 (* v1 (b0)))))))))
(70 (instantiate 69 ((v1 . v0)(v2 . v1))) ((= (* (b) (* v0 (* (b0) (* v1 (* (b0) v0))))) (* (a) (* (a0) (* v0 (* v1 (* v0 (b0)))))))))
(71 (instantiate 63 ((v0 . v64))) ((= (* (b) (* (d0) v64)) (* (a) (* (c0) v64)))))
(72 (instantiate 5 ((v0 . v64)(v1 . (d0))(v2 . (b)))) ((= (* v64 (* (d0) (* (b) (* (d0) v64)))) (* (d0) (* v64 (* (b) (* v64 (d0))))))))
(73 (paramod 71 (1 1) 72 (1 1 2 2)) ((= (* v64 (* (d0) (* (a) (* (c0) v64)))) (* (d0) (* v64 (* (b) (* v64 (d0))))))))
(74 (instantiate 73 ((v64 . v0))) ((= (* v0 (* (d0) (* (a) (* (c0) v0)))) (* (d0) (* v0 (* (b) (* v0 (d0))))))))
(75 (instantiate 4 ((v0 . (b0))(v1 . (* (d) (* v0 (* (c) (a0)))))(v2 . v66))) ((= (* (* (b0) (* (d) (* v0 (* (c) (a0))))) v66) (* (b0) (* (* (d) (* v0 (* (c) (a0)))) v66)))))
(76 (paramod 25 (1 1) 75 (1 1 1)) ((= (* (* (c) (* (a0) (* v0 (* (b0) (d))))) v66) (* (b0) (* (* (d) (* v0 (* (c) (a0)))) v66)))))
(77 (instantiate 4 ((v0 . (c))(v1 . (* (a0) (* v0 (* (b0) (d)))))(v2 . v66))) ((= (* (* (c) (* (a0) (* v0 (* (b0) (d))))) v66) (* (c) (* (* (a0) (* v0 (* (b0) (d)))) v66)))))
(78 (paramod 77 (1 1) 76 (1 1)) ((= (* (c) (* (* (a0) (* v0 (* (b0) (d)))) v66)) (* (b0) (* (* (d) (* v0 (* (c) (a0)))) v66)))))
(79 (instantiate 4 ((v0 . (a0))(v1 . (* v0 (* (b0) (d))))(v2 . v66))) ((= (* (* (a0) (* v0 (* (b0) (d)))) v66) (* (a0) (* (* v0 (* (b0) (d))) v66)))))
(80 (paramod 79 (1 1) 78 (1 1 2)) ((= (* (c) (* (a0) (* (* v0 (* (b0) (d))) v66))) (* (b0) (* (* (d) (* v0 (* (c) (a0)))) v66)))))
(81 (instantiate 4 ((v0 . v0)(v1 . (* (b0) (d)))(v2 . v66))) ((= (* (* v0 (* (b0) (d))) v66) (* v0 (* (* (b0) (d)) v66)))))
(82 (paramod 81 (1 1) 80 (1 1 2 2)) ((= (* (c) (* (a0) (* v0 (* (* (b0) (d)) v66)))) (* (b0) (* (* (d) (* v0 (* (c) (a0)))) v66)))))
(83 (instantiate 4 ((v0 . (b0))(v1 . (d))(v2 . v66))) ((= (* (* (b0) (d)) v66) (* (b0) (* (d) v66)))))
(84 (paramod 83 (1 1) 82 (1 1 2 2 2)) ((= (* (c) (* (a0) (* v0 (* (b0) (* (d) v66))))) (* (b0) (* (* (d) (* v0 (* (c) (a0)))) v66)))))
(85 (instantiate 4 ((v0 . (d))(v1 . (* v0 (* (c) (a0))))(v2 . v66))) ((= (* (* (d) (* v0 (* (c) (a0)))) v66) (* (d) (* (* v0 (* (c) (a0))) v66)))))
(86 (paramod 85 (1 1) 84 (1 2 2)) ((= (* (c) (* (a0) (* v0 (* (b0) (* (d) v66))))) (* (b0) (* (d) (* (* v0 (* (c) (a0))) v66))))))
(87 (instantiate 4 ((v0 . v0)(v1 . (* (c) (a0)))(v2 . v66))) ((= (* (* v0 (* (c) (a0))) v66) (* v0 (* (* (c) (a0)) v66)))))
(88 (paramod 87 (1 1) 86 (1 2 2 2)) ((= (* (c) (* (a0) (* v0 (* (b0) (* (d) v66))))) (* (b0) (* (d) (* v0 (* (* (c) (a0)) v66)))))))
(89 (instantiate 4 ((v0 . (c))(v1 . (a0))(v2 . v66))) ((= (* (* (c) (a0)) v66) (* (c) (* (a0) v66)))))
(90 (paramod 89 (1 1) 88 (1 2 2 2 2)) ((= (* (c) (* (a0) (* v0 (* (b0) (* (d) v66))))) (* (b0) (* (d) (* v0 (* (c) (* (a0) v66))))))))
(91 (instantiate 90 ((v66 . v1))) ((= (* (c) (* (a0) (* v0 (* (b0) (* (d) v1))))) (* (b0) (* (d) (* v0 (* (c) (* (a0) v1))))))))
(92 (instantiate 4 ((v0 . (b0))(v1 . (* (b) (* v0 (* (a) (a0)))))(v2 . v66))) ((= (* (* (b0) (* (b) (* v0 (* (a) (a0))))) v66) (* (b0) (* (* (b) (* v0 (* (a) (a0)))) v66)))))
(93 (paramod 30 (1 1) 92 (1 1 1)) ((= (* (* (a) (* (a0) (* v0 (* (b0) (b))))) v66) (* (b0) (* (* (b) (* v0 (* (a) (a0)))) v66)))))
(94 (instantiate 4 ((v0 . (a))(v1 . (* (a0) (* v0 (* (b0) (b)))))(v2 . v66))) ((= (* (* (a) (* (a0) (* v0 (* (b0) (b))))) v66) (* (a) (* (* (a0) (* v0 (* (b0) (b)))) v66)))))
(95 (paramod 94 (1 1) 93 (1 1)) ((= (* (a) (* (* (a0) (* v0 (* (b0) (b)))) v66)) (* (b0) (* (* (b) (* v0 (* (a) (a0)))) v66)))))
(96 (instantiate 4 ((v0 . (a0))(v1 . (* v0 (* (b0) (b))))(v2 . v66))) ((= (* (* (a0) (* v0 (* (b0) (b)))) v66) (* (a0) (* (* v0 (* (b0) (b))) v66)))))
(97 (paramod 96 (1 1) 95 (1 1 2)) ((= (* (a) (* (a0) (* (* v0 (* (b0) (b))) v66))) (* (b0) (* (* (b) (* v0 (* (a) (a0)))) v66)))))
(98 (instantiate 4 ((v0 . v0)(v1 . (* (b0) (b)))(v2 . v66))) ((= (* (* v0 (* (b0) (b))) v66) (* v0 (* (* (b0) (b)) v66)))))
(99 (paramod 98 (1 1) 97 (1 1 2 2)) ((= (* (a) (* (a0) (* v0 (* (* (b0) (b)) v66)))) (* (b0) (* (* (b) (* v0 (* (a) (a0)))) v66)))))
(100 (instantiate 4 ((v0 . (b0))(v1 . (b))(v2 . v66))) ((= (* (* (b0) (b)) v66) (* (b0) (* (b) v66)))))
(101 (paramod 100 (1 1) 99 (1 1 2 2 2)) ((= (* (a) (* (a0) (* v0 (* (b0) (* (b) v66))))) (* (b0) (* (* (b) (* v0 (* (a) (a0)))) v66)))))
(102 (instantiate 4 ((v0 . (b))(v1 . (* v0 (* (a) (a0))))(v2 . v66))) ((= (* (* (b) (* v0 (* (a) (a0)))) v66) (* (b) (* (* v0 (* (a) (a0))) v66)))))
(103 (paramod 102 (1 1) 101 (1 2 2)) ((= (* (a) (* (a0) (* v0 (* (b0) (* (b) v66))))) (* (b0) (* (b) (* (* v0 (* (a) (a0))) v66))))))
(104 (instantiate 4 ((v0 . v0)(v1 . (* (a) (a0)))(v2 . v66))) ((= (* (* v0 (* (a) (a0))) v66) (* v0 (* (* (a) (a0)) v66)))))
(105 (paramod 104 (1 1) 103 (1 2 2 2)) ((= (* (a) (* (a0) (* v0 (* (b0) (* (b) v66))))) (* (b0) (* (b) (* v0 (* (* (a) (a0)) v66)))))))
(106 (instantiate 4 ((v0 . (a))(v1 . (a0))(v2 . v66))) ((= (* (* (a) (a0)) v66) (* (a) (* (a0) v66)))))
(107 (paramod 106 (1 1) 105 (1 2 2 2 2)) ((= (* (a) (* (a0) (* v0 (* (b0) (* (b) v66))))) (* (b0) (* (b) (* v0 (* (a) (* (a0) v66))))))))
(108 (instantiate 107 ((v66 . v1))) ((= (* (a) (* (a0) (* v0 (* (b0) (* (b) v1))))) (* (b0) (* (b) (* v0 (* (a) (* (a0) v1))))))))
(109 (instantiate 4 ((v0 . (a))(v1 . (* (c0) (* v0 (* (d0) (b)))))(v2 . v66))) ((= (* (* (a) (* (c0) (* v0 (* (d0) (b))))) v66) (* (a) (* (* (c0) (* v0 (* (d0) (b)))) v66)))))
(110 (paramod 66 (1 1) 109 (1 1 1)) ((= (* (* (d0) (* (b) (* v0 (* (a) (c0))))) v66) (* (a) (* (* (c0) (* v0 (* (d0) (b)))) v66)))))
(111 (instantiate 4 ((v0 . (d0))(v1 . (* (b) (* v0 (* (a) (c0)))))(v2 . v66))) ((= (* (* (d0) (* (b) (* v0 (* (a) (c0))))) v66) (* (d0) (* (* (b) (* v0 (* (a) (c0)))) v66)))))
(112 (paramod 111 (1 1) 110 (1 1)) ((= (* (d0) (* (* (b) (* v0 (* (a) (c0)))) v66)) (* (a) (* (* (c0) (* v0 (* (d0) (b)))) v66)))))
(113 (instantiate 4 ((v0 . (b))(v1 . (* v0 (* (a) (c0))))(v2 . v66))) ((= (* (* (b) (* v0 (* (a) (c0)))) v66) (* (b) (* (* v0 (* (a) (c0))) v66)))))
(114 (paramod 113 (1 1) 112 (1 1 2)) ((= (* (d0) (* (b) (* (* v0 (* (a) (c0))) v66))) (* (a) (* (* (c0) (* v0 (* (d0) (b)))) v66)))))
(115 (instantiate 4 ((v0 . v0)(v1 . (* (a) (c0)))(v2 . v66))) ((= (* (* v0 (* (a) (c0))) v66) (* v0 (* (* (a) (c0)) v66)))))
(116 (paramod 115 (1 1) 114 (1 1 2 2)) ((= (* (d0) (* (b) (* v0 (* (* (a) (c0)) v66)))) (* (a) (* (* (c0) (* v0 (* (d0) (b)))) v66)))))
(117 (instantiate 4 ((v0 . (a))(v1 . (c0))(v2 . v66))) ((= (* (* (a) (c0)) v66) (* (a) (* (c0) v66)))))
(118 (paramod 117 (1 1) 116 (1 1 2 2 2)) ((= (* (d0) (* (b) (* v0 (* (a) (* (c0) v66))))) (* (a) (* (* (c0) (* v0 (* (d0) (b)))) v66)))))
(119 (instantiate 4 ((v0 . (c0))(v1 . (* v0 (* (d0) (b))))(v2 . v66))) ((= (* (* (c0) (* v0 (* (d0) (b)))) v66) (* (c0) (* (* v0 (* (d0) (b))) v66)))))
(120 (paramod 119 (1 1) 118 (1 2 2)) ((= (* (d0) (* (b) (* v0 (* (a) (* (c0) v66))))) (* (a) (* (c0) (* (* v0 (* (d0) (b))) v66))))))
(121 (instantiate 4 ((v0 . v0)(v1 . (* (d0) (b)))(v2 . v66))) ((= (* (* v0 (* (d0) (b))) v66) (* v0 (* (* (d0) (b)) v66)))))
(122 (paramod 121 (1 1) 120 (1 2 2 2)) ((= (* (d0) (* (b) (* v0 (* (a) (* (c0) v66))))) (* (a) (* (c0) (* v0 (* (* (d0) (b)) v66)))))))
(123 (instantiate 4 ((v0 . (d0))(v1 . (b))(v2 . v66))) ((= (* (* (d0) (b)) v66) (* (d0) (* (b) v66)))))
(124 (paramod 123 (1 1) 122 (1 2 2 2 2)) ((= (* (d0) (* (b) (* v0 (* (a) (* (c0) v66))))) (* (a) (* (c0) (* v0 (* (d0) (* (b) v66))))))))
(125 (instantiate 124 ((v66 . v1))) ((= (* (d0) (* (b) (* v0 (* (a) (* (c0) v1))))) (* (a) (* (c0) (* v0 (* (d0) (* (b) v1))))))))
(126 (flip 125 (1)) ((= (* (a) (* (c0) (* v0 (* (d0) (* (b) v1))))) (* (d0) (* (b) (* v0 (* (a) (* (c0) v1))))))))
(127 (instantiate 14 ((v0 . v64))) ((= (* (b) (* (b0) v64)) (* (a) (* (a0) v64)))))
(128 (instantiate 36 ((v0 . v64)(v1 . (b0))(v2 . v66)(v3 . (b)))) ((= (* v64 (* (b0) (* v66 (* (b) (* (b0) v64))))) (* (b0) (* v64 (* v66 (* (b) (* v64 (b0)))))))))
(129 (paramod 127 (1 1) 128 (1 1 2 2 2)) ((= (* v64 (* (b0) (* v66 (* (a) (* (a0) v64))))) (* (b0) (* v64 (* v66 (* (b) (* v64 (b0)))))))))
(130 (instantiate 129 ((v64 . v0)(v66 . v1))) ((= (* v0 (* (b0) (* v1 (* (a) (* (a0) v0))))) (* (b0) (* v0 (* v1 (* (b) (* v0 (b0)))))))))
(131 (instantiate 4 ((v2 . (* v65 v64)))) ((= (* (* v0 v1) (* v65 v64)) (* v0 (* v1 (* v65 v64))))))
(132 (instantiate 36 ((v0 . v64)(v1 . v65)(v2 . v66)(v3 . (* v0 v1)))) ((= (* v64 (* v65 (* v66 (* (* v0 v1) (* v65 v64))))) (* v65 (* v64 (* v66 (* (* v0 v1) (* v64 v65))))))))
(133 (paramod 131 (1 1) 132 (1 1 2 2 2)) ((= (* v64 (* v65 (* v66 (* v0 (* v1 (* v65 v64)))))) (* v65 (* v64 (* v66 (* (* v0 v1) (* v64 v65))))))))
(134 (instantiate 4 ((v0 . v0)(v1 . v1)(v2 . (* v64 v65)))) ((= (* (* v0 v1) (* v64 v65)) (* v0 (* v1 (* v64 v65))))))
(135 (paramod 134 (1 1) 133 (1 2 2 2 2)) ((= (* v64 (* v65 (* v66 (* v0 (* v1 (* v65 v64)))))) (* v65 (* v64 (* v66 (* v0 (* v1 (* v64 v65)))))))))
(136 (instantiate 135 ((v0 . v3)(v1 . v4)(v64 . v0)(v65 . v1)(v66 . v2))) ((= (* v0 (* v1 (* v2 (* v3 (* v4 (* v1 v0)))))) (* v1 (* v0 (* v2 (* v3 (* v4 (* v0 v1)))))))))
(137 (instantiate 74 ((v0 . v64))) ((= (* v64 (* (d0) (* (a) (* (c0) v64)))) (* (d0) (* v64 (* (b) (* v64 (d0))))))))
(138 (instantiate 4 ((v0 . v64)(v1 . (* (d0) (* (a) (* (c0) v64))))(v2 . v66))) ((= (* (* v64 (* (d0) (* (a) (* (c0) v64)))) v66) (* v64 (* (* (d0) (* (a) (* (c0) v64))) v66)))))
(139 (paramod 137 (1 1) 138 (1 1 1)) ((= (* (* (d0) (* v64 (* (b) (* v64 (d0))))) v66) (* v64 (* (* (d0) (* (a) (* (c0) v64))) v66)))))
(140 (instantiate 4 ((v0 . (d0))(v1 . (* v64 (* (b) (* v64 (d0)))))(v2 . v66))) ((= (* (* (d0) (* v64 (* (b) (* v64 (d0))))) v66) (* (d0) (* (* v64 (* (b) (* v64 (d0)))) v66)))))
(141 (paramod 140 (1 1) 139 (1 1)) ((= (* (d0) (* (* v64 (* (b) (* v64 (d0)))) v66)) (* v64 (* (* (d0) (* (a) (* (c0) v64))) v66)))))
(142 (instantiate 4 ((v0 . v64)(v1 . (* (b) (* v64 (d0))))(v2 . v66))) ((= (* (* v64 (* (b) (* v64 (d0)))) v66) (* v64 (* (* (b) (* v64 (d0))) v66)))))
(143 (paramod 142 (1 1) 141 (1 1 2)) ((= (* (d0) (* v64 (* (* (b) (* v64 (d0))) v66))) (* v64 (* (* (d0) (* (a) (* (c0) v64))) v66)))))
(144 (instantiate 4 ((v0 . (b))(v1 . (* v64 (d0)))(v2 . v66))) ((= (* (* (b) (* v64 (d0))) v66) (* (b) (* (* v64 (d0)) v66)))))
(145 (paramod 144 (1 1) 143 (1 1 2 2)) ((= (* (d0) (* v64 (* (b) (* (* v64 (d0)) v66)))) (* v64 (* (* (d0) (* (a) (* (c0) v64))) v66)))))
(146 (instantiate 4 ((v0 . v64)(v1 . (d0))(v2 . v66))) ((= (* (* v64 (d0)) v66) (* v64 (* (d0) v66)))))
(147 (paramod 146 (1 1) 145 (1 1 2 2 2)) ((= (* (d0) (* v64 (* (b) (* v64 (* (d0) v66))))) (* v64 (* (* (d0) (* (a) (* (c0) v64))) v66)))))
(148 (instantiate 4 ((v0 . (d0))(v1 . (* (a) (* (c0) v64)))(v2 . v66))) ((= (* (* (d0) (* (a) (* (c0) v64))) v66) (* (d0) (* (* (a) (* (c0) v64)) v66)))))
(149 (paramod 148 (1 1) 147 (1 2 2)) ((= (* (d0) (* v64 (* (b) (* v64 (* (d0) v66))))) (* v64 (* (d0) (* (* (a) (* (c0) v64)) v66))))))
(150 (instantiate 4 ((v0 . (a))(v1 . (* (c0) v64))(v2 . v66))) ((= (* (* (a) (* (c0) v64)) v66) (* (a) (* (* (c0) v64) v66)))))
(151 (paramod 150 (1 1) 149 (1 2 2 2)) ((= (* (d0) (* v64 (* (b) (* v64 (* (d0) v66))))) (* v64 (* (d0) (* (a) (* (* (c0) v64) v66)))))))
(152 (instantiate 4 ((v0 . (c0))(v1 . v64)(v2 . v66))) ((= (* (* (c0) v64) v66) (* (c0) (* v64 v66)))))
(153 (paramod 152 (1 1) 151 (1 2 2 2 2)) ((= (* (d0) (* v64 (* (b) (* v64 (* (d0) v66))))) (* v64 (* (d0) (* (a) (* (c0) (* v64 v66))))))))
(154 (instantiate 153 ((v64 . v0)(v66 . v1))) ((= (* (d0) (* v0 (* (b) (* v0 (* (d0) v1))))) (* v0 (* (d0) (* (a) (* (c0) (* v0 v1))))))))
(155 (flip 154 (1)) ((= (* v0 (* (d0) (* (a) (* (c0) (* v0 v1))))) (* (d0) (* v0 (* (b) (* v0 (* (d0) v1))))))))
(156 (instantiate 63 ((v0 . (* (b0) (* v65 (* (b0) (d0))))))) ((= (* (b) (* (d0) (* (b0) (* v65 (* (b0) (d0)))))) (* (a) (* (c0) (* (b0) (* v65 (* (b0) (d0)))))))))
(157 (instantiate 70 ((v0 . (d0))(v1 . v65))) ((= (* (b) (* (d0) (* (b0) (* v65 (* (b0) (d0)))))) (* (a) (* (a0) (* (d0) (* v65 (* (d0) (b0)))))))))
(158 (paramod 156 (1 1) 157 (1 1)) ((= (* (a) (* (c0) (* (b0) (* v65 (* (b0) (d0)))))) (* (a) (* (a0) (* (d0) (* v65 (* (d0) (b0)))))))))
(159 (flip 158 (1)) ((= (* (a) (* (a0) (* (d0) (* v65 (* (d0) (b0)))))) (* (a) (* (c0) (* (b0) (* v65 (* (b0) (d0)))))))))
(160 (instantiate 159 ((v65 . v0))) ((= (* (a) (* (a0) (* (d0) (* v0 (* (d0) (b0)))))) (* (a) (* (c0) (* (b0) (* v0 (* (b0) (d0)))))))))
(161 (instantiate 14 ((v0 . (* (d) v65)))) ((= (* (b) (* (b0) (* (d) v65))) (* (a) (* (a0) (* (d) v65))))))
(162 (instantiate 91 ((v0 . (b))(v1 . v65))) ((= (* (c) (* (a0) (* (b) (* (b0) (* (d) v65))))) (* (b0) (* (d) (* (b) (* (c) (* (a0) v65))))))))
(163 (paramod 161 (1 1) 162 (1 1 2 2)) ((= (* (c) (* (a0) (* (a) (* (a0) (* (d) v65))))) (* (b0) (* (d) (* (b) (* (c) (* (a0) v65))))))))
(164 (flip 163 (1)) ((= (* (b0) (* (d) (* (b) (* (c) (* (a0) v65))))) (* (c) (* (a0) (* (a) (* (a0) (* (d) v65))))))))
(165 (instantiate 164 ((v65 . v0))) ((= (* (b0) (* (d) (* (b) (* (c) (* (a0) v0))))) (* (c) (* (a0) (* (a) (* (a0) (* (d) v0))))))))
(166 (instantiate 108 ((v0 . v64)(v1 . (d0)))) ((= (* (a) (* (a0) (* v64 (* (b0) (* (b) (d0)))))) (* (b0) (* (b) (* v64 (* (a) (* (a0) (d0)))))))))
(167 (paramod 8 (1 1) 166 (1 1 2 2 2 2)) ((= (* (a) (* (a0) (* v64 (* (b0) (* (a) (c0)))))) (* (b0) (* (b) (* v64 (* (a) (* (a0) (d0)))))))))
(168 (instantiate 167 ((v64 . v0))) ((= (* (a) (* (a0) (* v0 (* (b0) (* (a) (c0)))))) (* (b0) (* (b) (* v0 (* (a) (* (a0) (d0)))))))))
(169 (instantiate 126 ((v0 . v64)(v1 . (b0)))) ((= (* (a) (* (c0) (* v64 (* (d0) (* (b) (b0)))))) (* (d0) (* (b) (* v64 (* (a) (* (c0) (b0)))))))))
(170 (paramod 6 (1 1) 169 (1 1 2 2 2 2)) ((= (* (a) (* (c0) (* v64 (* (d0) (* (a) (a0)))))) (* (d0) (* (b) (* v64 (* (a) (* (c0) (b0)))))))))
(171 (instantiate 170 ((v64 . v0))) ((= (* (a) (* (c0) (* v0 (* (d0) (* (a) (a0)))))) (* (d0) (* (b) (* v0 (* (a) (* (c0) (b0)))))))))
(172 (instantiate 4 ((v2 . (* (a) (* (a0) v64))))) ((= (* (* v0 v1) (* (a) (* (a0) v64))) (* v0 (* v1 (* (a) (* (a0) v64)))))))
(173 (instantiate 130 ((v0 . v64)(v1 . (* v0 v1)))) ((= (* v64 (* (b0) (* (* v0 v1) (* (a) (* (a0) v64))))) (* (b0) (* v64 (* (* v0 v1) (* (b) (* v64 (b0)))))))))
(174 (paramod 172 (1 1) 173 (1 1 2 2)) ((= (* v64 (* (b0) (* v0 (* v1 (* (a) (* (a0) v64)))))) (* (b0) (* v64 (* (* v0 v1) (* (b) (* v64 (b0)))))))))
(175 (instantiate 4 ((v0 . v0)(v1 . v1)(v2 . (* (b) (* v64 (b0)))))) ((= (* (* v0 v1) (* (b) (* v64 (b0)))) (* v0 (* v1 (* (b) (* v64 (b0))))))))
(176 (paramod 175 (1 1) 174 (1 2 2 2)) ((= (* v64 (* (b0) (* v0 (* v1 (* (a) (* (a0) v64)))))) (* (b0) (* v64 (* v0 (* v1 (* (b) (* v64 (b0))))))))))
(177 (instantiate 176 ((v0 . v1)(v1 . v2)(v64 . v0))) ((= (* v0 (* (b0) (* v1 (* v2 (* (a) (* (a0) v0)))))) (* (b0) (* v0 (* v1 (* v2 (* (b) (* v0 (b0))))))))))
(178 (flip 177 (1)) ((= (* (b0) (* v0 (* v1 (* v2 (* (b) (* v0 (b0))))))) (* v0 (* (b0) (* v1 (* v2 (* (a) (* (a0) v0)))))))))
(179 (instantiate 54 ((v0 . v65)(v1 . v68)(v2 . v67)(v3 . v64))) ((= (* v65 (* v68 (* v67 (* v68 (* v65 v64))))) (* v68 (* v65 (* v67 (* v65 (* v68 v64))))))))
(180 (instantiate 136 ((v0 . v64)(v1 . v65)(v2 . v68)(v3 . v67)(v4 . v68))) ((= (* v64 (* v65 (* v68 (* v67 (* v68 (* v65 v64)))))) (* v65 (* v64 (* v68 (* v67 (* v68 (* v64 v65)))))))))
(181 (paramod 179 (1 1) 180 (1 1 2)) ((= (* v64 (* v68 (* v65 (* v67 (* v65 (* v68 v64)))))) (* v65 (* v64 (* v68 (* v67 (* v68 (* v64 v65)))))))))
(182 (instantiate 181 ((v64 . v0)(v65 . v2)(v67 . v3)(v68 . v1))) ((= (* v0 (* v1 (* v2 (* v3 (* v2 (* v1 v0)))))) (* v2 (* v0 (* v1 (* v3 (* v1 (* v0 v2)))))))))
(183 (instantiate 155 ((v0 . (d))(v1 . (b0)))) ((= (* (d) (* (d0) (* (a) (* (c0) (* (d) (b0)))))) (* (d0) (* (d) (* (b) (* (d) (* (d0) (b0)))))))))
(184 (paramod 7 (1 1) 183 (1 1 2 2 2 2)) ((= (* (d) (* (d0) (* (a) (* (c0) (* (c) (a0)))))) (* (d0) (* (d) (* (b) (* (d) (* (d0) (b0)))))))))
(185 (flip 184 (1)) ((= (* (d0) (* (d) (* (b) (* (d) (* (d0) (b0)))))) (* (d) (* (d0) (* (a) (* (c0) (* (c) (a0)))))))))
(186 (instantiate 3 ((v2 . (* v0 v1)))) ((not (= (* v0 v1) (* v0 v1))) (not (= (* v0 v3) (* v0 v1))) (= v1 v3)))
(187 (instantiate 2 ((v0 . (* v0 v1)))) ((= (* v0 v1) (* v0 v1))))
(188 (resolve 186 (1) 187 (1)) ((not (= (* v0 v3) (* v0 v1))) (= v1 v3)))
(189 (instantiate 188 ((v1 . v2)(v3 . v1))) ((not (= (* v0 v1) (* v0 v2))) (= v2 v1)))
(190 (instantiate 189 ((v0 . (a))(v1 . (* (a0) (* (d0) (* v64 (* (d0) (b0))))))(v2 . (* (c0) (* (b0) (* v64 (* (b0) (d0)))))))) ((not (= (* (a) (* (a0) (* (d0) (* v64 (* (d0) (b0)))))) (* (a) (* (c0) (* (b0) (* v64 (* (b0) (d0)))))))) (= (* (c0) (* (b0) (* v64 (* (b0) (d0))))) (* (a0) (* (d0) (* v64 (* (d0) (b0))))))))
(191 (instantiate 160 ((v0 . v64))) ((= (* (a) (* (a0) (* (d0) (* v64 (* (d0) (b0)))))) (* (a) (* (c0) (* (b0) (* v64 (* (b0) (d0)))))))))
(192 (resolve 190 (1) 191 (1)) ((= (* (c0) (* (b0) (* v64 (* (b0) (d0))))) (* (a0) (* (d0) (* v64 (* (d0) (b0))))))))
(193 (instantiate 192 ((v64 . v0))) ((= (* (c0) (* (b0) (* v0 (* (b0) (d0))))) (* (a0) (* (d0) (* v0 (* (d0) (b0))))))))
(194 (flip 193 (1)) ((= (* (a0) (* (d0) (* v0 (* (d0) (b0))))) (* (c0) (* (b0) (* v0 (* (b0) (d0))))))))
(195 (instantiate 4 ((v2 . (* (d0) (b0))))) ((= (* (* v0 v1) (* (d0) (b0))) (* v0 (* v1 (* (d0) (b0)))))))
(196 (instantiate 194 ((v0 . (* v0 v1)))) ((= (* (a0) (* (d0) (* (* v0 v1) (* (d0) (b0))))) (* (c0) (* (b0) (* (* v0 v1) (* (b0) (d0))))))))
(197 (paramod 195 (1 1) 196 (1 1 2 2)) ((= (* (a0) (* (d0) (* v0 (* v1 (* (d0) (b0)))))) (* (c0) (* (b0) (* (* v0 v1) (* (b0) (d0))))))))
(198 (instantiate 4 ((v0 . v0)(v1 . v1)(v2 . (* (b0) (d0))))) ((= (* (* v0 v1) (* (b0) (d0))) (* v0 (* v1 (* (b0) (d0)))))))
(199 (paramod 198 (1 1) 197 (1 2 2 2)) ((= (* (a0) (* (d0) (* v0 (* v1 (* (d0) (b0)))))) (* (c0) (* (b0) (* v0 (* v1 (* (b0) (d0)))))))))
(200 (instantiate 168 ((v0 . v67))) ((= (* (a) (* (a0) (* v67 (* (b0) (* (a) (c0)))))) (* (b0) (* (b) (* v67 (* (a) (* (a0) (d0)))))))))
(201 (instantiate 136 ((v0 . (c0))(v1 . (a))(v2 . (a0))(v3 . v67)(v4 . (b0)))) ((= (* (c0) (* (a) (* (a0) (* v67 (* (b0) (* (a) (c0))))))) (* (a) (* (c0) (* (a0) (* v67 (* (b0) (* (c0) (a))))))))))
(202 (paramod 200 (1 1) 201 (1 1 2)) ((= (* (c0) (* (b0) (* (b) (* v67 (* (a) (* (a0) (d0))))))) (* (a) (* (c0) (* (a0) (* v67 (* (b0) (* (c0) (a))))))))))
(203 (instantiate 202 ((v67 . v0))) ((= (* (c0) (* (b0) (* (b) (* v0 (* (a) (* (a0) (d0))))))) (* (a) (* (c0) (* (a0) (* v0 (* (b0) (* (c0) (a))))))))))
(204 (flip 203 (1)) ((= (* (a) (* (c0) (* (a0) (* v0 (* (b0) (* (c0) (a))))))) (* (c0) (* (b0) (* (b) (* v0 (* (a) (* (a0) (d0))))))))))
(205 (instantiate 171 ((v0 . v67))) ((= (* (a) (* (c0) (* v67 (* (d0) (* (a) (a0)))))) (* (d0) (* (b) (* v67 (* (a) (* (c0) (b0)))))))))
(206 (instantiate 136 ((v0 . (a0))(v1 . (a))(v2 . (c0))(v3 . v67)(v4 . (d0)))) ((= (* (a0) (* (a) (* (c0) (* v67 (* (d0) (* (a) (a0))))))) (* (a) (* (a0) (* (c0) (* v67 (* (d0) (* (a0) (a))))))))))
(207 (paramod 205 (1 1) 206 (1 1 2)) ((= (* (a0) (* (d0) (* (b) (* v67 (* (a) (* (c0) (b0))))))) (* (a) (* (a0) (* (c0) (* v67 (* (d0) (* (a0) (a))))))))))
(208 (instantiate 207 ((v67 . v0))) ((= (* (a0) (* (d0) (* (b) (* v0 (* (a) (* (c0) (b0))))))) (* (a) (* (a0) (* (c0) (* v0 (* (d0) (* (a0) (a))))))))))
(209 (flip 208 (1)) ((= (* (a) (* (a0) (* (c0) (* v0 (* (d0) (* (a0) (a))))))) (* (a0) (* (d0) (* (b) (* v0 (* (a) (* (c0) (b0))))))))))
(210 (instantiate 63 ((v0 . (b0)))) ((= (* (b) (* (d0) (b0))) (* (a) (* (c0) (b0))))))
(211 (instantiate 199 ((v0 . v64)(v1 . (b)))) ((= (* (a0) (* (d0) (* v64 (* (b) (* (d0) (b0)))))) (* (c0) (* (b0) (* v64 (* (b) (* (b0) (d0)))))))))
(212 (paramod 210 (1 1) 211 (1 1 2 2 2)) ((= (* (a0) (* (d0) (* v64 (* (a) (* (c0) (b0)))))) (* (c0) (* (b0) (* v64 (* (b) (* (b0) (d0)))))))))
(213 (instantiate 14 ((v0 . (d0)))) ((= (* (b) (* (b0) (d0))) (* (a) (* (a0) (d0))))))
(214 (paramod 213 (1 1) 212 (1 2 2 2 2)) ((= (* (a0) (* (d0) (* v64 (* (a) (* (c0) (b0)))))) (* (c0) (* (b0) (* v64 (* (a) (* (a0) (d0)))))))))
(215 (instantiate 214 ((v64 . v0))) ((= (* (a0) (* (d0) (* v0 (* (a) (* (c0) (b0)))))) (* (c0) (* (b0) (* v0 (* (a) (* (a0) (d0)))))))))
(216 (instantiate 4 ((v2 . (* (d0) (b0))))) ((= (* (* v0 v1) (* (d0) (b0))) (* v0 (* v1 (* (d0) (b0)))))))
(217 (instantiate 199 ((v0 . v64)(v1 . (* v0 v1)))) ((= (* (a0) (* (d0) (* v64 (* (* v0 v1) (* (d0) (b0)))))) (* (c0) (* (b0) (* v64 (* (* v0 v1) (* (b0) (d0)))))))))
(218 (paramod 216 (1 1) 217 (1 1 2 2 2)) ((= (* (a0) (* (d0) (* v64 (* v0 (* v1 (* (d0) (b0))))))) (* (c0) (* (b0) (* v64 (* (* v0 v1) (* (b0) (d0)))))))))
(219 (instantiate 4 ((v0 . v0)(v1 . v1)(v2 . (* (b0) (d0))))) ((= (* (* v0 v1) (* (b0) (d0))) (* v0 (* v1 (* (b0) (d0)))))))
(220 (paramod 219 (1 1) 218 (1 2 2 2 2)) ((= (* (a0) (* (d0) (* v64 (* v0 (* v1 (* (d0) (b0))))))) (* (c0) (* (b0) (* v64 (* v0 (* v1 (* (b0) (d0))))))))))
(221 (instantiate 220 ((v0 . v1)(v1 . v2)(v64 . v0))) ((= (* (a0) (* (d0) (* v0 (* v1 (* v2 (* (d0) (b0))))))) (* (c0) (* (b0) (* v0 (* v1 (* v2 (* (b0) (d0))))))))))
(222 (instantiate 4 ((v2 . (* (a) (* (c0) (b0)))))) ((= (* (* v0 v1) (* (a) (* (c0) (b0)))) (* v0 (* v1 (* (a) (* (c0) (b0))))))))
(223 (instantiate 215 ((v0 . (* v0 v1)))) ((= (* (a0) (* (d0) (* (* v0 v1) (* (a) (* (c0) (b0)))))) (* (c0) (* (b0) (* (* v0 v1) (* (a) (* (a0) (d0)))))))))
(224 (paramod 222 (1 1) 223 (1 1 2 2)) ((= (* (a0) (* (d0) (* v0 (* v1 (* (a) (* (c0) (b0))))))) (* (c0) (* (b0) (* (* v0 v1) (* (a) (* (a0) (d0)))))))))
(225 (instantiate 4 ((v0 . v0)(v1 . v1)(v2 . (* (a) (* (a0) (d0)))))) ((= (* (* v0 v1) (* (a) (* (a0) (d0)))) (* v0 (* v1 (* (a) (* (a0) (d0))))))))
(226 (paramod 225 (1 1) 224 (1 2 2 2)) ((= (* (a0) (* (d0) (* v0 (* v1 (* (a) (* (c0) (b0))))))) (* (c0) (* (b0) (* v0 (* v1 (* (a) (* (a0) (d0))))))))))
(227 (instantiate 226 ((v0 . (b))(v1 . v0))) ((= (* (a0) (* (d0) (* (b) (* v0 (* (a) (* (c0) (b0))))))) (* (c0) (* (b0) (* (b) (* v0 (* (a) (* (a0) (d0))))))))))
(228 (paramod 227 (1 1) 209 (1 2)) ((= (* (a) (* (a0) (* (c0) (* v0 (* (d0) (* (a0) (a))))))) (* (c0) (* (b0) (* (b) (* v0 (* (a) (* (a0) (d0))))))))))
(229 (instantiate 136 ((v0 . v64)(v1 . v65)(v2 . v66)(v3 . v67)(v4 . v66))) ((= (* v64 (* v65 (* v66 (* v67 (* v66 (* v65 v64)))))) (* v65 (* v64 (* v66 (* v67 (* v66 (* v64 v65)))))))))
(230 (instantiate 182 ((v0 . v64)(v1 . v65)(v2 . v66)(v3 . v67))) ((= (* v64 (* v65 (* v66 (* v67 (* v66 (* v65 v64)))))) (* v66 (* v64 (* v65 (* v67 (* v65 (* v64 v66)))))))))
(231 (paramod 229 (1 1) 230 (1 1)) ((= (* v65 (* v64 (* v66 (* v67 (* v66 (* v64 v65)))))) (* v66 (* v64 (* v65 (* v67 (* v65 (* v64 v66)))))))))
(232 (instantiate 231 ((v64 . v1)(v65 . v0)(v66 . v2)(v67 . v3))) ((= (* v0 (* v1 (* v2 (* v3 (* v2 (* v1 v0)))))) (* v2 (* v1 (* v0 (* v3 (* v0 (* v1 v2)))))))))
(233 (instantiate 221 ((v0 . (d))(v1 . (b))(v2 . (d)))) ((= (* (a0) (* (d0) (* (d) (* (b) (* (d) (* (d0) (b0))))))) (* (c0) (* (b0) (* (d) (* (b) (* (d) (* (b0) (d0))))))))))
(234 (paramod 185 (1 1) 233 (1 1 2)) ((= (* (a0) (* (d) (* (d0) (* (a) (* (c0) (* (c) (a0))))))) (* (c0) (* (b0) (* (d) (* (b) (* (d) (* (b0) (d0))))))))))
(235 (instantiate 20 ((v0 . (d0)))) ((= (* (d) (* (b0) (d0))) (* (c) (* (a0) (d0))))))
(236 (paramod 235 (1 1) 234 (1 2 2 2 2 2)) ((= (* (a0) (* (d) (* (d0) (* (a) (* (c0) (* (c) (a0))))))) (* (c0) (* (b0) (* (d) (* (b) (* (c) (* (a0) (d0))))))))))
(237 (instantiate 165 ((v0 . (d0)))) ((= (* (b0) (* (d) (* (b) (* (c) (* (a0) (d0)))))) (* (c) (* (a0) (* (a) (* (a0) (* (d) (d0)))))))))
(238 (paramod 237 (1 1) 236 (1 2 2)) ((= (* (a0) (* (d) (* (d0) (* (a) (* (c0) (* (c) (a0))))))) (* (c0) (* (c) (* (a0) (* (a) (* (a0) (* (d) (d0))))))))))
(239 (instantiate 3 ((v0 . (a))(v1 . (* (c0) (* (a0) (* v64 (* (b0) (* (c0) (a)))))))(v2 . (* (c0) (* (b0) (* (b) (* v64 (* (a) (* (a0) (d0)))))))))) ((not (= (* (a) (* (c0) (* (a0) (* v64 (* (b0) (* (c0) (a))))))) (* (c0) (* (b0) (* (b) (* v64 (* (a) (* (a0) (d0))))))))) (not (= (* (a) v3) (* (c0) (* (b0) (* (b) (* v64 (* (a) (* (a0) (d0))))))))) (= (* (c0) (* (a0) (* v64 (* (b0) (* (c0) (a)))))) v3)))
(240 (instantiate 204 ((v0 . v64))) ((= (* (a) (* (c0) (* (a0) (* v64 (* (b0) (* (c0) (a))))))) (* (c0) (* (b0) (* (b) (* v64 (* (a) (* (a0) (d0))))))))))
(241 (resolve 239 (1) 240 (1)) ((not (= (* (a) v3) (* (c0) (* (b0) (* (b) (* v64 (* (a) (* (a0) (d0))))))))) (= (* (c0) (* (a0) (* v64 (* (b0) (* (c0) (a)))))) v3)))
(242 (instantiate 241 ((v3 . v0)(v64 . v1))) ((not (= (* (a) v0) (* (c0) (* (b0) (* (b) (* v1 (* (a) (* (a0) (d0))))))))) (= (* (c0) (* (a0) (* v1 (* (b0) (* (c0) (a)))))) v0)))
(243 (instantiate 242 ((v0 . (* (a0) (* (c0) (* v64 (* (d0) (* (a0) (a)))))))(v1 . v64))) ((not (= (* (a) (* (a0) (* (c0) (* v64 (* (d0) (* (a0) (a))))))) (* (c0) (* (b0) (* (b) (* v64 (* (a) (* (a0) (d0))))))))) (= (* (c0) (* (a0) (* v64 (* (b0) (* (c0) (a)))))) (* (a0) (* (c0) (* v64 (* (d0) (* (a0) (a)))))))))
(244 (instantiate 228 ((v0 . v64))) ((= (* (a) (* (a0) (* (c0) (* v64 (* (d0) (* (a0) (a))))))) (* (c0) (* (b0) (* (b) (* v64 (* (a) (* (a0) (d0))))))))))
(245 (resolve 243 (1) 244 (1)) ((= (* (c0) (* (a0) (* v64 (* (b0) (* (c0) (a)))))) (* (a0) (* (c0) (* v64 (* (d0) (* (a0) (a)))))))))
(246 (instantiate 245 ((v64 . v0))) ((= (* (c0) (* (a0) (* v0 (* (b0) (* (c0) (a)))))) (* (a0) (* (c0) (* v0 (* (d0) (* (a0) (a)))))))))
(247 (instantiate 20 ((v0 . (* (c0) (a))))) ((= (* (d) (* (b0) (* (c0) (a)))) (* (c) (* (a0) (* (c0) (a)))))))
(248 (instantiate 246 ((v0 . (d)))) ((= (* (c0) (* (a0) (* (d) (* (b0) (* (c0) (a)))))) (* (a0) (* (c0) (* (d) (* (d0) (* (a0) (a)))))))))
(249 (paramod 247 (1 1) 248 (1 1 2 2)) ((= (* (c0) (* (a0) (* (c) (* (a0) (* (c0) (a)))))) (* (a0) (* (c0) (* (d) (* (d0) (* (a0) (a)))))))))
(250 (flip 249 (1)) ((= (* (a0) (* (c0) (* (d) (* (d0) (* (a0) (a)))))) (* (c0) (* (a0) (* (c) (* (a0) (* (c0) (a)))))))))
(251 (instantiate 3 ((v0 . v64)(v1 . (* v65 (* v66 (* v65 (* v64 v67)))))(v2 . (* v65 (* v64 (* v66 (* v64 (* v65 v67)))))))) ((not (= (* v64 (* v65 (* v66 (* v65 (* v64 v67))))) (* v65 (* v64 (* v66 (* v64 (* v65 v67))))))) (not (= (* v64 v3) (* v65 (* v64 (* v66 (* v64 (* v65 v67))))))) (= (* v65 (* v66 (* v65 (* v64 v67)))) v3)))
(252 (instantiate 54 ((v0 . v64)(v1 . v65)(v2 . v66)(v3 . v67))) ((= (* v64 (* v65 (* v66 (* v65 (* v64 v67))))) (* v65 (* v64 (* v66 (* v64 (* v65 v67))))))))
(253 (resolve 251 (1) 252 (1)) ((not (= (* v64 v3) (* v65 (* v64 (* v66 (* v64 (* v65 v67))))))) (= (* v65 (* v66 (* v65 (* v64 v67)))) v3)))
(254 (instantiate 253 ((v3 . v1)(v64 . v0)(v65 . v2)(v66 . v3)(v67 . v4))) ((not (= (* v0 v1) (* v2 (* v0 (* v3 (* v0 (* v2 v4))))))) (= (* v2 (* v3 (* v2 (* v0 v4)))) v1)))
(255 (instantiate 254 ((v0 . (a0))(v1 . (* (c0) (* (d) (* (d0) (* (a0) (a))))))(v2 . (c0))(v3 . (c))(v4 . (a)))) ((not (= (* (a0) (* (c0) (* (d) (* (d0) (* (a0) (a)))))) (* (c0) (* (a0) (* (c) (* (a0) (* (c0) (a)))))))) (= (* (c0) (* (c) (* (c0) (* (a0) (a))))) (* (c0) (* (d) (* (d0) (* (a0) (a))))))))
(256 (resolve 255 (1) 250 (1)) ((= (* (c0) (* (c) (* (c0) (* (a0) (a))))) (* (c0) (* (d) (* (d0) (* (a0) (a))))))))
(257 (flip 256 (1)) ((= (* (c0) (* (d) (* (d0) (* (a0) (a))))) (* (c0) (* (c) (* (c0) (* (a0) (a))))))))
(258 (instantiate 3 ((v2 . (* v0 v1)))) ((not (= (* v0 v1) (* v0 v1))) (not (= (* v0 v3) (* v0 v1))) (= v1 v3)))
(259 (instantiate 2 ((v0 . (* v0 v1)))) ((= (* v0 v1) (* v0 v1))))
(260 (resolve 258 (1) 259 (1)) ((not (= (* v0 v3) (* v0 v1))) (= v1 v3)))
(261 (instantiate 260 ((v1 . v2)(v3 . v1))) ((not (= (* v0 v1) (* v0 v2))) (= v2 v1)))
(262 (instantiate 261 ((v0 . (c0))(v1 . (* (d) (* (d0) (* (a0) (a)))))(v2 . (* (c) (* (c0) (* (a0) (a))))))) ((not (= (* (c0) (* (d) (* (d0) (* (a0) (a))))) (* (c0) (* (c) (* (c0) (* (a0) (a))))))) (= (* (c) (* (c0) (* (a0) (a)))) (* (d) (* (d0) (* (a0) (a)))))))
(263 (resolve 262 (1) 257 (1)) ((= (* (c) (* (c0) (* (a0) (a)))) (* (d) (* (d0) (* (a0) (a)))))))
(264 (flip 263 (1)) ((= (* (d) (* (d0) (* (a0) (a)))) (* (c) (* (c0) (* (a0) (a)))))))
(265 (instantiate 36 ((v0 . (a))(v1 . (a0))(v2 . (d))(v3 . (d0)))) ((= (* (a) (* (a0) (* (d) (* (d0) (* (a0) (a)))))) (* (a0) (* (a) (* (d) (* (d0) (* (a) (a0)))))))))
(266 (paramod 264 (1 1) 265 (1 1 2 2)) ((= (* (a) (* (a0) (* (c) (* (c0) (* (a0) (a)))))) (* (a0) (* (a) (* (d) (* (d0) (* (a) (a0)))))))))
(267 (flip 266 (1)) ((= (* (a0) (* (a) (* (d) (* (d0) (* (a) (a0)))))) (* (a) (* (a0) (* (c) (* (c0) (* (a0) (a)))))))))
(268 (instantiate 3 ((v0 . v64)(v1 . (* v65 (* v66 (* v67 (* v65 v64)))))(v2 . (* v65 (* v64 (* v66 (* v67 (* v64 v65)))))))) ((not (= (* v64 (* v65 (* v66 (* v67 (* v65 v64))))) (* v65 (* v64 (* v66 (* v67 (* v64 v65))))))) (not (= (* v64 v3) (* v65 (* v64 (* v66 (* v67 (* v64 v65))))))) (= (* v65 (* v66 (* v67 (* v65 v64)))) v3)))
(269 (instantiate 36 ((v0 . v64)(v1 . v65)(v2 . v66)(v3 . v67))) ((= (* v64 (* v65 (* v66 (* v67 (* v65 v64))))) (* v65 (* v64 (* v66 (* v67 (* v64 v65))))))))
(270 (resolve 268 (1) 269 (1)) ((not (= (* v64 v3) (* v65 (* v64 (* v66 (* v67 (* v64 v65))))))) (= (* v65 (* v66 (* v67 (* v65 v64)))) v3)))
(271 (instantiate 270 ((v3 . v1)(v64 . v0)(v65 . v2)(v66 . v3)(v67 . v4))) ((not (= (* v0 v1) (* v2 (* v0 (* v3 (* v4 (* v0 v2))))))) (= (* v2 (* v3 (* v4 (* v2 v0)))) v1)))
(272 (instantiate 271 ((v0 . (a0))(v1 . (* (a) (* (d) (* (d0) (* (a) (a0))))))(v2 . (a))(v3 . (c))(v4 . (c0)))) ((not (= (* (a0) (* (a) (* (d) (* (d0) (* (a) (a0)))))) (* (a) (* (a0) (* (c) (* (c0) (* (a0) (a)))))))) (= (* (a) (* (c) (* (c0) (* (a) (a0))))) (* (a) (* (d) (* (d0) (* (a) (a0))))))))
(273 (resolve 272 (1) 267 (1)) ((= (* (a) (* (c) (* (c0) (* (a) (a0))))) (* (a) (* (d) (* (d0) (* (a) (a0))))))))
(274 (flip 273 (1)) ((= (* (a) (* (d) (* (d0) (* (a) (a0))))) (* (a) (* (c) (* (c0) (* (a) (a0))))))))
(275 (instantiate 3 ((v2 . (* v0 v1)))) ((not (= (* v0 v1) (* v0 v1))) (not (= (* v0 v3) (* v0 v1))) (= v1 v3)))
(276 (instantiate 2 ((v0 . (* v0 v1)))) ((= (* v0 v1) (* v0 v1))))
(277 (resolve 275 (1) 276 (1)) ((not (= (* v0 v3) (* v0 v1))) (= v1 v3)))
(278 (instantiate 277 ((v1 . v2)(v3 . v1))) ((not (= (* v0 v1) (* v0 v2))) (= v2 v1)))
(279 (instantiate 278 ((v0 . (a))(v1 . (* (d) (* (d0) (* (a) (a0)))))(v2 . (* (c) (* (c0) (* (a) (a0))))))) ((not (= (* (a) (* (d) (* (d0) (* (a) (a0))))) (* (a) (* (c) (* (c0) (* (a) (a0))))))) (= (* (c) (* (c0) (* (a) (a0)))) (* (d) (* (d0) (* (a) (a0)))))))
(280 (resolve 279 (1) 274 (1)) ((= (* (c) (* (c0) (* (a) (a0)))) (* (d) (* (d0) (* (a) (a0)))))))
(281 (flip 280 (1)) ((= (* (d) (* (d0) (* (a) (a0)))) (* (c) (* (c0) (* (a) (a0)))))))
(282 (instantiate 4 ((v0 . (d))(v1 . (* (d0) (* (a) (a0))))(v2 . v66))) ((= (* (* (d) (* (d0) (* (a) (a0)))) v66) (* (d) (* (* (d0) (* (a) (a0))) v66)))))
(283 (paramod 281 (1 1) 282 (1 1 1)) ((= (* (* (c) (* (c0) (* (a) (a0)))) v66) (* (d) (* (* (d0) (* (a) (a0))) v66)))))
(284 (instantiate 4 ((v0 . (c))(v1 . (* (c0) (* (a) (a0))))(v2 . v66))) ((= (* (* (c) (* (c0) (* (a) (a0)))) v66) (* (c) (* (* (c0) (* (a) (a0))) v66)))))
(285 (paramod 284 (1 1) 283 (1 1)) ((= (* (c) (* (* (c0) (* (a) (a0))) v66)) (* (d) (* (* (d0) (* (a) (a0))) v66)))))
(286 (instantiate 4 ((v0 . (c0))(v1 . (* (a) (a0)))(v2 . v66))) ((= (* (* (c0) (* (a) (a0))) v66) (* (c0) (* (* (a) (a0)) v66)))))
(287 (paramod 286 (1 1) 285 (1 1 2)) ((= (* (c) (* (c0) (* (* (a) (a0)) v66))) (* (d) (* (* (d0) (* (a) (a0))) v66)))))
(288 (instantiate 4 ((v0 . (a))(v1 . (a0))(v2 . v66))) ((= (* (* (a) (a0)) v66) (* (a) (* (a0) v66)))))
(289 (paramod 288 (1 1) 287 (1 1 2 2)) ((= (* (c) (* (c0) (* (a) (* (a0) v66)))) (* (d) (* (* (d0) (* (a) (a0))) v66)))))
(290 (instantiate 4 ((v0 . (d0))(v1 . (* (a) (a0)))(v2 . v66))) ((= (* (* (d0) (* (a) (a0))) v66) (* (d0) (* (* (a) (a0)) v66)))))
(291 (paramod 290 (1 1) 289 (1 2 2)) ((= (* (c) (* (c0) (* (a) (* (a0) v66)))) (* (d) (* (d0) (* (* (a) (a0)) v66))))))
(292 (instantiate 4 ((v0 . (a))(v1 . (a0))(v2 . v66))) ((= (* (* (a) (a0)) v66) (* (a) (* (a0) v66)))))
(293 (paramod 292 (1 1) 291 (1 2 2 2)) ((= (* (c) (* (c0) (* (a) (* (a0) v66)))) (* (d) (* (d0) (* (a) (* (a0) v66)))))))
(294 (flip 293 (1)) ((= (* (d) (* (d0) (* (a) (* (a0) v66)))) (* (c) (* (c0) (* (a) (* (a0) v66)))))))
(295 (instantiate 294 ((v66 . v0))) ((= (* (d) (* (d0) (* (a) (* (a0) v0)))) (* (c) (* (c0) (* (a) (* (a0) v0)))))))
(296 (instantiate 295 ((v0 . v64))) ((= (* (d) (* (d0) (* (a) (* (a0) v64)))) (* (c) (* (c0) (* (a) (* (a0) v64)))))))
(297 (instantiate 177 ((v0 . v64)(v1 . (d))(v2 . (d0)))) ((= (* v64 (* (b0) (* (d) (* (d0) (* (a) (* (a0) v64)))))) (* (b0) (* v64 (* (d) (* (d0) (* (b) (* v64 (b0))))))))))
(298 (paramod 296 (1 1) 297 (1 1 2 2)) ((= (* v64 (* (b0) (* (c) (* (c0) (* (a) (* (a0) v64)))))) (* (b0) (* v64 (* (d) (* (d0) (* (b) (* v64 (b0))))))))))
(299 (flip 298 (1)) ((= (* (b0) (* v64 (* (d) (* (d0) (* (b) (* v64 (b0))))))) (* v64 (* (b0) (* (c) (* (c0) (* (a) (* (a0) v64)))))))))
(300 (instantiate 299 ((v64 . v0))) ((= (* (b0) (* v0 (* (d) (* (d0) (* (b) (* v0 (b0))))))) (* v0 (* (b0) (* (c) (* (c0) (* (a) (* (a0) v0)))))))))
(301 (instantiate 3 ((v0 . (b0))(v1 . (* v64 (* v65 (* v66 (* (b) (* v64 (b0)))))))(v2 . (* v64 (* (b0) (* v65 (* v66 (* (a) (* (a0) v64))))))))) ((not (= (* (b0) (* v64 (* v65 (* v66 (* (b) (* v64 (b0))))))) (* v64 (* (b0) (* v65 (* v66 (* (a) (* (a0) v64)))))))) (not (= (* (b0) v3) (* v64 (* (b0) (* v65 (* v66 (* (a) (* (a0) v64)))))))) (= (* v64 (* v65 (* v66 (* (b) (* v64 (b0)))))) v3)))
(302 (instantiate 178 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (* (b0) (* v64 (* v65 (* v66 (* (b) (* v64 (b0))))))) (* v64 (* (b0) (* v65 (* v66 (* (a) (* (a0) v64)))))))))
(303 (resolve 301 (1) 302 (1)) ((not (= (* (b0) v3) (* v64 (* (b0) (* v65 (* v66 (* (a) (* (a0) v64)))))))) (= (* v64 (* v65 (* v66 (* (b) (* v64 (b0)))))) v3)))
(304 (instantiate 303 ((v3 . v0)(v64 . v1)(v65 . v2)(v66 . v3))) ((not (= (* (b0) v0) (* v1 (* (b0) (* v2 (* v3 (* (a) (* (a0) v1)))))))) (= (* v1 (* v2 (* v3 (* (b) (* v1 (b0)))))) v0)))
(305 (instantiate 304 ((v0 . (* v64 (* (d) (* (d0) (* (b) (* v64 (b0)))))))(v1 . v64)(v2 . (c))(v3 . (c0)))) ((not (= (* (b0) (* v64 (* (d) (* (d0) (* (b) (* v64 (b0))))))) (* v64 (* (b0) (* (c) (* (c0) (* (a) (* (a0) v64)))))))) (= (* v64 (* (c) (* (c0) (* (b) (* v64 (b0)))))) (* v64 (* (d) (* (d0) (* (b) (* v64 (b0)))))))))
(306 (instantiate 300 ((v0 . v64))) ((= (* (b0) (* v64 (* (d) (* (d0) (* (b) (* v64 (b0))))))) (* v64 (* (b0) (* (c) (* (c0) (* (a) (* (a0) v64)))))))))
(307 (resolve 305 (1) 306 (1)) ((= (* v64 (* (c) (* (c0) (* (b) (* v64 (b0)))))) (* v64 (* (d) (* (d0) (* (b) (* v64 (b0)))))))))
(308 (instantiate 307 ((v64 . v0))) ((= (* v0 (* (c) (* (c0) (* (b) (* v0 (b0)))))) (* v0 (* (d) (* (d0) (* (b) (* v0 (b0)))))))))
(309 (flip 308 (1)) ((= (* v0 (* (d) (* (d0) (* (b) (* v0 (b0)))))) (* v0 (* (c) (* (c0) (* (b) (* v0 (b0)))))))))
(310 (instantiate 3 ((v2 . (* v0 v1)))) ((not (= (* v0 v1) (* v0 v1))) (not (= (* v0 v3) (* v0 v1))) (= v1 v3)))
(311 (instantiate 2 ((v0 . (* v0 v1)))) ((= (* v0 v1) (* v0 v1))))
(312 (resolve 310 (1) 311 (1)) ((not (= (* v0 v3) (* v0 v1))) (= v1 v3)))
(313 (instantiate 312 ((v1 . v2)(v3 . v1))) ((not (= (* v0 v1) (* v0 v2))) (= v2 v1)))
(314 (instantiate 313 ((v0 . v64)(v1 . (* (d) (* (d0) (* (b) (* v64 (b0))))))(v2 . (* (c) (* (c0) (* (b) (* v64 (b0)))))))) ((not (= (* v64 (* (d) (* (d0) (* (b) (* v64 (b0)))))) (* v64 (* (c) (* (c0) (* (b) (* v64 (b0)))))))) (= (* (c) (* (c0) (* (b) (* v64 (b0))))) (* (d) (* (d0) (* (b) (* v64 (b0))))))))
(315 (instantiate 309 ((v0 . v64))) ((= (* v64 (* (d) (* (d0) (* (b) (* v64 (b0)))))) (* v64 (* (c) (* (c0) (* (b) (* v64 (b0)))))))))
(316 (resolve 314 (1) 315 (1)) ((= (* (c) (* (c0) (* (b) (* v64 (b0))))) (* (d) (* (d0) (* (b) (* v64 (b0))))))))
(317 (instantiate 316 ((v64 . v0))) ((= (* (c) (* (c0) (* (b) (* v0 (b0))))) (* (d) (* (d0) (* (b) (* v0 (b0))))))))
(318 (flip 317 (1)) ((= (* (d) (* (d0) (* (b) (* v0 (b0))))) (* (c) (* (c0) (* (b) (* v0 (b0))))))))
(319 (instantiate 4 ((v2 . (b0)))) ((= (* (* v0 v1) (b0)) (* v0 (* v1 (b0))))))
(320 (instantiate 318 ((v0 . (* v0 v1)))) ((= (* (d) (* (d0) (* (b) (* (* v0 v1) (b0))))) (* (c) (* (c0) (* (b) (* (* v0 v1) (b0))))))))
(321 (paramod 319 (1 1) 320 (1 1 2 2 2)) ((= (* (d) (* (d0) (* (b) (* v0 (* v1 (b0)))))) (* (c) (* (c0) (* (b) (* (* v0 v1) (b0))))))))
(322 (instantiate 4 ((v0 . v0)(v1 . v1)(v2 . (b0)))) ((= (* (* v0 v1) (b0)) (* v0 (* v1 (b0))))))
(323 (paramod 322 (1 1) 321 (1 2 2 2 2)) ((= (* (d) (* (d0) (* (b) (* v0 (* v1 (b0)))))) (* (c) (* (c0) (* (b) (* v0 (* v1 (b0)))))))))
(324 (instantiate 54 ((v0 . (d))(v1 . (d0))(v2 . (b))(v3 . (b0)))) ((= (* (d) (* (d0) (* (b) (* (d0) (* (d) (b0)))))) (* (d0) (* (d) (* (b) (* (d) (* (d0) (b0)))))))))
(325 (instantiate 323 ((v0 . (d0))(v1 . (d)))) ((= (* (d) (* (d0) (* (b) (* (d0) (* (d) (b0)))))) (* (c) (* (c0) (* (b) (* (d0) (* (d) (b0)))))))))
(326 (paramod 324 (1 1) 325 (1 1)) ((= (* (d0) (* (d) (* (b) (* (d) (* (d0) (b0)))))) (* (c) (* (c0) (* (b) (* (d0) (* (d) (b0)))))))))
(327 (paramod 185 (1 1) 326 (1 1)) ((= (* (d) (* (d0) (* (a) (* (c0) (* (c) (a0)))))) (* (c) (* (c0) (* (b) (* (d0) (* (d) (b0)))))))))
(328 (paramod 7 (1 1) 327 (1 2 2 2 2 2)) ((= (* (d) (* (d0) (* (a) (* (c0) (* (c) (a0)))))) (* (c) (* (c0) (* (b) (* (d0) (* (c) (a0)))))))))
(329 (instantiate 63 ((v0 . (* (c) (a0))))) ((= (* (b) (* (d0) (* (c) (a0)))) (* (a) (* (c0) (* (c) (a0)))))))
(330 (paramod 329 (1 1) 328 (1 2 2 2)) ((= (* (d) (* (d0) (* (a) (* (c0) (* (c) (a0)))))) (* (c) (* (c0) (* (a) (* (c0) (* (c) (a0)))))))))
(331 (paramod 330 (1 1) 238 (1 1 2)) ((= (* (a0) (* (c) (* (c0) (* (a) (* (c0) (* (c) (a0))))))) (* (c0) (* (c) (* (a0) (* (a) (* (a0) (* (d) (d0))))))))))
(332 (flip 331 (1)) ((= (* (c0) (* (c) (* (a0) (* (a) (* (a0) (* (d) (d0))))))) (* (a0) (* (c) (* (c0) (* (a) (* (c0) (* (c) (a0))))))))))
(333 (instantiate 3 ((v0 . v64)(v1 . (* v65 (* v66 (* v67 (* v66 (* v65 v64))))))(v2 . (* v66 (* v65 (* v64 (* v67 (* v64 (* v65 v66))))))))) ((not (= (* v64 (* v65 (* v66 (* v67 (* v66 (* v65 v64)))))) (* v66 (* v65 (* v64 (* v67 (* v64 (* v65 v66)))))))) (not (= (* v64 v3) (* v66 (* v65 (* v64 (* v67 (* v64 (* v65 v66)))))))) (= (* v65 (* v66 (* v67 (* v66 (* v65 v64))))) v3)))
(334 (instantiate 232 ((v0 . v64)(v1 . v65)(v2 . v66)(v3 . v67))) ((= (* v64 (* v65 (* v66 (* v67 (* v66 (* v65 v64)))))) (* v66 (* v65 (* v64 (* v67 (* v64 (* v65 v66)))))))))
(335 (resolve 333 (1) 334 (1)) ((not (= (* v64 v3) (* v66 (* v65 (* v64 (* v67 (* v64 (* v65 v66)))))))) (= (* v65 (* v66 (* v67 (* v66 (* v65 v64))))) v3)))
(336 (instantiate 335 ((v3 . v1)(v64 . v0)(v65 . v3)(v66 . v2)(v67 . v4))) ((not (= (* v0 v1) (* v2 (* v3 (* v0 (* v4 (* v0 (* v3 v2)))))))) (= (* v3 (* v2 (* v4 (* v2 (* v3 v0))))) v1)))
(337 (instantiate 336 ((v0 . (c0))(v1 . (* (c) (* (a0) (* (a) (* (a0) (* (d) (d0)))))))(v2 . (a0))(v3 . (c))(v4 . (a)))) ((not (= (* (c0) (* (c) (* (a0) (* (a) (* (a0) (* (d) (d0))))))) (* (a0) (* (c) (* (c0) (* (a) (* (c0) (* (c) (a0))))))))) (= (* (c) (* (a0) (* (a) (* (a0) (* (c) (c0)))))) (* (c) (* (a0) (* (a) (* (a0) (* (d) (d0)))))))))
(338 (resolve 337 (1) 332 (1)) ((= (* (c) (* (a0) (* (a) (* (a0) (* (c) (c0)))))) (* (c) (* (a0) (* (a) (* (a0) (* (d) (d0)))))))))
(339 (flip 338 (1)) ((= (* (c) (* (a0) (* (a) (* (a0) (* (d) (d0)))))) (* (c) (* (a0) (* (a) (* (a0) (* (c) (c0)))))))))
(340 (instantiate 3 ((v2 . (* v0 v1)))) ((not (= (* v0 v1) (* v0 v1))) (not (= (* v0 v3) (* v0 v1))) (= v1 v3)))
(341 (instantiate 2 ((v0 . (* v0 v1)))) ((= (* v0 v1) (* v0 v1))))
(342 (resolve 340 (1) 341 (1)) ((not (= (* v0 v3) (* v0 v1))) (= v1 v3)))
(343 (instantiate 342 ((v1 . v2)(v3 . v1))) ((not (= (* v0 v1) (* v0 v2))) (= v2 v1)))
(344 (instantiate 343 ((v0 . (c))(v1 . (* (a0) (* (a) (* (a0) (* (d) (d0))))))(v2 . (* (a0) (* (a) (* (a0) (* (c) (c0)))))))) ((not (= (* (c) (* (a0) (* (a) (* (a0) (* (d) (d0)))))) (* (c) (* (a0) (* (a) (* (a0) (* (c) (c0)))))))) (= (* (a0) (* (a) (* (a0) (* (c) (c0))))) (* (a0) (* (a) (* (a0) (* (d) (d0))))))))
(345 (resolve 344 (1) 339 (1)) ((= (* (a0) (* (a) (* (a0) (* (c) (c0))))) (* (a0) (* (a) (* (a0) (* (d) (d0))))))))
(346 (flip 345 (1)) ((= (* (a0) (* (a) (* (a0) (* (d) (d0))))) (* (a0) (* (a) (* (a0) (* (c) (c0))))))))
(347 (instantiate 3 ((v2 . (* v0 v1)))) ((not (= (* v0 v1) (* v0 v1))) (not (= (* v0 v3) (* v0 v1))) (= v1 v3)))
(348 (instantiate 2 ((v0 . (* v0 v1)))) ((= (* v0 v1) (* v0 v1))))
(349 (resolve 347 (1) 348 (1)) ((not (= (* v0 v3) (* v0 v1))) (= v1 v3)))
(350 (instantiate 349 ((v1 . v2)(v3 . v1))) ((not (= (* v0 v1) (* v0 v2))) (= v2 v1)))
(351 (instantiate 350 ((v0 . (a0))(v1 . (* (a) (* (a0) (* (d) (d0)))))(v2 . (* (a) (* (a0) (* (c) (c0))))))) ((not (= (* (a0) (* (a) (* (a0) (* (d) (d0))))) (* (a0) (* (a) (* (a0) (* (c) (c0))))))) (= (* (a) (* (a0) (* (c) (c0)))) (* (a) (* (a0) (* (d) (d0)))))))
(352 (resolve 351 (1) 346 (1)) ((= (* (a) (* (a0) (* (c) (c0)))) (* (a) (* (a0) (* (d) (d0)))))))
(353 (flip 352 (1)) ((= (* (a) (* (a0) (* (d) (d0)))) (* (a) (* (a0) (* (c) (c0)))))))
(354 (instantiate 3 ((v2 . (* v0 v1)))) ((not (= (* v0 v1) (* v0 v1))) (not (= (* v0 v3) (* v0 v1))) (= v1 v3)))
(355 (instantiate 2 ((v0 . (* v0 v1)))) ((= (* v0 v1) (* v0 v1))))
(356 (resolve 354 (1) 355 (1)) ((not (= (* v0 v3) (* v0 v1))) (= v1 v3)))
(357 (instantiate 356 ((v1 . v2)(v3 . v1))) ((not (= (* v0 v1) (* v0 v2))) (= v2 v1)))
(358 (instantiate 357 ((v0 . (a))(v1 . (* (a0) (* (d) (d0))))(v2 . (* (a0) (* (c) (c0)))))) ((not (= (* (a) (* (a0) (* (d) (d0)))) (* (a) (* (a0) (* (c) (c0)))))) (= (* (a0) (* (c) (c0))) (* (a0) (* (d) (d0))))))
(359 (resolve 358 (1) 353 (1)) ((= (* (a0) (* (c) (c0))) (* (a0) (* (d) (d0))))))
(360 (flip 359 (1)) ((= (* (a0) (* (d) (d0))) (* (a0) (* (c) (c0))))))
(361 (instantiate 3 ((v2 . (* v0 v1)))) ((not (= (* v0 v1) (* v0 v1))) (not (= (* v0 v3) (* v0 v1))) (= v1 v3)))
(362 (instantiate 2 ((v0 . (* v0 v1)))) ((= (* v0 v1) (* v0 v1))))
(363 (resolve 361 (1) 362 (1)) ((not (= (* v0 v3) (* v0 v1))) (= v1 v3)))
(364 (instantiate 363 ((v1 . v2)(v3 . v1))) ((not (= (* v0 v1) (* v0 v2))) (= v2 v1)))
(365 (instantiate 364 ((v0 . (a0))(v1 . (* (d) (d0)))(v2 . (* (c) (c0))))) ((not (= (* (a0) (* (d) (d0))) (* (a0) (* (c) (c0))))) (= (* (c) (c0)) (* (d) (d0)))))
(366 (resolve 365 (1) 360 (1)) ((= (* (c) (c0)) (* (d) (d0)))))
(367 (flip 366 (1)) ((= (* (d) (d0)) (* (c) (c0)))))
(368 (resolve 1 (1) 367 (1)) ())
)