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