;; ----- Otter 3.0.4, August 1995 -----
;; The job was started by mccune on gyro, Wed Nov  1 22:14:31 1995
;;
;;;;  -> x=x.
;;;; B^A=A^B, (A^B)^C=A^ (B^C), A^ (A v B)=A, B v A=A v B, (A v B) v C=A v (B v C), A v (A^B)=A -> .
;;;;  -> x^ (x v y)=x.
;;;;  -> x^ (y v z)= (z^x) v (y^x).
;;
;; ----> UNIT CONFLICT at  71.49 sec ----> 6572 [binary,6570.1,3692.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))) (not (= (v (B) (A)) (v (A) (B)))) (not (= (v (v (A) (B)) (C)) (v (A) (v (B) (C))))) (not (= (v (A) (^ (A) (B))) (A)))))
(3 (input) ((= (^ v0 (v v0 v1)) v0)))
(4 (input) ((= (^ v0 (v v1 v2)) (v (^ v2 v0) (^ v1 v0)))))
(5 (instantiate 3 ((v0 . (A))(v1 . (B)))) ((= (^ (A) (v (A) (B))) (A))))
(6 (paramod 5 (1 1) 2 (3 1 1)) ((not (= (^ (B) (A)) (^ (A) (B)))) (not (= (^ (^ (A) (B)) (C)) (^ (A) (^ (B) (C))))) (not (= (A) (A))) (not (= (v (B) (A)) (v (A) (B)))) (not (= (v (v (A) (B)) (C)) (v (A) (v (B) (C))))) (not (= (v (A) (^ (A) (B))) (A)))))
(7 (instantiate 1 ((v0 . (A)))) ((= (A) (A))))
(8 (resolve 6 (3) 7 (1)) ((not (= (^ (B) (A)) (^ (A) (B)))) (not (= (^ (^ (A) (B)) (C)) (^ (A) (^ (B) (C))))) (not (= (v (B) (A)) (v (A) (B)))) (not (= (v (v (A) (B)) (C)) (v (A) (v (B) (C))))) (not (= (v (A) (^ (A) (B))) (A)))))
(9 (flip 4 (1)) ((= (v (^ v2 v0) (^ v1 v0)) (^ v0 (v v1 v2)))))
(10 (instantiate 3 ((v0 . v65)(v1 . v66))) ((= (^ v65 (v v65 v66)) v65)))
(11 (instantiate 4 ((v0 . v65)(v1 . v65)(v2 . v66))) ((= (^ v65 (v v65 v66)) (v (^ v66 v65) (^ v65 v65)))))
(12 (paramod 10 (1 1) 11 (1 1)) ((= v65 (v (^ v66 v65) (^ v65 v65)))))
(13 (flip 12 (1)) ((= (v (^ v66 v65) (^ v65 v65)) v65)))
(14 (instantiate 13 ((v65 . v1)(v66 . v0))) ((= (v (^ v0 v1) (^ v1 v1)) v1)))
(15 (instantiate 3 ((v0 . (^ v0 v1))(v1 . (^ v1 v1)))) ((= (^ (^ v0 v1) (v (^ v0 v1) (^ v1 v1))) (^ v0 v1))))
(16 (paramod 14 (1 1) 15 (1 1 2)) ((= (^ (^ v0 v1) v1) (^ v0 v1))))
(17 (instantiate 4 ((v0 . v64))) ((= (^ v64 (v v1 v2)) (v (^ v2 v64) (^ v1 v64)))))
(18 (instantiate 16 ((v0 . v64)(v1 . (v v1 v2)))) ((= (^ (^ v64 (v v1 v2)) (v v1 v2)) (^ v64 (v v1 v2)))))
(19 (paramod 17 (1 1) 18 (1 1 1)) ((= (^ (v (^ v2 v64) (^ v1 v64)) (v v1 v2)) (^ v64 (v v1 v2)))))
(20 (instantiate 19 ((v1 . v2)(v2 . v0)(v64 . v1))) ((= (^ (v (^ v0 v1) (^ v2 v1)) (v v2 v0)) (^ v1 (v v2 v0)))))
(21 (instantiate 16 ((v1 . v64))) ((= (^ (^ v0 v64) v64) (^ v0 v64))))
(22 (instantiate 9 ((v0 . v64)(v1 . v65)(v2 . (^ v0 v64)))) ((= (v (^ (^ v0 v64) v64) (^ v65 v64)) (^ v64 (v v65 (^ v0 v64))))))
(23 (paramod 21 (1 1) 22 (1 1 1)) ((= (v (^ v0 v64) (^ v65 v64)) (^ v64 (v v65 (^ v0 v64))))))
(24 (instantiate 23 ((v64 . v1)(v65 . v2))) ((= (v (^ v0 v1) (^ v2 v1)) (^ v1 (v v2 (^ v0 v1))))))
(25 (instantiate 3 ((v0 . v66))) ((= (^ v66 (v v66 v1)) v66)))
(26 (instantiate 9 ((v0 . (v v66 v1))(v1 . v65)(v2 . v66))) ((= (v (^ v66 (v v66 v1)) (^ v65 (v v66 v1))) (^ (v v66 v1) (v v65 v66)))))
(27 (paramod 25 (1 1) 26 (1 1 1)) ((= (v v66 (^ v65 (v v66 v1))) (^ (v v66 v1) (v v65 v66)))))
(28 (instantiate 27 ((v1 . v2)(v65 . v1)(v66 . v0))) ((= (v v0 (^ v1 (v v0 v2))) (^ (v v0 v2) (v v1 v0)))))
(29 (instantiate 3 ((v0 . v65))) ((= (^ v65 (v v65 v1)) v65)))
(30 (instantiate 9 ((v0 . (v v65 v1))(v1 . v65)(v2 . v66))) ((= (v (^ v66 (v v65 v1)) (^ v65 (v v65 v1))) (^ (v v65 v1) (v v65 v66)))))
(31 (paramod 29 (1 1) 30 (1 1 2)) ((= (v (^ v66 (v v65 v1)) v65) (^ (v v65 v1) (v v65 v66)))))
(32 (instantiate 31 ((v1 . v2)(v65 . v1)(v66 . v0))) ((= (v (^ v0 (v v1 v2)) v1) (^ (v v1 v2) (v v1 v0)))))
(33 (instantiate 3 ((v0 . (^ v2 v0))(v1 . (^ v1 v0)))) ((= (^ (^ v2 v0) (v (^ v2 v0) (^ v1 v0))) (^ v2 v0))))
(34 (paramod 9 (1 1) 33 (1 1 2)) ((= (^ (^ v2 v0) (^ v0 (v v1 v2))) (^ v2 v0))))
(35 (instantiate 34 ((v0 . v1)(v1 . v2)(v2 . v0))) ((= (^ (^ v0 v1) (^ v1 (v v2 v0))) (^ v0 v1))))
(36 (instantiate 35 ((v0 . (^ v0 v1))(v1 . (^ v1 (v v2 v0)))(v2 . v66))) ((= (^ (^ (^ v0 v1) (^ v1 (v v2 v0))) (^ (^ v1 (v v2 v0)) (v v66 (^ v0 v1)))) (^ (^ v0 v1) (^ v1 (v v2 v0))))))
(37 (paramod 35 (1 1) 36 (1 1 1)) ((= (^ (^ v0 v1) (^ (^ v1 (v v2 v0)) (v v66 (^ v0 v1)))) (^ (^ v0 v1) (^ v1 (v v2 v0))))))
(38 (paramod 35 (1 1) 37 (1 2)) ((= (^ (^ v0 v1) (^ (^ v1 (v v2 v0)) (v v66 (^ v0 v1)))) (^ v0 v1))))
(39 (instantiate 38 ((v66 . v3))) ((= (^ (^ v0 v1) (^ (^ v1 (v v2 v0)) (v v3 (^ v0 v1)))) (^ v0 v1))))
(40 (instantiate 9 ((v0 . v65)(v1 . v66)(v2 . v64))) ((= (v (^ v64 v65) (^ v66 v65)) (^ v65 (v v66 v64)))))
(41 (instantiate 24 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (v (^ v64 v65) (^ v66 v65)) (^ v65 (v v66 (^ v64 v65))))))
(42 (paramod 40 (1 1) 41 (1 1)) ((= (^ v65 (v v66 v64)) (^ v65 (v v66 (^ v64 v65))))))
(43 (flip 42 (1)) ((= (^ v65 (v v66 (^ v64 v65))) (^ v65 (v v66 v64)))))
(44 (instantiate 43 ((v64 . v2)(v65 . v0)(v66 . v1))) ((= (^ v0 (v v1 (^ v2 v0))) (^ v0 (v v1 v2)))))
(45 (instantiate 14 ((v1 . v64))) ((= (v (^ v0 v64) (^ v64 v64)) v64)))
(46 (instantiate 44 ((v0 . v64)(v1 . (^ v0 v64))(v2 . v64))) ((= (^ v64 (v (^ v0 v64) (^ v64 v64))) (^ v64 (v (^ v0 v64) v64)))))
(47 (paramod 45 (1 1) 46 (1 1 2)) ((= (^ v64 v64) (^ v64 (v (^ v0 v64) v64)))))
(48 (flip 47 (1)) ((= (^ v64 (v (^ v0 v64) v64)) (^ v64 v64))))
(49 (instantiate 48 ((v0 . v1)(v64 . v0))) ((= (^ v0 (v (^ v1 v0) v0)) (^ v0 v0))))
(50 (instantiate 4 ((v0 . v64)(v1 . (^ v65 v64))(v2 . v64))) ((= (^ v64 (v (^ v65 v64) v64)) (v (^ v64 v64) (^ (^ v65 v64) v64)))))
(51 (instantiate 49 ((v0 . v64)(v1 . v65))) ((= (^ v64 (v (^ v65 v64) v64)) (^ v64 v64))))
(52 (paramod 50 (1 1) 51 (1 1)) ((= (v (^ v64 v64) (^ (^ v65 v64) v64)) (^ v64 v64))))
(53 (instantiate 16 ((v0 . v65)(v1 . v64))) ((= (^ (^ v65 v64) v64) (^ v65 v64))))
(54 (paramod 53 (1 1) 52 (1 1 2)) ((= (v (^ v64 v64) (^ v65 v64)) (^ v64 v64))))
(55 (instantiate 54 ((v64 . v0)(v65 . v1))) ((= (v (^ v0 v0) (^ v1 v0)) (^ v0 v0))))
(56 (instantiate 14 ((v0 . v65)(v1 . v65))) ((= (v (^ v65 v65) (^ v65 v65)) v65)))
(57 (instantiate 55 ((v0 . v65)(v1 . v65))) ((= (v (^ v65 v65) (^ v65 v65)) (^ v65 v65))))
(58 (paramod 56 (1 1) 57 (1 1)) ((= v65 (^ v65 v65))))
(59 (flip 58 (1)) ((= (^ v65 v65) v65)))
(60 (instantiate 59 ((v65 . v0))) ((= (^ v0 v0) v0)))
(61 (instantiate 9 ((v0 . v64)(v1 . v65)(v2 . v64))) ((= (v (^ v64 v64) (^ v65 v64)) (^ v64 (v v65 v64)))))
(62 (instantiate 55 ((v0 . v64)(v1 . v65))) ((= (v (^ v64 v64) (^ v65 v64)) (^ v64 v64))))
(63 (paramod 61 (1 1) 62 (1 1)) ((= (^ v64 (v v65 v64)) (^ v64 v64))))
(64 (instantiate 60 ((v0 . v64))) ((= (^ v64 v64) v64)))
(65 (paramod 64 (1 1) 63 (1 2)) ((= (^ v64 (v v65 v64)) v64)))
(66 (instantiate 65 ((v64 . v0)(v65 . v1))) ((= (^ v0 (v v1 v0)) v0)))
(67 (paramod 60 (1 1) 55 (1 1 1)) ((= (v v0 (^ v1 v0)) (^ v0 v0))))
(68 (paramod 60 (1 1) 67 (1 2)) ((= (v v0 (^ v1 v0)) v0)))
(69 (instantiate 60 ((v0 . v1))) ((= (^ v1 v1) v1)))
(70 (paramod 69 (1 1) 14 (1 1 2)) ((= (v (^ v0 v1) v1) v1)))
(71 (instantiate 4 ((v0 . (v v1 v2)))) ((= (^ (v v1 v2) (v v1 v2)) (v (^ v2 (v v1 v2)) (^ v1 (v v1 v2))))))
(72 (instantiate 60 ((v0 . (v v1 v2)))) ((= (^ (v v1 v2) (v v1 v2)) (v v1 v2))))
(73 (paramod 71 (1 1) 72 (1 1)) ((= (v (^ v2 (v v1 v2)) (^ v1 (v v1 v2))) (v v1 v2))))
(74 (instantiate 66 ((v0 . v2)(v1 . v1))) ((= (^ v2 (v v1 v2)) v2)))
(75 (paramod 74 (1 1) 73 (1 1 1)) ((= (v v2 (^ v1 (v v1 v2))) (v v1 v2))))
(76 (instantiate 3 ((v0 . v1)(v1 . v2))) ((= (^ v1 (v v1 v2)) v1)))
(77 (paramod 76 (1 1) 75 (1 1 2)) ((= (v v2 v1) (v v1 v2))))
(78 (instantiate 77 ((v2 . v0))) ((= (v v0 v1) (v v1 v0))))
(79 (instantiate 66 ((v0 . v65))) ((= (^ v65 (v v1 v65)) v65)))
(80 (instantiate 9 ((v0 . (v v1 v65))(v1 . v65)(v2 . v66))) ((= (v (^ v66 (v v1 v65)) (^ v65 (v v1 v65))) (^ (v v1 v65) (v v65 v66)))))
(81 (paramod 79 (1 1) 80 (1 1 2)) ((= (v (^ v66 (v v1 v65)) v65) (^ (v v1 v65) (v v65 v66)))))
(82 (instantiate 81 ((v65 . v2)(v66 . v0))) ((= (v (^ v0 (v v1 v2)) v2) (^ (v v1 v2) (v v2 v0)))))
(83 (instantiate 60 ((v0 . v64))) ((= (^ v64 v64) v64)))
(84 (instantiate 68 ((v0 . v64)(v1 . v64))) ((= (v v64 (^ v64 v64)) v64)))
(85 (paramod 83 (1 1) 84 (1 1 2)) ((= (v v64 v64) v64)))
(86 (instantiate 85 ((v64 . v0))) ((= (v v0 v0) v0)))
(87 (instantiate 44 ((v0 . v65))) ((= (^ v65 (v v1 (^ v2 v65))) (^ v65 (v v1 v2)))))
(88 (instantiate 68 ((v0 . (v v1 (^ v2 v65)))(v1 . v65))) ((= (v (v v1 (^ v2 v65)) (^ v65 (v v1 (^ v2 v65)))) (v v1 (^ v2 v65)))))
(89 (paramod 87 (1 1) 88 (1 1 2)) ((= (v (v v1 (^ v2 v65)) (^ v65 (v v1 v2))) (v v1 (^ v2 v65)))))
(90 (instantiate 89 ((v1 . v0)(v2 . v1)(v65 . v2))) ((= (v (v v0 (^ v1 v2)) (^ v2 (v v0 v1))) (v v0 (^ v1 v2)))))
(91 (instantiate 68 ((v0 . v66))) ((= (v v66 (^ v1 v66)) v66)))
(92 (instantiate 35 ((v0 . (^ v1 v66))(v1 . v65)(v2 . v66))) ((= (^ (^ (^ v1 v66) v65) (^ v65 (v v66 (^ v1 v66)))) (^ (^ v1 v66) v65))))
(93 (paramod 91 (1 1) 92 (1 1 2 2)) ((= (^ (^ (^ v1 v66) v65) (^ v65 v66)) (^ (^ v1 v66) v65))))
(94 (instantiate 93 ((v1 . v0)(v65 . v2)(v66 . v1))) ((= (^ (^ (^ v0 v1) v2) (^ v2 v1)) (^ (^ v0 v1) v2))))
(95 (instantiate 9 ((v1 . v2))) ((= (v (^ v2 v0) (^ v2 v0)) (^ v0 (v v2 v2)))))
(96 (instantiate 86 ((v0 . (^ v2 v0)))) ((= (v (^ v2 v0) (^ v2 v0)) (^ v2 v0))))
(97 (paramod 95 (1 1) 96 (1 1)) ((= (^ v0 (v v2 v2)) (^ v2 v0))))
(98 (instantiate 86 ((v0 . v2))) ((= (v v2 v2) v2)))
(99 (paramod 98 (1 1) 97 (1 1 2)) ((= (^ v0 v2) (^ v2 v0))))
(100 (instantiate 99 ((v2 . v1))) ((= (^ v0 v1) (^ v1 v0))))
(101 (instantiate 86 ((v0 . (^ v66 v65)))) ((= (v (^ v66 v65) (^ v66 v65)) (^ v66 v65))))
(102 (instantiate 20 ((v0 . v66)(v1 . v65)(v2 . v66))) ((= (^ (v (^ v66 v65) (^ v66 v65)) (v v66 v66)) (^ v65 (v v66 v66)))))
(103 (paramod 101 (1 1) 102 (1 1 1)) ((= (^ (^ v66 v65) (v v66 v66)) (^ v65 (v v66 v66)))))
(104 (instantiate 86 ((v0 . v66))) ((= (v v66 v66) v66)))
(105 (paramod 104 (1 1) 103 (1 1 2)) ((= (^ (^ v66 v65) v66) (^ v65 (v v66 v66)))))
(106 (instantiate 86 ((v0 . v66))) ((= (v v66 v66) v66)))
(107 (paramod 106 (1 1) 105 (1 2 2)) ((= (^ (^ v66 v65) v66) (^ v65 v66))))
(108 (instantiate 107 ((v65 . v1)(v66 . v0))) ((= (^ (^ v0 v1) v0) (^ v1 v0))))
(109 (instantiate 66 ((v0 . v66)(v1 . v64))) ((= (^ v66 (v v64 v66)) v66)))
(110 (instantiate 28 ((v0 . v64)(v1 . v66)(v2 . v66))) ((= (v v64 (^ v66 (v v64 v66))) (^ (v v64 v66) (v v66 v64)))))
(111 (paramod 109 (1 1) 110 (1 1 2)) ((= (v v64 v66) (^ (v v64 v66) (v v66 v64)))))
(112 (flip 111 (1)) ((= (^ (v v64 v66) (v v66 v64)) (v v64 v66))))
(113 (instantiate 112 ((v64 . v0)(v66 . v1))) ((= (^ (v v0 v1) (v v1 v0)) (v v0 v1))))
(114 (instantiate 3 ((v0 . v64)(v1 . v66))) ((= (^ v64 (v v64 v66)) v64)))
(115 (instantiate 28 ((v0 . v64)(v1 . v64)(v2 . v66))) ((= (v v64 (^ v64 (v v64 v66))) (^ (v v64 v66) (v v64 v64)))))
(116 (paramod 114 (1 1) 115 (1 1 2)) ((= (v v64 v64) (^ (v v64 v66) (v v64 v64)))))
(117 (instantiate 86 ((v0 . v64))) ((= (v v64 v64) v64)))
(118 (paramod 117 (1 1) 116 (1 1)) ((= v64 (^ (v v64 v66) (v v64 v64)))))
(119 (instantiate 86 ((v0 . v64))) ((= (v v64 v64) v64)))
(120 (paramod 119 (1 1) 118 (1 2 2)) ((= v64 (^ (v v64 v66) v64))))
(121 (flip 120 (1)) ((= (^ (v v64 v66) v64) v64)))
(122 (instantiate 121 ((v64 . v0)(v66 . v1))) ((= (^ (v v0 v1) v0) v0)))
(123 (instantiate 78 ((v0 . (^ v2 v0))(v1 . (^ v1 v0)))) ((= (v (^ v2 v0) (^ v1 v0)) (v (^ v1 v0) (^ v2 v0)))))
(124 (paramod 9 (1 1) 123 (1 1)) ((= (^ v0 (v v1 v2)) (v (^ v1 v0) (^ v2 v0)))))
(125 (flip 124 (1)) ((= (v (^ v1 v0) (^ v2 v0)) (^ v0 (v v1 v2)))))
(126 (instantiate 125 ((v0 . v1)(v1 . v0))) ((= (v (^ v0 v1) (^ v2 v1)) (^ v1 (v v0 v2)))))
(127 (instantiate 126 ((v0 . v2)(v1 . v0)(v2 . v1))) ((= (v (^ v2 v0) (^ v1 v0)) (^ v0 (v v2 v1)))))
(128 (paramod 127 (1 1) 9 (1 1)) ((= (^ v0 (v v2 v1)) (^ v0 (v v1 v2)))))
(129 (instantiate 128 ((v1 . v2)(v2 . v1))) ((= (^ v0 (v v1 v2)) (^ v0 (v v2 v1)))))
(130 (instantiate 44 ((v0 . v64))) ((= (^ v64 (v v1 (^ v2 v64))) (^ v64 (v v1 v2)))))
(131 (instantiate 100 ((v0 . v64)(v1 . (v v1 (^ v2 v64))))) ((= (^ v64 (v v1 (^ v2 v64))) (^ (v v1 (^ v2 v64)) v64))))
(132 (paramod 130 (1 1) 131 (1 1)) ((= (^ v64 (v v1 v2)) (^ (v v1 (^ v2 v64)) v64))))
(133 (flip 132 (1)) ((= (^ (v v1 (^ v2 v64)) v64) (^ v64 (v v1 v2)))))
(134 (instantiate 133 ((v1 . v0)(v2 . v1)(v64 . v2))) ((= (^ (v v0 (^ v1 v2)) v2) (^ v2 (v v0 v1)))))
(135 (instantiate 100 ((v0 . (^ v0 v1))(v1 . (^ v1 (v v2 v0))))) ((= (^ (^ v0 v1) (^ v1 (v v2 v0))) (^ (^ v1 (v v2 v0)) (^ v0 v1)))))
(136 (paramod 35 (1 1) 135 (1 1)) ((= (^ v0 v1) (^ (^ v1 (v v2 v0)) (^ v0 v1)))))
(137 (flip 136 (1)) ((= (^ (^ v1 (v v2 v0)) (^ v0 v1)) (^ v0 v1))))
(138 (instantiate 137 ((v0 . v2)(v1 . v0)(v2 . v1))) ((= (^ (^ v0 (v v1 v2)) (^ v2 v0)) (^ v2 v0))))
(139 (instantiate 16 ((v1 . v65))) ((= (^ (^ v0 v65) v65) (^ v0 v65))))
(140 (instantiate 100 ((v0 . (^ v0 v65))(v1 . v65))) ((= (^ (^ v0 v65) v65) (^ v65 (^ v0 v65)))))
(141 (paramod 139 (1 1) 140 (1 1)) ((= (^ v0 v65) (^ v65 (^ v0 v65)))))
(142 (flip 141 (1)) ((= (^ v65 (^ v0 v65)) (^ v0 v65))))
(143 (instantiate 142 ((v0 . v1)(v65 . v0))) ((= (^ v0 (^ v1 v0)) (^ v1 v0))))
(144 (instantiate 100 ((v0 . v64)(v1 . v65))) ((= (^ v64 v65) (^ v65 v64))))
(145 (instantiate 70 ((v0 . v64)(v1 . v65))) ((= (v (^ v64 v65) v65) v65)))
(146 (paramod 144 (1 1) 145 (1 1 1)) ((= (v (^ v65 v64) v65) v65)))
(147 (instantiate 146 ((v64 . v1)(v65 . v0))) ((= (v (^ v0 v1) v0) v0)))
(148 (instantiate 100 ((v0 . v64)(v1 . v65))) ((= (^ v64 v65) (^ v65 v64))))
(149 (instantiate 35 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (^ (^ v64 v65) (^ v65 (v v66 v64))) (^ v64 v65))))
(150 (paramod 148 (1 1) 149 (1 1 1)) ((= (^ (^ v65 v64) (^ v65 (v v66 v64))) (^ v64 v65))))
(151 (instantiate 150 ((v64 . v1)(v65 . v0)(v66 . v2))) ((= (^ (^ v0 v1) (^ v0 (v v2 v1))) (^ v1 v0))))
(152 (instantiate 100 ((v0 . v65)(v1 . v64))) ((= (^ v65 v64) (^ v64 v65))))
(153 (instantiate 68 ((v0 . v64)(v1 . v65))) ((= (v v64 (^ v65 v64)) v64)))
(154 (paramod 152 (1 1) 153 (1 1 2)) ((= (v v64 (^ v64 v65)) v64)))
(155 (instantiate 154 ((v64 . v0)(v65 . v1))) ((= (v v0 (^ v0 v1)) v0)))
(156 (instantiate 155 ((v0 . (A))(v1 . (B)))) ((= (v (A) (^ (A) (B))) (A))))
(157 (paramod 156 (1 1) 8 (5 1 1)) ((not (= (^ (B) (A)) (^ (A) (B)))) (not (= (^ (^ (A) (B)) (C)) (^ (A) (^ (B) (C))))) (not (= (v (B) (A)) (v (A) (B)))) (not (= (v (v (A) (B)) (C)) (v (A) (v (B) (C))))) (not (= (A) (A)))))
(158 (instantiate 100 ((v0 . (B))(v1 . (A)))) ((= (^ (B) (A)) (^ (A) (B)))))
(159 (resolve 157 (1) 158 (1)) ((not (= (^ (^ (A) (B)) (C)) (^ (A) (^ (B) (C))))) (not (= (v (B) (A)) (v (A) (B)))) (not (= (v (v (A) (B)) (C)) (v (A) (v (B) (C))))) (not (= (A) (A)))))
(160 (instantiate 78 ((v0 . (B))(v1 . (A)))) ((= (v (B) (A)) (v (A) (B)))))
(161 (resolve 159 (2) 160 (1)) ((not (= (^ (^ (A) (B)) (C)) (^ (A) (^ (B) (C))))) (not (= (v (v (A) (B)) (C)) (v (A) (v (B) (C))))) (not (= (A) (A)))))
(162 (instantiate 1 ((v0 . (A)))) ((= (A) (A))))
(163 (resolve 161 (3) 162 (1)) ((not (= (^ (^ (A) (B)) (C)) (^ (A) (^ (B) (C))))) (not (= (v (v (A) (B)) (C)) (v (A) (v (B) (C)))))))
(164 (instantiate 122 ((v0 . v64))) ((= (^ (v v64 v1) v64) v64)))
(165 (instantiate 44 ((v0 . v64)(v1 . v65)(v2 . (v v64 v1)))) ((= (^ v64 (v v65 (^ (v v64 v1) v64))) (^ v64 (v v65 (v v64 v1))))))
(166 (paramod 164 (1 1) 165 (1 1 2 2)) ((= (^ v64 (v v65 v64)) (^ v64 (v v65 (v v64 v1))))))
(167 (instantiate 66 ((v0 . v64)(v1 . v65))) ((= (^ v64 (v v65 v64)) v64)))
(168 (paramod 167 (1 1) 166 (1 1)) ((= v64 (^ v64 (v v65 (v v64 v1))))))
(169 (flip 168 (1)) ((= (^ v64 (v v65 (v v64 v1))) v64)))
(170 (instantiate 169 ((v1 . v2)(v64 . v0)(v65 . v1))) ((= (^ v0 (v v1 (v v0 v2))) v0)))
(171 (instantiate 44 ((v0 . v64)(v1 . v65))) ((= (^ v64 (v v65 (^ v2 v64))) (^ v64 (v v65 v2)))))
(172 (instantiate 32 ((v0 . v64)(v1 . v65)(v2 . (^ v2 v64)))) ((= (v (^ v64 (v v65 (^ v2 v64))) v65) (^ (v v65 (^ v2 v64)) (v v65 v64)))))
(173 (paramod 171 (1 1) 172 (1 1 1)) ((= (v (^ v64 (v v65 v2)) v65) (^ (v v65 (^ v2 v64)) (v v65 v64)))))
(174 (instantiate 32 ((v0 . v64)(v1 . v65)(v2 . v2))) ((= (v (^ v64 (v v65 v2)) v65) (^ (v v65 v2) (v v65 v64)))))
(175 (paramod 174 (1 1) 173 (1 1)) ((= (^ (v v65 v2) (v v65 v64)) (^ (v v65 (^ v2 v64)) (v v65 v64)))))
(176 (flip 175 (1)) ((= (^ (v v65 (^ v2 v64)) (v v65 v64)) (^ (v v65 v2) (v v65 v64)))))
(177 (instantiate 176 ((v2 . v1)(v64 . v2)(v65 . v0))) ((= (^ (v v0 (^ v1 v2)) (v v0 v2)) (^ (v v0 v1) (v v0 v2)))))
(178 (instantiate 147 ((v0 . v65))) ((= (v (^ v65 v1) v65) v65)))
(179 (instantiate 122 ((v0 . (^ v65 v1))(v1 . v65))) ((= (^ (v (^ v65 v1) v65) (^ v65 v1)) (^ v65 v1))))
(180 (paramod 178 (1 1) 179 (1 1 1)) ((= (^ v65 (^ v65 v1)) (^ v65 v1))))
(181 (instantiate 180 ((v65 . v0))) ((= (^ v0 (^ v0 v1)) (^ v0 v1))))
(182 (instantiate 155 ((v0 . v64)(v1 . v65))) ((= (v v64 (^ v64 v65)) v64)))
(183 (instantiate 39 ((v0 . v64)(v1 . v65)(v2 . v66)(v3 . v64))) ((= (^ (^ v64 v65) (^ (^ v65 (v v66 v64)) (v v64 (^ v64 v65)))) (^ v64 v65))))
(184 (paramod 182 (1 1) 183 (1 1 2 2)) ((= (^ (^ v64 v65) (^ (^ v65 (v v66 v64)) v64)) (^ v64 v65))))
(185 (instantiate 184 ((v64 . v0)(v65 . v1)(v66 . v2))) ((= (^ (^ v0 v1) (^ (^ v1 (v v2 v0)) v0)) (^ v0 v1))))
(186 (instantiate 108 ((v0 . v65))) ((= (^ (^ v65 v1) v65) (^ v1 v65))))
(187 (instantiate 155 ((v0 . (^ v65 v1))(v1 . v65))) ((= (v (^ v65 v1) (^ (^ v65 v1) v65)) (^ v65 v1))))
(188 (paramod 186 (1 1) 187 (1 1 2)) ((= (v (^ v65 v1) (^ v1 v65)) (^ v65 v1))))
(189 (instantiate 188 ((v65 . v0))) ((= (v (^ v0 v1) (^ v1 v0)) (^ v0 v1))))
(190 (instantiate 147 ((v0 . v66))) ((= (v (^ v66 v1) v66) v66)))
(191 (instantiate 170 ((v0 . (^ v66 v1))(v1 . v65)(v2 . v66))) ((= (^ (^ v66 v1) (v v65 (v (^ v66 v1) v66))) (^ v66 v1))))
(192 (paramod 190 (1 1) 191 (1 1 2 2)) ((= (^ (^ v66 v1) (v v65 v66)) (^ v66 v1))))
(193 (instantiate 192 ((v65 . v2)(v66 . v0))) ((= (^ (^ v0 v1) (v v2 v0)) (^ v0 v1))))
(194 (instantiate 100 ((v0 . v64)(v1 . (v v65 v66)))) ((= (^ v64 (v v65 v66)) (^ (v v65 v66) v64))))
(195 (instantiate 129 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (^ v64 (v v65 v66)) (^ v64 (v v66 v65)))))
(196 (paramod 194 (1 1) 195 (1 1)) ((= (^ (v v65 v66) v64) (^ v64 (v v66 v65)))))
(197 (instantiate 196 ((v64 . v2)(v65 . v0)(v66 . v1))) ((= (^ (v v0 v1) v2) (^ v2 (v v1 v0)))))
(198 (flip 197 (1)) ((= (^ v2 (v v1 v0)) (^ (v v0 v1) v2))))
(199 (instantiate 100 ((v0 . v64)(v1 . (v v65 v66)))) ((= (^ v64 (v v65 v66)) (^ (v v65 v66) v64))))
(200 (instantiate 82 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (v (^ v64 (v v65 v66)) v66) (^ (v v65 v66) (v v66 v64)))))
(201 (paramod 199 (1 1) 200 (1 1 1)) ((= (v (^ (v v65 v66) v64) v66) (^ (v v65 v66) (v v66 v64)))))
(202 (instantiate 201 ((v64 . v2)(v65 . v0)(v66 . v1))) ((= (v (^ (v v0 v1) v2) v1) (^ (v v0 v1) (v v1 v2)))))
(203 (instantiate 193 ((v0 . v66)(v2 . v65))) ((= (^ (^ v66 v1) (v v65 v66)) (^ v66 v1))))
(204 (instantiate 32 ((v0 . (^ v66 v1))(v1 . v65)(v2 . v66))) ((= (v (^ (^ v66 v1) (v v65 v66)) v65) (^ (v v65 v66) (v v65 (^ v66 v1))))))
(205 (paramod 203 (1 1) 204 (1 1 1)) ((= (v (^ v66 v1) v65) (^ (v v65 v66) (v v65 (^ v66 v1))))))
(206 (instantiate 205 ((v65 . v2)(v66 . v0))) ((= (v (^ v0 v1) v2) (^ (v v2 v0) (v v2 (^ v0 v1))))))
(207 (flip 206 (1)) ((= (^ (v v2 v0) (v v2 (^ v0 v1))) (v (^ v0 v1) v2))))
(208 (instantiate 100 ((v0 . v65)(v1 . v66))) ((= (^ v65 v66) (^ v66 v65))))
(209 (instantiate 90 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (v (v v64 (^ v65 v66)) (^ v66 (v v64 v65))) (v v64 (^ v65 v66)))))
(210 (paramod 208 (1 1) 209 (1 1 1 2)) ((= (v (v v64 (^ v66 v65)) (^ v66 (v v64 v65))) (v v64 (^ v65 v66)))))
(211 (instantiate 210 ((v64 . v0)(v65 . v2)(v66 . v1))) ((= (v (v v0 (^ v1 v2)) (^ v1 (v v0 v2))) (v v0 (^ v2 v1)))))
(212 (instantiate 100 ((v0 . (^ (^ v64 v65) v66))(v1 . (^ v66 v65)))) ((= (^ (^ (^ v64 v65) v66) (^ v66 v65)) (^ (^ v66 v65) (^ (^ v64 v65) v66)))))
(213 (instantiate 94 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (^ (^ (^ v64 v65) v66) (^ v66 v65)) (^ (^ v64 v65) v66))))
(214 (paramod 212 (1 1) 213 (1 1)) ((= (^ (^ v66 v65) (^ (^ v64 v65) v66)) (^ (^ v64 v65) v66))))
(215 (instantiate 214 ((v64 . v2)(v65 . v1)(v66 . v0))) ((= (^ (^ v0 v1) (^ (^ v2 v1) v0)) (^ (^ v2 v1) v0))))
(216 (instantiate 197 ((v0 . (^ v0 v1))(v1 . (^ v1 v0))(v2 . v66))) ((= (^ (v (^ v0 v1) (^ v1 v0)) v66) (^ v66 (v (^ v1 v0) (^ v0 v1))))))
(217 (paramod 189 (1 1) 216 (1 1 1)) ((= (^ (^ v0 v1) v66) (^ v66 (v (^ v1 v0) (^ v0 v1))))))
(218 (instantiate 189 ((v0 . v1)(v1 . v0))) ((= (v (^ v1 v0) (^ v0 v1)) (^ v1 v0))))
(219 (paramod 218 (1 1) 217 (1 2 2)) ((= (^ (^ v0 v1) v66) (^ v66 (^ v1 v0)))))
(220 (instantiate 219 ((v66 . v2))) ((= (^ (^ v0 v1) v2) (^ v2 (^ v1 v0)))))
(221 (instantiate 155 ((v0 . v65))) ((= (v v65 (^ v65 v1)) v65)))
(222 (instantiate 138 ((v0 . v64)(v1 . v65)(v2 . (^ v65 v1)))) ((= (^ (^ v64 (v v65 (^ v65 v1))) (^ (^ v65 v1) v64)) (^ (^ v65 v1) v64))))
(223 (paramod 221 (1 1) 222 (1 1 1 2)) ((= (^ (^ v64 v65) (^ (^ v65 v1) v64)) (^ (^ v65 v1) v64))))
(224 (instantiate 223 ((v1 . v2)(v64 . v0)(v65 . v1))) ((= (^ (^ v0 v1) (^ (^ v1 v2) v0)) (^ (^ v1 v2) v0))))
(225 (instantiate 224 ((v0 . v0)(v1 . v1)(v2 . (v v2 v0)))) ((= (^ (^ v0 v1) (^ (^ v1 (v v2 v0)) v0)) (^ (^ v1 (v v2 v0)) v0))))
(226 (paramod 225 (1 1) 185 (1 1)) ((= (^ (^ v1 (v v2 v0)) v0) (^ v0 v1))))
(227 (instantiate 226 ((v0 . v2)(v1 . v0)(v2 . v1))) ((= (^ (^ v0 (v v1 v2)) v2) (^ v2 v0))))
(228 (instantiate 16 ((v1 . (v v66 v65)))) ((= (^ (^ v0 (v v66 v65)) (v v66 v65)) (^ v0 (v v66 v65)))))
(229 (instantiate 151 ((v0 . (^ v0 (v v66 v65)))(v1 . v65)(v2 . v66))) ((= (^ (^ (^ v0 (v v66 v65)) v65) (^ (^ v0 (v v66 v65)) (v v66 v65))) (^ v65 (^ v0 (v v66 v65))))))
(230 (paramod 228 (1 1) 229 (1 1 2)) ((= (^ (^ (^ v0 (v v66 v65)) v65) (^ v0 (v v66 v65))) (^ v65 (^ v0 (v v66 v65))))))
(231 (instantiate 227 ((v0 . v0)(v1 . v66)(v2 . v65))) ((= (^ (^ v0 (v v66 v65)) v65) (^ v65 v0))))
(232 (paramod 231 (1 1) 230 (1 1 1)) ((= (^ (^ v65 v0) (^ v0 (v v66 v65))) (^ v65 (^ v0 (v v66 v65))))))
(233 (instantiate 35 ((v0 . v65)(v1 . v0)(v2 . v66))) ((= (^ (^ v65 v0) (^ v0 (v v66 v65))) (^ v65 v0))))
(234 (paramod 233 (1 1) 232 (1 1)) ((= (^ v65 v0) (^ v65 (^ v0 (v v66 v65))))))
(235 (flip 234 (1)) ((= (^ v65 (^ v0 (v v66 v65))) (^ v65 v0))))
(236 (instantiate 235 ((v0 . v1)(v65 . v0)(v66 . v2))) ((= (^ v0 (^ v1 (v v2 v0))) (^ v0 v1))))
(237 (instantiate 134 ((v2 . (v v65 v66)))) ((= (^ (v v0 (^ v1 (v v65 v66))) (v v65 v66)) (^ (v v65 v66) (v v0 v1)))))
(238 (instantiate 227 ((v0 . (v v0 (^ v1 (v v65 v66))))(v1 . v65)(v2 . v66))) ((= (^ (^ (v v0 (^ v1 (v v65 v66))) (v v65 v66)) v66) (^ v66 (v v0 (^ v1 (v v65 v66)))))))
(239 (paramod 237 (1 1) 238 (1 1 1)) ((= (^ (^ (v v65 v66) (v v0 v1)) v66) (^ v66 (v v0 (^ v1 (v v65 v66)))))))
(240 (flip 239 (1)) ((= (^ v66 (v v0 (^ v1 (v v65 v66)))) (^ (^ (v v65 v66) (v v0 v1)) v66))))
(241 (instantiate 240 ((v0 . v1)(v1 . v2)(v65 . v3)(v66 . v0))) ((= (^ v0 (v v1 (^ v2 (v v3 v0)))) (^ (^ (v v3 v0) (v v1 v2)) v0))))
(242 (instantiate 100 ((v0 . v64)(v1 . (v v65 v66)))) ((= (^ v64 (v v65 v66)) (^ (v v65 v66) v64))))
(243 (instantiate 227 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (^ (^ v64 (v v65 v66)) v66) (^ v66 v64))))
(244 (paramod 242 (1 1) 243 (1 1 1)) ((= (^ (^ (v v65 v66) v64) v66) (^ v66 v64))))
(245 (instantiate 244 ((v64 . v2)(v65 . v0)(v66 . v1))) ((= (^ (^ (v v0 v1) v2) v1) (^ v1 v2))))
(246 (instantiate 245 ((v0 . v3)(v1 . v0)(v2 . (v v1 v2)))) ((= (^ (^ (v v3 v0) (v v1 v2)) v0) (^ v0 (v v1 v2)))))
(247 (paramod 246 (1 1) 241 (1 2)) ((= (^ v0 (v v1 (^ v2 (v v3 v0)))) (^ v0 (v v1 v2)))))
(248 (instantiate 227 ((v2 . v66))) ((= (^ (^ v0 (v v1 v66)) v66) (^ v66 v0))))
(249 (instantiate 90 ((v0 . v64)(v1 . (^ v0 (v v1 v66)))(v2 . v66))) ((= (v (v v64 (^ (^ v0 (v v1 v66)) v66)) (^ v66 (v v64 (^ v0 (v v1 v66))))) (v v64 (^ (^ v0 (v v1 v66)) v66)))))
(250 (paramod 248 (1 1) 249 (1 1 1 2)) ((= (v (v v64 (^ v66 v0)) (^ v66 (v v64 (^ v0 (v v1 v66))))) (v v64 (^ (^ v0 (v v1 v66)) v66)))))
(251 (instantiate 247 ((v0 . v66)(v1 . v64)(v2 . v0)(v3 . v1))) ((= (^ v66 (v v64 (^ v0 (v v1 v66)))) (^ v66 (v v64 v0)))))
(252 (paramod 251 (1 1) 250 (1 1 2)) ((= (v (v v64 (^ v66 v0)) (^ v66 (v v64 v0))) (v v64 (^ (^ v0 (v v1 v66)) v66)))))
(253 (instantiate 211 ((v0 . v64)(v1 . v66)(v2 . v0))) ((= (v (v v64 (^ v66 v0)) (^ v66 (v v64 v0))) (v v64 (^ v0 v66)))))
(254 (paramod 253 (1 1) 252 (1 1)) ((= (v v64 (^ v0 v66)) (v v64 (^ (^ v0 (v v1 v66)) v66)))))
(255 (instantiate 227 ((v0 . v0)(v1 . v1)(v2 . v66))) ((= (^ (^ v0 (v v1 v66)) v66) (^ v66 v0))))
(256 (paramod 255 (1 1) 254 (1 2 2)) ((= (v v64 (^ v0 v66)) (v v64 (^ v66 v0)))))
(257 (instantiate 256 ((v0 . v1)(v64 . v0)(v66 . v2))) ((= (v v0 (^ v1 v2)) (v v0 (^ v2 v1)))))
(258 (instantiate 155 ((v0 . v66))) ((= (v v66 (^ v66 v1)) v66)))
(259 (instantiate 236 ((v0 . (^ v66 v1))(v1 . v65)(v2 . v66))) ((= (^ (^ v66 v1) (^ v65 (v v66 (^ v66 v1)))) (^ (^ v66 v1) v65))))
(260 (paramod 258 (1 1) 259 (1 1 2 2)) ((= (^ (^ v66 v1) (^ v65 v66)) (^ (^ v66 v1) v65))))
(261 (instantiate 260 ((v65 . v2)(v66 . v0))) ((= (^ (^ v0 v1) (^ v2 v0)) (^ (^ v0 v1) v2))))
(262 (instantiate 68 ((v0 . v66))) ((= (v v66 (^ v1 v66)) v66)))
(263 (instantiate 236 ((v0 . (^ v1 v66))(v1 . v65)(v2 . v66))) ((= (^ (^ v1 v66) (^ v65 (v v66 (^ v1 v66)))) (^ (^ v1 v66) v65))))
(264 (paramod 262 (1 1) 263 (1 1 2 2)) ((= (^ (^ v1 v66) (^ v65 v66)) (^ (^ v1 v66) v65))))
(265 (instantiate 264 ((v1 . v0)(v65 . v2)(v66 . v1))) ((= (^ (^ v0 v1) (^ v2 v1)) (^ (^ v0 v1) v2))))
(266 (instantiate 261 ((v0 . v0)(v1 . v1)(v2 . (^ v2 v1)))) ((= (^ (^ v0 v1) (^ (^ v2 v1) v0)) (^ (^ v0 v1) (^ v2 v1)))))
(267 (paramod 266 (1 1) 215 (1 1)) ((= (^ (^ v0 v1) (^ v2 v1)) (^ (^ v2 v1) v0))))
(268 (paramod 265 (1 1) 267 (1 1)) ((= (^ (^ v0 v1) v2) (^ (^ v2 v1) v0))))
(269 (instantiate 257 ((v0 . v64)(v1 . (v v0 v1))(v2 . (v v1 v0)))) ((= (v v64 (^ (v v0 v1) (v v1 v0))) (v v64 (^ (v v1 v0) (v v0 v1))))))
(270 (paramod 113 (1 1) 269 (1 1 2)) ((= (v v64 (v v0 v1)) (v v64 (^ (v v1 v0) (v v0 v1))))))
(271 (instantiate 113 ((v0 . v1)(v1 . v0))) ((= (^ (v v1 v0) (v v0 v1)) (v v1 v0))))
(272 (paramod 271 (1 1) 270 (1 2 2)) ((= (v v64 (v v0 v1)) (v v64 (v v1 v0)))))
(273 (instantiate 272 ((v0 . v1)(v1 . v2)(v64 . v0))) ((= (v v0 (v v1 v2)) (v v0 (v v2 v1)))))
(274 (instantiate 220 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (^ (^ v64 v65) v66) (^ v66 (^ v65 v64)))))
(275 (instantiate 268 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (^ (^ v64 v65) v66) (^ (^ v66 v65) v64))))
(276 (paramod 274 (1 1) 275 (1 1)) ((= (^ v66 (^ v65 v64)) (^ (^ v66 v65) v64))))
(277 (flip 276 (1)) ((= (^ (^ v66 v65) v64) (^ v66 (^ v65 v64)))))
(278 (instantiate 277 ((v64 . v2)(v65 . v1)(v66 . v0))) ((= (^ (^ v0 v1) v2) (^ v0 (^ v1 v2)))))
(279 (instantiate 278 ((v0 . (A))(v1 . (B))(v2 . (C)))) ((= (^ (^ (A) (B)) (C)) (^ (A) (^ (B) (C))))))
(280 (paramod 279 (1 1) 163 (1 1 1)) ((not (= (^ (A) (^ (B) (C))) (^ (A) (^ (B) (C))))) (not (= (v (v (A) (B)) (C)) (v (A) (v (B) (C)))))))
(281 (instantiate 1 ((v0 . (^ (A) (^ (B) (C)))))) ((= (^ (A) (^ (B) (C))) (^ (A) (^ (B) (C))))))
(282 (resolve 280 (1) 281 (1)) ((not (= (v (v (A) (B)) (C)) (v (A) (v (B) (C)))))))
(283 (instantiate 78 ((v0 . (A))(v1 . (B)))) ((= (v (A) (B)) (v (B) (A)))))
(284 (paramod 283 (1 1) 282 (1 1 1 1)) ((not (= (v (v (B) (A)) (C)) (v (A) (v (B) (C)))))))
(285 (instantiate 143 ((v0 . v65))) ((= (^ v65 (^ v1 v65)) (^ v1 v65))))
(286 (instantiate 177 ((v0 . v64)(v1 . v65)(v2 . (^ v1 v65)))) ((= (^ (v v64 (^ v65 (^ v1 v65))) (v v64 (^ v1 v65))) (^ (v v64 v65) (v v64 (^ v1 v65))))))
(287 (paramod 285 (1 1) 286 (1 1 1 2)) ((= (^ (v v64 (^ v1 v65)) (v v64 (^ v1 v65))) (^ (v v64 v65) (v v64 (^ v1 v65))))))
(288 (instantiate 60 ((v0 . (v v64 (^ v1 v65))))) ((= (^ (v v64 (^ v1 v65)) (v v64 (^ v1 v65))) (v v64 (^ v1 v65)))))
(289 (paramod 288 (1 1) 287 (1 1)) ((= (v v64 (^ v1 v65)) (^ (v v64 v65) (v v64 (^ v1 v65))))))
(290 (flip 289 (1)) ((= (^ (v v64 v65) (v v64 (^ v1 v65))) (v v64 (^ v1 v65)))))
(291 (instantiate 290 ((v1 . v2)(v64 . v0)(v65 . v1))) ((= (^ (v v0 v1) (v v0 (^ v2 v1))) (v v0 (^ v2 v1)))))
(292 (instantiate 122 ((v0 . v66))) ((= (^ (v v66 v1) v66) v66)))
(293 (instantiate 177 ((v0 . v64)(v1 . (v v66 v1))(v2 . v66))) ((= (^ (v v64 (^ (v v66 v1) v66)) (v v64 v66)) (^ (v v64 (v v66 v1)) (v v64 v66)))))
(294 (paramod 292 (1 1) 293 (1 1 1 2)) ((= (^ (v v64 v66) (v v64 v66)) (^ (v v64 (v v66 v1)) (v v64 v66)))))
(295 (instantiate 60 ((v0 . (v v64 v66)))) ((= (^ (v v64 v66) (v v64 v66)) (v v64 v66))))
(296 (paramod 295 (1 1) 294 (1 1)) ((= (v v64 v66) (^ (v v64 (v v66 v1)) (v v64 v66)))))
(297 (flip 296 (1)) ((= (^ (v v64 (v v66 v1)) (v v64 v66)) (v v64 v66))))
(298 (instantiate 297 ((v1 . v2)(v64 . v0)(v66 . v1))) ((= (^ (v v0 (v v1 v2)) (v v0 v1)) (v v0 v1))))
(299 (instantiate 100 ((v0 . (v v64 (^ v65 v66)))(v1 . (v v64 v66)))) ((= (^ (v v64 (^ v65 v66)) (v v64 v66)) (^ (v v64 v66) (v v64 (^ v65 v66))))))
(300 (instantiate 177 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (^ (v v64 (^ v65 v66)) (v v64 v66)) (^ (v v64 v65) (v v64 v66)))))
(301 (paramod 299 (1 1) 300 (1 1)) ((= (^ (v v64 v66) (v v64 (^ v65 v66))) (^ (v v64 v65) (v v64 v66)))))
(302 (instantiate 291 ((v0 . v64)(v1 . v66)(v2 . v65))) ((= (^ (v v64 v66) (v v64 (^ v65 v66))) (v v64 (^ v65 v66)))))
(303 (paramod 302 (1 1) 301 (1 1)) ((= (v v64 (^ v65 v66)) (^ (v v64 v65) (v v64 v66)))))
(304 (instantiate 303 ((v64 . v0)(v65 . v1)(v66 . v2))) ((= (v v0 (^ v1 v2)) (^ (v v0 v1) (v v0 v2)))))
(305 (instantiate 304 ((v0 . v2)(v1 . v0)(v2 . v1))) ((= (v v2 (^ v0 v1)) (^ (v v2 v0) (v v2 v1)))))
(306 (paramod 305 (1 1) 207 (1 1 2)) ((= (^ (v v2 v0) (^ (v v2 v0) (v v2 v1))) (v (^ v0 v1) v2))))
(307 (instantiate 181 ((v0 . (v v2 v0))(v1 . (v v2 v1)))) ((= (^ (v v2 v0) (^ (v v2 v0) (v v2 v1))) (^ (v v2 v0) (v v2 v1)))))
(308 (paramod 307 (1 1) 306 (1 1)) ((= (^ (v v2 v0) (v v2 v1)) (v (^ v0 v1) v2))))
(309 (instantiate 308 ((v0 . v1)(v1 . v2)(v2 . v0))) ((= (^ (v v0 v1) (v v0 v2)) (v (^ v1 v2) v0))))
(310 (instantiate 78 ((v0 . v64)(v1 . (v v65 v66)))) ((= (v v64 (v v65 v66)) (v (v v65 v66) v64))))
(311 (instantiate 273 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (v v64 (v v65 v66)) (v v64 (v v66 v65)))))
(312 (paramod 310 (1 1) 311 (1 1)) ((= (v (v v65 v66) v64) (v v64 (v v66 v65)))))
(313 (instantiate 312 ((v64 . v2)(v65 . v0)(v66 . v1))) ((= (v (v v0 v1) v2) (v v2 (v v1 v0)))))
(314 (instantiate 198 ((v0 . v65)(v1 . v64)(v2 . (v v64 (v v65 v66))))) ((= (^ (v v64 (v v65 v66)) (v v64 v65)) (^ (v v65 v64) (v v64 (v v65 v66))))))
(315 (instantiate 298 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (^ (v v64 (v v65 v66)) (v v64 v65)) (v v64 v65))))
(316 (paramod 314 (1 1) 315 (1 1)) ((= (^ (v v65 v64) (v v64 (v v65 v66))) (v v64 v65))))
(317 (instantiate 316 ((v64 . v1)(v65 . v0)(v66 . v2))) ((= (^ (v v0 v1) (v v1 (v v0 v2))) (v v1 v0))))
(318 (instantiate 298 ((v0 . v64))) ((= (^ (v v64 (v v1 v2)) (v v64 v1)) (v v64 v1))))
(319 (instantiate 202 ((v0 . v64)(v1 . (v v1 v2))(v2 . (v v64 v1)))) ((= (v (^ (v v64 (v v1 v2)) (v v64 v1)) (v v1 v2)) (^ (v v64 (v v1 v2)) (v (v v1 v2) (v v64 v1))))))
(320 (paramod 318 (1 1) 319 (1 1 1)) ((= (v (v v64 v1) (v v1 v2)) (^ (v v64 (v v1 v2)) (v (v v1 v2) (v v64 v1))))))
(321 (instantiate 317 ((v0 . v64)(v1 . (v v1 v2))(v2 . v1))) ((= (^ (v v64 (v v1 v2)) (v (v v1 v2) (v v64 v1))) (v (v v1 v2) v64))))
(322 (paramod 321 (1 1) 320 (1 2)) ((= (v (v v64 v1) (v v1 v2)) (v (v v1 v2) v64))))
(323 (instantiate 322 ((v64 . v0))) ((= (v (v v0 v1) (v v1 v2)) (v (v v1 v2) v0))))
(324 (instantiate 309 ((v0 . v64)(v1 . v65))) ((= (^ (v v64 v65) (v v64 v2)) (v (^ v65 v2) v64))))
(325 (instantiate 202 ((v0 . v64)(v1 . v65)(v2 . (v v64 v2)))) ((= (v (^ (v v64 v65) (v v64 v2)) v65) (^ (v v64 v65) (v v65 (v v64 v2))))))
(326 (paramod 324 (1 1) 325 (1 1 1)) ((= (v (v (^ v65 v2) v64) v65) (^ (v v64 v65) (v v65 (v v64 v2))))))
(327 (instantiate 317 ((v0 . v64)(v1 . v65)(v2 . v2))) ((= (^ (v v64 v65) (v v65 (v v64 v2))) (v v65 v64))))
(328 (paramod 327 (1 1) 326 (1 2)) ((= (v (v (^ v65 v2) v64) v65) (v v65 v64))))
(329 (instantiate 328 ((v2 . v1)(v64 . v2)(v65 . v0))) ((= (v (v (^ v0 v1) v2) v0) (v v0 v2))))
(330 (instantiate 122 ((v0 . v65))) ((= (^ (v v65 v1) v65) v65)))
(331 (instantiate 329 ((v0 . (v v65 v1))(v1 . v65)(v2 . v66))) ((= (v (v (^ (v v65 v1) v65) v66) (v v65 v1)) (v (v v65 v1) v66))))
(332 (paramod 330 (1 1) 331 (1 1 1 1)) ((= (v (v v65 v66) (v v65 v1)) (v (v v65 v1) v66))))
(333 (instantiate 332 ((v1 . v2)(v65 . v0)(v66 . v1))) ((= (v (v v0 v1) (v v0 v2)) (v (v v0 v2) v1))))
(334 (flip 333 (1)) ((= (v (v v0 v2) v1) (v (v v0 v1) (v v0 v2)))))
(335 (instantiate 313 ((v0 . v64)(v1 . v65)(v2 . (v v65 v66)))) ((= (v (v v64 v65) (v v65 v66)) (v (v v65 v66) (v v65 v64)))))
(336 (instantiate 323 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (v (v v64 v65) (v v65 v66)) (v (v v65 v66) v64))))
(337 (paramod 335 (1 1) 336 (1 1)) ((= (v (v v65 v66) (v v65 v64)) (v (v v65 v66) v64))))
(338 (instantiate 337 ((v64 . v2)(v65 . v0)(v66 . v1))) ((= (v (v v0 v1) (v v0 v2)) (v (v v0 v1) v2))))
(339 (paramod 338 (1 1) 334 (1 2)) ((= (v (v v0 v2) v1) (v (v v0 v1) v2))))
(340 (instantiate 339 ((v1 . v2)(v2 . v1))) ((= (v (v v0 v1) v2) (v (v v0 v2) v1))))
(341 (instantiate 78 ((v0 . (v v64 v65))(v1 . v66))) ((= (v (v v64 v65) v66) (v v66 (v v64 v65)))))
(342 (instantiate 340 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (v (v v64 v65) v66) (v (v v64 v66) v65))))
(343 (paramod 341 (1 1) 342 (1 1)) ((= (v v66 (v v64 v65)) (v (v v64 v66) v65))))
(344 (flip 343 (1)) ((= (v (v v64 v66) v65) (v v66 (v v64 v65)))))
(345 (instantiate 344 ((v64 . v0)(v65 . v2)(v66 . v1))) ((= (v (v v0 v1) v2) (v v1 (v v0 v2)))))
(346 (instantiate 345 ((v0 . (B))(v1 . (A))(v2 . (C)))) ((= (v (v (B) (A)) (C)) (v (A) (v (B) (C))))))
(347 (resolve 284 (1) 346 (1)) ())
)