;; ----- Otter 3.0.4, August 1995 -----
;; The job was started by mccune on gyro, Thu Nov  2 00:23:11 1995
;;
;;;;  -> x=x.
;;;; z1*x=u, z2*y=u, z1*z=w, z3*y=w -> z2*z=z3*x.
;;;;  -> (x*e)*e=x.
;;;;  -> e* (e*x)=x.
;;;;  -> C4*A=C3*B.
;;;;  -> C2*A=C1*B.
;;;;  -> C4*F=C3*E.
;;;; C2*F=C1*E -> .
;;
;; ----> UNIT CONFLICT at  55.76 sec ----> 72 [binary,70.1,13.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 (e)) (e)) v0)))
(4 (input) ((= (* (e) (* (e) v0)) v0)))
(5 (input) ((= (* (C4) (A)) (* (C3) (B)))))
(6 (input) ((= (* (C2) (A)) (* (C1) (B)))))
(7 (input) ((= (* (C4) (F)) (* (C3) (E)))))
(8 (input) ((not (= (* (C2) (F)) (* (C1) (E))))))
(9 (instantiate 2 ((v2 . (* v0 v1)))) ((not (= (* v0 v1) (* v0 v1))) (not (= (* v3 v4) (* v0 v1))) (not (= (* v0 v5) v6)) (not (= (* v7 v4) v6)) (= (* v3 v5) (* v7 v1))))
(10 (instantiate 1 ((v0 . (* v0 v1)))) ((= (* v0 v1) (* v0 v1))))
(11 (resolve 9 (1) 10 (1)) ((not (= (* v3 v4) (* v0 v1))) (not (= (* v0 v5) v6)) (not (= (* v7 v4) v6)) (= (* v3 v5) (* v7 v1))))
(12 (instantiate 11 ((v0 . v2)(v1 . v3)(v3 . v0)(v4 . v1)(v5 . v4)(v6 . v5)(v7 . v6))) ((not (= (* v0 v1) (* v2 v3))) (not (= (* v2 v4) v5)) (not (= (* v6 v1) v5)) (= (* v0 v4) (* v6 v3))))
(13 (instantiate 12 ((v0 . (* (* v2 v3) (e)))(v1 . (e)))) ((not (= (* (* (* v2 v3) (e)) (e)) (* v2 v3))) (not (= (* v2 v4) v5)) (not (= (* v6 (e)) v5)) (= (* (* (* v2 v3) (e)) v4) (* v6 v3))))
(14 (instantiate 3 ((v0 . (* v2 v3)))) ((= (* (* (* v2 v3) (e)) (e)) (* v2 v3))))
(15 (resolve 13 (1) 14 (1)) ((not (= (* v2 v4) v5)) (not (= (* v6 (e)) v5)) (= (* (* (* v2 v3) (e)) v4) (* v6 v3))))
(16 (instantiate 15 ((v2 . v0)(v3 . v4)(v4 . v1)(v5 . v2)(v6 . v3))) ((not (= (* v0 v1) v2)) (not (= (* v3 (e)) v2)) (= (* (* (* v0 v4) (e)) v1) (* v3 v4))))
(17 (instantiate 16 ((v0 . (e))(v1 . (* (e) v64))(v2 . v64))) ((not (= (* (e) (* (e) v64)) v64)) (not (= (* v3 (e)) v64)) (= (* (* (* (e) v4) (e)) (* (e) v64)) (* v3 v4))))
(18 (instantiate 4 ((v0 . v64))) ((= (* (e) (* (e) v64)) v64)))
(19 (resolve 17 (1) 18 (1)) ((not (= (* v3 (e)) v64)) (= (* (* (* (e) v4) (e)) (* (e) v64)) (* v3 v4))))
(20 (instantiate 19 ((v3 . v0)(v4 . v2)(v64 . v1))) ((not (= (* v0 (e)) v1)) (= (* (* (* (e) v2) (e)) (* (e) v1)) (* v0 v2))))
(21 (instantiate 20 ((v1 . (* v0 (e))))) ((not (= (* v0 (e)) (* v0 (e)))) (= (* (* (* (e) v2) (e)) (* (e) (* v0 (e)))) (* v0 v2))))
(22 (instantiate 1 ((v0 . (* v0 (e))))) ((= (* v0 (e)) (* v0 (e)))))
(23 (resolve 21 (1) 22 (1)) ((= (* (* (* (e) v2) (e)) (* (e) (* v0 (e)))) (* v0 v2))))
(24 (instantiate 23 ((v0 . v1)(v2 . v0))) ((= (* (* (* (e) v0) (e)) (* (e) (* v1 (e)))) (* v1 v0))))
(25 (instantiate 2 ((v0 . (e))(v1 . (* (e) v64))(v2 . v64))) ((not (= (* (e) (* (e) v64)) v64)) (not (= (* v3 v4) v64)) (not (= (* (e) v5) v6)) (not (= (* v7 v4) v6)) (= (* v3 v5) (* v7 (* (e) v64)))))
(26 (instantiate 4 ((v0 . v64))) ((= (* (e) (* (e) v64)) v64)))
(27 (resolve 25 (1) 26 (1)) ((not (= (* v3 v4) v64)) (not (= (* (e) v5) v6)) (not (= (* v7 v4) v6)) (= (* v3 v5) (* v7 (* (e) v64)))))
(28 (instantiate 27 ((v3 . v0)(v4 . v1)(v5 . v3)(v6 . v4)(v7 . v5)(v64 . v2))) ((not (= (* v0 v1) v2)) (not (= (* (e) v3) v4)) (not (= (* v5 v1) v4)) (= (* v0 v3) (* v5 (* (e) v2)))))
(29 (instantiate 28 ((v2 . (* v0 v1)))) ((not (= (* v0 v1) (* v0 v1))) (not (= (* (e) v3) v4)) (not (= (* v5 v1) v4)) (= (* v0 v3) (* v5 (* (e) (* v0 v1))))))
(30 (instantiate 1 ((v0 . (* v0 v1)))) ((= (* v0 v1) (* v0 v1))))
(31 (resolve 29 (1) 30 (1)) ((not (= (* (e) v3) v4)) (not (= (* v5 v1) v4)) (= (* v0 v3) (* v5 (* (e) (* v0 v1))))))
(32 (instantiate 31 ((v0 . v4)(v1 . v3)(v3 . v0)(v4 . v1)(v5 . v2))) ((not (= (* (e) v0) v1)) (not (= (* v2 v3) v1)) (= (* v4 v0) (* v2 (* (e) (* v4 v3))))))
(33 (instantiate 32 ((v1 . (* (e) v0)))) ((not (= (* (e) v0) (* (e) v0))) (not (= (* v2 v3) (* (e) v0))) (= (* v4 v0) (* v2 (* (e) (* v4 v3))))))
(34 (instantiate 1 ((v0 . (* (e) v0)))) ((= (* (e) v0) (* (e) v0))))
(35 (resolve 33 (1) 34 (1)) ((not (= (* v2 v3) (* (e) v0))) (= (* v4 v0) (* v2 (* (e) (* v4 v3))))))
(36 (instantiate 35 ((v0 . v2)(v2 . v0)(v3 . v1)(v4 . v3))) ((not (= (* v0 v1) (* (e) v2))) (= (* v3 v2) (* v0 (* (e) (* v3 v1))))))
(37 (instantiate 36 ((v0 . (* (* (e) v2) (e)))(v1 . (e)))) ((not (= (* (* (* (e) v2) (e)) (e)) (* (e) v2))) (= (* v3 v2) (* (* (* (e) v2) (e)) (* (e) (* v3 (e)))))))
(38 (instantiate 3 ((v0 . (* (e) v2)))) ((= (* (* (* (e) v2) (e)) (e)) (* (e) v2))))
(39 (resolve 37 (1) 38 (1)) ((= (* v3 v2) (* (* (* (e) v2) (e)) (* (e) (* v3 (e)))))))
(40 (instantiate 39 ((v2 . v1)(v3 . v0))) ((= (* v0 v1) (* (* (* (e) v1) (e)) (* (e) (* v0 (e)))))))
(41 (instantiate 2 ((v0 . (C4))(v1 . (F))(v2 . (* (C3) (E))))) ((not (= (* (C4) (F)) (* (C3) (E)))) (not (= (* v3 v4) (* (C3) (E)))) (not (= (* (C4) v5) v6)) (not (= (* v7 v4) v6)) (= (* v3 v5) (* v7 (F)))))
(42 (resolve 41 (1) 7 (1)) ((not (= (* v3 v4) (* (C3) (E)))) (not (= (* (C4) v5) v6)) (not (= (* v7 v4) v6)) (= (* v3 v5) (* v7 (F)))))
(43 (instantiate 42 ((v3 . v0)(v4 . v1)(v5 . v2)(v6 . v3)(v7 . v4))) ((not (= (* v0 v1) (* (C3) (E)))) (not (= (* (C4) v2) v3)) (not (= (* v4 v1) v3)) (= (* v0 v2) (* v4 (F)))))
(44 (instantiate 43 ((v0 . (* (* (e) (E)) (e)))(v1 . (* (e) (* (C3) (e)))))) ((not (= (* (* (* (e) (E)) (e)) (* (e) (* (C3) (e)))) (* (C3) (E)))) (not (= (* (C4) v2) v3)) (not (= (* v4 (* (e) (* (C3) (e)))) v3)) (= (* (* (* (e) (E)) (e)) v2) (* v4 (F)))))
(45 (instantiate 24 ((v0 . (E))(v1 . (C3)))) ((= (* (* (* (e) (E)) (e)) (* (e) (* (C3) (e)))) (* (C3) (E)))))
(46 (resolve 44 (1) 45 (1)) ((not (= (* (C4) v2) v3)) (not (= (* v4 (* (e) (* (C3) (e)))) v3)) (= (* (* (* (e) (E)) (e)) v2) (* v4 (F)))))
(47 (instantiate 46 ((v2 . v0)(v3 . v1)(v4 . v2))) ((not (= (* (C4) v0) v1)) (not (= (* v2 (* (e) (* (C3) (e)))) v1)) (= (* (* (* (e) (E)) (e)) v0) (* v2 (F)))))
(48 (instantiate 47 ((v0 . (A))(v1 . (* (C3) (B))))) ((not (= (* (C4) (A)) (* (C3) (B)))) (not (= (* v2 (* (e) (* (C3) (e)))) (* (C3) (B)))) (= (* (* (* (e) (E)) (e)) (A)) (* v2 (F)))))
(49 (resolve 48 (1) 5 (1)) ((not (= (* v2 (* (e) (* (C3) (e)))) (* (C3) (B)))) (= (* (* (* (e) (E)) (e)) (A)) (* v2 (F)))))
(50 (instantiate 49 ((v2 . v0))) ((not (= (* v0 (* (e) (* (C3) (e)))) (* (C3) (B)))) (= (* (* (* (e) (E)) (e)) (A)) (* v0 (F)))))
(51 (instantiate 50 ((v0 . (* (* (e) (B)) (e))))) ((not (= (* (* (* (e) (B)) (e)) (* (e) (* (C3) (e)))) (* (C3) (B)))) (= (* (* (* (e) (E)) (e)) (A)) (* (* (* (e) (B)) (e)) (F)))))
(52 (instantiate 24 ((v0 . (B))(v1 . (C3)))) ((= (* (* (* (e) (B)) (e)) (* (e) (* (C3) (e)))) (* (C3) (B)))))
(53 (resolve 51 (1) 52 (1)) ((= (* (* (* (e) (E)) (e)) (A)) (* (* (* (e) (B)) (e)) (F)))))
(54 (instantiate 2 ((v0 . (* (* (e) v64) (e)))(v1 . (* (e) (* v65 (e))))(v2 . (* v65 v64)))) ((not (= (* (* (* (e) v64) (e)) (* (e) (* v65 (e)))) (* v65 v64))) (not (= (* v3 v4) (* v65 v64))) (not (= (* (* (* (e) v64) (e)) v5) v6)) (not (= (* v7 v4) v6)) (= (* v3 v5) (* v7 (* (e) (* v65 (e)))))))
(55 (instantiate 24 ((v0 . v64)(v1 . v65))) ((= (* (* (* (e) v64) (e)) (* (e) (* v65 (e)))) (* v65 v64))))
(56 (resolve 54 (1) 55 (1)) ((not (= (* v3 v4) (* v65 v64))) (not (= (* (* (* (e) v64) (e)) v5) v6)) (not (= (* v7 v4) v6)) (= (* v3 v5) (* v7 (* (e) (* v65 (e)))))))
(57 (instantiate 56 ((v3 . v0)(v4 . v1)(v5 . v4)(v6 . v5)(v7 . v6)(v64 . v3)(v65 . v2))) ((not (= (* v0 v1) (* v2 v3))) (not (= (* (* (* (e) v3) (e)) v4) v5)) (not (= (* v6 v1) v5)) (= (* v0 v4) (* v6 (* (e) (* v2 (e)))))))
(58 (instantiate 57 ((v0 . (C2))(v1 . (A))(v2 . (C1))(v3 . (B)))) ((not (= (* (C2) (A)) (* (C1) (B)))) (not (= (* (* (* (e) (B)) (e)) v4) v5)) (not (= (* v6 (A)) v5)) (= (* (C2) v4) (* v6 (* (e) (* (C1) (e)))))))
(59 (resolve 58 (1) 6 (1)) ((not (= (* (* (* (e) (B)) (e)) v4) v5)) (not (= (* v6 (A)) v5)) (= (* (C2) v4) (* v6 (* (e) (* (C1) (e)))))))
(60 (instantiate 59 ((v4 . v0)(v5 . v1)(v6 . v2))) ((not (= (* (* (* (e) (B)) (e)) v0) v1)) (not (= (* v2 (A)) v1)) (= (* (C2) v0) (* v2 (* (e) (* (C1) (e)))))))
(61 (instantiate 60 ((v1 . (* (* (* (e) (B)) (e)) v0)))) ((not (= (* (* (* (e) (B)) (e)) v0) (* (* (* (e) (B)) (e)) v0))) (not (= (* v2 (A)) (* (* (* (e) (B)) (e)) v0))) (= (* (C2) v0) (* v2 (* (e) (* (C1) (e)))))))
(62 (instantiate 1 ((v0 . (* (* (* (e) (B)) (e)) v0)))) ((= (* (* (* (e) (B)) (e)) v0) (* (* (* (e) (B)) (e)) v0))))
(63 (resolve 61 (1) 62 (1)) ((not (= (* v2 (A)) (* (* (* (e) (B)) (e)) v0))) (= (* (C2) v0) (* v2 (* (e) (* (C1) (e)))))))
(64 (instantiate 63 ((v0 . v1)(v2 . v0))) ((not (= (* v0 (A)) (* (* (* (e) (B)) (e)) v1))) (= (* (C2) v1) (* v0 (* (e) (* (C1) (e)))))))
(65 (instantiate 64 ((v0 . (* (* (e) (E)) (e)))(v1 . (F)))) ((not (= (* (* (* (e) (E)) (e)) (A)) (* (* (* (e) (B)) (e)) (F)))) (= (* (C2) (F)) (* (* (* (e) (E)) (e)) (* (e) (* (C1) (e)))))))
(66 (resolve 65 (1) 53 (1)) ((= (* (C2) (F)) (* (* (* (e) (E)) (e)) (* (e) (* (C1) (e)))))))
(67 (flip 66 (1)) ((= (* (* (* (e) (E)) (e)) (* (e) (* (C1) (e)))) (* (C2) (F)))))
(68 (instantiate 40 ((v0 . (* (* (e) (E)) (e)))(v1 . (* (e) (* (C1) (e)))))) ((= (* (* (* (e) (E)) (e)) (* (e) (* (C1) (e)))) (* (* (* (e) (* (e) (* (C1) (e)))) (e)) (* (e) (* (* (* (e) (E)) (e)) (e)))))))
(69 (paramod 68 (1 1) 67 (1 1)) ((= (* (* (* (e) (* (e) (* (C1) (e)))) (e)) (* (e) (* (* (* (e) (E)) (e)) (e)))) (* (C2) (F)))))
(70 (instantiate 4 ((v0 . (* (C1) (e))))) ((= (* (e) (* (e) (* (C1) (e)))) (* (C1) (e)))))
(71 (paramod 70 (1 1) 69 (1 1 1 1)) ((= (* (* (* (C1) (e)) (e)) (* (e) (* (* (* (e) (E)) (e)) (e)))) (* (C2) (F)))))
(72 (instantiate 3 ((v0 . (C1)))) ((= (* (* (C1) (e)) (e)) (C1))))
(73 (paramod 72 (1 1) 71 (1 1 1)) ((= (* (C1) (* (e) (* (* (* (e) (E)) (e)) (e)))) (* (C2) (F)))))
(74 (instantiate 3 ((v0 . (* (e) (E))))) ((= (* (* (* (e) (E)) (e)) (e)) (* (e) (E)))))
(75 (paramod 74 (1 1) 73 (1 1 2 2)) ((= (* (C1) (* (e) (* (e) (E)))) (* (C2) (F)))))
(76 (instantiate 4 ((v0 . (E)))) ((= (* (e) (* (e) (E))) (E))))
(77 (paramod 76 (1 1) 75 (1 1 2)) ((= (* (C1) (E)) (* (C2) (F)))))
(78 (flip 77 (1)) ((= (* (C2) (F)) (* (C1) (E)))))
(79 (resolve 8 (1) 78 (1)) ())
)