The VLSAT-3 Benchmark Suite

Contents

1. What is the VLSAT-3 benchmark suite?

The VLSAT-3 benchmark suite (where "VL" stands for "Very Large") is a collection of 1200 SMT formulas to be used as benchmarks in scientific experiments and software competitions.

These SMT formulas have been obtained from the automatic conversion [BGP20] into Nested-Unit Petri Nets (NUPNs) [Gar19] of a large collection of Petri nets modelling real-life problems, such as communication protocols and concurrent systems.

For that, a complete tool chain has been developed [BGP20], which expresses the conversion either as a SAT problem, an SMT problem, a graph coloring problem, or a maximum clique problem. When a conversion method involving SMT solving is selected, the tool chain produces formulas to be processed by SMT solvers. The tool chain is solver-agnostic and supports six standard SMT logics:

The VLSAT-3 benchmarks have been carefully selected among a large collection of more than 51,000 SMT formulas produced by the tool chain. The selection took into account the criteria of the SMT-COMP 2020 and SMT-COMP 2021 solver competitions.

For each of the aforementioned logics, we considered six SMT solvers (namely, Boolector 3.2.0, Bitwuzla (the version submitted to the SMT-COMP 2020), CVC4 1.8, MathSAT 5.6.5, Yices 2.6.2, and Z3 4.8.9). These include all the solvers that participated in SMT-COMP 2019 and/or in SMT-COMP 2020 and have been the fastest or the second fastest for any logic fragment supported by our toolchain (i.e., Boolector, Bitwuzla, CVC4, Yices, and Z3), as well as the solvers used for constructing VLSAT-2 [BG21c] and that can solve both SAT and SMT formulas (i.e., MathSAT and Z3). We then selected only those formulas that can be solved between ten seconds and one hour (on a Xeon E5-2630 v3 with 128 GB RAM) using these solvers. We also tried to provide formulas of increasing complexities.

For each supported logic, we selected 100 satisfiable and 100 unsatisfiable formulas, which results in 12 families containing 100 benchmarks each. These families are listed in the table below, the columns of which have the following meaning:

family satisfiability logic selection SQT share MVT share UCT share
a UNSAT QF_BV 76% 0.86% 2.65%
b QF_DT 100% 49.02% 100%
c QF_IDL 100% 8.79% 100%
d QF_UFBV 88% 29.33% 30.67%
e QF_UFDT 100% 49.26% 100%
f QF_UFIDL 100% 33.33% 88.50%
g SAT QF_BV 76% 0.86% 1.05%
h QF_DT 100% 49.02%
i QF_IDL 70% 6.15% 10.13%
j QF_UFBV 81% 27.0% 21.6%
k QF_UFDT 100% 49.26%
l QF_UFIDL 100% 33.33% 48.54%

[B21]
Pierre Bouvier. The VLSAT-3 Benchmark Suite. INRIA Technical Report 516, December 2021.
[BG21c]
Pierre Bouvier and Hubert Garavel. The VLSAT-2 Benchmark Suite. INRIA Technical Report 514, September 2021.
[BGP20]
Pierre Bouvier, Hubert Garavel, and Hernán Ponce de León. Automatic Decomposition of Petri Nets into Automata Networks - A Synthetic Account. In Proceedings of the 41th International Conference on Application and Theory of Petri Nets and Concurrency (PETRI NETS'20), Paris, France, June 2020.
[Gar19]
Hubert Garavel. Nested-Unit Petri Nets. Journal of Logical and Algebraic Methods in Programming, vol. 104, pages 60-85, April 2019.

2. How to use the VLSAT-3 benchmark suite?

Each formula is provided as a separate file, encoded in the SMT-LIB 2.6 format, and then compressed using bzip2.

We do not provide a single archive file containing all the VLSAT-3 formulas, but one can download all them at once using either FTP: 

   wget "ftp://ftp.inrialpes.fr/pub/vasy/benchmarks/vlsat/vlsat3*"
or HTTPS: 
   wget -r --no-parent -A "vlsat3*" https://cadp.inria.fr/ftp/benchmarks/vlsat
With the latter command, the formulas will be put in directory "./cadp.inria.fr/ftp/benchmarks/vlsat".

It is also possible to download only VLSAT-3 formulas of a given family by specializing the above commands. For instance: 

   wget "ftp://ftp.inrialpes.fr/pub/vasy/benchmarks/vlsat/vlsat3_a*"
and 
   wget -r --no-parent -A "vlsat3_a*" https://cadp.inria.fr/ftp/benchmarks/vlsat
will download only those VLSAT-3 formulas belonging to family "a", i.e., 100 UNSAT QF_BV formulas.

3. Contents of the VLSAT-3 benchmark suite

The VLSAT-3 benchmarks can be downloaded from the 12 tables given in the 12 subsections below. Each row of a table corresponds to one benchmark. The columns of these tables contain the following data:

3.1. Family "a" of VLSAT-3 formulas

This family is composed of 100 unsatisfiable formulas written in the QF_BV logic.

name (.smt2.bz2) satisfiable #variables card #asserts #operators size (.smt2) size (.smt2.bz2)
vlsat3_a00 No 56 211 1463 7283 65,779 3886
vlsat3_a01 No 80 211 3050 15,170 134,477 6639
vlsat3_a02 No 80 217 3050 15,218 152,817 6693
vlsat3_a03 No 56 212 1463 7291 67,252 3893
vlsat3_a04 No 120 215 6975 34,747 334,500 13,872
vlsat3_a05 No 140 217 8750 43,598 438,326 18,095
vlsat3_a06 No 80 218 3050 15,226 155,871 6707
vlsat3_a07 No 122 211 6963 34,651 306,330 14,059
vlsat3_a08 No 244 210 16,134 80,254 706,507 34,469
vlsat3_a09 No 80 212 3050 15,178 137,537 6635
vlsat3_a10 No 112 211 6064 30,176 266,275 12,280
vlsat3_a11 No 164 211 13,172 65,612 581,961 25,673
vlsat3_a12 No 60 215 1407 7027 69,218 3860
vlsat3_a13 No 80 216 3050 15,210 149,840 6653
vlsat3_a14 No 138 211 9282 46,214 409,121 18,391
vlsat3_a15 No 48 223 1113 5645 64,013 3390
vlsat3_a16 No 56 216 1463 7323 73,183 3919
vlsat3_a17 No 84 212 1819 9015 83,846 4818
vlsat3_a18 No 87 214 3180 15,830 149,955 6900
vlsat3_a19 No 123 215 5120 25,466 246,597 11,014
vlsat3_a20 No 141 211 6054 30,068 268,468 12,646
vlsat3_a21 No 87 214 2672 13,290 126,558 6220
vlsat3_a22 No 101 219 3524 17,562 183,766 7833
vlsat3_a23 No 120 216 6975 34,755 341,481 13,872
vlsat3_a24 No 70 217 1633 8153 83,315 4401
vlsat3_a25 No 77 216 1907 9501 95,013 4902
vlsat3_a26 No 118 215 4995 24,851 240,064 10,451
vlsat3_a27 No 43 215 591 2981 30,566 2456
vlsat3_a28 No 99 211 4081 20,287 179,406 8520
vlsat3_a29 No 128 211 4185 20,749 186,231 9330
vlsat3_a30 No 56 213 1463 7299 68,724 3926
vlsat3_a31 No 85 214 2077 10,319 99,253 5149
vlsat3_a32 No 87 219 2672 13,330 139,860 6279
vlsat3_a33 No 139 211 5667 28,137 251,186 11,909
vlsat3_a34 No 161 211 6337 31,443 282,525 13,650
vlsat3_a35 No 155 214 9328 46,434 439,576 18,888
vlsat3_a36 No 61 215 1248 6230 61,777 3676
vlsat3_a37 No 78 213 2162 10,750 100,812 5219
vlsat3_a38 No 168 220 8560 42,616 456,229 18,174
vlsat3_a39 No 44 225 946 4834 56,618 3104
vlsat3_a40 No 130 215 6171 30,707 296,780 12,871
vlsat3_a41 No 224 213 15,832 78,808 736,534 33,648
vlsat3_a42 No 237 214 18,611 92,685 883,648 39,654
vlsat3_a43 No 28 211 224 1144 12,145 1723
vlsat3_a44 No 58 216 1555 7779 77,625 4060
vlsat3_a45 No 139 211 5449 27,047 241,780 11,592
vlsat3_a46 No 233 215 20,436 101,826 990,710 42,060
vlsat3_a47 No 45 214 679 3409 34,081 2603
vlsat3_a48 No 54 216 928 4652 47,541 3093
vlsat3_a49 No 62 230 1849 9353 117,656 4707
vlsat3_a50 No 140 219 8750 43,614 455,833 18,062
vlsat3_a51 No 114 211 2465 12,177 111,683 6208
vlsat3_a52 No 90 218 2808 13,996 144,167 6575
vlsat3_a53 No 118 218 6333 31,565 322,984 13,071
vlsat3_a54 No 176 211 12,053 59,993 535,158 24,554
vlsat3_a55 No 47 216 745 3751 38,612 2729
vlsat3_a56 No 57 213 1306 6512 61,798 3719
vlsat3_a57 No 106 211 4140 20,568 182,818 8844
vlsat3_a58 No 190 215 13,177 65,617 636,433 26,398
vlsat3_a59 No 80 213 3050 15,186 140,596 6631
vlsat3_a60 No 145 213 4258 21,096 198,336 9596
vlsat3_a61 No 418 211 76,832 383,404 3,430,704 178,369
vlsat3_a62 No 274 212 30,943 154,255 1,419,597 68,751
vlsat3_a63 No 321 211 46,286 230,868 2,065,369 101,933
vlsat3_a64 No 387 211 61,385 306,231 2,745,725 140,052
vlsat3_a65 No 409 211 76,216 380,342 3,407,296 176,832
vlsat3_a66 No 372 211 65,248 325,576 2,911,629 148,443
vlsat3_a67 No 739 211 263,743 1,317,317 11,816,292 678,199
vlsat3_a68 No 57 212 1306 6504 60,546 3676
vlsat3_a69 No 95 212 4076 20,278 183,107 8413
vlsat3_a70 No 143 248 9242 46,300 760,310 20,674
vlsat3_a71 No 187 213 15,773 78,587 733,578 32,030
vlsat3_a72 No 64 214 2003 9991 95,281 4818
vlsat3_a73 No 94 212 4007 19,935 180,051 8372
vlsat3_a74 No 214 213 16,183 80,583 752,133 33,333
vlsat3_a75 No 341 212 21,828 108,546 1,001,352 49,405
vlsat3_a76 No 124 211 3938 19,522 175,463 8833
vlsat3_a77 No 280 213 37,240 185,736 1,731,221 81,240
vlsat3_a78 No 80 211 1642 8130 74,618 4389
vlsat3_a79 No 115 212 5325 26,483 239,993 11,172
vlsat3_a80 No 279 211 33,589 167,467 1,494,431 72,137
vlsat3_a81 No 379 211 36,702 182,832 1,646,045 82,698
vlsat3_a82 No 438 211 89,288 445,644 3,990,445 208,851
vlsat3_a83 No 74 214 1048 5196 51,834 3416
vlsat3_a84 No 513 211 119,974 598,924 5,380,552 292,780
vlsat3_a85 No 73 214 1136 5638 55,821 3599
vlsat3_a86 No 549 211 70,640 352,182 3,170,085 170,618
vlsat3_a87 No 455 211 95,112 474,730 4,250,189 224,890
vlsat3_a88 No 519 211 63,046 314,272 2,829,071 151,072
vlsat3_a89 No 398 211 74,088 369,724 3,308,332 171,088
vlsat3_a90 No 589 211 83,903 418,417 3,765,589 204,963
vlsat3_a91 No 444 211 90,479 451,587 4,043,257 211,575
vlsat3_a92 No 374 211 44,026 219,462 1,968,035 98,429
vlsat3_a93 No 482 211 107,271 535,471 4,795,373 256,000
vlsat3_a94 No 588 211 144,272 720,264 6,476,835 353,766
vlsat3_a95 No 236 211 23,702 118,118 1,054,884 49,057
vlsat3_a96 No 342 211 50,614 252,466 2,259,286 113,617
vlsat3_a97 No 440 2121 91,418 457,170 14,231,979 226,250
vlsat3_a98 No 318 211 34,220 170,544 1,529,011 75,028
vlsat3_a99 No 202 211 16,451 81,931 731,250 33,673

3.2. Family "b" of VLSAT-3 formulas

This family is composed of 100 unsatisfiable formulas written in the QF_DT logic.

name (.smt2.bz2) satisfiable #variables card #asserts #operators size (.smt2) size (.smt2.bz2)
vlsat3_b00 No 56 16 1422 4504 43,600 3902
vlsat3_b01 No 164 11 13,018 39,162 379,855 25,645
vlsat3_b02 No 56 12 1418 4384 42,913 3828
vlsat3_b03 No 120 16 6870 20,848 199,411 13,864
vlsat3_b04 No 118 14 4890 14,850 142,533 10,268
vlsat3_b05 No 140 18 8627 26,185 252,011 17,902
vlsat3_b06 No 155 13 9185 27,709 267,703 18,576
vlsat3_b07 No 48 21 1085 3673 35,003 3498
vlsat3_b08 No 161 11 6186 18,666 183,040 13,290
vlsat3_b09 No 228 11 25,444 76,440 747,798 51,474
vlsat3_b10 No 56 17 1423 4539 43,802 3951
vlsat3_b11 No 122 11 3633 11,007 107,416 8209
vlsat3_b12 No 120 17 6871 20,883 199,855 13,860
vlsat3_b13 No 72 13 1947 5995 58,275 4826
vlsat3_b14 No 80 17 2986 9228 87,974 6629
vlsat3_b15 No 249 15 23,529 70,795 694,310 48,955
vlsat3_b16 No 168 20 8411 25,611 247,791 18,117
vlsat3_b17 No 155 14 9186 27,738 267,869 18,591
vlsat3_b18 No 192 11 9254 27,870 274,638 19,597
vlsat3_b19 No 70 15 1577 4939 48,133 4335
vlsat3_b20 No 71 11 1859 5685 55,831 4646
vlsat3_b21 No 80 13 2982 9100 87,239 6459
vlsat3_b22 No 137 11 4890 14,778 144,283 10,610
vlsat3_b23 No 112 12 5963 18,019 172,595 12,079
vlsat3_b24 No 231 11 17,648 53,052 520,806 36,726
vlsat3_b25 No 56 13 1419 4411 43,008 3859
vlsat3_b26 No 220 15 15,636 47,116 461,416 32,971
vlsat3_b27 No 366 11 33,082 99,354 986,365 73,574
vlsat3_b28 No 95 14 2688 8244 79,591 6273
vlsat3_b29 No 101 19 3441 10,663 101,624 7800
vlsat3_b30 No 164 12 13,019 39,187 379,997 25,437
vlsat3_b31 No 124 14 5446 16,518 158,762 11,421
vlsat3_b32 No 140 19 8628 26,224 252,237 17,850
vlsat3_b33 No 174 21 9097 27,709 268,230 19,504
vlsat3_b34 No 72 14 1948 6024 58,388 4806
vlsat3_b35 No 124 11 3797 11,499 112,388 8541
vlsat3_b36 No 118 15 4891 14,881 142,711 10,318
vlsat3_b37 No 250 11 16,203 48,717 481,280 34,655
vlsat3_b38 No 265 11 23,486 70,566 694,593 49,454
vlsat3_b39 No 318 11 33,912 101,844 1,006,257 73,446
vlsat3_b40 No 36 14 387 1341 14,044 2083
vlsat3_b41 No 128 11 4067 12,309 120,080 9077
vlsat3_b42 No 643 17 27,546 82,908 837,464 63,407
vlsat3_b43 No 244 11 15,900 47,808 473,545 33,977
vlsat3_b44 No 228 12 25,445 76,465 747,940 51,944
vlsat3_b45 No 262 12 33,713 101,269 993,227 71,660
vlsat3_b46 No 132 12 8072 24,346 234,635 15,912
vlsat3_b47 No 182 11 8875 26,733 262,080 18,732
vlsat3_b48 No 313 11 26,245 78,843 780,185 56,933
vlsat3_b49 No 48 22 1086 3718 35,265 3557
vlsat3_b50 No 74 13 1844 5686 55,455 4694
vlsat3_b51 No 141 11 5923 17,877 173,868 12,355
vlsat3_b52 No 187 11 8484 25,560 251,818 18,017
vlsat3_b53 No 163 14 9451 28,533 276,259 19,515
vlsat3_b54 No 263 11 18,641 56,031 552,974 39,992
vlsat3_b55 No 108 11 2849 8655 84,534 6298
vlsat3_b56 No 80 19 2988 9304 88,327 6712
vlsat3_b57 No 173 11 4966 15,006 149,466 11,502
vlsat3_b58 No 259 11 16,567 49,809 492,995 35,613
vlsat3_b59 No 290 12 33,862 101,716 1,004,064 72,318
vlsat3_b60 No 312 14 34,861 104,763 1,032,796 76,080
vlsat3_b61 No 100 11 2539 7725 75,432 5709
vlsat3_b62 No 182 12 15,492 46,606 453,403 30,556
vlsat3_b63 No 197 12 17,102 51,436 501,573 34,090
vlsat3_b64 No 121 12 4860 14,710 142,756 10,558
vlsat3_b65 No 146 12 9804 29,542 285,677 19,432
vlsat3_b66 No 218 12 22,476 67,558 660,007 44,994
vlsat3_b67 No 137 21 7951 24,271 235,571 17,237
vlsat3_b68 No 272 11 18,181 54,651 540,738 39,040
vlsat3_b69 No 266 12 33,804 101,542 995,960 71,796
vlsat3_b70 No 140 12 7273 21,949 212,470 14,945
vlsat3_b71 No 142 12 9392 28,306 273,425 18,470
vlsat3_b72 No 154 12 11,085 33,385 323,464 21,847
vlsat3_b73 No 196 12 18,722 56,296 548,833 37,526
vlsat3_b74 No 265 11 23,519 70,665 695,526 49,374
vlsat3_b75 No 271 12 33,783 101,479 996,013 71,601
vlsat3_b76 No 112 12 5732 17,326 166,055 11,631
vlsat3_b77 No 161 17 11,412 34,506 338,042 24,433
vlsat3_b78 No 287 12 34,877 104,761 1,031,266 75,365
vlsat3_b79 No 735 83 265,952 804,660 7,961,149 681,383
vlsat3_b80 No 735 84 265,953 804,829 7,962,155 681,811
vlsat3_b81 No 845 11 207,417 622,359 6,188,160 519,026
vlsat3_b82 No 236 11 23,476 70,536 692,523 48,049
vlsat3_b83 No 575 145 156,823 491,347 5,037,757 412,856
vlsat3_b84 No 735 85 265,954 805,000 7,963,173 681,764
vlsat3_b85 No 575 144 156,822 491,056 5,035,830 412,739
vlsat3_b86 No 575 146 156,824 491,640 5,039,698 413,366
vlsat3_b87 No 575 147 156,825 491,935 5,041,653 413,609
vlsat3_b88 No 575 148 156,826 492,232 5,043,622 414,349
vlsat3_b89 No 735 86 265,955 805,173 7,964,203 682,244
vlsat3_b90 No 609 11 149,949 449,955 4,467,182 364,889
vlsat3_b91 No 735 89 265,958 805,704 7,967,365 681,686
vlsat3_b92 No 242 12 23,786 71,488 701,946 49,415
vlsat3_b93 No 575 150 156,828 492,832 5,047,602 414,593
vlsat3_b94 No 48 31 1065 4123 37,299 3796
vlsat3_b95 No 1026 46 404,855 1,216,633 12,126,686 1,063,023
vlsat3_b96 No 575 149 156,827 492,531 5,045,605 414,677
vlsat3_b97 No 1016 81 509,749 1,535,725 15,269,228 1,362,984
vlsat3_b98 No 1019 81 512,764 1,544,770 15,359,496 1,373,709
vlsat3_b99 No 717 205 249,677 790,849 7,711,831 666,243

3.3. Family "c" of VLSAT-3 formulas

This family is composed of 100 unsatisfiable formulas written in the QF_IDL logic.

name (.smt2.bz2) satisfiable #variables card #asserts #operators size (.smt2) size (.smt2.bz2)
vlsat3_c00 No 56 ∞ 1463 5687 49,256 4522
vlsat3_c01 No 80 ∞ 3050 10,936 96,161 7539
vlsat3_c02 No 215 ∞ 19,420 61,226 583,124 40,070
vlsat3_c03 No 216 ∞ 23,436 117,176 963,878 77,165
vlsat3_c04 No 56 ∞ 1463 5773 49,729 4590
vlsat3_c05 No 80 ∞ 3050 11,072 96,992 7662
vlsat3_c06 No 80 ∞ 3050 11,206 97,646 7812
vlsat3_c07 No 194 ∞ 18,871 67,709 610,452 43,418
vlsat3_c08 No 84 ∞ 1819 7765 64,934 5893
vlsat3_c09 No 80 ∞ 3050 11,338 98,455 7967
vlsat3_c10 No 124 ∞ 5557 20,397 178,802 14,043
vlsat3_c11 No 194 ∞ 18,871 68,359 614,215 44,230
vlsat3_c12 No 56 ∞ 1463 5857 50,191 4726
vlsat3_c13 No 112 ∞ 6064 21,144 188,444 13,454
vlsat3_c14 No 132 ∞ 8193 28,091 253,904 17,862
vlsat3_c15 No 164 ∞ 13,172 43,924 404,738 27,908
vlsat3_c16 No 56 ∞ 1463 6019 51,141 4767
vlsat3_c17 No 136 ∞ 8792 32,796 287,238 21,076
vlsat3_c18 No 366 ∞ 33,438 108,254 1,033,308 80,646
vlsat3_c19 No 262 ∞ 33,964 108,546 1,031,824 76,790
vlsat3_c20 No 56 ∞ 1463 5939 50,642 4680
vlsat3_c21 No 87 ∞ 3180 12,082 104,093 8623
vlsat3_c22 No 141 ∞ 6054 21,412 191,907 14,862
vlsat3_c23 No 161 ∞ 6337 23,039 205,720 16,238
vlsat3_c24 No 71 ∞ 1920 7448 64,565 5625
vlsat3_c25 No 137 ∞ 8068 27,358 254,345 18,020
vlsat3_c26 No 166 ∞ 13,507 44,985 415,156 28,621
vlsat3_c27 No 325 ∞ 15,332 53,662 495,271 37,745
vlsat3_c28 No 84 ∞ 1819 7903 65,693 5954
vlsat3_c29 No 244 ∞ 16,134 54,124 506,845 38,059
vlsat3_c30 No 366 ∞ 33,438 108,964 1,037,480 81,118
vlsat3_c31 No 262 ∞ 33,964 109,044 1,034,726 77,197
vlsat3_c32 No 80 ∞ 3050 11,468 99,087 7943
vlsat3_c33 No 142 ∞ 9523 32,361 294,404 20,587
vlsat3_c34 No 265 ∞ 23,741 77,449 730,860 54,045
vlsat3_c35 No 228 ∞ 25,662 83,186 783,625 55,614
vlsat3_c36 No 137 ∞ 8068 27,608 255,794 18,110
vlsat3_c37 No 137 ∞ 8068 29,066 261,083 20,551
vlsat3_c38 No 285 ∞ 20,436 68,014 639,095 48,295
vlsat3_c39 No 228 ∞ 25,662 83,614 786,108 56,055
vlsat3_c40 No 226 ∞ 14,011 47,751 441,881 33,546
vlsat3_c41 No 215 ∞ 18,071 61,249 565,049 40,148
vlsat3_c42 No 285 ∞ 20,436 68,560 642,284 48,738
vlsat3_c43 No 289 ∞ 21,221 70,465 663,472 50,371
vlsat3_c44 No 139 ∞ 5667 20,709 183,063 14,273
vlsat3_c45 No 112 ∞ 6064 21,340 189,535 13,658
vlsat3_c46 No 231 ∞ 17,869 59,455 554,616 40,295
vlsat3_c47 No 289 ∞ 21,221 71,019 666,709 50,918
vlsat3_c48 No 60 ∞ 1407 5987 50,344 4828
vlsat3_c49 No 164 ∞ 13,172 44,224 406,453 28,214
vlsat3_c50 No 272 ∞ 18,443 62,243 581,067 44,377
vlsat3_c51 No 297 ∞ 22,683 75,613 710,185 54,313
vlsat3_c52 No 80 ∞ 3050 11,596 99,786 8148
vlsat3_c53 No 120 ∞ 6975 24,523 218,306 15,908
vlsat3_c54 No 136 ∞ 8792 33,016 288,484 21,318
vlsat3_c55 No 247 ∞ 15,746 53,502 497,028 38,196
vlsat3_c56 No 55 ∞ 1026 4750 39,223 4093
vlsat3_c57 No 118 ∞ 4995 18,723 162,544 12,608
vlsat3_c58 No 137 ∞ 8068 27,856 257,232 18,357
vlsat3_c59 No 198 ∞ 11,362 39,076 358,789 26,218
vlsat3_c60 No 47 ∞ 688 3388 27,940 3254
vlsat3_c61 No 168 ∞ 8560 31,420 278,634 21,255
vlsat3_c62 No 240 ∞ 13,924 48,308 446,027 34,033
vlsat3_c63 No 306 ∞ 24,224 80,470 757,316 58,028
vlsat3_c64 No 42 ∞ 599 2951 24,505 2989
vlsat3_c65 No 45 ∞ 680 3352 27,626 3260
vlsat3_c66 No 142 ∞ 4788 18,156 158,813 12,665
vlsat3_c67 No 142 ∞ 9523 32,617 295,855 20,778
vlsat3_c68 No 74 ∞ 1906 7844 66,311 5963
vlsat3_c69 No 161 ∞ 6337 23,335 207,410 16,003
vlsat3_c70 No 166 ∞ 13,507 45,289 416,895 29,214
vlsat3_c71 No 244 ∞ 16,134 54,588 509,552 38,604
vlsat3_c72 No 265 ∞ 23,741 77,955 733,809 54,292
vlsat3_c73 No 75 ∞ 1805 7691 64,264 6007
vlsat3_c74 No 83 ∞ 2524 10,120 85,800 7197
vlsat3_c75 No 128 ∞ 5689 21,145 184,559 14,427
vlsat3_c76 No 325 ∞ 15,332 54,912 502,598 38,295
vlsat3_c77 No 352 ∞ 52,053 163,107 1,573,818 121,277
vlsat3_c78 No 28 ∞ 224 1272 11,161 1950
vlsat3_c79 No 54 ∞ 918 4390 36,028 3894
vlsat3_c80 No 129 ∞ 2615 11,273 95,129 8326
vlsat3_c81 No 148 ∞ 5549 20,337 180,591 14,244
vlsat3_c82 No 152 ∞ 10,953 37,207 339,477 23,692
vlsat3_c83 No 48 ∞ 754 3620 29,983 3404
vlsat3_c84 No 250 ∞ 16,443 55,671 518,111 39,521
vlsat3_c85 No 321 ∞ 46,286 145,186 1,398,753 106,030
vlsat3_c86 No 342 ∞ 50,614 158,590 1,529,678 117,056
vlsat3_c87 No 622 ∞ 192,992 591,324 5,798,866 482,885
vlsat3_c88 No 57 ∞ 1306 5330 45,661 4328
vlsat3_c89 No 113 ∞ 4010 15,598 133,659 10,895
vlsat3_c90 No 96 ∞ 3125 12,523 105,769 8784
vlsat3_c91 No 176 ∞ 9488 34,808 309,369 23,566
vlsat3_c92 No 61 ∞ 1248 5632 46,567 4639
vlsat3_c93 No 508 ∞ 89,854 284,590 2,748,178 217,818
vlsat3_c94 No 520 ∞ 135,460 677,296 5,717,072 491,025
vlsat3_c95 No 52 ∞ 1321 5527 46,866 4551
vlsat3_c96 No 40 ∞ 793 3511 29,788 3252
vlsat3_c97 No 118 ∞ 3673 14,347 123,480 10,259
vlsat3_c98 No 67 ∞ 1245 5839 47,756 4756
vlsat3_c99 No 159 ∞ 5105 19,583 172,632 14,093

3.4. Family "d" of VLSAT-3 formulas

This family is composed of 100 unsatisfiable formulas written in the QF_UFBV logic.

name (.smt2.bz2) satisfiable cardin cardout #asserts #operators size (.smt2) size (.smt2.bz2)
vlsat3_d00 No 27 217 3050 21,142 211,366 7609
vlsat3_d01 No 28 214 8576 59,647 582,970 20,326
vlsat3_d02 No 27 216 6975 48,495 474,574 16,465
vlsat3_d03 No 28 215 8576 59,649 591,585 20,311
vlsat3_d04 No 27 212 1819 12,503 117,077 5065
vlsat3_d05 No 27 219 3050 21,146 217,558 7622
vlsat3_d06 No 26 213 1407 9693 89,756 4035
vlsat3_d07 No 26 216 1463 10,103 97,847 4139
vlsat3_d08 No 27 211 5833 40,515 367,688 13,776
vlsat3_d09 No 28 211 9282 64,580 603,011 21,789
vlsat3_d10 No 26 213 1463 10,097 93,341 4125
vlsat3_d11 No 28 211 9523 66,255 618,612 22,378
vlsat3_d12 No 27 213 3050 21,134 199,006 7589
vlsat3_d13 No 28 211 13,507 94,071 877,190 32,232
vlsat3_d14 No 27 212 3050 21,132 195,921 7571
vlsat3_d15 No 28 211 11,362 78,960 737,253 27,813
vlsat3_d16 No 26 215 1463 10,101 96,343 4129
vlsat3_d17 No 27 213 1819 12,505 118,931 5067
vlsat3_d18 No 26 213 1306 8995 83,435 3840
vlsat3_d19 No 27 214 1487 10,240 99,160 4320
vlsat3_d20 No 27 216 3050 21,140 208,273 7565
vlsat3_d21 No 27 214 5557 38,553 366,896 13,316
vlsat3_d22 No 27 213 3180 22,023 207,351 7909
vlsat3_d23 No 28 221 9488 65,928 711,093 23,179
vlsat3_d24 No 28 211 4788 33,110 310,837 12,036
vlsat3_d25 No 28 210 5667 39,270 362,322 13,849
vlsat3_d26 No 26 214 688 4701 45,364 2648
vlsat3_d27 No 28 217 8750 60,862 621,127 21,080
vlsat3_d28 No 27 215 3050 21,138 205,182 7569
vlsat3_d29 No 28 212 15,832 110,174 1,043,253 39,543
vlsat3_d30 No 27 215 1892 13,041 127,641 5189
vlsat3_d31 No 27 218 3050 21,144 214,461 7610
vlsat3_d32 No 28 211 6337 43,896 411,218 15,356
vlsat3_d33 No 28 211 13,924 96,768 903,111 34,186
vlsat3_d34 No 27 213 4995 34,635 324,862 12,071
vlsat3_d35 No 28 216 8576 59,651 600,202 20,328
vlsat3_d36 No 27 211 3083 21,271 194,468 7939
vlsat3_d37 No 27 215 6975 48,493 467,558 16,445
vlsat3_d38 No 27 215 1811 12,477 122,229 5082
vlsat3_d39 No 28 220 9488 65,926 701,554 23,183
vlsat3_d40 No 27 213 2672 18,467 174,331 6888
vlsat3_d41 No 27 216 3125 21,617 213,133 7901
vlsat3_d42 No 26 229 1140 7892 92,175 3585
vlsat3_d43 No 27 211 4007 27,787 252,919 9615
vlsat3_d44 No 26 212 679 4640 43,386 2603
vlsat3_d45 No 28 220 8068 56,103 597,098 19,819
vlsat3_d46 No 26 214 396 2693 26,844 2051
vlsat3_d47 No 26 213 578 3968 37,891 2337
vlsat3_d48 No 27 224 4346 30,180 331,329 10,611
vlsat3_d49 No 28 214 12,108 84,137 821,900 29,777
vlsat3_d50 No 27 213 2508 17,319 163,671 6578
vlsat3_d51 No 28 213 7304 50,723 489,037 17,642
vlsat3_d52 No 26 213 591 4032 38,584 2442
vlsat3_d53 No 27 212 3741 25,891 239,756 9186
vlsat3_d54 No 26 221 1113 7687 80,658 3472
vlsat3_d55 No 26 224 1506 10,423 113,147 4287
vlsat3_d56 No 27 213 6363 44,223 413,842 14,984
vlsat3_d57 No 25 210 143 953 9861 1508
vlsat3_d58 No 27 210 551 3734 35,311 2384
vlsat3_d59 No 28 210 4685 32,333 299,138 11,874
vlsat3_d60 No 27 211 2609 17,962 164,651 6864
vlsat3_d61 No 28 211 18,157 126,483 1,178,705 45,459
vlsat3_d62 No 29 210 100,629 702,915 6,634,843 289,744
vlsat3_d63 No 27 211 6064 42,132 382,241 14,284
vlsat3_d64 No 28 211 10,023 69,725 650,953 23,790
vlsat3_d65 No 28 211 13,813 96,093 896,440 33,631
vlsat3_d66 No 26 214 585 4001 38,870 2419
vlsat3_d67 No 28 211 17,483 121,807 1,135,119 43,399
vlsat3_d68 No 29 210 59,070 412,341 3,893,868 160,478
vlsat3_d69 No 26 213 1321 9115 84,450 3832
vlsat3_d70 No 29 211 58,589 408,976 3,920,742 159,848
vlsat3_d71 No 28 211 17,079 118,979 1,108,859 42,554
vlsat3_d72 No 28 211 18,431 128,419 1,196,611 45,744
vlsat3_d73 No 28 210 22,645 157,849 1,447,493 57,325
vlsat3_d74 No 27 210 2840 19,577 176,333 7233
vlsat3_d75 No 26 213 686 4688 44,527 2581
vlsat3_d76 No 29 211 52,979 369,892 3,545,926 143,712
vlsat3_d77 No 29 210 93,919 656,005 6,192,321 268,258
vlsat3_d78 No 26 212 754 5156 47,994 2772
vlsat3_d79 No 27 210 1971 13,551 122,739 5273
vlsat3_d80 No 27 211 4803 33,335 302,948 11,453
vlsat3_d81 No 26 213 599 4091 39,102 2466
vlsat3_d82 No 27 219 1778 12,299 127,531 4844
vlsat3_d83 No 26 215 946 6518 62,903 3126
vlsat3_d84 No 27 211 5325 36,950 335,639 12,810
vlsat3_d85 No 28 210 8768 60,959 560,690 20,711
vlsat3_d86 No 210 210 160,338 1,119,945 10,890,215 484,365
vlsat3_d87 No 27 213 2933 20,324 191,446 7247
vlsat3_d88 No 27 212 3801 26,320 243,641 9260
vlsat3_d89 No 27 212 3285 22,741 210,781 8048
vlsat3_d90 No 27 211 4380 30,362 276,239 10,627
vlsat3_d91 No 28 210 7927 54,793 505,378 20,253
vlsat3_d92 No 28 210 7937 54,851 505,954 20,313
vlsat3_d93 No 26 231 1083 7497 89,978 3444
vlsat3_d94 No 27 210 3607 24,973 224,021 8825
vlsat3_d95 No 28 211 5408 37,414 350,945 13,421
vlsat3_d96 No 29 210 30,074 209,735 1,982,206 77,748
vlsat3_d97 No 28 211 21,311 148,543 1,383,619 54,067
vlsat3_d98 No 28 211 22,759 158,655 1,477,611 57,729
vlsat3_d99 No 29 210 59,140 412,804 3,898,335 163,077

3.5. Family "e" of VLSAT-3 formulas

This family is composed of 100 unsatisfiable formulas written in the QF_UFDT logic.

name (.smt2.bz2) satisfiable cardin cardout #asserts #operators size (.smt2) size (.smt2.bz2)
vlsat3_e00 No 56 16 1422 7438 54,273 3802
vlsat3_e01 No 80 15 2984 15,205 110,220 6472
vlsat3_e02 No 80 16 2985 15,253 110,470 6495
vlsat3_e03 No 56 12 1418 7264 53,311 3750
vlsat3_e04 No 164 11 13,018 65,233 480,915 25,382
vlsat3_e05 No 196 11 18,721 93,748 694,735 37,208
vlsat3_e06 No 70 14 1576 8125 59,480 4211
vlsat3_e07 No 118 14 4890 24,695 179,609 10,272
vlsat3_e08 No 198 10 11,173 55,980 415,671 23,071
vlsat3_e09 No 39 14 451 2500 19,040 2180
vlsat3_e10 No 57 13 1261 6513 47,941 3575
vlsat3_e11 No 136 28 8683 44,493 323,489 17,835
vlsat3_e12 No 56 17 1423 7489 54,539 3855
vlsat3_e13 No 124 13 5445 27,433 199,948 11,311
vlsat3_e14 No 203 14 13,126 65,875 487,589 27,396
vlsat3_e15 No 65 14 1435 7420 54,395 3924
vlsat3_e16 No 231 11 17,648 88,383 657,566 36,469
vlsat3_e17 No 306 11 23,928 119,783 897,082 51,473
vlsat3_e18 No 34 15 382 2195 16,726 2072
vlsat3_e19 No 56 13 1419 7303 53,572 3754
vlsat3_e20 No 112 12 5963 29,989 218,291 11,908
vlsat3_e21 No 120 17 6871 34,729 252,653 13,712
vlsat3_e22 No 85 14 2005 10,270 74,947 5033
vlsat3_e23 No 80 17 2986 15,304 110,736 6519
vlsat3_e24 No 220 15 15,636 78,465 582,468 32,805
vlsat3_e25 No 259 11 16,530 82,793 619,189 35,307
vlsat3_e26 No 122 14 4662 23,555 171,601 9994
vlsat3_e27 No 118 15 4891 24,740 179,843 10,343
vlsat3_e28 No 140 18 8627 43,558 318,759 17,705
vlsat3_e29 No 244 11 15,900 79,643 596,061 33,811
vlsat3_e30 No 70 17 1579 8269 60,167 4309
vlsat3_e31 No 72 14 1948 9985 72,849 4737
vlsat3_e32 No 161 11 6186 31,073 229,504 13,096
vlsat3_e33 No 196 12 18,722 93,784 694,921 37,210
vlsat3_e34 No 80 20 2989 15,475 111,543 6795
vlsat3_e35 No 127 11 3885 19,568 143,527 8618
vlsat3_e36 No 216 11 11,924 59,763 444,977 25,141
vlsat3_e37 No 310 11 23,771 118,998 891,658 51,616
vlsat3_e38 No 49 15 779 4180 31,009 2792
vlsat3_e39 No 128 11 4067 20,478 150,252 8958
vlsat3_e40 No 124 14 5446 27,475 200,166 11,256
vlsat3_e41 No 166 12 13,352 66,934 493,801 26,119
vlsat3_e42 No 48 13 718 3798 28,486 2627
vlsat3_e43 No 156 11 7050 35,393 260,566 14,458
vlsat3_e44 No 168 20 8411 42,585 312,383 17,738
vlsat3_e45 No 140 19 8628 43,615 319,057 17,798
vlsat3_e46 No 37 13 422 2318 17,833 2102
vlsat3_e47 No 39 15 451 2540 19,217 2200
vlsat3_e48 No 45 13 646 3438 25,897 2497
vlsat3_e49 No 79 19 1960 10,275 74,372 5102
vlsat3_e50 No 74 13 1844 9428 69,000 4672
vlsat3_e51 No 141 11 5923 29,758 218,628 12,293
vlsat3_e52 No 169 11 7133 35,808 264,893 15,222
vlsat3_e53 No 201 17 12,460 62,674 464,184 26,220
vlsat3_e54 No 41 14 501 2750 20,834 2284
vlsat3_e55 No 87 14 2598 13,235 96,184 6059
vlsat3_e56 No 174 21 9097 46,073 338,262 19,113
vlsat3_e57 No 155 14 9186 46,175 338,573 18,398
vlsat3_e58 No 61 16 1202 6338 46,406 3567
vlsat3_e59 No 129 12 3518 17,764 130,944 8186
vlsat3_e60 No 113 19 3915 20,050 145,349 8881
vlsat3_e61 No 129 11 4054 20,413 149,771 8979
vlsat3_e62 No 100 11 2539 12,838 93,941 5672
vlsat3_e63 No 118 11 2611 13,198 97,811 6501
vlsat3_e64 No 124 11 2768 13,983 103,596 6850
vlsat3_e65 No 135 11 3118 15,733 116,726 7538
vlsat3_e66 No 140 12 7273 36,539 268,086 14,577
vlsat3_e67 No 132 12 8072 40,534 296,803 15,799
vlsat3_e68 No 182 11 8875 44,518 329,636 18,495
vlsat3_e69 No 268 13 25,434 127,378 946,310 53,361
vlsat3_e70 No 96 11 2523 12,758 93,315 5644
vlsat3_e71 No 176 21 9332 47,248 347,081 19,654
vlsat3_e72 No 628 16 21,528 107,968 819,100 49,248
vlsat3_e73 No 236 11 23,476 117,523 875,808 47,654
vlsat3_e74 No 137 11 4890 24,593 180,859 10,572
vlsat3_e75 No 212 12 10,265 51,499 383,553 22,228
vlsat3_e76 No 145 13 4125 20,833 152,681 9287
vlsat3_e77 No 166 12 10,260 51,474 381,549 20,885
vlsat3_e78 No 182 12 15,492 77,634 573,931 30,527
vlsat3_e79 No 228 12 25,445 127,399 947,173 52,557
vlsat3_e80 No 32 13 236 1388 11,208 1793
vlsat3_e81 No 162 12 10,199 51,169 378,078 20,822
vlsat3_e82 No 222 11 21,186 106,073 790,089 42,475
vlsat3_e83 No 32 14 493 2710 20,454 2154
vlsat3_e84 No 61 19 1735 9150 66,230 4489
vlsat3_e85 No 65 12 1763 8989 65,837 4306
vlsat3_e86 No 140 12 8621 43,279 317,680 17,129
vlsat3_e87 No 67 11 1545 7868 58,195 3997
vlsat3_e88 No 245 13 11,808 59,248 442,243 26,079
vlsat3_e89 No 309 12 21,686 108,604 813,871 47,908
vlsat3_e90 No 220 14 23,406 117,275 870,638 47,319
vlsat3_e91 No 96 24 4273 22,145 158,990 9346
vlsat3_e92 No 173 11 7665 38,468 285,535 16,350
vlsat3_e93 No 170 12 11,340 56,874 419,197 23,321
vlsat3_e94 No 241 12 13,389 67,119 500,954 29,094
vlsat3_e95 No 328 12 25,257 126,459 948,359 56,559
vlsat3_e96 No 546 11 138,321 691,748 5,209,316 333,083
vlsat3_e97 No 621 43 149,152 748,383 5,638,045 366,091
vlsat3_e98 No 202 12 16,260 81,474 605,164 33,325
vlsat3_e99 No 48 31 1065 6658 46,536 3723

3.6. Family "f" of VLSAT-3 formulas

This family is composed of 100 unsatisfiable formulas written in the QF_UFIDL logic.

name (.smt2.bz2) satisfiable cardin cardout #asserts #operators size (.smt2) size (.smt2.bz2)
vlsat3_f00 No ∞ ∞ 1463 9406 59,532 4296
vlsat3_f01 No ∞ ∞ 13,172 70,315 476,471 26,877
vlsat3_f02 No ∞ ∞ 18,871 112,070 741,340 43,339
vlsat3_f03 No ∞ ∞ 3050 18,949 120,197 7753
vlsat3_f04 No ∞ ∞ 6975 39,718 260,598 14,855
vlsat3_f05 No ∞ ∞ 8750 50,200 330,663 20,151
vlsat3_f06 No ∞ ∞ 1463 9151 58,343 4192
vlsat3_f07 No ∞ ∞ 3050 17,770 114,700 7095
vlsat3_f08 No ∞ ∞ 6064 33,625 221,570 12,444
vlsat3_f09 No ∞ ∞ 1463 9529 60,106 4329
vlsat3_f10 No ∞ ∞ 6975 40,033 262,089 15,007
vlsat3_f11 No ∞ ∞ 13,172 70,777 478,692 26,659
vlsat3_f12 No ∞ ∞ 8068 47,714 314,228 19,927
vlsat3_f13 No ∞ ∞ 8193 44,890 299,104 16,519
vlsat3_f14 No ∞ ∞ 9523 51,850 347,234 19,240
vlsat3_f15 No ∞ ∞ 1306 8403 53,209 4033
vlsat3_f16 No ∞ ∞ 5449 31,000 203,572 12,488
vlsat3_f17 No ∞ ∞ 25,662 135,211 930,280 54,266
vlsat3_f18 No ∞ ∞ 1633 10,690 67,040 4942
vlsat3_f19 No ∞ ∞ 8750 50,569 332,425 20,246
vlsat3_f20 No ∞ ∞ 13,507 72,514 491,050 27,785
vlsat3_f21 No ∞ ∞ 1133 7750 48,304 3903
vlsat3_f22 No ∞ ∞ 1463 9649 60,666 4364
vlsat3_f23 No ∞ ∞ 9251 56,237 365,881 22,683
vlsat3_f24 No ∞ ∞ 3050 19,135 121,065 7796
vlsat3_f25 No ∞ ∞ 3460 21,283 135,150 8617
vlsat3_f26 No ∞ ∞ 17,869 95,676 653,711 38,736
vlsat3_f27 No ∞ ∞ 5890 33,876 221,343 13,515
vlsat3_f28 No ∞ ∞ 10,953 59,310 398,966 22,045
vlsat3_f29 No ∞ ∞ 13,415 74,535 501,712 30,787
vlsat3_f30 No ∞ ∞ 476 3740 23,130 2471
vlsat3_f31 No ∞ ∞ 1487 10,063 62,681 4673
vlsat3_f32 No ∞ ∞ 22,639 123,370 840,624 50,451
vlsat3_f33 No ∞ ∞ 568 4325 26,735 2660
vlsat3_f34 No ∞ ∞ 698 5151 31,885 2932
vlsat3_f35 No ∞ ∞ 4974 28,765 188,361 11,952
vlsat3_f36 No ∞ ∞ 1287 9550 58,448 4462
vlsat3_f37 No ∞ ∞ 1487 9913 61,980 4616
vlsat3_f38 No ∞ ∞ 24,224 129,551 891,692 54,888
vlsat3_f39 No ∞ ∞ 1248 8546 53,145 4208
vlsat3_f40 No ∞ ∞ 1633 11,185 69,287 5130
vlsat3_f41 No ∞ ∞ 16,805 93,685 634,820 40,142
vlsat3_f42 No ∞ ∞ 599 4400 27,433 2666
vlsat3_f43 No ∞ ∞ 1907 12,898 80,040 5790
vlsat3_f44 No ∞ ∞ 2318 14,684 92,557 6321
vlsat3_f45 No ∞ ∞ 918 6595 40,759 3539
vlsat3_f46 No ∞ ∞ 2477 15,670 98,742 6630
vlsat3_f47 No ∞ ∞ 16,183 88,597 600,480 34,982
vlsat3_f48 No ∞ ∞ 1113 7942 49,189 3979
vlsat3_f49 No ∞ ∞ 3362 19,815 127,649 7896
vlsat3_f50 No ∞ ∞ 7816 43,871 293,034 18,035
vlsat3_f51 No ∞ ∞ 1140 8560 52,349 4072
vlsat3_f52 No ∞ ∞ 1245 8468 52,704 4153
vlsat3_f53 No ∞ ∞ 1642 10,313 65,537 4799
vlsat3_f54 No ∞ ∞ 320 2400 15,479 1995
vlsat3_f55 No ∞ ∞ 1778 11,856 74,142 5222
vlsat3_f56 No ∞ ∞ 21,296 135,145 880,612 52,435
vlsat3_f57 No ∞ ∞ 716 4905 31,030 2766
vlsat3_f58 No ∞ ∞ 2465 15,380 98,122 7021
vlsat3_f59 No ∞ ∞ 2609 15,596 99,892 6377
vlsat3_f60 No ∞ ∞ 1017 7738 47,279 3833
vlsat3_f61 No ∞ ∞ 2473 15,700 99,156 6381
vlsat3_f62 No ∞ ∞ 13,541 76,345 514,172 32,275
vlsat3_f63 No ∞ ∞ 2255 13,557 86,982 5762
vlsat3_f64 No ∞ ∞ 3491 20,145 130,414 7921
vlsat3_f65 No ∞ ∞ 17,209 92,203 627,069 35,840
vlsat3_f66 No ∞ ∞ 688 4787 30,490 3048
vlsat3_f67 No ∞ ∞ 2029 12,948 81,946 6070
vlsat3_f68 No ∞ ∞ 15,140 81,175 552,061 30,850
vlsat3_f69 No ∞ ∞ 1506 10,733 66,174 4821
vlsat3_f70 No ∞ ∞ 3008 18,683 119,756 8467
vlsat3_f71 No ∞ ∞ 17,483 93,947 639,440 36,779
vlsat3_f72 No ∞ ∞ 7828 43,847 293,120 17,952
vlsat3_f73 No ∞ ∞ 13,122 71,815 483,268 27,621
vlsat3_f74 No ∞ ∞ 18,528 101,246 695,340 39,828
vlsat3_f75 No ∞ ∞ 2783 17,557 111,368 7376
vlsat3_f76 No ∞ ∞ 5350 31,205 204,994 13,163
vlsat3_f77 No ∞ ∞ 12,010 68,885 457,505 28,037
vlsat3_f78 No ∞ ∞ 1210 8552 52,593 4240
vlsat3_f79 No ∞ ∞ 1227 8563 52,858 4194
vlsat3_f80 No ∞ ∞ 8750 52,015 339,368 20,354
vlsat3_f81 No ∞ ∞ 756 5183 32,744 2857
vlsat3_f82 No ∞ ∞ 45,060 234,207 1,632,774 100,739
vlsat3_f83 No ∞ ∞ 46,286 241,214 1,680,402 104,819
vlsat3_f84 No ∞ ∞ 9895 54,409 364,082 20,702
vlsat3_f85 No ∞ ∞ 36,971 194,630 1,348,396 85,266
vlsat3_f86 No ∞ ∞ 144,336 740,733 5,258,988 356,379
vlsat3_f87 No ∞ ∞ 51,099 267,146 1,864,424 120,193
vlsat3_f88 No ∞ ∞ 1080 7680 47,297 3907
vlsat3_f89 No ∞ ∞ 1321 8410 53,520 3900
vlsat3_f90 No ∞ ∞ 10,563 58,460 390,369 22,404
vlsat3_f91 No ∞ ∞ 11,111 61,498 412,310 25,016
vlsat3_f92 No ∞ ∞ 28,173 171,962 1,146,562 79,733
vlsat3_f93 No ∞ ∞ 31,647 167,323 1,153,239 70,013
vlsat3_f94 No ∞ ∞ 31,597 167,073 1,151,471 69,954
vlsat3_f95 No ∞ ∞ 36,045 212,498 1,433,122 98,296
vlsat3_f96 No ∞ ∞ 40,702 213,845 1,485,531 94,957
vlsat3_f97 No ∞ ∞ 54,201 282,712 1,974,436 128,525
vlsat3_f98 No ∞ ∞ 24,050 127,399 875,592 50,237
vlsat3_f99 No ∞ ∞ 25,412 136,444 935,456 57,566

3.7. Family "g" of VLSAT-3 formulas

This family is composed of 100 satisfiable formulas written in the QF_BV logic.

name (.smt2.bz2) satisfiable #variables card #asserts #operators size (.smt2) size (.smt2.bz2)
vlsat3_g00 Yes 127 246 7987 40,041 630,825 15,954
vlsat3_g01 Yes 238 227 9157 45,517 558,844 20,806
vlsat3_g02 Yes 160 262 12,490 62,618 1,187,806 24,670
vlsat3_g03 Yes 160 263 12,490 62,626 1,200,255 24,703
vlsat3_g04 Yes 224 289 15,832 79,416 1,937,522 34,177
vlsat3_g05 Yes 192 293 18,397 92,337 2,320,944 37,077
vlsat3_g06 Yes 200 280 19,735 98,907 2,234,535 39,984
vlsat3_g07 Yes 233 252 23,058 115,232 1,972,983 46,967
vlsat3_g08 Yes 310 240 24,071 120,047 1,775,700 53,416
vlsat3_g09 Yes 224 284 24,788 124,156 2,959,040 54,093
vlsat3_g10 Yes 273 255 29,938 149,576 2,654,453 64,662
vlsat3_g11 Yes 366 241 33,438 166,778 2,501,929 75,247
vlsat3_g12 Yes 277 238 34,144 170,462 2,443,357 74,555
vlsat3_g13 Yes 313 252 37,418 186,872 3,209,230 81,871
vlsat3_g14 Yes 313 257 37,418 186,912 3,396,155 81,868
vlsat3_g15 Yes 299 252 38,293 191,275 3,277,155 84,384
vlsat3_g16 Yes 353 253 45,498 227,200 3,949,647 100,545
vlsat3_g17 Yes 353 254 45,498 227,208 3,995,113 100,454
vlsat3_g18 Yes 353 257 45,498 227,232 4,131,505 100,390
vlsat3_g19 Yes 385 239 45,580 227,434 3,315,374 102,356
vlsat3_g20 Yes 321 244 46,286 231,132 3,592,607 102,253
vlsat3_g21 Yes 329 249 52,913 264,291 4,372,775 117,994
vlsat3_g22 Yes 451 256 59,422 296,648 5,335,855 138,147
vlsat3_g23 Yes 519 253 63,046 314,608 5,476,560 151,238
vlsat3_g24 Yes 455 244 85,677 427,819 6,666,986 200,333
vlsat3_g25 Yes 138 269 9282 46,678 946,402 18,820
vlsat3_g26 Yes 139 261 9428 47,342 886,061 18,802
vlsat3_g27 Yes 201 279 12,645 63,447 1,420,665 27,302
vlsat3_g28 Yes 202 271 15,452 77,416 1,611,667 31,789
vlsat3_g29 Yes 194 253 16,918 84,618 1,461,680 33,903
vlsat3_g30 Yes 210 273 17,096 85,636 1,816,884 35,290
vlsat3_g31 Yes 210 274 17,096 85,644 1,833,928 35,305
vlsat3_g32 Yes 305 262 18,569 92,723 1,779,004 41,409
vlsat3_g33 Yes 228 276 19,386 97,074 2,120,687 40,452
vlsat3_g34 Yes 248 299 19,689 98,733 2,606,511 42,763
vlsat3_g35 Yes 341 265 21,828 108,970 2,157,333 49,856
vlsat3_g36 Yes 233 254 23,058 115,248 2,019,036 46,808
vlsat3_g37 Yes 219 269 23,292 116,566 2,385,066 49,232
vlsat3_g38 Yes 252 251 31,379 156,791 2,649,021 67,466
vlsat3_g39 Yes 308 2106 34,025 170,349 4,747,717 75,666
vlsat3_g40 Yes 315 291 43,690 218,540 5,440,481 97,784
vlsat3_g41 Yes 415 248 47,966 239,376 3,924,427 110,660
vlsat3_g42 Yes 415 249 47,966 239,384 3,972,366 110,555
vlsat3_g43 Yes 473 250 53,819 268,541 4,512,912 127,863
vlsat3_g44 Yes 365 250 60,276 301,042 5,042,838 136,553
vlsat3_g45 Yes 428 244 62,937 314,173 4,896,931 149,092
vlsat3_g46 Yes 159 268 11,229 56,363 1,136,524 22,289
vlsat3_g47 Yes 160 260 12,490 62,602 1,162,905 24,687
vlsat3_g48 Yes 290 259 16,805 83,909 1,559,575 37,453
vlsat3_g49 Yes 200 277 19,735 98,883 2,175,501 40,050
vlsat3_g50 Yes 273 252 29,938 149,552 2,564,735 64,350
vlsat3_g51 Yes 299 253 38,293 191,283 3,315,417 84,388
vlsat3_g52 Yes 353 252 45,498 227,192 3,904,180 100,456
vlsat3_g53 Yes 459 247 49,154 245,220 3,974,574 116,382
vlsat3_g54 Yes 325 266 52,331 261,525 5,208,584 117,528
vlsat3_g55 Yes 120 260 7029 35,377 652,446 14,634
vlsat3_g56 Yes 157 256 12,212 61,186 1,088,364 24,197
vlsat3_g57 Yes 248 298 19,689 98,725 2,586,899 42,784
vlsat3_g58 Yes 320 265 20,421 101,977 2,017,721 45,676
vlsat3_g59 Yes 233 232 23,904 119,302 1,565,349 49,924
vlsat3_g60 Yes 273 251 29,938 149,544 2,534,827 64,285
vlsat3_g61 Yes 263 232 30,228 150,862 1,982,825 65,142
vlsat3_g62 Yes 313 253 37,418 186,880 3,246,617 81,815
vlsat3_g63 Yes 421 243 51,099 254,989 3,923,374 117,053
vlsat3_g64 Yes 459 248 63,423 316,573 5,186,753 147,541
vlsat3_g65 Yes 164 2100 13,466 67,794 1,790,038 27,120
vlsat3_g66 Yes 216 275 22,500 112,660 2,437,018 45,623
vlsat3_g67 Yes 249 286 23,764 119,002 2,837,650 50,307
vlsat3_g68 Yes 224 292 15,832 79,440 1,984,811 34,220
vlsat3_g69 Yes 200 2101 19,625 98,525 2,632,855 39,892
vlsat3_g70 Yes 441 221 25,411 126,333 1,404,824 60,693
vlsat3_g71 Yes 220 256 23,613 118,065 2,109,568 48,624
vlsat3_g72 Yes 374 256 40,702 203,202 3,651,149 92,219
vlsat3_g73 Yes 187 279 17,173 86,115 1,926,487 34,335
vlsat3_g74 Yes 228 2132 25,662 128,902 4,238,613 54,682
vlsat3_g75 Yes 444 247 47,338 236,170 3,827,156 111,311
vlsat3_g76 Yes 549 256 70,640 352,542 6,348,343 171,092
vlsat3_g77 Yes 192 291 18,397 92,321 2,284,291 37,054
vlsat3_g78 Yes 400 295 74,565 372,777 9,588,216 173,363
vlsat3_g79 Yes 159 2104 12,665 63,831 1,736,635 26,945
vlsat3_g80 Yes 308 2107 34,025 170,357 4,781,658 75,581
vlsat3_g81 Yes 326 265 40,287 201,295 3,979,348 89,344
vlsat3_g82 Yes 315 290 43,690 218,532 5,396,860 97,768
vlsat3_g83 Yes 423 250 54,201 270,551 4,539,622 124,851
vlsat3_g84 Yes 309 259 17,964 89,666 1,667,655 40,935
vlsat3_g85 Yes 313 251 37,418 186,864 3,171,842 81,805
vlsat3_g86 Yes 216 272 22,500 112,636 2,369,674 45,522
vlsat3_g87 Yes 560 259 75,758 378,134 7,035,533 184,434
vlsat3_g88 Yes 194 252 16,918 84,610 1,444,793 33,709
vlsat3_g89 Yes 357 238 30,391 151,537 2,182,602 69,567
vlsat3_g90 Yes 248 297 19,689 98,717 2,567,286 42,696
vlsat3_g91 Yes 308 2109 34,025 170,373 4,849,537 75,645
vlsat3_g92 Yes 410 283 83,441 417,041 9,730,465 194,681
vlsat3_g93 Yes 300 2150 44,559 223,387 8,168,873 99,110
vlsat3_g94 Yes 250 251 30,881 154,305 2,606,849 66,220
vlsat3_g95 Yes 312 2108 35,160 176,032 4,976,148 78,072
vlsat3_g96 Yes 176 249 13,719 68,627 1,131,370 28,785
vlsat3_g97 Yes 304 272 42,220 211,060 4,453,848 93,113
vlsat3_g98 Yes 412 283 84,259 421,127 9,826,013 196,849
vlsat3_g99 Yes 300 2100 44,850 224,442 5,984,755 98,900

3.6. Family "h" of VLSAT-3 formulas

This family is composed of 100 satisfiable formulas written in the QF_DT logic.

name (.smt2.bz2) satisfiable #variables card #asserts #operators size (.smt2) size (.smt2.bz2)
vlsat3_h00 Yes 120 84 6938 27,784 240,736 18,779
vlsat3_h01 Yes 138 119 9497 42,531 359,241 27,350
vlsat3_h02 Yes 138 118 9496 42,292 357,678 27,124
vlsat3_h03 Yes 138 113 9491 41,127 350,073 26,230
vlsat3_h04 Yes 215 124 19,328 73,234 660,451 47,583
vlsat3_h05 Yes 200 129 19,553 75,169 672,790 48,688
vlsat3_h06 Yes 200 130 19,554 75,430 674,507 49,244
vlsat3_h07 Yes 194 193 18,869 93,661 788,035 60,119
vlsat3_h08 Yes 200 137 19,561 77,313 686,403 50,201
vlsat3_h09 Yes 200 139 19,563 77,869 690,577 50,341
vlsat3_h10 Yes 194 173 18,849 86,301 738,715 55,755
vlsat3_h11 Yes 628 210 21,722 109,054 945,959 78,648
vlsat3_h12 Yes 244 99 22,493 77,179 718,990 52,982
vlsat3_h13 Yes 155 53 9225 30,429 283,701 20,388
vlsat3_h14 Yes 214 80 16,048 54,462 508,825 38,168
vlsat3_h15 Yes 237 101 18,474 65,520 602,701 46,962
vlsat3_h16 Yes 175 35 12,096 37,476 360,701 25,972
vlsat3_h17 Yes 263 29 27,162 82,296 805,091 56,535
vlsat3_h18 Yes 231 37 18,499 56,827 556,018 39,409
vlsat3_h19 Yes 271 54 33,926 104,638 1,015,738 75,044
vlsat3_h20 Yes 231 36 17,472 53,674 526,159 37,614
vlsat3_h21 Yes 258 43 21,183 65,353 639,926 47,619
vlsat3_h22 Yes 189 66 10,287 35,149 326,520 24,809
vlsat3_h23 Yes 296 36 23,011 70,291 689,595 50,468
vlsat3_h24 Yes 259 32 16,551 50,643 497,433 36,364
vlsat3_h25 Yes 231 36 18,498 56,752 555,576 39,370
vlsat3_h26 Yes 157 46 10,815 34,513 331,349 24,207
vlsat3_h27 Yes 282 162 37,101 137,383 1,258,706 97,304
vlsat3_h28 Yes 245 50 11,845 37,983 366,539 27,849
vlsat3_h29 Yes 172 44 14,142 44,316 423,180 29,558
vlsat3_h30 Yes 180 36 12,786 39,616 381,385 27,522
vlsat3_h31 Yes 324 37 29,130 88,720 857,606 56,328
vlsat3_h32 Yes 154 56 11,129 36,465 341,590 24,370
vlsat3_h33 Yes 154 57 11,130 36,580 342,272 24,604
vlsat3_h34 Yes 260 259 33,463 167,209 1,427,678 114,319
vlsat3_h35 Yes 288 195 37,422 150,094 1,346,142 105,668
vlsat3_h36 Yes 266 114 23,530 83,470 770,278 60,299
vlsat3_h37 Yes 287 117 31,277 107,401 1,005,404 76,619
vlsat3_h38 Yes 385 53 45,247 138,495 1,360,230 103,281
vlsat3_h39 Yes 323 135 48,601 163,891 1,602,371 126,988
vlsat3_h40 Yes 201 79 12,522 43,726 404,010 31,173
vlsat3_h41 Yes 270 28 31,245 94,489 926,164 66,768
vlsat3_h42 Yes 143 52 9150 30,100 305,853 21,574
vlsat3_h43 Yes 265 29 23,504 71,322 698,983 50,036
vlsat3_h44 Yes 261 50 12,661 40,431 391,241 30,450
vlsat3_h45 Yes 323 129 48,595 162,295 1,591,859 125,726
vlsat3_h46 Yes 285 26 29,014 87,690 861,284 62,671
vlsat3_h47 Yes 292 229 41,987 178,171 1,576,362 125,628
vlsat3_h48 Yes 270 29 16,946 51,648 508,192 37,978
vlsat3_h49 Yes 621 110 149,219 459,645 4,516,690 373,871
vlsat3_h50 Yes 279 29 17,595 53,595 527,925 39,544
vlsat3_h51 Yes 282 31 25,260 76,708 752,394 54,414
vlsat3_h52 Yes 244 32 15,921 48,753 479,045 34,894
vlsat3_h53 Yes 233 32 23,702 72,096 703,572 48,876
vlsat3_h54 Yes 172 44 14,208 44,514 425,079 29,561
vlsat3_h55 Yes 408 407 67,406 367,458 3,120,268 274,116
vlsat3_h56 Yes 248 101 19,541 68,721 635,220 49,226
vlsat3_h57 Yes 500 204 119,303 399,319 3,805,065 312,354
vlsat3_h58 Yes 258 30 21,170 64,378 634,180 46,886
vlsat3_h59 Yes 621 114 149,223 460,549 4,522,578 374,765
vlsat3_h60 Yes 233 32 23,648 71,934 701,993 48,725
vlsat3_h61 Yes 302 210 42,839 172,405 1,548,423 122,085
vlsat3_h62 Yes 258 31 21,171 64,441 634,550 47,082
vlsat3_h63 Yes 500 202 119,301 398,503 3,799,573 311,990
vlsat3_h64 Yes 258 40 21,180 65,098 638,420 47,621
vlsat3_h65 Yes 293 119 32,621 111,903 1,048,433 81,249
vlsat3_h66 Yes 138 69 9212 32,326 294,267 21,191
vlsat3_h67 Yes 316 243 49,213 206,443 1,835,678 146,644
vlsat3_h68 Yes 258 39 21,179 65,017 637,942 47,526
vlsat3_h69 Yes 258 41 21,181 65,181 638,910 47,456
vlsat3_h70 Yes 284 26 28,792 87,024 854,751 62,075
vlsat3_h71 Yes 500 207 119,306 400,558 3,813,408 313,400
vlsat3_h72 Yes 260 53 13,333 42,753 412,712 31,415
vlsat3_h73 Yes 500 210 119,309 401,815 3,821,877 314,340
vlsat3_h74 Yes 258 33 21,173 64,573 635,326 47,002
vlsat3_h75 Yes 283 57 32,424 100,462 975,951 72,991
vlsat3_h76 Yes 319 222 45,664 186,052 1,670,005 130,888
vlsat3_h77 Yes 408 124 57,697 188,341 1,800,074 140,847
vlsat3_h78 Yes 961 62 446,926 1,344,558 13,354,406 1,185,278
vlsat3_h79 Yes 961 72 446,936 1,345,918 13,362,486 1,186,215
vlsat3_h80 Yes 333 37 33,496 101,818 1,001,541 74,662
vlsat3_h81 Yes 500 228 119,327 409,735 3,875,337 319,061
vlsat3_h82 Yes 224 50 21,418 66,702 644,264 46,287
vlsat3_h83 Yes 500 226 119,325 408,823 3,869,173 318,882
vlsat3_h84 Yes 159 68 11,137 37,965 351,934 24,567
vlsat3_h85 Yes 500 227 119,326 409,278 3,872,248 318,539
vlsat3_h86 Yes 501 500 105,952 567,354 4,827,193 398,650
vlsat3_h87 Yes 500 225 119,324 408,370 3,866,112 318,506
vlsat3_h88 Yes 272 31 18,201 55,531 545,856 39,801
vlsat3_h89 Yes 467 466 55,858 384,262 3,125,201 251,314
vlsat3_h90 Yes 500 218 119,317 405,255 3,845,077 316,437
vlsat3_h91 Yes 500 251 119,350 420,798 3,950,248 326,338
vlsat3_h92 Yes 258 34 21,174 64,642 635,732 47,266
vlsat3_h93 Yes 500 237 119,336 413,938 3,903,768 321,620
vlsat3_h94 Yes 258 38 21,178 64,938 637,476 47,427
vlsat3_h95 Yes 500 238 119,337 414,415 3,906,997 321,903
vlsat3_h96 Yes 194 57 16,780 53,530 511,261 35,401
vlsat3_h97 Yes 258 36 21,176 64,786 636,580 47,199
vlsat3_h98 Yes 500 229 119,328 410,194 3,878,440 319,196
vlsat3_h99 Yes 500 233 119,332 412,050 3,890,992 320,521

3.7. Family "i" of VLSAT-3 formulas

This family is composed of 100 satisfiable formulas written in the QF_IDL logic.

name (.smt2.bz2) satisfiable #variables card #asserts #operators size (.smt2) size (.smt2.bz2)
vlsat3_i00 Yes 215 ∞ 19,420 62,056 587,501 40,519
vlsat3_i01 Yes 236 ∞ 19,484 61,252 585,242 40,707
vlsat3_i02 Yes 228 ∞ 19,386 86,806 731,823 56,027
vlsat3_i03 Yes 200 ∞ 19,625 88,973 744,920 54,378
vlsat3_i04 Yes 160 ∞ 12,490 53,526 451,570 32,677
vlsat3_i05 Yes 273 ∞ 29,938 115,552 1,031,266 77,411
vlsat3_i06 Yes 150 ∞ 11,175 46,073 392,094 28,854
vlsat3_i07 Yes 191 ∞ 12,636 43,778 403,761 29,025
vlsat3_i08 Yes 270 ∞ 17,901 87,865 725,059 58,000
vlsat3_i09 Yes 159 ∞ 11,229 50,753 419,833 30,477
vlsat3_i10 Yes 162 ∞ 13,122 59,128 492,098 35,807
vlsat3_i11 Yes 287 ∞ 31,448 141,088 1,197,196 91,853
vlsat3_i12 Yes 244 ∞ 19,020 62,316 589,922 42,786
vlsat3_i13 Yes 315 ∞ 47,970 197,438 1,724,756 131,598
vlsat3_i14 Yes 489 ∞ 55,884 214,100 1,929,964 156,013
vlsat3_i15 Yes 112 ∞ 6064 27,186 222,167 17,106
vlsat3_i16 Yes 144 ∞ 8176 30,886 271,475 19,937
vlsat3_i17 Yes 159 ∞ 12,665 60,353 500,586 39,791
vlsat3_i18 Yes 252 ∞ 31,379 117,289 1,051,346 78,589
vlsat3_i19 Yes 527 ∞ 87,908 324,356 2,962,011 238,505
vlsat3_i20 Yes 625 ∞ 96,444 381,918 3,414,241 280,554
vlsat3_i21 Yes 584 ∞ 84,282 324,604 2,926,183 241,279
vlsat3_i22 Yes 584 ∞ 84,282 335,912 2,993,712 247,262
vlsat3_i23 Yes 480 ∞ 92,070 290,398 2,814,350 221,815
vlsat3_i24 Yes 249 ∞ 23,764 106,808 901,891 69,523
vlsat3_i25 Yes 502 ∞ 60,716 232,602 2,097,837 170,620
vlsat3_i26 Yes 589 ∞ 83,903 320,961 2,901,186 237,695
vlsat3_i27 Yes 559 ∞ 77,529 301,095 2,707,469 219,946
vlsat3_i28 Yes 579 ∞ 78,666 300,896 2,718,946 223,109
vlsat3_i29 Yes 625 ∞ 96,444 384,100 3,427,294 285,252
vlsat3_i30 Yes 170 ∞ 12,010 48,068 415,611 31,356
vlsat3_i31 Yes 329 ∞ 52,913 188,627 1,735,201 130,766
vlsat3_i32 Yes 625 ∞ 96,444 383,010 3,420,773 280,870
vlsat3_i33 Yes 224 ∞ 24,788 105,022 969,943 74,830
vlsat3_i34 Yes 498 ∞ 124,202 619,126 5,225,438 444,906
vlsat3_i35 Yes 498 ∞ 124,202 619,384 5,227,115 447,840
vlsat3_i36 Yes 260 ∞ 33,465 161,933 1,357,761 108,955
vlsat3_i37 Yes 277 ∞ 34,144 122,076 1,116,122 84,207
vlsat3_i38 Yes 623 ∞ 95,106 375,406 3,360,936 277,779
vlsat3_i39 Yes 623 ∞ 95,106 376,498 3,367,466 276,973
vlsat3_i40 Yes 498 ∞ 124,202 621,104 5,238,295 445,814
vlsat3_i41 Yes 524 ∞ 137,318 677,740 5,738,711 491,328
vlsat3_i42 Yes 405 ∞ 76,926 378,694 3,187,185 266,827
vlsat3_i43 Yes 645 ∞ 102,997 408,127 3,649,102 300,415
vlsat3_i44 Yes 645 ∞ 102,997 411,499 3,669,286 304,810
vlsat3_i45 Yes 219 ∞ 23,292 94,798 824,937 67,093
vlsat3_i46 Yes 409 ∞ 76,114 271,068 2,501,471 197,752
vlsat3_i47 Yes 615 ∞ 94,241 368,339 3,307,516 274,966
vlsat3_i48 Yes 164 ∞ 13,466 63,296 519,970 38,153
vlsat3_i49 Yes 606 ∞ 183,500 908,240 7,706,371 660,335
vlsat3_i50 Yes 704 ∞ 245,856 1,176,046 10,081,846 875,242
vlsat3_i51 Yes 802 ∞ 309,062 1,427,170 12,373,598 1,092,435
vlsat3_i52 Yes 800 ∞ 314,447 1,512,047 12,966,643 1,144,884
vlsat3_i53 Yes 252 ∞ 31,647 139,789 1,190,938 92,299
vlsat3_i54 Yes 511 ∞ 130,476 653,056 5,510,346 472,095
vlsat3_i55 Yes 834 ∞ 218,412 683,318 6,656,476 583,064
vlsat3_i56 Yes 813 ∞ 300,190 1,493,444 12,699,417 1,110,656
vlsat3_i57 Yes 926 ∞ 378,528 1,795,514 15,472,398 1,357,457
vlsat3_i58 Yes 224 ∞ 24,788 104,740 968,110 74,551
vlsat3_i59 Yes 499 ∞ 124,750 623,748 5,260,963 449,831
vlsat3_i60 Yes 606 ∞ 183,500 908,440 7,707,671 662,273
vlsat3_i61 Yes 444 ∞ 47,338 181,586 1,634,132 130,817
vlsat3_i62 Yes 813 ∞ 300,190 1,520,938 12,878,128 1,119,685
vlsat3_i63 Yes 800 ∞ 314,447 1,482,059 12,771,721 1,124,568
vlsat3_i64 Yes 252 ∞ 31,597 133,105 1,148,105 87,440
vlsat3_i65 Yes 756 ∞ 153,961 599,233 5,400,063 453,704
vlsat3_i66 Yes 736 ∞ 267,936 1,288,878 11,039,682 962,080
vlsat3_i67 Yes 752 ∞ 282,287 1,391,359 11,854,898 1,022,275
vlsat3_i68 Yes 859 ∞ 298,000 996,732 9,475,541 811,360
vlsat3_i69 Yes 709 ∞ 130,363 526,635 4,684,838 383,104
vlsat3_i70 Yes 622 ∞ 192,992 941,358 8,019,095 684,448
vlsat3_i71 Yes 762 ∞ 290,182 1,451,944 12,329,457 1,066,641
vlsat3_i72 Yes 830 ∞ 342,480 1,672,436 14,509,684 1,299,758
vlsat3_i73 Yes 919 ∞ 361,735 1,362,921 12,482,053 1,078,871
vlsat3_i74 Yes 498 ∞ 124,202 619,214 5,226,010 447,631
vlsat3_i75 Yes 500 ∞ 125,250 626,248 5,282,253 449,987
vlsat3_i76 Yes 520 ∞ 135,460 677,298 5,717,083 491,908
vlsat3_i77 Yes 830 ∞ 342,480 1,717,166 14,816,908 1,312,316
vlsat3_i78 Yes 511 ∞ 130,449 647,427 5,473,774 469,104
vlsat3_i79 Yes 830 ∞ 338,025 1,634,371 14,005,189 1,225,955
vlsat3_i80 Yes 756 ∞ 153,961 600,551 5,407,969 453,015
vlsat3_i81 Yes 802 ∞ 321,602 1,608,804 13,670,676 1,191,271
vlsat3_i82 Yes 818 ∞ 324,914 1,566,002 13,426,611 1,181,261
vlsat3_i83 Yes 250 ∞ 30,881 115,591 1,035,398 77,453
vlsat3_i84 Yes 752 ∞ 282,437 1,413,559 12,000,741 1,036,141
vlsat3_i85 Yes 216 ∞ 22,500 94,064 809,348 59,607
vlsat3_i86 Yes 834 ∞ 347,625 1,739,261 14,781,732 1,280,818
vlsat3_i87 Yes 798 ∞ 168,909 678,521 6,062,358 504,014
vlsat3_i88 Yes 549 ∞ 70,640 270,326 2,440,954 199,471
vlsat3_i89 Yes 575 ∞ 165,568 827,900 7,447,876 666,047
vlsat3_i90 Yes 365 ∞ 60,366 215,146 1,980,885 154,012
vlsat3_i91 Yes 1098 ∞ 303,971 981,191 9,532,394 777,448
vlsat3_i92 Yes 560 ∞ 75,758 289,930 2,618,953 214,539
vlsat3_i93 Yes 804 ∞ 293,357 1,210,883 10,813,110 931,784
vlsat3_i94 Yes 490 ∞ 120,295 601,473 5,072,378 431,511
vlsat3_i95 Yes 160 ∞ 12,490 53,328 450,421 32,278
vlsat3_i96 Yes 1081 ∞ 451,115 1,364,133 13,582,102 1,186,857
vlsat3_i97 Yes 1329 ∞ 509,080 1,540,508 15,644,933 1,329,195
vlsat3_i98 Yes 575 ∞ 164,438 751,882 6,961,844 595,926
vlsat3_i99 Yes 1324 ∞ 497,123 1,501,947 15,229,840 1,318,556

3.8. Family "j" of VLSAT-3 formulas

This family is composed of 100 satisfiable formulas written in the QF_UFBV logic.

name (.smt2.bz2) satisfiable cardin cardout #asserts #operators size (.smt2) size (.smt2.bz2)
vlsat3_j00 Yes 26 230 1000 6908 82,153 3339
vlsat3_j01 Yes 26 225 1250 8648 95,579 3762
vlsat3_j02 Yes 26 230 1280 8853 104,484 3951
vlsat3_j03 Yes 26 230 1665 11,533 135,215 4655
vlsat3_j04 Yes 26 230 1719 11,911 139,535 4767
vlsat3_j05 Yes 27 240 4770 33,168 440,996 11,618
vlsat3_j06 Yes 211 298 6048 42,200 965,735 15,087
vlsat3_j07 Yes 211 2108 7768 54,215 1,317,052 19,329
vlsat3_j08 Yes 28 251 8610 59,968 906,673 20,422
vlsat3_j09 Yes 28 232 12,394 86,226 1,065,718 30,635
vlsat3_j10 Yes 28 238 16,841 117,406 1,549,895 41,678
vlsat3_j11 Yes 28 293 18,397 128,387 2,712,525 45,763
vlsat3_j12 Yes 28 250 18,611 129,787 1,937,067 46,189
vlsat3_j13 Yes 28 2100 18,675 130,323 2,885,411 47,145
vlsat3_j14 Yes 28 275 18,975 132,373 2,452,609 47,576
vlsat3_j15 Yes 28 2120 19,495 136,013 3,405,711 48,456
vlsat3_j16 Yes 28 275 19,735 137,693 2,550,649 49,051
vlsat3_j17 Yes 28 2199 19,900 139,099 5,074,768 51,046
vlsat3_j18 Yes 29 268 21,399 149,153 2,656,053 56,171
vlsat3_j19 Yes 29 269 21,399 149,155 2,677,599 56,165
vlsat3_j20 Yes 29 270 21,399 149,157 2,699,147 56,169
vlsat3_j21 Yes 29 271 21,399 149,159 2,720,697 56,189
vlsat3_j22 Yes 29 264 21,696 151,341 2,606,192 54,800
vlsat3_j23 Yes 212 281 24,788 173,004 3,549,235 63,335
vlsat3_j24 Yes 29 221 25,411 176,594 1,951,460 70,765
vlsat3_j25 Yes 29 275 31,017 216,349 4,066,059 81,768
vlsat3_j26 Yes 29 2157 33,964 237,274 7,257,758 89,585
vlsat3_j27 Yes 29 251 38,293 267,254 4,097,038 102,088
vlsat3_j28 Yes 29 265 40,287 281,159 4,875,719 106,522
vlsat3_j29 Yes 29 2229 43,029 300,579 12,313,537 115,897
vlsat3_j30 Yes 29 2231 43,029 300,583 12,400,535 115,909
vlsat3_j31 Yes 29 2232 43,029 300,585 12,444,037 115,885
vlsat3_j32 Yes 29 2233 43,029 300,587 12,487,541 115,917
vlsat3_j33 Yes 29 2234 43,029 300,589 12,531,047 115,943
vlsat3_j34 Yes 29 2235 43,029 300,591 12,574,555 115,909
vlsat3_j35 Yes 29 2236 43,029 300,593 12,618,065 115,936
vlsat3_j36 Yes 29 2237 43,029 300,595 12,661,577 115,913
vlsat3_j37 Yes 29 2238 43,029 300,597 12,705,091 115,959
vlsat3_j38 Yes 29 2239 43,029 300,599 12,748,607 115,812
vlsat3_j39 Yes 29 2240 43,029 300,601 12,792,125 115,226
vlsat3_j40 Yes 29 2241 43,029 300,603 12,835,645 115,236
vlsat3_j41 Yes 29 251 43,522 303,797 4,656,201 116,824
vlsat3_j42 Yes 29 290 43,690 305,063 6,384,044 117,768
vlsat3_j43 Yes 29 244 46,286 323,125 4,627,178 125,484
vlsat3_j44 Yes 29 2210 49,105 343,193 13,104,351 134,061
vlsat3_j45 Yes 29 2108 50,382 351,916 8,271,545 138,125
vlsat3_j46 Yes 29 2158 60,144 420,215 12,892,748 163,979
vlsat3_j47 Yes 210 273 62,937 439,419 8,244,762 180,422
vlsat3_j48 Yes 210 274 62,937 439,421 8,307,856 180,551
vlsat3_j49 Yes 210 275 62,937 439,423 8,370,952 180,567
vlsat3_j50 Yes 210 277 62,937 439,427 8,497,150 180,588
vlsat3_j51 Yes 210 278 62,937 439,429 8,560,252 180,497
vlsat3_j52 Yes 29 214 73,016 509,698 5,104,955 209,864
vlsat3_j53 Yes 29 256 76,114 531,681 8,523,170 212,727
vlsat3_j54 Yes 29 256 76,216 532,395 8,534,594 213,482
vlsat3_j55 Yes 210 261 77,529 541,146 9,221,880 226,794
vlsat3_j56 Yes 210 263 82,118 573,207 9,932,079 238,973
vlsat3_j57 Yes 210 262 83,903 585,676 10,063,882 249,684
vlsat3_j58 Yes 29 243 85,677 598,458 8,478,226 241,508
vlsat3_j59 Yes 210 262 87,124 608,163 10,450,042 260,044
vlsat3_j60 Yes 29 221 93,051 650,074 7,159,740 265,322
vlsat3_j61 Yes 29 257 114,402 799,432 12,924,440 334,423
vlsat3_j62 Yes 29 281 114,402 799,480 15,673,640 334,760
vlsat3_j63 Yes 29 282 114,402 799,482 15,788,215 334,850
vlsat3_j64 Yes 29 283 114,402 799,484 15,902,792 334,585
vlsat3_j65 Yes 29 284 114,402 799,486 16,017,371 334,968
vlsat3_j66 Yes 29 285 114,402 799,488 16,131,952 334,843
vlsat3_j67 Yes 27 233 2178 15,112 187,214 5692
vlsat3_j68 Yes 27 237 2738 19,016 245,966 6985
vlsat3_j69 Yes 27 240 2970 20,628 275,695 7623
vlsat3_j70 Yes 211 288 5458 38,065 816,070 13,741
vlsat3_j71 Yes 28 241 9962 69,388 947,865 23,641
vlsat3_j72 Yes 28 2104 12,665 88,384 2,012,042 31,447
vlsat3_j73 Yes 29 230 21,399 149,077 1,838,787 55,864
vlsat3_j74 Yes 28 256 23,613 164,741 2,599,265 60,009
vlsat3_j75 Yes 28 2132 25,662 179,212 4,789,889 65,694
vlsat3_j76 Yes 29 272 42,220 294,770 5,406,555 112,729
vlsat3_j77 Yes 29 214 75,529 527,289 5,280,865 212,582
vlsat3_j78 Yes 210 268 3548 24,715 452,478 9306
vlsat3_j79 Yes 27 245 3924 27,286 383,408 9707
vlsat3_j80 Yes 27 248 5848 40,694 587,560 14,182
vlsat3_j81 Yes 28 2100 13,466 93,968 2,083,800 32,543
vlsat3_j82 Yes 27 250 2745 19,073 283,445 7178
vlsat3_j83 Yes 27 260 7029 48,961 791,304 16,883
vlsat3_j84 Yes 27 264 7680 53,502 895,352 18,432
vlsat3_j85 Yes 28 236 17,668 123,053 1,589,739 44,687
vlsat3_j86 Yes 28 236 18,694 130,235 1,682,079 46,651
vlsat3_j87 Yes 27 253 2956 20,565 314,219 7692
vlsat3_j88 Yes 27 238 3524 24,475 319,304 8724
vlsat3_j89 Yes 27 260 7200 50,158 810,456 17,224
vlsat3_j90 Yes 29 2150 44,559 311,311 9,199,715 120,325
vlsat3_j91 Yes 28 272 20,264 141,342 2,557,371 52,370
vlsat3_j92 Yes 29 241 32,521 226,344 3,150,450 84,473
vlsat3_j93 Yes 28 260 11,010 76,708 1,258,438 26,983
vlsat3_j94 Yes 212 280 24,788 173,002 3,524,276 63,291
vlsat3_j95 Yes 210 244 62,937 439,361 6,415,906 180,271
vlsat3_j96 Yes 27 253 4518 31,445 477,959 11,146
vlsat3_j97 Yes 28 292 18,397 128,385 2,693,933 45,771
vlsat3_j98 Yes 28 250 11,175 77,873 1,164,458 26,704
vlsat3_j99 Yes 28 268 11,229 78,260 1,374,356 26,968

3.9. Family "k" of VLSAT-3 formulas

This family is composed of 100 satisfiable formulas written in the QF_UFDT logic.

name (.smt2.bz2) satisfiable cardin cardout #asserts #operators size (.smt2) size (.smt2.bz2)
vlsat3_k00 Yes 138 137 9515 75,249 499,361 29,236
vlsat3_k01 Yes 138 118 9496 67,953 457,618 26,273
vlsat3_k02 Yes 138 115 9493 66,900 451,621 25,919
vlsat3_k03 Yes 164 125 13,132 88,660 608,299 34,527
vlsat3_k04 Yes 200 126 19,550 121,123 850,165 47,814
vlsat3_k05 Yes 200 127 19,551 121,504 852,344 47,915
vlsat3_k06 Yes 200 136 19,560 125,068 873,280 49,453
vlsat3_k07 Yes 200 137 19,561 125,479 875,639 49,930
vlsat3_k08 Yes 200 138 19,562 125,893 878,016 50,013
vlsat3_k09 Yes 258 48 21,188 109,228 811,213 47,674
vlsat3_k10 Yes 194 174 18,850 139,055 946,845 56,696
vlsat3_k11 Yes 233 93 20,295 114,123 821,284 48,250
vlsat3_k12 Yes 258 44 21,184 108,670 808,261 47,693
vlsat3_k13 Yes 213 41 8455 44,653 327,471 20,064
vlsat3_k14 Yes 155 54 9226 50,315 360,411 20,083
vlsat3_k15 Yes 244 32 15,921 81,029 603,325 34,597
vlsat3_k16 Yes 241 26 13,403 67,938 505,236 29,636
vlsat3_k17 Yes 266 112 23,528 136,064 974,243 60,308
vlsat3_k18 Yes 167 35 10,978 56,605 414,307 23,579
vlsat3_k19 Yes 154 57 11,130 60,324 434,224 24,241
vlsat3_k20 Yes 189 66 10,287 57,738 413,152 24,306
vlsat3_k21 Yes 258 43 21,183 108,538 807,563 47,656
vlsat3_k22 Yes 134 53 8528 46,668 333,489 18,638
vlsat3_k23 Yes 249 26 13,916 70,503 524,760 30,755
vlsat3_k24 Yes 187 65 10,000 56,110 401,514 23,783
vlsat3_k25 Yes 247 30 15,528 78,885 586,270 33,864
vlsat3_k26 Yes 259 32 16,588 84,364 627,811 36,270
vlsat3_k27 Yes 296 35 23,010 116,765 869,490 49,911
vlsat3_k28 Yes 194 68 10,870 61,048 437,068 25,857
vlsat3_k29 Yes 265 29 23,504 118,680 883,172 49,703
vlsat3_k30 Yes 157 46 10,815 57,088 418,565 23,913
vlsat3_k31 Yes 168 35 11,143 57,430 420,375 23,913
vlsat3_k32 Yes 154 56 11,129 60,153 433,318 24,126
vlsat3_k33 Yes 265 29 23,537 118,845 884,369 49,727
vlsat3_k34 Yes 203 78 13,190 74,803 534,819 31,647
vlsat3_k35 Yes 292 34 26,255 132,890 990,620 57,456
vlsat3_k36 Yes 180 36 12,786 65,748 482,369 27,136
vlsat3_k37 Yes 274 171 35,066 218,593 1,549,957 93,475
vlsat3_k38 Yes 208 83 13,289 76,488 545,771 33,001
vlsat3_k39 Yes 252 201 31,545 217,623 1,512,080 92,482
vlsat3_k40 Yes 259 32 16,438 83,614 622,246 35,940
vlsat3_k41 Yes 270 29 16,946 85,890 639,816 37,830
vlsat3_k42 Yes 282 31 25,260 127,633 950,511 54,824
vlsat3_k43 Yes 260 216 33,420 236,328 1,642,207 100,831
vlsat3_k44 Yes 621 88 149,197 757,293 5,685,293 370,047
vlsat3_k45 Yes 621 104 149,213 761,925 5,710,218 371,860
vlsat3_k46 Yes 288 197 37,424 244,644 1,720,782 105,087
vlsat3_k47 Yes 265 209 34,792 238,750 1,662,336 102,007
vlsat3_k48 Yes 282 192 37,131 240,279 1,693,446 103,098
vlsat3_k49 Yes 172 44 14,142 73,460 536,372 29,265
vlsat3_k50 Yes 233 32 23,648 119,664 888,310 48,662
vlsat3_k51 Yes 185 38 16,693 85,498 627,972 34,043
vlsat3_k52 Yes 258 41 21,181 108,283 806,215 47,524
vlsat3_k53 Yes 400 399 79,897 636,890 4,375,250 277,060
vlsat3_k54 Yes 621 95 149,204 759,225 5,695,555 370,948
vlsat3_k55 Yes 621 112 149,221 764,529 5,724,986 373,508
vlsat3_k56 Yes 201 79 12,522 71,695 511,922 30,939
vlsat3_k57 Yes 292 225 41,798 284,140 2,022,097 121,675
vlsat3_k58 Yes 159 68 11,137 62,383 446,482 24,153
vlsat3_k59 Yes 245 47 11,165 58,974 433,357 26,610
vlsat3_k60 Yes 187 38 17,059 87,328 641,678 34,804
vlsat3_k61 Yes 258 30 21,170 107,095 799,945 46,880
vlsat3_k62 Yes 233 32 23,702 119,934 890,321 48,697
vlsat3_k63 Yes 302 213 42,842 281,518 1,982,386 122,373
vlsat3_k64 Yes 172 44 14,208 73,790 538,799 29,437
vlsat3_k65 Yes 292 39 21,479 109,540 815,124 47,328
vlsat3_k66 Yes 256 16 9280 46,728 351,964 21,505
vlsat3_k67 Yes 245 50 11,845 62,800 460,963 28,153
vlsat3_k68 Yes 258 35 21,175 107,590 802,555 47,185
vlsat3_k69 Yes 295 27 30,957 155,784 1,162,286 68,383
vlsat3_k70 Yes 258 31 21,171 107,188 800,435 46,933
vlsat3_k71 Yes 316 204 42,756 275,490 1,953,201 118,588
vlsat3_k72 Yes 316 243 49,213 333,788 2,338,794 146,719
vlsat3_k73 Yes 150 50 11,074 58,945 425,479 23,286
vlsat3_k74 Yes 279 29 17,595 89,135 664,561 39,323
vlsat3_k75 Yes 258 32 21,172 107,284 800,941 46,994
vlsat3_k76 Yes 258 40 21,180 108,160 805,565 47,447
vlsat3_k77 Yes 258 42 21,182 108,409 806,881 47,592
vlsat3_k78 Yes 365 364 65,923 527,085 3,613,489 229,011
vlsat3_k79 Yes 261 50 12,661 66,880 491,873 30,195
vlsat3_k80 Yes 308 125 33,841 192,205 1,390,272 85,633
vlsat3_k81 Yes 500 216 119,315 665,803 4,874,929 315,952
vlsat3_k82 Yes 500 220 119,319 668,425 4,890,233 316,300
vlsat3_k83 Yes 500 229 119,328 674,500 4,925,720 320,759
vlsat3_k84 Yes 500 223 119,322 670,423 4,901,900 317,938
vlsat3_k85 Yes 500 226 119,325 672,448 4,913,729 317,522
vlsat3_k86 Yes 500 218 119,317 667,108 4,882,545 317,266
vlsat3_k87 Yes 500 222 119,321 669,754 4,897,993 317,588
vlsat3_k88 Yes 315 314 49,630 394,945 2,699,854 171,415
vlsat3_k89 Yes 2317 7 67,403 337,064 2,600,725 166,353
vlsat3_k90 Yes 277 53 14,251 75,283 554,105 33,998
vlsat3_k91 Yes 500 225 119,324 671,770 4,909,768 319,050
vlsat3_k92 Yes 451 38 58,696 295,513 2,210,703 131,786
vlsat3_k93 Yes 500 241 119,340 682,978 4,975,304 323,018
vlsat3_k94 Yes 194 57 16,780 88,574 647,613 35,304
vlsat3_k95 Yes 435 17 83,685 418,799 3,149,499 193,817
vlsat3_k96 Yes 500 243 119,342 684,433 4,983,820 324,096
vlsat3_k97 Yes 500 249 119,348 688,870 5,009,800 327,100
vlsat3_k98 Yes 500 232 119,331 676,579 4,937,873 319,534
vlsat3_k99 Yes 500 242 119,341 683,704 4,979,553 323,995

3.10. Family "l" of VLSAT-3 formulas

This family is composed of 100 satisfiable formulas written in the QF_UFIDL logic.

name (.smt2.bz2) satisfiable cardin cardout #asserts #operators size (.smt2) size (.smt2.bz2)
vlsat3_l00 Yes ∞ ∞ 19,625 144,910 912,432 55,020
vlsat3_l01 Yes ∞ ∞ 19,625 145,189 913,920 55,179
vlsat3_l02 Yes ∞ ∞ 19,625 147,565 926,592 56,584
vlsat3_l03 Yes ∞ ∞ 19,625 153,889 960,320 60,608
vlsat3_l04 Yes ∞ ∞ 19,625 156,805 975,359 62,521
vlsat3_l05 Yes ∞ ∞ 19,625 157,978 982,115 63,669
vlsat3_l06 Yes ∞ ∞ 13,890 158,430 925,464 63,171
vlsat3_l07 Yes ∞ ∞ 21,173 132,481 873,055 55,057
vlsat3_l08 Yes ∞ ∞ 17,209 104,878 688,506 40,626
vlsat3_l09 Yes ∞ ∞ 19,420 166,325 1,025,143 67,166
vlsat3_l10 Yes ∞ ∞ 16,918 111,755 721,367 42,793
vlsat3_l11 Yes ∞ ∞ 45,580 273,055 1,831,947 117,212
vlsat3_l12 Yes ∞ ∞ 12,108 93,498 579,108 35,806
vlsat3_l13 Yes ∞ ∞ 25,512 150,310 1,005,644 62,291
vlsat3_l14 Yes ∞ ∞ 24,224 152,474 1,004,253 63,721
vlsat3_l15 Yes ∞ ∞ 47,966 297,573 1,982,204 128,661
vlsat3_l16 Yes ∞ ∞ 24,725 154,603 1,015,962 62,892
vlsat3_l17 Yes ∞ ∞ 45,580 272,023 1,826,845 115,507
vlsat3_l18 Yes ∞ ∞ 32,105 258,500 1,622,142 107,737
vlsat3_l19 Yes ∞ ∞ 47,966 299,760 1,993,042 129,878
vlsat3_l20 Yes ∞ ∞ 32,105 250,382 1,578,846 102,383
vlsat3_l21 Yes ∞ ∞ 32,105 261,830 1,639,902 110,400
vlsat3_l22 Yes ∞ ∞ 5689 42,992 262,249 16,371
vlsat3_l23 Yes ∞ ∞ 36,971 215,672 1,451,945 92,410
vlsat3_l24 Yes ∞ ∞ 16,443 103,568 678,718 42,124
vlsat3_l25 Yes ∞ ∞ 23,058 149,877 977,590 59,293
vlsat3_l26 Yes ∞ ∞ 24,071 155,403 1,017,479 65,374
vlsat3_l27 Yes ∞ ∞ 38,293 235,010 1,561,568 98,564
vlsat3_l28 Yes ∞ ∞ 9521 59,019 388,822 25,251
vlsat3_l29 Yes ∞ ∞ 18,687 118,766 772,592 45,653
vlsat3_l30 Yes ∞ ∞ 35,170 285,487 1,793,268 121,357
vlsat3_l31 Yes ∞ ∞ 47,966 296,475 1,976,764 130,025
vlsat3_l32 Yes ∞ ∞ 11,111 70,969 458,002 28,183
vlsat3_l33 Yes ∞ ∞ 35,170 288,262 1,808,068 122,420
vlsat3_l34 Yes ∞ ∞ 37,222 295,533 1,864,240 123,595
vlsat3_l35 Yes ∞ ∞ 37,222 301,869 1,898,032 128,314
vlsat3_l36 Yes ∞ ∞ 32,521 480,524 2,785,730 193,879
vlsat3_l37 Yes ∞ ∞ 57,982 417,135 2,682,632 173,284
vlsat3_l38 Yes ∞ ∞ 15,332 155,238 923,320 58,993
vlsat3_l39 Yes ∞ ∞ 22,683 143,005 940,721 59,428
vlsat3_l40 Yes ∞ ∞ 46,406 375,310 2,368,413 159,323
vlsat3_l41 Yes ∞ ∞ 57,982 417,990 2,687,192 173,860
vlsat3_l42 Yes ∞ ∞ 47,970 388,525 2,450,989 165,432
vlsat3_l43 Yes ∞ ∞ 65,043 668,252 4,063,251 277,412
vlsat3_l44 Yes ∞ ∞ 12,212 85,119 537,551 32,513
vlsat3_l45 Yes ∞ ∞ 43,834 363,240 2,279,474 152,069
vlsat3_l46 Yes ∞ ∞ 16,666 106,186 694,682 43,725
vlsat3_l47 Yes ∞ ∞ 125,692 1,006,204 6,427,518 448,994
vlsat3_l48 Yes ∞ ∞ 35,624 222,364 1,474,900 95,685
vlsat3_l49 Yes ∞ ∞ 47,338 295,161 1,963,447 130,174
vlsat3_l50 Yes ∞ ∞ 35,153 217,390 1,440,167 90,335
vlsat3_l51 Yes ∞ ∞ 45,762 378,581 2,382,072 158,664
vlsat3_l52 Yes ∞ ∞ 21,733 138,493 908,267 57,807
vlsat3_l53 Yes ∞ ∞ 164,523 1,555,162 9,695,931 661,032
vlsat3_l54 Yes ∞ ∞ 38,293 235,745 1,565,198 98,679
vlsat3_l55 Yes ∞ ∞ 77,738 632,091 4,006,717 274,165
vlsat3_l56 Yes ∞ ∞ 46,406 379,702 2,391,837 161,787
vlsat3_l57 Yes ∞ ∞ 65,043 672,530 4,086,067 280,662
vlsat3_l58 Yes ∞ ∞ 18,443 115,570 759,768 47,526
vlsat3_l59 Yes ∞ ∞ 37,418 233,652 1,551,719 96,487
vlsat3_l60 Yes ∞ ∞ 63,936 511,060 3,242,055 221,361
vlsat3_l61 Yes ∞ ∞ 77,738 617,841 3,930,717 266,536
vlsat3_l62 Yes ∞ ∞ 36,990 230,767 1,531,555 99,558
vlsat3_l63 Yes ∞ ∞ 54,201 335,497 2,235,344 147,866
vlsat3_l64 Yes ∞ ∞ 63,423 381,370 2,563,824 167,396
vlsat3_l65 Yes ∞ ∞ 164,523 1,553,947 9,689,451 660,926
vlsat3_l66 Yes ∞ ∞ 22,141 621,577 3,440,743 245,212
vlsat3_l67 Yes ∞ ∞ 55,352 451,949 2,854,542 194,523
vlsat3_l68 Yes ∞ ∞ 9117 61,366 388,556 23,041
vlsat3_l69 Yes ∞ ∞ 96,444 623,123 4,128,247 280,046
vlsat3_l70 Yes ∞ ∞ 95,106 619,200 4,095,703 278,223
vlsat3_l71 Yes ∞ ∞ 26,548 167,332 1,102,675 70,436
vlsat3_l72 Yes ∞ ∞ 72,225 680,480 4,178,911 282,519
vlsat3_l73 Yes ∞ ∞ 24,071 154,593 1,013,486 65,254
vlsat3_l74 Yes ∞ ∞ 82,118 536,371 3,542,615 241,736
vlsat3_l75 Yes ∞ ∞ 7401 56,958 352,236 23,565
vlsat3_l76 Yes ∞ ∞ 12,931 81,843 530,777 32,561
vlsat3_l77 Yes ∞ ∞ 56,145 466,238 2,938,916 199,133
vlsat3_l78 Yes ∞ ∞ 69,298 573,873 3,624,723 246,739
vlsat3_l79 Yes ∞ ∞ 148,022 1,222,049 7,773,887 545,073
vlsat3_l80 Yes ∞ ∞ 54,241 446,019 2,811,608 190,083
vlsat3_l81 Yes ∞ ∞ 65,248 533,565 3,374,298 228,603
vlsat3_l82 Yes ∞ ∞ 105,954 906,016 5,708,418 396,665
vlsat3_l83 Yes ∞ ∞ 76,532 624,755 3,962,441 269,297
vlsat3_l84 Yes ∞ ∞ 70,279 583,885 3,702,243 267,640
vlsat3_l85 Yes ∞ ∞ 99,132 637,527 4,229,662 288,318
vlsat3_l86 Yes ∞ ∞ 60,423 495,192 3,127,692 215,837
vlsat3_l87 Yes ∞ ∞ 282,437 2,260,054 14,520,806 1,018,046
vlsat3_l88 Yes ∞ ∞ 60,627 512,697 3,222,005 218,585
vlsat3_l89 Yes ∞ ∞ 77,240 649,222 4,094,004 280,504
vlsat3_l90 Yes ∞ ∞ 102,997 667,458 4,420,527 301,900
vlsat3_l91 Yes ∞ ∞ 17,096 130,103 811,923 49,171
vlsat3_l92 Yes ∞ ∞ 64,039 615,010 3,756,942 253,680
vlsat3_l93 Yes ∞ ∞ 245,802 1,967,854 12,631,928 885,313
vlsat3_l94 Yes ∞ ∞ 15,446 90,617 601,627 35,237
vlsat3_l95 Yes ∞ ∞ 68,549 576,499 3,632,782 249,216
vlsat3_l96 Yes ∞ ∞ 183,500 1,468,046 9,405,511 660,084
vlsat3_l97 Yes ∞ ∞ 10,635 67,890 438,020 26,862
vlsat3_l98 Yes ∞ ∞ 321,602 2,572,404 16,540,756 1,165,564
vlsat3_l99 Yes ∞ ∞ 79,681 652,354 4,133,448 281,732

4. History of versions - Contributors

Version 1.48 - Date 2022/01/04 17:46:11

Back to the CADP Home Page