;; ----- Otter 3.0.4, August 1995 -----
;; The job was started by mccune on gyro, Wed Nov  1 22:23:42 1995
;;
;;;; x=x.
;;;; 1*x=x.
;;;; x*1=x.
;;;; x* (x\y)=y.
;;;; x\ (x*y)=y.
;;;; (x/y)*y=x.
;;;; (x*y)/y=x.
;;;; x*R(x)=1.
;;;; L(x)*x=1.
;;;; (x* (y*z))*x= (x*y)* (z*x).
;;;; ((A*B)*C)*B!=A* (B* (C*B)).
;;
;; ----> UNIT CONFLICT at  11.55 sec ----> 956 [binary,954.1,20.1] $F.
;;
(
(1 (input) ((= (* (1) v0) v0)))
(2 (input) ((= (* v0 (1)) v0)))
(3 (input) ((= (* v0 (\ v0 v1)) v1)))
(4 (input) ((= (\ v0 (* v0 v1)) v1)))
(5 (input) ((= (* (/ v0 v1) v1) v0)))
(6 (input) ((= (/ (* v0 v1) v1) v0)))
(7 (input) ((= (* v0 (R v0)) (1))))
(8 (input) ((= (* (* v0 (* v1 v2)) v0) (* (* v0 v1) (* v2 v0)))))
(9 (input) ((not (= (* (* (* (A) (B)) (C)) (B)) (* (A) (* (B) (* (C) (B))))))))
(10 (instantiate 7 ((v0 . v64))) ((= (* v64 (R v64)) (1))))
(11 (instantiate 4 ((v0 . v64)(v1 . (R v64)))) ((= (\ v64 (* v64 (R v64))) (R v64))))
(12 (paramod 10 (1 1) 11 (1 1 2)) ((= (\ v64 (1)) (R v64))))
(13 (instantiate 12 ((v64 . v0))) ((= (\ v0 (1)) (R v0))))
(14 (instantiate 2 ((v0 . v64))) ((= (* v64 (1)) v64)))
(15 (instantiate 4 ((v0 . v64)(v1 . (1)))) ((= (\ v64 (* v64 (1))) (1))))
(16 (paramod 14 (1 1) 15 (1 1 2)) ((= (\ v64 v64) (1))))
(17 (instantiate 16 ((v64 . v0))) ((= (\ v0 v0) (1))))
(18 (instantiate 5 ((v1 . v66))) ((= (* (/ v0 v66) v66) v0)))
(19 (instantiate 8 ((v0 . v64)(v1 . (/ v0 v66))(v2 . v66))) ((= (* (* v64 (* (/ v0 v66) v66)) v64) (* (* v64 (/ v0 v66)) (* v66 v64)))))
(20 (paramod 18 (1 1) 19 (1 1 1 2)) ((= (* (* v64 v0) v64) (* (* v64 (/ v0 v66)) (* v66 v64)))))
(21 (flip 20 (1)) ((= (* (* v64 (/ v0 v66)) (* v66 v64)) (* (* v64 v0) v64))))
(22 (instantiate 21 ((v0 . v1)(v64 . v0)(v66 . v2))) ((= (* (* v0 (/ v1 v2)) (* v2 v0)) (* (* v0 v1) v0))))
(23 (instantiate 3 ((v0 . v65))) ((= (* v65 (\ v65 v1)) v1)))
(24 (instantiate 8 ((v0 . v64)(v1 . v65)(v2 . (\ v65 v1)))) ((= (* (* v64 (* v65 (\ v65 v1))) v64) (* (* v64 v65) (* (\ v65 v1) v64)))))
(25 (paramod 23 (1 1) 24 (1 1 1 2)) ((= (* (* v64 v1) v64) (* (* v64 v65) (* (\ v65 v1) v64)))))
(26 (instantiate 25 ((v64 . v0)(v65 . v2))) ((= (* (* v0 v1) v0) (* (* v0 v2) (* (\ v2 v1) v0)))))
(27 (instantiate 1 ((v0 . v66))) ((= (* (1) v66) v66)))
(28 (instantiate 8 ((v0 . v64)(v1 . (1))(v2 . v66))) ((= (* (* v64 (* (1) v66)) v64) (* (* v64 (1)) (* v66 v64)))))
(29 (paramod 27 (1 1) 28 (1 1 1 2)) ((= (* (* v64 v66) v64) (* (* v64 (1)) (* v66 v64)))))
(30 (instantiate 2 ((v0 . v64))) ((= (* v64 (1)) v64)))
(31 (paramod 30 (1 1) 29 (1 2 1)) ((= (* (* v64 v66) v64) (* v64 (* v66 v64)))))
(32 (instantiate 31 ((v64 . v0)(v66 . v1))) ((= (* (* v0 v1) v0) (* v0 (* v1 v0)))))
(33 (paramod 32 (1 1) 26 (1 1)) ((= (* v0 (* v1 v0)) (* (* v0 v2) (* (\ v2 v1) v0)))))
(34 (flip 33 (1)) ((= (* (* v0 v2) (* (\ v2 v1) v0)) (* v0 (* v1 v0)))))
(35 (instantiate 34 ((v1 . v2)(v2 . v1))) ((= (* (* v0 v1) (* (\ v1 v2) v0)) (* v0 (* v2 v0)))))
(36 (paramod 32 (1 1) 22 (1 2)) ((= (* (* v0 (/ v1 v2)) (* v2 v0)) (* v0 (* v1 v0)))))
(37 (instantiate 32 ((v0 . v0)(v1 . (* v1 v2)))) ((= (* (* v0 (* v1 v2)) v0) (* v0 (* (* v1 v2) v0)))))
(38 (paramod 37 (1 1) 8 (1 1)) ((= (* v0 (* (* v1 v2) v0)) (* (* v0 v1) (* v2 v0)))))
(39 (instantiate 7 ((v0 . v64))) ((= (* v64 (R v64)) (1))))
(40 (instantiate 32 ((v0 . v64)(v1 . (R v64)))) ((= (* (* v64 (R v64)) v64) (* v64 (* (R v64) v64)))))
(41 (paramod 39 (1 1) 40 (1 1 1)) ((= (* (1) v64) (* v64 (* (R v64) v64)))))
(42 (instantiate 1 ((v0 . v64))) ((= (* (1) v64) v64)))
(43 (paramod 42 (1 1) 41 (1 1)) ((= v64 (* v64 (* (R v64) v64)))))
(44 (flip 43 (1)) ((= (* v64 (* (R v64) v64)) v64)))
(45 (instantiate 44 ((v64 . v0))) ((= (* v0 (* (R v0) v0)) v0)))
(46 (instantiate 3 ((v0 . v64))) ((= (* v64 (\ v64 v1)) v1)))
(47 (instantiate 32 ((v0 . v64)(v1 . (\ v64 v1)))) ((= (* (* v64 (\ v64 v1)) v64) (* v64 (* (\ v64 v1) v64)))))
(48 (paramod 46 (1 1) 47 (1 1 1)) ((= (* v1 v64) (* v64 (* (\ v64 v1) v64)))))
(49 (flip 48 (1)) ((= (* v64 (* (\ v64 v1) v64)) (* v1 v64))))
(50 (instantiate 49 ((v64 . v0))) ((= (* v0 (* (\ v0 v1) v0)) (* v1 v0))))
(51 (instantiate 32 ((v0 . v65))) ((= (* (* v65 v1) v65) (* v65 (* v1 v65)))))
(52 (instantiate 6 ((v0 . (* v65 v1))(v1 . v65))) ((= (/ (* (* v65 v1) v65) v65) (* v65 v1))))
(53 (paramod 51 (1 1) 52 (1 1 1)) ((= (/ (* v65 (* v1 v65)) v65) (* v65 v1))))
(54 (instantiate 53 ((v65 . v0))) ((= (/ (* v0 (* v1 v0)) v0) (* v0 v1))))
(55 (instantiate 45 ((v0 . v64))) ((= (* v64 (* (R v64) v64)) v64)))
(56 (instantiate 4 ((v0 . v64)(v1 . (* (R v64) v64)))) ((= (\ v64 (* v64 (* (R v64) v64))) (* (R v64) v64))))
(57 (paramod 55 (1 1) 56 (1 1 2)) ((= (\ v64 v64) (* (R v64) v64))))
(58 (instantiate 17 ((v0 . v64))) ((= (\ v64 v64) (1))))
(59 (paramod 58 (1 1) 57 (1 1)) ((= (1) (* (R v64) v64))))
(60 (flip 59 (1)) ((= (* (R v64) v64) (1))))
(61 (instantiate 60 ((v64 . v0))) ((= (* (R v0) v0) (1))))
(62 (instantiate 61 ((v0 . v65))) ((= (* (R v65) v65) (1))))
(63 (instantiate 4 ((v0 . (R v65))(v1 . v65))) ((= (\ (R v65) (* (R v65) v65)) v65)))
(64 (paramod 62 (1 1) 63 (1 1 2)) ((= (\ (R v65) (1)) v65)))
(65 (instantiate 13 ((v0 . (R v65)))) ((= (\ (R v65) (1)) (R (R v65)))))
(66 (paramod 65 (1 1) 64 (1 1)) ((= (R (R v65)) v65)))
(67 (instantiate 66 ((v65 . v0))) ((= (R (R v0)) v0)))
(68 (instantiate 50 ((v0 . v64))) ((= (* v64 (* (\ v64 v1) v64)) (* v1 v64))))
(69 (instantiate 4 ((v0 . v64)(v1 . (* (\ v64 v1) v64)))) ((= (\ v64 (* v64 (* (\ v64 v1) v64))) (* (\ v64 v1) v64))))
(70 (paramod 68 (1 1) 69 (1 1 2)) ((= (\ v64 (* v1 v64)) (* (\ v64 v1) v64))))
(71 (instantiate 70 ((v64 . v0))) ((= (\ v0 (* v1 v0)) (* (\ v0 v1) v0))))
(72 (instantiate 61 ((v0 . v65))) ((= (* (R v65) v65) (1))))
(73 (instantiate 35 ((v0 . (R v65))(v1 . v65)(v2 . v66))) ((= (* (* (R v65) v65) (* (\ v65 v66) (R v65))) (* (R v65) (* v66 (R v65))))))
(74 (paramod 72 (1 1) 73 (1 1 1)) ((= (* (1) (* (\ v65 v66) (R v65))) (* (R v65) (* v66 (R v65))))))
(75 (instantiate 1 ((v0 . (* (\ v65 v66) (R v65))))) ((= (* (1) (* (\ v65 v66) (R v65))) (* (\ v65 v66) (R v65)))))
(76 (paramod 75 (1 1) 74 (1 1)) ((= (* (\ v65 v66) (R v65)) (* (R v65) (* v66 (R v65))))))
(77 (instantiate 76 ((v65 . v0)(v66 . v1))) ((= (* (\ v0 v1) (R v0)) (* (R v0) (* v1 (R v0))))))
(78 (instantiate 5 ((v1 . v64))) ((= (* (/ v0 v64) v64) v0)))
(79 (instantiate 54 ((v0 . v64)(v1 . (/ v0 v64)))) ((= (/ (* v64 (* (/ v0 v64) v64)) v64) (* v64 (/ v0 v64)))))
(80 (paramod 78 (1 1) 79 (1 1 1 2)) ((= (/ (* v64 v0) v64) (* v64 (/ v0 v64)))))
(81 (instantiate 80 ((v0 . v1)(v64 . v0))) ((= (/ (* v0 v1) v0) (* v0 (/ v1 v0)))))
(82 (instantiate 7 ((v0 . v66))) ((= (* v66 (R v66)) (1))))
(83 (instantiate 36 ((v0 . (R v66))(v1 . v65)(v2 . v66))) ((= (* (* (R v66) (/ v65 v66)) (* v66 (R v66))) (* (R v66) (* v65 (R v66))))))
(84 (paramod 82 (1 1) 83 (1 1 2)) ((= (* (* (R v66) (/ v65 v66)) (1)) (* (R v66) (* v65 (R v66))))))
(85 (instantiate 2 ((v0 . (* (R v66) (/ v65 v66))))) ((= (* (* (R v66) (/ v65 v66)) (1)) (* (R v66) (/ v65 v66)))))
(86 (paramod 85 (1 1) 84 (1 1)) ((= (* (R v66) (/ v65 v66)) (* (R v66) (* v65 (R v66))))))
(87 (instantiate 86 ((v65 . v1)(v66 . v0))) ((= (* (R v0) (/ v1 v0)) (* (R v0) (* v1 (R v0))))))
(88 (instantiate 5 ((v1 . v64))) ((= (* (/ v0 v64) v64) v0)))
(89 (instantiate 36 ((v0 . v64)(v1 . v65)(v2 . (/ v0 v64)))) ((= (* (* v64 (/ v65 (/ v0 v64))) (* (/ v0 v64) v64)) (* v64 (* v65 v64)))))
(90 (paramod 88 (1 1) 89 (1 1 2)) ((= (* (* v64 (/ v65 (/ v0 v64))) v0) (* v64 (* v65 v64)))))
(91 (instantiate 90 ((v0 . v2)(v64 . v0)(v65 . v1))) ((= (* (* v0 (/ v1 (/ v2 v0))) v2) (* v0 (* v1 v0)))))
(92 (instantiate 38 ((v0 . v64))) ((= (* v64 (* (* v1 v2) v64)) (* (* v64 v1) (* v2 v64)))))
(93 (instantiate 4 ((v0 . v64)(v1 . (* (* v1 v2) v64)))) ((= (\ v64 (* v64 (* (* v1 v2) v64))) (* (* v1 v2) v64))))
(94 (paramod 92 (1 1) 93 (1 1 2)) ((= (\ v64 (* (* v64 v1) (* v2 v64))) (* (* v1 v2) v64))))
(95 (instantiate 94 ((v64 . v0))) ((= (\ v0 (* (* v0 v1) (* v2 v0))) (* (* v1 v2) v0))))
(96 (instantiate 5 ((v1 . v64))) ((= (* (/ v0 v64) v64) v0)))
(97 (instantiate 71 ((v0 . v64)(v1 . (/ v0 v64)))) ((= (\ v64 (* (/ v0 v64) v64)) (* (\ v64 (/ v0 v64)) v64))))
(98 (paramod 96 (1 1) 97 (1 1 2)) ((= (\ v64 v0) (* (\ v64 (/ v0 v64)) v64))))
(99 (flip 98 (1)) ((= (* (\ v64 (/ v0 v64)) v64) (\ v64 v0))))
(100 (instantiate 99 ((v0 . v1)(v64 . v0))) ((= (* (\ v0 (/ v1 v0)) v0) (\ v0 v1))))
(101 (instantiate 3 ((v0 . v64))) ((= (* v64 (\ v64 v1)) v1)))
(102 (instantiate 81 ((v0 . v64)(v1 . (\ v64 v1)))) ((= (/ (* v64 (\ v64 v1)) v64) (* v64 (/ (\ v64 v1) v64)))))
(103 (paramod 101 (1 1) 102 (1 1 1)) ((= (/ v1 v64) (* v64 (/ (\ v64 v1) v64)))))
(104 (flip 103 (1)) ((= (* v64 (/ (\ v64 v1) v64)) (/ v1 v64))))
(105 (instantiate 104 ((v64 . v0))) ((= (* v0 (/ (\ v0 v1) v0)) (/ v1 v0))))
(106 (instantiate 100 ((v0 . v65))) ((= (* (\ v65 (/ v1 v65)) v65) (\ v65 v1))))
(107 (instantiate 6 ((v0 . (\ v65 (/ v1 v65)))(v1 . v65))) ((= (/ (* (\ v65 (/ v1 v65)) v65) v65) (\ v65 (/ v1 v65)))))
(108 (paramod 106 (1 1) 107 (1 1 1)) ((= (/ (\ v65 v1) v65) (\ v65 (/ v1 v65)))))
(109 (flip 108 (1)) ((= (\ v65 (/ v1 v65)) (/ (\ v65 v1) v65))))
(110 (instantiate 109 ((v65 . v0))) ((= (\ v0 (/ v1 v0)) (/ (\ v0 v1) v0))))
(111 (instantiate 6 ((v0 . (\ v0 v1))(v1 . (R v0)))) ((= (/ (* (\ v0 v1) (R v0)) (R v0)) (\ v0 v1))))
(112 (paramod 77 (1 1) 111 (1 1 1)) ((= (/ (* (R v0) (* v1 (R v0))) (R v0)) (\ v0 v1))))
(113 (instantiate 81 ((v0 . (R v0))(v1 . (* v1 (R v0))))) ((= (/ (* (R v0) (* v1 (R v0))) (R v0)) (* (R v0) (/ (* v1 (R v0)) (R v0))))))
(114 (paramod 113 (1 1) 112 (1 1)) ((= (* (R v0) (/ (* v1 (R v0)) (R v0))) (\ v0 v1))))
(115 (instantiate 6 ((v0 . v1)(v1 . (R v0)))) ((= (/ (* v1 (R v0)) (R v0)) v1)))
(116 (paramod 115 (1 1) 114 (1 1 2)) ((= (* (R v0) v1) (\ v0 v1))))
(117 (flip 116 (1)) ((= (\ v0 v1) (* (R v0) v1))))
(118 (instantiate 117 ((v0 . v0)(v1 . (/ v1 v0)))) ((= (\ v0 (/ v1 v0)) (* (R v0) (/ v1 v0)))))
(119 (paramod 118 (1 1) 110 (1 1)) ((= (* (R v0) (/ v1 v0)) (/ (\ v0 v1) v0))))
(120 (paramod 87 (1 1) 119 (1 1)) ((= (* (R v0) (* v1 (R v0))) (/ (\ v0 v1) v0))))
(121 (paramod 117 (1 1) 120 (1 2 1)) ((= (* (R v0) (* v1 (R v0))) (/ (* (R v0) v1) v0))))
(122 (flip 121 (1)) ((= (/ (* (R v0) v1) v0) (* (R v0) (* v1 (R v0))))))
(123 (paramod 117 (1 1) 105 (1 1 2 1)) ((= (* v0 (/ (* (R v0) v1) v0)) (/ v1 v0))))
(124 (paramod 122 (1 1) 123 (1 1 2)) ((= (* v0 (* (R v0) (* v1 (R v0)))) (/ v1 v0))))
(125 (flip 124 (1)) ((= (/ v1 v0) (* v0 (* (R v0) (* v1 (R v0)))))))
(126 (instantiate 125 ((v0 . v1)(v1 . v0))) ((= (/ v0 v1) (* v1 (* (R v1) (* v0 (R v1)))))))
(127 (instantiate 117 ((v0 . v0)(v1 . (* (* v0 v1) (* v2 v0))))) ((= (\ v0 (* (* v0 v1) (* v2 v0))) (* (R v0) (* (* v0 v1) (* v2 v0))))))
(128 (paramod 127 (1 1) 95 (1 1)) ((= (* (R v0) (* (* v0 v1) (* v2 v0))) (* (* v1 v2) v0))))
(129 (instantiate 117 ((v0 . v0)(v1 . (* v0 v1)))) ((= (\ v0 (* v0 v1)) (* (R v0) (* v0 v1)))))
(130 (paramod 129 (1 1) 4 (1 1)) ((= (* (R v0) (* v0 v1)) v1)))
(131 (paramod 117 (1 1) 3 (1 1 2)) ((= (* v0 (* (R v0) v1)) v1)))
(132 (instantiate 126 ((v0 . v2)(v1 . v0))) ((= (/ v2 v0) (* v0 (* (R v0) (* v2 (R v0)))))))
(133 (paramod 132 (1 1) 91 (1 1 1 2 2)) ((= (* (* v0 (/ v1 (* v0 (* (R v0) (* v2 (R v0)))))) v2) (* v0 (* v1 v0)))))
(134 (instantiate 131 ((v0 . v0)(v1 . (* v2 (R v0))))) ((= (* v0 (* (R v0) (* v2 (R v0)))) (* v2 (R v0)))))
(135 (paramod 134 (1 1) 133 (1 1 1 2 2)) ((= (* (* v0 (/ v1 (* v2 (R v0)))) v2) (* v0 (* v1 v0)))))
(136 (instantiate 126 ((v0 . v1)(v1 . (* v2 (R v0))))) ((= (/ v1 (* v2 (R v0))) (* (* v2 (R v0)) (* (R (* v2 (R v0))) (* v1 (R (* v2 (R v0)))))))))
(137 (paramod 136 (1 1) 135 (1 1 1 2)) ((= (* (* v0 (* (* v2 (R v0)) (* (R (* v2 (R v0))) (* v1 (R (* v2 (R v0))))))) v2) (* v0 (* v1 v0)))))
(138 (instantiate 131 ((v0 . (* v2 (R v0)))(v1 . (* v1 (R (* v2 (R v0))))))) ((= (* (* v2 (R v0)) (* (R (* v2 (R v0))) (* v1 (R (* v2 (R v0)))))) (* v1 (R (* v2 (R v0)))))))
(139 (paramod 138 (1 1) 137 (1 1 1 2)) ((= (* (* v0 (* v1 (R (* v2 (R v0))))) v2) (* v0 (* v1 v0)))))
(140 (paramod 126 (1 1) 5 (1 1 1)) ((= (* (* v1 (* (R v1) (* v0 (R v1)))) v1) v0)))
(141 (instantiate 131 ((v0 . v1)(v1 . (* v0 (R v1))))) ((= (* v1 (* (R v1) (* v0 (R v1)))) (* v0 (R v1)))))
(142 (paramod 141 (1 1) 140 (1 1 1)) ((= (* (* v0 (R v1)) v1) v0)))
(143 (instantiate 142 ((v0 . v64)(v1 . (R v0)))) ((= (* (* v64 (R (R v0))) (R v0)) v64)))
(144 (paramod 67 (1 1) 143 (1 1 1 2)) ((= (* (* v64 v0) (R v0)) v64)))
(145 (instantiate 144 ((v0 . v1)(v64 . v0))) ((= (* (* v0 v1) (R v1)) v0)))
(146 (instantiate 145 ((v0 . (R v0))(v1 . (* v0 v1)))) ((= (* (* (R v0) (* v0 v1)) (R (* v0 v1))) (R v0))))
(147 (paramod 130 (1 1) 146 (1 1 1)) ((= (* v1 (R (* v0 v1))) (R v0))))
(148 (instantiate 147 ((v0 . v1)(v1 . v0))) ((= (* v0 (R (* v1 v0))) (R v1))))
(149 (instantiate 148 ((v0 . (R v1))(v1 . (* v0 v1)))) ((= (* (R v1) (R (* (* v0 v1) (R v1)))) (R (* v0 v1)))))
(150 (paramod 145 (1 1) 149 (1 1 2 1)) ((= (* (R v1) (R v0)) (R (* v0 v1)))))
(151 (flip 150 (1)) ((= (R (* v0 v1)) (* (R v1) (R v0)))))
(152 (instantiate 151 ((v0 . v2)(v1 . (R v0)))) ((= (R (* v2 (R v0))) (* (R (R v0)) (R v2)))))
(153 (paramod 152 (1 1) 139 (1 1 1 2 2)) ((= (* (* v0 (* v1 (* (R (R v0)) (R v2)))) v2) (* v0 (* v1 v0)))))
(154 (paramod 67 (1 1) 153 (1 1 1 2 2 1)) ((= (* (* v0 (* v1 (* v0 (R v2)))) v2) (* v0 (* v1 v0)))))
(155 (instantiate 154 ((v2 . (R v65)))) ((= (* (* v0 (* v1 (* v0 (R (R v65))))) (R v65)) (* v0 (* v1 v0)))))
(156 (instantiate 142 ((v0 . (* v0 (* v1 (* v0 (R (R v65))))))(v1 . v65))) ((= (* (* (* v0 (* v1 (* v0 (R (R v65))))) (R v65)) v65) (* v0 (* v1 (* v0 (R (R v65))))))))
(157 (paramod 155 (1 1) 156 (1 1 1)) ((= (* (* v0 (* v1 v0)) v65) (* v0 (* v1 (* v0 (R (R v65))))))))
(158 (instantiate 67 ((v0 . v65))) ((= (R (R v65)) v65)))
(159 (paramod 158 (1 1) 157 (1 2 2 2 2)) ((= (* (* v0 (* v1 v0)) v65) (* v0 (* v1 (* v0 v65))))))
(160 (instantiate 159 ((v65 . v2))) ((= (* (* v0 (* v1 v0)) v2) (* v0 (* v1 (* v0 v2))))))
(161 (instantiate 160 ((v0 . v64)(v2 . (* v66 v64)))) ((= (* (* v64 (* v1 v64)) (* v66 v64)) (* v64 (* v1 (* v64 (* v66 v64)))))))
(162 (instantiate 128 ((v0 . v64)(v1 . (* v1 v64))(v2 . v66))) ((= (* (R v64) (* (* v64 (* v1 v64)) (* v66 v64))) (* (* (* v1 v64) v66) v64))))
(163 (paramod 161 (1 1) 162 (1 1 2)) ((= (* (R v64) (* v64 (* v1 (* v64 (* v66 v64))))) (* (* (* v1 v64) v66) v64))))
(164 (instantiate 130 ((v0 . v64)(v1 . (* v1 (* v64 (* v66 v64)))))) ((= (* (R v64) (* v64 (* v1 (* v64 (* v66 v64))))) (* v1 (* v64 (* v66 v64))))))
(165 (paramod 164 (1 1) 163 (1 1)) ((= (* v1 (* v64 (* v66 v64))) (* (* (* v1 v64) v66) v64))))
(166 (flip 165 (1)) ((= (* (* (* v1 v64) v66) v64) (* v1 (* v64 (* v66 v64))))))
(167 (instantiate 166 ((v1 . v0)(v64 . v1)(v66 . v2))) ((= (* (* (* v0 v1) v2) v1) (* v0 (* v1 (* v2 v1))))))
(168 (instantiate 167 ((v0 . (A))(v1 . (B))(v2 . (C)))) ((= (* (* (* (A) (B)) (C)) (B)) (* (A) (* (B) (* (C) (B)))))))
(169 (resolve 9 (1) 168 (1)) ())
)