# HG changeset patch
# User webertj
# Date 1154438935 -7200
# Node ID 967a3c7fd1f6cc1a4ff644be096923d149bf0f5f
# Parent  d94dc40673b1d90e103bb9f1111f298355319eb3
comment (timing information for last example) added

diff -r d94dc40673b1 -r 967a3c7fd1f6 src/HOL/ex/SAT_Examples.thy
--- a/src/HOL/ex/SAT_Examples.thy	Tue Aug 01 14:58:43 2006 +0200
+++ b/src/HOL/ex/SAT_Examples.thy	Tue Aug 01 15:28:55 2006 +0200
@@ -503,6 +503,11 @@
 200 201 202 203 204
 by sat
 
+(* zchaff_with_proofs: 8705 resolution steps in +++ User 1.173  All 1.194 secs
+   minisat_with_proofs: 40790 resolution steps in +++ User 4.199  All 4.240 secs
+   (as of 2006-08-01, on a 2.5 GHz Pentium 4)
+*)
+
 ML {* Toplevel.profiling := 0; *}
 
 end