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

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

tests
0

failures
0

ignored
14m6.17s

duration
100%

successful

Tests

Test Method name Duration Result
powPositive data()[100] 4.139s passed
powPositiveConcrete data()[101] 4.154s passed
powGeq1Concrete data()[102] 4.125s passed
pow2InIntLower data()[103] 4.119s passed
pow2InIntUpper data()[104] 4.124s passed
logSelfConcrete data()[105] 4.070s passed
log1Concrete data()[106] 4.197s passed
logProduct data()[107] 4.147s passed
logTimesBaseConcrete data()[108] 4.076s passed
logProdIdentity data()[109] 4.165s passed
moduloByteIsInByte data()[10] 4.619s passed
logProdIdentityConcrete data()[110] 4.120s passed
logPowIdentity data()[111] 4.094s passed
logPowIdentityConcrete data()[112] 4.183s passed
logPositive data()[113] 4.180s passed
logPositiveConcrete data()[114] 4.207s passed
logMono data()[115] 4.173s passed
logMonoConcrete data()[116] 4.142s passed
powLogLess data()[117] 4.135s passed
powLogMore2 data()[118] 4.191s passed
logLessThanPow data()[119] 4.133s passed
moduloCharIsInChar data()[11] 4.401s passed
logLessThanPowConcrete data()[120] 4.224s passed
logSqueeze data()[121] 4.000s passed
ifthenelse_equals data()[122] 4.011s passed
ifthenelse_equals_1 data()[123] 4.930s passed
ifthenelse_equals_2 data()[124] 3.951s passed
disjointWithSingleton1 data()[125] 3.876s passed
disjointWithSingleton2 data()[126] 3.876s passed
disjointArrayRanges data()[127] 3.895s passed
disjointArrayRangeAllFields1 data()[128] 3.991s passed
disjointArrayRangeAllFields2 data()[129] 3.885s passed
div_unique1 data()[12] 4.880s passed
seqSelfDefinition data()[130] 3.891s passed
seqOutsideValue data()[131] 3.915s passed
castedGetAny data()[132] 3.869s passed
seqGetAlphaCast data()[133] 3.907s passed
getOfSeqSingleton data()[134] 3.949s passed
getOfSeqSingletonConcrete data()[135] 4.029s passed
getOfSeqConcat data()[136] 3.947s passed
getOfSeqSub data()[137] 3.917s passed
getOfSeqReverse data()[138] 3.886s passed
lenOfSeqEmpty data()[139] 3.877s passed
div_unique2 data()[13] 4.425s passed
lenOfSeqSingleton data()[140] 3.869s passed
lenOfSeqConcat data()[141] 3.841s passed
lenOfSeqSub data()[142] 3.853s passed
lenOfSeqReverse data()[143] 3.839s passed
equalityToSeqGetAndSeqLenLeft data()[144] 3.968s passed
equalityToSeqGetAndSeqLenRight data()[145] 4.015s passed
getOfSeqSingletonEQ data()[146] 3.984s passed
getOfSeqConcatEQ data()[147] 3.910s passed
getOfSeqSubEQ data()[148] 3.853s passed
getOfSeqReverseEQ data()[149] 3.853s passed
div_exists data()[14] 4.643s passed
lenOfSeqEmptyEQ data()[150] 3.982s passed
lenOfSeqSingletonEQ data()[151] 3.925s passed
lenOfSeqConcatEQ data()[152] 3.948s passed
lenOfSeqSubEQ data()[153] 3.891s passed
lenOfSeqReverseEQ data()[154] 3.913s passed
getOfSeqDefEQ data()[155] 3.941s passed
lenOfSeqDefEQ data()[156] 3.883s passed
seqConcatWithSeqEmpty1 data()[157] 3.938s passed
seqConcatWithSeqEmpty2 data()[158] 4.074s passed
seqReverseOfSeqEmpty data()[159] 4.088s passed
div_one data()[15] 4.416s passed
subSeqComplete data()[160] 3.930s passed
subSeqTailR data()[161] 4.535s passed
subSeqTailL data()[162] 4.364s passed
subSeqTailEQR data()[163] 4.041s passed
subSeqTailEQL data()[164] 4.400s passed
seqDef_split data()[165] 4.310s passed
seqDef_induction_upper data()[166] 4.119s passed
seqDef_induction_upper_concrete data()[167] 4.205s passed
seqDef_induction_lower data()[168] 4.121s passed
seqDef_induction_lower_concrete data()[169] 4.201s passed
jdiv_one data()[16] 4.268s passed
seqDef_split_in_three data()[170] 4.282s passed
seqDef_empty data()[171] 4.200s passed
seqDef_one_summand data()[172] 4.301s passed
seqDef_lower_equals_upper data()[173] 4.191s passed
seqDefOfSeq data()[174] 4.126s passed
seqSelfDefinitionEQ2 data()[175] 4.178s passed
indexOfSeqSingleton data()[176] 4.117s passed
indexOfSeqConcatFirst data()[177] 4.524s passed
indexOfSeqConcatSecond data()[178] 3.959s passed
indexOfSeqSub data()[179] 3.954s passed
div_zero data()[17] 4.305s passed
lenOfArray2seq data()[180] 3.921s passed
getAnyOfArray2seq data()[181] 3.922s passed
getOfArray2seq data()[182] 3.965s passed
getAnyOfNPermInv data()[183] 4.031s passed
seqNPermRange data()[184] 4.124s passed
seqPermTrans data()[185] 3.957s passed
seqPermRefl data()[186] 4.021s passed
seqPermSplit data()[187] 3.920s passed
seqNPermRight data()[188] 4.118s passed
seqPermFromSwap data()[189] 3.990s passed
divResZero1 data()[18] 4.373s passed
seqPermTransAlt0 data()[190] 3.941s passed
seqPermTransAlt1 data()[191] 3.914s passed
seqPermTransAlt2 data()[192] 3.913s passed
seqPermTransAlt3 data()[193] 3.888s passed
seqPermForall data()[194] 4.026s passed
seqPermExists data()[195] 4.030s passed
schiffl_lemma_2 data()[196] 25.708s passed
schiffl_thm_1 data()[197] 4.957s passed
eqSameSeq data()[198] 4.080s passed
divResZero2 data()[19] 4.327s passed
eqTermCut data()[1] 4.939s passed
divResOne1 data()[20] 4.315s passed
divResOne2 data()[21] 4.334s passed
div_cancel1 data()[22] 4.313s passed
div_cancel2 data()[23] 4.241s passed
divAddMultDenom data()[24] 4.226s passed
divMinus data()[25] 4.279s passed
divMinusDenom data()[26] 4.278s passed
divLeastDPos data()[27] 4.243s passed
divLeastDNeg data()[28] 4.304s passed
divGreatestDPos data()[29] 4.169s passed
equivAllRight data()[2] 4.740s passed
divGreatestDNeg data()[30] 4.149s passed
divIncreasingPos data()[31] 4.216s passed
divIncreasingNeg data()[32] 4.156s passed
jdiv_zero data()[33] 4.130s passed
jdivPulloutMinusNum data()[34] 4.277s passed
jdivPulloutMinusDenom data()[35] 4.239s passed
jdiv_uniquePosPos data()[36] 4.192s passed
jdiv_uniquePosNeg data()[37] 4.257s passed
jdiv_uniqueNegPos data()[38] 4.190s passed
jdiv_uniqueNegNeg data()[39] 4.145s passed
irrflConcrete1 data()[3] 4.716s passed
jdivMultDenom1 data()[40] 4.207s passed
jdivMultDenom2 data()[41] 4.145s passed
mod_geZero data()[42] 4.208s passed
mod_lessDenom data()[43] 4.237s passed
jmod_NumPos data()[44] 4.199s passed
jmod_NumNeg data()[45] 4.143s passed
jmod_geZero data()[46] 4.174s passed
jmodNumZero data()[47] 4.173s passed
jmod_pulloutminusNum data()[48] 4.149s passed
jmod_pulloutminusDenom data()[49] 4.219s passed
irrflConcrete2 data()[4] 4.552s passed
jmodUnique1 data()[50] 4.225s passed
jmodUnique2 data()[51] 4.206s passed
intDivRem data()[52] 4.125s passed
jmodjmod data()[53] 4.125s passed
jmodDivisible data()[54] 4.109s passed
jmodDivisibleRep data()[55] 4.112s passed
jdivAddMultDenom data()[56] 4.455s passed
jmodAltZero data()[57] 4.220s passed
jmodAddMultDenomZero data()[58] 4.291s passed
polyDiv_zero data()[59] 4.209s passed
cancel_gtPos data()[5] 4.699s passed
polyMod_ltdivDenom data()[60] 4.168s passed
bsum_empty data()[61] 4.090s passed
bsum_induction_upper data()[62] 4.150s passed
bsum_induction_lower data()[63] 4.183s passed
bsum_num_of_bounds data()[64] 4.151s passed
bsum_num_of_bounds2 data()[65] 4.146s passed
bsum_induction_upper2 data()[66] 4.166s passed
bsum_induction_upper_concrete data()[67] 4.105s passed
bsum_induction_upper_concrete_2 data()[68] 4.101s passed
bsum_induction_upper2_concrete data()[69] 4.112s passed
cancel_gtNeg data()[6] 4.655s passed
bsum_induction_lower_concrete data()[70] 4.100s passed
bsum_induction_lower2 data()[71] 4.162s passed
bsum_induction_lower2_concrete data()[72] 4.126s passed
bsum_positive data()[73] 4.261s passed
bsum_upper_bound data()[74] 4.225s passed
bsum_lower_bound data()[75] 4.173s passed
bsum_positive_lower_bound_element data()[76] 4.236s passed
bsum_sub_same_index data()[77] 4.178s passed
bsum_less_same_index data()[78] 4.210s passed
bsum_equal_except_one_index data()[79] 4.144s passed
moduloIntIsInInt data()[7] 4.716s passed
bsum_num_of_is_max data()[80] 4.233s passed
bsum_num_of_is_max2 data()[81] 4.227s passed
bsum_num_of_is_max3 data()[82] 4.211s passed
bsum_num_of_is_max4 data()[83] 4.196s passed
bsum_num_of_lt_max data()[84] 4.184s passed
bsum_num_of_lt_max2 data()[85] 4.284s passed
bsum_num_of_lt_max3 data()[86] 4.203s passed
bsum_num_of_lt_max4 data()[87] 4.243s passed
bsum_num_of_gt0 data()[88] 4.200s passed
bsum_num_of_gt0_alt data()[89] 4.139s passed
moduloLongIsInLong data()[8] 4.711s passed
bsum_add_concrete data()[90] 4.199s passed
bprod_all_positive data()[91] 4.137s passed
bprod_split data()[92] 4.149s passed
powConcrete0 data()[93] 4.150s passed
powConcrete1 data()[94] 4.135s passed
powSplitFactor data()[95] 4.126s passed
powAdd data()[96] 4.103s passed
powMono data()[97] 4.093s passed
powMonoConcrete data()[98] 4.150s passed
powMonoConcreteRight data()[99] 4.212s passed
moduloShortIsInShort data()[9] 4.691s passed

Standard output

406        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
447        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 20.46ms 
750        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
784        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)

1948       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1990       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1992       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1993       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
3849       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
11155      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 10.4s 
11261      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
11321      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.8ns 
11338      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
11339      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 639.29ns 
11347      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
15065      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.72s 
15068      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
16235      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
16267      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.66ms 
16281      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
16282      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 192ns 
16284      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
19869      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.59s 
19870      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
21003      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
21019      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.76ms 
21021      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
21022      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 148.1ns 
21023      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
24556      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.53s 
24556      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
25717      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
25732      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.84ms 
25739      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
25740      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 160.3ns 
25742      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
29147      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.4s 
29147      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
30274      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
30289      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.51ms 
30294      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
30295      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.28ms 
30298      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
33704      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.41s 
33705      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
34893      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
34988      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 85.5ms 
34998      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
34999      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.17ms 
35001      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
38480      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.48s 
38481      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
39626      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
39647      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.96ms 
39652      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
39652      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 444.57ns 
39653      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
43177      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.52s 
43178      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
44359      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
44364      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.86ms 
44368      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
44368      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 381.8ns 
44370      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
47926      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.56s 
47927      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
49073      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
49076      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 656.19ns 
49080      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
49080      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 490.59ns 
49082      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
52588      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.51s 
52589      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
53765      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
53769      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 963.99ns 
53772      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
53773      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 440.1ns 
53774      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
57230      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.46s 
57230      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
58385      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
58389      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 595.59ns 
58396      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
58397      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 456.69ns 
58398      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
61741      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.34s 
61742      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
62786      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
62790      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 672.39ns 
62793      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
62793      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 393.3ns 
62795      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
66417      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.62s 
66418      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
67570      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
67661      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 78.82ms 
67672      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
67672      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 127.2ns 
67673      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
70961      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 
70962      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
72012      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
72095      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 76.14ms 
72098      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
72099      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 906.09ns 
72103      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
75532      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.43s 
75533      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
76605      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
76738      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 122.25ms 
76741      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
76742      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 381.4ns 
76744      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
80018      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 
80018      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
81148      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
81155      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.79ms 
81158      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
81158      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 216ns 
81159      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
84375      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
84376      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
85418      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
85424      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.7ms 
85426      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
85426      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.9ns 
85427      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
88607      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
88608      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
89661      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
89728      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 61.74ms 
89731      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
89731      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 427.1ns 
89733      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
93014      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
93015      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
94078      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
94100      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.5ms 
94104      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
94104      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 381.7ns 
94106      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
97360      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
97361      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
98405      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
98428      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.08ms 
98431      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
98431      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 119.9ns 
98432      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
101707     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
101708     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
102723     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
102744     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.17ms 
102745     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
102746     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 138.4ns 
102747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
106008     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
106008     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
107062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
107078     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.21ms 
107080     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
107081     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 248.9ns 
107082     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
110290     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
110290     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
111358     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
111391     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.01ms 
111396     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
111396     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 433.2ns 
111398     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
114628     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
114628     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
115627     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
115633     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.57ms 
115634     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
115635     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 140.1ns 
115636     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
118788     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
118789     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
119810     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
119858     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.95ms 
119861     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
119862     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 342.2ns 
119863     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
123025     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
123025     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
124041     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
124133     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 80.71ms 
124140     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
124141     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 369.4ns 
124142     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
127322     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
127322     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
128356     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
128416     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 54.15ms 
128418     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
128419     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 122.2ns 
128420     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
131601     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
131602     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
132650     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
132659     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.92ms 
132661     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
132661     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.3ns 
132662     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
135942     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
135942     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
136935     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
136962     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.75ms 
136965     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
136965     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.1ns 
136966     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
140126     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
140126     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
141114     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
141131     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.04ms 
141133     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
141134     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 136.7ns 
141136     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
144275     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
144275     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
145269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
145281     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.95ms 
145283     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
145283     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96ns 
145284     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
148442     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
148443     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
149487     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
149497     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.87ms 
149500     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
149500     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 433ns 
149502     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
152605     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
152606     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
153644     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
153653     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.35ms 
153655     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
153655     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.3ns 
153656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
156789     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
156789     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
157779     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
157784     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.14ms 
157785     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
157785     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.2ns 
157786     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
160980     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
160981     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
162046     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
162060     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.7ms 
162062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
162062     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 114.6ns 
162063     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
165210     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
165210     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
166248     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
166299     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.86ms 
166301     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
166301     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.1ns 
166302     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
169429     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
169431     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
170463     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
170490     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.74ms 
170493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
170494     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 412.5ns 
170495     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
173714     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
173714     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
174727     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
174748     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.65ms 
174750     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
174750     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 125.3ns 
174751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
177898     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
177898     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
178914     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
178938     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.59ms 
178940     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
178940     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 146.8ns 
178941     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
182076     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
182076     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
183062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
183083     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.49ms 
183085     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
183085     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.5ns 
183086     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
186227     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
186228     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
187245     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
187290     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.96ms 
187292     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
187292     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.3ns 
187293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
190429     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
190430     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
191432     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
191435     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.31ms 
191437     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
191438     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 219.49ns 
191439     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
194628     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
194629     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
195639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
195644     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.8ms 
195645     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
195645     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.3ns 
195646     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
198805     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
198806     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
199868     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
199879     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.5ms 
199882     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
199883     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 398.69ns 
199884     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
203033     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
203033     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
204070     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
204079     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.03ms 
204081     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
204081     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.3ns 
204082     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
207191     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
207191     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
208201     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
208222     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.84ms 
208223     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
208223     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 132.8ns 
208224     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
211364     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
211364     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
212384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
212396     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.32ms 
212398     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
212399     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.7ns 
212399     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
215542     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
215542     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
216564     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
216569     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.58ms 
216574     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
216574     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 398.3ns 
216575     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
219701     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
219702     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
220714     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
220719     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.55ms 
220721     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
220721     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.6ns 
220722     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
223882     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
223882     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
224923     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
224930     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.9ms 
224945     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
224946     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 296.8ns 
224947     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
228078     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
228079     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
229083     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
229166     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 73.45ms 
229170     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
229170     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 299.2ns 
229172     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
232280     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
232281     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
233276     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
233373     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 86.65ms 
233375     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
233375     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 175.3ns 
233376     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
236498     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
236498     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
237495     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
237499     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.59ms 
237500     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
237500     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.3ns 
237501     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
240570     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
240571     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
241583     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
241623     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.31ms 
241625     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
241625     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 190.3ns 
241626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
244704     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
244705     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
245703     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
245732     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.74ms 
245734     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
245734     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 122.5ns 
245735     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
248829     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
248830     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
249840     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
249844     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.7ms 
249846     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
249846     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 251.8ns 
249848     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
253048     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
253048     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
254079     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
254298     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 206.83ms 
254302     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
254302     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 303ns 
254303     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
257530     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
257530     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
258505     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
258519     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.43ms 
258520     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
258521     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 125.7ns 
258522     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
261769     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
261770     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
262803     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
262810     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.32ms 
262812     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
262812     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.9ns 
262813     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
265984     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
265984     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
267000     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
267019     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.37ms 
267021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
267021     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81ns 
267022     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
270162     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
270162     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
271173     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
271186     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.24ms 
271189     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
271189     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.3ns 
271190     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
274285     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
274285     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
275273     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
275277     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.74ms 
275278     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
275278     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.2ns 
275279     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
278429     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
278430     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
279423     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
279427     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.46ms 
279429     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
279429     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.9ns 
279430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
282573     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
282574     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
283591     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
283610     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.98ms 
283612     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
283612     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.2ns 
283613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
286742     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
286743     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
287744     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
287761     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.04ms 
287763     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
287763     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 117.5ns 
287764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
290932     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
290932     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
291892     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
291907     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.03ms 
291909     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
291909     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.1ns 
291910     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
295058     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
295058     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
296070     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
296074     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.63ms 
296075     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
296075     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.1ns 
296076     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
299165     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
299166     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
300174     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
300178     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.81ms 
300179     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
300180     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.1ns 
300180     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
303266     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
303266     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
304273     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
304279     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.79ms 
304281     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
304281     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.9ns 
304282     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
307374     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
307375     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
308388     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
308391     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.15ms 
308392     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
308392     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93ns 
308393     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
311482     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
311482     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
312488     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
312491     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 608.1ns 
312492     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
312492     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.7ns 
312493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
315656     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
315656     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
316649     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
316653     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.3ms 
316655     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
316655     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.8ns 
316656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
319781     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
319781     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
320775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
320778     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 872.69ns 
320781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
320781     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.3ns 
320782     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
323920     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
323920     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
324973     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
325040     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 63.61ms 
325042     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
325042     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.6ns 
325044     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
328242     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
328243     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
329224     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
329265     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.18ms 
329267     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
329268     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 229.9ns 
329269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
332414     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
332414     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
333401     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
333438     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.09ms 
333440     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
333440     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.9ns 
333441     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
336628     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
336629     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
337623     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
337674     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 45.5ms 
337676     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
337676     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 188.6ns 
337677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
340829     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
340829     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
341823     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
341851     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.06ms 
341854     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
341855     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 244.1ns 
341856     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
344997     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
344997     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
346020     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
346062     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.7ms 
346064     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
346064     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.9ns 
346065     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
349171     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
349171     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
350181     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
350206     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.72ms 
350207     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
350207     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.6ns 
350208     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
353398     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
353398     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
354422     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
354439     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.57ms 
354440     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
354440     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.5ns 
354441     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
357608     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
357608     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
358645     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
358666     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.05ms 
358669     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
358669     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 219.4ns 
358670     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
361837     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
361837     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
362861     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
362877     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.31ms 
362879     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
362879     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.5ns 
362880     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
366032     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
366032     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
367051     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
367073     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.37ms 
367075     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
367075     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.9ns 
367076     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
370222     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
370222     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
371232     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
371257     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.35ms 
371259     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
371259     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 124.4ns 
371260     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
374526     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 
374527     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
375520     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
375541     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.61ms 
375543     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
375543     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73ns 
375544     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
378718     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
378718     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
379725     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
379745     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.11ms 
379746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
379746     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.5ns 
379747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
382946     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
382946     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
383953     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
383987     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.82ms 
383989     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
383989     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 147.8ns 
383990     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
387154     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
387154     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
388158     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
388187     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.46ms 
388189     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
388189     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 260.2ns 
388190     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
391288     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
391288     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
392305     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
392327     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.38ms 
392328     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
392328     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.2ns 
392329     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
395509     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
395509     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
396516     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
396525     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.96ms 
396526     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
396527     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64ns 
396527     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
399643     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
399644     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
400648     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
400662     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.73ms 
400664     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
400664     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.7ns 
400665     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
403812     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
403813     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
404807     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
404811     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.99ms 
404813     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
404814     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 245ns 
404815     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
407965     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
407965     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
408958     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
408961     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 669.89ns 
408962     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
408963     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.3ns 
408963     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
412110     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
412110     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
413093     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
413096     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.04ms 
413097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
413098     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.5ns 
413099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
416220     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
416220     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
417213     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
417222     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.52ms 
417224     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
417224     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71ns 
417224     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
420320     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
420320     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
421319     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
421325     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.41ms 
421327     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
421327     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.5ns 
421328     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
424416     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
424416     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
425406     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
425419     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.16ms 
425420     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
425420     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79ns 
425421     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
428552     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
428552     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
429565     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
429569     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.18ms 
429570     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
429570     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 137.6ns 
429571     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
432699     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
432699     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
433778     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
433781     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 521.5ns 
433782     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
433782     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.3ns 
433783     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
436879     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
436880     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
437909     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
437919     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.33ms 
437921     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
437921     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 216.1ns 
437923     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
441053     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
441053     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
442070     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
442073     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 737.59ns 
442074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
442074     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.5ns 
442075     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
445226     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
445227     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
446195     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
446198     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 762.19ns 
446200     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
446200     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.2ns 
446201     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
449300     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
449301     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
450314     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
450317     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 690.8ns 
450319     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
450319     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 120.9ns 
450320     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
453427     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
453429     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
454438     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
454442     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.11ms 
454443     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
454443     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.7ns 
454444     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
457496     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
457497     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
458495     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
458511     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.57ms 
458513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
458513     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.8ns 
458514     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
461685     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
461686     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
462703     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
462708     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.14ms 
462710     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
462710     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.5ns 
462711     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
465835     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
465835     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
466848     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
466855     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.29ms 
466857     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
466857     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 159.2ns 
466857     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
469916     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
469916     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
470926     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
470931     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.73ms 
470932     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
470932     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.5ns 
470933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
474050     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
474050     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
475080     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
475096     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.24ms 
475097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
475097     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.1ns 
475098     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
478216     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
478216     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
479212     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
479217     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.08ms 
479218     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
479218     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.7ns 
479219     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
482321     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
482321     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
483306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
483310     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.26ms 
483311     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
483311     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.1ns 
483312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
486482     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
486482     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
487489     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
487494     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.17ms 
487495     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
487495     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.8ns 
487496     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
490674     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
490674     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
491656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
491673     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.54ms 
491675     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
491675     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.2ns 
491675     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
494854     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
494854     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
495874     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
495880     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 465.1ns 
495882     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
495882     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.9ns 
495883     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
499004     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
499004     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
500006     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
500053     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.35ms 
500054     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
500054     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.9ns 
500055     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
503197     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
503197     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
504191     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
504195     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.9ms 
504196     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
504196     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.1ns 
504197     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
507301     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
507301     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
508306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
508330     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.55ms 
508332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
508332     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 221.7ns 
508333     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
511484     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
511484     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
512493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
512521     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.92ms 
512523     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
512523     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 207.9ns 
512525     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
515617     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
515617     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
516630     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
516654     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.08ms 
516656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
516656     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 132.5ns 
516656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
519824     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
519824     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
520875     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
520878     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 655.9ns 
520880     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
520880     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.6ns 
520881     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
523947     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
523947     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
524872     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
524879     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.47ms 
524880     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
524880     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.8ns 
524881     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
527883     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
527883     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
528885     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
528889     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.77ms 
528891     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
528892     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 236.3ns 
528893     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
532809     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.92s 
532810     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
533816     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
533819     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.14ms 
533821     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
533821     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.6ns 
533822     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
536802     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
536802     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
537767     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
537770     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 935.99ns 
537772     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
537772     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.6ns 
537772     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
540689     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
540689     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
541643     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
541646     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.53ms 
541648     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
541648     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.5ns 
541649     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
544588     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
544588     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
545520     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
545523     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.41ms 
545524     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
545524     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.2ns 
545525     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
548479     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
548480     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
549397     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
549415     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.2ms 
549419     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
549419     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66ns 
549422     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
552377     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
552377     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
553398     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
553408     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.72ms 
553409     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
553409     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65ns 
553410     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
556296     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
556296     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
557286     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
557293     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.39ms 
557294     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
557295     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.6ns 
557295     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
560194     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
560194     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
561167     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
561182     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.07ms 
561187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
561187     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 248ns 
561188     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
564105     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
564105     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
565093     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
565099     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.33ms 
565101     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
565102     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 243.9ns 
565103     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
568042     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
568042     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
568963     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
568968     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.9ms 
568969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
568969     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.6ns 
568970     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
571893     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
571894     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
572871     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
572876     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.64ms 
572877     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
572877     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.2ns 
572878     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
575810     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
575810     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
576820     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
576824     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.82ms 
576825     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
576826     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.1ns 
576826     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
579877     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
579877     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
580850     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
580853     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.32ms 
580855     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
580855     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.2ns 
580856     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
583848     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
583848     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
584790     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
584801     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.43ms 
584802     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
584802     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71ns 
584803     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
587756     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
587756     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
588714     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
588718     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.92ms 
588719     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
588719     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.9ns 
588720     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
591608     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
591609     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
592595     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
592603     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.63ms 
592605     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
592605     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 273.8ns 
592606     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
595534     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
595534     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
596478     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
596480     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 998.29ns 
596481     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
596482     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.3ns 
596482     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
599378     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
599378     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
600346     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
600349     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 972.89ns 
600350     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
600351     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.6ns 
600351     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
603241     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
603241     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
604186     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
604190     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.74ms 
604191     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
604191     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.1ns 
604192     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
607081     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
607081     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
608041     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
608044     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 941.19ns 
608045     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
608045     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.5ns 
608046     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
610952     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
610953     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
611879     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
611882     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.35ms 
611884     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
611884     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.6ns 
611884     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
614849     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
614849     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
615847     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
615851     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.24ms 
615852     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
615852     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.1ns 
615853     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
618869     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
618869     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
619860     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
619865     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.78ms 
619866     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
619866     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.9ns 
619867     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
622848     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
622848     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
623846     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
623849     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.35ms 
623851     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
623851     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.1ns 
623852     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
626793     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
626793     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
627746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
627759     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.3ms 
627760     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
627761     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.5ns 
627761     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
630644     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
630644     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
631610     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
631612     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 726.77ns 
631614     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
631614     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.1ns 
631614     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
634494     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
634494     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
635458     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
635465     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.63ms 
635466     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
635467     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.2ns 
635467     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
638469     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
638469     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
639445     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
639447     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.02ms 
639449     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
639449     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52ns 
639449     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
642406     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
642406     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
643369     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
643372     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 860.79ns 
643373     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
643373     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.1ns 
643374     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
646360     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
646360     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
647316     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
647320     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.72ms 
647322     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
647322     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.7ns 
647323     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
650259     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
650259     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
651207     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
651211     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.58ms 
651214     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
651214     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 256.8ns 
651215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
654165     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
654165     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
655117     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
655125     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.01ms 
655126     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
655126     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.4ns 
655127     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
658110     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
658110     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
659061     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
659065     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.6ms 
659066     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
659066     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.3ns 
659067     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
661985     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
661986     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
662944     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
662949     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.49ms 
662950     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
662951     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.6ns 
662952     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
665882     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
665883     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
666876     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
666887     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.77ms 
666888     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
666888     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.8ns 
666889     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
669939     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
669939     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
670949     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
670960     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.63ms 
670961     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
670961     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.5ns 
670962     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
674054     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
674054     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
675039     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
675048     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.59ms 
675050     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
675050     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.1ns 
675051     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
677998     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
677998     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
678968     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
678978     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.69ms 
678979     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
678979     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.3ns 
678980     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
682323     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.34s 
682324     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
683499     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
683513     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.27ms 
683515     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
683515     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.9ns 
683516     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
686808     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 
686808     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
687862     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
687877     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.93ms 
687878     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
687878     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.7ns 
687879     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
690894     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
690894     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
691905     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
691919     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.72ms 
691920     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
691920     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.7ns 
691921     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
695116     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
695117     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
696305     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
696318     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.78ms 
696322     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
696322     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 261.8ns 
696323     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
699597     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 
699597     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
700604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
700629     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.82ms 
700631     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
700631     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.2ns 
700632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
703689     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
703689     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
704712     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
704748     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.41ms 
704750     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
704750     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.3ns 
704751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
707886     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
707886     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
708927     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
708953     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.06ms 
708955     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
708955     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.7ns 
708956     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
711958     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
711958     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
713043     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
713074     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.29ms 
713076     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
713076     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.8ns 
713077     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
716221     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
716221     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
717250     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
717275     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.02ms 
717276     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
717276     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.9ns 
717277     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
720441     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
720441     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
721493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
721557     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 56.85ms 
721559     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
721559     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.3ns 
721560     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
724696     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
724696     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
725749     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
725757     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.6ms 
725759     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
725760     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 184.6ns 
725760     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
728969     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
728969     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
730051     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
730058     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.91ms 
730060     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
730060     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.6ns 
730060     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
733168     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
733168     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
734245     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
734249     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.68ms 
734251     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
734251     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.1ns 
734252     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
737341     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
737341     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
738353     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
738375     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.98ms 
738377     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
738377     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95ns 
738378     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
741522     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
741522     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
742542     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
742553     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.74ms 
742554     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
742555     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76ns 
742556     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
745667     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
745667     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
746667     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
746670     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.56ms 
746672     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
746672     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 129.5ns 
746673     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
750163     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.49s 
750163     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
751182     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
751195     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.25ms 
751196     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
751196     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.5ns 
751197     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
754162     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
754162     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
755140     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
755154     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.3ms 
755155     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
755155     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.8ns 
755156     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
758120     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
758121     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
759086     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
759106     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.63ms 
759109     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
759109     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 194.6ns 
759110     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
762046     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
762046     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
763024     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
763028     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.59ms 
763029     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
763029     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.2ns 
763030     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
765975     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
765975     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
766945     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
766950     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.62ms 
766952     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
766952     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.5ns 
766952     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
769941     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
769941     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
770908     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
770915     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.22ms 
770917     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
770917     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.2ns 
770917     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
773954     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
773954     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
774940     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
774947     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.1ms 
774948     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
774948     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.7ns 
774949     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
778036     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
778037     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
779012     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
779070     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 50.91ms 
779072     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
779072     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.8ns 
779073     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
782012     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
782012     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
782992     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
783026     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.39ms 
783029     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
783029     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 217.3ns 
783030     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
786022     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
786022     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
787031     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
787048     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.53ms 
787050     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
787050     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.4ns 
787050     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
789992     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
789992     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
790966     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
790968     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 291ns 
790971     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
790971     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 218.8ns 
790973     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
793985     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
793985     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
794951     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
795086     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 122.2ms 
795089     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
795089     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 165.5ns 
795090     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
798067     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
798067     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
799035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
799077     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.41ms 
799079     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
799079     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.9ns 
799080     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
802060     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
802060     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
803016     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
803019     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 526.5ns 
803021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
803021     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.2ns 
803021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
805957     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
805957     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
806930     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
806932     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 353.9ns 
806934     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
806934     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.2ns 
806934     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
809870     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
809870     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
810843     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
810845     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 291.2ns 
810846     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
810846     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.4ns 
810847     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
813780     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
813780     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
814731     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
814733     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 397.6ns 
814735     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
814735     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.4ns 
814736     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
817689     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
817689     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
818641     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
818745     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
818759     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 114.62ms 
818762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
818762     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 215.4ns 
818763     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
821747     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
821747     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
822735     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
822787     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
822789     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 52.42ms 
822791     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
822791     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.6ns 
822792     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
825702     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
825702     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
826692     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
826694     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.7ns 
826732     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 49, command: 'macro split-prop' 
826796     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [2] goal: 3, source line: 50, command: 'rule allRight' 
826812     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [3] goal: 4, source line: 51, command: 'rule allRight' 
826819     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [4] goal: 5, source line: 52, command: 'macro split-prop' 
826836     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [5] goal: 11, source line: 53, command: 'rule 'seqPermDefLeft'' 
826837     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [6] goal: 12, source line: 54, command: 'rule 'andLeft'' 
826840     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [7] goal: 13, source line: 55, command: 'rule 'exLeft'' 
826841     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [8] goal: 14, source line: 56, command: 'macro split-prop' 
826849     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [9] goal: 16, source line: 57, command: 'rule  seqNPermRange' 
826852     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [10] goal: 17, source line: 59, command: 'instantiate var=iv with='v_x_0' occ=1' 
826856     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [11] goal: 18, source line: 60, command: 'rule impLeft' 
826860     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [12] goal: 19, source line: 61, command: 'tryclose branch' 
827136     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [13] goal: 20, source line: 62, command: 'rule andLeft' 
827138     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [14] goal: 97, source line: 63, command: 'rule andLeft' 
827141     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [15] goal: 98, source line: 64, command: 'instantiate var=iv with='v_y_0' occ=1' 
827142     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [16] goal: 99, source line: 66, command: 'rule impLeft' 
827143     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [17] goal: 100, source line: 67, command: 'tryclose branch' 
827319     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [18] goal: 101, source line: 68, command: 'rule andLeft' 
827320     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [19] goal: 188, source line: 69, command: 'rule andLeft' 
827324     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [20] goal: 189, source line: 70, command: 'rule seqNPermDefLeft' 
827325     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [21] goal: 190, source line: 72, command: 'instantiate var=iv with='v_x_0' occ=2' 
827326     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [22] goal: 191, source line: 73, command: 'rule impLeft' 
827329     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [23] goal: 192, source line: 74, command: 'tryclose branch' 
827578     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [24] goal: 193, source line: 75, command: 'rule exLeft' 
827581     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [25] goal: 310, source line: 76, command: 'rule andLeft' 
827582     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [26] goal: 311, source line: 77, command: 'rule andLeft' 
827583     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [27] goal: 312, source line: 78, command: 'instantiate hide var=iv with='v_y_0' occ=2' 
827584     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [28] goal: 313, source line: 80, command: 'rule impLeft' 
827587     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [29] goal: 314, source line: 81, command: 'tryclose branch' 
827766     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [30] goal: 315, source line: 82, command: 'rule exLeft' 
827769     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [31] goal: 420, source line: 83, command: 'rule andLeft' 
827770     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [32] goal: 421, source line: 84, command: 'rule andLeft' 
827771     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [33] goal: 422, source line: 85, command: 'instantiate var=iv with='jv_0' occ=1' 
827772     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [34] goal: 423, source line: 87, command: 'rule impLeft' 
827773     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [35] goal: 424, source line: 88, command: 'tryclose branch' 
827783     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [36] goal: 425, source line: 89, command: 'rule andLeft' 
827783     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [37] goal: 434, source line: 90, command: 'rule andLeft' 
827786     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [38] goal: 435, source line: 91, command: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
827787     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [39] goal: 436, source line: 92, command: 'instantiate hide var=iv with='jv_1' occ=1' 
827789     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [40] goal: 437, source line: 94, command: 'rule impLeft' 
827791     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [41] goal: 438, source line: 95, command: 'tryclose branch' 
827802     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [42] goal: 439, source line: 96, command: 'rule andLeft' 
827803     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [43] goal: 448, source line: 97, command: 'rule andLeft' 
827804     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [44] goal: 449, source line: 98, command: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
827805     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [45] goal: 450, source line: 99, command: 'instantiate var=iv  with='v_x_0'' 
827807     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [46] goal: 451, source line: 101, command: 'rule impLeft' 
827808     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [47] goal: 452, source line: 102, command: 'tryclose branch' 
827988     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [48] goal: 453, source line: 103, command: 'instantiate var=iv  with='v_y_0'' 
827990     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [49] goal: 562, source line: 105, command: 'rule impLeft' 
827991     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [50] goal: 563, source line: 106, command: 'tryclose branch' 
828138     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [51] goal: 564, source line: 107, command: 'cut 'v_x_0 = v_y_0'' 
828139     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [52] goal: 674, source line: 109, command: 'instantiate hide var='v_r' with='seqSwap(s_0,v_x_0,jv_0)'' 
828141     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [53] goal: 676, source line: 111, command: 'rule andRight' 
828143     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [54] goal: 677, source line: 113, command: 'rule andRight' 
828144     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [55] goal: 679, source line: 114, command: 'rule andRight' 
828145     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [56] goal: 681, source line: 115, command: 'rule andRight' 
828146     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [57] goal: 683, source line: 116, command: 'rule lenOfSwap' 
828146     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [58] goal: 685, source line: 117, command: 'tryclose branch' 
828154     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [59] goal: 684, source line: 118, command: 'rule seqNPermSwapNPerm' 
828155     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [60] goal: 687, source line: 120, command: 'instantiate hide var='iv' with='v_x_0' occ=1' 
828156     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [61] goal: 688, source line: 121, command: 'instantiate hide var='jv' with='jv_0'' 
828158     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [62] goal: 689, source line: 122, command: 'rule impLeft' 
828159     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [63] goal: 690, source line: 123, command: 'tryclose branch' 
828290     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [64] goal: 691, source line: 124, command: 'tryclose branch' 
828295     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [65] goal: 682, source line: 125, command: 'rule allRight' 
828296     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [66] goal: 796, source line: 127, command: 'rule impRight' 
828297     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [67] goal: 797, source line: 128, command: 'rule andLeft' 
828298     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [68] goal: 798, source line: 129, command: 'instantiate var=iv with='v_iv_0'' 
828299     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [69] goal: 799, source line: 130, command: 'rule impLeft' 
828300     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [70] goal: 800, source line: 131, command: 'tryclose branch' 
828460     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [71] goal: 801, source line: 132, command: 'rule getOfSwap' 
828462     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [72] goal: 912, source line: 133, command: 'rule ifthenelse_negated' 
828463     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [73] goal: 913, source line: 134, command: 'rule ifthenelse_split occ=0' 
828465     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [74] goal: 914, source line: 135, command: 'rule andLeft' 
828467     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [75] goal: 916, source line: 136, command: 'rule andLeft' 
828468     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [76] goal: 917, source line: 137, command: 'rule andLeft' 
828469     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [77] goal: 918, source line: 138, command: 'rule ifthenelse_split occ=0' 
828470     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [78] goal: 919, source line: 139, command: 'tryclose branch' 
828576     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [79] goal: 920, source line: 140, command: 'rule ifthenelse_split occ=0' 
828577     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [80] goal: 1011, source line: 141, command: 'tryclose branch' 
828684     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [81] goal: 1012, source line: 142, command: 'tryclose branch' 
828690     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [82] goal: 915, source line: 143, command: 'tryclose branch' 
828695     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [83] goal: 680, source line: 144, command: 'rule getOfSwap' 
828696     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [84] goal: 1099, source line: 146, command: 'rule ifthenelse_negated' 
828697     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [85] goal: 1100, source line: 147, command: 'rule ifthenelse_split occ=0' 
828699     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [86] goal: 1101, source line: 148, command: 'rule andLeft' 
828700     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [87] goal: 1103, source line: 149, command: 'rule andLeft' 
828700     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [88] goal: 1104, source line: 150, command: 'rule andLeft' 
828702     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [89] goal: 1105, source line: 151, command: 'rule ifthenelse_split occ=0' 
828703     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [90] goal: 1106, source line: 152, command: 'tryclose branch' 
828712     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [91] goal: 1107, source line: 153, command: 'tryclose branch' 
828717     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [92] goal: 1102, source line: 154, command: 'tryclose branch' 
828828     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [93] goal: 678, source line: 155, command: 'rule getOfSwap' 
828830     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [94] goal: 1225, source line: 157, command: 'rule ifthenelse_negated' 
828831     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [95] goal: 1226, source line: 158, command: 'rule ifthenelse_split occ=0' 
828832     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [96] goal: 1227, source line: 159, command: 'rule andLeft' 
828833     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [97] goal: 1229, source line: 160, command: 'rule andLeft' 
828834     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [98] goal: 1230, source line: 161, command: 'rule andLeft' 
828834     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [99] goal: 1231, source line: 162, command: 'rule ifthenelse_split occ=0' 
828835     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [100] goal: 1232, source line: 163, command: 'tryclose branch' 
828890     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [101] goal: 1233, source line: 164, command: 'tryclose branch' 
828897     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [102] goal: 1228, source line: 165, command: 'tryclose branch' 
829012     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [103] goal: 675, source line: 166, command: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
829013     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [104] goal: 1397, source line: 169, command: 'rule seqNPermInjective' 
829014     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [105] goal: 1399, source line: 170, command: 'instantiate hide var=iv with='v_x_0'' 
829016     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [106] goal: 1400, source line: 171, command: 'instantiate hide var=jv with='v_y_0'' 
829017     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [107] goal: 1401, source line: 172, command: 'rule impLeft' 
829018     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [108] goal: 1402, source line: 173, command: 'tryclose branch' 
829196     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [109] goal: 1403, source line: 174, command: 'tryclose branch' 
829202     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [110] goal: 1398, source line: 175, command: 'cut '(int)s_0[v_x_0] = v_x_0'' 
829203     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [111] goal: 1534, source line: 177, command: 'instantiate hide var=v_r with='seqSwap(s_0,v_y_0,jv_1)'' 
829204     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [112] goal: 1536, source line: 179, command: 'rule andRight' 
829257     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [113] goal: 1537, source line: 181, command: 'rule andRight' 
829258     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [114] goal: 1539, source line: 182, command: 'rule andRight' 
829258     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [115] goal: 1541, source line: 183, command: 'rule andRight' 
829259     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [116] goal: 1543, source line: 184, command: 'tryclose branch' 
829272     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [117] goal: 1544, source line: 185, command: 'rule seqNPermSwapNPerm' 
829273     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [118] goal: 1558, source line: 187, command: 'instantiate hide var=iv with='v_y_0'' 
829274     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [119] goal: 1559, source line: 188, command: 'instantiate hide var=jv with='jv_1'' 
829275     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [120] goal: 1560, source line: 189, command: 'tryclose branch' 
829400     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [121] goal: 1542, source line: 190, command: 'rule allRight' 
829407     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [122] goal: 1667, source line: 192, command: 'rule impRight' 
829409     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [123] goal: 1668, source line: 193, command: 'rule andLeft' 
829410     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [124] goal: 1669, source line: 194, command: 'instantiate var=iv with='v_iv_0'' 
829411     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [125] goal: 1670, source line: 195, command: 'rule impLeft' 
829412     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [126] goal: 1671, source line: 196, command: 'tryclose branch' 
829560     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [127] goal: 1672, source line: 197, command: 'rule getOfSwap' 
829561     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [128] goal: 1786, source line: 198, command: 'rule ifthenelse_negated' 
829562     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [129] goal: 1787, source line: 199, command: 'rule ifthenelse_split occ=0' 
829564     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [130] goal: 1788, source line: 200, command: 'rule andLeft' 
829565     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [131] goal: 1790, source line: 201, command: 'rule andLeft' 
829566     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [132] goal: 1791, source line: 202, command: 'rule andLeft' 
829567     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [133] goal: 1792, source line: 203, command: 'rule ifthenelse_split occ=0' 
829568     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [134] goal: 1793, source line: 204, command: 'tryclose branch' 
829673     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [135] goal: 1794, source line: 205, command: 'rule ifthenelse_split occ=0' 
829674     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [136] goal: 1885, source line: 206, command: 'tryclose branch' 
829764     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [137] goal: 1886, source line: 207, command: 'instantiate var=iv with='v_y_0'' 
829765     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [138] goal: 1968, source line: 208, command: 'rule impLeft' 
829766     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [139] goal: 1969, source line: 209, command: 'tryclose branch' 
829770     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [140] goal: 1970, source line: 210, command: 'tryclose branch' 
829775     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [141] goal: 1789, source line: 211, command: 'tryclose branch' 
829781     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [142] goal: 1540, source line: 212, command: 'tryclose branch' 
829929     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [143] goal: 1538, source line: 213, command: 'rule getOfSwap' 
829930     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [144] goal: 2097, source line: 215, command: 'rule ifthenelse_negated' 
829931     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [145] goal: 2098, source line: 216, command: 'rule ifthenelse_split occ=0' 
829932     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [146] goal: 2099, source line: 217, command: 'tryclose branch' 
829944     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [147] goal: 2100, source line: 218, command: 'tryclose branch' 
830046     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [148] goal: 1535, source line: 219, command: 'tryclose branch' 
834178     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [149] goal: 1535, source line: 221, command: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
834179     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [150] goal: 4266, source line: 224, command: 'instantiate hide var=v_r with='seqSwap(s_0,v_x_0,jv_0)'' 
834184     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [151] goal: 4268, source line: 226, command: 'rule andRight' 
834186     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [152] goal: 4269, source line: 228, command: 'rule andRight' 
834186     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [153] goal: 4271, source line: 229, command: 'rule andRight' 
834187     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [154] goal: 4273, source line: 230, command: 'rule andRight' 
834188     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [155] goal: 4275, source line: 231, command: 'tryclose branch' 
834199     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [156] goal: 4276, source line: 232, command: 'rule seqNPermSwapNPerm' 
834200     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [157] goal: 4287, source line: 234, command: 'instantiate hide var=iv with='v_x_0'' 
834201     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [158] goal: 4288, source line: 235, command: 'instantiate hide var=jv with='jv_0'' 
834202     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [159] goal: 4289, source line: 236, command: 'rule impLeft' 
834203     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [160] goal: 4290, source line: 237, command: 'tryclose branch' 
834322     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [161] goal: 4291, source line: 238, command: 'tryclose branch' 
834326     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [162] goal: 4274, source line: 239, command: 'rule allRight' 
834327     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [163] goal: 4400, source line: 241, command: 'rule impRight' 
834328     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [164] goal: 4401, source line: 242, command: 'rule andLeft' 
834329     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [165] goal: 4402, source line: 243, command: 'instantiate var=iv with='v_iv_0'' 
834330     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [166] goal: 4403, source line: 244, command: 'rule impLeft' 
834331     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [167] goal: 4404, source line: 245, command: 'tryclose branch' 
834495     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [168] goal: 4405, source line: 246, command: 'rule getOfSwap' 
834497     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [169] goal: 4521, source line: 247, command: 'rule ifthenelse_negated' 
834498     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [170] goal: 4522, source line: 248, command: 'rule ifthenelse_split occ=0' 
834499     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [171] goal: 4523, source line: 249, command: 'rule andLeft' 
834500     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [172] goal: 4525, source line: 250, command: 'rule andLeft' 
834500     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [173] goal: 4526, source line: 251, command: 'rule andLeft' 
834501     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [174] goal: 4527, source line: 252, command: 'rule ifthenelse_split occ=0' 
834502     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [175] goal: 4528, source line: 253, command: 'tryclose branch' 
834587     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [176] goal: 4529, source line: 254, command: 'rule ifthenelse_split occ=0' 
834588     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [177] goal: 4622, source line: 255, command: 'tryclose branch' 
834669     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [178] goal: 4623, source line: 256, command: 'tryclose branch' 
834674     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [179] goal: 4524, source line: 257, command: 'tryclose branch' 
834679     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [180] goal: 4272, source line: 258, command: 'rule getOfSwap' 
834679     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [181] goal: 4713, source line: 260, command: 'rule ifthenelse_negated' 
834680     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [182] goal: 4714, source line: 261, command: 'rule ifthenelse_split occ=0' 
834681     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [183] goal: 4715, source line: 262, command: 'tryclose branch' 
834693     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [184] goal: 4716, source line: 263, command: 'tryclose branch' 
834783     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [185] goal: 4270, source line: 264, command: 'rule getOfSwap' 
834784     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [186] goal: 4839, source line: 266, command: 'rule ifthenelse_negated' 
834785     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [187] goal: 4840, source line: 267, command: 'rule ifthenelse_split occ=0' 
834785     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [188] goal: 4841, source line: 268, command: 'tryclose branch' 
834872     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [189] goal: 4842, source line: 269, command: 'tryclose branch' 
834883     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [190] goal: 4267, source line: 270, command: 'cut '(int)s_0[v_x_0]=v_y_0'' 
834884     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [191] goal: 4948, source line: 273, command: 'instantiate hide var=v_r with='seqSwap(seqSwap(s_0,jv_0,v_x_0),jv_0,v_y_0)'' 
834885     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [192] goal: 4950, source line: 275, command: 'rule andRight' 
834887     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [193] goal: 4951, source line: 277, command: 'rule andRight' 
834887     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [194] goal: 4953, source line: 278, command: 'rule andRight' 
834888     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [195] goal: 4955, source line: 279, command: 'rule andRight' 
834888     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [196] goal: 4957, source line: 280, command: 'tryclose branch' 
834901     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [197] goal: 4958, source line: 281, command: 'rule seqNPermSwapNPerm' 
834902     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [198] goal: 4977, source line: 283, command: 'instantiate hide var=iv with='jv_0'' 
834903     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [199] goal: 4978, source line: 284, command: 'instantiate hide var=jv with='v_x_0'' 
834904     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [200] goal: 4979, source line: 285, command: 'rule impLeft' 
834905     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [201] goal: 4980, source line: 286, command: 'tryclose branch' 
835003     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [202] goal: 4981, source line: 287, command: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
835004     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [203] goal: 5093, source line: 288, command: 'instantiate hide var=iv with='jv_0'' 
835008     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [204] goal: 5094, source line: 289, command: 'instantiate hide var=jv with='v_y_0'' 
835010     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [205] goal: 5095, source line: 290, command: 'rule impLeft' 
835011     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [206] goal: 5096, source line: 291, command: 'tryclose branch' 
835113     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [207] goal: 5097, source line: 292, command: 'tryclose branch' 
835118     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [208] goal: 4956, source line: 293, command: 'rule allRight' 
835119     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [209] goal: 5212, source line: 295, command: 'rule impRight' 
835120     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [210] goal: 5213, source line: 296, command: 'rule andLeft' 
835121     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [211] goal: 5214, source line: 297, command: 'instantiate var=iv with='v_iv_0'' 
835121     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [212] goal: 5215, source line: 300, command: 'rule impLeft' 
835122     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [213] goal: 5216, source line: 301, command: 'tryclose branch' 
835234     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [214] goal: 5217, source line: 302, command: 'rule getOfSwap' 
835235     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [215] goal: 5337, source line: 304, command: 'rule ifthenelse_negated' 
835237     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [216] goal: 5338, source line: 305, command: 'rule ifthenelse_split occ=0' 
835238     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [217] goal: 5339, source line: 306, command: 'rule andLeft' 
835238     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [218] goal: 5341, source line: 307, command: 'rule andLeft' 
835239     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [219] goal: 5342, source line: 308, command: 'rule andLeft' 
835239     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [220] goal: 5343, source line: 309, command: 'rule ifthenelse_split occ=0' 
835240     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [221] goal: 5344, source line: 310, command: 'rule getOfSwap' 
835240     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [222] goal: 5346, source line: 311, command: 'rule ifthenelse_negated' 
835241     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [223] goal: 5347, source line: 312, command: 'rule ifthenelse_split occ=0' 
835242     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [224] goal: 5348, source line: 313, command: 'rule andLeft' 
835242     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [225] goal: 5350, source line: 314, command: 'rule andLeft' 
835243     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [226] goal: 5351, source line: 315, command: 'rule andLeft' 
835243     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [227] goal: 5352, source line: 316, command: 'rule ifthenelse_split occ=0' 
835244     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [228] goal: 5353, source line: 317, command: 'tryclose branch' 
835342     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [229] goal: 5354, source line: 318, command: 'rule ifthenelse_split occ=0' 
835343     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [230] goal: 5463, source line: 319, command: 'tryclose branch' 
835350     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [231] goal: 5464, source line: 320, command: 'tryclose branch' 
835441     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [232] goal: 5349, source line: 321, command: 'tryclose branch' 
835536     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [233] goal: 5345, source line: 322, command: 'rule ifthenelse_split' 
835537     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [234] goal: 5660, source line: 324, command: 'rule getOfSwap' 
835538     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [235] goal: 5662, source line: 325, command: 'rule ifthenelse_negated' 
835539     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [236] goal: 5663, source line: 326, command: 'rule ifthenelse_split occ=0' 
835540     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [237] goal: 5664, source line: 327, command: 'rule andLeft' 
835540     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [238] goal: 5666, source line: 328, command: 'rule andLeft' 
835541     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [239] goal: 5667, source line: 329, command: 'rule andLeft' 
835541     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [240] goal: 5668, source line: 330, command: 'rule ifthenelse_split occ=0' 
835542     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [241] goal: 5669, source line: 331, command: 'tryclose branch' 
835642     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [242] goal: 5670, source line: 332, command: 'tryclose branch' 
835649     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [243] goal: 5665, source line: 333, command: 'tryclose branch' 
835760     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [244] goal: 5661, source line: 334, command: 'rule getOfSwap' 
835761     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [245] goal: 5887, source line: 336, command: 'rule ifthenelse_negated' 
835762     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [246] goal: 5888, source line: 337, command: 'rule ifthenelse_split occ=0' 
835764     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [247] goal: 5889, source line: 338, command: 'rule andLeft' 
835764     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [248] goal: 5891, source line: 339, command: 'rule andLeft' 
835765     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [249] goal: 5892, source line: 340, command: 'rule andLeft' 
835765     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [250] goal: 5893, source line: 341, command: 'rule ifthenelse_split occ=0' 
835766     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [251] goal: 5894, source line: 342, command: 'tryclose branch' 
835772     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [252] goal: 5895, source line: 343, command: 'rule ifthenelse_split occ=0' 
835773     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [253] goal: 5897, source line: 344, command: 'tryclose branch' 
835874     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [254] goal: 5898, source line: 345, command: 'tryclose branch' 
835881     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [255] goal: 5890, source line: 346, command: 'tryclose branch' 
835887     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [256] goal: 5340, source line: 347, command: 'tryclose branch' 
836002     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [257] goal: 4954, source line: 348, command: 'rule getOfSwap' 
836002     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [258] goal: 6115, source line: 350, command: 'rule ifthenelse_negated' 
836003     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [259] goal: 6116, source line: 351, command: 'rule ifthenelse_split occ=0' 
836004     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [260] goal: 6117, source line: 352, command: 'rule andLeft' 
836005     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [261] goal: 6119, source line: 353, command: 'rule andLeft' 
836006     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [262] goal: 6120, source line: 354, command: 'rule andLeft' 
836006     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [263] goal: 6121, source line: 355, command: 'rule ifthenelse_split occ=0' 
836007     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [264] goal: 6122, source line: 356, command: 'tryclose branch' 
836073     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [265] goal: 6123, source line: 357, command: 'rule ifthenelse_split occ=0' 
836074     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [266] goal: 6193, source line: 358, command: 'rule getOfSwap' 
836075     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [267] goal: 6195, source line: 359, command: 'rule ifthenelse_negated' 
836076     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [268] goal: 6196, source line: 360, command: 'rule ifthenelse_split occ=0' 
836077     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [269] goal: 6197, source line: 361, command: 'tryclose branch' 
836083     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [270] goal: 6198, source line: 362, command: 'tryclose branch' 
836090     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [271] goal: 6194, source line: 363, command: 'tryclose branch' 
836219     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [272] goal: 6118, source line: 364, command: 'tryclose branch' 
836324     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [273] goal: 4952, source line: 365, command: 'rule getOfSwap' 
836325     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [274] goal: 6456, source line: 367, command: 'rule ifthenelse_negated' 
836326     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [275] goal: 6457, source line: 368, command: 'rule ifthenelse_split occ=0' 
836327     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [276] goal: 6458, source line: 369, command: 'tryclose branch' 
836573     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [277] goal: 6459, source line: 370, command: 'tryclose branch' 
836679     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [278] goal: 4949, source line: 371, command: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
836680     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [279] goal: 6735, source line: 375, command: 'tryclose branch' 
840046     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [280] goal: 6735, source line: 378, command: 'rule seqNPermSwapNPerm' 
840051     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [281] goal: 8783, source line: 380, command: 'instantiate hide var=iv with='jv_1'' 
840052     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [282] goal: 8784, source line: 381, command: 'instantiate hide var=jv with='v_y_0'' 
840053     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [283] goal: 8785, source line: 382, command: 'rule impLeft' 
840054     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [284] goal: 8786, source line: 383, command: 'tryclose branch' 
840182     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [285] goal: 8787, source line: 384, command: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
840183     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [286] goal: 8909, source line: 385, command: 'instantiate hide var=iv with='jv_1'' 
840184     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [287] goal: 8910, source line: 386, command: 'instantiate hide var=jv with='v_x_0'' 
840185     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [288] goal: 8911, source line: 387, command: 'rule impLeft' 
840185     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [289] goal: 8912, source line: 388, command: 'tryclose branch' 
840302     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [290] goal: 8913, source line: 389, command: 'tryclose branch' 
843620     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [291] goal: 6736, source line: 390, command: 'tryclose branch' 
847112     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [292] goal: 6736, source line: 397, command: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
847117     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [293] goal: 12633, source line: 399, command: 'instantiate hide var=iv with='v_x_0'' 
847118     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [294] goal: 12634, source line: 400, command: 'instantiate hide var=jv with='jv_0'' 
847118     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [295] goal: 12635, source line: 401, command: 'rule impLeft' 
847119     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [296] goal: 12636, source line: 402, command: 'tryclose branch' 
847249     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [297] goal: 12637, source line: 403, command: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
847250     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [298] goal: 12757, source line: 404, command: 'instantiate hide var=iv with='v_y_0'' 
847251     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [299] goal: 12758, source line: 405, command: 'instantiate hide var=jv with='jv_1'' 
847252     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [300] goal: 12759, source line: 406, command: 'instantiate hide var=v_r with='seqSwap(seqSwap(s_0, v_x_0, jv_0), v_y_0, jv_1)' ...' 
847253     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [301] goal: 12760, source line: 407, command: 'tryclose branch' 
848499     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
848499     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 192.7ns 
848500     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
851551     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
851551     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
852547     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
852549     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.8ns 
852549     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 50, command: 'macro split-prop' 
852559     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [2] goal: 10, source line: 51, command: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
852569     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [3] goal: 11, source line: 52, command: 'instantiate hide var=x with='f_x'' 
852571     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [4] goal: 12, source line: 53, command: 'instantiate hide var=y with='f_y'' 
852574     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [5] goal: 13, source line: 54, command: 'rule impLeft' 
852575     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [6] goal: 14, source line: 55, command: 'tryclose branch' 
852581     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [7] goal: 15, source line: 56, command: 'rule exLeft' 
852581     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [8] goal: 23, source line: 57, command: 'macro split-prop' 
852587     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [9] goal: 27, source line: 58, command: 'rule seqPermDef occ=1' 
852587     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [10] goal: 28, source line: 59, command: 'rule andRight' 
852589     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [11] goal: 29, source line: 60, command: 'tryclose branch' 
852601     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [12] goal: 30, source line: 61, command: 'instantiate hide var=s with='r_0'' 
852602     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [13] goal: 46, source line: 62, command: 'rule andRight' 
852603     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [14] goal: 47, source line: 63, command: 'tryclose branch' 
852661     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [15] goal: 48, source line: 64, command: 'rule allRight' 
852662     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [16] goal: 119, source line: 65, command: 'rule impRight' 
852663     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [17] goal: 120, source line: 66, command: 'instantiate hide var=iv with='iv_0'' 
852663     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [18] goal: 121, source line: 67, command: 'rule impLeft' 
852664     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [19] goal: 122, source line: 68, command: 'tryclose branch' 
852744     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [20] goal: 123, source line: 69, command: 'rule andLeft' 
852745     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [21] goal: 203, source line: 70, command: 'rule seqNPermRange' 
852745     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [22] goal: 204, source line: 71, command: 'instantiate hide var=iv with='iv_0'' 
852746     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [23] goal: 205, source line: 72, command: 'rule impLeft' 
852747     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [24] goal: 206, source line: 73, command: 'tryclose branch' 
852753     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [25] goal: 207, source line: 74, command: 'rule andLeft' 
852753     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [26] goal: 215, source line: 75, command: 'rule andLeft' 
852753     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [27] goal: 216, source line: 76, command: 'rule seqNPermRange' 
852754     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [28] goal: 217, source line: 77, command: 'instantiate hide var=iv with='f_x'' 
852755     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [29] goal: 218, source line: 78, command: 'rule impLeft' 
852756     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [30] goal: 219, source line: 79, command: 'tryclose branch' 
852871     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [31] goal: 220, source line: 80, command: 'rule andLeft' 
852872     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [32] goal: 311, source line: 81, command: 'rule andLeft' 
852872     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [33] goal: 312, source line: 82, command: 'rule seqNPermRange' 
852873     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [34] goal: 313, source line: 83, command: 'instantiate hide var=iv with='f_y'' 
852874     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [35] goal: 314, source line: 84, command: 'rule impLeft' 
852875     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [36] goal: 315, source line: 85, command: 'tryclose branch' 
853024     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [37] goal: 316, source line: 86, command: 'rule andLeft' 
853024     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [38] goal: 410, source line: 87, command: 'rule andLeft' 
853025     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [39] goal: 411, source line: 88, command: 'rule getOfSeqDef occ=0' 
853025     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [40] goal: 412, source line: 89, command: 'rule getOfSeqDef' 
853026     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [41] goal: 413, source line: 90, command: 'rule ifthenelse_split occ=0' 
853027     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [42] goal: 414, source line: 91, command: 'rule andLeft occ=0' 
853028     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [43] goal: 416, source line: 92, command: 'rule sub_zero_2 occ=0' 
853028     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [44] goal: 417, source line: 93, command: 'rule ifthenelse_split occ=2' 
853029     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [45] goal: 418, source line: 94, command: 'rule andLeft' 
853030     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [46] goal: 420, source line: 95, command: 'rule sub_zero_2 occ=0' 
853030     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [47] goal: 421, source line: 96, command: 'rule add_zero_right occ=0' 
853030     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [48] goal: 422, source line: 97, command: 'rule add_zero_right occ=0' 
853031     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [49] goal: 423, source line: 98, command: 'rule add_zero_right occ=0' 
853031     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [50] goal: 424, source line: 99, command: 'rule add_zero_right occ=0' 
853032     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [51] goal: 425, source line: 100, command: 'rule add_zero_right occ=0' 
853032     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [52] goal: 426, source line: 101, command: 'rule add_zero_right occ=0' 
853033     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [53] goal: 427, source line: 102, command: 'rule ifthenelse_split occ=0' 
853033     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [54] goal: 428, source line: 103, command: 'rule ifthenelse_split occ=0' 
853034     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [55] goal: 430, source line: 104, command: 'tryclose branch' 
853037     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [56] goal: 431, source line: 105, command: 'tryclose branch' 
853093     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [57] goal: 429, source line: 106, command: 'rule ifthenelse_split occ=0' 
853094     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [58] goal: 473, source line: 107, command: 'tryclose branch' 
853176     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [59] goal: 474, source line: 108, command: 'rule ifthenelse_split occ=0' 
853177     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [60] goal: 541, source line: 109, command: 'rule seqNPermInjective' 
853177     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [61] goal: 543, source line: 110, command: 'instantiate hide var=iv with='iv_0'' 
853179     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [62] goal: 544, source line: 111, command: 'instantiate hide var=jv with='f_y'' 
853180     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [63] goal: 545, source line: 112, command: 'rule impLeft' 
853181     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [64] goal: 546, source line: 113, command: 'tryclose branch' 
853242     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [65] goal: 547, source line: 114, command: 'tryclose branch' 
853245     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [66] goal: 542, source line: 115, command: 'rule ifthenelse_split occ=0' 
853246     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [67] goal: 606, source line: 116, command: 'rule seqNPermInjective' 
853247     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [68] goal: 608, source line: 117, command: 'instantiate hide var=iv with='iv_0'' 
853248     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [69] goal: 609, source line: 118, command: 'instantiate hide var=jv with='f_x'' 
853249     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [70] goal: 610, source line: 119, command: 'rule impLeft' 
853250     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [71] goal: 611, source line: 120, command: 'tryclose branch' 
853311     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [72] goal: 612, source line: 121, command: 'tryclose branch' 
853314     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [73] goal: 607, source line: 122, command: 'tryclose branch' 
853318     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [74] goal: 419, source line: 123, command: 'tryclose branch' 
853390     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [75] goal: 415, source line: 124, command: 'tryclose branch' 
853456     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
853456     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 150ns 
853457     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
856439     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
856439     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
857508     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
857534     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.9ms