001-sdiv15prop.real-time.png |
unsat, 640s, 12.1%
|
unsat, 389s, 22.7%
|
unsat, 371s, 15.2%
|
unsat, 294s, 6.8%
|
002-sdiv16prop.real-time.png |
-, 1001s, 11.7%
|
-, 1001s, 23.5%
|
unsat, 814s, 13.5%
|
unsat, 887s, 9.5%
|
003-sdiv17prop.real-time.png |
-, 1001s, 11.8%
|
-, 1001s, 23.6%
|
-, 1001s, 15.2%
|
-, 1001s, 8.7%
|
004-sdiv20prop.real-time.png |
-, 1001s, 12.2%
|
-, 1001s, 31.7%
|
-, 1001s, 26.5%
|
-, 1001s, 16.8%
|
005-sdiv25prop.real-time.png |
-, 1001s, 13.3%
|
-, 1001s, 29.3%
|
-, 1001s, 18.3%
|
-, 1001s, 16.7%
|
006-sdiv30prop.real-time.png |
-, 1001s, 15.3%
|
-, 1001s, 27.9%
|
-, 1001s, 16.7%
|
-, 1001s, 7.7%
|
007-sdiv40prop.real-time.png |
-, 1001s, 20.0%
|
-, 1001s, 29.8%
|
-, 1001s, 11.5%
|
-, 1001s, 8.3%
|
008-udiv35prop.real-time.png |
-, 1001s, 25.7%
|
unsat, 160s, 21.6%
|
unsat, 124s, 11.5%
|
unsat, 176s, 9.2%
|
009-udiv40prop.real-time.png |
-, 1001s, 26.7%
|
unsat, 722s, 24.2%
|
unsat, 848s, 13.9%
|
unsat, 747s, 7.8%
|
010-udiv45prop.real-time.png |
-, 1001s, 27.6%
|
-, 1001s, 27.2%
|
-, 1001s, 10.2%
|
-, 1001s, 6.1%
|
011-udiv46prop.real-time.png |
-, 1001s, 27.6%
|
-, 1001s, 24.6%
|
-, 1001s, 9.7%
|
-, 1001s, 7.7%
|
012-udiv47prop.real-time.png |
-, 1001s, 28.2%
|
-, 1001s, 25.7%
|
-, 1001s, 10.0%
|
-, 1001s, 10.1%
|
013-udiv48prop.real-time.png |
-, 1001s, 28.0%
|
-, 1001s, 25.6%
|
-, 1001s, 10.1%
|
-, 1001s, 11.2%
|
014-uniqinv20prop.real-time.png |
-, 1001s, 12.5%
|
unsat, 665s, 22.2%
|
unsat, 718s, 14.5%
|
unsat, 391s, 7.1%
|
015-uniqinv25prop.real-time.png |
-, 1001s, 13.0%
|
-, 1001s, 20.5%
|
-, 1001s, 14.3%
|
-, 1001s, 8.5%
|
016-uniqinv30prop.real-time.png |
-, 1001s, 13.4%
|
-, 1001s, 21.5%
|
-, 1001s, 17.0%
|
-, 1001s, 13.2%
|
017-uniqinv40prop.real-time.png |
-, 1001s, 16.3%
|
-, 1001s, 26.1%
|
-, 1001s, 13.2%
|
-, 1001s, 8.9%
|
018-uniqinv45prop.real-time.png |
-, 1001s, 17.8%
|
-, 1001s, 25.1%
|
-, 1001s, 15.1%
|
-, 1001s, 9.4%
|
019-uniqinv46prop.real-time.png |
-, 1001s, 17.8%
|
-, 1001s, 26.8%
|
-, 1001s, 23.5%
|
-, 1001s, 10.3%
|
020-uniqinv47prop.real-time.png |
-, 1001s, 18.7%
|
-, 1001s, 29.6%
|
-, 1001s, 17.5%
|
-, 1001s, 8.9%
|
021-20180321_110704973_p_cnf_320_1120.real-time.png |
sat, 807s, 9.5%
|
-, 1001s, 46.4%
|
-, 1001s, 26.5%
|
-, 1001s, 10.8%
|
022-20180321_110706599_p_cnf_320_1120.real-time.png |
-, 1001s, 9.7%
|
-, 1001s, 45.2%
|
-, 1001s, 15.9%
|
-, 1001s, 8.2%
|
023-20180321_110707239_p_cnf_320_1120.real-time.png |
sat, 574s, 9.5%
|
-, 1001s, 46.0%
|
-, 1001s, 25.8%
|
-, 1001s, 18.9%
|
024-20180321_140823961_p_cnf_320_1120.real-time.png |
-, 1001s, 9.6%
|
sat, 849s, 45.8%
|
-, 1001s, 26.3%
|
-, 1001s, 20.8%
|
025-20180321_140824282_p_cnf_320_1120.real-time.png |
-, 1001s, 9.5%
|
-, 1001s, 46.1%
|
-, 1001s, 25.2%
|
-, 1001s, 20.9%
|
026-20180321_140826713_p_cnf_320_1120.real-time.png |
sat, 376s, 9.1%
|
-, 1001s, 46.5%
|
-, 1001s, 14.1%
|
-, 1001s, 9.4%
|
027-20180321_140827428_p_cnf_320_1120.real-time.png |
-, 1001s, 9.6%
|
-, 1001s, 46.1%
|
-, 1001s, 26.3%
|
-, 1001s, 7.4%
|
028-20180321_140833987_p_cnf_320_1120.real-time.png |
sat, 906s, 9.7%
|
-, 1001s, 46.6%
|
-, 1001s, 24.5%
|
-, 1001s, 9.1%
|
029-20180322_164223076_p_cnf_320_1120.real-time.png |
-, 1001s, 10.1%
|
-, 1001s, 44.0%
|
-, 1001s, 26.7%
|
-, 1001s, 7.9%
|
030-20180322_164224543_p_cnf_320_1120.real-time.png |
-, 1001s, 9.6%
|
-, 1001s, 46.8%
|
-, 1001s, 16.0%
|
-, 1001s, 20.4%
|
031-20180322_164226378_p_cnf_320_1120.real-time.png |
sat, 585s, 9.6%
|
-, 1001s, 45.9%
|
-, 1001s, 22.0%
|
-, 1001s, 20.6%
|
032-20180322_164226661_p_cnf_320_1120.real-time.png |
-, 1001s, 9.5%
|
-, 1001s, 46.4%
|
-, 1001s, 26.1%
|
sat, 643s, 10.7%
|
033-20180322_164238439_p_cnf_320_1120.real-time.png |
sat, 756s, 9.3%
|
-, 1001s, 42.9%
|
-, 1001s, 22.9%
|
-, 1001s, 20.3%
|
034-20180322_164241329_p_cnf_320_1120.real-time.png |
sat, 516s, 9.1%
|
-, 1001s, 43.1%
|
-, 1001s, 26.4%
|
-, 1001s, 10.8%
|
035-20180322_164241842_p_cnf_320_1120.real-time.png |
sat, 17s, 6.4%
|
-, 1001s, 46.2%
|
-, 1001s, 16.8%
|
-, 1001s, 18.5%
|
036-20180322_164245263_p_cnf_320_1120.real-time.png |
sat, 105s, 7.8%
|
-, 1001s, 47.5%
|
-, 1001s, 26.5%
|
-, 1001s, 9.0%
|
037-20180326_095801070_p_cnf_320_1120.real-time.png |
sat, 268s, 8.9%
|
-, 1001s, 46.2%
|
-, 1001s, 25.8%
|
-, 1001s, 21.7%
|
038-20180326_095804286_p_cnf_320_1120.real-time.png |
-, 1001s, 10.1%
|
-, 1001s, 46.2%
|
-, 1001s, 26.1%
|
-, 1001s, 21.0%
|
039-20180326_095804936_p_cnf_320_1120.real-time.png |
sat, 669s, 9.4%
|
-, 1001s, 45.7%
|
-, 1001s, 25.5%
|
-, 1001s, 21.2%
|
040-20180326_095805836_p_cnf_320_1120.real-time.png |
sat, 738s, 9.4%
|
-, 1001s, 46.1%
|
-, 1001s, 24.6%
|
-, 1001s, 8.6%
|
041-gto_p50c291.real-time.png |
-, 1001s, 24.9%
|
-, 1001s, 54.3%
|
-, 1001s, 31.5%
|
-, 1001s, 25.7%
|
042-gto_p50c307.real-time.png |
-, 1001s, 24.9%
|
-, 1001s, 54.0%
|
-, 1001s, 25.8%
|
-, 1001s, 19.2%
|
043-gto_p50c311.real-time.png |
-, 1001s, 24.9%
|
-, 1001s, 42.9%
|
-, 1001s, 24.2%
|
-, 1001s, 18.3%
|
044-gto_p50c312.real-time.png |
-, 1001s, 26.2%
|
-, 1001s, 54.2%
|
-, 1001s, 24.0%
|
-, 1001s, 24.7%
|
045-gto_p50c314.real-time.png |
-, 1001s, 26.2%
|
-, 1001s, 44.5%
|
-, 1001s, 27.1%
|
-, 1001s, 19.0%
|
046-gto_p50c314_1.real-time.png |
-, 1001s, 25.2%
|
-, 1001s, 40.5%
|
-, 1001s, 29.6%
|
-, 1001s, 19.9%
|
047-gto_p50c345.real-time.png |
-, 1001s, 28.2%
|
-, 1001s, 44.5%
|
-, 1001s, 23.3%
|
-, 1001s, 19.5%
|
048-gto_p50c345_1.real-time.png |
-, 1001s, 24.6%
|
-, 1001s, 42.1%
|
-, 1001s, 23.4%
|
-, 1001s, 15.4%
|
049-gto_p60c231.real-time.png |
unsat, 37s, 12.1%
|
unsat, 112s, 46.4%
|
unsat, 44s, 17.1%
|
unsat, 46s, 8.6%
|
050-gto_p60c231_1.real-time.png |
unsat, 139s, 13.3%
|
unsat, 106s, 45.4%
|
unsat, 62s, 17.1%
|
unsat, 56s, 11.6%
|
051-gto_p60c233.real-time.png |
unsat, 171s, 13.9%
|
unsat, 180s, 47.2%
|
unsat, 73s, 16.1%
|
unsat, 69s, 8.7%
|
052-gto_p60c234.real-time.png |
unsat, 360s, 14.6%
|
unsat, 373s, 49.4%
|
unsat, 116s, 16.3%
|
unsat, 123s, 10.2%
|
053-gto_p60c235.real-time.png |
unsat, 489s, 15.1%
|
unsat, 905s, 51.2%
|
unsat, 335s, 20.5%
|
unsat, 428s, 10.9%
|
054-gto_p60c238.real-time.png |
unsat, 857s, 15.7%
|
unsat, 953s, 51.4%
|
unsat, 309s, 19.3%
|
unsat, 301s, 13.9%
|
055-gto_p60c239.real-time.png |
unsat, 162s, 14.3%
|
unsat, 149s, 35.4%
|
unsat, 99s, 17.9%
|
unsat, 62s, 13.1%
|
056-gto_p60c241.real-time.png |
unsat, 180s, 14.5%
|
unsat, 110s, 45.1%
|
unsat, 57s, 14.3%
|
unsat, 53s, 10.8%
|
057-gto_p60c243.real-time.png |
unsat, 336s, 15.1%
|
unsat, 213s, 47.0%
|
unsat, 136s, 16.7%
|
unsat, 141s, 10.8%
|
058-gto_p60c295.real-time.png |
-, 1001s, 21.4%
|
-, 1001s, 33.3%
|
-, 1001s, 33.3%
|
-, 1001s, 14.4%
|
059-gto_p60c343.real-time.png |
-, 1001s, 25.1%
|
-, 1001s, 53.3%
|
-, 1001s, 31.3%
|
-, 1001s, 24.1%
|
060-huck.col.11.real-time.png |
unsat, 37s, 24.9%
|
unsat, 177s, 35.4%
|
unsat, 77s, 16.1%
|
unsat, 139s, 8.8%
|
061-le450_15a.col.15.real-time.png |
-, 1001s, 46.4%
|
-, 1001s, 31.1%
|
-, 1001s, 23.1%
|
-, 1001s, 12.8%
|
062-le450_15b.col.15.real-time.png |
-, 1001s, 41.6%
|
-, 1001s, 31.6%
|
-, 1001s, 21.6%
|
-, 1001s, 12.8%
|
063-le450_15c.col.15.real-time.png |
-, 1001s, 46.0%
|
-, 1001s, 27.8%
|
-, 1001s, 20.5%
|
-, 1001s, 11.9%
|
064-le450_25a.col.25.real-time.png |
-, 1001s, 54.6%
|
-, 1001s, 40.1%
|
-, 1001s, 27.9%
|
-, 1001s, 19.5%
|
065-le450_25b.col.25.real-time.png |
-, 1001s, 57.9%
|
-, 1001s, 31.6%
|
-, 1001s, 26.4%
|
-, 1001s, 20.7%
|
066-le450_25c.col.25.real-time.png |
-, 1001s, 62.8%
|
-, 1001s, 38.6%
|
-, 1001s, 26.4%
|
-, 1001s, 20.0%
|
067-queen12_12.col.12.real-time.png |
-, 1001s, 31.0%
|
-, 1001s, 51.8%
|
-, 1001s, 18.9%
|
-, 1001s, 23.8%
|
068-queen13_13.col.13.real-time.png |
-, 1001s, 37.1%
|
-, 1001s, 28.3%
|
-, 1001s, 20.4%
|
-, 1001s, 11.5%
|
069-queen14_14.col.14.real-time.png |
-, 1001s, 34.5%
|
-, 1001s, 29.7%
|
-, 1001s, 22.1%
|
-, 1001s, 12.6%
|
070-queen15_15.col.15.real-time.png |
-, 1001s, 41.0%
|
-, 1001s, 31.2%
|
-, 1001s, 23.0%
|
-, 1001s, 15.0%
|
071-queen8_12.col.12.real-time.png |
-, 1001s, 38.5%
|
-, 1001s, 52.6%
|
-, 1001s, 19.0%
|
-, 1001s, 23.7%
|
072-queen8_8.col.9.real-time.png |
-, 1001s, 25.9%
|
-, 1001s, 16.7%
|
-, 1001s, 10.7%
|
-, 1001s, 7.9%
|
073-school1.col.14.real-time.png |
-, 1001s, 50.0%
|
-, 1001s, 29.8%
|
-, 1001s, 18.2%
|
-, 1001s, 11.6%
|
074-school1_nsh.col.14.real-time.png |
-, 1001s, 45.9%
|
-, 1001s, 29.1%
|
-, 1001s, 18.2%
|
-, 1001s, 10.5%
|
075-ex009_10.real-time.png |
-, 1001s, 14.2%
|
-, 1001s, 26.4%
|
-, 1001s, 11.9%
|
-, 1001s, 6.6%
|
076-ex015_14.real-time.png |
-, 1001s, 11.9%
|
-, 1001s, 19.1%
|
-, 1001s, 10.1%
|
-, 1001s, 7.0%
|
077-ex025_19.real-time.png |
-, 1001s, 13.9%
|
-, 1001s, 21.6%
|
-, 1001s, 9.0%
|
-, 1001s, 5.7%
|
078-ex039_33.real-time.png |
-, 1001s, 13.6%
|
-, 1001s, 22.0%
|
-, 1001s, 9.3%
|
sat, 137s, 7.6%
|
079-ex045_7.real-time.png |
-, 1001s, 13.4%
|
-, 1001s, 23.3%
|
-, 1001s, 16.3%
|
-, 1001s, 8.2%
|
080-ex051_9.real-time.png |
-, 1001s, 20.9%
|
-, 1001s, 19.2%
|
-, 1001s, 9.9%
|
-, 1001s, 6.1%
|
081-ex065_24.real-time.png |
-, 1001s, 15.3%
|
-, 1001s, 23.1%
|
-, 1001s, 9.5%
|
-, 1001s, 8.4%
|
082-ex065_25.real-time.png |
-, 1001s, 14.9%
|
-, 1001s, 22.9%
|
sat, 629s, 10.2%
|
-, 1001s, 8.0%
|
083-ex067_10.real-time.png |
sat, 332s, 13.3%
|
-, 1001s, 20.2%
|
-, 1001s, 8.4%
|
sat, 107s, 6.2%
|
084-ex095_8.real-time.png |
-, 1001s, 13.1%
|
-, 1001s, 17.6%
|
-, 1001s, 9.6%
|
-, 1001s, 8.7%
|
085-ex145_10.real-time.png |
-, 1001s, 18.6%
|
-, 1001s, 21.7%
|
-, 1001s, 11.1%
|
-, 1001s, 7.1%
|
086-ex145_11.real-time.png |
-, 1001s, 18.0%
|
-, 1001s, 22.2%
|
-, 1001s, 11.3%
|
-, 1001s, 10.4%
|
087-ex157_10.real-time.png |
sat, 114s, 13.1%
|
-, 1001s, 21.6%
|
-, 1001s, 10.3%
|
-, 1001s, 7.9%
|
088-ex175_17.real-time.png |
-, 1001s, 13.3%
|
-, 1001s, 19.0%
|
-, 1001s, 9.5%
|
-, 1001s, 9.5%
|
089-ex175_18.real-time.png |
sat, 989s, 14.2%
|
-, 1001s, 20.2%
|
-, 1001s, 9.8%
|
-, 1001s, 7.1%
|
090-ex175_20.real-time.png |
sat, 279s, 22.1%
|
-, 1001s, 25.3%
|
sat, 513s, 15.8%
|
sat, 363s, 8.6%
|
091-ex177_12.real-time.png |
-, 1001s, 11.6%
|
-, 1001s, 18.6%
|
-, 1001s, 9.4%
|
-, 1001s, 8.3%
|
092-ex177_13.real-time.png |
-, 1001s, 12.6%
|
-, 1001s, 19.9%
|
-, 1001s, 8.6%
|
-, 1001s, 7.9%
|
093-ex179_11.real-time.png |
sat, 234s, 13.7%
|
-, 1001s, 23.5%
|
-, 1001s, 10.0%
|
-, 1001s, 7.2%
|
094-ex187_10.real-time.png |
sat, 673s, 15.6%
|
-, 1001s, 20.6%
|
sat, 488s, 10.0%
|
sat, 768s, 7.7%
|
095-ecarev-110-1031-23-40-1.real-time.png |
sat, 298s, 28.6%
|
sat, 283s, 33.2%
|
sat, 256s, 17.3%
|
sat, 231s, 13.7%
|
096-ecarev-110-1031-23-40-2.real-time.png |
sat, 227s, 28.9%
|
sat, 211s, 33.1%
|
sat, 165s, 19.3%
|
sat, 167s, 20.0%
|
097-ecarev-110-1031-23-40-3.real-time.png |
unsat, 13s, 26.7%
|
unsat, 90s, 33.6%
|
unsat, 5s, 23.1%
|
unsat, 113s, 11.9%
|
098-ecarev-110-1031-23-40-5.real-time.png |
sat, 446s, 30.2%
|
sat, 343s, 35.8%
|
sat, 242s, 15.5%
|
sat, 222s, 15.1%
|
099-ecarev-110-1031-23-40-6.real-time.png |
-, 1001s, 31.9%
|
-, 1001s, 33.4%
|
-, 1001s, 17.0%
|
sat, 832s, 24.4%
|
100-ecarev-110-1031-23-40-7.real-time.png |
sat, 204s, 29.4%
|
sat, 238s, 34.8%
|
sat, 180s, 14.7%
|
sat, 186s, 18.6%
|
101-ecarev-110-1031-23-40-8.real-time.png |
-, 1001s, 30.3%
|
sat, 851s, 37.2%
|
sat, 979s, 23.1%
|
sat, 690s, 22.2%
|
102-ecarev-110-4099-22-30-2.real-time.png |
sat, 158s, 37.0%
|
sat, 470s, 53.1%
|
sat, 292s, 27.1%
|
sat, 291s, 24.2%
|
103-ecarev-110-4099-22-30-4.real-time.png |
sat, 248s, 37.9%
|
sat, 574s, 53.1%
|
sat, 372s, 25.8%
|
sat, 392s, 25.0%
|
104-ecarev-110-4099-22-30-5.real-time.png |
sat, 169s, 36.4%
|
sat, 647s, 53.2%
|
sat, 356s, 27.3%
|
sat, 352s, 22.7%
|
105-ecarev-110-4099-22-30-7.real-time.png |
sat, 155s, 37.6%
|
sat, 464s, 53.7%
|
sat, 301s, 26.8%
|
sat, 264s, 21.9%
|
106-CNP-5-0.real-time.png |
sat, 831s, 17.0%
|
-, 1001s, 17.6%
|
-, 1001s, 12.6%
|
-, 1001s, 7.7%
|
107-CNP-5-100.real-time.png |
sat, 838s, 25.4%
|
-, 1001s, 17.0%
|
sat, 206s, 9.2%
|
-, 1001s, 6.4%
|
108-CNP-5-1000.real-time.png |
sat, 546s, 22.4%
|
sat, 105s, 15.1%
|
sat, 801s, 9.8%
|
sat, 694s, 6.6%
|
109-CNP-5-1100.real-time.png |
sat, 568s, 23.7%
|
-, 1001s, 17.8%
|
-, 1001s, 12.4%
|
sat, 373s, 8.4%
|
110-CNP-5-1200.real-time.png |
sat, 271s, 24.4%
|
sat, 718s, 18.7%
|
sat, 145s, 10.0%
|
sat, 68s, 7.2%
|
111-CNP-5-1300.real-time.png |
sat, 266s, 24.7%
|
sat, 76s, 13.9%
|
sat, 185s, 11.4%
|
sat, 463s, 5.8%
|
112-CNP-5-1400.real-time.png |
sat, 96s, 21.8%
|
sat, 188s, 14.5%
|
sat, 48s, 11.2%
|
sat, 235s, 8.5%
|
113-CNP-5-1500.real-time.png |
sat, 153s, 20.3%
|
sat, 182s, 17.1%
|
sat, 8s, 10.5%
|
sat, 381s, 6.6%
|
114-CNP-5-1600.real-time.png |
sat, 170s, 21.1%
|
sat, 116s, 16.3%
|
sat, 50s, 10.5%
|
sat, 104s, 6.7%
|
115-CNP-5-1700.real-time.png |
sat, 5s, 17.1%
|
sat, 270s, 17.7%
|
sat, 31s, 11.3%
|
sat, 41s, 7.0%
|
116-CNP-5-1800.real-time.png |
sat, 44s, 22.4%
|
sat, 24s, 14.1%
|
sat, 11s, 10.9%
|
sat, 102s, 7.9%
|
117-CNP-5-1900.real-time.png |
sat, 8s, 14.3%
|
sat, 133s, 16.6%
|
sat, 307s, 11.6%
|
sat, 24s, 6.9%
|
118-CNP-5-200.real-time.png |
-, 1001s, 23.9%
|
-, 1001s, 16.8%
|
-, 1001s, 10.1%
|
-, 1001s, 6.6%
|
119-CNP-5-300.real-time.png |
-, 1001s, 26.0%
|
sat, 908s, 17.4%
|
-, 1001s, 10.6%
|
-, 1001s, 8.0%
|
120-CNP-5-400.real-time.png |
sat, 498s, 21.7%
|
-, 1001s, 18.2%
|
-, 1001s, 10.7%
|
-, 1001s, 6.4%
|
121-CNP-5-500.real-time.png |
sat, 474s, 21.6%
|
-, 1001s, 19.6%
|
sat, 922s, 11.7%
|
sat, 640s, 6.4%
|
122-CNP-5-600.real-time.png |
sat, 615s, 20.2%
|
sat, 397s, 17.3%
|
-, 1001s, 10.4%
|
-, 1001s, 7.3%
|
123-CNP-5-700.real-time.png |
-, 1001s, 24.0%
|
-, 1001s, 19.0%
|
sat, 190s, 9.7%
|
sat, 156s, 7.9%
|
124-CNP-5-800.real-time.png |
sat, 213s, 14.5%
|
-, 1001s, 18.7%
|
sat, 235s, 9.8%
|
sat, 552s, 6.9%
|
125-CNP-5-900.real-time.png |
sat, 633s, 20.4%
|
-, 1001s, 17.2%
|
-, 1001s, 12.2%
|
sat, 246s, 9.5%
|
126-satcoin-genesis-SAT-10.real-time.png |
-, 1001s, 34.8%
|
sat, 1s, 53.9%
|
sat, 1s, 10.4%
|
sat, 1s, 14.0%
|
127-satcoin-genesis-SAT-1024.real-time.png |
-, 1001s, 38.8%
|
sat, 46s, 58.5%
|
sat, 35s, 9.1%
|
sat, 39s, 11.1%
|
128-satcoin-genesis-SAT-128.real-time.png |
-, 1001s, 38.2%
|
sat, 2s, 57.0%
|
sat, 3s, 12.0%
|
sat, 3s, 12.9%
|
129-satcoin-genesis-SAT-16.real-time.png |
-, 1001s, 38.1%
|
sat, 1s, 49.8%
|
sat, 1s, 14.2%
|
sat, 1s, 13.9%
|
130-satcoin-genesis-SAT-2048.real-time.png |
-, 1001s, 39.0%
|
sat, 44s, 57.6%
|
sat, 65s, 9.6%
|
sat, 45s, 10.0%
|
131-satcoin-genesis-SAT-256.real-time.png |
sat, 14s, 72.1%
|
sat, 12s, 74.1%
|
-, 1001s, 14.5%
|
-, 1001s, 9.7%
|
132-satcoin-genesis-SAT-3.real-time.png |
sat, 1s, 29.8%
|
sat, 1s, 32.7%
|
sat, 1s, 14.4%
|
sat, 1s, 17.1%
|
133-satcoin-genesis-SAT-32.real-time.png |
-, 1001s, 38.1%
|
sat, 2s, 70.5%
|
sat, 2s, 12.2%
|
sat, 2s, 13.5%
|
134-satcoin-genesis-SAT-4.real-time.png |
sat, 1s, 34.9%
|
sat, 1s, 36.3%
|
sat, 1s, 16.9%
|
sat, 1s, 15.7%
|
135-satcoin-genesis-SAT-4096.real-time.png |
-, 1001s, 38.7%
|
sat, 200s, 68.8%
|
-, 1001s, 15.8%
|
sat, 150s, 11.4%
|
136-satcoin-genesis-SAT-5.real-time.png |
sat, 1s, 45.4%
|
sat, 1s, 37.7%
|
sat, 1s, 14.6%
|
sat, 1s, 11.8%
|
137-satcoin-genesis-SAT-512.real-time.png |
-, 1001s, 39.2%
|
sat, 23s, 62.5%
|
sat, 27s, 12.1%
|
sat, 35s, 11.3%
|
138-satcoin-genesis-SAT-64.real-time.png |
-, 1001s, 38.5%
|
sat, 3s, 54.7%
|
sat, 2s, 11.6%
|
sat, 2s, 10.8%
|
139-satcoin-genesis-SAT-7.real-time.png |
-, 1001s, 35.4%
|
sat, 1s, 48.6%
|
sat, 1s, 12.2%
|
sat, 1s, 15.1%
|
140-satcoin-genesis-SAT-8.real-time.png |
-, 1001s, 37.9%
|
sat, 1s, 42.4%
|
sat, 1s, 11.7%
|
sat, 1s, 15.6%
|
141-satcoin-genesis-SAT-8192.real-time.png |
-, 1001s, 39.4%
|
sat, 395s, 72.5%
|
sat, 282s, 12.0%
|
sat, 507s, 11.1%
|
142-satcoin-genesis-SAT-9.real-time.png |
-, 1001s, 38.3%
|
sat, 1s, 52.5%
|
sat, 1s, 13.0%
|
sat, 1s, 8.2%
|
143-a_rphp035_05.real-time.png |
-, 1001s, 21.8%
|
-, 1001s, 39.7%
|
unsat, 800s, 18.8%
|
unsat, 719s, 10.9%
|
144-a_rphp045_05.real-time.png |
-, 1001s, 24.2%
|
-, 1001s, 39.1%
|
-, 1001s, 27.5%
|
-, 1001s, 16.9%
|
145-a_rphp055_04.real-time.png |
unsat, 86s, 20.5%
|
unsat, 101s, 39.4%
|
unsat, 64s, 20.2%
|
unsat, 59s, 11.2%
|
146-a_rphp056_05.real-time.png |
-, 1001s, 26.0%
|
-, 1001s, 40.2%
|
-, 1001s, 31.5%
|
-, 1001s, 19.3%
|
147-a_rphp065_04.real-time.png |
unsat, 261s, 22.9%
|
unsat, 240s, 36.9%
|
unsat, 200s, 23.1%
|
unsat, 154s, 12.4%
|
148-a_rphp085_04.real-time.png |
-, 1001s, 26.4%
|
-, 1001s, 39.3%
|
-, 1001s, 25.6%
|
unsat, 836s, 14.9%
|
149-a_rphp098_04.real-time.png |
-, 1001s, 26.9%
|
-, 1001s, 37.0%
|
-, 1001s, 29.2%
|
-, 1001s, 18.3%
|
150-ae_rphp035_05.real-time.png |
-, 1001s, 21.9%
|
unsat, 512s, 28.0%
|
unsat, 435s, 17.4%
|
unsat, 456s, 10.5%
|
151-ae_rphp045_05.real-time.png |
-, 1001s, 24.2%
|
-, 1001s, 29.9%
|
-, 1001s, 24.0%
|
-, 1001s, 10.5%
|
152-ae_rphp055_04.real-time.png |
unsat, 139s, 21.1%
|
unsat, 65s, 33.3%
|
unsat, 70s, 26.0%
|
unsat, 64s, 15.0%
|
153-ae_rphp056_05.real-time.png |
-, 1001s, 24.3%
|
-, 1001s, 33.2%
|
-, 1001s, 23.8%
|
-, 1001s, 13.8%
|
154-ae_rphp062_05.real-time.png |
-, 1001s, 25.1%
|
-, 1001s, 35.6%
|
-, 1001s, 28.0%
|
-, 1001s, 18.1%
|
155-ae_rphp075_04.real-time.png |
-, 1001s, 24.5%
|
unsat, 550s, 37.0%
|
unsat, 641s, 31.5%
|
unsat, 527s, 19.8%
|
156-ae_rphp095_04.real-time.png |
-, 1001s, 27.1%
|
-, 1001s, 37.3%
|
-, 1001s, 34.5%
|
-, 1001s, 25.2%
|
157-e_rphp035_05.real-time.png |
-, 1001s, 21.4%
|
unsat, 456s, 27.9%
|
unsat, 427s, 19.1%
|
unsat, 400s, 12.4%
|
158-e_rphp055_04.real-time.png |
unsat, 77s, 21.5%
|
unsat, 59s, 34.7%
|
unsat, 69s, 26.2%
|
unsat, 49s, 14.7%
|
159-e_rphp056_05.real-time.png |
-, 1001s, 26.4%
|
-, 1001s, 33.9%
|
-, 1001s, 24.6%
|
-, 1001s, 12.9%
|
160-e_rphp065_04.real-time.png |
unsat, 206s, 23.8%
|
unsat, 200s, 36.5%
|
unsat, 188s, 25.9%
|
unsat, 152s, 18.6%
|
161-e_rphp065_05.real-time.png |
-, 1001s, 27.7%
|
-, 1001s, 36.1%
|
-, 1001s, 27.3%
|
-, 1001s, 14.0%
|
162-e_rphp096_04.real-time.png |
-, 1001s, 28.3%
|
-, 1001s, 37.0%
|
-, 1001s, 33.3%
|
-, 1001s, 22.0%
|
163-TimetableCNFEncoding_10_UNKNOWN.real-time.png |
-, 1001s, 19.8%
|
-, 1001s, 42.6%
|
-, 1001s, 31.3%
|
-, 1001s, 22.7%
|
164-TimetableCNFEncoding_16_UNKNOWN.real-time.png |
-, 1001s, 20.9%
|
-, 1001s, 46.9%
|
-, 1001s, 40.3%
|
-, 1001s, 14.5%
|
165-TimetableCNFEncoding_17_UNKNOWN.real-time.png |
-, 1001s, 28.3%
|
-, 1001s, 45.6%
|
-, 1001s, 19.0%
|
-, 1001s, 10.2%
|
166-TimetableCNFEncoding_1_UNKNOWN.real-time.png |
-, 1001s, 21.8%
|
-, 1001s, 25.9%
|
-, 1001s, 9.1%
|
-, 1001s, 8.2%
|
167-TimetableCNFEncoding_20_UNKNOWN.real-time.png |
sat, 218s, 14.4%
|
-, 1001s, 27.5%
|
sat, 92s, 9.4%
|
sat, 56s, 9.5%
|
168-TimetableCNFEncoding_2_UNKNOWN.real-time.png |
-, 1001s, 16.9%
|
-, 1001s, 45.8%
|
-, 1001s, 50.6%
|
-, 1001s, 20.0%
|
169-TimetableCNFEncoding_3_UNKNOWN.real-time.png |
-, 1001s, 27.6%
|
-, 1001s, 41.7%
|
-, 1001s, 19.6%
|
-, 1001s, 9.6%
|
170-TimetableCNFEncoding_4_UNKNOWN.real-time.png |
-, 1001s, 18.2%
|
-, 1001s, 46.5%
|
-, 1001s, 50.5%
|
-, 1001s, 20.7%
|
171-TimetableCNFEncoding_5_UNKNOWN.real-time.png |
-, 1001s, 19.1%
|
-, 1001s, 45.7%
|
-, 1001s, 49.6%
|
-, 1001s, 20.1%
|
172-TimetableCNFEncoding_6_UNKNOWN.real-time.png |
-, 1001s, 13.0%
|
-, 1001s, 26.3%
|
-, 1001s, 28.0%
|
-, 1001s, 12.5%
|
173-TimetableCNFEncoding_8_UNKNOWN.real-time.png |
-, 1001s, 12.3%
|
-, 1001s, 28.9%
|
-, 1001s, 22.0%
|
-, 1001s, 14.2%
|
174-TimetableCNFEncoding_9_UNKNOWN.real-time.png |
-, 1001s, 19.9%
|
-, 1001s, 34.5%
|
-, 1001s, 30.3%
|
-, 1001s, 25.4%
|
175-assoc2.c.real-time.png |
-, 1001s, 14.9%
|
-, 1001s, 23.4%
|
-, 1001s, 14.2%
|
-, 1001s, 9.8%
|
176-assoc_mult_err_3.c.real-time.png |
-, 1001s, 18.1%
|
unsat, 80s, 15.0%
|
unsat, 66s, 7.1%
|
unsat, 66s, 9.3%
|
177-commutativity.c.real-time.png |
-, 1001s, 12.8%
|
-, 1001s, 23.8%
|
-, 1001s, 12.2%
|
-, 1001s, 15.7%
|
178-commutativity3.c.real-time.png |
-, 1001s, 29.7%
|
-, 1001s, 30.7%
|
-, 1001s, 15.3%
|
-, 1001s, 17.7%
|
179-dist10.c.real-time.png |
unsat, 118s, 11.3%
|
unsat, 223s, 18.1%
|
unsat, 207s, 10.3%
|
unsat, 197s, 8.9%
|
180-dist4.c.real-time.png |
-, 1001s, 13.9%
|
unsat, 191s, 15.7%
|
unsat, 194s, 10.4%
|
unsat, 155s, 6.5%
|
181-dist5.c.real-time.png |
unsat, 125s, 10.7%
|
unsat, 224s, 17.2%
|
unsat, 189s, 10.1%
|
unsat, 225s, 8.7%
|
182-dist6.c.real-time.png |
unsat, 132s, 9.8%
|
unsat, 184s, 18.4%
|
unsat, 200s, 11.3%
|
unsat, 188s, 6.2%
|
183-dist7.c.real-time.png |
unsat, 494s, 14.4%
|
unsat, 224s, 18.4%
|
unsat, 195s, 9.5%
|
unsat, 156s, 6.1%
|
184-dist8.c.real-time.png |
unsat, 665s, 16.9%
|
unsat, 197s, 17.5%
|
unsat, 184s, 9.2%
|
unsat, 221s, 8.2%
|
185-dist9.c.real-time.png |
unsat, 147s, 10.8%
|
unsat, 239s, 16.9%
|
unsat, 211s, 11.4%
|
unsat, 207s, 5.6%
|
186-quadratic_loose_error.c.real-time.png |
unsat, 387s, 32.3%
|
unsat, 349s, 40.7%
|
unsat, 359s, 13.3%
|
unsat, 565s, 9.0%
|
187-quadratic_tight_error.c.real-time.png |
unsat, 922s, 31.4%
|
unsat, 439s, 41.5%
|
-, 1001s, 11.7%
|
unsat, 253s, 8.7%
|
188-sqrt_ineq_2.c.real-time.png |
sat, 933s, 35.8%
|
sat, 102s, 36.5%
|
sat, 104s, 11.0%
|
sat, 197s, 10.3%
|
189-sqrt_ineq_3.c.real-time.png |
-, 1001s, 32.4%
|
sat, 748s, 33.6%
|
-, 1001s, 11.9%
|
sat, 2s, 7.2%
|
190-Problem11_label29_false-unreach-call.c.real-time.png |
sat, 939s, 31.8%
|
-, 1001s, 47.6%
|
-, 1001s, 19.4%
|
-, 1001s, 25.9%
|
191-Problem11_label51_false-unreach-call.c.real-time.png |
-, 1001s, 36.2%
|
-, 1001s, 46.5%
|
-, 1001s, 15.0%
|
-, 1001s, 18.8%
|
192-Problem14_label14_false-unreach-call.c.real-time.png |
sat, 95s, 31.9%
|
sat, 243s, 46.0%
|
sat, 68s, 15.8%
|
sat, 160s, 16.3%
|
193-Problem14_label19_true-unreach-call.c.real-time.png |
unsat, 71s, 31.4%
|
unsat, 138s, 52.0%
|
unsat, 118s, 16.5%
|
unsat, 56s, 15.2%
|
194-Problem14_label20_true-unreach-call.c.real-time.png |
unsat, 7s, 22.3%
|
unsat, 6s, 49.8%
|
unsat, 7s, 31.5%
|
unsat, 7s, 29.4%
|
195-Problem14_label48_true-unreach-call.c.real-time.png |
unsat, 107s, 19.8%
|
unsat, 160s, 39.9%
|
unsat, 109s, 15.2%
|
unsat, 124s, 17.4%
|
196-Problem14_label55_true-unreach-call.c.real-time.png |
unsat, 27s, 24.5%
|
unsat, 36s, 41.5%
|
unsat, 24s, 20.8%
|
unsat, 23s, 22.7%
|
197-Problem14_label57_false-unreach-call.c.real-time.png |
sat, 89s, 25.6%
|
sat, 153s, 47.7%
|
sat, 66s, 14.2%
|
sat, 88s, 16.3%
|
198-avg_true-unreach-call.i.real-time.png |
unsat, 826s, 28.3%
|
unsat, 204s, 35.3%
|
unsat, 195s, 17.7%
|
unsat, 188s, 11.3%
|
199-filter1_true-unreach-call.c.real-time.png |
unsat, 196s, 39.0%
|
unsat, 293s, 54.9%
|
unsat, 203s, 17.4%
|
unsat, 175s, 15.5%
|
200-filter_iir_true-unreach-call.c.real-time.png |
unsat, 284s, 28.8%
|
unsat, 334s, 41.8%
|
unsat, 230s, 10.1%
|
unsat, 283s, 10.8%
|
201-newton_3_4_true-unreach-call.i.real-time.png |
unsat, 419s, 43.1%
|
unsat, 111s, 46.8%
|
unsat, 67s, 13.0%
|
unsat, 63s, 11.1%
|
202-newton_3_6_false-unreach-call.i.real-time.png |
sat, 173s, 43.6%
|
sat, 85s, 49.9%
|
sat, 84s, 12.9%
|
sat, 74s, 10.0%
|
203-pals_floodmax.5_overflow_false-unreach-call.ufo.UNBOUNDED.pals.c.real-time.png |
-, 1001s, 13.9%
|
-, 1001s, 24.1%
|
-, 1001s, 17.8%
|
-, 1001s, 7.9%
|
204-pals_lcr-var-start-time.5_true-unreach-call.ufo.UNBOUNDED.pals.c.real-time.png |
unsat, 912s, 8.8%
|
unsat, 70s, 18.3%
|
unsat, 68s, 6.4%
|
unsat, 65s, 8.4%
|
205-pals_lcr-var-start-time.6_true-unreach-call.ufo.UNBOUNDED.pals.c.real-time.png |
-, 1001s, 8.8%
|
unsat, 246s, 13.9%
|
unsat, 224s, 6.6%
|
unsat, 246s, 10.6%
|
206-pals_lcr.8_overflow_false-unreach-call.ufo.UNBOUNDED.pals.c.real-time.png |
-, 1001s, 10.1%
|
unsat, 231s, 16.5%
|
unsat, 200s, 6.1%
|
unsat, 170s, 5.0%
|
207-sqrt_Householder_pseudoconstant_true-unreach-call.c.real-time.png |
-, 1001s, 65.2%
|
-, 1001s, 58.8%
|
-, 1001s, 29.1%
|
-, 1001s, 31.1%
|
208-terminator_03_true-unreach-call_true-termination.i.real-time.png |
-, 1001s, 50.3%
|
unsat, 947s, 54.0%
|
unsat, 513s, 17.8%
|
unsat, 489s, 10.4%
|
209-10-3-13.real-time.png |
-, 1001s, 21.9%
|
-, 1001s, 26.7%
|
-, 1001s, 27.0%
|
-, 1001s, 12.8%
|
210-10-4-10.real-time.png |
-, 1001s, 13.6%
|
-, 1001s, 28.0%
|
-, 1001s, 15.3%
|
-, 1001s, 10.6%
|
211-6-3-8.real-time.png |
sat, 98s, 9.6%
|
sat, 748s, 12.3%
|
sat, 514s, 9.0%
|
-, 1001s, 4.5%
|
212-6-4-6.real-time.png |
-, 1001s, 16.7%
|
-, 1001s, 20.1%
|
-, 1001s, 10.2%
|
-, 1001s, 8.1%
|
213-6-4-7.real-time.png |
-, 1001s, 15.1%
|
-, 1001s, 22.0%
|
-, 1001s, 11.4%
|
-, 1001s, 8.0%
|
214-6-5-6.real-time.png |
-, 1001s, 11.5%
|
-, 1001s, 17.8%
|
-, 1001s, 11.0%
|
-, 1001s, 7.9%
|
215-7-4-7.real-time.png |
-, 1001s, 15.0%
|
-, 1001s, 22.1%
|
-, 1001s, 15.2%
|
-, 1001s, 9.8%
|
216-7-5-6.real-time.png |
-, 1001s, 21.5%
|
-, 1001s, 30.3%
|
-, 1001s, 16.1%
|
-, 1001s, 12.3%
|
217-8-4-10.real-time.png |
-, 1001s, 17.6%
|
-, 1001s, 29.3%
|
-, 1001s, 12.8%
|
-, 1001s, 8.9%
|
218-8-4-8.real-time.png |
-, 1001s, 13.5%
|
-, 1001s, 25.7%
|
-, 1001s, 14.5%
|
-, 1001s, 9.1%
|
219-8-4-9.real-time.png |
-, 1001s, 16.9%
|
-, 1001s, 25.3%
|
-, 1001s, 18.3%
|
-, 1001s, 10.3%
|
220-8-5-6.real-time.png |
-, 1001s, 15.7%
|
-, 1001s, 30.0%
|
-, 1001s, 14.4%
|
-, 1001s, 12.0%
|
221-9-4-10.real-time.png |
-, 1001s, 16.7%
|
-, 1001s, 25.6%
|
-, 1001s, 17.5%
|
-, 1001s, 10.0%
|
222-9-4-9.real-time.png |
-, 1001s, 14.3%
|
-, 1001s, 27.8%
|
-, 1001s, 15.0%
|
-, 1001s, 10.6%
|
223-course0.12_2018_3_1.real-time.png |
-, 1001s, 17.3%
|
-, 1001s, 29.7%
|
-, 1001s, 7.7%
|
sat, 618s, 6.7%
|
224-course0.12_2018_3_3.real-time.png |
-, 1001s, 8.6%
|
-, 1001s, 16.6%
|
-, 1001s, 10.3%
|
-, 1001s, 6.8%
|
225-course0.12_2018_3_5.real-time.png |
-, 1001s, 30.2%
|
-, 1001s, 39.8%
|
-, 1001s, 9.7%
|
-, 1001s, 6.8%
|
226-course0.16_2018_3_5.real-time.png |
-, 1001s, 28.5%
|
-, 1001s, 39.2%
|
-, 1001s, 9.0%
|
-, 1001s, 8.1%
|
227-course0.2_2018_3.real-time.png |
-, 1001s, 32.3%
|
-, 1001s, 51.3%
|
-, 1001s, 8.1%
|
-, 1001s, 10.0%
|
228-course0.2_2018_3_5.real-time.png |
sat, 121s, 30.3%
|
sat, 343s, 45.1%
|
sat, 421s, 8.3%
|
sat, 205s, 12.3%
|
229-course_flat_0.12_2018_3.real-time.png |
-, 1001s, 8.9%
|
-, 1001s, 21.3%
|
-, 1001s, 9.6%
|
-, 1001s, 10.4%
|
230-course_flat_0.12_2018_3_1.real-time.png |
-, 1001s, 9.8%
|
sat, 577s, 19.1%
|
sat, 145s, 9.0%
|
sat, 304s, 5.8%
|
231-course_flat_0.12_2018_3_3.real-time.png |
-, 1001s, 10.7%
|
-, 1001s, 23.9%
|
-, 1001s, 8.2%
|
-, 1001s, 7.8%
|
232-course_flat_0.12_2018_3_5.real-time.png |
-, 1001s, 11.3%
|
-, 1001s, 27.1%
|
-, 1001s, 8.7%
|
-, 1001s, 8.6%
|
233-course_flat_0.16_2018_3.real-time.png |
-, 1001s, 10.0%
|
-, 1001s, 22.3%
|
-, 1001s, 12.3%
|
-, 1001s, 9.2%
|
234-course_flat_0.2_2018_3.real-time.png |
sat, 284s, 9.4%
|
sat, 714s, 21.0%
|
sat, 346s, 8.6%
|
sat, 189s, 9.5%
|
235-courses0.12_2017_9.real-time.png |
-, 1001s, 11.8%
|
-, 1001s, 20.4%
|
-, 1001s, 8.7%
|
-, 1001s, 6.4%
|
236-courses0.2_2017_9.real-time.png |
-, 1001s, 33.3%
|
-, 1001s, 49.1%
|
-, 1001s, 8.1%
|
-, 1001s, 8.6%
|
237-courses_flat_0.12_2017_9.real-time.png |
-, 1001s, 11.6%
|
-, 1001s, 22.9%
|
-, 1001s, 7.3%
|
-, 1001s, 8.0%
|
238-courses_flat_0.16_2017_9.real-time.png |
-, 1001s, 12.3%
|
-, 1001s, 22.8%
|
-, 1001s, 7.1%
|
-, 1001s, 8.2%
|
239-exam0.04_2018_3.real-time.png |
-, 1001s, 20.5%
|
sat, 461s, 30.3%
|
sat, 380s, 10.2%
|
-, 1001s, 7.9%
|
240-exam_flat_0.04_2018_3.real-time.png |
-, 1001s, 17.7%
|
-, 1001s, 25.8%
|
-, 1001s, 15.9%
|
-, 1001s, 8.3%
|
241-exams0.04_2017_9.real-time.png |
-, 1001s, 16.5%
|
-, 1001s, 19.5%
|
-, 1001s, 8.9%
|
sat, 48s, 8.2%
|
242-exams_flat_0.04_2017_9.real-time.png |
-, 1001s, 17.3%
|
-, 1001s, 28.8%
|
-, 1001s, 16.4%
|
-, 1001s, 8.7%
|
243-Cake_8_16.real-time.png |
-, 1001s, 31.8%
|
-, 1001s, 27.8%
|
-, 1001s, 17.0%
|
-, 1001s, 12.3%
|
244-Cake_9_19.real-time.png |
-, 1001s, 45.8%
|
-, 1001s, 26.3%
|
-, 1001s, 13.5%
|
-, 1001s, 10.0%
|
245-Cake_9_20.real-time.png |
-, 1001s, 48.0%
|
-, 1001s, 24.0%
|
-, 1001s, 13.0%
|
-, 1001s, 12.0%
|
246-mchess_15.real-time.png |
-, 1001s, 15.3%
|
unsat, 416s, 21.2%
|
unsat, 174s, 15.0%
|
unsat, 119s, 7.1%
|
247-mchess_16.real-time.png |
-, 1001s, 16.0%
|
-, 1001s, 24.1%
|
-, 1001s, 17.0%
|
-, 1001s, 6.5%
|
248-mchess_17.real-time.png |
-, 1001s, 16.8%
|
-, 1001s, 24.6%
|
-, 1001s, 16.8%
|
-, 1001s, 6.6%
|
249-mchess_18.real-time.png |
-, 1001s, 17.6%
|
-, 1001s, 25.3%
|
-, 1001s, 17.5%
|
-, 1001s, 6.8%
|
250-mchess_19.real-time.png |
-, 1001s, 18.5%
|
-, 1001s, 27.7%
|
-, 1001s, 18.8%
|
-, 1001s, 10.5%
|
251-mchess_20.real-time.png |
-, 1001s, 19.2%
|
-, 1001s, 26.0%
|
-, 1001s, 18.2%
|
-, 1001s, 12.3%
|
252-cms-scheel-md4-families-r24-c4-p4-9-13-18.real-time.png |
-, 1001s, 25.1%
|
-, 1001s, 38.6%
|
-, 1001s, 28.5%
|
-, 1001s, 25.1%
|
253-cms-scheel-md4-families-r24-c4-p6-13-17-19.real-time.png |
sat, 316s, 20.9%
|
sat, 635s, 35.7%
|
sat, 795s, 17.0%
|
-, 1001s, 10.6%
|
254-cms-scheel-md4-families-r24-c5-p0-5-11-13-18.real-time.png |
-, 1001s, 25.6%
|
-, 1001s, 41.9%
|
-, 1001s, 22.6%
|
-, 1001s, 14.7%
|
255-cms-scheel-md4-families-r24-c5-p0-7-10-15-19.real-time.png |
sat, 28s, 21.6%
|
sat, 55s, 35.0%
|
sat, 33s, 15.3%
|
sat, 37s, 10.5%
|
256-cms-scheel-md4-families-r24-c5-p1-5-10-12-18.real-time.png |
unsat, 1s, 31.5%
|
-, 1001s, 37.8%
|
-, 1001s, 24.0%
|
-, 1001s, 21.8%
|
257-cms-scheel-md4-families-r24-c5-p1-8-13-18-19.real-time.png |
-, 1001s, 24.8%
|
-, 1001s, 40.2%
|
-, 1001s, 20.8%
|
-, 1001s, 14.9%
|
258-cms-scheel-md4-families-r24-c5-p1-8-9-16-19.real-time.png |
unsat, 1s, 29.6%
|
unsat, 242s, 36.5%
|
-, 1001s, 19.1%
|
-, 1001s, 13.1%
|
259-cms-scheel-md4-families-r24-c5-p5-13-16-17-19.real-time.png |
-, 1001s, 24.5%
|
-, 1001s, 40.3%
|
-, 1001s, 15.4%
|
-, 1001s, 9.3%
|
260-cms-scheel-md4-families-r24-c6-p0-5-10-11-17-18.real-time.png |
unsat, 1s, 28.4%
|
-, 1001s, 37.5%
|
unsat, 988s, 15.6%
|
unsat, 368s, 13.2%
|
261-cms-scheel-md4-families-r24-c6-p1-9-13-16-18-19.real-time.png |
-, 1001s, 22.1%
|
-, 1001s, 37.8%
|
-, 1001s, 14.9%
|
-, 1001s, 14.0%
|
262-cms-scheel-md4-families-r24-c6-p2-4-9-16-17-19.real-time.png |
unsat, 1s, 31.8%
|
unsat, 2s, 39.3%
|
unsat, 36s, 17.3%
|
unsat, 114s, 12.6%
|
263-cms-scheel-md4-families-r24-c8-p2-3-4-5-7-12-16-19.real-time.png |
sat, 23s, 20.8%
|
sat, 18s, 35.5%
|
sat, 26s, 18.4%
|
sat, 62s, 12.8%
|
264-cms-scheel-md5-families-r24-c11-p1-4-6-9-10-11-13-15-17-18-19.real-time.png |
sat, 73s, 21.7%
|
sat, 212s, 28.9%
|
sat, 241s, 11.4%
|
sat, 135s, 7.6%
|
265-cms-scheel-md5-families-r24-c4-p1-3-4-16.real-time.png |
sat, 465s, 21.9%
|
sat, 290s, 35.9%
|
sat, 183s, 14.7%
|
sat, 387s, 12.5%
|
266-cms-scheel-md5-families-r24-c5-p2-7-8-15-19.real-time.png |
-, 1001s, 22.3%
|
-, 1001s, 40.1%
|
-, 1001s, 17.9%
|
-, 1001s, 11.7%
|
267-cms-scheel-md5-families-r24-c5-p6-11-15-16-19.real-time.png |
unsat, 5s, 22.2%
|
unsat, 174s, 35.1%
|
unsat, 676s, 17.5%
|
unsat, 434s, 12.2%
|
268-cms-scheel-md5-families-r24-c6-p1-4-6-13-14-18.real-time.png |
-, 1001s, 22.3%
|
-, 1001s, 36.4%
|
-, 1001s, 19.3%
|
-, 1001s, 11.1%
|
269-cms-scheel-md5-families-r24-c7-p1-3-6-10-11-14-15.real-time.png |
unsat, 366s, 21.1%
|
unsat, 495s, 34.7%
|
unsat, 695s, 16.4%
|
-, 1001s, 12.5%
|
270-cms-scheel-md5-families-r24-c7-p1-5-6-12-16-18-19.real-time.png |
-, 1001s, 21.7%
|
-, 1001s, 36.6%
|
-, 1001s, 17.3%
|
-, 1001s, 11.1%
|
271-cms-scheel-md5-families-r24-c8-p0-3-5-6-14-16-18-19.real-time.png |
-, 1001s, 21.0%
|
-, 1001s, 32.8%
|
-, 1001s, 14.5%
|
-, 1001s, 15.2%
|
272-Nb11T118.real-time.png |
sat, 3s, 16.1%
|
-, 1001s, 36.0%
|
-, 1001s, 33.0%
|
-, 1001s, 8.9%
|
273-Nb13T165.real-time.png |
-, 1001s, 21.4%
|
-, 1001s, 34.3%
|
-, 1001s, 11.5%
|
-, 1001s, 9.4%
|
274-Nb13T166.real-time.png |
-, 1001s, 21.0%
|
-, 1001s, 35.7%
|
-, 1001s, 8.8%
|
-, 1001s, 7.4%
|
275-Nb14T194.real-time.png |
sat, 11s, 23.2%
|
sat, 32s, 42.5%
|
sat, 14s, 16.0%
|
sat, 12s, 18.7%
|
276-Nb27T6.real-time.png |
unsat, 979s, 13.5%
|
unsat, 358s, 27.9%
|
unsat, 383s, 10.6%
|
unsat, 400s, 9.3%
|
277-Nb29T6.real-time.png |
-, 1001s, 13.5%
|
unsat, 681s, 27.1%
|
unsat, 415s, 11.8%
|
unsat, 490s, 9.5%
|
278-Nb37T6.real-time.png |
-, 1001s, 17.4%
|
unsat, 991s, 30.3%
|
unsat, 810s, 15.6%
|
unsat, 959s, 15.9%
|
279-Nb39T6.real-time.png |
-, 1001s, 19.4%
|
-, 1001s, 36.3%
|
-, 1001s, 16.2%
|
-, 1001s, 17.7%
|
280-Nb42T6.real-time.png |
-, 1001s, 20.9%
|
-, 1001s, 30.7%
|
-, 1001s, 16.7%
|
-, 1001s, 20.0%
|
281-Nb44T6.real-time.png |
-, 1001s, 24.2%
|
-, 1001s, 32.2%
|
-, 1001s, 16.7%
|
-, 1001s, 24.6%
|
282-Nb45T6.real-time.png |
-, 1001s, 21.7%
|
-, 1001s, 34.2%
|
-, 1001s, 17.3%
|
-, 1001s, 24.1%
|
283-Nb49T6.real-time.png |
-, 1001s, 21.7%
|
-, 1001s, 33.9%
|
-, 1001s, 19.4%
|
-, 1001s, 28.9%
|
284-Nb51T6.real-time.png |
-, 1001s, 24.2%
|
-, 1001s, 36.7%
|
-, 1001s, 20.9%
|
-, 1001s, 30.4%
|
285-Nb52T6.real-time.png |
-, 1001s, 27.6%
|
-, 1001s, 36.9%
|
-, 1001s, 20.7%
|
-, 1001s, 30.3%
|
286-Nb54T6.real-time.png |
-, 1001s, 25.1%
|
-, 1001s, 35.7%
|
-, 1001s, 22.0%
|
-, 1001s, 34.6%
|
287-Nb8T60.real-time.png |
-, 1001s, 21.3%
|
-, 1001s, 29.8%
|
-, 1001s, 27.3%
|
-, 1001s, 8.8%
|
288-Nb8T61.real-time.png |
-, 1001s, 22.0%
|
-, 1001s, 30.0%
|
-, 1001s, 31.2%
|
-, 1001s, 8.1%
|
289-Nb8T62.real-time.png |
-, 1001s, 20.9%
|
-, 1001s, 27.3%
|
-, 1001s, 24.3%
|
-, 1001s, 9.8%
|
290-Nb8T63.real-time.png |
sat, 1s, 24.0%
|
-, 1001s, 29.9%
|
-, 1001s, 30.7%
|
-, 1001s, 10.1%
|
291-Karatsuba4477457x5308417.real-time.png |
sat, 348s, 17.1%
|
sat, 615s, 21.2%
|
-, 1001s, 9.4%
|
sat, 44s, 7.2%
|
292-Karatsuba6972593x13466917.real-time.png |
sat, 153s, 15.5%
|
sat, 288s, 21.7%
|
sat, 158s, 7.6%
|
sat, 572s, 6.8%
|
293-Karatsuba7654321x1234567.real-time.png |
sat, 47s, 18.3%
|
sat, 418s, 22.7%
|
sat, 251s, 8.4%
|
sat, 185s, 7.2%
|
294-factoring29986577x29986577.real-time.png |
sat, 51s, 14.2%
|
sat, 5s, 16.5%
|
-, 1001s, 12.0%
|
sat, 104s, 6.7%
|
295-factoring39916801x54018521.real-time.png |
-, 1001s, 14.2%
|
-, 1001s, 18.1%
|
sat, 7s, 6.8%
|
sat, 345s, 6.4%
|
296-factoring54018521x562448657.real-time.png |
-, 1001s, 15.7%
|
-, 1001s, 17.7%
|
-, 1001s, 11.7%
|
-, 1001s, 10.1%
|
297-factoring87654321x12345678.real-time.png |
sat, 62s, 15.0%
|
sat, 166s, 16.0%
|
sat, 204s, 12.9%
|
sat, 246s, 7.9%
|
298-factoring94418953x321534781.real-time.png |
-, 1001s, 14.2%
|
-, 1001s, 13.6%
|
-, 1001s, 10.0%
|
-, 1001s, 6.9%
|
299-prime_119218851371.real-time.png |
unsat, 28s, 10.3%
|
unsat, 88s, 17.1%
|
unsat, 94s, 10.0%
|
unsat, 82s, 6.8%
|
300-prime_200560490131.real-time.png |
unsat, 73s, 12.7%
|
unsat, 176s, 20.4%
|
unsat, 135s, 10.3%
|
unsat, 138s, 7.3%
|
301-T103.2.0.real-time.png |
unsat, 587s, 42.3%
|
-, 1001s, 55.5%
|
unsat, 912s, 22.7%
|
unsat, 763s, 24.6%
|
302-T105.2.0.real-time.png |
unsat, 640s, 39.3%
|
unsat, 802s, 54.7%
|
unsat, 862s, 20.6%
|
unsat, 855s, 26.1%
|
303-T107.2.0.real-time.png |
unsat, 624s, 42.1%
|
-, 1001s, 55.9%
|
-, 1001s, 23.5%
|
-, 1001s, 23.6%
|
304-T116.2.0.real-time.png |
unsat, 215s, 36.4%
|
unsat, 323s, 51.7%
|
unsat, 243s, 15.0%
|
unsat, 466s, 20.0%
|
305-T117.2.0.real-time.png |
unsat, 280s, 38.8%
|
unsat, 523s, 49.8%
|
unsat, 422s, 18.0%
|
unsat, 430s, 17.6%
|
306-T122.2.0.real-time.png |
unsat, 921s, 40.4%
|
-, 1001s, 53.8%
|
-, 1001s, 21.9%
|
-, 1001s, 23.8%
|
307-T125.2.0.real-time.png |
unsat, 426s, 41.4%
|
unsat, 776s, 53.2%
|
unsat, 573s, 19.0%
|
unsat, 481s, 19.9%
|
308-T129.2.0.real-time.png |
unsat, 688s, 39.3%
|
-, 1001s, 54.4%
|
unsat, 648s, 20.8%
|
unsat, 760s, 23.2%
|
309-T56.2.0.real-time.png |
unsat, 402s, 38.9%
|
unsat, 537s, 49.0%
|
unsat, 514s, 18.1%
|
unsat, 446s, 17.7%
|
310-T62.2.0.real-time.png |
-, 1001s, 42.6%
|
-, 1001s, 51.1%
|
-, 1001s, 20.4%
|
unsat, 933s, 22.1%
|
311-T77.2.0.real-time.png |
unsat, 403s, 39.6%
|
unsat, 719s, 53.7%
|
unsat, 714s, 18.5%
|
-, 1001s, 23.6%
|
312-T82.2.0.real-time.png |
unsat, 479s, 38.8%
|
-, 1001s, 55.3%
|
unsat, 633s, 17.0%
|
unsat, 640s, 19.4%
|
313-T84.2.0.real-time.png |
unsat, 691s, 39.7%
|
-, 1001s, 54.8%
|
unsat, 672s, 18.7%
|
unsat, 758s, 21.5%
|
314-T86.2.0.real-time.png |
unsat, 724s, 39.5%
|
-, 1001s, 54.8%
|
-, 1001s, 20.3%
|
unsat, 988s, 22.8%
|
315-T87.2.0.real-time.png |
unsat, 906s, 38.8%
|
-, 1001s, 53.2%
|
unsat, 840s, 19.9%
|
unsat, 716s, 19.4%
|
316-T90.2.0.real-time.png |
unsat, 691s, 41.7%
|
unsat, 980s, 54.2%
|
unsat, 724s, 19.5%
|
unsat, 757s, 24.1%
|
317-T92.2.0.real-time.png |
unsat, 479s, 39.7%
|
unsat, 762s, 53.8%
|
unsat, 741s, 19.8%
|
unsat, 477s, 16.3%
|
318-T93.2.0.real-time.png |
unsat, 674s, 40.9%
|
-, 1001s, 53.7%
|
-, 1001s, 21.7%
|
-, 1001s, 23.1%
|
319-T96.2.0.real-time.png |
unsat, 556s, 43.1%
|
unsat, 916s, 52.3%
|
unsat, 881s, 21.2%
|
-, 1001s, 27.5%
|
320-T98.2.0.real-time.png |
unsat, 697s, 40.8%
|
unsat, 808s, 54.9%
|
unsat, 548s, 19.5%
|
-, 1001s, 22.6%
|
321-1mod8.rules.7-7.real-time.png |
-, 1001s, 17.3%
|
-, 1001s, 19.8%
|
-, 1001s, 7.7%
|
-, 1001s, 6.2%
|
322-5or7mod8.rules.7-7.real-time.png |
-, 1001s, 12.6%
|
-, 1001s, 20.3%
|
-, 1001s, 6.9%
|
-, 1001s, 6.8%
|
323-C3-2-31.real-time.png |
sat, 8s, 13.4%
|
sat, 37s, 19.4%
|
sat, 39s, 11.3%
|
sat, 36s, 6.5%
|
324-ad-A-3-7-17.real-time.png |
-, 1001s, 8.2%
|
-, 1001s, 10.4%
|
-, 1001s, 5.6%
|
-, 1001s, 6.1%
|
325-ax-d-4-7-5.real-time.png |
-, 1001s, 10.9%
|
-, 1001s, 10.8%
|
-, 1001s, 7.1%
|
-, 1001s, 5.8%
|
326-bx-d-4-7-6.real-time.png |
sat, 363s, 11.3%
|
-, 1001s, 14.4%
|
-, 1001s, 5.9%
|
-, 1001s, 5.3%
|
327-bx-d-4-7-8.real-time.png |
-, 1001s, 11.1%
|
-, 1001s, 14.7%
|
-, 1001s, 6.2%
|
-, 1001s, 5.8%
|
328-by-X-2-7-100.real-time.png |
unsat, 558s, 22.8%
|
unsat, 474s, 26.4%
|
unsat, 426s, 10.3%
|
unsat, 469s, 8.6%
|
329-by-alt-5-7.real-time.png |
-, 1001s, 15.8%
|
-, 1001s, 19.1%
|
-, 1001s, 7.2%
|
-, 1001s, 5.8%
|
330-bz-X-4-7-6.real-time.png |
-, 1001s, 10.5%
|
-, 1001s, 13.8%
|
-, 1001s, 6.4%
|
-, 1001s, 4.5%
|
331-cannonball-opt-y.rules.4-10.real-time.png |
-, 1001s, 15.7%
|
-, 1001s, 14.5%
|
-, 1001s, 7.4%
|
-, 1001s, 6.3%
|
332-cz-3-7-7.real-time.png |
-, 1001s, 16.9%
|
-, 1001s, 14.2%
|
-, 1001s, 7.6%
|
-, 1001s, 4.9%
|
333-cz-alt-3-7.real-time.png |
-, 1001s, 11.2%
|
-, 1001s, 13.1%
|
-, 1001s, 6.0%
|
-, 1001s, 5.4%
|
334-cz-d-4-7-5.real-time.png |
-, 1001s, 15.0%
|
-, 1001s, 13.3%
|
-, 1001s, 7.2%
|
-, 1001s, 5.8%
|
335-full-ax-xa.rules.7-7.real-time.png |
sat, 572s, 13.7%
|
-, 1001s, 20.2%
|
sat, 550s, 7.3%
|
sat, 669s, 5.7%
|
336-full-by-za.rules.5-7.real-time.png |
sat, 480s, 9.1%
|
-, 1001s, 17.0%
|
-, 1001s, 7.4%
|
-, 1001s, 5.2%
|
337-full-cy-caa.rules.7-7.real-time.png |
sat, 114s, 18.1%
|
sat, 186s, 24.9%
|
sat, 413s, 9.4%
|
sat, 429s, 6.5%
|
338-less-cy-caa.rules.4-9.real-time.png |
-, 1001s, 12.4%
|
-, 1001s, 12.9%
|
-, 1001s, 5.6%
|
-, 1001s, 4.6%
|
339-less-cy-caa.rules.6-4.real-time.png |
-, 1001s, 12.6%
|
-, 1001s, 17.6%
|
-, 1001s, 8.3%
|
-, 1001s, 6.1%
|
340-mod8-abd-yad.rules.7-7.real-time.png |
sat, 165s, 18.4%
|
sat, 4s, 14.8%
|
sat, 4s, 6.6%
|
sat, 4s, 7.2%
|
341-mod8-bbd-zbd.rules.7-7.real-time.png |
-, 1001s, 12.0%
|
-, 1001s, 18.0%
|
-, 1001s, 8.6%
|
-, 1001s, 6.4%
|
342-sted1_0x0-330.real-time.png |
sat, 392s, 13.3%
|
sat, 185s, 12.2%
|
sat, 164s, 6.6%
|
sat, 174s, 5.2%
|
343-sted1_0x0-350.real-time.png |
-, 1001s, 16.9%
|
-, 1001s, 14.0%
|
-, 1001s, 11.7%
|
-, 1001s, 7.2%
|
344-sted1_0x0-380.real-time.png |
-, 1001s, 16.5%
|
-, 1001s, 15.3%
|
-, 1001s, 8.1%
|
-, 1001s, 10.3%
|
345-sted1_0x0-420.real-time.png |
-, 1001s, 11.6%
|
-, 1001s, 14.8%
|
-, 1001s, 11.3%
|
-, 1001s, 8.3%
|
346-sted1_0x1e3-100.real-time.png |
-, 1001s, 25.0%
|
-, 1001s, 33.8%
|
-, 1001s, 12.4%
|
-, 1001s, 4.8%
|
347-sted1_0x1e3-200.real-time.png |
-, 1001s, 19.9%
|
-, 1001s, 20.9%
|
-, 1001s, 15.8%
|
-, 1001s, 9.5%
|
348-sted1_0x1e3-300.real-time.png |
-, 1001s, 20.9%
|
-, 1001s, 20.7%
|
-, 1001s, 17.8%
|
-, 1001s, 8.3%
|
349-sted1_0x24204-330.real-time.png |
sat, 719s, 12.7%
|
sat, 144s, 10.8%
|
sat, 178s, 6.0%
|
sat, 183s, 5.0%
|
350-sted1_0x24204-350.real-time.png |
-, 1001s, 14.1%
|
-, 1001s, 15.0%
|
-, 1001s, 10.4%
|
-, 1001s, 5.6%
|
351-sted1_0x24204-380.real-time.png |
-, 1001s, 12.6%
|
-, 1001s, 15.4%
|
-, 1001s, 10.4%
|
-, 1001s, 6.1%
|
352-sted5_0x0-40.real-time.png |
sat, 1s, 6.8%
|
sat, 1s, 10.9%
|
sat, 2s, 5.0%
|
sat, 2s, 4.9%
|
353-sted5_0x0-50.real-time.png |
-, 1001s, 17.3%
|
sat, 96s, 13.4%
|
sat, 9s, 6.7%
|
sat, 46s, 4.4%
|
354-sted5_0x0-60.real-time.png |
-, 1001s, 23.3%
|
-, 1001s, 16.2%
|
-, 1001s, 12.5%
|
-, 1001s, 6.6%
|
355-sted5_0x0-70.real-time.png |
-, 1001s, 13.3%
|
-, 1001s, 16.2%
|
-, 1001s, 13.0%
|
-, 1001s, 9.0%
|
356-sted5_0x1e3-20.real-time.png |
-, 1001s, 22.2%
|
-, 1001s, 22.8%
|
-, 1001s, 14.6%
|
-, 1001s, 11.3%
|
357-sted5_0x1e3-40.real-time.png |
-, 1001s, 19.0%
|
-, 1001s, 23.6%
|
-, 1001s, 16.2%
|
-, 1001s, 9.1%
|
358-sted5_0x1e3-60.real-time.png |
-, 1001s, 17.6%
|
-, 1001s, 19.7%
|
-, 1001s, 13.0%
|
-, 1001s, 8.2%
|
359-sted5_0x24204-50.real-time.png |
sat, 323s, 15.9%
|
sat, 83s, 12.8%
|
sat, 207s, 7.5%
|
sat, 250s, 5.2%
|
360-sted5_0x24204-60.real-time.png |
-, 1001s, 21.5%
|
-, 1001s, 15.6%
|
-, 1001s, 12.1%
|
-, 1001s, 7.2%
|
361-sted5_0x24204-70.real-time.png |
-, 1001s, 15.2%
|
-, 1001s, 15.9%
|
-, 1001s, 12.6%
|
-, 1001s, 5.3%
|
362-apn-sbox5-cut3-symmbreak.real-time.png |
-, 1001s, 22.2%
|
-, 1001s, 19.4%
|
-, 1001s, 10.3%
|
-, 1001s, 7.3%
|
363-apn-sbox5-cut4-symmbreak.real-time.png |
-, 1001s, 22.2%
|
-, 1001s, 22.5%
|
-, 1001s, 10.1%
|
-, 1001s, 8.0%
|
364-apn-sbox5-cut5-symmbreak.real-time.png |
-, 1001s, 25.7%
|
-, 1001s, 16.7%
|
-, 1001s, 8.8%
|
-, 1001s, 7.5%
|
365-apn-sbox6-cut3-helpbox23.real-time.png |
-, 1001s, 20.5%
|
-, 1001s, 26.7%
|
-, 1001s, 17.7%
|
-, 1001s, 9.8%
|
366-apn-sbox6-cut3-helpbox26.real-time.png |
-, 1001s, 16.1%
|
-, 1001s, 22.9%
|
-, 1001s, 12.9%
|
-, 1001s, 14.6%
|
367-apn-sbox6-cut3-helpbox28.real-time.png |
-, 1001s, 16.2%
|
-, 1001s, 19.7%
|
-, 1001s, 14.3%
|
-, 1001s, 10.1%
|
368-apn-sbox6-cut3-helpbox29.real-time.png |
-, 1001s, 16.5%
|
-, 1001s, 15.8%
|
-, 1001s, 10.0%
|
sat, 284s, 6.3%
|
369-apn-sbox6-cut3-helpbox30.real-time.png |
-, 1001s, 19.0%
|
-, 1001s, 16.0%
|
sat, 117s, 6.9%
|
sat, 44s, 6.2%
|
370-apn-sbox6-cut3-helpbox31.real-time.png |
-, 1001s, 13.8%
|
sat, 59s, 17.2%
|
sat, 858s, 8.3%
|
sat, 87s, 6.6%
|
371-apn-sbox6-cut4-helpbox23.real-time.png |
-, 1001s, 14.4%
|
-, 1001s, 30.5%
|
-, 1001s, 18.6%
|
-, 1001s, 14.8%
|
372-apn-sbox6-cut4-helpbox26.real-time.png |
-, 1001s, 20.3%
|
-, 1001s, 20.5%
|
-, 1001s, 15.4%
|
-, 1001s, 10.4%
|
373-apn-sbox6-cut4-helpbox28.real-time.png |
-, 1001s, 20.0%
|
-, 1001s, 19.5%
|
-, 1001s, 14.2%
|
-, 1001s, 9.6%
|
374-apn-sbox6-cut4-helpbox29.real-time.png |
-, 1001s, 29.5%
|
sat, 644s, 16.3%
|
-, 1001s, 8.9%
|
-, 1001s, 10.9%
|
375-apn-sbox6-cut4-helpbox30.real-time.png |
-, 1001s, 27.3%
|
-, 1001s, 17.2%
|
sat, 331s, 7.5%
|
sat, 139s, 8.6%
|
376-apn-sbox6-cut4-helpbox31.real-time.png |
sat, 2s, 17.2%
|
-, 1001s, 15.7%
|
sat, 69s, 7.5%
|
sat, 241s, 11.3%
|
377-apn-sbox6-cut5-helpbox23.real-time.png |
-, 1001s, 25.9%
|
-, 1001s, 25.3%
|
-, 1001s, 19.8%
|
-, 1001s, 13.9%
|
378-apn-sbox6-cut5-helpbox26.real-time.png |
-, 1001s, 23.5%
|
-, 1001s, 22.3%
|
-, 1001s, 17.0%
|
-, 1001s, 12.9%
|
379-apn-sbox6-cut5-helpbox28.real-time.png |
-, 1001s, 27.0%
|
-, 1001s, 18.4%
|
-, 1001s, 13.4%
|
sat, 167s, 6.9%
|
380-apn-sbox6-cut5-helpbox29.real-time.png |
-, 1001s, 27.2%
|
sat, 479s, 16.5%
|
sat, 518s, 11.7%
|
-, 1001s, 14.1%
|
381-apn-sbox6-cut5-helpbox30.real-time.png |
sat, 7s, 12.1%
|
sat, 21s, 18.9%
|
sat, 567s, 9.1%
|
sat, 623s, 8.1%
|
382-bibd-16-80-15-3-2_glb.real-time.png |
sat, 2s, 35.5%
|
sat, 16s, 34.8%
|
sat, 17s, 22.8%
|
sat, 3s, 16.0%
|
383-bibd-19-57-9-3-1_glb.real-time.png |
sat, 49s, 14.7%
|
sat, 0s, 25.7%
|
sat, 42s, 8.9%
|
sat, 45s, 5.8%
|
384-bibd-8-70-35-4-15_glb.real-time.png |
sat, 9s, 19.1%
|
sat, 31s, 25.8%
|
sat, 25s, 8.7%
|
sat, 27s, 8.5%
|
385-frb35-17-5-mgd_ext.real-time.png |
sat, 35s, 19.6%
|
sat, 3s, 19.0%
|
sat, 61s, 11.2%
|
sat, 44s, 7.2%
|
386-frb35-17-5_ext.real-time.png |
sat, 115s, 22.0%
|
sat, 123s, 18.9%
|
sat, 36s, 11.2%
|
sat, 24s, 6.7%
|
387-lei450-05b-05.real-time.png |
sat, 5s, 18.5%
|
sat, 8s, 15.2%
|
sat, 12s, 8.8%
|
sat, 9s, 6.2%
|
388-magicSquare-8_glb.real-time.png |
sat, 5s, 13.4%
|
sat, 173s, 19.0%
|
sat, 382s, 9.3%
|
sat, 223s, 8.9%
|
389-magicSquare-9_glb.real-time.png |
sat, 15s, 15.2%
|
-, 1001s, 18.8%
|
-, 1001s, 8.8%
|
-, 1001s, 7.4%
|
390-ortholatin-7.real-time.png |
sat, 93s, 8.1%
|
sat, 16s, 20.0%
|
sat, 3s, 5.0%
|
sat, 3s, 4.0%
|
391-patat-08-comp-3.real-time.png |
sat, 6s, 32.3%
|
sat, 32s, 33.9%
|
sat, 27s, 12.0%
|
sat, 52s, 9.0%
|
392-queen8-8-9.real-time.png |
sat, 0s, 15.1%
|
sat, 32s, 14.9%
|
sat, 19s, 9.4%
|
sat, 7s, 5.0%
|
393-ramsey-30-4.real-time.png |
-, 1001s, 10.9%
|
sat, 3s, 15.7%
|
sat, 2s, 7.4%
|
sat, 3s, 4.1%
|
394-ramsey-32-4.real-time.png |
-, 1001s, 9.4%
|
sat, 4s, 16.9%
|
sat, 4s, 10.3%
|
sat, 4s, 6.4%
|
395-si2-b03m-m400-03.real-time.png |
sat, 1s, 23.0%
|
sat, 53s, 35.2%
|
sat, 53s, 15.6%
|
sat, 52s, 8.1%
|
396-si2-b03m-m800-03.real-time.png |
sat, 1s, 14.1%
|
sat, 93s, 28.9%
|
sat, 93s, 13.7%
|
sat, 91s, 10.3%
|
397-si2-b06m-m1000-03.real-time.png |
sat, 1s, 17.3%
|
sat, 101s, 24.5%
|
sat, 102s, 8.5%
|
sat, 101s, 6.3%
|
398-si2-m4Dr2-m256-08.real-time.png |
sat, 3s, 29.5%
|
sat, 674s, 36.9%
|
sat, 675s, 12.3%
|
sat, 652s, 11.0%
|
399-si2-r001-m200-00.real-time.png |
sat, 5s, 12.0%
|
sat, 830s, 21.6%
|
sat, 787s, 10.9%
|
sat, 813s, 6.3%
|
400-si2-r001-m200-09.real-time.png |
sat, 7s, 16.3%
|
sat, 554s, 20.1%
|
sat, 543s, 10.9%
|
sat, 532s, 9.2%
|
401-toughsat_22bits_0.real-time.png |
sat, 32s, 18.0%
|
sat, 37s, 25.8%
|
sat, 43s, 9.8%
|
sat, 19s, 10.0%
|
402-toughsat_22bits_1.real-time.png |
sat, 12s, 18.4%
|
sat, 34s, 24.9%
|
sat, 68s, 10.8%
|
sat, 21s, 9.3%
|
403-toughsat_23bits_0.real-time.png |
sat, 7s, 19.0%
|
sat, 36s, 25.0%
|
sat, 54s, 10.1%
|
sat, 112s, 6.4%
|
404-toughsat_23bits_1.real-time.png |
sat, 13s, 18.0%
|
sat, 53s, 29.0%
|
sat, 209s, 10.8%
|
sat, 141s, 7.8%
|
405-toughsat_23bits_2.real-time.png |
sat, 110s, 17.5%
|
sat, 153s, 23.2%
|
sat, 346s, 9.3%
|
sat, 202s, 7.4%
|
406-toughsat_23bits_3.real-time.png |
sat, 154s, 17.1%
|
sat, 35s, 27.5%
|
sat, 164s, 7.3%
|
sat, 127s, 7.3%
|
407-toughsat_24bits_0.real-time.png |
sat, 162s, 16.9%
|
sat, 212s, 16.3%
|
sat, 158s, 10.2%
|
sat, 116s, 7.8%
|
408-toughsat_24bits_1.real-time.png |
sat, 94s, 16.5%
|
sat, 411s, 20.8%
|
sat, 82s, 8.3%
|
sat, 340s, 6.9%
|
409-toughsat_24bits_2.real-time.png |
sat, 31s, 15.8%
|
sat, 99s, 24.7%
|
sat, 66s, 11.6%
|
sat, 84s, 8.8%
|
410-toughsat_24bits_3.real-time.png |
sat, 133s, 17.0%
|
sat, 226s, 20.8%
|
sat, 534s, 11.2%
|
sat, 338s, 6.8%
|
411-toughsat_25bits_0.real-time.png |
sat, 26s, 17.1%
|
sat, 274s, 19.1%
|
sat, 274s, 8.5%
|
sat, 748s, 8.2%
|
412-toughsat_25bits_1.real-time.png |
sat, 103s, 18.6%
|
sat, 860s, 18.8%
|
sat, 556s, 9.5%
|
sat, 495s, 8.8%
|
413-toughsat_25bits_2.real-time.png |
sat, 114s, 18.1%
|
sat, 510s, 20.2%
|
sat, 621s, 11.7%
|
sat, 157s, 7.3%
|
414-toughsat_25bits_3.real-time.png |
sat, 5s, 17.8%
|
sat, 575s, 21.4%
|
sat, 18s, 9.6%
|
sat, 48s, 7.5%
|
415-toughsat_26bits_0.real-time.png |
sat, 275s, 20.0%
|
sat, 468s, 24.7%
|
-, 1001s, 8.6%
|
-, 1001s, 4.9%
|
416-toughsat_26bits_1.real-time.png |
sat, 220s, 19.3%
|
-, 1001s, 24.7%
|
-, 1001s, 14.3%
|
-, 1001s, 4.7%
|
417-toughsat_26bits_2.real-time.png |
sat, 797s, 20.0%
|
-, 1001s, 24.5%
|
-, 1001s, 9.5%
|
-, 1001s, 6.8%
|
418-toughsat_26bits_3.real-time.png |
sat, 188s, 19.1%
|
-, 1001s, 20.5%
|
sat, 747s, 10.3%
|
sat, 728s, 6.1%
|
419-toughsat_27bits_0.real-time.png |
sat, 388s, 21.7%
|
-, 1001s, 24.3%
|
-, 1001s, 9.0%
|
-, 1001s, 6.5%
|
420-toughsat_28bits_0.real-time.png |
-, 1001s, 21.9%
|
-, 1001s, 28.2%
|
-, 1001s, 12.9%
|
-, 1001s, 7.9%
|
421-toughsat_29bits_0.real-time.png |
-, 1001s, 22.9%
|
-, 1001s, 23.4%
|
-, 1001s, 12.7%
|
-, 1001s, 10.7%
|
422-toughsat_30bits_0.real-time.png |
-, 1001s, 23.7%
|
-, 1001s, 28.8%
|
-, 1001s, 17.2%
|
-, 1001s, 11.7%
|
423-cruxmiter28seed8.real-time.png |
unsat, 450s, 11.9%
|
-, 1001s, 38.0%
|
unsat, 633s, 19.6%
|
unsat, 628s, 16.6%
|
424-cruxmiter29seed4.real-time.png |
unsat, 616s, 11.7%
|
-, 1001s, 47.9%
|
unsat, 802s, 21.2%
|
unsat, 558s, 17.1%
|
425-cruxmiter29seed9.real-time.png |
-, 1001s, 13.3%
|
-, 1001s, 51.6%
|
-, 1001s, 25.7%
|
-, 1001s, 15.8%
|
426-cruxmiter32seed4.real-time.png |
-, 1001s, 12.1%
|
-, 1001s, 37.1%
|
-, 1001s, 20.3%
|
-, 1001s, 11.4%
|
427-eq2csparrc162cbpwtcl16.real-time.png |
-, 1001s, 19.7%
|
-, 1001s, 22.2%
|
-, 1001s, 10.2%
|
-, 1001s, 13.4%
|
428-eqbparrc12spctbk12.real-time.png |
-, 1001s, 13.9%
|
-, 1001s, 36.2%
|
-, 1001s, 13.8%
|
-, 1001s, 9.7%
|
429-eqbparrc14spwtcl14.real-time.png |
-, 1001s, 13.6%
|
-, 1001s, 31.6%
|
-, 1001s, 14.8%
|
-, 1001s, 8.6%
|
430-eqbparrc18spwtrc18.real-time.png |
-, 1001s, 15.4%
|
-, 1001s, 19.9%
|
-, 1001s, 14.2%
|
-, 1001s, 7.6%
|
431-eqbpdtlf12bparrc12.real-time.png |
-, 1001s, 15.3%
|
-, 1001s, 32.1%
|
-, 1001s, 15.1%
|
-, 1001s, 9.5%
|
432-eqbpdtlf14bpwtcl14.real-time.png |
-, 1001s, 15.6%
|
-, 1001s, 38.0%
|
-, 1001s, 11.8%
|
-, 1001s, 10.9%
|
433-eqbpdtlf14spctbk14.real-time.png |
-, 1001s, 16.1%
|
-, 1001s, 34.2%
|
-, 1001s, 15.5%
|
-, 1001s, 8.6%
|
434-eqbpdtlf14spdtlf14.real-time.png |
-, 1001s, 14.0%
|
-, 1001s, 19.7%
|
-, 1001s, 13.7%
|
-, 1001s, 10.6%
|
435-eqbpdtlf16spdtlf16.real-time.png |
-, 1001s, 15.3%
|
-, 1001s, 17.2%
|
-, 1001s, 13.8%
|
-, 1001s, 8.5%
|
436-eqbpdtlf18sparcl18.real-time.png |
-, 1001s, 21.1%
|
-, 1001s, 18.6%
|
-, 1001s, 11.9%
|
-, 1001s, 7.5%
|
437-eqbpwtcl10spwtcl10.real-time.png |
unsat, 381s, 13.4%
|
unsat, 357s, 37.2%
|
unsat, 208s, 13.0%
|
unsat, 222s, 12.1%
|
438-eqbpwtrc10bpdtlf10.real-time.png |
unsat, 512s, 14.7%
|
unsat, 441s, 30.0%
|
unsat, 214s, 14.8%
|
unsat, 218s, 15.4%
|
439-eqbpwtrc10spctbk10.real-time.png |
-, 1001s, 12.9%
|
unsat, 462s, 40.2%
|
unsat, 393s, 16.0%
|
unsat, 374s, 8.5%
|
440-eqsparcl10bpwtrc10.real-time.png |
unsat, 184s, 13.1%
|
unsat, 415s, 30.8%
|
unsat, 268s, 16.0%
|
unsat, 201s, 13.8%
|
441-eqsparcl12bpwtrc12.real-time.png |
-, 1001s, 15.9%
|
-, 1001s, 42.3%
|
-, 1001s, 17.3%
|
-, 1001s, 11.2%
|
442-eqsparrc12bpdtlf12.real-time.png |
-, 1001s, 16.5%
|
-, 1001s, 44.0%
|
-, 1001s, 14.1%
|
-, 1001s, 11.8%
|
443-eqsparrc14spctbk14.real-time.png |
-, 1001s, 16.1%
|
-, 1001s, 19.7%
|
-, 1001s, 14.5%
|
-, 1001s, 8.2%
|
444-eqsparrc16spwtcl16.real-time.png |
-, 1001s, 14.1%
|
-, 1001s, 23.0%
|
-, 1001s, 12.3%
|
-, 1001s, 7.4%
|
445-eqspctbk12bpwtrc12.real-time.png |
-, 1001s, 14.7%
|
-, 1001s, 25.7%
|
-, 1001s, 17.9%
|
-, 1001s, 8.3%
|
446-eqspctbk14sparcl14.real-time.png |
-, 1001s, 16.9%
|
-, 1001s, 21.9%
|
-, 1001s, 13.7%
|
-, 1001s, 7.8%
|
447-eqspctbk14spwtcl14.real-time.png |
-, 1001s, 14.0%
|
-, 1001s, 27.0%
|
-, 1001s, 10.2%
|
-, 1001s, 9.4%
|
448-eqspdtlf14bpwtrc14.real-time.png |
-, 1001s, 14.5%
|
-, 1001s, 20.7%
|
-, 1001s, 17.1%
|
-, 1001s, 13.1%
|
449-eqspwtcl14bpwtcl14.real-time.png |
-, 1001s, 12.0%
|
-, 1001s, 29.3%
|
-, 1001s, 12.6%
|
-, 1001s, 17.6%
|
450-eqspwtrc16bparrc16.real-time.png |
-, 1001s, 17.5%
|
-, 1001s, 26.1%
|
-, 1001s, 14.0%
|
-, 1001s, 6.9%
|
451-hcp_CP14_14.real-time.png |
-, 1001s, 16.2%
|
-, 1001s, 26.8%
|
-, 1001s, 12.0%
|
-, 1001s, 7.6%
|
452-hcp_CP16_16.real-time.png |
-, 1001s, 14.4%
|
-, 1001s, 23.7%
|
-, 1001s, 12.0%
|
-, 1001s, 6.3%
|
453-hcp_CP18_18.real-time.png |
-, 1001s, 15.0%
|
-, 1001s, 22.8%
|
-, 1001s, 12.1%
|
-, 1001s, 5.7%
|
454-hcp_CP20_20.real-time.png |
-, 1001s, 13.7%
|
-, 1001s, 23.1%
|
-, 1001s, 12.6%
|
-, 1001s, 5.4%
|
455-hcp_CP22_22.real-time.png |
-, 1001s, 13.0%
|
-, 1001s, 23.9%
|
-, 1001s, 12.3%
|
-, 1001s, 6.3%
|
456-hcp_CP24_24.real-time.png |
-, 1001s, 12.6%
|
-, 1001s, 25.9%
|
-, 1001s, 12.5%
|
-, 1001s, 5.4%
|
457-hcp_CP26_26.real-time.png |
-, 1001s, 11.8%
|
-, 1001s, 26.1%
|
-, 1001s, 10.2%
|
-, 1001s, 5.2%
|
458-hcp_bij16_16.real-time.png |
unknown error (134), 344s
|
unknown error (134), 862s
|
-, 1001s, 41.1%
|
-, 1001s, 23.8%
|
459-hcp_d12_12.real-time.png |
-, 1001s, 19.4%
|
-, 1001s, 27.9%
|
-, 1001s, 24.0%
|
-, 1001s, 12.3%
|
460-hcp_d14_14.real-time.png |
-, 1001s, 15.0%
|
-, 1001s, 26.1%
|
-, 1001s, 17.7%
|
-, 1001s, 9.8%
|
461-hcp_d16_16.real-time.png |
-, 1001s, 16.2%
|
-, 1001s, 27.7%
|
-, 1001s, 19.1%
|
-, 1001s, 13.7%
|
462-hcp_d18_18.real-time.png |
-, 1001s, 17.7%
|
-, 1001s, 24.7%
|
-, 1001s, 22.5%
|
-, 1001s, 16.6%
|
463-hcp_d20_20.real-time.png |
-, 1001s, 15.5%
|
-, 1001s, 25.6%
|
-, 1001s, 17.4%
|
-, 1001s, 10.6%
|
464-hcp_d22_22.real-time.png |
-, 1001s, 16.0%
|
-, 1001s, 29.7%
|
-, 1001s, 18.4%
|
-, 1001s, 12.5%
|
465-hcp_d24_24.real-time.png |
-, 1001s, 15.5%
|
-, 1001s, 26.8%
|
-, 1001s, 15.7%
|
-, 1001s, 17.0%
|
466-hcp_r20_20.real-time.png |
sat, 19s, 25.8%
|
sat, 14s, 17.2%
|
sat, 14s, 0.0%
|
sat, 13s, 9.2%
|
467-hcp_r26_26.real-time.png |
-, 41s
|
out of memory, 63s
|
out of memory, 64s
|
out of memory, 53s
|
468-MM-22.real-time.png |
-, 1001s, 26.4%
|
-, 1001s, 28.6%
|
-, 1001s, 11.0%
|
-, 1001s, 12.0%
|
469-MM-23-2-2-2-2-3.real-time.png |
-, 1001s, 25.5%
|
-, 1001s, 24.7%
|
-, 1001s, 16.6%
|
-, 1001s, 9.3%
|
470-MM-23-2-2-2-2-A.real-time.png |
-, 1001s, 25.4%
|
-, 1001s, 23.9%
|
-, 1001s, 15.7%
|
-, 1001s, 9.3%
|
471-MM-23-2-2-2-2-B.real-time.png |
-, 1001s, 25.4%
|
-, 1001s, 24.5%
|
-, 1001s, 16.3%
|
-, 1001s, 11.4%
|
472-MM-23-2-2-2-2-C.real-time.png |
-, 1001s, 24.2%
|
-, 1001s, 25.0%
|
-, 1001s, 14.9%
|
-, 1001s, 10.2%
|
473-MM-23-2-2-2-2-D.real-time.png |
-, 1001s, 25.0%
|
-, 1001s, 24.8%
|
-, 1001s, 13.6%
|
-, 1001s, 11.4%
|
474-MM-23-2-2-2-2-M.real-time.png |
-, 1001s, 24.8%
|
-, 1001s, 24.3%
|
-, 1001s, 14.1%
|
-, 1001s, 9.2%
|
475-MM-23-2-2-2-3-4.real-time.png |
-, 1001s, 25.7%
|
-, 1001s, 23.7%
|
-, 1001s, 14.9%
|
-, 1001s, 9.1%
|
476-MM-23-2-2-2-4-A.real-time.png |
-, 1001s, 26.1%
|
-, 1001s, 24.1%
|
-, 1001s, 15.0%
|
-, 1001s, 9.2%
|
477-MM-23-2-2-2-4-B.real-time.png |
-, 1001s, 26.2%
|
-, 1001s, 23.5%
|
-, 1001s, 15.5%
|
-, 1001s, 10.6%
|
478-MM-23-2-2-3-A.real-time.png |
-, 1001s, 25.9%
|
-, 1001s, 24.8%
|
-, 1001s, 14.4%
|
-, 1001s, 9.4%
|
479-MM-23-2-2-3-B.real-time.png |
-, 1001s, 26.2%
|
-, 1001s, 26.3%
|
-, 1001s, 13.8%
|
-, 1001s, 11.6%
|
480-MM-23-2-4-A.real-time.png |
-, 1001s, 23.9%
|
-, 1001s, 24.8%
|
-, 1001s, 14.7%
|
-, 1001s, 11.9%
|
481-MM-23-2-4-B.real-time.png |
-, 1001s, 27.6%
|
-, 1001s, 23.3%
|
-, 1001s, 19.0%
|
-, 1001s, 10.2%
|
482-MM-23-3-3-A.real-time.png |
-, 1001s, 27.0%
|
-, 1001s, 24.8%
|
-, 1001s, 16.3%
|
-, 1001s, 11.8%
|
483-MM-23-3-3-B.real-time.png |
-, 1001s, 24.9%
|
-, 1001s, 24.3%
|
-, 1001s, 14.4%
|
-, 1001s, 9.1%
|
484-MM-23-3-3-M.real-time.png |
-, 1001s, 26.8%
|
-, 1001s, 23.9%
|
-, 1001s, 15.0%
|
-, 1001s, 9.1%
|
485-MM-23-3-3-N.real-time.png |
-, 1001s, 26.0%
|
-, 1001s, 23.4%
|
-, 1001s, 16.2%
|
-, 1001s, 11.5%
|
486-MM-23-4-4-4-4-1.real-time.png |
-, 1001s, 26.0%
|
-, 1001s, 24.2%
|
-, 1001s, 12.8%
|
-, 1001s, 11.4%
|
487-MM-23-5-A.real-time.png |
-, 1001s, 25.9%
|
-, 1001s, 23.5%
|
-, 1001s, 16.4%
|
-, 1001s, 10.7%
|
488-MM-23-5-B.real-time.png |
-, 1001s, 28.3%
|
-, 1001s, 24.7%
|
-, 1001s, 14.6%
|
-, 1001s, 10.2%
|
489-MM-23-no-type3.real-time.png |
-, 1001s, 24.5%
|
-, 1001s, 32.5%
|
-, 1001s, 27.1%
|
-, 1001s, 20.8%
|
490-sv-comp19_prop-reachsafety.25_stack_longest_false-unreach-call.i-witness.real-time.png |
sat, 67s, 49.3%
|
sat, 58s, 49.7%
|
sat, 66s, 7.6%
|
sat, 66s, 8.7%
|
491-sv-comp19_prop-reachsafety.26_stack_cas_longer_false-unreach-call.i-witness.real-time.png |
sat, 64s, 69.5%
|
sat, 27s, 71.8%
|
sat, 30s, 18.2%
|
sat, 30s, 24.2%
|
492-sv-comp19_prop-reachsafety.barrier_3t_true-unreach-call.i-witness.real-time.png |
-, 51s
|
-, 1001s, 0.0%
|
-, 1001s, 0.0%
|
-, 1001s, 0.0%
|
493-sv-comp19_prop-reachsafety.fib_bench_longest_false-unreach-call.i-witness.real-time.png |
sat, 466s, 16.5%
|
sat, 300s, 23.0%
|
sat, 275s, 12.8%
|
sat, 230s, 6.1%
|
494-sv-comp19_prop-reachsafety.newton_2_2_true-unreach-call_true-termination.i-witness.real-time.png |
unsat, 155s, 42.3%
|
unsat, 54s, 45.6%
|
unsat, 37s, 13.1%
|
unsat, 35s, 9.2%
|
495-sv-comp19_prop-reachsafety.newton_2_3_true-unreach-call_true-termination.i-witness.real-time.png |
unsat, 83s, 35.4%
|
unsat, 60s, 47.6%
|
unsat, 42s, 12.6%
|
unsat, 40s, 9.3%
|
496-sv-comp19_prop-reachsafety.newton_2_4_true-unreach-call_true-termination.i-witness.real-time.png |
unsat, 163s, 40.5%
|
unsat, 62s, 46.5%
|
unsat, 41s, 13.5%
|
unsat, 43s, 8.8%
|
497-sv-comp19_prop-reachsafety.newton_2_6_false-unreach-call_true-termination.i-witness.real-time.png |
sat, 91s, 42.2%
|
sat, 28s, 48.0%
|
sat, 6s, 11.5%
|
sat, 17s, 7.7%
|
498-sv-comp19_prop-reachsafety.newton_2_8_false-unreach-call_true-termination.i-witness.real-time.png |
sat, 71s, 43.1%
|
sat, 28s, 50.1%
|
sat, 23s, 12.2%
|
sat, 2s, 8.6%
|
499-sv-comp19_prop-reachsafety.newton_3_6_false-unreach-call_true-termination.i-witness.real-time.png |
sat, 137s, 41.7%
|
sat, 114s, 47.5%
|
sat, 108s, 12.8%
|
sat, 43s, 9.4%
|
500-sv-comp19_prop-reachsafety.newton_3_7_false-unreach-call_true-termination.i-witness.real-time.png |
sat, 98s, 41.9%
|
sat, 44s, 51.6%
|
sat, 29s, 13.9%
|
sat, 20s, 10.2%
|
501-sv-comp19_prop-reachsafety.newton_3_8_false-unreach-call_true-termination.i-witness.real-time.png |
sat, 238s, 41.0%
|
sat, 40s, 51.7%
|
sat, 30s, 12.2%
|
sat, 22s, 11.2%
|
502-sv-comp19_prop-reachsafety.queue_longer_false-unreach-call.i-witness.real-time.png |
-, 56s
|
sat, 140s, 0.0%
|
sat, 138s, 0.0%
|
sat, 133s, 0.0%
|
503-sv-comp19_prop-reachsafety.race-4_2-thread_local_vars_false-unreach-call.i-witness.real-time.png |
sat, 26s, 31.2%
|
sat, 141s, 42.6%
|
sat, 139s, 10.0%
|
sat, 135s, 5.3%
|
504-sv-comp19_prop-reachsafety.sigma_false-unreach-call.i-witness.real-time.png |
sat, 911s, 26.3%
|
-, 1001s, 43.1%
|
-, 1001s, 11.0%
|
-, 1001s, 12.8%
|
505-sv-comp19_prop-reachsafety.sine_8_true-unreach-call_true-termination.i-witness.real-time.png |
unsat, 2s, 34.2%
|
unsat, 3s, 41.9%
|
unsat, 2s, 9.1%
|
unsat, 2s, 7.0%
|
506-sv-comp19_prop-reachsafety.square_5_true-unreach-call_true-termination.i-witness.real-time.png |
unsat, 79s, 19.7%
|
unsat, 110s, 22.0%
|
unsat, 61s, 6.2%
|
unsat, 124s, 4.5%
|
507-sv-comp19_prop-reachsafety.triangular-longer_false-unreach-call.i-witness.real-time.png |
sat, 143s, 18.7%
|
sat, 129s, 22.1%
|
sat, 146s, 11.7%
|
sat, 109s, 6.8%
|
508-size_4_4_4_i0418_r8.real-time.png |
-, 1001s, 14.8%
|
unsat, 556s, 16.5%
|
unsat, 196s, 12.2%
|
unsat, 449s, 6.9%
|
509-size_4_4_4_i0566_r8.real-time.png |
-, 1001s, 15.1%
|
unsat, 701s, 18.3%
|
unsat, 623s, 12.5%
|
unsat, 600s, 6.4%
|
510-size_4_4_4_i2704_r8.real-time.png |
-, 1001s, 14.4%
|
unsat, 572s, 18.1%
|
unsat, 389s, 12.0%
|
unsat, 424s, 7.3%
|
511-size_4_4_4_i3499_r8.real-time.png |
-, 1001s, 15.6%
|
unsat, 589s, 19.2%
|
unsat, 643s, 11.7%
|
unsat, 600s, 8.8%
|
512-size_4_4_4_i4096_r8.real-time.png |
-, 1001s, 14.9%
|
unsat, 421s, 18.6%
|
unsat, 373s, 12.3%
|
unsat, 406s, 8.0%
|
513-size_4_4_4_i4295_r8.real-time.png |
unsat, 959s, 14.5%
|
unsat, 335s, 22.0%
|
unsat, 152s, 11.9%
|
unsat, 119s, 8.8%
|
514-size_4_4_4_i4473_r8.real-time.png |
-, 1001s, 15.0%
|
unsat, 494s, 19.5%
|
unsat, 197s, 12.1%
|
unsat, 211s, 8.9%
|
515-size_4_4_4_i4828_r8.real-time.png |
-, 1001s, 16.0%
|
unsat, 626s, 17.9%
|
unsat, 465s, 13.3%
|
unsat, 593s, 9.3%
|
516-size_5_5_5_i003_r12.real-time.png |
-, 1001s, 19.3%
|
-, 1001s, 33.0%
|
-, 1001s, 24.2%
|
-, 1001s, 19.1%
|
517-size_5_5_5_i044_r12.real-time.png |
-, 1001s, 20.0%
|
-, 1001s, 39.8%
|
-, 1001s, 24.8%
|
-, 1001s, 20.1%
|
518-size_5_5_5_i063_r12.real-time.png |
-, 1001s, 18.4%
|
sat, 295s, 27.9%
|
-, 1001s, 19.1%
|
-, 1001s, 10.6%
|
519-size_5_5_5_i116_r12.real-time.png |
-, 1001s, 18.1%
|
-, 1001s, 30.6%
|
-, 1001s, 23.7%
|
-, 1001s, 12.6%
|
520-size_5_5_5_i171_r12.real-time.png |
-, 1001s, 19.1%
|
sat, 781s, 30.1%
|
-, 1001s, 23.5%
|
-, 1001s, 13.0%
|
521-size_5_5_5_i198_r12.real-time.png |
-, 1001s, 19.0%
|
-, 1001s, 39.0%
|
-, 1001s, 22.2%
|
-, 1001s, 10.5%
|
522-size_5_5_5_i218_r12.real-time.png |
-, 1001s, 18.1%
|
-, 1001s, 34.4%
|
-, 1001s, 24.4%
|
-, 1001s, 13.7%
|
523-size_5_5_5_i223_r12.real-time.png |
-, 1001s, 17.7%
|
-, 1001s, 28.6%
|
-, 1001s, 14.5%
|
-, 1001s, 7.2%
|
524-size_5_5_5_i235_r12.real-time.png |
-, 1001s, 19.1%
|
-, 1001s, 31.4%
|
-, 1001s, 19.1%
|
-, 1001s, 10.1%
|
525-size_5_5_5_i251_r12.real-time.png |
-, 1001s, 18.7%
|
-, 1001s, 28.6%
|
-, 1001s, 17.5%
|
-, 1001s, 16.5%
|
526-size_5_5_5_i260_r12.real-time.png |
-, 1001s, 19.6%
|
-, 1001s, 29.7%
|
sat, 444s, 15.9%
|
-, 1001s, 9.8%
|
527-size_5_5_5_i272_r12.real-time.png |
-, 1001s, 18.5%
|
-, 1001s, 30.3%
|
-, 1001s, 14.7%
|
-, 1001s, 12.2%
|
528-sha1r17m145ABCD.real-time.png |
sat, 161s, 15.2%
|
sat, 155s, 15.9%
|
-, 1001s, 13.2%
|
sat, 161s, 7.8%
|
529-sha1r17m145ABCD_p.real-time.png |
sat, 418s, 14.8%
|
sat, 231s, 15.6%
|
sat, 517s, 10.9%
|
sat, 243s, 7.2%
|
530-sha1r17m146ABCD.real-time.png |
-, 1001s, 14.3%
|
-, 1001s, 18.0%
|
sat, 455s, 8.3%
|
-, 1001s, 7.9%
|
531-sha1r17m146ABCD_p.real-time.png |
sat, 478s, 14.6%
|
-, 1001s, 18.3%
|
sat, 958s, 12.9%
|
sat, 260s, 6.8%
|
532-sha1r17m147ABCD.real-time.png |
sat, 788s, 13.9%
|
-, 1001s, 19.0%
|
-, 1001s, 9.1%
|
sat, 79s, 7.0%
|
533-sha1r17m147ABCD_p.real-time.png |
sat, 97s, 15.3%
|
sat, 600s, 16.5%
|
-, 1001s, 12.6%
|
sat, 0s, 8.3%
|
534-sha1r17m148ABCD.real-time.png |
sat, 94s, 13.0%
|
sat, 681s, 15.9%
|
-, 1001s, 13.8%
|
-, 1001s, 11.9%
|
535-sha1r17m148ABCD_p.real-time.png |
sat, 46s, 14.3%
|
-, 1001s, 16.4%
|
-, 1001s, 12.5%
|
-, 1001s, 6.0%
|
536-sha1r17m149ABCD.real-time.png |
-, 1001s, 13.3%
|
-, 1001s, 19.5%
|
-, 1001s, 12.7%
|
sat, 537s, 8.3%
|
537-sha1r17m149ABCD_p.real-time.png |
sat, 588s, 13.5%
|
-, 1001s, 18.9%
|
-, 1001s, 12.4%
|
sat, 302s, 7.3%
|
538-sha1r17m63a.real-time.png |
sat, 210s, 14.4%
|
sat, 370s, 18.4%
|
sat, 46s, 8.6%
|
sat, 354s, 9.8%
|
539-sha1r17m63a_p.real-time.png |
sat, 92s, 13.5%
|
sat, 457s, 18.1%
|
sat, 62s, 9.5%
|
sat, 130s, 9.6%
|
540-sha1r17m66a.real-time.png |
sat, 201s, 15.8%
|
sat, 899s, 22.2%
|
sat, 579s, 11.1%
|
sat, 737s, 8.8%
|
541-sha1r17m66a_p.real-time.png |
sat, 299s, 13.9%
|
sat, 86s, 17.4%
|
sat, 653s, 12.1%
|
sat, 571s, 6.7%
|
542-sha1r17m67a.real-time.png |
sat, 518s, 14.7%
|
sat, 931s, 22.4%
|
sat, 492s, 10.9%
|
sat, 788s, 7.4%
|
543-sha1r17m67a_p.real-time.png |
sat, 160s, 12.8%
|
sat, 539s, 20.3%
|
sat, 744s, 11.1%
|
sat, 698s, 8.6%
|
544-sha1r17m72a.real-time.png |
sat, 66s, 14.4%
|
sat, 452s, 18.8%
|
sat, 185s, 10.3%
|
sat, 630s, 8.7%
|
545-sha1r17m72a_p.real-time.png |
sat, 148s, 14.1%
|
sat, 165s, 17.8%
|
sat, 190s, 9.7%
|
sat, 604s, 8.7%
|
546-sha1r17m75a.real-time.png |
sat, 370s, 14.0%
|
sat, 950s, 23.0%
|
sat, 160s, 9.3%
|
sat, 230s, 7.9%
|
547-sha1r17m75a_p.real-time.png |
sat, 73s, 14.6%
|
sat, 74s, 19.2%
|
sat, 778s, 11.0%
|
sat, 482s, 6.8%
|
548-ASG_72_keystream76_1.real-time.png |
sat, 309s, 10.1%
|
sat, 472s, 34.0%
|
sat, 109s, 9.9%
|
sat, 212s, 18.4%
|
549-ASG_72_keystream76_2.real-time.png |
sat, 172s, 9.4%
|
sat, 269s, 29.3%
|
sat, 70s, 7.6%
|
sat, 148s, 14.6%
|
550-ASG_96_len112_known_last12_2.real-time.png |
sat, 671s, 7.6%
|
-, 1001s, 27.2%
|
sat, 428s, 8.2%
|
sat, 452s, 11.6%
|
551-ASG_96_len112_known_last12_2_u.real-time.png |
sat, 676s, 7.2%
|
-, 1001s, 27.2%
|
sat, 433s, 8.2%
|
sat, 496s, 14.3%
|
552-ASG_96_len112_known_last13_2.real-time.png |
sat, 71s, 9.0%
|
sat, 321s, 20.7%
|
sat, 573s, 9.1%
|
sat, 520s, 11.9%
|
553-ASG_96_len112_known_last13_2_u.real-time.png |
unsat, 423s, 8.8%
|
unsat, 421s, 23.3%
|
unsat, 370s, 6.8%
|
unsat, 383s, 12.5%
|
554-Grain_no_init_ver1_out200_known_last104_0.real-time.png |
sat, 4s, 10.3%
|
-, 1001s, 47.4%
|
sat, 680s, 13.8%
|
sat, 422s, 20.9%
|
555-Grain_no_init_ver1_out200_known_last104_0_u.real-time.png |
-, 1001s, 15.6%
|
-, 1001s, 47.6%
|
-, 1001s
|
-, 1001s, 19.6%
|
556-Grain_no_init_ver1_out200_known_last105_0.real-time.png |
sat, 216s, 15.5%
|
sat, 36s, 32.1%
|
sat, 676s, 13.4%
|
sat, 711s, 21.8%
|
557-Grain_no_init_ver1_out200_known_last105_0_u.real-time.png |
-, 1001s, 12.5%
|
unsat, 892s, 46.3%
|
unsat, 485s, 12.5%
|
unsat, 541s, 16.1%
|
558-MASG0_72_keystream76_0.real-time.png |
sat, 34s, 4.7%
|
sat, 566s, 30.4%
|
-, 1001s, 9.3%
|
-, 1001s, 21.2%
|
559-MASG_72_keystream76_0.real-time.png |
sat, 75s, 6.1%
|
sat, 2s, 15.7%
|
sat, 916s, 11.5%
|
-, 1001s, 23.9%
|
560-Mickey_out250_known_last146_0.real-time.png |
sat, 239s, 26.6%
|
sat, 222s, 43.4%
|
-, 1001s, 19.0%
|
sat, 163s, 13.9%
|
561-Mickey_out250_known_last146_0_u.real-time.png |
unsat, 565s, 33.4%
|
-, 1001s, 36.7%
|
-, 1001s, 19.6%
|
unsat, 613s, 12.3%
|
562-Mickey_out250_known_last147_0.real-time.png |
sat, 632s, 40.0%
|
sat, 799s, 37.1%
|
sat, 447s, 17.7%
|
sat, 493s, 12.8%
|
563-Mickey_out250_known_last147_0_u.real-time.png |
unsat, 407s, 33.2%
|
unsat, 201s, 53.9%
|
unsat, 476s, 12.2%
|
unsat, 201s, 13.2%
|
564-Trivium_no_init_out350_known_last142_1.real-time.png |
-, 1001s, 14.6%
|
-, 1001s, 22.2%
|
-, 1001s, 14.1%
|
-, 1001s, 10.8%
|
565-Trivium_no_init_out350_known_last142_1_u.real-time.png |
-, 1001s, 14.7%
|
-, 1001s, 21.7%
|
-, 1001s, 17.8%
|
-, 1001s, 16.2%
|
566-Trivium_no_init_out350_known_last143_1.real-time.png |
-, 1001s, 15.6%
|
-, 1001s, 21.6%
|
sat, 312s, 14.4%
|
-, 1001s, 14.3%
|
567-Trivium_no_init_out350_known_last143_1_u.real-time.png |
-, 1001s, 14.7%
|
-, 1001s, 43.2%
|
unsat, 873s, 21.3%
|
unsat, 902s, 17.0%
|
568-Bibd-sc-10-03-08_c18.real-time.png |
sat, 2s, 13.0%
|
sat, 8s, 22.3%
|
sat, 6s, 8.8%
|
sat, 8s, 6.7%
|
569-CarSequencing-90-01_c18.real-time.png |
sat, 41s, 23.7%
|
sat, 128s, 34.3%
|
sat, 112s, 8.3%
|
sat, 95s, 7.0%
|
570-CarSequencing-90-02_c18.real-time.png |
sat, 27s, 24.9%
|
sat, 100s, 33.5%
|
sat, 79s, 8.9%
|
sat, 57s, 6.3%
|
571-Eternity-10-05_c18.real-time.png |
sat, 14s, 8.0%
|
sat, 26s, 15.2%
|
sat, 8s, 11.5%
|
sat, 41s, 7.0%
|
572-Eternity-10-06_c18.real-time.png |
sat, 573s, 11.0%
|
-, 1001s, 20.8%
|
-, 1001s, 20.3%
|
sat, 440s, 6.7%
|
573-GracefulGraph-K04-P04_c18.real-time.png |
sat, 25s, 11.9%
|
sat, 44s, 19.6%
|
sat, 20s, 12.2%
|
sat, 26s, 11.1%
|
574-GracefulGraph-K05-P02_c18.real-time.png |
sat, 40s, 12.3%
|
sat, 30s, 14.2%
|
sat, 104s, 10.5%
|
sat, 6s, 7.9%
|
575-Haystacks-ext-12_c18.real-time.png |
-, 1001s, 41.4%
|
-, 1001s, 39.4%
|
-, 1001s, 42.8%
|
-, 1001s, 19.5%
|
576-Haystacks-ext-13_c18.real-time.png |
-, 1001s, 42.1%
|
-, 1001s, 49.5%
|
-, 1001s, 33.0%
|
-, 1001s, 21.9%
|
577-Mario-t-hard-2_c18.real-time.png |
sat, 2s, 10.6%
|
sat, 29s, 35.7%
|
sat, 28s, 5.4%
|
sat, 28s, 5.8%
|
578-Mario-t-hard-5_c18.real-time.png |
sat, 2s, 10.5%
|
sat, 25s, 36.9%
|
sat, 27s, 5.3%
|
sat, 26s, 4.8%
|
579-Pb-chnl15-16_c18.real-time.png |
-, 1001s, 34.7%
|
-, 1001s, 35.8%
|
-, 1001s, 27.7%
|
-, 1001s, 13.5%
|
580-Pb-chnl20-21_c18.real-time.png |
-, 1001s, 44.6%
|
-, 1001s, 55.3%
|
-, 1001s, 26.6%
|
-, 1001s, 22.9%
|
581-QuasiGroup-4-10_c18.real-time.png |
-, 1001s, 19.1%
|
-, 1001s, 11.5%
|
-, 1001s, 9.3%
|
-, 1001s, 5.7%
|
582-QuasiGroup-4-12_c18.real-time.png |
-, 1001s, 13.3%
|
sat, 755s, 11.8%
|
sat, 555s, 7.2%
|
sat, 899s, 4.1%
|
583-SocialGolfers-6-6-6-cp_c18.real-time.png |
-, 1001s, 19.7%
|
-, 1001s, 19.2%
|
-, 1001s, 9.8%
|
-, 1001s, 9.7%
|
584-SocialGolfers-6-6-7-cp_c18.real-time.png |
-, 1001s, 22.6%
|
-, 1001s, 18.2%
|
-, 1001s, 10.5%
|
-, 1001s, 8.9%
|
585-Subisomorphism-g10-g23_c18.real-time.png |
-, 1001s, 46.5%
|
-, 1001s, 20.0%
|
-, 1001s, 13.1%
|
-, 1001s, 10.5%
|
586-Subisomorphism-g10-g27_c18.real-time.png |
sat, 171s, 35.5%
|
sat, 424s, 23.0%
|
sat, 667s, 13.9%
|
sat, 132s, 10.7%
|
587-Tal-07_c18.real-time.png |
sat, 30s, 33.8%
|
sat, 16s, 36.1%
|
sat, 10s, 31.6%
|
sat, 21s, 26.0%
|
588-Tal-08_c18.real-time.png |
sat, 81s, 40.9%
|
sat, 41s, 41.9%
|
sat, 38s, 36.4%
|
sat, 34s, 26.9%
|
589-frb-40-19-1-mgd_c18.real-time.png |
sat, 5s, 11.6%
|
sat, 1s, 13.3%
|
sat, 5s, 8.7%
|
sat, 1s, 4.9%
|
590-knight_14.real-time.png |
-, 1001s, 20.7%
|
-, 1001s, 27.8%
|
-, 1001s, 17.3%
|
-, 1001s, 7.2%
|
591-knight_16.real-time.png |
sat, 127s, 11.1%
|
sat, 327s, 33.3%
|
sat, 171s, 16.9%
|
sat, 146s, 8.5%
|
592-knight_18.real-time.png |
sat, 314s, 12.6%
|
-, 1001s, 35.2%
|
-, 1001s, 20.3%
|
-, 1001s, 10.1%
|
593-knight_20.real-time.png |
sat, 847s, 14.5%
|
-, 1001s, 33.3%
|
-, 1001s, 21.6%
|
-, 1001s, 10.0%
|
594-b1904P1-8x8c6h5SAT.real-time.png |
-, 1001s, 10.8%
|
-, 1001s, 20.2%
|
-, 1001s, 15.0%
|
-, 1001s, 8.2%
|
595-b1904P1-8x8c6h7SAT.real-time.png |
-, 1001s, 11.2%
|
-, 1001s, 21.5%
|
-, 1001s, 9.1%
|
-, 1001s, 8.7%
|
596-b1904P2-8x8c9h5SAT.real-time.png |
-, 1001s, 12.6%
|
-, 1001s, 20.7%
|
-, 1001s, 9.6%
|
-, 1001s, 7.5%
|
597-b1904P2-8x8c9h7UNSAT.real-time.png |
-, 1001s, 13.1%
|
-, 1001s, 17.9%
|
-, 1001s, 9.7%
|
-, 1001s, 6.4%
|
598-b1904P3-8x8c11h0SAT.real-time.png |
-, 1001s, 10.1%
|
-, 1001s, 19.5%
|
-, 1001s, 11.6%
|
-, 1001s, 7.1%
|
599-b1904P3-8x8c11h7SAT.real-time.png |
-, 1001s, 11.8%
|
-, 1001s, 17.8%
|
-, 1001s, 10.3%
|
-, 1001s, 7.4%
|
600-b1904P3-8x8c11h7UNSAT.real-time.png |
-, 1001s, 12.7%
|
unsat, 810s, 15.8%
|
unsat, 571s, 7.7%
|
unsat, 808s, 4.9%
|
601-001-80-12-sc2014.real-time.png |
-, 1001s, 42.3%
|
-, 1001s, 44.8%
|
sat, 815s, 18.3%
|
-, 1001s, 9.8%
|
602-002-80-8-sc2014.real-time.png |
-, 1001s, 40.9%
|
sat, 856s, 42.0%
|
sat, 519s, 17.3%
|
sat, 191s, 9.2%
|
603-002-sc2013.real-time.png |
sat, 224s, 20.6%
|
-, 1001s, 26.1%
|
-, 1001s, 20.4%
|
-, 1001s, 11.0%
|
604-003-sc2013.real-time.png |
-, 1001s, 16.3%
|
-, 1001s, 25.1%
|
-, 1001s, 18.1%
|
-, 1001s, 11.2%
|
605-004-22-160-sc2014.real-time.png |
-, 1001s, 19.4%
|
-, 1001s, 29.4%
|
-, 1001s, 20.6%
|
-, 1001s, 11.8%
|
606-004-80-8-sc2014.real-time.png |
sat, 544s, 33.8%
|
sat, 245s, 30.8%
|
sat, 545s, 16.7%
|
sat, 176s, 11.2%
|
607-004-sc2013.real-time.png |
sat, 506s, 16.8%
|
-, 1001s, 25.8%
|
sat, 900s, 20.7%
|
sat, 228s, 9.6%
|
608-006-23-96-sc2014.real-time.png |
-, 1001s, 16.1%
|
-, 1001s, 24.4%
|
-, 1001s, 21.1%
|
-, 1001s, 7.6%
|
609-007-sc2013.real-time.png |
-, 1001s, 18.8%
|
-, 1001s, 24.4%
|
-, 1001s, 20.5%
|
sat, 254s, 12.2%
|
610-008-80-8-sc2014.real-time.png |
-, 1001s, 37.5%
|
sat, 801s, 42.0%
|
sat, 433s, 19.0%
|
sat, 544s, 10.0%
|
611-11pipe_11_ooo-sc2011.real-time.png |
-, 1001s, 13.1%
|
-, 1001s, 26.7%
|
-, 1001s, 18.2%
|
-, 1001s, 14.4%
|
612-20180322_164224543_p_cnf_320_1120-sc2018.real-time.png |
-, 1001s, 9.9%
|
-, 1001s, 46.6%
|
-, 1001s, 26.1%
|
-, 1001s, 20.2%
|
613-20180326_095804936_p_cnf_320_1120-sc2018.real-time.png |
sat, 992s, 9.8%
|
-, 1001s, 46.1%
|
-, 1001s, 26.1%
|
-, 1001s, 8.3%
|
614-24.4-sc2017.real-time.png |
-, 1001s, 20.7%
|
-, 1001s, 24.0%
|
-, 1001s, 19.2%
|
-, 1001s, 10.1%
|
615-26_stack_cas_longest_true-unreach-call.i-cbmc-u2-sc2016.real-time.png |
-, 52s
|
sat, 82s, 0.0%
|
sat, 83s, 0.0%
|
sat, 77s, 0.0%
|
616-289-unsat-21x14-sc2011.real-time.png |
-, 1001s, 22.5%
|
-, 1001s, 34.4%
|
-, 1001s, 16.1%
|
-, 1001s, 14.9%
|
617-58bits_13.dimacs-sr2015.real-time.png |
-, 1001s, 23.5%
|
-, 1001s, 30.5%
|
-, 1001s, 13.9%
|
-, 1001s, 9.3%
|
618-6-4-6-sc2018.real-time.png |
-, 1001s, 17.8%
|
-, 1001s, 18.6%
|
-, 1001s, 11.8%
|
-, 1001s, 9.4%
|
619-62bits_14.dimacs-sr2015.real-time.png |
-, 1001s, 23.2%
|
-, 1001s, 25.8%
|
-, 1001s, 13.3%
|
-, 1001s, 9.6%
|
620-6s126-opt-sc2014.real-time.png |
-, 1001s, 8.7%
|
-, 1001s, 25.7%
|
-, 1001s, 11.3%
|
-, 1001s, 7.5%
|
621-6s133-sc2014.real-time.png |
-, 1001s, 22.4%
|
unsat, 168s, 30.4%
|
unsat, 158s, 20.9%
|
unsat, 138s, 9.4%
|
622-6s139-sc2013.real-time.png |
-, 1001s, 33.8%
|
-, 1001s, 52.6%
|
-, 1001s, 6.8%
|
-, 1001s, 6.6%
|
623-6s166-sc2013.real-time.png |
-, 1001s, 13.9%
|
unsat, 69s, 28.1%
|
unsat, 18s, 11.0%
|
unsat, 37s, 10.3%
|
624-6s169-opt-sc2014.real-time.png |
-, 1001s, 19.5%
|
unsat, 48s, 25.7%
|
unsat, 76s, 15.0%
|
unsat, 24s, 9.6%
|
625-6s20-sc2013.real-time.png |
-, 1001s, 18.7%
|
unsat, 898s, 22.4%
|
unsat, 865s, 11.1%
|
unsat, 852s, 5.3%
|
626-9_50-sc2017.real-time.png |
sat, 32s, 18.9%
|
-, 1001s, 28.5%
|
-, 1001s, 13.5%
|
sat, 485s, 9.5%
|
627-9dlx_vliw_at_b_iq8-sc2007.real-time.png |
-, 1001s, 25.4%
|
-, 1001s, 33.5%
|
-, 1001s, 14.2%
|
-, 1001s, 14.3%
|
628-9pipe_k-sc2012.real-time.png |
unsat, 675s, 22.0%
|
unsat, 147s, 25.5%
|
unsat, 143s, 24.1%
|
unsat, 97s, 17.3%
|
629-ACG-20-10p1-sc2009.real-time.png |
-, 1001s, 15.6%
|
-, 1001s, 14.1%
|
sat, 983s, 10.5%
|
-, 1001s, 6.6%
|
630-AProVE07-26-sc2007.real-time.png |
-, 1001s, 24.0%
|
-, 1001s, 41.6%
|
-, 1001s, 36.8%
|
-, 1001s, 27.7%
|
631-EDP3-70000-sc2014.real-time.png |
-, 1001s, 14.6%
|
-, 1001s, 20.3%
|
-, 1001s, 5.2%
|
-, 1001s, 8.0%
|
632-IBM_FV_20002_31_1_rule_1_SAT_dat.k95-sc2007.real-time.png |
-, 1001s, 19.9%
|
-, 1001s, 28.3%
|
-, 1001s, 10.5%
|
-, 1001s, 9.3%
|
633-IBM_FV_2004_rule_batch_2_31_2_SAT_dat.k45.debugged-sc2012.real-time.png |
-, 1001s, 14.8%
|
-, 1001s, 19.8%
|
-, 1001s, 8.5%
|
-, 1001s, 5.8%
|
634-LABS_n066_goal005-sc2013.real-time.png |
-, 1001s, 14.7%
|
sat, 160s, 12.7%
|
-, 1001s, 6.9%
|
-, 1001s, 4.5%
|
635-LABS_n071_goal001-sc2013.real-time.png |
-, 1001s, 9.7%
|
-, 1001s, 14.7%
|
-, 1001s, 6.1%
|
-, 1001s, 6.3%
|
636-LABS_n087_goal008-sc2013.real-time.png |
-, 1001s, 27.4%
|
sat, 612s, 15.3%
|
-, 1001s, 10.4%
|
sat, 239s, 9.0%
|
637-LABS_n089_goal008-sc2013.real-time.png |
-, 1001s, 25.5%
|
-, 1001s, 18.7%
|
-, 1001s, 7.0%
|
-, 1001s, 4.0%
|
638-MD5-29-4-sc2014.real-time.png |
-, 1001s, 15.0%
|
-, 1001s, 16.6%
|
-, 1001s, 7.0%
|
-, 1001s, 6.2%
|
639-MD5-29-5-sc2014.real-time.png |
-, 1001s, 14.3%
|
-, 1001s, 15.7%
|
-, 1001s, 8.6%
|
-, 1001s, 5.7%
|
640-MUS-v310-4-sc2013.real-time.png |
unsat, 324s, 8.5%
|
unsat, 931s, 44.7%
|
unsat, 461s, 13.4%
|
unsat, 508s, 10.6%
|
641-Nb51T6-sc2018.real-time.png |
-, 1001s, 26.2%
|
-, 1001s, 35.1%
|
-, 1001s, 17.5%
|
-, 1001s, 34.8%
|
642-Nb7T44-sc2017.real-time.png |
-, 1001s, 20.5%
|
-, 1001s, 32.8%
|
-, 1001s, 32.4%
|
-, 1001s, 11.4%
|
643-QG7a-gensys-icl001.sat05-3822.reshuffled-07-sc2007.real-time.png |
unsat, 380s, 16.5%
|
unsat, 65s, 13.1%
|
unsat, 64s, 7.6%
|
unsat, 58s, 5.3%
|
644-QG7a-gensys-ukn002.sat05-3842.reshuffled-07-sc2007.real-time.png |
-, 1001s, 20.3%
|
unsat, 594s, 13.2%
|
unsat, 616s, 8.6%
|
unsat, 546s, 5.7%
|
645-SAT_dat.k100-sc2012.real-time.png |
-, 1001s, 16.0%
|
unsat, 372s, 30.8%
|
unsat, 347s, 8.9%
|
unsat, 319s, 10.2%
|
646-SAT_dat.k85-sc2013.real-time.png |
-, 1001s, 20.7%
|
-, 1001s, 35.2%
|
-, 1001s, 11.0%
|
-, 1001s, 12.5%
|
647-SGI_30_60_24_40_2-dir.shuffled-as.sat03-118-sc2002.real-time.png |
-, 1001s, 27.1%
|
-, 1001s, 22.4%
|
-, 1001s, 14.5%
|
-, 1001s, 7.6%
|
648-SGI_30_60_28_40_2-dir.shuffled-as.sat03-124-sc2002.real-time.png |
-, 1001s, 29.2%
|
-, 1001s, 20.2%
|
-, 1001s, 14.4%
|
-, 1001s, 8.6%
|
649-Schur_160_5_d38-sc2016.real-time.png |
-, 1001s, 28.1%
|
-, 1001s, 24.2%
|
-, 1001s, 17.9%
|
-, 1001s, 9.1%
|
650-Schur_161_5_d22-sc2016.real-time.png |
-, 1001s, 24.0%
|
-, 1001s, 19.4%
|
-, 1001s, 15.6%
|
-, 1001s, 10.0%
|
651-T103.2.1-sc2017.real-time.png |
-, 1001s, 38.0%
|
-, 1001s, 51.1%
|
-, 1001s, 13.9%
|
-, 1001s, 19.9%
|
652-T169.1.0-sc2017.real-time.png |
-, 1001s, 39.1%
|
-, 1001s, 50.9%
|
-, 1001s, 7.0%
|
-, 1001s, 9.9%
|
653-TimetableCNFEncoding_5_UNKNOWN-sc2018.real-time.png |
-, 1001s, 17.1%
|
-, 1001s, 47.0%
|
-, 1001s, 48.5%
|
-, 1001s, 20.1%
|
654-UCG-20-10p1-sc2009.real-time.png |
-, 1001s, 14.4%
|
-, 1001s, 15.2%
|
sat, 481s, 11.6%
|
sat, 867s, 7.5%
|
655-UR-20-5p1-sc2009.real-time.png |
-, 1001s, 12.2%
|
sat, 362s, 18.4%
|
sat, 403s, 11.6%
|
sat, 408s, 9.5%
|
656-UTI-20-10p0-sc2009.real-time.png |
-, 1001s, 18.4%
|
unsat, 335s, 25.2%
|
unsat, 300s, 15.6%
|
unsat, 308s, 10.7%
|
657-UTI-20-10p1-sc2009.real-time.png |
-, 1001s, 20.6%
|
sat, 798s, 26.6%
|
sat, 750s, 16.6%
|
sat, 747s, 11.3%
|
658-UTI-20-5p0-sc2009.real-time.png |
-, 1001s, 14.4%
|
unsat, 321s, 22.5%
|
unsat, 463s, 15.0%
|
unsat, 396s, 9.3%
|
659-aaai10-planning-ipc5-TPP-21-step11-sc2011.real-time.png |
-, 1001s, 10.4%
|
unsat, 704s, 13.7%
|
unsat, 678s, 13.8%
|
unsat, 668s, 8.3%
|
660-aaai10-planning-ipc5-pathways-17-step21-sc2011.real-time.png |
-, 1001s, 17.9%
|
sat, 572s, 21.6%
|
sat, 593s, 22.6%
|
-, 1001s, 10.3%
|
661-ablmulub16x4o-sc2016.real-time.png |
unsat, 269s, 13.1%
|
unsat, 396s, 21.4%
|
unsat, 439s, 10.9%
|
unsat, 368s, 7.5%
|
662-ablmulub2x32o-sc2016.real-time.png |
unsat, 317s, 13.1%
|
unsat, 911s, 24.9%
|
unsat, 805s, 15.3%
|
unsat, 695s, 7.3%
|
663-ae_rphp095_04-sc2018.real-time.png |
-, 1001s, 27.2%
|
-, 1001s, 37.7%
|
-, 1001s, 32.6%
|
-, 1001s, 24.1%
|
664-aes_24_4_keyfind_2-sc2013.real-time.png |
sat, 263s, 22.6%
|
-, 1001s, 18.4%
|
-, 1001s, 14.1%
|
-, 1001s, 11.6%
|
665-aes_24_4_keyfind_5-sc2014.real-time.png |
-, 1001s, 23.3%
|
-, 1001s, 34.3%
|
-, 1001s, 12.9%
|
-, 1001s, 7.9%
|
666-aes_32_3_keyfind_1-sc2011.real-time.png |
sat, 189s, 10.9%
|
-, 1001s, 47.2%
|
sat, 245s, 20.1%
|
sat, 925s, 21.7%
|
667-aes_equiv_encry_3_rounds.debugged-sc2012.real-time.png |
-, 1001s, 28.6%
|
unsat, 134s, 36.0%
|
unsat, 118s, 18.8%
|
unsat, 111s, 14.4%
|
668-ak128astepbg2msaig-sc2016.real-time.png |
-, 1001s, 44.3%
|
-, 1001s, 38.7%
|
-, 1001s, 8.7%
|
-, 1001s, 9.3%
|
669-ak128modasbg2asisc-sc2016.real-time.png |
-, 1001s, 36.7%
|
-, 1001s, 39.4%
|
-, 1001s, 11.5%
|
-, 1001s, 9.7%
|
670-apn-sbox6-cut4-helpbox31-sc2018.real-time.png |
-, 1001s, 23.2%
|
sat, 573s, 15.3%
|
sat, 166s, 6.9%
|
sat, 313s, 6.2%
|
671-atco_enc1_opt1_04_32-sc2014.real-time.png |
-, 1001s, 8.3%
|
sat, 479s, 13.9%
|
sat, 424s, 6.9%
|
sat, 661s, 4.9%
|
672-atco_enc1_opt2_10_16-sc2014.real-time.png |
sat, 890s, 19.0%
|
-, 1001s, 19.2%
|
-, 1001s, 12.7%
|
-, 1001s, 6.2%
|
673-atco_enc1_opt2_20_12-sc2014.real-time.png |
-, 1001s, 21.6%
|
-, 1001s, 25.2%
|
unsat, 989s, 17.7%
|
unsat, 946s, 6.6%
|
674-atco_enc2_opt2_05_9-sc2014.real-time.png |
sat, 118s, 11.4%
|
sat, 551s, 24.0%
|
sat, 710s, 14.5%
|
sat, 324s, 12.3%
|
675-atco_enc2_opt2_10_21-sc2014.real-time.png |
sat, 412s, 21.9%
|
-, 1001s, 26.8%
|
sat, 330s, 17.9%
|
sat, 684s, 17.2%
|
676-atco_enc3_opt2_10_12-sc2014.real-time.png |
unsat, 992s, 16.0%
|
-, 1001s, 27.4%
|
unsat, 992s, 10.4%
|
unsat, 847s, 13.6%
|
677-b04_s_2_unknown_pre-sc2013.real-time.png |
-, 1001s, 12.7%
|
-, 1001s, 14.9%
|
-, 1001s, 6.0%
|
-, 1001s, 5.1%
|
678-b04_s_unknown-sc2013.real-time.png |
-, 1001s, 8.1%
|
-, 1001s, 17.7%
|
-, 1001s, 5.2%
|
-, 1001s, 4.8%
|
679-b_unsat-sc2013.real-time.png |
unsat, 518s, 13.0%
|
unsat, 467s, 12.8%
|
unsat, 520s, 7.9%
|
unsat, 403s, 5.3%
|
680-blockpuzzle_5x10_s3_free4-sc2017.real-time.png |
-, 1001s, 24.7%
|
unsat, 251s, 18.7%
|
unsat, 295s, 16.2%
|
unsat, 225s, 6.8%
|
681-blocks-blocks-36-0.120-NOTKNOWN-sc2011.real-time.png |
unsat, 939s, 22.2%
|
unsat, 724s, 28.3%
|
unsat, 654s, 28.4%
|
unsat, 676s, 12.8%
|
682-blocks-blocks-37-1.130-NOTKNOWN-sc2011.real-time.png |
unsat, 479s, 28.2%
|
unsat, 548s, 35.8%
|
unsat, 479s, 33.2%
|
unsat, 340s, 21.4%
|
683-bob12s06-sc2013.real-time.png |
-, 1001s, 6.5%
|
-, 1001s, 29.8%
|
-, 1001s, 6.9%
|
-, 1001s, 6.9%
|
684-c6288mul.miter.shuffled-as.sat03-346-sc2002.real-time.png |
-, 1001s, 20.3%
|
unsat, 105s, 30.0%
|
unsat, 76s, 9.7%
|
unsat, 89s, 8.8%
|
685-cms-scheel-md5-families-r24-c8-p0-3-5-6-14-16-18-19-sc2018.real-time.png |
-, 1001s, 21.4%
|
-, 1001s, 33.1%
|
-, 1001s, 14.6%
|
-, 1001s, 6.8%
|
686-connm-ue-csp-sat-n800-d0.02-s111845174.used-as.sat04-958-sc2011.real-time.png |
-, 1001s, 11.1%
|
-, 1001s, 44.3%
|
-, 1001s, 19.2%
|
-, 1001s, 18.3%
|
687-countbitsrotate032-sc2009.real-time.png |
-, 1001s, 5.0%
|
-, 1001s, 20.6%
|
-, 1001s, 13.0%
|
-, 1001s, 9.6%
|
688-countbitssrl032-sc2009.real-time.png |
-, 1001s, 18.6%
|
unsat, 139s, 19.1%
|
unsat, 157s, 9.6%
|
unsat, 184s, 7.8%
|
689-countbitswegner128-sc2011.real-time.png |
-, 1001s, 28.5%
|
-, 1001s, 28.4%
|
-, 1001s, 14.4%
|
-, 1001s, 8.4%
|
690-course0.2_2018_3-sc2018.real-time.png |
-, 1001s, 35.4%
|
-, 1001s, 51.2%
|
-, 1001s, 7.8%
|
-, 1001s, 10.3%
|
691-crafted_n11_d6_c3_num24-sc2013.real-time.png |
-, 1001s, 20.0%
|
-, 1001s, 23.2%
|
-, 1001s, 23.4%
|
-, 1001s, 22.1%
|
692-ctl_4291_567_2_unsat-sc2013.real-time.png |
unsat, 486s, 13.4%
|
unsat, 451s, 18.1%
|
unsat, 375s, 8.4%
|
unsat, 397s, 6.4%
|
693-ctl_4291_567_2_unsat_pre-sc2013.real-time.png |
unsat, 579s, 12.5%
|
unsat, 505s, 13.9%
|
unsat, 461s, 8.4%
|
unsat, 474s, 6.3%
|
694-ctl_4291_567_5_unsat_pre-sc2014.real-time.png |
-, 1001s, 9.8%
|
-, 1001s, 22.0%
|
-, 1001s, 8.1%
|
-, 1001s, 7.7%
|
695-custmulsb2x32o-sc2016.real-time.png |
-, 1001s, 13.4%
|
-, 1001s, 25.8%
|
-, 1001s, 11.4%
|
-, 1001s, 8.8%
|
696-custmulun16x16o-sc2016.real-time.png |
-, 1001s, 15.0%
|
-, 1001s, 22.2%
|
-, 1001s, 13.2%
|
-, 1001s, 7.2%
|
697-dist6.c-sc2018.real-time.png |
-, 1001s, 15.6%
|
unsat, 238s, 16.7%
|
unsat, 205s, 8.0%
|
unsat, 222s, 6.6%
|
698-dp12u11.used-as.sat04-358-sc2004.real-time.png |
unsat, 197s, 10.5%
|
unsat, 129s, 15.0%
|
unsat, 178s, 8.9%
|
unsat, 148s, 6.4%
|
699-e_rphp035_05-sc2018.real-time.png |
unsat, 795s, 21.6%
|
unsat, 394s, 26.5%
|
unsat, 348s, 17.9%
|
unsat, 328s, 9.6%
|
700-ecarev-110-1031-23-40-8-sc2018.real-time.png |
-, 1001s, 27.1%
|
sat, 920s, 32.4%
|
-, 1001s, 21.0%
|
sat, 827s, 12.4%
|
701-edges-024-4-5613555-1-00-sc2014.real-time.png |
-, 1001s, 9.7%
|
-, 1001s, 47.3%
|
-, 1001s, 23.6%
|
-, 1001s, 7.8%
|
702-ex051_9-sc2018.real-time.png |
-, 1001s, 17.8%
|
-, 1001s, 19.7%
|
-, 1001s, 10.1%
|
-, 1001s, 4.9%
|
703-ex145_11-sc2018.real-time.png |
-, 1001s, 18.2%
|
-, 1001s, 21.9%
|
-, 1001s, 11.5%
|
-, 1001s, 6.3%
|
704-ex175_17-sc2018.real-time.png |
-, 1001s, 11.7%
|
-, 1001s, 21.1%
|
-, 1001s, 11.3%
|
-, 1001s, 8.3%
|
705-ex175_18-sc2018.real-time.png |
-, 1001s, 15.3%
|
-, 1001s, 21.4%
|
-, 1001s, 11.7%
|
-, 1001s, 8.5%
|
706-ezfact64_6.shuffled-as.sat03-1522-sc2002.real-time.png |
-, 1001s, 12.4%
|
sat, 393s, 15.0%
|
sat, 754s, 7.8%
|
sat, 807s, 6.4%
|
707-ezfact64_8.shuffled-as.sat03-1524-sc2002.real-time.png |
-, 1001s, 12.8%
|
sat, 757s, 16.2%
|
sat, 865s, 12.4%
|
sat, 730s, 6.6%
|
708-f10nidw-sc2012.real-time.png |
-, 1001s, 24.6%
|
unsat, 627s, 41.2%
|
unsat, 558s, 13.3%
|
unsat, 469s, 11.0%
|
709-f6nidw-sc2012.real-time.png |
unsat, 15s, 18.9%
|
unsat, 6s, 38.2%
|
unsat, 5s, 11.0%
|
unsat, 4s, 6.4%
|
710-frb59-26-1.used-as.sat04-891-sc2011.real-time.png |
-, 1001s, 23.5%
|
-, 1001s, 16.0%
|
-, 1001s, 11.4%
|
-, 1001s, 6.6%
|
711-gensys-icl005.shuffled-as.sat05-3826-sc2011.real-time.png |
-, 1001s, 18.8%
|
unsat, 428s, 12.8%
|
unsat, 431s, 8.1%
|
unsat, 378s, 5.1%
|
712-gss-20-s100-sc2009.real-time.png |
sat, 725s, 12.4%
|
sat, 358s, 13.3%
|
-, 1001s, 8.5%
|
-, 1001s, 7.4%
|
713-gss-33-s100-sc2009.real-time.png |
-, 1001s, 10.8%
|
-, 1001s, 14.7%
|
-, 1001s, 10.8%
|
-, 1001s, 5.5%
|
714-gto_p60c238-sc2018.real-time.png |
unsat, 462s, 15.1%
|
unsat, 786s, 24.7%
|
unsat, 409s, 19.5%
|
unsat, 548s, 21.7%
|
715-gus-md5-14-sc2009.real-time.png |
-, 1001s, 14.0%
|
-, 1001s, 14.9%
|
-, 1001s, 8.8%
|
-, 1001s, 6.1%
|
716-hitag2-8-60-0-0x880693399044612-25-SAT-sc2013.real-time.png |
-, 1001s, 12.8%
|
-, 1001s, 37.3%
|
-, 1001s, 13.8%
|
-, 1001s, 11.7%
|
717-hwb-n26-01-S1957858365.shuffled-as.sat03-1622-sc2002.real-time.png |
unsat, 614s, 10.0%
|
-, 1001s, 50.5%
|
unsat, 775s, 25.3%
|
unsat, 599s, 14.2%
|
718-hwb-n26-03-S540351185.sat05-490.reshuffled-07-sc2007.real-time.png |
-, 1001s, 9.6%
|
-, 1001s, 51.9%
|
-, 1001s, 26.8%
|
unsat, 802s, 11.7%
|
719-hwmcc10-timeframe-expansion-k45-pdtpmspalu-tseitin-sc2011.real-time.png |
-, 1001s, 20.2%
|
-, 1001s, 31.2%
|
-, 1001s, 17.1%
|
-, 1001s, 8.8%
|
720-hwmcc15deep-6s516r-k18-sc2017.real-time.png |
-, 1001s, 12.2%
|
-, 1001s, 31.5%
|
-, 1001s, 15.7%
|
-, 1001s, 12.1%
|
721-hwmcc15deep-oski15a10b10s-k22-sc2017.real-time.png |
-, 1001s, 14.9%
|
-, 1001s, 32.1%
|
-, 1001s, 9.8%
|
-, 1001s, 6.0%
|
722-jgiraldezlevy.2200.9086.08.40.149-sr2015.real-time.png |
-, 1001s, 12.1%
|
-, 1001s, 16.5%
|
-, 1001s, 14.4%
|
sat, 829s, 10.8%
|
723-k_unsat-sc2013.real-time.png |
-, 1001s, 19.3%
|
-, 1001s, 18.4%
|
-, 1001s, 11.2%
|
-, 1001s, 5.5%
|
724-le450_15b.col.15-sc2018.real-time.png |
-, 1001s, 45.9%
|
-, 1001s, 32.5%
|
-, 1001s, 21.5%
|
-, 1001s, 12.9%
|
725-li-exam-63.shuffled-as.sat03-368-sc2002.real-time.png |
-, 1001s, 17.5%
|
-, 1001s, 27.0%
|
-, 1001s, 15.4%
|
-, 1001s, 9.8%
|
726-li-test4-99.shuffled-as.sat03-377-sc2002.real-time.png |
-, 1001s, 15.7%
|
-, 1001s, 25.0%
|
-, 1001s, 11.7%
|
-, 1001s, 7.7%
|
727-manthey_DimacsSorter_37_3-sr2015.real-time.png |
-, 1001s, 10.8%
|
-, 1001s, 18.2%
|
-, 1001s, 13.2%
|
-, 1001s, 7.7%
|
728-manthey_single-ordered-initialized-w50-b7-sr2015.real-time.png |
unsat, 522s, 10.1%
|
unsat, 455s, 12.2%
|
unsat, 476s, 7.8%
|
unsat, 434s, 5.3%
|
729-maxxor032-sc2011.real-time.png |
-, 1001s, 21.2%
|
unsat, 41s, 20.1%
|
unsat, 49s, 9.8%
|
unsat, 44s, 7.7%
|
730-minxorminand128-sc2009.real-time.png |
-, 1001s, 14.5%
|
-, 1001s, 31.9%
|
-, 1001s, 30.1%
|
-, 1001s, 16.9%
|
731-mod2c-3cage-unsat-10-2.sat05-2567.reshuffled-07-sc2007.real-time.png |
-, 1001s, 14.9%
|
unsat, 359s, 41.2%
|
unsat, 674s, 28.7%
|
unsat, 587s, 16.0%
|
732-mod2c-3cage-unsat-10-3.sat05-2568.reshuffled-07-sc2007.real-time.png |
-, 1001s, 14.6%
|
unsat, 558s, 54.2%
|
unsat, 269s, 26.5%
|
unsat, 144s, 13.7%
|
733-mod4block_2vars_10gates_u2_autoenc-sc2009.real-time.png |
sat, 165s, 23.8%
|
-, 1001s, 29.0%
|
sat, 465s, 16.6%
|
sat, 485s, 7.7%
|
734-mrpp_6x6#12_24-sc2013.real-time.png |
sat, 33s, 19.6%
|
sat, 52s, 26.1%
|
sat, 25s, 8.8%
|
sat, 51s, 8.6%
|
735-mrpp_8x8#20_24-sc2014.real-time.png |
-, 1001s, 19.9%
|
-, 1001s, 32.4%
|
-, 1001s, 13.8%
|
-, 1001s, 12.5%
|
736-mulhs016-sc2009.real-time.png |
-, 1001s, 13.3%
|
-, 1001s, 25.9%
|
-, 1001s, 10.0%
|
-, 1001s, 9.1%
|
737-ndhf_xits_16_UNKNOWN-sc2009.real-time.png |
-, 1001s, 52.3%
|
-, 1001s, 38.8%
|
-, 1001s, 25.6%
|
-, 1001s, 16.3%
|
738-ndhf_xits_19_UNKNOWN-sc2011.real-time.png |
sat, 6s, 12.0%
|
sat, 6s, 15.4%
|
sat, 6s, 14.6%
|
sat, 6s, 4.2%
|
739-newton.2.3.i.smt2-cvc4-sc2016.real-time.png |
-, 1001s, 52.9%
|
unsat, 533s, 52.2%
|
unsat, 310s, 10.5%
|
unsat, 445s, 11.7%
|
740-par32-1-c.shuffled-as.sat03-1531-sc2002.real-time.png |
-, 1001s, 5.7%
|
-, 1001s
|
-, 1001s, 19.4%
|
-, 1001s, 22.4%
|
741-partial-10-11-s-sc2007.real-time.png |
sat, 473s, 14.3%
|
sat, 295s, 15.9%
|
sat, 51s, 16.4%
|
sat, 214s, 9.9%
|
742-partial-10-11-u-sc2007.real-time.png |
-, 1001s, 11.0%
|
-, 1001s, 14.1%
|
-, 1001s, 17.9%
|
-, 1001s, 10.6%
|
743-partial-5-11-u-sc2007.real-time.png |
-, 1001s, 8.8%
|
-, 1001s, 12.1%
|
-, 1001s, 15.3%
|
-, 1001s, 9.6%
|
744-partial-5-17-s-sc2007.real-time.png |
sat, 376s, 16.5%
|
sat, 293s, 19.5%
|
-, 1001s, 13.3%
|
sat, 363s, 7.6%
|
745-partial-5-19-u-sc2007.real-time.png |
-, 1001s, 14.2%
|
-, 1001s, 17.4%
|
-, 1001s, 13.2%
|
-, 1001s, 7.0%
|
746-pb_300_10_lb_08-sc2014.real-time.png |
unsat, 418s, 17.8%
|
unsat, 82s, 21.6%
|
unsat, 74s, 9.9%
|
unsat, 66s, 8.4%
|
747-ps_5000_21250_3_0_0.7_0_1.45_4-sc2017.real-time.png |
-, 1001s, 14.2%
|
-, 1001s, 43.8%
|
-, 1001s, 15.7%
|
-, 1001s, 17.5%
|
748-ps_5000_21250_3_0_0.8_0_1.55_2-sc2017.real-time.png |
-, 1001s, 14.5%
|
unsat, 600s, 37.4%
|
unsat, 464s, 11.0%
|
unsat, 509s, 17.7%
|
749-rbcl_xits_11_UNKNOWN-sc2009.real-time.png |
-, 1001s, 47.1%
|
-, 1001s, 33.0%
|
-, 1001s, 19.6%
|
-, 1001s, 10.1%
|
750-rbcl_xits_13_UNKNOWN-sc2009.real-time.png |
-, 1001s, 55.0%
|
-, 1001s, 31.6%
|
-, 1001s, 20.6%
|
-, 1001s, 13.2%
|
751-rbsat-v2100c215164g4-sc2011.real-time.png |
-, 1001s, 11.1%
|
-, 1001s, 16.2%
|
-, 1001s, 13.3%
|
-, 1001s, 6.8%
|
752-rbsat-v2400c266431g5-sc2009.real-time.png |
-, 1001s, 8.6%
|
-, 1001s, 16.1%
|
-, 1001s, 11.9%
|
-, 1001s, 7.7%
|
753-rbsat-v945c61409gyes9-sc2009.real-time.png |
sat, 34s, 12.7%
|
sat, 549s, 15.3%
|
sat, 82s, 9.9%
|
sat, 365s, 6.4%
|
754-rphp5_100_shuffled-sc2016.real-time.png |
-, 1001s, 28.9%
|
-, 1001s, 43.7%
|
-, 1001s, 36.6%
|
-, 1001s, 23.7%
|
755-rpoc_xits_11_UNKNOWN-sc2009.real-time.png |
-, 1001s, 49.6%
|
-, 1001s, 27.8%
|
-, 1001s, 34.6%
|
-, 1001s, 11.8%
|
756-rpoc_xits_12_UNKNOWN-sc2009.real-time.png |
-, 1001s, 55.0%
|
-, 1001s, 32.4%
|
-, 1001s, 20.5%
|
-, 1001s, 12.2%
|
757-rubikcube701-sc2017.real-time.png |
unsat, 241s, 13.1%
|
unsat, 396s, 18.8%
|
unsat, 290s, 12.3%
|
unsat, 313s, 10.5%
|
758-rubikcube912-sc2017.real-time.png |
-, 1001s, 14.7%
|
-, 1001s, 20.7%
|
-, 1001s, 19.6%
|
-, 1001s, 8.8%
|
759-safe-30-h29-unsat-sc2007.real-time.png |
-, 1001s, 18.5%
|
-, 1001s, 43.0%
|
-, 1001s, 30.0%
|
-, 1001s, 12.4%
|
760-satcoin-genesis-SAT-10-sc2018.real-time.png |
sat, 2s, 41.8%
|
sat, 2s, 68.5%
|
sat, 2s, 10.5%
|
sat, 2s, 9.3%
|
761-sgen1-sat-180-100-sc2009.real-time.png |
sat, 39s, 6.5%
|
-, 1001s, 51.1%
|
-, 1001s, 29.7%
|
sat, 445s, 14.8%
|
762-sgen1-unsat-109-100-sc2009.real-time.png |
-, 1001s, 9.8%
|
-, 1001s, 31.4%
|
-, 1001s, 23.3%
|
-, 1001s, 6.8%
|
763-sha2.shuffled-as.sat03-442-sc2002.real-time.png |
-, 1001s, 61.3%
|
-, 1001s, 49.9%
|
-, 1001s, 12.1%
|
-, 1001s, 9.2%
|
764-sin.c.75.smt2-cvc4-sc2016.real-time.png |
-, 41s
|
-, 1001s, 0.0%
|
-, 1001s, 0.0%
|
-, 1001s, 0.0%
|
765-slp-synthesis-aes-bottom13-sc2011.real-time.png |
-, 1001s, 16.6%
|
unsat, 80s, 17.3%
|
unsat, 38s, 10.0%
|
unsat, 84s, 9.6%
|
766-slp-synthesis-aes-bottom18-sc2011.real-time.png |
-, 1001s, 13.9%
|
-, 1001s, 24.7%
|
-, 1001s, 23.6%
|
-, 1001s, 21.2%
|
767-slp-synthesis-aes-bottom22-sc2011.real-time.png |
-, 1001s, 13.4%
|
-, 1001s, 24.8%
|
-, 1001s, 22.6%
|
-, 1001s, 20.2%
|
768-slp-synthesis-aes-bottom26-sc2011.real-time.png |
-, 1001s, 12.9%
|
-, 1001s, 24.8%
|
-, 1001s, 18.9%
|
-, 1001s, 16.7%
|
769-slp-synthesis-aes-top21-sc2011.real-time.png |
-, 1001s, 12.2%
|
-, 1001s, 41.3%
|
-, 1001s, 33.6%
|
-, 1001s, 36.2%
|
770-slp-synthesis-aes-top26-sc2011.real-time.png |
-, 1001s, 11.1%
|
-, 1001s, 22.7%
|
-, 1001s, 23.8%
|
-, 1001s, 8.1%
|
771-smtlib-qfbv-aigs-countbits128-tseitin-sc2011.real-time.png |
-, 1001s, 27.3%
|
-, 1001s, 29.0%
|
-, 1001s, 14.4%
|
-, 1001s, 8.4%
|
772-smulo032-sc2012.real-time.png |
-, 1001s, 20.9%
|
unsat, 284s, 22.7%
|
unsat, 279s, 9.0%
|
unsat, 261s, 7.0%
|
773-snw_13_8_pre-sc2016.real-time.png |
unsat, 995s, 7.0%
|
unsat, 817s, 9.6%
|
unsat, 778s, 6.2%
|
unsat, 729s, 4.3%
|
774-snw_16_8_nopre-sc2016.real-time.png |
-, 1001s, 6.4%
|
-, 1001s, 9.9%
|
-, 1001s, 6.6%
|
-, 1001s, 7.2%
|
775-snw_16_8_pre-sc2016.real-time.png |
-, 1001s, 5.8%
|
-, 1001s, 9.7%
|
-, 1001s, 6.9%
|
-, 1001s, 5.7%
|
776-sokoban-p16.sas.ex.15-sc2016.real-time.png |
-, 1001s, 18.7%
|
unsat, 883s, 29.7%
|
unsat, 925s, 32.5%
|
unsat, 722s, 18.3%
|
777-sokoban-p16.sas.ex.19-sc2016.real-time.png |
-, 1001s, 16.0%
|
-, 1001s, 26.8%
|
-, 1001s, 34.7%
|
-, 1001s, 15.7%
|
778-sokoban-p16.sas.ex.21-sc2016.real-time.png |
-, 1001s, 16.7%
|
-, 1001s, 24.4%
|
-, 1001s, 34.4%
|
-, 1001s, 24.4%
|
779-sokoban-p16.sas.ex.23-sc2016.real-time.png |
-, 1001s, 18.4%
|
-, 1001s, 22.5%
|
-, 1001s, 34.6%
|
-, 1001s, 14.4%
|
780-sokoban-p20.sas.cr.35-sc2016.real-time.png |
-, 1001s, 15.6%
|
-, 1001s, 19.2%
|
-, 1001s, 17.5%
|
-, 1001s, 7.4%
|
781-sokoban-p20.sas.ex.15-sc2016.real-time.png |
-, 1001s, 14.4%
|
-, 1001s, 32.7%
|
-, 1001s, 33.9%
|
-, 1001s, 16.0%
|
782-sokoban-p20.sas.ex.17-sc2016.real-time.png |
-, 1001s, 13.8%
|
-, 1001s, 23.0%
|
-, 1001s, 36.8%
|
-, 1001s, 14.0%
|
783-sokoban-p20.sas.ex.23-sc2016.real-time.png |
-, 1001s, 14.1%
|
-, 1001s, 20.0%
|
-, 1001s, 34.4%
|
-, 1001s, 21.5%
|
784-squ_ali_s10x10_c39_abix_SAT-sc2017.real-time.png |
sat, 14s, 10.5%
|
sat, 233s, 20.5%
|
sat, 269s, 17.7%
|
sat, 109s, 11.9%
|
785-squ_any_s09x07_c27_abio_UNS-sc2017.real-time.png |
unsat, 730s, 9.9%
|
unsat, 471s, 17.2%
|
unsat, 454s, 12.4%
|
unsat, 419s, 8.8%
|
786-srhd-sgi-m62-q1504.5-n60-p30-s88600538-sc2011.real-time.png |
-, 1001s, 65.2%
|
-, 1001s, 28.1%
|
-, 1001s, 21.7%
|
-, 1001s, 12.1%
|
787-stable-400-0.1-4-9876543214004-sc2014.real-time.png |
-, 1001s, 13.7%
|
-, 1001s, 20.8%
|
-, 1001s, 11.9%
|
-, 1001s, 7.5%
|
788-sted1_0x0-380-sc2018.real-time.png |
-, 1001s, 14.0%
|
-, 1001s, 12.2%
|
-, 1001s, 8.9%
|
-, 1001s, 8.3%
|
789-stone-width3chain-nmarkers-20_shuffled-sc2016.real-time.png |
unknown error (134), 434s
|
-, 1001s, 48.5%
|
-, 1001s, 37.7%
|
-, 1001s, 27.4%
|
790-test_v7_r12_vr10_c1_s18160.smt2-stp212-sc2016.real-time.png |
-, 1001s, 17.3%
|
-, 1001s, 27.2%
|
-, 1001s, 6.4%
|
-, 1001s, 7.1%
|
791-total-10-15-s-sc2007.real-time.png |
sat, 61s, 15.4%
|
sat, 12s, 23.1%
|
sat, 32s, 22.5%
|
sat, 25s, 14.2%
|
792-total-10-15-u-sc2007.real-time.png |
-, 1001s, 12.6%
|
-, 1001s, 25.8%
|
-, 1001s, 23.7%
|
-, 1001s, 15.2%
|
793-tseitingrid7x160_shuffled-sc2016.real-time.png |
-, 1001s, 30.5%
|
-, 1001s, 42.2%
|
-, 1001s, 39.0%
|
-, 1001s, 24.8%
|
794-uniqinv47prop-sc2018.real-time.png |
-, 1001s, 18.8%
|
-, 1001s, 27.6%
|
-, 1001s, 17.7%
|
-, 1001s, 8.1%
|
795-unsat-set-a-fclqcolor-20-13-14.sat05-1278.reshuffled-07-sc2007.real-time.png |
-, 1001s, 28.0%
|
-, 1001s, 25.5%
|
-, 1001s, 27.5%
|
-, 1001s, 25.9%
|
796-vmpc_30-sc2007.real-time.png |
sat, 201s, 10.1%
|
sat, 39s, 14.7%
|
sat, 28s, 9.0%
|
sat, 34s, 6.2%
|
797-vmpc_31-sc2007.real-time.png |
sat, 338s, 9.2%
|
sat, 53s, 15.2%
|
sat, 189s, 10.1%
|
sat, 146s, 7.3%
|
798-vmpc_34.shuffled-as.sat05-1958-sc2005.real-time.png |
-, 1001s, 9.2%
|
sat, 617s, 16.8%
|
sat, 134s, 9.6%
|
sat, 246s, 7.3%
|
799-vmpc_36.renamed-as.sat05-1922-sc2005.real-time.png |
-, 1001s, 9.9%
|
-, 1001s, 16.8%
|
-, 1001s, 10.4%
|
-, 1001s, 8.4%
|
800-x2_128.shuffled-as.sat03-1598-sc2002.real-time.png |
-, 1001s, 16.8%
|
-, 1001s, 44.9%
|
-, 1001s, 37.6%
|
-, 1001s, 22.4%
|