benchmark type = generated
benchmark name = ../benchmarks/avgceiling/32.v
problem = variable_elimination
machine = prolient
number of factors = 1
number of variables to eliminate = 32
number of variables = 96

aig sizes of factors = 661, 

variables in factors = 96, 

variables to eliminate in factors = 32, 

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	1	3	16	756	756	3	669	3	0	4	0	1	0	1,	661,	

2	i_10	1	5	42	743	743	4	701	3	0	4	0	1	1	1,	669,	

3	i_11	1	8	54	773	773	8	741	3	0	4	0	1	0	1,	701,	

4	i_12	1	2	70	810	810	2	792	3	0	4	0	1	0	1,	741,	

5	i_13	1	13	90	858	858	11	859	3	1	4	0	1	0	1,	792,	

6	i_14	1	5	103	922	922	5	930	3	0	4	0	1	0	1,	859,	

7	i_15	1	12	145	991	991	4	1043	3	0	4	0	1	0	1,	930,	

8	i_16	1	10	156	1101	1101	10	1159	3	0	4	0	1	0	1,	1043,	

9	i_17	1	15	256	1214	1214	14	1371	3	1	4	0	1	0	1,	1159,	

10	i_18	1	17	238	1423	1423	16	1557	3	0	4	0	1	0	1,	1371,	

11	i_19	1	23	257	1607	1607	22	1754	3	0	4	0	1	0	1,	1557,	

12	i_2	1	12	35	1851	1851	8	1774	3	1	4	0	1	0	1,	1754,	

13	i_20	1	28	531	1821	1821	27	2246	3	1	4	0	1	0	1,	1774,	

14	i_21	1	32	372	2290	2290	27	2547	3	0	4	0	1	0	1,	2246,	

15	i_22	1	31	320	2588	2588	24	2795	3	1	4	0	1	0	1,	2547,	

16	i_23	1	36	333	2867	2867	34	3040	3	2	4	0	1	0	1,	2795,	

17	i_24	1	40	537	3075	3075	38	3471	3	2	4	0	1	0	1,	3040,	

18	i_25	1	62	579	3503	3503	60	3956	3	1	4	0	1	0	1,	3471,	

19	i_26	1	55	447	3985	3985	53	4285	3	1	4	0	1	0	1,	3956,	

20	i_27	1	88	568	4310	4310	87	4757	3	1	4	0	1	0	1,	4285,	

21	i_28	1	77	664	4778	4778	74	5296	3	1	4	0	1	1	1,	4757,	

22	i_29	1	86	786	5313	5313	80	5933	3	2	4	0	1	0	1,	5296,	

23	i_3	1	24	51	6027	6027	22	5967	3	2	4	0	1	0	1,	5933,	

24	i_30	1	46	268	5980	5980	43	6125	3	1	4	0	1	1	1,	5967,	

25	i_31	1	59	344	6170	6170	52	6358	3	1	4	0	1	1	1,	6125,	

26	i_32	1	67	270	6418	6418	64	6511	3	2	4	0	1	1	1,	6358,	

27	i_4	1	34	112	6602	6602	31	6597	3	2	4	0	1	1	1,	6511,	

28	i_5	1	24	81	6685	6685	21	6642	3	2	4	0	1	0	1,	6597,	

29	i_6	1	37	87	6727	6727	26	6699	3	1	4	0	1	0	1,	6642,	

30	i_7	1	29	155	6782	6782	26	6817	3	2	4	0	1	0	1,	6699,	

31	i_8	1	40	161	6897	6897	35	6937	3	2	4	0	1	1	1,	6817,	

32	i_9	1	53	193	11614	11614	47	6937	2	2	4	0	1	0	1,	6937,	



total_number_of_compose_operations_in_initial_skolem_function_generation = 95
total_ComposeTime_in_initial_skolem_function_generation = 32 milliseconds
total_number_of_boolean_operations_in_initial_skolem_function_generation = 128
total_BooleanOpTime_in_initial_skolem_function_generation = 0 milliseconds
total_number_of_support_operations_in_initial_skolem_function_generation = 32
total_FactorFindingTime_in_initial_skolem_function_generation = 7 milliseconds

total-time-in-initial-skolem-function-generation-without-size-computation-time = 1055 milliseconds
total time in initialization of skolem function generator-without-size-computation-time = 0

total-time-in-initial-skolem-function-generation-without-size-computation-time = 1055 milliseconds
total-time-in-reverse-substitution-without-size-computation-time = 29 milliseconds
total-time-without-size-computation-time = 1084 milliseconds
total-time-in-interpolant-computation = 978

algorithm-used = monolithic_compositionqe_interpolantskf_cofactorone
ordering-used = least-occurring-first
total time in ordering = 0 milliseconds
total time in compute-size = 20
total time in compute-support = 5
total time in initialization of skolem function generator-without-size-computation-time = 0
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 = 19 milliseconds
size_computation_time_in_reverse_substitution_in_cegar = 1 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 = 20 milliseconds
compose-in-reverse-substitution = 496
time-in-reverse-substitution = 18
final-skolem-function-sizes = 16, 230, 242, 258, 278, 291, 333, 344, 444, 426, 445, 35, 719, 560, 776, 521, 725, 767, 635, 752, 852, 974, 51, 879, 708, 458, 112, 81, 87, 155, 161, 193,