;; ----- Otter 3.0.4, August 1995 -----
;; The job was started by mccune on gyro, Thu Nov  2 00:20:18 1995
;;
;;;; x=x.
;;;; x*x=x.
;;;; (x*y)*x=y.
;;;; (((A*A)*B)*A)* (C*B)!=C.
;;
;; ----> UNIT CONFLICT at   0.03 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)) (A)) (* (C) (B))) (C)))))
(4 (instantiate 1 ((v0 . (A)))) ((= (* (A) (A)) (A))))
(5 (paramod 4 (1 1) 3 (1 1 1 1 1 1)) ((not (= (* (* (* (A) (B)) (A)) (* (C) (B))) (C)))))
(6 (instantiate 2 ((v0 . (A))(v1 . (B)))) ((= (* (* (A) (B)) (A)) (B))))
(7 (paramod 6 (1 1) 5 (1 1 1 1)) ((not (= (* (B) (* (C) (B))) (C)))))
(8 (instantiate 2 ((v0 . v65))) ((= (* (* v65 v1) v65) v1)))
(9 (instantiate 2 ((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 11 ((v0 . (B))(v1 . (C)))) ((= (* (B) (* (C) (B))) (C))))
(13 (resolve 7 (1) 12 (1)) ())
)