benchmark type = generated
benchmark name = ../benchmarks/intermediate/16.v
problem = variable_elimination
machine = prolient
number of factors = 1
number of variables to eliminate = 16
number of variables = 48

aig sizes of factors = 247, 

variables in factors = 48, 

variables to eliminate in factors = 16, 

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	14	613	300	300	14	769	3	0	4	0	1	0	1,	247,	

2	i_10	1	25	1575	1035	1035	24	2241	3	0	4	0	1	1	1,	769,	

3	i_11	1	47	2354	2774	2774	46	4455	3	1	4	0	1	0	1,	2241,	

4	i_12	1	54	2161	5425	5425	51	6472	3	2	4	0	1	0	1,	4455,	

5	i_13	1	54	1219	8046	8046	51	7561	3	3	4	0	1	0	1,	6472,	

6	i_14	1	64	1161	9151	9151	57	8602	3	7	4	0	1	0	1,	7561,	

7	i_15	1	52	380	10404	10404	46	8869	3	3	4	0	1	1	1,	8602,	

8	i_16	1	59	708	10224	10224	54	9464	3	5	4	0	1	0	1,	8869,	

9	i_2	1	10254	91612	18490	18490	10208	100978	3	33	4	0	1	0	1,	9464,	

10	i_3	1	311537	293835	172875	172875	311286	393448	3	179	4	0	1	10	1,	100978,	


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 = 1893215 milliseconds
total-time-in-interpolant-computation = 1892509

algorithm-used = monolithic_compositionqe_interpolantskf_cofactorone
ordering-used = least-occurring-first
total time in ordering = 0 milliseconds
total time in compute-size = 201
total time in compute-support = 7
total time in initialization of skolem function generator-without-size-computation-time = 1
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 = 201 milliseconds
compose-in-reverse-substitution = 2
time-in-reverse-substitution = 446
final-skolem-function-sizes =