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