Class de.uka.ilkd.key.proof.proverules.ProveRulesTest

all > de.uka.ilkd.key.proof.proverules > ProveRulesTest
198

tests
0

failures
0

ignored
11m0.02s

duration
100%

successful

Tests

Test Method name Duration Result
powPositive data()[100] 3.180s passed
powPositiveConcrete data()[101] 3.195s passed
powGeq1Concrete data()[102] 3.192s passed
pow2InIntLower data()[103] 3.196s passed
pow2InIntUpper data()[104] 3.196s passed
logSelfConcrete data()[105] 3.191s passed
log1Concrete data()[106] 3.203s passed
logProduct data()[107] 3.201s passed
logTimesBaseConcrete data()[108] 3.183s passed
logProdIdentity data()[109] 3.199s passed
moduloByteIsInByte data()[10] 3.253s passed
logProdIdentityConcrete data()[110] 3.198s passed
logPowIdentity data()[111] 3.197s passed
logPowIdentityConcrete data()[112] 3.179s passed
logPositive data()[113] 3.183s passed
logPositiveConcrete data()[114] 3.193s passed
logMono data()[115] 3.207s passed
logMonoConcrete data()[116] 3.179s passed
powLogLess data()[117] 3.192s passed
powLogMore2 data()[118] 3.198s passed
logLessThanPow data()[119] 3.225s passed
moduloCharIsInChar data()[11] 3.246s passed
logLessThanPowConcrete data()[120] 3.216s passed
logSqueeze data()[121] 3.207s passed
ifthenelse_equals data()[122] 3.187s passed
ifthenelse_equals_1 data()[123] 3.180s passed
ifthenelse_equals_2 data()[124] 3.184s passed
disjointWithSingleton1 data()[125] 3.185s passed
disjointWithSingleton2 data()[126] 3.182s passed
disjointArrayRanges data()[127] 3.206s passed
disjointArrayRangeAllFields1 data()[128] 3.197s passed
disjointArrayRangeAllFields2 data()[129] 3.196s passed
div_unique1 data()[12] 3.328s passed
seqSelfDefinition data()[130] 3.206s passed
seqOutsideValue data()[131] 3.196s passed
castedGetAny data()[132] 3.192s passed
seqGetAlphaCast data()[133] 3.185s passed
getOfSeqSingleton data()[134] 3.190s passed
getOfSeqSingletonConcrete data()[135] 3.181s passed
getOfSeqConcat data()[136] 3.204s passed
getOfSeqSub data()[137] 3.207s passed
getOfSeqReverse data()[138] 3.194s passed
lenOfSeqEmpty data()[139] 3.188s passed
div_unique2 data()[13] 3.331s passed
lenOfSeqSingleton data()[140] 3.173s passed
lenOfSeqConcat data()[141] 3.174s passed
lenOfSeqSub data()[142] 3.168s passed
lenOfSeqReverse data()[143] 3.224s passed
equalityToSeqGetAndSeqLenLeft data()[144] 3.194s passed
equalityToSeqGetAndSeqLenRight data()[145] 3.185s passed
getOfSeqSingletonEQ data()[146] 3.188s passed
getOfSeqConcatEQ data()[147] 3.181s passed
getOfSeqSubEQ data()[148] 3.214s passed
getOfSeqReverseEQ data()[149] 3.189s passed
div_exists data()[14] 3.427s passed
lenOfSeqEmptyEQ data()[150] 3.195s passed
lenOfSeqSingletonEQ data()[151] 3.165s passed
lenOfSeqConcatEQ data()[152] 3.231s passed
lenOfSeqSubEQ data()[153] 3.196s passed
lenOfSeqReverseEQ data()[154] 3.179s passed
getOfSeqDefEQ data()[155] 3.178s passed
lenOfSeqDefEQ data()[156] 3.221s passed
seqConcatWithSeqEmpty1 data()[157] 3.194s passed
seqConcatWithSeqEmpty2 data()[158] 3.209s passed
seqReverseOfSeqEmpty data()[159] 3.214s passed
div_one data()[15] 3.253s passed
subSeqComplete data()[160] 3.188s passed
subSeqTailR data()[161] 3.188s passed
subSeqTailL data()[162] 3.210s passed
subSeqTailEQR data()[163] 3.183s passed
subSeqTailEQL data()[164] 3.178s passed
seqDef_split data()[165] 3.216s passed
seqDef_induction_upper data()[166] 3.208s passed
seqDef_induction_upper_concrete data()[167] 3.226s passed
seqDef_induction_lower data()[168] 3.219s passed
seqDef_induction_lower_concrete data()[169] 3.207s passed
jdiv_one data()[16] 3.272s passed
seqDef_split_in_three data()[170] 3.256s passed
seqDef_empty data()[171] 3.195s passed
seqDef_one_summand data()[172] 3.236s passed
seqDef_lower_equals_upper data()[173] 3.185s passed
seqDefOfSeq data()[174] 3.217s passed
seqSelfDefinitionEQ2 data()[175] 3.191s passed
indexOfSeqSingleton data()[176] 3.199s passed
indexOfSeqConcatFirst data()[177] 3.191s passed
indexOfSeqConcatSecond data()[178] 3.206s passed
indexOfSeqSub data()[179] 3.201s passed
div_zero data()[17] 3.316s passed
lenOfArray2seq data()[180] 3.215s passed
getAnyOfArray2seq data()[181] 3.202s passed
getOfArray2seq data()[182] 3.221s passed
getAnyOfNPermInv data()[183] 3.180s passed
seqNPermRange data()[184] 3.240s passed
seqPermTrans data()[185] 3.249s passed
seqPermRefl data()[186] 3.198s passed
seqPermSplit data()[187] 3.208s passed
seqNPermRight data()[188] 3.288s passed
seqPermFromSwap data()[189] 3.219s passed
divResZero1 data()[18] 3.281s passed
seqPermTransAlt0 data()[190] 3.212s passed
seqPermTransAlt1 data()[191] 3.185s passed
seqPermTransAlt2 data()[192] 3.223s passed
seqPermTransAlt3 data()[193] 3.220s passed
seqPermForall data()[194] 3.314s passed
seqPermExists data()[195] 3.289s passed
schiffl_lemma_2 data()[196] 22.700s passed
schiffl_thm_1 data()[197] 4.050s passed
eqSameSeq data()[198] 3.268s passed
divResZero2 data()[19] 3.235s passed
eqTermCut data()[1] 3.909s passed
divResOne1 data()[20] 3.253s passed
divResOne2 data()[21] 3.358s passed
div_cancel1 data()[22] 3.286s passed
div_cancel2 data()[23] 3.270s passed
divAddMultDenom data()[24] 3.274s passed
divMinus data()[25] 3.268s passed
divMinusDenom data()[26] 3.279s passed
divLeastDPos data()[27] 3.267s passed
divLeastDNeg data()[28] 3.243s passed
divGreatestDPos data()[29] 3.242s passed
equivAllRight data()[2] 3.605s passed
divGreatestDNeg data()[30] 3.232s passed
divIncreasingPos data()[31] 3.233s passed
divIncreasingNeg data()[32] 3.284s passed
jdiv_zero data()[33] 3.247s passed
jdivPulloutMinusNum data()[34] 3.238s passed
jdivPulloutMinusDenom data()[35] 3.279s passed
jdiv_uniquePosPos data()[36] 3.246s passed
jdiv_uniquePosNeg data()[37] 3.269s passed
jdiv_uniqueNegPos data()[38] 3.233s passed
jdiv_uniqueNegNeg data()[39] 3.224s passed
irrflConcrete1 data()[3] 3.571s passed
jdivMultDenom1 data()[40] 3.246s passed
jdivMultDenom2 data()[41] 3.216s passed
mod_geZero data()[42] 3.206s passed
mod_lessDenom data()[43] 3.201s passed
jmod_NumPos data()[44] 3.224s passed
jmod_NumNeg data()[45] 3.213s passed
jmod_geZero data()[46] 3.201s passed
jmodNumZero data()[47] 3.198s passed
jmod_pulloutminusNum data()[48] 3.238s passed
jmod_pulloutminusDenom data()[49] 3.253s passed
irrflConcrete2 data()[4] 3.487s passed
jmodUnique1 data()[50] 3.263s passed
jmodUnique2 data()[51] 3.286s passed
intDivRem data()[52] 3.196s passed
jmodjmod data()[53] 3.241s passed
jmodDivisible data()[54] 3.231s passed
jmodDivisibleRep data()[55] 3.212s passed
jdivAddMultDenom data()[56] 3.337s passed
jmodAltZero data()[57] 3.263s passed
jmodAddMultDenomZero data()[58] 3.222s passed
polyDiv_zero data()[59] 3.230s passed
cancel_gtPos data()[5] 3.371s passed
polyMod_ltdivDenom data()[60] 3.205s passed
bsum_empty data()[61] 3.190s passed
bsum_induction_upper data()[62] 3.194s passed
bsum_induction_lower data()[63] 3.217s passed
bsum_num_of_bounds data()[64] 3.238s passed
bsum_num_of_bounds2 data()[65] 3.226s passed
bsum_induction_upper2 data()[66] 3.207s passed
bsum_induction_upper_concrete data()[67] 3.210s passed
bsum_induction_upper_concrete_2 data()[68] 3.182s passed
bsum_induction_upper2_concrete data()[69] 3.206s passed
cancel_gtNeg data()[6] 3.337s passed
bsum_induction_lower_concrete data()[70] 3.209s passed
bsum_induction_lower2 data()[71] 3.223s passed
bsum_induction_lower2_concrete data()[72] 3.189s passed
bsum_positive data()[73] 3.225s passed
bsum_upper_bound data()[74] 3.232s passed
bsum_lower_bound data()[75] 3.285s passed
bsum_positive_lower_bound_element data()[76] 3.256s passed
bsum_sub_same_index data()[77] 3.193s passed
bsum_less_same_index data()[78] 3.220s passed
bsum_equal_except_one_index data()[79] 3.209s passed
moduloIntIsInInt data()[7] 3.329s passed
bsum_num_of_is_max data()[80] 3.192s passed
bsum_num_of_is_max2 data()[81] 3.204s passed
bsum_num_of_is_max3 data()[82] 3.205s passed
bsum_num_of_is_max4 data()[83] 3.193s passed
bsum_num_of_lt_max data()[84] 3.215s passed
bsum_num_of_lt_max2 data()[85] 3.302s passed
bsum_num_of_lt_max3 data()[86] 3.214s passed
bsum_num_of_lt_max4 data()[87] 3.205s passed
bsum_num_of_gt0 data()[88] 3.216s passed
bsum_num_of_gt0_alt data()[89] 3.197s passed
moduloLongIsInLong data()[8] 3.315s passed
bsum_add_concrete data()[90] 3.196s passed
bprod_all_positive data()[91] 3.209s passed
bprod_split data()[92] 3.201s passed
powConcrete0 data()[93] 3.201s passed
powConcrete1 data()[94] 3.193s passed
powSplitFactor data()[95] 3.202s passed
powAdd data()[96] 3.190s passed
powMono data()[97] 3.264s passed
powMonoConcrete data()[98] 3.193s passed
powMonoConcreteRight data()[99] 3.194s passed
moduloShortIsInShort data()[9] 3.327s passed

Standard output

425        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
449        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 8.13ms 
687        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
710        WARN  Test worker     d.u.i.k.s.ProofSettings   No proof-settings could be loaded, using defaults java.io.FileNotFoundException: /home/runner/.key/proof-settings.props (No such file or directory)
	at java.base/java.io.FileInputStream.open0(Native Method)

1643       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1644       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1646       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1646       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
3284       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
8545       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 7.86s 
8631       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
8669       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.2ns 
8686       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
8687       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 659.71ns 
8694       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
11568      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
11571      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
12560      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
12584      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.68ms 
12597      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
12599      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.53ms 
12600      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
15281      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
15282      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
16178      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
16199      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.97ms 
16203      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
16203      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 161ns 
16204      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
18897      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
18898      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
19759      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
19769      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.88ms 
19776      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
19776      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 357.4ns 
19778      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
22392      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
22393      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
23249      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
23259      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.04ms 
23263      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
23269      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 5.46ms 
23271      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
25803      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
25804      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
26597      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
26633      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.3ms 
26635      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
26635      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 134.5ns 
26636      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
29154      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
29154      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
29953      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
29970      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.58ms 
29972      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
29972      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 121.4ns 
29973      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
32505      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
32505      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
33296      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
33299      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 813.21ns 
33301      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
33301      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 129.5ns 
33302      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
35806      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
35806      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
36608      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
36613      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.68ms 
36618      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
36618      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 373.8ns 
36620      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
39156      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
39156      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
39940      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
39942      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 564.4ns 
39944      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
39944      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.4ns 
39944      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
42413      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
42413      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
43192      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
43195      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 609.4ns 
43197      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
43197      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.6ns 
43198      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
45659      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
45660      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
46438      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
46441      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 636.11ns 
46444      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
46444      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 363.4ns 
46446      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
48956      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
48957      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
49733      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
49769      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.48ms 
49770      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
49770      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 123.2ns 
49771      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
52247      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
52247      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
53034      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
53094      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 55.71ms 
53103      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
53104      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 627.5ns 
53106      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
55630      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
55631      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
56410      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
56528      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 109.04ms 
56531      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
56531      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 419.3ns 
56533      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
58999      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
59000      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
59775      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
59780      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.42ms 
59783      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
59783      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 329ns 
59785      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
62241      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
62242      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
63050      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
63053      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.15ms 
63056      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
63057      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 324.9ns 
63058      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
65497      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
65498      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
66302      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
66369      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 63.18ms 
66373      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
66374      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 432.9ns 
66375      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
68840      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
68840      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
69640      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
69652      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.34ms 
69654      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
69654      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.8ns 
69655      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
72078      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
72079      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
72871      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
72887      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.44ms 
72890      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
72890      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 322.5ns 
72891      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
75328      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
75329      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
76127      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
76139      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.27ms 
76142      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
76142      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 365.4ns 
76144      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
78655      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
78655      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
79486      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
79498      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.99ms 
79500      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
79500      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 125.7ns 
79501      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
81967      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
81968      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
82767      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
82784      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.22ms 
82786      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
82786      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 127.5ns 
82787      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
85234      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
85235      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
86047      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
86055      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.75ms 
86056      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
86056      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 124.3ns 
86058      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
88503      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
88504      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
89299      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
89328      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.8ms 
89330      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
89330      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 130.6ns 
89331      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
91756      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
91756      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
92554      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
92596      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.2ms 
92598      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
92598      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.5ns 
92599      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
95027      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
95027      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
95845      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
95875      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.24ms 
95877      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
95877      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 125.7ns 
95878      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
98330      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
98330      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
99136      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
99142      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.57ms 
99144      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
99144      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 110.6ns 
99145      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
101579     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
101579     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
102374     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
102386     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.56ms 
102387     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
102387     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.9ns 
102388     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
104821     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
104821     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
105617     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
105627     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.95ms 
105629     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
105630     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 309.3ns 
105631     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
108062     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
108062     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
108853     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
108860     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.21ms 
108861     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
108861     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.1ns 
108862     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
111287     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
111287     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
112086     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
112093     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.13ms 
112094     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
112094     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.9ns 
112095     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
114577     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
114577     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
115370     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
115376     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.75ms 
115378     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
115378     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.7ns 
115379     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
117830     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
117830     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
118620     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
118623     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.24ms 
118625     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
118625     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.4ns 
118626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
121054     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
121054     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
121844     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
121861     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.51ms 
121863     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
121863     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 117.2ns 
121866     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
124301     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
124302     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
125097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
125139     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.86ms 
125142     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
125143     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 116.4ns 
125143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
127570     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
127570     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
128364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
128385     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.01ms 
128391     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
128391     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 362.4ns 
128393     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
130834     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
130834     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
131635     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
131658     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.05ms 
131660     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
131660     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 127.2ns 
131661     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
134081     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
134081     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
134877     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
134891     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.04ms 
134893     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
134893     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.9ns 
134894     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
137308     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
137308     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
138102     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
138115     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.12ms 
138116     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
138116     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103ns 
138117     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
140538     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
140539     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
141332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
141361     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.78ms 
141362     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
141362     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.9ns 
141363     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
143784     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
143784     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
144575     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
144577     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 888.41ns 
144579     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
144579     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 115.5ns 
144579     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
146992     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
146992     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
147780     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
147784     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.84ms 
147785     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
147785     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.6ns 
147786     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
150190     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
150190     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
150977     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
150984     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.61ms 
150986     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
150986     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.6ns 
150987     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
153403     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
153403     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
154194     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
154208     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.02ms 
154210     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
154211     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100ns 
154211     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
156613     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
156614     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
157404     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
157422     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.04ms 
157425     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
157425     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 327.2ns 
157426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
159824     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
159824     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
160615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
160623     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.16ms 
160624     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
160624     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.4ns 
160625     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
163026     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
163026     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
163818     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
163821     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.3ms 
163823     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
163824     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 288.5ns 
163825     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
166262     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
166262     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
167052     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
167056     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.37ms 
167062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
167062     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107ns 
167063     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
169513     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
169514     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
170309     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
170313     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.73ms 
170316     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
170317     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 305ns 
170318     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
172738     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
172738     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
173525     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
173578     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.89ms 
173580     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
173580     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.8ns 
173581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
175998     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
175999     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
176793     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
176864     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 62.54ms 
176866     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
176866     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.4ns 
176867     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
179270     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
179271     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
180057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
180060     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.22ms 
180061     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
180062     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.8ns 
180062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
182482     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
182483     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
183272     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
183301     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.21ms 
183303     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
183303     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 226ns 
183304     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
185716     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
185716     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
186511     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
186532     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.19ms 
186534     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
186534     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 283.3ns 
186535     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
188950     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
188950     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
189741     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
189744     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.44ms 
189746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
189746     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.9ns 
189747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
192173     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
192173     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
192978     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
193081     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 92.12ms 
193083     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
193083     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.4ns 
193084     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
195515     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
195515     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
196330     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
196344     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.63ms 
196346     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
196346     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.8ns 
196348     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
198770     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
198770     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
199561     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
199567     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.18ms 
199568     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
199568     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.1ns 
199569     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
201987     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
201987     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
202776     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
202796     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.64ms 
202798     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
202798     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 265.2ns 
202799     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
205206     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
205207     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
205991     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
206001     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.14ms 
206003     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
206003     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.3ns 
206004     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
208406     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
208406     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
209188     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
209191     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.38ms 
209193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
209193     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.6ns 
209193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
211594     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
211594     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
212382     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
212385     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.94ms 
212387     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
212387     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75ns 
212388     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
214798     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
214799     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
215588     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
215602     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.19ms 
215603     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
215603     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.4ns 
215604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
218031     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
218031     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
218828     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
218840     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.55ms 
218842     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
218842     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.8ns 
218843     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
221266     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
221266     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
222054     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
222066     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.11ms 
222067     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
222067     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.3ns 
222068     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
224485     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
224485     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
225270     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
225273     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.05ms 
225276     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
225277     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 261.7ns 
225278     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
227695     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
227695     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
228480     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
228483     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.4ms 
228484     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
228485     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.5ns 
228485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
230877     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
230877     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
231661     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
231665     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.87ms 
231667     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
231667     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.4ns 
231667     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
234102     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
234103     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
234869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
234872     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 823.91ns 
234873     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
234873     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.4ns 
234874     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
237310     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
237311     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
238078     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
238080     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 525.6ns 
238082     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
238082     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.2ns 
238083     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
240532     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
240532     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
241300     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
241303     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.57ms 
241305     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
241305     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.4ns 
241306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
243728     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
243729     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
244490     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
244493     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 671.8ns 
244494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
244494     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.2ns 
244495     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
246917     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
246918     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
247682     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
247717     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.91ms 
247719     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
247720     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 242.5ns 
247721     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
250153     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
250153     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
250916     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
250949     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.9ms 
250951     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
250951     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88ns 
250952     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
253396     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
253396     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
254208     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
254234     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.37ms 
254238     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
254238     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 259.9ns 
254239     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
256700     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
256700     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
257462     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
257491     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.91ms 
257493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
257493     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.5ns 
257493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
259904     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
259904     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
260664     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
260684     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.91ms 
260686     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
260686     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.2ns 
260687     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
263104     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
263104     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
263867     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
263904     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.06ms 
263906     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
263906     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.3ns 
263907     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
266334     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
266334     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
267095     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
267113     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.82ms 
267115     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
267115     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.1ns 
267116     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
269529     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
269529     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
270291     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
270305     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.44ms 
270306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
270306     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.7ns 
270307     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
272732     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
272732     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
273494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
273509     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.46ms 
273510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
273511     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.2ns 
273511     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
275923     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
275923     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
276683     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
276715     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.19ms 
276716     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
276716     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.4ns 
276717     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
279132     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
279132     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
279891     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
279907     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.63ms 
279909     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
279909     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.9ns 
279910     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
282348     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
282348     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
283106     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
283122     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.71ms 
283123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
283124     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.2ns 
283124     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
285643     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
285643     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
286407     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
286424     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.48ms 
286426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
286426     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.7ns 
286426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
288859     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
288859     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
289622     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
289638     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.03ms 
289639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
289639     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.1ns 
289640     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
292064     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
292064     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
292829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
292843     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.12ms 
292844     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
292845     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.5ns 
292845     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
295280     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
295280     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
296044     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
296060     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.09ms 
296061     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
296061     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.2ns 
296062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
298479     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
298479     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
299241     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
299256     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.54ms 
299258     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
299258     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.1ns 
299258     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
301684     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
301684     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
302446     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
302452     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.59ms 
302453     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
302454     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.6ns 
302454     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
304885     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
304885     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
305650     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
305661     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.19ms 
305663     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
305663     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.3ns 
305663     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
308095     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
308095     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
308859     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
308862     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.64ms 
308863     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
308863     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.1ns 
308864     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
311297     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
311298     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
312061     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
312063     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 588.9ns 
312065     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
312065     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.6ns 
312065     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
314484     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
314484     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
315252     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
315256     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.56ms 
315259     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
315259     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 220.4ns 
315260     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
317688     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
317688     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
318454     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
318459     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.11ms 
318461     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
318461     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.4ns 
318462     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
320878     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
320878     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
321643     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
321649     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.35ms 
321651     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
321651     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 215.5ns 
321652     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
324109     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
324110     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
324874     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
324913     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.44ms 
324915     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
324915     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.5ns 
324915     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
327314     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
327314     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
328103     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
328107     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.58ms 
328108     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
328108     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.1ns 
328108     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
330509     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
330509     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
331298     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
331300     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 489.2ns 
331302     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
331302     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.6ns 
331302     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
333692     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
333692     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
334475     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
334480     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.72ms 
334481     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
334481     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.5ns 
334482     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
336878     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
336878     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
337673     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
337675     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 487.1ns 
337679     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
337679     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 220.2ns 
337680     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
340081     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
340081     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
340867     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
340869     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 499.8ns 
340870     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
340870     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.8ns 
340871     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
343278     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
343278     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
344063     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
344065     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 528.4ns 
344067     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
344067     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 192.6ns 
344068     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
346465     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
346466     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
347258     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
347262     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.71ms 
347263     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
347263     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.1ns 
347264     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
349658     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
349658     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
350446     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
350453     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.8ms 
350454     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
350454     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.2ns 
350455     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
352857     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
352857     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
353652     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
353655     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.41ms 
353656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
353657     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.2ns 
353657     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
356063     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
356063     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
356851     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
356856     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.38ms 
356857     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
356857     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.3ns 
356858     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
359252     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
359252     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
360035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
360039     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.95ms 
360040     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
360040     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.2ns 
360041     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
362443     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
362443     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
363227     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
363239     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.44ms 
363240     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
363240     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.6ns 
363241     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
365647     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
365648     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
366433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
366436     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.57ms 
366437     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
366437     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.9ns 
366438     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
368845     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
368845     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
369631     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
369634     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.11ms 
369635     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
369635     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.9ns 
369635     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
372026     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
372026     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
372809     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
372812     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.66ms 
372813     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
372814     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.5ns 
372814     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
375200     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
375200     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
375983     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
375996     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.28ms 
375997     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
375997     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.6ns 
375998     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
378400     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
378401     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
379183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
379187     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 300ns 
379189     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
379190     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.2ns 
379190     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
381589     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
381589     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
382369     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
382395     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.7ms 
382396     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
382397     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.6ns 
382397     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
384785     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
384785     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
385570     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
385574     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.5ms 
385575     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
385575     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.2ns 
385577     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
387969     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
387969     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
388752     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
388767     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.68ms 
388768     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
388768     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.7ns 
388769     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
391162     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
391162     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
391950     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
391964     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.4ms 
391966     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
391966     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.8ns 
391966     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
394385     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
394386     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
395171     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
395189     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.76ms 
395191     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
395191     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.4ns 
395191     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
397613     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
397613     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
398403     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
398405     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 508.7ns 
398407     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
398407     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.8ns 
398407     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
400819     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
400819     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
401608     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
401613     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.07ms 
401614     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
401614     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.6ns 
401615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
404009     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
404009     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
404796     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
404799     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.39ms 
404800     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
404800     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61ns 
404801     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
407191     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
407191     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
407977     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
407980     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 744.71ns 
407981     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
407981     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.6ns 
407982     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
410373     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
410373     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
411160     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
411163     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 698.01ns 
411165     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
411165     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 212.5ns 
411166     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
413559     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
413559     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
414346     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
414348     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.06ms 
414350     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
414350     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.7ns 
414350     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
416739     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
416739     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
417528     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
417531     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 993.21ns 
417532     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
417532     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.5ns 
417533     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
419937     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
419938     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
420729     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
420737     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.89ms 
420738     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
420738     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.3ns 
420739     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
423135     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
423135     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
423927     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
423934     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.25ms 
423935     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
423935     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.6ns 
423936     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
426330     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
426330     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
427119     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
427125     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.14ms 
427132     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
427132     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 232.7ns 
427133     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
429535     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
429535     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
430328     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
430335     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.88ms 
430337     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
430337     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.1ns 
430337     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
432732     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
432732     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
433528     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
433532     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.08ms 
433533     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
433533     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.1ns 
433534     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
435924     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
435924     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
436719     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
436724     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.93ms 
436725     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
436725     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.3ns 
436726     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
439135     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
439135     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
439906     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
439909     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 758.71ns 
439910     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
439910     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.4ns 
439911     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
442326     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
442326     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
443096     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
443098     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 951.81ns 
443100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
443100     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.1ns 
443100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
445505     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
445505     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
446277     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
446280     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 938.41ns 
446281     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
446281     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.7ns 
446282     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
448680     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
448681     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
449474     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
449483     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.71ms 
449484     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
449484     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.4ns 
449485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
451893     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
451893     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
452687     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
452690     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.22ms 
452691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
452691     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.6ns 
452692     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
455081     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
455081     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
455878     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
455884     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.11ms 
455887     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
455887     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.8ns 
455887     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
458276     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
458276     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
459070     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
459072     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 740.4ns 
459073     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
459073     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.2ns 
459074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
461453     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
461453     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
462243     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
462246     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 616.7ns 
462247     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
462247     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.1ns 
462248     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
464650     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
464650     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
465416     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
465419     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.29ms 
465420     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
465420     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.1ns 
465421     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
467818     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
467818     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
468586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
468588     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 749.3ns 
468589     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
468589     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.6ns 
468590     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
471017     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
471017     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
471808     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
471811     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.05ms 
471812     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
471812     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.6ns 
471813     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
474210     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
474210     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
475003     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
475005     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 999.01ns 
475007     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
475007     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.7ns 
475007     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
477398     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
477398     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
478187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
478190     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.93ms 
478192     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
478192     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64ns 
478192     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
480568     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
480568     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
481373     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
481377     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.65ms 
481380     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
481380     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.7ns 
481380     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
483783     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
483783     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
484551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
484559     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.21ms 
484560     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
484560     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.3ns 
484561     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
486976     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
486976     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
487771     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
487773     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 530.9ns 
487775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
487775     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61ns 
487775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
490163     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
490163     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
490957     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
490962     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.51ms 
490964     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
490964     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.7ns 
490965     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
493345     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
493345     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
494155     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
494158     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 795.11ns 
494159     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
494159     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.3ns 
494159     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
496552     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
496553     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
497321     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
497323     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 680.71ns 
497324     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
497324     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.4ns 
497325     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
499751     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
499751     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
500550     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
500553     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.77ms 
500554     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
500554     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.9ns 
500555     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
502947     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
502947     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
503747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
503749     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 826.31ns 
503750     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
503750     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.9ns 
503751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
506134     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
506134     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
506925     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
506928     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.29ms 
506929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
506929     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.5ns 
506930     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
509335     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
509335     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
510104     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
510107     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.2ms 
510109     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
510109     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.8ns 
510110     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
512530     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
512530     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
513324     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
513328     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.24ms 
513329     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
513330     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.9ns 
513330     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
515723     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
515723     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
516515     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
516522     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.2ms 
516524     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
516524     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.3ns 
516524     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
518923     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
518923     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
519723     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
519731     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.56ms 
519732     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
519732     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.3ns 
519733     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
522146     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
522146     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
522940     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
522946     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.04ms 
522947     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
522947     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70ns 
522948     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
525336     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
525336     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
526127     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
526133     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.93ms 
526135     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
526135     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.8ns 
526135     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
528516     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
528516     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
529311     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
529321     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.61ms 
529322     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
529322     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.3ns 
529323     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
531729     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
531729     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
532521     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
532531     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.46ms 
532532     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
532533     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.6ns 
532533     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
534913     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
534914     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
535705     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
535714     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.84ms 
535716     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
535716     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.7ns 
535716     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
538117     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
538118     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
538886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
538892     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.5ms 
538894     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
538894     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.8ns 
538894     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
541294     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
541295     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
542089     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
542109     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.45ms 
542110     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
542110     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.4ns 
542111     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
544498     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
544498     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
545290     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
545316     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.79ms 
545318     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
545318     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 207ns 
545319     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
547732     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
547732     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
548523     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
548542     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.61ms 
548544     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
548544     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.3ns 
548544     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
550946     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
550946     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
551743     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
551762     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.89ms 
551763     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
551763     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.3ns 
551764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
554178     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
554178     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
554950     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
554968     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.12ms 
554970     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
554970     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.7ns 
554971     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
557385     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
557385     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
558178     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
558223     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.01ms 
558225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
558225     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.4ns 
558226     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
560621     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
560621     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
561415     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
561419     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.57ms 
561421     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
561421     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.2ns 
561422     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
563858     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
563858     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
564651     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
564655     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.99ms 
564657     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
564657     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.2ns 
564657     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
567044     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
567044     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
567837     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
567840     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.86ms 
567842     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
567842     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.4ns 
567842     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
570253     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
570253     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
571045     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
571057     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.49ms 
571059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
571059     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.1ns 
571059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
573447     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
573448     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
574242     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
574248     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.06ms 
574249     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
574249     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.8ns 
574250     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
576653     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
576653     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
577444     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
577447     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.28ms 
577448     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
577448     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.3ns 
577449     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
579836     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
579836     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
580629     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
580638     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.02ms 
580640     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
580640     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.5ns 
580640     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
583038     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
583039     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
583834     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
583844     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.66ms 
583845     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
583845     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.8ns 
583846     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
586238     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
586238     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
587032     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
587045     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.09ms 
587047     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
587047     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 193.7ns 
587048     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
589463     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
589464     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
590258     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
590260     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 990.01ns 
590262     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
590262     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53ns 
590262     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
592657     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
592657     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
593459     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
593462     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.55ms 
593463     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
593463     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72ns 
593464     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
595880     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
595880     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
596678     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
596683     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.83ms 
596685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
596685     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.2ns 
596685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
599090     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
599090     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
599859     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
599864     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.56ms 
599865     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
599865     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.5ns 
599866     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
602274     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
602274     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
603063     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
603104     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.15ms 
603105     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
603105     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.8ns 
603106     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
605532     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
605532     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
606330     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
606352     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.54ms 
606354     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
606354     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 222.8ns 
606355     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
608748     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
608748     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
609540     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
609551     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.69ms 
609552     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
609552     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.3ns 
609553     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
611959     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
611959     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
612757     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
612759     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 197.7ns 
612760     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
612760     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.5ns 
612761     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
615168     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
615168     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
615939     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
616045     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 94.77ms 
616047     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
616047     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 122.1ns 
616048     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
618440     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
618441     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
619232     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
619265     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.47ms 
619267     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
619267     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.7ns 
619268     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
621679     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
621679     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
622475     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
622477     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 270.8ns 
622479     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
622479     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65ns 
622479     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
624888     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
624888     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
625660     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
625662     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 207.7ns 
625663     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
625663     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.5ns 
625664     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
628085     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
628085     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
628884     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
628886     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 202.2ns 
628887     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
628887     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.6ns 
628888     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
631304     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
631304     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
632103     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
632105     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 443.7ns 
632106     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
632106     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.1ns 
632107     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
634526     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
634526     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
635325     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
635408     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
635416     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 88.57ms 
635423     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
635423     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101ns 
635424     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
637866     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
637866     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
638660     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
638709     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
638710     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 47.56ms 
638712     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
638712     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.6ns 
638712     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
641165     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
641165     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
641968     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
641969     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.8ns 
641995     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
642033     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
642046     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
642050     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
642060     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
642061     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
642063     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
642064     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
642067     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
642068     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
642070     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
642071     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
642230     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
642231     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
642232     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
642233     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
642234     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
642345     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
642347     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
642348     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
642349     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
642350     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
642351     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
642530     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
642532     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
642533     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
642534     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
642535     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
642536     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
642686     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
642687     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
642688     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
642688     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
642689     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
642690     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
642707     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
642708     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
642709     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
642711     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
642712     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
642713     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
642724     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
642725     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
642726     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
642727     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
642727     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
642728     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
642892     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
642893     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
642895     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
643039     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
643040     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'instantiate hide var='v_r' with='seqSwap(s_0,v_x_0,jv_0)'' 
643042     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
643044     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
643045     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
643046     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
643047     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
643048     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
643052     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
643053     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
643055     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
643056     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
643057     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
643179     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
643183     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
643185     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
643186     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
643187     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
643187     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
643188     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
643323     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
643325     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
643326     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
643328     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
643329     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
643329     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
643330     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
643331     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
643439     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
643441     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
643535     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
643540     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
643545     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
643546     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
643547     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
643548     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
643549     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
643550     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
643551     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
643551     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
643560     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
643566     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
643673     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
643674     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
643676     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
643677     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
643678     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
643678     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
643679     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
643680     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
643736     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
643743     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
643902     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
643903     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
643904     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
643906     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
643907     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
643908     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
644084     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
644088     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
644089     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 111: 'instantiate hide var=v_r with='seqSwap(s_0,v_y_0,jv_1)'' 
644090     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
644092     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
644093     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
644093     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
644094     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
644105     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
644107     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
644108     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
644109     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
644237     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
644238     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
644239     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
644240     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
644241     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
644242     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
644372     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
644373     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
644374     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
644375     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
644376     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
644377     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
644378     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
644378     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
644472     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
644473     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
644565     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
644566     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
644567     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
644572     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
644576     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
644581     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
644728     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
644729     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
644735     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
644736     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
644748     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
644859     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
648803     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
648805     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 150: 'instantiate hide var=v_r with='seqSwap(s_0,v_x_0,jv_0)'' 
648810     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
648812     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
648813     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
648814     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
648814     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
648824     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
648825     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
648826     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
648828     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
648829     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
648926     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
648930     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
648931     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
648932     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
648932     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
648933     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
648934     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
649030     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
649031     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
649032     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
649033     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
649034     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
649035     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
649035     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
649036     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
649155     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
649157     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
649231     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
649235     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
649239     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
649240     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
649241     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
649244     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
649254     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
649335     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
649336     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
649337     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
649338     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
649411     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
649420     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
649421     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 191: 'instantiate hide var=v_r with='seqSwap(seqSwap(s_0,jv_0,v_x_0),jv_0,v_y_0)'' 
649422     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
649424     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
649424     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
649425     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
649425     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
649437     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
649437     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
649438     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
649439     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
649440     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
649529     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
649530     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
649531     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
649532     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
649533     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
649625     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
649634     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
649635     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
649636     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
649636     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
649637     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
649638     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
649747     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
649748     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
649750     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
649751     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
649753     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
649755     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
649757     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
649757     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
649758     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
649759     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
649760     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
649760     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
649761     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
649761     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
649761     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
649852     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
649853     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
649859     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
649936     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
650015     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
650017     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
650017     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
650018     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
650019     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
650020     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
650020     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
650020     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
650021     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
650109     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
650115     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
650206     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
650207     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
650208     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
650210     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
650210     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
650211     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
650211     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
650212     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
650217     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
650218     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
650296     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
650302     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
650312     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
650414     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
650416     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
650417     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
650418     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
650418     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
650419     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
650419     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
650420     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
650473     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
650475     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
650475     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
650476     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
650477     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
650482     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
650488     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
650603     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
650691     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
650692     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
650693     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
650694     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
650865     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
650953     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
650954     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
653938     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
653943     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
653944     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
653945     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
653946     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
654060     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
654061     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
654062     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
654063     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
654064     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
654168     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
657086     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
660167     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
660171     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
660172     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
660173     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
660173     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
660285     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
660286     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
660286     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
660287     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 300: 'instantiate hide var=v_r with='seqSwap(seqSwap(s_0, v_x_0, jv_0), v_y_0, jv_1)' ...' 
660288     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
661412     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
661412     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.3ns 
661413     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
663912     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
663912     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
664738     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
664740     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.7ns 
664740     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
664746     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
664755     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
664758     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
664760     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
664761     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
664765     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
664766     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
664770     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
664770     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
664772     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
664781     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
664781     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
664783     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
664828     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
664828     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
664829     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
664829     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
664830     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
664896     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
664896     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
664896     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
664897     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
664898     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
664902     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
664902     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
664902     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
664903     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
664903     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
664904     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
664986     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
664987     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
664987     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
664988     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
664989     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
664989     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
665076     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
665077     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
665078     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
665078     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
665079     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
665079     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
665080     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
665080     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
665081     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
665081     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
665082     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
665082     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
665082     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
665083     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
665083     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
665084     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
665084     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
665085     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
665086     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
665088     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
665128     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
665129     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
665192     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
665193     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
665194     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
665195     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
665196     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
665197     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
665254     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
665256     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
665257     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
665258     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
665259     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
665260     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
665261     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
665320     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
665323     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
665326     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
665399     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
665463     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
665463     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 257.5ns 
665464     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
667895     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
667895     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
668712     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
668728     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.92ms