benchmark type = generated benchmark name = ../benchmarks/decomposition/32.v problem = variable_elimination machine = prolient number of factors = 62 number of variables to eliminate = 64 number of variables = 96 aig sizes of factors = 193, 193, 183, 187, 187, 175, 175, 169, 169, 163, 163, 157, 157, 151, 151, 145, 145, 139, 139, 133, 133, 127, 127, 121, 121, 115, 115, 109, 109, 103, 103, 97, 97, 91, 91, 85, 85, 79, 79, 73, 73, 67, 67, 61, 61, 55, 55, 49, 49, 43, 43, 37, 37, 13, 19, 13, 25, 25, 9, 19, 31, 31, variables in factors = 65, 65, 61, 63, 63, 59, 59, 57, 57, 55, 55, 53, 53, 51, 51, 49, 49, 47, 47, 45, 45, 43, 43, 41, 41, 39, 39, 37, 37, 35, 35, 33, 33, 31, 31, 29, 29, 27, 27, 25, 25, 23, 23, 21, 21, 19, 19, 17, 17, 15, 15, 13, 13, 5, 7, 5, 9, 9, 3, 7, 11, 11, variables to eliminate in factors = 64, 64, 60, 62, 62, 58, 58, 56, 56, 54, 54, 52, 52, 50, 50, 48, 48, 46, 46, 44, 44, 42, 42, 40, 40, 38, 38, 36, 36, 34, 34, 32, 32, 30, 30, 28, 28, 26, 26, 24, 24, 22, 22, 20, 20, 18, 18, 16, 16, 14, 14, 12, 12, 4, 6, 4, 8, 8, 2, 6, 10, 10, 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_32 2 4 410 204 204 3 479 6 0 82 0 62 1 1,2, 193,193, 2 i_2_32 1 4 1 494 494 3 459 3 0 4 0 62 1 2, 479, 3 i_1_31 3 6 696 504 504 5 1033 9 0 45 0 62 1 2,4,5, 459,187,187, 4 i_2_31 1 9 39 1344 1344 7 1066 3 1 4 0 62 1 5, 1033, 5 i_1_30 2 12 319 1390 1390 9 1266 6 0 21 0 62 1 3,5, 183,1066, 6 i_2_30 1 11 1 1596 1596 10 1156 3 0 4 0 62 1 5, 1266, 7 i_1_29 3 12 308 1462 1462 10 1252 9 1 45 0 62 1 5,6,7, 1156,175,175, 8 i_2_29 1 20 85 1552 1552 18 1328 3 1 4 0 62 1 7, 1252, 9 i_1_28 3 13 453 1712 1712 10 1669 9 2 45 0 62 1 7,8,9, 1328,169,169, 10 i_2_28 1 45 29 2101 2101 44 1689 3 0 4 0 62 1 9, 1669, 11 i_1_27 3 16 329 2137 2137 14 1826 9 1 45 0 62 1 9,10,11, 1689,163,163, 12 i_2_27 1 75 1788 2246 2246 73 3513 3 1 4 0 62 1 11, 1826, 13 i_1_26 3 28 328 4892 4892 25 3729 9 2 45 0 62 1 11,12,13, 3513,157,157, 14 i_2_26 1 115 1 5084 5084 112 3440 3 2 4 0 62 1 13, 3729, 15 i_1_25 3 27 280 4690 4690 24 3619 9 1 45 0 62 1 13,14,15, 3440,151,151, 16 i_2_25 1 103 3468 4854 4854 100 6918 3 1 4 0 62 1 15, 3619, 17 i_1_24 3 43 383 8481 8481 37 7189 9 3 45 0 62 2 15,16,17, 6918,145,145, 18 i_2_24 1 578 367 8906 8906 568 7538 3 3 4 0 62 1 17, 7189, 19 i_1_23 3 77 318 10010 10010 69 7767 9 5 45 0 62 1 17,18,19, 7538,139,139, 20 i_2_23 1 655 1 10382 10382 645 7580 3 3 4 0 62 5 19, 7767, 21 i_1_22 3 145 288 10322 10322 134 7773 9 6 45 0 62 1 19,20,21, 7580,133,133, 22 i_2_22 1 1034 14894 10492 10492 1009 22427 3 20 4 0 62 2 21, 7773, 23 i_1_21 3 215 344 29990 29990 191 22680 9 14 45 0 62 2 21,22,23, 22427,127,127, 24 i_2_21 1 4727 1 30515 30515 4698 22107 3 20 4 0 62 2 23, 22680, 25 i_1_20 3 647 309 29578 29578 628 22328 9 14 45 0 62 2 23,24,25, 22107,121,121, 26 i_2_20 1 6008 24604 29941 29941 5966 46375 3 35 4 0 62 2 25, 22328, 27 i_1_19 3 754 525 62296 62296 664 46806 9 70 45 0 62 3 25,26,27, 46375,115,115, 28 i_2_19 1 9923 1 63956 63956 9742 44555 3 167 4 0 62 3 27, 46806, 29 i_1_18 3 819 199 55336 55336 765 44672 9 41 45 0 62 3 27,28,29, 44555,109,109, 30 i_2_18 1 19718 14688 60949 60949 19626 58992 3 57 4 0 62 2 29, 44672, 31 i_1_17 3 3706 314 84961 84961 3593 59231 9 91 45 0 62 3 29,30,31, 58992,103,103, 32 i_2_17 1 28993 14838 85374 85374 28857 73644 3 97 4 0 62 3 31, 59231, 33 i_1_16 3 2117 309 117639 117639 1965 73891 9 114 45 0 62 4 31,32,33, 73644,97,97, 34 i_2_16 1 33606 11470 117863 117863 33412 84954 3 144 4 0 62 5 33, 73891, 35 i_1_15 3 3867 231 133802 133802 3643 85126 9 163 45 0 62 7 33,34,35, 84954,91,91, 36 i_2_15 1 38624 9350 133858 133858 38420 94203 3 150 4 0 62 10 35, 85126, 37 i_1_14 3 1905 151 153951 153951 1704 94297 9 142 45 0 62 13 35,36,37, 94203,85,85, 38 i_2_14 1 44831 9739 153533 153533 44641 103665 3 136 4 0 62 11 37, 94297, 39 i_1_13 3 5399 272 171325 171325 5171 103887 9 162 45 0 62 9 37,38,39, 103665,79,79, 40 i_2_13 1 45655 9631 171056 171056 45411 113173 3 188 4 0 62 9 39, 103887, 41 i_1_12 3 8964 245 190312 190312 8680 113358 9 206 45 0 62 14 39,40,41, 113173,73,73, 42 i_2_12 1 57099 16500 189881 189881 56814 129432 3 199 4 1 62 11 41, 113358, 43 i_1_11 3 4060 121 215854 215854 3743 129514 9 234 45 0 62 16 41,42,43, 129432,67,67, 44 i_2_11 1 62097 13196 215353 215353 61815 142221 3 206 4 0 62 16 43, 129514, 45 i_1_10 3 5255 145 236764 236764 4974 142314 9 201 45 0 62 9 43,44,45, 142221,61,61, 46 i_2_10 1 78896 12672 236354 236354 78587 154503 3 216 4 0 62 17 45, 142314, 47 i_1_9 3 7816 111 257449 257449 7594 154574 9 171 45 1 62 12 45,46,47, 154503,55,55, 48 i_2_9 1 80593 10839 257628 257628 80359 165049 3 179 4 0 62 13 47, 154574, 49 i_1_8 3 5155 152 280243 280243 4775 165162 9 327 45 0 62 12 47,48,49, 165049,49,49, 50 i_2_8 1 100851 12973 280047 280047 99410 177709 3 1365 4 0 62 22 49, 165162, 51 i_1_7 3 8502 246 305173 305173 8130 177920 9 285 45 0 62 22 49,50,51, 177709,43,43, 52 i_2_7 1 217809 20237 304344 304344 217463 197745 3 254 4 0 62 21 51, 177920, 53 i_1_6 3 8919 68 345330 345330 8492 197789 9 301 45 0 62 26 51,52,53, 197745,37,37, 54 i_2_6 1 238389 1 344616 344616 235328 194420 3 2871 4 0 62 15 53, 197789, 55 i_1_5 3 15519 69 342343 342343 12190 194468 9 2927 45 0 62 63 53,61,62, 194420,31,31, total-time-in-initial-skolem-function-generation-without-size-computation-time = 0 milliseconds total-time-in-reverse-substitution-without-size-computation-time = 0 milliseconds total-time-without-size-computation-time = 1336382 milliseconds total-time-in-interpolant-computation = 1322262 algorithm-used = monolithic_compositionqe_interpolantskf_cofactorone ordering-used = least-occurring-first total time in ordering = 0 milliseconds total time in compute-size = 1678 total time in compute-support = 198 total time in initialization of skolem function generator-without-size-computation-time = 6 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 = 0 milliseconds size_computation_time_in_reverse_substitution_in_cegar = 0 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 = 1678 milliseconds compose-in-reverse-substitution = 2 time-in-reverse-substitution = 765 final-skolem-function-sizes =