;; ----- Otter 3.0.4, August 1995 -----
;; The job was started by mccune on gyro, Wed Nov  1 23:11:44 1995
;;
;;;; x=x.
;;;; x^x=x.
;;;; x^y=y^x.
;;;; (x^y)^z=x^ (y^z).
;;;; x v x=x.
;;;; x v y=y v x.
;;;; (x v y) v z=x v (y v z).
;;;; (x^ (y v z)) v (x^y)=x^ (y v z).
;;;; (x v (y^z))^ (x v y)=x v (y^z).
;;;; (((x^y) v z)^y) v (z^x)= (((x v y)^z) v y)^ (z v x).
;;;; A^ (B v C)!= (A^B) v (A^C).
;;
;; ----> UNIT CONFLICT at 165.96 sec ----> 958 [binary,957.1,952.1] $F.
;;
(
(1 (input) ((= (^ v0 v0) v0)))
(2 (input) ((= (^ v0 v1) (^ v1 v0))))
(3 (input) ((= (^ (^ v0 v1) v2) (^ v0 (^ v1 v2)))))
(4 (input) ((= (v v0 v0) v0)))
(5 (input) ((= (v v0 v1) (v v1 v0))))
(6 (input) ((= (v (v v0 v1) v2) (v v0 (v v1 v2)))))
(7 (input) ((= (v (^ v0 (v v1 v2)) (^ v0 v1)) (^ v0 (v v1 v2)))))
(8 (input) ((= (^ (v v0 (^ v1 v2)) (v v0 v1)) (v v0 (^ v1 v2)))))
(9 (input) ((= (v (^ (v (^ v0 v1) v2) v1) (^ v2 v0)) (^ (v (^ (v v0 v1) v2) v1) (v v2 v0)))))
(10 (input) ((not (= (^ (A) (v (B) (C))) (v (^ (A) (B)) (^ (A) (C)))))))
(11 (flip 10 (1)) ((not (= (v (^ (A) (B)) (^ (A) (C))) (^ (A) (v (B) (C)))))))
(12 (instantiate 2 ((v0 . v64)(v1 . v65))) ((= (^ v64 v65) (^ v65 v64))))
(13 (instantiate 3 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (^ (^ v64 v65) v66) (^ v64 (^ v65 v66)))))
(14 (paramod 12 (1 1) 13 (1 1 1)) ((= (^ (^ v65 v64) v66) (^ v64 (^ v65 v66)))))
(15 (instantiate 3 ((v0 . v65)(v1 . v64)(v2 . v66))) ((= (^ (^ v65 v64) v66) (^ v65 (^ v64 v66)))))
(16 (paramod 15 (1 1) 14 (1 1)) ((= (^ v65 (^ v64 v66)) (^ v64 (^ v65 v66)))))
(17 (instantiate 16 ((v64 . v1)(v65 . v0)(v66 . v2))) ((= (^ v0 (^ v1 v2)) (^ v1 (^ v0 v2)))))
(18 (instantiate 1 ((v0 . v65))) ((= (^ v65 v65) v65)))
(19 (instantiate 3 ((v0 . v65)(v1 . v65)(v2 . v66))) ((= (^ (^ v65 v65) v66) (^ v65 (^ v65 v66)))))
(20 (paramod 18 (1 1) 19 (1 1 1)) ((= (^ v65 v66) (^ v65 (^ v65 v66)))))
(21 (flip 20 (1)) ((= (^ v65 (^ v65 v66)) (^ v65 v66))))
(22 (instantiate 21 ((v65 . v0)(v66 . v1))) ((= (^ v0 (^ v0 v1)) (^ v0 v1))))
(23 (instantiate 2 ((v0 . (^ v64 v65))(v1 . v66))) ((= (^ (^ v64 v65) v66) (^ v66 (^ v64 v65)))))
(24 (instantiate 3 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (^ (^ v64 v65) v66) (^ v64 (^ v65 v66)))))
(25 (paramod 23 (1 1) 24 (1 1)) ((= (^ v66 (^ v64 v65)) (^ v64 (^ v65 v66)))))
(26 (instantiate 25 ((v64 . v1)(v65 . v2)(v66 . v0))) ((= (^ v0 (^ v1 v2)) (^ v1 (^ v2 v0)))))
(27 (flip 26 (1)) ((= (^ v1 (^ v2 v0)) (^ v0 (^ v1 v2)))))
(28 (instantiate 1 ((v0 . v66))) ((= (^ v66 v66) v66)))
(29 (instantiate 17 ((v0 . v64)(v1 . v66)(v2 . v66))) ((= (^ v64 (^ v66 v66)) (^ v66 (^ v64 v66)))))
(30 (paramod 28 (1 1) 29 (1 1 2)) ((= (^ v64 v66) (^ v66 (^ v64 v66)))))
(31 (flip 30 (1)) ((= (^ v66 (^ v64 v66)) (^ v64 v66))))
(32 (instantiate 31 ((v64 . v1)(v66 . v0))) ((= (^ v0 (^ v1 v0)) (^ v1 v0))))
(33 (instantiate 17 ((v0 . v64))) ((= (^ v64 (^ v1 v2)) (^ v1 (^ v64 v2)))))
(34 (instantiate 22 ((v0 . v64)(v1 . (^ v1 v2)))) ((= (^ v64 (^ v64 (^ v1 v2))) (^ v64 (^ v1 v2)))))
(35 (paramod 33 (1 1) 34 (1 1 2)) ((= (^ v64 (^ v1 (^ v64 v2))) (^ v64 (^ v1 v2)))))
(36 (instantiate 35 ((v64 . v0))) ((= (^ v0 (^ v1 (^ v0 v2))) (^ v0 (^ v1 v2)))))
(37 (instantiate 5 ((v0 . v64)(v1 . v65))) ((= (v v64 v65) (v v65 v64))))
(38 (instantiate 6 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (v (v v64 v65) v66) (v v64 (v v65 v66)))))
(39 (paramod 37 (1 1) 38 (1 1 1)) ((= (v (v v65 v64) v66) (v v64 (v v65 v66)))))
(40 (instantiate 6 ((v0 . v65)(v1 . v64)(v2 . v66))) ((= (v (v v65 v64) v66) (v v65 (v v64 v66)))))
(41 (paramod 40 (1 1) 39 (1 1)) ((= (v v65 (v v64 v66)) (v v64 (v v65 v66)))))
(42 (instantiate 41 ((v64 . v1)(v65 . v0)(v66 . v2))) ((= (v v0 (v v1 v2)) (v v1 (v v0 v2)))))
(43 (instantiate 4 ((v0 . v65))) ((= (v v65 v65) v65)))
(44 (instantiate 6 ((v0 . v65)(v1 . v65)(v2 . v66))) ((= (v (v v65 v65) v66) (v v65 (v v65 v66)))))
(45 (paramod 43 (1 1) 44 (1 1 1)) ((= (v v65 v66) (v v65 (v v65 v66)))))
(46 (flip 45 (1)) ((= (v v65 (v v65 v66)) (v v65 v66))))
(47 (instantiate 46 ((v65 . v0)(v66 . v1))) ((= (v v0 (v v0 v1)) (v v0 v1))))
(48 (instantiate 5 ((v0 . (v v64 v65))(v1 . v66))) ((= (v (v v64 v65) v66) (v v66 (v v64 v65)))))
(49 (instantiate 6 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (v (v v64 v65) v66) (v v64 (v v65 v66)))))
(50 (paramod 48 (1 1) 49 (1 1)) ((= (v v66 (v v64 v65)) (v v64 (v v65 v66)))))
(51 (instantiate 50 ((v64 . v1)(v65 . v2)(v66 . v0))) ((= (v v0 (v v1 v2)) (v v1 (v v2 v0)))))
(52 (flip 51 (1)) ((= (v v1 (v v2 v0)) (v v0 (v v1 v2)))))
(53 (instantiate 4 ((v0 . v66))) ((= (v v66 v66) v66)))
(54 (instantiate 42 ((v0 . v64)(v1 . v66)(v2 . v66))) ((= (v v64 (v v66 v66)) (v v66 (v v64 v66)))))
(55 (paramod 53 (1 1) 54 (1 1 2)) ((= (v v64 v66) (v v66 (v v64 v66)))))
(56 (flip 55 (1)) ((= (v v66 (v v64 v66)) (v v64 v66))))
(57 (instantiate 56 ((v64 . v1)(v66 . v0))) ((= (v v0 (v v1 v0)) (v v1 v0))))
(58 (instantiate 42 ((v0 . v64))) ((= (v v64 (v v1 v2)) (v v1 (v v64 v2)))))
(59 (instantiate 47 ((v0 . v64)(v1 . (v v1 v2)))) ((= (v v64 (v v64 (v v1 v2))) (v v64 (v v1 v2)))))
(60 (paramod 58 (1 1) 59 (1 1 2)) ((= (v v64 (v v1 (v v64 v2))) (v v64 (v v1 v2)))))
(61 (instantiate 60 ((v64 . v0))) ((= (v v0 (v v1 (v v0 v2))) (v v0 (v v1 v2)))))
(62 (instantiate 5 ((v0 . v65)(v1 . v66))) ((= (v v65 v66) (v v66 v65))))
(63 (instantiate 51 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (v v64 (v v65 v66)) (v v65 (v v66 v64)))))
(64 (paramod 62 (1 1) 63 (1 1 2)) ((= (v v64 (v v66 v65)) (v v65 (v v66 v64)))))
(65 (instantiate 64 ((v64 . v0)(v65 . v2)(v66 . v1))) ((= (v v0 (v v1 v2)) (v v2 (v v1 v0)))))
(66 (instantiate 42 ((v0 . v66))) ((= (v v66 (v v1 v2)) (v v1 (v v66 v2)))))
(67 (instantiate 52 ((v0 . (v v1 v2))(v1 . v65)(v2 . v66))) ((= (v v65 (v v66 (v v1 v2))) (v (v v1 v2) (v v65 v66)))))
(68 (paramod 66 (1 1) 67 (1 1 2)) ((= (v v65 (v v1 (v v66 v2))) (v (v v1 v2) (v v65 v66)))))
(69 (instantiate 6 ((v0 . v1)(v1 . v2)(v2 . (v v65 v66)))) ((= (v (v v1 v2) (v v65 v66)) (v v1 (v v2 (v v65 v66))))))
(70 (paramod 69 (1 1) 68 (1 2)) ((= (v v65 (v v1 (v v66 v2))) (v v1 (v v2 (v v65 v66))))))
(71 (instantiate 70 ((v2 . v3)(v65 . v0)(v66 . v2))) ((= (v v0 (v v1 (v v2 v3))) (v v1 (v v3 (v v0 v2))))))
(72 (flip 71 (1)) ((= (v v1 (v v3 (v v0 v2))) (v v0 (v v1 (v v2 v3))))))
(73 (instantiate 51 ((v0 . v65))) ((= (v v65 (v v1 v2)) (v v1 (v v2 v65)))))
(74 (instantiate 7 ((v0 . v64)(v1 . v65)(v2 . (v v1 v2)))) ((= (v (^ v64 (v v65 (v v1 v2))) (^ v64 v65)) (^ v64 (v v65 (v v1 v2))))))
(75 (paramod 73 (1 1) 74 (1 1 1 2)) ((= (v (^ v64 (v v1 (v v2 v65))) (^ v64 v65)) (^ v64 (v v65 (v v1 v2))))))
(76 (instantiate 75 ((v64 . v0)(v65 . v3))) ((= (v (^ v0 (v v1 (v v2 v3))) (^ v0 v3)) (^ v0 (v v3 (v v1 v2))))))
(77 (instantiate 3 ((v2 . (v v65 v66)))) ((= (^ (^ v0 v1) (v v65 v66)) (^ v0 (^ v1 (v v65 v66))))))
(78 (instantiate 7 ((v0 . (^ v0 v1))(v1 . v65)(v2 . v66))) ((= (v (^ (^ v0 v1) (v v65 v66)) (^ (^ v0 v1) v65)) (^ (^ v0 v1) (v v65 v66)))))
(79 (paramod 77 (1 1) 78 (1 1 1)) ((= (v (^ v0 (^ v1 (v v65 v66))) (^ (^ v0 v1) v65)) (^ (^ v0 v1) (v v65 v66)))))
(80 (instantiate 3 ((v0 . v0)(v1 . v1)(v2 . v65))) ((= (^ (^ v0 v1) v65) (^ v0 (^ v1 v65)))))
(81 (paramod 80 (1 1) 79 (1 1 2)) ((= (v (^ v0 (^ v1 (v v65 v66))) (^ v0 (^ v1 v65))) (^ (^ v0 v1) (v v65 v66)))))
(82 (instantiate 3 ((v0 . v0)(v1 . v1)(v2 . (v v65 v66)))) ((= (^ (^ v0 v1) (v v65 v66)) (^ v0 (^ v1 (v v65 v66))))))
(83 (paramod 82 (1 1) 81 (1 2)) ((= (v (^ v0 (^ v1 (v v65 v66))) (^ v0 (^ v1 v65))) (^ v0 (^ v1 (v v65 v66))))))
(84 (instantiate 83 ((v65 . v2)(v66 . v3))) ((= (v (^ v0 (^ v1 (v v2 v3))) (^ v0 (^ v1 v2))) (^ v0 (^ v1 (v v2 v3))))))
(85 (instantiate 2 ((v0 . v64)(v1 . (v v65 v66)))) ((= (^ v64 (v v65 v66)) (^ (v v65 v66) v64))))
(86 (instantiate 7 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (v (^ v64 (v v65 v66)) (^ v64 v65)) (^ v64 (v v65 v66)))))
(87 (paramod 85 (1 1) 86 (1 1 1)) ((= (v (^ (v v65 v66) v64) (^ v64 v65)) (^ v64 (v v65 v66)))))
(88 (instantiate 87 ((v64 . v2)(v65 . v0)(v66 . v1))) ((= (v (^ (v v0 v1) v2) (^ v2 v0)) (^ v2 (v v0 v1)))))
(89 (instantiate 1 ((v0 . (v v65 v66)))) ((= (^ (v v65 v66) (v v65 v66)) (v v65 v66))))
(90 (instantiate 7 ((v0 . (v v65 v66))(v1 . v65)(v2 . v66))) ((= (v (^ (v v65 v66) (v v65 v66)) (^ (v v65 v66) v65)) (^ (v v65 v66) (v v65 v66)))))
(91 (paramod 89 (1 1) 90 (1 1 1)) ((= (v (v v65 v66) (^ (v v65 v66) v65)) (^ (v v65 v66) (v v65 v66)))))
(92 (instantiate 6 ((v0 . v65)(v1 . v66)(v2 . (^ (v v65 v66) v65)))) ((= (v (v v65 v66) (^ (v v65 v66) v65)) (v v65 (v v66 (^ (v v65 v66) v65))))))
(93 (paramod 92 (1 1) 91 (1 1)) ((= (v v65 (v v66 (^ (v v65 v66) v65))) (^ (v v65 v66) (v v65 v66)))))
(94 (instantiate 1 ((v0 . (v v65 v66)))) ((= (^ (v v65 v66) (v v65 v66)) (v v65 v66))))
(95 (paramod 94 (1 1) 93 (1 2)) ((= (v v65 (v v66 (^ (v v65 v66) v65))) (v v65 v66))))
(96 (instantiate 95 ((v65 . v0)(v66 . v1))) ((= (v v0 (v v1 (^ (v v0 v1) v0))) (v v0 v1))))
(97 (instantiate 32 ((v0 . v64))) ((= (^ v64 (^ v1 v64)) (^ v1 v64))))
(98 (instantiate 7 ((v0 . v64)(v1 . (^ v1 v64))(v2 . v66))) ((= (v (^ v64 (v (^ v1 v64) v66)) (^ v64 (^ v1 v64))) (^ v64 (v (^ v1 v64) v66)))))
(99 (paramod 97 (1 1) 98 (1 1 2)) ((= (v (^ v64 (v (^ v1 v64) v66)) (^ v1 v64)) (^ v64 (v (^ v1 v64) v66)))))
(100 (instantiate 99 ((v64 . v0)(v66 . v2))) ((= (v (^ v0 (v (^ v1 v0) v2)) (^ v1 v0)) (^ v0 (v (^ v1 v0) v2)))))
(101 (instantiate 2 ((v0 . v64)(v1 . v65))) ((= (^ v64 v65) (^ v65 v64))))
(102 (instantiate 7 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (v (^ v64 (v v65 v66)) (^ v64 v65)) (^ v64 (v v65 v66)))))
(103 (paramod 101 (1 1) 102 (1 1 2)) ((= (v (^ v64 (v v65 v66)) (^ v65 v64)) (^ v64 (v v65 v66)))))
(104 (instantiate 103 ((v64 . v0)(v65 . v1)(v66 . v2))) ((= (v (^ v0 (v v1 v2)) (^ v1 v0)) (^ v0 (v v1 v2)))))
(105 (instantiate 5 ((v0 . (^ v64 (v v65 v66)))(v1 . (^ v64 v65)))) ((= (v (^ v64 (v v65 v66)) (^ v64 v65)) (v (^ v64 v65) (^ v64 (v v65 v66))))))
(106 (instantiate 7 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (v (^ v64 (v v65 v66)) (^ v64 v65)) (^ v64 (v v65 v66)))))
(107 (paramod 105 (1 1) 106 (1 1)) ((= (v (^ v64 v65) (^ v64 (v v65 v66))) (^ v64 (v v65 v66)))))
(108 (instantiate 107 ((v64 . v0)(v65 . v1)(v66 . v2))) ((= (v (^ v0 v1) (^ v0 (v v1 v2))) (^ v0 (v v1 v2)))))
(109 (instantiate 5 ((v0 . v64)(v1 . (^ v65 v66)))) ((= (v v64 (^ v65 v66)) (v (^ v65 v66) v64))))
(110 (instantiate 8 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (^ (v v64 (^ v65 v66)) (v v64 v65)) (v v64 (^ v65 v66)))))
(111 (paramod 109 (1 1) 110 (1 1 1)) ((= (^ (v (^ v65 v66) v64) (v v64 v65)) (v v64 (^ v65 v66)))))
(112 (instantiate 111 ((v64 . v2)(v65 . v0)(v66 . v1))) ((= (^ (v (^ v0 v1) v2) (v v2 v0)) (v v2 (^ v0 v1)))))
(113 (instantiate 5 ((v0 . v64)(v1 . v65))) ((= (v v64 v65) (v v65 v64))))
(114 (instantiate 8 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (^ (v v64 (^ v65 v66)) (v v64 v65)) (v v64 (^ v65 v66)))))
(115 (paramod 113 (1 1) 114 (1 1 2)) ((= (^ (v v64 (^ v65 v66)) (v v65 v64)) (v v64 (^ v65 v66)))))
(116 (instantiate 115 ((v64 . v0)(v65 . v1)(v66 . v2))) ((= (^ (v v0 (^ v1 v2)) (v v1 v0)) (v v0 (^ v1 v2)))))
(117 (instantiate 4 ((v0 . v65))) ((= (v v65 v65) v65)))
(118 (instantiate 8 ((v0 . v65)(v1 . v65)(v2 . v66))) ((= (^ (v v65 (^ v65 v66)) (v v65 v65)) (v v65 (^ v65 v66)))))
(119 (paramod 117 (1 1) 118 (1 1 2)) ((= (^ (v v65 (^ v65 v66)) v65) (v v65 (^ v65 v66)))))
(120 (instantiate 119 ((v65 . v0)(v66 . v1))) ((= (^ (v v0 (^ v0 v1)) v0) (v v0 (^ v0 v1)))))
(121 (instantiate 2 ((v0 . (v v64 (^ v65 v66)))(v1 . (v v64 v65)))) ((= (^ (v v64 (^ v65 v66)) (v v64 v65)) (^ (v v64 v65) (v v64 (^ v65 v66))))))
(122 (instantiate 8 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (^ (v v64 (^ v65 v66)) (v v64 v65)) (v v64 (^ v65 v66)))))
(123 (paramod 121 (1 1) 122 (1 1)) ((= (^ (v v64 v65) (v v64 (^ v65 v66))) (v v64 (^ v65 v66)))))
(124 (instantiate 123 ((v64 . v0)(v65 . v1)(v66 . v2))) ((= (^ (v v0 v1) (v v0 (^ v1 v2))) (v v0 (^ v1 v2)))))
(125 (instantiate 1 ((v0 . v65))) ((= (^ v65 v65) v65)))
(126 (instantiate 9 ((v0 . v65)(v1 . v65)(v2 . v66))) ((= (v (^ (v (^ v65 v65) v66) v65) (^ v66 v65)) (^ (v (^ (v v65 v65) v66) v65) (v v66 v65)))))
(127 (paramod 125 (1 1) 126 (1 1 1 1 1)) ((= (v (^ (v v65 v66) v65) (^ v66 v65)) (^ (v (^ (v v65 v65) v66) v65) (v v66 v65)))))
(128 (instantiate 4 ((v0 . v65))) ((= (v v65 v65) v65)))
(129 (paramod 128 (1 1) 127 (1 2 1 1 1)) ((= (v (^ (v v65 v66) v65) (^ v66 v65)) (^ (v (^ v65 v66) v65) (v v66 v65)))))
(130 (instantiate 129 ((v65 . v0)(v66 . v1))) ((= (v (^ (v v0 v1) v0) (^ v1 v0)) (^ (v (^ v0 v1) v0) (v v1 v0)))))
(131 (instantiate 2 ((v0 . (v (^ v64 v65) v66))(v1 . v65))) ((= (^ (v (^ v64 v65) v66) v65) (^ v65 (v (^ v64 v65) v66)))))
(132 (instantiate 9 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (v (^ (v (^ v64 v65) v66) v65) (^ v66 v64)) (^ (v (^ (v v64 v65) v66) v65) (v v66 v64)))))
(133 (paramod 131 (1 1) 132 (1 1 1)) ((= (v (^ v65 (v (^ v64 v65) v66)) (^ v66 v64)) (^ (v (^ (v v64 v65) v66) v65) (v v66 v64)))))
(134 (instantiate 133 ((v64 . v1)(v65 . v0)(v66 . v2))) ((= (v (^ v0 (v (^ v1 v0) v2)) (^ v2 v1)) (^ (v (^ (v v1 v0) v2) v0) (v v2 v1)))))
(135 (instantiate 57 ((v0 . v66))) ((= (v v66 (v v1 v66)) (v v1 v66))))
(136 (instantiate 84 ((v0 . v64)(v1 . v65)(v2 . v66)(v3 . (v v1 v66)))) ((= (v (^ v64 (^ v65 (v v66 (v v1 v66)))) (^ v64 (^ v65 v66))) (^ v64 (^ v65 (v v66 (v v1 v66)))))))
(137 (paramod 135 (1 1) 136 (1 1 1 2 2)) ((= (v (^ v64 (^ v65 (v v1 v66))) (^ v64 (^ v65 v66))) (^ v64 (^ v65 (v v66 (v v1 v66)))))))
(138 (instantiate 57 ((v0 . v66)(v1 . v1))) ((= (v v66 (v v1 v66)) (v v1 v66))))
(139 (paramod 138 (1 1) 137 (1 2 2 2)) ((= (v (^ v64 (^ v65 (v v1 v66))) (^ v64 (^ v65 v66))) (^ v64 (^ v65 (v v1 v66))))))
(140 (instantiate 139 ((v1 . v2)(v64 . v0)(v65 . v1)(v66 . v3))) ((= (v (^ v0 (^ v1 (v v2 v3))) (^ v0 (^ v1 v3))) (^ v0 (^ v1 (v v2 v3))))))
(141 (instantiate 1 ((v0 . (v v66 v67)))) ((= (^ (v v66 v67) (v v66 v67)) (v v66 v67))))
(142 (instantiate 84 ((v0 . v64)(v1 . (v v66 v67))(v2 . v66)(v3 . v67))) ((= (v (^ v64 (^ (v v66 v67) (v v66 v67))) (^ v64 (^ (v v66 v67) v66))) (^ v64 (^ (v v66 v67) (v v66 v67))))))
(143 (paramod 141 (1 1) 142 (1 1 1 2)) ((= (v (^ v64 (v v66 v67)) (^ v64 (^ (v v66 v67) v66))) (^ v64 (^ (v v66 v67) (v v66 v67))))))
(144 (instantiate 1 ((v0 . (v v66 v67)))) ((= (^ (v v66 v67) (v v66 v67)) (v v66 v67))))
(145 (paramod 144 (1 1) 143 (1 2 2)) ((= (v (^ v64 (v v66 v67)) (^ v64 (^ (v v66 v67) v66))) (^ v64 (v v66 v67)))))
(146 (instantiate 145 ((v64 . v0)(v66 . v1)(v67 . v2))) ((= (v (^ v0 (v v1 v2)) (^ v0 (^ (v v1 v2) v1))) (^ v0 (v v1 v2)))))
(147 (instantiate 57 ((v0 . v64))) ((= (v v64 (v v1 v64)) (v v1 v64))))
(148 (instantiate 88 ((v0 . v64)(v1 . (v v1 v64))(v2 . v66))) ((= (v (^ (v v64 (v v1 v64)) v66) (^ v66 v64)) (^ v66 (v v64 (v v1 v64))))))
(149 (paramod 147 (1 1) 148 (1 1 1 1)) ((= (v (^ (v v1 v64) v66) (^ v66 v64)) (^ v66 (v v64 (v v1 v64))))))
(150 (instantiate 57 ((v0 . v64)(v1 . v1))) ((= (v v64 (v v1 v64)) (v v1 v64))))
(151 (paramod 150 (1 1) 149 (1 2 2)) ((= (v (^ (v v1 v64) v66) (^ v66 v64)) (^ v66 (v v1 v64)))))
(152 (instantiate 151 ((v1 . v0)(v64 . v1)(v66 . v2))) ((= (v (^ (v v0 v1) v2) (^ v2 v1)) (^ v2 (v v0 v1)))))
(153 (instantiate 4 ((v0 . v65))) ((= (v v65 v65) v65)))
(154 (instantiate 88 ((v0 . v65)(v1 . v65)(v2 . v66))) ((= (v (^ (v v65 v65) v66) (^ v66 v65)) (^ v66 (v v65 v65)))))
(155 (paramod 153 (1 1) 154 (1 1 1 1)) ((= (v (^ v65 v66) (^ v66 v65)) (^ v66 (v v65 v65)))))
(156 (instantiate 4 ((v0 . v65))) ((= (v v65 v65) v65)))
(157 (paramod 156 (1 1) 155 (1 2 2)) ((= (v (^ v65 v66) (^ v66 v65)) (^ v66 v65))))
(158 (instantiate 157 ((v65 . v0)(v66 . v1))) ((= (v (^ v0 v1) (^ v1 v0)) (^ v1 v0))))
(159 (instantiate 32 ((v0 . v66))) ((= (^ v66 (^ v1 v66)) (^ v1 v66))))
(160 (instantiate 88 ((v0 . (^ v1 v66))(v1 . v65)(v2 . v66))) ((= (v (^ (v (^ v1 v66) v65) v66) (^ v66 (^ v1 v66))) (^ v66 (v (^ v1 v66) v65)))))
(161 (paramod 159 (1 1) 160 (1 1 2)) ((= (v (^ (v (^ v1 v66) v65) v66) (^ v1 v66)) (^ v66 (v (^ v1 v66) v65)))))
(162 (instantiate 161 ((v1 . v0)(v65 . v2)(v66 . v1))) ((= (v (^ (v (^ v0 v1) v2) v1) (^ v0 v1)) (^ v1 (v (^ v0 v1) v2)))))
(163 (instantiate 2 ((v0 . v66)(v1 . v64))) ((= (^ v66 v64) (^ v64 v66))))
(164 (instantiate 88 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (v (^ (v v64 v65) v66) (^ v66 v64)) (^ v66 (v v64 v65)))))
(165 (paramod 163 (1 1) 164 (1 1 2)) ((= (v (^ (v v64 v65) v66) (^ v64 v66)) (^ v66 (v v64 v65)))))
(166 (instantiate 165 ((v64 . v0)(v65 . v1)(v66 . v2))) ((= (v (^ (v v0 v1) v2) (^ v0 v2)) (^ v2 (v v0 v1)))))
(167 (instantiate 1 ((v0 . v64))) ((= (^ v64 v64) v64)))
(168 (instantiate 88 ((v0 . v64)(v1 . v65)(v2 . v64))) ((= (v (^ (v v64 v65) v64) (^ v64 v64)) (^ v64 (v v64 v65)))))
(169 (paramod 167 (1 1) 168 (1 1 2)) ((= (v (^ (v v64 v65) v64) v64) (^ v64 (v v64 v65)))))
(170 (instantiate 169 ((v64 . v0)(v65 . v1))) ((= (v (^ (v v0 v1) v0) v0) (^ v0 (v v0 v1)))))
(171 (instantiate 76 ((v0 . (v v1 (v v2 v1)))(v3 . v1))) ((= (v (^ (v v1 (v v2 v1)) (v v1 (v v2 v1))) (^ (v v1 (v v2 v1)) v1)) (^ (v v1 (v v2 v1)) (v v1 (v v1 v2))))))
(172 (instantiate 88 ((v0 . v1)(v1 . (v v2 v1))(v2 . (v v1 (v v2 v1))))) ((= (v (^ (v v1 (v v2 v1)) (v v1 (v v2 v1))) (^ (v v1 (v v2 v1)) v1)) (^ (v v1 (v v2 v1)) (v v1 (v v2 v1))))))
(173 (paramod 171 (1 1) 172 (1 1)) ((= (^ (v v1 (v v2 v1)) (v v1 (v v1 v2))) (^ (v v1 (v v2 v1)) (v v1 (v v2 v1))))))
(174 (instantiate 57 ((v0 . v1)(v1 . v2))) ((= (v v1 (v v2 v1)) (v v2 v1))))
(175 (paramod 174 (1 1) 173 (1 1 1)) ((= (^ (v v2 v1) (v v1 (v v1 v2))) (^ (v v1 (v v2 v1)) (v v1 (v v2 v1))))))
(176 (instantiate 47 ((v0 . v1)(v1 . v2))) ((= (v v1 (v v1 v2)) (v v1 v2))))
(177 (paramod 176 (1 1) 175 (1 1 2)) ((= (^ (v v2 v1) (v v1 v2)) (^ (v v1 (v v2 v1)) (v v1 (v v2 v1))))))
(178 (instantiate 57 ((v0 . v1)(v1 . v2))) ((= (v v1 (v v2 v1)) (v v2 v1))))
(179 (paramod 178 (1 1) 177 (1 2 1)) ((= (^ (v v2 v1) (v v1 v2)) (^ (v v2 v1) (v v1 (v v2 v1))))))
(180 (instantiate 57 ((v0 . v1)(v1 . v2))) ((= (v v1 (v v2 v1)) (v v2 v1))))
(181 (paramod 180 (1 1) 179 (1 2 2)) ((= (^ (v v2 v1) (v v1 v2)) (^ (v v2 v1) (v v2 v1)))))
(182 (instantiate 1 ((v0 . (v v2 v1)))) ((= (^ (v v2 v1) (v v2 v1)) (v v2 v1))))
(183 (paramod 182 (1 1) 181 (1 2)) ((= (^ (v v2 v1) (v v1 v2)) (v v2 v1))))
(184 (instantiate 183 ((v2 . v0))) ((= (^ (v v0 v1) (v v1 v0)) (v v0 v1))))
(185 (instantiate 5 ((v0 . (^ (v v64 v65) v66))(v1 . (^ v66 v64)))) ((= (v (^ (v v64 v65) v66) (^ v66 v64)) (v (^ v66 v64) (^ (v v64 v65) v66)))))
(186 (instantiate 88 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (v (^ (v v64 v65) v66) (^ v66 v64)) (^ v66 (v v64 v65)))))
(187 (paramod 185 (1 1) 186 (1 1)) ((= (v (^ v66 v64) (^ (v v64 v65) v66)) (^ v66 (v v64 v65)))))
(188 (instantiate 187 ((v64 . v1)(v65 . v2)(v66 . v0))) ((= (v (^ v0 v1) (^ (v v1 v2) v0)) (^ v0 (v v1 v2)))))
(189 (instantiate 57 ((v0 . v64))) ((= (v v64 (v v1 v64)) (v v1 v64))))
(190 (instantiate 96 ((v0 . v64)(v1 . (v v1 v64)))) ((= (v v64 (v (v v1 v64) (^ (v v64 (v v1 v64)) v64))) (v v64 (v v1 v64)))))
(191 (paramod 189 (1 1) 190 (1 1 2 2 1)) ((= (v v64 (v (v v1 v64) (^ (v v1 v64) v64))) (v v64 (v v1 v64)))))
(192 (instantiate 6 ((v0 . v1)(v1 . v64)(v2 . (^ (v v1 v64) v64)))) ((= (v (v v1 v64) (^ (v v1 v64) v64)) (v v1 (v v64 (^ (v v1 v64) v64))))))
(193 (paramod 192 (1 1) 191 (1 1 2)) ((= (v v64 (v v1 (v v64 (^ (v v1 v64) v64)))) (v v64 (v v1 v64)))))
(194 (instantiate 61 ((v0 . v64)(v1 . v1)(v2 . (^ (v v1 v64) v64)))) ((= (v v64 (v v1 (v v64 (^ (v v1 v64) v64)))) (v v64 (v v1 (^ (v v1 v64) v64))))))
(195 (paramod 194 (1 1) 193 (1 1)) ((= (v v64 (v v1 (^ (v v1 v64) v64))) (v v64 (v v1 v64)))))
(196 (instantiate 57 ((v0 . v64)(v1 . v1))) ((= (v v64 (v v1 v64)) (v v1 v64))))
(197 (paramod 196 (1 1) 195 (1 2)) ((= (v v64 (v v1 (^ (v v1 v64) v64))) (v v1 v64))))
(198 (instantiate 197 ((v64 . v0))) ((= (v v0 (v v1 (^ (v v1 v0) v0))) (v v1 v0))))
(199 (instantiate 52 ((v0 . (^ (v v64 v65) v64))(v1 . v64)(v2 . v65))) ((= (v v64 (v v65 (^ (v v64 v65) v64))) (v (^ (v v64 v65) v64) (v v64 v65)))))
(200 (instantiate 96 ((v0 . v64)(v1 . v65))) ((= (v v64 (v v65 (^ (v v64 v65) v64))) (v v64 v65))))
(201 (paramod 199 (1 1) 200 (1 1)) ((= (v (^ (v v64 v65) v64) (v v64 v65)) (v v64 v65))))
(202 (instantiate 201 ((v64 . v0)(v65 . v1))) ((= (v (^ (v v0 v1) v0) (v v0 v1)) (v v0 v1))))
(203 (instantiate 96 ((v0 . v67)(v1 . v64))) ((= (v v67 (v v64 (^ (v v67 v64) v67))) (v v67 v64))))
(204 (instantiate 72 ((v0 . v64)(v1 . v65)(v2 . (^ (v v67 v64) v67))(v3 . v67))) ((= (v v65 (v v67 (v v64 (^ (v v67 v64) v67)))) (v v64 (v v65 (v (^ (v v67 v64) v67) v67))))))
(205 (paramod 203 (1 1) 204 (1 1 2)) ((= (v v65 (v v67 v64)) (v v64 (v v65 (v (^ (v v67 v64) v67) v67))))))
(206 (instantiate 170 ((v0 . v67)(v1 . v64))) ((= (v (^ (v v67 v64) v67) v67) (^ v67 (v v67 v64)))))
(207 (paramod 206 (1 1) 205 (1 2 2 2)) ((= (v v65 (v v67 v64)) (v v64 (v v65 (^ v67 (v v67 v64)))))))
(208 (flip 207 (1)) ((= (v v64 (v v65 (^ v67 (v v67 v64)))) (v v65 (v v67 v64)))))
(209 (instantiate 208 ((v64 . v0)(v65 . v1)(v67 . v2))) ((= (v v0 (v v1 (^ v2 (v v2 v0)))) (v v1 (v v2 v0)))))
(210 (instantiate 2 ((v0 . v65)(v1 . v64))) ((= (^ v65 v64) (^ v64 v65))))
(211 (instantiate 100 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (v (^ v64 (v (^ v65 v64) v66)) (^ v65 v64)) (^ v64 (v (^ v65 v64) v66)))))
(212 (paramod 210 (1 1) 211 (1 1 2)) ((= (v (^ v64 (v (^ v65 v64) v66)) (^ v64 v65)) (^ v64 (v (^ v65 v64) v66)))))
(213 (instantiate 212 ((v64 . v0)(v65 . v1)(v66 . v2))) ((= (v (^ v0 (v (^ v1 v0) v2)) (^ v0 v1)) (^ v0 (v (^ v1 v0) v2)))))
(214 (instantiate 5 ((v0 . (^ v64 (v (^ v65 v64) v66)))(v1 . (^ v65 v64)))) ((= (v (^ v64 (v (^ v65 v64) v66)) (^ v65 v64)) (v (^ v65 v64) (^ v64 (v (^ v65 v64) v66))))))
(215 (instantiate 100 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (v (^ v64 (v (^ v65 v64) v66)) (^ v65 v64)) (^ v64 (v (^ v65 v64) v66)))))
(216 (paramod 214 (1 1) 215 (1 1)) ((= (v (^ v65 v64) (^ v64 (v (^ v65 v64) v66))) (^ v64 (v (^ v65 v64) v66)))))
(217 (instantiate 216 ((v64 . v1)(v65 . v0)(v66 . v2))) ((= (v (^ v0 v1) (^ v1 (v (^ v0 v1) v2))) (^ v1 (v (^ v0 v1) v2)))))
(218 (instantiate 2 ((v0 . v64)(v1 . v65))) ((= (^ v64 v65) (^ v65 v64))))
(219 (instantiate 108 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (v (^ v64 v65) (^ v64 (v v65 v66))) (^ v64 (v v65 v66)))))
(220 (paramod 218 (1 1) 219 (1 1 1)) ((= (v (^ v65 v64) (^ v64 (v v65 v66))) (^ v64 (v v65 v66)))))
(221 (instantiate 220 ((v64 . v1)(v65 . v0)(v66 . v2))) ((= (v (^ v0 v1) (^ v1 (v v0 v2))) (^ v1 (v v0 v2)))))
(222 (instantiate 57 ((v0 . v65))) ((= (v v65 (v v1 v65)) (v v1 v65))))
(223 (instantiate 108 ((v0 . v64)(v1 . v65)(v2 . (v v1 v65)))) ((= (v (^ v64 v65) (^ v64 (v v65 (v v1 v65)))) (^ v64 (v v65 (v v1 v65))))))
(224 (paramod 222 (1 1) 223 (1 1 2 2)) ((= (v (^ v64 v65) (^ v64 (v v1 v65))) (^ v64 (v v65 (v v1 v65))))))
(225 (instantiate 57 ((v0 . v65)(v1 . v1))) ((= (v v65 (v v1 v65)) (v v1 v65))))
(226 (paramod 225 (1 1) 224 (1 2 2)) ((= (v (^ v64 v65) (^ v64 (v v1 v65))) (^ v64 (v v1 v65)))))
(227 (instantiate 226 ((v1 . v2)(v64 . v0)(v65 . v1))) ((= (v (^ v0 v1) (^ v0 (v v2 v1))) (^ v0 (v v2 v1)))))
(228 (instantiate 6 ((v0 . (^ v0 v1))(v1 . (^ v0 (v v1 v2)))(v2 . v66))) ((= (v (v (^ v0 v1) (^ v0 (v v1 v2))) v66) (v (^ v0 v1) (v (^ v0 (v v1 v2)) v66)))))
(229 (paramod 108 (1 1) 228 (1 1 1)) ((= (v (^ v0 (v v1 v2)) v66) (v (^ v0 v1) (v (^ v0 (v v1 v2)) v66)))))
(230 (flip 229 (1)) ((= (v (^ v0 v1) (v (^ v0 (v v1 v2)) v66)) (v (^ v0 (v v1 v2)) v66))))
(231 (instantiate 230 ((v66 . v3))) ((= (v (^ v0 v1) (v (^ v0 (v v1 v2)) v3)) (v (^ v0 (v v1 v2)) v3))))
(232 (instantiate 32 ((v0 . v64))) ((= (^ v64 (^ v1 v64)) (^ v1 v64))))
(233 (instantiate 112 ((v0 . v64)(v1 . (^ v1 v64))(v2 . v66))) ((= (^ (v (^ v64 (^ v1 v64)) v66) (v v66 v64)) (v v66 (^ v64 (^ v1 v64))))))
(234 (paramod 232 (1 1) 233 (1 1 1 1)) ((= (^ (v (^ v1 v64) v66) (v v66 v64)) (v v66 (^ v64 (^ v1 v64))))))
(235 (instantiate 32 ((v0 . v64)(v1 . v1))) ((= (^ v64 (^ v1 v64)) (^ v1 v64))))
(236 (paramod 235 (1 1) 234 (1 2 2)) ((= (^ (v (^ v1 v64) v66) (v v66 v64)) (v v66 (^ v1 v64)))))
(237 (instantiate 236 ((v1 . v0)(v64 . v1)(v66 . v2))) ((= (^ (v (^ v0 v1) v2) (v v2 v1)) (v v2 (^ v0 v1)))))
(238 (instantiate 5 ((v0 . v66)(v1 . v64))) ((= (v v66 v64) (v v64 v66))))
(239 (instantiate 112 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (^ (v (^ v64 v65) v66) (v v66 v64)) (v v66 (^ v64 v65)))))
(240 (paramod 238 (1 1) 239 (1 1 2)) ((= (^ (v (^ v64 v65) v66) (v v64 v66)) (v v66 (^ v64 v65)))))
(241 (instantiate 240 ((v64 . v0)(v65 . v1)(v66 . v2))) ((= (^ (v (^ v0 v1) v2) (v v0 v2)) (v v2 (^ v0 v1)))))
(242 (instantiate 4 ((v0 . v64))) ((= (v v64 v64) v64)))
(243 (instantiate 112 ((v0 . v64)(v1 . v65)(v2 . v64))) ((= (^ (v (^ v64 v65) v64) (v v64 v64)) (v v64 (^ v64 v65)))))
(244 (paramod 242 (1 1) 243 (1 1 2)) ((= (^ (v (^ v64 v65) v64) v64) (v v64 (^ v64 v65)))))
(245 (instantiate 244 ((v64 . v0)(v65 . v1))) ((= (^ (v (^ v0 v1) v0) v0) (v v0 (^ v0 v1)))))
(246 (instantiate 112 ((v0 . v64)(v1 . (v v66 v64))(v2 . v66))) ((= (^ (v (^ v64 (v v66 v64)) v66) (v v66 v64)) (v v66 (^ v64 (v v66 v64))))))
(247 (instantiate 9 ((v0 . v64)(v1 . (v v66 v64))(v2 . v66))) ((= (v (^ (v (^ v64 (v v66 v64)) v66) (v v66 v64)) (^ v66 v64)) (^ (v (^ (v v64 (v v66 v64)) v66) (v v66 v64)) (v v66 v64)))))
(248 (paramod 246 (1 1) 247 (1 1 1)) ((= (v (v v66 (^ v64 (v v66 v64))) (^ v66 v64)) (^ (v (^ (v v64 (v v66 v64)) v66) (v v66 v64)) (v v66 v64)))))
(249 (instantiate 6 ((v0 . v66)(v1 . (^ v64 (v v66 v64)))(v2 . (^ v66 v64)))) ((= (v (v v66 (^ v64 (v v66 v64))) (^ v66 v64)) (v v66 (v (^ v64 (v v66 v64)) (^ v66 v64))))))
(250 (paramod 249 (1 1) 248 (1 1)) ((= (v v66 (v (^ v64 (v v66 v64)) (^ v66 v64))) (^ (v (^ (v v64 (v v66 v64)) v66) (v v66 v64)) (v v66 v64)))))
(251 (instantiate 104 ((v0 . v64)(v1 . v66)(v2 . v64))) ((= (v (^ v64 (v v66 v64)) (^ v66 v64)) (^ v64 (v v66 v64)))))
(252 (paramod 251 (1 1) 250 (1 1 2)) ((= (v v66 (^ v64 (v v66 v64))) (^ (v (^ (v v64 (v v66 v64)) v66) (v v66 v64)) (v v66 v64)))))
(253 (instantiate 57 ((v0 . v64)(v1 . v66))) ((= (v v64 (v v66 v64)) (v v66 v64))))
(254 (paramod 253 (1 1) 252 (1 2 1 1 1)) ((= (v v66 (^ v64 (v v66 v64))) (^ (v (^ (v v66 v64) v66) (v v66 v64)) (v v66 v64)))))
(255 (instantiate 202 ((v0 . v66)(v1 . v64))) ((= (v (^ (v v66 v64) v66) (v v66 v64)) (v v66 v64))))
(256 (paramod 255 (1 1) 254 (1 2 1)) ((= (v v66 (^ v64 (v v66 v64))) (^ (v v66 v64) (v v66 v64)))))
(257 (instantiate 1 ((v0 . (v v66 v64)))) ((= (^ (v v66 v64) (v v66 v64)) (v v66 v64))))
(258 (paramod 257 (1 1) 256 (1 2)) ((= (v v66 (^ v64 (v v66 v64))) (v v66 v64))))
(259 (instantiate 258 ((v64 . v1)(v66 . v0))) ((= (v v0 (^ v1 (v v0 v1))) (v v0 v1))))
(260 (instantiate 112 ((v0 . v66)(v2 . v65))) ((= (^ (v (^ v66 v1) v65) (v v65 v66)) (v v65 (^ v66 v1)))))
(261 (instantiate 7 ((v0 . (v (^ v66 v1) v65))(v1 . v65)(v2 . v66))) ((= (v (^ (v (^ v66 v1) v65) (v v65 v66)) (^ (v (^ v66 v1) v65) v65)) (^ (v (^ v66 v1) v65) (v v65 v66)))))
(262 (paramod 260 (1 1) 261 (1 1 1)) ((= (v (v v65 (^ v66 v1)) (^ (v (^ v66 v1) v65) v65)) (^ (v (^ v66 v1) v65) (v v65 v66)))))
(263 (instantiate 6 ((v0 . v65)(v1 . (^ v66 v1))(v2 . (^ (v (^ v66 v1) v65) v65)))) ((= (v (v v65 (^ v66 v1)) (^ (v (^ v66 v1) v65) v65)) (v v65 (v (^ v66 v1) (^ (v (^ v66 v1) v65) v65))))))
(264 (paramod 263 (1 1) 262 (1 1)) ((= (v v65 (v (^ v66 v1) (^ (v (^ v66 v1) v65) v65))) (^ (v (^ v66 v1) v65) (v v65 v66)))))
(265 (instantiate 198 ((v0 . v65)(v1 . (^ v66 v1)))) ((= (v v65 (v (^ v66 v1) (^ (v (^ v66 v1) v65) v65))) (v (^ v66 v1) v65))))
(266 (paramod 265 (1 1) 264 (1 1)) ((= (v (^ v66 v1) v65) (^ (v (^ v66 v1) v65) (v v65 v66)))))
(267 (flip 266 (1)) ((= (^ (v (^ v66 v1) v65) (v v65 v66)) (v (^ v66 v1) v65))))
(268 (instantiate 267 ((v65 . v2)(v66 . v0))) ((= (^ (v (^ v0 v1) v2) (v v2 v0)) (v (^ v0 v1) v2))))
(269 (instantiate 5 ((v0 . v64)(v1 . v65))) ((= (v v64 v65) (v v65 v64))))
(270 (instantiate 124 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (^ (v v64 v65) (v v64 (^ v65 v66))) (v v64 (^ v65 v66)))))
(271 (paramod 269 (1 1) 270 (1 1 1)) ((= (^ (v v65 v64) (v v64 (^ v65 v66))) (v v64 (^ v65 v66)))))
(272 (instantiate 271 ((v64 . v1)(v65 . v0)(v66 . v2))) ((= (^ (v v0 v1) (v v1 (^ v0 v2))) (v v1 (^ v0 v2)))))
(273 (instantiate 32 ((v0 . v65))) ((= (^ v65 (^ v1 v65)) (^ v1 v65))))
(274 (instantiate 124 ((v0 . v64)(v1 . v65)(v2 . (^ v1 v65)))) ((= (^ (v v64 v65) (v v64 (^ v65 (^ v1 v65)))) (v v64 (^ v65 (^ v1 v65))))))
(275 (paramod 273 (1 1) 274 (1 1 2 2)) ((= (^ (v v64 v65) (v v64 (^ v1 v65))) (v v64 (^ v65 (^ v1 v65))))))
(276 (instantiate 32 ((v0 . v65)(v1 . v1))) ((= (^ v65 (^ v1 v65)) (^ v1 v65))))
(277 (paramod 276 (1 1) 275 (1 2 2)) ((= (^ (v v64 v65) (v v64 (^ v1 v65))) (v v64 (^ v1 v65)))))
(278 (instantiate 277 ((v1 . v2)(v64 . v0)(v65 . v1))) ((= (^ (v v0 v1) (v v0 (^ v2 v1))) (v v0 (^ v2 v1)))))
(279 (instantiate 108 ((v0 . v65))) ((= (v (^ v65 v1) (^ v65 (v v1 v2))) (^ v65 (v v1 v2)))))
(280 (instantiate 124 ((v0 . (^ v65 v1))(v1 . v65)(v2 . (v v1 v2)))) ((= (^ (v (^ v65 v1) v65) (v (^ v65 v1) (^ v65 (v v1 v2)))) (v (^ v65 v1) (^ v65 (v v1 v2))))))
(281 (paramod 279 (1 1) 280 (1 1 2)) ((= (^ (v (^ v65 v1) v65) (^ v65 (v v1 v2))) (v (^ v65 v1) (^ v65 (v v1 v2))))))
(282 (instantiate 108 ((v0 . v65)(v1 . v1)(v2 . v2))) ((= (v (^ v65 v1) (^ v65 (v v1 v2))) (^ v65 (v v1 v2)))))
(283 (paramod 282 (1 1) 281 (1 2)) ((= (^ (v (^ v65 v1) v65) (^ v65 (v v1 v2))) (^ v65 (v v1 v2)))))
(284 (instantiate 283 ((v65 . v0))) ((= (^ (v (^ v0 v1) v0) (^ v0 (v v1 v2))) (^ v0 (v v1 v2)))))
(285 (instantiate 120 ((v0 . v64))) ((= (^ (v v64 (^ v64 v1)) v64) (v v64 (^ v64 v1)))))
(286 (instantiate 130 ((v0 . v64)(v1 . (^ v64 v1)))) ((= (v (^ (v v64 (^ v64 v1)) v64) (^ (^ v64 v1) v64)) (^ (v (^ v64 (^ v64 v1)) v64) (v (^ v64 v1) v64)))))
(287 (paramod 285 (1 1) 286 (1 1 1)) ((= (v (v v64 (^ v64 v1)) (^ (^ v64 v1) v64)) (^ (v (^ v64 (^ v64 v1)) v64) (v (^ v64 v1) v64)))))
(288 (instantiate 3 ((v0 . v64)(v1 . v1)(v2 . v64))) ((= (^ (^ v64 v1) v64) (^ v64 (^ v1 v64)))))
(289 (paramod 288 (1 1) 287 (1 1 2)) ((= (v (v v64 (^ v64 v1)) (^ v64 (^ v1 v64))) (^ (v (^ v64 (^ v64 v1)) v64) (v (^ v64 v1) v64)))))
(290 (instantiate 32 ((v0 . v64)(v1 . v1))) ((= (^ v64 (^ v1 v64)) (^ v1 v64))))
(291 (paramod 290 (1 1) 289 (1 1 2)) ((= (v (v v64 (^ v64 v1)) (^ v1 v64)) (^ (v (^ v64 (^ v64 v1)) v64) (v (^ v64 v1) v64)))))
(292 (instantiate 6 ((v0 . v64)(v1 . (^ v64 v1))(v2 . (^ v1 v64)))) ((= (v (v v64 (^ v64 v1)) (^ v1 v64)) (v v64 (v (^ v64 v1) (^ v1 v64))))))
(293 (paramod 292 (1 1) 291 (1 1)) ((= (v v64 (v (^ v64 v1) (^ v1 v64))) (^ (v (^ v64 (^ v64 v1)) v64) (v (^ v64 v1) v64)))))
(294 (instantiate 158 ((v0 . v64)(v1 . v1))) ((= (v (^ v64 v1) (^ v1 v64)) (^ v1 v64))))
(295 (paramod 294 (1 1) 293 (1 1 2)) ((= (v v64 (^ v1 v64)) (^ (v (^ v64 (^ v64 v1)) v64) (v (^ v64 v1) v64)))))
(296 (instantiate 22 ((v0 . v64)(v1 . v1))) ((= (^ v64 (^ v64 v1)) (^ v64 v1))))
(297 (paramod 296 (1 1) 295 (1 2 1 1)) ((= (v v64 (^ v1 v64)) (^ (v (^ v64 v1) v64) (v (^ v64 v1) v64)))))
(298 (instantiate 1 ((v0 . (v (^ v64 v1) v64)))) ((= (^ (v (^ v64 v1) v64) (v (^ v64 v1) v64)) (v (^ v64 v1) v64))))
(299 (paramod 298 (1 1) 297 (1 2)) ((= (v v64 (^ v1 v64)) (v (^ v64 v1) v64))))
(300 (flip 299 (1)) ((= (v (^ v64 v1) v64) (v v64 (^ v1 v64)))))
(301 (instantiate 300 ((v64 . v0))) ((= (v (^ v0 v1) v0) (v v0 (^ v1 v0)))))
(302 (instantiate 2 ((v0 . v65)(v1 . v64))) ((= (^ v65 v64) (^ v64 v65))))
(303 (instantiate 130 ((v0 . v64)(v1 . v65))) ((= (v (^ (v v64 v65) v64) (^ v65 v64)) (^ (v (^ v64 v65) v64) (v v65 v64)))))
(304 (paramod 302 (1 1) 303 (1 1 2)) ((= (v (^ (v v64 v65) v64) (^ v64 v65)) (^ (v (^ v64 v65) v64) (v v65 v64)))))
(305 (instantiate 152 ((v0 . v64)(v1 . v65)(v2 . v64))) ((= (v (^ (v v64 v65) v64) (^ v64 v65)) (^ v64 (v v64 v65)))))
(306 (paramod 305 (1 1) 304 (1 1)) ((= (^ v64 (v v64 v65)) (^ (v (^ v64 v65) v64) (v v65 v64)))))
(307 (instantiate 301 ((v0 . v64)(v1 . v65))) ((= (v (^ v64 v65) v64) (v v64 (^ v65 v64)))))
(308 (paramod 307 (1 1) 306 (1 2 1)) ((= (^ v64 (v v64 v65)) (^ (v v64 (^ v65 v64)) (v v65 v64)))))
(309 (instantiate 116 ((v0 . v64)(v1 . v65)(v2 . v64))) ((= (^ (v v64 (^ v65 v64)) (v v65 v64)) (v v64 (^ v65 v64)))))
(310 (paramod 309 (1 1) 308 (1 2)) ((= (^ v64 (v v64 v65)) (v v64 (^ v65 v64)))))
(311 (flip 310 (1)) ((= (v v64 (^ v65 v64)) (^ v64 (v v64 v65)))))
(312 (instantiate 311 ((v64 . v0)(v65 . v1))) ((= (v v0 (^ v1 v0)) (^ v0 (v v0 v1)))))
(313 (paramod 301 (1 1) 284 (1 1 1)) ((= (^ (v v0 (^ v1 v0)) (^ v0 (v v1 v2))) (^ v0 (v v1 v2)))))
(314 (paramod 312 (1 1) 313 (1 1 1)) ((= (^ (^ v0 (v v0 v1)) (^ v0 (v v1 v2))) (^ v0 (v v1 v2)))))
(315 (instantiate 3 ((v0 . v0)(v1 . (v v0 v1))(v2 . (^ v0 (v v1 v2))))) ((= (^ (^ v0 (v v0 v1)) (^ v0 (v v1 v2))) (^ v0 (^ (v v0 v1) (^ v0 (v v1 v2)))))))
(316 (paramod 315 (1 1) 314 (1 1)) ((= (^ v0 (^ (v v0 v1) (^ v0 (v v1 v2)))) (^ v0 (v v1 v2)))))
(317 (instantiate 36 ((v0 . v0)(v1 . (v v0 v1))(v2 . (v v1 v2)))) ((= (^ v0 (^ (v v0 v1) (^ v0 (v v1 v2)))) (^ v0 (^ (v v0 v1) (v v1 v2))))))
(318 (paramod 317 (1 1) 316 (1 1)) ((= (^ v0 (^ (v v0 v1) (v v1 v2))) (^ v0 (v v1 v2)))))
(319 (paramod 301 (1 1) 245 (1 1 1)) ((= (^ (v v0 (^ v1 v0)) v0) (v v0 (^ v0 v1)))))
(320 (paramod 312 (1 1) 319 (1 1 1)) ((= (^ (^ v0 (v v0 v1)) v0) (v v0 (^ v0 v1)))))
(321 (instantiate 3 ((v0 . v0)(v1 . (v v0 v1))(v2 . v0))) ((= (^ (^ v0 (v v0 v1)) v0) (^ v0 (^ (v v0 v1) v0)))))
(322 (paramod 321 (1 1) 320 (1 1)) ((= (^ v0 (^ (v v0 v1) v0)) (v v0 (^ v0 v1)))))
(323 (instantiate 32 ((v0 . v0)(v1 . (v v0 v1)))) ((= (^ v0 (^ (v v0 v1) v0)) (^ (v v0 v1) v0))))
(324 (paramod 323 (1 1) 322 (1 1)) ((= (^ (v v0 v1) v0) (v v0 (^ v0 v1)))))
(325 (flip 324 (1)) ((= (v v0 (^ v0 v1)) (^ (v v0 v1) v0))))
(326 (paramod 312 (1 1) 301 (1 2)) ((= (v (^ v0 v1) v0) (^ v0 (v v0 v1)))))
(327 (instantiate 2 ((v0 . v66)(v1 . v65))) ((= (^ v66 v65) (^ v65 v66))))
(328 (instantiate 134 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (v (^ v64 (v (^ v65 v64) v66)) (^ v66 v65)) (^ (v (^ (v v65 v64) v66) v64) (v v66 v65)))))
(329 (paramod 327 (1 1) 328 (1 1 2)) ((= (v (^ v64 (v (^ v65 v64) v66)) (^ v65 v66)) (^ (v (^ (v v65 v64) v66) v64) (v v66 v65)))))
(330 (instantiate 329 ((v64 . v0)(v65 . v1)(v66 . v2))) ((= (v (^ v0 (v (^ v1 v0) v2)) (^ v1 v2)) (^ (v (^ (v v1 v0) v2) v0) (v v2 v1)))))
(331 (instantiate 17 ((v0 . v64)(v1 . v65)(v2 . (v v66 v67)))) ((= (^ v64 (^ v65 (v v66 v67))) (^ v65 (^ v64 (v v66 v67))))))
(332 (instantiate 140 ((v0 . v64)(v1 . v65)(v2 . v66)(v3 . v67))) ((= (v (^ v64 (^ v65 (v v66 v67))) (^ v64 (^ v65 v67))) (^ v64 (^ v65 (v v66 v67))))))
(333 (paramod 331 (1 1) 332 (1 1 1)) ((= (v (^ v65 (^ v64 (v v66 v67))) (^ v64 (^ v65 v67))) (^ v64 (^ v65 (v v66 v67))))))
(334 (instantiate 333 ((v64 . v1)(v65 . v0)(v66 . v2)(v67 . v3))) ((= (v (^ v0 (^ v1 (v v2 v3))) (^ v1 (^ v0 v3))) (^ v1 (^ v0 (v v2 v3))))))
(335 (instantiate 5 ((v0 . v65)(v1 . v66))) ((= (v v65 v66) (v v66 v65))))
(336 (instantiate 146 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (v (^ v64 (v v65 v66)) (^ v64 (^ (v v65 v66) v65))) (^ v64 (v v65 v66)))))
(337 (paramod 335 (1 1) 336 (1 1 2 2 1)) ((= (v (^ v64 (v v65 v66)) (^ v64 (^ (v v66 v65) v65))) (^ v64 (v v65 v66)))))
(338 (instantiate 337 ((v64 . v0)(v65 . v1)(v66 . v2))) ((= (v (^ v0 (v v1 v2)) (^ v0 (^ (v v2 v1) v1))) (^ v0 (v v1 v2)))))
(339 (instantiate 2 ((v0 . v66)(v1 . v65))) ((= (^ v66 v65) (^ v65 v66))))
(340 (instantiate 152 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (v (^ (v v64 v65) v66) (^ v66 v65)) (^ v66 (v v64 v65)))))
(341 (paramod 339 (1 1) 340 (1 1 2)) ((= (v (^ (v v64 v65) v66) (^ v65 v66)) (^ v66 (v v64 v65)))))
(342 (instantiate 341 ((v64 . v0)(v65 . v1)(v66 . v2))) ((= (v (^ (v v0 v1) v2) (^ v1 v2)) (^ v2 (v v0 v1)))))
(343 (instantiate 1 ((v0 . v65))) ((= (^ v65 v65) v65)))
(344 (instantiate 152 ((v0 . v64)(v1 . v65)(v2 . v65))) ((= (v (^ (v v64 v65) v65) (^ v65 v65)) (^ v65 (v v64 v65)))))
(345 (paramod 343 (1 1) 344 (1 1 2)) ((= (v (^ (v v64 v65) v65) v65) (^ v65 (v v64 v65)))))
(346 (instantiate 345 ((v64 . v0)(v65 . v1))) ((= (v (^ (v v0 v1) v1) v1) (^ v1 (v v0 v1)))))
(347 (instantiate 5 ((v0 . (^ (v v64 v65) v66))(v1 . (^ v66 v65)))) ((= (v (^ (v v64 v65) v66) (^ v66 v65)) (v (^ v66 v65) (^ (v v64 v65) v66)))))
(348 (instantiate 152 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (v (^ (v v64 v65) v66) (^ v66 v65)) (^ v66 (v v64 v65)))))
(349 (paramod 347 (1 1) 348 (1 1)) ((= (v (^ v66 v65) (^ (v v64 v65) v66)) (^ v66 (v v64 v65)))))
(350 (instantiate 349 ((v64 . v2)(v65 . v1)(v66 . v0))) ((= (v (^ v0 v1) (^ (v v2 v1) v0)) (^ v0 (v v2 v1)))))
(351 (instantiate 65 ((v0 . v64)(v1 . (^ v0 v1))(v2 . (^ v1 v0)))) ((= (v v64 (v (^ v0 v1) (^ v1 v0))) (v (^ v1 v0) (v (^ v0 v1) v64)))))
(352 (paramod 158 (1 1) 351 (1 1 2)) ((= (v v64 (^ v1 v0)) (v (^ v1 v0) (v (^ v0 v1) v64)))))
(353 (instantiate 352 ((v0 . v2)(v64 . v0))) ((= (v v0 (^ v1 v2)) (v (^ v1 v2) (v (^ v2 v1) v0)))))
(354 (instantiate 42 ((v0 . v64)(v1 . (^ v0 v1))(v2 . (^ v1 v0)))) ((= (v v64 (v (^ v0 v1) (^ v1 v0))) (v (^ v0 v1) (v v64 (^ v1 v0))))))
(355 (paramod 158 (1 1) 354 (1 1 2)) ((= (v v64 (^ v1 v0)) (v (^ v0 v1) (v v64 (^ v1 v0))))))
(356 (flip 355 (1)) ((= (v (^ v0 v1) (v v64 (^ v1 v0))) (v v64 (^ v1 v0)))))
(357 (instantiate 356 ((v64 . v2))) ((= (v (^ v0 v1) (v v2 (^ v1 v0))) (v v2 (^ v1 v0)))))
(358 (instantiate 6 ((v0 . (^ v0 v1))(v1 . (^ v1 v0))(v2 . v66))) ((= (v (v (^ v0 v1) (^ v1 v0)) v66) (v (^ v0 v1) (v (^ v1 v0) v66)))))
(359 (paramod 158 (1 1) 358 (1 1 1)) ((= (v (^ v1 v0) v66) (v (^ v0 v1) (v (^ v1 v0) v66)))))
(360 (flip 359 (1)) ((= (v (^ v0 v1) (v (^ v1 v0) v66)) (v (^ v1 v0) v66))))
(361 (instantiate 360 ((v66 . v2))) ((= (v (^ v0 v1) (v (^ v1 v0) v2)) (v (^ v1 v0) v2))))
(362 (instantiate 361 ((v0 . v1)(v1 . v2)(v2 . v0))) ((= (v (^ v1 v2) (v (^ v2 v1) v0)) (v (^ v2 v1) v0))))
(363 (paramod 362 (1 1) 353 (1 2)) ((= (v v0 (^ v1 v2)) (v (^ v2 v1) v0))))
(364 (instantiate 2 ((v0 . v64)(v1 . v65))) ((= (^ v64 v65) (^ v65 v64))))
(365 (instantiate 162 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (v (^ (v (^ v64 v65) v66) v65) (^ v64 v65)) (^ v65 (v (^ v64 v65) v66)))))
(366 (paramod 364 (1 1) 365 (1 1 2)) ((= (v (^ (v (^ v64 v65) v66) v65) (^ v65 v64)) (^ v65 (v (^ v64 v65) v66)))))
(367 (instantiate 366 ((v64 . v0)(v65 . v1)(v66 . v2))) ((= (v (^ (v (^ v0 v1) v2) v1) (^ v1 v0)) (^ v1 (v (^ v0 v1) v2)))))
(368 (instantiate 5 ((v0 . (^ (v v64 v65) v66))(v1 . (^ v64 v66)))) ((= (v (^ (v v64 v65) v66) (^ v64 v66)) (v (^ v64 v66) (^ (v v64 v65) v66)))))
(369 (instantiate 166 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (v (^ (v v64 v65) v66) (^ v64 v66)) (^ v66 (v v64 v65)))))
(370 (paramod 368 (1 1) 369 (1 1)) ((= (v (^ v64 v66) (^ (v v64 v65) v66)) (^ v66 (v v64 v65)))))
(371 (instantiate 370 ((v64 . v0)(v65 . v2)(v66 . v1))) ((= (v (^ v0 v1) (^ (v v0 v2) v1)) (^ v1 (v v0 v2)))))
(372 (instantiate 27 ((v0 . (v v1 v0))(v1 . v65)(v2 . (v v0 v1)))) ((= (^ v65 (^ (v v0 v1) (v v1 v0))) (^ (v v1 v0) (^ v65 (v v0 v1))))))
(373 (paramod 184 (1 1) 372 (1 1 2)) ((= (^ v65 (v v0 v1)) (^ (v v1 v0) (^ v65 (v v0 v1))))))
(374 (flip 373 (1)) ((= (^ (v v1 v0) (^ v65 (v v0 v1))) (^ v65 (v v0 v1)))))
(375 (instantiate 374 ((v0 . v1)(v1 . v0)(v65 . v2))) ((= (^ (v v0 v1) (^ v2 (v v1 v0))) (^ v2 (v v1 v0)))))
(376 (instantiate 184 ((v0 . v65)(v1 . v66))) ((= (^ (v v65 v66) (v v66 v65)) (v v65 v66))))
(377 (instantiate 188 ((v0 . (v v66 v65))(v1 . v65)(v2 . v66))) ((= (v (^ (v v66 v65) v65) (^ (v v65 v66) (v v66 v65))) (^ (v v66 v65) (v v65 v66)))))
(378 (paramod 376 (1 1) 377 (1 1 2)) ((= (v (^ (v v66 v65) v65) (v v65 v66)) (^ (v v66 v65) (v v65 v66)))))
(379 (instantiate 184 ((v0 . v66)(v1 . v65))) ((= (^ (v v66 v65) (v v65 v66)) (v v66 v65))))
(380 (paramod 379 (1 1) 378 (1 2)) ((= (v (^ (v v66 v65) v65) (v v65 v66)) (v v66 v65))))
(381 (instantiate 380 ((v65 . v1)(v66 . v0))) ((= (v (^ (v v0 v1) v1) (v v1 v0)) (v v0 v1))))
(382 (instantiate 198 ((v0 . v67)(v1 . v64))) ((= (v v67 (v v64 (^ (v v64 v67) v67))) (v v64 v67))))
(383 (instantiate 72 ((v0 . v64)(v1 . v65)(v2 . (^ (v v64 v67) v67))(v3 . v67))) ((= (v v65 (v v67 (v v64 (^ (v v64 v67) v67)))) (v v64 (v v65 (v (^ (v v64 v67) v67) v67))))))
(384 (paramod 382 (1 1) 383 (1 1 2)) ((= (v v65 (v v64 v67)) (v v64 (v v65 (v (^ (v v64 v67) v67) v67))))))
(385 (instantiate 346 ((v0 . v64)(v1 . v67))) ((= (v (^ (v v64 v67) v67) v67) (^ v67 (v v64 v67)))))
(386 (paramod 385 (1 1) 384 (1 2 2 2)) ((= (v v65 (v v64 v67)) (v v64 (v v65 (^ v67 (v v64 v67)))))))
(387 (flip 386 (1)) ((= (v v64 (v v65 (^ v67 (v v64 v67)))) (v v65 (v v64 v67)))))
(388 (instantiate 387 ((v64 . v0)(v65 . v1)(v67 . v2))) ((= (v v0 (v v1 (^ v2 (v v0 v2)))) (v v1 (v v0 v2)))))
(389 (instantiate 134 ((v0 . v64)(v1 . v65)(v2 . v64))) ((= (v (^ v64 (v (^ v65 v64) v64)) (^ v64 v65)) (^ (v (^ (v v65 v64) v64) v64) (v v64 v65)))))
(390 (instantiate 213 ((v0 . v64)(v1 . v65)(v2 . v64))) ((= (v (^ v64 (v (^ v65 v64) v64)) (^ v64 v65)) (^ v64 (v (^ v65 v64) v64)))))
(391 (paramod 389 (1 1) 390 (1 1)) ((= (^ (v (^ (v v65 v64) v64) v64) (v v64 v65)) (^ v64 (v (^ v65 v64) v64)))))
(392 (instantiate 346 ((v0 . v65)(v1 . v64))) ((= (v (^ (v v65 v64) v64) v64) (^ v64 (v v65 v64)))))
(393 (paramod 392 (1 1) 391 (1 1 1)) ((= (^ (^ v64 (v v65 v64)) (v v64 v65)) (^ v64 (v (^ v65 v64) v64)))))
(394 (instantiate 3 ((v0 . v64)(v1 . (v v65 v64))(v2 . (v v64 v65)))) ((= (^ (^ v64 (v v65 v64)) (v v64 v65)) (^ v64 (^ (v v65 v64) (v v64 v65))))))
(395 (paramod 394 (1 1) 393 (1 1)) ((= (^ v64 (^ (v v65 v64) (v v64 v65))) (^ v64 (v (^ v65 v64) v64)))))
(396 (instantiate 184 ((v0 . v65)(v1 . v64))) ((= (^ (v v65 v64) (v v64 v65)) (v v65 v64))))
(397 (paramod 396 (1 1) 395 (1 1 2)) ((= (^ v64 (v v65 v64)) (^ v64 (v (^ v65 v64) v64)))))
(398 (flip 397 (1)) ((= (^ v64 (v (^ v65 v64) v64)) (^ v64 (v v65 v64)))))
(399 (instantiate 398 ((v64 . v0)(v65 . v1))) ((= (^ v0 (v (^ v1 v0) v0)) (^ v0 (v v1 v0)))))
(400 (instantiate 221 ((v1 . v65))) ((= (v (^ v0 v65) (^ v65 (v v0 v2))) (^ v65 (v v0 v2)))))
(401 (instantiate 124 ((v0 . (^ v0 v65))(v1 . v65)(v2 . (v v0 v2)))) ((= (^ (v (^ v0 v65) v65) (v (^ v0 v65) (^ v65 (v v0 v2)))) (v (^ v0 v65) (^ v65 (v v0 v2))))))
(402 (paramod 400 (1 1) 401 (1 1 2)) ((= (^ (v (^ v0 v65) v65) (^ v65 (v v0 v2))) (v (^ v0 v65) (^ v65 (v v0 v2))))))
(403 (instantiate 221 ((v0 . v0)(v1 . v65)(v2 . v2))) ((= (v (^ v0 v65) (^ v65 (v v0 v2))) (^ v65 (v v0 v2)))))
(404 (paramod 403 (1 1) 402 (1 2)) ((= (^ (v (^ v0 v65) v65) (^ v65 (v v0 v2))) (^ v65 (v v0 v2)))))
(405 (instantiate 404 ((v65 . v1))) ((= (^ (v (^ v0 v1) v1) (^ v1 (v v0 v2))) (^ v1 (v v0 v2)))))
(406 (instantiate 221 ((v1 . v65))) ((= (v (^ v0 v65) (^ v65 (v v0 v2))) (^ v65 (v v0 v2)))))
(407 (instantiate 8 ((v0 . (^ v0 v65))(v1 . v65)(v2 . (v v0 v2)))) ((= (^ (v (^ v0 v65) (^ v65 (v v0 v2))) (v (^ v0 v65) v65)) (v (^ v0 v65) (^ v65 (v v0 v2))))))
(408 (paramod 406 (1 1) 407 (1 1 1)) ((= (^ (^ v65 (v v0 v2)) (v (^ v0 v65) v65)) (v (^ v0 v65) (^ v65 (v v0 v2))))))
(409 (instantiate 3 ((v0 . v65)(v1 . (v v0 v2))(v2 . (v (^ v0 v65) v65)))) ((= (^ (^ v65 (v v0 v2)) (v (^ v0 v65) v65)) (^ v65 (^ (v v0 v2) (v (^ v0 v65) v65))))))
(410 (paramod 409 (1 1) 408 (1 1)) ((= (^ v65 (^ (v v0 v2) (v (^ v0 v65) v65))) (v (^ v0 v65) (^ v65 (v v0 v2))))))
(411 (instantiate 221 ((v0 . v0)(v1 . v65)(v2 . v2))) ((= (v (^ v0 v65) (^ v65 (v v0 v2))) (^ v65 (v v0 v2)))))
(412 (paramod 411 (1 1) 410 (1 2)) ((= (^ v65 (^ (v v0 v2) (v (^ v0 v65) v65))) (^ v65 (v v0 v2)))))
(413 (instantiate 412 ((v0 . v1)(v65 . v0))) ((= (^ v0 (^ (v v1 v2) (v (^ v1 v0) v0))) (^ v0 (v v1 v2)))))
(414 (instantiate 237 ((v1 . v66)(v2 . v65))) ((= (^ (v (^ v0 v66) v65) (v v65 v66)) (v v65 (^ v0 v66)))))
(415 (instantiate 108 ((v0 . (v (^ v0 v66) v65))(v1 . v65)(v2 . v66))) ((= (v (^ (v (^ v0 v66) v65) v65) (^ (v (^ v0 v66) v65) (v v65 v66))) (^ (v (^ v0 v66) v65) (v v65 v66)))))
(416 (paramod 414 (1 1) 415 (1 1 2)) ((= (v (^ (v (^ v0 v66) v65) v65) (v v65 (^ v0 v66))) (^ (v (^ v0 v66) v65) (v v65 v66)))))
(417 (instantiate 381 ((v0 . (^ v0 v66))(v1 . v65))) ((= (v (^ (v (^ v0 v66) v65) v65) (v v65 (^ v0 v66))) (v (^ v0 v66) v65))))
(418 (paramod 417 (1 1) 416 (1 1)) ((= (v (^ v0 v66) v65) (^ (v (^ v0 v66) v65) (v v65 v66)))))
(419 (flip 418 (1)) ((= (^ (v (^ v0 v66) v65) (v v65 v66)) (v (^ v0 v66) v65))))
(420 (instantiate 419 ((v65 . v2)(v66 . v1))) ((= (^ (v (^ v0 v1) v2) (v v2 v1)) (v (^ v0 v1) v2))))
(421 (instantiate 221 ((v0 . v64)(v1 . v65))) ((= (v (^ v64 v65) (^ v65 (v v64 v2))) (^ v65 (v v64 v2)))))
(422 (instantiate 241 ((v0 . v64)(v1 . v65)(v2 . (^ v65 (v v64 v2))))) ((= (^ (v (^ v64 v65) (^ v65 (v v64 v2))) (v v64 (^ v65 (v v64 v2)))) (v (^ v65 (v v64 v2)) (^ v64 v65)))))
(423 (paramod 421 (1 1) 422 (1 1 1)) ((= (^ (^ v65 (v v64 v2)) (v v64 (^ v65 (v v64 v2)))) (v (^ v65 (v v64 v2)) (^ v64 v65)))))
(424 (instantiate 3 ((v0 . v65)(v1 . (v v64 v2))(v2 . (v v64 (^ v65 (v v64 v2)))))) ((= (^ (^ v65 (v v64 v2)) (v v64 (^ v65 (v v64 v2)))) (^ v65 (^ (v v64 v2) (v v64 (^ v65 (v v64 v2))))))))
(425 (paramod 424 (1 1) 423 (1 1)) ((= (^ v65 (^ (v v64 v2) (v v64 (^ v65 (v v64 v2))))) (v (^ v65 (v v64 v2)) (^ v64 v65)))))
(426 (instantiate 104 ((v0 . v65)(v1 . v64)(v2 . v2))) ((= (v (^ v65 (v v64 v2)) (^ v64 v65)) (^ v65 (v v64 v2)))))
(427 (paramod 426 (1 1) 425 (1 2)) ((= (^ v65 (^ (v v64 v2) (v v64 (^ v65 (v v64 v2))))) (^ v65 (v v64 v2)))))
(428 (instantiate 427 ((v64 . v1)(v65 . v0))) ((= (^ v0 (^ (v v1 v2) (v v1 (^ v0 (v v1 v2))))) (^ v0 (v v1 v2)))))
(429 (instantiate 152 ((v2 . v65))) ((= (v (^ (v v0 v1) v65) (^ v65 v1)) (^ v65 (v v0 v1)))))
(430 (instantiate 241 ((v0 . (v v0 v1))(v1 . v65)(v2 . (^ v65 v1)))) ((= (^ (v (^ (v v0 v1) v65) (^ v65 v1)) (v (v v0 v1) (^ v65 v1))) (v (^ v65 v1) (^ (v v0 v1) v65)))))
(431 (paramod 429 (1 1) 430 (1 1 1)) ((= (^ (^ v65 (v v0 v1)) (v (v v0 v1) (^ v65 v1))) (v (^ v65 v1) (^ (v v0 v1) v65)))))
(432 (instantiate 6 ((v0 . v0)(v1 . v1)(v2 . (^ v65 v1)))) ((= (v (v v0 v1) (^ v65 v1)) (v v0 (v v1 (^ v65 v1))))))
(433 (paramod 432 (1 1) 431 (1 1 2)) ((= (^ (^ v65 (v v0 v1)) (v v0 (v v1 (^ v65 v1)))) (v (^ v65 v1) (^ (v v0 v1) v65)))))
(434 (instantiate 312 ((v0 . v1)(v1 . v65))) ((= (v v1 (^ v65 v1)) (^ v1 (v v1 v65)))))
(435 (paramod 434 (1 1) 433 (1 1 2 2)) ((= (^ (^ v65 (v v0 v1)) (v v0 (^ v1 (v v1 v65)))) (v (^ v65 v1) (^ (v v0 v1) v65)))))
(436 (instantiate 3 ((v0 . v65)(v1 . (v v0 v1))(v2 . (v v0 (^ v1 (v v1 v65)))))) ((= (^ (^ v65 (v v0 v1)) (v v0 (^ v1 (v v1 v65)))) (^ v65 (^ (v v0 v1) (v v0 (^ v1 (v v1 v65))))))))
(437 (paramod 436 (1 1) 435 (1 1)) ((= (^ v65 (^ (v v0 v1) (v v0 (^ v1 (v v1 v65))))) (v (^ v65 v1) (^ (v v0 v1) v65)))))
(438 (instantiate 124 ((v0 . v0)(v1 . v1)(v2 . (v v1 v65)))) ((= (^ (v v0 v1) (v v0 (^ v1 (v v1 v65)))) (v v0 (^ v1 (v v1 v65))))))
(439 (paramod 438 (1 1) 437 (1 1 2)) ((= (^ v65 (v v0 (^ v1 (v v1 v65)))) (v (^ v65 v1) (^ (v v0 v1) v65)))))
(440 (instantiate 350 ((v0 . v65)(v1 . v1)(v2 . v0))) ((= (v (^ v65 v1) (^ (v v0 v1) v65)) (^ v65 (v v0 v1)))))
(441 (paramod 440 (1 1) 439 (1 2)) ((= (^ v65 (v v0 (^ v1 (v v1 v65)))) (^ v65 (v v0 v1)))))
(442 (instantiate 441 ((v0 . v1)(v1 . v2)(v65 . v0))) ((= (^ v0 (v v1 (^ v2 (v v2 v0)))) (^ v0 (v v1 v2)))))
(443 (instantiate 241 ((v0 . v66)(v2 . v65))) ((= (^ (v (^ v66 v1) v65) (v v66 v65)) (v v65 (^ v66 v1)))))
(444 (instantiate 227 ((v0 . (v (^ v66 v1) v65))(v1 . v65)(v2 . v66))) ((= (v (^ (v (^ v66 v1) v65) v65) (^ (v (^ v66 v1) v65) (v v66 v65))) (^ (v (^ v66 v1) v65) (v v66 v65)))))
(445 (paramod 443 (1 1) 444 (1 1 2)) ((= (v (^ (v (^ v66 v1) v65) v65) (v v65 (^ v66 v1))) (^ (v (^ v66 v1) v65) (v v66 v65)))))
(446 (instantiate 381 ((v0 . (^ v66 v1))(v1 . v65))) ((= (v (^ (v (^ v66 v1) v65) v65) (v v65 (^ v66 v1))) (v (^ v66 v1) v65))))
(447 (paramod 446 (1 1) 445 (1 1)) ((= (v (^ v66 v1) v65) (^ (v (^ v66 v1) v65) (v v66 v65)))))
(448 (flip 447 (1)) ((= (^ (v (^ v66 v1) v65) (v v66 v65)) (v (^ v66 v1) v65))))
(449 (instantiate 448 ((v65 . v2)(v66 . v0))) ((= (^ (v (^ v0 v1) v2) (v v0 v2)) (v (^ v0 v1) v2))))
(450 (instantiate 217 ((v1 . v65)(v2 . v65))) ((= (v (^ v0 v65) (^ v65 (v (^ v0 v65) v65))) (^ v65 (v (^ v0 v65) v65)))))
(451 (instantiate 259 ((v0 . (^ v0 v65))(v1 . v65))) ((= (v (^ v0 v65) (^ v65 (v (^ v0 v65) v65))) (v (^ v0 v65) v65))))
(452 (paramod 450 (1 1) 451 (1 1)) ((= (^ v65 (v (^ v0 v65) v65)) (v (^ v0 v65) v65))))
(453 (instantiate 399 ((v0 . v65)(v1 . v0))) ((= (^ v65 (v (^ v0 v65) v65)) (^ v65 (v v0 v65)))))
(454 (paramod 453 (1 1) 452 (1 1)) ((= (^ v65 (v v0 v65)) (v (^ v0 v65) v65))))
(455 (flip 454 (1)) ((= (v (^ v0 v65) v65) (^ v65 (v v0 v65)))))
(456 (instantiate 455 ((v65 . v1))) ((= (v (^ v0 v1) v1) (^ v1 (v v0 v1)))))
(457 (instantiate 456 ((v0 . v1)(v1 . v0))) ((= (v (^ v1 v0) v0) (^ v0 (v v1 v0)))))
(458 (paramod 457 (1 1) 413 (1 1 2 2)) ((= (^ v0 (^ (v v1 v2) (^ v0 (v v1 v0)))) (^ v0 (v v1 v2)))))
(459 (instantiate 36 ((v0 . v0)(v1 . (v v1 v2))(v2 . (v v1 v0)))) ((= (^ v0 (^ (v v1 v2) (^ v0 (v v1 v0)))) (^ v0 (^ (v v1 v2) (v v1 v0))))))
(460 (paramod 459 (1 1) 458 (1 1)) ((= (^ v0 (^ (v v1 v2) (v v1 v0))) (^ v0 (v v1 v2)))))
(461 (paramod 456 (1 1) 405 (1 1 1)) ((= (^ (^ v1 (v v0 v1)) (^ v1 (v v0 v2))) (^ v1 (v v0 v2)))))
(462 (instantiate 3 ((v0 . v1)(v1 . (v v0 v1))(v2 . (^ v1 (v v0 v2))))) ((= (^ (^ v1 (v v0 v1)) (^ v1 (v v0 v2))) (^ v1 (^ (v v0 v1) (^ v1 (v v0 v2)))))))
(463 (paramod 462 (1 1) 461 (1 1)) ((= (^ v1 (^ (v v0 v1) (^ v1 (v v0 v2)))) (^ v1 (v v0 v2)))))
(464 (instantiate 36 ((v0 . v1)(v1 . (v v0 v1))(v2 . (v v0 v2)))) ((= (^ v1 (^ (v v0 v1) (^ v1 (v v0 v2)))) (^ v1 (^ (v v0 v1) (v v0 v2))))))
(465 (paramod 464 (1 1) 463 (1 1)) ((= (^ v1 (^ (v v0 v1) (v v0 v2))) (^ v1 (v v0 v2)))))
(466 (instantiate 465 ((v0 . v1)(v1 . v0))) ((= (^ v0 (^ (v v1 v0) (v v1 v2))) (^ v0 (v v1 v2)))))
(467 (instantiate 217 ((v1 . v64))) ((= (v (^ v0 v64) (^ v64 (v (^ v0 v64) v2))) (^ v64 (v (^ v0 v64) v2)))))
(468 (instantiate 272 ((v0 . v64)(v1 . (^ v0 v64))(v2 . (v (^ v0 v64) v2)))) ((= (^ (v v64 (^ v0 v64)) (v (^ v0 v64) (^ v64 (v (^ v0 v64) v2)))) (v (^ v0 v64) (^ v64 (v (^ v0 v64) v2))))))
(469 (paramod 467 (1 1) 468 (1 1 2)) ((= (^ (v v64 (^ v0 v64)) (^ v64 (v (^ v0 v64) v2))) (v (^ v0 v64) (^ v64 (v (^ v0 v64) v2))))))
(470 (instantiate 312 ((v0 . v64)(v1 . v0))) ((= (v v64 (^ v0 v64)) (^ v64 (v v64 v0)))))
(471 (paramod 470 (1 1) 469 (1 1 1)) ((= (^ (^ v64 (v v64 v0)) (^ v64 (v (^ v0 v64) v2))) (v (^ v0 v64) (^ v64 (v (^ v0 v64) v2))))))
(472 (instantiate 3 ((v0 . v64)(v1 . (v v64 v0))(v2 . (^ v64 (v (^ v0 v64) v2))))) ((= (^ (^ v64 (v v64 v0)) (^ v64 (v (^ v0 v64) v2))) (^ v64 (^ (v v64 v0) (^ v64 (v (^ v0 v64) v2)))))))
(473 (paramod 472 (1 1) 471 (1 1)) ((= (^ v64 (^ (v v64 v0) (^ v64 (v (^ v0 v64) v2)))) (v (^ v0 v64) (^ v64 (v (^ v0 v64) v2))))))
(474 (instantiate 36 ((v0 . v64)(v1 . (v v64 v0))(v2 . (v (^ v0 v64) v2)))) ((= (^ v64 (^ (v v64 v0) (^ v64 (v (^ v0 v64) v2)))) (^ v64 (^ (v v64 v0) (v (^ v0 v64) v2))))))
(475 (paramod 474 (1 1) 473 (1 1)) ((= (^ v64 (^ (v v64 v0) (v (^ v0 v64) v2))) (v (^ v0 v64) (^ v64 (v (^ v0 v64) v2))))))
(476 (instantiate 217 ((v0 . v0)(v1 . v64)(v2 . v2))) ((= (v (^ v0 v64) (^ v64 (v (^ v0 v64) v2))) (^ v64 (v (^ v0 v64) v2)))))
(477 (paramod 476 (1 1) 475 (1 2)) ((= (^ v64 (^ (v v64 v0) (v (^ v0 v64) v2))) (^ v64 (v (^ v0 v64) v2)))))
(478 (instantiate 477 ((v0 . v1)(v64 . v0))) ((= (^ v0 (^ (v v0 v1) (v (^ v1 v0) v2))) (^ v0 (v (^ v1 v0) v2)))))
(479 (instantiate 57 ((v0 . v64))) ((= (v v64 (v v1 v64)) (v v1 v64))))
(480 (instantiate 278 ((v0 . v64)(v1 . (v v1 v64))(v2 . v66))) ((= (^ (v v64 (v v1 v64)) (v v64 (^ v66 (v v1 v64)))) (v v64 (^ v66 (v v1 v64))))))
(481 (paramod 479 (1 1) 480 (1 1 1)) ((= (^ (v v1 v64) (v v64 (^ v66 (v v1 v64)))) (v v64 (^ v66 (v v1 v64))))))
(482 (instantiate 481 ((v1 . v0)(v64 . v1)(v66 . v2))) ((= (^ (v v0 v1) (v v1 (^ v2 (v v0 v1)))) (v v1 (^ v2 (v v0 v1))))))
(483 (instantiate 47 ((v0 . v64))) ((= (v v64 (v v64 v1)) (v v64 v1))))
(484 (instantiate 278 ((v0 . v64)(v1 . (v v64 v1))(v2 . v66))) ((= (^ (v v64 (v v64 v1)) (v v64 (^ v66 (v v64 v1)))) (v v64 (^ v66 (v v64 v1))))))
(485 (paramod 483 (1 1) 484 (1 1 1)) ((= (^ (v v64 v1) (v v64 (^ v66 (v v64 v1)))) (v v64 (^ v66 (v v64 v1))))))
(486 (instantiate 485 ((v64 . v0)(v66 . v2))) ((= (^ (v v0 v1) (v v0 (^ v2 (v v0 v1)))) (v v0 (^ v2 (v v0 v1))))))
(487 (instantiate 486 ((v0 . v1)(v1 . v2)(v2 . v0))) ((= (^ (v v1 v2) (v v1 (^ v0 (v v1 v2)))) (v v1 (^ v0 (v v1 v2))))))
(488 (paramod 487 (1 1) 428 (1 1 2)) ((= (^ v0 (v v1 (^ v0 (v v1 v2)))) (^ v0 (v v1 v2)))))
(489 (instantiate 312 ((v0 . v64))) ((= (v v64 (^ v1 v64)) (^ v64 (v v64 v1)))))
(490 (instantiate 272 ((v0 . v64)(v1 . (^ v1 v64))(v2 . v66))) ((= (^ (v v64 (^ v1 v64)) (v (^ v1 v64) (^ v64 v66))) (v (^ v1 v64) (^ v64 v66)))))
(491 (paramod 489 (1 1) 490 (1 1 1)) ((= (^ (^ v64 (v v64 v1)) (v (^ v1 v64) (^ v64 v66))) (v (^ v1 v64) (^ v64 v66)))))
(492 (instantiate 3 ((v0 . v64)(v1 . (v v64 v1))(v2 . (v (^ v1 v64) (^ v64 v66))))) ((= (^ (^ v64 (v v64 v1)) (v (^ v1 v64) (^ v64 v66))) (^ v64 (^ (v v64 v1) (v (^ v1 v64) (^ v64 v66)))))))
(493 (paramod 492 (1 1) 491 (1 1)) ((= (^ v64 (^ (v v64 v1) (v (^ v1 v64) (^ v64 v66)))) (v (^ v1 v64) (^ v64 v66)))))
(494 (instantiate 478 ((v0 . v64)(v1 . v1)(v2 . (^ v64 v66)))) ((= (^ v64 (^ (v v64 v1) (v (^ v1 v64) (^ v64 v66)))) (^ v64 (v (^ v1 v64) (^ v64 v66))))))
(495 (paramod 494 (1 1) 493 (1 1)) ((= (^ v64 (v (^ v1 v64) (^ v64 v66))) (v (^ v1 v64) (^ v64 v66)))))
(496 (instantiate 495 ((v64 . v0)(v66 . v2))) ((= (^ v0 (v (^ v1 v0) (^ v0 v2))) (v (^ v1 v0) (^ v0 v2)))))
(497 (instantiate 209 ((v0 . v65))) ((= (v v65 (v v1 (^ v2 (v v2 v65)))) (v v1 (v v2 v65)))))
(498 (instantiate 318 ((v0 . v64)(v1 . v65)(v2 . (v v1 (^ v2 (v v2 v65)))))) ((= (^ v64 (^ (v v64 v65) (v v65 (v v1 (^ v2 (v v2 v65)))))) (^ v64 (v v65 (v v1 (^ v2 (v v2 v65))))))))
(499 (paramod 497 (1 1) 498 (1 1 2 2)) ((= (^ v64 (^ (v v64 v65) (v v1 (v v2 v65)))) (^ v64 (v v65 (v v1 (^ v2 (v v2 v65))))))))
(500 (instantiate 209 ((v0 . v65)(v1 . v1)(v2 . v2))) ((= (v v65 (v v1 (^ v2 (v v2 v65)))) (v v1 (v v2 v65)))))
(501 (paramod 500 (1 1) 499 (1 2 2)) ((= (^ v64 (^ (v v64 v65) (v v1 (v v2 v65)))) (^ v64 (v v1 (v v2 v65))))))
(502 (instantiate 501 ((v1 . v2)(v2 . v3)(v64 . v0)(v65 . v1))) ((= (^ v0 (^ (v v0 v1) (v v2 (v v3 v1)))) (^ v0 (v v2 (v v3 v1))))))
(503 (instantiate 5 ((v0 . (^ v64 (v (^ v65 v64) v66)))(v1 . (^ v65 v66)))) ((= (v (^ v64 (v (^ v65 v64) v66)) (^ v65 v66)) (v (^ v65 v66) (^ v64 (v (^ v65 v64) v66))))))
(504 (instantiate 330 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (v (^ v64 (v (^ v65 v64) v66)) (^ v65 v66)) (^ (v (^ (v v65 v64) v66) v64) (v v66 v65)))))
(505 (paramod 503 (1 1) 504 (1 1)) ((= (v (^ v65 v66) (^ v64 (v (^ v65 v64) v66))) (^ (v (^ (v v65 v64) v66) v64) (v v66 v65)))))
(506 (flip 505 (1)) ((= (^ (v (^ (v v65 v64) v66) v64) (v v66 v65)) (v (^ v65 v66) (^ v64 (v (^ v65 v64) v66))))))
(507 (instantiate 506 ((v64 . v1)(v65 . v0)(v66 . v2))) ((= (^ (v (^ (v v0 v1) v2) v1) (v v2 v0)) (v (^ v0 v2) (^ v1 (v (^ v0 v1) v2))))))
(508 (instantiate 268 ((v0 . v66)(v2 . v65))) ((= (^ (v (^ v66 v1) v65) (v v65 v66)) (v (^ v66 v1) v65))))
(509 (instantiate 338 ((v0 . (v (^ v66 v1) v65))(v1 . v65)(v2 . v66))) ((= (v (^ (v (^ v66 v1) v65) (v v65 v66)) (^ (v (^ v66 v1) v65) (^ (v v66 v65) v65))) (^ (v (^ v66 v1) v65) (v v65 v66)))))
(510 (paramod 508 (1 1) 509 (1 1 1)) ((= (v (v (^ v66 v1) v65) (^ (v (^ v66 v1) v65) (^ (v v66 v65) v65))) (^ (v (^ v66 v1) v65) (v v65 v66)))))
(511 (instantiate 325 ((v0 . (v (^ v66 v1) v65))(v1 . (^ (v v66 v65) v65)))) ((= (v (v (^ v66 v1) v65) (^ (v (^ v66 v1) v65) (^ (v v66 v65) v65))) (^ (v (v (^ v66 v1) v65) (^ (v v66 v65) v65)) (v (^ v66 v1) v65)))))
(512 (paramod 511 (1 1) 510 (1 1)) ((= (^ (v (v (^ v66 v1) v65) (^ (v v66 v65) v65)) (v (^ v66 v1) v65)) (^ (v (^ v66 v1) v65) (v v65 v66)))))
(513 (instantiate 6 ((v0 . (^ v66 v1))(v1 . v65)(v2 . (^ (v v66 v65) v65)))) ((= (v (v (^ v66 v1) v65) (^ (v v66 v65) v65)) (v (^ v66 v1) (v v65 (^ (v v66 v65) v65))))))
(514 (paramod 513 (1 1) 512 (1 1 1)) ((= (^ (v (^ v66 v1) (v v65 (^ (v v66 v65) v65))) (v (^ v66 v1) v65)) (^ (v (^ v66 v1) v65) (v v65 v66)))))
(515 (instantiate 312 ((v0 . v65)(v1 . (v v66 v65)))) ((= (v v65 (^ (v v66 v65) v65)) (^ v65 (v v65 (v v66 v65))))))
(516 (paramod 515 (1 1) 514 (1 1 1 2)) ((= (^ (v (^ v66 v1) (^ v65 (v v65 (v v66 v65)))) (v (^ v66 v1) v65)) (^ (v (^ v66 v1) v65) (v v65 v66)))))
(517 (instantiate 57 ((v0 . v65)(v1 . v66))) ((= (v v65 (v v66 v65)) (v v66 v65))))
(518 (paramod 517 (1 1) 516 (1 1 1 2 2)) ((= (^ (v (^ v66 v1) (^ v65 (v v66 v65))) (v (^ v66 v1) v65)) (^ (v (^ v66 v1) v65) (v v65 v66)))))
(519 (instantiate 8 ((v0 . (^ v66 v1))(v1 . v65)(v2 . (v v66 v65)))) ((= (^ (v (^ v66 v1) (^ v65 (v v66 v65))) (v (^ v66 v1) v65)) (v (^ v66 v1) (^ v65 (v v66 v65))))))
(520 (paramod 519 (1 1) 518 (1 1)) ((= (v (^ v66 v1) (^ v65 (v v66 v65))) (^ (v (^ v66 v1) v65) (v v65 v66)))))
(521 (instantiate 268 ((v0 . v66)(v1 . v1)(v2 . v65))) ((= (^ (v (^ v66 v1) v65) (v v65 v66)) (v (^ v66 v1) v65))))
(522 (paramod 521 (1 1) 520 (1 2)) ((= (v (^ v66 v1) (^ v65 (v v66 v65))) (v (^ v66 v1) v65))))
(523 (instantiate 522 ((v65 . v2)(v66 . v0))) ((= (v (^ v0 v1) (^ v2 (v v0 v2))) (v (^ v0 v1) v2))))
(524 (instantiate 363 ((v0 . (^ (A) (B)))(v1 . (A))(v2 . (C)))) ((= (v (^ (A) (B)) (^ (A) (C))) (v (^ (C) (A)) (^ (A) (B))))))
(525 (paramod 524 (1 1) 11 (1 1 1)) ((not (= (v (^ (C) (A)) (^ (A) (B))) (^ (A) (v (B) (C)))))))
(526 (instantiate 375 ((v0 . v64)(v1 . v66))) ((= (^ (v v64 v66) (^ v2 (v v66 v64))) (^ v2 (v v66 v64)))))
(527 (instantiate 371 ((v0 . v64)(v1 . (^ v2 (v v66 v64)))(v2 . v66))) ((= (v (^ v64 (^ v2 (v v66 v64))) (^ (v v64 v66) (^ v2 (v v66 v64)))) (^ (^ v2 (v v66 v64)) (v v64 v66)))))
(528 (paramod 526 (1 1) 527 (1 1 2)) ((= (v (^ v64 (^ v2 (v v66 v64))) (^ v2 (v v66 v64))) (^ (^ v2 (v v66 v64)) (v v64 v66)))))
(529 (instantiate 456 ((v0 . v64)(v1 . (^ v2 (v v66 v64))))) ((= (v (^ v64 (^ v2 (v v66 v64))) (^ v2 (v v66 v64))) (^ (^ v2 (v v66 v64)) (v v64 (^ v2 (v v66 v64)))))))
(530 (paramod 529 (1 1) 528 (1 1)) ((= (^ (^ v2 (v v66 v64)) (v v64 (^ v2 (v v66 v64)))) (^ (^ v2 (v v66 v64)) (v v64 v66)))))
(531 (instantiate 3 ((v0 . v2)(v1 . (v v66 v64))(v2 . (v v64 (^ v2 (v v66 v64)))))) ((= (^ (^ v2 (v v66 v64)) (v v64 (^ v2 (v v66 v64)))) (^ v2 (^ (v v66 v64) (v v64 (^ v2 (v v66 v64))))))))
(532 (paramod 531 (1 1) 530 (1 1)) ((= (^ v2 (^ (v v66 v64) (v v64 (^ v2 (v v66 v64))))) (^ (^ v2 (v v66 v64)) (v v64 v66)))))
(533 (instantiate 482 ((v0 . v66)(v1 . v64)(v2 . v2))) ((= (^ (v v66 v64) (v v64 (^ v2 (v v66 v64)))) (v v64 (^ v2 (v v66 v64))))))
(534 (paramod 533 (1 1) 532 (1 1 2)) ((= (^ v2 (v v64 (^ v2 (v v66 v64)))) (^ (^ v2 (v v66 v64)) (v v64 v66)))))
(535 (instantiate 3 ((v0 . v2)(v1 . (v v66 v64))(v2 . (v v64 v66)))) ((= (^ (^ v2 (v v66 v64)) (v v64 v66)) (^ v2 (^ (v v66 v64) (v v64 v66))))))
(536 (paramod 535 (1 1) 534 (1 2)) ((= (^ v2 (v v64 (^ v2 (v v66 v64)))) (^ v2 (^ (v v66 v64) (v v64 v66))))))
(537 (instantiate 184 ((v0 . v66)(v1 . v64))) ((= (^ (v v66 v64) (v v64 v66)) (v v66 v64))))
(538 (paramod 537 (1 1) 536 (1 2 2)) ((= (^ v2 (v v64 (^ v2 (v v66 v64)))) (^ v2 (v v66 v64)))))
(539 (instantiate 538 ((v2 . v0)(v64 . v1)(v66 . v2))) ((= (^ v0 (v v1 (^ v0 (v v2 v1)))) (^ v0 (v v2 v1)))))
(540 (instantiate 2 ((v0 . (v (^ v64 v65) v66))(v1 . (v v66 v65)))) ((= (^ (v (^ v64 v65) v66) (v v66 v65)) (^ (v v66 v65) (v (^ v64 v65) v66)))))
(541 (instantiate 420 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (^ (v (^ v64 v65) v66) (v v66 v65)) (v (^ v64 v65) v66))))
(542 (paramod 540 (1 1) 541 (1 1)) ((= (^ (v v66 v65) (v (^ v64 v65) v66)) (v (^ v64 v65) v66))))
(543 (instantiate 542 ((v64 . v2)(v65 . v1)(v66 . v0))) ((= (^ (v v0 v1) (v (^ v2 v1) v0)) (v (^ v2 v1) v0))))
(544 (instantiate 420 ((v2 . v65))) ((= (^ (v (^ v0 v1) v65) (v v65 v1)) (v (^ v0 v1) v65))))
(545 (instantiate 342 ((v0 . (^ v0 v1))(v1 . v65)(v2 . (v v65 v1)))) ((= (v (^ (v (^ v0 v1) v65) (v v65 v1)) (^ v65 (v v65 v1))) (^ (v v65 v1) (v (^ v0 v1) v65)))))
(546 (paramod 544 (1 1) 545 (1 1 1)) ((= (v (v (^ v0 v1) v65) (^ v65 (v v65 v1))) (^ (v v65 v1) (v (^ v0 v1) v65)))))
(547 (instantiate 6 ((v0 . (^ v0 v1))(v1 . v65)(v2 . (^ v65 (v v65 v1))))) ((= (v (v (^ v0 v1) v65) (^ v65 (v v65 v1))) (v (^ v0 v1) (v v65 (^ v65 (v v65 v1)))))))
(548 (paramod 547 (1 1) 546 (1 1)) ((= (v (^ v0 v1) (v v65 (^ v65 (v v65 v1)))) (^ (v v65 v1) (v (^ v0 v1) v65)))))
(549 (instantiate 325 ((v0 . v65)(v1 . (v v65 v1)))) ((= (v v65 (^ v65 (v v65 v1))) (^ (v v65 (v v65 v1)) v65))))
(550 (paramod 549 (1 1) 548 (1 1 2)) ((= (v (^ v0 v1) (^ (v v65 (v v65 v1)) v65)) (^ (v v65 v1) (v (^ v0 v1) v65)))))
(551 (instantiate 47 ((v0 . v65)(v1 . v1))) ((= (v v65 (v v65 v1)) (v v65 v1))))
(552 (paramod 551 (1 1) 550 (1 1 2 1)) ((= (v (^ v0 v1) (^ (v v65 v1) v65)) (^ (v v65 v1) (v (^ v0 v1) v65)))))
(553 (instantiate 543 ((v0 . v65)(v1 . v1)(v2 . v0))) ((= (^ (v v65 v1) (v (^ v0 v1) v65)) (v (^ v0 v1) v65))))
(554 (paramod 553 (1 1) 552 (1 2)) ((= (v (^ v0 v1) (^ (v v65 v1) v65)) (v (^ v0 v1) v65))))
(555 (instantiate 554 ((v65 . v2))) ((= (v (^ v0 v1) (^ (v v2 v1) v2)) (v (^ v0 v1) v2))))
(556 (instantiate 420 ((v1 . v66)(v2 . v65))) ((= (^ (v (^ v0 v66) v65) (v v65 v66)) (v (^ v0 v66) v65))))
(557 (instantiate 338 ((v0 . (v (^ v0 v66) v65))(v1 . v65)(v2 . v66))) ((= (v (^ (v (^ v0 v66) v65) (v v65 v66)) (^ (v (^ v0 v66) v65) (^ (v v66 v65) v65))) (^ (v (^ v0 v66) v65) (v v65 v66)))))
(558 (paramod 556 (1 1) 557 (1 1 1)) ((= (v (v (^ v0 v66) v65) (^ (v (^ v0 v66) v65) (^ (v v66 v65) v65))) (^ (v (^ v0 v66) v65) (v v65 v66)))))
(559 (instantiate 325 ((v0 . (v (^ v0 v66) v65))(v1 . (^ (v v66 v65) v65)))) ((= (v (v (^ v0 v66) v65) (^ (v (^ v0 v66) v65) (^ (v v66 v65) v65))) (^ (v (v (^ v0 v66) v65) (^ (v v66 v65) v65)) (v (^ v0 v66) v65)))))
(560 (paramod 559 (1 1) 558 (1 1)) ((= (^ (v (v (^ v0 v66) v65) (^ (v v66 v65) v65)) (v (^ v0 v66) v65)) (^ (v (^ v0 v66) v65) (v v65 v66)))))
(561 (instantiate 6 ((v0 . (^ v0 v66))(v1 . v65)(v2 . (^ (v v66 v65) v65)))) ((= (v (v (^ v0 v66) v65) (^ (v v66 v65) v65)) (v (^ v0 v66) (v v65 (^ (v v66 v65) v65))))))
(562 (paramod 561 (1 1) 560 (1 1 1)) ((= (^ (v (^ v0 v66) (v v65 (^ (v v66 v65) v65))) (v (^ v0 v66) v65)) (^ (v (^ v0 v66) v65) (v v65 v66)))))
(563 (instantiate 312 ((v0 . v65)(v1 . (v v66 v65)))) ((= (v v65 (^ (v v66 v65) v65)) (^ v65 (v v65 (v v66 v65))))))
(564 (paramod 563 (1 1) 562 (1 1 1 2)) ((= (^ (v (^ v0 v66) (^ v65 (v v65 (v v66 v65)))) (v (^ v0 v66) v65)) (^ (v (^ v0 v66) v65) (v v65 v66)))))
(565 (instantiate 57 ((v0 . v65)(v1 . v66))) ((= (v v65 (v v66 v65)) (v v66 v65))))
(566 (paramod 565 (1 1) 564 (1 1 1 2 2)) ((= (^ (v (^ v0 v66) (^ v65 (v v66 v65))) (v (^ v0 v66) v65)) (^ (v (^ v0 v66) v65) (v v65 v66)))))
(567 (instantiate 8 ((v0 . (^ v0 v66))(v1 . v65)(v2 . (v v66 v65)))) ((= (^ (v (^ v0 v66) (^ v65 (v v66 v65))) (v (^ v0 v66) v65)) (v (^ v0 v66) (^ v65 (v v66 v65))))))
(568 (paramod 567 (1 1) 566 (1 1)) ((= (v (^ v0 v66) (^ v65 (v v66 v65))) (^ (v (^ v0 v66) v65) (v v65 v66)))))
(569 (instantiate 420 ((v0 . v0)(v1 . v66)(v2 . v65))) ((= (^ (v (^ v0 v66) v65) (v v65 v66)) (v (^ v0 v66) v65))))
(570 (paramod 569 (1 1) 568 (1 2)) ((= (v (^ v0 v66) (^ v65 (v v66 v65))) (v (^ v0 v66) v65))))
(571 (instantiate 570 ((v65 . v2)(v66 . v1))) ((= (v (^ v0 v1) (^ v2 (v v1 v2))) (v (^ v0 v1) v2))))
(572 (instantiate 27 ((v0 . (v v0 v2))(v1 . v65)(v2 . (v (^ v0 v1) v2)))) ((= (^ v65 (^ (v (^ v0 v1) v2) (v v0 v2))) (^ (v v0 v2) (^ v65 (v (^ v0 v1) v2))))))
(573 (paramod 449 (1 1) 572 (1 1 2)) ((= (^ v65 (v (^ v0 v1) v2)) (^ (v v0 v2) (^ v65 (v (^ v0 v1) v2))))))
(574 (flip 573 (1)) ((= (^ (v v0 v2) (^ v65 (v (^ v0 v1) v2))) (^ v65 (v (^ v0 v1) v2)))))
(575 (instantiate 574 ((v1 . v3)(v2 . v1)(v65 . v2))) ((= (^ (v v0 v1) (^ v2 (v (^ v0 v3) v1))) (^ v2 (v (^ v0 v3) v1)))))
(576 (instantiate 456 ((v0 . v64)(v1 . (v v65 v66)))) ((= (v (^ v64 (v v65 v66)) (v v65 v66)) (^ (v v65 v66) (v v64 (v v65 v66))))))
(577 (instantiate 231 ((v0 . v64)(v1 . v65)(v2 . v66)(v3 . (v v65 v66)))) ((= (v (^ v64 v65) (v (^ v64 (v v65 v66)) (v v65 v66))) (v (^ v64 (v v65 v66)) (v v65 v66)))))
(578 (paramod 576 (1 1) 577 (1 1 2)) ((= (v (^ v64 v65) (^ (v v65 v66) (v v64 (v v65 v66)))) (v (^ v64 (v v65 v66)) (v v65 v66)))))
(579 (instantiate 523 ((v0 . v64)(v1 . v65)(v2 . (v v65 v66)))) ((= (v (^ v64 v65) (^ (v v65 v66) (v v64 (v v65 v66)))) (v (^ v64 v65) (v v65 v66)))))
(580 (paramod 579 (1 1) 578 (1 1)) ((= (v (^ v64 v65) (v v65 v66)) (v (^ v64 (v v65 v66)) (v v65 v66)))))
(581 (instantiate 456 ((v0 . v64)(v1 . (v v65 v66)))) ((= (v (^ v64 (v v65 v66)) (v v65 v66)) (^ (v v65 v66) (v v64 (v v65 v66))))))
(582 (paramod 581 (1 1) 580 (1 2)) ((= (v (^ v64 v65) (v v65 v66)) (^ (v v65 v66) (v v64 (v v65 v66))))))
(583 (instantiate 582 ((v64 . v0)(v65 . v1)(v66 . v2))) ((= (v (^ v0 v1) (v v1 v2)) (^ (v v1 v2) (v v0 (v v1 v2))))))
(584 (instantiate 278 ((v0 . v65)(v1 . v66))) ((= (^ (v v65 v66) (v v65 (^ v2 v66))) (v v65 (^ v2 v66)))))
(585 (instantiate 460 ((v0 . (^ v2 v66))(v1 . v65)(v2 . v66))) ((= (^ (^ v2 v66) (^ (v v65 v66) (v v65 (^ v2 v66)))) (^ (^ v2 v66) (v v65 v66)))))
(586 (paramod 584 (1 1) 585 (1 1 2)) ((= (^ (^ v2 v66) (v v65 (^ v2 v66))) (^ (^ v2 v66) (v v65 v66)))))
(587 (instantiate 3 ((v0 . v2)(v1 . v66)(v2 . (v v65 (^ v2 v66))))) ((= (^ (^ v2 v66) (v v65 (^ v2 v66))) (^ v2 (^ v66 (v v65 (^ v2 v66)))))))
(588 (paramod 587 (1 1) 586 (1 1)) ((= (^ v2 (^ v66 (v v65 (^ v2 v66)))) (^ (^ v2 v66) (v v65 v66)))))
(589 (instantiate 3 ((v0 . v2)(v1 . v66)(v2 . (v v65 v66)))) ((= (^ (^ v2 v66) (v v65 v66)) (^ v2 (^ v66 (v v65 v66))))))
(590 (paramod 589 (1 1) 588 (1 2)) ((= (^ v2 (^ v66 (v v65 (^ v2 v66)))) (^ v2 (^ v66 (v v65 v66))))))
(591 (instantiate 590 ((v2 . v0)(v65 . v2)(v66 . v1))) ((= (^ v0 (^ v1 (v v2 (^ v0 v1)))) (^ v0 (^ v1 (v v2 v1))))))
(592 (instantiate 460 ((v0 . v67)(v1 . v66))) ((= (^ v67 (^ (v v66 v2) (v v66 v67))) (^ v67 (v v66 v2)))))
(593 (instantiate 334 ((v0 . v67)(v1 . (v v66 v2))(v2 . v66)(v3 . v67))) ((= (v (^ v67 (^ (v v66 v2) (v v66 v67))) (^ (v v66 v2) (^ v67 v67))) (^ (v v66 v2) (^ v67 (v v66 v67))))))
(594 (paramod 592 (1 1) 593 (1 1 1)) ((= (v (^ v67 (v v66 v2)) (^ (v v66 v2) (^ v67 v67))) (^ (v v66 v2) (^ v67 (v v66 v67))))))
(595 (instantiate 1 ((v0 . v67))) ((= (^ v67 v67) v67)))
(596 (paramod 595 (1 1) 594 (1 1 2 2)) ((= (v (^ v67 (v v66 v2)) (^ (v v66 v2) v67)) (^ (v v66 v2) (^ v67 (v v66 v67))))))
(597 (instantiate 158 ((v0 . v67)(v1 . (v v66 v2)))) ((= (v (^ v67 (v v66 v2)) (^ (v v66 v2) v67)) (^ (v v66 v2) v67))))
(598 (paramod 597 (1 1) 596 (1 1)) ((= (^ (v v66 v2) v67) (^ (v v66 v2) (^ v67 (v v66 v67))))))
(599 (flip 598 (1)) ((= (^ (v v66 v2) (^ v67 (v v66 v67))) (^ (v v66 v2) v67))))
(600 (instantiate 599 ((v2 . v1)(v66 . v0)(v67 . v2))) ((= (^ (v v0 v1) (^ v2 (v v0 v2))) (^ (v v0 v1) v2))))
(601 (instantiate 488 ((v0 . v66)(v1 . v66))) ((= (^ v66 (v v66 (^ v66 (v v66 v2)))) (^ v66 (v v66 v2)))))
(602 (instantiate 442 ((v0 . (^ v66 (v v66 v2)))(v1 . v65)(v2 . v66))) ((= (^ (^ v66 (v v66 v2)) (v v65 (^ v66 (v v66 (^ v66 (v v66 v2)))))) (^ (^ v66 (v v66 v2)) (v v65 v66)))))
(603 (paramod 601 (1 1) 602 (1 1 2 2)) ((= (^ (^ v66 (v v66 v2)) (v v65 (^ v66 (v v66 v2)))) (^ (^ v66 (v v66 v2)) (v v65 v66)))))
(604 (instantiate 3 ((v0 . v66)(v1 . (v v66 v2))(v2 . (v v65 (^ v66 (v v66 v2)))))) ((= (^ (^ v66 (v v66 v2)) (v v65 (^ v66 (v v66 v2)))) (^ v66 (^ (v v66 v2) (v v65 (^ v66 (v v66 v2))))))))
(605 (paramod 604 (1 1) 603 (1 1)) ((= (^ v66 (^ (v v66 v2) (v v65 (^ v66 (v v66 v2))))) (^ (^ v66 (v v66 v2)) (v v65 v66)))))
(606 (instantiate 591 ((v0 . v66)(v1 . (v v66 v2))(v2 . v65))) ((= (^ v66 (^ (v v66 v2) (v v65 (^ v66 (v v66 v2))))) (^ v66 (^ (v v66 v2) (v v65 (v v66 v2)))))))
(607 (paramod 606 (1 1) 605 (1 1)) ((= (^ v66 (^ (v v66 v2) (v v65 (v v66 v2)))) (^ (^ v66 (v v66 v2)) (v v65 v66)))))
(608 (instantiate 502 ((v0 . v66)(v1 . v2)(v2 . v65)(v3 . v66))) ((= (^ v66 (^ (v v66 v2) (v v65 (v v66 v2)))) (^ v66 (v v65 (v v66 v2))))))
(609 (paramod 608 (1 1) 607 (1 1)) ((= (^ v66 (v v65 (v v66 v2))) (^ (^ v66 (v v66 v2)) (v v65 v66)))))
(610 (instantiate 3 ((v0 . v66)(v1 . (v v66 v2))(v2 . (v v65 v66)))) ((= (^ (^ v66 (v v66 v2)) (v v65 v66)) (^ v66 (^ (v v66 v2) (v v65 v66))))))
(611 (paramod 610 (1 1) 609 (1 2)) ((= (^ v66 (v v65 (v v66 v2))) (^ v66 (^ (v v66 v2) (v v65 v66))))))
(612 (instantiate 611 ((v65 . v1)(v66 . v0))) ((= (^ v0 (v v1 (v v0 v2))) (^ v0 (^ (v v0 v2) (v v1 v0))))))
(613 (instantiate 5 ((v0 . v66)(v1 . v64))) ((= (v v66 v64) (v v64 v66))))
(614 (instantiate 507 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (^ (v (^ (v v64 v65) v66) v65) (v v66 v64)) (v (^ v64 v66) (^ v65 (v (^ v64 v65) v66))))))
(615 (paramod 613 (1 1) 614 (1 1 2)) ((= (^ (v (^ (v v64 v65) v66) v65) (v v64 v66)) (v (^ v64 v66) (^ v65 (v (^ v64 v65) v66))))))
(616 (instantiate 615 ((v64 . v0)(v65 . v1)(v66 . v2))) ((= (^ (v (^ (v v0 v1) v2) v1) (v v0 v2)) (v (^ v0 v2) (^ v1 (v (^ v0 v1) v2))))))
(617 (instantiate 3 ((v2 . (v v64 (^ v0 v1))))) ((= (^ (^ v0 v1) (v v64 (^ v0 v1))) (^ v0 (^ v1 (v v64 (^ v0 v1)))))))
(618 (instantiate 523 ((v0 . v64)(v1 . v65)(v2 . (^ v0 v1)))) ((= (v (^ v64 v65) (^ (^ v0 v1) (v v64 (^ v0 v1)))) (v (^ v64 v65) (^ v0 v1)))))
(619 (paramod 617 (1 1) 618 (1 1 2)) ((= (v (^ v64 v65) (^ v0 (^ v1 (v v64 (^ v0 v1))))) (v (^ v64 v65) (^ v0 v1)))))
(620 (instantiate 591 ((v0 . v0)(v1 . v1)(v2 . v64))) ((= (^ v0 (^ v1 (v v64 (^ v0 v1)))) (^ v0 (^ v1 (v v64 v1))))))
(621 (paramod 620 (1 1) 619 (1 1 2)) ((= (v (^ v64 v65) (^ v0 (^ v1 (v v64 v1)))) (v (^ v64 v65) (^ v0 v1)))))
(622 (instantiate 621 ((v0 . v2)(v1 . v3)(v64 . v0)(v65 . v1))) ((= (v (^ v0 v1) (^ v2 (^ v3 (v v0 v3)))) (v (^ v0 v1) (^ v2 v3)))))
(623 (instantiate 460 ((v0 . (^ v2 (v v0 v2)))(v1 . (^ v0 v1))(v2 . v66))) ((= (^ (^ v2 (v v0 v2)) (^ (v (^ v0 v1) v66) (v (^ v0 v1) (^ v2 (v v0 v2))))) (^ (^ v2 (v v0 v2)) (v (^ v0 v1) v66)))))
(624 (paramod 523 (1 1) 623 (1 1 2 2)) ((= (^ (^ v2 (v v0 v2)) (^ (v (^ v0 v1) v66) (v (^ v0 v1) v2))) (^ (^ v2 (v v0 v2)) (v (^ v0 v1) v66)))))
(625 (instantiate 3 ((v0 . v2)(v1 . (v v0 v2))(v2 . (^ (v (^ v0 v1) v66) (v (^ v0 v1) v2))))) ((= (^ (^ v2 (v v0 v2)) (^ (v (^ v0 v1) v66) (v (^ v0 v1) v2))) (^ v2 (^ (v v0 v2) (^ (v (^ v0 v1) v66) (v (^ v0 v1) v2)))))))
(626 (paramod 625 (1 1) 624 (1 1)) ((= (^ v2 (^ (v v0 v2) (^ (v (^ v0 v1) v66) (v (^ v0 v1) v2)))) (^ (^ v2 (v v0 v2)) (v (^ v0 v1) v66)))))
(627 (instantiate 575 ((v0 . v0)(v1 . v2)(v2 . (v (^ v0 v1) v66))(v3 . v1))) ((= (^ (v v0 v2) (^ (v (^ v0 v1) v66) (v (^ v0 v1) v2))) (^ (v (^ v0 v1) v66) (v (^ v0 v1) v2)))))
(628 (paramod 627 (1 1) 626 (1 1 2)) ((= (^ v2 (^ (v (^ v0 v1) v66) (v (^ v0 v1) v2))) (^ (^ v2 (v v0 v2)) (v (^ v0 v1) v66)))))
(629 (instantiate 460 ((v0 . v2)(v1 . (^ v0 v1))(v2 . v66))) ((= (^ v2 (^ (v (^ v0 v1) v66) (v (^ v0 v1) v2))) (^ v2 (v (^ v0 v1) v66)))))
(630 (paramod 629 (1 1) 628 (1 1)) ((= (^ v2 (v (^ v0 v1) v66)) (^ (^ v2 (v v0 v2)) (v (^ v0 v1) v66)))))
(631 (instantiate 3 ((v0 . v2)(v1 . (v v0 v2))(v2 . (v (^ v0 v1) v66)))) ((= (^ (^ v2 (v v0 v2)) (v (^ v0 v1) v66)) (^ v2 (^ (v v0 v2) (v (^ v0 v1) v66))))))
(632 (paramod 631 (1 1) 630 (1 2)) ((= (^ v2 (v (^ v0 v1) v66)) (^ v2 (^ (v v0 v2) (v (^ v0 v1) v66))))))
(633 (flip 632 (1)) ((= (^ v2 (^ (v v0 v2) (v (^ v0 v1) v66))) (^ v2 (v (^ v0 v1) v66)))))
(634 (instantiate 633 ((v0 . v1)(v1 . v2)(v2 . v0)(v66 . v3))) ((= (^ v0 (^ (v v1 v0) (v (^ v1 v2) v3))) (^ v0 (v (^ v1 v2) v3)))))
(635 (instantiate 363 ((v0 . v65)(v1 . v64)(v2 . (v v66 v65)))) ((= (v v65 (^ v64 (v v66 v65))) (v (^ (v v66 v65) v64) v65))))
(636 (instantiate 539 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (^ v64 (v v65 (^ v64 (v v66 v65)))) (^ v64 (v v66 v65)))))
(637 (paramod 635 (1 1) 636 (1 1 2)) ((= (^ v64 (v (^ (v v66 v65) v64) v65)) (^ v64 (v v66 v65)))))
(638 (instantiate 637 ((v64 . v0)(v65 . v2)(v66 . v1))) ((= (^ v0 (v (^ (v v1 v2) v0) v2)) (^ v0 (v v1 v2)))))
(639 (instantiate 571 ((v1 . v64)(v2 . v66))) ((= (v (^ v0 v64) (^ v66 (v v64 v66))) (v (^ v0 v64) v66))))
(640 (instantiate 388 ((v0 . v64)(v1 . (^ v0 v64))(v2 . v66))) ((= (v v64 (v (^ v0 v64) (^ v66 (v v64 v66)))) (v (^ v0 v64) (v v64 v66)))))
(641 (paramod 639 (1 1) 640 (1 1 2)) ((= (v v64 (v (^ v0 v64) v66)) (v (^ v0 v64) (v v64 v66)))))
(642 (instantiate 583 ((v0 . v0)(v1 . v64)(v2 . v66))) ((= (v (^ v0 v64) (v v64 v66)) (^ (v v64 v66) (v v0 (v v64 v66))))))
(643 (paramod 642 (1 1) 641 (1 2)) ((= (v v64 (v (^ v0 v64) v66)) (^ (v v64 v66) (v v0 (v v64 v66))))))
(644 (instantiate 643 ((v0 . v1)(v64 . v0)(v66 . v2))) ((= (v v0 (v (^ v1 v0) v2)) (^ (v v0 v2) (v v1 (v v0 v2))))))
(645 (instantiate 17 ((v0 . v66)(v1 . v67)(v2 . (v v64 v67)))) ((= (^ v66 (^ v67 (v v64 v67))) (^ v67 (^ v66 (v v64 v67))))))
(646 (instantiate 622 ((v0 . v64)(v1 . v65)(v2 . v66)(v3 . v67))) ((= (v (^ v64 v65) (^ v66 (^ v67 (v v64 v67)))) (v (^ v64 v65) (^ v66 v67)))))
(647 (paramod 645 (1 1) 646 (1 1 2)) ((= (v (^ v64 v65) (^ v67 (^ v66 (v v64 v67)))) (v (^ v64 v65) (^ v66 v67)))))
(648 (instantiate 647 ((v64 . v0)(v65 . v1)(v66 . v3)(v67 . v2))) ((= (v (^ v0 v1) (^ v2 (^ v3 (v v0 v2)))) (v (^ v0 v1) (^ v3 v2)))))
(649 (instantiate 616 ((v1 . v66))) ((= (^ (v (^ (v v0 v66) v2) v66) (v v0 v2)) (v (^ v0 v2) (^ v66 (v (^ v0 v66) v2))))))
(650 (instantiate 638 ((v0 . (v v0 v2))(v1 . (^ (v v0 v66) v2))(v2 . v66))) ((= (^ (v v0 v2) (v (^ (v (^ (v v0 v66) v2) v66) (v v0 v2)) v66)) (^ (v v0 v2) (v (^ (v v0 v66) v2) v66)))))
(651 (paramod 649 (1 1) 650 (1 1 2 1)) ((= (^ (v v0 v2) (v (v (^ v0 v2) (^ v66 (v (^ v0 v66) v2))) v66)) (^ (v v0 v2) (v (^ (v v0 v66) v2) v66)))))
(652 (instantiate 6 ((v0 . (^ v0 v2))(v1 . (^ v66 (v (^ v0 v66) v2)))(v2 . v66))) ((= (v (v (^ v0 v2) (^ v66 (v (^ v0 v66) v2))) v66) (v (^ v0 v2) (v (^ v66 (v (^ v0 v66) v2)) v66)))))
(653 (paramod 652 (1 1) 651 (1 1 2)) ((= (^ (v v0 v2) (v (^ v0 v2) (v (^ v66 (v (^ v0 v66) v2)) v66))) (^ (v v0 v2) (v (^ (v v0 v66) v2) v66)))))
(654 (instantiate 326 ((v0 . v66)(v1 . (v (^ v0 v66) v2)))) ((= (v (^ v66 (v (^ v0 v66) v2)) v66) (^ v66 (v v66 (v (^ v0 v66) v2))))))
(655 (paramod 654 (1 1) 653 (1 1 2 2)) ((= (^ (v v0 v2) (v (^ v0 v2) (^ v66 (v v66 (v (^ v0 v66) v2))))) (^ (v v0 v2) (v (^ (v v0 v66) v2) v66)))))
(656 (instantiate 644 ((v0 . v66)(v1 . v0)(v2 . v2))) ((= (v v66 (v (^ v0 v66) v2)) (^ (v v66 v2) (v v0 (v v66 v2))))))
(657 (paramod 656 (1 1) 655 (1 1 2 2 2)) ((= (^ (v v0 v2) (v (^ v0 v2) (^ v66 (^ (v v66 v2) (v v0 (v v66 v2)))))) (^ (v v0 v2) (v (^ (v v0 v66) v2) v66)))))
(658 (instantiate 502 ((v0 . v66)(v1 . v2)(v2 . v0)(v3 . v66))) ((= (^ v66 (^ (v v66 v2) (v v0 (v v66 v2)))) (^ v66 (v v0 (v v66 v2))))))
(659 (paramod 658 (1 1) 657 (1 1 2 2)) ((= (^ (v v0 v2) (v (^ v0 v2) (^ v66 (v v0 (v v66 v2))))) (^ (v v0 v2) (v (^ (v v0 v66) v2) v66)))))
(660 (instantiate 612 ((v0 . v66)(v1 . v0)(v2 . v2))) ((= (^ v66 (v v0 (v v66 v2))) (^ v66 (^ (v v66 v2) (v v0 v66))))))
(661 (paramod 660 (1 1) 659 (1 1 2 2)) ((= (^ (v v0 v2) (v (^ v0 v2) (^ v66 (^ (v v66 v2) (v v0 v66))))) (^ (v v0 v2) (v (^ (v v0 v66) v2) v66)))))
(662 (instantiate 648 ((v0 . v0)(v1 . v2)(v2 . v66)(v3 . (v v66 v2)))) ((= (v (^ v0 v2) (^ v66 (^ (v v66 v2) (v v0 v66)))) (v (^ v0 v2) (^ (v v66 v2) v66)))))
(663 (paramod 662 (1 1) 661 (1 1 2)) ((= (^ (v v0 v2) (v (^ v0 v2) (^ (v v66 v2) v66))) (^ (v v0 v2) (v (^ (v v0 v66) v2) v66)))))
(664 (instantiate 555 ((v0 . v0)(v1 . v2)(v2 . v66))) ((= (v (^ v0 v2) (^ (v v66 v2) v66)) (v (^ v0 v2) v66))))
(665 (paramod 664 (1 1) 663 (1 1 2)) ((= (^ (v v0 v2) (v (^ v0 v2) v66)) (^ (v v0 v2) (v (^ (v v0 v66) v2) v66)))))
(666 (flip 665 (1)) ((= (^ (v v0 v2) (v (^ (v v0 v66) v2) v66)) (^ (v v0 v2) (v (^ v0 v2) v66)))))
(667 (instantiate 666 ((v2 . v1)(v66 . v2))) ((= (^ (v v0 v1) (v (^ (v v0 v2) v1) v2)) (^ (v v0 v1) (v (^ v0 v1) v2)))))
(668 (instantiate 600 ((v0 . v65)(v1 . v66))) ((= (^ (v v65 v66) (^ v2 (v v65 v2))) (^ (v v65 v66) v2))))
(669 (instantiate 638 ((v0 . (^ v2 (v v65 v2)))(v1 . v65)(v2 . v66))) ((= (^ (^ v2 (v v65 v2)) (v (^ (v v65 v66) (^ v2 (v v65 v2))) v66)) (^ (^ v2 (v v65 v2)) (v v65 v66)))))
(670 (paramod 668 (1 1) 669 (1 1 2 1)) ((= (^ (^ v2 (v v65 v2)) (v (^ (v v65 v66) v2) v66)) (^ (^ v2 (v v65 v2)) (v v65 v66)))))
(671 (instantiate 3 ((v0 . v2)(v1 . (v v65 v2))(v2 . (v (^ (v v65 v66) v2) v66)))) ((= (^ (^ v2 (v v65 v2)) (v (^ (v v65 v66) v2) v66)) (^ v2 (^ (v v65 v2) (v (^ (v v65 v66) v2) v66))))))
(672 (paramod 671 (1 1) 670 (1 1)) ((= (^ v2 (^ (v v65 v2) (v (^ (v v65 v66) v2) v66))) (^ (^ v2 (v v65 v2)) (v v65 v66)))))
(673 (instantiate 667 ((v0 . v65)(v1 . v2)(v2 . v66))) ((= (^ (v v65 v2) (v (^ (v v65 v66) v2) v66)) (^ (v v65 v2) (v (^ v65 v2) v66)))))
(674 (paramod 673 (1 1) 672 (1 1 2)) ((= (^ v2 (^ (v v65 v2) (v (^ v65 v2) v66))) (^ (^ v2 (v v65 v2)) (v v65 v66)))))
(675 (instantiate 634 ((v0 . v2)(v1 . v65)(v2 . v2)(v3 . v66))) ((= (^ v2 (^ (v v65 v2) (v (^ v65 v2) v66))) (^ v2 (v (^ v65 v2) v66)))))
(676 (paramod 675 (1 1) 674 (1 1)) ((= (^ v2 (v (^ v65 v2) v66)) (^ (^ v2 (v v65 v2)) (v v65 v66)))))
(677 (instantiate 3 ((v0 . v2)(v1 . (v v65 v2))(v2 . (v v65 v66)))) ((= (^ (^ v2 (v v65 v2)) (v v65 v66)) (^ v2 (^ (v v65 v2) (v v65 v66))))))
(678 (paramod 677 (1 1) 676 (1 2)) ((= (^ v2 (v (^ v65 v2) v66)) (^ v2 (^ (v v65 v2) (v v65 v66))))))
(679 (instantiate 466 ((v0 . v2)(v1 . v65)(v2 . v66))) ((= (^ v2 (^ (v v65 v2) (v v65 v66))) (^ v2 (v v65 v66)))))
(680 (paramod 679 (1 1) 678 (1 2)) ((= (^ v2 (v (^ v65 v2) v66)) (^ v2 (v v65 v66)))))
(681 (instantiate 680 ((v2 . v0)(v65 . v1)(v66 . v2))) ((= (^ v0 (v (^ v1 v0) v2)) (^ v0 (v v1 v2)))))
(682 (instantiate 681 ((v0 . v0)(v1 . v1)(v2 . (^ v0 v2)))) ((= (^ v0 (v (^ v1 v0) (^ v0 v2))) (^ v0 (v v1 (^ v0 v2))))))
(683 (paramod 682 (1 1) 496 (1 1)) ((= (^ v0 (v v1 (^ v0 v2))) (v (^ v1 v0) (^ v0 v2)))))
(684 (flip 683 (1)) ((= (v (^ v1 v0) (^ v0 v2)) (^ v0 (v v1 (^ v0 v2))))))
(685 (instantiate 684 ((v0 . v1)(v1 . v0))) ((= (v (^ v0 v1) (^ v1 v2)) (^ v1 (v v0 (^ v1 v2))))))
(686 (instantiate 685 ((v0 . (v (^ v0 v1) v2))(v1 . v1)(v2 . v0))) ((= (v (^ (v (^ v0 v1) v2) v1) (^ v1 v0)) (^ v1 (v (v (^ v0 v1) v2) (^ v1 v0))))))
(687 (paramod 686 (1 1) 367 (1 1)) ((= (^ v1 (v (v (^ v0 v1) v2) (^ v1 v0))) (^ v1 (v (^ v0 v1) v2)))))
(688 (instantiate 6 ((v0 . (^ v0 v1))(v1 . v2)(v2 . (^ v1 v0)))) ((= (v (v (^ v0 v1) v2) (^ v1 v0)) (v (^ v0 v1) (v v2 (^ v1 v0))))))
(689 (paramod 688 (1 1) 687 (1 1 2)) ((= (^ v1 (v (^ v0 v1) (v v2 (^ v1 v0)))) (^ v1 (v (^ v0 v1) v2)))))
(690 (paramod 357 (1 1) 689 (1 1 2)) ((= (^ v1 (v v2 (^ v1 v0))) (^ v1 (v (^ v0 v1) v2)))))
(691 (instantiate 681 ((v0 . v1)(v1 . v0)(v2 . v2))) ((= (^ v1 (v (^ v0 v1) v2)) (^ v1 (v v0 v2)))))
(692 (paramod 691 (1 1) 690 (1 2)) ((= (^ v1 (v v2 (^ v1 v0))) (^ v1 (v v0 v2)))))
(693 (instantiate 692 ((v0 . v2)(v1 . v0)(v2 . v1))) ((= (^ v0 (v v1 (^ v0 v2))) (^ v0 (v v2 v1)))))
(694 (instantiate 685 ((v0 . (C))(v1 . (A))(v2 . (B)))) ((= (v (^ (C) (A)) (^ (A) (B))) (^ (A) (v (C) (^ (A) (B)))))))
(695 (paramod 694 (1 1) 525 (1 1 1)) ((not (= (^ (A) (v (C) (^ (A) (B)))) (^ (A) (v (B) (C)))))))
(696 (instantiate 693 ((v0 . (A))(v1 . (C))(v2 . (B)))) ((= (^ (A) (v (C) (^ (A) (B)))) (^ (A) (v (B) (C))))))
(697 (resolve 695 (1) 696 (1)) ())
)