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

aig sizes of factors = 157, 

variables in factors = 24, 

variables to eliminate in factors = 8, 

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	2	19	182	182	2	168	3	0	4	0	1	0	1,	157,	

2	i_2	1	1	42	195	195	1	195	3	0	4	0	1	0	1,	168,	

3	i_3	1	5	55	219	219	5	228	3	0	4	0	1	0	1,	195,	

4	i_4	1	2	80	261	261	1	283	3	1	4	0	1	0	1,	228,	

5	i_5	1	2	131	340	340	2	387	3	0	4	0	1	0	1,	283,	

6	i_6	1	8	115	400	400	4	468	3	1	4	0	1	0	1,	387,	

7	i_7	1	3	77	478	478	2	509	3	1	4	0	1	0	1,	468,	

8	i_8	1	6	81	518	518	6	509	2	0	4	0	1	0	1,	509,	



total_number_of_compose_operations_in_initial_skolem_function_generation = 23
total_ComposeTime_in_initial_skolem_function_generation = 3 milliseconds
total_number_of_boolean_operations_in_initial_skolem_function_generation = 32
total_BooleanOpTime_in_initial_skolem_function_generation = 0 milliseconds
total_number_of_support_operations_in_initial_skolem_function_generation = 8
total_FactorFindingTime_in_initial_skolem_function_generation = 0 milliseconds

total-time-in-initial-skolem-function-generation-without-size-computation-time = 29 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 = 29 milliseconds
total-time-in-reverse-substitution-without-size-computation-time = 0 milliseconds
total-time-without-size-computation-time = 29 milliseconds
total-time-in-interpolant-computation = 23

algorithm-used = monolithic_compositionqe_interpolantskf_cofactorone
ordering-used = least-occurring-first
total time in ordering = 0 milliseconds
total time in compute-size = 0
total time in compute-support = 0
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 = 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 = 0 milliseconds
compose-in-reverse-substitution = 28
time-in-reverse-substitution = 0
final-skolem-function-sizes = 19, 42, 222, 187, 131, 115, 127, 81,