benchmark type = generated benchmark name = ../benchmarks/min/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 = 380, 380, 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 31 444 982 982 26 959 9 0 49 0 5 0 1,2,5, 380,380,703, 2 i_10 1 16 621 1168 1168 15 1337 3 1 4 0 5 0 5, 959, 3 i_11 1 33 436 1823 1823 32 1506 3 1 4 0 5 0 5, 1337, 4 i_12 1 22 580 2115 2115 21 1856 3 1 4 0 5 0 5, 1506, 5 i_13 1 37 567 2738 2738 31 2195 3 1 4 0 5 1 5, 1856, 6 i_14 1 53 571 3323 3323 51 2545 3 2 4 0 5 0 5, 2195, 7 i_15 1 54 544 3948 3948 52 2874 3 2 4 0 5 0 5, 2545, 8 i_16 1 44 544 4546 4546 41 3208 3 0 4 0 5 1 5, 2874, 9 i_17 1 72 533 5168 5168 63 3536 3 3 4 0 5 0 5, 3208, 10 i_18 1 59 540 5763 5763 55 3875 3 3 4 0 5 0 5, 3536, 11 i_19 1 94 527 6368 6368 81 4206 3 7 4 0 5 1 5, 3875, 12 i_2 1 123 927 4352 4352 117 4835 3 2 4 0 5 0 5, 4206, 13 i_20 1 102 523 7996 7996 94 5167 3 3 4 0 5 0 5, 4835, 14 i_21 1 126 496 8586 8586 114 5478 3 6 4 0 5 0 5, 5167, 15 i_22 1 144 490 9147 9147 135 5788 3 3 4 0 5 1 5, 5478, 16 i_23 1 157 488 9713 9713 147 6101 3 5 4 0 5 0 5, 5788, 17 i_24 1 104 474 10291 10291 98 6405 3 5 4 0 5 0 5, 6101, 18 i_25 1 220 460 10846 10846 182 6700 3 31 4 0 5 1 5, 6405, 19 i_26 1 102 453 11383 11383 96 6993 3 4 4 1 5 1 5, 6700, 20 i_27 1 122 445 11923 11923 116 7282 3 4 4 0 5 1 5, 6993, 21 i_28 1 146 436 12459 12459 139 7567 3 4 4 0 5 1 5, 7282, 22 i_29 1 268 425 12982 12982 257 7847 3 6 4 0 5 1 5, 7567, 23 i_3 1 210 870 8618 8618 201 8471 3 5 4 0 5 1 5, 7847, 24 i_30 1 438 414 14602 14602 426 8745 3 7 4 0 5 1 5, 8471, 25 i_31 1 395 403 15109 15109 383 9012 3 8 4 0 5 0 5, 8745, 26 i_32 1 464 390 15599 15599 442 9270 3 11 4 0 5 0 5, 9012, 27 i_33 1 541 379 16077 16077 524 9521 3 9 4 0 5 1 5, 9270, 28 i_34 1 538 366 16536 16536 518 9763 3 7 4 0 5 2 5, 9521, 29 i_35 1 504 355 16992 16992 490 9998 3 10 4 0 5 1 5, 9763, 30 i_36 1 529 342 17444 17444 511 10224 3 15 4 0 5 0 5, 9998, 31 i_37 1 544 331 17885 17885 526 10443 3 16 4 0 5 0 5, 10224, 32 i_38 1 586 318 18298 18298 571 10653 3 12 4 0 5 0 5, 10443, 33 i_39 1 595 307 18697 18697 574 10856 3 12 4 0 5 0 5, 10653, 34 i_4 1 818 831 12181 12181 804 11479 3 10 4 0 5 1 5, 10856, 35 i_40 1 748 294 20153 20153 605 11673 3 125 4 0 5 1 5, 11479, 36 i_41 1 752 283 20530 20530 733 11860 3 11 4 0 5 1 5, 11673, 37 i_42 1 663 270 20887 20887 641 12038 3 18 4 0 5 1 5, 11860, 38 i_43 1 864 259 21232 21232 833 12209 3 22 4 0 5 1 5, 12038, 39 i_44 1 693 246 21573 21573 671 12371 3 10 4 0 5 1 5, 12209, 40 i_45 1 844 235 21895 21895 814 12526 3 16 4 0 5 1 5, 12371, 41 i_46 1 957 222 22203 22203 934 12672 3 19 4 0 5 0 5, 12526, 42 i_47 1 774 211 22498 22498 753 12811 3 18 4 0 5 1 5, 12672, 43 i_48 1 1049 198 22811 22811 1007 12941 3 27 4 0 5 1 5, 12811, 44 i_49 1 799 187 23082 23082 770 13064 3 15 4 0 5 1 5, 12941, 45 i_5 1 985 938 14934 14934 957 13827 3 23 4 0 5 1 5, 13064, 46 i_50 1 1085 174 24729 24729 1057 13941 3 23 4 0 5 1 5, 13827, 47 i_51 1 1148 163 24977 24977 1128 14048 3 16 4 0 5 1 5, 13941, 48 i_52 1 1170 150 25229 25229 1134 14146 3 26 4 0 5 0 5, 14048, 49 i_53 1 1047 139 25434 25434 1024 14237 3 18 4 0 5 0 5, 14146, 50 i_54 1 1074 126 25641 25641 1051 14319 3 12 4 0 5 1 5, 14237, 51 i_55 1 1302 115 25837 25837 1265 14394 3 28 4 1 5 0 5, 14319, 52 i_56 1 1226 102 26016 26016 1193 14460 3 29 4 0 5 1 5, 14394, 53 i_57 1 1226 91 26171 26171 1182 14518 3 29 4 0 5 1 5, 14460, 54 i_58 1 1357 76 26321 26321 1319 14567 3 31 4 0 5 1 5, 14518, 55 i_59 1 1432 67 26456 26456 1393 14610 3 30 4 0 5 1 5, 14567, 56 i_6 1 1364 886 17122 17122 1315 15337 3 39 4 0 5 1 5, 14610, 57 i_60 1 1397 52 27841 27841 1364 15369 3 28 4 0 5 1 5, 15337, 58 i_61 1 1373 41 27939 27939 1327 15394 3 42 4 0 5 1 5, 15369, 59 i_62 1 1640 23 28021 28021 1604 15406 3 31 4 0 5 1 5, 15394, 60 i_63 1 1568 10 28050 28050 1528 15408 3 30 4 0 5 1 5, 15406, 61 i_7 1 1679 1267 18476 18476 1641 16507 3 34 4 0 5 1 5, 15408, 62 i_8 1 1674 919 20185 20185 1642 17257 3 19 4 0 5 1 5, 16507, 63 i_9 1 1901 1300 21474 21474 1863 18382 3 22 4 0 5 1 5, 17257, 64 i_64 3 1598 3 32993 32997 1579 18382 6 14 41 0 5 1 3,4,5, 3,3,18382, total_number_of_compose_operations_in_initial_skolem_function_generation = 201 total_ComposeTime_in_initial_skolem_function_generation = 1021 milliseconds total_number_of_boolean_operations_in_initial_skolem_function_generation = 338 total_BooleanOpTime_in_initial_skolem_function_generation = 2 milliseconds total_number_of_support_operations_in_initial_skolem_function_generation = 320 total_FactorFindingTime_in_initial_skolem_function_generation = 42 milliseconds total-time-in-initial-skolem-function-generation-without-size-computation-time = 43501 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 = 43501 milliseconds total-time-in-reverse-substitution-without-size-computation-time = 2379 milliseconds total-time-without-size-computation-time = 45880 milliseconds total-time-in-interpolant-computation = 42260 algorithm-used = monolithic_compositionqe_interpolantskf_cofactorone ordering-used = least-occurring-first total time in ordering = 0 milliseconds total time in compute-size = 213 total time in compute-support = 25 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 = 190 milliseconds size_computation_time_in_reverse_substitution_in_cegar = 23 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 = 213 milliseconds compose-in-reverse-substitution = 2016 time-in-reverse-substitution = 2269 final-skolem-function-sizes = 17908, 11377, 10992, 10797, 10445, 10096, 9739, 9404, 9065, 8731, 8387, 14483, 8050, 7711, 7394, 7078, 6759, 6451, 6150, 5852, 5558, 5267, 10786, 4982, 4704, 4432, 4170, 3914, 3668, 3428, 3198, 2974, 2760, 7739, 2552, 2354, 2162, 1980, 1804, 1638, 1478, 1328, 1184, 1050, 5500, 922, 804, 692, 590, 494, 408, 328, 258, 194, 141, 3942, 93, 57, 26, 10, 3151, 2058, 1300, 3,