benchmark type = generated benchmark name = ../benchmarks/max/128.v problem = variable_elimination machine = prolient number of factors = 5 number of variables to eliminate = 128 number of variables = 384 aig sizes of factors = 763, 763, 3, 3, 1407, variables in factors = 256, 256, 2, 2, 384, variables to eliminate in factors = 128, 128, 1, 1, 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_1 3 98 949 1948 1948 96 1972 9 0 49 0 5 2 1,2,5, 763,763,1407, 2 i_10 1 81 847 2375 2375 81 2218 3 0 4 0 5 0 5, 1972, 3 i_100 1 18 380 2803 2803 17 2454 3 0 4 0 5 0 5, 2218, 4 i_101 1 29 365 3277 3277 23 2680 3 1 4 0 5 5 5, 2454, 5 i_102 1 30 353 3729 3729 27 2898 3 2 4 0 5 1 5, 2680, 6 i_103 1 28 336 4178 4178 27 3105 3 0 4 0 5 1 5, 2898, 7 i_104 1 43 335 4623 4623 36 3316 3 2 4 0 5 1 5, 3105, 8 i_105 1 49 326 5173 5173 46 3523 3 2 4 0 5 1 5, 3316, 9 i_106 1 54 299 5588 5588 51 3708 3 2 4 0 5 0 5, 3523, 10 i_107 1 65 285 5969 5969 59 3884 3 6 4 0 5 0 5, 3708, 11 i_108 1 70 270 6320 6320 60 4050 3 5 4 0 5 1 5, 3884, 12 i_109 1 81 259 6670 6670 78 4210 3 1 4 0 5 1 5, 4050, 13 i_11 1 141 1155 4658 4658 138 4796 3 1 4 0 5 0 5, 4210, 14 i_110 1 96 256 8067 8067 93 4957 3 3 4 0 5 0 5, 4796, 15 i_111 1 121 232 8407 8407 117 5100 3 2 4 0 5 1 5, 4957, 16 i_112 1 119 221 8718 8718 111 5237 3 6 4 0 5 1 5, 5100, 17 i_113 1 118 212 9007 9007 113 5370 3 3 4 0 5 1 5, 5237, 18 i_114 1 129 195 9274 9274 122 5491 3 4 4 0 5 1 5, 5370, 19 i_115 1 136 179 9534 9534 131 5601 3 3 4 0 5 1 5, 5491, 20 i_116 1 144 164 9758 9758 139 5701 3 4 4 0 5 0 5, 5601, 21 i_117 1 148 155 9972 9972 143 5797 3 5 4 0 5 0 5, 5701, 22 i_118 1 157 137 10158 10158 150 5880 3 4 4 0 5 1 5, 5797, 23 i_119 1 165 130 10349 10349 159 5961 3 5 4 0 5 0 5, 5880, 24 i_12 1 228 1263 6769 6769 221 6658 3 4 4 0 5 1 5, 5961, 25 i_120 1 210 111 11719 11719 128 6725 3 80 4 0 5 0 5, 6658, 26 i_121 1 218 103 11863 11863 212 6789 3 4 4 0 5 1 5, 6725, 27 i_122 1 203 85 11990 11990 198 6840 3 4 4 0 5 0 5, 6789, 28 i_123 1 209 69 12114 12114 203 6880 3 5 4 0 5 1 5, 6840, 29 i_124 1 243 56 12194 12194 237 6912 3 5 4 0 5 1 5, 6880, 30 i_125 1 234 43 12271 12271 226 6936 3 6 4 0 5 1 5, 6912, 31 i_126 1 243 24 12318 12318 236 6947 3 5 4 0 5 0 5, 6936, 32 i_127 1 349 13 12356 12356 343 6952 3 5 4 0 5 1 5, 6947, 33 i_13 1 364 1625 8264 8264 360 8012 3 3 4 0 5 1 5, 6952, 34 i_14 1 420 1385 9785 9785 413 8842 3 5 4 0 5 0 5, 8012, 35 i_15 1 387 1599 10939 10939 379 9877 3 5 4 0 5 1 5, 8842, 36 i_16 1 386 1667 12928 12928 379 10993 3 5 4 0 5 0 5, 9877, 37 i_17 1 368 2187 14898 14898 360 12627 3 6 4 0 5 1 5, 10993, 38 i_18 1 444 2041 17639 17639 432 14047 3 7 4 0 5 1 5, 12627, 39 i_19 1 454 1640 20012 20012 436 15126 3 9 4 0 5 1 5, 14047, 40 i_2 1 551 1386 15473 15473 536 15919 3 7 4 0 5 1 5, 15126, 41 i_20 1 576 2197 22849 22849 555 17474 3 18 4 0 5 1 5, 15919, 42 i_21 1 743 1551 25165 25165 688 18485 3 47 4 0 5 1 5, 17474, 43 i_22 1 892 1462 26916 26916 851 19419 3 27 4 0 5 1 5, 18485, 44 i_23 1 741 1711 28550 28550 700 20528 3 33 4 1 5 1 5, 19419, 45 i_24 1 772 2311 30121 30121 730 22175 3 34 4 0 5 1 5, 20528, 46 i_25 1 733 1477 32840 32840 688 23031 3 34 4 0 5 6 5, 22175, 47 i_26 1 1130 1836 34211 34211 1072 24115 3 44 4 0 5 7 5, 23031, 48 i_27 1 1006 1232 35716 35716 952 24736 3 40 4 0 5 6 5, 24115, 49 i_28 1 970 1476 36785 36785 906 25614 3 37 4 0 5 6 5, 24736, 50 i_29 1 838 1455 38187 38187 776 26537 3 43 4 0 5 5 5, 25614, 51 i_3 1 978 2097 27044 27044 936 28005 3 36 4 2 5 2 5, 26537, 52 i_30 1 879 1443 41563 41563 796 28961 3 52 4 0 5 7 5, 28005, 53 i_31 1 1200 1725 43331 43331 945 30074 3 240 4 0 5 2 5, 28961, 54 i_32 1 1093 1566 45338 45338 1023 31100 3 41 4 0 5 2 5, 30074, 55 i_33 1 1159 1318 47035 47035 1100 31822 3 45 4 0 5 3 5, 31100, 56 i_34 1 1352 2224 47983 47983 1283 33452 3 33 4 0 5 8 5, 31822, 57 i_35 1 1183 1451 50355 50355 1099 34396 3 49 4 0 5 2 5, 33452, 58 i_36 1 1155 1751 51999 51999 1084 35617 3 50 4 0 5 1 5, 34396, 59 i_37 1 1452 1686 54182 54182 1374 36711 3 51 4 0 5 3 5, 35617, 60 i_38 1 1296 1740 55862 55862 1220 37941 3 61 4 0 5 2 5, 36711, 61 i_39 1 1450 1392 57765 57765 1361 38873 3 68 4 0 5 3 5, 37941, 62 i_4 1 2181 1925 39623 39623 2109 40077 3 57 4 0 5 2 5, 38873, 63 i_40 1 1917 1521 60946 60946 1826 41003 3 58 4 0 5 11 5, 40077, 64 i_41 1 1576 1344 62351 62351 1486 41880 3 65 4 0 5 3 5, 41003, 65 i_42 1 1870 1525 63798 63798 1781 42936 3 67 4 0 5 3 5, 41880, 66 i_43 1 1994 1540 65558 65558 1882 43962 3 80 4 1 5 2 5, 42936, 67 i_44 1 1876 1822 67302 67302 1770 45262 3 83 4 0 5 2 5, 43962, 68 i_45 1 1953 1790 69338 69338 1846 46530 3 85 4 0 5 2 5, 45262, 69 i_46 1 1945 1416 71184 71184 1836 47505 3 85 4 0 5 3 5, 46530, 70 i_47 1 2099 1511 72728 72728 1980 48516 3 88 4 0 5 2 5, 47505, 71 i_48 1 2185 1510 74556 74556 2064 49612 3 98 4 0 5 5 5, 48516, 72 i_49 1 2218 1504 76461 76461 2092 50621 3 101 4 0 5 2 5, 49612, 73 i_5 1 2830 3866 51810 51810 2722 53864 3 95 4 0 5 3 5, 50621, 74 i_50 1 2246 1189 83551 83551 2063 54653 3 152 4 0 5 2 5, 53864, 75 i_51 1 2562 1373 85027 85027 2413 55578 3 127 4 0 5 5 5, 54653, 76 i_52 1 2639 1334 86668 86668 2481 56443 3 119 4 0 5 10 5, 55578, 77 i_53 1 2915 1166 88178 88178 2769 57187 3 121 4 0 5 12 5, 56443, 78 i_54 1 2704 1817 89365 89365 2545 58596 3 130 4 0 5 13 5, 57187, 79 i_55 1 2967 1118 91624 91624 2808 59339 3 130 4 0 5 9 5, 58596, 80 i_56 1 3188 1325 92927 92927 3021 60259 3 144 4 0 5 6 5, 59339, 81 i_57 1 3195 1125 94573 94573 3001 61034 3 167 4 0 5 3 5, 60259, 82 i_58 1 3229 1570 95953 95953 3041 62199 3 169 4 0 5 8 5, 61034, 83 i_59 1 4178 1165 97758 97758 3968 62992 3 181 4 0 5 7 5, 62199, 84 i_6 1 6555 2898 65132 65132 6258 65221 3 261 4 0 5 13 5, 62992, 85 i_60 1 4880 1125 102057 102057 3547 66004 3 1303 4 0 5 9 5, 65221, 86 i_61 1 4156 1802 103446 103446 3971 67438 3 141 4 0 5 4 5, 66004, 87 i_62 1 4815 1059 105824 105824 4563 68156 3 200 4 0 5 6 5, 67438, 88 i_63 1 4855 839 107306 107306 4635 68569 3 178 4 0 5 9 5, 68156, 89 i_64 1 4919 1103 108192 108192 4730 69331 3 138 4 0 5 13 5, 68569, 90 i_65 1 4482 1215 109563 109563 4287 70229 3 161 4 0 5 10 5, 69331, 91 i_66 1 5338 1014 111105 111105 5150 70950 3 156 4 0 5 7 5, 70229, 92 i_67 1 5247 1163 112432 112432 5039 71811 3 155 4 0 5 13 5, 70950, 93 i_68 1 4734 991 113983 113983 4475 72503 3 192 4 0 5 25 5, 71811, 94 i_69 1 5151 1067 115313 115313 4992 73256 3 129 4 0 5 4 5, 72503, 95 i_7 1 5684 3762 76166 76166 5527 76294 3 120 4 0 5 8 5, 73256, 96 i_70 1 5022 1273 121235 121235 4838 77292 3 158 4 0 5 4 5, 76294, 97 i_71 1 4927 981 122816 122816 4730 78005 3 168 4 0 5 5 5, 77292, 98 i_72 1 5073 948 124469 124469 4867 78678 3 169 4 0 5 10 5, 78005, 99 i_73 1 5299 902 125772 125772 5104 79335 3 158 4 0 5 5 5, 78678, 100 i_74 1 5143 949 127027 127027 4948 80047 3 161 4 0 5 10 5, 79335, 101 i_75 1 5849 982 128432 128432 5626 80796 3 185 4 0 5 4 5, 80047, 102 i_76 1 5740 872 129911 129911 5530 81442 3 179 4 0 5 8 5, 80796, 103 i_77 1 5945 897 131099 131099 5733 82140 3 175 4 1 5 5 5, 81442, 104 i_78 1 5695 840 132462 132462 5475 82787 3 184 4 0 5 5 5, 82140, 105 i_79 1 6066 853 133721 133721 5864 83450 3 171 4 0 5 8 5, 82787, 106 i_8 1 7384 2963 87299 87299 7157 85814 3 186 4 0 5 18 5, 83450, 107 i_80 1 6394 876 138637 138637 6154 86491 3 206 4 0 5 4 5, 85814, 108 i_81 1 6330 891 139897 139897 6106 87174 3 191 4 0 5 5 5, 86491, 109 i_82 1 6743 809 141181 141181 6473 87805 3 237 4 0 5 11 5, 87174, 110 i_83 1 6617 836 142413 142413 6395 88460 3 194 4 0 5 5 5, 87805, 111 i_84 1 6921 748 143669 143669 6662 89059 3 223 4 0 5 10 5, 88460, 112 i_85 1 7279 756 144863 144863 6996 89657 3 257 4 0 5 5 5, 89059, 113 i_86 1 7212 748 145977 145977 6939 90263 3 236 4 0 5 9 5, 89657, 114 i_87 1 8118 750 147170 147170 7130 90878 3 934 4 0 5 20 5, 90263, 115 i_88 1 8230 696 148384 148384 7524 91444 3 652 4 0 5 12 5, 90878, 116 i_89 1 9919 745 149487 149487 8167 92060 3 1703 4 0 5 6 5, 91444, 117 i_9 1 19371 5314 96783 96783 19037 96724 3 285 4 0 5 18 5, 92060, 118 i_90 1 16008 727 157351 157351 15641 97335 3 302 4 0 5 20 5, 96724, 119 i_91 1 16584 687 158548 158548 16131 97912 3 386 4 0 5 10 5, 97335, 120 i_92 1 17386 644 159683 159683 16350 98451 3 964 4 0 5 9 5, 97912, 121 i_93 1 144251 635 160754 160754 53722 98985 3 90177 4 0 5 15 5, 98451, 122 i_94 1 311249 618 161804 161804 78367 99508 3 232546 4 0 5 68 5, 98985, 123 i_95 1 115084 593 162935 162935 51505 100011 3 63134 4 0 5 60 5, 99508, 124 i_96 1 66305 618 163942 163942 32673 100546 3 33320 4 0 5 119 5, 100011, 125 i_97 1 159755 625 165019 165019 40006 101093 3 119372 4 0 5 167 5, 100546, 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 = 1216324 milliseconds total-time-in-interpolant-computation = 640064 algorithm-used = monolithic_compositionqe_interpolantskf_cofactorone ordering-used = least-occurring-first total time in ordering = 1 milliseconds total time in compute-size = 2294 total time in compute-support = 495 total time in initialization of skolem function generator-without-size-computation-time = 3 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 = 2294 milliseconds compose-in-reverse-substitution = 2 time-in-reverse-substitution = 18676 final-skolem-function-sizes =