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