;; ----- Otter 3.0.4, August 1995 -----
;; The job was started by mccune on gyro, Wed Nov  1 22:16:13 1995
;;
;;;; x=x.
;;;; x v x=x.
;;;; x^x=x.
;;;; x v y=y v x.
;;;; x^y=y^x.
;;;; (x v y) v z=x v (y v z).
;;;; (x^y)^z=x^ (y^z).
;;;; x^ (x v y)=x.
;;;; x v (x^y)=x.
;;;; x^ (y v (z^ (x v u)))= (x^ (y v (x^z))) v (x^ ((x^y) v (z^u))).
;;;; x v (y^ (z v (x^u)))= (x v (y^ (x v z)))^ (x v ((x v y)^ (z v u))).
;;;; (x v (y^z))^ (z v (x^y))= (z^ (x v (y^z))) v (x^ (y v z)).
;;;; A^ ((B v C)^ (B v D))!= (A^ ((B v C)^ (B v D)))^ ((A^ (B v (C^D))) v ((A^C) v (A^D))).
;;
;; ----> UNIT CONFLICT at 101.45 sec ----> 11478 [binary,11477.1,1.1] $F.
;;
(
(1 (input) ((= v0 v0)))
(2 (input) ((= (v v0 v0) v0)))
(3 (input) ((= (^ v0 v0) v0)))
(4 (input) ((= (v v0 v1) (v v1 v0))))
(5 (input) ((= (^ v0 v1) (^ v1 v0))))
(6 (input) ((= (v (v v0 v1) v2) (v v0 (v v1 v2)))))
(7 (input) ((= (^ (^ v0 v1) v2) (^ v0 (^ v1 v2)))))
(8 (input) ((= (^ v0 (v v0 v1)) v0)))
(9 (input) ((= (v v0 (^ v0 v1)) v0)))
(10 (input) ((= (^ v0 (v v1 (^ v2 (v v0 v3)))) (v (^ v0 (v v1 (^ v0 v2))) (^ v0 (v (^ v0 v1) (^ v2 v3)))))))
(11 (flip 10 (1)) ((= (v (^ v0 (v v1 (^ v0 v2))) (^ v0 (v (^ v0 v1) (^ v2 v3)))) (^ v0 (v v1 (^ v2 (v v0 v3)))))))
(12 (input) ((= (v v0 (^ v1 (v v2 (^ v0 v3)))) (^ (v v0 (^ v1 (v v0 v2))) (v v0 (^ (v v0 v1) (v v2 v3)))))))
(13 (input) ((= (^ (v v0 (^ v1 v2)) (v v2 (^ v0 v1))) (v (^ v2 (v v0 (^ v1 v2))) (^ v0 (v v1 v2))))))
(14 (flip 13 (1)) ((= (v (^ v2 (v v0 (^ v1 v2))) (^ v0 (v v1 v2))) (^ (v v0 (^ v1 v2)) (v v2 (^ v0 v1))))))
(15 (instantiate 14 ((v0 . v1)(v1 . v2)(v2 . v0))) ((= (v (^ v0 (v v1 (^ v2 v0))) (^ v1 (v v2 v0))) (^ (v v1 (^ v2 v0)) (v v0 (^ v1 v2))))))
(16 (input) ((not (= (^ (A) (^ (v (B) (C)) (v (B) (D)))) (^ (^ (A) (^ (v (B) (C)) (v (B) (D)))) (v (^ (A) (v (B) (^ (C) (D)))) (v (^ (A) (C)) (^ (A) (D)))))))))
(17 (instantiate 7 ((v0 . (A))(v1 . (^ (v (B) (C)) (v (B) (D))))(v2 . (v (^ (A) (v (B) (^ (C) (D)))) (v (^ (A) (C)) (^ (A) (D))))))) ((= (^ (^ (A) (^ (v (B) (C)) (v (B) (D)))) (v (^ (A) (v (B) (^ (C) (D)))) (v (^ (A) (C)) (^ (A) (D))))) (^ (A) (^ (^ (v (B) (C)) (v (B) (D))) (v (^ (A) (v (B) (^ (C) (D)))) (v (^ (A) (C)) (^ (A) (D)))))))))
(18 (paramod 17 (1 1) 16 (1 1 2)) ((not (= (^ (A) (^ (v (B) (C)) (v (B) (D)))) (^ (A) (^ (^ (v (B) (C)) (v (B) (D))) (v (^ (A) (v (B) (^ (C) (D)))) (v (^ (A) (C)) (^ (A) (D))))))))))
(19 (instantiate 7 ((v0 . (v (B) (C)))(v1 . (v (B) (D)))(v2 . (v (^ (A) (v (B) (^ (C) (D)))) (v (^ (A) (C)) (^ (A) (D))))))) ((= (^ (^ (v (B) (C)) (v (B) (D))) (v (^ (A) (v (B) (^ (C) (D)))) (v (^ (A) (C)) (^ (A) (D))))) (^ (v (B) (C)) (^ (v (B) (D)) (v (^ (A) (v (B) (^ (C) (D)))) (v (^ (A) (C)) (^ (A) (D)))))))))
(20 (paramod 19 (1 1) 18 (1 1 2 2)) ((not (= (^ (A) (^ (v (B) (C)) (v (B) (D)))) (^ (A) (^ (v (B) (C)) (^ (v (B) (D)) (v (^ (A) (v (B) (^ (C) (D)))) (v (^ (A) (C)) (^ (A) (D)))))))))))
(21 (flip 20 (1)) ((not (= (^ (A) (^ (v (B) (C)) (^ (v (B) (D)) (v (^ (A) (v (B) (^ (C) (D)))) (v (^ (A) (C)) (^ (A) (D))))))) (^ (A) (^ (v (B) (C)) (v (B) (D))))))))
(22 (flip 12 (1)) ((= (^ (v v0 (^ v1 (v v0 v2))) (v v0 (^ (v v0 v1) (v v2 v3)))) (v v0 (^ v1 (v v2 (^ v0 v3)))))))
(23 (instantiate 4 ((v0 . v64)(v1 . v65))) ((= (v v64 v65) (v v65 v64))))
(24 (instantiate 8 ((v0 . v64)(v1 . v65))) ((= (^ v64 (v v64 v65)) v64)))
(25 (paramod 23 (1 1) 24 (1 1 2)) ((= (^ v64 (v v65 v64)) v64)))
(26 (instantiate 25 ((v64 . v0)(v65 . v1))) ((= (^ v0 (v v1 v0)) v0)))
(27 (instantiate 5 ((v0 . v64)(v1 . (v v64 v65)))) ((= (^ v64 (v v64 v65)) (^ (v v64 v65) v64))))
(28 (instantiate 8 ((v0 . v64)(v1 . v65))) ((= (^ v64 (v v64 v65)) v64)))
(29 (paramod 27 (1 1) 28 (1 1)) ((= (^ (v v64 v65) v64) v64)))
(30 (instantiate 29 ((v64 . v0)(v65 . v1))) ((= (^ (v v0 v1) v0) v0)))
(31 (instantiate 4 ((v0 . v64)(v1 . v65))) ((= (v v64 v65) (v v65 v64))))
(32 (instantiate 6 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (v (v v64 v65) v66) (v v64 (v v65 v66)))))
(33 (paramod 31 (1 1) 32 (1 1 1)) ((= (v (v v65 v64) v66) (v v64 (v v65 v66)))))
(34 (instantiate 6 ((v0 . v65)(v1 . v64)(v2 . v66))) ((= (v (v v65 v64) v66) (v v65 (v v64 v66)))))
(35 (paramod 34 (1 1) 33 (1 1)) ((= (v v65 (v v64 v66)) (v v64 (v v65 v66)))))
(36 (instantiate 35 ((v64 . v1)(v65 . v0)(v66 . v2))) ((= (v v0 (v v1 v2)) (v v1 (v v0 v2)))))
(37 (instantiate 2 ((v0 . v65))) ((= (v v65 v65) v65)))
(38 (instantiate 6 ((v0 . v65)(v1 . v65)(v2 . v66))) ((= (v (v v65 v65) v66) (v v65 (v v65 v66)))))
(39 (paramod 37 (1 1) 38 (1 1 1)) ((= (v v65 v66) (v v65 (v v65 v66)))))
(40 (flip 39 (1)) ((= (v v65 (v v65 v66)) (v v65 v66))))
(41 (instantiate 40 ((v65 . v0)(v66 . v1))) ((= (v v0 (v v0 v1)) (v v0 v1))))
(42 (instantiate 4 ((v0 . (v v64 v65))(v1 . v66))) ((= (v (v v64 v65) v66) (v v66 (v v64 v65)))))
(43 (instantiate 6 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (v (v v64 v65) v66) (v v64 (v v65 v66)))))
(44 (paramod 42 (1 1) 43 (1 1)) ((= (v v66 (v v64 v65)) (v v64 (v v65 v66)))))
(45 (instantiate 44 ((v64 . v1)(v65 . v2)(v66 . v0))) ((= (v v0 (v v1 v2)) (v v1 (v v2 v0)))))
(46 (flip 45 (1)) ((= (v v1 (v v2 v0)) (v v0 (v v1 v2)))))
(47 (instantiate 5 ((v0 . v64)(v1 . v65))) ((= (^ v64 v65) (^ v65 v64))))
(48 (instantiate 9 ((v0 . v64)(v1 . v65))) ((= (v v64 (^ v64 v65)) v64)))
(49 (paramod 47 (1 1) 48 (1 1 2)) ((= (v v64 (^ v65 v64)) v64)))
(50 (instantiate 49 ((v64 . v0)(v65 . v1))) ((= (v v0 (^ v1 v0)) v0)))
(51 (instantiate 4 ((v0 . v64)(v1 . (^ v64 v65)))) ((= (v v64 (^ v64 v65)) (v (^ v64 v65) v64))))
(52 (instantiate 9 ((v0 . v64)(v1 . v65))) ((= (v v64 (^ v64 v65)) v64)))
(53 (paramod 51 (1 1) 52 (1 1)) ((= (v (^ v64 v65) v64) v64)))
(54 (instantiate 53 ((v64 . v0)(v65 . v1))) ((= (v (^ v0 v1) v0) v0)))
(55 (instantiate 9 ((v0 . v64))) ((= (v v64 (^ v64 v1)) v64)))
(56 (instantiate 6 ((v0 . v64)(v1 . (^ v64 v1))(v2 . v66))) ((= (v (v v64 (^ v64 v1)) v66) (v v64 (v (^ v64 v1) v66)))))
(57 (paramod 55 (1 1) 56 (1 1 1)) ((= (v v64 v66) (v v64 (v (^ v64 v1) v66)))))
(58 (flip 57 (1)) ((= (v v64 (v (^ v64 v1) v66)) (v v64 v66))))
(59 (instantiate 58 ((v64 . v0)(v66 . v2))) ((= (v v0 (v (^ v0 v1) v2)) (v v0 v2))))
(60 (instantiate 9 ((v0 . v65))) ((= (v v65 (^ v65 v1)) v65)))
(61 (instantiate 26 ((v0 . (^ v65 v1))(v1 . v65))) ((= (^ (^ v65 v1) (v v65 (^ v65 v1))) (^ v65 v1))))
(62 (paramod 60 (1 1) 61 (1 1 2)) ((= (^ (^ v65 v1) v65) (^ v65 v1))))
(63 (instantiate 7 ((v0 . v65)(v1 . v1)(v2 . v65))) ((= (^ (^ v65 v1) v65) (^ v65 (^ v1 v65)))))
(64 (paramod 63 (1 1) 62 (1 1)) ((= (^ v65 (^ v1 v65)) (^ v65 v1))))
(65 (instantiate 64 ((v65 . v0))) ((= (^ v0 (^ v1 v0)) (^ v0 v1))))
(66 (instantiate 6 ((v2 . v64))) ((= (v (v v0 v1) v64) (v v0 (v v1 v64)))))
(67 (instantiate 26 ((v0 . v64)(v1 . (v v0 v1)))) ((= (^ v64 (v (v v0 v1) v64)) v64)))
(68 (paramod 66 (1 1) 67 (1 1 2)) ((= (^ v64 (v v0 (v v1 v64))) v64)))
(69 (instantiate 68 ((v0 . v1)(v1 . v2)(v64 . v0))) ((= (^ v0 (v v1 (v v2 v0))) v0)))
(70 (instantiate 5 ((v0 . v64)(v1 . (v v65 v64)))) ((= (^ v64 (v v65 v64)) (^ (v v65 v64) v64))))
(71 (instantiate 26 ((v0 . v64)(v1 . v65))) ((= (^ v64 (v v65 v64)) v64)))
(72 (paramod 70 (1 1) 71 (1 1)) ((= (^ (v v65 v64) v64) v64)))
(73 (instantiate 72 ((v64 . v1)(v65 . v0))) ((= (^ (v v0 v1) v1) v1)))
(74 (instantiate 30 ((v0 . v65))) ((= (^ (v v65 v1) v65) v65)))
(75 (instantiate 9 ((v0 . (v v65 v1))(v1 . v65))) ((= (v (v v65 v1) (^ (v v65 v1) v65)) (v v65 v1))))
(76 (paramod 74 (1 1) 75 (1 1 2)) ((= (v (v v65 v1) v65) (v v65 v1))))
(77 (instantiate 6 ((v0 . v65)(v1 . v1)(v2 . v65))) ((= (v (v v65 v1) v65) (v v65 (v v1 v65)))))
(78 (paramod 77 (1 1) 76 (1 1)) ((= (v v65 (v v1 v65)) (v v65 v1))))
(79 (instantiate 78 ((v65 . v0))) ((= (v v0 (v v1 v0)) (v v0 v1))))
(80 (instantiate 4 ((v0 . v64)(v1 . (^ v65 v64)))) ((= (v v64 (^ v65 v64)) (v (^ v65 v64) v64))))
(81 (instantiate 50 ((v0 . v64)(v1 . v65))) ((= (v v64 (^ v65 v64)) v64)))
(82 (paramod 80 (1 1) 81 (1 1)) ((= (v (^ v65 v64) v64) v64)))
(83 (instantiate 82 ((v64 . v1)(v65 . v0))) ((= (v (^ v0 v1) v1) v1)))
(84 (instantiate 50 ((v0 . v64))) ((= (v v64 (^ v1 v64)) v64)))
(85 (instantiate 6 ((v0 . v64)(v1 . (^ v1 v64))(v2 . v66))) ((= (v (v v64 (^ v1 v64)) v66) (v v64 (v (^ v1 v64) v66)))))
(86 (paramod 84 (1 1) 85 (1 1 1)) ((= (v v64 v66) (v v64 (v (^ v1 v64) v66)))))
(87 (flip 86 (1)) ((= (v v64 (v (^ v1 v64) v66)) (v v64 v66))))
(88 (instantiate 87 ((v64 . v0)(v66 . v2))) ((= (v v0 (v (^ v1 v0) v2)) (v v0 v2))))
(89 (instantiate 30 ((v0 . v65))) ((= (^ (v v65 v1) v65) v65)))
(90 (instantiate 7 ((v0 . (v v65 v1))(v1 . v65)(v2 . v66))) ((= (^ (^ (v v65 v1) v65) v66) (^ (v v65 v1) (^ v65 v66)))))
(91 (paramod 89 (1 1) 90 (1 1 1)) ((= (^ v65 v66) (^ (v v65 v1) (^ v65 v66)))))
(92 (flip 91 (1)) ((= (^ (v v65 v1) (^ v65 v66)) (^ v65 v66))))
(93 (instantiate 92 ((v65 . v0)(v66 . v2))) ((= (^ (v v0 v1) (^ v0 v2)) (^ v0 v2))))
(94 (instantiate 5 ((v0 . v64)(v1 . v65))) ((= (^ v64 v65) (^ v65 v64))))
(95 (instantiate 7 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (^ (^ v64 v65) v66) (^ v64 (^ v65 v66)))))
(96 (paramod 94 (1 1) 95 (1 1 1)) ((= (^ (^ v65 v64) v66) (^ v64 (^ v65 v66)))))
(97 (instantiate 7 ((v0 . v65)(v1 . v64)(v2 . v66))) ((= (^ (^ v65 v64) v66) (^ v65 (^ v64 v66)))))
(98 (paramod 97 (1 1) 96 (1 1)) ((= (^ v65 (^ v64 v66)) (^ v64 (^ v65 v66)))))
(99 (instantiate 98 ((v64 . v1)(v65 . v0)(v66 . v2))) ((= (^ v0 (^ v1 v2)) (^ v1 (^ v0 v2)))))
(100 (instantiate 3 ((v0 . v65))) ((= (^ v65 v65) v65)))
(101 (instantiate 7 ((v0 . v65)(v1 . v65)(v2 . v66))) ((= (^ (^ v65 v65) v66) (^ v65 (^ v65 v66)))))
(102 (paramod 100 (1 1) 101 (1 1 1)) ((= (^ v65 v66) (^ v65 (^ v65 v66)))))
(103 (flip 102 (1)) ((= (^ v65 (^ v65 v66)) (^ v65 v66))))
(104 (instantiate 103 ((v65 . v0)(v66 . v1))) ((= (^ v0 (^ v0 v1)) (^ v0 v1))))
(105 (instantiate 5 ((v0 . (^ v64 v65))(v1 . v66))) ((= (^ (^ v64 v65) v66) (^ v66 (^ v64 v65)))))
(106 (instantiate 7 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (^ (^ v64 v65) v66) (^ v64 (^ v65 v66)))))
(107 (paramod 105 (1 1) 106 (1 1)) ((= (^ v66 (^ v64 v65)) (^ v64 (^ v65 v66)))))
(108 (instantiate 107 ((v64 . v1)(v65 . v2)(v66 . v0))) ((= (^ v0 (^ v1 v2)) (^ v1 (^ v2 v0)))))
(109 (flip 108 (1)) ((= (^ v1 (^ v2 v0)) (^ v0 (^ v1 v2)))))
(110 (instantiate 7 ((v2 . v64))) ((= (^ (^ v0 v1) v64) (^ v0 (^ v1 v64)))))
(111 (instantiate 50 ((v0 . v64)(v1 . (^ v0 v1)))) ((= (v v64 (^ (^ v0 v1) v64)) v64)))
(112 (paramod 110 (1 1) 111 (1 1 2)) ((= (v v64 (^ v0 (^ v1 v64))) v64)))
(113 (instantiate 112 ((v0 . v1)(v1 . v2)(v64 . v0))) ((= (v v0 (^ v1 (^ v2 v0))) v0)))
(114 (instantiate 7 ((v2 . v65))) ((= (^ (^ v0 v1) v65) (^ v0 (^ v1 v65)))))
(115 (instantiate 54 ((v0 . (^ v0 v1))(v1 . v65))) ((= (v (^ (^ v0 v1) v65) (^ v0 v1)) (^ v0 v1))))
(116 (paramod 114 (1 1) 115 (1 1 1)) ((= (v (^ v0 (^ v1 v65)) (^ v0 v1)) (^ v0 v1))))
(117 (instantiate 116 ((v65 . v2))) ((= (v (^ v0 (^ v1 v2)) (^ v0 v1)) (^ v0 v1))))
(118 (instantiate 6 ((v2 . v65))) ((= (v (v v0 v1) v65) (v v0 (v v1 v65)))))
(119 (instantiate 73 ((v0 . (v v0 v1))(v1 . v65))) ((= (^ (v (v v0 v1) v65) v65) v65)))
(120 (paramod 118 (1 1) 119 (1 1 1)) ((= (^ (v v0 (v v1 v65)) v65) v65)))
(121 (instantiate 120 ((v65 . v2))) ((= (^ (v v0 (v v1 v2)) v2) v2)))
(122 (instantiate 7 ((v2 . v65))) ((= (^ (^ v0 v1) v65) (^ v0 (^ v1 v65)))))
(123 (instantiate 83 ((v0 . (^ v0 v1))(v1 . v65))) ((= (v (^ (^ v0 v1) v65) v65) v65)))
(124 (paramod 122 (1 1) 123 (1 1 1)) ((= (v (^ v0 (^ v1 v65)) v65) v65)))
(125 (instantiate 124 ((v65 . v2))) ((= (v (^ v0 (^ v1 v2)) v2) v2)))
(126 (instantiate 83 ((v1 . v65))) ((= (v (^ v0 v65) v65) v65)))
(127 (instantiate 6 ((v0 . (^ v0 v65))(v1 . v65)(v2 . v66))) ((= (v (v (^ v0 v65) v65) v66) (v (^ v0 v65) (v v65 v66)))))
(128 (paramod 126 (1 1) 127 (1 1 1)) ((= (v v65 v66) (v (^ v0 v65) (v v65 v66)))))
(129 (flip 128 (1)) ((= (v (^ v0 v65) (v v65 v66)) (v v65 v66))))
(130 (instantiate 129 ((v65 . v1)(v66 . v2))) ((= (v (^ v0 v1) (v v1 v2)) (v v1 v2))))
(131 (instantiate 5 ((v0 . v64)(v1 . v66))) ((= (^ v64 v66) (^ v66 v64))))
(132 (instantiate 11 ((v0 . v64)(v1 . v65)(v2 . v66)(v3 . v67))) ((= (v (^ v64 (v v65 (^ v64 v66))) (^ v64 (v (^ v64 v65) (^ v66 v67)))) (^ v64 (v v65 (^ v66 (v v64 v67)))))))
(133 (paramod 131 (1 1) 132 (1 1 1 2 2)) ((= (v (^ v64 (v v65 (^ v66 v64))) (^ v64 (v (^ v64 v65) (^ v66 v67)))) (^ v64 (v v65 (^ v66 (v v64 v67)))))))
(134 (instantiate 133 ((v64 . v0)(v65 . v1)(v66 . v2)(v67 . v3))) ((= (v (^ v0 (v v1 (^ v2 v0))) (^ v0 (v (^ v0 v1) (^ v2 v3)))) (^ v0 (v v1 (^ v2 (v v0 v3)))))))
(135 (instantiate 6 ((v2 . (^ v64 v66)))) ((= (v (v v0 v1) (^ v64 v66)) (v v0 (v v1 (^ v64 v66))))))
(136 (instantiate 11 ((v0 . v64)(v1 . (v v0 v1))(v2 . v66)(v3 . v67))) ((= (v (^ v64 (v (v v0 v1) (^ v64 v66))) (^ v64 (v (^ v64 (v v0 v1)) (^ v66 v67)))) (^ v64 (v (v v0 v1) (^ v66 (v v64 v67)))))))
(137 (paramod 135 (1 1) 136 (1 1 1 2)) ((= (v (^ v64 (v v0 (v v1 (^ v64 v66)))) (^ v64 (v (^ v64 (v v0 v1)) (^ v66 v67)))) (^ v64 (v (v v0 v1) (^ v66 (v v64 v67)))))))
(138 (instantiate 6 ((v0 . v0)(v1 . v1)(v2 . (^ v66 (v v64 v67))))) ((= (v (v v0 v1) (^ v66 (v v64 v67))) (v v0 (v v1 (^ v66 (v v64 v67)))))))
(139 (paramod 138 (1 1) 137 (1 2 2)) ((= (v (^ v64 (v v0 (v v1 (^ v64 v66)))) (^ v64 (v (^ v64 (v v0 v1)) (^ v66 v67)))) (^ v64 (v v0 (v v1 (^ v66 (v v64 v67))))))))
(140 (instantiate 139 ((v0 . v1)(v1 . v2)(v64 . v0)(v66 . v3)(v67 . v4))) ((= (v (^ v0 (v v1 (v v2 (^ v0 v3)))) (^ v0 (v (^ v0 (v v1 v2)) (^ v3 v4)))) (^ v0 (v v1 (v v2 (^ v3 (v v0 v4))))))))
(141 (instantiate 5 ((v0 . v64)(v1 . v65))) ((= (^ v64 v65) (^ v65 v64))))
(142 (instantiate 11 ((v0 . v64)(v1 . v65)(v2 . v66)(v3 . v67))) ((= (v (^ v64 (v v65 (^ v64 v66))) (^ v64 (v (^ v64 v65) (^ v66 v67)))) (^ v64 (v v65 (^ v66 (v v64 v67)))))))
(143 (paramod 141 (1 1) 142 (1 1 2 2 1)) ((= (v (^ v64 (v v65 (^ v64 v66))) (^ v64 (v (^ v65 v64) (^ v66 v67)))) (^ v64 (v v65 (^ v66 (v v64 v67)))))))
(144 (instantiate 143 ((v64 . v0)(v65 . v1)(v66 . v2)(v67 . v3))) ((= (v (^ v0 (v v1 (^ v0 v2))) (^ v0 (v (^ v1 v0) (^ v2 v3)))) (^ v0 (v v1 (^ v2 (v v0 v3)))))))
(145 (instantiate 73 ((v1 . v67))) ((= (^ (v v0 v67) v67) v67)))
(146 (instantiate 11 ((v0 . v64)(v1 . v65)(v2 . (v v0 v67))(v3 . v67))) ((= (v (^ v64 (v v65 (^ v64 (v v0 v67)))) (^ v64 (v (^ v64 v65) (^ (v v0 v67) v67)))) (^ v64 (v v65 (^ (v v0 v67) (v v64 v67)))))))
(147 (paramod 145 (1 1) 146 (1 1 2 2 2)) ((= (v (^ v64 (v v65 (^ v64 (v v0 v67)))) (^ v64 (v (^ v64 v65) v67))) (^ v64 (v v65 (^ (v v0 v67) (v v64 v67)))))))
(148 (instantiate 147 ((v0 . v2)(v64 . v0)(v65 . v1)(v67 . v3))) ((= (v (^ v0 (v v1 (^ v0 (v v2 v3)))) (^ v0 (v (^ v0 v1) v3))) (^ v0 (v v1 (^ (v v2 v3) (v v0 v3)))))))
(149 (instantiate 26 ((v0 . v66))) ((= (^ v66 (v v1 v66)) v66)))
(150 (instantiate 11 ((v0 . v64)(v1 . v65)(v2 . v66)(v3 . (v v1 v66)))) ((= (v (^ v64 (v v65 (^ v64 v66))) (^ v64 (v (^ v64 v65) (^ v66 (v v1 v66))))) (^ v64 (v v65 (^ v66 (v v64 (v v1 v66))))))))
(151 (paramod 149 (1 1) 150 (1 1 2 2 2)) ((= (v (^ v64 (v v65 (^ v64 v66))) (^ v64 (v (^ v64 v65) v66))) (^ v64 (v v65 (^ v66 (v v64 (v v1 v66))))))))
(152 (instantiate 69 ((v0 . v66)(v1 . v64)(v2 . v1))) ((= (^ v66 (v v64 (v v1 v66))) v66)))
(153 (paramod 152 (1 1) 151 (1 2 2 2)) ((= (v (^ v64 (v v65 (^ v64 v66))) (^ v64 (v (^ v64 v65) v66))) (^ v64 (v v65 v66)))))
(154 (instantiate 153 ((v64 . v0)(v65 . v1)(v66 . v2))) ((= (v (^ v0 (v v1 (^ v0 v2))) (^ v0 (v (^ v0 v1) v2))) (^ v0 (v v1 v2)))))
(155 (instantiate 7 ((v2 . v64))) ((= (^ (^ v0 v1) v64) (^ v0 (^ v1 v64)))))
(156 (instantiate 65 ((v0 . v64)(v1 . (^ v0 v1)))) ((= (^ v64 (^ (^ v0 v1) v64)) (^ v64 (^ v0 v1)))))
(157 (paramod 155 (1 1) 156 (1 1 2)) ((= (^ v64 (^ v0 (^ v1 v64))) (^ v64 (^ v0 v1)))))
(158 (instantiate 157 ((v0 . v1)(v1 . v2)(v64 . v0))) ((= (^ v0 (^ v1 (^ v2 v0))) (^ v0 (^ v1 v2)))))
(159 (instantiate 65 ((v0 . v65))) ((= (^ v65 (^ v1 v65)) (^ v65 v1))))
(160 (instantiate 50 ((v0 . (^ v1 v65))(v1 . v65))) ((= (v (^ v1 v65) (^ v65 (^ v1 v65))) (^ v1 v65))))
(161 (paramod 159 (1 1) 160 (1 1 2)) ((= (v (^ v1 v65) (^ v65 v1)) (^ v1 v65))))
(162 (instantiate 161 ((v1 . v0)(v65 . v1))) ((= (v (^ v0 v1) (^ v1 v0)) (^ v0 v1))))
(163 (instantiate 65 ((v0 . v64))) ((= (^ v64 (^ v1 v64)) (^ v64 v1))))
(164 (instantiate 7 ((v0 . v64)(v1 . (^ v1 v64))(v2 . v66))) ((= (^ (^ v64 (^ v1 v64)) v66) (^ v64 (^ (^ v1 v64) v66)))))
(165 (paramod 163 (1 1) 164 (1 1 1)) ((= (^ (^ v64 v1) v66) (^ v64 (^ (^ v1 v64) v66)))))
(166 (instantiate 7 ((v0 . v64)(v1 . v1)(v2 . v66))) ((= (^ (^ v64 v1) v66) (^ v64 (^ v1 v66)))))
(167 (paramod 166 (1 1) 165 (1 1)) ((= (^ v64 (^ v1 v66)) (^ v64 (^ (^ v1 v64) v66)))))
(168 (instantiate 7 ((v0 . v1)(v1 . v64)(v2 . v66))) ((= (^ (^ v1 v64) v66) (^ v1 (^ v64 v66)))))
(169 (paramod 168 (1 1) 167 (1 2 2)) ((= (^ v64 (^ v1 v66)) (^ v64 (^ v1 (^ v64 v66))))))
(170 (flip 169 (1)) ((= (^ v64 (^ v1 (^ v64 v66))) (^ v64 (^ v1 v66)))))
(171 (instantiate 170 ((v64 . v0)(v66 . v2))) ((= (^ v0 (^ v1 (^ v0 v2))) (^ v0 (^ v1 v2)))))
(172 (instantiate 9 ((v0 . v66))) ((= (v v66 (^ v66 v1)) v66)))
(173 (instantiate 69 ((v0 . (^ v66 v1))(v1 . v65)(v2 . v66))) ((= (^ (^ v66 v1) (v v65 (v v66 (^ v66 v1)))) (^ v66 v1))))
(174 (paramod 172 (1 1) 173 (1 1 2 2)) ((= (^ (^ v66 v1) (v v65 v66)) (^ v66 v1))))
(175 (instantiate 7 ((v0 . v66)(v1 . v1)(v2 . (v v65 v66)))) ((= (^ (^ v66 v1) (v v65 v66)) (^ v66 (^ v1 (v v65 v66))))))
(176 (paramod 175 (1 1) 174 (1 1)) ((= (^ v66 (^ v1 (v v65 v66))) (^ v66 v1))))
(177 (instantiate 176 ((v65 . v2)(v66 . v0))) ((= (^ v0 (^ v1 (v v2 v0))) (^ v0 v1))))
(178 (instantiate 4 ((v0 . v66)(v1 . v64))) ((= (v v66 v64) (v v64 v66))))
(179 (instantiate 69 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (^ v64 (v v65 (v v66 v64))) v64)))
(180 (paramod 178 (1 1) 179 (1 1 2 2)) ((= (^ v64 (v v65 (v v64 v66))) v64)))
(181 (instantiate 180 ((v64 . v0)(v65 . v1)(v66 . v2))) ((= (^ v0 (v v1 (v v0 v2))) v0)))
(182 (instantiate 79 ((v0 . v65))) ((= (v v65 (v v1 v65)) (v v65 v1))))
(183 (instantiate 26 ((v0 . (v v1 v65))(v1 . v65))) ((= (^ (v v1 v65) (v v65 (v v1 v65))) (v v1 v65))))
(184 (paramod 182 (1 1) 183 (1 1 2)) ((= (^ (v v1 v65) (v v65 v1)) (v v1 v65))))
(185 (instantiate 184 ((v1 . v0)(v65 . v1))) ((= (^ (v v0 v1) (v v1 v0)) (v v0 v1))))
(186 (instantiate 54 ((v0 . (^ v64 v67)))) ((= (v (^ (^ v64 v67) v1) (^ v64 v67)) (^ v64 v67))))
(187 (instantiate 12 ((v0 . v64)(v1 . v65)(v2 . (^ (^ v64 v67) v1))(v3 . v67))) ((= (v v64 (^ v65 (v (^ (^ v64 v67) v1) (^ v64 v67)))) (^ (v v64 (^ v65 (v v64 (^ (^ v64 v67) v1)))) (v v64 (^ (v v64 v65) (v (^ (^ v64 v67) v1) v67)))))))
(188 (paramod 186 (1 1) 187 (1 1 2 2)) ((= (v v64 (^ v65 (^ v64 v67))) (^ (v v64 (^ v65 (v v64 (^ (^ v64 v67) v1)))) (v v64 (^ (v v64 v65) (v (^ (^ v64 v67) v1) v67)))))))
(189 (instantiate 7 ((v0 . v64)(v1 . v67)(v2 . v1))) ((= (^ (^ v64 v67) v1) (^ v64 (^ v67 v1)))))
(190 (paramod 189 (1 1) 188 (1 2 1 2 2 2)) ((= (v v64 (^ v65 (^ v64 v67))) (^ (v v64 (^ v65 (v v64 (^ v64 (^ v67 v1))))) (v v64 (^ (v v64 v65) (v (^ (^ v64 v67) v1) v67)))))))
(191 (instantiate 9 ((v0 . v64)(v1 . (^ v67 v1)))) ((= (v v64 (^ v64 (^ v67 v1))) v64)))
(192 (paramod 191 (1 1) 190 (1 2 1 2 2)) ((= (v v64 (^ v65 (^ v64 v67))) (^ (v v64 (^ v65 v64)) (v v64 (^ (v v64 v65) (v (^ (^ v64 v67) v1) v67)))))))
(193 (instantiate 50 ((v0 . v64)(v1 . v65))) ((= (v v64 (^ v65 v64)) v64)))
(194 (paramod 193 (1 1) 192 (1 2 1)) ((= (v v64 (^ v65 (^ v64 v67))) (^ v64 (v v64 (^ (v v64 v65) (v (^ (^ v64 v67) v1) v67)))))))
(195 (instantiate 7 ((v0 . v64)(v1 . v67)(v2 . v1))) ((= (^ (^ v64 v67) v1) (^ v64 (^ v67 v1)))))
(196 (paramod 195 (1 1) 194 (1 2 2 2 2 1)) ((= (v v64 (^ v65 (^ v64 v67))) (^ v64 (v v64 (^ (v v64 v65) (v (^ v64 (^ v67 v1)) v67)))))))
(197 (instantiate 8 ((v0 . v64)(v1 . (^ (v v64 v65) (v (^ v64 (^ v67 v1)) v67))))) ((= (^ v64 (v v64 (^ (v v64 v65) (v (^ v64 (^ v67 v1)) v67)))) v64)))
(198 (paramod 197 (1 1) 196 (1 2)) ((= (v v64 (^ v65 (^ v64 v67))) v64)))
(199 (instantiate 198 ((v64 . v0)(v65 . v1)(v67 . v2))) ((= (v v0 (^ v1 (^ v0 v2))) v0)))
(200 (instantiate 8 ((v0 . v66))) ((= (^ v66 (v v66 v1)) v66)))
(201 (instantiate 113 ((v0 . (v v66 v1))(v1 . v65)(v2 . v66))) ((= (v (v v66 v1) (^ v65 (^ v66 (v v66 v1)))) (v v66 v1))))
(202 (paramod 200 (1 1) 201 (1 1 2 2)) ((= (v (v v66 v1) (^ v65 v66)) (v v66 v1))))
(203 (instantiate 6 ((v0 . v66)(v1 . v1)(v2 . (^ v65 v66)))) ((= (v (v v66 v1) (^ v65 v66)) (v v66 (v v1 (^ v65 v66))))))
(204 (paramod 203 (1 1) 202 (1 1)) ((= (v v66 (v v1 (^ v65 v66))) (v v66 v1))))
(205 (instantiate 204 ((v65 . v2)(v66 . v0))) ((= (v v0 (v v1 (^ v2 v0))) (v v0 v1))))
(206 (instantiate 4 ((v0 . v65)(v1 . v66))) ((= (v v65 v66) (v v66 v65))))
(207 (instantiate 121 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (^ (v v64 (v v65 v66)) v66) v66)))
(208 (paramod 206 (1 1) 207 (1 1 1 2)) ((= (^ (v v64 (v v66 v65)) v66) v66)))
(209 (instantiate 208 ((v64 . v0)(v65 . v2)(v66 . v1))) ((= (^ (v v0 (v v1 v2)) v1) v1)))
(210 (instantiate 26 ((v0 . v65))) ((= (^ v65 (v v1 v65)) v65)))
(211 (instantiate 125 ((v0 . v64)(v1 . v65)(v2 . (v v1 v65)))) ((= (v (^ v64 (^ v65 (v v1 v65))) (v v1 v65)) (v v1 v65))))
(212 (paramod 210 (1 1) 211 (1 1 1 2)) ((= (v (^ v64 v65) (v v1 v65)) (v v1 v65))))
(213 (instantiate 212 ((v1 . v2)(v64 . v0)(v65 . v1))) ((= (v (^ v0 v1) (v v2 v1)) (v v2 v1))))
(214 (instantiate 54 ((v0 . (^ v66 v64)))) ((= (v (^ (^ v66 v64) v1) (^ v66 v64)) (^ v66 v64))))
(215 (instantiate 15 ((v0 . v64)(v1 . (^ (^ v66 v64) v1))(v2 . v66))) ((= (v (^ v64 (v (^ (^ v66 v64) v1) (^ v66 v64))) (^ (^ (^ v66 v64) v1) (v v66 v64))) (^ (v (^ (^ v66 v64) v1) (^ v66 v64)) (v v64 (^ (^ (^ v66 v64) v1) v66))))))
(216 (paramod 214 (1 1) 215 (1 1 1 2)) ((= (v (^ v64 (^ v66 v64)) (^ (^ (^ v66 v64) v1) (v v66 v64))) (^ (v (^ (^ v66 v64) v1) (^ v66 v64)) (v v64 (^ (^ (^ v66 v64) v1) v66))))))
(217 (instantiate 65 ((v0 . v64)(v1 . v66))) ((= (^ v64 (^ v66 v64)) (^ v64 v66))))
(218 (paramod 217 (1 1) 216 (1 1 1)) ((= (v (^ v64 v66) (^ (^ (^ v66 v64) v1) (v v66 v64))) (^ (v (^ (^ v66 v64) v1) (^ v66 v64)) (v v64 (^ (^ (^ v66 v64) v1) v66))))))
(219 (instantiate 7 ((v0 . v66)(v1 . v64)(v2 . v1))) ((= (^ (^ v66 v64) v1) (^ v66 (^ v64 v1)))))
(220 (paramod 219 (1 1) 218 (1 1 2 1)) ((= (v (^ v64 v66) (^ (^ v66 (^ v64 v1)) (v v66 v64))) (^ (v (^ (^ v66 v64) v1) (^ v66 v64)) (v v64 (^ (^ (^ v66 v64) v1) v66))))))
(221 (instantiate 7 ((v0 . v66)(v1 . (^ v64 v1))(v2 . (v v66 v64)))) ((= (^ (^ v66 (^ v64 v1)) (v v66 v64)) (^ v66 (^ (^ v64 v1) (v v66 v64))))))
(222 (paramod 221 (1 1) 220 (1 1 2)) ((= (v (^ v64 v66) (^ v66 (^ (^ v64 v1) (v v66 v64)))) (^ (v (^ (^ v66 v64) v1) (^ v66 v64)) (v v64 (^ (^ (^ v66 v64) v1) v66))))))
(223 (instantiate 7 ((v0 . v64)(v1 . v1)(v2 . (v v66 v64)))) ((= (^ (^ v64 v1) (v v66 v64)) (^ v64 (^ v1 (v v66 v64))))))
(224 (paramod 223 (1 1) 222 (1 1 2 2)) ((= (v (^ v64 v66) (^ v66 (^ v64 (^ v1 (v v66 v64))))) (^ (v (^ (^ v66 v64) v1) (^ v66 v64)) (v v64 (^ (^ (^ v66 v64) v1) v66))))))
(225 (instantiate 177 ((v0 . v64)(v1 . v1)(v2 . v66))) ((= (^ v64 (^ v1 (v v66 v64))) (^ v64 v1))))
(226 (paramod 225 (1 1) 224 (1 1 2 2)) ((= (v (^ v64 v66) (^ v66 (^ v64 v1))) (^ (v (^ (^ v66 v64) v1) (^ v66 v64)) (v v64 (^ (^ (^ v66 v64) v1) v66))))))
(227 (instantiate 7 ((v0 . v66)(v1 . v64)(v2 . v1))) ((= (^ (^ v66 v64) v1) (^ v66 (^ v64 v1)))))
(228 (paramod 227 (1 1) 226 (1 2 1 1)) ((= (v (^ v64 v66) (^ v66 (^ v64 v1))) (^ (v (^ v66 (^ v64 v1)) (^ v66 v64)) (v v64 (^ (^ (^ v66 v64) v1) v66))))))
(229 (instantiate 117 ((v0 . v66)(v1 . v64)(v2 . v1))) ((= (v (^ v66 (^ v64 v1)) (^ v66 v64)) (^ v66 v64))))
(230 (paramod 229 (1 1) 228 (1 2 1)) ((= (v (^ v64 v66) (^ v66 (^ v64 v1))) (^ (^ v66 v64) (v v64 (^ (^ (^ v66 v64) v1) v66))))))
(231 (instantiate 7 ((v0 . v66)(v1 . v64)(v2 . v1))) ((= (^ (^ v66 v64) v1) (^ v66 (^ v64 v1)))))
(232 (paramod 231 (1 1) 230 (1 2 2 2 1)) ((= (v (^ v64 v66) (^ v66 (^ v64 v1))) (^ (^ v66 v64) (v v64 (^ (^ v66 (^ v64 v1)) v66))))))
(233 (instantiate 7 ((v0 . v66)(v1 . (^ v64 v1))(v2 . v66))) ((= (^ (^ v66 (^ v64 v1)) v66) (^ v66 (^ (^ v64 v1) v66)))))
(234 (paramod 233 (1 1) 232 (1 2 2 2)) ((= (v (^ v64 v66) (^ v66 (^ v64 v1))) (^ (^ v66 v64) (v v64 (^ v66 (^ (^ v64 v1) v66)))))))
(235 (instantiate 7 ((v0 . v64)(v1 . v1)(v2 . v66))) ((= (^ (^ v64 v1) v66) (^ v64 (^ v1 v66)))))
(236 (paramod 235 (1 1) 234 (1 2 2 2 2)) ((= (v (^ v64 v66) (^ v66 (^ v64 v1))) (^ (^ v66 v64) (v v64 (^ v66 (^ v64 (^ v1 v66))))))))
(237 (instantiate 158 ((v0 . v66)(v1 . v64)(v2 . v1))) ((= (^ v66 (^ v64 (^ v1 v66))) (^ v66 (^ v64 v1)))))
(238 (paramod 237 (1 1) 236 (1 2 2 2)) ((= (v (^ v64 v66) (^ v66 (^ v64 v1))) (^ (^ v66 v64) (v v64 (^ v66 (^ v64 v1)))))))
(239 (instantiate 199 ((v0 . v64)(v1 . v66)(v2 . v1))) ((= (v v64 (^ v66 (^ v64 v1))) v64)))
(240 (paramod 239 (1 1) 238 (1 2 2)) ((= (v (^ v64 v66) (^ v66 (^ v64 v1))) (^ (^ v66 v64) v64))))
(241 (instantiate 7 ((v0 . v66)(v1 . v64)(v2 . v64))) ((= (^ (^ v66 v64) v64) (^ v66 (^ v64 v64)))))
(242 (paramod 241 (1 1) 240 (1 2)) ((= (v (^ v64 v66) (^ v66 (^ v64 v1))) (^ v66 (^ v64 v64)))))
(243 (instantiate 3 ((v0 . v64))) ((= (^ v64 v64) v64)))
(244 (paramod 243 (1 1) 242 (1 2 2)) ((= (v (^ v64 v66) (^ v66 (^ v64 v1))) (^ v66 v64))))
(245 (instantiate 244 ((v1 . v2)(v64 . v0)(v66 . v1))) ((= (v (^ v0 v1) (^ v1 (^ v0 v2))) (^ v1 v0))))
(246 (instantiate 73 ((v0 . (^ v0 (v v1 (^ v2 v0))))(v1 . (^ v1 (v v2 v0))))) ((= (^ (v (^ v0 (v v1 (^ v2 v0))) (^ v1 (v v2 v0))) (^ v1 (v v2 v0))) (^ v1 (v v2 v0)))))
(247 (paramod 15 (1 1) 246 (1 1 1)) ((= (^ (^ (v v1 (^ v2 v0)) (v v0 (^ v1 v2))) (^ v1 (v v2 v0))) (^ v1 (v v2 v0)))))
(248 (instantiate 7 ((v0 . (v v1 (^ v2 v0)))(v1 . (v v0 (^ v1 v2)))(v2 . (^ v1 (v v2 v0))))) ((= (^ (^ (v v1 (^ v2 v0)) (v v0 (^ v1 v2))) (^ v1 (v v2 v0))) (^ (v v1 (^ v2 v0)) (^ (v v0 (^ v1 v2)) (^ v1 (v v2 v0)))))))
(249 (paramod 248 (1 1) 247 (1 1)) ((= (^ (v v1 (^ v2 v0)) (^ (v v0 (^ v1 v2)) (^ v1 (v v2 v0)))) (^ v1 (v v2 v0)))))
(250 (instantiate 249 ((v0 . v2)(v1 . v0)(v2 . v1))) ((= (^ (v v0 (^ v1 v2)) (^ (v v2 (^ v0 v1)) (^ v0 (v v1 v2)))) (^ v0 (v v1 v2)))))
(251 (instantiate 9 ((v0 . v65))) ((= (v v65 (^ v65 v1)) v65)))
(252 (instantiate 36 ((v0 . v64)(v1 . v65)(v2 . (^ v65 v1)))) ((= (v v64 (v v65 (^ v65 v1))) (v v65 (v v64 (^ v65 v1))))))
(253 (paramod 251 (1 1) 252 (1 1 2)) ((= (v v64 v65) (v v65 (v v64 (^ v65 v1))))))
(254 (flip 253 (1)) ((= (v v65 (v v64 (^ v65 v1))) (v v64 v65))))
(255 (instantiate 254 ((v1 . v2)(v64 . v1)(v65 . v0))) ((= (v v0 (v v1 (^ v0 v2))) (v v1 v0))))
(256 (instantiate 83 ((v1 . (v v65 v66)))) ((= (v (^ v0 (v v65 v66)) (v v65 v66)) (v v65 v66))))
(257 (instantiate 36 ((v0 . (^ v0 (v v65 v66)))(v1 . v65)(v2 . v66))) ((= (v (^ v0 (v v65 v66)) (v v65 v66)) (v v65 (v (^ v0 (v v65 v66)) v66)))))
(258 (paramod 256 (1 1) 257 (1 1)) ((= (v v65 v66) (v v65 (v (^ v0 (v v65 v66)) v66)))))
(259 (flip 258 (1)) ((= (v v65 (v (^ v0 (v v65 v66)) v66)) (v v65 v66))))
(260 (instantiate 259 ((v0 . v1)(v65 . v0)(v66 . v2))) ((= (v v0 (v (^ v1 (v v0 v2)) v2)) (v v0 v2))))
(261 (instantiate 4 ((v0 . v65)(v1 . v66))) ((= (v v65 v66) (v v66 v65))))
(262 (instantiate 45 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (v v64 (v v65 v66)) (v v65 (v v66 v64)))))
(263 (paramod 261 (1 1) 262 (1 1 2)) ((= (v v64 (v v66 v65)) (v v65 (v v66 v64)))))
(264 (instantiate 263 ((v64 . v0)(v65 . v2)(v66 . v1))) ((= (v v0 (v v1 v2)) (v v2 (v v1 v0)))))
(265 (instantiate 59 ((v0 . v65)(v2 . v66))) ((= (v v65 (v (^ v65 v1) v66)) (v v65 v66))))
(266 (instantiate 181 ((v0 . (^ v65 v1))(v1 . v65)(v2 . v66))) ((= (^ (^ v65 v1) (v v65 (v (^ v65 v1) v66))) (^ v65 v1))))
(267 (paramod 265 (1 1) 266 (1 1 2)) ((= (^ (^ v65 v1) (v v65 v66)) (^ v65 v1))))
(268 (instantiate 7 ((v0 . v65)(v1 . v1)(v2 . (v v65 v66)))) ((= (^ (^ v65 v1) (v v65 v66)) (^ v65 (^ v1 (v v65 v66))))))
(269 (paramod 268 (1 1) 267 (1 1)) ((= (^ v65 (^ v1 (v v65 v66))) (^ v65 v1))))
(270 (instantiate 269 ((v65 . v0)(v66 . v2))) ((= (^ v0 (^ v1 (v v0 v2))) (^ v0 v1))))
(271 (instantiate 59 ((v0 . v65))) ((= (v v65 (v (^ v65 v1) v2)) (v v65 v2))))
(272 (instantiate 26 ((v0 . (v (^ v65 v1) v2))(v1 . v65))) ((= (^ (v (^ v65 v1) v2) (v v65 (v (^ v65 v1) v2))) (v (^ v65 v1) v2))))
(273 (paramod 271 (1 1) 272 (1 1 2)) ((= (^ (v (^ v65 v1) v2) (v v65 v2)) (v (^ v65 v1) v2))))
(274 (instantiate 273 ((v65 . v0))) ((= (^ (v (^ v0 v1) v2) (v v0 v2)) (v (^ v0 v1) v2))))
(275 (instantiate 9 ((v0 . v64))) ((= (v v64 (^ v64 v1)) v64)))
(276 (instantiate 22 ((v0 . v64)(v1 . v65)(v2 . (^ v64 v1))(v3 . v67))) ((= (^ (v v64 (^ v65 (v v64 (^ v64 v1)))) (v v64 (^ (v v64 v65) (v (^ v64 v1) v67)))) (v v64 (^ v65 (v (^ v64 v1) (^ v64 v67)))))))
(277 (paramod 275 (1 1) 276 (1 1 1 2 2)) ((= (^ (v v64 (^ v65 v64)) (v v64 (^ (v v64 v65) (v (^ v64 v1) v67)))) (v v64 (^ v65 (v (^ v64 v1) (^ v64 v67)))))))
(278 (instantiate 50 ((v0 . v64)(v1 . v65))) ((= (v v64 (^ v65 v64)) v64)))
(279 (paramod 278 (1 1) 277 (1 1 1)) ((= (^ v64 (v v64 (^ (v v64 v65) (v (^ v64 v1) v67)))) (v v64 (^ v65 (v (^ v64 v1) (^ v64 v67)))))))
(280 (instantiate 8 ((v0 . v64)(v1 . (^ (v v64 v65) (v (^ v64 v1) v67))))) ((= (^ v64 (v v64 (^ (v v64 v65) (v (^ v64 v1) v67)))) v64)))
(281 (paramod 280 (1 1) 279 (1 1)) ((= v64 (v v64 (^ v65 (v (^ v64 v1) (^ v64 v67)))))))
(282 (flip 281 (1)) ((= (v v64 (^ v65 (v (^ v64 v1) (^ v64 v67)))) v64)))
(283 (instantiate 282 ((v1 . v2)(v64 . v0)(v65 . v1)(v67 . v3))) ((= (v v0 (^ v1 (v (^ v0 v2) (^ v0 v3)))) v0)))
(284 (instantiate 54 ((v0 . v65))) ((= (v (^ v65 v1) v65) v65)))
(285 (instantiate 22 ((v0 . (^ v65 v1))(v1 . v65)(v2 . v66)(v3 . v67))) ((= (^ (v (^ v65 v1) (^ v65 (v (^ v65 v1) v66))) (v (^ v65 v1) (^ (v (^ v65 v1) v65) (v v66 v67)))) (v (^ v65 v1) (^ v65 (v v66 (^ (^ v65 v1) v67)))))))
(286 (paramod 284 (1 1) 285 (1 1 2 2 1)) ((= (^ (v (^ v65 v1) (^ v65 (v (^ v65 v1) v66))) (v (^ v65 v1) (^ v65 (v v66 v67)))) (v (^ v65 v1) (^ v65 (v v66 (^ (^ v65 v1) v67)))))))
(287 (instantiate 7 ((v0 . v65)(v1 . v1)(v2 . v67))) ((= (^ (^ v65 v1) v67) (^ v65 (^ v1 v67)))))
(288 (paramod 287 (1 1) 286 (1 2 2 2 2)) ((= (^ (v (^ v65 v1) (^ v65 (v (^ v65 v1) v66))) (v (^ v65 v1) (^ v65 (v v66 v67)))) (v (^ v65 v1) (^ v65 (v v66 (^ v65 (^ v1 v67))))))))
(289 (instantiate 288 ((v65 . v0)(v66 . v2)(v67 . v3))) ((= (^ (v (^ v0 v1) (^ v0 (v (^ v0 v1) v2))) (v (^ v0 v1) (^ v0 (v v2 v3)))) (v (^ v0 v1) (^ v0 (v v2 (^ v0 (^ v1 v3))))))))
(290 (flip 289 (1)) ((= (v (^ v0 v1) (^ v0 (v v2 (^ v0 (^ v1 v3))))) (^ (v (^ v0 v1) (^ v0 (v (^ v0 v1) v2))) (v (^ v0 v1) (^ v0 (v v2 v3)))))))
(291 (instantiate 99 ((v0 . v64)(v1 . (v v0 v1))(v2 . (^ v0 v2)))) ((= (^ v64 (^ (v v0 v1) (^ v0 v2))) (^ (v v0 v1) (^ v64 (^ v0 v2))))))
(292 (paramod 93 (1 1) 291 (1 1 2)) ((= (^ v64 (^ v0 v2)) (^ (v v0 v1) (^ v64 (^ v0 v2))))))
(293 (flip 292 (1)) ((= (^ (v v0 v1) (^ v64 (^ v0 v2))) (^ v64 (^ v0 v2)))))
(294 (instantiate 293 ((v2 . v3)(v64 . v2))) ((= (^ (v v0 v1) (^ v2 (^ v0 v3))) (^ v2 (^ v0 v3)))))
(295 (instantiate 30 ((v0 . (^ v65 v66)))) ((= (^ (v (^ v65 v66) v1) (^ v65 v66)) (^ v65 v66))))
(296 (instantiate 99 ((v0 . (v (^ v65 v66) v1))(v1 . v65)(v2 . v66))) ((= (^ (v (^ v65 v66) v1) (^ v65 v66)) (^ v65 (^ (v (^ v65 v66) v1) v66)))))
(297 (paramod 295 (1 1) 296 (1 1)) ((= (^ v65 v66) (^ v65 (^ (v (^ v65 v66) v1) v66)))))
(298 (flip 297 (1)) ((= (^ v65 (^ (v (^ v65 v66) v1) v66)) (^ v65 v66))))
(299 (instantiate 298 ((v1 . v2)(v65 . v0)(v66 . v1))) ((= (^ v0 (^ (v (^ v0 v1) v2) v1)) (^ v0 v1))))
(300 (instantiate 294 ((v0 . v0)(v1 . (^ v1 v2))(v2 . (v v2 (^ v0 v1)))(v3 . (v v1 v2)))) ((= (^ (v v0 (^ v1 v2)) (^ (v v2 (^ v0 v1)) (^ v0 (v v1 v2)))) (^ (v v2 (^ v0 v1)) (^ v0 (v v1 v2))))))
(301 (paramod 300 (1 1) 250 (1 1)) ((= (^ (v v2 (^ v0 v1)) (^ v0 (v v1 v2))) (^ v0 (v v1 v2)))))
(302 (instantiate 301 ((v0 . v1)(v1 . v2)(v2 . v0))) ((= (^ (v v0 (^ v1 v2)) (^ v1 (v v2 v0))) (^ v1 (v v2 v0)))))
(303 (instantiate 69 ((v0 . (^ v1 v0))(v1 . v65)(v2 . (^ v0 v1)))) ((= (^ (^ v1 v0) (v v65 (v (^ v0 v1) (^ v1 v0)))) (^ v1 v0))))
(304 (paramod 162 (1 1) 303 (1 1 2 2)) ((= (^ (^ v1 v0) (v v65 (^ v0 v1))) (^ v1 v0))))
(305 (instantiate 7 ((v0 . v1)(v1 . v0)(v2 . (v v65 (^ v0 v1))))) ((= (^ (^ v1 v0) (v v65 (^ v0 v1))) (^ v1 (^ v0 (v v65 (^ v0 v1)))))))
(306 (paramod 305 (1 1) 304 (1 1)) ((= (^ v1 (^ v0 (v v65 (^ v0 v1)))) (^ v1 v0))))
(307 (instantiate 306 ((v0 . v1)(v1 . v0)(v65 . v2))) ((= (^ v0 (^ v1 (v v2 (^ v1 v0)))) (^ v0 v1))))
(308 (instantiate 88 ((v0 . v66))) ((= (v v66 (v (^ v1 v66) v2)) (v v66 v2))))
(309 (instantiate 177 ((v0 . (v (^ v1 v66) v2))(v1 . v65)(v2 . v66))) ((= (^ (v (^ v1 v66) v2) (^ v65 (v v66 (v (^ v1 v66) v2)))) (^ (v (^ v1 v66) v2) v65))))
(310 (paramod 308 (1 1) 309 (1 1 2 2)) ((= (^ (v (^ v1 v66) v2) (^ v65 (v v66 v2))) (^ (v (^ v1 v66) v2) v65))))
(311 (instantiate 310 ((v1 . v0)(v65 . v3)(v66 . v1))) ((= (^ (v (^ v0 v1) v2) (^ v3 (v v1 v2))) (^ (v (^ v0 v1) v2) v3))))
(312 (instantiate 79 ((v0 . v66))) ((= (v v66 (v v1 v66)) (v v66 v1))))
(313 (instantiate 177 ((v0 . (v v1 v66))(v1 . v65)(v2 . v66))) ((= (^ (v v1 v66) (^ v65 (v v66 (v v1 v66)))) (^ (v v1 v66) v65))))
(314 (paramod 312 (1 1) 313 (1 1 2 2)) ((= (^ (v v1 v66) (^ v65 (v v66 v1))) (^ (v v1 v66) v65))))
(315 (instantiate 314 ((v1 . v0)(v65 . v2)(v66 . v1))) ((= (^ (v v0 v1) (^ v2 (v v1 v0))) (^ (v v0 v1) v2))))
(316 (instantiate 46 ((v1 . v66))) ((= (v v66 (v v2 v0)) (v v0 (v v66 v2)))))
(317 (instantiate 177 ((v0 . (v v2 v0))(v1 . v65)(v2 . v66))) ((= (^ (v v2 v0) (^ v65 (v v66 (v v2 v0)))) (^ (v v2 v0) v65))))
(318 (paramod 316 (1 1) 317 (1 1 2 2)) ((= (^ (v v2 v0) (^ v65 (v v0 (v v66 v2)))) (^ (v v2 v0) v65))))
(319 (instantiate 318 ((v0 . v1)(v2 . v0)(v65 . v2)(v66 . v3))) ((= (^ (v v0 v1) (^ v2 (v v1 (v v3 v0)))) (^ (v v0 v1) v2))))
(320 (instantiate 177 ((v0 . v64))) ((= (^ v64 (^ v1 (v v2 v64))) (^ v64 v1))))
(321 (instantiate 83 ((v0 . v64)(v1 . (^ v1 (v v2 v64))))) ((= (v (^ v64 (^ v1 (v v2 v64))) (^ v1 (v v2 v64))) (^ v1 (v v2 v64)))))
(322 (paramod 320 (1 1) 321 (1 1 1)) ((= (v (^ v64 v1) (^ v1 (v v2 v64))) (^ v1 (v v2 v64)))))
(323 (instantiate 322 ((v64 . v0))) ((= (v (^ v0 v1) (^ v1 (v v2 v0))) (^ v1 (v v2 v0)))))
(324 (instantiate 109 ((v0 . (v v1 v0))(v1 . v65)(v2 . (v v0 v1)))) ((= (^ v65 (^ (v v0 v1) (v v1 v0))) (^ (v v1 v0) (^ v65 (v v0 v1))))))
(325 (paramod 185 (1 1) 324 (1 1 2)) ((= (^ v65 (v v0 v1)) (^ (v v1 v0) (^ v65 (v v0 v1))))))
(326 (instantiate 315 ((v0 . v1)(v1 . v0)(v2 . v65))) ((= (^ (v v1 v0) (^ v65 (v v0 v1))) (^ (v v1 v0) v65))))
(327 (paramod 326 (1 1) 325 (1 2)) ((= (^ v65 (v v0 v1)) (^ (v v1 v0) v65))))
(328 (instantiate 327 ((v0 . v1)(v1 . v2)(v65 . v0))) ((= (^ v0 (v v1 v2)) (^ (v v2 v1) v0))))
(329 (flip 328 (1)) ((= (^ (v v2 v1) v0) (^ v0 (v v1 v2)))))
(330 (instantiate 205 ((v0 . v66))) ((= (v v66 (v v1 (^ v2 v66))) (v v66 v1))))
(331 (instantiate 177 ((v0 . (v v1 (^ v2 v66)))(v1 . v65)(v2 . v66))) ((= (^ (v v1 (^ v2 v66)) (^ v65 (v v66 (v v1 (^ v2 v66))))) (^ (v v1 (^ v2 v66)) v65))))
(332 (paramod 330 (1 1) 331 (1 1 2 2)) ((= (^ (v v1 (^ v2 v66)) (^ v65 (v v66 v1))) (^ (v v1 (^ v2 v66)) v65))))
(333 (instantiate 332 ((v1 . v0)(v2 . v1)(v65 . v3)(v66 . v2))) ((= (^ (v v0 (^ v1 v2)) (^ v3 (v v2 v0))) (^ (v v0 (^ v1 v2)) v3))))
(334 (instantiate 333 ((v0 . v0)(v1 . v1)(v2 . v2)(v3 . v1))) ((= (^ (v v0 (^ v1 v2)) (^ v1 (v v2 v0))) (^ (v v0 (^ v1 v2)) v1))))
(335 (paramod 334 (1 1) 302 (1 1)) ((= (^ (v v0 (^ v1 v2)) v1) (^ v1 (v v2 v0)))))
(336 (instantiate 264 ((v0 . (^ (A) (v (B) (^ (C) (D)))))(v1 . (^ (A) (C)))(v2 . (^ (A) (D))))) ((= (v (^ (A) (v (B) (^ (C) (D)))) (v (^ (A) (C)) (^ (A) (D)))) (v (^ (A) (D)) (v (^ (A) (C)) (^ (A) (v (B) (^ (C) (D)))))))))
(337 (paramod 336 (1 1) 21 (1 1 1 2 2 2)) ((not (= (^ (A) (^ (v (B) (C)) (^ (v (B) (D)) (v (^ (A) (D)) (v (^ (A) (C)) (^ (A) (v (B) (^ (C) (D))))))))) (^ (A) (^ (v (B) (C)) (v (B) (D))))))))
(338 (instantiate 270 ((v0 . v64))) ((= (^ v64 (^ v1 (v v64 v2))) (^ v64 v1))))
(339 (instantiate 213 ((v0 . v64)(v1 . (^ v1 (v v64 v2)))(v2 . v66))) ((= (v (^ v64 (^ v1 (v v64 v2))) (v v66 (^ v1 (v v64 v2)))) (v v66 (^ v1 (v v64 v2))))))
(340 (paramod 338 (1 1) 339 (1 1 1)) ((= (v (^ v64 v1) (v v66 (^ v1 (v v64 v2)))) (v v66 (^ v1 (v v64 v2))))))
(341 (instantiate 340 ((v2 . v3)(v64 . v0)(v66 . v2))) ((= (v (^ v0 v1) (v v2 (^ v1 (v v0 v3)))) (v v2 (^ v1 (v v0 v3))))))
(342 (instantiate 209 ((v1 . v66))) ((= (^ (v v0 (v v66 v2)) v66) v66)))
(343 (instantiate 117 ((v0 . v64)(v1 . (v v0 (v v66 v2)))(v2 . v66))) ((= (v (^ v64 (^ (v v0 (v v66 v2)) v66)) (^ v64 (v v0 (v v66 v2)))) (^ v64 (v v0 (v v66 v2))))))
(344 (paramod 342 (1 1) 343 (1 1 1 2)) ((= (v (^ v64 v66) (^ v64 (v v0 (v v66 v2)))) (^ v64 (v v0 (v v66 v2))))))
(345 (instantiate 344 ((v0 . v2)(v2 . v3)(v64 . v0)(v66 . v1))) ((= (v (^ v0 v1) (^ v0 (v v2 (v v1 v3)))) (^ v0 (v v2 (v v1 v3))))))
(346 (instantiate 117 ((v0 . v64)(v1 . (v v0 v1))(v2 . (^ v0 v2)))) ((= (v (^ v64 (^ (v v0 v1) (^ v0 v2))) (^ v64 (v v0 v1))) (^ v64 (v v0 v1)))))
(347 (paramod 93 (1 1) 346 (1 1 1 2)) ((= (v (^ v64 (^ v0 v2)) (^ v64 (v v0 v1))) (^ v64 (v v0 v1)))))
(348 (instantiate 347 ((v0 . v1)(v1 . v3)(v64 . v0))) ((= (v (^ v0 (^ v1 v2)) (^ v0 (v v1 v3))) (^ v0 (v v1 v3)))))
(349 (instantiate 73 ((v1 . v66))) ((= (^ (v v0 v66) v66) v66)))
(350 (instantiate 117 ((v0 . v64)(v1 . (v v0 v66))(v2 . v66))) ((= (v (^ v64 (^ (v v0 v66) v66)) (^ v64 (v v0 v66))) (^ v64 (v v0 v66)))))
(351 (paramod 349 (1 1) 350 (1 1 1 2)) ((= (v (^ v64 v66) (^ v64 (v v0 v66))) (^ v64 (v v0 v66)))))
(352 (instantiate 351 ((v0 . v2)(v64 . v0)(v66 . v1))) ((= (v (^ v0 v1) (^ v0 (v v2 v1))) (^ v0 (v v2 v1)))))
(353 (instantiate 117 ((v0 . v66)(v1 . v64))) ((= (v (^ v66 (^ v64 v2)) (^ v66 v64)) (^ v66 v64))))
(354 (instantiate 134 ((v0 . v64)(v1 . (^ v66 (^ v64 v2)))(v2 . v66)(v3 . v67))) ((= (v (^ v64 (v (^ v66 (^ v64 v2)) (^ v66 v64))) (^ v64 (v (^ v64 (^ v66 (^ v64 v2))) (^ v66 v67)))) (^ v64 (v (^ v66 (^ v64 v2)) (^ v66 (v v64 v67)))))))
(355 (paramod 353 (1 1) 354 (1 1 1 2)) ((= (v (^ v64 (^ v66 v64)) (^ v64 (v (^ v64 (^ v66 (^ v64 v2))) (^ v66 v67)))) (^ v64 (v (^ v66 (^ v64 v2)) (^ v66 (v v64 v67)))))))
(356 (instantiate 65 ((v0 . v64)(v1 . v66))) ((= (^ v64 (^ v66 v64)) (^ v64 v66))))
(357 (paramod 356 (1 1) 355 (1 1 1)) ((= (v (^ v64 v66) (^ v64 (v (^ v64 (^ v66 (^ v64 v2))) (^ v66 v67)))) (^ v64 (v (^ v66 (^ v64 v2)) (^ v66 (v v64 v67)))))))
(358 (instantiate 171 ((v0 . v64)(v1 . v66)(v2 . v2))) ((= (^ v64 (^ v66 (^ v64 v2))) (^ v64 (^ v66 v2)))))
(359 (paramod 358 (1 1) 357 (1 1 2 2 1)) ((= (v (^ v64 v66) (^ v64 (v (^ v64 (^ v66 v2)) (^ v66 v67)))) (^ v64 (v (^ v66 (^ v64 v2)) (^ v66 (v v64 v67)))))))
(360 (instantiate 348 ((v0 . v66)(v1 . v64)(v2 . v2)(v3 . v67))) ((= (v (^ v66 (^ v64 v2)) (^ v66 (v v64 v67))) (^ v66 (v v64 v67)))))
(361 (paramod 360 (1 1) 359 (1 2 2)) ((= (v (^ v64 v66) (^ v64 (v (^ v64 (^ v66 v2)) (^ v66 v67)))) (^ v64 (^ v66 (v v64 v67))))))
(362 (instantiate 270 ((v0 . v64)(v1 . v66)(v2 . v67))) ((= (^ v64 (^ v66 (v v64 v67))) (^ v64 v66))))
(363 (paramod 362 (1 1) 361 (1 2)) ((= (v (^ v64 v66) (^ v64 (v (^ v64 (^ v66 v2)) (^ v66 v67)))) (^ v64 v66))))
(364 (instantiate 363 ((v64 . v0)(v66 . v1)(v67 . v3))) ((= (v (^ v0 v1) (^ v0 (v (^ v0 (^ v1 v2)) (^ v1 v3)))) (^ v0 v1))))
(365 (instantiate 79 ((v0 . (^ v64 v67))(v1 . v66))) ((= (v (^ v64 v67) (v v66 (^ v64 v67))) (v (^ v64 v67) v66))))
(366 (instantiate 140 ((v0 . v64)(v1 . (^ v64 v67))(v2 . v66)(v3 . v67)(v4 . v68))) ((= (v (^ v64 (v (^ v64 v67) (v v66 (^ v64 v67)))) (^ v64 (v (^ v64 (v (^ v64 v67) v66)) (^ v67 v68)))) (^ v64 (v (^ v64 v67) (v v66 (^ v67 (v v64 v68))))))))
(367 (paramod 365 (1 1) 366 (1 1 1 2)) ((= (v (^ v64 (v (^ v64 v67) v66)) (^ v64 (v (^ v64 (v (^ v64 v67) v66)) (^ v67 v68)))) (^ v64 (v (^ v64 v67) (v v66 (^ v67 (v v64 v68))))))))
(368 (instantiate 341 ((v0 . v64)(v1 . v67)(v2 . v66)(v3 . v68))) ((= (v (^ v64 v67) (v v66 (^ v67 (v v64 v68)))) (v v66 (^ v67 (v v64 v68))))))
(369 (paramod 368 (1 1) 367 (1 2 2)) ((= (v (^ v64 (v (^ v64 v67) v66)) (^ v64 (v (^ v64 (v (^ v64 v67) v66)) (^ v67 v68)))) (^ v64 (v v66 (^ v67 (v v64 v68)))))))
(370 (instantiate 369 ((v64 . v0)(v66 . v2)(v67 . v1)(v68 . v3))) ((= (v (^ v0 (v (^ v0 v1) v2)) (^ v0 (v (^ v0 (v (^ v0 v1) v2)) (^ v1 v3)))) (^ v0 (v v2 (^ v1 (v v0 v3)))))))
(371 (instantiate 73 ((v1 . (^ v64 v66)))) ((= (^ (v v0 (^ v64 v66)) (^ v64 v66)) (^ v64 v66))))
(372 (instantiate 245 ((v0 . v64)(v1 . (v v0 (^ v64 v66)))(v2 . v66))) ((= (v (^ v64 (v v0 (^ v64 v66))) (^ (v v0 (^ v64 v66)) (^ v64 v66))) (^ (v v0 (^ v64 v66)) v64))))
(373 (paramod 371 (1 1) 372 (1 1 2)) ((= (v (^ v64 (v v0 (^ v64 v66))) (^ v64 v66)) (^ (v v0 (^ v64 v66)) v64))))
(374 (instantiate 373 ((v0 . v1)(v64 . v0)(v66 . v2))) ((= (v (^ v0 (v v1 (^ v0 v2))) (^ v0 v2)) (^ (v v1 (^ v0 v2)) v0))))
(375 (instantiate 144 ((v0 . v66))) ((= (v (^ v66 (v v1 (^ v66 v2))) (^ v66 (v (^ v1 v66) (^ v2 v3)))) (^ v66 (v v1 (^ v2 (v v66 v3)))))))
(376 (instantiate 205 ((v0 . (v (^ v1 v66) (^ v2 v3)))(v1 . (^ v66 (v v1 (^ v66 v2))))(v2 . v66))) ((= (v (v (^ v1 v66) (^ v2 v3)) (v (^ v66 (v v1 (^ v66 v2))) (^ v66 (v (^ v1 v66) (^ v2 v3))))) (v (v (^ v1 v66) (^ v2 v3)) (^ v66 (v v1 (^ v66 v2)))))))
(377 (paramod 375 (1 1) 376 (1 1 2)) ((= (v (v (^ v1 v66) (^ v2 v3)) (^ v66 (v v1 (^ v2 (v v66 v3))))) (v (v (^ v1 v66) (^ v2 v3)) (^ v66 (v v1 (^ v66 v2)))))))
(378 (instantiate 6 ((v0 . (^ v1 v66))(v1 . (^ v2 v3))(v2 . (^ v66 (v v1 (^ v2 (v v66 v3))))))) ((= (v (v (^ v1 v66) (^ v2 v3)) (^ v66 (v v1 (^ v2 (v v66 v3))))) (v (^ v1 v66) (v (^ v2 v3) (^ v66 (v v1 (^ v2 (v v66 v3)))))))))
(379 (paramod 378 (1 1) 377 (1 1)) ((= (v (^ v1 v66) (v (^ v2 v3) (^ v66 (v v1 (^ v2 (v v66 v3)))))) (v (v (^ v1 v66) (^ v2 v3)) (^ v66 (v v1 (^ v66 v2)))))))
(380 (instantiate 341 ((v0 . v1)(v1 . v66)(v2 . (^ v2 v3))(v3 . (^ v2 (v v66 v3))))) ((= (v (^ v1 v66) (v (^ v2 v3) (^ v66 (v v1 (^ v2 (v v66 v3)))))) (v (^ v2 v3) (^ v66 (v v1 (^ v2 (v v66 v3))))))))
(381 (paramod 380 (1 1) 379 (1 1)) ((= (v (^ v2 v3) (^ v66 (v v1 (^ v2 (v v66 v3))))) (v (v (^ v1 v66) (^ v2 v3)) (^ v66 (v v1 (^ v66 v2)))))))
(382 (instantiate 6 ((v0 . (^ v1 v66))(v1 . (^ v2 v3))(v2 . (^ v66 (v v1 (^ v66 v2)))))) ((= (v (v (^ v1 v66) (^ v2 v3)) (^ v66 (v v1 (^ v66 v2)))) (v (^ v1 v66) (v (^ v2 v3) (^ v66 (v v1 (^ v66 v2))))))))
(383 (paramod 382 (1 1) 381 (1 2)) ((= (v (^ v2 v3) (^ v66 (v v1 (^ v2 (v v66 v3))))) (v (^ v1 v66) (v (^ v2 v3) (^ v66 (v v1 (^ v66 v2))))))))
(384 (instantiate 341 ((v0 . v1)(v1 . v66)(v2 . (^ v2 v3))(v3 . (^ v66 v2)))) ((= (v (^ v1 v66) (v (^ v2 v3) (^ v66 (v v1 (^ v66 v2))))) (v (^ v2 v3) (^ v66 (v v1 (^ v66 v2)))))))
(385 (paramod 384 (1 1) 383 (1 2)) ((= (v (^ v2 v3) (^ v66 (v v1 (^ v2 (v v66 v3))))) (v (^ v2 v3) (^ v66 (v v1 (^ v66 v2)))))))
(386 (instantiate 385 ((v1 . v3)(v2 . v0)(v3 . v1)(v66 . v2))) ((= (v (^ v0 v1) (^ v2 (v v3 (^ v0 (v v2 v1))))) (v (^ v0 v1) (^ v2 (v v3 (^ v2 v0)))))))
(387 (flip 386 (1)) ((= (v (^ v0 v1) (^ v2 (v v3 (^ v2 v0)))) (v (^ v0 v1) (^ v2 (v v3 (^ v0 (v v2 v1))))))))
(388 (instantiate 148 ((v0 . v65)(v1 . v64)(v2 . (^ v65 v64)))) ((= (v (^ v65 (v v64 (^ v65 (v (^ v65 v64) v3)))) (^ v65 (v (^ v65 v64) v3))) (^ v65 (v v64 (^ (v (^ v65 v64) v3) (v v65 v3)))))))
(389 (instantiate 260 ((v0 . v64)(v1 . v65)(v2 . (^ v65 (v (^ v65 v64) v3))))) ((= (v v64 (v (^ v65 (v v64 (^ v65 (v (^ v65 v64) v3)))) (^ v65 (v (^ v65 v64) v3)))) (v v64 (^ v65 (v (^ v65 v64) v3))))))
(390 (paramod 388 (1 1) 389 (1 1 2)) ((= (v v64 (^ v65 (v v64 (^ (v (^ v65 v64) v3) (v v65 v3))))) (v v64 (^ v65 (v (^ v65 v64) v3))))))
(391 (instantiate 274 ((v0 . v65)(v1 . v64)(v2 . v3))) ((= (^ (v (^ v65 v64) v3) (v v65 v3)) (v (^ v65 v64) v3))))
(392 (paramod 391 (1 1) 390 (1 1 2 2 2)) ((= (v v64 (^ v65 (v v64 (v (^ v65 v64) v3)))) (v v64 (^ v65 (v (^ v65 v64) v3))))))
(393 (instantiate 88 ((v0 . v64)(v1 . v65)(v2 . v3))) ((= (v v64 (v (^ v65 v64) v3)) (v v64 v3))))
(394 (paramod 393 (1 1) 392 (1 1 2 2)) ((= (v v64 (^ v65 (v v64 v3))) (v v64 (^ v65 (v (^ v65 v64) v3))))))
(395 (flip 394 (1)) ((= (v v64 (^ v65 (v (^ v65 v64) v3))) (v v64 (^ v65 (v v64 v3))))))
(396 (instantiate 395 ((v3 . v2)(v64 . v0)(v65 . v1))) ((= (v v0 (^ v1 (v (^ v1 v0) v2))) (v v0 (^ v1 (v v0 v2))))))
(397 (instantiate 283 ((v0 . v65))) ((= (v v65 (^ v1 (v (^ v65 v2) (^ v65 v3)))) v65)))
(398 (instantiate 26 ((v0 . (^ v1 (v (^ v65 v2) (^ v65 v3))))(v1 . v65))) ((= (^ (^ v1 (v (^ v65 v2) (^ v65 v3))) (v v65 (^ v1 (v (^ v65 v2) (^ v65 v3))))) (^ v1 (v (^ v65 v2) (^ v65 v3))))))
(399 (paramod 397 (1 1) 398 (1 1 2)) ((= (^ (^ v1 (v (^ v65 v2) (^ v65 v3))) v65) (^ v1 (v (^ v65 v2) (^ v65 v3))))))
(400 (instantiate 7 ((v0 . v1)(v1 . (v (^ v65 v2) (^ v65 v3)))(v2 . v65))) ((= (^ (^ v1 (v (^ v65 v2) (^ v65 v3))) v65) (^ v1 (^ (v (^ v65 v2) (^ v65 v3)) v65)))))
(401 (paramod 400 (1 1) 399 (1 1)) ((= (^ v1 (^ (v (^ v65 v2) (^ v65 v3)) v65)) (^ v1 (v (^ v65 v2) (^ v65 v3))))))
(402 (instantiate 401 ((v1 . v0)(v65 . v1))) ((= (^ v0 (^ (v (^ v1 v2) (^ v1 v3)) v1)) (^ v0 (v (^ v1 v2) (^ v1 v3))))))
(403 (instantiate 283 ((v0 . v64))) ((= (v v64 (^ v1 (v (^ v64 v2) (^ v64 v3)))) v64)))
(404 (instantiate 73 ((v0 . v64)(v1 . (^ v1 (v (^ v64 v2) (^ v64 v3)))))) ((= (^ (v v64 (^ v1 (v (^ v64 v2) (^ v64 v3)))) (^ v1 (v (^ v64 v2) (^ v64 v3)))) (^ v1 (v (^ v64 v2) (^ v64 v3))))))
(405 (paramod 403 (1 1) 404 (1 1 1)) ((= (^ v64 (^ v1 (v (^ v64 v2) (^ v64 v3)))) (^ v1 (v (^ v64 v2) (^ v64 v3))))))
(406 (instantiate 405 ((v64 . v0))) ((= (^ v0 (^ v1 (v (^ v0 v2) (^ v0 v3)))) (^ v1 (v (^ v0 v2) (^ v0 v3))))))
(407 (instantiate 130 ((v0 . v64)(v1 . v65))) ((= (v (^ v64 v65) (v v65 v2)) (v v65 v2))))
(408 (instantiate 154 ((v0 . v64)(v1 . v65)(v2 . (v v65 v2)))) ((= (v (^ v64 (v v65 (^ v64 (v v65 v2)))) (^ v64 (v (^ v64 v65) (v v65 v2)))) (^ v64 (v v65 (v v65 v2))))))
(409 (paramod 407 (1 1) 408 (1 1 2 2)) ((= (v (^ v64 (v v65 (^ v64 (v v65 v2)))) (^ v64 (v v65 v2))) (^ v64 (v v65 (v v65 v2))))))
(410 (instantiate 374 ((v0 . v64)(v1 . v65)(v2 . (v v65 v2)))) ((= (v (^ v64 (v v65 (^ v64 (v v65 v2)))) (^ v64 (v v65 v2))) (^ (v v65 (^ v64 (v v65 v2))) v64))))
(411 (paramod 410 (1 1) 409 (1 1)) ((= (^ (v v65 (^ v64 (v v65 v2))) v64) (^ v64 (v v65 (v v65 v2))))))
(412 (instantiate 41 ((v0 . v65)(v1 . v2))) ((= (v v65 (v v65 v2)) (v v65 v2))))
(413 (paramod 412 (1 1) 411 (1 2 2)) ((= (^ (v v65 (^ v64 (v v65 v2))) v64) (^ v64 (v v65 v2)))))
(414 (instantiate 413 ((v64 . v1)(v65 . v0))) ((= (^ (v v0 (^ v1 (v v0 v2))) v1) (^ v1 (v v0 v2)))))
(415 (instantiate 154 ((v0 . v64))) ((= (v (^ v64 (v v1 (^ v64 v2))) (^ v64 (v (^ v64 v1) v2))) (^ v64 (v v1 v2)))))
(416 (instantiate 154 ((v0 . v64)(v1 . (v v1 (^ v64 v2)))(v2 . (^ v64 (v (^ v64 v1) v2))))) ((= (v (^ v64 (v (v v1 (^ v64 v2)) (^ v64 (^ v64 (v (^ v64 v1) v2))))) (^ v64 (v (^ v64 (v v1 (^ v64 v2))) (^ v64 (v (^ v64 v1) v2))))) (^ v64 (v (v v1 (^ v64 v2)) (^ v64 (v (^ v64 v1) v2)))))))
(417 (paramod 415 (1 1) 416 (1 1 2 2)) ((= (v (^ v64 (v (v v1 (^ v64 v2)) (^ v64 (^ v64 (v (^ v64 v1) v2))))) (^ v64 (^ v64 (v v1 v2)))) (^ v64 (v (v v1 (^ v64 v2)) (^ v64 (v (^ v64 v1) v2)))))))
(418 (instantiate 104 ((v0 . v64)(v1 . (v (^ v64 v1) v2)))) ((= (^ v64 (^ v64 (v (^ v64 v1) v2))) (^ v64 (v (^ v64 v1) v2)))))
(419 (paramod 418 (1 1) 417 (1 1 1 2 2)) ((= (v (^ v64 (v (v v1 (^ v64 v2)) (^ v64 (v (^ v64 v1) v2)))) (^ v64 (^ v64 (v v1 v2)))) (^ v64 (v (v v1 (^ v64 v2)) (^ v64 (v (^ v64 v1) v2)))))))
(420 (instantiate 6 ((v0 . v1)(v1 . (^ v64 v2))(v2 . (^ v64 (v (^ v64 v1) v2))))) ((= (v (v v1 (^ v64 v2)) (^ v64 (v (^ v64 v1) v2))) (v v1 (v (^ v64 v2) (^ v64 (v (^ v64 v1) v2)))))))
(421 (paramod 420 (1 1) 419 (1 1 1 2)) ((= (v (^ v64 (v v1 (v (^ v64 v2) (^ v64 (v (^ v64 v1) v2))))) (^ v64 (^ v64 (v v1 v2)))) (^ v64 (v (v v1 (^ v64 v2)) (^ v64 (v (^ v64 v1) v2)))))))
(422 (instantiate 352 ((v0 . v64)(v1 . v2)(v2 . (^ v64 v1)))) ((= (v (^ v64 v2) (^ v64 (v (^ v64 v1) v2))) (^ v64 (v (^ v64 v1) v2)))))
(423 (paramod 422 (1 1) 421 (1 1 1 2 2)) ((= (v (^ v64 (v v1 (^ v64 (v (^ v64 v1) v2)))) (^ v64 (^ v64 (v v1 v2)))) (^ v64 (v (v v1 (^ v64 v2)) (^ v64 (v (^ v64 v1) v2)))))))
(424 (instantiate 396 ((v0 . v1)(v1 . v64)(v2 . v2))) ((= (v v1 (^ v64 (v (^ v64 v1) v2))) (v v1 (^ v64 (v v1 v2))))))
(425 (paramod 424 (1 1) 423 (1 1 1 2)) ((= (v (^ v64 (v v1 (^ v64 (v v1 v2)))) (^ v64 (^ v64 (v v1 v2)))) (^ v64 (v (v v1 (^ v64 v2)) (^ v64 (v (^ v64 v1) v2)))))))
(426 (instantiate 104 ((v0 . v64)(v1 . (v v1 v2)))) ((= (^ v64 (^ v64 (v v1 v2))) (^ v64 (v v1 v2)))))
(427 (paramod 426 (1 1) 425 (1 1 2)) ((= (v (^ v64 (v v1 (^ v64 (v v1 v2)))) (^ v64 (v v1 v2))) (^ v64 (v (v v1 (^ v64 v2)) (^ v64 (v (^ v64 v1) v2)))))))
(428 (instantiate 374 ((v0 . v64)(v1 . v1)(v2 . (v v1 v2)))) ((= (v (^ v64 (v v1 (^ v64 (v v1 v2)))) (^ v64 (v v1 v2))) (^ (v v1 (^ v64 (v v1 v2))) v64))))
(429 (paramod 428 (1 1) 427 (1 1)) ((= (^ (v v1 (^ v64 (v v1 v2))) v64) (^ v64 (v (v v1 (^ v64 v2)) (^ v64 (v (^ v64 v1) v2)))))))
(430 (instantiate 414 ((v0 . v1)(v1 . v64)(v2 . v2))) ((= (^ (v v1 (^ v64 (v v1 v2))) v64) (^ v64 (v v1 v2)))))
(431 (paramod 430 (1 1) 429 (1 1)) ((= (^ v64 (v v1 v2)) (^ v64 (v (v v1 (^ v64 v2)) (^ v64 (v (^ v64 v1) v2)))))))
(432 (instantiate 6 ((v0 . v1)(v1 . (^ v64 v2))(v2 . (^ v64 (v (^ v64 v1) v2))))) ((= (v (v v1 (^ v64 v2)) (^ v64 (v (^ v64 v1) v2))) (v v1 (v (^ v64 v2) (^ v64 (v (^ v64 v1) v2)))))))
(433 (paramod 432 (1 1) 431 (1 2 2)) ((= (^ v64 (v v1 v2)) (^ v64 (v v1 (v (^ v64 v2) (^ v64 (v (^ v64 v1) v2))))))))
(434 (instantiate 352 ((v0 . v64)(v1 . v2)(v2 . (^ v64 v1)))) ((= (v (^ v64 v2) (^ v64 (v (^ v64 v1) v2))) (^ v64 (v (^ v64 v1) v2)))))
(435 (paramod 434 (1 1) 433 (1 2 2 2)) ((= (^ v64 (v v1 v2)) (^ v64 (v v1 (^ v64 (v (^ v64 v1) v2)))))))
(436 (instantiate 396 ((v0 . v1)(v1 . v64)(v2 . v2))) ((= (v v1 (^ v64 (v (^ v64 v1) v2))) (v v1 (^ v64 (v v1 v2))))))
(437 (paramod 436 (1 1) 435 (1 2 2)) ((= (^ v64 (v v1 v2)) (^ v64 (v v1 (^ v64 (v v1 v2)))))))
(438 (flip 437 (1)) ((= (^ v64 (v v1 (^ v64 (v v1 v2)))) (^ v64 (v v1 v2)))))
(439 (instantiate 438 ((v64 . v0))) ((= (^ v0 (v v1 (^ v0 (v v1 v2)))) (^ v0 (v v1 v2)))))
(440 (instantiate 154 ((v0 . v66))) ((= (v (^ v66 (v v1 (^ v66 v2))) (^ v66 (v (^ v66 v1) v2))) (^ v66 (v v1 v2)))))
(441 (instantiate 134 ((v0 . (v (^ v66 v1) v2))(v1 . (^ v66 (v v1 (^ v66 v2))))(v2 . v66)(v3 . v67))) ((= (v (^ (v (^ v66 v1) v2) (v (^ v66 (v v1 (^ v66 v2))) (^ v66 (v (^ v66 v1) v2)))) (^ (v (^ v66 v1) v2) (v (^ (v (^ v66 v1) v2) (^ v66 (v v1 (^ v66 v2)))) (^ v66 v67)))) (^ (v (^ v66 v1) v2) (v (^ v66 (v v1 (^ v66 v2))) (^ v66 (v (v (^ v66 v1) v2) v67)))))))
(442 (paramod 440 (1 1) 441 (1 1 1 2)) ((= (v (^ (v (^ v66 v1) v2) (^ v66 (v v1 v2))) (^ (v (^ v66 v1) v2) (v (^ (v (^ v66 v1) v2) (^ v66 (v v1 (^ v66 v2)))) (^ v66 v67)))) (^ (v (^ v66 v1) v2) (v (^ v66 (v v1 (^ v66 v2))) (^ v66 (v (v (^ v66 v1) v2) v67)))))))
(443 (instantiate 311 ((v0 . v66)(v1 . v1)(v2 . v2)(v3 . v66))) ((= (^ (v (^ v66 v1) v2) (^ v66 (v v1 v2))) (^ (v (^ v66 v1) v2) v66))))
(444 (paramod 443 (1 1) 442 (1 1 1)) ((= (v (^ (v (^ v66 v1) v2) v66) (^ (v (^ v66 v1) v2) (v (^ (v (^ v66 v1) v2) (^ v66 (v v1 (^ v66 v2)))) (^ v66 v67)))) (^ (v (^ v66 v1) v2) (v (^ v66 (v v1 (^ v66 v2))) (^ v66 (v (v (^ v66 v1) v2) v67)))))))
(445 (instantiate 364 ((v0 . (v (^ v66 v1) v2))(v1 . v66)(v2 . (v v1 (^ v66 v2)))(v3 . v67))) ((= (v (^ (v (^ v66 v1) v2) v66) (^ (v (^ v66 v1) v2) (v (^ (v (^ v66 v1) v2) (^ v66 (v v1 (^ v66 v2)))) (^ v66 v67)))) (^ (v (^ v66 v1) v2) v66))))
(446 (paramod 445 (1 1) 444 (1 1)) ((= (^ (v (^ v66 v1) v2) v66) (^ (v (^ v66 v1) v2) (v (^ v66 (v v1 (^ v66 v2))) (^ v66 (v (v (^ v66 v1) v2) v67)))))))
(447 (instantiate 6 ((v0 . (^ v66 v1))(v1 . v2)(v2 . v67))) ((= (v (v (^ v66 v1) v2) v67) (v (^ v66 v1) (v v2 v67)))))
(448 (paramod 447 (1 1) 446 (1 2 2 2 2)) ((= (^ (v (^ v66 v1) v2) v66) (^ (v (^ v66 v1) v2) (v (^ v66 (v v1 (^ v66 v2))) (^ v66 (v (^ v66 v1) (v v2 v67))))))))
(449 (flip 448 (1)) ((= (^ (v (^ v66 v1) v2) (v (^ v66 (v v1 (^ v66 v2))) (^ v66 (v (^ v66 v1) (v v2 v67))))) (^ (v (^ v66 v1) v2) v66))))
(450 (instantiate 449 ((v66 . v0)(v67 . v3))) ((= (^ (v (^ v0 v1) v2) (v (^ v0 (v v1 (^ v0 v2))) (^ v0 (v (^ v0 v1) (v v2 v3))))) (^ (v (^ v0 v1) v2) v0))))
(451 (instantiate 299 ((v0 . v64)(v1 . v66))) ((= (^ v64 (^ (v (^ v64 v66) v2) v66)) (^ v64 v66))))
(452 (instantiate 117 ((v0 . v64)(v1 . (v (^ v64 v66) v2))(v2 . v66))) ((= (v (^ v64 (^ (v (^ v64 v66) v2) v66)) (^ v64 (v (^ v64 v66) v2))) (^ v64 (v (^ v64 v66) v2)))))
(453 (paramod 451 (1 1) 452 (1 1 1)) ((= (v (^ v64 v66) (^ v64 (v (^ v64 v66) v2))) (^ v64 (v (^ v64 v66) v2)))))
(454 (instantiate 453 ((v64 . v0)(v66 . v1))) ((= (v (^ v0 v1) (^ v0 (v (^ v0 v1) v2))) (^ v0 (v (^ v0 v1) v2)))))
(455 (instantiate 454 ((v0 . v0)(v1 . (v (^ v0 v1) v2))(v2 . (^ v1 v3)))) ((= (v (^ v0 (v (^ v0 v1) v2)) (^ v0 (v (^ v0 (v (^ v0 v1) v2)) (^ v1 v3)))) (^ v0 (v (^ v0 (v (^ v0 v1) v2)) (^ v1 v3))))))
(456 (paramod 455 (1 1) 370 (1 1)) ((= (^ v0 (v (^ v0 (v (^ v0 v1) v2)) (^ v1 v3))) (^ v0 (v v2 (^ v1 (v v0 v3)))))))
(457 (paramod 454 (1 1) 290 (1 2 1)) ((= (v (^ v0 v1) (^ v0 (v v2 (^ v0 (^ v1 v3))))) (^ (^ v0 (v (^ v0 v1) v2)) (v (^ v0 v1) (^ v0 (v v2 v3)))))))
(458 (instantiate 7 ((v0 . v0)(v1 . (v (^ v0 v1) v2))(v2 . (v (^ v0 v1) (^ v0 (v v2 v3)))))) ((= (^ (^ v0 (v (^ v0 v1) v2)) (v (^ v0 v1) (^ v0 (v v2 v3)))) (^ v0 (^ (v (^ v0 v1) v2) (v (^ v0 v1) (^ v0 (v v2 v3))))))))
(459 (paramod 458 (1 1) 457 (1 2)) ((= (v (^ v0 v1) (^ v0 (v v2 (^ v0 (^ v1 v3))))) (^ v0 (^ (v (^ v0 v1) v2) (v (^ v0 v1) (^ v0 (v v2 v3))))))))
(460 (instantiate 406 ((v0 . v0)(v1 . (v (^ v0 v1) v2))(v2 . v1)(v3 . (v v2 v3)))) ((= (^ v0 (^ (v (^ v0 v1) v2) (v (^ v0 v1) (^ v0 (v v2 v3))))) (^ (v (^ v0 v1) v2) (v (^ v0 v1) (^ v0 (v v2 v3)))))))
(461 (paramod 460 (1 1) 459 (1 2)) ((= (v (^ v0 v1) (^ v0 (v v2 (^ v0 (^ v1 v3))))) (^ (v (^ v0 v1) v2) (v (^ v0 v1) (^ v0 (v v2 v3)))))))
(462 (instantiate 307 ((v0 . v64))) ((= (^ v64 (^ v1 (v v2 (^ v1 v64)))) (^ v64 v1))))
(463 (instantiate 83 ((v0 . v64)(v1 . (^ v1 (v v2 (^ v1 v64)))))) ((= (v (^ v64 (^ v1 (v v2 (^ v1 v64)))) (^ v1 (v v2 (^ v1 v64)))) (^ v1 (v v2 (^ v1 v64))))))
(464 (paramod 462 (1 1) 463 (1 1 1)) ((= (v (^ v64 v1) (^ v1 (v v2 (^ v1 v64)))) (^ v1 (v v2 (^ v1 v64))))))
(465 (instantiate 464 ((v64 . v0))) ((= (v (^ v0 v1) (^ v1 (v v2 (^ v1 v0)))) (^ v1 (v v2 (^ v1 v0))))))
(466 (instantiate 4 ((v0 . v64)(v1 . (^ v65 v66)))) ((= (v v64 (^ v65 v66)) (v (^ v65 v66) v64))))
(467 (instantiate 335 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (^ (v v64 (^ v65 v66)) v65) (^ v65 (v v66 v64)))))
(468 (paramod 466 (1 1) 467 (1 1 1)) ((= (^ (v (^ v65 v66) v64) v65) (^ v65 (v v66 v64)))))
(469 (instantiate 468 ((v64 . v2)(v65 . v0)(v66 . v1))) ((= (^ (v (^ v0 v1) v2) v0) (^ v0 (v v1 v2)))))
(470 (instantiate 329 ((v0 . v65)(v1 . (^ v65 v66))(v2 . v64))) ((= (^ (v v64 (^ v65 v66)) v65) (^ v65 (v (^ v65 v66) v64)))))
(471 (instantiate 335 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (^ (v v64 (^ v65 v66)) v65) (^ v65 (v v66 v64)))))
(472 (paramod 470 (1 1) 471 (1 1)) ((= (^ v65 (v (^ v65 v66) v64)) (^ v65 (v v66 v64)))))
(473 (instantiate 472 ((v64 . v2)(v65 . v0)(v66 . v1))) ((= (^ v0 (v (^ v0 v1) v2)) (^ v0 (v v1 v2)))))
(474 (instantiate 469 ((v0 . v1)(v1 . v2)(v2 . (^ v1 v3)))) ((= (^ (v (^ v1 v2) (^ v1 v3)) v1) (^ v1 (v v2 (^ v1 v3))))))
(475 (paramod 474 (1 1) 402 (1 1 2)) ((= (^ v0 (^ v1 (v v2 (^ v1 v3)))) (^ v0 (v (^ v1 v2) (^ v1 v3))))))
(476 (flip 475 (1)) ((= (^ v0 (v (^ v1 v2) (^ v1 v3))) (^ v0 (^ v1 (v v2 (^ v1 v3)))))))
(477 (paramod 473 (1 1) 456 (1 1 2 1)) ((= (^ v0 (v (^ v0 (v v1 v2)) (^ v1 v3))) (^ v0 (v v2 (^ v1 (v v0 v3)))))))
(478 (instantiate 473 ((v0 . v0)(v1 . (v v1 v2))(v2 . (^ v1 v3)))) ((= (^ v0 (v (^ v0 (v v1 v2)) (^ v1 v3))) (^ v0 (v (v v1 v2) (^ v1 v3))))))
(479 (paramod 478 (1 1) 477 (1 1)) ((= (^ v0 (v (v v1 v2) (^ v1 v3))) (^ v0 (v v2 (^ v1 (v v0 v3)))))))
(480 (instantiate 6 ((v0 . v1)(v1 . v2)(v2 . (^ v1 v3)))) ((= (v (v v1 v2) (^ v1 v3)) (v v1 (v v2 (^ v1 v3))))))
(481 (paramod 480 (1 1) 479 (1 1 2)) ((= (^ v0 (v v1 (v v2 (^ v1 v3)))) (^ v0 (v v2 (^ v1 (v v0 v3)))))))
(482 (instantiate 255 ((v0 . v1)(v1 . v2)(v2 . v3))) ((= (v v1 (v v2 (^ v1 v3))) (v v2 v1))))
(483 (paramod 482 (1 1) 481 (1 1 2)) ((= (^ v0 (v v2 v1)) (^ v0 (v v2 (^ v1 (v v0 v3)))))))
(484 (flip 483 (1)) ((= (^ v0 (v v2 (^ v1 (v v0 v3)))) (^ v0 (v v2 v1)))))
(485 (instantiate 484 ((v1 . v2)(v2 . v1))) ((= (^ v0 (v v1 (^ v2 (v v0 v3)))) (^ v0 (v v1 v2)))))
(486 (instantiate 473 ((v0 . v0)(v1 . v1)(v2 . (v v2 v3)))) ((= (^ v0 (v (^ v0 v1) (v v2 v3))) (^ v0 (v v1 (v v2 v3))))))
(487 (paramod 486 (1 1) 450 (1 1 2 2)) ((= (^ (v (^ v0 v1) v2) (v (^ v0 (v v1 (^ v0 v2))) (^ v0 (v v1 (v v2 v3))))) (^ (v (^ v0 v1) v2) v0))))
(488 (instantiate 476 ((v0 . (v (^ v0 v1) v2))(v1 . v0)(v2 . (v v1 (^ v0 v2)))(v3 . (v v1 (v v2 v3))))) ((= (^ (v (^ v0 v1) v2) (v (^ v0 (v v1 (^ v0 v2))) (^ v0 (v v1 (v v2 v3))))) (^ (v (^ v0 v1) v2) (^ v0 (v (v v1 (^ v0 v2)) (^ v0 (v v1 (v v2 v3)))))))))
(489 (paramod 488 (1 1) 487 (1 1)) ((= (^ (v (^ v0 v1) v2) (^ v0 (v (v v1 (^ v0 v2)) (^ v0 (v v1 (v v2 v3)))))) (^ (v (^ v0 v1) v2) v0))))
(490 (instantiate 6 ((v0 . v1)(v1 . (^ v0 v2))(v2 . (^ v0 (v v1 (v v2 v3)))))) ((= (v (v v1 (^ v0 v2)) (^ v0 (v v1 (v v2 v3)))) (v v1 (v (^ v0 v2) (^ v0 (v v1 (v v2 v3))))))))
(491 (paramod 490 (1 1) 489 (1 1 2 2)) ((= (^ (v (^ v0 v1) v2) (^ v0 (v v1 (v (^ v0 v2) (^ v0 (v v1 (v v2 v3))))))) (^ (v (^ v0 v1) v2) v0))))
(492 (instantiate 345 ((v0 . v0)(v1 . v2)(v2 . v1)(v3 . v3))) ((= (v (^ v0 v2) (^ v0 (v v1 (v v2 v3)))) (^ v0 (v v1 (v v2 v3))))))
(493 (paramod 492 (1 1) 491 (1 1 2 2 2)) ((= (^ (v (^ v0 v1) v2) (^ v0 (v v1 (^ v0 (v v1 (v v2 v3)))))) (^ (v (^ v0 v1) v2) v0))))
(494 (instantiate 439 ((v0 . v0)(v1 . v1)(v2 . (v v2 v3)))) ((= (^ v0 (v v1 (^ v0 (v v1 (v v2 v3))))) (^ v0 (v v1 (v v2 v3))))))
(495 (paramod 494 (1 1) 493 (1 1 2)) ((= (^ (v (^ v0 v1) v2) (^ v0 (v v1 (v v2 v3)))) (^ (v (^ v0 v1) v2) v0))))
(496 (paramod 469 (1 1) 495 (1 2)) ((= (^ (v (^ v0 v1) v2) (^ v0 (v v1 (v v2 v3)))) (^ v0 (v v1 v2)))))
(497 (instantiate 476 ((v0 . (v (^ v0 v1) v2))(v1 . v0)(v2 . v1)(v3 . (v v2 v3)))) ((= (^ (v (^ v0 v1) v2) (v (^ v0 v1) (^ v0 (v v2 v3)))) (^ (v (^ v0 v1) v2) (^ v0 (v v1 (^ v0 (v v2 v3))))))))
(498 (paramod 497 (1 1) 461 (1 2)) ((= (v (^ v0 v1) (^ v0 (v v2 (^ v0 (^ v1 v3))))) (^ (v (^ v0 v1) v2) (^ v0 (v v1 (^ v0 (v v2 v3))))))))
(499 (instantiate 485 ((v0 . v2)(v1 . v3)(v2 . v0)(v3 . v1))) ((= (^ v2 (v v3 (^ v0 (v v2 v1)))) (^ v2 (v v3 v0)))))
(500 (paramod 499 (1 1) 387 (1 2 2)) ((= (v (^ v0 v1) (^ v2 (v v3 (^ v2 v0)))) (v (^ v0 v1) (^ v2 (v v3 v0))))))
(501 (instantiate 500 ((v0 . v0)(v1 . v1)(v2 . v1)(v3 . v2))) ((= (v (^ v0 v1) (^ v1 (v v2 (^ v1 v0)))) (v (^ v0 v1) (^ v1 (v v2 v0))))))
(502 (paramod 501 (1 1) 465 (1 1)) ((= (v (^ v0 v1) (^ v1 (v v2 v0))) (^ v1 (v v2 (^ v1 v0))))))
(503 (paramod 323 (1 1) 502 (1 1)) ((= (^ v1 (v v2 v0)) (^ v1 (v v2 (^ v1 v0))))))
(504 (flip 503 (1)) ((= (^ v1 (v v2 (^ v1 v0))) (^ v1 (v v2 v0)))))
(505 (instantiate 504 ((v0 . v2)(v1 . v0)(v2 . v1))) ((= (^ v0 (v v1 (^ v0 v2))) (^ v0 (v v1 v2)))))
(506 (instantiate 505 ((v0 . v0)(v1 . v2)(v2 . (^ v1 v3)))) ((= (^ v0 (v v2 (^ v0 (^ v1 v3)))) (^ v0 (v v2 (^ v1 v3))))))
(507 (paramod 506 (1 1) 498 (1 1 2)) ((= (v (^ v0 v1) (^ v0 (v v2 (^ v1 v3)))) (^ (v (^ v0 v1) v2) (^ v0 (v v1 (^ v0 (v v2 v3))))))))
(508 (instantiate 505 ((v0 . v0)(v1 . v1)(v2 . (v v2 v3)))) ((= (^ v0 (v v1 (^ v0 (v v2 v3)))) (^ v0 (v v1 (v v2 v3))))))
(509 (paramod 508 (1 1) 507 (1 2 2)) ((= (v (^ v0 v1) (^ v0 (v v2 (^ v1 v3)))) (^ (v (^ v0 v1) v2) (^ v0 (v v1 (v v2 v3)))))))
(510 (paramod 496 (1 1) 509 (1 2)) ((= (v (^ v0 v1) (^ v0 (v v2 (^ v1 v3)))) (^ v0 (v v1 v2)))))
(511 (instantiate 505 ((v0 . v1)(v1 . v2)(v2 . v3))) ((= (^ v1 (v v2 (^ v1 v3))) (^ v1 (v v2 v3)))))
(512 (paramod 511 (1 1) 476 (1 2 2)) ((= (^ v0 (v (^ v1 v2) (^ v1 v3))) (^ v0 (^ v1 (v v2 v3))))))
(513 (instantiate 510 ((v0 . (A))(v1 . (C))(v2 . (B))(v3 . (D)))) ((= (v (^ (A) (C)) (^ (A) (v (B) (^ (C) (D))))) (^ (A) (v (C) (B))))))
(514 (paramod 513 (1 1) 337 (1 1 1 2 2 2 2)) ((not (= (^ (A) (^ (v (B) (C)) (^ (v (B) (D)) (v (^ (A) (D)) (^ (A) (v (C) (B))))))) (^ (A) (^ (v (B) (C)) (v (B) (D))))))))
(515 (instantiate 512 ((v0 . (v (B) (D)))(v1 . (A))(v2 . (D))(v3 . (v (C) (B))))) ((= (^ (v (B) (D)) (v (^ (A) (D)) (^ (A) (v (C) (B))))) (^ (v (B) (D)) (^ (A) (v (D) (v (C) (B))))))))
(516 (paramod 515 (1 1) 514 (1 1 1 2 2)) ((not (= (^ (A) (^ (v (B) (C)) (^ (v (B) (D)) (^ (A) (v (D) (v (C) (B))))))) (^ (A) (^ (v (B) (C)) (v (B) (D))))))))
(517 (instantiate 319 ((v0 . (B))(v1 . (D))(v2 . (A))(v3 . (C)))) ((= (^ (v (B) (D)) (^ (A) (v (D) (v (C) (B))))) (^ (v (B) (D)) (A)))))
(518 (paramod 517 (1 1) 516 (1 1 1 2 2)) ((not (= (^ (A) (^ (v (B) (C)) (^ (v (B) (D)) (A)))) (^ (A) (^ (v (B) (C)) (v (B) (D))))))))
(519 (instantiate 158 ((v0 . (A))(v1 . (v (B) (C)))(v2 . (v (B) (D))))) ((= (^ (A) (^ (v (B) (C)) (^ (v (B) (D)) (A)))) (^ (A) (^ (v (B) (C)) (v (B) (D)))))))
(520 (paramod 519 (1 1) 518 (1 1 1)) ((not (= (^ (A) (^ (v (B) (C)) (v (B) (D)))) (^ (A) (^ (v (B) (C)) (v (B) (D))))))))
(521 (instantiate 1 ((v0 . (^ (A) (^ (v (B) (C)) (v (B) (D))))))) ((= (^ (A) (^ (v (B) (C)) (v (B) (D)))) (^ (A) (^ (v (B) (C)) (v (B) (D)))))))
(522 (resolve 520 (1) 521 (1)) ())
)