(set-logic QF_UF)
(set-info :source |
Generating minimum transitivity constraints in P-time for deciding Equality Logic,
Ofer Strichman and Mirron Rozanov,
SMT Workshop 2005.

Translator: Leonardo de Moura. |)
(set-info :smt-lib-version 2.0)
(set-info :category "crafted")
(set-info :status unsat)
(declare-sort U 0)
(declare-fun x0 () U)
(declare-fun y0 () U)
(declare-fun z0 () U)
(declare-fun x1 () U)
(declare-fun y1 () U)
(declare-fun z1 () U)
(declare-fun x2 () U)
(declare-fun y2 () U)
(declare-fun z2 () U)
(declare-fun x3 () U)
(declare-fun y3 () U)
(declare-fun z3 () U)
(declare-fun x4 () U)
(declare-fun y4 () U)
(declare-fun z4 () U)
(declare-fun x5 () U)
(declare-fun y5 () U)
(declare-fun z5 () U)
(declare-fun x6 () U)
(declare-fun y6 () U)
(declare-fun z6 () U)
(declare-fun x7 () U)
(declare-fun y7 () U)
(declare-fun z7 () U)
(declare-fun x8 () U)
(declare-fun y8 () U)
(declare-fun z8 () U)
(declare-fun x9 () U)
(declare-fun y9 () U)
(declare-fun z9 () U)
(declare-fun x10 () U)
(declare-fun y10 () U)
(declare-fun z10 () U)
(declare-fun x11 () U)
(declare-fun y11 () U)
(declare-fun z11 () U)
(declare-fun x12 () U)
(declare-fun y12 () U)
(declare-fun z12 () U)
(declare-fun x13 () U)
(declare-fun y13 () U)
(declare-fun z13 () U)
(declare-fun x14 () U)
(declare-fun y14 () U)
(declare-fun z14 () U)
(declare-fun x15 () U)
(declare-fun y15 () U)
(declare-fun z15 () U)
(declare-fun x16 () U)
(declare-fun y16 () U)
(declare-fun z16 () U)
(declare-fun x17 () U)
(declare-fun y17 () U)
(declare-fun z17 () U)
(declare-fun x18 () U)
(declare-fun y18 () U)
(declare-fun z18 () U)
(declare-fun x19 () U)
(declare-fun y19 () U)
(declare-fun z19 () U)
(declare-fun x20 () U)
(declare-fun y20 () U)
(declare-fun z20 () U)
(declare-fun x21 () U)
(declare-fun y21 () U)
(declare-fun z21 () U)
(declare-fun x22 () U)
(declare-fun y22 () U)
(declare-fun z22 () U)
(declare-fun x23 () U)
(declare-fun y23 () U)
(declare-fun z23 () U)
(declare-fun x24 () U)
(declare-fun y24 () U)
(declare-fun z24 () U)
(declare-fun x25 () U)
(declare-fun y25 () U)
(declare-fun z25 () U)
(declare-fun x26 () U)
(declare-fun y26 () U)
(declare-fun z26 () U)
(declare-fun x27 () U)
(declare-fun y27 () U)
(declare-fun z27 () U)
(declare-fun x28 () U)
(declare-fun y28 () U)
(declare-fun z28 () U)
(declare-fun x29 () U)
(declare-fun y29 () U)
(declare-fun z29 () U)
(declare-fun x30 () U)
(declare-fun y30 () U)
(declare-fun z30 () U)
(declare-fun x31 () U)
(declare-fun y31 () U)
(declare-fun z31 () U)
(declare-fun x32 () U)
(declare-fun y32 () U)
(declare-fun z32 () U)
(declare-fun x33 () U)
(declare-fun y33 () U)
(declare-fun z33 () U)
(declare-fun x34 () U)
(declare-fun y34 () U)
(declare-fun z34 () U)
(declare-fun x35 () U)
(declare-fun y35 () U)
(declare-fun z35 () U)
(declare-fun x36 () U)
(declare-fun y36 () U)
(declare-fun z36 () U)
(assert
  (and (or (and (= x0 y0) (= y0 x1)) (and (= x0 z0) (= z0 x1)))
  (and (or (and (= x1 y1) (= y1 x2)) (and (= x1 z1) (= z1 x2)))
  (and (or (and (= x2 y2) (= y2 x3)) (and (= x2 z2) (= z2 x3)))
  (and (or (and (= x3 y3) (= y3 x4)) (and (= x3 z3) (= z3 x4)))
  (and (or (and (= x4 y4) (= y4 x5)) (and (= x4 z4) (= z4 x5)))
  (and (or (and (= x5 y5) (= y5 x6)) (and (= x5 z5) (= z5 x6)))
  (and (or (and (= x6 y6) (= y6 x7)) (and (= x6 z6) (= z6 x7)))
  (and (or (and (= x7 y7) (= y7 x8)) (and (= x7 z7) (= z7 x8)))
  (and (or (and (= x8 y8) (= y8 x9)) (and (= x8 z8) (= z8 x9)))
  (and (or (and (= x9 y9) (= y9 x10)) (and (= x9 z9) (= z9 x10)))
  (and (or (and (= x10 y10) (= y10 x11)) (and (= x10 z10) (= z10 x11)))
  (and (or (and (= x11 y11) (= y11 x12)) (and (= x11 z11) (= z11 x12)))
  (and (or (and (= x12 y12) (= y12 x13)) (and (= x12 z12) (= z12 x13)))
  (and (or (and (= x13 y13) (= y13 x14)) (and (= x13 z13) (= z13 x14)))
  (and (or (and (= x14 y14) (= y14 x15)) (and (= x14 z14) (= z14 x15)))
  (and (or (and (= x15 y15) (= y15 x16)) (and (= x15 z15) (= z15 x16)))
  (and (or (and (= x16 y16) (= y16 x17)) (and (= x16 z16) (= z16 x17)))
  (and (or (and (= x17 y17) (= y17 x18)) (and (= x17 z17) (= z17 x18)))
  (and (or (and (= x18 y18) (= y18 x19)) (and (= x18 z18) (= z18 x19)))
  (and (or (and (= x19 y19) (= y19 x20)) (and (= x19 z19) (= z19 x20)))
  (and (or (and (= x20 y20) (= y20 x21)) (and (= x20 z20) (= z20 x21)))
  (and (or (and (= x21 y21) (= y21 x22)) (and (= x21 z21) (= z21 x22)))
  (and (or (and (= x22 y22) (= y22 x23)) (and (= x22 z22) (= z22 x23)))
  (and (or (and (= x23 y23) (= y23 x24)) (and (= x23 z23) (= z23 x24)))
  (and (or (and (= x24 y24) (= y24 x25)) (and (= x24 z24) (= z24 x25)))
  (and (or (and (= x25 y25) (= y25 x26)) (and (= x25 z25) (= z25 x26)))
  (and (or (and (= x26 y26) (= y26 x27)) (and (= x26 z26) (= z26 x27)))
  (and (or (and (= x27 y27) (= y27 x28)) (and (= x27 z27) (= z27 x28)))
  (and (or (and (= x28 y28) (= y28 x29)) (and (= x28 z28) (= z28 x29)))
  (and (or (and (= x29 y29) (= y29 x30)) (and (= x29 z29) (= z29 x30)))
  (and (or (and (= x30 y30) (= y30 x31)) (and (= x30 z30) (= z30 x31)))
  (and (or (and (= x31 y31) (= y31 x32)) (and (= x31 z31) (= z31 x32)))
  (and (or (and (= x32 y32) (= y32 x33)) (and (= x32 z32) (= z32 x33)))
  (and (or (and (= x33 y33) (= y33 x34)) (and (= x33 z33) (= z33 x34)))
  (and (or (and (= x34 y34) (= y34 x35)) (and (= x34 z34) (= z34 x35)))
  (and (or (and (= x35 y35) (= y35 x36)) (and (= x35 z35) (= z35 x36)))
       (not (= x0 x36)))))))))))))))))))))))))))))))))))))))
(check-sat)
(exit)