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