Experimental Evaluation of "Automated Detection of Non-Termination and NullPointerExceptions for Java Bytecode"

Recently, we developed an approach for automated termination proofs of Java Bytecode (JBC), which is based on constructing and analyzing termination graphs. These graphs represent all possible program executions in a finite way. In this paper, we show that this approach can also be used to detect non-termination or NullPointerExceptions. Our approach automatically generates witnesses, i.e., calling the JBC method with these witness arguments indeed leads to non-termination resp. to a NullPointerException. Thus, we never obtain "false positives". We implemented our results in the termination prover AProVE and provide experimental evidence for the power of our approach.

Literature

Here, we provide links to our papers on analyzing Java Bytecode. The extended versions of the respective papers include all proofs.

M. Brockschmidt, T. Ströder, C. Otto, and J. Giesl
Automated Detection of Non-Termination and NullPointerExceptions for Java Bytecode
In Proceedings of the 2nd International Conference on Formal Verification of Object-Oriented Software (FoVeOOS '11), Turin, Italy, Lecture Notes in Computer Science. To appear.
Extended version appeared as Technical Report AIB-2011-19, RWTH Aachen, Germany.
M. Brockschmidt, C. Otto, and J. Giesl
Modular Termination Proofs of Recursive Java Bytecode Programs by Term Rewriting
In Proceedings of the 22th International Conference on Rewriting Techniques and Applications (RTA '11), Novi Sad, Serbia, LIPIcs Leibniz International Proceedings in Informatics 10, pages 155-170, 2011.
Extended version appeared as Technical Report AIB-2011-02, RWTH Aachen, Germany.
M. Brockschmidt, C. Otto, C. von Essen, and J. Giesl
Termination Graphs for Java Bytecode
In Verification, Induction, Termination Analysis, LNAI 6463, pages 17-37, 2010.
Extended version appeared as Technical Report AIB-2010-15, RWTH Aachen, Germany.
C. Otto, M. Brockschmidt, C. von Essen, and J. Giesl
Automated Termination Analysis of Java Bytecode by Term Rewriting
In Proceedings of the 21th International Conference on Rewriting Techniques and Applications (RTA '10), Edinburgh, UK, LIPIcs Leibniz International Proceedings in Informatics 6, pages 259-276, 2010.
Extended version appeared as Technical Report AIB-2010-08, RWTH Aachen, Germany.

Implementation in AProVE

A new version of the termination tool AProVE implementing our approach is available here. In particular, this new version of AProVE allows to repeat the experiments below. It can be accessed via a web interface.

The web interface takes an arbitrary jar-file as input. As in the International Termination Competition, it then tries to prove (non-)termination of the main method of the class that is indicated in the file META-INF/MANIFEST.MF. For details, please see the definition of JBC termination problems. In order to prove (non-)termination of a specific method, one therefore has to add an appropriate main method calling the specific method with random inputs.

Tools

We compare our implementation with the previous version of AProVE and two other tools for (non-)termination analysis of Java. Thus, in our experiments we use the following four tools:

AProVE 2011-No
This is a new version of AProVE which is available through our web interface. For AProVE, we ran the experiments using an Intel Core i7 950 CPU with four CPU cores and 3.06 GHz each.
AProVE 2011
This is the old version of AProVE which implements only the techniques from earlier papers. The main difference to AProVE 2011-No is that it is not able to prove non-termination. For more details on AProVE 2011 and to run this previous version of AProVE via a web interface, we refer to the evaluation web site of our RTA 2011 paper.
Julia
Julia is a nullness and (non-)termination analyzer for Java Bytecode based on path-length abstraction, developed at the University of Verona, Italy and the University of Réunion, France. The Julia team kindly provided us with access to a web interface running the current version of Julia. We performed the experiments on July 26, 2011. The Julia web interface was powered by an Intel Xeon CPU with four CPU cores and 2.66GHz each.
Invel
Invel is a tool for detecting non-termination of Java programs. It is based on the KeY system which is developed at the Karlsruhe Institute of Technology, Germany and the Chalmers University of Technology of Gothenburg, Sweden.
As we were not able to obtain a running version of Invel, we have used the results reported in the detailed description of the tool. However, this description does not provide runtimes.

Examples

In our experiments, we tested the tools on a collection of 325 examples. These examples have been taken from three sources:

the 2 examples from our paper.
the 268 Java Bytecode examples from the Termination Problem Data Base (TPDB), which is used in the International Termination Competition. However, we removed one controversial example ("Overflow") from the TPDB whose termination depends on the treatment of integer overflows.
the 55 examples from the evaluation of Invel.

In the experiments, we used a timeout of 60 seconds for each example.

The tables below summarize our experiments. They show that for the problems in the current example collection, AProVE currently yields the most precise results both for termination and non-termination analysis. (However, there are also several examples where Julia could prove termination whereas AProVE fails.)

In the following table, Yes gives the number of examples where termination was proven, No gives the number of examples where non-termination was proven, Maybe means that the proof failed in less than 60 seconds, Timeout gives the number of examples where the tool took longer than 60 seconds, and Runtime is the average time in seconds needed per example.

TPDB and our examples (270)

Tool	Yes	No	Maybe	Timeout	Runtime
AProVE 2011-No	204	30	12	24	11.2
AProVE 2011	204	0	27	39	14.5
Julia	166	22	82	0	3.9

Invel examples (55)

Tool	Yes	No	Maybe	Timeout	Runtime
AProVE 2011-No	1	51	0	3	5.1
AProVE 2011	1	0	5	49	54.0
Julia	1	0	54	0	2.2
Invel	0	42	13	0	?

In the following tables, each row shows the behavior of the tools on one example. The entry "YES" means that termination of that example could be proved by the corresponding tool, "NO" means that non-termination could be proved, while "MAYBE" states that the tool gave up without success. Finally, "TIMEOUT" indicates that the tool exceeded the given time limit and was therefore stopped. By clicking on the respective runtime, one can inspect the output produced by the tool, but note that for Invel, we have no proofs. To load an example into the web interface of AProVE, just click on the corresponding button in the first column. Then you can run AProVE on the respective example yourself. Of those examples, 90 are known to be non-terminating. The corresponding lines contain the remark "(non-term.)". Moreover, 233 examples are known to be terminating, and for 2 examples, the termination behavior is unknown (they are variations of the Collatz function).

When using the AProVE web interface, please keep in mind that the computer running the web interface is considerably slower (four AMD Opteron CPU cores with 2.2GHz each) than the one used for the experiments. Therefore, a higher timeout of up to 600 seconds is needed to solve all examples that AProVE could solve in the table below. Please also keep in mind that the computer used for the web interface is used by several other applications as well, so the runtimes may vary.

TPDB and our examples

Example	AProVE2011-No		AProVE2011		Julia
(non-term.)	NO	1.24	TIMEOUT	60	MAYBE	1.99
(non-term.)	NO	1.8	TIMEOUT	60	MAYBE	2.74
	YES	2.25	YES	1.82	YES	2.39
	TIMEOUT	60	TIMEOUT	60	MAYBE	2.24
	YES	4.64	YES	4.79	YES	2.75
	YES	10.18	YES	10.05	MAYBE	8.08
	YES	5.35	YES	5.13	MAYBE	4.39
	YES	2.19	YES	1.86	YES	2.1
	YES	4.36	YES	2.78	YES	2.1
	YES	2.05	YES	1.87	YES	2.0
	YES	18.13	YES	17.7	YES	2.29
	YES	2.13	YES	1.84	YES	2.07
	YES	9.2	YES	9.22	YES	4.57
	YES	14.4	YES	11.11	MAYBE	5.1
	YES	8.13	YES	8.2	MAYBE	8.0
	YES	5.99	YES	4.74	MAYBE	2.1
	YES	3.0	YES	2.58	MAYBE	2.05
	YES	2.98	YES	2.68	MAYBE	2.04
	TIMEOUT	60	TIMEOUT	60	YES	2.05
	TIMEOUT	60	TIMEOUT	60	MAYBE	2.09
	YES	12.33	YES	11.79	MAYBE	3.49
	YES	2.36	YES	2.28	YES	2.65
	YES	2.05	YES	2.02	YES	2.5
	YES	6.5	YES	6.08	YES	2.69
	YES	2.6	YES	2.65	YES	3.09
	YES	4.66	YES	3.96	MAYBE	2.04
	YES	1.84	YES	1.64	YES	2.06
	YES	2.4	YES	2.26	YES	2.1
	YES	4.68	YES	3.91	MAYBE	2.04
	YES	1.75	YES	1.7	YES	2.12
	TIMEOUT	60	TIMEOUT	60	MAYBE	2.14
	YES	1.81	YES	1.79	YES	1.97
	YES	2.22	YES	1.95	YES	1.99
	TIMEOUT	60	TIMEOUT	60	MAYBE	2.01
	YES	9.28	YES	9.0	MAYBE	4.1
	YES	2.68	YES	18.17	YES	2.26
	YES	6.88	YES	6.35	YES	2.09
	YES	2.15	YES	1.76	YES	1.99
	YES	1.84	YES	1.8	YES	1.89
	YES	1.8	YES	1.8	YES	1.91
	YES	1.77	YES	1.79	YES	1.96
	YES	1.82	YES	1.81	YES	1.95
	YES	1.81	YES	1.87	YES	1.9
	YES	2.19	YES	1.9	YES	1.96
	YES	2.1	YES	1.86	YES	1.95
	YES	3.32	YES	1.97	YES	1.99
	YES	1.88	YES	1.8	YES	1.99
	YES	9.28	YES	6.76	YES	2.04
	YES	2.33	YES	1.83	YES	1.99
	YES	2.63	YES	1.82	YES	2.01
	YES	1.86	YES	1.82	YES	2.01
	YES	2.86	YES	2.24	YES	2.15
	YES	3.95	YES	2.75	YES	2.05
	YES	1.79	YES	1.82	YES	1.93
	YES	1.82	YES	1.79	YES	1.91
	YES	1.99	YES	1.83	YES	1.89
	YES	1.81	YES	1.85	YES	1.89
	YES	1.57	YES	1.52	YES	2.0
	YES	1.79	YES	1.82	YES	1.89
	YES	1.9	YES	1.84	YES	1.94
	YES	2.35	YES	2.1	YES	2.21
	YES	4.09	YES	4.06	YES	2.09
	YES	3.07	YES	2.54	YES	1.99
	YES	3.29	YES	2.34	YES	2.16
	YES	2.9	YES	2.48	YES	2.1
	YES	3.65	YES	3.22	YES	2.09
	TIMEOUT	60	TIMEOUT	60	MAYBE	2.14
	YES	2.66	YES	2.43	YES	2.01
	YES	4.26	YES	3.63	YES	2.09
	YES	2.05	YES	1.87	YES	2.52
	TIMEOUT	60	TIMEOUT	60	MAYBE	1.94
	YES	1.96	YES	1.94	YES	2.55
	YES	13.62	YES	14.7	MAYBE	6.95
	YES	3.27	YES	3.27	YES	3.19
	TIMEOUT	60	TIMEOUT	60	YES	3.36
	YES	1.89	YES	2.0	YES	1.8
	YES	1.84	YES	1.8	YES	2.45
	YES	2.0	YES	1.82	YES	2.27
	YES	1.16	YES	1.15	MAYBE	1.94
	YES	3.79	YES	3.58	YES	2.39
	YES	1.19	YES	1.2	MAYBE	2.25
	YES	1.16	YES	1.16	MAYBE	2.04
	YES	8.65	YES	8.6	YES	4.09
	YES	11.48	YES	12.6	MAYBE	5.3
	YES	1.15	YES	1.15	YES	1.91
	YES	1.15	YES	1.15	YES	1.92
	YES	1.85	YES	1.85	MAYBE	2.19
	YES	6.67	YES	6.23	YES	2.99
	YES	1.16	YES	1.15	YES	1.94
	YES	1.23	YES	1.23	MAYBE	2.51
	YES	1.17	YES	1.17	MAYBE	2.2
	YES	4.36	YES	4.39	MAYBE	2.59
	YES	9.94	YES	9.93	MAYBE	2.87
	YES	1.17	YES	1.16	MAYBE	2.04
	YES	1.22	YES	1.22	MAYBE	2.19
	YES	1.87	YES	1.9	MAYBE	2.2
	YES	2.25	YES	1.89	MAYBE	2.69
	YES	1.15	YES	1.15	MAYBE	2.04
	YES	3.37	YES	2.46	MAYBE	2.52
	YES	7.51	YES	7.54	MAYBE	3.65
	YES	7.1	YES	7.29	MAYBE	4.14
	YES	5.4	YES	5.52	MAYBE	2.63
	YES	13.57	YES	13.45	MAYBE	2.91
	YES	9.0	YES	9.03	MAYBE	6.35
	YES	1.87	YES	1.85	MAYBE	2.26
	YES	2.22	YES	2.21	YES	2.84
	YES	1.16	YES	1.15	MAYBE	2.06
	YES	12.11	YES	11.87	MAYBE	2.44
	YES	4.71	YES	4.61	MAYBE	2.5
	YES	16.33	YES	16.02	MAYBE	3.64
	YES	33.04	YES	33.92	MAYBE	6.32
	YES	11.41	YES	12.0	YES	3.85
	YES	12.51	YES	12.66	YES	2.39
	YES	6.39	YES	6.76	YES	2.8
	YES	2.69	YES	3.25	YES	3.04
	YES	2.76	YES	2.67	YES	2.44
	YES	6.2	YES	6.79	MAYBE	2.81
	YES	1.86	YES	1.82	MAYBE	2.45
	YES	8.01	YES	7.63	MAYBE	3.31
	MAYBE	18.38	MAYBE	18.7	MAYBE	8.5
	YES	14.08	YES	14.35	MAYBE	4.0
	YES	29.58	YES	29.48	YES	3.55
	MAYBE	6.59	MAYBE	6.42	MAYBE	3.54
	YES	18.06	YES	15.92	MAYBE	4.1
	YES	10.88	YES	16.5	MAYBE	3.45
	YES	1.79	YES	1.8	YES	2.16
	YES	2.31	YES	2.35	YES	1.99
	YES	14.38	YES	13.9	MAYBE	4.76
	MAYBE	12.76	MAYBE	12.84	MAYBE	6.35
	YES	6.55	YES	6.62	MAYBE	3.82
	YES	16.08	YES	15.64	MAYBE	3.3
	YES	14.15	YES	14.1	MAYBE	2.6
	YES	4.08	YES	3.86	YES	2.55
	YES	56.83	YES	58.38	MAYBE	3.5
	YES	1.79	YES	1.82	YES	2.14
	YES	2.42	YES	2.49	YES	2.07
	YES	8.57	YES	8.46	MAYBE	2.89
	YES	7.43	YES	7.64	MAYBE	3.04
	YES	6.08	YES	5.86	MAYBE	3.05
	YES	5.13	YES	5.22	MAYBE	2.74
	YES	12.79	YES	12.83	YES	3.39
	MAYBE	10.55	MAYBE	9.63	MAYBE	3.14
	YES	9.87	YES	9.93	MAYBE	3.21
	YES	17.46	YES	14.67	MAYBE	3.22
	YES	1.6	YES	1.59	YES	1.91
	MAYBE	19.2	MAYBE	18.72	MAYBE	5.85
	YES	11.61	YES	11.96	YES	3.04
	YES	5.76	YES	5.5	YES	2.45
	MAYBE	8.86	MAYBE	8.84	YES	2.76
	YES	2.21	YES	2.15	YES	2.02
	YES	1.52	YES	1.59	YES	1.99
(non-term.)	TIMEOUT	60	TIMEOUT	60	MAYBE	1.84
(non-term.)	TIMEOUT	60	TIMEOUT	60	MAYBE	1.9
	YES	3.31	YES	3.19	YES	2.39
	YES	1.67	YES	1.67	YES	2.16
	YES	1.14	YES	1.12	YES	1.79
	YES	5.85	YES	4.35	YES	2.48
	YES	1.15	YES	1.15	YES	1.85
(non-term.)	NO	1.17	MAYBE	6.38	NO	1.84
	YES	8.63	YES	2.0	YES	2.45
	YES	1.81	YES	1.85	YES	2.29
	YES	1.17	YES	1.15	YES	1.89
	YES	1.75	YES	1.73	YES	2.24
(non-term.)	NO	1.22	MAYBE	6.49	MAYBE	1.9
(non-term.)	TIMEOUT	60	TIMEOUT	60	MAYBE	2.99
	YES	1.51	YES	1.49	YES	4.34
(non-term.)	NO	1.31	TIMEOUT	60	MAYBE	1.86
(non-term.)	NO	1.54	TIMEOUT	60	MAYBE	1.84
	YES	1.24	YES	1.51	YES	1.9
(non-term.)	NO	1.54	TIMEOUT	60	MAYBE	1.84
	YES	1.28	YES	1.25	YES	1.89
	YES	1.13	YES	1.14	YES	1.94
(non-term.)	MAYBE	6.31	MAYBE	6.4	MAYBE	1.84
	YES	10.6	YES	10.81	YES	16.96
	YES	8.23	YES	6.68	YES	3.7
	YES	1.59	YES	1.49	YES	1.84
	YES	1.41	YES	1.42	YES	1.94
	YES	1.31	YES	1.39	YES	1.9
	YES	1.16	YES	1.17	YES	2.8
(non-term.)	NO	1.23	MAYBE	6.46	MAYBE	1.85
(non-term.)	NO	1.26	MAYBE	6.37	MAYBE	2.09
(non-term.)	TIMEOUT	60	TIMEOUT	60	MAYBE	3.24
	YES	1.13	YES	1.13	YES	2.09
	YES	1.48	YES	1.49	YES	3.67
	YES	2.33	YES	2.3	YES	2.15
	YES	1.61	YES	1.72	YES	2.6
	YES	1.66	YES	1.63	YES	3.49
	MAYBE	7.89	MAYBE	7.81	YES	22.16
	YES	1.61	YES	1.61	YES	1.94
	YES	1.56	YES	1.59	YES	1.84
	YES	2.09	YES	2.03	YES	1.94
	YES	1.15	YES	1.15	YES	1.99
	YES	1.59	YES	1.56	YES	2.09
	YES	1.14	YES	1.13	YES	4.7
	YES	1.32	YES	1.32	YES	2.45
	YES	1.86	YES	1.49	YES	7.64
	YES	1.4	YES	1.4	YES	5.8
	YES	15.82	YES	13.12	YES	3.76
	YES	21.7	YES	22.06	YES	10.11
	YES	45.6	YES	25.23	YES	3.69
(non-term.)	MAYBE	6.52	MAYBE	6.42	MAYBE	1.95
(non-term.)	MAYBE	7.17	MAYBE	7.15	MAYBE	2.21
	YES	1.74	YES	1.87	YES	2.36
	YES	21.52	YES	21.04	YES	3.85
	YES	20.14	YES	20.01	YES	3.62
	YES	24.46	YES	23.77	YES	4.06
	YES	19.55	YES	19.54	YES	3.66
	YES	21.26	YES	21.27	YES	3.75
	YES	7.1	YES	6.36	YES	3.39
	MAYBE	57.81	MAYBE	55.38	YES	20.16
	TIMEOUT	60	TIMEOUT	60	YES	14.23
	YES	20.65	YES	23.78	YES	7.7
	TIMEOUT	60	TIMEOUT	60	YES	16.01
	YES	1.13	YES	1.13	YES	1.94
	TIMEOUT	60	TIMEOUT	60	YES	28.19
	YES	4.96	YES	4.19	YES	2.85
(non-term.)	TIMEOUT	60	TIMEOUT	60	MAYBE	2.54
	YES	8.89	YES	6.56	YES	3.29
	YES	17.61	YES	21.84	YES	4.74
	YES	21.97	YES	24.43	YES	27.62
	YES	8.06	YES	7.91	YES	3.45
	YES	4.05	YES	4.15	YES	3.09
	YES	9.48	YES	9.4	YES	6.0
	YES	2.73	YES	2.35	YES	2.19
	YES	4.47	YES	4.05	YES	3.85
	YES	8.23	YES	8.01	YES	2.8
	YES	2.26	YES	2.27	YES	2.64
	YES	2.3	YES	2.3	YES	2.64
	YES	2.04	YES	2.02	YES	2.36
	TIMEOUT	60	TIMEOUT	60	YES	20.61
	TIMEOUT	60	TIMEOUT	60	YES	5.8
	TIMEOUT	60	TIMEOUT	60	YES	12.0
	YES	3.69	YES	5.88	YES	3.15
	YES	5.53	YES	5.3	YES	2.46
	YES	27.07	YES	28.92	YES	12.6
	YES	2.96	YES	3.12	YES	2.25
	YES	9.63	YES	9.16	YES	2.76
	YES	3.5	YES	3.56	YES	3.35
	TIMEOUT	60	TIMEOUT	60	YES	9.87
	TIMEOUT	60	TIMEOUT	60	YES	29.5
	YES	28.18	YES	27.55	YES	3.24
	MAYBE	8.9	MAYBE	8.21	YES	57.84
	YES	30.66	YES	30.79	YES	10.62
(non-term.)	NO	5.89	TIMEOUT	60	NO	1.94
(non-term.)	NO	1.26	TIMEOUT	60	NO	2.0
(non-term.)	NO	1.16	MAYBE	6.39	NO	1.88
	YES	33.07	YES	31.46	YES	48.85
(non-term.)	NO	1.18	MAYBE	6.57	NO	1.89
(non-term.)	NO	1.22	MAYBE	6.4	NO	1.79
(non-term.)	NO	1.19	MAYBE	6.52	NO	1.94
(non-term.)	NO	1.16	MAYBE	6.41	NO	1.84
(non-term.)	NO	1.21	MAYBE	6.46	NO	1.84
(non-term.)	NO	1.32	MAYBE	6.4	NO	2.69
(non-term.)	NO	5.01	MAYBE	6.5	NO	1.95
(non-term.)	NO	1.19	MAYBE	6.46	NO	1.89
(non-term.)	NO	6.98	TIMEOUT	60	NO	1.84
(non-term.)	NO	14.22	TIMEOUT	60	NO	1.91
(non-term.)	NO	12.26	TIMEOUT	60	NO	1.91
(non-term.)	NO	3.06	TIMEOUT	60	NO	1.84
(non-term.)	NO	1.15	MAYBE	6.38	NO	1.84
(non-term.)	NO	1.18	MAYBE	6.46	NO	1.79
(non-term.)	NO	2.9	TIMEOUT	60	NO	1.89
(non-term.)	NO	1.2	TIMEOUT	60	NO	1.84
(non-term.)	NO	1.3	TIMEOUT	60	NO	1.92
(non-term.)	NO	1.21	TIMEOUT	60	NO	1.85
	TIMEOUT	60	TIMEOUT	60	YES	4.3
	TIMEOUT	60	TIMEOUT	60	YES	3.44
	TIMEOUT	60	TIMEOUT	60	YES	3.1
	YES	8.25	YES	10.63	YES	2.59
	YES	6.18	YES	6.09	YES	3.95

Invel examples

Example	AProVE2011-No		AProVE2011		Julia		Invel
(non-term.)	NO	1.34	TIMEOUT	60	MAYBE	1.96	NO
(non-term.)	NO	1.25	TIMEOUT	60	MAYBE	2.01	NO
(non-term.)	NO	2.08	TIMEOUT	60	MAYBE	2.08	MAYBE
(non-term.)	NO	1.3	TIMEOUT	60	MAYBE	2.16	MAYBE
(non-term.)	NO	1.34	TIMEOUT	60	MAYBE	2.09	NO
	TIMEOUT	60	TIMEOUT	60	MAYBE	2.09	MAYBE
(non-term.)	NO	1.17	TIMEOUT	60	MAYBE	1.95	NO
(non-term.)	NO	1.21	TIMEOUT	60	MAYBE	1.97	NO
(non-term.)	NO	1.25	TIMEOUT	60	MAYBE	1.94	NO
(non-term.)	NO	3.06	MAYBE	6.35	MAYBE	2.34	MAYBE
(non-term.)	NO	1.2	TIMEOUT	60	MAYBE	1.89	NO
(non-term.)	NO	1.78	TIMEOUT	60	MAYBE	2.05	NO
(non-term.)	NO	2.16	TIMEOUT	60	MAYBE	3.6	MAYBE
(non-term.)	NO	1.58	TIMEOUT	60	MAYBE	2.19	NO
(non-term.)	NO	1.48	TIMEOUT	60	MAYBE	2.19	NO
(non-term.)	NO	1.16	TIMEOUT	60	MAYBE	1.84	NO
(non-term.)	NO	1.45	TIMEOUT	60	MAYBE	2.22	NO
(non-term.)	NO	14.24	MAYBE	6.32	MAYBE	1.84	NO
(non-term.)	NO	1.17	MAYBE	6.35	MAYBE	1.85	NO
(non-term.)	NO	1.57	TIMEOUT	60	MAYBE	2.25	NO
(non-term.)	NO	1.59	TIMEOUT	60	MAYBE	2.15	NO
(non-term.)	NO	3.68	TIMEOUT	60	MAYBE	2.05	NO
(non-term.)	NO	1.23	TIMEOUT	60	MAYBE	1.99	MAYBE
(non-term.)	TIMEOUT	60	TIMEOUT	60	MAYBE	5.54	MAYBE
(non-term.)	NO	1.37	TIMEOUT	60	MAYBE	2.4	NO
(non-term.)	NO	1.78	TIMEOUT	60	MAYBE	2.24	MAYBE
(non-term.)	NO	1.79	TIMEOUT	60	MAYBE	2.14	NO
(non-term.)	NO	1.47	TIMEOUT	60	MAYBE	2.26	NO
(non-term.)	TIMEOUT	60	TIMEOUT	60	MAYBE	3.42	MAYBE
(non-term.)	NO	2.71	TIMEOUT	60	MAYBE	3.7	NO
(non-term.)	NO	1.2	TIMEOUT	60	MAYBE	1.84	NO
(non-term.)	NO	1.16	MAYBE	6.51	MAYBE	1.84	NO
(non-term.)	NO	1.8	TIMEOUT	60	MAYBE	2.14	NO
(non-term.)	NO	1.91	TIMEOUT	60	MAYBE	2.29	MAYBE
(non-term.)	NO	1.31	TIMEOUT	60	MAYBE	1.89	NO
(non-term.)	NO	1.17	TIMEOUT	60	MAYBE	1.94	NO
(non-term.)	NO	1.44	TIMEOUT	60	MAYBE	1.94	NO
(non-term.)	NO	4.34	TIMEOUT	60	MAYBE	2.99	NO
(non-term.)	NO	2.7	TIMEOUT	60	MAYBE	2.04	NO
(non-term.)	NO	2.46	TIMEOUT	60	MAYBE	4.14	MAYBE
(non-term.)	NO	1.42	TIMEOUT	60	MAYBE	1.99	NO
(non-term.)	NO	1.24	TIMEOUT	60	MAYBE	1.84	NO
(non-term.)	NO	1.46	TIMEOUT	60	MAYBE	2.05	NO
(non-term.)	NO	1.45	TIMEOUT	60	MAYBE	2.11	NO
(non-term.)	NO	1.56	TIMEOUT	60	MAYBE	2.09	NO
(non-term.)	NO	1.95	TIMEOUT	60	MAYBE	1.89	NO
	YES	1.46	YES	1.41	YES	1.91	MAYBE
(non-term.)	NO	1.2	TIMEOUT	60	MAYBE	1.86	NO
(non-term.)	NO	1.24	TIMEOUT	60	MAYBE	1.85	NO
(non-term.)	NO	1.34	TIMEOUT	60	MAYBE	1.89	NO
(non-term.)	NO	1.38	TIMEOUT	60	MAYBE	1.89	NO
(non-term.)	NO	1.17	TIMEOUT	60	MAYBE	1.89	NO
(non-term.)	NO	1.17	TIMEOUT	60	MAYBE	1.84	NO
(non-term.)	NO	1.77	TIMEOUT	60	MAYBE	2.41	MAYBE
(non-term.)	NO	1.16	MAYBE	6.42	MAYBE	1.8	NO