;; ----- Otter 3.0.4, August 1995 -----
;; The job was started by mccune on gyro, Thu Nov  2 00:20:46 1995
;;
;;;; x=x.
;;;; x*y=y*x.
;;;; g(x)=x.
;;;; (x*y)*x=y.
;;;; (g(A)*B)* (C* (B*A))!=C.
;;
;; ----> UNIT CONFLICT at   0.09 sec ----> 16 [binary,15.1,1.1] $F.
;;
(
(1 (input) ((= v0 v0)))
(2 (input) ((= (* v0 v1) (* v1 v0))))
(3 (input) ((= (g v0) v0)))
(4 (input) ((= (* (* v0 v1) v0) v1)))
(5 (input) ((not (= (* (* (g (A)) (B)) (* (C) (* (B) (A)))) (C)))))
(6 (instantiate 3 ((v0 . (A)))) ((= (g (A)) (A))))
(7 (paramod 6 (1 1) 5 (1 1 1 1 1)) ((not (= (* (* (A) (B)) (* (C) (* (B) (A)))) (C)))))
(8 (instantiate 4 ((v0 . v65))) ((= (* (* v65 v1) v65) v1)))
(9 (instantiate 4 ((v0 . (* v65 v1))(v1 . v65))) ((= (* (* (* v65 v1) v65) (* v65 v1)) v65)))
(10 (paramod 8 (1 1) 9 (1 1 1)) ((= (* v1 (* v65 v1)) v65)))
(11 (instantiate 10 ((v1 . v0)(v65 . v1))) ((= (* v0 (* v1 v0)) v1)))
(12 (instantiate 2 ((v0 . (A))(v1 . (B)))) ((= (* (A) (B)) (* (B) (A)))))
(13 (paramod 12 (1 1) 7 (1 1 1 1)) ((not (= (* (* (B) (A)) (* (C) (* (B) (A)))) (C)))))
(14 (instantiate 11 ((v0 . (* (B) (A)))(v1 . (C)))) ((= (* (* (B) (A)) (* (C) (* (B) (A)))) (C))))
(15 (paramod 14 (1 1) 13 (1 1 1)) ((not (= (C) (C)))))
(16 (instantiate 1 ((v0 . (C)))) ((= (C) (C))))
(17 (resolve 15 (1) 16 (1)) ())
)