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

aig sizes of factors = 44, 44, 3, 3, 87, 

variables in factors = 16, 16, 2, 2, 24, 

variables to eliminate in factors = 8, 8, 1, 1, 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	3	2	72	139	139	2	138	9	0	49	0	5	0	1,2,5,	44,44,87,	

2	i_2	1	4	115	178	178	4	219	3	0	4	0	5	0	5,	138,	

3	i_3	1	1	67	343	343	1	262	3	0	4	0	5	0	5,	219,	

4	i_4	1	2	52	421	421	2	294	3	0	4	0	5	0	5,	262,	

5	i_5	1	7	41	474	474	2	319	3	0	4	0	5	1	5,	294,	

6	i_6	1	2	23	520	520	1	331	3	0	4	0	5	0	5,	319,	

7	i_7	1	8	10	541	541	7	333	3	0	4	0	5	0	5,	331,	

8	i_8	3	3	3	565	569	3	333	6	0	41	0	5	0	3,4,5,	3,3,333,	



total_number_of_compose_operations_in_initial_skolem_function_generation = 33
total_ComposeTime_in_initial_skolem_function_generation = 0 milliseconds
total_number_of_boolean_operations_in_initial_skolem_function_generation = 114
total_BooleanOpTime_in_initial_skolem_function_generation = 0 milliseconds
total_number_of_support_operations_in_initial_skolem_function_generation = 40
total_FactorFindingTime_in_initial_skolem_function_generation = 1 milliseconds

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

total-time-in-initial-skolem-function-generation-without-size-computation-time = 74 milliseconds
total-time-in-reverse-substitution-without-size-computation-time = 1 milliseconds
total-time-without-size-computation-time = 107 milliseconds
total-time-in-interpolant-computation = 22

algorithm-used = monolithic_compositionqe_interpolantskf_cofactorone
ordering-used = least-occurring-first
total time in ordering = 0 milliseconds
total time in compute-size = 1
total time in compute-support = 1
total time in initialization of skolem function generator-without-size-computation-time = 45
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 = 1 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 = 1 milliseconds
compose-in-reverse-substitution = 28
time-in-reverse-substitution = 1
final-skolem-function-sizes = 270, 230, 141, 93, 57, 26, 10, 3,