Str | Args | Deps | Syms | Prems | Prover | Thm% | CoS% | Uniq | ST⌀ | STΣ | Thm | CoS | Maybe | Empty | Err | Found |
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
hhjournal | nb_t_nts_ad2 | orig | 0 | 154 | epar | 24.666 | 0.111 | 3 | 0.055 | 24.43 | 443 | 2 | 1351 | 0 | 1796 | |
hhjournal | nb_t_nts_ad2 | orig | 0 | 92 | vam | 23.998 | 0.056 | 5 | 0.057 | 24.72 | 431 | 1 | 1341 | 23 | 1796 | |
hhjournal | nb_t_nts_ad2 | orig | 0 | 128 | epar | 23.719 | 0.111 | 0 | 0.043 | 18.56 | 426 | 2 | 1368 | 0 | 1796 | |
default | default | 0 | 0 | 512 | epar | 22.439 | 0.000 | 1 | 0.018 | 7.06 | 403 | 0 | 1393 | 0 | 1796 | |
seq | d2_div_s | 0 | 10 | 128 | epar | 22.383 | 0.000 | 0 | 0.013 | 5.31 | 402 | 0 | 1393 | 1 | 1796 | |
default | default | 0 | 0 | 128 | epar | 22.327 | 0.000 | 0 | 0.013 | 5.25 | 401 | 0 | 1395 | 0 | 1796 | |
seq | d2_div_s | 0 | 20 | 128 | epar | 22.105 | 0.000 | 0 | 0.012 | 4.93 | 397 | 0 | 1394 | 5 | 1796 | |
pgrank | u_div_s | 0 | 10 | 128 | epar | 22.049 | 0.000 | 0 | 0.013 | 5.17 | 396 | 0 | 1339 | 61 | 1796 | |
seq | d2_div_s | 0 | 10 | 512 | epar | 22.049 | 0.000 | 0 | 0.015 | 5.77 | 396 | 0 | 1400 | 0 | 1796 | |
maxcut | default | 0 | 1 | 128 | epar | 21.993 | 0.000 | 0 | 0.014 | 5.43 | 395 | 0 | 1396 | 5 | 1796 | |
pgrank | du_div_s | 0 | 20 | 128 | epar | 21.882 | 0.000 | 0 | 0.014 | 5.56 | 393 | 0 | 1355 | 48 | 1796 | |
seq | d_u_div_s2 | 0 | 10 | 128 | epar | 21.826 | 0.000 | 0 | 0.012 | 4.75 | 392 | 0 | 1396 | 8 | 1796 | |
pgrank | du_div_s | 0 | 10 | 128 | epar | 21.771 | 0.000 | 0 | 0.013 | 5.23 | 391 | 0 | 1386 | 19 | 1796 | |
epcl | default | 0 | 10 | 128 | epar | 21.715 | 0.000 | 0 | 0.013 | 5.05 | 390 | 0 | 1399 | 7 | 1796 | |
seq | d2_div_s | 0 | 20 | 512 | epar | 21.715 | 0.000 | 0 | 0.015 | 5.75 | 390 | 0 | 1404 | 2 | 1796 | |
seq | d_u_div_exps | 0 | 20 | 128 | epar | 21.659 | 0.000 | 0 | 0.013 | 5.23 | 389 | 0 | 1387 | 20 | 1796 | |
seq | d_u_div_exps | 0 | 10 | 128 | epar | 21.548 | 0.000 | 0 | 0.013 | 4.87 | 387 | 0 | 1401 | 8 | 1796 | |
seq | d_u_div_s | 0 | 10 | 128 | epar | 21.548 | 0.000 | 0 | 0.013 | 5.08 | 387 | 0 | 1403 | 6 | 1796 | |
seq | d_u_div_exps | 0 | 10 | 512 | epar | 21.437 | 0.000 | 0 | 0.013 | 4.87 | 385 | 0 | 1404 | 7 | 1796 | |
seq | d_u_div_s2 | 0 | 20 | 128 | epar | 21.437 | 0.000 | 0 | 0.013 | 5.03 | 385 | 0 | 1396 | 15 | 1796 | |
pgrank | u_div_s | 0 | 20 | 128 | epar | 21.381 | 0.000 | 1 | 0.017 | 6.43 | 384 | 0 | 1307 | 105 | 1796 | |
pgrank | u_div_s | 0 | 10 | 512 | epar | 21.325 | 0.000 | 0 | 0.014 | 5.23 | 383 | 0 | 1355 | 58 | 1796 | |
maxcut | default | 0 | 5 | 512 | epar | 21.214 | 0.000 | 0 | 0.014 | 5.16 | 381 | 0 | 1391 | 24 | 1796 | |
pgrank | du | 0 | 10 | 128 | epar | 21.214 | 0.000 | 0 | 0.012 | 4.50 | 381 | 0 | 1409 | 6 | 1796 | |
epcl | default | 0 | 20 | 128 | epar | 21.158 | 0.000 | 0 | 0.012 | 4.55 | 380 | 0 | 1404 | 12 | 1796 | |
maxcut | default | 0 | 10 | 512 | epar | 21.102 | 0.000 | 0 | 0.015 | 5.72 | 379 | 0 | 1377 | 40 | 1796 | |
seq | d_u_div_s | 0 | 20 | 128 | epar | 21.047 | 0.000 | 0 | 0.013 | 4.89 | 378 | 0 | 1402 | 16 | 1796 | |
pgrank | du_div_s | 0 | 10 | 512 | epar | 20.935 | 0.000 | 0 | 0.014 | 5.18 | 376 | 0 | 1403 | 17 | 1796 | |
pgrank | du_div_s | 0 | 20 | 512 | epar | 20.935 | 0.000 | 1 | 0.018 | 6.85 | 376 | 0 | 1376 | 44 | 1796 | |
maxcut | default | 0 | 1 | 512 | epar | 22.368 | 0.000 | 0 | 0.013 | 4.84 | 374 | 0 | 1292 | 6 | 1672 | |
pgrank | u | 0 | 10 | 128 | epar | 20.824 | 0.000 | 0 | 0.011 | 4.20 | 374 | 0 | 1415 | 7 | 1796 | |
epcl | default | 0 | 10 | 512 | epar | 20.768 | 0.000 | 0 | 0.013 | 4.71 | 373 | 0 | 1415 | 8 | 1796 | |
pgrank | du | 0 | 10 | 512 | epar | 20.713 | 0.000 | 0 | 0.013 | 4.67 | 372 | 0 | 1419 | 5 | 1796 | |
seq | d_u_div_exps | 0 | 20 | 512 | epar | 20.713 | 0.000 | 1 | 0.015 | 5.57 | 372 | 0 | 1407 | 17 | 1796 | |
seq | d_u_div_s2 | 0 | 10 | 512 | epar | 20.713 | 0.000 | 0 | 0.012 | 4.53 | 372 | 0 | 1417 | 7 | 1796 | |
hhjournal | nb_t_nts_ad2 | orig | 0 | 1024 | epar | 20.601 | 0.111 | 6 | 0.057 | 21.04 | 370 | 2 | 1424 | 0 | 1796 | |
maxcut | default | 0 | 5 | 128 | epar | 20.601 | 0.000 | 0 | 0.012 | 4.57 | 370 | 0 | 1392 | 34 | 1796 | |
seq | d2_div_s | 0 | 60 | 128 | epar | 20.601 | 0.000 | 0 | 0.012 | 4.27 | 370 | 0 | 1361 | 65 | 1796 | |
seq | d_u_div_s | 0 | 10 | 512 | epar | 20.601 | 0.000 | 0 | 0.012 | 4.57 | 370 | 0 | 1420 | 6 | 1796 | |
pgrank | u | 0 | 10 | 512 | epar | 20.490 | 0.000 | 0 | 0.013 | 4.87 | 368 | 0 | 1421 | 7 | 1796 | |
pgrank | u_div_s | 0 | 20 | 512 | epar | 20.490 | 0.000 | 0 | 0.014 | 5.06 | 368 | 0 | 1331 | 97 | 1796 | |
pgrank | d_div_s | 0 | 20 | 128 | epar | 20.434 | 0.000 | 0 | 0.015 | 5.64 | 367 | 0 | 1310 | 119 | 1796 | |
pgrank | du | 0 | 20 | 128 | epar | 20.379 | 0.000 | 0 | 0.012 | 4.24 | 366 | 0 | 1420 | 10 | 1796 | |
pgrank | du | 0 | 20 | 512 | epar | 20.379 | 0.000 | 0 | 0.015 | 5.48 | 366 | 0 | 1423 | 7 | 1796 | |
seq | d_u_div_s2 | 0 | 20 | 512 | epar | 20.323 | 0.000 | 0 | 0.012 | 4.47 | 365 | 0 | 1418 | 13 | 1796 | |
pgrank | d | 0 | 10 | 128 | epar | 20.267 | 0.000 | 0 | 0.013 | 4.80 | 364 | 0 | 1369 | 63 | 1796 | |
seq | d2_div_s | 0 | 60 | 512 | epar | 20.267 | 0.000 | 0 | 0.014 | 4.98 | 364 | 0 | 1378 | 54 | 1796 | |
seq | d_u_div_s | 0 | 20 | 512 | epar | 20.267 | 0.000 | 0 | 0.013 | 4.65 | 364 | 0 | 1419 | 13 | 1796 | |
hhjournal | nb_0_hd | orig | 0 | 512 | epar | 20.212 | 0.000 | 3 | 0.044 | 16.09 | 363 | 0 | 1433 | 0 | 1796 | |
pgrank | d_div_s | 0 | 10 | 128 | epar | 20.156 | 0.000 | 0 | 0.013 | 4.70 | 362 | 0 | 1363 | 71 | 1796 | |
pgrank | u | 0 | 20 | 128 | epar | 20.156 | 0.000 | 1 | 0.015 | 5.30 | 362 | 0 | 1417 | 17 | 1796 | |
seq | d_u_div_s2 | 0 | 60 | 128 | epar | 20.156 | 0.000 | 0 | 0.013 | 4.63 | 362 | 0 | 1321 | 113 | 1796 | |
epcl | default | 0 | 20 | 512 | epar | 20.100 | 0.000 | 0 | 0.012 | 4.48 | 361 | 0 | 1424 | 11 | 1796 | |
pgrank | u | 0 | 20 | 512 | epar | 20.100 | 0.000 | 0 | 0.015 | 5.45 | 361 | 0 | 1423 | 12 | 1796 | |
maxcut | default | 0 | 10 | 128 | epar | 19.933 | 0.000 | 0 | 0.013 | 4.65 | 358 | 0 | 1391 | 47 | 1796 | |
seq | d_u_div_s2 | 0 | 60 | 512 | epar | 19.878 | 0.000 | 0 | 0.012 | 4.31 | 357 | 0 | 1348 | 91 | 1796 | |
pgrank | d | 0 | 20 | 128 | epar | 19.822 | 0.000 | 0 | 0.012 | 4.34 | 356 | 0 | 1354 | 86 | 1796 | |
epcl | default | 0 | 60 | 128 | epar | 19.543 | 0.000 | 0 | 0.013 | 4.67 | 351 | 0 | 1409 | 36 | 1796 | |
pgrank | u | 0 | 60 | 128 | epar | 19.543 | 0.000 | 1 | 0.015 | 5.14 | 351 | 0 | 1400 | 45 | 1796 | |
seq | u2_div_s | 0 | 10 | 128 | epar | 19.543 | 0.000 | 0 | 0.011 | 3.96 | 351 | 0 | 1422 | 23 | 1796 | |
pgrank | du_div_s | 0 | 60 | 128 | epar | 19.488 | 0.000 | 0 | 0.016 | 5.54 | 350 | 0 | 1299 | 147 | 1796 | |
seq | d_u_div_exps | 0 | 60 | 128 | epar | 19.376 | 0.000 | 0 | 0.014 | 4.76 | 348 | 0 | 1290 | 158 | 1796 | |
seq | u2_div_s | 0 | 20 | 128 | epar | 19.376 | 0.000 | 0 | 0.013 | 4.39 | 348 | 0 | 1409 | 39 | 1796 | |
pgrank | du | 0 | 60 | 128 | epar | 19.154 | 0.000 | 0 | 0.012 | 4.24 | 344 | 0 | 1416 | 36 | 1796 | |
pgrank | d | 0 | 60 | 128 | epar | 18.931 | 0.000 | 0 | 0.011 | 3.89 | 340 | 0 | 1343 | 113 | 1796 | |
pgrank | u_div_s | 0 | 60 | 128 | epar | 18.820 | 0.000 | 0 | 0.015 | 4.97 | 338 | 0 | 1257 | 201 | 1796 | |
seq | u2_div_s | 0 | 60 | 128 | epar | 18.597 | 0.000 | 0 | 0.011 | 3.83 | 334 | 0 | 1374 | 88 | 1796 | |
seq | d_u_div_s | 0 | 60 | 512 | epar | 18.541 | 0.000 | 0 | 0.013 | 4.25 | 333 | 0 | 1388 | 75 | 1796 | |
pgrank | d_div_s | 0 | 60 | 128 | epar | 18.374 | 0.000 | 0 | 0.015 | 4.80 | 330 | 0 | 1236 | 230 | 1796 | |
seq | d_u_div_exps | 0 | 60 | 512 | epar | 18.374 | 0.000 | 0 | 0.012 | 4.05 | 330 | 0 | 1325 | 141 | 1796 | |
pgrank | du_div_s | 0 | 60 | 512 | epar | 18.263 | 0.000 | 0 | 0.014 | 4.54 | 328 | 0 | 1335 | 133 | 1796 | |
seq | d_u_div_s | 0 | 60 | 128 | epar | 18.207 | 0.000 | 0 | 0.013 | 4.09 | 327 | 0 | 1373 | 96 | 1796 | |
pgrank | du | 0 | 60 | 512 | epar | 18.151 | 0.000 | 0 | 0.011 | 3.69 | 326 | 0 | 1437 | 33 | 1796 | |
epcl | default | 0 | 60 | 512 | epar | 18.040 | 0.000 | 0 | 0.011 | 3.67 | 324 | 0 | 1444 | 28 | 1796 | |
pgrank | d | 0 | 10 | 512 | epar | 17.762 | 0.000 | 0 | 0.012 | 3.91 | 319 | 0 | 1427 | 50 | 1796 | |
pgrank | u_div_s | 0 | 60 | 512 | epar | 17.762 | 0.000 | 0 | 0.014 | 4.37 | 319 | 0 | 1298 | 179 | 1796 | |
pgrank | d_div_s | 0 | 10 | 512 | epar | 17.650 | 0.000 | 0 | 0.012 | 3.95 | 317 | 0 | 1416 | 63 | 1796 | |
hhjournal | nb_vd1 | orig | 0 | 128 | epar | 17.038 | 0.000 | 0 | 0.035 | 10.63 | 306 | 0 | 1490 | 0 | 1796 | |
pgrank | d_div_s | 0 | 20 | 512 | epar | 16.370 | 0.000 | 0 | 0.016 | 4.59 | 294 | 0 | 1393 | 109 | 1796 | |
seq | u2_div_s | 0 | 10 | 512 | epar | 15.813 | 0.000 | 0 | 0.011 | 3.22 | 284 | 0 | 1495 | 17 | 1796 | |
pgrank | d | 0 | 20 | 512 | epar | 15.646 | 0.000 | 0 | 0.011 | 2.97 | 281 | 0 | 1435 | 80 | 1796 | |
hhjournal | nb_o_hd | orig | 0 | 128 | vam | 15.590 | 0.000 | 2 | 0.045 | 12.54 | 280 | 0 | 1515 | 1 | 1796 | |
pgrank | u | 0 | 60 | 512 | epar | 15.312 | 0.000 | 0 | 0.011 | 3.13 | 275 | 0 | 1493 | 28 | 1796 | |
seq | d2_div_s | 0 | 10 | 32 | z3_4 | 15.145 | 0.000 | 0 | 0.011 | 2.95 | 272 | 0 | 0 | 1524 | 1796 | |
default | default | 0 | 0 | 32 | z3_4 | 15.089 | 0.000 | 0 | 0.011 | 2.92 | 271 | 0 | 0 | 1525 | 1796 | |
hhjournal | kn40_t_nts_ad1 | orig | 0 | 32 | epar | 15.089 | 5.624 | 1 | 0.030 | 11.16 | 271 | 101 | 1424 | 0 | 1796 | |
seq | d2_div_s | 0 | 20 | 32 | z3_4 | 15.089 | 0.000 | 0 | 0.013 | 3.51 | 271 | 0 | 0 | 1525 | 1796 | |
pgrank | u | 0 | 60 | 32 | z3_4 | 14.978 | 0.000 | 4 | 0.037 | 9.87 | 269 | 0 | 0 | 1527 | 1796 | |
epcl | default | 0 | 10 | 32 | z3_4 | 14.922 | 0.000 | 0 | 0.012 | 3.14 | 268 | 0 | 0 | 1528 | 1796 | |
pgrank | d | 0 | 60 | 512 | epar | 14.811 | 0.000 | 0 | 0.010 | 2.68 | 266 | 0 | 1442 | 88 | 1796 | |
seq | d2_div_s | 0 | 60 | 32 | z3_4 | 14.755 | 0.000 | 6 | 0.037 | 9.70 | 265 | 0 | 0 | 1531 | 1796 | |
seq | u2_div_s | 0 | 20 | 512 | epar | 14.755 | 0.000 | 0 | 0.010 | 2.59 | 265 | 0 | 1498 | 33 | 1796 | |
epcl | default | 0 | 20 | 32 | z3_4 | 14.644 | 0.000 | 0 | 0.013 | 3.30 | 263 | 0 | 0 | 1533 | 1796 | |
pgrank | u_div_s | 0 | 10 | 32 | z3_4 | 14.703 | 0.000 | 0 | 0.012 | 3.20 | 262 | 0 | 0 | 1520 | 1782 | |
seq | d_u_div_exps | 0 | 10 | 32 | z3_4 | 14.588 | 0.000 | 0 | 0.012 | 3.02 | 262 | 0 | 0 | 1534 | 1796 | |
pgrank | u | 0 | 10 | 32 | z3_4 | 14.477 | 0.000 | 0 | 0.013 | 3.26 | 260 | 0 | 0 | 1536 | 1796 | |
seq | u2_div_s | 0 | 60 | 512 | epar | 14.477 | 0.000 | 0 | 0.010 | 2.63 | 260 | 0 | 1467 | 69 | 1796 | |
maxcut | default | 0 | 1 | 32 | z3_4 | 14.421 | 0.000 | 0 | 0.011 | 2.75 | 259 | 0 | 0 | 1537 | 1796 | |
seq | d_u_div_s | 0 | 60 | 32 | z3_4 | 14.421 | 0.000 | 4 | 0.041 | 10.61 | 259 | 0 | 0 | 1537 | 1796 | |
pgrank | u_div_s | 0 | 20 | 32 | z3_4 | 14.430 | 0.000 | 0 | 0.014 | 3.74 | 258 | 0 | 0 | 1530 | 1788 | |
seq | d_u_div_s | 0 | 20 | 32 | z3_4 | 14.310 | 0.000 | 1 | 0.019 | 4.95 | 257 | 0 | 0 | 1539 | 1796 | |
seq | d_u_div_s2 | 0 | 10 | 32 | z3_4 | 14.310 | 0.000 | 0 | 0.011 | 2.79 | 257 | 0 | 0 | 1539 | 1796 | |
epcl | default | 0 | 60 | 32 | z3_4 | 14.254 | 0.000 | 0 | 0.018 | 4.61 | 256 | 0 | 0 | 1540 | 1796 | |
seq | d_u_div_s | 0 | 10 | 32 | z3_4 | 14.198 | 0.000 | 0 | 0.012 | 3.00 | 255 | 0 | 0 | 1541 | 1796 | |
maxcut | default | 0 | 10 | 32 | z3_4 | 14.143 | 0.000 | 0 | 0.011 | 2.92 | 254 | 0 | 0 | 1542 | 1796 | |
pgrank | du_div_s | 0 | 20 | 32 | z3_4 | 14.143 | 0.000 | 0 | 0.012 | 2.95 | 254 | 0 | 0 | 1542 | 1796 | |
pgrank | du_div_s | 0 | 10 | 32 | z3_4 | 14.087 | 0.000 | 0 | 0.010 | 2.57 | 253 | 0 | 0 | 1543 | 1796 | |
seq | d_u_div_exps | 0 | 20 | 32 | z3_4 | 14.087 | 0.000 | 0 | 0.011 | 2.89 | 253 | 0 | 0 | 1543 | 1796 | |
hhjournal | nb_t_nts_ad1 | orig | 0 | 32 | z3_4 | 13.976 | 0.000 | 4 | 0.052 | 13.14 | 251 | 0 | 0 | 1545 | 1796 | |
maxcut | default | 0 | 5 | 32 | z3_4 | 13.983 | 0.000 | 0 | 0.011 | 2.78 | 251 | 0 | 0 | 1544 | 1795 | |
pgrank | du | 0 | 10 | 32 | z3_4 | 13.976 | 0.000 | 0 | 0.010 | 2.63 | 251 | 0 | 0 | 1545 | 1796 | |
pgrank | du | 0 | 60 | 32 | z3_4 | 13.976 | 0.000 | 1 | 0.020 | 4.96 | 251 | 0 | 0 | 1545 | 1796 | |
seq | u2_div_s | 0 | 60 | 32 | z3_4 | 13.808 | 0.000 | 5 | 0.041 | 10.08 | 248 | 0 | 0 | 1548 | 1796 | |
all | default | 0 | all | 128 | epar | 13.753 | 0.000 | 0 | 0.016 | 3.86 | 247 | 0 | 1274 | 275 | 1796 | |
hhjournal | nb_t_nts_vd1 | orig | 0 | 128 | z3_4 | 13.641 | 0.000 | 0 | 0.039 | 9.55 | 245 | 0 | 0 | 1551 | 1796 | |
pgrank | u_div_s | 0 | 60 | 32 | z3_4 | 13.641 | 0.000 | 1 | 0.030 | 7.26 | 245 | 0 | 0 | 1551 | 1796 | |
seq | u2_div_s | 0 | 20 | 32 | z3_4 | 13.586 | 0.000 | 0 | 0.019 | 4.69 | 244 | 0 | 0 | 1552 | 1796 | |
pgrank | du | 0 | 20 | 32 | z3_4 | 13.530 | 0.000 | 0 | 0.009 | 2.31 | 243 | 0 | 0 | 1553 | 1796 | |
seq | d2_div_s | 0 | 10 | 92 | vam | 13.474 | 0.000 | 0 | 0.009 | 2.12 | 242 | 0 | 1553 | 1 | 1796 | |
seq | d_u_div_s2 | 0 | 60 | 32 | z3_4 | 13.474 | 0.000 | 3 | 0.029 | 6.95 | 242 | 0 | 0 | 1554 | 1796 | |
pgrank | d_div_s | 0 | 60 | 512 | epar | 13.419 | 0.000 | 1 | 0.018 | 4.36 | 241 | 0 | 1364 | 191 | 1796 | |
pgrank | u_div_s | 0 | 10 | 92 | vam | 13.419 | 0.000 | 0 | 0.010 | 2.45 | 241 | 0 | 1505 | 50 | 1796 | |
seq | d_u_div_exps | 0 | 60 | 32 | z3_4 | 13.419 | 0.000 | 0 | 0.019 | 4.66 | 241 | 0 | 0 | 1555 | 1796 | |
pgrank | u | 0 | 20 | 32 | z3_4 | 14.060 | 0.000 | 0 | 0.024 | 5.77 | 240 | 0 | 0 | 1467 | 1707 | |
seq | d2_div_s | 0 | 20 | 92 | vam | 13.363 | 0.000 | 0 | 0.009 | 2.10 | 240 | 0 | 1556 | 0 | 1796 | |
default | default | 0 | 0 | 92 | vam | 13.556 | 0.000 | 0 | 0.009 | 2.05 | 239 | 0 | 1524 | 0 | 1763 | |
maxcut | default | 0 | 1 | 92 | vam | 13.307 | 0.000 | 0 | 0.009 | 2.08 | 239 | 0 | 1552 | 5 | 1796 | |
seq | d_u_div_exps | 0 | 10 | 92 | vam | 13.252 | 0.000 | 0 | 0.009 | 2.07 | 238 | 0 | 1550 | 8 | 1796 | |
seq | u2_div_s | 0 | 10 | 32 | z3_4 | 13.500 | 0.000 | 0 | 0.019 | 4.64 | 238 | 0 | 0 | 1525 | 1763 | |
pgrank | du | 0 | 10 | 92 | vam | 13.196 | 0.000 | 0 | 0.008 | 1.94 | 237 | 0 | 1554 | 5 | 1796 | |
pgrank | d_div_s | 0 | 20 | 32 | z3_4 | 13.124 | 0.000 | 0 | 0.017 | 4.01 | 234 | 0 | 0 | 1549 | 1783 | |
pgrank | du_div_s | 0 | 10 | 92 | vam | 13.029 | 0.000 | 0 | 0.008 | 1.96 | 234 | 0 | 1547 | 15 | 1796 | |
seq | d_u_div_exps | 0 | 20 | 92 | vam | 13.029 | 0.000 | 0 | 0.009 | 2.08 | 234 | 0 | 1546 | 16 | 1796 | |
epcl | default | 0 | 20 | 92 | vam | 13.053 | 0.000 | 0 | 0.009 | 2.00 | 233 | 0 | 1537 | 15 | 1785 | |
pgrank | d | 0 | 20 | 32 | z3_4 | 13.053 | 0.000 | 3 | 0.029 | 6.82 | 233 | 0 | 0 | 1552 | 1785 | |
pgrank | d_div_s | 0 | 10 | 32 | z3_4 | 12.973 | 0.000 | 0 | 0.015 | 3.43 | 233 | 0 | 0 | 1563 | 1796 | |
all | default | 0 | all | 32 | z3_4 | 12.918 | 0.000 | 23 | 0.153 | 35.38 | 232 | 0 | 0 | 1564 | 1796 | |
epcl | default | 0 | 10 | 92 | vam | 12.918 | 0.000 | 0 | 0.008 | 1.91 | 232 | 0 | 1561 | 3 | 1796 | |
seq | d_u_div_s | 0 | 10 | 92 | vam | 13.053 | 0.000 | 0 | 0.009 | 2.00 | 230 | 0 | 1526 | 6 | 1762 | |
seq | d_u_div_s2 | 0 | 10 | 92 | vam | 12.806 | 0.000 | 0 | 0.008 | 1.90 | 230 | 0 | 1559 | 7 | 1796 | |
pgrank | du | 0 | 20 | 92 | vam | 12.751 | 0.000 | 0 | 0.009 | 2.05 | 229 | 0 | 1552 | 15 | 1796 | |
pgrank | du_div_s | 0 | 60 | 32 | z3_4 | 12.695 | 0.000 | 0 | 0.015 | 3.39 | 228 | 0 | 0 | 1568 | 1796 | |
seq | d2_div_s | 0 | 60 | 92 | vam | 12.695 | 0.000 | 0 | 0.009 | 2.13 | 228 | 0 | 1535 | 33 | 1796 | |
pgrank | du_div_s | 0 | 20 | 92 | vam | 12.639 | 0.000 | 0 | 0.008 | 1.93 | 227 | 0 | 1522 | 47 | 1796 | |
seq | d_u_div_s | 0 | 20 | 92 | vam | 12.584 | 0.000 | 0 | 0.008 | 1.91 | 226 | 0 | 1559 | 11 | 1796 | |
seq | d_u_div_s2 | 0 | 20 | 92 | vam | 12.834 | 0.000 | 0 | 0.008 | 1.89 | 226 | 0 | 1525 | 10 | 1761 | |
seq | d_u_div_s2 | 0 | 20 | 32 | z3_4 | 14.423 | 0.000 | 0 | 0.013 | 2.96 | 225 | 0 | 0 | 1335 | 1560 | |
pgrank | d | 0 | 60 | 32 | z3_4 | 12.472 | 0.000 | 1 | 0.020 | 4.52 | 224 | 0 | 0 | 1572 | 1796 | |
pgrank | d | 0 | 10 | 32 | z3_4 | 12.556 | 0.000 | 0 | 0.010 | 2.34 | 223 | 0 | 0 | 1553 | 1776 | |
pgrank | u | 0 | 10 | 92 | vam | 12.416 | 0.000 | 0 | 0.009 | 1.99 | 223 | 0 | 1565 | 8 | 1796 | |
pgrank | d | 0 | 10 | 92 | vam | 12.361 | 0.000 | 0 | 0.009 | 1.98 | 222 | 0 | 1529 | 45 | 1796 | |
pgrank | u_div_s | 0 | 20 | 92 | vam | 12.249 | 0.000 | 0 | 0.009 | 2.08 | 220 | 0 | 1492 | 84 | 1796 | |
pgrank | u | 0 | 60 | 92 | vam | 12.138 | 0.000 | 0 | 0.010 | 2.15 | 218 | 0 | 1554 | 24 | 1796 | |
maxcut | default | 0 | 5 | 92 | vam | 12.082 | 0.000 | 0 | 0.009 | 1.88 | 217 | 0 | 1528 | 51 | 1796 | |
pgrank | d_div_s | 0 | 10 | 92 | vam | 12.082 | 0.000 | 0 | 0.009 | 1.90 | 217 | 0 | 1518 | 61 | 1796 | |
seq | d_u_div_s2 | 0 | 60 | 92 | vam | 11.971 | 0.000 | 0 | 0.009 | 1.85 | 215 | 0 | 1502 | 79 | 1796 | |
epcl | default | 0 | 60 | 92 | vam | 11.915 | 0.000 | 0 | 0.008 | 1.70 | 214 | 0 | 1548 | 34 | 1796 | |
seq | d_u_div_exps | 0 | 60 | 92 | vam | 11.860 | 0.000 | 0 | 0.012 | 2.54 | 213 | 0 | 1452 | 131 | 1796 | |
pgrank | d_div_s | 0 | 60 | 32 | z3_4 | 11.748 | 0.000 | 1 | 0.019 | 3.92 | 211 | 0 | 0 | 1585 | 1796 | |
hhjournal | kn160_t_nts_ad1 | orig | 0 | 512 | z3_4 | 11.693 | 0.000 | 3 | 0.059 | 12.31 | 210 | 0 | 0 | 1586 | 1796 | |
pgrank | u | 0 | 20 | 92 | vam | 11.693 | 0.000 | 0 | 0.009 | 1.80 | 210 | 0 | 1580 | 6 | 1796 | |
pgrank | d | 0 | 20 | 92 | vam | 11.581 | 0.000 | 0 | 0.009 | 1.80 | 208 | 0 | 1523 | 65 | 1796 | |
pgrank | d_div_s | 0 | 20 | 92 | vam | 11.581 | 0.000 | 0 | 0.009 | 1.80 | 208 | 0 | 1484 | 104 | 1796 | |
pgrank | du | 0 | 60 | 92 | vam | 11.526 | 0.000 | 0 | 0.009 | 1.89 | 207 | 0 | 1566 | 23 | 1796 | |
seq | u2_div_s | 0 | 10 | 92 | vam | 11.470 | 0.000 | 0 | 0.008 | 1.65 | 206 | 0 | 1573 | 17 | 1796 | |
maxcut | default | 0 | 10 | 92 | vam | 11.440 | 0.000 | 0 | 0.008 | 1.69 | 205 | 0 | 1522 | 65 | 1792 | |
seq | u2_div_s | 0 | 60 | 92 | vam | 11.303 | 0.000 | 0 | 0.009 | 1.83 | 203 | 0 | 1546 | 47 | 1796 | |
pgrank | u_div_s | 0 | 60 | 92 | vam | 11.192 | 0.000 | 0 | 0.011 | 2.15 | 201 | 0 | 1452 | 143 | 1796 | |
seq | u2_div_s | 0 | 20 | 92 | vam | 11.136 | 0.000 | 0 | 0.008 | 1.56 | 195 | 0 | 1532 | 24 | 1751 | |
pgrank | du_div_s | 0 | 60 | 92 | vam | 10.690 | 0.000 | 0 | 0.009 | 1.78 | 192 | 0 | 1482 | 122 | 1796 | |
pgrank | d | 0 | 60 | 92 | vam | 10.626 | 0.000 | 0 | 0.009 | 1.72 | 190 | 0 | 1502 | 96 | 1788 | |
seq | d_u_div_s | 0 | 60 | 92 | vam | 10.579 | 0.000 | 0 | 0.008 | 1.52 | 190 | 0 | 1522 | 84 | 1796 | |
pgrank | d_div_s | 0 | 60 | 92 | vam | 10.329 | 0.000 | 0 | 0.011 | 2.13 | 185 | 0 | 1429 | 177 | 1791 | |
hhjournal | win_t_nts_hd | orig | 0 | 128 | epar | 9.967 | 0.056 | 2 | 0.037 | 6.60 | 179 | 1 | 1616 | 0 | 1796 | |
all | default | 0 | all | 92 | vam | 9.020 | 0.000 | 0 | 0.014 | 2.24 | 162 | 0 | 1434 | 200 | 1796 | |
all | default | 0 | all | 512 | epar | 8.519 | 0.000 | 0 | 0.010 | 1.48 | 153 | 0 | 1489 | 154 | 1796 | |
hhjournal | nb_t_nts_hd | orig | 0 | 32 | z3_4 | 7.906 | 0.000 | 0 | 0.028 | 4.03 | 142 | 0 | 0 | 1654 | 1796 | |
hhjournal | win_t_nts_hd | orig | 0 | 32 | z3_4 | 3.786 | 0.000 | 0 | 0.027 | 1.84 | 68 | 0 | 0 | 1728 | 1796 | |
any | 47.884 | 5.791 | 860 | 104 | 1796 |
Prover | Sum% | Sum | G+2 | G1+2 | G-1+2 | G+2M | Alt |
hhjournal-nb_t_nts_ad2-orig-0-154-epar | 24.666 | 443 | |||||
maxcut-default-0-1-128-epar | 31.180 | 560 | = pgrank-d_div_s-0-20-128-epar | ||||
all-default-0-all-32-z3_4 | 34.855 | 626 | |||||
hhjournal-nb_t_nts_ad2-orig-0-1024-epar | 36.693 | 659 | = seq-d_u_div_s-0-60-32-z3_4 | ||||
seq-d_u_div_s-0-60-32-z3_4 | 38.474 | 691 | |||||
hhjournal-nb_t_nts_ad2-orig-0-92-vam | 40.033 | 719 | |||||
default-default-0-0-512-epar | 40.980 | 736 | |||||
seq-u2_div_s-0-60-32-z3_4 | 41.759 | 750 | |||||
hhjournal-kn160_t_nts_ad1-orig-0-512-z3_4 | 42.316 | 760 | |||||
seq-d2_div_s-0-60-32-z3_4 | 42.762 | 768 | = pgrank-du_div_s-0-20-512-epar = pgrank-du_div_s-0-60-128-epar = pgrank-d_div_s-0-20-128-epar | ||||
pgrank-du_div_s-0-20-512-epar | 43.207 | 776 | = pgrank-du_div_s-0-60-128-epar = pgrank-d_div_s-0-20-128-epar | ||||
hhjournal-nb_0_hd-orig-0-512-epar | 43.541 | 782 | = pgrank-d-0-20-32-z3_4 = pgrank-u_div_s-0-20-128-epar = hhjournal-nb_t_nts_ad1-orig-0-32-z3_4 = ... (5) | ||||
pgrank-d-0-20-32-z3_4 | 43.875 | 788 | = pgrank-u_div_s-0-20-128-epar = hhjournal-nb_t_nts_ad1-orig-0-32-z3_4 = epcl-default-0-60-32-z3_4 = ... (4) | ||||
pgrank-u_div_s-0-20-128-epar | 44.209 | 794 | = hhjournal-nb_t_nts_ad1-orig-0-32-z3_4 = seq-d_u_div_s-0-20-32-z3_4 | ||||
hhjournal-nb_t_nts_ad1-orig-0-32-z3_4 | 44.543 | 800 | = seq-d_u_div_s-0-20-32-z3_4 | ||||
seq-d_u_div_s-0-20-32-z3_4 | 44.878 | 806 | |||||
pgrank-u_div_s-0-60-32-z3_4 | 45.156 | 811 | = pgrank-u-0-60-32-z3_4 | ||||
hhjournal-kn40_t_nts_ad1-orig-0-32-epar | 45.379 | 815 | = hhjournal-win_t_nts_hd-orig-0-128-epar = pgrank-du_div_s-0-60-128-epar = pgrank-u-0-60-32-z3_4 | ||||
pgrank-du_div_s-0-60-128-epar | 45.601 | 819 | = pgrank-u-0-60-32-z3_4 | ||||
pgrank-u-0-60-32-z3_4 | 45.824 | 823 | |||||
pgrank-d_div_s-0-10-92-vam | 45.991 | 826 | = seq-d_u_div_exps-0-10-92-vam = pgrank-d_div_s-0-20-32-z3_4 = hhjournal-win_t_nts_hd-orig-0-128-epar = ... (13) | ||||
pgrank-d_div_s-0-20-32-z3_4 | 46.158 | 829 | = seq-d_u_div_s2-0-60-32-z3_4 | ||||
seq-d_u_div_s2-0-60-32-z3_4 | 46.325 | 832 | |||||
seq-d_u_div_s-0-60-512-epar | 46.437 | 834 | = pgrank-d-0-10-128-epar = hhjournal-win_t_nts_hd-orig-0-128-epar = epcl-default-0-20-32-z3_4 = ... (7) | ||||
pgrank-d-0-10-128-epar | 46.548 | 836 | = hhjournal-win_t_nts_hd-orig-0-128-epar = epcl-default-0-20-32-z3_4 = seq-d_u_div_exps-0-60-32-z3_4 = ... (5) | ||||
hhjournal-win_t_nts_hd-orig-0-128-epar | 46.659 | 838 | = epcl-default-0-20-32-z3_4 = seq-d_u_div_exps-0-60-32-z3_4 = hhjournal-nb_o_hd-orig-0-128-vam | ||||
epcl-default-0-20-32-z3_4 | 46.771 | 840 | = seq-d_u_div_exps-0-60-32-z3_4 = hhjournal-nb_o_hd-orig-0-128-vam | ||||
seq-d_u_div_exps-0-60-32-z3_4 | 46.882 | 842 | = hhjournal-nb_o_hd-orig-0-128-vam | ||||
hhjournal-nb_o_hd-orig-0-128-vam | 46.993 | 844 | |||||
pgrank-u-0-60-128-epar | 47.049 | 845 | = pgrank-u_div_s-0-60-512-epar = pgrank-d_div_s-0-60-32-z3_4 = pgrank-d_div_s-0-20-512-epar = ... (26) | ||||
pgrank-u_div_s-0-60-512-epar | 47.105 | 846 | = pgrank-d_div_s-0-60-32-z3_4 = pgrank-d_div_s-0-20-512-epar = seq-d_u_div_s-0-20-128-epar = ... (25) | ||||
pgrank-d_div_s-0-60-32-z3_4 | 47.160 | 847 | = pgrank-d_div_s-0-20-512-epar = seq-d_u_div_s-0-20-128-epar = pgrank-u-0-20-512-epar = ... (23) | ||||
pgrank-d_div_s-0-20-512-epar | 47.216 | 848 | = seq-d_u_div_s-0-20-128-epar = pgrank-u-0-20-512-epar = seq-u2_div_s-0-10-32-z3_4 = ... (22) | ||||
seq-d_u_div_s-0-20-128-epar | 47.272 | 849 | = seq-u2_div_s-0-10-32-z3_4 = pgrank-d_div_s-0-60-512-epar = all-default-0-all-92-vam = ... (19) | ||||
seq-u2_div_s-0-10-32-z3_4 | 47.327 | 850 | = pgrank-d_div_s-0-60-512-epar = all-default-0-all-92-vam = all-default-0-all-128-epar = ... (17) | ||||
pgrank-d_div_s-0-60-512-epar | 47.383 | 851 | = all-default-0-all-92-vam = all-default-0-all-128-epar = seq-d_u_div_s-0-10-128-epar = ... (15) | ||||
all-default-0-all-92-vam | 47.439 | 852 | = all-default-0-all-128-epar = seq-d_u_div_s-0-10-128-epar = pgrank-du_div_s-0-10-128-epar = ... (14) | ||||
seq-d_u_div_s-0-10-128-epar | 47.494 | 853 | = pgrank-du_div_s-0-10-128-epar = seq-d_u_div_exps-0-20-512-epar = pgrank-d_div_s-0-10-32-z3_4 = ... (11) | ||||
seq-d_u_div_exps-0-20-512-epar | 47.550 | 854 | = pgrank-d_div_s-0-10-32-z3_4 = pgrank-d-0-60-32-z3_4 = pgrank-du-0-60-32-z3_4 = ... (9) | ||||
pgrank-d_div_s-0-10-32-z3_4 | 47.606 | 855 | = pgrank-d-0-60-32-z3_4 = pgrank-du-0-60-32-z3_4 = pgrank-u-0-20-32-z3_4 = ... (8) | ||||
pgrank-d-0-60-32-z3_4 | 47.661 | 856 | = pgrank-du-0-60-32-z3_4 = pgrank-u-0-20-32-z3_4 = pgrank-d_div_s-0-20-128-epar = ... (6) | ||||
pgrank-du-0-60-32-z3_4 | 47.717 | 857 | = pgrank-u-0-20-32-z3_4 = pgrank-d_div_s-0-20-128-epar = epcl-default-0-60-128-epar = ... (5) | ||||
pgrank-u-0-20-32-z3_4 | 47.773 | 858 | = pgrank-d_div_s-0-20-128-epar = epcl-default-0-60-128-epar = pgrank-u-0-20-128-epar = ... (4) | ||||
pgrank-d_div_s-0-20-128-epar | 47.829 | 859 | = epcl-default-0-60-128-epar = pgrank-u-0-20-128-epar | ||||
pgrank-u-0-20-128-epar | 47.884 | 860 |