;; ----- Otter 3.0.4, August 1995 -----
;; The job was started by mccune on gyro, Wed Nov  1 22:43:40 1995
;;
;;;; 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^ (y v z)) v (x^y)=x^ (y v z).
;;;; (x v (y^z))^ (x v y)=x v (y^z).
;;;; x^ (y v z)= (x^y) v (x^z).
;;;; A v (B^C)!= (A v B)^ (A v C).
;;
;; ----> UNIT CONFLICT at   7.28 sec ----> 1442 [binary,1440.1,163.1] $F.
;;
(
(1 (input) ((= (^ v0 v0) v0)))
(2 (input) ((= (^ v0 v1) (^ v1 v0))))
(3 (input) ((= (^ (^ v0 v1) v2) (^ v0 (^ v1 v2)))))
(4 (input) ((= (v v0 v0) v0)))
(5 (input) ((= (v v0 v1) (v v1 v0))))
(6 (input) ((= (v (v v0 v1) v2) (v v0 (v v1 v2)))))
(7 (input) ((= (^ (v v0 (^ v1 v2)) (v v0 v1)) (v v0 (^ v1 v2)))))
(8 (input) ((= (^ v0 (v v1 v2)) (v (^ v0 v1) (^ v0 v2)))))
(9 (flip 8 (1)) ((= (v (^ v0 v1) (^ v0 v2)) (^ v0 (v v1 v2)))))
(10 (input) ((not (= (v (A) (^ (B) (C))) (^ (v (A) (B)) (v (A) (C)))))))
(11 (instantiate 1 ((v0 . v65))) ((= (^ v65 v65) v65)))
(12 (instantiate 3 ((v0 . v65)(v1 . v65)(v2 . v66))) ((= (^ (^ v65 v65) v66) (^ v65 (^ v65 v66)))))
(13 (paramod 11 (1 1) 12 (1 1 1)) ((= (^ v65 v66) (^ v65 (^ v65 v66)))))
(14 (flip 13 (1)) ((= (^ v65 (^ v65 v66)) (^ v65 v66))))
(15 (instantiate 14 ((v65 . v0)(v66 . v1))) ((= (^ v0 (^ v0 v1)) (^ v0 v1))))
(16 (instantiate 4 ((v0 . v65))) ((= (v v65 v65) v65)))
(17 (instantiate 6 ((v0 . v65)(v1 . v65)(v2 . v66))) ((= (v (v v65 v65) v66) (v v65 (v v65 v66)))))
(18 (paramod 16 (1 1) 17 (1 1 1)) ((= (v v65 v66) (v v65 (v v65 v66)))))
(19 (flip 18 (1)) ((= (v v65 (v v65 v66)) (v v65 v66))))
(20 (instantiate 19 ((v65 . v0)(v66 . v1))) ((= (v v0 (v v0 v1)) (v v0 v1))))
(21 (instantiate 5 ((v0 . v64)(v1 . v65))) ((= (v v64 v65) (v v65 v64))))
(22 (instantiate 20 ((v0 . v64)(v1 . v65))) ((= (v v64 (v v64 v65)) (v v64 v65))))
(23 (paramod 21 (1 1) 22 (1 1 2)) ((= (v v64 (v v65 v64)) (v v64 v65))))
(24 (instantiate 23 ((v64 . v0)(v65 . v1))) ((= (v v0 (v v1 v0)) (v v0 v1))))
(25 (instantiate 24 ((v0 . v64))) ((= (v v64 (v v1 v64)) (v v64 v1))))
(26 (instantiate 6 ((v0 . v64)(v1 . (v v1 v64))(v2 . v66))) ((= (v (v v64 (v v1 v64)) v66) (v v64 (v (v v1 v64) v66)))))
(27 (paramod 25 (1 1) 26 (1 1 1)) ((= (v (v v64 v1) v66) (v v64 (v (v v1 v64) v66)))))
(28 (instantiate 6 ((v0 . v64)(v1 . v1)(v2 . v66))) ((= (v (v v64 v1) v66) (v v64 (v v1 v66)))))
(29 (paramod 28 (1 1) 27 (1 1)) ((= (v v64 (v v1 v66)) (v v64 (v (v v1 v64) v66)))))
(30 (instantiate 6 ((v0 . v1)(v1 . v64)(v2 . v66))) ((= (v (v v1 v64) v66) (v v1 (v v64 v66)))))
(31 (paramod 30 (1 1) 29 (1 2 2)) ((= (v v64 (v v1 v66)) (v v64 (v v1 (v v64 v66))))))
(32 (flip 31 (1)) ((= (v v64 (v v1 (v v64 v66))) (v v64 (v v1 v66)))))
(33 (instantiate 32 ((v64 . v0)(v66 . v2))) ((= (v v0 (v v1 (v v0 v2))) (v v0 (v v1 v2)))))
(34 (instantiate 20 ((v0 . v64))) ((= (v v64 (v v64 v1)) (v v64 v1))))
(35 (instantiate 7 ((v0 . v64)(v1 . (v v64 v1))(v2 . v66))) ((= (^ (v v64 (^ (v v64 v1) v66)) (v v64 (v v64 v1))) (v v64 (^ (v v64 v1) v66)))))
(36 (paramod 34 (1 1) 35 (1 1 2)) ((= (^ (v v64 (^ (v v64 v1) v66)) (v v64 v1)) (v v64 (^ (v v64 v1) v66)))))
(37 (instantiate 36 ((v64 . v0)(v66 . v2))) ((= (^ (v v0 (^ (v v0 v1) v2)) (v v0 v1)) (v v0 (^ (v v0 v1) v2)))))
(38 (instantiate 1 ((v0 . v65))) ((= (^ v65 v65) v65)))
(39 (instantiate 9 ((v0 . v65)(v1 . v65)(v2 . v66))) ((= (v (^ v65 v65) (^ v65 v66)) (^ v65 (v v65 v66)))))
(40 (paramod 38 (1 1) 39 (1 1 1)) ((= (v v65 (^ v65 v66)) (^ v65 (v v65 v66)))))
(41 (instantiate 40 ((v65 . v0)(v66 . v1))) ((= (v v0 (^ v0 v1)) (^ v0 (v v0 v1)))))
(42 (instantiate 15 ((v0 . v64))) ((= (^ v64 (^ v64 v1)) (^ v64 v1))))
(43 (instantiate 9 ((v0 . v64)(v1 . v65)(v2 . (^ v64 v1)))) ((= (v (^ v64 v65) (^ v64 (^ v64 v1))) (^ v64 (v v65 (^ v64 v1))))))
(44 (paramod 42 (1 1) 43 (1 1 2)) ((= (v (^ v64 v65) (^ v64 v1)) (^ v64 (v v65 (^ v64 v1))))))
(45 (instantiate 9 ((v0 . v64)(v1 . v65)(v2 . v1))) ((= (v (^ v64 v65) (^ v64 v1)) (^ v64 (v v65 v1)))))
(46 (paramod 45 (1 1) 44 (1 1)) ((= (^ v64 (v v65 v1)) (^ v64 (v v65 (^ v64 v1))))))
(47 (flip 46 (1)) ((= (^ v64 (v v65 (^ v64 v1))) (^ v64 (v v65 v1)))))
(48 (instantiate 47 ((v1 . v2)(v64 . v0)(v65 . v1))) ((= (^ v0 (v v1 (^ v0 v2))) (^ v0 (v v1 v2)))))
(49 (instantiate 1 ((v0 . v66))) ((= (^ v66 v66) v66)))
(50 (instantiate 9 ((v0 . v66)(v1 . v65)(v2 . v66))) ((= (v (^ v66 v65) (^ v66 v66)) (^ v66 (v v65 v66)))))
(51 (paramod 49 (1 1) 50 (1 1 2)) ((= (v (^ v66 v65) v66) (^ v66 (v v65 v66)))))
(52 (instantiate 51 ((v65 . v1)(v66 . v0))) ((= (v (^ v0 v1) v0) (^ v0 (v v1 v0)))))
(53 (instantiate 5 ((v0 . (^ v64 v65))(v1 . (^ v64 v66)))) ((= (v (^ v64 v65) (^ v64 v66)) (v (^ v64 v66) (^ v64 v65)))))
(54 (instantiate 9 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (v (^ v64 v65) (^ v64 v66)) (^ v64 (v v65 v66)))))
(55 (paramod 53 (1 1) 54 (1 1)) ((= (v (^ v64 v66) (^ v64 v65)) (^ v64 (v v65 v66)))))
(56 (instantiate 9 ((v0 . v64)(v1 . v66)(v2 . v65))) ((= (v (^ v64 v66) (^ v64 v65)) (^ v64 (v v66 v65)))))
(57 (paramod 56 (1 1) 55 (1 1)) ((= (^ v64 (v v66 v65)) (^ v64 (v v65 v66)))))
(58 (instantiate 57 ((v64 . v0)(v65 . v2)(v66 . v1))) ((= (^ v0 (v v1 v2)) (^ v0 (v v2 v1)))))
(59 (instantiate 2 ((v0 . (B))(v1 . (C)))) ((= (^ (B) (C)) (^ (C) (B)))))
(60 (paramod 59 (1 1) 10 (1 1 1 2)) ((not (= (v (A) (^ (C) (B))) (^ (v (A) (B)) (v (A) (C)))))))
(61 (instantiate 41 ((v0 . (v v0 (^ v1 v2)))(v1 . (v v0 v1)))) ((= (v (v v0 (^ v1 v2)) (^ (v v0 (^ v1 v2)) (v v0 v1))) (^ (v v0 (^ v1 v2)) (v (v v0 (^ v1 v2)) (v v0 v1))))))
(62 (paramod 7 (1 1) 61 (1 1 2)) ((= (v (v v0 (^ v1 v2)) (v v0 (^ v1 v2))) (^ (v v0 (^ v1 v2)) (v (v v0 (^ v1 v2)) (v v0 v1))))))
(63 (instantiate 4 ((v0 . (v v0 (^ v1 v2))))) ((= (v (v v0 (^ v1 v2)) (v v0 (^ v1 v2))) (v v0 (^ v1 v2)))))
(64 (paramod 63 (1 1) 62 (1 1)) ((= (v v0 (^ v1 v2)) (^ (v v0 (^ v1 v2)) (v (v v0 (^ v1 v2)) (v v0 v1))))))
(65 (instantiate 6 ((v0 . v0)(v1 . (^ v1 v2))(v2 . (v v0 v1)))) ((= (v (v v0 (^ v1 v2)) (v v0 v1)) (v v0 (v (^ v1 v2) (v v0 v1))))))
(66 (paramod 65 (1 1) 64 (1 2 2)) ((= (v v0 (^ v1 v2)) (^ (v v0 (^ v1 v2)) (v v0 (v (^ v1 v2) (v v0 v1)))))))
(67 (instantiate 33 ((v0 . v0)(v1 . (^ v1 v2))(v2 . v1))) ((= (v v0 (v (^ v1 v2) (v v0 v1))) (v v0 (v (^ v1 v2) v1)))))
(68 (paramod 67 (1 1) 66 (1 2 2)) ((= (v v0 (^ v1 v2)) (^ (v v0 (^ v1 v2)) (v v0 (v (^ v1 v2) v1))))))
(69 (instantiate 52 ((v0 . v1)(v1 . v2))) ((= (v (^ v1 v2) v1) (^ v1 (v v2 v1)))))
(70 (paramod 69 (1 1) 68 (1 2 2 2)) ((= (v v0 (^ v1 v2)) (^ (v v0 (^ v1 v2)) (v v0 (^ v1 (v v2 v1)))))))
(71 (flip 70 (1)) ((= (^ (v v0 (^ v1 v2)) (v v0 (^ v1 (v v2 v1)))) (v v0 (^ v1 v2)))))
(72 (instantiate 2 ((v0 . v64)(v1 . v65))) ((= (^ v64 v65) (^ v65 v64))))
(73 (instantiate 41 ((v0 . v64)(v1 . v65))) ((= (v v64 (^ v64 v65)) (^ v64 (v v64 v65)))))
(74 (paramod 72 (1 1) 73 (1 1 2)) ((= (v v64 (^ v65 v64)) (^ v64 (v v64 v65)))))
(75 (instantiate 74 ((v64 . v0)(v65 . v1))) ((= (v v0 (^ v1 v0)) (^ v0 (v v0 v1)))))
(76 (instantiate 2 ((v0 . v64)(v1 . (v v65 v66)))) ((= (^ v64 (v v65 v66)) (^ (v v65 v66) v64))))
(77 (instantiate 58 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (^ v64 (v v65 v66)) (^ v64 (v v66 v65)))))
(78 (paramod 76 (1 1) 77 (1 1)) ((= (^ (v v65 v66) v64) (^ v64 (v v66 v65)))))
(79 (instantiate 78 ((v64 . v2)(v65 . v0)(v66 . v1))) ((= (^ (v v0 v1) v2) (^ v2 (v v1 v0)))))
(80 (flip 79 (1)) ((= (^ v2 (v v1 v0)) (^ (v v0 v1) v2))))
(81 (instantiate 2 ((v0 . v64)(v1 . (v v65 (^ v64 v66))))) ((= (^ v64 (v v65 (^ v64 v66))) (^ (v v65 (^ v64 v66)) v64))))
(82 (instantiate 48 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (^ v64 (v v65 (^ v64 v66))) (^ v64 (v v65 v66)))))
(83 (paramod 81 (1 1) 82 (1 1)) ((= (^ (v v65 (^ v64 v66)) v64) (^ v64 (v v65 v66)))))
(84 (instantiate 83 ((v64 . v1)(v65 . v0)(v66 . v2))) ((= (^ (v v0 (^ v1 v2)) v1) (^ v1 (v v0 v2)))))
(85 (instantiate 84 ((v0 . v0)(v1 . (v v0 v1))(v2 . v2))) ((= (^ (v v0 (^ (v v0 v1) v2)) (v v0 v1)) (^ (v v0 v1) (v v0 v2)))))
(86 (paramod 85 (1 1) 37 (1 1)) ((= (^ (v v0 v1) (v v0 v2)) (v v0 (^ (v v0 v1) v2)))))
(87 (flip 86 (1)) ((= (v v0 (^ (v v0 v1) v2)) (^ (v v0 v1) (v v0 v2)))))
(88 (instantiate 48 ((v0 . v65))) ((= (^ v65 (v v1 (^ v65 v2))) (^ v65 (v v1 v2)))))
(89 (instantiate 75 ((v0 . (v v1 (^ v65 v2)))(v1 . v65))) ((= (v (v v1 (^ v65 v2)) (^ v65 (v v1 (^ v65 v2)))) (^ (v v1 (^ v65 v2)) (v (v v1 (^ v65 v2)) v65)))))
(90 (paramod 88 (1 1) 89 (1 1 2)) ((= (v (v v1 (^ v65 v2)) (^ v65 (v v1 v2))) (^ (v v1 (^ v65 v2)) (v (v v1 (^ v65 v2)) v65)))))
(91 (instantiate 6 ((v0 . v1)(v1 . (^ v65 v2))(v2 . (^ v65 (v v1 v2))))) ((= (v (v v1 (^ v65 v2)) (^ v65 (v v1 v2))) (v v1 (v (^ v65 v2) (^ v65 (v v1 v2)))))))
(92 (paramod 91 (1 1) 90 (1 1)) ((= (v v1 (v (^ v65 v2) (^ v65 (v v1 v2)))) (^ (v v1 (^ v65 v2)) (v (v v1 (^ v65 v2)) v65)))))
(93 (instantiate 9 ((v0 . v65)(v1 . v2)(v2 . (v v1 v2)))) ((= (v (^ v65 v2) (^ v65 (v v1 v2))) (^ v65 (v v2 (v v1 v2))))))
(94 (paramod 93 (1 1) 92 (1 1 2)) ((= (v v1 (^ v65 (v v2 (v v1 v2)))) (^ (v v1 (^ v65 v2)) (v (v v1 (^ v65 v2)) v65)))))
(95 (instantiate 24 ((v0 . v2)(v1 . v1))) ((= (v v2 (v v1 v2)) (v v2 v1))))
(96 (paramod 95 (1 1) 94 (1 1 2 2)) ((= (v v1 (^ v65 (v v2 v1))) (^ (v v1 (^ v65 v2)) (v (v v1 (^ v65 v2)) v65)))))
(97 (instantiate 6 ((v0 . v1)(v1 . (^ v65 v2))(v2 . v65))) ((= (v (v v1 (^ v65 v2)) v65) (v v1 (v (^ v65 v2) v65)))))
(98 (paramod 97 (1 1) 96 (1 2 2)) ((= (v v1 (^ v65 (v v2 v1))) (^ (v v1 (^ v65 v2)) (v v1 (v (^ v65 v2) v65))))))
(99 (instantiate 52 ((v0 . v65)(v1 . v2))) ((= (v (^ v65 v2) v65) (^ v65 (v v2 v65)))))
(100 (paramod 99 (1 1) 98 (1 2 2 2)) ((= (v v1 (^ v65 (v v2 v1))) (^ (v v1 (^ v65 v2)) (v v1 (^ v65 (v v2 v65)))))))
(101 (instantiate 71 ((v0 . v1)(v1 . v65)(v2 . v2))) ((= (^ (v v1 (^ v65 v2)) (v v1 (^ v65 (v v2 v65)))) (v v1 (^ v65 v2)))))
(102 (paramod 101 (1 1) 100 (1 2)) ((= (v v1 (^ v65 (v v2 v1))) (v v1 (^ v65 v2)))))
(103 (instantiate 102 ((v1 . v0)(v65 . v1))) ((= (v v0 (^ v1 (v v2 v0))) (v v0 (^ v1 v2)))))
(104 (instantiate 80 ((v0 . v64)(v1 . v66)(v2 . v65))) ((= (^ v65 (v v66 v64)) (^ (v v64 v66) v65))))
(105 (instantiate 103 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (v v64 (^ v65 (v v66 v64))) (v v64 (^ v65 v66)))))
(106 (paramod 104 (1 1) 105 (1 1 2)) ((= (v v64 (^ (v v64 v66) v65)) (v v64 (^ v65 v66)))))
(107 (instantiate 87 ((v0 . v64)(v1 . v66)(v2 . v65))) ((= (v v64 (^ (v v64 v66) v65)) (^ (v v64 v66) (v v64 v65)))))
(108 (paramod 107 (1 1) 106 (1 1)) ((= (^ (v v64 v66) (v v64 v65)) (v v64 (^ v65 v66)))))
(109 (flip 108 (1)) ((= (v v64 (^ v65 v66)) (^ (v v64 v66) (v v64 v65)))))
(110 (instantiate 109 ((v64 . v0)(v65 . v1)(v66 . v2))) ((= (v v0 (^ v1 v2)) (^ (v v0 v2) (v v0 v1)))))
(111 (instantiate 110 ((v0 . (A))(v1 . (C))(v2 . (B)))) ((= (v (A) (^ (C) (B))) (^ (v (A) (B)) (v (A) (C))))))
(112 (resolve 60 (1) 111 (1)) ())
)