;; ----- Otter 3.0.4, August 1995 -----
;; The job was started by mccune on gyro, Wed Nov  1 22:04:06 1995
;;
;;;;  -> x=x.
;;;; B^A=A^B, (A^B)^C=A^ (B^C), A^ (A v B)=A -> .
;;;;  -> y v (x^ (y^z))=y.
;;;;  -> y^ (x v (y v z))=y.
;;;;  -> ((x^y) v (y^z)) v y=y.
;;;;  -> ((x v y)^ (y v z))^y=y.
;;
;; ----> UNIT CONFLICT at 392.74 sec ----> 24035 [binary,24033.1,2914.1]  -> .
;;
(
(1 (input) ((= v0 v0)))
(2 (input) ((not (= (^ (B) (A)) (^ (A) (B)))) (not (= (^ (^ (A) (B)) (C)) (^ (A) (^ (B) (C))))) (not (= (^ (A) (v (A) (B))) (A)))))
(3 (input) ((= (v v0 (^ v1 (^ v0 v2))) v0)))
(4 (input) ((= (^ v0 (v v1 (v v0 v2))) v0)))
(5 (input) ((= (v (v (^ v0 v1) (^ v1 v2)) v1) v1)))
(6 (input) ((= (^ (^ (v v0 v1) (v v1 v2)) v1) v1)))
(7 (instantiate 3 ((v0 . v64))) ((= (v v64 (^ v1 (^ v64 v2))) v64)))
(8 (instantiate 4 ((v0 . v64)(v1 . v65)(v2 . (^ v1 (^ v64 v2))))) ((= (^ v64 (v v65 (v v64 (^ v1 (^ v64 v2))))) v64)))
(9 (paramod 7 (1 1) 8 (1 1 2 2)) ((= (^ v64 (v v65 v64)) v64)))
(10 (instantiate 9 ((v64 . v0)(v65 . v1))) ((= (^ v0 (v v1 v0)) v0)))
(11 (instantiate 4 ((v0 . v64))) ((= (^ v64 (v v1 (v v64 v2))) v64)))
(12 (instantiate 3 ((v0 . v64)(v1 . v65)(v2 . (v v1 (v v64 v2))))) ((= (v v64 (^ v65 (^ v64 (v v1 (v v64 v2))))) v64)))
(13 (paramod 11 (1 1) 12 (1 1 2 2)) ((= (v v64 (^ v65 v64)) v64)))
(14 (instantiate 13 ((v64 . v0)(v65 . v1))) ((= (v v0 (^ v1 v0)) v0)))
(15 (instantiate 3 ((v0 . v65))) ((= (v v65 (^ v1 (^ v65 v2))) v65)))
(16 (instantiate 10 ((v0 . (^ v1 (^ v65 v2)))(v1 . v65))) ((= (^ (^ v1 (^ v65 v2)) (v v65 (^ v1 (^ v65 v2)))) (^ v1 (^ v65 v2)))))
(17 (paramod 15 (1 1) 16 (1 1 2)) ((= (^ (^ v1 (^ v65 v2)) v65) (^ v1 (^ v65 v2)))))
(18 (instantiate 17 ((v1 . v0)(v65 . v1))) ((= (^ (^ v0 (^ v1 v2)) v1) (^ v0 (^ v1 v2)))))
(19 (instantiate 10 ((v0 . v65))) ((= (^ v65 (v v1 v65)) v65)))
(20 (instantiate 14 ((v0 . (v v1 v65))(v1 . v65))) ((= (v (v v1 v65) (^ v65 (v v1 v65))) (v v1 v65))))
(21 (paramod 19 (1 1) 20 (1 1 2)) ((= (v (v v1 v65) v65) (v v1 v65))))
(22 (instantiate 21 ((v1 . v0)(v65 . v1))) ((= (v (v v0 v1) v1) (v v0 v1))))
(23 (instantiate 4 ((v0 . v65))) ((= (^ v65 (v v1 (v v65 v2))) v65)))
(24 (instantiate 14 ((v0 . (v v1 (v v65 v2)))(v1 . v65))) ((= (v (v v1 (v v65 v2)) (^ v65 (v v1 (v v65 v2)))) (v v1 (v v65 v2)))))
(25 (paramod 23 (1 1) 24 (1 1 2)) ((= (v (v v1 (v v65 v2)) v65) (v v1 (v v65 v2)))))
(26 (instantiate 25 ((v1 . v0)(v65 . v1))) ((= (v (v v0 (v v1 v2)) v1) (v v0 (v v1 v2)))))
(27 (instantiate 14 ((v0 . v65))) ((= (v v65 (^ v1 v65)) v65)))
(28 (instantiate 10 ((v0 . (^ v1 v65))(v1 . v65))) ((= (^ (^ v1 v65) (v v65 (^ v1 v65))) (^ v1 v65))))
(29 (paramod 27 (1 1) 28 (1 1 2)) ((= (^ (^ v1 v65) v65) (^ v1 v65))))
(30 (instantiate 29 ((v1 . v0)(v65 . v1))) ((= (^ (^ v0 v1) v1) (^ v0 v1))))
(31 (instantiate 10 ((v0 . v65))) ((= (^ v65 (v v1 v65)) v65)))
(32 (instantiate 5 ((v0 . v64)(v1 . v65)(v2 . (v v1 v65)))) ((= (v (v (^ v64 v65) (^ v65 (v v1 v65))) v65) v65)))
(33 (paramod 31 (1 1) 32 (1 1 1 2)) ((= (v (v (^ v64 v65) v65) v65) v65)))
(34 (instantiate 22 ((v0 . (^ v64 v65))(v1 . v65))) ((= (v (v (^ v64 v65) v65) v65) (v (^ v64 v65) v65))))
(35 (paramod 34 (1 1) 33 (1 1)) ((= (v (^ v64 v65) v65) v65)))
(36 (instantiate 35 ((v64 . v0)(v65 . v1))) ((= (v (^ v0 v1) v1) v1)))
(37 (instantiate 4 ((v0 . v65))) ((= (^ v65 (v v1 (v v65 v2))) v65)))
(38 (instantiate 5 ((v0 . v64)(v1 . v65)(v2 . (v v1 (v v65 v2))))) ((= (v (v (^ v64 v65) (^ v65 (v v1 (v v65 v2)))) v65) v65)))
(39 (paramod 37 (1 1) 38 (1 1 1 2)) ((= (v (v (^ v64 v65) v65) v65) v65)))
(40 (instantiate 36 ((v0 . v64)(v1 . v65))) ((= (v (^ v64 v65) v65) v65)))
(41 (paramod 40 (1 1) 39 (1 1 1)) ((= (v v65 v65) v65)))
(42 (instantiate 41 ((v65 . v0))) ((= (v v0 v0) v0)))
(43 (instantiate 5 ((v1 . v64))) ((= (v (v (^ v0 v64) (^ v64 v2)) v64) v64)))
(44 (instantiate 10 ((v0 . v64)(v1 . (v (^ v0 v64) (^ v64 v2))))) ((= (^ v64 (v (v (^ v0 v64) (^ v64 v2)) v64)) v64)))
(45 (paramod 43 (1 1) 44 (1 1 2)) ((= (^ v64 v64) v64)))
(46 (instantiate 45 ((v64 . v0))) ((= (^ v0 v0) v0)))
(47 (instantiate 5 ((v1 . (v v64 v66)))) ((= (v (v (^ v0 (v v64 v66)) (^ (v v64 v66) v2)) (v v64 v66)) (v v64 v66))))
(48 (instantiate 4 ((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)))
(49 (paramod 47 (1 1) 48 (1 1 2)) ((= (^ v64 (v v64 v66)) v64)))
(50 (instantiate 49 ((v64 . v0)(v66 . v1))) ((= (^ v0 (v v0 v1)) v0)))
(51 (instantiate 50 ((v0 . (A))(v1 . (B)))) ((= (^ (A) (v (A) (B))) (A))))
(52 (paramod 51 (1 1) 2 (3 1 1)) ((not (= (^ (B) (A)) (^ (A) (B)))) (not (= (^ (^ (A) (B)) (C)) (^ (A) (^ (B) (C))))) (not (= (A) (A)))))
(53 (instantiate 1 ((v0 . (A)))) ((= (A) (A))))
(54 (resolve 52 (3) 53 (1)) ((not (= (^ (B) (A)) (^ (A) (B)))) (not (= (^ (^ (A) (B)) (C)) (^ (A) (^ (B) (C)))))))
(55 (instantiate 46 ((v0 . (^ v64 v66)))) ((= (^ (^ v64 v66) (^ v64 v66)) (^ v64 v66))))
(56 (instantiate 3 ((v0 . v64)(v1 . (^ v64 v66))(v2 . v66))) ((= (v v64 (^ (^ v64 v66) (^ v64 v66))) v64)))
(57 (paramod 55 (1 1) 56 (1 1 2)) ((= (v v64 (^ v64 v66)) v64)))
(58 (instantiate 57 ((v64 . v0)(v66 . v1))) ((= (v v0 (^ v0 v1)) v0)))
(59 (instantiate 10 ((v0 . v64))) ((= (^ v64 (v v1 v64)) v64)))
(60 (instantiate 36 ((v0 . v64)(v1 . (v v1 v64)))) ((= (v (^ v64 (v v1 v64)) (v v1 v64)) (v v1 v64))))
(61 (paramod 59 (1 1) 60 (1 1 1)) ((= (v v64 (v v1 v64)) (v v1 v64))))
(62 (instantiate 61 ((v64 . v0))) ((= (v v0 (v v1 v0)) (v v1 v0))))
(63 (instantiate 5 ((v1 . v65))) ((= (v (v (^ v0 v65) (^ v65 v2)) v65) v65)))
(64 (instantiate 50 ((v0 . (v (^ v0 v65) (^ v65 v2)))(v1 . v65))) ((= (^ (v (^ v0 v65) (^ v65 v2)) (v (v (^ v0 v65) (^ v65 v2)) v65)) (v (^ v0 v65) (^ v65 v2)))))
(65 (paramod 63 (1 1) 64 (1 1 2)) ((= (^ (v (^ v0 v65) (^ v65 v2)) v65) (v (^ v0 v65) (^ v65 v2)))))
(66 (instantiate 65 ((v65 . v1))) ((= (^ (v (^ v0 v1) (^ v1 v2)) v1) (v (^ v0 v1) (^ v1 v2)))))
(67 (instantiate 14 ((v0 . v64))) ((= (v v64 (^ v1 v64)) v64)))
(68 (instantiate 6 ((v0 . v64)(v1 . (^ v1 v64))(v2 . v66))) ((= (^ (^ (v v64 (^ v1 v64)) (v (^ v1 v64) v66)) (^ v1 v64)) (^ v1 v64))))
(69 (paramod 67 (1 1) 68 (1 1 1 1)) ((= (^ (^ v64 (v (^ v1 v64) v66)) (^ v1 v64)) (^ v1 v64))))
(70 (instantiate 69 ((v64 . v0)(v66 . v2))) ((= (^ (^ v0 (v (^ v1 v0) v2)) (^ v1 v0)) (^ v1 v0))))
(71 (instantiate 42 ((v0 . v66))) ((= (v v66 v66) v66)))
(72 (instantiate 6 ((v0 . v64)(v1 . v66)(v2 . v66))) ((= (^ (^ (v v64 v66) (v v66 v66)) v66) v66)))
(73 (paramod 71 (1 1) 72 (1 1 1 2)) ((= (^ (^ (v v64 v66) v66) v66) v66)))
(74 (instantiate 30 ((v0 . (v v64 v66))(v1 . v66))) ((= (^ (^ (v v64 v66) v66) v66) (^ (v v64 v66) v66))))
(75 (paramod 74 (1 1) 73 (1 1)) ((= (^ (v v64 v66) v66) v66)))
(76 (instantiate 75 ((v64 . v0)(v66 . v1))) ((= (^ (v v0 v1) v1) v1)))
(77 (instantiate 36 ((v1 . v66))) ((= (v (^ v0 v66) v66) v66)))
(78 (instantiate 6 ((v0 . v64)(v1 . (^ v0 v66))(v2 . v66))) ((= (^ (^ (v v64 (^ v0 v66)) (v (^ v0 v66) v66)) (^ v0 v66)) (^ v0 v66))))
(79 (paramod 77 (1 1) 78 (1 1 1 2)) ((= (^ (^ (v v64 (^ v0 v66)) v66) (^ v0 v66)) (^ v0 v66))))
(80 (instantiate 79 ((v0 . v1)(v64 . v0)(v66 . v2))) ((= (^ (^ (v v0 (^ v1 v2)) v2) (^ v1 v2)) (^ v1 v2))))
(81 (instantiate 58 ((v0 . v65))) ((= (v v65 (^ v65 v1)) v65)))
(82 (instantiate 10 ((v0 . (^ v65 v1))(v1 . v65))) ((= (^ (^ v65 v1) (v v65 (^ v65 v1))) (^ v65 v1))))
(83 (paramod 81 (1 1) 82 (1 1 2)) ((= (^ (^ v65 v1) v65) (^ v65 v1))))
(84 (instantiate 83 ((v65 . v0))) ((= (^ (^ v0 v1) v0) (^ v0 v1))))
(85 (instantiate 58 ((v0 . v64))) ((= (v v64 (^ v64 v1)) v64)))
(86 (instantiate 6 ((v0 . v64)(v1 . (^ v64 v1))(v2 . v66))) ((= (^ (^ (v v64 (^ v64 v1)) (v (^ v64 v1) v66)) (^ v64 v1)) (^ v64 v1))))
(87 (paramod 85 (1 1) 86 (1 1 1 1)) ((= (^ (^ v64 (v (^ v64 v1) v66)) (^ v64 v1)) (^ v64 v1))))
(88 (instantiate 87 ((v64 . v0)(v66 . v2))) ((= (^ (^ v0 (v (^ v0 v1) v2)) (^ v0 v1)) (^ v0 v1))))
(89 (instantiate 14 ((v0 . v64))) ((= (v v64 (^ v1 v64)) v64)))
(90 (instantiate 76 ((v0 . v64)(v1 . (^ v1 v64)))) ((= (^ (v v64 (^ v1 v64)) (^ v1 v64)) (^ v1 v64))))
(91 (paramod 89 (1 1) 90 (1 1 1)) ((= (^ v64 (^ v1 v64)) (^ v1 v64))))
(92 (instantiate 91 ((v64 . v0))) ((= (^ v0 (^ v1 v0)) (^ v1 v0))))
(93 (instantiate 58 ((v0 . v65))) ((= (v v65 (^ v65 v1)) v65)))
(94 (instantiate 62 ((v0 . (^ v65 v1))(v1 . v65))) ((= (v (^ v65 v1) (v v65 (^ v65 v1))) (v v65 (^ v65 v1)))))
(95 (paramod 93 (1 1) 94 (1 1 2)) ((= (v (^ v65 v1) v65) (v v65 (^ v65 v1)))))
(96 (instantiate 58 ((v0 . v65)(v1 . v1))) ((= (v v65 (^ v65 v1)) v65)))
(97 (paramod 96 (1 1) 95 (1 2)) ((= (v (^ v65 v1) v65) v65)))
(98 (instantiate 97 ((v65 . v0))) ((= (v (^ v0 v1) v0) v0)))
(99 (instantiate 3 ((v0 . v65))) ((= (v v65 (^ v1 (^ v65 v2))) v65)))
(100 (instantiate 62 ((v0 . (^ v1 (^ v65 v2)))(v1 . v65))) ((= (v (^ v1 (^ v65 v2)) (v v65 (^ v1 (^ v65 v2)))) (v v65 (^ v1 (^ v65 v2))))))
(101 (paramod 99 (1 1) 100 (1 1 2)) ((= (v (^ v1 (^ v65 v2)) v65) (v v65 (^ v1 (^ v65 v2))))))
(102 (instantiate 3 ((v0 . v65)(v1 . v1)(v2 . v2))) ((= (v v65 (^ v1 (^ v65 v2))) v65)))
(103 (paramod 102 (1 1) 101 (1 2)) ((= (v (^ v1 (^ v65 v2)) v65) v65)))
(104 (instantiate 103 ((v1 . v0)(v65 . v1))) ((= (v (^ v0 (^ v1 v2)) v1) v1)))
(105 (instantiate 98 ((v0 . v66))) ((= (v (^ v66 v1) v66) v66)))
(106 (instantiate 26 ((v0 . v64)(v1 . (^ v66 v1))(v2 . v66))) ((= (v (v v64 (v (^ v66 v1) v66)) (^ v66 v1)) (v v64 (v (^ v66 v1) v66)))))
(107 (paramod 105 (1 1) 106 (1 1 1 2)) ((= (v (v v64 v66) (^ v66 v1)) (v v64 (v (^ v66 v1) v66)))))
(108 (instantiate 98 ((v0 . v66)(v1 . v1))) ((= (v (^ v66 v1) v66) v66)))
(109 (paramod 108 (1 1) 107 (1 2 2)) ((= (v (v v64 v66) (^ v66 v1)) (v v64 v66))))
(110 (instantiate 109 ((v1 . v2)(v64 . v0)(v66 . v1))) ((= (v (v v0 v1) (^ v1 v2)) (v v0 v1))))
(111 (instantiate 92 ((v0 . v65))) ((= (^ v65 (^ v1 v65)) (^ v1 v65))))
(112 (instantiate 18 ((v0 . v64)(v1 . v65)(v2 . (^ v1 v65)))) ((= (^ (^ v64 (^ v65 (^ v1 v65))) v65) (^ v64 (^ v65 (^ v1 v65))))))
(113 (paramod 111 (1 1) 112 (1 1 1 2)) ((= (^ (^ v64 (^ v1 v65)) v65) (^ v64 (^ v65 (^ v1 v65))))))
(114 (instantiate 92 ((v0 . v65)(v1 . v1))) ((= (^ v65 (^ v1 v65)) (^ v1 v65))))
(115 (paramod 114 (1 1) 113 (1 2 2)) ((= (^ (^ v64 (^ v1 v65)) v65) (^ v64 (^ v1 v65)))))
(116 (instantiate 115 ((v64 . v0)(v65 . v2))) ((= (^ (^ v0 (^ v1 v2)) v2) (^ v0 (^ v1 v2)))))
(117 (instantiate 92 ((v0 . v65))) ((= (^ v65 (^ v1 v65)) (^ v1 v65))))
(118 (instantiate 104 ((v0 . v64)(v1 . v65)(v2 . (^ v1 v65)))) ((= (v (^ v64 (^ v65 (^ v1 v65))) v65) v65)))
(119 (paramod 117 (1 1) 118 (1 1 1 2)) ((= (v (^ v64 (^ v1 v65)) v65) v65)))
(120 (instantiate 119 ((v64 . v0)(v65 . v2))) ((= (v (^ v0 (^ v1 v2)) v2) v2)))
(121 (instantiate 84 ((v0 . (^ v65 v66)))) ((= (^ (^ (^ v65 v66) v1) (^ v65 v66)) (^ (^ v65 v66) v1))))
(122 (instantiate 104 ((v0 . (^ (^ v65 v66) v1))(v1 . v65)(v2 . v66))) ((= (v (^ (^ (^ v65 v66) v1) (^ v65 v66)) v65) v65)))
(123 (paramod 121 (1 1) 122 (1 1 1)) ((= (v (^ (^ v65 v66) v1) v65) v65)))
(124 (instantiate 123 ((v1 . v2)(v65 . v0)(v66 . v1))) ((= (v (^ (^ v0 v1) v2) v0) v0)))
(125 (instantiate 84 ((v0 . (^ v65 v66)))) ((= (^ (^ (^ v65 v66) v1) (^ v65 v66)) (^ (^ v65 v66) v1))))
(126 (instantiate 120 ((v0 . (^ (^ v65 v66) v1))(v1 . v65)(v2 . v66))) ((= (v (^ (^ (^ v65 v66) v1) (^ v65 v66)) v66) v66)))
(127 (paramod 125 (1 1) 126 (1 1 1)) ((= (v (^ (^ v65 v66) v1) v66) v66)))
(128 (instantiate 127 ((v1 . v2)(v65 . v0)(v66 . v1))) ((= (v (^ (^ v0 v1) v2) v1) v1)))
(129 (instantiate 76 ((v1 . v65))) ((= (^ (v v0 v65) v65) v65)))
(130 (instantiate 124 ((v0 . (v v0 v65))(v1 . v65)(v2 . v66))) ((= (v (^ (^ (v v0 v65) v65) v66) (v v0 v65)) (v v0 v65))))
(131 (paramod 129 (1 1) 130 (1 1 1 1)) ((= (v (^ v65 v66) (v v0 v65)) (v v0 v65))))
(132 (instantiate 131 ((v0 . v2)(v65 . v0)(v66 . v1))) ((= (v (^ v0 v1) (v v2 v0)) (v v2 v0))))
(133 (instantiate 128 ((v1 . v66)(v2 . v64))) ((= (v (^ (^ v0 v66) v64) v66) v66)))
(134 (instantiate 70 ((v0 . v64)(v1 . (^ v0 v66))(v2 . v66))) ((= (^ (^ v64 (v (^ (^ v0 v66) v64) v66)) (^ (^ v0 v66) v64)) (^ (^ v0 v66) v64))))
(135 (paramod 133 (1 1) 134 (1 1 1 2)) ((= (^ (^ v64 v66) (^ (^ v0 v66) v64)) (^ (^ v0 v66) v64))))
(136 (instantiate 135 ((v0 . v2)(v64 . v0)(v66 . v1))) ((= (^ (^ v0 v1) (^ (^ v2 v1) v0)) (^ (^ v2 v1) v0))))
(137 (instantiate 98 ((v0 . v66)(v1 . v64))) ((= (v (^ v66 v64) v66) v66)))
(138 (instantiate 70 ((v0 . v64)(v1 . v66)(v2 . v66))) ((= (^ (^ v64 (v (^ v66 v64) v66)) (^ v66 v64)) (^ v66 v64))))
(139 (paramod 137 (1 1) 138 (1 1 1 2)) ((= (^ (^ v64 v66) (^ v66 v64)) (^ v66 v64))))
(140 (instantiate 139 ((v64 . v0)(v66 . v1))) ((= (^ (^ v0 v1) (^ v1 v0)) (^ v1 v0))))
(141 (instantiate 110 ((v1 . v65)(v2 . v66))) ((= (v (v v0 v65) (^ v65 v66)) (v v0 v65))))
(142 (instantiate 80 ((v0 . (v v0 v65))(v1 . v65)(v2 . v66))) ((= (^ (^ (v (v v0 v65) (^ v65 v66)) v66) (^ v65 v66)) (^ v65 v66))))
(143 (paramod 141 (1 1) 142 (1 1 1 1)) ((= (^ (^ (v v0 v65) v66) (^ v65 v66)) (^ v65 v66))))
(144 (instantiate 143 ((v65 . v1)(v66 . v2))) ((= (^ (^ (v v0 v1) v2) (^ v1 v2)) (^ v1 v2))))
(145 (instantiate 132 ((v0 . v65)(v1 . v64))) ((= (v (^ v65 v64) (v v2 v65)) (v v2 v65))))
(146 (instantiate 70 ((v0 . v64)(v1 . v65)(v2 . (v v2 v65)))) ((= (^ (^ v64 (v (^ v65 v64) (v v2 v65))) (^ v65 v64)) (^ v65 v64))))
(147 (paramod 145 (1 1) 146 (1 1 1 2)) ((= (^ (^ v64 (v v2 v65)) (^ v65 v64)) (^ v65 v64))))
(148 (instantiate 147 ((v2 . v1)(v64 . v0)(v65 . v2))) ((= (^ (^ v0 (v v1 v2)) (^ v2 v0)) (^ v2 v0))))
(149 (instantiate 104 ((v0 . v64)(v1 . v66))) ((= (v (^ v64 (^ v66 v2)) v66) v66)))
(150 (instantiate 88 ((v0 . v64)(v1 . (^ v66 v2))(v2 . v66))) ((= (^ (^ v64 (v (^ v64 (^ v66 v2)) v66)) (^ v64 (^ v66 v2))) (^ v64 (^ v66 v2)))))
(151 (paramod 149 (1 1) 150 (1 1 1 2)) ((= (^ (^ v64 v66) (^ v64 (^ v66 v2))) (^ v64 (^ v66 v2)))))
(152 (instantiate 151 ((v64 . v0)(v66 . v1))) ((= (^ (^ v0 v1) (^ v0 (^ v1 v2))) (^ v0 (^ v1 v2)))))
(153 (instantiate 104 ((v0 . v64)(v1 . (^ v0 v1))(v2 . (^ v1 v0)))) ((= (v (^ v64 (^ (^ v0 v1) (^ v1 v0))) (^ v0 v1)) (^ v0 v1))))
(154 (paramod 140 (1 1) 153 (1 1 1 2)) ((= (v (^ v64 (^ v1 v0)) (^ v0 v1)) (^ v0 v1))))
(155 (instantiate 154 ((v0 . v2)(v64 . v0))) ((= (v (^ v0 (^ v1 v2)) (^ v2 v1)) (^ v2 v1))))
(156 (instantiate 66 ((v0 . v64)(v1 . (^ v0 v1))(v2 . (^ v1 v0)))) ((= (^ (v (^ v64 (^ v0 v1)) (^ (^ v0 v1) (^ v1 v0))) (^ v0 v1)) (v (^ v64 (^ v0 v1)) (^ (^ v0 v1) (^ v1 v0))))))
(157 (paramod 140 (1 1) 156 (1 1 1 2)) ((= (^ (v (^ v64 (^ v0 v1)) (^ v1 v0)) (^ v0 v1)) (v (^ v64 (^ v0 v1)) (^ (^ v0 v1) (^ v1 v0))))))
(158 (instantiate 155 ((v0 . v64)(v1 . v0)(v2 . v1))) ((= (v (^ v64 (^ v0 v1)) (^ v1 v0)) (^ v1 v0))))
(159 (paramod 158 (1 1) 157 (1 1 1)) ((= (^ (^ v1 v0) (^ v0 v1)) (v (^ v64 (^ v0 v1)) (^ (^ v0 v1) (^ v1 v0))))))
(160 (instantiate 140 ((v0 . v1)(v1 . v0))) ((= (^ (^ v1 v0) (^ v0 v1)) (^ v0 v1))))
(161 (paramod 160 (1 1) 159 (1 1)) ((= (^ v0 v1) (v (^ v64 (^ v0 v1)) (^ (^ v0 v1) (^ v1 v0))))))
(162 (paramod 140 (1 1) 161 (1 2 2)) ((= (^ v0 v1) (v (^ v64 (^ v0 v1)) (^ v1 v0)))))
(163 (instantiate 155 ((v0 . v64)(v1 . v0)(v2 . v1))) ((= (v (^ v64 (^ v0 v1)) (^ v1 v0)) (^ v1 v0))))
(164 (paramod 163 (1 1) 162 (1 2)) ((= (^ v0 v1) (^ v1 v0))))
(165 (instantiate 164 ((v0 . v65)(v1 . v66))) ((= (^ v65 v66) (^ v66 v65))))
(166 (instantiate 18 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (^ (^ v64 (^ v65 v66)) v65) (^ v64 (^ v65 v66)))))
(167 (paramod 165 (1 1) 166 (1 1 1 2)) ((= (^ (^ v64 (^ v66 v65)) v65) (^ v64 (^ v65 v66)))))
(168 (instantiate 116 ((v0 . v64)(v1 . v66)(v2 . v65))) ((= (^ (^ v64 (^ v66 v65)) v65) (^ v64 (^ v66 v65)))))
(169 (paramod 168 (1 1) 167 (1 1)) ((= (^ v64 (^ v66 v65)) (^ v64 (^ v65 v66)))))
(170 (instantiate 169 ((v64 . v0)(v65 . v2)(v66 . v1))) ((= (^ v0 (^ v1 v2)) (^ v0 (^ v2 v1)))))
(171 (instantiate 164 ((v0 . (B))(v1 . (A)))) ((= (^ (B) (A)) (^ (A) (B)))))
(172 (paramod 171 (1 1) 54 (1 1 1)) ((not (= (^ (A) (B)) (^ (A) (B)))) (not (= (^ (^ (A) (B)) (C)) (^ (A) (^ (B) (C)))))))
(173 (instantiate 1 ((v0 . (^ (A) (B))))) ((= (^ (A) (B)) (^ (A) (B)))))
(174 (resolve 172 (1) 173 (1)) ((not (= (^ (^ (A) (B)) (C)) (^ (A) (^ (B) (C)))))))
(175 (instantiate 164 ((v0 . v64)(v1 . (^ v65 v66)))) ((= (^ v64 (^ v65 v66)) (^ (^ v65 v66) v64))))
(176 (instantiate 170 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (^ v64 (^ v65 v66)) (^ v64 (^ v66 v65)))))
(177 (paramod 175 (1 1) 176 (1 1)) ((= (^ (^ v65 v66) v64) (^ v64 (^ v66 v65)))))
(178 (instantiate 177 ((v64 . v2)(v65 . v0)(v66 . v1))) ((= (^ (^ v0 v1) v2) (^ v2 (^ v1 v0)))))
(179 (flip 178 (1)) ((= (^ v2 (^ v1 v0)) (^ (^ v0 v1) v2))))
(180 (instantiate 179 ((v0 . v66)(v1 . v65)(v2 . (^ (v v64 v65) v66)))) ((= (^ (^ (v v64 v65) v66) (^ v65 v66)) (^ (^ v66 v65) (^ (v v64 v65) v66)))))
(181 (instantiate 144 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (^ (^ (v v64 v65) v66) (^ v65 v66)) (^ v65 v66))))
(182 (paramod 180 (1 1) 181 (1 1)) ((= (^ (^ v66 v65) (^ (v v64 v65) v66)) (^ v65 v66))))
(183 (instantiate 182 ((v64 . v2)(v65 . v1)(v66 . v0))) ((= (^ (^ v0 v1) (^ (v v2 v1) v0)) (^ v1 v0))))
(184 (instantiate 178 ((v0 . (v v64 v65))(v1 . v66)(v2 . (^ v65 v66)))) ((= (^ (^ (v v64 v65) v66) (^ v65 v66)) (^ (^ v65 v66) (^ v66 (v v64 v65))))))
(185 (instantiate 144 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (^ (^ (v v64 v65) v66) (^ v65 v66)) (^ v65 v66))))
(186 (paramod 184 (1 1) 185 (1 1)) ((= (^ (^ v65 v66) (^ v66 (v v64 v65))) (^ v65 v66))))
(187 (instantiate 186 ((v64 . v2)(v65 . v0)(v66 . v1))) ((= (^ (^ v0 v1) (^ v1 (v v2 v0))) (^ v0 v1))))
(188 (instantiate 179 ((v0 . v64)(v1 . v66)(v2 . (^ v64 (v v65 v66))))) ((= (^ (^ v64 (v v65 v66)) (^ v66 v64)) (^ (^ v64 v66) (^ v64 (v v65 v66))))))
(189 (instantiate 148 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (^ (^ v64 (v v65 v66)) (^ v66 v64)) (^ v66 v64))))
(190 (paramod 188 (1 1) 189 (1 1)) ((= (^ (^ v64 v66) (^ v64 (v v65 v66))) (^ v66 v64))))
(191 (instantiate 190 ((v64 . v0)(v65 . v2)(v66 . v1))) ((= (^ (^ v0 v1) (^ v0 (v v2 v1))) (^ v1 v0))))
(192 (instantiate 58 ((v0 . v66))) ((= (v v66 (^ v66 v1)) v66)))
(193 (instantiate 187 ((v0 . (^ v66 v1))(v1 . v65)(v2 . v66))) ((= (^ (^ (^ v66 v1) v65) (^ v65 (v v66 (^ v66 v1)))) (^ (^ v66 v1) v65))))
(194 (paramod 192 (1 1) 193 (1 1 2 2)) ((= (^ (^ (^ v66 v1) v65) (^ v65 v66)) (^ (^ v66 v1) v65))))
(195 (instantiate 194 ((v65 . v2)(v66 . v0))) ((= (^ (^ (^ v0 v1) v2) (^ v2 v0)) (^ (^ v0 v1) v2))))
(196 (instantiate 14 ((v0 . v66))) ((= (v v66 (^ v1 v66)) v66)))
(197 (instantiate 187 ((v0 . (^ v1 v66))(v1 . v65)(v2 . v66))) ((= (^ (^ (^ v1 v66) v65) (^ v65 (v v66 (^ v1 v66)))) (^ (^ v1 v66) v65))))
(198 (paramod 196 (1 1) 197 (1 1 2 2)) ((= (^ (^ (^ v1 v66) v65) (^ v65 v66)) (^ (^ v1 v66) v65))))
(199 (instantiate 198 ((v1 . v0)(v65 . v2)(v66 . v1))) ((= (^ (^ (^ v0 v1) v2) (^ v2 v1)) (^ (^ v0 v1) v2))))
(200 (instantiate 191 ((v0 . v66)(v1 . v65))) ((= (^ (^ v66 v65) (^ v66 (v v2 v65))) (^ v65 v66))))
(201 (instantiate 136 ((v0 . (^ v66 (v v2 v65)))(v1 . v65)(v2 . v66))) ((= (^ (^ (^ v66 (v v2 v65)) v65) (^ (^ v66 v65) (^ v66 (v v2 v65)))) (^ (^ v66 v65) (^ v66 (v v2 v65))))))
(202 (paramod 200 (1 1) 201 (1 1 2)) ((= (^ (^ (^ v66 (v v2 v65)) v65) (^ v65 v66)) (^ (^ v66 v65) (^ v66 (v v2 v65))))))
(203 (instantiate 195 ((v0 . v66)(v1 . (v v2 v65))(v2 . v65))) ((= (^ (^ (^ v66 (v v2 v65)) v65) (^ v65 v66)) (^ (^ v66 (v v2 v65)) v65))))
(204 (paramod 203 (1 1) 202 (1 1)) ((= (^ (^ v66 (v v2 v65)) v65) (^ (^ v66 v65) (^ v66 (v v2 v65))))))
(205 (instantiate 191 ((v0 . v66)(v1 . v65)(v2 . v2))) ((= (^ (^ v66 v65) (^ v66 (v v2 v65))) (^ v65 v66))))
(206 (paramod 205 (1 1) 204 (1 2)) ((= (^ (^ v66 (v v2 v65)) v65) (^ v65 v66))))
(207 (instantiate 206 ((v2 . v1)(v65 . v2)(v66 . v0))) ((= (^ (^ v0 (v v1 v2)) v2) (^ v2 v0))))
(208 (instantiate 183 ((v0 . v66)(v1 . v65))) ((= (^ (^ v66 v65) (^ (v v2 v65) v66)) (^ v65 v66))))
(209 (instantiate 136 ((v0 . (^ (v v2 v65) v66))(v1 . v65)(v2 . v66))) ((= (^ (^ (^ (v v2 v65) v66) v65) (^ (^ v66 v65) (^ (v v2 v65) v66))) (^ (^ v66 v65) (^ (v v2 v65) v66)))))
(210 (paramod 208 (1 1) 209 (1 1 2)) ((= (^ (^ (^ (v v2 v65) v66) v65) (^ v65 v66)) (^ (^ v66 v65) (^ (v v2 v65) v66)))))
(211 (instantiate 199 ((v0 . (v v2 v65))(v1 . v66)(v2 . v65))) ((= (^ (^ (^ (v v2 v65) v66) v65) (^ v65 v66)) (^ (^ (v v2 v65) v66) v65))))
(212 (paramod 211 (1 1) 210 (1 1)) ((= (^ (^ (v v2 v65) v66) v65) (^ (^ v66 v65) (^ (v v2 v65) v66)))))
(213 (instantiate 183 ((v0 . v66)(v1 . v65)(v2 . v2))) ((= (^ (^ v66 v65) (^ (v v2 v65) v66)) (^ v65 v66))))
(214 (paramod 213 (1 1) 212 (1 2)) ((= (^ (^ (v v2 v65) v66) v65) (^ v65 v66))))
(215 (instantiate 214 ((v2 . v0)(v65 . v1)(v66 . v2))) ((= (^ (^ (v v0 v1) v2) v1) (^ v1 v2))))
(216 (instantiate 84 ((v0 . (v v65 v66)))) ((= (^ (^ (v v65 v66) v1) (v v65 v66)) (^ (v v65 v66) v1))))
(217 (instantiate 207 ((v0 . (^ (v v65 v66) v1))(v1 . v65)(v2 . v66))) ((= (^ (^ (^ (v v65 v66) v1) (v v65 v66)) v66) (^ v66 (^ (v v65 v66) v1)))))
(218 (paramod 216 (1 1) 217 (1 1 1)) ((= (^ (^ (v v65 v66) v1) v66) (^ v66 (^ (v v65 v66) v1)))))
(219 (instantiate 215 ((v0 . v65)(v1 . v66)(v2 . v1))) ((= (^ (^ (v v65 v66) v1) v66) (^ v66 v1))))
(220 (paramod 219 (1 1) 218 (1 1)) ((= (^ v66 v1) (^ v66 (^ (v v65 v66) v1)))))
(221 (flip 220 (1)) ((= (^ v66 (^ (v v65 v66) v1)) (^ v66 v1))))
(222 (instantiate 221 ((v1 . v2)(v65 . v1)(v66 . v0))) ((= (^ v0 (^ (v v1 v0) v2)) (^ v0 v2))))
(223 (instantiate 58 ((v0 . v65))) ((= (v v65 (^ v65 v1)) v65)))
(224 (instantiate 222 ((v0 . (^ v65 v1))(v1 . v65)(v2 . v66))) ((= (^ (^ v65 v1) (^ (v v65 (^ v65 v1)) v66)) (^ (^ v65 v1) v66))))
(225 (paramod 223 (1 1) 224 (1 1 2 1)) ((= (^ (^ v65 v1) (^ v65 v66)) (^ (^ v65 v1) v66))))
(226 (instantiate 225 ((v65 . v0)(v66 . v2))) ((= (^ (^ v0 v1) (^ v0 v2)) (^ (^ v0 v1) v2))))
(227 (instantiate 14 ((v0 . v65))) ((= (v v65 (^ v1 v65)) v65)))
(228 (instantiate 222 ((v0 . (^ v1 v65))(v1 . v65)(v2 . v66))) ((= (^ (^ v1 v65) (^ (v v65 (^ v1 v65)) v66)) (^ (^ v1 v65) v66))))
(229 (paramod 227 (1 1) 228 (1 1 2 1)) ((= (^ (^ v1 v65) (^ v65 v66)) (^ (^ v1 v65) v66))))
(230 (instantiate 229 ((v1 . v0)(v65 . v1)(v66 . v2))) ((= (^ (^ v0 v1) (^ v1 v2)) (^ (^ v0 v1) v2))))
(231 (instantiate 226 ((v0 . v0)(v1 . v1)(v2 . (^ v1 v2)))) ((= (^ (^ v0 v1) (^ v0 (^ v1 v2))) (^ (^ v0 v1) (^ v1 v2)))))
(232 (paramod 231 (1 1) 152 (1 1)) ((= (^ (^ v0 v1) (^ v1 v2)) (^ v0 (^ v1 v2)))))
(233 (paramod 230 (1 1) 232 (1 1)) ((= (^ (^ v0 v1) v2) (^ v0 (^ v1 v2)))))
(234 (instantiate 233 ((v0 . (A))(v1 . (B))(v2 . (C)))) ((= (^ (^ (A) (B)) (C)) (^ (A) (^ (B) (C))))))
(235 (resolve 174 (1) 234 (1)) ())
)