% EXPECT: valid
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;
ASSERT NOT x_1 OR NOT x_10;
ASSERT NOT x_1 OR NOT x_19;
ASSERT NOT x_1 OR NOT x_28;
ASSERT NOT x_1 OR NOT x_37;
ASSERT NOT x_1 OR NOT x_46;
ASSERT NOT x_1 OR NOT x_55;
ASSERT NOT x_1 OR NOT x_64;
ASSERT NOT x_1 OR NOT x_73;
ASSERT NOT x_1 OR NOT x_82;
ASSERT NOT x_10 OR NOT x_19;
ASSERT NOT x_10 OR NOT x_28;
ASSERT NOT x_10 OR NOT x_37;
ASSERT NOT x_10 OR NOT x_46;
ASSERT NOT x_10 OR NOT x_55;
ASSERT NOT x_10 OR NOT x_64;
ASSERT NOT x_10 OR NOT x_73;
ASSERT NOT x_10 OR NOT x_82;
ASSERT NOT x_19 OR NOT x_28;
ASSERT NOT x_19 OR NOT x_37;
ASSERT NOT x_19 OR NOT x_46;
ASSERT NOT x_19 OR NOT x_55;
ASSERT NOT x_19 OR NOT x_64;
ASSERT NOT x_19 OR NOT x_73;
ASSERT NOT x_19 OR NOT x_82;
ASSERT NOT x_28 OR NOT x_37;
ASSERT NOT x_28 OR NOT x_46;
ASSERT NOT x_28 OR NOT x_55;
ASSERT NOT x_28 OR NOT x_64;
ASSERT NOT x_28 OR NOT x_73;
ASSERT NOT x_28 OR NOT x_82;
ASSERT NOT x_37 OR NOT x_46;
ASSERT NOT x_37 OR NOT x_55;
ASSERT NOT x_37 OR NOT x_64;
ASSERT NOT x_37 OR NOT x_73;
ASSERT NOT x_37 OR NOT x_82;
ASSERT NOT x_46 OR NOT x_55;
ASSERT NOT x_46 OR NOT x_64;
ASSERT NOT x_46 OR NOT x_73;
ASSERT NOT x_46 OR NOT x_82;
ASSERT NOT x_55 OR NOT x_64;
ASSERT NOT x_55 OR NOT x_73;
ASSERT NOT x_55 OR NOT x_82;
ASSERT NOT x_64 OR NOT x_73;
ASSERT NOT x_64 OR NOT x_82;
ASSERT NOT x_73 OR NOT x_82;
ASSERT NOT x_2 OR NOT x_11;
ASSERT NOT x_2 OR NOT x_20;
ASSERT NOT x_2 OR NOT x_29;
ASSERT NOT x_2 OR NOT x_38;
ASSERT NOT x_2 OR NOT x_47;
ASSERT NOT x_2 OR NOT x_56;
ASSERT NOT x_2 OR NOT x_65;
ASSERT NOT x_2 OR NOT x_74;
ASSERT NOT x_2 OR NOT x_83;
ASSERT NOT x_11 OR NOT x_20;
ASSERT NOT x_11 OR NOT x_29;
ASSERT NOT x_11 OR NOT x_38;
ASSERT NOT x_11 OR NOT x_47;
ASSERT NOT x_11 OR NOT x_56;
ASSERT NOT x_11 OR NOT x_65;
ASSERT NOT x_11 OR NOT x_74;
ASSERT NOT x_11 OR NOT x_83;
ASSERT NOT x_20 OR NOT x_29;
ASSERT NOT x_20 OR NOT x_38;
ASSERT NOT x_20 OR NOT x_47;
ASSERT NOT x_20 OR NOT x_56;
ASSERT NOT x_20 OR NOT x_65;
ASSERT NOT x_20 OR NOT x_74;
ASSERT NOT x_20 OR NOT x_83;
ASSERT NOT x_29 OR NOT x_38;
ASSERT NOT x_29 OR NOT x_47;
ASSERT NOT x_29 OR NOT x_56;
ASSERT NOT x_29 OR NOT x_65;
ASSERT NOT x_29 OR NOT x_74;
ASSERT NOT x_29 OR NOT x_83;
ASSERT NOT x_38 OR NOT x_47;
ASSERT NOT x_38 OR NOT x_56;
ASSERT NOT x_38 OR NOT x_65;
ASSERT NOT x_38 OR NOT x_74;
ASSERT NOT x_38 OR NOT x_83;
ASSERT NOT x_47 OR NOT x_56;
ASSERT NOT x_47 OR NOT x_65;
ASSERT NOT x_47 OR NOT x_74;
ASSERT NOT x_47 OR NOT x_83;
ASSERT NOT x_56 OR NOT x_65;
ASSERT NOT x_56 OR NOT x_74;
ASSERT NOT x_56 OR NOT x_83;
ASSERT NOT x_65 OR NOT x_74;
ASSERT NOT x_65 OR NOT x_83;
ASSERT NOT x_74 OR NOT x_83;
ASSERT NOT x_3 OR NOT x_12;
ASSERT NOT x_3 OR NOT x_21;
ASSERT NOT x_3 OR NOT x_30;
ASSERT NOT x_3 OR NOT x_39;
ASSERT NOT x_3 OR NOT x_48;
ASSERT NOT x_3 OR NOT x_57;
ASSERT NOT x_3 OR NOT x_66;
ASSERT NOT x_3 OR NOT x_75;
ASSERT NOT x_3 OR NOT x_84;
ASSERT NOT x_12 OR NOT x_21;
ASSERT NOT x_12 OR NOT x_30;
ASSERT NOT x_12 OR NOT x_39;
ASSERT NOT x_12 OR NOT x_48;
ASSERT NOT x_12 OR NOT x_57;
ASSERT NOT x_12 OR NOT x_66;
ASSERT NOT x_12 OR NOT x_75;
ASSERT NOT x_12 OR NOT x_84;
ASSERT NOT x_21 OR NOT x_30;
ASSERT NOT x_21 OR NOT x_39;
ASSERT NOT x_21 OR NOT x_48;
ASSERT NOT x_21 OR NOT x_57;
ASSERT NOT x_21 OR NOT x_66;
ASSERT NOT x_21 OR NOT x_75;
ASSERT NOT x_21 OR NOT x_84;
ASSERT NOT x_30 OR NOT x_39;
ASSERT NOT x_30 OR NOT x_48;
ASSERT NOT x_30 OR NOT x_57;
ASSERT NOT x_30 OR NOT x_66;
ASSERT NOT x_30 OR NOT x_75;
ASSERT NOT x_30 OR NOT x_84;
ASSERT NOT x_39 OR NOT x_48;
ASSERT NOT x_39 OR NOT x_57;
ASSERT NOT x_39 OR NOT x_66;
ASSERT NOT x_39 OR NOT x_75;
ASSERT NOT x_39 OR NOT x_84;
ASSERT NOT x_48 OR NOT x_57;
ASSERT NOT x_48 OR NOT x_66;
ASSERT NOT x_48 OR NOT x_75;
ASSERT NOT x_48 OR NOT x_84;
ASSERT NOT x_57 OR NOT x_66;
ASSERT NOT x_57 OR NOT x_75;
ASSERT NOT x_57 OR NOT x_84;
ASSERT NOT x_66 OR NOT x_75;
ASSERT NOT x_66 OR NOT x_84;
ASSERT NOT x_75 OR NOT x_84;
ASSERT NOT x_4 OR NOT x_13;
ASSERT NOT x_4 OR NOT x_22;
ASSERT NOT x_4 OR NOT x_31;
ASSERT NOT x_4 OR NOT x_40;
ASSERT NOT x_4 OR NOT x_49;
ASSERT NOT x_4 OR NOT x_58;
ASSERT NOT x_4 OR NOT x_67;
ASSERT NOT x_4 OR NOT x_76;
ASSERT NOT x_4 OR NOT x_85;
ASSERT NOT x_13 OR NOT x_22;
ASSERT NOT x_13 OR NOT x_31;
ASSERT NOT x_13 OR NOT x_40;
ASSERT NOT x_13 OR NOT x_49;
ASSERT NOT x_13 OR NOT x_58;
ASSERT NOT x_13 OR NOT x_67;
ASSERT NOT x_13 OR NOT x_76;
ASSERT NOT x_13 OR NOT x_85;
ASSERT NOT x_22 OR NOT x_31;
ASSERT NOT x_22 OR NOT x_40;
ASSERT NOT x_22 OR NOT x_49;
ASSERT NOT x_22 OR NOT x_58;
ASSERT NOT x_22 OR NOT x_67;
ASSERT NOT x_22 OR NOT x_76;
ASSERT NOT x_22 OR NOT x_85;
ASSERT NOT x_31 OR NOT x_40;
ASSERT NOT x_31 OR NOT x_49;
ASSERT NOT x_31 OR NOT x_58;
ASSERT NOT x_31 OR NOT x_67;
ASSERT NOT x_31 OR NOT x_76;
ASSERT NOT x_31 OR NOT x_85;
ASSERT NOT x_40 OR NOT x_49;
ASSERT NOT x_40 OR NOT x_58;
ASSERT NOT x_40 OR NOT x_67;
ASSERT NOT x_40 OR NOT x_76;
ASSERT NOT x_40 OR NOT x_85;
ASSERT NOT x_49 OR NOT x_58;
ASSERT NOT x_49 OR NOT x_67;
ASSERT NOT x_49 OR NOT x_76;
ASSERT NOT x_49 OR NOT x_85;
ASSERT NOT x_58 OR NOT x_67;
ASSERT NOT x_58 OR NOT x_76;
ASSERT NOT x_58 OR NOT x_85;
ASSERT NOT x_67 OR NOT x_76;
ASSERT NOT x_67 OR NOT x_85;
ASSERT NOT x_76 OR NOT x_85;
ASSERT NOT x_5 OR NOT x_14;
ASSERT NOT x_5 OR NOT x_23;
ASSERT NOT x_5 OR NOT x_32;
ASSERT NOT x_5 OR NOT x_41;
ASSERT NOT x_5 OR NOT x_50;
ASSERT NOT x_5 OR NOT x_59;
ASSERT NOT x_5 OR NOT x_68;
ASSERT NOT x_5 OR NOT x_77;
ASSERT NOT x_5 OR NOT x_86;
ASSERT NOT x_14 OR NOT x_23;
ASSERT NOT x_14 OR NOT x_32;
ASSERT NOT x_14 OR NOT x_41;
ASSERT NOT x_14 OR NOT x_50;
ASSERT NOT x_14 OR NOT x_59;
ASSERT NOT x_14 OR NOT x_68;
ASSERT NOT x_14 OR NOT x_77;
ASSERT NOT x_14 OR NOT x_86;
ASSERT NOT x_23 OR NOT x_32;
ASSERT NOT x_23 OR NOT x_41;
ASSERT NOT x_23 OR NOT x_50;
ASSERT NOT x_23 OR NOT x_59;
ASSERT NOT x_23 OR NOT x_68;
ASSERT NOT x_23 OR NOT x_77;
ASSERT NOT x_23 OR NOT x_86;
ASSERT NOT x_32 OR NOT x_41;
ASSERT NOT x_32 OR NOT x_50;
ASSERT NOT x_32 OR NOT x_59;
ASSERT NOT x_32 OR NOT x_68;
ASSERT NOT x_32 OR NOT x_77;
ASSERT NOT x_32 OR NOT x_86;
ASSERT NOT x_41 OR NOT x_50;
ASSERT NOT x_41 OR NOT x_59;
ASSERT NOT x_41 OR NOT x_68;
ASSERT NOT x_41 OR NOT x_77;
ASSERT NOT x_41 OR NOT x_86;
ASSERT NOT x_50 OR NOT x_59;
ASSERT NOT x_50 OR NOT x_68;
ASSERT NOT x_50 OR NOT x_77;
ASSERT NOT x_50 OR NOT x_86;
ASSERT NOT x_59 OR NOT x_68;
ASSERT NOT x_59 OR NOT x_77;
ASSERT NOT x_59 OR NOT x_86;
ASSERT NOT x_68 OR NOT x_77;
ASSERT NOT x_68 OR NOT x_86;
ASSERT NOT x_77 OR NOT x_86;
ASSERT NOT x_6 OR NOT x_15;
ASSERT NOT x_6 OR NOT x_24;
ASSERT NOT x_6 OR NOT x_33;
ASSERT NOT x_6 OR NOT x_42;
ASSERT NOT x_6 OR NOT x_51;
ASSERT NOT x_6 OR NOT x_60;
ASSERT NOT x_6 OR NOT x_69;
ASSERT NOT x_6 OR NOT x_78;
ASSERT NOT x_6 OR NOT x_87;
ASSERT NOT x_15 OR NOT x_24;
ASSERT NOT x_15 OR NOT x_33;
ASSERT NOT x_15 OR NOT x_42;
ASSERT NOT x_15 OR NOT x_51;
ASSERT NOT x_15 OR NOT x_60;
ASSERT NOT x_15 OR NOT x_69;
ASSERT NOT x_15 OR NOT x_78;
ASSERT NOT x_15 OR NOT x_87;
ASSERT NOT x_24 OR NOT x_33;
ASSERT NOT x_24 OR NOT x_42;
ASSERT NOT x_24 OR NOT x_51;
ASSERT NOT x_24 OR NOT x_60;
ASSERT NOT x_24 OR NOT x_69;
ASSERT NOT x_24 OR NOT x_78;
ASSERT NOT x_24 OR NOT x_87;
ASSERT NOT x_33 OR NOT x_42;
ASSERT NOT x_33 OR NOT x_51;
ASSERT NOT x_33 OR NOT x_60;
ASSERT NOT x_33 OR NOT x_69;
ASSERT NOT x_33 OR NOT x_78;
ASSERT NOT x_33 OR NOT x_87;
ASSERT NOT x_42 OR NOT x_51;
ASSERT NOT x_42 OR NOT x_60;
ASSERT NOT x_42 OR NOT x_69;
ASSERT NOT x_42 OR NOT x_78;
ASSERT NOT x_42 OR NOT x_87;
ASSERT NOT x_51 OR NOT x_60;
ASSERT NOT x_51 OR NOT x_69;
ASSERT NOT x_51 OR NOT x_78;
ASSERT NOT x_51 OR NOT x_87;
ASSERT NOT x_60 OR NOT x_69;
ASSERT NOT x_60 OR NOT x_78;
ASSERT NOT x_60 OR NOT x_87;
ASSERT NOT x_69 OR NOT x_78;
ASSERT NOT x_69 OR NOT x_87;
ASSERT NOT x_78 OR NOT x_87;
ASSERT NOT x_7 OR NOT x_16;
ASSERT NOT x_7 OR NOT x_25;
ASSERT NOT x_7 OR NOT x_34;
ASSERT NOT x_7 OR NOT x_43;
ASSERT NOT x_7 OR NOT x_52;
ASSERT NOT x_7 OR NOT x_61;
ASSERT NOT x_7 OR NOT x_70;
ASSERT NOT x_7 OR NOT x_79;
ASSERT NOT x_7 OR NOT x_88;
ASSERT NOT x_16 OR NOT x_25;
ASSERT NOT x_16 OR NOT x_34;
ASSERT NOT x_16 OR NOT x_43;
ASSERT NOT x_16 OR NOT x_52;
ASSERT NOT x_16 OR NOT x_61;
ASSERT NOT x_16 OR NOT x_70;
ASSERT NOT x_16 OR NOT x_79;
ASSERT NOT x_16 OR NOT x_88;
ASSERT NOT x_25 OR NOT x_34;
ASSERT NOT x_25 OR NOT x_43;
ASSERT NOT x_25 OR NOT x_52;
ASSERT NOT x_25 OR NOT x_61;
ASSERT NOT x_25 OR NOT x_70;
ASSERT NOT x_25 OR NOT x_79;
ASSERT NOT x_25 OR NOT x_88;
ASSERT NOT x_34 OR NOT x_43;
ASSERT NOT x_34 OR NOT x_52;
ASSERT NOT x_34 OR NOT x_61;
ASSERT NOT x_34 OR NOT x_70;
ASSERT NOT x_34 OR NOT x_79;
ASSERT NOT x_34 OR NOT x_88;
ASSERT NOT x_43 OR NOT x_52;
ASSERT NOT x_43 OR NOT x_61;
ASSERT NOT x_43 OR NOT x_70;
ASSERT NOT x_43 OR NOT x_79;
ASSERT NOT x_43 OR NOT x_88;
ASSERT NOT x_52 OR NOT x_61;
ASSERT NOT x_52 OR NOT x_70;
ASSERT NOT x_52 OR NOT x_79;
ASSERT NOT x_52 OR NOT x_88;
ASSERT NOT x_61 OR NOT x_70;
ASSERT NOT x_61 OR NOT x_79;
ASSERT NOT x_61 OR NOT x_88;
ASSERT NOT x_70 OR NOT x_79;
ASSERT NOT x_70 OR NOT x_88;
ASSERT NOT x_79 OR NOT x_88;
ASSERT NOT x_8 OR NOT x_17;
ASSERT NOT x_8 OR NOT x_26;
ASSERT NOT x_8 OR NOT x_35;
ASSERT NOT x_8 OR NOT x_44;
ASSERT NOT x_8 OR NOT x_53;
ASSERT NOT x_8 OR NOT x_62;
ASSERT NOT x_8 OR NOT x_71;
ASSERT NOT x_8 OR NOT x_80;
ASSERT NOT x_8 OR NOT x_89;
ASSERT NOT x_17 OR NOT x_26;
ASSERT NOT x_17 OR NOT x_35;
ASSERT NOT x_17 OR NOT x_44;
ASSERT NOT x_17 OR NOT x_53;
ASSERT NOT x_17 OR NOT x_62;
ASSERT NOT x_17 OR NOT x_71;
ASSERT NOT x_17 OR NOT x_80;
ASSERT NOT x_17 OR NOT x_89;
ASSERT NOT x_26 OR NOT x_35;
ASSERT NOT x_26 OR NOT x_44;
ASSERT NOT x_26 OR NOT x_53;
ASSERT NOT x_26 OR NOT x_62;
ASSERT NOT x_26 OR NOT x_71;
ASSERT NOT x_26 OR NOT x_80;
ASSERT NOT x_26 OR NOT x_89;
ASSERT NOT x_35 OR NOT x_44;
ASSERT NOT x_35 OR NOT x_53;
ASSERT NOT x_35 OR NOT x_62;
ASSERT NOT x_35 OR NOT x_71;
ASSERT NOT x_35 OR NOT x_80;
ASSERT NOT x_35 OR NOT x_89;
ASSERT NOT x_44 OR NOT x_53;
ASSERT NOT x_44 OR NOT x_62;
ASSERT NOT x_44 OR NOT x_71;
ASSERT NOT x_44 OR NOT x_80;
ASSERT NOT x_44 OR NOT x_89;
ASSERT NOT x_53 OR NOT x_62;
ASSERT NOT x_53 OR NOT x_71;
ASSERT NOT x_53 OR NOT x_80;
ASSERT NOT x_53 OR NOT x_89;
ASSERT NOT x_62 OR NOT x_71;
ASSERT NOT x_62 OR NOT x_80;
ASSERT NOT x_62 OR NOT x_89;
ASSERT NOT x_71 OR NOT x_80;
ASSERT NOT x_71 OR NOT x_89;
ASSERT NOT x_80 OR NOT x_89;
ASSERT NOT x_9 OR NOT x_18;
ASSERT NOT x_9 OR NOT x_27;
ASSERT NOT x_9 OR NOT x_36;
ASSERT NOT x_9 OR NOT x_45;
ASSERT NOT x_9 OR NOT x_54;
ASSERT NOT x_9 OR NOT x_63;
ASSERT NOT x_9 OR NOT x_72;
ASSERT NOT x_9 OR NOT x_81;
ASSERT NOT x_9 OR NOT x_90;
ASSERT NOT x_18 OR NOT x_27;
ASSERT NOT x_18 OR NOT x_36;
ASSERT NOT x_18 OR NOT x_45;
ASSERT NOT x_18 OR NOT x_54;
ASSERT NOT x_18 OR NOT x_63;
ASSERT NOT x_18 OR NOT x_72;
ASSERT NOT x_18 OR NOT x_81;
ASSERT NOT x_18 OR NOT x_90;
ASSERT NOT x_27 OR NOT x_36;
ASSERT NOT x_27 OR NOT x_45;
ASSERT NOT x_27 OR NOT x_54;
ASSERT NOT x_27 OR NOT x_63;
ASSERT NOT x_27 OR NOT x_72;
ASSERT NOT x_27 OR NOT x_81;
ASSERT NOT x_27 OR NOT x_90;
ASSERT NOT x_36 OR NOT x_45;
ASSERT NOT x_36 OR NOT x_54;
ASSERT NOT x_36 OR NOT x_63;
ASSERT NOT x_36 OR NOT x_72;
ASSERT NOT x_36 OR NOT x_81;
ASSERT NOT x_36 OR NOT x_90;
ASSERT NOT x_45 OR NOT x_54;
ASSERT NOT x_45 OR NOT x_63;
ASSERT NOT x_45 OR NOT x_72;
ASSERT NOT x_45 OR NOT x_81;
ASSERT NOT x_45 OR NOT x_90;
ASSERT NOT x_54 OR NOT x_63;
ASSERT NOT x_54 OR NOT x_72;
ASSERT NOT x_54 OR NOT x_81;
ASSERT NOT x_54 OR NOT x_90;
ASSERT NOT x_63 OR NOT x_72;
ASSERT NOT x_63 OR NOT x_81;
ASSERT NOT x_63 OR NOT x_90;
ASSERT NOT x_72 OR NOT x_81;
ASSERT NOT x_72 OR NOT x_90;
ASSERT NOT x_81 OR NOT x_90;
ASSERT 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_18 OR x_17 OR x_16 OR x_15 OR x_14 OR x_13 OR x_12 OR x_11 OR x_10;
ASSERT x_27 OR x_26 OR x_25 OR x_24 OR x_23 OR x_22 OR x_21 OR x_20 OR x_19;
ASSERT x_36 OR x_35 OR x_34 OR x_33 OR x_32 OR x_31 OR x_30 OR x_29 OR x_28;
ASSERT x_45 OR x_44 OR x_43 OR x_42 OR x_41 OR x_40 OR x_39 OR x_38 OR x_37;
ASSERT x_54 OR x_53 OR x_52 OR x_51 OR x_50 OR x_49 OR x_48 OR x_47 OR x_46;
ASSERT x_63 OR x_62 OR x_61 OR x_60 OR x_59 OR x_58 OR x_57 OR x_56 OR x_55;
ASSERT x_72 OR x_71 OR x_70 OR x_69 OR x_68 OR x_67 OR x_66 OR x_65 OR x_64;
ASSERT x_81 OR x_80 OR x_79 OR x_78 OR x_77 OR x_76 OR x_75 OR x_74 OR x_73;
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;


QUERY FALSE;