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