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