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