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