mirror of
https://github.com/c-cube/sidekick.git
synced 2025-12-06 03:05:31 -05:00
26 lines
11 KiB
Text
26 lines
11 KiB
Text
(set-logic QF_UF)
|
|
(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 :smt-lib-version 2.0)
|
|
(set-info :category "crafted")
|
|
(set-info :status sat)
|
|
(declare-sort U 0)
|
|
(declare-fun c4 () U)
|
|
(declare-fun f1 (U) U)
|
|
(declare-fun c5 () U)
|
|
(declare-fun f2 (U) U)
|
|
(declare-fun c6 () U)
|
|
(declare-fun f3 (U U) U)
|
|
(declare-fun c7 () U)
|
|
(declare-fun c_0 () U)
|
|
(declare-fun c_1 () U)
|
|
(declare-fun c_2 () U)
|
|
(declare-fun c_3 () U)
|
|
(assert (let ((?v_0 (f1 c4)) (?v_1 (f1 c_0)) (?v_2 (f1 c_1)) (?v_3 (f1 c_2)) (?v_4 (f1 c_3)) (?v_10 (f3 c_0 c_0)) (?v_5 (f2 c_0))) (let ((?v_9 (not (= ?v_1 ?v_5))) (?v_12 (f3 c_0 c_1)) (?v_6 (f2 c_1))) (let ((?v_11 (not (= ?v_1 ?v_6))) (?v_14 (f3 c_0 c_2)) (?v_7 (f2 c_2))) (let ((?v_13 (not (= ?v_1 ?v_7))) (?v_16 (f3 c_0 c_3)) (?v_8 (f2 c_3))) (let ((?v_15 (not (= ?v_1 ?v_8))) (?v_18 (f3 c_1 c_0)) (?v_17 (not (= ?v_2 ?v_5))) (?v_20 (f3 c_1 c_1)) (?v_19 (not (= ?v_2 ?v_6))) (?v_22 (f3 c_1 c_2)) (?v_21 (not (= ?v_2 ?v_7))) (?v_24 (f3 c_1 c_3)) (?v_23 (not (= ?v_2 ?v_8))) (?v_26 (f3 c_2 c_0)) (?v_25 (not (= ?v_3 ?v_5))) (?v_28 (f3 c_2 c_1)) (?v_27 (not (= ?v_3 ?v_6))) (?v_30 (f3 c_2 c_2)) (?v_29 (not (= ?v_3 ?v_7))) (?v_32 (f3 c_2 c_3)) (?v_31 (not (= ?v_3 ?v_8))) (?v_34 (f3 c_3 c_0)) (?v_33 (not (= ?v_4 ?v_5))) (?v_36 (f3 c_3 c_1)) (?v_35 (not (= ?v_4 ?v_6))) (?v_38 (f3 c_3 c_2)) (?v_37 (not (= ?v_4 ?v_7))) (?v_40 (f3 c_3 c_3)) (?v_39 (not (= ?v_4 ?v_8))) (?v_41 (f3 c4 c5))) (let ((?v_45 (f3 c_0 ?v_41))) (let ((?v_42 (not (= ?v_45 c_0))) (?v_44 (f2 ?v_41))) (let ((?v_43 (not (= ?v_1 ?v_44))) (?v_47 (= c_0 c_0)) (?v_48 (f3 c_1 ?v_41))) (let ((?v_59 (not (= ?v_48 c_0))) (?v_49 (= c_1 c_0)) (?v_50 (not (= ?v_2 ?v_44))) (?v_51 (f3 c_2 ?v_41))) (let ((?v_60 (not (= ?v_51 c_0))) (?v_52 (= c_2 c_0)) (?v_53 (not (= ?v_3 ?v_44))) (?v_54 (f3 c_3 ?v_41))) (let ((?v_61 (not (= ?v_54 c_0))) (?v_55 (= c_3 c_0)) (?v_56 (not (= ?v_4 ?v_44))) (?v_46 (not (= ?v_45 c_1))) (?v_62 (not (= ?v_48 c_1))) (?v_65 (not (= ?v_51 c_1))) (?v_67 (not (= ?v_54 c_1))) (?v_57 (not (= ?v_45 c_2))) (?v_69 (not (= ?v_48 c_2))) (?v_70 (not (= ?v_51 c_2))) (?v_71 (not (= ?v_54 c_2))) (?v_58 (not (= ?v_45 c_3))) (?v_72 (not (= ?v_48 c_3))) (?v_73 (not (= ?v_51 c_3))) (?v_74 (not (= ?v_54 c_3))) (?v_63 (= c_0 c_1)) (?v_64 (= c_1 c_1)) (?v_66 (= c_2 c_1)) (?v_68 (= c_3 c_1)) (?v_75 (= c_0 c_2)) (?v_76 (= c_1 c_2)) (?v_77 (= c_2 c_2)) (?v_78 (= c_3 c_2)) (?v_79 (= c_0 c_3)) (?v_80 (= c_1 c_3)) (?v_81 (= c_2 c_3)) (?v_82 (= c_3 c_3))) (and (distinct c_0 c_1 c_2 c_3) (= ?v_0 (f2 c5)) (= ?v_0 (f2 c6)) (= (f2 ?v_1) ?v_1) (= (f2 ?v_2) ?v_2) (= (f2 ?v_3) ?v_3) (= (f2 ?v_4) ?v_4) (or (= (f2 ?v_10) ?v_5) ?v_9) (or (= (f2 ?v_12) ?v_5) ?v_11) (or (= (f2 ?v_14) ?v_5) ?v_13) (or (= (f2 ?v_16) ?v_5) ?v_15) (or (= (f2 ?v_18) ?v_6) ?v_17) (or (= (f2 ?v_20) ?v_6) ?v_19) (or (= (f2 ?v_22) ?v_6) ?v_21) (or (= (f2 ?v_24) ?v_6) ?v_23) (or (= (f2 ?v_26) ?v_7) ?v_25) (or (= (f2 ?v_28) ?v_7) ?v_27) (or (= (f2 ?v_30) ?v_7) ?v_29) (or (= (f2 ?v_32) ?v_7) ?v_31) (or (= (f2 ?v_34) ?v_8) ?v_33) (or (= (f2 ?v_36) ?v_8) ?v_35) (or (= (f2 ?v_38) ?v_8) ?v_37) (or (= (f2 ?v_40) ?v_8) ?v_39) (= (f3 c4 c6) (f3 c4 c7)) (= ?v_0 (f2 c7)) (or ?v_9 (= (f1 ?v_10) ?v_1)) (or ?v_11 (= (f1 ?v_12) ?v_2)) (or ?v_13 (= (f1 ?v_14) ?v_3)) (or ?v_15 (= (f1 ?v_16) ?v_4)) (or ?v_17 (= (f1 ?v_18) ?v_1)) (or ?v_19 (= (f1 ?v_20) ?v_2)) (or ?v_21 (= (f1 ?v_22) ?v_3)) (or ?v_23 (= (f1 ?v_24) ?v_4)) (or ?v_25 (= (f1 ?v_26) ?v_1)) (or ?v_27 (= (f1 ?v_28) ?v_2)) (or ?v_29 (= (f1 ?v_30) ?v_3)) (or ?v_31 (= (f1 ?v_32) ?v_4)) (or ?v_33 (= (f1 ?v_34) ?v_1)) (or ?v_35 (= (f1 ?v_36) ?v_2)) (or ?v_37 (= (f1 ?v_38) ?v_3)) (or ?v_39 (= (f1 ?v_40) ?v_4)) (not (= c6 c7)) (= (f3 ?v_5 c_0) c_0) (= (f3 ?v_6 c_1) c_1) (= (f3 ?v_7 c_2) c_2) (= (f3 ?v_8 c_3) c_3) (or ?v_9 ?v_9 (= (f3 c_0 ?v_10) (f3 ?v_10 c_0))) (or ?v_9 ?v_11 (= (f3 c_0 ?v_12) (f3 ?v_10 c_1))) (or ?v_9 ?v_13 (= (f3 c_0 ?v_14) (f3 ?v_10 c_2))) (or ?v_9 ?v_15 (= (f3 c_0 ?v_16) (f3 ?v_10 c_3))) (or ?v_11 ?v_17 (= (f3 c_0 ?v_18) (f3 ?v_12 c_0))) (or ?v_11 ?v_19 (= (f3 c_0 ?v_20) (f3 ?v_12 c_1))) (or ?v_11 ?v_21 (= (f3 c_0 ?v_22) (f3 ?v_12 c_2))) (or ?v_11 ?v_23 (= (f3 c_0 ?v_24) (f3 ?v_12 c_3))) (or ?v_13 ?v_25 (= (f3 c_0 ?v_26) (f3 ?v_14 c_0))) (or ?v_13 ?v_27 (= (f3 c_0 ?v_28) (f3 ?v_14 c_1))) (or ?v_13 ?v_29 (= (f3 c_0 ?v_30) (f3 ?v_14 c_2))) (or ?v_13 ?v_31 (= (f3 c_0 ?v_32) (f3 ?v_14 c_3))) (or ?v_15 ?v_33 (= (f3 c_0 ?v_34) (f3 ?v_16 c_0))) (or ?v_15 ?v_35 (= (f3 c_0 ?v_36) (f3 ?v_16 c_1))) (or ?v_15 ?v_37 (= (f3 c_0 ?v_38) (f3 ?v_16 c_2))) (or ?v_15 ?v_39 (= (f3 c_0 ?v_40) (f3 ?v_16 c_3))) (or ?v_17 ?v_9 (= (f3 c_1 ?v_10) (f3 ?v_18 c_0))) (or ?v_17 ?v_11 (= (f3 c_1 ?v_12) (f3 ?v_18 c_1))) (or ?v_17 ?v_13 (= (f3 c_1 ?v_14) (f3 ?v_18 c_2))) (or ?v_17 ?v_15 (= (f3 c_1 ?v_16) (f3 ?v_18 c_3))) (or ?v_19 ?v_17 (= (f3 c_1 ?v_18) (f3 ?v_20 c_0))) (or ?v_19 ?v_19 (= (f3 c_1 ?v_20) (f3 ?v_20 c_1))) (or ?v_19 ?v_21 (= (f3 c_1 ?v_22) (f3 ?v_20 c_2))) (or ?v_19 ?v_23 (= (f3 c_1 ?v_24) (f3 ?v_20 c_3))) (or ?v_21 ?v_25 (= (f3 c_1 ?v_26) (f3 ?v_22 c_0))) (or ?v_21 ?v_27 (= (f3 c_1 ?v_28) (f3 ?v_22 c_1))) (or ?v_21 ?v_29 (= (f3 c_1 ?v_30) (f3 ?v_22 c_2))) (or ?v_21 ?v_31 (= (f3 c_1 ?v_32) (f3 ?v_22 c_3))) (or ?v_23 ?v_33 (= (f3 c_1 ?v_34) (f3 ?v_24 c_0))) (or ?v_23 ?v_35 (= (f3 c_1 ?v_36) (f3 ?v_24 c_1))) (or ?v_23 ?v_37 (= (f3 c_1 ?v_38) (f3 ?v_24 c_2))) (or ?v_23 ?v_39 (= (f3 c_1 ?v_40) (f3 ?v_24 c_3))) (or ?v_25 ?v_9 (= (f3 c_2 ?v_10) (f3 ?v_26 c_0))) (or ?v_25 ?v_11 (= (f3 c_2 ?v_12) (f3 ?v_26 c_1))) (or ?v_25 ?v_13 (= (f3 c_2 ?v_14) (f3 ?v_26 c_2))) (or ?v_25 ?v_15 (= (f3 c_2 ?v_16) (f3 ?v_26 c_3))) (or ?v_27 ?v_17 (= (f3 c_2 ?v_18) (f3 ?v_28 c_0))) (or ?v_27 ?v_19 (= (f3 c_2 ?v_20) (f3 ?v_28 c_1))) (or ?v_27 ?v_21 (= (f3 c_2 ?v_22) (f3 ?v_28 c_2))) (or ?v_27 ?v_23 (= (f3 c_2 ?v_24) (f3 ?v_28 c_3))) (or ?v_29 ?v_25 (= (f3 c_2 ?v_26) (f3 ?v_30 c_0))) (or ?v_29 ?v_27 (= (f3 c_2 ?v_28) (f3 ?v_30 c_1))) (or ?v_29 ?v_29 (= (f3 c_2 ?v_30) (f3 ?v_30 c_2))) (or ?v_29 ?v_31 (= (f3 c_2 ?v_32) (f3 ?v_30 c_3))) (or ?v_31 ?v_33 (= (f3 c_2 ?v_34) (f3 ?v_32 c_0))) (or ?v_31 ?v_35 (= (f3 c_2 ?v_36) (f3 ?v_32 c_1))) (or ?v_31 ?v_37 (= (f3 c_2 ?v_38) (f3 ?v_32 c_2))) (or ?v_31 ?v_39 (= (f3 c_2 ?v_40) (f3 ?v_32 c_3))) (or ?v_33 ?v_9 (= (f3 c_3 ?v_10) (f3 ?v_34 c_0))) (or ?v_33 ?v_11 (= (f3 c_3 ?v_12) (f3 ?v_34 c_1))) (or ?v_33 ?v_13 (= (f3 c_3 ?v_14) (f3 ?v_34 c_2))) (or ?v_33 ?v_15 (= (f3 c_3 ?v_16) (f3 ?v_34 c_3))) (or ?v_35 ?v_17 (= (f3 c_3 ?v_18) (f3 ?v_36 c_0))) (or ?v_35 ?v_19 (= (f3 c_3 ?v_20) (f3 ?v_36 c_1))) (or ?v_35 ?v_21 (= (f3 c_3 ?v_22) (f3 ?v_36 c_2))) (or ?v_35 ?v_23 (= (f3 c_3 ?v_24) (f3 ?v_36 c_3))) (or ?v_37 ?v_25 (= (f3 c_3 ?v_26) (f3 ?v_38 c_0))) (or ?v_37 ?v_27 (= (f3 c_3 ?v_28) (f3 ?v_38 c_1))) (or ?v_37 ?v_29 (= (f3 c_3 ?v_30) (f3 ?v_38 c_2))) (or ?v_37 ?v_31 (= (f3 c_3 ?v_32) (f3 ?v_38 c_3))) (or ?v_39 ?v_33 (= (f3 c_3 ?v_34) (f3 ?v_40 c_0))) (or ?v_39 ?v_35 (= (f3 c_3 ?v_36) (f3 ?v_40 c_1))) (or ?v_39 ?v_37 (= (f3 c_3 ?v_38) (f3 ?v_40 c_2))) (or ?v_39 ?v_39 (= (f3 c_3 ?v_40) (f3 ?v_40 c_3))) (= (f1 ?v_5) ?v_5) (= (f1 ?v_6) ?v_6) (= (f1 ?v_7) ?v_7) (= (f1 ?v_8) ?v_8) (or ?v_42 ?v_43 ?v_42 ?v_47 ?v_43) (or ?v_42 ?v_43 ?v_59 ?v_49 ?v_50) (or ?v_42 ?v_43 ?v_60 ?v_52 ?v_53) (or ?v_42 ?v_43 ?v_61 ?v_55 ?v_56) (or ?v_46 ?v_43 ?v_46 ?v_47 ?v_43) (or ?v_46 ?v_43 ?v_62 ?v_49 ?v_50) (or ?v_46 ?v_43 ?v_65 ?v_52 ?v_53) (or ?v_46 ?v_43 ?v_67 ?v_55 ?v_56) (or ?v_57 ?v_43 ?v_57 ?v_47 ?v_43) (or ?v_57 ?v_43 ?v_69 ?v_49 ?v_50) (or ?v_57 ?v_43 ?v_70 ?v_52 ?v_53) (or ?v_57 ?v_43 ?v_71 ?v_55 ?v_56) (or ?v_58 ?v_43 ?v_58 ?v_47 ?v_43) (or ?v_58 ?v_43 ?v_72 ?v_49 ?v_50) (or ?v_58 ?v_43 ?v_73 ?v_52 ?v_53) (or ?v_58 ?v_43 ?v_74 ?v_55 ?v_56) (or ?v_59 ?v_50 ?v_42 ?v_63 ?v_43) (or ?v_59 ?v_50 ?v_59 ?v_64 ?v_50) (or ?v_59 ?v_50 ?v_60 ?v_66 ?v_53) (or ?v_59 ?v_50 ?v_61 ?v_68 ?v_56) (or ?v_62 ?v_50 ?v_46 ?v_63 ?v_43) (or ?v_62 ?v_50 ?v_62 ?v_64 ?v_50) (or ?v_62 ?v_50 ?v_65 ?v_66 ?v_53) (or ?v_62 ?v_50 ?v_67 ?v_68 ?v_56) (or ?v_69 ?v_50 ?v_57 ?v_63 ?v_43) (or ?v_69 ?v_50 ?v_69 ?v_64 ?v_50) (or ?v_69 ?v_50 ?v_70 ?v_66 ?v_53) (or ?v_69 ?v_50 ?v_71 ?v_68 ?v_56) (or ?v_72 ?v_50 ?v_58 ?v_63 ?v_43) (or ?v_72 ?v_50 ?v_72 ?v_64 ?v_50) (or ?v_72 ?v_50 ?v_73 ?v_66 ?v_53) (or ?v_72 ?v_50 ?v_74 ?v_68 ?v_56) (or ?v_60 ?v_53 ?v_42 ?v_75 ?v_43) (or ?v_60 ?v_53 ?v_59 ?v_76 ?v_50) (or ?v_60 ?v_53 ?v_60 ?v_77 ?v_53) (or ?v_60 ?v_53 ?v_61 ?v_78 ?v_56) (or ?v_65 ?v_53 ?v_46 ?v_75 ?v_43) (or ?v_65 ?v_53 ?v_62 ?v_76 ?v_50) (or ?v_65 ?v_53 ?v_65 ?v_77 ?v_53) (or ?v_65 ?v_53 ?v_67 ?v_78 ?v_56) (or ?v_70 ?v_53 ?v_57 ?v_75 ?v_43) (or ?v_70 ?v_53 ?v_69 ?v_76 ?v_50) (or ?v_70 ?v_53 ?v_70 ?v_77 ?v_53) (or ?v_70 ?v_53 ?v_71 ?v_78 ?v_56) (or ?v_73 ?v_53 ?v_58 ?v_75 ?v_43) (or ?v_73 ?v_53 ?v_72 ?v_76 ?v_50) (or ?v_73 ?v_53 ?v_73 ?v_77 ?v_53) (or ?v_73 ?v_53 ?v_74 ?v_78 ?v_56) (or ?v_61 ?v_56 ?v_42 ?v_79 ?v_43) (or ?v_61 ?v_56 ?v_59 ?v_80 ?v_50) (or ?v_61 ?v_56 ?v_60 ?v_81 ?v_53) (or ?v_61 ?v_56 ?v_61 ?v_82 ?v_56) (or ?v_67 ?v_56 ?v_46 ?v_79 ?v_43) (or ?v_67 ?v_56 ?v_62 ?v_80 ?v_50) (or ?v_67 ?v_56 ?v_65 ?v_81 ?v_53) (or ?v_67 ?v_56 ?v_67 ?v_82 ?v_56) (or ?v_71 ?v_56 ?v_57 ?v_79 ?v_43) (or ?v_71 ?v_56 ?v_69 ?v_80 ?v_50) (or ?v_71 ?v_56 ?v_70 ?v_81 ?v_53) (or ?v_71 ?v_56 ?v_71 ?v_82 ?v_56) (or ?v_74 ?v_56 ?v_58 ?v_79 ?v_43) (or ?v_74 ?v_56 ?v_72 ?v_80 ?v_50) (or ?v_74 ?v_56 ?v_73 ?v_81 ?v_53) (or ?v_74 ?v_56 ?v_74 ?v_82 ?v_56) (= (f3 c_0 ?v_1) c_0) (= (f3 c_1 ?v_2) c_1) (= (f3 c_2 ?v_3) c_2) (= (f3 c_3 ?v_4) c_3) (or (= ?v_10 c_0) (= ?v_10 c_1) (= ?v_10 c_2) (= ?v_10 c_3)) (or (= ?v_12 c_0) (= ?v_12 c_1) (= ?v_12 c_2) (= ?v_12 c_3)) (or (= ?v_14 c_0) (= ?v_14 c_1) (= ?v_14 c_2) (= ?v_14 c_3)) (or (= ?v_16 c_0) (= ?v_16 c_1) (= ?v_16 c_2) (= ?v_16 c_3)) (or (= ?v_18 c_0) (= ?v_18 c_1) (= ?v_18 c_2) (= ?v_18 c_3)) (or (= ?v_20 c_0) (= ?v_20 c_1) (= ?v_20 c_2) (= ?v_20 c_3)) (or (= ?v_22 c_0) (= ?v_22 c_1) (= ?v_22 c_2) (= ?v_22 c_3)) (or (= ?v_24 c_0) (= ?v_24 c_1) (= ?v_24 c_2) (= ?v_24 c_3)) (or (= ?v_26 c_0) (= ?v_26 c_1) (= ?v_26 c_2) (= ?v_26 c_3)) (or (= ?v_28 c_0) (= ?v_28 c_1) (= ?v_28 c_2) (= ?v_28 c_3)) (or (= ?v_30 c_0) (= ?v_30 c_1) (= ?v_30 c_2) (= ?v_30 c_3)) (or (= ?v_32 c_0) (= ?v_32 c_1) (= ?v_32 c_2) (= ?v_32 c_3)) (or (= ?v_34 c_0) (= ?v_34 c_1) (= ?v_34 c_2) (= ?v_34 c_3)) (or (= ?v_36 c_0) (= ?v_36 c_1) (= ?v_36 c_2) (= ?v_36 c_3)) (or (= ?v_38 c_0) (= ?v_38 c_1) (= ?v_38 c_2) (= ?v_38 c_3)) (or (= ?v_40 c_0) (= ?v_40 c_1) (= ?v_40 c_2) (= ?v_40 c_3)) (or (= ?v_1 c_0) (= ?v_1 c_1) (= ?v_1 c_2) (= ?v_1 c_3)) (or (= ?v_2 c_0) (= ?v_2 c_1) (= ?v_2 c_2) (= ?v_2 c_3)) (or (= ?v_3 c_0) (= ?v_3 c_1) (= ?v_3 c_2) (= ?v_3 c_3)) (or (= ?v_4 c_0) (= ?v_4 c_1) (= ?v_4 c_2) (= ?v_4 c_3)) (or (= ?v_5 c_0) (= ?v_5 c_1) (= ?v_5 c_2) (= ?v_5 c_3)) (or (= ?v_6 c_0) (= ?v_6 c_1) (= ?v_6 c_2) (= ?v_6 c_3)) (or (= ?v_7 c_0) (= ?v_7 c_1) (= ?v_7 c_2) (= ?v_7 c_3)) (or (= ?v_8 c_0) (= ?v_8 c_1) (= ?v_8 c_2) (= ?v_8 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)))))))))))))))
|
|
(check-sat)
|
|
(exit)
|