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