;; ----- Otter 3.0.4, August 1995 -----
;; The job was started by mccune on gyro, Wed Nov  1 22:03:26 1995
;;
;;;; x=x.
;;;; x^x=x.
;;;; x^y=y^x.
;;;; (x^y)^z=x^ (y^z).
;;;; x v x=x.
;;;; x v y=y v x.
;;;; (x v y) v z=x v (y v z).
;;;; x^ (x v y)=x.
;;;; x v (x^y)=x.
;;;; x^ (y v z)= (x^y) v (x^z).
;;;; A v (B^C)!= (A v B)^ (A v C).
;;
;; ----> UNIT CONFLICT at   4.08 sec ----> 818 [binary,816.1,145.1] $F.
;;
(
(1 (input) ((= (^ v0 v1) (^ v1 v0))))
(2 (input) ((= (^ (^ v0 v1) v2) (^ v0 (^ v1 v2)))))
(3 (input) ((= (v v0 v1) (v v1 v0))))
(4 (input) ((= (v (v v0 v1) v2) (v v0 (v v1 v2)))))
(5 (input) ((= (^ v0 (v v0 v1)) v0)))
(6 (input) ((= (v v0 (^ v0 v1)) v0)))
(7 (input) ((= (^ v0 (v v1 v2)) (v (^ v0 v1) (^ v0 v2)))))
(8 (flip 7 (1)) ((= (v (^ v0 v1) (^ v0 v2)) (^ v0 (v v1 v2)))))
(9 (input) ((not (= (v (A) (^ (B) (C))) (^ (v (A) (B)) (v (A) (C)))))))
(10 (instantiate 3 ((v0 . v64)(v1 . v65))) ((= (v v64 v65) (v v65 v64))))
(11 (instantiate 5 ((v0 . v64)(v1 . v65))) ((= (^ v64 (v v64 v65)) v64)))
(12 (paramod 10 (1 1) 11 (1 1 2)) ((= (^ v64 (v v65 v64)) v64)))
(13 (instantiate 12 ((v64 . v0)(v65 . v1))) ((= (^ v0 (v v1 v0)) v0)))
(14 (instantiate 1 ((v0 . v64)(v1 . (v v64 v65)))) ((= (^ v64 (v v64 v65)) (^ (v v64 v65) v64))))
(15 (instantiate 5 ((v0 . v64)(v1 . v65))) ((= (^ v64 (v v64 v65)) v64)))
(16 (paramod 14 (1 1) 15 (1 1)) ((= (^ (v v64 v65) v64) v64)))
(17 (instantiate 16 ((v64 . v0)(v65 . v1))) ((= (^ (v v0 v1) v0) v0)))
(18 (instantiate 1 ((v0 . v64)(v1 . v65))) ((= (^ v64 v65) (^ v65 v64))))
(19 (instantiate 6 ((v0 . v64)(v1 . v65))) ((= (v v64 (^ v64 v65)) v64)))
(20 (paramod 18 (1 1) 19 (1 1 2)) ((= (v v64 (^ v65 v64)) v64)))
(21 (instantiate 20 ((v64 . v0)(v65 . v1))) ((= (v v0 (^ v1 v0)) v0)))
(22 (instantiate 6 ((v0 . v65))) ((= (v v65 (^ v65 v1)) v65)))
(23 (instantiate 13 ((v0 . (^ v65 v1))(v1 . v65))) ((= (^ (^ v65 v1) (v v65 (^ v65 v1))) (^ v65 v1))))
(24 (paramod 22 (1 1) 23 (1 1 2)) ((= (^ (^ v65 v1) v65) (^ v65 v1))))
(25 (instantiate 2 ((v0 . v65)(v1 . v1)(v2 . v65))) ((= (^ (^ v65 v1) v65) (^ v65 (^ v1 v65)))))
(26 (paramod 25 (1 1) 24 (1 1)) ((= (^ v65 (^ v1 v65)) (^ v65 v1))))
(27 (instantiate 26 ((v65 . v0))) ((= (^ v0 (^ v1 v0)) (^ v0 v1))))
(28 (instantiate 3 ((v0 . v64)(v1 . (^ v65 v64)))) ((= (v v64 (^ v65 v64)) (v (^ v65 v64) v64))))
(29 (instantiate 21 ((v0 . v64)(v1 . v65))) ((= (v v64 (^ v65 v64)) v64)))
(30 (paramod 28 (1 1) 29 (1 1)) ((= (v (^ v65 v64) v64) v64)))
(31 (instantiate 30 ((v64 . v1)(v65 . v0))) ((= (v (^ v0 v1) v1) v1)))
(32 (instantiate 21 ((v0 . v64))) ((= (v v64 (^ v1 v64)) v64)))
(33 (instantiate 4 ((v0 . v64)(v1 . (^ v1 v64))(v2 . v66))) ((= (v (v v64 (^ v1 v64)) v66) (v v64 (v (^ v1 v64) v66)))))
(34 (paramod 32 (1 1) 33 (1 1 1)) ((= (v v64 v66) (v v64 (v (^ v1 v64) v66)))))
(35 (flip 34 (1)) ((= (v v64 (v (^ v1 v64) v66)) (v v64 v66))))
(36 (instantiate 35 ((v64 . v0)(v66 . v2))) ((= (v v0 (v (^ v1 v0) v2)) (v v0 v2))))
(37 (instantiate 4 ((v2 . v65))) ((= (v (v v0 v1) v65) (v v0 (v v1 v65)))))
(38 (instantiate 17 ((v0 . (v v0 v1))(v1 . v65))) ((= (^ (v (v v0 v1) v65) (v v0 v1)) (v v0 v1))))
(39 (paramod 37 (1 1) 38 (1 1 1)) ((= (^ (v v0 (v v1 v65)) (v v0 v1)) (v v0 v1))))
(40 (instantiate 39 ((v65 . v2))) ((= (^ (v v0 (v v1 v2)) (v v0 v1)) (v v0 v1))))
(41 (instantiate 17 ((v0 . v65))) ((= (^ (v v65 v1) v65) v65)))
(42 (instantiate 8 ((v0 . (v v65 v1))(v1 . v65)(v2 . v66))) ((= (v (^ (v v65 v1) v65) (^ (v v65 v1) v66)) (^ (v v65 v1) (v v65 v66)))))
(43 (paramod 41 (1 1) 42 (1 1 1)) ((= (v v65 (^ (v v65 v1) v66)) (^ (v v65 v1) (v v65 v66)))))
(44 (instantiate 43 ((v65 . v0)(v66 . v2))) ((= (v v0 (^ (v v0 v1) v2)) (^ (v v0 v1) (v v0 v2)))))
(45 (instantiate 1 ((v0 . (B))(v1 . (C)))) ((= (^ (B) (C)) (^ (C) (B)))))
(46 (paramod 45 (1 1) 9 (1 1 1 2)) ((not (= (v (A) (^ (C) (B))) (^ (v (A) (B)) (v (A) (C)))))))
(47 (instantiate 8 ((v0 . v65)(v1 . v64))) ((= (v (^ v65 v64) (^ v65 v2)) (^ v65 (v v64 v2)))))
(48 (instantiate 36 ((v0 . v64)(v1 . v65)(v2 . (^ v65 v2)))) ((= (v v64 (v (^ v65 v64) (^ v65 v2))) (v v64 (^ v65 v2)))))
(49 (paramod 47 (1 1) 48 (1 1 2)) ((= (v v64 (^ v65 (v v64 v2))) (v v64 (^ v65 v2)))))
(50 (instantiate 49 ((v64 . v0)(v65 . v1))) ((= (v v0 (^ v1 (v v0 v2))) (v v0 (^ v1 v2)))))
(51 (instantiate 31 ((v1 . v66))) ((= (v (^ v0 v66) v66) v66)))
(52 (instantiate 40 ((v0 . v64)(v1 . (^ v0 v66))(v2 . v66))) ((= (^ (v v64 (v (^ v0 v66) v66)) (v v64 (^ v0 v66))) (v v64 (^ v0 v66)))))
(53 (paramod 51 (1 1) 52 (1 1 1 2)) ((= (^ (v v64 v66) (v v64 (^ v0 v66))) (v v64 (^ v0 v66)))))
(54 (instantiate 53 ((v0 . v2)(v64 . v0)(v66 . v1))) ((= (^ (v v0 v1) (v v0 (^ v2 v1))) (v v0 (^ v2 v1)))))
(55 (instantiate 27 ((v0 . (v v64 v65)))) ((= (^ (v v64 v65) (^ v1 (v v64 v65))) (^ (v v64 v65) v1))))
(56 (instantiate 44 ((v0 . v64)(v1 . v65)(v2 . (^ v1 (v v64 v65))))) ((= (v v64 (^ (v v64 v65) (^ v1 (v v64 v65)))) (^ (v v64 v65) (v v64 (^ v1 (v v64 v65)))))))
(57 (paramod 55 (1 1) 56 (1 1 2)) ((= (v v64 (^ (v v64 v65) v1)) (^ (v v64 v65) (v v64 (^ v1 (v v64 v65)))))))
(58 (instantiate 44 ((v0 . v64)(v1 . v65)(v2 . v1))) ((= (v v64 (^ (v v64 v65) v1)) (^ (v v64 v65) (v v64 v1)))))
(59 (paramod 58 (1 1) 57 (1 1)) ((= (^ (v v64 v65) (v v64 v1)) (^ (v v64 v65) (v v64 (^ v1 (v v64 v65)))))))
(60 (instantiate 50 ((v0 . v64)(v1 . v1)(v2 . v65))) ((= (v v64 (^ v1 (v v64 v65))) (v v64 (^ v1 v65)))))
(61 (paramod 60 (1 1) 59 (1 2 2)) ((= (^ (v v64 v65) (v v64 v1)) (^ (v v64 v65) (v v64 (^ v1 v65))))))
(62 (instantiate 54 ((v0 . v64)(v1 . v65)(v2 . v1))) ((= (^ (v v64 v65) (v v64 (^ v1 v65))) (v v64 (^ v1 v65)))))
(63 (paramod 62 (1 1) 61 (1 2)) ((= (^ (v v64 v65) (v v64 v1)) (v v64 (^ v1 v65)))))
(64 (flip 63 (1)) ((= (v v64 (^ v1 v65)) (^ (v v64 v65) (v v64 v1)))))
(65 (instantiate 64 ((v64 . v0)(v65 . v2))) ((= (v v0 (^ v1 v2)) (^ (v v0 v2) (v v0 v1)))))
(66 (instantiate 65 ((v0 . (A))(v1 . (C))(v2 . (B)))) ((= (v (A) (^ (C) (B))) (^ (v (A) (B)) (v (A) (C))))))
(67 (resolve 46 (1) 66 (1)) ())
)