path: root/test/regress/regress3/PEQ018_size4.smtv1.smt2

(set-option :incremental false)
(set-info :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).")
(set-info :status unsat)
(set-info :category "crafted")
(set-info :difficulty "0")
(set-logic QF_UF)
(declare-sort U 0)
(declare-fun f1 (U U) U)
(declare-fun f2 (U) U)
(declare-fun c10 () U)
(declare-fun c11 () U)
(declare-fun c3 () U)
(declare-fun c4 () U)
(declare-fun c5 () U)
(declare-fun c6 () U)
(declare-fun c7 () U)
(declare-fun c8 () U)
(declare-fun c9 () U)
(declare-fun c_0 () U)
(declare-fun c_1 () U)
(declare-fun c_2 () U)
(declare-fun c_3 () U)
(check-sat-assuming ( (let ((_let_0 (f1 c_0 c_0))) (let ((_let_1 (f2 _let_0))) (let ((_let_2 (f1 c_0 c_1))) (let ((_let_3 (f2 _let_2))) (let ((_let_4 (f1 c_0 c_2))) (let ((_let_5 (f2 _let_4))) (let ((_let_6 (f1 c_0 c_3))) (let ((_let_7 (f2 _let_6))) (let ((_let_8 (f1 c_1 c_0))) (let ((_let_9 (f1 c_1 c_1))) (let ((_let_10 (f1 c_1 c_2))) (let ((_let_11 (f1 c_1 c_3))) (let ((_let_12 (f1 c_2 c_0))) (let ((_let_13 (f1 c_2 c_1))) (let ((_let_14 (f1 c_2 c_2))) (let ((_let_15 (f1 c_2 c_3))) (let ((_let_16 (f1 c_3 c_0))) (let ((_let_17 (f1 c_3 c_1))) (let ((_let_18 (f1 c_3 c_2))) (let ((_let_19 (f1 c_3 c_3))) (let ((_let_20 (f2 _let_8))) (let ((_let_21 (f2 _let_9))) (let ((_let_22 (f2 _let_10))) (let ((_let_23 (f2 _let_11))) (let ((_let_24 (f2 _let_12))) (let ((_let_25 (f2 _let_13))) (let ((_let_26 (f2 _let_14))) (let ((_let_27 (f2 _let_15))) (let ((_let_28 (f2 _let_16))) (let ((_let_29 (f2 _let_17))) (let ((_let_30 (f2 _let_18))) (let ((_let_31 (f2 _let_19))) (let ((_let_32 (f2 c_0))) (let ((_let_33 (f2 c_1))) (let ((_let_34 (f2 c_2))) (let ((_let_35 (f2 c_3))) (and (distinct c_0 c_1 c_2 c_3) (= (f1 c_0 (f1 _let_0 _let_1)) c_0) (= (f1 c_0 (f1 _let_2 _let_3)) c_0) (= (f1 c_0 (f1 _let_4 _let_5)) c_0) (= (f1 c_0 (f1 _let_6 _let_7)) c_0) (= (f1 c_0 (f1 _let_8 _let_1)) c_1) (= (f1 c_0 (f1 _let_9 _let_3)) c_1) (= (f1 c_0 (f1 _let_10 _let_5)) c_1) (= (f1 c_0 (f1 _let_11 _let_7)) c_1) (= (f1 c_0 (f1 _let_12 _let_1)) c_2) (= (f1 c_0 (f1 _let_13 _let_3)) c_2) (= (f1 c_0 (f1 _let_14 _let_5)) c_2) (= (f1 c_0 (f1 _let_15 _let_7)) c_2) (= (f1 c_0 (f1 _let_16 _let_1)) c_3) (= (f1 c_0 (f1 _let_17 _let_3)) c_3) (= (f1 c_0 (f1 _let_18 _let_5)) c_3) (= (f1 c_0 (f1 _let_19 _let_7)) c_3) (= (f1 c_1 (f1 _let_0 _let_20)) c_0) (= (f1 c_1 (f1 _let_2 _let_21)) c_0) (= (f1 c_1 (f1 _let_4 _let_22)) c_0) (= (f1 c_1 (f1 _let_6 _let_23)) c_0) (= (f1 c_1 (f1 _let_8 _let_20)) c_1) (= (f1 c_1 (f1 _let_9 _let_21)) c_1) (= (f1 c_1 (f1 _let_10 _let_22)) c_1) (= (f1 c_1 (f1 _let_11 _let_23)) c_1) (= (f1 c_1 (f1 _let_12 _let_20)) c_2) (= (f1 c_1 (f1 _let_13 _let_21)) c_2) (= (f1 c_1 (f1 _let_14 _let_22)) c_2) (= (f1 c_1 (f1 _let_15 _let_23)) c_2) (= (f1 c_1 (f1 _let_16 _let_20)) c_3) (= (f1 c_1 (f1 _let_17 _let_21)) c_3) (= (f1 c_1 (f1 _let_18 _let_22)) c_3) (= (f1 c_1 (f1 _let_19 _let_23)) c_3) (= (f1 c_2 (f1 _let_0 _let_24)) c_0) (= (f1 c_2 (f1 _let_2 _let_25)) c_0) (= (f1 c_2 (f1 _let_4 _let_26)) c_0) (= (f1 c_2 (f1 _let_6 _let_27)) c_0) (= (f1 c_2 (f1 _let_8 _let_24)) c_1) (= (f1 c_2 (f1 _let_9 _let_25)) c_1) (= (f1 c_2 (f1 _let_10 _let_26)) c_1) (= (f1 c_2 (f1 _let_11 _let_27)) c_1) (= (f1 c_2 (f1 _let_12 _let_24)) c_2) (= (f1 c_2 (f1 _let_13 _let_25)) c_2) (= (f1 c_2 (f1 _let_14 _let_26)) c_2) (= (f1 c_2 (f1 _let_15 _let_27)) c_2) (= (f1 c_2 (f1 _let_16 _let_24)) c_3) (= (f1 c_2 (f1 _let_17 _let_25)) c_3) (= (f1 c_2 (f1 _let_18 _let_26)) c_3) (= (f1 c_2 (f1 _let_19 _let_27)) c_3) (= (f1 c_3 (f1 _let_0 _let_28)) c_0) (= (f1 c_3 (f1 _let_2 _let_29)) c_0) (= (f1 c_3 (f1 _let_4 _let_30)) c_0) (= (f1 c_3 (f1 _let_6 _let_31)) c_0) (= (f1 c_3 (f1 _let_8 _let_28)) c_1) (= (f1 c_3 (f1 _let_9 _let_29)) c_1) (= (f1 c_3 (f1 _let_10 _let_30)) c_1) (= (f1 c_3 (f1 _let_11 _let_31)) c_1) (= (f1 c_3 (f1 _let_12 _let_28)) c_2) (= (f1 c_3 (f1 _let_13 _let_29)) c_2) (= (f1 c_3 (f1 _let_14 _let_30)) c_2) (= (f1 c_3 (f1 _let_15 _let_31)) c_2) (= (f1 c_3 (f1 _let_16 _let_28)) c_3) (= (f1 c_3 (f1 _let_17 _let_29)) c_3) (= (f1 c_3 (f1 _let_18 _let_30)) c_3) (= (f1 c_3 (f1 _let_19 _let_31)) 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 (= _let_0 c_0) (= _let_0 c_1) (= _let_0 c_2) (= _let_0 c_3)) (or (= _let_2 c_0) (= _let_2 c_1) (= _let_2 c_2) (= _let_2 c_3)) (or (= _let_4 c_0) (= _let_4 c_1) (= _let_4 c_2) (= _let_4 c_3)) (or (= _let_6 c_0) (= _let_6 c_1) (= _let_6 c_2) (= _let_6 c_3)) (or (= _let_8 c_0) (= _let_8 c_1) (= _let_8 c_2) (= _let_8 c_3)) (or (= _let_9 c_0) (= _let_9 c_1) (= _let_9 c_2) (= _let_9 c_3)) (or (= _let_10 c_0) (= _let_10 c_1) (= _let_10 c_2) (= _let_10 c_3)) (or (= _let_11 c_0) (= _let_11 c_1) (= _let_11 c_2) (= _let_11 c_3)) (or (= _let_12 c_0) (= _let_12 c_1) (= _let_12 c_2) (= _let_12 c_3)) (or (= _let_13 c_0) (= _let_13 c_1) (= _let_13 c_2) (= _let_13 c_3)) (or (= _let_14 c_0) (= _let_14 c_1) (= _let_14 c_2) (= _let_14 c_3)) (or (= _let_15 c_0) (= _let_15 c_1) (= _let_15 c_2) (= _let_15 c_3)) (or (= _let_16 c_0) (= _let_16 c_1) (= _let_16 c_2) (= _let_16 c_3)) (or (= _let_17 c_0) (= _let_17 c_1) (= _let_17 c_2) (= _let_17 c_3)) (or (= _let_18 c_0) (= _let_18 c_1) (= _let_18 c_2) (= _let_18 c_3)) (or (= _let_19 c_0) (= _let_19 c_1) (= _let_19 c_2) (= _let_19 c_3)) (or (= _let_32 c_0) (= _let_32 c_1) (= _let_32 c_2) (= _let_32 c_3)) (or (= _let_33 c_0) (= _let_33 c_1) (= _let_33 c_2) (= _let_33 c_3)) (or (= _let_34 c_0) (= _let_34 c_1) (= _let_34 c_2) (= _let_34 c_3)) (or (= _let_35 c_0) (= _let_35 c_1) (= _let_35 c_2) (= _let_35 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))))))))))))))))))))))))))))))))))))))) ))