Isabelle:
unidentified repository version
58e2d0cd81ae tip
AFP:
bfe8d4f24e47 tip
*** m=1 q=0 ***
Started at Mon Feb 4 17:41:56 CET 2013 (polyml-5.5.0_x86-darwin on lri29-163.lri.fr)
ISABELLE_BUILD_OPTIONS="threads_trace=2 threads=1 parallel_proofs=0"
ML_PLATFORM="x86-darwin"
ML_HOME="/Volumes/Macintosh_HD/Users/makarius/.isabelle/contrib/polyml-5.5.0-3/x86-darwin"
ML_SYSTEM="polyml-5.5.0"
ML_OPTIONS="--minheap 1000 --gcthreads 1"
Session Pure
Session HOL (main)
Session HOL-Auth
Session HOL-Bali
Session HOL-Decision_Procs
Session HOL-Hoare_Parallel
Session HOL-IMP
Session HOL-Library (main)
Session HOL-MicroJava
Session HOL-Multivariate_Analysis (main)
Session HOL-Probability
Session HOL-Nominal (main)
Session HOL-Nominal-Examples
Session HOL-SET_Protocol
Session HOL-UNITY
Session HOL-Proofs
Session HOL-Proofs-Extraction
Session ZF (main)
Session ZF-UNITY
Building Pure ...
Finished Pure (0:00:10 elapsed time, 0:00:08 cpu time, factor 0.80)
Building HOL ...
HOL: theory Code_Generator
HOL: theory HOL
HOL: theory Orderings
HOL: theory Groups
HOL: theory Rings
HOL: theory Fields
HOL: theory Lattices
HOL: theory Set
HOL: theory Complete_Lattices
HOL: theory Fun
HOL: theory Inductive
HOL: theory Typedef
HOL: theory Nat
HOL: theory Product_Type
HOL: theory Complete_Partial_Order
HOL: theory Sum_Type
HOL: theory Datatype
HOL: theory Meson
HOL: theory ATP
HOL: theory Metis
HOL: theory Num
HOL: theory Power
HOL: theory Option
HOL: theory Extraction
HOL: theory Finite_Set
HOL: theory Partial_Function
HOL: theory Relation
HOL: theory Transitive_Closure
HOL: theory Wellfounded
HOL: theory SAT
HOL: theory FunDef
HOL: theory Plain
HOL: theory Big_Operators
HOL: theory Hilbert_Choice
HOL: theory Equiv_Relations
HOL: theory Transfer
HOL: theory Lifting
HOL: theory Quotient
HOL: theory Int
HOL: theory Nat_Transfer
HOL: theory Divides
HOL: theory Code_Numeral
HOL: theory Numeral_Simprocs
HOL: theory Semiring_Normalization
HOL: theory Groebner_Basis
HOL: theory Set_Interval
HOL: theory Presburger
HOL: theory List
HOL: theory Map
HOL: theory Enum
HOL: theory Predicate
HOL: theory Lazy_Sequence
HOL: theory DSequence
HOL: theory New_DSequence
HOL: theory Random
HOL: theory String
HOL: theory Typerep
HOL: theory Code_Evaluation
HOL: theory Quickcheck
HOL: theory Quickcheck_Exhaustive
HOL: theory Quickcheck_Narrowing
HOL: theory Record
HOL: theory SMT
HOL: theory Sledgehammer
HOL: theory Nitpick
HOL: theory Random_Sequence
HOL: theory New_Random_Sequence
HOL: theory Predicate_Compile
HOL: theory Main
HOL: theory Archimedean_Field
HOL: theory Fact
HOL: theory Lubs
HOL: theory Parity
HOL: theory GCD
HOL: theory Rat
HOL: theory RealDef
HOL: theory RComplete
HOL: theory RealVector
HOL: theory Limits
HOL: theory Real
HOL: theory SEQ
HOL: theory Lim
HOL: theory Deriv
HOL: theory Series
HOL: theory SupInf
HOL: theory NthRoot
HOL: theory Transcendental
HOL: theory Complex
HOL: theory Ln
HOL: theory Log
HOL: theory MacLaurin
HOL: theory Taylor
HOL: theory Complex_Main
Timing HOL (1 threads, 210.601s elapsed time, 210.586s cpu time, 9.116s GC time, factor 1.00)
Finished HOL (0:03:59 elapsed time, 0:03:58 cpu time, factor 0.99)
Building HOL-Multivariate_Analysis ...
HOL-Multivariate_Analysis: theory Extended_Nat
HOL-Multivariate_Analysis: theory FuncSet
HOL-Multivariate_Analysis: theory Indicator_Function
HOL-Multivariate_Analysis: theory Infinite_Set
HOL-Multivariate_Analysis: theory Glbs
HOL-Multivariate_Analysis: theory Nat_Bijection
HOL-Multivariate_Analysis: theory Countable
HOL-Multivariate_Analysis: theory Countable_Set
HOL-Multivariate_Analysis: theory L2_Norm
HOL-Multivariate_Analysis: theory Extended_Real
HOL-Multivariate_Analysis: theory FrechetDeriv
HOL-Multivariate_Analysis: theory Inner_Product
HOL-Multivariate_Analysis: theory Sum_of_Squares
HOL-Multivariate_Analysis: theory Norm_Arith
HOL-Multivariate_Analysis: theory Permutations
HOL-Multivariate_Analysis: theory Phantom_Type
HOL-Multivariate_Analysis: theory Cardinality
HOL-Multivariate_Analysis: theory Numeral_Type
HOL-Multivariate_Analysis: theory Product_plus
HOL-Multivariate_Analysis: theory Product_Vector
HOL-Multivariate_Analysis: theory Convex
HOL-Multivariate_Analysis: theory Euclidean_Space
HOL-Multivariate_Analysis: theory Finite_Cartesian_Product
HOL-Multivariate_Analysis: theory Linear_Algebra
HOL-Multivariate_Analysis: theory Operator_Norm
HOL-Multivariate_Analysis: theory Topology_Euclidean_Space
HOL-Multivariate_Analysis: theory Extended_Real_Limits
HOL-Multivariate_Analysis: theory Set_Algebras
HOL-Multivariate_Analysis: theory Convex_Euclidean_Space
HOL-Multivariate_Analysis: theory Brouwer_Fixpoint
HOL-Multivariate_Analysis: theory Derivative
HOL-Multivariate_Analysis: theory Integration
HOL-Multivariate_Analysis: theory Cartesian_Euclidean_Space
HOL-Multivariate_Analysis: theory Determinants
HOL-Multivariate_Analysis: theory Path_Connected
HOL-Multivariate_Analysis: theory Fashoda
HOL-Multivariate_Analysis: theory Multivariate_Analysis
Timing HOL-Multivariate_Analysis (1 threads, 176.812s elapsed time, 176.811s cpu time, 4.212s GC time, factor 1.00)
Finished HOL-Multivariate_Analysis (0:03:13 elapsed time, 0:03:10 cpu time, factor 0.98)
Building HOL-Nominal ...
HOL-Nominal: theory Infinite_Set
HOL-Nominal: theory Nominal
Timing HOL-Nominal (1 threads, 7.722s elapsed time, 7.722s cpu time, 0.336s GC time, factor 1.00)
Finished HOL-Nominal (0:00:17 elapsed time, 0:00:15 cpu time, factor 0.88)
Building HOL-Proofs ...
HOL-Proofs: theory Code_Generator
HOL-Proofs: theory HOL
HOL-Proofs: theory Orderings
HOL-Proofs: theory Groups
HOL-Proofs: theory Rings
HOL-Proofs: theory Fields
HOL-Proofs: theory Lattices
HOL-Proofs: theory Set
HOL-Proofs: theory Complete_Lattices
HOL-Proofs: theory Fun
HOL-Proofs: theory Inductive
HOL-Proofs: theory Typedef
HOL-Proofs: theory Nat
HOL-Proofs: theory Product_Type
HOL-Proofs: theory Complete_Partial_Order
HOL-Proofs: theory Sum_Type
HOL-Proofs: theory Datatype
HOL-Proofs: theory Meson
HOL-Proofs: theory ATP
HOL-Proofs: theory Metis
HOL-Proofs: theory Num
HOL-Proofs: theory Power
HOL-Proofs: theory Option
HOL-Proofs: theory Extraction
HOL-Proofs: theory Finite_Set
HOL-Proofs: theory Partial_Function
HOL-Proofs: theory Relation
HOL-Proofs: theory Transitive_Closure
HOL-Proofs: theory Wellfounded
HOL-Proofs: theory SAT
HOL-Proofs: theory FunDef
HOL-Proofs: theory Plain
HOL-Proofs: theory Big_Operators
HOL-Proofs: theory Hilbert_Choice
HOL-Proofs: theory Equiv_Relations
HOL-Proofs: theory Transfer
HOL-Proofs: theory Lifting
HOL-Proofs: theory Quotient
HOL-Proofs: theory Int
HOL-Proofs: theory Nat_Transfer
HOL-Proofs: theory Divides
HOL-Proofs: theory Code_Numeral
HOL-Proofs: theory Numeral_Simprocs
HOL-Proofs: theory Semiring_Normalization
HOL-Proofs: theory Groebner_Basis
HOL-Proofs: theory Set_Interval
HOL-Proofs: theory Presburger
HOL-Proofs: theory List
HOL-Proofs: theory Map
HOL-Proofs: theory Enum
HOL-Proofs: theory Predicate
HOL-Proofs: theory Lazy_Sequence
HOL-Proofs: theory DSequence
HOL-Proofs: theory New_DSequence
HOL-Proofs: theory Random
HOL-Proofs: theory String
HOL-Proofs: theory Typerep
HOL-Proofs: theory Code_Evaluation
HOL-Proofs: theory Quickcheck
HOL-Proofs: theory Quickcheck_Exhaustive
HOL-Proofs: theory Quickcheck_Narrowing
HOL-Proofs: theory Record
HOL-Proofs: theory SMT
HOL-Proofs: theory Sledgehammer
HOL-Proofs: theory Nitpick
HOL-Proofs: theory Random_Sequence
HOL-Proofs: theory New_Random_Sequence
HOL-Proofs: theory Predicate_Compile
HOL-Proofs: theory Main
Timing HOL-Proofs (1 threads, 474.331s elapsed time, 474.238s cpu time, 28.983s GC time, factor 1.00)
Finished HOL-Proofs (0:08:33 elapsed time, 0:08:31 cpu time, factor 0.99)
Building ZF ...
ZF: theory IFOL
ZF: theory FOL
ZF: theory ZF
ZF: theory upair
ZF: theory pair
ZF: theory Bool
ZF: theory equalities
ZF: theory Fixedpt
ZF: theory Sum
ZF: theory func
ZF: theory Perm
ZF: theory Trancl
ZF: theory EquivClass
ZF: theory WF
ZF: theory Order
ZF: theory Ordinal
ZF: theory OrdQuant
ZF: theory Nat_ZF
ZF: theory Epsilon
ZF: theory OrderArith
ZF: theory OrderType
ZF: theory QPair
ZF: theory Inductive_ZF
ZF: theory Finite
ZF: theory Cardinal
ZF: theory Univ
ZF: theory Arith
ZF: theory ArithSimp
ZF: theory Int_ZF
ZF: theory CardinalArith
ZF: theory QUniv
ZF: theory Datatype_ZF
ZF: theory Bin
ZF: theory IntArith
ZF: theory IntDiv_ZF
ZF: theory List_ZF
ZF: theory Main_ZF
ZF: theory AC
ZF: theory Zorn
ZF: theory Cardinal_AC
ZF: theory InfDatatype
ZF: theory Main
ZF: theory Main_ZFC
Timing ZF (1 threads, 25.719s elapsed time, 25.365s cpu time, 0.760s GC time, factor 0.99)
Finished ZF (0:00:29 elapsed time, 0:00:27 cpu time, factor 0.93)
Running HOL-Nominal-Examples ...
HOL-Nominal-Examples: theory CK_Machine
HOL-Nominal-Examples: theory CR_Takahashi
HOL-Nominal-Examples: theory Class1
HOL-Nominal-Examples: theory Class2
HOL-Nominal-Examples: theory Class3
HOL-Nominal-Examples: theory Compile
HOL-Nominal-Examples: theory Contexts
HOL-Nominal-Examples: theory Crary
HOL-Nominal-Examples: theory Fsub
HOL-Nominal-Examples: theory Height
HOL-Nominal-Examples: theory Lam_Funs
HOL-Nominal-Examples: theory CR
HOL-Nominal-Examples: theory SN
HOL-Nominal-Examples: theory Lambda_mu
HOL-Nominal-Examples: theory LocalWeakening
HOL-Nominal-Examples: theory Pattern
HOL-Nominal-Examples: theory SOS
HOL-Nominal-Examples: theory Standardization
HOL-Nominal-Examples: theory Support
HOL-Nominal-Examples: theory Type_Preservation
HOL-Nominal-Examples: theory W
HOL-Nominal-Examples: theory Weakening
HOL-Nominal-Examples: theory Nominal_Examples
HOL-Nominal-Examples: theory VC_Condition
Timing HOL-Nominal-Examples (1 threads, 525.252s elapsed time, 525.166s cpu time, 20.632s GC time, factor 1.00)
Finished HOL-Nominal-Examples (0:08:47 elapsed time, 0:08:45 cpu time, factor 0.99)
Running HOL-Auth ...
HOL-Auth: theory Message
HOL-Auth: theory All_Symmetric
HOL-Auth: theory Event
HOL-Auth: theory Extensions
HOL-Auth: theory Analz
HOL-Auth: theory Guard
HOL-Auth: theory GuardK
HOL-Auth: theory List_Msg
HOL-Auth: theory Public
HOL-Auth: theory CertifiedEmail
HOL-Auth: theory Guard_Public
HOL-Auth: theory Guard_NS_Public
HOL-Auth: theory P2
HOL-Auth: theory Proto
HOL-Auth: theory KerberosIV
HOL-Auth: theory KerberosIV_Gets
HOL-Auth: theory KerberosV
HOL-Auth: theory Kerberos_BAN
HOL-Auth: theory Kerberos_BAN_Gets
HOL-Auth: theory NS_Public
HOL-Auth: theory NS_Public_Bad
HOL-Auth: theory NS_Shared
HOL-Auth: theory OtwayRees
HOL-Auth: theory OtwayReesBella
HOL-Auth: theory OtwayRees_AN
HOL-Auth: theory OtwayRees_Bad
HOL-Auth: theory P1
HOL-Auth: theory Auth_Guard_Public
HOL-Auth: theory Recur
HOL-Auth: theory WooLam
HOL-Auth: theory Yahalom
HOL-Auth: theory Yahalom2
HOL-Auth: theory Yahalom_Bad
HOL-Auth: theory ZhouGollmann
HOL-Auth: theory Auth_Shared
HOL-Auth: theory Shared
HOL-Auth: theory Guard_Shared
HOL-Auth: theory Guard_OtwayRees
HOL-Auth: theory Guard_Yahalom
HOL-Auth: theory Auth_Guard_Shared
HOL-Auth: theory EventSC
HOL-Auth: theory Smartcard
HOL-Auth: theory ShoupRubin
HOL-Auth: theory ShoupRubinBella
HOL-Auth: theory Auth_Smartcard
HOL-Auth: theory Nat_Bijection
HOL-Auth: theory TLS
HOL-Auth: theory Auth_Public
Timing HOL-Auth (1 threads, 227.957s elapsed time, 227.954s cpu time, 5.676s GC time, factor 1.00)
Finished HOL-Auth (0:03:50 elapsed time, 0:03:48 cpu time, factor 0.99)
Running HOL-Bali ...
HOL-Bali: theory Wfrec
HOL-Bali: theory Old_Recdef
HOL-Bali: theory Basis
HOL-Bali: theory Name
HOL-Bali: theory Type
HOL-Bali: theory Value
HOL-Bali: theory Table
HOL-Bali: theory Term
HOL-Bali: theory Decl
HOL-Bali: theory TypeRel
HOL-Bali: theory DeclConcepts
HOL-Bali: theory State
HOL-Bali: theory Conform
HOL-Bali: theory Eval
HOL-Bali: theory WellType
HOL-Bali: theory DefiniteAssignment
HOL-Bali: theory WellForm
HOL-Bali: theory DefiniteAssignmentCorrect
HOL-Bali: theory TypeSafe
HOL-Bali: theory Evaln
HOL-Bali: theory AxSem
HOL-Bali: theory AxCompl
HOL-Bali: theory AxSound
HOL-Bali: theory Trans
HOL-Bali: theory Example
HOL-Bali: theory AxExample
Timing HOL-Bali (1 threads, 142.156s elapsed time, 142.157s cpu time, 3.687s GC time, factor 1.00)
Finished HOL-Bali (0:02:23 elapsed time, 0:02:23 cpu time, factor 1.00)
Running HOL-Decision_Procs ...
HOL-Decision_Procs: theory Code_Binary_Nat
HOL-Decision_Procs: theory Code_Natural
HOL-Decision_Procs: theory Code_Integer
HOL-Decision_Procs: theory DP_Library
HOL-Decision_Procs: theory Dense_Linear_Order
HOL-Decision_Procs: theory Dense_Linear_Order_Ex
HOL-Decision_Procs: theory Efficient_Nat
HOL-Decision_Procs: theory Commutative_Ring
HOL-Decision_Procs: theory Commutative_Ring_Complete
HOL-Decision_Procs: theory Commutative_Ring_Ex
HOL-Decision_Procs: theory Abstract_Rat
HOL-Decision_Procs: theory Lattice_Algebras
HOL-Decision_Procs: theory Float
HOL-Decision_Procs: theory Polynomial_List
HOL-Decision_Procs: theory Reflected_Multivariate_Polynomial
HOL-Decision_Procs: theory Reflection
HOL-Decision_Procs: theory Approximation
HOL-Decision_Procs: theory Approximation_Ex
HOL-Decision_Procs: theory Wfrec
HOL-Decision_Procs: theory Old_Recdef
HOL-Decision_Procs: theory Cooper
HOL-Decision_Procs: theory Ferrack
HOL-Decision_Procs: theory MIR
HOL-Decision_Procs: theory Parametric_Ferrante_Rackoff
HOL-Decision_Procs: theory Decision_Procs
Timing HOL-Decision_Procs (1 threads, 415.680s elapsed time, 415.676s cpu time, 16.813s GC time, factor 1.00)
Finished HOL-Decision_Procs (0:06:57 elapsed time, 0:06:56 cpu time, factor 0.99)
Running HOL-Hoare_Parallel ...
HOL-Hoare_Parallel: theory Graph
HOL-Hoare_Parallel: theory OG_Com
HOL-Hoare_Parallel: theory OG_Tran
HOL-Hoare_Parallel: theory OG_Hoare
HOL-Hoare_Parallel: theory OG_Tactics
HOL-Hoare_Parallel: theory Quote_Antiquote
HOL-Hoare_Parallel: theory OG_Syntax
HOL-Hoare_Parallel: theory Gar_Coll
HOL-Hoare_Parallel: theory Mul_Gar_Coll
HOL-Hoare_Parallel: theory OG_Examples
HOL-Hoare_Parallel: theory RG_Com
HOL-Hoare_Parallel: theory RG_Tran
HOL-Hoare_Parallel: theory RG_Hoare
HOL-Hoare_Parallel: theory RG_Syntax
HOL-Hoare_Parallel: theory RG_Examples
HOL-Hoare_Parallel: theory Hoare_Parallel
Timing HOL-Hoare_Parallel (1 threads, 218.796s elapsed time, 218.796s cpu time, 2.565s GC time, factor 1.00)
Finished HOL-Hoare_Parallel (0:03:40 elapsed time, 0:03:39 cpu time, factor 0.99)
Running HOL-IMP ...
HOL-IMP: theory Char_nat
HOL-IMP: theory Char_ord
HOL-IMP: theory List_lexord
HOL-IMP: theory While_Combinator
HOL-IMP: theory Interpretation_with_Defs
HOL-IMP: theory AExp
HOL-IMP: theory ASM
HOL-IMP: theory BExp
HOL-IMP: theory Com
HOL-IMP: theory ACom
HOL-IMP: theory ACom_ITP
HOL-IMP: theory Abs_Int_Tests
HOL-IMP: theory Big_Step
HOL-IMP: theory Compiler
HOL-IMP: theory Comp_Rev
HOL-IMP: theory Denotation
HOL-IMP: theory Hoare
HOL-IMP: theory Hoare_Examples
HOL-IMP: theory Hoare_Sound_Complete
HOL-IMP: theory HoareT
HOL-IMP: theory VC
HOL-IMP: theory Sec_Type_Expr
HOL-IMP: theory Sec_Typing
HOL-IMP: theory Sec_TypingT
HOL-IMP: theory Sem_Equiv
HOL-IMP: theory Fold
HOL-IMP: theory Procs
HOL-IMP: theory Procs_Dyn_Vars_Dyn
HOL-IMP: theory Procs_Stat_Vars_Dyn
HOL-IMP: theory Procs_Stat_Vars_Stat
HOL-IMP: theory Vars
HOL-IMP: theory Def_Init
HOL-IMP: theory Def_Init_Exp
HOL-IMP: theory Def_Init_Big
HOL-IMP: theory Def_Init_Sound_Big
HOL-IMP: theory Live
HOL-IMP: theory C_like
HOL-IMP: theory Complete_Lattice
HOL-IMP: theory Collecting
HOL-IMP: theory Collecting1
HOL-IMP: theory Collecting_Examples
HOL-IMP: theory Complete_Lattice_ix
HOL-IMP: theory Collecting_ITP
HOL-IMP: theory OO
HOL-IMP: theory Star
HOL-IMP: theory Def_Init_Small
HOL-IMP: theory Def_Init_Sound_Small
HOL-IMP: theory Small_Step
HOL-IMP: theory Finite_Reachable
HOL-IMP: theory Types
HOL-IMP: theory Poly_Types
HOL-IMP: theory Live_True
HOL-IMP: theory Abs_Int0_ITP
HOL-IMP: theory Abs_State_ITP
HOL-IMP: theory Abs_Int1_ITP
HOL-IMP: theory Abs_Int1_const_ITP
HOL-IMP: theory Abs_Int1_parity_ITP
HOL-IMP: theory Abs_Int2_ITP
HOL-IMP: theory Abs_Int2_ivl_ITP
HOL-IMP: theory Abs_Int3_ITP
HOL-IMP: theory Abs_Int_den0_fun
HOL-IMP: theory Abs_State_den
HOL-IMP: theory Abs_Int_den0
HOL-IMP: theory Abs_Int_den0_const
HOL-IMP: theory Abs_Int_den1
HOL-IMP: theory Abs_Int_den1_ivl
HOL-IMP: theory Abs_Int_den2
HOL-IMP: theory Abs_Int_init
HOL-IMP: theory Abs_Int0
HOL-IMP: theory Abs_State
HOL-IMP: theory Abs_Int1
HOL-IMP: theory Abs_Int1_const
HOL-IMP: theory Abs_Int1_parity
HOL-IMP: theory Abs_Int2
HOL-IMP: theory Abs_Int2_ivl
HOL-IMP: theory Abs_Int3
Timing HOL-IMP (1 threads, 441.076s elapsed time, 439.701s cpu time, 19.318s GC time, factor 1.00)
Finished HOL-IMP (0:07:22 elapsed time, 0:07:20 cpu time, factor 0.99)
Running HOL-Library ...
HOL-Library: theory Adhoc_Overloading
HOL-Library: theory Lattice_Syntax
HOL-Library: theory Preorder
HOL-Library: theory Refute
HOL-Library: theory AList
HOL-Library: theory DAList
HOL-Library: theory Bit
HOL-Library: theory Boolean_Algebra
HOL-Library: theory Char_nat
HOL-Library: theory Char_ord
HOL-Library: theory Code_Binary_Nat
HOL-Library: theory Code_Char
HOL-Library: theory Code_Char_ord
HOL-Library: theory Code_Natural
HOL-Library: theory Code_Integer
HOL-Library: theory Code_Char_chr
HOL-Library: theory Code_Numeral_Types
HOL-Library: theory Code_Target_Int
HOL-Library: theory Code_Target_Nat
HOL-Library: theory Code_Target_Numeral
HOL-Library: theory Continuity
HOL-Library: theory Debug
HOL-Library: theory Dlist
HOL-Library: theory Efficient_Nat
HOL-Library: theory IArray
HOL-Library: theory Eval_Witness
HOL-Library: theory Extended_Nat
HOL-Library: theory Fraction_Field
HOL-Library: theory FuncSet
HOL-Library: theory Function_Algebras
HOL-Library: theory Function_Division
HOL-Library: theory Indicator_Function
HOL-Library: theory Infinite_Set
HOL-Library: theory Kleene_Algebra
HOL-Library: theory LaTeXsugar
HOL-Library: theory ListVector
HOL-Library: theory List_lexord
HOL-Library: theory Monad_Syntax
HOL-Library: theory Multiset
HOL-Library: theory Option_ord
HOL-Library: theory Order_Relation
HOL-Library: theory Zorn
HOL-Library: theory Parallel
HOL-Library: theory Diagonal_Subsequence
HOL-Library: theory Nat_Bijection
HOL-Library: theory Countable
HOL-Library: theory Countable_Set
HOL-Library: theory Abstract_Rat
HOL-Library: theory Binomial
HOL-Library: theory Code_Real_Approx_By_Float
HOL-Library: theory ContNotDenum
HOL-Library: theory Formal_Power_Series
HOL-Library: theory FrechetDeriv
HOL-Library: theory Inner_Product
HOL-Library: theory Lattice_Algebras
HOL-Library: theory Float
HOL-Library: theory OptionalSugar
HOL-Library: theory Sum_of_Squares
HOL-Library: theory Permutations
HOL-Library: theory Permutation
HOL-Library: theory Phantom_Type
HOL-Library: theory Cardinality
HOL-Library: theory FinFun
HOL-Library: theory Numeral_Type
HOL-Library: theory Type_Length
HOL-Library: theory Polynomial
HOL-Library: theory Fundamental_Theorem_Algebra
HOL-Library: theory Poly_Deriv
HOL-Library: theory Product_plus
HOL-Library: theory Product_Lattice
HOL-Library: theory Finite_Lattice
HOL-Library: theory Product_Vector
HOL-Library: theory Convex
HOL-Library: theory Quotient_Syntax
HOL-Library: theory Quotient_Option
HOL-Library: theory Mapping
HOL-Library: theory AList_Mapping
HOL-Library: theory Quotient_Product
HOL-Library: theory Quotient_Set
HOL-Library: theory Quotient_List
HOL-Library: theory Quotient_Sum
HOL-Library: theory Quotient_Type
HOL-Library: theory RBT_Impl
HOL-Library: theory RBT
HOL-Library: theory RBT_Mapping
HOL-Library: theory Ramsey
HOL-Library: theory Reflection
HOL-Library: theory Saturated
HOL-Library: theory Set_Algebras
HOL-Library: theory BigO
HOL-Library: theory State_Monad
HOL-Library: theory Sublist
HOL-Library: theory Sublist_Order
HOL-Library: theory Transitive_Closure_Table
HOL-Library: theory Univ_Poly
HOL-Library: theory Wfrec
HOL-Library: theory Old_Recdef
HOL-Library: theory While_Combinator
HOL-Library: theory Library
Skipping theories "Sum_of_Squares_Remote" (undefined ISABELLE_FULL_TEST)
Timing HOL-Library (1 threads, 220.468s elapsed time, 220.426s cpu time, 6.360s GC time, factor 1.00)
Finished HOL-Library (0:03:42 elapsed time, 0:03:41 cpu time, factor 0.99)
Running HOL-MicroJava ...
HOL-MicroJava: theory While_Combinator
HOL-MicroJava: theory Transitive_Closure_Table
HOL-MicroJava: theory JBasis
HOL-MicroJava: theory AuxLemmas
HOL-MicroJava: theory Type
HOL-MicroJava: theory Decl
HOL-MicroJava: theory SystemClasses
HOL-MicroJava: theory Value
HOL-MicroJava: theory Term
HOL-MicroJava: theory Wfrec
HOL-MicroJava: theory TypeRel
HOL-MicroJava: theory State
HOL-MicroJava: theory Exceptions
HOL-MicroJava: theory WellForm
HOL-MicroJava: theory WellType
HOL-MicroJava: theory Conform
HOL-MicroJava: theory JVMState
HOL-MicroJava: theory JVMInstructions
HOL-MicroJava: theory JVMExceptions
HOL-MicroJava: theory JVMExecInstr
HOL-MicroJava: theory JVMExec
HOL-MicroJava: theory DefsComp
HOL-MicroJava: theory Index
HOL-MicroJava: theory JVMDefensive
HOL-MicroJava: theory JVMListExample
HOL-MicroJava: theory Eval
HOL-MicroJava: theory Example
HOL-MicroJava: theory JListExample
HOL-MicroJava: theory JTypeSafe
HOL-MicroJava: theory TypeInf
HOL-MicroJava: theory Semilat
HOL-MicroJava: theory Err
HOL-MicroJava: theory Listn
HOL-MicroJava: theory Typing_Framework
HOL-MicroJava: theory Opt
HOL-MicroJava: theory Product
HOL-MicroJava: theory SemilatAlg
HOL-MicroJava: theory Kildall
HOL-MicroJava: theory LBVSpec
HOL-MicroJava: theory LBVComplete
HOL-MicroJava: theory LBVCorrect
HOL-MicroJava: theory Typing_Framework_err
HOL-MicroJava: theory Abstract_BV
HOL-MicroJava: theory Semilattices
HOL-MicroJava: theory JType
HOL-MicroJava: theory JVMType
HOL-MicroJava: theory Effect
HOL-MicroJava: theory BVSpec
HOL-MicroJava: theory Altern
HOL-MicroJava: theory Correct
HOL-MicroJava: theory BVSpecTypeSafe
HOL-MicroJava: theory BVNoTypeError
HOL-MicroJava: theory EffectMono
HOL-MicroJava: theory TranslCompTp
HOL-MicroJava: theory TranslComp
HOL-MicroJava: theory LemmasComp
HOL-MicroJava: theory CorrComp
HOL-MicroJava: theory Typing_Framework_JVM
HOL-MicroJava: theory JVM
HOL-MicroJava: theory BVExample
HOL-MicroJava: theory CorrCompTp
HOL-MicroJava: theory LBVJVM
HOL-MicroJava: theory MicroJava
Timing HOL-MicroJava (1 threads, 218.028s elapsed time, 217.987s cpu time, 5.350s GC time, factor 1.00)
Finished HOL-MicroJava (0:03:40 elapsed time, 0:03:38 cpu time, factor 0.99)
Running HOL-Probability ...
HOL-Probability: theory AList
HOL-Probability: theory DAList
HOL-Probability: theory Multiset
HOL-Probability: theory Permutation
HOL-Probability: theory Diagonal_Subsequence
HOL-Probability: theory Sigma_Algebra
HOL-Probability: theory Measurable
HOL-Probability: theory Measure_Space
HOL-Probability: theory Caratheodory
HOL-Probability: theory Borel_Space
HOL-Probability: theory Lebesgue_Integration
HOL-Probability: theory Binary_Product_Measure
HOL-Probability: theory Finite_Product_Measure
HOL-Probability: theory Fin_Map
HOL-Probability: theory Lebesgue_Measure
HOL-Probability: theory Complete_Measure
HOL-Probability: theory Radon_Nikodym
HOL-Probability: theory Probability_Measure
HOL-Probability: theory Distributions
HOL-Probability: theory Projective_Family
HOL-Probability: theory Infinite_Product_Measure
HOL-Probability: theory Independent_Family
HOL-Probability: theory Information
HOL-Probability: theory Dining_Cryptographers
HOL-Probability: theory Koepf_Duermuth_Countermeasure
HOL-Probability: theory Regularity
HOL-Probability: theory Projective_Limit
HOL-Probability: theory Discrete_Topology
HOL-Probability: theory Probability
Timing HOL-Probability (1 threads, 157.890s elapsed time, 157.892s cpu time, 3.521s GC time, factor 1.00)
Finished HOL-Probability (0:02:40 elapsed time, 0:02:39 cpu time, factor 0.99)
Running HOL-Proofs-Extraction ...
HOL-Proofs-Extraction: theory Adhoc_Overloading
HOL-Proofs-Extraction: theory AList
HOL-Proofs-Extraction: theory DAList
HOL-Proofs-Extraction: theory Code_Binary_Nat
HOL-Proofs-Extraction: theory Code_Natural
HOL-Proofs-Extraction: theory Code_Integer
HOL-Proofs-Extraction: theory Efficient_Nat
HOL-Proofs-Extraction: theory Fact
HOL-Proofs-Extraction: theory Monad_Syntax
HOL-Proofs-Extraction: theory Multiset
HOL-Proofs-Extraction: theory Parity
HOL-Proofs-Extraction: theory GCD
HOL-Proofs-Extraction: theory Primes
HOL-Proofs-Extraction: theory Cong
HOL-Proofs-Extraction: theory UniqueFactorization
HOL-Proofs-Extraction: theory State_Monad
HOL-Proofs-Extraction: theory Higman
HOL-Proofs-Extraction: theory Higman_Extraction
HOL-Proofs-Extraction: theory Util
HOL-Proofs-Extraction: theory Euclid
HOL-Proofs-Extraction: theory Pigeonhole
HOL-Proofs-Extraction: theory QuotRem
HOL-Proofs-Extraction: theory Greatest_Common_Divisor
HOL-Proofs-Extraction: theory Warshall
Timing HOL-Proofs-Extraction (1 threads, 314.309s elapsed time, 314.311s cpu time, 14.862s GC time, factor 1.00)
Finished HOL-Proofs-Extraction (0:05:16 elapsed time, 0:05:14 cpu time, factor 0.99)
Running HOL-SET_Protocol ...
HOL-SET_Protocol: theory Nat_Bijection
HOL-SET_Protocol: theory Message_SET
HOL-SET_Protocol: theory Event_SET
HOL-SET_Protocol: theory Public_SET
HOL-SET_Protocol: theory Cardholder_Registration
HOL-SET_Protocol: theory Merchant_Registration
HOL-SET_Protocol: theory Purchase
HOL-SET_Protocol: theory SET_Protocol
Timing HOL-SET_Protocol (1 threads, 69.571s elapsed time, 69.573s cpu time, 1.015s GC time, factor 1.00)
Finished HOL-SET_Protocol (0:01:11 elapsed time, 0:01:09 cpu time, factor 0.97)
Running HOL-UNITY ...
HOL-UNITY: theory Message
HOL-UNITY: theory Event
HOL-UNITY: theory Public
HOL-UNITY: theory AList
HOL-UNITY: theory DAList
HOL-UNITY: theory ListOrder
HOL-UNITY: theory Multiset
HOL-UNITY: theory UNITY
HOL-UNITY: theory Constrains
HOL-UNITY: theory Deadlock
HOL-UNITY: theory FP
HOL-UNITY: theory Network
HOL-UNITY: theory WFair
HOL-UNITY: theory SubstAx
HOL-UNITY: theory Detects
HOL-UNITY: theory Follows
HOL-UNITY: theory Union
HOL-UNITY: theory Comp
HOL-UNITY: theory Guar
HOL-UNITY: theory Extend
HOL-UNITY: theory Project
HOL-UNITY: theory ELT
HOL-UNITY: theory Rename
HOL-UNITY: theory Lift_prog
HOL-UNITY: theory PPROD
HOL-UNITY: theory Transformers
HOL-UNITY: theory ProgressSets
HOL-UNITY: theory UNITY_Main
HOL-UNITY: theory AllocBase
HOL-UNITY: theory Alloc
HOL-UNITY: theory AllocImpl
HOL-UNITY: theory Client
HOL-UNITY: theory Channel
HOL-UNITY: theory Common
HOL-UNITY: theory Counter
HOL-UNITY: theory Counterc
HOL-UNITY: theory Handshake
HOL-UNITY: theory Lift
HOL-UNITY: theory Mutex
HOL-UNITY: theory NSP_Bad
HOL-UNITY: theory PriorityAux
HOL-UNITY: theory Priority
HOL-UNITY: theory Progress
HOL-UNITY: theory Reach
HOL-UNITY: theory Reachability
HOL-UNITY: theory TimerArray
HOL-UNITY: theory Token
Timing HOL-UNITY (1 threads, 68.615s elapsed time, 68.616s cpu time, 1.881s GC time, factor 1.00)
Finished HOL-UNITY (0:01:10 elapsed time, 0:01:08 cpu time, factor 0.97)
Running ZF-UNITY ...
ZF-UNITY: theory Acc
ZF-UNITY: theory FoldSet
ZF-UNITY: theory Multiset
ZF-UNITY: theory MultisetSum
ZF-UNITY: theory GenPrefix
ZF-UNITY: theory Monotonicity
ZF-UNITY: theory State
ZF-UNITY: theory UNITY
ZF-UNITY: theory Constrains
ZF-UNITY: theory Increasing
ZF-UNITY: theory FP
ZF-UNITY: theory WFair
ZF-UNITY: theory SubstAx
ZF-UNITY: theory Follows
ZF-UNITY: theory Mutex
ZF-UNITY: theory Union
ZF-UNITY: theory Comp
ZF-UNITY: theory Guar
ZF-UNITY: theory AllocBase
ZF-UNITY: theory ClientImpl
ZF-UNITY: theory AllocImpl
ZF-UNITY: theory Distributor
ZF-UNITY: theory Merge
Timing ZF-UNITY (1 threads, 30.067s elapsed time, 30.067s cpu time, 0.546s GC time, factor 1.00)
Finished ZF-UNITY (0:00:31 elapsed time, 0:00:29 cpu time, factor 0.93)
Finished at Mon Feb 4 18:50:05 CET 2013
1:08:08 elapsed time, 1:08:05 cpu time, factor 0.99
*** m=2 q=2 ***
Started at Mon Feb 4 18:50:05 CET 2013 (polyml-5.5.0_x86-darwin on lri29-163.lri.fr)
ISABELLE_BUILD_OPTIONS="threads_trace=2 threads=2 parallel_proofs=2"
ML_PLATFORM="x86-darwin"
ML_HOME="/Volumes/Macintosh_HD/Users/makarius/.isabelle/contrib/polyml-5.5.0-3/x86-darwin"
ML_SYSTEM="polyml-5.5.0"
ML_OPTIONS="--minheap 1000 --gcthreads 2"
Session Pure
Session HOL (main)
Session HOL-Auth
Session HOL-Bali
Session HOL-Decision_Procs
Session HOL-Hoare_Parallel
Session HOL-IMP
Session HOL-Library (main)
Session HOL-MicroJava
Session HOL-Multivariate_Analysis (main)
Session HOL-Probability
Session HOL-Nominal (main)
Session HOL-Nominal-Examples
Session HOL-SET_Protocol
Session HOL-UNITY
Session HOL-Proofs
Session HOL-Proofs-Extraction
Session ZF (main)
Session ZF-UNITY
Building Pure ...
Finished Pure (0:00:09 elapsed time, 0:00:08 cpu time, factor 0.88)
Building HOL ...
HOL: theory Code_Generator
HOL: theory HOL
HOL: theory Orderings
HOL: theory SAT
HOL: theory Groups
HOL: theory Rings
HOL: theory Lattices
HOL: theory Set
HOL: theory Complete_Lattices
HOL: theory Fun
HOL: theory Inductive
HOL: theory Fields
HOL: theory Typedef
HOL: theory Product_Type
HOL: theory Complete_Partial_Order
HOL: theory Sum_Type
HOL: theory Nat
HOL: theory Datatype
HOL: theory Meson
HOL: theory Num
HOL: theory ATP
HOL: theory Power
HOL: theory Metis
HOL: theory Option
HOL: theory Extraction
HOL: theory Finite_Set
HOL: theory Partial_Function
HOL: theory Relation
HOL: theory Transitive_Closure
HOL: theory Wellfounded
HOL: theory FunDef
HOL: theory Plain
HOL: theory Big_Operators
HOL: theory Hilbert_Choice
HOL: theory Equiv_Relations
HOL: theory Transfer
HOL: theory Lifting
HOL: theory Quotient
HOL: theory Int
HOL: theory Nat_Transfer
HOL: theory Divides
HOL: theory Set_Interval
HOL: theory Code_Numeral
HOL: theory Numeral_Simprocs
HOL: theory Semiring_Normalization
HOL: theory Groebner_Basis
HOL: theory Presburger
HOL: theory List
HOL: theory Map
HOL: theory Predicate
HOL: theory Enum
HOL: theory Lazy_Sequence
HOL: theory Random
HOL: theory DSequence
HOL: theory String
HOL: theory New_DSequence
HOL: theory Typerep
HOL: theory Code_Evaluation
HOL: theory Quickcheck
HOL: theory Quickcheck_Exhaustive
HOL: theory Random_Sequence
HOL: theory New_Random_Sequence
HOL: theory Quickcheck_Narrowing
HOL: theory Predicate_Compile
HOL: theory Record
HOL: theory SMT
HOL: theory Sledgehammer
HOL: theory Nitpick
HOL: theory Main
HOL: theory Archimedean_Field
HOL: theory Fact
HOL: theory Lubs
HOL: theory Parity
HOL: theory GCD
HOL: theory Rat
HOL: theory RealDef
HOL: theory RComplete
HOL: theory RealVector
HOL: theory SupInf
HOL: theory Limits
HOL: theory Real
HOL: theory SEQ
HOL: theory Lim
HOL: theory Deriv
HOL: theory Series
HOL: theory NthRoot
HOL: theory Transcendental
HOL: theory Complex
HOL: theory Ln
HOL: theory Log
HOL: theory MacLaurin
HOL: theory Taylor
HOL: theory Complex_Main
Timing HOL (2 threads, 114.860s elapsed time, 224.714s cpu time, 19.037s GC time, factor 1.96)
Finished HOL (0:02:20 elapsed time, 0:04:18 cpu time, factor 1.84)
Building HOL-Multivariate_Analysis ...
HOL-Multivariate_Analysis: theory Extended_Nat
HOL-Multivariate_Analysis: theory FuncSet
HOL-Multivariate_Analysis: theory Indicator_Function
HOL-Multivariate_Analysis: theory Infinite_Set
HOL-Multivariate_Analysis: theory Glbs
HOL-Multivariate_Analysis: theory Nat_Bijection
HOL-Multivariate_Analysis: theory L2_Norm
HOL-Multivariate_Analysis: theory Extended_Real
HOL-Multivariate_Analysis: theory Countable
HOL-Multivariate_Analysis: theory Countable_Set
HOL-Multivariate_Analysis: theory FrechetDeriv
HOL-Multivariate_Analysis: theory Inner_Product
HOL-Multivariate_Analysis: theory Sum_of_Squares
HOL-Multivariate_Analysis: theory Norm_Arith
HOL-Multivariate_Analysis: theory Permutations
HOL-Multivariate_Analysis: theory Phantom_Type
HOL-Multivariate_Analysis: theory Cardinality
HOL-Multivariate_Analysis: theory Product_plus
HOL-Multivariate_Analysis: theory Product_Vector
HOL-Multivariate_Analysis: theory Convex
HOL-Multivariate_Analysis: theory Euclidean_Space
HOL-Multivariate_Analysis: theory Numeral_Type
HOL-Multivariate_Analysis: theory Set_Algebras
HOL-Multivariate_Analysis: theory Finite_Cartesian_Product
HOL-Multivariate_Analysis: theory Linear_Algebra
HOL-Multivariate_Analysis: theory Operator_Norm
HOL-Multivariate_Analysis: theory Topology_Euclidean_Space
HOL-Multivariate_Analysis: theory Extended_Real_Limits
HOL-Multivariate_Analysis: theory Convex_Euclidean_Space
HOL-Multivariate_Analysis: theory Brouwer_Fixpoint
HOL-Multivariate_Analysis: theory Path_Connected
HOL-Multivariate_Analysis: theory Derivative
HOL-Multivariate_Analysis: theory Integration
HOL-Multivariate_Analysis: theory Cartesian_Euclidean_Space
HOL-Multivariate_Analysis: theory Determinants
HOL-Multivariate_Analysis: theory Fashoda
HOL-Multivariate_Analysis: theory Multivariate_Analysis
Timing HOL-Multivariate_Analysis (2 threads, 90.705s elapsed time, 181.242s cpu time, 6.457s GC time, factor 2.00)
Finished HOL-Multivariate_Analysis (0:01:47 elapsed time, 0:03:19 cpu time, factor 1.85)
Building HOL-Nominal ...
HOL-Nominal: theory Infinite_Set
HOL-Nominal: theory Nominal
Timing HOL-Nominal (2 threads, 4.642s elapsed time, 8.786s cpu time, 0.515s GC time, factor 1.89)
Finished HOL-Nominal (0:00:15 elapsed time, 0:00:18 cpu time, factor 1.20)
Building HOL-Proofs ...
HOL-Proofs: theory Code_Generator
HOL-Proofs: theory HOL
HOL-Proofs: theory Orderings
HOL-Proofs: theory SAT
HOL-Proofs: theory Groups
HOL-Proofs: theory Rings
HOL-Proofs: theory Lattices
HOL-Proofs: theory Set
HOL-Proofs: theory Complete_Lattices
HOL-Proofs: theory Fun
HOL-Proofs: theory Inductive
HOL-Proofs: theory Fields
HOL-Proofs: theory Typedef
HOL-Proofs: theory Product_Type
HOL-Proofs: theory Complete_Partial_Order
HOL-Proofs: theory Sum_Type
HOL-Proofs: theory Nat
HOL-Proofs: theory Datatype
HOL-Proofs: theory Meson
HOL-Proofs: theory Num
HOL-Proofs: theory ATP
HOL-Proofs: theory Metis
HOL-Proofs: theory Power
HOL-Proofs: theory Option
HOL-Proofs: theory Extraction
HOL-Proofs: theory Finite_Set
HOL-Proofs: theory Partial_Function
HOL-Proofs: theory Relation
HOL-Proofs: theory Transitive_Closure
HOL-Proofs: theory Wellfounded
HOL-Proofs: theory FunDef
HOL-Proofs: theory Plain
HOL-Proofs: theory Big_Operators
HOL-Proofs: theory Hilbert_Choice
HOL-Proofs: theory Equiv_Relations
HOL-Proofs: theory Transfer
HOL-Proofs: theory Lifting
HOL-Proofs: theory Quotient
HOL-Proofs: theory Int
HOL-Proofs: theory Nat_Transfer
HOL-Proofs: theory Divides
HOL-Proofs: theory Code_Numeral
HOL-Proofs: theory Numeral_Simprocs
HOL-Proofs: theory Semiring_Normalization
HOL-Proofs: theory Set_Interval
HOL-Proofs: theory Groebner_Basis
HOL-Proofs: theory Presburger
HOL-Proofs: theory List
HOL-Proofs: theory Map
HOL-Proofs: theory Enum
HOL-Proofs: theory Predicate
HOL-Proofs: theory Lazy_Sequence
HOL-Proofs: theory DSequence
HOL-Proofs: theory New_DSequence
HOL-Proofs: theory Random
HOL-Proofs: theory String
HOL-Proofs: theory Typerep
HOL-Proofs: theory Code_Evaluation
HOL-Proofs: theory Quickcheck
HOL-Proofs: theory Quickcheck_Exhaustive
HOL-Proofs: theory Random_Sequence
HOL-Proofs: theory New_Random_Sequence
HOL-Proofs: theory Quickcheck_Narrowing
HOL-Proofs: theory Predicate_Compile
HOL-Proofs: theory Record
HOL-Proofs: theory SMT
HOL-Proofs: theory Sledgehammer
HOL-Proofs: theory Nitpick
HOL-Proofs: theory Main
Timing HOL-Proofs (2 threads, 264.139s elapsed time, 520.268s cpu time, 45.590s GC time, factor 1.97)
Finished HOL-Proofs (0:05:01 elapsed time, 0:09:31 cpu time, factor 1.89)
Building ZF ...
ZF: theory IFOL
ZF: theory FOL
ZF: theory ZF
ZF: theory upair
ZF: theory pair
ZF: theory Bool
ZF: theory equalities
ZF: theory Fixedpt
ZF: theory Sum
ZF: theory func
ZF: theory Perm
ZF: theory QPair
ZF: theory Trancl
ZF: theory EquivClass
ZF: theory WF
ZF: theory Order
ZF: theory Ordinal
ZF: theory OrdQuant
ZF: theory OrderArith
ZF: theory Nat_ZF
ZF: theory Epsilon
ZF: theory OrderType
ZF: theory Inductive_ZF
ZF: theory Finite
ZF: theory Cardinal
ZF: theory Univ
ZF: theory Arith
ZF: theory QUniv
ZF: theory Datatype_ZF
ZF: theory ArithSimp
ZF: theory Int_ZF
ZF: theory CardinalArith
ZF: theory List_ZF
ZF: theory Bin
ZF: theory IntArith
ZF: theory IntDiv_ZF
ZF: theory Main_ZF
ZF: theory AC
ZF: theory Main
ZF: theory Zorn
ZF: theory Cardinal_AC
ZF: theory InfDatatype
ZF: theory Main_ZFC
Timing ZF (2 threads, 15.462s elapsed time, 29.251s cpu time, 2.666s GC time, factor 1.89)
Finished ZF (0:00:19 elapsed time, 0:00:32 cpu time, factor 1.68)
Running HOL-Nominal-Examples ...
HOL-Nominal-Examples: theory CK_Machine
HOL-Nominal-Examples: theory CR_Takahashi
HOL-Nominal-Examples: theory Class1
HOL-Nominal-Examples: theory Compile
HOL-Nominal-Examples: theory Contexts
HOL-Nominal-Examples: theory Crary
HOL-Nominal-Examples: theory Fsub
HOL-Nominal-Examples: theory Height
HOL-Nominal-Examples: theory Lam_Funs
HOL-Nominal-Examples: theory CR
HOL-Nominal-Examples: theory SN
HOL-Nominal-Examples: theory Lambda_mu
HOL-Nominal-Examples: theory LocalWeakening
HOL-Nominal-Examples: theory Pattern
HOL-Nominal-Examples: theory SOS
HOL-Nominal-Examples: theory Class2
HOL-Nominal-Examples: theory Standardization
HOL-Nominal-Examples: theory Class3
HOL-Nominal-Examples: theory Support
HOL-Nominal-Examples: theory Type_Preservation
HOL-Nominal-Examples: theory W
HOL-Nominal-Examples: theory Weakening
HOL-Nominal-Examples: theory Nominal_Examples
HOL-Nominal-Examples: theory VC_Condition
Timing HOL-Nominal-Examples (2 threads, 273.794s elapsed time, 543.758s cpu time, 32.324s GC time, factor 1.99)
Finished HOL-Nominal-Examples (0:04:36 elapsed time, 0:09:05 cpu time, factor 1.97)
Running HOL-Auth ...
HOL-Auth: theory Message
HOL-Auth: theory Nat_Bijection
HOL-Auth: theory All_Symmetric
HOL-Auth: theory Event
HOL-Auth: theory EventSC
HOL-Auth: theory Extensions
HOL-Auth: theory Public
HOL-Auth: theory Analz
HOL-Auth: theory Guard
HOL-Auth: theory GuardK
HOL-Auth: theory List_Msg
HOL-Auth: theory CertifiedEmail
HOL-Auth: theory Guard_Public
HOL-Auth: theory Guard_NS_Public
HOL-Auth: theory Proto
HOL-Auth: theory P2
HOL-Auth: theory KerberosIV
HOL-Auth: theory KerberosIV_Gets
HOL-Auth: theory KerberosV
HOL-Auth: theory Kerberos_BAN
HOL-Auth: theory Kerberos_BAN_Gets
HOL-Auth: theory NS_Public
HOL-Auth: theory NS_Public_Bad
HOL-Auth: theory NS_Shared
HOL-Auth: theory OtwayRees
HOL-Auth: theory OtwayReesBella
HOL-Auth: theory OtwayRees_AN
HOL-Auth: theory OtwayRees_Bad
HOL-Auth: theory P1
HOL-Auth: theory Recur
HOL-Auth: theory WooLam
HOL-Auth: theory Yahalom
HOL-Auth: theory Yahalom2
HOL-Auth: theory Yahalom_Bad
HOL-Auth: theory ZhouGollmann
HOL-Auth: theory Auth_Shared
HOL-Auth: theory Auth_Guard_Public
HOL-Auth: theory Shared
HOL-Auth: theory Guard_Shared
HOL-Auth: theory Smartcard
HOL-Auth: theory Guard_OtwayRees
HOL-Auth: theory Guard_Yahalom
HOL-Auth: theory ShoupRubin
HOL-Auth: theory Auth_Guard_Shared
HOL-Auth: theory ShoupRubinBella
HOL-Auth: theory TLS
HOL-Auth: theory Auth_Smartcard
HOL-Auth: theory Auth_Public
Timing HOL-Auth (2 threads, 116.758s elapsed time, 231.877s cpu time, 8.854s GC time, factor 1.99)
Finished HOL-Auth (0:01:58 elapsed time, 0:03:52 cpu time, factor 1.96)
Running HOL-Bali ...
HOL-Bali: theory Wfrec
HOL-Bali: theory Old_Recdef
HOL-Bali: theory Basis
HOL-Bali: theory Name
HOL-Bali: theory Table
HOL-Bali: theory Type
HOL-Bali: theory Value
HOL-Bali: theory Term
HOL-Bali: theory Decl
HOL-Bali: theory TypeRel
HOL-Bali: theory DeclConcepts
HOL-Bali: theory State
HOL-Bali: theory WellType
HOL-Bali: theory Conform
HOL-Bali: theory Eval
HOL-Bali: theory DefiniteAssignment
HOL-Bali: theory WellForm
HOL-Bali: theory DefiniteAssignmentCorrect
HOL-Bali: theory Example
HOL-Bali: theory TypeSafe
HOL-Bali: theory Evaln
HOL-Bali: theory AxSem
HOL-Bali: theory Trans
HOL-Bali: theory AxCompl
HOL-Bali: theory AxSound
HOL-Bali: theory AxExample
Timing HOL-Bali (2 threads, 77.600s elapsed time, 146.954s cpu time, 5.984s GC time, factor 1.89)
Finished HOL-Bali (0:01:19 elapsed time, 0:02:27 cpu time, factor 1.86)
Running HOL-Decision_Procs ...
HOL-Decision_Procs: theory Code_Binary_Nat
HOL-Decision_Procs: theory Code_Natural
HOL-Decision_Procs: theory Code_Integer
HOL-Decision_Procs: theory DP_Library
HOL-Decision_Procs: theory Dense_Linear_Order
HOL-Decision_Procs: theory Efficient_Nat
HOL-Decision_Procs: theory Commutative_Ring
HOL-Decision_Procs: theory Dense_Linear_Order_Ex
HOL-Decision_Procs: theory Abstract_Rat
HOL-Decision_Procs: theory Lattice_Algebras
HOL-Decision_Procs: theory Commutative_Ring_Complete
HOL-Decision_Procs: theory Commutative_Ring_Ex
HOL-Decision_Procs: theory Polynomial_List
HOL-Decision_Procs: theory Reflected_Multivariate_Polynomial
HOL-Decision_Procs: theory Float
HOL-Decision_Procs: theory Reflection
HOL-Decision_Procs: theory Approximation
HOL-Decision_Procs: theory Wfrec
HOL-Decision_Procs: theory Old_Recdef
HOL-Decision_Procs: theory Cooper
HOL-Decision_Procs: theory Approximation_Ex
HOL-Decision_Procs: theory Ferrack
HOL-Decision_Procs: theory MIR
HOL-Decision_Procs: theory Parametric_Ferrante_Rackoff
HOL-Decision_Procs: theory Decision_Procs
Timing HOL-Decision_Procs (2 threads, 216.082s elapsed time, 429.601s cpu time, 24.976s GC time, factor 1.99)
Finished HOL-Decision_Procs (0:03:38 elapsed time, 0:07:10 cpu time, factor 1.97)
Running HOL-Hoare_Parallel ...
HOL-Hoare_Parallel: theory Graph
HOL-Hoare_Parallel: theory OG_Com
HOL-Hoare_Parallel: theory Quote_Antiquote
HOL-Hoare_Parallel: theory RG_Com
HOL-Hoare_Parallel: theory RG_Tran
HOL-Hoare_Parallel: theory RG_Hoare
HOL-Hoare_Parallel: theory OG_Tran
HOL-Hoare_Parallel: theory RG_Syntax
HOL-Hoare_Parallel: theory RG_Examples
HOL-Hoare_Parallel: theory OG_Hoare
HOL-Hoare_Parallel: theory OG_Tactics
HOL-Hoare_Parallel: theory OG_Syntax
HOL-Hoare_Parallel: theory Gar_Coll
HOL-Hoare_Parallel: theory Mul_Gar_Coll
HOL-Hoare_Parallel: theory OG_Examples
HOL-Hoare_Parallel: theory Hoare_Parallel
Timing HOL-Hoare_Parallel (2 threads, 111.285s elapsed time, 219.664s cpu time, 3.917s GC time, factor 1.97)
Finished HOL-Hoare_Parallel (0:01:53 elapsed time, 0:03:40 cpu time, factor 1.94)
Running HOL-IMP ...
HOL-IMP: theory Char_nat
HOL-IMP: theory List_lexord
HOL-IMP: theory While_Combinator
HOL-IMP: theory Char_ord
HOL-IMP: theory Interpretation_with_Defs
HOL-IMP: theory AExp
HOL-IMP: theory C_like
HOL-IMP: theory Complete_Lattice
HOL-IMP: theory Complete_Lattice_ix
HOL-IMP: theory OO
HOL-IMP: theory ASM
HOL-IMP: theory BExp
HOL-IMP: theory Com
HOL-IMP: theory ACom
HOL-IMP: theory ACom_ITP
HOL-IMP: theory Abs_Int_Tests
HOL-IMP: theory Big_Step
HOL-IMP: theory Procs
HOL-IMP: theory Procs_Dyn_Vars_Dyn
HOL-IMP: theory Compiler
HOL-IMP: theory Denotation
HOL-IMP: theory Hoare
HOL-IMP: theory Hoare_Examples
HOL-IMP: theory Hoare_Sound_Complete
HOL-IMP: theory HoareT
HOL-IMP: theory VC
HOL-IMP: theory Sec_Type_Expr
HOL-IMP: theory Sec_Typing
HOL-IMP: theory Sec_TypingT
HOL-IMP: theory Sem_Equiv
HOL-IMP: theory Fold
HOL-IMP: theory Procs_Stat_Vars_Dyn
HOL-IMP: theory Comp_Rev
HOL-IMP: theory Procs_Stat_Vars_Stat
HOL-IMP: theory Vars
HOL-IMP: theory Def_Init
HOL-IMP: theory Def_Init_Exp
HOL-IMP: theory Live
HOL-IMP: theory Def_Init_Big
HOL-IMP: theory Def_Init_Sound_Big
HOL-IMP: theory Collecting
HOL-IMP: theory Collecting_ITP
HOL-IMP: theory Collecting1
HOL-IMP: theory Collecting_Examples
HOL-IMP: theory Star
HOL-IMP: theory Def_Init_Small
HOL-IMP: theory Def_Init_Sound_Small
HOL-IMP: theory Small_Step
HOL-IMP: theory Finite_Reachable
HOL-IMP: theory Types
HOL-IMP: theory Live_True
HOL-IMP: theory Abs_Int0_ITP
HOL-IMP: theory Poly_Types
HOL-IMP: theory Abs_Int_den0_fun
HOL-IMP: theory Abs_State_den
HOL-IMP: theory Abs_State_ITP
HOL-IMP: theory Abs_Int_den0
HOL-IMP: theory Abs_Int_den0_const
HOL-IMP: theory Abs_Int1_ITP
HOL-IMP: theory Abs_Int1_const_ITP
HOL-IMP: theory Abs_Int1_parity_ITP
HOL-IMP: theory Abs_Int2_ITP
HOL-IMP: theory Abs_Int_den1
HOL-IMP: theory Abs_Int2_ivl_ITP
HOL-IMP: theory Abs_Int_den1_ivl
HOL-IMP: theory Abs_Int_den2
HOL-IMP: theory Abs_Int_init
HOL-IMP: theory Abs_Int0
HOL-IMP: theory Abs_Int3_ITP
HOL-IMP: theory Abs_State
HOL-IMP: theory Abs_Int1
HOL-IMP: theory Abs_Int1_const
HOL-IMP: theory Abs_Int1_parity
HOL-IMP: theory Abs_Int2
HOL-IMP: theory Abs_Int2_ivl
HOL-IMP: theory Abs_Int3
Timing HOL-IMP (2 threads, 237.657s elapsed time, 469.633s cpu time, 44.537s GC time, factor 1.98)
Finished HOL-IMP (0:03:59 elapsed time, 0:07:51 cpu time, factor 1.97)
Running HOL-Library ...
HOL-Library: theory Adhoc_Overloading
HOL-Library: theory Lattice_Syntax
HOL-Library: theory Preorder
HOL-Library: theory Refute
HOL-Library: theory AList
HOL-Library: theory Bit
HOL-Library: theory Boolean_Algebra
HOL-Library: theory DAList
HOL-Library: theory Char_nat
HOL-Library: theory Char_ord
HOL-Library: theory Code_Binary_Nat
HOL-Library: theory Code_Char
HOL-Library: theory Code_Char_ord
HOL-Library: theory Code_Natural
HOL-Library: theory Code_Integer
HOL-Library: theory Code_Char_chr
HOL-Library: theory Code_Numeral_Types
HOL-Library: theory Continuity
HOL-Library: theory Debug
HOL-Library: theory Dlist
HOL-Library: theory Efficient_Nat
HOL-Library: theory IArray
HOL-Library: theory Code_Target_Int
HOL-Library: theory Code_Target_Nat
HOL-Library: theory Code_Target_Numeral
HOL-Library: theory Eval_Witness
HOL-Library: theory Extended_Nat
HOL-Library: theory Fraction_Field
HOL-Library: theory FuncSet
HOL-Library: theory Function_Algebras
HOL-Library: theory Function_Division
HOL-Library: theory Indicator_Function
HOL-Library: theory Infinite_Set
HOL-Library: theory Kleene_Algebra
HOL-Library: theory LaTeXsugar
HOL-Library: theory ListVector
HOL-Library: theory List_lexord
HOL-Library: theory Monad_Syntax
HOL-Library: theory Multiset
HOL-Library: theory Option_ord
HOL-Library: theory Order_Relation
HOL-Library: theory Zorn
HOL-Library: theory Parallel
HOL-Library: theory Diagonal_Subsequence
HOL-Library: theory Nat_Bijection
HOL-Library: theory Abstract_Rat
HOL-Library: theory Binomial
HOL-Library: theory Countable
HOL-Library: theory Code_Real_Approx_By_Float
HOL-Library: theory Countable_Set
HOL-Library: theory ContNotDenum
HOL-Library: theory Formal_Power_Series
HOL-Library: theory FrechetDeriv
HOL-Library: theory Inner_Product
HOL-Library: theory Lattice_Algebras
HOL-Library: theory OptionalSugar
HOL-Library: theory Sum_of_Squares
HOL-Library: theory Float
HOL-Library: theory Permutations
HOL-Library: theory Permutation
HOL-Library: theory Phantom_Type
HOL-Library: theory Polynomial
HOL-Library: theory Cardinality
HOL-Library: theory FinFun
HOL-Library: theory Numeral_Type
HOL-Library: theory Type_Length
HOL-Library: theory Fundamental_Theorem_Algebra
HOL-Library: theory Poly_Deriv
HOL-Library: theory Product_plus
HOL-Library: theory Product_Lattice
HOL-Library: theory Product_Vector
HOL-Library: theory Finite_Lattice
HOL-Library: theory Convex
HOL-Library: theory Quotient_Syntax
HOL-Library: theory Quotient_Option
HOL-Library: theory Mapping
HOL-Library: theory Quotient_Product
HOL-Library: theory Quotient_Set
HOL-Library: theory AList_Mapping
HOL-Library: theory Quotient_List
HOL-Library: theory Quotient_Sum
HOL-Library: theory Quotient_Type
HOL-Library: theory RBT_Impl
HOL-Library: theory Ramsey
HOL-Library: theory Reflection
HOL-Library: theory Saturated
HOL-Library: theory Set_Algebras
HOL-Library: theory BigO
HOL-Library: theory State_Monad
HOL-Library: theory Sublist
HOL-Library: theory Sublist_Order
HOL-Library: theory Transitive_Closure_Table
HOL-Library: theory Univ_Poly
HOL-Library: theory Wfrec
HOL-Library: theory Old_Recdef
HOL-Library: theory While_Combinator
HOL-Library: theory RBT
HOL-Library: theory RBT_Mapping
HOL-Library: theory Library
Skipping theories "Sum_of_Squares_Remote" (undefined ISABELLE_FULL_TEST)
Timing HOL-Library (2 threads, 117.786s elapsed time, 232.049s cpu time, 15.031s GC time, factor 1.97)
Finished HOL-Library (0:01:59 elapsed time, 0:03:53 cpu time, factor 1.95)
Running HOL-MicroJava ...
HOL-MicroJava: theory While_Combinator
HOL-MicroJava: theory Transitive_Closure_Table
HOL-MicroJava: theory Wfrec
HOL-MicroJava: theory Semilat
HOL-MicroJava: theory Err
HOL-MicroJava: theory JBasis
HOL-MicroJava: theory Listn
HOL-MicroJava: theory AuxLemmas
HOL-MicroJava: theory Type
HOL-MicroJava: theory Typing_Framework
HOL-MicroJava: theory Opt
HOL-MicroJava: theory Product
HOL-MicroJava: theory SemilatAlg
HOL-MicroJava: theory Kildall
HOL-MicroJava: theory LBVSpec
HOL-MicroJava: theory Decl
HOL-MicroJava: theory Value
HOL-MicroJava: theory SystemClasses
HOL-MicroJava: theory TypeRel
HOL-MicroJava: theory Term
HOL-MicroJava: theory State
HOL-MicroJava: theory Exceptions
HOL-MicroJava: theory WellForm
HOL-MicroJava: theory LBVComplete
HOL-MicroJava: theory WellType
HOL-MicroJava: theory LBVCorrect
HOL-MicroJava: theory Typing_Framework_err
HOL-MicroJava: theory Abstract_BV
HOL-MicroJava: theory Conform
HOL-MicroJava: theory Eval
HOL-MicroJava: theory JVMState
HOL-MicroJava: theory JVMInstructions
HOL-MicroJava: theory JVMExceptions
HOL-MicroJava: theory JVMExecInstr
HOL-MicroJava: theory JVMExec
HOL-MicroJava: theory DefsComp
HOL-MicroJava: theory Index
HOL-MicroJava: theory JVMDefensive
HOL-MicroJava: theory JVMListExample
HOL-MicroJava: theory Example
HOL-MicroJava: theory JListExample
HOL-MicroJava: theory JTypeSafe
HOL-MicroJava: theory TypeInf
HOL-MicroJava: theory Semilattices
HOL-MicroJava: theory JType
HOL-MicroJava: theory JVMType
HOL-MicroJava: theory Effect
HOL-MicroJava: theory TranslCompTp
HOL-MicroJava: theory TranslComp
HOL-MicroJava: theory LemmasComp
HOL-MicroJava: theory CorrComp
HOL-MicroJava: theory BVSpec
HOL-MicroJava: theory EffectMono
HOL-MicroJava: theory Altern
HOL-MicroJava: theory Correct
HOL-MicroJava: theory Typing_Framework_JVM
HOL-MicroJava: theory BVSpecTypeSafe
HOL-MicroJava: theory JVM
HOL-MicroJava: theory CorrCompTp
HOL-MicroJava: theory BVNoTypeError
HOL-MicroJava: theory BVExample
HOL-MicroJava: theory LBVJVM
HOL-MicroJava: theory MicroJava
Timing HOL-MicroJava (2 threads, 111.353s elapsed time, 221.872s cpu time, 8.033s GC time, factor 1.99)
Finished HOL-MicroJava (0:01:53 elapsed time, 0:03:42 cpu time, factor 1.96)
Running HOL-Probability ...
HOL-Probability: theory AList
HOL-Probability: theory DAList
HOL-Probability: theory Multiset
HOL-Probability: theory Permutation
HOL-Probability: theory Diagonal_Subsequence
HOL-Probability: theory Sigma_Algebra
HOL-Probability: theory Discrete_Topology
HOL-Probability: theory Measurable
HOL-Probability: theory Measure_Space
HOL-Probability: theory Borel_Space
HOL-Probability: theory Caratheodory
HOL-Probability: theory Lebesgue_Integration
HOL-Probability: theory Regularity
HOL-Probability: theory Binary_Product_Measure
HOL-Probability: theory Complete_Measure
HOL-Probability: theory Radon_Nikodym
HOL-Probability: theory Finite_Product_Measure
HOL-Probability: theory Fin_Map
HOL-Probability: theory Lebesgue_Measure
HOL-Probability: theory Probability_Measure
HOL-Probability: theory Distributions
HOL-Probability: theory Projective_Family
HOL-Probability: theory Infinite_Product_Measure
HOL-Probability: theory Independent_Family
HOL-Probability: theory Projective_Limit
HOL-Probability: theory Information
HOL-Probability: theory Dining_Cryptographers
HOL-Probability: theory Koepf_Duermuth_Countermeasure
HOL-Probability: theory Probability
Timing HOL-Probability (2 threads, 81.298s elapsed time, 162.591s cpu time, 5.089s GC time, factor 2.00)
Finished HOL-Probability (0:01:24 elapsed time, 0:02:44 cpu time, factor 1.95)
Running HOL-Proofs-Extraction ...
HOL-Proofs-Extraction: theory Adhoc_Overloading
HOL-Proofs-Extraction: theory AList
HOL-Proofs-Extraction: theory Code_Binary_Nat
HOL-Proofs-Extraction: theory Code_Natural
HOL-Proofs-Extraction: theory Code_Integer
HOL-Proofs-Extraction: theory Efficient_Nat
HOL-Proofs-Extraction: theory Fact
HOL-Proofs-Extraction: theory Monad_Syntax
HOL-Proofs-Extraction: theory DAList
HOL-Proofs-Extraction: theory Parity
HOL-Proofs-Extraction: theory Multiset
HOL-Proofs-Extraction: theory State_Monad
HOL-Proofs-Extraction: theory GCD
HOL-Proofs-Extraction: theory Primes
HOL-Proofs-Extraction: theory Cong
HOL-Proofs-Extraction: theory UniqueFactorization
HOL-Proofs-Extraction: theory Higman
HOL-Proofs-Extraction: theory Util
HOL-Proofs-Extraction: theory Euclid
HOL-Proofs-Extraction: theory Higman_Extraction
HOL-Proofs-Extraction: theory Pigeonhole
HOL-Proofs-Extraction: theory QuotRem
HOL-Proofs-Extraction: theory Greatest_Common_Divisor
HOL-Proofs-Extraction: theory Warshall
Timing HOL-Proofs-Extraction (2 threads, 181.168s elapsed time, 349.644s cpu time, 23.006s GC time, factor 1.93)
Finished HOL-Proofs-Extraction (0:03:03 elapsed time, 0:05:51 cpu time, factor 1.91)
Running HOL-SET_Protocol ...
HOL-SET_Protocol: theory Nat_Bijection
HOL-SET_Protocol: theory Message_SET
HOL-SET_Protocol: theory Event_SET
HOL-SET_Protocol: theory Public_SET
HOL-SET_Protocol: theory Cardholder_Registration
HOL-SET_Protocol: theory Merchant_Registration
HOL-SET_Protocol: theory Purchase
HOL-SET_Protocol: theory SET_Protocol
Timing HOL-SET_Protocol (2 threads, 36.425s elapsed time, 70.277s cpu time, 1.328s GC time, factor 1.93)
Finished HOL-SET_Protocol (0:00:38 elapsed time, 0:01:11 cpu time, factor 1.86)
Running HOL-UNITY ...
HOL-UNITY: theory Message
HOL-UNITY: theory Event
HOL-UNITY: theory Public
HOL-UNITY: theory AList
HOL-UNITY: theory ListOrder
HOL-UNITY: theory UNITY
HOL-UNITY: theory Constrains
HOL-UNITY: theory DAList
HOL-UNITY: theory Deadlock
HOL-UNITY: theory FP
HOL-UNITY: theory Network
HOL-UNITY: theory WFair
HOL-UNITY: theory Multiset
HOL-UNITY: theory SubstAx
HOL-UNITY: theory Detects
HOL-UNITY: theory Union
HOL-UNITY: theory Comp
HOL-UNITY: theory Guar
HOL-UNITY: theory Extend
HOL-UNITY: theory Follows
HOL-UNITY: theory Transformers
HOL-UNITY: theory Project
HOL-UNITY: theory Rename
HOL-UNITY: theory ELT
HOL-UNITY: theory Lift_prog
HOL-UNITY: theory PPROD
HOL-UNITY: theory ProgressSets
HOL-UNITY: theory Token
HOL-UNITY: theory UNITY_Main
HOL-UNITY: theory AllocBase
HOL-UNITY: theory Channel
HOL-UNITY: theory Alloc
HOL-UNITY: theory AllocImpl
HOL-UNITY: theory Client
HOL-UNITY: theory Common
HOL-UNITY: theory Counter
HOL-UNITY: theory Counterc
HOL-UNITY: theory Handshake
HOL-UNITY: theory Lift
HOL-UNITY: theory Mutex
HOL-UNITY: theory NSP_Bad
HOL-UNITY: theory PriorityAux
HOL-UNITY: theory Priority
HOL-UNITY: theory Progress
HOL-UNITY: theory Reach
HOL-UNITY: theory TimerArray
HOL-UNITY: theory Reachability
Timing HOL-UNITY (2 threads, 36.244s elapsed time, 71.480s cpu time, 3.340s GC time, factor 1.97)
Finished HOL-UNITY (0:00:38 elapsed time, 0:01:12 cpu time, factor 1.89)
Running ZF-UNITY ...
ZF-UNITY: theory Acc
ZF-UNITY: theory FoldSet
ZF-UNITY: theory GenPrefix
ZF-UNITY: theory Multiset
ZF-UNITY: theory State
ZF-UNITY: theory UNITY
ZF-UNITY: theory Constrains
ZF-UNITY: theory MultisetSum
ZF-UNITY: theory Monotonicity
ZF-UNITY: theory FP
ZF-UNITY: theory Increasing
ZF-UNITY: theory WFair
ZF-UNITY: theory SubstAx
ZF-UNITY: theory Follows
ZF-UNITY: theory Mutex
ZF-UNITY: theory Union
ZF-UNITY: theory Comp
ZF-UNITY: theory Guar
ZF-UNITY: theory AllocBase
ZF-UNITY: theory ClientImpl
ZF-UNITY: theory Distributor
ZF-UNITY: theory Merge
ZF-UNITY: theory AllocImpl
Timing ZF-UNITY (2 threads, 15.590s elapsed time, 31.136s cpu time, 1.101s GC time, factor 2.00)
Finished ZF-UNITY (0:00:16 elapsed time, 0:00:31 cpu time, factor 1.93)
Finished at Mon Feb 4 19:27:27 CET 2013
0:37:22 elapsed time, 1:12:11 cpu time, factor 1.93
*** m=3 q=2 ***
Started at Mon Feb 4 19:27:27 CET 2013 (polyml-5.5.0_x86-darwin on lri29-163.lri.fr)
ISABELLE_BUILD_OPTIONS="threads_trace=2 threads=3 parallel_proofs=2"
ML_PLATFORM="x86-darwin"
ML_HOME="/Volumes/Macintosh_HD/Users/makarius/.isabelle/contrib/polyml-5.5.0-3/x86-darwin"
ML_SYSTEM="polyml-5.5.0"
ML_OPTIONS="--minheap 1000 --gcthreads 3"
Session Pure
Session HOL (main)
Session HOL-Auth
Session HOL-Bali
Session HOL-Decision_Procs
Session HOL-Hoare_Parallel
Session HOL-IMP
Session HOL-Library (main)
Session HOL-MicroJava
Session HOL-Multivariate_Analysis (main)
Session HOL-Probability
Session HOL-Nominal (main)
Session HOL-Nominal-Examples
Session HOL-SET_Protocol
Session HOL-UNITY
Session HOL-Proofs
Session HOL-Proofs-Extraction
Session ZF (main)
Session ZF-UNITY
Building Pure ...
Finished Pure (0:00:08 elapsed time, 0:00:08 cpu time, factor 1.00)
Building HOL ...
HOL: theory Code_Generator
HOL: theory HOL
HOL: theory Orderings
HOL: theory SAT
HOL: theory Groups
HOL: theory Rings
HOL: theory Lattices
HOL: theory Set
HOL: theory Complete_Lattices
HOL: theory Typedef
HOL: theory Fun
HOL: theory Inductive
HOL: theory Fields
HOL: theory Product_Type
HOL: theory Sum_Type
HOL: theory Complete_Partial_Order
HOL: theory Nat
HOL: theory Datatype
HOL: theory Meson
HOL: theory Num
HOL: theory Option
HOL: theory Extraction
HOL: theory ATP
HOL: theory Partial_Function
HOL: theory Power
HOL: theory Metis
HOL: theory Finite_Set
HOL: theory Relation
HOL: theory Transitive_Closure
HOL: theory Wellfounded
HOL: theory FunDef
HOL: theory Plain
HOL: theory Big_Operators
HOL: theory Hilbert_Choice
HOL: theory Equiv_Relations
HOL: theory Transfer
HOL: theory Lifting
HOL: theory Quotient
HOL: theory Int
HOL: theory Nat_Transfer
HOL: theory Divides
HOL: theory Set_Interval
HOL: theory Code_Numeral
HOL: theory Numeral_Simprocs
HOL: theory Semiring_Normalization
HOL: theory Groebner_Basis
HOL: theory Presburger
HOL: theory List
HOL: theory Map
HOL: theory Predicate
HOL: theory Random
HOL: theory Enum
HOL: theory Lazy_Sequence
HOL: theory String
HOL: theory DSequence
HOL: theory New_DSequence
HOL: theory Typerep
HOL: theory Code_Evaluation
HOL: theory Quickcheck
HOL: theory Quickcheck_Exhaustive
HOL: theory Random_Sequence
HOL: theory New_Random_Sequence
HOL: theory Quickcheck_Narrowing
HOL: theory Predicate_Compile
HOL: theory Record
HOL: theory SMT
HOL: theory Sledgehammer
HOL: theory Nitpick
HOL: theory Main
HOL: theory Archimedean_Field
HOL: theory Fact
HOL: theory Lubs
HOL: theory Parity
HOL: theory GCD
HOL: theory Rat
HOL: theory RealDef
HOL: theory RComplete
HOL: theory RealVector
HOL: theory SupInf
HOL: theory Limits
HOL: theory Real
HOL: theory SEQ
HOL: theory Lim
HOL: theory Deriv
HOL: theory Series
HOL: theory NthRoot
HOL: theory Transcendental
HOL: theory Complex
HOL: theory Ln
HOL: theory Log
HOL: theory MacLaurin
HOL: theory Taylor
HOL: theory Complex_Main
Timing HOL (3 threads, 91.848s elapsed time, 221.935s cpu time, 14.278s GC time, factor 2.42)
Finished HOL (0:01:55 elapsed time, 0:04:18 cpu time, factor 2.24)
Building HOL-Multivariate_Analysis ...
HOL-Multivariate_Analysis: theory Extended_Nat
HOL-Multivariate_Analysis: theory FuncSet
HOL-Multivariate_Analysis: theory Indicator_Function
HOL-Multivariate_Analysis: theory Infinite_Set
HOL-Multivariate_Analysis: theory Glbs
HOL-Multivariate_Analysis: theory Nat_Bijection
HOL-Multivariate_Analysis: theory L2_Norm
HOL-Multivariate_Analysis: theory FrechetDeriv
HOL-Multivariate_Analysis: theory Extended_Real
HOL-Multivariate_Analysis: theory Inner_Product
HOL-Multivariate_Analysis: theory Countable
HOL-Multivariate_Analysis: theory Sum_of_Squares
HOL-Multivariate_Analysis: theory Countable_Set
HOL-Multivariate_Analysis: theory Permutations
HOL-Multivariate_Analysis: theory Phantom_Type
HOL-Multivariate_Analysis: theory Cardinality
HOL-Multivariate_Analysis: theory Norm_Arith
HOL-Multivariate_Analysis: theory Product_plus
HOL-Multivariate_Analysis: theory Product_Vector
HOL-Multivariate_Analysis: theory Numeral_Type
HOL-Multivariate_Analysis: theory Convex
HOL-Multivariate_Analysis: theory Euclidean_Space
HOL-Multivariate_Analysis: theory Set_Algebras
HOL-Multivariate_Analysis: theory Finite_Cartesian_Product
HOL-Multivariate_Analysis: theory Linear_Algebra
HOL-Multivariate_Analysis: theory Operator_Norm
HOL-Multivariate_Analysis: theory Topology_Euclidean_Space
HOL-Multivariate_Analysis: theory Extended_Real_Limits
HOL-Multivariate_Analysis: theory Convex_Euclidean_Space
HOL-Multivariate_Analysis: theory Brouwer_Fixpoint
HOL-Multivariate_Analysis: theory Path_Connected
HOL-Multivariate_Analysis: theory Derivative
HOL-Multivariate_Analysis: theory Integration
HOL-Multivariate_Analysis: theory Cartesian_Euclidean_Space
HOL-Multivariate_Analysis: theory Determinants
HOL-Multivariate_Analysis: theory Fashoda
HOL-Multivariate_Analysis: theory Multivariate_Analysis
Timing HOL-Multivariate_Analysis (3 threads, 61.249s elapsed time, 181.955s cpu time, 6.706s GC time, factor 2.97)
Finished HOL-Multivariate_Analysis (0:01:17 elapsed time, 0:03:21 cpu time, factor 2.61)
Building HOL-Nominal ...
HOL-Nominal: theory Infinite_Set
HOL-Nominal: theory Nominal
Timing HOL-Nominal (3 threads, 4.362s elapsed time, 8.837s cpu time, 0.378s GC time, factor 2.03)
Finished HOL-Nominal (0:00:14 elapsed time, 0:00:19 cpu time, factor 1.35)
Building HOL-Proofs ...
HOL-Proofs: theory Code_Generator
HOL-Proofs: theory HOL
HOL-Proofs: theory Orderings
HOL-Proofs: theory SAT
HOL-Proofs: theory Groups
HOL-Proofs: theory Rings
HOL-Proofs: theory Lattices
HOL-Proofs: theory Set
HOL-Proofs: theory Complete_Lattices
HOL-Proofs: theory Typedef
HOL-Proofs: theory Fun
HOL-Proofs: theory Inductive
HOL-Proofs: theory Fields
HOL-Proofs: theory Product_Type
HOL-Proofs: theory Sum_Type
HOL-Proofs: theory Complete_Partial_Order
HOL-Proofs: theory Nat
HOL-Proofs: theory Datatype
HOL-Proofs: theory Meson
HOL-Proofs: theory Num
HOL-Proofs: theory Option
HOL-Proofs: theory ATP
HOL-Proofs: theory Extraction
HOL-Proofs: theory Partial_Function
HOL-Proofs: theory Metis
HOL-Proofs: theory Power
HOL-Proofs: theory Finite_Set
HOL-Proofs: theory Relation
HOL-Proofs: theory Transitive_Closure
HOL-Proofs: theory Wellfounded
HOL-Proofs: theory FunDef
HOL-Proofs: theory Plain
HOL-Proofs: theory Big_Operators
HOL-Proofs: theory Hilbert_Choice
HOL-Proofs: theory Equiv_Relations
HOL-Proofs: theory Transfer
HOL-Proofs: theory Lifting
HOL-Proofs: theory Quotient
HOL-Proofs: theory Int
HOL-Proofs: theory Nat_Transfer
HOL-Proofs: theory Divides
HOL-Proofs: theory Set_Interval
HOL-Proofs: theory Code_Numeral
HOL-Proofs: theory Numeral_Simprocs
HOL-Proofs: theory Semiring_Normalization
HOL-Proofs: theory Groebner_Basis
HOL-Proofs: theory Presburger
HOL-Proofs: theory List
HOL-Proofs: theory Map
HOL-Proofs: theory Enum
HOL-Proofs: theory Predicate
HOL-Proofs: theory Random
HOL-Proofs: theory String
HOL-Proofs: theory Lazy_Sequence
HOL-Proofs: theory DSequence
HOL-Proofs: theory New_DSequence
HOL-Proofs: theory Typerep
HOL-Proofs: theory Code_Evaluation
HOL-Proofs: theory Quickcheck
HOL-Proofs: theory Quickcheck_Exhaustive
HOL-Proofs: theory Random_Sequence
HOL-Proofs: theory New_Random_Sequence
HOL-Proofs: theory Quickcheck_Narrowing
HOL-Proofs: theory Predicate_Compile
HOL-Proofs: theory Record
HOL-Proofs: theory SMT
HOL-Proofs: theory Sledgehammer
HOL-Proofs: theory Nitpick
HOL-Proofs: theory Main
Timing HOL-Proofs (3 threads, 187.013s elapsed time, 541.463s cpu time, 53.875s GC time, factor 2.90)
Finished HOL-Proofs (0:03:39 elapsed time, 0:09:53 cpu time, factor 2.70)
Building ZF ...
ZF: theory IFOL
ZF: theory FOL
ZF: theory ZF
ZF: theory upair
ZF: theory pair
ZF: theory Bool
ZF: theory equalities
ZF: theory Fixedpt
ZF: theory Sum
ZF: theory func
ZF: theory Perm
ZF: theory QPair
ZF: theory Trancl
ZF: theory EquivClass
ZF: theory WF
ZF: theory Order
ZF: theory Ordinal
ZF: theory OrdQuant
ZF: theory OrderArith
ZF: theory Nat_ZF
ZF: theory Epsilon
ZF: theory OrderType
ZF: theory Inductive_ZF
ZF: theory Finite
ZF: theory Cardinal
ZF: theory Univ
ZF: theory Arith
ZF: theory QUniv
ZF: theory Datatype_ZF
ZF: theory ArithSimp
ZF: theory Int_ZF
ZF: theory CardinalArith
ZF: theory Bin
ZF: theory IntArith
ZF: theory IntDiv_ZF
ZF: theory List_ZF
ZF: theory Main_ZF
ZF: theory AC
ZF: theory Main
ZF: theory Zorn
ZF: theory Cardinal_AC
ZF: theory InfDatatype
ZF: theory Main_ZFC
Timing ZF (3 threads, 10.695s elapsed time, 27.642s cpu time, 1.748s GC time, factor 2.58)
Finished ZF (0:00:13 elapsed time, 0:00:31 cpu time, factor 2.38)
Running HOL-Nominal-Examples ...
HOL-Nominal-Examples: theory CK_Machine
HOL-Nominal-Examples: theory Class1
HOL-Nominal-Examples: theory CR_Takahashi
HOL-Nominal-Examples: theory Compile
HOL-Nominal-Examples: theory Contexts
HOL-Nominal-Examples: theory Crary
HOL-Nominal-Examples: theory Fsub
HOL-Nominal-Examples: theory Height
HOL-Nominal-Examples: theory Lam_Funs
HOL-Nominal-Examples: theory Lambda_mu
HOL-Nominal-Examples: theory CR
HOL-Nominal-Examples: theory SN
HOL-Nominal-Examples: theory LocalWeakening
HOL-Nominal-Examples: theory Pattern
HOL-Nominal-Examples: theory SOS
HOL-Nominal-Examples: theory Standardization
HOL-Nominal-Examples: theory Support
HOL-Nominal-Examples: theory Type_Preservation
HOL-Nominal-Examples: theory W
HOL-Nominal-Examples: theory Weakening
HOL-Nominal-Examples: theory Class2
HOL-Nominal-Examples: theory Class3
HOL-Nominal-Examples: theory Nominal_Examples
HOL-Nominal-Examples: theory VC_Condition
Timing HOL-Nominal-Examples (3 threads, 182.836s elapsed time, 539.322s cpu time, 25.464s GC time, factor 2.95)
Finished HOL-Nominal-Examples (0:03:05 elapsed time, 0:09:01 cpu time, factor 2.92)
Running HOL-Auth ...
HOL-Auth: theory Message
HOL-Auth: theory Nat_Bijection
HOL-Auth: theory All_Symmetric
HOL-Auth: theory Event
HOL-Auth: theory EventSC
HOL-Auth: theory Extensions
HOL-Auth: theory Public
HOL-Auth: theory CertifiedEmail
HOL-Auth: theory KerberosIV
HOL-Auth: theory Analz
HOL-Auth: theory List_Msg
HOL-Auth: theory Guard
HOL-Auth: theory GuardK
HOL-Auth: theory Guard_Public
HOL-Auth: theory KerberosIV_Gets
HOL-Auth: theory Guard_NS_Public
HOL-Auth: theory Proto
HOL-Auth: theory P2
HOL-Auth: theory KerberosV
HOL-Auth: theory Kerberos_BAN
HOL-Auth: theory Kerberos_BAN_Gets
HOL-Auth: theory NS_Public
HOL-Auth: theory NS_Public_Bad
HOL-Auth: theory NS_Shared
HOL-Auth: theory OtwayRees
HOL-Auth: theory OtwayReesBella
HOL-Auth: theory OtwayRees_AN
HOL-Auth: theory OtwayRees_Bad
HOL-Auth: theory P1
HOL-Auth: theory Recur
HOL-Auth: theory WooLam
HOL-Auth: theory Yahalom
HOL-Auth: theory Yahalom2
HOL-Auth: theory Yahalom_Bad
HOL-Auth: theory ZhouGollmann
HOL-Auth: theory Shared
HOL-Auth: theory Guard_Shared
HOL-Auth: theory Auth_Shared
HOL-Auth: theory Guard_OtwayRees
HOL-Auth: theory Guard_Yahalom
HOL-Auth: theory Auth_Guard_Shared
HOL-Auth: theory Smartcard
HOL-Auth: theory TLS
HOL-Auth: theory ShoupRubin
HOL-Auth: theory Auth_Guard_Public
HOL-Auth: theory ShoupRubinBella
HOL-Auth: theory Auth_Public
HOL-Auth: theory Auth_Smartcard
Timing HOL-Auth (3 threads, 79.718s elapsed time, 233.531s cpu time, 9.525s GC time, factor 2.93)
Finished HOL-Auth (0:01:22 elapsed time, 0:03:54 cpu time, factor 2.85)
Running HOL-Bali ...
HOL-Bali: theory Wfrec
HOL-Bali: theory Old_Recdef
HOL-Bali: theory Basis
HOL-Bali: theory Name
HOL-Bali: theory Table
HOL-Bali: theory Type
HOL-Bali: theory Value
HOL-Bali: theory Term
HOL-Bali: theory Decl
HOL-Bali: theory TypeRel
HOL-Bali: theory DeclConcepts
HOL-Bali: theory State
HOL-Bali: theory WellType
HOL-Bali: theory Conform
HOL-Bali: theory Eval
HOL-Bali: theory DefiniteAssignment
HOL-Bali: theory WellForm
HOL-Bali: theory DefiniteAssignmentCorrect
HOL-Bali: theory Example
HOL-Bali: theory TypeSafe
HOL-Bali: theory Evaln
HOL-Bali: theory AxSem
HOL-Bali: theory Trans
HOL-Bali: theory AxCompl
HOL-Bali: theory AxSound
HOL-Bali: theory AxExample
Timing HOL-Bali (3 threads, 59.248s elapsed time, 149.030s cpu time, 6.312s GC time, factor 2.52)
Finished HOL-Bali (0:01:01 elapsed time, 0:02:30 cpu time, factor 2.45)
Running HOL-Decision_Procs ...
HOL-Decision_Procs: theory Code_Binary_Nat
HOL-Decision_Procs: theory Code_Natural
HOL-Decision_Procs: theory DP_Library
HOL-Decision_Procs: theory Code_Integer
HOL-Decision_Procs: theory Dense_Linear_Order
HOL-Decision_Procs: theory Commutative_Ring
HOL-Decision_Procs: theory Efficient_Nat
HOL-Decision_Procs: theory Abstract_Rat
HOL-Decision_Procs: theory Lattice_Algebras
HOL-Decision_Procs: theory Dense_Linear_Order_Ex
HOL-Decision_Procs: theory Polynomial_List
HOL-Decision_Procs: theory Reflected_Multivariate_Polynomial
HOL-Decision_Procs: theory Commutative_Ring_Complete
HOL-Decision_Procs: theory Commutative_Ring_Ex
HOL-Decision_Procs: theory Float
HOL-Decision_Procs: theory Reflection
HOL-Decision_Procs: theory Wfrec
HOL-Decision_Procs: theory Old_Recdef
HOL-Decision_Procs: theory Cooper
HOL-Decision_Procs: theory Approximation
HOL-Decision_Procs: theory Ferrack
HOL-Decision_Procs: theory Approximation_Ex
HOL-Decision_Procs: theory MIR
HOL-Decision_Procs: theory Parametric_Ferrante_Rackoff
HOL-Decision_Procs: theory Decision_Procs
Timing HOL-Decision_Procs (3 threads, 148.003s elapsed time, 436.145s cpu time, 26.471s GC time, factor 2.95)
Finished HOL-Decision_Procs (0:02:30 elapsed time, 0:07:17 cpu time, factor 2.91)
Running HOL-Hoare_Parallel ...
HOL-Hoare_Parallel: theory Graph
HOL-Hoare_Parallel: theory OG_Com
HOL-Hoare_Parallel: theory Quote_Antiquote
HOL-Hoare_Parallel: theory RG_Com
HOL-Hoare_Parallel: theory RG_Tran
HOL-Hoare_Parallel: theory RG_Hoare
HOL-Hoare_Parallel: theory OG_Tran
HOL-Hoare_Parallel: theory RG_Syntax
HOL-Hoare_Parallel: theory RG_Examples
HOL-Hoare_Parallel: theory OG_Hoare
HOL-Hoare_Parallel: theory OG_Tactics
HOL-Hoare_Parallel: theory OG_Syntax
HOL-Hoare_Parallel: theory Gar_Coll
HOL-Hoare_Parallel: theory Mul_Gar_Coll
HOL-Hoare_Parallel: theory OG_Examples
HOL-Hoare_Parallel: theory Hoare_Parallel
Timing HOL-Hoare_Parallel (3 threads, 75.839s elapsed time, 221.446s cpu time, 4.226s GC time, factor 2.92)
Finished HOL-Hoare_Parallel (0:01:17 elapsed time, 0:03:43 cpu time, factor 2.89)
Running HOL-IMP ...
HOL-IMP: theory Char_nat
HOL-IMP: theory List_lexord
HOL-IMP: theory While_Combinator
HOL-IMP: theory Interpretation_with_Defs
HOL-IMP: theory Char_ord
HOL-IMP: theory AExp
HOL-IMP: theory C_like
HOL-IMP: theory Complete_Lattice
HOL-IMP: theory Complete_Lattice_ix
HOL-IMP: theory OO
HOL-IMP: theory Star
HOL-IMP: theory Types
HOL-IMP: theory ASM
HOL-IMP: theory BExp
HOL-IMP: theory Poly_Types
HOL-IMP: theory Com
HOL-IMP: theory Procs
HOL-IMP: theory Vars
HOL-IMP: theory ACom
HOL-IMP: theory ACom_ITP
HOL-IMP: theory Abs_Int_Tests
HOL-IMP: theory Big_Step
HOL-IMP: theory Procs_Dyn_Vars_Dyn
HOL-IMP: theory Procs_Stat_Vars_Dyn
HOL-IMP: theory Compiler
HOL-IMP: theory Denotation
HOL-IMP: theory Hoare
HOL-IMP: theory Hoare_Examples
HOL-IMP: theory Hoare_Sound_Complete
HOL-IMP: theory HoareT
HOL-IMP: theory VC
HOL-IMP: theory Sec_Type_Expr
HOL-IMP: theory Sec_Typing
HOL-IMP: theory Sec_TypingT
HOL-IMP: theory Sem_Equiv
HOL-IMP: theory Procs_Stat_Vars_Stat
HOL-IMP: theory Fold
HOL-IMP: theory Def_Init
HOL-IMP: theory Def_Init_Exp
HOL-IMP: theory Def_Init_Big
HOL-IMP: theory Def_Init_Sound_Big
HOL-IMP: theory Live
HOL-IMP: theory Collecting
HOL-IMP: theory Collecting_ITP
HOL-IMP: theory Comp_Rev
HOL-IMP: theory Def_Init_Small
HOL-IMP: theory Def_Init_Sound_Small
HOL-IMP: theory Small_Step
HOL-IMP: theory Live_True
HOL-IMP: theory Collecting1
HOL-IMP: theory Collecting_Examples
HOL-IMP: theory Abs_Int0_ITP
HOL-IMP: theory Finite_Reachable
HOL-IMP: theory Abs_Int_den0_fun
HOL-IMP: theory Abs_State_den
HOL-IMP: theory Abs_Int_den0
HOL-IMP: theory Abs_Int_den0_const
HOL-IMP: theory Abs_State_ITP
HOL-IMP: theory Abs_Int_init
HOL-IMP: theory Abs_Int0
HOL-IMP: theory Abs_Int1_ITP
HOL-IMP: theory Abs_Int1_const_ITP
HOL-IMP: theory Abs_Int1_parity_ITP
HOL-IMP: theory Abs_Int2_ITP
HOL-IMP: theory Abs_Int2_ivl_ITP
HOL-IMP: theory Abs_Int_den1
HOL-IMP: theory Abs_State
HOL-IMP: theory Abs_Int_den1_ivl
HOL-IMP: theory Abs_Int1
HOL-IMP: theory Abs_Int1_const
HOL-IMP: theory Abs_Int1_parity
HOL-IMP: theory Abs_Int2
HOL-IMP: theory Abs_Int2_ivl
HOL-IMP: theory Abs_Int_den2
HOL-IMP: theory Abs_Int3_ITP
HOL-IMP: theory Abs_Int3
Timing HOL-IMP (3 threads, 166.949s elapsed time, 481.903s cpu time, 48.125s GC time, factor 2.89)
Finished HOL-IMP (0:02:49 elapsed time, 0:08:04 cpu time, factor 2.86)
Running HOL-Library ...
HOL-Library: theory Adhoc_Overloading
HOL-Library: theory Lattice_Syntax
HOL-Library: theory Preorder
HOL-Library: theory Refute
HOL-Library: theory AList
HOL-Library: theory Bit
HOL-Library: theory Boolean_Algebra
HOL-Library: theory Char_nat
HOL-Library: theory Char_ord
HOL-Library: theory Code_Binary_Nat
HOL-Library: theory Code_Char
HOL-Library: theory Code_Natural
HOL-Library: theory Code_Char_ord
HOL-Library: theory Code_Integer
HOL-Library: theory Code_Numeral_Types
HOL-Library: theory Code_Char_chr
HOL-Library: theory Continuity
HOL-Library: theory DAList
HOL-Library: theory Debug
HOL-Library: theory Dlist
HOL-Library: theory Efficient_Nat
HOL-Library: theory IArray
HOL-Library: theory Code_Target_Int
HOL-Library: theory Code_Target_Nat
HOL-Library: theory Eval_Witness
HOL-Library: theory Extended_Nat
HOL-Library: theory Code_Target_Numeral
HOL-Library: theory Fraction_Field
HOL-Library: theory FuncSet
HOL-Library: theory Function_Algebras
HOL-Library: theory Indicator_Function
HOL-Library: theory Function_Division
HOL-Library: theory Infinite_Set
HOL-Library: theory Kleene_Algebra
HOL-Library: theory LaTeXsugar
HOL-Library: theory ListVector
HOL-Library: theory List_lexord
HOL-Library: theory Monad_Syntax
HOL-Library: theory Multiset
HOL-Library: theory Option_ord
HOL-Library: theory Order_Relation
HOL-Library: theory Zorn
HOL-Library: theory Parallel
HOL-Library: theory Diagonal_Subsequence
HOL-Library: theory Nat_Bijection
HOL-Library: theory Abstract_Rat
HOL-Library: theory Binomial
HOL-Library: theory Countable
HOL-Library: theory Code_Real_Approx_By_Float
HOL-Library: theory ContNotDenum
HOL-Library: theory Formal_Power_Series
HOL-Library: theory Countable_Set
HOL-Library: theory FrechetDeriv
HOL-Library: theory Inner_Product
HOL-Library: theory Lattice_Algebras
HOL-Library: theory OptionalSugar
HOL-Library: theory Sum_of_Squares
HOL-Library: theory Permutations
HOL-Library: theory Permutation
HOL-Library: theory Float
HOL-Library: theory Phantom_Type
HOL-Library: theory Polynomial
HOL-Library: theory Cardinality
HOL-Library: theory FinFun
HOL-Library: theory Numeral_Type
HOL-Library: theory Fundamental_Theorem_Algebra
HOL-Library: theory Type_Length
HOL-Library: theory Poly_Deriv
HOL-Library: theory Product_plus
HOL-Library: theory Product_Lattice
HOL-Library: theory Product_Vector
HOL-Library: theory Finite_Lattice
HOL-Library: theory Quotient_Syntax
HOL-Library: theory Quotient_Option
HOL-Library: theory Convex
HOL-Library: theory Quotient_Product
HOL-Library: theory Mapping
HOL-Library: theory Quotient_Set
HOL-Library: theory Quotient_List
HOL-Library: theory AList_Mapping
HOL-Library: theory Quotient_Sum
HOL-Library: theory Quotient_Type
HOL-Library: theory RBT_Impl
HOL-Library: theory Ramsey
HOL-Library: theory Reflection
HOL-Library: theory Saturated
HOL-Library: theory Set_Algebras
HOL-Library: theory BigO
HOL-Library: theory State_Monad
HOL-Library: theory Sublist
HOL-Library: theory Sublist_Order
HOL-Library: theory Transitive_Closure_Table
HOL-Library: theory Univ_Poly
HOL-Library: theory Wfrec
HOL-Library: theory Old_Recdef
HOL-Library: theory While_Combinator
HOL-Library: theory RBT
HOL-Library: theory RBT_Mapping
HOL-Library: theory Library
Skipping theories "Sum_of_Squares_Remote" (undefined ISABELLE_FULL_TEST)
Timing HOL-Library (3 threads, 81.673s elapsed time, 238.808s cpu time, 19.508s GC time, factor 2.92)
Finished HOL-Library (0:01:24 elapsed time, 0:04:00 cpu time, factor 2.85)
Running HOL-MicroJava ...
HOL-MicroJava: theory While_Combinator
HOL-MicroJava: theory Transitive_Closure_Table
HOL-MicroJava: theory Wfrec
HOL-MicroJava: theory Semilat
HOL-MicroJava: theory Err
HOL-MicroJava: theory Listn
HOL-MicroJava: theory JBasis
HOL-MicroJava: theory AuxLemmas
HOL-MicroJava: theory Type
HOL-MicroJava: theory Typing_Framework
HOL-MicroJava: theory Opt
HOL-MicroJava: theory Product
HOL-MicroJava: theory SemilatAlg
HOL-MicroJava: theory Kildall
HOL-MicroJava: theory LBVSpec
HOL-MicroJava: theory LBVComplete
HOL-MicroJava: theory Decl
HOL-MicroJava: theory SystemClasses
HOL-MicroJava: theory Value
HOL-MicroJava: theory TypeRel
HOL-MicroJava: theory LBVCorrect
HOL-MicroJava: theory Typing_Framework_err
HOL-MicroJava: theory Abstract_BV
HOL-MicroJava: theory Term
HOL-MicroJava: theory Semilattices
HOL-MicroJava: theory State
HOL-MicroJava: theory WellForm
HOL-MicroJava: theory Exceptions
HOL-MicroJava: theory JType
HOL-MicroJava: theory JVMType
HOL-MicroJava: theory WellType
HOL-MicroJava: theory Conform
HOL-MicroJava: theory Eval
HOL-MicroJava: theory JVMState
HOL-MicroJava: theory JVMInstructions
HOL-MicroJava: theory JVMExceptions
HOL-MicroJava: theory JVMExecInstr
HOL-MicroJava: theory TypeInf
HOL-MicroJava: theory Effect
HOL-MicroJava: theory JVMExec
HOL-MicroJava: theory DefsComp
HOL-MicroJava: theory Index
HOL-MicroJava: theory JVMDefensive
HOL-MicroJava: theory JVMListExample
HOL-MicroJava: theory Example
HOL-MicroJava: theory JListExample
HOL-MicroJava: theory JTypeSafe
HOL-MicroJava: theory TranslCompTp
HOL-MicroJava: theory TranslComp
HOL-MicroJava: theory LemmasComp
HOL-MicroJava: theory CorrComp
HOL-MicroJava: theory BVSpec
HOL-MicroJava: theory Altern
HOL-MicroJava: theory Correct
HOL-MicroJava: theory EffectMono
HOL-MicroJava: theory Typing_Framework_JVM
HOL-MicroJava: theory BVSpecTypeSafe
HOL-MicroJava: theory JVM
HOL-MicroJava: theory CorrCompTp
HOL-MicroJava: theory LBVJVM
HOL-MicroJava: theory BVNoTypeError
HOL-MicroJava: theory BVExample
HOL-MicroJava: theory MicroJava
Timing HOL-MicroJava (3 threads, 75.830s elapsed time, 223.390s cpu time, 8.301s GC time, factor 2.95)
Finished HOL-MicroJava (0:01:17 elapsed time, 0:03:44 cpu time, factor 2.90)
Running HOL-Probability ...
HOL-Probability: theory AList
HOL-Probability: theory DAList
HOL-Probability: theory Multiset
HOL-Probability: theory Permutation
HOL-Probability: theory Diagonal_Subsequence
HOL-Probability: theory Sigma_Algebra
HOL-Probability: theory Discrete_Topology
HOL-Probability: theory Measurable
HOL-Probability: theory Measure_Space
HOL-Probability: theory Borel_Space
HOL-Probability: theory Caratheodory
HOL-Probability: theory Lebesgue_Integration
HOL-Probability: theory Regularity
HOL-Probability: theory Binary_Product_Measure
HOL-Probability: theory Complete_Measure
HOL-Probability: theory Radon_Nikodym
HOL-Probability: theory Finite_Product_Measure
HOL-Probability: theory Fin_Map
HOL-Probability: theory Lebesgue_Measure
HOL-Probability: theory Probability_Measure
HOL-Probability: theory Distributions
HOL-Probability: theory Projective_Family
HOL-Probability: theory Infinite_Product_Measure
HOL-Probability: theory Independent_Family
HOL-Probability: theory Projective_Limit
HOL-Probability: theory Information
HOL-Probability: theory Dining_Cryptographers
HOL-Probability: theory Koepf_Duermuth_Countermeasure
HOL-Probability: theory Probability
Timing HOL-Probability (3 threads, 55.962s elapsed time, 163.108s cpu time, 5.493s GC time, factor 2.91)
Finished HOL-Probability (0:00:59 elapsed time, 0:02:45 cpu time, factor 2.79)
Running HOL-Proofs-Extraction ...
HOL-Proofs-Extraction: theory Adhoc_Overloading
HOL-Proofs-Extraction: theory AList
HOL-Proofs-Extraction: theory Code_Binary_Nat
HOL-Proofs-Extraction: theory Code_Natural
HOL-Proofs-Extraction: theory Code_Integer
HOL-Proofs-Extraction: theory Fact
HOL-Proofs-Extraction: theory Efficient_Nat
HOL-Proofs-Extraction: theory Monad_Syntax
HOL-Proofs-Extraction: theory Parity
HOL-Proofs-Extraction: theory State_Monad
HOL-Proofs-Extraction: theory DAList
HOL-Proofs-Extraction: theory Multiset
HOL-Proofs-Extraction: theory GCD
HOL-Proofs-Extraction: theory Primes
HOL-Proofs-Extraction: theory Cong
HOL-Proofs-Extraction: theory UniqueFactorization
HOL-Proofs-Extraction: theory Higman
HOL-Proofs-Extraction: theory Util
HOL-Proofs-Extraction: theory Warshall
HOL-Proofs-Extraction: theory Euclid
HOL-Proofs-Extraction: theory Higman_Extraction
HOL-Proofs-Extraction: theory Pigeonhole
HOL-Proofs-Extraction: theory QuotRem
HOL-Proofs-Extraction: theory Greatest_Common_Divisor
Timing HOL-Proofs-Extraction (3 threads, 136.246s elapsed time, 352.610s cpu time, 23.684s GC time, factor 2.59)
Finished HOL-Proofs-Extraction (0:02:19 elapsed time, 0:05:53 cpu time, factor 2.53)
Running HOL-SET_Protocol ...
HOL-SET_Protocol: theory Nat_Bijection
HOL-SET_Protocol: theory Message_SET
HOL-SET_Protocol: theory Event_SET
HOL-SET_Protocol: theory Public_SET
HOL-SET_Protocol: theory Cardholder_Registration
HOL-SET_Protocol: theory Merchant_Registration
HOL-SET_Protocol: theory Purchase
HOL-SET_Protocol: theory SET_Protocol
Timing HOL-SET_Protocol (3 threads, 26.064s elapsed time, 70.734s cpu time, 1.423s GC time, factor 2.71)
Finished HOL-SET_Protocol (0:00:28 elapsed time, 0:01:12 cpu time, factor 2.57)
Running HOL-UNITY ...
HOL-UNITY: theory Message
HOL-UNITY: theory Event
HOL-UNITY: theory Public
HOL-UNITY: theory AList
HOL-UNITY: theory UNITY
HOL-UNITY: theory ListOrder
HOL-UNITY: theory Constrains
HOL-UNITY: theory Deadlock
HOL-UNITY: theory FP
HOL-UNITY: theory Network
HOL-UNITY: theory WFair
HOL-UNITY: theory DAList
HOL-UNITY: theory SubstAx
HOL-UNITY: theory Token
HOL-UNITY: theory Detects
HOL-UNITY: theory Union
HOL-UNITY: theory Multiset
HOL-UNITY: theory Comp
HOL-UNITY: theory Guar
HOL-UNITY: theory Transformers
HOL-UNITY: theory Extend
HOL-UNITY: theory ProgressSets
HOL-UNITY: theory Project
HOL-UNITY: theory Rename
HOL-UNITY: theory Lift_prog
HOL-UNITY: theory ELT
HOL-UNITY: theory Follows
HOL-UNITY: theory PPROD
HOL-UNITY: theory UNITY_Main
HOL-UNITY: theory AllocBase
HOL-UNITY: theory Channel
HOL-UNITY: theory Alloc
HOL-UNITY: theory AllocImpl
HOL-UNITY: theory Client
HOL-UNITY: theory Common
HOL-UNITY: theory Counter
HOL-UNITY: theory Counterc
HOL-UNITY: theory Handshake
HOL-UNITY: theory Lift
HOL-UNITY: theory Mutex
HOL-UNITY: theory NSP_Bad
HOL-UNITY: theory PriorityAux
HOL-UNITY: theory Priority
HOL-UNITY: theory Progress
HOL-UNITY: theory Reach
HOL-UNITY: theory TimerArray
HOL-UNITY: theory Reachability
Timing HOL-UNITY (3 threads, 25.574s elapsed time, 72.020s cpu time, 3.529s GC time, factor 2.82)
Finished HOL-UNITY (0:00:27 elapsed time, 0:01:13 cpu time, factor 2.70)
Running ZF-UNITY ...
ZF-UNITY: theory Acc
ZF-UNITY: theory GenPrefix
ZF-UNITY: theory FoldSet
ZF-UNITY: theory State
ZF-UNITY: theory UNITY
ZF-UNITY: theory Multiset
ZF-UNITY: theory Constrains
ZF-UNITY: theory FP
ZF-UNITY: theory WFair
ZF-UNITY: theory MultisetSum
ZF-UNITY: theory SubstAx
ZF-UNITY: theory Monotonicity
ZF-UNITY: theory Increasing
ZF-UNITY: theory Mutex
ZF-UNITY: theory Follows
ZF-UNITY: theory Union
ZF-UNITY: theory Comp
ZF-UNITY: theory Guar
ZF-UNITY: theory AllocBase
ZF-UNITY: theory ClientImpl
ZF-UNITY: theory Distributor
ZF-UNITY: theory Merge
ZF-UNITY: theory AllocImpl
Timing ZF-UNITY (3 threads, 10.766s elapsed time, 31.422s cpu time, 1.128s GC time, factor 2.92)
Finished ZF-UNITY (0:00:12 elapsed time, 0:00:31 cpu time, factor 2.58)
Finished at Mon Feb 4 19:54:19 CET 2013
0:26:52 elapsed time, 1:13:07 cpu time, factor 2.72
*** m=4 q=2 ***
Started at Mon Feb 4 19:54:19 CET 2013 (polyml-5.5.0_x86-darwin on lri29-163.lri.fr)
ISABELLE_BUILD_OPTIONS="threads_trace=2 threads=4 parallel_proofs=2"
ML_PLATFORM="x86-darwin"
ML_HOME="/Volumes/Macintosh_HD/Users/makarius/.isabelle/contrib/polyml-5.5.0-3/x86-darwin"
ML_SYSTEM="polyml-5.5.0"
ML_OPTIONS="--minheap 1000 --gcthreads 4"
Session Pure
Session HOL (main)
Session HOL-Auth
Session HOL-Bali
Session HOL-Decision_Procs
Session HOL-Hoare_Parallel
Session HOL-IMP
Session HOL-Library (main)
Session HOL-MicroJava
Session HOL-Multivariate_Analysis (main)
Session HOL-Probability
Session HOL-Nominal (main)
Session HOL-Nominal-Examples
Session HOL-SET_Protocol
Session HOL-UNITY
Session HOL-Proofs
Session HOL-Proofs-Extraction
Session ZF (main)
Session ZF-UNITY
Building Pure ...
Finished Pure (0:00:09 elapsed time, 0:00:08 cpu time, factor 0.88)
Building HOL ...
HOL: theory Code_Generator
HOL: theory HOL
HOL: theory Orderings
HOL: theory SAT
HOL: theory Groups
HOL: theory Rings
HOL: theory Lattices
HOL: theory Set
HOL: theory Complete_Lattices
HOL: theory Typedef
HOL: theory Fun
HOL: theory Inductive
HOL: theory Fields
HOL: theory Product_Type
HOL: theory Sum_Type
HOL: theory Complete_Partial_Order
HOL: theory Nat
HOL: theory Datatype
HOL: theory Meson
HOL: theory Num
HOL: theory Option
HOL: theory Extraction
HOL: theory Partial_Function
HOL: theory ATP
HOL: theory Power
HOL: theory Metis
HOL: theory Finite_Set
HOL: theory Relation
HOL: theory Transitive_Closure
HOL: theory Wellfounded
HOL: theory FunDef
HOL: theory Plain
HOL: theory Big_Operators
HOL: theory Hilbert_Choice
HOL: theory Equiv_Relations
HOL: theory Transfer
HOL: theory Lifting
HOL: theory Quotient
HOL: theory Int
HOL: theory Nat_Transfer
HOL: theory Divides
HOL: theory Set_Interval
HOL: theory Code_Numeral
HOL: theory Numeral_Simprocs
HOL: theory Semiring_Normalization
HOL: theory Groebner_Basis
HOL: theory Presburger
HOL: theory List
HOL: theory Map
HOL: theory Predicate
HOL: theory Random
HOL: theory Enum
HOL: theory Lazy_Sequence
HOL: theory String
HOL: theory DSequence
HOL: theory New_DSequence
HOL: theory Typerep
HOL: theory Code_Evaluation
HOL: theory Quickcheck
HOL: theory Quickcheck_Exhaustive
HOL: theory Random_Sequence
HOL: theory New_Random_Sequence
HOL: theory Quickcheck_Narrowing
HOL: theory Predicate_Compile
HOL: theory Record
HOL: theory SMT
HOL: theory Sledgehammer
HOL: theory Nitpick
HOL: theory Main
HOL: theory Archimedean_Field
HOL: theory Lubs
HOL: theory Fact
HOL: theory Parity
HOL: theory GCD
HOL: theory Rat
HOL: theory RealDef
HOL: theory RComplete
HOL: theory RealVector
HOL: theory SupInf
HOL: theory Limits
HOL: theory Real
HOL: theory SEQ
HOL: theory Lim
HOL: theory Deriv
HOL: theory Series
HOL: theory NthRoot
HOL: theory Transcendental
HOL: theory Complex
HOL: theory Ln
HOL: theory Log
HOL: theory MacLaurin
HOL: theory Taylor
HOL: theory Complex_Main
Timing HOL (4 threads, 90.243s elapsed time, 231.528s cpu time, 19.436s GC time, factor 2.57)
Finished HOL (0:01:52 elapsed time, 0:04:28 cpu time, factor 2.39)
Building HOL-Multivariate_Analysis ...
HOL-Multivariate_Analysis: theory Extended_Nat
HOL-Multivariate_Analysis: theory Indicator_Function
HOL-Multivariate_Analysis: theory FuncSet
HOL-Multivariate_Analysis: theory Infinite_Set
HOL-Multivariate_Analysis: theory Glbs
HOL-Multivariate_Analysis: theory Nat_Bijection
HOL-Multivariate_Analysis: theory L2_Norm
HOL-Multivariate_Analysis: theory FrechetDeriv
HOL-Multivariate_Analysis: theory Sum_of_Squares
HOL-Multivariate_Analysis: theory Inner_Product
HOL-Multivariate_Analysis: theory Countable
HOL-Multivariate_Analysis: theory Extended_Real
HOL-Multivariate_Analysis: theory Permutations
HOL-Multivariate_Analysis: theory Countable_Set
HOL-Multivariate_Analysis: theory Phantom_Type
HOL-Multivariate_Analysis: theory Product_plus
HOL-Multivariate_Analysis: theory Product_Vector
HOL-Multivariate_Analysis: theory Cardinality
HOL-Multivariate_Analysis: theory Convex
HOL-Multivariate_Analysis: theory Euclidean_Space
HOL-Multivariate_Analysis: theory Norm_Arith
HOL-Multivariate_Analysis: theory Set_Algebras
HOL-Multivariate_Analysis: theory Numeral_Type
HOL-Multivariate_Analysis: theory Linear_Algebra
HOL-Multivariate_Analysis: theory Finite_Cartesian_Product
HOL-Multivariate_Analysis: theory Operator_Norm
HOL-Multivariate_Analysis: theory Topology_Euclidean_Space
HOL-Multivariate_Analysis: theory Extended_Real_Limits
HOL-Multivariate_Analysis: theory Convex_Euclidean_Space
HOL-Multivariate_Analysis: theory Brouwer_Fixpoint
HOL-Multivariate_Analysis: theory Path_Connected
HOL-Multivariate_Analysis: theory Derivative
HOL-Multivariate_Analysis: theory Integration
HOL-Multivariate_Analysis: theory Cartesian_Euclidean_Space
HOL-Multivariate_Analysis: theory Determinants
HOL-Multivariate_Analysis: theory Fashoda
HOL-Multivariate_Analysis: theory Multivariate_Analysis
Timing HOL-Multivariate_Analysis (4 threads, 47.033s elapsed time, 184.610s cpu time, 7.315s GC time, factor 3.93)
Finished HOL-Multivariate_Analysis (0:01:02 elapsed time, 0:03:24 cpu time, factor 3.29)
Building HOL-Nominal ...
HOL-Nominal: theory Infinite_Set
HOL-Nominal: theory Nominal
Timing HOL-Nominal (4 threads, 4.329s elapsed time, 9.011s cpu time, 0.402s GC time, factor 2.08)
Finished HOL-Nominal (0:00:14 elapsed time, 0:00:20 cpu time, factor 1.42)
Building HOL-Proofs ...
HOL-Proofs: theory Code_Generator
HOL-Proofs: theory HOL
HOL-Proofs: theory Orderings
HOL-Proofs: theory SAT
HOL-Proofs: theory Groups
HOL-Proofs: theory Rings
HOL-Proofs: theory Lattices
HOL-Proofs: theory Set
HOL-Proofs: theory Complete_Lattices
HOL-Proofs: theory Typedef
HOL-Proofs: theory Fun
HOL-Proofs: theory Inductive
HOL-Proofs: theory Fields
HOL-Proofs: theory Product_Type
HOL-Proofs: theory Sum_Type
HOL-Proofs: theory Complete_Partial_Order
HOL-Proofs: theory Nat
HOL-Proofs: theory Datatype
HOL-Proofs: theory Meson
HOL-Proofs: theory Num
HOL-Proofs: theory ATP
HOL-Proofs: theory Option
HOL-Proofs: theory Extraction
HOL-Proofs: theory Metis
HOL-Proofs: theory Partial_Function
HOL-Proofs: theory Power
HOL-Proofs: theory Finite_Set
HOL-Proofs: theory Relation
HOL-Proofs: theory Transitive_Closure
HOL-Proofs: theory Wellfounded
HOL-Proofs: theory FunDef
HOL-Proofs: theory Plain
HOL-Proofs: theory Big_Operators
HOL-Proofs: theory Hilbert_Choice
HOL-Proofs: theory Equiv_Relations
HOL-Proofs: theory Transfer
HOL-Proofs: theory Lifting
HOL-Proofs: theory Quotient
HOL-Proofs: theory Int
HOL-Proofs: theory Nat_Transfer
HOL-Proofs: theory Divides
HOL-Proofs: theory Set_Interval
HOL-Proofs: theory Code_Numeral
HOL-Proofs: theory Numeral_Simprocs
HOL-Proofs: theory Semiring_Normalization
HOL-Proofs: theory Groebner_Basis
HOL-Proofs: theory Presburger
HOL-Proofs: theory List
HOL-Proofs: theory Map
HOL-Proofs: theory Predicate
HOL-Proofs: theory Random
HOL-Proofs: theory Enum
HOL-Proofs: theory Lazy_Sequence
HOL-Proofs: theory String
HOL-Proofs: theory DSequence
HOL-Proofs: theory New_DSequence
HOL-Proofs: theory Typerep
HOL-Proofs: theory Code_Evaluation
HOL-Proofs: theory Quickcheck
HOL-Proofs: theory Quickcheck_Exhaustive
HOL-Proofs: theory Random_Sequence
HOL-Proofs: theory New_Random_Sequence
HOL-Proofs: theory Quickcheck_Narrowing
HOL-Proofs: theory Predicate_Compile
HOL-Proofs: theory Record
HOL-Proofs: theory SMT
HOL-Proofs: theory Sledgehammer
HOL-Proofs: theory Nitpick
HOL-Proofs: theory Main
Timing HOL-Proofs (4 threads, 152.260s elapsed time, 529.584s cpu time, 41.335s GC time, factor 3.48)
Finished HOL-Proofs (0:03:03 elapsed time, 0:09:45 cpu time, factor 3.19)
Building ZF ...
ZF: theory IFOL
ZF: theory FOL
ZF: theory ZF
ZF: theory upair
ZF: theory pair
ZF: theory Bool
ZF: theory equalities
ZF: theory Fixedpt
ZF: theory Sum
ZF: theory func
ZF: theory Perm
ZF: theory QPair
ZF: theory Trancl
ZF: theory EquivClass
ZF: theory WF
ZF: theory Order
ZF: theory Ordinal
ZF: theory OrdQuant
ZF: theory OrderArith
ZF: theory Nat_ZF
ZF: theory Epsilon
ZF: theory OrderType
ZF: theory Inductive_ZF
ZF: theory Finite
ZF: theory Cardinal
ZF: theory Univ
ZF: theory Arith
ZF: theory QUniv
ZF: theory Datatype_ZF
ZF: theory ArithSimp
ZF: theory Int_ZF
ZF: theory CardinalArith
ZF: theory List_ZF
ZF: theory Bin
ZF: theory IntArith
ZF: theory IntDiv_ZF
ZF: theory Main_ZF
ZF: theory AC
ZF: theory Main
ZF: theory Zorn
ZF: theory Cardinal_AC
ZF: theory InfDatatype
ZF: theory Main_ZFC
Timing ZF (4 threads, 8.801s elapsed time, 27.775s cpu time, 1.700s GC time, factor 3.16)
Finished ZF (0:00:12 elapsed time, 0:00:31 cpu time, factor 2.58)
Running HOL-Nominal-Examples ...
HOL-Nominal-Examples: theory CK_Machine
HOL-Nominal-Examples: theory CR_Takahashi
HOL-Nominal-Examples: theory Class1
HOL-Nominal-Examples: theory Compile
HOL-Nominal-Examples: theory Contexts
HOL-Nominal-Examples: theory Crary
HOL-Nominal-Examples: theory Fsub
HOL-Nominal-Examples: theory Height
HOL-Nominal-Examples: theory Lam_Funs
HOL-Nominal-Examples: theory Lambda_mu
HOL-Nominal-Examples: theory CR
HOL-Nominal-Examples: theory SN
HOL-Nominal-Examples: theory LocalWeakening
HOL-Nominal-Examples: theory Pattern
HOL-Nominal-Examples: theory SOS
HOL-Nominal-Examples: theory Standardization
HOL-Nominal-Examples: theory Support
HOL-Nominal-Examples: theory Type_Preservation
HOL-Nominal-Examples: theory W
HOL-Nominal-Examples: theory Weakening
HOL-Nominal-Examples: theory Class2
HOL-Nominal-Examples: theory Class3
HOL-Nominal-Examples: theory Nominal_Examples
HOL-Nominal-Examples: theory VC_Condition
Timing HOL-Nominal-Examples (4 threads, 142.768s elapsed time, 556.184s cpu time, 28.822s GC time, factor 3.90)
Finished HOL-Nominal-Examples (0:02:26 elapsed time, 0:09:18 cpu time, factor 3.82)
Running HOL-Auth ...
HOL-Auth: theory Message
HOL-Auth: theory Nat_Bijection
HOL-Auth: theory All_Symmetric
HOL-Auth: theory Event
HOL-Auth: theory EventSC
HOL-Auth: theory Extensions
HOL-Auth: theory Public
HOL-Auth: theory Shared
HOL-Auth: theory CertifiedEmail
HOL-Auth: theory KerberosIV
HOL-Auth: theory KerberosIV_Gets
HOL-Auth: theory Analz
HOL-Auth: theory Guard
HOL-Auth: theory GuardK
HOL-Auth: theory List_Msg
HOL-Auth: theory Guard_Public
HOL-Auth: theory KerberosV
HOL-Auth: theory Guard_NS_Public
HOL-Auth: theory Proto
HOL-Auth: theory Kerberos_BAN
HOL-Auth: theory Kerberos_BAN_Gets
HOL-Auth: theory NS_Public
HOL-Auth: theory NS_Public_Bad
HOL-Auth: theory NS_Shared
HOL-Auth: theory OtwayRees
HOL-Auth: theory P2
HOL-Auth: theory OtwayReesBella
HOL-Auth: theory OtwayRees_AN
HOL-Auth: theory OtwayRees_Bad
HOL-Auth: theory P1
HOL-Auth: theory Recur
HOL-Auth: theory WooLam
HOL-Auth: theory Yahalom
HOL-Auth: theory Yahalom2
HOL-Auth: theory Yahalom_Bad
HOL-Auth: theory ZhouGollmann
HOL-Auth: theory Guard_Shared
HOL-Auth: theory Auth_Shared
HOL-Auth: theory Guard_OtwayRees
HOL-Auth: theory Guard_Yahalom
HOL-Auth: theory Smartcard
HOL-Auth: theory Auth_Guard_Shared
HOL-Auth: theory TLS
HOL-Auth: theory ShoupRubin
HOL-Auth: theory ShoupRubinBella
HOL-Auth: theory Auth_Public
HOL-Auth: theory Auth_Guard_Public
HOL-Auth: theory Auth_Smartcard
Timing HOL-Auth (4 threads, 62.029s elapsed time, 237.081s cpu time, 10.843s GC time, factor 3.82)
Finished HOL-Auth (0:01:04 elapsed time, 0:03:58 cpu time, factor 3.71)
Running HOL-Bali ...
HOL-Bali: theory Wfrec
HOL-Bali: theory Old_Recdef
HOL-Bali: theory Basis
HOL-Bali: theory Name
HOL-Bali: theory Table
HOL-Bali: theory Type
HOL-Bali: theory Value
HOL-Bali: theory Term
HOL-Bali: theory Decl
HOL-Bali: theory TypeRel
HOL-Bali: theory DeclConcepts
HOL-Bali: theory State
HOL-Bali: theory WellType
HOL-Bali: theory Conform
HOL-Bali: theory Eval
HOL-Bali: theory DefiniteAssignment
HOL-Bali: theory WellForm
HOL-Bali: theory DefiniteAssignmentCorrect
HOL-Bali: theory Example
HOL-Bali: theory TypeSafe
HOL-Bali: theory Evaln
HOL-Bali: theory AxSem
HOL-Bali: theory Trans
HOL-Bali: theory AxCompl
HOL-Bali: theory AxSound
HOL-Bali: theory AxExample
Timing HOL-Bali (4 threads, 50.271s elapsed time, 152.698s cpu time, 7.031s GC time, factor 3.04)
Finished HOL-Bali (0:00:52 elapsed time, 0:02:33 cpu time, factor 2.94)
Running HOL-Decision_Procs ...
HOL-Decision_Procs: theory Code_Binary_Nat
HOL-Decision_Procs: theory Code_Natural
HOL-Decision_Procs: theory Dense_Linear_Order
HOL-Decision_Procs: theory DP_Library
HOL-Decision_Procs: theory Code_Integer
HOL-Decision_Procs: theory Commutative_Ring
HOL-Decision_Procs: theory Abstract_Rat
HOL-Decision_Procs: theory Efficient_Nat
HOL-Decision_Procs: theory Lattice_Algebras
HOL-Decision_Procs: theory Polynomial_List
HOL-Decision_Procs: theory Reflected_Multivariate_Polynomial
HOL-Decision_Procs: theory Dense_Linear_Order_Ex
HOL-Decision_Procs: theory Reflection
HOL-Decision_Procs: theory Wfrec
HOL-Decision_Procs: theory Old_Recdef
HOL-Decision_Procs: theory Commutative_Ring_Complete
HOL-Decision_Procs: theory Commutative_Ring_Ex
HOL-Decision_Procs: theory Cooper
HOL-Decision_Procs: theory Float
HOL-Decision_Procs: theory Ferrack
HOL-Decision_Procs: theory Approximation
HOL-Decision_Procs: theory MIR
HOL-Decision_Procs: theory Parametric_Ferrante_Rackoff
HOL-Decision_Procs: theory Approximation_Ex
HOL-Decision_Procs: theory Decision_Procs
Timing HOL-Decision_Procs (4 threads, 114.745s elapsed time, 443.012s cpu time, 29.168s GC time, factor 3.86)
Finished HOL-Decision_Procs (0:01:56 elapsed time, 0:07:23 cpu time, factor 3.81)
Running HOL-Hoare_Parallel ...
HOL-Hoare_Parallel: theory Graph
HOL-Hoare_Parallel: theory RG_Com
HOL-Hoare_Parallel: theory OG_Com
HOL-Hoare_Parallel: theory Quote_Antiquote
HOL-Hoare_Parallel: theory RG_Tran
HOL-Hoare_Parallel: theory RG_Hoare
HOL-Hoare_Parallel: theory OG_Tran
HOL-Hoare_Parallel: theory RG_Syntax
HOL-Hoare_Parallel: theory RG_Examples
HOL-Hoare_Parallel: theory OG_Hoare
HOL-Hoare_Parallel: theory OG_Tactics
HOL-Hoare_Parallel: theory OG_Syntax
HOL-Hoare_Parallel: theory Gar_Coll
HOL-Hoare_Parallel: theory Mul_Gar_Coll
HOL-Hoare_Parallel: theory OG_Examples
HOL-Hoare_Parallel: theory Hoare_Parallel
Timing HOL-Hoare_Parallel (4 threads, 58.497s elapsed time, 224.861s cpu time, 4.632s GC time, factor 3.84)
Finished HOL-Hoare_Parallel (0:01:01 elapsed time, 0:03:46 cpu time, factor 3.70)
Running HOL-IMP ...
HOL-IMP: theory Char_nat
HOL-IMP: theory List_lexord
HOL-IMP: theory While_Combinator
HOL-IMP: theory Interpretation_with_Defs
HOL-IMP: theory Char_ord
HOL-IMP: theory AExp
HOL-IMP: theory C_like
HOL-IMP: theory Complete_Lattice
HOL-IMP: theory Complete_Lattice_ix
HOL-IMP: theory OO
HOL-IMP: theory Star
HOL-IMP: theory Types
HOL-IMP: theory Poly_Types
HOL-IMP: theory ASM
HOL-IMP: theory BExp
HOL-IMP: theory Com
HOL-IMP: theory Procs
HOL-IMP: theory Vars
HOL-IMP: theory ACom_ITP
HOL-IMP: theory ACom
HOL-IMP: theory Abs_Int_Tests
HOL-IMP: theory Big_Step
HOL-IMP: theory Procs_Dyn_Vars_Dyn
HOL-IMP: theory Procs_Stat_Vars_Dyn
HOL-IMP: theory Procs_Stat_Vars_Stat
HOL-IMP: theory Compiler
HOL-IMP: theory Denotation
HOL-IMP: theory Hoare
HOL-IMP: theory Sec_Type_Expr
HOL-IMP: theory Hoare_Examples
HOL-IMP: theory Hoare_Sound_Complete
HOL-IMP: theory HoareT
HOL-IMP: theory VC
HOL-IMP: theory Sec_Typing
HOL-IMP: theory Sec_TypingT
HOL-IMP: theory Sem_Equiv
HOL-IMP: theory Def_Init
HOL-IMP: theory Fold
HOL-IMP: theory Def_Init_Exp
HOL-IMP: theory Live
HOL-IMP: theory Def_Init_Big
HOL-IMP: theory Collecting
HOL-IMP: theory Def_Init_Sound_Big
HOL-IMP: theory Collecting_ITP
HOL-IMP: theory Def_Init_Small
HOL-IMP: theory Def_Init_Sound_Small
HOL-IMP: theory Small_Step
HOL-IMP: theory Live_True
HOL-IMP: theory Comp_Rev
HOL-IMP: theory Collecting1
HOL-IMP: theory Collecting_Examples
HOL-IMP: theory Abs_Int0_ITP
HOL-IMP: theory Finite_Reachable
HOL-IMP: theory Abs_Int_den0_fun
HOL-IMP: theory Abs_Int_init
HOL-IMP: theory Abs_Int0
HOL-IMP: theory Abs_State_den
HOL-IMP: theory Abs_Int_den0
HOL-IMP: theory Abs_Int_den0_const
HOL-IMP: theory Abs_State_ITP
HOL-IMP: theory Abs_Int1_ITP
HOL-IMP: theory Abs_State
HOL-IMP: theory Abs_Int1_const_ITP
HOL-IMP: theory Abs_Int1_parity_ITP
HOL-IMP: theory Abs_Int2_ITP
HOL-IMP: theory Abs_Int_den1
HOL-IMP: theory Abs_Int2_ivl_ITP
HOL-IMP: theory Abs_Int_den1_ivl
HOL-IMP: theory Abs_Int1
HOL-IMP: theory Abs_Int1_const
HOL-IMP: theory Abs_Int1_parity
HOL-IMP: theory Abs_Int2
HOL-IMP: theory Abs_Int2_ivl
HOL-IMP: theory Abs_Int_den2
HOL-IMP: theory Abs_Int3_ITP
HOL-IMP: theory Abs_Int3
Timing HOL-IMP (4 threads, 130.966s elapsed time, 484.868s cpu time, 47.209s GC time, factor 3.70)
Finished HOL-IMP (0:02:13 elapsed time, 0:08:07 cpu time, factor 3.66)
Running HOL-Library ...
HOL-Library: theory Adhoc_Overloading
HOL-Library: theory Lattice_Syntax
HOL-Library: theory Preorder
HOL-Library: theory Refute
HOL-Library: theory AList
HOL-Library: theory Bit
HOL-Library: theory Boolean_Algebra
HOL-Library: theory Char_nat
HOL-Library: theory Code_Binary_Nat
HOL-Library: theory Char_ord
HOL-Library: theory Code_Char
HOL-Library: theory Code_Natural
HOL-Library: theory Code_Integer
HOL-Library: theory Code_Numeral_Types
HOL-Library: theory Code_Char_ord
HOL-Library: theory Code_Char_chr
HOL-Library: theory Continuity
HOL-Library: theory Debug
HOL-Library: theory Dlist
HOL-Library: theory Efficient_Nat
HOL-Library: theory IArray
HOL-Library: theory DAList
HOL-Library: theory Eval_Witness
HOL-Library: theory Extended_Nat
HOL-Library: theory Fraction_Field
HOL-Library: theory Code_Target_Int
HOL-Library: theory Code_Target_Nat
HOL-Library: theory FuncSet
HOL-Library: theory Code_Target_Numeral
HOL-Library: theory Function_Algebras
HOL-Library: theory Indicator_Function
HOL-Library: theory Infinite_Set
HOL-Library: theory Function_Division
HOL-Library: theory Kleene_Algebra
HOL-Library: theory LaTeXsugar
HOL-Library: theory ListVector
HOL-Library: theory List_lexord
HOL-Library: theory Monad_Syntax
HOL-Library: theory Multiset
HOL-Library: theory Option_ord
HOL-Library: theory Order_Relation
HOL-Library: theory Parallel
HOL-Library: theory Zorn
HOL-Library: theory Diagonal_Subsequence
HOL-Library: theory Nat_Bijection
HOL-Library: theory Abstract_Rat
HOL-Library: theory Binomial
HOL-Library: theory Countable
HOL-Library: theory Code_Real_Approx_By_Float
HOL-Library: theory ContNotDenum
HOL-Library: theory Formal_Power_Series
HOL-Library: theory Countable_Set
HOL-Library: theory FrechetDeriv
HOL-Library: theory Inner_Product
HOL-Library: theory Lattice_Algebras
HOL-Library: theory OptionalSugar
HOL-Library: theory Sum_of_Squares
HOL-Library: theory Permutations
HOL-Library: theory Permutation
HOL-Library: theory Phantom_Type
HOL-Library: theory Cardinality
HOL-Library: theory Polynomial
HOL-Library: theory Product_plus
HOL-Library: theory Product_Lattice
HOL-Library: theory FinFun
HOL-Library: theory Float
HOL-Library: theory Numeral_Type
HOL-Library: theory Type_Length
HOL-Library: theory Finite_Lattice
HOL-Library: theory Fundamental_Theorem_Algebra
HOL-Library: theory Poly_Deriv
HOL-Library: theory Product_Vector
HOL-Library: theory Quotient_Syntax
HOL-Library: theory Quotient_Option
HOL-Library: theory Quotient_Product
HOL-Library: theory Convex
HOL-Library: theory Mapping
HOL-Library: theory Quotient_Set
HOL-Library: theory Quotient_Sum
HOL-Library: theory Quotient_List
HOL-Library: theory Quotient_Type
HOL-Library: theory RBT_Impl
HOL-Library: theory AList_Mapping
HOL-Library: theory Ramsey
HOL-Library: theory Reflection
HOL-Library: theory Saturated
HOL-Library: theory Set_Algebras
HOL-Library: theory State_Monad
HOL-Library: theory Sublist
HOL-Library: theory BigO
HOL-Library: theory Transitive_Closure_Table
HOL-Library: theory Sublist_Order
HOL-Library: theory Univ_Poly
HOL-Library: theory Wfrec
HOL-Library: theory Old_Recdef
HOL-Library: theory While_Combinator
HOL-Library: theory RBT
HOL-Library: theory RBT_Mapping
HOL-Library: theory Library
Skipping theories "Sum_of_Squares_Remote" (undefined ISABELLE_FULL_TEST)
Timing HOL-Library (4 threads, 62.821s elapsed time, 240.654s cpu time, 19.421s GC time, factor 3.83)
Finished HOL-Library (0:01:05 elapsed time, 0:04:01 cpu time, factor 3.70)
Running HOL-MicroJava ...
HOL-MicroJava: theory While_Combinator
HOL-MicroJava: theory Transitive_Closure_Table
HOL-MicroJava: theory Wfrec
HOL-MicroJava: theory Semilat
HOL-MicroJava: theory Err
HOL-MicroJava: theory Listn
HOL-MicroJava: theory JBasis
HOL-MicroJava: theory AuxLemmas
HOL-MicroJava: theory Type
HOL-MicroJava: theory Typing_Framework
HOL-MicroJava: theory Opt
HOL-MicroJava: theory Product
HOL-MicroJava: theory SemilatAlg
HOL-MicroJava: theory Semilattices
HOL-MicroJava: theory Kildall
HOL-MicroJava: theory LBVSpec
HOL-MicroJava: theory Typing_Framework_err
HOL-MicroJava: theory LBVComplete
HOL-MicroJava: theory LBVCorrect
HOL-MicroJava: theory Abstract_BV
HOL-MicroJava: theory Decl
HOL-MicroJava: theory Value
HOL-MicroJava: theory SystemClasses
HOL-MicroJava: theory TypeRel
HOL-MicroJava: theory Term
HOL-MicroJava: theory State
HOL-MicroJava: theory WellForm
HOL-MicroJava: theory Exceptions
HOL-MicroJava: theory JType
HOL-MicroJava: theory JVMType
HOL-MicroJava: theory WellType
HOL-MicroJava: theory Conform
HOL-MicroJava: theory Eval
HOL-MicroJava: theory TypeInf
HOL-MicroJava: theory JVMState
HOL-MicroJava: theory JVMInstructions
HOL-MicroJava: theory JVMExceptions
HOL-MicroJava: theory JVMExecInstr
HOL-MicroJava: theory Effect
HOL-MicroJava: theory JVMExec
HOL-MicroJava: theory DefsComp
HOL-MicroJava: theory JVMDefensive
HOL-MicroJava: theory Index
HOL-MicroJava: theory JVMListExample
HOL-MicroJava: theory TranslCompTp
HOL-MicroJava: theory Example
HOL-MicroJava: theory JListExample
HOL-MicroJava: theory JTypeSafe
HOL-MicroJava: theory TranslComp
HOL-MicroJava: theory LemmasComp
HOL-MicroJava: theory CorrComp
HOL-MicroJava: theory BVSpec
HOL-MicroJava: theory EffectMono
HOL-MicroJava: theory Altern
HOL-MicroJava: theory Correct
HOL-MicroJava: theory Typing_Framework_JVM
HOL-MicroJava: theory BVSpecTypeSafe
HOL-MicroJava: theory JVM
HOL-MicroJava: theory LBVJVM
HOL-MicroJava: theory CorrCompTp
HOL-MicroJava: theory BVNoTypeError
HOL-MicroJava: theory BVExample
HOL-MicroJava: theory MicroJava
Timing HOL-MicroJava (4 threads, 59.323s elapsed time, 228.707s cpu time, 9.546s GC time, factor 3.86)
Finished HOL-MicroJava (0:01:01 elapsed time, 0:03:50 cpu time, factor 3.77)
Running HOL-Probability ...
HOL-Probability: theory AList
HOL-Probability: theory DAList
HOL-Probability: theory Multiset
HOL-Probability: theory Permutation
HOL-Probability: theory Diagonal_Subsequence
HOL-Probability: theory Sigma_Algebra
HOL-Probability: theory Discrete_Topology
HOL-Probability: theory Measurable
HOL-Probability: theory Measure_Space
HOL-Probability: theory Borel_Space
HOL-Probability: theory Caratheodory
HOL-Probability: theory Lebesgue_Integration
HOL-Probability: theory Regularity
HOL-Probability: theory Binary_Product_Measure
HOL-Probability: theory Complete_Measure
HOL-Probability: theory Radon_Nikodym
HOL-Probability: theory Finite_Product_Measure
HOL-Probability: theory Fin_Map
HOL-Probability: theory Lebesgue_Measure
HOL-Probability: theory Probability_Measure
HOL-Probability: theory Distributions
HOL-Probability: theory Projective_Family
HOL-Probability: theory Infinite_Product_Measure
HOL-Probability: theory Independent_Family
HOL-Probability: theory Projective_Limit
HOL-Probability: theory Information
HOL-Probability: theory Dining_Cryptographers
HOL-Probability: theory Koepf_Duermuth_Countermeasure
HOL-Probability: theory Probability
Timing HOL-Probability (4 threads, 44.342s elapsed time, 166.684s cpu time, 5.890s GC time, factor 3.76)
Finished HOL-Probability (0:00:47 elapsed time, 0:02:49 cpu time, factor 3.59)
Running HOL-Proofs-Extraction ...
HOL-Proofs-Extraction: theory Adhoc_Overloading
HOL-Proofs-Extraction: theory AList
HOL-Proofs-Extraction: theory Code_Binary_Nat
HOL-Proofs-Extraction: theory Code_Natural
HOL-Proofs-Extraction: theory Fact
HOL-Proofs-Extraction: theory Code_Integer
HOL-Proofs-Extraction: theory Monad_Syntax
HOL-Proofs-Extraction: theory Parity
HOL-Proofs-Extraction: theory Efficient_Nat
HOL-Proofs-Extraction: theory State_Monad
HOL-Proofs-Extraction: theory DAList
HOL-Proofs-Extraction: theory Multiset
HOL-Proofs-Extraction: theory GCD
HOL-Proofs-Extraction: theory Primes
HOL-Proofs-Extraction: theory Cong
HOL-Proofs-Extraction: theory UniqueFactorization
HOL-Proofs-Extraction: theory Util
HOL-Proofs-Extraction: theory Higman
HOL-Proofs-Extraction: theory Warshall
HOL-Proofs-Extraction: theory Euclid
HOL-Proofs-Extraction: theory Pigeonhole
HOL-Proofs-Extraction: theory Higman_Extraction
HOL-Proofs-Extraction: theory QuotRem
HOL-Proofs-Extraction: theory Greatest_Common_Divisor
Timing HOL-Proofs-Extraction (4 threads, 117.962s elapsed time, 363.094s cpu time, 25.684s GC time, factor 3.08)
Finished HOL-Proofs-Extraction (0:02:00 elapsed time, 0:06:04 cpu time, factor 3.03)
Running HOL-SET_Protocol ...
HOL-SET_Protocol: theory Nat_Bijection
HOL-SET_Protocol: theory Message_SET
HOL-SET_Protocol: theory Event_SET
HOL-SET_Protocol: theory Public_SET
HOL-SET_Protocol: theory Cardholder_Registration
HOL-SET_Protocol: theory Merchant_Registration
HOL-SET_Protocol: theory Purchase
HOL-SET_Protocol: theory SET_Protocol
Timing HOL-SET_Protocol (4 threads, 20.884s elapsed time, 71.341s cpu time, 1.530s GC time, factor 3.42)
Finished HOL-SET_Protocol (0:00:23 elapsed time, 0:01:12 cpu time, factor 3.13)
Running HOL-UNITY ...
HOL-UNITY: theory Message
HOL-UNITY: theory Event
HOL-UNITY: theory Public
HOL-UNITY: theory AList
HOL-UNITY: theory ListOrder
HOL-UNITY: theory UNITY
HOL-UNITY: theory Constrains
HOL-UNITY: theory Deadlock
HOL-UNITY: theory FP
HOL-UNITY: theory Network
HOL-UNITY: theory WFair
HOL-UNITY: theory DAList
HOL-UNITY: theory SubstAx
HOL-UNITY: theory Token
HOL-UNITY: theory Detects
HOL-UNITY: theory Union
HOL-UNITY: theory Comp
HOL-UNITY: theory Multiset
HOL-UNITY: theory Guar
HOL-UNITY: theory Transformers
HOL-UNITY: theory Extend
HOL-UNITY: theory ProgressSets
HOL-UNITY: theory Project
HOL-UNITY: theory Rename
HOL-UNITY: theory Lift_prog
HOL-UNITY: theory Follows
HOL-UNITY: theory ELT
HOL-UNITY: theory PPROD
HOL-UNITY: theory UNITY_Main
HOL-UNITY: theory AllocBase
HOL-UNITY: theory Channel
HOL-UNITY: theory Common
HOL-UNITY: theory Counter
HOL-UNITY: theory Alloc
HOL-UNITY: theory AllocImpl
HOL-UNITY: theory Client
HOL-UNITY: theory Counterc
HOL-UNITY: theory Handshake
HOL-UNITY: theory Lift
HOL-UNITY: theory Mutex
HOL-UNITY: theory NSP_Bad
HOL-UNITY: theory PriorityAux
HOL-UNITY: theory Priority
HOL-UNITY: theory Progress
HOL-UNITY: theory Reach
HOL-UNITY: theory TimerArray
HOL-UNITY: theory Reachability
Timing HOL-UNITY (4 threads, 21.482s elapsed time, 77.205s cpu time, 3.652s GC time, factor 3.59)
Finished HOL-UNITY (0:00:23 elapsed time, 0:01:18 cpu time, factor 3.39)
Running ZF-UNITY ...
ZF-UNITY: theory Acc
ZF-UNITY: theory FoldSet
ZF-UNITY: theory GenPrefix
ZF-UNITY: theory State
ZF-UNITY: theory UNITY
ZF-UNITY: theory Multiset
ZF-UNITY: theory Constrains
ZF-UNITY: theory FP
ZF-UNITY: theory WFair
ZF-UNITY: theory SubstAx
ZF-UNITY: theory MultisetSum
ZF-UNITY: theory Monotonicity
ZF-UNITY: theory Mutex
ZF-UNITY: theory Union
ZF-UNITY: theory Increasing
ZF-UNITY: theory Follows
ZF-UNITY: theory Comp
ZF-UNITY: theory Guar
ZF-UNITY: theory AllocBase
ZF-UNITY: theory ClientImpl
ZF-UNITY: theory Distributor
ZF-UNITY: theory Merge
ZF-UNITY: theory AllocImpl
Timing ZF-UNITY (4 threads, 8.428s elapsed time, 31.854s cpu time, 1.178s GC time, factor 3.78)
Finished ZF-UNITY (0:00:09 elapsed time, 0:00:31 cpu time, factor 3.44)
Finished at Mon Feb 4 20:16:26 CET 2013
0:22:07 elapsed time, 1:14:19 cpu time, factor 3.36
*** m=5 q=2 ***
Started at Mon Feb 4 20:16:27 CET 2013 (polyml-5.5.0_x86-darwin on lri29-163.lri.fr)
ISABELLE_BUILD_OPTIONS="threads_trace=2 threads=5 parallel_proofs=2"
ML_PLATFORM="x86-darwin"
ML_HOME="/Volumes/Macintosh_HD/Users/makarius/.isabelle/contrib/polyml-5.5.0-3/x86-darwin"
ML_SYSTEM="polyml-5.5.0"
ML_OPTIONS="--minheap 1000 --gcthreads 5"
Session Pure
Session HOL (main)
Session HOL-Auth
Session HOL-Bali
Session HOL-Decision_Procs
Session HOL-Hoare_Parallel
Session HOL-IMP
Session HOL-Library (main)
Session HOL-MicroJava
Session HOL-Multivariate_Analysis (main)
Session HOL-Probability
Session HOL-Nominal (main)
Session HOL-Nominal-Examples
Session HOL-SET_Protocol
Session HOL-UNITY
Session HOL-Proofs
Session HOL-Proofs-Extraction
Session ZF (main)
Session ZF-UNITY
Building Pure ...
Finished Pure (0:00:09 elapsed time, 0:00:09 cpu time, factor 1.00)
Building HOL ...
HOL: theory Code_Generator
HOL: theory HOL
HOL: theory Orderings
HOL: theory SAT
HOL: theory Groups
HOL: theory Rings
HOL: theory Lattices
HOL: theory Set
HOL: theory Complete_Lattices
HOL: theory Typedef
HOL: theory Fun
HOL: theory Inductive
HOL: theory Fields
HOL: theory Product_Type
HOL: theory Sum_Type
HOL: theory Complete_Partial_Order
HOL: theory Nat
HOL: theory Datatype
HOL: theory Meson
HOL: theory Num
HOL: theory Option
HOL: theory Extraction
HOL: theory Partial_Function
HOL: theory ATP
HOL: theory Power
HOL: theory Metis
HOL: theory Finite_Set
HOL: theory Relation
HOL: theory Transitive_Closure
HOL: theory Wellfounded
HOL: theory FunDef
HOL: theory Plain
HOL: theory Big_Operators
HOL: theory Hilbert_Choice
HOL: theory Equiv_Relations
HOL: theory Transfer
HOL: theory Lifting
HOL: theory Quotient
HOL: theory Int
HOL: theory Nat_Transfer
HOL: theory Divides
HOL: theory Set_Interval
HOL: theory Code_Numeral
HOL: theory Numeral_Simprocs
HOL: theory Semiring_Normalization
HOL: theory Groebner_Basis
HOL: theory Presburger
HOL: theory List
HOL: theory Map
HOL: theory Predicate
HOL: theory Random
HOL: theory Enum
HOL: theory Lazy_Sequence
HOL: theory String
HOL: theory DSequence
HOL: theory New_DSequence
HOL: theory Typerep
HOL: theory Code_Evaluation
HOL: theory Quickcheck
HOL: theory Quickcheck_Exhaustive
HOL: theory Random_Sequence
HOL: theory New_Random_Sequence
HOL: theory Quickcheck_Narrowing
HOL: theory Predicate_Compile
HOL: theory Record
HOL: theory SMT
HOL: theory Sledgehammer
HOL: theory Nitpick
HOL: theory Main
HOL: theory Archimedean_Field
HOL: theory Lubs
HOL: theory Fact
HOL: theory Parity
HOL: theory GCD
HOL: theory Rat
HOL: theory RealDef
HOL: theory RComplete
HOL: theory RealVector
HOL: theory SupInf
HOL: theory Real
HOL: theory Limits
HOL: theory SEQ
HOL: theory Lim
HOL: theory Deriv
HOL: theory Series
HOL: theory NthRoot
HOL: theory Transcendental
HOL: theory Complex
HOL: theory Ln
HOL: theory Log
HOL: theory MacLaurin
HOL: theory Taylor
HOL: theory Complex_Main
Timing HOL (5 threads, 87.723s elapsed time, 234.006s cpu time, 20.155s GC time, factor 2.67)
Finished HOL (0:01:49 elapsed time, 0:04:33 cpu time, factor 2.50)
Building HOL-Multivariate_Analysis ...
HOL-Multivariate_Analysis: theory Indicator_Function
HOL-Multivariate_Analysis: theory FuncSet
HOL-Multivariate_Analysis: theory Extended_Nat
HOL-Multivariate_Analysis: theory Infinite_Set
HOL-Multivariate_Analysis: theory Glbs
HOL-Multivariate_Analysis: theory Nat_Bijection
HOL-Multivariate_Analysis: theory L2_Norm
HOL-Multivariate_Analysis: theory FrechetDeriv
HOL-Multivariate_Analysis: theory Sum_of_Squares
HOL-Multivariate_Analysis: theory Inner_Product
HOL-Multivariate_Analysis: theory Permutations
HOL-Multivariate_Analysis: theory Countable
HOL-Multivariate_Analysis: theory Extended_Real
HOL-Multivariate_Analysis: theory Phantom_Type
HOL-Multivariate_Analysis: theory Product_plus
HOL-Multivariate_Analysis: theory Product_Vector
HOL-Multivariate_Analysis: theory Countable_Set
HOL-Multivariate_Analysis: theory Cardinality
HOL-Multivariate_Analysis: theory Convex
HOL-Multivariate_Analysis: theory Euclidean_Space
HOL-Multivariate_Analysis: theory Set_Algebras
HOL-Multivariate_Analysis: theory Norm_Arith
HOL-Multivariate_Analysis: theory Numeral_Type
HOL-Multivariate_Analysis: theory Linear_Algebra
HOL-Multivariate_Analysis: theory Finite_Cartesian_Product
HOL-Multivariate_Analysis: theory Operator_Norm
HOL-Multivariate_Analysis: theory Topology_Euclidean_Space
HOL-Multivariate_Analysis: theory Extended_Real_Limits
HOL-Multivariate_Analysis: theory Convex_Euclidean_Space
HOL-Multivariate_Analysis: theory Brouwer_Fixpoint
HOL-Multivariate_Analysis: theory Path_Connected
HOL-Multivariate_Analysis: theory Derivative
HOL-Multivariate_Analysis: theory Integration
HOL-Multivariate_Analysis: theory Cartesian_Euclidean_Space
HOL-Multivariate_Analysis: theory Determinants
HOL-Multivariate_Analysis: theory Fashoda
HOL-Multivariate_Analysis: theory Multivariate_Analysis
Timing HOL-Multivariate_Analysis (5 threads, 39.456s elapsed time, 189.789s cpu time, 8.308s GC time, factor 4.81)
Finished HOL-Multivariate_Analysis (0:00:54 elapsed time, 0:03:30 cpu time, factor 3.88)
Building HOL-Nominal ...
HOL-Nominal: theory Infinite_Set
HOL-Nominal: theory Nominal
Timing HOL-Nominal (5 threads, 4.311s elapsed time, 9.156s cpu time, 0.430s GC time, factor 2.12)
Finished HOL-Nominal (0:00:15 elapsed time, 0:00:20 cpu time, factor 1.33)
Building HOL-Proofs ...
HOL-Proofs: theory Code_Generator
HOL-Proofs: theory HOL
HOL-Proofs: theory Orderings
HOL-Proofs: theory SAT
HOL-Proofs: theory Groups
HOL-Proofs: theory Rings
HOL-Proofs: theory Lattices
HOL-Proofs: theory Set
HOL-Proofs: theory Complete_Lattices
HOL-Proofs: theory Typedef
HOL-Proofs: theory Fun
HOL-Proofs: theory Inductive
HOL-Proofs: theory Fields
HOL-Proofs: theory Product_Type
HOL-Proofs: theory Sum_Type
HOL-Proofs: theory Complete_Partial_Order
HOL-Proofs: theory Nat
HOL-Proofs: theory Datatype
HOL-Proofs: theory Meson
HOL-Proofs: theory Num
HOL-Proofs: theory Option
HOL-Proofs: theory ATP
HOL-Proofs: theory Extraction
HOL-Proofs: theory Partial_Function
HOL-Proofs: theory Metis
HOL-Proofs: theory Power
HOL-Proofs: theory Finite_Set
HOL-Proofs: theory Relation
HOL-Proofs: theory Transitive_Closure
HOL-Proofs: theory Wellfounded
HOL-Proofs: theory FunDef
HOL-Proofs: theory Plain
HOL-Proofs: theory Big_Operators
HOL-Proofs: theory Hilbert_Choice
HOL-Proofs: theory Equiv_Relations
HOL-Proofs: theory Transfer
HOL-Proofs: theory Lifting
HOL-Proofs: theory Quotient
HOL-Proofs: theory Int
HOL-Proofs: theory Nat_Transfer
HOL-Proofs: theory Divides
HOL-Proofs: theory Set_Interval
HOL-Proofs: theory Code_Numeral
HOL-Proofs: theory Numeral_Simprocs
HOL-Proofs: theory Semiring_Normalization
HOL-Proofs: theory Groebner_Basis
HOL-Proofs: theory Presburger
HOL-Proofs: theory List
HOL-Proofs: theory Map
HOL-Proofs: theory Predicate
HOL-Proofs: theory Random
HOL-Proofs: theory Enum
HOL-Proofs: theory Lazy_Sequence
HOL-Proofs: theory String
HOL-Proofs: theory DSequence
HOL-Proofs: theory New_DSequence
HOL-Proofs: theory Typerep
HOL-Proofs: theory Code_Evaluation
HOL-Proofs: theory Quickcheck
HOL-Proofs: theory Quickcheck_Exhaustive
HOL-Proofs: theory Random_Sequence
HOL-Proofs: theory New_Random_Sequence
HOL-Proofs: theory Quickcheck_Narrowing
HOL-Proofs: theory Predicate_Compile
HOL-Proofs: theory Record
HOL-Proofs: theory SMT
HOL-Proofs: theory Sledgehammer
HOL-Proofs: theory Nitpick
HOL-Proofs: theory Main
Timing HOL-Proofs (5 threads, 135.580s elapsed time, 535.672s cpu time, 51.111s GC time, factor 3.95)
Finished HOL-Proofs (0:02:46 elapsed time, 0:09:52 cpu time, factor 3.56)
Building ZF ...
ZF: theory IFOL
ZF: theory FOL
ZF: theory ZF
ZF: theory upair
ZF: theory pair
ZF: theory Bool
ZF: theory equalities
ZF: theory Fixedpt
ZF: theory Sum
ZF: theory func
ZF: theory Perm
ZF: theory QPair
ZF: theory Trancl
ZF: theory EquivClass
ZF: theory WF
ZF: theory Order
ZF: theory Ordinal
ZF: theory OrdQuant
ZF: theory OrderArith
ZF: theory Nat_ZF
ZF: theory Epsilon
ZF: theory OrderType
ZF: theory Inductive_ZF
ZF: theory Finite
ZF: theory Cardinal
ZF: theory Univ
ZF: theory Arith
ZF: theory QUniv
ZF: theory Datatype_ZF
ZF: theory ArithSimp
ZF: theory Int_ZF
ZF: theory CardinalArith
ZF: theory List_ZF
ZF: theory Bin
ZF: theory IntArith
ZF: theory IntDiv_ZF
ZF: theory Main_ZF
ZF: theory AC
ZF: theory Main
ZF: theory Zorn
ZF: theory Cardinal_AC
ZF: theory InfDatatype
ZF: theory Main_ZFC
Timing ZF (5 threads, 7.928s elapsed time, 28.425s cpu time, 1.788s GC time, factor 3.59)
Finished ZF (0:00:11 elapsed time, 0:00:32 cpu time, factor 2.90)
Running HOL-Nominal-Examples ...
HOL-Nominal-Examples: theory CK_Machine
HOL-Nominal-Examples: theory CR_Takahashi
HOL-Nominal-Examples: theory Class1
HOL-Nominal-Examples: theory Compile
HOL-Nominal-Examples: theory Contexts
HOL-Nominal-Examples: theory Crary
HOL-Nominal-Examples: theory Fsub
HOL-Nominal-Examples: theory Height
HOL-Nominal-Examples: theory Lam_Funs
HOL-Nominal-Examples: theory Lambda_mu
HOL-Nominal-Examples: theory LocalWeakening
HOL-Nominal-Examples: theory Pattern
HOL-Nominal-Examples: theory CR
HOL-Nominal-Examples: theory SN
HOL-Nominal-Examples: theory SOS
HOL-Nominal-Examples: theory Standardization
HOL-Nominal-Examples: theory Support
HOL-Nominal-Examples: theory Type_Preservation
HOL-Nominal-Examples: theory W
HOL-Nominal-Examples: theory Weakening
HOL-Nominal-Examples: theory Class2
HOL-Nominal-Examples: theory Class3
HOL-Nominal-Examples: theory Nominal_Examples
HOL-Nominal-Examples: theory VC_Condition
Timing HOL-Nominal-Examples (5 threads, 117.119s elapsed time, 563.985s cpu time, 33.102s GC time, factor 4.82)
Finished HOL-Nominal-Examples (0:02:00 elapsed time, 0:09:26 cpu time, factor 4.71)
Running HOL-Auth ...
HOL-Auth: theory Message
HOL-Auth: theory Nat_Bijection
HOL-Auth: theory All_Symmetric
HOL-Auth: theory Event
HOL-Auth: theory EventSC
HOL-Auth: theory Extensions
HOL-Auth: theory Public
HOL-Auth: theory Shared
HOL-Auth: theory CertifiedEmail
HOL-Auth: theory KerberosIV
HOL-Auth: theory Analz
HOL-Auth: theory List_Msg
HOL-Auth: theory KerberosIV_Gets
HOL-Auth: theory KerberosV
HOL-Auth: theory Guard
HOL-Auth: theory GuardK
HOL-Auth: theory Guard_Public
HOL-Auth: theory Kerberos_BAN
HOL-Auth: theory Kerberos_BAN_Gets
HOL-Auth: theory Guard_NS_Public
HOL-Auth: theory Proto
HOL-Auth: theory NS_Public
HOL-Auth: theory NS_Public_Bad
HOL-Auth: theory P2
HOL-Auth: theory NS_Shared
HOL-Auth: theory OtwayRees
HOL-Auth: theory OtwayReesBella
HOL-Auth: theory OtwayRees_AN
HOL-Auth: theory OtwayRees_Bad
HOL-Auth: theory P1
HOL-Auth: theory Recur
HOL-Auth: theory WooLam
HOL-Auth: theory Yahalom
HOL-Auth: theory Yahalom2
HOL-Auth: theory Yahalom_Bad
HOL-Auth: theory ZhouGollmann
HOL-Auth: theory Guard_Shared
HOL-Auth: theory Smartcard
HOL-Auth: theory Guard_OtwayRees
HOL-Auth: theory Guard_Yahalom
HOL-Auth: theory Auth_Shared
HOL-Auth: theory ShoupRubin
HOL-Auth: theory Auth_Guard_Shared
HOL-Auth: theory ShoupRubinBella
HOL-Auth: theory TLS
HOL-Auth: theory Auth_Smartcard
HOL-Auth: theory Auth_Public
HOL-Auth: theory Auth_Guard_Public
Timing HOL-Auth (5 threads, 53.794s elapsed time, 242.635s cpu time, 12.319s GC time, factor 4.51)
Finished HOL-Auth (0:00:56 elapsed time, 0:04:03 cpu time, factor 4.33)
Running HOL-Bali ...
HOL-Bali: theory Wfrec
HOL-Bali: theory Old_Recdef
HOL-Bali: theory Basis
HOL-Bali: theory Name
HOL-Bali: theory Table
HOL-Bali: theory Type
HOL-Bali: theory Value
HOL-Bali: theory Term
HOL-Bali: theory Decl
HOL-Bali: theory TypeRel
HOL-Bali: theory DeclConcepts
HOL-Bali: theory State
HOL-Bali: theory WellType
HOL-Bali: theory Conform
HOL-Bali: theory Eval
HOL-Bali: theory DefiniteAssignment
HOL-Bali: theory WellForm
HOL-Bali: theory DefiniteAssignmentCorrect
HOL-Bali: theory Example
HOL-Bali: theory TypeSafe
HOL-Bali: theory Evaln
HOL-Bali: theory AxSem
HOL-Bali: theory Trans
HOL-Bali: theory AxCompl
HOL-Bali: theory AxSound
HOL-Bali: theory AxExample
Timing HOL-Bali (5 threads, 46.342s elapsed time, 156.760s cpu time, 7.514s GC time, factor 3.38)
Finished HOL-Bali (0:00:48 elapsed time, 0:02:37 cpu time, factor 3.27)
Running HOL-Decision_Procs ...
HOL-Decision_Procs: theory Code_Natural
HOL-Decision_Procs: theory DP_Library
HOL-Decision_Procs: theory Code_Binary_Nat
HOL-Decision_Procs: theory Dense_Linear_Order
HOL-Decision_Procs: theory Commutative_Ring
HOL-Decision_Procs: theory Code_Integer
HOL-Decision_Procs: theory Abstract_Rat
HOL-Decision_Procs: theory Lattice_Algebras
HOL-Decision_Procs: theory Efficient_Nat
HOL-Decision_Procs: theory Polynomial_List
HOL-Decision_Procs: theory Reflection
HOL-Decision_Procs: theory Wfrec
HOL-Decision_Procs: theory Old_Recdef
HOL-Decision_Procs: theory Reflected_Multivariate_Polynomial
HOL-Decision_Procs: theory Cooper
HOL-Decision_Procs: theory Dense_Linear_Order_Ex
HOL-Decision_Procs: theory Ferrack
HOL-Decision_Procs: theory Commutative_Ring_Complete
HOL-Decision_Procs: theory Commutative_Ring_Ex
HOL-Decision_Procs: theory Float
HOL-Decision_Procs: theory MIR
HOL-Decision_Procs: theory Approximation
HOL-Decision_Procs: theory Parametric_Ferrante_Rackoff
HOL-Decision_Procs: theory Approximation_Ex
HOL-Decision_Procs: theory Decision_Procs
Timing HOL-Decision_Procs (5 threads, 91.333s elapsed time, 443.530s cpu time, 23.211s GC time, factor 4.86)
Finished HOL-Decision_Procs (0:01:33 elapsed time, 0:07:25 cpu time, factor 4.78)
Running HOL-Hoare_Parallel ...
HOL-Hoare_Parallel: theory Graph
HOL-Hoare_Parallel: theory Quote_Antiquote
HOL-Hoare_Parallel: theory OG_Com
HOL-Hoare_Parallel: theory RG_Com
HOL-Hoare_Parallel: theory RG_Tran
HOL-Hoare_Parallel: theory RG_Hoare
HOL-Hoare_Parallel: theory OG_Tran
HOL-Hoare_Parallel: theory RG_Syntax
HOL-Hoare_Parallel: theory RG_Examples
HOL-Hoare_Parallel: theory OG_Hoare
HOL-Hoare_Parallel: theory OG_Tactics
HOL-Hoare_Parallel: theory OG_Syntax
HOL-Hoare_Parallel: theory Gar_Coll
HOL-Hoare_Parallel: theory Mul_Gar_Coll
HOL-Hoare_Parallel: theory OG_Examples
HOL-Hoare_Parallel: theory Hoare_Parallel
Timing HOL-Hoare_Parallel (5 threads, 47.834s elapsed time, 227.908s cpu time, 4.866s GC time, factor 4.76)
Finished HOL-Hoare_Parallel (0:00:49 elapsed time, 0:03:49 cpu time, factor 4.67)
Running HOL-IMP ...
HOL-IMP: theory Char_nat
HOL-IMP: theory List_lexord
HOL-IMP: theory While_Combinator
HOL-IMP: theory Interpretation_with_Defs
HOL-IMP: theory Char_ord
HOL-IMP: theory AExp
HOL-IMP: theory C_like
HOL-IMP: theory Complete_Lattice
HOL-IMP: theory Complete_Lattice_ix
HOL-IMP: theory OO
HOL-IMP: theory Star
HOL-IMP: theory Types
HOL-IMP: theory Poly_Types
HOL-IMP: theory ASM
HOL-IMP: theory BExp
HOL-IMP: theory Com
HOL-IMP: theory Vars
HOL-IMP: theory Procs
HOL-IMP: theory ACom
HOL-IMP: theory ACom_ITP
HOL-IMP: theory Abs_Int_Tests
HOL-IMP: theory Big_Step
HOL-IMP: theory Procs_Dyn_Vars_Dyn
HOL-IMP: theory Procs_Stat_Vars_Dyn
HOL-IMP: theory Procs_Stat_Vars_Stat
HOL-IMP: theory Compiler
HOL-IMP: theory Denotation
HOL-IMP: theory Hoare
HOL-IMP: theory Hoare_Examples
HOL-IMP: theory Hoare_Sound_Complete
HOL-IMP: theory VC
HOL-IMP: theory HoareT
HOL-IMP: theory Sec_Type_Expr
HOL-IMP: theory Sec_Typing
HOL-IMP: theory Sec_TypingT
HOL-IMP: theory Sem_Equiv
HOL-IMP: theory Def_Init
HOL-IMP: theory Fold
HOL-IMP: theory Def_Init_Exp
HOL-IMP: theory Live
HOL-IMP: theory Def_Init_Big
HOL-IMP: theory Collecting
HOL-IMP: theory Def_Init_Sound_Big
HOL-IMP: theory Collecting_ITP
HOL-IMP: theory Def_Init_Small
HOL-IMP: theory Def_Init_Sound_Small
HOL-IMP: theory Small_Step
HOL-IMP: theory Live_True
HOL-IMP: theory Abs_Int_den0_fun
HOL-IMP: theory Finite_Reachable
HOL-IMP: theory Abs_Int0_ITP
HOL-IMP: theory Abs_State_den
HOL-IMP: theory Collecting1
HOL-IMP: theory Collecting_Examples
HOL-IMP: theory Abs_Int_init
HOL-IMP: theory Abs_Int_den0
HOL-IMP: theory Abs_Int0
HOL-IMP: theory Abs_Int_den0_const
HOL-IMP: theory Comp_Rev
HOL-IMP: theory Abs_State_ITP
HOL-IMP: theory Abs_State
HOL-IMP: theory Abs_Int1_ITP
HOL-IMP: theory Abs_Int1_const_ITP
HOL-IMP: theory Abs_Int1_parity_ITP
HOL-IMP: theory Abs_Int2_ITP
HOL-IMP: theory Abs_Int_den1
HOL-IMP: theory Abs_Int1
HOL-IMP: theory Abs_Int2_ivl_ITP
HOL-IMP: theory Abs_Int1_const
HOL-IMP: theory Abs_Int_den1_ivl
HOL-IMP: theory Abs_Int1_parity
HOL-IMP: theory Abs_Int2
HOL-IMP: theory Abs_Int2_ivl
HOL-IMP: theory Abs_Int_den2
HOL-IMP: theory Abs_Int3_ITP
HOL-IMP: theory Abs_Int3
Timing HOL-IMP (5 threads, 111.899s elapsed time, 489.116s cpu time, 45.730s GC time, factor 4.37)
Finished HOL-IMP (0:01:54 elapsed time, 0:08:11 cpu time, factor 4.30)
Running HOL-Library ...
HOL-Library: theory Adhoc_Overloading
HOL-Library: theory Lattice_Syntax
HOL-Library: theory Preorder
HOL-Library: theory Refute
HOL-Library: theory AList
HOL-Library: theory Bit
HOL-Library: theory Boolean_Algebra
HOL-Library: theory Char_nat
HOL-Library: theory Char_ord
HOL-Library: theory Code_Binary_Nat
HOL-Library: theory Code_Char
HOL-Library: theory Code_Natural
HOL-Library: theory Code_Numeral_Types
HOL-Library: theory Code_Char_ord
HOL-Library: theory Code_Integer
HOL-Library: theory Continuity
HOL-Library: theory Debug
HOL-Library: theory Code_Char_chr
HOL-Library: theory Dlist
HOL-Library: theory Efficient_Nat
HOL-Library: theory Eval_Witness
HOL-Library: theory Extended_Nat
HOL-Library: theory IArray
HOL-Library: theory Fraction_Field
HOL-Library: theory DAList
HOL-Library: theory FuncSet
HOL-Library: theory Function_Algebras
HOL-Library: theory Code_Target_Int
HOL-Library: theory Code_Target_Nat
HOL-Library: theory Function_Division
HOL-Library: theory Indicator_Function
HOL-Library: theory Infinite_Set
HOL-Library: theory Kleene_Algebra
HOL-Library: theory Code_Target_Numeral
HOL-Library: theory LaTeXsugar
HOL-Library: theory ListVector
HOL-Library: theory List_lexord
HOL-Library: theory Monad_Syntax
HOL-Library: theory Multiset
HOL-Library: theory Option_ord
HOL-Library: theory Order_Relation
HOL-Library: theory Parallel
HOL-Library: theory Zorn
HOL-Library: theory Diagonal_Subsequence
HOL-Library: theory Nat_Bijection
HOL-Library: theory Abstract_Rat
HOL-Library: theory Binomial
HOL-Library: theory Code_Real_Approx_By_Float
HOL-Library: theory ContNotDenum
HOL-Library: theory Countable
HOL-Library: theory Formal_Power_Series
HOL-Library: theory FrechetDeriv
HOL-Library: theory Inner_Product
HOL-Library: theory Countable_Set
HOL-Library: theory Lattice_Algebras
HOL-Library: theory OptionalSugar
HOL-Library: theory Sum_of_Squares
HOL-Library: theory Permutations
HOL-Library: theory Permutation
HOL-Library: theory Phantom_Type
HOL-Library: theory Polynomial
HOL-Library: theory Cardinality
HOL-Library: theory FinFun
HOL-Library: theory Numeral_Type
HOL-Library: theory Fundamental_Theorem_Algebra
HOL-Library: theory Poly_Deriv
HOL-Library: theory Float
HOL-Library: theory Type_Length
HOL-Library: theory Product_plus
HOL-Library: theory Quotient_Syntax
HOL-Library: theory Quotient_Option
HOL-Library: theory Product_Lattice
HOL-Library: theory Product_Vector
HOL-Library: theory Finite_Lattice
HOL-Library: theory Mapping
HOL-Library: theory Convex
HOL-Library: theory Quotient_Product
HOL-Library: theory Quotient_Set
HOL-Library: theory Quotient_Sum
HOL-Library: theory AList_Mapping
HOL-Library: theory Quotient_List
HOL-Library: theory Quotient_Type
HOL-Library: theory RBT_Impl
HOL-Library: theory Ramsey
HOL-Library: theory Reflection
HOL-Library: theory Saturated
HOL-Library: theory Set_Algebras
HOL-Library: theory State_Monad
HOL-Library: theory Sublist
HOL-Library: theory Transitive_Closure_Table
HOL-Library: theory BigO
HOL-Library: theory Univ_Poly
HOL-Library: theory Sublist_Order
HOL-Library: theory Wfrec
HOL-Library: theory Old_Recdef
HOL-Library: theory While_Combinator
HOL-Library: theory RBT
HOL-Library: theory RBT_Mapping
HOL-Library: theory Library
Skipping theories "Sum_of_Squares_Remote" (undefined ISABELLE_FULL_TEST)
Timing HOL-Library (5 threads, 53.444s elapsed time, 247.286s cpu time, 20.341s GC time, factor 4.63)
Finished HOL-Library (0:00:55 elapsed time, 0:04:08 cpu time, factor 4.50)
Running HOL-MicroJava ...
HOL-MicroJava: theory While_Combinator
HOL-MicroJava: theory Wfrec
HOL-MicroJava: theory Transitive_Closure_Table
HOL-MicroJava: theory Semilat
HOL-MicroJava: theory Err
HOL-MicroJava: theory Listn
HOL-MicroJava: theory Opt
HOL-MicroJava: theory Product
HOL-MicroJava: theory JBasis
HOL-MicroJava: theory AuxLemmas
HOL-MicroJava: theory Type
HOL-MicroJava: theory Typing_Framework
HOL-MicroJava: theory Semilattices
HOL-MicroJava: theory SemilatAlg
HOL-MicroJava: theory Kildall
HOL-MicroJava: theory LBVSpec
HOL-MicroJava: theory Typing_Framework_err
HOL-MicroJava: theory LBVComplete
HOL-MicroJava: theory LBVCorrect
HOL-MicroJava: theory Abstract_BV
HOL-MicroJava: theory Decl
HOL-MicroJava: theory Value
HOL-MicroJava: theory SystemClasses
HOL-MicroJava: theory TypeRel
HOL-MicroJava: theory Term
HOL-MicroJava: theory State
HOL-MicroJava: theory WellForm
HOL-MicroJava: theory Exceptions
HOL-MicroJava: theory JType
HOL-MicroJava: theory JVMType
HOL-MicroJava: theory WellType
HOL-MicroJava: theory Conform
HOL-MicroJava: theory Eval
HOL-MicroJava: theory TypeInf
HOL-MicroJava: theory JVMState
HOL-MicroJava: theory JVMInstructions
HOL-MicroJava: theory JVMExceptions
HOL-MicroJava: theory JVMExecInstr
HOL-MicroJava: theory Effect
HOL-MicroJava: theory JVMExec
HOL-MicroJava: theory DefsComp
HOL-MicroJava: theory JVMDefensive
HOL-MicroJava: theory Index
HOL-MicroJava: theory JVMListExample
HOL-MicroJava: theory TranslCompTp
HOL-MicroJava: theory TranslComp
HOL-MicroJava: theory LemmasComp
HOL-MicroJava: theory Example
HOL-MicroJava: theory JListExample
HOL-MicroJava: theory JTypeSafe
HOL-MicroJava: theory CorrComp
HOL-MicroJava: theory BVSpec
HOL-MicroJava: theory EffectMono
HOL-MicroJava: theory Altern
HOL-MicroJava: theory Correct
HOL-MicroJava: theory Typing_Framework_JVM
HOL-MicroJava: theory BVSpecTypeSafe
HOL-MicroJava: theory JVM
HOL-MicroJava: theory LBVJVM
HOL-MicroJava: theory CorrCompTp
HOL-MicroJava: theory BVNoTypeError
HOL-MicroJava: theory BVExample
HOL-MicroJava: theory MicroJava
Timing HOL-MicroJava (5 threads, 50.135s elapsed time, 232.335s cpu time, 10.160s GC time, factor 4.63)
Finished HOL-MicroJava (0:00:52 elapsed time, 0:03:53 cpu time, factor 4.48)
Running HOL-Probability ...
HOL-Probability: theory AList
HOL-Probability: theory DAList
HOL-Probability: theory Multiset
HOL-Probability: theory Permutation
HOL-Probability: theory Sigma_Algebra
HOL-Probability: theory Diagonal_Subsequence
HOL-Probability: theory Discrete_Topology
HOL-Probability: theory Measurable
HOL-Probability: theory Measure_Space
HOL-Probability: theory Borel_Space
HOL-Probability: theory Caratheodory
HOL-Probability: theory Lebesgue_Integration
HOL-Probability: theory Regularity
HOL-Probability: theory Binary_Product_Measure
HOL-Probability: theory Complete_Measure
HOL-Probability: theory Radon_Nikodym
HOL-Probability: theory Finite_Product_Measure
HOL-Probability: theory Fin_Map
HOL-Probability: theory Lebesgue_Measure
HOL-Probability: theory Probability_Measure
HOL-Probability: theory Distributions
HOL-Probability: theory Projective_Family
HOL-Probability: theory Infinite_Product_Measure
HOL-Probability: theory Independent_Family
HOL-Probability: theory Projective_Limit
HOL-Probability: theory Information
HOL-Probability: theory Dining_Cryptographers
HOL-Probability: theory Koepf_Duermuth_Countermeasure
HOL-Probability: theory Probability
Timing HOL-Probability (5 threads, 37.726s elapsed time, 169.851s cpu time, 6.391s GC time, factor 4.50)
Finished HOL-Probability (0:00:41 elapsed time, 0:02:52 cpu time, factor 4.19)
Running HOL-Proofs-Extraction ...
HOL-Proofs-Extraction: theory Adhoc_Overloading
HOL-Proofs-Extraction: theory AList
HOL-Proofs-Extraction: theory Code_Binary_Nat
HOL-Proofs-Extraction: theory Code_Natural
HOL-Proofs-Extraction: theory Fact
HOL-Proofs-Extraction: theory Monad_Syntax
HOL-Proofs-Extraction: theory Code_Integer
HOL-Proofs-Extraction: theory Parity
HOL-Proofs-Extraction: theory State_Monad
HOL-Proofs-Extraction: theory Efficient_Nat
HOL-Proofs-Extraction: theory DAList
HOL-Proofs-Extraction: theory Multiset
HOL-Proofs-Extraction: theory GCD
HOL-Proofs-Extraction: theory Primes
HOL-Proofs-Extraction: theory Cong
HOL-Proofs-Extraction: theory UniqueFactorization
HOL-Proofs-Extraction: theory Higman
HOL-Proofs-Extraction: theory Warshall
HOL-Proofs-Extraction: theory Util
HOL-Proofs-Extraction: theory Euclid
HOL-Proofs-Extraction: theory Pigeonhole
HOL-Proofs-Extraction: theory QuotRem
HOL-Proofs-Extraction: theory Higman_Extraction
HOL-Proofs-Extraction: theory Greatest_Common_Divisor
Timing HOL-Proofs-Extraction (5 threads, 107.726s elapsed time, 370.197s cpu time, 28.284s GC time, factor 3.44)
Finished HOL-Proofs-Extraction (0:01:50 elapsed time, 0:06:11 cpu time, factor 3.37)
Running HOL-SET_Protocol ...
HOL-SET_Protocol: theory Nat_Bijection
HOL-SET_Protocol: theory Message_SET
HOL-SET_Protocol: theory Event_SET
HOL-SET_Protocol: theory Public_SET
HOL-SET_Protocol: theory Cardholder_Registration
HOL-SET_Protocol: theory Merchant_Registration
HOL-SET_Protocol: theory Purchase
HOL-SET_Protocol: theory SET_Protocol
Timing HOL-SET_Protocol (5 threads, 17.862s elapsed time, 72.772s cpu time, 1.630s GC time, factor 4.07)
Finished HOL-SET_Protocol (0:00:19 elapsed time, 0:01:14 cpu time, factor 3.89)
Running HOL-UNITY ...
HOL-UNITY: theory Message
HOL-UNITY: theory Event
HOL-UNITY: theory Public
HOL-UNITY: theory AList
HOL-UNITY: theory ListOrder
HOL-UNITY: theory UNITY
HOL-UNITY: theory Constrains
HOL-UNITY: theory Deadlock
HOL-UNITY: theory FP
HOL-UNITY: theory Network
HOL-UNITY: theory WFair
HOL-UNITY: theory DAList
HOL-UNITY: theory SubstAx
HOL-UNITY: theory Token
HOL-UNITY: theory Detects
HOL-UNITY: theory Union
HOL-UNITY: theory Comp
HOL-UNITY: theory Multiset
HOL-UNITY: theory Guar
HOL-UNITY: theory Transformers
HOL-UNITY: theory Extend
HOL-UNITY: theory ProgressSets
HOL-UNITY: theory Project
HOL-UNITY: theory Rename
HOL-UNITY: theory Lift_prog
HOL-UNITY: theory ELT
HOL-UNITY: theory PPROD
HOL-UNITY: theory Follows
HOL-UNITY: theory UNITY_Main
HOL-UNITY: theory AllocBase
HOL-UNITY: theory Channel
HOL-UNITY: theory Common
HOL-UNITY: theory Counter
HOL-UNITY: theory Counterc
HOL-UNITY: theory Alloc
HOL-UNITY: theory AllocImpl
HOL-UNITY: theory Client
HOL-UNITY: theory Handshake
HOL-UNITY: theory Lift
HOL-UNITY: theory Mutex
HOL-UNITY: theory NSP_Bad
HOL-UNITY: theory PriorityAux
HOL-UNITY: theory Progress
HOL-UNITY: theory Reach
HOL-UNITY: theory Priority
HOL-UNITY: theory TimerArray
HOL-UNITY: theory Reachability
Timing HOL-UNITY (5 threads, 17.572s elapsed time, 74.398s cpu time, 3.761s GC time, factor 4.23)
Finished HOL-UNITY (0:00:19 elapsed time, 0:01:15 cpu time, factor 3.94)
Running ZF-UNITY ...
ZF-UNITY: theory Acc
ZF-UNITY: theory FoldSet
ZF-UNITY: theory GenPrefix
ZF-UNITY: theory State
ZF-UNITY: theory UNITY
ZF-UNITY: theory Multiset
ZF-UNITY: theory Constrains
ZF-UNITY: theory FP
ZF-UNITY: theory WFair
ZF-UNITY: theory SubstAx
ZF-UNITY: theory MultisetSum
ZF-UNITY: theory Monotonicity
ZF-UNITY: theory Mutex
ZF-UNITY: theory Increasing
ZF-UNITY: theory Union
ZF-UNITY: theory Follows
ZF-UNITY: theory Comp
ZF-UNITY: theory Guar
ZF-UNITY: theory AllocBase
ZF-UNITY: theory ClientImpl
ZF-UNITY: theory Distributor
ZF-UNITY: theory Merge
ZF-UNITY: theory AllocImpl
Timing ZF-UNITY (5 threads, 7.104s elapsed time, 32.614s cpu time, 1.246s GC time, factor 4.59)
Finished ZF-UNITY (0:00:08 elapsed time, 0:00:32 cpu time, factor 4.00)
Finished at Mon Feb 4 20:35:50 CET 2013
0:19:23 elapsed time, 1:15:24 cpu time, factor 3.88
*** m=6 q=2 ***
Started at Mon Feb 4 20:35:51 CET 2013 (polyml-5.5.0_x86-darwin on lri29-163.lri.fr)
ISABELLE_BUILD_OPTIONS="threads_trace=2 threads=6 parallel_proofs=2"
ML_PLATFORM="x86-darwin"
ML_HOME="/Volumes/Macintosh_HD/Users/makarius/.isabelle/contrib/polyml-5.5.0-3/x86-darwin"
ML_SYSTEM="polyml-5.5.0"
ML_OPTIONS="--minheap 1000 --gcthreads 6"
Session Pure
Session HOL (main)
Session HOL-Auth
Session HOL-Bali
Session HOL-Decision_Procs
Session HOL-Hoare_Parallel
Session HOL-IMP
Session HOL-Library (main)
Session HOL-MicroJava
Session HOL-Multivariate_Analysis (main)
Session HOL-Probability
Session HOL-Nominal (main)
Session HOL-Nominal-Examples
Session HOL-SET_Protocol
Session HOL-UNITY
Session HOL-Proofs
Session HOL-Proofs-Extraction
Session ZF (main)
Session ZF-UNITY
Building Pure ...
Finished Pure (0:00:09 elapsed time, 0:00:10 cpu time, factor 1.11)
Building HOL ...
HOL: theory Code_Generator
HOL: theory HOL
HOL: theory Orderings
HOL: theory SAT
HOL: theory Groups
HOL: theory Rings
HOL: theory Lattices
HOL: theory Set
HOL: theory Complete_Lattices
HOL: theory Typedef
HOL: theory Fun
HOL: theory Inductive
HOL: theory Fields
HOL: theory Product_Type
HOL: theory Sum_Type
HOL: theory Complete_Partial_Order
HOL: theory Nat
HOL: theory Datatype
HOL: theory Meson
HOL: theory Num
HOL: theory Option
HOL: theory Extraction
HOL: theory Partial_Function
HOL: theory ATP
HOL: theory Power
HOL: theory Metis
HOL: theory Finite_Set
HOL: theory Relation
HOL: theory Transitive_Closure
HOL: theory Wellfounded
HOL: theory FunDef
HOL: theory Plain
HOL: theory Big_Operators
HOL: theory Hilbert_Choice
HOL: theory Equiv_Relations
HOL: theory Transfer
HOL: theory Lifting
HOL: theory Quotient
HOL: theory Int
HOL: theory Nat_Transfer
HOL: theory Divides
HOL: theory Set_Interval
HOL: theory Code_Numeral
HOL: theory Numeral_Simprocs
HOL: theory Semiring_Normalization
HOL: theory Groebner_Basis
HOL: theory Presburger
HOL: theory List
HOL: theory Map
HOL: theory Predicate
HOL: theory Random
HOL: theory Enum
HOL: theory Lazy_Sequence
HOL: theory String
HOL: theory DSequence
HOL: theory New_DSequence
HOL: theory Typerep
HOL: theory Code_Evaluation
HOL: theory Quickcheck
HOL: theory Quickcheck_Exhaustive
HOL: theory Random_Sequence
HOL: theory New_Random_Sequence
HOL: theory Quickcheck_Narrowing
HOL: theory Predicate_Compile
HOL: theory Record
HOL: theory SMT
HOL: theory Sledgehammer
HOL: theory Nitpick
HOL: theory Main
HOL: theory Archimedean_Field
HOL: theory Fact
HOL: theory Lubs
HOL: theory Parity
HOL: theory GCD
HOL: theory Rat
HOL: theory RealDef
HOL: theory RComplete
HOL: theory RealVector
HOL: theory SupInf
HOL: theory Limits
HOL: theory Real
HOL: theory SEQ
HOL: theory Lim
HOL: theory Deriv
HOL: theory Series
HOL: theory NthRoot
HOL: theory Transcendental
HOL: theory Complex
HOL: theory Ln
HOL: theory Log
HOL: theory MacLaurin
HOL: theory Taylor
HOL: theory Complex_Main
Timing HOL (6 threads, 86.669s elapsed time, 235.547s cpu time, 20.292s GC time, factor 2.72)
Finished HOL (0:01:48 elapsed time, 0:04:36 cpu time, factor 2.55)
Building HOL-Multivariate_Analysis ...
HOL-Multivariate_Analysis: theory FuncSet
HOL-Multivariate_Analysis: theory Infinite_Set
HOL-Multivariate_Analysis: theory Indicator_Function
HOL-Multivariate_Analysis: theory Nat_Bijection
HOL-Multivariate_Analysis: theory Glbs
HOL-Multivariate_Analysis: theory Extended_Nat
HOL-Multivariate_Analysis: theory L2_Norm
HOL-Multivariate_Analysis: theory FrechetDeriv
HOL-Multivariate_Analysis: theory Sum_of_Squares
HOL-Multivariate_Analysis: theory Inner_Product
HOL-Multivariate_Analysis: theory Permutations
HOL-Multivariate_Analysis: theory Phantom_Type
HOL-Multivariate_Analysis: theory Countable
HOL-Multivariate_Analysis: theory Extended_Real
HOL-Multivariate_Analysis: theory Cardinality
HOL-Multivariate_Analysis: theory Product_plus
HOL-Multivariate_Analysis: theory Set_Algebras
HOL-Multivariate_Analysis: theory Product_Vector
HOL-Multivariate_Analysis: theory Countable_Set
HOL-Multivariate_Analysis: theory Convex
HOL-Multivariate_Analysis: theory Euclidean_Space
HOL-Multivariate_Analysis: theory Numeral_Type
HOL-Multivariate_Analysis: theory Linear_Algebra
HOL-Multivariate_Analysis: theory Norm_Arith
HOL-Multivariate_Analysis: theory Finite_Cartesian_Product
HOL-Multivariate_Analysis: theory Operator_Norm
HOL-Multivariate_Analysis: theory Topology_Euclidean_Space
HOL-Multivariate_Analysis: theory Extended_Real_Limits
HOL-Multivariate_Analysis: theory Convex_Euclidean_Space
HOL-Multivariate_Analysis: theory Brouwer_Fixpoint
HOL-Multivariate_Analysis: theory Path_Connected
HOL-Multivariate_Analysis: theory Derivative
HOL-Multivariate_Analysis: theory Integration
HOL-Multivariate_Analysis: theory Cartesian_Euclidean_Space
HOL-Multivariate_Analysis: theory Determinants
HOL-Multivariate_Analysis: theory Fashoda
HOL-Multivariate_Analysis: theory Multivariate_Analysis
Timing HOL-Multivariate_Analysis (6 threads, 33.574s elapsed time, 192.976s cpu time, 9.037s GC time, factor 5.75)
Finished HOL-Multivariate_Analysis (0:00:49 elapsed time, 0:03:34 cpu time, factor 4.36)
Building HOL-Nominal ...
HOL-Nominal: theory Infinite_Set
HOL-Nominal: theory Nominal
Timing HOL-Nominal (6 threads, 4.332s elapsed time, 9.247s cpu time, 0.440s GC time, factor 2.13)
Finished HOL-Nominal (0:00:14 elapsed time, 0:00:21 cpu time, factor 1.50)
Building HOL-Proofs ...
HOL-Proofs: theory Code_Generator
HOL-Proofs: theory HOL
HOL-Proofs: theory Orderings
HOL-Proofs: theory SAT
HOL-Proofs: theory Groups
HOL-Proofs: theory Rings
HOL-Proofs: theory Lattices
HOL-Proofs: theory Set
HOL-Proofs: theory Complete_Lattices
HOL-Proofs: theory Typedef
HOL-Proofs: theory Fun
HOL-Proofs: theory Inductive
HOL-Proofs: theory Fields
HOL-Proofs: theory Product_Type
HOL-Proofs: theory Sum_Type
HOL-Proofs: theory Complete_Partial_Order
HOL-Proofs: theory Nat
HOL-Proofs: theory Datatype
HOL-Proofs: theory Meson
HOL-Proofs: theory Num
HOL-Proofs: theory Option
HOL-Proofs: theory Extraction
HOL-Proofs: theory ATP
HOL-Proofs: theory Partial_Function
HOL-Proofs: theory Metis
HOL-Proofs: theory Power
HOL-Proofs: theory Finite_Set
HOL-Proofs: theory Relation
HOL-Proofs: theory Transitive_Closure
HOL-Proofs: theory Wellfounded
HOL-Proofs: theory FunDef
HOL-Proofs: theory Plain
HOL-Proofs: theory Big_Operators
HOL-Proofs: theory Hilbert_Choice
HOL-Proofs: theory Equiv_Relations
HOL-Proofs: theory Transfer
HOL-Proofs: theory Lifting
HOL-Proofs: theory Quotient
HOL-Proofs: theory Int
HOL-Proofs: theory Nat_Transfer
HOL-Proofs: theory Divides
HOL-Proofs: theory Set_Interval
HOL-Proofs: theory Code_Numeral
HOL-Proofs: theory Numeral_Simprocs
HOL-Proofs: theory Semiring_Normalization
HOL-Proofs: theory Groebner_Basis
HOL-Proofs: theory Presburger
HOL-Proofs: theory List
HOL-Proofs: theory Map
HOL-Proofs: theory Predicate
HOL-Proofs: theory Random
HOL-Proofs: theory Enum
HOL-Proofs: theory Lazy_Sequence
HOL-Proofs: theory String
HOL-Proofs: theory DSequence
HOL-Proofs: theory New_DSequence
HOL-Proofs: theory Typerep
HOL-Proofs: theory Code_Evaluation
HOL-Proofs: theory Quickcheck
HOL-Proofs: theory Quickcheck_Exhaustive
HOL-Proofs: theory Random_Sequence
HOL-Proofs: theory New_Random_Sequence
HOL-Proofs: theory Quickcheck_Narrowing
HOL-Proofs: theory Predicate_Compile
HOL-Proofs: theory Record
HOL-Proofs: theory SMT
HOL-Proofs: theory Sledgehammer
HOL-Proofs: theory Nitpick
HOL-Proofs: theory Main
Timing HOL-Proofs (6 threads, 128.346s elapsed time, 528.124s cpu time, 45.443s GC time, factor 4.11)
Finished HOL-Proofs (0:02:39 elapsed time, 0:09:48 cpu time, factor 3.69)
Building ZF ...
ZF: theory IFOL
ZF: theory FOL
ZF: theory ZF
ZF: theory upair
ZF: theory pair
ZF: theory Bool
ZF: theory equalities
ZF: theory Fixedpt
ZF: theory Sum
ZF: theory func
ZF: theory Perm
ZF: theory QPair
ZF: theory Trancl
ZF: theory EquivClass
ZF: theory WF
ZF: theory Order
ZF: theory Ordinal
ZF: theory OrdQuant
ZF: theory OrderArith
ZF: theory Nat_ZF
ZF: theory Epsilon
ZF: theory OrderType
ZF: theory Inductive_ZF
ZF: theory Finite
ZF: theory Cardinal
ZF: theory Univ
ZF: theory Arith
ZF: theory QUniv
ZF: theory Datatype_ZF
ZF: theory ArithSimp
ZF: theory Int_ZF
ZF: theory CardinalArith
ZF: theory List_ZF
ZF: theory Bin
ZF: theory IntArith
ZF: theory IntDiv_ZF
ZF: theory Main_ZF
ZF: theory AC
ZF: theory Main
ZF: theory Zorn
ZF: theory Cardinal_AC
ZF: theory InfDatatype
ZF: theory Main_ZFC
Timing ZF (6 threads, 7.414s elapsed time, 28.760s cpu time, 1.821s GC time, factor 3.88)
Finished ZF (0:00:10 elapsed time, 0:00:32 cpu time, factor 3.20)
Running HOL-Nominal-Examples ...
HOL-Nominal-Examples: theory Class1
HOL-Nominal-Examples: theory Compile
HOL-Nominal-Examples: theory Contexts
HOL-Nominal-Examples: theory CK_Machine
HOL-Nominal-Examples: theory CR_Takahashi
HOL-Nominal-Examples: theory Crary
HOL-Nominal-Examples: theory Fsub
HOL-Nominal-Examples: theory Height
HOL-Nominal-Examples: theory Lam_Funs
HOL-Nominal-Examples: theory Lambda_mu
HOL-Nominal-Examples: theory CR
HOL-Nominal-Examples: theory SN
HOL-Nominal-Examples: theory LocalWeakening
HOL-Nominal-Examples: theory Pattern
HOL-Nominal-Examples: theory SOS
HOL-Nominal-Examples: theory Standardization
HOL-Nominal-Examples: theory Support
HOL-Nominal-Examples: theory Type_Preservation
HOL-Nominal-Examples: theory W
HOL-Nominal-Examples: theory Weakening
HOL-Nominal-Examples: theory Class2
HOL-Nominal-Examples: theory Class3
HOL-Nominal-Examples: theory Nominal_Examples
HOL-Nominal-Examples: theory VC_Condition
Timing HOL-Nominal-Examples (6 threads, 106.768s elapsed time, 583.930s cpu time, 47.267s GC time, factor 5.47)
Finished HOL-Nominal-Examples (0:01:50 elapsed time, 0:09:46 cpu time, factor 5.32)
Running HOL-Auth ...
HOL-Auth: theory Message
HOL-Auth: theory Nat_Bijection
HOL-Auth: theory All_Symmetric
HOL-Auth: theory Event
HOL-Auth: theory EventSC
HOL-Auth: theory Extensions
HOL-Auth: theory Public
HOL-Auth: theory Shared
HOL-Auth: theory CertifiedEmail
HOL-Auth: theory KerberosIV
HOL-Auth: theory KerberosIV_Gets
HOL-Auth: theory Analz
HOL-Auth: theory List_Msg
HOL-Auth: theory KerberosV
HOL-Auth: theory Kerberos_BAN
HOL-Auth: theory Guard
HOL-Auth: theory GuardK
HOL-Auth: theory Guard_Public
HOL-Auth: theory Kerberos_BAN_Gets
HOL-Auth: theory NS_Public
HOL-Auth: theory Guard_NS_Public
HOL-Auth: theory Proto
HOL-Auth: theory NS_Public_Bad
HOL-Auth: theory NS_Shared
HOL-Auth: theory OtwayRees
HOL-Auth: theory OtwayReesBella
HOL-Auth: theory P2
HOL-Auth: theory OtwayRees_AN
HOL-Auth: theory OtwayRees_Bad
HOL-Auth: theory P1
HOL-Auth: theory Recur
HOL-Auth: theory WooLam
HOL-Auth: theory Yahalom
HOL-Auth: theory Yahalom2
HOL-Auth: theory Yahalom_Bad
HOL-Auth: theory ZhouGollmann
HOL-Auth: theory Guard_Shared
HOL-Auth: theory Smartcard
HOL-Auth: theory TLS
HOL-Auth: theory Guard_OtwayRees
HOL-Auth: theory Guard_Yahalom
HOL-Auth: theory Auth_Shared
HOL-Auth: theory ShoupRubin
HOL-Auth: theory Auth_Guard_Shared
HOL-Auth: theory ShoupRubinBella
HOL-Auth: theory Auth_Public
HOL-Auth: theory Auth_Smartcard
HOL-Auth: theory Auth_Guard_Public
Timing HOL-Auth (6 threads, 47.280s elapsed time, 246.471s cpu time, 13.673s GC time, factor 5.21)
Finished HOL-Auth (0:00:49 elapsed time, 0:04:08 cpu time, factor 5.06)
Running HOL-Bali ...
HOL-Bali: theory Wfrec
HOL-Bali: theory Old_Recdef
HOL-Bali: theory Basis
HOL-Bali: theory Name
HOL-Bali: theory Table
HOL-Bali: theory Type
HOL-Bali: theory Value
HOL-Bali: theory Term
HOL-Bali: theory Decl
HOL-Bali: theory TypeRel
HOL-Bali: theory DeclConcepts
HOL-Bali: theory State
HOL-Bali: theory WellType
HOL-Bali: theory Conform
HOL-Bali: theory Eval
HOL-Bali: theory DefiniteAssignment
HOL-Bali: theory WellForm
HOL-Bali: theory DefiniteAssignmentCorrect
HOL-Bali: theory Example
HOL-Bali: theory TypeSafe
HOL-Bali: theory Evaln
HOL-Bali: theory AxSem
HOL-Bali: theory Trans
HOL-Bali: theory AxCompl
HOL-Bali: theory AxSound
HOL-Bali: theory AxExample
Timing HOL-Bali (6 threads, 44.236s elapsed time, 160.019s cpu time, 8.525s GC time, factor 3.62)
Finished HOL-Bali (0:00:46 elapsed time, 0:02:41 cpu time, factor 3.50)
Running HOL-Decision_Procs ...
HOL-Decision_Procs: theory Code_Natural
HOL-Decision_Procs: theory Code_Binary_Nat
HOL-Decision_Procs: theory DP_Library
HOL-Decision_Procs: theory Dense_Linear_Order
HOL-Decision_Procs: theory Commutative_Ring
HOL-Decision_Procs: theory Abstract_Rat
HOL-Decision_Procs: theory Code_Integer
HOL-Decision_Procs: theory Lattice_Algebras
HOL-Decision_Procs: theory Polynomial_List
HOL-Decision_Procs: theory Efficient_Nat
HOL-Decision_Procs: theory Reflection
HOL-Decision_Procs: theory Wfrec
HOL-Decision_Procs: theory Old_Recdef
HOL-Decision_Procs: theory Reflected_Multivariate_Polynomial
HOL-Decision_Procs: theory Cooper
HOL-Decision_Procs: theory Dense_Linear_Order_Ex
HOL-Decision_Procs: theory Ferrack
HOL-Decision_Procs: theory MIR
HOL-Decision_Procs: theory Commutative_Ring_Complete
HOL-Decision_Procs: theory Commutative_Ring_Ex
HOL-Decision_Procs: theory Float
HOL-Decision_Procs: theory Approximation
HOL-Decision_Procs: theory Parametric_Ferrante_Rackoff
HOL-Decision_Procs: theory Approximation_Ex
HOL-Decision_Procs: theory Decision_Procs
Timing HOL-Decision_Procs (6 threads, 83.960s elapsed time, 467.899s cpu time, 41.250s GC time, factor 5.57)
Finished HOL-Decision_Procs (0:01:26 elapsed time, 0:07:49 cpu time, factor 5.45)
Running HOL-Hoare_Parallel ...
HOL-Hoare_Parallel: theory Graph
HOL-Hoare_Parallel: theory Quote_Antiquote
HOL-Hoare_Parallel: theory RG_Com
HOL-Hoare_Parallel: theory OG_Com
HOL-Hoare_Parallel: theory RG_Tran
HOL-Hoare_Parallel: theory RG_Hoare
HOL-Hoare_Parallel: theory OG_Tran
HOL-Hoare_Parallel: theory RG_Syntax
HOL-Hoare_Parallel: theory RG_Examples
HOL-Hoare_Parallel: theory OG_Hoare
HOL-Hoare_Parallel: theory OG_Tactics
HOL-Hoare_Parallel: theory OG_Syntax
HOL-Hoare_Parallel: theory Gar_Coll
HOL-Hoare_Parallel: theory Mul_Gar_Coll
HOL-Hoare_Parallel: theory OG_Examples
HOL-Hoare_Parallel: theory Hoare_Parallel
Timing HOL-Hoare_Parallel (6 threads, 41.599s elapsed time, 230.704s cpu time, 5.156s GC time, factor 5.55)
Finished HOL-Hoare_Parallel (0:00:43 elapsed time, 0:03:51 cpu time, factor 5.37)
Running HOL-IMP ...
HOL-IMP: theory Char_nat
HOL-IMP: theory List_lexord
HOL-IMP: theory While_Combinator
HOL-IMP: theory Interpretation_with_Defs
HOL-IMP: theory Char_ord
HOL-IMP: theory AExp
HOL-IMP: theory Complete_Lattice
HOL-IMP: theory OO
HOL-IMP: theory C_like
HOL-IMP: theory Complete_Lattice_ix
HOL-IMP: theory Star
HOL-IMP: theory Types
HOL-IMP: theory Poly_Types
HOL-IMP: theory ASM
HOL-IMP: theory BExp
HOL-IMP: theory Com
HOL-IMP: theory Procs
HOL-IMP: theory Vars
HOL-IMP: theory ACom
HOL-IMP: theory ACom_ITP
HOL-IMP: theory Abs_Int_Tests
HOL-IMP: theory Big_Step
HOL-IMP: theory Procs_Dyn_Vars_Dyn
HOL-IMP: theory Procs_Stat_Vars_Dyn
HOL-IMP: theory Procs_Stat_Vars_Stat
HOL-IMP: theory Collecting_ITP
HOL-IMP: theory Compiler
HOL-IMP: theory Denotation
HOL-IMP: theory Hoare
HOL-IMP: theory Hoare_Examples
HOL-IMP: theory Hoare_Sound_Complete
HOL-IMP: theory VC
HOL-IMP: theory HoareT
HOL-IMP: theory Sec_Type_Expr
HOL-IMP: theory Sem_Equiv
HOL-IMP: theory Sec_Typing
HOL-IMP: theory Sec_TypingT
HOL-IMP: theory Fold
HOL-IMP: theory Def_Init
HOL-IMP: theory Def_Init_Exp
HOL-IMP: theory Live
HOL-IMP: theory Collecting
HOL-IMP: theory Def_Init_Big
HOL-IMP: theory Def_Init_Sound_Big
HOL-IMP: theory Def_Init_Small
HOL-IMP: theory Small_Step
HOL-IMP: theory Def_Init_Sound_Small
HOL-IMP: theory Live_True
HOL-IMP: theory Abs_Int0_ITP
HOL-IMP: theory Abs_Int_den0_fun
HOL-IMP: theory Abs_State_den
HOL-IMP: theory Abs_Int_den0
HOL-IMP: theory Finite_Reachable
HOL-IMP: theory Collecting1
HOL-IMP: theory Collecting_Examples
HOL-IMP: theory Abs_Int_init
HOL-IMP: theory Abs_Int_den0_const
HOL-IMP: theory Abs_State_ITP
HOL-IMP: theory Abs_Int0
HOL-IMP: theory Abs_Int1_ITP
HOL-IMP: theory Comp_Rev
HOL-IMP: theory Abs_Int1_const_ITP
HOL-IMP: theory Abs_Int1_parity_ITP
HOL-IMP: theory Abs_Int2_ITP
HOL-IMP: theory Abs_Int_den1
HOL-IMP: theory Abs_State
HOL-IMP: theory Abs_Int2_ivl_ITP
HOL-IMP: theory Abs_Int_den1_ivl
HOL-IMP: theory Abs_Int1
HOL-IMP: theory Abs_Int1_const
HOL-IMP: theory Abs_Int1_parity
HOL-IMP: theory Abs_Int2
HOL-IMP: theory Abs_Int2_ivl
HOL-IMP: theory Abs_Int3_ITP
HOL-IMP: theory Abs_Int_den2
HOL-IMP: theory Abs_Int3
Timing HOL-IMP (6 threads, 99.605s elapsed time, 493.776s cpu time, 46.000s GC time, factor 4.96)
Finished HOL-IMP (0:01:42 elapsed time, 0:08:16 cpu time, factor 4.86)
Running HOL-Library ...
HOL-Library: theory Adhoc_Overloading
HOL-Library: theory Lattice_Syntax
HOL-Library: theory Preorder
HOL-Library: theory Refute
HOL-Library: theory AList
HOL-Library: theory Bit
HOL-Library: theory Boolean_Algebra
HOL-Library: theory Char_nat
HOL-Library: theory Code_Binary_Nat
HOL-Library: theory Char_ord
HOL-Library: theory Code_Char
HOL-Library: theory Code_Natural
HOL-Library: theory Code_Numeral_Types
HOL-Library: theory Code_Integer
HOL-Library: theory Code_Char_ord
HOL-Library: theory Code_Char_chr
HOL-Library: theory Continuity
HOL-Library: theory Debug
HOL-Library: theory Dlist
HOL-Library: theory Efficient_Nat
HOL-Library: theory Eval_Witness
HOL-Library: theory Extended_Nat
HOL-Library: theory Fraction_Field
HOL-Library: theory IArray
HOL-Library: theory FuncSet
HOL-Library: theory DAList
HOL-Library: theory Function_Algebras
HOL-Library: theory Indicator_Function
HOL-Library: theory Infinite_Set
HOL-Library: theory Kleene_Algebra
HOL-Library: theory LaTeXsugar
HOL-Library: theory Function_Division
HOL-Library: theory ListVector
HOL-Library: theory Code_Target_Int
HOL-Library: theory Code_Target_Nat
HOL-Library: theory List_lexord
HOL-Library: theory Monad_Syntax
HOL-Library: theory Code_Target_Numeral
HOL-Library: theory Option_ord
HOL-Library: theory Order_Relation
HOL-Library: theory Parallel
HOL-Library: theory Diagonal_Subsequence
HOL-Library: theory Zorn
HOL-Library: theory Nat_Bijection
HOL-Library: theory Abstract_Rat
HOL-Library: theory Binomial
HOL-Library: theory Multiset
HOL-Library: theory Code_Real_Approx_By_Float
HOL-Library: theory ContNotDenum
HOL-Library: theory Formal_Power_Series
HOL-Library: theory Countable
HOL-Library: theory FrechetDeriv
HOL-Library: theory Inner_Product
HOL-Library: theory Lattice_Algebras
HOL-Library: theory Countable_Set
HOL-Library: theory OptionalSugar
HOL-Library: theory Sum_of_Squares
HOL-Library: theory Permutations
HOL-Library: theory Phantom_Type
HOL-Library: theory Cardinality
HOL-Library: theory Polynomial
HOL-Library: theory Permutation
HOL-Library: theory Product_plus
HOL-Library: theory Product_Lattice
HOL-Library: theory Finite_Lattice
HOL-Library: theory FinFun
HOL-Library: theory Numeral_Type
HOL-Library: theory Product_Vector
HOL-Library: theory Fundamental_Theorem_Algebra
HOL-Library: theory Float
HOL-Library: theory Type_Length
HOL-Library: theory Poly_Deriv
HOL-Library: theory Convex
HOL-Library: theory Quotient_Syntax
HOL-Library: theory Quotient_Option
HOL-Library: theory Quotient_Product
HOL-Library: theory Quotient_Set
HOL-Library: theory Quotient_Sum
HOL-Library: theory Quotient_Type
HOL-Library: theory RBT_Impl
HOL-Library: theory Mapping
HOL-Library: theory Quotient_List
HOL-Library: theory Ramsey
HOL-Library: theory Reflection
HOL-Library: theory Saturated
HOL-Library: theory Set_Algebras
HOL-Library: theory State_Monad
HOL-Library: theory AList_Mapping
HOL-Library: theory Sublist
HOL-Library: theory BigO
HOL-Library: theory Transitive_Closure_Table
HOL-Library: theory Univ_Poly
HOL-Library: theory Wfrec
HOL-Library: theory Sublist_Order
HOL-Library: theory Old_Recdef
HOL-Library: theory While_Combinator
HOL-Library: theory RBT
HOL-Library: theory RBT_Mapping
HOL-Library: theory Library
Skipping theories "Sum_of_Squares_Remote" (undefined ISABELLE_FULL_TEST)
Timing HOL-Library (6 threads, 46.268s elapsed time, 251.260s cpu time, 21.261s GC time, factor 5.43)
Finished HOL-Library (0:00:48 elapsed time, 0:04:12 cpu time, factor 5.25)
Running HOL-MicroJava ...
HOL-MicroJava: theory While_Combinator
HOL-MicroJava: theory Wfrec
HOL-MicroJava: theory Transitive_Closure_Table
HOL-MicroJava: theory Semilat
HOL-MicroJava: theory Err
HOL-MicroJava: theory Listn
HOL-MicroJava: theory Opt
HOL-MicroJava: theory Product
HOL-MicroJava: theory JBasis
HOL-MicroJava: theory AuxLemmas
HOL-MicroJava: theory Type
HOL-MicroJava: theory Typing_Framework
HOL-MicroJava: theory Semilattices
HOL-MicroJava: theory SemilatAlg
HOL-MicroJava: theory Kildall
HOL-MicroJava: theory LBVSpec
HOL-MicroJava: theory Typing_Framework_err
HOL-MicroJava: theory LBVComplete
HOL-MicroJava: theory LBVCorrect
HOL-MicroJava: theory Abstract_BV
HOL-MicroJava: theory Decl
HOL-MicroJava: theory Value
HOL-MicroJava: theory SystemClasses
HOL-MicroJava: theory TypeRel
HOL-MicroJava: theory Term
HOL-MicroJava: theory State
HOL-MicroJava: theory WellForm
HOL-MicroJava: theory Exceptions
HOL-MicroJava: theory JType
HOL-MicroJava: theory JVMType
HOL-MicroJava: theory WellType
HOL-MicroJava: theory Conform
HOL-MicroJava: theory Eval
HOL-MicroJava: theory TypeInf
HOL-MicroJava: theory JVMState
HOL-MicroJava: theory JVMInstructions
HOL-MicroJava: theory JVMExceptions
HOL-MicroJava: theory JVMExecInstr
HOL-MicroJava: theory Effect
HOL-MicroJava: theory JVMExec
HOL-MicroJava: theory DefsComp
HOL-MicroJava: theory JVMDefensive
HOL-MicroJava: theory JVMListExample
HOL-MicroJava: theory Index
HOL-MicroJava: theory TranslCompTp
HOL-MicroJava: theory TranslComp
HOL-MicroJava: theory Example
HOL-MicroJava: theory JListExample
HOL-MicroJava: theory JTypeSafe
HOL-MicroJava: theory LemmasComp
HOL-MicroJava: theory CorrComp
HOL-MicroJava: theory BVSpec
HOL-MicroJava: theory EffectMono
HOL-MicroJava: theory Altern
HOL-MicroJava: theory Correct
HOL-MicroJava: theory Typing_Framework_JVM
HOL-MicroJava: theory BVSpecTypeSafe
HOL-MicroJava: theory JVM
HOL-MicroJava: theory LBVJVM
HOL-MicroJava: theory CorrCompTp
HOL-MicroJava: theory BVNoTypeError
HOL-MicroJava: theory BVExample
HOL-MicroJava: theory MicroJava
Timing HOL-MicroJava (6 threads, 45.750s elapsed time, 235.185s cpu time, 11.135s GC time, factor 5.14)
Finished HOL-MicroJava (0:00:48 elapsed time, 0:03:56 cpu time, factor 4.91)
Running HOL-Probability ...
HOL-Probability: theory AList
HOL-Probability: theory DAList
HOL-Probability: theory Multiset
HOL-Probability: theory Permutation
HOL-Probability: theory Diagonal_Subsequence
HOL-Probability: theory Sigma_Algebra
HOL-Probability: theory Discrete_Topology
HOL-Probability: theory Measurable
HOL-Probability: theory Measure_Space
HOL-Probability: theory Borel_Space
HOL-Probability: theory Caratheodory
HOL-Probability: theory Lebesgue_Integration
HOL-Probability: theory Regularity
HOL-Probability: theory Binary_Product_Measure
HOL-Probability: theory Complete_Measure
HOL-Probability: theory Radon_Nikodym
HOL-Probability: theory Finite_Product_Measure
HOL-Probability: theory Fin_Map
HOL-Probability: theory Lebesgue_Measure
HOL-Probability: theory Probability_Measure
HOL-Probability: theory Distributions
HOL-Probability: theory Projective_Family
HOL-Probability: theory Infinite_Product_Measure
HOL-Probability: theory Independent_Family
HOL-Probability: theory Projective_Limit
HOL-Probability: theory Information
HOL-Probability: theory Dining_Cryptographers
HOL-Probability: theory Koepf_Duermuth_Countermeasure
HOL-Probability: theory Probability
Timing HOL-Probability (6 threads, 33.781s elapsed time, 174.624s cpu time, 6.623s GC time, factor 5.17)
Finished HOL-Probability (0:00:37 elapsed time, 0:02:57 cpu time, factor 4.78)
Running HOL-Proofs-Extraction ...
HOL-Proofs-Extraction: theory Adhoc_Overloading
HOL-Proofs-Extraction: theory AList
HOL-Proofs-Extraction: theory Code_Binary_Nat
HOL-Proofs-Extraction: theory Code_Natural
HOL-Proofs-Extraction: theory Fact
HOL-Proofs-Extraction: theory Parity
HOL-Proofs-Extraction: theory Monad_Syntax
HOL-Proofs-Extraction: theory Code_Integer
HOL-Proofs-Extraction: theory State_Monad
HOL-Proofs-Extraction: theory Efficient_Nat
HOL-Proofs-Extraction: theory DAList
HOL-Proofs-Extraction: theory Multiset
HOL-Proofs-Extraction: theory GCD
HOL-Proofs-Extraction: theory Primes
HOL-Proofs-Extraction: theory Cong
HOL-Proofs-Extraction: theory UniqueFactorization
HOL-Proofs-Extraction: theory Warshall
HOL-Proofs-Extraction: theory Util
HOL-Proofs-Extraction: theory Higman
HOL-Proofs-Extraction: theory Euclid
HOL-Proofs-Extraction: theory Pigeonhole
HOL-Proofs-Extraction: theory QuotRem
HOL-Proofs-Extraction: theory Higman_Extraction
HOL-Proofs-Extraction: theory Greatest_Common_Divisor
Timing HOL-Proofs-Extraction (6 threads, 109.223s elapsed time, 383.002s cpu time, 30.888s GC time, factor 3.51)
Finished HOL-Proofs-Extraction (0:01:52 elapsed time, 0:06:24 cpu time, factor 3.42)
Running HOL-SET_Protocol ...
HOL-SET_Protocol: theory Nat_Bijection
HOL-SET_Protocol: theory Message_SET
HOL-SET_Protocol: theory Event_SET
HOL-SET_Protocol: theory Public_SET
HOL-SET_Protocol: theory Cardholder_Registration
HOL-SET_Protocol: theory Merchant_Registration
HOL-SET_Protocol: theory Purchase
HOL-SET_Protocol: theory SET_Protocol
Timing HOL-SET_Protocol (6 threads, 15.954s elapsed time, 73.493s cpu time, 1.739s GC time, factor 4.61)
Finished HOL-SET_Protocol (0:00:17 elapsed time, 0:01:14 cpu time, factor 4.35)
Running HOL-UNITY ...
HOL-UNITY: theory Message
HOL-UNITY: theory Event
HOL-UNITY: theory Public
HOL-UNITY: theory AList
HOL-UNITY: theory ListOrder
HOL-UNITY: theory UNITY
HOL-UNITY: theory Constrains
HOL-UNITY: theory Deadlock
HOL-UNITY: theory FP
HOL-UNITY: theory Network
HOL-UNITY: theory WFair
HOL-UNITY: theory SubstAx
HOL-UNITY: theory Token
HOL-UNITY: theory DAList
HOL-UNITY: theory Detects
HOL-UNITY: theory Union
HOL-UNITY: theory Comp
HOL-UNITY: theory Guar
HOL-UNITY: theory Transformers
HOL-UNITY: theory Multiset
HOL-UNITY: theory Extend
HOL-UNITY: theory ProgressSets
HOL-UNITY: theory Project
HOL-UNITY: theory Rename
HOL-UNITY: theory Lift_prog
HOL-UNITY: theory ELT
HOL-UNITY: theory PPROD
HOL-UNITY: theory Follows
HOL-UNITY: theory UNITY_Main
HOL-UNITY: theory AllocBase
HOL-UNITY: theory Channel
HOL-UNITY: theory Common
HOL-UNITY: theory Counter
HOL-UNITY: theory Counterc
HOL-UNITY: theory Alloc
HOL-UNITY: theory AllocImpl
HOL-UNITY: theory Client
HOL-UNITY: theory Handshake
HOL-UNITY: theory Lift
HOL-UNITY: theory Mutex
HOL-UNITY: theory NSP_Bad
HOL-UNITY: theory PriorityAux
HOL-UNITY: theory Priority
HOL-UNITY: theory Progress
HOL-UNITY: theory Reach
HOL-UNITY: theory TimerArray
HOL-UNITY: theory Reachability
Timing HOL-UNITY (6 threads, 15.599s elapsed time, 75.395s cpu time, 4.043s GC time, factor 4.83)
Finished HOL-UNITY (0:00:17 elapsed time, 0:01:16 cpu time, factor 4.47)
Running ZF-UNITY ...
ZF-UNITY: theory State
ZF-UNITY: theory FoldSet
ZF-UNITY: theory GenPrefix
ZF-UNITY: theory Acc
ZF-UNITY: theory UNITY
ZF-UNITY: theory Multiset
ZF-UNITY: theory Constrains
ZF-UNITY: theory FP
ZF-UNITY: theory WFair
ZF-UNITY: theory SubstAx
ZF-UNITY: theory MultisetSum
ZF-UNITY: theory Monotonicity
ZF-UNITY: theory Mutex
ZF-UNITY: theory Union
ZF-UNITY: theory Increasing
ZF-UNITY: theory Follows
ZF-UNITY: theory Comp
ZF-UNITY: theory Guar
ZF-UNITY: theory AllocBase
ZF-UNITY: theory ClientImpl
ZF-UNITY: theory Distributor
ZF-UNITY: theory Merge
ZF-UNITY: theory AllocImpl
Timing ZF-UNITY (6 threads, 6.176s elapsed time, 33.086s cpu time, 1.317s GC time, factor 5.36)
Finished ZF-UNITY (0:00:07 elapsed time, 0:00:32 cpu time, factor 4.57)
Finished at Mon Feb 4 20:53:55 CET 2013
0:18:04 elapsed time, 1:16:52 cpu time, factor 4.25
*** m=7 q=2 ***
Started at Mon Feb 4 20:53:55 CET 2013 (polyml-5.5.0_x86-darwin on lri29-163.lri.fr)
ISABELLE_BUILD_OPTIONS="threads_trace=2 threads=7 parallel_proofs=2"
ML_PLATFORM="x86-darwin"
ML_HOME="/Volumes/Macintosh_HD/Users/makarius/.isabelle/contrib/polyml-5.5.0-3/x86-darwin"
ML_SYSTEM="polyml-5.5.0"
ML_OPTIONS="--minheap 1000 --gcthreads 7"
Session Pure
Session HOL (main)
Session HOL-Auth
Session HOL-Bali
Session HOL-Decision_Procs
Session HOL-Hoare_Parallel
Session HOL-IMP
Session HOL-Library (main)
Session HOL-MicroJava
Session HOL-Multivariate_Analysis (main)
Session HOL-Probability
Session HOL-Nominal (main)
Session HOL-Nominal-Examples
Session HOL-SET_Protocol
Session HOL-UNITY
Session HOL-Proofs
Session HOL-Proofs-Extraction
Session ZF (main)
Session ZF-UNITY
Building Pure ...
Finished Pure (0:00:09 elapsed time, 0:00:10 cpu time, factor 1.11)
Building HOL ...
HOL: theory Code_Generator
HOL: theory HOL
HOL: theory Orderings
HOL: theory SAT
HOL: theory Groups
HOL: theory Rings
HOL: theory Lattices
HOL: theory Set
HOL: theory Complete_Lattices
HOL: theory Typedef
HOL: theory Fun
HOL: theory Inductive
HOL: theory Fields
HOL: theory Product_Type
HOL: theory Sum_Type
HOL: theory Complete_Partial_Order
HOL: theory Nat
HOL: theory Datatype
HOL: theory Meson
HOL: theory Option
HOL: theory Num
HOL: theory Extraction
HOL: theory Partial_Function
HOL: theory ATP
HOL: theory Power
HOL: theory Metis
HOL: theory Finite_Set
HOL: theory Relation
HOL: theory Transitive_Closure
HOL: theory Wellfounded
HOL: theory FunDef
HOL: theory Plain
HOL: theory Big_Operators
HOL: theory Hilbert_Choice
HOL: theory Equiv_Relations
HOL: theory Transfer
HOL: theory Lifting
HOL: theory Quotient
HOL: theory Int
HOL: theory Nat_Transfer
HOL: theory Divides
HOL: theory Set_Interval
HOL: theory Code_Numeral
HOL: theory Numeral_Simprocs
HOL: theory Semiring_Normalization
HOL: theory Groebner_Basis
HOL: theory Presburger
HOL: theory List
HOL: theory Map
HOL: theory Predicate
HOL: theory Random
HOL: theory Enum
HOL: theory Lazy_Sequence
HOL: theory String
HOL: theory DSequence
HOL: theory New_DSequence
HOL: theory Typerep
HOL: theory Code_Evaluation
HOL: theory Quickcheck
HOL: theory Quickcheck_Exhaustive
HOL: theory Random_Sequence
HOL: theory New_Random_Sequence
HOL: theory Quickcheck_Narrowing
HOL: theory Predicate_Compile
HOL: theory Record
HOL: theory SMT
HOL: theory Sledgehammer
HOL: theory Nitpick
HOL: theory Main
HOL: theory Archimedean_Field
HOL: theory Fact
HOL: theory Lubs
HOL: theory Parity
HOL: theory GCD
HOL: theory Rat
HOL: theory RealDef
HOL: theory RComplete
HOL: theory RealVector
HOL: theory SupInf
HOL: theory Real
HOL: theory Limits
HOL: theory SEQ
HOL: theory Lim
HOL: theory Deriv
HOL: theory Series
HOL: theory NthRoot
HOL: theory Transcendental
HOL: theory Complex
HOL: theory Ln
HOL: theory Log
HOL: theory MacLaurin
HOL: theory Taylor
HOL: theory Complex_Main
Timing HOL (7 threads, 84.396s elapsed time, 231.180s cpu time, 14.794s GC time, factor 2.74)
Finished HOL (0:01:45 elapsed time, 0:04:33 cpu time, factor 2.60)
Building HOL-Multivariate_Analysis ...
HOL-Multivariate_Analysis: theory Extended_Nat
HOL-Multivariate_Analysis: theory FuncSet
HOL-Multivariate_Analysis: theory Infinite_Set
HOL-Multivariate_Analysis: theory Nat_Bijection
HOL-Multivariate_Analysis: theory Glbs
HOL-Multivariate_Analysis: theory L2_Norm
HOL-Multivariate_Analysis: theory Indicator_Function
HOL-Multivariate_Analysis: theory FrechetDeriv
HOL-Multivariate_Analysis: theory Sum_of_Squares
HOL-Multivariate_Analysis: theory Permutations
HOL-Multivariate_Analysis: theory Inner_Product
HOL-Multivariate_Analysis: theory Phantom_Type
HOL-Multivariate_Analysis: theory Product_plus
HOL-Multivariate_Analysis: theory Countable
HOL-Multivariate_Analysis: theory Set_Algebras
HOL-Multivariate_Analysis: theory Cardinality
HOL-Multivariate_Analysis: theory Extended_Real
HOL-Multivariate_Analysis: theory Product_Vector
HOL-Multivariate_Analysis: theory Countable_Set
HOL-Multivariate_Analysis: theory Convex
HOL-Multivariate_Analysis: theory Euclidean_Space
HOL-Multivariate_Analysis: theory Numeral_Type
HOL-Multivariate_Analysis: theory Linear_Algebra
HOL-Multivariate_Analysis: theory Norm_Arith
HOL-Multivariate_Analysis: theory Finite_Cartesian_Product
HOL-Multivariate_Analysis: theory Operator_Norm
HOL-Multivariate_Analysis: theory Topology_Euclidean_Space
HOL-Multivariate_Analysis: theory Extended_Real_Limits
HOL-Multivariate_Analysis: theory Convex_Euclidean_Space
HOL-Multivariate_Analysis: theory Brouwer_Fixpoint
HOL-Multivariate_Analysis: theory Path_Connected
HOL-Multivariate_Analysis: theory Derivative
HOL-Multivariate_Analysis: theory Integration
HOL-Multivariate_Analysis: theory Cartesian_Euclidean_Space
HOL-Multivariate_Analysis: theory Determinants
HOL-Multivariate_Analysis: theory Fashoda
HOL-Multivariate_Analysis: theory Multivariate_Analysis
Timing HOL-Multivariate_Analysis (7 threads, 30.019s elapsed time, 197.165s cpu time, 10.224s GC time, factor 6.57)
Finished HOL-Multivariate_Analysis (0:00:46 elapsed time, 0:03:41 cpu time, factor 4.80)
Building HOL-Nominal ...
HOL-Nominal: theory Infinite_Set
HOL-Nominal: theory Nominal
Timing HOL-Nominal (7 threads, 4.339s elapsed time, 9.328s cpu time, 0.463s GC time, factor 2.15)
Finished HOL-Nominal (0:00:14 elapsed time, 0:00:21 cpu time, factor 1.50)
Building HOL-Proofs ...
HOL-Proofs: theory Code_Generator
HOL-Proofs: theory HOL
HOL-Proofs: theory Orderings
HOL-Proofs: theory SAT
HOL-Proofs: theory Groups
HOL-Proofs: theory Rings
HOL-Proofs: theory Lattices
HOL-Proofs: theory Set
HOL-Proofs: theory Complete_Lattices
HOL-Proofs: theory Typedef
HOL-Proofs: theory Fun
HOL-Proofs: theory Inductive
HOL-Proofs: theory Fields
HOL-Proofs: theory Product_Type
HOL-Proofs: theory Sum_Type
HOL-Proofs: theory Complete_Partial_Order
HOL-Proofs: theory Nat
HOL-Proofs: theory Datatype
HOL-Proofs: theory Meson
HOL-Proofs: theory Num
HOL-Proofs: theory Option
HOL-Proofs: theory Extraction
HOL-Proofs: theory Partial_Function
HOL-Proofs: theory ATP
HOL-Proofs: theory Metis
HOL-Proofs: theory Power
HOL-Proofs: theory Finite_Set
HOL-Proofs: theory Relation
HOL-Proofs: theory Transitive_Closure
HOL-Proofs: theory Wellfounded
HOL-Proofs: theory FunDef
HOL-Proofs: theory Plain
HOL-Proofs: theory Big_Operators
HOL-Proofs: theory Hilbert_Choice
HOL-Proofs: theory Equiv_Relations
HOL-Proofs: theory Transfer
HOL-Proofs: theory Lifting
HOL-Proofs: theory Quotient
HOL-Proofs: theory Int
HOL-Proofs: theory Nat_Transfer
HOL-Proofs: theory Divides
HOL-Proofs: theory Set_Interval
HOL-Proofs: theory Code_Numeral
HOL-Proofs: theory Numeral_Simprocs
HOL-Proofs: theory Semiring_Normalization
HOL-Proofs: theory Groebner_Basis
HOL-Proofs: theory Presburger
HOL-Proofs: theory List
HOL-Proofs: theory Map
HOL-Proofs: theory Predicate
HOL-Proofs: theory Enum
HOL-Proofs: theory Lazy_Sequence
HOL-Proofs: theory Random
HOL-Proofs: theory String
HOL-Proofs: theory DSequence
HOL-Proofs: theory New_DSequence
HOL-Proofs: theory Typerep
HOL-Proofs: theory Code_Evaluation
HOL-Proofs: theory Quickcheck
HOL-Proofs: theory Quickcheck_Exhaustive
HOL-Proofs: theory Random_Sequence
HOL-Proofs: theory New_Random_Sequence
HOL-Proofs: theory Quickcheck_Narrowing
HOL-Proofs: theory Predicate_Compile
HOL-Proofs: theory Record
HOL-Proofs: theory SMT
HOL-Proofs: theory Sledgehammer
HOL-Proofs: theory Nitpick
HOL-Proofs: theory Main
Timing HOL-Proofs (7 threads, 80.954s elapsed time, 380.370s cpu time, 36.790s GC time, factor 4.70)
Finished HOL-Proofs (0:01:50 elapsed time, 0:07:19 cpu time, factor 3.99)
Building ZF ...
ZF: theory IFOL
ZF: theory FOL
ZF: theory ZF
ZF: theory upair
ZF: theory pair
ZF: theory Bool
ZF: theory equalities
ZF: theory Fixedpt
ZF: theory Sum
ZF: theory func
ZF: theory Perm
ZF: theory QPair
ZF: theory Trancl
ZF: theory EquivClass
ZF: theory WF
ZF: theory Order
ZF: theory Ordinal
ZF: theory OrdQuant
ZF: theory OrderArith
ZF: theory Nat_ZF
ZF: theory Epsilon
ZF: theory OrderType
ZF: theory Inductive_ZF
ZF: theory Finite
ZF: theory Cardinal
ZF: theory Univ
ZF: theory Arith
ZF: theory QUniv
ZF: theory Datatype_ZF
ZF: theory ArithSimp
ZF: theory Int_ZF
ZF: theory List_ZF
ZF: theory CardinalArith
ZF: theory Bin
ZF: theory IntArith
ZF: theory IntDiv_ZF
ZF: theory Main_ZF
ZF: theory AC
ZF: theory Main
ZF: theory Zorn
ZF: theory Cardinal_AC
ZF: theory InfDatatype
ZF: theory Main_ZFC
Timing ZF (7 threads, 7.315s elapsed time, 28.739s cpu time, 1.652s GC time, factor 3.93)
Finished ZF (0:00:10 elapsed time, 0:00:32 cpu time, factor 3.20)
Running HOL-Nominal-Examples ...
HOL-Nominal-Examples: theory CK_Machine
HOL-Nominal-Examples: theory CR_Takahashi
HOL-Nominal-Examples: theory Class1
HOL-Nominal-Examples: theory Compile
HOL-Nominal-Examples: theory Contexts
HOL-Nominal-Examples: theory Crary
HOL-Nominal-Examples: theory Fsub
HOL-Nominal-Examples: theory Height
HOL-Nominal-Examples: theory Lam_Funs
HOL-Nominal-Examples: theory Lambda_mu
HOL-Nominal-Examples: theory LocalWeakening
HOL-Nominal-Examples: theory CR
HOL-Nominal-Examples: theory SN
HOL-Nominal-Examples: theory Pattern
HOL-Nominal-Examples: theory SOS
HOL-Nominal-Examples: theory Standardization
HOL-Nominal-Examples: theory Support
HOL-Nominal-Examples: theory Type_Preservation
HOL-Nominal-Examples: theory W
HOL-Nominal-Examples: theory Weakening
HOL-Nominal-Examples: theory Class2
HOL-Nominal-Examples: theory Class3
HOL-Nominal-Examples: theory Nominal_Examples
HOL-Nominal-Examples: theory VC_Condition
Timing HOL-Nominal-Examples (7 threads, 98.261s elapsed time, 591.926s cpu time, 49.504s GC time, factor 6.02)
Finished HOL-Nominal-Examples (0:01:41 elapsed time, 0:09:53 cpu time, factor 5.87)
Running HOL-Auth ...
HOL-Auth: theory Message
HOL-Auth: theory Nat_Bijection
HOL-Auth: theory All_Symmetric
HOL-Auth: theory Event
HOL-Auth: theory EventSC
HOL-Auth: theory Extensions
HOL-Auth: theory Public
HOL-Auth: theory Shared
HOL-Auth: theory CertifiedEmail
HOL-Auth: theory KerberosIV
HOL-Auth: theory KerberosIV_Gets
HOL-Auth: theory KerberosV
HOL-Auth: theory Analz
HOL-Auth: theory List_Msg
HOL-Auth: theory Kerberos_BAN
HOL-Auth: theory Kerberos_BAN_Gets
HOL-Auth: theory Guard
HOL-Auth: theory GuardK
HOL-Auth: theory Guard_Public
HOL-Auth: theory NS_Public
HOL-Auth: theory NS_Public_Bad
HOL-Auth: theory Guard_NS_Public
HOL-Auth: theory Proto
HOL-Auth: theory NS_Shared
HOL-Auth: theory OtwayRees
HOL-Auth: theory OtwayReesBella
HOL-Auth: theory OtwayRees_AN
HOL-Auth: theory OtwayRees_Bad
HOL-Auth: theory Recur
HOL-Auth: theory WooLam
HOL-Auth: theory Yahalom
HOL-Auth: theory Yahalom2
HOL-Auth: theory P2
HOL-Auth: theory P1
HOL-Auth: theory Yahalom_Bad
HOL-Auth: theory ZhouGollmann
HOL-Auth: theory Guard_Shared
HOL-Auth: theory Smartcard
HOL-Auth: theory TLS
HOL-Auth: theory Guard_OtwayRees
HOL-Auth: theory Guard_Yahalom
HOL-Auth: theory ShoupRubin
HOL-Auth: theory Auth_Shared
HOL-Auth: theory ShoupRubinBella
HOL-Auth: theory Auth_Guard_Shared
HOL-Auth: theory Auth_Public
HOL-Auth: theory Auth_Smartcard
HOL-Auth: theory Auth_Guard_Public
Timing HOL-Auth (7 threads, 44.841s elapsed time, 256.205s cpu time, 20.624s GC time, factor 5.71)
Finished HOL-Auth (0:00:47 elapsed time, 0:04:17 cpu time, factor 5.46)
Running HOL-Bali ...
HOL-Bali: theory Wfrec
HOL-Bali: theory Old_Recdef
HOL-Bali: theory Basis
HOL-Bali: theory Name
HOL-Bali: theory Table
HOL-Bali: theory Type
HOL-Bali: theory Value
HOL-Bali: theory Term
HOL-Bali: theory Decl
HOL-Bali: theory TypeRel
HOL-Bali: theory DeclConcepts
HOL-Bali: theory State
HOL-Bali: theory WellType
HOL-Bali: theory Conform
HOL-Bali: theory Eval
HOL-Bali: theory DefiniteAssignment
HOL-Bali: theory WellForm
HOL-Bali: theory DefiniteAssignmentCorrect
HOL-Bali: theory Example
HOL-Bali: theory TypeSafe
HOL-Bali: theory Evaln
HOL-Bali: theory AxSem
HOL-Bali: theory Trans
HOL-Bali: theory AxCompl
HOL-Bali: theory AxSound
HOL-Bali: theory AxExample
Timing HOL-Bali (7 threads, 42.289s elapsed time, 162.912s cpu time, 9.634s GC time, factor 3.85)
Finished HOL-Bali (0:00:45 elapsed time, 0:02:44 cpu time, factor 3.64)
Running HOL-Decision_Procs ...
HOL-Decision_Procs: theory DP_Library
HOL-Decision_Procs: theory Code_Binary_Nat
HOL-Decision_Procs: theory Code_Natural
HOL-Decision_Procs: theory Dense_Linear_Order
HOL-Decision_Procs: theory Commutative_Ring
HOL-Decision_Procs: theory Abstract_Rat
HOL-Decision_Procs: theory Lattice_Algebras
HOL-Decision_Procs: theory Code_Integer
HOL-Decision_Procs: theory Polynomial_List
HOL-Decision_Procs: theory Reflection
HOL-Decision_Procs: theory Efficient_Nat
HOL-Decision_Procs: theory Wfrec
HOL-Decision_Procs: theory Old_Recdef
HOL-Decision_Procs: theory Reflected_Multivariate_Polynomial
HOL-Decision_Procs: theory Cooper
HOL-Decision_Procs: theory Dense_Linear_Order_Ex
HOL-Decision_Procs: theory Ferrack
HOL-Decision_Procs: theory MIR
HOL-Decision_Procs: theory Float
HOL-Decision_Procs: theory Commutative_Ring_Complete
HOL-Decision_Procs: theory Commutative_Ring_Ex
HOL-Decision_Procs: theory Approximation
HOL-Decision_Procs: theory Parametric_Ferrante_Rackoff
HOL-Decision_Procs: theory Approximation_Ex
HOL-Decision_Procs: theory Decision_Procs
Timing HOL-Decision_Procs (7 threads, 74.938s elapsed time, 476.670s cpu time, 45.260s GC time, factor 6.36)
Finished HOL-Decision_Procs (0:01:17 elapsed time, 0:07:57 cpu time, factor 6.19)
Running HOL-Hoare_Parallel ...
HOL-Hoare_Parallel: theory Graph
HOL-Hoare_Parallel: theory RG_Com
HOL-Hoare_Parallel: theory Quote_Antiquote
HOL-Hoare_Parallel: theory OG_Com
HOL-Hoare_Parallel: theory RG_Tran
HOL-Hoare_Parallel: theory RG_Hoare
HOL-Hoare_Parallel: theory OG_Tran
HOL-Hoare_Parallel: theory RG_Syntax
HOL-Hoare_Parallel: theory RG_Examples
HOL-Hoare_Parallel: theory OG_Hoare
HOL-Hoare_Parallel: theory OG_Tactics
HOL-Hoare_Parallel: theory OG_Syntax
HOL-Hoare_Parallel: theory Gar_Coll
HOL-Hoare_Parallel: theory Mul_Gar_Coll
HOL-Hoare_Parallel: theory OG_Examples
HOL-Hoare_Parallel: theory Hoare_Parallel
Timing HOL-Hoare_Parallel (7 threads, 37.045s elapsed time, 232.547s cpu time, 5.469s GC time, factor 6.28)
Finished HOL-Hoare_Parallel (0:00:39 elapsed time, 0:03:53 cpu time, factor 5.97)
Running HOL-IMP ...
HOL-IMP: theory Char_nat
HOL-IMP: theory List_lexord
HOL-IMP: theory While_Combinator
HOL-IMP: theory Interpretation_with_Defs
HOL-IMP: theory Char_ord
HOL-IMP: theory AExp
HOL-IMP: theory C_like
HOL-IMP: theory Complete_Lattice
HOL-IMP: theory Complete_Lattice_ix
HOL-IMP: theory OO
HOL-IMP: theory Star
HOL-IMP: theory Types
HOL-IMP: theory Poly_Types
HOL-IMP: theory ASM
HOL-IMP: theory BExp
HOL-IMP: theory Com
HOL-IMP: theory Procs
HOL-IMP: theory Vars
HOL-IMP: theory ACom
HOL-IMP: theory ACom_ITP
HOL-IMP: theory Abs_Int_Tests
HOL-IMP: theory Big_Step
HOL-IMP: theory Procs_Dyn_Vars_Dyn
HOL-IMP: theory Procs_Stat_Vars_Dyn
HOL-IMP: theory Procs_Stat_Vars_Stat
HOL-IMP: theory Collecting_ITP
HOL-IMP: theory Compiler
HOL-IMP: theory Denotation
HOL-IMP: theory Hoare
HOL-IMP: theory Sec_Type_Expr
HOL-IMP: theory Sem_Equiv
HOL-IMP: theory Hoare_Examples
HOL-IMP: theory Hoare_Sound_Complete
HOL-IMP: theory VC
HOL-IMP: theory Fold
HOL-IMP: theory HoareT
HOL-IMP: theory Sec_Typing
HOL-IMP: theory Sec_TypingT
HOL-IMP: theory Def_Init
HOL-IMP: theory Def_Init_Exp
HOL-IMP: theory Live
HOL-IMP: theory Collecting
HOL-IMP: theory Small_Step
HOL-IMP: theory Def_Init_Big
HOL-IMP: theory Def_Init_Sound_Big
HOL-IMP: theory Def_Init_Small
HOL-IMP: theory Live_True
HOL-IMP: theory Def_Init_Sound_Small
HOL-IMP: theory Abs_Int_den0_fun
HOL-IMP: theory Abs_Int0_ITP
HOL-IMP: theory Abs_State_den
HOL-IMP: theory Abs_Int_den0
HOL-IMP: theory Finite_Reachable
HOL-IMP: theory Abs_Int_den0_const
HOL-IMP: theory Collecting1
HOL-IMP: theory Collecting_Examples
HOL-IMP: theory Abs_Int_init
HOL-IMP: theory Abs_Int0
HOL-IMP: theory Abs_State_ITP
HOL-IMP: theory Abs_Int1_ITP
HOL-IMP: theory Comp_Rev
HOL-IMP: theory Abs_Int1_const_ITP
HOL-IMP: theory Abs_Int1_parity_ITP
HOL-IMP: theory Abs_Int2_ITP
HOL-IMP: theory Abs_Int_den1
HOL-IMP: theory Abs_State
HOL-IMP: theory Abs_Int2_ivl_ITP
HOL-IMP: theory Abs_Int_den1_ivl
HOL-IMP: theory Abs_Int1
HOL-IMP: theory Abs_Int1_const
HOL-IMP: theory Abs_Int1_parity
HOL-IMP: theory Abs_Int2
HOL-IMP: theory Abs_Int2_ivl
HOL-IMP: theory Abs_Int3_ITP
HOL-IMP: theory Abs_Int_den2
HOL-IMP: theory Abs_Int3
Timing HOL-IMP (7 threads, 86.426s elapsed time, 499.778s cpu time, 48.706s GC time, factor 5.78)
Finished HOL-IMP (0:01:28 elapsed time, 0:08:21 cpu time, factor 5.69)
Running HOL-Library ...
HOL-Library: theory Adhoc_Overloading
HOL-Library: theory Lattice_Syntax
HOL-Library: theory Refute
HOL-Library: theory Preorder
HOL-Library: theory AList
HOL-Library: theory Bit
HOL-Library: theory Boolean_Algebra
HOL-Library: theory Char_nat
HOL-Library: theory Code_Binary_Nat
HOL-Library: theory Code_Char
HOL-Library: theory Code_Natural
HOL-Library: theory Code_Integer
HOL-Library: theory Code_Numeral_Types
HOL-Library: theory Char_ord
HOL-Library: theory Code_Char_chr
HOL-Library: theory Continuity
HOL-Library: theory Code_Char_ord
HOL-Library: theory Debug
HOL-Library: theory Dlist
HOL-Library: theory Efficient_Nat
HOL-Library: theory Eval_Witness
HOL-Library: theory Extended_Nat
HOL-Library: theory Fraction_Field
HOL-Library: theory FuncSet
HOL-Library: theory IArray
HOL-Library: theory Function_Algebras
HOL-Library: theory Function_Division
HOL-Library: theory Indicator_Function
HOL-Library: theory Infinite_Set
HOL-Library: theory Kleene_Algebra
HOL-Library: theory DAList
HOL-Library: theory LaTeXsugar
HOL-Library: theory ListVector
HOL-Library: theory List_lexord
HOL-Library: theory Monad_Syntax
HOL-Library: theory Option_ord
HOL-Library: theory Order_Relation
HOL-Library: theory Parallel
HOL-Library: theory Code_Target_Int
HOL-Library: theory Code_Target_Nat
HOL-Library: theory Zorn
HOL-Library: theory Diagonal_Subsequence
HOL-Library: theory Nat_Bijection
HOL-Library: theory Abstract_Rat
HOL-Library: theory Code_Target_Numeral
HOL-Library: theory Binomial
HOL-Library: theory Code_Real_Approx_By_Float
HOL-Library: theory ContNotDenum
HOL-Library: theory Formal_Power_Series
HOL-Library: theory FrechetDeriv
HOL-Library: theory Lattice_Algebras
HOL-Library: theory Countable
HOL-Library: theory Multiset
HOL-Library: theory Inner_Product
HOL-Library: theory OptionalSugar
HOL-Library: theory Sum_of_Squares
HOL-Library: theory Countable_Set
HOL-Library: theory Permutations
HOL-Library: theory Phantom_Type
HOL-Library: theory Polynomial
HOL-Library: theory Product_plus
HOL-Library: theory Cardinality
HOL-Library: theory Product_Lattice
HOL-Library: theory Finite_Lattice
HOL-Library: theory Permutation
HOL-Library: theory Product_Vector
HOL-Library: theory FinFun
HOL-Library: theory Numeral_Type
HOL-Library: theory Fundamental_Theorem_Algebra
HOL-Library: theory Poly_Deriv
HOL-Library: theory Float
HOL-Library: theory Convex
HOL-Library: theory Quotient_Syntax
HOL-Library: theory Quotient_Option
HOL-Library: theory Quotient_Product
HOL-Library: theory Quotient_Set
HOL-Library: theory Quotient_Sum
HOL-Library: theory Quotient_Type
HOL-Library: theory Type_Length
HOL-Library: theory RBT_Impl
HOL-Library: theory Mapping
HOL-Library: theory Quotient_List
HOL-Library: theory Ramsey
HOL-Library: theory Reflection
HOL-Library: theory Saturated
HOL-Library: theory Set_Algebras
HOL-Library: theory State_Monad
HOL-Library: theory Sublist
HOL-Library: theory AList_Mapping
HOL-Library: theory Transitive_Closure_Table
HOL-Library: theory BigO
HOL-Library: theory Univ_Poly
HOL-Library: theory Wfrec
HOL-Library: theory Old_Recdef
HOL-Library: theory Sublist_Order
HOL-Library: theory While_Combinator
HOL-Library: theory RBT
HOL-Library: theory RBT_Mapping
HOL-Library: theory Library
Skipping theories "Sum_of_Squares_Remote" (undefined ISABELLE_FULL_TEST)
Timing HOL-Library (7 threads, 44.101s elapsed time, 253.206s cpu time, 22.124s GC time, factor 5.74)
Finished HOL-Library (0:00:46 elapsed time, 0:04:14 cpu time, factor 5.52)
Running HOL-MicroJava ...
HOL-MicroJava: theory While_Combinator
HOL-MicroJava: theory Transitive_Closure_Table
HOL-MicroJava: theory Wfrec
HOL-MicroJava: theory Semilat
HOL-MicroJava: theory Err
HOL-MicroJava: theory Listn
HOL-MicroJava: theory Opt
HOL-MicroJava: theory Product
HOL-MicroJava: theory JBasis
HOL-MicroJava: theory AuxLemmas
HOL-MicroJava: theory Type
HOL-MicroJava: theory Typing_Framework
HOL-MicroJava: theory Semilattices
HOL-MicroJava: theory SemilatAlg
HOL-MicroJava: theory Kildall
HOL-MicroJava: theory LBVSpec
HOL-MicroJava: theory Typing_Framework_err
HOL-MicroJava: theory LBVComplete
HOL-MicroJava: theory LBVCorrect
HOL-MicroJava: theory Abstract_BV
HOL-MicroJava: theory Decl
HOL-MicroJava: theory Value
HOL-MicroJava: theory SystemClasses
HOL-MicroJava: theory TypeRel
HOL-MicroJava: theory Term
HOL-MicroJava: theory State
HOL-MicroJava: theory WellForm
HOL-MicroJava: theory Exceptions
HOL-MicroJava: theory JType
HOL-MicroJava: theory JVMType
HOL-MicroJava: theory WellType
HOL-MicroJava: theory Conform
HOL-MicroJava: theory Eval
HOL-MicroJava: theory TypeInf
HOL-MicroJava: theory JVMState
HOL-MicroJava: theory JVMInstructions
HOL-MicroJava: theory JVMExceptions
HOL-MicroJava: theory JVMExecInstr
HOL-MicroJava: theory Effect
HOL-MicroJava: theory JVMExec
HOL-MicroJava: theory JVMDefensive
HOL-MicroJava: theory DefsComp
HOL-MicroJava: theory JVMListExample
HOL-MicroJava: theory Index
HOL-MicroJava: theory TranslCompTp
HOL-MicroJava: theory TranslComp
HOL-MicroJava: theory Example
HOL-MicroJava: theory JListExample
HOL-MicroJava: theory JTypeSafe
HOL-MicroJava: theory LemmasComp
HOL-MicroJava: theory CorrComp
HOL-MicroJava: theory BVSpec
HOL-MicroJava: theory EffectMono
HOL-MicroJava: theory Altern
HOL-MicroJava: theory Correct
HOL-MicroJava: theory Typing_Framework_JVM
HOL-MicroJava: theory BVSpecTypeSafe
HOL-MicroJava: theory JVM
HOL-MicroJava: theory LBVJVM
HOL-MicroJava: theory CorrCompTp
HOL-MicroJava: theory BVNoTypeError
HOL-MicroJava: theory BVExample
HOL-MicroJava: theory MicroJava
Timing HOL-MicroJava (7 threads, 44.014s elapsed time, 237.914s cpu time, 12.575s GC time, factor 5.41)
Finished HOL-MicroJava (0:00:46 elapsed time, 0:03:59 cpu time, factor 5.19)
Running HOL-Probability ...
HOL-Probability: theory AList
HOL-Probability: theory DAList
HOL-Probability: theory Multiset
HOL-Probability: theory Permutation
HOL-Probability: theory Sigma_Algebra
HOL-Probability: theory Diagonal_Subsequence
HOL-Probability: theory Discrete_Topology
HOL-Probability: theory Measurable
HOL-Probability: theory Measure_Space
HOL-Probability: theory Borel_Space
HOL-Probability: theory Caratheodory
HOL-Probability: theory Lebesgue_Integration
HOL-Probability: theory Regularity
HOL-Probability: theory Binary_Product_Measure
HOL-Probability: theory Complete_Measure
HOL-Probability: theory Radon_Nikodym
HOL-Probability: theory Finite_Product_Measure
HOL-Probability: theory Fin_Map
HOL-Probability: theory Lebesgue_Measure
HOL-Probability: theory Probability_Measure
HOL-Probability: theory Distributions
HOL-Probability: theory Projective_Family
HOL-Probability: theory Infinite_Product_Measure
HOL-Probability: theory Independent_Family
HOL-Probability: theory Projective_Limit
HOL-Probability: theory Information
HOL-Probability: theory Dining_Cryptographers
HOL-Probability: theory Koepf_Duermuth_Countermeasure
HOL-Probability: theory Probability
Timing HOL-Probability (7 threads, 30.269s elapsed time, 174.415s cpu time, 7.411s GC time, factor 5.76)
Finished HOL-Probability (0:00:34 elapsed time, 0:02:56 cpu time, factor 5.17)
Running HOL-Proofs-Extraction ...
HOL-Proofs-Extraction: theory Adhoc_Overloading
HOL-Proofs-Extraction: theory AList
HOL-Proofs-Extraction: theory Code_Binary_Nat
HOL-Proofs-Extraction: theory Code_Natural
HOL-Proofs-Extraction: theory Fact
HOL-Proofs-Extraction: theory Parity
HOL-Proofs-Extraction: theory Monad_Syntax
HOL-Proofs-Extraction: theory Code_Integer
HOL-Proofs-Extraction: theory State_Monad
HOL-Proofs-Extraction: theory Efficient_Nat
HOL-Proofs-Extraction: theory DAList
HOL-Proofs-Extraction: theory Multiset
HOL-Proofs-Extraction: theory GCD
HOL-Proofs-Extraction: theory Primes
HOL-Proofs-Extraction: theory Cong
HOL-Proofs-Extraction: theory UniqueFactorization
HOL-Proofs-Extraction: theory Higman
HOL-Proofs-Extraction: theory Util
HOL-Proofs-Extraction: theory Warshall
HOL-Proofs-Extraction: theory Euclid
HOL-Proofs-Extraction: theory Pigeonhole
HOL-Proofs-Extraction: theory QuotRem
HOL-Proofs-Extraction: theory Higman_Extraction
HOL-Proofs-Extraction: theory Greatest_Common_Divisor
Timing HOL-Proofs-Extraction (7 threads, 107.828s elapsed time, 388.367s cpu time, 32.169s GC time, factor 3.60)
Finished HOL-Proofs-Extraction (0:01:50 elapsed time, 0:06:29 cpu time, factor 3.53)
Running HOL-SET_Protocol ...
HOL-SET_Protocol: theory Nat_Bijection
HOL-SET_Protocol: theory Message_SET
HOL-SET_Protocol: theory Event_SET
HOL-SET_Protocol: theory Public_SET
HOL-SET_Protocol: theory Cardholder_Registration
HOL-SET_Protocol: theory Merchant_Registration
HOL-SET_Protocol: theory Purchase
HOL-SET_Protocol: theory SET_Protocol
Timing HOL-SET_Protocol (7 threads, 14.565s elapsed time, 73.988s cpu time, 1.818s GC time, factor 5.08)
Finished HOL-SET_Protocol (0:00:16 elapsed time, 0:01:15 cpu time, factor 4.68)
Running HOL-UNITY ...
HOL-UNITY: theory Message
HOL-UNITY: theory Event
HOL-UNITY: theory Public
HOL-UNITY: theory AList
HOL-UNITY: theory UNITY
HOL-UNITY: theory ListOrder
HOL-UNITY: theory Constrains
HOL-UNITY: theory Deadlock
HOL-UNITY: theory FP
HOL-UNITY: theory Network
HOL-UNITY: theory WFair
HOL-UNITY: theory SubstAx
HOL-UNITY: theory Token
HOL-UNITY: theory DAList
HOL-UNITY: theory Detects
HOL-UNITY: theory Union
HOL-UNITY: theory Comp
HOL-UNITY: theory Guar
HOL-UNITY: theory Transformers
HOL-UNITY: theory Multiset
HOL-UNITY: theory Extend
HOL-UNITY: theory ProgressSets
HOL-UNITY: theory Project
HOL-UNITY: theory Rename
HOL-UNITY: theory Lift_prog
HOL-UNITY: theory ELT
HOL-UNITY: theory PPROD
HOL-UNITY: theory Follows
HOL-UNITY: theory UNITY_Main
HOL-UNITY: theory AllocBase
HOL-UNITY: theory Channel
HOL-UNITY: theory Common
HOL-UNITY: theory Counter
HOL-UNITY: theory Counterc
HOL-UNITY: theory Alloc
HOL-UNITY: theory AllocImpl
HOL-UNITY: theory Client
HOL-UNITY: theory Handshake
HOL-UNITY: theory Lift
HOL-UNITY: theory Mutex
HOL-UNITY: theory NSP_Bad
HOL-UNITY: theory PriorityAux
HOL-UNITY: theory Priority
HOL-UNITY: theory Progress
HOL-UNITY: theory Reach
HOL-UNITY: theory TimerArray
HOL-UNITY: theory Reachability
Timing HOL-UNITY (7 threads, 14.185s elapsed time, 75.896s cpu time, 3.926s GC time, factor 5.35)
Finished HOL-UNITY (0:00:16 elapsed time, 0:01:16 cpu time, factor 4.75)
Running ZF-UNITY ...
ZF-UNITY: theory FoldSet
ZF-UNITY: theory State
ZF-UNITY: theory GenPrefix
ZF-UNITY: theory Acc
ZF-UNITY: theory UNITY
ZF-UNITY: theory Multiset
ZF-UNITY: theory Constrains
ZF-UNITY: theory FP
ZF-UNITY: theory WFair
ZF-UNITY: theory SubstAx
ZF-UNITY: theory MultisetSum
ZF-UNITY: theory Monotonicity
ZF-UNITY: theory Mutex
ZF-UNITY: theory Union
ZF-UNITY: theory Increasing
ZF-UNITY: theory Follows
ZF-UNITY: theory Comp
ZF-UNITY: theory Guar
ZF-UNITY: theory AllocBase
ZF-UNITY: theory ClientImpl
ZF-UNITY: theory Distributor
ZF-UNITY: theory Merge
ZF-UNITY: theory AllocImpl
Timing ZF-UNITY (7 threads, 5.465s elapsed time, 33.418s cpu time, 1.373s GC time, factor 6.12)
Finished ZF-UNITY (0:00:06 elapsed time, 0:00:33 cpu time, factor 5.50)
Finished at Mon Feb 4 21:10:14 CET 2013
0:16:19 elapsed time, 1:15:18 cpu time, factor 4.61
*** m=8 q=2 ***
Started at Mon Feb 4 21:10:14 CET 2013 (polyml-5.5.0_x86-darwin on lri29-163.lri.fr)
ISABELLE_BUILD_OPTIONS="threads_trace=2 threads=8 parallel_proofs=2"
ML_PLATFORM="x86-darwin"
ML_HOME="/Volumes/Macintosh_HD/Users/makarius/.isabelle/contrib/polyml-5.5.0-3/x86-darwin"
ML_SYSTEM="polyml-5.5.0"
ML_OPTIONS="--minheap 1000 --gcthreads 8"
Session Pure
Session HOL (main)
Session HOL-Auth
Session HOL-Bali
Session HOL-Decision_Procs
Session HOL-Hoare_Parallel
Session HOL-IMP
Session HOL-Library (main)
Session HOL-MicroJava
Session HOL-Multivariate_Analysis (main)
Session HOL-Probability
Session HOL-Nominal (main)
Session HOL-Nominal-Examples
Session HOL-SET_Protocol
Session HOL-UNITY
Session HOL-Proofs
Session HOL-Proofs-Extraction
Session ZF (main)
Session ZF-UNITY
Building Pure ...
Finished Pure (0:00:09 elapsed time, 0:00:10 cpu time, factor 1.11)
Building HOL ...
HOL: theory Code_Generator
HOL: theory HOL
HOL: theory Orderings
HOL: theory SAT
HOL: theory Groups
HOL: theory Rings
HOL: theory Lattices
HOL: theory Set
HOL: theory Complete_Lattices
HOL: theory Typedef
HOL: theory Fun
HOL: theory Inductive
HOL: theory Fields
HOL: theory Product_Type
HOL: theory Sum_Type
HOL: theory Complete_Partial_Order
HOL: theory Nat
HOL: theory Datatype
HOL: theory Meson
HOL: theory Num
HOL: theory Option
HOL: theory Extraction
HOL: theory Partial_Function
HOL: theory ATP
HOL: theory Power
HOL: theory Metis
HOL: theory Finite_Set
HOL: theory Relation
HOL: theory Transitive_Closure
HOL: theory Wellfounded
HOL: theory FunDef
HOL: theory Plain
HOL: theory Big_Operators
HOL: theory Hilbert_Choice
HOL: theory Equiv_Relations
HOL: theory Transfer
HOL: theory Lifting
HOL: theory Quotient
HOL: theory Int
HOL: theory Nat_Transfer
HOL: theory Divides
HOL: theory Set_Interval
HOL: theory Code_Numeral
HOL: theory Numeral_Simprocs
HOL: theory Semiring_Normalization
HOL: theory Groebner_Basis
HOL: theory Presburger
HOL: theory List
HOL: theory Map
HOL: theory Random
HOL: theory Predicate
HOL: theory Enum
HOL: theory Lazy_Sequence
HOL: theory String
HOL: theory DSequence
HOL: theory New_DSequence
HOL: theory Typerep
HOL: theory Code_Evaluation
HOL: theory Quickcheck
HOL: theory Quickcheck_Exhaustive
HOL: theory Random_Sequence
HOL: theory New_Random_Sequence
HOL: theory Quickcheck_Narrowing
HOL: theory Predicate_Compile
HOL: theory Record
HOL: theory SMT
HOL: theory Sledgehammer
HOL: theory Nitpick
HOL: theory Main
HOL: theory Archimedean_Field
HOL: theory Lubs
HOL: theory Fact
HOL: theory Parity
HOL: theory GCD
HOL: theory Rat
HOL: theory RealDef
HOL: theory RComplete
HOL: theory RealVector
HOL: theory SupInf
HOL: theory Limits
HOL: theory Real
HOL: theory SEQ
HOL: theory Lim
HOL: theory Deriv
HOL: theory Series
HOL: theory NthRoot
HOL: theory Transcendental
HOL: theory Complex
HOL: theory Ln
HOL: theory Log
HOL: theory MacLaurin
HOL: theory Taylor
HOL: theory Complex_Main
Timing HOL (8 threads, 84.487s elapsed time, 233.848s cpu time, 15.634s GC time, factor 2.77)
Finished HOL (0:01:46 elapsed time, 0:04:37 cpu time, factor 2.61)
Building HOL-Multivariate_Analysis ...
HOL-Multivariate_Analysis: theory Extended_Nat
HOL-Multivariate_Analysis: theory FuncSet
HOL-Multivariate_Analysis: theory Indicator_Function
HOL-Multivariate_Analysis: theory Glbs
HOL-Multivariate_Analysis: theory Infinite_Set
HOL-Multivariate_Analysis: theory Nat_Bijection
HOL-Multivariate_Analysis: theory L2_Norm
HOL-Multivariate_Analysis: theory FrechetDeriv
HOL-Multivariate_Analysis: theory Sum_of_Squares
HOL-Multivariate_Analysis: theory Permutations
HOL-Multivariate_Analysis: theory Phantom_Type
HOL-Multivariate_Analysis: theory Inner_Product
HOL-Multivariate_Analysis: theory Product_plus
HOL-Multivariate_Analysis: theory Set_Algebras
HOL-Multivariate_Analysis: theory Cardinality
HOL-Multivariate_Analysis: theory Countable
HOL-Multivariate_Analysis: theory Extended_Real
HOL-Multivariate_Analysis: theory Product_Vector
HOL-Multivariate_Analysis: theory Countable_Set
HOL-Multivariate_Analysis: theory Convex
HOL-Multivariate_Analysis: theory Euclidean_Space
HOL-Multivariate_Analysis: theory Numeral_Type
HOL-Multivariate_Analysis: theory Finite_Cartesian_Product
HOL-Multivariate_Analysis: theory Linear_Algebra
HOL-Multivariate_Analysis: theory Norm_Arith
HOL-Multivariate_Analysis: theory Operator_Norm
HOL-Multivariate_Analysis: theory Topology_Euclidean_Space
HOL-Multivariate_Analysis: theory Extended_Real_Limits
HOL-Multivariate_Analysis: theory Convex_Euclidean_Space
HOL-Multivariate_Analysis: theory Brouwer_Fixpoint
HOL-Multivariate_Analysis: theory Path_Connected
HOL-Multivariate_Analysis: theory Derivative
HOL-Multivariate_Analysis: theory Integration
HOL-Multivariate_Analysis: theory Cartesian_Euclidean_Space
HOL-Multivariate_Analysis: theory Determinants
HOL-Multivariate_Analysis: theory Fashoda
HOL-Multivariate_Analysis: theory Multivariate_Analysis
Timing HOL-Multivariate_Analysis (8 threads, 28.610s elapsed time, 205.283s cpu time, 12.407s GC time, factor 7.18)
Finished HOL-Multivariate_Analysis (0:00:46 elapsed time, 0:03:53 cpu time, factor 5.06)
Building HOL-Nominal ...
HOL-Nominal: theory Infinite_Set
HOL-Nominal: theory Nominal
Timing HOL-Nominal (8 threads, 4.327s elapsed time, 9.371s cpu time, 0.453s GC time, factor 2.17)
Finished HOL-Nominal (0:00:14 elapsed time, 0:00:22 cpu time, factor 1.57)
Building HOL-Proofs ...
HOL-Proofs: theory Code_Generator
HOL-Proofs: theory HOL
HOL-Proofs: theory Orderings
HOL-Proofs: theory SAT
HOL-Proofs: theory Groups
HOL-Proofs: theory Rings
HOL-Proofs: theory Lattices
HOL-Proofs: theory Set
HOL-Proofs: theory Complete_Lattices
HOL-Proofs: theory Typedef
HOL-Proofs: theory Fun
HOL-Proofs: theory Inductive
HOL-Proofs: theory Fields
HOL-Proofs: theory Product_Type
HOL-Proofs: theory Sum_Type
HOL-Proofs: theory Complete_Partial_Order
HOL-Proofs: theory Nat
HOL-Proofs: theory Datatype
HOL-Proofs: theory Meson
HOL-Proofs: theory Option
HOL-Proofs: theory Num
HOL-Proofs: theory Extraction
HOL-Proofs: theory Partial_Function
HOL-Proofs: theory ATP
HOL-Proofs: theory Metis
HOL-Proofs: theory Power
HOL-Proofs: theory Finite_Set
HOL-Proofs: theory Relation
HOL-Proofs: theory Transitive_Closure
HOL-Proofs: theory Wellfounded
HOL-Proofs: theory FunDef
HOL-Proofs: theory Plain
HOL-Proofs: theory Big_Operators
HOL-Proofs: theory Hilbert_Choice
HOL-Proofs: theory Equiv_Relations
HOL-Proofs: theory Transfer
HOL-Proofs: theory Lifting
HOL-Proofs: theory Quotient
HOL-Proofs: theory Int
HOL-Proofs: theory Nat_Transfer
HOL-Proofs: theory Divides
HOL-Proofs: theory Set_Interval
HOL-Proofs: theory Code_Numeral
HOL-Proofs: theory Numeral_Simprocs
HOL-Proofs: theory Semiring_Normalization
HOL-Proofs: theory Groebner_Basis
HOL-Proofs: theory Presburger
HOL-Proofs: theory List
HOL-Proofs: theory Map
HOL-Proofs: theory Predicate
HOL-Proofs: theory Random
HOL-Proofs: theory Enum
HOL-Proofs: theory Lazy_Sequence
HOL-Proofs: theory String
HOL-Proofs: theory DSequence
HOL-Proofs: theory New_DSequence
HOL-Proofs: theory Typerep
HOL-Proofs: theory Code_Evaluation
HOL-Proofs: theory Quickcheck
HOL-Proofs: theory Quickcheck_Exhaustive
HOL-Proofs: theory Random_Sequence
HOL-Proofs: theory New_Random_Sequence
HOL-Proofs: theory Quickcheck_Narrowing
HOL-Proofs: theory Predicate_Compile
HOL-Proofs: theory Record
HOL-Proofs: theory SMT
HOL-Proofs: theory Sledgehammer
HOL-Proofs: theory Nitpick
HOL-Proofs: theory Main
Timing HOL-Proofs (8 threads, 81.118s elapsed time, 386.649s cpu time, 39.967s GC time, factor 4.77)
Finished HOL-Proofs (0:01:50 elapsed time, 0:07:27 cpu time, factor 4.06)
Building ZF ...
ZF: theory IFOL
ZF: theory FOL
ZF: theory ZF
ZF: theory upair
ZF: theory pair
ZF: theory Bool
ZF: theory equalities
ZF: theory Fixedpt
ZF: theory Sum
ZF: theory func
ZF: theory Perm
ZF: theory QPair
ZF: theory Trancl
ZF: theory EquivClass
ZF: theory WF
ZF: theory Order
ZF: theory Ordinal
ZF: theory OrdQuant
ZF: theory OrderArith
ZF: theory Nat_ZF
ZF: theory Epsilon
ZF: theory OrderType
ZF: theory Inductive_ZF
ZF: theory Finite
ZF: theory Cardinal
ZF: theory Univ
ZF: theory Arith
ZF: theory QUniv
ZF: theory Datatype_ZF
ZF: theory ArithSimp
ZF: theory Int_ZF
ZF: theory CardinalArith
ZF: theory List_ZF
ZF: theory Bin
ZF: theory IntArith
ZF: theory IntDiv_ZF
ZF: theory Main_ZF
ZF: theory AC
ZF: theory Main
ZF: theory Zorn
ZF: theory Cardinal_AC
ZF: theory InfDatatype
ZF: theory Main_ZFC
Timing ZF (8 threads, 7.337s elapsed time, 29.184s cpu time, 1.657s GC time, factor 3.98)
Finished ZF (0:00:11 elapsed time, 0:00:33 cpu time, factor 3.00)
Running HOL-Nominal-Examples ...
HOL-Nominal-Examples: theory CK_Machine
HOL-Nominal-Examples: theory CR_Takahashi
HOL-Nominal-Examples: theory Class1
HOL-Nominal-Examples: theory Crary
HOL-Nominal-Examples: theory Contexts
HOL-Nominal-Examples: theory Compile
HOL-Nominal-Examples: theory Fsub
HOL-Nominal-Examples: theory Height
HOL-Nominal-Examples: theory Lam_Funs
HOL-Nominal-Examples: theory Lambda_mu
HOL-Nominal-Examples: theory LocalWeakening
HOL-Nominal-Examples: theory CR
HOL-Nominal-Examples: theory SN
HOL-Nominal-Examples: theory Pattern
HOL-Nominal-Examples: theory SOS
HOL-Nominal-Examples: theory Standardization
HOL-Nominal-Examples: theory Support
HOL-Nominal-Examples: theory Type_Preservation
HOL-Nominal-Examples: theory W
HOL-Nominal-Examples: theory Weakening
HOL-Nominal-Examples: theory Class2
HOL-Nominal-Examples: theory Class3
HOL-Nominal-Examples: theory Nominal_Examples
HOL-Nominal-Examples: theory VC_Condition
Timing HOL-Nominal-Examples (8 threads, 92.151s elapsed time, 600.372s cpu time, 51.740s GC time, factor 6.52)
Finished HOL-Nominal-Examples (0:01:34 elapsed time, 0:10:02 cpu time, factor 6.40)
Running HOL-Auth ...
HOL-Auth: theory Message
HOL-Auth: theory Nat_Bijection
HOL-Auth: theory All_Symmetric
HOL-Auth: theory Event
HOL-Auth: theory EventSC
HOL-Auth: theory Extensions
HOL-Auth: theory Public
HOL-Auth: theory Shared
HOL-Auth: theory CertifiedEmail
HOL-Auth: theory KerberosIV
HOL-Auth: theory KerberosIV_Gets
HOL-Auth: theory KerberosV
HOL-Auth: theory Kerberos_BAN
HOL-Auth: theory Kerberos_BAN_Gets
HOL-Auth: theory Analz
HOL-Auth: theory List_Msg
HOL-Auth: theory NS_Public
HOL-Auth: theory Guard
HOL-Auth: theory GuardK
HOL-Auth: theory NS_Public_Bad
HOL-Auth: theory NS_Shared
HOL-Auth: theory Guard_Public
HOL-Auth: theory OtwayRees
HOL-Auth: theory OtwayReesBella
HOL-Auth: theory OtwayRees_AN
HOL-Auth: theory OtwayRees_Bad
HOL-Auth: theory Guard_NS_Public
HOL-Auth: theory Proto
HOL-Auth: theory Recur
HOL-Auth: theory WooLam
HOL-Auth: theory Yahalom
HOL-Auth: theory Yahalom2
HOL-Auth: theory Yahalom_Bad
HOL-Auth: theory ZhouGollmann
HOL-Auth: theory Guard_Shared
HOL-Auth: theory Smartcard
HOL-Auth: theory TLS
HOL-Auth: theory P2
HOL-Auth: theory P1
HOL-Auth: theory Guard_OtwayRees
HOL-Auth: theory Guard_Yahalom
HOL-Auth: theory ShoupRubin
HOL-Auth: theory Auth_Shared
HOL-Auth: theory ShoupRubinBella
HOL-Auth: theory Auth_Guard_Shared
HOL-Auth: theory Auth_Public
HOL-Auth: theory Auth_Smartcard
HOL-Auth: theory Auth_Guard_Public
Timing HOL-Auth (8 threads, 40.553s elapsed time, 260.642s cpu time, 21.098s GC time, factor 6.43)
Finished HOL-Auth (0:00:42 elapsed time, 0:04:21 cpu time, factor 6.21)
Running HOL-Bali ...
HOL-Bali: theory Wfrec
HOL-Bali: theory Old_Recdef
HOL-Bali: theory Basis
HOL-Bali: theory Name
HOL-Bali: theory Table
HOL-Bali: theory Type
HOL-Bali: theory Value
HOL-Bali: theory Term
HOL-Bali: theory Decl
HOL-Bali: theory TypeRel
HOL-Bali: theory DeclConcepts
HOL-Bali: theory State
HOL-Bali: theory WellType
HOL-Bali: theory Conform
HOL-Bali: theory Eval
HOL-Bali: theory DefiniteAssignment
HOL-Bali: theory WellForm
HOL-Bali: theory DefiniteAssignmentCorrect
HOL-Bali: theory Example
HOL-Bali: theory TypeSafe
HOL-Bali: theory Evaln
HOL-Bali: theory AxSem
HOL-Bali: theory Trans
HOL-Bali: theory AxCompl
HOL-Bali: theory AxSound
HOL-Bali: theory AxExample
Timing HOL-Bali (8 threads, 40.979s elapsed time, 165.323s cpu time, 9.937s GC time, factor 4.03)
Finished HOL-Bali (0:00:42 elapsed time, 0:02:46 cpu time, factor 3.95)
Running HOL-Decision_Procs ...
HOL-Decision_Procs: theory Code_Binary_Nat
HOL-Decision_Procs: theory Code_Natural
HOL-Decision_Procs: theory DP_Library
HOL-Decision_Procs: theory Dense_Linear_Order
HOL-Decision_Procs: theory Commutative_Ring
HOL-Decision_Procs: theory Abstract_Rat
HOL-Decision_Procs: theory Lattice_Algebras
HOL-Decision_Procs: theory Polynomial_List
HOL-Decision_Procs: theory Code_Integer
HOL-Decision_Procs: theory Reflection
HOL-Decision_Procs: theory Wfrec
HOL-Decision_Procs: theory Efficient_Nat
HOL-Decision_Procs: theory Old_Recdef
HOL-Decision_Procs: theory Reflected_Multivariate_Polynomial
HOL-Decision_Procs: theory Cooper
HOL-Decision_Procs: theory Dense_Linear_Order_Ex
HOL-Decision_Procs: theory Ferrack
HOL-Decision_Procs: theory MIR
HOL-Decision_Procs: theory Float
HOL-Decision_Procs: theory Commutative_Ring_Complete
HOL-Decision_Procs: theory Commutative_Ring_Ex
HOL-Decision_Procs: theory Approximation
HOL-Decision_Procs: theory Parametric_Ferrante_Rackoff
HOL-Decision_Procs: theory Approximation_Ex
HOL-Decision_Procs: theory Decision_Procs
Timing HOL-Decision_Procs (8 threads, 68.300s elapsed time, 485.080s cpu time, 46.012s GC time, factor 7.10)
Finished HOL-Decision_Procs (0:01:10 elapsed time, 0:08:06 cpu time, factor 6.94)
Running HOL-Hoare_Parallel ...
HOL-Hoare_Parallel: theory Graph
HOL-Hoare_Parallel: theory Quote_Antiquote
HOL-Hoare_Parallel: theory RG_Com
HOL-Hoare_Parallel: theory OG_Com
HOL-Hoare_Parallel: theory RG_Tran
HOL-Hoare_Parallel: theory RG_Hoare
HOL-Hoare_Parallel: theory OG_Tran
HOL-Hoare_Parallel: theory RG_Syntax
HOL-Hoare_Parallel: theory RG_Examples
HOL-Hoare_Parallel: theory OG_Hoare
HOL-Hoare_Parallel: theory OG_Tactics
HOL-Hoare_Parallel: theory OG_Syntax
HOL-Hoare_Parallel: theory Gar_Coll
HOL-Hoare_Parallel: theory Mul_Gar_Coll
HOL-Hoare_Parallel: theory OG_Examples
HOL-Hoare_Parallel: theory Hoare_Parallel
Timing HOL-Hoare_Parallel (8 threads, 34.372s elapsed time, 234.636s cpu time, 5.580s GC time, factor 6.83)
Finished HOL-Hoare_Parallel (0:00:36 elapsed time, 0:03:55 cpu time, factor 6.52)
Running HOL-IMP ...
HOL-IMP: theory While_Combinator
HOL-IMP: theory List_lexord
HOL-IMP: theory Interpretation_with_Defs
HOL-IMP: theory Char_nat
HOL-IMP: theory Char_ord
HOL-IMP: theory AExp
HOL-IMP: theory C_like
HOL-IMP: theory Complete_Lattice
HOL-IMP: theory Complete_Lattice_ix
HOL-IMP: theory Star
HOL-IMP: theory OO
HOL-IMP: theory Types
HOL-IMP: theory Poly_Types
HOL-IMP: theory ASM
HOL-IMP: theory BExp
HOL-IMP: theory Com
HOL-IMP: theory Procs
HOL-IMP: theory Vars
HOL-IMP: theory ACom
HOL-IMP: theory ACom_ITP
HOL-IMP: theory Abs_Int_Tests
HOL-IMP: theory Big_Step
HOL-IMP: theory Procs_Dyn_Vars_Dyn
HOL-IMP: theory Procs_Stat_Vars_Dyn
HOL-IMP: theory Procs_Stat_Vars_Stat
HOL-IMP: theory Collecting_ITP
HOL-IMP: theory Compiler
HOL-IMP: theory Denotation
HOL-IMP: theory Hoare
HOL-IMP: theory Hoare_Examples
HOL-IMP: theory Hoare_Sound_Complete
HOL-IMP: theory VC
HOL-IMP: theory HoareT
HOL-IMP: theory Sec_Type_Expr
HOL-IMP: theory Sem_Equiv
HOL-IMP: theory Fold
HOL-IMP: theory Def_Init
HOL-IMP: theory Def_Init_Exp
HOL-IMP: theory Sec_Typing
HOL-IMP: theory Sec_TypingT
HOL-IMP: theory Def_Init_Big
HOL-IMP: theory Live
HOL-IMP: theory Collecting
HOL-IMP: theory Def_Init_Sound_Big
HOL-IMP: theory Def_Init_Small
HOL-IMP: theory Small_Step
HOL-IMP: theory Live_True
HOL-IMP: theory Def_Init_Sound_Small
HOL-IMP: theory Abs_Int_den0_fun
HOL-IMP: theory Abs_State_den
HOL-IMP: theory Abs_Int0_ITP
HOL-IMP: theory Abs_Int_den0
HOL-IMP: theory Abs_Int_den0_const
HOL-IMP: theory Finite_Reachable
HOL-IMP: theory Collecting1
HOL-IMP: theory Collecting_Examples
HOL-IMP: theory Abs_Int_init
HOL-IMP: theory Abs_Int0
HOL-IMP: theory Abs_State_ITP
HOL-IMP: theory Abs_Int1_ITP
HOL-IMP: theory Comp_Rev
HOL-IMP: theory Abs_Int1_const_ITP
HOL-IMP: theory Abs_Int1_parity_ITP
HOL-IMP: theory Abs_Int2_ITP
HOL-IMP: theory Abs_Int_den1
HOL-IMP: theory Abs_State
HOL-IMP: theory Abs_Int2_ivl_ITP
HOL-IMP: theory Abs_Int_den1_ivl
HOL-IMP: theory Abs_Int1
HOL-IMP: theory Abs_Int1_const
HOL-IMP: theory Abs_Int1_parity
HOL-IMP: theory Abs_Int2
HOL-IMP: theory Abs_Int2_ivl
HOL-IMP: theory Abs_Int3_ITP
HOL-IMP: theory Abs_Int_den2
HOL-IMP: theory Abs_Int3
Timing HOL-IMP (8 threads, 86.434s elapsed time, 507.539s cpu time, 49.968s GC time, factor 5.87)
Finished HOL-IMP (0:01:28 elapsed time, 0:08:29 cpu time, factor 5.78)
Running HOL-Library ...
HOL-Library: theory Adhoc_Overloading
HOL-Library: theory Preorder
HOL-Library: theory Lattice_Syntax
HOL-Library: theory Refute
HOL-Library: theory AList
HOL-Library: theory Bit
HOL-Library: theory Boolean_Algebra
HOL-Library: theory Char_nat
HOL-Library: theory Code_Binary_Nat
HOL-Library: theory Code_Char
HOL-Library: theory Code_Natural
HOL-Library: theory Code_Numeral_Types
HOL-Library: theory Code_Integer
HOL-Library: theory Continuity
HOL-Library: theory Char_ord
HOL-Library: theory Code_Char_chr
HOL-Library: theory Debug
HOL-Library: theory Dlist
HOL-Library: theory Efficient_Nat
HOL-Library: theory Code_Char_ord
HOL-Library: theory Eval_Witness
HOL-Library: theory Extended_Nat
HOL-Library: theory Fraction_Field
HOL-Library: theory FuncSet
HOL-Library: theory IArray
HOL-Library: theory Function_Algebras
HOL-Library: theory Function_Division
HOL-Library: theory Indicator_Function
HOL-Library: theory Infinite_Set
HOL-Library: theory Kleene_Algebra
HOL-Library: theory LaTeXsugar
HOL-Library: theory ListVector
HOL-Library: theory List_lexord
HOL-Library: theory DAList
HOL-Library: theory Monad_Syntax
HOL-Library: theory Option_ord
HOL-Library: theory Order_Relation
HOL-Library: theory Parallel
HOL-Library: theory Diagonal_Subsequence
HOL-Library: theory Nat_Bijection
HOL-Library: theory Code_Target_Int
HOL-Library: theory Code_Target_Nat
HOL-Library: theory Zorn
HOL-Library: theory Abstract_Rat
HOL-Library: theory Binomial
HOL-Library: theory Code_Target_Numeral
HOL-Library: theory Code_Real_Approx_By_Float
HOL-Library: theory ContNotDenum
HOL-Library: theory FrechetDeriv
HOL-Library: theory Lattice_Algebras
HOL-Library: theory Formal_Power_Series
HOL-Library: theory Countable
HOL-Library: theory OptionalSugar
HOL-Library: theory Inner_Product
HOL-Library: theory Sum_of_Squares
HOL-Library: theory Permutations
HOL-Library: theory Multiset
HOL-Library: theory Countable_Set
HOL-Library: theory Phantom_Type
HOL-Library: theory Polynomial
HOL-Library: theory Product_plus
HOL-Library: theory Quotient_Syntax
HOL-Library: theory Quotient_Option
HOL-Library: theory Cardinality
HOL-Library: theory Product_Lattice
HOL-Library: theory Finite_Lattice
HOL-Library: theory Product_Vector
HOL-Library: theory Convex
HOL-Library: theory Mapping
HOL-Library: theory FinFun
HOL-Library: theory Numeral_Type
HOL-Library: theory Fundamental_Theorem_Algebra
HOL-Library: theory Permutation
HOL-Library: theory Poly_Deriv
HOL-Library: theory Quotient_Product
HOL-Library: theory Float
HOL-Library: theory Quotient_Set
HOL-Library: theory AList_Mapping
HOL-Library: theory Quotient_Sum
HOL-Library: theory Quotient_Type
HOL-Library: theory Quotient_List
HOL-Library: theory RBT_Impl
HOL-Library: theory Type_Length
HOL-Library: theory Ramsey
HOL-Library: theory Reflection
HOL-Library: theory Saturated
HOL-Library: theory Set_Algebras
HOL-Library: theory State_Monad
HOL-Library: theory Sublist
HOL-Library: theory Transitive_Closure_Table
HOL-Library: theory Univ_Poly
HOL-Library: theory BigO
HOL-Library: theory Wfrec
HOL-Library: theory Sublist_Order
HOL-Library: theory While_Combinator
HOL-Library: theory Old_Recdef
HOL-Library: theory RBT
HOL-Library: theory RBT_Mapping
HOL-Library: theory Library
Skipping theories "Sum_of_Squares_Remote" (undefined ISABELLE_FULL_TEST)
Timing HOL-Library (8 threads, 43.236s elapsed time, 257.698s cpu time, 22.674s GC time, factor 5.96)
Finished HOL-Library (0:00:45 elapsed time, 0:04:18 cpu time, factor 5.73)
Running HOL-MicroJava ...
HOL-MicroJava: theory While_Combinator
HOL-MicroJava: theory Transitive_Closure_Table
HOL-MicroJava: theory Wfrec
HOL-MicroJava: theory Semilat
HOL-MicroJava: theory Err
HOL-MicroJava: theory Listn
HOL-MicroJava: theory Opt
HOL-MicroJava: theory Product
HOL-MicroJava: theory JBasis
HOL-MicroJava: theory AuxLemmas
HOL-MicroJava: theory Type
HOL-MicroJava: theory Typing_Framework
HOL-MicroJava: theory Semilattices
HOL-MicroJava: theory SemilatAlg
HOL-MicroJava: theory Kildall
HOL-MicroJava: theory LBVSpec
HOL-MicroJava: theory Typing_Framework_err
HOL-MicroJava: theory LBVComplete
HOL-MicroJava: theory LBVCorrect
HOL-MicroJava: theory Abstract_BV
HOL-MicroJava: theory Decl
HOL-MicroJava: theory Value
HOL-MicroJava: theory SystemClasses
HOL-MicroJava: theory TypeRel
HOL-MicroJava: theory Term
HOL-MicroJava: theory State
HOL-MicroJava: theory WellForm
HOL-MicroJava: theory Exceptions
HOL-MicroJava: theory JType
HOL-MicroJava: theory JVMType
HOL-MicroJava: theory WellType
HOL-MicroJava: theory Conform
HOL-MicroJava: theory Eval
HOL-MicroJava: theory TypeInf
HOL-MicroJava: theory JVMState
HOL-MicroJava: theory JVMInstructions
HOL-MicroJava: theory JVMExceptions
HOL-MicroJava: theory JVMExecInstr
HOL-MicroJava: theory Effect
HOL-MicroJava: theory JVMExec
HOL-MicroJava: theory DefsComp
HOL-MicroJava: theory JVMDefensive
HOL-MicroJava: theory JVMListExample
HOL-MicroJava: theory Index
HOL-MicroJava: theory TranslCompTp
HOL-MicroJava: theory TranslComp
HOL-MicroJava: theory JListExample
HOL-MicroJava: theory Example
HOL-MicroJava: theory JTypeSafe
HOL-MicroJava: theory LemmasComp
HOL-MicroJava: theory CorrComp
HOL-MicroJava: theory BVSpec
HOL-MicroJava: theory EffectMono
HOL-MicroJava: theory Altern
HOL-MicroJava: theory Correct
HOL-MicroJava: theory Typing_Framework_JVM
HOL-MicroJava: theory BVSpecTypeSafe
HOL-MicroJava: theory JVM
HOL-MicroJava: theory LBVJVM
HOL-MicroJava: theory CorrCompTp
HOL-MicroJava: theory BVNoTypeError
HOL-MicroJava: theory BVExample
HOL-MicroJava: theory MicroJava
Timing HOL-MicroJava (8 threads, 43.338s elapsed time, 240.940s cpu time, 13.963s GC time, factor 5.56)
Finished HOL-MicroJava (0:00:45 elapsed time, 0:04:02 cpu time, factor 5.37)
Running HOL-Probability ...
HOL-Probability: theory AList
HOL-Probability: theory DAList
HOL-Probability: theory Multiset
HOL-Probability: theory Permutation
HOL-Probability: theory Sigma_Algebra
HOL-Probability: theory Diagonal_Subsequence
HOL-Probability: theory Discrete_Topology
HOL-Probability: theory Measurable
HOL-Probability: theory Measure_Space
HOL-Probability: theory Borel_Space
HOL-Probability: theory Caratheodory
HOL-Probability: theory Lebesgue_Integration
HOL-Probability: theory Regularity
HOL-Probability: theory Binary_Product_Measure
HOL-Probability: theory Complete_Measure
HOL-Probability: theory Radon_Nikodym
HOL-Probability: theory Finite_Product_Measure
HOL-Probability: theory Fin_Map
HOL-Probability: theory Lebesgue_Measure
HOL-Probability: theory Probability_Measure
HOL-Probability: theory Distributions
HOL-Probability: theory Projective_Family
HOL-Probability: theory Infinite_Product_Measure
HOL-Probability: theory Independent_Family
HOL-Probability: theory Projective_Limit
HOL-Probability: theory Information
HOL-Probability: theory Dining_Cryptographers
HOL-Probability: theory Koepf_Duermuth_Countermeasure
HOL-Probability: theory Probability
Timing HOL-Probability (8 threads, 28.263s elapsed time, 179.201s cpu time, 8.437s GC time, factor 6.34)
Finished HOL-Probability (0:00:32 elapsed time, 0:03:02 cpu time, factor 5.68)
Running HOL-Proofs-Extraction ...
HOL-Proofs-Extraction: theory AList
HOL-Proofs-Extraction: theory Adhoc_Overloading
HOL-Proofs-Extraction: theory Code_Binary_Nat
HOL-Proofs-Extraction: theory Code_Natural
HOL-Proofs-Extraction: theory Fact
HOL-Proofs-Extraction: theory Parity
HOL-Proofs-Extraction: theory Monad_Syntax
HOL-Proofs-Extraction: theory Code_Integer
HOL-Proofs-Extraction: theory State_Monad
HOL-Proofs-Extraction: theory Efficient_Nat
HOL-Proofs-Extraction: theory DAList
HOL-Proofs-Extraction: theory Multiset
HOL-Proofs-Extraction: theory GCD
HOL-Proofs-Extraction: theory Primes
HOL-Proofs-Extraction: theory Cong
HOL-Proofs-Extraction: theory UniqueFactorization
HOL-Proofs-Extraction: theory Higman
HOL-Proofs-Extraction: theory Util
HOL-Proofs-Extraction: theory Warshall
HOL-Proofs-Extraction: theory Euclid
HOL-Proofs-Extraction: theory Pigeonhole
HOL-Proofs-Extraction: theory QuotRem
HOL-Proofs-Extraction: theory Higman_Extraction
HOL-Proofs-Extraction: theory Greatest_Common_Divisor
Timing HOL-Proofs-Extraction (8 threads, 106.862s elapsed time, 393.385s cpu time, 33.805s GC time, factor 3.68)
Finished HOL-Proofs-Extraction (0:01:50 elapsed time, 0:06:34 cpu time, factor 3.58)
Running HOL-SET_Protocol ...
HOL-SET_Protocol: theory Nat_Bijection
HOL-SET_Protocol: theory Message_SET
HOL-SET_Protocol: theory Event_SET
HOL-SET_Protocol: theory Public_SET
HOL-SET_Protocol: theory Cardholder_Registration
HOL-SET_Protocol: theory Merchant_Registration
HOL-SET_Protocol: theory Purchase
HOL-SET_Protocol: theory SET_Protocol
Timing HOL-SET_Protocol (8 threads, 13.504s elapsed time, 75.569s cpu time, 1.988s GC time, factor 5.60)
Finished HOL-SET_Protocol (0:00:16 elapsed time, 0:01:16 cpu time, factor 4.75)
Running HOL-UNITY ...
HOL-UNITY: theory Message
HOL-UNITY: theory Event
HOL-UNITY: theory Public
HOL-UNITY: theory AList
HOL-UNITY: theory ListOrder
HOL-UNITY: theory UNITY
HOL-UNITY: theory Constrains
HOL-UNITY: theory Deadlock
HOL-UNITY: theory FP
HOL-UNITY: theory Network
HOL-UNITY: theory WFair
HOL-UNITY: theory SubstAx
HOL-UNITY: theory Token
HOL-UNITY: theory DAList
HOL-UNITY: theory Detects
HOL-UNITY: theory Union
HOL-UNITY: theory Comp
HOL-UNITY: theory Guar
HOL-UNITY: theory Transformers
HOL-UNITY: theory Multiset
HOL-UNITY: theory Extend
HOL-UNITY: theory ProgressSets
HOL-UNITY: theory Project
HOL-UNITY: theory Rename
HOL-UNITY: theory Lift_prog
HOL-UNITY: theory ELT
HOL-UNITY: theory PPROD
HOL-UNITY: theory Follows
HOL-UNITY: theory UNITY_Main
HOL-UNITY: theory AllocBase
HOL-UNITY: theory Channel
HOL-UNITY: theory Common
HOL-UNITY: theory Counter
HOL-UNITY: theory Counterc
HOL-UNITY: theory Handshake
HOL-UNITY: theory Alloc
HOL-UNITY: theory AllocImpl
HOL-UNITY: theory Client
HOL-UNITY: theory Lift
HOL-UNITY: theory Mutex
HOL-UNITY: theory NSP_Bad
HOL-UNITY: theory PriorityAux
HOL-UNITY: theory Priority
HOL-UNITY: theory Progress
HOL-UNITY: theory Reach
HOL-UNITY: theory TimerArray
HOL-UNITY: theory Reachability
Timing HOL-UNITY (8 threads, 13.366s elapsed time, 77.301s cpu time, 4.125s GC time, factor 5.78)
Finished HOL-UNITY (0:00:15 elapsed time, 0:01:18 cpu time, factor 5.20)
Running ZF-UNITY ...
ZF-UNITY: theory FoldSet
ZF-UNITY: theory Acc
ZF-UNITY: theory GenPrefix
ZF-UNITY: theory State
ZF-UNITY: theory UNITY
ZF-UNITY: theory Multiset
ZF-UNITY: theory Constrains
ZF-UNITY: theory FP
ZF-UNITY: theory WFair
ZF-UNITY: theory SubstAx
ZF-UNITY: theory MultisetSum
ZF-UNITY: theory Monotonicity
ZF-UNITY: theory Mutex
ZF-UNITY: theory Increasing
ZF-UNITY: theory Union
ZF-UNITY: theory Follows
ZF-UNITY: theory Comp
ZF-UNITY: theory Guar
ZF-UNITY: theory AllocBase
ZF-UNITY: theory ClientImpl
ZF-UNITY: theory Distributor
ZF-UNITY: theory Merge
ZF-UNITY: theory AllocImpl
Timing ZF-UNITY (8 threads, 5.007s elapsed time, 34.089s cpu time, 1.412s GC time, factor 6.81)
Finished ZF-UNITY (0:00:06 elapsed time, 0:00:33 cpu time, factor 5.50)
Finished at Mon Feb 4 21:26:07 CET 2013
0:15:53 elapsed time, 1:16:38 cpu time, factor 4.82