--- /dev/null
+(benchmark NEQ016_size5.smt
+:source {
+CADE ATP System competition. See http://www.cs.miami.edu/~tptp/CASC
+ for more information.
+
+This benchmark was obtained by trying to find a finite model of a first-order
+formula (Albert Oliveras).
+}
+:status unsat
+:category { crafted }
+:difficulty { 0 }
+:logic QF_UF
+:extrapreds ((p2 U))
+:extrafuns ((f1 U U U))
+:extrapreds ((p4 U))
+:extrapreds ((p3 U))
+:extrafuns ((c6 U))
+:extrafuns ((c5 U))
+:extrafuns ((c7 U))
+:extrafuns ((c_0 U))
+:extrafuns ((c_1 U))
+:extrafuns ((c_2 U))
+:extrafuns ((c_3 U))
+:extrafuns ((c_4 U))
+:formula
+( and
+( distinct c_0 c_1 c_2 c_3 c_4 )(or (not (p2 c_0)) (not (p2 c_0)) (p4 (f1 c_0 c_0)) (p3 (f1 c_0 c_0)) )(or (not (p2 c_0)) (not (p2 c_1)) (p4 (f1 c_1 c_0)) (p3 (f1 c_1 c_0)) )(or (not (p2 c_0)) (not (p2 c_2)) (p4 (f1 c_2 c_0)) (p3 (f1 c_2 c_0)) )(or (not (p2 c_0)) (not (p2 c_3)) (p4 (f1 c_3 c_0)) (p3 (f1 c_3 c_0)) )(or (not (p2 c_0)) (not (p2 c_4)) (p4 (f1 c_4 c_0)) (p3 (f1 c_4 c_0)) )(or (not (p2 c_1)) (not (p2 c_0)) (p4 (f1 c_0 c_1)) (p3 (f1 c_0 c_1)) )(or (not (p2 c_1)) (not (p2 c_1)) (p4 (f1 c_1 c_1)) (p3 (f1 c_1 c_1)) )(or (not (p2 c_1)) (not (p2 c_2)) (p4 (f1 c_2 c_1)) (p3 (f1 c_2 c_1)) )(or (not (p2 c_1)) (not (p2 c_3)) (p4 (f1 c_3 c_1)) (p3 (f1 c_3 c_1)) )(or (not (p2 c_1)) (not (p2 c_4)) (p4 (f1 c_4 c_1)) (p3 (f1 c_4 c_1)) )(or (not (p2 c_2)) (not (p2 c_0)) (p4 (f1 c_0 c_2)) (p3 (f1 c_0 c_2)) )(or (not (p2 c_2)) (not (p2 c_1)) (p4 (f1 c_1 c_2)) (p3 (f1 c_1 c_2)) )(or (not (p2 c_2)) (not (p2 c_2)) (p4 (f1 c_2 c_2)) (p3 (f1 c_2 c_2)) )(or (not (p2 c_2)) (not (p2 c_3)) (p4 (f1 c_3 c_2)) (p3 (f1 c_3 c_2)) )(or (not (p2 c_2)) (not (p2 c_4)) (p4 (f1 c_4 c_2)) (p3 (f1 c_4 c_2)) )(or (not (p2 c_3)) (not (p2 c_0)) (p4 (f1 c_0 c_3)) (p3 (f1 c_0 c_3)) )(or (not (p2 c_3)) (not (p2 c_1)) (p4 (f1 c_1 c_3)) (p3 (f1 c_1 c_3)) )(or (not (p2 c_3)) (not (p2 c_2)) (p4 (f1 c_2 c_3)) (p3 (f1 c_2 c_3)) )(or (not (p2 c_3)) (not (p2 c_3)) (p4 (f1 c_3 c_3)) (p3 (f1 c_3 c_3)) )(or (not (p2 c_3)) (not (p2 c_4)) (p4 (f1 c_4 c_3)) (p3 (f1 c_4 c_3)) )(or (not (p2 c_4)) (not (p2 c_0)) (p4 (f1 c_0 c_4)) (p3 (f1 c_0 c_4)) )(or (not (p2 c_4)) (not (p2 c_1)) (p4 (f1 c_1 c_4)) (p3 (f1 c_1 c_4)) )(or (not (p2 c_4)) (not (p2 c_2)) (p4 (f1 c_2 c_4)) (p3 (f1 c_2 c_4)) )(or (not (p2 c_4)) (not (p2 c_3)) (p4 (f1 c_3 c_4)) (p3 (f1 c_3 c_4)) )(or (not (p2 c_4)) (not (p2 c_4)) (p4 (f1 c_4 c_4)) (p3 (f1 c_4 c_4)) )(or (not (p2 c_0)) (not (p3 c_0)) )(or (not (p2 c_1)) (not (p3 c_1)) )(or (not (p2 c_2)) (not (p3 c_2)) )(or (not (p2 c_3)) (not (p3 c_3)) )(or (not (p2 c_4)) (not (p3 c_4)) )(or (p4 c_0) (p3 c_0) (p2 c_0) )(or (p4 c_1) (p3 c_1) (p2 c_1) )(or (p4 c_2) (p3 c_2) (p2 c_2) )(or (p4 c_3) (p3 c_3) (p2 c_3) )(or (p4 c_4) (p3 c_4) (p2 c_4) )(p3 c6) (p2 c5) (or (not (p4 c_0)) (not (p4 c_0)) (p2 (f1 c_0 c_0)) )(or (not (p4 c_0)) (not (p4 c_1)) (p2 (f1 c_1 c_0)) )(or (not (p4 c_0)) (not (p4 c_2)) (p2 (f1 c_2 c_0)) )(or (not (p4 c_0)) (not (p4 c_3)) (p2 (f1 c_3 c_0)) )(or (not (p4 c_0)) (not (p4 c_4)) (p2 (f1 c_4 c_0)) )(or (not (p4 c_1)) (not (p4 c_0)) (p2 (f1 c_0 c_1)) )(or (not (p4 c_1)) (not (p4 c_1)) (p2 (f1 c_1 c_1)) )(or (not (p4 c_1)) (not (p4 c_2)) (p2 (f1 c_2 c_1)) )(or (not (p4 c_1)) (not (p4 c_3)) (p2 (f1 c_3 c_1)) )(or (not (p4 c_1)) (not (p4 c_4)) (p2 (f1 c_4 c_1)) )(or (not (p4 c_2)) (not (p4 c_0)) (p2 (f1 c_0 c_2)) )(or (not (p4 c_2)) (not (p4 c_1)) (p2 (f1 c_1 c_2)) )(or (not (p4 c_2)) (not (p4 c_2)) (p2 (f1 c_2 c_2)) )(or (not (p4 c_2)) (not (p4 c_3)) (p2 (f1 c_3 c_2)) )(or (not (p4 c_2)) (not (p4 c_4)) (p2 (f1 c_4 c_2)) )(or (not (p4 c_3)) (not (p4 c_0)) (p2 (f1 c_0 c_3)) )(or (not (p4 c_3)) (not (p4 c_1)) (p2 (f1 c_1 c_3)) )(or (not (p4 c_3)) (not (p4 c_2)) (p2 (f1 c_2 c_3)) )(or (not (p4 c_3)) (not (p4 c_3)) (p2 (f1 c_3 c_3)) )(or (not (p4 c_3)) (not (p4 c_4)) (p2 (f1 c_4 c_3)) )(or (not (p4 c_4)) (not (p4 c_0)) (p2 (f1 c_0 c_4)) )(or (not (p4 c_4)) (not (p4 c_1)) (p2 (f1 c_1 c_4)) )(or (not (p4 c_4)) (not (p4 c_2)) (p2 (f1 c_2 c_4)) )(or (not (p4 c_4)) (not (p4 c_3)) (p2 (f1 c_3 c_4)) )(or (not (p4 c_4)) (not (p4 c_4)) (p2 (f1 c_4 c_4)) )(= (f1 c_0 (f1 c_0 c_0)) (f1 (f1 c_0 c_0) c_0)) (= (f1 c_0 (f1 c_0 c_1)) (f1 (f1 c_0 c_0) c_1)) (= (f1 c_0 (f1 c_0 c_2)) (f1 (f1 c_0 c_0) c_2)) (= (f1 c_0 (f1 c_0 c_3)) (f1 (f1 c_0 c_0) c_3)) (= (f1 c_0 (f1 c_0 c_4)) (f1 (f1 c_0 c_0) c_4)) (= (f1 c_0 (f1 c_1 c_0)) (f1 (f1 c_0 c_1) c_0)) (= (f1 c_0 (f1 c_1 c_1)) (f1 (f1 c_0 c_1) c_1)) (= (f1 c_0 (f1 c_1 c_2)) (f1 (f1 c_0 c_1) c_2)) (= (f1 c_0 (f1 c_1 c_3)) (f1 (f1 c_0 c_1) c_3)) (= (f1 c_0 (f1 c_1 c_4)) (f1 (f1 c_0 c_1) c_4)) (= (f1 c_0 (f1 c_2 c_0)) (f1 (f1 c_0 c_2) c_0)) (= (f1 c_0 (f1 c_2 c_1)) (f1 (f1 c_0 c_2) c_1)) (= (f1 c_0 (f1 c_2 c_2)) (f1 (f1 c_0 c_2) c_2)) (= (f1 c_0 (f1 c_2 c_3)) (f1 (f1 c_0 c_2) c_3)) (= (f1 c_0 (f1 c_2 c_4)) (f1 (f1 c_0 c_2) c_4)) (= (f1 c_0 (f1 c_3 c_0)) (f1 (f1 c_0 c_3) c_0)) (= (f1 c_0 (f1 c_3 c_1)) (f1 (f1 c_0 c_3) c_1)) (= (f1 c_0 (f1 c_3 c_2)) (f1 (f1 c_0 c_3) c_2)) (= (f1 c_0 (f1 c_3 c_3)) (f1 (f1 c_0 c_3) c_3)) (= (f1 c_0 (f1 c_3 c_4)) (f1 (f1 c_0 c_3) c_4)) (= (f1 c_0 (f1 c_4 c_0)) (f1 (f1 c_0 c_4) c_0)) (= (f1 c_0 (f1 c_4 c_1)) (f1 (f1 c_0 c_4) c_1)) (= (f1 c_0 (f1 c_4 c_2)) (f1 (f1 c_0 c_4) c_2)) (= (f1 c_0 (f1 c_4 c_3)) (f1 (f1 c_0 c_4) c_3)) (= (f1 c_0 (f1 c_4 c_4)) (f1 (f1 c_0 c_4) c_4)) (= (f1 c_1 (f1 c_0 c_0)) (f1 (f1 c_1 c_0) c_0)) (= (f1 c_1 (f1 c_0 c_1)) (f1 (f1 c_1 c_0) c_1)) (= (f1 c_1 (f1 c_0 c_2)) (f1 (f1 c_1 c_0) c_2)) (= (f1 c_1 (f1 c_0 c_3)) (f1 (f1 c_1 c_0) c_3)) (= (f1 c_1 (f1 c_0 c_4)) (f1 (f1 c_1 c_0) c_4)) (= (f1 c_1 (f1 c_1 c_0)) (f1 (f1 c_1 c_1) c_0)) (= (f1 c_1 (f1 c_1 c_1)) (f1 (f1 c_1 c_1) c_1)) (= (f1 c_1 (f1 c_1 c_2)) (f1 (f1 c_1 c_1) c_2)) (= (f1 c_1 (f1 c_1 c_3)) (f1 (f1 c_1 c_1) c_3)) (= (f1 c_1 (f1 c_1 c_4)) (f1 (f1 c_1 c_1) c_4)) (= (f1 c_1 (f1 c_2 c_0)) (f1 (f1 c_1 c_2) c_0)) (= (f1 c_1 (f1 c_2 c_1)) (f1 (f1 c_1 c_2) c_1)) (= (f1 c_1 (f1 c_2 c_2)) (f1 (f1 c_1 c_2) c_2)) (= (f1 c_1 (f1 c_2 c_3)) (f1 (f1 c_1 c_2) c_3)) (= (f1 c_1 (f1 c_2 c_4)) (f1 (f1 c_1 c_2) c_4)) (= (f1 c_1 (f1 c_3 c_0)) (f1 (f1 c_1 c_3) c_0)) (= (f1 c_1 (f1 c_3 c_1)) (f1 (f1 c_1 c_3) c_1)) (= (f1 c_1 (f1 c_3 c_2)) (f1 (f1 c_1 c_3) c_2)) (= (f1 c_1 (f1 c_3 c_3)) (f1 (f1 c_1 c_3) c_3)) (= (f1 c_1 (f1 c_3 c_4)) (f1 (f1 c_1 c_3) c_4)) (= (f1 c_1 (f1 c_4 c_0)) (f1 (f1 c_1 c_4) c_0)) (= (f1 c_1 (f1 c_4 c_1)) (f1 (f1 c_1 c_4) c_1)) (= (f1 c_1 (f1 c_4 c_2)) (f1 (f1 c_1 c_4) c_2)) (= (f1 c_1 (f1 c_4 c_3)) (f1 (f1 c_1 c_4) c_3)) (= (f1 c_1 (f1 c_4 c_4)) (f1 (f1 c_1 c_4) c_4)) (= (f1 c_2 (f1 c_0 c_0)) (f1 (f1 c_2 c_0) c_0)) (= (f1 c_2 (f1 c_0 c_1)) (f1 (f1 c_2 c_0) c_1)) (= (f1 c_2 (f1 c_0 c_2)) (f1 (f1 c_2 c_0) c_2)) (= (f1 c_2 (f1 c_0 c_3)) (f1 (f1 c_2 c_0) c_3)) (= (f1 c_2 (f1 c_0 c_4)) (f1 (f1 c_2 c_0) c_4)) (= (f1 c_2 (f1 c_1 c_0)) (f1 (f1 c_2 c_1) c_0)) (= (f1 c_2 (f1 c_1 c_1)) (f1 (f1 c_2 c_1) c_1)) (= (f1 c_2 (f1 c_1 c_2)) (f1 (f1 c_2 c_1) c_2)) (= (f1 c_2 (f1 c_1 c_3)) (f1 (f1 c_2 c_1) c_3)) (= (f1 c_2 (f1 c_1 c_4)) (f1 (f1 c_2 c_1) c_4)) (= (f1 c_2 (f1 c_2 c_0)) (f1 (f1 c_2 c_2) c_0)) (= (f1 c_2 (f1 c_2 c_1)) (f1 (f1 c_2 c_2) c_1)) (= (f1 c_2 (f1 c_2 c_2)) (f1 (f1 c_2 c_2) c_2)) (= (f1 c_2 (f1 c_2 c_3)) (f1 (f1 c_2 c_2) c_3)) (= (f1 c_2 (f1 c_2 c_4)) (f1 (f1 c_2 c_2) c_4)) (= (f1 c_2 (f1 c_3 c_0)) (f1 (f1 c_2 c_3) c_0)) (= (f1 c_2 (f1 c_3 c_1)) (f1 (f1 c_2 c_3) c_1)) (= (f1 c_2 (f1 c_3 c_2)) (f1 (f1 c_2 c_3) c_2)) (= (f1 c_2 (f1 c_3 c_3)) (f1 (f1 c_2 c_3) c_3)) (= (f1 c_2 (f1 c_3 c_4)) (f1 (f1 c_2 c_3) c_4)) (= (f1 c_2 (f1 c_4 c_0)) (f1 (f1 c_2 c_4) c_0)) (= (f1 c_2 (f1 c_4 c_1)) (f1 (f1 c_2 c_4) c_1)) (= (f1 c_2 (f1 c_4 c_2)) (f1 (f1 c_2 c_4) c_2)) (= (f1 c_2 (f1 c_4 c_3)) (f1 (f1 c_2 c_4) c_3)) (= (f1 c_2 (f1 c_4 c_4)) (f1 (f1 c_2 c_4) c_4)) (= (f1 c_3 (f1 c_0 c_0)) (f1 (f1 c_3 c_0) c_0)) (= (f1 c_3 (f1 c_0 c_1)) (f1 (f1 c_3 c_0) c_1)) (= (f1 c_3 (f1 c_0 c_2)) (f1 (f1 c_3 c_0) c_2)) (= (f1 c_3 (f1 c_0 c_3)) (f1 (f1 c_3 c_0) c_3)) (= (f1 c_3 (f1 c_0 c_4)) (f1 (f1 c_3 c_0) c_4)) (= (f1 c_3 (f1 c_1 c_0)) (f1 (f1 c_3 c_1) c_0)) (= (f1 c_3 (f1 c_1 c_1)) (f1 (f1 c_3 c_1) c_1)) (= (f1 c_3 (f1 c_1 c_2)) (f1 (f1 c_3 c_1) c_2)) (= (f1 c_3 (f1 c_1 c_3)) (f1 (f1 c_3 c_1) c_3)) (= (f1 c_3 (f1 c_1 c_4)) (f1 (f1 c_3 c_1) c_4)) (= (f1 c_3 (f1 c_2 c_0)) (f1 (f1 c_3 c_2) c_0)) (= (f1 c_3 (f1 c_2 c_1)) (f1 (f1 c_3 c_2) c_1)) (= (f1 c_3 (f1 c_2 c_2)) (f1 (f1 c_3 c_2) c_2)) (= (f1 c_3 (f1 c_2 c_3)) (f1 (f1 c_3 c_2) c_3)) (= (f1 c_3 (f1 c_2 c_4)) (f1 (f1 c_3 c_2) c_4)) (= (f1 c_3 (f1 c_3 c_0)) (f1 (f1 c_3 c_3) c_0)) (= (f1 c_3 (f1 c_3 c_1)) (f1 (f1 c_3 c_3) c_1)) (= (f1 c_3 (f1 c_3 c_2)) (f1 (f1 c_3 c_3) c_2)) (= (f1 c_3 (f1 c_3 c_3)) (f1 (f1 c_3 c_3) c_3)) (= (f1 c_3 (f1 c_3 c_4)) (f1 (f1 c_3 c_3) c_4)) (= (f1 c_3 (f1 c_4 c_0)) (f1 (f1 c_3 c_4) c_0)) (= (f1 c_3 (f1 c_4 c_1)) (f1 (f1 c_3 c_4) c_1)) (= (f1 c_3 (f1 c_4 c_2)) (f1 (f1 c_3 c_4) c_2)) (= (f1 c_3 (f1 c_4 c_3)) (f1 (f1 c_3 c_4) c_3)) (= (f1 c_3 (f1 c_4 c_4)) (f1 (f1 c_3 c_4) c_4)) (= (f1 c_4 (f1 c_0 c_0)) (f1 (f1 c_4 c_0) c_0)) (= (f1 c_4 (f1 c_0 c_1)) (f1 (f1 c_4 c_0) c_1)) (= (f1 c_4 (f1 c_0 c_2)) (f1 (f1 c_4 c_0) c_2)) (= (f1 c_4 (f1 c_0 c_3)) (f1 (f1 c_4 c_0) c_3)) (= (f1 c_4 (f1 c_0 c_4)) (f1 (f1 c_4 c_0) c_4)) (= (f1 c_4 (f1 c_1 c_0)) (f1 (f1 c_4 c_1) c_0)) (= (f1 c_4 (f1 c_1 c_1)) (f1 (f1 c_4 c_1) c_1)) (= (f1 c_4 (f1 c_1 c_2)) (f1 (f1 c_4 c_1) c_2)) (= (f1 c_4 (f1 c_1 c_3)) (f1 (f1 c_4 c_1) c_3)) (= (f1 c_4 (f1 c_1 c_4)) (f1 (f1 c_4 c_1) c_4)) (= (f1 c_4 (f1 c_2 c_0)) (f1 (f1 c_4 c_2) c_0)) (= (f1 c_4 (f1 c_2 c_1)) (f1 (f1 c_4 c_2) c_1)) (= (f1 c_4 (f1 c_2 c_2)) (f1 (f1 c_4 c_2) c_2)) (= (f1 c_4 (f1 c_2 c_3)) (f1 (f1 c_4 c_2) c_3)) (= (f1 c_4 (f1 c_2 c_4)) (f1 (f1 c_4 c_2) c_4)) (= (f1 c_4 (f1 c_3 c_0)) (f1 (f1 c_4 c_3) c_0)) (= (f1 c_4 (f1 c_3 c_1)) (f1 (f1 c_4 c_3) c_1)) (= (f1 c_4 (f1 c_3 c_2)) (f1 (f1 c_4 c_3) c_2)) (= (f1 c_4 (f1 c_3 c_3)) (f1 (f1 c_4 c_3) c_3)) (= (f1 c_4 (f1 c_3 c_4)) (f1 (f1 c_4 c_3) c_4)) (= (f1 c_4 (f1 c_4 c_0)) (f1 (f1 c_4 c_4) c_0)) (= (f1 c_4 (f1 c_4 c_1)) (f1 (f1 c_4 c_4) c_1)) (= (f1 c_4 (f1 c_4 c_2)) (f1 (f1 c_4 c_4) c_2)) (= (f1 c_4 (f1 c_4 c_3)) (f1 (f1 c_4 c_4) c_3)) (= (f1 c_4 (f1 c_4 c_4)) (f1 (f1 c_4 c_4) c_4)) (or (p2 (f1 c_0 c_0)) (not (p3 c_0)) (not (p3 c_0)) )(or (p2 (f1 c_0 c_1)) (not (p3 c_0)) (not (p3 c_1)) )(or (p2 (f1 c_0 c_2)) (not (p3 c_0)) (not (p3 c_2)) )(or (p2 (f1 c_0 c_3)) (not (p3 c_0)) (not (p3 c_3)) )(or (p2 (f1 c_0 c_4)) (not (p3 c_0)) (not (p3 c_4)) )(or (p2 (f1 c_1 c_0)) (not (p3 c_1)) (not (p3 c_0)) )(or (p2 (f1 c_1 c_1)) (not (p3 c_1)) (not (p3 c_1)) )(or (p2 (f1 c_1 c_2)) (not (p3 c_1)) (not (p3 c_2)) )(or (p2 (f1 c_1 c_3)) (not (p3 c_1)) (not (p3 c_3)) )(or (p2 (f1 c_1 c_4)) (not (p3 c_1)) (not (p3 c_4)) )(or (p2 (f1 c_2 c_0)) (not (p3 c_2)) (not (p3 c_0)) )(or (p2 (f1 c_2 c_1)) (not (p3 c_2)) (not (p3 c_1)) )(or (p2 (f1 c_2 c_2)) (not (p3 c_2)) (not (p3 c_2)) )(or (p2 (f1 c_2 c_3)) (not (p3 c_2)) (not (p3 c_3)) )(or (p2 (f1 c_2 c_4)) (not (p3 c_2)) (not (p3 c_4)) )(or (p2 (f1 c_3 c_0)) (not (p3 c_3)) (not (p3 c_0)) )(or (p2 (f1 c_3 c_1)) (not (p3 c_3)) (not (p3 c_1)) )(or (p2 (f1 c_3 c_2)) (not (p3 c_3)) (not (p3 c_2)) )(or (p2 (f1 c_3 c_3)) (not (p3 c_3)) (not (p3 c_3)) )(or (p2 (f1 c_3 c_4)) (not (p3 c_3)) (not (p3 c_4)) )(or (p2 (f1 c_4 c_0)) (not (p3 c_4)) (not (p3 c_0)) )(or (p2 (f1 c_4 c_1)) (not (p3 c_4)) (not (p3 c_1)) )(or (p2 (f1 c_4 c_2)) (not (p3 c_4)) (not (p3 c_2)) )(or (p2 (f1 c_4 c_3)) (not (p3 c_4)) (not (p3 c_3)) )(or (p2 (f1 c_4 c_4)) (not (p3 c_4)) (not (p3 c_4)) )(p4 c7) (or (not (p4 c_0)) (not (p2 c_0)) )(or (not (p4 c_1)) (not (p2 c_1)) )(or (not (p4 c_2)) (not (p2 c_2)) )(or (not (p4 c_3)) (not (p2 c_3)) )(or (not (p4 c_4)) (not (p2 c_4)) )(or (not (p3 c_0)) (not (p4 c_0)) )(or (not (p3 c_1)) (not (p4 c_1)) )(or (not (p3 c_2)) (not (p4 c_2)) )(or (not (p3 c_3)) (not (p4 c_3)) )(or (not (p3 c_4)) (not (p4 c_4)) )(or (= (f1 c_0 c_0) c_0)(= (f1 c_0 c_0) c_1)(= (f1 c_0 c_0) c_2)(= (f1 c_0 c_0) c_3)(= (f1 c_0 c_0) c_4))(or (= (f1 c_0 c_1) c_0)(= (f1 c_0 c_1) c_1)(= (f1 c_0 c_1) c_2)(= (f1 c_0 c_1) c_3)(= (f1 c_0 c_1) c_4))(or (= (f1 c_0 c_2) c_0)(= (f1 c_0 c_2) c_1)(= (f1 c_0 c_2) c_2)(= (f1 c_0 c_2) c_3)(= (f1 c_0 c_2) c_4))(or (= (f1 c_0 c_3) c_0)(= (f1 c_0 c_3) c_1)(= (f1 c_0 c_3) c_2)(= (f1 c_0 c_3) c_3)(= (f1 c_0 c_3) c_4))(or (= (f1 c_0 c_4) c_0)(= (f1 c_0 c_4) c_1)(= (f1 c_0 c_4) c_2)(= (f1 c_0 c_4) c_3)(= (f1 c_0 c_4) c_4))(or (= (f1 c_1 c_0) c_0)(= (f1 c_1 c_0) c_1)(= (f1 c_1 c_0) c_2)(= (f1 c_1 c_0) c_3)(= (f1 c_1 c_0) c_4))(or (= (f1 c_1 c_1) c_0)(= (f1 c_1 c_1) c_1)(= (f1 c_1 c_1) c_2)(= (f1 c_1 c_1) c_3)(= (f1 c_1 c_1) c_4))(or (= (f1 c_1 c_2) c_0)(= (f1 c_1 c_2) c_1)(= (f1 c_1 c_2) c_2)(= (f1 c_1 c_2) c_3)(= (f1 c_1 c_2) c_4))(or (= (f1 c_1 c_3) c_0)(= (f1 c_1 c_3) c_1)(= (f1 c_1 c_3) c_2)(= (f1 c_1 c_3) c_3)(= (f1 c_1 c_3) c_4))(or (= (f1 c_1 c_4) c_0)(= (f1 c_1 c_4) c_1)(= (f1 c_1 c_4) c_2)(= (f1 c_1 c_4) c_3)(= (f1 c_1 c_4) c_4))(or (= (f1 c_2 c_0) c_0)(= (f1 c_2 c_0) c_1)(= (f1 c_2 c_0) c_2)(= (f1 c_2 c_0) c_3)(= (f1 c_2 c_0) c_4))(or (= (f1 c_2 c_1) c_0)(= (f1 c_2 c_1) c_1)(= (f1 c_2 c_1) c_2)(= (f1 c_2 c_1) c_3)(= (f1 c_2 c_1) c_4))(or (= (f1 c_2 c_2) c_0)(= (f1 c_2 c_2) c_1)(= (f1 c_2 c_2) c_2)(= (f1 c_2 c_2) c_3)(= (f1 c_2 c_2) c_4))(or (= (f1 c_2 c_3) c_0)(= (f1 c_2 c_3) c_1)(= (f1 c_2 c_3) c_2)(= (f1 c_2 c_3) c_3)(= (f1 c_2 c_3) c_4))(or (= (f1 c_2 c_4) c_0)(= (f1 c_2 c_4) c_1)(= (f1 c_2 c_4) c_2)(= (f1 c_2 c_4) c_3)(= (f1 c_2 c_4) c_4))(or (= (f1 c_3 c_0) c_0)(= (f1 c_3 c_0) c_1)(= (f1 c_3 c_0) c_2)(= (f1 c_3 c_0) c_3)(= (f1 c_3 c_0) c_4))(or (= (f1 c_3 c_1) c_0)(= (f1 c_3 c_1) c_1)(= (f1 c_3 c_1) c_2)(= (f1 c_3 c_1) c_3)(= (f1 c_3 c_1) c_4))(or (= (f1 c_3 c_2) c_0)(= (f1 c_3 c_2) c_1)(= (f1 c_3 c_2) c_2)(= (f1 c_3 c_2) c_3)(= (f1 c_3 c_2) c_4))(or (= (f1 c_3 c_3) c_0)(= (f1 c_3 c_3) c_1)(= (f1 c_3 c_3) c_2)(= (f1 c_3 c_3) c_3)(= (f1 c_3 c_3) c_4))(or (= (f1 c_3 c_4) c_0)(= (f1 c_3 c_4) c_1)(= (f1 c_3 c_4) c_2)(= (f1 c_3 c_4) c_3)(= (f1 c_3 c_4) c_4))(or (= (f1 c_4 c_0) c_0)(= (f1 c_4 c_0) c_1)(= (f1 c_4 c_0) c_2)(= (f1 c_4 c_0) c_3)(= (f1 c_4 c_0) c_4))(or (= (f1 c_4 c_1) c_0)(= (f1 c_4 c_1) c_1)(= (f1 c_4 c_1) c_2)(= (f1 c_4 c_1) c_3)(= (f1 c_4 c_1) c_4))(or (= (f1 c_4 c_2) c_0)(= (f1 c_4 c_2) c_1)(= (f1 c_4 c_2) c_2)(= (f1 c_4 c_2) c_3)(= (f1 c_4 c_2) c_4))(or (= (f1 c_4 c_3) c_0)(= (f1 c_4 c_3) c_1)(= (f1 c_4 c_3) c_2)(= (f1 c_4 c_3) c_3)(= (f1 c_4 c_3) c_4))(or (= (f1 c_4 c_4) c_0)(= (f1 c_4 c_4) c_1)(= (f1 c_4 c_4) c_2)(= (f1 c_4 c_4) c_3)(= (f1 c_4 c_4) c_4))(or (= c6 c_0)(= c6 c_1)(= c6 c_2)(= c6 c_3)(= c6 c_4))(or (= c5 c_0)(= c5 c_1)(= c5 c_2)(= c5 c_3)(= c5 c_4))(or (= c7 c_0)(= c7 c_1)(= c7 c_2)(= c7 c_3)(= c7 c_4))))
--- /dev/null
+(benchmark PEQ018_size4.smt
+:source {
+CADE ATP System competition. See http://www.cs.miami.edu/~tptp/CASC
+ for more information.
+
+This benchmark was obtained by trying to find a finite model of a first-order
+formula (Albert Oliveras).
+}
+:status unsat
+:category { crafted }
+:difficulty { 0 }
+:logic QF_UF
+:extrafuns ((f1 U U U))
+:extrafuns ((f2 U U))
+:extrafuns ((c10 U))
+:extrafuns ((c11 U))
+:extrafuns ((c3 U))
+:extrafuns ((c4 U))
+:extrafuns ((c5 U))
+:extrafuns ((c6 U))
+:extrafuns ((c7 U))
+:extrafuns ((c8 U))
+:extrafuns ((c9 U))
+:extrafuns ((c_0 U))
+:extrafuns ((c_1 U))
+:extrafuns ((c_2 U))
+:extrafuns ((c_3 U))
+:formula
+( and
+( distinct c_0 c_1 c_2 c_3 )(= (f1 c_0 (f1 (f1 c_0 c_0) (f2 (f1 c_0 c_0)))) c_0) (= (f1 c_0 (f1 (f1 c_0 c_1) (f2 (f1 c_0 c_1)))) c_0) (= (f1 c_0 (f1 (f1 c_0 c_2) (f2 (f1 c_0 c_2)))) c_0) (= (f1 c_0 (f1 (f1 c_0 c_3) (f2 (f1 c_0 c_3)))) c_0) (= (f1 c_0 (f1 (f1 c_1 c_0) (f2 (f1 c_0 c_0)))) c_1) (= (f1 c_0 (f1 (f1 c_1 c_1) (f2 (f1 c_0 c_1)))) c_1) (= (f1 c_0 (f1 (f1 c_1 c_2) (f2 (f1 c_0 c_2)))) c_1) (= (f1 c_0 (f1 (f1 c_1 c_3) (f2 (f1 c_0 c_3)))) c_1) (= (f1 c_0 (f1 (f1 c_2 c_0) (f2 (f1 c_0 c_0)))) c_2) (= (f1 c_0 (f1 (f1 c_2 c_1) (f2 (f1 c_0 c_1)))) c_2) (= (f1 c_0 (f1 (f1 c_2 c_2) (f2 (f1 c_0 c_2)))) c_2) (= (f1 c_0 (f1 (f1 c_2 c_3) (f2 (f1 c_0 c_3)))) c_2) (= (f1 c_0 (f1 (f1 c_3 c_0) (f2 (f1 c_0 c_0)))) c_3) (= (f1 c_0 (f1 (f1 c_3 c_1) (f2 (f1 c_0 c_1)))) c_3) (= (f1 c_0 (f1 (f1 c_3 c_2) (f2 (f1 c_0 c_2)))) c_3) (= (f1 c_0 (f1 (f1 c_3 c_3) (f2 (f1 c_0 c_3)))) c_3) (= (f1 c_1 (f1 (f1 c_0 c_0) (f2 (f1 c_1 c_0)))) c_0) (= (f1 c_1 (f1 (f1 c_0 c_1) (f2 (f1 c_1 c_1)))) c_0) (= (f1 c_1 (f1 (f1 c_0 c_2) (f2 (f1 c_1 c_2)))) c_0) (= (f1 c_1 (f1 (f1 c_0 c_3) (f2 (f1 c_1 c_3)))) c_0) (= (f1 c_1 (f1 (f1 c_1 c_0) (f2 (f1 c_1 c_0)))) c_1) (= (f1 c_1 (f1 (f1 c_1 c_1) (f2 (f1 c_1 c_1)))) c_1) (= (f1 c_1 (f1 (f1 c_1 c_2) (f2 (f1 c_1 c_2)))) c_1) (= (f1 c_1 (f1 (f1 c_1 c_3) (f2 (f1 c_1 c_3)))) c_1) (= (f1 c_1 (f1 (f1 c_2 c_0) (f2 (f1 c_1 c_0)))) c_2) (= (f1 c_1 (f1 (f1 c_2 c_1) (f2 (f1 c_1 c_1)))) c_2) (= (f1 c_1 (f1 (f1 c_2 c_2) (f2 (f1 c_1 c_2)))) c_2) (= (f1 c_1 (f1 (f1 c_2 c_3) (f2 (f1 c_1 c_3)))) c_2) (= (f1 c_1 (f1 (f1 c_3 c_0) (f2 (f1 c_1 c_0)))) c_3) (= (f1 c_1 (f1 (f1 c_3 c_1) (f2 (f1 c_1 c_1)))) c_3) (= (f1 c_1 (f1 (f1 c_3 c_2) (f2 (f1 c_1 c_2)))) c_3) (= (f1 c_1 (f1 (f1 c_3 c_3) (f2 (f1 c_1 c_3)))) c_3) (= (f1 c_2 (f1 (f1 c_0 c_0) (f2 (f1 c_2 c_0)))) c_0) (= (f1 c_2 (f1 (f1 c_0 c_1) (f2 (f1 c_2 c_1)))) c_0) (= (f1 c_2 (f1 (f1 c_0 c_2) (f2 (f1 c_2 c_2)))) c_0) (= (f1 c_2 (f1 (f1 c_0 c_3) (f2 (f1 c_2 c_3)))) c_0) (= (f1 c_2 (f1 (f1 c_1 c_0) (f2 (f1 c_2 c_0)))) c_1) (= (f1 c_2 (f1 (f1 c_1 c_1) (f2 (f1 c_2 c_1)))) c_1) (= (f1 c_2 (f1 (f1 c_1 c_2) (f2 (f1 c_2 c_2)))) c_1) (= (f1 c_2 (f1 (f1 c_1 c_3) (f2 (f1 c_2 c_3)))) c_1) (= (f1 c_2 (f1 (f1 c_2 c_0) (f2 (f1 c_2 c_0)))) c_2) (= (f1 c_2 (f1 (f1 c_2 c_1) (f2 (f1 c_2 c_1)))) c_2) (= (f1 c_2 (f1 (f1 c_2 c_2) (f2 (f1 c_2 c_2)))) c_2) (= (f1 c_2 (f1 (f1 c_2 c_3) (f2 (f1 c_2 c_3)))) c_2) (= (f1 c_2 (f1 (f1 c_3 c_0) (f2 (f1 c_2 c_0)))) c_3) (= (f1 c_2 (f1 (f1 c_3 c_1) (f2 (f1 c_2 c_1)))) c_3) (= (f1 c_2 (f1 (f1 c_3 c_2) (f2 (f1 c_2 c_2)))) c_3) (= (f1 c_2 (f1 (f1 c_3 c_3) (f2 (f1 c_2 c_3)))) c_3) (= (f1 c_3 (f1 (f1 c_0 c_0) (f2 (f1 c_3 c_0)))) c_0) (= (f1 c_3 (f1 (f1 c_0 c_1) (f2 (f1 c_3 c_1)))) c_0) (= (f1 c_3 (f1 (f1 c_0 c_2) (f2 (f1 c_3 c_2)))) c_0) (= (f1 c_3 (f1 (f1 c_0 c_3) (f2 (f1 c_3 c_3)))) c_0) (= (f1 c_3 (f1 (f1 c_1 c_0) (f2 (f1 c_3 c_0)))) c_1) (= (f1 c_3 (f1 (f1 c_1 c_1) (f2 (f1 c_3 c_1)))) c_1) (= (f1 c_3 (f1 (f1 c_1 c_2) (f2 (f1 c_3 c_2)))) c_1) (= (f1 c_3 (f1 (f1 c_1 c_3) (f2 (f1 c_3 c_3)))) c_1) (= (f1 c_3 (f1 (f1 c_2 c_0) (f2 (f1 c_3 c_0)))) c_2) (= (f1 c_3 (f1 (f1 c_2 c_1) (f2 (f1 c_3 c_1)))) c_2) (= (f1 c_3 (f1 (f1 c_2 c_2) (f2 (f1 c_3 c_2)))) c_2) (= (f1 c_3 (f1 (f1 c_2 c_3) (f2 (f1 c_3 c_3)))) c_2) (= (f1 c_3 (f1 (f1 c_3 c_0) (f2 (f1 c_3 c_0)))) c_3) (= (f1 c_3 (f1 (f1 c_3 c_1) (f2 (f1 c_3 c_1)))) c_3) (= (f1 c_3 (f1 (f1 c_3 c_2) (f2 (f1 c_3 c_2)))) c_3) (= (f1 c_3 (f1 (f1 c_3 c_3) (f2 (f1 c_3 c_3)))) c_3) (or (not (= (f1 c10 c11) (f1 c11 c10))) (not (= (f1 (f2 c3) c3) (f1 (f2 c4) c4))) (not (= (f1 (f1 (f2 c5) c5) c6) c6)) (not (= (f1 (f1 c7 c8) c9) (f1 c7 (f1 c8 c9)))) )(or (= (f1 c_0 c_0) c_0)(= (f1 c_0 c_0) c_1)(= (f1 c_0 c_0) c_2)(= (f1 c_0 c_0) c_3))(or (= (f1 c_0 c_1) c_0)(= (f1 c_0 c_1) c_1)(= (f1 c_0 c_1) c_2)(= (f1 c_0 c_1) c_3))(or (= (f1 c_0 c_2) c_0)(= (f1 c_0 c_2) c_1)(= (f1 c_0 c_2) c_2)(= (f1 c_0 c_2) c_3))(or (= (f1 c_0 c_3) c_0)(= (f1 c_0 c_3) c_1)(= (f1 c_0 c_3) c_2)(= (f1 c_0 c_3) c_3))(or (= (f1 c_1 c_0) c_0)(= (f1 c_1 c_0) c_1)(= (f1 c_1 c_0) c_2)(= (f1 c_1 c_0) c_3))(or (= (f1 c_1 c_1) c_0)(= (f1 c_1 c_1) c_1)(= (f1 c_1 c_1) c_2)(= (f1 c_1 c_1) c_3))(or (= (f1 c_1 c_2) c_0)(= (f1 c_1 c_2) c_1)(= (f1 c_1 c_2) c_2)(= (f1 c_1 c_2) c_3))(or (= (f1 c_1 c_3) c_0)(= (f1 c_1 c_3) c_1)(= (f1 c_1 c_3) c_2)(= (f1 c_1 c_3) c_3))(or (= (f1 c_2 c_0) c_0)(= (f1 c_2 c_0) c_1)(= (f1 c_2 c_0) c_2)(= (f1 c_2 c_0) c_3))(or (= (f1 c_2 c_1) c_0)(= (f1 c_2 c_1) c_1)(= (f1 c_2 c_1) c_2)(= (f1 c_2 c_1) c_3))(or (= (f1 c_2 c_2) c_0)(= (f1 c_2 c_2) c_1)(= (f1 c_2 c_2) c_2)(= (f1 c_2 c_2) c_3))(or (= (f1 c_2 c_3) c_0)(= (f1 c_2 c_3) c_1)(= (f1 c_2 c_3) c_2)(= (f1 c_2 c_3) c_3))(or (= (f1 c_3 c_0) c_0)(= (f1 c_3 c_0) c_1)(= (f1 c_3 c_0) c_2)(= (f1 c_3 c_0) c_3))(or (= (f1 c_3 c_1) c_0)(= (f1 c_3 c_1) c_1)(= (f1 c_3 c_1) c_2)(= (f1 c_3 c_1) c_3))(or (= (f1 c_3 c_2) c_0)(= (f1 c_3 c_2) c_1)(= (f1 c_3 c_2) c_2)(= (f1 c_3 c_2) c_3))(or (= (f1 c_3 c_3) c_0)(= (f1 c_3 c_3) c_1)(= (f1 c_3 c_3) c_2)(= (f1 c_3 c_3) c_3))(or (= (f2 c_0) c_0)(= (f2 c_0) c_1)(= (f2 c_0) c_2)(= (f2 c_0) c_3))(or (= (f2 c_1) c_0)(= (f2 c_1) c_1)(= (f2 c_1) c_2)(= (f2 c_1) c_3))(or (= (f2 c_2) c_0)(= (f2 c_2) c_1)(= (f2 c_2) c_2)(= (f2 c_2) c_3))(or (= (f2 c_3) c_0)(= (f2 c_3) c_1)(= (f2 c_3) c_2)(= (f2 c_3) c_3))(or (= c10 c_0)(= c10 c_1)(= c10 c_2)(= c10 c_3))(or (= c11 c_0)(= c11 c_1)(= c11 c_2)(= c11 c_3))(or (= c3 c_0)(= c3 c_1)(= c3 c_2)(= c3 c_3))(or (= c4 c_0)(= c4 c_1)(= c4 c_2)(= c4 c_3))(or (= c5 c_0)(= c5 c_1)(= c5 c_2)(= c5 c_3))(or (= c6 c_0)(= c6 c_1)(= c6 c_2)(= c6 c_3))(or (= c7 c_0)(= c7 c_1)(= c7 c_2)(= c7 c_3))(or (= c8 c_0)(= c8 c_1)(= c8 c_2)(= c8 c_3))(or (= c9 c_0)(= c9 c_1)(= c9 c_2)(= c9 c_3))))
--- /dev/null
+(benchmark SEQ032_size2.smt
+:source {
+CADE ATP System competition. See http://www.cs.miami.edu/~tptp/CASC
+ for more information.
+
+This benchmark was obtained by trying to find a finite model of a first-order
+formula (Albert Oliveras).
+}
+:status unsat
+:category { crafted }
+:difficulty { 0 }
+:logic QF_UF
+:extrafuns ((c3 U))
+:extrafuns ((f1 U U U))
+:extrafuns ((c2 U))
+:extrafuns ((f4 U U))
+:extrafuns ((c_0 U))
+:extrafuns ((c_1 U))
+:formula
+( and
+( distinct c_0 c_1 )(= (f1 (f1 (f1 c3 c_0) c_0) c_0) (f1 c_0 (f1 c_0 c_0))) (= (f1 (f1 (f1 c3 c_0) c_0) c_1) (f1 c_0 (f1 c_0 c_1))) (= (f1 (f1 (f1 c3 c_0) c_1) c_0) (f1 c_1 (f1 c_0 c_0))) (= (f1 (f1 (f1 c3 c_0) c_1) c_1) (f1 c_1 (f1 c_0 c_1))) (= (f1 (f1 (f1 c3 c_1) c_0) c_0) (f1 c_0 (f1 c_1 c_0))) (= (f1 (f1 (f1 c3 c_1) c_0) c_1) (f1 c_0 (f1 c_1 c_1))) (= (f1 (f1 (f1 c3 c_1) c_1) c_0) (f1 c_1 (f1 c_1 c_0))) (= (f1 (f1 (f1 c3 c_1) c_1) c_1) (f1 c_1 (f1 c_1 c_1))) (= (f1 (f1 c2 c_0) c_0) (f1 c_0 (f1 c_0 c_0))) (= (f1 (f1 c2 c_0) c_1) (f1 c_0 (f1 c_1 c_1))) (= (f1 (f1 c2 c_1) c_0) (f1 c_1 (f1 c_0 c_0))) (= (f1 (f1 c2 c_1) c_1) (f1 c_1 (f1 c_1 c_1))) (not (= (f1 c_0 (f4 c_0)) (f1 (f4 c_0) (f1 c_0 (f4 c_0))))) (not (= (f1 c_1 (f4 c_1)) (f1 (f4 c_1) (f1 c_1 (f4 c_1))))) (or (= (f1 c_0 c_0) c_0)(= (f1 c_0 c_0) c_1))(or (= (f1 c_0 c_1) c_0)(= (f1 c_0 c_1) c_1))(or (= (f1 c_1 c_0) c_0)(= (f1 c_1 c_0) c_1))(or (= (f1 c_1 c_1) c_0)(= (f1 c_1 c_1) c_1))(or (= (f4 c_0) c_0)(= (f4 c_0) c_1))(or (= (f4 c_1) c_0)(= (f4 c_1) c_1))(or (= c3 c_0)(= c3 c_1))(or (= c2 c_0)(= c2 c_1))))
--- /dev/null
+(benchmark dead_dnd002.smt
+ :source {
+http://www.cs.bham.ac.uk/~vxs/quasigroups/benchmark/
+
+}
+ :status unsat
+ :difficulty { 0 }
+ :category { crafted }
+ :logic QF_UF
+ :extrasorts (I)
+ :extrafuns ((op I I I))
+ :extrafuns ((e4 I))
+ :extrafuns ((e3 I))
+ :extrafuns ((e2 I))
+ :extrafuns ((e1 I))
+ :extrafuns ((e0 I))
+ :assumption
+(let (?cvc_0 (op e0 e0)) (let (?cvc_1 (op e0 e1)) (let (?cvc_2 (op e0 e2)) (let (?cvc_3 (op e0 e3)) (let (?cvc_4 (op e0 e4)) (let (?cvc_5 (op e1 e0)) (let (?cvc_6 (op e1 e1)) (let (?cvc_7 (op e1 e2)) (let (?cvc_8 (op e1 e3)) (let (?cvc_9 (op e1 e4)) (let (?cvc_10 (op e2 e0)) (let (?cvc_11 (op e2 e1)) (let (?cvc_12 (op e2 e2)) (let (?cvc_13 (op e2 e3)) (let (?cvc_14 (op e2 e4)) (let (?cvc_15 (op e3 e0)) (let (?cvc_16 (op e3 e1)) (let (?cvc_17 (op e3 e2)) (let (?cvc_18 (op e3 e3)) (let (?cvc_19 (op e3 e4)) (let (?cvc_20 (op e4 e0)) (let (?cvc_21 (op e4 e1)) (let (?cvc_22 (op e4 e2)) (let (?cvc_23 (op e4 e3)) (let (?cvc_24 (op e4 e4)) (and (and (and (and (and (and (and (and (or (or (or (or (= ?cvc_0 e0) (= ?cvc_0 e1) ) (= ?cvc_0 e2) ) (= ?cvc_0 e3) ) (= ?cvc_0 e4) ) (or (or (or (or (= ?cvc_1 e0) (= ?cvc_1 e1) ) (= ?cvc_1 e2) ) (= ?cvc_1 e3) ) (= ?cvc_1 e4) )) (or (or (or (or (= ?cvc_2 e0) (= ?cvc_2 e1) ) (= ?cvc_2 e2) ) (= ?cvc_2 e3) ) (= ?cvc_2 e4) )) (or (or (or (or (= ?cvc_3 e0) (= ?cvc_3 e1) ) (= ?cvc_3 e2) ) (= ?cvc_3 e3) ) (= ?cvc_3 e4) )) (or (or (or (or (= ?cvc_4 e0) (= ?cvc_4 e1) ) (= ?cvc_4 e2) ) (= ?cvc_4 e3) ) (= ?cvc_4 e4) )) (and (and (and (and (or (or (or (or (= ?cvc_5 e0) (= ?cvc_5 e1) ) (= ?cvc_5 e2) ) (= ?cvc_5 e3) ) (= ?cvc_5 e4) ) (or (or (or (or (= ?cvc_6 e0) (= ?cvc_6 e1) ) (= ?cvc_6 e2) ) (= ?cvc_6 e3) ) (= ?cvc_6 e4) )) (or (or (or (or (= ?cvc_7 e0) (= ?cvc_7 e1) ) (= ?cvc_7 e2) ) (= ?cvc_7 e3) ) (= ?cvc_7 e4) )) (or (or (or (or (= ?cvc_8 e0) (= ?cvc_8 e1) ) (= ?cvc_8 e2) ) (= ?cvc_8 e3) ) (= ?cvc_8 e4) )) (or (or (or (or (= ?cvc_9 e0) (= ?cvc_9 e1) ) (= ?cvc_9 e2) ) (= ?cvc_9 e3) ) (= ?cvc_9 e4) ))) (and (and (and (and (or (or (or (or (= ?cvc_10 e0) (= ?cvc_10 e1) ) (= ?cvc_10 e2) ) (= ?cvc_10 e3) ) (= ?cvc_10 e4) ) (or (or (or (or (= ?cvc_11 e0) (= ?cvc_11 e1) ) (= ?cvc_11 e2) ) (= ?cvc_11 e3) ) (= ?cvc_11 e4) )) (or (or (or (or (= ?cvc_12 e0) (= ?cvc_12 e1) ) (= ?cvc_12 e2) ) (= ?cvc_12 e3) ) (= ?cvc_12 e4) )) (or (or (or (or (= ?cvc_13 e0) (= ?cvc_13 e1) ) (= ?cvc_13 e2) ) (= ?cvc_13 e3) ) (= ?cvc_13 e4) )) (or (or (or (or (= ?cvc_14 e0) (= ?cvc_14 e1) ) (= ?cvc_14 e2) ) (= ?cvc_14 e3) ) (= ?cvc_14 e4) ))) (and (and (and (and (or (or (or (or (= ?cvc_15 e0) (= ?cvc_15 e1) ) (= ?cvc_15 e2) ) (= ?cvc_15 e3) ) (= ?cvc_15 e4) ) (or (or (or (or (= ?cvc_16 e0) (= ?cvc_16 e1) ) (= ?cvc_16 e2) ) (= ?cvc_16 e3) ) (= ?cvc_16 e4) )) (or (or (or (or (= ?cvc_17 e0) (= ?cvc_17 e1) ) (= ?cvc_17 e2) ) (= ?cvc_17 e3) ) (= ?cvc_17 e4) )) (or (or (or (or (= ?cvc_18 e0) (= ?cvc_18 e1) ) (= ?cvc_18 e2) ) (= ?cvc_18 e3) ) (= ?cvc_18 e4) )) (or (or (or (or (= ?cvc_19 e0) (= ?cvc_19 e1) ) (= ?cvc_19 e2) ) (= ?cvc_19 e3) ) (= ?cvc_19 e4) ))) (and (and (and (and (or (or (or (or (= ?cvc_20 e0) (= ?cvc_20 e1) ) (= ?cvc_20 e2) ) (= ?cvc_20 e3) ) (= ?cvc_20 e4) ) (or (or (or (or (= ?cvc_21 e0) (= ?cvc_21 e1) ) (= ?cvc_21 e2) ) (= ?cvc_21 e3) ) (= ?cvc_21 e4) )) (or (or (or (or (= ?cvc_22 e0) (= ?cvc_22 e1) ) (= ?cvc_22 e2) ) (= ?cvc_22 e3) ) (= ?cvc_22 e4) )) (or (or (or (or (= ?cvc_23 e0) (= ?cvc_23 e1) ) (= ?cvc_23 e2) ) (= ?cvc_23 e3) ) (= ?cvc_23 e4) )) (or (or (or (or (= ?cvc_24 e0) (= ?cvc_24 e1) ) (= ?cvc_24 e2) ) (= ?cvc_24 e3) ) (= ?cvc_24 e4) ))))))))))))))))))))))))))))
+ :assumption
+(let (?cvc_1 (op e0 e0)) (flet ($cvc_0 (= ?cvc_1 e0)) (flet ($cvc_6 (= ?cvc_1 e1)) (flet ($cvc_11 (= ?cvc_1 e2)) (flet ($cvc_12 (= ?cvc_1 e3)) (flet ($cvc_13 (= ?cvc_1 e4)) (let (?cvc_2 (op e0 e1)) (flet ($cvc_15 (= ?cvc_2 e0)) (flet ($cvc_22 (= ?cvc_2 e1)) (flet ($cvc_28 (= ?cvc_2 e2)) (flet ($cvc_31 (= ?cvc_2 e3)) (flet ($cvc_34 (= ?cvc_2 e4)) (let (?cvc_3 (op e0 e2)) (flet ($cvc_38 (= ?cvc_3 e0)) (flet ($cvc_46 (= ?cvc_3 e1)) (flet ($cvc_53 (= ?cvc_3 e2)) (flet ($cvc_58 (= ?cvc_3 e3)) (flet ($cvc_63 (= ?cvc_3 e4)) (let (?cvc_4 (op e0 e3)) (flet ($cvc_69 (= ?cvc_4 e0)) (flet ($cvc_78 (= ?cvc_4 e1)) (flet ($cvc_86 (= ?cvc_4 e2)) (flet ($cvc_93 (= ?cvc_4 e3)) (flet ($cvc_100 (= ?cvc_4 e4)) (let (?cvc_5 (op e0 e4)) (flet ($cvc_108 (= ?cvc_5 e0)) (flet ($cvc_118 (= ?cvc_5 e1)) (flet ($cvc_127 (= ?cvc_5 e2)) (flet ($cvc_136 (= ?cvc_5 e3)) (flet ($cvc_145 (= ?cvc_5 e4)) (let (?cvc_7 (op e1 e0)) (flet ($cvc_14 (= ?cvc_7 e0)) (flet ($cvc_17 (= ?cvc_7 e1)) (flet ($cvc_27 (= ?cvc_7 e2)) (flet ($cvc_30 (= ?cvc_7 e3)) (flet ($cvc_33 (= ?cvc_7 e4)) (let (?cvc_18 (op e1 e1)) (flet ($cvc_16 (= ?cvc_18 e0)) (flet ($cvc_23 (= ?cvc_18 e1)) (flet ($cvc_29 (= ?cvc_18 e2)) (flet ($cvc_32 (= ?cvc_18 e3)) (flet ($cvc_35 (= ?cvc_18 e4)) (let (?cvc_19 (op e1 e2)) (flet ($cvc_39 (= ?cvc_19 e0)) (flet ($cvc_47 (= ?cvc_19 e1)) (flet ($cvc_54 (= ?cvc_19 e2)) (flet ($cvc_59 (= ?cvc_19 e3)) (flet ($cvc_64 (= ?cvc_19 e4)) (let (?cvc_20 (op e1 e3)) (flet ($cvc_70 (= ?cvc_20 e0)) (flet ($cvc_79 (= ?cvc_20 e1)) (flet ($cvc_87 (= ?cvc_20 e2)) (flet ($cvc_94 (= ?cvc_20 e3)) (flet ($cvc_101 (= ?cvc_20 e4)) (let (?cvc_21 (op e1 e4)) (flet ($cvc_109 (= ?cvc_21 e0)) (flet ($cvc_119 (= ?cvc_21 e1)) (flet ($cvc_128 (= ?cvc_21 e2)) (flet ($cvc_137 (= ?cvc_21 e3)) (flet ($cvc_146 (= ?cvc_21 e4)) (let (?cvc_8 (op e2 e0)) (flet ($cvc_36 (= ?cvc_8 e0)) (flet ($cvc_41 (= ?cvc_8 e1)) (flet ($cvc_51 (= ?cvc_8 e2)) (flet ($cvc_56 (= ?cvc_8 e3)) (flet ($cvc_61 (= ?cvc_8 e4)) (let (?cvc_24 (op e2 e1)) (flet ($cvc_37 (= ?cvc_24 e0)) (flet ($cvc_42 (= ?cvc_24 e1)) (flet ($cvc_52 (= ?cvc_24 e2)) (flet ($cvc_57 (= ?cvc_24 e3)) (flet ($cvc_62 (= ?cvc_24 e4)) (let (?cvc_43 (op e2 e2)) (flet ($cvc_40 (= ?cvc_43 e0)) (flet ($cvc_48 (= ?cvc_43 e1)) (flet ($cvc_55 (= ?cvc_43 e2)) (flet ($cvc_60 (= ?cvc_43 e3)) (flet ($cvc_65 (= ?cvc_43 e4)) (let (?cvc_44 (op e2 e3)) (flet ($cvc_71 (= ?cvc_44 e0)) (flet ($cvc_80 (= ?cvc_44 e1)) (flet ($cvc_88 (= ?cvc_44 e2)) (flet ($cvc_95 (= ?cvc_44 e3)) (flet ($cvc_102 (= ?cvc_44 e4)) (let (?cvc_45 (op e2 e4)) (flet ($cvc_110 (= ?cvc_45 e0)) (flet ($cvc_120 (= ?cvc_45 e1)) (flet ($cvc_129 (= ?cvc_45 e2)) (flet ($cvc_138 (= ?cvc_45 e3)) (flet ($cvc_147 (= ?cvc_45 e4)) (let (?cvc_9 (op e3 e0)) (flet ($cvc_66 (= ?cvc_9 e0)) (flet ($cvc_73 (= ?cvc_9 e1)) (flet ($cvc_83 (= ?cvc_9 e2)) (flet ($cvc_90 (= ?cvc_9 e3)) (flet ($cvc_97 (= ?cvc_9 e4)) (let (?cvc_25 (op e3 e1)) (flet ($cvc_67 (= ?cvc_25 e0)) (flet ($cvc_74 (= ?cvc_25 e1)) (flet ($cvc_84 (= ?cvc_25 e2)) (flet ($cvc_91 (= ?cvc_25 e3)) (flet ($cvc_98 (= ?cvc_25 e4)) (let (?cvc_49 (op e3 e2)) (flet ($cvc_68 (= ?cvc_49 e0)) (flet ($cvc_75 (= ?cvc_49 e1)) (flet ($cvc_85 (= ?cvc_49 e2)) (flet ($cvc_92 (= ?cvc_49 e3)) (flet ($cvc_99 (= ?cvc_49 e4)) (let (?cvc_76 (op e3 e3)) (flet ($cvc_72 (= ?cvc_76 e0)) (flet ($cvc_81 (= ?cvc_76 e1)) (flet ($cvc_89 (= ?cvc_76 e2)) (flet ($cvc_96 (= ?cvc_76 e3)) (flet ($cvc_103 (= ?cvc_76 e4)) (let (?cvc_77 (op e3 e4)) (flet ($cvc_111 (= ?cvc_77 e0)) (flet ($cvc_121 (= ?cvc_77 e1)) (flet ($cvc_130 (= ?cvc_77 e2)) (flet ($cvc_139 (= ?cvc_77 e3)) (flet ($cvc_148 (= ?cvc_77 e4)) (let (?cvc_10 (op e4 e0)) (flet ($cvc_104 (= ?cvc_10 e0)) (flet ($cvc_113 (= ?cvc_10 e1)) (flet ($cvc_123 (= ?cvc_10 e2)) (flet ($cvc_132 (= ?cvc_10 e3)) (flet ($cvc_141 (= ?cvc_10 e4)) (let (?cvc_26 (op e4 e1)) (flet ($cvc_105 (= ?cvc_26 e0)) (flet ($cvc_114 (= ?cvc_26 e1)) (flet ($cvc_124 (= ?cvc_26 e2)) (flet ($cvc_133 (= ?cvc_26 e3)) (flet ($cvc_142 (= ?cvc_26 e4)) (let (?cvc_50 (op e4 e2)) (flet ($cvc_106 (= ?cvc_50 e0)) (flet ($cvc_115 (= ?cvc_50 e1)) (flet ($cvc_125 (= ?cvc_50 e2)) (flet ($cvc_134 (= ?cvc_50 e3)) (flet ($cvc_143 (= ?cvc_50 e4)) (let (?cvc_82 (op e4 e3)) (flet ($cvc_107 (= ?cvc_82 e0)) (flet ($cvc_116 (= ?cvc_82 e1)) (flet ($cvc_126 (= ?cvc_82 e2)) (flet ($cvc_135 (= ?cvc_82 e3)) (flet ($cvc_144 (= ?cvc_82 e4)) (let (?cvc_117 (op e4 e4)) (flet ($cvc_112 (= ?cvc_117 e0)) (flet ($cvc_122 (= ?cvc_117 e1)) (flet ($cvc_131 (= ?cvc_117 e2)) (flet ($cvc_140 (= ?cvc_117 e3)) (flet ($cvc_149 (= ?cvc_117 e4)) (and (and (and (and (and (and (and (and (and (or (or (or (or $cvc_0 $cvc_15 ) $cvc_38 ) $cvc_69 ) $cvc_108 ) (or (or (or (or $cvc_0 $cvc_14 ) $cvc_36 ) $cvc_66 ) $cvc_104 )) (and (or (or (or (or $cvc_6 $cvc_22 ) $cvc_46 ) $cvc_78 ) $cvc_118 ) (or (or (or (or $cvc_6 $cvc_17 ) $cvc_41 ) $cvc_73 ) $cvc_113 ))) (and (or (or (or (or $cvc_11 $cvc_28 ) $cvc_53 ) $cvc_86 ) $cvc_127 ) (or (or (or (or $cvc_11 $cvc_27 ) $cvc_51 ) $cvc_83 ) $cvc_123 ))) (and (or (or (or (or $cvc_12 $cvc_31 ) $cvc_58 ) $cvc_93 ) $cvc_136 ) (or (or (or (or $cvc_12 $cvc_30 ) $cvc_56 ) $cvc_90 ) $cvc_132 ))) (and (or (or (or (or $cvc_13 $cvc_34 ) $cvc_63 ) $cvc_100 ) $cvc_145 ) (or (or (or (or $cvc_13 $cvc_33 ) $cvc_61 ) $cvc_97 ) $cvc_141 ))) (and (and (and (and (and (or (or (or (or $cvc_14 $cvc_16 ) $cvc_39 ) $cvc_70 ) $cvc_109 ) (or (or (or (or $cvc_15 $cvc_16 ) $cvc_37 ) $cvc_67 ) $cvc_105 )) (and (or (or (or (or $cvc_17 $cvc_23 ) $cvc_47 ) $cvc_79 ) $cvc_119 ) (or (or (or (or $cvc_22 $cvc_23 ) $cvc_42 ) $cvc_74 ) $cvc_114 ))) (and (or (or (or (or $cvc_27 $cvc_29 ) $cvc_54 ) $cvc_87 ) $cvc_128 ) (or (or (or (or $cvc_28 $cvc_29 ) $cvc_52 ) $cvc_84 ) $cvc_124 ))) (and (or (or (or (or $cvc_30 $cvc_32 ) $cvc_59 ) $cvc_94 ) $cvc_137 ) (or (or (or (or $cvc_31 $cvc_32 ) $cvc_57 ) $cvc_91 ) $cvc_133 ))) (and (or (or (or (or $cvc_33 $cvc_35 ) $cvc_64 ) $cvc_101 ) $cvc_146 ) (or (or (or (or $cvc_34 $cvc_35 ) $cvc_62 ) $cvc_98 ) $cvc_142 )))) (and (and (and (and (and (or (or (or (or $cvc_36 $cvc_37 ) $cvc_40 ) $cvc_71 ) $cvc_110 ) (or (or (or (or $cvc_38 $cvc_39 ) $cvc_40 ) $cvc_68 ) $cvc_106 )) (and (or (or (or (or $cvc_41 $cvc_42 ) $cvc_48 ) $cvc_80 ) $cvc_120 ) (or (or (or (or $cvc_46 $cvc_47 ) $cvc_48 ) $cvc_75 ) $cvc_115 ))) (and (or (or (or (or $cvc_51 $cvc_52 ) $cvc_55 ) $cvc_88 ) $cvc_129 ) (or (or (or (or $cvc_53 $cvc_54 ) $cvc_55 ) $cvc_85 ) $cvc_125 ))) (and (or (or (or (or $cvc_56 $cvc_57 ) $cvc_60 ) $cvc_95 ) $cvc_138 ) (or (or (or (or $cvc_58 $cvc_59 ) $cvc_60 ) $cvc_92 ) $cvc_134 ))) (and (or (or (or (or $cvc_61 $cvc_62 ) $cvc_65 ) $cvc_102 ) $cvc_147 ) (or (or (or (or $cvc_63 $cvc_64 ) $cvc_65 ) $cvc_99 ) $cvc_143 )))) (and (and (and (and (and (or (or (or (or $cvc_66 $cvc_67 ) $cvc_68 ) $cvc_72 ) $cvc_111 ) (or (or (or (or $cvc_69 $cvc_70 ) $cvc_71 ) $cvc_72 ) $cvc_107 )) (and (or (or (or (or $cvc_73 $cvc_74 ) $cvc_75 ) $cvc_81 ) $cvc_121 ) (or (or (or (or $cvc_78 $cvc_79 ) $cvc_80 ) $cvc_81 ) $cvc_116 ))) (and (or (or (or (or $cvc_83 $cvc_84 ) $cvc_85 ) $cvc_89 ) $cvc_130 ) (or (or (or (or $cvc_86 $cvc_87 ) $cvc_88 ) $cvc_89 ) $cvc_126 ))) (and (or (or (or (or $cvc_90 $cvc_91 ) $cvc_92 ) $cvc_96 ) $cvc_139 ) (or (or (or (or $cvc_93 $cvc_94 ) $cvc_95 ) $cvc_96 ) $cvc_135 ))) (and (or (or (or (or $cvc_97 $cvc_98 ) $cvc_99 ) $cvc_103 ) $cvc_148 ) (or (or (or (or $cvc_100 $cvc_101 ) $cvc_102 ) $cvc_103 ) $cvc_144 )))) (and (and (and (and (and (or (or (or (or $cvc_104 $cvc_105 ) $cvc_106 ) $cvc_107 ) $cvc_112 ) (or (or (or (or $cvc_108 $cvc_109 ) $cvc_110 ) $cvc_111 ) $cvc_112 )) (and (or (or (or (or $cvc_113 $cvc_114 ) $cvc_115 ) $cvc_116 ) $cvc_122 ) (or (or (or (or $cvc_118 $cvc_119 ) $cvc_120 ) $cvc_121 ) $cvc_122 ))) (and (or (or (or (or $cvc_123 $cvc_124 ) $cvc_125 ) $cvc_126 ) $cvc_131 ) (or (or (or (or $cvc_127 $cvc_128 ) $cvc_129 ) $cvc_130 ) $cvc_131 ))) (and (or (or (or (or $cvc_132 $cvc_133 ) $cvc_134 ) $cvc_135 ) $cvc_140 ) (or (or (or (or $cvc_136 $cvc_137 ) $cvc_138 ) $cvc_139 ) $cvc_140 ))) (and (or (or (or (or $cvc_141 $cvc_142 ) $cvc_143 ) $cvc_144 ) $cvc_149 ) (or (or (or (or $cvc_145 $cvc_146 ) $cvc_147 ) $cvc_148 ) $cvc_149 ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+ :assumption
+(let (?cvc_0 (op e0 e0)) (let (?cvc_1 (op e1 e1)) (let (?cvc_2 (op e2 e2)) (let (?cvc_3 (op e3 e3)) (let (?cvc_4 (op e4 e4)) (and (and (and (and (or (or (or (or (= ?cvc_0 e0) (= ?cvc_1 e0) ) (= ?cvc_2 e0) ) (= ?cvc_3 e0) ) (= ?cvc_4 e0) ) (or (or (or (or (= ?cvc_0 e1) (= ?cvc_1 e1) ) (= ?cvc_2 e1) ) (= ?cvc_3 e1) ) (= ?cvc_4 e1) )) (or (or (or (or (= ?cvc_0 e2) (= ?cvc_1 e2) ) (= ?cvc_2 e2) ) (= ?cvc_3 e2) ) (= ?cvc_4 e2) )) (or (or (or (or (= ?cvc_0 e3) (= ?cvc_1 e3) ) (= ?cvc_2 e3) ) (= ?cvc_3 e3) ) (= ?cvc_4 e3) )) (or (or (or (or (= ?cvc_0 e4) (= ?cvc_1 e4) ) (= ?cvc_2 e4) ) (= ?cvc_3 e4) ) (= ?cvc_4 e4) )))))))
+ :assumption
+(and (and (and (and (or (or (or (or (= (op e0 e0) e0) (= (op e1 e0) e1) ) (= (op e2 e0) e2) ) (= (op e3 e0) e3) ) (= (op e4 e0) e4) ) (or (or (or (or (= (op e0 e1) e0) (= (op e1 e1) e1) ) (= (op e2 e1) e2) ) (= (op e3 e1) e3) ) (= (op e4 e1) e4) )) (or (or (or (or (= (op e0 e2) e0) (= (op e1 e2) e1) ) (= (op e2 e2) e2) ) (= (op e3 e2) e3) ) (= (op e4 e2) e4) )) (or (or (or (or (= (op e0 e3) e0) (= (op e1 e3) e1) ) (= (op e2 e3) e2) ) (= (op e3 e3) e3) ) (= (op e4 e3) e4) )) (or (or (or (or (= (op e0 e4) e0) (= (op e1 e4) e1) ) (= (op e2 e4) e2) ) (= (op e3 e4) e3) ) (= (op e4 e4) e4) ))
+ :assumption
+(let (?cvc_0 (op e0 e0)) (let (?cvc_1 (op e0 e1)) (let (?cvc_4 (op e0 e2)) (let (?cvc_9 (op e0 e3)) (let (?cvc_16 (op e0 e4)) (let (?cvc_2 (op e1 e0)) (let (?cvc_3 (op e1 e1)) (let (?cvc_6 (op e1 e2)) (let (?cvc_11 (op e1 e3)) (let (?cvc_18 (op e1 e4)) (let (?cvc_5 (op e2 e0)) (let (?cvc_7 (op e2 e1)) (let (?cvc_8 (op e2 e2)) (let (?cvc_13 (op e2 e3)) (let (?cvc_20 (op e2 e4)) (let (?cvc_10 (op e3 e0)) (let (?cvc_12 (op e3 e1)) (let (?cvc_14 (op e3 e2)) (let (?cvc_15 (op e3 e3)) (let (?cvc_22 (op e3 e4)) (let (?cvc_17 (op e4 e0)) (let (?cvc_19 (op e4 e1)) (let (?cvc_21 (op e4 e2)) (let (?cvc_23 (op e4 e3)) (let (?cvc_24 (op e4 e4)) (or (or (or (or (or (or (or (or (not (= ?cvc_0 ?cvc_0)) (not (= ?cvc_2 ?cvc_1)) ) (not (= ?cvc_5 ?cvc_4)) ) (not (= ?cvc_10 ?cvc_9)) ) (not (= ?cvc_17 ?cvc_16)) ) (or (or (or (or (not (= ?cvc_1 ?cvc_2)) (not (= ?cvc_3 ?cvc_3)) ) (not (= ?cvc_7 ?cvc_6)) ) (not (= ?cvc_12 ?cvc_11)) ) (not (= ?cvc_19 ?cvc_18)) ) ) (or (or (or (or (not (= ?cvc_4 ?cvc_5)) (not (= ?cvc_6 ?cvc_7)) ) (not (= ?cvc_8 ?cvc_8)) ) (not (= ?cvc_14 ?cvc_13)) ) (not (= ?cvc_21 ?cvc_20)) ) ) (or (or (or (or (not (= ?cvc_9 ?cvc_10)) (not (= ?cvc_11 ?cvc_12)) ) (not (= ?cvc_13 ?cvc_14)) ) (not (= ?cvc_15 ?cvc_15)) ) (not (= ?cvc_23 ?cvc_22)) ) ) (or (or (or (or (not (= ?cvc_16 ?cvc_17)) (not (= ?cvc_18 ?cvc_19)) ) (not (= ?cvc_20 ?cvc_21)) ) (not (= ?cvc_22 ?cvc_23)) ) (not (= ?cvc_24 ?cvc_24)) ) ))))))))))))))))))))))))))
+ :assumption
+(and (and (and (and (not (= (op e0 e0) e0)) (not (= (op e1 e1) e1))) (not (= (op e2 e2) e2))) (not (= (op e3 e3) e3))) (not (= (op e4 e4) e4)))
+ :assumption
+(flet ($cvc_0 (= (op e0 (op e0 e0)) e0)) (flet ($cvc_1 (= (op e1 (op e1 e1)) e1)) (flet ($cvc_2 (= (op e2 (op e2 e2)) e2)) (flet ($cvc_3 (= (op e3 (op e3 e3)) e3)) (flet ($cvc_4 (= (op e4 (op e4 e4)) e4)) (and (and (and (and (and (not $cvc_0) (not $cvc_1)) (not $cvc_2)) (not $cvc_3)) (not $cvc_4)) (and (and (and (and (and (and (and (and $cvc_0 (= (op e0 (op e0 e1)) e1)) (= (op e0 (op e0 e2)) e2)) (= (op e0 (op e0 e3)) e3)) (= (op e0 (op e0 e4)) e4)) (and (and (and (and (= (op e1 (op e1 e0)) e0) $cvc_1) (= (op e1 (op e1 e2)) e2)) (= (op e1 (op e1 e3)) e3)) (= (op e1 (op e1 e4)) e4))) (and (and (and (and (= (op e2 (op e2 e0)) e0) (= (op e2 (op e2 e1)) e1)) $cvc_2) (= (op e2 (op e2 e3)) e3)) (= (op e2 (op e2 e4)) e4))) (and (and (and (and (= (op e3 (op e3 e0)) e0) (= (op e3 (op e3 e1)) e1)) (= (op e3 (op e3 e2)) e2)) $cvc_3) (= (op e3 (op e3 e4)) e4))) (and (and (and (and (= (op e4 (op e4 e0)) e0) (= (op e4 (op e4 e1)) e1)) (= (op e4 (op e4 e2)) e2)) (= (op e4 (op e4 e3)) e3)) $cvc_4))))))))
+ :assumption
+(let (?cvc_0 (op e0 e0)) (let (?cvc_5 (op e0 e1)) (let (?cvc_10 (op e0 e2)) (let (?cvc_15 (op e0 e3)) (let (?cvc_20 (op e0 e4)) (let (?cvc_1 (op e1 e0)) (let (?cvc_6 (op e1 e1)) (let (?cvc_11 (op e1 e2)) (let (?cvc_16 (op e1 e3)) (let (?cvc_21 (op e1 e4)) (let (?cvc_2 (op e2 e0)) (let (?cvc_7 (op e2 e1)) (let (?cvc_12 (op e2 e2)) (let (?cvc_17 (op e2 e3)) (let (?cvc_22 (op e2 e4)) (let (?cvc_3 (op e3 e0)) (let (?cvc_8 (op e3 e1)) (let (?cvc_13 (op e3 e2)) (let (?cvc_18 (op e3 e3)) (let (?cvc_23 (op e3 e4)) (let (?cvc_4 (op e4 e0)) (let (?cvc_9 (op e4 e1)) (let (?cvc_14 (op e4 e2)) (let (?cvc_19 (op e4 e3)) (let (?cvc_24 (op e4 e4)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (= ?cvc_0 ?cvc_1)) (not (= ?cvc_0 ?cvc_2))) (not (= ?cvc_0 ?cvc_3))) (not (= ?cvc_0 ?cvc_4))) (not (= ?cvc_1 ?cvc_2))) (not (= ?cvc_1 ?cvc_3))) (not (= ?cvc_1 ?cvc_4))) (not (= ?cvc_2 ?cvc_3))) (not (= ?cvc_2 ?cvc_4))) (not (= ?cvc_3 ?cvc_4))) (and (and (and (and (and (and (and (and (and (not (= ?cvc_5 ?cvc_6)) (not (= ?cvc_5 ?cvc_7))) (not (= ?cvc_5 ?cvc_8))) (not (= ?cvc_5 ?cvc_9))) (not (= ?cvc_6 ?cvc_7))) (not (= ?cvc_6 ?cvc_8))) (not (= ?cvc_6 ?cvc_9))) (not (= ?cvc_7 ?cvc_8))) (not (= ?cvc_7 ?cvc_9))) (not (= ?cvc_8 ?cvc_9)))) (and (and (and (and (and (and (and (and (and (not (= ?cvc_10 ?cvc_11)) (not (= ?cvc_10 ?cvc_12))) (not (= ?cvc_10 ?cvc_13))) (not (= ?cvc_10 ?cvc_14))) (not (= ?cvc_11 ?cvc_12))) (not (= ?cvc_11 ?cvc_13))) (not (= ?cvc_11 ?cvc_14))) (not (= ?cvc_12 ?cvc_13))) (not (= ?cvc_12 ?cvc_14))) (not (= ?cvc_13 ?cvc_14)))) (and (and (and (and (and (and (and (and (and (not (= ?cvc_15 ?cvc_16)) (not (= ?cvc_15 ?cvc_17))) (not (= ?cvc_15 ?cvc_18))) (not (= ?cvc_15 ?cvc_19))) (not (= ?cvc_16 ?cvc_17))) (not (= ?cvc_16 ?cvc_18))) (not (= ?cvc_16 ?cvc_19))) (not (= ?cvc_17 ?cvc_18))) (not (= ?cvc_17 ?cvc_19))) (not (= ?cvc_18 ?cvc_19)))) (and (and (and (and (and (and (and (and (and (not (= ?cvc_20 ?cvc_21)) (not (= ?cvc_20 ?cvc_22))) (not (= ?cvc_20 ?cvc_23))) (not (= ?cvc_20 ?cvc_24))) (not (= ?cvc_21 ?cvc_22))) (not (= ?cvc_21 ?cvc_23))) (not (= ?cvc_21 ?cvc_24))) (not (= ?cvc_22 ?cvc_23))) (not (= ?cvc_22 ?cvc_24))) (not (= ?cvc_23 ?cvc_24)))) (and (and (and (and (and (and (and (and (and (and (and (and (and (not (= ?cvc_0 ?cvc_5)) (not (= ?cvc_0 ?cvc_10))) (not (= ?cvc_0 ?cvc_15))) (not (= ?cvc_0 ?cvc_20))) (not (= ?cvc_5 ?cvc_10))) (not (= ?cvc_5 ?cvc_15))) (not (= ?cvc_5 ?cvc_20))) (not (= ?cvc_10 ?cvc_15))) (not (= ?cvc_10 ?cvc_20))) (not (= ?cvc_15 ?cvc_20))) (and (and (and (and (and (and (and (and (and (not (= ?cvc_1 ?cvc_6)) (not (= ?cvc_1 ?cvc_11))) (not (= ?cvc_1 ?cvc_16))) (not (= ?cvc_1 ?cvc_21))) (not (= ?cvc_6 ?cvc_11))) (not (= ?cvc_6 ?cvc_16))) (not (= ?cvc_6 ?cvc_21))) (not (= ?cvc_11 ?cvc_16))) (not (= ?cvc_11 ?cvc_21))) (not (= ?cvc_16 ?cvc_21)))) (and (and (and (and (and (and (and (and (and (not (= ?cvc_2 ?cvc_7)) (not (= ?cvc_2 ?cvc_12))) (not (= ?cvc_2 ?cvc_17))) (not (= ?cvc_2 ?cvc_22))) (not (= ?cvc_7 ?cvc_12))) (not (= ?cvc_7 ?cvc_17))) (not (= ?cvc_7 ?cvc_22))) (not (= ?cvc_12 ?cvc_17))) (not (= ?cvc_12 ?cvc_22))) (not (= ?cvc_17 ?cvc_22)))) (and (and (and (and (and (and (and (and (and (not (= ?cvc_3 ?cvc_8)) (not (= ?cvc_3 ?cvc_13))) (not (= ?cvc_3 ?cvc_18))) (not (= ?cvc_3 ?cvc_23))) (not (= ?cvc_8 ?cvc_13))) (not (= ?cvc_8 ?cvc_18))) (not (= ?cvc_8 ?cvc_23))) (not (= ?cvc_13 ?cvc_18))) (not (= ?cvc_13 ?cvc_23))) (not (= ?cvc_18 ?cvc_23)))) (and (and (and (and (and (and (and (and (and (not (= ?cvc_4 ?cvc_9)) (not (= ?cvc_4 ?cvc_14))) (not (= ?cvc_4 ?cvc_19))) (not (= ?cvc_4 ?cvc_24))) (not (= ?cvc_9 ?cvc_14))) (not (= ?cvc_9 ?cvc_19))) (not (= ?cvc_9 ?cvc_24))) (not (= ?cvc_14 ?cvc_19))) (not (= ?cvc_14 ?cvc_24))) (not (= ?cvc_19 ?cvc_24))))))))))))))))))))))))))))))
+ :assumption
+(and (and (and (and (and (and (and (and (and (not (= e0 e1)) (not (= e0 e2))) (not (= e0 e3))) (not (= e0 e4))) (not (= e1 e2))) (not (= e1 e3))) (not (= e1 e4))) (not (= e2 e3))) (not (= e2 e4))) (not (= e3 e4)))
+ :formula
+(not false)
+)
--- /dev/null
+(benchmark eq_diamond1
+:source{
+Generating minimum transitivity constraints in P-time for deciding Equality Logic,
+Ofer Strichman and Mirron Rozanov,
+SMT Workshop 2005.
+
+Translator: Leonardo de Moura. }
+:status unsat
+:category { crafted }
+:logic QF_UF
+:difficulty { 0 }
+:extrafuns ((x0 U) (y0 U) (z0 U)
+)
+:formula (and
+(not (= x0 x0))))
--- /dev/null
+(benchmark iso_brn001.smt
+ :source {
+http://www.cs.bham.ac.uk/~vxs/quasigroups/benchmark/
+
+}
+ :status sat
+ :difficulty { 0 }
+ :category { crafted }
+ :logic QF_UF
+ :extrasorts (I)
+ :extrafuns ((op1 I I I))
+ :extrafuns ((op I I I))
+ :extrafuns ((e4 I))
+ :extrafuns ((e3 I))
+ :extrafuns ((e2 I))
+ :extrafuns ((e1 I))
+ :extrafuns ((e0 I))
+ :assumption
+(let (?cvc_0 (op e0 e0)) (let (?cvc_1 (op e0 e1)) (let (?cvc_2 (op e0 e2)) (let (?cvc_3 (op e0 e3)) (let (?cvc_4 (op e0 e4)) (let (?cvc_5 (op e1 e0)) (let (?cvc_6 (op e1 e1)) (let (?cvc_7 (op e1 e2)) (let (?cvc_8 (op e1 e3)) (let (?cvc_9 (op e1 e4)) (let (?cvc_10 (op e2 e0)) (let (?cvc_11 (op e2 e1)) (let (?cvc_12 (op e2 e2)) (let (?cvc_13 (op e2 e3)) (let (?cvc_14 (op e2 e4)) (let (?cvc_15 (op e3 e0)) (let (?cvc_16 (op e3 e1)) (let (?cvc_17 (op e3 e2)) (let (?cvc_18 (op e3 e3)) (let (?cvc_19 (op e3 e4)) (let (?cvc_20 (op e4 e0)) (let (?cvc_21 (op e4 e1)) (let (?cvc_22 (op e4 e2)) (let (?cvc_23 (op e4 e3)) (let (?cvc_24 (op e4 e4)) (and (and (and (and (and (and (and (and (or (or (or (or (= ?cvc_0 e0) (= ?cvc_0 e1) ) (= ?cvc_0 e2) ) (= ?cvc_0 e3) ) (= ?cvc_0 e4) ) (or (or (or (or (= ?cvc_1 e0) (= ?cvc_1 e1) ) (= ?cvc_1 e2) ) (= ?cvc_1 e3) ) (= ?cvc_1 e4) )) (or (or (or (or (= ?cvc_2 e0) (= ?cvc_2 e1) ) (= ?cvc_2 e2) ) (= ?cvc_2 e3) ) (= ?cvc_2 e4) )) (or (or (or (or (= ?cvc_3 e0) (= ?cvc_3 e1) ) (= ?cvc_3 e2) ) (= ?cvc_3 e3) ) (= ?cvc_3 e4) )) (or (or (or (or (= ?cvc_4 e0) (= ?cvc_4 e1) ) (= ?cvc_4 e2) ) (= ?cvc_4 e3) ) (= ?cvc_4 e4) )) (and (and (and (and (or (or (or (or (= ?cvc_5 e0) (= ?cvc_5 e1) ) (= ?cvc_5 e2) ) (= ?cvc_5 e3) ) (= ?cvc_5 e4) ) (or (or (or (or (= ?cvc_6 e0) (= ?cvc_6 e1) ) (= ?cvc_6 e2) ) (= ?cvc_6 e3) ) (= ?cvc_6 e4) )) (or (or (or (or (= ?cvc_7 e0) (= ?cvc_7 e1) ) (= ?cvc_7 e2) ) (= ?cvc_7 e3) ) (= ?cvc_7 e4) )) (or (or (or (or (= ?cvc_8 e0) (= ?cvc_8 e1) ) (= ?cvc_8 e2) ) (= ?cvc_8 e3) ) (= ?cvc_8 e4) )) (or (or (or (or (= ?cvc_9 e0) (= ?cvc_9 e1) ) (= ?cvc_9 e2) ) (= ?cvc_9 e3) ) (= ?cvc_9 e4) ))) (and (and (and (and (or (or (or (or (= ?cvc_10 e0) (= ?cvc_10 e1) ) (= ?cvc_10 e2) ) (= ?cvc_10 e3) ) (= ?cvc_10 e4) ) (or (or (or (or (= ?cvc_11 e0) (= ?cvc_11 e1) ) (= ?cvc_11 e2) ) (= ?cvc_11 e3) ) (= ?cvc_11 e4) )) (or (or (or (or (= ?cvc_12 e0) (= ?cvc_12 e1) ) (= ?cvc_12 e2) ) (= ?cvc_12 e3) ) (= ?cvc_12 e4) )) (or (or (or (or (= ?cvc_13 e0) (= ?cvc_13 e1) ) (= ?cvc_13 e2) ) (= ?cvc_13 e3) ) (= ?cvc_13 e4) )) (or (or (or (or (= ?cvc_14 e0) (= ?cvc_14 e1) ) (= ?cvc_14 e2) ) (= ?cvc_14 e3) ) (= ?cvc_14 e4) ))) (and (and (and (and (or (or (or (or (= ?cvc_15 e0) (= ?cvc_15 e1) ) (= ?cvc_15 e2) ) (= ?cvc_15 e3) ) (= ?cvc_15 e4) ) (or (or (or (or (= ?cvc_16 e0) (= ?cvc_16 e1) ) (= ?cvc_16 e2) ) (= ?cvc_16 e3) ) (= ?cvc_16 e4) )) (or (or (or (or (= ?cvc_17 e0) (= ?cvc_17 e1) ) (= ?cvc_17 e2) ) (= ?cvc_17 e3) ) (= ?cvc_17 e4) )) (or (or (or (or (= ?cvc_18 e0) (= ?cvc_18 e1) ) (= ?cvc_18 e2) ) (= ?cvc_18 e3) ) (= ?cvc_18 e4) )) (or (or (or (or (= ?cvc_19 e0) (= ?cvc_19 e1) ) (= ?cvc_19 e2) ) (= ?cvc_19 e3) ) (= ?cvc_19 e4) ))) (and (and (and (and (or (or (or (or (= ?cvc_20 e0) (= ?cvc_20 e1) ) (= ?cvc_20 e2) ) (= ?cvc_20 e3) ) (= ?cvc_20 e4) ) (or (or (or (or (= ?cvc_21 e0) (= ?cvc_21 e1) ) (= ?cvc_21 e2) ) (= ?cvc_21 e3) ) (= ?cvc_21 e4) )) (or (or (or (or (= ?cvc_22 e0) (= ?cvc_22 e1) ) (= ?cvc_22 e2) ) (= ?cvc_22 e3) ) (= ?cvc_22 e4) )) (or (or (or (or (= ?cvc_23 e0) (= ?cvc_23 e1) ) (= ?cvc_23 e2) ) (= ?cvc_23 e3) ) (= ?cvc_23 e4) )) (or (or (or (or (= ?cvc_24 e0) (= ?cvc_24 e1) ) (= ?cvc_24 e2) ) (= ?cvc_24 e3) ) (= ?cvc_24 e4) ))))))))))))))))))))))))))))
+ :assumption
+(let (?cvc_1 (op e0 e0)) (flet ($cvc_0 (= ?cvc_1 e0)) (flet ($cvc_6 (= ?cvc_1 e1)) (flet ($cvc_11 (= ?cvc_1 e2)) (flet ($cvc_12 (= ?cvc_1 e3)) (flet ($cvc_13 (= ?cvc_1 e4)) (let (?cvc_2 (op e0 e1)) (flet ($cvc_15 (= ?cvc_2 e0)) (flet ($cvc_22 (= ?cvc_2 e1)) (flet ($cvc_28 (= ?cvc_2 e2)) (flet ($cvc_31 (= ?cvc_2 e3)) (flet ($cvc_34 (= ?cvc_2 e4)) (let (?cvc_3 (op e0 e2)) (flet ($cvc_38 (= ?cvc_3 e0)) (flet ($cvc_46 (= ?cvc_3 e1)) (flet ($cvc_53 (= ?cvc_3 e2)) (flet ($cvc_58 (= ?cvc_3 e3)) (flet ($cvc_63 (= ?cvc_3 e4)) (let (?cvc_4 (op e0 e3)) (flet ($cvc_69 (= ?cvc_4 e0)) (flet ($cvc_78 (= ?cvc_4 e1)) (flet ($cvc_86 (= ?cvc_4 e2)) (flet ($cvc_93 (= ?cvc_4 e3)) (flet ($cvc_100 (= ?cvc_4 e4)) (let (?cvc_5 (op e0 e4)) (flet ($cvc_108 (= ?cvc_5 e0)) (flet ($cvc_118 (= ?cvc_5 e1)) (flet ($cvc_127 (= ?cvc_5 e2)) (flet ($cvc_136 (= ?cvc_5 e3)) (flet ($cvc_145 (= ?cvc_5 e4)) (let (?cvc_7 (op e1 e0)) (flet ($cvc_14 (= ?cvc_7 e0)) (flet ($cvc_17 (= ?cvc_7 e1)) (flet ($cvc_27 (= ?cvc_7 e2)) (flet ($cvc_30 (= ?cvc_7 e3)) (flet ($cvc_33 (= ?cvc_7 e4)) (let (?cvc_18 (op e1 e1)) (flet ($cvc_16 (= ?cvc_18 e0)) (flet ($cvc_23 (= ?cvc_18 e1)) (flet ($cvc_29 (= ?cvc_18 e2)) (flet ($cvc_32 (= ?cvc_18 e3)) (flet ($cvc_35 (= ?cvc_18 e4)) (let (?cvc_19 (op e1 e2)) (flet ($cvc_39 (= ?cvc_19 e0)) (flet ($cvc_47 (= ?cvc_19 e1)) (flet ($cvc_54 (= ?cvc_19 e2)) (flet ($cvc_59 (= ?cvc_19 e3)) (flet ($cvc_64 (= ?cvc_19 e4)) (let (?cvc_20 (op e1 e3)) (flet ($cvc_70 (= ?cvc_20 e0)) (flet ($cvc_79 (= ?cvc_20 e1)) (flet ($cvc_87 (= ?cvc_20 e2)) (flet ($cvc_94 (= ?cvc_20 e3)) (flet ($cvc_101 (= ?cvc_20 e4)) (let (?cvc_21 (op e1 e4)) (flet ($cvc_109 (= ?cvc_21 e0)) (flet ($cvc_119 (= ?cvc_21 e1)) (flet ($cvc_128 (= ?cvc_21 e2)) (flet ($cvc_137 (= ?cvc_21 e3)) (flet ($cvc_146 (= ?cvc_21 e4)) (let (?cvc_8 (op e2 e0)) (flet ($cvc_36 (= ?cvc_8 e0)) (flet ($cvc_41 (= ?cvc_8 e1)) (flet ($cvc_51 (= ?cvc_8 e2)) (flet ($cvc_56 (= ?cvc_8 e3)) (flet ($cvc_61 (= ?cvc_8 e4)) (let (?cvc_24 (op e2 e1)) (flet ($cvc_37 (= ?cvc_24 e0)) (flet ($cvc_42 (= ?cvc_24 e1)) (flet ($cvc_52 (= ?cvc_24 e2)) (flet ($cvc_57 (= ?cvc_24 e3)) (flet ($cvc_62 (= ?cvc_24 e4)) (let (?cvc_43 (op e2 e2)) (flet ($cvc_40 (= ?cvc_43 e0)) (flet ($cvc_48 (= ?cvc_43 e1)) (flet ($cvc_55 (= ?cvc_43 e2)) (flet ($cvc_60 (= ?cvc_43 e3)) (flet ($cvc_65 (= ?cvc_43 e4)) (let (?cvc_44 (op e2 e3)) (flet ($cvc_71 (= ?cvc_44 e0)) (flet ($cvc_80 (= ?cvc_44 e1)) (flet ($cvc_88 (= ?cvc_44 e2)) (flet ($cvc_95 (= ?cvc_44 e3)) (flet ($cvc_102 (= ?cvc_44 e4)) (let (?cvc_45 (op e2 e4)) (flet ($cvc_110 (= ?cvc_45 e0)) (flet ($cvc_120 (= ?cvc_45 e1)) (flet ($cvc_129 (= ?cvc_45 e2)) (flet ($cvc_138 (= ?cvc_45 e3)) (flet ($cvc_147 (= ?cvc_45 e4)) (let (?cvc_9 (op e3 e0)) (flet ($cvc_66 (= ?cvc_9 e0)) (flet ($cvc_73 (= ?cvc_9 e1)) (flet ($cvc_83 (= ?cvc_9 e2)) (flet ($cvc_90 (= ?cvc_9 e3)) (flet ($cvc_97 (= ?cvc_9 e4)) (let (?cvc_25 (op e3 e1)) (flet ($cvc_67 (= ?cvc_25 e0)) (flet ($cvc_74 (= ?cvc_25 e1)) (flet ($cvc_84 (= ?cvc_25 e2)) (flet ($cvc_91 (= ?cvc_25 e3)) (flet ($cvc_98 (= ?cvc_25 e4)) (let (?cvc_49 (op e3 e2)) (flet ($cvc_68 (= ?cvc_49 e0)) (flet ($cvc_75 (= ?cvc_49 e1)) (flet ($cvc_85 (= ?cvc_49 e2)) (flet ($cvc_92 (= ?cvc_49 e3)) (flet ($cvc_99 (= ?cvc_49 e4)) (let (?cvc_76 (op e3 e3)) (flet ($cvc_72 (= ?cvc_76 e0)) (flet ($cvc_81 (= ?cvc_76 e1)) (flet ($cvc_89 (= ?cvc_76 e2)) (flet ($cvc_96 (= ?cvc_76 e3)) (flet ($cvc_103 (= ?cvc_76 e4)) (let (?cvc_77 (op e3 e4)) (flet ($cvc_111 (= ?cvc_77 e0)) (flet ($cvc_121 (= ?cvc_77 e1)) (flet ($cvc_130 (= ?cvc_77 e2)) (flet ($cvc_139 (= ?cvc_77 e3)) (flet ($cvc_148 (= ?cvc_77 e4)) (let (?cvc_10 (op e4 e0)) (flet ($cvc_104 (= ?cvc_10 e0)) (flet ($cvc_113 (= ?cvc_10 e1)) (flet ($cvc_123 (= ?cvc_10 e2)) (flet ($cvc_132 (= ?cvc_10 e3)) (flet ($cvc_141 (= ?cvc_10 e4)) (let (?cvc_26 (op e4 e1)) (flet ($cvc_105 (= ?cvc_26 e0)) (flet ($cvc_114 (= ?cvc_26 e1)) (flet ($cvc_124 (= ?cvc_26 e2)) (flet ($cvc_133 (= ?cvc_26 e3)) (flet ($cvc_142 (= ?cvc_26 e4)) (let (?cvc_50 (op e4 e2)) (flet ($cvc_106 (= ?cvc_50 e0)) (flet ($cvc_115 (= ?cvc_50 e1)) (flet ($cvc_125 (= ?cvc_50 e2)) (flet ($cvc_134 (= ?cvc_50 e3)) (flet ($cvc_143 (= ?cvc_50 e4)) (let (?cvc_82 (op e4 e3)) (flet ($cvc_107 (= ?cvc_82 e0)) (flet ($cvc_116 (= ?cvc_82 e1)) (flet ($cvc_126 (= ?cvc_82 e2)) (flet ($cvc_135 (= ?cvc_82 e3)) (flet ($cvc_144 (= ?cvc_82 e4)) (let (?cvc_117 (op e4 e4)) (flet ($cvc_112 (= ?cvc_117 e0)) (flet ($cvc_122 (= ?cvc_117 e1)) (flet ($cvc_131 (= ?cvc_117 e2)) (flet ($cvc_140 (= ?cvc_117 e3)) (flet ($cvc_149 (= ?cvc_117 e4)) (and (and (and (and (and (and (and (and (and (or (or (or (or $cvc_0 $cvc_15 ) $cvc_38 ) $cvc_69 ) $cvc_108 ) (or (or (or (or $cvc_0 $cvc_14 ) $cvc_36 ) $cvc_66 ) $cvc_104 )) (and (or (or (or (or $cvc_6 $cvc_22 ) $cvc_46 ) $cvc_78 ) $cvc_118 ) (or (or (or (or $cvc_6 $cvc_17 ) $cvc_41 ) $cvc_73 ) $cvc_113 ))) (and (or (or (or (or $cvc_11 $cvc_28 ) $cvc_53 ) $cvc_86 ) $cvc_127 ) (or (or (or (or $cvc_11 $cvc_27 ) $cvc_51 ) $cvc_83 ) $cvc_123 ))) (and (or (or (or (or $cvc_12 $cvc_31 ) $cvc_58 ) $cvc_93 ) $cvc_136 ) (or (or (or (or $cvc_12 $cvc_30 ) $cvc_56 ) $cvc_90 ) $cvc_132 ))) (and (or (or (or (or $cvc_13 $cvc_34 ) $cvc_63 ) $cvc_100 ) $cvc_145 ) (or (or (or (or $cvc_13 $cvc_33 ) $cvc_61 ) $cvc_97 ) $cvc_141 ))) (and (and (and (and (and (or (or (or (or $cvc_14 $cvc_16 ) $cvc_39 ) $cvc_70 ) $cvc_109 ) (or (or (or (or $cvc_15 $cvc_16 ) $cvc_37 ) $cvc_67 ) $cvc_105 )) (and (or (or (or (or $cvc_17 $cvc_23 ) $cvc_47 ) $cvc_79 ) $cvc_119 ) (or (or (or (or $cvc_22 $cvc_23 ) $cvc_42 ) $cvc_74 ) $cvc_114 ))) (and (or (or (or (or $cvc_27 $cvc_29 ) $cvc_54 ) $cvc_87 ) $cvc_128 ) (or (or (or (or $cvc_28 $cvc_29 ) $cvc_52 ) $cvc_84 ) $cvc_124 ))) (and (or (or (or (or $cvc_30 $cvc_32 ) $cvc_59 ) $cvc_94 ) $cvc_137 ) (or (or (or (or $cvc_31 $cvc_32 ) $cvc_57 ) $cvc_91 ) $cvc_133 ))) (and (or (or (or (or $cvc_33 $cvc_35 ) $cvc_64 ) $cvc_101 ) $cvc_146 ) (or (or (or (or $cvc_34 $cvc_35 ) $cvc_62 ) $cvc_98 ) $cvc_142 )))) (and (and (and (and (and (or (or (or (or $cvc_36 $cvc_37 ) $cvc_40 ) $cvc_71 ) $cvc_110 ) (or (or (or (or $cvc_38 $cvc_39 ) $cvc_40 ) $cvc_68 ) $cvc_106 )) (and (or (or (or (or $cvc_41 $cvc_42 ) $cvc_48 ) $cvc_80 ) $cvc_120 ) (or (or (or (or $cvc_46 $cvc_47 ) $cvc_48 ) $cvc_75 ) $cvc_115 ))) (and (or (or (or (or $cvc_51 $cvc_52 ) $cvc_55 ) $cvc_88 ) $cvc_129 ) (or (or (or (or $cvc_53 $cvc_54 ) $cvc_55 ) $cvc_85 ) $cvc_125 ))) (and (or (or (or (or $cvc_56 $cvc_57 ) $cvc_60 ) $cvc_95 ) $cvc_138 ) (or (or (or (or $cvc_58 $cvc_59 ) $cvc_60 ) $cvc_92 ) $cvc_134 ))) (and (or (or (or (or $cvc_61 $cvc_62 ) $cvc_65 ) $cvc_102 ) $cvc_147 ) (or (or (or (or $cvc_63 $cvc_64 ) $cvc_65 ) $cvc_99 ) $cvc_143 )))) (and (and (and (and (and (or (or (or (or $cvc_66 $cvc_67 ) $cvc_68 ) $cvc_72 ) $cvc_111 ) (or (or (or (or $cvc_69 $cvc_70 ) $cvc_71 ) $cvc_72 ) $cvc_107 )) (and (or (or (or (or $cvc_73 $cvc_74 ) $cvc_75 ) $cvc_81 ) $cvc_121 ) (or (or (or (or $cvc_78 $cvc_79 ) $cvc_80 ) $cvc_81 ) $cvc_116 ))) (and (or (or (or (or $cvc_83 $cvc_84 ) $cvc_85 ) $cvc_89 ) $cvc_130 ) (or (or (or (or $cvc_86 $cvc_87 ) $cvc_88 ) $cvc_89 ) $cvc_126 ))) (and (or (or (or (or $cvc_90 $cvc_91 ) $cvc_92 ) $cvc_96 ) $cvc_139 ) (or (or (or (or $cvc_93 $cvc_94 ) $cvc_95 ) $cvc_96 ) $cvc_135 ))) (and (or (or (or (or $cvc_97 $cvc_98 ) $cvc_99 ) $cvc_103 ) $cvc_148 ) (or (or (or (or $cvc_100 $cvc_101 ) $cvc_102 ) $cvc_103 ) $cvc_144 )))) (and (and (and (and (and (or (or (or (or $cvc_104 $cvc_105 ) $cvc_106 ) $cvc_107 ) $cvc_112 ) (or (or (or (or $cvc_108 $cvc_109 ) $cvc_110 ) $cvc_111 ) $cvc_112 )) (and (or (or (or (or $cvc_113 $cvc_114 ) $cvc_115 ) $cvc_116 ) $cvc_122 ) (or (or (or (or $cvc_118 $cvc_119 ) $cvc_120 ) $cvc_121 ) $cvc_122 ))) (and (or (or (or (or $cvc_123 $cvc_124 ) $cvc_125 ) $cvc_126 ) $cvc_131 ) (or (or (or (or $cvc_127 $cvc_128 ) $cvc_129 ) $cvc_130 ) $cvc_131 ))) (and (or (or (or (or $cvc_132 $cvc_133 ) $cvc_134 ) $cvc_135 ) $cvc_140 ) (or (or (or (or $cvc_136 $cvc_137 ) $cvc_138 ) $cvc_139 ) $cvc_140 ))) (and (or (or (or (or $cvc_141 $cvc_142 ) $cvc_143 ) $cvc_144 ) $cvc_149 ) (or (or (or (or $cvc_145 $cvc_146 ) $cvc_147 ) $cvc_148 ) $cvc_149 ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+ :assumption
+(let (?cvc_0 (op e0 e0)) (let (?cvc_5 (op e0 e1)) (let (?cvc_10 (op e0 e2)) (let (?cvc_15 (op e0 e3)) (let (?cvc_20 (op e0 e4)) (let (?cvc_1 (op e1 e0)) (let (?cvc_6 (op e1 e1)) (let (?cvc_11 (op e1 e2)) (let (?cvc_16 (op e1 e3)) (let (?cvc_21 (op e1 e4)) (let (?cvc_2 (op e2 e0)) (let (?cvc_7 (op e2 e1)) (let (?cvc_12 (op e2 e2)) (let (?cvc_17 (op e2 e3)) (let (?cvc_22 (op e2 e4)) (let (?cvc_3 (op e3 e0)) (let (?cvc_8 (op e3 e1)) (let (?cvc_13 (op e3 e2)) (let (?cvc_18 (op e3 e3)) (let (?cvc_23 (op e3 e4)) (let (?cvc_4 (op e4 e0)) (let (?cvc_9 (op e4 e1)) (let (?cvc_14 (op e4 e2)) (let (?cvc_19 (op e4 e3)) (let (?cvc_24 (op e4 e4)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (= ?cvc_0 ?cvc_1)) (not (= ?cvc_0 ?cvc_2))) (not (= ?cvc_0 ?cvc_3))) (not (= ?cvc_0 ?cvc_4))) (not (= ?cvc_1 ?cvc_2))) (not (= ?cvc_1 ?cvc_3))) (not (= ?cvc_1 ?cvc_4))) (not (= ?cvc_2 ?cvc_3))) (not (= ?cvc_2 ?cvc_4))) (not (= ?cvc_3 ?cvc_4))) (and (and (and (and (and (and (and (and (and (not (= ?cvc_5 ?cvc_6)) (not (= ?cvc_5 ?cvc_7))) (not (= ?cvc_5 ?cvc_8))) (not (= ?cvc_5 ?cvc_9))) (not (= ?cvc_6 ?cvc_7))) (not (= ?cvc_6 ?cvc_8))) (not (= ?cvc_6 ?cvc_9))) (not (= ?cvc_7 ?cvc_8))) (not (= ?cvc_7 ?cvc_9))) (not (= ?cvc_8 ?cvc_9)))) (and (and (and (and (and (and (and (and (and (not (= ?cvc_10 ?cvc_11)) (not (= ?cvc_10 ?cvc_12))) (not (= ?cvc_10 ?cvc_13))) (not (= ?cvc_10 ?cvc_14))) (not (= ?cvc_11 ?cvc_12))) (not (= ?cvc_11 ?cvc_13))) (not (= ?cvc_11 ?cvc_14))) (not (= ?cvc_12 ?cvc_13))) (not (= ?cvc_12 ?cvc_14))) (not (= ?cvc_13 ?cvc_14)))) (and (and (and (and (and (and (and (and (and (not (= ?cvc_15 ?cvc_16)) (not (= ?cvc_15 ?cvc_17))) (not (= ?cvc_15 ?cvc_18))) (not (= ?cvc_15 ?cvc_19))) (not (= ?cvc_16 ?cvc_17))) (not (= ?cvc_16 ?cvc_18))) (not (= ?cvc_16 ?cvc_19))) (not (= ?cvc_17 ?cvc_18))) (not (= ?cvc_17 ?cvc_19))) (not (= ?cvc_18 ?cvc_19)))) (and (and (and (and (and (and (and (and (and (not (= ?cvc_20 ?cvc_21)) (not (= ?cvc_20 ?cvc_22))) (not (= ?cvc_20 ?cvc_23))) (not (= ?cvc_20 ?cvc_24))) (not (= ?cvc_21 ?cvc_22))) (not (= ?cvc_21 ?cvc_23))) (not (= ?cvc_21 ?cvc_24))) (not (= ?cvc_22 ?cvc_23))) (not (= ?cvc_22 ?cvc_24))) (not (= ?cvc_23 ?cvc_24)))) (and (and (and (and (and (and (and (and (and (and (and (and (and (not (= ?cvc_0 ?cvc_5)) (not (= ?cvc_0 ?cvc_10))) (not (= ?cvc_0 ?cvc_15))) (not (= ?cvc_0 ?cvc_20))) (not (= ?cvc_5 ?cvc_10))) (not (= ?cvc_5 ?cvc_15))) (not (= ?cvc_5 ?cvc_20))) (not (= ?cvc_10 ?cvc_15))) (not (= ?cvc_10 ?cvc_20))) (not (= ?cvc_15 ?cvc_20))) (and (and (and (and (and (and (and (and (and (not (= ?cvc_1 ?cvc_6)) (not (= ?cvc_1 ?cvc_11))) (not (= ?cvc_1 ?cvc_16))) (not (= ?cvc_1 ?cvc_21))) (not (= ?cvc_6 ?cvc_11))) (not (= ?cvc_6 ?cvc_16))) (not (= ?cvc_6 ?cvc_21))) (not (= ?cvc_11 ?cvc_16))) (not (= ?cvc_11 ?cvc_21))) (not (= ?cvc_16 ?cvc_21)))) (and (and (and (and (and (and (and (and (and (not (= ?cvc_2 ?cvc_7)) (not (= ?cvc_2 ?cvc_12))) (not (= ?cvc_2 ?cvc_17))) (not (= ?cvc_2 ?cvc_22))) (not (= ?cvc_7 ?cvc_12))) (not (= ?cvc_7 ?cvc_17))) (not (= ?cvc_7 ?cvc_22))) (not (= ?cvc_12 ?cvc_17))) (not (= ?cvc_12 ?cvc_22))) (not (= ?cvc_17 ?cvc_22)))) (and (and (and (and (and (and (and (and (and (not (= ?cvc_3 ?cvc_8)) (not (= ?cvc_3 ?cvc_13))) (not (= ?cvc_3 ?cvc_18))) (not (= ?cvc_3 ?cvc_23))) (not (= ?cvc_8 ?cvc_13))) (not (= ?cvc_8 ?cvc_18))) (not (= ?cvc_8 ?cvc_23))) (not (= ?cvc_13 ?cvc_18))) (not (= ?cvc_13 ?cvc_23))) (not (= ?cvc_18 ?cvc_23)))) (and (and (and (and (and (and (and (and (and (not (= ?cvc_4 ?cvc_9)) (not (= ?cvc_4 ?cvc_14))) (not (= ?cvc_4 ?cvc_19))) (not (= ?cvc_4 ?cvc_24))) (not (= ?cvc_9 ?cvc_14))) (not (= ?cvc_9 ?cvc_19))) (not (= ?cvc_9 ?cvc_24))) (not (= ?cvc_14 ?cvc_19))) (not (= ?cvc_14 ?cvc_24))) (not (= ?cvc_19 ?cvc_24))))))))))))))))))))))))))))))
+ :assumption
+(and (and (and (and (and (and (and (and (and (not (= e0 e1)) (not (= e0 e2))) (not (= e0 e3))) (not (= e0 e4))) (not (= e1 e2))) (not (= e1 e3))) (not (= e1 e4))) (not (= e2 e3))) (not (= e2 e4))) (not (= e3 e4)))
+ :assumption
+(and (and (and (= e0 (op e4 e4)) (= e1 (op e3 e4))) (= e2 (op e3 e1))) (= e4 (op e3 e3)))
+ :assumption
+(not (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= (op e0 e0) e2) (= (op e0 e1) e0)) (= (op e0 e2) e1)) (= (op e0 e3) e3)) (= (op e0 e4) e4)) (= (op e1 e0) e0)) (= (op e1 e1) e1)) (= (op e1 e2) e4)) (= (op e1 e3) e2)) (= (op e1 e4) e3)) (= (op e2 e0) e1)) (= (op e2 e1) e4)) (= (op e2 e2) e3)) (= (op e2 e3) e0)) (= (op e2 e4) e2)) (= (op e3 e0) e3)) (= (op e3 e1) e2)) (= (op e3 e2) e0)) (= (op e3 e3) e4)) (= (op e3 e4) e1)) (= (op e4 e0) e4)) (= (op e4 e1) e3)) (= (op e4 e2) e2)) (= (op e4 e3) e1)) (= (op e4 e4) e0)))
+ :assumption
+(not (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= (op e0 e0) e1) (= (op e0 e1) e0)) (= (op e0 e2) e4)) (= (op e0 e3) e3)) (= (op e0 e4) e2)) (= (op e1 e0) e0)) (= (op e1 e1) e3)) (= (op e1 e2) e1)) (= (op e1 e3) e2)) (= (op e1 e4) e4)) (= (op e2 e0) e4)) (= (op e2 e1) e1)) (= (op e2 e2) e2)) (= (op e2 e3) e0)) (= (op e2 e4) e3)) (= (op e3 e0) e3)) (= (op e3 e1) e2)) (= (op e3 e2) e0)) (= (op e3 e3) e4)) (= (op e3 e4) e1)) (= (op e4 e0) e2)) (= (op e4 e1) e4)) (= (op e4 e2) e3)) (= (op e4 e3) e1)) (= (op e4 e4) e0)))
+ :formula
+(not false)
+)
projects / cvc5.git / commitdiff