;; ----- Otter 3.0.4, August 1995 -----
;; The job was started by mccune on gyro, Thu Nov  2 00:18:48 1995
;;
;;;; x=x.
;;;; x- (y-x)=x.
;;;; x- (x-y)=y- (y-x).
;;;; (x-y)-z= (x-z)- (y-z).
;;;; (A-C)-B!= (A-B)-C.
;;
;; ----> UNIT CONFLICT at   2.72 sec ----> 629 [binary,627.1,35.1] $F.
;;
(
(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) ((not (= (- (- (A) (C)) (B)) (- (- (A) (B)) (C))))))
(5 (flip 3 (1)) ((= (- (- v0 v2) (- v1 v2)) (- (- v0 v1) v2))))
(6 (instantiate 1 ((v0 . v65))) ((= (- v65 (- v1 v65)) v65)))
(7 (instantiate 1 ((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 9 ((v1 . v65))) ((= (- (- v0 v65) v65) (- v0 v65))))
(11 (instantiate 2 ((v0 . (- v0 v65))(v1 . v65))) ((= (- (- v0 v65) (- (- v0 v65) v65)) (- v65 (- v65 (- v0 v65))))))
(12 (paramod 10 (1 1) 11 (1 1 2)) ((= (- (- v0 v65) (- v0 v65)) (- v65 (- v65 (- v0 v65))))))
(13 (instantiate 1 ((v0 . v65)(v1 . v0))) ((= (- v65 (- v0 v65)) v65)))
(14 (paramod 13 (1 1) 12 (1 2 2)) ((= (- (- v0 v65) (- v0 v65)) (- v65 v65))))
(15 (instantiate 14 ((v65 . v1))) ((= (- (- v0 v1) (- v0 v1)) (- v1 v1))))
(16 (instantiate 2 ((v0 . v64))) ((= (- v64 (- v64 v1)) (- v1 (- v1 v64)))))
(17 (instantiate 2 ((v0 . v64)(v1 . (- v64 v1)))) ((= (- v64 (- v64 (- v64 v1))) (- (- v64 v1) (- (- v64 v1) v64)))))
(18 (paramod 16 (1 1) 17 (1 1 2)) ((= (- v64 (- v1 (- v1 v64))) (- (- v64 v1) (- (- v64 v1) v64)))))
(19 (flip 18 (1)) ((= (- (- v64 v1) (- (- v64 v1) v64)) (- v64 (- v1 (- v1 v64))))))
(20 (instantiate 19 ((v64 . v0))) ((= (- (- v0 v1) (- (- v0 v1) v0)) (- v0 (- v1 (- v1 v0))))))
(21 (instantiate 2 ((v0 . v64))) ((= (- v64 (- v64 v1)) (- v1 (- v1 v64)))))
(22 (instantiate 15 ((v0 . v64)(v1 . (- v64 v1)))) ((= (- (- v64 (- v64 v1)) (- v64 (- v64 v1))) (- (- v64 v1) (- v64 v1)))))
(23 (paramod 21 (1 1) 22 (1 1 1)) ((= (- (- v1 (- v1 v64)) (- v64 (- v64 v1))) (- (- v64 v1) (- v64 v1)))))
(24 (instantiate 15 ((v0 . v64)(v1 . v1))) ((= (- (- v64 v1) (- v64 v1)) (- v1 v1))))
(25 (paramod 24 (1 1) 23 (1 2)) ((= (- (- v1 (- v1 v64)) (- v64 (- v64 v1))) (- v1 v1))))
(26 (instantiate 25 ((v1 . v0)(v64 . v1))) ((= (- (- v0 (- v0 v1)) (- v1 (- v1 v0))) (- v0 v0))))
(27 (instantiate 2 ((v0 . v64))) ((= (- v64 (- v64 v1)) (- v1 (- v1 v64)))))
(28 (instantiate 15 ((v0 . v64)(v1 . (- v64 v1)))) ((= (- (- v64 (- v64 v1)) (- v64 (- v64 v1))) (- (- v64 v1) (- v64 v1)))))
(29 (paramod 27 (1 1) 28 (1 1 2)) ((= (- (- v64 (- v64 v1)) (- v1 (- v1 v64))) (- (- v64 v1) (- v64 v1)))))
(30 (instantiate 26 ((v0 . v64)(v1 . v1))) ((= (- (- v64 (- v64 v1)) (- v1 (- v1 v64))) (- v64 v64))))
(31 (paramod 30 (1 1) 29 (1 1)) ((= (- v64 v64) (- (- v64 v1) (- v64 v1)))))
(32 (instantiate 15 ((v0 . v64)(v1 . v1))) ((= (- (- v64 v1) (- v64 v1)) (- v1 v1))))
(33 (paramod 32 (1 1) 31 (1 2)) ((= (- v64 v64) (- v1 v1))))
(34 (instantiate 33 ((v64 . v0))) ((= (- v0 v0) (- v1 v1))))
(35 (instantiate 3 ((v0 . (A))(v1 . (C))(v2 . (B)))) ((= (- (- (A) (C)) (B)) (- (- (A) (B)) (- (C) (B))))))
(36 (paramod 35 (1 1) 4 (1 1 1)) ((not (= (- (- (A) (B)) (- (C) (B))) (- (- (A) (B)) (C))))))
(37 (instantiate 34 ((v0 . v65))) ((= (- v65 v65) (- v1 v1))))
(38 (instantiate 2 ((v0 . v65)(v1 . v65))) ((= (- v65 (- v65 v65)) (- v65 (- v65 v65)))))
(39 (paramod 37 (1 1) 38 (1 1 2)) ((= (- v65 (- v1 v1)) (- v65 (- v65 v65)))))
(40 (instantiate 1 ((v0 . v65)(v1 . v65))) ((= (- v65 (- v65 v65)) v65)))
(41 (paramod 40 (1 1) 39 (1 2)) ((= (- v65 (- v1 v1)) v65)))
(42 (instantiate 41 ((v65 . v0))) ((= (- v0 (- v1 v1)) v0)))
(43 (instantiate 42 ((v0 . v65))) ((= (- v65 (- v1 v1)) v65)))
(44 (instantiate 1 ((v0 . (- v1 v1))(v1 . v65))) ((= (- (- v1 v1) (- v65 (- v1 v1))) (- v1 v1))))
(45 (paramod 43 (1 1) 44 (1 1 2)) ((= (- (- v1 v1) v65) (- v1 v1))))
(46 (instantiate 45 ((v1 . v0)(v65 . v1))) ((= (- (- v0 v0) v1) (- v0 v0))))
(47 (instantiate 9 ((v1 . v66))) ((= (- (- v0 v66) v66) (- v0 v66))))
(48 (instantiate 5 ((v0 . (- v0 v66))(v1 . v65)(v2 . v66))) ((= (- (- (- v0 v66) v66) (- v65 v66)) (- (- (- v0 v66) v65) v66))))
(49 (paramod 47 (1 1) 48 (1 1 1)) ((= (- (- v0 v66) (- v65 v66)) (- (- (- v0 v66) v65) v66))))
(50 (flip 49 (1)) ((= (- (- (- v0 v66) v65) v66) (- (- v0 v66) (- v65 v66)))))
(51 (instantiate 50 ((v65 . v2)(v66 . v1))) ((= (- (- (- v0 v1) v2) v1) (- (- v0 v1) (- v2 v1)))))
(52 (instantiate 46 ((v0 . v66)(v1 . (- v65 v66)))) ((= (- (- v66 v66) (- v65 v66)) (- v66 v66))))
(53 (instantiate 5 ((v0 . v66)(v1 . v65)(v2 . v66))) ((= (- (- v66 v66) (- v65 v66)) (- (- v66 v65) v66))))
(54 (paramod 52 (1 1) 53 (1 1)) ((= (- v66 v66) (- (- v66 v65) v66))))
(55 (flip 54 (1)) ((= (- (- v66 v65) v66) (- v66 v66))))
(56 (instantiate 55 ((v65 . v1)(v66 . v0))) ((= (- (- v0 v1) v0) (- v0 v0))))
(57 (paramod 56 (1 1) 20 (1 1 2)) ((= (- (- v0 v1) (- v0 v0)) (- v0 (- v1 (- v1 v0))))))
(58 (instantiate 42 ((v0 . (- v0 v1))(v1 . v0))) ((= (- (- v0 v1) (- v0 v0)) (- v0 v1))))
(59 (paramod 58 (1 1) 57 (1 1)) ((= (- v0 v1) (- v0 (- v1 (- v1 v0))))))
(60 (flip 59 (1)) ((= (- v0 (- v1 (- v1 v0))) (- v0 v1))))
(61 (instantiate 56 ((v0 . v66))) ((= (- (- v66 v1) v66) (- v66 v66))))
(62 (instantiate 5 ((v0 . v64)(v1 . (- v66 v1))(v2 . v66))) ((= (- (- v64 v66) (- (- v66 v1) v66)) (- (- v64 (- v66 v1)) v66))))
(63 (paramod 61 (1 1) 62 (1 1 2)) ((= (- (- v64 v66) (- v66 v66)) (- (- v64 (- v66 v1)) v66))))
(64 (instantiate 42 ((v0 . (- v64 v66))(v1 . v66))) ((= (- (- v64 v66) (- v66 v66)) (- v64 v66))))
(65 (paramod 64 (1 1) 63 (1 1)) ((= (- v64 v66) (- (- v64 (- v66 v1)) v66))))
(66 (flip 65 (1)) ((= (- (- v64 (- v66 v1)) v66) (- v64 v66))))
(67 (instantiate 66 ((v1 . v2)(v64 . v0)(v66 . v1))) ((= (- (- v0 (- v1 v2)) v1) (- v0 v1))))
(68 (instantiate 67 ((v1 . v65))) ((= (- (- v0 (- v65 v2)) v65) (- v0 v65))))
(69 (instantiate 56 ((v0 . (- v0 (- v65 v2)))(v1 . v65))) ((= (- (- (- v0 (- v65 v2)) v65) (- v0 (- v65 v2))) (- (- v0 (- v65 v2)) (- v0 (- v65 v2))))))
(70 (paramod 68 (1 1) 69 (1 1 1)) ((= (- (- v0 v65) (- v0 (- v65 v2))) (- (- v0 (- v65 v2)) (- v0 (- v65 v2))))))
(71 (instantiate 15 ((v0 . v0)(v1 . (- v65 v2)))) ((= (- (- v0 (- v65 v2)) (- v0 (- v65 v2))) (- (- v65 v2) (- v65 v2)))))
(72 (paramod 71 (1 1) 70 (1 2)) ((= (- (- v0 v65) (- v0 (- v65 v2))) (- (- v65 v2) (- v65 v2)))))
(73 (instantiate 15 ((v0 . v65)(v1 . v2))) ((= (- (- v65 v2) (- v65 v2)) (- v2 v2))))
(74 (paramod 73 (1 1) 72 (1 2)) ((= (- (- v0 v65) (- v0 (- v65 v2))) (- v2 v2))))
(75 (instantiate 74 ((v65 . v1))) ((= (- (- v0 v1) (- v0 (- v1 v2))) (- v2 v2))))
(76 (instantiate 1 ((v0 . v64))) ((= (- v64 (- v1 v64)) v64)))
(77 (instantiate 75 ((v0 . v64)(v1 . (- v1 v64))(v2 . v66))) ((= (- (- v64 (- v1 v64)) (- v64 (- (- v1 v64) v66))) (- v66 v66))))
(78 (paramod 76 (1 1) 77 (1 1 1)) ((= (- v64 (- v64 (- (- v1 v64) v66))) (- v66 v66))))
(79 (instantiate 78 ((v64 . v0)(v66 . v2))) ((= (- v0 (- v0 (- (- v1 v0) v2))) (- v2 v2))))
(80 (instantiate 60 ((v0 . (- v65 v64)))) ((= (- (- v65 v64) (- v1 (- v1 (- v65 v64)))) (- (- v65 v64) v1))))
(81 (instantiate 79 ((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)))))))
(82 (paramod 80 (1 1) 81 (1 1 2 2)) ((= (- v64 (- v64 (- (- v65 v64) v1))) (- (- v1 (- v1 (- v65 v64))) (- v1 (- v1 (- v65 v64)))))))
(83 (instantiate 15 ((v0 . v1)(v1 . (- v1 (- v65 v64))))) ((= (- (- v1 (- v1 (- v65 v64))) (- v1 (- v1 (- v65 v64)))) (- (- v1 (- v65 v64)) (- v1 (- v65 v64))))))
(84 (paramod 83 (1 1) 82 (1 2)) ((= (- v64 (- v64 (- (- v65 v64) v1))) (- (- v1 (- v65 v64)) (- v1 (- v65 v64))))))
(85 (instantiate 15 ((v0 . v1)(v1 . (- v65 v64)))) ((= (- (- v1 (- v65 v64)) (- v1 (- v65 v64))) (- (- v65 v64) (- v65 v64)))))
(86 (paramod 85 (1 1) 84 (1 2)) ((= (- v64 (- v64 (- (- v65 v64) v1))) (- (- v65 v64) (- v65 v64)))))
(87 (instantiate 15 ((v0 . v65)(v1 . v64))) ((= (- (- v65 v64) (- v65 v64)) (- v64 v64))))
(88 (paramod 87 (1 1) 86 (1 2)) ((= (- v64 (- v64 (- (- v65 v64) v1))) (- v64 v64))))
(89 (instantiate 88 ((v1 . v2)(v64 . v0)(v65 . v1))) ((= (- v0 (- v0 (- (- v1 v0) v2))) (- v0 v0))))
(90 (instantiate 89 ((v0 . v65))) ((= (- v65 (- v65 (- (- v1 v65) v2))) (- v65 v65))))
(91 (instantiate 60 ((v0 . (- (- v1 v65) v2))(v1 . v65))) ((= (- (- (- v1 v65) v2) (- v65 (- v65 (- (- v1 v65) v2)))) (- (- (- v1 v65) v2) v65))))
(92 (paramod 90 (1 1) 91 (1 1 2)) ((= (- (- (- v1 v65) v2) (- v65 v65)) (- (- (- v1 v65) v2) v65))))
(93 (instantiate 42 ((v0 . (- (- v1 v65) v2))(v1 . v65))) ((= (- (- (- v1 v65) v2) (- v65 v65)) (- (- v1 v65) v2))))
(94 (paramod 93 (1 1) 92 (1 1)) ((= (- (- v1 v65) v2) (- (- (- v1 v65) v2) v65))))
(95 (instantiate 51 ((v0 . v1)(v1 . v65)(v2 . v2))) ((= (- (- (- v1 v65) v2) v65) (- (- v1 v65) (- v2 v65)))))
(96 (paramod 95 (1 1) 94 (1 2)) ((= (- (- v1 v65) v2) (- (- v1 v65) (- v2 v65)))))
(97 (flip 96 (1)) ((= (- (- v1 v65) (- v2 v65)) (- (- v1 v65) v2))))
(98 (instantiate 97 ((v1 . v0)(v65 . v1))) ((= (- (- v0 v1) (- v2 v1)) (- (- v0 v1) v2))))
(99 (instantiate 98 ((v0 . (A))(v1 . (B))(v2 . (C)))) ((= (- (- (A) (B)) (- (C) (B))) (- (- (A) (B)) (C)))))
(100 (resolve 36 (1) 99 (1)) ())
)