;; ----- Otter 3.0.4, August 1995 -----
;; The job was started by mccune on gyro, Thu Nov  2 00:26:43 1995
;;
;;;;  -> x=x.
;;;; z1*x=u, z2*y=u, z1*z=w, z3*y=w -> z2*z=z3*x.
;;;;  -> x* (y*x)=y.
;;;; (A*C)* (B*D)= (A*B)* (C*D) -> .
;;
;; ----> UNIT CONFLICT at   0.09 sec ----> 20 [binary,19.1,5.1]  -> .
;;
(
(1 (input) ((not (= (* v0 v1) v2)) (not (= (* v3 v4) v2)) (not (= (* v0 v5) v6)) (not (= (* v7 v4) v6)) (= (* v3 v5) (* v7 v1))))
(2 (input) ((= (* v0 (* v1 v0)) v1)))
(3 (input) ((not (= (* (* (A) (C)) (* (B) (D))) (* (* (A) (B)) (* (C) (D)))))))
(4 (instantiate 2 ((v0 . v65))) ((= (* v65 (* v1 v65)) v1)))
(5 (instantiate 2 ((v0 . (* v1 v65))(v1 . v65))) ((= (* (* v1 v65) (* v65 (* v1 v65))) v65)))
(6 (paramod 4 (1 1) 5 (1 1 2)) ((= (* (* v1 v65) v1) v65)))
(7 (instantiate 6 ((v1 . v0)(v65 . v1))) ((= (* (* v0 v1) v0) v1)))
(8 (instantiate 1 ((v0 . v64)(v1 . (* v65 v64))(v2 . v65))) ((not (= (* v64 (* v65 v64)) v65)) (not (= (* v3 v4) v65)) (not (= (* v64 v5) v6)) (not (= (* v7 v4) v6)) (= (* v3 v5) (* v7 (* v65 v64)))))
(9 (instantiate 2 ((v0 . v64)(v1 . v65))) ((= (* v64 (* v65 v64)) v65)))
(10 (resolve 8 (1) 9 (1)) ((not (= (* v3 v4) v65)) (not (= (* v64 v5) v6)) (not (= (* v7 v4) v6)) (= (* v3 v5) (* v7 (* v65 v64)))))
(11 (instantiate 10 ((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 (* v2 v3)))))
(12 (instantiate 11 ((v0 . (* v64 v65))(v1 . v64)(v2 . v65))) ((not (= (* (* v64 v65) v64) v65)) (not (= (* v3 v4) v5)) (not (= (* v6 v64) v5)) (= (* (* v64 v65) v4) (* v6 (* v65 v3)))))
(13 (instantiate 7 ((v0 . v64)(v1 . v65))) ((= (* (* v64 v65) v64) v65)))
(14 (resolve 12 (1) 13 (1)) ((not (= (* v3 v4) v5)) (not (= (* v6 v64) v5)) (= (* (* v64 v65) v4) (* v6 (* v65 v3)))))
(15 (instantiate 14 ((v3 . v0)(v4 . v1)(v5 . v2)(v6 . v3)(v64 . v4)(v65 . v5))) ((not (= (* v0 v1) v2)) (not (= (* v3 v4) v2)) (= (* (* v4 v5) v1) (* v3 (* v5 v0)))))
(16 (instantiate 15 ((v0 . v64)(v1 . (* v65 v64))(v2 . v65))) ((not (= (* v64 (* v65 v64)) v65)) (not (= (* v3 v4) v65)) (= (* (* v4 v5) (* v65 v64)) (* v3 (* v5 v64)))))
(17 (instantiate 2 ((v0 . v64)(v1 . v65))) ((= (* v64 (* v65 v64)) v65)))
(18 (resolve 16 (1) 17 (1)) ((not (= (* v3 v4) v65)) (= (* (* v4 v5) (* v65 v64)) (* v3 (* v5 v64)))))
(19 (instantiate 18 ((v3 . v0)(v4 . v1)(v5 . v3)(v64 . v4)(v65 . v2))) ((not (= (* v0 v1) v2)) (= (* (* v1 v3) (* v2 v4)) (* v0 (* v3 v4)))))
(20 (instantiate 19 ((v0 . (* v64 v65))(v1 . v64)(v2 . v65))) ((not (= (* (* v64 v65) v64) v65)) (= (* (* v64 v3) (* v65 v4)) (* (* v64 v65) (* v3 v4)))))
(21 (instantiate 7 ((v0 . v64)(v1 . v65))) ((= (* (* v64 v65) v64) v65)))
(22 (resolve 20 (1) 21 (1)) ((= (* (* v64 v3) (* v65 v4)) (* (* v64 v65) (* v3 v4)))))
(23 (instantiate 22 ((v3 . v1)(v4 . v3)(v64 . v0)(v65 . v2))) ((= (* (* v0 v1) (* v2 v3)) (* (* v0 v2) (* v1 v3)))))
(24 (instantiate 23 ((v0 . (A))(v1 . (C))(v2 . (B))(v3 . (D)))) ((= (* (* (A) (C)) (* (B) (D))) (* (* (A) (B)) (* (C) (D))))))
(25 (resolve 3 (1) 24 (1)) ())
)