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