benchmark type = generated benchmark name = ../benchmarks/avgceiling/64.v problem = variable_elimination machine = prolient number of factors = 1 number of variables to eliminate = 64 number of variables = 192 aig sizes of factors = 1333, variables in factors = 192, variables to eliminate in factors = 64, i: index of variable to be eliminated v: name of variable to be eliminated F_v: Number of factors with the variable to be eliminated T_v: Time (in milliseconds) to eliminate the variable N_v: Size of the skolem function psi_i = interpolant between alpha_i and beta_i Q_v: Size of the quantified result q_i = conjunction of factors with variable substituted by skolem function A_v: Size of alpha_i B_v: Size of beta_i I_T: Time consumed in computing interpolant between alpha_i and beta_i cmp_v: Number of composes in elimination of the variable cmp_T: Time consumed in composes in elimination of the variable B_v: Number of boolean operations in elimination of the variable B_T: Time consumed in boolean operations in elimination of the variable S_v: Number of support operations in elimination of the variable S_T: Time consumed in support operations in elimination of the variable I_v: Indices of factors containing the variable to be eliminated X_v: Sizes of factors containing the variable to be eliminated i v F_v T_v N_v A_v B_v I_T Q_v cmp_v cmp_T B_v B_T S_v S_T I_v X_v 1 i_1 1 2 21 1516 1516 2 1345 3 0 4 0 1 0 1, 1333, 2 i_10 1 5 42 1507 1507 5 1377 3 0 4 0 1 0 1, 1345, 3 i_11 1 10 54 1537 1537 7 1417 3 1 4 0 1 0 1, 1377, 4 i_12 1 8 105 1574 1574 7 1499 3 0 4 0 1 1 1, 1417, 5 i_13 1 13 150 1653 1653 12 1619 3 0 4 0 1 1 1, 1499, 6 i_14 1 16 147 1770 1770 15 1737 3 1 4 0 1 0 1, 1619, 7 i_15 1 16 169 1886 1886 11 1870 3 1 4 0 1 0 1, 1737, 8 i_16 1 19 280 2016 2016 19 2108 3 0 4 0 1 0 1, 1870, 9 i_17 1 27 296 2251 2251 26 2359 3 0 4 0 1 1 1, 2108, 10 i_18 1 33 252 2499 2499 32 2564 3 1 4 0 1 0 1, 2359, 11 i_19 1 29 280 2702 2702 28 2786 3 1 4 0 1 0 1, 2564, 12 i_2 1 20 36 2971 2971 18 2808 3 2 4 0 1 0 1, 2786, 13 i_20 1 36 464 2943 2943 34 3213 3 1 4 0 1 0 1, 2808, 14 i_21 1 46 339 3345 3345 39 3475 3 2 4 0 1 0 1, 3213, 15 i_22 1 48 587 3604 3604 45 3991 3 0 4 0 1 1 1, 3475, 16 i_23 1 68 382 4118 4118 68 4297 3 0 4 0 1 0 1, 3991, 17 i_24 1 78 860 4421 4421 77 5066 3 0 4 0 1 1 1, 4297, 18 i_25 1 93 710 5187 5187 86 5689 3 6 4 0 1 1 1, 5066, 19 i_26 1 100 612 5807 5807 93 6212 3 2 4 0 1 1 1, 5689, 20 i_27 1 93 618 6328 6328 91 6738 3 1 4 0 1 1 1, 6212, 21 i_28 1 120 600 6851 6851 111 7219 3 2 4 0 1 0 1, 6738, 22 i_29 1 176 540 7329 7329 173 7642 3 3 4 0 1 0 1, 7219, 23 i_3 1 55 61 7824 7824 50 7685 3 2 4 0 1 1 1, 7642, 24 i_30 1 82 254 7792 7792 67 7802 3 13 4 0 1 1 1, 7685, 25 i_31 1 122 382 7934 7934 112 8026 3 2 4 0 1 0 1, 7802, 26 i_32 1 153 1113 8128 8128 145 8995 3 2 4 0 1 1 1, 8026, 27 i_33 1 159 424 9094 9094 153 9282 3 2 4 0 1 0 1, 8995, 28 i_34 1 184 988 9378 9378 181 10142 3 2 4 0 1 1 1, 9282, 29 i_35 1 196 789 10236 10236 188 10760 3 3 4 0 1 1 1, 10142, 30 i_36 1 193 935 10851 10851 189 11547 3 3 4 0 1 0 1, 10760, 31 i_37 1 242 600 11635 11635 235 11977 3 2 4 0 1 0 1, 11547, 32 i_38 1 354 1875 12062 12062 350 13662 3 2 4 0 1 1 1, 11977, 33 i_39 1 283 1253 13745 13745 273 14733 3 7 4 0 1 0 1, 13662, 34 i_4 1 55 55 14912 14912 44 14765 3 5 4 0 1 1 1, 14733, 35 i_40 1 285 862 14845 14845 278 15431 3 5 4 0 1 1 1, 14765, 36 i_41 1 381 1630 15508 15508 366 16863 3 10 4 0 1 1 1, 15431, 37 i_42 1 380 1348 16937 16937 368 18018 3 5 4 0 1 1 1, 16863, 38 i_43 1 332 1182 18090 18090 324 19001 3 5 4 0 1 1 1, 18018, 39 i_44 1 424 1411 19070 19070 411 20225 3 6 4 0 1 0 1, 19001, 40 i_45 1 487 1788 20291 20291 477 21788 3 8 4 0 1 0 1, 20225, 41 i_46 1 407 946 21851 21851 396 22519 3 7 4 0 1 1 1, 21788, 42 i_47 1 562 1363 22975 22975 547 23672 3 6 4 0 1 1 1, 22519, 43 i_48 1 512 1150 23730 23730 499 24557 3 9 4 0 1 1 1, 23672, 44 i_49 1 576 1235 24612 24612 565 25574 3 7 4 0 1 1 1, 24557, 45 i_5 1 121 92 25750 25750 98 25639 3 17 4 0 1 1 1, 25574, 46 i_50 1 568 1471 25691 25691 547 26839 3 11 4 0 1 6 1, 25639, 47 i_51 1 527 1295 26889 26889 507 27905 3 7 4 0 1 1 1, 26839, 48 i_52 1 766 1349 27952 27952 752 29009 3 7 4 0 1 1 1, 27905, 49 i_53 1 668 2869 29053 29053 652 31618 3 12 4 0 1 2 1, 29009, 50 i_54 1 858 1513 31659 31659 844 32901 3 9 4 0 1 1 1, 31618, 51 i_55 1 902 1982 32939 32939 882 34600 3 16 4 0 1 1 1, 32901, 52 i_56 1 780 3010 34635 34635 759 37315 3 16 4 0 1 2 1, 34600, 53 i_57 1 923 1382 37347 37347 881 38377 3 22 4 0 1 3 1, 37315, 54 i_58 1 942 1290 38406 38406 914 39353 3 14 4 0 1 2 1, 38377, 55 i_59 1 867 1634 39378 39378 851 40720 3 12 4 0 1 1 1, 39353, 56 i_6 1 174 124 40893 40893 151 40809 3 17 4 0 1 2 1, 40720, 57 i_60 1 901 2436 40830 40830 870 42938 3 10 4 0 1 5 1, 40809, 58 i_61 1 1045 1239 42955 42955 1027 43892 3 13 4 0 1 2 1, 42938, 59 i_62 1 1094 1126 43905 43905 1068 44766 3 12 4 0 1 2 1, 43892, 60 i_63 1 897 3057 44776 44776 867 47527 3 19 4 0 1 2 1, 44766, 61 i_64 1 756 655 49963 49963 722 47943 3 26 4 0 1 1 1, 47527, 62 i_7 1 219 149 48114 48114 185 48048 3 19 4 0 1 2 1, 47943, 63 i_8 1 236 154 48216 48216 181 48152 3 37 4 0 1 2 1, 48048, 64 i_9 1 420 242 78560 78560 377 48152 2 29 4 0 1 2 1, 48152, total_number_of_compose_operations_in_initial_skolem_function_generation = 191 total_ComposeTime_in_initial_skolem_function_generation = 462 milliseconds total_number_of_boolean_operations_in_initial_skolem_function_generation = 256 total_BooleanOpTime_in_initial_skolem_function_generation = 0 milliseconds total_number_of_support_operations_in_initial_skolem_function_generation = 64 total_FactorFindingTime_in_initial_skolem_function_generation = 64 milliseconds total-time-in-initial-skolem-function-generation-without-size-computation-time = 20980 milliseconds total time in initialization of skolem function generator-without-size-computation-time = 1 total-time-in-initial-skolem-function-generation-without-size-computation-time = 20980 milliseconds total-time-in-reverse-substitution-without-size-computation-time = 390 milliseconds total-time-without-size-computation-time = 21371 milliseconds total-time-in-interpolant-computation = 20352 algorithm-used = monolithic_compositionqe_interpolantskf_cofactorone ordering-used = least-occurring-first total time in ordering = 0 milliseconds total time in compute-size = 182 total time in compute-support = 28 total time in initialization of skolem function generator-without-size-computation-time = 1 total time in sat solving = 0 solver used = abc number of cegar iterations = 0 Compose Details: Hit_1 = 0 Miss_1 = 0 Hit_2 = 0 Miss_2 = 0 Leaves = 0 Non-leaves = 0 No-create-expr = 0 Create-expr = 0 Create-expr/Miss_2 = -nan size_computation_time_in_initialization = 0 milliseconds size_computation_time_in_initial_abstraction_generation_in_cegar = 179 milliseconds size_computation_time_in_reverse_substitution_in_cegar = 3 milliseconds size_computation_time_in_cegar_loops_in_cegar = 0 milliseconds size_computation_time_in_connection_substitution_in_cegar = 0 milliseconds total_time_in_compute_size = 182 milliseconds compose-in-reverse-substitution = 2016 time-in-reverse-substitution = 277 final-skolem-function-sizes = 21, 279, 291, 342, 387, 384, 402, 517, 533, 489, 517, 36, 701, 572, 824, 619, 1093, 947, 849, 855, 833, 773, 61, 733, 615, 1346, 657, 1221, 1022, 1172, 826, 2109, 1490, 55, 1096, 1867, 1581, 1416, 1648, 2021, 2363, 1593, 1387, 1468, 92, 1704, 1532, 1582, 3102, 1746, 2213, 3243, 1619, 1523, 1841, 124, 2669, 1476, 1356, 3723, 892, 149, 154, 242,