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