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