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