Benchmark Properties				Interpolation Properties				iPrincess Results		QE Results
Name	Status	Difficulty	Category	L/R Ratio (%)	#C	#LC	Dec. Time (ms)	IS	Time (ms)	IS	Time (ms)
mathsat/FISCHER1-2-fair.pri	unsat	0	industrial	60	42	2	912	20	17	793	384
mathsat/FISCHER1-2-fair.pri	unsat	0	industrial	70	42	5	912	18	18	2205	775
mathsat/FISCHER1-2-fair.pri	unsat	0	industrial	80	42	12	912	16	19	68	201
mathsat/FISCHER1-2-fair.pri	unsat	0	industrial	90	42	23	912	15	22	61	344
mathsat/FISCHER1-3-fair.pri	unsat	0	industrial	60	59	2	1452	76	47	1277	387
mathsat/FISCHER1-3-fair.pri	unsat	0	industrial	70	59	8	1452	57	47	9608	2420
mathsat/FISCHER1-3-fair.pri	unsat	0	industrial	80	59	14	1452	48	50	7143	4928
mathsat/FISCHER1-3-fair.pri	unsat	0	industrial	90	59	32	1452	36	33	313	1272
mathsat/FISCHER1-4-fair.pri	unsat	0	industrial	60	76	3	2493	163	77	2309	559
mathsat/FISCHER1-4-fair.pri	unsat	0	industrial	70	76	11	2493	100	76	23039	4361
mathsat/FISCHER1-4-fair.pri	unsat	0	industrial	80	76	17	2493	63	87	196921	113244
mathsat/FISCHER1-4-fair.pri	unsat	0	industrial	90	76	41	2493	59	86	341	446
mathsat/FISCHER1-5-fair.pri	unsat	0	industrial	60	93	3	3472	189	154	2954	608
mathsat/FISCHER1-5-fair.pri	unsat	0	industrial	70	93	13	3472	124	118	35839	7455
mathsat/FISCHER1-5-fair.pri	unsat	0	industrial	80	93	20	3472	111	104	-	T/O
mathsat/FISCHER1-5-fair.pri	unsat	0	industrial	90	93	50	3472	128	111	579	10274
mathsat/FISCHER1-6-fair.pri	unsat	0	industrial	60	110	3	4057	336	115	3609	708
mathsat/FISCHER1-6-fair.pri	unsat	0	industrial	70	110	16	4057	204	105	83925	23948
mathsat/FISCHER1-6-fair.pri	unsat	0	industrial	80	110	26	4057	169	104	-	T/O
mathsat/FISCHER1-6-fair.pri	unsat	0	industrial	90	110	59	4057	126	127	-	T/O
mathsat/FISCHER2-2-fair.pri	unsat	0	industrial	60	78	2	2711	128	97	1876	546
mathsat/FISCHER2-2-fair.pri	unsat	0	industrial	70	78	12	2711	118	110	42344	7103
mathsat/FISCHER2-2-fair.pri	unsat	0	industrial	80	78	21	2711	91	69	1483	582
mathsat/FISCHER2-2-fair.pri	unsat	0	industrial	90	78	44	2711	64	59	378	476
mathsat/FISCHER2-3-fair.pri	unsat	0	industrial	70	110	16	13002	2439	731	279672	68650
mathsat/FISCHER2-3-fair.pri	unsat	0	industrial	80	110	28	13002	2342	731	-	T/O
mathsat/FISCHER2-3-fair.pri	unsat	0	industrial	90	110	61	13002	1799	728	-	T/O
mathsat/FISCHER2-4-fair.pri	unsat	0	industrial	70	142	20	102642	13080	7687	-	T/O
mathsat/FISCHER2-4-fair.pri	unsat	0	industrial	80	142	37	102642	11473	7239	-	T/O
mathsat/FISCHER2-4-fair.pri	unsat	0	industrial	90	142	79	102642	11715	7025	-	T/O
mathsat/FISCHER3-2-fair.pri	unsat	0	industrial	60	112	3	21052	4937	1349	3846	746
mathsat/FISCHER3-2-fair.pri	unsat	0	industrial	70	112	15	21052	4930	1354	-	T/O
mathsat/FISCHER3-2-fair.pri	unsat	0	industrial	80	112	33	21052	4628	1344	3180	1442
mathsat/FISCHER3-2-fair.pri	unsat	0	industrial	90	112	61	21052	3128	1290	2009	1355

Statistics
Number of benchmarks:	34
Number of benchmarks on which iPrincess is faster:	33
Number of benchmarks on which iPrincess is at least 1 order of magnitude faster:	23
Number of benchmarks on which iPrincess yields smaller interpolants:	31
Number of benchmarks on which iPrincess yiels interpolants that are 1 order of magnitude smaller:	25

Legend
L/R Ratio:	Ratio of the number of conjuncts on the left and on the right part of the formula
#C:	Number of constants in the input formula
#LC:	Number of local constants in the input formula (constants occuring in the left part of the formula only)
IS:	Size of the generated interpolant (number of operators)
T/O:	Timeout
O/M:	Out of Memory