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