;; ----- Otter 3.0.4, August 1995 -----
;; The job was started by mccune on gyro, Thu Nov  2 00:21:43 1995
;;
;;;;  -> x=x.
;;;; z1-x=u, z2-y=u, z1-z=w, z3-y=w -> z2-z=z3-x.
;;;;  -> x=x.
;;;;  -> x- (y-x)=x.
;;;;  -> x- (x-y)=y- (y-x).
;;;; A=B -> .
;;
;; ----> UNIT CONFLICT at   0.75 sec ----> 51 [binary,50.1,1.1]  -> .
;;
(
(1 (input) ((not (= (A) (B)))))
(2 (input) ((= v0 v0)))
(3 (input) ((not (= (- v0 v1) v2)) (not (= (- v3 v4) v2)) (not (= (- v0 v5) v6)) (not (= (- v7 v4) v6)) (= (- v3 v5) (- v7 v1))))
(4 (input) ((= (- v0 (- v1 v0)) v0)))
(5 (input) ((= (- v0 (- v0 v1)) (- v1 (- v1 v0)))))
(6 (instantiate 4 ((v0 . v65))) ((= (- v65 (- v1 v65)) v65)))
(7 (instantiate 4 ((v0 . (- v1 v65))(v1 . v65))) ((= (- (- v1 v65) (- v65 (- v1 v65))) (- v1 v65))))
(8 (paramod 6 (1 1) 7 (1 1 2)) ((= (- (- v1 v65) v65) (- v1 v65))))
(9 (instantiate 8 ((v1 . v0)(v65 . v1))) ((= (- (- v0 v1) v1) (- v0 v1))))
(10 (instantiate 3 ((v0 . (- v64 v65))(v1 . v65)(v2 . (- v64 v65)))) ((not (= (- (- v64 v65) v65) (- v64 v65))) (not (= (- v3 v4) (- v64 v65))) (not (= (- (- v64 v65) v5) v6)) (not (= (- v7 v4) v6)) (= (- v3 v5) (- v7 v65))))
(11 (instantiate 9 ((v0 . v64)(v1 . v65))) ((= (- (- v64 v65) v65) (- v64 v65))))
(12 (resolve 10 (1) 11 (1)) ((not (= (- v3 v4) (- v64 v65))) (not (= (- (- v64 v65) v5) v6)) (not (= (- v7 v4) v6)) (= (- v3 v5) (- v7 v65))))
(13 (instantiate 12 ((v3 . v0)(v4 . v1)(v5 . v4)(v6 . v5)(v7 . v6)(v64 . v2)(v65 . v3))) ((not (= (- v0 v1) (- v2 v3))) (not (= (- (- v2 v3) v4) v5)) (not (= (- v6 v1) v5)) (= (- v0 v4) (- v6 v3))))
(14 (instantiate 13 ((v2 . v0)(v3 . v1))) ((not (= (- v0 v1) (- v0 v1))) (not (= (- (- v0 v1) v4) v5)) (not (= (- v6 v1) v5)) (= (- v0 v4) (- v6 v1))))
(15 (instantiate 2 ((v0 . (- v0 v1)))) ((= (- v0 v1) (- v0 v1))))
(16 (resolve 14 (1) 15 (1)) ((not (= (- (- v0 v1) v4) v5)) (not (= (- v6 v1) v5)) (= (- v0 v4) (- v6 v1))))
(17 (instantiate 16 ((v4 . v2)(v5 . v3)(v6 . v4))) ((not (= (- (- v0 v1) v2) v3)) (not (= (- v4 v1) v3)) (= (- v0 v2) (- v4 v1))))
(18 (instantiate 17 ((v2 . (- v65 (- v0 v1)))(v3 . (- v0 v1)))) ((not (= (- (- v0 v1) (- v65 (- v0 v1))) (- v0 v1))) (not (= (- v4 v1) (- v0 v1))) (= (- v0 (- v65 (- v0 v1))) (- v4 v1))))
(19 (instantiate 4 ((v0 . (- v0 v1))(v1 . v65))) ((= (- (- v0 v1) (- v65 (- v0 v1))) (- v0 v1))))
(20 (resolve 18 (1) 19 (1)) ((not (= (- v4 v1) (- v0 v1))) (= (- v0 (- v65 (- v0 v1))) (- v4 v1))))
(21 (instantiate 20 ((v0 . v2)(v4 . v0)(v65 . v3))) ((not (= (- v0 v1) (- v2 v1))) (= (- v2 (- v3 (- v2 v1))) (- v0 v1))))
(22 (instantiate 21 ((v0 . (- v64 v65))(v1 . v65)(v2 . v64))) ((not (= (- (- v64 v65) v65) (- v64 v65))) (= (- v64 (- v3 (- v64 v65))) (- (- v64 v65) v65))))
(23 (instantiate 9 ((v0 . v64)(v1 . v65))) ((= (- (- v64 v65) v65) (- v64 v65))))
(24 (resolve 22 (1) 23 (1)) ((= (- v64 (- v3 (- v64 v65))) (- (- v64 v65) v65))))
(25 (instantiate 24 ((v3 . v1)(v64 . v0)(v65 . v2))) ((= (- v0 (- v1 (- v0 v2))) (- (- v0 v2) v2))))
(26 (instantiate 9 ((v0 . v0)(v1 . v2))) ((= (- (- v0 v2) v2) (- v0 v2))))
(27 (paramod 26 (1 1) 25 (1 2)) ((= (- v0 (- v1 (- v0 v2))) (- v0 v2))))
(28 (instantiate 3 ((v0 . (- v64 v65))(v1 . v65)(v2 . (- v64 v65)))) ((not (= (- (- v64 v65) v65) (- v64 v65))) (not (= (- v3 v4) (- v64 v65))) (not (= (- (- v64 v65) v5) v6)) (not (= (- v7 v4) v6)) (= (- v3 v5) (- v7 v65))))
(29 (instantiate 9 ((v0 . v64)(v1 . v65))) ((= (- (- v64 v65) v65) (- v64 v65))))
(30 (resolve 28 (1) 29 (1)) ((not (= (- v3 v4) (- v64 v65))) (not (= (- (- v64 v65) v5) v6)) (not (= (- v7 v4) v6)) (= (- v3 v5) (- v7 v65))))
(31 (instantiate 30 ((v3 . v0)(v4 . v1)(v5 . v4)(v6 . v5)(v7 . v6)(v64 . v2)(v65 . v3))) ((not (= (- v0 v1) (- v2 v3))) (not (= (- (- v2 v3) v4) v5)) (not (= (- v6 v1) v5)) (= (- v0 v4) (- v6 v3))))
(32 (instantiate 31 ((v0 . (- v2 v3))(v1 . (- v65 (- v2 v3))))) ((not (= (- (- v2 v3) (- v65 (- v2 v3))) (- v2 v3))) (not (= (- (- v2 v3) v4) v5)) (not (= (- v6 (- v65 (- v2 v3))) v5)) (= (- (- v2 v3) v4) (- v6 v3))))
(33 (instantiate 4 ((v0 . (- v2 v3))(v1 . v65))) ((= (- (- v2 v3) (- v65 (- v2 v3))) (- v2 v3))))
(34 (resolve 32 (1) 33 (1)) ((not (= (- (- v2 v3) v4) v5)) (not (= (- v6 (- v65 (- v2 v3))) v5)) (= (- (- v2 v3) v4) (- v6 v3))))
(35 (instantiate 34 ((v2 . v0)(v3 . v1)(v4 . v2)(v5 . v3)(v6 . v4)(v65 . v5))) ((not (= (- (- v0 v1) v2) v3)) (not (= (- v4 (- v5 (- v0 v1))) v3)) (= (- (- v0 v1) v2) (- v4 v1))))
(36 (instantiate 35 ((v3 . (- (- v0 v1) v2)))) ((not (= (- (- v0 v1) v2) (- (- v0 v1) v2))) (not (= (- v4 (- v5 (- v0 v1))) (- (- v0 v1) v2))) (= (- (- v0 v1) v2) (- v4 v1))))
(37 (instantiate 2 ((v0 . (- (- v0 v1) v2)))) ((= (- (- v0 v1) v2) (- (- v0 v1) v2))))
(38 (resolve 36 (1) 37 (1)) ((not (= (- v4 (- v5 (- v0 v1))) (- (- v0 v1) v2))) (= (- (- v0 v1) v2) (- v4 v1))))
(39 (instantiate 38 ((v0 . v2)(v1 . v3)(v2 . v4)(v4 . v0)(v5 . v1))) ((not (= (- v0 (- v1 (- v2 v3))) (- (- v2 v3) v4))) (= (- (- v2 v3) v4) (- v0 v3))))
(40 (instantiate 39 ((v0 . v64)(v1 . v64)(v4 . (- (- v2 v3) v64)))) ((not (= (- v64 (- v64 (- v2 v3))) (- (- v2 v3) (- (- v2 v3) v64)))) (= (- (- v2 v3) (- (- v2 v3) v64)) (- v64 v3))))
(41 (instantiate 5 ((v0 . v64)(v1 . (- v2 v3)))) ((= (- v64 (- v64 (- v2 v3))) (- (- v2 v3) (- (- v2 v3) v64)))))
(42 (resolve 40 (1) 41 (1)) ((= (- (- v2 v3) (- (- v2 v3) v64)) (- v64 v3))))
(43 (instantiate 42 ((v2 . v0)(v3 . v1)(v64 . v2))) ((= (- (- v0 v1) (- (- v0 v1) v2)) (- v2 v1))))
(44 (instantiate 3 ((v0 . v64)(v1 . (- v65 (- v64 v66)))(v2 . (- v64 v66)))) ((not (= (- v64 (- v65 (- v64 v66))) (- v64 v66))) (not (= (- v3 v4) (- v64 v66))) (not (= (- v64 v5) v6)) (not (= (- v7 v4) v6)) (= (- v3 v5) (- v7 (- v65 (- v64 v66))))))
(45 (instantiate 27 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (- v64 (- v65 (- v64 v66))) (- v64 v66))))
(46 (resolve 44 (1) 45 (1)) ((not (= (- v3 v4) (- v64 v66))) (not (= (- v64 v5) v6)) (not (= (- v7 v4) v6)) (= (- v3 v5) (- v7 (- v65 (- v64 v66))))))
(47 (instantiate 46 ((v3 . v0)(v4 . v1)(v5 . v4)(v6 . v5)(v7 . v6)(v64 . v2)(v65 . v7)(v66 . v3))) ((not (= (- v0 v1) (- v2 v3))) (not (= (- v2 v4) v5)) (not (= (- v6 v1) v5)) (= (- v0 v4) (- v6 (- v7 (- v2 v3))))))
(48 (instantiate 47 ((v0 . v64)(v1 . (- v65 (- v64 v66)))(v2 . v64)(v3 . v66))) ((not (= (- v64 (- v65 (- v64 v66))) (- v64 v66))) (not (= (- v64 v4) v5)) (not (= (- v6 (- v65 (- v64 v66))) v5)) (= (- v64 v4) (- v6 (- v7 (- v64 v66))))))
(49 (instantiate 27 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (- v64 (- v65 (- v64 v66))) (- v64 v66))))
(50 (resolve 48 (1) 49 (1)) ((not (= (- v64 v4) v5)) (not (= (- v6 (- v65 (- v64 v66))) v5)) (= (- v64 v4) (- v6 (- v7 (- v64 v66))))))
(51 (instantiate 50 ((v4 . v1)(v5 . v2)(v6 . v3)(v7 . v6)(v64 . v0)(v65 . v4)(v66 . v5))) ((not (= (- v0 v1) v2)) (not (= (- v3 (- v4 (- v0 v5))) v2)) (= (- v0 v1) (- v3 (- v6 (- v0 v5))))))
(52 (instantiate 51 ((v0 . (- v64 v65))(v1 . (- (- v64 v65) v66))(v2 . (- v66 v65)))) ((not (= (- (- v64 v65) (- (- v64 v65) v66)) (- v66 v65))) (not (= (- v3 (- v4 (- (- v64 v65) v5))) (- v66 v65))) (= (- (- v64 v65) (- (- v64 v65) v66)) (- v3 (- v6 (- (- v64 v65) v5))))))
(53 (instantiate 43 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (- (- v64 v65) (- (- v64 v65) v66)) (- v66 v65))))
(54 (resolve 52 (1) 53 (1)) ((not (= (- v3 (- v4 (- (- v64 v65) v5))) (- v66 v65))) (= (- (- v64 v65) (- (- v64 v65) v66)) (- v3 (- v6 (- (- v64 v65) v5))))))
(55 (instantiate 54 ((v3 . v0)(v4 . v1)(v5 . v4)(v64 . v2)(v65 . v3)(v66 . v5))) ((not (= (- v0 (- v1 (- (- v2 v3) v4))) (- v5 v3))) (= (- (- v2 v3) (- (- v2 v3) v5)) (- v0 (- v6 (- (- v2 v3) v4))))))
(56 (instantiate 55 ((v0 . (- v64 v65))(v1 . (- v64 v65))(v3 . v65)(v5 . (- (- v2 v65) v4)))) ((not (= (- (- v64 v65) (- (- v64 v65) (- (- v2 v65) v4))) (- (- (- v2 v65) v4) v65))) (= (- (- v2 v65) (- (- v2 v65) (- (- v2 v65) v4))) (- (- v64 v65) (- v6 (- (- v2 v65) v4))))))
(57 (instantiate 43 ((v0 . v64)(v1 . v65)(v2 . (- (- v2 v65) v4)))) ((= (- (- v64 v65) (- (- v64 v65) (- (- v2 v65) v4))) (- (- (- v2 v65) v4) v65))))
(58 (resolve 56 (1) 57 (1)) ((= (- (- v2 v65) (- (- v2 v65) (- (- v2 v65) v4))) (- (- v64 v65) (- v6 (- (- v2 v65) v4))))))
(59 (instantiate 58 ((v2 . v0)(v4 . v2)(v6 . v4)(v64 . v3)(v65 . v1))) ((= (- (- v0 v1) (- (- v0 v1) (- (- v0 v1) v2))) (- (- v3 v1) (- v4 (- (- v0 v1) v2))))))
(60 (instantiate 27 ((v0 . (- v0 v1))(v1 . (- v0 v1))(v2 . v2))) ((= (- (- v0 v1) (- (- v0 v1) (- (- v0 v1) v2))) (- (- v0 v1) v2))))
(61 (paramod 60 (1 1) 59 (1 1)) ((= (- (- v0 v1) v2) (- (- v3 v1) (- v4 (- (- v0 v1) v2))))))
(62 (flip 61 (1)) ((= (- (- v3 v1) (- v4 (- (- v0 v1) v2))) (- (- v0 v1) v2))))
(63 (instantiate 62 ((v0 . v3)(v2 . v4)(v3 . v0)(v4 . v2))) ((= (- (- v0 v1) (- v2 (- (- v3 v1) v4))) (- (- v3 v1) v4))))
(64 (instantiate 3 ((v0 . v64)(v1 . (- v65 (- v64 v66)))(v2 . (- v64 v66)))) ((not (= (- v64 (- v65 (- v64 v66))) (- v64 v66))) (not (= (- v3 v4) (- v64 v66))) (not (= (- v64 v5) v6)) (not (= (- v7 v4) v6)) (= (- v3 v5) (- v7 (- v65 (- v64 v66))))))
(65 (instantiate 27 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (- v64 (- v65 (- v64 v66))) (- v64 v66))))
(66 (resolve 64 (1) 65 (1)) ((not (= (- v3 v4) (- v64 v66))) (not (= (- v64 v5) v6)) (not (= (- v7 v4) v6)) (= (- v3 v5) (- v7 (- v65 (- v64 v66))))))
(67 (instantiate 66 ((v3 . v0)(v4 . v1)(v5 . v4)(v6 . v5)(v7 . v6)(v64 . v2)(v65 . v7)(v66 . v3))) ((not (= (- v0 v1) (- v2 v3))) (not (= (- v2 v4) v5)) (not (= (- v6 v1) v5)) (= (- v0 v4) (- v6 (- v7 (- v2 v3))))))
(68 (instantiate 67 ((v2 . v0)(v3 . v1))) ((not (= (- v0 v1) (- v0 v1))) (not (= (- v0 v4) v5)) (not (= (- v6 v1) v5)) (= (- v0 v4) (- v6 (- v7 (- v0 v1))))))
(69 (instantiate 2 ((v0 . (- v0 v1)))) ((= (- v0 v1) (- v0 v1))))
(70 (resolve 68 (1) 69 (1)) ((not (= (- v0 v4) v5)) (not (= (- v6 v1) v5)) (= (- v0 v4) (- v6 (- v7 (- v0 v1))))))
(71 (instantiate 70 ((v1 . v4)(v4 . v1)(v5 . v2)(v6 . v3)(v7 . v5))) ((not (= (- v0 v1) v2)) (not (= (- v3 v4) v2)) (= (- v0 v1) (- v3 (- v5 (- v0 v4))))))
(72 (instantiate 71 ((v0 . (- v64 v65))(v1 . v65)(v2 . (- v64 v65)))) ((not (= (- (- v64 v65) v65) (- v64 v65))) (not (= (- v3 v4) (- v64 v65))) (= (- (- v64 v65) v65) (- v3 (- v5 (- (- v64 v65) v4))))))
(73 (instantiate 9 ((v0 . v64)(v1 . v65))) ((= (- (- v64 v65) v65) (- v64 v65))))
(74 (resolve 72 (1) 73 (1)) ((not (= (- v3 v4) (- v64 v65))) (= (- (- v64 v65) v65) (- v3 (- v5 (- (- v64 v65) v4))))))
(75 (instantiate 74 ((v3 . v0)(v4 . v1)(v5 . v4)(v64 . v2)(v65 . v3))) ((not (= (- v0 v1) (- v2 v3))) (= (- (- v2 v3) v3) (- v0 (- v4 (- (- v2 v3) v1))))))
(76 (instantiate 75 ((v0 . (- v64 v65))(v1 . (- (- v64 v65) v66))(v2 . v66)(v3 . v65))) ((not (= (- (- v64 v65) (- (- v64 v65) v66)) (- v66 v65))) (= (- (- v66 v65) v65) (- (- v64 v65) (- v4 (- (- v66 v65) (- (- v64 v65) v66)))))))
(77 (instantiate 43 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (- (- v64 v65) (- (- v64 v65) v66)) (- v66 v65))))
(78 (resolve 76 (1) 77 (1)) ((= (- (- v66 v65) v65) (- (- v64 v65) (- v4 (- (- v66 v65) (- (- v64 v65) v66)))))))
(79 (instantiate 78 ((v4 . v3)(v64 . v2)(v65 . v1)(v66 . v0))) ((= (- (- v0 v1) v1) (- (- v2 v1) (- v3 (- (- v0 v1) (- (- v2 v1) v0)))))))
(80 (paramod 9 (1 1) 79 (1 1)) ((= (- v0 v1) (- (- v2 v1) (- v3 (- (- v0 v1) (- (- v2 v1) v0)))))))
(81 (instantiate 63 ((v0 . v2)(v1 . v1)(v2 . v3)(v3 . v0)(v4 . (- (- v2 v1) v0)))) ((= (- (- v2 v1) (- v3 (- (- v0 v1) (- (- v2 v1) v0)))) (- (- v0 v1) (- (- v2 v1) v0)))))
(82 (paramod 81 (1 1) 80 (1 2)) ((= (- v0 v1) (- (- v0 v1) (- (- v2 v1) v0)))))
(83 (flip 82 (1)) ((= (- (- v0 v1) (- (- v2 v1) v0)) (- v0 v1))))
(84 (instantiate 3 ((v0 . (- v64 v65))(v1 . (- (- v64 v65) v66))(v2 . (- v66 v65)))) ((not (= (- (- v64 v65) (- (- v64 v65) v66)) (- v66 v65))) (not (= (- v3 v4) (- v66 v65))) (not (= (- (- v64 v65) v5) v6)) (not (= (- v7 v4) v6)) (= (- v3 v5) (- v7 (- (- v64 v65) v66)))))
(85 (instantiate 43 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (- (- v64 v65) (- (- v64 v65) v66)) (- v66 v65))))
(86 (resolve 84 (1) 85 (1)) ((not (= (- v3 v4) (- v66 v65))) (not (= (- (- v64 v65) v5) v6)) (not (= (- v7 v4) v6)) (= (- v3 v5) (- v7 (- (- v64 v65) v66)))))
(87 (instantiate 86 ((v3 . v0)(v4 . v1)(v64 . v4)(v65 . v3)(v66 . v2))) ((not (= (- v0 v1) (- v2 v3))) (not (= (- (- v4 v3) v5) v6)) (not (= (- v7 v1) v6)) (= (- v0 v5) (- v7 (- (- v4 v3) v2)))))
(88 (instantiate 87 ((v0 . v64)(v1 . (- v65 (- v64 v66)))(v2 . v64)(v3 . v66))) ((not (= (- v64 (- v65 (- v64 v66))) (- v64 v66))) (not (= (- (- v4 v66) v5) v6)) (not (= (- v7 (- v65 (- v64 v66))) v6)) (= (- v64 v5) (- v7 (- (- v4 v66) v64)))))
(89 (instantiate 27 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (- v64 (- v65 (- v64 v66))) (- v64 v66))))
(90 (resolve 88 (1) 89 (1)) ((not (= (- (- v4 v66) v5) v6)) (not (= (- v7 (- v65 (- v64 v66))) v6)) (= (- v64 v5) (- v7 (- (- v4 v66) v64)))))
(91 (instantiate 90 ((v4 . v0)(v5 . v2)(v6 . v3)(v7 . v4)(v64 . v6)(v65 . v5)(v66 . v1))) ((not (= (- (- v0 v1) v2) v3)) (not (= (- v4 (- v5 (- v6 v1))) v3)) (= (- v6 v2) (- v4 (- (- v0 v1) v6)))))
(92 (instantiate 91 ((v0 . v64)(v1 . v65)(v2 . (- (- v64 v65) v66))(v3 . (- v66 v65)))) ((not (= (- (- v64 v65) (- (- v64 v65) v66)) (- v66 v65))) (not (= (- v4 (- v5 (- v6 v65))) (- v66 v65))) (= (- v6 (- (- v64 v65) v66)) (- v4 (- (- v64 v65) v6)))))
(93 (instantiate 43 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (- (- v64 v65) (- (- v64 v65) v66)) (- v66 v65))))
(94 (resolve 92 (1) 93 (1)) ((not (= (- v4 (- v5 (- v6 v65))) (- v66 v65))) (= (- v6 (- (- v64 v65) v66)) (- v4 (- (- v64 v65) v6)))))
(95 (instantiate 94 ((v4 . v0)(v5 . v1)(v6 . v2)(v64 . v5)(v65 . v3)(v66 . v4))) ((not (= (- v0 (- v1 (- v2 v3))) (- v4 v3))) (= (- v2 (- (- v5 v3) v4)) (- v0 (- (- v5 v3) v2)))))
(96 (instantiate 95 ((v0 . (- v2 v3))(v1 . v65)(v4 . v2))) ((not (= (- (- v2 v3) (- v65 (- v2 v3))) (- v2 v3))) (= (- v2 (- (- v5 v3) v2)) (- (- v2 v3) (- (- v5 v3) v2)))))
(97 (instantiate 4 ((v0 . (- v2 v3))(v1 . v65))) ((= (- (- v2 v3) (- v65 (- v2 v3))) (- v2 v3))))
(98 (resolve 96 (1) 97 (1)) ((= (- v2 (- (- v5 v3) v2)) (- (- v2 v3) (- (- v5 v3) v2)))))
(99 (instantiate 98 ((v2 . v0)(v3 . v2)(v5 . v1))) ((= (- v0 (- (- v1 v2) v0)) (- (- v0 v2) (- (- v1 v2) v0)))))
(100 (instantiate 4 ((v0 . v0)(v1 . (- v1 v2)))) ((= (- v0 (- (- v1 v2) v0)) v0)))
(101 (paramod 100 (1 1) 99 (1 1)) ((= v0 (- (- v0 v2) (- (- v1 v2) v0)))))
(102 (instantiate 83 ((v0 . v0)(v1 . v2)(v2 . v1))) ((= (- (- v0 v2) (- (- v1 v2) v0)) (- v0 v2))))
(103 (paramod 102 (1 1) 101 (1 2)) ((= v0 (- v0 v2))))
(104 (flip 103 (1)) ((= (- v0 v2) v0)))
(105 (instantiate 104 ((v2 . v1))) ((= (- v0 v1) v0)))
(106 (instantiate 3 ((v0 . (- v64 v65))(v1 . (- (- v64 v65) v66))(v2 . (- v66 v65)))) ((not (= (- (- v64 v65) (- (- v64 v65) v66)) (- v66 v65))) (not (= (- v3 v4) (- v66 v65))) (not (= (- (- v64 v65) v5) v6)) (not (= (- v7 v4) v6)) (= (- v3 v5) (- v7 (- (- v64 v65) v66)))))
(107 (instantiate 43 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (- (- v64 v65) (- (- v64 v65) v66)) (- v66 v65))))
(108 (resolve 106 (1) 107 (1)) ((not (= (- v3 v4) (- v66 v65))) (not (= (- (- v64 v65) v5) v6)) (not (= (- v7 v4) v6)) (= (- v3 v5) (- v7 (- (- v64 v65) v66)))))
(109 (instantiate 108 ((v3 . v0)(v4 . v1)(v64 . v4)(v65 . v3)(v66 . v2))) ((not (= (- v0 v1) (- v2 v3))) (not (= (- (- v4 v3) v5) v6)) (not (= (- v7 v1) v6)) (= (- v0 v5) (- v7 (- (- v4 v3) v2)))))
(110 (instantiate 109 ((v0 . (- v64 v65))(v1 . v65)(v2 . v64)(v3 . v65))) ((not (= (- (- v64 v65) v65) (- v64 v65))) (not (= (- (- v4 v65) v5) v6)) (not (= (- v7 v65) v6)) (= (- (- v64 v65) v5) (- v7 (- (- v4 v65) v64)))))
(111 (instantiate 9 ((v0 . v64)(v1 . v65))) ((= (- (- v64 v65) v65) (- v64 v65))))
(112 (resolve 110 (1) 111 (1)) ((not (= (- (- v4 v65) v5) v6)) (not (= (- v7 v65) v6)) (= (- (- v64 v65) v5) (- v7 (- (- v4 v65) v64)))))
(113 (instantiate 112 ((v4 . v0)(v5 . v2)(v6 . v3)(v7 . v4)(v64 . v5)(v65 . v1))) ((not (= (- (- v0 v1) v2) v3)) (not (= (- v4 v1) v3)) (= (- (- v5 v1) v2) (- v4 (- (- v0 v1) v5)))))
(114 (instantiate 113 ((v0 . v64)(v1 . v65)(v2 . (- (- v64 v65) v66))(v3 . (- v66 v65)))) ((not (= (- (- v64 v65) (- (- v64 v65) v66)) (- v66 v65))) (not (= (- v4 v65) (- v66 v65))) (= (- (- v5 v65) (- (- v64 v65) v66)) (- v4 (- (- v64 v65) v5)))))
(115 (instantiate 43 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (- (- v64 v65) (- (- v64 v65) v66)) (- v66 v65))))
(116 (resolve 114 (1) 115 (1)) ((not (= (- v4 v65) (- v66 v65))) (= (- (- v5 v65) (- (- v64 v65) v66)) (- v4 (- (- v64 v65) v5)))))
(117 (instantiate 116 ((v4 . v0)(v5 . v3)(v64 . v4)(v65 . v1)(v66 . v2))) ((not (= (- v0 v1) (- v2 v1))) (= (- (- v3 v1) (- (- v4 v1) v2)) (- v0 (- (- v4 v1) v3)))))
(118 (instantiate 117 ((v0 . (- v64 v65))(v1 . v65)(v2 . v64))) ((not (= (- (- v64 v65) v65) (- v64 v65))) (= (- (- v3 v65) (- (- v4 v65) v64)) (- (- v64 v65) (- (- v4 v65) v3)))))
(119 (instantiate 9 ((v0 . v64)(v1 . v65))) ((= (- (- v64 v65) v65) (- v64 v65))))
(120 (resolve 118 (1) 119 (1)) ((= (- (- v3 v65) (- (- v4 v65) v64)) (- (- v64 v65) (- (- v4 v65) v3)))))
(121 (instantiate 120 ((v3 . v0)(v4 . v2)(v64 . v3)(v65 . v1))) ((= (- (- v0 v1) (- (- v2 v1) v3)) (- (- v3 v1) (- (- v2 v1) v0)))))
(122 (paramod 105 (1 1) 121 (1 1 1)) ((= (- v0 (- (- v2 v1) v3)) (- (- v3 v1) (- (- v2 v1) v0)))))
(123 (instantiate 105 ((v0 . v2)(v1 . v1))) ((= (- v2 v1) v2)))
(124 (paramod 123 (1 1) 122 (1 1 2 1)) ((= (- v0 (- v2 v3)) (- (- v3 v1) (- (- v2 v1) v0)))))
(125 (instantiate 105 ((v0 . v2)(v1 . v3))) ((= (- v2 v3) v2)))
(126 (paramod 125 (1 1) 124 (1 1 2)) ((= (- v0 v2) (- (- v3 v1) (- (- v2 v1) v0)))))
(127 (instantiate 105 ((v0 . v0)(v1 . v2))) ((= (- v0 v2) v0)))
(128 (paramod 127 (1 1) 126 (1 1)) ((= v0 (- (- v3 v1) (- (- v2 v1) v0)))))
(129 (instantiate 105 ((v0 . v3)(v1 . v1))) ((= (- v3 v1) v3)))
(130 (paramod 129 (1 1) 128 (1 2 1)) ((= v0 (- v3 (- (- v2 v1) v0)))))
(131 (instantiate 105 ((v0 . v2)(v1 . v1))) ((= (- v2 v1) v2)))
(132 (paramod 131 (1 1) 130 (1 2 2 1)) ((= v0 (- v3 (- v2 v0)))))
(133 (instantiate 105 ((v0 . v2)(v1 . v0))) ((= (- v2 v0) v2)))
(134 (paramod 133 (1 1) 132 (1 2 2)) ((= v0 (- v3 v2))))
(135 (instantiate 105 ((v0 . v3)(v1 . v2))) ((= (- v3 v2) v3)))
(136 (paramod 135 (1 1) 134 (1 2)) ((= v0 v3)))
(137 (instantiate 136 ((v3 . v1))) ((= v0 v1)))
(138 (instantiate 137 ((v0 . (A))(v1 . (B)))) ((= (A) (B))))
(139 (resolve 1 (1) 138 (1)) ())
)