diff options
Diffstat (limited to 'test/regress/regress1/hole6.cvc')
| -rw-r--r-- | test/regress/regress1/hole6.cvc | 180 |
1 files changed, 0 insertions, 180 deletions
diff --git a/test/regress/regress1/hole6.cvc b/test/regress/regress1/hole6.cvc deleted file mode 100644 index c191de6ba..000000000 --- a/test/regress/regress1/hole6.cvc +++ /dev/null @@ -1,180 +0,0 @@ -% COMMAND-LINE: --no-check-proofs -% 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; -ASSERT NOT x_1 OR NOT x_7; -ASSERT NOT x_1 OR NOT x_13; -ASSERT NOT x_1 OR NOT x_19; -ASSERT NOT x_1 OR NOT x_25; -ASSERT NOT x_1 OR NOT x_31; -ASSERT NOT x_1 OR NOT x_37; -ASSERT NOT x_7 OR NOT x_13; -ASSERT NOT x_7 OR NOT x_19; -ASSERT NOT x_7 OR NOT x_25; -ASSERT NOT x_7 OR NOT x_31; -ASSERT NOT x_7 OR NOT x_37; -ASSERT NOT x_13 OR NOT x_19; -ASSERT NOT x_13 OR NOT x_25; -ASSERT NOT x_13 OR NOT x_31; -ASSERT NOT x_13 OR NOT x_37; -ASSERT NOT x_19 OR NOT x_25; -ASSERT NOT x_19 OR NOT x_31; -ASSERT NOT x_19 OR NOT x_37; -ASSERT NOT x_25 OR NOT x_31; -ASSERT NOT x_25 OR NOT x_37; -ASSERT NOT x_31 OR NOT x_37; -ASSERT NOT x_2 OR NOT x_8; -ASSERT NOT x_2 OR NOT x_14; -ASSERT NOT x_2 OR NOT x_20; -ASSERT NOT x_2 OR NOT x_26; -ASSERT NOT x_2 OR NOT x_32; -ASSERT NOT x_2 OR NOT x_38; -ASSERT NOT x_8 OR NOT x_14; -ASSERT NOT x_8 OR NOT x_20; -ASSERT NOT x_8 OR NOT x_26; -ASSERT NOT x_8 OR NOT x_32; -ASSERT NOT x_8 OR NOT x_38; -ASSERT NOT x_14 OR NOT x_20; -ASSERT NOT x_14 OR NOT x_26; -ASSERT NOT x_14 OR NOT x_32; -ASSERT NOT x_14 OR NOT x_38; -ASSERT NOT x_20 OR NOT x_26; -ASSERT NOT x_20 OR NOT x_32; -ASSERT NOT x_20 OR NOT x_38; -ASSERT NOT x_26 OR NOT x_32; -ASSERT NOT x_26 OR NOT x_38; -ASSERT NOT x_32 OR NOT x_38; -ASSERT NOT x_3 OR NOT x_9; -ASSERT NOT x_3 OR NOT x_15; -ASSERT NOT x_3 OR NOT x_21; -ASSERT NOT x_3 OR NOT x_27; -ASSERT NOT x_3 OR NOT x_33; -ASSERT NOT x_3 OR NOT x_39; -ASSERT NOT x_9 OR NOT x_15; -ASSERT NOT x_9 OR NOT x_21; -ASSERT NOT x_9 OR NOT x_27; -ASSERT NOT x_9 OR NOT x_33; -ASSERT NOT x_9 OR NOT x_39; -ASSERT NOT x_15 OR NOT x_21; -ASSERT NOT x_15 OR NOT x_27; -ASSERT NOT x_15 OR NOT x_33; -ASSERT NOT x_15 OR NOT x_39; -ASSERT NOT x_21 OR NOT x_27; -ASSERT NOT x_21 OR NOT x_33; -ASSERT NOT x_21 OR NOT x_39; -ASSERT NOT x_27 OR NOT x_33; -ASSERT NOT x_27 OR NOT x_39; -ASSERT NOT x_33 OR NOT x_39; -ASSERT NOT x_4 OR NOT x_10; -ASSERT NOT x_4 OR NOT x_16; -ASSERT NOT x_4 OR NOT x_22; -ASSERT NOT x_4 OR NOT x_28; -ASSERT NOT x_4 OR NOT x_34; -ASSERT NOT x_4 OR NOT x_40; -ASSERT NOT x_10 OR NOT x_16; -ASSERT NOT x_10 OR NOT x_22; -ASSERT NOT x_10 OR NOT x_28; -ASSERT NOT x_10 OR NOT x_34; -ASSERT NOT x_10 OR NOT x_40; -ASSERT NOT x_16 OR NOT x_22; -ASSERT NOT x_16 OR NOT x_28; -ASSERT NOT x_16 OR NOT x_34; -ASSERT NOT x_16 OR NOT x_40; -ASSERT NOT x_22 OR NOT x_28; -ASSERT NOT x_22 OR NOT x_34; -ASSERT NOT x_22 OR NOT x_40; -ASSERT NOT x_28 OR NOT x_34; -ASSERT NOT x_28 OR NOT x_40; -ASSERT NOT x_34 OR NOT x_40; -ASSERT NOT x_5 OR NOT x_11; -ASSERT NOT x_5 OR NOT x_17; -ASSERT NOT x_5 OR NOT x_23; -ASSERT NOT x_5 OR NOT x_29; -ASSERT NOT x_5 OR NOT x_35; -ASSERT NOT x_5 OR NOT x_41; -ASSERT NOT x_11 OR NOT x_17; -ASSERT NOT x_11 OR NOT x_23; -ASSERT NOT x_11 OR NOT x_29; -ASSERT NOT x_11 OR NOT x_35; -ASSERT NOT x_11 OR NOT x_41; -ASSERT NOT x_17 OR NOT x_23; -ASSERT NOT x_17 OR NOT x_29; -ASSERT NOT x_17 OR NOT x_35; -ASSERT NOT x_17 OR NOT x_41; -ASSERT NOT x_23 OR NOT x_29; -ASSERT NOT x_23 OR NOT x_35; -ASSERT NOT x_23 OR NOT x_41; -ASSERT NOT x_29 OR NOT x_35; -ASSERT NOT x_29 OR NOT x_41; -ASSERT NOT x_35 OR NOT x_41; -ASSERT NOT x_6 OR NOT x_12; -ASSERT NOT x_6 OR NOT x_18; -ASSERT NOT x_6 OR NOT x_24; -ASSERT NOT x_6 OR NOT x_30; -ASSERT NOT x_6 OR NOT x_36; -ASSERT NOT x_6 OR NOT x_42; -ASSERT NOT x_12 OR NOT x_18; -ASSERT NOT x_12 OR NOT x_24; -ASSERT NOT x_12 OR NOT x_30; -ASSERT NOT x_12 OR NOT x_36; -ASSERT NOT x_12 OR NOT x_42; -ASSERT NOT x_18 OR NOT x_24; -ASSERT NOT x_18 OR NOT x_30; -ASSERT NOT x_18 OR NOT x_36; -ASSERT NOT x_18 OR NOT x_42; -ASSERT NOT x_24 OR NOT x_30; -ASSERT NOT x_24 OR NOT x_36; -ASSERT NOT x_24 OR NOT x_42; -ASSERT NOT x_30 OR NOT x_36; -ASSERT NOT x_30 OR NOT x_42; -ASSERT NOT x_36 OR NOT x_42; -ASSERT x_6 OR x_5 OR x_4 OR x_3 OR x_2 OR x_1; -ASSERT x_12 OR x_11 OR x_10 OR x_9 OR x_8 OR x_7; -ASSERT x_18 OR x_17 OR x_16 OR x_15 OR x_14 OR x_13; -ASSERT x_24 OR x_23 OR x_22 OR x_21 OR x_20 OR x_19; -ASSERT x_30 OR x_29 OR x_28 OR x_27 OR x_26 OR x_25; -ASSERT x_36 OR x_35 OR x_34 OR x_33 OR x_32 OR x_31; -ASSERT x_42 OR x_41 OR x_40 OR x_39 OR x_38 OR x_37; - - -QUERY FALSE; |