;; ----- Otter 3.0.4, August 1995 -----
;; The job was started by mccune on gyro, Thu Nov  2 00:17:32 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*y=y*x.
;;;;  -> x* (y*x)=y.
;;;; (A*C)* (B*D)= (A*B)* (C*D) -> .
;;
;; ----> UNIT CONFLICT at  10.48 sec ----> 1097 [binary,1096.1,6.1]  -> .
;;
(
(1 (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))))
(2 (input) ((= (* v0 v1) (* v1 v0))))
(3 (input) ((= (* v0 (* v1 v0)) v1)))
(4 (input) ((not (= (* (* (A) (C)) (* (B) (D))) (* (* (A) (B)) (* (C) (D)))))))
(5 (instantiate 3 ((v0 . v65))) ((= (* v65 (* v1 v65)) v1)))
(6 (instantiate 3 ((v0 . (* v1 v65))(v1 . v65))) ((= (* (* v1 v65) (* v65 (* v1 v65))) v65)))
(7 (paramod 5 (1 1) 6 (1 1 2)) ((= (* (* v1 v65) v1) v65)))
(8 (instantiate 7 ((v1 . v0)(v65 . v1))) ((= (* (* v0 v1) v0) v1)))
(9 (instantiate 2 ((v0 . v65)(v1 . v64))) ((= (* v65 v64) (* v64 v65))))
(10 (instantiate 3 ((v0 . v64)(v1 . v65))) ((= (* v64 (* v65 v64)) v65)))
(11 (paramod 9 (1 1) 10 (1 1 2)) ((= (* v64 (* v64 v65)) v65)))
(12 (instantiate 11 ((v64 . v0)(v65 . v1))) ((= (* v0 (* v0 v1)) v1)))
(13 (instantiate 1 ((v0 . v64)(v1 . (* v64 v65))(v2 . v65))) ((not (= (* v64 (* v64 v65)) v65)) (not (= (* v3 v4) v65)) (not (= (* v5 (* v64 v65)) v6)) (not (= (* v7 v4) v6)) (not (= (* v64 v8) v9)) (not (= (* v3 v10) v9)) (= (* v5 v8) (* v7 v10))))
(14 (instantiate 12 ((v0 . v64)(v1 . v65))) ((= (* v64 (* v64 v65)) v65)))
(15 (resolve 13 (1) 14 (1)) ((not (= (* v3 v4) v65)) (not (= (* v5 (* v64 v65)) v6)) (not (= (* v7 v4) v6)) (not (= (* v64 v8) v9)) (not (= (* v3 v10) v9)) (= (* v5 v8) (* v7 v10))))
(16 (instantiate 15 ((v3 . v0)(v4 . v1)(v5 . v3)(v6 . v5)(v7 . v6)(v8 . v7)(v9 . v8)(v10 . v9)(v64 . v4)(v65 . v2))) ((not (= (* v0 v1) v2)) (not (= (* v3 (* v4 v2)) v5)) (not (= (* v6 v1) v5)) (not (= (* v4 v7) v8)) (not (= (* v0 v9) v8)) (= (* v3 v7) (* v6 v9))))
(17 (instantiate 16 ((v0 . v64)(v1 . v65)(v2 . (* v65 v64)))) ((not (= (* v64 v65) (* v65 v64))) (not (= (* v3 (* v4 (* v65 v64))) v5)) (not (= (* v6 v65) v5)) (not (= (* v4 v7) v8)) (not (= (* v64 v9) v8)) (= (* v3 v7) (* v6 v9))))
(18 (instantiate 2 ((v0 . v64)(v1 . v65))) ((= (* v64 v65) (* v65 v64))))
(19 (resolve 17 (1) 18 (1)) ((not (= (* v3 (* v4 (* v65 v64))) v5)) (not (= (* v6 v65) v5)) (not (= (* v4 v7) v8)) (not (= (* v64 v9) v8)) (= (* v3 v7) (* v6 v9))))
(20 (instantiate 19 ((v3 . v0)(v4 . v1)(v5 . v4)(v6 . v5)(v7 . v6)(v8 . v7)(v9 . v8)(v64 . v3)(v65 . v2))) ((not (= (* v0 (* v1 (* v2 v3))) v4)) (not (= (* v5 v2) v4)) (not (= (* v1 v6) v7)) (not (= (* v3 v8) v7)) (= (* v0 v6) (* v5 v8))))
(21 (instantiate 20 ((v0 . (* v2 v3))(v1 . v65)(v4 . v65))) ((not (= (* (* v2 v3) (* v65 (* v2 v3))) v65)) (not (= (* v5 v2) v65)) (not (= (* v65 v6) v7)) (not (= (* v3 v8) v7)) (= (* (* v2 v3) v6) (* v5 v8))))
(22 (instantiate 3 ((v0 . (* v2 v3))(v1 . v65))) ((= (* (* v2 v3) (* v65 (* v2 v3))) v65)))
(23 (resolve 21 (1) 22 (1)) ((not (= (* v5 v2) v65)) (not (= (* v65 v6) v7)) (not (= (* v3 v8) v7)) (= (* (* v2 v3) v6) (* v5 v8))))
(24 (instantiate 23 ((v2 . v1)(v3 . v5)(v5 . v0)(v6 . v3)(v7 . v4)(v8 . v6)(v65 . v2))) ((not (= (* v0 v1) v2)) (not (= (* v2 v3) v4)) (not (= (* v5 v6) v4)) (= (* (* v1 v5) v3) (* v0 v6))))
(25 (instantiate 24 ((v0 . (* v64 v65))(v1 . v64)(v2 . v65))) ((not (= (* (* v64 v65) v64) v65)) (not (= (* v65 v3) v4)) (not (= (* v5 v6) v4)) (= (* (* v64 v5) v3) (* (* v64 v65) v6))))
(26 (instantiate 8 ((v0 . v64)(v1 . v65))) ((= (* (* v64 v65) v64) v65)))
(27 (resolve 25 (1) 26 (1)) ((not (= (* v65 v3) v4)) (not (= (* v5 v6) v4)) (= (* (* v64 v5) v3) (* (* v64 v65) v6))))
(28 (instantiate 27 ((v3 . v1)(v4 . v2)(v5 . v3)(v6 . v4)(v64 . v5)(v65 . v0))) ((not (= (* v0 v1) v2)) (not (= (* v3 v4) v2)) (= (* (* v5 v3) v1) (* (* v5 v0) v4))))
(29 (instantiate 28 ((v0 . v64)(v1 . (* v64 v65))(v2 . v65))) ((not (= (* v64 (* v64 v65)) v65)) (not (= (* v3 v4) v65)) (= (* (* v5 v3) (* v64 v65)) (* (* v5 v64) v4))))
(30 (instantiate 12 ((v0 . v64)(v1 . v65))) ((= (* v64 (* v64 v65)) v65)))
(31 (resolve 29 (1) 30 (1)) ((not (= (* v3 v4) v65)) (= (* (* v5 v3) (* v64 v65)) (* (* v5 v64) v4))))
(32 (instantiate 31 ((v3 . v0)(v4 . v1)(v5 . v3)(v64 . v4)(v65 . v2))) ((not (= (* v0 v1) v2)) (= (* (* v3 v0) (* v4 v2)) (* (* v3 v4) v1))))
(33 (instantiate 32 ((v0 . v64)(v1 . (* v64 v65))(v2 . v65))) ((not (= (* v64 (* v64 v65)) v65)) (= (* (* v3 v64) (* v4 v65)) (* (* v3 v4) (* v64 v65)))))
(34 (instantiate 12 ((v0 . v64)(v1 . v65))) ((= (* v64 (* v64 v65)) v65)))
(35 (resolve 33 (1) 34 (1)) ((= (* (* v3 v64) (* v4 v65)) (* (* v3 v4) (* v64 v65)))))
(36 (instantiate 35 ((v3 . v0)(v4 . v2)(v64 . v1)(v65 . v3))) ((= (* (* v0 v1) (* v2 v3)) (* (* v0 v2) (* v1 v3)))))
(37 (instantiate 36 ((v0 . (A))(v1 . (C))(v2 . (B))(v3 . (D)))) ((= (* (* (A) (C)) (* (B) (D))) (* (* (A) (B)) (* (C) (D))))))
(38 (resolve 4 (1) 37 (1)) ())
)