;; ----- Otter 3.0.4, August 1995 -----
;; The job was started by mccune on gyro, Wed Nov  1 21:58:35 1995
;;
;;;;  -> x=x.
;;;; B*B@ =A*A@ , A* (B*B@ )=A, (A*B)*C=A* (B*C) -> .
;;;;  -> ((x*y)* (alpha*z))* (y* (alpha*z))@ =x.
;;;;  -> ((x*beta)*y)@ * ((x*beta)* (y*z))=z.
;;
;; ----> UNIT CONFLICT at   2.62 sec ----> 676 [binary,675.1,634.1]  -> .
;;
(
(1 (input) ((= v0 v0)))
(2 (input) ((not (= (* (B) (@ (B))) (* (A) (@ (A))))) (not (= (* (A) (* (B) (@ (B)))) (A))) (not (= (* (* (A) (B)) (C)) (* (A) (* (B) (C)))))))
(3 (input) ((= (* (* (* v0 v1) (* (alpha) v2)) (@ (* v1 (* (alpha) v2)))) v0)))
(4 (input) ((= (* (@ (* (* v0 (beta)) v1)) (* (* v0 (beta)) (* v1 v2))) v2)))
(5 (instantiate 3 ((v0 . (* (* v0 v1) (* (alpha) v2)))(v1 . (@ (* v1 (* (alpha) v2))))(v2 . v66))) ((= (* (* (* (* (* v0 v1) (* (alpha) v2)) (@ (* v1 (* (alpha) v2)))) (* (alpha) v66)) (@ (* (@ (* v1 (* (alpha) v2))) (* (alpha) v66)))) (* (* v0 v1) (* (alpha) v2)))))
(6 (paramod 3 (1 1) 5 (1 1 1 1)) ((= (* (* v0 (* (alpha) v66)) (@ (* (@ (* v1 (* (alpha) v2))) (* (alpha) v66)))) (* (* v0 v1) (* (alpha) v2)))))
(7 (instantiate 6 ((v1 . v2)(v2 . v3)(v66 . v1))) ((= (* (* v0 (* (alpha) v1)) (@ (* (@ (* v2 (* (alpha) v3))) (* (alpha) v1)))) (* (* v0 v2) (* (alpha) v3)))))
(8 (instantiate 3 ((v1 . (@ (* v66 (* (alpha) v67))))(v2 . v65))) ((= (* (* (* v0 (@ (* v66 (* (alpha) v67)))) (* (alpha) v65)) (@ (* (@ (* v66 (* (alpha) v67))) (* (alpha) v65)))) v0)))
(9 (instantiate 7 ((v0 . (* v0 (@ (* v66 (* (alpha) v67)))))(v1 . v65)(v2 . v66)(v3 . v67))) ((= (* (* (* v0 (@ (* v66 (* (alpha) v67)))) (* (alpha) v65)) (@ (* (@ (* v66 (* (alpha) v67))) (* (alpha) v65)))) (* (* (* v0 (@ (* v66 (* (alpha) v67)))) v66) (* (alpha) v67)))))
(10 (paramod 8 (1 1) 9 (1 1)) ((= v0 (* (* (* v0 (@ (* v66 (* (alpha) v67)))) v66) (* (alpha) v67)))))
(11 (flip 10 (1)) ((= (* (* (* v0 (@ (* v66 (* (alpha) v67)))) v66) (* (alpha) v67)) v0)))
(12 (instantiate 11 ((v66 . v1)(v67 . v2))) ((= (* (* (* v0 (@ (* v1 (* (alpha) v2)))) v1) (* (alpha) v2)) v0)))
(13 (instantiate 12 ((v1 . (beta))(v2 . v66))) ((= (* (* (* v0 (@ (* (beta) (* (alpha) v66)))) (beta)) (* (alpha) v66)) v0)))
(14 (instantiate 4 ((v0 . (* v0 (@ (* (beta) (* (alpha) v66)))))(v1 . (alpha))(v2 . v66))) ((= (* (@ (* (* (* v0 (@ (* (beta) (* (alpha) v66)))) (beta)) (alpha))) (* (* (* v0 (@ (* (beta) (* (alpha) v66)))) (beta)) (* (alpha) v66))) v66)))
(15 (paramod 13 (1 1) 14 (1 1 2)) ((= (* (@ (* (* (* v0 (@ (* (beta) (* (alpha) v66)))) (beta)) (alpha))) v0) v66)))
(16 (instantiate 15 ((v66 . v1))) ((= (* (@ (* (* (* v0 (@ (* (beta) (* (alpha) v1)))) (beta)) (alpha))) v0) v1)))
(17 (instantiate 16 ((v0 . (beta)))) ((= (* (@ (* (* (* (beta) (@ (* (beta) (* (alpha) v1)))) (beta)) (alpha))) (beta)) v1)))
(18 (instantiate 4 ((v0 . (@ (* (* (* (beta) (@ (* (beta) (* (alpha) v1)))) (beta)) (alpha))))(v1 . v65)(v2 . v66))) ((= (* (@ (* (* (@ (* (* (* (beta) (@ (* (beta) (* (alpha) v1)))) (beta)) (alpha))) (beta)) v65)) (* (* (@ (* (* (* (beta) (@ (* (beta) (* (alpha) v1)))) (beta)) (alpha))) (beta)) (* v65 v66))) v66)))
(19 (paramod 17 (1 1) 18 (1 1 2 1)) ((= (* (@ (* (* (@ (* (* (* (beta) (@ (* (beta) (* (alpha) v1)))) (beta)) (alpha))) (beta)) v65)) (* v1 (* v65 v66))) v66)))
(20 (instantiate 16 ((v0 . (beta))(v1 . v1))) ((= (* (@ (* (* (* (beta) (@ (* (beta) (* (alpha) v1)))) (beta)) (alpha))) (beta)) v1)))
(21 (paramod 20 (1 1) 19 (1 1 1 1 1)) ((= (* (@ (* v1 v65)) (* v1 (* v65 v66))) v66)))
(22 (instantiate 21 ((v1 . v0)(v65 . v1)(v66 . v2))) ((= (* (@ (* v0 v1)) (* v0 (* v1 v2))) v2)))
(23 (instantiate 22 ((v0 . v65))) ((= (* (@ (* v65 v1)) (* v65 (* v1 v2))) v2)))
(24 (instantiate 22 ((v0 . (@ (* v65 v1)))(v1 . v65)(v2 . (* v1 v2)))) ((= (* (@ (* (@ (* v65 v1)) v65)) (* (@ (* v65 v1)) (* v65 (* v1 v2)))) (* v1 v2))))
(25 (paramod 23 (1 1) 24 (1 1 2)) ((= (* (@ (* (@ (* v65 v1)) v65)) v2) (* v1 v2))))
(26 (instantiate 25 ((v65 . v0))) ((= (* (@ (* (@ (* v0 v1)) v0)) v2) (* v1 v2))))
(27 (instantiate 22 ((v0 . (@ (* v64 v65)))(v1 . v64))) ((= (* (@ (* (@ (* v64 v65)) v64)) (* (@ (* v64 v65)) (* v64 v2))) v2)))
(28 (instantiate 26 ((v0 . v64)(v1 . v65)(v2 . (* (@ (* v64 v65)) (* v64 v2))))) ((= (* (@ (* (@ (* v64 v65)) v64)) (* (@ (* v64 v65)) (* v64 v2))) (* v65 (* (@ (* v64 v65)) (* v64 v2))))))
(29 (paramod 27 (1 1) 28 (1 1)) ((= v2 (* v65 (* (@ (* v64 v65)) (* v64 v2))))))
(30 (flip 29 (1)) ((= (* v65 (* (@ (* v64 v65)) (* v64 v2))) v2)))
(31 (instantiate 30 ((v64 . v1)(v65 . v0))) ((= (* v0 (* (@ (* v1 v0)) (* v1 v2))) v2)))
(32 (instantiate 26 ((v2 . (@ (* v65 (* (alpha) v66)))))) ((= (* (@ (* (@ (* v0 v1)) v0)) (@ (* v65 (* (alpha) v66)))) (* v1 (@ (* v65 (* (alpha) v66)))))))
(33 (instantiate 12 ((v0 . (@ (* (@ (* v0 v1)) v0)))(v1 . v65)(v2 . v66))) ((= (* (* (* (@ (* (@ (* v0 v1)) v0)) (@ (* v65 (* (alpha) v66)))) v65) (* (alpha) v66)) (@ (* (@ (* v0 v1)) v0)))))
(34 (paramod 32 (1 1) 33 (1 1 1 1)) ((= (* (* (* v1 (@ (* v65 (* (alpha) v66)))) v65) (* (alpha) v66)) (@ (* (@ (* v0 v1)) v0)))))
(35 (instantiate 12 ((v0 . v1)(v1 . v65)(v2 . v66))) ((= (* (* (* v1 (@ (* v65 (* (alpha) v66)))) v65) (* (alpha) v66)) v1)))
(36 (paramod 35 (1 1) 34 (1 1)) ((= v1 (@ (* (@ (* v0 v1)) v0)))))
(37 (flip 36 (1)) ((= (@ (* (@ (* v0 v1)) v0)) v1)))
(38 (instantiate 37 ((v0 . (@ (* v0 v1)))(v1 . (* v0 (* v1 v2))))) ((= (@ (* (@ (* (@ (* v0 v1)) (* v0 (* v1 v2)))) (@ (* v0 v1)))) (* v0 (* v1 v2)))))
(39 (paramod 22 (1 1) 38 (1 1 1 1 1)) ((= (@ (* (@ v2) (@ (* v0 v1)))) (* v0 (* v1 v2)))))
(40 (instantiate 39 ((v0 . v1)(v1 . v2)(v2 . v0))) ((= (@ (* (@ v0) (@ (* v1 v2)))) (* v1 (* v2 v0)))))
(41 (instantiate 37 ((v0 . v65))) ((= (@ (* (@ (* v65 v1)) v65)) v1)))
(42 (instantiate 37 ((v0 . (@ (* v65 v1)))(v1 . v65))) ((= (@ (* (@ (* (@ (* v65 v1)) v65)) (@ (* v65 v1)))) v65)))
(43 (paramod 41 (1 1) 42 (1 1 1 1)) ((= (@ (* v1 (@ (* v65 v1)))) v65)))
(44 (instantiate 43 ((v1 . v0)(v65 . v1))) ((= (@ (* v0 (@ (* v1 v0)))) v1)))
(45 (instantiate 44 ((v0 . v64))) ((= (@ (* v64 (@ (* v1 v64)))) v1)))
(46 (instantiate 22 ((v0 . v64)(v1 . (@ (* v1 v64)))(v2 . v66))) ((= (* (@ (* v64 (@ (* v1 v64)))) (* v64 (* (@ (* v1 v64)) v66))) v66)))
(47 (paramod 45 (1 1) 46 (1 1 1)) ((= (* v1 (* v64 (* (@ (* v1 v64)) v66))) v66)))
(48 (instantiate 47 ((v1 . v0)(v64 . v1)(v66 . v2))) ((= (* v0 (* v1 (* (@ (* v0 v1)) v2))) v2)))
(49 (instantiate 31 ((v0 . (alpha)))) ((= (* (alpha) (* (@ (* v1 (alpha))) (* v1 v2))) v2)))
(50 (instantiate 12 ((v0 . v64)(v1 . v65)(v2 . (* (@ (* v1 (alpha))) (* v1 v2))))) ((= (* (* (* v64 (@ (* v65 (* (alpha) (* (@ (* v1 (alpha))) (* v1 v2)))))) v65) (* (alpha) (* (@ (* v1 (alpha))) (* v1 v2)))) v64)))
(51 (paramod 49 (1 1) 50 (1 1 2)) ((= (* (* (* v64 (@ (* v65 (* (alpha) (* (@ (* v1 (alpha))) (* v1 v2)))))) v65) v2) v64)))
(52 (instantiate 31 ((v0 . (alpha))(v1 . v1)(v2 . v2))) ((= (* (alpha) (* (@ (* v1 (alpha))) (* v1 v2))) v2)))
(53 (paramod 52 (1 1) 51 (1 1 1 1 2 1 2)) ((= (* (* (* v64 (@ (* v65 v2))) v65) v2) v64)))
(54 (instantiate 53 ((v64 . v0)(v65 . v1))) ((= (* (* (* v0 (@ (* v1 v2))) v1) v2) v0)))
(55 (instantiate 31 ((v0 . (alpha)))) ((= (* (alpha) (* (@ (* v1 (alpha))) (* v1 v2))) v2)))
(56 (instantiate 3 ((v0 . v64)(v1 . v65)(v2 . (* (@ (* v1 (alpha))) (* v1 v2))))) ((= (* (* (* v64 v65) (* (alpha) (* (@ (* v1 (alpha))) (* v1 v2)))) (@ (* v65 (* (alpha) (* (@ (* v1 (alpha))) (* v1 v2)))))) v64)))
(57 (paramod 55 (1 1) 56 (1 1 2 1 2)) ((= (* (* (* v64 v65) (* (alpha) (* (@ (* v1 (alpha))) (* v1 v2)))) (@ (* v65 v2))) v64)))
(58 (instantiate 31 ((v0 . (alpha))(v1 . v1)(v2 . v2))) ((= (* (alpha) (* (@ (* v1 (alpha))) (* v1 v2))) v2)))
(59 (paramod 58 (1 1) 57 (1 1 1 2)) ((= (* (* (* v64 v65) v2) (@ (* v65 v2))) v64)))
(60 (instantiate 59 ((v64 . v0)(v65 . v1))) ((= (* (* (* v0 v1) v2) (@ (* v1 v2))) v0)))
(61 (instantiate 37 ((v0 . v66))) ((= (@ (* (@ (* v66 v1)) v66)) v1)))
(62 (instantiate 54 ((v0 . v64)(v1 . (@ (* v66 v1)))(v2 . v66))) ((= (* (* (* v64 (@ (* (@ (* v66 v1)) v66))) (@ (* v66 v1))) v66) v64)))
(63 (paramod 61 (1 1) 62 (1 1 1 1 2)) ((= (* (* (* v64 v1) (@ (* v66 v1))) v66) v64)))
(64 (instantiate 63 ((v64 . v0)(v66 . v2))) ((= (* (* (* v0 v1) (@ (* v2 v1))) v2) v0)))
(65 (instantiate 64 ((v2 . v65))) ((= (* (* (* v0 v1) (@ (* v65 v1))) v65) v0)))
(66 (instantiate 22 ((v0 . (* (* v0 v1) (@ (* v65 v1))))(v1 . v65)(v2 . v66))) ((= (* (@ (* (* (* v0 v1) (@ (* v65 v1))) v65)) (* (* (* v0 v1) (@ (* v65 v1))) (* v65 v66))) v66)))
(67 (paramod 65 (1 1) 66 (1 1 1 1)) ((= (* (@ v0) (* (* (* v0 v1) (@ (* v65 v1))) (* v65 v66))) v66)))
(68 (instantiate 67 ((v65 . v2)(v66 . v3))) ((= (* (@ v0) (* (* (* v0 v1) (@ (* v2 v1))) (* v2 v3))) v3)))
(69 (instantiate 44 ((v0 . (@ v64))(v1 . v65))) ((= (@ (* (@ v64) (@ (* v65 (@ v64))))) v65)))
(70 (instantiate 40 ((v0 . v64)(v1 . v65)(v2 . (@ v64)))) ((= (@ (* (@ v64) (@ (* v65 (@ v64))))) (* v65 (* (@ v64) v64)))))
(71 (paramod 69 (1 1) 70 (1 1)) ((= v65 (* v65 (* (@ v64) v64)))))
(72 (flip 71 (1)) ((= (* v65 (* (@ v64) v64)) v65)))
(73 (instantiate 72 ((v64 . v1)(v65 . v0))) ((= (* v0 (* (@ v1) v1)) v0)))
(74 (instantiate 54 ((v2 . (* (@ v65) v65)))) ((= (* (* (* v0 (@ (* v1 (* (@ v65) v65)))) v1) (* (@ v65) v65)) v0)))
(75 (instantiate 73 ((v0 . (* (* v0 (@ (* v1 (* (@ v65) v65)))) v1))(v1 . v65))) ((= (* (* (* v0 (@ (* v1 (* (@ v65) v65)))) v1) (* (@ v65) v65)) (* (* v0 (@ (* v1 (* (@ v65) v65)))) v1))))
(76 (paramod 74 (1 1) 75 (1 1)) ((= v0 (* (* v0 (@ (* v1 (* (@ v65) v65)))) v1))))
(77 (instantiate 73 ((v0 . v1)(v1 . v65))) ((= (* v1 (* (@ v65) v65)) v1)))
(78 (paramod 77 (1 1) 76 (1 2 1 2 1)) ((= v0 (* (* v0 (@ v1)) v1))))
(79 (flip 78 (1)) ((= (* (* v0 (@ v1)) v1) v0)))
(80 (instantiate 73 ((v0 . v65))) ((= (* v65 (* (@ v1) v1)) v65)))
(81 (instantiate 44 ((v0 . (* (@ v1) v1))(v1 . v65))) ((= (@ (* (* (@ v1) v1) (@ (* v65 (* (@ v1) v1))))) v65)))
(82 (paramod 80 (1 1) 81 (1 1 1 2 1)) ((= (@ (* (* (@ v1) v1) (@ v65))) v65)))
(83 (instantiate 82 ((v1 . v0)(v65 . v1))) ((= (@ (* (* (@ v0) v0) (@ v1))) v1)))
(84 (instantiate 73 ((v0 . (* v64 v65)))) ((= (* (* v64 v65) (* (@ v1) v1)) (* v64 v65))))
(85 (instantiate 60 ((v0 . v64)(v1 . v65)(v2 . (* (@ v1) v1)))) ((= (* (* (* v64 v65) (* (@ v1) v1)) (@ (* v65 (* (@ v1) v1)))) v64)))
(86 (paramod 84 (1 1) 85 (1 1 1)) ((= (* (* v64 v65) (@ (* v65 (* (@ v1) v1)))) v64)))
(87 (instantiate 73 ((v0 . v65)(v1 . v1))) ((= (* v65 (* (@ v1) v1)) v65)))
(88 (paramod 87 (1 1) 86 (1 1 2 1)) ((= (* (* v64 v65) (@ v65)) v64)))
(89 (instantiate 88 ((v64 . v0)(v65 . v1))) ((= (* (* v0 v1) (@ v1)) v0)))
(90 (instantiate 79 ((v0 . (* (* v0 v1) v2))(v1 . (* v1 v2)))) ((= (* (* (* (* v0 v1) v2) (@ (* v1 v2))) (* v1 v2)) (* (* v0 v1) v2))))
(91 (paramod 60 (1 1) 90 (1 1 1)) ((= (* v0 (* v1 v2)) (* (* v0 v1) v2))))
(92 (flip 91 (1)) ((= (* (* v0 v1) v2) (* v0 (* v1 v2)))))
(93 (instantiate 92 ((v0 . v0)(v1 . v1)(v2 . (@ v1)))) ((= (* (* v0 v1) (@ v1)) (* v0 (* v1 (@ v1))))))
(94 (paramod 93 (1 1) 89 (1 1)) ((= (* v0 (* v1 (@ v1))) v0)))
(95 (instantiate 92 ((v0 . (@ v0))(v1 . v0)(v2 . (@ v1)))) ((= (* (* (@ v0) v0) (@ v1)) (* (@ v0) (* v0 (@ v1))))))
(96 (paramod 95 (1 1) 83 (1 1 1)) ((= (@ (* (@ v0) (* v0 (@ v1)))) v1)))
(97 (instantiate 92 ((v0 . v0)(v1 . v1)(v2 . (@ (* v2 v1))))) ((= (* (* v0 v1) (@ (* v2 v1))) (* v0 (* v1 (@ (* v2 v1)))))))
(98 (paramod 97 (1 1) 68 (1 1 2 1)) ((= (* (@ v0) (* (* v0 (* v1 (@ (* v2 v1)))) (* v2 v3))) v3)))
(99 (instantiate 92 ((v0 . v0)(v1 . (* v1 (@ (* v2 v1))))(v2 . (* v2 v3)))) ((= (* (* v0 (* v1 (@ (* v2 v1)))) (* v2 v3)) (* v0 (* (* v1 (@ (* v2 v1))) (* v2 v3))))))
(100 (paramod 99 (1 1) 98 (1 1 2)) ((= (* (@ v0) (* v0 (* (* v1 (@ (* v2 v1))) (* v2 v3)))) v3)))
(101 (instantiate 92 ((v0 . v1)(v1 . (@ (* v2 v1)))(v2 . (* v2 v3)))) ((= (* (* v1 (@ (* v2 v1))) (* v2 v3)) (* v1 (* (@ (* v2 v1)) (* v2 v3))))))
(102 (paramod 101 (1 1) 100 (1 1 2 2)) ((= (* (@ v0) (* v0 (* v1 (* (@ (* v2 v1)) (* v2 v3))))) v3)))
(103 (instantiate 31 ((v0 . v1)(v1 . v2)(v2 . v3))) ((= (* v1 (* (@ (* v2 v1)) (* v2 v3))) v3)))
(104 (paramod 103 (1 1) 102 (1 1 2 2)) ((= (* (@ v0) (* v0 v3)) v3)))
(105 (instantiate 104 ((v3 . v1))) ((= (* (@ v0) (* v0 v1)) v1)))
(106 (instantiate 94 ((v0 . (A))(v1 . (B)))) ((= (* (A) (* (B) (@ (B)))) (A))))
(107 (paramod 106 (1 1) 2 (2 1 1)) ((not (= (* (B) (@ (B))) (* (A) (@ (A))))) (not (= (A) (A))) (not (= (* (* (A) (B)) (C)) (* (A) (* (B) (C)))))))
(108 (instantiate 92 ((v0 . (A))(v1 . (B))(v2 . (C)))) ((= (* (* (A) (B)) (C)) (* (A) (* (B) (C))))))
(109 (paramod 108 (1 1) 107 (3 1 1)) ((not (= (* (B) (@ (B))) (* (A) (@ (A))))) (not (= (A) (A))) (not (= (* (A) (* (B) (C))) (* (A) (* (B) (C)))))))
(110 (instantiate 1 ((v0 . (A)))) ((= (A) (A))))
(111 (resolve 109 (2) 110 (1)) ((not (= (* (B) (@ (B))) (* (A) (@ (A))))) (not (= (* (A) (* (B) (C))) (* (A) (* (B) (C)))))))
(112 (instantiate 1 ((v0 . (* (A) (* (B) (C)))))) ((= (* (A) (* (B) (C))) (* (A) (* (B) (C))))))
(113 (resolve 111 (2) 112 (1)) ((not (= (* (B) (@ (B))) (* (A) (@ (A)))))))
(114 (instantiate 105 ((v0 . v0)(v1 . (@ v1)))) ((= (* (@ v0) (* v0 (@ v1))) (@ v1))))
(115 (paramod 114 (1 1) 96 (1 1 1)) ((= (@ (@ v1)) v1)))
(116 (instantiate 115 ((v1 . v0))) ((= (@ (@ v0)) v0)))
(117 (instantiate 116 ((v0 . (* v0 (@ (* v1 v0)))))) ((= (@ (@ (* v0 (@ (* v1 v0))))) (* v0 (@ (* v1 v0))))))
(118 (paramod 44 (1 1) 117 (1 1 1)) ((= (@ v1) (* v0 (@ (* v1 v0))))))
(119 (flip 118 (1)) ((= (* v0 (@ (* v1 v0))) (@ v1))))
(120 (instantiate 94 ((v0 . (@ (* v64 v65))))) ((= (* (@ (* v64 v65)) (* v1 (@ v1))) (@ (* v64 v65)))))
(121 (instantiate 48 ((v0 . v64)(v1 . v65)(v2 . (* v1 (@ v1))))) ((= (* v64 (* v65 (* (@ (* v64 v65)) (* v1 (@ v1))))) (* v1 (@ v1)))))
(122 (paramod 120 (1 1) 121 (1 1 2 2)) ((= (* v64 (* v65 (@ (* v64 v65)))) (* v1 (@ v1)))))
(123 (instantiate 119 ((v0 . v65)(v1 . v64))) ((= (* v65 (@ (* v64 v65))) (@ v64))))
(124 (paramod 123 (1 1) 122 (1 1 2)) ((= (* v64 (@ v64)) (* v1 (@ v1)))))
(125 (instantiate 124 ((v64 . v0))) ((= (* v0 (@ v0)) (* v1 (@ v1)))))
(126 (instantiate 125 ((v0 . (B))(v1 . (A)))) ((= (* (B) (@ (B))) (* (A) (@ (A))))))
(127 (resolve 113 (1) 126 (1)) ())
)