Benchmark Properties Interpolation Properties iPrincess Results QE Results
Name Status Difficulty Category L/R Ratio (%) #C #LC Dec. Time (ms) IS Time (ms) IS Time (ms)
rings/ring_2exp10_3vars_0ite_unsat.pri unsat 0 crafted 60 81 31 4942 26 325 - T/O
rings/ring_2exp10_3vars_0ite_unsat.pri unsat 0 crafted 70 81 43 4942 20 326 - T/O
rings/ring_2exp10_3vars_0ite_unsat.pri unsat 0 crafted 80 81 55 4942 14 343 - T/O
rings/ring_2exp10_3vars_0ite_unsat.pri unsat 0 crafted 90 81 69 4942 7 350 - T/O
rings/ring_2exp10_3vars_1ite_unsat.pri unsat 1 crafted 10 81 69 5152 - T/O 19 11
rings/ring_2exp10_3vars_1ite_unsat.pri unsat 1 crafted 20 81 69 5152 - T/O 76 10
rings/ring_2exp10_3vars_1ite_unsat.pri unsat 1 crafted 60 75 27 5152 24 351 - T/O
rings/ring_2exp10_3vars_1ite_unsat.pri unsat 1 crafted 70 75 39 5152 19 344 - T/O
rings/ring_2exp10_3vars_1ite_unsat.pri unsat 1 crafted 80 75 51 5152 13 355 - T/O
rings/ring_2exp10_3vars_1ite_unsat.pri unsat 1 crafted 90 75 63 5152 7 345 - T/O
rings/ring_2exp10_3vars_2ite_unsat.pri unsat 0 crafted 10 69 3 4946 52 2588 18 16
rings/ring_2exp10_3vars_2ite_unsat.pri unsat 0 crafted 20 69 3 4946 - T/O 55 14
rings/ring_2exp10_3vars_2ite_unsat.pri unsat 0 crafted 30 69 3 4946 - T/O 294 33
rings/ring_2exp10_3vars_2ite_unsat.pri unsat 0 crafted 60 69 25 4946 22 314 - T/O
rings/ring_2exp10_3vars_2ite_unsat.pri unsat 0 crafted 70 69 37 4946 17 320 - T/O
rings/ring_2exp10_3vars_2ite_unsat.pri unsat 0 crafted 80 69 47 4946 12 343 - T/O
rings/ring_2exp10_3vars_2ite_unsat.pri unsat 0 crafted 90 69 59 4946 6 316 - T/O
rings/ring_2exp12_3vars_0ite_unsat.pri unsat 0 crafted 60 81 31 5024 26 322 - T/O
rings/ring_2exp12_3vars_0ite_unsat.pri unsat 0 crafted 70 81 43 5024 20 323 - T/O
rings/ring_2exp12_3vars_0ite_unsat.pri unsat 0 crafted 80 81 55 5024 14 348 - T/O
rings/ring_2exp12_3vars_0ite_unsat.pri unsat 0 crafted 90 81 69 5024 7 329 - T/O
rings/ring_2exp12_3vars_1ite_unsat.pri unsat 0 crafted 10 81 69 5132 - T/O 19 11
rings/ring_2exp12_3vars_1ite_unsat.pri unsat 0 crafted 20 81 69 5132 - T/O 76 10
rings/ring_2exp12_3vars_1ite_unsat.pri unsat 0 crafted 60 75 27 5132 24 346 - T/O
rings/ring_2exp12_3vars_1ite_unsat.pri unsat 0 crafted 70 75 39 5132 19 356 - T/O
rings/ring_2exp12_3vars_1ite_unsat.pri unsat 0 crafted 80 75 51 5132 13 365 - T/O
rings/ring_2exp12_3vars_1ite_unsat.pri unsat 0 crafted 90 75 63 5132 7 332 - T/O
rings/ring_2exp12_3vars_2ite_unsat.pri unsat 1 crafted 10 69 3 5044 52 2542 18 16
rings/ring_2exp12_3vars_2ite_unsat.pri unsat 1 crafted 20 69 3 5044 - T/O 55 17
rings/ring_2exp12_3vars_2ite_unsat.pri unsat 1 crafted 30 69 3 5044 - T/O 294 39
rings/ring_2exp12_3vars_2ite_unsat.pri unsat 1 crafted 60 69 25 5044 22 314 - T/O
rings/ring_2exp12_3vars_2ite_unsat.pri unsat 1 crafted 70 69 37 5044 17 458 - T/O
rings/ring_2exp12_3vars_2ite_unsat.pri unsat 1 crafted 80 69 47 5044 12 335 - T/O
rings/ring_2exp12_3vars_2ite_unsat.pri unsat 1 crafted 90 69 59 5044 6 343 - T/O
rings/ring_2exp14_3vars_0ite_unsat.pri unsat 0 crafted 60 81 31 4982 26 325 - T/O
rings/ring_2exp14_3vars_0ite_unsat.pri unsat 0 crafted 70 81 43 4982 20 322 - T/O
rings/ring_2exp14_3vars_0ite_unsat.pri unsat 0 crafted 80 81 55 4982 14 341 - T/O
rings/ring_2exp14_3vars_0ite_unsat.pri unsat 0 crafted 90 81 69 4982 7 344 - T/O
rings/ring_2exp14_3vars_1ite_unsat.pri unsat 0 crafted 10 81 69 5138 - T/O 19 11
rings/ring_2exp14_3vars_1ite_unsat.pri unsat 0 crafted 20 81 69 5138 - T/O 76 10
rings/ring_2exp14_3vars_1ite_unsat.pri unsat 0 crafted 60 75 27 5138 24 349 - T/O
rings/ring_2exp14_3vars_1ite_unsat.pri unsat 0 crafted 70 75 39 5138 19 347 - T/O
rings/ring_2exp14_3vars_1ite_unsat.pri unsat 0 crafted 80 75 51 5138 13 363 - T/O
rings/ring_2exp14_3vars_1ite_unsat.pri unsat 0 crafted 90 75 63 5138 7 324 - T/O
rings/ring_2exp14_3vars_2ite_unsat.pri unsat 1 crafted 10 69 3 5009 52 2578 18 14
rings/ring_2exp14_3vars_2ite_unsat.pri unsat 1 crafted 20 69 3 5009 - T/O 55 13
rings/ring_2exp14_3vars_2ite_unsat.pri unsat 1 crafted 30 69 3 5009 - T/O 294 32
rings/ring_2exp14_3vars_2ite_unsat.pri unsat 1 crafted 60 69 25 5009 22 315 - T/O
rings/ring_2exp14_3vars_2ite_unsat.pri unsat 1 crafted 70 69 37 5009 17 316 - T/O
rings/ring_2exp14_3vars_2ite_unsat.pri unsat 1 crafted 80 69 47 5009 12 335 - T/O
rings/ring_2exp14_3vars_2ite_unsat.pri unsat 1 crafted 90 69 59 5009 6 348 - T/O
rings/ring_2exp16_3vars_0ite_unsat.pri unsat 0 crafted 60 81 31 5005 26 309 - T/O
rings/ring_2exp16_3vars_0ite_unsat.pri unsat 0 crafted 70 81 43 5005 20 327 - T/O
rings/ring_2exp16_3vars_0ite_unsat.pri unsat 0 crafted 80 81 55 5005 14 334 - T/O
rings/ring_2exp16_3vars_0ite_unsat.pri unsat 0 crafted 90 81 69 5005 7 344 - T/O
rings/ring_2exp16_3vars_1ite_unsat.pri unsat 0 crafted 10 81 69 5202 - T/O 19 11
rings/ring_2exp16_3vars_1ite_unsat.pri unsat 0 crafted 20 81 69 5202 - T/O 76 10
rings/ring_2exp16_3vars_1ite_unsat.pri unsat 0 crafted 60 75 27 5202 24 347 - T/O
rings/ring_2exp16_3vars_1ite_unsat.pri unsat 0 crafted 70 75 39 5202 19 340 - T/O
rings/ring_2exp16_3vars_1ite_unsat.pri unsat 0 crafted 80 75 51 5202 13 348 - T/O
rings/ring_2exp16_3vars_1ite_unsat.pri unsat 0 crafted 90 75 63 5202 7 333 - T/O
rings/ring_2exp16_3vars_2ite_unsat.pri unsat 1 crafted 10 69 3 4987 52 2718 18 15
rings/ring_2exp16_3vars_2ite_unsat.pri unsat 1 crafted 20 69 3 4987 - T/O 55 14
rings/ring_2exp16_3vars_2ite_unsat.pri unsat 1 crafted 30 69 3 4987 - T/O 294 31
rings/ring_2exp16_3vars_2ite_unsat.pri unsat 1 crafted 60 69 25 4987 22 302 - T/O
rings/ring_2exp16_3vars_2ite_unsat.pri unsat 1 crafted 70 69 37 4987 17 318 - T/O
rings/ring_2exp16_3vars_2ite_unsat.pri unsat 1 crafted 80 69 47 4987 12 325 - T/O
rings/ring_2exp16_3vars_2ite_unsat.pri unsat 1 crafted 90 69 59 4987 6 321 - T/O
rings/ring_2exp4_3vars_0ite_unsat.pri unsat 0 crafted 50 81 21 4978 137 857 - T/O
rings/ring_2exp4_3vars_0ite_unsat.pri unsat 0 crafted 60 81 31 4978 26 338 - T/O
rings/ring_2exp4_3vars_0ite_unsat.pri unsat 0 crafted 70 81 43 4978 20 329 - T/O
rings/ring_2exp4_3vars_0ite_unsat.pri unsat 0 crafted 80 81 55 4978 14 310 - T/O
rings/ring_2exp4_3vars_0ite_unsat.pri unsat 0 crafted 90 81 69 4978 7 304 - T/O
rings/ring_2exp4_3vars_1ite_unsat.pri unsat 0 crafted 10 81 69 5153 - T/O 19 10
rings/ring_2exp4_3vars_1ite_unsat.pri unsat 0 crafted 20 81 69 5153 - T/O 76 10
rings/ring_2exp4_3vars_1ite_unsat.pri unsat 0 crafted 30 81 69 5153 - T/O 30442 16111
rings/ring_2exp4_3vars_1ite_unsat.pri unsat 0 crafted 50 75 21 5153 79 733 - T/O
rings/ring_2exp4_3vars_1ite_unsat.pri unsat 0 crafted 60 75 27 5153 24 340 - T/O
rings/ring_2exp4_3vars_1ite_unsat.pri unsat 0 crafted 70 75 39 5153 19 326 - T/O
rings/ring_2exp4_3vars_1ite_unsat.pri unsat 0 crafted 80 75 51 5153 13 309 - T/O
rings/ring_2exp4_3vars_1ite_unsat.pri unsat 0 crafted 90 75 63 5153 7 302 - T/O
rings/ring_2exp4_3vars_2ite_unsat.pri unsat 0 crafted 10 69 3 5043 52 2730 18 13
rings/ring_2exp4_3vars_2ite_unsat.pri unsat 0 crafted 20 69 3 5043 - T/O 55 14
rings/ring_2exp4_3vars_2ite_unsat.pri unsat 0 crafted 30 69 3 5043 - T/O 294 33
rings/ring_2exp4_3vars_2ite_unsat.pri unsat 0 crafted 50 69 20 5043 521 1035 - T/O
rings/ring_2exp4_3vars_2ite_unsat.pri unsat 0 crafted 60 69 25 5043 22 317 - T/O
rings/ring_2exp4_3vars_2ite_unsat.pri unsat 0 crafted 70 69 37 5043 17 319 - T/O
rings/ring_2exp4_3vars_2ite_unsat.pri unsat 0 crafted 80 69 47 5043 12 351 - T/O
rings/ring_2exp4_3vars_2ite_unsat.pri unsat 0 crafted 90 69 59 5043 6 282 - T/O
rings/ring_2exp6_3vars_0ite_unsat.pri unsat 0 crafted 50 81 21 5139 473 4167 - T/O
rings/ring_2exp6_3vars_0ite_unsat.pri unsat 0 crafted 60 81 31 5139 26 331 - T/O
rings/ring_2exp6_3vars_0ite_unsat.pri unsat 0 crafted 70 81 43 5139 20 323 - T/O
rings/ring_2exp6_3vars_0ite_unsat.pri unsat 0 crafted 80 81 55 5139 14 312 - T/O
rings/ring_2exp6_3vars_0ite_unsat.pri unsat 0 crafted 90 81 69 5139 7 299 - T/O
rings/ring_2exp6_3vars_1ite_unsat.pri unsat 1 crafted 10 81 69 5170 - T/O 19 10
rings/ring_2exp6_3vars_1ite_unsat.pri unsat 1 crafted 20 81 69 5170 - T/O 76 10
rings/ring_2exp6_3vars_1ite_unsat.pri unsat 1 crafted 50 75 21 5170 175 1624 - T/O
rings/ring_2exp6_3vars_1ite_unsat.pri unsat 1 crafted 60 75 27 5170 24 339 - T/O
rings/ring_2exp6_3vars_1ite_unsat.pri unsat 1 crafted 70 75 39 5170 19 318 - T/O
rings/ring_2exp6_3vars_1ite_unsat.pri unsat 1 crafted 80 75 51 5170 13 309 - T/O
rings/ring_2exp6_3vars_1ite_unsat.pri unsat 1 crafted 90 75 63 5170 7 305 - T/O
rings/ring_2exp6_3vars_2ite_unsat.pri unsat 0 crafted 10 69 3 4993 52 2611 18 14
rings/ring_2exp6_3vars_2ite_unsat.pri unsat 0 crafted 20 69 3 4993 - T/O 55 13
rings/ring_2exp6_3vars_2ite_unsat.pri unsat 0 crafted 30 69 3 4993 - T/O 294 32
rings/ring_2exp6_3vars_2ite_unsat.pri unsat 0 crafted 50 69 20 4993 1865 3863 - T/O
rings/ring_2exp6_3vars_2ite_unsat.pri unsat 0 crafted 60 69 25 4993 22 324 - T/O
rings/ring_2exp6_3vars_2ite_unsat.pri unsat 0 crafted 70 69 37 4993 17 331 - T/O
rings/ring_2exp6_3vars_2ite_unsat.pri unsat 0 crafted 80 69 47 4993 12 349 - T/O
rings/ring_2exp6_3vars_2ite_unsat.pri unsat 0 crafted 90 69 59 4993 6 283 - T/O
rings/ring_2exp8_3vars_0ite_unsat.pri unsat 0 crafted 50 81 21 4976 1817 69824 - T/O
rings/ring_2exp8_3vars_0ite_unsat.pri unsat 0 crafted 60 81 31 4976 26 322 - T/O
rings/ring_2exp8_3vars_0ite_unsat.pri unsat 0 crafted 70 81 43 4976 20 475 - T/O
rings/ring_2exp8_3vars_0ite_unsat.pri unsat 0 crafted 80 81 55 4976 14 341 - T/O
rings/ring_2exp8_3vars_0ite_unsat.pri unsat 0 crafted 90 81 69 4976 7 343 - T/O
rings/ring_2exp8_3vars_1ite_unsat.pri unsat 0 crafted 10 81 69 5070 - T/O 19 10
rings/ring_2exp8_3vars_1ite_unsat.pri unsat 0 crafted 20 81 69 5070 - T/O 76 10
rings/ring_2exp8_3vars_1ite_unsat.pri unsat 0 crafted 50 75 21 5070 559 31597 - T/O
rings/ring_2exp8_3vars_1ite_unsat.pri unsat 0 crafted 60 75 27 5070 24 338 - T/O
rings/ring_2exp8_3vars_1ite_unsat.pri unsat 0 crafted 70 75 39 5070 19 351 - T/O
rings/ring_2exp8_3vars_1ite_unsat.pri unsat 0 crafted 80 75 51 5070 13 376 - T/O
rings/ring_2exp8_3vars_1ite_unsat.pri unsat 0 crafted 90 75 63 5070 7 316 - T/O
rings/ring_2exp8_3vars_2ite_unsat.pri unsat 0 crafted 10 69 3 4997 52 2613 18 14
rings/ring_2exp8_3vars_2ite_unsat.pri unsat 0 crafted 20 69 3 4997 - T/O 55 13
rings/ring_2exp8_3vars_2ite_unsat.pri unsat 0 crafted 30 69 3 4997 - T/O 294 32
rings/ring_2exp8_3vars_2ite_unsat.pri unsat 0 crafted 50 69 20 4997 7241 44389 - T/O
rings/ring_2exp8_3vars_2ite_unsat.pri unsat 0 crafted 60 69 25 4997 22 315 - T/O
rings/ring_2exp8_3vars_2ite_unsat.pri unsat 0 crafted 70 69 37 4997 17 318 - T/O
rings/ring_2exp8_3vars_2ite_unsat.pri unsat 0 crafted 80 69 47 4997 12 351 - T/O
rings/ring_2exp8_3vars_2ite_unsat.pri unsat 0 crafted 90 69 59 4997 6 343 - T/O
Statistics
Number of benchmarks: 129
Number of benchmarks on which iPrincess is faster: 93
Number of benchmarks on which iPrincess is at least 1 order of magnitude faster: 90
Number of benchmarks on which iPrincess yields smaller interpolants: 93
Number of benchmarks on which iPrincess yiels interpolants that are 1 order of magnitude smaller: 93
Legend
L/R Ratio: Ratio of the number of conjuncts on the left and on the right part of the formula
#C: Number of constants in the input formula
#LC: Number of local constants in the input formula (constants occuring in the left part of the formula only)
IS: Size of the generated interpolant (number of operators)
T/O: Timeout
O/M: Out of Memory