;; ----- Otter 3.0.4, August 1995 -----
;; The job was started by mccune on gyro, Sun Feb 11 18:47:32 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.
;;;; 0^x=0.
;;;; 0 v x=x.
;;;; 1^x=x.
;;;; 1 v x=1.
;;;; x^x=x.
;;;; x v x=x.
;;;; (x^y) v (x^z)=x^ (y v (x^z)).
;;;; C1 v (A v B)=1.
;;;; C1^ (A v B)=0.
;;;; C2 v (A^B)=1.
;;;; C2^ (A^B)=0.
;;;; C1 v (A^C2)=D.
;;;; C1 v (B^C2)=E.
;;;; D^E!=C1.
;;
;; ----> UNIT CONFLICT at  23.51 sec ----> 4974 [binary,4972.1,39.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) ((= (v (v v0 v1) v2) (v v0 (v v1 v2)))))
(5 (input) ((= (^ v0 (v v0 v1)) v0)))
(6 (input) ((= (v v0 (^ v0 v1)) v0)))
(7 (input) ((= (^ (0) v0) (0))))
(8 (input) ((= (v (0) v0) v0)))
(9 (input) ((= (^ (1) v0) v0)))
(10 (input) ((= (v (^ v0 v1) (^ v0 v2)) (^ v0 (v v1 (^ v0 v2))))))
(11 (input) ((= (^ (C1) (v (A) (B))) (0))))
(12 (input) ((= (v (C2) (^ (A) (B))) (1))))
(13 (input) ((= (^ (C2) (^ (A) (B))) (0))))
(14 (input) ((= (v (C1) (^ (A) (C2))) (D))))
(15 (input) ((= (v (C1) (^ (B) (C2))) (E))))
(16 (input) ((not (= (^ (D) (E)) (C1)))))
(17 (instantiate 1 ((v0 . (D))(v1 . (E)))) ((= (^ (D) (E)) (^ (E) (D)))))
(18 (paramod 17 (1 1) 16 (1 1 1)) ((not (= (^ (E) (D)) (C1)))))
(19 (instantiate 1 ((v0 . (B))(v1 . (C2)))) ((= (^ (B) (C2)) (^ (C2) (B)))))
(20 (paramod 19 (1 1) 15 (1 1 2)) ((= (v (C1) (^ (C2) (B))) (E))))
(21 (instantiate 1 ((v0 . (C1))(v1 . (v (A) (B))))) ((= (^ (C1) (v (A) (B))) (^ (v (A) (B)) (C1)))))
(22 (paramod 21 (1 1) 11 (1 1)) ((= (^ (v (A) (B)) (C1)) (0))))
(23 (instantiate 2 ((v0 . (C1))(v1 . (v (A) (B)))(v2 . v66))) ((= (^ (^ (C1) (v (A) (B))) v66) (^ (C1) (^ (v (A) (B)) v66)))))
(24 (paramod 11 (1 1) 23 (1 1 1)) ((= (^ (0) v66) (^ (C1) (^ (v (A) (B)) v66)))))
(25 (instantiate 7 ((v0 . v66))) ((= (^ (0) v66) (0))))
(26 (paramod 25 (1 1) 24 (1 1)) ((= (0) (^ (C1) (^ (v (A) (B)) v66)))))
(27 (flip 26 (1)) ((= (^ (C1) (^ (v (A) (B)) v66)) (0))))
(28 (instantiate 27 ((v66 . v0))) ((= (^ (C1) (^ (v (A) (B)) v0)) (0))))
(29 (instantiate 1 ((v0 . (^ v64 v65))(v1 . v66))) ((= (^ (^ v64 v65) v66) (^ v66 (^ v64 v65)))))
(30 (instantiate 2 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (^ (^ v64 v65) v66) (^ v64 (^ v65 v66)))))
(31 (paramod 29 (1 1) 30 (1 1)) ((= (^ v66 (^ v64 v65)) (^ v64 (^ v65 v66)))))
(32 (instantiate 31 ((v64 . v1)(v65 . v2)(v66 . v0))) ((= (^ v0 (^ v1 v2)) (^ v1 (^ v2 v0)))))
(33 (flip 32 (1)) ((= (^ v1 (^ v2 v0)) (^ v0 (^ v1 v2)))))
(34 (instantiate 1 ((v0 . (A))(v1 . (B)))) ((= (^ (A) (B)) (^ (B) (A)))))
(35 (paramod 34 (1 1) 12 (1 1 2)) ((= (v (C2) (^ (B) (A))) (1))))
(36 (instantiate 1 ((v0 . (C2))(v1 . (^ (A) (B))))) ((= (^ (C2) (^ (A) (B))) (^ (^ (A) (B)) (C2)))))
(37 (paramod 36 (1 1) 13 (1 1)) ((= (^ (^ (A) (B)) (C2)) (0))))
(38 (instantiate 2 ((v0 . (A))(v1 . (B))(v2 . (C2)))) ((= (^ (^ (A) (B)) (C2)) (^ (A) (^ (B) (C2))))))
(39 (paramod 38 (1 1) 37 (1 1)) ((= (^ (A) (^ (B) (C2))) (0))))
(40 (instantiate 3 ((v0 . (C1))(v1 . (^ (A) (C2))))) ((= (v (C1) (^ (A) (C2))) (v (^ (A) (C2)) (C1)))))
(41 (paramod 14 (1 1) 40 (1 1)) ((= (D) (v (^ (A) (C2)) (C1)))))
(42 (flip 41 (1)) ((= (v (^ (A) (C2)) (C1)) (D))))
(43 (instantiate 5 ((v0 . (C1))(v1 . (^ (C2) (B))))) ((= (^ (C1) (v (C1) (^ (C2) (B)))) (C1))))
(44 (paramod 20 (1 1) 43 (1 1 2)) ((= (^ (C1) (E)) (C1))))
(45 (instantiate 1 ((v0 . v64)(v1 . (v v64 v65)))) ((= (^ v64 (v v64 v65)) (^ (v v64 v65) v64))))
(46 (instantiate 5 ((v0 . v64)(v1 . v65))) ((= (^ v64 (v v64 v65)) v64)))
(47 (paramod 45 (1 1) 46 (1 1)) ((= (^ (v v64 v65) v64) v64)))
(48 (instantiate 47 ((v64 . v0)(v65 . v1))) ((= (^ (v v0 v1) v0) v0)))
(49 (instantiate 5 ((v0 . v64))) ((= (^ v64 (v v64 v1)) v64)))
(50 (instantiate 2 ((v0 . v64)(v1 . (v v64 v1))(v2 . v66))) ((= (^ (^ v64 (v v64 v1)) v66) (^ v64 (^ (v v64 v1) v66)))))
(51 (paramod 49 (1 1) 50 (1 1 1)) ((= (^ v64 v66) (^ v64 (^ (v v64 v1) v66)))))
(52 (flip 51 (1)) ((= (^ v64 (^ (v v64 v1) v66)) (^ v64 v66))))
(53 (instantiate 52 ((v64 . v0)(v66 . v2))) ((= (^ v0 (^ (v v0 v1) v2)) (^ v0 v2))))
(54 (instantiate 1 ((v0 . (C1))(v1 . (E)))) ((= (^ (C1) (E)) (^ (E) (C1)))))
(55 (paramod 54 (1 1) 44 (1 1)) ((= (^ (E) (C1)) (C1))))
(56 (instantiate 1 ((v0 . v64)(v1 . v65))) ((= (^ v64 v65) (^ v65 v64))))
(57 (instantiate 6 ((v0 . v64)(v1 . v65))) ((= (v v64 (^ v64 v65)) v64)))
(58 (paramod 56 (1 1) 57 (1 1 2)) ((= (v v64 (^ v65 v64)) v64)))
(59 (instantiate 58 ((v64 . v0)(v65 . v1))) ((= (v v0 (^ v1 v0)) v0)))
(60 (instantiate 3 ((v0 . v64)(v1 . (^ v64 v65)))) ((= (v v64 (^ v64 v65)) (v (^ v64 v65) v64))))
(61 (instantiate 6 ((v0 . v64)(v1 . v65))) ((= (v v64 (^ v64 v65)) v64)))
(62 (paramod 60 (1 1) 61 (1 1)) ((= (v (^ v64 v65) v64) v64)))
(63 (instantiate 62 ((v64 . v0)(v65 . v1))) ((= (v (^ v0 v1) v0) v0)))
(64 (instantiate 1 ((v0 . (0))(v1 . v64))) ((= (^ (0) v64) (^ v64 (0)))))
(65 (instantiate 7 ((v0 . v64))) ((= (^ (0) v64) (0))))
(66 (paramod 64 (1 1) 65 (1 1)) ((= (^ v64 (0)) (0))))
(67 (instantiate 66 ((v64 . v0))) ((= (^ v0 (0)) (0))))
(68 (instantiate 3 ((v0 . (0))(v1 . v64))) ((= (v (0) v64) (v v64 (0)))))
(69 (instantiate 8 ((v0 . v64))) ((= (v (0) v64) v64)))
(70 (paramod 68 (1 1) 69 (1 1)) ((= (v v64 (0)) v64)))
(71 (instantiate 70 ((v64 . v0))) ((= (v v0 (0)) v0)))
(72 (instantiate 1 ((v0 . (1))(v1 . v64))) ((= (^ (1) v64) (^ v64 (1)))))
(73 (instantiate 9 ((v0 . v64))) ((= (^ (1) v64) v64)))
(74 (paramod 72 (1 1) 73 (1 1)) ((= (^ v64 (1)) v64)))
(75 (instantiate 74 ((v64 . v0))) ((= (^ v0 (1)) v0)))
(76 (instantiate 10 ((v0 . (v (A) (B)))(v1 . (C1))(v2 . v66))) ((= (v (^ (v (A) (B)) (C1)) (^ (v (A) (B)) v66)) (^ (v (A) (B)) (v (C1) (^ (v (A) (B)) v66))))))
(77 (paramod 22 (1 1) 76 (1 1 1)) ((= (v (0) (^ (v (A) (B)) v66)) (^ (v (A) (B)) (v (C1) (^ (v (A) (B)) v66))))))
(78 (instantiate 8 ((v0 . (^ (v (A) (B)) v66)))) ((= (v (0) (^ (v (A) (B)) v66)) (^ (v (A) (B)) v66))))
(79 (paramod 78 (1 1) 77 (1 1)) ((= (^ (v (A) (B)) v66) (^ (v (A) (B)) (v (C1) (^ (v (A) (B)) v66))))))
(80 (flip 79 (1)) ((= (^ (v (A) (B)) (v (C1) (^ (v (A) (B)) v66))) (^ (v (A) (B)) v66))))
(81 (instantiate 80 ((v66 . v0))) ((= (^ (v (A) (B)) (v (C1) (^ (v (A) (B)) v0))) (^ (v (A) (B)) v0))))
(82 (instantiate 10 ((v0 . (E))(v1 . v65)(v2 . (C1)))) ((= (v (^ (E) v65) (^ (E) (C1))) (^ (E) (v v65 (^ (E) (C1)))))))
(83 (paramod 55 (1 1) 82 (1 1 2)) ((= (v (^ (E) v65) (C1)) (^ (E) (v v65 (^ (E) (C1)))))))
(84 (paramod 55 (1 1) 83 (1 2 2 2)) ((= (v (^ (E) v65) (C1)) (^ (E) (v v65 (C1))))))
(85 (instantiate 84 ((v65 . v0))) ((= (v (^ (E) v0) (C1)) (^ (E) (v v0 (C1))))))
(86 (instantiate 3 ((v0 . (^ v64 v65))(v1 . (^ v64 v66)))) ((= (v (^ v64 v65) (^ v64 v66)) (v (^ v64 v66) (^ v64 v65)))))
(87 (instantiate 10 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (v (^ v64 v65) (^ v64 v66)) (^ v64 (v v65 (^ v64 v66))))))
(88 (paramod 86 (1 1) 87 (1 1)) ((= (v (^ v64 v66) (^ v64 v65)) (^ v64 (v v65 (^ v64 v66))))))
(89 (instantiate 10 ((v0 . v64)(v1 . v66)(v2 . v65))) ((= (v (^ v64 v66) (^ v64 v65)) (^ v64 (v v66 (^ v64 v65))))))
(90 (paramod 89 (1 1) 88 (1 1)) ((= (^ v64 (v v66 (^ v64 v65))) (^ v64 (v v65 (^ v64 v66))))))
(91 (instantiate 90 ((v64 . v0)(v65 . v2)(v66 . v1))) ((= (^ v0 (v v1 (^ v0 v2))) (^ v0 (v v2 (^ v0 v1))))))
(92 (instantiate 1 ((v0 . (v (A) (B)))(v1 . v64))) ((= (^ (v (A) (B)) v64) (^ v64 (v (A) (B))))))
(93 (instantiate 28 ((v0 . v64))) ((= (^ (C1) (^ (v (A) (B)) v64)) (0))))
(94 (paramod 92 (1 1) 93 (1 1 2)) ((= (^ (C1) (^ v64 (v (A) (B)))) (0))))
(95 (instantiate 94 ((v64 . v0))) ((= (^ (C1) (^ v0 (v (A) (B)))) (0))))
(96 (instantiate 5 ((v0 . (A))(v1 . (B)))) ((= (^ (A) (v (A) (B))) (A))))
(97 (instantiate 95 ((v0 . (A)))) ((= (^ (C1) (^ (A) (v (A) (B)))) (0))))
(98 (paramod 96 (1 1) 97 (1 1 2)) ((= (^ (C1) (A)) (0))))
(99 (instantiate 1 ((v0 . (C1))(v1 . (A)))) ((= (^ (C1) (A)) (^ (A) (C1)))))
(100 (paramod 99 (1 1) 98 (1 1)) ((= (^ (A) (C1)) (0))))
(101 (instantiate 91 ((v0 . (B))(v1 . (C2))(v2 . (A)))) ((= (^ (B) (v (C2) (^ (B) (A)))) (^ (B) (v (A) (^ (B) (C2)))))))
(102 (paramod 35 (1 1) 101 (1 1 2)) ((= (^ (B) (1)) (^ (B) (v (A) (^ (B) (C2)))))))
(103 (instantiate 75 ((v0 . (B)))) ((= (^ (B) (1)) (B))))
(104 (paramod 103 (1 1) 102 (1 1)) ((= (B) (^ (B) (v (A) (^ (B) (C2)))))))
(105 (flip 104 (1)) ((= (^ (B) (v (A) (^ (B) (C2)))) (B))))
(106 (instantiate 91 ((v0 . (A))(v1 . (C1))(v2 . (C2)))) ((= (^ (A) (v (C1) (^ (A) (C2)))) (^ (A) (v (C2) (^ (A) (C1)))))))
(107 (paramod 14 (1 1) 106 (1 1 2)) ((= (^ (A) (D)) (^ (A) (v (C2) (^ (A) (C1)))))))
(108 (paramod 100 (1 1) 107 (1 2 2 2)) ((= (^ (A) (D)) (^ (A) (v (C2) (0))))))
(109 (instantiate 71 ((v0 . (C2)))) ((= (v (C2) (0)) (C2))))
(110 (paramod 109 (1 1) 108 (1 2 2)) ((= (^ (A) (D)) (^ (A) (C2)))))
(111 (instantiate 1 ((v0 . (A))(v1 . (D)))) ((= (^ (A) (D)) (^ (D) (A)))))
(112 (paramod 111 (1 1) 110 (1 1)) ((= (^ (D) (A)) (^ (A) (C2)))))
(113 (instantiate 59 ((v0 . (v (A) (^ (B) (C2))))(v1 . (B)))) ((= (v (v (A) (^ (B) (C2))) (^ (B) (v (A) (^ (B) (C2))))) (v (A) (^ (B) (C2))))))
(114 (paramod 105 (1 1) 113 (1 1 2)) ((= (v (v (A) (^ (B) (C2))) (B)) (v (A) (^ (B) (C2))))))
(115 (instantiate 4 ((v0 . (A))(v1 . (^ (B) (C2)))(v2 . (B)))) ((= (v (v (A) (^ (B) (C2))) (B)) (v (A) (v (^ (B) (C2)) (B))))))
(116 (paramod 115 (1 1) 114 (1 1)) ((= (v (A) (v (^ (B) (C2)) (B))) (v (A) (^ (B) (C2))))))
(117 (instantiate 63 ((v0 . (B))(v1 . (C2)))) ((= (v (^ (B) (C2)) (B)) (B))))
(118 (paramod 117 (1 1) 116 (1 1 2)) ((= (v (A) (B)) (v (A) (^ (B) (C2))))))
(119 (flip 118 (1)) ((= (v (A) (^ (B) (C2))) (v (A) (B)))))
(120 (instantiate 3 ((v0 . (A))(v1 . (^ (B) (C2))))) ((= (v (A) (^ (B) (C2))) (v (^ (B) (C2)) (A)))))
(121 (paramod 120 (1 1) 119 (1 1)) ((= (v (^ (B) (C2)) (A)) (v (A) (B)))))
(122 (instantiate 48 ((v0 . (^ (B) (C2)))(v1 . (A)))) ((= (^ (v (^ (B) (C2)) (A)) (^ (B) (C2))) (^ (B) (C2)))))
(123 (paramod 121 (1 1) 122 (1 1 1)) ((= (^ (v (A) (B)) (^ (B) (C2))) (^ (B) (C2)))))
(124 (instantiate 81 ((v0 . (^ (B) (C2))))) ((= (^ (v (A) (B)) (v (C1) (^ (v (A) (B)) (^ (B) (C2))))) (^ (v (A) (B)) (^ (B) (C2))))))
(125 (paramod 123 (1 1) 124 (1 1 2 2)) ((= (^ (v (A) (B)) (v (C1) (^ (B) (C2)))) (^ (v (A) (B)) (^ (B) (C2))))))
(126 (paramod 15 (1 1) 125 (1 1 2)) ((= (^ (v (A) (B)) (E)) (^ (v (A) (B)) (^ (B) (C2))))))
(127 (paramod 123 (1 1) 126 (1 2)) ((= (^ (v (A) (B)) (E)) (^ (B) (C2)))))
(128 (instantiate 53 ((v0 . (A))(v1 . (B))(v2 . (E)))) ((= (^ (A) (^ (v (A) (B)) (E))) (^ (A) (E)))))
(129 (paramod 127 (1 1) 128 (1 1 2)) ((= (^ (A) (^ (B) (C2))) (^ (A) (E)))))
(130 (paramod 39 (1 1) 129 (1 1)) ((= (0) (^ (A) (E)))))
(131 (flip 130 (1)) ((= (^ (A) (E)) (0))))
(132 (instantiate 33 ((v0 . (E))(v1 . v65)(v2 . (A)))) ((= (^ v65 (^ (A) (E))) (^ (E) (^ v65 (A))))))
(133 (paramod 131 (1 1) 132 (1 1 2)) ((= (^ v65 (0)) (^ (E) (^ v65 (A))))))
(134 (instantiate 67 ((v0 . v65))) ((= (^ v65 (0)) (0))))
(135 (paramod 134 (1 1) 133 (1 1)) ((= (0) (^ (E) (^ v65 (A))))))
(136 (flip 135 (1)) ((= (^ (E) (^ v65 (A))) (0))))
(137 (instantiate 136 ((v65 . v0))) ((= (^ (E) (^ v0 (A))) (0))))
(138 (instantiate 85 ((v0 . (^ v0 (A))))) ((= (v (^ (E) (^ v0 (A))) (C1)) (^ (E) (v (^ v0 (A)) (C1))))))
(139 (paramod 137 (1 1) 138 (1 1 1)) ((= (v (0) (C1)) (^ (E) (v (^ v0 (A)) (C1))))))
(140 (instantiate 8 ((v0 . (C1)))) ((= (v (0) (C1)) (C1))))
(141 (paramod 140 (1 1) 139 (1 1)) ((= (C1) (^ (E) (v (^ v0 (A)) (C1))))))
(142 (flip 141 (1)) ((= (^ (E) (v (^ v0 (A)) (C1))) (C1))))
(143 (instantiate 142 ((v0 . (D)))) ((= (^ (E) (v (^ (D) (A)) (C1))) (C1))))
(144 (paramod 112 (1 1) 143 (1 1 2 1)) ((= (^ (E) (v (^ (A) (C2)) (C1))) (C1))))
(145 (paramod 42 (1 1) 144 (1 1 2)) ((= (^ (E) (D)) (C1))))
(146 (resolve 18 (1) 145 (1)) ())
)