;; ----- Otter 3.0.4, August 1995 -----
;; The job was started by mccune on gyro, Thu Nov  2 00:22:35 1995
;;
;;;;  -> x=x.
;;;; x*y=u, x*z=u -> y=z.
;;;; y*x=u, z*x=u -> y=z.
;;;;  -> (x*y)* (z*u)= (x*z)* (y*u).
;;;;  -> C3*A=C2*B.
;;;;  -> C3*D=C1*B.
;;;; C2*D=C1*A -> .
;;
;; ----> UNIT CONFLICT at   1.09 sec ----> 237 [binary,235.1,9.1]  -> .
;;
(
(1 (input) ((not (= (* v0 v1) v2)) (not (= (* v0 v3) v2)) (= v1 v3)))
(2 (input) ((= (* (* v0 v1) (* v2 v3)) (* (* v0 v2) (* v1 v3)))))
(3 (input) ((= (* (C3) (A)) (* (C2) (B)))))
(4 (input) ((= (* (C3) (D)) (* (C1) (B)))))
(5 (input) ((not (= (* (C2) (D)) (* (C1) (A))))))
(6 (instantiate 2 ((v0 . v64)(v1 . v65)(v2 . (C3))(v3 . (A)))) ((= (* (* v64 v65) (* (C3) (A))) (* (* v64 (C3)) (* v65 (A))))))
(7 (paramod 3 (1 1) 6 (1 1 2)) ((= (* (* v64 v65) (* (C2) (B))) (* (* v64 (C3)) (* v65 (A))))))
(8 (instantiate 7 ((v64 . v0)(v65 . v1))) ((= (* (* v0 v1) (* (C2) (B))) (* (* v0 (C3)) (* v1 (A))))))
(9 (flip 8 (1)) ((= (* (* v0 (C3)) (* v1 (A))) (* (* v0 v1) (* (C2) (B))))))
(10 (instantiate 2 ((v0 . v64)(v1 . v65)(v2 . (C3))(v3 . (D)))) ((= (* (* v64 v65) (* (C3) (D))) (* (* v64 (C3)) (* v65 (D))))))
(11 (paramod 4 (1 1) 10 (1 1 2)) ((= (* (* v64 v65) (* (C1) (B))) (* (* v64 (C3)) (* v65 (D))))))
(12 (instantiate 11 ((v64 . v0)(v65 . v1))) ((= (* (* v0 v1) (* (C1) (B))) (* (* v0 (C3)) (* v1 (D))))))
(13 (instantiate 2 ((v0 . v64)(v1 . v65)(v2 . (C1))(v3 . (B)))) ((= (* (* v64 v65) (* (C1) (B))) (* (* v64 (C1)) (* v65 (B))))))
(14 (instantiate 12 ((v0 . v64)(v1 . v65))) ((= (* (* v64 v65) (* (C1) (B))) (* (* v64 (C3)) (* v65 (D))))))
(15 (paramod 13 (1 1) 14 (1 1)) ((= (* (* v64 (C1)) (* v65 (B))) (* (* v64 (C3)) (* v65 (D))))))
(16 (flip 15 (1)) ((= (* (* v64 (C3)) (* v65 (D))) (* (* v64 (C1)) (* v65 (B))))))
(17 (instantiate 16 ((v64 . v0)(v65 . v1))) ((= (* (* v0 (C3)) (* v1 (D))) (* (* v0 (C1)) (* v1 (B))))))
(18 (instantiate 1 ((v0 . (* v64 (C3)))(v1 . (* v65 (A)))(v2 . (* (* v64 v65) (* (C2) (B)))))) ((not (= (* (* v64 (C3)) (* v65 (A))) (* (* v64 v65) (* (C2) (B))))) (not (= (* (* v64 (C3)) v3) (* (* v64 v65) (* (C2) (B))))) (= (* v65 (A)) v3)))
(19 (instantiate 9 ((v0 . v64)(v1 . v65))) ((= (* (* v64 (C3)) (* v65 (A))) (* (* v64 v65) (* (C2) (B))))))
(20 (resolve 18 (1) 19 (1)) ((not (= (* (* v64 (C3)) v3) (* (* v64 v65) (* (C2) (B))))) (= (* v65 (A)) v3)))
(21 (instantiate 20 ((v3 . v1)(v64 . v0)(v65 . v2))) ((not (= (* (* v0 (C3)) v1) (* (* v0 v2) (* (C2) (B))))) (= (* v2 (A)) v1)))
(22 (instantiate 21 ((v0 . v64)(v1 . (* (C2) (D)))(v2 . (C1)))) ((not (= (* (* v64 (C3)) (* (C2) (D))) (* (* v64 (C1)) (* (C2) (B))))) (= (* (C1) (A)) (* (C2) (D)))))
(23 (instantiate 17 ((v0 . v64)(v1 . (C2)))) ((= (* (* v64 (C3)) (* (C2) (D))) (* (* v64 (C1)) (* (C2) (B))))))
(24 (resolve 22 (1) 23 (1)) ((= (* (C1) (A)) (* (C2) (D)))))
(25 (flip 24 (1)) ((= (* (C2) (D)) (* (C1) (A)))))
(26 (resolve 5 (1) 25 (1)) ())
)