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