Benchmark is taking 40 seconds on production, due to the configuration that tests --check-unsat-cores.
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
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
+++ /dev/null
-% 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;
--- /dev/null
+% 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;
projects / cvc5.git / commitdiff