benchmark type = generated benchmark name = ../benchmarks/subtraction/128.v problem = variable_elimination machine = prolient number of factors = 254 number of variables to eliminate = 128 number of variables = 384 aig sizes of factors = 759, 763, 763, 751, 751, 745, 745, 739, 739, 733, 733, 727, 727, 721, 721, 715, 715, 709, 709, 703, 703, 697, 697, 691, 691, 685, 685, 679, 679, 673, 673, 667, 667, 661, 661, 655, 655, 649, 649, 643, 643, 637, 637, 631, 631, 625, 625, 619, 619, 613, 613, 607, 607, 601, 601, 595, 595, 589, 589, 583, 583, 577, 577, 571, 571, 565, 565, 559, 559, 553, 553, 547, 547, 541, 541, 535, 535, 529, 529, 523, 523, 517, 517, 511, 511, 505, 505, 499, 499, 493, 493, 487, 487, 481, 481, 475, 475, 469, 469, 463, 463, 457, 457, 451, 451, 445, 445, 439, 439, 433, 433, 427, 427, 421, 421, 415, 415, 409, 409, 403, 403, 397, 397, 391, 391, 385, 385, 379, 379, 373, 373, 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, 769, 769, variables in factors = 253, 255, 255, 251, 251, 249, 249, 247, 247, 245, 245, 243, 243, 241, 241, 239, 239, 237, 237, 235, 235, 233, 233, 231, 231, 229, 229, 227, 227, 225, 225, 223, 223, 221, 221, 219, 219, 217, 217, 215, 215, 213, 213, 211, 211, 209, 209, 207, 207, 205, 205, 203, 203, 201, 201, 199, 199, 197, 197, 195, 195, 193, 193, 191, 191, 189, 189, 187, 187, 185, 185, 183, 183, 181, 181, 179, 179, 177, 177, 175, 175, 173, 173, 171, 171, 169, 169, 167, 167, 165, 165, 163, 163, 161, 161, 159, 159, 157, 157, 155, 155, 153, 153, 151, 151, 149, 149, 147, 147, 145, 145, 143, 143, 141, 141, 139, 139, 137, 137, 135, 135, 133, 133, 131, 131, 129, 129, 127, 127, 125, 125, 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, 257, 257, variables to eliminate in factors = 126, 127, 127, 125, 125, 124, 124, 123, 123, 122, 122, 121, 121, 120, 120, 119, 119, 118, 118, 117, 117, 116, 116, 115, 115, 114, 114, 113, 113, 112, 112, 111, 111, 110, 110, 109, 109, 108, 108, 107, 107, 106, 106, 105, 105, 104, 104, 103, 103, 102, 102, 101, 101, 100, 100, 99, 99, 98, 98, 97, 97, 96, 96, 95, 95, 94, 94, 93, 93, 92, 92, 91, 91, 90, 90, 89, 89, 88, 88, 87, 87, 86, 86, 85, 85, 84, 84, 83, 83, 82, 82, 81, 81, 80, 80, 79, 79, 78, 78, 77, 77, 76, 76, 75, 75, 74, 74, 73, 73, 72, 72, 71, 71, 70, 70, 69, 69, 68, 68, 67, 67, 66, 66, 65, 65, 64, 64, 63, 63, 62, 62, 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, 128, 128, 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_128 2 92 2891 780 780 43 3150 6 1 274 0 254 48 253,254, 769,769, 2 i_127 3 170 3192 3691 3691 114 5815 9 1 45 0 254 50 2,3,254, 763,763,3150, 3 i_126 2 352 4015 7709 7709 297 9307 6 2 21 0 254 48 1,254, 759,5815, 4 i_125 3 367 2451 13042 13042 309 11209 9 3 45 0 254 47 4,5,254, 751,751,9307, 5 i_124 3 466 3079 15803 15803 411 13750 9 5 45 0 254 46 6,7,254, 745,745,11209, 6 i_123 3 531 2663 19720 19720 470 15882 9 11 45 0 254 43 8,9,254, 739,739,13750, 7 i_122 3 617 3181 22813 22813 556 18519 9 11 45 0 254 47 10,11,254, 733,733,15882, 8 i_121 3 1093 4432 26683 26683 1056 22430 9 9 45 0 254 24 12,13,254, 727,727,18519, 9 i_120 3 838 2921 32877 32877 765 24845 9 20 45 0 254 45 14,15,254, 721,721,22430, 10 i_119 3 945 6532 36849 36849 858 30822 9 28 45 0 254 50 16,17,254, 715,715,24845, 11 i_118 3 1516 1677 47074 47074 1351 31987 9 114 45 0 254 48 18,19,254, 709,709,30822, 12 i_117 3 1077 6299 48869 48869 987 37738 9 27 45 1 254 47 20,21,254, 703,703,31987, 13 i_116 3 1944 2489 59680 59680 1831 39722 9 46 45 0 254 59 22,23,254, 697,697,37738, 14 i_115 3 1854 4621 62908 62908 1755 43826 9 48 45 1 254 45 24,25,254, 691,691,39722, 15 i_114 3 1932 3122 70331 70331 1831 46443 9 42 45 0 254 22 26,27,254, 685,685,43826, 16 i_113 3 2063 2151 74986 74986 1921 48077 9 71 45 0 254 53 28,29,254, 679,679,46443, 17 i_112 3 2377 4413 77587 77587 2231 51941 9 82 45 0 254 38 30,31,254, 673,673,48077, 18 i_111 3 3410 4101 84683 84683 3248 55534 9 108 45 0 254 42 32,33,254, 667,667,51941, 19 i_110 3 4180 4993 91432 91432 4011 59978 9 98 45 0 254 39 34,35,254, 661,661,55534, 20 i_109 3 3765 1863 98871 98871 3585 61360 9 103 45 0 254 44 36,37,254, 655,655,59978, 21 i_108 3 3142 1969 101071 101071 2958 62858 9 103 45 0 254 60 38,39,254, 649,649,61360, 22 i_107 3 4292 2978 103808 103808 4110 65343 9 118 45 0 254 46 40,41,254, 643,643,62858, 23 i_106 3 4031 2169 107654 107654 3834 67020 9 140 45 0 254 38 42,43,254, 637,637,65343, 24 i_105 3 3557 2568 110173 110173 3315 69066 9 140 45 0 254 62 44,45,254, 631,631,67020, 25 i_104 3 5523 1476 113816 113816 5335 70097 9 124 45 0 254 41 46,47,254, 625,625,69066, 26 i_103 3 4756 2086 115526 115526 4565 71699 9 133 45 0 254 32 48,49,254, 619,619,70097, 27 i_102 3 4783 1454 117974 117974 4547 72653 9 171 45 0 254 39 50,51,254, 613,613,71699, 28 i_101 3 4453 1989 119307 119307 4235 74166 9 149 45 0 254 41 52,53,254, 607,607,72653, 29 i_100 3 5188 4794 121919 121919 4979 78500 9 138 45 0 254 35 54,55,254, 601,601,74166, 30 i_99 3 4874 2008 130376 130376 4646 80044 9 163 45 0 254 38 56,57,254, 595,595,78500, 31 i_98 3 6157 3145 133296 133296 5895 82720 9 194 45 0 254 37 58,59,254, 589,589,80044, 32 i_97 3 5398 1849 137462 137462 5143 84115 9 184 45 0 254 32 60,61,254, 583,583,82720, 33 i_96 3 5990 2025 139680 139680 5718 85697 9 195 45 0 254 40 62,63,254, 577,577,84115, 34 i_95 3 5360 2024 142522 142522 5106 87262 9 185 45 7 254 33 64,65,254, 571,571,85697, 35 i_94 3 6941 6427 145065 145065 6667 93216 9 208 45 1 254 36 66,67,254, 565,565,87262, 36 i_93 3 6710 1843 155500 155500 6401 94608 9 236 45 0 254 36 68,69,254, 559,559,93216, 37 i_92 3 8070 3098 158189 158189 6750 97261 9 1270 45 0 254 28 70,71,254, 553,553,94608, 38 i_91 3 8025 3054 162833 162833 7780 99850 9 163 45 0 254 35 72,73,254, 547,547,97261, 39 i_90 3 8695 2065 167642 167642 8441 101469 9 172 45 0 254 33 74,75,254, 541,541,99850, 40 i_89 3 9104 4100 170961 170961 8870 105149 9 158 45 0 254 27 76,77,254, 535,535,101469, 41 i_88 3 7516 2517 178282 178282 7259 107237 9 174 45 0 254 36 78,79,254, 529,529,105149, 42 i_87 3 7572 1337 182497 182497 7313 108157 9 181 45 0 254 33 80,81,254, 523,523,107237, 43 i_86 3 7931 1794 184052 184052 7670 109523 9 179 45 0 254 24 82,83,254, 517,517,108157, 44 i_85 3 9807 2278 186571 186571 9526 111380 9 195 45 0 254 27 84,85,254, 511,511,109523, 45 i_84 3 8215 1364 190117 190117 7859 112343 9 256 45 0 254 52 86,87,254, 505,505,111380, 46 i_83 3 9216 1805 192298 192298 8930 113737 9 203 45 0 254 32 88,89,254, 499,499,112343, 47 i_82 3 9331 1352 195014 195014 9022 114713 9 225 45 0 254 23 90,91,254, 493,493,113737, 48 i_81 3 10512 1398 196918 196918 10219 115724 9 219 45 0 254 32 92,93,254, 487,487,114713, 49 i_80 3 14181 2678 198896 198896 13885 117996 9 219 45 0 254 29 94,95,254, 481,481,115724, 50 i_79 3 10551 1740 203012 203012 10239 119319 9 225 45 0 254 31 96,97,254, 475,475,117996, 51 i_78 3 9621 954 205466 205466 9308 119884 9 230 45 0 254 30 98,99,254, 469,469,119319, 52 i_77 3 11971 1380 206600 206600 11647 120840 9 241 45 0 254 31 100,101,254, 463,463,119884, 53 i_76 3 11355 1586 208785 208785 10554 122027 9 332 45 0 254 29 102,103,254, 457,457,120840, 54 i_75 3 12252 2195 211839 211839 11762 123835 9 137 45 0 254 198 104,105,254, 451,451,122027, 55 i_74 3 53841 1883 214489 214489 52504 125379 9 1146 45 0 254 51 106,107,254, 445,445,123835, 56 i_73 3 73007 2332 217725 217725 40189 127353 9 32519 45 0 254 53 108,109,254, 439,439,125379, 57 i_72 3 71232 1375 221970 221970 50011 128373 9 21010 45 0 254 68 110,111,254, 433,433,127353, 58 i_71 3 175685 1187 223740 223740 34055 129226 9 141311 45 0 254 153 112,113,254, 427,427,128373, 59 i_70 3 79227 919 225841 225841 40386 129817 9 38550 45 0 254 56 114,115,254, 421,421,129226, 60 i_69 3 387637 991 226989 226989 124618 130481 9 262792 45 0 254 102 116,117,254, 415,415,129817, 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 = 1218623 milliseconds total-time-in-interpolant-computation = 685839 algorithm-used = monolithic_compositionqe_interpolantskf_cofactorone ordering-used = least-occurring-first total time in ordering = 5 milliseconds total time in compute-size = 1975 total time in compute-support = 2277 total time in initialization of skolem function generator-without-size-computation-time = 150 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 = 1 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 = 1975 milliseconds compose-in-reverse-substitution = 6 time-in-reverse-substitution = 21707 final-skolem-function-sizes =