;; ----- Otter 3.0.4, August 1995 -----
;; The job was started by mccune on gyro, Sun Feb 11 18:48:46 1996
;;
;;;; x=x.
;;;; x^x=x.
;;;; x^y=y^x.
;;;; ((x v z)^ (y v z))^z=z.
;;;; x v x=x.
;;;; x v y=y v x.
;;;; ((x^z) v (y^z)) v z=z.
;;;; x*x=x.
;;;; x*y=y*x.
;;;; ((x v z)* (y v z))*z=z.
;;;; ((x*z) v (y*z)) v z=z.
;;;; A^B!=A*B.
;;
;; ----> UNIT CONFLICT at  13.99 sec ----> 1473 [binary,1471.1,19.1] $F.
;;
(
(1 (input) ((= (^ v0 v0) v0)))
(2 (input) ((= (^ v0 v1) (^ v1 v0))))
(3 (input) ((= (^ (^ (v v0 v1) (v v2 v1)) v1) v1)))
(4 (input) ((= (v v0 v0) v0)))
(5 (input) ((= (v v0 v1) (v v1 v0))))
(6 (input) ((= (v (v (^ v0 v1) (^ v2 v1)) v1) v1)))
(7 (input) ((= (* v0 v0) v0)))
(8 (input) ((= (* v0 v1) (* v1 v0))))
(9 (input) ((= (* (* (v v0 v1) (v v2 v1)) v1) v1)))
(10 (input) ((= (v (v (* v0 v1) (* v2 v1)) v1) v1)))
(11 (input) ((not (= (^ (A) (B)) (* (A) (B))))))
(12 (instantiate 1 ((v0 . (v v66 v65)))) ((= (^ (v v66 v65) (v v66 v65)) (v v66 v65))))
(13 (instantiate 3 ((v0 . v66)(v1 . v65)(v2 . v66))) ((= (^ (^ (v v66 v65) (v v66 v65)) v65) v65)))
(14 (paramod 12 (1 1) 13 (1 1 1)) ((= (^ (v v66 v65) v65) v65)))
(15 (instantiate 14 ((v65 . v1)(v66 . v0))) ((= (^ (v v0 v1) v1) v1)))
(16 (instantiate 5 ((v0 . v64)(v1 . v65))) ((= (v v64 v65) (v v65 v64))))
(17 (instantiate 15 ((v0 . v64)(v1 . v65))) ((= (^ (v v64 v65) v65) v65)))
(18 (paramod 16 (1 1) 17 (1 1 1)) ((= (^ (v v65 v64) v65) v65)))
(19 (instantiate 18 ((v64 . v1)(v65 . v0))) ((= (^ (v v0 v1) v0) v0)))
(20 (instantiate 2 ((v0 . (v v64 v65))(v1 . v65))) ((= (^ (v v64 v65) v65) (^ v65 (v v64 v65)))))
(21 (instantiate 15 ((v0 . v64)(v1 . v65))) ((= (^ (v v64 v65) v65) v65)))
(22 (paramod 20 (1 1) 21 (1 1)) ((= (^ v65 (v v64 v65)) v65)))
(23 (instantiate 22 ((v64 . v1)(v65 . v0))) ((= (^ v0 (v v1 v0)) v0)))
(24 (instantiate 4 ((v0 . (^ v66 v65)))) ((= (v (^ v66 v65) (^ v66 v65)) (^ v66 v65))))
(25 (instantiate 6 ((v0 . v66)(v1 . v65)(v2 . v66))) ((= (v (v (^ v66 v65) (^ v66 v65)) v65) v65)))
(26 (paramod 24 (1 1) 25 (1 1 1)) ((= (v (^ v66 v65) v65) v65)))
(27 (instantiate 26 ((v65 . v1)(v66 . v0))) ((= (v (^ v0 v1) v1) v1)))
(28 (instantiate 2 ((v0 . (v v64 v65))(v1 . v64))) ((= (^ (v v64 v65) v64) (^ v64 (v v64 v65)))))
(29 (instantiate 19 ((v0 . v64)(v1 . v65))) ((= (^ (v v64 v65) v64) v64)))
(30 (paramod 28 (1 1) 29 (1 1)) ((= (^ v64 (v v64 v65)) v64)))
(31 (instantiate 30 ((v64 . v0)(v65 . v1))) ((= (^ v0 (v v0 v1)) v0)))
(32 (instantiate 2 ((v0 . v64)(v1 . v65))) ((= (^ v64 v65) (^ v65 v64))))
(33 (instantiate 27 ((v0 . v64)(v1 . v65))) ((= (v (^ v64 v65) v65) v65)))
(34 (paramod 32 (1 1) 33 (1 1 1)) ((= (v (^ v65 v64) v65) v65)))
(35 (instantiate 34 ((v64 . v1)(v65 . v0))) ((= (v (^ v0 v1) v0) v0)))
(36 (instantiate 5 ((v0 . (^ v64 v65))(v1 . v65))) ((= (v (^ v64 v65) v65) (v v65 (^ v64 v65)))))
(37 (instantiate 27 ((v0 . v64)(v1 . v65))) ((= (v (^ v64 v65) v65) v65)))
(38 (paramod 36 (1 1) 37 (1 1)) ((= (v v65 (^ v64 v65)) v65)))
(39 (instantiate 38 ((v64 . v1)(v65 . v0))) ((= (v v0 (^ v1 v0)) v0)))
(40 (instantiate 7 ((v0 . (v v66 v65)))) ((= (* (v v66 v65) (v v66 v65)) (v v66 v65))))
(41 (instantiate 9 ((v0 . v66)(v1 . v65)(v2 . v66))) ((= (* (* (v v66 v65) (v v66 v65)) v65) v65)))
(42 (paramod 40 (1 1) 41 (1 1 1)) ((= (* (v v66 v65) v65) v65)))
(43 (instantiate 42 ((v65 . v1)(v66 . v0))) ((= (* (v v0 v1) v1) v1)))
(44 (instantiate 5 ((v0 . (^ v64 v65))(v1 . v64))) ((= (v (^ v64 v65) v64) (v v64 (^ v64 v65)))))
(45 (instantiate 35 ((v0 . v64)(v1 . v65))) ((= (v (^ v64 v65) v64) v64)))
(46 (paramod 44 (1 1) 45 (1 1)) ((= (v v64 (^ v64 v65)) v64)))
(47 (instantiate 46 ((v64 . v0)(v65 . v1))) ((= (v v0 (^ v0 v1)) v0)))
(48 (instantiate 31 ((v0 . v65))) ((= (^ v65 (v v65 v1)) v65)))
(49 (instantiate 39 ((v0 . (v v65 v1))(v1 . v65))) ((= (v (v v65 v1) (^ v65 (v v65 v1))) (v v65 v1))))
(50 (paramod 48 (1 1) 49 (1 1 2)) ((= (v (v v65 v1) v65) (v v65 v1))))
(51 (instantiate 50 ((v65 . v0))) ((= (v (v v0 v1) v0) (v v0 v1))))
(52 (instantiate 39 ((v0 . v66))) ((= (v v66 (^ v1 v66)) v66)))
(53 (instantiate 9 ((v0 . v64)(v1 . (^ v1 v66))(v2 . v66))) ((= (* (* (v v64 (^ v1 v66)) (v v66 (^ v1 v66))) (^ v1 v66)) (^ v1 v66))))
(54 (paramod 52 (1 1) 53 (1 1 1 2)) ((= (* (* (v v64 (^ v1 v66)) v66) (^ v1 v66)) (^ v1 v66))))
(55 (instantiate 54 ((v64 . v0)(v66 . v2))) ((= (* (* (v v0 (^ v1 v2)) v2) (^ v1 v2)) (^ v1 v2))))
(56 (instantiate 43 ((v1 . v65))) ((= (* (v v0 v65) v65) v65)))
(57 (instantiate 10 ((v0 . (v v0 v65))(v1 . v65)(v2 . v66))) ((= (v (v (* (v v0 v65) v65) (* v66 v65)) v65) v65)))
(58 (paramod 56 (1 1) 57 (1 1 1 1)) ((= (v (v v65 (* v66 v65)) v65) v65)))
(59 (instantiate 51 ((v0 . v65)(v1 . (* v66 v65)))) ((= (v (v v65 (* v66 v65)) v65) (v v65 (* v66 v65)))))
(60 (paramod 59 (1 1) 58 (1 1)) ((= (v v65 (* v66 v65)) v65)))
(61 (instantiate 60 ((v65 . v0)(v66 . v1))) ((= (v v0 (* v1 v0)) v0)))
(62 (instantiate 8 ((v0 . v65)(v1 . v64))) ((= (* v65 v64) (* v64 v65))))
(63 (instantiate 61 ((v0 . v64)(v1 . v65))) ((= (v v64 (* v65 v64)) v64)))
(64 (paramod 62 (1 1) 63 (1 1 2)) ((= (v v64 (* v64 v65)) v64)))
(65 (instantiate 64 ((v64 . v0)(v65 . v1))) ((= (v v0 (* v0 v1)) v0)))
(66 (instantiate 61 ((v0 . v66))) ((= (v v66 (* v1 v66)) v66)))
(67 (instantiate 3 ((v0 . v64)(v1 . (* v1 v66))(v2 . v66))) ((= (^ (^ (v v64 (* v1 v66)) (v v66 (* v1 v66))) (* v1 v66)) (* v1 v66))))
(68 (paramod 66 (1 1) 67 (1 1 1 2)) ((= (^ (^ (v v64 (* v1 v66)) v66) (* v1 v66)) (* v1 v66))))
(69 (instantiate 68 ((v64 . v0)(v66 . v2))) ((= (^ (^ (v v0 (* v1 v2)) v2) (* v1 v2)) (* v1 v2))))
(70 (instantiate 65 ((v0 . v65))) ((= (v v65 (* v65 v1)) v65)))
(71 (instantiate 23 ((v0 . (* v65 v1))(v1 . v65))) ((= (^ (* v65 v1) (v v65 (* v65 v1))) (* v65 v1))))
(72 (paramod 70 (1 1) 71 (1 1 2)) ((= (^ (* v65 v1) v65) (* v65 v1))))
(73 (instantiate 72 ((v65 . v0))) ((= (^ (* v0 v1) v0) (* v0 v1))))
(74 (instantiate 47 ((v0 . v65)(v1 . v66))) ((= (v v65 (^ v65 v66)) v65)))
(75 (instantiate 55 ((v0 . v65)(v1 . v65)(v2 . v66))) ((= (* (* (v v65 (^ v65 v66)) v66) (^ v65 v66)) (^ v65 v66))))
(76 (paramod 74 (1 1) 75 (1 1 1 1)) ((= (* (* v65 v66) (^ v65 v66)) (^ v65 v66))))
(77 (instantiate 76 ((v65 . v0)(v66 . v1))) ((= (* (* v0 v1) (^ v0 v1)) (^ v0 v1))))
(78 (instantiate 73 ((v0 . (* v0 v1))(v1 . (^ v0 v1)))) ((= (^ (* (* v0 v1) (^ v0 v1)) (* v0 v1)) (* (* v0 v1) (^ v0 v1)))))
(79 (paramod 77 (1 1) 78 (1 1 1)) ((= (^ (^ v0 v1) (* v0 v1)) (* (* v0 v1) (^ v0 v1)))))
(80 (paramod 77 (1 1) 79 (1 2)) ((= (^ (^ v0 v1) (* v0 v1)) (^ v0 v1))))
(81 (instantiate 65 ((v0 . v65)(v1 . v66))) ((= (v v65 (* v65 v66)) v65)))
(82 (instantiate 69 ((v0 . v65)(v1 . v65)(v2 . v66))) ((= (^ (^ (v v65 (* v65 v66)) v66) (* v65 v66)) (* v65 v66))))
(83 (paramod 81 (1 1) 82 (1 1 1 1)) ((= (^ (^ v65 v66) (* v65 v66)) (* v65 v66))))
(84 (instantiate 80 ((v0 . v65)(v1 . v66))) ((= (^ (^ v65 v66) (* v65 v66)) (^ v65 v66))))
(85 (paramod 84 (1 1) 83 (1 1)) ((= (^ v65 v66) (* v65 v66))))
(86 (instantiate 85 ((v65 . v0)(v66 . v1))) ((= (^ v0 v1) (* v0 v1))))
(87 (instantiate 86 ((v0 . (A))(v1 . (B)))) ((= (^ (A) (B)) (* (A) (B)))))
(88 (resolve 11 (1) 87 (1)) ())
)