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