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