Dear GHC developers, dear users,
I am starting to doubt in the GHC time profiling.
Why can advise, please, on the following example?
This is important for me: I need to find who eats time in this
particular example.
This is for ghc-6.6.
I `make' my large program (of many modules) via Cabal, with -O -prof
and -enable-profiling included.
The Main module contains the test example main.
`main' calls for LemmaSearch.searchLemmataInInitial.
`Main' is also built under -prof and run under +RTS -p -RTS.
I set the cost centers only inside LemmaSearch.hs.
And I set {-# SCC ... #-} in all valuable places in the module
LemmaSearch.hs, I skip only the places where a data field is
extracted/set, or such.
(I would like to set -auto-all for the module LemmaSearch.hs
only, but GHC does not accept the pragma {-# OPTIONS_GHC auto-all #-},
I wonder, why
).
The .prof file shows
----------------------------------------
...
COST CENTRE MODULE %time %alloc
searchLemmata LemmaSearch 91.9 93.2
splitDisjunctScheme LemmaSearch 3.9 3.0
addEquationsWithReduction LemmaSearch 3.7 3.3
individual inherited
COST CENTRE MODULE
...
----------------------------------------
searchLemmata is the main loop inside searchLemmataInInitial
where everything happens,
and splitDisjunctScheme, addEquationsWithReduction
are called from this loop.
It looks correct that searchLemmata costs 90%.
I could believe that splitDisjunctScheme and addEquationsWithReduction
take together about 8% of what searchLemma costs.
But who inside the searchLemmata loop takes the rest of (90 - 8)% ?
I do not see this, because all other parts (about 15 of centers) are
shown in profiling as close to zero %.
The centers for the imported functions are set before each their
envocation in this module.
The centers for the functions from this module are set before their
first defining statement, and they are all defined in the style of
``f = ...'', with single equality at top.
I append below the module LemmaSearch.hs (with comments skipped)
and the .prof file.
(Does this 770 line letter damage the ghc-users list?
I am sorry, if it does).
If the GHC team asks for the whole example source and provides me with
a private address for this, then I would send the source archive of the
project.
Thank you in advance for help,
-----------------
Serge Mechveliani
mechvel(a)botik.ru
--------------------------------------------------------------------
module LemmaSearch (searchLemmataInInitial)
where
import qualified Data.Set as Set ...
import qualified Data.Map as Map ...
import Char (isDigit)
import List (genericLength, nub, (\\), insertBy)
import Ratio (numerator, denominator)
import Dumatel.Prelude ...
...
import ...
root :: Natural -> Natural -> Natural
root n = {-# SCC "root" #-} fst . intRoot n
type ExtLemmataSearchState =
((LemmataSearchState, [Disjunct]), Resource)
searchLemmataInInitial :: ProverOptions -> -- proverOpts
Resource -> -- rc
Resource -> -- rcPerLemma
PreferableOrOrdinary -> -- pref
LemmataSearchState -> -- searchState
ExtLemmataSearchState
searchLemmataInInitial proverOpts rc rcPerLemma pref searchState =
(let ((state', newProveds), rcRem) =
searchLemmata ((searchState, []), rc)
cost = lsisCost searchState
in
((state' {lsisCost = cost + rc - rcRem}, newProveds), rcRem)
)
where
message0 =
showString "\nsearchLemmataInInitial " .
showString "(skolParam, superpty, jump, lsearchParams)\n " .
shows rc . showChar ' ' . shows rcPerLemma . showChar ' ' .
shows pref . showString " searchState,\n" .
showString "lsisVariables = " . shows (lsisVariables searchState) .
showChar '\n' .
showString "lsisOperators =\n " . shows (map name ordOps) .
showChar '\n'
(superpty, jump, umrBounds, lsearchParams) =
(provOptSupty proverOpts, provOptRdJump proverOpts,
provOptUMRMemoBounds proverOpts, provOptLSIParams proverOpts
)
(_, mBounds, rKeyBound) = umrBounds
mrBounds = (mBounds, rKeyBound)
rcForDisproof = quot rcPerLemma 2
rcForProof = 0
calculusEquationsSize = genericLength . equationList
testRangePerVariable = lsipTestRangePerVariable lsearchParams
depthBoundForGroundSubst = lsipDepthBoundForGroundSubst lsearchParams
ordOps = lsisOperators searchState
isFalseTerm t = case t of VarT _ -> False
App o _ -> name o == "false"
isTrivialFormula f = case f of VarT _ -> False
App o _ ->
name o == "true" || name o == "false"
addFormula :: Calculus -> Formula -> Calculus
addFormula calc f =
{-# SCC "addFormula" #-}
let memo = (Map.empty, Map.empty, Map.empty)
in
tuple41 $ addFormulae mrBounds memo jump calc
SkolemizeNot Ordinary superpty [f]
allSorts = Map.keys $ snd $ sortIdTabs $ lsisCalculus searchState
----------------------------------------------------------------------
searchLemmata extState@ ((searchState, newProveds), rc) =
{-# SCC "searchLemmata" #-}
let umMemo = lsisUnifMatchMemo searchState
(uMemo, mMemo) = umMemo
store = lsisStore searchState
disproveds = lsiDisproved store
passedCps = lsiPassedCompletion store
sMulty = lsiMultiplicity store
in
(case splitCs
of
[] -> extState
(((calc', lastName, newVars, preeqs), dj, _), djCost) : splitCs' ->
if rc < minRc then extState
else
case (findMatchEquivalentIn2tables mBounds (uMemo, mMemo)
(opTab calc') (fst passedCps) (fst disproveds) dj,
{-# SCC "opVarMulKind" #-}
opVarMulKind dj, -- djOVKind
{-# SCC "nonSchemeOpVarMultisets" #-}
nonSchemeOpVarMultisets isSchemeOperator dj -- djOVMS
)
of
((mMemo2, Just dj', searchCost1), _, _) ->
let state' = searchState
{lsisDSplits = splitCs',
lsisStore = sStore
{lsiMultiplicity = succ sMulty},
lsisUnifMatchMemo = (uMemo, mMemo2)
}
rc' = rc - djCost - searchCost1
in
searchLemmata ((state', newProveds), rc')
((mMemo2, _, searchCost1), djOVKind, djOVMS) ->
case findSchemeEquivalentTermIn2tables
mrBounds (uMemo, mMemo2) isSchemeOperator calc'
(snd passedCps) (snd disproveds) dj djOVMS
of
(Just dj', searchCost2) ->
let state' = searchState
{lsisDSplits = splitCs',
lsisStore = sStore
{lsiMultiplicity = succ sMulty},
lsisUnifMatchMemo = (uMemo, mMemo2)
}
rc' = rc - djCost - searchCost1 - searchCost2
in
searchLemmata ((state', newProveds), rc')
(_, searchCost2) ->
let (matchRes, matchCost) =
{-# SCC "matchAnySubdisjunctSchemeInList" #-}
matchAnySubdisjunctSchemeInList
mrBounds (uMemo, mMemo2) isSchemeOperator calc'
(filter hasScheme disprovedsL) dj
rc' = rc - djCost - searchCost1 - searchCost2 - matchCost
in
case matchRes
of
Just (dj', litSubset, _rCalc) ->
let
state' =
searchState
{lsisDSplits = splitCs',
lsisStore = sStore {lsiMultiplicity = succ sMulty},
lsisUnifMatchMemo = (uMemo, mMemo2)}
in
searchLemmata ((state', newProveds), rc')
_ ->
case {-# SCC "matchAnySubdisjunctInList" #-}
matchAnySubdisjunctInList mBounds (uMemo, mMemo2)
(opTab calc') disprovedsL dj
of
(mMemo3, Just (dj', subD, _), matchCost) ->
let
state' =
searchState
{lsisDSplits = splitCs',
lsisStore = sStore {lsiMultiplicity = succ sMulty},
lsisUnifMatchMemo = (uMemo, mMemo3)}
in
searchLemmata ((state', newProveds), rc' - matchCost)
(mMemo3, _, matchCost) ->
let
(disprovedByTilde, ukbbRes, rcRem) =
-- {-# "disproveStatement" #-}
disproveStatement calc' rcForDisproof dj
rcAfterDispr = rc' - matchCost - rcForDisproof + rcRem
disprovedByCompl = ukbbGoalRem ukbbRes == ([], [])
(complEqs, _, complBTs) = ukbbCompl ukbbRes
calc'1 = calc'
(calc'', addCost) =
let umrMemo = (uMemo, mMemo3, Map.empty)
(_, cc, c1) =
{-# SCC "addEquationsWithReduction" #-}
addEquationsWithReduction
mrBounds umrMemo jump calc'1 complEqs
in
mapTuple22 (+ c1) $
{-# SCC "addBTLawsWithReduction" #-}
addBTLawsWithReduction mrBounds umrMemo
jump cc complBTs
calc''scTopOrNonSc =
setEquations calc''
[e | e <- equationList calc'',
not $ hasScheme e || isSchemeTopEq e
] []
(_, dj', djRdCost) = {-# SCC "reduceDisjunct" #-}
reduceDisjunct mrBounds
(uMemo, mMemo, Map.empty) jump
calc''scTopOrNonSc dj
rcAfterRd = rcAfterDispr - djRdCost - addCost
djSchemeOps = Set.toList $ schemeOperators dj
in
if disprovedByTilde
then
let disps' = insertToMapListPair djOVKind djOVMS dj
disproveds
state' =
searchState
{lsisDSplits = splitCs',
lsisStore = sStore {lsiDisproved = disps'},
lsisUnifMatchMemo = (uMemo, mMemo3)}
in
searchLemmata ((state', newProveds), rcAfterDispr)
else
if disprovedByCompl
then
let disps' = insertToMapListPair djOVKind djOVMS dj
disproveds
state' =
searchState
{lsisDSplits = splitCs',
lsisUnifMatchMemo = (uMemo, mMemo3),
lsisStore =
sStore {lsiDisproved = disps',
lsiPassedTilde =
Set.insert dj passedTildes}}
in
searchLemmata ((state', newProveds), rcAfterDispr)
else
if (not $ null djSchemeOps) && dj /= dj'
then
let
dj'sp = {-# SCC "dj'sp" #-}
(((calc'', lastName, newVars, preeqs), dj',
termSplitMeasure isSchemeOperator dj'), 0)
splitCs'' = {-# SCC "splitCs''" #-}
if isTrivialFormula dj' then splitCs'
else
insertBy (\ (s, _) (s', _) ->
compareTermSplitsByMeasure s s'
)
dj'sp splitCs'
passedCps' = insertToMapListPair djOVKind djOVMS dj
passedCps
state' =
searchState
{lsisDSplits = splitCs'',
lsisUnifMatchMemo = (uMemo, mMemo3),
lsisStore =
sStore
{lsiPassedCompletion = passedCps',
lsiPassedTilde = Set.insert dj passedTildes,
lsiHasReduced = Set.insert dj reduceds} }
in
searchLemmata ((state', newProveds), rcAfterRd)
else
if not $ null djSchemeOps
then
let
(splitCs0, _splitStatistic) =
{-# SCC "splitDisjunctScheme" #-}
splitDisjunctScheme mrBounds umMemo ordOps
calc'' jump lastName dj djSchemeOps
splitCs'' =
{-# SCC "splitCs''" #-}
map (\ ((osp, dis, meas), c) ->
((mapTuple44 (++ preeqs) osp, dis, meas), c)
) $
filter (\ ((_, d, _), _) -> d /= dj) splitCs0
passedCps' = insertToMapListPair djOVKind djOVMS dj
passedCps
state' =
searchState
{lsisUnifMatchMemo = (uMemo, mMemo3),
lsisDSplits =
{-# SCC "lsisDSplits = ..mergeBy.." #-}
mergeBy (\ (s, _) (s', _) ->
compareTermSplitsByMeasure s s'
)
splitCs' splitCs'',
lsisStore =
sStore
{lsiPassedCompletion = passedCps',
lsiPassedTilde = Set.insert dj passedTildes}}
in
searchLemmata ((state', newProveds), rcAfterRd)
else
let
lemParamsForProof = lsearchParams {lsipFactor = 0,
lsipExponent = 0}
opts' = proverOpts
{provOptLSIParams = lemParamsForProof}
(proved, _, rcRem) =
proveStatementInInitial opts' rcForProof dj
rc' = rcAfterDispr - rcForProof + rcRem
in
if not proved
then
let passedCps' = insertToMapListPair djOVKind djOVMS dj
passedCps
state' =
searchState
{lsisDSplits = splitCs',
lsisUnifMatchMemo = (uMemo, mMemo3),
lsisStore =
sStore
{lsiPassedCompletion = passedCps',
lsiPassedTilde = Set.insert dj passedTildes}
}
in
searchLemmata ((state', newProveds), rc')
else
let
passedCps' = insertToMapListPair djOVKind djOVMS dj
passedCps
state' =
searchState
{lsisDSplits = map addStatement splitCs',
lsisUnifMatchMemo = (uMemo, mMemo3),
lsisStore =
sStore
{lsiPassedTilde = Set.insert dj passedTildes,
lsiPassedCompletion = passedCps',
lsiProved = Set.insert dj proveds} }
addStatement ((osp, d, m), c) =
{-# SCC "addStatement" #-}
((mapTuple41 (\ calc -> addF calc dj) osp, d, m), c)
addF calc = addFormula calc . closeFormula calc
in
searchLemmata ((state', dj : newProveds), rc')
)
where
calc0 = lsisCalculus searchState
sStore = lsisStore searchState
splitCs = lsisDSplits searchState
calc0ops = operators calc0
minRc = calculusEquationsSize calc0
isSchemeOperator f =
{-# SCC "isSchemeOperator" #-}
(not $ Set.member f calc0ops) && (isScName $ name f)
isScName nm = case nm of 's': 'c': nm' -> all isDigit nm'
_ -> False
schemeOperators :: WithOperatorSet a => a -> Set.Set Operator
schemeOperators = {-# SCC "schemeOperators" #-}
Set.filter isSchemeOperator . operators
hasScheme :: WithOperatorSet a => a -> Bool
hasScheme = {-# SCC "hasScheme" #-}
not . Set.null . schemeOperators
isSchemeTopEq e =
{-# SCC "isSchemeTopEq" #-}
any isSTop [l, r]
where
(l, r) = sides e
isSTop t = (not $ isVariable t) &&
(not $ Set.member (topOperator t) calc0ops)
disproveds = lsiDisproved sStore
passedTildes = lsiPassedTilde sStore
passedCps = lsiPassedCompletion sStore
reduceds = lsiHasReduced sStore
proveds = lsiProved sStore
disprovedsL =
{-# SCC "disprovedsL" #-}
concat $ Map.elems $ fst disproveds
opsForSubst = {-# SCC "opsForSubst" #-}
(extraRelatedConstants calc0 ordOps) ++ ordOps
where
extraRelatedConstants calc ops =
(concat $ map contantsOfSort relatedSorts) \\ ops
where
calcConsts = filter isConstantOperator $ Set.toList $
operators calc
relatedSorts = Set.toList $ sUnion $ map sortageUnion ops
contantsOfSort s = filter ((s ==) . coarity) calcConsts
sortageUnion f = let ((lsorts, rsorts), cosort) = sortage f
in
Set.insert cosort $
sUnion [Set.fromList lsorts, Set.fromList rsorts]
--------------------------------------------------------------------
disproveStatement ::
Calculus -> Resource -> Disjunct -> (Bool, UKBBResult, Resource)
disproveStatement calcExt rc dj =
{-# SCC "disproveStatement" #-}
(if disprovedByTilde then
(True, dummy "dummy complRes in disproveStatement",
rcAfterTilde)
else (False, ukbbRes, rcAfterCompl)
)
where
testingSubsts = groundSubstsForTest $ Set.toList $ vars dj
(tildePairsPassed, tildePairsRest) =
let memo = (Map.empty, Map.empty, Map.empty)
in
span (not . isFalseTerm . fst)
[(dj', c) |
sb <- testingSubsts,
let (_, dj', c) = reduceDisjunct mrBounds memo jump calcExt
$ substitute sb dj]
disprovedByTilde = not $ null tildePairsRest
tildeCost = succ $ sum $ map snd tildePairsPassed
rcAfterTilde = rc - tildeCost
rcCompl = 0
refutRes =
let uMtMemo = (Map.empty, Map.empty)
in
refuteFormulaSetByCompletion
TraceNot umrBounds uMtMemo jump (Fin rcCompl) (Fin rcCompl)
0 SkolemizeNot Preferable superpty calcExt
[closeFormula calcExt dj]
ukbbRes = cpRefInitialCompletion refutRes
Fin complRcRem = cpRefRcRem refutRes
rcAfterCompl = rcAfterTilde - rcCompl + complRcRem
groundSubstsForTest xs =
(if null opsForSubst || null xs then [identitySubstitution]
else gsubsForTest xs testRangePerVariable
)
where
varSorts = nub $ map sort xs
varDomains =
Map.fromList [(s, varDomain calc0 s) | s <- varSorts]
gsubsForTest xs range = case xs of
[] -> []
[x] -> map (Map.singleton x) $
takeTermsFromTermsOfSort
range depthBoundForGroundSubst
(varDomain calc0 $ sort x)
x: ys ->
case Map.lookup (sort x) varDomains
of
Nothing ->
error $ concat
["\ndisproveStatement calcExt ", shows rc "\n ",
shows dj "\n...",
"gsubsForTest ", shows xs " ", shows range
"\n...Impossible happened:\n",
"Map.lookup (sort x) varDomains failed for x = ",
shows x ".\n"
]
Just vd ->
case takeTermsFromTermsOfSort
range depthBoundForGroundSubst vd
of
[] -> []
vals -> [Map.insert x v sb | sb <- sbs', v <- vals]
where
cardVals = genericLength vals
sbs' = gsubsForTest ys (2*range - cardVals)
varDomain :: Calculus -> Sort -> TermsOfSort
varDomain calc s =
(case Map.lookup s nts of Just v -> v
_ -> Map.empty
)
where
nts =
let umMemo = (Map.empty, Map.empty)
in
termSetUpToLevel (not . reducesAtTop mBounds umMemo calc)
allSorts [] opsForGround depthBoundForGroundSubst
opsForGround = sgens ++ (opsForSubst \\ sgens)
-- move generators of s ahead
sgens = concat $ sortGeneratorLists (sortGenTab calc) s
--------------------------------------------------------------------
proveStatementInInitial ::
ProverOptions-> Resource-> Disjunct-> (Bool, Inference, Resource)
proveStatementInInitial proverOpts rc dj =
{-# SCC "proveStatementInInitial" #-}
(isProved $ psStateTree inferState, reduceInference inference,
rc - inferenceCost)
where
goal = Prove {goalCalculus = calc0,
goalFormula = closeFormula calc0 dj,
goalMode = InInitial
}
state0 = proofSearchStateFromGoal umrBounds superpty jump rc goal
p = lsipExponent lsearchParams
(n, m) = (numerator p, denominator p)
rcPerStepInLemma = if p == 0 then 1
else
if p == 1 then rc else (root m rc)^n
inferenceBound = rc
inference = takeUpToBound inferenceBound $
prove proverOpts rcPerStepInLemma state0
inferState = last inference
inferenceCost = rcPerStepInLemma * (genericLength inference)
takeUpToBound :: Natural -> Inference -> Inference
takeUpToBound bound inference = tk 0 inference
where
tk _ [] = []
tk volume (state: states) =
if
volume > bound then []
else
state : (tk (volume + (inferenceVolume [state])) states)
------------------------------------------------------------------------
insertToMapListPair :: -- local
(Ord key1, Ord key2) =>
key1 -> key2 -> v -> (Map.Map key1 [v], Map.Map key2 [v]) ->
(Map.Map key1 [v], Map.Map key2 [v])
insertToMapListPair key1 key2 v (map1, map2) =
{-# SCC "insertToMapListPair" #-}
(Map.insertWith (++) key1 [v] map1, Map.insertWith (++) key2 [v] map2)
findMatchEquivalentIn2tables mBounds (uMemo, mMemo) otab tab1 tab2 dj =
-- local
{-# SCC "findMatchEquivalentIn2tables" #-}
(case find1 0 mMemo tab1
of
(mMemo', Nothing, cost) -> find1 cost mMemo' tab2
triple -> triple
)
where
ovKind = opVarMulKind dj
find1 cost mMemo tab = case Map.lookup ovKind tab of
Nothing -> (mMemo, Nothing, cost)
Just listOfKey -> mapTuple33 (+ cost) $
findMatchEquivalent mBounds (uMemo, mMemo)
otab listOfKey dj
findSchemeEquivalentTermIn2tables -- local
mrBounds umMemo isSchemeOperator calc tab1 tab2 t key =
{-# SCC "findSchemeEquivalentTermIn2tables" #-}
(case find1 0 tab1 of (Nothing, cost) -> find1 cost tab2
pair -> pair
)
where
find1 cost tab = case Map.lookup key tab
of
Nothing -> (Nothing, cost)
Just ts -> mapTuple22 (+ cost) $
findSchemeEquivalentTerm mrBounds umMemo
isSchemeOperator calc ts t
--------------------------------------------------------------------------
Sat Dec 2 17:18 2006 Time and Allocation Profiling Report (Final)
LemSearchList +RTS -M200m -p -RTS
total time = 268.25 secs (5365 ticks @ 50 ms)
total alloc = 9,796,199,364 bytes (excludes profiling overheads)
COST CENTRE MODULE %time %alloc
searchLemmata LemmaSearch 91.9 93.2
splitDisjunctScheme LemmaSearch 3.9 3.0
addEquationsWithReduction LemmaSearch 3.7 3.3
individual inherited
COST CENTRE MODULE no. entries %time %alloc %time %alloc
MAIN MAIN 1 0 0.0 0.0 100.0 100.0
CAF Main 280 66 0.0 0.0 100.0 100.0
disprovedsL LemmaSearch 295 1 0.0 0.0 0.0 0.0
opsForSubst LemmaSearch 290 1 0.0 0.0 0.0 0.0
hasScheme LemmaSearch 289 0 0.0 0.0 0.0 0.0
isSchemeOperator LemmaSearch 288 0 0.0 0.0 0.0 0.0
addFormula LemmaSearch 287 0 0.0 0.0 0.0 0.0
searchLemmata LemmaSearch 286 3143 91.9 93.2 100.0 99.9
root LemmaSearch 315 8 0.0 0.0 0.0 0.0
disprovedsL LemmaSearch 314 303 0.0 0.0 0.0 0.0
opVarMulKind LemmaSearch 312 128 0.0 0.0 0.0 0.0
opsForSubst LemmaSearch 311 128 0.1 0.0 0.1 0.0
isSchemeOperator LemmaSearch 310 23738 0.0 0.0 0.0 0.0
lsisDSplits = ..mergeBy.. LemmaSearch 309 89 0.0 0.0 0.0 0.0
splitCs'' LemmaSearch 308 841 0.0 0.0 0.0 0.0
splitDisjunctScheme LemmaSearch 307 89 3.9 3.0 3.9 3.0
isSchemeTopEq LemmaSearch 306 2670 0.0 0.0 0.0 0.0
hasScheme LemmaSearch 303 7275 0.0 0.0 0.0 0.0
schemeOperators LemmaSearch 304 7275 0.0 0.0 0.0 0.0
isSchemeOperator LemmaSearch 305 82 0.0 0.0 0.0 0.0
addBTLawsWithReduction LemmaSearch 302 89 0.0 0.0 0.0 0.0
addEquationsWithReduction LemmaSearch 301 89 3.7 3.3 3.7 3.3
schemeOperators LemmaSearch 299 97 0.0 0.0 0.0 0.0
isSchemeOperator LemmaSearch 300 3 0.0 0.0 0.0 0.0
reduceDisjunct LemmaSearch 298 267 0.1 0.1 0.1 0.1
disproveStatement LemmaSearch 297 129 0.0 0.0 0.0 0.0
matchAnySubdisjunctInList LemmaSearch 296 190 0.2 0.2 0.2 0.2
matchAnySubdisjunctSchemeInList LemmaSearch 294 304 0.0 0.0 0.0 0.0
findSchemeEquivalentTermIn2tables LemmaSearch 293 343 0.0 0.0 0.0 0.0
nonSchemeOpVarMultisets LemmaSearch 292 343 0.0 0.0 0.0 0.0
isSchemeOperator LemmaSearch 313 3 0.0 0.0 0.0 0.0
findMatchEquivalentIn2tables LemmaSearch 291 664 0.0 0.1 0.0 0.1
CAF Text.Read.Lex 257 14 0.0 0.0 0.0 0.0
CAF GHC.Real 254 1 0.0 0.0 0.0 0.0
CAF GHC.Read 251 2 0.0 0.0 0.0 0.0
CAF GHC.Handle 233 3 0.0 0.0 0.0 0.0
CAF BTerm0 192 1 0.0 0.0 0.0 0.0
CAF Unify 191 5 0.0 0.0 0.0 0.0
CAF Parse1 190 4 0.0 0.0 0.0 0.0
CAF Prelude4 189 5 0.0 0.0 0.0 0.0
CAF Prelude3_1 188 7 0.0 0.0 0.0 0.0
CAF Prelude3_0 187 2 0.0 0.0 0.0 0.0
CAF Prelude3 186 8 0.0 0.0 0.0 0.0
CAF Prelude2_0 185 6 0.0 0.0 0.0 0.0
CAF Prelude2 184 1 0.0 0.0 0.0 0.0
CAF Prelude1 183 2 0.0 0.0 0.0 0.0
CAF Prelude00 168 1 0.0 0.0 0.0 0.0
CAF Dumatel.Reduce 166 1 0.0 0.0 0.0 0.0
CAF Split 165 7 0.0 0.0 0.0 0.0
CAF Bool0 163 55 0.0 0.0 0.0 0.0
CAF Parse2 162 5 0.0 0.0 0.0 0.0
CAF LemmaSearch 156 1 0.0 0.0 0.0 0.0
CAF Prover1 154 1 0.0 0.0 0.0 0.0
CAF Prover00 153 6 0.0 0.0 0.0 0.0
CAF Dumatel.Prelude5 152 1 0.0 0.0 0.0 0.0
CAF Dumatel.BTerm 151 2 0.0 0.0 0.0 0.0
CAF UKBB0 147 1 0.0 0.0 0.0 0.0
