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