;; ----- Otter 3.0.4, August 1995 -----
;; The job was started by mccune on gyro, Wed Nov  1 22:01:45 1995
;;
;;;; x=x.
;;;; (x*y)*z=x* (y*z).
;;;; e*x=x.
;;;; x*e=x.
;;;; x@ *x=e.
;;;; x*x@ =e.
;;;; (x*y)@ =y@ *x@ .
;;;; x@ * (x*y)=y.
;;;; x* (x@ *y)=y.
;;;; e@ =e.
;;;; x@ @ =x.
;;;; a*a0=b*b0.
;;;; c*a0=d*b0.
;;;; a*c0=b*d0.
;;;; d*d0!=c*c0.
;;
;; ----> UNIT CONFLICT at   0.35 sec ----> 116 [binary,114.1,1.1] $F.
;;
(
(1 (input) ((not (= (* (d) (d0)) (* (c) (c0))))))
(2 (input) ((= (* (* v0 v1) v2) (* v0 (* v1 v2)))))
(3 (input) ((= (* (@ v0) (* v0 v1)) v1)))
(4 (input) ((= (* v0 (* (@ v0) v1)) v1)))
(5 (input) ((= (* (a) (a0)) (* (b) (b0)))))
(6 (flip 5 (1)) ((= (* (b) (b0)) (* (a) (a0)))))
(7 (input) ((= (* (c) (a0)) (* (d) (b0)))))
(8 (flip 7 (1)) ((= (* (d) (b0)) (* (c) (a0)))))
(9 (input) ((= (* (a) (c0)) (* (b) (d0)))))
(10 (flip 9 (1)) ((= (* (b) (d0)) (* (a) (c0)))))
(11 (instantiate 2 ((v0 . (b))(v1 . (b0))(v2 . v66))) ((= (* (* (b) (b0)) v66) (* (b) (* (b0) v66)))))
(12 (paramod 6 (1 1) 11 (1 1 1)) ((= (* (* (a) (a0)) v66) (* (b) (* (b0) v66)))))
(13 (instantiate 2 ((v0 . (a))(v1 . (a0))(v2 . v66))) ((= (* (* (a) (a0)) v66) (* (a) (* (a0) v66)))))
(14 (paramod 13 (1 1) 12 (1 1)) ((= (* (a) (* (a0) v66)) (* (b) (* (b0) v66)))))
(15 (flip 14 (1)) ((= (* (b) (* (b0) v66)) (* (a) (* (a0) v66)))))
(16 (instantiate 15 ((v66 . v0))) ((= (* (b) (* (b0) v0)) (* (a) (* (a0) v0)))))
(17 (instantiate 2 ((v0 . (d))(v1 . (b0))(v2 . v66))) ((= (* (* (d) (b0)) v66) (* (d) (* (b0) v66)))))
(18 (paramod 8 (1 1) 17 (1 1 1)) ((= (* (* (c) (a0)) v66) (* (d) (* (b0) v66)))))
(19 (instantiate 2 ((v0 . (c))(v1 . (a0))(v2 . v66))) ((= (* (* (c) (a0)) v66) (* (c) (* (a0) v66)))))
(20 (paramod 19 (1 1) 18 (1 1)) ((= (* (c) (* (a0) v66)) (* (d) (* (b0) v66)))))
(21 (flip 20 (1)) ((= (* (d) (* (b0) v66)) (* (c) (* (a0) v66)))))
(22 (instantiate 21 ((v66 . v0))) ((= (* (d) (* (b0) v0)) (* (c) (* (a0) v0)))))
(23 (instantiate 3 ((v0 . (b))(v1 . (d0)))) ((= (* (@ (b)) (* (b) (d0))) (d0))))
(24 (paramod 10 (1 1) 23 (1 1 2)) ((= (* (@ (b)) (* (a) (c0))) (d0))))
(25 (instantiate 3 ((v0 . (b))(v1 . (* (b0) v0)))) ((= (* (@ (b)) (* (b) (* (b0) v0))) (* (b0) v0))))
(26 (paramod 16 (1 1) 25 (1 1 2)) ((= (* (@ (b)) (* (a) (* (a0) v0))) (* (b0) v0))))
(27 (instantiate 4 ((v0 . (a0)))) ((= (* (a0) (* (@ (a0)) v1)) v1)))
(28 (instantiate 26 ((v0 . (* (@ (a0)) v1)))) ((= (* (@ (b)) (* (a) (* (a0) (* (@ (a0)) v1)))) (* (b0) (* (@ (a0)) v1)))))
(29 (paramod 27 (1 1) 28 (1 1 2 2)) ((= (* (@ (b)) (* (a) v1)) (* (b0) (* (@ (a0)) v1)))))
(30 (instantiate 29 ((v1 . v0))) ((= (* (@ (b)) (* (a) v0)) (* (b0) (* (@ (a0)) v0)))))
(31 (instantiate 30 ((v0 . (c0)))) ((= (* (@ (b)) (* (a) (c0))) (* (b0) (* (@ (a0)) (c0))))))
(32 (paramod 31 (1 1) 24 (1 1)) ((= (* (b0) (* (@ (a0)) (c0))) (d0))))
(33 (instantiate 22 ((v0 . (* (@ (a0)) (c0))))) ((= (* (d) (* (b0) (* (@ (a0)) (c0)))) (* (c) (* (a0) (* (@ (a0)) (c0)))))))
(34 (paramod 32 (1 1) 33 (1 1 2)) ((= (* (d) (d0)) (* (c) (* (a0) (* (@ (a0)) (c0)))))))
(35 (instantiate 4 ((v0 . (a0))(v1 . (c0)))) ((= (* (a0) (* (@ (a0)) (c0))) (c0))))
(36 (paramod 35 (1 1) 34 (1 2 2)) ((= (* (d) (d0)) (* (c) (c0)))))
(37 (resolve 1 (1) 36 (1)) ())
)