benchmark type = generated benchmark name = ../benchmarks/subtraction/64.v problem = variable_elimination machine = prolient number of factors = 126 number of variables to eliminate = 64 number of variables = 192 aig sizes of factors = 375, 379, 379, 367, 367, 361, 361, 355, 355, 349, 349, 343, 343, 337, 337, 331, 331, 325, 325, 319, 319, 313, 313, 307, 307, 301, 301, 295, 295, 289, 289, 283, 283, 277, 277, 271, 271, 265, 265, 259, 259, 253, 253, 247, 247, 241, 241, 235, 235, 229, 229, 223, 223, 217, 217, 211, 211, 205, 205, 199, 199, 193, 193, 187, 187, 181, 181, 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, 385, 385, variables in factors = 125, 127, 127, 123, 123, 121, 121, 119, 119, 117, 117, 115, 115, 113, 113, 111, 111, 109, 109, 107, 107, 105, 105, 103, 103, 101, 101, 99, 99, 97, 97, 95, 95, 93, 93, 91, 91, 89, 89, 87, 87, 85, 85, 83, 83, 81, 81, 79, 79, 77, 77, 75, 75, 73, 73, 71, 71, 69, 69, 67, 67, 65, 65, 63, 63, 61, 61, 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, 129, 129, variables to eliminate in factors = 62, 63, 63, 61, 61, 60, 60, 59, 59, 58, 58, 57, 57, 56, 56, 55, 55, 54, 54, 53, 53, 52, 52, 51, 51, 50, 50, 49, 49, 48, 48, 47, 47, 46, 46, 45, 45, 44, 44, 43, 43, 42, 42, 41, 41, 40, 40, 39, 39, 38, 38, 37, 37, 36, 36, 35, 35, 34, 34, 33, 33, 32, 32, 31, 31, 30, 30, 29, 29, 28, 28, 27, 27, 26, 26, 25, 25, 24, 24, 23, 23, 22, 22, 21, 21, 20, 20, 19, 19, 18, 18, 17, 17, 16, 16, 15, 15, 14, 14, 13, 13, 12, 12, 11, 11, 10, 10, 9, 9, 8, 8, 7, 7, 6, 6, 2, 3, 2, 4, 4, 1, 3, 5, 5, 64, 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_64 2 27 1030 396 396 12 1163 6 0 146 0 126 15 125,126, 385,385, 2 i_63 3 56 942 1281 1281 36 1788 9 1 45 0 126 19 2,3,126, 379,379,1163, 3 i_62 2 59 1669 2039 2039 44 3173 6 1 21 0 126 10 1,126, 375,1788, 4 i_61 3 109 1222 4316 4316 93 4137 9 1 45 0 126 9 4,5,126, 367,367,3173, 5 i_60 3 148 1615 5782 5782 135 5463 9 2 45 0 126 5 6,7,126, 361,361,4137, 6 i_59 3 145 1288 7797 7797 129 6485 9 3 45 0 126 4 8,9,126, 355,355,5463, 7 i_58 3 166 1004 9319 9319 153 7232 9 4 45 1 126 7 10,11,126, 349,349,6485, 8 i_57 3 160 1291 10401 10401 139 8276 9 3 45 0 126 6 12,13,126, 343,343,7232, 9 i_56 3 201 1033 12023 12023 179 9058 9 5 45 0 126 5 14,15,126, 337,337,8276, 10 i_55 3 266 1869 13214 13214 250 10613 9 4 45 0 126 5 16,17,126, 331,331,9058, 11 i_54 3 313 838 15638 15638 290 11224 9 11 45 0 126 5 18,19,126, 325,325,10613, 12 i_53 3 307 803 16580 16580 284 11795 9 6 45 0 126 8 20,21,126, 319,319,11224, 13 i_52 3 345 664 17590 17590 289 12235 9 50 45 0 126 5 22,23,126, 313,313,11795, 14 i_51 3 354 1147 18219 18219 322 13155 9 6 45 0 126 4 24,25,126, 307,307,12235, 15 i_50 3 375 660 19784 19784 349 13600 9 16 45 0 126 8 26,27,126, 301,301,13155, 16 i_49 3 522 980 20520 20520 499 14351 9 14 45 0 126 4 28,29,126, 295,295,13600, 17 i_48 3 550 1005 21871 21871 514 15135 9 9 45 0 126 12 30,31,126, 289,289,14351, 18 i_47 3 426 1228 23295 23295 405 16135 9 10 45 0 126 4 32,33,126, 283,283,15135, 19 i_46 3 557 1807 24851 24851 524 17730 9 20 45 0 126 11 34,35,126, 277,277,16135, 20 i_45 3 610 881 28179 28179 591 18402 9 13 45 0 126 4 36,37,126, 271,271,17730, 21 i_44 3 701 632 29315 29315 649 18851 9 30 45 0 126 10 38,39,126, 265,265,18402, 22 i_43 3 855 966 30034 30034 820 19622 9 28 45 0 126 4 40,41,126, 259,259,18851, 23 i_42 3 938 2106 31233 31233 887 21511 9 39 45 0 126 3 42,43,126, 253,253,19622, 24 i_41 3 672 541 34328 34328 626 21858 9 32 45 0 126 3 44,45,126, 247,247,21511, 25 i_40 3 1084 567 35073 35073 826 22229 9 239 45 0 126 10 46,47,126, 241,241,21858, 26 i_39 3 1007 371 35806 35806 965 22441 9 17 45 0 126 5 48,49,126, 235,235,22229, 27 i_38 3 821 819 36452 36452 776 23085 9 29 45 0 126 4 50,51,126, 229,229,22441, 28 i_37 3 978 615 37693 37693 937 23523 9 25 45 0 126 3 52,53,126, 223,223,23085, 29 i_36 3 996 661 38573 38573 971 23999 9 17 45 0 126 2 54,55,126, 217,217,23523, 30 i_35 3 995 1237 39522 39522 967 25053 9 20 45 0 126 3 56,57,126, 211,211,23999, 31 i_34 3 965 492 41658 41658 908 25378 9 34 45 0 126 8 58,59,126, 205,205,25053, 32 i_33 3 1101 381 42434 42434 1053 25605 9 31 45 0 126 7 60,61,126, 199,199,25378, 33 i_32 3 1320 585 42897 42897 1258 26033 9 41 45 0 126 8 62,63,126, 193,193,25605, 34 i_31 3 1388 468 43818 43818 1332 26356 9 45 45 1 126 3 64,65,126, 187,187,26033, 35 i_30 3 1328 456 44617 44617 1279 26665 9 37 45 0 126 2 66,67,126, 181,181,26356, 36 i_29 3 1442 605 45411 45411 1379 27129 9 41 45 5 126 8 68,69,126, 175,175,26665, 37 i_28 3 1372 400 46544 46544 1319 27395 9 39 45 0 126 2 70,71,126, 169,169,27129, 38 i_27 3 1384 308 47169 47169 1317 27589 9 40 45 0 126 3 72,73,126, 163,163,27395, 39 i_26 3 1528 320 47722 47722 1451 27799 9 50 45 0 126 3 74,75,126, 157,157,27589, 40 i_25 3 1774 563 48434 48434 1704 28251 9 58 45 0 126 3 76,77,126, 151,151,27799, 41 i_24 3 1747 330 49582 49582 1670 28476 9 60 45 0 126 2 78,79,126, 145,145,28251, 42 i_23 3 1932 210 50106 50106 1861 28577 9 56 45 0 126 2 80,81,126, 139,139,28476, 43 i_22 3 2246 474 50631 50631 2164 28948 9 58 45 0 126 2 82,83,126, 133,133,28577, 44 i_21 3 2001 398 51586 51586 1916 29246 9 74 45 0 126 3 84,85,126, 127,127,28948, 45 i_20 3 2311 381 52420 52420 2241 29527 9 56 45 0 126 2 86,87,126, 121,121,29246, 46 i_19 3 2184 243 53050 53050 2102 29685 9 66 45 0 126 1 88,89,126, 115,115,29527, 47 i_18 3 2073 207 53575 53575 1986 29807 9 76 45 0 126 2 90,91,126, 109,109,29685, 48 i_17 3 2409 287 54095 54095 2321 30016 9 79 45 0 126 1 92,93,126, 103,103,29807, 49 i_16 3 3251 284 54877 54877 2301 30223 9 941 45 0 126 5 94,95,126, 97,97,30016, 50 i_15 3 2379 267 55500 55500 2318 30415 9 34 45 0 126 2 96,97,126, 91,91,30223, 51 i_14 3 2292 159 56196 56196 2227 30508 9 52 45 0 126 2 98,99,126, 85,85,30415, 52 i_13 3 2447 191 56675 56675 2377 30642 9 47 45 0 126 1 100,101,126, 79,79,30508, 53 i_12 3 2488 155 57378 57378 2418 30743 9 51 45 0 126 2 102,103,126, 73,73,30642, 54 i_11 3 2786 108 57772 57772 2710 30798 9 63 45 0 126 2 104,105,126, 67,67,30743, 55 i_10 3 2651 177 58261 58261 2573 30934 9 68 45 0 126 2 106,107,126, 61,61,30798, 56 i_9 3 3003 240 58657 58657 2915 31141 9 62 45 0 126 2 108,109,126, 55,55,30934, 57 i_8 3 3037 153 59352 59352 2966 31248 9 60 45 0 126 1 110,111,126, 49,49,31141, 58 i_7 3 3184 119 59868 59868 3107 31338 9 55 45 0 126 1 112,113,126, 43,43,31248, 59 i_6 3 3279 62 60518 60518 3192 31375 9 69 45 0 126 1 114,115,126, 37,37,31338, 60 i_5 3 3044 87 60933 60933 2963 31451 9 60 45 1 126 2 123,124,126, 31,31,31375, 61 i_4 3 3311 70 61294 61294 3231 31513 9 65 45 0 126 2 119,120,126, 25,25,31451, 62 i_3 3 3118 32 61551 61551 3040 31540 9 66 45 0 126 2 117,122,126, 19,19,31513, 63 i_2 3 3430 29 61602 61602 3350 31572 9 65 45 0 126 1 116,118,126, 13,13,31540, 64 i_1 2 3419 7 62201 62201 3367 31572 4 35 20 1 126 5 121,126, 9,31572, total_number_of_compose_operations_in_initial_skolem_function_generation = 565 total_ComposeTime_in_initial_skolem_function_generation = 3389 milliseconds total_number_of_boolean_operations_in_initial_skolem_function_generation = 2932 total_BooleanOpTime_in_initial_skolem_function_generation = 9 milliseconds total_number_of_support_operations_in_initial_skolem_function_generation = 8064 total_FactorFindingTime_in_initial_skolem_function_generation = 292 milliseconds total-time-in-initial-skolem-function-generation-without-size-computation-time = 91975 milliseconds total time in initialization of skolem function generator-without-size-computation-time = 36 total-time-in-initial-skolem-function-generation-without-size-computation-time = 91975 milliseconds total-time-in-reverse-substitution-without-size-computation-time = 5196 milliseconds total-time-without-size-computation-time = 97171 milliseconds total-time-in-interpolant-computation = 87977 algorithm-used = monolithic_compositionqe_interpolantskf_cofactorone ordering-used = least-occurring-first total time in ordering = 0 milliseconds total time in compute-size = 501 total time in compute-support = 237 total time in initialization of skolem function generator-without-size-computation-time = 36 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 = 437 milliseconds size_computation_time_in_reverse_substitution_in_cegar = 64 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 = 501 milliseconds compose-in-reverse-substitution = 2016 time-in-reverse-substitution = 5026 final-skolem-function-sizes = 30967, 30281, 29683, 28356, 27434, 26138, 25159, 24444, 23439, 22677, 21091, 20498, 19941, 19498, 18603, 18177, 17428, 16646, 15645, 14063, 13384, 12951, 12186, 10297, 9935, 9562, 9354, 8708, 8269, 7790, 6739, 6398, 6170, 5728, 5395, 5068, 4589, 4311, 4112, 3905, 3451, 3228, 3117, 2738, 2432, 2143, 1982, 1851, 1635, 1418, 1217, 1115, 977, 871, 806, 665, 457, 333, 238, 195, 122, 61, 34, 7,