;; ----- Otter 3.0.4, August 1995 -----
;; The job was started by mccune on gyro, Thu Nov  2 00:17:52 1995
;;
;;;;  -> x=x.
;;;; z1*x=w1, z2*y=w1, z3*x=w2, z4*y=w2, z1*u=w3, z2*v=w3 -> z3*u=z4*v.
;;;;  -> x*e=x.
;;;;  -> e*x=x.
;;;; (A*B)*C=A* (B*C) -> .
;;
;; ----> UNIT CONFLICT at   0.14 sec ----> 10 [binary,8.1,7.1]  -> .
;;
(
(1 (input) ((= v0 v0)))
(2 (input) ((not (= (* v0 v1) v2)) (not (= (* v3 v4) v2)) (not (= (* v5 v1) v6)) (not (= (* v7 v4) v6)) (not (= (* v0 v8) v9)) (not (= (* v3 v10) v9)) (= (* v5 v8) (* v7 v10))))
(3 (input) ((= (* v0 (e)) v0)))
(4 (input) ((= (* (e) v0) v0)))
(5 (input) ((not (= (* (* (A) (B)) (C)) (* (A) (* (B) (C)))))))
(6 (instantiate 2 ((v0 . v64)(v1 . (e))(v2 . v64))) ((not (= (* v64 (e)) v64)) (not (= (* v3 v4) v64)) (not (= (* v5 (e)) v6)) (not (= (* v7 v4) v6)) (not (= (* v64 v8) v9)) (not (= (* v3 v10) v9)) (= (* v5 v8) (* v7 v10))))
(7 (instantiate 3 ((v0 . v64))) ((= (* v64 (e)) v64)))
(8 (resolve 6 (1) 7 (1)) ((not (= (* v3 v4) v64)) (not (= (* v5 (e)) v6)) (not (= (* v7 v4) v6)) (not (= (* v64 v8) v9)) (not (= (* v3 v10) v9)) (= (* v5 v8) (* v7 v10))))
(9 (instantiate 8 ((v3 . v0)(v4 . v1)(v5 . v3)(v6 . v4)(v7 . v5)(v8 . v6)(v9 . v7)(v10 . v8)(v64 . v2))) ((not (= (* v0 v1) v2)) (not (= (* v3 (e)) v4)) (not (= (* v5 v1) v4)) (not (= (* v2 v6) v7)) (not (= (* v0 v8) v7)) (= (* v3 v6) (* v5 v8))))
(10 (instantiate 9 ((v0 . (e))(v1 . v64)(v2 . v64))) ((not (= (* (e) v64) v64)) (not (= (* v3 (e)) v4)) (not (= (* v5 v64) v4)) (not (= (* v64 v6) v7)) (not (= (* (e) v8) v7)) (= (* v3 v6) (* v5 v8))))
(11 (instantiate 4 ((v0 . v64))) ((= (* (e) v64) v64)))
(12 (resolve 10 (1) 11 (1)) ((not (= (* v3 (e)) v4)) (not (= (* v5 v64) v4)) (not (= (* v64 v6) v7)) (not (= (* (e) v8) v7)) (= (* v3 v6) (* v5 v8))))
(13 (instantiate 12 ((v3 . v0)(v4 . v1)(v5 . v2)(v6 . v4)(v7 . v5)(v8 . v6)(v64 . v3))) ((not (= (* v0 (e)) v1)) (not (= (* v2 v3) v1)) (not (= (* v3 v4) v5)) (not (= (* (e) v6) v5)) (= (* v0 v4) (* v2 v6))))
(14 (instantiate 13 ((v0 . v64)(v1 . v64))) ((not (= (* v64 (e)) v64)) (not (= (* v2 v3) v64)) (not (= (* v3 v4) v5)) (not (= (* (e) v6) v5)) (= (* v64 v4) (* v2 v6))))
(15 (instantiate 3 ((v0 . v64))) ((= (* v64 (e)) v64)))
(16 (resolve 14 (1) 15 (1)) ((not (= (* v2 v3) v64)) (not (= (* v3 v4) v5)) (not (= (* (e) v6) v5)) (= (* v64 v4) (* v2 v6))))
(17 (instantiate 16 ((v2 . v0)(v3 . v1)(v4 . v3)(v5 . v4)(v6 . v5)(v64 . v2))) ((not (= (* v0 v1) v2)) (not (= (* v1 v3) v4)) (not (= (* (e) v5) v4)) (= (* v2 v3) (* v0 v5))))
(18 (instantiate 17 ((v2 . (* v0 v1)))) ((not (= (* v0 v1) (* v0 v1))) (not (= (* v1 v3) v4)) (not (= (* (e) v5) v4)) (= (* (* v0 v1) v3) (* v0 v5))))
(19 (instantiate 1 ((v0 . (* v0 v1)))) ((= (* v0 v1) (* v0 v1))))
(20 (resolve 18 (1) 19 (1)) ((not (= (* v1 v3) v4)) (not (= (* (e) v5) v4)) (= (* (* v0 v1) v3) (* v0 v5))))
(21 (instantiate 20 ((v0 . v4)(v1 . v0)(v3 . v1)(v4 . v2)(v5 . v3))) ((not (= (* v0 v1) v2)) (not (= (* (e) v3) v2)) (= (* (* v4 v0) v1) (* v4 v3))))
(22 (instantiate 21 ((v2 . (* v0 v1)))) ((not (= (* v0 v1) (* v0 v1))) (not (= (* (e) v3) (* v0 v1))) (= (* (* v4 v0) v1) (* v4 v3))))
(23 (instantiate 1 ((v0 . (* v0 v1)))) ((= (* v0 v1) (* v0 v1))))
(24 (resolve 22 (1) 23 (1)) ((not (= (* (e) v3) (* v0 v1))) (= (* (* v4 v0) v1) (* v4 v3))))
(25 (instantiate 24 ((v0 . v1)(v1 . v2)(v3 . v0)(v4 . v3))) ((not (= (* (e) v0) (* v1 v2))) (= (* (* v3 v1) v2) (* v3 v0))))
(26 (instantiate 25 ((v0 . (* v1 v2)))) ((not (= (* (e) (* v1 v2)) (* v1 v2))) (= (* (* v3 v1) v2) (* v3 (* v1 v2)))))
(27 (instantiate 4 ((v0 . (* v1 v2)))) ((= (* (e) (* v1 v2)) (* v1 v2))))
(28 (resolve 26 (1) 27 (1)) ((= (* (* v3 v1) v2) (* v3 (* v1 v2)))))
(29 (instantiate 28 ((v3 . v0))) ((= (* (* v0 v1) v2) (* v0 (* v1 v2)))))
(30 (instantiate 29 ((v0 . (A))(v1 . (B))(v2 . (C)))) ((= (* (* (A) (B)) (C)) (* (A) (* (B) (C))))))
(31 (resolve 5 (1) 30 (1)) ())
)