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