From: Andrew Reynolds Date: Tue, 27 Apr 2021 21:58:25 +0000 (-0500) Subject: Move slow regression to regress3 (#6451) X-Git-Tag: cvc5-1.0.0~1821 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=145d58ae0146ba591cd0d5531208e78abd849019;p=cvc5.git Move slow regression to regress3 (#6451) Benchmark is taking 40 seconds on production, due to the configuration that tests --check-unsat-cores. --- diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index f2d017e02..8773c3583 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -2374,7 +2374,6 @@ set(regress_2_tests regress2/ho/SYO362^5.p regress2/hole7.cvc regress2/hole8.cvc - regress2/hole10.cvc regress2/instance_1444.smtv1.smt2 regress2/issue3687-check-models.smt2 regress2/issue4707-bv-to-bool-large.smt2 @@ -2474,6 +2473,7 @@ set(regress_3_tests regress3/friedman_n4_i5.smtv1.smt2 regress3/friedman_n6_i4.smtv1.smt2 regress3/hole9.cvc + regress3/hole10.cvc regress3/incorrect1.smtv1.smt2 regress3/interpol2.smt2 regress3/inv_gen_n_c11.sy diff --git a/test/regress/regress2/hole10.cvc b/test/regress/regress2/hole10.cvc deleted file mode 100644 index fb4c41b35..000000000 --- a/test/regress/regress2/hole10.cvc +++ /dev/null @@ -1,675 +0,0 @@ -% EXPECT: entailed -x_1 : BOOLEAN; -x_2 : BOOLEAN; -x_3 : BOOLEAN; -x_4 : BOOLEAN; -x_5 : BOOLEAN; -x_6 : BOOLEAN; -x_7 : BOOLEAN; -x_8 : BOOLEAN; -x_9 : BOOLEAN; -x_10 : BOOLEAN; -x_11 : BOOLEAN; -x_12 : BOOLEAN; -x_13 : BOOLEAN; -x_14 : BOOLEAN; -x_15 : BOOLEAN; -x_16 : BOOLEAN; -x_17 : BOOLEAN; -x_18 : BOOLEAN; -x_19 : BOOLEAN; -x_20 : BOOLEAN; -x_21 : BOOLEAN; -x_22 : BOOLEAN; -x_23 : BOOLEAN; -x_24 : BOOLEAN; -x_25 : BOOLEAN; -x_26 : BOOLEAN; -x_27 : BOOLEAN; -x_28 : BOOLEAN; -x_29 : BOOLEAN; -x_30 : BOOLEAN; -x_31 : BOOLEAN; -x_32 : BOOLEAN; -x_33 : BOOLEAN; -x_34 : BOOLEAN; -x_35 : BOOLEAN; -x_36 : BOOLEAN; -x_37 : BOOLEAN; -x_38 : BOOLEAN; -x_39 : BOOLEAN; -x_40 : BOOLEAN; -x_41 : BOOLEAN; -x_42 : BOOLEAN; -x_43 : BOOLEAN; -x_44 : BOOLEAN; -x_45 : BOOLEAN; -x_46 : BOOLEAN; -x_47 : BOOLEAN; -x_48 : BOOLEAN; -x_49 : BOOLEAN; -x_50 : BOOLEAN; -x_51 : BOOLEAN; -x_52 : BOOLEAN; -x_53 : BOOLEAN; -x_54 : BOOLEAN; -x_55 : BOOLEAN; -x_56 : BOOLEAN; -x_57 : BOOLEAN; -x_58 : BOOLEAN; -x_59 : BOOLEAN; -x_60 : BOOLEAN; -x_61 : BOOLEAN; -x_62 : BOOLEAN; -x_63 : BOOLEAN; -x_64 : BOOLEAN; -x_65 : BOOLEAN; -x_66 : BOOLEAN; -x_67 : BOOLEAN; -x_68 : BOOLEAN; -x_69 : BOOLEAN; -x_70 : BOOLEAN; -x_71 : BOOLEAN; -x_72 : BOOLEAN; -x_73 : BOOLEAN; -x_74 : BOOLEAN; -x_75 : BOOLEAN; -x_76 : BOOLEAN; -x_77 : BOOLEAN; -x_78 : BOOLEAN; -x_79 : BOOLEAN; -x_80 : BOOLEAN; -x_81 : BOOLEAN; -x_82 : BOOLEAN; -x_83 : BOOLEAN; -x_84 : BOOLEAN; -x_85 : BOOLEAN; -x_86 : BOOLEAN; -x_87 : BOOLEAN; -x_88 : BOOLEAN; -x_89 : BOOLEAN; -x_90 : BOOLEAN; -x_91 : BOOLEAN; -x_92 : BOOLEAN; -x_93 : BOOLEAN; -x_94 : BOOLEAN; -x_95 : BOOLEAN; -x_96 : BOOLEAN; -x_97 : BOOLEAN; -x_98 : BOOLEAN; -x_99 : BOOLEAN; -x_100 : BOOLEAN; -x_101 : BOOLEAN; -x_102 : BOOLEAN; -x_103 : BOOLEAN; -x_104 : BOOLEAN; -x_105 : BOOLEAN; -x_106 : BOOLEAN; -x_107 : BOOLEAN; -x_108 : BOOLEAN; -x_109 : BOOLEAN; -x_110 : BOOLEAN; -ASSERT NOT x_1 OR NOT x_11; -ASSERT NOT x_1 OR NOT x_21; -ASSERT NOT x_1 OR NOT x_31; -ASSERT NOT x_1 OR NOT x_41; -ASSERT NOT x_1 OR NOT x_51; -ASSERT NOT x_1 OR NOT x_61; -ASSERT NOT x_1 OR NOT x_71; -ASSERT NOT x_1 OR NOT x_81; -ASSERT NOT x_1 OR NOT x_91; -ASSERT NOT x_1 OR NOT x_101; -ASSERT NOT x_11 OR NOT x_21; -ASSERT NOT x_11 OR NOT x_31; -ASSERT NOT x_11 OR NOT x_41; -ASSERT NOT x_11 OR NOT x_51; -ASSERT NOT x_11 OR NOT x_61; -ASSERT NOT x_11 OR NOT x_71; -ASSERT NOT x_11 OR NOT x_81; -ASSERT NOT x_11 OR NOT x_91; -ASSERT NOT x_11 OR NOT x_101; -ASSERT NOT x_21 OR NOT x_31; -ASSERT NOT x_21 OR NOT x_41; -ASSERT NOT x_21 OR NOT x_51; -ASSERT NOT x_21 OR NOT x_61; -ASSERT NOT x_21 OR NOT x_71; -ASSERT NOT x_21 OR NOT x_81; -ASSERT NOT x_21 OR NOT x_91; -ASSERT NOT x_21 OR NOT x_101; -ASSERT NOT x_31 OR NOT x_41; -ASSERT NOT x_31 OR NOT x_51; -ASSERT NOT x_31 OR NOT x_61; -ASSERT NOT x_31 OR NOT x_71; -ASSERT NOT x_31 OR NOT x_81; -ASSERT NOT x_31 OR NOT x_91; -ASSERT NOT x_31 OR NOT x_101; -ASSERT NOT x_41 OR NOT x_51; -ASSERT NOT x_41 OR NOT x_61; -ASSERT NOT x_41 OR NOT x_71; -ASSERT NOT x_41 OR NOT x_81; -ASSERT NOT x_41 OR NOT x_91; -ASSERT NOT x_41 OR NOT x_101; -ASSERT NOT x_51 OR NOT x_61; -ASSERT NOT x_51 OR NOT x_71; -ASSERT NOT x_51 OR NOT x_81; -ASSERT NOT x_51 OR NOT x_91; -ASSERT NOT x_51 OR NOT x_101; -ASSERT NOT x_61 OR NOT x_71; -ASSERT NOT x_61 OR NOT x_81; -ASSERT NOT x_61 OR NOT x_91; -ASSERT NOT x_61 OR NOT x_101; -ASSERT NOT x_71 OR NOT x_81; -ASSERT NOT x_71 OR NOT x_91; -ASSERT NOT x_71 OR NOT x_101; -ASSERT NOT x_81 OR NOT x_91; -ASSERT NOT x_81 OR NOT x_101; -ASSERT NOT x_91 OR NOT x_101; -ASSERT NOT x_2 OR NOT x_12; -ASSERT NOT x_2 OR NOT x_22; -ASSERT NOT x_2 OR NOT x_32; -ASSERT NOT x_2 OR NOT x_42; -ASSERT NOT x_2 OR NOT x_52; -ASSERT NOT x_2 OR NOT x_62; -ASSERT NOT x_2 OR NOT x_72; -ASSERT NOT x_2 OR NOT x_82; -ASSERT NOT x_2 OR NOT x_92; -ASSERT NOT x_2 OR NOT x_102; -ASSERT NOT x_12 OR NOT x_22; -ASSERT NOT x_12 OR NOT x_32; -ASSERT NOT x_12 OR NOT x_42; -ASSERT NOT x_12 OR NOT x_52; -ASSERT NOT x_12 OR NOT x_62; -ASSERT NOT x_12 OR NOT x_72; -ASSERT NOT x_12 OR NOT x_82; -ASSERT NOT x_12 OR NOT x_92; -ASSERT NOT x_12 OR NOT x_102; -ASSERT NOT x_22 OR NOT x_32; -ASSERT NOT x_22 OR NOT x_42; -ASSERT NOT x_22 OR NOT x_52; -ASSERT NOT x_22 OR NOT x_62; -ASSERT NOT x_22 OR NOT x_72; -ASSERT NOT x_22 OR NOT x_82; -ASSERT NOT x_22 OR NOT x_92; -ASSERT NOT x_22 OR NOT x_102; -ASSERT NOT x_32 OR NOT x_42; -ASSERT NOT x_32 OR NOT x_52; -ASSERT NOT x_32 OR NOT x_62; -ASSERT NOT x_32 OR NOT x_72; -ASSERT NOT x_32 OR NOT x_82; -ASSERT NOT x_32 OR NOT x_92; -ASSERT NOT x_32 OR NOT x_102; -ASSERT NOT x_42 OR NOT x_52; -ASSERT NOT x_42 OR NOT x_62; -ASSERT NOT x_42 OR NOT x_72; -ASSERT NOT x_42 OR NOT x_82; -ASSERT NOT x_42 OR NOT x_92; -ASSERT NOT x_42 OR NOT x_102; -ASSERT NOT x_52 OR NOT x_62; -ASSERT NOT x_52 OR NOT x_72; -ASSERT NOT x_52 OR NOT x_82; -ASSERT NOT x_52 OR NOT x_92; -ASSERT NOT x_52 OR NOT x_102; -ASSERT NOT x_62 OR NOT x_72; -ASSERT NOT x_62 OR NOT x_82; -ASSERT NOT x_62 OR NOT x_92; -ASSERT NOT x_62 OR NOT x_102; -ASSERT NOT x_72 OR NOT x_82; -ASSERT NOT x_72 OR NOT x_92; -ASSERT NOT x_72 OR NOT x_102; -ASSERT NOT x_82 OR NOT x_92; -ASSERT NOT x_82 OR NOT x_102; -ASSERT NOT x_92 OR NOT x_102; -ASSERT NOT x_3 OR NOT x_13; -ASSERT NOT x_3 OR NOT x_23; -ASSERT NOT x_3 OR NOT x_33; -ASSERT NOT x_3 OR NOT x_43; -ASSERT NOT x_3 OR NOT x_53; -ASSERT NOT x_3 OR NOT x_63; -ASSERT NOT x_3 OR NOT x_73; -ASSERT NOT x_3 OR NOT x_83; -ASSERT NOT x_3 OR NOT x_93; -ASSERT NOT x_3 OR NOT x_103; -ASSERT NOT x_13 OR NOT x_23; -ASSERT NOT x_13 OR NOT x_33; -ASSERT NOT x_13 OR NOT x_43; -ASSERT NOT x_13 OR NOT x_53; -ASSERT NOT x_13 OR NOT x_63; -ASSERT NOT x_13 OR NOT x_73; -ASSERT NOT x_13 OR NOT x_83; -ASSERT NOT x_13 OR NOT x_93; -ASSERT NOT x_13 OR NOT x_103; -ASSERT NOT x_23 OR NOT x_33; -ASSERT NOT x_23 OR NOT x_43; -ASSERT NOT x_23 OR NOT x_53; -ASSERT NOT x_23 OR NOT x_63; -ASSERT NOT x_23 OR NOT x_73; -ASSERT NOT x_23 OR NOT x_83; -ASSERT NOT x_23 OR NOT x_93; -ASSERT NOT x_23 OR NOT x_103; -ASSERT NOT x_33 OR NOT x_43; -ASSERT NOT x_33 OR NOT x_53; -ASSERT NOT x_33 OR NOT x_63; -ASSERT NOT x_33 OR NOT x_73; -ASSERT NOT x_33 OR NOT x_83; -ASSERT NOT x_33 OR NOT x_93; -ASSERT NOT x_33 OR NOT x_103; -ASSERT NOT x_43 OR NOT x_53; -ASSERT NOT x_43 OR NOT x_63; -ASSERT NOT x_43 OR NOT x_73; -ASSERT NOT x_43 OR NOT x_83; -ASSERT NOT x_43 OR NOT x_93; -ASSERT NOT x_43 OR NOT x_103; -ASSERT NOT x_53 OR NOT x_63; -ASSERT NOT x_53 OR NOT x_73; -ASSERT NOT x_53 OR NOT x_83; -ASSERT NOT x_53 OR NOT x_93; -ASSERT NOT x_53 OR NOT x_103; -ASSERT NOT x_63 OR NOT x_73; -ASSERT NOT x_63 OR NOT x_83; -ASSERT NOT x_63 OR NOT x_93; -ASSERT NOT x_63 OR NOT x_103; -ASSERT NOT x_73 OR NOT x_83; -ASSERT NOT x_73 OR NOT x_93; -ASSERT NOT x_73 OR NOT x_103; -ASSERT NOT x_83 OR NOT x_93; -ASSERT NOT x_83 OR NOT x_103; -ASSERT NOT x_93 OR NOT x_103; -ASSERT NOT x_4 OR NOT x_14; -ASSERT NOT x_4 OR NOT x_24; -ASSERT NOT x_4 OR NOT x_34; -ASSERT NOT x_4 OR NOT x_44; -ASSERT NOT x_4 OR NOT x_54; -ASSERT NOT x_4 OR NOT x_64; -ASSERT NOT x_4 OR NOT x_74; -ASSERT NOT x_4 OR NOT x_84; -ASSERT NOT x_4 OR NOT x_94; -ASSERT NOT x_4 OR NOT x_104; -ASSERT NOT x_14 OR NOT x_24; -ASSERT NOT x_14 OR NOT x_34; -ASSERT NOT x_14 OR NOT x_44; -ASSERT NOT x_14 OR NOT x_54; -ASSERT NOT x_14 OR NOT x_64; -ASSERT NOT x_14 OR NOT x_74; -ASSERT NOT x_14 OR NOT x_84; -ASSERT NOT x_14 OR NOT x_94; -ASSERT NOT x_14 OR NOT x_104; -ASSERT NOT x_24 OR NOT x_34; -ASSERT NOT x_24 OR NOT x_44; -ASSERT NOT x_24 OR NOT x_54; -ASSERT NOT x_24 OR NOT x_64; -ASSERT NOT x_24 OR NOT x_74; -ASSERT NOT x_24 OR NOT x_84; -ASSERT NOT x_24 OR NOT x_94; -ASSERT NOT x_24 OR NOT x_104; -ASSERT NOT x_34 OR NOT x_44; -ASSERT NOT x_34 OR NOT x_54; -ASSERT NOT x_34 OR NOT x_64; -ASSERT NOT x_34 OR NOT x_74; -ASSERT NOT x_34 OR NOT x_84; -ASSERT NOT x_34 OR NOT x_94; -ASSERT NOT x_34 OR NOT x_104; -ASSERT NOT x_44 OR NOT x_54; -ASSERT NOT x_44 OR NOT x_64; -ASSERT NOT x_44 OR NOT x_74; -ASSERT NOT x_44 OR NOT x_84; -ASSERT NOT x_44 OR NOT x_94; -ASSERT NOT x_44 OR NOT x_104; -ASSERT NOT x_54 OR NOT x_64; -ASSERT NOT x_54 OR NOT x_74; -ASSERT NOT x_54 OR NOT x_84; -ASSERT NOT x_54 OR NOT x_94; -ASSERT NOT x_54 OR NOT x_104; -ASSERT NOT x_64 OR NOT x_74; -ASSERT NOT x_64 OR NOT x_84; -ASSERT NOT x_64 OR NOT x_94; -ASSERT NOT x_64 OR NOT x_104; -ASSERT NOT x_74 OR NOT x_84; -ASSERT NOT x_74 OR NOT x_94; -ASSERT NOT x_74 OR NOT x_104; -ASSERT NOT x_84 OR NOT x_94; -ASSERT NOT x_84 OR NOT x_104; -ASSERT NOT x_94 OR NOT x_104; -ASSERT NOT x_5 OR NOT x_15; -ASSERT NOT x_5 OR NOT x_25; -ASSERT NOT x_5 OR NOT x_35; -ASSERT NOT x_5 OR NOT x_45; -ASSERT NOT x_5 OR NOT x_55; -ASSERT NOT x_5 OR NOT x_65; -ASSERT NOT x_5 OR NOT x_75; -ASSERT NOT x_5 OR NOT x_85; -ASSERT NOT x_5 OR NOT x_95; -ASSERT NOT x_5 OR NOT x_105; -ASSERT NOT x_15 OR NOT x_25; -ASSERT NOT x_15 OR NOT x_35; -ASSERT NOT x_15 OR NOT x_45; -ASSERT NOT x_15 OR NOT x_55; -ASSERT NOT x_15 OR NOT x_65; -ASSERT NOT x_15 OR NOT x_75; -ASSERT NOT x_15 OR NOT x_85; -ASSERT NOT x_15 OR NOT x_95; -ASSERT NOT x_15 OR NOT x_105; -ASSERT NOT x_25 OR NOT x_35; -ASSERT NOT x_25 OR NOT x_45; -ASSERT NOT x_25 OR NOT x_55; -ASSERT NOT x_25 OR NOT x_65; -ASSERT NOT x_25 OR NOT x_75; -ASSERT NOT x_25 OR NOT x_85; -ASSERT NOT x_25 OR NOT x_95; -ASSERT NOT x_25 OR NOT x_105; -ASSERT NOT x_35 OR NOT x_45; -ASSERT NOT x_35 OR NOT x_55; -ASSERT NOT x_35 OR NOT x_65; -ASSERT NOT x_35 OR NOT x_75; -ASSERT NOT x_35 OR NOT x_85; -ASSERT NOT x_35 OR NOT x_95; -ASSERT NOT x_35 OR NOT x_105; -ASSERT NOT x_45 OR NOT x_55; -ASSERT NOT x_45 OR NOT x_65; -ASSERT NOT x_45 OR NOT x_75; -ASSERT NOT x_45 OR NOT x_85; -ASSERT NOT x_45 OR NOT x_95; -ASSERT NOT x_45 OR NOT x_105; -ASSERT NOT x_55 OR NOT x_65; -ASSERT NOT x_55 OR NOT x_75; -ASSERT NOT x_55 OR NOT x_85; -ASSERT NOT x_55 OR NOT x_95; -ASSERT NOT x_55 OR NOT x_105; -ASSERT NOT x_65 OR NOT x_75; -ASSERT NOT x_65 OR NOT x_85; -ASSERT NOT x_65 OR NOT x_95; -ASSERT NOT x_65 OR NOT x_105; -ASSERT NOT x_75 OR NOT x_85; -ASSERT NOT x_75 OR NOT x_95; -ASSERT NOT x_75 OR NOT x_105; -ASSERT NOT x_85 OR NOT x_95; -ASSERT NOT x_85 OR NOT x_105; -ASSERT NOT x_95 OR NOT x_105; -ASSERT NOT x_6 OR NOT x_16; -ASSERT NOT x_6 OR NOT x_26; -ASSERT NOT x_6 OR NOT x_36; -ASSERT NOT x_6 OR NOT x_46; -ASSERT NOT x_6 OR NOT x_56; -ASSERT NOT x_6 OR NOT x_66; -ASSERT NOT x_6 OR NOT x_76; -ASSERT NOT x_6 OR NOT x_86; -ASSERT NOT x_6 OR NOT x_96; -ASSERT NOT x_6 OR NOT x_106; -ASSERT NOT x_16 OR NOT x_26; -ASSERT NOT x_16 OR NOT x_36; -ASSERT NOT x_16 OR NOT x_46; -ASSERT NOT x_16 OR NOT x_56; -ASSERT NOT x_16 OR NOT x_66; -ASSERT NOT x_16 OR NOT x_76; -ASSERT NOT x_16 OR NOT x_86; -ASSERT NOT x_16 OR NOT x_96; -ASSERT NOT x_16 OR NOT x_106; -ASSERT NOT x_26 OR NOT x_36; -ASSERT NOT x_26 OR NOT x_46; -ASSERT NOT x_26 OR NOT x_56; -ASSERT NOT x_26 OR NOT x_66; -ASSERT NOT x_26 OR NOT x_76; -ASSERT NOT x_26 OR NOT x_86; -ASSERT NOT x_26 OR NOT x_96; -ASSERT NOT x_26 OR NOT x_106; -ASSERT NOT x_36 OR NOT x_46; -ASSERT NOT x_36 OR NOT x_56; -ASSERT NOT x_36 OR NOT x_66; -ASSERT NOT x_36 OR NOT x_76; -ASSERT NOT x_36 OR NOT x_86; -ASSERT NOT x_36 OR NOT x_96; -ASSERT NOT x_36 OR NOT x_106; -ASSERT NOT x_46 OR NOT x_56; -ASSERT NOT x_46 OR NOT x_66; -ASSERT NOT x_46 OR NOT x_76; -ASSERT NOT x_46 OR NOT x_86; -ASSERT NOT x_46 OR NOT x_96; -ASSERT NOT x_46 OR NOT x_106; -ASSERT NOT x_56 OR NOT x_66; -ASSERT NOT x_56 OR NOT x_76; -ASSERT NOT x_56 OR NOT x_86; -ASSERT NOT x_56 OR NOT x_96; -ASSERT NOT x_56 OR NOT x_106; -ASSERT NOT x_66 OR NOT x_76; -ASSERT NOT x_66 OR NOT x_86; -ASSERT NOT x_66 OR NOT x_96; -ASSERT NOT x_66 OR NOT x_106; -ASSERT NOT x_76 OR NOT x_86; -ASSERT NOT x_76 OR NOT x_96; -ASSERT NOT x_76 OR NOT x_106; -ASSERT NOT x_86 OR NOT x_96; -ASSERT NOT x_86 OR NOT x_106; -ASSERT NOT x_96 OR NOT x_106; -ASSERT NOT x_7 OR NOT x_17; -ASSERT NOT x_7 OR NOT x_27; -ASSERT NOT x_7 OR NOT x_37; -ASSERT NOT x_7 OR NOT x_47; -ASSERT NOT x_7 OR NOT x_57; -ASSERT NOT x_7 OR NOT x_67; -ASSERT NOT x_7 OR NOT x_77; -ASSERT NOT x_7 OR NOT x_87; -ASSERT NOT x_7 OR NOT x_97; -ASSERT NOT x_7 OR NOT x_107; -ASSERT NOT x_17 OR NOT x_27; -ASSERT NOT x_17 OR NOT x_37; -ASSERT NOT x_17 OR NOT x_47; -ASSERT NOT x_17 OR NOT x_57; -ASSERT NOT x_17 OR NOT x_67; -ASSERT NOT x_17 OR NOT x_77; -ASSERT NOT x_17 OR NOT x_87; -ASSERT NOT x_17 OR NOT x_97; -ASSERT NOT x_17 OR NOT x_107; -ASSERT NOT x_27 OR NOT x_37; -ASSERT NOT x_27 OR NOT x_47; -ASSERT NOT x_27 OR NOT x_57; -ASSERT NOT x_27 OR NOT x_67; -ASSERT NOT x_27 OR NOT x_77; -ASSERT NOT x_27 OR NOT x_87; -ASSERT NOT x_27 OR NOT x_97; -ASSERT NOT x_27 OR NOT x_107; -ASSERT NOT x_37 OR NOT x_47; -ASSERT NOT x_37 OR NOT x_57; -ASSERT NOT x_37 OR NOT x_67; -ASSERT NOT x_37 OR NOT x_77; -ASSERT NOT x_37 OR NOT x_87; -ASSERT NOT x_37 OR NOT x_97; -ASSERT NOT x_37 OR NOT x_107; -ASSERT NOT x_47 OR NOT x_57; -ASSERT NOT x_47 OR NOT x_67; -ASSERT NOT x_47 OR NOT x_77; -ASSERT NOT x_47 OR NOT x_87; -ASSERT NOT x_47 OR NOT x_97; -ASSERT NOT x_47 OR NOT x_107; -ASSERT NOT x_57 OR NOT x_67; -ASSERT NOT x_57 OR NOT x_77; -ASSERT NOT x_57 OR NOT x_87; -ASSERT NOT x_57 OR NOT x_97; -ASSERT NOT x_57 OR NOT x_107; -ASSERT NOT x_67 OR NOT x_77; -ASSERT NOT x_67 OR NOT x_87; -ASSERT NOT x_67 OR NOT x_97; -ASSERT NOT x_67 OR NOT x_107; -ASSERT NOT x_77 OR NOT x_87; -ASSERT NOT x_77 OR NOT x_97; -ASSERT NOT x_77 OR NOT x_107; -ASSERT NOT x_87 OR NOT x_97; -ASSERT NOT x_87 OR NOT x_107; -ASSERT NOT x_97 OR NOT x_107; -ASSERT NOT x_8 OR NOT x_18; -ASSERT NOT x_8 OR NOT x_28; -ASSERT NOT x_8 OR NOT x_38; -ASSERT NOT x_8 OR NOT x_48; -ASSERT NOT x_8 OR NOT x_58; -ASSERT NOT x_8 OR NOT x_68; -ASSERT NOT x_8 OR NOT x_78; -ASSERT NOT x_8 OR NOT x_88; -ASSERT NOT x_8 OR NOT x_98; -ASSERT NOT x_8 OR NOT x_108; -ASSERT NOT x_18 OR NOT x_28; -ASSERT NOT x_18 OR NOT x_38; -ASSERT NOT x_18 OR NOT x_48; -ASSERT NOT x_18 OR NOT x_58; -ASSERT NOT x_18 OR NOT x_68; -ASSERT NOT x_18 OR NOT x_78; -ASSERT NOT x_18 OR NOT x_88; -ASSERT NOT x_18 OR NOT x_98; -ASSERT NOT x_18 OR NOT x_108; -ASSERT NOT x_28 OR NOT x_38; -ASSERT NOT x_28 OR NOT x_48; -ASSERT NOT x_28 OR NOT x_58; -ASSERT NOT x_28 OR NOT x_68; -ASSERT NOT x_28 OR NOT x_78; -ASSERT NOT x_28 OR NOT x_88; -ASSERT NOT x_28 OR NOT x_98; -ASSERT NOT x_28 OR NOT x_108; -ASSERT NOT x_38 OR NOT x_48; -ASSERT NOT x_38 OR NOT x_58; -ASSERT NOT x_38 OR NOT x_68; -ASSERT NOT x_38 OR NOT x_78; -ASSERT NOT x_38 OR NOT x_88; -ASSERT NOT x_38 OR NOT x_98; -ASSERT NOT x_38 OR NOT x_108; -ASSERT NOT x_48 OR NOT x_58; -ASSERT NOT x_48 OR NOT x_68; -ASSERT NOT x_48 OR NOT x_78; -ASSERT NOT x_48 OR NOT x_88; -ASSERT NOT x_48 OR NOT x_98; -ASSERT NOT x_48 OR NOT x_108; -ASSERT NOT x_58 OR NOT x_68; -ASSERT NOT x_58 OR NOT x_78; -ASSERT NOT x_58 OR NOT x_88; -ASSERT NOT x_58 OR NOT x_98; -ASSERT NOT x_58 OR NOT x_108; -ASSERT NOT x_68 OR NOT x_78; -ASSERT NOT x_68 OR NOT x_88; -ASSERT NOT x_68 OR NOT x_98; -ASSERT NOT x_68 OR NOT x_108; -ASSERT NOT x_78 OR NOT x_88; -ASSERT NOT x_78 OR NOT x_98; -ASSERT NOT x_78 OR NOT x_108; -ASSERT NOT x_88 OR NOT x_98; -ASSERT NOT x_88 OR NOT x_108; -ASSERT NOT x_98 OR NOT x_108; -ASSERT NOT x_9 OR NOT x_19; -ASSERT NOT x_9 OR NOT x_29; -ASSERT NOT x_9 OR NOT x_39; -ASSERT NOT x_9 OR NOT x_49; -ASSERT NOT x_9 OR NOT x_59; -ASSERT NOT x_9 OR NOT x_69; -ASSERT NOT x_9 OR NOT x_79; -ASSERT NOT x_9 OR NOT x_89; -ASSERT NOT x_9 OR NOT x_99; -ASSERT NOT x_9 OR NOT x_109; -ASSERT NOT x_19 OR NOT x_29; -ASSERT NOT x_19 OR NOT x_39; -ASSERT NOT x_19 OR NOT x_49; -ASSERT NOT x_19 OR NOT x_59; -ASSERT NOT x_19 OR NOT x_69; -ASSERT NOT x_19 OR NOT x_79; -ASSERT NOT x_19 OR NOT x_89; -ASSERT NOT x_19 OR NOT x_99; -ASSERT NOT x_19 OR NOT x_109; -ASSERT NOT x_29 OR NOT x_39; -ASSERT NOT x_29 OR NOT x_49; -ASSERT NOT x_29 OR NOT x_59; -ASSERT NOT x_29 OR NOT x_69; -ASSERT NOT x_29 OR NOT x_79; -ASSERT NOT x_29 OR NOT x_89; -ASSERT NOT x_29 OR NOT x_99; -ASSERT NOT x_29 OR NOT x_109; -ASSERT NOT x_39 OR NOT x_49; -ASSERT NOT x_39 OR NOT x_59; -ASSERT NOT x_39 OR NOT x_69; -ASSERT NOT x_39 OR NOT x_79; -ASSERT NOT x_39 OR NOT x_89; -ASSERT NOT x_39 OR NOT x_99; -ASSERT NOT x_39 OR NOT x_109; -ASSERT NOT x_49 OR NOT x_59; -ASSERT NOT x_49 OR NOT x_69; -ASSERT NOT x_49 OR NOT x_79; -ASSERT NOT x_49 OR NOT x_89; -ASSERT NOT x_49 OR NOT x_99; -ASSERT NOT x_49 OR NOT x_109; -ASSERT NOT x_59 OR NOT x_69; -ASSERT NOT x_59 OR NOT x_79; -ASSERT NOT x_59 OR NOT x_89; -ASSERT NOT x_59 OR NOT x_99; -ASSERT NOT x_59 OR NOT x_109; -ASSERT NOT x_69 OR NOT x_79; -ASSERT NOT x_69 OR NOT x_89; -ASSERT NOT x_69 OR NOT x_99; -ASSERT NOT x_69 OR NOT x_109; -ASSERT NOT x_79 OR NOT x_89; -ASSERT NOT x_79 OR NOT x_99; -ASSERT NOT x_79 OR NOT x_109; -ASSERT NOT x_89 OR NOT x_99; -ASSERT NOT x_89 OR NOT x_109; -ASSERT NOT x_99 OR NOT x_109; -ASSERT NOT x_10 OR NOT x_20; -ASSERT NOT x_10 OR NOT x_30; -ASSERT NOT x_10 OR NOT x_40; -ASSERT NOT x_10 OR NOT x_50; -ASSERT NOT x_10 OR NOT x_60; -ASSERT NOT x_10 OR NOT x_70; -ASSERT NOT x_10 OR NOT x_80; -ASSERT NOT x_10 OR NOT x_90; -ASSERT NOT x_10 OR NOT x_100; -ASSERT NOT x_10 OR NOT x_110; -ASSERT NOT x_20 OR NOT x_30; -ASSERT NOT x_20 OR NOT x_40; -ASSERT NOT x_20 OR NOT x_50; -ASSERT NOT x_20 OR NOT x_60; -ASSERT NOT x_20 OR NOT x_70; -ASSERT NOT x_20 OR NOT x_80; -ASSERT NOT x_20 OR NOT x_90; -ASSERT NOT x_20 OR NOT x_100; -ASSERT NOT x_20 OR NOT x_110; -ASSERT NOT x_30 OR NOT x_40; -ASSERT NOT x_30 OR NOT x_50; -ASSERT NOT x_30 OR NOT x_60; -ASSERT NOT x_30 OR NOT x_70; -ASSERT NOT x_30 OR NOT x_80; -ASSERT NOT x_30 OR NOT x_90; -ASSERT NOT x_30 OR NOT x_100; -ASSERT NOT x_30 OR NOT x_110; -ASSERT NOT x_40 OR NOT x_50; -ASSERT NOT x_40 OR NOT x_60; -ASSERT NOT x_40 OR NOT x_70; -ASSERT NOT x_40 OR NOT x_80; -ASSERT NOT x_40 OR NOT x_90; -ASSERT NOT x_40 OR NOT x_100; -ASSERT NOT x_40 OR NOT x_110; -ASSERT NOT x_50 OR NOT x_60; -ASSERT NOT x_50 OR NOT x_70; -ASSERT NOT x_50 OR NOT x_80; -ASSERT NOT x_50 OR NOT x_90; -ASSERT NOT x_50 OR NOT x_100; -ASSERT NOT x_50 OR NOT x_110; -ASSERT NOT x_60 OR NOT x_70; -ASSERT NOT x_60 OR NOT x_80; -ASSERT NOT x_60 OR NOT x_90; -ASSERT NOT x_60 OR NOT x_100; -ASSERT NOT x_60 OR NOT x_110; -ASSERT NOT x_70 OR NOT x_80; -ASSERT NOT x_70 OR NOT x_90; -ASSERT NOT x_70 OR NOT x_100; -ASSERT NOT x_70 OR NOT x_110; -ASSERT NOT x_80 OR NOT x_90; -ASSERT NOT x_80 OR NOT x_100; -ASSERT NOT x_80 OR NOT x_110; -ASSERT NOT x_90 OR NOT x_100; -ASSERT NOT x_90 OR NOT x_110; -ASSERT NOT x_100 OR NOT x_110; -ASSERT x_10 OR x_9 OR x_8 OR x_7 OR x_6 OR x_5 OR x_4 OR x_3 OR x_2 OR x_1; -ASSERT x_20 OR x_19 OR x_18 OR x_17 OR x_16 OR x_15 OR x_14 OR x_13 OR x_12 OR x_11; -ASSERT x_30 OR x_29 OR x_28 OR x_27 OR x_26 OR x_25 OR x_24 OR x_23 OR x_22 OR x_21; -ASSERT x_40 OR x_39 OR x_38 OR x_37 OR x_36 OR x_35 OR x_34 OR x_33 OR x_32 OR x_31; -ASSERT x_50 OR x_49 OR x_48 OR x_47 OR x_46 OR x_45 OR x_44 OR x_43 OR x_42 OR x_41; -ASSERT x_60 OR x_59 OR x_58 OR x_57 OR x_56 OR x_55 OR x_54 OR x_53 OR x_52 OR x_51; -ASSERT x_70 OR x_69 OR x_68 OR x_67 OR x_66 OR x_65 OR x_64 OR x_63 OR x_62 OR x_61; -ASSERT x_80 OR x_79 OR x_78 OR x_77 OR x_76 OR x_75 OR x_74 OR x_73 OR x_72 OR x_71; -ASSERT x_90 OR x_89 OR x_88 OR x_87 OR x_86 OR x_85 OR x_84 OR x_83 OR x_82 OR x_81; -ASSERT x_100 OR x_99 OR x_98 OR x_97 OR x_96 OR x_95 OR x_94 OR x_93 OR x_92 OR x_91; -ASSERT x_110 OR x_109 OR x_108 OR x_107 OR x_106 OR x_105 OR x_104 OR x_103 OR x_102 OR x_101; - - -QUERY FALSE; diff --git a/test/regress/regress3/hole10.cvc b/test/regress/regress3/hole10.cvc new file mode 100644 index 000000000..fb4c41b35 --- /dev/null +++ b/test/regress/regress3/hole10.cvc @@ -0,0 +1,675 @@ +% EXPECT: entailed +x_1 : BOOLEAN; +x_2 : BOOLEAN; +x_3 : BOOLEAN; +x_4 : BOOLEAN; +x_5 : BOOLEAN; +x_6 : BOOLEAN; +x_7 : BOOLEAN; +x_8 : BOOLEAN; +x_9 : BOOLEAN; +x_10 : BOOLEAN; +x_11 : BOOLEAN; +x_12 : BOOLEAN; +x_13 : BOOLEAN; +x_14 : BOOLEAN; +x_15 : BOOLEAN; +x_16 : BOOLEAN; +x_17 : BOOLEAN; +x_18 : BOOLEAN; +x_19 : BOOLEAN; +x_20 : BOOLEAN; +x_21 : BOOLEAN; +x_22 : BOOLEAN; +x_23 : BOOLEAN; +x_24 : BOOLEAN; +x_25 : BOOLEAN; +x_26 : BOOLEAN; +x_27 : BOOLEAN; +x_28 : BOOLEAN; +x_29 : BOOLEAN; +x_30 : BOOLEAN; +x_31 : BOOLEAN; +x_32 : BOOLEAN; +x_33 : BOOLEAN; +x_34 : BOOLEAN; +x_35 : BOOLEAN; +x_36 : BOOLEAN; +x_37 : BOOLEAN; +x_38 : BOOLEAN; +x_39 : BOOLEAN; +x_40 : BOOLEAN; +x_41 : BOOLEAN; +x_42 : BOOLEAN; +x_43 : BOOLEAN; +x_44 : BOOLEAN; +x_45 : BOOLEAN; +x_46 : BOOLEAN; +x_47 : BOOLEAN; +x_48 : BOOLEAN; +x_49 : BOOLEAN; +x_50 : BOOLEAN; +x_51 : BOOLEAN; +x_52 : BOOLEAN; +x_53 : BOOLEAN; +x_54 : BOOLEAN; +x_55 : BOOLEAN; +x_56 : BOOLEAN; +x_57 : BOOLEAN; +x_58 : BOOLEAN; +x_59 : BOOLEAN; +x_60 : BOOLEAN; +x_61 : BOOLEAN; +x_62 : BOOLEAN; +x_63 : BOOLEAN; +x_64 : BOOLEAN; +x_65 : BOOLEAN; +x_66 : BOOLEAN; +x_67 : BOOLEAN; +x_68 : BOOLEAN; +x_69 : BOOLEAN; +x_70 : BOOLEAN; +x_71 : BOOLEAN; +x_72 : BOOLEAN; +x_73 : BOOLEAN; +x_74 : BOOLEAN; +x_75 : BOOLEAN; +x_76 : BOOLEAN; +x_77 : BOOLEAN; +x_78 : BOOLEAN; +x_79 : BOOLEAN; +x_80 : BOOLEAN; +x_81 : BOOLEAN; +x_82 : BOOLEAN; +x_83 : BOOLEAN; +x_84 : BOOLEAN; +x_85 : BOOLEAN; +x_86 : BOOLEAN; +x_87 : BOOLEAN; +x_88 : BOOLEAN; +x_89 : BOOLEAN; +x_90 : BOOLEAN; +x_91 : BOOLEAN; +x_92 : BOOLEAN; +x_93 : BOOLEAN; +x_94 : BOOLEAN; +x_95 : BOOLEAN; +x_96 : BOOLEAN; +x_97 : BOOLEAN; +x_98 : BOOLEAN; +x_99 : BOOLEAN; +x_100 : BOOLEAN; +x_101 : BOOLEAN; +x_102 : BOOLEAN; +x_103 : BOOLEAN; +x_104 : BOOLEAN; +x_105 : BOOLEAN; +x_106 : BOOLEAN; +x_107 : BOOLEAN; +x_108 : BOOLEAN; +x_109 : BOOLEAN; +x_110 : BOOLEAN; +ASSERT NOT x_1 OR NOT x_11; +ASSERT NOT x_1 OR NOT x_21; +ASSERT NOT x_1 OR NOT x_31; +ASSERT NOT x_1 OR NOT x_41; +ASSERT NOT x_1 OR NOT x_51; +ASSERT NOT x_1 OR NOT x_61; +ASSERT NOT x_1 OR NOT x_71; +ASSERT NOT x_1 OR NOT x_81; +ASSERT NOT x_1 OR NOT x_91; +ASSERT NOT x_1 OR NOT x_101; +ASSERT NOT x_11 OR NOT x_21; +ASSERT NOT x_11 OR NOT x_31; +ASSERT NOT x_11 OR NOT x_41; +ASSERT NOT x_11 OR NOT x_51; +ASSERT NOT x_11 OR NOT x_61; +ASSERT NOT x_11 OR NOT x_71; +ASSERT NOT x_11 OR NOT x_81; +ASSERT NOT x_11 OR NOT x_91; +ASSERT NOT x_11 OR NOT x_101; +ASSERT NOT x_21 OR NOT x_31; +ASSERT NOT x_21 OR NOT x_41; +ASSERT NOT x_21 OR NOT x_51; +ASSERT NOT x_21 OR NOT x_61; +ASSERT NOT x_21 OR NOT x_71; +ASSERT NOT x_21 OR NOT x_81; +ASSERT NOT x_21 OR NOT x_91; +ASSERT NOT x_21 OR NOT x_101; +ASSERT NOT x_31 OR NOT x_41; +ASSERT NOT x_31 OR NOT x_51; +ASSERT NOT x_31 OR NOT x_61; +ASSERT NOT x_31 OR NOT x_71; +ASSERT NOT x_31 OR NOT x_81; +ASSERT NOT x_31 OR NOT x_91; +ASSERT NOT x_31 OR NOT x_101; +ASSERT NOT x_41 OR NOT x_51; +ASSERT NOT x_41 OR NOT x_61; +ASSERT NOT x_41 OR NOT x_71; +ASSERT NOT x_41 OR NOT x_81; +ASSERT NOT x_41 OR NOT x_91; +ASSERT NOT x_41 OR NOT x_101; +ASSERT NOT x_51 OR NOT x_61; +ASSERT NOT x_51 OR NOT x_71; +ASSERT NOT x_51 OR NOT x_81; +ASSERT NOT x_51 OR NOT x_91; +ASSERT NOT x_51 OR NOT x_101; +ASSERT NOT x_61 OR NOT x_71; +ASSERT NOT x_61 OR NOT x_81; +ASSERT NOT x_61 OR NOT x_91; +ASSERT NOT x_61 OR NOT x_101; +ASSERT NOT x_71 OR NOT x_81; +ASSERT NOT x_71 OR NOT x_91; +ASSERT NOT x_71 OR NOT x_101; +ASSERT NOT x_81 OR NOT x_91; +ASSERT NOT x_81 OR NOT x_101; +ASSERT NOT x_91 OR NOT x_101; +ASSERT NOT x_2 OR NOT x_12; +ASSERT NOT x_2 OR NOT x_22; +ASSERT NOT x_2 OR NOT x_32; +ASSERT NOT x_2 OR NOT x_42; +ASSERT NOT x_2 OR NOT x_52; +ASSERT NOT x_2 OR NOT x_62; +ASSERT NOT x_2 OR NOT x_72; +ASSERT NOT x_2 OR NOT x_82; +ASSERT NOT x_2 OR NOT x_92; +ASSERT NOT x_2 OR NOT x_102; +ASSERT NOT x_12 OR NOT x_22; +ASSERT NOT x_12 OR NOT x_32; +ASSERT NOT x_12 OR NOT x_42; +ASSERT NOT x_12 OR NOT x_52; +ASSERT NOT x_12 OR NOT x_62; +ASSERT NOT x_12 OR NOT x_72; +ASSERT NOT x_12 OR NOT x_82; +ASSERT NOT x_12 OR NOT x_92; +ASSERT NOT x_12 OR NOT x_102; +ASSERT NOT x_22 OR NOT x_32; +ASSERT NOT x_22 OR NOT x_42; +ASSERT NOT x_22 OR NOT x_52; +ASSERT NOT x_22 OR NOT x_62; +ASSERT NOT x_22 OR NOT x_72; +ASSERT NOT x_22 OR NOT x_82; +ASSERT NOT x_22 OR NOT x_92; +ASSERT NOT x_22 OR NOT x_102; +ASSERT NOT x_32 OR NOT x_42; +ASSERT NOT x_32 OR NOT x_52; +ASSERT NOT x_32 OR NOT x_62; +ASSERT NOT x_32 OR NOT x_72; +ASSERT NOT x_32 OR NOT x_82; +ASSERT NOT x_32 OR NOT x_92; +ASSERT NOT x_32 OR NOT x_102; +ASSERT NOT x_42 OR NOT x_52; +ASSERT NOT x_42 OR NOT x_62; +ASSERT NOT x_42 OR NOT x_72; +ASSERT NOT x_42 OR NOT x_82; +ASSERT NOT x_42 OR NOT x_92; +ASSERT NOT x_42 OR NOT x_102; +ASSERT NOT x_52 OR NOT x_62; +ASSERT NOT x_52 OR NOT x_72; +ASSERT NOT x_52 OR NOT x_82; +ASSERT NOT x_52 OR NOT x_92; +ASSERT NOT x_52 OR NOT x_102; +ASSERT NOT x_62 OR NOT x_72; +ASSERT NOT x_62 OR NOT x_82; +ASSERT NOT x_62 OR NOT x_92; +ASSERT NOT x_62 OR NOT x_102; +ASSERT NOT x_72 OR NOT x_82; +ASSERT NOT x_72 OR NOT x_92; +ASSERT NOT x_72 OR NOT x_102; +ASSERT NOT x_82 OR NOT x_92; +ASSERT NOT x_82 OR NOT x_102; +ASSERT NOT x_92 OR NOT x_102; +ASSERT NOT x_3 OR NOT x_13; +ASSERT NOT x_3 OR NOT x_23; +ASSERT NOT x_3 OR NOT x_33; +ASSERT NOT x_3 OR NOT x_43; +ASSERT NOT x_3 OR NOT x_53; +ASSERT NOT x_3 OR NOT x_63; +ASSERT NOT x_3 OR NOT x_73; +ASSERT NOT x_3 OR NOT x_83; +ASSERT NOT x_3 OR NOT x_93; +ASSERT NOT x_3 OR NOT x_103; +ASSERT NOT x_13 OR NOT x_23; +ASSERT NOT x_13 OR NOT x_33; +ASSERT NOT x_13 OR NOT x_43; +ASSERT NOT x_13 OR NOT x_53; +ASSERT NOT x_13 OR NOT x_63; +ASSERT NOT x_13 OR NOT x_73; +ASSERT NOT x_13 OR NOT x_83; +ASSERT NOT x_13 OR NOT x_93; +ASSERT NOT x_13 OR NOT x_103; +ASSERT NOT x_23 OR NOT x_33; +ASSERT NOT x_23 OR NOT x_43; +ASSERT NOT x_23 OR NOT x_53; +ASSERT NOT x_23 OR NOT x_63; +ASSERT NOT x_23 OR NOT x_73; +ASSERT NOT x_23 OR NOT x_83; +ASSERT NOT x_23 OR NOT x_93; +ASSERT NOT x_23 OR NOT x_103; +ASSERT NOT x_33 OR NOT x_43; +ASSERT NOT x_33 OR NOT x_53; +ASSERT NOT x_33 OR NOT x_63; +ASSERT NOT x_33 OR NOT x_73; +ASSERT NOT x_33 OR NOT x_83; +ASSERT NOT x_33 OR NOT x_93; +ASSERT NOT x_33 OR NOT x_103; +ASSERT NOT x_43 OR NOT x_53; +ASSERT NOT x_43 OR NOT x_63; +ASSERT NOT x_43 OR NOT x_73; +ASSERT NOT x_43 OR NOT x_83; +ASSERT NOT x_43 OR NOT x_93; +ASSERT NOT x_43 OR NOT x_103; +ASSERT NOT x_53 OR NOT x_63; +ASSERT NOT x_53 OR NOT x_73; +ASSERT NOT x_53 OR NOT x_83; +ASSERT NOT x_53 OR NOT x_93; +ASSERT NOT x_53 OR NOT x_103; +ASSERT NOT x_63 OR NOT x_73; +ASSERT NOT x_63 OR NOT x_83; +ASSERT NOT x_63 OR NOT x_93; +ASSERT NOT x_63 OR NOT x_103; +ASSERT NOT x_73 OR NOT x_83; +ASSERT NOT x_73 OR NOT x_93; +ASSERT NOT x_73 OR NOT x_103; +ASSERT NOT x_83 OR NOT x_93; +ASSERT NOT x_83 OR NOT x_103; +ASSERT NOT x_93 OR NOT x_103; +ASSERT NOT x_4 OR NOT x_14; +ASSERT NOT x_4 OR NOT x_24; +ASSERT NOT x_4 OR NOT x_34; +ASSERT NOT x_4 OR NOT x_44; +ASSERT NOT x_4 OR NOT x_54; +ASSERT NOT x_4 OR NOT x_64; +ASSERT NOT x_4 OR NOT x_74; +ASSERT NOT x_4 OR NOT x_84; +ASSERT NOT x_4 OR NOT x_94; +ASSERT NOT x_4 OR NOT x_104; +ASSERT NOT x_14 OR NOT x_24; +ASSERT NOT x_14 OR NOT x_34; +ASSERT NOT x_14 OR NOT x_44; +ASSERT NOT x_14 OR NOT x_54; +ASSERT NOT x_14 OR NOT x_64; +ASSERT NOT x_14 OR NOT x_74; +ASSERT NOT x_14 OR NOT x_84; +ASSERT NOT x_14 OR NOT x_94; +ASSERT NOT x_14 OR NOT x_104; +ASSERT NOT x_24 OR NOT x_34; +ASSERT NOT x_24 OR NOT x_44; +ASSERT NOT x_24 OR NOT x_54; +ASSERT NOT x_24 OR NOT x_64; +ASSERT NOT x_24 OR NOT x_74; +ASSERT NOT x_24 OR NOT x_84; +ASSERT NOT x_24 OR NOT x_94; +ASSERT NOT x_24 OR NOT x_104; +ASSERT NOT x_34 OR NOT x_44; +ASSERT NOT x_34 OR NOT x_54; +ASSERT NOT x_34 OR NOT x_64; +ASSERT NOT x_34 OR NOT x_74; +ASSERT NOT x_34 OR NOT x_84; +ASSERT NOT x_34 OR NOT x_94; +ASSERT NOT x_34 OR NOT x_104; +ASSERT NOT x_44 OR NOT x_54; +ASSERT NOT x_44 OR NOT x_64; +ASSERT NOT x_44 OR NOT x_74; +ASSERT NOT x_44 OR NOT x_84; +ASSERT NOT x_44 OR NOT x_94; +ASSERT NOT x_44 OR NOT x_104; +ASSERT NOT x_54 OR NOT x_64; +ASSERT NOT x_54 OR NOT x_74; +ASSERT NOT x_54 OR NOT x_84; +ASSERT NOT x_54 OR NOT x_94; +ASSERT NOT x_54 OR NOT x_104; +ASSERT NOT x_64 OR NOT x_74; +ASSERT NOT x_64 OR NOT x_84; +ASSERT NOT x_64 OR NOT x_94; +ASSERT NOT x_64 OR NOT x_104; +ASSERT NOT x_74 OR NOT x_84; +ASSERT NOT x_74 OR NOT x_94; +ASSERT NOT x_74 OR NOT x_104; +ASSERT NOT x_84 OR NOT x_94; +ASSERT NOT x_84 OR NOT x_104; +ASSERT NOT x_94 OR NOT x_104; +ASSERT NOT x_5 OR NOT x_15; +ASSERT NOT x_5 OR NOT x_25; +ASSERT NOT x_5 OR NOT x_35; +ASSERT NOT x_5 OR NOT x_45; +ASSERT NOT x_5 OR NOT x_55; +ASSERT NOT x_5 OR NOT x_65; +ASSERT NOT x_5 OR NOT x_75; +ASSERT NOT x_5 OR NOT x_85; +ASSERT NOT x_5 OR NOT x_95; +ASSERT NOT x_5 OR NOT x_105; +ASSERT NOT x_15 OR NOT x_25; +ASSERT NOT x_15 OR NOT x_35; +ASSERT NOT x_15 OR NOT x_45; +ASSERT NOT x_15 OR NOT x_55; +ASSERT NOT x_15 OR NOT x_65; +ASSERT NOT x_15 OR NOT x_75; +ASSERT NOT x_15 OR NOT x_85; +ASSERT NOT x_15 OR NOT x_95; +ASSERT NOT x_15 OR NOT x_105; +ASSERT NOT x_25 OR NOT x_35; +ASSERT NOT x_25 OR NOT x_45; +ASSERT NOT x_25 OR NOT x_55; +ASSERT NOT x_25 OR NOT x_65; +ASSERT NOT x_25 OR NOT x_75; +ASSERT NOT x_25 OR NOT x_85; +ASSERT NOT x_25 OR NOT x_95; +ASSERT NOT x_25 OR NOT x_105; +ASSERT NOT x_35 OR NOT x_45; +ASSERT NOT x_35 OR NOT x_55; +ASSERT NOT x_35 OR NOT x_65; +ASSERT NOT x_35 OR NOT x_75; +ASSERT NOT x_35 OR NOT x_85; +ASSERT NOT x_35 OR NOT x_95; +ASSERT NOT x_35 OR NOT x_105; +ASSERT NOT x_45 OR NOT x_55; +ASSERT NOT x_45 OR NOT x_65; +ASSERT NOT x_45 OR NOT x_75; +ASSERT NOT x_45 OR NOT x_85; +ASSERT NOT x_45 OR NOT x_95; +ASSERT NOT x_45 OR NOT x_105; +ASSERT NOT x_55 OR NOT x_65; +ASSERT NOT x_55 OR NOT x_75; +ASSERT NOT x_55 OR NOT x_85; +ASSERT NOT x_55 OR NOT x_95; +ASSERT NOT x_55 OR NOT x_105; +ASSERT NOT x_65 OR NOT x_75; +ASSERT NOT x_65 OR NOT x_85; +ASSERT NOT x_65 OR NOT x_95; +ASSERT NOT x_65 OR NOT x_105; +ASSERT NOT x_75 OR NOT x_85; +ASSERT NOT x_75 OR NOT x_95; +ASSERT NOT x_75 OR NOT x_105; +ASSERT NOT x_85 OR NOT x_95; +ASSERT NOT x_85 OR NOT x_105; +ASSERT NOT x_95 OR NOT x_105; +ASSERT NOT x_6 OR NOT x_16; +ASSERT NOT x_6 OR NOT x_26; +ASSERT NOT x_6 OR NOT x_36; +ASSERT NOT x_6 OR NOT x_46; +ASSERT NOT x_6 OR NOT x_56; +ASSERT NOT x_6 OR NOT x_66; +ASSERT NOT x_6 OR NOT x_76; +ASSERT NOT x_6 OR NOT x_86; +ASSERT NOT x_6 OR NOT x_96; +ASSERT NOT x_6 OR NOT x_106; +ASSERT NOT x_16 OR NOT x_26; +ASSERT NOT x_16 OR NOT x_36; +ASSERT NOT x_16 OR NOT x_46; +ASSERT NOT x_16 OR NOT x_56; +ASSERT NOT x_16 OR NOT x_66; +ASSERT NOT x_16 OR NOT x_76; +ASSERT NOT x_16 OR NOT x_86; +ASSERT NOT x_16 OR NOT x_96; +ASSERT NOT x_16 OR NOT x_106; +ASSERT NOT x_26 OR NOT x_36; +ASSERT NOT x_26 OR NOT x_46; +ASSERT NOT x_26 OR NOT x_56; +ASSERT NOT x_26 OR NOT x_66; +ASSERT NOT x_26 OR NOT x_76; +ASSERT NOT x_26 OR NOT x_86; +ASSERT NOT x_26 OR NOT x_96; +ASSERT NOT x_26 OR NOT x_106; +ASSERT NOT x_36 OR NOT x_46; +ASSERT NOT x_36 OR NOT x_56; +ASSERT NOT x_36 OR NOT x_66; +ASSERT NOT x_36 OR NOT x_76; +ASSERT NOT x_36 OR NOT x_86; +ASSERT NOT x_36 OR NOT x_96; +ASSERT NOT x_36 OR NOT x_106; +ASSERT NOT x_46 OR NOT x_56; +ASSERT NOT x_46 OR NOT x_66; +ASSERT NOT x_46 OR NOT x_76; +ASSERT NOT x_46 OR NOT x_86; +ASSERT NOT x_46 OR NOT x_96; +ASSERT NOT x_46 OR NOT x_106; +ASSERT NOT x_56 OR NOT x_66; +ASSERT NOT x_56 OR NOT x_76; +ASSERT NOT x_56 OR NOT x_86; +ASSERT NOT x_56 OR NOT x_96; +ASSERT NOT x_56 OR NOT x_106; +ASSERT NOT x_66 OR NOT x_76; +ASSERT NOT x_66 OR NOT x_86; +ASSERT NOT x_66 OR NOT x_96; +ASSERT NOT x_66 OR NOT x_106; +ASSERT NOT x_76 OR NOT x_86; +ASSERT NOT x_76 OR NOT x_96; +ASSERT NOT x_76 OR NOT x_106; +ASSERT NOT x_86 OR NOT x_96; +ASSERT NOT x_86 OR NOT x_106; +ASSERT NOT x_96 OR NOT x_106; +ASSERT NOT x_7 OR NOT x_17; +ASSERT NOT x_7 OR NOT x_27; +ASSERT NOT x_7 OR NOT x_37; +ASSERT NOT x_7 OR NOT x_47; +ASSERT NOT x_7 OR NOT x_57; +ASSERT NOT x_7 OR NOT x_67; +ASSERT NOT x_7 OR NOT x_77; +ASSERT NOT x_7 OR NOT x_87; +ASSERT NOT x_7 OR NOT x_97; +ASSERT NOT x_7 OR NOT x_107; +ASSERT NOT x_17 OR NOT x_27; +ASSERT NOT x_17 OR NOT x_37; +ASSERT NOT x_17 OR NOT x_47; +ASSERT NOT x_17 OR NOT x_57; +ASSERT NOT x_17 OR NOT x_67; +ASSERT NOT x_17 OR NOT x_77; +ASSERT NOT x_17 OR NOT x_87; +ASSERT NOT x_17 OR NOT x_97; +ASSERT NOT x_17 OR NOT x_107; +ASSERT NOT x_27 OR NOT x_37; +ASSERT NOT x_27 OR NOT x_47; +ASSERT NOT x_27 OR NOT x_57; +ASSERT NOT x_27 OR NOT x_67; +ASSERT NOT x_27 OR NOT x_77; +ASSERT NOT x_27 OR NOT x_87; +ASSERT NOT x_27 OR NOT x_97; +ASSERT NOT x_27 OR NOT x_107; +ASSERT NOT x_37 OR NOT x_47; +ASSERT NOT x_37 OR NOT x_57; +ASSERT NOT x_37 OR NOT x_67; +ASSERT NOT x_37 OR NOT x_77; +ASSERT NOT x_37 OR NOT x_87; +ASSERT NOT x_37 OR NOT x_97; +ASSERT NOT x_37 OR NOT x_107; +ASSERT NOT x_47 OR NOT x_57; +ASSERT NOT x_47 OR NOT x_67; +ASSERT NOT x_47 OR NOT x_77; +ASSERT NOT x_47 OR NOT x_87; +ASSERT NOT x_47 OR NOT x_97; +ASSERT NOT x_47 OR NOT x_107; +ASSERT NOT x_57 OR NOT x_67; +ASSERT NOT x_57 OR NOT x_77; +ASSERT NOT x_57 OR NOT x_87; +ASSERT NOT x_57 OR NOT x_97; +ASSERT NOT x_57 OR NOT x_107; +ASSERT NOT x_67 OR NOT x_77; +ASSERT NOT x_67 OR NOT x_87; +ASSERT NOT x_67 OR NOT x_97; +ASSERT NOT x_67 OR NOT x_107; +ASSERT NOT x_77 OR NOT x_87; +ASSERT NOT x_77 OR NOT x_97; +ASSERT NOT x_77 OR NOT x_107; +ASSERT NOT x_87 OR NOT x_97; +ASSERT NOT x_87 OR NOT x_107; +ASSERT NOT x_97 OR NOT x_107; +ASSERT NOT x_8 OR NOT x_18; +ASSERT NOT x_8 OR NOT x_28; +ASSERT NOT x_8 OR NOT x_38; +ASSERT NOT x_8 OR NOT x_48; +ASSERT NOT x_8 OR NOT x_58; +ASSERT NOT x_8 OR NOT x_68; +ASSERT NOT x_8 OR NOT x_78; +ASSERT NOT x_8 OR NOT x_88; +ASSERT NOT x_8 OR NOT x_98; +ASSERT NOT x_8 OR NOT x_108; +ASSERT NOT x_18 OR NOT x_28; +ASSERT NOT x_18 OR NOT x_38; +ASSERT NOT x_18 OR NOT x_48; +ASSERT NOT x_18 OR NOT x_58; +ASSERT NOT x_18 OR NOT x_68; +ASSERT NOT x_18 OR NOT x_78; +ASSERT NOT x_18 OR NOT x_88; +ASSERT NOT x_18 OR NOT x_98; +ASSERT NOT x_18 OR NOT x_108; +ASSERT NOT x_28 OR NOT x_38; +ASSERT NOT x_28 OR NOT x_48; +ASSERT NOT x_28 OR NOT x_58; +ASSERT NOT x_28 OR NOT x_68; +ASSERT NOT x_28 OR NOT x_78; +ASSERT NOT x_28 OR NOT x_88; +ASSERT NOT x_28 OR NOT x_98; +ASSERT NOT x_28 OR NOT x_108; +ASSERT NOT x_38 OR NOT x_48; +ASSERT NOT x_38 OR NOT x_58; +ASSERT NOT x_38 OR NOT x_68; +ASSERT NOT x_38 OR NOT x_78; +ASSERT NOT x_38 OR NOT x_88; +ASSERT NOT x_38 OR NOT x_98; +ASSERT NOT x_38 OR NOT x_108; +ASSERT NOT x_48 OR NOT x_58; +ASSERT NOT x_48 OR NOT x_68; +ASSERT NOT x_48 OR NOT x_78; +ASSERT NOT x_48 OR NOT x_88; +ASSERT NOT x_48 OR NOT x_98; +ASSERT NOT x_48 OR NOT x_108; +ASSERT NOT x_58 OR NOT x_68; +ASSERT NOT x_58 OR NOT x_78; +ASSERT NOT x_58 OR NOT x_88; +ASSERT NOT x_58 OR NOT x_98; +ASSERT NOT x_58 OR NOT x_108; +ASSERT NOT x_68 OR NOT x_78; +ASSERT NOT x_68 OR NOT x_88; +ASSERT NOT x_68 OR NOT x_98; +ASSERT NOT x_68 OR NOT x_108; +ASSERT NOT x_78 OR NOT x_88; +ASSERT NOT x_78 OR NOT x_98; +ASSERT NOT x_78 OR NOT x_108; +ASSERT NOT x_88 OR NOT x_98; +ASSERT NOT x_88 OR NOT x_108; +ASSERT NOT x_98 OR NOT x_108; +ASSERT NOT x_9 OR NOT x_19; +ASSERT NOT x_9 OR NOT x_29; +ASSERT NOT x_9 OR NOT x_39; +ASSERT NOT x_9 OR NOT x_49; +ASSERT NOT x_9 OR NOT x_59; +ASSERT NOT x_9 OR NOT x_69; +ASSERT NOT x_9 OR NOT x_79; +ASSERT NOT x_9 OR NOT x_89; +ASSERT NOT x_9 OR NOT x_99; +ASSERT NOT x_9 OR NOT x_109; +ASSERT NOT x_19 OR NOT x_29; +ASSERT NOT x_19 OR NOT x_39; +ASSERT NOT x_19 OR NOT x_49; +ASSERT NOT x_19 OR NOT x_59; +ASSERT NOT x_19 OR NOT x_69; +ASSERT NOT x_19 OR NOT x_79; +ASSERT NOT x_19 OR NOT x_89; +ASSERT NOT x_19 OR NOT x_99; +ASSERT NOT x_19 OR NOT x_109; +ASSERT NOT x_29 OR NOT x_39; +ASSERT NOT x_29 OR NOT x_49; +ASSERT NOT x_29 OR NOT x_59; +ASSERT NOT x_29 OR NOT x_69; +ASSERT NOT x_29 OR NOT x_79; +ASSERT NOT x_29 OR NOT x_89; +ASSERT NOT x_29 OR NOT x_99; +ASSERT NOT x_29 OR NOT x_109; +ASSERT NOT x_39 OR NOT x_49; +ASSERT NOT x_39 OR NOT x_59; +ASSERT NOT x_39 OR NOT x_69; +ASSERT NOT x_39 OR NOT x_79; +ASSERT NOT x_39 OR NOT x_89; +ASSERT NOT x_39 OR NOT x_99; +ASSERT NOT x_39 OR NOT x_109; +ASSERT NOT x_49 OR NOT x_59; +ASSERT NOT x_49 OR NOT x_69; +ASSERT NOT x_49 OR NOT x_79; +ASSERT NOT x_49 OR NOT x_89; +ASSERT NOT x_49 OR NOT x_99; +ASSERT NOT x_49 OR NOT x_109; +ASSERT NOT x_59 OR NOT x_69; +ASSERT NOT x_59 OR NOT x_79; +ASSERT NOT x_59 OR NOT x_89; +ASSERT NOT x_59 OR NOT x_99; +ASSERT NOT x_59 OR NOT x_109; +ASSERT NOT x_69 OR NOT x_79; +ASSERT NOT x_69 OR NOT x_89; +ASSERT NOT x_69 OR NOT x_99; +ASSERT NOT x_69 OR NOT x_109; +ASSERT NOT x_79 OR NOT x_89; +ASSERT NOT x_79 OR NOT x_99; +ASSERT NOT x_79 OR NOT x_109; +ASSERT NOT x_89 OR NOT x_99; +ASSERT NOT x_89 OR NOT x_109; +ASSERT NOT x_99 OR NOT x_109; +ASSERT NOT x_10 OR NOT x_20; +ASSERT NOT x_10 OR NOT x_30; +ASSERT NOT x_10 OR NOT x_40; +ASSERT NOT x_10 OR NOT x_50; +ASSERT NOT x_10 OR NOT x_60; +ASSERT NOT x_10 OR NOT x_70; +ASSERT NOT x_10 OR NOT x_80; +ASSERT NOT x_10 OR NOT x_90; +ASSERT NOT x_10 OR NOT x_100; +ASSERT NOT x_10 OR NOT x_110; +ASSERT NOT x_20 OR NOT x_30; +ASSERT NOT x_20 OR NOT x_40; +ASSERT NOT x_20 OR NOT x_50; +ASSERT NOT x_20 OR NOT x_60; +ASSERT NOT x_20 OR NOT x_70; +ASSERT NOT x_20 OR NOT x_80; +ASSERT NOT x_20 OR NOT x_90; +ASSERT NOT x_20 OR NOT x_100; +ASSERT NOT x_20 OR NOT x_110; +ASSERT NOT x_30 OR NOT x_40; +ASSERT NOT x_30 OR NOT x_50; +ASSERT NOT x_30 OR NOT x_60; +ASSERT NOT x_30 OR NOT x_70; +ASSERT NOT x_30 OR NOT x_80; +ASSERT NOT x_30 OR NOT x_90; +ASSERT NOT x_30 OR NOT x_100; +ASSERT NOT x_30 OR NOT x_110; +ASSERT NOT x_40 OR NOT x_50; +ASSERT NOT x_40 OR NOT x_60; +ASSERT NOT x_40 OR NOT x_70; +ASSERT NOT x_40 OR NOT x_80; +ASSERT NOT x_40 OR NOT x_90; +ASSERT NOT x_40 OR NOT x_100; +ASSERT NOT x_40 OR NOT x_110; +ASSERT NOT x_50 OR NOT x_60; +ASSERT NOT x_50 OR NOT x_70; +ASSERT NOT x_50 OR NOT x_80; +ASSERT NOT x_50 OR NOT x_90; +ASSERT NOT x_50 OR NOT x_100; +ASSERT NOT x_50 OR NOT x_110; +ASSERT NOT x_60 OR NOT x_70; +ASSERT NOT x_60 OR NOT x_80; +ASSERT NOT x_60 OR NOT x_90; +ASSERT NOT x_60 OR NOT x_100; +ASSERT NOT x_60 OR NOT x_110; +ASSERT NOT x_70 OR NOT x_80; +ASSERT NOT x_70 OR NOT x_90; +ASSERT NOT x_70 OR NOT x_100; +ASSERT NOT x_70 OR NOT x_110; +ASSERT NOT x_80 OR NOT x_90; +ASSERT NOT x_80 OR NOT x_100; +ASSERT NOT x_80 OR NOT x_110; +ASSERT NOT x_90 OR NOT x_100; +ASSERT NOT x_90 OR NOT x_110; +ASSERT NOT x_100 OR NOT x_110; +ASSERT x_10 OR x_9 OR x_8 OR x_7 OR x_6 OR x_5 OR x_4 OR x_3 OR x_2 OR x_1; +ASSERT x_20 OR x_19 OR x_18 OR x_17 OR x_16 OR x_15 OR x_14 OR x_13 OR x_12 OR x_11; +ASSERT x_30 OR x_29 OR x_28 OR x_27 OR x_26 OR x_25 OR x_24 OR x_23 OR x_22 OR x_21; +ASSERT x_40 OR x_39 OR x_38 OR x_37 OR x_36 OR x_35 OR x_34 OR x_33 OR x_32 OR x_31; +ASSERT x_50 OR x_49 OR x_48 OR x_47 OR x_46 OR x_45 OR x_44 OR x_43 OR x_42 OR x_41; +ASSERT x_60 OR x_59 OR x_58 OR x_57 OR x_56 OR x_55 OR x_54 OR x_53 OR x_52 OR x_51; +ASSERT x_70 OR x_69 OR x_68 OR x_67 OR x_66 OR x_65 OR x_64 OR x_63 OR x_62 OR x_61; +ASSERT x_80 OR x_79 OR x_78 OR x_77 OR x_76 OR x_75 OR x_74 OR x_73 OR x_72 OR x_71; +ASSERT x_90 OR x_89 OR x_88 OR x_87 OR x_86 OR x_85 OR x_84 OR x_83 OR x_82 OR x_81; +ASSERT x_100 OR x_99 OR x_98 OR x_97 OR x_96 OR x_95 OR x_94 OR x_93 OR x_92 OR x_91; +ASSERT x_110 OR x_109 OR x_108 OR x_107 OR x_106 OR x_105 OR x_104 OR x_103 OR x_102 OR x_101; + + +QUERY FALSE;