;; ----- Otter 3.0.4, August 1995 -----
;; The job was started by mccune on gyro, Thu Nov  2 00:26:07 1995
;;
;;;;  -> x=x.
;;;; z1*x=u, z2*y=u, z1*z=w, z3*y=w -> z2*z=z3*x.
;;;;  -> x*x=x.
;;;;  -> x*y=y*x.
;;;;  -> (x*y)*z=x* (y*z).
;;;; B=A -> .
;;
;; ----> UNIT CONFLICT at   0.41 sec ----> 45 [binary,44.1,8.1]  -> .
;;
(
(1 (input) ((= v0 v0)))
(2 (input) ((not (= (* v0 v1) v2)) (not (= (* v3 v4) v2)) (not (= (* v0 v5) v6)) (not (= (* v7 v4) v6)) (= (* v3 v5) (* v7 v1))))
(3 (input) ((= (* v0 v0) v0)))
(4 (input) ((= (* v0 v1) (* v1 v0))))
(5 (input) ((= (* (* v0 v1) v2) (* v0 (* v1 v2)))))
(6 (input) ((not (= (B) (A)))))
(7 (instantiate 2 ((v0 . (* v64 v65))(v1 . v66)(v2 . (* v64 (* v65 v66))))) ((not (= (* (* v64 v65) v66) (* v64 (* v65 v66)))) (not (= (* v3 v4) (* v64 (* v65 v66)))) (not (= (* (* v64 v65) v5) v6)) (not (= (* v7 v4) v6)) (= (* v3 v5) (* v7 v66))))
(8 (instantiate 5 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (* (* v64 v65) v66) (* v64 (* v65 v66)))))
(9 (resolve 7 (1) 8 (1)) ((not (= (* v3 v4) (* v64 (* v65 v66)))) (not (= (* (* v64 v65) v5) v6)) (not (= (* v7 v4) v6)) (= (* v3 v5) (* v7 v66))))
(10 (instantiate 9 ((v3 . v0)(v4 . v1)(v64 . v2)(v65 . v3)(v66 . v4))) ((not (= (* v0 v1) (* v2 (* v3 v4)))) (not (= (* (* v2 v3) v5) v6)) (not (= (* v7 v1) v6)) (= (* v0 v5) (* v7 v4))))
(11 (instantiate 10 ((v0 . (* v2 (* v3 v4)))(v1 . (* v2 (* v3 v4))))) ((not (= (* (* v2 (* v3 v4)) (* v2 (* v3 v4))) (* v2 (* v3 v4)))) (not (= (* (* v2 v3) v5) v6)) (not (= (* v7 (* v2 (* v3 v4))) v6)) (= (* (* v2 (* v3 v4)) v5) (* v7 v4))))
(12 (instantiate 3 ((v0 . (* v2 (* v3 v4))))) ((= (* (* v2 (* v3 v4)) (* v2 (* v3 v4))) (* v2 (* v3 v4)))))
(13 (resolve 11 (1) 12 (1)) ((not (= (* (* v2 v3) v5) v6)) (not (= (* v7 (* v2 (* v3 v4))) v6)) (= (* (* v2 (* v3 v4)) v5) (* v7 v4))))
(14 (instantiate 13 ((v2 . v0)(v3 . v1)(v4 . v5)(v5 . v2)(v6 . v3)(v7 . v4))) ((not (= (* (* v0 v1) v2) v3)) (not (= (* v4 (* v0 (* v1 v5))) v3)) (= (* (* v0 (* v1 v5)) v2) (* v4 v5))))
(15 (instantiate 14 ((v0 . v64)(v1 . v65)(v2 . v66)(v3 . (* v64 (* v65 v66))))) ((not (= (* (* v64 v65) v66) (* v64 (* v65 v66)))) (not (= (* v4 (* v64 (* v65 v5))) (* v64 (* v65 v66)))) (= (* (* v64 (* v65 v5)) v66) (* v4 v5))))
(16 (instantiate 5 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (* (* v64 v65) v66) (* v64 (* v65 v66)))))
(17 (resolve 15 (1) 16 (1)) ((not (= (* v4 (* v64 (* v65 v5))) (* v64 (* v65 v66)))) (= (* (* v64 (* v65 v5)) v66) (* v4 v5))))
(18 (instantiate 17 ((v4 . v0)(v5 . v3)(v64 . v1)(v65 . v2)(v66 . v4))) ((not (= (* v0 (* v1 (* v2 v3))) (* v1 (* v2 v4)))) (= (* (* v1 (* v2 v3)) v4) (* v0 v3))))
(19 (instantiate 18 ((v1 . v0)(v2 . v0)(v4 . (* v0 v3)))) ((not (= (* v0 (* v0 (* v0 v3))) (* v0 (* v0 (* v0 v3))))) (= (* (* v0 (* v0 v3)) (* v0 v3)) (* v0 v3))))
(20 (instantiate 1 ((v0 . (* v0 (* v0 (* v0 v3)))))) ((= (* v0 (* v0 (* v0 v3))) (* v0 (* v0 (* v0 v3))))))
(21 (resolve 19 (1) 20 (1)) ((= (* (* v0 (* v0 v3)) (* v0 v3)) (* v0 v3))))
(22 (instantiate 21 ((v3 . v1))) ((= (* (* v0 (* v0 v1)) (* v0 v1)) (* v0 v1))))
(23 (instantiate 5 ((v0 . v0)(v1 . (* v0 v1))(v2 . (* v0 v1)))) ((= (* (* v0 (* v0 v1)) (* v0 v1)) (* v0 (* (* v0 v1) (* v0 v1))))))
(24 (paramod 23 (1 1) 22 (1 1)) ((= (* v0 (* (* v0 v1) (* v0 v1))) (* v0 v1))))
(25 (instantiate 3 ((v0 . (* v0 v1)))) ((= (* (* v0 v1) (* v0 v1)) (* v0 v1))))
(26 (paramod 25 (1 1) 24 (1 1 2)) ((= (* v0 (* v0 v1)) (* v0 v1))))
(27 (instantiate 2 ((v0 . v64)(v1 . v65)(v2 . (* v65 v64)))) ((not (= (* v64 v65) (* v65 v64))) (not (= (* v3 v4) (* v65 v64))) (not (= (* v64 v5) v6)) (not (= (* v7 v4) v6)) (= (* v3 v5) (* v7 v65))))
(28 (instantiate 4 ((v0 . v64)(v1 . v65))) ((= (* v64 v65) (* v65 v64))))
(29 (resolve 27 (1) 28 (1)) ((not (= (* v3 v4) (* v65 v64))) (not (= (* v64 v5) v6)) (not (= (* v7 v4) v6)) (= (* v3 v5) (* v7 v65))))
(30 (instantiate 29 ((v3 . v0)(v4 . v1)(v5 . v4)(v6 . v5)(v7 . v6)(v64 . v3)(v65 . v2))) ((not (= (* v0 v1) (* v2 v3))) (not (= (* v3 v4) v5)) (not (= (* v6 v1) v5)) (= (* v0 v4) (* v6 v2))))
(31 (instantiate 30 ((v0 . (* v2 v3))(v1 . (* v2 v3)))) ((not (= (* (* v2 v3) (* v2 v3)) (* v2 v3))) (not (= (* v3 v4) v5)) (not (= (* v6 (* v2 v3)) v5)) (= (* (* v2 v3) v4) (* v6 v2))))
(32 (instantiate 3 ((v0 . (* v2 v3)))) ((= (* (* v2 v3) (* v2 v3)) (* v2 v3))))
(33 (resolve 31 (1) 32 (1)) ((not (= (* v3 v4) v5)) (not (= (* v6 (* v2 v3)) v5)) (= (* (* v2 v3) v4) (* v6 v2))))
(34 (instantiate 33 ((v2 . v4)(v3 . v0)(v4 . v1)(v5 . v2)(v6 . v3))) ((not (= (* v0 v1) v2)) (not (= (* v3 (* v4 v0)) v2)) (= (* (* v4 v0) v1) (* v3 v4))))
(35 (instantiate 34 ((v0 . (* v64 v65))(v1 . v66)(v2 . (* v64 (* v65 v66))))) ((not (= (* (* v64 v65) v66) (* v64 (* v65 v66)))) (not (= (* v3 (* v4 (* v64 v65))) (* v64 (* v65 v66)))) (= (* (* v4 (* v64 v65)) v66) (* v3 v4))))
(36 (instantiate 5 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (* (* v64 v65) v66) (* v64 (* v65 v66)))))
(37 (resolve 35 (1) 36 (1)) ((not (= (* v3 (* v4 (* v64 v65))) (* v64 (* v65 v66)))) (= (* (* v4 (* v64 v65)) v66) (* v3 v4))))
(38 (instantiate 37 ((v3 . v0)(v4 . v1)(v64 . v2)(v65 . v3)(v66 . v4))) ((not (= (* v0 (* v1 (* v2 v3))) (* v2 (* v3 v4)))) (= (* (* v1 (* v2 v3)) v4) (* v0 v1))))
(39 (instantiate 38 ((v2 . v0)(v3 . v1)(v4 . (* v0 v1)))) ((not (= (* v0 (* v1 (* v0 v1))) (* v0 (* v1 (* v0 v1))))) (= (* (* v1 (* v0 v1)) (* v0 v1)) (* v0 v1))))
(40 (instantiate 1 ((v0 . (* v0 (* v1 (* v0 v1)))))) ((= (* v0 (* v1 (* v0 v1))) (* v0 (* v1 (* v0 v1))))))
(41 (resolve 39 (1) 40 (1)) ((= (* (* v1 (* v0 v1)) (* v0 v1)) (* v0 v1))))
(42 (instantiate 41 ((v0 . v1)(v1 . v0))) ((= (* (* v0 (* v1 v0)) (* v1 v0)) (* v1 v0))))
(43 (instantiate 5 ((v0 . v0)(v1 . (* v1 v0))(v2 . (* v1 v0)))) ((= (* (* v0 (* v1 v0)) (* v1 v0)) (* v0 (* (* v1 v0) (* v1 v0))))))
(44 (paramod 43 (1 1) 42 (1 1)) ((= (* v0 (* (* v1 v0) (* v1 v0))) (* v1 v0))))
(45 (instantiate 3 ((v0 . (* v1 v0)))) ((= (* (* v1 v0) (* v1 v0)) (* v1 v0))))
(46 (paramod 45 (1 1) 44 (1 1 2)) ((= (* v0 (* v1 v0)) (* v1 v0))))
(47 (instantiate 2 ((v0 . v64)(v1 . v65)(v2 . (* v65 v64)))) ((not (= (* v64 v65) (* v65 v64))) (not (= (* v3 v4) (* v65 v64))) (not (= (* v64 v5) v6)) (not (= (* v7 v4) v6)) (= (* v3 v5) (* v7 v65))))
(48 (instantiate 4 ((v0 . v64)(v1 . v65))) ((= (* v64 v65) (* v65 v64))))
(49 (resolve 47 (1) 48 (1)) ((not (= (* v3 v4) (* v65 v64))) (not (= (* v64 v5) v6)) (not (= (* v7 v4) v6)) (= (* v3 v5) (* v7 v65))))
(50 (instantiate 49 ((v3 . v0)(v4 . v1)(v5 . v4)(v6 . v5)(v7 . v6)(v64 . v3)(v65 . v2))) ((not (= (* v0 v1) (* v2 v3))) (not (= (* v3 v4) v5)) (not (= (* v6 v1) v5)) (= (* v0 v4) (* v6 v2))))
(51 (instantiate 50 ((v0 . (* v2 v3))(v1 . (* v2 v3)))) ((not (= (* (* v2 v3) (* v2 v3)) (* v2 v3))) (not (= (* v3 v4) v5)) (not (= (* v6 (* v2 v3)) v5)) (= (* (* v2 v3) v4) (* v6 v2))))
(52 (instantiate 3 ((v0 . (* v2 v3)))) ((= (* (* v2 v3) (* v2 v3)) (* v2 v3))))
(53 (resolve 51 (1) 52 (1)) ((not (= (* v3 v4) v5)) (not (= (* v6 (* v2 v3)) v5)) (= (* (* v2 v3) v4) (* v6 v2))))
(54 (instantiate 53 ((v2 . v4)(v3 . v0)(v4 . v1)(v5 . v2)(v6 . v3))) ((not (= (* v0 v1) v2)) (not (= (* v3 (* v4 v0)) v2)) (= (* (* v4 v0) v1) (* v3 v4))))
(55 (instantiate 54 ((v0 . v64)(v1 . v65)(v2 . (* v65 v64)))) ((not (= (* v64 v65) (* v65 v64))) (not (= (* v3 (* v4 v64)) (* v65 v64))) (= (* (* v4 v64) v65) (* v3 v4))))
(56 (instantiate 4 ((v0 . v64)(v1 . v65))) ((= (* v64 v65) (* v65 v64))))
(57 (resolve 55 (1) 56 (1)) ((not (= (* v3 (* v4 v64)) (* v65 v64))) (= (* (* v4 v64) v65) (* v3 v4))))
(58 (instantiate 57 ((v3 . v0)(v4 . v1)(v64 . v2)(v65 . v3))) ((not (= (* v0 (* v1 v2)) (* v3 v2))) (= (* (* v1 v2) v3) (* v0 v1))))
(59 (instantiate 58 ((v0 . v64)(v1 . v64)(v2 . v65)(v3 . v64))) ((not (= (* v64 (* v64 v65)) (* v64 v65))) (= (* (* v64 v65) v64) (* v64 v64))))
(60 (instantiate 26 ((v0 . v64)(v1 . v65))) ((= (* v64 (* v64 v65)) (* v64 v65))))
(61 (resolve 59 (1) 60 (1)) ((= (* (* v64 v65) v64) (* v64 v64))))
(62 (instantiate 61 ((v64 . v0)(v65 . v1))) ((= (* (* v0 v1) v0) (* v0 v0))))
(63 (instantiate 5 ((v0 . v0)(v1 . v1)(v2 . v0))) ((= (* (* v0 v1) v0) (* v0 (* v1 v0)))))
(64 (paramod 63 (1 1) 62 (1 1)) ((= (* v0 (* v1 v0)) (* v0 v0))))
(65 (paramod 46 (1 1) 64 (1 1)) ((= (* v1 v0) (* v0 v0))))
(66 (paramod 3 (1 1) 65 (1 2)) ((= (* v1 v0) v0)))
(67 (instantiate 66 ((v0 . v1)(v1 . v0))) ((= (* v0 v1) v1)))
(68 (instantiate 2 ((v0 . v64)(v1 . v65)(v2 . (* v65 v64)))) ((not (= (* v64 v65) (* v65 v64))) (not (= (* v3 v4) (* v65 v64))) (not (= (* v64 v5) v6)) (not (= (* v7 v4) v6)) (= (* v3 v5) (* v7 v65))))
(69 (instantiate 4 ((v0 . v64)(v1 . v65))) ((= (* v64 v65) (* v65 v64))))
(70 (resolve 68 (1) 69 (1)) ((not (= (* v3 v4) (* v65 v64))) (not (= (* v64 v5) v6)) (not (= (* v7 v4) v6)) (= (* v3 v5) (* v7 v65))))
(71 (instantiate 70 ((v3 . v0)(v4 . v1)(v5 . v4)(v6 . v5)(v7 . v6)(v64 . v3)(v65 . v2))) ((not (= (* v0 v1) (* v2 v3))) (not (= (* v3 v4) v5)) (not (= (* v6 v1) v5)) (= (* v0 v4) (* v6 v2))))
(72 (instantiate 71 ((v2 . v0)(v3 . v1))) ((not (= (* v0 v1) (* v0 v1))) (not (= (* v1 v4) v5)) (not (= (* v6 v1) v5)) (= (* v0 v4) (* v6 v0))))
(73 (instantiate 1 ((v0 . (* v0 v1)))) ((= (* v0 v1) (* v0 v1))))
(74 (resolve 72 (1) 73 (1)) ((not (= (* v1 v4) v5)) (not (= (* v6 v1) v5)) (= (* v0 v4) (* v6 v0))))
(75 (instantiate 74 ((v0 . v4)(v1 . v0)(v4 . v1)(v5 . v2)(v6 . v3))) ((not (= (* v0 v1) v2)) (not (= (* v3 v0) v2)) (= (* v4 v1) (* v3 v4))))
(76 (instantiate 75 ((v0 . v64)(v1 . v64)(v2 . v64))) ((not (= (* v64 v64) v64)) (not (= (* v3 v64) v64)) (= (* v4 v64) (* v3 v4))))
(77 (instantiate 3 ((v0 . v64))) ((= (* v64 v64) v64)))
(78 (resolve 76 (1) 77 (1)) ((not (= (* v3 v64) v64)) (= (* v4 v64) (* v3 v4))))
(79 (instantiate 78 ((v3 . v0)(v4 . v2)(v64 . v1))) ((not (= (* v0 v1) v1)) (= (* v2 v1) (* v0 v2))))
(80 (instantiate 79 ((v0 . v64)(v1 . (* v64 v65)))) ((not (= (* v64 (* v64 v65)) (* v64 v65))) (= (* v2 (* v64 v65)) (* v64 v2))))
(81 (instantiate 26 ((v0 . v64)(v1 . v65))) ((= (* v64 (* v64 v65)) (* v64 v65))))
(82 (resolve 80 (1) 81 (1)) ((= (* v2 (* v64 v65)) (* v64 v2))))
(83 (instantiate 82 ((v2 . v0)(v64 . v1)(v65 . v2))) ((= (* v0 (* v1 v2)) (* v1 v0))))
(84 (instantiate 67 ((v0 . v1)(v1 . v2))) ((= (* v1 v2) v2)))
(85 (paramod 84 (1 1) 83 (1 1 2)) ((= (* v0 v2) (* v1 v0))))
(86 (instantiate 67 ((v0 . v0)(v1 . v2))) ((= (* v0 v2) v2)))
(87 (paramod 86 (1 1) 85 (1 1)) ((= v2 (* v1 v0))))
(88 (instantiate 67 ((v0 . v1)(v1 . v0))) ((= (* v1 v0) v0)))
(89 (paramod 88 (1 1) 87 (1 2)) ((= v2 v0)))
(90 (instantiate 89 ((v0 . v1)(v2 . v0))) ((= v0 v1)))
(91 (instantiate 90 ((v0 . (B))(v1 . (A)))) ((= (B) (A))))
(92 (resolve 6 (1) 91 (1)) ())
)