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