benchmark type = generated benchmark name = ../benchmarks/max/64.v problem = variable_elimination machine = prolient number of factors = 5 number of variables to eliminate = 64 number of variables = 192 aig sizes of factors = 379, 379, 3, 3, 703, variables in factors = 128, 128, 2, 2, 192, variables to eliminate in factors = 64, 64, 1, 1, 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 3 23 507 986 986 22 1019 9 0 49 0 5 1 1,2,5, 379,379,703, 2 i_10 1 20 673 1311 1311 19 1419 3 0 4 0 5 1 5, 1019, 3 i_11 1 32 513 2116 2116 31 1663 3 0 4 0 5 0 5, 1419, 4 i_12 1 26 710 2599 2599 23 2109 3 1 4 0 5 0 5, 1663, 5 i_13 1 55 439 3498 3498 54 2283 3 0 4 0 5 0 5, 2109, 6 i_14 1 60 597 3754 3754 44 2619 3 2 4 0 5 5 5, 2283, 7 i_15 1 46 656 4365 4365 38 3026 3 1 4 0 5 0 5, 2619, 8 i_16 1 72 639 5214 5214 55 3421 3 7 4 0 5 1 5, 3026, 9 i_17 1 62 654 6027 6027 59 3836 3 2 4 0 5 1 5, 3421, 10 i_18 1 89 620 6869 6869 77 4222 3 2 4 0 5 0 5, 3836, 11 i_19 1 102 599 7651 7651 98 4592 3 3 4 0 5 0 5, 4222, 12 i_2 1 145 1066 4873 4873 141 5374 3 2 4 0 5 1 5, 4592, 13 i_20 1 105 592 9636 9636 99 5742 3 4 4 0 5 0 5, 5374, 14 i_21 1 114 613 10387 10387 109 6136 3 4 4 0 5 0 5, 5742, 15 i_22 1 169 563 11186 11186 120 6485 3 23 4 0 5 1 5, 6136, 16 i_23 1 151 544 11953 11953 131 6820 3 14 4 0 5 0 5, 6485, 17 i_24 1 145 563 12654 12654 139 7179 3 5 4 0 5 0 5, 6820, 18 i_25 1 169 529 13387 13387 163 7509 3 5 4 0 5 0 5, 7179, 19 i_26 1 181 507 14044 14044 174 7822 3 5 4 0 5 1 5, 7509, 20 i_27 1 217 497 14699 14699 210 8130 3 5 4 0 5 0 5, 7822, 21 i_28 1 227 482 15328 15328 220 8428 3 6 4 0 5 0 5, 8130, 22 i_29 1 226 467 15935 15935 217 8716 3 6 4 0 5 1 5, 8428, 23 i_3 1 287 974 9350 9350 281 9419 3 5 4 0 5 1 5, 8716, 24 i_30 1 246 460 17661 17661 235 9705 3 9 4 0 5 1 5, 9419, 25 i_31 1 299 456 18258 18258 287 9992 3 8 4 0 5 1 5, 9705, 26 i_32 1 280 431 18957 18957 263 10259 3 10 4 0 5 0 5, 9992, 27 i_33 1 414 420 19518 19518 402 10520 3 11 4 0 5 0 5, 10259, 28 i_34 1 351 408 20034 20034 330 10774 3 17 4 0 5 0 5, 10520, 29 i_35 1 354 391 20569 20569 335 11016 3 17 4 0 5 0 5, 10774, 30 i_36 1 477 380 21067 21067 330 11252 3 144 4 0 5 1 5, 11016, 31 i_37 1 418 381 21561 21561 405 11494 3 7 4 0 5 1 5, 11252, 32 i_38 1 419 351 22041 22041 403 11711 3 9 4 0 5 0 5, 11494, 33 i_39 1 481 336 22496 22496 450 11918 3 28 4 0 5 1 5, 11711, 34 i_4 1 522 973 13049 13049 515 12676 3 5 4 0 5 0 5, 11918, 35 i_40 1 475 335 23847 23847 456 12887 3 17 4 0 5 0 5, 12676, 36 i_41 1 533 325 24301 24301 513 13093 3 17 4 0 5 1 5, 12887, 37 i_42 1 556 299 24715 24715 538 13278 3 10 4 0 5 0 5, 13093, 38 i_43 1 685 285 25104 25104 666 13454 3 16 4 0 5 1 5, 13278, 39 i_44 1 613 270 25449 25449 592 13620 3 17 4 0 5 1 5, 13454, 40 i_45 1 640 259 25804 25804 611 13780 3 19 4 0 5 1 5, 13620, 41 i_46 1 678 244 26120 26120 648 13930 3 18 4 0 5 0 5, 13780, 42 i_47 1 745 232 26446 26446 716 14073 3 24 4 0 5 1 5, 13930, 43 i_48 1 934 221 26778 26778 906 14210 3 24 4 0 5 0 5, 14073, 44 i_49 1 909 212 27077 27077 879 14343 3 26 4 0 5 1 5, 14210, 45 i_5 1 924 1102 16132 16132 905 15263 3 16 4 0 5 1 5, 14343, 46 i_50 1 913 195 28989 28989 885 15384 3 24 4 0 5 1 5, 15263, 47 i_51 1 913 179 29259 29259 835 15494 3 61 4 0 5 1 5, 15384, 48 i_52 1 962 164 29488 29488 918 15594 3 35 4 0 5 3 5, 15494, 49 i_53 1 992 155 29725 29725 952 15690 3 35 4 0 5 1 5, 15594, 50 i_54 1 1065 137 29912 29912 1010 15773 3 37 4 0 5 6 5, 15690, 51 i_55 1 1171 121 30104 30104 1113 15845 3 43 4 0 5 1 5, 15773, 52 i_56 1 1142 111 30235 30235 1101 15912 3 37 4 0 5 1 5, 15845, 53 i_57 1 1205 103 30391 30391 1150 15976 3 34 4 0 5 6 5, 15912, 54 i_58 1 1212 85 30515 30515 1167 16027 3 32 4 0 5 1 5, 15976, 55 i_59 1 1352 69 30644 30644 1271 16067 3 61 4 0 5 6 5, 16027, 56 i_6 1 1380 1299 18644 18644 1341 17203 3 26 4 0 5 1 5, 16067, 57 i_60 1 1316 56 32680 32680 1265 17235 3 31 4 0 5 6 5, 17203, 58 i_61 1 1364 43 32774 32774 1301 17259 3 49 4 0 5 1 5, 17235, 59 i_62 1 1570 24 32826 32826 1494 17270 3 69 4 0 5 2 5, 17259, 60 i_63 1 1524 13 32880 32880 1458 17275 3 51 4 0 5 7 5, 17270, 61 i_7 1 1532 1174 20670 20670 1489 18277 3 36 4 0 5 1 5, 17275, 62 i_8 1 1620 1190 22517 22517 1575 19272 3 39 4 0 5 0 5, 18277, 63 i_9 1 1612 1121 24112 24112 1538 20210 3 51 4 0 5 1 5, 19272, 64 i_64 3 1480 4 38003 37999 1435 20210 6 36 41 0 5 1 3,4,5, 3,3,20210, total_number_of_compose_operations_in_initial_skolem_function_generation = 201 total_ComposeTime_in_initial_skolem_function_generation = 1358 milliseconds total_number_of_boolean_operations_in_initial_skolem_function_generation = 338 total_BooleanOpTime_in_initial_skolem_function_generation = 0 milliseconds total_number_of_support_operations_in_initial_skolem_function_generation = 320 total_FactorFindingTime_in_initial_skolem_function_generation = 73 milliseconds total-time-in-initial-skolem-function-generation-without-size-computation-time = 38757 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 = 38757 milliseconds total-time-in-reverse-substitution-without-size-computation-time = 2635 milliseconds total-time-without-size-computation-time = 41393 milliseconds total-time-in-interpolant-computation = 37207 algorithm-used = monolithic_compositionqe_interpolantskf_cofactorone ordering-used = least-occurring-first total time in ordering = 0 milliseconds total time in compute-size = 286 total time in compute-support = 22 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 = 259 milliseconds size_computation_time_in_reverse_substitution_in_cegar = 27 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 = 286 milliseconds compose-in-reverse-substitution = 2016 time-in-reverse-substitution = 2460 final-skolem-function-sizes = 19766, 12294, 11889, 11639, 11187, 11002, 10653, 10240, 9839, 9418, 9026, 15952, 8650, 8276, 7876, 7521, 7180, 6815, 6479, 6160, 5846, 5542, 11805, 5248, 4956, 4663, 4390, 4123, 3863, 3615, 3373, 3125, 2902, 8555, 2689, 2472, 2260, 2069, 1887, 1715, 1549, 1393, 1244, 1101, 6088, 962, 835, 719, 613, 511, 422, 344, 271, 201, 144, 4336, 98, 60, 30, 14, 3132, 2138, 1122, 4,