;; ----- Otter 3.0.4, August 1995 -----
;; The job was started by mccune on gyro, Wed Nov  1 22:23:22 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).
;;;;  -> b*b0=a*a0.
;;;;  -> d*b0=c*a0.
;;;;  -> b*d0=a*c0.
;;;; d*d0=c*c0 -> .
;;
;; ----> UNIT CONFLICT at   9.76 sec ----> 508 [binary,506.1,1.1]  -> .
;;
(
(1 (input) ((not (= (* (d) (d0)) (* (c) (c0))))))
(2 (input) ((not (= (* v0 v1) v2)) (not (= (* v0 v3) v2)) (= v1 v3)))
(3 (input) ((not (= (* v0 v1) v2)) (not (= (* v3 v1) v2)) (= v0 v3)))
(4 (input) ((= (* (* v0 v1) (* v2 v3)) (* (* v0 v2) (* v1 v3)))))
(5 (input) ((= (* (b) (b0)) (* (a) (a0)))))
(6 (input) ((= (* (d) (b0)) (* (c) (a0)))))
(7 (input) ((= (* (b) (d0)) (* (a) (c0)))))
(8 (instantiate 4 ((v0 . (* v0 v1))(v1 . (* v2 v3))(v2 . v66)(v3 . v67))) ((= (* (* (* v0 v1) (* v2 v3)) (* v66 v67)) (* (* (* v0 v1) v66) (* (* v2 v3) v67)))))
(9 (paramod 4 (1 1) 8 (1 1 1)) ((= (* (* (* v0 v2) (* v1 v3)) (* v66 v67)) (* (* (* v0 v1) v66) (* (* v2 v3) v67)))))
(10 (instantiate 9 ((v1 . v2)(v2 . v1)(v66 . v4)(v67 . v5))) ((= (* (* (* v0 v1) (* v2 v3)) (* v4 v5)) (* (* (* v0 v2) v4) (* (* v1 v3) v5)))))
(11 (flip 10 (1)) ((= (* (* (* v0 v2) v4) (* (* v1 v3) v5)) (* (* (* v0 v1) (* v2 v3)) (* v4 v5)))))
(12 (instantiate 4 ((v0 . (b))(v1 . (b0))(v2 . v66)(v3 . v67))) ((= (* (* (b) (b0)) (* v66 v67)) (* (* (b) v66) (* (b0) v67)))))
(13 (paramod 5 (1 1) 12 (1 1 1)) ((= (* (* (a) (a0)) (* v66 v67)) (* (* (b) v66) (* (b0) v67)))))
(14 (flip 13 (1)) ((= (* (* (b) v66) (* (b0) v67)) (* (* (a) (a0)) (* v66 v67)))))
(15 (instantiate 14 ((v66 . v0)(v67 . v1))) ((= (* (* (b) v0) (* (b0) v1)) (* (* (a) (a0)) (* v0 v1)))))
(16 (instantiate 4 ((v0 . (d))(v1 . (b0))(v2 . v66)(v3 . v67))) ((= (* (* (d) (b0)) (* v66 v67)) (* (* (d) v66) (* (b0) v67)))))
(17 (paramod 6 (1 1) 16 (1 1 1)) ((= (* (* (c) (a0)) (* v66 v67)) (* (* (d) v66) (* (b0) v67)))))
(18 (flip 17 (1)) ((= (* (* (d) v66) (* (b0) v67)) (* (* (c) (a0)) (* v66 v67)))))
(19 (instantiate 18 ((v66 . v0)(v67 . v1))) ((= (* (* (d) v0) (* (b0) v1)) (* (* (c) (a0)) (* v0 v1)))))
(20 (instantiate 15 ((v0 . (d0))(v1 . v65))) ((= (* (* (b) (d0)) (* (b0) v65)) (* (* (a) (a0)) (* (d0) v65)))))
(21 (paramod 7 (1 1) 20 (1 1 1)) ((= (* (* (a) (c0)) (* (b0) v65)) (* (* (a) (a0)) (* (d0) v65)))))
(22 (instantiate 21 ((v65 . v0))) ((= (* (* (a) (c0)) (* (b0) v0)) (* (* (a) (a0)) (* (d0) v0)))))
(23 (instantiate 4 ((v0 . v64)(v1 . v65)(v2 . (* (a) (c0)))(v3 . (* (b0) v0)))) ((= (* (* v64 v65) (* (* (a) (c0)) (* (b0) v0))) (* (* v64 (* (a) (c0))) (* v65 (* (b0) v0))))))
(24 (paramod 22 (1 1) 23 (1 1 2)) ((= (* (* v64 v65) (* (* (a) (a0)) (* (d0) v0))) (* (* v64 (* (a) (c0))) (* v65 (* (b0) v0))))))
(25 (instantiate 24 ((v0 . v2)(v64 . v0)(v65 . v1))) ((= (* (* v0 v1) (* (* (a) (a0)) (* (d0) v2))) (* (* v0 (* (a) (c0))) (* v1 (* (b0) v2))))))
(26 (instantiate 4 ((v0 . v64)(v1 . v66))) ((= (* (* v64 v66) (* v2 v3)) (* (* v64 v2) (* v66 v3)))))
(27 (instantiate 11 ((v0 . v64)(v1 . v65)(v2 . v66)(v3 . v67)(v4 . (* v2 v3))(v5 . v69))) ((= (* (* (* v64 v66) (* v2 v3)) (* (* v65 v67) v69)) (* (* (* v64 v65) (* v66 v67)) (* (* v2 v3) v69)))))
(28 (paramod 26 (1 1) 27 (1 1 1)) ((= (* (* (* v64 v2) (* v66 v3)) (* (* v65 v67) v69)) (* (* (* v64 v65) (* v66 v67)) (* (* v2 v3) v69)))))
(29 (instantiate 28 ((v2 . v1)(v64 . v0)(v65 . v4)(v66 . v2)(v67 . v5)(v69 . v6))) ((= (* (* (* v0 v1) (* v2 v3)) (* (* v4 v5) v6)) (* (* (* v0 v4) (* v2 v5)) (* (* v1 v3) v6)))))
(30 (instantiate 4 ((v0 . v64)(v1 . v65)(v2 . (* (a) (a0)))(v3 . (* (d0) v66)))) ((= (* (* v64 v65) (* (* (a) (a0)) (* (d0) v66))) (* (* v64 (* (a) (a0))) (* v65 (* (d0) v66))))))
(31 (instantiate 25 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (* (* v64 v65) (* (* (a) (a0)) (* (d0) v66))) (* (* v64 (* (a) (c0))) (* v65 (* (b0) v66))))))
(32 (paramod 30 (1 1) 31 (1 1)) ((= (* (* v64 (* (a) (a0))) (* v65 (* (d0) v66))) (* (* v64 (* (a) (c0))) (* v65 (* (b0) v66))))))
(33 (flip 32 (1)) ((= (* (* v64 (* (a) (c0))) (* v65 (* (b0) v66))) (* (* v64 (* (a) (a0))) (* v65 (* (d0) v66))))))
(34 (instantiate 33 ((v64 . v0)(v65 . v1)(v66 . v2))) ((= (* (* v0 (* (a) (c0))) (* v1 (* (b0) v2))) (* (* v0 (* (a) (a0))) (* v1 (* (d0) v2))))))
(35 (instantiate 2 ((v0 . (* v64 (* (a) (c0))))(v1 . (* v65 (* (b0) v66)))(v2 . (* (* v64 (* (a) (a0))) (* v65 (* (d0) v66)))))) ((not (= (* (* v64 (* (a) (c0))) (* v65 (* (b0) v66))) (* (* v64 (* (a) (a0))) (* v65 (* (d0) v66))))) (not (= (* (* v64 (* (a) (c0))) v3) (* (* v64 (* (a) (a0))) (* v65 (* (d0) v66))))) (= (* v65 (* (b0) v66)) v3)))
(36 (instantiate 34 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (* (* v64 (* (a) (c0))) (* v65 (* (b0) v66))) (* (* v64 (* (a) (a0))) (* v65 (* (d0) v66))))))
(37 (resolve 35 (1) 36 (1)) ((not (= (* (* v64 (* (a) (c0))) v3) (* (* v64 (* (a) (a0))) (* v65 (* (d0) v66))))) (= (* v65 (* (b0) v66)) v3)))
(38 (instantiate 37 ((v3 . v1)(v64 . v0)(v65 . v2)(v66 . v3))) ((not (= (* (* v0 (* (a) (c0))) v1) (* (* v0 (* (a) (a0))) (* v2 (* (d0) v3))))) (= (* v2 (* (b0) v3)) v1)))
(39 (instantiate 38 ((v0 . (* v64 v68))(v1 . (* (* v68 (a0)) (* (d0) v3)))(v2 . (* v68 (c0))))) ((not (= (* (* (* v64 v68) (* (a) (c0))) (* (* v68 (a0)) (* (d0) v3))) (* (* (* v64 v68) (* (a) (a0))) (* (* v68 (c0)) (* (d0) v3))))) (= (* (* v68 (c0)) (* (b0) v3)) (* (* v68 (a0)) (* (d0) v3)))))
(40 (instantiate 29 ((v0 . v64)(v1 . v68)(v2 . (a))(v3 . (c0))(v4 . v68)(v5 . (a0))(v6 . (* (d0) v3)))) ((= (* (* (* v64 v68) (* (a) (c0))) (* (* v68 (a0)) (* (d0) v3))) (* (* (* v64 v68) (* (a) (a0))) (* (* v68 (c0)) (* (d0) v3))))))
(41 (resolve 39 (1) 40 (1)) ((= (* (* v68 (c0)) (* (b0) v3)) (* (* v68 (a0)) (* (d0) v3)))))
(42 (instantiate 41 ((v3 . v1)(v68 . v0))) ((= (* (* v0 (c0)) (* (b0) v1)) (* (* v0 (a0)) (* (d0) v1)))))
(43 (instantiate 3 ((v0 . (* (d) v64))(v1 . (* (b0) v65))(v2 . (* (* (c) (a0)) (* v64 v65))))) ((not (= (* (* (d) v64) (* (b0) v65)) (* (* (c) (a0)) (* v64 v65)))) (not (= (* v3 (* (b0) v65)) (* (* (c) (a0)) (* v64 v65)))) (= (* (d) v64) v3)))
(44 (instantiate 19 ((v0 . v64)(v1 . v65))) ((= (* (* (d) v64) (* (b0) v65)) (* (* (c) (a0)) (* v64 v65)))))
(45 (resolve 43 (1) 44 (1)) ((not (= (* v3 (* (b0) v65)) (* (* (c) (a0)) (* v64 v65)))) (= (* (d) v64) v3)))
(46 (instantiate 45 ((v3 . v0)(v64 . v2)(v65 . v1))) ((not (= (* v0 (* (b0) v1)) (* (* (c) (a0)) (* v2 v1)))) (= (* (d) v2) v0)))
(47 (instantiate 46 ((v0 . (* (c) (c0)))(v1 . v65)(v2 . (d0)))) ((not (= (* (* (c) (c0)) (* (b0) v65)) (* (* (c) (a0)) (* (d0) v65)))) (= (* (d) (d0)) (* (c) (c0)))))
(48 (instantiate 42 ((v0 . (c))(v1 . v65))) ((= (* (* (c) (c0)) (* (b0) v65)) (* (* (c) (a0)) (* (d0) v65)))))
(49 (resolve 47 (1) 48 (1)) ((= (* (d) (d0)) (* (c) (c0)))))
(50 (resolve 1 (1) 49 (1)) ())
)