benchmark type = generated
benchmark name = ../benchmarks/max/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	18	64	139	139	7	124	9	0	49	0	5	0	1,2,5,	44,44,87,	

2	i_2	1	1	81	156	156	1	172	3	0	4	0	5	0	5,	124,	

3	i_3	1	5	73	267	267	5	216	3	0	4	0	5	0	5,	172,	

4	i_4	1	2	56	365	365	2	248	3	0	4	0	5	0	5,	216,	

5	i_5	1	1	40	430	430	1	270	3	0	4	0	5	0	5,	248,	

6	i_6	1	3	24	476	476	3	281	3	0	4	0	5	0	5,	270,	

7	i_7	1	8	13	502	502	5	286	3	1	4	0	5	0	5,	281,	

8	i_8	3	6	4	522	518	6	286	6	0	41	0	5	0	3,4,5,	3,3,286,	



total_number_of_compose_operations_in_initial_skolem_function_generation = 33
total_ComposeTime_in_initial_skolem_function_generation = 1 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 = 0 milliseconds

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

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 = 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 = 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 = 0
final-skolem-function-sizes = 229, 198, 145, 95, 57, 30, 14, 4,