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