;; ----- Otter 3.0.4, August 1995 -----
;; The job was started by mccune on gyro, Sun Feb 11 18:31:13 1996
;;
;;;; 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 (z^ (x v y))= (x v y)^ (z v (x^y)).
;;;; A^ (B v (A^C))!= (A^B) v (A^C).
;;
;; ----> UNIT CONFLICT at  12.04 sec ----> 533 [binary,532.1,3.1] $F.
;;
(
(1 (input) ((= (v v0 v1) (v v1 v0))))
(2 (input) ((= v0 v0)))
(3 (input) ((= (^ v0 v0) v0)))
(4 (input) ((= (^ v0 v1) (^ v1 v0))))
(5 (input) ((= (^ (^ v0 v1) v2) (^ v0 (^ v1 v2)))))
(6 (input) ((= (v v0 v0) v0)))
(7 (input) ((= (v (v v0 v1) v2) (v v0 (v v1 v2)))))
(8 (input) ((= (v (^ v0 (v v1 v2)) (^ v0 v1)) (^ v0 (v v1 v2)))))
(9 (input) ((= (^ (v v0 (^ v1 v2)) (v v0 v1)) (v v0 (^ v1 v2)))))
(10 (input) ((= (v (^ v0 v1) (^ v2 (v v0 v1))) (^ (v v0 v1) (v v2 (^ v0 v1))))))
(11 (input) ((not (= (^ (A) (v (B) (^ (A) (C)))) (v (^ (A) (B)) (^ (A) (C)))))))
(12 (flip 11 (1)) ((not (= (v (^ (A) (B)) (^ (A) (C))) (^ (A) (v (B) (^ (A) (C))))))))
(13 (instantiate 3 ((v0 . (v v65 v66)))) ((= (^ (v v65 v66) (v v65 v66)) (v v65 v66))))
(14 (instantiate 8 ((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)))))
(15 (paramod 13 (1 1) 14 (1 1 1)) ((= (v (v v65 v66) (^ (v v65 v66) v65)) (^ (v v65 v66) (v v65 v66)))))
(16 (instantiate 7 ((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))))))
(17 (paramod 16 (1 1) 15 (1 1)) ((= (v v65 (v v66 (^ (v v65 v66) v65))) (^ (v v65 v66) (v v65 v66)))))
(18 (instantiate 3 ((v0 . (v v65 v66)))) ((= (^ (v v65 v66) (v v65 v66)) (v v65 v66))))
(19 (paramod 18 (1 1) 17 (1 2)) ((= (v v65 (v v66 (^ (v v65 v66) v65))) (v v65 v66))))
(20 (instantiate 19 ((v65 . v0)(v66 . v1))) ((= (v v0 (v v1 (^ (v v0 v1) v0))) (v v0 v1))))
(21 (instantiate 1 ((v0 . v64)(v1 . (v v65 (^ (v v64 v65) v64))))) ((= (v v64 (v v65 (^ (v v64 v65) v64))) (v (v v65 (^ (v v64 v65) v64)) v64))))
(22 (instantiate 20 ((v0 . v64)(v1 . v65))) ((= (v v64 (v v65 (^ (v v64 v65) v64))) (v v64 v65))))
(23 (paramod 21 (1 1) 22 (1 1)) ((= (v (v v65 (^ (v v64 v65) v64)) v64) (v v64 v65))))
(24 (instantiate 7 ((v0 . v65)(v1 . (^ (v v64 v65) v64))(v2 . v64))) ((= (v (v v65 (^ (v v64 v65) v64)) v64) (v v65 (v (^ (v v64 v65) v64) v64)))))
(25 (paramod 24 (1 1) 23 (1 1)) ((= (v v65 (v (^ (v v64 v65) v64) v64)) (v v64 v65))))
(26 (instantiate 25 ((v64 . v1)(v65 . v0))) ((= (v v0 (v (^ (v v1 v0) v1) v1)) (v v1 v0))))
(27 (instantiate 26 ((v0 . (^ v0 v1))(v1 . (^ v0 (v v1 v2))))) ((= (v (^ v0 v1) (v (^ (v (^ v0 (v v1 v2)) (^ v0 v1)) (^ v0 (v v1 v2))) (^ v0 (v v1 v2)))) (v (^ v0 (v v1 v2)) (^ v0 v1)))))
(28 (paramod 8 (1 1) 27 (1 1 2 1 1)) ((= (v (^ v0 v1) (v (^ (^ v0 (v v1 v2)) (^ v0 (v v1 v2))) (^ v0 (v v1 v2)))) (v (^ v0 (v v1 v2)) (^ v0 v1)))))
(29 (instantiate 3 ((v0 . (^ v0 (v v1 v2))))) ((= (^ (^ v0 (v v1 v2)) (^ v0 (v v1 v2))) (^ v0 (v v1 v2)))))
(30 (paramod 29 (1 1) 28 (1 1 2 1)) ((= (v (^ v0 v1) (v (^ v0 (v v1 v2)) (^ v0 (v v1 v2)))) (v (^ v0 (v v1 v2)) (^ v0 v1)))))
(31 (instantiate 6 ((v0 . (^ v0 (v v1 v2))))) ((= (v (^ v0 (v v1 v2)) (^ v0 (v v1 v2))) (^ v0 (v v1 v2)))))
(32 (paramod 31 (1 1) 30 (1 1 2)) ((= (v (^ v0 v1) (^ v0 (v v1 v2))) (v (^ v0 (v v1 v2)) (^ v0 v1)))))
(33 (paramod 8 (1 1) 32 (1 2)) ((= (v (^ v0 v1) (^ v0 (v v1 v2))) (^ v0 (v v1 v2)))))
(34 (instantiate 26 ((v0 . v65))) ((= (v v65 (v (^ (v v1 v65) v1) v1)) (v v1 v65))))
(35 (instantiate 8 ((v0 . v64)(v1 . v65)(v2 . (v (^ (v v1 v65) v1) v1)))) ((= (v (^ v64 (v v65 (v (^ (v v1 v65) v1) v1))) (^ v64 v65)) (^ v64 (v v65 (v (^ (v v1 v65) v1) v1))))))
(36 (paramod 34 (1 1) 35 (1 1 1 2)) ((= (v (^ v64 (v v1 v65)) (^ v64 v65)) (^ v64 (v v65 (v (^ (v v1 v65) v1) v1))))))
(37 (instantiate 26 ((v0 . v65)(v1 . v1))) ((= (v v65 (v (^ (v v1 v65) v1) v1)) (v v1 v65))))
(38 (paramod 37 (1 1) 36 (1 2 2)) ((= (v (^ v64 (v v1 v65)) (^ v64 v65)) (^ v64 (v v1 v65)))))
(39 (instantiate 38 ((v64 . v0)(v65 . v2))) ((= (v (^ v0 (v v1 v2)) (^ v0 v2)) (^ v0 (v v1 v2)))))
(40 (instantiate 4 ((v0 . (v v0 (^ v1 v2)))(v1 . (v v0 v1)))) ((= (^ (v v0 (^ v1 v2)) (v v0 v1)) (^ (v v0 v1) (v v0 (^ v1 v2))))))
(41 (paramod 9 (1 1) 40 (1 1)) ((= (v v0 (^ v1 v2)) (^ (v v0 v1) (v v0 (^ v1 v2))))))
(42 (flip 41 (1)) ((= (^ (v v0 v1) (v v0 (^ v1 v2))) (v v0 (^ v1 v2)))))
(43 (instantiate 1 ((v0 . v64)(v1 . v65))) ((= (v v64 v65) (v v65 v64))))
(44 (instantiate 42 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (^ (v v64 v65) (v v64 (^ v65 v66))) (v v64 (^ v65 v66)))))
(45 (paramod 43 (1 1) 44 (1 1 1)) ((= (^ (v v65 v64) (v v64 (^ v65 v66))) (v v64 (^ v65 v66)))))
(46 (instantiate 45 ((v64 . v1)(v65 . v0)(v66 . v2))) ((= (^ (v v0 v1) (v v1 (^ v0 v2))) (v v1 (^ v0 v2)))))
(47 (instantiate 4 ((v0 . v65)(v1 . v66))) ((= (^ v65 v66) (^ v66 v65))))
(48 (instantiate 9 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (^ (v v64 (^ v65 v66)) (v v64 v65)) (v v64 (^ v65 v66)))))
(49 (paramod 47 (1 1) 48 (1 1 1 2)) ((= (^ (v v64 (^ v66 v65)) (v v64 v65)) (v v64 (^ v65 v66)))))
(50 (instantiate 49 ((v64 . v0)(v65 . v2)(v66 . v1))) ((= (^ (v v0 (^ v1 v2)) (v v0 v2)) (v v0 (^ v2 v1)))))
(51 (instantiate 4 ((v0 . v64)(v1 . v65))) ((= (^ v64 v65) (^ v65 v64))))
(52 (instantiate 33 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (v (^ v64 v65) (^ v64 (v v65 v66))) (^ v64 (v v65 v66)))))
(53 (paramod 51 (1 1) 52 (1 1 1)) ((= (v (^ v65 v64) (^ v64 (v v65 v66))) (^ v64 (v v65 v66)))))
(54 (instantiate 53 ((v64 . v1)(v65 . v0)(v66 . v2))) ((= (v (^ v0 v1) (^ v1 (v v0 v2))) (^ v1 (v v0 v2)))))
(55 (flip 50 (1)) ((= (v v0 (^ v2 v1)) (^ (v v0 (^ v1 v2)) (v v0 v2)))))
(56 (instantiate 3 ((v0 . v65))) ((= (^ v65 v65) v65)))
(57 (instantiate 5 ((v0 . v65)(v1 . v65)(v2 . v66))) ((= (^ (^ v65 v65) v66) (^ v65 (^ v65 v66)))))
(58 (paramod 56 (1 1) 57 (1 1 1)) ((= (^ v65 v66) (^ v65 (^ v65 v66)))))
(59 (flip 58 (1)) ((= (^ v65 (^ v65 v66)) (^ v65 v66))))
(60 (instantiate 59 ((v65 . v0)(v66 . v1))) ((= (^ v0 (^ v0 v1)) (^ v0 v1))))
(61 (instantiate 4 ((v0 . v66)(v1 . v65))) ((= (^ v66 v65) (^ v65 v66))))
(62 (instantiate 55 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (v v64 (^ v66 v65)) (^ (v v64 (^ v65 v66)) (v v64 v66)))))
(63 (paramod 61 (1 1) 62 (1 1 2)) ((= (v v64 (^ v65 v66)) (^ (v v64 (^ v65 v66)) (v v64 v66)))))
(64 (flip 63 (1)) ((= (^ (v v64 (^ v65 v66)) (v v64 v66)) (v v64 (^ v65 v66)))))
(65 (instantiate 64 ((v64 . v0)(v65 . v1)(v66 . v2))) ((= (^ (v v0 (^ v1 v2)) (v v0 v2)) (v v0 (^ v1 v2)))))
(66 (instantiate 1 ((v0 . v64)(v1 . v66))) ((= (v v64 v66) (v v66 v64))))
(67 (instantiate 65 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (^ (v v64 (^ v65 v66)) (v v64 v66)) (v v64 (^ v65 v66)))))
(68 (paramod 66 (1 1) 67 (1 1 2)) ((= (^ (v v64 (^ v65 v66)) (v v66 v64)) (v v64 (^ v65 v66)))))
(69 (instantiate 68 ((v64 . v0)(v65 . v1)(v66 . v2))) ((= (^ (v v0 (^ v1 v2)) (v v2 v0)) (v v0 (^ v1 v2)))))
(70 (instantiate 4 ((v0 . v64)(v1 . v65))) ((= (^ v64 v65) (^ v65 v64))))
(71 (instantiate 60 ((v0 . v64)(v1 . v65))) ((= (^ v64 (^ v64 v65)) (^ v64 v65))))
(72 (paramod 70 (1 1) 71 (1 1 2)) ((= (^ v64 (^ v65 v64)) (^ v64 v65))))
(73 (instantiate 72 ((v64 . v0)(v65 . v1))) ((= (^ v0 (^ v1 v0)) (^ v0 v1))))
(74 (instantiate 60 ((v0 . v64))) ((= (^ v64 (^ v64 v1)) (^ v64 v1))))
(75 (instantiate 39 ((v0 . v64)(v1 . v65)(v2 . (^ v64 v1)))) ((= (v (^ v64 (v v65 (^ v64 v1))) (^ v64 (^ v64 v1))) (^ v64 (v v65 (^ v64 v1))))))
(76 (paramod 74 (1 1) 75 (1 1 2)) ((= (v (^ v64 (v v65 (^ v64 v1))) (^ v64 v1)) (^ v64 (v v65 (^ v64 v1))))))
(77 (instantiate 76 ((v1 . v2)(v64 . v0)(v65 . v1))) ((= (v (^ v0 (v v1 (^ v0 v2))) (^ v0 v2)) (^ v0 (v v1 (^ v0 v2))))))
(78 (instantiate 5 ((v0 . (v v0 (^ v1 v2)))(v1 . (v v0 v2))(v2 . v66))) ((= (^ (^ (v v0 (^ v1 v2)) (v v0 v2)) v66) (^ (v v0 (^ v1 v2)) (^ (v v0 v2) v66)))))
(79 (paramod 65 (1 1) 78 (1 1 1)) ((= (^ (v v0 (^ v1 v2)) v66) (^ (v v0 (^ v1 v2)) (^ (v v0 v2) v66)))))
(80 (flip 79 (1)) ((= (^ (v v0 (^ v1 v2)) (^ (v v0 v2) v66)) (^ (v v0 (^ v1 v2)) v66))))
(81 (instantiate 80 ((v66 . v3))) ((= (^ (v v0 (^ v1 v2)) (^ (v v0 v2) v3)) (^ (v v0 (^ v1 v2)) v3))))
(82 (instantiate 1 ((v0 . v64)(v1 . v66))) ((= (v v64 v66) (v v66 v64))))
(83 (instantiate 81 ((v0 . v64)(v1 . v65)(v2 . v66)(v3 . v67))) ((= (^ (v v64 (^ v65 v66)) (^ (v v64 v66) v67)) (^ (v v64 (^ v65 v66)) v67))))
(84 (paramod 82 (1 1) 83 (1 1 2 1)) ((= (^ (v v64 (^ v65 v66)) (^ (v v66 v64) v67)) (^ (v v64 (^ v65 v66)) v67))))
(85 (instantiate 84 ((v64 . v0)(v65 . v1)(v66 . v2)(v67 . v3))) ((= (^ (v v0 (^ v1 v2)) (^ (v v2 v0) v3)) (^ (v v0 (^ v1 v2)) v3))))
(86 (instantiate 69 ((v0 . v66))) ((= (^ (v v66 (^ v1 v2)) (v v2 v66)) (v v66 (^ v1 v2)))))
(87 (instantiate 85 ((v0 . (^ v1 v2))(v1 . v65)(v2 . v66)(v3 . (v v2 v66)))) ((= (^ (v (^ v1 v2) (^ v65 v66)) (^ (v v66 (^ v1 v2)) (v v2 v66))) (^ (v (^ v1 v2) (^ v65 v66)) (v v2 v66)))))
(88 (paramod 86 (1 1) 87 (1 1 2)) ((= (^ (v (^ v1 v2) (^ v65 v66)) (v v66 (^ v1 v2))) (^ (v (^ v1 v2) (^ v65 v66)) (v v2 v66)))))
(89 (instantiate 69 ((v0 . (^ v1 v2))(v1 . v65)(v2 . v66))) ((= (^ (v (^ v1 v2) (^ v65 v66)) (v v66 (^ v1 v2))) (v (^ v1 v2) (^ v65 v66)))))
(90 (paramod 89 (1 1) 88 (1 1)) ((= (v (^ v1 v2) (^ v65 v66)) (^ (v (^ v1 v2) (^ v65 v66)) (v v2 v66)))))
(91 (flip 90 (1)) ((= (^ (v (^ v1 v2) (^ v65 v66)) (v v2 v66)) (v (^ v1 v2) (^ v65 v66)))))
(92 (instantiate 91 ((v1 . v0)(v2 . v1)(v65 . v2)(v66 . v3))) ((= (^ (v (^ v0 v1) (^ v2 v3)) (v v1 v3)) (v (^ v0 v1) (^ v2 v3)))))
(93 (instantiate 4 ((v0 . (v (^ v64 v65) (^ v66 v67)))(v1 . (v v65 v67)))) ((= (^ (v (^ v64 v65) (^ v66 v67)) (v v65 v67)) (^ (v v65 v67) (v (^ v64 v65) (^ v66 v67))))))
(94 (instantiate 92 ((v0 . v64)(v1 . v65)(v2 . v66)(v3 . v67))) ((= (^ (v (^ v64 v65) (^ v66 v67)) (v v65 v67)) (v (^ v64 v65) (^ v66 v67)))))
(95 (paramod 93 (1 1) 94 (1 1)) ((= (^ (v v65 v67) (v (^ v64 v65) (^ v66 v67))) (v (^ v64 v65) (^ v66 v67)))))
(96 (instantiate 95 ((v64 . v2)(v65 . v0)(v66 . v3)(v67 . v1))) ((= (^ (v v0 v1) (v (^ v2 v0) (^ v3 v1))) (v (^ v2 v0) (^ v3 v1)))))
(97 (instantiate 1 ((v0 . v64)(v1 . v65))) ((= (v v64 v65) (v v65 v64))))
(98 (instantiate 96 ((v0 . v64)(v1 . v65)(v2 . v66)(v3 . v67))) ((= (^ (v v64 v65) (v (^ v66 v64) (^ v67 v65))) (v (^ v66 v64) (^ v67 v65)))))
(99 (paramod 97 (1 1) 98 (1 1 1)) ((= (^ (v v65 v64) (v (^ v66 v64) (^ v67 v65))) (v (^ v66 v64) (^ v67 v65)))))
(100 (instantiate 99 ((v64 . v1)(v65 . v0)(v66 . v2)(v67 . v3))) ((= (^ (v v0 v1) (v (^ v2 v1) (^ v3 v0))) (v (^ v2 v1) (^ v3 v0)))))
(101 (instantiate 5 ((v2 . (v v64 v65)))) ((= (^ (^ v0 v1) (v v64 v65)) (^ v0 (^ v1 (v v64 v65))))))
(102 (instantiate 10 ((v0 . v64)(v1 . v65)(v2 . (^ v0 v1)))) ((= (v (^ v64 v65) (^ (^ v0 v1) (v v64 v65))) (^ (v v64 v65) (v (^ v0 v1) (^ v64 v65))))))
(103 (paramod 101 (1 1) 102 (1 1 2)) ((= (v (^ v64 v65) (^ v0 (^ v1 (v v64 v65)))) (^ (v v64 v65) (v (^ v0 v1) (^ v64 v65))))))
(104 (instantiate 103 ((v0 . v2)(v1 . v3)(v64 . v0)(v65 . v1))) ((= (v (^ v0 v1) (^ v2 (^ v3 (v v0 v1)))) (^ (v v0 v1) (v (^ v2 v3) (^ v0 v1))))))
(105 (instantiate 54 ((v0 . v64)(v1 . v66)(v2 . v66))) ((= (v (^ v64 v66) (^ v66 (v v64 v66))) (^ v66 (v v64 v66)))))
(106 (instantiate 10 ((v0 . v64)(v1 . v66)(v2 . v66))) ((= (v (^ v64 v66) (^ v66 (v v64 v66))) (^ (v v64 v66) (v v66 (^ v64 v66))))))
(107 (paramod 105 (1 1) 106 (1 1)) ((= (^ v66 (v v64 v66)) (^ (v v64 v66) (v v66 (^ v64 v66))))))
(108 (instantiate 46 ((v0 . v64)(v1 . v66)(v2 . v66))) ((= (^ (v v64 v66) (v v66 (^ v64 v66))) (v v66 (^ v64 v66)))))
(109 (paramod 108 (1 1) 107 (1 2)) ((= (^ v66 (v v64 v66)) (v v66 (^ v64 v66)))))
(110 (instantiate 109 ((v64 . v1)(v66 . v0))) ((= (^ v0 (v v1 v0)) (v v0 (^ v1 v0)))))
(111 (flip 104 (1)) ((= (^ (v v0 v1) (v (^ v2 v3) (^ v0 v1))) (v (^ v0 v1) (^ v2 (^ v3 (v v0 v1)))))))
(112 (instantiate 1 ((v0 . v65)(v1 . v64))) ((= (v v65 v64) (v v64 v65))))
(113 (instantiate 110 ((v0 . v64)(v1 . v65))) ((= (^ v64 (v v65 v64)) (v v64 (^ v65 v64)))))
(114 (paramod 112 (1 1) 113 (1 1 2)) ((= (^ v64 (v v64 v65)) (v v64 (^ v65 v64)))))
(115 (flip 114 (1)) ((= (v v64 (^ v65 v64)) (^ v64 (v v64 v65)))))
(116 (instantiate 115 ((v64 . v0)(v65 . v1))) ((= (v v0 (^ v1 v0)) (^ v0 (v v0 v1)))))
(117 (instantiate 1 ((v0 . (^ v66 v67))(v1 . (^ v64 v65)))) ((= (v (^ v66 v67) (^ v64 v65)) (v (^ v64 v65) (^ v66 v67)))))
(118 (instantiate 111 ((v0 . v64)(v1 . v65)(v2 . v66)(v3 . v67))) ((= (^ (v v64 v65) (v (^ v66 v67) (^ v64 v65))) (v (^ v64 v65) (^ v66 (^ v67 (v v64 v65)))))))
(119 (paramod 117 (1 1) 118 (1 1 2)) ((= (^ (v v64 v65) (v (^ v64 v65) (^ v66 v67))) (v (^ v64 v65) (^ v66 (^ v67 (v v64 v65)))))))
(120 (flip 119 (1)) ((= (v (^ v64 v65) (^ v66 (^ v67 (v v64 v65)))) (^ (v v64 v65) (v (^ v64 v65) (^ v66 v67))))))
(121 (instantiate 120 ((v64 . v0)(v65 . v1)(v66 . v2)(v67 . v3))) ((= (v (^ v0 v1) (^ v2 (^ v3 (v v0 v1)))) (^ (v v0 v1) (v (^ v0 v1) (^ v2 v3))))))
(122 (instantiate 116 ((v0 . v64))) ((= (v v64 (^ v1 v64)) (^ v64 (v v64 v1)))))
(123 (instantiate 10 ((v0 . v64)(v1 . (^ v1 v64))(v2 . v66))) ((= (v (^ v64 (^ v1 v64)) (^ v66 (v v64 (^ v1 v64)))) (^ (v v64 (^ v1 v64)) (v v66 (^ v64 (^ v1 v64)))))))
(124 (paramod 122 (1 1) 123 (1 1 2 2)) ((= (v (^ v64 (^ v1 v64)) (^ v66 (^ v64 (v v64 v1)))) (^ (v v64 (^ v1 v64)) (v v66 (^ v64 (^ v1 v64)))))))
(125 (instantiate 73 ((v0 . v64)(v1 . v1))) ((= (^ v64 (^ v1 v64)) (^ v64 v1))))
(126 (paramod 125 (1 1) 124 (1 1 1)) ((= (v (^ v64 v1) (^ v66 (^ v64 (v v64 v1)))) (^ (v v64 (^ v1 v64)) (v v66 (^ v64 (^ v1 v64)))))))
(127 (instantiate 121 ((v0 . v64)(v1 . v1)(v2 . v66)(v3 . v64))) ((= (v (^ v64 v1) (^ v66 (^ v64 (v v64 v1)))) (^ (v v64 v1) (v (^ v64 v1) (^ v66 v64))))))
(128 (paramod 127 (1 1) 126 (1 1)) ((= (^ (v v64 v1) (v (^ v64 v1) (^ v66 v64))) (^ (v v64 (^ v1 v64)) (v v66 (^ v64 (^ v1 v64)))))))
(129 (instantiate 100 ((v0 . v64)(v1 . v1)(v2 . v64)(v3 . v66))) ((= (^ (v v64 v1) (v (^ v64 v1) (^ v66 v64))) (v (^ v64 v1) (^ v66 v64)))))
(130 (paramod 129 (1 1) 128 (1 1)) ((= (v (^ v64 v1) (^ v66 v64)) (^ (v v64 (^ v1 v64)) (v v66 (^ v64 (^ v1 v64)))))))
(131 (instantiate 116 ((v0 . v64)(v1 . v1))) ((= (v v64 (^ v1 v64)) (^ v64 (v v64 v1)))))
(132 (paramod 131 (1 1) 130 (1 2 1)) ((= (v (^ v64 v1) (^ v66 v64)) (^ (^ v64 (v v64 v1)) (v v66 (^ v64 (^ v1 v64)))))))
(133 (instantiate 73 ((v0 . v64)(v1 . v1))) ((= (^ v64 (^ v1 v64)) (^ v64 v1))))
(134 (paramod 133 (1 1) 132 (1 2 2 2)) ((= (v (^ v64 v1) (^ v66 v64)) (^ (^ v64 (v v64 v1)) (v v66 (^ v64 v1))))))
(135 (instantiate 5 ((v0 . v64)(v1 . (v v64 v1))(v2 . (v v66 (^ v64 v1))))) ((= (^ (^ v64 (v v64 v1)) (v v66 (^ v64 v1))) (^ v64 (^ (v v64 v1) (v v66 (^ v64 v1)))))))
(136 (paramod 135 (1 1) 134 (1 2)) ((= (v (^ v64 v1) (^ v66 v64)) (^ v64 (^ (v v64 v1) (v v66 (^ v64 v1)))))))
(137 (instantiate 136 ((v64 . v0)(v66 . v2))) ((= (v (^ v0 v1) (^ v2 v0)) (^ v0 (^ (v v0 v1) (v v2 (^ v0 v1)))))))
(138 (instantiate 4 ((v0 . v66)(v1 . v64))) ((= (^ v66 v64) (^ v64 v66))))
(139 (instantiate 137 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (v (^ v64 v65) (^ v66 v64)) (^ v64 (^ (v v64 v65) (v v66 (^ v64 v65)))))))
(140 (paramod 138 (1 1) 139 (1 1 2)) ((= (v (^ v64 v65) (^ v64 v66)) (^ v64 (^ (v v64 v65) (v v66 (^ v64 v65)))))))
(141 (instantiate 140 ((v64 . v0)(v65 . v1)(v66 . v2))) ((= (v (^ v0 v1) (^ v0 v2)) (^ v0 (^ (v v0 v1) (v v2 (^ v0 v1)))))))
(142 (instantiate 1 ((v0 . (^ v64 v65))(v1 . (^ v64 v66)))) ((= (v (^ v64 v65) (^ v64 v66)) (v (^ v64 v66) (^ v64 v65)))))
(143 (instantiate 141 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (v (^ v64 v65) (^ v64 v66)) (^ v64 (^ (v v64 v65) (v v66 (^ v64 v65)))))))
(144 (paramod 142 (1 1) 143 (1 1)) ((= (v (^ v64 v66) (^ v64 v65)) (^ v64 (^ (v v64 v65) (v v66 (^ v64 v65)))))))
(145 (instantiate 144 ((v64 . v0)(v65 . v2)(v66 . v1))) ((= (v (^ v0 v1) (^ v0 v2)) (^ v0 (^ (v v0 v2) (v v1 (^ v0 v2)))))))
(146 (instantiate 145 ((v0 . v0)(v1 . (v v1 (^ v0 v2)))(v2 . v2))) ((= (v (^ v0 (v v1 (^ v0 v2))) (^ v0 v2)) (^ v0 (^ (v v0 v2) (v (v v1 (^ v0 v2)) (^ v0 v2)))))))
(147 (paramod 146 (1 1) 77 (1 1)) ((= (^ v0 (^ (v v0 v2) (v (v v1 (^ v0 v2)) (^ v0 v2)))) (^ v0 (v v1 (^ v0 v2))))))
(148 (instantiate 7 ((v0 . v1)(v1 . (^ v0 v2))(v2 . (^ v0 v2)))) ((= (v (v v1 (^ v0 v2)) (^ v0 v2)) (v v1 (v (^ v0 v2) (^ v0 v2))))))
(149 (paramod 148 (1 1) 147 (1 1 2 2)) ((= (^ v0 (^ (v v0 v2) (v v1 (v (^ v0 v2) (^ v0 v2))))) (^ v0 (v v1 (^ v0 v2))))))
(150 (instantiate 6 ((v0 . (^ v0 v2)))) ((= (v (^ v0 v2) (^ v0 v2)) (^ v0 v2))))
(151 (paramod 150 (1 1) 149 (1 1 2 2 2)) ((= (^ v0 (^ (v v0 v2) (v v1 (^ v0 v2)))) (^ v0 (v v1 (^ v0 v2))))))
(152 (instantiate 151 ((v1 . v2)(v2 . v1))) ((= (^ v0 (^ (v v0 v1) (v v2 (^ v0 v1)))) (^ v0 (v v2 (^ v0 v1))))))
(153 (instantiate 145 ((v0 . (A))(v1 . (B))(v2 . (C)))) ((= (v (^ (A) (B)) (^ (A) (C))) (^ (A) (^ (v (A) (C)) (v (B) (^ (A) (C))))))))
(154 (paramod 153 (1 1) 12 (1 1 1)) ((not (= (^ (A) (^ (v (A) (C)) (v (B) (^ (A) (C))))) (^ (A) (v (B) (^ (A) (C))))))))
(155 (instantiate 152 ((v0 . (A))(v1 . (C))(v2 . (B)))) ((= (^ (A) (^ (v (A) (C)) (v (B) (^ (A) (C))))) (^ (A) (v (B) (^ (A) (C)))))))
(156 (paramod 155 (1 1) 154 (1 1 1)) ((not (= (^ (A) (v (B) (^ (A) (C)))) (^ (A) (v (B) (^ (A) (C))))))))
(157 (instantiate 2 ((v0 . (^ (A) (v (B) (^ (A) (C))))))) ((= (^ (A) (v (B) (^ (A) (C)))) (^ (A) (v (B) (^ (A) (C)))))))
(158 (resolve 156 (1) 157 (1)) ())
)